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
].

let rec eval_expr (ge:genv) (e:expr) (en:env) (sp:block) (m:mem) on e : res (trace × val) ≝
match e with
[ Id i ⇒
    do r ← opt_to_res … (lookup ?? en i);
    OK ? 〈E0, r〉
| Cst c ⇒
    do r ← opt_to_res … (eval_constant (find_symbol … ge) sp c);
    OK ? 〈E0, r〉
| Op1 op e' ⇒
    do 〈tr,v〉 ← eval_expr ge e' en sp m;
    do r ← opt_to_res … (eval_unop op v);
    OK ? 〈tr, r〉
| Op2 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 … (eval_binop op v1 v2);
    OK ? 〈tr1 ⧺ tr2, r〉
| Mem chunk e ⇒
    do 〈tr,v〉 ← eval_expr ge e en sp m;
    do r ← opt_to_res … (loadv chunk m v);
    OK ? 〈tr, r〉
| Cond 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 l e' ⇒
    do 〈tr,r〉 ← eval_expr ge e' en sp m;
    OK ? 〈Echarge l ⧺ tr, r〉
].

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

let rec find_case (A:Type[0]) (i:int) (cs:list (int × A)) (default:A) on cs : A ≝
match cs with
[ nil ⇒ default
| cons h t ⇒
    let 〈hi,a〉 ≝ h in
    if eq i hi then a else find_case A 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 ?
].

let rec bind_params (vs:list val) (ids:list ident) : res env ≝
match vs with
[ nil ⇒ match ids with [ nil ⇒ OK ? (empty_map ??) | _ ⇒ Error ? ]
| cons v vt ⇒
    match ids with
    [ nil ⇒ Error ?
    | cons id idt ⇒
        do en ← bind_params vt idt;
        OK ? (add ?? en id v)
    ]
].

definition init_locals : env → list ident → env ≝
foldr ?? (λid,en. add ?? en id Vundef).

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 ???
        | 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 … (storev chunk m vdst v);
        ret ? 〈tr ⧺ tr', State f St_skip en m' sp k〉

    | St_call dst ef args sig ⇒ (* XXX sig unused? *)
        ! 〈tr,vf〉 ← eval_expr ge ef en sp m;
        ! fd ← opt_to_res … (find_funct ?? ge vf);
        ! 〈tr',vargs〉 ← trace_map … (λ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 sig ⇒
        ! 〈tr,vf〉 ← eval_expr ge ef en sp m;
        ! fd ← opt_to_res … (find_funct ?? ge vf);
        ! 〈tr',vargs〉 ← trace_map … (λ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 e cs default ⇒
        ! 〈tr,v〉 ← eval_expr ge e en sp m;
        match v with
        [ Vint i ⇒
            ! k' ← k_exit (find_case ? i cs default) k;
            ret ? 〈tr, State f St_skip en m sp k'〉
        | _ ⇒ Wrong ???
        ]
    | St_return eo ⇒
        match eo with
        [ None ⇒ ret ? 〈E0, Returnstate (None ?) (free m sp) (call_cont k)〉
        | Some 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 … (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 (match (sig_res (ef_sig fn)) with [ None ⇒ ASTint | Some t ⇒ t ]);  (* XXX hack, should allow none *)
        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 ? ]
                | Some v ⇒ match dst with [ None ⇒ Error ?
                                          | Some id ⇒ update ?? en id v ]
                ];
        ret ? 〈E0, State f St_skip en' m sp k'〉
    | _ ⇒ Wrong ???
    ]
].

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 i ⇒ Some ? i
            | _ ⇒ None ?
            ]
        ]
    | _ ⇒ None ?
    ]
| _ ⇒ None ?
].

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

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 ? (find_symbol ? ? ge (prog_main ?? p));
  do f ← opt_to_res ? (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.