Skip to content

Instantly share code, notes, and snippets.

@gallais
Last active Mar 26, 2019
Embed
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
variable
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)
Set
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