Remove Neutral data type

diff --git a/CTT.hs b/CTT.hs
index 9324fe8fee06d0402c1ad3734a946d5293f10af4..bf775fc204f67a34863b8d50a765a994240cf5c6 100644 (file)
--- a/CTT.hs
+++ b/CTT.hs
@@ -78,9 +78,6 @@ mkApps :: Ter -> [Ter] -> Ter
 mkApps (Con l us) vs = Con l (us ++ vs)
 mkApps t ts          = foldl App t ts
 
--- mkLams :: [String] -> Ter -> Ter
--- mkLams bs t = foldr Lam t [ noLoc b | b <- bs ]
-
 mkWheres :: [Decls] -> Ter -> Ter
 mkWheres []     e = e
 mkWheres (d:ds) e = Where (mkWheres ds e) d
@@ -95,19 +92,25 @@ data Val = VU
          | VSigma Val Val
          | VSPair Val Val
          | VCon String [Val]
-         | VN Neutral
+         -- Neutral values:
+         | VVar String Val
+         | VFst Val
+         | VSnd Val
+         | VSplit Val Val
+         | VApp Val Val
   deriving Eq
 
--- neutral values
-data Neutral = VVar String Val
-             | VFst Neutral
-             | VSnd Neutral
-             | VSplit Val Neutral
-             | VApp Neutral Val
-  deriving Eq
+isNeutral :: Val -> Bool
+isNeutral v = case v of
+  VVar _ _   -> True
+  VFst v     -> isNeutral v
+  VSnd v     -> isNeutral v
+  VSplit _ v -> isNeutral v
+  VApp v _   -> isNeutral v
+  _          -> False
 
 mkVar :: Int -> Val -> Val
-mkVar k t = VN (VVar ('X' : show k) t)
+mkVar k = VVar ('X' : show k)
 
 --------------------------------------------------------------------------------
 -- | Environments
@@ -187,7 +190,7 @@ showTer1 t = case t of
   _        -> parens (showTer t)
 
 showDecls :: Decls -> Doc
-showDecls defs = hsep $ punctuate (char ',')
+showDecls defs = hsep $ punctuate comma
                       [ text x <+> equals <+> showTer d | ((x,_),(_,d)) <- defs ]
 
 instance Show Val where
@@ -202,25 +205,17 @@ showVal v = case v of
   VPi a b    -> text "Pi" <+> showVals [a,b]
   VSPair u v -> parens (showVal1 u <> comma <> showVal1 v)
   VSigma u v -> text "Sigma" <+> showVals [u,v]
-  VN n       -> showNeutral n
+  VApp u v   -> showVal u <+> showVal1 v
+  VSplit u v -> showVal u <+> showVal1 v
+  VVar x t   -> text x
+  VFst u     -> showVal u <> text ".1"
+  VSnd u     -> showVal u <> text ".2"
 showVal1 v = case v of
   VU        -> char 'U'
   VCon c [] -> text c
+  VVar{}    -> showVal v
   _         -> parens (showVal v)
 
 showVals :: [Val] -> Doc
 showVals = hsep . map showVal1
 
-instance Show Neutral where
-  show = render . showNeutral
-
-showNeutral, showNeutral1 :: Neutral -> Doc
-showNeutral n = case n of
-  VApp u v   -> showNeutral u <+> showVal1 v
-  VSplit u v -> showVal u <+> showNeutral1 v
-  VVar x t   -> text x
-  VFst u     -> showNeutral u <> text ".1"
-  VSnd u     -> showNeutral u <> text ".2"
-showNeutral1 n = case n of
-  VVar{} -> showNeutral n
-  _      -> parens (showNeutral n)

diff --git a/Eval.hs b/Eval.hs
index 5edca5f598f4000959925a6259f87c48a9243f08..27f08a92f14c8749a73c641fe207f0753e03b175 100644 (file)
--- a/Eval.hs
+++ b/Eval.hs
@@ -13,8 +13,8 @@ look x r@(PDef es r1) = case lookupIdent x es of
   Nothing -> look x r1
 
 lookType :: String -> Env -> Val
-lookType x (Pair rho ((y,_),VN (VVar _ a))) | x == y    = a
-                                            | otherwise = lookType x rho
+lookType x (Pair rho ((y,_),VVar _ a)) | x == y    = a
+                                       | otherwise = lookType x rho
 lookType x r@(PDef es r1) = case lookupIdent x es of
   Just (a,_) -> eval r a
   Nothing -> lookType x r1
@@ -45,14 +45,15 @@ app (Ter (Split _ _ nvs) e) (VCon name us) = case lookup name nvs of
   Just (xs,t) -> eval (pairs e (zip xs us)) t
   Nothing     -> error $ "app: Split with insufficient arguments; " ++
                          " missing case for " ++ name
-app u@(Ter (Split _ _ _) _) (VN v) = VN (VSplit u v)
-app (VN r) s = VN (VApp r s)
+app u@(Ter (Split _ _ _) _) v | isNeutral v = VSplit u v
+app r s | isNeutral r = VApp r s
+app _ _ = error "app"
 
 fstVal, sndVal :: Val -> Val
-fstVal (VSPair a b) = a
-fstVal (VN u)       = VN (VFst u)
-sndVal (VSPair a b) = b
-sndVal (VN u)       = VN (VSnd u)
+fstVal (VSPair a b)    = a
+fstVal u | isNeutral u = VFst u
+sndVal (VSPair a b)    = b
+sndVal u | isNeutral u = VSnd u
 
 -------------------------------------------------------------------------------
 -- | Conversion
@@ -82,16 +83,12 @@ conv k u v | u == v    = True
   (VSPair u v,VSPair u' v') -> conv k u u' && conv k v v'
   (VSPair u v,w)            -> conv k u (fstVal w) && conv k v (sndVal w)
   (w,VSPair u v)            -> conv k (fstVal w) u && conv k (sndVal w) v
-  (VN u,VN v)               -> convNeutral k u v
-  _                         -> False
-
-convNeutral :: Int -> Neutral -> Neutral -> Bool
-convNeutral k u v = case (u,v) of
-  (VFst u,VFst u')          -> convNeutral k u u'
-  (VSnd u,VSnd u')          -> convNeutral k u u'
-  (VApp u v,VApp u' v')     -> convNeutral k u u' && conv k v v'
-  (VSplit u v,VSplit u' v') -> conv k u u' && convNeutral k v v'
+  (VFst u,VFst u')          -> conv k u u'
+  (VSnd u,VSnd u')          -> conv k u u'
+  (VApp u v,VApp u' v')     -> conv k u u' && conv k v v'
+  (VSplit u v,VSplit u' v') -> conv k u u' && conv k v v'
   (VVar x _, VVar x' _)     -> x == x'
+  _                         -> False
 
 convEnv :: Int -> Env -> Env -> Bool
 convEnv k e e' = and $ zipWith (conv k) (valOfEnv e) (valOfEnv e')