Changeset 1166
- Timestamp:
- Sep 2, 2011, 10:35:24 AM (10 years ago)
- Location:
- src
- Files:
-
- 1 added
- 4 edited
- 1 moved
Legend:
- Unmodified
- Added
- Removed
-
src/ERTL/ERTLToLTL.ma
r1165 r1166 60 60 let off ≝ adjust_off globals int_fun off in 61 61 let luniv ≝ ertl_if_luniverse globals int_fun in 62 let 〈l, graph, luniv〉 ≝ generate globals luniv graph (joint_st_sequential globals (joint_instr_move … globals (from_acc r)) l) in62 let 〈l, graph, luniv〉 ≝ generate globals luniv graph (joint_st_sequential ??????? globals (joint_instr_move … globals (from_acc r)) l) in 63 63 ?. 64 64 -
src/LIN/LIN.ma
r1164 r1166 1 1 include "LIN/JointLTLLIN.ma". 2 2 3 definition pre_lin_statement ≝ 4 joint_statement unit Register Register 5 Register Register Register 6 registers_move. 3 inductive pre_lin_statement (globals: list ident): Type[0] ≝ 4 | lin_st_lift_joint: joint_statement unit Register Register Register Register Register registers_move globals → pre_lin_statement globals. 7 5 8 6 definition lin_statement ≝ -
src/LTL/LTL.ma
r1164 r1166 3 3 include "LIN/JointLTLLIN.ma". 4 4 5 definition ltl_statement ≝ 6 joint_statement label Register Register 7 Register Register Register 8 registers_move. 5 inductive ltl_statement (globals: list ident): Type[0] ≝ 6 ltl_st_lift_joint: joint_statement label Register Register Register Register Register registers_move globals → ltl_statement globals. 9 7 10 8 definition ltl_statement_graph ≝ λglobals. graph (ltl_statement globals). -
src/LTL/LTLToLIN.ma
r1164 r1166 9 9 λglobals: list ident. 10 10 λs: ltl_statement globals. 11 match s with 11 match s with 12 [ ltl_st_lift_joint joint ⇒ 13 match joint with 12 14 [ joint_st_return ⇒ joint_st_return … globals 13 15 | joint_st_sequential instr _ ⇒ joint_st_sequential … globals instr it 14 16 | joint_st_goto l ⇒ joint_st_goto … globals l 15 ]. 17 ] 18 ]. 16 19 17 20 definition require: label → BitVectorTrieSet 16 → BitVectorTrieSet 16 ≝ … … 78 81 let generated'' ≝ translated_statement :: generated in 79 82 match statement with 80 [ joint_st_sequential instr l2 ⇒ 81 match instr with 82 [ joint_instr_cond acc_a_reg l1 ⇒ 83 [ ltl_st_lift_joint joint ⇒ 84 match joint with 85 [ joint_st_sequential instr l2 ⇒ 86 match instr with 87 [ joint_instr_cond acc_a_reg l1 ⇒ 88 let required' ≝ 89 if marked l2 visited' then 90 require l2 required 91 else 92 required in 93 let 〈required', generated''〉 ≝ 94 foo l2 visited' required' globals generated'' g n' visit (* 95 if marked l2 visited' then 96 〈required', (Joint_St_Goto ? globals l2) :: generated''〉 97 else 98 visit globals g required' visited' generated'' l2 n'*) in 99 let required'' ≝ require l1 required' in 100 if ¬(marked l1 visited') then 101 visit globals g required'' visited' generated'' l1 n' 102 else 103 〈required', generated''〉 104 | _ ⇒ 83 105 let required' ≝ 84 106 if marked l2 visited' then … … 86 108 else 87 109 required in 88 let 〈required', generated''〉 ≝89 foo l2 visited' required' globals generated'' g n' visit (*90 if marked l2 visited' then91 〈required', (Joint_St_Goto ? globals l2) :: generated''〉92 else93 visit globals g required' visited' generated'' l2 n'*) in94 let required'' ≝ require l1 required' in95 if ¬(marked l1 visited') then96 visit globals g required'' visited' generated'' l1 n'97 else98 〈required', generated''〉99 | _ ⇒100 let required' ≝101 110 if marked l2 visited' then 102 require l2 required111 〈required', joint_st_goto … globals l2 :: generated''〉 103 112 else 104 required in 105 if marked l2 visited' then 106 〈required', joint_st_goto … globals l2 :: generated''〉 107 else 108 visit globals g required' visited' generated'' l2 n' 109 ] 110 | joint_st_return ⇒ 〈required, generated''〉 (* dpm: correct? *) 111 | joint_st_goto l ⇒ 112 let required' ≝ 113 if marked l visited' then 114 require l required 115 else 116 required 117 in 118 if marked l visited' then 119 〈required', joint_st_goto … globals l :: generated''〉 120 else 121 visit globals g required' visited' generated'' l n' 113 visit globals g required' visited' generated'' l2 n' 114 ] 115 | joint_st_return ⇒ 〈required, generated''〉 (* dpm: correct? *) 116 | joint_st_goto l ⇒ 117 let required' ≝ 118 if marked l visited' then 119 require l required 120 else 121 required 122 in 123 if marked l visited' then 124 〈required', joint_st_goto … globals l :: generated''〉 125 else 126 visit globals g required' visited' generated'' l n' 127 ] 122 128 ] 123 129 ]
Note: See TracChangeset
for help on using the changeset viewer.