diff options
| -rw-r--r-- | app/Interpreter.hs | 74 | ||||
| -rw-r--r-- | app/Main.hs | 45 | ||||
| -rw-r--r-- | 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 } - {- goal head matching succeeded, make a normal call -} - | (Goal:U (Struct fn):ngs) <- hed - , (Call:gs) <- gol = + {- 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 = ngs, stk = gs : stk} - , cho = [Cho oh ngs stk chos | oh <- ohs] ++ chos + { cur = cur {hed = hs, gol = gs} + , cho = [Cho oh gs stk cut | oh <- ohs] ++ cut } - {- R: Successful match continued by tail call -} + {- goal head matching succeeded, make a normal call -} + | (Goal:U (Struct fn):ngs) <- hed + , (Call:gs) <- gol = + withDef fn $ \(hs:ohs) -> + 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 @@ -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 |