Changeset 1168 for src/LIN

Timestamp:

Sep 2, 2011, 11:36:15 AM (10 years ago)

Author:

sacerdot

Message:

Joint statements parameterized over a record.

Location:

src/LIN

Files:

• LIN.ma (modified) (1 diff)
• LINToASM.ma (modified) (1 diff)

src/LIN/LIN.ma

@@ -1 @@
-include "Joint/JointLTLLIN.ma".
-  
-inductive pre_lin_statement (globals: list ident): Type[0] ≝
-  | lin_st_lift_joint: joint_statement unit Register Register Register Register Register registers_move globals → pre_lin_statement globals.
+include "joint/Joint.ma".
+
+definition lin_params: params ≝
+ mk_params unit unit unit unit registers_move Register.
+
+definition pre_lin_statement ≝
+ λglobals: list ident. joint_statement unit lin_params globals.
 
 definition lin_statement ≝

src/LIN/LINToASM.ma

@@ -35 +35 @@
       match instr' with
       [ joint_instr_cost_label lbl ⇒ set_insert ? (word_of_identifier ? lbl) (set_empty ?)
-      | joint_instr_cond_acc lbl ⇒ set_insert ? (word_of_identifier ? lbl) (set_empty ?)
+      | joint_instr_cond lbl ⇒ set_insert ? (word_of_identifier ? lbl) (set_empty ?)
       | _ ⇒ set_empty ?
       ]