Expression definitions and operations for CC.

inductive CC.Exp : Sig → Type

An expression in CC.

• var {s : Sig} : Var Kind.var s → Exp s
• abs {s : Sig} : CaptureSet s → Ty TySort.capt s → Exp (s,x) → Exp s
• tabs {s : Sig} : CaptureSet s → Ty TySort.shape s → Exp (s,X) → Exp s
• cabs {s : Sig} : CaptureSet s → CaptureBound s → Exp (s,C) → Exp s
• pack {s : Sig} : CaptureSet s → Var Kind.var s → Exp s
• app {s : Sig} : Var Kind.var s → Var Kind.var s → Exp s
• tapp {s : Sig} : Var Kind.var s → Ty TySort.shape s → Exp s
• capp {s : Sig} : Var Kind.var s → CaptureSet s → Exp s
• letin {s : Sig} : Exp s → Exp (s,x) → Exp s
• unpack {s : Sig} : Exp s → Exp (s,C,x) → Exp s
• unit {s : Sig} : Exp s
• btrue {s : Sig} : Exp s
• bfalse {s : Sig} : Exp s
• read {s : Sig} : Var Kind.var s → Exp s
• write {s : Sig} : Var Kind.var s → Var Kind.var s → Exp s
• cond {s : Sig} : Var Kind.var s → Exp s → Exp s → Exp s

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

Applies a renaming to all bound variables in an expression.

Equations

• (CC.Exp.var x_2).rename x✝ = CC.Exp.var (x_2.rename x✝)
• (CC.Exp.abs cs T e).rename x✝ = CC.Exp.abs (cs.rename x✝) (T.rename x✝) (e.rename x✝.lift)
• (CC.Exp.tabs cs T e).rename x✝ = CC.Exp.tabs (cs.rename x✝) (T.rename x✝) (e.rename x✝.lift)
• (CC.Exp.cabs cs cb e).rename x✝ = CC.Exp.cabs (cs.rename x✝) (cb.rename x✝) (e.rename x✝.lift)
• (CC.Exp.pack cs x_2).rename x✝ = CC.Exp.pack (cs.rename x✝) (x_2.rename x✝)
• (CC.Exp.app x_2 y).rename x✝ = CC.Exp.app (x_2.rename x✝) (y.rename x✝)
• (CC.Exp.tapp x_2 T).rename x✝ = CC.Exp.tapp (x_2.rename x✝) (T.rename x✝)
• (CC.Exp.capp x_2 cs).rename x✝ = CC.Exp.capp (x_2.rename x✝) (cs.rename x✝)
• (e1.letin e2).rename x✝ = (e1.rename x✝).letin (e2.rename x✝.lift)
• (e1.unpack e2).rename x✝ = (e1.rename x✝).unpack (e2.rename x✝.lift.lift)
• CC.Exp.unit.rename x✝ = CC.Exp.unit
• CC.Exp.btrue.rename x✝ = CC.Exp.btrue
• CC.Exp.bfalse.rename x✝ = CC.Exp.bfalse
• (CC.Exp.read x_2).rename x✝ = CC.Exp.read (x_2.rename x✝)
• (CC.Exp.write x_2 y).rename x✝ = CC.Exp.write (x_2.rename x✝) (y.rename x✝)
• (CC.Exp.cond x_2 e2 e3).rename x✝ = CC.Exp.cond (x_2.rename x✝) (e2.rename x✝) (e3.rename x✝)

inductive CC.Exp.IsVal {s : Sig} : Exp s → Prop

An expression is a value if it is an abstraction, pack, or unit.

• abs {s : Sig} {cs : CaptureSet s} {T : Ty TySort.capt s} {e : Exp (s,x)} : (Exp.abs cs T e).IsVal
• tabs {s : Sig} {cs : CaptureSet s} {T : Ty TySort.shape s} {e : Exp (s,X)} : (Exp.tabs cs T e).IsVal
• cabs {s : Sig} {cs : CaptureSet s} {cb : CaptureBound s} {e : Exp (s,C)} : (Exp.cabs cs cb e).IsVal
• pack {s : Sig} {cs : CaptureSet s} {x : Var Kind.var s} : (Exp.pack cs x).IsVal
• unit {s : Sig} : Exp.unit.IsVal
• btrue {s : Sig} : Exp.btrue.IsVal
• bfalse {s : Sig} : Exp.bfalse.IsVal

inductive CC.Exp.IsSimpleVal {s : Sig} : Exp s → Prop

A simple value is a value that is not a pack. Therefore, a simple value always has a capturing type, not an existential type.

• abs {s : Sig} {cs : CaptureSet s} {T : Ty TySort.capt s} {e : Exp (s,x)} : (Exp.abs cs T e).IsSimpleVal
• tabs {s : Sig} {cs : CaptureSet s} {T : Ty TySort.shape s} {e : Exp (s,X)} : (Exp.tabs cs T e).IsSimpleVal
• cabs {s : Sig} {cs : CaptureSet s} {cb : CaptureBound s} {e : Exp (s,C)} : (Exp.cabs cs cb e).IsSimpleVal
• unit {s : Sig} : Exp.unit.IsSimpleVal
• btrue {s : Sig} : Exp.btrue.IsSimpleVal
• bfalse {s : Sig} : Exp.bfalse.IsSimpleVal

inductive CC.Exp.IsSimpleAns {s : Sig} : Exp s → Prop

• is_simple_val {s : Sig} {v : Exp s} (hv : v.IsSimpleVal) : v.IsSimpleAns
• is_var {s : Sig} {x : Var Kind.var s} : (var x).IsSimpleAns

inductive CC.Exp.IsPack {s : Sig} : Exp s → Prop

• pack {s : Sig} {cs : CaptureSet s} {x : Var Kind.var s} : (Exp.pack cs x).IsPack

structure CC.Val (s : Sig) : Type

A value, bundling an expression with a proof that it is a value.

• unwrap : Exp s
• isVal : self.unwrap.IsVal

def CC.Var.rename_id {k : Kind} {s : Sig} {x : Var k s} : x.rename Rename.id = x

Renaming by the identity renaming leaves a variable unchanged.

Equations

• ⋯ = ⋯

def CC.Exp.rename_id {s : Sig} {e : Exp s} : e.rename Rename.id = e

Renaming by the identity renaming leaves an expression unchanged.

Equations

• ⋯ = ⋯

theorem CC.Var.rename_comp {k : Kind} {s1 s2 s3 : Sig} {x : Var k s1} {f : Rename s1 s2} {g : Rename s2 s3} : (x.rename f).rename g = x.rename (f.comp g)

Renaming distributes over composition of renamings.

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

Renaming distributes over composition of renamings.

theorem CC.Var.weaken_rename_comm {k : Kind} {s1 s2 : Sig} {k0 : Kind} {x : Var k s1} {f : Rename s1 s2} : (x.rename Rename.succ).rename f.lift = (x.rename f).rename Rename.succ

Weakening commutes with renaming under a binder.

inductive CC.Exp.IsAns : Exp ∅ → Prop

An answer is a value or a free variable in the empty context.

• is_val {v : Exp ∅} (hv : v.IsVal) : v.IsAns
• is_var {x : Var Kind.var ∅} : (var x).IsAns

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

An expression is closed if it contains no heap pointers.

• var {s : Sig} {x : Var Kind.var s} : x.IsClosed → (Exp.var x).IsClosed
• abs {s : Sig} {cs : CaptureSet s} {T : Ty TySort.capt s} {e : Exp (s,x)} : cs.IsClosed → T.IsClosed → e.IsClosed → (Exp.abs cs T e).IsClosed
• tabs {s : Sig} {cs : CaptureSet s} {T : Ty TySort.shape s} {e : Exp (s,X)} : cs.IsClosed → T.IsClosed → e.IsClosed → (Exp.tabs cs T e).IsClosed
• cabs {s : Sig} {cs : CaptureSet s} {cb : CaptureBound s} {e : Exp (s,C)} : cs.IsClosed → cb.IsClosed → e.IsClosed → (Exp.cabs cs cb e).IsClosed
• pack {s : Sig} {cs : CaptureSet s} {x : Var Kind.var s} : cs.IsClosed → x.IsClosed → (Exp.pack cs x).IsClosed
• app {s : Sig} {x y : Var Kind.var s} : x.IsClosed → y.IsClosed → (Exp.app x y).IsClosed
• tapp {s : Sig} {x : Var Kind.var s} {T : Ty TySort.shape s} : x.IsClosed → T.IsClosed → (Exp.tapp x T).IsClosed
• capp {s : Sig} {x : Var Kind.var s} {cs : CaptureSet s} : x.IsClosed → cs.IsClosed → (Exp.capp x cs).IsClosed
• letin {s : Sig} {e1 : Exp s} {e2 : Exp (s,x)} : e1.IsClosed → e2.IsClosed → (e1.letin e2).IsClosed
• unpack {s : Sig} {e1 : Exp s} {e2 : Exp (s,C,x)} : e1.IsClosed → e2.IsClosed → (e1.unpack e2).IsClosed
• unit {s : Sig} : Exp.unit.IsClosed
• btrue {s : Sig} : Exp.btrue.IsClosed
• bfalse {s : Sig} : Exp.bfalse.IsClosed
• read {s : Sig} {x : Var Kind.var s} : x.IsClosed → (Exp.read x).IsClosed
• write {s : Sig} {x y : Var Kind.var s} : x.IsClosed → y.IsClosed → (Exp.write x y).IsClosed
• cond {s : Sig} {x : Var Kind.var s} {e2 e3 : Exp s} : x.IsClosed → e2.IsClosed → e3.IsClosed → (Exp.cond x e2 e3).IsClosed