include "common/Events.ma".
include "common/Mem.ma".
include "common/IO.ma".
include "common/Globalenvs.ma".
include "common/SmallstepExec.ma".

include "Cminor/syntax.ma".

definition env ≝ identifier_map SymbolTag val.
definition genv ≝ (genv_t Genv) (fundef internal_function).

inductive cont : Type[0] ≝
| Kstop : cont
| Kseq : stmt → cont → cont
| Kblock : cont → cont
| Kcall : option ident → internal_function → block (* sp *) → env → cont → cont.

inductive state : Type[0] ≝
| State:
    ∀    f: internal_function.
    ∀    s: stmt.
    ∀   en: env.
    ∀    m: mem.
    ∀   sp: block.
    ∀    k: cont.
            state
| Callstate:
    ∀   fd: fundef internal_function.
    ∀ args: list val.
    ∀    m: mem.
    ∀    k: cont.
            state
| Returnstate:
    ∀    v: option val.
    ∀    m: mem.
    ∀    k: cont.
            state.

definition mem_of_state : state → mem ≝
λst. match st with
[ State _ _ _ m _ _ ⇒ m
| Callstate _ _ m _ ⇒ m
| Returnstate _ m _ ⇒ m
].

axiom UnknownLocal : String.
axiom FailedConstant : String.
axiom FailedOp : String.
axiom FailedLoad : String.

let rec eval_expr (ge:genv) (ty0:typ) (e:expr ty0) (en:env) (sp:block) (m:mem) on e : res (trace × val) ≝
match e with
[ Id _ i ⇒
    do r ← opt_to_res … [MSG UnknownLocal; CTX ? i] (lookup ?? en i);
    OK ? 〈E0, r〉
| Cst _ c ⇒
    do r ← opt_to_res … (msg FailedConstant) (eval_constant (find_symbol … ge) sp c);
    OK ? 〈E0, r〉
| Op1 ty ty' op e' ⇒
    do 〈tr,v〉 ← eval_expr ge ? e' en sp m;
    do r ← opt_to_res … (msg FailedOp) (eval_unop op v);
    OK ? 〈tr, r〉
| Op2 ty1 ty2 ty' op e1 e2 ⇒
    do 〈tr1,v1〉 ← eval_expr ge ? e1 en sp m;
    do 〈tr2,v2〉 ← eval_expr ge ? e2 en sp m;
    do r ← opt_to_res … (msg FailedOp) (eval_binop op v1 v2);
    OK ? 〈tr1 ⧺ tr2, r〉
| Mem rg ty chunk e ⇒
    do 〈tr,v〉 ← eval_expr ge ? e en sp m;
    do r ← opt_to_res … (msg FailedLoad) (loadv chunk m v);
    OK ? 〈tr, r〉
| Cond sz sg ty e' e1 e2 ⇒
    do 〈tr,v〉 ← eval_expr ge ? e' en sp m;
    do b ← eval_bool_of_val v;
    do 〈tr',r〉 ← eval_expr ge ? (if b then e1 else e2) en sp m;
    OK ? 〈tr ⧺ tr', r〉
| Ecost ty l e' ⇒
    do 〈tr,r〉 ← eval_expr ge ty e' en sp m;
    OK ? 〈Echarge l ⧺ tr, r〉
].

axiom BadState : String.

let rec k_exit (n:nat) (k:cont) on k : res cont ≝
match k with
[ Kstop ⇒ Error ? (msg BadState)
| Kseq _ k' ⇒ k_exit n k'
| Kblock k' ⇒ match n with [ O ⇒ OK ? k' | S m ⇒ k_exit m k' ]
| Kcall _ _ _ _ _ ⇒ Error ? (msg BadState)
].

let rec find_case (A:Type[0]) (sz:intsize) (i:bvint sz) (cs:list (bvint sz × A)) (default:A) on cs : A ≝
match cs with
[ nil ⇒ default
| cons h t ⇒
    let 〈hi,a〉 ≝ h in
    if eq_bv ? i hi then a else find_case A sz i t default
].

let rec call_cont (k:cont) : cont ≝
match k with
[ Kseq _ k' ⇒ call_cont k'
| Kblock k' ⇒ call_cont k'
| _ ⇒ k
].

let rec find_label (l:ident) (s:stmt) (k:cont) on s : option (stmt × cont) ≝
match s with
[ St_seq s1 s2 ⇒
    match find_label l s1 (Kseq s2 k) with
    [ None ⇒ find_label l s2 k
    | Some sk ⇒ Some ? sk
    ]
| St_ifthenelse _ _ _ s1 s2 ⇒
    match find_label l s1 k with
    [ None ⇒ find_label l s2 k
    | Some sk ⇒ Some ? sk
    ]
| St_loop s' ⇒ find_label l s' (Kseq (St_loop s') k)
| St_block s' ⇒ find_label l s' (Kblock k)
| St_label l' s' ⇒ 
    match ident_eq l l' with
    [ inl _ ⇒ Some ? 〈s',k〉
    | inr _ ⇒ find_label l s' k
    ]
| St_cost _ s' ⇒ find_label l s' k
| _ ⇒ None ?
].

axiom WrongNumberOfParameters : String.

(* TODO: perhaps should do a little type checking? *)
let rec bind_params (vs:list val) (ids:list (ident×typ)) : res env ≝
match vs with
[ nil ⇒ match ids with [ nil ⇒ OK ? (empty_map ??) | _ ⇒ Error ? (msg WrongNumberOfParameters) ]
| cons v vt ⇒
    match ids with
    [ nil ⇒ Error ? (msg WrongNumberOfParameters)
    | cons idh idt ⇒
        let 〈id,ty〉 ≝ idh in
        do en ← bind_params vt idt;
        OK ? (add ?? en id v)
    ]
].

(* TODO: perhaps should do a little type checking? *)
definition init_locals : env → list (ident×typ) → env ≝
foldr ?? (λidty,en. add ?? en (\fst idty) Vundef).

axiom FailedStore : String.
axiom BadFunctionValue : String.
axiom BadSwitchValue : String.
axiom UnknownLabel : String.
axiom ReturnMismatch : String.

definition eval_step : genv → state → IO io_out io_in (trace × state) ≝
λge,st.
match st with
[ State f s en m sp k ⇒
    match s with
    [ St_skip ⇒
        match k with
        [ Kstop ⇒ Wrong ??? (msg BadState)
        | Kseq s' k' ⇒ ret ? 〈E0, State f s' en m sp k'〉
        | Kblock k' ⇒ ret ? 〈E0, State f s en m sp k'〉
          (* cminor allows functions without an explicit return statement *)
        | Kcall _ _ _ _ _ ⇒ ret ? 〈E0, Returnstate (None ?) (free m sp) k〉
        ]
    | St_assign _ id e ⇒
        ! 〈tr,v〉 ← eval_expr ge ? e en sp m;
        ! en' ← update ?? en id v;
        ret ? 〈tr, State f St_skip en' m sp k〉
    | St_store _ _ chunk edst e ⇒
        ! 〈tr,vdst〉 ← eval_expr ge ? edst en sp m;
        ! 〈tr',v〉 ← eval_expr ge ? e en sp m;
        ! m' ← opt_to_res … (msg FailedStore) (storev chunk m vdst v);
        ret ? 〈tr ⧺ tr', State f St_skip en m' sp k〉

    | St_call dst ef args ⇒
        ! 〈tr,vf〉 ← eval_expr ge ? ef en sp m;
        ! fd ← opt_to_res … (msg BadFunctionValue) (find_funct ?? ge vf);
        ! 〈tr',vargs〉 ← trace_map … (λe. match e with [ dp ty e ⇒ eval_expr ge ? e en sp m ]) args;
        ret ? 〈tr ⧺ tr', Callstate fd vargs m (Kcall dst f sp en k)〉
    | St_tailcall ef args ⇒
        ! 〈tr,vf〉 ← eval_expr ge ? ef en sp m;
        ! fd ← opt_to_res … (msg BadFunctionValue) (find_funct ?? ge vf);
        ! 〈tr',vargs〉 ← trace_map … (λe. match e with [ dp ty e ⇒ eval_expr ge ? e en sp m ]) args;
        ret ? 〈tr ⧺ tr', Callstate fd vargs (free m sp) (call_cont k)〉
        
    | St_seq s1 s2 ⇒ ret ? 〈E0, State f s1 en m sp (Kseq s2 k)〉
    | St_ifthenelse _ _ e strue sfalse ⇒
        ! 〈tr,v〉 ← eval_expr ge ? e en sp m;
        ! b ← eval_bool_of_val v;
        ret ? 〈tr, State f (if b then strue else sfalse) en m sp k〉
    | St_loop s ⇒ ret ? 〈E0, State f s en m sp (Kseq (St_loop s) k)〉
    | St_block s ⇒ ret ? 〈E0, State f s en m sp (Kblock k)〉
    | St_exit n ⇒
        ! k' ← k_exit n k;
        ret ? 〈E0, State f St_skip en m sp k'〉
    | St_switch sz _ e cs default ⇒
        ! 〈tr,v〉 ← eval_expr ge ? e en sp m;
        match v with
        [ Vint sz' i ⇒ intsize_eq_elim ? sz' sz ? i (λi.
            ! k' ← k_exit (find_case ?? i cs default) k;
            ret ? 〈tr, State f St_skip en m sp k'〉)
            (Wrong ??? (msg BadSwitchValue))
        | _ ⇒ Wrong ??? (msg BadSwitchValue)
        ]
    | St_return eo ⇒
        match eo with
        [ None ⇒ ret ? 〈E0, Returnstate (None ?) (free m sp) (call_cont k)〉
        | Some e ⇒
            match e with [ dp ty e ⇒
              ! 〈tr,v〉 ← eval_expr ge ? e en sp m;
              ret ? 〈tr, Returnstate (Some ? v) (free m sp) (call_cont k)〉
            ]
        ]
    | St_label l s' ⇒ ret ? 〈E0, State f s' en m sp k〉
    | St_goto l ⇒
        ! 〈s', k'〉 ← opt_to_res … [MSG UnknownLabel; CTX ? l] (find_label l (f_body f) (call_cont k));
        ret ? 〈E0, State f s' en m sp k'〉
    | St_cost l s' ⇒
        ret ? 〈Echarge l, State f s' en m sp k〉
    ]
| Callstate fd args m k ⇒
    match fd with
    [ Internal f ⇒
        let 〈m',sp〉 ≝ alloc m 0 (f_stacksize f) Any in
        ! en ← bind_params args (f_params f);
        ret ? 〈E0, State f (f_body f) (init_locals en (f_vars f)) m' sp k〉
    | External fn ⇒
        ! evargs ← check_eventval_list args (sig_args (ef_sig fn));
        ! evres ← do_io (ef_id fn) evargs (proj_sig_res (ef_sig fn));
        let res ≝ match (sig_res (ef_sig fn)) with [ None ⇒ None ? | Some _ ⇒ Some ? (mk_val ? evres) ] in
        ret ? 〈Eextcall (ef_id fn) evargs (mk_eventval ? evres), Returnstate res m k〉
    ]
| Returnstate res m k ⇒
    match k with
    [ Kcall dst f sp en k' ⇒
        ! en' ← match res with
                [ None ⇒ match dst with [ None ⇒ OK ? en | Some _ ⇒ Error ? (msg ReturnMismatch)]
                | Some v ⇒ match dst with [ None ⇒ Error ? (msg ReturnMismatch)
                                          | Some id ⇒ update ?? en id v ]
                ];
        ret ? 〈E0, State f St_skip en' m sp k'〉
    | _ ⇒ Wrong ??? (msg BadState)
    ]
].

definition is_final : state → option int ≝
λs. match s with
[ Returnstate res m k ⇒
    match k with
    [ Kstop ⇒
        match res with
        [ None ⇒ None ?
        | Some v ⇒
            match v with
            [ Vint sz i ⇒ intsize_eq_elim ? sz I32 ? i (λi. Some ? i) (None ?)
            | _ ⇒ None ?
            ]
        ]
    | _ ⇒ None ?
    ]
| _ ⇒ None ?
].

definition Cminor_exec : execstep io_out io_in ≝
  mk_execstep … ? is_final mem_of_state eval_step.

axiom MainMissing : String.

definition make_initial_state : Cminor_program → res (genv × state) ≝
λp.
  do ge ← globalenv Genv ?? p;
  do m ← init_mem Genv ?? p;
  do b ← opt_to_res ? (msg MainMissing) (find_symbol ? ? ge (prog_main ?? p));
  do f ← opt_to_res ? (msg MainMissing) (find_funct_ptr ? ? ge b);
  OK ? 〈ge, Callstate f (nil ?) m Kstop〉.

definition Cminor_fullexec : fullexec io_out io_in ≝
  mk_fullexec … Cminor_exec ? make_initial_state.