pi-forall (empty) → 0.1.1
raw patch · 7 files changed
+2101/−0 lines, 7 filesdep +HUnitdep +QuickCheckdep +arraysetup-changed
Dependencies added: HUnit, QuickCheck, array, base, containers, directory, filepath, mtl, parsec, pretty, transformers, unbound-generics
Files
- LICENSE +24/−0
- Setup.hs +2/−0
- pi-forall.cabal +54/−0
- src/Main.hs +106/−0
- src/Parser.hs +669/−0
- src/Syntax.hs +399/−0
- src/TypeCheck.hs +847/−0
+ LICENSE view
@@ -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.
+ Setup.hs view
@@ -0,0 +1,2 @@+import Distribution.Simple+main = defaultMain
+ pi-forall.cabal view
@@ -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 <sweirich@cis.upenn.edu>, based on code by Trellys Team <trellys@...>+Maintainer: Stephanie Weirich <sweirich@cis.upenn.edu>+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++
+ src/Main.hs view
@@ -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 <filename>' 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+
+ src/Parser.hs view
@@ -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}) [] "<interactive>" 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 (<expr> := <expr> <expr>) 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))+ +
+ src/Syntax.hs view
@@ -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+
+ src/TypeCheck.hs view
@@ -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)] + ++