source: src/Cminor/test/factorial.Cminor.ma @ 1680

Last change on this file since 1680 was 1633, checked in by campbell, 8 years ago

Update Cminor pretty printer and examples.

File size: 2.9 KB
Line 
1include "Cminor/semantics.ma".
2include "common/Animation.ma".
3
4definition label_of_nat : nat -> identifier Label := identifier_of_nat ?.
5
6
7
8definition id_get_input := ident_of_nat 0.
9definition f_get_input := External internal_function (mk_external_function id_get_input (mk_signature [] (Some ? (ASTint I32 Signed)))).
10definition id_main := ident_of_nat 1.
11definition id_main_i := ident_of_nat 7.
12definition id_main_j := ident_of_nat 8.
13definition id_main_r := ident_of_nat 9.
14definition id_main__tmp0 := ident_of_nat 10.
15definition C_cost2 := costlabel_of_nat 6.
16definition L_tmp1 := label_of_nat 5.
17definition C_cost0 := costlabel_of_nat 4.
18definition L_tmp2 := label_of_nat 3.
19definition C_cost1 := costlabel_of_nat 2.
20definition f_main := Internal ? (mk_internal_function
21  (Some ? (ASTint I32 Signed))
22  []
23  [mk_Prod ?? id_main_i (ASTint I32 Signed); mk_Prod ?? id_main_j (ASTint I32 Signed); mk_Prod ?? id_main_r (ASTint I32 Signed); mk_Prod ?? id_main__tmp0 (ASTint I32 Signed)]
24  (match daemon in False with [ ])
250 (
26  St_cost C_cost2 (
27  St_seq (
28    St_seq (
29      St_call (Some ? (mk_Prod ?? id_main__tmp0 (ASTint I32 Signed))) (Cst ? (Oaddrsymbol id_get_input 0)) []
30    ) (
31    St_assign (ASTint I32 Signed) id_main_i (Id (ASTint I32 Signed) id_main__tmp0)
32    )
33  ) (
34  St_seq (
35    St_assign (ASTint I32 Signed) id_main_r (Op1 (ASTint I8 Signed) (ASTint I32 Signed) (Ocastint ????) (Cst (ASTint I8 Signed) (Ointconst I8 (repr ? 1))))
36  ) (
37  St_seq (
38    St_seq (
39      St_seq (
40        St_assign (ASTint I32 Signed) id_main_j (Op1 (ASTint I8 Signed) (ASTint I32 Signed) (Ocastint ????) (Cst (ASTint I8 Signed) (Ointconst I8 (repr ? 2))))
41      ) (
42      St_seq (
43        St_label L_tmp1 (
44        St_seq (
45          St_ifthenelse I32 Signed (Op2 (ASTint I32 Signed) (ASTint I32 Signed) (ASTint I32 Signed) (Ocmp Cle) (Id (ASTint I32 Signed) id_main_j) (Id (ASTint I32 Signed) id_main_i)) (
46            St_skip          ) (
47            St_goto L_tmp2
48          )
49        ) (
50        St_seq (
51          St_seq (
52            St_cost C_cost0 (
53            St_assign (ASTint I32 Signed) id_main_r (Op2 (ASTint I32 Signed) (ASTint I32 Signed) (ASTint I32 Signed) Omul (Id (ASTint I32 Signed) id_main_r) (Id (ASTint I32 Signed) id_main_j))
54            )
55          ) (
56          St_assign (ASTint I32 Signed) id_main_j (Op2 (ASTint I32 Signed) (ASTint I32 Signed) (ASTint I32 Signed) Oadd (Id (ASTint I32 Signed) id_main_j) (Cst (ASTint I32 Signed) (Ointconst I32 (repr ? 1))))
57          )
58        ) (
59        St_goto L_tmp1
60        )
61        )
62        )
63      ) (
64      St_label L_tmp2 (
65      St_skip      )
66      )
67      )
68    ) (
69    St_cost C_cost1 (
70    St_skip    )
71    )
72  ) (
73  St_return (Some ? (mk_DPair ?? (ASTint I32 Signed) (Id (ASTint I32 Signed) id_main_r)))
74  )
75  )
76  )
77  )
78
79) (match daemon in False with [ ])).
80
81
82
83definition myprog : Cminor_program :=
84mk_program ?? [] [
85  (mk_Prod ?? id_get_input f_get_input);
86  (mk_Prod ?? id_main f_main)
87]  id_main
88.
Note: See TracBrowser for help on using the repository browser.