type Name = Text
type Index = Int
data Term
= Var Index
| Pi Term Term
| Lam Term
| Term :$ Term
| Ann Term Term
| Star
data Val
= VLam Term Env
| VPi Val Term Env
| VStar
| Ne Ne
data Ne = NV Index | Ne :$$ Val
type Env = [Val]
type Ctx = [Val]
env !! i
whnf (Pi d r) env = do
vd <- (whnf d env)
Just $ VPi vd r env
whnf (Lam t) env = Just $ VLam t env
whnf (f :$ a) env = do
vf <- whnf f env
va <- whnf a env
vf $$ va
whnf (Ann t _) env = whnf t env
whnf Star _ = Just VStar
whnf r (a : env)
Ne n $$ a = Just (Ne (n :$$ a))
_ $$ _ = Nothing
VLam t (ewk env)
wk (VPi d r env) = VPi (wk d) r (ewk env)
wk VStar = VStar
wk (Ne ne) = Ne $ nwk ne
map wk
map wk
NV (i + 1)
nwk (n :$$ v) = nwk n :$$ wk v
Ne (NV 0)
return ()
eq ctx VStar (VPi d1 r1 env1) (VPi d2 r2 env2) = do
eq ctx VStar d1 d2
whnfr1 <- (whnf r1 ((Ne (NV 0)) : ewk env1))
whnfr2 <- (whnf r2 ((Ne (NV 0)) : ewk env2))
eq (fresh : cwk ctx) VStar whnfr1 whnfr2
eq ctx (VPi _ r env) f g = do
vr <- whnf r ((Ne (NV 0)) : ewk env)
vf <- wk f $$ (Ne (NV 0))
vg <- wk g $$ (Ne (NV 0))
eq (fresh : cwk ctx) vr vf vg
eq ctx _ (Ne n1) (Ne n2) = neq ctx n1 n2 >> return ()
eq _ _ _ _ = Nothing
if i == j then ctx !! i else Nothing
neq ctx (n1 :$$ v1) (n2 :$$ v2) = do
VPi d r env <- neq ctx n1 n2
eq ctx d v1 v2
whnf r (v1 : env)
neq _ _ _ = Nothing