diff options
Diffstat (limited to 'src')
| -rw-r--r-- | src/AST.hs | 9 | ||||
| -rw-r--r-- | src/Parser.hs | 138 | ||||
| -rw-r--r-- | src/TypeCheck.hs | 64 |
3 files changed, 185 insertions, 26 deletions
@@ -22,6 +22,8 @@ data Term | TIMax Term Term -- ^ Maximum of two levels | TISucc Term -- ^ Level + 1 + | TAnnot (OfType Term Term) -- ^ term : type + -- Temporary stuff until we have proper inductive types: | TOne -- ^ The unit type | TUnit -- ^ The element of the unit type @@ -31,4 +33,11 @@ data Term | TProj2 Term -- ^ Second projection of a dependent pair deriving (Show) +data Definition = Definition Name (OfType Term Term) + deriving (Show) + type Env = Map Name Term + +data OfType a b = a :| b + deriving (Show) +infix 1 :| diff --git a/src/Parser.hs b/src/Parser.hs new file mode 100644 index 0000000..7464d85 --- /dev/null +++ b/src/Parser.hs @@ -0,0 +1,138 @@ +module Parser (parseProgram) where + +import Control.Monad +import Data.Char +import Data.List (foldl') +import Text.Parsec hiding (token) +import Text.Parsec.Expr + +import AST + + +type Parser = Parsec String () + +parseProgram :: String -> String -> Either ParseError [Definition] +parseProgram fname source = parse pProgram fname source + +pProgram :: Parser [Definition] +pProgram = do + whitespaceTo0 + choice + [eof >> return [] + ,(:) <$> pDef <*> pProgram] + +-- | Assumes column 0 +pDef :: Parser Definition +pDef = do + name <- pName + whitespace + token ":" + whitespace + typ <- pTerm + whitespaceTo0 + name2 <- pName + when (name /= name2) $ + fail $ "Definition of '" ++ name ++ "' followed by definition for '" ++ name2 ++ "'" + whitespace + token "=" + whitespace + rhs <- pTerm + return (Definition name (rhs :| typ)) + +pTerm :: Parser Term +pTerm = buildExpressionParser optable pTermEAtom + where + optable = + [[Infix (token "->" >> return makePi) AssocRight + ,Infix (token "→" >> return makePi) AssocRight] + ,[Infix (token ":" >> return (\a b -> TAnnot (a :| b))) AssocNone]] + +makePi :: Term -> Term -> Term +makePi (TAnnot (TVar x :| ty1)) ty2 = TPi x ty1 ty2 +makePi ty1 ty2 = TPi ";_" ty1 ty2 + +pTermEAtom :: Parser Term +pTermEAtom = pLambda <|> pApp + +pLambda :: Parser Term +pLambda = do + token "\\" <|> token "λ" + whitespace + _ <- char '(' + whitespace + x <- pName + whitespace + token ":" + whitespace + ty <- pTerm + whitespace + _ <- char ')' + whitespace + token "->" + rhs <- pTerm + return (TLam x ty rhs) + +pApp :: Parser Term +pApp = do + e1 <- pAtom + args <- many (try (whitespace >> pTerm)) + return (foldl' TApp e1 args) + +pAtom :: Parser Term +pAtom = choice + [do _ <- char '(' + whitespace + e <- pTerm + whitespace + _ <- char ')' + return e + ,TVar <$> pName] + +TODO TPair, TSigma ("%"). The rest are environment entries. + +pName :: Parser Name +pName = do + name <- many1 pNameChar + guard (name `notElem` keywords) + return name + where + keywords = ["=", "->", "→", ":", "?", "\\", "λ", "∀", "..", "..." + ,"%" -- for Sigma; hopefully temporary + ,"forall", "data", "import", "in", "let"] + +pNameChar :: Parser Char +pNameChar = satisfy (\c -> not (isSpace c) && c `notElem` ".;{}()@\"") + +inlineWhite :: Parser () +inlineWhite = do + spaces + choice + [inlineComment + -- TODO: nested {- -} comments + ,return ()] + +inlineComment :: Parser () +inlineComment = token "--" >> manyTill anyChar newline >> return () + +-- | Skips to the furthest point from here that can be reached without +-- consuming any tokens, and without ending on column 0. +whitespace :: Parser () +whitespace = do + inlineWhite + optional $ + many newline >> (void space <|> inlineComment) >> whitespace + +-- | Skips as much whitespace as possible, and throws an error if that doesn't +-- leave us on column 0. +whitespaceTo0 :: Parser () +whitespaceTo0 = do + inlineWhite + choice + [eof + ,newline >> whitespaceTo0 + ,do pos <- getPosition + when (sourceColumn pos /= 1) $ + unexpected "indented code"] + +token :: String -> Parser () +token s = try $ string s >> (eof <|> void (lookAhead (satisfy (\c -> isSpace c || c `elem` ".;{}()@\"")))) diff --git a/src/TypeCheck.hs b/src/TypeCheck.hs index 4c05c4b..1406a67 100644 --- a/src/TypeCheck.hs +++ b/src/TypeCheck.hs @@ -3,22 +3,37 @@ {-# LANGUAGE DeriveFunctor #-} {-# LANGUAGE GeneralizedNewtypeDeriving #-} {-# LANGUAGE DeriveFoldable #-} -module TypeCheck where +module TypeCheck (typeCheck, typeInfer) where import Control.Monad -import Control.Monad.Trans.Class -import Control.Monad.Trans.State.Strict -import Control.Monad.Trans.Writer.CPS -import Data.Foldable (toList) -import Data.Map.Strict (Map) +-- import Control.Monad.Trans.Class +-- import Control.Monad.Trans.State.Strict +-- import Control.Monad.Trans.Writer.CPS +-- import Data.Foldable (toList) +-- import Data.Map.Strict (Map) import qualified Data.Map.Strict as Map -import Numeric.Natural +-- import Numeric.Natural import AST +typeCheck :: Env -> Term -> Term -> Either String Term +typeCheck env typ term = + runTM (check env term typ) + -- runTM (check env term typ) >>= \case + -- ([], term') -> return term' + -- (_, _) -> error "Don't know how to solve constraints yet" + +typeInfer :: Env -> Term -> Either String (OfType Term Term) +typeInfer env term = + runTM (infer env term) + -- runTM (infer env term) >>= \case + -- ([], jud) -> return jud + -- (_, _) -> error "Don't know how to solve constraints yet" + + -- | type checking monad -newtype TM a = TM (WriterT (Bag Constr) (StateT Natural (Either String)) a) +newtype TM a = TM ({- WriterT (Bag Constr) (StateT Natural ( -} Either String {- )) -} a) deriving stock (Functor) deriving newtype (Applicative, Monad) @@ -31,28 +46,23 @@ data Constr = VarEq Name Term | LevelLeq Term Term deriving (Show) -type Subst = Map Name Term - -runTM :: TM a -> Either String ([Constr], a) -runTM (TM m) = do - (res, cs) <- evalStateT (runWriterT m) 0 - return (toList cs, res) +runTM :: TM a -> Either String a +runTM (TM m) = m + -- (res, cs) <- evalStateT (runWriterT m) 0 + -- return (toList cs, res) -genId :: TM Natural -genId = TM (lift (state (\i -> (i, i + 1)))) +-- genId :: TM Natural +-- genId = TM (lift (state (\i -> (i, i + 1)))) -genName :: TM Name -genName = ("." ++) . show <$> genId +-- genName :: TM Name +-- genName = ("." ++) . show <$> genId throw :: String -> TM a -throw err = TM (lift (lift (Left err))) +-- throw err = TM (lift (lift (Left err))) +throw err = TM (Left err) -emit :: Constr -> TM () -emit c = TM (tell (BOne c)) - -data OfType a b = a :| b - deriving stock (Show) -infix 1 :| +-- emit :: Constr -> TM () +-- emit c = TM (tell (BOne c)) check :: Env -> Term -> Term -> TM Term check env topTerm typ = case topTerm of @@ -151,8 +161,10 @@ infer env = \case TSigma x a b -> do inferW env a >>= \case a' :| TSet lvlA -> do - inferW env b >>= \case + inferW (Map.insert x a' env) b >>= \case b' :| TSet lvlB -> do + when (x `freeIn` lvlB) $ + throw $ "Variable " ++ show x ++ " escapes Sigma" return (TSigma x a' b' :| TSet (TIMax lvlA lvlB)) _ :| tb -> throw $ "RHS of a Sigma not of type Set i, but: " ++ show tb _ :| ta -> throw $ "LHS type of a Sigma not of type Set i, but: " ++ show ta |