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

Consider making MEM e list an abbrevation for e ∈ set list #52

Closed
mn200 opened this issue Feb 1, 2012 · 1 comment
Closed

Consider making MEM e list an abbrevation for e ∈ set list #52

mn200 opened this issue Feb 1, 2012 · 1 comment
Labels
Feature Request Printing-Parsing

Comments

@mn200
Copy link
Member

mn200 commented Feb 1, 2012

The use of ∈ rather than just application (i.e., set list e) is necessary to get things like MEM e (list1 ++ list2) to expand nicely.

It seems clear that the abbreviation has to be this way round. The alternative the other way would be to have set list map to { x | MEM x list}, which is surely too complicated.

I will look into how much this change would break.
@mn200 mn200 mentioned this issue Oct 23, 2012
Closed
mn200 added a commit that referenced this issue Oct 30, 2012
@mn200
Start of work to replace MEM with λx l. x ∈ set l. See #52.
f42df6b
mn200 added a commit that referenced this issue Oct 30, 2012
@mn200
Get listTheory to build in features/mem-abbrev branch. See #52.
d1e604d
mn200 added a commit that referenced this issue Oct 30, 2012
@mn200
Build all of src/list/src and up to integer_word. See #52.
b033ece 
listSyntax loses mem_tm, but retains a mk_mem and a dest_mem that do
the obvious thing.
mn200 added a commit that referenced this issue Oct 30, 2012
@mn200
Fix bug in Cooper's algorithm; build-sequence at selftest=0 builds.
9d250cb 
Progress with #52.
mn200 added a commit that referenced this issue Oct 30, 2012
@mn200
Add IN_INSERT and NOT_IN_EMPTY to list_ss.
b415adb 
This allows simplification of MEM terms to work in all circumstances.  For example, if the term is

  MEM x (FRONT [y])

the simplification works like

     x IN set (FRONT [y])
     ^^^^^^^^^^^^^^^^^^^^

 --> x IN set (FRONT [y])
          ^^^^^^^^^^^^^^^

 --> x IN set (FRONT [y])
               ^^^^^^^^^

 --> x IN set []
              ^^

 --> x IN set []
          ^^^^^^

 --> x IN EMPTY

and the simplifier's theorem for MEM x [] (= x IN set []) never gets to fire.

This is progress with #52.
mn200 added a commit that referenced this issue Oct 30, 2012
@mn200
Get quotient examples (finite sets) to work in mem-abbrev world.
82f0ca3 
Progress with #52.
mn200 added a commit that referenced this issue Oct 30, 2012
@mn200
Add IN_UNION to list_ss; handles set(l1 ++ l2) being rewritten.
d40f8f6 
This is progress with #52.
mn200 added a commit that referenced this issue Oct 30, 2012
@mn200
Get decidable separation logic example to build.
b66984e 
Now that IN_LIST_TO_SET is gone, some scripts have to change. Another
alternative would be to bind that name to a trivial theorem that can't
hurt the progress of simplification (TRUTH would do).

This is progress with #52.
mn200 added a commit that referenced this issue Oct 30, 2012
@mn200
Get cheney_allocTheory to build in mem-abbrev world.
ad067e7 
Progress with #52.
mn200 added a commit that referenced this issue Oct 30, 2012
@mn200
Get all of machine-code/garbage-collectors to build.
8747783 
Progress with #52. General principle is to avoid use of IN_DEF, and to
instead prove rewrites of the form

  |- x ∈ myconstant arg1 .. argn ⇔ somerhs

rewriting set l x back to MEM x l as necessary.
@mn200 mn200 closed this as completed in 471787b Oct 30, 2012
@xrchz xrchz mentioned this issue Oct 30, 2012
Open
mn200 added a commit that referenced this issue Oct 31, 2012
@mn200
Merge branch 'features/mem-abbrev'.
a32838c 
This merges in fixes for the problems with EmitML.

This is fallout from #52.
mn200 added a commit that referenced this issue Nov 1, 2012
@mn200
Add a selftest for emit (catching a bug found by Ramana).
a84c1f3 
Fall-out from #52.
mn200 added a commit that referenced this issue Nov 1, 2012
@mn200
Fix bug whereby IN was stored incorrectly in ConstMap.
4060d52 
Continued fallout from #52.
mn200 added a commit that referenced this issue Nov 1, 2012
@mn200
Merge branch 'features/mem-abbrev', fixing another EmitML bug.
92b9b2d 
See 4060d52 for fix; other commits are new tests.

Perhaps this will finally put #52 to rest.
@xrchz
Copy link
Member

xrchz commented Nov 5, 2012

When definitions with LIST_TO_SET and other set-producing constants are passed through EmitML, the emitted SML fails to compile because of references to listML.LIST_TO_SET which has the wrong type ('a -> bool rather than 'a set). See comments on f0ab91f.

@xrchz xrchz reopened this Nov 5, 2012
@mn200 mn200 closed this as completed in caf91d0 Nov 5, 2012
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Assignees
No one assigned
Labels
Feature Request Printing-Parsing
Projects
None yet
Milestone
No milestone
Development

No branches or pull requests
2 participants
@mn200 @xrchz