Documentation

Semantic.CC.Syntax.CaptureSet

This module defines the capture set syntax of CC.

inductive CC.Var :

Kind → Sig → Type

A variable, either bound (de Bruijn indexed) or free (heap pointer).

bound {s : Sig} {k : Kind} : BVar s k → Var k s
free {k : Kind} {s : Sig} : ℕ → Var k s

Instances For

inductive CC.CaptureSet :

A set of captured variables.

empty {s : Sig} : CaptureSet s
union {s : Sig} : CaptureSet s → CaptureSet s → CaptureSet s
var {s : Sig} : Var Kind.var s → CaptureSet s
cvar {s : Sig} : BVar s Kind.cvar → CaptureSet s

Instances For

instance CC.CaptureSet.instEmptyCollection {s : Sig} :

EmptyCollection (CaptureSet s)

Provides {} notation for the empty capture set.

Equations

CC.CaptureSet.instEmptyCollection = { emptyCollection := CC.CaptureSet.empty }

instance CC.CaptureSet.instUnion {s : Sig} :

Union (CaptureSet s)

Provides ∪ notation for capture set union.

Equations

CC.CaptureSet.instUnion = { union := CC.CaptureSet.union }

def CC.Var.rename {k : Kind} {s1 s2 : Sig} :

Var k s1 → Rename s1 s2 → Var k s2

Applies a renaming to a variable. Free variables remain unchanged.

Equations

(CC.Var.bound x_2).rename x✝ = CC.Var.bound (x✝.var x_2)
(CC.Var.free n).rename x✝ = CC.Var.free n

Instances For

def CC.CaptureSet.rename {s1 s2 : Sig} :

CaptureSet s1 → Rename s1 s2 → CaptureSet s2

Applies a renaming to all bound variables in a capture set.

Equations

CC.CaptureSet.empty.rename x✝ = CC.CaptureSet.empty
(cs1.union cs2).rename x✝ = (cs1.rename x✝).union (cs2.rename x✝)
(CC.CaptureSet.var x_2).rename x✝ = CC.CaptureSet.var (x_2.rename x✝)
(CC.CaptureSet.cvar x_2).rename x✝ = CC.CaptureSet.cvar (x✝.var x_2)

Instances For

theorem CC.CaptureSet.rename_id {s : Sig} {cs : CaptureSet s} :

cs.rename Rename.id = cs

Renaming by the identity renaming leaves a capture set unchanged.

theorem CC.CaptureSet.rename_comp {s1 s2 s3 : Sig} {cs : CaptureSet s1} {f : Rename s1 s2} {g : Rename s2 s3} :

(cs.rename f).rename g = cs.rename (f.comp g)

Renaming distributes over composition of renamings.

inductive CC.CaptureSet.Subset {s : Sig} :

CaptureSet s → CaptureSet s → Prop

The subset relation on capture sets.

refl {s : Sig} {C : CaptureSet s} : C.Subset C
union_left {s : Sig} {C1 C C2 : CaptureSet s} : C1.Subset C → C2.Subset C → (C1.union C2).Subset C
union_right_left {s : Sig} {C C1 C2 : CaptureSet s} : C.Subset C1 → C.Subset (C1.union C2)
union_right_right {s : Sig} {C C2 C1 : CaptureSet s} : C.Subset C2 → C.Subset (C1.union C2)

Instances For

instance CC.CaptureSet.instHasSubset {s : Sig} :

HasSubset (CaptureSet s)

Provides ⊆ notation for capture set subset.

Equations

CC.CaptureSet.instHasSubset = { Subset := CC.CaptureSet.Subset }

inductive CC.Var.IsClosed {k : Kind} {s : Sig} :

Var k s → Prop

A variable is closed if it contains no heap pointers.

bound {k : Kind} {s : Sig} {x : BVar s k} : (Var.bound x).IsClosed

Instances For

inductive CC.CaptureSet.IsClosed {s : Sig} :

CaptureSet s → Prop

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

empty {s : Sig} : CaptureSet.empty.IsClosed
union {s : Sig} {cs1 cs2 : CaptureSet s} : cs1.IsClosed → cs2.IsClosed → (cs1.union cs2).IsClosed
cvar {s : Sig} {x : BVar s Kind.cvar} : (CaptureSet.cvar x).IsClosed
var_bound {s : Sig} {x : BVar s Kind.var} : (var (Var.bound x)).IsClosed

Instances For