Changeset 1236
 Timestamp:
 Sep 21, 2011, 3:56:54 PM (9 years ago)
 Location:
 src
 Files:

 3 edited
Legend:
 Unmodified
 Added
 Removed

src/LIN/LIN.ma
r1233 r1236 25 25 *) 26 26 27 definition l tl_program ≝ joint_program lin_params.27 definition lin_program ≝ joint_program lin_params. 
src/LTL/LTLToLIN.ma
r1233 r1236 2 2 include "LIN/LIN.ma". 3 3 include "utilities/BitVectorTrieSet.ma". 4 include "utilities/lists.ma". 4 5 5 6 definition translate_statement: ∀globals. ltl_statement globals → lin_statement globals ≝ … … 19 20 Note: the OCaml code contains some useful explanatory comments. *) 20 21 let rec visit 21 (globals: list ident) (g: graph(ltl_statement globals))22 (globals: list ident) (g: label → option (ltl_statement globals)) 22 23 (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)) ≝24 (generated: list ((option label) × (lin_statement globals))) (l: label) (n: nat) 25 on n: BitVectorTrieSet 16 × (list ((option label) × (lin_statement globals))) ≝ 25 26 match n with 26 27 [ O ⇒ ⊥ (* CSC: Case to be made impossible; use dummy value? *) 27 28  S n' ⇒ 28 29 if set_member … (word_of_identifier … l) visited then 29 〈set_insert ? (word_of_identifier ? l) required, joint_st_goto … globals l:: generated〉30 〈set_insert ? (word_of_identifier ? l) required, 〈None …, joint_st_goto … globals l〉 :: generated〉 30 31 else 31 32 let visited' ≝ set_insert ? (word_of_identifier ? l) visited in 32 match lookup LabelTag ?g (an_identifier LabelTag (word_of_identifier … l)) with33 match g (an_identifier LabelTag (word_of_identifier … l)) with 33 34 [ None ⇒ ⊥ (* Case to be made impossible with more dependent types *) 34 35  Some statement ⇒ 35 36 let translated_statement ≝ translate_statement globals statement in 36 let generated' ≝ translated_statement:: generated in37 let generated' ≝ 〈Some … l, translated_statement〉 :: generated in 37 38 match statement with 38 39 [ joint_st_sequential instr l2 ⇒ … … 56 57 (* CSC: The branch compression (aka tunneling) optimization is not implemented 57 58 in Matita *) 58 definition branch_compress ≝ λglobals.λa: graph(ltl_statement globals).a.59 definition branch_compress ≝ λglobals.λa:label → option (ltl_statement globals).a. 59 60 60 definition translate_graph ≝ 61 λglobals: list Identifier. 62 λg: graph (ltl_statement globals). 63 λentry: label. 64 let g ≝ branch_compress ? g in 65 let visited ≝ set_empty ? in 66 let required ≝ set_insert ? (word_of_identifier … entry) (set_empty ?) in 67 let 〈required', translated〉 ≝ visit globals g required visited [ ] entry in 68 let reversed ≝ rev ? translated in 69 filter (λs: PreLINStatement globals. ?) reversed. 61 definition translate_graph: 62 ∀globals. label → nat → 63 (label → option (ltl_statement globals)) → (label → option (lin_statement globals)) 64 ≝ 65 λglobals,entry,labels_upper_bound,g. 66 let g ≝ branch_compress ? g in 67 let visited ≝ set_empty ? in 68 let required ≝ set_insert ? (word_of_identifier … entry) (set_empty ?) in 69 let 〈required', translated〉 ≝ visit globals g required visited [ ] entry labels_upper_bound in 70 let reversed ≝ rev ? translated in 71 let final ≝ 72 map ?? 73 (λs. let 〈l,x〉 ≝ s in 74 match l with 75 [ None ⇒ 〈None …,x〉 76  Some l ⇒ 77 〈if set_member … (word_of_identifier … l) required' then Some ? l else None ?, 78 x〉]) 79 reversed in 80 λl. 81 find ?? (λs. let 〈l',x〉 ≝ s in 82 match l' with [ None ⇒ None …  Some l'' ⇒ if eq_identifier … l l'' then Some … x else None ?]) final. 83 84 definition translate_int_fun: 85 ∀globals. 86 joint_internal_function ltl_params globals → 87 joint_internal_function lin_params globals 88 ≝ 89 λglobals,f. 90 mk_joint_internal_function lin_params globals 91 (joint_if_luniverse ?? f) (joint_if_runiverse ?? f) it it it (joint_if_stacksize ?? f) 92 (translate_graph globals (joint_if_entry ?? f) (nat_of_bitvector … (next_identifier … (joint_if_luniverse … f))) 93 (joint_if_lookup ?? f)) 94 ??. 95 cases daemon (*CSC: XXXXXXXXX Dead code produced *) 96 qed. 97 98 definition ltl_to_lin : ltl_program → lin_program ≝ 99 λp. transform_program … p (transf_fundef … (translate_int_fun …)). 
src/joint/Joint.ma
r1233 r1236 56 56 joint_if_params : paramsT p; 57 57 joint_if_locals : localsT p; 58 (*CSC: XXXXX stacksize unused for LTL...*) 58 59 joint_if_stacksize: nat; 59 60 joint_if_lookup : label → option (joint_statement p globals); 61 (*CSC: XXXXX entry unused for LIN, but invariant in that case... *) 60 62 joint_if_entry : Σl: label. joint_if_lookup l ≠ None ?; 63 (*CSC: XXXXX exit only used up to RTL (and only for tailcall removal) *) 61 64 joint_if_exit : Σl: label. joint_if_lookup l ≠ None ? 62 65 }.
Note: See TracChangeset
for help on using the changeset viewer.