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
|
{-# LANGUAGE LambdaCase #-}
module Term
( Term(..)
, fromBLC
, nf
) where
import Control.Concurrent.MVar
import Data.List ( elemIndex )
import Data.Map.Strict ( Map )
import qualified Data.Map.Strict as Map
import Data.Maybe ( fromMaybe )
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'
-- RKNL abstract machine, call-by-need reducer
-- written for my bruijn programming language
type Store = Map Int Box
type Stack = [Redex]
newtype NameGen = NameGen Int
data BoxValue = Todo Redex | Done Redex | Empty
newtype Box = Box (MVar BoxValue)
data Ridx = Num Int | Hole
data Redex = Rabs Int Redex | Rapp Redex Redex | Ridx Ridx | Rclosure Redex Store | Rcache Box Redex
data Conf = Econf NameGen Redex Store Stack | Cconf NameGen Stack Redex | End
nextName :: NameGen -> (Int, NameGen)
nextName (NameGen x) = (x, NameGen $ x + 1)
toRedex :: Term -> Redex
toRedex = convertWorker (NameGen 1) []
where
convertWorker g ns (Abs e) =
let (v, g') = nextName g
t = convertWorker g' (v : ns) e
in Rabs v t
convertWorker g ns (App l r) =
let lhs = convertWorker g ns l
rhs = convertWorker g ns r
in Rapp lhs rhs
convertWorker _ ns (Idx i) =
Ridx $ Num (if i < 0 || i >= length ns then i else ns !! i)
fromRedex :: Redex -> Term
fromRedex = convertWorker []
where
convertWorker es (Rabs n e) = Abs $ convertWorker (n : es) e
convertWorker es (Rapp l r) =
let lhs = convertWorker es l
rhs = convertWorker es r
in App lhs rhs
convertWorker es (Ridx (Num n)) = Idx $ fromMaybe n (elemIndex n es)
convertWorker _ _ = invalid
transition :: Conf -> IO Conf
transition (Econf g (Rapp u v) e s) =
pure $ Econf g u e (Rapp (Ridx Hole) (Rclosure v e) : s)
transition (Econf g (Rabs x t) e s) = do
box <- newMVar Empty
pure $ Cconf g s (Rcache (Box box) (Rclosure (Rabs x t) e))
transition (Econf g (Ridx (Num x)) e s) = do
def <- newMVar $ Done $ Ridx $ Num x
let b@(Box m) = Map.findWithDefault (Box def) x e
rd <- readMVar m
case rd of
Todo (Rclosure v e') -> pure $ Econf g v e' (Rcache b (Ridx Hole) : s)
Done t -> pure $ Cconf g s t
_ -> invalid
transition (Cconf g ((Rcache (Box m) (Ridx Hole)) : s) t) = do
modifyMVar_ m (\_ -> pure $ Done t)
pure $ Cconf g s t
transition (Cconf g ((Rapp (Ridx Hole) ve) : s) (Rcache _ (Rclosure (Rabs x t) e)))
= do
box <- newMVar (Todo ve)
pure $ Econf g t (Map.insert x (Box box) e) s
transition (Cconf g s (Rcache (Box m) (Rclosure (Rabs x t) e))) = do
rd <- readMVar m
case rd of
Done v -> pure $ Cconf g s v
Empty -> do
let (x1, g') = nextName g
box <- newMVar $ Done $ Ridx $ Num x1
pure $ Econf g'
t
(Map.insert x (Box box) e)
(Rabs x1 (Ridx Hole) : Rcache (Box m) (Ridx Hole) : s)
Todo _ -> invalid
transition (Cconf g ((Rapp (Ridx Hole) (Rclosure v e)) : s) t) =
pure $ Econf g v e (Rapp t (Ridx Hole) : s)
transition (Cconf g ((Rapp t (Ridx Hole)) : s) v) = pure $ Cconf g s (Rapp t v)
transition (Cconf g ((Rabs x1 (Ridx Hole)) : s) v) =
pure $ Cconf g s (Rabs x1 v)
transition (Cconf _ [] _) = pure End
transition _ = invalid
forEachState :: Conf -> (Conf -> IO Conf) -> IO Conf
forEachState conf trans = trans conf >>= \case
End -> pure conf
next -> forEachState next trans
-- TODO: NameGen is arbitrary to not conflict with toRedex
loadTerm :: Redex -> Conf
loadTerm t = Econf (NameGen 1000000) t Map.empty []
nf :: Term -> IO Term
nf e = do
let redex = toRedex e
forEachState (loadTerm redex) transition >>= \case
Cconf _ [] v -> pure $ fromRedex v
_ -> invalid
|
