Transpilation

5 files changed, 105 insertions, 9 deletions

diff --git a/app/Main.hs b/app/Main.hs
index c1f1c2d..cbcaeac 100644
--- a/app/Main.hs
+++ b/app/Main.hs
@@ -1,5 +1,3 @@
-{-# LANGUAGE LambdaCase #-}
-
 module Main
   ( main
   ) where
@@ -7,6 +5,15 @@ module Main
 import           Lib
 import           System.Environment             ( getArgs )
 import           Term
+import           Transpile
+
+transpile :: String -> IO ()
+transpile path = do
+  file <- readFile path
+  let term    = fromBLC file
+  let ski     = transpileSKI term
+  let jottary = transpileJottary ski
+  putStrLn jottary
 
 reduce :: String -> IO ()
 reduce path = do
@@ -20,5 +27,6 @@ main :: IO ()
 main = do
   args <- getArgs
   case args of
-    ["reduce", path] -> reduce path
-    _                -> putStrLn "Usage: jottary [transpile|reduce] <file>"
+    ["transpile", path] -> transpile path
+    ["reduce"   , path] -> reduce path
+    _                   -> putStrLn "Usage: jottary [transpile|reduce] <file>"
diff --git a/jottary.cabal b/jottary.cabal
index c633640..96bf72e 100644
--- a/jottary.cabal
+++ b/jottary.cabal
@@ -25,6 +25,7 @@ library
   exposed-modules:
       Lib
       Term
+      Transpile
       Utils
   other-modules:
       Paths_jottary
diff --git a/readme.md b/readme.md
index fb5691a..c186d99 100644
--- a/readme.md
+++ b/readme.md
@@ -7,6 +7,9 @@ better Gödel-numbering than its sister language
 Read my [blog post](https://text.marvinborner.de/2023-10-05-15.html) for
 more information.
 
+This project is basically just a slightly modified version of
+[birb](https://github.com/marvinborner/birb).
+
 ## Performance
 
 The [bruijn
@@ -25,3 +28,21 @@ $ hyperfine "jottary reduce <(printf '1%.0s' {1..503})"
   Time (mean ± σ):      10.8 ms ±   0.7 ms    [User: 1.7 ms, System: 9.0 ms]
   Range (min … max):     9.5 ms …  12.5 ms    163 runs
 ```
+
+## Transpiler
+
+The transpiler converts binary lambda calculus to Jottary. It does this
+by converting to SKI combinators, then to Jot, and finally to Jottary.
+Aside from general inefficiency of LC-SKI conversion, the jottary
+programs will grow *exponentially* compared to its Jot variant. For
+example, the `id` program `0010` gets transpiled to 2089884 unary
+symbols (260KB!).
+
+## Usage
+
+Install Haskell's stack. Then,
+
+-   `stack run -- reduce file.jottary` or
+    `stack run -- reduce <(echo 1111111)`
+-   `stack run -- transpile <(echo 0010)` to transpile the `id` program
+-   `stack install` so you can enjoy `jottary` from anywhere
diff --git a/src/Lib.hs b/src/Lib.hs
index 698c0ae..28d02ba 100644
--- a/src/Lib.hs
+++ b/src/Lib.hs
@@ -1,10 +1,5 @@
-{-# LANGUAGE LambdaCase #-}
-
 module Lib
   ( fromJottary
-  , s
-  , k
-  , i
   ) where
 
 import           Control.Monad                  ( replicateM )
diff --git a/src/Transpile.hs b/src/Transpile.hs
new file mode 100644
index 0000000..9d5a509
--- /dev/null
+++ b/src/Transpile.hs
@@ -0,0 +1,71 @@
+-- This code partly uses algorithms (drip/abstract) created by John Tromp.
+-- Since they did not license their code (afaik), I assume it's okay to reuse it.
+
+module Transpile
+  ( transpileSKI
+  , transpileJottary
+  ) where
+
+import           Term
+import           Utils
+
+data SKI = S | K | I | AppSKI SKI SKI | IdxSKI Int
+  deriving (Eq, Ord)
+
+instance Show SKI where
+  showsPrec _ S = showString "s"
+  showsPrec _ K = showString "k"
+  showsPrec _ I = showString "i"
+  showsPrec _ (AppSKI x y) =
+    showString "(" . shows x . showString " " . shows y . showString ")"
+  showsPrec _ (IdxSKI i) = shows i
+
+drip :: SKI -> SKI
+drip i@(AppSKI (AppSKI S K) _) = i
+drip (  IdxSKI 0             ) = invalid
+drip (  IdxSKI i             ) = IdxSKI (i - 1)
+drip (  AppSKI x y           ) = AppSKI (drip x) (drip y)
+drip x                         = x
+
+abstract :: SKI -> SKI
+abstract (AppSKI sk@(AppSKI S K) _) = sk
+abstract e = if freeIn (== 0) e then occabstract e else AppSKI K (drip e) where
+  freeIn _  (AppSKI (AppSKI S K) _) = False
+  freeIn fv (AppSKI x            y) = freeIn fv x || freeIn fv y
+  freeIn fv (IdxSKI i             ) = fv i
+  freeIn _  _                       = False
+  isConst = not . freeIn (const True)
+  occabstract (IdxSKI 0) = I
+  occabstract (AppSKI m (IdxSKI 0)) | not (freeIn (== 0) m) = drip m
+  occabstract (AppSKI (AppSKI l m) l') | l == l' =
+    occabstract (AppSKI (AppSKI (AppSKI (AppSKI S S) K) l) m)
+  occabstract (AppSKI m (AppSKI n l)) | isConst m && isConst n =
+    occabstract (AppSKI (AppSKI (AppSKI S (abstract m)) n) l)
+  occabstract (AppSKI (AppSKI m n) l) | isConst m && isConst l =
+    occabstract (AppSKI (AppSKI (AppSKI S m) (abstract l)) n)
+  occabstract (AppSKI (AppSKI m l) (AppSKI n l'))
+    | l == l' && isConst m && isConst n = occabstract
+      (AppSKI (AppSKI (AppSKI S m) n) l)
+  occabstract (AppSKI e1 e2) = AppSKI (AppSKI S (abstract e1)) (abstract e2)
+  occabstract _              = invalid
+
+transpileSKI :: Term -> SKI
+transpileSKI (Idx i  ) = IdxSKI i
+transpileSKI (App m n) = AppSKI (transpileSKI m) (transpileSKI n)
+transpileSKI (Abs m  ) = abstract (transpileSKI m)
+
+fromBinary :: [Bool] -> Int
+fromBinary (x : xs) = fromEnum x + 2 * fromBinary xs
+fromBinary []       = 0
+
+jottarify :: SKI -> Int
+jottarify s = fromBinary (reverse $ True : go s) - 1
+ where
+  go S            = [True, True, True, True, True, False, False, False]
+  go K            = [True, True, True, False, False]
+  go I            = go $ AppSKI (AppSKI S K) K
+  go (AppSKI a b) = True : (go a ++ go b)
+  go _            = invalid
+
+transpileJottary :: SKI -> String
+transpileJottary s = replicate (jottarify s) '1'