source: src/joint/ProofUtils.ma @ 1471

Last change on this file since 1471 was 1471, checked in by mulligan, 10 years ago

finished erasure and generalised so as to work on arbitrary joint programs

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.