small things

This commit is contained in:
Mirek Kratochvil 2023-03-04 22:46:07 +01:00
parent 336feaeba0
commit 45c3f81891
3 changed files with 23 additions and 18 deletions

View file

@ -51,7 +51,8 @@ data Cho =
, _retcut :: Bool -- cut after this goal succeeds , _retcut :: Bool -- cut after this goal succeeds
, _heap :: Heap -- a snapshot of the heap (there's no trail; we rely on CoW copies in other choicepoints) , _heap :: Heap -- a snapshot of the heap (there's no trail; we rely on CoW copies in other choicepoints)
, _stk :: [(Code, Scope, [Cho], Bool)] -- remaining goals together with their vars, cuts, and ret-cut flag , _stk :: [(Code, Scope, [Cho], Bool)] -- remaining goals together with their vars, cuts, and ret-cut flag
, _cut :: [Cho] -- snapshot of choicepoints before entering , _cut :: [Cho] -- snapshot of choicepoints before entering the goal
, _hcut :: [Cho] -- save of choicepoints just before starting to match head
} }
deriving (Show) deriving (Show)

View file

@ -35,6 +35,7 @@ prove g = do
, _heap = emptyHeap , _heap = emptyHeap
, _stk = [] , _stk = []
, _cut = [] , _cut = []
, _hcut = []
} }
cho .= [] cho .= []
loop loop
@ -54,10 +55,14 @@ proveStep = do
import Control.Monad.Trans.Class (lift) import Control.Monad.Trans.Class (lift)
import System.Console.Haskeline import System.Console.Haskeline
g <- use (cur . gol) g <- use (cur . gol)
cho <- use cho
cut <- use (cur . cut)
lift $ do lift $ do
outputStrLn $ "STEP (unis="++show u++")" outputStrLn $ "STEP (unis="++show u++")"
outputStrLn $ "head = "++ show h outputStrLn $ "head = "++ show h
outputStrLn $ "goal = "++ show g outputStrLn $ "goal = "++ show g
outputStrLn $ "cut = " ++ show cut
outputStrLn $ "cho = " ++ show cho
-} -}
case (u, h) of case (u, h) of
(0, []) -> goalStep (0, []) -> goalStep
@ -92,7 +97,7 @@ headStep h = do
case (h, g) of case (h, g) of
([Done], _) -> succeedHead ([Done], _) -> succeedHead
(Cut:_, _) -> cutHead (Cut:_, _) -> cutHead
(Invoke (Builtin bf):_, _) -> advanceHead >> bf (Invoke (Builtin bf):_, _) -> cur . hed .= [Done] >> bf
(_, [Done]) -> tailCall (_, [Done]) -> tailCall
(_, [Cut, Done]) -> tailCut (_, [Cut, Done]) -> tailCut
(_, _) -> pushCall (_, _) -> pushCall
@ -134,7 +139,9 @@ retCut = do
doCut doCut
cur . retcut .= False cur . retcut .= False
cutHead = doCut >> advanceHead cutHead = do
use (cur . hcut) >>= assign cho
advanceHead
cutGoal = doCut >> advance cutGoal = doCut >> advance
@ -147,7 +154,8 @@ openGoal fn = do
cur . hvar .= emptyScope cur . hvar .= emptyScope
cur . unis .= arity fn cur . unis .= arity fn
cc <- use cur cc <- use cur
let (newcur:newcho) = [cc & hed .~ h | h <- hs] oldcho <- use cho
let (newcur:newcho) = [cc & hcut .~ oldcho & hed .~ h | h <- hs]
cur .= newcur cur .= newcur
cho %= (newcho ++) cho %= (newcho ++)
continue continue
@ -162,12 +170,15 @@ pushCall = do
ngol <- use (cur . hed) ngol <- use (cur . hed)
ngvar <- use (cur . hvar) ngvar <- use (cur . hvar)
scut <- use (cur . cut) scut <- use (cur . cut)
ncut <- use (cur . hcut)
sretcut <- use (cur . retcut) sretcut <- use (cur . retcut)
cur . stk %= ((sgol, sgvar, scut, sretcut) :) cur . stk %= ((sgol, sgvar, scut, sretcut) :)
cur . gol .= ngol cur . gol .= ngol
cur . gvar .= ngvar cur . gvar .= ngvar
cur . cut .= ncut
cur . hed .= [] cur . hed .= []
cur . hvar .= emptyScope cur . hvar .= emptyScope
cur . hcut .= []
cur . retcut .= False cur . retcut .= False
continue continue
@ -179,6 +190,7 @@ tailCall = do
cur . gvar .= ngvar cur . gvar .= ngvar
cur . hed .= [] cur . hed .= []
cur . hvar .= emptyScope cur . hvar .= emptyScope
cur . hcut .= []
continue continue
tailCut :: InterpFn tailCut :: InterpFn
@ -189,8 +201,9 @@ tailCut = do
succeedHead :: InterpFn succeedHead :: InterpFn
succeedHead = do succeedHead = do
cur . hvar .= emptyScope
cur . hed .= [] cur . hed .= []
cur . hvar .= emptyScope
cur . hcut .= []
continue continue
succeedGoal :: InterpFn succeedGoal :: InterpFn

View file

@ -45,17 +45,8 @@ Ax > Bx :- A is Ax, B is Bx, int2p_lt(B,A).
Ax >= Bx :- A is Ax, B is Bx, int2p_leq(B,A). Ax >= Bx :- A is Ax, B is Bx, int2p_leq(B,A).
zero(Ax) :- A is Ax, int1p_zero(A). zero(Ax) :- A is Ax, int1p_zero(A).
gcd(X,Y,R) :- writeln(a), fail. gcd(X,Y,R) :- Y > X, !, gcd(Y,X,R).
gcd(X,Y,R) :- writeln(b), zero(Y), !, R=X. gcd(X,Y,R) :- zero(Y), !, R=X.
gcd(X,Y,R) :- writeln(c), X1 is X mod Y, gcd(Y,X1,R). gcd(X,Y,R) :- X1 is X mod Y, gcd(Y,X1,R).
gcd(X,Y,R) :- writeln(a), Y > X, writeln(wat), !, gcd(Y,X,R).
gcd(X,Y,R) :- writeln(b), zero(Y), !, R=X.
gcd(X,Y,R) :- writeln(c), X1 is X mod Y, gcd(Y,X1,R).
test(X) :- writeln(there), zero(X), fail. lcm(X,Y,R) :- gcd(X,Y,GCD), R is X*(Y/GCD).
test(X) :- writeln(here).
test :- writeln(a), a=a, !, fail.
test :- writeln(b).
xxx :- test.