1 | include "LTL/LTL.ma". |
---|
2 | include "LIN/LIN.ma". |
---|
3 | include "utilities/BitVectorTrieSet.ma". |
---|
4 | |
---|
5 | axiom LTLTag: String. |
---|
6 | |
---|
7 | definition translate_statement: ∀globals. ltl_statement globals → pre_lin_statement globals ≝ |
---|
8 | λglobals: list ident. |
---|
9 | λs: ltl_statement globals. |
---|
10 | match s with |
---|
11 | [ joint_st_return ⇒ joint_st_return lin_params globals |
---|
12 | | joint_st_sequential instr lbl ⇒ joint_st_sequential lin_params globals instr lbl |
---|
13 | | joint_st_goto l ⇒ joint_st_goto lin_params globals l |
---|
14 | | joint_st_extension ext ⇒ joint_st_extension lin_params globals ext |
---|
15 | ]. |
---|
16 | |
---|
17 | definition require: label → BitVectorTrieSet 16 → BitVectorTrieSet 16 ≝ |
---|
18 | λl: label. |
---|
19 | λg: BitVectorTrieSet 16. |
---|
20 | set_insert ? (word_of_identifier ? l) g. |
---|
21 | |
---|
22 | definition mark: label → BitVectorTrieSet 16 → BitVectorTrieSet 16 ≝ |
---|
23 | λl: label. |
---|
24 | λg: BitVectorTrieSet 16. |
---|
25 | set_insert ? (word_of_identifier ? l) g. |
---|
26 | |
---|
27 | definition marked: label → BitVectorTrieSet 16 → bool ≝ |
---|
28 | λl: label. |
---|
29 | λg: BitVectorTrieSet 16. |
---|
30 | set_member ? (word_of_identifier ? l) g. |
---|
31 | |
---|
32 | definition graph_lookup ≝ |
---|
33 | λglobals: list ident. |
---|
34 | λl: label. |
---|
35 | λgr: graph (ltl_statement globals). |
---|
36 | lookup LabelTag ? gr (an_identifier LabelTag (word_of_identifier ? l)). |
---|
37 | |
---|
38 | definition fetch: ∀globals: list ident. label → graph (ltl_statement globals) → option (ltl_statement globals) ≝ |
---|
39 | λglobals,l,g.graph_lookup globals l g. |
---|
40 | |
---|
41 | definition foo ≝ |
---|
42 | λl2, visited, required, globals, generated, g, n. |
---|
43 | λvisit: |
---|
44 | ∀globals: list ident. |
---|
45 | ∀g: graph (ltl_statement globals). |
---|
46 | ∀required: BitVectorTrieSet 16. |
---|
47 | ∀visited: BitVectorTrieSet 16. |
---|
48 | ∀generated: list (pre_lin_statement globals). |
---|
49 | ∀l: label. |
---|
50 | ∀n: nat. |
---|
51 | BitVectorTrieSet 16 × (list (pre_lin_statement globals)). |
---|
52 | if marked l2 visited then |
---|
53 | 〈require l2 required, (joint_st_goto … globals l2) :: generated〉 |
---|
54 | else |
---|
55 | visit globals g required visited generated l2 n. |
---|
56 | |
---|
57 | (* XXX: look at this. way too complicated to understand whether it is correct, |
---|
58 | in my opinion. |
---|
59 | *) |
---|
60 | let rec visit |
---|
61 | (globals: list ident) (g: graph (ltl_statement globals)) |
---|
62 | (required: BitVectorTrieSet 16) (visited: BitVectorTrieSet 16) |
---|
63 | (generated: list (pre_lin_statement globals)) (l: label) (n: nat) |
---|
64 | on n: BitVectorTrieSet 16 × (list (pre_lin_statement globals)) ≝ |
---|
65 | match n with |
---|
66 | [ O ⇒ 〈required, generated〉 |
---|
67 | | S n' ⇒ |
---|
68 | let visited' ≝ mark l visited in |
---|
69 | match fetch globals l g with |
---|
70 | [ None ⇒ 〈required, generated〉 (* dpm: correct? *) |
---|
71 | | Some statement ⇒ |
---|
72 | let translated_statement ≝ translate_statement globals statement in |
---|
73 | let generated'' ≝ translated_statement :: generated in |
---|
74 | match statement with |
---|
75 | [ joint_st_sequential instr l2 ⇒ |
---|
76 | match instr with |
---|
77 | [ joint_instr_cond acc_a_reg l1 ⇒ |
---|
78 | let required' ≝ |
---|
79 | if marked l2 visited' then |
---|
80 | require l2 required |
---|
81 | else |
---|
82 | required in |
---|
83 | let 〈required', generated''〉 ≝ |
---|
84 | foo l2 visited' required' globals generated'' g n' visit (* |
---|
85 | if marked l2 visited' then |
---|
86 | 〈required', (Joint_St_Goto ? globals l2) :: generated''〉 |
---|
87 | else |
---|
88 | visit globals g required' visited' generated'' l2 n'*) in |
---|
89 | let required'' ≝ require l1 required' in |
---|
90 | if ¬(marked l1 visited') then |
---|
91 | visit globals g required'' visited' generated'' l1 n' |
---|
92 | else |
---|
93 | 〈required', generated''〉 |
---|
94 | | _ ⇒ |
---|
95 | let required' ≝ |
---|
96 | if marked l2 visited' then |
---|
97 | require l2 required |
---|
98 | else |
---|
99 | required in |
---|
100 | if marked l2 visited' then |
---|
101 | 〈required', joint_st_goto … globals l2 :: generated''〉 |
---|
102 | else |
---|
103 | visit globals g required' visited' generated'' l2 n' |
---|
104 | ] |
---|
105 | | joint_st_return ⇒ 〈required, generated''〉 (* dpm: correct? *) |
---|
106 | | joint_st_goto l ⇒ |
---|
107 | let required' ≝ |
---|
108 | if marked l visited' then |
---|
109 | require l required |
---|
110 | else |
---|
111 | required |
---|
112 | in |
---|
113 | if marked l visited' then |
---|
114 | 〈required', joint_st_goto … globals l :: generated''〉 |
---|
115 | else |
---|
116 | visit globals g required' visited' generated'' l n' |
---|
117 | | joint_st_extension ext ⇒ 〈required, generated〉 |
---|
118 | ] |
---|
119 | ] |
---|
120 | ]. |
---|
121 | |
---|
122 | (* |
---|
123 | definition translate_graph ≝ |
---|
124 | λglobals: list Identifier. |
---|
125 | λg: LTLStatementGraph globals. |
---|
126 | λentry: Identifier. |
---|
127 | let visited ≝ set_empty ? in |
---|
128 | let required ≝ set_insert ? entry (set_empty ?) in |
---|
129 | let 〈required', translated〉 ≝ visit globals g required visited [ ] entry in |
---|
130 | let reversed ≝ rev ? translated in |
---|
131 | filter (λs: PreLINStatement globals. ?) reversed. |
---|
132 | *) |
---|