diff options
| -rw-r--r-- | src/Eval.hs | 39 | ||||
| -rw-r--r-- | src/Helper.hs | 2 | ||||
| -rw-r--r-- | src/Parser.hs | 20 | ||||
| -rw-r--r-- | src/Reducer.hs | 4 | ||||
| -rw-r--r-- | std.bruijn | 63 | ||||
| -rw-r--r-- | test.bruijn | 70 |
6 files changed, 159 insertions, 39 deletions
diff --git a/src/Eval.hs b/src/Eval.hs index 47ca4ca..c65bf0e 100644 --- a/src/Eval.hs +++ b/src/Eval.hs @@ -47,6 +47,14 @@ evalDefine name exp = Right f -> modify ((name, f) :) >> pure (Right f) ) +evalTest :: Expression -> Expression -> Program (Failable Instruction) +evalTest exp1 exp2 = + evalExp exp1 + >>= (\case + Left exp1 -> pure $ Left exp1 + Right exp1 -> fmap (Test exp1) <$> evalExp exp2 + ) + eval :: [String] -> Environment -> IO Environment eval [] env = pure env eval (line : ls) env = case parse parseLine "FILE" line of @@ -56,7 +64,21 @@ eval (line : ls) env = case parse parseLine "FILE" line of 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' + Right _ -> eval ls env' + Test exp1 exp2 -> + let (res, _) = evalTest exp1 exp2 `runState` env + in case res of + Left err -> putStrLn (show err) >> pure env + Right (Test exp1' exp2') -> + when + (reduce exp1' /= reduce exp2') + ( putStrLn + $ "ERROR: test failed: " + <> (show exp1) + <> " != " + <> (show exp2) + ) + >> eval ls env _ -> eval ls env evalFunc :: String -> Environment -> IO Environment @@ -65,6 +87,7 @@ evalFunc func env = case lookup func env of Just exp -> (print $ reduce exp) >> pure env -- TODO: Less duplicate code (liftIO?) +-- TODO: Generally improve eval code evalRepl :: String -> Environment -> InputT IO Environment evalRepl line env = case parse parseReplLine "REPL" line of Left err -> outputStrLn (show err) >> pure env @@ -97,6 +120,20 @@ evalRepl line env = case parse parseReplLine "REPL" line of Left exception -> print (exception :: IOError) >> pure env Right file -> eval (filter (not . null) $ lines file) [] >>= pure ) + Test exp1 exp2 -> + let (res, _) = evalTest exp1 exp2 `runState` env + in case res of + Left err -> outputStrLn (show err) >> pure env + Right (Test exp1' exp2') -> + when + (reduce exp1' /= reduce exp2') + ( outputStrLn + $ "ERROR: test failed: " + <> (show exp1) + <> " != " + <> (show exp2) + ) + >> pure env _ -> pure env evalFile :: String -> IO () diff --git a/src/Helper.hs b/src/Helper.hs index 5e02a94..57fb9f4 100644 --- a/src/Helper.hs +++ b/src/Helper.hs @@ -14,7 +14,7 @@ type Failable = Either Error data Expression = Bruijn Int | Variable String | Abstraction Expression | Application Expression Expression deriving (Ord, Eq) -data Instruction = Define String Expression | Evaluate Expression | Comment String | Load String +data Instruction = Define String Expression | Evaluate Expression | Comment String | Load String | Test Expression Expression deriving (Show) instance Show Expression where show (Bruijn x ) = show x diff --git a/src/Parser.hs b/src/Parser.hs index 6fbeca4..33b3c44 100644 --- a/src/Parser.hs +++ b/src/Parser.hs @@ -6,7 +6,7 @@ module Parser import Control.Monad ( ap ) import Data.Functor.Identity import Helper -import Text.Parsec +import Text.Parsec hiding ( parseTest ) import Text.Parsec.Language import qualified Text.Parsec.Token as Token @@ -107,9 +107,23 @@ parseComment = string "#" >> Comment <$> almostAnything parseLoad :: Parser Instruction parseLoad = string ":load " >> Load <$> almostAnything +parseTest :: Parser Instruction +parseTest = do + string ":test " + exp1 <- parseExpression + spaces + reservedOp "=" + spaces + exp2 <- parseExpression + pure $ Test exp1 exp2 + parseLine :: Parser Instruction -parseLine = try parseDefine <|> parseComment +parseLine = try parseDefine <|> try parseComment <|> try parseTest parseReplLine :: Parser Instruction parseReplLine = - try parseReplDefine <|> parseComment <|> parseEvaluate <|> parseLoad + try parseReplDefine + <|> try parseComment + <|> try parseEvaluate + <|> try parseLoad + <|> try parseTest diff --git a/src/Reducer.hs b/src/Reducer.hs index 809687b..a7c544a 100644 --- a/src/Reducer.hs +++ b/src/Reducer.hs @@ -20,11 +20,11 @@ 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 (exp <-> 0) exp' (succ n)) +bind exp (Abstraction exp') n = Abstraction (bind (exp <-> (-1)) exp' (succ n)) step :: Expression -> Expression step (Bruijn exp ) = Bruijn exp -step (Application (Abstraction exp) app ) = (bind (app <-> 0) exp 0) <+> 0 +step (Application (Abstraction exp) app ) = (bind (app <-> (-1)) exp 0) <+> 0 step (Application exp1 exp2) = Application (step exp1) (step exp2) step (Abstraction exp ) = Abstraction (step exp) @@ -15,9 +15,18 @@ Y [[1 (0 0)] [1 (0 0)]] Θ [[0 (1 1 0)]] [[0 (1 1 0)]] i [0 S K] -# ======= +# ===== +# Pairs +# ===== + +pair [[[0 2 1]]] +fst [0 T] +snd [0 F] + +# =================================== # Ternary -# ======= +# According to works of T.Æ. Mogensen +# =================================== zero? [0 T [F] I [F]] upNeg [[[[[2 (4 3 2 1 0)]]]]] @@ -30,13 +39,26 @@ negate [[[[[4 3 0 1 2]]]]] tritNeg [[[2]]] tritZero [[[1]]] tritPos [[[0]]] +lst [0 tritZero [tritNeg] [tritZero] [tritPos]] + +_succZ (pair +0 +1) +_succANeg [0 [[[pair (upNeg 2) (upZero 2)]]]] +_succAZero [0 [[[pair (upZero 2) (upPos 2)]]]] +_succAPos [0 [[[pair (upPos 2) (upNeg 1)]]]] +succ [snd (0 _succZ _succANeg _succAZero _succAPos)] + +_predZ (pair +0 -1) +_predANeg [0 [[[pair (upNeg 2) (upPos 1)]]]] +_predAZero [0 [[[pair (upZero 2) (upNeg 2)]]]] +_predAPos [0 [[[pair (upPos 2) (upZero 2)]]]] +pred [snd (0 _predZ _predANeg _predAZero _predAPos)] _absNeg [[[[[2 4]]]]] _absZero [[[[[1 4]]]]] _absPos [[[[[0 4]]]]] abstractify [0 [[[[3]]]] _absNeg _absZero _absPos] -_normalize [[0 [ +0 ] [[upNeg (1 1 0)]] [[upZero (1 1 0)]] [[upPos (1 1 0)]] 0]] +_normalize [[0 [ +0 ] [[upNeg (1 1 0)]] [[upZero (1 1 0)]] [[upPos (1 1 0)]] 1]] normalize ω _normalize _eqZero? [zero? (normalize 0)] @@ -46,24 +68,9 @@ _eqPos [[0 F [F] [F] [2 0]]] _eqAbs [0 _eqZero? _eqNeg _eqZero _eqPos] eq [[_eqAbs 1 (abstractify 0)]] -proj22 [0 [[0]]] -tuple [[[0 1 2]]] - -_succZ (tuple +0 +1) -_succANeg [0 [[[tuple (upNeg 2) (upZero 2)]]]] -_succAZero [0 [[[tuple (upZero 2) (upPos 2)]]]] -_succAPos [0 [[[tuple (upPos 2) (upNeg 1)]]]] -succ [proj22 (0 _succZ _succANeg _succAZero _succAPos)] - -_predZ (tuple +0 -1) -_predANeg [0 [[[tuple (upNeg 2) (upPos 1)]]]] -_predAZero [0 [[[tuple (upZero 2) (upNeg 2)]]]] -_predAPos [0 [[[tuple (upPos 2) (upZero 2)]]]] -pred [proj22 (0 _predZ _predANeg _predAZero _predAPos)] - _addZ [[0 (pred (normalize 1)) (normalize 1) (succ (normalize 1))]] _addC [[1 0 tritZero]] -_addBNeg2 [1 (upZero (3 0 tritNeg)) (upPos (3 0 tritZero)) (upNeg (3 0 tritZero))] +_addBNeg2 [1 (upZero (3 0 tritNeg)) (upPos (3 0 tritNeg)) (upNeg (3 0 tritZero))] _addBNeg [1 (upPos (3 0 tritNeg)) (upNeg (3 0 tritZero)) (upZero (3 0 tritZero))] _addBZero [up 1 (3 0 tritZero)] _addBPos [1 (upZero (3 0 tritZero)) (upPos (3 0 tritZero)) (upNeg (3 0 tritPos))] @@ -76,14 +83,6 @@ add [[_addAbs 1 (abstractify 0)]] sub [[add 1 (negate 0)]] -# ===== -# Pairs -# ===== - -pair [[[0 2 1]]] -fst [0 T] -snd [0 F] - # =============== # Boolean algebra # =============== @@ -98,10 +97,10 @@ if [[[2 1 0]]] # Church numerals # =============== -zero [[0]] -succ [[[1 (2 1 0)]]] -add [[[[3 1 (2 1 0)]]]] -mul [[[2 (1 0)]]] -exp [[0 1]] +churchZero [[0]] +churchSucc [[[1 (2 1 0)]]] +churchAdd [[[[3 1 (2 1 0)]]]] +churchMul [[[2 (1 0)]]] +churchExp [[0 1]] main I F diff --git a/test.bruijn b/test.bruijn new file mode 100644 index 0000000..1a12d1c --- /dev/null +++ b/test.bruijn @@ -0,0 +1,70 @@ +atom0 [[[[[4]]]]] +atom1 [[[[[3]]]]] +atom2 [[[[[2]]]]] +atom3 [[[[[1]]]]] +atom4 [[[[[0]]]]] + +# ========= +# Reduction +# ========= + +:test [0] atom0 = atom0 +:test [[0 1 0]] atom0 atom1 = atom1 atom0 atom1 +:test [[[[3 2 1 0]]]] atom0 atom1 atom2 atom3 = atom0 atom1 atom2 atom3 + +# =============== +# Church numerals +# =============== + +chrch_n0 [[0]] +chrch_n1 [[1 0]] +chrch_n2 [[1 (1 0)]] +chrch_n3 [[1 (1 (1 0))]] +chrch_n4 [[1 (1 (1 (1 0)))]] +chrch_n5 [[1 (1 (1 (1 (1 0))))]] +chrch_n6 [[1 (1 (1 (1 (1 (1 0)))))]] +chrch_n7 [[1 (1 (1 (1 (1 (1 (1 0))))))]] +chrch_n8 [[1 (1 (1 (1 (1 (1 (1 (1 0)))))))]] +chrch_n9 [[1 (1 (1 (1 (1 (1 (1 (1 (1 0))))))))]] +chrch_add [[[[3 1 (2 1 0)]]]] +chrch_mul [[[2 (1 0)]]] +chrch_pow [[0 1]] + +:test chrch_add chrch_n2 chrch_n3 = chrch_n5 +:test chrch_mul chrch_n2 chrch_n3 = chrch_n6 +:test chrch_pow chrch_n2 chrch_n3 = chrch_n8 + +# ================== +# Lennart +# From Lambda-n-ways +# ================== + +lnnrt_true [[0]] +lnnrt_false [[1]] +lnnrt_if [[[2 0 1]]] +lnnrt_zero [[1]] +lnnrt_succ [[[0 2]]] +lnnrt_one lnnrt_succ lnnrt_zero +lnnrt_two lnnrt_succ lnnrt_one +lnnrt_three lnnrt_succ lnnrt_two +lnnrt_const [[1]] +lnnrt_pair [[[0 2 1]]] +lnnrt_fst [[1 0 [[1]]]] +lnnrt_snd [[1 0 [[0]]]] +lnnrt_fix [[1 (0 0)] [1 (0 0)]] +lnnrt_add lnnrt_fix [[[1 0 [lnnrt_succ (3 0 1)]]]] +lnnrt_mul lnnrt_fix [[[1 lnnrt_zero [lnnrt_add 1 (3 0 1)]]]] +lnnrt_fac lnnrt_fix [[0 lnnrt_one [lnnrt_mul 1 (2 0)]]] +lnnrt_eqnat lnnrt_fix [[[1 (0 lnnrt_true (lnnrt_const lnnrt_false)) [1 lnnrt_false [4 1 0]]]]] +lnnrt_sumto lnnrt_fix [[0 lnnrt_zero [lnnrt_add 1 (2 0)]]] +lnnrt_n5 lnnrt_add lnnrt_two lnnrt_three +lnnrt_n6 lnnrt_add lnnrt_three lnnrt_three +lnnrt_n17 lnnrt_add lnnrt_n6 (lnnrt_add lnnrt_n6 lnnrt_n5) +lnnrt_n37 lnnrt_succ (lnnrt_mul lnnrt_n6 lnnrt_n6) +lnnrt_n703 lnnrt_sumto lnnrt_n37 +lnnrt_n720 lnnrt_fac lnnrt_n6 + +# this test can take a minute, comment it if you're in a hurry +:test lnnrt_eqnat lnnrt_n720 (lnnrt_add lnnrt_n703 lnnrt_n17) = lnnrt_true + +main [[1]] |