diff options
| author | Mirek Kratochvil <exa.exa@gmail.com> | 2022-11-15 20:30:53 +0100 |
|---|---|---|
| committer | Mirek Kratochvil <exa.exa@gmail.com> | 2022-11-15 20:30:53 +0100 |
| commit | e074e454d5f8b5bc5dc45dccab1d138c5cd4ab0c (patch) | |
| tree | 3d12a566190bdcfa1672a5a5bf69bcc79259b50c /app/Interpreter.hs | |
| parent | 8d5353dc8c7ef3eefb0ae4860e67602c455c1a58 (diff) | |
| download | prlg-e074e454d5f8b5bc5dc45dccab1d138c5cd4ab0c.tar.gz prlg-e074e454d5f8b5bc5dc45dccab1d138c5cd4ab0c.tar.bz2 | |
ok simplify the refs back
Diffstat (limited to 'app/Interpreter.hs')
| -rw-r--r-- | app/Interpreter.hs | 80 |
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" |
