diff options
| -rw-r--r-- | app/Main.hs | 4 | ||||
| -rw-r--r-- | readme.md | 2 | ||||
| -rw-r--r-- | src/Lib.hs | 45 | ||||
| -rw-r--r-- | src/Term.hs | 48 | ||||
| -rw-r--r-- | src/Transpile.hs | 69 |
5 files changed, 120 insertions, 48 deletions
diff --git a/app/Main.hs b/app/Main.hs index 004d079..9c62589 100644 --- a/app/Main.hs +++ b/app/Main.hs @@ -14,7 +14,9 @@ transpile = do let term = fromBLC file putStrLn $ "input: " ++ show term let ski = transpileSKI term - putStrLn $ "transpiled: " ++ show ski + putStrLn $ "SKI transpiled: " ++ show ski + let birb = transpileBirb ski + putStrLn $ "Birb transpiled: " ++ show birb return () reduce :: IO () @@ -127,7 +127,7 @@ sometimes manually converted the term back to birbs. Birb is Turing complete, since one can construct any term of the [Jot](https://esolangs.org/wiki/Jot) variant of Iota. A Jot term `((X s) k)` is equivalent to `🐦X🦢🐥`. Similarly, `(s (k X))` is -equivalent to `🐦🐦🐧🦢🐥X`. This can be extended for arbitrary long terms +equivalent to `🐦🦆X🐥🦢`. This can be extended for arbitrary long terms using increasingly more complicated construction of composition combinators. @@ -14,12 +14,6 @@ import Data.Bifunctor ( first import Data.Char ( digitToInt , isDigit ) -import Data.IORef ( IORef - , modifyIORef - , newIORef - , readIORef - , writeIORef - ) import Data.Map ( Map ) import qualified Data.Map as Map import Term @@ -49,45 +43,6 @@ termify m s = foldlr (odd $ length lst) lst foldlr False (x : xs) = let t = foldlr True xs in App x t foldlr _ _ = invalid -shift :: Int -> Term -> Term -shift i (Idx j) | i <= j = Idx $ j + 1 - | otherwise = Idx j -shift i (App a b) = App (shift i a) (shift i b) -shift i (Abs a ) = Abs (shift (i + 1) a) - -subst :: Int -> Term -> Term -> Term -subst i (Idx j) c | i == j = c - | j > i = Idx $ j - 1 - | otherwise = Idx j -subst i (App a b) c = App (subst i a c) (subst i b c) -subst i (Abs a ) c = Abs (subst (i + 1) a (shift 0 c)) - -nf :: Term -> IO Term -nf o = do -- TODO: pointfree?? - -- i <- newIORef 1000 - i <- newIORef 100000000 - go i o - where - go :: IORef Integer -> Term -> IO Term - go i t = do -- oracle - readIORef i >>= \case - -- 0 -> writeIORef i (-1) >> return (Idx 0) - 0 -> do - putStrLn "💥 potential infinite loop, continue? [yn]" - getLine >>= \case - "y" -> writeIORef i (-2) >> re i t - "n" -> writeIORef i (-1) >> return t - _ -> go i t - (-1) -> return t - _ -> modifyIORef i (subtract 1) >> re i t - - re :: IORef Integer -> Term -> IO Term - re i (App l r) = go i l >>= \case - Abs t -> go i (subst 0 t r) - t -> App t <$> go i r - re i (Abs t) = Abs <$> go i t - re _ t = pure t - fromBirbs :: String -> Term fromBirbs s = let birbsies = Map.fromList $ second parse <$> birbs diff --git a/src/Term.hs b/src/Term.hs index 081363d..c2a47f1 100644 --- a/src/Term.hs +++ b/src/Term.hs @@ -1,8 +1,17 @@ +{-# LANGUAGE LambdaCase #-} + module Term ( Term(..) , fromBLC + , nf ) where +import Data.IORef ( IORef + , modifyIORef + , newIORef + , readIORef + , writeIORef + ) import Utils data Term = Abs Term | App Term Term | Idx Int @@ -32,3 +41,42 @@ fromBLC' inp = case inp of fromBLC :: String -> Term fromBLC = fst . fromBLC' + +shift :: Int -> Term -> Term +shift i (Idx j) | i <= j = Idx $ j + 1 + | otherwise = Idx j +shift i (App a b) = App (shift i a) (shift i b) +shift i (Abs a ) = Abs (shift (i + 1) a) + +subst :: Int -> Term -> Term -> Term +subst i (Idx j) c | i == j = c + | j > i = Idx $ j - 1 + | otherwise = Idx j +subst i (App a b) c = App (subst i a c) (subst i b c) +subst i (Abs a ) c = Abs (subst (i + 1) a (shift 0 c)) + +nf :: Term -> IO Term +nf o = do -- TODO: pointfree?? + -- i <- newIORef 1000 + i <- newIORef 100000000 + go i o + where + go :: IORef Integer -> Term -> IO Term + go i t = do -- oracle + readIORef i >>= \case + -- 0 -> writeIORef i (-1) >> return (Idx 0) + 0 -> do + putStrLn "💥 potential infinite loop, continue? [yn]" + getLine >>= \case + "y" -> writeIORef i (-2) >> re i t + "n" -> writeIORef i (-1) >> return t + _ -> go i t + (-1) -> return t + _ -> modifyIORef i (subtract 1) >> re i t + + re :: IORef Integer -> Term -> IO Term + re i (App l r) = go i l >>= \case + Abs t -> go i (subst 0 t r) + t -> App t <$> go i r + re i (Abs t) = Abs <$> go i t + re _ t = pure t diff --git a/src/Transpile.hs b/src/Transpile.hs index 2b8134f..3c0c1dc 100644 --- a/src/Transpile.hs +++ b/src/Transpile.hs @@ -1,8 +1,75 @@ +-- This code partly uses algorithms created by John Tromp. +-- Since they did not license their code (afaik), I assume it's okay to reuse it. + module Transpile ( transpileSKI + , transpileBirb ) where import Term +import Utils + +data SKI = S | K | I | AppSKI SKI SKI | IdxSKI Int + deriving (Eq, Ord) + +data Birb = Swan | Kool | Bird | Quacky + deriving (Eq, Ord, Show) + +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' -- && freeIn (==0) e1 + = + 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 t = t +transpileSKI (Idx i ) = IdxSKI i +transpileSKI (App m n) = AppSKI (transpileSKI m) (transpileSKI n) +transpileSKI (Abs m ) = abstract (transpileSKI m) + +fromSKI :: SKI -> Birb +fromSKI S = Swan +fromSKI K = Kool +fromSKI I = Bird +fromSKI _ = invalid + +transpileBirb :: SKI -> [Birb] +transpileBirb (AppSKI a b) = case [a, b] of + [AppSKI x l, AppSKI y r] -> invalid -- TODO + [AppSKI x l, r] -> [Bird, Bird] ++ transpileBirb x ++ [fromSKI a, fromSKI b] + [l, AppSKI r x] -> + [Bird, Quacky] ++ transpileBirb x ++ [fromSKI r, fromSKI l] + [l, r] -> [fromSKI l, fromSKI r] +transpileBirb (IdxSKI _) = invalid +transpileBirb s = [fromSKI s] |