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. LTLStatement globals → PreLINStatement globals ≝ |
---|
9 | λglobals: list Identifier. |
---|
10 | λs: LTLStatement globals. |
---|
11 | match s with |
---|
12 | [ Joint_St_Return ⇒ Joint_St_Return ? globals |
---|
13 | | Joint_St_Sequential instr _ ⇒ Joint_St_Sequential ? globals instr it |
---|
14 | | Joint_St_Goto lbl ⇒ Joint_St_Goto ? globals lbl |
---|
15 | ]. |
---|
16 | |
---|
17 | definition require: Identifier → BitVectorTrieSet 16 → BitVectorTrieSet 16 ≝ |
---|
18 | λl: Identifier. |
---|
19 | λg: BitVectorTrieSet 16. |
---|
20 | set_insert ? l g. |
---|
21 | |
---|
22 | definition mark: Identifier → BitVectorTrieSet 16 → BitVectorTrieSet 16 ≝ |
---|
23 | λl: Identifier. |
---|
24 | λg: BitVectorTrieSet 16. |
---|
25 | set_insert ? l g. |
---|
26 | |
---|
27 | definition marked: Identifier → BitVectorTrieSet 16 → bool ≝ |
---|
28 | λl: Identifier. |
---|
29 | λg: BitVectorTrieSet 16. |
---|
30 | set_member ? l g. |
---|
31 | |
---|
32 | definition graph_lookup ≝ |
---|
33 | λglobals. |
---|
34 | λl: Identifier. |
---|
35 | λg: LTLStatementGraph globals. |
---|
36 | lookup LabelTag (LTLStatement globals) g (an_identifier LabelTag l). |
---|
37 | |
---|
38 | definition fetch: ∀globals: list Identifier. Identifier → LTLStatementGraph globals → option (LTLStatement globals) ≝ |
---|
39 | λglobals: list Identifier. |
---|
40 | λl: Identifier. |
---|
41 | λg: LTLStatementGraph globals. |
---|
42 | graph_lookup globals l g. |
---|
43 | |
---|
44 | definition foo ≝ |
---|
45 | λl2, visited, required, globals, generated, g, n. |
---|
46 | λvisit: |
---|
47 | ∀globals: list Identifier. |
---|
48 | ∀g: LTLStatementGraph globals. |
---|
49 | ∀required: BitVectorTrieSet 16. |
---|
50 | ∀visited: BitVectorTrieSet 16. |
---|
51 | ∀generated: list (PreLINStatement globals). |
---|
52 | ∀l: Identifier. |
---|
53 | ∀n: nat. |
---|
54 | BitVectorTrieSet 16 × (list (PreLINStatement globals)). |
---|
55 | if marked l2 visited then |
---|
56 | 〈require l2 required, (Joint_St_Goto ? globals l2) :: generated〉 |
---|
57 | else |
---|
58 | visit globals g required visited generated l2 n. |
---|
59 | |
---|
60 | let rec visit (globals: list Identifier) (g: LTLStatementGraph globals) |
---|
61 | (required: BitVectorTrieSet 16) (visited: BitVectorTrieSet 16) |
---|
62 | (generated: list (PreLINStatement globals)) (l: Identifier) (n: nat) on n: BitVectorTrieSet 16 × (list (PreLINStatement globals)) ≝ |
---|
63 | match n with |
---|
64 | [ O ⇒ 〈required, generated〉 |
---|
65 | | S n' ⇒ |
---|
66 | let visited' ≝ mark l visited in |
---|
67 | match fetch globals l g with |
---|
68 | [ None ⇒ 〈required, generated〉 (* dpm: correct? *) |
---|
69 | | Some statement ⇒ |
---|
70 | let translated_statement ≝ translate_statement globals statement in |
---|
71 | let generated'' ≝ translated_statement :: generated in |
---|
72 | match statement with |
---|
73 | [ Joint_St_Sequential instr l2 ⇒ |
---|
74 | match instr with |
---|
75 | [ Joint_Instr_CondAcc l1 ⇒ |
---|
76 | let required' ≝ |
---|
77 | if marked l2 visited' then |
---|
78 | require l2 required |
---|
79 | else |
---|
80 | required in |
---|
81 | let 〈required', generated''〉 ≝ |
---|
82 | foo l2 visited' required' globals generated'' g n' visit (* |
---|
83 | if marked l2 visited' then |
---|
84 | 〈required', (Joint_St_Goto ? globals l2) :: generated''〉 |
---|
85 | else |
---|
86 | visit globals g required' visited' generated'' l2 n'*) in |
---|
87 | let required'' ≝ require l1 required' in |
---|
88 | if ¬(marked l1 visited') then |
---|
89 | visit globals g required'' visited' generated'' l1 n' |
---|
90 | else |
---|
91 | 〈required', generated''〉 |
---|
92 | | _ ⇒ |
---|
93 | let required' ≝ |
---|
94 | if marked l2 visited' then |
---|
95 | require l2 required |
---|
96 | else |
---|
97 | required in |
---|
98 | if marked l2 visited' then |
---|
99 | 〈required', Joint_St_Goto ? globals l2 :: generated''〉 |
---|
100 | else |
---|
101 | visit globals g required' visited' generated'' l2 n' |
---|
102 | ] |
---|
103 | | Joint_St_Goto lbl ⇒ |
---|
104 | let required' ≝ |
---|
105 | if marked lbl visited' then |
---|
106 | require lbl required |
---|
107 | else |
---|
108 | required in |
---|
109 | if marked lbl visited' then |
---|
110 | 〈required', (Joint_St_Goto ? globals lbl) :: generated''〉 |
---|
111 | else |
---|
112 | visit globals g required' visited' generated'' lbl n' |
---|
113 | | Joint_St_Return ⇒ 〈required, generated''〉 (* dpm: correct? *) |
---|
114 | ] |
---|
115 | ] |
---|
116 | ]. |
---|
117 | |
---|
118 | (* |
---|
119 | definition translate_graph ≝ |
---|
120 | λglobals: list Identifier. |
---|
121 | λg: LTLStatementGraph globals. |
---|
122 | λentry: Identifier. |
---|
123 | let visited ≝ set_empty ? in |
---|
124 | let required ≝ set_insert ? entry (set_empty ?) in |
---|
125 | let 〈required', translated〉 ≝ visit globals g required visited [ ] entry in |
---|
126 | let reversed ≝ rev ? translated in |
---|
127 | filter (λs: PreLINStatement globals. ?) reversed. |
---|
128 | *) |
---|