source: src/joint/ProofUtils.ma @ 1470

Last change on this file since 1470 was 1470, checked in by mulligan, 8 years ago

finished, pretty ugly though as matita's disambiguation is a nightmare, so had to use tactics in some places

File size: 12.8 KB
Line 
1include "joint/Joint.ma".
2include "LIN/LIN.ma".
3
4let rec pre_erase_lin_internal_function'
5  (globals: list ident) (the_program: list (lin_statement globals))
6    (labels: list label)
7      on the_program: ((BitVectorTrie Word 16) × (list (lin_statement globals))) ≝
8  match the_program with
9  [ nil        ⇒
10    match labels with
11    [ nil ⇒ 〈Stub Word 16, [ ]〉 (* XXX: labels should be empty *)
12    | _   ⇒ ⊥
13    ]
14  | cons hd tl ⇒
15    let 〈lbl, instr〉 ≝ hd in
16      match lbl with
17      [ None ⇒
18        let 〈maps, instructions〉 ≝ pre_erase_lin_internal_function' globals tl labels in
19          match instr with
20          [ sequential seq l ⇒
21            match seq with
22            [ COST_LABEL cost ⇒ 〈maps, instructions〉
23            | _ ⇒ 〈maps, 〈None …, instr〉 :: instructions〉
24            ]
25          | _ ⇒ 〈maps, 〈None …, instr〉 :: instructions〉
26          ]
27      | Some lbl ⇒
28        let lbl' ≝ match lbl with [ an_identifier lbl ⇒ lbl ] in
29        match instr with
30        [ sequential seq l ⇒
31          match seq with
32          [ COST_LABEL cost ⇒ pre_erase_lin_internal_function' globals tl (lbl :: labels)
33          | _ ⇒
34            let 〈maps, instructions〉 ≝ pre_erase_lin_internal_function' globals tl labels in
35            let maps ≝ foldr ? ? (λl. λmap.
36              match l with
37              [ an_identifier l ⇒ insert … l lbl' map
38              ]) maps (lbl :: labels)
39            in
40              〈maps, instructions〉
41          ]
42        | _ ⇒
43          let 〈maps, instructions〉 ≝ pre_erase_lin_internal_function' globals tl labels in
44          let maps ≝ foldr ? ? (λl. λmap.
45            match l with
46            [ an_identifier l ⇒ insert … l lbl' map
47            ]) maps (lbl :: labels)
48          in
49            〈maps, instructions〉
50        ]
51      ]
52  ].
53  @daemon
54qed.
55
56definition relabel_joint_instruction:
57    ∀globals: list ident.
58    ∀params: params_.
59      BitVectorTrie Word 16 → joint_instruction params globals → joint_instruction params globals ≝
60  λglobals: list ident.
61  λparams.
62  λmap.
63  λinstr.
64  match instr with
65  [ COND acc_a lbl ⇒
66    let lbl ≝ match lbl with [ an_identifier lbl ⇒ lbl ] in
67    let located ≝ an_identifier LabelTag (lookup … lbl map lbl) in
68      COND params globals acc_a located
69  | _ ⇒ instr
70  ].
71
72definition relabel_joint_statement:
73  ∀globals: list ident.
74  ∀params: params_.
75    BitVectorTrie Word 16 → joint_statement params globals → joint_statement params globals ≝
76  λglobals: list ident.
77  λparams: params_.
78  λmap: BitVectorTrie Word 16.
79  λstmt: joint_statement params globals.
80  match stmt with
81  [ sequential seq l ⇒
82    let relabelled ≝ relabel_joint_instruction globals params map seq in
83      sequential params globals relabelled l
84  | RETURN ⇒ RETURN params globals
85  | GOTO l ⇒
86    let l ≝ match l with [ an_identifier l ⇒ l ] in
87    let located ≝ an_identifier LabelTag (lookup … l map l) in
88      GOTO params globals located
89  ].
90
91let rec relabel
92  (globals: list ident) (map: BitVectorTrie Word 16)
93    (program: list (lin_statement globals))
94      on program: list (lin_statement globals) ≝
95  match program with
96  [ nil        ⇒ [ ]
97  | cons hd tl ⇒
98    let 〈label, stmt〉 ≝ hd in
99    let relabelled ≝ relabel_joint_statement globals lin_params_ map stmt in
100    let label ≝
101      match label with
102      [ None ⇒ None …
103      | Some label ⇒
104        let label ≝ match label with [ an_identifier l ⇒ l ] in
105          Some … (an_identifier LabelTag (lookup … label map label))
106      ]
107    in
108      〈label, relabelled〉 :: relabel globals map tl
109  ].
110
111definition pre_erase_lin_internal_function:
112    ∀globals: list ident. joint_internal_function globals (lin_params globals) → joint_internal_function globals (lin_params globals) ≝
113  λglobals.
114  λfunction.
115    let luniverse ≝ joint_if_luniverse … function in
116    let runiverse ≝ joint_if_runiverse … function in
117    let result ≝ joint_if_result … function in
118    let params ≝ joint_if_params … function in
119    let locals ≝ joint_if_locals … function in
120    let stacksize ≝ joint_if_stacksize … function in
121    let code ≝ joint_if_code … function in
122    let entry ≝ ? in
123    let exit ≝ ? in
124    let 〈maps, code〉 ≝ pre_erase_lin_internal_function' globals code [ ] in
125    let code ≝ relabel globals maps code in
126      mk_joint_internal_function …
127        luniverse runiverse result params
128        locals stacksize code entry exit.
129  cases daemon (* XXX *)
130qed.
131
132definition erase_lin_program: lin_program → lin_program ≝
133  λprogram.
134    transform_program … program (transf_fundef … (pre_erase_lin_internal_function …)).
135
136include "joint/SemanticUtils.ma".
137
138definition empty_graph ≝
139  λa: Type[0].
140    an_id_map LabelTag a (Stub a 16).
141
142let rec pre_erase_graph_internal_function'
143  (params1: params1) (globals: list ident)
144    (the_graph: codeT globals (graph_params params1 globals)) (labels: list label)
145      (entry_point: label) (size_counter: nat) (map: BitVectorTrie Word 16)
146        (visited: BitVectorTrie bool 16)
147          on size_counter: ((BitVectorTrie Word 16) × (BitVectorTrie bool 16) × (codeT globals (graph_params params1 globals))) ≝
148  match size_counter return λ_.  ((BitVectorTrie Word 16) × (BitVectorTrie bool 16) × (codeT globals (graph_params params1 globals))) with
149  [ O ⇒
150    match labels with
151    [ nil ⇒ 〈map, visited, the_graph〉
152    | _   ⇒ ⊥
153    ]
154  | S size_counter ⇒
155    let entry_point' ≝ match entry_point with [ an_identifier e ⇒ e ] in
156    let statement ≝ lookup LabelTag ? the_graph entry_point in
157    match statement return λs: option (joint_statement (graph_params params1 globals) globals). ((BitVectorTrie Word 16) × (BitVectorTrie bool 16) × (codeT globals (graph_params params1 globals))) with
158    [ None ⇒ ⊥ (* XXX: should not happen *)
159    | Some statement ⇒
160      let entered_previously ≝ ? in
161      let visited ≝ insert … entry_point' true visited in
162      match entered_previously return λe: bool. ((BitVectorTrie Word 16) × (BitVectorTrie bool 16) × (codeT globals (graph_params params1 globals))) with
163      [ true ⇒ 〈map, visited, the_graph〉
164      | false ⇒ (* XXX: never visited here before *)
165        match statement return λs: joint_statement (graph_params params1 globals) globals. ((BitVectorTrie Word 16) × (BitVectorTrie bool 16) × (codeT globals (graph_params params1 globals))) with
166        [ sequential seq l ⇒
167          match seq with
168          [ COST_LABEL cost_label ⇒
169            pre_erase_graph_internal_function' params1 globals the_graph (entry_point :: labels) l size_counter map visited
170          | COND acc_a cond_label ⇒
171            let 〈map, visited, the_graph〉 ≝ pre_erase_graph_internal_function' params1 globals the_graph labels l size_counter map visited in
172              match size_counter with
173              [ O ⇒ ⊥ (* XXX: should never happen *)
174              | S size_counter ⇒
175                let 〈map, visited, the_graph〉 ≝ pre_erase_graph_internal_function' params1 globals the_graph labels cond_label size_counter map visited in
176                let map ≝ foldr … (λl. λmap. match l with [ an_identifier l ⇒ insert … l entry_point' map ]) map (entry_point :: labels) in
177                  〈map, visited, the_graph〉
178              ]
179          | _ ⇒
180            let 〈map, visited, the_graph〉 ≝ pre_erase_graph_internal_function' params1 globals the_graph labels l size_counter map visited in
181            let map ≝ foldr … (λl. λmap. match l with [ an_identifier l ⇒ insert … l entry_point' map ]) map (entry_point :: labels) in
182              〈map, visited, the_graph〉
183          ]
184        | RETURN ⇒
185          let map ≝ foldr … (λl. λmap. match l with [ an_identifier l ⇒ insert … l entry_point' map ]) map (entry_point :: labels) in
186            〈map, visited, the_graph〉
187        | GOTO l ⇒
188          let 〈map, visited, the_graph〉 ≝ pre_erase_graph_internal_function' params1 globals the_graph labels l size_counter map visited in
189          let map ≝ foldr … (λl. λmap. match l with [ an_identifier l ⇒ insert … l entry_point' map ]) map (entry_point :: labels) in
190            〈map, visited, the_graph〉
191        ]
192      ]
193    ]
194  ].
195  [4: @(lookup … entry_point' visited false)
196  |*: cases daemon
197  ]
198qed.
199
200definition pre_erase_graph_internal_function ≝
201  λparams1: params1.
202  λglobals: list ident.
203  λthe_graph: codeT globals (graph_params params1 globals).
204  λentry_point: label.
205    let 〈map, visited, the_graph〉 ≝ pre_erase_graph_internal_function' params1 globals the_graph [ ] entry_point (graph_num_nodes … the_graph) (Stub …) (Stub …) in
206      〈map, the_graph〉.
207
208let rec relabel_graph'
209  (params1: params1) (globals: list ident)
210    (the_graph: codeT globals (graph_params params1 globals)) (map: BitVectorTrie Word 16)
211      (visited: BitVectorTrie bool 16) (entry_point: label) (size_counter: nat)
212        on size_counter: codeT globals (graph_params params1 globals) ≝
213  match size_counter return λs: nat. codeT globals (graph_params params1 globals) with
214  [ O ⇒ empty_graph …
215  | S size_counter ⇒
216    let entry_point' ≝ match entry_point with [ an_identifier e ⇒ e ] in
217    let relabelled_entry_point ≝ an_identifier LabelTag ? in
218    let statement ≝ lookup LabelTag ? the_graph entry_point in
219    match statement return λs: option (joint_statement (graph_params params1 globals) globals). codeT globals (graph_params params1 globals) with
220    [ None ⇒ ⊥ (* XXX: should not happen *)
221    | Some statement ⇒
222      let entered_previously ≝ ? in
223      let visited ≝ insert … entry_point' true visited in
224      match entered_previously return λe: bool. codeT globals (graph_params params1 globals) with
225      [ true ⇒ the_graph
226      | false ⇒ (* XXX: never visited here before *)
227        match statement return λs: joint_statement (graph_params params1 globals) globals. codeT globals (graph_params params1 globals) with
228        [ sequential seq l ⇒
229          let l' ≝ match l with [ an_identifier l ⇒ l ] in
230          let 〈the_graph, new_seq〉 ≝
231            match seq return λs. (codeT globals (graph_params params1 globals)) × ? with
232            [ COND acc_a cond_label ⇒
233              let cond_label' ≝ match cond_label with [ an_identifier l ⇒ l ] in
234              let relabelled ≝ an_identifier LabelTag ? in
235              let tail_graph ≝ relabel_graph' params1 globals the_graph map visited cond_label size_counter in
236                〈tail_graph, COND … acc_a relabelled〉
237            | _ ⇒ 〈the_graph, seq〉
238            ]
239          in
240            match size_counter with
241            [ O ⇒ ⊥ (* XXX: impossible *)
242            | S size_counter ⇒
243              let tail_graph ≝ relabel_graph' params1 globals the_graph map visited l size_counter in
244              let relabelled ≝ an_identifier LabelTag ? in
245                add LabelTag … tail_graph relabelled_entry_point (sequential … new_seq relabelled)
246            ]
247        | RETURN ⇒ the_graph
248        | GOTO l ⇒
249          let l' ≝ match l with [ an_identifier l ⇒ l ] in
250          let relabelled ≝ an_identifier LabelTag ? in
251            add LabelTag … the_graph relabelled_entry_point (GOTO … relabelled)         
252        ]
253      ]
254    ]
255  ].
256  [3: @(lookup … l' map l')
257  |4: @(lookup … cond_label' map cond_label')
258  |5: @(lookup … l' map l')
259  |6: @(lookup … entry_point' visited false)
260  |7: @(lookup … entry_point' map entry_point')
261  |*: cases daemon
262  ]
263qed.
264
265definition relabel_graph ≝
266  λparams1: params1.
267  λglobals: list ident.
268  λthe_graph: codeT globals (graph_params params1 globals).
269  λentry_point: label.
270  λmap: BitVectorTrie Word 16.
271    relabel_graph' params1 globals the_graph map (Stub …) entry_point (graph_num_nodes … the_graph).
272
273definition pre_erase_graph_joint_internal_function ≝
274  λparams1: params1.
275  λglobals: list ident.
276  λint_fun: joint_internal_function globals (graph_params params1 globals).
277  let luniverse ≝ joint_if_luniverse globals (graph_params params1 globals) int_fun in
278  let runiverse ≝ joint_if_runiverse … int_fun in
279  let result ≝ joint_if_result … int_fun in
280  let params ≝ joint_if_params … int_fun in
281  let locals ≝ joint_if_locals … int_fun in
282  let stacksize ≝ joint_if_stacksize … int_fun in
283  let code ≝ joint_if_code … int_fun in
284  match joint_if_entry … int_fun with
285  [ dp entry entry_prf ⇒
286    match joint_if_exit … int_fun with
287    [ dp exit exit_prf ⇒
288      let 〈maps, code〉 ≝ pre_erase_graph_internal_function params1 globals code entry in
289      let code ≝ relabel_graph params1 globals code entry maps in
290        mk_joint_internal_function …
291          luniverse runiverse result params
292          locals stacksize code entry exit
293    ]
294  ].
295  cases daemon (* XXX *)
296qed.
Note: See TracBrowser for help on using the repository browser.