{- 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"