diff options
| -rw-r--r-- | app/Code.hs | 3 | ||||
| -rw-r--r-- | app/Interpreter.hs | 21 | ||||
| -rw-r--r-- | inst/prelude.pl | 17 |
3 files changed, 23 insertions, 18 deletions
diff --git a/app/Code.hs b/app/Code.hs index 684686f..b60ab66 100644 --- a/app/Code.hs +++ b/app/Code.hs @@ -51,7 +51,8 @@ data Cho = , _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) , _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) diff --git a/app/Interpreter.hs b/app/Interpreter.hs index 5d1e2ab..2ad0118 100644 --- a/app/Interpreter.hs +++ b/app/Interpreter.hs @@ -35,6 +35,7 @@ prove g = do , _heap = emptyHeap , _stk = [] , _cut = [] + , _hcut = [] } cho .= [] loop @@ -54,10 +55,14 @@ proveStep = do import Control.Monad.Trans.Class (lift) import System.Console.Haskeline g <- use (cur . gol) + cho <- use cho + cut <- use (cur . cut) lift $ do outputStrLn $ "STEP (unis="++show u++")" outputStrLn $ "head = "++ show h outputStrLn $ "goal = "++ show g + outputStrLn $ "cut = " ++ show cut + outputStrLn $ "cho = " ++ show cho -} case (u, h) of (0, []) -> goalStep @@ -92,7 +97,7 @@ headStep h = do case (h, g) of ([Done], _) -> succeedHead (Cut:_, _) -> cutHead - (Invoke (Builtin bf):_, _) -> advanceHead >> bf + (Invoke (Builtin bf):_, _) -> cur . hed .= [Done] >> bf (_, [Done]) -> tailCall (_, [Cut, Done]) -> tailCut (_, _) -> pushCall @@ -134,7 +139,9 @@ retCut = do doCut cur . retcut .= False -cutHead = doCut >> advanceHead +cutHead = do + use (cur . hcut) >>= assign cho + advanceHead cutGoal = doCut >> advance @@ -147,7 +154,8 @@ openGoal fn = do cur . hvar .= emptyScope cur . unis .= arity fn 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 cho %= (newcho ++) continue @@ -162,12 +170,15 @@ pushCall = do ngol <- use (cur . hed) ngvar <- use (cur . hvar) scut <- use (cur . cut) + ncut <- use (cur . hcut) sretcut <- use (cur . retcut) cur . stk %= ((sgol, sgvar, scut, sretcut) :) cur . gol .= ngol cur . gvar .= ngvar + cur . cut .= ncut cur . hed .= [] cur . hvar .= emptyScope + cur . hcut .= [] cur . retcut .= False continue @@ -179,6 +190,7 @@ tailCall = do cur . gvar .= ngvar cur . hed .= [] cur . hvar .= emptyScope + cur . hcut .= [] continue tailCut :: InterpFn @@ -189,8 +201,9 @@ tailCut = do succeedHead :: InterpFn succeedHead = do - cur . hvar .= emptyScope cur . hed .= [] + cur . hvar .= emptyScope + cur . hcut .= [] continue succeedGoal :: InterpFn diff --git a/inst/prelude.pl b/inst/prelude.pl index cc0c940..34e7853 100644 --- a/inst/prelude.pl +++ b/inst/prelude.pl @@ -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). zero(Ax) :- A is Ax, int1p_zero(A). -gcd(X,Y,R) :- writeln(a), fail. -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). -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). +gcd(X,Y,R) :- Y > X, !, gcd(Y,X,R). +gcd(X,Y,R) :- zero(Y), !, R=X. +gcd(X,Y,R) :- X1 is X mod Y, gcd(Y,X1,R). -test(X) :- writeln(there), zero(X), fail. -test(X) :- writeln(here). - -test :- writeln(a), a=a, !, fail. -test :- writeln(b). - -xxx :- test. +lcm(X,Y,R) :- gcd(X,Y,GCD), R is X*(Y/GCD). |