| [898] | 1 | include "Cminor/semantics.ma". |
|---|
| 2 | include "common/Animation.ma". |
|---|
| 3 | |
|---|
| 4 | |
|---|
| 5 | |
|---|
| 6 | definition id_main := ident_of_nat 0. |
|---|
| 7 | definition id_main_p := ident_of_nat 6. |
|---|
| 8 | definition id_main_q := ident_of_nat 7. |
|---|
| 9 | definition C_cost4 := costlabel_of_nat 5. |
|---|
| 10 | definition C_cost2 := costlabel_of_nat 4. |
|---|
| 11 | definition C_cost3 := costlabel_of_nat 3. |
|---|
| 12 | definition C_cost0 := costlabel_of_nat 2. |
|---|
| 13 | definition C_cost1 := costlabel_of_nat 1. |
|---|
| 14 | definition f_main := Internal ? (mk_internal_function |
|---|
| 15 | (Some ? (ASTint I32 Signed)) |
|---|
| 16 | [] |
|---|
| 17 | [pair ?? id_main_p (ASTptr Any); pair ?? id_main_q (ASTptr Any)] |
|---|
| 18 | 4 ( |
|---|
| 19 | St_cost C_cost4 ( |
|---|
| 20 | St_seq ( |
|---|
| 21 | St_assign (ASTptr Any) id_main_p (Op1 (ASTint I8 Signed) (ASTptr Any) (Optrofint Any) (Cst (ASTint I8 Signed) (Ointconst (repr 0)))) |
|---|
| 22 | ) ( |
|---|
| 23 | St_seq ( |
|---|
| 24 | St_assign (ASTptr Any) id_main_q (Op2 (ASTptr Any) (ASTint I32 Unsigned) (ASTptr Any) Oaddp (Cst (ASTptr Any) (Oaddrstack (repr 0))) (Cst (ASTint I32 Unsigned) (Ointconst (repr 0)))) |
|---|
| 25 | ) ( |
|---|
| 26 | St_seq ( |
|---|
| 27 | 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)) ( |
|---|
| 28 | St_cost C_cost2 ( |
|---|
| 29 | St_return (Some ? (dp ?? (ASTint I32 Signed) (Op1 (ASTint I8 Signed) (ASTint I32 Signed) Ocast8signed (Cst (ASTint I8 Signed) (Ointconst (repr 0)))))) |
|---|
| 30 | ) |
|---|
| 31 | ) ( |
|---|
| 32 | St_cost C_cost3 ( |
|---|
| 33 | St_skip ) |
|---|
| 34 | ) |
|---|
| 35 | ) ( |
|---|
| 36 | St_seq ( |
|---|
| 37 | 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 (Id (ASTptr Any) id_main_p) (Id (ASTptr Any) id_main_p)) (Cst (ASTint I32 Signed) (Ointconst (repr 0)))) ( |
|---|
| 38 | St_cost C_cost0 ( |
|---|
| 39 | St_return (Some ? (dp ?? (ASTint I32 Signed) (Op1 (ASTint I8 Signed) (ASTint I32 Signed) Ocast8signed (Cst (ASTint I8 Signed) (Ointconst (repr 0)))))) |
|---|
| 40 | ) |
|---|
| 41 | ) ( |
|---|
| 42 | St_cost C_cost1 ( |
|---|
| 43 | St_skip ) |
|---|
| 44 | ) |
|---|
| 45 | ) ( |
|---|
| 46 | St_seq ( |
|---|
| 47 | 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 (repr 0))) (Cst (ASTint I8 Signed) (Ointconst (repr 1))))) |
|---|
| 48 | ) ( |
|---|
| 49 | St_seq ( |
|---|
| 50 | 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 (repr 0))) (Cst (ASTint I8 Signed) (Ointconst (repr 1))))) |
|---|
| 51 | ) ( |
|---|
| 52 | St_seq ( |
|---|
| 53 | 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 (repr 0))) (Cst (ASTint I8 Signed) (Ointconst (repr 1))))) |
|---|
| 54 | ) ( |
|---|
| 55 | 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 (repr 0))))))) |
|---|
| 56 | ) |
|---|
| 57 | ) |
|---|
| 58 | ) |
|---|
| 59 | ) |
|---|
| 60 | ) |
|---|
| 61 | ) |
|---|
| 62 | ) |
|---|
| 63 | ) |
|---|
| 64 | |
|---|
| 65 | )). |
|---|
| 66 | |
|---|
| 67 | |
|---|
| 68 | |
|---|
| 69 | definition myprog : Cminor_program := |
|---|
| 70 | mk_program ?? [ |
|---|
| 71 | (pair ?? id_main f_main) |
|---|
| 72 | ] id_main |
|---|
| 73 | [] |
|---|
| 74 | . |
|---|
| 75 | |
|---|
| 76 | example exec: finishes_with (repr 1) ? (exec_up_to Cminor_fullexec myprog 1000 [ ]). |
|---|
| 77 | normalize (* you can examine the result here *) |
|---|
| 78 | @refl |
|---|
| 79 | qed. |
|---|
| 80 | |
|---|
| 81 | include "Cminor/toRTLabs.ma". |
|---|
| 82 | include "RTLabs/semantics.ma". |
|---|
| 83 | |
|---|
| 84 | example execRTL: finishes_with (repr 1) ? (do myprog' ← cminor_init_to_rtlabs myprog; exec_up_to RTLabs_fullexec myprog' 1000 [ ]). |
|---|
| 85 | normalize (* you can examine the result here *) |
|---|
| 86 | @refl |
|---|
| 87 | qed. |
|---|
