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

Last change on this file since 762 was 751, checked in by campbell, 10 years ago

Initial version of the Cminor syntax and semantics.

File size: 2.0 KB
Line 
1include "Cminor/semantics.ma".
2include "common/Animation.ma".
3
4definition id_get_input := ident_of_nat 0.
5definition f_get_input := External internal_function (mk_external_function id_get_input (mk_signature [] (Some ? ASTint))).
6definition id_main := ident_of_nat 1.
7definition id_main_tmp0 := ident_of_nat 5.
8definition id_main_r := ident_of_nat 6.
9definition id_main_j := ident_of_nat 7.
10definition id_main_i := ident_of_nat 8.
11definition C_cost2 := costlabel_of_nat 4.
12definition C_cost0 := costlabel_of_nat 3.
13definition C_cost1 := costlabel_of_nat 2.
14definition f_main := Internal ? (mk_internal_function
15  (mk_signature [] (Some ? ASTint))
16  []
17  [id_main_tmp0; id_main_r; id_main_j; id_main_i]
18  []
19  0 (
20  St_cost C_cost2 (
21  St_seq (
22    St_call (Some ? id_main_i) (Cst (Oaddrsymbol id_get_input (repr 0))) [] (mk_signature [] (Some ? ASTint))
23  ) (
24  St_seq (
25    St_assign id_main_r (Cst (Ointconst (repr 1)))
26  ) (
27  St_seq (
28    St_seq (
29      St_seq (
30        St_assign id_main_j (Cst (Ointconst (repr 2)))
31      ) (
32      St_block (
33        St_loop (
34          St_seq (
35            St_ifthenelse (Op1 Onotbool (Op2 (Ocmp Cle) (Id id_main_j) (Id id_main_i))) (
36              St_exit 0
37            ) (
38              St_skip            )
39          ) (
40          St_seq (
41            St_block (
42              St_cost C_cost0 (
43              St_assign id_main_r (Op2 Omul (Id id_main_r) (Id id_main_j))
44              )
45            )
46          ) (
47          St_assign id_main_j (Op2 Oadd (Id id_main_j) (Cst (Ointconst (repr 1))))
48          )
49          )
50        )
51      )
52      )
53    ) (
54    St_cost C_cost1 (
55    St_skip    )
56    )
57  ) (
58  St_return (Some ? (Id id_main_r))
59  )
60  )
61  )
62  )
63
64)).
65
66
67
68definition myprog : Cminor_program :=
69mk_program ?? [
70  (pair ?? id_get_input f_get_input);
71  (pair ?? id_main f_main)
72]  id_main
73[]
74.
75
76example exec: finishes_with (repr 120) ? (exec_up_to Cminor_fullexec myprog 100 [EVint (repr 5)]).
77normalize  (* you can examine the result here *)
78@refl qed.
Note: See TracBrowser for help on using the repository browser.