Changeset 1470 for src/joint/ProofUtils.ma

Timestamp:

Oct 27, 2011, 5:29:32 PM (8 years ago)

Author:

mulligan

Message:

finished, pretty ugly though as matita's disambiguation is a nightmare, so had to use tactics in some places

File:

• src/joint/ProofUtils.ma (modified) (4 diffs)

src/joint/ProofUtils.ma

@@ -158 +158 @@
     [ None ⇒ ⊥ (* XXX: should not happen *)
     | Some statement ⇒
+      let entered_previously ≝ ? in
       let visited ≝ insert … entry_point' true visited in
-      let entered_previously ≝ ? in
       match entered_previously return λe: bool. ((BitVectorTrie Word 16) × (BitVectorTrie bool 16) × (codeT globals (graph_params params1 globals))) with
       [ true ⇒ 〈map, visited, the_graph〉
@@ -206 +206 @@
       〈map, the_graph〉.
 
-axiom relabel_graph':
-  ∀params1: params1.
-  ∀globals: list ident.
-  ∀the_graph: codeT globals (graph_params params1 globals).
-  ∀map: BitVectorTrie Word 16.
-  ∀visited: BitVectorTrie bool 16.
-  ∀num_nodes: nat.
-    codeT globals (graph_params params1 globals).
+let rec relabel_graph'
+  (params1: params1) (globals: list ident)
+    (the_graph: codeT globals (graph_params params1 globals)) (map: BitVectorTrie Word 16)
+      (visited: BitVectorTrie bool 16) (entry_point: label) (size_counter: nat)
+        on size_counter: codeT globals (graph_params params1 globals) ≝
+  match size_counter return λs: nat. codeT globals (graph_params params1 globals) with
+  [ O ⇒ empty_graph …
+  | S size_counter ⇒
+    let entry_point' ≝ match entry_point with [ an_identifier e ⇒ e ] in
+    let relabelled_entry_point ≝ an_identifier LabelTag ? in
+    let statement ≝ lookup LabelTag ? the_graph entry_point in
+    match statement return λs: option (joint_statement (graph_params params1 globals) globals). codeT globals (graph_params params1 globals) with
+    [ None ⇒ ⊥ (* XXX: should not happen *)
+    | Some statement ⇒
+      let entered_previously ≝ ? in
+      let visited ≝ insert … entry_point' true visited in
+      match entered_previously return λe: bool. codeT globals (graph_params params1 globals) with
+      [ true ⇒ the_graph
+      | false ⇒ (* XXX: never visited here before *)
+        match statement return λs: joint_statement (graph_params params1 globals) globals. codeT globals (graph_params params1 globals) with
+        [ sequential seq l ⇒
+          let l' ≝ match l with [ an_identifier l ⇒ l ] in
+          let 〈the_graph, new_seq〉 ≝
+            match seq return λs. (codeT globals (graph_params params1 globals)) × ? with
+            [ COND acc_a cond_label ⇒
+              let cond_label' ≝ match cond_label with [ an_identifier l ⇒ l ] in
+              let relabelled ≝ an_identifier LabelTag ? in
+              let tail_graph ≝ relabel_graph' params1 globals the_graph map visited cond_label size_counter in
+                〈tail_graph, COND … acc_a relabelled〉
+            | _ ⇒ 〈the_graph, seq〉
+            ]
+          in
+            match size_counter with
+            [ O ⇒ ⊥ (* XXX: impossible *)
+            | S size_counter ⇒
+              let tail_graph ≝ relabel_graph' params1 globals the_graph map visited l size_counter in
+              let relabelled ≝ an_identifier LabelTag ? in
+                add LabelTag … tail_graph relabelled_entry_point (sequential … new_seq relabelled)
+            ]
+        | RETURN ⇒ the_graph
+        | GOTO l ⇒
+          let l' ≝ match l with [ an_identifier l ⇒ l ] in
+          let relabelled ≝ an_identifier LabelTag ? in
+            add LabelTag … the_graph relabelled_entry_point (GOTO … relabelled)          
+        ]
+      ]
+    ]
+  ].
+  [3: @(lookup … l' map l')
+  |4: @(lookup … cond_label' map cond_label')
+  |5: @(lookup … l' map l')
+  |6: @(lookup … entry_point' visited false)
+  |7: @(lookup … entry_point' map entry_point')
+  |*: cases daemon
+  ]
+qed.
 
 definition relabel_graph ≝
@@ -219 +267 @@
   λglobals: list ident.
   λthe_graph: codeT globals (graph_params params1 globals).
+  λentry_point: label.
   λmap: BitVectorTrie Word 16.
-    relabel_graph' params1 globals the_graph map (Stub …) (graph_num_nodes … the_graph).
+    relabel_graph' params1 globals the_graph map (Stub …) entry_point (graph_num_nodes … the_graph).
 
 definition pre_erase_graph_joint_internal_function ≝
@@ -238 +287 @@
     [ dp exit exit_prf ⇒
       let 〈maps, code〉 ≝ pre_erase_graph_internal_function params1 globals code entry in
-      let code ≝ relabel_graph params1 globals code maps in
+      let code ≝ relabel_graph params1 globals code entry maps in
         mk_joint_internal_function …
           luniverse runiverse result params