Changeset 1311 for Deliverables/D3.3/idlookupbranch/LTL
 Timestamp:
 Oct 6, 2011, 6:45:54 PM (9 years ago)
 Location:
 Deliverables/D3.3/idlookupbranch
 Files:

 3 edited
Legend:
 Unmodified
 Added
 Removed

Deliverables/D3.3/idlookupbranch
 Property svn:mergeinfo changed
/src merged: 1198,12061233,12361260,12621264,1266,12681271,12741276,12781290,1292
 Property svn:mergeinfo changed

Deliverables/D3.3/idlookupbranch/LTL/LTL.ma
r1197 r1311 1 include "common/Graphs.ma".2 include "utilities/IdentifierTools.ma".3 1 include "joint/Joint.ma". 4 2 5 definition ltl_params: params ≝ 6 mk_params 7 unit unit unit unit registers_move Register 8 unit unit unit unit. 3 definition ltl_params__: params__ ≝ 4 (mk_params__ unit unit unit unit registers_move Register nat unit False). 5 definition ltl_params_ : params_ ≝ graph_params_ ltl_params__. 6 definition ltl_params0 : params0 ≝ mk_params0 ltl_params__ unit unit. 7 definition ltl_params1 : params1 ≝ mk_params1 ltl_params0 unit. 8 definition ltl_params: ∀globals. params globals ≝ graph_params ltl_params1. 9 9 10 definition ltl_statement ≝ λglobals: list ident. joint_statement ltl_params globals. 11 12 definition ltl_statement_graph ≝ λglobals. graph (ltl_statement globals). 13 14 record ltl_internal_function (globals: list ident): Type[0] ≝ 15 { 16 ltl_if_luniverse: universe LabelTag; 17 ltl_if_runiverse: universe RegisterTag; 18 ltl_if_stacksize: nat; 19 ltl_if_graph: ltl_statement_graph globals; 20 ltl_if_entry: Σl: label. lookup ? ? ltl_if_graph l ≠ None ?; 21 ltl_if_exit: Σl: label. lookup ? ? ltl_if_graph l ≠ None ? 22 }. 10 definition ltl_statement ≝ joint_statement ltl_params_. 23 11 24 inductive ltl_function_definition (globals: list ident): Type[0] ≝ 25  ltl_fu_internal_function: ltl_internal_function globals → ltl_function_definition globals 26  ltl_fu_external_function: external_function → ltl_function_definition globals. 27 28 record ltl_program (globals: list (ident × nat)): Type[0] ≝ 29 { 30 ltl_pr_funcs: list (ident × (ltl_function_definition (map ? ? \fst globals))); 31 ltl_pr_main: option ident 32 }. 12 definition ltl_program ≝ joint_program ltl_params. 13 14 definition ltl_internal_function ≝ 15 λglobals. joint_internal_function … (ltl_params globals). 
Deliverables/D3.3/idlookupbranch/LTL/LTLToLIN.ma
r1197 r1311 2 2 include "LIN/LIN.ma". 3 3 include "utilities/BitVectorTrieSet.ma". 4 include "common/Graphs.ma". 5 6 axiom LTLTag: String. 4 include alias "common/Graphs.ma". 7 5 8 6 definition translate_statement: ∀globals. ltl_statement globals → pre_lin_statement globals ≝ … … 10 8 λs: ltl_statement globals. 11 9 match s with 12 [ joint_st_return ⇒ joint_st_return lin_params globals 13  joint_st_sequential instr lbl ⇒ joint_st_sequential lin_params globals instr lbl 14  joint_st_goto l ⇒ joint_st_goto lin_params globals l 15  joint_st_extension ext ⇒ joint_st_extension lin_params globals ext 10 [ RETURN ⇒ RETURN ?? 11  sequential instr lbl ⇒ sequential … instr it 12  GOTO l ⇒ GOTO lin_params_ globals l 16 13 ]. 17 18 definition require: label → BitVectorTrieSet 16 → BitVectorTrieSet 16 ≝19 λl: label.20 λg: BitVectorTrieSet 16.21 set_insert ? (word_of_identifier ? l) g.22 23 definition mark: label → BitVectorTrieSet 16 → BitVectorTrieSet 16 ≝24 λl: label.25 λg: BitVectorTrieSet 16.26 set_insert ? (word_of_identifier ? l) g.27 28 definition marked: label → BitVectorTrieSet 16 → bool ≝29 λl: label.30 λg: BitVectorTrieSet 16.31 set_member ? (word_of_identifier ? l) g.32 33 (* alias id "lookupn" = "cic:/matita/cerco/common/Identifiers/lookup.def(3)". *)34 35 definition graph_lookup ≝36 λglobals: list ident.37 λl: label.38 λgr: ltl_statement_graph globals.39 lookup LabelTag ? gr (an_identifier LabelTag (word_of_identifier ? l)).40 41 definition fetch: ∀globals: list ident. label → ltl_statement_graph globals → option (ltl_statement globals) ≝42 λglobals: list ident.43 λl: label.44 λg: ltl_statement_graph globals.45 graph_lookup globals l g.46 14 47 definition foo ≝ 48 λl2, visited, required, globals, generated, g, n. 49 λvisit: 50 ∀globals: list ident. 51 ∀g: ltl_statement_graph globals. 52 ∀required: BitVectorTrieSet 16. 53 ∀visited: BitVectorTrieSet 16. 54 ∀generated: list (pre_lin_statement globals). 55 ∀l: label. 56 ∀n: nat. 57 BitVectorTrieSet 16 × (list (pre_lin_statement globals)). 58 if marked l2 visited then 59 〈require l2 required, (joint_st_goto … globals l2) :: generated〉 60 else 61 visit globals g required visited generated l2 n. 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. *) 20 let rec visit 21 (globals: list ident) (g: label → option (ltl_statement globals)) 22 (required: BitVectorTrieSet 16) (visited: BitVectorTrieSet 16) 23 (generated: list (lin_statement globals)) (l: label) (n: nat) 24 on n: BitVectorTrieSet 16 × (list (lin_statement globals)) ≝ 25 match n with 26 [ O ⇒ ⊥ (* CSC: Case to be made impossible; use dummy value? *) 27  S n' ⇒ 28 if set_member … (word_of_identifier … l) visited then 29 〈set_insert ? (word_of_identifier ? l) required, 〈None …, GOTO … globals l〉 :: generated〉 30 else 31 let visited' ≝ set_insert ? (word_of_identifier ? l) visited in 32 match 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' ≝ 〈Some … l, translated_statement〉 :: generated in 37 match statement with 38 [ sequential instr l2 ⇒ 39 match instr with 40 [ 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  RETURN ⇒ 〈required, generated'〉 50  GOTO l2 ⇒ visit globals g required visited' generated' l2 n']]]. 51 [1,2: @daemon (*CSC: impossible cases, use more dependent types *) ] 52 qed. 62 53 63 (* XXX: look at this. way too complicated to understand whether it is correct, 64 in my opinion. 65 *) 66 let rec visit 67 (globals: list ident) (g: ltl_statement_graph globals) 68 (required: BitVectorTrieSet 16) (visited: BitVectorTrieSet 16) 69 (generated: list (pre_lin_statement globals)) (l: label) (n: nat) 70 on n: BitVectorTrieSet 16 × (list (pre_lin_statement globals)) ≝ 71 match n with 72 [ O ⇒ 〈required, generated〉 73  S n' ⇒ 74 let visited' ≝ mark l visited in 75 match fetch globals l g with 76 [ None ⇒ 〈required, generated〉 (* dpm: correct? *) 77  Some statement ⇒ 78 let translated_statement ≝ translate_statement globals statement in 79 let generated'' ≝ translated_statement :: generated in 80 match statement with 81 [ joint_st_sequential instr l2 ⇒ 82 match instr with 83 [ joint_instr_cond acc_a_reg l1 ⇒ 84 let required' ≝ 85 if marked l2 visited' then 86 require l2 required 87 else 88 required in 89 let 〈required', generated''〉 ≝ 90 foo l2 visited' required' globals generated'' g n' visit (* 91 if marked l2 visited' then 92 〈required', (Joint_St_Goto ? globals l2) :: generated''〉 93 else 94 visit globals g required' visited' generated'' l2 n'*) in 95 let required'' ≝ require l1 required' in 96 if ¬(marked l1 visited') then 97 visit globals g required'' visited' generated'' l1 n' 98 else 99 〈required', generated''〉 100  _ ⇒ 101 let required' ≝ 102 if marked l2 visited' then 103 require l2 required 104 else 105 required in 106 if marked l2 visited' then 107 〈required', joint_st_goto … globals l2 :: generated''〉 108 else 109 visit globals g required' visited' generated'' l2 n' 110 ] 111  joint_st_return ⇒ 〈required, generated''〉 (* dpm: correct? *) 112  joint_st_goto l ⇒ 113 let required' ≝ 114 if marked l visited' then 115 require l required 116 else 117 required 118 in 119 if marked l visited' then 120 〈required', joint_st_goto … globals l :: generated''〉 121 else 122 visit globals g required' visited' generated'' l n' 123  joint_st_extension ext ⇒ 〈required, generated〉 124 ] 125 ] 126 ]. 54 (* CSC: The branch compression (aka tunneling) optimization is not implemented 55 in Matita *) 56 definition branch_compress ≝ λglobals.λa:label → option (ltl_statement globals).a. 127 57 128 (* 129 definition translate_graph ≝ 130 λglobals: list Identifier. 131 λg: LTLStatementGraph globals. 132 λentry: Identifier. 133 let visited ≝ set_empty ? in 134 let required ≝ set_insert ? entry (set_empty ?) in 135 let 〈required', translated〉 ≝ visit globals g required visited [ ] entry in 136 let reversed ≝ rev ? translated in 137 filter (λs: PreLINStatement globals. ?) reversed. 138 *) 58 definition translate_graph: 59 ∀globals. label → nat → 60 (label → option (ltl_statement globals)) → codeT … (lin_params globals) 61 ≝ 62 λglobals,entry,labels_upper_bound,g. 63 let g ≝ branch_compress ? g in 64 let visited ≝ set_empty ? in 65 let required ≝ set_insert ? (word_of_identifier … entry) (set_empty ?) in 66 let 〈required', translated〉 ≝ visit globals g required visited [ ] entry labels_upper_bound in 67 let reversed ≝ rev ? translated in 68 let final ≝ 69 map ?? 70 (λs. let 〈l,x〉 ≝ s in 71 match l with 72 [ None ⇒ 〈None …,x〉 73  Some l ⇒ 74 〈if set_member … (word_of_identifier … l) required' then Some ? l else None ?, 75 x〉]) 76 reversed 77 in 78 dp … final ?. 79 (*CSC: XXXXXXX missing proof of well formedness here; but it seems false! *) 80 cases daemon 81 qed. 82 83 definition translate_int_fun: 84 ∀globals. 85 joint_internal_function … (ltl_params globals) → 86 joint_internal_function … (lin_params globals) 87 ≝ 88 λglobals,f. 89 mk_joint_internal_function globals (lin_params globals) 90 (joint_if_luniverse ?? f) (joint_if_runiverse ?? f) it it it (joint_if_stacksize ?? f) 91 (translate_graph globals (joint_if_entry ?? f) (nat_of_bitvector … (next_identifier … (joint_if_luniverse … f))) 92 (lookup ?? (joint_if_code … f))) 93 ??. 94 cases daemon (*CSC: XXXXXXXXX Dead code produced *) 95 qed. 96 97 definition ltl_to_lin : ltl_program → lin_program ≝ 98 λp. transform_program … p (transf_fundef … (translate_int_fun …)).
Note: See TracChangeset
for help on using the changeset viewer.