Module RevelationDefinition

Set Implicit Arguments.
Require Import MyTactics.
Require Import Arithmetic.
Require Import DeBruijn.
Require Import Layers.
Require Import Coercions.
Require Import Programs.
Require Import ValueLists.
Require Import RawPrograms.
Require Import Erasure.

-------------------------------------------------------------------------

The functions reveal_value and reveal_term indicate how values and terms are transformed by the revelation of an extra capability.

If v has type T, then reveal_value v has type TyTensor T U. In particular, if v is a function, then it takes and returns an extra argument, a capability.

If t has type T, then reveal_term k t has type TyTensor T U, under an environment where a binding of k to U has been inserted -- this represents the extra capability that is revealed. We do not impose k = 0, because this added flexibility simplifies the transformation of TLetUnpack and other binding constructs.

In the definition of reveal_term, every call to reveal_value is followed with a use of lift_value k, so as to compensate for the insertion of the new capability at index k.

Fixpoint reveal_value (v : value) :=
  match v with
  | VVar _
  | VUnit _ =>
      v
  | VAbs t =>

The function argument x is decomposed into a pair y, z, where y is the original argument and z is the new capability. References to x within t are (transparently) replaced with references to y -- this is index 1 -- and an application of lift_term 2 is used in order to jump above the now unused binding of x.

      VAbs (TLetPair Physical Logical (VVar 0) (lift_term 2 (reveal_term 0 t)))
  | VPair layer1 layer2 v1 v2 =>
      VPair layer1 layer2 (reveal_value v1) (reveal_value v2)
  | VTyAbs v =>
      VTyAbs (reveal_value v)
  | VPack v =>
      VPack (reveal_value v)
  | VCoApp c v =>

At coercion applications, the revelation lemma for subtyping is used.

      VCoApp (co_tensor c) (reveal_value v)
  | VBang v =>
      VBang (reveal_value v)
  | VLoc l v =>
      VLoc l (reveal_value v)
  | VRegionCap vs =>
      VRegionCap (reveal_values vs)
  | VRegionCapPunched vs =>
      VRegionCapPunched (reveal_values vs)
  | VInhabitant v =>
      VInhabitant (reveal_value v)
  end

with reveal_values (vs : values) :=
  match vs with
  | VNil =>
      VNil
  | VCons v vs =>
      VCons (reveal_value v) (reveal_values vs)
  end

with reveal_term (k : nat) (t : term) :=
  match t with
  | TVal v =>

At values, we must return a pair of the original result -- the value -- and the extra capability -- which has index k.

TVal (VMixPair (lift_value k (reveal_value v)) (VVar k))
| TApp v t =>

At function applications, the argument -- a term -- produces a pair, and the function expects a pair, so there is nothing to do.

TApp (lift_value k (reveal_value v)) (reveal_term k t)
| TMixPair t v =>

At mixed pairs, the extra pair that the tensor creates must commute with the pair that was there in the first place.

TCoApp CoMixPairExchange (TMixPair (reveal_term k t) (lift_value k (reveal_value v)))
| TTyAbs t =>

At type abstractions, the natural translation produces a universally quantified pair, whose right-hand component we must extract out of the universal quantification -- or, conversely, we must intrude the universal quantifier into the pair.

TCoApp (CoForallPairLeft Physical Logical) (TTyAbs (reveal_term k t))
| TCoApp c t =>

At coercion applications, the revelation lemma for subtyping is used, but only in the left-hand side of the value/capability pair.

TCoApp (CoMixPair (co_tensor c) CoId) (reveal_term k t)
| TLetUnpack v t =>

The easiest way of translating a binding construct is to let the new variable have index 0, as usual -- so the extra capability, which was at index k, now is at index k+1.

      TLetUnpack (lift_value k (reveal_value v)) (reveal_term (S k) t)
  | TLetBang v t =>
      TLetBang (lift_value k (reveal_value v)) (reveal_term (S k) t)
  | TLetPair layer1 layer2 v t =>
      TLetPair layer1 layer2 (lift_value k (reveal_value v)) (reveal_term (S (S k)) t)
  | TPrimApp p v =>

At a primitive operation, the extra capability must be framed out while the primitive operation is carried out.

      TMixPair
        (TPrimApp p (lift_value k (reveal_value v)))
        (VVar k)
  | THide v t =>

Let us write reveal v for reveal_value v and reveal k in t for reveal_term k t. Let us further use informal nominal syntax. We must now offer a definition for reveal y in (hide x = v in t) The definition that we propose is: hide z = (reveal v, y) in let (x, y) = z in let x = CoTensorExchange 0 x in CoComposExchange (reveal y in t) where the replacement of x with CoTensorExchange 0 x is in fact performed via a substitution, not via a let construct, so as to avoid disturbing the erasure of the term. The term reveal y in t has two free variables, namely x and y, and we wish to place it in the scope of a hide construct, which supports only one free variable, so we must (somewhat artifically, but that is not a problem) pair them up before entering the hide construct and deconstruct the pair immediately after entering it. What is more subtle is that the type of x has two tensors -- one created by reveal v, the other created by hide -- and they are in the wrong order, so we must use CoTensorExchange 0 to swap them. Symmetrically, the result produced by reveal y in t also has two tensors, again in the wrong order, so we must use CoComposExchange to swap them.

      THide
        (VMixPair (lift_value k (reveal_value v)) (VVar k))
        (lift_term (S k) (
          TLetMixPair (VVar 0) (lift_term 2 (
            subst_term (VCoApp (CoTensorExchange 0) (VVar 1)) 1 (lift_term 2 (
              TCoApp CoComposExchange (reveal_term 0 t)
        ))))))
  end.

Fixpoint fold_reveal_value (nh : nat) v :=
  match nh with
  | 0 =>
      v
  | S nh =>
      fold_reveal_value nh (reveal_value v)
  end.

-------------------------------------------------------------------------

Up to erasure, revelation has no effect.

Hint Extern 1 => rewrite <- raw_lift_subst_2_term : erase_reveal.
Hint Extern 1 => rewrite <- raw_lift_subst_2_term_rawverased : erase_reveal.
Hint Extern 1 => rewrite raw_lift_lift_value : erase_reveal.

Lemma erase_reveal:
(
  forall v,
  erase_value (reveal_value v) = erase_value v
) /\ (
  forall vs : values,
  pwe vs (reveal_values vs)
) /\ (
  forall t k,
  erase_term (reveal_term k t) = lift_raw_term k (erase_term t)
).

Proof.

  apply value_term_ind; simpl; intros; try prim; layers;
  try rewrite (pi1 erase_lift);
  try rewrite (pi3 erase_lift);
  repeat match goal with ihv: _ = _ |- _ => rewrite ihv end;
  repeat match goal with iht: forall k, _ = _ |- _ => rewrite iht end;
  try congruence;
  eauto with erase_reveal.

VAbs

  rewrite <- raw_lift_subst_2_term_rawverased; eauto.
  rewrite raw_subst_lift_term.
  rewrite (proj2 raw_pun_2); eauto.

THide.

  rewrite (pi3 erase_lift).
  rewrite (pi3 erase_subst). simpl.
  rewrite (pi3 erase_lift).
  match goal with iht: forall k, _ = _ |- _ => rewrite iht end.
  rewrite (proj2 raw_pun_2).
  rewrite <- raw_lift_subst_2_term_rawverased; eauto.
  change (RawVVar (lift_var (S k) 0)) with (lift_raw_value (S k) (RawVVar 0)).
  rewrite <- raw_lift_subst_2_term; eauto.
  rewrite <- raw_lift_subst_2_term; eauto.
  do 2 f_equal.
  rewrite <- raw_lift_lift_term; eauto.
  rewrite raw_subst_lift_term.
  rewrite (proj2 raw_pun_2); eauto.
Qed.

Lemma erase_reveal_value:
forall v,
erase_value (reveal_value v) = erase_value v.

Proof.

eauto using (pi1 erase_reveal).
Qed.

Lemma erase_reveal_term:
forall t k,
erase_term (reveal_term k t) = lift_raw_term k (erase_term t).

Proof.

eauto using (pi3 erase_reveal).
Qed.

Hint Resolve (pi2 erase_reveal).

Lemma fold_erase_reveal:
forall nh v,
erase_value (fold_reveal_value nh v) = erase_value v.

Proof.

induction nh; simpl; intros. eauto. rewrite IHnh. eapply erase_reveal_value.
Qed.

-------------------------------------------------------------------------

Revelation commutes with lifting. This means, in particular, that applying revelation to a closed value yields a closed value.

Lemma lift_reveal:
(
  forall v j,
  lift_value j (reveal_value v) = reveal_value (lift_value j v)
) /\ (
  forall vs : values,
  True
) /\ (
  forall t k j,
  k <= j ->
  lift_term (S j) (reveal_term k t) = reveal_term k (lift_term j t)
).
Local Hint Extern 1 (_ = _) => congruence.

Proof.

  apply value_term_ind; simpl; intros; eauto 2;
  try (rewrite lift_var_recent; eauto);
  try (rewrite <- lift_lift_value; eauto);
  try (rewrite <- lift_lift_term; eauto);
  try solve [
    try match goal with ihv: forall j, _ = _ |- _ => rewrite ihv; eauto end;
    try match goal with iht: forall k j, _ -> _ = _ |- _ => rewrite iht; eauto end
  ].

THide

  f_equal.
  eauto.
  do 3 f_equal.
  rewrite <- lift_lift_term; eauto; f_equal.
  rewrite lift_subst_2_term; eauto; f_equal.
  rewrite <- lift_lift_term; eauto; f_equal.
  eauto.
Qed.

Lemma well_scoped_reveal:
  forall v k,
  well_scoped_lift lift_value k v ->
  well_scoped_lift lift_value k (reveal_value v).

Proof.

unfold well_scoped_lift. intros. rewrite (pi1 lift_reveal). f_equal. eauto.
Qed.

Lemma closed_reveal:
  forall v,
  closed_value v ->
  closed_value (reveal_value v).

Proof.

unfold closed_value, closed. eauto using well_scoped_reveal.
Qed.

-------------------------------------------------------------------------

A coercion that lifts a bunch of composition operators out of a pair.

This is pretty boring. One could probably avoid the need for a recursive definition if one exploited the fact that active hide constructs extrude only one at a time (so n is always 0 or 1).

This coercion is used in the definition of the semantics, and we do not want the semantics to depend on the typing rules, so we must separate the definition of the coercion and the proof of its derived typing rule.

Fixpoint CoMixPairCompossExchange (n : nat) (t : term) : term :=
  match n with
  | 0 =>
      t
  | S n =>
      TCoApp (co_composs n CoMixPairComposExchange) (CoMixPairCompossExchange n t)
  end.

Lemma erase_CoMixPairCompossExchange:
  forall n t,
  erase_term (CoMixPairCompossExchange n t) = erase_term t.

Proof.

induction n; simpl; eauto.
Qed.