Closure conversion

InductiveSource values of closure conversion#✓fully proved

A source value is a closure of a raw term \(b\) (the body of a lambda) over an environment \(\rho\), which is a list of source values.

inductive Value (Base : Type u) where
  | clo : Stlc.RawTm Base → List (Value Base) → Value Base

Uses 1 · Used by 14

Statement usesRaw lambda terms

Used byAccessors implementing a source environment · Code accessors implement the extended closure environment · Correctness of closure conversion in the empty environment · Correctness of flat closure conversion for closed programs · Correctness of closure conversion · Correctness of flat closure conversion · Source evaluation is deterministic · Packed accessors evaluate to an encoded related environment · Big-step semantics of the closure-conversion source · Evaluating a flat environment · Accessors implementing the free variables of a term · Flat accessors implement the variables of a closure body · Flat value relation · Value relation for closure conversion

InductiveBig-step semantics of the closure-conversion source#✓fully proved

Evaluation \(\rho \vdash t \Downarrow v\) of a raw term \(t\) to a source value \(v\) in an environment \(\rho\) (a list of source values, where variable \(n\) refers to the entry of \(\rho\) at index \(n\), counting from \(0\)) is the least relation closed under the following rules, a call-by-value environment semantics that ignores the type annotations of lambdas. A variable \(n\) evaluates to the entry of \(\rho\) at index \(n\), when that entry exists. A lambda \(\lambda. b\) evaluates to the closure of \(b\) over \(\rho\). If \(f\) evaluates in \(\rho\) to the closure of \(b\) over \(\rho'\), if \(\rho \vdash a \Downarrow v\), and if \(v :: \rho' \vdash b \Downarrow w\), where \(v :: \rho'\) is \(\rho'\) with \(v\) added at index \(0\), then \(\rho \vdash f\,a \Downarrow w\).

inductive Eval : List (Value Base) → Stlc.RawTm Base → Value Base → Prop
  | var {ρ : List (Value Base)} {n : Nat} {v : Value Base} (h : ρ[n]? = some v) :
      Eval ρ (.var n) v
  | lam {ρ : List (Value Base)} {A : Stlc.Ty Base} {body : Stlc.RawTm Base} :
      Eval ρ (.lam A body) (.clo body ρ)
  | app {ρ ρ' : List (Value Base)} {f a body : Stlc.RawTm Base} {v w : Value Base}
      (hf : Eval ρ f (.clo body ρ')) (ha : Eval ρ a v) (hbody : Eval (v :: ρ') body w) :
      Eval ρ (.app f a) w

Uses 3 · Used by 5

Statement usesSource values of closure conversion · Raw lambda terms · Simple types

Used byCorrectness of closure conversion in the empty environment · Correctness of flat closure conversion for closed programs · Correctness of closure conversion · Correctness of flat closure conversion · Source evaluation is deterministic

TheoremSource evaluation is deterministic#✓fully proved

For every environment \(\rho\) of source values and every raw term \(t\), if \(t\) evaluates in \(\rho\) to source values \(v\) and \(w\), then \(v = w\).

theorem Eval.deterministic {ρ : List (Value Base)} {t : Stlc.RawTm Base} {v w : Value Base}
    (hv : Eval ρ t v) (hw : Eval ρ t w) : v = w

Uses 4

Statement usesBig-step semantics of the closure-conversion source · Source values of closure conversion · Raw lambda terms

Proof usesSimple types

InductiveTarget terms of closure conversion#✓fully proved

The terms of the closure-conversion target language, with variables as de Bruijn indices, are: a variable \(n\) for each natural number \(n\); code \(\mathsf{code}\,b\) of one parameter, whose body \(b\) is evaluated with only its parameter in scope, as variable \(0\); application \(f\,a\) of code to an argument; the unit term \(\mathsf{unit}\) (the empty tuple); pairs \((a, b)\); the projections \(\mathsf{fst}\,e\) and \(\mathsf{snd}\,e\); and \(\mathsf{let}\ e\ \mathsf{in}\ b\), which binds the value of \(e\) as variable \(0\) in \(b\).

Cslib.Languages.LambdaCalculus.ClosureConversion.Target.Tm · 18 lines

inductive Tm where
  /-- A de Bruijn variable. -/
  | var : Nat → Tm
  /-- Closed code of one parameter; the body sees only variable `0`. -/
  | code : Tm → Tm
  /-- Call code with an argument. -/
  | app : Tm → Tm → Tm
  /-- The empty tuple. -/
  | unit : Tm
  /-- Pairing. -/
  | pair : Tm → Tm → Tm
  /-- First projection. -/
  | fst : Tm → Tm
  /-- Second projection. -/
  | snd : Tm → Tm
  /-- `letIn e b` evaluates `e` and binds it as variable `0` in `b`. -/
  | letIn : Tm → Tm → Tm
  deriving DecidableEq, Repr

Used by 35

Used byAccessors implementing a source environment · Code accessors implement the extended closure environment · Closure conversion of a program · Correctness of closure conversion in the empty environment · Flat closure conversion of a program · Correctness of flat closure conversion for closed programs · Flat closure conversion of a closed term is well scoped · Closure conversion of a closed term is well scoped · Accessors inside converted code · Closure conversion with accessors · Correctness of closure conversion · Flat closure conversion · Correctness of flat closure conversion · Flat closure conversion preserves scoping · Converted terms are well scoped · Flat closure environment · Length of an evaluated flat environment · Environment-packing term · Packed accessors evaluate to an encoded related environment · Big-step semantics of the closure-conversion target · Evaluating a flat environment · Iterated second projections of an encoded environment · Accessors inside flat code · Accessors implementing the free variables of a term · Flat accessors implement the variables of a closure body · Flat value relation · Renaming target terms · Evaluation is stable under renaming · Well-scoped target terms · Shifting a target term · Evaluation of a shifted term · Shifting preserves scoping · Iterated second projection · Value relation for closure conversion · Target values of closure conversion

InductiveTarget values of closure conversion#✓fully proved

A value of the closure-conversion target language is code \(\mathsf{code}\,b\) for a target term \(b\), the unit value \(\mathsf{unit}\), or a pair \((v, w)\) of values.

inductive Value where
  | code : Tm → Value
  | unit : Value
  | pair : Value → Value → Value
  deriving DecidableEq, Repr

Uses 1 · Used by 18

Statement usesTarget terms of closure conversion

Used byAccessors implementing a source environment · Code accessors implement the extended closure environment · Correctness of closure conversion in the empty environment · Correctness of flat closure conversion for closed programs · Correctness of closure conversion · Correctness of flat closure conversion · Encoding a list of target values · Length of an evaluated flat environment · Packed accessors evaluate to an encoded related environment · Big-step semantics of the closure-conversion target · Evaluating a flat environment · Iterated second projections of an encoded environment · Accessors implementing the free variables of a term · Flat accessors implement the variables of a closure body · Flat value relation · Evaluation is stable under renaming · Evaluation of a shifted term · Value relation for closure conversion

InductiveBig-step semantics of the closure-conversion target#✓fully proved

Evaluation \(\rho \vdash e \Downarrow v\) of a target term \(e\) to a target value \(v\) in an environment \(\rho\) (a list of values, where variable \(n\) refers to the entry of \(\rho\) at index \(n\), counting from \(0\)) is the least relation closed under the following rules. A variable \(n\) evaluates to the entry of \(\rho\) at index \(n\), when that entry exists. Code evaluates to itself: \(\rho \vdash \mathsf{code}\,b \Downarrow \mathsf{code}\,b\). If \(\rho \vdash f \Downarrow \mathsf{code}\,b\), \(\rho \vdash a \Downarrow v\) and \([v] \vdash b \Downarrow w\), then \(\rho \vdash f\,a \Downarrow w\); so a code body runs in the one-element environment \([v]\) and never sees \(\rho\). The unit term evaluates to the unit value. If \(\rho \vdash a \Downarrow v\) and \(\rho \vdash b \Downarrow w\), then \(\rho \vdash (a, b) \Downarrow (v, w)\). If \(\rho \vdash e \Downarrow (v, w)\), then \(\rho \vdash \mathsf{fst}\,e \Downarrow v\) and \(\rho \vdash \mathsf{snd}\,e \Downarrow w\). If \(\rho \vdash e \Downarrow v\) and \(v :: \rho \vdash b \Downarrow w\), where \(v :: \rho\) is \(\rho\) with \(v\) added at index \(0\), then \(\rho \vdash \mathsf{let}\ e\ \mathsf{in}\ b \Downarrow w\).

inductive Eval : List Value → Tm → Value → Prop
  | var {ρ : List Value} {n : Nat} {v : Value} (h : ρ[n]? = some v) : Eval ρ (.var n) v
  | code {ρ : List Value} {b : Tm} : Eval ρ (.code b) (.code b)
  | app {ρ : List Value} {f a b : Tm} {v w : Value}
      (hf : Eval ρ f (.code b)) (ha : Eval ρ a v) (hb : Eval [v] b w) : Eval ρ (.app f a) w
  | unit {ρ : List Value} : Eval ρ .unit .unit
  | pair {ρ : List Value} {a b : Tm} {v w : Value}
      (ha : Eval ρ a v) (hb : Eval ρ b w) : Eval ρ (.pair a b) (.pair v w)
  | fst {ρ : List Value} {e : Tm} {v w : Value}
      (h : Eval ρ e (.pair v w)) : Eval ρ (.fst e) v
  | snd {ρ : List Value} {e : Tm} {v w : Value}
      (h : Eval ρ e (.pair v w)) : Eval ρ (.snd e) w
  | letIn {ρ : List Value} {e b : Tm} {v w : Value}
      (he : Eval ρ e v) (hb : Eval (v :: ρ) b w) : Eval ρ (.letIn e b) w

Uses 2 · Used by 14

Statement usesTarget terms of closure conversion · Target values of closure conversion

Used byAccessors implementing a source environment · Code accessors implement the extended closure environment · Correctness of closure conversion in the empty environment · Correctness of flat closure conversion for closed programs · Correctness of closure conversion · Correctness of flat closure conversion · Length of an evaluated flat environment · Packed accessors evaluate to an encoded related environment · Evaluating a flat environment · Iterated second projections of an encoded environment · Accessors implementing the free variables of a term · Flat accessors implement the variables of a closure body · Evaluation is stable under renaming · Evaluation of a shifted term

DefinitionLifting a renaming under a binder, for the closure-conversion target#✓fully proved

The lift \(r^{\uparrow}\) of a renaming \(r : \mathbb{N} \to \mathbb{N}\) of de Bruijn indices sends \(0\) to \(0\) and \(i + 1\) to \(r(i) + 1\).

def liftRen (r : Nat → Nat) : Nat → Nat
  | 0 => 0
  | i + 1 => r i + 1

Used by 3

Used byRenaming target terms · Evaluation is stable under renaming · Shifting preserves scoping

DefinitionRenaming target terms#✓fully proved

For \(r : \mathbb{N} \to \mathbb{N}\), the renaming \(t[r]\) of a target term \(t\) replaces each variable \(i\) by \(r(i)\), leaves code \(\mathsf{code}\,b\) unchanged (its body \(b\) is not renamed), fixes \(\mathsf{unit}\), commutes with application, pairing and the two projections, and sends \(\mathsf{let}\ e\ \mathsf{in}\ b\) to \(\mathsf{let}\ e[r]\ \mathsf{in}\ b[r^{\uparrow}]\), where \(r^{\uparrow}\), the lift of \(r\) under one binder, sends \(0\) to \(0\) and \(i + 1\) to \(r(i) + 1\).

def rename (r : Nat → Nat) : Tm → Tm
  | .var i => .var (r i)
  | .code b => .code b
  | .app f a => .app (rename r f) (rename r a)
  | .unit => .unit
  | .pair a b => .pair (rename r a) (rename r b)
  | .fst e => .fst (rename r e)
  | .snd e => .snd (rename r e)
  | .letIn e b => .letIn (rename r e) (rename (liftRen r) b)

Uses 2 · Used by 3

Statement usesTarget terms of closure conversion · Lifting a renaming under a binder, for the closure-conversion target

Used byEvaluation is stable under renaming · Shifting a target term · Shifting preserves scoping

DefinitionShifting a target term#✓fully proved

The shift of a target term \(e\) is its renaming by the successor map \(i \mapsto i + 1\): every free variable of \(e\) goes up by one, and code bodies are left unchanged.

def shift (e : Tm) : Tm := rename Nat.succ e

Uses 2 · Used by 8

Statement usesTarget terms of closure conversion · Renaming target terms

Used byClosure conversion with accessors · Correctness of closure conversion · Flat closure conversion · Correctness of flat closure conversion · Flat closure conversion preserves scoping · Converted terms are well scoped · Evaluation of a shifted term · Shifting preserves scoping

TheoremEvaluation is stable under renaming#✓fully proved

Let \(\rho\) and \(\rho'\) be environments and \(r : \mathbb{N} \to \mathbb{N}\) a renaming such that, for every index \(i\) and value \(w\), if \(\rho\) has entry \(w\) at index \(i\) then \(\rho'\) has entry \(w\) at index \(r(i)\). If a target term \(e\) evaluates to \(v\) in \(\rho\), then the renaming of \(e\) by \(r\) evaluates to \(v\) in \(\rho'\).

theorem Eval.rename {ρ ρ' : List Value} {e : Tm} {v : Value} (h : Eval ρ e v)
    {r : Nat → Nat} (hr : ∀ i w, ρ[i]? = some w → ρ'[r i]? = some w) :
    Eval ρ' (e.rename r) v

Uses 5 · Used by 1

Statement usesTarget terms of closure conversion · Big-step semantics of the closure-conversion target · Renaming target terms · Target values of closure conversion

Proof usesLifting a renaming under a binder, for the closure-conversion target

Used byEvaluation of a shifted term

TheoremEvaluation of a shifted term#✓fully proved

If a target term \(e\) evaluates to \(v\) in an environment \(\rho\), then for every value \(x\) the shift of \(e\) evaluates to \(v\) in the environment \(x :: \rho\) obtained from \(\rho\) by adding \(x\) at index \(0\).

theorem Eval.shift {ρ : List Value} {e : Tm} {v : Value} (x : Value) (h : Eval ρ e v) :
    Eval (x :: ρ) e.shift v

Uses 5 · Used by 2

Statement usesTarget terms of closure conversion · Big-step semantics of the closure-conversion target · Shifting a target term · Target values of closure conversion

Proof usesEvaluation is stable under renaming

Used byCorrectness of closure conversion · Correctness of flat closure conversion

InductiveWell-scoped target terms#✓fully proved

For a natural number \(m\), a target term \(e\) is scoped in \(m\) when every free variable of \(e\) is less than \(m\) and every code body in \(e\) is closed, that is, scoped in \(1\). Inductively: a variable \(i\) is scoped in \(m\) when \(i < m\); \(\mathsf{code}\,b\) is scoped in every \(m\) when \(b\) is scoped in \(1\); \(\mathsf{unit}\) is scoped in every \(m\); an application, a pair or a projection is scoped in \(m\) when its immediate subterms are; and \(\mathsf{let}\ e\ \mathsf{in}\ b\) is scoped in \(m\) when \(e\) is scoped in \(m\) and \(b\) is scoped in \(m + 1\).

inductive Scoped : Nat → Tm → Prop
  | var {m i : Nat} (h : i < m) : Scoped m (.var i)
  | code {m : Nat} {b : Tm} (hb : Scoped 1 b) : Scoped m (.code b)
  | app {m : Nat} {f a : Tm} (hf : Scoped m f) (ha : Scoped m a) : Scoped m (.app f a)
  | unit {m : Nat} : Scoped m .unit
  | pair {m : Nat} {a b : Tm} (ha : Scoped m a) (hb : Scoped m b) : Scoped m (.pair a b)
  | fst {m : Nat} {e : Tm} (h : Scoped m e) : Scoped m (.fst e)
  | snd {m : Nat} {e : Tm} (h : Scoped m e) : Scoped m (.snd e)
  | letIn {m : Nat} {e b : Tm} (he : Scoped m e) (hb : Scoped (m + 1) b) :
      Scoped m (.letIn e b)

Uses 1 · Used by 5

Statement usesTarget terms of closure conversion

Used byFlat closure conversion of a closed term is well scoped · Closure conversion of a closed term is well scoped · Flat closure conversion preserves scoping · Converted terms are well scoped · Shifting preserves scoping

TheoremShifting preserves scoping#✓fully proved

If a target term \(e\) is scoped in \(m\), then its shift is scoped in \(m + 1\).

theorem Scoped.shift {m : Nat} {e : Tm} (h : Scoped m e) : Scoped (m + 1) e.shift

Uses 5 · Used by 2

Statement usesTarget terms of closure conversion · Well-scoped target terms · Shifting a target term

Proof usesLifting a renaming under a binder, for the closure-conversion target · Renaming target terms

Used byFlat closure conversion preserves scoping · Converted terms are well scoped

DefinitionIterated second projection#✓fully proved

For a natural number \(k\) and a target term \(e\), the term \(\mathsf{snd}^k\,e\) applies the second projection \(k\) times to \(e\): \(\mathsf{snd}^0\,e = e\) and \(\mathsf{snd}^{k+1}\,e = \mathsf{snd}\,(\mathsf{snd}^k\,e)\).

def snds : Nat → Tm → Tm
  | 0, e => e
  | k + 1, e => .snd (snds k e)

Uses 1 · Used by 7

Statement usesTarget terms of closure conversion

Used byCode accessors implement the extended closure environment · Accessors inside converted code · Flat closure conversion preserves scoping · Converted terms are well scoped · Iterated second projections of an encoded environment · Accessors inside flat code · Flat accessors implement the variables of a closure body

DefinitionEnvironment-packing term#✓fully proved

For a map \(\mathit{acc}\) from natural numbers to target terms and a natural number \(n\), the environment-packing term of \(\mathit{acc}\) and \(n\) is the target term \((\mathit{acc}(0), (\mathit{acc}(1), \dots (\mathit{acc}(n - 1), \mathsf{unit})\dots))\) packing \(\mathit{acc}(0), \dots, \mathit{acc}(n - 1)\) as nested pairs ending in \(\mathsf{unit}\). Recursively, it is \(\mathsf{unit}\) for \(n = 0\), and for \(n + 1\) it is the pair of \(\mathit{acc}(0)\) and the environment-packing term of \(i \mapsto \mathit{acc}(i + 1)\) and \(n\).

def envOf (acc : Nat → Tm) : Nat → Tm
  | 0 => .unit
  | n + 1 => .pair (acc 0) (envOf (fun i => acc (i + 1)) n)

Uses 1 · Used by 4

Statement usesTarget terms of closure conversion

Used byClosure conversion with accessors · Correctness of closure conversion · Converted terms are well scoped · Packed accessors evaluate to an encoded related environment

DefinitionAccessors inside converted code#✓fully proved

Write \(\#0\) for the target variable \(0\) and \(\mathsf{snd}^i\) for \(i\) applications of the second projection. The code accessor for index \(0\) is \(\mathsf{fst}\,\#0\), and the code accessor for index \(i + 1\) is \(\mathsf{fst}\,(\mathsf{snd}^i\,(\mathsf{snd}\,\#0))\). When the code parameter \(\#0\) is the pair of the argument and an environment encoded as nested pairs, accessor \(0\) fetches the argument and accessor \(i + 1\) fetches entry \(i\) of the environment.

def codeAcc : Nat → Tm
  | 0 => .fst (.var 0)
  | i + 1 => .fst (snds i (.snd (.var 0)))

Uses 2 · Used by 5

Statement usesTarget terms of closure conversion · Iterated second projection

Used byCode accessors implement the extended closure environment · Closure conversion with accessors · Correctness of closure conversion · Converted terms are well scoped · Value relation for closure conversion

DefinitionClosure conversion with accessors#✓fully proved

Let \(\mathit{acc}\) be a family of target terms indexed by the natural numbers (accessor \(i\) fetches source variable \(i\)) and \(n\) a natural number (the number of source variables in scope). The conversion \(\mathcal{C}(\mathit{acc}, n, t)\) of a source term \(t\) is defined by recursion on \(t\). A variable \(i\) converts to \(\mathit{acc}(i)\). A lambda with body \(b\) (whatever its parameter type) converts to the pair of \(\mathsf{code}\,\mathcal{C}(c, n + 1, b)\), where \(c\) is the family of code accessors, and the target term packing \(\mathit{acc}(0), \dots, \mathit{acc}(n - 1)\) as nested pairs ending in \(\mathsf{unit}\). An application \(f\,a\) converts to \(\mathsf{let}\ \mathcal{C}(\mathit{acc}, n, f)\ \mathsf{in}\ (\mathsf{fst}\,\#0)\, (\mathcal{C}(\mathit{acc}', n, a), \mathsf{snd}\,\#0)\), where \(\#0\) is the target variable \(0\) and \(\mathit{acc}'(i)\) is the shift of \(\mathit{acc}(i)\) for every \(i\).

def convert : (Nat → Tm) → Nat → Stlc.RawTm Base → Tm
  | acc, _, .var i => acc i
  | acc, n, .lam _ body => .pair (.code (convert codeAcc (n + 1) body)) (envOf acc n)
  | acc, n, .app f a =>
      .letIn (convert acc n f)
        (.app (.fst (.var 0)) (.pair (convert (fun i => (acc i).shift) n a) (.snd (.var 0))))

Uses 6 · Used by 4

Statement usesTarget terms of closure conversion · Shifting a target term · Accessors inside converted code · Environment-packing term · Raw lambda terms · Simple types

Used byClosure conversion of a program · Correctness of closure conversion · Converted terms are well scoped · Value relation for closure conversion

DefinitionClosure conversion of a program#✓fully proved

The closure conversion of a source term \(t\) is the conversion of \(t\) in a scope of \(0\) variables with the accessors that send each index \(i\) to the target variable \(i\). It is intended for closed terms.

def closureConvert (t : Stlc.RawTm Base) : Tm :=
  convert .var 0 t

Uses 3 · Used by 2

Statement usesTarget terms of closure conversion · Closure conversion with accessors · Raw lambda terms

Used byCorrectness of closure conversion in the empty environment · Closure conversion of a closed term is well scoped

DefinitionEncoding a list of target values#✓fully proved

The encoding of a list of target values as nested pairs sends the empty list to the unit value and a list with head \(w\) and tail \(ws\) to the pair of \(w\) and the encoding of \(ws\). Thus \([w_0, \dots, w_{k-1}]\) is encoded as \((w_0, (w_1, \dots (w_{k-1}, \mathsf{unit})))\).

def encodeEnv : List Value → Value
  | [] => .unit
  | w :: ws => .pair w (encodeEnv ws)

Uses 1 · Used by 10

Statement usesTarget values of closure conversion

Used byCode accessors implement the extended closure environment · Correctness of closure conversion · Correctness of flat closure conversion · Length of an evaluated flat environment · Packed accessors evaluate to an encoded related environment · Evaluating a flat environment · Iterated second projections of an encoded environment · Flat accessors implement the variables of a closure body · Flat value relation · Value relation for closure conversion

InductiveValue relation for closure conversion#✓fully proved

The relation between source values and target values of closure conversion is the least relation such that, for every source lambda body \(b\), every list \(\rho\) of source values and every list \(ws\) of target values with \(|\rho| = |ws|\) and \(\rho_i\) related to \(ws_i\) for every \(i < |\rho|\), the source closure of \(b\) over \(\rho\) is related to the target pair \((\mathsf{code}\,c, E)\). Here \(c\) is the closure conversion of \(b\) in a scope of \(|\rho| + 1\) variables with the code accessors, which read variable \(0\) as \(\mathsf{fst}\,\#0\) and variable \(i + 1\) as \(\mathsf{fst}\,(\mathsf{snd}^i\,(\mathsf{snd}\,\#0))\), where \(\#0\) is the code parameter and \(\mathsf{snd}^i\) applies the second projection \(i\) times; and \(E\) is the encoding of \(ws\) as nested pairs ending in the unit value.

inductive ValRel : Source.Value Base → Value → Prop
  | clo {body : Stlc.RawTm Base} {ρ : List (Source.Value Base)} {ws : List Value}
      (hlen : ρ.length = ws.length)
      (hrel : ∀ i (h₁ : i < ρ.length) (h₂ : i < ws.length), ValRel ρ[i] ws[i]) :
      ValRel (.clo body ρ) (.pair (.code (convert codeAcc (ρ.length + 1) body)) (encodeEnv ws))

Uses 7 · Used by 5

Statement usesSource values of closure conversion · Target terms of closure conversion · Target values of closure conversion · Accessors inside converted code · Closure conversion with accessors · Encoding a list of target values · Raw lambda terms

Used byAccessors implementing a source environment · Code accessors implement the extended closure environment · Correctness of closure conversion in the empty environment · Correctness of closure conversion · Packed accessors evaluate to an encoded related environment

DefinitionAccessors implementing a source environment#✓fully proved

Let \(\rho\) be a list of source values, \(\rho_t\) a list of target values and \(\mathit{acc}\) a family of target terms indexed by the natural numbers. The accessors \(\mathit{acc}\) implement \(\rho\) in \(\rho_t\) when, for every index \(i\) less than the length of \(\rho\), there is a target value \(w\) such that \(\mathit{acc}(i)\) evaluates to \(w\) in the environment \(\rho_t\) and the entry of \(\rho\) at index \(i\) is related to \(w\) by the value relation of closure conversion.

def AccRel (ρ : List (Source.Value Base)) (ρt : List Value) (acc : Nat → Tm) : Prop :=
  ∀ i (h : i < ρ.length), ∃ w, Eval ρt (acc i) w ∧ ValRel ρ[i] w

Uses 5 · Used by 3

Statement usesSource values of closure conversion · Target terms of closure conversion · Big-step semantics of the closure-conversion target · Target values of closure conversion · Value relation for closure conversion

Used byCode accessors implement the extended closure environment · Correctness of closure conversion · Packed accessors evaluate to an encoded related environment

TheoremPacked accessors evaluate to an encoded related environment#✓fully proved

Let \(\rho\) be a list of source values, \(\rho_t\) a list of target values and \(\mathit{acc}\) a map from natural numbers to target terms, and suppose the accessors \(\mathit{acc}\) implement \(\rho\) in \(\rho_t\): for every \(i < |\rho|\), the term \(\mathit{acc}(i)\) evaluates in \(\rho_t\) to a target value related to \(\rho_i\) by the value relation. Then there is a list \(ws\) of target values with \(|ws| = |\rho|\) and \(\rho_i\) related to \(ws_i\) for every \(i < |\rho|\), such that the target term packing \(\mathit{acc}(0), \dots, \mathit{acc}(|\rho| - 1)\) as nested pairs ending in \(\mathsf{unit}\) evaluates in \(\rho_t\) to the encoding of \(ws\) as nested pairs ending in the unit value.

theorem AccRel.envOf {ρ : List (Source.Value Base)} {ρt : List Value} {acc : Nat → Tm}
    (h : AccRel ρ ρt acc) :
    ∃ ws : List Value, Eval ρt (ClosureConversion.envOf acc ρ.length) (encodeEnv ws) ∧
      ρ.length = ws.length ∧
      ∀ i (h₁ : i < ρ.length) (h₂ : i < ws.length), ValRel ρ[i] ws[i]

Uses 8 · Used by 1

Statement usesAccessors implementing a source environment · Source values of closure conversion · Target terms of closure conversion · Big-step semantics of the closure-conversion target · Target values of closure conversion · Value relation for closure conversion · Encoding a list of target values · Environment-packing term

Used byCorrectness of closure conversion

TheoremIterated second projections of an encoded environment#✓fully proved

Let \(\rho\) be a list of target values, \(e\) a target term and \(ws = [w_0, \dots, w_{m-1}]\) a list of target values, and suppose \(e\) evaluates in \(\rho\) to the encoding of \(ws\), the nested pairs \((w_0, (w_1, \dots (w_{m-1}, \mathsf{unit})\dots))\). Then for every natural number \(k \le m\), the term obtained by applying the second projection \(k\) times to \(e\) evaluates in \(\rho\) to the encoding of \([w_k, \dots, w_{m-1}]\), the list \(ws\) with its first \(k\) entries dropped.

theorem eval_snds {ρt : List Value} {e : Tm} {ws : List Value}
    (he : Eval ρt e (encodeEnv ws)) {k : Nat} (hk : k ≤ ws.length) :
    Eval ρt (snds k e) (encodeEnv (ws.drop k))

Uses 5 · Used by 2

Statement usesTarget terms of closure conversion · Big-step semantics of the closure-conversion target · Target values of closure conversion · Encoding a list of target values · Iterated second projection

Used byCode accessors implement the extended closure environment · Flat accessors implement the variables of a closure body

TheoremCode accessors implement the extended closure environment#✓fully proved

Let \(v\) be a source value related to a target value \(w\) by the value relation of closure conversion, and let \(\rho\) and \(ws\) be lists of source and target values of the same length such that, for every index \(i\) below that length, the entry of \(\rho\) at \(i\) is related to the entry of \(ws\) at \(i\). Then the code accessors implement the source environment \(v :: \rho\) (\(\rho\) with \(v\) added at index \(0\)) in the one-element target environment whose entry is the pair of \(w\) and the encoding of \(ws\) as nested pairs ending in \(\mathsf{unit}\).

theorem accRel_codeAcc {v : Source.Value Base} {ρ : List (Source.Value Base)} {w : Value}
    {ws : List Value} (hvw : ValRel v w) (hlen : ρ.length = ws.length)
    (hrel : ∀ i (h₁ : i < ρ.length) (h₂ : i < ws.length), ValRel ρ[i] ws[i]) :
    AccRel (v :: ρ) [.pair w (encodeEnv ws)] codeAcc

Uses 10 · Used by 1

Statement usesAccessors implementing a source environment · Source values of closure conversion · Target values of closure conversion · Value relation for closure conversion · Accessors inside converted code · Encoding a list of target values

Proof usesTarget terms of closure conversion · Big-step semantics of the closure-conversion target · Iterated second projections of an encoded environment · Iterated second projection

Used byCorrectness of closure conversion

TheoremCorrectness of closure conversion#✓fully proved

Let \(\rho\) be a list of source values, \(\ell\) its length, and \(t\) a source term that evaluates to a source value \(v\) in the environment \(\rho\). Let \(\rho_t\) be a list of target values and \(\mathit{acc}\) a family of target terms indexed by the natural numbers that implement \(\rho\) in \(\rho_t\). Then there is a target value \(w\) such that the conversion of \(t\) in a scope of \(\ell\) variables with accessors \(\mathit{acc}\) evaluates to \(w\) in the environment \(\rho_t\), and \(v\) is related to \(w\) by the value relation of closure conversion.

theorem convert_correct {ρ : List (Source.Value Base)} {t : Stlc.RawTm Base}
    {v : Source.Value Base} (h : Source.Eval ρ t v) {ρt : List Value} {acc : Nat → Tm}
    (hacc : AccRel ρ ρt acc) :
    ∃ w, Eval ρt (convert acc ρ.length t) w ∧ ValRel v w

Uses 17 · Used by 1

Statement usesAccessors implementing a source environment · Big-step semantics of the closure-conversion source · Source values of closure conversion · Target terms of closure conversion · Big-step semantics of the closure-conversion target · Target values of closure conversion · Value relation for closure conversion · Closure conversion with accessors · Raw lambda terms

Proof usesPacked accessors evaluate to an encoded related environment · Evaluation of a shifted term · Shifting a target term · Code accessors implement the extended closure environment · Accessors inside converted code · Encoding a list of target values · Environment-packing term · Simple types

Used byCorrectness of closure conversion in the empty environment

TheoremCorrectness of closure conversion in the empty environment#✓fully proved

If a source term \(t\) evaluates to a source value \(v\) in the empty environment, then there is a target value \(w\) such that the closure conversion of \(t\) evaluates to \(w\) in the empty environment and \(v\) is related to \(w\) by the value relation of closure conversion.

theorem closureConvert_correct {t : Stlc.RawTm Base} {v : Source.Value Base}
    (h : Source.Eval [] t v) : ∃ w, Eval [] (closureConvert t) w ∧ ValRel v w

Uses 9

Statement usesBig-step semantics of the closure-conversion source · Source values of closure conversion · Big-step semantics of the closure-conversion target · Target values of closure conversion · Value relation for closure conversion · Closure conversion of a program · Raw lambda terms

Proof usesTarget terms of closure conversion · Correctness of closure conversion

TheoremConverted terms are well scoped#✓fully proved

Let \(m\) and \(n\) be natural numbers and \(t\) a source term whose list of free indices at binder depth \(n\) is empty, that is, \(t\) is scoped in \(n\) variables. If \(\mathit{acc}\) is a family of target terms indexed by the natural numbers such that \(\mathit{acc}(i)\) is scoped in \(m\) for every \(i < n\), then the conversion of \(t\) in a scope of \(n\) variables with accessors \(\mathit{acc}\) is scoped in \(m\); in particular, every code body it contains is scoped in \(1\).

theorem convert_scoped {m : Nat} (t : Stlc.RawTm Base) :
    ∀ {n : Nat}, Stlc.RawTm.freeIndices n t = [] →
      ∀ {acc : Nat → Tm}, (∀ i, i < n → Scoped m (acc i)) → Scoped m (convert acc n t)

Uses 11 · Used by 1

Statement usesTarget terms of closure conversion · Well-scoped target terms · Closure conversion with accessors · Raw lambda terms · Free indices of a raw term

Proof usesShifting preserves scoping · Shifting a target term · Accessors inside converted code · Environment-packing term · Iterated second projection · Simple types

Used byClosure conversion of a closed term is well scoped

TheoremClosure conversion of a closed term is well scoped#✓fully proved

If a source term \(t\) is closed (it has no free variables), then its closure conversion is scoped in \(0\): it has no free variables, and every code body in it is scoped in \(1\), so refers only to its parameter.

theorem closureConvert_scoped {t : Stlc.RawTm Base} (ht : t.Closed) :
    Scoped 0 (closureConvert t)

Uses 6

Statement usesWell-scoped target terms · Closure conversion of a program · Raw lambda terms · Closed raw terms

Proof usesTarget terms of closure conversion · Converted terms are well scoped

TheoremFree variables one binder deeper#✓fully proved

For every raw term \(t\) and natural numbers \(d\) and \(j\), \(j\) is a free index of \(t\) at binder depth \(d + 1\) if and only if \(j + 1\) is a free index of \(t\) at binder depth \(d\).

theorem mem_freeIndices_succ (t : Stlc.RawTm Base) (d j : Nat) :
    j ∈ freeIndices (d + 1) t ↔ j + 1 ∈ freeIndices d t

Uses 3 · Used by 3

Statement usesRaw lambda terms · Free indices of a raw term

Proof usesSimple types

Used byCorrectness of flat closure conversion · Flat closure conversion preserves scoping · Flat accessors implement the variables of a closure body

DefinitionVariables captured by a lambda#✓fully proved

For a raw term \(b\), the captured variables of \(b\) form the list of free indices of \(b\) at binder depth \(1\) with duplicates removed: the de Bruijn indices \(j\) such that variable \(j + 1\) occurs free in \(b\), that is, the free variables of the abstraction \(\lambda.\,b\), each listed once.

def captured (body : Stlc.RawTm Base) : List Nat := (freeIndices 1 body).dedup

Uses 2 · Used by 5

Statement usesRaw lambda terms · Free indices of a raw term

Used byFlat closure conversion · Correctness of flat closure conversion · Flat closure conversion preserves scoping · Flat accessors implement the variables of a closure body · Flat value relation

DefinitionFlat closure environment#✓fully proved

For a map \(\mathrm{acc}\) from natural numbers to target terms and a list \(i_1, \dots, i_n\) of natural numbers, the flat environment is the target term \((\mathrm{acc}(i_1), (\mathrm{acc}(i_2), \dots, (\mathrm{acc}(i_n), \mathsf{unit})\dots))\), which packs \(\mathrm{acc}(i)\) for each \(i\) in the list, in order, as nested pairs ending in \(\mathsf{unit}\); the empty list gives \(\mathsf{unit}\).

def envFlat (acc : Nat → Tm) : List Nat → Tm
  | [] => .unit
  | i :: is => .pair (acc i) (envFlat acc is)

Uses 1 · Used by 5

Statement usesTarget terms of closure conversion

Used byFlat closure conversion · Correctness of flat closure conversion · Flat closure conversion preserves scoping · Length of an evaluated flat environment · Evaluating a flat environment

DefinitionAccessors inside flat code#✓fully proved

For a list \(L\) of natural numbers, the flat accessors for \(L\) assign a target term to each variable: variable \(0\) is sent to \(\mathsf{fst}\,\#0\), and variable \(j + 1\) is sent to \(\mathsf{fst}\,(\mathsf{snd}^k\,(\mathsf{snd}\,\#0))\). Here \(\#0\) is target variable \(0\), \(\mathsf{snd}^k\) applies the second projection \(k\) times, and \(k\) is the index of the first occurrence of \(j\) in \(L\), or the length of \(L\) if \(j\) does not occur in \(L\).

Inside flat code the parameter \(\#0\) is the pair of the argument and the environment, so variable \(0\) is the argument and variable \(j + 1\) is the entry of the environment at the position of \(j\) in \(L\).

def flatAcc (fvs : List Nat) : Nat → Tm
  | 0 => .fst (.var 0)
  | j + 1 => .fst (snds (fvs.idxOf j) (.snd (.var 0)))

Uses 2 · Used by 5

Statement usesTarget terms of closure conversion · Iterated second projection

Used byFlat closure conversion · Correctness of flat closure conversion · Flat closure conversion preserves scoping · Flat accessors implement the variables of a closure body · Flat value relation

DefinitionFlat closure conversion#✓fully proved

Given accessors \(\mathrm{acc}\), a map from natural numbers to target terms, the flat conversion \(C_{\mathrm{acc}}(t)\) of a raw term \(t\) is defined by recursion on \(t\). A variable \(i\) becomes \(\mathrm{acc}(i)\). A lambda \(\lambda.\,b\), whose parameter type is ignored, becomes the pair \((\mathsf{code}\,C_{\mathrm{acc}'}(b), e)\). Here \(i_1, \dots, i_n\) are the captured variables of \(b\), the environment \(e\) is \((\mathrm{acc}(i_1), (\mathrm{acc}(i_2), \dots, (\mathrm{acc}(i_n), \mathsf{unit})\dots))\), and \(\mathrm{acc}'\) sends \(0\) to \(\mathsf{fst}\,(\mathsf{var}\,0)\) and \(j + 1\) to \(\mathsf{fst}\,(\mathsf{snd}^{k+1}\,(\mathsf{var}\,0))\), where \(k\) is the position of \(j\) in that list, counting from \(0\) (the length \(n\) if \(j\) does not occur). An application \(f\,a\) becomes \(\mathsf{let}\ C_{\mathrm{acc}}(f)\ \mathsf{in}\ (\mathsf{fst}\,(\mathsf{var}\,0))\, (C_{\mathrm{acc}^{+}}(a), \mathsf{snd}\,(\mathsf{var}\,0))\), where \(\mathsf{var}\,0\) is the variable bound by the \(\mathsf{let}\) and \(\mathrm{acc}^{+}(i)\) is the shift of \(\mathrm{acc}(i)\).

def convertFlat : (Nat → Tm) → Stlc.RawTm Base → Tm
  | acc, .var i => acc i
  | acc, .lam _ body =>
      .pair (.code (convertFlat (flatAcc (captured body)) body)) (envFlat acc (captured body))
  | acc, .app f a =>
      .letIn (convertFlat acc f)
        (.app (.fst (.var 0)) (.pair (convertFlat (fun i => (acc i).shift) a) (.snd (.var 0))))

Uses 7 · Used by 4

Statement usesTarget terms of closure conversion · Shifting a target term · Variables captured by a lambda · Flat closure environment · Accessors inside flat code · Raw lambda terms · Simple types

Used byFlat closure conversion of a program · Correctness of flat closure conversion · Flat closure conversion preserves scoping · Flat value relation

DefinitionFlat closure conversion of a program#✓fully proved

The flat closure conversion of a raw term \(t\) is the flat conversion of \(t\) with the accessors \(i \mapsto \mathsf{var}\,i\), which send each free variable \(i\) of \(t\) to the target variable \(i\). It is meant for closed terms.

def closureConvertFlat (t : Stlc.RawTm Base) : Tm := convertFlat .var t

Uses 3 · Used by 2

Statement usesTarget terms of closure conversion · Flat closure conversion · Raw lambda terms

Used byCorrectness of flat closure conversion for closed programs · Flat closure conversion of a closed term is well scoped

InductiveFlat value relation#✓fully proved

The flat value relation between source values and target values is the least relation with the following property. Let \(b\) be a raw term, \(\rho\) a list of source values of length \(|\rho|\), \(c = (c_0, \dots, c_{m-1})\) the list of variables captured by \(\lambda. b\), and \(w_0, \dots, w_{m-1}\) target values, as many as there are captured variables. If, for every \(k < m\), \(c_k < |\rho|\) and the entry of \(\rho\) at index \(c_k\) (counting from \(0\)) is related to \(w_k\), then the source closure of \(b\) over \(\rho\) is related to the target value \((\mathsf{code}\,B, \mathrm{enc}(w_0, \dots, w_{m-1}))\), where \(B\) is the flat closure conversion of \(b\) with the flat accessors for \(c\), and \(\mathrm{enc}\) encodes a list of target values as nested pairs ending in \(\mathsf{unit}\).

inductive FlatValRel : Source.Value Base → Value → Prop
  | clo {body : Stlc.RawTm Base} {ρ : List (Source.Value Base)} {ws : List Value}
      (hlen : (captured body).length = ws.length)
      (hbound : ∀ k (h₁ : k < (captured body).length), (captured body)[k] < ρ.length)
      (hrel : ∀ k (h₁ : k < (captured body).length) (h₂ : k < ws.length),
        FlatValRel (ρ[(captured body)[k]]'(hbound k h₁)) ws[k]) :
      FlatValRel (.clo body ρ)
        (.pair (.code (convertFlat (flatAcc (captured body)) body)) (encodeEnv ws))

Uses 8 · Used by 5

Statement usesSource values of closure conversion · Target terms of closure conversion · Target values of closure conversion · Variables captured by a lambda · Flat closure conversion · Encoding a list of target values · Accessors inside flat code · Raw lambda terms

Used byCorrectness of flat closure conversion for closed programs · Correctness of flat closure conversion · Evaluating a flat environment · Accessors implementing the free variables of a term · Flat accessors implement the variables of a closure body

DefinitionAccessors implementing the free variables of a term#✓fully proved

Let \(\rho\) be a list of source values of length \(|\rho|\), \(\rho_t\) a list of target values, \(\mathrm{acc}\) a map assigning a target term to each natural number, and \(t\) a raw term. The accessors \(\mathrm{acc}\) implement \(t\) for \(\rho\) in \(\rho_t\) when, for every free variable \(i\) of \(t\), \(i < |\rho|\) and \(\mathrm{acc}(i)\) evaluates in the target environment \(\rho_t\) to a target value that is related, by the flat value relation, to the entry of \(\rho\) at index \(i\) (counting from \(0\)).

def FlatAccRel (ρ : List (Source.Value Base)) (ρt : List Value) (acc : Nat → Tm)
    (t : Stlc.RawTm Base) : Prop :=
  ∀ i ∈ freeIndices 0 t, ∃ h : i < ρ.length, ∃ w, Eval ρt (acc i) w ∧ FlatValRel ρ[i] w

Uses 7 · Used by 2

Statement usesFlat value relation · Source values of closure conversion · Target terms of closure conversion · Big-step semantics of the closure-conversion target · Target values of closure conversion · Raw lambda terms · Free indices of a raw term

Used byCorrectness of flat closure conversion · Flat accessors implement the variables of a closure body

TheoremEvaluating a flat environment#✓fully proved

Let \(\rho\) be a source environment, \(\rho_t\) a target environment, \(\mathrm{acc}\) a map from natural numbers to target terms, and \(i_1, \dots, i_n\) a list of natural numbers. Write \(\rho_i\) for the entry of \(\rho\) at index \(i\), counting from \(0\). Suppose every \(i\) in the list is less than the length of \(\rho\) and \(\mathrm{acc}(i)\) evaluates in \(\rho_t\) to a target value related to \(\rho_i\) by the flat value relation. Then there are target values \(w_1, \dots, w_n\) such that the flat environment \((\mathrm{acc}(i_1), (\dots, (\mathrm{acc}(i_n), \mathsf{unit})\dots))\) evaluates in \(\rho_t\) to \((w_1, (\dots, (w_n, \mathsf{unit})\dots))\), and for each \(k\) the index \(i_k\) is less than the length of \(\rho\) and \(w_k\) is related to \(\rho_{i_k}\) by the flat value relation.

theorem eval_envFlat {ρ : List (Source.Value Base)} {ρt : List Value} {acc : Nat → Tm} :
    ∀ (is : List Nat), (∀ i ∈ is, ∃ h : i < ρ.length, ∃ w, Eval ρt (acc i) w ∧
      FlatValRel ρ[i] w) →
    ∃ ws : List Value, Eval ρt (envFlat acc is) (encodeEnv ws) ∧ is.length = ws.length ∧
      ∃ hbound : ∀ k (h₁ : k < is.length), is[k] < ρ.length,
      ∀ k (h₁ : k < is.length) (h₂ : k < ws.length), FlatValRel (ρ[is[k]]'(hbound k h₁)) ws[k]

Uses 7 · Used by 1

Statement usesFlat value relation · Source values of closure conversion · Target terms of closure conversion · Big-step semantics of the closure-conversion target · Target values of closure conversion · Encoding a list of target values · Flat closure environment

Used byCorrectness of flat closure conversion

TheoremLength of an evaluated flat environment#✓fully proved

Let \(\mathrm{acc}\) be a map from natural numbers to target terms and \(i_1, \dots, i_n\) a list of natural numbers. If the flat environment \((\mathrm{acc}(i_1), (\dots, (\mathrm{acc}(i_n), \mathsf{unit})\dots))\) evaluates in some target environment to the encoding \((w_1, (\dots, (w_k, \mathsf{unit})\dots))\) of a list of target values \(w_1, \dots, w_k\), then \(k = n\).

theorem envFlat_length {ρt : List Value} {acc : Nat → Tm}
    {is : List Nat} {ws : List Value} (h : Eval ρt (envFlat acc is) (encodeEnv ws)) :
    ws.length = is.length

Uses 5

Statement usesTarget terms of closure conversion · Big-step semantics of the closure-conversion target · Target values of closure conversion · Encoding a list of target values · Flat closure environment

TheoremFlat accessors implement the variables of a closure body#✓fully proved

Let \(b\) be a raw term, let \(c = (c_0, \dots, c_{m-1})\) be the list of variables captured by \(\lambda. b\), let \(\rho\) be a list of source values of length \(|\rho|\), write \(\rho_n\) for the entry of \(\rho\) at index \(n\) (counting from \(0\)), and let \(w_0, \dots, w_{m-1}\) be target values such that \(c_k < |\rho|\) and \(\rho_{c_k}\) is related to \(w_k\) by the flat value relation for every \(k < m\). If a source value \(v\) is related to a target value \(w\) by the flat value relation, then the flat accessors for \(c\) implement the free variables of \(b\) for the source environment \(v :: \rho\) (the list \(\rho\) with \(v\) added at index \(0\)) in the one-entry target environment \([(w, \mathrm{enc}(w_0, \dots, w_{m-1}))]\), where \(\mathrm{enc}\) encodes a list of target values as nested pairs ending in \(\mathsf{unit}\). That is, for every free variable \(i\) of \(b\), \(i < |\rho| + 1\) and the flat accessor for \(i\) evaluates in that target environment to a target value related to the entry of \(v :: \rho\) at index \(i\) by the flat value relation.

theorem flatAccRel_flatAcc {v : Source.Value Base} {ρ : List (Source.Value Base)}
    {body : Stlc.RawTm Base} {w : Value} {ws : List Value} (hvw : FlatValRel v w)
    (hlen : (captured body).length = ws.length)
    (hbound : ∀ k (h₁ : k < (captured body).length), (captured body)[k] < ρ.length)
    (hrel : ∀ k (h₁ : k < (captured body).length) (h₂ : k < ws.length),
      FlatValRel (ρ[(captured body)[k]]'(hbound k h₁)) ws[k]) :
    FlatAccRel (v :: ρ) [.pair w (encodeEnv ws)] (flatAcc (captured body)) body

Uses 14 · Used by 1

Statement usesAccessors implementing the free variables of a term · Flat value relation · Source values of closure conversion · Target values of closure conversion · Variables captured by a lambda · Encoding a list of target values · Accessors inside flat code · Raw lambda terms

Proof usesTarget terms of closure conversion · Big-step semantics of the closure-conversion target · Iterated second projections of an encoded environment · Free variables one binder deeper · Iterated second projection · Free indices of a raw term

Used byCorrectness of flat closure conversion

TheoremCorrectness of flat closure conversion#✓fully proved

Let \(\rho\) be a source environment, \(\rho_t\) a target environment, \(\mathrm{acc}\) a map from natural numbers to target terms, and \(t\) a raw term that evaluates to a source value \(v\) in \(\rho\). Suppose that for every free variable \(i\) of \(t\), \(i\) is less than the length of \(\rho\) and \(\mathrm{acc}(i)\) evaluates in \(\rho_t\) to a target value related by the flat value relation to the entry \(\rho_i\) of \(\rho\) at index \(i\) (counting from \(0\)). Then the flat conversion of \(t\) with accessors \(\mathrm{acc}\) evaluates in \(\rho_t\) to some target value related to \(v\) by the flat value relation.

theorem convertFlat_correct {ρ : List (Source.Value Base)} {t : Stlc.RawTm Base}
    {v : Source.Value Base} (h : Source.Eval ρ t v) {ρt : List Value} {acc : Nat → Tm}
    (hacc : FlatAccRel ρ ρt acc t) :
    ∃ w, Eval ρt (convertFlat acc t) w ∧ FlatValRel v w

Uses 20 · Used by 1

Statement usesAccessors implementing the free variables of a term · Flat value relation · Big-step semantics of the closure-conversion source · Source values of closure conversion · Target terms of closure conversion · Big-step semantics of the closure-conversion target · Target values of closure conversion · Flat closure conversion · Raw lambda terms

Proof usesEvaluation of a shifted term · Shifting a target term · Variables captured by a lambda · Encoding a list of target values · Flat closure environment · Evaluating a flat environment · Accessors inside flat code · Flat accessors implement the variables of a closure body · Free variables one binder deeper · Free indices of a raw term · Simple types

Used byCorrectness of flat closure conversion for closed programs

TheoremCorrectness of flat closure conversion for closed programs#✓fully proved

Let \(t\) be a closed raw term, that is, one with no free variables. If \(t\) evaluates to a source value \(v\) in the empty environment, then the flat closure conversion of \(t\) evaluates in the empty target environment to some target value \(w\) related to \(v\) by the flat value relation.

theorem closureConvertFlat_correct {t : Stlc.RawTm Base} {v : Source.Value Base}
    (ht : t.Closed) (h : Source.Eval [] t v) :
    ∃ w, Eval [] (closureConvertFlat t) w ∧ FlatValRel v w

Uses 11

Statement usesFlat value relation · Big-step semantics of the closure-conversion source · Source values of closure conversion · Big-step semantics of the closure-conversion target · Target values of closure conversion · Flat closure conversion of a program · Raw lambda terms · Closed raw terms

Proof usesTarget terms of closure conversion · Correctness of flat closure conversion · Free indices of a raw term

TheoremFlat closure conversion preserves scoping#✓fully proved

Let \(t\) be a raw term, \(m\) a natural number and \(\mathrm{acc}\) a map from natural numbers to target terms. If \(\mathrm{acc}(i)\) is scoped in \(m\) for every free variable \(i\) of \(t\), then the flat conversion of \(t\) with accessors \(\mathrm{acc}\) is scoped in \(m\). In particular every code body it contains is scoped in \(1\), so refers only to its parameter.

theorem convertFlat_scoped {m : Nat} (t : Stlc.RawTm Base) {acc : Nat → Tm}
    (hacc : ∀ i ∈ freeIndices 0 t, Scoped m (acc i)) : Scoped m (convertFlat acc t)

Uses 13 · Used by 1

Statement usesTarget terms of closure conversion · Well-scoped target terms · Flat closure conversion · Raw lambda terms · Free indices of a raw term

Proof usesShifting preserves scoping · Shifting a target term · Variables captured by a lambda · Flat closure environment · Accessors inside flat code · Free variables one binder deeper · Iterated second projection · Simple types

Used byFlat closure conversion of a closed term is well scoped

TheoremFlat closure conversion of a closed term is well scoped#✓fully proved

If a raw term \(t\) is closed, then its flat closure conversion is scoped in \(0\): it has no free variables, and every code body in it is scoped in \(1\), so refers only to its parameter.

theorem closureConvertFlat_scoped {t : Stlc.RawTm Base} (ht : t.Closed) :
    Scoped 0 (closureConvertFlat t)

Uses 7

Statement usesWell-scoped target terms · Flat closure conversion of a program · Raw lambda terms · Closed raw terms

Proof usesTarget terms of closure conversion · Flat closure conversion preserves scoping · Free indices of a raw term

43 fully proved

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.