source: src/LIN/LIN.ma @ 1246

Last change on this file since 1246 was 1246, checked in by sacerdot, 8 years ago

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 size: 1.2 KB
Line 
1include "joint/Joint.ma".
2include "utilities/lists.ma".
3
4definition lin_params_: params_ ≝
5 mk_params_ (mk_params__ unit unit unit unit registers_move Register False unit unit unit) unit.
6
7definition pre_lin_statement ≝ joint_statement lin_params_.
8
9definition well_formed_P ≝
10  λA, B: Type[0].
11  λcode: list (option A × B).
12    match code with
13    [ nil ⇒ False
14    | cons hd tl ⇒
15      match \fst hd with
16      [ Some lbl ⇒ False
17      | None ⇒ True]].
18
19definition lin_statement ≝ λglobals.(option label) × (pre_lin_statement globals).
20
21(*CSC: move elsewhere, also in joint/semantics.ma *)
22definition pi1: ∀A.∀P:A → Prop. (Σx:A. P x) → A ≝
23 λA,P,c. match c with [ dp w _ ⇒ w ].
24coercion pi1: ∀A.∀P:A → Prop.∀p:(Σx:A. P x).A ≝ pi1 on _p:Σx:?.? to ?.
25
26definition lin_params: ∀globals. params globals ≝
27 λglobals.
28  mk_params globals lin_params_ (Σcode:list (lin_statement globals). well_formed_P … code)
29   (λcode:Σcode.?. λl.
30    find ?? (λs. let 〈l',x〉 ≝ s in
31     match l' with [ None ⇒ None … | Some l'' ⇒ if eq_identifier … l l'' then Some … x else None ?]) code).
32
33definition lin_program ≝ joint_program lin_params.
Note: See TracBrowser for help on using the repository browser.