Require Import Util EqDec DecSolve Val CSet Map Env EnvTy Option Get SetOperations.
Require Import Arith.

Set Implicit Arguments.

  Definition binop : Set := nat.
  Definition option_lift2 A B C (f:A → B → C) := fun x y ⇒ Some (f x y).
  Definition binop_eval (o:binop) :=
    match o with
      | 0 ⇒ option_lift2 Peano.plus
      | 1 ⇒ option_lift2 minus
      | 2 ⇒ option_lift2 mult
      | 3 ⇒ option_lift2 (fun x y ⇒ if [x = y] then 1 else 0)
      | 4 ⇒ option_lift2 (fun x y ⇒ if [x ≠ y] then 1 else 0)
      | _ ⇒ fun _ _ ⇒ None
    end.

  Definition unop : Set := nat.
  Definition option_lift1 A B (f:A → B) := fun x ⇒ Some (f x).

  Definition bool2val (b:bool) :=
    match b with
      | true ⇒ 1
      | false ⇒ 0
    end.

  Definition unop_eval (o:unop) :=
    match o with
      | 0 ⇒ option_lift1 (val2bool ∘ bool2val)
      | _ ⇒ fun _ ⇒ None
    end.

  Inductive exp :=
     Con : val → exp
   | Var : var → exp
   | UnOp : unop → exp → exp
   | BinOp : binop → exp → exp → exp.

  Inductive isVar : exp → Prop :=
    IisVar v : isVar (Var v).

  Instance isVar_dec e : Computable (isVar e).

  Definition getVar (e:exp) :=
    match e with
      | Var y ⇒ y
      | _ ⇒ 0
    end.

  Global Instance inst_eq_dec_exp : EqDec exp eq.
  Defined.

  Fixpoint exp_eval (E:onv val) (e:exp) : option val :=
    match e with
      | Con v ⇒ Some v
      | Var x ⇒ E x
      | UnOp o e ⇒ mdo v <- exp_eval E e;
                   unop_eval o v
      | BinOp o e1 e2 ⇒ mdo v1 <- exp_eval E e1;
                        mdo v2 <- exp_eval E e2;
                        binop_eval o v1 v2
    end.

  Inductive expOfType : onv ty → exp → ty → Prop :=
  | conOfType ET v t : expOfType ET (Con v) t
  | varOfType ET x t : ET x = Some t → expOfType ET (Var x) t.

  Lemma expOfType_subEnv
    : ∀ ET ET´ e t, subEnv ET´ ET → expOfType ET´ e t → expOfType ET e t.

  Lemma exp_type_soundness :
    ∀ ET E e t v, expOfType ET e t →
                       envOfType E ET →
                       exp_eval E e = Some v →
                       valOfType v t.

  Lemma exp_eval_typed_eq
    : ∀ ET E E´ e t, typed_eq ET E E´ → expOfType ET e t
      → exp_eval E e = exp_eval E´ e.

  Inductive live_exp_sound : exp → set var → Prop :=
  | ConLiveSound v lv : live_exp_sound (Con v) lv
  | VarLiveSound x lv : x ∈ lv → live_exp_sound (Var x) lv
  | UnopLiveSound o e lv :
      live_exp_sound e lv
      → live_exp_sound (UnOp o e) lv
  | binopLiveSound o e1 e2 lv :
      live_exp_sound e1 lv →
      live_exp_sound e2 lv →
      live_exp_sound (BinOp o e1 e2) lv.

  Instance live_exp_sound_dec e lv
  : Computable (live_exp_sound e lv).

  Lemma live_exp_sound_incl
    : ∀ e lv lv´, lv´ ⊆ lv → live_exp_sound e lv´ → live_exp_sound e lv.

  Fixpoint freeVars (e:exp) : set var :=
    match e with
      | Con _ ⇒ ∅
      | Var v ⇒ {v}
      | UnOp o e ⇒ freeVars e
      | BinOp o e1 e2 ⇒ freeVars e1 ∪ freeVars e2
    end.

  Lemma live_freeVars
    : ∀ e, live_exp_sound e (freeVars e).

  Lemma freeVars_live e lv
     : live_exp_sound e lv → freeVars e ⊆ lv.

  Lemma exp_eval_live
    : ∀ e lv E E´, live_exp_sound e lv → agree_on eq lv E E´ →
      exp_eval E e = exp_eval E´ e.

  Global Instance eval_exp_ext
  : Proper (@feq _ _ eq ==> eq ==> eq) exp_eval.

  Definition var_to_exp : ∀ x:var, exp := Var.
  Lemma var_to_exp_correct : ∀ M x,
     exp_eval M (var_to_exp x) = M x.

  Fixpoint rename_exp (ϱ:env var) (s:exp) : exp :=
    match s with
      | Con v ⇒ Con v
      | Var v ⇒ Var (ϱ v)
      | UnOp o e ⇒ UnOp o (rename_exp ϱ e)
      | BinOp o e1 e2 ⇒ BinOp o (rename_exp ϱ e1) (rename_exp ϱ e2)
    end.

  Lemma rename_exp_comp e ϱ ϱ´
  : rename_exp ϱ (rename_exp ϱ´ e) = rename_exp (ϱ´ ∘ ϱ) e.

  Lemma rename_exp_ext
    : ∀ e (ϱ ϱ´:env var), feq (R:=eq) ϱ ϱ´ → rename_exp ϱ e = rename_exp ϱ´ e.

  Lemma rename_exp_agree ϱ ϱ´ e
  : agree_on eq (Exp.freeVars e) ϱ ϱ´
    → rename_exp ϱ e = rename_exp ϱ´ e.

  Lemma rename_exp_freeVars
  : ∀ e ϱ `{Proper _ (_eq ==> _eq) ϱ},
      freeVars (rename_exp ϱ e) ⊆ lookup_set ϱ (freeVars e).

  Lemma live_exp_rename_sound e lv (ϱ:env var)
  : live_exp_sound e lv
    → live_exp_sound (rename_exp ϱ e) (lookup_set ϱ lv).

  Fixpoint subst_exp (ϱ:env exp) (s:exp) : exp :=
    match s with
      | Con v ⇒ Con v
      | Var v ⇒ (ϱ v)
      | UnOp o e ⇒ UnOp o (subst_exp ϱ e)
      | BinOp o e1 e2 ⇒ BinOp o (subst_exp ϱ e1) (subst_exp ϱ e2)
    end.

  Lemma subst_exp_comp e ϱ ϱ´
  : subst_exp ϱ (subst_exp ϱ´ e) = subst_exp (fun x ⇒ subst_exp ϱ (ϱ´ x)) e.

  Lemma subst_exp_ext
    : ∀ e (ϱ ϱ´:env exp), feq (R:=eq) ϱ ϱ´ → subst_exp ϱ e = subst_exp ϱ´ e.

  Inductive alpha_exp : env var → env var → exp → exp → Prop :=
  | AlphaCon ϱ ϱ´ v : alpha_exp ϱ ϱ´ (Con v) (Con v)
  | AlphaVar ϱ ϱ´ x y : ϱ x = y → ϱ´ y = x → alpha_exp ϱ ϱ´ (Var x) (Var y)
  | AlphaUnOp ϱ ϱ´ o e e´ :
      alpha_exp ϱ ϱ´ e e´
      → alpha_exp ϱ ϱ´ (UnOp o e) (UnOp o e´)
  | AlphaBinOp ϱ ϱ´ o e1 e1´ e2 e2´ :
      alpha_exp ϱ ϱ´ e1 e1´ →
      alpha_exp ϱ ϱ´ e2 e2´ →
      alpha_exp ϱ ϱ´ (BinOp o e1 e2) (BinOp o e1´ e2´).

  Lemma alpha_exp_rename_injective
  : ∀ e ϱ ϱ´,
      inverse_on (freeVars e) ϱ ϱ´
      → alpha_exp ϱ ϱ´ e (rename_exp ϱ e).

  Lemma alpha_exp_refl : ∀ e, alpha_exp id id e e.

  Lemma alpha_exp_sym : ∀ ϱ ϱ´ e e´, alpha_exp ϱ ϱ´ e e´ → alpha_exp ϱ´ ϱ e´ e.

  Lemma alpha_exp_trans
  : ∀ ϱ1 ϱ1´ ϱ2 ϱ2´ s s´ s´´,
      alpha_exp ϱ1 ϱ1´ s s´
      → alpha_exp ϱ2 ϱ2´ s´ s´´
      → alpha_exp (ϱ1 ∘ ϱ2) (ϱ2´ ∘ ϱ1´) s s´´.

  Lemma alpha_exp_inverse_on
    : ∀ ϱ ϱ´ s t, alpha_exp ϱ ϱ´ s t → inverse_on (freeVars s) ϱ ϱ´.

  Lemma alpha_exp_agree_on_morph
  : ∀ f g ϱ ϱ´ s t,
      alpha_exp ϱ ϱ´ s t
      → agree_on _eq (lookup_set ϱ (freeVars s)) g ϱ´
      → agree_on _eq (freeVars s) f ϱ
      → alpha_exp f g s t.

  Lemma exp_rename_renamedApart_all_alpha e e´ ϱ ϱ´
  : alpha_exp ϱ ϱ´ e e´
    → rename_exp ϱ e = e´.

  Lemma alpha_exp_morph
  : ∀ (ϱ1 ϱ1´ ϱ2 ϱ2´:env var) e e´,
      @feq _ _ eq ϱ1 ϱ1´
      → @feq _ _ eq ϱ2 ϱ2´
      → alpha_exp ϱ1 ϱ2 e e´
      → alpha_exp ϱ1´ ϱ2´ e e´.

Inductive expLt : exp → exp → Prop :=
| ExpLtCon c c´
  : _lt c c´
    → expLt (Con c) (Con c´)
| ExpLtConVar c v
  : expLt (Con c) (Var v)
| ExpLtConUnOp c o e
  : expLt (Con c) (UnOp o e)
| ExpLtConBinop c o e1 e2
  : expLt (Con c) (BinOp o e1 e2)
| ExpLtVar v v´
  : _lt v v´
    → expLt (Var v) (Var v´)
| ExpLtVarUnOp v o e
  : expLt (Var v) (UnOp o e)
| ExpLtVarBinop v o e1 e2
  : expLt (Var v) (BinOp o e1 e2)
| ExpLtUnOpBinOp o e o´ e1 e2
  : expLt (UnOp o e) (BinOp o´ e1 e2)
| ExpLtUnOp1 o o´ e e´
  : _lt o o´
    → expLt (UnOp o e) (UnOp o´ e´)
| ExpLtUnOp2 o e e´
  : expLt e e´
    → expLt (UnOp o e) (UnOp o e´)
| ExpLtBinOp1 o o´ e1 e1´ e2 e2´
  : _lt o o´
    → expLt (BinOp o e1 e2) (BinOp o´ e1´ e2´)
| ExpLtBinOp2 o e1 e1´ e2 e2´
  : expLt e1 e1´
    → expLt (BinOp o e1 e2) (BinOp o e1´ e2´)
| ExpLtBinOp3 o e1 e2 e2´
  : expLt e2 e2´
    → expLt (BinOp o e1 e2) (BinOp o e1 e2´).

Instance expLt_irr : Irreflexive expLt.
Qed.

Instance expLt_trans : Transitive expLt.
Qed.

Notation "´Compare´ x ´next´ y" :=
  (match x with
    | Eq ⇒ y
    | z ⇒ z
  end) (at level 100).

Fixpoint exp_cmp (e e´:exp) :=
  match e, e´ with
    | Con c, Con c´ ⇒ _cmp c c´
    | Con _, _ ⇒ Lt
    | Var v, Var v´ ⇒ _cmp v v´
    | Var v, UnOp _ _ ⇒ Lt
    | Var v, BinOp _ _ _ ⇒ Lt
    | UnOp _ _, BinOp _ _ _ ⇒ Lt
    | UnOp o e, UnOp o´ e´ ⇒
      Compare _cmp o o´ next
      Compare exp_cmp e e´ next Eq
    | BinOp o e1 e2, BinOp o´ e1´ e2´ ⇒
      Compare _cmp o o´ next
      Compare exp_cmp e1 e1´ next
      Compare exp_cmp e2 e2´ next Eq
    | _, _ ⇒ Gt
  end.

Instance StrictOrder_expLt : OrderedType.StrictOrder expLt eq.
Qed.

Instance OrderedType_exp : OrderedType exp :=
 { _eq := eq;
  _lt := expLt;
  _cmp := exp_cmp}.
Defined.

Lemma freeVars_renameExp ϱ e
: freeVars (rename_exp ϱ e) [=] lookup_set ϱ (freeVars e).

Definition exp2bool (e:exp) : option bool :=
  match e with
    | Con c ⇒ Some (val2bool c)
    | _ ⇒ None
  end.

Lemma exp2bool_val2bool E e b
: exp2bool e = Some b
  → ∃ v, exp_eval E e = Some v ∧ val2bool v = b.