1 | include "LTL/LTL.ma". |
---|
2 | include "LIN/LIN.ma". |
---|
3 | include "utilities/BitVectorTrieSet.ma". |
---|
4 | include "utilities/lists.ma". |
---|
5 | |
---|
6 | definition translate_statement: ∀globals. ltl_statement globals → lin_statement globals ≝ |
---|
7 | λglobals: list ident. |
---|
8 | λs: ltl_statement globals. |
---|
9 | match s with |
---|
10 | [ joint_st_return ⇒ joint_st_return … |
---|
11 | | joint_st_sequential instr lbl ⇒ joint_st_sequential … instr it |
---|
12 | | joint_st_goto l ⇒ joint_st_goto … l |
---|
13 | | joint_st_extension ext ⇒ joint_st_extension lin_params … ext |
---|
14 | ]. |
---|
15 | |
---|
16 | (* Invariant: l has not been visited yet the very first time the |
---|
17 | function is called and in the true branch of a conditional call. |
---|
18 | This avoid useless gotos. |
---|
19 | |
---|
20 | Note: the OCaml code contains some useful explanatory comments. *) |
---|
21 | let rec visit |
---|
22 | (globals: list ident) (g: label → option (ltl_statement globals)) |
---|
23 | (required: BitVectorTrieSet 16) (visited: BitVectorTrieSet 16) |
---|
24 | (generated: list ((option label) × (lin_statement globals))) (l: label) (n: nat) |
---|
25 | on n: BitVectorTrieSet 16 × (list ((option label) × (lin_statement globals))) ≝ |
---|
26 | match n with |
---|
27 | [ O ⇒ ⊥ (* CSC: Case to be made impossible; use dummy value? *) |
---|
28 | | S n' ⇒ |
---|
29 | if set_member … (word_of_identifier … l) visited then |
---|
30 | 〈set_insert ? (word_of_identifier ? l) required, 〈None …, joint_st_goto … globals l〉 :: generated〉 |
---|
31 | else |
---|
32 | let visited' ≝ set_insert ? (word_of_identifier ? l) visited in |
---|
33 | match g (an_identifier LabelTag (word_of_identifier … l)) with |
---|
34 | [ None ⇒ ⊥ (* Case to be made impossible with more dependent types *) |
---|
35 | | Some statement ⇒ |
---|
36 | let translated_statement ≝ translate_statement globals statement in |
---|
37 | let generated' ≝ 〈Some … l, translated_statement〉 :: generated in |
---|
38 | match statement with |
---|
39 | [ joint_st_sequential instr l2 ⇒ |
---|
40 | match instr with |
---|
41 | [ joint_instr_cond acc_a_reg l1 ⇒ |
---|
42 | let 〈required', generated''〉 ≝ |
---|
43 | visit globals g required visited' generated' l2 n' in |
---|
44 | let required'' ≝ set_insert ? (word_of_identifier ? l1) required' in |
---|
45 | if set_member … (word_of_identifier … l1) visited' then |
---|
46 | 〈required', generated''〉 |
---|
47 | else |
---|
48 | visit globals g required'' visited' generated'' l1 n' |
---|
49 | | _ ⇒ visit globals g required visited' generated' l2 n'] |
---|
50 | | joint_st_return ⇒ 〈required, generated'〉 |
---|
51 | | joint_st_goto l2 ⇒ visit globals g required visited' generated' l2 n' |
---|
52 | | joint_st_extension ext ⇒ ⊥ ]]]. |
---|
53 | [3: @ext |
---|
54 | |1,2: @daemon (*CSC: impossible cases, use more dependent types *) ] |
---|
55 | qed. |
---|
56 | |
---|
57 | (* CSC: The branch compression (aka tunneling) optimization is not implemented |
---|
58 | in Matita *) |
---|
59 | definition branch_compress ≝ λglobals.λa:label → option (ltl_statement globals).a. |
---|
60 | |
---|
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 …)). |
---|