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
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
169
170
171
172
173
174
175
176
177
178
179
180
181
182
183
184
185
186
187
188
189
190
191
192
193
194
195
196
197
198
199
200
201
202
203
204
205
206
207
208
209
210
211
212
213
214
215
216
217
218
219
220
221
222
223
224
225
226
227
228
229
230
231
232
233
234
235
236
237
238
239
240
241
242
243
244
245
246
247
248
249
250
251
252
253
254
255
256
257
258
259
260
261
262
263
264
265
266
267
268
269
270
271
272
273
274
275
276
277
278
279
280
281
282
283
284
285
286
287
288
289
290
291
292
293
294
295
296
|
{- VAM 2P, done the lazy way -}
module Interpreter where
--import Data.Function
import qualified Data.Map as M
import Code
import IR (Id(..))
prove :: Code -> Defs -> (Interp, Either String Bool)
prove g ds =
let i0 =
Interp
{ defs = ds
, cur =
Cho
{ hed = g
, hvar = emptyScope
, gol = [LastCall]
, gvar = emptyScope
, heap = emptyHeap
, stk = []
, cut = []
}
, cho = []
}
run (Left x) = x
run (Right x) = run $ proveStep Right (\i e -> Left (i, e)) x
in run (Right i0)
data Dereferenced
= FreeRef Int
| BoundRef Int Datum
| NoRef
{- this gonna need Either String Bool for errors later -}
proveStep :: (Interp -> a) -> (Interp -> Either String Bool -> a) -> Interp -> a
proveStep c f i = go i
where
ifail msg = f i $ Left msg
tailcut [LastCall] chos _ = Just chos
tailcut [LastCall, Cut] _ cut = Just cut
tailcut _ _ _ = Nothing
withDef fn
| Just d <- defs i M.!? fn = ($ d)
| otherwise = const $ ifail $ "no definition: " ++ show fn
{- Backtracking -}
backtrack i@Interp {cho = chos}
{- if available, restore the easiest choicepoint -}
| (cho:chos) <- chos = c i {cur = cho, cho = chos}
{- if there's no other choice, answer no -}
| otherwise = f i $ Right False
{- Unification -}
go i@Interp {cur = cur@Cho { hed = U h:hs
, gol = U g:gs
, heap = heap@(Heap _ hmap)
}} = unify h g
{- termination tools -}
where
uok = c i {cur = cur {hed = hs, gol = gs}}
setHeap r x =
c i {cur = cur {hed = hs, gol = gs, heap = writeHeap r x heap}}
{- heap tools -}
deref x =
case hmap M.!? x of
Just (HeapRef x') ->
if x == x'
then FreeRef x'
else deref x'
Just x' -> BoundRef x x'
_ -> NoRef
writeHeap addr x (Heap nxt m) = Heap nxt (M.adjust (const x) addr m)
newHeapVar h = head <$> newHeapVars 1 h
newHeapVars n (Heap nxt m) =
let addrs = [nxt + i - 1 | i <- [1 .. n]]
in ( Heap (nxt + n) $
foldr (uncurry M.insert) m $ zip addrs (map HeapRef addrs)
, addrs)
allocLocal reg scope cont
| Just addr <- scope M.!? reg = cont scope heap addr
| (heap', addr) <- newHeapVar heap =
cont (M.insert reg addr scope) heap' addr
newHeapStruct addr s@(Struct Id {arity = arity}) cont =
let (Heap nxt' m', addrs) = newHeapVars (arity + 1) heap
m'' =
M.insert addr (HeapRef $ head addrs) . M.insert (head addrs) s $
m'
in cont (map HeapRef $ tail addrs) (Heap nxt' m'')
{- simple cases first -}
unify VoidRef VoidRef = uok
unify (Atom a) (Atom b)
| a == b = uok
unify VoidRef (Atom _) = uok
unify (Atom _) VoidRef = uok
unify (Struct a) (Struct b)
| a == b = uok
{- unifying a struct with void must cause us to skip the void -}
unify VoidRef (Struct Id {arity = a}) =
c i {cur = cur {hed = replicate a (U VoidRef) ++ hs, gol = gs}}
unify (Struct Id {arity = a}) VoidRef =
c i {cur = cur {hed = hs, gol = replicate a (U VoidRef) ++ gs}}
{- handle local refs; first ignore their combination with voids to save memory -}
unify (LocalRef _) VoidRef = uok
unify VoidRef (LocalRef _) = uok
{- allocate heap for LocalRefs and retry with HeapRefs -}
unify (LocalRef hv) _ =
allocLocal hv (hvar cur) $ \hvar' heap' addr ->
c
i
{ cur =
cur
{hed = U (HeapRef addr) : hs, hvar = hvar', heap = heap'}
}
unify _ (LocalRef gv) =
allocLocal gv (gvar cur) $ \gvar' heap' addr ->
c
i
{ cur =
cur
{gol = U (HeapRef addr) : gs, gvar = gvar', heap = heap'}
}
{- handle heap refs; first ignore their combination with voids again -}
unify (HeapRef _) VoidRef = uok
unify VoidRef (HeapRef _) = uok
{- actual HeapRefs, these are dereferenced and then unified; decide between copying and linking -}
unify (HeapRef hr') g =
case deref hr' of
FreeRef hr ->
case g of
atom@(Atom _) -> setHeap hr atom
s@(Struct _) ->
newHeapStruct
hr
s
(\nhs nheap ->
c
i
{ cur =
cur
{hed = map U nhs ++ hs, gol = gs, heap = nheap}
})
HeapRef gr' ->
case deref gr' of
FreeRef gr -> setHeap hr (HeapRef gr)
BoundRef addr _ -> setHeap hr (HeapRef addr)
_ -> ifail "dangling goal ref (from head ref)"
BoundRef _ atom@(Atom a) -> unify atom g
BoundRef addr struct@(Struct Id {arity = arity}) ->
c
i
{ cur =
cur
{ hed =
U struct :
[U (HeapRef $ addr + i) | i <- [1 .. arity]] ++ hs
, gol = U g : gs
}
}
_ -> ifail "dangling head ref"
unify h (HeapRef gr') =
case deref gr' of
FreeRef gr ->
case h of
atom@(Atom _) -> setHeap gr atom
s@(Struct _) ->
newHeapStruct
gr
s
(\ngs nheap ->
c
i
{ cur =
cur
{hed = hs, gol = map U ngs ++ gs, heap = nheap}
})
BoundRef _ atom@(Atom b) -> unify h atom
BoundRef addr struct@(Struct Id {arity = arity}) ->
c
i
{ cur =
cur
{ hed = U h : hs
, gol =
U struct :
[U (HeapRef $ addr + i) | i <- [1 .. arity]] ++ gs
}
}
_ -> ifail "dangling goal ref"
unify _ _ = backtrack i
{- Resolution -}
go i@Interp { cur = cur@Cho { hed = hed
, hvar = hvar
, gol = gol
, gvar = gvar
, heap = heap
, stk = stk
, cut = cut
}
, cho = chos
}
{- top-level success -}
| [NoGoal] <- hed
, Just nchos <- tailcut gol chos cut
, [] <- stk =
f i {cur = cur {hed = [], gol = []}, cho = nchos} $ Right True
{- cut before the first goal (this solves all cuts in head) -}
| Cut:hs <- hed = c i {cur = cur {hed = hs}, cho = cut}
{- succeed and return to caller -}
| [NoGoal] <- hed
, Just nchos <- tailcut gol chos cut
, (Goal:U (Struct fn):gs, ngvar, _):ss <- stk =
withDef fn $ \(hs:ohs) ->
c
i
{ cur =
cur
{ hed = hs
, hvar = emptyScope
, gol = gs
, gvar = ngvar
, stk = ss
}
, cho =
[Cho oh emptyScope gs ngvar heap ss nchos | oh <- ohs] ++
nchos
}
{- succeed and return to caller, and the caller wants a cut -}
| [NoGoal] <- hed
, Just _ <- tailcut gol chos cut
, (Cut:Goal:U (Struct fn):gs, ngvar, rchos):ss <- stk =
withDef fn $ \(hs:ohs) ->
c
i
{ cur =
cur
{ hed = hs
, hvar = emptyScope
, gol = gs
, gvar = ngvar
, stk = ss
}
, cho =
[Cho oh emptyScope gs ngvar heap ss rchos | oh <- ohs] ++
rchos
}
{- start matching next goal -}
| [NoGoal] <- hed
, (Call:Goal:U (Struct fn):gs) <- gol =
withDef fn $ \(hs:ohs) ->
c
i
{ cur = cur {hed = hs, hvar = emptyScope, gol = gs}
, cho =
[Cho oh emptyScope gs gvar heap stk chos | oh <- ohs] ++ chos
}
{- start matching next goal after a cut -}
| [NoGoal] <- hed
, (Call:Cut:Goal:U (Struct fn):gs) <- gol =
withDef fn $ \(hs:ohs) ->
c
i
{ cur = cur {hed = hs, hvar = emptyScope, gol = gs}
, cho =
[Cho oh emptyScope gs gvar heap stk cut | oh <- ohs] ++ cut
}
{- goal head matching succeeded, make a normal call -}
| (Goal:U (Struct fn):ngs) <- hed
, (Call:gs) <- gol =
withDef fn $ \(hs:ohs) ->
let nstk = (gs, gvar, chos) : stk
in c i
{ cur =
cur
{ hed = hs
, hvar = emptyScope
, gol = ngs
, gvar = hvar
, stk = nstk
}
, cho =
[Cho oh emptyScope ngs hvar heap nstk chos | oh <- ohs] ++
chos
}
{- successful match continued by tail call -}
| (Goal:U (Struct fn):ngs) <- hed
, Just nchos <- tailcut gol chos cut =
withDef fn $ \(hs:ohs) ->
c
i
{ cur = cur {hed = hs, hvar = emptyScope, gol = ngs, gvar = hvar}
, cho =
[Cho oh emptyScope ngs hvar heap stk nchos | oh <- ohs] ++
nchos
}
{- The End -}
go _ = ifail "code broken: impossible instruction combo"
|
