diff options
author | Marvin | 2023-09-19 17:32:36 +0200 |
---|---|---|
committer | GitHub | 2023-09-19 17:32:36 +0200 |
commit | 457b31355be1a5ce2086c43126f35e91b5a2cbdc (patch) | |
tree | 365fbf42ce9c0a218f66b8f410eb992aae845821 /src/Transpile.hs | |
parent | 1ec6f5b8e86ce9265b7bdcd1d5a9e1b4ca29afd5 (diff) | |
parent | 8a8f82d20803bc6a9d626d337d0021db55804e5c (diff) |
Merge pull request #1 from marvinborner/transpiler
Transpiler
Diffstat (limited to 'src/Transpile.hs')
-rw-r--r-- | src/Transpile.hs | 94 |
1 files changed, 94 insertions, 0 deletions
diff --git a/src/Transpile.hs b/src/Transpile.hs new file mode 100644 index 0000000..d1dc077 --- /dev/null +++ b/src/Transpile.hs @@ -0,0 +1,94 @@ +-- 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 + , transpileBirb + ) where + +import Term +import Utils + +data SKI = S | K | I | AppSKI SKI SKI | IdxSKI Int + deriving (Eq, Ord) + +data Birb = Swan | Kool | Idiot | Quacky + deriving (Eq, Ord) + +instance Show Birb where + showsPrec _ Swan = showString "\x1F9A2" + showsPrec _ Kool = showString "\x1F425" + showsPrec _ Idiot = showString "\x1F426" + showsPrec _ Quacky = showString "\x1F986" + +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) + +fromSKI :: SKI -> Birb +fromSKI S = Swan +fromSKI K = Kool +fromSKI I = Idiot +fromSKI _ = invalid + +jotify :: SKI -> [Bool] +jotify = reverse . go + 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 + +dejotify :: [Bool] -> SKI +dejotify (False : js) = AppSKI (AppSKI (dejotify js) S) K +dejotify (True : js) = AppSKI S (AppSKI K (dejotify js)) +dejotify _ = I + +transpileBirb :: SKI -> [Birb] +transpileBirb = go . dejotify . jotify + where + go (AppSKI a b) = case [a, b] of + [AppSKI x l, r] -> [Idiot, Idiot] ++ go x ++ [fromSKI l, fromSKI r] + [l, AppSKI r x] -> [Idiot, Quacky] ++ go x ++ [fromSKI r, fromSKI l] + [l, r] -> [fromSKI l, fromSKI r] + go (IdxSKI _) = invalid + go s = [fromSKI s] |