Changeset 14 for C-semantics/README


Ignore:
Timestamp:
Jul 21, 2010, 3:08:58 PM (10 years ago)
Author:
campbell
Message:

Make Integers.ma respect bounds again, and reenable the rest of Mem.ma.

File:
1 edited

Legend:

Unmodified
Added
Removed
  • C-semantics/README

    r12 r14  
    4848No unfold tactic yet; use reduction or rewriting instead.
    4949
    50 ndestruct often takes too long; getting rid of irrelevant information (e.g.,
    51 replacing the goal with False) sometimes helps, or an extra lemma can be used.
     50Normalization of term containing large definitions (such as some of the
     51Integers library) can be prohibitive.  This is a particular problem because
     52ndestruct currently normalizes the goal and every hypothesis that is rewritten.
     53For ndestruct, getting rid of irrelevant information (e.g., replacing the goal
     54with False) sometimes helps, or an extra lemma can be used.
    5255
    5356Some of the pattern matching in the C syntax has had to be unfolded in
     
    6063The lack of sections has been replaced by duplicating the variables in some
    6164places, and adding a record in others.
     65
     66The meminj_no_overlap definition in Mem.ma uses the logical Or explicitly
     67rather than the ∨ notation to regain reasonable performance. (This is
     68presumably due to disambiguation - the notation is also used for booleans.)
     69
     70There are a couple of places in Mem.ma where rewriting had to be done carefully
     71to avoid assertions during unification; I'm not really sure what the problem
     72is.
    6273
    6374Detail per-file
     
    115126Mem.ma
    116127
    117   Everything except for omega in proofs.  Much of the transformations sections
    118   are commented out until Integers.ma is done properly.
     128  Everything except for omega in proofs.
    119129
    120130Smallstep.ma
Note: See TracChangeset for help on using the changeset viewer.