Changeset 1110 for src/LTL/LTLToLIN.ma
- Timestamp:
- Aug 24, 2011, 6:45:01 PM (10 years ago)
- File:
-
- 1 edited
Legend:
- Unmodified
- Added
- Removed
-
src/LTL/LTLToLIN.ma
r759 r1110 10 10 λs: ltl_statement globals. 11 11 match s with 12 [ joint_st_return ⇒ joint_st_return ? globals 13 | joint_st_sequential instr _ ⇒ joint_st_sequential ? globals instr it 14 | joint_st_goto lbl ⇒ joint_st_goto ? globals lbl 12 [ ltl_st_lift l ⇒ 13 match l with 14 [ joint_st_return ⇒ lin_st_lift globals (joint_st_return ? globals) 15 | joint_st_sequential instr _ ⇒ lin_st_lift globals (joint_st_sequential ? globals instr it) 16 ] 17 | ltl_st_skip l ⇒ lin_st_goto globals l 15 18 ]. 16 19 17 definition require: ident→ BitVectorTrieSet 16 → BitVectorTrieSet 16 ≝18 λl: ident.20 definition require: label → BitVectorTrieSet 16 → BitVectorTrieSet 16 ≝ 21 λl: label. 19 22 λg: BitVectorTrieSet 16. 20 23 set_insert ? (word_of_identifier ? l) g. 21 24 22 definition mark: ident→ BitVectorTrieSet 16 → BitVectorTrieSet 16 ≝23 λl: ident.25 definition mark: label → BitVectorTrieSet 16 → BitVectorTrieSet 16 ≝ 26 λl: label. 24 27 λg: BitVectorTrieSet 16. 25 28 set_insert ? (word_of_identifier ? l) g. 26 29 27 definition marked: ident→ BitVectorTrieSet 16 → bool ≝28 λl: ident.30 definition marked: label → BitVectorTrieSet 16 → bool ≝ 31 λl: label. 29 32 λg: BitVectorTrieSet 16. 30 33 set_member ? (word_of_identifier ? l) g. … … 34 37 definition graph_lookup ≝ 35 38 λglobals: list ident. 36 λl: ident.39 λl: label. 37 40 λgr: ltl_statement_graph globals. 38 41 lookup LabelTag ? gr (an_identifier LabelTag (word_of_identifier ? l)). 39 42 40 definition fetch: ∀globals: list ident. ident→ ltl_statement_graph globals → option (ltl_statement globals) ≝43 definition fetch: ∀globals: list ident. label → ltl_statement_graph globals → option (ltl_statement globals) ≝ 41 44 λglobals: list ident. 42 λl: ident.45 λl: label. 43 46 λg: ltl_statement_graph globals. 44 47 graph_lookup globals l g. … … 47 50 λl2, visited, required, globals, generated, g, n. 48 51 λvisit: 49 ∀globals: list Identifier.50 ∀g: LTLStatementGraph globals.52 ∀globals: list ident. 53 ∀g: ltl_statement_graph globals. 51 54 ∀required: BitVectorTrieSet 16. 52 55 ∀visited: BitVectorTrieSet 16. 53 ∀generated: list ( PreLINStatement globals).54 ∀l: Identifier.56 ∀generated: list (pre_lin_statement globals). 57 ∀l: label. 55 58 ∀n: nat. 56 BitVectorTrieSet 16 × (list ( PreLINStatement globals)).59 BitVectorTrieSet 16 × (list (pre_lin_statement globals)). 57 60 if marked l2 visited then 58 〈require l2 required, ( Joint_St_Goto ?globals l2) :: generated〉61 〈require l2 required, (lin_st_goto globals l2) :: generated〉 59 62 else 60 63 visit globals g required visited generated l2 n. 61 64 62 let rec visit (globals: list ident) (g: ltl_statement_graph globals) 63 (required: BitVectorTrieSet 16) (visited: BitVectorTrieSet 16) 64 (generated: list (pre_lin_statement globals)) (l: ident) (n: nat) on n: BitVectorTrieSet 16 × (list (PreLINStatement globals)) ≝ 65 let rec visit 66 (globals: list ident) (g: ltl_statement_graph globals) 67 (required: BitVectorTrieSet 16) (visited: BitVectorTrieSet 16) 68 (generated: list (pre_lin_statement globals)) (l: label) (n: nat) 69 on n: BitVectorTrieSet 16 × (list (pre_lin_statement globals)) ≝ 65 70 match n with 66 71 [ O ⇒ 〈required, generated〉 … … 73 78 let generated'' ≝ translated_statement :: generated in 74 79 match statement with 75 [ joint_st_sequential instr l2 ⇒ 76 match instr with 77 [ joint_instr_cond_acc l1 ⇒ 80 [ ltl_st_lift l ⇒ 81 match l with 82 [ joint_st_sequential instr l2 ⇒ 83 match instr with 84 [ joint_instr_cond_acc l1 ⇒ 85 let required' ≝ 86 if marked l2 visited' then 87 require l2 required 88 else 89 required in 90 let 〈required', generated''〉 ≝ 91 foo l2 visited' required' globals generated'' g n' visit (* 92 if marked l2 visited' then 93 〈required', (Joint_St_Goto ? globals l2) :: generated''〉 94 else 95 visit globals g required' visited' generated'' l2 n'*) in 96 let required'' ≝ require l1 required' in 97 if ¬(marked l1 visited') then 98 visit globals g required'' visited' generated'' l1 n' 99 else 100 〈required', generated''〉 101 | _ ⇒ 78 102 let required' ≝ 79 103 if marked l2 visited' then … … 81 105 else 82 106 required in 83 let 〈required', generated''〉 ≝84 foo l2 visited' required' globals generated'' g n' visit (*85 if marked l2 visited' then86 〈required', (Joint_St_Goto ? globals l2) :: generated''〉87 else88 visit globals g required' visited' generated'' l2 n'*) in89 let required'' ≝ require l1 required' in90 if ¬(marked l1 visited') then91 visit globals g required'' visited' generated'' l1 n'92 else93 〈required', generated''〉94 | _ ⇒95 let required' ≝96 107 if marked l2 visited' then 97 require l2 required108 〈required', lin_st_goto globals l2 :: generated''〉 98 109 else 99 required in 100 if marked l2 visited' then 101 〈required', Joint_St_Goto ? globals l2 :: generated''〉 102 else 103 visit globals g required' visited' generated'' l2 n' 104 ] 105 | joint_st_goto lbl ⇒ 106 let required' ≝ 107 if marked lbl visited' then 108 require lbl required 109 else 110 required in 111 if marked lbl visited' then 112 〈required', (Joint_St_Goto ? globals lbl) :: generated''〉 113 else 114 visit globals g required' visited' generated'' lbl n' 115 | joint_st_Return ⇒ 〈required, generated''〉 (* dpm: correct? *) 110 visit globals g required' visited' generated'' l2 n' 111 ] 112 | joint_st_return ⇒ 〈required, generated''〉 (* dpm: correct? *) 116 113 ] 114 | ltl_st_skip l ⇒ 115 let required' ≝ 116 if marked l visited' then 117 require l required 118 else 119 required 120 in 121 if marked l visited' then 122 〈required', lin_st_goto globals l :: generated''〉 123 else 124 visit globals g required' visited' generated'' l n' 117 125 ] 118 ]. 126 ] 127 ]. 119 128 120 129 (*
Note: See TracChangeset
for help on using the changeset viewer.