summaryrefslogtreecommitdiff
path: root/app/Interpreter.hs
diff options
context:
space:
mode:
authorMirek Kratochvil <exa.exa@gmail.com>2022-11-15 20:30:53 +0100
committerMirek Kratochvil <exa.exa@gmail.com>2022-11-15 20:30:53 +0100
commite074e454d5f8b5bc5dc45dccab1d138c5cd4ab0c (patch)
tree3d12a566190bdcfa1672a5a5bf69bcc79259b50c /app/Interpreter.hs
parent8d5353dc8c7ef3eefb0ae4860e67602c455c1a58 (diff)
downloadprlg-e074e454d5f8b5bc5dc45dccab1d138c5cd4ab0c.tar.gz
prlg-e074e454d5f8b5bc5dc45dccab1d138c5cd4ab0c.tar.bz2
ok simplify the refs back
Diffstat (limited to 'app/Interpreter.hs')
-rw-r--r--app/Interpreter.hs80
1 files changed, 31 insertions, 49 deletions
diff --git a/app/Interpreter.hs b/app/Interpreter.hs
index 3d1c569..ada3cf0 100644
--- a/app/Interpreter.hs
+++ b/app/Interpreter.hs
@@ -69,7 +69,6 @@ proveStep = St.get >>= go
, 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 =
@@ -77,7 +76,7 @@ proveStep = St.get >>= go
{- heap tools -}
deref x =
case hmap M.!? x of
- Just (HeapRef x' _) ->
+ Just (HeapRef x') ->
if x == x'
then FreeRef x'
else deref x'
@@ -88,71 +87,56 @@ proveStep = St.get >>= go
newHeapVars n (Heap nxt m) =
let addrs = [nxt + i - 1 | i <- [1 .. n]]
in ( Heap (nxt + n) $
- foldr (uncurry M.insert) m [(a, HeapRef a Nothing) | a <- addrs]
+ foldr (uncurry M.insert) m [(a, HeapRef a) | a <- addrs]
, addrs)
- allocLocal reg scope cont
- | Just addr <- scope M.!? reg = cont scope heap addr
+ allocLocal (LocalRef reg ident) scope cont
+ | Just (addr, _) <- scope M.!? reg = cont scope heap addr
| (heap', addr) <- newHeapVar heap =
- cont (M.insert reg addr scope) heap' addr
+ cont (M.insert reg (addr, ident) 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) Nothing) .
- M.insert (head addrs) s $
+ M.insert addr (HeapRef $ head addrs) . M.insert (head addrs) s $
m'
- in cont [HeapRef a Nothing | a <- tail addrs] (Heap nxt' m'')
+ in cont (map HeapRef $ tail addrs) (Heap nxt' m'')
{- simple cases first -}
- unify (VoidRef _) (VoidRef _) = uok
+ unify VoidRef VoidRef = uok
unify (Atom a) (Atom b)
| a == b = uok
- unify (VoidRef _) (Atom _) = uok
- unify (Atom _) (VoidRef _) = 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 Nothing) ++ hs, gol = gs}
- }
- unify (Struct Id {arity = a}) (VoidRef _) =
- c
- i
- { cur =
- cur {hed = hs, gol = replicate a (U $ VoidRef Nothing) ++ gs}
- }
+ 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
+ unify (LocalRef _ _) VoidRef = uok
+ unify VoidRef (LocalRef _ _) = uok
{- allocate heap for LocalRefs and retry with HeapRefs -}
- unify (LocalRef hv ident) _ =
- allocLocal hv (hvar cur) $ \hvar' heap' addr ->
+ unify lr@(LocalRef _ _) _ =
+ allocLocal lr (hvar cur) $ \hvar' heap' addr ->
c
i
{ cur =
cur
- { hed = U (HeapRef addr ident) : hs
- , hvar = hvar'
- , heap = heap'
- }
+ {hed = U (HeapRef addr) : hs, hvar = hvar', heap = heap'}
}
- unify _ (LocalRef gv ident) =
- allocLocal gv (gvar cur) $ \gvar' heap' addr ->
+ unify _ lr@(LocalRef _ _) =
+ allocLocal lr (gvar cur) $ \gvar' heap' addr ->
c
i
{ cur =
cur
- { gol = U (HeapRef addr ident) : gs
- , gvar = gvar'
- , heap = heap'
- }
+ {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
+ unify (HeapRef _) VoidRef = uok
+ unify VoidRef (HeapRef _) = uok
{- actual HeapRefs, these are dereferenced and then unified (sometimes with copying) -}
- unify (HeapRef hr' hident) g =
+ unify (HeapRef hr') g =
case deref hr' of
FreeRef hr ->
case g of
@@ -168,10 +152,10 @@ proveStep = St.get >>= go
cur
{hed = map U nhs ++ hs, gol = gs, heap = nheap}
})
- HeapRef gr' _ ->
+ HeapRef gr' ->
case deref gr' of
- FreeRef gr -> setHeap hr (HeapRef gr hident)
- BoundRef addr _ -> setHeap hr (HeapRef addr hident)
+ 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}) ->
@@ -181,13 +165,12 @@ proveStep = St.get >>= go
cur
{ hed =
U struct :
- [U (HeapRef (addr + i) Nothing) | i <- [1 .. arity]] ++
- hs
+ [U (HeapRef $ addr + i) | i <- [1 .. arity]] ++ hs
, gol = U g : gs
}
}
_ -> ifail "dangling head ref"
- unify h (HeapRef gr' gident) =
+ unify h (HeapRef gr') =
case deref gr' of
FreeRef gr ->
case h of
@@ -212,8 +195,7 @@ proveStep = St.get >>= go
{ hed = U h : hs
, gol =
U struct :
- [U (HeapRef (addr + i) Nothing) | i <- [1 .. arity]] ++
- gs
+ [U (HeapRef $ addr + i) | i <- [1 .. arity]] ++ gs
}
}
_ -> ifail "dangling goal ref"