source: src/joint/Erasure.ma @ 1472

Last change on this file since 1472 was 1472, checked in by mulligan, 9 years ago

moved proof utils to erasure.ma

File size: 12.6 KB
Line 
1include "LIN/LIN.ma".
2include "joint/SemanticUtils.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 pre_erase_lin_internal_function ≝
57  λglobals: list ident.
58  λint_fun: joint_internal_function … (lin_params globals).
59    pre_erase_lin_internal_function' … (joint_if_code … (lin_params …) int_fun) [ ].
60
61definition relabel_joint_instruction:
62    ∀globals: list ident.
63    ∀params: params_.
64      BitVectorTrie Word 16 → joint_instruction params globals → joint_instruction params globals ≝
65  λglobals: list ident.
66  λparams.
67  λmap.
68  λinstr.
69  match instr with
70  [ COND acc_a lbl ⇒
71    let lbl ≝ match lbl with [ an_identifier lbl ⇒ lbl ] in
72    let located ≝ an_identifier LabelTag (lookup … lbl map lbl) in
73      COND params globals acc_a located
74  | _ ⇒ instr
75  ].
76
77definition relabel_joint_statement:
78  ∀globals: list ident.
79  ∀params: params_.
80    BitVectorTrie Word 16 → joint_statement params globals → joint_statement params globals ≝
81  λglobals: list ident.
82  λparams: params_.
83  λmap: BitVectorTrie Word 16.
84  λstmt: joint_statement params globals.
85  match stmt with
86  [ sequential seq l ⇒
87    let relabelled ≝ relabel_joint_instruction globals params map seq in
88      sequential params globals relabelled l
89  | RETURN ⇒ RETURN params globals
90  | GOTO l ⇒
91    let l ≝ match l with [ an_identifier l ⇒ l ] in
92    let located ≝ an_identifier LabelTag (lookup … l map l) in
93      GOTO params globals located
94  ].
95
96let rec relabel_lin_internal_function'
97  (globals: list ident) (map: BitVectorTrie Word 16)
98    (program: list (lin_statement globals))
99      on program: list (lin_statement globals) ≝
100  match program with
101  [ nil        ⇒ [ ]
102  | cons hd tl ⇒
103    let 〈label, stmt〉 ≝ hd in
104    let relabelled ≝ relabel_joint_statement globals lin_params_ map stmt in
105    let label ≝
106      match label with
107      [ None ⇒ None …
108      | Some label ⇒
109        let label ≝ match label with [ an_identifier l ⇒ l ] in
110          Some … (an_identifier LabelTag (lookup … label map label))
111      ]
112    in
113      〈label, relabelled〉 :: relabel_lin_internal_function' globals map tl
114  ].
115
116definition relabel_lin_internal_function ≝
117  λglobals.
118  λmap.
119  λint_fun: joint_internal_function globals (lin_params globals).
120    relabel_lin_internal_function' globals map (joint_if_code … int_fun).
121
122definition empty_graph ≝
123  λa: Type[0].
124    an_id_map LabelTag a (Stub a 16).
125
126let rec pre_erase_graph_internal_function'
127  (params1: params1) (globals: list ident)
128    (the_graph: codeT globals (graph_params params1 globals)) (labels: list label)
129      (entry_point: label) (size_counter: nat) (map: BitVectorTrie Word 16)
130        (visited: BitVectorTrie bool 16)
131          on size_counter: ((BitVectorTrie Word 16) × (BitVectorTrie bool 16) × (codeT globals (graph_params params1 globals))) ≝
132  match size_counter return λ_.  ((BitVectorTrie Word 16) × (BitVectorTrie bool 16) × (codeT globals (graph_params params1 globals))) with
133  [ O ⇒
134    match labels with
135    [ nil ⇒ 〈map, visited, the_graph〉
136    | _   ⇒ ⊥
137    ]
138  | S size_counter ⇒
139    let entry_point' ≝ match entry_point with [ an_identifier e ⇒ e ] in
140    let statement ≝ lookup LabelTag ? the_graph entry_point in
141    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
142    [ None ⇒ ⊥ (* XXX: should not happen *)
143    | Some statement ⇒
144      let entered_previously ≝ bvt_lookup … entry_point' visited false in
145      match entered_previously return λe: bool. ((BitVectorTrie Word 16) × (BitVectorTrie bool 16) × (codeT globals (graph_params params1 globals))) with
146      [ true ⇒ 〈map, visited, the_graph〉
147      | false ⇒ (* XXX: never visited here before *)
148        let visited ≝ insert … entry_point' true visited in
149        match statement return λs: joint_statement (graph_params params1 globals) globals. ((BitVectorTrie Word 16) × (BitVectorTrie bool 16) × (codeT globals (graph_params params1 globals))) with
150        [ sequential seq l ⇒
151          match seq with
152          [ COST_LABEL cost_label ⇒
153            pre_erase_graph_internal_function' params1 globals the_graph (entry_point :: labels) l size_counter map visited
154          | COND acc_a cond_label ⇒
155            let 〈map, visited, the_graph〉 ≝ pre_erase_graph_internal_function' params1 globals the_graph [ ] l size_counter map visited in
156            let 〈map, visited, the_graph〉 ≝ pre_erase_graph_internal_function' params1 globals the_graph [ ] cond_label size_counter map visited in
157            let map ≝ foldr … (λl. λmap. match l with [ an_identifier l ⇒ insert … l entry_point' map ]) map (entry_point :: labels) in
158              〈map, visited, the_graph〉
159          | _ ⇒
160            let 〈map, visited, the_graph〉 ≝ pre_erase_graph_internal_function' params1 globals the_graph [ ] l size_counter map visited in
161            let map ≝ foldr … (λl. λmap. match l with [ an_identifier l ⇒ insert … l entry_point' map ]) map (entry_point :: labels) in
162              〈map, visited, the_graph〉
163          ]
164        | RETURN ⇒
165          let map ≝ foldr … (λl. λmap. match l with [ an_identifier l ⇒ insert … l entry_point' map ]) map (entry_point :: labels) in
166            〈map, visited, the_graph〉
167        | GOTO l ⇒
168          let 〈map, visited, the_graph〉 ≝ pre_erase_graph_internal_function' params1 globals the_graph [ ] l size_counter map visited in
169          let map ≝ foldr … (λl. λmap. match l with [ an_identifier l ⇒ insert … l entry_point' map ]) map (entry_point :: labels) in
170            〈map, visited, the_graph〉
171        ]
172      ]
173    ]
174  ].
175  cases daemon
176qed.
177
178definition pre_erase_graph_internal_function ≝
179  λparams1: params1.
180  λglobals: list ident.
181  λint_fun: joint_internal_function globals (graph_params params1 globals).
182  match joint_if_entry … int_fun with
183  [ dp entry entry_proof ⇒
184    let code ≝ joint_if_code … int_fun in
185    let 〈map, visited, the_graph〉 ≝ pre_erase_graph_internal_function' params1 globals code [ ] entry (graph_num_nodes … code) (Stub …) (Stub …) in
186      〈map, the_graph〉
187  ].
188
189let rec relabel_graph'
190  (params1: params1) (globals: list ident)
191    (the_graph: codeT globals (graph_params params1 globals)) (map: BitVectorTrie Word 16)
192      (visited: BitVectorTrie bool 16) (entry_point: label) (size_counter: nat)
193        on size_counter: codeT globals (graph_params params1 globals) ≝
194  match size_counter return λs: nat. codeT globals (graph_params params1 globals) with
195  [ O ⇒ empty_graph …
196  | S size_counter ⇒
197    let entry_point' ≝ match entry_point with [ an_identifier e ⇒ e ] in
198    let relabelled_entry_point ≝ an_identifier LabelTag (bvt_lookup … entry_point' map entry_point') in
199    let statement ≝ lookup LabelTag ? the_graph entry_point in
200    match statement return λs: option (joint_statement (graph_params params1 globals) globals). codeT globals (graph_params params1 globals) with
201    [ None ⇒ ⊥ (* XXX: should not happen *)
202    | Some statement ⇒
203      let entered_previously ≝ (bvt_lookup … entry_point' visited false) in
204      match entered_previously return λe: bool. codeT globals (graph_params params1 globals) with
205      [ true ⇒ the_graph
206      | false ⇒ (* XXX: never visited here before *)
207        let visited ≝ insert … entry_point' true visited in
208        match statement return λs: joint_statement (graph_params params1 globals) globals. codeT globals (graph_params params1 globals) with
209        [ sequential seq l ⇒
210          let l' ≝ match l with [ an_identifier l ⇒ l ] in
211          let 〈the_graph, new_seq〉 ≝
212            match seq return λs. (codeT globals (graph_params params1 globals)) × ? with
213            [ COND acc_a cond_label ⇒
214              let cond_label' ≝ match cond_label with [ an_identifier l ⇒ l ] in
215              let relabelled ≝ an_identifier LabelTag (bvt_lookup … cond_label' map cond_label') in
216              let tail_graph ≝ relabel_graph' params1 globals the_graph map visited cond_label size_counter in
217                〈tail_graph, COND … acc_a relabelled〉
218            | _ ⇒ 〈the_graph, seq〉
219            ]
220          in
221            let tail_graph ≝ relabel_graph' params1 globals the_graph map visited l size_counter in
222            let relabelled ≝ an_identifier LabelTag (bvt_lookup … l' map l') in
223              add LabelTag … tail_graph relabelled_entry_point (sequential … new_seq relabelled)
224        | RETURN ⇒ the_graph
225        | GOTO l ⇒
226          let l' ≝ match l with [ an_identifier l ⇒ l ] in
227          let relabelled ≝ an_identifier LabelTag (bvt_lookup … l' map l') in
228            add LabelTag … the_graph relabelled_entry_point (GOTO … relabelled)         
229        ]
230      ]
231    ]
232  ].
233  cases daemon
234qed.
235
236definition relabel_graph ≝
237  λglobals: list ident.
238  λparams1: params1.
239  λmap: BitVectorTrie Word 16.
240  λint_fun: joint_internal_function globals (graph_params params1 globals).
241    match joint_if_entry … int_fun with
242    [ dp entry entry_prf ⇒
243      let code ≝ joint_if_code … int_fun in
244        relabel_graph' … code map (Stub …) entry (graph_num_nodes … code)
245    ].
246   
247definition pre_erase_joint_internal_function ≝
248  λglobals: list ident.
249  λpars: params globals.
250  λerasure_function: joint_internal_function globals pars → (BitVectorTrie Word 16) × (codeT … pars).
251  λrelabelling_function: BitVectorTrie Word 16 → joint_internal_function globals pars → codeT … pars.
252  λint_fun: joint_internal_function globals pars.
253  match joint_if_entry … int_fun with
254  [ dp entry entry_prf ⇒
255    match joint_if_exit … int_fun with
256    [ dp exit exit_prf ⇒
257      let exit' ≝ word_of_identifier … exit in
258      let entry' ≝ word_of_identifier … entry in
259      let 〈maps, code〉 ≝ erasure_function int_fun in
260      let int_fun ≝ set_joint_code globals pars int_fun code entry exit in
261      let code ≝ relabelling_function maps int_fun in
262        set_joint_code globals pars int_fun code (an_identifier … (bvt_lookup … entry' maps entry'))
263        (an_identifier … (bvt_lookup … exit' maps exit'))
264    ]
265  ].
266  cases daemon (* XXX *)
267qed.
268
269definition erase_graph_program:
270    ∀params1: params1. joint_program (graph_params params1) → joint_program (graph_params params1) ≝
271  λparams1.
272  λprogram.
273    transform_program … program (transf_fundef … (pre_erase_joint_internal_function … (pre_erase_graph_internal_function …) (relabel_graph …))).
274
275definition erase_lin_program: lin_program → lin_program ≝
276  λprogram.
277    transform_program … program (transf_fundef … (pre_erase_joint_internal_function … (pre_erase_lin_internal_function …) (relabel_lin_internal_function …))).
Note: See TracBrowser for help on using the repository browser.