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 : nat → Type[0] ≝
| Kstop : cont O
| Kseq : ∀n. stmt n → cont n → cont n
| Kblock : ∀n. cont n → cont (S n)
| Kcall : option ident → internal_function → block (* sp *) → env → ∀n. cont n → cont O.

inductive state : Type[0] ≝
| State:
    ∀    f: internal_function.
    ∀    n: nat.
    ∀    s: stmt n.
    ∀   en: env.
    ∀    m: mem.
    ∀   sp: block.
    ∀    k: cont n.
            state
| Callstate:
    ∀   fd: fundef internal_function.
    ∀ args: list val.
    ∀    m: mem.
    ∀    k: cont O.
            state
| Returnstate:
    ∀    v: option val.
    ∀    m: mem.
    ∀    k: cont O.
            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) (m:Fin n) (k:cont n) on k : Sig nat cont ≝
(match k return λx.λ_.Fin x → Sig nat cont with
[ Kstop ⇒ λm.?
| Kseq n' _ k' ⇒ λm. k_exit ? m k'
| Kblock n' k' ⇒ λm.match m return λx.λ_.match x with [ O ⇒ True | S y ⇒ (Fin y → Sig nat cont) → Sig nat cont ] with [ FO _ ⇒ λ_.dp ??? k' | FS n' m' ⇒ λr.r m' ] (λm'. k_exit ? m' k')
| Kcall _ _ _ _ _ _ ⇒ λm.?
]) m.
@(match m return λx.λ_.match x return λ_.Type[0] with [ O ⇒ Sig nat cont | S _ ⇒ True] with [ FO x ⇒ I | FS x y ⇒ I ])
qed. 


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 (n:nat) (k:cont n) on k : cont O ≝
match k return λ_.λ_.cont O with
[ Kseq _ _ k' ⇒ call_cont ? k'
| Kblock _ k' ⇒ call_cont ? k'
| Kstop ⇒ Kstop
| Kcall a b c d e f ⇒ Kcall a b c d e f
].

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

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 n0 s en m sp k ⇒
    (match s return λx.λ_. cont x → IO io_out io_in (trace × state) with
    [ St_skip n ⇒ λk.
        match k with
        [ Kstop ⇒ Wrong ???
        | Kseq n' s' k' ⇒ ret ? 〈E0, State f n' s' en m sp k'〉
        | Kblock n' k' ⇒ ret ? 〈E0, State f n' (St_skip ?) en m sp k'〉
          (* cminor allows functions without an explicit return statement *)
        | Kcall a b c d e f ⇒ ret ? 〈E0, Returnstate (None ?) (free m sp) (Kcall a b c d e f)〉
        ]
    | St_assign id e n ⇒ λk.
        ! 〈tr,v〉 ← eval_expr ge e en sp m;
        ! en' ← update ?? en id v;
        ret ? 〈tr, State f n (St_skip ?) en' m sp k〉
    | St_store chunk edst e n ⇒ λk.
        ! 〈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 n (St_skip ?) en m' sp k〉

    | St_call dst ef args sig n ⇒ λk. (* 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 n k)〉
    | St_tailcall ef args sig n ⇒ λk.
        ! 〈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 n s1 s2 ⇒ λk. ret ? 〈E0, State f n s1 en m sp (Kseq ? s2 k)〉
    | St_ifthenelse e n strue sfalse ⇒ λk.
        ! 〈tr,v〉 ← eval_expr ge e en sp m;
        ! b ← eval_bool_of_val v;
        ret ? 〈tr, State f n (if b then strue else sfalse) en m sp k〉
    | St_loop n s ⇒ λk. ret ? 〈E0, State f n s en m sp (Kseq ? (St_loop ? s) k)〉
    | St_block n s ⇒ λk. ret ? 〈E0, State f ? s en m sp (Kblock ? k)〉
    | St_exit n x ⇒ λk.
        match k_exit n x k with
        [ dp n' k' ⇒
            ret ? 〈E0, State f ? (St_skip ?) en m sp k'〉
        ]
    | St_switch e n cs default ⇒ λk.
        ! 〈tr,v〉 ← eval_expr ge e en sp m;
        match v with
        [ Vint i ⇒
            match k_exit ? (find_case ? i cs default) k with
            [ dp n k' ⇒ 
                ret ? 〈tr, State f n (St_skip ?) en m sp k'〉
            ]
        | _ ⇒ Wrong ???
        ]
    | St_return eo n ⇒ λk.
        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 n s' ⇒ λk. ret ? 〈E0, State f ? s' en m sp k〉
    | St_goto l n ⇒ λk.
        ! x ← opt_to_res … (find_label l ? (f_body f) (call_cont ? k));
        match x with [ dp n' x' ⇒ let 〈s', k'〉 ≝ x' in
          ret ? 〈E0, State f ? s' en m sp k'〉
        ]
    | St_cost l n s' ⇒ λk.
        ret ? 〈Echarge l, State f n s' en m sp k〉
    ]) 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 O (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 n 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 n (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.