diff --git a/LICENSE b/LICENSE new file mode 100644 --- /dev/null +++ b/LICENSE @@ -0,0 +1,24 @@ +Copyright (c) 2013, University of Pennsylvania +All rights reserved. + +Redistribution and use in source and binary forms, with or without +modification, are permitted provided that the following conditions are met: + * Redistributions of source code must retain the above copyright + notice, this list of conditions and the following disclaimer. + * Redistributions in binary form must reproduce the above copyright + notice, this list of conditions and the following disclaimer in the + documentation and/or other materials provided with the distribution. + * Neither the name of the University of Pennsylvania nor the + names of its contributors may be used to endorse or promote products + derived from this software without specific prior written permission. + +THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS "AS IS" AND +ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT LIMITED TO, THE IMPLIED +WARRANTIES OF MERCHANTABILITY AND FITNESS FOR A PARTICULAR PURPOSE ARE +DISCLAIMED. IN NO EVENT SHALL UNIVERSITY OF PENNSYLVANIA BE LIABLE FOR ANY +DIRECT, INDIRECT, INCIDENTAL, SPECIAL, EXEMPLARY, OR CONSEQUENTIAL DAMAGES +(INCLUDING, BUT NOT LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS OR SERVICES; +LOSS OF USE, DATA, OR PROFITS; OR BUSINESS INTERRUPTION) HOWEVER CAUSED AND +ON ANY THEORY OF LIABILITY, WHETHER IN CONTRACT, STRICT LIABILITY, OR TORT +(INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT OF THE USE OF THIS +SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE. diff --git a/Setup.hs b/Setup.hs new file mode 100644 --- /dev/null +++ b/Setup.hs @@ -0,0 +1,2 @@ +import Distribution.Simple +main = defaultMain diff --git a/pi-forall.cabal b/pi-forall.cabal new file mode 100644 --- /dev/null +++ b/pi-forall.cabal @@ -0,0 +1,54 @@ +Name: pi-forall +Version: 0.1.1 +License: BSD3 +License-file: LICENSE +Copyright: (c) 2013-2016 University of Pennsylvania +Description: An implementation of a simple dependently typed language for OPLSS 2013 +Author: Stephanie Weirich , based on code by Trellys Team +Maintainer: Stephanie Weirich +Cabal-Version: >= 1.8 +Build-type: Simple +tested-with: GHC == 7.8.4, GHC == 7.10.3, GHC == 8.0.1 +Category: Compilers/Interpreters +Homepage: https://github.com/sweirich/pi-forall +Synopsis: Demo implementation of typechecker for dependently-typed language + + +library + hs-source-dirs: src/ + Exposed-modules: Syntax + Parser + TypeCheck + Main + Build-depends: base >= 4 && < 5, + parsec >= 3.1.8 && < 3.2, + mtl >= 2.2.1, + pretty >= 1.0.1.0, + unbound-generics >= 0.2, + transformers, + array >= 0.3.0.2 && < 0.6, + containers, + directory, + filepath, + HUnit, + QuickCheck + + +executable pi-forall + hs-source-dirs: src/ + Main-is: Main.hs + Build-depends: base >=4, + parsec >= 3.1.8 && < 3.2, + mtl >= 2.2.1, + pretty >= 1.0.1.0, + unbound-generics >= 0.2, + transformers, + array >= 0.3.0.2 && < 0.6, + containers, + directory, + filepath, + HUnit, + QuickCheck + Ghc-Options: -Wall -fno-warn-unused-matches + + diff --git a/src/Main.hs b/src/Main.hs new file mode 100644 --- /dev/null +++ b/src/Main.hs @@ -0,0 +1,106 @@ +{- PiForall language, OPLSS -} + +{-# OPTIONS_GHC -Wall -fno-warn-unused-matches #-} + +-- | The command line interface to the pi type checker. +-- Also provides functions for type checking individual terms +-- and files. +module Main(goFilename,go,main, test) where + +import Modules (getModules) +import PrettyPrint +import Environment +import TypeCheck +import Parser + +import Text.PrettyPrint.HughesPJ (render) +import Text.ParserCombinators.Parsec.Error + +import Control.Monad.Except + +import System.Environment(getArgs) +import System.Exit (exitFailure,exitSuccess) +import System.FilePath (splitFileName) + +exitWith :: Either a b -> (a -> IO ()) -> IO b +exitWith res f = + case res of + Left x -> f x >> exitFailure + Right y -> return y + +-- | Type check the given string in the empty environment +go :: String -> IO () +go str = do + case parseExpr str of + Left parseError -> putParseError parseError + Right term -> do + putStrLn "parsed as" + putStrLn $ render $ disp term + res <- runTcMonad emptyEnv (inferType term) + case res of + Left typeError -> putTypeError typeError + Right (aterm, ty) -> do + putStrLn $ render $ disp aterm + putStrLn "typed with type" + putStrLn $ render $ disp ty + +-- | Display a parse error to the user +putParseError :: ParseError -> IO () +putParseError parseError = do + putStrLn $ render $ disp $ errorPos parseError + putStrLn $ show parseError + +-- | Display a type error to the user +putTypeError :: Disp d => d -> IO () +putTypeError typeError = do + putStrLn "Type Error:" + putStrLn $ render $ disp typeError + +-- | Type check the given file +goFilename :: String -> IO () +goFilename pathToMainFile = do + let prefixes = currentDir : mainFilePrefix : [] + (mainFilePrefix, name) = splitFileName pathToMainFile + currentDir = "" + putStrLn $ "processing " ++ name ++ "..." + v <- runExceptT (getModules prefixes name) + val <- v `exitWith` putParseError + putStrLn "type checking..." + d <- runTcMonad emptyEnv (tcModules val) + defs <- d `exitWith` putTypeError + putStrLn $ render $ disp (last defs) + + +test :: IO () +test = do + goFilename "../test/Lec1.pi" + goFilename "../test/Hw1.pi" + goFilename "../test/Lec2.pi" + goFilename "../test/Hw2.pi" + goFilename "../test/Lec3.pi" + goFilename "../test/Fin1.pi" + goFilename "../test/Lec4.pi" + + goFilename "../test/Logic.pi" + goFilename "../test/Equality.pi" + goFilename "../test/Product.pi" + goFilename "../test/Nat.pi" + goFilename "../test/Fin.pi" + goFilename "../test/Vec.pi" + + goFilename "../test/Lambda0.pi" + goFilename "../test/Lambda1.pi" + goFilename "../test/Lambda2.pi" + + + + +-- | 'pi ' invokes the type checker on the given +-- file and either prints the types of all definitions in the module +-- or prints an error message. +main :: IO () +main = do + [pathToMainFile] <- getArgs + goFilename pathToMainFile + exitSuccess + diff --git a/src/Parser.hs b/src/Parser.hs new file mode 100644 --- /dev/null +++ b/src/Parser.hs @@ -0,0 +1,669 @@ +{- PiForall language, OPLSS -} + +{-# LANGUAGE PatternGuards, FlexibleInstances, FlexibleContexts, TupleSections, ExplicitForAll, CPP #-} +{-# OPTIONS_GHC -Wall -fno-warn-unused-matches -fno-warn-orphans #-} + +-- | A parsec-based parser for the concrete syntax. +module Parser + ( + parseModuleFile, + parseModuleImports, + parseExpr + ) + where + + +import Syntax hiding (moduleImports) + +import Unbound.Generics.LocallyNameless + +import Text.Parsec hiding (State,Empty) +import Text.Parsec.Expr(Operator(..),Assoc(..),buildExpressionParser) +import qualified LayoutToken as Token + +import Control.Monad.State.Lazy hiding (join) + + +#ifdef MIN_VERSION_GLASGOW_HASKELL +#if MIN_VERSION_GLASGOW_HASKELL(7,10,3,0) +-- ghc >= 7.10.3 +#else +-- older ghc versions, but MIN_VERSION_GLASGOW_HASKELL defined +#endif +#else +-- MIN_VERSION_GLASGOW_HASKELL not even defined yet (ghc <= 7.8.x) +import Control.Applicative ( (<$>), (<*>)) +#endif + + + + + +import Control.Monad.Except hiding (join) + + + + +import Data.List +import qualified Data.Set as S + +{- + +Concrete syntax for the language: +Optional components in this BNF are marked with < > + + terms: + a,b,A,B ::= + Type Universes + | x Variables (start with lowercase) + | \ x . a Function definition + | a b Application + | (x : A) -> B Pi type + + | (a : A) Annotations + | (a) Parens + | TRUSTME An axiom 'TRUSTME', inhabits all types + + | let x = a in b Let expression + + | One Unit type + | tt Unit value + + | Bool Boolean type + | True | False Boolean values + | if a then b else c If + + | { x : A | B } Dependent pair type + | (a, b) Prod introduction + | pcase a of (x,y) -> b Prod elimination + | a = b Equality type + | refl Equality proof + | subst a by b Type conversion + | contra a Contra + + | C a ... Type / Term constructors + | case a [y] of Pattern matching + C1 [x] y z -> b1 + C2 x [y] -> b2 + + | \ [x <:A> ] . a Erased lambda + | a [b] Erased application + | [x : A] -> B Erased pi + + + declarations: + + foo : A + foo = a + + data T D : Type where + C1 of D1 + ... + Cn of Dn + + telescopes: + D ::= + Empty + | (x : A) D runtime cons + | (A) D runtime cons + | [x : A] D erased cons + | [A = B] D equality constraint + + + Syntax sugar: + + - You can collapse lambdas, like: + + \ x [y] z . a + + This gets parsed as \ x . \ [y] . \ z . a + +-} + +liftError :: (MonadError e m) => Either e a -> m a +liftError (Left e) = throwError e +liftError (Right a) = return a + +-- | Parse a module declaration from the given filepath. +parseModuleFile :: (MonadError ParseError m, MonadIO m) => ConstructorNames -> String -> m Module +parseModuleFile cnames name = do + liftIO $ putStrLn $ "Parsing File " ++ show name + contents <- liftIO $ readFile name + liftError $ runFreshM $ + flip evalStateT cnames $ + (runParserT (do { whiteSpace; v <- moduleDef;eof; return v}) [] name contents) + + +-- | Parse only the imports part of a module from the given filepath. +parseModuleImports :: (MonadError ParseError m, MonadIO m) => String -> m Module +parseModuleImports name = do + contents <- liftIO $ readFile name + liftError $ runFreshM $ + flip evalStateT emptyConstructorNames $ + + (runParserT (do { whiteSpace; moduleImports }) [] name contents) + +-- | Test an 'LParser' on a String. +testParser :: (LParser t) -> String -> Either ParseError t +testParser parser str = runFreshM $ + flip evalStateT emptyConstructorNames $ + + runParserT (do { whiteSpace; v <- parser; eof; return v}) [] "" str + +-- | Parse an expression. +parseExpr :: String -> Either ParseError Term +parseExpr = testParser expr + +-- * Lexer definitions +type LParser a = ParsecT + String -- The input is a sequence of Char + [Column] ( -- The internal state for Layout tabs + StateT ConstructorNames + FreshM) -- The internal state for generating fresh names, + a -- the type of the object being parsed + +instance Fresh (ParsecT s u (StateT ConstructorNames FreshM)) where + fresh = lift . lift . fresh + + + +-- Based on Parsec's haskellStyle (which we can not use directly since +-- Parsec gives it a too specific type). +trellysStyle :: (Stream s m Char, Monad m) => Token.GenLanguageDef s u m +trellysStyle = Token.LanguageDef + { Token.commentStart = "{-" + , Token.commentEnd = "-}" + , Token.commentLine = "--" + , Token.nestedComments = True + , Token.identStart = letter + , Token.identLetter = alphaNum <|> oneOf "_'" + , Token.opStart = oneOf ":!#$%&*+.,/<=>?@\\^|-" + , Token.opLetter = oneOf ":!#$%&*+.,/<=>?@\\^|-" + , Token.caseSensitive = True + , Token.reservedNames = + ["refl" + ,"ind" + ,"Type" + ,"data" + ,"where" + ,"case" + ,"of" + ,"with" + ,"contra" + ,"subst", "by", "at" + ,"let", "in" + ,"axiom" + ,"erased" + ,"TRUSTME" + ,"ord" + , "pcase" + , "Bool", "True", "False" + ,"if","then","else" + , "One", "tt" + ] + , Token.reservedOpNames = + ["!","?","\\",":",".",",","<", "=", "+", "-", "^", "()", "_","|","{", "}"] + } +tokenizer :: Token.GenTokenParser String [Column] (StateT ConstructorNames FreshM) + +layout :: forall a t. LParser a -> LParser t -> LParser [a] +(tokenizer, layout) = + let (t, Token.LayFun l) = Token.makeTokenParser trellysStyle "{" ";" "}" + in (t, l) + +identifier :: LParser String +identifier = Token.identifier tokenizer + +whiteSpace :: LParser () +whiteSpace = Token.whiteSpace tokenizer + +variable :: LParser TName +variable = + do i <- identifier + cnames <- get + if (i `S.member` (tconNames cnames) || + i `S.member` (dconNames cnames)) + then fail "Expected a variable, but a constructor was found" + else return $ string2Name i + + +wildcard :: LParser TName +wildcard = reservedOp "_" >> return wildcardName + +varOrWildcard :: LParser TName +varOrWildcard = try wildcard <|> variable + +dconstructor :: LParser DCName +dconstructor = + 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 TCName +tconstructor = + do i <- identifier + cnames <- get + if (i `S.member` tconNames cnames) + 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" + + +-- variables or zero-argument constructors +varOrCon :: LParser Term +varOrCon = do i <- identifier + cnames <- get + if (i `S.member` (dconNames cnames)) + then return (DCon i [] (Annot Nothing)) + else if (i `S.member` tconNames cnames) + then return (TCon i []) + else return (Var (string2Name i)) + + +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 + +parens :: LParser a -> LParser a +parens = Token.parens tokenizer +brackets :: LParser a -> LParser a +brackets = Token.brackets tokenizer + +-- braces = Token.braces tokenizer + +natural :: LParser Int +natural = fromInteger <$> Token.natural tokenizer + +natenc :: LParser Term +natenc = + do n <- natural + return $ encode n + where encode 0 = DCon "Zero" [] natty + encode n = DCon "Succ" [Arg Runtime (encode (n-1))] natty + natty = Annot $ Just (TCon "Nat" []) + + +moduleImports :: LParser Module +moduleImports = do + reserved "module" + modName <- identifier + reserved "where" + imports <- layout importDef (return ()) + return $ Module modName imports [] emptyConstructorNames + +moduleDef :: LParser Module +moduleDef = do + reserved "module" + modName <- identifier + reserved "where" + imports <- layout importDef (return ()) + decls <- layout decl (return ()) + cnames <- get + return $ Module modName imports decls cnames + +importDef :: LParser ModuleImport +importDef = do reserved "import" >> (ModuleImport <$> importName) + where importName = identifier + +telescope :: LParser Telescope +telescope = do + bindings <- telebindings + return $ foldr id Empty bindings where + +telebindings :: LParser [Telescope -> Telescope] +telebindings = many teleBinding + where + annot = do + (x,ty) <- try ((,) <$> varOrWildcard <*> (colon >> expr)) + <|> ((,) <$> (fresh wildcardName) <*> expr) + return (Cons Runtime x ty) + + imp = do + v <- varOrWildcard + colon + t <- expr + return (Cons Erased v t) + + equal = do + v <- variable + reservedOp "=" + t <- expr + return (Constraint (Var v) t) + + teleBinding :: LParser (Telescope -> Telescope) + teleBinding = + ( parens annot + <|> try (brackets imp) + <|> brackets equal) "binding" + + +--- +--- Top level declarations +--- + +decl,sigDef,valDef :: LParser Decl +decl = (try dataDef) <|> sigDef <|> valDef + +-- datatype declarations. +dataDef :: LParser Decl +dataDef = do + reserved "data" + name <- identifier + params <- telescope + colon + Type <- typen + modify (\cnames -> + cnames{ tconNames = S.insert name + (tconNames cnames) }) + reserved "where" + cs <- layout constructorDef (return ()) + forM_ cs + (\(ConstructorDef _ cname _) -> + modify (\cnames -> cnames{ dconNames = S.insert cname (dconNames cnames)})) + return $ Data name params cs + +constructorDef :: LParser ConstructorDef +constructorDef = do + pos <- getPosition + cname <- identifier + args <- option Empty (reserved "of" >> telescope) + return $ ConstructorDef pos cname args + "Constructor" + + +sigDef = do + n <- try (variable >>= \v -> colon >> return v) + ty <- expr + return $ Sig n ty + +valDef = do + n <- try (do {n <- variable; reservedOp "="; return n}) + val <- expr + return $ Def n val + + +------------------------ +------------------------ +-- Terms +------------------------ +------------------------ + +trustme :: LParser Term +trustme = do reserved "TRUSTME" + return (TrustMe (Annot Nothing)) + +refl :: LParser Term +refl = + do reserved "refl" + return $ Refl (Annot Nothing) + + +-- Expressions + +expr,term,factor :: LParser Term + +-- expr is the toplevel expression grammar +expr = do + p <- getPosition + Pos p <$> (buildExpressionParser table term) + where table = [ + [ifix AssocLeft "=" TyEq], + [ifixM AssocRight "->" mkArrow] + ] + ifix assoc op f = Infix (reservedOp op >> return f) assoc + ifixM assoc op f = Infix (reservedOp op >> f) assoc + mkArrow = + do n <- fresh wildcardName + return $ \tyA tyB -> + Pi (bind (n,embed tyA) 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 +-- allows us to keep constructors fully applied in the abstract syntax. +term = try dconapp <|> try tconapp <|> funapp + +arg :: LParser Arg +arg = (Arg Erased) <$> brackets expr <|> (Arg Runtime) <$> factor + +dconapp :: LParser Term +dconapp = do + c <- dconstructor + args <- many arg + return $ DCon c args (Annot Nothing) + +tconapp :: LParser Term +tconapp = do + c <- tconstructor + ts <- many factor + return $ TCon c ts + + +funapp :: LParser Term +funapp = do + f <- factor + foldl' app f <$> many bfactor + where + bfactor = ((,Erased) <$> brackets expr) + <|> ((,Runtime) <$> factor) + app e1 (e2,Runtime) = App e1 e2 + app e1 (e2,Erased) = ErasedApp e1 e2 + + +factor = choice [ varOrCon "a variable or nullary data constructor" + + , typen "Type" + , lambda "a lambda" + , letExpr "a let" + , natenc "a literal" + , caseExpr "a case" + , substExpr "a subst" + , refl "refl" + , contra "a contra" + , trustme "TRUSTME" + , impProd "an implicit function type" + + , bconst "a constant" + , ifExpr "an if expression" + , sigmaTy "a sigma type" + , pcaseExpr "a pcase" + , expProdOrAnnotOrParens + "an explicit function type or annotated expression" + ] + +impOrExpVar :: LParser (TName, Epsilon) +impOrExpVar = try ((,Erased) <$> (brackets variable)) + <|> (,Runtime) <$> variable + + +typen :: LParser Term +typen = + do reserved "Type" + return Type + + + + -- Lambda abstractions have the syntax '\x . e' +lambda :: LParser Term +lambda = do reservedOp "\\" + binds <- many1 impOrExpVar + dot + body <- expr + return $ foldr lam body binds + where + lam (x, Runtime) m = Lam (bind (x, embed $ Annot Nothing) m) + + lam (x, Erased) m = ErasedLam (bind (x, embed $ Annot Nothing) m) + + + + + +bconst :: LParser Term +bconst = choice [reserved "Bool" >> return TyBool, + reserved "False" >> return (LitBool False), + reserved "True" >> return (LitBool True), + reserved "One" >> return TyUnit, + reserved "tt" >> return LitUnit] + +ifExpr :: LParser Term +ifExpr = + do reserved "if" + a <- expr + reserved "then" + b <- expr + reserved "else" + c <- expr + return (If a b c (Annot Nothing)) + {- + let tm = Match (bind (PatCon "True" []) b) + let fm = Match (bind (PatCon "False" []) c) + return $ (Case a [tm, fm] (Annot Nothing)) + -} + +-- +letExpr :: LParser Term +letExpr = + do reserved "let" + x <- variable + reservedOp "=" + boundExp <- expr + reserved "in" + body <- expr + return $ (Let (bind (x,embed boundExp) body)) + +-- impProd - implicit dependent products +-- These have the syntax [x:a] -> b or [a] -> b . +impProd :: LParser Term +impProd = + do (x,tyA) <- brackets + (try ((,) <$> variable <*> (colon >> expr)) + <|> ((,) <$> fresh wildcardName <*> expr)) + reservedOp "->" + tyB <- expr + return $ ErasedPi (bind (x,embed tyA) tyB) + + +-- Function types have the syntax '(x:A) -> B'. This production deals +-- with the ambiguity caused because these types, annotations and +-- regular old parens all start with parens. + +data InParens = Colon Term Term | Comma Term Term | Nope Term + +expProdOrAnnotOrParens :: LParser Term +expProdOrAnnotOrParens = + let + -- afterBinder picks up the return type of a pi + afterBinder :: LParser Term + afterBinder = do reservedOp "->" + rest <- expr + return rest + + -- before binder parses an expression in parens + -- If it doesn't involve a colon, you get (Right tm) + -- If it does, you get (Left tm1 tm2). tm1 might be a variable, + -- in which case you might be looking at an explicit pi type. + beforeBinder :: LParser InParens + beforeBinder = parens $ + choice [do e1 <- try (term >>= (\e1 -> colon >> return e1)) + e2 <- expr + return $ Colon e1 e2 + , do e1 <- try (term >>= (\e1 -> comma >> return e1)) + e2 <- expr + return $ Comma e1 e2 + , Nope <$> expr] + in + do bd <- beforeBinder + case bd of + Colon (Var x) a -> + option (Ann (Var x) a) + (do b <- afterBinder + return $ Pi (bind (x,embed a) b)) + Colon a b -> return $ Ann a b + Comma a b -> return $ Prod a b (Annot Nothing) + Nope a -> return $ Paren a + +pattern :: LParser Pattern +-- Note that 'dconstructor' and 'variable' overlaps, annoyingly. +pattern = try (PatCon <$> dconstructor <*> many arg_pattern) + <|> atomic_pattern + where + arg_pattern = ((,Erased) <$> brackets pattern) + <|> ((,Runtime) <$> atomic_pattern) + atomic_pattern = (parens pattern) + <|> (PatVar <$> wildcard) + <|> do t <- varOrCon + case t of + (Var x) -> return $ PatVar x + (DCon c [] _) -> return $ PatCon c [] + (TCon c []) -> fail "expected a data constructor but a type constructor was found" + _ -> error "internal error in atomic_pattern" + +match :: LParser Match +match = + do pat <- pattern + reservedOp "->" + body <- term + return $ Match (bind pat body) + +caseExpr :: LParser Term +caseExpr = do + reserved "case" + scrut <- factor + reserved "of" + alts <- layout match (return ()) + return $ Case scrut alts (Annot Nothing) + + +pcaseExpr :: LParser Term +pcaseExpr = do + reserved "pcase" + scrut <- expr + reserved "of" + reservedOp "(" + x <- variable + reservedOp "," + y <- variable + reservedOp ")" + reservedOp "->" + a <- expr + return $ Pcase scrut (bind (x,y) a) (Annot Nothing) + +-- subst e0 by e1 +substExpr :: LParser Term +substExpr = do + reserved "subst" + a <- expr + reserved "by" + b <- expr + return $ Subst a b (Annot Nothing) + +contra :: LParser Term +contra = do + reserved "contra" + witness <- expr + return $ Contra witness (Annot Nothing) + + +sigmaTy :: LParser Term +sigmaTy = do + reservedOp "{" + x <- variable + colon + a <- expr + reservedOp "|" + b <- expr + reservedOp "}" + return (Sigma (bind (x, embed a) b)) + + diff --git a/src/Syntax.hs b/src/Syntax.hs new file mode 100644 --- /dev/null +++ b/src/Syntax.hs @@ -0,0 +1,399 @@ +{- PiForall language, OPLSS -} + +{-# LANGUAGE TemplateHaskell, + FlexibleInstances, + MultiParamTypeClasses, + FlexibleContexts, + UndecidableInstances, + ViewPatterns, + EmptyDataDecls, + DeriveGeneric, + DeriveDataTypeable, + CPP #-} + +{-# OPTIONS_GHC -Wall -fno-warn-unused-matches -fno-warn-orphans #-} + + + +-- | The abstract syntax of the simple dependently typed language +-- See comment at the top of 'Parser' for the concrete syntax + +module Syntax where + +#ifdef MIN_VERSION_GLASGOW_HASKELL +#if MIN_VERSION_GLASGOW_HASKELL(7,10,3,0) +-- ghc >= 7.10.3 +#else +-- older ghc versions, but MIN_VERSION_GLASGOW_HASKELL defined +#endif +#else +-- MIN_VERSION_GLASGOW_HASKELL not even defined yet (ghc <= 7.8.x) + +-- both needed only on even earlier ghc's +-- import Control.Applicative (pure) +-- import Data.Monoid (mempty) +#endif + + +import GHC.Generics (Generic) +import Data.Typeable (Typeable) + +import Unbound.Generics.LocallyNameless +import Unbound.Generics.LocallyNameless.Unsafe (unsafeUnbind) +import Unbound.Generics.LocallyNameless.TH (makeClosedAlpha) +import Text.ParserCombinators.Parsec.Pos +import Data.Set (Set) +import qualified Data.Set as S +import Data.Maybe (fromMaybe) + +----------------------------------------- +-- * Variable names +----------------------------------------- + +-- | term names, use unbound library to +-- automatically generate fv, subst, alpha-eq +type TName = Name Term + +-- | module names +type MName = String + +-- | type constructor names +type TCName = String + +-- | data constructor names +type DCName = String + +----------------------------------------- +-- * Core language +----------------------------------------- + + +-- Type abbreviation for documentation +type Type = Term + +data Term = + -- basic language + Type -- ^ type of types + | Var TName -- ^ variables + | Lam (Bind (TName, Embed Annot) Term) + -- ^ abstraction + | App Term Term -- ^ application + | Pi (Bind (TName, Embed Term) Term) -- ^ function type + + -- practical matters for surface language + | Ann Term Term -- ^ Annotated terms `( x : A )` + | Paren Term -- ^ parenthesized term, useful for printing + | Pos SourcePos Term -- ^ marked source position, for error messages + + -- conveniences + | TrustMe Annot -- ^ an axiom 'TRUSTME', inhabits all types + + -- unit + | TyUnit -- ^ The type with a single inhabitant `One` + | LitUnit -- ^ The inhabitant, written `tt` + + -- homework: boolean expressions + | TyBool -- ^ The type with two inhabitants + | LitBool Bool -- ^ True and False + | If Term Term Term Annot -- ^ If expression for eliminating booleans + + -- homework sigma types + | Sigma (Bind (TName, Embed Term) Term) + -- ^ sigma type `{ x : A | B }` + | Prod Term Term Annot + -- ^ introduction for sigmas `( a , b )` + | Pcase Term (Bind (TName, TName) Term) Annot + -- ^ elimination form `pcase p of (x,y) -> p` + + -- homework let expression + | Let (Bind (TName, Embed Term) Term) + -- ^ let expression, introduces a new (potentially recursive) + -- definition in the ctx + + + -- propositional equality + | TyEq Term Term -- ^ Equality type `a = b` + | Refl Annot -- ^ Proof of equality + | Subst Term Term Annot + -- ^ equality elimination + | Contra Term Annot -- ^ witness to an equality contradiction + + -- erasure + | ErasedLam (Bind (TName, Embed Annot) Term) -- ^ abstraction + | ErasedPi (Bind (TName, Embed Term) Term) -- ^ function type + | ErasedApp Term Term -- ^ application + + -- datatypes + | TCon String [Term] -- ^ type constructors (fully applied) + | DCon String [Arg] Annot -- ^ term constructors + --- (fully applied, erased arguments first) + | Case Term [Match] Annot -- ^ case analysis + + deriving (Show, Generic, Typeable) + +-- | An 'Annot' is optional type information +newtype Annot = Annot (Maybe Term) deriving (Show, Generic, Typeable) + +-- | A 'Match' represents a case alternative +data Match = Match (Bind Pattern Term) deriving (Show, Generic, Typeable) + +-- | The patterns of case expressions bind all variables +-- in their respective branches. +data Pattern = PatCon DCName [(Pattern, Epsilon)] + | PatVar TName deriving (Show, Eq, Generic, Typeable) + + + +----------------------------------------- +-- * Modules and declarations +----------------------------------------- + +-- | 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 :: MName, + moduleImports :: [ModuleImport], + moduleEntries :: [Decl] + , moduleConstructors :: ConstructorNames + + } + + deriving (Show, Generic, Typeable) + +newtype ModuleImport = ModuleImport MName + deriving (Show,Eq, Generic, Typeable) + +data ConstructorNames = ConstructorNames { + tconNames :: Set String, + dconNames :: Set String + } + deriving (Show, Eq, Generic, Typeable) + + +-- | Declarations are the components of modules +data Decl = Sig TName Term + -- ^ Declaration for the type of a term + + | Def TName Term + -- ^ The definition of a particular name, must + -- already have a type declaration in scope + + | RecDef TName Term + -- ^ A potentially (recursive) definition of + -- a particular name, must be declared + + | Data TCName Telescope [ConstructorDef] + -- ^ Declaration for a datatype including all of + -- its data constructors + | DataSig TCName Telescope + -- ^ An abstract view of a datatype. Does + -- not include any information about its data + -- constructors + + deriving (Show, Generic, Typeable) + +-- | A Data constructor has a name and a telescope of arguments +data ConstructorDef = ConstructorDef SourcePos DCName Telescope + deriving (Show, Generic, Typeable) + +------------- +-- * Telescopes +------------- +-- | A telescope is like a first class context. It binds each name +-- in the rest of the telescope. For example +-- Delta = x:* , y:x, y = w, empty +data Telescope = Empty + | Cons Epsilon TName Term Telescope + | Constraint Term Term Telescope + deriving (Show, Generic, Typeable) + +-- | Epsilon annotates the sort of a data constructor argument +data Epsilon = + Runtime + | Erased + deriving (Eq,Show,Read,Bounded,Ord,Generic,Typeable) + +-- | An argument is tagged with whether it should be erased +data Arg = Arg Epsilon Term deriving (Show, Generic, Typeable) + + +------------- +-- * Auxiliary functions on syntax +------------- + +-- | empty set of constructor names +emptyConstructorNames :: ConstructorNames +emptyConstructorNames = ConstructorNames S.empty S.empty + +-- | Extract the term from an Arg +unArg :: Arg -> Term +unArg (Arg _ t) = t + + + +-- | Default name for '_' occurring in patterns +wildcardName :: TName +wildcardName = string2Name "_" + +-- | empty Annotation +noAnn :: Annot +noAnn = Annot Nothing + +-- | Partial inverse of Pos +unPos :: Term -> Maybe SourcePos +unPos (Pos p _) = Just p +unPos _ = Nothing + +-- | Tries to find a Pos anywhere inside a term +unPosDeep :: Term -> Maybe SourcePos +unPosDeep = unPos -- something (mkQ Nothing unPos) -- TODO: Generic version of this + +-- | Tries to find a Pos inside a term, otherwise just gives up. +unPosFlaky :: Term -> SourcePos +unPosFlaky t = fromMaybe (newPos "unknown location" 0 0) (unPosDeep t) + +-- | Is this the syntax of a literal (natural) number +isNumeral :: Term -> Maybe Int +isNumeral (Pos _ t) = isNumeral t +isNumeral (Paren t) = isNumeral t +isNumeral (DCon c [] _) | c== "Zero" = Just 0 +isNumeral (DCon c [Arg _ t] _) | c== "Succ" = + do n <- isNumeral t ; return (n+1) +isNumeral _ = Nothing + +-- | Is this pattern a variable +isPatVar :: Pattern -> Bool +isPatVar (PatVar _) = True +isPatVar _ = False + + +--------------------- +-- * Erasure +--------------------- + +class Erase a where + -- | erase all computationally irrelevant parts of an expression + -- these include all typing annotations + -- irrelevant arguments are replaced by unit + erase :: a -> a + +instance Erase Term where + erase (Var x) = Var x + erase (Lam bnd) = Lam (bind (x, embed noAnn) (erase body)) + where ((x,unembed -> _), body) = unsafeUnbind bnd + erase (App a1 a2) = App (erase a1) (erase a2) + erase (Type) = Type + erase (Pi bnd) = Pi (bind (x, embed (erase tyA)) (erase tyB)) + where ((x,unembed -> tyA), tyB) = unsafeUnbind bnd + erase (Ann t1 t2) = erase t1 + erase (Paren t1) = erase t1 + erase (Pos sp t) = erase t + erase (TrustMe _) = TrustMe noAnn + erase (TyUnit) = TyUnit + erase (LitUnit) = LitUnit + erase (TyBool) = TyBool + erase (LitBool b) = LitBool b + erase (If a b c _) = If (erase a) (erase b) (erase c) noAnn + erase (Let bnd) = Let (bind (x,embed (erase rhs)) (erase body)) + where ((x,unembed -> rhs),body) = unsafeUnbind bnd + + erase (TyEq a b) = TyEq (erase a) (erase b) + erase (Refl _) = Refl noAnn + erase (Subst tm pf _) = Subst (erase tm) (erase pf) noAnn + erase (Contra tm _) = Contra (erase tm) noAnn + + erase (ErasedLam bnd) = ErasedLam (bind (x, embed noAnn) (erase body)) + where ((x,unembed -> _), body) = unsafeUnbind bnd + erase (ErasedApp tm1 tm2) = ErasedApp (erase tm1) LitUnit + erase (ErasedPi bnd) = ErasedPi (bind (x, embed (erase tyA)) (erase tyB)) + where ((x,unembed -> tyA), tyB) = unsafeUnbind bnd + + erase (TCon n tms) = TCon n (map erase tms) + erase (DCon n args _) = DCon n (map erase args) noAnn + erase (Case tm ms _) = Case (erase tm) (map erase ms) noAnn + + erase (Sigma bnd) = Sigma (bind (x, embed (erase tyA)) (erase tyB)) + where ((x,unembed->tyA),tyB) = unsafeUnbind bnd + erase (Prod a b _) = Prod (erase a) (erase b) noAnn + erase (Pcase a bnd _) = + Pcase (erase a) (bind (x,y) (erase body)) noAnn where + ((x,y),body) = unsafeUnbind bnd + +instance Erase Match where + erase (Match bnd) = Match (bind p (erase t)) where + (p,t) = unsafeUnbind bnd + +instance Erase Arg where + erase (Arg Runtime t) = Arg Runtime (erase t) + erase (Arg Erased t) = Arg Erased LitUnit + + +----------------- +-- * Alpha equivalence, free variables and substitution. +------------------ + +{- We use the unbound 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 the template haskell directives and default class instances + below. +-} + +-- Defining SourcePos abstractly means that they get ignored +-- when comparing terms. +-- XXX need one with aeq' that always returns true. +$(makeClosedAlpha ''SourcePos) +-- instance Alpha SourcePos where +-- aeq' _ctx _ _ = True +-- fvAny' _ctx _nfn = pure +-- open _ _ = id +-- close _ _ = id +-- isPat _ = mempty +-- isTerm _ = True +-- nthPatFind _ _ = Left 0 +-- namePatFind _ _ = Left 0 +-- swaps' _ _ = id +-- freshen' _ x = return (x, mempty) +-- lfreshen' _ x cont = cont x mempty + +instance Subst b SourcePos where subst _ _ = id ; substs _ = id + +-- Among other things, the Alpha class enables the following +-- functions: +-- aeq :: Alpha a => a -> a -> Bool +-- fv :: Alpha a => a -> [Name a] + +instance Alpha Term where + +instance Alpha Match +instance Alpha Pattern +instance Alpha Epsilon +instance Alpha Telescope +instance Alpha Arg +instance Alpha ConstructorDef + +instance Alpha Annot where + -- override default behavior so that type annotations are ignored + -- when comparing for alpha-equivalence + aeq' _ _ _ = True + +-- The subst class derives capture-avoiding substitution +-- It has two parameters because the sort of thing we are substiting +-- for may not be the same as what we are substituting into: + +-- class Subst b a where +-- subst :: Name b -> b -> a -> a -- single substitution +-- substs :: [(Name b, b)] -> a -> a -- multiple substitution + +instance Subst Term Term where + isvar (Var x) = Just (SubstName x) + isvar _ = Nothing + +instance Subst Term Epsilon +instance Subst Term Match +instance Subst Term Pattern +instance Subst Term Telescope +instance Subst Term Arg +instance Subst Term ConstructorDef + +instance Subst Term Annot + diff --git a/src/TypeCheck.hs b/src/TypeCheck.hs new file mode 100644 --- /dev/null +++ b/src/TypeCheck.hs @@ -0,0 +1,847 @@ +{- PiForall language -} + +{-# LANGUAGE ViewPatterns, TypeSynonymInstances, + ExistentialQuantification, NamedFieldPuns, + ParallelListComp, FlexibleContexts, ScopedTypeVariables, + TupleSections, FlexibleInstances, CPP #-} +{-# OPTIONS_GHC -Wall -fno-warn-unused-matches #-} + +-- | The main routines for type-checking +module TypeCheck(tcModules, inferType, checkType) where + +import Syntax +import Environment +import PrettyPrint +import Equal + +import Unbound.Generics.LocallyNameless +import Unbound.Generics.LocallyNameless.Internal.Fold (toListOf) + + +#ifdef MIN_VERSION_GLASGOW_HASKELL +#if MIN_VERSION_GLASGOW_HASKELL(7,10,3,0) +-- ghc >= 7.10.3 +#else +-- older ghc versions, but MIN_VERSION_GLASGOW_HASKELL defined +#endif +#else +-- MIN_VERSION_GLASGOW_HASKELL not even defined yet (ghc <= 7.8.x) +import Control.Applicative +#endif + + + + +import Control.Monad.Except +import Text.PrettyPrint.HughesPJ +import Data.Maybe +import Data.List(nub) +import Unbound.Generics.LocallyNameless.Unsafe (unsafeUnbind) + + + +-- | Infer the type of a term, producing an annotated version of the +-- term (whose type can *always* be inferred). +inferType :: Term -> TcMonad (Term,Type) +inferType t = tcTerm t Nothing + +-- | Check that the given term has the expected type. +-- The provided type does not necessarily need to be in whnf, but it should be +-- elaborated (i.e. already checked to be a good type). +checkType :: Term -> Type -> TcMonad (Term, Type) +checkType tm expectedTy = do + nf <- whnf expectedTy + tcTerm tm (Just nf) + +-- | check a term, producing an elaborated term +-- where all of the type annotations have been filled in +-- The second argument is 'Nothing' in inference mode and +-- an expected type (must be in whnf) in checking mode +tcTerm :: Term -> Maybe Type -> TcMonad (Term,Type) + +tcTerm t@(Var x) Nothing = do + ty <- lookupTy x + return (t,ty) + +tcTerm t@(Type) Nothing = return (t,Type) + +tcTerm (Pi bnd) Nothing = do + ((x, unembed -> tyA), tyB) <- unbind bnd + atyA <- tcType tyA + atyB <- extendCtx (Sig x atyA) $ tcType tyB + return (Pi (bind (x, embed atyA) atyB), Type) + +-- Check the type of a function +tcTerm (Lam bnd) (Just (Pi bnd2)) = do + -- unbind the variables in the lambda expression and pi type + ((x,unembed -> Annot ma), body, + (_, unembed -> tyA), tyB) <- unbind2Plus bnd bnd2 + -- check tyA matches type annotation on binder, if present + maybe (return ()) (equate tyA) ma + -- check the type of the body of the lambda expression + (ebody, etyB) <- extendCtx (Sig x tyA) (checkType body tyB) + return (Lam (bind (x, embed (Annot (Just tyA))) ebody), + Pi bnd2) +tcTerm (Lam _) (Just nf) = + err [DS "Lambda expression has a function type, not", DD nf] + +-- infer the type of a lambda expression, when an annotation +-- on the binder is present +tcTerm (Lam bnd) Nothing = do + ((x,(unembed -> Annot annot)), body) <- unbind bnd + tyA <- maybe (err [DS "Must annotate lambda"]) (return) annot + -- check that the type annotation is well-formed + atyA <- tcType tyA + -- infer the type of the body of the lambda expression + (ebody, atyB) <- extendCtx (Sig x atyA) (inferType body) + return (Lam (bind (x, embed (Annot (Just atyA))) ebody), + Pi (bind (x, embed atyA) atyB)) + +tcTerm (App t1 t2) Nothing = do + (at1, ty1) <- inferType t1 + (x, tyA, tyB) <- ensurePi ty1 + (at2, ty2) <- checkType t2 tyA + let result = (App at1 at2, subst x at2 tyB) + return result + +-- Check the type of a function +tcTerm (ErasedLam bnd) (Just (ErasedPi bnd2)) = do + -- unbind the variables in the lambda expression and pi type + ((x,unembed -> Annot ma), body, + (_, unembed -> tyA), tyB) <- unbind2Plus bnd bnd2 + -- check tyA matches type annotation on binder, if present + maybe (return ()) (equate tyA) ma + -- check the type of the body of the lambda expression + (ebody, etyB) <- extendCtx (Sig x tyA) (checkType body tyB) + -- make sure that an 'erased' variable isn't used + when (x `elem` toListOf fv (erase ebody)) $ + err [DS "Erased variable", DD x, + DS "used in body"] + return (ErasedLam (bind (x, embed (Annot (Just tyA))) ebody), + ErasedPi bnd2) +tcTerm (ErasedLam _) (Just nf) = + err [DS "Lambda expression has a function type, not", DD nf] + +-- infer the type of a lambda expression, when an annotation +-- on the binder is present +tcTerm (ErasedLam bnd) Nothing = do + ((x,(unembed -> Annot annot)), body) <- unbind bnd + tyA <- maybe (err [DS "Must annotate lambda"]) (return) annot + -- check that the type annotation is well-formed + atyA <- tcType tyA + -- infer the type of the body of the lambda expression + (ebody, atyB) <- extendCtx (Sig x atyA) (inferType body) + -- make sure that an 'erased' variable isn't used + when (x `elem` toListOf fv (erase ebody)) $ + err [DS "Erased variable", DD x, + DS "used in body"] + return (ErasedLam (bind (x, embed (Annot (Just atyA))) ebody), + ErasedPi (bind (x, embed atyA) atyB)) + +tcTerm (ErasedApp t1 t2) Nothing = do + (at1, ty1) <- inferType t1 + (x, tyA, tyB) <- ensureErasedPi ty1 + (at2, ty2) <- checkType t2 tyA + let result = (ErasedApp at1 at2, subst x at2 tyB) + return result + +tcTerm (ErasedPi bnd) Nothing = do + ((x, unembed -> tyA), tyB) <- unbind bnd + atyA <- tcType tyA + atyB <- extendCtx (Sig x atyA) $ tcType tyB + return (ErasedPi (bind (x, embed atyA) atyB), Type) + + +tcTerm (Ann tm ty) Nothing = do + ty' <- tcType ty + (tm', ty'') <- checkType tm ty' + + return (tm', ty'') + +tcTerm (Pos p tm) mTy = + extendSourceLocation p tm $ tcTerm tm mTy + +tcTerm (Paren tm) mTy = tcTerm tm mTy + +tcTerm t@(TrustMe ann1) ann2 = do + expectedTy <- matchAnnots t ann1 ann2 + return (TrustMe (Annot (Just expectedTy)), expectedTy) + +tcTerm (TyUnit) Nothing = return (TyUnit, Type) + +tcTerm (LitUnit) Nothing = return (LitUnit, TyUnit) + +tcTerm (TyBool) Nothing = return (TyBool,Type) + + +tcTerm (LitBool b) Nothing = do + return (LitBool b, TyBool) + + +tcTerm t@(If t1 t2 t3 ann1) ann2 = do + ty <- matchAnnots t ann1 ann2 + (at1,_) <- checkType t1 TyBool + nf <- whnf at1 + let ctx b = case nf of + Var x -> [Def x (LitBool b)] + _ -> [] + (at2, _) <- extendCtxs (ctx True) $ checkType t2 ty + (at3, _) <- extendCtxs (ctx False) $ checkType t3 ty + return (If at1 at2 at3 (Annot (Just ty)), ty) + + +tcTerm (Let bnd) ann = do + ((x,unembed->rhs),body) <- unbind bnd + (arhs,aty) <- inferType rhs + (abody,ty) <- extendCtxs [Sig x aty, Def x arhs] $ + tcTerm body ann + when (x `elem` toListOf fv ty) $ + err [DS "Let bound variable", DD x, DS "escapes in type", DD ty] + return (Let (bind (x,embed arhs) abody), ty) + + +-- Type constructor application +tcTerm (TCon c params) Nothing = do + (delta, _) <- lookupTCon c + unless (length params == teleLength delta) $ + err [DS "Datatype constructor", DD c, + DS $ "should have " ++ show (teleLength delta) ++ + "parameters, but was given", DD (length params)] + eparams <- tsTele params delta + return (TCon c eparams, Type) + +-- 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@(DCon c args (Annot Nothing)) Nothing = do + matches <- lookupDConAll c + case matches of + [(tname,(Empty,ConstructorDef _ _ deltai))] -> do + let numArgs = teleLength deltai + unless (length args == numArgs) $ + err [DS "Constructor", DS c, + DS "should have", DD numArgs, + DS "data arguments, but was given", + DD (length args), DS "arguments."] + eargs <- tcArgTele args deltai + let ty = TCon tname [] + return (DCon c eargs (Annot (Just ty)),ty) + [_] -> err [DS "Cannot infer the parameters to data constructors.", + DS "Add an annotation."] + _ -> 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@(DCon c args ann1) ann2 = do + ty <- matchAnnots t ann1 ann2 + case ty of + (TCon tname params) -> do + (delta, deltai) <- lookupDCon c tname + let numArgs = teleLength deltai + unless (length args == numArgs) $ + 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 + eargs <- tcArgTele args newTele + return (DCon c eargs (Annot (Just ty)), ty) + _ -> + err [DS "Unexpected type", DD ty, DS "for data constructor", DD t] + +-- If we are in inference mode, then +-- we do not use refinement +-- otherwise, we must have a typing annotation +tcTerm t@(Case scrut alts ann1) ann2 = do + ty <- matchAnnots t ann1 ann2 + (ascrut, sty) <- inferType scrut + scrut' <- whnf ascrut + (n, params) <- ensureTCon sty + let checkAlt (Match bnd) = do + (pat, body) <- unbind bnd + -- add variables from pattern to context + -- could fail if branch is in-accessible + (decls, evars) <- declarePat pat Runtime (TCon n params) + -- add defs to the contents from scrut = pat + -- could fail if branch is in-accessible + decls' <- equateWithPat scrut' pat (TCon n params) + (ebody, _) <- extendCtxs (decls ++ decls') $ + checkType body ty + + -- make sure 'erased' components aren't used + when (any (`elem` (toListOf fv (erase ebody))) evars) $ + err [DS "Erased variable bound in match used"] + + return (Match (bind pat ebody)) + let pats = map (\(Match bnd) -> fst (unsafeUnbind bnd)) alts + aalts <- mapM checkAlt alts + exhaustivityCheck scrut' sty pats + return (Case ascrut aalts (Annot (Just ty)), ty) + + +tcTerm (TyEq a b) Nothing = do + (aa,aTy) <- inferType a + (ab,bTy) <- checkType b aTy + return (TyEq aa ab, Type) + + +tcTerm t@(Refl ann1) ann2 = do + ty <- matchAnnots t ann1 ann2 + case ty of + (TyEq a b) -> do + equate a b + return (Refl (Annot (Just ty)), ty) + _ -> err [DS "refl annotated with", DD ty] + +tcTerm t@(Subst tm p ann1) ann2 = do + ty <- matchAnnots t ann1 ann2 + -- infer the type of the proof p + (apf, tp) <- inferType p + -- make sure that it is an equality between m and n + (m,n) <- ensureTyEq tp + -- if either side is a variable, add a definition to the context + edecl <- do + m' <- whnf m + n' <- whnf n + case (m',n') of + (Var x, _) -> return [Def x n'] + (_, Var y) -> return [Def y m'] + (_,_) -> return [] + + pdecl <- do + p' <- whnf apf + case p' of + (Var x) -> return [Def x (Refl (Annot (Just tp)))] + _ -> return [] + let refined = extendCtxs (edecl ++ pdecl) + (atm, _) <- refined $ checkType tm ty + return (Subst atm apf (Annot (Just ty)), ty) + +tcTerm t@(Contra p ann1) ann2 = do + ty <- matchAnnots t ann1 ann2 + (apf, ty') <- inferType p + (a,b) <- ensureTyEq ty' + a' <- whnf a + b' <- whnf b + case (a',b') of + + (DCon da _ _, DCon db _ _) | da /= db -> + return (Contra apf (Annot (Just ty)), ty) + + (LitBool b1, LitBool b2) | b1 /= b2 -> + return (Contra apf (Annot (Just ty)), ty) + (_,_) -> err [DS "I can't tell that", DD a, DS "and", DD b, + DS "are contradictory"] + + +tcTerm t@(Sigma bnd) Nothing = do + ((x,unembed->tyA),tyB) <- unbind bnd + aa <- tcType tyA + ba <- extendCtx (Sig x aa) $ tcType tyB + return (Sigma (bind (x,embed aa) ba), Type) + + +tcTerm t@(Prod a b ann1) ann2 = do + ty <- matchAnnots t ann1 ann2 + case ty of + (Sigma bnd) -> do + ((x, unembed-> tyA), tyB) <- unbind bnd + (aa,_) <- checkType a tyA + (ba,_) <- extendCtxs [Sig x tyA, Def x aa] $ checkType b tyB + return (Prod aa ba (Annot (Just ty)), ty) + _ -> err [DS "Products must have Sigma Type", DD ty, + DS "found instead"] + + +tcTerm t@(Pcase p bnd ann1) ann2 = do + ty <- matchAnnots t ann1 ann2 + (apr, pty) <- inferType p + pty' <- whnf pty + case pty' of + Sigma bnd' -> do + ((x,unembed->tyA),tyB) <- unbind bnd' + ((x',y'),body) <- unbind bnd + let tyB' = subst x (Var x') tyB + nfp <- whnf apr + let ctx = case nfp of + Var x0 -> [Def x0 (Prod (Var x') (Var y') + (Annot (Just pty')))] + _ -> [] + (abody, bTy) <- extendCtxs ([Sig x' tyA, Sig y' tyB'] ++ ctx) $ + checkType body ty + return (Pcase apr (bind (x',y') abody) (Annot (Just ty)), bTy) + _ -> err [DS "Scrutinee of pcase must have Sigma type"] + + +tcTerm tm (Just ty) = do + (atm, ty') <- inferType tm + equate ty' ty + + return (atm, ty) + + + + +--------------------------------------------------------------------- +-- helper functions for type checking + +-- | Merge together two sources of type information +-- The first annotation is assumed to come from an annotation on +-- the syntax of the term itself, the second as an argument to +-- 'checkType'. +matchAnnots :: Term -> Annot -> Maybe Type -> TcMonad Type +matchAnnots e (Annot Nothing) Nothing = err + [DD e, DS "requires annotation"] +matchAnnots e (Annot Nothing) (Just t) = return t +matchAnnots e (Annot (Just t)) Nothing = do + at <- tcType t + return at +matchAnnots e (Annot (Just t1)) (Just t2) = do + at1 <- tcType t1 + equate at1 t2 + return at1 + +-- | Make sure that the term is a type (i.e. has type 'Type') +tcType :: Term -> TcMonad Term +tcType tm = do + (atm, _) <- checkType tm Type + return atm + + +--------------------------------------------------------------------- +-- helper functions for type constructor creation + +-- | type check a list of type constructor arguments against a telescope +tsTele :: [Term] -> Telescope -> TcMonad [Term] +tsTele tms tele = do + args <- tcArgTele (map (Arg Runtime) tms) tele + return (map unArg args) + +--------------------------------------------------------------------- +-- helper functions for data constructor creation + +-- | calculate the length of a telescope +teleLength :: Telescope -> Int +teleLength Empty = 0 +teleLength (Constraint _ _ tele) = teleLength tele +teleLength (Cons _ _ _ tele) = 1 + teleLength tele + +-- | type check a list of data constructor arguments against a telescope +tcArgTele :: [Arg] -> Telescope -> TcMonad [Arg] +tcArgTele [] Empty = return [] +tcArgTele args (Constraint tx ty tele) = do + equate tx ty + tcArgTele args tele +tcArgTele (Arg ep1 tm:terms) (Cons ep2 x ty tele') | ep1 == ep2 = do + (etm, ety) <- checkType tm ty + tele'' <- doSubst [(x,etm)] tele' + eterms <- tcArgTele terms tele'' + return $ Arg ep1 etm:eterms +tcArgTele (Arg ep1 _ : _) (Cons ep2 _ _ _) = + err [DD ep1, DS "argument provided when", + DD ep2, DS "argument was expected"] +tcArgTele [] _ = + err [DD "Too few arguments provided."] +tcArgTele _ Empty = + err [DD "Too many arguments provided."] + +-- | Substitute a list of terms for the variables bound in a telescope +-- This is used to instantiate the parameters of a data constructor +-- to find the types of its arguments. +-- The first argument should only contain 'Runtime' type declarations. +substTele :: Telescope -> [ Term ] -> Telescope -> TcMonad Telescope +substTele tele args delta = doSubst (mkSubst tele args) delta where + mkSubst Empty [] = [] + mkSubst (Cons Runtime x _ tele') (tm : tms) = + (x, tm) : mkSubst tele' tms + mkSubst _ _ = error "Internal error: substTele given illegal arguments" + +-- From a constraint, fetch all declarations +-- derived from unifying the two terms +-- If the terms are not unifiable, throw an error +-- Note: we could do better with our unification +amb :: Term -> Bool +amb (App t1 t2) = True +amb (Pi _) = True +amb (If _ _ _ _) = True +amb (Sigma _) = True +amb (Pcase _ _ _ ) = True +amb (Let _ ) = True +amb (ErasedLam _) = True +amb (ErasedPi _) = True +amb (ErasedApp _ _) = True +amb (Case _ _ _) = True +amb _ = False + +constraintToDecls :: Term -> Term -> TcMonad [Decl] +constraintToDecls tx ty = do + txnf <- whnf tx + tynf <- whnf ty + if (aeq txnf tynf) then return [] + else case (txnf, tynf) of + (Var y, yty) -> return [Def y yty] + (yty, Var y) -> return [Def y yty] + (TCon s1 tms1, TCon s2 tms2) + | s1 == s2 -> matchTerms tms1 tms2 + (Prod a1 a2 _, Prod b1 b2 _) -> matchTerms [a1,a2] [b1,b2] + (TyEq a1 a2, TyEq b1 b2) -> matchTerms [a1,a2] [b1,b2] + (DCon s1 a1s _, DCon s2 a2s _) + | s1 == s2 -> matchArgs a1s a2s + _ -> + if amb txnf || amb tynf + then return [] + else err [DS "Cannot equate", DD txnf, DS "and", DD tynf] + + where + matchTerms ts1 ts2 = matchArgs (map (Arg Runtime) ts1) (map (Arg Runtime) ts2) + matchArgs (Arg _ t1 : a1s) (Arg _ t2 : a2s) = do + ds <- constraintToDecls t1 t2 + ds' <- matchArgs a1s a2s + return $ ds ++ ds' + matchArgs [] [] = return [] + matchArgs _ _ = err [DS "internal error (constraintToDecls)"] + + +-- Propagate the given substitution through the telescope, potentially +-- reworking the constraints. +doSubst :: [(TName,Term)] -> Telescope -> TcMonad Telescope +doSubst ss Empty = return Empty +doSubst ss (Constraint tx ty tele') = do + let tx' = substs ss tx + let ty' = substs ss ty + -- (_decls, tsf) <- match tx' ty' + decls <- constraintToDecls tx' ty' + tele <- extendCtxs decls $ (doSubst ss tele') + return $ (Constraint tx' ty' tele) +doSubst ss (Cons ep x ty tele') = do + tynf <- whnf (substs ss ty) + tele'' <- doSubst ss tele' + return $ Cons ep x tynf tele'' + + +----------------------------------------------------------- +-- helper functions for checking pattern matching + +-- | Create a binding in the context for each of the variables in +-- the pattern. +-- Also returns the erased variables so that they can be checked +declarePat :: Pattern -> Epsilon -> Type -> TcMonad ([Decl], [TName]) +declarePat (PatVar x) Runtime y = return ([Sig x y],[]) +declarePat (PatVar x) Erased y = return ([Sig x y],[x]) +declarePat (PatCon d pats) Runtime (TCon c params) = do + (delta, deltai) <- lookupDCon d c + tele <- substTele delta params deltai + declarePats d pats tele +declarePat (PatCon d pats) Erased (TCon c params) = + err [DS "Cannot pattern match erased arguments"] +declarePat pat ep ty = + err [DS "Cannot match pattern", DD pat, DS "with type", DD ty] + +declarePats :: DCName -> [(Pattern,Epsilon)] -> Telescope -> TcMonad ([Decl],[TName]) +declarePats dc [] Empty = return ([],[]) +declarePats dc pats (Constraint tx ty tele) = do + new_decls <- constraintToDecls tx ty + (decls, names) <- extendCtxs new_decls $ declarePats dc pats tele + return (new_decls ++ decls, names) +declarePats dc ((pat,_):pats) (Cons ep x ty tele) = do + (ds1,v1) <- declarePat pat ep ty + tm <- pat2Term pat ty + (ds2,v2) <- declarePats dc pats (subst x tm tele) + return ((ds1 ++ ds2),(v1 ++ v2)) +declarePats dc [] _ = err [DS "Not enough patterns in match for data constructor", DD dc] +declarePats dc pats Empty = err [DS "Too many patterns in match for data constructor", DD dc] + + +-- | Convert a pattern to an (annotated) term so that we can substitute it for +-- variables in telescopes. Because data constructors must be annotated with +-- their types, we need to have the expected type of the pattern available. +pat2Term :: Pattern -> Type -> TcMonad Term +pat2Term (PatCon dc pats) ty@(TCon n params) = do + (delta, deltai) <- lookupDCon dc n + tele <- substTele delta params deltai + args <- pats2Terms pats tele + return (DCon dc args (Annot (Just ty))) + where + pats2Terms :: [(Pattern,Epsilon)] -> Telescope -> TcMonad [Arg] + pats2Terms [] Empty = return [] + pats2Terms ps (Constraint tx' ty' tele') = do + decls <- constraintToDecls tx' ty' + extendCtxs decls $ pats2Terms ps tele' + pats2Terms ((p,_) : ps) (Cons ep x ty1 d) = do + ty' <- whnf ty1 + t <- pat2Term p ty' + ts <- pats2Terms ps (subst x t d) + return (Arg ep t : ts) + pats2Terms _ _ = err [DS "Invalid number of args to pattern", DD dc] +pat2Term (PatCon _ _) ty = error "Internal error: should be a tcon" +pat2Term (PatVar x) ty = return (Var x) + +-- | Create a list of variable definitions from the scrutinee +-- of a case expression and the pattern in a branch. Scrutinees +-- that are not variables or constructors applied to vars may not +-- produce any equations. +equateWithPat :: Term -> Pattern -> Type -> TcMonad [Decl] +equateWithPat (Var x) pat ty = do + tm <- pat2Term pat ty + return [Def x tm] +equateWithPat (DCon dc args _) (PatCon dc' pats) (TCon n params) + | dc == dc' = do + (delta, deltai) <- lookupDCon dc n + tele <- substTele delta params deltai + let eqWithPats :: [Term] -> [(Pattern,Epsilon)] -> Telescope -> TcMonad [Decl] + eqWithPats [] [] Empty = return [] + eqWithPats ts ps (Constraint tx ty tl) = do + decls <- constraintToDecls tx ty + extendCtxs decls $ eqWithPats ts ps tl + eqWithPats (t : ts) ((p,_) : ps) (Cons _ x ty tl) = do + t' <- whnf t + decls <- equateWithPat t' p ty + decls' <- eqWithPats ts ps (subst x t' tl) + return (decls ++ decls') + eqWithPats _ _ _ = + err [DS "Invalid number of args to pattern", DD dc] + eqWithPats (map unArg args) pats tele +equateWithPat (DCon dc args _) (PatCon dc' pats) (TCon n params) = do + warn [DS "The case for", DD dc', DS "is unreachable.", + DS "However, this implementation cannot yet allow it", + DS "to be omitted."] >> return [] +equateWithPat _ _ _ = return [] + + +-- | Check all of the types contained within a telescope +-- returns a telescope where all of the types have been annotated +tcTypeTele :: Telescope -> TcMonad Telescope +tcTypeTele Empty = return Empty +tcTypeTele (Constraint tm1 tm2 tl) = do + (tm1', ty1) <- inferType tm1 + (tm2',_) <- checkType tm2 ty1 + decls <- constraintToDecls tm1' tm2' + tele' <- extendCtxs decls $ tcTypeTele tl + return (Constraint tm1' tm2' tele') +tcTypeTele (Cons ep x ty tl) = do + ty' <- tcType ty + tele' <- extendCtx (Sig x ty') $ tcTypeTele tl + return (Cons ep x ty' tele') + + + +-------------------------------------------------------- +-- Using the typechecker for decls and modules and stuff +-------------------------------------------------------- + +-- | Typecheck a collection of modules. Assumes that each module +-- appears after its dependencies. Returns the same list of modules +-- with each definition typechecked +tcModules :: [Module] -> TcMonad [Module] +tcModules mods = foldM tcM [] mods + -- Check module m against modules in defs, then add m to the list. + where defs `tcM` m = do -- "M" is for "Module" not "monad" + let name = moduleName m + liftIO $ putStrLn $ "Checking module " ++ show name + m' <- defs `tcModule` m + return $ defs++[m'] + +-- | Typecheck an entire module. +tcModule :: [Module] -- ^ List of already checked modules (including their Decls). + -> Module -- ^ Module to check. + -> TcMonad Module -- ^ The same module with all Decls checked and elaborated. +tcModule defs m' = do checkedEntries <- extendCtxMods importedModules $ + foldr tcE (return []) + (moduleEntries m') + return $ m' { moduleEntries = checkedEntries } + where d `tcE` m = do + -- Extend the Env per the current Decl before checking + -- subsequent Decls. + x <- tcEntry d + case x of + AddHint hint -> extendHints hint m + -- Add decls to the Decls to be returned + AddCtx decls -> (decls++) <$> (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. +data HintOrCtx = AddHint Hint + | AddCtx [Decl] + +-- | Check each sort of declaration in a module +tcEntry :: Decl -> TcMonad HintOrCtx +tcEntry (Def n term) = do + oldDef <- lookupDef n + case oldDef of + Nothing -> tc + Just term' -> die term' + where + tc = do + lkup <- lookupHint n + case lkup of + Nothing -> do (aterm, ty) <- inferType term + return $ AddCtx [Sig n ty, Def n aterm] + Just ty -> + let handler (Err ps msg) = throwError $ Err (ps) (msg $$ msg') + msg' = disp [DS "When checking the term ", DD term, + DS "against the signature", DD ty] + in do + (eterm, ety) <- extendCtx (Sig n ty) $ + checkType term ty `catchError` handler + -- Put the elaborated version of term into the context. + if (n `elem` toListOf fv eterm) then + return $ AddCtx [Sig n ety, RecDef n eterm] + else + return $ AddCtx [Sig n ety, Def n eterm] + die term' = + extendSourceLocation (unPosFlaky term) term $ + err [DS "Multiple definitions of", DD n, + DS "Previous definition was", DD term'] + +tcEntry (Sig n ty) = do + duplicateTypeBindingCheck n ty + ety <- tcType ty + return $ AddHint (Hint n ety) + +-- rule Decl_data +tcEntry (Data t delta cs) = + do -- Check that the telescope for the datatype definition is well-formed + edelta <- tcTypeTele delta + ---- check that the telescope provided + --- for each data constructor is wellfomed, and elaborate them + let elabConstructorDef defn@(ConstructorDef pos d tele) = + extendSourceLocation pos defn $ + extendCtx (DataSig t edelta) $ + extendCtxTele edelta $ do + etele <- tcTypeTele tele + return (ConstructorDef pos d etele) + ecs <- mapM elabConstructorDef cs + -- Implicitly, we expect the constructors to actually be different... + let cnames = map (\(ConstructorDef _ c _) -> c) cs + unless (length cnames == length (nub cnames)) $ + 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 edelta ecs] +tcEntry (DataSig _ _ ) = err [DS "internal construct"] +tcEntry (RecDef _ _ ) = 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 :: TName -> Term -> TcMonad () +duplicateTypeBindingCheck n ty = do + -- Look for existing type bindings ... + l <- lookupTyMaybe n + l' <- 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. + ty':_ -> + let (Pos p _) = ty + msg = [DS "Duplicate type signature ", DD ty, + DS "for name ", DD n, + DS "Previous typing was", DD ty'] + in + extendSourceLocation p ty $ err msg + +----------------------------------------------------------- +-- Checking that pattern matching is exhaustive +----------------------------------------------------------- + +-- | Given a particular type and a list of patterns, make +-- sure that the patterns cover all potential cases for that +-- type. +-- If the list of patterns starts with a variable, then it doesn't +-- matter what the type is, the variable is exhaustive. (This code +-- does not report unreachable patterns.) +-- Otherwise, the scrutinee type must be a type constructor, so the +-- code looks up the data constructors for that type and makes sure that +-- there are patterns for each one. +exhaustivityCheck :: Term -> Type -> [Pattern] -> TcMonad () +exhaustivityCheck scrut ty (PatVar x:_) = return () +exhaustivityCheck scrut ty pats = do + (tcon, tys) <- ensureTCon ty + (delta,mdefs) <- lookupTCon tcon + case mdefs of + Just datacons -> loop pats datacons + where + loop [] [] = return () + loop [] dcons = do + l <- checkImpossible dcons + if null l then return () + else err $ [DS "Missing case for "] ++ map DD l + loop ((PatVar x):_) dcons = return () + loop ((PatCon dc args):pats') dcons = do + (cd@(ConstructorDef _ _ tele, dcons')) <- removeDcon dc dcons + tele' <- substTele delta tys tele + let (aargs, pats'') = relatedPats dc pats' + checkSubPats dc tele' (args:aargs) + loop pats'' dcons' + + -- make sure that the given list of constructors is impossible + -- in the current environment + checkImpossible :: [ConstructorDef] -> TcMonad [DCName] + checkImpossible [] = return [] + checkImpossible cd@(ConstructorDef _ dc tele : rest) = do + this <- (do + tele' <- substTele delta tys tele + _ <- tcTypeTele tele' + return [dc]) `catchError` (\_ -> return []) + others <- checkImpossible rest + return (this ++ others) + + Nothing -> + err [DS "Cannot determine constructors of", DD ty] + + +-- this could be because the scrutinee is not unifiable with the pattern +-- or because the constraints on the pattern are not satisfiable + + + + +-- | Given a particular data constructor name and a list of data +-- constructor definitions, pull the definition out of the list and +-- return it paired with the remainder of the list. +removeDcon :: DCName -> [ConstructorDef] -> + TcMonad (ConstructorDef, [ConstructorDef]) +removeDcon dc (cd@(ConstructorDef _ dc' _):rest) | dc == dc' = + return (cd, rest) +removeDcon dc (cd1:rest) = do + (cd2, rr) <- removeDcon dc rest + return (cd2, cd1:rr) +removeDcon dc [] = err [DS $ "Internal error: Can't find" ++ show dc] + +-- | Given a particular data constructor name and a list of patterns, +-- pull out the subpatterns that occur as arguments to that data +-- constructor and return them paired with the remaining patterns. +relatedPats :: DCName -> [Pattern] -> ([[(Pattern,Epsilon)]], [Pattern]) +relatedPats dc [] = ([],[]) +relatedPats dc ((PatCon dc' args):pats) | dc == dc' = + let (aargs, rest) = relatedPats dc pats in + (args:aargs, rest) +relatedPats dc (pc@(PatCon _ _):pats) = + let (aargs, rest) = relatedPats dc pats in + (aargs, pc:rest) +relatedPats dc (pc@(PatVar _):pats) = ([], pc:pats) + +-- | Occurs check for the subpatterns of a data constructor. Given +-- the telescope specifying the types of the arguments, plus the +-- subpatterns identified by relatedPats, check that they are each +-- exhaustive. + +-- for simplicity, this function requires that all subpatterns +-- are pattern variables. +checkSubPats :: DCName -> Telescope -> [[(Pattern,Epsilon)]] -> TcMonad () +checkSubPats dc Empty _ = return () +checkSubPats dc (Constraint _ _ tele) patss = checkSubPats dc tele patss +checkSubPats dc (Cons _ name tyP tele) patss + | length patss > 0 && (all ((> 0) . length) patss) = do + let hds = map (fst . head) patss + let tls = map tail patss + case hds of + (PatVar _ : []) -> checkSubPats dc tele tls + _ -> err [DS "All subpatterns must be variables in this version."] +checkSubPats dc t ps = + err [DS "Internal error in checkSubPats", DD dc, DD t, DS (show ps)] + + +