aboutsummaryrefslogtreecommitdiffhomepage
diff options
context:
space:
mode:
Diffstat
-rw-r--r--bruijn.cabal4
-rw-r--r--package.yaml1
-rw-r--r--src/Eval.hs65
-rw-r--r--src/Parser.hs25
-rw-r--r--src/Reducer.hs46
5 files changed, 115 insertions, 26 deletions
diff --git a/bruijn.cabal b/bruijn.cabal
index 8d443f6..744058c 100644
--- a/bruijn.cabal
+++ b/bruijn.cabal
@@ -27,6 +27,7 @@ library
exposed-modules:
Eval
Parser
+ Reducer
other-modules:
Paths_bruijn
hs-source-dirs:
@@ -35,6 +36,7 @@ library
LambdaCase
build-depends:
base >=4.7 && <5
+ , containers
, haskeline
, mtl
, parsec
@@ -52,6 +54,7 @@ executable bruijn-exe
build-depends:
base >=4.7 && <5
, bruijn
+ , containers
, haskeline
, mtl
, parsec
@@ -70,6 +73,7 @@ test-suite bruijn-test
build-depends:
base >=4.7 && <5
, bruijn
+ , containers
, haskeline
, mtl
, parsec
diff --git a/package.yaml b/package.yaml
index d5e1c58..9fdee03 100644
--- a/package.yaml
+++ b/package.yaml
@@ -27,6 +27,7 @@ dependencies:
- mtl
- haskeline
- parsec
+- containers
library:
source-dirs: src
diff --git a/src/Eval.hs b/src/Eval.hs
index 4e73778..3b5453b 100644
--- a/src/Eval.hs
+++ b/src/Eval.hs
@@ -6,6 +6,7 @@ import Control.Exception
import Control.Monad.State
import Debug.Trace
import Parser
+import Reducer
import System.Console.Haskeline
import System.Environment
import System.Exit
@@ -17,19 +18,6 @@ import Text.Parsec hiding ( State
type Environment = [(String, Expression)]
type Program = State Environment
-eval :: [String] -> Environment -> IO Environment
-eval [] env = pure env
-eval (line : ls) env = case parse parseLine "Evaluator" line of
- Left err -> print err >> pure env
- Right instr -> case instr of
- Define name exp ->
- let (res, env') = evalDefine name exp `runState` env
- in case res of
- Left err -> print err >> eval ls env'
- Right _ -> eval ls env'
- Evaluate exp -> putStrLn "ok" >> pure env
- _ -> eval ls env
-
evalVar :: String -> Program (Failable Expression)
evalVar var = state $ \e ->
( case lookup var e of
@@ -49,9 +37,10 @@ evalApp f g =
evalExp :: Expression -> Program (Failable Expression)
evalExp idx@(Bruijn _ ) = pure $ Right idx
evalExp ( Variable var) = evalVar var
-evalExp ( Abstraction exp) = evalExp exp
+evalExp ( Abstraction exp) = evalExp exp >>= pure . fmap Abstraction
evalExp ( Application f g) = evalApp f g
+-- TODO: Duplicate function error
evalDefine :: String -> Expression -> Program (Failable Expression)
evalDefine name exp =
evalExp exp
@@ -60,6 +49,47 @@ evalDefine name exp =
Right f -> modify ((name, f) :) >> pure (Right f)
)
+eval :: [String] -> Environment -> IO Environment
+eval [] env = pure env
+eval (line : ls) env = case parse parseLine "Evaluator" line of
+ Left err -> print err >> pure env
+ Right instr -> case instr of
+ Define name exp ->
+ let (res, env') = evalDefine name exp `runState` env
+ in case res of
+ Left err -> print err >> eval ls env'
+ Right _ -> (putStrLn $ name <> " = " <> show exp) >> eval ls env'
+ Evaluate exp ->
+ let (res, env') = evalExp exp `runState` env
+ in putStrLn
+ (case res of
+ Left err -> show err
+ Right exp -> show $ reduce exp
+ )
+ >> pure env
+ _ -> eval ls env
+
+-- TODO: Less duplicate code (liftIO?)
+-- TODO: Convert back to my notation using custom show
+evalRepl :: String -> Environment -> InputT IO Environment
+evalRepl line env = case parse parseReplLine "Repl" line of
+ Left err -> outputStrLn (show err) >> pure env
+ Right instr -> case instr of
+ Define name exp ->
+ let (res, env') = evalDefine name exp `runState` env
+ in case res of
+ Left err -> outputStrLn (show err) >> pure env'
+ Right _ -> (outputStrLn $ name <> " = " <> show exp) >> pure env'
+ Evaluate exp ->
+ let (res, env') = evalExp exp `runState` env
+ in outputStrLn
+ (case res of
+ Left err -> show err
+ Right exp -> (show exp) <> "\n-> " <> (show $ reduce exp)
+ )
+ >> pure env
+ _ -> pure env
+
evalFile :: String -> IO ()
evalFile path = do
file <- try $ readFile path :: IO (Either IOError String)
@@ -67,12 +97,9 @@ evalFile path = do
Left exception -> print (exception :: IOError)
Right file -> eval (lines file) [] >> putStrLn "Done"
-evalRepl :: String -> Environment -> InputT IO Environment
-evalRepl line env = outputStrLn (show env) >> pure env
-
repl :: Environment -> InputT IO ()
repl env =
- getInputLine ":: "
+ getInputLine "λ "
>>= (\case
Nothing -> pure ()
Just line -> evalRepl line env >>= repl
@@ -85,7 +112,7 @@ evalMain :: IO ()
evalMain = do
args <- getArgs
case args of
- [] -> runInputT defaultSettings { historyFile = Just ".brown-history" }
+ [] -> runInputT defaultSettings { historyFile = Just ".bruijn-history" }
$ repl []
[path] -> evalFile path
_ -> usage
diff --git a/src/Parser.hs b/src/Parser.hs
index 1f768bd..b6ab9fb 100644
--- a/src/Parser.hs
+++ b/src/Parser.hs
@@ -5,10 +5,11 @@ import Text.Parsec
import Text.Parsec.Language
import qualified Text.Parsec.Token as Token
-data Error = SyntaxError ParseError | UndeclaredFunction String | InvalidIndex Int | FatalError String
+data Error = SyntaxError ParseError | UndeclaredFunction String | DuplicateFunction String | InvalidIndex Int | FatalError String
instance Show Error where
show (SyntaxError err) = show err
show (UndeclaredFunction err) = "ERROR: undeclared function " <> show err
+ show (DuplicateFunction err) = "ERROR: duplicate function " <> show err
show (InvalidIndex err) = "ERROR: invalid index " <> show err
show (FatalError err) = show err
type Failable = Either Error
@@ -17,7 +18,7 @@ languageDef :: GenLanguageDef String u Identity
languageDef = emptyDef { Token.commentLine = "#"
, Token.identStart = letter
, Token.identLetter = alphaNum <|> char '?'
- , Token.reservedOpNames = ["[", "]"]
+ , Token.reservedOpNames = ["[", "]", "="]
}
type Parser = Parsec String ()
@@ -42,7 +43,7 @@ data Instruction = Define String Expression | Evaluate Expression | Comment Stri
parseAbstraction :: Parser Expression
parseAbstraction = do
reservedOp "["
- exp <- parseExpression
+ exp <- parseExpression <|> parseBruijn
reservedOp "]"
pure $ Abstraction exp
@@ -64,25 +65,35 @@ parseVariable = do
pure $ Variable var
parseSingleton :: Parser Expression
-parseSingleton =
- parseAbstraction <|> parens parseApplication <|> parseBruijn <|> parseVariable
+parseSingleton = parseAbstraction <|> parens parseApplication <|> parseVariable
parseExpression :: Parser Expression
parseExpression = do
expr <- parseApplication <|> parseSingleton
pure expr
+parseEvaluate :: Parser Instruction
+parseEvaluate = Evaluate <$> parseExpression
+
parseDefine :: Parser Instruction
parseDefine = do
var <- identifier
spaces
Define var <$> parseExpression
+parseReplDefine :: Parser Instruction
+parseReplDefine = do
+ var <- identifier
+ spaces
+ reservedOp "="
+ spaces
+ Define var <$> parseExpression
+
parseComment :: Parser Instruction
parseComment = string "#" >> Comment <$> many letter
parseLine :: Parser Instruction
parseLine = try parseDefine <|> parseComment
-parseReplLine :: Parser Expression
-parseReplLine = try parseExpression
+parseReplLine :: Parser Instruction
+parseReplLine = try parseReplDefine <|> parseComment <|> parseEvaluate
diff --git a/src/Reducer.hs b/src/Reducer.hs
new file mode 100644
index 0000000..1bc001f
--- /dev/null
+++ b/src/Reducer.hs
@@ -0,0 +1,46 @@
+module Reducer
+ ( reduce
+ ) where
+
+import Data.Bifunctor ( first )
+import Data.Set hiding ( fold )
+import Parser
+
+-- TODO: Reduce variable -> later: only reduce main in non-repl
+-- TODO: Use zero-based indexing (?)
+
+shiftUp :: Expression -> Int -> Expression
+shiftUp (Bruijn x) n = if x > n then Bruijn (pred x) else Bruijn x
+shiftUp (Application exp1 exp2) n =
+ Application (shiftUp exp1 n) (shiftUp exp2 n)
+shiftUp (Abstraction exp) n = Abstraction (shiftUp exp (succ n))
+
+shiftDown :: Expression -> Int -> Expression
+shiftDown (Bruijn x) n = if x > n then Bruijn (succ x) else Bruijn x
+shiftDown (Application exp1 exp2) n =
+ Application (shiftDown exp1 n) (shiftDown exp2 n)
+shiftDown (Abstraction exp) n = Abstraction (shiftDown exp (succ n))
+
+bind :: Expression -> Expression -> Int -> Expression
+bind exp (Bruijn x) n = if x == n then exp else Bruijn x
+bind exp (Application exp1 exp2) n =
+ Application (bind exp exp1 n) (bind exp exp2 n)
+bind exp (Abstraction exp') n =
+ Abstraction (bind (shiftDown exp 0) exp' (succ n))
+
+step :: Expression -> Expression
+step (Bruijn exp) = Bruijn exp
+step (Application (Abstraction exp) app) =
+ shiftUp (bind (shiftDown app 0) exp 1) 1
+step (Application exp1 exp2) = Application (step exp1) (step exp2)
+step (Abstraction exp ) = Abstraction (step exp)
+
+reduceable :: Expression -> Bool
+reduceable (Bruijn _ ) = False
+reduceable (Application (Abstraction _) _ ) = True
+reduceable (Application exp1 exp2) = reduceable exp1 || reduceable exp2
+reduceable (Abstraction exp ) = reduceable exp
+
+-- alpha conversion is not needed with de bruijn indexing
+reduce :: Expression -> Expression
+reduce = until (not . reduceable) step