Module Erasure

Set Implicit Arguments.
Require Import Coq.Relations.Relations.
Require Import MyTactics.
Require Import DeBruijn.
Require Import Coercions.
Require Import Store.
Require Import Layers.
Require Import Programs.
Require Import ValueLists.
Require Import RawPrograms.



Fixpoint erase_value (v : value) : raw_value :=
  match v with
  | VVar x =>
      RawVVar x
  | VAbs t =>
      RawVAbs (erase_term t)
  | VPair Physical Physical w1 w2 =>
      RawVPair (erase_value w1) (erase_value w2)
  | VPair Logical Physical w1 w2 =>
      erase_value w2
  | VPair Physical Logical w1 w2 =>
      erase_value w1
  | VPair Logical Logical w1 w2 =>
      RawVErased
  | VPhyUnit =>
      RawVUnit
  | VLoc l _ =>
      RawVLoc l
  | VTyAbs v
  | VPack v
  | VCoApp _ v
  | VBang v
  | VInhabitant v =>
      erase_value v
  | VRegionCap _
  | VRegionCapPunched _
  | VLogUnit =>
      RawVErased
  end

with erase_term (t : term) : raw_term :=
  match t with
  | TVal v =>
      RawTVal (erase_value v)
  | TApp v t =>
      RawTApp (erase_value v) (erase_term t)
  | TMixPair t1 v2 =>
      erase_term t1
  | TTyAbs t =>
      erase_term t
  | TCoApp _ t =>
      erase_term t
  | TLetBang v t
  | TLetUnpack v t
  | THide v t =>
      subst_raw_term (erase_value v) 0 (erase_term t)
  | TLetPair Physical Physical v t =>
      RawTLetPair (erase_value v) (erase_term t)
  | TLetPair Physical Logical v t =>
      subst_raw_term (erase_value v) 0 (subst_raw_term RawVErased 0 (erase_term t))
  | TLetPair Logical Physical v t =>
      subst_raw_term RawVErased 0 (subst_raw_term (lift_raw_value 0 (erase_value v)) 0 (erase_term t))
  | TLetPair Logical Logical v t =>
      subst_raw_term RawVErased 0 (subst_raw_term RawVErased 0 (erase_term t))
  | TPrimApp (PDefocusDuplicable _) v
  | TPrimApp (PFocus _) v
  | TPrimApp PNewGroup v
  | TPrimApp PAdopt v
  | TPrimApp PFocusGroup v =>
      RawTVal (erase_value v)
  | TPrimApp PNewAffine v
  | TPrimApp PNewCap v =>
      RawTNew (erase_value v)
  | TPrimApp PReadCap v =>
      RawTRead (erase_value v)
  | TPrimApp PWriteCap v =>
      RawTWrite (erase_value v)
  | TPrimApp PReadAffine v =>
      RawTLet (RawTRead (erase_value v)) (RawTVal (RawVPair (RawVVar 0) (lift_raw_value 0 (erase_value v))))
  | TPrimApp PWriteAffine v =>
      RawTLet (RawTWrite (erase_value v)) (RawTFirst (lift_raw_value 0 (erase_value v)))
  end.

Definition erase_store (s : store) : raw_store :=
  match s with
  | Store limit m =>
      Store limit (transform erase_value m)
  end.



Hint Extern 1 => match goal with eq: forall k, _ = _ |- _ => rewrite eq end : erase_lift.
Hint Extern 1 => rewrite raw_lift_lift_value : erase_lift.
Hint Extern 1 => rewrite raw_lift_subst_2_term : erase_lift.

Lemma erase_lift:
  (forall v k, erase_value (lift_value k v) = lift_raw_value k (erase_value v)) /\
  (forall vs : values, True) /\
  (forall t k, erase_term (lift_term k t) = lift_raw_term k (erase_term t)).

Hint Extern 1 => rewrite (pi1 erase_lift).
Hint Extern 1 => rewrite (pi3 erase_lift).

Hint Extern 1 => repeat match goal with eq: forall v k, _ = _ |- _ => rewrite eq end : erase_subst.
Hint Extern 1 => rewrite <- raw_lift_subst_1_value : erase_subst.

Ltac push_subst :=
  match goal with |- context[subst_raw_term _ ?s (subst_raw_term _ ?k _)] =>
    match s with
    | 0 => fail 1
    | _ => rewrite raw_subst_subst_term with (s1 := s); simpl; eauto
    end
  end.

Hint Extern 1 => push_subst : erase_subst.

Lemma erase_subst:
  (forall w v k, erase_value (subst_value v k w) = subst_raw_value (erase_value v) k (erase_value w)) /\
  (forall vs : values, True) /\
  (forall t v k, erase_term (subst_term v k t) = subst_raw_term (erase_value v) k (erase_term t)).

Hint Extern 1 => rewrite (pi3 erase_subst); simpl.
Hint Extern 1 => rewrite (proj2 raw_pun_1).
Hint Extern 1 => rewrite (proj2 raw_pun_2).



Inductive pwe : values -> values -> Prop :=
| PweNil:
    pwe VNil VNil
| PweCons:
    forall v1 v2 vs1 vs2,
    erase_value v1 = erase_value v2 ->
    pwe vs1 vs2 ->
    pwe (VCons v1 vs1) (VCons v2 vs2).

Hint Constructors pwe.

Lemma pwe_reflexive:
  forall vs,
  pwe vs vs.

Lemma pwe_some:
  forall (P : value -> Prop),
  (forall v w, erase_value v = erase_value w -> P v -> P w) ->
  forall vs1 vs2,
  pwe vs1 vs2 ->
  some P vs1 ->
  some P vs2.

Lemma pwe_count:
  forall vs1 vs2,
  pwe vs1 vs2 ->
  count vs1 = count vs2.

Lemma pwe_vmap_coapp:
  forall c vs,
  pwe vs (vmap (VCoApp c) vs).

Lemma pwe_vmap_vtyabs:
  forall vs,
  pwe vs (vmap VTyAbs vs).