diff options
| -rw-r--r-- | src/Eval.hs | 54 | ||||
| -rw-r--r-- | src/Helper.hs | 28 | ||||
| -rw-r--r-- | src/Parser.hs | 59 | ||||
| -rw-r--r-- | src/Typer.hs | 45 |
4 files changed, 152 insertions, 34 deletions
diff --git a/src/Eval.hs b/src/Eval.hs index f6974de..6cf1fb8 100644 --- a/src/Eval.hs +++ b/src/Eval.hs @@ -13,7 +13,6 @@ import Data.List import qualified Data.Map as M import Data.Maybe import Helper --- import Inet ( reduce ) import Parser import Paths_bruijn import Reducer @@ -24,6 +23,7 @@ import System.FilePath.Posix ( takeBaseName ) import Text.Megaparsec hiding ( State , try ) +import Typer data EnvState = EnvState { _env :: Environment @@ -67,8 +67,8 @@ loadFile path conf cache = do evalFun :: Identifier -> Environment -> EvalState (Failable Expression) evalFun fun (Environment sub) = state $ \env@(Environment e) -> let lookup' env' = case M.lookup fun env' of - Nothing -> Left $ UndefinedIdentifier fun - Just (EnvDef { _exp = x }) -> Right x + Nothing -> Left $ UndefinedIdentifier fun + Just (EnvDef { _exp = x, _type = t }) -> Right $ TypedExpression t x matching n | null e = "<no idea>" | otherwise = snd $ minimumBy (compare `on` fst) $ map @@ -122,26 +122,38 @@ evalMixfix m sub = resolve (mixfixKind m) mixfixArgs evalPrefix :: Identifier -> Expression -> Environment -> EvalState (Failable Expression) +-- IDEA: typing and reduce if all arguments are fulfilled +-- evalPrefix (PrefixFunction "⊩") e sub = evalExp e sub >>= \case +-- Left e' -> pure $ Left e' +-- Right e' -> pure $ Right $ reduce e' +-- evalPrefix p e sub = evalExp (Application (Function p) e) sub evalPrefix p e = evalExp $ Application (Function p) e evalExp :: Expression -> Environment -> EvalState (Failable Expression) -evalExp idx@(Bruijn _ ) = const $ pure $ Right idx -evalExp ( Function fun) = evalFun fun -evalExp ( Abstraction e ) = evalAbs e -evalExp ( Application f g) = evalApp f g -evalExp ( MixfixChain es ) = evalMixfix es -evalExp ( Prefix p e ) = evalPrefix p e +evalExp idx@(Bruijn _ ) = const $ pure $ Right idx +evalExp ( Function fun ) = evalFun fun +evalExp ( Abstraction e ) = evalAbs e +evalExp ( Application f g ) = evalApp f g +evalExp ( MixfixChain es ) = evalMixfix es +evalExp ( Prefix p e) = evalPrefix p e +evalExp ( TypedExpression t e) = error "invalid" evalDefinition - :: Identifier -> Expression -> Environment -> EvalState (Failable Expression) -evalDefinition i e sub = evalExp e sub >>= \case - Left e' -> pure $ Left e' - Right f -> - modify - (\(Environment s) -> Environment - $ M.insert i (EnvDef f (Environment M.empty) defaultFlags) s - ) - >> pure (Right f) + :: Identifier + -> Expression + -> Type + -> Environment + -> EvalState (Failable Expression) +evalDefinition i e t sub = evalExp e sub >>= \case + Left e' -> pure $ Left e' + Right f -> case typeCheck f t of + err@(Left _) -> pure err + Right f' -> + modify + (\(Environment s) -> Environment + $ M.insert i (EnvDef f' t (Environment M.empty) defaultFlags) s + ) + >> pure (Right f) evalTest :: Expression -> Expression -> Environment -> EvalState (Failable Command) @@ -262,9 +274,9 @@ evalInstruction :: Instruction -> EnvState -> (EnvState -> IO EnvState) -> IO EnvState evalInstruction (ContextualInstruction instr inp) s@(EnvState env conf _) rec = case instr of - Define i e sub -> do - EnvState subEnv _ _ <- evalSubEnv sub s - ( res , env') <- pure $ evalDefinition i e subEnv `runState` env + Define i e t sub -> do + EnvState subEnv _ _ <- evalSubEnv sub s + (res, env') <- pure $ evalDefinition i e t subEnv `runState` env case res of Left err -> print (ContextualError err $ Context inp $ _nicePath conf) >> pure s -- don't continue diff --git a/src/Helper.hs b/src/Helper.hs index 87ae8fc..9c3df50 100644 --- a/src/Helper.hs +++ b/src/Helper.hs @@ -30,7 +30,7 @@ printContext (Context inp path) = p $ lines inp inText = "\ESC[104m\ESC[30min\ESC[0m " nearText = "\ESC[105m\ESC[30mnear\ESC[0m\n" p [] = withinText <> show path <> "\n" - p [l] = inText <> show l <> "\n" <> withinText <> show path <> "\n" + p [l] = inText <> l <> "\n" <> withinText <> path <> "\n" p (l : ls) = (p [l]) <> nearText @@ -39,7 +39,7 @@ printContext (Context inp path) = p $ lines inp errPrefix :: String errPrefix = "\ESC[101m\ESC[30mERROR\ESC[0m " -data Error = SyntaxError String | UndefinedIdentifier Identifier | UnmatchedMixfix [MixfixIdentifierKind] [Mixfix] | InvalidIndex Int | FailedTest Expression Expression Expression Expression | ContextualError Error Context | SuggestSolution Error String | ImportError String +data Error = SyntaxError String | UndefinedIdentifier Identifier | UnmatchedMixfix [MixfixIdentifierKind] [Mixfix] | InvalidIndex Int | FailedTest Expression Expression Expression Expression | ContextualError Error Context | SuggestSolution Error String | ImportError String | TypeError [Type] instance Show Error where show (ContextualError err ctx) = show err <> "\n" <> (printContext ctx) show (SuggestSolution err sol) = @@ -68,6 +68,8 @@ instance Show Error where <> " = " <> show red2 show (ImportError path) = errPrefix <> "invalid import " <> show path + show (TypeError ts) = + errPrefix <> "couldn't match types " <> intercalate " and " (map show ts) type Failable = Either Error -- Modified from megaparsec's errorBundlePretty @@ -126,7 +128,7 @@ instance Show Mixfix where show (MixfixOperator i) = show i show (MixfixExpression e) = show e -- TODO: Remove Application and replace with Chain (renaming of MixfixChain) -data Expression = Bruijn Int | Function Identifier | Abstraction Expression | Application Expression Expression | MixfixChain [Mixfix] | Prefix Identifier Expression +data Expression = Bruijn Int | Function Identifier | Abstraction Expression | Application Expression Expression | MixfixChain [Mixfix] | Prefix Identifier Expression | TypedExpression Type Expression deriving (Ord, Eq) instance Show Expression where show (Bruijn x ) = "\ESC[91m" <> show x <> "\ESC[0m" @@ -136,10 +138,25 @@ instance Show Expression where "\ESC[33m(\ESC[0m" <> show exp1 <> " " <> show exp2 <> "\ESC[33m)\ESC[0m" show (MixfixChain ms) = "\ESC[33m(\ESC[0m" <> (intercalate " " $ map show ms) <> "\ESC[33m)\ESC[0m" - show (Prefix p e) = show p <> " " <> show e + show (Prefix p e) = show p <> " " <> show e + show (TypedExpression t e) = show e <> " ⧗ " <> show t data Command = Input String | Import String String | Test Expression Expression deriving (Show) -data Instruction = Define Identifier Expression [Instruction] | Evaluate Expression | Comment | Commands [Command] | ContextualInstruction Instruction String +data Type = AnyType | PolymorphicType String | NormalType String | ConstructorType String [Type] | FunctionType [Type] + deriving (Ord, Eq) +instance Show Type where + show AnyType = "\ESC[33mAny\ESC[0m" + show (PolymorphicType n) = "\ESC[36m" <> n <> "\ESC[0m" + show (NormalType n) = "\ESC[95m" <> n <> "\ESC[0m" + show (ConstructorType n ts) = + "(" + <> "\ESC[95m" + <> n + <> "\ESC[0m" + <> (intercalate " " (map show ts)) + <> ")" + show (FunctionType ts) = "(" <> (intercalate " → " (map show ts)) <> ")" +data Instruction = Define Identifier Expression Type [Instruction] | Evaluate Expression | Comment | Commands [Command] | ContextualInstruction Instruction String deriving (Show) data EvalConf = EvalConf @@ -154,6 +171,7 @@ data ExpFlags = ExpFlags deriving Show data EnvDef = EnvDef { _exp :: Expression + , _type :: Type , _sub :: Environment , _flags :: ExpFlags } diff --git a/src/Parser.hs b/src/Parser.hs index af9aa70..b65a59e 100644 --- a/src/Parser.hs +++ b/src/Parser.hs @@ -85,6 +85,12 @@ identifier = namespace :: Parser String namespace = (:) <$> upperChar <*> many letterChar <?> "namespace" +typeIdentifier :: Parser String +typeIdentifier = (:) <$> upperChar <*> many letterChar <?> "type" + +polymorphicTypeIdentifier :: Parser String +polymorphicTypeIdentifier = many lowerChar <?> "polymorphic type" + dottedNamespace :: Parser String dottedNamespace = (\n d -> n ++ [d]) <$> namespace <*> char '.' @@ -148,7 +154,7 @@ parseFunction = do parseMixfix :: Parser Expression parseMixfix = do - s <- sepBy1 + s <- sepEndBy1 ( try prefixAsMixfix <|> try prefixOperatorAsMixfix <|> try operatorAsMixfix @@ -191,46 +197,83 @@ parseEvaluate = do e <- parseExpression pure $ ContextualInstruction (Evaluate e) inp +parseFunctionType :: Parser Type +parseFunctionType = + (FunctionType <$> sepBy1 parseTypeSingleton (sc *> char '→' <* sc)) + <?> "function type" + +parseConstructorType :: Parser Type +parseConstructorType = do + i <- typeIdentifier + sc + is <- sepBy1 parseTypeSingleton sc + (pure $ ConstructorType i is) <?> "constructor type" + +parseTypeIdentifier :: Parser Type +parseTypeIdentifier = NormalType <$> typeIdentifier <?> "type identifier" + +parsePolymorphicTypeIdentifier :: Parser Type +parsePolymorphicTypeIdentifier = + PolymorphicType + <$> polymorphicTypeIdentifier + <?> "polymorphic type identifier" + +parseTypeSingleton :: Parser Type +parseTypeSingleton = + try (parens parseFunctionType) + <|> try (parens parseConstructorType) + <|> try parseTypeIdentifier + <|> try parsePolymorphicTypeIdentifier + +parseTypeExpression :: Parser Type +parseTypeExpression = parseFunctionType <?> "type expression" + +parseDefineType :: Parser Type +parseDefineType = do + (try $ char '⧗' <* sc *> parseTypeExpression) <|> (return AnyType) + parseDefine :: Int -> Parser Instruction parseDefine lvl = do inp <- getInput var <- defIdentifier sc e <- parseExpression + t <- parseDefineType subs <- (try $ newline *> (many (parseBlock (lvl + 1)))) <|> (try eof >> return []) - pure $ ContextualInstruction (Define var e subs) inp + pure $ ContextualInstruction (Define var e t subs) inp parseReplDefine :: Parser Instruction parseReplDefine = do inp <- getInput var <- defIdentifier - _ <- string " = " + _ <- sc *> char '=' <* sc e <- parseExpression - pure $ ContextualInstruction (Define var e []) inp + t <- parseDefineType + pure $ ContextualInstruction (Define var e t []) inp parseComment :: Parser () parseComment = do - _ <- string "# " <?> "comment" + _ <- char '#' <* sc <?> "comment" _ <- some $ noneOf "\r\n" return () parseImport :: Parser Command parseImport = do - _ <- string ":import " <?> "import instruction" + _ <- string ":import" <* sc <?> "import instruction" path <- importPath ns <- (try $ (sc *> (namespace <|> string "."))) <|> (eof >> return "") pure (Import (path ++ ".bruijn") ns) parseInput :: Parser Command parseInput = do - _ <- string ":input " <?> "input instruction" + _ <- string ":input" <* sc <?> "input instruction" path <- importPath pure (Input $ path ++ ".bruijn") parseTest :: Parser Command parseTest = do - _ <- string ":test " <?> "test" + _ <- string ":test" <* sc <?> "test" e1 <- (parens parseExpression <?> "first expression") sc e2 <- (parens parseExpression <?> "second expression") diff --git a/src/Typer.hs b/src/Typer.hs new file mode 100644 index 0000000..0de01dd --- /dev/null +++ b/src/Typer.hs @@ -0,0 +1,45 @@ +module Typer + ( typeCheck + ) where + +import Helper + +-- removes ys from start of xs +dropList :: (Eq a) => [a] -> [a] -> [a] +dropList [] _ = [] +dropList xs [] = xs +dropList e@(x : xs) (y : ys) | x == y = dropList xs ys + | otherwise = e + +typeMatches :: Type -> Type -> Bool +typeMatches AnyType _ = True +typeMatches _ AnyType = True +typeMatches a b = a == b + +typeApply :: Type -> Type -> Type +typeApply (FunctionType ts1) (FunctionType ts2) = + FunctionType $ dropList ts1 ts2 +typeApply AnyType _ = AnyType +typeApply _ AnyType = AnyType +typeApply a b = error "invalid" + +typeImply :: Expression -> Type +typeImply (Bruijn _ ) = AnyType +typeImply (Abstraction e ) = typeImply e +typeImply (Application e1 e2) = typeApply (typeImply e1) (typeImply e2) +typeImply (TypedExpression t _ ) = t +typeImply _ = error "invalid" + +typeCheck :: Expression -> Type -> Failable Expression +typeCheck e@(Bruijn _) _ = Right e +typeCheck e@(Function _) _ = error "invalid" +typeCheck e@(Abstraction e') (FunctionType (t : ts)) = + typeCheck e' (FunctionType ts) >>= pure (Right e) +typeCheck e@(Abstraction _) _ = Right e +typeCheck e@(Application e1 e2) t + | typeMatches (typeImply e) t = Right e + | otherwise = Left $ TypeError [(typeImply e1), (typeImply e2), t] +typeCheck e@(MixfixChain _) _ = Right e +typeCheck e@(Prefix _ _ ) _ = Right e +typeCheck (TypedExpression t' e) t | typeMatches t' t = Right e + | otherwise = Left $ TypeError [t', t] |