1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
|
{-# LANGUAGE LambdaCase #-}
module Main
( main
) where
import Data.Bifunctor ( first
, second
)
import Data.Char ( digitToInt
, isDigit
)
import Data.IORef
import Data.Map ( Map )
import qualified Data.Map as Map
import System.Environment ( getArgs )
data Term = Abs Term | App Term Term | Idx Int
deriving (Eq, Ord)
type Birb = Char
invalid :: a
invalid = error "invalid program state"
instance Show Term where
showsPrec _ (Abs body) = showString "[" . shows body . showString "]"
showsPrec _ (App lhs rhs) =
showString "(" . shows lhs . showString " " . shows rhs . showString ")"
showsPrec _ (Idx i) = shows i
birbify :: Term -> Map Term Birb -> String
birbify t m | t `Map.member` m = [Map.findWithDefault invalid t m]
| (Abs a) <- t = "[" ++ birbify a m ++ "]"
| (App l r) <- t = "(" ++ birbify l m ++ " " ++ birbify r m ++ ")"
| (Idx i) <- t = show i
termify :: String -> Map Birb Term -> Term
termify s m = foldlr (odd $ length lst) lst
where
go [c ] = [Map.findWithDefault invalid c m]
go (c : cs) = go [c] ++ go cs
go _ = invalid
lst = go s
-- TODO: Rewrite so last/init aren't needed
foldlr :: Bool -> [Term] -> Term
foldlr _ [x] = x
foldlr _ [x, y] = App x y
foldlr True xs = let t = foldlr False (init xs) in App t (last xs)
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 t = do -- TODO: pointfree??
i <- newIORef 100000000
go i t
where
go :: IORef Integer -> Term -> IO Term
go i t = do -- oracle
readIORef i >>= \case
0 -> do
putStrLn "💥 potential infinite loop, continue? [yn]"
getLine >>= \case
"y" -> writeIORef i (-2) >> re i t
_ -> return 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
filtered = filter (`Map.member` birbsies) s
term = termify filtered birbsies
in term
fromTerm :: Term -> String
fromTerm t =
let flipped = (\(a, b) -> (b, a)) <$> birbs
termsies = Map.fromList $ first parse <$> flipped
in birbify t termsies
main :: IO ()
main = do
args <- getArgs
file <- readFile (head args)
let birbified = fromBirbs file
let retermified = fromTerm birbified
putStrLn $ "input: " ++ retermified
normalBirbs <- nf birbified
let rebirbified = fromTerm normalBirbs
putStrLn $ "reduced: " ++ rebirbified
return ()
-- this isn't really relevant but I'm too lazy to type the terms manually
parse :: String -> Term
parse = fst . go
where
go ('!' : cs) = let (t, cs') = go cs in (Abs t, cs')
go ('@' : cs) =
let (l, cs' ) = go cs
(r, cs'') = go cs'
in (App l r, cs'')
go (i : cs) | isDigit i = (Idx $ digitToInt i, cs)
go _ = invalid
birbs :: [(Birb, String)]
birbs =
[ ('\x1F426', "!0") -- bird
, ('\x1F54A', "!!!!@@32@10") -- dove
, ('\x1F424', "!!@0@@110") -- chick
, ('\x1F425', "!!1") -- front chick
, ('\x1F423', "!!!@0@21") -- hatching chick
, ('\x1F989', "!!@0@10") -- owl
, ('\x1F986', "!!@0@12") -- duck
, ('\x1F9A4', "!@!@1@00!@1@00") -- dodo
, ('\x1F9A9', "!!!@@201") -- flamingo
, ('\x1F9A2', "!!!@@20@10") -- swan
, ('\x1FABD', "!!!!@@3@20@10") -- wing
, ('\x1F99A', "!!!@1@20") -- peacock
, ('\x1F99C', "!@00") -- parrot
, ('\x1F985', "!!!!!@@43@@210") -- eagle
, ('\x1F427', "!!!@2@10") -- penguin
-- , ('\x1FAB6', "") -- feather
-- , ('\x1F413', "") -- rooster
-- , ('\x1F414', "") -- chicken
-- , ('\x1F983', "") -- turkey
]
|
