diff options
| -rw-r--r-- | src/Eval.hs | 12 | ||||
| -rw-r--r-- | src/Helper.hs | 28 | ||||
| -rw-r--r-- | src/Parser.hs | 26 | ||||
| -rw-r--r-- | src/Reducer.hs | 2 | ||||
| -rw-r--r-- | std.bruijn | 107 | ||||
| -rw-r--r-- | test.bruijn | 14 |
6 files changed, 167 insertions, 22 deletions
diff --git a/src/Eval.hs b/src/Eval.hs index c40a118..47ca4ca 100644 --- a/src/Eval.hs +++ b/src/Eval.hs @@ -78,8 +78,16 @@ evalRepl line env = case parse parseReplLine "REPL" line of let (res, env') = evalExp exp `runState` env in outputStrLn (case res of - Left err -> show err - Right exp -> (show exp) <> "\n-> " <> (show $ reduce exp) + Left err -> show err + Right exp -> + "<> " + <> (show exp) + <> "\n*> " + <> (show reduced) + <> "\t(" + <> (show $ ternaryToDecimal reduced) + <> ")" + where reduced = reduce exp ) >> pure env Load path -> diff --git a/src/Helper.hs b/src/Helper.hs index a8e393e..5e02a94 100644 --- a/src/Helper.hs +++ b/src/Helper.hs @@ -18,9 +18,35 @@ data Instruction = Define String Expression | Evaluate Expression | Comment Stri deriving (Show) instance Show Expression where show (Bruijn x ) = show x - show (Variable var ) = show var + show (Variable var ) = var show (Abstraction exp ) = "[" <> show exp <> "]" show (Application exp1 exp2) = "(" <> show exp1 <> " " <> show exp2 <> ")" type Environment = [(String, Expression)] type Program = State Environment + +-- Dec to Bal3 in Bruijn encoding: reversed application with 1=>0; 0=>1; T=>2; end=>3 +-- e.g. 0=0=[[[[3]]]]; 2=1T=[[[[2 (0 3)]]]] -5=T11=[[[[0 (0 (2 3))]]]] +decimalToTernary :: Integer -> Expression +decimalToTernary n = + Abstraction $ Abstraction $ Abstraction $ Abstraction $ gen n + where -- TODO: Consider switching 0 and 1 for better readability + fix 0 = 1 + fix 1 = 0 + fix 2 = 2 + gen 0 = Bruijn 3 + gen n = Application (Bruijn $ fix $ mod n 3) (gen $ div (n + 1) 3) + +ternaryToDecimal :: Expression -> Integer +ternaryToDecimal exp = sum $ zipWith (*) (resolve exp) (iterate (* 3) 1) + where + multiplier (Bruijn 0) = 1 + multiplier (Bruijn 1) = 0 + multiplier (Bruijn 2) = (-1) + resolve' (Application x@(Bruijn _) (Bruijn 3)) = [multiplier x] + resolve' (Application fst@(Bruijn _) rst@(Application _ _)) = + (multiplier fst) : (resolve' rst) + resolve' _ = [0] + resolve (Abstraction (Abstraction (Abstraction (Abstraction n)))) = + resolve' n + resolve _ = [0] diff --git a/src/Parser.hs b/src/Parser.hs index 1669bcd..6fbeca4 100644 --- a/src/Parser.hs +++ b/src/Parser.hs @@ -1,5 +1,9 @@ -module Parser where +module Parser + ( parseLine + , parseReplLine + ) where +import Control.Monad ( ap ) import Data.Functor.Identity import Helper import Text.Parsec @@ -8,8 +12,8 @@ import qualified Text.Parsec.Token as Token languageDef :: GenLanguageDef String u Identity languageDef = emptyDef { Token.commentLine = "#" - , Token.identStart = letter - , Token.identLetter = alphaNum <|> char '?' + , Token.identStart = letter <|> char '_' + , Token.identLetter = alphaNum <|> oneOf "?!'_" , Token.reservedOpNames = ["[", "]", "="] } @@ -49,6 +53,16 @@ parseBruijn = do spaces pure $ Bruijn $ (read . pure) idx +parseNumeral :: Parser Expression +parseNumeral = do + num <- number + spaces + pure $ decimalToTernary num + where + sign = (char '-' >> return negate) <|> (char '+' >> return id) + nat = read <$> many1 digit + number = ap sign nat + parseVariable :: Parser Expression parseVariable = do var <- identifier @@ -57,7 +71,11 @@ parseVariable = do parseSingleton :: Parser Expression parseSingleton = - parseBruijn <|> parseAbstraction <|> parens parseApplication <|> parseVariable + parseBruijn + <|> parseNumeral + <|> parseAbstraction + <|> parens parseApplication + <|> parseVariable parseExpression :: Parser Expression parseExpression = do diff --git a/src/Reducer.hs b/src/Reducer.hs index 0760a82..809687b 100644 --- a/src/Reducer.hs +++ b/src/Reducer.hs @@ -4,7 +4,7 @@ module Reducer import Helper --- TODO: Reduce variable -> later: only reduce main in non-repl +-- TODO: Research interaction nets and optimal reduction (<+>) :: Expression -> Int -> Expression (<+>) (Bruijn x ) n = if x > n then Bruijn (pred x) else Bruijn x diff --git a/std.bruijn b/std.bruijn new file mode 100644 index 0000000..16d851a --- /dev/null +++ b/std.bruijn @@ -0,0 +1,107 @@ +# ================== +# Common combinators +# ================== + +S [[[2 0 (1 0)]]] +K [[1]] +I [0] +B [[[2 (1 0)]]] +C [[[2 0 1]]] +T [[1]] +F [[0]] +ω [0 0] +Ω ω ω +Y [[1 (0 0)] [1 (0 0)]] +Θ [[0 (1 1 0)]] [[0 (1 1 0)]] +i [0 S K] + +# ======= +# Ternary +# ======= + +zero? [0 T [F] I [F]] +upNeg [[[[[2 (4 3 2 1 0)]]]]] +upZero [[[[[1 (4 3 2 1 0)]]]]] +upPos [[[[[0 (4 3 2 1 0)]]]]] +up [[[[[[5 2 1 0 (4 3 2 1 0)]]]]]] + +negate [[[[[4 3 0 1 2]]]]] + +tritNeg [[[2]]] +tritZero [[[1]]] +tritPos [[[0]]] + +_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 ω _normalize + +_eqZero? [zero? (normalize 0)] +_eqNeg [[0 F [2 0] [F] [F]]] +_eqZero [[0 (1 0) [F] [2 0] [F]]] +_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))] +_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))] +_addBPos2 [1 (upPos (3 0 tritZero)) (upNeg (3 0 tritPos)) (upZero (3 0 tritPos))] +_addANeg [[[1 (_addBNeg 1) _addBNeg2 _addBNeg _addBZero]]] +_addAZero [[[1 (_addBZero 1) _addBNeg _addBZero _addBPos]]] +_addAPos [[[1 (_addBPos 1) _addBZero _addBPos _addBPos2]]] +_addAbs [_addC (0 _addZ _addANeg _addAZero _addAPos)] +add [[_addAbs 1 (abstractify 0)]] + +sub [[add 1 (negate 0)]] + +# ===== +# Pairs +# ===== + +pair [[[0 2 1]]] +fst [0 T] +snd [0 F] + +# =============== +# Boolean algebra +# =============== + +not [0 F T] +and [[1 0 F]] +or [[1 T 0]] +xor [[1 (not 0) 0]] +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]] + +main I F diff --git a/test.bruijn b/test.bruijn deleted file mode 100644 index cd5133b..0000000 --- a/test.bruijn +++ /dev/null @@ -1,14 +0,0 @@ -# Church numerals -zero [[0]] -succ [[[1 (2 1 0)]]] -add [[[[3 1 (2 1 0)]]]] -mul [[[2 (1 0)]]] -exp [[0 1]] - -Y [[1 (0 0)] [1 (0 0)]] - -true [[1]] -false [[0]] -id [0] -iota [0 [[[2 0 (1 0)]]] [[1]]] -main id false |