source: src/joint/ProofUtils.ma @ 1469

Last change on this file since 1469 was 1469, checked in by mulligan, 9 years ago

finished new relabelling for graphs subject to one axiom closed

File size: 10.2 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) (globals: list ident)
144    (the_graph: codeT globals (graph_params params1 globals)) (labels: list label)
145      (entry_point: label) (size_counter: nat) (map: BitVectorTrie Word 16)
146        (visited: BitVectorTrie bool 16)
147          on size_counter: ((BitVectorTrie Word 16) × (BitVectorTrie bool 16) × (codeT globals (graph_params params1 globals))) ≝
148  match size_counter return λ_.  ((BitVectorTrie Word 16) × (BitVectorTrie bool 16) × (codeT globals (graph_params params1 globals))) with
149  [ O ⇒
150    match labels with
151    [ nil ⇒ 〈map, visited, the_graph〉
152    | _   ⇒ ⊥
153    ]
154  | S size_counter ⇒
155    let entry_point' ≝ match entry_point with [ an_identifier e ⇒ e ] in
156    let statement ≝ lookup LabelTag ? the_graph entry_point in
157    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
158    [ None ⇒ ⊥ (* XXX: should not happen *)
159    | Some statement ⇒
160      let visited ≝ insert … entry_point' true visited in
161      let entered_previously ≝ ? in
162      match entered_previously return λe: bool. ((BitVectorTrie Word 16) × (BitVectorTrie bool 16) × (codeT globals (graph_params params1 globals))) with
163      [ true ⇒ 〈map, visited, the_graph〉
164      | false ⇒ (* XXX: never visited here before *)
165        match statement return λs: joint_statement (graph_params params1 globals) globals. ((BitVectorTrie Word 16) × (BitVectorTrie bool 16) × (codeT globals (graph_params params1 globals))) with
166        [ sequential seq l ⇒
167          match seq with
168          [ COST_LABEL cost_label ⇒
169            pre_erase_graph_internal_function' params1 globals the_graph (entry_point :: labels) l size_counter map visited
170          | COND acc_a cond_label ⇒
171            let 〈map, visited, the_graph〉 ≝ pre_erase_graph_internal_function' params1 globals the_graph labels l size_counter map visited in
172              match size_counter with
173              [ O ⇒ ⊥ (* XXX: should never happen *)
174              | S size_counter ⇒
175                let 〈map, visited, the_graph〉 ≝ pre_erase_graph_internal_function' params1 globals the_graph labels cond_label size_counter map visited in
176                let map ≝ foldr … (λl. λmap. match l with [ an_identifier l ⇒ insert … l entry_point' map ]) map (entry_point :: labels) in
177                  〈map, visited, the_graph〉
178              ]
179          | _ ⇒
180            let 〈map, visited, the_graph〉 ≝ pre_erase_graph_internal_function' params1 globals the_graph labels l size_counter map visited in
181            let map ≝ foldr … (λl. λmap. match l with [ an_identifier l ⇒ insert … l entry_point' map ]) map (entry_point :: labels) in
182              〈map, visited, the_graph〉
183          ]
184        | RETURN ⇒
185          let map ≝ foldr … (λl. λmap. match l with [ an_identifier l ⇒ insert … l entry_point' map ]) map (entry_point :: labels) in
186            〈map, visited, the_graph〉
187        | GOTO l ⇒
188          let 〈map, visited, the_graph〉 ≝ pre_erase_graph_internal_function' params1 globals the_graph labels l size_counter map visited in
189          let map ≝ foldr … (λl. λmap. match l with [ an_identifier l ⇒ insert … l entry_point' map ]) map (entry_point :: labels) in
190            〈map, visited, the_graph〉
191        ]
192      ]
193    ]
194  ].
195  [4: @(lookup … entry_point' visited false)
196  |*: cases daemon
197  ]
198qed.
199
200definition pre_erase_graph_internal_function ≝
201  λparams1: params1.
202  λglobals: list ident.
203  λthe_graph: codeT globals (graph_params params1 globals).
204  λentry_point: label.
205    let 〈map, visited, the_graph〉 ≝ pre_erase_graph_internal_function' params1 globals the_graph [ ] entry_point (graph_num_nodes … the_graph) (Stub …) (Stub …) in
206      〈map, the_graph〉.
207
208axiom relabel_graph':
209  ∀params1: params1.
210  ∀globals: list ident.
211  ∀the_graph: codeT globals (graph_params params1 globals).
212  ∀map: BitVectorTrie Word 16.
213  ∀visited: BitVectorTrie bool 16.
214  ∀num_nodes: nat.
215    codeT globals (graph_params params1 globals).
216
217definition relabel_graph ≝
218  λparams1: params1.
219  λglobals: list ident.
220  λthe_graph: codeT globals (graph_params params1 globals).
221  λmap: BitVectorTrie Word 16.
222    relabel_graph' params1 globals the_graph map (Stub …) (graph_num_nodes … the_graph).
223
224definition pre_erase_graph_joint_internal_function ≝
225  λparams1: params1.
226  λglobals: list ident.
227  λint_fun: joint_internal_function globals (graph_params params1 globals).
228  let luniverse ≝ joint_if_luniverse globals (graph_params params1 globals) int_fun in
229  let runiverse ≝ joint_if_runiverse … int_fun in
230  let result ≝ joint_if_result … int_fun in
231  let params ≝ joint_if_params … int_fun in
232  let locals ≝ joint_if_locals … int_fun in
233  let stacksize ≝ joint_if_stacksize … int_fun in
234  let code ≝ joint_if_code … int_fun in
235  match joint_if_entry … int_fun with
236  [ dp entry entry_prf ⇒
237    match joint_if_exit … int_fun with
238    [ dp exit exit_prf ⇒
239      let 〈maps, code〉 ≝ pre_erase_graph_internal_function params1 globals code entry in
240      let code ≝ relabel_graph params1 globals code maps in
241        mk_joint_internal_function …
242          luniverse runiverse result params
243          locals stacksize code entry exit
244    ]
245  ].
246  cases daemon (* XXX *)
247qed.
Note: See TracBrowser for help on using the repository browser.