From: Anders Date: Tue, 17 Mar 2015 13:59:45 +0000 (+0100) Subject: Remove Neutral data type X-Git-Url: https://git.ak3n.com/?a=commitdiff_plain;h=707f58a03b0878833c1c16d74c79028e862b5b2d;p=cubicaltt.git Remove Neutral data type --- diff --git a/CTT.hs b/CTT.hs index 9324fe8..bf775fc 100644 --- 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 5edca5f..27f08a9 100644 --- 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')