Module Semantics

Set Implicit Arguments.
Require Import MyTactics.
Require Import Coercions.
Require Import Store.
Require Import RawPrograms.
Require Import Layers.
Require Import Programs.
Require Import ValueLists.
Require Import PathSemantics.
Require Import Erasure.
Require Import RevelationDefinition.
Require Import SemanticsValues.

Operational semantics: the reduction of terms.

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

Evaluation contexts for the reduction of terms.

Inductive ectx :=
| EAppRight: value -> ectx
| EMixPairLeft: value -> ectx
| ECoApp: coercion -> ectx
.

Filling an evaluation context with a term.

Fixpoint efill (EC : ectx) (t : term) :=
  match EC with
  | EAppRight v =>
      TApp v t
  | EMixPairLeft v2 =>
      TMixPair t v2
  | ECoApp c =>
      TCoApp c t
  end.

Applying revelation to an evaluation context produces another evaluation context.

Technically, reveal_ectx nh EC cannot be an evaluation context, because it would have to be more than one level high in some cases (see EMixPairLeft), whereas our evaluation contexts are exactly one level high. Never mind -- we represent it as function of type term -> term. This works fine for our purposes.

Definition reveal_ectx nh (EC : ectx) (t : term) :=
match EC with
| EAppRight v =>

Applying revelation to an application context v [] amounts to applying revelation to the value v.

TApp (fold_reveal_value nh v) t
| EMixPairLeft v2 =>

To apply revelation to a mixed pair context ([], v2), we apply revelation to v2; this yields a pair of type (T1 o U, T2 x U), out of which we extract the invariant U, so as to obtain a pair of type (T1 x U, T2 x U) * U, that is, (T1, T2) o U.

CoMixPairCompossExchange nh (TMixPair t (fold_reveal_value nh v2))
| ECoApp c =>

To apply revelation to a coercion context c [], we wrap the coercion c, so that it works under the type context [] o U.

      TCoApp (co_composs nh c) t
  end.

Ltac ectx :=
  repeat match goal with EC : ectx |- _ => destruct EC end.

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

Reduction of terms.

The reduction judgement for terms is unusual in that it is asymmetric: on the left-hand side is a store/term pair, while on the right-hand side we find not only a new store and a new term, but also an integer that counts how many active hide constructs have extruded during this reduction step. This integer is usually zero or one.

Inductive red : store -> term -> nat -> store -> term -> Prop :=
| RedVal:
    forall s v1 v2,
    redv v1 v2 ->
    red s (TVal v1) 0 s (TVal v2)
| RedBeta:
    forall s t v,
    red
      s (TApp (VAbs t) (TVal v)) 0
      s (subst_term v 0 t)
| RedMixPair:
    forall s v1 v2,
    red
      s (TMixPair (TVal v1) v2) 0
      s (TVal (VMixPair v1 v2))
| RedLetBang:
    forall s v t,
    red
      s (TLetBang (VBang v) t) 0
      s (subst_term v 0 t)
| RedLetPair:
    forall s layer1 layer2 v1 v2 t,
    red
      s (TLetPair layer1 layer2 (VPair layer1 layer2 v1 v2) t) 0
      s (subst_term v1 0 (subst_term (lift_value 0 v2) 0 t))
| RedTyAbs:
    forall s v,
    red
      s (TTyAbs (TVal v)) 0
      s (TVal (VTyAbs v))
| RedUnpack:
    forall s v t,
    red
      s (TLetUnpack (VPack v) t) 0
      s (subst_term v 0 t)
| RedCoApp:
    forall s c v,
    red
      s (TCoApp c (TVal v)) 0
      s (TVal (VCoApp c v))
| RedDefocusDuplicable:

note: one could further require w to be canonical; this would imply that w has zero weight and could be useful if one wishes to make this a coercion

forall s v1 v2 pi v vs w,

Extract out of v1 the component v of interest

select pi v1 (VInhabitant v) ->

Find in the list vs an inhabitant w that matches v up to erasure

member (VBang w) vs ->

erase_value v = erase_value w follows from select and plug

Plug w into v1 to obtain v2

    plug pi v1 (VBang w) v2 ->
    red
      s (TPrimApp (PDefocusDuplicable pi) (VMixPair v1 (VRegionCap vs))) 0
      s (TVal (VMixPair v2 (VRegionCap vs)))
| RedFocus:
    forall s pi v1 v2 v'1,
    select pi v1 v2 ->
    plug pi v1 (VInhabitant v2) v'1 ->
    red
      s (TPrimApp (PFocus pi) v1) 0
      s (TVal (VPack (VMixPair v'1 (VRegionCap (VCons v2 VNil)))))
| RedNewGroup:
    forall s,
    red
      s (TPrimApp PNewGroup VPhyUnit) 0
      s (TVal (VPack (VMixPair VPhyUnit (VRegionCap VNil))))
| RedAdopt:
    forall s v vs,
    red
      s (TPrimApp PAdopt (VMixPair v (VRegionCap vs))) 0
      s (TVal (VMixPair (VInhabitant v) (VRegionCap (VCons v vs))))
| RedFocusGroup:
    forall s v w vs,

The list vs of the region inhabitants must decompose into the value in the hole w, and the other inhabitants, remove w vs. The choice of w is dictated by the key v -- that is, v and w must be equal up to erasure.

    erase_value v = erase_value w ->
    member w vs ->
    red
      s (TPrimApp PFocusGroup (VMixPair (VInhabitant v) (VRegionCap vs))) 0
      s (TVal (VPack (VMixPair
                       (VInhabitant v)
                       (VLogPair (VRegionCap (VCons w VNil)) (VRegionCapPunched (remove w vs))))))
| RedNewAffine:
    forall m1 l v m2,
    extend m1 l v = m2 ->
    red
      (Store l m1) (TPrimApp PNewAffine v) 0
      (Store (S l) m2) (TVal (VLoc l v))
| RedReadAffine:
    forall limit m l v w,
    m l = Some v ->
    erase_value v = erase_value w ->
    red
      (Store limit m) (TPrimApp PReadAffine (VLoc l (VBang w))) 0
      (Store limit m) (TVal (VPhyPair (VBang w) (VLoc l (VBang w))))
| RedWriteAffine:
    forall limit m1 l v1 v2 m2 w,
    m1 l = Some v1 ->
    extend m1 l v2 = m2 ->
    red
      (Store limit m1) (TPrimApp PWriteAffine (VPhyPair (VLoc l w) v2)) 0
      (Store limit m2) (TVal (VLoc l v2))
| RedNewCap:
    forall m1 l v m2,
    extend m1 l v = m2 ->
    red
      (Store l m1)
      (TPrimApp PNewCap v)
      0
      (Store (S l) m2)
      (TVal (VPack (VMixPair (VInhabitant (VLoc l v)) (VRegionCap (VCons (VLoc l v) VNil)))))
| RedReadCap:
    forall limit m l v w v',
    m l = Some v ->
    erase_value v = erase_value w ->
    erase_value v' = RawVLoc l ->
    red
      (Store limit m)
      (TPrimApp PReadCap (VMixPair (VInhabitant v') (VRegionCap (VCons (VLoc l (VBang w)) VNil))))
      0
      (Store limit m)
      (TVal (VMixPair (VBang w) (VRegionCap (VCons (VLoc l (VBang w)) VNil))))
| RedWriteCap:
    forall limit m1 l v1 v2 m2 w v'1,
    m1 l = Some v1 ->
    extend m1 l v2 = m2 ->
    erase_value v'1 = RawVLoc l ->
    red
      (Store limit m1)
      (TPrimApp PWriteCap (VMixPair
                            (VPhyPair (VInhabitant v'1) v2)
                            (VRegionCap (VCons (VLoc l w) VNil))))
      0
      (Store limit m2)
      (TVal (VMixPair VPhyUnit (VRegionCap (VCons (VLoc l v2) VNil))))
| RedAppContextLeft:
    forall s v1 v2 t,
    redv v1 v2 ->
    red s (TApp v1 t) 0 s (TApp v2 t)
| RedContext:

If the reduction of t1 into t2 emits active hide constructs, then these constructs extrude out of the evaluation context EC, which means that revelation must be applied to EC.

    forall EC s1 s2 nh t1 t2,
    red s1 t1 nh s2 t2 ->
    red s1 (efill EC t1) nh s2 (reveal_ectx nh EC t2)
| RedTTyAbsContext:

An active hide construct cannot extrude out of TTyAbsContext, because the hidden invariant might refer to the type variable that is bound by this type abstraction. This is exactly the unsound interaction between unrestricted polymorphism and the anti-frame rule, a well-known special case of which is the unsound interaction betwen unrestricted polymorphism and ML references.

    forall s1 s2 t1 t2,
    red s1 t1 0 s2 t2 ->
    red s1 (TTyAbs t1) 0 s2 (TTyAbs t2)
| RedTLetUnpackContext:
    forall s v1 v2 t,
    redv v1 v2 ->
    red s (TLetUnpack v1 t) 0 s (TLetUnpack v2 t)
| RedTLetBangContext:
    forall s v1 v2 t,
    redv v1 v2 ->
    red s (TLetBang v1 t) 0 s (TLetBang v2 t)
| RedTLetPairContext:
    forall s layer1 layer2 v1 v2 t,
    redv v1 v2 ->
    red s (TLetPair layer1 layer2 v1 t) 0 s (TLetPair layer1 layer2 v2 t)
| RedTPrimAppContext:
    forall s p v1 v2,
    redv v1 v2 ->
    red s (TPrimApp p v1) 0 s (TPrimApp p v2)
| RedTHide:

When it reaches a position where it can be evaluated, a construct hide x = v in t becomes active: the value v is substituted for x in t, yielding a closed term, and an active hide is emitted -- represented by the integer 1. In fact, reveal_value v is used, rather than v. The value v represents the entry point(s) provided by the environment to the module that has hidden state; these entry points are initially not aware of the existence of a hidden state.

forall s v t,
red s (THide v t) 1 s (subst_term (reveal_value v) 0 t)
.

Hint Constructors red.

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

The rule RedContext must be specialized for every form of evaluation context, otherwise eauto is unable to apply it.

We do nevertheless consider it useful to introduce the notion of evaluation context, and to have just one rule for evaluation under a context, because this leads to just one case in the subject reduction proof -- and this is a hairy case, which we would not wish to duplicate.

Lemma RedContextEAppRight:
  forall s1 s2 nh t1 t2 v,
  red s1 t1 nh s2 t2 ->
  red s1 (TApp v t1) nh s2 (TApp (fold_reveal_value nh v) t2).

Proof.

intros. forwards: (RedContext (EAppRight v)). eassumption. assumption.
Qed.

Lemma RedContextEMixPairLeft:
  forall s1 s2 nh t1 t2 v,
  red s1 t1 nh s2 t2 ->
  red s1 (TMixPair t1 v) nh s2 (reveal_ectx nh (EMixPairLeft v) t2).

Proof.

intros. forwards: (RedContext (EMixPairLeft v)). eassumption. assumption.
Qed.

Lemma RedContextECoApp:
  forall s1 s2 nh t1 t2 c,
  red s1 t1 nh s2 t2 ->
  red s1 (TCoApp c t1) nh s2 (TCoApp (co_composs nh c) t2).

Proof.

intros. forwards: (RedContext (ECoApp c)). eassumption. assumption.
Qed.

Hint Resolve RedContextEAppRight RedContextEMixPairLeft RedContextECoApp : red_context.

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

The reflexive and transitive closure of red.

Inductive redstar (s1 : store) (t1 : term) : store -> term -> Prop :=
| RedstarRefl:
    redstar s1 t1 s1 t1
| RedstarStep:
    forall nh s2 t2, red s1 t1 nh s2 t2 -> redstar s1 t1 s2 t2
| RedstarTrans:
    forall s2 t2 s3 t3, redstar s1 t1 s2 t2 -> redstar s2 t2 s3 t3 -> redstar s1 t1 s3 t3.

Hint Constructors redstar.