include "Cminor/semantics.ma".
include "common/Animation.ma".

definition id_get_input := ident_of_nat 0.
definition f_get_input := External internal_function (mk_external_function id_get_input (mk_signature [] (Some ? (ASTint I32 Signed)))).
definition id_main := ident_of_nat 1.
definition id_main_tmp0 := ident_of_nat 5.
definition id_main_r := ident_of_nat 6.
definition id_main_j := ident_of_nat 7.
definition id_main_i := ident_of_nat 8.
definition C_cost2 := costlabel_of_nat 4.
definition C_cost0 := costlabel_of_nat 3.
definition C_cost1 := costlabel_of_nat 2.
definition f_main := Internal ? (mk_internal_function
  (mk_signature [] (Some ? (ASTint I32 Signed)))
  []
  [id_main_tmp0; id_main_r; id_main_j; id_main_i]
  []
  0 (
  St_cost C_cost2 (
  St_seq (
    St_call (Some ? id_main_i) (Cst (Oaddrsymbol id_get_input (repr 0))) []
  ) (
  St_seq (
    St_assign id_main_r (Cst (Ointconst (repr 1)))
  ) (
  St_seq (
    St_seq (
      St_seq (
        St_assign id_main_j (Cst (Ointconst (repr 2)))
      ) (
      St_block (
        St_loop (
          St_seq (
            St_ifthenelse (Op1 Onotbool (Op2 (Ocmp Cle) (Id id_main_j) (Id id_main_i))) (
              St_exit 0
            ) (
              St_skip            )
          ) (
          St_seq (
            St_block (
              St_cost C_cost0 (
              St_assign id_main_r (Op2 Omul (Id id_main_r) (Id id_main_j))
              )
            )
          ) (
          St_assign id_main_j (Op2 Oadd (Id id_main_j) (Cst (Ointconst (repr 1))))
          )
          )
        )
      )
      )
    ) (
    St_cost C_cost1 (
    St_skip    )
    )
  ) (
  St_return (Some ? (Id id_main_r))
  )
  )
  )
  )

)).



definition myprog : Cminor_program :=
mk_program ?? [
  (pair ?? id_get_input f_get_input);
  (pair ?? id_main f_main)
]  id_main
[]
.

example exec: finishes_with (repr 120) ? (exec_up_to Cminor_fullexec myprog 100 [EVint (repr 5)]).
normalize  (* you can examine the result here *)
@refl qed.

include "Cminor/toRTLabs.ma".
include "RTLabs/semantics.ma".

example execRTL: finishes_with (repr 120) ? (do myprog' ← cminor_init_to_rtlabs myprog; exec_up_to RTLabs_fullexec myprog' 1000 [EVint (repr 5)]).
normalize  (* you can examine the result here *)
@refl
qed.