diff options
| author | Mirek Kratochvil <exa.exa@gmail.com> | 2022-11-12 23:25:50 +0100 |
|---|---|---|
| committer | Mirek Kratochvil <exa.exa@gmail.com> | 2022-11-12 23:25:50 +0100 |
| commit | 9d7868431792dcd94ec71adb9f95f55ab4bf027d (patch) | |
| tree | d5a9a371920edab2d7ddd00a6f87c8809dfb3221 /app/Interpreter.hs | |
| parent | e248226f442f289f3b7399411cdfd127a0de4d1a (diff) | |
| download | prlg-9d7868431792dcd94ec71adb9f95f55ab4bf027d.tar.gz prlg-9d7868431792dcd94ec71adb9f95f55ab4bf027d.tar.bz2 | |
reorg 1
Diffstat (limited to 'app/Interpreter.hs')
| -rw-r--r-- | app/Interpreter.hs | 49 |
1 files changed, 26 insertions, 23 deletions
diff --git a/app/Interpreter.hs b/app/Interpreter.hs index ebec859..743f68b 100644 --- a/app/Interpreter.hs +++ b/app/Interpreter.hs @@ -1,39 +1,42 @@ {- VAM 2P, done the lazy way -} module Interpreter where +import Code --import Data.Function import qualified Data.Map as M - -import Code +import Env (PrlgEnv(..)) import IR (Id(..)) +import qualified Control.Monad.Trans.State.Lazy as St -prove :: Code -> Defs -> (Interp, Either String Bool) -prove g ds = - let i0 = - Interp - { defs = ds - , cur = - Cho - { hed = g - , hvar = emptyScope - , gol = [LastCall] - , gvar = emptyScope - , heap = emptyHeap - , stk = [] - , cut = [] - } - , cho = [] - } - run (Left x) = x - run (Right x) = run $ proveStep Right (\i e -> Left (i, e)) x - in run (Right i0) +prove :: Code -> PrlgEnv (Either String Bool) +prove g = do + St.modify $ \i -> + i + { cur = + Cho + { hed = g + , hvar = emptyScope + , gol = [LastCall] + , gvar = emptyScope + , heap = emptyHeap + , stk = [] + , cut = [] + } + , cho = [] + } + loop + where + loop = do + i <- St.get + proveStep cont finish i + cont i = St.put i >> loop + finish i res = St.put i >> return res data Dereferenced = FreeRef Int | BoundRef Int Datum | NoRef -{- this gonna need Either String Bool for errors later -} proveStep :: (Interp -> a) -> (Interp -> Either String Bool -> a) -> Interp -> a proveStep c f i = go i where |
