Ignore:
Timestamp:
Sep 22, 2011, 2:50:44 AM (9 years ago)
Author:
sacerdot
Message:

Yet another change to Joint.ma to accomodate all passes.
The concrete memory representation for the code of internal functions is
back, at the price of more complexity in the definition of the parameters.

Note: I do not understand any more the well_formed_P invariant for LIN code.
Moreover, the invariant does not seem to hold for code produced using LTLToLin.

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/joint/semantics.ma

    r1233 r1246  
    206206axiom BadFunction : String.
    207207
    208 (*CSC: move elsewhere *)
     208(*CSC: move elsewhere, also in LIN.ma *)
    209209definition pi1: ∀A.∀P:A → Prop. (Σx:A. P x) → A ≝
    210210 λA,P,c. match c with [ dp w _ ⇒ w ].
Note: See TracChangeset for help on using the changeset viewer.