Browse Source

check in a bunch of files

Some of these are potentially not needed--I need to go through the
imports to check.
main
scottolsen 6 months ago
parent
commit
3726e0f7e0
  1. 27
      Rose/Data/Function.idr
  2. 34
      Rose/Data/Let.idr
  3. 16
      Rose/Data/Macro.idr
  4. 17
      Rose/Data/Match.idr
  5. 17
      Rose/Inference.idr
  6. 32
      Rose/Parser/Core.idr
  7. 155
      Rose/Parser/Forms.idr
  8. 111
      Rose/Parser/Literal.idr
  9. 23
      Rose/Parser/Test/Literal.idr
  10. 27
      Rose/Testing.idr
  11. 11
      Rose/Typed.idr

27
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))

34
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

16
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))

17
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

17
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

32
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

155
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

111
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)

23
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")]

27
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")

11
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
Loading…
Cancel
Save