From 0c77a02756d273c1487a91d006f01e09676fb398 Mon Sep 17 00:00:00 2001 From: =?utf8?q?Anders=20M=C3=B6rtberg?= Date: Tue, 14 Apr 2015 23:03:53 +0200 Subject: [PATCH] Make undefined only occur as a declaration so that the type can be inferred --- CTT.hs | 8 ++++-- Eval.hs | 10 +++++-- Exp.cf | 1 + Resolver.hs | 67 +++++++++++++++++++++----------------------- TypeChecker.hs | 6 ++-- examples/integer.ctt | 3 +- 6 files changed, 49 insertions(+), 46 deletions(-) diff --git a/CTT.hs b/CTT.hs index c4940da..fb8d42e 100644 --- a/CTT.hs +++ b/CTT.hs @@ -95,7 +95,7 @@ data Ter = App Ter Ter -- labelled sum c1 A1s,..., cn Ans (assumes terms are constructors) | Sum Loc Ident [Label] -- undefined - | Undef Loc + | Undef Loc Ter -- Location and type -- Id type | IdP Ter Ter Ter @@ -155,6 +155,7 @@ data Val = VU -- Neutral values: | VVar Ident Val + | VUndef Loc Val | VFst Val | VSnd Val | VSplit Val Val @@ -165,7 +166,7 @@ data Val = VU isNeutral :: Val -> Bool isNeutral v = case v of - Ter (Undef _) _ -> True + VUndef _ _ -> True VVar _ _ -> True VFst v -> isNeutral v VSnd v -> isNeutral v @@ -311,7 +312,7 @@ showTer v = case v of showTers es <+> showFormula phi Split f _ _ _ -> text f Sum _ n _ -> text n - Undef _ -> text "undefined" + Undef _ _ -> text "undefined" IdP e0 e1 e2 -> text "IdP" <+> showTers [e0,e1,e2] Path i e -> char '<' <> text (show i) <> char '>' <+> showTer e AppFormula e phi -> showTer1 e <+> char '@' <+> showFormula phi @@ -359,6 +360,7 @@ showVal v = case v of text "->" <+> showVal e VSplit u v -> showVal u <+> showVal1 v VVar x t -> text x + VUndef _ _ -> text "undefined" VFst u -> showVal1 u <> text ".1" VSnd u -> showVal1 u <> text ".2" VIdP v0 v1 v2 -> text "IdP" <+> showVals [v0,v1,v2] diff --git a/Eval.hs b/Eval.hs index 695f39e..3118272 100644 --- a/Eval.hs +++ b/Eval.hs @@ -59,6 +59,7 @@ instance Nominal Val where support (VCon _ vs) = support vs support (VPCon _ a vs phi) = support (a,vs,phi) support (VVar _ v) = support v + support (VUndef _ v) = support v support (VApp u v) = support (u,v) support (VLam _ u v) = support (u,v) support (VAppFormula u phi) = support (u,phi) @@ -90,6 +91,7 @@ instance Nominal Val where VCon c vs -> VCon c (acti vs) VPCon c a vs phi -> pcon c (acti a) (acti vs) (acti phi) VVar x v -> VVar x (acti v) + VUndef x v -> VUndef x (acti v) VAppFormula u psi -> acti u @@ acti psi VApp u v -> app (acti u) (acti v) VLam x t u -> VLam x (acti t) (acti u) @@ -118,6 +120,7 @@ instance Nominal Val where VCon c vs -> VCon c (sw vs) VPCon c a vs phi -> VPCon c (sw a) (sw vs) (sw phi) VVar x v -> VVar x (sw v) + VUndef x v -> VUndef x (sw v) VAppFormula u psi -> VAppFormula (sw u) (sw psi) VApp u v -> VApp (sw u) (sw v) VLam x u v -> VLam x (sw u) (sw v) @@ -132,10 +135,10 @@ instance Nominal Val where eval :: Env -> Ter -> Val eval rho v = case v of - Undef{} -> Ter v rho U -> VU App r s -> app (eval rho r) (eval rho s) Var i -> look i rho + Undef l t -> VUndef l (eval rho t) Pi t@(Lam _ a _) -> VPi (eval rho a) (eval rho t) Lam{} -> Ter v rho Sigma t@(Lam _ a _) -> VSigma (eval rho a) (eval rho t) @@ -231,6 +234,7 @@ sndVal u = error $ "sndVal: " ++ show u ++ " is not neutral." inferType :: Val -> Val inferType v = case v of VVar _ t -> t + VUndef _ t -> t VFst t -> case inferType t of VSigma a _ -> a ty -> error $ "inferType: expected Sigma type for " ++ show v @@ -695,8 +699,8 @@ instance Convertible Val where let v = mkVar k (eval e a) in conv (k+1) (app u' v) (eval (Upd e (x,v)) u) (Ter (Split _ p _ _) e,Ter (Split _ p' _ _) e') -> (p == p') && conv k e e' - (Ter (Sum p _ _) e,Ter (Sum p' _ _) e') -> (p == p') && conv k e e' - (Ter (Undef p) e,Ter (Undef p') e') -> (p == p') && conv k e e' + (Ter (Sum p _ _) e,Ter (Sum p' _ _) e') -> (p == p') && conv k e e' + (VUndef p _,VUndef p' _) -> p == p' (VPi u v,VPi u' v') -> let w = mkVar k u in conv k u u' && conv (k+1) (app v w) (app v' w) diff --git a/Exp.cf b/Exp.cf index f65dc35..4c8d347 100644 --- a/Exp.cf +++ b/Exp.cf @@ -15,6 +15,7 @@ separator Imp ";" ; DeclDef. Decl ::= AIdent [Tele] ":" Exp "=" ExpWhere ; DeclData. Decl ::= "data" AIdent [Tele] "=" [Label] ; DeclSplit. Decl ::= AIdent [Tele] ":" Exp "=" "split" "{" [Branch] "}" ; +DeclUndef. Decl ::= AIdent [Tele] ":" Exp "=" "undefined" ; -- DeclMutual. Decl ::= "mutual" "{" [Decl] "}" ; separator Decl ";" ; diff --git a/Resolver.hs b/Resolver.hs index 5cb5ddc..2492949 100644 --- a/Resolver.hs +++ b/Resolver.hs @@ -87,8 +87,8 @@ updateModule mod e = e{envModule = mod} insertIdent :: (Ident,SymKind) -> Env -> Env insertIdent (n,var) e - | n == "_" || n == "undefined" = e - | otherwise = e{variables = (n,var) : variables e} + | n == "_" = e + | otherwise = e{variables = (n,var) : variables e} insertIdents :: [(Ident,SymKind)] -> Env -> Env insertIdents = flip $ foldr insertIdent @@ -111,12 +111,6 @@ insertAIdents = flip $ foldr insertAIdent getLoc :: (Int,Int) -> Resolver CTT.Loc getLoc l = CTT.Loc <$> asks envModule <*> pure l --- noLoc :: AIdent --- noLoc = AIdent ((0,0),"_") - --- resolveAIdent :: AIdent -> Resolver (Ident,CTT.Loc) --- resolveAIdent (AIdent (l,x)) = (x,) <$> getLoc l - unAIdent :: AIdent -> Ident unAIdent (AIdent (_,x)) = x @@ -130,23 +124,21 @@ resolveName (AIdent (l,x)) = do show l ++ " in module " ++ modName resolveVar :: AIdent -> Resolver Ter -resolveVar (AIdent (l,x)) - | (x == "_") || (x == "undefined") = CTT.Undef <$> getLoc l - | otherwise = do - modName <- asks envModule - vars <- asks variables - case lookup x vars of - Just Variable -> return $ CTT.Var x - Just Constructor -> return $ CTT.Con x [] - Just PConstructor -> throwError $ "The path constructor " ++ x ++ " is used as a" - ++ " variable at " ++ show l ++ " in " ++ modName - ++ " (path constructors should have their type in" - ++ " curly braces as first argument)" - Just Name -> - throwError $ "Name " ++ x ++ " used as a variable at position " ++ - show l ++ " in module " ++ modName - _ -> throwError $ "Cannot resolve variable " ++ x ++ " at position " ++ - show l ++ " in module " ++ modName +resolveVar (AIdent (l,x)) = do + modName <- asks envModule + vars <- asks variables + case lookup x vars of + Just Variable -> return $ CTT.Var x + Just Constructor -> return $ CTT.Con x [] + Just PConstructor -> throwError $ "The path constructor " ++ x ++ " is used as a" + ++ " variable at " ++ show l ++ " in " ++ modName + ++ " (path constructors should have their type in" + ++ " curly braces as first argument)" + Just Name -> + throwError $ "Name " ++ x ++ " used as a variable at position " ++ + show l ++ " in module " ++ modName + _ -> throwError $ "Cannot resolve variable " ++ x ++ " at position " ++ + show l ++ " in module " ++ modName lam :: (Ident,Exp) -> Resolver Ter -> Resolver Ter lam (a,t) e = CTT.Lam a <$> resolveExp t <*> local (insertVar a) e @@ -240,13 +232,13 @@ resolveDir Dir0 = return 0 resolveDir Dir1 = return 1 resolveFormula :: Formula -> Resolver C.Formula -resolveFormula (Dir d) = C.Dir <$> resolveDir d -resolveFormula (Atom i) = C.Atom <$> resolveName i -resolveFormula (Neg phi) = C.negFormula <$> resolveFormula phi -resolveFormula (Conj phi _ psi) = C.andFormula <$> resolveFormula phi - <*> resolveFormula psi -resolveFormula (Disj phi psi) = C.orFormula <$> resolveFormula phi - <*> resolveFormula psi +resolveFormula (Dir d) = C.Dir <$> resolveDir d +resolveFormula (Atom i) = C.Atom <$> resolveName i +resolveFormula (Neg phi) = C.negFormula <$> resolveFormula phi +resolveFormula (Conj phi _ psi) = + C.andFormula <$> resolveFormula phi <*> resolveFormula psi +resolveFormula (Disj phi psi) = + C.orFormula <$> resolveFormula phi <*> resolveFormula psi resolveBranch :: Branch -> Resolver CTT.Branch resolveBranch (OBranch (AIdent (_,lbl)) args e) = do @@ -296,13 +288,18 @@ resolveDecl d = case d of brs' <- local (insertVars (f:vars)) (mapM resolveBranch brs) body <- lams tele' (return $ CTT.Split f loc ty brs') return ((f,(a,body)),[(f,Variable)]) + DeclUndef (AIdent (l,f)) tele t -> do + let tele' = flattenTele tele + a <- binds CTT.Pi tele' (resolveExp t) + d <- CTT.Undef <$> getLoc l <*> pure a + return ((f,(a,d)),[(f,Variable)]) resolveDecls :: [Decl] -> Resolver ([[CTT.Decl]],[(Ident,SymKind)]) resolveDecls [] = return ([],[]) resolveDecls (d:ds) = do - (rtd,names) <- resolveDecl d - (rds,names') <- local (insertIdents names) $ resolveDecls ds - return ([rtd] : rds, names' ++ names) + (rtd,names) <- resolveDecl d + (rds,names') <- local (insertIdents names) $ resolveDecls ds + return ([rtd] : rds, names' ++ names) resolveModule :: Module -> Resolver ([[CTT.Decl]],[(Ident,SymKind)]) resolveModule (Module (AIdent (_,n)) _ decls) = diff --git a/TypeChecker.hs b/TypeChecker.hs index 25bedd1..588d22e 100644 --- a/TypeChecker.hs +++ b/TypeChecker.hs @@ -179,7 +179,6 @@ check a t = case (a,t) of (_,Where e d) -> do checkDecls d local (addDecls d) $ check a e - (_,Undef _) -> return () (VU,IdP a e0 e1) -> do (a0,a1) <- checkPath (constPath VU) a check a0 e0 @@ -354,8 +353,9 @@ checks _ _ = throwError "checks" -- infer the type of e infer :: Ter -> Typing Val infer e = case e of - U -> return VU -- U : U - Var n -> lookType n <$> asks env + U -> return VU -- U : U + Var n -> lookType n <$> asks env + Undef _ t -> evalTyping t App t u -> do c <- infer t case c of diff --git a/examples/integer.ctt b/examples/integer.ctt index da9b4b3..58e8d99 100644 --- a/examples/integer.ctt +++ b/examples/integer.ctt @@ -59,8 +59,7 @@ fromZK : (a : int) -> Id int (fromZ (toZ a)) a = split where rem : (n : nat) -> Id int (fromZ (toZ (neg n))) (neg n) = split zero -> zeroP' suc n -> refl int (neg (suc n)) - zeroP @ i -> temp - where temp : Id int (pos zero) (zeroP{int} @ i) = undefined + zeroP @ i -> sq @ i isoIntZ : Id U Z int = isoId Z int fromZ toZ fromZK toZK -- 2.34.1