actually yolo
This commit is contained in:
parent
bb40a4f8ca
commit
b1fef8522a
|
|
@ -313,269 +313,3 @@ setSimple addr val = do
|
||||||
BoundRef _ val'
|
BoundRef _ val'
|
||||||
| val == val' -> uOK
|
| val == val' -> uOK
|
||||||
_ -> backtrack
|
_ -> backtrack
|
||||||
{- original, TODO remove -}
|
|
||||||
{-proveStep :: InterpFn
|
|
||||||
proveStep = St.get >>= go
|
|
||||||
where
|
|
||||||
finish = pure . Just
|
|
||||||
c i = St.put i >> pure Nothing
|
|
||||||
ifail msg = finish $ Left msg
|
|
||||||
tailcut [LastCall] chos _ = Just chos
|
|
||||||
tailcut [LastCall, Cut] _ cut = Just cut
|
|
||||||
tailcut _ _ _ = Nothing
|
|
||||||
withDef fn cont = do
|
|
||||||
d <- St.gets defs
|
|
||||||
case d M.!? fn of
|
|
||||||
Just d -> cont d
|
|
||||||
_ -> do
|
|
||||||
StrTable _ _ itos <- St.gets strtable
|
|
||||||
ifail $
|
|
||||||
"no definition: '" ++ (itos M.! str fn) ++ "'/" ++ show (arity fn)
|
|
||||||
{- Unification -}
|
|
||||||
go i@Interp {cur = cur@Cho {hed = U h:hs, gol = U g:gs, heap = heap}} =
|
|
||||||
unify h g
|
|
||||||
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 = derefHeap heap
|
|
||||||
withNewLocal (LocalRef reg) scope cont
|
|
||||||
| Just addr <- scope M.!? reg = cont scope heap addr
|
|
||||||
| (heap', addr) <- newHeapVar heap =
|
|
||||||
cont (M.insert reg addr scope) heap' addr
|
|
||||||
{- simple cases first -}
|
|
||||||
unify VoidRef VoidRef = uok
|
|
||||||
unify (Atom a) (Atom b)
|
|
||||||
| a == b = uok
|
|
||||||
unify VoidRef (Atom _) = uok
|
|
||||||
unify (Atom _) VoidRef = uok
|
|
||||||
unify (Number a) (Number b)
|
|
||||||
| a == b = uok
|
|
||||||
unify VoidRef (Number _) = uok
|
|
||||||
unify (Number _) 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 -- TRICKY: builtins need to check if locals actually exist because of this
|
|
||||||
unify VoidRef (LocalRef _) = uok
|
|
||||||
{- allocate heap for LocalRefs and retry with HeapRefs -}
|
|
||||||
unify lr@(LocalRef _) _ =
|
|
||||||
withNewLocal lr (hvar cur) $ \hvar' heap' addr ->
|
|
||||||
c
|
|
||||||
i
|
|
||||||
{ cur =
|
|
||||||
cur
|
|
||||||
{hed = U (HeapRef addr) : hs, hvar = hvar', heap = heap'}
|
|
||||||
}
|
|
||||||
unify _ lr@(LocalRef _) =
|
|
||||||
withNewLocal lr (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 (sometimes with copying) -}
|
|
||||||
unify (HeapRef hr) (HeapRef gr)
|
|
||||||
| BoundRef ha _ <- deref hr
|
|
||||||
, BoundRef ga _ <- deref gr
|
|
||||||
, ha == ga = uok -- BUG, structs!
|
|
||||||
| FreeRef ha <- deref hr
|
|
||||||
, BoundRef ga _ <- deref gr = setHeap ha (HeapRef ga)
|
|
||||||
| BoundRef ha _ <- deref hr
|
|
||||||
, FreeRef ga <- deref gr = setHeap ga (HeapRef ha)
|
|
||||||
| FreeRef ha <- deref hr
|
|
||||||
, FreeRef ga <- deref gr = setHeap ha (HeapRef ga)
|
|
||||||
unify (HeapRef hr') g =
|
|
||||||
case deref hr' of
|
|
||||||
FreeRef hr ->
|
|
||||||
case g of
|
|
||||||
atom@(Atom _) -> setHeap hr atom
|
|
||||||
number@(Number _) -> setHeap hr number
|
|
||||||
s@(Struct _) ->
|
|
||||||
withNewHeapStruct
|
|
||||||
hr
|
|
||||||
s
|
|
||||||
heap
|
|
||||||
(\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 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
|
|
||||||
}
|
|
||||||
}
|
|
||||||
BoundRef _ x -> unify x g
|
|
||||||
_ -> ifail "dangling head ref"
|
|
||||||
unify h (HeapRef gr') =
|
|
||||||
case deref gr' of
|
|
||||||
FreeRef gr ->
|
|
||||||
case h of
|
|
||||||
s@(Struct _) ->
|
|
||||||
withNewHeapStruct
|
|
||||||
gr
|
|
||||||
s
|
|
||||||
heap
|
|
||||||
(\ngs nheap ->
|
|
||||||
c
|
|
||||||
i
|
|
||||||
{ cur =
|
|
||||||
cur
|
|
||||||
{hed = hs, gol = map U ngs ++ gs, heap = nheap}
|
|
||||||
})
|
|
||||||
x -> setHeap gr x
|
|
||||||
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
|
|
||||||
}
|
|
||||||
}
|
|
||||||
BoundRef _ x -> unify h x
|
|
||||||
_ -> ifail "dangling goal ref"
|
|
||||||
unify _ _ = backtrack
|
|
||||||
{- Resolution -}
|
|
||||||
go i@Interp { cur = cur@Cho { hed = hed
|
|
||||||
, hvar = hvar
|
|
||||||
, gol = gol
|
|
||||||
, gvar = gvar
|
|
||||||
, heap = heap
|
|
||||||
, stk = stk
|
|
||||||
, cut = cut
|
|
||||||
}
|
|
||||||
, cho = chos
|
|
||||||
}
|
|
||||||
{- invoke a built-in (this gets replaced by NoGoal by default but the
|
|
||||||
- builtin can actually do whatever it wants with the code) -}
|
|
||||||
| [Invoke (Builtin bf)] <- hed =
|
|
||||||
St.put i {cur = cur {hed = [NoGoal]}} >> bf
|
|
||||||
{- top-level success -}
|
|
||||||
| [NoGoal] <- hed
|
|
||||||
, Just nchos <- tailcut gol chos cut
|
|
||||||
, [] <- stk = do
|
|
||||||
St.put i {cur = cur {hed = [], gol = []}, cho = nchos}
|
|
||||||
finish $ 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 i =
|
|
||||||
ifail $
|
|
||||||
"code broken: impossible instruction combo hed=" ++
|
|
||||||
show (hed . cur $ i) ++
|
|
||||||
" gol=" ++ show (gol . cur $ i) ++ " stk=" ++ show (stk . cur $ i)
|
|
||||||
-}
|
|
||||||
|
|
|
||||||
Loading…
Reference in a new issue