From cbd6aa4021f744be7301e9d5b6fce2c6c98c46ae Mon Sep 17 00:00:00 2001
From: Mirek Kratochvil <exa.exa@gmail.com>
Date: Sat, 15 Oct 2022 20:47:20 +0200
Subject: [PATCH] cuts
---
app/Interpreter.hs | 74 ++++++++++++++++++++++++++++++++--------------
app/Main.hs | 45 +++++++++++++++-------------
prlg.cabal | 2 +-
3 files changed, 78 insertions(+), 43 deletions(-)
diff --git a/app/Interpreter.hs b/app/Interpreter.hs
index cd1ab34..81ecb3d 100644
--- a/app/Interpreter.hs
+++ b/app/Interpreter.hs
@@ -32,8 +32,8 @@ data Cho =
Cho
{ hed :: Code -- head pointer
, gol :: Code -- goal pointer
- , stk :: [Code] -- remaining "and" goals
- , cut :: [Cho] -- snapshot of choicepoints
+ , stk :: [(Code, [Cho])] -- remaining "and" goals
+ , cut :: [Cho] -- snapshot of choicepoints before entering
}
deriving (Show)
@@ -45,20 +45,26 @@ data Interp =
}
deriving (Show)
-prove :: Code -> Defs -> Either (Interp, String) Bool
+prove :: Code -> Defs -> (Interp, Either String Bool)
prove g ds =
let i0 =
Interp
- {defs = ds, cur = Cho {hed = g, gol = [LastCall], stk = [], cut = []}, cho = []}
+ { defs = ds
+ , cur = Cho {hed = g, gol = [LastCall], stk = [], cut = []}
+ , cho = []
+ }
run (Left x) = x
- run (Right x) = run $ proveStep Right Left x
+ run (Right x) = run $ proveStep Right (\i e -> Left (i, e)) x
in run (Right i0)
{- this gonna need Either String Bool for errors later -}
-proveStep :: (Interp -> a) -> (Either (Interp, String) Bool -> a) -> Interp -> a
+proveStep :: (Interp -> a) -> (Interp -> Either String Bool -> a) -> Interp -> a
proveStep c f i = go i
where
- ifail msg = f $ Left (i, msg)
+ 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
@@ -67,7 +73,7 @@ proveStep c f i = go i
{- 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 (Right False)
+ | otherwise = f i $ Right False
{- Unification -}
go i@Interp {cur = cur@Cho {hed = U a:hs, gol = U b:gs}} -- unify constants
= unify a b
@@ -79,20 +85,35 @@ proveStep c f i = go i
| a == b = uok
unify _ _ = backtrack i
{- Resulution -}
- go i@Interp {cur = cur@Cho {hed = hed, gol = gol, stk = stk}, cho = chos}
+ go i@Interp { cur = cur@Cho {hed = hed, gol = gol, stk = stk, cut = cut}
+ , cho = chos
+ }
{- top-level success -}
| [NoGoal] <- hed
- , [LastCall] <- gol
- , [] <- stk = f (Right True)
+ , 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
- , [LastCall] <- gol
- , (Goal:U (Struct fn):gs):ss <- stk =
+ , Just nchos <- tailcut gol chos cut
+ , (Goal:U (Struct fn):gs, _):ss <- stk =
withDef fn $ \(hs:ohs) ->
c
i
{ cur = cur {hed = hs, gol = gs, stk = ss}
- , cho = [Cho oh gs ss chos | oh <- ohs] ++ chos
+ , cho = [Cho oh gs 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, rchos):ss <- stk =
+ withDef fn $ \(hs:ohs) ->
+ c
+ i
+ { cur = cur {hed = hs, gol = gs, stk = ss}
+ , cho = [Cho oh gs ss rchos | oh <- ohs] ++ rchos
}
{- start matching next goal -}
| [NoGoal] <- hed
@@ -103,23 +124,32 @@ proveStep c f i = go i
{ cur = cur {hed = hs, gol = gs}
, cho = [Cho oh gs 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, gol = gs}
+ , cho = [Cho oh gs 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) ->
- c
- i
- { cur = cur {hed = hs, gol = ngs, stk = gs : stk}
- , cho = [Cho oh ngs stk chos | oh <- ohs] ++ chos
- }
- {- R: Successful match continued by tail call -}
+ let nstk = (gs, chos) : stk
+ in c i
+ { cur = cur {hed = hs, gol = ngs, stk = nstk}
+ , cho = [Cho oh ngs nstk chos | oh <- ohs] ++ chos
+ }
+ {- successful match continued by tail call -}
| (Goal:U (Struct fn):ngs) <- hed
- , [LastCall] <- gol =
+ , Just nchos <- tailcut gol chos cut =
withDef fn $ \(hs:ohs) ->
c
i
{ cur = cur {hed = hs, gol = ngs}
- , cho = [Cho oh ngs stk chos | oh <- ohs] ++ chos
+ , cho = [Cho oh ngs stk nchos | oh <- ohs] ++ nchos
}
{- The End -}
go _ = ifail "impossible instruction combo"
diff --git a/app/Main.hs b/app/Main.hs
index be4febe..c2f03ee 100644
--- a/app/Main.hs
+++ b/app/Main.hs
@@ -1,27 +1,32 @@
module Main where
import Interpreter
-
+import Text.Pretty.Simple
import qualified Data.Map as M
+ppr :: Show a => a -> IO ()
+ppr = pPrintOpt CheckColorTty defaultOutputOptionsDarkBg {outputOptionsCompactParens = True, outputOptionsIndentAmount = 2, outputOptionsPageWidth=80}
+
main :: IO ()
-main =
- print $
- prove [Goal, U (Struct (1, 2)), U (Atom 1), U (Atom 2), LastCall] $
- M.fromList
- [ ( (1, 2)
- , [ [U (Atom 333), U (Atom 444), NoGoal]
- , [ U (Atom 1)
- , U (Atom 2)
- , Goal
- , U (Struct (2, 0))
- , Call
- , Goal
- , U (Struct (1, 2))
- , U (Atom 333)
- , U (Atom 444)
- , LastCall
+main = do
+ let (res, interp) =
+ prove [Goal, U (Struct (1, 2)), U (Atom 1), U (Atom 2), LastCall] $
+ M.fromList
+ [ ( (1, 2)
+ , [ [U (Atom 333), U (Atom 444), NoGoal]
+ , [ U (Atom 1)
+ , U (Atom 2)
+ , Goal
+ , U (Struct (2, 0))
+ , Call
+ , Goal
+ , U (Struct (5, 2))
+ , U (Atom 333)
+ , U (Atom 444)
+ , LastCall
+ ]
+ ])
+ , ((2, 0), [[NoGoal]])
]
- ])
- , ((2, 0), [[NoGoal]])
- ]
+ ppr interp
+ ppr res
diff --git a/prlg.cabal b/prlg.cabal
index 21da1dc..929744d 100644
--- a/prlg.cabal
+++ b/prlg.cabal
@@ -29,6 +29,6 @@ executable prlg
-- LANGUAGE extensions used by modules in this package.
-- other-extensions:
- build-depends: base >=4.16, containers, megaparsec, haskeline
+ build-depends: base >=4.16, containers, megaparsec, haskeline, pretty-simple
hs-source-dirs: app
default-language: Haskell2010