Type definitions and operations for CC.

inductive CC.TySort : Type

The sort of a type: capturing, shape, or existential.

• capt : TySort

  capturing types

• shape : TySort

  shape types

• exi : TySort

  existential types

inductive CC.CaptureBound : Sig → Type

A capture bound, either unbound or bounded by a capture set. It bounds capture set parameters.

• unbound {s : Sig} : CaptureBound s
• bound {s : Sig} : CaptureSet s → CaptureBound s

inductive CC.Ty : TySort → Sig → Type

A type in CC, indexed by its sort (capturing, shape, or existential).

• top {s : Sig} : Ty TySort.shape s
• tvar {s : Sig} : BVar s Kind.tvar → Ty TySort.shape s
• arrow {s : Sig} : Ty TySort.capt s → Ty TySort.exi (s,x) → Ty TySort.shape s
• poly {s : Sig} : Ty TySort.shape s → Ty TySort.exi (s,X) → Ty TySort.shape s
• cpoly {s : Sig} : CaptureBound s → Ty TySort.exi (s,C) → Ty TySort.shape s
• unit {s : Sig} : Ty TySort.shape s
• cap {s : Sig} : Ty TySort.shape s
• bool {s : Sig} : Ty TySort.shape s
• cell {s : Sig} : Ty TySort.shape s
• capt {s : Sig} : CaptureSet s → Ty TySort.shape s → Ty TySort.capt s
• exi {s : Sig} : Ty TySort.capt (s,C) → Ty TySort.exi s
• typ {s : Sig} : Ty TySort.capt s → Ty TySort.exi s

def CC.CaptureBound.rename {s1 s2 : Sig} : CaptureBound s1 → Rename s1 s2 → CaptureBound s2

Applies a renaming to a capture bound.

Equations

• CC.CaptureBound.unbound.rename x✝ = CC.CaptureBound.unbound
• (CC.CaptureBound.bound cs).rename x✝ = CC.CaptureBound.bound (cs.rename x✝)

def CC.CaptureBound.rename_id {s : Sig} {cb : CaptureBound s} : cb.rename Rename.id = cb

Renaming by the identity renaming leaves a capture bound unchanged.

Equations

• ⋯ = ⋯

theorem CC.CaptureBound.rename_comp {s1 s2 s3 : Sig} {cb : CaptureBound s1} {f : Rename s1 s2} {g : Rename s2 s3} : (cb.rename f).rename g = cb.rename (f.comp g)

Renaming distributes over composition of renamings.

def CC.Ty.rename {sort : TySort} {s1 s2 : Sig} : Ty sort s1 → Rename s1 s2 → Ty sort s2

Applies a renaming to all bound variables in a type.

Equations

• CC.Ty.top.rename x✝ = CC.Ty.top
• (CC.Ty.tvar x_2).rename x✝ = CC.Ty.tvar (x✝.var x_2)
• (T1.arrow T2).rename x✝ = (T1.rename x✝).arrow (T2.rename x✝.lift)
• (T1.poly T2).rename x✝ = (T1.rename x✝).poly (T2.rename x✝.lift)
• (CC.Ty.cpoly cb T).rename x✝ = CC.Ty.cpoly (cb.rename x✝) (T.rename x✝.lift)
• CC.Ty.unit.rename x✝ = CC.Ty.unit
• CC.Ty.cap.rename x✝ = CC.Ty.cap
• CC.Ty.bool.rename x✝ = CC.Ty.bool
• CC.Ty.cell.rename x✝ = CC.Ty.cell
• (CC.Ty.capt cs T).rename x✝ = CC.Ty.capt (cs.rename x✝) (T.rename x✝)
• T.exi.rename x✝ = (T.rename x✝.lift).exi
• T.typ.rename x✝ = (T.rename x✝).typ

def CC.Ty.rename_id {sort : TySort} {s : Sig} {T : Ty sort s} : T.rename Rename.id = T

Renaming by the identity renaming leaves a type unchanged.

Equations

• ⋯ = ⋯

theorem CC.Ty.rename_comp {sort : TySort} {s1 s2 s3 : Sig} {T : Ty sort s1} {f : Rename s1 s2} {g : Rename s2 s3} : (T.rename f).rename g = T.rename (f.comp g)

Renaming distributes over composition of renamings.

theorem CC.Ty.weaken_rename_comm {sort : TySort} {s1 s2 : Sig} {k0 : Kind} {T : Ty sort s1} {f : Rename s1 s2} : (T.rename Rename.succ).rename f.lift = (T.rename f).rename Rename.succ

Weakening commutes with renaming under a binder.

def CC.Ty.captureSet {s : Sig} : Ty TySort.capt s → CaptureSet s

Extracts the capture set from a capturing type.

Equations

• (CC.Ty.capt C a).captureSet = C

inductive CC.CaptureBound.IsClosed {s : Sig} : CaptureBound s → Prop

A capture bound is closed if it contains no heap pointers.

• unbound {s : Sig} : CaptureBound.unbound.IsClosed
• bound {s : Sig} {cs : CaptureSet s} : cs.IsClosed → (CaptureBound.bound cs).IsClosed

inductive CC.Ty.IsClosed {sort : TySort} {s : Sig} : Ty sort s → Prop

A type is closed if it contains no heap pointers.

• top {x✝ : Sig} : Ty.top.IsClosed
• tvar {x✝ : Sig} {x : BVar x✝ Kind.tvar} : (Ty.tvar x).IsClosed
• arrow {x✝ : Sig} {T1 : Ty TySort.capt x✝} {T2 : Ty TySort.exi (x✝,x)} : T1.IsClosed → T2.IsClosed → (T1.arrow T2).IsClosed
• poly {x✝ : Sig} {T1 : Ty TySort.shape x✝} {T2 : Ty TySort.exi (x✝,X)} : T1.IsClosed → T2.IsClosed → (T1.poly T2).IsClosed
• cpoly {x✝ : Sig} {cb : CaptureBound x✝} {T : Ty TySort.exi (x✝,C)} : cb.IsClosed → T.IsClosed → (Ty.cpoly cb T).IsClosed
• unit {x✝ : Sig} : Ty.unit.IsClosed
• cap {x✝ : Sig} : Ty.cap.IsClosed
• bool {x✝ : Sig} : Ty.bool.IsClosed
• cell {x✝ : Sig} : Ty.cell.IsClosed
• capt {x✝ : Sig} {cs : CaptureSet x✝} {S : Ty TySort.shape x✝} : cs.IsClosed → S.IsClosed → (Ty.capt cs S).IsClosed
• exi {x✝ : Sig} {T : Ty TySort.capt (x✝,C)} : T.IsClosed → T.exi.IsClosed
• typ {x✝ : Sig} {T : Ty TySort.capt x✝} : T.IsClosed → T.typ.IsClosed