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

cuts

Browse source
This commit is contained in:
Mirek Kratochvil 2022-10-15 20:47:20 +02:00
parent 31c20628ea
commit cbd6aa4021
3 changed files with 78 additions and 43 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

74
app/Interpreter.hs
View file

@ -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"

45
app/Main.hs
View file

@ -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

2
prlg.cabal
View file

@ -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