NbE with case commutation for sum types

NbECaseCommute.hs

{-# language Strict, BangPatterns, LambdaCase, ViewPatterns, OverloadedStrings #-}
{-# options_ghc -Wincomplete-patterns #-}

-- NbE with case commutation for sum types.

import Data.Maybe
import Data.String

type Name = String

data Tm
  = Var Name
  | App Tm Tm
  | Lam Name Tm
  | Let Name Tm Tm
  | Unit
  | Case Tm Name Tm Name Tm
  | Inl Tm
  | Inr Tm
  deriving Show

data Val
  = VVar Name
  | VApp Val Val
  | VLam Name (Val -> Val)
  | VUnit
  | VCase Val Name (Val -> Val) Name (Val -> Val)
  | VInl Val
  | VInr Val

type Env = [(Name, Val)]

app :: Val -> Val -> Val
app t u = case t of
  VLam _ t        -> t u
  VCase t x l y r -> VCase t x (\v -> app (l v) u)
                             y (\v -> app (r v) u)
  t               -> VApp t u

vcase :: Val -> Name -> (Val -> Val) -> Name -> (Val -> Val) -> Val
vcase t x l y r = case t of
  VInl t              -> l t
  VInr t              -> r t
  VCase t x' l' y' r' -> VCase t x' (\u -> vcase (l' u) x l y r)
                                 y' (\u -> vcase (r' u) x l y r)
  t                   -> VCase t x l y r

eval :: Env -> Tm -> Val
eval env t = let
  go           = eval env
  goBind x t u = eval ((x, u):env) t
  in case t of
    Var x          -> fromJust $ lookup x env
    App t u        -> app (go t) (go u)
    Lam x t        -> VLam x (goBind x t)
    Let x t u      -> goBind x u (go t)
    Unit           -> VUnit
    Case t x l y r -> vcase (go t) x (goBind x l) y (goBind y r)
    Inl t          -> VInl (go t)
    Inr t          -> VInr (go t)

quote :: [Name] -> Val -> Tm
quote ns t = let
  go         = quote ns
  goBind x t = quote (x:ns) (t (VVar x))

  fsh x | elem x ns = fsh (x ++ "'")
        | True      = x

  in case t of
    VVar x                            -> Var x
    VApp t u                          -> App (go t) (go u)
    VLam (fsh -> x) t                 -> Lam x (goBind x t)
    VUnit                             -> Unit
    VCase t (fsh -> x) l (fsh -> y) r -> Case (go t) x (goBind x l) y (goBind y r)
    VInl t                            -> Inl (go t)
    VInr t                            -> Inr (go t)


nf :: Tm -> Tm
nf = quote [] . eval []

--------------------------------------------------------------------------------

instance IsString Tm where fromString = Var

infixl 7 $$
($$) = App

ite b t f = Case b "_" t "_" f
true      = Inl Unit
false     = Inr Unit
comp      = Lam "f" $ Lam "g" $ Lam "x" $ "f" $$ ("g" $$ "x")
not'      = Lam "b" $ ite "b" false true