assert v0

This commit is contained in:
Mirek Kratochvil 2022-11-25 22:18:11 +01:00
parent 6f123999e0
commit 58367975ae
4 changed files with 133 additions and 63 deletions

View file

@ -4,6 +4,7 @@ import Code
import Control.Monad.IO.Class import Control.Monad.IO.Class
import Control.Monad.Trans.Class import Control.Monad.Trans.Class
import Control.Monad.Trans.State.Lazy import Control.Monad.Trans.State.Lazy
import Data.Functor.Identity
import Data.List (intercalate) import Data.List (intercalate)
import qualified Data.Map as M import qualified Data.Map as M
import Env hiding (PrlgEnv) import Env hiding (PrlgEnv)
@ -14,28 +15,27 @@ import System.Console.Haskeline
bi = Builtin bi = Builtin
showTerm itos heap visited ref showTerm itos heap = runIdentity . heapStruct atom struct hrec heap
| ref `elem` visited = "_Rec" ++ show ref where
| HeapRef r <- heap M.! ref = atom (Atom a) = pure $ itos M.! a
if r == ref atom VoidRef = pure "_"
then "_X" ++ show ref struct (Struct (IR.Id h _)) args =
else showTerm itos heap (ref : visited) r pure $ itos M.! h ++ "(" ++ intercalate "," args ++ ")"
| Struct (IR.Id h arity) <- heap M.! ref = hrec (HeapRef hr) ref =
itos M.! h ++ pure $
"(" ++ (if hr == ref
intercalate then "_X"
"," else "_Rec") ++
[showTerm itos heap (ref : visited) (ref + i) | i <- [1 .. arity]] ++ show hr
")"
| Atom a <- heap M.! ref = itos M.! a
printLocals :: BuiltinFn printLocals :: BuiltinFn
printLocals = do printLocals = do
scope <- gets (gvar . cur) scope <- gets (gvar . cur)
Heap _ heap <- gets (heap . cur) heap <- gets (heap . cur)
IR.StrTable _ _ itos <- gets strtable IR.StrTable _ _ itos <- gets strtable
flip traverse (M.elems scope) $ \(ref, name) -> flip traverse (M.elems scope) $ \(ref, name) ->
lift . outputStrLn $ (itos M.! name) ++ " = " ++ showTerm itos heap [] ref lift . outputStrLn $
(maybe "_" id $ itos M.!? name) ++ " = " ++ showTerm itos heap ref
return Nothing return Nothing
promptRetry :: BuiltinFn promptRetry :: BuiltinFn
@ -48,9 +48,9 @@ promptRetry = do
write :: BuiltinFn write :: BuiltinFn
write = do write = do
scope <- gets (hvar . cur) scope <- gets (hvar . cur)
Heap _ heap <- gets (heap . cur) heap <- gets (heap . cur)
IR.StrTable _ _ itos <- gets strtable IR.StrTable _ _ itos <- gets strtable
lift . outputStr $ showTerm itos heap [] (fst $ scope M.! 0) lift . outputStr . showTerm itos heap . fst $ scope M.! 0
return Nothing return Nothing
nl :: BuiltinFn nl :: BuiltinFn
@ -61,45 +61,66 @@ nl = do
writeln :: BuiltinFn writeln :: BuiltinFn
writeln = write >> nl writeln = write >> nl
addBuiltins :: PrlgEnv () assertFact :: BuiltinFn
addBuiltins = do assertFact = do
a1 <- findStruct "a" 1 scope <- gets (hvar . cur)
a <- findAtom "a" heap <- gets (heap . cur)
b <- findAtom "b" {- TODO this needs to go through PrlgInt because of cuts in assertClause -}
c <- findAtom "c" let atom a = Just [U a]
varX <- findAtom "X" struct s args = Just (U s : concat args)
b0 <- findStruct "b" 0 hrec (HeapRef tgt) src
any1 <- findStruct "any" 1 | src == tgt = Just [U (LocalRef tgt 0)]
eq2 <- findStruct "=" 2 | otherwise = Nothing
hello0 <- findStruct "hello" 0 code = heapStruct atom struct hrec heap . fst $ scope M.! 0
fail0 <- findStruct "fail" 0 case code of
true0 <- findStruct "true" 0 Just (U (Struct s):head) -> do
printlocals0 <- findStruct "print_locals" 0 addClause s (head ++ [NoGoal])
debugprint0 <- findStruct "interpreter_state" 0 return Nothing
promptretry0 <- findStruct "prompt_retry" 0 Just [U (Atom a)] -> do
write1 <- findStruct "write" 1 addClause (IR.Id a 0) [NoGoal]
writeln1 <- findStruct "writeln" 1 return Nothing
nl0 <- findStruct "nl" 0 _ -> backtrack
retractall :: BuiltinFn
retractall = do
return Nothing
{- adding the builtins -}
addOp op = modify $ \s -> s {ops = op : ops s}
addClause struct head =
modify $ \s -> modify $ \s ->
s s {defs = M.alter (Just . maybe [head] (\hs -> head : hs)) struct $ defs s}
{ defs =
M.fromList addProcedure struct heads =
[ (eq2, [[U (LocalRef 0 varX), U (LocalRef 0 varX), NoGoal]]) modify $ \s -> s {defs = M.insert struct heads $ defs s}
, (any1, [[U VoidRef, NoGoal]])
, (fail0, [[Invoke $ bi backtrack]]) addProc n a c = do
, (true0, [[Invoke $ bi (pure Nothing)]]) sym <- findStruct n a
, ( debugprint0 addProcedure sym c
, [[Invoke $ bi (get >>= liftIO . print >> pure Nothing)]])
, (printlocals0, [[Invoke $ bi printLocals]]) addBi0 n b = addProc n 0 [[Invoke $ bi b]]
, (promptretry0, [[Invoke $ bi promptRetry]])
, (write1, [[U (LocalRef 0 varX), Invoke $ bi write]]) addPrelude :: PrlgEnv ()
, (writeln1, [[U (LocalRef 0 varX), Invoke $ bi writeln]]) addPrelude = do
, (nl0, [[Invoke $ bi nl]]) pure undefined
, (a1, [[U (Atom a), NoGoal], [U (Atom b), NoGoal]]) {- primitives -}
, ( b0 addBi0 "true" (pure Nothing)
, [ [Goal, U (Struct a1), U (Atom c), LastCall] addBi0 "fail" backtrack
, [Goal, U (Struct a1), U (Atom b), LastCall] addOp $ O.xfx "=" 700
]) addProc "=" 2 [[U (LocalRef 0 0), U (LocalRef 0 0), NoGoal]]
] {- clauses -}
, ops = [(O.xfy "," 1000), (O.xfx "=" 700)] addOp $ O.xfy "," 1000
} addOp $ O.xfx ":-" 1200
addOp $ O.fx ":-" 1200
addProc "assert" 1 [[U (LocalRef 0 0), Invoke (bi assertFact)]]
addProc "retractall" 1 [[U (LocalRef 0 0), Invoke (bi retractall)]]
{- query tools -}
addBi0 "print_locals" printLocals
addBi0 "prompt_retry" promptRetry
{- IO -}
addProc "write" 1 [[U (LocalRef 0 0), Invoke (bi write)]]
addProc "writeln" 1 [[U (LocalRef 0 0), Invoke (bi writeln)]]
addBi0 "nl" nl
{- debug -}
addBi0 "interpreter_trace" (get >>= liftIO . print >> pure Nothing)

View file

@ -1,3 +1,5 @@
{-# LANGUAGE TupleSections #-}
module Code where module Code where
import Control.Monad.Trans.State.Lazy import Control.Monad.Trans.State.Lazy
@ -32,7 +34,7 @@ data Heap =
Heap Int (M.Map Int Datum) Heap Int (M.Map Int Datum)
deriving (Show) deriving (Show)
emptyHeap = Heap 0 M.empty emptyHeap = Heap 1 M.empty
type Scope = M.Map Int (Int, Int) type Scope = M.Map Int (Int, Int)
@ -70,3 +72,50 @@ data Builtin =
instance Show Builtin where instance Show Builtin where
show _ = "Builtin _" show _ = "Builtin _"
codeStruct ::
Monad m
=> (Datum -> m a)
-> (Datum -> [a] -> m a)
-> (Datum -> m (Either Int a))
-> (Datum -> Int -> m a)
-> m a
-> Heap
-> Code
-> m (Code, a)
codeStruct atom struct local rec end heap = go
where
go [] = ([], ) <$> end
go (U lr@(LocalRef _ _):cs) = do
x <- local lr
case x of
Left ref -> (cs, ) <$> heapStruct atom struct rec heap ref
Right a -> pure (cs, a)
go (U s@(Struct (IR.Id _ arity)):cs) = eat arity cs >>= traverse (struct s)
go (U x:cs) = (cs, ) <$> atom x
go cs = (cs, ) <$> end
eat n cs
| n <= 0 = pure (cs, [])
| otherwise = do
(rest, a) <- go cs
fmap (a :) <$> eat (n - 1) rest
heapStruct ::
Monad m
=> (Datum -> m a)
-> (Datum -> [a] -> m a)
-> (Datum -> Int -> m a)
-> Heap
-> Int
-> m a
heapStruct atom struct rec (Heap _ heap) hr = go [hr] hr
where
go visited ref
| rr@(HeapRef r) <- heap M.! ref =
if r == ref || r `elem` visited
then rec rr ref
else go (r : visited) r
| s@(Struct (IR.Id _ arity)) <- heap M.! ref =
sequence [go (ref + i : visited) (ref + i) | i <- [1 .. arity]] >>=
struct s
| x <- heap M.! ref = atom x

View file

@ -68,12 +68,12 @@ interpret = (>> return True) . lex
interpreterStart :: PrlgEnv () interpreterStart :: PrlgEnv ()
interpreterStart = do interpreterStart = do
addBuiltins addPrelude
interpreterLoop interpreterLoop
interpreterLoop :: PrlgEnv () interpreterLoop :: PrlgEnv ()
interpreterLoop = do interpreterLoop = do
minput <- lift $ getInputLine "prlg> " minput <- lift $ getInputLine "prlg? " --TODO switch with plain .
case minput of case minput of
Nothing -> return () Nothing -> return ()
Just input -> do Just input -> do

View file

@ -25,7 +25,7 @@ data StrTable =
StrTable Int (M.Map String Int) (M.Map Int String) StrTable Int (M.Map String Int) (M.Map Int String)
deriving (Show) deriving (Show)
emptystrtable = StrTable 0 M.empty M.empty emptystrtable = StrTable 1 M.empty M.empty
strtablize t@(StrTable nxt fwd rev) str = strtablize t@(StrTable nxt fwd rev) str =
case fwd M.!? str of case fwd M.!? str of