source: src/LTL/LTLToLIN.ma @ 1282

Last change on this file since 1282 was 1282, checked in by sacerdot, 9 years ago

Cosmetic change: names of joint statements/instructions shortened and made
uppercase.

File size: 4.0 KB
RevLine 
[714]1include "LTL/LTL.ma".
2include "LIN/LIN.ma".
[728]3include "utilities/BitVectorTrieSet.ma".
[1246]4include alias "common/Graphs.ma".
[714]5
[1246]6definition translate_statement: ∀globals. ltl_statement globals → pre_lin_statement globals ≝
[757]7  λglobals: list ident.
8  λs: ltl_statement globals.
[1166]9  match s with
[1282]10  [ RETURN ⇒ RETURN ??
11  | sequential instr lbl ⇒ sequential … instr it
12  | GOTO l ⇒ GOTO lin_params_ globals l
[1166]13  ].
[728]14
[1233]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. *)
[1110]20let rec visit
[1236]21  (globals: list ident) (g: label → option (ltl_statement globals))
[1110]22  (required: BitVectorTrieSet 16) (visited: BitVectorTrieSet 16)
[1246]23  (generated: list (lin_statement globals)) (l: label) (n: nat)
24    on n: BitVectorTrieSet 16 × (list (lin_statement globals)) ≝
[728]25  match n with
[1233]26  [ O ⇒ ⊥ (* CSC: Case to be made impossible; use dummy value? *)
[728]27  | S n' ⇒
[1233]28    if set_member … (word_of_identifier … l) visited then
[1282]29     〈set_insert ? (word_of_identifier ? l) required, 〈None …, GOTO … globals l〉 :: generated〉
[1233]30    else
31     let visited' ≝ set_insert ? (word_of_identifier ? l) visited in
[1236]32     match g (an_identifier LabelTag (word_of_identifier … l)) with
[1233]33     [ None ⇒ ⊥ (* Case to be made impossible with more dependent types *)
34     | Some statement ⇒
35       let translated_statement ≝ translate_statement globals statement in
[1236]36       let generated' ≝ 〈Some … l, translated_statement〉 :: generated in
[1233]37       match statement with
[1282]38       [ sequential instr l2 ⇒
[1233]39         match instr with
[1282]40         [ COND acc_a_reg l1 ⇒
[1233]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']
[1282]49     | RETURN ⇒ 〈required, generated'〉
50     | GOTO l2 ⇒ visit globals g required visited' generated' l2 n']]].
[1250]51[1,2: @daemon (*CSC: impossible cases, use more dependent types *) ]
[1233]52qed.
[728]53
[1233]54(* CSC: The branch compression (aka tunneling) optimization is not implemented
55   in Matita *)
[1236]56definition branch_compress ≝ λglobals.λa:label → option (ltl_statement globals).a.
[1233]57
[1236]58definition translate_graph:
59 ∀globals. label → nat →
[1246]60  (label → option (ltl_statement globals)) → codeT … (lin_params globals)
[1236]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〉])
[1246]76    reversed
77  in
78   dp … final ?.
79(*CSC: XXXXXXX missing proof of well formedness here; but it seems false! *)
80cases daemon
81qed.
[1236]82
83definition translate_int_fun:
84 ∀globals.
[1246]85  joint_internal_function … (ltl_params globals) →
86   joint_internal_function … (lin_params globals)
[1236]87
88 λglobals,f.
[1246]89  mk_joint_internal_function globals (lin_params globals)
[1236]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)))
[1246]92     (lookup ?? (joint_if_code … f)))
[1236]93    ??.
94cases daemon (*CSC: XXXXXXXXX Dead code produced *)
95qed.
96
97definition ltl_to_lin : ltl_program → lin_program ≝
[1282]98 λp. transform_program … p (transf_fundef … (translate_int_fun …)).
Note: See TracBrowser for help on using the repository browser.