include "Csyntax.ma".
include "Csem.ma".
include "Cexec.ma".

ndefinition main : ident ≝ O.
naxiom ident_eq_eq: ∀i. ident_eq i i = inl ?? (refl ? i).

ndefinition trivial : program.
@ [ 〈main, Internal ?〉 ] main [];
@ (Tint I32 Signed) [ ] [ ] (Sreturn (Some ??));
@ ? (Tint I32 Signed); napply (Econst_int zero);
nqed.

nremark trivial_behaves : ∃behaviour. exec_program trivial behaviour.
@; ##[ ##2:
  napply program_terminates; 
  ##[ ##5: @; (* initial state *)
    ##[ ##3: nnormalize; nrewrite > (ident_eq_eq ?); //;
    ##| ##4: nnormalize; //;
    ##| ##*: ##skip
    ##] 
  ##| ##6:
    @2; ##[ ##4: napply step_internal_function;
          ##[ ##4: napply alloc_variables_nil; ##| ##5: napply bind_parameters_nil; ##| ##*: ##skip ##] 
        ##| ##5: @2;
          ##[ ##4: napply step_return_1; //; napply nmk; #H; ndestruct;
          ##| ##5: @1; 
          ##| ##6: //;
          ##| ##*: ##skip ##]
        ##| ##6: //;
        ##| ##*: ##skip
        ##]
  ##| ##7: @;
  ##]
##] nqed.

nlemma nab : ∀A,P,e,v. e = OK (Σv:A.P v) v → ∃v:A. P v.
#A P e v; ncases v; /2/; nqed.

nremark trivial_init : ∃s. initial_state trivial s.
napply (nab ?? (make_initial_state trivial) ? (refl ??));
nqed.

nremark hacktonormalize : True.
nletin s ≝ (err_eject ?? (make_initial_state trivial)).
nnormalize in s.
//; nqed.

nremark trivial_executes : True.
nletin ts ≝ (s ← make_initial_state trivial;:
             exec_steps 10 (globalenv Genv ?? trivial) s);
nnormalize in ts;
//; nqed.