(************************************************************
* Lambda-calculus with references,                          *
* Interpreter in pretty-big-step semantics                  *
*************************************************************)

Set Implicit Arguments.
Require Import LambdaRef.

Implicit Types v : val.
Implicit Types t : trm.
Implicit Types c : ctx.
Implicit Types m : mem.


(************************************************************)
(* * Definitions *)

(** Definition of behaviors *)

Inductive beh :=
  | beh_ret : val -> beh.

Coercion beh_ret : val >-> beh.
Implicit Types b : beh.

(** Outcome of an evaluation *)

Inductive out :=
  | out_ter : mem -> beh -> out
  | out_div : out.

Implicit Types o : out.

(** Grammar of extended terms *)

Inductive ext : Type :=
  | ext_trm : trm -> ext
  | ext_app_1 : out -> trm -> ext
  | ext_app_2 : val -> out -> ext
  | ext_new_1 : out -> ext
  | ext_get_1 : out -> ext
  | ext_set_1 : out -> trm -> ext
  | ext_set_2 : val -> out -> ext.

Coercion ext_trm : trm >-> ext.
Implicit Types e : ext.

(** Generation of fresh names *)

Parameter fresh_for : mem -> loc.
Parameter fresh_for_spec : forall m,
  ~ Heap.indom m (fresh_for m).

(** Semantics (without error rules for the time being) *)

Inductive red : mem -> ctx -> ext -> out -> Prop :=
  | red_val : forall m c v,
      red m c v (out_ter m v)
  | red_var : forall m c x v,
      LibEnv.binds x v c ->
      red m c (trm_var x) (out_ter m v)
  | red_abs : forall m c x t,
      red m c (trm_abs x t) (out_ter m (val_clo c x t))
  | red_app : forall o1 o m c t1 t2,
      red m c t1 o1 -> 
      red m c (ext_app_1 o1 t2) o -> 
      red m c (trm_app t1 t2) o
  | red_app_1 : forall o2 o m m0 c v1 t2,
      red m c t2 o2 -> 
      red m c (ext_app_2 v1 o2) o -> 
      red m0 c (ext_app_1 (out_ter m v1) t2) o
  | red_app_2 : forall o m c m0 c0 v2 x t3,
      red m (c & x ~~ v2) t3 o -> 
      red m0 c0 (ext_app_2 (val_clo c x t3) (out_ter m v2)) o
  | red_new : forall o1 o m c t1,
      red m c t1 o1 -> 
      red m c (ext_new_1 o1) o -> 
      red m c (trm_new t1) o
  | red_new_1 : forall l m' m m0 c v,
      l = fresh_for m ->
      m' = Heap.write m l v ->      
      red m0 c (ext_new_1 (out_ter m v)) (out_ter m' (val_loc l))
  | red_get : forall o1 o m c t1,
      red m c t1 o1 -> 
      red m c (ext_get_1 o1) o -> 
      red m c (trm_get t1) o
  | red_get_1 : forall l m c m0 v,
      Heap.binds m l v ->      
      red m0 c (ext_get_1 (out_ter m (val_loc l))) (out_ter m v)
  | red_set : forall o1 o m c t1 t2,
      red m c t1 o1 -> 
      red m c (ext_set_1 o1 t2) o -> 
      red m c (trm_set t1 t2) o
  | red_set_1 : forall o2 o m c m0 v1 t2,
      red m c t2 o2 -> 
      red m c (ext_set_2 v1 o2) o -> 
      red m0 c (ext_set_1 (out_ter m v1) t2) o
  | red_set_2 : forall l m' m c m0 v,
      Heap.indom m l ->
      m' = Heap.write m l v ->
      red m0 c (ext_set_2 (val_loc l) (out_ter m v)) (out_ter m' v).


(************************************************************)
(* * Induction principle on the height of a derivation *)

(** Ideally, this section would be automatically generated by Coq *)

Section BigredInd.

Inductive redh : nat -> mem -> ctx -> ext -> out -> Prop :=
  | redh_val : forall n m c v,
      redh (S n) m c v (out_ter m v)
  | redh_var : forall n m c x v,
      LibEnv.binds x v c ->
      redh (S n) m c (trm_var x) (out_ter m v)
  | redh_abs : forall n m c x t,
      redh (S n) m c (trm_abs x t) (out_ter m (val_clo c x t))
  | redh_app : forall n o1 o m c t1 t2,
      redh n m c t1 o1 -> 
      redh n m c (ext_app_1 o1 t2) o -> 
      redh (S n) m c (trm_app t1 t2) o
  | redh_app_1 : forall n o2 o m m0 c v1 t2,
      redh n m c t2 o2 -> 
      redh n m c (ext_app_2 v1 o2) o -> 
      redh (S n) m0 c (ext_app_1 (out_ter m v1) t2) o
  | redh_app_2 : forall n o m c m0 c0 v2 x t3,
      redh n m (c & x ~~ v2) t3 o -> 
      redh (S n) m0 c0 (ext_app_2 (val_clo c x t3) (out_ter m v2)) o
  | redh_new : forall n o1 o m c t1,
      redh n m c t1 o1 -> 
      redh n m c (ext_new_1 o1) o -> 
      redh (S n) m c (trm_new t1) o
  | redh_new_1 : forall n l m' m c m0 v,
      l = fresh_for m ->
      m' = Heap.write m l v ->      
      redh (S n) m0 c (ext_new_1 (out_ter m v)) (out_ter m' (val_loc l))
  | redh_get : forall n o1 o m c t1,
      redh n m c t1 o1 -> 
      redh n m c (ext_get_1 o1) o -> 
      redh (S n) m c (trm_get t1) o
  | redh_get_1 : forall n l m c m0 v,
      Heap.binds m l v ->      
      redh (S n) m0 c (ext_get_1 (out_ter m (val_loc l))) (out_ter m v)
  | redh_set : forall n o1 o m c t1 t2,
      redh n m c t1 o1 -> 
      redh n m c (ext_set_1 o1 t2) o -> 
      redh (S n) m c (trm_set t1 t2) o
  | redh_set_1 : forall n o2 o m c m0 v1 t2,
      redh n m c t2 o2 -> 
      redh n m c (ext_set_2 v1 o2) o -> 
      redh (S n) m0 c (ext_set_1 (out_ter m v1) t2) o
  | redh_set_2 : forall n l m' m c m0 v,
      Heap.indom m l ->
      m' = Heap.write m l v ->
      redh (S n) m0 c (ext_set_2 (val_loc l) (out_ter m v)) (out_ter m' v).

Hint Constructors red redh.
Hint Extern 1 (_ < _) => math.

Lemma redh_lt : forall n n' m c e o,
  redh n m c e o -> n < n' -> redh n' m c e o.
Proof.
  introv H. gen n'. induction H; introv L; 
   (destruct n' as [|n']; [ false; math | autos* ]).
Qed.

Lemma red_redh : forall m c e o,
  red m c e o -> exists n, redh n m c e o.
Proof. hint redh_lt. introv H. induction H; try induct_height. Qed.

End BigredInd.


(************************************************************)
(* * Facts *)

Hint Constructors red.

Instance val_Inhab : Inhab val.
Proof. apply (Inhab_of_val (val_int 0)). Qed.

Instance loc_Comparable : Comparable loc.
(*Proof. constructor ; apply eq_nat_dec. Qed.*)


(************************************************************)
(* * Interpreter *)

(** Definition of a result *)

Inductive res :=
  | res_return : mem -> beh -> res
  | res_unspec : res
  | res_bottom : res.

Implicit Types r : res.

(** Bind-style operators *)

Definition if_success (r:res) (k:mem->val->res) : res :=
  match r with
  | res_return m (beh_ret v) => k m v
  | _ => r
  end.

Definition if_isclo (v:val) (k:ctx->var->trm->res) : res :=
  match v with
  | val_clo c x t => k c x t
  | _ => res_unspec
  end.

Definition if_true (i:bool) (k:unit->res) : res :=
  if i then k tt else res_unspec.

Definition if_isloc (v:trm) (k:loc->res) : res :=
  match v with
  | val_loc l => k l
  | _ => res_unspec
  end.

Fixpoint run (n:nat) (m:mem) (c:ctx) (t:trm) : res :=
  match n with 
  | O => res_bottom
  | S n' => 
    let run' := run n' in
    let ret := res_return m in
    match t with
    | trm_val v => ret v
    | trm_var x => 
       if_true (decide (x \in EnvOps.dom c)) (fun _ =>
         ret (get_or_arbitrary x c))
    | trm_abs x t1 => ret (val_clo c x t1)
    | trm_app t1 t2 => 
       if_success (run' m c t1) (fun m1 v1 =>
         if_success (run' m1 c t2) (fun m2 v2 =>
           if_isclo v1 (fun c' x t3 =>
             run' m2 (c' & x ~~ v2) t3)))
    | trm_new t1 => 
       if_success (run' m c t1) (fun m1 v1 =>
         let l := fresh_for m1 in
         let m2 := Heap.write m1 l v1 in
         res_return m2 (val_loc l))
    | trm_get t1 => 
       if_success (run' m c t1) (fun m1 v1 =>
         if_isloc v1 (fun l =>
           let v := Heap.read m1 l in
           if_true (decide (indom m1 l)) (fun _ =>
             res_return m1 v)))
    | trm_set t1 t2 => 
       if_success (run' m c t1) (fun m1 v1 =>
         if_success (run' m1 c t2) (fun m2 v2 =>
           if_isloc v1 (fun l =>
             res_return (Heap.write m2 l v2) v2)))
    end
  end.


(************************************************************)
(* * Completeness of the interpreter *)

Hint Extern 1 (_ > _) => abstract math.
Hint Extern 1 (_ < _) => abstract math.

Lemma if_true_elim : forall i P k,
  istrue i = P -> P ->
  (if_true i k) = k tt.
Proof.
  introv H F. unfolds. case_if.
  auto.
  rewrite <- H in F. false.
Qed.

Lemma if_success_elim : forall r k m v,
  r = res_return m (beh_ret v) ->
  if_success r k = k m v.
Proof. introv E ; rewrite* E. Qed.

Lemma redh_not_div : forall n m c e,
  ~redh n m c e out_div.
Proof. intro n ; induction* n ; introv H ; inverts* H. Qed.

Lemma runh_complete_ter : forall n m c t m' v,
  redh n m c t (out_ter m' v) -> 
  forall k, k > n -> 
    run k m c t = res_return m' v.
Proof.
  induction n using peano_induction.
  introv R L. destruct k. math. 
  asserts IH: (
    forall m0 c t m' v n',
    redh n' m0 c t (out_ter m' v) ->
    n' < n ->
    run k m0 c t = res_return m' v).
    intros. applys* H. clear H.
  inverts R as; simpl.
  auto.
  introv B. erewrite if_true_elim; eauto.
   fequals. rewrite~ (binds_get_or_arbitrary B).
   rewrite istrue_decide. applys* get_some_inv.
  auto.
  introv R1 R2. inverts R2 as R2 R3. inverts R3 as R3.
   rewrites~ (>> IH R1). simpl.
   rewrites~ (>> IH R2). simpl.
   applys* IH.
  introv R1 R2. inverts R2 as. rewrites~ (>> IH R1).
  introv R1 R2. inverts R2 as B.
   rewrites~ (>> IH R1). simpl.
   erewrite if_true_elim; eauto. 
     fequals_rec. applys (binds_read B).
     rewrite istrue_decide. applys* @LibHeap.binds_indom.
  introv R1 R2. inverts R2 as R2 R3. inverts R3 as R3.
   rewrites~ (>> IH R1). simpl.
   rewrites~ (>> IH R2). 
Qed.

Theorem run_complete_ter : forall m c t m' v,
  red m c t (out_ter m' v) -> 
  exists n0, forall n, n > n0 -> 
    run n m c t = res_return m' v.
Proof.
  introv H. lets (n0&R): red_redh (rm H).
  exists n0. introv L. 
  applys~ runh_complete_ter R.
Qed.


