 Timestamp:
 Sep 21, 2011, 11:57:20 AM (9 years ago)
 Location:
 src/LTL
 Files:

 2 edited
Legend:
 Unmodified
 Added
 Removed

src/LTL/LTL.ma
r1222 r1233 3 3 4 4 definition ltl_params: params ≝ 5 mk_params 6 unit unit unit unit registers_move Register 7 unit unit unit unit. 5 mk_params (mk_params_ unit unit unit unit registers_move Register False unit unit unit) label. 8 6 9 definition ltl_statement ≝ λglobals: list ident. joint_statement ltl_params globals.7 definition ltl_statement ≝ joint_statement ltl_params. 10 8 11 definition ltl_sem_params_: ∀globals. sem_params_ ltl_params globals ≝9 (*definition ltl_sem_params_: ∀globals. sem_params_ ltl_params globals ≝ 12 10 λglobals. 13 mk_sem_params_ ltl_params globals (graph (ltl_statement globals)) (lookup …). 11 mk_sem_params_ ltl_params globals (graph (ltl_statement globals)) (lookup …).*) 14 12 15 definition ltl_program ≝ λglobals. joint_program globals … (ltl_sem_params_ globals). 16 (* 17 18 record ltl_internal_function (globals: list ident): Type[0] ≝ 19 { 20 ltl_if_luniverse: universe LabelTag; 21 ltl_if_runiverse: universe RegisterTag; 22 ltl_if_stacksize: nat; 23 ltl_if_graph: ltl_statement_graph globals; 24 ltl_if_entry: Σl: label. lookup ? ? ltl_if_graph l ≠ None ?; 25 ltl_if_exit: Σl: label. lookup ? ? ltl_if_graph l ≠ None ? 26 }. 27 28 inductive ltl_function_definition (globals: list ident): Type[0] ≝ 29  ltl_fu_internal_function: ltl_internal_function globals → ltl_function_definition globals 30  ltl_fu_external_function: external_function → ltl_function_definition globals. 31 32 record ltl_program (globals: list (ident × nat)): Type[0] ≝ 33 { 34 ltl_pr_funcs: list (ident × (ltl_function_definition (map ? ? \fst globals))); 35 ltl_pr_main: option ident 36 }. 37 *) 13 definition ltl_program ≝ joint_program ltl_params. 
src/LTL/LTLToLIN.ma
r1224 r1233 3 3 include "utilities/BitVectorTrieSet.ma". 4 4 5 axiom LTLTag: String. 6 7 definition translate_statement: ∀globals. ltl_statement globals → pre_lin_statement globals ≝ 5 definition translate_statement: ∀globals. ltl_statement globals → lin_statement globals ≝ 8 6 λglobals: list ident. 9 7 λs: ltl_statement globals. 10 8 match s with 11 [ joint_st_return ⇒ joint_st_return lin_params globals12  joint_st_sequential instr lbl ⇒ joint_st_sequential lin_params globals instr lbl13  joint_st_goto l ⇒ joint_st_goto lin_params globalsl14  joint_st_extension ext ⇒ joint_st_extension lin_params globalsext9 [ joint_st_return ⇒ joint_st_return … 10  joint_st_sequential instr lbl ⇒ joint_st_sequential … instr it 11  joint_st_goto l ⇒ joint_st_goto … l 12  joint_st_extension ext ⇒ joint_st_extension lin_params … ext 15 13 ]. 16 17 definition require: label → BitVectorTrieSet 16 → BitVectorTrieSet 16 ≝18 λl: label.19 λg: BitVectorTrieSet 16.20 set_insert ? (word_of_identifier ? l) g.21 22 definition mark: label → BitVectorTrieSet 16 → BitVectorTrieSet 16 ≝23 λl: label.24 λg: BitVectorTrieSet 16.25 set_insert ? (word_of_identifier ? l) g.26 27 definition marked: label → BitVectorTrieSet 16 → bool ≝28 λl: label.29 λg: BitVectorTrieSet 16.30 set_member ? (word_of_identifier ? l) g.31 32 definition graph_lookup ≝33 λglobals: list ident.34 λl: label.35 λgr: graph (ltl_statement globals).36 lookup LabelTag ? gr (an_identifier LabelTag (word_of_identifier ? l)).37 38 definition fetch: ∀globals: list ident. label → graph (ltl_statement globals) → option (ltl_statement globals) ≝39 λglobals,l,g.graph_lookup globals l g.40 14 41 definition foo ≝ 42 λl2, visited, required, globals, generated, g, n. 43 λvisit: 44 ∀globals: list ident. 45 ∀g: graph (ltl_statement globals). 46 ∀required: BitVectorTrieSet 16. 47 ∀visited: BitVectorTrieSet 16. 48 ∀generated: list (pre_lin_statement globals). 49 ∀l: label. 50 ∀n: nat. 51 BitVectorTrieSet 16 × (list (pre_lin_statement globals)). 52 if marked l2 visited then 53 〈require l2 required, (joint_st_goto … globals l2) :: generated〉 54 else 55 visit globals g required visited generated l2 n. 56 57 (* XXX: look at this. way too complicated to understand whether it is correct, 58 in my opinion. 59 *) 15 (* Invariant: l has not been visited yet the very first time the 16 function is called and in the true branch of a conditional call. 17 This avoid useless gotos. 18 19 Note: the OCaml code contains some useful explanatory comments. *) 60 20 let rec visit 61 21 (globals: list ident) (g: graph (ltl_statement globals)) 62 22 (required: BitVectorTrieSet 16) (visited: BitVectorTrieSet 16) 63 (generated: list ( pre_lin_statement globals)) (l: label) (n: nat)64 on n: BitVectorTrieSet 16 × (list ( pre_lin_statement globals)) ≝23 (generated: list (lin_statement globals)) (l: label) (n: nat) 24 on n: BitVectorTrieSet 16 × (list (lin_statement globals)) ≝ 65 25 match n with 66 [ O ⇒ 〈required, generated〉26 [ O ⇒ ⊥ (* CSC: Case to be made impossible; use dummy value? *) 67 27  S n' ⇒ 68 let visited' ≝ mark l visited in 69 match fetch globals l g with 70 [ None ⇒ 〈required, generated〉 (* dpm: correct? *) 71  Some statement ⇒ 72 let translated_statement ≝ translate_statement globals statement in 73 let generated'' ≝ translated_statement :: generated in 74 match statement with 75 [ joint_st_sequential instr l2 ⇒ 76 match instr with 77 [ joint_instr_cond acc_a_reg l1 ⇒ 78 let required' ≝ 79 if marked l2 visited' then 80 require l2 required 81 else 82 required in 83 let 〈required', generated''〉 ≝ 84 foo l2 visited' required' globals generated'' g n' visit (* 85 if marked l2 visited' then 86 〈required', (Joint_St_Goto ? globals l2) :: generated''〉 87 else 88 visit globals g required' visited' generated'' l2 n'*) in 89 let required'' ≝ require l1 required' in 90 if ¬(marked l1 visited') then 91 visit globals g required'' visited' generated'' l1 n' 92 else 93 〈required', generated''〉 94  _ ⇒ 95 let required' ≝ 96 if marked l2 visited' then 97 require l2 required 98 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_return ⇒ 〈required, generated''〉 (* dpm: correct? *) 106  joint_st_goto l ⇒ 107 let required' ≝ 108 if marked l visited' then 109 require l required 110 else 111 required 112 in 113 if marked l visited' then 114 〈required', joint_st_goto … globals l :: generated''〉 115 else 116 visit globals g required' visited' generated'' l n' 117  joint_st_extension ext ⇒ 〈required, generated〉 118 ] 119 ] 120 ]. 28 if set_member … (word_of_identifier … l) visited then 29 〈set_insert ? (word_of_identifier ? l) required, joint_st_goto … globals l :: generated〉 30 else 31 let visited' ≝ set_insert ? (word_of_identifier ? l) visited in 32 match lookup LabelTag ? g (an_identifier LabelTag (word_of_identifier … l)) with 33 [ None ⇒ ⊥ (* Case to be made impossible with more dependent types *) 34  Some statement ⇒ 35 let translated_statement ≝ translate_statement globals statement in 36 let generated' ≝ translated_statement :: generated in 37 match statement with 38 [ joint_st_sequential instr l2 ⇒ 39 match instr with 40 [ joint_instr_cond acc_a_reg l1 ⇒ 41 let 〈required', generated''〉 ≝ 42 visit globals g required visited' generated' l2 n' in 43 let required'' ≝ set_insert ? (word_of_identifier ? l1) required' in 44 if set_member … (word_of_identifier … l1) visited' then 45 〈required', generated''〉 46 else 47 visit globals g required'' visited' generated'' l1 n' 48  _ ⇒ visit globals g required visited' generated' l2 n'] 49  joint_st_return ⇒ 〈required, generated'〉 50  joint_st_goto l2 ⇒ visit globals g required visited' generated' l2 n' 51  joint_st_extension ext ⇒ ⊥ ]]]. 52 [3: @ext 53 1,2: @daemon (*CSC: impossible cases, use more dependent types *) ] 54 qed. 121 55 122 (* 56 (* CSC: The branch compression (aka tunneling) optimization is not implemented 57 in Matita *) 58 definition branch_compress ≝ λglobals.λa:graph (ltl_statement globals).a. 59 123 60 definition translate_graph ≝ 124 61 λglobals: list Identifier. 125 λg: LTLStatementGraph globals. 126 λentry: Identifier. 62 λg: graph (ltl_statement globals). 63 λentry: label. 64 let g ≝ branch_compress ? g in 127 65 let visited ≝ set_empty ? in 128 let required ≝ set_insert ? entry(set_empty ?) in66 let required ≝ set_insert ? (word_of_identifier … entry) (set_empty ?) in 129 67 let 〈required', translated〉 ≝ visit globals g required visited [ ] entry in 130 68 let reversed ≝ rev ? translated in 131 69 filter (λs: PreLINStatement globals. ?) reversed. 132 *)
Note: See TracChangeset
for help on using the changeset viewer.