include "common/IOMonad.ma".
include "common/Events.ma".

(* Checking types of values given to / received from an external function call. *)

definition eventval_type : ∀ty:typ. Type[0] ≝
λty. match ty with [ ASTint sz _ ⇒ bvint sz | ASTptr ⇒ False | ASTfloat _ ⇒ float ].

definition mk_eventval: ∀ty:typ. eventval_type ty → eventval ≝
λty:typ. match ty return λty'.eventval_type ty' → eventval with [ ASTint sz sg ⇒ λv.EVint sz v | ASTptr ⇒ ? | ASTfloat _ ⇒ λv.EVfloat v ].
*; qed.

definition mk_val: ∀ty:typ. eventval_type ty → val ≝
λty:typ. match ty return λty'.eventval_type ty' → val with [ ASTint sz _ ⇒ λv.Vint sz v | ASTptr ⇒ ? | ASTfloat _ ⇒ λv.Vfloat v ].
*; qed.

lemma mk_val_correct: ∀ty:typ. ∀v:eventval_type ty.
  eventval_match (mk_eventval ty v) ty (mk_val ty v).
#ty cases ty; normalize; // * *; qed.

axiom IllTypedEvent : String.

definition convert_eventval : ∀ev:eventval. ∀ty:typ. res val ≝
λev,ty.
match ty with
[ ASTint sz _ ⇒ match ev with
  [ EVint sz' i ⇒ if eq_intsize sz sz' then OK ? (Vint sz' i) else Error ? (msg IllTypedEvent)
  | _ ⇒ Error ? (msg IllTypedEvent)]
| ASTfloat _ ⇒ match ev with [ EVfloat f ⇒ OK ? (Vfloat f) | _ ⇒ Error ? (msg IllTypedEvent)]
| _ ⇒ Error ? (msg IllTypedEvent)
].

definition check_eventval' : ∀v:val. ∀ty:typ. res eventval ≝
λv,ty.
match ty with
[ ASTint sz _ ⇒ match v with
  [ Vint sz' i ⇒ if eq_intsize sz sz' then OK ? (EVint sz' i) else Error ? (msg IllTypedEvent)
  | _ ⇒ Error ? (msg IllTypedEvent) ]
| ASTfloat _ ⇒ match v with [ Vfloat f ⇒ OK ? (EVfloat f) | _ ⇒ Error ? (msg IllTypedEvent) ]
| _ ⇒ Error ? (msg IllTypedEvent)
].

let rec check_eventval_list (vs: list val) (tys: list typ) : res (list eventval) ≝
match vs with
[ nil ⇒ match tys with [ nil ⇒ OK ? (nil ?) | _ ⇒ Error ? (msg IllTypedEvent) ]
| cons v vt ⇒
  match tys with
  [ nil ⇒ Error ? (msg IllTypedEvent)
  | cons ty tyt ⇒
    do ev ← check_eventval' v ty;
    do evt ← check_eventval_list vt tyt;
    OK ? (ev::evt)
  ]
].

(* IO monad *)

(* Interactions are function calls that return a value and do not change
   the rest of the Clight program's state. *)
record io_out : Type[0] ≝
{ io_function: ident
; io_args: list eventval
; io_in_typ: typ
}.

definition io_in ≝ λo. eventval_type (io_in_typ o).

definition do_io : ident → list eventval → ∀t:typ. IO io_out io_in (eventval_type t) ≝
λfn,args,t. Interact ??? (mk_io_out fn args t) (λres. Value ??? res).

definition ret: ∀T. T → (IO io_out io_in T) ≝
λT,x.(Value ?? T x).