diff --git a/doc/oplss.mng b/doc/oplss.mng index 1e356e6..dc1e2f0 100644 --- a/doc/oplss.mng +++ b/doc/oplss.mng @@ -1059,68 +1059,57 @@ that we can print warning messages. {[}Typecheck.hs{]}} Now that we have the type checking monad available, we can start our -implementation. For flexibility \texttt{inferType} and \texttt{checkType} will -\emph{both} be implemented by the same function, called \cd{tcTerm}. +implementation. -\begin{verbatim} -inferType :: Term -> TcMonad Type -inferType t = tcTerm t Nothing - -checkType :: Term -> Type -> TcMonad () -checkType tm ty = void $ tcTerm tm (Just ty) -\end{verbatim} - -The \texttt{tcTerm} function checks a term, producing its type. The -second argument is \texttt{Nothing} in inference mode and an expected -type in checking mode. +The general structure of the \cd{inferType} function starts with a pattern +match for the various syntactic forms. There are also several cases for +practical reasons (annotations, source code positions, etc.) and a few cases +for homework. If the form of the term does not match any of the forms of the +terms that we can synthesize types for, then the type checker produces an +error. \begin{verbatim} -tcTerm :: Term -> Maybe Type -> TcMonad Type -\end{verbatim} +inferType tm = case tm of + (Var x) -> ... -We combine these two functions into a single definition so that we can share -code between checking and inference modes. While none of the expression forms -of the core language can take advantage of this functionality, it is useful -for some extensions to the language. + TyType -> ... -The general structure of the \cd{tcTerm} function starts with a pattern match -for the various syntactic forms in inference mode: + (TyPi tyA bnd) -> ... -\begin{verbatim} -tcTerm (Var x) Nothing = ... - -tcTerm TyType Nothing = ... + (App t1 t2) -> ... -tcTerm (TyPi tyA bnd) Nothing = ... + (Ann tm ty) -> ... -tcTerm (App t1 t2) Nothing = ... + ... + _ -> Env.err [DS "Must have a type for", DD tm] \end{verbatim} +For checking, the general form of the function also + Mixed in here, we also have a pattern for lambda expressions in checking mode: \begin{verbatim} -tcTerm (Lam bnd) (Just (TyPi tyA bnd2)) = ... - -- pass in the Pi type for the lambda expression - -tcTerm (Lam _) (Just nf) = -- checking mode wrong type - err [DS "Lambda expression has a function type, not ", DD nf] +checkType tm ty = case tm of + (Lam bnd) -> case ty of + TyPi tyA bnd2 = ... + -- pass in the Pi type for the lambda expression + _ -> + Env.err [DS "Lambda expression has a function type, not ", DD ty] \end{verbatim} -There are also several cases for practical reasons (annotations, source code -positions, etc.) and a few cases for homework. - -Finally, the last case covers all other forms of checking mode, by -calling inference mode and making sure that the inferred type is equal -to the checked type. This case is the implementation of \rref{c-infer}. +Again there are several cases for practical reasons, plus cases for homework. +Finally, the last case covers all other forms of checking mode, by calling +inference mode and making sure that the inferred type is equal to the checked +type. This case is the implementation of \rref{c-infer}. \begin{verbatim} -tcTerm tm (Just ty) = do - ty' <- inferType tm - unless (Unbound.aeq ty' ty) $ - err [DS "Types don't match", DD ty, DS "and", DD ty'] - return ty + -- c-infer + tm -> do + ty' <- inferType tm + unless (Unbound.aeq ty' ty) $ + Env.err [DS "Types don't match", DD ty, DS "and", DD ty'] -} \end{verbatim} The function \texttt{aeq} ensures that the two types are alpha-equivalent. If @@ -1419,12 +1408,12 @@ whnf :: Term -> TcMonad Term In \texttt{version2} of the \href{version2/src/TypeCheck.hs}{implementation}, these functions are called in a few places: \begin{itemize} -\item \texttt{equate} is called at the -end of \texttt{tcTerm} +\item \texttt{equate} is called at the end of \texttt{checkType} to make sure +that the annotate type matches the inferred type. \item \texttt{ensurePi} is called in the \texttt{App} case -of \texttt{tcTerm} -\item \texttt{whnf} is called in \texttt{checkType}, before the call to - \texttt{tcTerm}, to make sure that we are using the head form in checking +of \texttt{inferType} +\item \texttt{whnf} is called in \texttt{checkType} + to make sure that we are using the head form of the type in checking mode. \end{itemize} @@ -1533,8 +1522,6 @@ For example, we can only type check the example below using the first (checking) \[ [[ |- \y. if y then (\x.x) else (\x. not x) <= Bool -> Bool -> Bool]] \] and we can only type check this next example using the second (inference) rule: \[ [[ x:Bool,y:Bool->Bool |- (if x then y else not) true => Bool ]] \] -Fortunately, it is not difficult to implement our type checking function so that it implements both rules. Indeed, because \cd{tcTerm} combines both judgments into a single Haskell function in the implementation, it is possible to implement both -rules with the same code. However, note that we can strengthen the specification of the type checking rule for \cd{if} by making the result type \texttt{A} depend on whether the diff --git a/doc/oplss.pdf b/doc/oplss.pdf index 9e61aca..00e7349 100644 Binary files a/doc/oplss.pdf and b/doc/oplss.pdf differ diff --git a/full/pi-forall.cabal b/full/pi-forall.cabal index e7a8c0c..ee29759 100644 --- a/full/pi-forall.cabal +++ b/full/pi-forall.cabal @@ -21,7 +21,7 @@ common shared-properties default-language: GHC2021 ghc-options: - -Wall -fno-warn-unused-matches -fno-warn-orphans -fno-warn-unused-top-binds -fno-warn-unused-imports -fno-warn-name-shadowing + -Wall -fno-warn-unused-matches -fno-warn-orphans -fno-warn-unused-top-binds -fno-warn-unused-imports -fno-warn-name-shadowing -Wno-unrecognised-pragmas default-extensions: DefaultSignatures DeriveAnyClass diff --git a/full/src/Environment.hs b/full/src/Environment.hs index 69ff773..85a7e92 100644 --- a/full/src/Environment.hs +++ b/full/src/Environment.hs @@ -9,7 +9,6 @@ module Environment lookupTy, lookupTyMaybe, lookupDef, - lookupRecDef, lookupHint , lookupTCon, lookupDCon, @@ -66,15 +65,15 @@ data SourceLocation where -- | Environment manipulation and accessing functions -- The context 'gamma' is a list data Env = Env - { -- | elaborated term and datatype declarations. - ctx :: [Decl], + { -- | elaborated term and datatype declarations + ctx :: [Entry], -- | how long the tail of "global" variables in the context is -- (used to supress printing those in error messages) globals :: Int, - -- | Type declarations (signatures): it's not safe to + -- | Type declarations: it's not safe to -- put these in the context until a corresponding term -- has been checked. - hints :: [Sig], + hints :: [Decl], -- | what part of the file we are in (for errors/warnings) sourceLocation :: [SourceLocation] } @@ -96,35 +95,35 @@ instance Disp Env where debugDisp e = vcat [debugDisp decl | decl <- ctx e] -- | Find a name's user supplied type signature. -lookupHint :: (MonadReader Env m) => TName -> m (Maybe Sig) +lookupHint :: (MonadReader Env m) => TName -> m (Maybe Decl) lookupHint v = do hints <- asks hints - return $ listToMaybe [ sig | sig <- hints, v == sigName sig] + return $ listToMaybe [ sig | sig <- hints, v == declName sig] -- | Find a name's type in the context. lookupTyMaybe :: (MonadReader Env m) => TName -> - m (Maybe Sig) + m (Maybe Decl) lookupTyMaybe v = do ctx <- asks ctx return $ go ctx where go [] = Nothing - go (TypeSig sig : ctx) - | v == sigName sig = Just sig + go (TypeDecl sig : ctx) + | v == declName sig = Just sig | otherwise = go ctx - go (Demote ep : ctx) = demoteSig ep <$> go ctx + go (Demote ep : ctx) = demoteDecl ep <$> go ctx go (_ : ctx) = go ctx -demoteSig :: Epsilon -> Sig -> Sig -demoteSig ep s = s { sigEp = min ep (sigEp s) } +demoteDecl :: Epsilon -> Decl -> Decl +demoteDecl ep s = s { declEp = min ep (declEp s) } -- | Find the type of a name specified in the context -- throwing an error if the name doesn't exist lookupTy :: - TName -> TcMonad Sig + TName -> TcMonad Decl lookupTy v = do x <- lookupTyMaybe v @@ -147,14 +146,6 @@ lookupDef v = do ctx <- asks ctx return $ listToMaybe [a | Def v' a <- ctx, v == v'] -lookupRecDef :: - (MonadReader Env m) => - TName -> - m (Maybe Term) -lookupRecDef v = do - ctx <- asks ctx - return $ listToMaybe [a | RecDef v' a <- ctx, v == v'] - -- | Find a type constructor in the context lookupTCon :: (MonadReader Env m, MonadError Err m) => @@ -177,10 +168,6 @@ lookupTCon v = do if v == v' then return (delta, Just cs) else scanGamma g - scanGamma ((DataSig v' delta) : g) = - if v == v' - then return (delta, Nothing) - else scanGamma g scanGamma (_ : g) = scanGamma g -- | Find a data constructor in the context, returns a list of @@ -200,7 +187,6 @@ lookupDConAll v = do Just c -> do more <- scanGamma g return $ (v', (delta, c)) : more - scanGamma ((DataSig v' delta) : g) = scanGamma g scanGamma (_ : g) = scanGamma g -- | Given the name of a data constructor and the type that it should @@ -231,17 +217,17 @@ lookupDCon c tname = do -- | Extend the context with a new binding -extendCtx :: (MonadReader Env m) => Decl -> m a -> m a +extendCtx :: (MonadReader Env m) => Entry -> m a -> m a extendCtx d = local (\m@Env{ctx = cs} -> m {ctx = d : cs}) -- | Extend the context with a list of bindings -extendCtxs :: (MonadReader Env m) => [Decl] -> m a -> m a +extendCtxs :: (MonadReader Env m) => [Entry] -> m a -> m a extendCtxs ds = local (\m@Env {ctx = cs} -> m {ctx = ds ++ cs}) -- | Extend the context with a list of bindings, marking them as "global" -extendCtxsGlobal :: (MonadReader Env m) => [Decl] -> m a -> m a +extendCtxsGlobal :: (MonadReader Env m) => [Entry] -> m a -> m a extendCtxsGlobal ds = local ( \m@Env {ctx = cs} -> @@ -252,12 +238,12 @@ extendCtxsGlobal ds = ) -- | Extend the context with a telescope -extendCtxTele :: (MonadReader Env m, MonadIO m, MonadError Err m) => [Decl] -> m a -> m a +extendCtxTele :: (MonadReader Env m, MonadIO m, MonadError Err m) => [Entry] -> m a -> m a extendCtxTele [] m = m extendCtxTele (Def x t2 : tele) m = extendCtx (Def x t2) $ extendCtxTele tele m -extendCtxTele (TypeSig sig : tele) m = - extendCtx (TypeSig sig) $ extendCtxTele tele m +extendCtxTele (TypeDecl sig : tele) m = + extendCtx (TypeDecl sig) $ extendCtxTele tele m extendCtxTele ( _ : tele) m = err [DS "Invalid telescope ", DD tele] @@ -273,11 +259,11 @@ extendCtxMods :: (MonadReader Env m) => [Module] -> m a -> m a extendCtxMods mods k = foldr extendCtxMod k mods -- | Get the complete current context -getCtx :: MonadReader Env m => m [Decl] +getCtx :: MonadReader Env m => m [Entry] getCtx = asks ctx -- | Get the prefix of the context that corresponds to local variables. -getLocalCtx :: MonadReader Env m => m [Decl] +getLocalCtx :: MonadReader Env m => m [Entry] getLocalCtx = do g <- asks ctx glen <- asks globals @@ -293,7 +279,7 @@ getSourceLocation :: MonadReader Env m => m [SourceLocation] getSourceLocation = asks sourceLocation -- | Add a type hint -extendHints :: (MonadReader Env m) => Sig -> m a -> m a +extendHints :: (MonadReader Env m) => Decl -> m a -> m a extendHints h = local (\m@Env {hints = hs} -> m {hints = h : hs}) -- | An error that should be reported to the user diff --git a/full/src/Equal.hs b/full/src/Equal.hs index 56ba625..0393f00 100644 --- a/full/src/Equal.hs +++ b/full/src/Equal.hs @@ -177,11 +177,7 @@ whnf (Var x) = do maybeDef <- Env.lookupDef x case maybeDef of (Just d) -> whnf d - _ -> do - maybeRecDef <- Env.lookupRecDef x - case maybeRecDef of - (Just d) -> whnf d - _ -> return (Var x) + _ -> return (Var x) whnf (App t1 t2) = do nf <- whnf t1 @@ -235,7 +231,7 @@ whnf tm = return tm -- | 'Unify' the two terms, producing a list of Defs -- If there is an obvious mismatch, this function produces an error -- If either term is "ambiguous" just ignore. -unify :: [TName] -> Term -> Term -> TcMonad [Decl] +unify :: [TName] -> Term -> Term -> TcMonad [Entry] unify ns tx ty = do txnf <- whnf tx tynf <- whnf ty diff --git a/full/src/Modules.hs b/full/src/Modules.hs index 1888bb2..c4f0fc0 100644 --- a/full/src/Modules.hs +++ b/full/src/Modules.hs @@ -23,7 +23,7 @@ getModules [FilePath] -> String -> m [Module] getModules prefixes top = do toParse <- gatherModules prefixes [ModuleImport top] - flip evalStateT emptyConstructorNames $ mapM reparse toParse + flip evalStateT initialConstructorNames $ mapM reparse toParse data ModuleInfo = ModuleInfo { diff --git a/full/src/Parser.hs b/full/src/Parser.hs index 856b0e3..d987855 100644 --- a/full/src/Parser.hs +++ b/full/src/Parser.hs @@ -3,7 +3,7 @@ -- | A parsec-based parser for the concrete syntax module Parser ( - parseModuleFile, + parseModuleFile, parseModuleImports, parseExpr, expr, @@ -19,7 +19,7 @@ import qualified Unbound.Generics.LocallyNameless as Unbound import Text.Parsec hiding (State,Empty) import Text.Parsec.Expr(Operator(..),Assoc(..),buildExpressionParser) -import qualified LayoutToken as Token +import qualified LayoutToken as Token import Control.Monad.State.Lazy hiding (join) import Control.Monad.Except ( MonadError(throwError) ) @@ -99,13 +99,13 @@ Optional components in this BNF are marked with < > A -> B - Get parsed as (x:A) -> B, with an internal name for x + Get parsed as (_:A) -> B, with a wildcard name for the binder - Nondependent product types, like: A * B - Get parsed as { x:A | B }, with an internal name for x + Get parsed as { _:A | B }, with a wildcard name for the binder - You can collapse lambdas, like: @@ -121,6 +121,12 @@ Optional components in this BNF are marked with < > -} + +-- | Default name (for parsing 'A -> B' as '(_:A) -> B') +wildcardName :: TName +wildcardName = Unbound.string2Name "_" + + liftError :: (MonadError e m) => Either e a -> m a liftError (Left e) = throwError e liftError (Right a) = return a @@ -130,8 +136,8 @@ parseModuleFile :: (MonadError ParseError m, MonadIO m) => ConstructorNames -> S parseModuleFile cnames name = do liftIO $ putStrLn $ "Parsing File " ++ show name contents <- liftIO $ readFile name - liftError $ Unbound.runFreshM $ - flip evalStateT cnames + liftError $ Unbound.runFreshM $ + flip evalStateT cnames (runParserT (do { whiteSpace; v <- moduleDef;eof; return v}) [] name contents) @@ -139,21 +145,23 @@ parseModuleFile cnames name = do parseModuleImports :: (MonadError ParseError m, MonadIO m) => String -> m Module parseModuleImports name = do contents <- liftIO $ readFile name - liftError $ Unbound.runFreshM $ - flip evalStateT emptyConstructorNames $ + liftError $ Unbound.runFreshM $ +{- SOLN DATA -} + flip evalStateT initialConstructorNames $ (runParserT (do { whiteSpace; moduleImports }) [] name contents) -- | Test an 'LParser' on a String. testParser :: ConstructorNames -> LParser t -> String -> Either ParseError t -testParser cn parser str = Unbound.runFreshM $ +testParser cn parser str = Unbound.runFreshM $ +{- SOLN DATA -} flip evalStateT cn $ runParserT (do { whiteSpace; v <- parser; eof; return v}) [] "" str -- | Parse an expression. parseExpr :: String -> Either ParseError Term -parseExpr = testParser emptyConstructorNames expr +parseExpr = testParser initialConstructorNames expr -- * Lexer definitions type LParser a = ParsecT @@ -196,10 +204,10 @@ piforallStyle = Token.LanguageDef ,"axiom" ,"TRUSTME" ,"PRINTME" - ,"ord" - ,"Bool", "True", "False" + ,"ord" + ,"Bool", "True", "False" ,"if","then","else" - ,"Unit", "()" + ,"Unit", "()" ] , Token.reservedOpNames = ["!","?","\\",":",".",",","<", "=", "+", "-", "*", "^", "()", "_","|","{", "}"] @@ -217,14 +225,14 @@ whiteSpace = Token.whiteSpace tokenizer variable :: LParser TName variable = - do i <- identifier + do i <- identifier cnames <- get - if (i `S.member` (tconNames cnames) || + if (i `S.member` (tconNames cnames) || i `S.member` (dconNames cnames)) then fail "Expected a variable, but a constructor was found" else return $ Unbound.string2Name i - + wildcard :: LParser TName wildcard = reservedOp "_" >> return wildcardName @@ -233,14 +241,14 @@ varOrWildcard = try wildcard <|> variable dconstructor :: LParser DataConName dconstructor = - do i <- identifier + do i <- identifier cnames <- get if (i `S.member` dconNames cnames) then return i else if (i `S.member` tconNames cnames) then fail "Expected a data constructor, but a type constructor was found." else fail "Expected a constructor, but a variable was found" - + tconstructor :: LParser TyConName tconstructor = do i <- identifier @@ -249,7 +257,7 @@ tconstructor = then return i else if (i `S.member` dconNames cnames) then fail "Expected a type constructor, but a data constructor was found." - else fail "Expected a constructor, but a variable was found" + else fail "Expected a constructor, but a variable was found" -- variables or zero-argument constructors @@ -267,7 +275,7 @@ colon, dot, comma :: LParser () colon = Token.colon tokenizer >> return () dot = Token.dot tokenizer >> return () comma = Token.comma tokenizer >> return () - + reserved,reservedOp :: String -> LParser () reserved = Token.reserved tokenizer reservedOp = Token.reservedOp tokenizer @@ -281,7 +289,7 @@ natural :: LParser Int natural = fromInteger <$> Token.natural tokenizer natenc :: LParser Term -natenc = encode <$> natural +natenc = encode <$> natural where encode 0 = DataCon "Zero" [] encode n = DataCon "Succ" [Arg Rel (encode (n-1))] @@ -292,7 +300,7 @@ moduleImports = do modName <- identifier reserved "where" imports <- layout importDef (return ()) - return $ Module modName imports [] emptyConstructorNames + return $ Module modName imports [] initialConstructorNames moduleDef :: LParser Module moduleDef = do @@ -309,54 +317,54 @@ importDef = do reserved "import" >> (ModuleImport <$> importName) where importName = identifier telescope :: LParser Telescope -telescope = do +telescope = do bindings <- telebindings return $ Telescope (foldr id [] bindings) where - -telebindings :: LParser [[Decl] -> [Decl]] + +telebindings :: LParser [[Entry] -> [Entry]] telebindings = many teleBinding where annot = do (x,ty) <- try ((,) <$> varOrWildcard <*> (colon >> expr)) <|> ((,) <$> (Unbound.fresh wildcardName) <*> expr) - return (TypeSig (Sig x Rel ty):) + return (TypeDecl (Decl x Rel ty):) imp = do v <- varOrWildcard colon t <- expr - return (TypeSig (Sig v Irr t):) - + return (TypeDecl (Decl v Irr t):) + equal = do v <- variable reservedOp "=" t <- expr return (Def v t :) - - teleBinding :: LParser ([Decl] -> [Decl]) + + teleBinding :: LParser ([Entry] -> [Entry]) teleBinding = ( parens annot <|> try (brackets imp) <|> brackets equal) "binding" - + --- --- Top level declarations --- -decl,sigDef,valDef :: LParser Decl -decl = (try dataDef) <|> sigDef <|> valDef +decl,declDef,valDef :: LParser Entry +decl = try dataDef <|> declDef <|> valDef -- datatype declarations. -dataDef :: LParser Decl +dataDef :: LParser Entry dataDef = do reserved "data" name <- identifier params <- telescope colon TyType <- typen - modify (\cnames -> - cnames{ tconNames = S.insert name + modify (\cnames -> + cnames{ tconNames = S.insert name (tconNames cnames) }) reserved "where" cs <- layout constructorDef (return ()) @@ -373,11 +381,11 @@ constructorDef = do return $ ConstructorDef pos cname args "Constructor" - -sigDef = do + +declDef = do n <- try (variable >>= \v -> colon >> return v) ty <- expr - return (mkSig n ty) + return (mkDecl n ty) valDef = do n <- try (do {n <- variable; reservedOp "="; return n}) @@ -400,13 +408,13 @@ printme = reserved "PRINTME" *> return (PrintMe ) refl :: LParser Term refl = do reserved "Refl" - return $ Refl + return $ Refl -- Expressions expr,term,factor :: LParser Term - + -- expr is the toplevel expression grammar expr = do p <- getPosition @@ -415,19 +423,19 @@ expr = do [ifix AssocLeft "=" TyEq], [ifixM AssocRight "->" mkArrowType], [ifixM AssocRight "*" mkTupleType] - ] + ] ifix assoc op f = Infix (reservedOp op >> return f) assoc ifixM assoc op f = Infix (reservedOp op >> f) assoc - mkArrowType = + mkArrowType = do n <- Unbound.fresh wildcardName - return $ \tyA tyB -> + return $ \tyA tyB -> TyPi Rel tyA (Unbound.bind n tyB) - mkTupleType = + mkTupleType = do n <- Unbound.fresh wildcardName - return $ \tyA tyB -> + return $ \tyA tyB -> TyCon sigmaName [Arg Rel tyA, Arg Rel $ Lam Rel (Unbound.bind n tyB)] - + -- A "term" is either a function application or a constructor -- application. Breaking it out as a seperate category both -- eliminates left-recursion in ( := ) and @@ -439,36 +447,36 @@ arg = try (Arg Irr <$> brackets expr) <|> Arg Rel <$> factor dconapp :: LParser Term -dconapp = do +dconapp = do c <- dconstructor args <- many arg - return $ DataCon c args - -tconapp :: LParser Term + return $ DataCon c args + +tconapp :: LParser Term tconapp = do c <- tconstructor ts <- many arg return $ TyCon c ts - + funapp :: LParser Term -funapp = do +funapp = do f <- factor foldl' app f <$> many bfactor where - bfactor = ((,Irr) <$> brackets expr) + bfactor = ((,Irr) <$> brackets expr) <|> ((,Rel) <$> factor) app e1 (e2,ep) = App e1 (Arg ep e2) factor = choice [ varOrCon "a variable or nullary data constructor" - + , typen "Type" , lambda "a lambda" , try letPairExp "a let pair" , letExpr "a let" - , natenc "a literal" + , natenc "a literal" , caseExpr "a case" , substExpr "a subst" , refl "Refl" @@ -477,16 +485,16 @@ factor = choice [ varOrCon "a variable or nullary data constructor" , printme "PRINTME" , impProd "an implicit function type" - , bconst "a constant" - , ifExpr "an if expression" - , sigmaTy "a sigma type" - + , bconst "a constant" + , ifExpr "an if expression" + , sigmaTy "a sigma type" + , expProdOrAnnotOrParens "an explicit function type or annotated expression" ] impOrExpVar :: LParser (TName, Epsilon) -impOrExpVar = try ((,Irr) <$> (brackets variable)) +impOrExpVar = try ((,Irr) <$> (brackets variable)) <|> (,Rel) <$> variable @@ -503,12 +511,12 @@ lambda = do reservedOp "\\" binds <- many1 impOrExpVar dot body <- expr - return $ foldr lam body binds + return $ foldr lam body binds where - lam (x, ep) m = Lam ep (Unbound.bind x m) - + lam (x, ep) m = Lam ep (Unbound.bind x m) + + - bconst :: LParser Term @@ -521,17 +529,17 @@ bconst = choice [reserved "Bool" >> return (TyCon boolName []), ifExpr :: LParser Term -ifExpr = +ifExpr = do reserved "if" a <- expr reserved "then" b <- expr reserved "else" c <- expr - return (Case a [Match $ Unbound.bind (PatCon trueName []) b, + return (Case a [Match $ Unbound.bind (PatCon trueName []) b, Match $ Unbound.bind (PatCon falseName []) c]) - + -- letExpr :: LParser Term @@ -565,10 +573,10 @@ letPairExp = do -- These have the syntax [x:a] -> b or [a] -> b . impProd :: LParser Term impProd = - do (x,tyA) <- brackets + do (x,tyA) <- brackets (try ((,) <$> variable <*> (colon >> expr)) <|> ((,) <$> Unbound.fresh wildcardName <*> expr)) - reservedOp "->" + reservedOp "->" tyB <- expr return $ TyPi Irr tyA (Unbound.bind x tyB) @@ -609,9 +617,9 @@ expProdOrAnnotOrParens = (do b <- afterBinder return $ TyPi Rel a (Unbound.bind x b)) Colon a b -> return $ Ann a b - - Comma a b -> - return $ DataCon prodName [Arg Rel a, Arg Rel b] + + Comma a b -> + return $ DataCon prodName [Arg Rel a, Arg Rel b] Nope a -> return a @@ -628,14 +636,14 @@ pattern :: LParser Pattern pattern = try (PatCon <$> dconstructor <*> many arg_pattern) <|> atomic_pattern where - arg_pattern = ((,Irr) <$> brackets pattern) + arg_pattern = ((,Irr) <$> brackets pattern) <|> ((,Rel) <$> atomic_pattern) - paren_pattern = do + paren_pattern = do pattern >>= \p -> ( (reservedOp ")" >> pure p) - <|> reservedOp "," *> (atomic_pattern >>= \q -> + <|> reservedOp "," *> (atomic_pattern >>= \q -> pure (PatCon prodName [(p, Rel), (q, Rel)])) - ) + ) atomic_pattern = reservedOp "(" *> paren_pattern <|> reserved "True" *> pure (PatCon trueName []) <|> reserved "False" *> pure (PatCon falseName []) @@ -650,8 +658,8 @@ pattern = try (PatCon <$> dconstructor <*> many arg_pattern) match :: LParser Match -match = - do pat <- pattern +match = + do pat <- pattern reservedOp "->" pos <- getPosition body <- expr @@ -664,9 +672,9 @@ caseExpr = do scrut <- expr reserved "of" alts <- layout match (return ()) - return $ Case (Pos pos scrut) alts - - + return $ Case (Pos pos scrut) alts + + -- subst e0 by e1 substExpr :: LParser Term @@ -675,16 +683,16 @@ substExpr = do a <- expr reserved "by" b <- expr - return $ Subst a b + return $ Subst a b contra :: LParser Term contra = do reserved "contra" witness <- expr - return $ Contra witness + return $ Contra witness -sigmaTy :: LParser Term +sigmaTy :: LParser Term sigmaTy = do reservedOp "{" x <- variable @@ -695,5 +703,5 @@ sigmaTy = do reservedOp "}" return $ TyCon sigmaName [Arg Rel a, Arg Rel (Lam Rel (Unbound.bind x b))] - - + + diff --git a/full/src/PrettyPrint.hs b/full/src/PrettyPrint.hs index 5a18a39..2b8d850 100644 --- a/full/src/PrettyPrint.hs +++ b/full/src/PrettyPrint.hs @@ -120,11 +120,11 @@ instance Disp Module instance Disp ModuleImport -instance Disp Decl +instance Disp Entry -instance Disp [Decl] +instance Disp [Entry] -instance Disp Sig +instance Disp Decl instance Disp Arg @@ -160,24 +160,23 @@ instance Display Module where instance Display ModuleImport where display (ModuleImport i) = pure $ PP.text "import" <+> disp i -instance Display [Decl] where +instance Display [Entry] where display ds = do dd <- mapM display ds pure $ PP.vcat dd -instance Display Sig where - display sig = do - dn <- display (sigName sig) - dt <- display (sigType sig) +instance Display Decl where + display decl = do + dn <- display (declName decl) + dt <- display (declType decl) pure $ dn <+> PP.text ":" <+> dt -instance Display Decl where +instance Display Entry where display (Def n term) = do dn <- display n dt <- display term pure $ dn <+> PP.text "=" <+> dt - display (RecDef n f) = display (Def n f) - display (TypeSig sig) = display sig + display (TypeDecl decl) = display decl display (Demote ep) = return mempty display (Data n params constructors) = do dn <- display n @@ -191,12 +190,6 @@ instance Display Decl where ) 2 (PP.vcat dc) - display (DataSig t delta) = do - dt <- display t - dd <- display delta - - pure $ PP.text "data" <+> dt <+> dd <+> PP.colon - <+> PP.text "Type" instance Display ConstructorDef where diff --git a/full/src/Syntax.hs b/full/src/Syntax.hs index 3c3d305..f474485 100644 --- a/full/src/Syntax.hs +++ b/full/src/Syntax.hs @@ -25,16 +25,8 @@ import Data.Function (on) -- and alpha-equality function. The abstract type `Name` from -- this library is indexed by the AST type that this variable -- is a name for. -type TName = Unbound.Name Term - --- | module names -type ModuleName = String - --- | type constructor names -type TyConName = String --- | data constructor names -type DataConName = String +type TName = Unbound.Name Term ----------------------------------------- @@ -143,12 +135,15 @@ data Pattern ----------------------------------------- +-- | module names +type ModuleName = String + -- | A Module has a name, a list of imports, a list of declarations, -- and a set of constructor names (which affect parsing). data Module = Module { moduleName :: ModuleName, moduleImports :: [ModuleImport], - moduleEntries :: [Decl] , + moduleEntries :: [Entry] , moduleConstructors :: ConstructorNames } deriving (Show, Generic, Typeable, Unbound.Alpha) @@ -158,36 +153,40 @@ newtype ModuleImport = ModuleImport ModuleName deriving (Show, Eq, Generic, Typeable) deriving anyclass (Unbound.Alpha) --- | A type declaration (or type signature) -data Sig = Sig {sigName :: TName , sigEp :: Epsilon , sigType :: Type} +-- | A type declaration (or type declnature) +data Decl = Decl {declName :: TName , declEp :: Epsilon , declType :: Type} deriving (Show, Generic, Typeable, Unbound.Alpha, Unbound.Subst Term) -- | Declare the type of a term -mkSig :: TName -> Type -> Decl -mkSig n ty = TypeSig (Sig n Rel ty) - --- | Declarations are the components of modules -data Decl - = -- | Declaration for the type of a term - TypeSig Sig - | -- | The definition of a particular name, must +mkDecl :: TName -> Type -> Entry +mkDecl n ty = TypeDecl (Decl n Rel ty) + +-- | Entries are the components of modules +data Entry + = -- | Declaration for the type of a term 'x : A' + TypeDecl Decl + | -- | The definition of a particular name, must 'x = a' -- already have a type declaration in scope Def TName Term - | -- | A potentially (recursive) definition of - -- a particular name, must be declared - RecDef TName Term -- | Adjust the context for relevance checking | Demote Epsilon - | -- | Declaration for a datatype including all of - -- its data constructors + | -- | Datatype definition (must be at the module level) Data TyConName Telescope [ConstructorDef] - | -- | An abstract view of a datatype. Does - -- not include any information about its data - -- constructors - DataSig TyConName Telescope deriving (Show, Generic, Typeable) deriving anyclass (Unbound.Alpha, Unbound.Subst Term) + +----------------------------------------- + +-- * Datatypes + +----------------------------------------- +-- | type constructor names +type TyConName = String + +-- | data constructor names +type DataConName = String + -- | The names of type/data constructors used in the module data ConstructorNames = ConstructorNames { tconNames :: Set String, @@ -200,36 +199,19 @@ data ConstructorDef = ConstructorDef SourcePos DataConName Telescope deriving (Show, Generic) deriving anyclass (Unbound.Alpha, Unbound.Subst Term) --- * Telescopes +-- ** Telescopes -- | A telescope is like a first class context. It is a list of -- assumptions, binding each variable in terms that appear -- later in the list. -- For example -- Delta = [ x:Type , y:x, y = w ] -newtype Telescope = Telescope [Decl] +newtype Telescope = Telescope [Entry] deriving (Show, Generic) deriving anyclass (Unbound.Alpha, Unbound.Subst Term) - --- * Auxiliary functions on syntax - --- | empty set of constructor names -emptyConstructorNames :: ConstructorNames -emptyConstructorNames = ConstructorNames initialTCNames initialDCNames - --- | Default name for '_' occurring in patterns -wildcardName :: TName -wildcardName = Unbound.string2Name "_" - --- | Partial inverse of Pos -unPos :: Term -> Maybe SourcePos -unPos (Pos p _) = Just p -unPos _ = Nothing - --- | Tries to find a Pos inside a term, otherwise just gives up. -unPosFlaky :: Term -> SourcePos -unPosFlaky t = fromMaybe (newPos "unknown location" 0 0) (unPos t) +----------------------------------------- +-- Definitions related to datatypes -- | Is this the syntax of a literal (natural) number isNumeral :: Term -> Maybe Int @@ -244,9 +226,9 @@ isPatVar :: Pattern -> Bool isPatVar (PatVar _) = True isPatVar _ = False -------------------------------------------------------------------- --- Prelude declarations for datatypes - +-- | built-in set of constructor names +initialConstructorNames :: ConstructorNames +initialConstructorNames = ConstructorNames initialTCNames initialDCNames -- | prelude names for built-in datatypes sigmaName :: TyConName @@ -269,7 +251,8 @@ initialTCNames = Set.fromList [sigmaName, boolName, tyUnitName] initialDCNames :: Set DataConName initialDCNames = Set.fromList [prodName, trueName, falseName, litUnitName] -preludeDataDecls :: [Decl] + +preludeDataDecls :: [Entry] preludeDataDecls = [ Data sigmaName sigmaTele [prodConstructorDef] , Data tyUnitName (Telescope []) [unitConstructorDef] @@ -283,27 +266,76 @@ preludeDataDecls = unitConstructorDef = ConstructorDef internalPos litUnitName (Telescope []) -- Sigma-type - sigmaTele = Telescope [TypeSig sigA, TypeSig sigB] - prodConstructorDef = ConstructorDef internalPos prodName (Telescope [TypeSig sigX, TypeSig sigY]) - sigA = Sig aName Rel TyType - sigB = Sig bName Rel (TyPi Rel (Var aName) (Unbound.bind xName TyType)) - sigX = Sig xName Rel (Var aName) - sigY = Sig yName Rel (App (Var bName) (Arg Rel (Var xName))) + sigmaTele = Telescope [TypeDecl declA, TypeDecl declB] + prodConstructorDef = ConstructorDef internalPos prodName (Telescope [TypeDecl declX, TypeDecl declY]) + declA = Decl aName Rel TyType + declB = Decl bName Rel (TyPi Rel (Var aName) (Unbound.bind xName TyType)) + declX = Decl xName Rel (Var aName) + declY = Decl yName Rel (App (Var bName) (Arg Rel (Var xName))) aName = Unbound.string2Name "a" bName = Unbound.string2Name "b" ------------------ + internalPos :: SourcePos + internalPos = initialPos "prelude" + + + +----------------------------------------- +-- * Auxiliary functions on syntax +----------------------------------------- + + +-- | Remove source positions and type annotations from the top level of a term +strip :: Term -> Term +strip (Pos _ tm) = strip tm +strip (Ann tm _) = strip tm +strip tm = tm + +-- | Partial inverse of Pos +unPos :: Term -> Maybe SourcePos +unPos (Pos p _) = Just p +unPos _ = Nothing + +-- | Tries to find a Pos inside a term, otherwise just gives up. +unPosFlaky :: Term -> SourcePos +unPosFlaky t = fromMaybe (newPos "unknown location" 0 0) (unPos t) + + + +----------------------------------------- +-- * Unbound library +----------------------------------------- -- We use the unbound-generics library to mark the binding occurrences of -- variables in the syntax. That allows us to automatically derive -- functions for alpha-equivalence, free variables and substitution -- using generic programming. +-- | Determine when two terms are alpha-equivalent (see below) +aeq :: Term -> Term -> Bool +aeq = Unbound.aeq + +-- | Calculate the free variables of a term +fv :: Term -> [Unbound.Name Term] +fv = Unbound.toListOf Unbound.fv + +-- | subst x b a means to replace x with b in a +-- i.e. a [ b / x ] +subst :: TName -> Term -> Term -> Term +subst = Unbound.subst + +-- | in a binder "x.a" replace x with b +instantiate :: Unbound.Bind TName Term -> Term -> Term +instantiate bnd a = Unbound.instantiate bnd [a] + +-- | in a binder "x.a" replace x with a fresh name +unbind :: (Unbound.Fresh m) => Unbound.Bind TName Term -> m (TName, Term) +unbind = Unbound.unbind ------------------ -- * Alpha equivalence and free variables --- Among other things, the Alpha class enables the following +-- The Unbound library's Alpha class enables the following -- functions: -- -- Compare terms for alpha equivalence -- aeq :: Alpha a => a -> a -> Bool @@ -313,23 +345,23 @@ preludeDataDecls = -- unbind :: (Alpha p, Alpha t, Fresh m) => Bind p t -> m (p, t) -- For Terms, we'd like Alpha equivalence to ignore --- source positions and type annotations. --- We can add these special cases to the definition of `aeq'` --- and then defer all other cases to the generic version of --- the function (Unbound.gaeq). +-- source positions and type annotations. So we make sure to +-- remove them before calling the generic operation. instance Unbound.Alpha Term where - aeq' ctx (Ann a _) b = Unbound.aeq' ctx a b - aeq' ctx a (Ann b _) = Unbound.aeq' ctx a b - aeq' ctx (Pos _ a) b = Unbound.aeq' ctx a b - aeq' ctx a (Pos _ b) = Unbound.aeq' ctx a b - aeq' ctx a b = (Unbound.gaeq ctx `on` from) a b + aeq' :: Unbound.AlphaCtx -> Term -> Term -> Bool + aeq' ctx a b = (Unbound.gaeq ctx `on` from) (strip a) (strip b) + -- For example, all occurrences of annotations and source positions -- are ignored by this definition. --- >>> Unbound.aeq (Pos internalPos (Ann TyBool Type)) TyBool --- True +-- '(Bool : Type)' is alpha-equivalent to 'Bool' +-- >>> aeq (Ann TyBool TyType) TyBool + +-- '(Bool, Bool:Type)' is alpha-equivalent to (Bool, Bool) +-- >>> aeq (Prod TyBool (Ann TyBool TyType)) (Prod TyBool TyBool) + -- At the same time, the generic operation equates terms that differ only -- in the names of bound variables. @@ -350,7 +382,7 @@ idx = Lam Rel (Unbound.bind xName (Var xName)) idy :: Term idy = Lam Rel (Unbound.bind yName (Var yName)) --- >>> Unbound.aeq idx idy +-- >>> aeq idx idy -- True @@ -379,14 +411,6 @@ pi2 :: Term pi2 = TyPi Rel TyBool (Unbound.bind yName (Var yName)) -- >>> Unbound.aeq (Unbound.subst xName TyBool pi1) pi2 --- True --- - ---------------- --- | Bridge function to calculate the free variables of a term - -fv :: Term -> [Unbound.Name Term] -fv = Unbound.toListOf Unbound.fv ----------------- @@ -410,15 +434,18 @@ instance Unbound.Alpha SourcePos where acompare' _ _ _ = EQ -- Substitutions ignore source positions -instance Unbound.Subst b SourcePos where subst _ _ = id; substs _ = id; substBvs _ _ = id +instance Unbound.Subst b SourcePos where + subst _ _ = id + substs _ = id + substBvs _ _ = id --- Internally generated source positions -internalPos :: SourcePos -internalPos = initialPos "internal" -- * Constructor Names +-- ConstructorNames are sets, so they also do not have an instance of the +-- Generic class available so we cannot automatically define their +-- Alpha and Subst instances. instance Unbound.Alpha ConstructorNames where aeq' _ a1 a2 = a1 == a2 fvAny' _ _ = pure diff --git a/full/src/TypeCheck.hs b/full/src/TypeCheck.hs index c6eb792..1cb272f 100644 --- a/full/src/TypeCheck.hs +++ b/full/src/TypeCheck.hs @@ -1,7 +1,6 @@ {- pi-forall -} -- | The main routines for type-checking -{-# OPTIONS_GHC -Wno-unrecognised-pragmas #-} {-# HLINT ignore "Use forM_" #-} module TypeCheck (tcModules, inferType, checkType) where @@ -25,314 +24,309 @@ import Unbound.Generics.LocallyNameless.Internal.Fold qualified as Unbound import Unbound.Generics.LocallyNameless.Unsafe (unsafeUnbind) --- | Infer/synthesize the type of a term -inferType :: Term -> TcMonad Type -inferType t = tcTerm t Nothing - --- | Check that the given term has the expected type -checkType :: Term -> Type -> TcMonad () -checkType tm (Pos _ ty) = checkType tm ty -- ignore source positions/annotations -checkType tm (Ann ty _) = checkType tm ty -checkType tm ty = do - nf <- Equal.whnf ty - void $ tcTerm tm (Just nf) - - --- | Make sure that the term is a "type" (i.e. that it has type 'Type') -tcType :: Term -> TcMonad () -tcType tm = void $ Env.withStage Irr $ checkType tm TyType --------------------------------------------------------------------- --- | Combined type checking/inference function --- The second argument is 'Just expectedType' in checking mode and 'Nothing' in inference mode --- In either case, this function returns the type of the term -tcTerm :: Term -> Maybe Type -> TcMonad Type --- i-var -tcTerm t@(Var x) Nothing = do - sig <- Env.lookupTy x -- make sure the variable is accessible - Env.checkStage (sigEp sig) - return (sigType sig) --- i-type -tcTerm TyType Nothing = return TyType --- i-pi -tcTerm (TyPi ep tyA bnd) Nothing = do - (x, tyB) <- Unbound.unbind bnd - tcType tyA - Env.extendCtx (TypeSig (Sig x ep tyA)) (tcType tyB) - return TyType --- c-lam: check the type of a function -tcTerm (Lam ep1 bnd) (Just (TyPi ep2 tyA bnd2)) = do - -- unbind the variables in the lambda expression and pi type - (x, body,_,tyB) <- Unbound.unbind2Plus bnd bnd2 --- epsilons should match up - unless (ep1 == ep2) $ Env.err [DS "In function definition, expected", DD ep2, DS "parameter", DD x, - DS "but found", DD ep1, DS "instead."] - -- check the type of the body of the lambda expression - Env.extendCtx (TypeSig (Sig x ep1 tyA)) (checkType body tyB) - return (TyPi ep1 tyA bnd2) -tcTerm (Lam _ _) (Just nf) = - Env.err [DS "Lambda expression should have a function type, not", DD nf] --- i-app -tcTerm (App t1 t2) Nothing = do - ty1 <- inferType t1 - let ensurePi = Equal.ensurePi - - (ep1, tyA, bnd) <- ensurePi ty1 - unless (ep1 == argEp t2) $ Env.err - [DS "In application, expected", DD ep1, DS "argument but found", - DD t2, DS "instead." ] - -- if the argument is Irrelevant, resurrect the context - (if ep1 == Irr then Env.extendCtx (Demote Rel) else id) $ - checkType (unArg t2) tyA - return (Unbound.instantiate bnd [unArg t2]) - +-- | Infer/synthesize the type of a term +inferType :: Term -> TcMonad Type +inferType t = case t of + -- i-var + (Var x) -> do + decl <- Env.lookupTy x -- make sure the variable is accessible + Env.checkStage (declEp decl) + return (declType decl) + + -- i-type + TyType -> return TyType + + -- i-pi + (TyPi ep tyA bnd) -> do + (x, tyB) <- Unbound.unbind bnd + tcType tyA + Env.extendCtx (TypeDecl (Decl x ep tyA)) (tcType tyB) + return TyType + + -- i-app + (App t1 t2) -> do + ty1 <- inferType t1 + let ensurePi = Equal.ensurePi + + (ep1, tyA, bnd) <- ensurePi ty1 + unless (ep1 == argEp t2) $ Env.err + [DS "In application, expected", DD ep1, DS "argument but found", + DD t2, DS "instead." ] + -- if the argument is Irrelevant, resurrect the context + (if ep1 == Irr then Env.extendCtx (Demote Rel) else id) $ + checkType (unArg t2) tyA + return (Unbound.instantiate bnd [unArg t2]) + --- i-ann -tcTerm (Ann tm ty) Nothing = do - tcType ty - checkType tm ty - return ty + -- i-ann + (Ann tm ty) -> do + tcType ty + checkType tm ty + return ty --- practicalities --- remember the current position in the type checking monad -tcTerm (Pos p tm) mTy = - Env.extendSourceLocation p tm $ tcTerm tm mTy --- ignore term, just return type annotation -tcTerm TrustMe (Just ty) = return ty + -- Practicalities + -- remember the current position in the type checking monad + (Pos p tm) -> + Env.extendSourceLocation p tm $ inferType tm --- i-unit -tcTerm TyUnit Nothing = return TyType -tcTerm LitUnit Nothing = return TyUnit - --- i-bool -tcTerm TyBool Nothing = return TyType - + -- Extensions to the core language + -- i-unit + TyUnit -> return TyType + LitUnit -> return TyUnit --- i-true/false -tcTerm (LitBool b) Nothing = do - return TyBool + -- i-bool + TyBool -> return TyType + -- i-true/false + (LitBool b) -> return TyBool --- c-if -tcTerm t@(If t1 t2 t3) mty = do - case mty of - Just ty -> do - checkType t1 TyBool - dtrue <- Equal.unify [] t1 (LitBool True) - dfalse <- Equal.unify [] t1 (LitBool False) - Env.extendCtxs dtrue $ checkType t2 ty - Env.extendCtxs dfalse $ checkType t3 ty - return ty - Nothing -> do + -- i-if + (If t1 t2 t3) -> do checkType t1 TyBool ty <- inferType t2 checkType t3 ty - return ty - - -tcTerm (Let rhs bnd) mty = do - (x, body) <- Unbound.unbind bnd - aty <- inferType rhs - ty <- Env.extendCtxs [mkSig x aty, Def x rhs] $ - tcTerm body mty - case mty of - Just _ -> return ty - Nothing -> return $ Unbound.subst x rhs ty - --- TyType constructor application -tcTerm (TyCon c params) Nothing = do - (Telescope delta, _) <- Env.lookupTCon c - unless (length params == length delta) $ - Env.err - [ DS "Datatype constructor", - DD c, - DS $ - "should have " ++ show (length delta) - ++ "parameters, but was given", - DD (length params) - ] - tcArgTele params delta - return TyType - --- Data constructor application --- we don't know the expected type, so see if there --- is only one datacon of that name that takes no --- parameters -tcTerm t@(DataCon c args) Nothing = do - matches <- Env.lookupDConAll c - case matches of - [(tname, (Telescope [], ConstructorDef _ _ (Telescope deltai)))] -> do - let numArgs = length deltai - unless (length args == numArgs) $ - Env.err - [ DS "Constructor", - DS c, - DS "should have", - DD numArgs, - DS "data arguments, but was given", - DD (length args), - DS "arguments." - ] - tcArgTele args deltai - return $ TyCon tname [] - - [_] -> + return ty + -- i-eq + (TyEq a b) -> do + aTy <- inferType a + checkType b aTy + return TyType + + -- i-sigma + (TySigma tyA bnd) -> do + (x, tyB) <- Unbound.unbind bnd + tcType tyA + Env.extendCtx (mkDecl x tyA) $ tcType tyB + return TyType + + -- Type constructor application + (TyCon c params) -> do + (Telescope delta, _) <- Env.lookupTCon c + unless (length params == length delta) $ Env.err - [ DS "Cannot infer the parameters to data constructors.", - DS "Add an annotation." + [ DS "Datatype constructor", + DD c, + DS $ + "should have " ++ show (length delta) + ++ "parameters, but was given", + DD (length params) ] - _ -> Env.err [DS "Ambiguous data constructor", DS c] - --- we know the expected type of the data constructor --- so look up its type in the context -tcTerm t@(DataCon c args) (Just ty) = do - case ty of - (TyCon tname params) -> do - (Telescope delta, Telescope deltai) <- Env.lookupDCon c tname - let isTypeSig :: Decl -> Bool - isTypeSig (TypeSig _) = True - isTypeSig _ = False - let numArgs = length (filter isTypeSig deltai) - unless (length args == numArgs) $ + tcArgTele params delta + return TyType + + -- Data constructor application + -- we don't know the expected type, so see if there + -- is only one datacon of that name that takes no + -- parameters + (DataCon c args) -> do + matches <- Env.lookupDConAll c + case matches of + [(tname, (Telescope [], ConstructorDef _ _ (Telescope deltai)))] -> do + let numArgs = length deltai + unless (length args == numArgs) $ + Env.err + [ DS "Constructor", + DS c, + DS "should have", + DD numArgs, + DS "data arguments, but was given", + DD (length args), + DS "arguments." + ] + tcArgTele args deltai + return $ TyCon tname [] + [_] -> Env.err - [ DS "Constructor", - DS c, - DS "should have", - DD numArgs, - DS "data arguments, but was given", - DD (length args), - DS "arguments." + [ DS "Cannot infer the parameters to data constructors.", + DS "Add an annotation." ] - newTele <- substTele delta params deltai - tcArgTele args newTele - return ty - _ -> - Env.err [DS "Unexpected type", DD ty, DS "for data constructor", DD t] - --- Must have an annotation for Case -tcTerm t@(Case scrut alts) (Just ty) = do - sty <- inferType scrut - scrut' <- Equal.whnf scrut - (c, args) <- Equal.ensureTCon sty - let checkAlt (Match bnd) = do - (pat, body) <- Unbound.unbind bnd - -- add variables from pattern to context - -- could fail if branch is in-accessible - decls <- declarePat pat Rel (TyCon c args) - -- add defs to the contents from scrut = pat - -- could fail if branch is in-accessible - decls' <- Equal.unify [] scrut' (pat2Term pat) - Env.extendCtxs (decls ++ decls') $ checkType body ty - - return () - let pats = map (\(Match bnd) -> fst (unsafeUnbind bnd)) alts - mapM_ checkAlt alts - exhaustivityCheck scrut' sty pats - return ty - -tcTerm (TyEq a b) Nothing = do - aTy <- inferType a - checkType b aTy - return TyType -tcTerm Refl (Just ty@(TyEq a b)) = do - Equal.equate a b - return ty -tcTerm Refl (Just ty) = - Env.err [DS "Refl annotated with", DD ty] -tcTerm t@(Subst a b) (Just ty) = do - -- infer the type of the proof 'b' - tp <- inferType b - -- make sure that it is an equality between m and n - (m, n) <- Equal.ensureTyEq tp - -- if either side is a variable, add a definition to the context - edecl <- Equal.unify [] m n - -- if proof is a variable, add a definition to the context - pdecl <- Equal.unify [] b Refl - _ <- Env.extendCtxs (edecl ++ pdecl) $ checkType a ty - return ty -tcTerm t@(Contra p) (Just ty) = do - ty' <- inferType p - (a, b) <- Equal.ensureTyEq ty' - a' <- Equal.whnf a - b' <- Equal.whnf b - case (a', b') of - - (DataCon da _, DataCon db _) - | da /= db -> - return ty - - (LitBool b1, LitBool b2) - | b1 /= b2 -> - return ty - (_, _) -> - Env.err - [ DS "I can't tell that", - DD a, - DS "and", - DD b, - DS "are contradictory" - ] - + _ -> Env.err [DS "Ambiguous data constructor", DS c] -tcTerm t@(TySigma tyA bnd) Nothing = do - (x, tyB) <- Unbound.unbind bnd - tcType tyA - Env.extendCtx (mkSig x tyA) $ tcType tyB - return TyType + -- cannot synthesize the type of the term + tm -> + Env.err [DS "Must have a type for", DD tm] -tcTerm t@(Prod a b) (Just ty) = do - case ty of - (TySigma tyA bnd) -> do - (x, tyB) <- Unbound.unbind bnd - checkType a tyA - Env.extendCtxs [mkSig x tyA, Def x a] $ checkType b tyB - return (TySigma tyA (Unbound.bind x tyB)) - _ -> - Env.err - [ DS "Products must have Sigma Type", - DD ty, - DS "found instead" - ] - +------------------------------------------------------------------------- -tcTerm t@(LetPair p bnd) (Just ty) = do - ((x, y), body) <- Unbound.unbind bnd - pty <- inferType p - pty' <- Equal.whnf pty - case pty' of - TySigma tyA bnd' -> do - let tyB = Unbound.instantiate bnd' [Var x] - decl <- Equal.unify [] p (Prod (Var x) (Var y)) - Env.extendCtxs ([mkSig x tyA, mkSig y tyB] ++ decl) $ - checkType body ty - return ty - _ -> Env.err [DS "Scrutinee of LetPair must have Sigma type"] +-- | Make sure that the term is a "type" (i.e. that it has type 'Type') +tcType :: Term -> TcMonad () +tcType tm = Env.withStage Irr $ checkType tm TyType +------------------------------------------------------------------------- +-- | Check that the given term has the expected type +checkType :: Term -> Type -> TcMonad () +checkType tm ty' = do + ty <- Equal.whnf ty' + case tm of + -- c-lam: check the type of a function + (Lam ep1 bnd) -> case ty of + (TyPi ep2 tyA bnd2) -> do + -- unbind the variables in the lambda expression and pi type + (x, body,_,tyB) <- Unbound.unbind2Plus bnd bnd2 +-- epsilons should match up + unless (ep1 == ep2) $ Env.err [DS "In function definition, expected", DD ep2, DS "parameter", DD x, + DS "but found", DD ep1, DS "instead."] + -- check the type of the body of the lambda expression + Env.extendCtx (TypeDecl (Decl x ep1 tyA)) (checkType body tyB) + _ -> Env.err [DS "Lambda expression should have a function type, not", DD ty] + + -- Practicalities + (Pos p tm) -> + Env.extendSourceLocation p tm $ checkType tm ty + + TrustMe -> return () + + PrintMe -> do + gamma <- Env.getLocalCtx + Env.warn [DS "Unmet obligation.\nContext:", DD gamma, + DS "\nGoal:", DD ty] + + -- Extensions to the core language + -- c-if + (If t1 t2 t3) -> do + checkType t1 TyBool + dtrue <- Equal.unify [] t1 (LitBool True) + dfalse <- Equal.unify [] t1 (LitBool False) + Env.extendCtxs dtrue $ checkType t2 ty + Env.extendCtxs dfalse $ checkType t3 ty + + -- c-let + (Let rhs bnd) -> do + (x, body) <- Unbound.unbind bnd + aty <- inferType rhs + Env.extendCtxs [mkDecl x aty, Def x rhs] $ + checkType body ty + -- c-data + -- we know the expected type of the data constructor + -- so look up its type in the context + (DataCon c args) -> do + case ty of + (TyCon tname params) -> do + (Telescope delta, Telescope deltai) <- Env.lookupDCon c tname + let isTypeDecl :: Entry -> Bool + isTypeDecl (TypeDecl _) = True + isTypeDecl _ = False + let numArgs = length (filter isTypeDecl deltai) + unless (length args == numArgs) $ + Env.err + [ DS "Constructor", + DS c, + DS "should have", + DD numArgs, + DS "data arguments, but was given", + DD (length args), + DS "arguments." + ] + newTele <- substTele delta params deltai + tcArgTele args newTele + _ -> + Env.err [DS "Unexpected type", DD ty, DS "for data constructor", DD tm] + + (Case scrut alts) -> do + sty <- inferType scrut + scrut' <- Equal.whnf scrut + (c, args) <- Equal.ensureTCon sty + let checkAlt (Match bnd) = do + (pat, body) <- Unbound.unbind bnd + -- add variables from pattern to context + -- could fail if branch is in-accessible + decls <- declarePat pat Rel (TyCon c args) + -- add defs to the contents from scrut = pat + -- could fail if branch is in-accessible + decls' <- Equal.unify [] scrut' (pat2Term pat) + Env.extendCtxs (decls ++ decls') $ checkType body ty + + return () + let pats = map (\(Match bnd) -> fst (unsafeUnbind bnd)) alts + mapM_ checkAlt alts + exhaustivityCheck scrut' sty pats + + -- c-refl + Refl -> case ty of + (TyEq a b) -> Equal.equate a b + _ -> Env.err [DS "Refl annotated with", DD ty] + -- c-subst + (Subst a b) -> do + -- infer the type of the proof 'b' + tp <- inferType b + -- make sure that it is an equality between m and n + (m, n) <- Equal.ensureTyEq tp + -- if either side is a variable, add a definition to the context + edecl <- Equal.unify [] m n + -- if proof is a variable, add a definition to the context + pdecl <- Equal.unify [] b Refl + Env.extendCtxs (edecl ++ pdecl) $ checkType a ty + -- c-contra + (Contra p) -> do + ty' <- inferType p + (a, b) <- Equal.ensureTyEq ty' + a' <- Equal.whnf a + b' <- Equal.whnf b + case (a', b') of + + (DataCon da _, DataCon db _) + | da /= db -> + return () + + (LitBool b1, LitBool b2) + | b1 /= b2 -> + return () + (_, _) -> + Env.err + [ DS "I can't tell that", + DD a, + DS "and", + DD b, + DS "are contradictory" + ] + + -- c-prod + (Prod a b) -> do + case ty of + (TySigma tyA bnd) -> do + (x, tyB) <- Unbound.unbind bnd + checkType a tyA + Env.extendCtxs [mkDecl x tyA, Def x a] $ checkType b tyB + _ -> + Env.err + [ DS "Products must have Sigma Type", + DD ty, + DS "found instead" + ] + -tcTerm PrintMe (Just ty) = do - gamma <- Env.getLocalCtx - Env.warn [DS "Unmet obligation.\nContext:", DD gamma, - DS "\nGoal:", DD ty] - return ty + -- c-letpair + (LetPair p bnd) -> do + ((x, y), body) <- Unbound.unbind bnd + pty <- inferType p + pty' <- Equal.whnf pty + case pty' of + TySigma tyA bnd' -> do + let tyB = Unbound.instantiate bnd' [Var x] + decl <- Equal.unify [] p (Prod (Var x) (Var y)) + Env.extendCtxs ([mkDecl x tyA, mkDecl y tyB] ++ decl) $ + checkType body ty + _ -> Env.err [DS "Scrutinee of LetPair must have Sigma type"] + --- c-infer -tcTerm tm (Just ty) = do - ty' <- inferType tm - Equal.equate ty' ty - return ty' + -- c-infer + tm -> do + ty' <- inferType tm + Equal.equate ty' ty + -tcTerm tm Nothing = - Env.err [DS "Must have a type annotation to check", DD tm] --------------------------------------------------------------------- -- helper functions for type checking -- | Create a Def if either side normalizes to a single variable -def :: Term -> Term -> TcMonad [Decl] +def :: Term -> Term -> TcMonad [Entry] def t1 t2 = do nf1 <- Equal.whnf t1 nf2 <- Equal.whnf t2 @@ -347,13 +341,13 @@ def t1 t2 = do -- helper functions for datatypes -- | type check a list of data constructor arguments against a telescope -tcArgTele :: [Arg] -> [Decl] -> TcMonad () +tcArgTele :: [Arg] -> [Entry] -> TcMonad () tcArgTele [] [] = return () tcArgTele args (Def x ty : tele) = do -- ensure that the equality is provable at this point Equal.equate (Var x) ty tcArgTele args tele -tcArgTele (Arg ep1 tm : terms) (TypeSig (Sig x ep2 ty) : tele) +tcArgTele (Arg ep1 tm : terms) (TypeDecl (Decl x ep2 ty) : tele) | ep1 == ep2 = do Env.withStage ep1 $ checkType tm ty tele' <- doSubst [(x, tm)] tele @@ -376,11 +370,11 @@ tcArgTele _ tele = -- This is used to instantiate the parameters of a data constructor -- to find the types of its arguments. -- The first argument should only contain 'Rel' type declarations. -substTele :: [Decl] -> [Arg] -> [Decl] -> TcMonad [Decl] +substTele :: [Entry] -> [Arg] -> [Entry] -> TcMonad [Entry] substTele tele args = doSubst (mkSubst tele (map unArg args)) where mkSubst [] [] = [] - mkSubst (TypeSig (Sig x Rel _) : tele') (tm : tms) = + mkSubst (TypeDecl (Decl x Rel _) : tele') (tm : tms) = (x, tm) : mkSubst tele' tms mkSubst _ _ = error "Internal error: substTele given illegal arguments" @@ -388,7 +382,7 @@ substTele tele args = doSubst (mkSubst tele (map unArg args)) -- Propagate the given substitution through the telescope, potentially -- reworking the constraints -doSubst :: [(TName, Term)] -> [Decl] -> TcMonad [Decl] +doSubst :: [(TName, Term)] -> [Entry] -> TcMonad [Entry] doSubst ss [] = return [] doSubst ss (Def x ty : tele') = do let tx' = Unbound.substs ss (Var x) @@ -396,19 +390,19 @@ doSubst ss (Def x ty : tele') = do decls1 <- Equal.unify [] tx' ty' decls2 <- Env.extendCtxs decls1 (doSubst ss tele') return $ decls1 ++ decls2 -doSubst ss (TypeSig sig : tele') = do - tynf <- Equal.whnf (Unbound.substs ss (sigType sig)) - let sig' = sig{sigType = tynf} +doSubst ss (TypeDecl decl : tele') = do + tynf <- Equal.whnf (Unbound.substs ss (declType decl)) + let decl' = decl{declType = tynf} tele'' <- doSubst ss tele' - return $ TypeSig sig' : tele'' + return $ TypeDecl decl' : tele'' doSubst _ tele = Env.err [DS "Invalid telescope", DD tele] ----------------------------------------------------------- -- | Create a binding for each of the variables in the pattern -declarePat :: Pattern -> Epsilon -> Type -> TcMonad [Decl] -declarePat (PatVar x) ep ty = return [TypeSig (Sig x ep ty)] +declarePat :: Pattern -> Epsilon -> Type -> TcMonad [Entry] +declarePat (PatVar x) ep ty = return [TypeDecl (Decl x ep ty)] declarePat (PatCon dc pats) Rel ty = do (tc,params) <- Equal.ensureTCon ty (Telescope delta, Telescope deltai) <- Env.lookupDCon dc tc @@ -419,12 +413,12 @@ declarePat pat Irr _ty = -- | Given a list of pattern arguments and a telescope, create a binding for -- each of the variables in the pattern, -declarePats :: DataConName -> [(Pattern, Epsilon)] -> [Decl] -> TcMonad [Decl] +declarePats :: DataConName -> [(Pattern, Epsilon)] -> [Entry] -> TcMonad [Entry] declarePats dc pats (Def x ty : tele) = do let ds1 = [Def x ty] ds2 <- Env.extendCtxs ds1 $ declarePats dc pats tele return (ds1 ++ ds2) -declarePats dc ((pat, _) : pats) (TypeSig (Sig x ep ty) : tele) = do +declarePats dc ((pat, _) : pats) (TypeDecl (Decl x ep ty) : tele) = do ds1 <- declarePat pat ep ty let tm = pat2Term pat tele' <- doSubst [(x,tm)] tele @@ -448,16 +442,16 @@ pat2Term (PatCon dc pats) = DataCon dc (pats2Terms pats) -- | Check all of the types contained within a telescope -tcTypeTele :: [Decl] -> TcMonad () +tcTypeTele :: [Entry] -> TcMonad () tcTypeTele [] = return () tcTypeTele (Def x tm : tl) = do ty1 <- Env.withStage Irr $ inferType (Var x) Env.withStage Irr $ checkType tm ty1 let decls = [Def x tm] Env.extendCtxs decls $ tcTypeTele tl -tcTypeTele (TypeSig sig : tl) = do - tcType (sigType sig) - Env.extendCtx (TypeSig sig) $ tcTypeTele tl +tcTypeTele (TypeDecl decl : tl) = do + tcType (declType decl) + Env.extendCtx (TypeDecl decl) $ tcTypeTele tl tcTypeTele tele = Env.err [DS "Invalid telescope: ", DD tele] @@ -483,11 +477,11 @@ tcModules = foldM tcM [] -- | Typecheck an entire module. tcModule :: - -- | List of already checked modules (including their Decls). + -- | List of already checked modules (including their entries). [Module] -> -- | Module to check. Module -> - -- | The same module with all Decls checked and elaborated. + -- | The same module with all entries checked and elaborated. TcMonad Module tcModule defs m' = do checkedEntries <- @@ -499,23 +493,23 @@ tcModule defs m' = do return $ m' {moduleEntries = checkedEntries} where d `tcE` m = do - -- Extend the Env per the current Decl before checking - -- subsequent Decls. + -- Extend the Env per the current Entry before checking + -- subsequent entries. x <- tcEntry d case x of AddHint hint -> Env.extendHints hint m - -- Add decls to the Decls to be returned + -- Add decls to the entries to be returned AddCtx decls -> (decls ++) <$> Env.extendCtxsGlobal decls m -- Get all of the defs from imported modules (this is the env to check current module in) importedModules = filter (\x -> ModuleImport (moduleName x) `elem` moduleImports m') defs --- | The Env-delta returned when type-checking a top-level Decl. +-- | The Env-delta returned when type-checking a top-level Entry. data HintOrCtx - = AddHint Sig - | AddCtx [Decl] + = AddHint Decl + | AddCtx [Entry] -- | Check each sort of declaration in a module -tcEntry :: Decl -> TcMonad HintOrCtx +tcEntry :: Entry -> TcMonad HintOrCtx tcEntry (Def n term) = do oldDef <- Env.lookupDef n maybe tc die oldDef @@ -525,22 +519,20 @@ tcEntry (Def n term) = do case lkup of Nothing -> do ty <- inferType term - return $ AddCtx [TypeSig (Sig n Rel ty), Def n term] - Just sig -> + return $ AddCtx [TypeDecl (Decl n Rel ty), Def n term] + Just decl -> let handler (Env.Err ps msg) = throwError $ Env.Err ps (msg $$ msg') msg' = disp [ DS "When checking the term", DD term, - DS "against the signature", - DD sig + DS "against the type", + DD decl ] in do - Env.extendCtx (TypeSig sig) $ checkType term (sigType sig) `catchError` handler - if n `elem` fv term - then return $ AddCtx [TypeSig sig, RecDef n term] - else return $ AddCtx [TypeSig sig, Def n term] + Env.extendCtx (TypeDecl decl) $ checkType term (declType decl) `catchError` handler + return $ AddCtx [TypeDecl decl, Def n term] die term' = Env.extendSourceLocation (unPosFlaky term) term $ Env.err @@ -549,14 +541,14 @@ tcEntry (Def n term) = do DS "Previous definition was", DD term' ] -tcEntry (TypeSig sig) = do - duplicateTypeBindingCheck sig - tcType (sigType sig) - return $ AddHint sig +tcEntry (TypeDecl decl) = do + duplicateTypeBindingCheck decl + tcType (declType decl) + return $ AddHint decl tcEntry (Demote ep) = return (AddCtx [Demote ep]) --- rule Decl_data +-- rule Entry_data tcEntry (Data t (Telescope delta) cs) = do -- Check that the telescope for the datatype definition is well-formed @@ -565,7 +557,7 @@ tcEntry (Data t (Telescope delta) cs) = --- for each data constructor is wellfomed, and elaborate them let elabConstructorDef defn@(ConstructorDef pos d (Telescope tele)) = Env.extendSourceLocation pos defn $ - Env.extendCtx (DataSig t (Telescope delta)) $ + Env.extendCtx (Data t (Telescope delta) []) $ Env.extendCtxTele delta $ do etele <- tcTypeTele tele return (ConstructorDef pos d (Telescope tele)) @@ -576,32 +568,29 @@ tcEntry (Data t (Telescope delta) cs) = Env.err [DS "Datatype definition", DD t, DS "contains duplicated constructors"] -- finally, add the datatype to the env and perform action m return $ AddCtx [Data t (Telescope delta) ecs] -tcEntry (DataSig _ _) = Env.err [DS "internal construct"] -tcEntry (RecDef _ _) = Env.err [DS "internal construct"] - -- | Make sure that we don't have the same name twice in the -- environment. (We don't rename top-level module definitions.) -duplicateTypeBindingCheck :: Sig -> TcMonad () -duplicateTypeBindingCheck sig = do +duplicateTypeBindingCheck :: Decl -> TcMonad () +duplicateTypeBindingCheck decl = do -- Look for existing type bindings ... - let n = sigName sig + let n = declName decl l <- Env.lookupTyMaybe n l' <- Env.lookupHint n -- ... we don't care which, if either are Just. case catMaybes [l, l'] of [] -> return () -- We already have a type in the environment so fail. - sig' : _ -> - let p = unPosFlaky $ sigType sig + decl' : _ -> + let p = unPosFlaky $ declType decl msg = - [ DS "Duplicate type signature", - DD sig, + [ DS "Duplicate type declaration", + DD decl, DS "Previous was", - DD sig' + DD decl' ] - in Env.extendSourceLocation p sig $ Env.err msg + in Env.extendSourceLocation p decl $ Env.err msg ----------------------------------------------------------- -- Checking that pattern matching is exhaustive @@ -695,10 +684,10 @@ relatedPats dc (pc : pats) = -- for simplicity, this function requires that all subpatterns -- are pattern variables. -checkSubPats :: DataConName -> [Decl] -> [[(Pattern, Epsilon)]] -> TcMonad () +checkSubPats :: DataConName -> [Entry] -> [[(Pattern, Epsilon)]] -> TcMonad () checkSubPats dc [] _ = return () checkSubPats dc (Def _ _ : tele) patss = checkSubPats dc tele patss -checkSubPats dc (TypeSig _ : tele) patss +checkSubPats dc (TypeDecl _ : tele) patss | (not . null) patss && not (any null patss) = do let hds = map (fst . head) patss let tls = map tail patss diff --git a/main/pi-forall.cabal b/main/pi-forall.cabal index e7a8c0c..ee29759 100644 --- a/main/pi-forall.cabal +++ b/main/pi-forall.cabal @@ -21,7 +21,7 @@ common shared-properties default-language: GHC2021 ghc-options: - -Wall -fno-warn-unused-matches -fno-warn-orphans -fno-warn-unused-top-binds -fno-warn-unused-imports -fno-warn-name-shadowing + -Wall -fno-warn-unused-matches -fno-warn-orphans -fno-warn-unused-top-binds -fno-warn-unused-imports -fno-warn-name-shadowing -Wno-unrecognised-pragmas default-extensions: DefaultSignatures DeriveAnyClass diff --git a/main/src/Environment.hs b/main/src/Environment.hs index c6f6db2..0f084b5 100644 --- a/main/src/Environment.hs +++ b/main/src/Environment.hs @@ -74,7 +74,7 @@ data Env = Env -- | Type declarations: it's not safe to -- put these in the context until a corresponding term -- has been checked. - hints :: [Sig], + hints :: [Decl], -- | what part of the file we are in (for errors/warnings) sourceLocation :: [SourceLocation] } @@ -96,37 +96,37 @@ instance Disp Env where debugDisp e = vcat [debugDisp decl | decl <- ctx e] -- | Find a name's user supplied type signature. -lookupHint :: (MonadReader Env m) => TName -> m (Maybe Sig) +lookupHint :: (MonadReader Env m) => TName -> m (Maybe Decl) lookupHint v = do hints <- asks hints - return $ listToMaybe [ sig | sig <- hints, v == sigName sig] + return $ listToMaybe [ sig | sig <- hints, v == declName sig] -- | Find a name's type in the context. lookupTyMaybe :: (MonadReader Env m) => TName -> - m (Maybe Sig) + m (Maybe Decl) lookupTyMaybe v = do ctx <- asks ctx return $ go ctx where go [] = Nothing - go (TypeSig sig : ctx) - | v == sigName sig = Just sig + go (TypeDecl sig : ctx) + | v == declName sig = Just sig | otherwise = go ctx {- SOLN EP -} - go (Demote ep : ctx) = demoteSig ep <$> go ctx + go (Demote ep : ctx) = demoteDecl ep <$> go ctx {- STUBWITH -} go (_ : ctx) = go ctx {- SOLN EP -} -demoteSig :: Epsilon -> Sig -> Sig -demoteSig ep s = s { sigEp = min ep (sigEp s) } +demoteDecl :: Epsilon -> Decl -> Decl +demoteDecl ep s = s { declEp = min ep (declEp s) } {- STUBWITH -} -- | Find the type of a name specified in the context -- throwing an error if the name doesn't exist lookupTy :: - TName -> TcMonad Sig + TName -> TcMonad Decl lookupTy v = do x <- lookupTyMaybe v @@ -175,10 +175,6 @@ lookupTCon v = do if v == v' then return (delta, Just cs) else scanGamma g - scanGamma ((DataSig v' delta) : g) = - if v == v' - then return (delta, Nothing) - else scanGamma g scanGamma (_ : g) = scanGamma g -- | Find a data constructor in the context, returns a list of @@ -198,7 +194,6 @@ lookupDConAll v = do Just c -> do more <- scanGamma g return $ (v', (delta, c)) : more - scanGamma ((DataSig v' delta) : g) = scanGamma g scanGamma (_ : g) = scanGamma g -- | Given the name of a data constructor and the type that it should @@ -256,8 +251,8 @@ extendCtxTele :: (MonadReader Env m, MonadIO m, MonadError Err m) => [Entry] -> extendCtxTele [] m = m extendCtxTele (Def x t2 : tele) m = extendCtx (Def x t2) $ extendCtxTele tele m -extendCtxTele (TypeSig sig : tele) m = - extendCtx (TypeSig sig) $ extendCtxTele tele m +extendCtxTele (TypeDecl sig : tele) m = + extendCtx (TypeDecl sig) $ extendCtxTele tele m extendCtxTele ( _ : tele) m = err [DS "Invalid telescope ", DD tele] @@ -293,7 +288,7 @@ getSourceLocation :: MonadReader Env m => m [SourceLocation] getSourceLocation = asks sourceLocation -- | Add a type hint -extendHints :: (MonadReader Env m) => Sig -> m a -> m a +extendHints :: (MonadReader Env m) => Decl -> m a -> m a extendHints h = local (\m@Env {hints = hs} -> m {hints = h : hs}) -- | An error that should be reported to the user diff --git a/main/src/Parser.hs b/main/src/Parser.hs index 840f209..6a2b6d6 100644 --- a/main/src/Parser.hs +++ b/main/src/Parser.hs @@ -104,13 +104,13 @@ Optional components in this BNF are marked with < > A -> B - Get parsed as (x:A) -> B, with an internal name for x + Get parsed as (_:A) -> B, with a wildcard name for the binder - Nondependent product types, like: A * B - Get parsed as { x:A | B }, with an internal name for x + Get parsed as { _:A | B }, with a wildcard name for the binder - You can collapse lambdas, like: @@ -126,6 +126,12 @@ Optional components in this BNF are marked with < > -} + +-- | Default name (for parsing 'A -> B' as '(_:A) -> B') +wildcardName :: TName +wildcardName = Unbound.string2Name "_" + + liftError :: (MonadError e m) => Either e a -> m a liftError (Left e) = throwError e liftError (Right a) = return a @@ -351,13 +357,13 @@ telebindings = many teleBinding annot = do (x,ty) <- try ((,) <$> varOrWildcard <*> (colon >> expr)) <|> ((,) <$> (Unbound.fresh wildcardName) <*> expr) - return (TypeSig (Sig x Rel ty):) + return (TypeDecl (Decl x Rel ty):) imp = do v <- varOrWildcard colon t <- expr - return (TypeSig (Sig v Irr t):) + return (TypeDecl (Decl v Irr t):) equal = do v <- variable @@ -376,8 +382,8 @@ telebindings = many teleBinding --- Top level declarations --- -decl,sigDef,valDef :: LParser Entry -decl = {- SOLN DATA -} try dataDef <|> {- STUBWITH -} sigDef <|> valDef +decl,declDef,valDef :: LParser Entry +decl = {- SOLN DATA -} try dataDef <|> {- STUBWITH -} declDef <|> valDef {- SOLN DATA -} -- datatype declarations. @@ -407,10 +413,10 @@ constructorDef = do "Constructor" {- STUBWITH -} -sigDef = do +declDef = do n <- try (variable >>= \v -> colon >> return v) ty <- expr - return (mkSig n ty) + return (mkDecl n ty) valDef = do n <- try (do {n <- variable; reservedOp "="; return n}) diff --git a/main/src/PrettyPrint.hs b/main/src/PrettyPrint.hs index 2cb3fa6..1e9a2e5 100644 --- a/main/src/PrettyPrint.hs +++ b/main/src/PrettyPrint.hs @@ -124,7 +124,7 @@ instance Disp Entry instance Disp [Entry] -instance Disp Sig +instance Disp Decl {- SOLN EP -} @@ -168,10 +168,10 @@ instance Display [Entry] where dd <- mapM display ds pure $ PP.vcat dd -instance Display Sig where - display sig = do - dn <- display (sigName sig) - dt <- display (sigType sig) +instance Display Decl where + display decl = do + dn <- display (declName decl) + dt <- display (declType decl) pure $ dn <+> PP.text ":" <+> dt instance Display Entry where @@ -179,7 +179,7 @@ instance Display Entry where dn <- display n dt <- display term pure $ dn <+> PP.text "=" <+> dt - display (TypeSig sig) = display sig + display (TypeDecl decl) = display decl {- SOLN EP -} display (Demote ep) = return mempty {- STUBWITH -} {- SOLN DATA -} @@ -195,12 +195,6 @@ instance Display Entry where ) 2 (PP.vcat dc) - display (DataSig t delta) = do - dt <- display t - dd <- display delta - - pure $ PP.text "data" <+> dt <+> dd <+> PP.colon - <+> PP.text "Type" {- STUBWITH -} {- SOLN DATA -} diff --git a/main/src/Syntax.hs b/main/src/Syntax.hs index 9fc205e..dad7cc8 100644 --- a/main/src/Syntax.hs +++ b/main/src/Syntax.hs @@ -158,32 +158,27 @@ newtype ModuleImport = ModuleImport ModuleName deriving (Show, Eq, Generic, Typeable) deriving anyclass (Unbound.Alpha) --- | A type declaration (or type signature) -data Sig = Sig {sigName :: TName {- SOLN EP -} , sigEp :: Epsilon {- STUBWITH -} , sigType :: Type} +-- | A type declaration (or type declnature) +data Decl = Decl {declName :: TName {- SOLN EP -} , declEp :: Epsilon {- STUBWITH -} , declType :: Type} deriving (Show, Generic, Typeable, Unbound.Alpha, Unbound.Subst Term) -- | Declare the type of a term -mkSig :: TName -> Type -> Entry -mkSig n ty = TypeSig (Sig n {- SOLN EP -} Rel {- STUBWITH -} ty) +mkDecl :: TName -> Type -> Entry +mkDecl n ty = TypeDecl (Decl n {- SOLN EP -} Rel {- STUBWITH -} ty) -- | Entries are the components of modules data Entry - = -- | Declaration for the type of a term - TypeSig Sig - | -- | The definition of a particular name, must + = -- | Declaration for the type of a term 'x : A' + TypeDecl Decl + | -- | The definition of a particular name, must 'x = a' -- already have a type declaration in scope Def TName Term {- SOLN EP -} -- | Adjust the context for relevance checking | Demote Epsilon {- STUBWITH -} {- SOLN DATA -} - | -- | Declaration for a datatype including all of - -- its data constructors + | -- | Datatype definition (must be at the module level) Data TyConName Telescope [ConstructorDef] - | -- | An abstract view of a datatype. Does - -- not include any information about its data - -- constructors - DataSig TyConName Telescope {- STUBWITH -} deriving (Show, Generic, Typeable) deriving anyclass (Unbound.Alpha, Unbound.Subst Term) @@ -279,12 +274,12 @@ preludeDataDecls = unitConstructorDef = ConstructorDef internalPos litUnitName (Telescope []) -- Sigma-type - sigmaTele = Telescope [TypeSig sigA, TypeSig sigB] - prodConstructorDef = ConstructorDef internalPos prodName (Telescope [TypeSig sigX, TypeSig sigY]) - sigA = Sig aName Rel TyType - sigB = Sig bName Rel (TyPi Rel (Var aName) (Unbound.bind xName TyType)) - sigX = Sig xName Rel (Var aName) - sigY = Sig yName Rel (App (Var bName) (Arg Rel (Var xName))) + sigmaTele = Telescope [TypeDecl declA, TypeDecl declB] + prodConstructorDef = ConstructorDef internalPos prodName (Telescope [TypeDecl declX, TypeDecl declY]) + declA = Decl aName Rel TyType + declB = Decl bName Rel (TyPi Rel (Var aName) (Unbound.bind xName TyType)) + declX = Decl xName Rel (Var aName) + declY = Decl yName Rel (App (Var bName) (Arg Rel (Var xName))) aName = Unbound.string2Name "a" bName = Unbound.string2Name "b" @@ -297,9 +292,12 @@ preludeDataDecls = -- * Auxiliary functions on syntax ----------------------------------------- --- | Default name (for parsing 'A -> B' as '(_:A) -> B') -wildcardName :: TName -wildcardName = Unbound.string2Name "_" + +-- | Remove source positions and type annotations from the top level of a term +strip :: Term -> Term +strip (Pos _ tm) = strip tm +strip (Ann tm _) = strip tm +strip tm = tm -- | Partial inverse of Pos unPos :: Term -> Maybe SourcePos @@ -311,6 +309,7 @@ unPosFlaky :: Term -> SourcePos unPosFlaky t = fromMaybe (newPos "unknown location" 0 0) (unPos t) + ----------------------------------------- -- * Unbound library ----------------------------------------- @@ -354,24 +353,22 @@ unbind = Unbound.unbind -- unbind :: (Alpha p, Alpha t, Fresh m) => Bind p t -> m (p, t) -- For Terms, we'd like Alpha equivalence to ignore --- source positions and type annotations. --- We can add these special cases to the definition of `aeq'` --- and then defer all other cases to the generic version of --- the function (Unbound.gaeq). +-- source positions and type annotations. So we make sure to +-- remove them before calling the generic operation. instance Unbound.Alpha Term where aeq' :: Unbound.AlphaCtx -> Term -> Term -> Bool - aeq' ctx (Ann a _) b = Unbound.aeq' ctx a b - aeq' ctx a (Ann b _) = Unbound.aeq' ctx a b - aeq' ctx (Pos _ a) b = Unbound.aeq' ctx a b - aeq' ctx a (Pos _ b) = Unbound.aeq' ctx a b - aeq' ctx a b = (Unbound.gaeq ctx `on` from) a b + aeq' ctx a b = (Unbound.gaeq ctx `on` from) (strip a) (strip b) + -- For example, all occurrences of annotations and source positions -- are ignored by this definition. --- '(Bool : Type)' is alpha-equivalent to 'Type' --- >>> aeq (Pos internalPos (Ann TyBool Type)) TyBool +-- '(Bool : Type)' is alpha-equivalent to 'Bool' +-- >>> aeq (Ann TyBool TyType) TyBool + +-- '(Bool, Bool:Type)' is alpha-equivalent to (Bool, Bool) +-- >>> aeq (Prod TyBool (Ann TyBool TyType)) (Prod TyBool TyBool) -- At the same time, the generic operation equates terms that differ only @@ -472,4 +469,4 @@ instance Unbound.Alpha ConstructorNames where freshen' _ x = return (x, mempty) lfreshen' _ x cont = cont x mempty acompare' _ _ _ = EQ -{- STUBWITH -} \ No newline at end of file +{- STUBWITH -} diff --git a/main/src/TypeCheck.hs b/main/src/TypeCheck.hs index a943124..a109274 100644 --- a/main/src/TypeCheck.hs +++ b/main/src/TypeCheck.hs @@ -1,7 +1,6 @@ {- pi-forall -} -- | The main routines for type-checking -{-# OPTIONS_GHC -Wno-unrecognised-pragmas #-} {-# HLINT ignore "Use forM_" #-} module TypeCheck (tcModules, inferType, checkType) where @@ -27,327 +26,324 @@ import Unbound.Generics.LocallyNameless.Internal.Fold qualified as Unbound import Unbound.Generics.LocallyNameless.Unsafe (unsafeUnbind) {- STUBWITH -} --- | Infer/synthesize the type of a term -inferType :: Term -> TcMonad Type -inferType t = tcTerm t Nothing --- | Check that the given term has the expected type -checkType :: Term -> Type -> TcMonad () -checkType tm (Pos _ ty) = checkType tm ty -- ignore source positions/annotations -checkType tm (Ann ty _) = checkType tm ty -checkType tm ty = {- SOLN EQUAL -} do - nf <- Equal.whnf ty - void $ tcTerm tm (Just nf) -{- STUBWITH void $ tcTerm tm (Just ty) -} - - --- | Make sure that the term is a "type" (i.e. that it has type 'Type') -tcType :: Term -> TcMonad () -tcType tm = void $ {- SOLN EP -} Env.withStage Irr $ {- STUBWITH -}checkType tm TyType --------------------------------------------------------------------- --- | Combined type checking/inference function --- The second argument is 'Just expectedType' in checking mode and 'Nothing' in inference mode --- In either case, this function returns the type of the term -tcTerm :: Term -> Maybe Type -> TcMonad Type --- i-var -tcTerm t@(Var x) Nothing = do - sig <- Env.lookupTy x {- SOLN EP -} - -- make sure the variable is accessible - Env.checkStage (sigEp sig) {- STUBWITH -} - return (sigType sig) --- i-type -tcTerm TyType Nothing = return TyType --- i-pi -tcTerm (TyPi {- SOLN EP -} ep {- STUBWITH -}tyA bnd) Nothing = do - (x, tyB) <- Unbound.unbind bnd - tcType tyA - Env.extendCtx {- SOLN EP -} (TypeSig (Sig x ep tyA)){- STUBWITH (mkSig x tyA) -} (tcType tyB) - return TyType --- c-lam: check the type of a function -tcTerm (Lam {- SOLN EP -} ep1 {- STUBWITH -} bnd) (Just (TyPi {- SOLN EP -} ep2 {- STUBWITH -}tyA bnd2)) = do - -- unbind the variables in the lambda expression and pi type - (x, body,_,tyB) <- Unbound.unbind2Plus bnd bnd2 -{- SOLN EP -} -- epsilons should match up - unless (ep1 == ep2) $ Env.err [DS "In function definition, expected", DD ep2, DS "parameter", DD x, - DS "but found", DD ep1, DS "instead."] {- STUBWITH -} - -- check the type of the body of the lambda expression - Env.extendCtx {- SOLN EP -} (TypeSig (Sig x ep1 tyA)){- STUBWITH (mkSig x tyA) -} (checkType body tyB) - return (TyPi {- SOLN EP -} ep1{- STUBWITH -} tyA bnd2) -tcTerm (Lam {- SOLN EP -} _ {- STUBWITH -}_) (Just nf) = - Env.err [DS "Lambda expression should have a function type, not", DD nf] --- i-app -tcTerm (App t1 t2) Nothing = do - ty1 <- inferType t1 +-- | Infer/synthesize the type of a term +inferType :: Term -> TcMonad Type +inferType t = case t of + -- i-var + (Var x) -> do + decl <- Env.lookupTy x {- SOLN EP -} + -- make sure the variable is accessible + Env.checkStage (declEp decl) {- STUBWITH -} + return (declType decl) + + -- i-type + TyType -> return TyType + + -- i-pi + (TyPi {- SOLN EP -} ep {- STUBWITH -}tyA bnd) -> do + (x, tyB) <- Unbound.unbind bnd + tcType tyA + Env.extendCtx {- SOLN EP -} (TypeDecl (Decl x ep tyA)){- STUBWITH (mkDecl x tyA) -} (tcType tyB) + return TyType + + -- i-app + (App t1 t2) -> do + ty1 <- inferType t1 {- SOLN EQUAL -} - let ensurePi = Equal.ensurePi - {- STUBWITH - - let ensurePi :: Type -> TcMonad (Type, Unbound.Bind TName Type) - ensurePi (Ann a _) = ensurePi a - ensurePi (Pos _ a) = ensurePi a - ensurePi (TyPi tyA bnd) = return (tyA,bnd) - ensurePi ty = Env.err [DS "Expected a function type but found ", DD ty] -} + let ensurePi = Equal.ensurePi + {- STUBWITH + + let ensurePi :: Type -> TcMonad (Type, Unbound.Bind TName Type) + ensurePi (Pos _ ty) = ensurePi ty + ensurePi (Ann tm _) = ensurePi tm + ensurePi (TyPi tyA bnd) = return (tyA,bnd) + ensurePi ty = Env.err [DS "Expected a function type but found ", DD ty] -} {- SOLN EP -} - (ep1, tyA, bnd) <- ensurePi ty1 - unless (ep1 == argEp t2) $ Env.err - [DS "In application, expected", DD ep1, DS "argument but found", - DD t2, DS "instead." ] - -- if the argument is Irrelevant, resurrect the context - (if ep1 == Irr then Env.extendCtx (Demote Rel) else id) $ - checkType (unArg t2) tyA - return (Unbound.instantiate bnd [unArg t2]) - {- STUBWITH - - (tyA,bnd) <- ensurePi ty1 - checkType t2 tyA - return (Unbound.instantiate bnd [t2]) -} - --- i-ann -tcTerm (Ann tm ty) Nothing = do - tcType ty - checkType tm ty - return ty + (ep1, tyA, bnd) <- ensurePi ty1 + unless (ep1 == argEp t2) $ Env.err + [DS "In application, expected", DD ep1, DS "argument but found", + DD t2, DS "instead." ] + -- if the argument is Irrelevant, resurrect the context + (if ep1 == Irr then Env.extendCtx (Demote Rel) else id) $ + checkType (unArg t2) tyA + return (Unbound.instantiate bnd [unArg t2]) + {- STUBWITH + + (tyA,bnd) <- ensurePi ty1 + checkType t2 tyA + return (Unbound.instantiate bnd [t2]) -} + + -- i-ann + (Ann tm ty) -> do + tcType ty + checkType tm ty + return ty --- practicalities --- remember the current position in the type checking monad -tcTerm (Pos p tm) mTy = - Env.extendSourceLocation p tm $ tcTerm tm mTy --- ignore term, just return type annotation -tcTerm TrustMe (Just ty) = return ty + -- Practicalities + -- remember the current position in the type checking monad + (Pos p tm) -> + Env.extendSourceLocation p tm $ inferType tm --- i-unit -tcTerm TyUnit Nothing = return TyType -tcTerm LitUnit Nothing = return TyUnit - --- i-bool -tcTerm TyBool Nothing = {- SOLN HW -} return TyType -{- STUBWITH Env.err [DS "unimplemented"] -} - --- i-true/false -tcTerm (LitBool b) Nothing = {- SOLN HW -} do - return TyBool -{- STUBWITH Env.err [DS "unimplemented"] -} - --- c-if -tcTerm t@(If t1 t2 t3) mty = {- SOLN HW -} do - case mty of - Just ty -> do - checkType t1 TyBool - dtrue <- Equal.unify [] t1 (LitBool True) - dfalse <- Equal.unify [] t1 (LitBool False) - Env.extendCtxs dtrue $ checkType t2 ty - Env.extendCtxs dfalse $ checkType t3 ty - return ty - Nothing -> do + -- Extensions to the core language + -- i-unit + TyUnit -> return TyType + LitUnit -> return TyUnit + + -- i-bool + TyBool -> {- SOLN HW -} return TyType {- STUBWITH Env.err [DS "unimplemented"] -} + + -- i-true/false + (LitBool b) -> {- SOLN HW -} return TyBool {- STUBWITH Env.err [DS "unimplemented"] -} + + -- i-if + (If t1 t2 t3) -> {- SOLN HW -} do checkType t1 TyBool ty <- inferType t2 checkType t3 ty - return ty -{- STUBWITH Env.err [DS "unimplemented"] -} - -tcTerm (Let rhs bnd) mty = {- SOLN HW -} do - (x, body) <- Unbound.unbind bnd - aty <- inferType rhs - ty <- Env.extendCtxs [mkSig x aty, Def x rhs] $ - tcTerm body mty - case mty of - Just _ -> return ty - Nothing -> return $ Unbound.subst x rhs ty -{- STUBWITH Env.err [DS "unimplemented"] -} + return ty {- STUBWITH Env.err [DS "unimplemented"] -} +{- SOLN EQUAL -} + -- i-eq + (TyEq a b) -> do + aTy <- inferType a + checkType b aTy + return TyType {- STUBWITH -} + + -- i-sigma + (TySigma tyA bnd) -> {- SOLN EQUAL -} do + (x, tyB) <- Unbound.unbind bnd + tcType tyA + Env.extendCtx (mkDecl x tyA) $ tcType tyB + return TyType {- STUBWITH Env.err [DS "unimplemented"] -} + {- SOLN DATA -} --- TyType constructor application -tcTerm (TyCon c params) Nothing = do - (Telescope delta, _) <- Env.lookupTCon c - unless (length params == length delta) $ - Env.err - [ DS "Datatype constructor", - DD c, - DS $ - "should have " ++ show (length delta) - ++ "parameters, but was given", - DD (length params) - ] - tcArgTele params delta - return TyType - --- Data constructor application --- we don't know the expected type, so see if there --- is only one datacon of that name that takes no --- parameters -tcTerm t@(DataCon c args) Nothing = do - matches <- Env.lookupDConAll c - case matches of - [(tname, (Telescope [], ConstructorDef _ _ (Telescope deltai)))] -> do - let numArgs = length deltai - unless (length args == numArgs) $ - Env.err - [ DS "Constructor", - DS c, - DS "should have", - DD numArgs, - DS "data arguments, but was given", - DD (length args), - DS "arguments." - ] - tcArgTele args deltai - return $ TyCon tname [] - - [_] -> + -- Type constructor application + (TyCon c params) -> do + (Telescope delta, _) <- Env.lookupTCon c + unless (length params == length delta) $ Env.err - [ DS "Cannot infer the parameters to data constructors.", - DS "Add an annotation." + [ DS "Datatype constructor", + DD c, + DS $ + "should have " ++ show (length delta) + ++ "parameters, but was given", + DD (length params) ] - _ -> Env.err [DS "Ambiguous data constructor", DS c] - --- we know the expected type of the data constructor --- so look up its type in the context -tcTerm t@(DataCon c args) (Just ty) = do - case ty of - (TyCon tname params) -> do - (Telescope delta, Telescope deltai) <- Env.lookupDCon c tname - let isTypeSig :: Entry -> Bool - isTypeSig (TypeSig _) = True - isTypeSig _ = False - let numArgs = length (filter isTypeSig deltai) - unless (length args == numArgs) $ + tcArgTele params delta + return TyType + + -- Data constructor application + -- we don't know the expected type, so see if there + -- is only one datacon of that name that takes no + -- parameters + (DataCon c args) -> do + matches <- Env.lookupDConAll c + case matches of + [(tname, (Telescope [], ConstructorDef _ _ (Telescope deltai)))] -> do + let numArgs = length deltai + unless (length args == numArgs) $ + Env.err + [ DS "Constructor", + DS c, + DS "should have", + DD numArgs, + DS "data arguments, but was given", + DD (length args), + DS "arguments." + ] + tcArgTele args deltai + return $ TyCon tname [] + [_] -> Env.err - [ DS "Constructor", - DS c, - DS "should have", - DD numArgs, - DS "data arguments, but was given", - DD (length args), - DS "arguments." + [ DS "Cannot infer the parameters to data constructors.", + DS "Add an annotation." ] - newTele <- substTele delta params deltai - tcArgTele args newTele - return ty - _ -> - Env.err [DS "Unexpected type", DD ty, DS "for data constructor", DD t] - --- Must have an annotation for Case -tcTerm t@(Case scrut alts) (Just ty) = do - sty <- inferType scrut - scrut' <- Equal.whnf scrut - (c, args) <- Equal.ensureTCon sty - let checkAlt (Match bnd) = do - (pat, body) <- Unbound.unbind bnd - -- add variables from pattern to context - -- could fail if branch is in-accessible - decls <- declarePat pat Rel (TyCon c args) - -- add defs to the contents from scrut = pat - -- could fail if branch is in-accessible - decls' <- Equal.unify [] scrut' (pat2Term pat) - Env.extendCtxs (decls ++ decls') $ checkType body ty - {- STUBWITH -} + _ -> Env.err [DS "Ambiguous data constructor", DS c] {- STUBWITH -} + + -- cannot synthesize the type of the term + tm -> + Env.err [DS "Must have a type for", DD tm] + + +------------------------------------------------------------------------- + +-- | Make sure that the term is a "type" (i.e. that it has type 'Type') +tcType :: Term -> TcMonad () +tcType tm = {- SOLN EP -} Env.withStage Irr $ {- STUBWITH -} checkType tm TyType + +------------------------------------------------------------------------- +-- | Check that the given term has the expected type +checkType :: Term -> Type -> TcMonad () +checkType tm ty' = do +{- SOLN EQUAL -} + ty <- Equal.whnf ty' {- STUBWITH let ty = strip ty' -- ignore source positions/annotations -} + case tm of + -- c-lam: check the type of a function + (Lam {- SOLN EP -} ep1 {- STUBWITH -} bnd) -> case ty of + (TyPi {- SOLN EP -} ep2 {- STUBWITH -}tyA bnd2) -> do + -- unbind the variables in the lambda expression and pi type + (x, body,_,tyB) <- Unbound.unbind2Plus bnd bnd2 +{- SOLN EP -} -- epsilons should match up + unless (ep1 == ep2) $ Env.err [DS "In function definition, expected", DD ep2, DS "parameter", DD x, + DS "but found", DD ep1, DS "instead."] {- STUBWITH -} + -- check the type of the body of the lambda expression + Env.extendCtx {- SOLN EP -} (TypeDecl (Decl x ep1 tyA)){- STUBWITH (mkDecl x tyA) -} (checkType body tyB) + _ -> Env.err [DS "Lambda expression should have a function type, not", DD ty] + + -- Practicalities + (Pos p tm) -> + Env.extendSourceLocation p tm $ checkType tm ty + + TrustMe -> return () + + PrintMe -> do + gamma <- Env.getLocalCtx + Env.warn [DS "Unmet obligation.\nContext:", DD gamma, + DS "\nGoal:", DD ty] + + -- Extensions to the core language + -- c-if + (If t1 t2 t3) -> {- SOLN HW -} do + checkType t1 TyBool + dtrue <- Equal.unify [] t1 (LitBool True) + dfalse <- Equal.unify [] t1 (LitBool False) + Env.extendCtxs dtrue $ checkType t2 ty + Env.extendCtxs dfalse $ checkType t3 ty {- STUBWITH Env.err [DS "unimplemented"] -} + + -- c-let + (Let rhs bnd) -> {- SOLN HW -} do + (x, body) <- Unbound.unbind bnd + aty <- inferType rhs + Env.extendCtxs [mkDecl x aty, Def x rhs] $ + checkType body ty {- STUBWITH Env.err [DS "unimplemented"] -} {- SOLN DATA -} - return () - let pats = map (\(Match bnd) -> fst (unsafeUnbind bnd)) alts - mapM_ checkAlt alts - exhaustivityCheck scrut' sty pats - return ty -{- STUBWITH -} -{- SOLN EQUAL -} -tcTerm (TyEq a b) Nothing = do - aTy <- inferType a - checkType b aTy - return TyType -tcTerm Refl (Just ty@(TyEq a b)) = do - Equal.equate a b - return ty -tcTerm Refl (Just ty) = - Env.err [DS "Refl annotated with", DD ty] -tcTerm t@(Subst a b) (Just ty) = do - -- infer the type of the proof 'b' - tp <- inferType b - -- make sure that it is an equality between m and n - (m, n) <- Equal.ensureTyEq tp - -- if either side is a variable, add a definition to the context - edecl <- Equal.unify [] m n - -- if proof is a variable, add a definition to the context - pdecl <- Equal.unify [] b Refl - _ <- Env.extendCtxs (edecl ++ pdecl) $ checkType a ty - return ty -tcTerm t@(Contra p) (Just ty) = do - ty' <- inferType p - (a, b) <- Equal.ensureTyEq ty' - a' <- Equal.whnf a - b' <- Equal.whnf b - case (a', b') of + -- c-data + -- we know the expected type of the data constructor + -- so look up its type in the context + (DataCon c args) -> do + case ty of + (TyCon tname params) -> do + (Telescope delta, Telescope deltai) <- Env.lookupDCon c tname + let isTypeDecl :: Entry -> Bool + isTypeDecl (TypeDecl _) = True + isTypeDecl _ = False + let numArgs = length (filter isTypeDecl deltai) + unless (length args == numArgs) $ + Env.err + [ DS "Constructor", + DS c, + DS "should have", + DD numArgs, + DS "data arguments, but was given", + DD (length args), + DS "arguments." + ] + newTele <- substTele delta params deltai + tcArgTele args newTele + _ -> + Env.err [DS "Unexpected type", DD ty, DS "for data constructor", DD tm] + + (Case scrut alts) -> do + sty <- inferType scrut + scrut' <- Equal.whnf scrut + (c, args) <- Equal.ensureTCon sty + let checkAlt (Match bnd) = do + (pat, body) <- Unbound.unbind bnd + -- add variables from pattern to context + -- could fail if branch is in-accessible + decls <- declarePat pat Rel (TyCon c args) + -- add defs to the contents from scrut = pat + -- could fail if branch is in-accessible + decls' <- Equal.unify [] scrut' (pat2Term pat) + Env.extendCtxs (decls ++ decls') $ checkType body ty + + return () + let pats = map (\(Match bnd) -> fst (unsafeUnbind bnd)) alts + mapM_ checkAlt alts + exhaustivityCheck scrut' sty pats {- STUBWITH -} +{- SOLN EQUAL -} + -- c-refl + Refl -> case ty of + (TyEq a b) -> Equal.equate a b + _ -> Env.err [DS "Refl annotated with", DD ty] + -- c-subst + (Subst a b) -> do + -- infer the type of the proof 'b' + tp <- inferType b + -- make sure that it is an equality between m and n + (m, n) <- Equal.ensureTyEq tp + -- if either side is a variable, add a definition to the context + edecl <- Equal.unify [] m n + -- if proof is a variable, add a definition to the context + pdecl <- Equal.unify [] b Refl + Env.extendCtxs (edecl ++ pdecl) $ checkType a ty + -- c-contra + (Contra p) -> do + ty' <- inferType p + (a, b) <- Equal.ensureTyEq ty' + a' <- Equal.whnf a + b' <- Equal.whnf b + case (a', b') of + {- STUBWITH -} {- SOLN DATA -} - (DataCon da _, DataCon db _) - | da /= db -> - return ty - {- STUBWITH -} + (DataCon da _, DataCon db _) + | da /= db -> + return () + {- STUBWITH -} {- SOLN EQUAL -} - (LitBool b1, LitBool b2) - | b1 /= b2 -> - return ty - (_, _) -> - Env.err - [ DS "I can't tell that", - DD a, - DS "and", - DD b, - DS "are contradictory" - ] -{- STUBWITH -} - -tcTerm t@(TySigma tyA bnd) Nothing = {- SOLN EQUAL -} do - (x, tyB) <- Unbound.unbind bnd - tcType tyA - Env.extendCtx (mkSig x tyA) $ tcType tyB - return TyType -{- STUBWITH Env.err [DS "unimplemented"] -} - -tcTerm t@(Prod a b) (Just ty) = {- SOLN EQUAL -} do - case ty of - (TySigma tyA bnd) -> do - (x, tyB) <- Unbound.unbind bnd - checkType a tyA - Env.extendCtxs [mkSig x tyA, Def x a] $ checkType b tyB - return (TySigma tyA (Unbound.bind x tyB)) - _ -> - Env.err - [ DS "Products must have Sigma Type", - DD ty, - DS "found instead" - ] -{- STUBWITH Env.err [DS "unimplemented"] -} - -tcTerm t@(LetPair p bnd) (Just ty) = {- SOLN EQUAL -} do - ((x, y), body) <- Unbound.unbind bnd - pty <- inferType p - pty' <- Equal.whnf pty - case pty' of - TySigma tyA bnd' -> do - let tyB = Unbound.instantiate bnd' [Var x] - decl <- Equal.unify [] p (Prod (Var x) (Var y)) - Env.extendCtxs ([mkSig x tyA, mkSig y tyB] ++ decl) $ - checkType body ty - return ty - _ -> Env.err [DS "Scrutinee of LetPair must have Sigma type"] -{- STUBWITH Env.err [DS "unimplemented"] -} - -tcTerm PrintMe (Just ty) = do - gamma <- Env.getLocalCtx - Env.warn [DS "Unmet obligation.\nContext:", DD gamma, - DS "\nGoal:", DD ty] - return ty - --- c-infer -tcTerm tm (Just ty) = do - ty' <- inferType tm + (LitBool b1, LitBool b2) + | b1 /= b2 -> + return () + (_, _) -> + Env.err + [ DS "I can't tell that", + DD a, + DS "and", + DD b, + DS "are contradictory" + ] + {- STUBWITH -} + -- c-prod + (Prod a b) -> {- SOLN EQUAL -} do + case ty of + (TySigma tyA bnd) -> do + (x, tyB) <- Unbound.unbind bnd + checkType a tyA + Env.extendCtxs [mkDecl x tyA, Def x a] $ checkType b tyB + _ -> + Env.err + [ DS "Products must have Sigma Type", + DD ty, + DS "found instead" + ] + {- STUBWITH Env.err [DS "unimplemented"] -} + + -- c-letpair + (LetPair p bnd) -> {- SOLN EQUAL -} do + ((x, y), body) <- Unbound.unbind bnd + pty <- inferType p + pty' <- Equal.whnf pty + case pty' of + TySigma tyA bnd' -> do + let tyB = Unbound.instantiate bnd' [Var x] + decl <- Equal.unify [] p (Prod (Var x) (Var y)) + Env.extendCtxs ([mkDecl x tyA, mkDecl y tyB] ++ decl) $ + checkType body ty + _ -> Env.err [DS "Scrutinee of LetPair must have Sigma type"] + {- STUBWITH Env.err [DS "unimplemented"] -} + + + -- c-infer + tm -> do + ty' <- inferType tm {- SOLN EQUAL -} - Equal.equate ty' ty -{- STUBWITH unless (Unbound.aeq ty' ty) $ Env.err [DS "Types don't match", DD ty, DS "and", DD ty'] -} - return ty' + Equal.equate ty' ty + {- STUBWITH unless (Unbound.aeq ty' ty) $ Env.err [DS "Types don't match", DD ty, DS "and", DD ty'] -} -tcTerm tm Nothing = - Env.err [DS "Must have a type annotation to check", DD tm] {- SOLN HW -} --------------------------------------------------------------------- @@ -376,7 +372,7 @@ tcArgTele args (Def x ty : tele) = do -- ensure that the equality is provable at this point Equal.equate (Var x) ty tcArgTele args tele -tcArgTele (Arg ep1 tm : terms) (TypeSig (Sig x ep2 ty) : tele) +tcArgTele (Arg ep1 tm : terms) (TypeDecl (Decl x ep2 ty) : tele) | ep1 == ep2 = do Env.withStage ep1 $ checkType tm ty tele' <- doSubst [(x, tm)] tele @@ -403,7 +399,7 @@ substTele :: [Entry] -> [Arg] -> [Entry] -> TcMonad [Entry] substTele tele args = doSubst (mkSubst tele (map unArg args)) where mkSubst [] [] = [] - mkSubst (TypeSig (Sig x Rel _) : tele') (tm : tms) = + mkSubst (TypeDecl (Decl x Rel _) : tele') (tm : tms) = (x, tm) : mkSubst tele' tms mkSubst _ _ = error "Internal error: substTele given illegal arguments" @@ -419,11 +415,11 @@ doSubst ss (Def x ty : tele') = do decls1 <- Equal.unify [] tx' ty' decls2 <- Env.extendCtxs decls1 (doSubst ss tele') return $ decls1 ++ decls2 -doSubst ss (TypeSig sig : tele') = do - tynf <- Equal.whnf (Unbound.substs ss (sigType sig)) - let sig' = sig{sigType = tynf} +doSubst ss (TypeDecl decl : tele') = do + tynf <- Equal.whnf (Unbound.substs ss (declType decl)) + let decl' = decl{declType = tynf} tele'' <- doSubst ss tele' - return $ TypeSig sig' : tele'' + return $ TypeDecl decl' : tele'' doSubst _ tele = Env.err [DS "Invalid telescope", DD tele] @@ -431,7 +427,7 @@ doSubst _ tele = -- | Create a binding for each of the variables in the pattern declarePat :: Pattern -> Epsilon -> Type -> TcMonad [Entry] -declarePat (PatVar x) ep ty = return [TypeSig (Sig x ep ty)] +declarePat (PatVar x) ep ty = return [TypeDecl (Decl x ep ty)] declarePat (PatCon dc pats) Rel ty = do (tc,params) <- Equal.ensureTCon ty (Telescope delta, Telescope deltai) <- Env.lookupDCon dc tc @@ -447,7 +443,7 @@ declarePats dc pats (Def x ty : tele) = do let ds1 = [Def x ty] ds2 <- Env.extendCtxs ds1 $ declarePats dc pats tele return (ds1 ++ ds2) -declarePats dc ((pat, _) : pats) (TypeSig (Sig x ep ty) : tele) = do +declarePats dc ((pat, _) : pats) (TypeDecl (Decl x ep ty) : tele) = do ds1 <- declarePat pat ep ty let tm = pat2Term pat tele' <- doSubst [(x,tm)] tele @@ -478,9 +474,9 @@ tcTypeTele (Def x tm : tl) = do Env.withStage Irr $ checkType tm ty1 let decls = [Def x tm] Env.extendCtxs decls $ tcTypeTele tl -tcTypeTele (TypeSig sig : tl) = do - tcType (sigType sig) - Env.extendCtx (TypeSig sig) $ tcTypeTele tl +tcTypeTele (TypeDecl decl : tl) = do + tcType (declType decl) + Env.extendCtx (TypeDecl decl) $ tcTypeTele tl tcTypeTele tele = Env.err [DS "Invalid telescope: ", DD tele] @@ -534,7 +530,7 @@ tcModule defs m' = do -- | The Env-delta returned when type-checking a top-level Entry. data HintOrCtx - = AddHint Sig + = AddHint Decl | AddCtx [Entry] -- | Check each sort of declaration in a module @@ -548,20 +544,20 @@ tcEntry (Def n term) = do case lkup of Nothing -> do ty <- inferType term - return $ AddCtx [TypeSig (Sig n {- SOLN EP -} Rel{- STUBWITH -} ty), Def n term] - Just sig -> + return $ AddCtx [TypeDecl (Decl n {- SOLN EP -} Rel{- STUBWITH -} ty), Def n term] + Just decl -> let handler (Env.Err ps msg) = throwError $ Env.Err ps (msg $$ msg') msg' = disp [ DS "When checking the term", DD term, - DS "against the signature", - DD sig + DS "against the type", + DD decl ] in do - Env.extendCtx (TypeSig sig) $ checkType term (sigType sig) `catchError` handler - return $ AddCtx [TypeSig sig, Def n term] + Env.extendCtx (TypeDecl decl) $ checkType term (declType decl) `catchError` handler + return $ AddCtx [TypeDecl decl, Def n term] die term' = Env.extendSourceLocation (unPosFlaky term) term $ Env.err @@ -570,10 +566,10 @@ tcEntry (Def n term) = do DS "Previous definition was", DD term' ] -tcEntry (TypeSig sig) = do - duplicateTypeBindingCheck sig - tcType (sigType sig) - return $ AddHint sig +tcEntry (TypeDecl decl) = do + duplicateTypeBindingCheck decl + tcType (declType decl) + return $ AddHint decl {- SOLN EP -} tcEntry (Demote ep) = return (AddCtx [Demote ep]) {- STUBWITH -} @@ -588,7 +584,7 @@ tcEntry (Data t (Telescope delta) cs) = --- for each data constructor is wellfomed, and elaborate them let elabConstructorDef defn@(ConstructorDef pos d (Telescope tele)) = Env.extendSourceLocation pos defn $ - Env.extendCtx (DataSig t (Telescope delta)) $ + Env.extendCtx (Data t (Telescope delta) []) $ Env.extendCtxTele delta $ do etele <- tcTypeTele tele return (ConstructorDef pos d (Telescope tele)) @@ -599,32 +595,29 @@ tcEntry (Data t (Telescope delta) cs) = Env.err [DS "Datatype definition", DD t, DS "contains duplicated constructors"] -- finally, add the datatype to the env and perform action m return $ AddCtx [Data t (Telescope delta) ecs] -tcEntry (DataSig _ _) = Env.err [DS "internal construct"] - - -{- STUBWITH tcEntry _ = Env.err "unimplemented" -} +{- STUBWITH -} -- | Make sure that we don't have the same name twice in the -- environment. (We don't rename top-level module definitions.) -duplicateTypeBindingCheck :: Sig -> TcMonad () -duplicateTypeBindingCheck sig = do +duplicateTypeBindingCheck :: Decl -> TcMonad () +duplicateTypeBindingCheck decl = do -- Look for existing type bindings ... - let n = sigName sig + let n = declName decl l <- Env.lookupTyMaybe n l' <- Env.lookupHint n -- ... we don't care which, if either are Just. case catMaybes [l, l'] of [] -> return () -- We already have a type in the environment so fail. - sig' : _ -> - let p = unPosFlaky $ sigType sig + decl' : _ -> + let p = unPosFlaky $ declType decl msg = - [ DS "Duplicate type signature", - DD sig, + [ DS "Duplicate type declaration", + DD decl, DS "Previous was", - DD sig' + DD decl' ] - in Env.extendSourceLocation p sig $ Env.err msg + in Env.extendSourceLocation p decl $ Env.err msg {- SOLN DATA -} ----------------------------------------------------------- @@ -722,7 +715,7 @@ relatedPats dc (pc : pats) = checkSubPats :: DataConName -> [Entry] -> [[(Pattern, Epsilon)]] -> TcMonad () checkSubPats dc [] _ = return () checkSubPats dc (Def _ _ : tele) patss = checkSubPats dc tele patss -checkSubPats dc (TypeSig _ : tele) patss +checkSubPats dc (TypeDecl _ : tele) patss | (not . null) patss && not (any null patss) = do let hds = map (fst . head) patss let tls = map tail patss diff --git a/version1/pi-forall.cabal b/version1/pi-forall.cabal index e7a8c0c..ee29759 100644 --- a/version1/pi-forall.cabal +++ b/version1/pi-forall.cabal @@ -21,7 +21,7 @@ common shared-properties default-language: GHC2021 ghc-options: - -Wall -fno-warn-unused-matches -fno-warn-orphans -fno-warn-unused-top-binds -fno-warn-unused-imports -fno-warn-name-shadowing + -Wall -fno-warn-unused-matches -fno-warn-orphans -fno-warn-unused-top-binds -fno-warn-unused-imports -fno-warn-name-shadowing -Wno-unrecognised-pragmas default-extensions: DefaultSignatures DeriveAnyClass diff --git a/version1/pi/Lec1.pi b/version1/pi/Lec1.pi index 9e43048..eb6a040 100644 --- a/version1/pi/Lec1.pi +++ b/version1/pi/Lec1.pi @@ -2,13 +2,10 @@ module Lec1 where -ida : Type -> Type -ida = \y . y - -id : (x:Type) -> ((y : x) -> x) +id : (x:Type) -> x -> x id = \x y . y -idid : ((x:Type) -> x -> x) +idid : ((x:Type) -> (y : x) -> x) idid = id ((x:Type) -> (y : x) -> x) id compose : (A : Type) -> (B : Type) -> (C:Type) -> diff --git a/version1/src/Environment.hs b/version1/src/Environment.hs index 6ef3da0..fcfa194 100644 --- a/version1/src/Environment.hs +++ b/version1/src/Environment.hs @@ -9,7 +9,6 @@ module Environment lookupTy, lookupTyMaybe, lookupDef, - lookupRecDef, lookupHint, getCtx, getLocalCtx, @@ -67,15 +66,15 @@ data SourceLocation where -- | Environment manipulation and accessing functions -- The context 'gamma' is a list data Env = Env - { -- | elaborated term and datatype declarations. - ctx :: [Decl], + { -- | elaborated term and datatype declarations + ctx :: [Entry], -- | how long the tail of "global" variables in the context is -- (used to supress printing those in error messages) globals :: Int, - -- | Type declarations (signatures): it's not safe to + -- | Type declarations: it's not safe to -- put these in the context until a corresponding term -- has been checked. - hints :: [Sig], + hints :: [Decl], -- | what part of the file we are in (for errors/warnings) sourceLocation :: [SourceLocation] } @@ -97,30 +96,30 @@ instance Disp Env where debugDisp e = vcat [debugDisp decl | decl <- ctx e] -- | Find a name's user supplied type signature. -lookupHint :: (MonadReader Env m) => TName -> m (Maybe Sig) +lookupHint :: (MonadReader Env m) => TName -> m (Maybe Decl) lookupHint v = do hints <- asks hints - return $ listToMaybe [sig | sig <- hints, v == sigName sig] + return $ listToMaybe [sig | sig <- hints, v == declName sig] -- | Find a name's type in the context. lookupTyMaybe :: (MonadReader Env m) => TName -> - m (Maybe Sig) + m (Maybe Decl) lookupTyMaybe v = do ctx <- asks ctx return $ go ctx where go [] = Nothing - go (TypeSig sig : ctx) - | v == sigName sig = Just sig + go (TypeDecl sig : ctx) + | v == declName sig = Just sig | otherwise = go ctx go (_ : ctx) = go ctx -- | Find the type of a name specified in the context -- throwing an error if the name doesn't exist lookupTy :: - TName -> TcMonad Sig + TName -> TcMonad Decl lookupTy v = do x <- lookupTyMaybe v @@ -143,26 +142,18 @@ lookupDef v = do ctx <- asks ctx return $ listToMaybe [a | Def v' a <- ctx, v == v'] -lookupRecDef :: - (MonadReader Env m) => - TName -> - m (Maybe Term) -lookupRecDef v = do - ctx <- asks ctx - return $ listToMaybe [a | RecDef v' a <- ctx, v == v'] - -- | Extend the context with a new binding -extendCtx :: (MonadReader Env m) => Decl -> m a -> m a +extendCtx :: (MonadReader Env m) => Entry -> m a -> m a extendCtx d = local (\m@Env {ctx = cs} -> m {ctx = d : cs}) -- | Extend the context with a list of bindings -extendCtxs :: (MonadReader Env m) => [Decl] -> m a -> m a +extendCtxs :: (MonadReader Env m) => [Entry] -> m a -> m a extendCtxs ds = local (\m@Env {ctx = cs} -> m {ctx = ds ++ cs}) -- | Extend the context with a list of bindings, marking them as "global" -extendCtxsGlobal :: (MonadReader Env m) => [Decl] -> m a -> m a +extendCtxsGlobal :: (MonadReader Env m) => [Entry] -> m a -> m a extendCtxsGlobal ds = local ( \m@Env {ctx = cs} -> @@ -182,11 +173,11 @@ extendCtxMods :: (MonadReader Env m) => [Module] -> m a -> m a extendCtxMods mods k = foldr extendCtxMod k mods -- | Get the complete current context -getCtx :: MonadReader Env m => m [Decl] +getCtx :: MonadReader Env m => m [Entry] getCtx = asks ctx -- | Get the prefix of the context that corresponds to local variables. -getLocalCtx :: MonadReader Env m => m [Decl] +getLocalCtx :: MonadReader Env m => m [Entry] getLocalCtx = do g <- asks ctx glen <- asks globals @@ -202,7 +193,7 @@ getSourceLocation :: MonadReader Env m => m [SourceLocation] getSourceLocation = asks sourceLocation -- | Add a type hint -extendHints :: (MonadReader Env m) => Sig -> m a -> m a +extendHints :: (MonadReader Env m) => Decl -> m a -> m a extendHints h = local (\m@Env {hints = hs} -> m {hints = h : hs}) -- | An error that should be reported to the user diff --git a/version1/src/Equal.hs b/version1/src/Equal.hs index 91ace75..b92c8cd 100644 --- a/version1/src/Equal.hs +++ b/version1/src/Equal.hs @@ -98,11 +98,7 @@ whnf (Var x) = do maybeDef <- Env.lookupDef x case maybeDef of (Just d) -> whnf d - _ -> do - maybeRecDef <- Env.lookupRecDef x - case maybeRecDef of - (Just d) -> whnf d - _ -> return (Var x) + _ -> return (Var x) whnf (App t1 t2) = do nf <- whnf t1 case nf of @@ -132,7 +128,7 @@ whnf tm = return tm -- | 'Unify' the two terms, producing a list of Defs -- If there is an obvious mismatch, this function produces an error -- If either term is "ambiguous" just ignore. -unify :: [TName] -> Term -> Term -> TcMonad [Decl] +unify :: [TName] -> Term -> Term -> TcMonad [Entry] unify ns tx ty = do txnf <- whnf tx tynf <- whnf ty diff --git a/version1/src/Parser.hs b/version1/src/Parser.hs index 55b5252..62c07b5 100644 --- a/version1/src/Parser.hs +++ b/version1/src/Parser.hs @@ -63,13 +63,13 @@ Optional components in this BNF are marked with < > A -> B - Get parsed as (x:A) -> B, with an internal name for x + Get parsed as (_:A) -> B, with a wildcard name for the binder - Nondependent product types, like: A * B - Get parsed as { x:A | B }, with an internal name for x + Get parsed as { _:A | B }, with a wildcard name for the binder - You can collapse lambdas, like: @@ -85,6 +85,10 @@ Optional components in this BNF are marked with < > -} +-- | Default name (for parsing 'A -> B' as '(_:A) -> B') +wildcardName :: TName +wildcardName = Unbound.string2Name "_" + liftError :: (MonadError e m) => Either e a -> m a liftError (Left e) = throwError e liftError (Right a) = return a @@ -233,12 +237,12 @@ importDef = do reserved "import" >> (ModuleImport <$> importName) --- Top level declarations --- -decl, sigDef, valDef :: LParser Decl -decl = sigDef <|> valDef -sigDef = do +decl, declDef, valDef :: LParser Entry +decl = declDef <|> valDef +declDef = do n <- try (variable >>= \v -> colon >> return v) ty <- expr - return (mkSig n ty) + return (mkDecl n ty) valDef = do n <- try (do n <- variable; reservedOp "="; return n) val <- expr diff --git a/version1/src/PrettyPrint.hs b/version1/src/PrettyPrint.hs index 1f0892c..d375ba4 100644 --- a/version1/src/PrettyPrint.hs +++ b/version1/src/PrettyPrint.hs @@ -119,11 +119,11 @@ instance Disp Module instance Disp ModuleImport -instance Disp Decl +instance Disp Entry -instance Disp [Decl] +instance Disp [Entry] -instance Disp Sig +instance Disp Decl ------------------------------------------------------------------------ @@ -144,24 +144,23 @@ instance Display Module where instance Display ModuleImport where display (ModuleImport i) = pure $ PP.text "import" <+> disp i -instance Display [Decl] where +instance Display [Entry] where display ds = do dd <- mapM display ds pure $ PP.vcat dd -instance Display Sig where - display sig = do - dn <- display (sigName sig) - dt <- display (sigType sig) +instance Display Decl where + display decl = do + dn <- display (declName decl) + dt <- display (declType decl) pure $ dn <+> PP.text ":" <+> dt -instance Display Decl where +instance Display Entry where display (Def n term) = do dn <- display n dt <- display term pure $ dn <+> PP.text "=" <+> dt - display (RecDef n f) = display (Def n f) - display (TypeSig sig) = display sig + display (TypeDecl decl) = display decl ------------------------------------------------------------------------- diff --git a/version1/src/Syntax.hs b/version1/src/Syntax.hs index 0c3ce34..f17276d 100644 --- a/version1/src/Syntax.hs +++ b/version1/src/Syntax.hs @@ -25,9 +25,6 @@ import Unbound.Generics.LocallyNameless.Internal.Fold qualified as Unbound -- is a name for. type TName = Unbound.Name Term --- | module names -type ModuleName = String - ----------------------------------------- -- * Core language of pi-forall (Combined syntax for types and terms) @@ -86,12 +83,15 @@ data Term ----------------------------------------- +-- | module names +type ModuleName = String + -- | A Module has a name, a list of imports, a list of declarations, -- and a set of constructor names (which affect parsing). data Module = Module { moduleName :: ModuleName, moduleImports :: [ModuleImport], - moduleEntries :: [Decl] + moduleEntries :: [Entry] } deriving (Show, Generic, Typeable, Unbound.Alpha) @@ -100,32 +100,35 @@ newtype ModuleImport = ModuleImport ModuleName deriving (Show, Eq, Generic, Typeable) deriving anyclass (Unbound.Alpha) --- | A type declaration (or type signature) -data Sig = Sig {sigName :: TName, sigType :: Type} +-- | A type declaration (or type declnature) +data Decl = Decl {declName :: TName, declType :: Type} deriving (Show, Generic, Typeable, Unbound.Alpha, Unbound.Subst Term) -- | Declare the type of a term -mkSig :: TName -> Type -> Decl -mkSig n ty = TypeSig (Sig n ty) - --- | Declarations are the components of modules -data Decl - = -- | Declaration for the type of a term - TypeSig Sig - | -- | The definition of a particular name, must +mkDecl :: TName -> Type -> Entry +mkDecl n ty = TypeDecl (Decl n ty) + +-- | Entries are the components of modules +data Entry + = -- | Declaration for the type of a term 'x : A' + TypeDecl Decl + | -- | The definition of a particular name, must 'x = a' -- already have a type declaration in scope Def TName Term - | -- | A potentially (recursive) definition of - -- a particular name, must be declared - RecDef TName Term deriving (Show, Generic, Typeable) deriving anyclass (Unbound.Alpha, Unbound.Subst Term) +----------------------------------------- + -- * Auxiliary functions on syntax --- | Default name for '_' occurring in patterns -wildcardName :: TName -wildcardName = Unbound.string2Name "_" +----------------------------------------- + +-- | Remove source positions and type annotations from the top level of a term +strip :: Term -> Term +strip (Pos _ tm) = strip tm +strip (Ann tm _) = strip tm +strip tm = tm -- | Partial inverse of Pos unPos :: Term -> Maybe SourcePos @@ -136,18 +139,43 @@ unPos _ = Nothing unPosFlaky :: Term -> SourcePos unPosFlaky t = fromMaybe (newPos "unknown location" 0 0) (unPos t) ------------------ +----------------------------------------- + +-- * Unbound library + +----------------------------------------- -- We use the unbound-generics library to mark the binding occurrences of -- variables in the syntax. That allows us to automatically derive -- functions for alpha-equivalence, free variables and substitution -- using generic programming. +-- | Determine when two terms are alpha-equivalent (see below) +aeq :: Term -> Term -> Bool +aeq = Unbound.aeq + +-- | Calculate the free variables of a term +fv :: Term -> [Unbound.Name Term] +fv = Unbound.toListOf Unbound.fv + +-- | subst x b a means to replace x with b in a +-- i.e. a [ b / x ] +subst :: TName -> Term -> Term -> Term +subst = Unbound.subst + +-- | in a binder "x.a" replace x with b +instantiate :: Unbound.Bind TName Term -> Term -> Term +instantiate bnd a = Unbound.instantiate bnd [a] + +-- | in a binder "x.a" replace x with a fresh name +unbind :: (Unbound.Fresh m) => Unbound.Bind TName Term -> m (TName, Term) +unbind = Unbound.unbind + ------------------ -- * Alpha equivalence and free variables --- Among other things, the Alpha class enables the following +-- The Unbound library's Alpha class enables the following -- functions: -- -- Compare terms for alpha equivalence -- aeq :: Alpha a => a -> a -> Bool @@ -157,23 +185,21 @@ unPosFlaky t = fromMaybe (newPos "unknown location" 0 0) (unPos t) -- unbind :: (Alpha p, Alpha t, Fresh m) => Bind p t -> m (p, t) -- For Terms, we'd like Alpha equivalence to ignore --- source positions and type annotations. --- We can add these special cases to the definition of `aeq'` --- and then defer all other cases to the generic version of --- the function (Unbound.gaeq). +-- source positions and type annotations. So we make sure to +-- remove them before calling the generic operation. instance Unbound.Alpha Term where - aeq' ctx (Ann a _) b = Unbound.aeq' ctx a b - aeq' ctx a (Ann b _) = Unbound.aeq' ctx a b - aeq' ctx (Pos _ a) b = Unbound.aeq' ctx a b - aeq' ctx a (Pos _ b) = Unbound.aeq' ctx a b - aeq' ctx a b = (Unbound.gaeq ctx `on` from) a b + aeq' :: Unbound.AlphaCtx -> Term -> Term -> Bool + aeq' ctx a b = (Unbound.gaeq ctx `on` from) (strip a) (strip b) -- For example, all occurrences of annotations and source positions -- are ignored by this definition. --- >>> Unbound.aeq (Pos internalPos (Ann TyBool Type)) TyBool --- True +-- '(Bool : Type)' is alpha-equivalent to 'Bool' +-- >>> aeq (Ann TyBool TyType) TyBool + +-- '(Bool, Bool:Type)' is alpha-equivalent to (Bool, Bool) +-- >>> aeq (Prod TyBool (Ann TyBool TyType)) (Prod TyBool TyBool) -- At the same time, the generic operation equates terms that differ only -- in the names of bound variables. @@ -194,7 +220,7 @@ idx = Lam (Unbound.bind xName (Var xName)) idy :: Term idy = Lam (Unbound.bind yName (Var yName)) --- >>> Unbound.aeq idx idy +-- >>> aeq idx idy -- True --------------- @@ -221,14 +247,6 @@ pi2 :: Term pi2 = TyPi TyBool (Unbound.bind yName (Var yName)) -- >>> Unbound.aeq (Unbound.subst xName TyBool pi1) pi2 --- True --- - ---------------- - --- | Bridge function to calculate the free variables of a term -fv :: Term -> [Unbound.Name Term] -fv = Unbound.toListOf Unbound.fv ----------------- @@ -252,8 +270,7 @@ instance Unbound.Alpha SourcePos where acompare' _ _ _ = EQ -- Substitutions ignore source positions -instance Unbound.Subst b SourcePos where subst _ _ = id; substs _ = id; substBvs _ _ = id - --- Internally generated source positions -internalPos :: SourcePos -internalPos = initialPos "internal" +instance Unbound.Subst b SourcePos where + subst _ _ = id + substs _ = id + substBvs _ _ = id diff --git a/version1/src/TypeCheck.hs b/version1/src/TypeCheck.hs index 024f577..64f9548 100644 --- a/version1/src/TypeCheck.hs +++ b/version1/src/TypeCheck.hs @@ -1,5 +1,4 @@ {- pi-forall -} -{-# OPTIONS_GHC -Wno-unrecognised-pragmas #-} {-# HLINT ignore "Use forM_" #-} @@ -18,102 +17,111 @@ import Text.PrettyPrint.HughesPJ (render, ($$)) import Unbound.Generics.LocallyNameless qualified as Unbound import Unbound.Generics.LocallyNameless.Internal.Fold qualified as Unbound +--------------------------------------------------------------------- + -- | Infer/synthesize the type of a term inferType :: Term -> TcMonad Type -inferType t = tcTerm t Nothing - --- | Check that the given term has the expected type -checkType :: Term -> Type -> TcMonad () -checkType tm (Pos _ ty) = checkType tm ty -- ignore source positions/annotations -checkType tm (Ann ty _) = checkType tm ty -checkType tm ty = void $ tcTerm tm (Just ty) +inferType t = case t of + -- i-var + (Var x) -> do + decl <- Env.lookupTy x + return (declType decl) + + -- i-type + TyType -> return TyType + -- i-pi + (TyPi tyA bnd) -> do + (x, tyB) <- Unbound.unbind bnd + tcType tyA + Env.extendCtx (mkDecl x tyA) (tcType tyB) + return TyType + + -- i-app + (App t1 t2) -> do + ty1 <- inferType t1 + let ensurePi :: Type -> TcMonad (Type, Unbound.Bind TName Type) + ensurePi (Pos _ ty) = ensurePi ty + ensurePi (Ann tm _) = ensurePi tm + ensurePi (TyPi tyA bnd) = return (tyA, bnd) + ensurePi ty = Env.err [DS "Expected a function type but found ", DD ty] + (tyA, bnd) <- ensurePi ty1 + checkType t2 tyA + return (Unbound.instantiate bnd [t2]) + + -- i-ann + (Ann tm ty) -> do + tcType ty + checkType tm ty + return ty + + -- Practicalities + -- remember the current position in the type checking monad + (Pos p tm) -> + Env.extendSourceLocation p tm $ inferType tm + -- Extensions to the core language + -- i-unit + TyUnit -> return TyType + LitUnit -> return TyUnit + -- i-bool + TyBool -> Env.err [DS "unimplemented"] + -- i-true/false + (LitBool b) -> Env.err [DS "unimplemented"] + -- i-if + (If t1 t2 t3) -> Env.err [DS "unimplemented"] + -- i-sigma + (TySigma tyA bnd) -> Env.err [DS "unimplemented"] + -- cannot synthesize the type of the term + tm -> + Env.err [DS "Must have a type for", DD tm] + +------------------------------------------------------------------------- -- | Make sure that the term is a "type" (i.e. that it has type 'Type') tcType :: Term -> TcMonad () -tcType tm = void $ checkType tm TyType +tcType tm = checkType tm TyType ---------------------------------------------------------------------- +------------------------------------------------------------------------- --- | Combined type checking/inference function --- The second argument is 'Just expectedType' in checking mode and 'Nothing' in inference mode --- In either case, this function returns the type of the term -tcTerm :: Term -> Maybe Type -> TcMonad Type --- i-var -tcTerm t@(Var x) Nothing = do - sig <- Env.lookupTy x - return (sigType sig) --- i-type -tcTerm TyType Nothing = return TyType --- i-pi -tcTerm (TyPi tyA bnd) Nothing = do - (x, tyB) <- Unbound.unbind bnd - tcType tyA - Env.extendCtx (mkSig x tyA) (tcType tyB) - return TyType --- c-lam: check the type of a function -tcTerm (Lam bnd) (Just (TyPi tyA bnd2)) = do - -- unbind the variables in the lambda expression and pi type - (x, body, _, tyB) <- Unbound.unbind2Plus bnd bnd2 - - -- check the type of the body of the lambda expression - Env.extendCtx (mkSig x tyA) (checkType body tyB) - return (TyPi tyA bnd2) -tcTerm (Lam _) (Just nf) = - Env.err [DS "Lambda expression should have a function type, not", DD nf] --- i-app -tcTerm (App t1 t2) Nothing = do - ty1 <- inferType t1 - let ensurePi :: Type -> TcMonad (Type, Unbound.Bind TName Type) - ensurePi (Ann a _) = ensurePi a - ensurePi (Pos _ a) = ensurePi a - ensurePi (TyPi tyA bnd) = return (tyA, bnd) - ensurePi ty = Env.err [DS "Expected a function type but found ", DD ty] - (tyA, bnd) <- ensurePi ty1 - checkType t2 tyA - return (Unbound.instantiate bnd [t2]) - --- i-ann -tcTerm (Ann tm ty) Nothing = do - tcType ty - checkType tm ty - return ty - --- practicalities --- remember the current position in the type checking monad -tcTerm (Pos p tm) mTy = - Env.extendSourceLocation p tm $ tcTerm tm mTy --- ignore term, just return type annotation -tcTerm TrustMe (Just ty) = return ty --- i-unit -tcTerm TyUnit Nothing = return TyType -tcTerm LitUnit Nothing = return TyUnit --- i-bool -tcTerm TyBool Nothing = Env.err [DS "unimplemented"] --- i-true/false -tcTerm (LitBool b) Nothing = Env.err [DS "unimplemented"] --- c-if -tcTerm t@(If t1 t2 t3) mty = Env.err [DS "unimplemented"] -tcTerm (Let rhs bnd) mty = Env.err [DS "unimplemented"] -tcTerm t@(TySigma tyA bnd) Nothing = Env.err [DS "unimplemented"] -tcTerm t@(Prod a b) (Just ty) = Env.err [DS "unimplemented"] -tcTerm t@(LetPair p bnd) (Just ty) = Env.err [DS "unimplemented"] -tcTerm PrintMe (Just ty) = do - gamma <- Env.getLocalCtx - Env.warn - [ DS "Unmet obligation.\nContext:", - DD gamma, - DS "\nGoal:", - DD ty - ] - return ty - --- c-infer -tcTerm tm (Just ty) = do - ty' <- inferType tm - unless (Unbound.aeq ty' ty) $ Env.err [DS "Types don't match", DD ty, DS "and", DD ty'] - return ty' -tcTerm tm Nothing = - Env.err [DS "Must have a type annotation to check", DD tm] +-- | Check that the given term has the expected type +checkType :: Term -> Type -> TcMonad () +checkType tm ty' = do + let ty = strip ty' -- ignore source positions/annotations + case tm of + -- c-lam: check the type of a function + (Lam bnd) -> case ty of + (TyPi tyA bnd2) -> do + -- unbind the variables in the lambda expression and pi type + (x, body, _, tyB) <- Unbound.unbind2Plus bnd bnd2 + + -- check the type of the body of the lambda expression + Env.extendCtx (mkDecl x tyA) (checkType body tyB) + _ -> Env.err [DS "Lambda expression should have a function type, not", DD ty] + -- Practicalities + (Pos p tm) -> + Env.extendSourceLocation p tm $ checkType tm ty + TrustMe -> return () + PrintMe -> do + gamma <- Env.getLocalCtx + Env.warn + [ DS "Unmet obligation.\nContext:", + DD gamma, + DS "\nGoal:", + DD ty + ] + + -- Extensions to the core language + -- c-if + (If t1 t2 t3) -> Env.err [DS "unimplemented"] + -- c-let + (Let rhs bnd) -> Env.err [DS "unimplemented"] + -- c-prod + (Prod a b) -> Env.err [DS "unimplemented"] + -- c-letpair + (LetPair p bnd) -> Env.err [DS "unimplemented"] + -- c-infer + tm -> do + ty' <- inferType tm + unless (Unbound.aeq ty' ty) $ Env.err [DS "Types don't match", DD ty, DS "and", DD ty'] -------------------------------------------------------- -- Using the typechecker for decls and modules and stuff @@ -135,11 +143,11 @@ tcModules = foldM tcM [] -- | Typecheck an entire module. tcModule :: - -- | List of already checked modules (including their Decls). + -- | List of already checked modules (including their entries). [Module] -> -- | Module to check. Module -> - -- | The same module with all Decls checked and elaborated. + -- | The same module with all entries checked and elaborated. TcMonad Module tcModule defs m' = do checkedEntries <- @@ -151,23 +159,23 @@ tcModule defs m' = do return $ m' {moduleEntries = checkedEntries} where d `tcE` m = do - -- Extend the Env per the current Decl before checking - -- subsequent Decls. + -- Extend the Env per the current Entry before checking + -- subsequent entries. x <- tcEntry d case x of AddHint hint -> Env.extendHints hint m - -- Add decls to the Decls to be returned + -- Add decls to the entries to be returned AddCtx decls -> (decls ++) <$> Env.extendCtxsGlobal decls m -- Get all of the defs from imported modules (this is the env to check current module in) importedModules = filter (\x -> ModuleImport (moduleName x) `elem` moduleImports m') defs --- | The Env-delta returned when type-checking a top-level Decl. +-- | The Env-delta returned when type-checking a top-level Entry. data HintOrCtx - = AddHint Sig - | AddCtx [Decl] + = AddHint Decl + | AddCtx [Entry] -- | Check each sort of declaration in a module -tcEntry :: Decl -> TcMonad HintOrCtx +tcEntry :: Entry -> TcMonad HintOrCtx tcEntry (Def n term) = do oldDef <- Env.lookupDef n maybe tc die oldDef @@ -177,21 +185,19 @@ tcEntry (Def n term) = do case lkup of Nothing -> do ty <- inferType term - return $ AddCtx [TypeSig (Sig n ty), Def n term] - Just sig -> + return $ AddCtx [TypeDecl (Decl n ty), Def n term] + Just decl -> let handler (Env.Err ps msg) = throwError $ Env.Err ps (msg $$ msg') msg' = disp [ DS "When checking the term", DD term, - DS "against the signature", - DD sig + DS "against the type", + DD decl ] in do - Env.extendCtx (TypeSig sig) $ checkType term (sigType sig) `catchError` handler - if n `elem` fv term - then return $ AddCtx [TypeSig sig, RecDef n term] - else return $ AddCtx [TypeSig sig, Def n term] + Env.extendCtx (TypeDecl decl) $ checkType term (declType decl) `catchError` handler + return $ AddCtx [TypeDecl decl, Def n term] die term' = Env.extendSourceLocation (unPosFlaky term) term $ Env.err @@ -200,30 +206,29 @@ tcEntry (Def n term) = do DS "Previous definition was", DD term' ] -tcEntry (TypeSig sig) = do - duplicateTypeBindingCheck sig - tcType (sigType sig) - return $ AddHint sig -tcEntry _ = Env.err "unimplemented" +tcEntry (TypeDecl decl) = do + duplicateTypeBindingCheck decl + tcType (declType decl) + return $ AddHint decl -- | Make sure that we don't have the same name twice in the -- environment. (We don't rename top-level module definitions.) -duplicateTypeBindingCheck :: Sig -> TcMonad () -duplicateTypeBindingCheck sig = do +duplicateTypeBindingCheck :: Decl -> TcMonad () +duplicateTypeBindingCheck decl = do -- Look for existing type bindings ... - let n = sigName sig + let n = declName decl l <- Env.lookupTyMaybe n l' <- Env.lookupHint n -- ... we don't care which, if either are Just. case catMaybes [l, l'] of [] -> return () -- We already have a type in the environment so fail. - sig' : _ -> - let p = unPosFlaky $ sigType sig + decl' : _ -> + let p = unPosFlaky $ declType decl msg = - [ DS "Duplicate type signature", - DD sig, + [ DS "Duplicate type declaration", + DD decl, DS "Previous was", - DD sig' + DD decl' ] - in Env.extendSourceLocation p sig $ Env.err msg + in Env.extendSourceLocation p decl $ Env.err msg diff --git a/version2/pi-forall.cabal b/version2/pi-forall.cabal index e7a8c0c..ee29759 100644 --- a/version2/pi-forall.cabal +++ b/version2/pi-forall.cabal @@ -21,7 +21,7 @@ common shared-properties default-language: GHC2021 ghc-options: - -Wall -fno-warn-unused-matches -fno-warn-orphans -fno-warn-unused-top-binds -fno-warn-unused-imports -fno-warn-name-shadowing + -Wall -fno-warn-unused-matches -fno-warn-orphans -fno-warn-unused-top-binds -fno-warn-unused-imports -fno-warn-name-shadowing -Wno-unrecognised-pragmas default-extensions: DefaultSignatures DeriveAnyClass diff --git a/version2/src/Environment.hs b/version2/src/Environment.hs index f452302..b052e1f 100644 --- a/version2/src/Environment.hs +++ b/version2/src/Environment.hs @@ -9,7 +9,6 @@ module Environment lookupTy, lookupTyMaybe, lookupDef, - lookupRecDef, lookupHint , getCtx, getLocalCtx, @@ -60,15 +59,15 @@ data SourceLocation where -- | Environment manipulation and accessing functions -- The context 'gamma' is a list data Env = Env - { -- | elaborated term and datatype declarations. - ctx :: [Decl], + { -- | elaborated term and datatype declarations + ctx :: [Entry], -- | how long the tail of "global" variables in the context is -- (used to supress printing those in error messages) globals :: Int, - -- | Type declarations (signatures): it's not safe to + -- | Type declarations: it's not safe to -- put these in the context until a corresponding term -- has been checked. - hints :: [Sig], + hints :: [Decl], -- | what part of the file we are in (for errors/warnings) sourceLocation :: [SourceLocation] } @@ -90,22 +89,22 @@ instance Disp Env where debugDisp e = vcat [debugDisp decl | decl <- ctx e] -- | Find a name's user supplied type signature. -lookupHint :: (MonadReader Env m) => TName -> m (Maybe Sig) +lookupHint :: (MonadReader Env m) => TName -> m (Maybe Decl) lookupHint v = do hints <- asks hints - return $ listToMaybe [ sig | sig <- hints, v == sigName sig] + return $ listToMaybe [ sig | sig <- hints, v == declName sig] -- | Find a name's type in the context. lookupTyMaybe :: (MonadReader Env m) => TName -> - m (Maybe Sig) + m (Maybe Decl) lookupTyMaybe v = do ctx <- asks ctx return $ go ctx where go [] = Nothing - go (TypeSig sig : ctx) - | v == sigName sig = Just sig + go (TypeDecl sig : ctx) + | v == declName sig = Just sig | otherwise = go ctx go (_ : ctx) = go ctx @@ -115,7 +114,7 @@ lookupTyMaybe v = do -- | Find the type of a name specified in the context -- throwing an error if the name doesn't exist lookupTy :: - TName -> TcMonad Sig + TName -> TcMonad Decl lookupTy v = do x <- lookupTyMaybe v @@ -138,28 +137,20 @@ lookupDef v = do ctx <- asks ctx return $ listToMaybe [a | Def v' a <- ctx, v == v'] -lookupRecDef :: - (MonadReader Env m) => - TName -> - m (Maybe Term) -lookupRecDef v = do - ctx <- asks ctx - return $ listToMaybe [a | RecDef v' a <- ctx, v == v'] - -- | Extend the context with a new binding -extendCtx :: (MonadReader Env m) => Decl -> m a -> m a +extendCtx :: (MonadReader Env m) => Entry -> m a -> m a extendCtx d = local (\m@Env{ctx = cs} -> m {ctx = d : cs}) -- | Extend the context with a list of bindings -extendCtxs :: (MonadReader Env m) => [Decl] -> m a -> m a +extendCtxs :: (MonadReader Env m) => [Entry] -> m a -> m a extendCtxs ds = local (\m@Env {ctx = cs} -> m {ctx = ds ++ cs}) -- | Extend the context with a list of bindings, marking them as "global" -extendCtxsGlobal :: (MonadReader Env m) => [Decl] -> m a -> m a +extendCtxsGlobal :: (MonadReader Env m) => [Entry] -> m a -> m a extendCtxsGlobal ds = local ( \m@Env {ctx = cs} -> @@ -181,11 +172,11 @@ extendCtxMods :: (MonadReader Env m) => [Module] -> m a -> m a extendCtxMods mods k = foldr extendCtxMod k mods -- | Get the complete current context -getCtx :: MonadReader Env m => m [Decl] +getCtx :: MonadReader Env m => m [Entry] getCtx = asks ctx -- | Get the prefix of the context that corresponds to local variables. -getLocalCtx :: MonadReader Env m => m [Decl] +getLocalCtx :: MonadReader Env m => m [Entry] getLocalCtx = do g <- asks ctx glen <- asks globals @@ -201,7 +192,7 @@ getSourceLocation :: MonadReader Env m => m [SourceLocation] getSourceLocation = asks sourceLocation -- | Add a type hint -extendHints :: (MonadReader Env m) => Sig -> m a -> m a +extendHints :: (MonadReader Env m) => Decl -> m a -> m a extendHints h = local (\m@Env {hints = hs} -> m {hints = h : hs}) -- | An error that should be reported to the user diff --git a/version2/src/Equal.hs b/version2/src/Equal.hs index 48a82d6..d91dd5a 100644 --- a/version2/src/Equal.hs +++ b/version2/src/Equal.hs @@ -129,11 +129,7 @@ whnf (Var x) = do maybeDef <- Env.lookupDef x case maybeDef of (Just d) -> whnf d - _ -> do - maybeRecDef <- Env.lookupRecDef x - case maybeRecDef of - (Just d) -> whnf d - _ -> return (Var x) + _ -> return (Var x) whnf (App t1 t2) = do nf <- whnf t1 @@ -176,7 +172,7 @@ whnf tm = return tm -- | 'Unify' the two terms, producing a list of Defs -- If there is an obvious mismatch, this function produces an error -- If either term is "ambiguous" just ignore. -unify :: [TName] -> Term -> Term -> TcMonad [Decl] +unify :: [TName] -> Term -> Term -> TcMonad [Entry] unify ns tx ty = do txnf <- whnf tx tynf <- whnf ty diff --git a/version2/src/Parser.hs b/version2/src/Parser.hs index 4957156..a6039d6 100644 --- a/version2/src/Parser.hs +++ b/version2/src/Parser.hs @@ -3,7 +3,7 @@ -- | A parsec-based parser for the concrete syntax module Parser ( - parseModuleFile, + parseModuleFile, parseModuleImports, parseExpr, expr, @@ -19,7 +19,7 @@ import qualified Unbound.Generics.LocallyNameless as Unbound import Text.Parsec hiding (State,Empty) import Text.Parsec.Expr(Operator(..),Assoc(..),buildExpressionParser) -import qualified LayoutToken as Token +import qualified LayoutToken as Token import Control.Monad.State.Lazy hiding (join) import Control.Monad.Except ( MonadError(throwError) ) @@ -79,13 +79,13 @@ Optional components in this BNF are marked with < > A -> B - Get parsed as (x:A) -> B, with an internal name for x + Get parsed as (_:A) -> B, with a wildcard name for the binder - Nondependent product types, like: A * B - Get parsed as { x:A | B }, with an internal name for x + Get parsed as { _:A | B }, with a wildcard name for the binder - You can collapse lambdas, like: @@ -101,6 +101,12 @@ Optional components in this BNF are marked with < > -} + +-- | Default name (for parsing 'A -> B' as '(_:A) -> B') +wildcardName :: TName +wildcardName = Unbound.string2Name "_" + + liftError :: (MonadError e m) => Either e a -> m a liftError (Left e) = throwError e liftError (Right a) = return a @@ -117,13 +123,13 @@ parseModuleFile name = do parseModuleImports :: (MonadError ParseError m, MonadIO m) => String -> m Module parseModuleImports name = do contents <- liftIO $ readFile name - liftError $ Unbound.runFreshM $ + liftError $ Unbound.runFreshM $ (runParserT (do { whiteSpace; moduleImports }) [] name contents) -- | Test an 'LParser' on a String. testParser :: LParser t -> String -> Either ParseError t -testParser parser str = Unbound.runFreshM $ +testParser parser str = Unbound.runFreshM $ runParserT (do { whiteSpace; v <- parser; eof; return v}) [] "" str @@ -171,10 +177,10 @@ piforallStyle = Token.LanguageDef ,"axiom" ,"TRUSTME" ,"PRINTME" - ,"ord" - ,"Bool", "True", "False" + ,"ord" + ,"Bool", "True", "False" ,"if","then","else" - ,"Unit", "()" + ,"Unit", "()" ] , Token.reservedOpNames = ["!","?","\\",":",".",",","<", "=", "+", "-", "*", "^", "()", "_","|","{", "}"] @@ -191,9 +197,9 @@ whiteSpace = Token.whiteSpace tokenizer variable :: LParser TName variable = - do i <- identifier + do i <- identifier return $ Unbound.string2Name i - + @@ -202,7 +208,7 @@ colon, dot, comma :: LParser () colon = Token.colon tokenizer >> return () dot = Token.dot tokenizer >> return () comma = Token.comma tokenizer >> return () - + reserved,reservedOp :: String -> LParser () reserved = Token.reserved tokenizer reservedOp = Token.reservedOp tokenizer @@ -237,20 +243,20 @@ importDef = do reserved "import" >> (ModuleImport <$> importName) where importName = identifier - + --- --- Top level declarations --- -decl,sigDef,valDef :: LParser Decl -decl = sigDef <|> valDef +decl,declDef,valDef :: LParser Entry +decl = declDef <|> valDef + - -sigDef = do +declDef = do n <- try (variable >>= \v -> colon >> return v) ty <- expr - return (mkSig n ty) + return (mkDecl n ty) valDef = do n <- try (do {n <- variable; reservedOp "="; return n}) @@ -273,13 +279,13 @@ printme = reserved "PRINTME" *> return (PrintMe ) refl :: LParser Term refl = do reserved "Refl" - return $ Refl + return $ Refl -- Expressions expr,term,factor :: LParser Term - + -- expr is the toplevel expression grammar expr = do p <- getPosition @@ -288,18 +294,18 @@ expr = do [ifix AssocLeft "=" TyEq], [ifixM AssocRight "->" mkArrowType], [ifixM AssocRight "*" mkTupleType] - ] + ] ifix assoc op f = Infix (reservedOp op >> return f) assoc ifixM assoc op f = Infix (reservedOp op >> f) assoc - mkArrowType = + mkArrowType = do n <- Unbound.fresh wildcardName - return $ \tyA tyB -> + return $ \tyA tyB -> TyPi tyA (Unbound.bind n tyB) - mkTupleType = + mkTupleType = do n <- Unbound.fresh wildcardName - return $ \tyA tyB -> + return $ \tyA tyB -> TySigma tyA (Unbound.bind n tyB) - + -- A "term" is either a function application or a constructor -- application. Breaking it out as a seperate category both -- eliminates left-recursion in ( := ) and @@ -307,16 +313,16 @@ expr = do term = funapp - + funapp :: LParser Term -funapp = do +funapp = do f <- factor foldl' app f <$> many bfactor where bfactor = factor app e1 e2 = App e1 e2 -factor = choice [ Var <$> variable "a variable" +factor = choice [ Var <$> variable "a variable" , typen "Type" , lambda "a lambda" , try letPairExp "a let pair" @@ -328,10 +334,10 @@ factor = choice [ Var <$> variable "a variable" , trustme "TRUSTME" , printme "PRINTME" - , bconst "a constant" - , ifExpr "an if expression" - , sigmaTy "a sigma type" - + , bconst "a constant" + , ifExpr "an if expression" + , sigmaTy "a sigma type" + , expProdOrAnnotOrParens "an explicit function type or annotated expression" ] @@ -351,11 +357,11 @@ lambda = do reservedOp "\\" binds <- many1 variable dot body <- expr - return $ foldr lam body binds + return $ foldr lam body binds where - lam x m = Lam (Unbound.bind x m) + lam x m = Lam (Unbound.bind x m) + - bconst :: LParser Term @@ -367,7 +373,7 @@ bconst = choice [reserved "Bool" >> return TyBool, ifExpr :: LParser Term -ifExpr = +ifExpr = do reserved "if" a <- expr reserved "then" @@ -375,7 +381,7 @@ ifExpr = reserved "else" c <- expr return (If a b c ) - + -- letExpr :: LParser Term @@ -441,13 +447,13 @@ expProdOrAnnotOrParens = (do b <- afterBinder return $ TyPi a (Unbound.bind x b)) Colon a b -> return $ Ann a b - - Comma a b -> + + Comma a b -> return $ Prod a b Nope a -> return a - - + + -- subst e0 by e1 substExpr :: LParser Term @@ -456,16 +462,16 @@ substExpr = do a <- expr reserved "by" b <- expr - return $ Subst a b + return $ Subst a b contra :: LParser Term contra = do reserved "contra" witness <- expr - return $ Contra witness + return $ Contra witness -sigmaTy :: LParser Term +sigmaTy :: LParser Term sigmaTy = do reservedOp "{" x <- variable @@ -475,5 +481,5 @@ sigmaTy = do b <- expr reservedOp "}" return (TySigma a (Unbound.bind x b)) - - + + diff --git a/version2/src/PrettyPrint.hs b/version2/src/PrettyPrint.hs index 11dfc74..b7d7937 100644 --- a/version2/src/PrettyPrint.hs +++ b/version2/src/PrettyPrint.hs @@ -120,11 +120,11 @@ instance Disp Module instance Disp ModuleImport -instance Disp Decl +instance Disp Entry -instance Disp [Decl] +instance Disp [Entry] -instance Disp Sig +instance Disp Decl @@ -149,24 +149,23 @@ instance Display Module where instance Display ModuleImport where display (ModuleImport i) = pure $ PP.text "import" <+> disp i -instance Display [Decl] where +instance Display [Entry] where display ds = do dd <- mapM display ds pure $ PP.vcat dd -instance Display Sig where - display sig = do - dn <- display (sigName sig) - dt <- display (sigType sig) +instance Display Decl where + display decl = do + dn <- display (declName decl) + dt <- display (declType decl) pure $ dn <+> PP.text ":" <+> dt -instance Display Decl where +instance Display Entry where display (Def n term) = do dn <- display n dt <- display term pure $ dn <+> PP.text "=" <+> dt - display (RecDef n f) = display (Def n f) - display (TypeSig sig) = display sig + display (TypeDecl decl) = display decl diff --git a/version2/src/Syntax.hs b/version2/src/Syntax.hs index 119e13e..47e68cc 100644 --- a/version2/src/Syntax.hs +++ b/version2/src/Syntax.hs @@ -25,11 +25,8 @@ import Data.Function (on) -- and alpha-equality function. The abstract type `Name` from -- this library is indexed by the AST type that this variable -- is a name for. -type TName = Unbound.Name Term - --- | module names -type ModuleName = String +type TName = Unbound.Name Term ----------------------------------------- @@ -102,12 +99,15 @@ data Term ----------------------------------------- +-- | module names +type ModuleName = String + -- | A Module has a name, a list of imports, a list of declarations, -- and a set of constructor names (which affect parsing). data Module = Module { moduleName :: ModuleName, moduleImports :: [ModuleImport], - moduleEntries :: [Decl] + moduleEntries :: [Entry] } deriving (Show, Generic, Typeable, Unbound.Alpha) @@ -116,36 +116,39 @@ newtype ModuleImport = ModuleImport ModuleName deriving (Show, Eq, Generic, Typeable) deriving anyclass (Unbound.Alpha) --- | A type declaration (or type signature) -data Sig = Sig {sigName :: TName , sigType :: Type} +-- | A type declaration (or type declnature) +data Decl = Decl {declName :: TName , declType :: Type} deriving (Show, Generic, Typeable, Unbound.Alpha, Unbound.Subst Term) -- | Declare the type of a term -mkSig :: TName -> Type -> Decl -mkSig n ty = TypeSig (Sig n ty) - --- | Declarations are the components of modules -data Decl - = -- | Declaration for the type of a term - TypeSig Sig - | -- | The definition of a particular name, must +mkDecl :: TName -> Type -> Entry +mkDecl n ty = TypeDecl (Decl n ty) + +-- | Entries are the components of modules +data Entry + = -- | Declaration for the type of a term 'x : A' + TypeDecl Decl + | -- | The definition of a particular name, must 'x = a' -- already have a type declaration in scope Def TName Term - | -- | A potentially (recursive) definition of - -- a particular name, must be declared - RecDef TName Term deriving (Show, Generic, Typeable) deriving anyclass (Unbound.Alpha, Unbound.Subst Term) --- * Auxiliary functions on syntax --- | Default name for '_' occurring in patterns -wildcardName :: TName -wildcardName = Unbound.string2Name "_" +----------------------------------------- +-- * Auxiliary functions on syntax +----------------------------------------- + + +-- | Remove source positions and type annotations from the top level of a term +strip :: Term -> Term +strip (Pos _ tm) = strip tm +strip (Ann tm _) = strip tm +strip tm = tm -- | Partial inverse of Pos unPos :: Term -> Maybe SourcePos @@ -157,18 +160,41 @@ unPosFlaky :: Term -> SourcePos unPosFlaky t = fromMaybe (newPos "unknown location" 0 0) (unPos t) ------------------ + +----------------------------------------- +-- * Unbound library +----------------------------------------- -- We use the unbound-generics library to mark the binding occurrences of -- variables in the syntax. That allows us to automatically derive -- functions for alpha-equivalence, free variables and substitution -- using generic programming. +-- | Determine when two terms are alpha-equivalent (see below) +aeq :: Term -> Term -> Bool +aeq = Unbound.aeq + +-- | Calculate the free variables of a term +fv :: Term -> [Unbound.Name Term] +fv = Unbound.toListOf Unbound.fv + +-- | subst x b a means to replace x with b in a +-- i.e. a [ b / x ] +subst :: TName -> Term -> Term -> Term +subst = Unbound.subst + +-- | in a binder "x.a" replace x with b +instantiate :: Unbound.Bind TName Term -> Term -> Term +instantiate bnd a = Unbound.instantiate bnd [a] + +-- | in a binder "x.a" replace x with a fresh name +unbind :: (Unbound.Fresh m) => Unbound.Bind TName Term -> m (TName, Term) +unbind = Unbound.unbind ------------------ -- * Alpha equivalence and free variables --- Among other things, the Alpha class enables the following +-- The Unbound library's Alpha class enables the following -- functions: -- -- Compare terms for alpha equivalence -- aeq :: Alpha a => a -> a -> Bool @@ -178,23 +204,23 @@ unPosFlaky t = fromMaybe (newPos "unknown location" 0 0) (unPos t) -- unbind :: (Alpha p, Alpha t, Fresh m) => Bind p t -> m (p, t) -- For Terms, we'd like Alpha equivalence to ignore --- source positions and type annotations. --- We can add these special cases to the definition of `aeq'` --- and then defer all other cases to the generic version of --- the function (Unbound.gaeq). +-- source positions and type annotations. So we make sure to +-- remove them before calling the generic operation. instance Unbound.Alpha Term where - aeq' ctx (Ann a _) b = Unbound.aeq' ctx a b - aeq' ctx a (Ann b _) = Unbound.aeq' ctx a b - aeq' ctx (Pos _ a) b = Unbound.aeq' ctx a b - aeq' ctx a (Pos _ b) = Unbound.aeq' ctx a b - aeq' ctx a b = (Unbound.gaeq ctx `on` from) a b + aeq' :: Unbound.AlphaCtx -> Term -> Term -> Bool + aeq' ctx a b = (Unbound.gaeq ctx `on` from) (strip a) (strip b) + -- For example, all occurrences of annotations and source positions -- are ignored by this definition. --- >>> Unbound.aeq (Pos internalPos (Ann TyBool Type)) TyBool --- True +-- '(Bool : Type)' is alpha-equivalent to 'Bool' +-- >>> aeq (Ann TyBool TyType) TyBool + +-- '(Bool, Bool:Type)' is alpha-equivalent to (Bool, Bool) +-- >>> aeq (Prod TyBool (Ann TyBool TyType)) (Prod TyBool TyBool) + -- At the same time, the generic operation equates terms that differ only -- in the names of bound variables. @@ -215,7 +241,7 @@ idx = Lam (Unbound.bind xName (Var xName)) idy :: Term idy = Lam (Unbound.bind yName (Var yName)) --- >>> Unbound.aeq idx idy +-- >>> aeq idx idy -- True @@ -244,14 +270,6 @@ pi2 :: Term pi2 = TyPi TyBool (Unbound.bind yName (Var yName)) -- >>> Unbound.aeq (Unbound.subst xName TyBool pi1) pi2 --- True --- - ---------------- --- | Bridge function to calculate the free variables of a term - -fv :: Term -> [Unbound.Name Term] -fv = Unbound.toListOf Unbound.fv ----------------- @@ -275,10 +293,11 @@ instance Unbound.Alpha SourcePos where acompare' _ _ _ = EQ -- Substitutions ignore source positions -instance Unbound.Subst b SourcePos where subst _ _ = id; substs _ = id; substBvs _ _ = id +instance Unbound.Subst b SourcePos where + subst _ _ = id + substs _ = id + substBvs _ _ = id + --- Internally generated source positions -internalPos :: SourcePos -internalPos = initialPos "internal" diff --git a/version2/src/TypeCheck.hs b/version2/src/TypeCheck.hs index a6afc3c..be6a8ec 100644 --- a/version2/src/TypeCheck.hs +++ b/version2/src/TypeCheck.hs @@ -1,7 +1,6 @@ {- pi-forall -} -- | The main routines for type-checking -{-# OPTIONS_GHC -Wno-unrecognised-pragmas #-} {-# HLINT ignore "Use forM_" #-} module TypeCheck (tcModules, inferType, checkType) where @@ -23,213 +22,212 @@ import Unbound.Generics.LocallyNameless qualified as Unbound import Unbound.Generics.LocallyNameless.Internal.Fold qualified as Unbound + + +--------------------------------------------------------------------- + -- | Infer/synthesize the type of a term inferType :: Term -> TcMonad Type -inferType t = tcTerm t Nothing +inferType t = case t of + -- i-var + (Var x) -> do + decl <- Env.lookupTy x + return (declType decl) + + -- i-type + TyType -> return TyType + + -- i-pi + (TyPi tyA bnd) -> do + (x, tyB) <- Unbound.unbind bnd + tcType tyA + Env.extendCtx (mkDecl x tyA) (tcType tyB) + return TyType + + -- i-app + (App t1 t2) -> do + ty1 <- inferType t1 + let ensurePi = Equal.ensurePi + + (tyA,bnd) <- ensurePi ty1 + checkType t2 tyA + return (Unbound.instantiate bnd [t2]) + + -- i-ann + (Ann tm ty) -> do + tcType ty + checkType tm ty + return ty + + -- Practicalities + -- remember the current position in the type checking monad + (Pos p tm) -> + Env.extendSourceLocation p tm $ inferType tm + + -- Extensions to the core language + -- i-unit + TyUnit -> return TyType + LitUnit -> return TyUnit --- | Check that the given term has the expected type -checkType :: Term -> Type -> TcMonad () -checkType tm (Pos _ ty) = checkType tm ty -- ignore source positions/annotations -checkType tm (Ann ty _) = checkType tm ty -checkType tm ty = do - nf <- Equal.whnf ty - void $ tcTerm tm (Just nf) + -- i-bool + TyBool -> return TyType + -- i-true/false + (LitBool b) -> return TyBool + -- i-if + (If t1 t2 t3) -> do + checkType t1 TyBool + ty <- inferType t2 + checkType t3 ty + return ty + -- i-eq + (TyEq a b) -> do + aTy <- inferType a + checkType b aTy + return TyType --- | Make sure that the term is a "type" (i.e. that it has type 'Type') -tcType :: Term -> TcMonad () -tcType tm = void $ checkType tm TyType + -- i-sigma + (TySigma tyA bnd) -> do + (x, tyB) <- Unbound.unbind bnd + tcType tyA + Env.extendCtx (mkDecl x tyA) $ tcType tyB + return TyType ---------------------------------------------------------------------- --- | Combined type checking/inference function --- The second argument is 'Just expectedType' in checking mode and 'Nothing' in inference mode --- In either case, this function returns the type of the term -tcTerm :: Term -> Maybe Type -> TcMonad Type --- i-var -tcTerm t@(Var x) Nothing = do - sig <- Env.lookupTy x - return (sigType sig) --- i-type -tcTerm TyType Nothing = return TyType --- i-pi -tcTerm (TyPi tyA bnd) Nothing = do - (x, tyB) <- Unbound.unbind bnd - tcType tyA - Env.extendCtx (mkSig x tyA) (tcType tyB) - return TyType --- c-lam: check the type of a function -tcTerm (Lam bnd) (Just (TyPi tyA bnd2)) = do - -- unbind the variables in the lambda expression and pi type - (x, body,_,tyB) <- Unbound.unbind2Plus bnd bnd2 - - -- check the type of the body of the lambda expression - Env.extendCtx (mkSig x tyA) (checkType body tyB) - return (TyPi tyA bnd2) -tcTerm (Lam _) (Just nf) = - Env.err [DS "Lambda expression should have a function type, not", DD nf] --- i-app -tcTerm (App t1 t2) Nothing = do - ty1 <- inferType t1 - let ensurePi = Equal.ensurePi - - (tyA,bnd) <- ensurePi ty1 - checkType t2 tyA - return (Unbound.instantiate bnd [t2]) - --- i-ann -tcTerm (Ann tm ty) Nothing = do - tcType ty - checkType tm ty - return ty - --- practicalities --- remember the current position in the type checking monad -tcTerm (Pos p tm) mTy = - Env.extendSourceLocation p tm $ tcTerm tm mTy --- ignore term, just return type annotation -tcTerm TrustMe (Just ty) = return ty - --- i-unit -tcTerm TyUnit Nothing = return TyType -tcTerm LitUnit Nothing = return TyUnit --- i-bool -tcTerm TyBool Nothing = return TyType + -- cannot synthesize the type of the term + tm -> + Env.err [DS "Must have a type for", DD tm] --- i-true/false -tcTerm (LitBool b) Nothing = do - return TyBool +------------------------------------------------------------------------- +-- | Make sure that the term is a "type" (i.e. that it has type 'Type') +tcType :: Term -> TcMonad () +tcType tm = checkType tm TyType --- c-if -tcTerm t@(If t1 t2 t3) mty = do - case mty of - Just ty -> do +------------------------------------------------------------------------- +-- | Check that the given term has the expected type +checkType :: Term -> Type -> TcMonad () +checkType tm ty' = do + ty <- Equal.whnf ty' + case tm of + -- c-lam: check the type of a function + (Lam bnd) -> case ty of + (TyPi tyA bnd2) -> do + -- unbind the variables in the lambda expression and pi type + (x, body,_,tyB) <- Unbound.unbind2Plus bnd bnd2 + + -- check the type of the body of the lambda expression + Env.extendCtx (mkDecl x tyA) (checkType body tyB) + _ -> Env.err [DS "Lambda expression should have a function type, not", DD ty] + + -- Practicalities + (Pos p tm) -> + Env.extendSourceLocation p tm $ checkType tm ty + + TrustMe -> return () + + PrintMe -> do + gamma <- Env.getLocalCtx + Env.warn [DS "Unmet obligation.\nContext:", DD gamma, + DS "\nGoal:", DD ty] + + -- Extensions to the core language + -- c-if + (If t1 t2 t3) -> do checkType t1 TyBool dtrue <- Equal.unify [] t1 (LitBool True) dfalse <- Equal.unify [] t1 (LitBool False) Env.extendCtxs dtrue $ checkType t2 ty - Env.extendCtxs dfalse $ checkType t3 ty - return ty - Nothing -> do - checkType t1 TyBool - ty <- inferType t2 - checkType t3 ty - return ty - - -tcTerm (Let rhs bnd) mty = do - (x, body) <- Unbound.unbind bnd - aty <- inferType rhs - ty <- Env.extendCtxs [mkSig x aty, Def x rhs] $ - tcTerm body mty - case mty of - Just _ -> return ty - Nothing -> return $ Unbound.subst x rhs ty - - - -tcTerm (TyEq a b) Nothing = do - aTy <- inferType a - checkType b aTy - return TyType -tcTerm Refl (Just ty@(TyEq a b)) = do - Equal.equate a b - return ty -tcTerm Refl (Just ty) = - Env.err [DS "Refl annotated with", DD ty] -tcTerm t@(Subst a b) (Just ty) = do - -- infer the type of the proof 'b' - tp <- inferType b - -- make sure that it is an equality between m and n - (m, n) <- Equal.ensureTyEq tp - -- if either side is a variable, add a definition to the context - edecl <- Equal.unify [] m n - -- if proof is a variable, add a definition to the context - pdecl <- Equal.unify [] b Refl - _ <- Env.extendCtxs (edecl ++ pdecl) $ checkType a ty - return ty -tcTerm t@(Contra p) (Just ty) = do - ty' <- inferType p - (a, b) <- Equal.ensureTyEq ty' - a' <- Equal.whnf a - b' <- Equal.whnf b - case (a', b') of + Env.extendCtxs dfalse $ checkType t3 ty + + -- c-let + (Let rhs bnd) -> do + (x, body) <- Unbound.unbind bnd + aty <- inferType rhs + Env.extendCtxs [mkDecl x aty, Def x rhs] $ + checkType body ty + + -- c-refl + Refl -> case ty of + (TyEq a b) -> Equal.equate a b + _ -> Env.err [DS "Refl annotated with", DD ty] + -- c-subst + (Subst a b) -> do + -- infer the type of the proof 'b' + tp <- inferType b + -- make sure that it is an equality between m and n + (m, n) <- Equal.ensureTyEq tp + -- if either side is a variable, add a definition to the context + edecl <- Equal.unify [] m n + -- if proof is a variable, add a definition to the context + pdecl <- Equal.unify [] b Refl + Env.extendCtxs (edecl ++ pdecl) $ checkType a ty + -- c-contra + (Contra p) -> do + ty' <- inferType p + (a, b) <- Equal.ensureTyEq ty' + a' <- Equal.whnf a + b' <- Equal.whnf b + case (a', b') of + + + (LitBool b1, LitBool b2) + | b1 /= b2 -> + return () + (_, _) -> + Env.err + [ DS "I can't tell that", + DD a, + DS "and", + DD b, + DS "are contradictory" + ] + + -- c-prod + (Prod a b) -> do + case ty of + (TySigma tyA bnd) -> do + (x, tyB) <- Unbound.unbind bnd + checkType a tyA + Env.extendCtxs [mkDecl x tyA, Def x a] $ checkType b tyB + _ -> + Env.err + [ DS "Products must have Sigma Type", + DD ty, + DS "found instead" + ] + + + -- c-letpair + (LetPair p bnd) -> do + ((x, y), body) <- Unbound.unbind bnd + pty <- inferType p + pty' <- Equal.whnf pty + case pty' of + TySigma tyA bnd' -> do + let tyB = Unbound.instantiate bnd' [Var x] + decl <- Equal.unify [] p (Prod (Var x) (Var y)) + Env.extendCtxs ([mkDecl x tyA, mkDecl y tyB] ++ decl) $ + checkType body ty + _ -> Env.err [DS "Scrutinee of LetPair must have Sigma type"] + + + + -- c-infer + tm -> do + ty' <- inferType tm + Equal.equate ty' ty - (LitBool b1, LitBool b2) - | b1 /= b2 -> - return ty - (_, _) -> - Env.err - [ DS "I can't tell that", - DD a, - DS "and", - DD b, - DS "are contradictory" - ] - - -tcTerm t@(TySigma tyA bnd) Nothing = do - (x, tyB) <- Unbound.unbind bnd - tcType tyA - Env.extendCtx (mkSig x tyA) $ tcType tyB - return TyType - - -tcTerm t@(Prod a b) (Just ty) = do - case ty of - (TySigma tyA bnd) -> do - (x, tyB) <- Unbound.unbind bnd - checkType a tyA - Env.extendCtxs [mkSig x tyA, Def x a] $ checkType b tyB - return (TySigma tyA (Unbound.bind x tyB)) - _ -> - Env.err - [ DS "Products must have Sigma Type", - DD ty, - DS "found instead" - ] - - -tcTerm t@(LetPair p bnd) (Just ty) = do - ((x, y), body) <- Unbound.unbind bnd - pty <- inferType p - pty' <- Equal.whnf pty - case pty' of - TySigma tyA bnd' -> do - let tyB = Unbound.instantiate bnd' [Var x] - decl <- Equal.unify [] p (Prod (Var x) (Var y)) - Env.extendCtxs ([mkSig x tyA, mkSig y tyB] ++ decl) $ - checkType body ty - return ty - _ -> Env.err [DS "Scrutinee of LetPair must have Sigma type"] - - -tcTerm PrintMe (Just ty) = do - gamma <- Env.getLocalCtx - Env.warn [DS "Unmet obligation.\nContext:", DD gamma, - DS "\nGoal:", DD ty] - return ty - --- c-infer -tcTerm tm (Just ty) = do - ty' <- inferType tm - Equal.equate ty' ty - - return ty' - -tcTerm tm Nothing = - Env.err [DS "Must have a type annotation to check", DD tm] --------------------------------------------------------------------- -- helper functions for type checking -- | Create a Def if either side normalizes to a single variable -def :: Term -> Term -> TcMonad [Decl] +def :: Term -> Term -> TcMonad [Entry] def t1 t2 = do nf1 <- Equal.whnf t1 nf2 <- Equal.whnf t2 @@ -262,11 +260,11 @@ tcModules = foldM tcM [] -- | Typecheck an entire module. tcModule :: - -- | List of already checked modules (including their Decls). + -- | List of already checked modules (including their entries). [Module] -> -- | Module to check. Module -> - -- | The same module with all Decls checked and elaborated. + -- | The same module with all entries checked and elaborated. TcMonad Module tcModule defs m' = do checkedEntries <- @@ -278,23 +276,23 @@ tcModule defs m' = do return $ m' {moduleEntries = checkedEntries} where d `tcE` m = do - -- Extend the Env per the current Decl before checking - -- subsequent Decls. + -- Extend the Env per the current Entry before checking + -- subsequent entries. x <- tcEntry d case x of AddHint hint -> Env.extendHints hint m - -- Add decls to the Decls to be returned + -- Add decls to the entries to be returned AddCtx decls -> (decls ++) <$> Env.extendCtxsGlobal decls m -- Get all of the defs from imported modules (this is the env to check current module in) importedModules = filter (\x -> ModuleImport (moduleName x) `elem` moduleImports m') defs --- | The Env-delta returned when type-checking a top-level Decl. +-- | The Env-delta returned when type-checking a top-level Entry. data HintOrCtx - = AddHint Sig - | AddCtx [Decl] + = AddHint Decl + | AddCtx [Entry] -- | Check each sort of declaration in a module -tcEntry :: Decl -> TcMonad HintOrCtx +tcEntry :: Entry -> TcMonad HintOrCtx tcEntry (Def n term) = do oldDef <- Env.lookupDef n maybe tc die oldDef @@ -304,22 +302,20 @@ tcEntry (Def n term) = do case lkup of Nothing -> do ty <- inferType term - return $ AddCtx [TypeSig (Sig n ty), Def n term] - Just sig -> + return $ AddCtx [TypeDecl (Decl n ty), Def n term] + Just decl -> let handler (Env.Err ps msg) = throwError $ Env.Err ps (msg $$ msg') msg' = disp [ DS "When checking the term", DD term, - DS "against the signature", - DD sig + DS "against the type", + DD decl ] in do - Env.extendCtx (TypeSig sig) $ checkType term (sigType sig) `catchError` handler - if n `elem` fv term - then return $ AddCtx [TypeSig sig, RecDef n term] - else return $ AddCtx [TypeSig sig, Def n term] + Env.extendCtx (TypeDecl decl) $ checkType term (declType decl) `catchError` handler + return $ AddCtx [TypeDecl decl, Def n term] die term' = Env.extendSourceLocation (unPosFlaky term) term $ Env.err @@ -328,34 +324,34 @@ tcEntry (Def n term) = do DS "Previous definition was", DD term' ] -tcEntry (TypeSig sig) = do - duplicateTypeBindingCheck sig - tcType (sigType sig) - return $ AddHint sig +tcEntry (TypeDecl decl) = do + duplicateTypeBindingCheck decl + tcType (declType decl) + return $ AddHint decl + -tcEntry _ = Env.err "unimplemented" -- | Make sure that we don't have the same name twice in the -- environment. (We don't rename top-level module definitions.) -duplicateTypeBindingCheck :: Sig -> TcMonad () -duplicateTypeBindingCheck sig = do +duplicateTypeBindingCheck :: Decl -> TcMonad () +duplicateTypeBindingCheck decl = do -- Look for existing type bindings ... - let n = sigName sig + let n = declName decl l <- Env.lookupTyMaybe n l' <- Env.lookupHint n -- ... we don't care which, if either are Just. case catMaybes [l, l'] of [] -> return () -- We already have a type in the environment so fail. - sig' : _ -> - let p = unPosFlaky $ sigType sig + decl' : _ -> + let p = unPosFlaky $ declType decl msg = - [ DS "Duplicate type signature", - DD sig, + [ DS "Duplicate type declaration", + DD decl, DS "Previous was", - DD sig' + DD decl' ] - in Env.extendSourceLocation p sig $ Env.err msg + in Env.extendSourceLocation p decl $ Env.err msg diff --git a/version3/pi-forall.cabal b/version3/pi-forall.cabal index e7a8c0c..ee29759 100644 --- a/version3/pi-forall.cabal +++ b/version3/pi-forall.cabal @@ -21,7 +21,7 @@ common shared-properties default-language: GHC2021 ghc-options: - -Wall -fno-warn-unused-matches -fno-warn-orphans -fno-warn-unused-top-binds -fno-warn-unused-imports -fno-warn-name-shadowing + -Wall -fno-warn-unused-matches -fno-warn-orphans -fno-warn-unused-top-binds -fno-warn-unused-imports -fno-warn-name-shadowing -Wno-unrecognised-pragmas default-extensions: DefaultSignatures DeriveAnyClass diff --git a/version3/src/Environment.hs b/version3/src/Environment.hs index 7eb9703..0937d36 100644 --- a/version3/src/Environment.hs +++ b/version3/src/Environment.hs @@ -9,7 +9,6 @@ module Environment lookupTy, lookupTyMaybe, lookupDef, - lookupRecDef, lookupHint , getCtx, getLocalCtx, @@ -62,15 +61,15 @@ data SourceLocation where -- | Environment manipulation and accessing functions -- The context 'gamma' is a list data Env = Env - { -- | elaborated term and datatype declarations. - ctx :: [Decl], + { -- | elaborated term and datatype declarations + ctx :: [Entry], -- | how long the tail of "global" variables in the context is -- (used to supress printing those in error messages) globals :: Int, - -- | Type declarations (signatures): it's not safe to + -- | Type declarations: it's not safe to -- put these in the context until a corresponding term -- has been checked. - hints :: [Sig], + hints :: [Decl], -- | what part of the file we are in (for errors/warnings) sourceLocation :: [SourceLocation] } @@ -92,35 +91,35 @@ instance Disp Env where debugDisp e = vcat [debugDisp decl | decl <- ctx e] -- | Find a name's user supplied type signature. -lookupHint :: (MonadReader Env m) => TName -> m (Maybe Sig) +lookupHint :: (MonadReader Env m) => TName -> m (Maybe Decl) lookupHint v = do hints <- asks hints - return $ listToMaybe [ sig | sig <- hints, v == sigName sig] + return $ listToMaybe [ sig | sig <- hints, v == declName sig] -- | Find a name's type in the context. lookupTyMaybe :: (MonadReader Env m) => TName -> - m (Maybe Sig) + m (Maybe Decl) lookupTyMaybe v = do ctx <- asks ctx return $ go ctx where go [] = Nothing - go (TypeSig sig : ctx) - | v == sigName sig = Just sig + go (TypeDecl sig : ctx) + | v == declName sig = Just sig | otherwise = go ctx - go (Demote ep : ctx) = demoteSig ep <$> go ctx + go (Demote ep : ctx) = demoteDecl ep <$> go ctx go (_ : ctx) = go ctx -demoteSig :: Epsilon -> Sig -> Sig -demoteSig ep s = s { sigEp = min ep (sigEp s) } +demoteDecl :: Epsilon -> Decl -> Decl +demoteDecl ep s = s { declEp = min ep (declEp s) } -- | Find the type of a name specified in the context -- throwing an error if the name doesn't exist lookupTy :: - TName -> TcMonad Sig + TName -> TcMonad Decl lookupTy v = do x <- lookupTyMaybe v @@ -143,28 +142,20 @@ lookupDef v = do ctx <- asks ctx return $ listToMaybe [a | Def v' a <- ctx, v == v'] -lookupRecDef :: - (MonadReader Env m) => - TName -> - m (Maybe Term) -lookupRecDef v = do - ctx <- asks ctx - return $ listToMaybe [a | RecDef v' a <- ctx, v == v'] - -- | Extend the context with a new binding -extendCtx :: (MonadReader Env m) => Decl -> m a -> m a +extendCtx :: (MonadReader Env m) => Entry -> m a -> m a extendCtx d = local (\m@Env{ctx = cs} -> m {ctx = d : cs}) -- | Extend the context with a list of bindings -extendCtxs :: (MonadReader Env m) => [Decl] -> m a -> m a +extendCtxs :: (MonadReader Env m) => [Entry] -> m a -> m a extendCtxs ds = local (\m@Env {ctx = cs} -> m {ctx = ds ++ cs}) -- | Extend the context with a list of bindings, marking them as "global" -extendCtxsGlobal :: (MonadReader Env m) => [Decl] -> m a -> m a +extendCtxsGlobal :: (MonadReader Env m) => [Entry] -> m a -> m a extendCtxsGlobal ds = local ( \m@Env {ctx = cs} -> @@ -186,11 +177,11 @@ extendCtxMods :: (MonadReader Env m) => [Module] -> m a -> m a extendCtxMods mods k = foldr extendCtxMod k mods -- | Get the complete current context -getCtx :: MonadReader Env m => m [Decl] +getCtx :: MonadReader Env m => m [Entry] getCtx = asks ctx -- | Get the prefix of the context that corresponds to local variables. -getLocalCtx :: MonadReader Env m => m [Decl] +getLocalCtx :: MonadReader Env m => m [Entry] getLocalCtx = do g <- asks ctx glen <- asks globals @@ -206,7 +197,7 @@ getSourceLocation :: MonadReader Env m => m [SourceLocation] getSourceLocation = asks sourceLocation -- | Add a type hint -extendHints :: (MonadReader Env m) => Sig -> m a -> m a +extendHints :: (MonadReader Env m) => Decl -> m a -> m a extendHints h = local (\m@Env {hints = hs} -> m {hints = h : hs}) -- | An error that should be reported to the user diff --git a/version3/src/Equal.hs b/version3/src/Equal.hs index 81a98af..e33092e 100644 --- a/version3/src/Equal.hs +++ b/version3/src/Equal.hs @@ -151,11 +151,7 @@ whnf (Var x) = do maybeDef <- Env.lookupDef x case maybeDef of (Just d) -> whnf d - _ -> do - maybeRecDef <- Env.lookupRecDef x - case maybeRecDef of - (Just d) -> whnf d - _ -> return (Var x) + _ -> return (Var x) whnf (App t1 t2) = do nf <- whnf t1 @@ -198,7 +194,7 @@ whnf tm = return tm -- | 'Unify' the two terms, producing a list of Defs -- If there is an obvious mismatch, this function produces an error -- If either term is "ambiguous" just ignore. -unify :: [TName] -> Term -> Term -> TcMonad [Decl] +unify :: [TName] -> Term -> Term -> TcMonad [Entry] unify ns tx ty = do txnf <- whnf tx tynf <- whnf ty diff --git a/version3/src/Parser.hs b/version3/src/Parser.hs index 122f99a..55b32a0 100644 --- a/version3/src/Parser.hs +++ b/version3/src/Parser.hs @@ -3,7 +3,7 @@ -- | A parsec-based parser for the concrete syntax module Parser ( - parseModuleFile, + parseModuleFile, parseModuleImports, parseExpr, expr, @@ -19,7 +19,7 @@ import qualified Unbound.Generics.LocallyNameless as Unbound import Text.Parsec hiding (State,Empty) import Text.Parsec.Expr(Operator(..),Assoc(..),buildExpressionParser) -import qualified LayoutToken as Token +import qualified LayoutToken as Token import Control.Monad.State.Lazy hiding (join) import Control.Monad.Except ( MonadError(throwError) ) @@ -82,13 +82,13 @@ Optional components in this BNF are marked with < > A -> B - Get parsed as (x:A) -> B, with an internal name for x + Get parsed as (_:A) -> B, with a wildcard name for the binder - Nondependent product types, like: A * B - Get parsed as { x:A | B }, with an internal name for x + Get parsed as { _:A | B }, with a wildcard name for the binder - You can collapse lambdas, like: @@ -104,6 +104,12 @@ Optional components in this BNF are marked with < > -} + +-- | Default name (for parsing 'A -> B' as '(_:A) -> B') +wildcardName :: TName +wildcardName = Unbound.string2Name "_" + + liftError :: (MonadError e m) => Either e a -> m a liftError (Left e) = throwError e liftError (Right a) = return a @@ -120,13 +126,13 @@ parseModuleFile name = do parseModuleImports :: (MonadError ParseError m, MonadIO m) => String -> m Module parseModuleImports name = do contents <- liftIO $ readFile name - liftError $ Unbound.runFreshM $ + liftError $ Unbound.runFreshM $ (runParserT (do { whiteSpace; moduleImports }) [] name contents) -- | Test an 'LParser' on a String. testParser :: LParser t -> String -> Either ParseError t -testParser parser str = Unbound.runFreshM $ +testParser parser str = Unbound.runFreshM $ runParserT (do { whiteSpace; v <- parser; eof; return v}) [] "" str @@ -174,10 +180,10 @@ piforallStyle = Token.LanguageDef ,"axiom" ,"TRUSTME" ,"PRINTME" - ,"ord" - ,"Bool", "True", "False" + ,"ord" + ,"Bool", "True", "False" ,"if","then","else" - ,"Unit", "()" + ,"Unit", "()" ] , Token.reservedOpNames = ["!","?","\\",":",".",",","<", "=", "+", "-", "*", "^", "()", "_","|","{", "}"] @@ -194,9 +200,9 @@ whiteSpace = Token.whiteSpace tokenizer variable :: LParser TName variable = - do i <- identifier + do i <- identifier return $ Unbound.string2Name i - + @@ -205,7 +211,7 @@ colon, dot, comma :: LParser () colon = Token.colon tokenizer >> return () dot = Token.dot tokenizer >> return () comma = Token.comma tokenizer >> return () - + reserved,reservedOp :: String -> LParser () reserved = Token.reserved tokenizer reservedOp = Token.reservedOp tokenizer @@ -240,20 +246,20 @@ importDef = do reserved "import" >> (ModuleImport <$> importName) where importName = identifier - + --- --- Top level declarations --- -decl,sigDef,valDef :: LParser Decl -decl = sigDef <|> valDef +decl,declDef,valDef :: LParser Entry +decl = declDef <|> valDef + - -sigDef = do +declDef = do n <- try (variable >>= \v -> colon >> return v) ty <- expr - return (mkSig n ty) + return (mkDecl n ty) valDef = do n <- try (do {n <- variable; reservedOp "="; return n}) @@ -276,13 +282,13 @@ printme = reserved "PRINTME" *> return (PrintMe ) refl :: LParser Term refl = do reserved "Refl" - return $ Refl + return $ Refl -- Expressions expr,term,factor :: LParser Term - + -- expr is the toplevel expression grammar expr = do p <- getPosition @@ -291,18 +297,18 @@ expr = do [ifix AssocLeft "=" TyEq], [ifixM AssocRight "->" mkArrowType], [ifixM AssocRight "*" mkTupleType] - ] + ] ifix assoc op f = Infix (reservedOp op >> return f) assoc ifixM assoc op f = Infix (reservedOp op >> f) assoc - mkArrowType = + mkArrowType = do n <- Unbound.fresh wildcardName - return $ \tyA tyB -> + return $ \tyA tyB -> TyPi Rel tyA (Unbound.bind n tyB) - mkTupleType = + mkTupleType = do n <- Unbound.fresh wildcardName - return $ \tyA tyB -> + return $ \tyA tyB -> TySigma tyA (Unbound.bind n tyB) - + -- A "term" is either a function application or a constructor -- application. Breaking it out as a seperate category both -- eliminates left-recursion in ( := ) and @@ -310,19 +316,19 @@ expr = do term = funapp - + funapp :: LParser Term -funapp = do +funapp = do f <- factor foldl' app f <$> many bfactor where - bfactor = ((,Irr) <$> brackets expr) + bfactor = ((,Irr) <$> brackets expr) <|> ((,Rel) <$> factor) app e1 (e2,ep) = App e1 (Arg ep e2) -factor = choice [ Var <$> variable "a variable" +factor = choice [ Var <$> variable "a variable" , typen "Type" , lambda "a lambda" , try letPairExp "a let pair" @@ -335,16 +341,16 @@ factor = choice [ Var <$> variable "a variable" , printme "PRINTME" , impProd "an implicit function type" - , bconst "a constant" - , ifExpr "an if expression" - , sigmaTy "a sigma type" - + , bconst "a constant" + , ifExpr "an if expression" + , sigmaTy "a sigma type" + , expProdOrAnnotOrParens "an explicit function type or annotated expression" ] impOrExpVar :: LParser (TName, Epsilon) -impOrExpVar = try ((,Irr) <$> (brackets variable)) +impOrExpVar = try ((,Irr) <$> (brackets variable)) <|> (,Rel) <$> variable @@ -361,12 +367,12 @@ lambda = do reservedOp "\\" binds <- many1 impOrExpVar dot body <- expr - return $ foldr lam body binds + return $ foldr lam body binds where - lam (x, ep) m = Lam ep (Unbound.bind x m) - + lam (x, ep) m = Lam ep (Unbound.bind x m) + + - bconst :: LParser Term @@ -378,7 +384,7 @@ bconst = choice [reserved "Bool" >> return TyBool, ifExpr :: LParser Term -ifExpr = +ifExpr = do reserved "if" a <- expr reserved "then" @@ -386,7 +392,7 @@ ifExpr = reserved "else" c <- expr return (If a b c ) - + -- letExpr :: LParser Term @@ -418,10 +424,10 @@ letPairExp = do -- These have the syntax [x:a] -> b or [a] -> b . impProd :: LParser Term impProd = - do (x,tyA) <- brackets + do (x,tyA) <- brackets (try ((,) <$> variable <*> (colon >> expr)) <|> ((,) <$> Unbound.fresh wildcardName <*> expr)) - reservedOp "->" + reservedOp "->" tyB <- expr return $ TyPi Irr tyA (Unbound.bind x tyB) @@ -462,13 +468,13 @@ expProdOrAnnotOrParens = (do b <- afterBinder return $ TyPi Rel a (Unbound.bind x b)) Colon a b -> return $ Ann a b - - Comma a b -> + + Comma a b -> return $ Prod a b Nope a -> return a - - + + -- subst e0 by e1 substExpr :: LParser Term @@ -477,16 +483,16 @@ substExpr = do a <- expr reserved "by" b <- expr - return $ Subst a b + return $ Subst a b contra :: LParser Term contra = do reserved "contra" witness <- expr - return $ Contra witness + return $ Contra witness -sigmaTy :: LParser Term +sigmaTy :: LParser Term sigmaTy = do reservedOp "{" x <- variable @@ -496,5 +502,5 @@ sigmaTy = do b <- expr reservedOp "}" return (TySigma a (Unbound.bind x b)) - - + + diff --git a/version3/src/PrettyPrint.hs b/version3/src/PrettyPrint.hs index 60c1ea2..c130026 100644 --- a/version3/src/PrettyPrint.hs +++ b/version3/src/PrettyPrint.hs @@ -120,11 +120,11 @@ instance Disp Module instance Disp ModuleImport -instance Disp Decl +instance Disp Entry -instance Disp [Decl] +instance Disp [Entry] -instance Disp Sig +instance Disp Decl instance Disp Arg @@ -152,24 +152,23 @@ instance Display Module where instance Display ModuleImport where display (ModuleImport i) = pure $ PP.text "import" <+> disp i -instance Display [Decl] where +instance Display [Entry] where display ds = do dd <- mapM display ds pure $ PP.vcat dd -instance Display Sig where - display sig = do - dn <- display (sigName sig) - dt <- display (sigType sig) +instance Display Decl where + display decl = do + dn <- display (declName decl) + dt <- display (declType decl) pure $ dn <+> PP.text ":" <+> dt -instance Display Decl where +instance Display Entry where display (Def n term) = do dn <- display n dt <- display term pure $ dn <+> PP.text "=" <+> dt - display (RecDef n f) = display (Def n f) - display (TypeSig sig) = display sig + display (TypeDecl decl) = display decl display (Demote ep) = return mempty diff --git a/version3/src/Syntax.hs b/version3/src/Syntax.hs index e1f50cd..206d461 100644 --- a/version3/src/Syntax.hs +++ b/version3/src/Syntax.hs @@ -25,11 +25,8 @@ import Data.Function (on) -- and alpha-equality function. The abstract type `Name` from -- this library is indexed by the AST type that this variable -- is a name for. -type TName = Unbound.Name Term - --- | module names -type ModuleName = String +type TName = Unbound.Name Term ----------------------------------------- @@ -121,12 +118,15 @@ data Epsilon ----------------------------------------- +-- | module names +type ModuleName = String + -- | A Module has a name, a list of imports, a list of declarations, -- and a set of constructor names (which affect parsing). data Module = Module { moduleName :: ModuleName, moduleImports :: [ModuleImport], - moduleEntries :: [Decl] + moduleEntries :: [Entry] } deriving (Show, Generic, Typeable, Unbound.Alpha) @@ -135,37 +135,40 @@ newtype ModuleImport = ModuleImport ModuleName deriving (Show, Eq, Generic, Typeable) deriving anyclass (Unbound.Alpha) --- | A type declaration (or type signature) -data Sig = Sig {sigName :: TName , sigEp :: Epsilon , sigType :: Type} +-- | A type declaration (or type declnature) +data Decl = Decl {declName :: TName , declEp :: Epsilon , declType :: Type} deriving (Show, Generic, Typeable, Unbound.Alpha, Unbound.Subst Term) -- | Declare the type of a term -mkSig :: TName -> Type -> Decl -mkSig n ty = TypeSig (Sig n Rel ty) - --- | Declarations are the components of modules -data Decl - = -- | Declaration for the type of a term - TypeSig Sig - | -- | The definition of a particular name, must +mkDecl :: TName -> Type -> Entry +mkDecl n ty = TypeDecl (Decl n Rel ty) + +-- | Entries are the components of modules +data Entry + = -- | Declaration for the type of a term 'x : A' + TypeDecl Decl + | -- | The definition of a particular name, must 'x = a' -- already have a type declaration in scope Def TName Term - | -- | A potentially (recursive) definition of - -- a particular name, must be declared - RecDef TName Term -- | Adjust the context for relevance checking | Demote Epsilon deriving (Show, Generic, Typeable) deriving anyclass (Unbound.Alpha, Unbound.Subst Term) --- * Auxiliary functions on syntax --- | Default name for '_' occurring in patterns -wildcardName :: TName -wildcardName = Unbound.string2Name "_" +----------------------------------------- +-- * Auxiliary functions on syntax +----------------------------------------- + + +-- | Remove source positions and type annotations from the top level of a term +strip :: Term -> Term +strip (Pos _ tm) = strip tm +strip (Ann tm _) = strip tm +strip tm = tm -- | Partial inverse of Pos unPos :: Term -> Maybe SourcePos @@ -177,18 +180,41 @@ unPosFlaky :: Term -> SourcePos unPosFlaky t = fromMaybe (newPos "unknown location" 0 0) (unPos t) ------------------ + +----------------------------------------- +-- * Unbound library +----------------------------------------- -- We use the unbound-generics library to mark the binding occurrences of -- variables in the syntax. That allows us to automatically derive -- functions for alpha-equivalence, free variables and substitution -- using generic programming. +-- | Determine when two terms are alpha-equivalent (see below) +aeq :: Term -> Term -> Bool +aeq = Unbound.aeq + +-- | Calculate the free variables of a term +fv :: Term -> [Unbound.Name Term] +fv = Unbound.toListOf Unbound.fv + +-- | subst x b a means to replace x with b in a +-- i.e. a [ b / x ] +subst :: TName -> Term -> Term -> Term +subst = Unbound.subst + +-- | in a binder "x.a" replace x with b +instantiate :: Unbound.Bind TName Term -> Term -> Term +instantiate bnd a = Unbound.instantiate bnd [a] + +-- | in a binder "x.a" replace x with a fresh name +unbind :: (Unbound.Fresh m) => Unbound.Bind TName Term -> m (TName, Term) +unbind = Unbound.unbind ------------------ -- * Alpha equivalence and free variables --- Among other things, the Alpha class enables the following +-- The Unbound library's Alpha class enables the following -- functions: -- -- Compare terms for alpha equivalence -- aeq :: Alpha a => a -> a -> Bool @@ -198,23 +224,23 @@ unPosFlaky t = fromMaybe (newPos "unknown location" 0 0) (unPos t) -- unbind :: (Alpha p, Alpha t, Fresh m) => Bind p t -> m (p, t) -- For Terms, we'd like Alpha equivalence to ignore --- source positions and type annotations. --- We can add these special cases to the definition of `aeq'` --- and then defer all other cases to the generic version of --- the function (Unbound.gaeq). +-- source positions and type annotations. So we make sure to +-- remove them before calling the generic operation. instance Unbound.Alpha Term where - aeq' ctx (Ann a _) b = Unbound.aeq' ctx a b - aeq' ctx a (Ann b _) = Unbound.aeq' ctx a b - aeq' ctx (Pos _ a) b = Unbound.aeq' ctx a b - aeq' ctx a (Pos _ b) = Unbound.aeq' ctx a b - aeq' ctx a b = (Unbound.gaeq ctx `on` from) a b + aeq' :: Unbound.AlphaCtx -> Term -> Term -> Bool + aeq' ctx a b = (Unbound.gaeq ctx `on` from) (strip a) (strip b) + -- For example, all occurrences of annotations and source positions -- are ignored by this definition. --- >>> Unbound.aeq (Pos internalPos (Ann TyBool Type)) TyBool --- True +-- '(Bool : Type)' is alpha-equivalent to 'Bool' +-- >>> aeq (Ann TyBool TyType) TyBool + +-- '(Bool, Bool:Type)' is alpha-equivalent to (Bool, Bool) +-- >>> aeq (Prod TyBool (Ann TyBool TyType)) (Prod TyBool TyBool) + -- At the same time, the generic operation equates terms that differ only -- in the names of bound variables. @@ -235,7 +261,7 @@ idx = Lam Rel (Unbound.bind xName (Var xName)) idy :: Term idy = Lam Rel (Unbound.bind yName (Var yName)) --- >>> Unbound.aeq idx idy +-- >>> aeq idx idy -- True @@ -264,14 +290,6 @@ pi2 :: Term pi2 = TyPi Rel TyBool (Unbound.bind yName (Var yName)) -- >>> Unbound.aeq (Unbound.subst xName TyBool pi1) pi2 --- True --- - ---------------- --- | Bridge function to calculate the free variables of a term - -fv :: Term -> [Unbound.Name Term] -fv = Unbound.toListOf Unbound.fv ----------------- @@ -295,10 +313,11 @@ instance Unbound.Alpha SourcePos where acompare' _ _ _ = EQ -- Substitutions ignore source positions -instance Unbound.Subst b SourcePos where subst _ _ = id; substs _ = id; substBvs _ _ = id +instance Unbound.Subst b SourcePos where + subst _ _ = id + substs _ = id + substBvs _ _ = id + --- Internally generated source positions -internalPos :: SourcePos -internalPos = initialPos "internal" diff --git a/version3/src/TypeCheck.hs b/version3/src/TypeCheck.hs index 0b35105..25cd666 100644 --- a/version3/src/TypeCheck.hs +++ b/version3/src/TypeCheck.hs @@ -1,7 +1,6 @@ {- pi-forall -} -- | The main routines for type-checking -{-# OPTIONS_GHC -Wno-unrecognised-pragmas #-} {-# HLINT ignore "Use forM_" #-} module TypeCheck (tcModules, inferType, checkType) where @@ -23,222 +22,221 @@ import Unbound.Generics.LocallyNameless qualified as Unbound import Unbound.Generics.LocallyNameless.Internal.Fold qualified as Unbound + + +--------------------------------------------------------------------- + -- | Infer/synthesize the type of a term inferType :: Term -> TcMonad Type -inferType t = tcTerm t Nothing +inferType t = case t of + -- i-var + (Var x) -> do + decl <- Env.lookupTy x -- make sure the variable is accessible + Env.checkStage (declEp decl) + return (declType decl) + + -- i-type + TyType -> return TyType + + -- i-pi + (TyPi ep tyA bnd) -> do + (x, tyB) <- Unbound.unbind bnd + tcType tyA + Env.extendCtx (TypeDecl (Decl x ep tyA)) (tcType tyB) + return TyType + + -- i-app + (App t1 t2) -> do + ty1 <- inferType t1 + let ensurePi = Equal.ensurePi + + (ep1, tyA, bnd) <- ensurePi ty1 + unless (ep1 == argEp t2) $ Env.err + [DS "In application, expected", DD ep1, DS "argument but found", + DD t2, DS "instead." ] + -- if the argument is Irrelevant, resurrect the context + (if ep1 == Irr then Env.extendCtx (Demote Rel) else id) $ + checkType (unArg t2) tyA + return (Unbound.instantiate bnd [unArg t2]) + --- | Check that the given term has the expected type -checkType :: Term -> Type -> TcMonad () -checkType tm (Pos _ ty) = checkType tm ty -- ignore source positions/annotations -checkType tm (Ann ty _) = checkType tm ty -checkType tm ty = do - nf <- Equal.whnf ty - void $ tcTerm tm (Just nf) + -- i-ann + (Ann tm ty) -> do + tcType ty + checkType tm ty + return ty + + -- Practicalities + -- remember the current position in the type checking monad + (Pos p tm) -> + Env.extendSourceLocation p tm $ inferType tm + + -- Extensions to the core language + -- i-unit + TyUnit -> return TyType + LitUnit -> return TyUnit + -- i-bool + TyBool -> return TyType + -- i-true/false + (LitBool b) -> return TyBool --- | Make sure that the term is a "type" (i.e. that it has type 'Type') -tcType :: Term -> TcMonad () -tcType tm = void $ Env.withStage Irr $ checkType tm TyType + -- i-if + (If t1 t2 t3) -> do + checkType t1 TyBool + ty <- inferType t2 + checkType t3 ty + return ty + -- i-eq + (TyEq a b) -> do + aTy <- inferType a + checkType b aTy + return TyType ---------------------------------------------------------------------- + -- i-sigma + (TySigma tyA bnd) -> do + (x, tyB) <- Unbound.unbind bnd + tcType tyA + Env.extendCtx (mkDecl x tyA) $ tcType tyB + return TyType --- | Combined type checking/inference function --- The second argument is 'Just expectedType' in checking mode and 'Nothing' in inference mode --- In either case, this function returns the type of the term -tcTerm :: Term -> Maybe Type -> TcMonad Type --- i-var -tcTerm t@(Var x) Nothing = do - sig <- Env.lookupTy x -- make sure the variable is accessible - Env.checkStage (sigEp sig) - return (sigType sig) --- i-type -tcTerm TyType Nothing = return TyType --- i-pi -tcTerm (TyPi ep tyA bnd) Nothing = do - (x, tyB) <- Unbound.unbind bnd - tcType tyA - Env.extendCtx (TypeSig (Sig x ep tyA)) (tcType tyB) - return TyType --- c-lam: check the type of a function -tcTerm (Lam ep1 bnd) (Just (TyPi ep2 tyA bnd2)) = do - -- unbind the variables in the lambda expression and pi type - (x, body,_,tyB) <- Unbound.unbind2Plus bnd bnd2 --- epsilons should match up - unless (ep1 == ep2) $ Env.err [DS "In function definition, expected", DD ep2, DS "parameter", DD x, - DS "but found", DD ep1, DS "instead."] - -- check the type of the body of the lambda expression - Env.extendCtx (TypeSig (Sig x ep1 tyA)) (checkType body tyB) - return (TyPi ep1 tyA bnd2) -tcTerm (Lam _ _) (Just nf) = - Env.err [DS "Lambda expression should have a function type, not", DD nf] --- i-app -tcTerm (App t1 t2) Nothing = do - ty1 <- inferType t1 - let ensurePi = Equal.ensurePi - - (ep1, tyA, bnd) <- ensurePi ty1 - unless (ep1 == argEp t2) $ Env.err - [DS "In application, expected", DD ep1, DS "argument but found", - DD t2, DS "instead." ] - -- if the argument is Irrelevant, resurrect the context - (if ep1 == Irr then Env.extendCtx (Demote Rel) else id) $ - checkType (unArg t2) tyA - return (Unbound.instantiate bnd [unArg t2]) - --- i-ann -tcTerm (Ann tm ty) Nothing = do - tcType ty - checkType tm ty - return ty - --- practicalities --- remember the current position in the type checking monad -tcTerm (Pos p tm) mTy = - Env.extendSourceLocation p tm $ tcTerm tm mTy --- ignore term, just return type annotation -tcTerm TrustMe (Just ty) = return ty - --- i-unit -tcTerm TyUnit Nothing = return TyType -tcTerm LitUnit Nothing = return TyUnit --- i-bool -tcTerm TyBool Nothing = return TyType + -- cannot synthesize the type of the term + tm -> + Env.err [DS "Must have a type for", DD tm] --- i-true/false -tcTerm (LitBool b) Nothing = do - return TyBool +------------------------------------------------------------------------- +-- | Make sure that the term is a "type" (i.e. that it has type 'Type') +tcType :: Term -> TcMonad () +tcType tm = Env.withStage Irr $ checkType tm TyType --- c-if -tcTerm t@(If t1 t2 t3) mty = do - case mty of - Just ty -> do +------------------------------------------------------------------------- +-- | Check that the given term has the expected type +checkType :: Term -> Type -> TcMonad () +checkType tm ty' = do + ty <- Equal.whnf ty' + case tm of + -- c-lam: check the type of a function + (Lam ep1 bnd) -> case ty of + (TyPi ep2 tyA bnd2) -> do + -- unbind the variables in the lambda expression and pi type + (x, body,_,tyB) <- Unbound.unbind2Plus bnd bnd2 +-- epsilons should match up + unless (ep1 == ep2) $ Env.err [DS "In function definition, expected", DD ep2, DS "parameter", DD x, + DS "but found", DD ep1, DS "instead."] + -- check the type of the body of the lambda expression + Env.extendCtx (TypeDecl (Decl x ep1 tyA)) (checkType body tyB) + _ -> Env.err [DS "Lambda expression should have a function type, not", DD ty] + + -- Practicalities + (Pos p tm) -> + Env.extendSourceLocation p tm $ checkType tm ty + + TrustMe -> return () + + PrintMe -> do + gamma <- Env.getLocalCtx + Env.warn [DS "Unmet obligation.\nContext:", DD gamma, + DS "\nGoal:", DD ty] + + -- Extensions to the core language + -- c-if + (If t1 t2 t3) -> do checkType t1 TyBool dtrue <- Equal.unify [] t1 (LitBool True) dfalse <- Equal.unify [] t1 (LitBool False) Env.extendCtxs dtrue $ checkType t2 ty - Env.extendCtxs dfalse $ checkType t3 ty - return ty - Nothing -> do - checkType t1 TyBool - ty <- inferType t2 - checkType t3 ty - return ty - - -tcTerm (Let rhs bnd) mty = do - (x, body) <- Unbound.unbind bnd - aty <- inferType rhs - ty <- Env.extendCtxs [mkSig x aty, Def x rhs] $ - tcTerm body mty - case mty of - Just _ -> return ty - Nothing -> return $ Unbound.subst x rhs ty - - - -tcTerm (TyEq a b) Nothing = do - aTy <- inferType a - checkType b aTy - return TyType -tcTerm Refl (Just ty@(TyEq a b)) = do - Equal.equate a b - return ty -tcTerm Refl (Just ty) = - Env.err [DS "Refl annotated with", DD ty] -tcTerm t@(Subst a b) (Just ty) = do - -- infer the type of the proof 'b' - tp <- inferType b - -- make sure that it is an equality between m and n - (m, n) <- Equal.ensureTyEq tp - -- if either side is a variable, add a definition to the context - edecl <- Equal.unify [] m n - -- if proof is a variable, add a definition to the context - pdecl <- Equal.unify [] b Refl - _ <- Env.extendCtxs (edecl ++ pdecl) $ checkType a ty - return ty -tcTerm t@(Contra p) (Just ty) = do - ty' <- inferType p - (a, b) <- Equal.ensureTyEq ty' - a' <- Equal.whnf a - b' <- Equal.whnf b - case (a', b') of + Env.extendCtxs dfalse $ checkType t3 ty + + -- c-let + (Let rhs bnd) -> do + (x, body) <- Unbound.unbind bnd + aty <- inferType rhs + Env.extendCtxs [mkDecl x aty, Def x rhs] $ + checkType body ty + + -- c-refl + Refl -> case ty of + (TyEq a b) -> Equal.equate a b + _ -> Env.err [DS "Refl annotated with", DD ty] + -- c-subst + (Subst a b) -> do + -- infer the type of the proof 'b' + tp <- inferType b + -- make sure that it is an equality between m and n + (m, n) <- Equal.ensureTyEq tp + -- if either side is a variable, add a definition to the context + edecl <- Equal.unify [] m n + -- if proof is a variable, add a definition to the context + pdecl <- Equal.unify [] b Refl + Env.extendCtxs (edecl ++ pdecl) $ checkType a ty + -- c-contra + (Contra p) -> do + ty' <- inferType p + (a, b) <- Equal.ensureTyEq ty' + a' <- Equal.whnf a + b' <- Equal.whnf b + case (a', b') of + + + (LitBool b1, LitBool b2) + | b1 /= b2 -> + return () + (_, _) -> + Env.err + [ DS "I can't tell that", + DD a, + DS "and", + DD b, + DS "are contradictory" + ] + + -- c-prod + (Prod a b) -> do + case ty of + (TySigma tyA bnd) -> do + (x, tyB) <- Unbound.unbind bnd + checkType a tyA + Env.extendCtxs [mkDecl x tyA, Def x a] $ checkType b tyB + _ -> + Env.err + [ DS "Products must have Sigma Type", + DD ty, + DS "found instead" + ] + + + -- c-letpair + (LetPair p bnd) -> do + ((x, y), body) <- Unbound.unbind bnd + pty <- inferType p + pty' <- Equal.whnf pty + case pty' of + TySigma tyA bnd' -> do + let tyB = Unbound.instantiate bnd' [Var x] + decl <- Equal.unify [] p (Prod (Var x) (Var y)) + Env.extendCtxs ([mkDecl x tyA, mkDecl y tyB] ++ decl) $ + checkType body ty + _ -> Env.err [DS "Scrutinee of LetPair must have Sigma type"] + + + + -- c-infer + tm -> do + ty' <- inferType tm + Equal.equate ty' ty - (LitBool b1, LitBool b2) - | b1 /= b2 -> - return ty - (_, _) -> - Env.err - [ DS "I can't tell that", - DD a, - DS "and", - DD b, - DS "are contradictory" - ] - - -tcTerm t@(TySigma tyA bnd) Nothing = do - (x, tyB) <- Unbound.unbind bnd - tcType tyA - Env.extendCtx (mkSig x tyA) $ tcType tyB - return TyType - - -tcTerm t@(Prod a b) (Just ty) = do - case ty of - (TySigma tyA bnd) -> do - (x, tyB) <- Unbound.unbind bnd - checkType a tyA - Env.extendCtxs [mkSig x tyA, Def x a] $ checkType b tyB - return (TySigma tyA (Unbound.bind x tyB)) - _ -> - Env.err - [ DS "Products must have Sigma Type", - DD ty, - DS "found instead" - ] - - -tcTerm t@(LetPair p bnd) (Just ty) = do - ((x, y), body) <- Unbound.unbind bnd - pty <- inferType p - pty' <- Equal.whnf pty - case pty' of - TySigma tyA bnd' -> do - let tyB = Unbound.instantiate bnd' [Var x] - decl <- Equal.unify [] p (Prod (Var x) (Var y)) - Env.extendCtxs ([mkSig x tyA, mkSig y tyB] ++ decl) $ - checkType body ty - return ty - _ -> Env.err [DS "Scrutinee of LetPair must have Sigma type"] - - -tcTerm PrintMe (Just ty) = do - gamma <- Env.getLocalCtx - Env.warn [DS "Unmet obligation.\nContext:", DD gamma, - DS "\nGoal:", DD ty] - return ty - --- c-infer -tcTerm tm (Just ty) = do - ty' <- inferType tm - Equal.equate ty' ty - - return ty' - -tcTerm tm Nothing = - Env.err [DS "Must have a type annotation to check", DD tm] --------------------------------------------------------------------- -- helper functions for type checking -- | Create a Def if either side normalizes to a single variable -def :: Term -> Term -> TcMonad [Decl] +def :: Term -> Term -> TcMonad [Entry] def t1 t2 = do nf1 <- Equal.whnf t1 nf2 <- Equal.whnf t2 @@ -271,11 +269,11 @@ tcModules = foldM tcM [] -- | Typecheck an entire module. tcModule :: - -- | List of already checked modules (including their Decls). + -- | List of already checked modules (including their entries). [Module] -> -- | Module to check. Module -> - -- | The same module with all Decls checked and elaborated. + -- | The same module with all entries checked and elaborated. TcMonad Module tcModule defs m' = do checkedEntries <- @@ -287,23 +285,23 @@ tcModule defs m' = do return $ m' {moduleEntries = checkedEntries} where d `tcE` m = do - -- Extend the Env per the current Decl before checking - -- subsequent Decls. + -- Extend the Env per the current Entry before checking + -- subsequent entries. x <- tcEntry d case x of AddHint hint -> Env.extendHints hint m - -- Add decls to the Decls to be returned + -- Add decls to the entries to be returned AddCtx decls -> (decls ++) <$> Env.extendCtxsGlobal decls m -- Get all of the defs from imported modules (this is the env to check current module in) importedModules = filter (\x -> ModuleImport (moduleName x) `elem` moduleImports m') defs --- | The Env-delta returned when type-checking a top-level Decl. +-- | The Env-delta returned when type-checking a top-level Entry. data HintOrCtx - = AddHint Sig - | AddCtx [Decl] + = AddHint Decl + | AddCtx [Entry] -- | Check each sort of declaration in a module -tcEntry :: Decl -> TcMonad HintOrCtx +tcEntry :: Entry -> TcMonad HintOrCtx tcEntry (Def n term) = do oldDef <- Env.lookupDef n maybe tc die oldDef @@ -313,22 +311,20 @@ tcEntry (Def n term) = do case lkup of Nothing -> do ty <- inferType term - return $ AddCtx [TypeSig (Sig n Rel ty), Def n term] - Just sig -> + return $ AddCtx [TypeDecl (Decl n Rel ty), Def n term] + Just decl -> let handler (Env.Err ps msg) = throwError $ Env.Err ps (msg $$ msg') msg' = disp [ DS "When checking the term", DD term, - DS "against the signature", - DD sig + DS "against the type", + DD decl ] in do - Env.extendCtx (TypeSig sig) $ checkType term (sigType sig) `catchError` handler - if n `elem` fv term - then return $ AddCtx [TypeSig sig, RecDef n term] - else return $ AddCtx [TypeSig sig, Def n term] + Env.extendCtx (TypeDecl decl) $ checkType term (declType decl) `catchError` handler + return $ AddCtx [TypeDecl decl, Def n term] die term' = Env.extendSourceLocation (unPosFlaky term) term $ Env.err @@ -337,35 +333,35 @@ tcEntry (Def n term) = do DS "Previous definition was", DD term' ] -tcEntry (TypeSig sig) = do - duplicateTypeBindingCheck sig - tcType (sigType sig) - return $ AddHint sig +tcEntry (TypeDecl decl) = do + duplicateTypeBindingCheck decl + tcType (declType decl) + return $ AddHint decl tcEntry (Demote ep) = return (AddCtx [Demote ep]) -tcEntry _ = Env.err "unimplemented" + -- | Make sure that we don't have the same name twice in the -- environment. (We don't rename top-level module definitions.) -duplicateTypeBindingCheck :: Sig -> TcMonad () -duplicateTypeBindingCheck sig = do +duplicateTypeBindingCheck :: Decl -> TcMonad () +duplicateTypeBindingCheck decl = do -- Look for existing type bindings ... - let n = sigName sig + let n = declName decl l <- Env.lookupTyMaybe n l' <- Env.lookupHint n -- ... we don't care which, if either are Just. case catMaybes [l, l'] of [] -> return () -- We already have a type in the environment so fail. - sig' : _ -> - let p = unPosFlaky $ sigType sig + decl' : _ -> + let p = unPosFlaky $ declType decl msg = - [ DS "Duplicate type signature", - DD sig, + [ DS "Duplicate type declaration", + DD decl, DS "Previous was", - DD sig' + DD decl' ] - in Env.extendSourceLocation p sig $ Env.err msg + in Env.extendSourceLocation p decl $ Env.err msg