Changeset 1633 for src/Cminor/test/null-op.Cminor.ma

Timestamp:

Jan 4, 2012, 7:19:09 PM (8 years ago)

Author:

campbell

Message:

Update Cminor pretty printer and examples.

File:

• src/Cminor/test/null-op.Cminor.ma (modified) (6 diffs)

src/Cminor/test/null-op.Cminor.ma

@@ -1 +1 @@
 include "Cminor/semantics.ma".
 include "common/Animation.ma".
+
+definition label_of_nat : nat -> identifier Label := identifier_of_nat ?.
 
 
@@ -15 +17 @@
   (Some ? (ASTint I32 Signed))
   []
-  [pair ?? id_main_p (ASTptr Any); pair ?? id_main_q (ASTptr Any)]
-  1 (
+  [mk_Prod ?? id_main_p (ASTptr Any); mk_Prod ?? id_main_q (ASTptr Any)]
+  (match daemon in False with [ ])
+1 (
   St_cost C_cost4 (
   St_seq (
-    St_assign (ASTptr Any) id_main_p (Op1 (ASTint I8 Signed) (ASTptr Any) (Optrofint Any) (Cst (ASTint I8 Signed) (Ointconst I8 (repr ? 0))))
+    St_assign (ASTptr Any) id_main_p (Op1 (ASTint I8 Signed) (ASTptr Any) (Optrofint ?? Any) (Cst (ASTint I8 Signed) (Ointconst I8 (repr ? 0))))
   ) (
   St_seq (
@@ -27 +30 @@
     St_ifthenelse I32 Signed (Op2 (ASTptr Any) (ASTptr Any) (ASTint I32 Signed) (Ocmpp Ceq) (Id (ASTptr Any) id_main_p) (Id (ASTptr Any) id_main_q)) (
       St_cost C_cost2 (
-      St_return (Some ? (dp ?? (ASTint I32 Signed) (Op1 (ASTint I8 Signed) (ASTint I32 Signed) (Ocastint Signed I32) (Cst (ASTint I8 Signed) (Ointconst I8 (repr ? 0))))))
+      St_return (Some ? (mk_DPair ?? (ASTint I32 Signed) (Op1 (ASTint I8 Signed) (ASTint I32 Signed) (Ocastint ????) (Cst (ASTint I8 Signed) (Ointconst I8 (repr ? 0))))))
       )
     ) (
@@ -37 +40 @@
     St_ifthenelse I32 Signed (Op2 (ASTint I32 Signed) (ASTint I32 Signed) (ASTint I32 Signed) (Ocmp Cgt) (Op2 (ASTptr Any) (ASTptr Any) (ASTint I32 Signed) (Osubpp I32) (Id (ASTptr Any) id_main_p) (Id (ASTptr Any) id_main_p)) (Cst (ASTint I32 Signed) (Ointconst I32 (repr ? 0)))) (
       St_cost C_cost0 (
-      St_return (Some ? (dp ?? (ASTint I32 Signed) (Op1 (ASTint I8 Signed) (ASTint I32 Signed) (Ocastint Signed I32) (Cst (ASTint I8 Signed) (Ointconst I8 (repr ? 0))))))
+      St_return (Some ? (mk_DPair ?? (ASTint I32 Signed) (Op1 (ASTint I8 Signed) (ASTint I32 Signed) (Ocastint ????) (Cst (ASTint I8 Signed) (Ointconst I8 (repr ? 0))))))
       )
     ) (
@@ -45 +48 @@
   ) (
   St_seq (
-    St_assign (ASTptr Any) id_main_p (Op2 (ASTptr Any) (ASTint I8 Signed) (ASTptr Any) Oaddp (Id (ASTptr Any) id_main_p) (Op2 (ASTint I8 Signed) (ASTint I8 Signed) (ASTint I8 Signed) Omul (Cst (ASTint I8 Signed) (Ointconst I8 (repr ? 0))) (Cst (ASTint I8 Signed) (Ointconst I8 (repr ? 1)))))
+    St_assign (ASTptr Any) id_main_p (Op2 (ASTptr Any) (ASTint I32 Signed) (ASTptr Any) Oaddp (Id (ASTptr Any) id_main_p) (Op2 (ASTint I32 Signed) (ASTint I32 Signed) (ASTint I32 Signed) Omul (Cst (ASTint I32 Signed) (Ointconst I32 (repr ? 0))) (Cst (ASTint I32 Signed) (Ointconst I32 (repr ? 1)))))
   ) (
   St_seq (
-    St_assign (ASTptr Any) id_main_p (Op2 (ASTptr Any) (ASTint I8 Signed) (ASTptr Any) Oaddp (Id (ASTptr Any) id_main_p) (Op2 (ASTint I8 Signed) (ASTint I8 Signed) (ASTint I8 Signed) Omul (Cst (ASTint I8 Signed) (Ointconst I8 (repr ? 0))) (Cst (ASTint I8 Signed) (Ointconst I8 (repr ? 1)))))
+    St_assign (ASTptr Any) id_main_p (Op2 (ASTptr Any) (ASTint I32 Signed) (ASTptr Any) Oaddp (Id (ASTptr Any) id_main_p) (Op2 (ASTint I32 Signed) (ASTint I32 Signed) (ASTint I32 Signed) Omul (Cst (ASTint I32 Signed) (Ointconst I32 (repr ? 0))) (Cst (ASTint I32 Signed) (Ointconst I32 (repr ? 1)))))
   ) (
   St_seq (
-    St_assign (ASTptr Any) id_main_p (Op2 (ASTptr Any) (ASTint I8 Signed) (ASTptr Any) Osubpi (Id (ASTptr Any) id_main_p) (Op2 (ASTint I8 Signed) (ASTint I8 Signed) (ASTint I8 Signed) Omul (Cst (ASTint I8 Signed) (Ointconst I8 (repr ? 0))) (Cst (ASTint I8 Signed) (Ointconst I8 (repr ? 1)))))
+    St_assign (ASTptr Any) id_main_p (Op2 (ASTptr Any) (ASTint I32 Signed) (ASTptr Any) Osubpi (Id (ASTptr Any) id_main_p) (Op2 (ASTint I32 Signed) (ASTint I32 Signed) (ASTint I32 Signed) Omul (Cst (ASTint I32 Signed) (Ointconst I32 (repr ? 0))) (Cst (ASTint I32 Signed) (Ointconst I32 (repr ? 1)))))
   ) (
-  St_return (Some ? (dp ?? (ASTint I32 Signed) (Op2 (ASTptr Any) (ASTptr Any) (ASTint I32 Signed) (Ocmpp Ceq) (Id (ASTptr Any) id_main_p) (Op1 (ASTint I8 Signed) (ASTptr Any) (Optrofint Any) (Cst (ASTint I8 Signed) (Ointconst I8 (repr ? 0)))))))
+  St_return (Some ? (mk_DPair ?? (ASTint I32 Signed) (Op2 (ASTptr Any) (ASTptr Any) (ASTint I32 Signed) (Ocmpp Ceq) (Id (ASTptr Any) id_main_p) (Op1 (ASTint I32 Signed) (ASTptr Any) (Optrofint ?? Any) (Cst (ASTint I32 Signed) (Ointconst I32 (repr ? 0)))))))
   )
   )
@@ -63 +66 @@
   )
 
-)).
+) (match daemon in False with [ ])).
 
 
 
 definition myprog : Cminor_program :=
-mk_program ?? [
-  (pair ?? id_main f_main)
+mk_program ?? [] [
+  (mk_Prod ?? id_main f_main)
 ]  id_main
-[]
 .
-
-example exec: finishes_with (repr I32 1) ? (exec_up_to Cminor_fullexec myprog 1000 [ ]).
-normalize  (* you can examine the result here *)
-@refl
-qed.
-
-include "Cminor/toRTLabs.ma".
-include "RTLabs/semantics.ma".
-
-example execRTL: finishes_with (repr 1) ? (do myprog' ← cminor_init_to_rtlabs myprog; exec_up_to RTLabs_fullexec myprog' 1000 [ ]).
-normalize  (* you can examine the result here *)
-@refl
-qed.
-