Browse Source

First commit

As of this inaugural commit, Rose is a dumb repl that supports some of
the lambda calculus and three basic arithmetic operations.

Of course, we also have a lexer, parser, and the underlying data
structures/types we need to represent s-expressions and evaluate lisp
forms.

Onward march from here!
main
scottolsen 2 years ago
commit
12109c8ea9
  1. 2
      .gitignore
  2. 4
      Makefile
  3. 3
      README.md
  4. 26
      Rose/Data/Atom.idr
  5. 11
      Rose/Data/Error.idr
  6. 68
      Rose/Data/Form.idr
  7. 127
      Rose/Data/SExpression.idr
  8. 80
      Rose/Evaluator.idr
  9. 63
      Rose/Lambda.idr
  10. 135
      Rose/Lexer.idr
  11. 86
      Rose/Parser.idr
  12. 61
      Rose/Primitives.idr
  13. 34
      Rose/Repl.idr
  14. 30
      rose.ipkg

2
.gitignore vendored

@ -0,0 +1,2 @@
*.ibc
out/

4
Makefile

@ -0,0 +1,4 @@
build:
idris --build rose.ipkg
mv rosie out/rose
idris --clean rose.ipkg

3
README.md

@ -0,0 +1,3 @@
# Rose
A statically typed, theorem-proving lisp.

26
Rose/Data/Atom.idr

@ -0,0 +1,26 @@
||| Module Atom defines a representation of atoms in the Rose language.
module Rose.Data.Atom
||| The type of Rose language atoms, integers, characters, strings, symbols;
||| effectively anything that is not Nil or an s-expression.
public export
data Atom : Type where
MkInteger : Integer -> Atom
MkString : String -> Atom
MkChar : Char -> Atom
MkSymbol : String -> Atom
export
Show Atom where
show (MkSymbol s) = s
show (MkString s) = show s
show (MkInteger s) = show s
show (MkChar s) = show s
export
Eq Atom where
(MkSymbol s) == (MkSymbol t) = s == t
(MkInteger s) == (MkInteger t) = s == t
(MkString s) == (MkString t) = s == t
(MkChar s) == (MkChar t) = s == t
_ == _ = False

11
Rose/Data/Error.idr

@ -0,0 +1,11 @@
||| Module Error contains a definition of errors for the Rose compiler.
module Rose.Data.Error
||| The type of Rose compiler errors.
public export
data RoseError : Type where
MkError : String -> RoseError
export
Show RoseError where
show (MkError e) = e

68
Rose/Data/Form.idr

@ -0,0 +1,68 @@
module Rose.Data.Form
import Data.SExpression
import Data.Error
||| Malformed expression generates an error for improperly formed s-expressions.
export
MalformedExpression : SE -> RoseError
MalformedExpression expr = MkError ("The expression: " ++ show expr ++ " is malformed.")
||| Form is a subtype of s-expression that are valid, that is:
||| Expressions that end with either:
||| Nil
||| An expression that terminates with Nil.
-- TODO: Make this a subtype of SE.
public export
Form : Type
Form = SE
||| fromList converts a list of s-expressions into an s-expression.
export total
fromList : List SE -> SE
fromList expressions = (foldr (<::>) neutral expressions)
||| toList converts an s-expression into a list of its component parts.
export total
toList : SE -> (List SE)
toList (Expression first rest) = first::toList rest
toList Nil = []
toList x = [x]
||| For well-formed expressions, Nil or (Expression _ Nil),
||| toList and fromList are inverses. That is, there is a partial mapping
||| from SE to (List SE).
--TODO: Make this total?
list_identity : (n : SE) -> n = (fromList (toList n))
list_identity Nil = Refl
list_identity (Expression x Nil) = Refl
||| Lambda generates an anonymous function or macro with `args` and `body`.
export
Lambda : String -> List SE -> SE -> Either RoseError Form
Lambda s args body =
if (any (not . isSymbol) args)
then Left $ MalformedExpression (fromList args)
else pure $ symbol s <::> (fromList args <::> (body <::> neutral))
||| Macro generates an anonymous macro
export total
Macro : List SE -> SE -> Either RoseError Form
Macro = Lambda "macro"
||| Macro generates an anonymous function
export total
Fn : List SE -> SE -> Either RoseError Form
Fn = Lambda "fn"
||| Apply generates an s-expression corresponding to function application.
export total
Apply : SE -> List SE -> Form
Apply f args = f <::> fromList args
||| Wrap nests an s-expression in a parent expression ending in Nil;
||| Wrap (a b) -> ((a b)).
export total
Wrap : SE -> Form
Wrap expr = expr <::> neutral

127
Rose/Data/SExpression.idr

@ -0,0 +1,127 @@
||| Module SExpression defines the representation of s-expressions in the Rose language.
module Rose.Data.SExpression
import Data.Atom
infixl 6 <::>
||| The type of s-expressions.
||| The type is a straightforward representation of a tree-like structure.
||| Rather than make this type inhabited, we keep the representation simple.
||| This prevents us from defining functors, over the type etc. and prevents
||| obvious injections/projections to Idris structures like List, but we can leverage
||| proofs to confirm that the subset of *well-formed* s-expressions is translatable
||| into and from a structure like a List.
public export
data SE : Type where
Nil : SE -- () the empty list (or empty array [])
MkAtom : Atom -> SE -- atoms, 1, 'a', "foo", etc.
Expression : SE -> SE -> SE -- (x . y)
export
Show SE where
show Nil = "()"
show (MkAtom x) = show x
show (Expression hd Nil) = "(" ++ (show hd) ++ ")"
show (Expression hd tl) = "(" ++ (show hd) ++ " " ++ (inner tl) ++ ")"
where inner : SE -> String
inner Nil = ""
inner (MkAtom x) = show x
inner (Expression Nil rest) = "()" ++ " " ++ inner rest
inner (Expression e@(Expression h t) Nil) = show e ++ ""
inner (Expression e@(Expression h t) rest) = show e ++ " " ++ inner rest
inner (Expression h Nil) = inner h ++ ""
inner (Expression h t) = inner h ++ " " ++ inner t
export
Eq SE where
Nil == Nil = True
(MkAtom x) == (MkAtom y) = x == y
(Expression first rest) == (Expression hd tl) = (first == hd) && (rest == tl)
_ == _ = False
public export
Semigroup SE where
(<+>) Nil x = x
(<+>) x Nil = x
(<+>) first rest = (Expression first rest)
public export
Monoid SE where
neutral = Nil
public export
[combinatorial] Semigroup SE where
(<+>) first rest = (Expression first rest)
||| <::> is a convenient infix constructor for s-expressions.
||| Analogous to the list constructor ::, but for s-expressions.
public export
(<::>) : SE -> SE -> SE
(<::>) first rest = (<+>) @{combinatorial} first rest
||| car returns the first element of an s-expression.
export
car : SE -> SE
car (Expression first rest) = first
car x = x
||| cdr returns the last element of an s-expression.
export
cdr : SE -> SE
cdr (Expression first rest) = rest
cdr x = x
||| map maps a function f across the members of an s-expression.
export
map : (SE -> SE) -> SE -> SE
map f (Expression first rest) =
(map f first) <::> (map f rest)
map f atom@(MkAtom _) = f atom
map f Nil = f Nil
||| length returns the length of an s-expression.
export
length : SE -> Integer
length Nil = 0
length (MkAtom _) = 1
length (Expression first rest) = (length first) + (length rest)
||| Convenience function for producing a symbol atom.
export
symbol : String -> SE
symbol s = (MkAtom (MkSymbol s))
||| isSymbol returns true if an s-expression is a symbol atom.
export
isSymbol : SE -> Bool
isSymbol (MkAtom (MkSymbol _)) = True
isSymbol _ = False
||| isAtom returns true if an s-expression is an atom.
export
isAtom : SE -> Bool
isAtom (MkAtom _) = True
isAtom _ = False
||| isNil returns true if an s-expression is Nil.
export
isNil : SE -> Bool
isNil = (neutral==)
||| isExpression returns true if an s-expression is an Expression.
export
isExpression : SE -> Bool
isExpression (Expression first rest) = True
isExpression _ = False
-- The following syntax patterns are provided for convenience; we can match on longer forms
-- such as anonymous functions with fewer characters.
-- Match an arbitrary expression
pattern syntax ExpressionPat = (Expression _ _)
-- Match an anonymous function
pattern syntax FunctionPat [args] [body] = (Expression (MkAtom (MkSymbol "fn")) (Expression args body))
-- Match an anonymous macro
pattern syntax MacroPat [args] [body] = (Expression (MkAtom (MkSymbol "macro")) (Expression args body))
-- Match a function application
pattern syntax ApplicationPat [func] [args]= (Expression func args)

80
Rose/Evaluator.idr

@ -0,0 +1,80 @@
||| Module Evaluator defines an evaluator for the Rose language.
module Rose.Evaluator
import Control.ST
import Data.Vect
import Parser
import Primitives
import Lookup
import Lambda
import Data.Morphisms
import Data.Error
import Data.SExpression
import Data.Atom
import Data.Form
||| EvaluationError generates an error from an un-evaluable s-expression.
EvaluationError : SE -> RoseError
EvaluationError expr = MkError $ "Couldn't evaluate the form: " ++ show expr
morphWithFailure : RoseError -> Maybe SE ~> Either RoseError SE
morphWithFailure e = Mor (maybe (Left e) Right)
morphWithSuccess : SE -> Maybe SE ~> Either RoseError SE
morphWithSuccess se = Mor (maybe (Right se) Right)
orErr : RoseError -> (Maybe SE -> Either RoseError SE)
orErr e = (applyMor (morphWithFailure e))
orForm : SE -> (Maybe SE -> Either RoseError SE)
orForm se = (applyMor (morphWithSuccess se))
-- We probably don't need this combinator; learn how to use Data.Morphisms more effectively
infixr 6 >>-
infixr 6 >-
(>>-) : (Maybe SE) -> RoseError -> Either RoseError SE
(>>-) m e = (orErr e) m
(>-) : (Maybe SE) -> SE -> Either RoseError SE
(>-) m e = (orForm e) m
-- TODO: Define define.
--define : Environment -> SE -> (Either RoseError Environment)
--define env (Expression (MkAtom (MkSymbol name)) val) =
-- pure $ maybe ((name,val)::env) (\x => (name,val)::(delete (name,x) env)) (Lookup.lookup name env)
--define env _ = Left $ EvaluationError Nil
||| Evaluate an s-expression.
export
evaluate : Environment -> SE -> (Either RoseError SE)
evaluate env m@(MacroPat (Expression first rest) bod) =
(eta m) >- m
>>= \x => if (x == m) then pure m else evaluate env x
evaluate env f@(FunctionPat (Expression first rest) bod) =
(eta f) >- f >>= \x => if (x == f) then pure f else evaluate env x
evaluate env (ApplicationPat (MkAtom (MkSymbol "eval")) rest@(Expression first Nil)) =
either Left (evaluate env) $ (evaluate env) first
evaluate env (ApplicationPat m@(MacroPat _ _) e) =
beta m e
evaluate env (ApplicationPat f@(FunctionPat _ _) e) =
case (beta f e) of
Right g@(FunctionPat _ _) => Right g
Right x => (evaluate env) x
Left e => Left e
evaluate env (ApplicationPat a@(ApplicationPat (MkAtom (MkSymbol _)) _) rest@(Expression _ _)) =
(evaluate env) a
>>= \x => (evaluate env) rest
>>= \y => (evaluate env)
$ Apply x [y]
--evaluate env (ApplicationPat (MkAtom (MkSymbol "def")) decl) =
-- either Left (const $ Right decl) $ define env decl
evaluate env (ApplicationPat s@(MkAtom (MkSymbol st)) rest@(Expression _ _)) =
(case getPrimitive st of
Nothing => Left $ EvaluationError Nil
Just f => f rest)
-- <|> Just (Right $ s) -- TODO: Lookup
evaluate env (Expression x Nil) = (evaluate env) x
evaluate env (MkAtom x) = Right (MkAtom x)
evaluate env Nil = Right Nil

63
Rose/Lambda.idr

@ -0,0 +1,63 @@
||| Module Lambda defines lambda calculus operations for the Rose language.
module Rose.Lambda
import Data.SExpression
import Data.Atom
import Data.Form
import Data.Error
||| Generate an error reporting that a variable could not be bound to an argument.
export
MalformedBind : SE -> SE -> SE -> RoseError
MalformedBind free arg body = MkError ("Can't bind the variable: " ++ show free ++ " to " ++ show arg ++ " in " ++ show body)
||| Generate an error reporting that an s-expression could not be beta reduced.
export
BetaReductionError : SE -> RoseError
BetaReductionError se = MkError ("Couldn't beta reduce: " ++ show se)
||| Replace instances of a symbol with another SExpression.
total
bind : SE -> SE -> SE -> Either RoseError SE
bind s@(MkAtom (MkSymbol _)) arg body =
Right $ map (\elem => if elem == s then arg else elem) body
bind s arg body = Left $ MalformedBind s arg body
mutual
||| beta reduce an s-expression.
total
reduce : (List SE -> SE -> Either RoseError Form) -> SE -> SE -> SE -> Either RoseError SE
reduce _ body Nil Nil = pure body
reduce f body params Nil = (f (toList params) body)
reduce f body (Expression first rest) (Expression hd tl) =
bind first hd body
>>= \bound => (f (toList rest) bound)
>>= \new => beta new tl
reduce f body params args =
(f (toList params) body)
>>= \form => Left $ BetaReductionError (fromList [form, args])
||| Beta reduction of terms.
||| Terms are partially reduced if their parameters are not completely filled.
export total
beta : SE -> SE -> Either RoseError SE
beta m@(MacroPat params body) args =
reduce Macro body params args
beta f@(FunctionPat params body) args =
reduce Fn body params args
beta expr args = Left $ BetaReductionError (fromList [expr, args])
||| Eta conversion of terms
export
eta : SE -> Maybe SE
eta f@(FunctionPat args a@(Expression (ApplicationPat (MkAtom (MkSymbol _)) ap) Nil)) =
Just $ if args == ap
then a
else f
eta m@(MacroPat args a@(Expression (ApplicationPat (MkAtom (MkSymbol _)) ap) Nil)) =
Just $ if args == ap
then a
else m
eta f = Nothing
-- TODO: Alpha conversion

135
Rose/Lexer.idr

@ -0,0 +1,135 @@
||| Module Lexer defines a lexer for the Rose langauge.
module Rose.Lexer
import Text.Lexer
import Text.Lexer.Core
||| Token represents valid tokens of the Rose language.
public export
data Token : Type where
TkChar : Char -> Token
TkString : String -> Token
TkNum : Integer -> Token
TkSymbol : String -> Token
DoubleQuote : Token
Quote : Token
RParen : Token
LParen : Token
RBracket : Token
LBracket : Token
Whitespace : Token
Comment : Token
EOF : Token
export
Show Token where
show (TkNum x) = show x
show (TkSymbol s) = s
show (TkString s) = show s
show (TkChar c) = show c
show DoubleQuote = "\""
show Quote = "'"
show RParen = "right paren"
show LParen = "left paren"
show RBracket = "right bracket"
show LBracket = "left bracket"
show Whitespace = "space"
show Comment = "comment"
show EOF = "End of file"
export
Eq Token where
(TkChar _) == (TkChar _) = True
(TkString _) == (TkString _) = True
(TkNum _) == (TkNum _) = True
(TkSymbol _) == (TkSymbol _) = True
DoubleQuote == DoubleQuote = True
Quote == Quote = True
RParen == RParen = True
LParen == LParen = True
RBracket == RBracket = True
LBracket == LBracket = True
Whitespace == Whitespace = True
EOF == EOF = True
_ == _ = False
export
Show (TokenData Token) where
show (MkToken l c t) =
show t ++ " at " ++ "line: "
++ show l
++ " col: " ++ show c
||| A helper function that returns a token provider that just returns a given
||| token.
precisely : Token -> String -> Token
precisely = const
||| symbolTerminator marks the end of a contiguous symbol.
symbolTerminator : Lexer
symbolTerminator = is '('
<|> is ')'
<|> is '['
<|> is ']'
<|> spaces
||| sym is a lexer for symbol atoms in the Rose language.
sym : Lexer
sym = some (non (symbolTerminator <|> digits <|> charLit <|> stringLit))
<+> opt digits
||| comment is a lexer for line comments in the Rose language.
comment : Lexer
comment = (some $ is ';')
<+> any
<+> newline
||| blckComment is a lexer for block comments in the Rose language.
||| n.b. `blockComment` is already an exported name, thus the munging of this name.
blckComment : Lexer
blckComment = is ';'
<+> is '|'
<+> any
<+> is '|'
<+> is ';'
-- TODO: Cast is lossy, use Data.String.parseInteger
toInt' : String -> Integer
toInt' = cast
||| Map of recognized tokens of the Rose language.
tokenMap : TokenMap Token
tokenMap =
[(is '(', precisely LParen)
,(is ')', precisely RParen)
,(is '[', precisely LBracket)
,(is ']', precisely RBracket)
,(digits, TkNum . toInt')
,(stringLit, TkString)
,(charLit, TkChar . strHead)
,(is '"', precisely DoubleQuote)
,(is '\'', precisely Quote)
,(sym, TkSymbol)
,(spaces, precisely Whitespace)
]
||| Drop tokens that don't matter for parsing, such as whitespace and comments.
export
dropExtraTokens : (List (TokenData Token), (Int, Int, String)) ->
(List (TokenData Token), (Int, Int, String))
dropExtraTokens (toks, info) = ((filter (not . irrelevant) toks), info)
where irrelevant : (TokenData Token) -> Bool
irrelevant t =
case tok t of
Whitespace => True
_ => False
||| runLex runs the Rose lexer, dropping meaningless tokens such as comments.
export
runLex : String -> (List (TokenData Token), (Int, Int, String))
runLex = dropExtraTokens . lex tokenMap
||| tokens returns the list of tokens generated by the Rose lexer.
export
tokens : (List (TokenData Token), (Int, Int, String)) -> List (TokenData Token)
tokens = fst

86
Rose/Parser.idr

@ -0,0 +1,86 @@
||| 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
||| Helper function for computing Grammars
public export
Rule : Type -> Type
Rule ty = Grammar (TokenData Token) True ty
export
Show (ParseError (TokenData Token)) where
show (Error e tok) = "Unable to parse token " ++ show tok
||| atoms is a rule for parsing atoms of the Rose language.
export total
atoms : Rule SE
atoms = terminal
(\x => untok (tok x))
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 _ = Nothing
||| 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)
lbrack : Rule ()
lbrack = punct LBracket
rbrack : Rule ()
rbrack = punct RBracket
rparen : Rule ()
rparen = punct RParen
lparen : Rule ()
lparen = punct LParen
-- Required to break recursion and permit constructs such as:
-- ((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)
||| A program is a list of s-expressions
export
program : Grammar (TokenData Token) False (List SE)
program =
manyTill eof list

61
Rose/Primitives.idr

@ -0,0 +1,61 @@
||| Module Primitives defines the primitives of the Rose language.
module Primitives
import Data.Atom
import Data.SExpression
import Data.Error
import Data.Form
||| par is a helper function for producing a partial function
||| for a primitive.
export
par : SE -> List SE -> List SE -> Either RoseError SE
par f params args = (Fn params (Apply f (args ++ params)))
||| Primitive represents the type of primitive operations in the Rose language.
Primitive : Type
Primitive = (String, SE -> Either RoseError SE)
-- TODO: make this dry
||| Primitive addition.
add : SE -> Either RoseError SE
add (Expression i@(MkAtom (MkInteger x)) rest) =
resolve rest
where resolve : SE -> Either RoseError SE
resolve (Expression (MkAtom (MkInteger y)) Nil) = Right $ MkAtom (MkInteger (x + y))
resolve Nil = par (symbol "+") [(symbol "x")] [i]
resolve _ = Left $ MkError "bad argument"
add _ = Left $ MkError "Can't pass arg to add"
||| Primitive subtraction.
minus : SE -> Either RoseError SE
minus (Expression i@(MkAtom (MkInteger x)) rest) =
resolve rest
where resolve : SE -> Either RoseError SE
resolve (Expression (MkAtom (MkInteger y)) Nil) = Right $ MkAtom (MkInteger (x - y))
resolve Nil = par (symbol "-") [(symbol "x")] [i]
resolve _ = Left $ MkError "bad argument"
minus _ = Left $ MkError "Can't pass arg to minus"
||| Primitive multiplication.
mult : SE -> Either RoseError SE
mult (Expression i@(MkAtom (MkInteger x)) rest) =
resolve rest
where resolve : SE -> Either RoseError SE
resolve (Expression (MkAtom (MkInteger y)) Nil) = Right $ MkAtom (MkInteger (x * y))
resolve Nil = par (symbol "*") [(symbol "x")] [i]
resolve _ = Left $ MkError "bad argument"
mult _ = Left $ MkError "Can't pass arg to mult"
||| Primitives lists all the primitives of the Rose language.
Primitives : List Primitive
Primitives =
[ ("+", add)
, ("-", minus)
, ("*", mult)
]
||| getPrimitive retrieves a primitive.
export
getPrimitive : String -> Maybe (SE -> Either RoseError SE)
getPrimitive s = lookup s Primitives

34
Rose/Repl.idr

@ -0,0 +1,34 @@
module Main
import Text.Parser
import Text.Parser.Core
import Text.Lexer
import Lexer
import Parser
import Data.SExpression
import Evaluator
import Data.Error
import Lookup
read : IO String
read = getLine
>>= (\x => pure (parse (list <|> array)
$ tokens
$ runLex x))
>>= pure . go
where go : Either (ParseError (TokenData Token)) (SE, (List (TokenData Token))) -> String
go = either show (either show show . evaluate [] . fst)
print : String -> IO ()
print s = putStrLn s
main : IO ()
main =
putStrLn "Rose version 1.0"
*> putStrLn "ctrl+c to exit"
*> loop
where loop : IO ()
loop = putStr "⚘: "
*> read
>>= putStrLn
>>= \_ => loop

30
rose.ipkg

@ -0,0 +1,30 @@
package rose
brief = "A statically typed, theorem proving lisp."
version = 0.0.1
readme = README.md
license = MIT
author = scg.olsen@gmail.com
maintainer = scg.olsen@gmail.com
homepage = http://rose.dev
sourceloc = http://www.github.com/rose-lang/rose
sourceloc = http://www.github.com/rose-lang/rose/issues
pkgs = contrib
modules = Rose.Data.Atom
, Rose.Data.SExpression
, Rose.Data.Error
, Rose.Data.Form
, Rose.Lambda
, Rose.Lexer
, Rose.Parser
, Rose.Evaluator
, Rose.Repl
sourcedir = Rose
-- On macOS case insensitivity leads to conflicts between the source directory 'Rose' and the executable name 'rose'
-- thus we use rosie instead, the Makefile copies the executable into out as 'rose'.
executable = rosie
main = Repl
Loading…
Cancel
Save