source: src/joint/Erasure.ma @ 1651

Last change on this file since 1651 was 1515, checked in by campbell, 8 years ago

Add type of maps on positive binary numbers, and use them for identifers.

Also:

  • fix interpretation for - on positives
  • move eq_nat_dec to a more appropriate place
  • split out costs from other identifiers in ASM
  • use identifier abstractions in back-end
File size: 11.5 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: ((identifier_map ? label) × (list (lin_statement globals))) ≝
8  match the_program with
9  [ nil        ⇒
10    match labels with
11    [ nil ⇒ 〈empty_map …, [ ]〉 (* 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        match instr with
29        [ sequential seq l ⇒
30          match seq with
31          [ COST_LABEL cost ⇒ pre_erase_lin_internal_function' globals tl (lbl :: labels)
32          | _ ⇒
33            let 〈maps, instructions〉 ≝ pre_erase_lin_internal_function' globals tl labels in
34            let maps ≝ foldr ? ? (λl. λmap. add … map l lbl) maps (lbl :: labels)
35            in
36              〈maps, instructions〉
37          ]
38        | _ ⇒
39          let 〈maps, instructions〉 ≝ pre_erase_lin_internal_function' globals tl labels in
40          let maps ≝ foldr ? ? (λl. λmap. add … map l lbl) maps (lbl :: labels)
41          in
42            〈maps, instructions〉
43        ]
44      ]
45  ].
46  @daemon
47qed.
48
49definition pre_erase_lin_internal_function ≝
50  λglobals: list ident.
51  λint_fun: joint_internal_function … (lin_params globals).
52    pre_erase_lin_internal_function' … (joint_if_code … (lin_params …) int_fun) [ ].
53
54definition relabel_joint_instruction:
55    ∀globals: list ident.
56    ∀params: params_.
57      identifier_map LabelTag label → joint_instruction params globals → joint_instruction params globals ≝
58  λglobals: list ident.
59  λparams.
60  λmap.
61  λinstr.
62  match instr with
63  [ COND acc_a lbl ⇒
64    let located ≝ lookup_def ?? map lbl lbl in
65      COND params globals acc_a located
66  | _ ⇒ instr
67  ].
68
69definition relabel_joint_statement:
70  ∀globals: list ident.
71  ∀params: params_.
72    identifier_map LabelTag label → joint_statement params globals → joint_statement params globals ≝
73  λglobals: list ident.
74  λparams: params_.
75  λmap: identifier_map LabelTag label.
76  λstmt: joint_statement params globals.
77  match stmt with
78  [ sequential seq l ⇒
79    let relabelled ≝ relabel_joint_instruction globals params map seq in
80      sequential params globals relabelled l
81  | RETURN ⇒ RETURN params globals
82  | GOTO l ⇒
83    let located ≝ lookup_def ?? map l l in
84      GOTO params globals located
85  ].
86
87let rec relabel_lin_internal_function'
88  (globals: list ident) (map: identifier_map LabelTag label)
89    (program: list (lin_statement globals))
90      on program: list (lin_statement globals) ≝
91  match program with
92  [ nil        ⇒ [ ]
93  | cons hd tl ⇒
94    let 〈label, stmt〉 ≝ hd in
95    let relabelled ≝ relabel_joint_statement globals lin_params_ map stmt in
96    let label ≝
97      match label with
98      [ None ⇒ None …
99      | Some label ⇒
100          Some … (lookup_def ?? map label label)
101      ]
102    in
103      〈label, relabelled〉 :: relabel_lin_internal_function' globals map tl
104  ].
105
106definition relabel_lin_internal_function ≝
107  λglobals.
108  λmap.
109  λint_fun: joint_internal_function globals (lin_params globals).
110    relabel_lin_internal_function' globals map (joint_if_code … int_fun).
111
112definition empty_graph ≝
113  λa: Type[0].
114    empty_map LabelTag a.
115
116let rec pre_erase_graph_internal_function'
117  (params1: params1) (globals: list ident)
118    (the_graph: codeT globals (graph_params params1 globals)) (labels: list label)
119      (entry_point: label) (size_counter: nat) (map: identifier_map LabelTag label)
120        (visited: identifier_map LabelTag bool)
121          on size_counter: ((identifier_map LabelTag label) × (identifier_map LabelTag bool) × (codeT globals (graph_params params1 globals))) ≝
122  match size_counter return λ_.  ((identifier_map LabelTag label) × (identifier_map LabelTag bool) × (codeT globals (graph_params params1 globals))) with
123  [ O ⇒
124    match labels with
125    [ nil ⇒ 〈map, visited, the_graph〉
126    | _   ⇒ ⊥
127    ]
128  | S size_counter ⇒
129    let statement ≝ lookup LabelTag ? the_graph entry_point in
130    match statement return λs: option (joint_statement (graph_params params1 globals) globals). ((identifier_map LabelTag label) × (identifier_map LabelTag bool) × (codeT globals (graph_params params1 globals))) with
131    [ None ⇒ ⊥ (* XXX: should not happen *)
132    | Some statement ⇒
133      let entered_previously ≝ lookup_def … visited entry_point false in
134      match entered_previously return λe: bool. ((identifier_map LabelTag label) × (identifier_map LabelTag bool) × (codeT globals (graph_params params1 globals))) with
135      [ true ⇒ 〈map, visited, the_graph〉
136      | false ⇒ (* XXX: never visited here before *)
137        let visited ≝ add … visited entry_point true in
138        match statement return λs: joint_statement (graph_params params1 globals) globals. ((identifier_map LabelTag label) × (identifier_map LabelTag bool) × (codeT globals (graph_params params1 globals))) with
139        [ sequential seq l ⇒
140          match seq with
141          [ COST_LABEL cost_label ⇒
142            pre_erase_graph_internal_function' params1 globals the_graph (entry_point :: labels) l size_counter map visited
143          | COND acc_a cond_label ⇒
144            let 〈map, visited, the_graph〉 ≝ pre_erase_graph_internal_function' params1 globals the_graph [ ] l size_counter map visited in
145            let 〈map, visited, the_graph〉 ≝ pre_erase_graph_internal_function' params1 globals the_graph [ ] cond_label size_counter map visited in
146            let map ≝ foldr … (λl. λmap. add … map l entry_point) map (entry_point :: labels) in
147              〈map, visited, the_graph〉
148          | _ ⇒
149            let 〈map, visited, the_graph〉 ≝ pre_erase_graph_internal_function' params1 globals the_graph [ ] l size_counter map visited in
150            let map ≝ foldr … (λl. λmap. add … map l entry_point) map (entry_point :: labels) in
151              〈map, visited, the_graph〉
152          ]
153        | RETURN ⇒
154          let map ≝ foldr … (λl. λmap. add … map l entry_point) map (entry_point :: labels) in
155            〈map, visited, the_graph〉
156        | GOTO l ⇒
157          let 〈map, visited, the_graph〉 ≝ pre_erase_graph_internal_function' params1 globals the_graph [ ] l size_counter map visited in
158          let map ≝ foldr … (λl. λmap. add … map l entry_point) map (entry_point :: labels) in
159            〈map, visited, the_graph〉
160        ]
161      ]
162    ]
163  ].
164  cases daemon
165qed.
166
167definition pre_erase_graph_internal_function ≝
168  λparams1: params1.
169  λglobals: list ident.
170  λint_fun: joint_internal_function globals (graph_params params1 globals).
171  match joint_if_entry … int_fun with
172  [ dp entry entry_proof ⇒
173    let code ≝ joint_if_code … int_fun in
174    let 〈map, visited, the_graph〉 ≝ pre_erase_graph_internal_function' params1 globals code [ ] entry (graph_num_nodes … code) (empty_map …) (empty_map …) in
175      〈map, the_graph〉
176  ].
177
178let rec relabel_graph'
179  (params1: params1) (globals: list ident)
180    (the_graph: codeT globals (graph_params params1 globals)) (map: identifier_map LabelTag label)
181      (visited: identifier_map LabelTag bool) (entry_point: label) (size_counter: nat)
182        on size_counter: codeT globals (graph_params params1 globals) ≝
183  match size_counter return λs: nat. codeT globals (graph_params params1 globals) with
184  [ O ⇒ empty_graph …
185  | S size_counter ⇒
186    let relabelled_entry_point ≝ lookup_def … map entry_point entry_point in
187    let statement ≝ lookup LabelTag ? the_graph entry_point in
188    match statement return λs: option (joint_statement (graph_params params1 globals) globals). codeT globals (graph_params params1 globals) with
189    [ None ⇒ ⊥ (* XXX: should not happen *)
190    | Some statement ⇒
191      let entered_previously ≝ lookup_def … visited entry_point false in
192      match entered_previously return λe: bool. codeT globals (graph_params params1 globals) with
193      [ true ⇒ the_graph
194      | false ⇒ (* XXX: never visited here before *)
195        let visited ≝ add … visited entry_point true in
196        match statement return λs: joint_statement (graph_params params1 globals) globals. codeT globals (graph_params params1 globals) with
197        [ sequential seq l ⇒
198          let 〈the_graph, new_seq〉 ≝
199            match seq return λs. (codeT globals (graph_params params1 globals)) × ? with
200            [ COND acc_a cond_label ⇒
201              let relabelled ≝ lookup_def … map cond_label cond_label in
202              let tail_graph ≝ relabel_graph' params1 globals the_graph map visited cond_label size_counter in
203                〈tail_graph, COND … acc_a relabelled〉
204            | _ ⇒ 〈the_graph, seq〉
205            ]
206          in
207            let tail_graph ≝ relabel_graph' params1 globals the_graph map visited l size_counter in
208            let relabelled ≝ lookup_def … map l l in
209              add LabelTag … tail_graph relabelled_entry_point (sequential … new_seq relabelled)
210        | RETURN ⇒ the_graph
211        | GOTO l ⇒
212          let relabelled ≝ lookup_def … map l l in
213            add LabelTag … the_graph relabelled_entry_point (GOTO … relabelled)         
214        ]
215      ]
216    ]
217  ].
218  cases daemon
219qed.
220
221definition relabel_graph ≝
222  λglobals: list ident.
223  λparams1: params1.
224  λmap: identifier_map LabelTag label.
225  λint_fun: joint_internal_function globals (graph_params params1 globals).
226    match joint_if_entry … int_fun with
227    [ dp entry entry_prf ⇒
228      let code ≝ joint_if_code … int_fun in
229        relabel_graph' … code map (empty_map …) entry (graph_num_nodes … code)
230    ].
231   
232definition pre_erase_joint_internal_function ≝
233  λglobals: list ident.
234  λpars: params globals.
235  λerasure_function: joint_internal_function globals pars → (identifier_map LabelTag label) × (codeT … pars).
236  λrelabelling_function: identifier_map LabelTag label → joint_internal_function globals pars → codeT … pars.
237  λint_fun: joint_internal_function globals pars.
238  match joint_if_entry … int_fun with
239  [ dp entry entry_prf ⇒
240    match joint_if_exit … int_fun with
241    [ dp exit exit_prf ⇒
242      let 〈maps, code〉 ≝ erasure_function int_fun in
243      let int_fun ≝ set_joint_code globals pars int_fun code entry exit in
244      let code ≝ relabelling_function maps int_fun in
245        set_joint_code globals pars int_fun code (lookup_def … maps entry entry)
246        (lookup_def … maps exit exit)
247    ]
248  ].
249  cases daemon (* XXX *)
250qed.
251
252definition erase_graph_program:
253    ∀params1: params1. joint_program (graph_params params1) → joint_program (graph_params params1) ≝
254  λparams1.
255  λprogram.
256    transform_program … program (transf_fundef … (pre_erase_joint_internal_function … (pre_erase_graph_internal_function …) (relabel_graph …))).
257
258definition erase_lin_program: lin_program → lin_program ≝
259  λprogram.
260    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.