source: src/joint/Erasure.ma @ 2562

Last change on this file since 2562 was 2103, checked in by campbell, 8 years ago

Make transform_*program take a more general transformation to make
properties easier to state.

File size: 11.6 KB
RevLine 
[1463]1include "LIN/LIN.ma".
[1471]2include "joint/SemanticUtils.ma".
[1463]3
4let rec pre_erase_lin_internal_function'
5  (globals: list ident) (the_program: list (lin_statement globals))
6    (labels: list label)
[1515]7      on the_program: ((identifier_map ? label) × (list (lin_statement globals))) ≝
[1463]8  match the_program with
9  [ nil        ⇒
10    match labels with
[1515]11    [ nil ⇒ 〈empty_map …, [ ]〉 (* XXX: labels should be empty *)
[1463]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
[1515]34            let maps ≝ foldr ? ? (λl. λmap. add … map l lbl) maps (lbl :: labels)
[1463]35            in
36              〈maps, instructions〉
37          ]
38        | _ ⇒
39          let 〈maps, instructions〉 ≝ pre_erase_lin_internal_function' globals tl labels in
[1515]40          let maps ≝ foldr ? ? (λl. λmap. add … map l lbl) maps (lbl :: labels)
[1463]41          in
42            〈maps, instructions〉
43        ]
44      ]
45  ].
46  @daemon
47qed.
48
[1471]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
[1466]54definition relabel_joint_instruction:
55    ∀globals: list ident.
56    ∀params: params_.
[1515]57      identifier_map LabelTag label → joint_instruction params globals → joint_instruction params globals ≝
[1463]58  λglobals: list ident.
[1466]59  λparams.
[1463]60  λmap.
61  λinstr.
62  match instr with
63  [ COND acc_a lbl ⇒
[1515]64    let located ≝ lookup_def ?? map lbl lbl in
[1466]65      COND params globals acc_a located
[1463]66  | _ ⇒ instr
67  ].
68
[1466]69definition relabel_joint_statement:
70  ∀globals: list ident.
71  ∀params: params_.
[1515]72    identifier_map LabelTag label → joint_statement params globals → joint_statement params globals ≝
[1463]73  λglobals: list ident.
[1466]74  λparams: params_.
[1515]75  λmap: identifier_map LabelTag label.
[1466]76  λstmt: joint_statement params globals.
[1463]77  match stmt with
78  [ sequential seq l ⇒
[1466]79    let relabelled ≝ relabel_joint_instruction globals params map seq in
80      sequential params globals relabelled l
81  | RETURN ⇒ RETURN params globals
[1463]82  | GOTO l ⇒
[1515]83    let located ≝ lookup_def ?? map l l in
[1466]84      GOTO params globals located
[1463]85  ].
86
[1471]87let rec relabel_lin_internal_function'
[1515]88  (globals: list ident) (map: identifier_map LabelTag label)
[1463]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
[1466]95    let relabelled ≝ relabel_joint_statement globals lin_params_ map stmt in
[1463]96    let label ≝
97      match label with
98      [ None ⇒ None …
99      | Some label ⇒
[1515]100          Some … (lookup_def ?? map label label)
[1463]101      ]
102    in
[1471]103      〈label, relabelled〉 :: relabel_lin_internal_function' globals map tl
[1463]104  ].
105
[1471]106definition relabel_lin_internal_function ≝
[1463]107  λglobals.
[1471]108  λmap.
109  λint_fun: joint_internal_function globals (lin_params globals).
110    relabel_lin_internal_function' globals map (joint_if_code … int_fun).
[1463]111
[1466]112definition empty_graph ≝
113  λa: Type[0].
[1515]114    empty_map LabelTag a.
[1466]115
116let rec pre_erase_graph_internal_function'
[1469]117  (params1: params1) (globals: list ident)
118    (the_graph: codeT globals (graph_params params1 globals)) (labels: list label)
[1515]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
[1466]123  [ O ⇒
124    match labels with
[1469]125    [ nil ⇒ 〈map, visited, the_graph〉
[1466]126    | _   ⇒ ⊥
127    ]
[1469]128  | S size_counter ⇒
129    let statement ≝ lookup LabelTag ? the_graph entry_point in
[1515]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
[1469]131    [ None ⇒ ⊥ (* XXX: should not happen *)
132    | Some statement ⇒
[1515]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
[1469]135      [ true ⇒ 〈map, visited, the_graph〉
136      | false ⇒ (* XXX: never visited here before *)
[1515]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
[1469]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 ⇒
[1471]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
[1515]146            let map ≝ foldr … (λl. λmap. add … map l entry_point) map (entry_point :: labels) in
[1471]147              〈map, visited, the_graph〉
[1469]148          | _ ⇒
[1471]149            let 〈map, visited, the_graph〉 ≝ pre_erase_graph_internal_function' params1 globals the_graph [ ] l size_counter map visited in
[1515]150            let map ≝ foldr … (λl. λmap. add … map l entry_point) map (entry_point :: labels) in
[1469]151              〈map, visited, the_graph〉
[1466]152          ]
[1469]153        | RETURN ⇒
[1515]154          let map ≝ foldr … (λl. λmap. add … map l entry_point) map (entry_point :: labels) in
[1469]155            〈map, visited, the_graph〉
156        | GOTO l ⇒
[1471]157          let 〈map, visited, the_graph〉 ≝ pre_erase_graph_internal_function' params1 globals the_graph [ ] l size_counter map visited in
[1515]158          let map ≝ foldr … (λl. λmap. add … map l entry_point) map (entry_point :: labels) in
[1469]159            〈map, visited, the_graph〉
[1466]160        ]
161      ]
[1469]162    ]
[1466]163  ].
[1471]164  cases daemon
[1466]165qed.
166
167definition pre_erase_graph_internal_function ≝
168  λparams1: params1.
169  λglobals: list ident.
[1471]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
[1515]174    let 〈map, visited, the_graph〉 ≝ pre_erase_graph_internal_function' params1 globals code [ ] entry (graph_num_nodes … code) (empty_map …) (empty_map …) in
[1471]175      〈map, the_graph〉
176  ].
[1466]177
[1470]178let rec relabel_graph'
179  (params1: params1) (globals: list ident)
[1515]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)
[1470]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 ⇒
[1515]186    let relabelled_entry_point ≝ lookup_def … map entry_point entry_point in
[1470]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 ⇒
[1515]191      let entered_previously ≝ lookup_def … visited entry_point false in
[1470]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 *)
[1515]195        let visited ≝ add … visited entry_point true in
[1470]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 ⇒
[1515]201              let relabelled ≝ lookup_def … map cond_label cond_label in
[1470]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
[1471]207            let tail_graph ≝ relabel_graph' params1 globals the_graph map visited l size_counter in
[1515]208            let relabelled ≝ lookup_def … map l l in
[1471]209              add LabelTag … tail_graph relabelled_entry_point (sequential … new_seq relabelled)
[1470]210        | RETURN ⇒ the_graph
211        | GOTO l ⇒
[1515]212          let relabelled ≝ lookup_def … map l l in
[1470]213            add LabelTag … the_graph relabelled_entry_point (GOTO … relabelled)         
214        ]
215      ]
216    ]
217  ].
[1471]218  cases daemon
[1470]219qed.
[1466]220
221definition relabel_graph ≝
[1471]222  λglobals: list ident.
[1469]223  λparams1: params1.
[1515]224  λmap: identifier_map LabelTag label.
[1471]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
[1515]229        relabel_graph' … code map (empty_map …) entry (graph_num_nodes … code)
[1471]230    ].
231   
232definition pre_erase_joint_internal_function ≝
[1466]233  λglobals: list ident.
[1471]234  λpars: params globals.
[1515]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.
[1471]237  λint_fun: joint_internal_function globals pars.
[1467]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 ⇒
[1471]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
[1515]245        set_joint_code globals pars int_fun code (lookup_def … maps entry entry)
246        (lookup_def … maps exit exit)
[1467]247    ]
248  ].
[1466]249  cases daemon (* XXX *)
[1471]250qed.
251
252definition erase_graph_program:
253    ∀params1: params1. joint_program (graph_params params1) → joint_program (graph_params params1) ≝
254  λparams1.
255  λprogram.
[2103]256    transform_program … program (transf_fundef … (λvarnames. pre_erase_joint_internal_function varnames … (pre_erase_graph_internal_function varnames …) (relabel_graph varnames …))).
[1471]257
258definition erase_lin_program: lin_program → lin_program ≝
259  λprogram.
[2103]260    transform_program … program (transf_fundef … (λvarnames. pre_erase_joint_internal_function varnames … (pre_erase_lin_internal_function varnames …) (relabel_lin_internal_function varnames …))).
Note: See TracBrowser for help on using the repository browser.