Changeset 1467 for src/joint

Timestamp:

Oct 26, 2011, 5:25:15 PM (10 years ago)

Author:

mulligan

Message:

small change, adding entry and exit labels into the internal function, as these are necessary in graph based languages, unlike lin

File:

• src/joint/ProofUtils.ma (modified) (1 diff)

src/joint/ProofUtils.ma

@@ -249 +249 @@
   let stacksize ≝ joint_if_stacksize … int_fun in
   let code ≝ joint_if_code … int_fun in
-  let entry ≝ ? in
-  let exit ≝ ? in
-  let 〈maps, code〉 ≝ pre_erase_graph_internal_function params1 sem_params globals state code [ ] in
-  let code ≝ relabel_graph params1 sem_params globals state code maps in
-      mk_joint_internal_function …
-        luniverse runiverse result params
-        locals stacksize code entry exit.
+  match joint_if_entry … int_fun with
+  [ dp entry entry_prf ⇒
+    match joint_if_exit … int_fun with
+    [ dp exit exit_prf ⇒
+      let 〈maps, code〉 ≝ pre_erase_graph_internal_function params1 sem_params globals state code [ ] in
+      let code ≝ relabel_graph params1 sem_params globals state code maps in
+        mk_joint_internal_function …
+          luniverse runiverse result params
+          locals stacksize code entry exit
+    ]
+  ].
   cases daemon (* XXX *)
 qed.