include "CexecIO.ma".

ndefinition myprog := mk_program fundef type
  [  mk_pair ?? (succ_pos_of_nat 17) (External (succ_pos_of_nat 17) (Tcons (Tint I32 Signed  ) Tnil) (Tint I32 Signed  ));
  mk_pair ?? (succ_pos_of_nat 19) (Internal (
    mk_function (Tint I32 Signed  ) [] [mk_pair ?? (succ_pos_of_nat 18) (Tint I32 Signed  )]
      (Ssequence
      (Scall (Some ? (Expr (Evar (succ_pos_of_nat 18)) (Tint I32 Signed  )))
        (Expr (Evar (succ_pos_of_nat 17)) (Tfunction (Tcons (Tint I32 Signed  ) Tnil) (Tint I32 Signed  )))
        [(Expr (Econst_int (repr 10)) (Tint I32 Signed  ))])
      (Sreturn (Some ? (Expr (Evar (succ_pos_of_nat 18)) (Tint I32 Signed  )))))
    
    
    
  ))]
  (succ_pos_of_nat 19)
  []
.

(* not useful :(
notation < "maction ('Interact' T f args 'WHATEVER') ('Interact' T f args k)" with precedence 1 for @{ 'interact $T $f $args $k }.
interpretation "interaction" 'interact T f args k = (Interact T f args k).
*)

(* ndefinition works fine for this, whereas nletin during proof seems to blow up. *)
ndefinition ts ≝ (
 ! s0 ← make_initial_state myprog;:
 ! 〈t,s〉 ← exec_steps 7 (globalenv Genv ?? myprog) s0;:
   ret ? 〈t,s〉).

ninductive result (T:Type) : T → Prop ≝
| witness : ∀t:T. result T t.

(* The trick to being able to normalize the term is to avoid looking at the 
   continuations! *)
nremark exec_OK:
    match match ts with [ Interact call k ⇒ k (EVint (repr 6))
                 | Value v ⇒ Wrong ???
                 | Wrong ⇒ Wrong ??? ] with
    [ Interact _ _ ⇒ False
    | Value v ⇒ result ? v
    | Wrong ⇒ False
    ].
nnormalize; //; nqed.