Changeset 1246 for src/LIN/LIN.ma

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:

• src/LIN/LIN.ma (modified) (2 diffs)

src/LIN/LIN.ma

@@ -1 +1 @@
 include "joint/Joint.ma".
+include "utilities/lists.ma".
 
-definition lin_params: params ≝
- mk_params (mk_params_ unit unit unit unit registers_move Register False unit unit unit) unit.
+definition lin_params_: params_ ≝
+ mk_params_ (mk_params__ unit unit unit unit registers_move Register False unit unit unit) unit.
 
-definition lin_statement ≝ joint_statement lin_params.
+definition pre_lin_statement ≝ joint_statement lin_params_.
 
 definition well_formed_P ≝
@@ -16 +17 @@
       | None ⇒ True]].
 
-(*
-definition lin_sem_params_: ∀globals. sem_params_ lin_params globals ≝
+definition lin_statement ≝ λglobals.(option label) × (pre_lin_statement globals).
+
+(*CSC: move elsewhere, also in joint/semantics.ma *)
+definition pi1: ∀A.∀P:A → Prop. (Σx:A. P x) → A ≝
+ λA,P,c. match c with [ dp w _ ⇒ w ].
+coercion pi1: ∀A.∀P:A → Prop.∀p:(Σx:A. P x).A ≝ pi1 on _p:Σx:?.? to ?.
+
+definition lin_params: ∀globals. params globals ≝
  λglobals.
-  mk_sem_params_ lin_params globals (Σcode:list (lin_statement globals). well_formed_P … code) ?.
-(*CSC: lookup function to be implemented *)
-cases daemon
-qed.
-*)
+  mk_params globals lin_params_ (Σcode:list (lin_statement globals). well_formed_P … code)
+   (λcode:Σcode.?. λl.
+    find ?? (λs. let 〈l',x〉 ≝ s in
+     match l' with [ None ⇒ None … | Some l'' ⇒ if eq_identifier … l l'' then Some … x else None ?]) code).
 
 definition lin_program ≝ joint_program lin_params.