source: src/joint/ProofUtils.ma @ 1466

Last change on this file since 1466 was 1466, checked in by mulligan, 8 years ago

erasure for graph based joint languages almost complete

File size: 9.9 KB
Line 
1include "joint/Joint.ma".
2include "LIN/LIN.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 relabel_joint_instruction:
57    ∀globals: list ident.
58    ∀params: params_.
59      BitVectorTrie Word 16 → joint_instruction params globals → joint_instruction params globals ≝
60  λglobals: list ident.
61  λparams.
62  λmap.
63  λinstr.
64  match instr with
65  [ COND acc_a lbl ⇒
66    let lbl ≝ match lbl with [ an_identifier lbl ⇒ lbl ] in
67    let located ≝ an_identifier LabelTag (lookup … lbl map lbl) in
68      COND params globals acc_a located
69  | _ ⇒ instr
70  ].
71
72definition relabel_joint_statement:
73  ∀globals: list ident.
74  ∀params: params_.
75    BitVectorTrie Word 16 → joint_statement params globals → joint_statement params globals ≝
76  λglobals: list ident.
77  λparams: params_.
78  λmap: BitVectorTrie Word 16.
79  λstmt: joint_statement params globals.
80  match stmt with
81  [ sequential seq l ⇒
82    let relabelled ≝ relabel_joint_instruction globals params map seq in
83      sequential params globals relabelled l
84  | RETURN ⇒ RETURN params globals
85  | GOTO l ⇒
86    let l ≝ match l with [ an_identifier l ⇒ l ] in
87    let located ≝ an_identifier LabelTag (lookup … l map l) in
88      GOTO params globals located
89  ].
90
91let rec relabel
92  (globals: list ident) (map: BitVectorTrie Word 16)
93    (program: list (lin_statement globals))
94      on program: list (lin_statement globals) ≝
95  match program with
96  [ nil        ⇒ [ ]
97  | cons hd tl ⇒
98    let 〈label, stmt〉 ≝ hd in
99    let relabelled ≝ relabel_joint_statement globals lin_params_ map stmt in
100    let label ≝
101      match label with
102      [ None ⇒ None …
103      | Some label ⇒
104        let label ≝ match label with [ an_identifier l ⇒ l ] in
105          Some … (an_identifier LabelTag (lookup … label map label))
106      ]
107    in
108      〈label, relabelled〉 :: relabel globals map tl
109  ].
110
111definition pre_erase_lin_internal_function:
112    ∀globals: list ident. joint_internal_function globals (lin_params globals) → joint_internal_function globals (lin_params globals) ≝
113  λglobals.
114  λfunction.
115    let luniverse ≝ joint_if_luniverse … function in
116    let runiverse ≝ joint_if_runiverse … function in
117    let result ≝ joint_if_result … function in
118    let params ≝ joint_if_params … function in
119    let locals ≝ joint_if_locals … function in
120    let stacksize ≝ joint_if_stacksize … function in
121    let code ≝ joint_if_code … function in
122    let entry ≝ ? in
123    let exit ≝ ? in
124    let 〈maps, code〉 ≝ pre_erase_lin_internal_function' globals code [ ] in
125    let code ≝ relabel globals maps code in
126      mk_joint_internal_function …
127        luniverse runiverse result params
128        locals stacksize code entry exit.
129  cases daemon (* XXX *)
130qed.
131
132definition erase_lin_program: lin_program → lin_program ≝
133  λprogram.
134    transform_program … program (transf_fundef … (pre_erase_lin_internal_function …)).
135
136include "joint/SemanticUtils.ma".
137
138definition empty_graph ≝
139  λa: Type[0].
140    an_id_map LabelTag a (Stub a 16).
141
142let rec pre_erase_graph_internal_function'
143  (params1: params1) (sem_params: sem_params) (globals: list ident)
144    (state: state sem_params) (the_graph: codeT globals (graph_params params1 globals))
145      (labels: list label) (num_nodes: nat)
146        on num_nodes: ((BitVectorTrie Word 16) × (codeT globals (graph_params params1 globals))) ≝
147  match num_nodes return λn. ((BitVectorTrie Word 16) × (codeT globals (graph_params params1 globals))) with
148  [ O ⇒
149    match labels with
150    [ nil ⇒ 〈Stub Word 16, empty_graph …〉
151    | _   ⇒ ⊥
152    ]
153  | S num_nodes ⇒
154    let program_counter ≝ (pc … state) in
155      match code_pointer_of_address program_counter with
156      [ OK code_pointer ⇒
157        match graph_label_of_pointer code_pointer with
158        [ OK lbl ⇒
159          match lookup … the_graph lbl with
160          [ Some statement ⇒
161            let lbl' ≝ match lbl with [ an_identifier lbl ⇒ lbl ] in
162            let state ≝ set_pc … program_counter state in
163            match statement with
164            [ sequential seq l ⇒
165              match seq with
166              [ COST_LABEL cost_label ⇒ pre_erase_graph_internal_function' params1 sem_params globals state the_graph (lbl :: labels) num_nodes
167              | _ ⇒
168                let 〈maps, instructions〉 ≝ pre_erase_graph_internal_function' params1 sem_params globals state the_graph labels num_nodes in
169                let maps ≝ foldr … (λl. λmap. match l with [ an_identifier l ⇒ insert … l lbl' map ]) maps (lbl :: labels) in
170                  〈maps, instructions〉
171              ]
172            | _ ⇒
173              let 〈maps, instructions〉 ≝ pre_erase_graph_internal_function' params1 sem_params globals state the_graph labels num_nodes in
174              let maps ≝ foldr … (λl. λmap. match l with [ an_identifier l ⇒ insert … l lbl' map ]) maps (lbl :: labels) in
175                〈maps, instructions〉
176            ]
177          | None           ⇒ ⊥ (* XXX: shouldn't happen *)
178          ]
179        | Error message ⇒ ⊥ (* XXX: shouldn't happen *)
180        ]
181      | Error message   ⇒ ⊥ (* XXX: shouldn't happen *)
182      ]
183  ].
184  cases daemon (* XXX *)
185qed.
186
187definition pre_erase_graph_internal_function ≝
188  λparams1: params1.
189  λsem_params: sem_params.
190  λglobals: list ident.
191  λstate: state sem_params.
192  λthe_graph: codeT globals (graph_params params1 globals).
193  λlabels: list label.
194    pre_erase_graph_internal_function' params1 sem_params globals state the_graph labels (graph_num_nodes … the_graph).
195
196let rec relabel_graph'
197  (params1: params1) (sem_params: sem_params) (globals: list ident)
198    (state: state sem_params) (the_graph: codeT globals (graph_params params1 globals))
199      (map: BitVectorTrie Word 16) (num_nodes: nat)
200        on num_nodes: codeT globals (graph_params params1 globals) ≝
201  match num_nodes with
202  [ O ⇒ empty_graph …
203  | S num_nodes ⇒
204    let program_counter ≝ (pc … state) in
205    match code_pointer_of_address program_counter with
206    [ OK code_pointer ⇒
207      match graph_label_of_pointer code_pointer with
208      [ OK lbl ⇒
209        match lookup … the_graph lbl with
210        [ Some statement ⇒
211          let lbl' ≝ match lbl with [ an_identifier lbl ⇒ lbl ] in
212          let new_statement ≝ relabel_joint_statement globals (graph_params params1 globals) map statement in
213          let new_lbl ≝ an_identifier LabelTag ? in
214          let state' ≝ set_pc … program_counter state in
215          let tail_graph ≝ relabel_graph' params1 sem_params globals state' the_graph map num_nodes in
216            add … tail_graph new_lbl new_statement
217        | None ⇒ ⊥
218        ]
219      | Error message ⇒ ⊥
220      ]
221    | Error message ⇒ ⊥
222    ]         
223  ].
224  [2: @(lookup … lbl' map lbl')
225  |*: cases daemon (* XXX *)
226  ]
227qed.
228
229definition relabel_graph ≝
230  λparams1.
231  λsem_params.
232  λglobals.
233  λstate: state sem_params.
234  λthe_graph: codeT globals (graph_params params1 globals).
235  λmap: BitVectorTrie Word 16.
236    relabel_graph' params1 sem_params globals state the_graph map (graph_num_nodes … the_graph).
237
238definition pre_erase_graph_joint_internal_function ≝
239  λparams1: params1.
240  λsem_params: sem_params.
241  λglobals: list ident.
242  λstate: state sem_params.
243  λint_fun: joint_internal_function globals (graph_params params1 globals).
244  let luniverse ≝ joint_if_luniverse globals (graph_params params1 globals) int_fun in
245  let runiverse ≝ joint_if_runiverse … int_fun in
246  let result ≝ joint_if_result … int_fun in
247  let params ≝ joint_if_params … int_fun in
248  let locals ≝ joint_if_locals … int_fun in
249  let stacksize ≝ joint_if_stacksize … int_fun in
250  let code ≝ joint_if_code … int_fun in
251  let entry ≝ ? in
252  let exit ≝ ? in
253  let 〈maps, code〉 ≝ pre_erase_graph_internal_function params1 sem_params globals state code [ ] in
254  let code ≝ relabel_graph params1 sem_params globals state code maps in
255      mk_joint_internal_function …
256        luniverse runiverse result params
257        locals stacksize code entry exit.
258  cases daemon (* XXX *)
259qed.
260
261(* XXX: use make_initial_state to build an initial state for a program *)
Note: See TracBrowser for help on using the repository browser.