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 ? 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: ident → BitVectorTrieSet 16 → BitVectorTrieSet 16 ≝ |
---|
18 | λl: ident. |
---|
19 | λg: BitVectorTrieSet 16. |
---|
20 | set_insert ? (word_of_identifier ? l) g. |
---|
21 | |
---|
22 | definition mark: ident → BitVectorTrieSet 16 → BitVectorTrieSet 16 ≝ |
---|
23 | λl: ident. |
---|
24 | λg: BitVectorTrieSet 16. |
---|
25 | set_insert ? (word_of_identifier ? l) g. |
---|
26 | |
---|
27 | definition marked: ident → BitVectorTrieSet 16 → bool ≝ |
---|
28 | λl: ident. |
---|
29 | λg: BitVectorTrieSet 16. |
---|
30 | set_member ? (word_of_identifier ? l) g. |
---|
31 | |
---|
32 | (* alias id "lookupn" = "cic:/matita/cerco/common/Identifiers/lookup.def(3)". *) |
---|
33 | |
---|
34 | definition graph_lookup ≝ |
---|
35 | λglobals: list ident. |
---|
36 | λl: ident. |
---|
37 | λgr: ltl_statement_graph globals. |
---|
38 | lookup LabelTag ? gr (an_identifier LabelTag (word_of_identifier ? l)). |
---|
39 | |
---|
40 | definition fetch: ∀globals: list ident. ident → ltl_statement_graph globals → option (ltl_statement globals) ≝ |
---|
41 | λglobals: list ident. |
---|
42 | λl: ident. |
---|
43 | λg: ltl_statement_graph globals. |
---|
44 | graph_lookup globals l g. |
---|
45 | |
---|
46 | definition foo ≝ |
---|
47 | λl2, visited, required, globals, generated, g, n. |
---|
48 | λvisit: |
---|
49 | ∀globals: list Identifier. |
---|
50 | ∀g: LTLStatementGraph globals. |
---|
51 | ∀required: BitVectorTrieSet 16. |
---|
52 | ∀visited: BitVectorTrieSet 16. |
---|
53 | ∀generated: list (PreLINStatement globals). |
---|
54 | ∀l: Identifier. |
---|
55 | ∀n: nat. |
---|
56 | BitVectorTrieSet 16 × (list (PreLINStatement globals)). |
---|
57 | if marked l2 visited then |
---|
58 | 〈require l2 required, (Joint_St_Goto ? globals l2) :: generated〉 |
---|
59 | else |
---|
60 | visit globals g required visited generated l2 n. |
---|
61 | |
---|
62 | let rec visit (globals: list ident) (g: ltl_statement_graph globals) |
---|
63 | (required: BitVectorTrieSet 16) (visited: BitVectorTrieSet 16) |
---|
64 | (generated: list (pre_lin_statement globals)) (l: ident) (n: nat) on n: BitVectorTrieSet 16 × (list (PreLINStatement 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 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_goto lbl ⇒ |
---|
106 | let required' ≝ |
---|
107 | if marked lbl visited' then |
---|
108 | require lbl required |
---|
109 | else |
---|
110 | required in |
---|
111 | if marked lbl visited' then |
---|
112 | 〈required', (Joint_St_Goto ? globals lbl) :: generated''〉 |
---|
113 | else |
---|
114 | visit globals g required' visited' generated'' lbl n' |
---|
115 | | joint_st_Return ⇒ 〈required, generated''〉 (* dpm: correct? *) |
---|
116 | ] |
---|
117 | ] |
---|
118 | ]. |
---|
119 | |
---|
120 | (* |
---|
121 | definition translate_graph ≝ |
---|
122 | λglobals: list Identifier. |
---|
123 | λg: LTLStatementGraph globals. |
---|
124 | λentry: Identifier. |
---|
125 | let visited ≝ set_empty ? in |
---|
126 | let required ≝ set_insert ? entry (set_empty ?) in |
---|
127 | let 〈required', translated〉 ≝ visit globals g required visited [ ] entry in |
---|
128 | let reversed ≝ rev ? translated in |
---|
129 | filter (λs: PreLINStatement globals. ?) reversed. |
---|
130 | *) |
---|