{-# OPTIONS --without-K --safe #-}
module README.Pointers-to-results-from-the-paper where
import Colist
import Conat
import Omniscience
import Delay-monad
import Delay-monad.Bisimilarity
import Delay-monad.Monad
import Delay-monad.Quantitative-weak-bisimilarity
import Only-allocation
import Unbounded-space
import Upper-bounds
import Lambda.Compiler
import Lambda.Compiler-correctness
import Lambda.Compiler-correctness.Sizes-match
import Lambda.Compiler-correctness.Steps-match
import Lambda.Delay-crash
import Lambda.Delay-crash-trace
import Lambda.Interpreter
import Lambda.Interpreter.Stack-sizes
import Lambda.Interpreter.Stack-sizes.Counterexample
import Lambda.Interpreter.Stack-sizes.Example
import Lambda.Interpreter.Steps
import Lambda.Interpreter.Steps.Counterexample
import Lambda.Virtual-machine
import Lambda.Virtual-machine.Instructions
import Lambda.Syntax
Conat = Conat.Conat
Conat′ = Conat.Conat′
infinity = Conat.infinity
[_]_≤_ = Conat.[_]_≤_
[_]_≤′_ = Conat.[_]_≤′_
[_]_∼N_ = Conat.[_]_∼_
Stmt = Only-allocation.Stmt
Program = Only-allocation.Program
Colist = Colist.Colist
modify = Unbounded-space.modify
⟦_⟧₁ = Unbounded-space.⟦_⟧
⟦_⟧′ = Unbounded-space.⟦_⟧′
[_]_⊑_ = Upper-bounds.[_]_⊑_
[_]_⊑′_ = Upper-bounds.[_]_⊑′_
□ = Colist.□
LUB = Upper-bounds.LUB
lub-unique = Upper-bounds.lub-unique
antisymmetric = Conat.antisymmetric-≤
WLPO = Omniscience.WLPO
LEM→WLPO = Omniscience.LEM→WLPO
wlpo⇔lub = Unbounded-space.wlpo⇔lub
Heap-usage = Unbounded-space.Heap-usage
wlpo⇔max = Unbounded-space.wlpo⇔max
max-unique = Unbounded-space.max-unique
bounded = Only-allocation.bounded
bounded₂ = Only-allocation.bounded₂
unbounded = Only-allocation.unbounded
_∷′_ = Colist._∷′_
bounded-loops = Unbounded-space.bounded-loops
bounded₂-loops = Unbounded-space.bounded₂-loops
unbounded-loops = Unbounded-space.unbounded-loops
max-bounded-1 = Unbounded-space.max-bounded-1
max-bounded₂-2 = Unbounded-space.max-bounded₂-2
max-unbounded-∞ = Unbounded-space.max-unbounded-∞
no-finite-max→infinite-max = Unbounded-space.no-finite-max→infinite-max
no-finite→infinite = Upper-bounds.no-finite→infinite
opt = Unbounded-space.opt
opt-improves = Unbounded-space.opt-improves
opt-bounded₂∼bounded = Unbounded-space.opt-bounded₂∼bounded
[_]_∼L_ = Colist.[_]_∼_
opt-correct = Unbounded-space.opt-correct
[_]_≲_ = Upper-bounds.[_]_≲_
[_]_≲′_ = Upper-bounds.[_]_≲′_
≲⇔least-upper-bounds-≤ = Upper-bounds.≲⇔least-upper-bounds-≤
[]≲ = Upper-bounds.[]≲
consʳ-≲ = Upper-bounds.consʳ-≲
consˡ-≲ = Upper-bounds.consˡ-≲
cons′-≲ = Upper-bounds.cons′-≲
Bounded = Upper-bounds.Bounded
consʳ-≲′→≲-infinite = Upper-bounds.consʳ-≲′→≲-infinite
¬-consʳ-≲′ = Upper-bounds.¬-consʳ-≲′
reflexive-≲ = Upper-bounds._□≲
transitive-≲ = Upper-bounds.step-≲
¬-transitivity-size-preservingʳ =
Upper-bounds.¬-transitivity-size-preservingʳ
transitive-∼≲ = Upper-bounds.step-∼≲
opt-correct-≲ = Unbounded-space.opt-correct-≲
Delay = Delay-monad.Delay
never = Delay-monad.never
monad-instance₁ = Delay-monad.Monad.delay-raw-monad
[_]_∼D_ = Delay-monad.Bisimilarity.[_]_∼_
left-identity₁ = Delay-monad.Monad.left-identity′
right-identity₁ = Delay-monad.Monad.right-identity′
associativity₁ = Delay-monad.Monad.associativity′
[_]_≈D_ = Delay-monad.Bisimilarity.[_]_≈_
Tm = Lambda.Syntax.Tm
Env = Lambda.Syntax.Closure.Env
Value = Lambda.Syntax.Closure.Value
DelayC = Lambda.Delay-crash.Delay-crash
crash = Lambda.Delay-crash.crash
now≉never = Delay-monad.Bisimilarity.now≉never
_∙_ = Lambda.Interpreter._∙_
⟦_⟧₂ = Lambda.Interpreter.⟦_⟧
⟦if⟧ = Lambda.Interpreter.⟦if⟧
DelayCT = Lambda.Delay-crash-trace.Delay-crash-trace
trace = Lambda.Delay-crash-trace.trace
delayC = Lambda.Delay-crash-trace.delay-crash
monad-instance₂ = Lambda.Delay-crash-trace.raw-monad
[_]_∼DCT_ = Lambda.Delay-crash-trace.[_]_∼_
left-identity₂ = Lambda.Delay-crash-trace.left-identity
right-identity₂ = Lambda.Delay-crash-trace.right-identity
associativity₂ = Lambda.Delay-crash-trace.associativity
Instr = Lambda.Virtual-machine.Instructions.Instr
Code = Lambda.Virtual-machine.Instructions.Code
VM-Env = Lambda.Syntax.Closure.Env
VM-Value = Lambda.Syntax.Closure.Value
Stack-element = Lambda.Virtual-machine.Instructions.Stack-element
Stack = Lambda.Virtual-machine.Instructions.Stack
State = Lambda.Virtual-machine.Instructions.State
Result = Lambda.Virtual-machine.Instructions.Result
step = Lambda.Virtual-machine.step
exec⁺ = Lambda.Virtual-machine.exec⁺
exec⁺′ = Lambda.Virtual-machine.exec⁺′
exec = Lambda.Virtual-machine.exec
stack-sizes = Lambda.Virtual-machine.stack-sizes
In-tail-context = Lambda.Compiler.In-tail-context
comp = Lambda.Compiler.comp
comp-body = Lambda.Compiler.comp-body
comp-name = Lambda.Compiler.comp-name
comp-env = Lambda.Compiler.comp-env
comp-val = Lambda.Compiler.comp-val
comp₀ = Lambda.Compiler.comp₀
compiler-correct = Lambda.Compiler-correctness.correct
key-lemma₁ = Lambda.Compiler-correctness.⟦⟧-correct
Cont-OK = Lambda.Compiler-correctness.Cont-OK
Stack-OK = Lambda.Compiler-correctness.Stack-OK
[_,_]_∙S_ = Lambda.Interpreter.Stack-sizes.[_,_]_∙_
⟦_⟧S = Lambda.Interpreter.Stack-sizes.⟦_⟧
δ = Lambda.Interpreter.Stack-sizes.δ
⟦if⟧S = Lambda.Interpreter.Stack-sizes.⟦if⟧
scanl = Colist.scanl
numbers = Lambda.Interpreter.Stack-sizes.numbers
stack-sizesS = Lambda.Interpreter.Stack-sizes.stack-sizes
⟦⟧∼⟦⟧ = Lambda.Interpreter.Stack-sizes.⟦⟧∼⟦⟧
maximum-stack-sizes-match =
Lambda.Compiler-correctness.Sizes-match.maximum-stack-sizes-match
stack-sizes-not-bisimilar =
Lambda.Interpreter.Stack-sizes.Counterexample.stack-sizes-not-bisimilar
stack-sizes-related =
Lambda.Compiler-correctness.Sizes-match.stack-sizes-related
[_]_≂_ = Upper-bounds.[_]_≂_
[_]_≂′_ = Upper-bounds.[_]_≂′_
LUB-cong = Upper-bounds.LUB-cong
consʳ-≂ = Upper-bounds.consʳ-≂
consˡ-≂ = Upper-bounds.consˡ-≂
cons-≂ = Upper-bounds.cons-≂
cons′-≂ = Upper-bounds.cons′-≂
reflexive-≂ = Upper-bounds._□≂
symmetric-≂ = Upper-bounds.symmetric-≂
transitive-≂ = Upper-bounds.step-≂
transitive-∼≂ = Upper-bounds.step-∼≂
transitive-≂∼ = Upper-bounds.step-≂∼
[_]_≂″_ = Upper-bounds.[_]_≂″_
≂′⇔≂″ = Upper-bounds.≂′⇔≂″
[_]_≲″_ = Upper-bounds.[_]_≲″_
≲′⇔≲″ = Upper-bounds.≲′⇔≲″
key-lemma₂ = Lambda.Compiler-correctness.Sizes-match.⟦⟧-correct
Ω = Lambda.Syntax.Ω
Ω-loops = Lambda.Interpreter.Ω-loops′
Ω-requires-unbounded-space =
Lambda.Interpreter.Stack-sizes.Ω-requires-unbounded-space
go = Lambda.Interpreter.Stack-sizes.Example.go
go-loops = Lambda.Interpreter.Stack-sizes.Example.go-loops
go-bounded-stack =
Lambda.Interpreter.Stack-sizes.Example.go-bounded-stack
not-suitable-cost-measure =
Lambda.Interpreter.Steps.Counterexample.not-suitable-cost-measure
✓_ = Lambda.Interpreter.Steps.✓_
_∙T_ = Lambda.Interpreter.Steps._∙_
⟦_⟧T = Lambda.Interpreter.Steps.⟦_⟧
⟦if⟧T = Lambda.Interpreter.Steps.⟦if⟧
the-cost-measure-is-suitable =
Lambda.Compiler-correctness.Steps-match.steps-match
[_∣_∣_∣_∣_]_≈D_ =
Delay-monad.Quantitative-weak-bisimilarity.[_∣_∣_∣_∣_]_≈_
≈⇔≈×steps≤steps² =
Delay-monad.Quantitative-weak-bisimilarity.≈⇔≈×steps≤steps²
≈→≈×steps≤steps² =
Delay-monad.Quantitative-weak-bisimilarity.≈→≈×steps≤steps²
≈×steps≤steps²→≈⇔uninhabited =
Delay-monad.Quantitative-weak-bisimilarity.≈×steps≤steps²→≈⇔uninhabited
weaken = Delay-monad.Quantitative-weak-bisimilarity.weaken
transitive-≳∼ = Delay-monad.Quantitative-weak-bisimilarity.transitive-≳∼
transitive-≈∼ = Delay-monad.Quantitative-weak-bisimilarity.transitive-≈∼
transitive-∼≈ = Delay-monad.Quantitative-weak-bisimilarity.transitive-∼≈
key-lemma₃ = Lambda.Compiler-correctness.Steps-match.⟦⟧-correct