exa/prlg
1
0
Fork 0
Code Issues Pull requests Actions Packages Projects Releases Wiki Activity

have a normal Stk

Browse source
This commit is contained in:
Mirek Kratochvil 2022-10-15 15:02:13 +02:00
parent eb67b6b665
commit 6fa4cec10b
1 changed files with 38 additions and 32 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

70
app/Interpreter.hs
View file

@ -26,6 +26,10 @@ type Code = [Instr]
type Alts = [(Code, Code)] -- clauses to try and the corresponding goals to restore type Alts = [(Code, Code)] -- clauses to try and the corresponding goals to restore
data Stk =
Stk Alts [(Code, Alts)]
deriving (Show) -- local backtracks (skipped on cut) + return&backtracks
type Defs = M.Map (Int, Int) [Code] type Defs = M.Map (Int, Int) [Code]
data Interp = data Interp =
@ -33,13 +37,13 @@ data Interp =
{ defs :: Defs -- global definitions for lookup { defs :: Defs -- global definitions for lookup
, hed :: Code -- current head , hed :: Code -- current head
, gol :: Code -- current goal , gol :: Code -- current goal
, stk :: [Alts] -- possible heads with stored original goal , stk :: Stk -- possible heads with stored original goal
} }
deriving (Show) deriving (Show)
prove :: Code -> Defs -> Either (Interp, String) Bool prove :: Code -> Defs -> Either (Interp, String) Bool
prove g ds = prove g ds =
let i0 = Interp ds g [LastCall] [[]] let i0 = Interp ds g [LastCall] (Stk [] [])
run (Left x) = x run (Left x) = x
run (Right x) = run $ proveStep Right Left x run (Right x) = run $ proveStep Right Left x
in run (Right i0) in run (Right i0)
@ -52,15 +56,14 @@ proveStep c f i = go i
withDef f withDef f
| Just d <- defs i M.!? f = ($ d) | Just d <- defs i M.!? f = ($ d)
| otherwise = const $ ifail $ "no definition: " ++ show f | otherwise = const $ ifail $ "no definition: " ++ show f
{- Backtracking -} {- Backtracking: try a fallback clause, restoring goal -}
backtrack i@Interp {stk = ((s, gs):ss):sss} -- backtrack to next clause, restoring goal backtrack i@Interp {stk = Stk ((s, gs):ss) sss} =
= c i {hed = s, gol = gs, stk = ss : sss} c i {hed = s, gol = gs, stk = Stk ss sss}
backtrack i@Interp {stk = []:ss@(_:_):sss} -- no next clause, pop stack and backtrack the caller clause {- B: no next clause, pop stack and continue backtracking at the caller -}
= backtrack i@Interp {stk = Stk [] ((g, ss):sss)} =
backtrack backtrack i {hed = error "failed hed", gol = g, stk = Stk ss sss}
i {hed = error "failed hed", gol = error "failed gol", stk = ss : sss} {- B: we ran out of possibilities and there's nothing else to backtrack. No solution found. -}
backtrack i@Interp {stk = [[]]} = f (Right False) backtrack i@Interp {stk = Stk [] []} = f (Right False)
backtrack i@Interp {stk = []:[]:_} = ifail "broken stk" -- this should not happen
{- Unification -} {- Unification -}
go i@Interp {hed = (U a:hs), gol = (U b:gs)} -- unify constants go i@Interp {hed = (U a:hs), gol = (U b:gs)} -- unify constants
= unify a b = unify a b
@ -71,33 +74,36 @@ proveStep c f i = go i
unify (Struct a) (Struct b) unify (Struct a) (Struct b)
| a == b = uok | a == b = uok
unify _ _ = backtrack i unify _ _ = backtrack i
{- Resolution -} {- Resolution: Final success -}
go i@Interp {hed = [NoGoal], gol = [LastCall], stk = [_]} = f (Right True) -- final success go i@Interp {hed = [NoGoal], gol = [LastCall], stk = Stk _ []} =
f (Right True)
{- R: Goal succeeded; continue at parent frame -}
go i@Interp { hed = [NoGoal] go i@Interp { hed = [NoGoal]
, gol = [LastCall] , gol = [LastCall]
, stk = _:((Goal:U (Struct f):gs, _):ss):sss , stk = Stk _ ((Goal:U (Struct f):gs, ss):sss)
} -- goal succeeded, continue with parent frame } =
=
withDef f $ \(hs:ohs) -> withDef f $ \(hs:ohs) ->
c i {hed = hs, gol = gs, stk = (map (, gs) ohs ++ ss) : sss} c i {hed = hs, gol = gs, stk = Stk (map (, gs) ohs ++ ss) sss}
{- R: Start matching next goal -}
go i@Interp { hed = [NoGoal] go i@Interp { hed = [NoGoal]
, gol = (Call:Goal:U (Struct f):gs) , gol = (Call:Goal:U (Struct f):gs)
, stk = ss:sss , stk = Stk ss sss
} -- next goal } =
=
withDef f $ \(hs:ohs) -> withDef f $ \(hs:ohs) ->
c i {hed = hs, gol = gs, stk = (map (, gs) ohs ++ ss) : sss} c i {hed = hs, gol = gs, stk = Stk (map (, gs) ohs ++ ss) sss}
go i@Interp {hed = (Goal:U (Struct f):ngs), gol = (Call:gs), stk = ss:sss} -- normal call {- R: Goal head matching succeeded, make a normal call -}
= go i@Interp { hed = (Goal:U (Struct f):ngs)
, gol = (Call:gs)
, stk = Stk ss sss
} =
withDef f $ \(hs:ohs) -> withDef f $ \(hs:ohs) ->
c c i {hed = hs, gol = ngs, stk = Stk (map (, ngs) ohs) ((gs, ss) : sss)}
i {- R: Successful match continued by tail call -}
{ hed = hs go i@Interp { hed = (Goal:U (Struct f):ngs)
, gol = ngs , gol = [LastCall]
, stk = (map (, ngs) ohs) : ((gs, error "gol no hed") : ss) : sss , stk = Stk _ sss
} } =
go i@Interp {hed = (Goal:U (Struct f):ngs), gol = [LastCall], stk = _:sss} -- tail call
=
withDef f $ \(hs:ohs) -> withDef f $ \(hs:ohs) ->
c i {hed = hs, gol = ngs, stk = map (, ngs) ohs : sss} c i {hed = hs, gol = ngs, stk = Stk (map (, ngs) ohs) sss}
{- The End -}
go _ = ifail "impossible instruction combo" go _ = ifail "impossible instruction combo"