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
|
{-# 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
deriving (Eq, Ord)
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
fromBLC' :: String -> (Term, String)
fromBLC' inp = case inp of
'0' : '0' : rst -> let (e, es) = fromBLC' rst in (Abs e, es)
'0' : '1' : rst ->
let (exp1, rst1) = fromBLC' rst
(exp2, rst2) = fromBLC' rst1
in (App exp1 exp2, rst2)
'1' : _ : rst -> binaryBruijn rst
_ -> invalid
where
binaryBruijn rst =
let idx = length (takeWhile (== '1') inp) - 1
in case rst of
"" -> (Idx idx, "")
_ -> (Idx idx, drop idx rst)
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
|
