Library DomainsSign

Require Export Ascii.
Require Export String.

Require Export Containers.OrderedType Containers.Tactics.

Set Implicit Arguments.
Require Export ConcreteWhile.
Require Export LibHeap.

Section Domains.

Require Export sign.
Require Export otherlattices.

Definition aVal := Sign.t.

Definition gamma_aVal : aVal → ℘ Val := Sign.gamma.

Instance var_OrderedType : OrderedType.OrderedType var.
Admitted.

Lemma var_eq_eq : ∀ v1 v2 : var,
  v1 === v2 → v1 = v2.
Admitted.

Definition aErr := PowerSet.t error.

Global Instance aErrPoset : PosetDec.t aErr.
  apply PowerSet.Poset with (fun f ⇒ f Err).
   introv. iff I; repeat intros (); apply I.
   apply make_comparable.
    intros () (). apply decidable_make with true. fold_bool. rew_refl¬.
Defined.

Global Instance aErrLat : LatticeDec.t aErr.
  apply PowerSet.Lattice with (fun f ⇒ f Err).
   introv. iff I; repeat intros (); apply I.
   apply make_comparable.
    intros () (). apply decidable_make with true. fold_bool. rew_refl¬.
Defined.

Global Instance aErrTop : TopDec.t aErr.
  typeclass.
Defined.

Definition gamma_aErr : aErr → ℘ error := PowerSet.gamma _.

Definition UndefLat := LiftBot.t UnitLattice.t.

Global Instance UndefLat_lattice : LatticeDec.t UndefLat.
Proof. apply LiftBot.Lat. typeclass. Defined.

Definition aValVar := SumLattice.t aVal UndefLat.

Definition gamma_aValVar : aValVar → ℘ (Val + unit) :=
  SumLattice.gamma _ _ _ (LiftBot.Lat _ UnitLattice.Lat) _ _
    gamma_aVal (LiftBot.gamma _ _ UnitLattice.gamma).

Definition aUndef : aValVar := SumLattice.make2 _ _ (Some tt).

Definition aEnv :=
  MapDefault.t var aValVar _ (SumLattice.Lattice _ _ _ (LiftBot.Lat _ UnitLattice.Lat)).

Definition gamma_aEnv : aEnv → ℘ Env :=
  immerse_gamma _ _ (MapDefault.gammaf _ _ _ _ _ gamma_aValVar) _
    (fun E x ⇒
       match read_option E x with
       | Some v ⇒ inl v
       | None ⇒ inr tt
       end).

Definition aOute := (aVal × aErr)%type.

Definition gamma_aOute : aOute → ℘ oute :=
  immerse_gamma _ _ (productSumGamma _ _ _ _ gamma_aVal gamma_aErr) _
    (fun o ⇒
       match o return Val + error with
       | oute_val v ⇒ inl v
       | oute_error err ⇒ inr err
       end).

Definition aOuts := (aEnv × aErr)%type.

Definition gamma_aOuts : aOuts → ℘ outs :=
  immerse_gamma _ _ (productSumGamma _ _ _ _ gamma_aEnv gamma_aErr) _
    (fun o ⇒
       match o return Env + error with
       | outs_normal E ⇒ inl E
       | outs_error err ⇒ inr err
       end).

Global Instance : Gamma.t _ _ gamma_aOuts.
Proof.   apply immerseGamma. apply ProductSumGamma; typeclass.
Defined.

Definition read_env (E : aEnv) x :=
  MapDefault.read _ _ _ _ E x.

Definition write_env (E : aEnv) x v : aEnv :=
  MapDefault.write _ _ _ _ E x (Some (inl v)).

Definition get_value : aValVar → aVal :=
  fun v ⇒
    match v with
    | Some (inl v) ⇒ v
    | Some (inr undef) ⇒ ⊥♯
    | None ⇒ ⊤♯
    end.

Lemma gamma_aEnv_awrite : ∀ E aE x av,
  gamma_aEnv (write_env aE x av) E →
  ∃ v,
    binds E x v ∧
    gamma_aVal av v.
Proof.
  introv G. unfold write_env in G.
  set (R := MapDefault.read_write_eq var aValVar var_OrderedType _
               aE x x (Some (inl av)) (Equivalence_Reflexive _)). clearbody R.
  do 3 unfolds in G. rename G into G'.
  set (G := G' x). clearbody G. clear G'.
  rewrite Heap.read_option_def in G. cases_if as I.
   inverts G as G G'.
    rewrite <- G' in R. clear G'. inverts R as R. eexists. splits.
      apply× @read_binds.
      clear - G R. set (G' := Gamma_eq _ _ _ _ gamma_aVal _ _ _ R). clearbody G'. clear R.
       apply¬ G'.
    rewrite <- G in R. inverts R.
    inverts G.
   set (Er := Gamma_eq _ _ _ _ gamma_aValVar _ _ _ R). clearbody Er. clear R.
    set (Er' := proj1 (Er (inr tt))). clearbody Er'. clear Er. apply Er' in G. clear Er'.
    inverts G as G. simpl in G. destruct G.
Qed.

End Domains.

Extract Constant var_OrderedType ⇒ "(fun s1 s2 -> if s1 = s2 then Eq else if s1 < s2 then Lt else Gt)".