Extension to cubical (WIP)

Simple.hs

module Simple where

import Bwd -- https://gist.github.com/cheery/eb515304a0a7bcf524cb89ccf53266c2

data Interval
  = I0
  | I1
  | In Int
  deriving (Show, Eq)

data Tms
  = Idt
  | Comp Tms Tms
  | Epsilon
  | TCons Tms Tm
  | Fst Tms
  deriving (Show)

data Tm
  = Snd Tms
  | Sub Tm Tms
  | Lam Tm
  | App Tm
  | ElU
  | ElPi Tm Tm
  | ElSig Tm Tm
  | ElUnit
  | Pair Tm Tm
  | Proj1 Tm
  | Proj2 Tm
  | Constant
  | ElPath Tm Tm Tm
  | PIntr Tm
  | PElim Tm Interval
  | ElEmpty
  | Abort
  deriving (Show)

tm_app :: Tm -> Tm -> Tm
tm_app f u = Sub (App f) (TCons Idt u)

class Repr a where
  repr :: a -> Tm

instance Repr Int where
  repr 0 = Snd Idt
  repr n = Sub (repr (n-1)) (Fst Idt)

data Val
  = Susp Int (Bwd XElim)
  | Clos (Val -> Val)
  | VU
  | VPi Val (Val -> Val)
  | VSig Val (Val -> Val)
  | VUnit
  | VPair Val Val
  | VConstant
  | VPath Val Val Val
  | VPIntr Val
  | VEmpty
  | VAbort

data XElim
  = XApp Val
  | XProj1
  | XProj2
  | XPElim Interval

data Cofib
  = Eq Val Val
  | Disj Cofib Cofib
  | Forall (Val -> Cofib)

type Env = Bwd Val

eval :: Tm -> Env -> Val
eval (Snd s) p = hd (evals s p)
eval (Sub u s) p = eval u (evals s p)
eval (Lam u) p = Clos (\v -> eval u (p :> v))
eval (App u) (p :> v) = apply (eval u p) v
eval ElU p = VU
eval (ElPi a b) p = VPi (eval a p) (\v -> eval b (p :> v))
eval (ElSig a b) p = VSig (eval a p) (\v -> eval b (p :> v))
eval ElUnit p = VUnit
eval (Pair a b) p = VPair (eval a p) (eval b p)
eval (Proj1 u) p = proj1 (eval u p)
eval (Proj2 u) p = proj2 (eval u p)
eval Constant p = VConstant
eval (ElPath a u t) p = VPath (eval a (fmap (mapi 0 (weaken 1)) p))
                              (eval u p)
                              (eval t p)
eval (PIntr u) p = VPIntr (eval u (fmap (mapi 0 (weaken 1)) p))
eval (PElim f i) p = pelim (eval f p) i
eval ElEmpty p = VEmpty
eval Abort p = VAbort

evals :: Tms -> Env -> Env
evals Idt p = p
evals (Comp s w) p = evals s (evals w p)
evals Epsilon p = Empty
evals (TCons s u) p = (evals s p) :> (eval u p)
evals (Fst s) p = tl (evals s p)

apply :: Val -> Val -> Val
apply (Clos f) v = f v
apply (Susp h e) v = Susp h (e :> XApp v)
apply VAbort v = VAbort

proj1 :: Val -> Val
proj1 (VPair t u) = t
proj1 (Susp h e) = Susp h (e :> XProj1)
proj1 VAbort = VAbort

proj2 :: Val -> Val
proj2 (VPair t u) = u
proj2 (Susp h e) = Susp h (e :> XProj2)
proj2 VAbort = VAbort

pelim :: Val -> Interval -> Val
pelim (VPIntr f) i = mapi 0 (select i) f
pelim (Susp h e) i = Susp h (e :> XPElim i)
pelim VAbort u = VAbort

mapi :: Int -> (Int -> Interval -> Interval) -> Val -> Val
mapi d i (Susp k e) = Susp k (fmap (select_elim d i) e)
mapi d i (Clos f) = Clos (select d i . f)
mapi d i VU = VU
mapi d i (VPi a b) = VPi (select d i a) (select d i . b)
mapi d i (VSig a b) = VSig (select d i a) (select d i . b)
mapi d i VUnit = VUnit
mapi d i (VPair a b) = VPair (select d i a) (select d i b)
mapi d i VConstant = VConstant
mapi d i (VPath a u t) = VPath (select (d+1) i a)
                                 (select d i u)
                                 (select d i t)
mapi d i (VPIntr f) = VPIntr (select (d+1) i f)
mapi d i VEmpty = VEmpty
mapi d i VAbort = VAbort

mapi_elim :: Int -> Interval -> XElim -> XElim
mapi_elim d i (XApp u) = XApp (mapi d i u)
mapi_elim d i XProj1 = XProj1
mapi_elim d i XProj2 = XProj2
mapi_elim d i (XPElim j) = XPElim (i d j)

select :: Interval -> Int -> Interval -> Interval
select i d I0 = I0
select i d I1 = I1
select i d (In j) | j > d = In (j-1)
                  | j == d = weaken d 0 i
                  | otherwise = In j

weaken :: Int -> Int -> Interval -> Interval
weaken d m I0 = I0
weaken d m I1 = I1
weaken d m (In i) | (i >= m) = In (i+d)
                  | otherwise = In i

data Nf
  = Neu Int (Bwd Elim)
  | NLam Nf
  | NU
  | NPi Nf Nf
  | NSig Nf Nf
  | NUnit
  | NPair Nf Nf
  | NConstant
  | NPath Nf Nf Nf
  | NPIntr Nf
  | NEmpty
  | NAbort
  deriving (Show, Eq)

data Elim
  = EApp Nf 
  | EProj1
  | EProj2
  | EPElim Interval
  deriving (Show, Eq)

instance Repr Nf where
  repr (Neu h e) = foldl repr_apply (repr h) e
  repr (NLam f) = Lam (repr f)
  repr NU = ElU
  repr (NPi a b) = ElPi (repr a) (repr b)
  repr (NSig a b) = ElSig (repr a) (repr b)
  repr NUnit = ElUnit
  repr (NPair a b) = Pair (repr a) (repr b)
  repr NConstant = Constant
  repr (NPath a u t) = ElPath (repr a) (repr u) (repr t)
  repr (NPIntr u) = PIntr (repr u)
  repr NEmpty = ElEmpty
  repr NAbort = Abort

repr_apply :: Tm -> Elim -> Tm
repr_apply t (EApp u) = tm_app t (repr u)
repr_apply t EProj1 = Proj1 t
repr_apply t EProj2 = Proj2 t
repr_apply t (EPElim u) = PElim t u

quote :: Int -> Val -> Nf
quote d (Susp h e) = Neu (d - h - 1)
                         (fmap (quote_elim d) e)
quote d (Clos f) = NLam (quote (d+1) (f (Susp d Empty)))
quote d VU = NU
quote d (VPi a b) = NPi (quote d a)
                        (quote (d+1) (b (Susp d Empty)))
quote d (VSig a b) = NSig (quote d a)
                          (quote (d+1) (b (Susp d Empty)))
quote d VUnit = NUnit
quote d (VPair a b) = NPair (quote d a) (quote d b)
quote d VConstant = NConstant
quote d (VPath a t u) = NPath (quote d a)
                              (quote d t)
                              (quote d u)
quote d (VPIntr u) = NPIntr (quote d u)
quote d VEmpty = NEmpty
quote d VAbort = NAbort

quote_elim :: Int -> XElim -> Elim
quote_elim d (XApp u) = EApp (quote d u)
quote_elim d XProj1 = EProj1
quote_elim d XProj2 = EProj2
quote_elim d (XPElim i) = EPElim i

idenv :: Int -> Env
idenv 0 = Empty
idenv n = idenv (n-1) :> Susp (n-1) Empty