Got some things working

7 files changed, 169 insertions, 131 deletions

diff --git a/bruijn.cabal b/bruijn.cabal
index 7501764..139f41e 100644
--- a/bruijn.cabal
+++ b/bruijn.cabal
@@ -18,6 +18,7 @@ extra-source-files:
     README.md
 data-files:
     config
+    std.bruijn
 
 source-repository head
   type: git
@@ -38,9 +39,11 @@ library
       LambdaCase
   build-depends:
       base >=4.7 && <5
+    , binary
     , bitstring
     , bytestring
     , containers
+    , directory
     , haskeline
     , megaparsec
     , mtl
@@ -57,10 +60,12 @@ executable bruijn
   ghc-options: -threaded -rtsopts -with-rtsopts=-N
   build-depends:
       base >=4.7 && <5
+    , binary
     , bitstring
     , bruijn
     , bytestring
     , containers
+    , directory
     , haskeline
     , megaparsec
     , mtl
@@ -78,10 +83,12 @@ test-suite bruijn-test
   ghc-options: -threaded -rtsopts -with-rtsopts=-N
   build-depends:
       base >=4.7 && <5
+    , binary
     , bitstring
     , bruijn
     , bytestring
     , containers
+    , directory
     , haskeline
     , megaparsec
     , mtl
diff --git a/package.yaml b/package.yaml
index 567249c..9f83342 100644
--- a/package.yaml
+++ b/package.yaml
@@ -11,6 +11,7 @@ extra-source-files:
 
 data-files:
 - config
+- std.bruijn
 
 # Metadata used when publishing your package
 # synopsis:            Short description of your package
@@ -30,8 +31,10 @@ dependencies:
 - haskeline
 - megaparsec
 - containers
+- directory
 - bytestring
 - bitstring
+- binary
 
 library:
   source-dirs: src
diff --git a/src/Binary.hs b/src/Binary.hs
index 974bf8d..2a1c891 100644
--- a/src/Binary.hs
+++ b/src/Binary.hs
@@ -20,24 +20,8 @@ toBinary (Bruijn      x        ) = (replicate (x + 1) '1') ++ "0"
 toBinary (Abstraction exp      ) = "00" ++ toBinary exp
 toBinary (Application exp1 exp2) = "01" ++ (toBinary exp1) ++ (toBinary exp2)
 
--- Stolen from John Tromp
--- fromBinary :: String -> Expression
--- fromBinary = foldr
---   (\x -> Abstraction . (Application . Application (Bruijn 0) . code $ x))
---   nil
---  where
---   nil = code '1'
---   code '0' = Abstraction (Abstraction (Bruijn 1))
---   code '1' = Abstraction (Abstraction (Bruijn 0))
---   code x   = fromBinary (showsBin 8 (ord x) "")
---   showsBin n x = if n == 0
---     then id
---     else let (x', b) = divMod x 2 in showsBin (n - 1) x' . (intToDigit b :)
-
--- https://github.com/ljedrz/blc/blob/master/src/encoding/binary.rs
 fromBinary' :: String -> (Expression, String)
 fromBinary' = \case
-  -- "" -> (Bruijn 0, "")
   '0' : '0' : rst ->
     let (exp, rst) = fromBinary' rst in (Abstraction exp, rst)
   '0' : '1' : rst ->
diff --git a/src/Eval.hs b/src/Eval.hs
index ebca545..1c33fa2 100644
--- a/src/Eval.hs
+++ b/src/Eval.hs
@@ -16,6 +16,7 @@ import           Paths_bruijn
 import           Reducer
 import           System.Console.Haskeline
 import           System.Console.Haskeline.Completion
+import           System.Directory
 import           System.Environment
 import           System.Exit
 import           System.IO
@@ -92,24 +93,27 @@ eval (line : ls) state@(EnvState env) isRepl =
                     else eval ls (EnvState env') isRepl
           Import path -> do
             lib    <- getDataFileName path -- TODO: Use actual lib directory
-            exists <- doesFileExist lib
+            exists <- pure False -- doesFileExist lib
             loadFile $ if exists then lib else path
           Evaluate exp ->
             let (res, env') = evalExp exp `runState` env
-            in  putStrLn
-                    (case res of
-                      Left err -> show err
-                      Right exp ->
-                        "<> "
-                          <> (show exp)
-                          <> "\n*> "
-                          <> (show reduced)
-                          <> "\t("
-                          <> (show $ binaryToDecimal reduced)
-                          <> ")"
-                        where reduced = reduce exp
-                    )
-                  >> eval ls state isRepl
+            in
+              putStrLn
+                  (case res of
+                    Left err -> show err
+                    Right exp ->
+                      "<> "
+                        <> (show exp)
+                        <> "\n*> "
+                        <> (show reduced)
+                        <> (if likeTernary reduced
+                             then
+                               "\t(" <> (show $ ternaryToDecimal reduced) <> ")"
+                             else ""
+                           )
+                      where reduced = reduce exp
+                  )
+                >> eval ls state isRepl
           Test exp1 exp2 ->
             let (res, _) = evalTest exp1 exp2 `runState` env
             in  case res of
@@ -201,3 +205,4 @@ evalMain = do
     ["-E", path] -> exec path (try . readFile) id
     ['-' : _]    -> usage
     [path   ]    -> evalFile path print id
+    _            -> usage
diff --git a/src/Helper.hs b/src/Helper.hs
index d45a02b..76a1f83 100644
--- a/src/Helper.hs
+++ b/src/Helper.hs
@@ -24,23 +24,25 @@ instance Show Expression where
 type Environment = [(String, Expression)]
 type Program = State Environment
 
-decimalToBinary :: Integer -> Expression
-decimalToBinary n = Abstraction $ Abstraction $ Abstraction $ Abstraction $ gen
-  n
- where -- TODO: Consider switching 0 and 1 for better readability
-  fix 0 = 1
-  fix 1 = 0
+likeTernary :: Expression -> Bool
+likeTernary (Abstraction (Abstraction (Abstraction (Abstraction _)))) = True
+likeTernary _ = False
+
+-- Dec to Bal3 in Bruijn encoding: reversed application with 0=>0; 1=>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
   gen 0 = Bruijn 3
-  gen 1 = Application (Bruijn 0) (gen 0)
-  gen n | n < 0     = Application (Bruijn 2) (gen (-n))
-        | otherwise = Application (Bruijn $ fix $ mod n 2) (gen $ div n 2)
+  gen n = Application (Bruijn $ fromIntegral $ mod n 3) (gen $ div (n + 1) 3)
 
-binaryToDecimal :: Expression -> Integer
-binaryToDecimal exp = sum $ zipWith (*) (resolve exp) (iterate (* 2) 1)
+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 -- TODO
+  multiplier (Bruijn 0) = 0
+  multiplier (Bruijn 1) = 1
+  multiplier (Bruijn 2) = (-1)
   resolve' (Application x@(Bruijn _) (Bruijn 3)) = [multiplier x]
   resolve' (Application fst@(Bruijn _) rst@(Application _ _)) =
     (multiplier fst) : (resolve' rst)
diff --git a/src/Parser.hs b/src/Parser.hs
index 16f4202..29f40b9 100644
--- a/src/Parser.hs
+++ b/src/Parser.hs
@@ -58,7 +58,7 @@ parseNumeral :: Parser Expression
 parseNumeral = do
   num <- number
   space
-  pure $ decimalToBinary num
+  pure $ decimalToTernary num
  where
   sign :: Parser (Integer -> Integer)
   sign = (char '-' >> return negate) <|> (char '+' >> return id)
diff --git a/std.bruijn b/std.bruijn
index f211a98..377ba8c 100644
--- a/std.bruijn
+++ b/std.bruijn
@@ -31,100 +31,137 @@ pair [[[0 2 1]]]
 fst [0 T]
 snd [0 F]
 
-# ===================================
-# Binary
-# According to works of T.Æ. Mogensen
-# ===================================
+:test fst (pair [[0]] [[1]]) = [[0]]
+:test snd (pair [[0]] [[1]]) = [[1]]
 
 # TODO: contract-like type-checking
 #       like: `+ ... : [[[[# 3]]]]`
 
-# TODO: Fix for negative 4x abstraction
-
-upZero [[[[1 (3 2 1 0)]]]]
-upOne [[[[0 (3 2 1 0)]]]]
-up [[[[[4 1 0 (3 2 1 0)]]]]]
-
-lsb [0 [[[0]]] [[[[0]]]] [[[[1]]]] [[[[0]]]]]
-
-# TODO: almost!
-zero? [0 [[[1]]] [[[[0]]]] [[[[0]]]] [[[[0]]]]]
-
-_succZ pair +0 +1
-_succA [0 [[pair (upZero 1) (upOne 1)]]]
-_succB [0 [[pair (upOne 1) (upZero 0)]]]
-succ [snd (0 _succZ _succA _succB)]
-
-_predZ pair +0 +1
-_predA [0 [[pair (upZero 1) (upOne 0)]]]
-_predB [0 [[pair (upOne 1) (upZero 1)]]]
-pred [snd (0 _predZ _predA _predB)]
-
 # ===================================
 # Ternary
 # According to works of T.Æ. Mogensen
 # ===================================
 
-# 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]]]
-# lst [0 tritZero [tritNeg] [tritZero] [tritPos]]
-# 
-# _stripZ pair +0 T
-# _stripANeg [0 [[pair (0 +0 (upNeg 1)) 0]]]
-# _stripAZero [0 [[pair (upZero 1) F]]]
-# _stripAPos [0 [[pair (upPos 1) F]]]
-# strip [fst (0 _stripZ _stripANeg _stripAZero _stripAPos)]
-# 
-# _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)]] 1]]
-# 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)]]
-# 
-# _addZ [[0 (pred (normalize 1)) (normalize 1) (succ (normalize 1))]]
-# _addC [[1 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))]
-# _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)]]
+zero? [0 T [F] [F] I]
+:test zero? +0 = T
+:test zero? -1 = F
+:test zero? +1 = F
+:test zero? +42 = F
+
+upNeg [[[[[2 (4 3 2 1 0)]]]]]
+:test upNeg +0 = -1
+:test upNeg -1 = -4
+:test upNeg +42 = +125
+
+upPos [[[[[1 (4 3 2 1 0)]]]]]
+:test upPos +0 = +1
+:test upPos -1 = -2
+:test upPos +42 = +127
+
+upZero [[[[[0 (4 3 2 1 0)]]]]]
+:test upZero +0 = [[[[0 3]]]]
+:test upZero +1 = +3
+:test upZero +42 = +126
+
+up [[[[[[5 2 1 0 (4 3 2 1 0)]]]]]]
+# TODO: up is incorrect
+
+negate [[[[[4 3 1 2 0]]]]]
+:test negate +0 = +0
+:test negate -1 = +1
+:test negate +42 = -42
+
+tritNeg [[[2]]]
+tritPos [[[1]]]
+tritZero [[[0]]]
+lst [0 tritZero [tritNeg] [tritPos] [tritZero]]
+:test lst +0 = tritZero
+:test lst -1 = tritNeg
+:test lst +1 = tritPos
+:test lst +42 = tritZero
+
+_stripZ pair +0 T
+_stripANeg [0 [[pair (upNeg 1) F]]]
+_stripAPos [0 [[pair (upPos 1) F]]]
+_stripAZero [0 [[pair (0 +0 (upZero 1)) 0]]]
+strip [fst (0 _stripZ _stripANeg _stripAPos _stripAZero)]
+:test strip [[[[0 3]]]] = +0
+:test strip [[[[2 (0 (0 (0 (0 3))))]]]] = -1
+:test strip +42 = +42
+
+# I believe Mogensen's Paper has an error in its succ/pred definitions.
+# They use 3 abstractions in the _succ* functions, also we use switched +/0
+# in comparison to their implementation, yet the order of neg/pos/zero is
+# the same. Something's weird.
+
+_succZ pair +0 +1
+_succNeg [0 [[pair (upNeg 1) (upZero 1)]]]
+_succZero [0 [[pair (upZero 1) (upPos 1)]]]
+_succPos [0 [[pair (upPos 1) (upNeg 0)]]]
+succ [snd (0 _succZ _succNeg _succPos _succZero)]
+ssucc [strip (succ 0)]
+:test succ -42 = -41
+:test ssucc -1 = +0
+:test succ +0 = +1
+:test succ (succ (succ (succ (succ +0)))) = +5
+:test succ +42 = +43
+
+_predZ pair +0 -1
+_predNeg [0 [[pair (upNeg 1) (upPos 0)]]]
+_predZero [0 [[pair (upZero 1) (upNeg 1)]]]
+_predPos [0 [[pair (upPos 1) (upZero 1)]]]
+pred [snd (0 _predZ _predNeg _predPos _predZero)]
+spred [strip (pred 0)]
+:test pred -42 = -43
+:test pred +0 = -1
+:test spred (pred (pred (pred (pred +5)))) = +0
+:test spred +1 = +0
+:test pred +42 = +41
+
+_absNeg [[[[[2 4]]]]]
+_absPos [[[[[1 4]]]]]
+_absZero [[[[[0 4]]]]]
+abstractify [0 [[[[3]]]] _absNeg _absPos _absZero]
+:test abstractify -3 = [[[[0 [[[[2 [[[[3]]]]]]]]]]]]
+:test abstractify +0 = [[[[3]]]]
+:test abstractify +3 = [[[[0 [[[[1 [[[[3]]]]]]]]]]]]
+
+# solving recursion using Y/ω
+_normalize [[0 +0 [upNeg ([3 3 0] 0)] [upPos ([3 3 0] 0)] [upZero ([3 3 0] 0)]]]
+normalize ω _normalize
+:test normalize [[[[3]]]] = +0
+:test normalize (abstractify +42) = +42
+:test normalize (abstractify -42) = -42
+
+_eqZ [zero? (normalize 0)]
+_eqNeg [[0 F [2 0] [F] [F]]]
+_eqPos [[0 F [F] [2 0] [F]]]
+_eqZero [[0 (1 0) [F] [F] [2 0]]]
+_eqAbs [0 _eqZ _eqNeg _eqPos _eqZero]
+eq [[_eqAbs 1 (abstractify 0)]]
+:test eq -42 -42 = T
+:test eq -1 -1 = T
+:test eq -1 +0 = F
+:test eq +0 +0 = T
+:test eq +1 +0 = F
+:test eq +1 +1 = T
+:test eq +42 +42 = T
+
+# TODO: Much zero/one switching needed
+_addZ [[0 (pred (normalize 1)) (normalize 1) (succ (normalize 1))]]
+_addC [[1 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))]
+_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)]]
 
 # ===============
 # Boolean algebra