From 58367975aed706172487727330670d62fcb0e6d1 Mon Sep 17 00:00:00 2001 From: Mirek Kratochvil Date: Fri, 25 Nov 2022 22:18:11 +0100 Subject: [PATCH] assert v0 --- app/Builtins.hs | 139 ++++++++++++++++++++++++++++-------------------- app/Code.hs | 51 +++++++++++++++++- app/Frontend.hs | 4 +- app/IR.hs | 2 +- 4 files changed, 133 insertions(+), 63 deletions(-) diff --git a/app/Builtins.hs b/app/Builtins.hs index 8ad94ef..4c08884 100644 --- a/app/Builtins.hs +++ b/app/Builtins.hs @@ -4,6 +4,7 @@ import Code import Control.Monad.IO.Class import Control.Monad.Trans.Class import Control.Monad.Trans.State.Lazy +import Data.Functor.Identity import Data.List (intercalate) import qualified Data.Map as M import Env hiding (PrlgEnv) @@ -14,28 +15,27 @@ import System.Console.Haskeline bi = Builtin -showTerm itos heap visited ref - | ref `elem` visited = "_Rec" ++ show ref - | HeapRef r <- heap M.! ref = - if r == ref - then "_X" ++ show ref - else showTerm itos heap (ref : visited) r - | Struct (IR.Id h arity) <- heap M.! ref = - itos M.! h ++ - "(" ++ - intercalate - "," - [showTerm itos heap (ref : visited) (ref + i) | i <- [1 .. arity]] ++ - ")" - | Atom a <- heap M.! ref = itos M.! a +showTerm itos heap = runIdentity . heapStruct atom struct hrec heap + where + atom (Atom a) = pure $ itos M.! a + atom VoidRef = pure "_" + struct (Struct (IR.Id h _)) args = + pure $ itos M.! h ++ "(" ++ intercalate "," args ++ ")" + hrec (HeapRef hr) ref = + pure $ + (if hr == ref + then "_X" + else "_Rec") ++ + show hr printLocals :: BuiltinFn printLocals = do scope <- gets (gvar . cur) - Heap _ heap <- gets (heap . cur) + heap <- gets (heap . cur) IR.StrTable _ _ itos <- gets strtable 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 promptRetry :: BuiltinFn @@ -48,9 +48,9 @@ promptRetry = do write :: BuiltinFn write = do scope <- gets (hvar . cur) - Heap _ heap <- gets (heap . cur) + heap <- gets (heap . cur) 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 nl :: BuiltinFn @@ -61,45 +61,66 @@ nl = do writeln :: BuiltinFn writeln = write >> nl -addBuiltins :: PrlgEnv () -addBuiltins = do - a1 <- findStruct "a" 1 - a <- findAtom "a" - b <- findAtom "b" - c <- findAtom "c" - varX <- findAtom "X" - b0 <- findStruct "b" 0 - any1 <- findStruct "any" 1 - eq2 <- findStruct "=" 2 - hello0 <- findStruct "hello" 0 - fail0 <- findStruct "fail" 0 - true0 <- findStruct "true" 0 - printlocals0 <- findStruct "print_locals" 0 - debugprint0 <- findStruct "interpreter_state" 0 - promptretry0 <- findStruct "prompt_retry" 0 - write1 <- findStruct "write" 1 - writeln1 <- findStruct "writeln" 1 - nl0 <- findStruct "nl" 0 +assertFact :: BuiltinFn +assertFact = do + scope <- gets (hvar . cur) + heap <- gets (heap . cur) + {- TODO this needs to go through PrlgInt because of cuts in assertClause -} + let atom a = Just [U a] + struct s args = Just (U s : concat args) + hrec (HeapRef tgt) src + | src == tgt = Just [U (LocalRef tgt 0)] + | otherwise = Nothing + code = heapStruct atom struct hrec heap . fst $ scope M.! 0 + case code of + Just (U (Struct s):head) -> do + addClause s (head ++ [NoGoal]) + return Nothing + Just [U (Atom a)] -> do + addClause (IR.Id a 0) [NoGoal] + return Nothing + _ -> backtrack + +retractall :: BuiltinFn +retractall = do + return Nothing + +{- adding the builtins -} +addOp op = modify $ \s -> s {ops = op : ops s} + +addClause struct head = modify $ \s -> - s - { defs = - M.fromList - [ (eq2, [[U (LocalRef 0 varX), U (LocalRef 0 varX), NoGoal]]) - , (any1, [[U VoidRef, NoGoal]]) - , (fail0, [[Invoke $ bi backtrack]]) - , (true0, [[Invoke $ bi (pure Nothing)]]) - , ( debugprint0 - , [[Invoke $ bi (get >>= liftIO . print >> pure Nothing)]]) - , (printlocals0, [[Invoke $ bi printLocals]]) - , (promptretry0, [[Invoke $ bi promptRetry]]) - , (write1, [[U (LocalRef 0 varX), Invoke $ bi write]]) - , (writeln1, [[U (LocalRef 0 varX), Invoke $ bi writeln]]) - , (nl0, [[Invoke $ bi nl]]) - , (a1, [[U (Atom a), NoGoal], [U (Atom b), NoGoal]]) - , ( b0 - , [ [Goal, U (Struct a1), U (Atom c), LastCall] - , [Goal, U (Struct a1), U (Atom b), LastCall] - ]) - ] - , ops = [(O.xfy "," 1000), (O.xfx "=" 700)] - } + s {defs = M.alter (Just . maybe [head] (\hs -> head : hs)) struct $ defs s} + +addProcedure struct heads = + modify $ \s -> s {defs = M.insert struct heads $ defs s} + +addProc n a c = do + sym <- findStruct n a + addProcedure sym c + +addBi0 n b = addProc n 0 [[Invoke $ bi b]] + +addPrelude :: PrlgEnv () +addPrelude = do + pure undefined + {- primitives -} + addBi0 "true" (pure Nothing) + addBi0 "fail" backtrack + addOp $ O.xfx "=" 700 + addProc "=" 2 [[U (LocalRef 0 0), U (LocalRef 0 0), NoGoal]] + {- clauses -} + 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) diff --git a/app/Code.hs b/app/Code.hs index df3401e..b1c474b 100644 --- a/app/Code.hs +++ b/app/Code.hs @@ -1,3 +1,5 @@ +{-# LANGUAGE TupleSections #-} + module Code where import Control.Monad.Trans.State.Lazy @@ -32,7 +34,7 @@ data Heap = Heap Int (M.Map Int Datum) deriving (Show) -emptyHeap = Heap 0 M.empty +emptyHeap = Heap 1 M.empty type Scope = M.Map Int (Int, Int) @@ -70,3 +72,50 @@ data Builtin = instance Show Builtin where 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 diff --git a/app/Frontend.hs b/app/Frontend.hs index fc57efc..8232b15 100644 --- a/app/Frontend.hs +++ b/app/Frontend.hs @@ -68,12 +68,12 @@ interpret = (>> return True) . lex interpreterStart :: PrlgEnv () interpreterStart = do - addBuiltins + addPrelude interpreterLoop interpreterLoop :: PrlgEnv () interpreterLoop = do - minput <- lift $ getInputLine "prlg> " + minput <- lift $ getInputLine "prlg? " --TODO switch with plain . case minput of Nothing -> return () Just input -> do diff --git a/app/IR.hs b/app/IR.hs index 50c7493..fa987e5 100644 --- a/app/IR.hs +++ b/app/IR.hs @@ -25,7 +25,7 @@ data StrTable = StrTable Int (M.Map String Int) (M.Map Int String) deriving (Show) -emptystrtable = StrTable 0 M.empty M.empty +emptystrtable = StrTable 1 M.empty M.empty strtablize t@(StrTable nxt fwd rev) str = case fwd M.!? str of