summaryrefslogtreecommitdiff
diff options
context:
space:
mode:
authorMirek Kratochvil <exa.exa@gmail.com>2023-02-26 12:16:06 +0100
committerMirek Kratochvil <exa.exa@gmail.com>2023-02-26 12:16:06 +0100
commit27494c044e54f1bfe8fac466f9416b6e17d58b4d (patch)
treed5a8ce0346bf119303dbf67ef6bbac5ddf24beb8
parent81df52f6565c073f9638108a66304d0ecc6cac02 (diff)
downloadprlg-27494c044e54f1bfe8fac466f9416b6e17d58b4d.tar.gz
prlg-27494c044e54f1bfe8fac466f9416b6e17d58b4d.tar.bz2
PAS continues
-rw-r--r--app/Interpreter.hs140
1 files changed, 117 insertions, 23 deletions
diff --git a/app/Interpreter.hs b/app/Interpreter.hs
index 43ea1d5..4f21709 100644
--- a/app/Interpreter.hs
+++ b/app/Interpreter.hs
@@ -17,9 +17,11 @@ import Code
, writeHeap
)
import CodeLens
+import Control.Monad (when)
import qualified Data.Map as M
import Env (PrlgEnv)
import IR (Id(..), StrTable(..))
+import Lens.Family2
import Lens.Family2.State
prove :: Code -> PrlgEnv (Either String Bool)
@@ -55,7 +57,13 @@ proveStep = do
(0, _) -> headStep h
(_, _)
| u > 0 -> unifyStep h
- _ -> err "invalid state"
+ _ -> err "invalid interpreter state"
+
+continue :: InterpFn
+continue = pure Nothing
+
+finish :: Bool -> InterpFn
+finish = pure . Just . Right
err :: String -> InterpFn
err = return . Just . Left
@@ -65,29 +73,26 @@ goalStep :: InterpFn
goalStep = do
g <- use (cur . gol)
case g of
- U (Struct _):gs -> undefined -- TODO these things NEED lens-family.
- [Done] -> undefined
- [Cut, Done] -> undefined
- Cut:gs -> undefined
- [Choices cs, Done] -> undefined
- [Choices cs, Cut, Done] -> undefined
- Choices cs:gs -> undefined
+ U (Struct s):gs -> openGoal s
+ [Done] -> succeedGoal
+ Cut:gs -> cutGoal
+ Choices cs:gs -> pushChoices cs
_ -> err "invalid goal code"
headStep :: [Instr] -> InterpFn
headStep h = do
g <- use (cur . gol)
case (h, g) of
- ([Done], _) -> undefined
- ([Cut, Done], _) -> undefined
- (_, [Done]) -> undefined
- (_, [Cut, Done]) -> undefined
- (_, _) -> undefined
+ ([Done], _) -> succeedHead
+ (Cut:_, _) -> cutHead
+ (_, [Done]) -> tailCall
+ (_, [Cut, Done]) -> tailCut
+ (_, _) -> pushCall
unifyStep h = do
g <- use (cur . gol)
case (h, g) of
- (U hd:_, U gd:_) -> undefined hd gd
+ (U hd:_, U gd:_) -> unify hd gd
(_, _) -> err "invalid unification code"
{- helpers -}
@@ -100,18 +105,107 @@ backtrack = do
-> do
cur .= c
cho .= cs
- pure Nothing
- {- if there's no other choice, answer no -}
- _ -> pure . Just $ Right False
+ continue
+ {- if there's no other choice available, answer no -}
+ _ -> finish False
+
+advance = do
+ cur . gol %= tail
+ continue
+
+advanceHead = do
+ cur . hed %= tail
+ continue
+
+doCut = use (cur . cut) >>= assign cho
+
+retCut = do
+ rc <- use (cur . retcut)
+ when rc $ do
+ doCut
+ cur . retcut .= False
+
+cutHead = doCut >> advanceHead
+
+cutGoal = doCut >> advance
+
+openGoal :: IR.Id -> InterpFn
+openGoal fn = do
+ def <- defs `uses` (M.!? fn)
+ case def of
+ Just hs@(_:_) -> do
+ advance
+ cur . hvar .= emptyScope
+ cur . unis .= arity fn
+ cc <- use cur
+ let (newcur:newcho) = [cc & hed .~ h | h <- hs]
+ cur .= newcur
+ cho %= (newcho ++)
+ continue
+ _ -> do
+ StrTable _ _ itos <- use strtable
+ err $ "no definition: '" ++ (itos M.! str fn) ++ "'/" ++ show (arity fn)
+
+pushCall :: InterpFn
+pushCall = do
+ sgol <- use (cur . gol)
+ sgvar <- use (cur . gvar)
+ ngol <- use (cur . hed)
+ ngvar <- use (cur . hvar)
+ scut <- use (cur . cut)
+ sretcut <- use (cur . retcut)
+ cur . stk %= ((sgol, sgvar, scut, sretcut) :)
+ cur . gol .= ngol
+ cur . gvar .= ngvar
+ cur . hed .= []
+ cur . hvar .= emptyScope
+ cur . retcut .= False
+ continue
+
+tailCall :: InterpFn
+tailCall = do
+ ngol <- use (cur . hed)
+ ngvar <- use (cur . hvar)
+ cur . gol .= ngol
+ cur . gvar .= ngvar
+ cur . hed .= []
+ cur . hvar .= emptyScope
+ continue
+
+tailCut :: InterpFn
+tailCut = do
+ cur . retcut .= True
+ advance
+ tailCall
+
+succeedHead :: InterpFn
+succeedHead = do
+ cur . hvar .= emptyScope
+ cur . hed .= []
+ continue
-retCut :: InterpFn
-retCut = undefined
+succeedGoal :: InterpFn
+succeedGoal = do
+ retCut
+ st <- use (cur . stk)
+ case st of
+ [] -> do
+ cur . gol .= []
+ finish True
+ ((sgol, sgvar, scut, sretcut):st') -> do
+ zoom cur $ do
+ gol .= sgol
+ gvar .= sgvar
+ cut .= scut
+ retcut .= sretcut
+ stk .= st'
+ continue
-cutHead :: InterpFn
-cutHead = undefined
+pushChoices :: [[Code]] -> InterpFn
+pushChoices cs = undefined
-cutGoal :: InterpFn
-cutGoal = undefined
+unify :: Datum -> Datum -> InterpFn
+unify = undefined
{- original, TODO remove -}
{-proveStep :: InterpFn
proveStep = St.get >>= go