Here are terms and values, bidirectionally. Inevitably, I can’t decide what to call things and forgot what I did last time.
> data Dir = In | Ex
> data Phase = TT | VV
>
> data Tm :: {Dir, Phase} -> * -> * where
> L :: Scope p x -> Tm {In, p} x
> C :: Can (Tm {In, p} x) -> Tm {In, p} x
> N :: Tm {Ex, p} x -> Tm {In, p} x
> P :: x -> Tm {Ex, p} x
> V :: Int -> Tm {Ex, TT} x
> (:-) :: Tm {Ex, p} x -> Elim (Tm {In, p} x) -> Tm {Ex, p} x
> (:?) :: Tm {In, TT} x -> Tm {In, TT} x -> Tm {Ex, TT} x
>
> data Scope :: {Phase} -> * -> * where
> (:.) :: String -> Tm {In, TT} x -> Scope {TT} x
> H :: Env -> String -> Tm {In, TT} x -> Scope {VV} x
> K :: Tm {In, p} x -> Scope p x
>
> data Can :: * -> * where
> Set :: Can t
> Pi :: t -> t -> Can t
> deriving (Show, Eq)
>
> data Elim :: * -> * where
> A :: t -> Elim t
> deriving (Show, Eq)
And there’ll be more, no doubt. The parser is a bit scrappy.
The evaluator is idiombastic:
> ($-) :: VAL -> Elim VAL -> VAL
> L (K v) $- A _ = v
> L (H g _ t) $- A v = eval t (g :< v)
> N n $- e = N (n :- e)
> body :: Scope {TT} REF -> Env -> Scope {VV} REF
> body (K v) g = K (eval v g)
> body (x :. t) g = H g x t
> eval :: Tm {d, TT} REF -> Env -> VAL
> eval (L b) = (|L (body b)|)
> eval (C c) = (|C (eval ^$ c)|)
> eval (N n) = eval n
> eval (P x) = (|(pval x)|)
> eval (V i) = (!. i)
> eval (t :- e) = (|eval t $- (eval ^$ e)|)
> eval (t :? _) = eval t
where ^$ is a short infix name for traverse.