From 3726e0f7e0f6afb817b23a566397329e13d10184 Mon Sep 17 00:00:00 2001 From: scottolsen Date: Wed, 24 Nov 2021 14:48:38 -0500 Subject: [PATCH] check in a bunch of files Some of these are potentially not needed--I need to go through the imports to check. --- Rose/Data/Function.idr | 27 ++++++ Rose/Data/Let.idr | 34 ++++++++ Rose/Data/Macro.idr | 16 ++++ Rose/Data/Match.idr | 17 ++++ Rose/Inference.idr | 17 ++++ Rose/Parser/Core.idr | 32 ++++++++ Rose/Parser/Forms.idr | 155 +++++++++++++++++++++++++++++++++++ Rose/Parser/Literal.idr | 111 +++++++++++++++++++++++++ Rose/Parser/Test/Literal.idr | 23 ++++++ Rose/Testing.idr | 27 ++++++ Rose/Typed.idr | 11 +++ 11 files changed, 470 insertions(+) create mode 100644 Rose/Data/Function.idr create mode 100644 Rose/Data/Let.idr create mode 100644 Rose/Data/Macro.idr create mode 100644 Rose/Data/Match.idr create mode 100644 Rose/Inference.idr create mode 100644 Rose/Parser/Core.idr create mode 100644 Rose/Parser/Forms.idr create mode 100644 Rose/Parser/Literal.idr create mode 100644 Rose/Parser/Test/Literal.idr create mode 100644 Rose/Testing.idr create mode 100644 Rose/Typed.idr diff --git a/Rose/Data/Function.idr b/Rose/Data/Function.idr new file mode 100644 index 0000000..299db5b --- /dev/null +++ b/Rose/Data/Function.idr @@ -0,0 +1,27 @@ +module Rose.Data.Function + +import Data.Error +import Data.Atom +import Data.SExpression + +NonsymbolicArgumentsError : SE -> RoseError +NonsymbolicArgumentsError se = MkError $ "Functions can only have symbols as arguments: " ++ se + +FnError : SE -> RoseError +FnError se = MkError $ "The function: " ++ show se ++ "is invalid." + +data Fn : Type where + MkFn : List (SE Atomic) -> SE a -> Fn + InvalidFn : RoseError -> SE a -> Fn + +Interpreted Fn where + invalid = InvalidFn + + interpret (Expression (Expression (Atom (MkSymbol "fn")) Nil) (Expression args body)) = + if (any (not . isSymbol) args) + then invalid (NonSymbolicArgumentsError args) (Expression args body) + else MkFn (toList args) body + interpret se = invalid (FnError se) se + + expression (MkFn args body) = + (Expression (MkSymbol "fn") (Expression (fromList args) body)) diff --git a/Rose/Data/Let.idr b/Rose/Data/Let.idr new file mode 100644 index 0000000..1510ff4 --- /dev/null +++ b/Rose/Data/Let.idr @@ -0,0 +1,34 @@ +module Rose.Data.Let + +import Data.Error +import Data.Atom +import Data.SExpression +import Data.Form +import Util + +export +LetError : SE -> RoseError +LetError se = MkError $ "Invalid let form: " ++ show se + +export +UnevenBindingsError : SE -> RoseError +UnevenBindingsError se = MkError $ "Bindings must be even: " ++ show se + +export +data Let : Type where + MkLet : List SE -> List SE -> SE -> Let + InvalidLet : RoseError -> SE -> Let + +export +Interpreted Let where + interpret (Expression (MkAtom (MkSymbol "let")) (Expression bindings body)) = + if (mod (length (toList bindings)) 2) == 0 + then MkLet (evenPositions bindings) (oddPositions bindings) body + else InvalidLet (UnevenBindingsError bindings) (Expression (MkAtom (MkSymbol "let")) (Expression bindings body)) + interpret se = InvalidLet (LetError se) se + + expression (MkLet variables values body) = + (Expression (MkAtom (MkSymbol "let")) (Expression (fromList bindings) body)) + where bindings : List SE + bindings = foldr (++) [] $ zipWith (\x,y => x::y::[]) variables values + expression (InvalidLet _ se) = se diff --git a/Rose/Data/Macro.idr b/Rose/Data/Macro.idr new file mode 100644 index 0000000..9e337f6 --- /dev/null +++ b/Rose/Data/Macro.idr @@ -0,0 +1,16 @@ +module Rose.Data.Macro + +import Data.SExpression + +data Macro : Type where + MkMacro : List SE -> SE -> Macro + +Interpreted Macro where + interpret (Expression args body) = + if (any (not . isSymbol) args) + then MkError "Improper function." + else MkMacro (toList args) body + interpret _ = MkError "Improper function." + + expression (MkMacro args body) = + (Expression (MkAtom (MkSymbol "macro")) (Expression (fromList args) body)) diff --git a/Rose/Data/Match.idr b/Rose/Data/Match.idr new file mode 100644 index 0000000..2ad26ce --- /dev/null +++ b/Rose/Data/Match.idr @@ -0,0 +1,17 @@ +module Rose.Data.Match + +import Data.SExpression +import Util + +data Match : Type where + MkMatch : List (List SE, SE) -> Match + +fromExpression : SE -> Match +-- ([x] (foo) [y] (bar)) +-- [(x), (foo), ...] +fromExpression e = + case toList e of + [] => MkMatch [] + xs => MkMatch $ zipper (evenPositions xs) (oddPositions xs) + where zipper : List SE -> List (List SE, SE) + zipper xs ys = zip (map toList xs) ys diff --git a/Rose/Inference.idr b/Rose/Inference.idr new file mode 100644 index 0000000..aadf27b --- /dev/null +++ b/Rose/Inference.idr @@ -0,0 +1,17 @@ +||| Type inference +module Inference + +TypeEnvironment : Type -> Type where + TypeEnv : r -> List (Int, r) + +interface (Base r) => Inferable + (t : Type) -- Representation of types + (v : Type) -- Type variables--should be a specialization over t + (m : Type -> Type -> Type) -- Container for type/variable associations + (e : Type -> Type) where -- Type environment + generate : (e (m v t)) -> v + extend : (e (m v t)) -> (m v t) -> (e (m v t)) + lookup : (e (m v t)) -> v -> Maybe t + substitute : (e (m v t)) -> t -> t + unify : t -> t -> (e (m v t)) -> Either String (e (m v t)) + free : v -> t -> (e (m v t)) -> Bool diff --git a/Rose/Parser/Core.idr b/Rose/Parser/Core.idr new file mode 100644 index 0000000..e78f0dc --- /dev/null +++ b/Rose/Parser/Core.idr @@ -0,0 +1,32 @@ +||| Core definitions for the rose language parser +module Rose.Parser.Core + +import Text.Lexer +import Text.Parser + +import Rose.Lexer + +infixl 6 + +||| Abstracts over our representation of tokens +public export +ParseToken : Type +ParseToken = (TokenData Token) + +||| Produces a Grammar that consumes a ParseToken +public export +Rule : Type -> Type +Rule ty = Grammar ParseToken True ty + +||| Alternative failure. +||| Helper combinator for failing with a message when the Grammar +||| `g` doesn't succeed. +export +() : Grammar tok c a -> String -> Grammar tok (c && c) a +g s = g <|> fail s + +export +Show (ParseError ParseToken) where + show (Error e (tok::rest)) = + "Parsing error: " ++ show tok ++ "\n\t" ++ e + diff --git a/Rose/Parser/Forms.idr b/Rose/Parser/Forms.idr new file mode 100644 index 0000000..aca4630 --- /dev/null +++ b/Rose/Parser/Forms.idr @@ -0,0 +1,155 @@ +||| Module Parser defines a parser for the Rose language. +module Rose.Parser + +import Text.Parser +import Text.Parser.Core +import Lexer +import Text.Lexer +import Data.Atom +import Data.SExpression +import Data.Form + +reservedWords : List String +reservedWords = ["let", "def", "macro", "fn", "where"] + +checkReserved : Rule SE -> Rule SE +checkReserved r = join $ pure isReserved <*> r + where isReserved : SE -> Grammar ParsedToken False SE + isReserved (MkAtom (MkSymbol name)) = if (not $ name `elem` reservedWords) + then pure $ MkAtom (MkSymbol name) + else (fail (ReservedWord name)) + isReserved x = pure x + ReservedWord : String -> String + ReservedWord word = + "The symbol " ++ word ++ " is reserved. Use a different symbol, such as x." + +reserved : String -> Rule SE +reserved s = terminal + (\x => case (tok x) of + (TkSymbol s') => if s == s' then (Just $ MkAtom (MkSymbol s)) else Nothing + _ => Nothing) + +manyEnclosed : Rule ty -> Rule (List ty) +manyEnclosed r = (lparen *> manyTill rparen r) + <|> (lbrack *> manyTill rbrack r) + +someEnclosed : Rule ty -> Rule (List ty) +someEnclosed r = (lparen *> someTill rparen r) + <|> (lbrack *> someTill rbrack r) + +enclosed : Grammar ParsedToken t ty -> Rule ty +enclosed r = + (between lbrack rbrack r) <|> (between lparen rparen r) + +mutual + ||| Let forms + ||| (let [binding value...] body) + export + lett : Rule SE + lett = + enclosed + $ reserved "let" + *> manyEnclosed bindings + >>= \bs => (atoms <|> expression) + >>= \body => pure $ fromList (bs ++ [body]) + where bindings : Rule SE + bindings = + checkReserved symbol + >>= \binding => (atoms <|> expression) UnevenLetBindings binding + >>= \value => pure $ (Expression binding value) + UnevenLetBindings : SE -> String + UnevenLetBindings binding = + "Uneven let bindings. Let bindings must contain an even number of names and values: (let [binding value] body)" + ++ "\n\t" + ++ "The binding " ++ show binding ++ " should be followed by a value or expression." + + ||| Where forms + ||| (where x (fn [] 2) + ||| y 2) + export + wheref : Rule SE + wheref = + lparen + *> reserved "where" + *> manyTill rparen bindings + >>= \bs => pure $ fromList bs + where bindings : Rule SE + bindings = + checkReserved symbol + >>= \name => (fn <|> macro <|> app <|> atoms) UnevenWhereBindings name + >>= \value => pure $ Expression name value + UnevenWhereBindings : SE -> String + UnevenWhereBindings binding = + "Uneven where bindings. Where bindings must contain an even number of names and values: (where binding value...)" + ++ "\n\t" + ++ "The binding " ++ show binding ++ " should be followed by a value or expression." + + ||| Anonymous macros + ||| (macro [x] foo) + export + macro : Rule SE + macro = + enclosed + $ reserved "macro" + *> pattern + where pattern : Rule SE + pattern = + pure fromList + <*> manyEnclosed (checkReserved atoms) MissingMacroArgList + >>= \args => (atoms <|> macro <|> expression) MissingMacroBody args + >>= \body => pure $ (Expression args body) + MissingMacroArgList : String + MissingMacroArgList = + "Expected a list of arguments or pattern matches." + ++ "\n\t" + ++ "Macros take an even number of argument lists and bodies." + MissingMacroBody : SE -> String + MissingMacroBody pat = + "Missing macro body. Macros must contain an argument list and function body: (macro [x] 1)" + ++ "\n\t" + ++ "The arguments " ++ show pat ++ " should be followed by a function body." + + app : Rule SE + app = + enclosed + $ (symbol <|> fn <|> macro) + >>= \f => many (atoms <|> expression) + >>= \args => pure $ Expression f (fromList args) + + ||| Anonymous functions + ||| (fn [0] 1 + ||| [n] (- n 1)) + export + fn : Rule SE + fn = + enclosed + $ reserved "fn" + *> many patterns + >>= \pats => pure $ fromList pats + where patterns = + manyEnclosed atoms + >>= \args => (atoms <|> lett <|> fn <|> app) InvalidFunctionBody args + >>= \body => pure $ (Expression (fromList args) body) + InvalidFunctionBody : (List SE) -> String + InvalidFunctionBody args = + "Invalid function body. Functions must contain an argument list and function body: (fn [x] 1)" + ++ "\n\t" + ++ "The arguments " ++ show args ++ " should be followed by a function body." + + export + def : Rule SE + def = + enclosed + $ reserved "def" + *> symbol + >>= \name => (atoms <|> expression) MissingDefinitionBody + >>= \body => pure $ Expression name body + where MissingDefinitionBody : String + MissingDefinitionBody = "Expected a definition body." + +||| A program is a list of s-expressions +export +program : Grammar ParsedToken False (List SE) +program = + manyTill eof list + diff --git a/Rose/Parser/Literal.idr b/Rose/Parser/Literal.idr new file mode 100644 index 0000000..fea1abf --- /dev/null +++ b/Rose/Parser/Literal.idr @@ -0,0 +1,111 @@ +||| Defines parsing rules for literals of the Rose language. +module Rose.Parser.Literal + +import Text.Parser +import Text.Parser.Core +import Text.Lexer + +import Rose.Lexer +import Rose.Parser.Core +import Rose.Data.Atom +import Rose.Data.SExpression +import Rose.Data.Form + +||| Parses a symbol token, returning the SE representation of the symbol. +export +symbol : Rule SE +symbol = (terminal + (\x => case (tok x) of + (TkSymbol s) => pure $ MkAtom (MkSymbol s) + _ => Nothing)) NotASymbol + where NotASymbol : String + NotASymbol = "Expected a symbol, such as x, y, or z." + +||| atoms is a rule for parsing atoms of the Rose language. +export total +atoms : Rule SE +atoms = terminal + (\x => untok (tok x)) NotAnAtom + where untok : Token -> Maybe SE + untok (TkNum i) = Just $ MkAtom (MkInteger i) + untok (TkChar c) = Just $ MkAtom (MkChar c) + untok (TkString s) = Just $ MkAtom (MkString s) + untok (TkSymbol s) = Just $ MkAtom (MkSymbol s) + untok (TkBool b) = Just $ MkAtom (MkBool b) + untok _ = Nothing + NotAnAtom : String + NotAnAtom = "Expected a value or symbol, such as 1, x, or \"foo\"." + +||| punct defines a punctuation rule for the Rose language. +||| Used to define rules for parens, brackets, etc. +export +punct : Token -> Rule () +punct t = terminal + (\x => if (tok x) == t + then Just () + else Nothing) NotPunctuation + where NotPunctuation : String + NotPunctuation = "Expected the start or close of a bracket or list, (, ), [, or, ]." + +||| Parses a left bracket. +export +lbrack : Rule () +lbrack = punct LBracket ExpectedLeftBracket + where ExpectedLeftBracket : String + ExpectedLeftBracket = "Expected [" +||| Parses a right bracket. +export +rbrack : Rule () +rbrack = punct RBracket ExpectedRightBracket + where ExpectedRightBracket : String + ExpectedRightBracket = "Expected ]" +||| Parses a left parentheses. +export +lparen : Rule () +lparen = punct LParen ExpectedLeftParenthesis + where ExpectedLeftParenthesis : String + ExpectedLeftParenthesis = "Expected (" +||| Parses a right parentheses. +export +rparen : Rule () +rparen = punct RParen ExpectedRightParenthesis + where ExpectedRightParenthesis : String + ExpectedRightParenthesis = "Expected )" + +||| Parses a finite list. +||| This function is required to parse lists within lists: +||| e.g. ((a b) c) +finite : Rule SE +finite = + (lparen <|> lbrack) + >>= \_ => many (atoms <|> finite) + >>= \result => (rparen <|> rbrack) + >>= \_ => pure $ fromList result + +mutual + ||| list is a rule for parsing lists in the Rose language + ||| (y . (x . ()) + export + list : Rule SE + list = + between lparen rparen + $ many (atoms <|> finite) + >>= \as => many (list <|> array) + >>= \rest => pure $ fromList (as ++ rest) + + ||| array is a rule for parsing 'arrays' in the Rose language + ||| [y . [x . []]] + ||| arrays and lists are alternative syntax for the same underlying form + ||| an s-expression. In Rose, brackets and parens may be used interchangeably. + export + array : Rule SE + array = + between lbrack rbrack + $ many (atoms <|> finite) >>= \as => many (list <|> array) + >>= \rest => pure $ fromList (as ++ rest) + +||| Parses an s-expression surrounded in either parentheses or brackets. +export +expression : Rule SE +expression = (list <|> array) + diff --git a/Rose/Parser/Test/Literal.idr b/Rose/Parser/Test/Literal.idr new file mode 100644 index 0000000..00a0344 --- /dev/null +++ b/Rose/Parser/Test/Literal.idr @@ -0,0 +1,23 @@ +module Rose.Parser.Test.Literal + +import Text.Parser +import Text.Lexer +import Test.Unit.Assertions + +import Rose.Testing +import Rose.Lexer +import Rose.Data.SExpression +import Rose.Parser.Core +import Rose.Parser.Literal + +tokenize : Token -> List ParseToken +tokenize = pure . MkToken 0 0 + +testSymbol : IO () +testSymbol = + runTest "testSymbol" + (testWith [parsesSymbol, doesNotParseAString] (map (parse symbol) examples)) + where parsesSymbol = assertWith "Parses a symbol?" assertRight + doesNotParseAString = assertWith "Doesn't parse a string?" assertLeft + examples : List (List ParseToken) + examples = map tokenize [(TkSymbol "foo"), (TkString "bar")] diff --git a/Rose/Testing.idr b/Rose/Testing.idr new file mode 100644 index 0000000..d356c7c --- /dev/null +++ b/Rose/Testing.idr @@ -0,0 +1,27 @@ +module Rose.Testing + +import Test.Unit.Display +import Test.Unit.Generic + +export +testWith : List (b -> c) -> List b -> List c +testWith = zipWith apply + +export +assertWith : String -> (a -> IO Bool) -> (a -> IO Bool) +assertWith s f = + (\x => putStr (s ++ "\t") + >>= \_ => f x + >>= \b => if b + then (putStrLn "passed\n" >>= \_ => pure b) + else (putStrLn "failed\n" >>= \_ => pure b)) + +export +runTest : String -> List (IO Bool) -> IO () +runTest name bs = + putStrLn (heading name) + >>= \_ => sequence bs + >>= pure . all (==True) + >>= \result => if result + then putStrLn (succLine ++ name ++ " passed") + else putStrLn (errLine ++ name ++ " failed") diff --git a/Rose/Typed.idr b/Rose/Typed.idr new file mode 100644 index 0000000..c3e572e --- /dev/null +++ b/Rose/Typed.idr @@ -0,0 +1,11 @@ +module Typed + +interface Typed (t : Type -> Type) where + int_ty : t Int + fn_ty : t a -> t b -> t (a -> b) + +data PrintableType : (a : Type) -> Type where + MkPrintableType : {a : Type} -> String -> PrintableType a + +viewType : PrintableType a -> String +viewType (MkPrintable s) = s