diff options
Diffstat (limited to 'app')
| -rw-r--r-- | app/Interpreter.hs | 266 |
1 files changed, 0 insertions, 266 deletions
diff --git a/app/Interpreter.hs b/app/Interpreter.hs index ecf1ebe..31c4c12 100644 --- a/app/Interpreter.hs +++ b/app/Interpreter.hs @@ -313,269 +313,3 @@ setSimple addr val = do BoundRef _ val' | val == val' -> uOK _ -> 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) --} |