source: src/joint/Erasure.ma @ 1697

Last change on this file since 1697 was 1515, checked in by campbell, 10 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.