Changeset 1197 for Deliverables/D3.3/id-lookup-branch/LTL

Timestamp:

Sep 7, 2011, 12:10:27 PM (9 years ago)

Author:

campbell

Message:

Merge trunk to branch.

Location:

Deliverables/D3.3/id-lookup-branch

Files:

• . (modified) (1 prop)
• LTL/LTL.ma (modified) (1 diff)
• LTL/LTLToLIN.ma (modified) (4 diffs)

Deliverables/D3.3/id-lookup-branch/LTL/LTL.ma

@@ -1 +1 @@
 include "common/Graphs.ma".
 include "utilities/IdentifierTools.ma".
-include "LIN/LIN.ma".
+include "joint/Joint.ma".
 
-definition ltl_statement ≝ joint_statement label.
+definition ltl_params: params ≝
+ mk_params
+   unit unit unit unit registers_move Register
+     unit unit unit unit.
+
+definition ltl_statement ≝ λglobals: list ident. joint_statement ltl_params globals.
   
 definition ltl_statement_graph ≝ λglobals. graph (ltl_statement globals).

Deliverables/D3.3/id-lookup-branch/LTL/LTLToLIN.ma

@@ -9 +9 @@
   λglobals: list ident.
   λs: ltl_statement globals.
-    match s with
-    [ joint_st_return ⇒ joint_st_return ? globals
-    | joint_st_sequential instr _ ⇒ joint_st_sequential ? globals instr it
-    | joint_st_goto l ⇒ joint_st_goto ? globals l
-    ].
+  match s with
+  [ joint_st_return ⇒ joint_st_return lin_params globals
+  | joint_st_sequential instr lbl ⇒ joint_st_sequential lin_params globals instr lbl
+  | joint_st_goto l ⇒ joint_st_goto lin_params globals l
+  | joint_st_extension ext ⇒ joint_st_extension lin_params globals ext
+  ].
     
 definition require: label → BitVectorTrieSet 16 → BitVectorTrieSet 16 ≝
@@ -56 +57 @@
     BitVectorTrieSet 16 × (list (pre_lin_statement globals)).
   if marked l2 visited then
-    〈require l2 required, (joint_st_goto ? globals l2) :: generated〉
+    〈require l2 required, (joint_st_goto … globals l2) :: generated〉
   else
    visit globals g required visited generated l2 n.
@@ -80 +81 @@
       [ joint_st_sequential instr l2 ⇒
         match instr with
-        [ joint_instr_cond_acc l1 ⇒
+        [ joint_instr_cond acc_a_reg l1 ⇒
               let required' ≝
                 if marked l2 visited' then
@@ -104 +105 @@
                 required in
             if marked l2 visited' then
-              〈required', joint_st_goto ? globals l2 :: generated''〉
+              〈required', joint_st_goto … globals l2 :: generated''〉
             else
               visit globals g required' visited' generated'' l2 n'
           ]
-        | joint_st_return ⇒ 〈required, generated''〉 (* dpm: correct? *)
+    | joint_st_return ⇒ 〈required, generated''〉 (* dpm: correct? *)
     | joint_st_goto l ⇒
-       let required' ≝
-         if marked l visited' then
-           require l required
-         else
-           required
-       in
-         if marked l visited' then
-           〈required', joint_st_goto ? globals l :: generated''〉
-         else
-           visit globals g required' visited' generated'' l n'
+      let required' ≝
+        if marked l visited' then
+         require l required
+        else
+         required
+      in
+        if marked l visited' then
+          〈required', joint_st_goto … globals l :: generated''〉
+        else
+          visit globals g required' visited' generated'' l n'
+    | joint_st_extension ext ⇒ 〈required, generated〉
     ]
   ]