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 | [ ltl_st_lift l ⇒ |
---|
13 | match l with |
---|
14 | [ joint_st_return ⇒ lin_st_lift globals (joint_st_return ? globals) |
---|
15 | | joint_st_sequential instr _ ⇒ lin_st_lift globals (joint_st_sequential ? globals instr it) |
---|
16 | ] |
---|
17 | | ltl_st_skip l ⇒ lin_st_goto globals l |
---|
18 | ]. |
---|
19 | |
---|
20 | definition require: label → BitVectorTrieSet 16 → BitVectorTrieSet 16 ≝ |
---|
21 | λl: label. |
---|
22 | λg: BitVectorTrieSet 16. |
---|
23 | set_insert ? (word_of_identifier ? l) g. |
---|
24 | |
---|
25 | definition mark: label → BitVectorTrieSet 16 → BitVectorTrieSet 16 ≝ |
---|
26 | λl: label. |
---|
27 | λg: BitVectorTrieSet 16. |
---|
28 | set_insert ? (word_of_identifier ? l) g. |
---|
29 | |
---|
30 | definition marked: label → BitVectorTrieSet 16 → bool ≝ |
---|
31 | λl: label. |
---|
32 | λg: BitVectorTrieSet 16. |
---|
33 | set_member ? (word_of_identifier ? l) g. |
---|
34 | |
---|
35 | (* alias id "lookupn" = "cic:/matita/cerco/common/Identifiers/lookup.def(3)". *) |
---|
36 | |
---|
37 | definition graph_lookup ≝ |
---|
38 | λglobals: list ident. |
---|
39 | λl: label. |
---|
40 | λgr: ltl_statement_graph globals. |
---|
41 | lookup LabelTag ? gr (an_identifier LabelTag (word_of_identifier ? l)). |
---|
42 | |
---|
43 | definition fetch: ∀globals: list ident. label → ltl_statement_graph globals → option (ltl_statement globals) ≝ |
---|
44 | λglobals: list ident. |
---|
45 | λl: label. |
---|
46 | λg: ltl_statement_graph globals. |
---|
47 | graph_lookup globals l g. |
---|
48 | |
---|
49 | definition foo ≝ |
---|
50 | λl2, visited, required, globals, generated, g, n. |
---|
51 | λvisit: |
---|
52 | ∀globals: list ident. |
---|
53 | ∀g: ltl_statement_graph globals. |
---|
54 | ∀required: BitVectorTrieSet 16. |
---|
55 | ∀visited: BitVectorTrieSet 16. |
---|
56 | ∀generated: list (pre_lin_statement globals). |
---|
57 | ∀l: label. |
---|
58 | ∀n: nat. |
---|
59 | BitVectorTrieSet 16 × (list (pre_lin_statement globals)). |
---|
60 | if marked l2 visited then |
---|
61 | 〈require l2 required, (lin_st_goto globals l2) :: generated〉 |
---|
62 | else |
---|
63 | visit globals g required visited generated l2 n. |
---|
64 | |
---|
65 | (* XXX: look at this. way too complicated to understand whether it is correct, |
---|
66 | in my opinion. |
---|
67 | *) |
---|
68 | let rec visit |
---|
69 | (globals: list ident) (g: ltl_statement_graph globals) |
---|
70 | (required: BitVectorTrieSet 16) (visited: BitVectorTrieSet 16) |
---|
71 | (generated: list (pre_lin_statement globals)) (l: label) (n: nat) |
---|
72 | on n: BitVectorTrieSet 16 × (list (pre_lin_statement globals)) ≝ |
---|
73 | match n with |
---|
74 | [ O ⇒ 〈required, generated〉 |
---|
75 | | S n' ⇒ |
---|
76 | let visited' ≝ mark l visited in |
---|
77 | match fetch globals l g with |
---|
78 | [ None ⇒ 〈required, generated〉 (* dpm: correct? *) |
---|
79 | | Some statement ⇒ |
---|
80 | let translated_statement ≝ translate_statement globals statement in |
---|
81 | let generated'' ≝ translated_statement :: generated in |
---|
82 | match statement with |
---|
83 | [ ltl_st_lift l ⇒ |
---|
84 | match l with |
---|
85 | [ joint_st_sequential instr l2 ⇒ |
---|
86 | match instr with |
---|
87 | [ joint_instr_cond_acc l1 ⇒ |
---|
88 | let required' ≝ |
---|
89 | if marked l2 visited' then |
---|
90 | require l2 required |
---|
91 | else |
---|
92 | required in |
---|
93 | let 〈required', generated''〉 ≝ |
---|
94 | foo l2 visited' required' globals generated'' g n' visit (* |
---|
95 | if marked l2 visited' then |
---|
96 | 〈required', (Joint_St_Goto ? globals l2) :: generated''〉 |
---|
97 | else |
---|
98 | visit globals g required' visited' generated'' l2 n'*) in |
---|
99 | let required'' ≝ require l1 required' in |
---|
100 | if ¬(marked l1 visited') then |
---|
101 | visit globals g required'' visited' generated'' l1 n' |
---|
102 | else |
---|
103 | 〈required', generated''〉 |
---|
104 | | _ ⇒ |
---|
105 | let required' ≝ |
---|
106 | if marked l2 visited' then |
---|
107 | require l2 required |
---|
108 | else |
---|
109 | required in |
---|
110 | if marked l2 visited' then |
---|
111 | 〈required', lin_st_goto globals l2 :: generated''〉 |
---|
112 | else |
---|
113 | visit globals g required' visited' generated'' l2 n' |
---|
114 | ] |
---|
115 | | joint_st_return ⇒ 〈required, generated''〉 (* dpm: correct? *) |
---|
116 | ] |
---|
117 | | ltl_st_skip l ⇒ |
---|
118 | let required' ≝ |
---|
119 | if marked l visited' then |
---|
120 | require l required |
---|
121 | else |
---|
122 | required |
---|
123 | in |
---|
124 | if marked l visited' then |
---|
125 | 〈required', lin_st_goto globals l :: generated''〉 |
---|
126 | else |
---|
127 | visit globals g required' visited' generated'' l n' |
---|
128 | ] |
---|
129 | ] |
---|
130 | ]. |
---|
131 | |
---|
132 | (* |
---|
133 | definition translate_graph ≝ |
---|
134 | λglobals: list Identifier. |
---|
135 | λg: LTLStatementGraph globals. |
---|
136 | λentry: Identifier. |
---|
137 | let visited ≝ set_empty ? in |
---|
138 | let required ≝ set_insert ? entry (set_empty ?) in |
---|
139 | let 〈required', translated〉 ≝ visit globals g required visited [ ] entry in |
---|
140 | let reversed ≝ rev ? translated in |
---|
141 | filter (λs: PreLINStatement globals. ?) reversed. |
---|
142 | *) |
---|