include "Cexec.ma".

(* Functions to allow programs to be executed up to some number of steps, given
   a predetermined set of input values.  Note that we throw away the state if
   we stop at a continuation - it can be too large to work with. *)

definition get_input : ∀o:io_out. eventval → res (io_in o) ≝
λo,ev.
match io_in_typ o return λt. res (eventval_type t) with
[ ASTint ⇒ match ev with [ EVint i ⇒ OK ? i | _ ⇒ Error ? ]
| ASTfloat ⇒ match ev with [ EVfloat f ⇒ OK ? f | _ ⇒ Error ? ]
].

let rec up_to_nth_step (n:nat) (input:list eventval) (e:execution state io_out io_in) (t:trace) : res (trace × state) ≝
match n with
[ O ⇒ match e with [ e_step tr s _ ⇒ OK ? 〈t⧺tr, s〉
                   | e_stop tr r m ⇒ OK ? 〈t⧺tr, Returnstate (Vint r) Kstop m〉
                   | _ ⇒ Error ? ]
| S m ⇒ match e with [ e_step tr s e' ⇒ up_to_nth_step m input e' (t⧺tr)
                     | e_stop tr r m ⇒ OK ? 〈t⧺tr, Returnstate (Vint r) Kstop m〉
                     | e_interact o k ⇒ 
                         match input with
                         [ nil ⇒ Error ?
                         | cons h tl ⇒ do i ← get_input o h;
                                       up_to_nth_step m tl (k i) t
                         ]
                     | e_wrong ⇒ Error ?
                     ]
].

definition exec_up_to : clight_program → nat → list eventval → res (trace × state) ≝
λp,n,i. up_to_nth_step n i (exec_inf p) E0.

(* Provide an easy way to get a term in proof mode for reduction.
   For example,
   
   example exec: result ? (exec_up_to myprog 20 [EVint (repr 12)]).
   normalize  (* you can examine the result here *)
   % qed.
   
 *)

inductive result (A:Type[0]) : A → Type[0] ≝
| witness : ∀a:A. result A a.

(* Hide the representation of memory to make displaying the results easier. *)

notation < "'MEM'" with precedence 1 for @{ 'mem }.
interpretation "hide memory" 'mem = (mk_mem ???).