contextual-sequent.idr

module Dual.SeqCalc.Contextual

import Data.List
import Data.List.Elem
import Data.List.Quantifiers
import All
import Subset

%default total

data Ty = A
        | Imp Ty Ty
        | Box (List Ty) Ty

infixr 5 ~>
(~>) : Ty -> Ty -> Ty
(~>) = Imp

record BoxT where
  constructor MkBox
  ph : List Ty
  t : Ty

data Term : List BoxT -> List Ty -> Ty -> Type where
  AVar : Elem A g -> Term d g A
  MVar : Elem (MkBox ps a) d -> All (Term d g) ps -> Term d (a::g) b -> Term d g b
  Lam  : Term d (a::g) b -> Term d g (a~>b)
  ImpL : Elem (a~>b) g -> Term d g a -> Term d (b::g) c -> Term d g c
  Shut : Term d g a -> Term d s (Box g a)
  BoxL : Elem (Box ps a) g -> Term (MkBox ps a::d) g c -> Term d g c

renameM : Subset d s -> Term d g c -> Term s g c
renameM s (AVar el)     = AVar el
renameM s (MVar el a t) = MVar (s el) (assert_total $ mapPredicate (renameM s) a) (renameM s t)
renameM s (Lam  t)      = Lam $ renameM s t
renameM s (ImpL el t u) = ImpL el (renameM s t) (renameM s u)
renameM s (Shut t)      = Shut $ renameM s t
renameM s (BoxL el t)   = BoxL el (renameM (ext s) t)

rename : Subset g s -> Term d g c -> Term d s c
rename s (AVar el)     = AVar $ s el
rename s (MVar el a t) = MVar el (assert_total $ mapPredicate (rename s) a) (rename (ext s) t)
rename s (Lam  t)      = Lam $ rename (ext s) t
rename s (ImpL el t u) = ImpL (s el) (rename s t) (rename (ext s) u)
rename s (Shut t)      = Shut t
rename s (BoxL el t)   = BoxL (s el) (rename s t)

mutual
  identityCtx : (g : List Ty) -> All (Term d g) g
  identityCtx []     = []
  identityCtx (a::g) = identity a Here :: mapPredicate (rename There) (identityCtx g)

  identity : (a : Ty) -> Elem a g -> Term d g a
  identity  A         el = AVar el
  identity (Imp a b)  el = Lam $ ImpL (There el) (identity a Here) (identity b Here)
  identity (Box ps a) el = BoxL el (Shut $ MVar Here (identityCtx ps) (identity a Here))