1 | include "LTL/LTL.ma". |
---|
2 | include "LIN/LIN.ma". |
---|
3 | include "utilities/BitVectorTrieSet.ma". |
---|
4 | include "common/Graphs.ma". |
---|
5 | |
---|
6 | axiom LTLTag: String. |
---|
7 | |
---|
8 | definition translate_statement: ∀globals. ltl_statement globals → pre_lin_statement globals ≝ |
---|
9 | λglobals: list ident. |
---|
10 | λs: ltl_statement globals. |
---|
11 | 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 |
---|
16 | ]. |
---|
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 | |
---|
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. |
---|
62 | |
---|
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 | ]. |
---|
127 | |
---|
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 | *) |
---|