 Timestamp:
 Oct 27, 2011, 5:29:32 PM (9 years ago)
 File:

 1 edited
Legend:
 Unmodified
 Added
 Removed

src/joint/ProofUtils.ma
r1469 r1470 158 158 [ None ⇒ ⊥ (* XXX: should not happen *) 159 159  Some statement ⇒ 160 let entered_previously ≝ ? in 160 161 let visited ≝ insert … entry_point' true visited in 161 let entered_previously ≝ ? in162 162 match entered_previously return λe: bool. ((BitVectorTrie Word 16) × (BitVectorTrie bool 16) × (codeT globals (graph_params params1 globals))) with 163 163 [ true ⇒ 〈map, visited, the_graph〉 … … 206 206 〈map, the_graph〉. 207 207 208 axiom 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). 208 let rec relabel_graph' 209 (params1: params1) (globals: list ident) 210 (the_graph: codeT globals (graph_params params1 globals)) (map: BitVectorTrie Word 16) 211 (visited: BitVectorTrie bool 16) (entry_point: label) (size_counter: nat) 212 on size_counter: codeT globals (graph_params params1 globals) ≝ 213 match size_counter return λs: nat. codeT globals (graph_params params1 globals) with 214 [ O ⇒ empty_graph … 215  S size_counter ⇒ 216 let entry_point' ≝ match entry_point with [ an_identifier e ⇒ e ] in 217 let relabelled_entry_point ≝ an_identifier LabelTag ? in 218 let statement ≝ lookup LabelTag ? the_graph entry_point in 219 match statement return λs: option (joint_statement (graph_params params1 globals) globals). codeT globals (graph_params params1 globals) with 220 [ None ⇒ ⊥ (* XXX: should not happen *) 221  Some statement ⇒ 222 let entered_previously ≝ ? in 223 let visited ≝ insert … entry_point' true visited in 224 match entered_previously return λe: bool. codeT globals (graph_params params1 globals) with 225 [ true ⇒ the_graph 226  false ⇒ (* XXX: never visited here before *) 227 match statement return λs: joint_statement (graph_params params1 globals) globals. codeT globals (graph_params params1 globals) with 228 [ sequential seq l ⇒ 229 let l' ≝ match l with [ an_identifier l ⇒ l ] in 230 let 〈the_graph, new_seq〉 ≝ 231 match seq return λs. (codeT globals (graph_params params1 globals)) × ? with 232 [ COND acc_a cond_label ⇒ 233 let cond_label' ≝ match cond_label with [ an_identifier l ⇒ l ] in 234 let relabelled ≝ an_identifier LabelTag ? in 235 let tail_graph ≝ relabel_graph' params1 globals the_graph map visited cond_label size_counter in 236 〈tail_graph, COND … acc_a relabelled〉 237  _ ⇒ 〈the_graph, seq〉 238 ] 239 in 240 match size_counter with 241 [ O ⇒ ⊥ (* XXX: impossible *) 242  S size_counter ⇒ 243 let tail_graph ≝ relabel_graph' params1 globals the_graph map visited l size_counter in 244 let relabelled ≝ an_identifier LabelTag ? in 245 add LabelTag … tail_graph relabelled_entry_point (sequential … new_seq relabelled) 246 ] 247  RETURN ⇒ the_graph 248  GOTO l ⇒ 249 let l' ≝ match l with [ an_identifier l ⇒ l ] in 250 let relabelled ≝ an_identifier LabelTag ? in 251 add LabelTag … the_graph relabelled_entry_point (GOTO … relabelled) 252 ] 253 ] 254 ] 255 ]. 256 [3: @(lookup … l' map l') 257 4: @(lookup … cond_label' map cond_label') 258 5: @(lookup … l' map l') 259 6: @(lookup … entry_point' visited false) 260 7: @(lookup … entry_point' map entry_point') 261 *: cases daemon 262 ] 263 qed. 216 264 217 265 definition relabel_graph ≝ … … 219 267 λglobals: list ident. 220 268 λthe_graph: codeT globals (graph_params params1 globals). 269 λentry_point: label. 221 270 λmap: BitVectorTrie Word 16. 222 relabel_graph' params1 globals the_graph map (Stub …) (graph_num_nodes … the_graph).271 relabel_graph' params1 globals the_graph map (Stub …) entry_point (graph_num_nodes … the_graph). 223 272 224 273 definition pre_erase_graph_joint_internal_function ≝ … … 238 287 [ dp exit exit_prf ⇒ 239 288 let 〈maps, code〉 ≝ pre_erase_graph_internal_function params1 globals code entry in 240 let code ≝ relabel_graph params1 globals code maps in289 let code ≝ relabel_graph params1 globals code entry maps in 241 290 mk_joint_internal_function … 242 291 luniverse runiverse result params
Note: See TracChangeset
for help on using the changeset viewer.