Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Jump to bottom

Overloads with free variables cause unexportable theory #115

Closed
mn200 opened this issue Apr 13, 2013 · 2 comments
Closed

Overloads with free variables cause unexportable theory #115

mn200 opened this issue Apr 13, 2013 · 2 comments
Labels
Bug Kernel Printing-Parsing

Comments

@mn200
Copy link
Member

mn200 commented Apr 13, 2013

The following results in a theory that fails to export correctly:

val _ = overload_on ("foo", ``\x. x + y``)

val sample = store_thm(
  "sample",
  ``!y:bool. foo x < foo z ==> x < z``,
  SRW_TAC [ARITH_ss][])

val _ = export_theory()

The theorem sample proves OK but the call to export_theory fails with a NotFound exception.
mn200 added a commit that referenced this issue Apr 13, 2013
@mn200
A test-case demonstrating the problem with github issue #115.
ce19025 
Currently failing so I've put this onto a branch of its own.
@mn200
Copy link
Member Author

mn200 commented Apr 13, 2013

Incidentally, overloads are supposed to be able to have free variables. It makes doing some group (algebra) theory much smoother because you can do things like

val _ = overload_on ("+", ``G.op``)

where G is of type :α group and a bit like a “locale parameter”.

@mn200
Copy link
Member Author

mn200 commented Apr 13, 2013

I should also note that this bug was stumbled upon by Joseph Chan.

mn200 added a commit that referenced this issue Apr 26, 2013
@mn200
Move issue #115 test-case to much earlier in the build sequence.
6665111
mn200 added a commit that referenced this issue Apr 26, 2013
@mn200
Simplify the issue #115 test-case.
91b7f2b 
The problem arises in the standard kernel (only) when a term has a
bound variable of name n with scope over a different variable of the
same name (i.e., there is a free variable of the same name but a
different type under the binder).

Fundamentally, the issue is that the standard kernel’s dest_abs
necessarily traverses the body of a term in order to turn indexes into
free vars. In the process it detects if it is about to create a term
with free variables of same names and different types. In that
situation it renames the bound variable and repeats. Perhaps this is a
mis-design.
@mn200 mn200 closed this as completed in 649f70e Apr 26, 2013
mn200 added a commit that referenced this issue Apr 26, 2013
@mn200
Merge in fix for issue #115.
66da693
mn200 added a commit that referenced this issue Apr 26, 2013
@mn200
Remove debugging cruft from work on fixing issue #115.
70fbc9d
mn200 added a commit that referenced this issue Aug 12, 2013
@mn200
Mention fix of bug #115 in the release notes.
ae9afee
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Assignees
No one assigned
Labels
Bug Kernel Printing-Parsing
Projects
None yet
Milestone
No milestone
Development

No branches or pull requests
1 participant
@mn200