Module Types

Set Implicit Arguments.
Require Import DeBruijn.
Require Import Layers.

A region is just a natural integer. Regions appear in types via the TyRegion constructor. Resources map regions to permissions. Regions can be thought of as runtime objects -- they do not appear in a typing derivation for a source program.

Regions must not be confused with region variables. The latter are just type variables -- that is, de Bruijn indices -- and they appear in types via the TyVar constructor.

Definition region :=
nat.

Types.

Inductive quantifier :=
| QForall: quantifier
| QExists: quantifier .

Inductive region_kind :=
| Singleton: region_kind
| Group: region_kind .

Inductive ty :=
| TyVar: nat -> ty
| TyArrow: ty -> ty -> ty
| TyPair: layer -> layer -> ty -> ty -> ty
| TyUnit: layer -> ty
| TyQ: quantifier -> ty -> ty
| TyMu: ty -> ty
| TyBang: ty -> ty
| TyRef: ty -> ty
| TyRegion: region -> ty
| TyAt: ty -> ty
| TyRegionCap: region_kind -> ty -> ty -> ty
| TyRegionCapPunched: ty -> ty -> ty -> ty
| TyTensor: ty -> ty -> ty
.

Notation TyForall :=
  (TyQ QForall).

Notation TyExists :=
  (TyQ QExists).

Notation TyPhyPair :=
  (TyPair Physical Physical).

Notation TyMixPair :=
  (TyPair Physical Logical).

Notation TyLogPair :=
  (TyPair Logical Logical).

Notation TyPhyUnit :=
  (TyUnit Physical).

Notation TyLogUnit :=
  (TyUnit Logical).

Notation TyCompos T U :=
  (TyMixPair (TyTensor T U) U).

De Bruijn operations over types.

Fixpoint lift_ty (k : nat) (t : ty) : ty :=
  match t with
  | TyVar x =>
      TyVar (lift_var k x)
  | TyArrow t1 t2 =>
      TyArrow (lift_ty k t1) (lift_ty k t2)
  | TyPair layer1 layer2 t1 t2 =>
      TyPair layer1 layer2 (lift_ty k t1) (lift_ty k t2)
  | TyUnit layer =>
      TyUnit layer
  | TyQ q t =>
      TyQ q (lift_ty (1 + k) t)
  | TyMu t =>
      TyMu (lift_ty (1 + k) t)
  | TyBang t =>
      TyBang (lift_ty k t)
  | TyRef t =>
      TyRef (lift_ty k t)
  | TyRegion r =>
      TyRegion r
  | TyAt t =>
      TyAt (lift_ty k t)
  | TyRegionCap rk t1 t2 =>
      TyRegionCap rk (lift_ty k t1) (lift_ty k t2)
  | TyRegionCapPunched t1 t2 t3 =>
      TyRegionCapPunched (lift_ty k t1) (lift_ty k t2) (lift_ty k t3)
  | TyTensor t1 t2 =>
      TyTensor (lift_ty k t1) (lift_ty k t2)
  end.

Fixpoint subst_ty (t : ty) (k : nat) (u : ty) : ty :=
  match u with
  | TyVar x =>
      subst_var TyVar t k x
  | TyArrow u1 u2 =>
      TyArrow (subst_ty t k u1) (subst_ty t k u2)
  | TyPair layer1 layer2 u1 u2 =>
      TyPair layer1 layer2 (subst_ty t k u1) (subst_ty t k u2)
  | TyUnit layer =>
      TyUnit layer
  | TyQ q u =>
      TyQ q (subst_ty (lift_ty 0 t) (1 + k) u)
  | TyMu u =>
      TyMu (subst_ty (lift_ty 0 t) (1 + k) u)
  | TyBang u =>
      TyBang (subst_ty t k u)
  | TyRef u =>
      TyRef (subst_ty t k u)
  | TyRegion r =>
      TyRegion r
  | TyAt u =>
      TyAt (subst_ty t k u)
  | TyRegionCap rk u1 u2 =>
      TyRegionCap rk (subst_ty t k u1) (subst_ty t k u2)
  | TyRegionCapPunched u1 u2 u3 =>
      TyRegionCapPunched (subst_ty t k u1) (subst_ty t k u2) (subst_ty t k u3)
  | TyTensor u1 u2 =>
      TyTensor (subst_ty t k u1) (subst_ty t k u2)
  end.

De Bruijn lemmas.

Lemma subst_lift_ty:
subst_lift lift_ty subst_ty.

Proof.

subst_lift_tac.
Qed.

Local Hint Resolve subst_lift_ty.

Lemma lift_lift_ty:
lift_lift lift_ty.

Proof.

unfold lift_lift; intro a; induction a; intros; simpl in *; f_equal; eauto with lift_lift_db.
Qed.

Local Hint Resolve lift_lift_ty.

Lemma lift_zero_lift_ty:
lift_zero_lift lift_ty.

Proof.

lift_zero_lift_tac.
Qed.

Ltac lzl_ty :=
lzl lift_ty lift_zero_lift_ty.

Hint Extern 1 => lzl_ty : lift_subst_1_db.
Hint Extern 1 => lzl_ty : lift_subst_2_db.
Hint Extern 1 => lzl_ty : subst_subst_db.

Lemma lift_subst_1_ty:
lift_subst_1 lift_ty lift_ty subst_ty.

Proof.

lift_subst_1_tac.
Qed.

Local Hint Resolve lift_subst_1_ty.

Hint Extern 1 => rewrite lift_subst_1_ty; [ idtac | omega ] : subst_subst_db.

Lemma lift_subst_2_ty:
lift_subst_2 lift_ty lift_ty subst_ty.

Proof.

lift_subst_2_tac.
Qed.

Local Hint Resolve lift_subst_2_ty.

Lemma subst_subst_ty:
subst_subst lift_ty subst_ty subst_ty.

Proof.

subst_subst_tac.
Qed.

Local Hint Resolve subst_subst_ty.

Lemma pun_1_ty:
pun_1 TyVar lift_ty subst_ty.

Proof.

pun_tac.
Qed.

Lemma pun_2_ty:
pun_2 TyVar lift_ty subst_ty.

Proof.

pun_tac.
Qed.

Make the above two statements explicit for inclusion in the paper.

Lemma pun_1_ty_explicit:
forall T k, subst_ty (TyVar k) (S k) (lift_ty k T) = T.

Proof.

eauto using pun_1_ty.
Qed.

Lemma pun_2_ty_explicit:
forall T k, subst_ty (TyVar k) k (lift_ty (S k) T) = T.

Proof.

eauto using pun_2_ty.
Qed.

Lemma lift_ty_injective:
lift_injective lift_ty.

Proof.

lift_injective_tac.
Qed.

Definition rotate_ty : nat -> ty -> ty :=
  rotate TyVar lift_ty subst_ty.

Lemma rotate_ty_1_self_inverse:
  forall T,
  rotate_ty 1 (rotate_ty 1 T) = T.

Proof.

intro. unfold rotate_ty. eapply rotate1_self_inverse_holds; eauto using pun_2_ty.
Qed.