source: src/Cminor/test/null-op.Cminor.ma @ 2309

Last change on this file since 2309 was 1633, checked in by campbell, 9 years ago

Update Cminor pretty printer and examples.

File size: 3.3 KB
RevLine 
[898]1include "Cminor/semantics.ma".
2include "common/Animation.ma".
3
[1633]4definition label_of_nat : nat -> identifier Label := identifier_of_nat ?.
[898]5
6
[1633]7
[898]8definition id_main := ident_of_nat 0.
9definition id_main_p := ident_of_nat 6.
10definition id_main_q := ident_of_nat 7.
11definition C_cost4 := costlabel_of_nat 5.
12definition C_cost2 := costlabel_of_nat 4.
13definition C_cost3 := costlabel_of_nat 3.
14definition C_cost0 := costlabel_of_nat 2.
15definition C_cost1 := costlabel_of_nat 1.
16definition f_main := Internal ? (mk_internal_function
17  (Some ? (ASTint I32 Signed))
18  []
[1633]19  [mk_Prod ?? id_main_p (ASTptr Any); mk_Prod ?? id_main_q (ASTptr Any)]
20  (match daemon in False with [ ])
211 (
[898]22  St_cost C_cost4 (
23  St_seq (
[1633]24    St_assign (ASTptr Any) id_main_p (Op1 (ASTint I8 Signed) (ASTptr Any) (Optrofint ?? Any) (Cst (ASTint I8 Signed) (Ointconst I8 (repr ? 0))))
[898]25  ) (
26  St_seq (
[966]27    St_assign (ASTptr Any) id_main_q (Op2 (ASTptr Any) (ASTint I32 Unsigned) (ASTptr Any) Oaddp (Cst (ASTptr Any) (Oaddrstack 0)) (Cst (ASTint I32 Unsigned) (Ointconst I32 (repr ? 0))))
[898]28  ) (
29  St_seq (
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)) (
31      St_cost C_cost2 (
[1633]32      St_return (Some ? (mk_DPair ?? (ASTint I32 Signed) (Op1 (ASTint I8 Signed) (ASTint I32 Signed) (Ocastint ????) (Cst (ASTint I8 Signed) (Ointconst I8 (repr ? 0))))))
[898]33      )
34    ) (
35      St_cost C_cost3 (
36      St_skip      )
37    )
38  ) (
39  St_seq (
[966]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)))) (
[898]41      St_cost C_cost0 (
[1633]42      St_return (Some ? (mk_DPair ?? (ASTint I32 Signed) (Op1 (ASTint I8 Signed) (ASTint I32 Signed) (Ocastint ????) (Cst (ASTint I8 Signed) (Ointconst I8 (repr ? 0))))))
[898]43      )
44    ) (
45      St_cost C_cost1 (
46      St_skip      )
47    )
48  ) (
49  St_seq (
[1633]50    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)))))
[898]51  ) (
52  St_seq (
[1633]53    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)))))
[898]54  ) (
55  St_seq (
[1633]56    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)))))
[898]57  ) (
[1633]58  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)))))))
[898]59  )
60  )
61  )
62  )
63  )
64  )
65  )
66  )
67
[1633]68) (match daemon in False with [ ])).
[898]69
70
71
72definition myprog : Cminor_program :=
[1633]73mk_program ?? [] [
74  (mk_Prod ?? id_main f_main)
[898]75]  id_main
76.
Note: See TracBrowser for help on using the repository browser.