Raw linear terms

linear.agda

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) = {!!}