Skip to content

Instantly share code, notes, and snippets.

Last active Mar 26, 2019
What would you like to do?
Raw linear terms
open import Data.Nat.Base
open import Data.Vec
open import Data.Bool.Base using (Bool; false; true)
open import Data.Product
m n :
b : Bool
Γ Δ Ξ T I O : Vec Bool n
-- A Linear term has an output and an output usage annotation
-- For each variable (i.e. index in the Vec):
-- * true: available
-- * false: already consumed
Linear : Set₁
Linear = {n} (Γ Δ : Vec Bool n) Set
data Var : Linear where
z : Var (true ∷ Γ) (false ∷ Γ)
s : Var Γ Δ Var (b ∷ Γ) (b ∷ Δ)
data Lam : Linear where
var : Var Γ Δ Lam Γ Δ
app : Lam Γ Δ Lam Δ Ξ Lam Γ Ξ
lam : Lam (true ∷ Γ) (false ∷ Δ) Lam Γ Δ
data Env : (Γ Δ : Vec Bool n) -- input and output usage of the env
(T : Vec Bool m) -- target usafe covered by the content of the env
Set where
-- empty environment
[] : Env Γ Γ []
-- 0th variable is available so we have a value for it
-- + env for the rest of the usage T
_∷_ : Lam Γ Δ Env Δ Ξ T Env Γ Ξ (true ∷ T)
-- 0th variable has already been consumed: we don't have a term for it anymore
-- + env for the rest of the usage T
─∷_ : Env Γ Δ T Env Γ Δ (false ∷ T)
-- When we go under binders, we need to be able to extend the input/output
-- context to cope with the extended context
[v]∷_ : Env Γ Δ T Env (true ∷ Γ) (false ∷ Δ) (false ∷ T)
]v[∷_ : Env Γ Δ T Env (false ∷ Γ) (false ∷ Δ) (false ∷ T)
Subst : (R : Linear) -- target of the substitution
(V : Linear) -- output (e.g. substituting for vars yields terms)
Subst R V = {m n} {Γ Δ I O}
Env {m} {n} Γ Δ I -- environment targetting I
R I O -- R consuming resources in I, returning O leftovers
-- the result is a usage annotation
-- a value V consuming in the input, returning M leftovers
-- an environment of leftovers for whatever is still true in O
λ M V Γ M × Env M Δ O
substVar : Subst Var Lam
substVar (t ∷ ρ) z = -, t , ─∷ ρ
substVar (x ∷ ρ) (s v) = {!!}
substVar (─∷ ρ) (s v) = {!!}
substVar ([v]∷ ρ) (s v) = {!!}
substVar (]v[∷ ρ) (s v) = {!!}
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment