From 8eb307e3e11a109aeae7f96ffcb7476d93493ffb Mon Sep 17 00:00:00 2001
From: Mirek Kratochvil <exa.exa@gmail.com>
Date: Sat, 5 Nov 2022 18:02:14 +0100
Subject: [PATCH] interpreter interprets.
---
app/Compiler.hs | 4 +-
app/Frontend.hs | 128 ++++++++++++++++++++++++++++++++++++++++++++++++
app/Main.hs | 44 ++---------------
app/Parser.hs | 99 +++++++++++++++++++------------------
prlg.cabal | 4 +-
5 files changed, 186 insertions(+), 93 deletions(-)
create mode 100644 app/Frontend.hs
diff --git a/app/Compiler.hs b/app/Compiler.hs
index 7684f80..08e4b24 100644
--- a/app/Compiler.hs
+++ b/app/Compiler.hs
@@ -43,8 +43,8 @@ seqGoals [x] = [Goal] ++ x ++ [LastCall]
seqGoals [x, [Cut]] = [Goal] ++ x ++ [LastCall, Cut]
seqGoals (x:xs) = [Goal] ++ x ++ [Call] ++ seqGoals xs
-compileRule :: Id -> Id -> PrlgInt -> Code
-compileRule proveop andop = go
+compileClause :: Id -> Id -> PrlgInt -> Code
+compileClause proveop andop = go
where
go :: PrlgInt -> Code
go h@(CallI x args)
diff --git a/app/Frontend.hs b/app/Frontend.hs
new file mode 100644
index 0000000..8dc8b8a
--- /dev/null
+++ b/app/Frontend.hs
@@ -0,0 +1,128 @@
+module Frontend where
+
+import qualified Compiler as C
+import Control.Monad.IO.Class
+import Control.Monad.Trans.Class
+import Control.Monad.Trans.State.Lazy
+import Data.Foldable (traverse_)
+import qualified Data.Map as M
+import qualified Interpreter as I
+import qualified Parser as P
+import System.Console.Haskeline
+import qualified Text.Megaparsec as MP
+import Text.Pretty.Simple
+
+data PrlgState =
+ PrlgState
+ { defs :: I.Defs
+ , ops :: P.Ops
+ , strtable :: I.StrTable
+ }
+ deriving (Show)
+
+type PrlgEnv a = StateT PrlgState (InputT IO) a
+
+ppr :: Show a => a -> PrlgEnv ()
+ppr x =
+ liftIO $
+ pPrintOpt
+ CheckColorTty
+ defaultOutputOptionsDarkBg
+ { outputOptionsCompactParens = True
+ , outputOptionsIndentAmount = 2
+ , outputOptionsPageWidth = 80
+ }
+ x
+
+withStrTable :: (I.StrTable -> (I.StrTable, a)) -> PrlgEnv a
+withStrTable f = do
+ st <- gets strtable
+ let (st', x) = f st
+ modify (\s -> s {strtable = st'})
+ return x
+
+findStruct :: String -> Int -> PrlgEnv I.Id
+findStruct str arity = do
+ stri <- findAtom str
+ return I.Id {I.str = stri, I.arity = arity}
+
+findAtom :: String -> PrlgEnv Int
+findAtom = withStrTable . flip I.strtablize
+
+interpret :: String -> PrlgEnv Bool
+interpret = (>> return True) . lex
+ where
+ lex input = do
+ case MP.parse P.lexPrlg "-" input of
+ Left bundle -> liftIO $ putStr (MP.errorBundlePretty bundle)
+ Right toks -> parse toks
+ parse toks = do
+ case MP.parse P.parsePrlg "-" toks of
+ Left bundle -> liftIO $ putStr (MP.errorBundlePretty bundle)
+ Right asts -> traverse_ prologize asts
+ prologize ast = do
+ o <- gets ops
+ case P.ast2prlg o ast of
+ Left err -> liftIO $ putStrLn $ "expression parsing: " ++ err
+ Right prlg -> intern prlg
+ intern prlgs = do
+ prlgi <- withStrTable $ flip C.strtablizePrlg prlgs
+ compile prlgi
+ compile prlgi
+ {- TODO: switch between prove goal/compile clause here -}
+ = do
+ commaId <- findStruct "," 2
+ let code = C.seqGoals $ C.compileGoals commaId prlgi
+ execute code
+ execute code = do
+ ds <- gets defs
+ let (_, res) = I.prove code ds
+ case res of
+ Left err -> liftIO $ putStrLn err
+ Right res ->
+ liftIO $
+ putStrLn $
+ if res
+ then "yes."
+ else "no proof."
+
+addBuiltins = do
+ a1 <- findStruct "a" 1
+ a <- findAtom "a"
+ b <- findAtom "b"
+ c <- findAtom "c"
+ b0 <- findStruct "b" 0
+ modify $ \s ->
+ s
+ { defs =
+ M.fromList
+ [ (a1, [[I.U (I.Atom a), I.NoGoal], [I.U (I.Atom b), I.NoGoal]])
+ , ( b0
+ , [ [I.Goal, I.U (I.Struct a1), I.U (I.Atom c), I.LastCall]
+ , [I.Goal, I.U (I.Struct a1), I.U (I.Atom b), I.LastCall]
+ ])
+ ]
+ , ops = [(",", P.Op 1000 $ P.Infix P.X P.Y)]
+ }
+
+interpreterStart :: PrlgEnv ()
+interpreterStart = do
+ addBuiltins
+ interpreterLoop
+
+interpreterLoop :: PrlgEnv ()
+interpreterLoop = do
+ minput <- lift $ getInputLine "prlg> "
+ case minput of
+ Nothing -> return ()
+ Just input -> do
+ continue <- interpret input
+ if continue
+ then interpreterLoop
+ else return ()
+
+interpreter :: InputT IO ()
+interpreter =
+ evalStateT
+ interpreterStart
+ (PrlgState {defs = M.empty, ops = [], strtable = I.emptystrtable})
diff --git a/app/Main.hs b/app/Main.hs
index 5dfb25e..2222450 100644
--- a/app/Main.hs
+++ b/app/Main.hs
@@ -1,46 +1,8 @@
module Main where
-import qualified Compiler as C
-import Control.Monad.IO.Class
-import qualified Data.Map as M
-import qualified Interpreter as I
-import qualified Parser as P
+import Control.Monad
import System.Console.Haskeline
-import qualified Text.Megaparsec as MP
-import Text.Pretty.Simple
-
-ppr :: Show a => a -> IO ()
-ppr =
- pPrintOpt
- CheckColorTty
- defaultOutputOptionsDarkBg
- { outputOptionsCompactParens = True
- , outputOptionsIndentAmount = 2
- , outputOptionsPageWidth = 80
- }
-
-interpret :: String -> IO ()
-interpret = lex
- where
- lex input =
- case MP.parse P.lexPrlg "-" input of
- Left bundle -> putStr (MP.errorBundlePretty bundle)
- Right toks -> parse toks
- parse toks =
- case MP.parse P.parsePrlg "-" toks of
- Left bundle -> putStr (MP.errorBundlePretty bundle)
- Right ast -> prologize ast
- prologize ast = ppr $ map (P.ast2prlg P.defaultOps) ast
+import Frontend (interpreter)
main :: IO ()
-main =
- runInputT defaultSettings loop
- where
- loop :: InputT IO ()
- loop = do
- minput <- getInputLine "prlg> "
- case minput of
- Nothing -> return ()
- Just input -> do
- liftIO $ interpret input
- loop
+main = runInputT defaultSettings interpreter
diff --git a/app/Parser.hs b/app/Parser.hs
index 694eb64..302194e 100644
--- a/app/Parser.hs
+++ b/app/Parser.hs
@@ -13,7 +13,6 @@ import Text.Megaparsec
import Text.Megaparsec.Char
import Compiler (PrlgStr(..))
-import Debug.Trace
singleToks = ",;|()[]"
@@ -83,7 +82,8 @@ instance TraversableStream [Lexeme] where
handleEmpty x = x
go
| o <= pstateOffset pst =
- ( Just . handleEmpty $ pstateLinePrefix pst ++
+ ( Just . handleEmpty $
+ pstateLinePrefix pst ++
takeWhile (/= '\n') (concatMap showTok $ pstateInput pst)
, pst)
| o > pstateOffset pst =
@@ -209,34 +209,21 @@ numArgs (Op _ f) = go f
type Ops = [(String, Op)]
-defaultOps :: Ops
-defaultOps =
- [ ("", Op 0 $ Infix X Y)
- , ("+", Op 100 $ Prefix X)
- , ("!", Op 100 $ Suffix Y)
- , ("-", Op 100 $ Prefix Y)
- , ("*", Op 100 $ Infix Y X)
- , ("+", Op 200 $ Infix Y X)
- , ("++", Op 200 $ Infix X Y)
- , ("-", Op 200 $ Infix Y X)
- , ("<", Op 300 $ Infix X X)
- , (">", Op 300 $ Infix X X)
- , ("=", Op 400 $ Infix X X)
- , (",", Op 800 $ Infix X Y)
- , (";", Op 900 $ Infix X Y)
- , (":-", Op 1000 $ Infix X X)
- ]
-
type PrlgError = String
+
type PrlgResult = Either PrlgError PrlgStr
+
err :: PrlgError -> Either PrlgError a
err = Left
ast2prlg :: Ops -> AST -> PrlgResult
-ast2prlg ot (List _ _) = err "no lists yet"
-ast2prlg ot (Seq ss) = shunt ot ss
-ast2prlg ot (Literal s) = pure (LiteralS s)
-ast2prlg ot (Call fn ss) = CallS fn <$> traverse (shunt ot) ss
+ast2prlg ot = ast2prlg' (("", Op 0 $ Infix X Y) : ot)
+
+ast2prlg' :: Ops -> AST -> PrlgResult
+ast2prlg' ot (List _ _) = err "no lists yet"
+ast2prlg' ot (Seq ss) = shunt ot ss
+ast2prlg' ot (Literal s) = pure (LiteralS s)
+ast2prlg' ot (Call fn ss) = CallS fn <$> traverse (shunt ot) ss
shunt :: Ops -> [AST] -> PrlgResult
shunt optable = start
@@ -245,38 +232,51 @@ shunt optable = start
start [x] = rec x --singleton, possibly either a single operator name or a single value
start [] = err "empty parentheses?"
start xs = wo [] [] xs
+ resolve = foldr1 (<|>)
{- "want operand" state, incoming literal -}
wo :: Ops -> [PrlgStr] -> [AST] -> PrlgResult
- wo ops vs (l@(Literal x):xs)
- | Right _ <- getPrefix x
- , Right (ops', vs') <- pushPrefix ops vs x = wo ops' vs' xs
- | isOperand x = do l' <- rec l
- ho ops (l' : vs) xs
- | otherwise = err "expected operand"
+ wo ops vs (l@(Literal x):xs) =
+ resolve
+ [ do getPrefix x
+ (ops', vs') <- pushPrefix ops vs x
+ wo ops' vs' xs
+ , do getOperand x
+ l' <- rec l
+ ho ops (l' : vs) xs
+ , err "expected operand"
+ ]
{- incoming non-literal (i.e., surely operand), push it and switch to "have operand" -}
- wo ops vs (x:xs) = do x' <- rec x
- ho ops (x' : vs) xs
+ wo ops vs (x:xs) = do
+ x' <- rec x
+ ho ops (x' : vs) xs
{- end of stream, but the operand is missing -}
wo ops vs [] = err "expected final operand"
- {- "have operand" state, incoming operator -}
+ {- "have operand" state, expecting an operator -}
ho :: Ops -> [PrlgStr] -> [AST] -> PrlgResult
- ho ops vs xs'@(Literal x:xs)
- | Right _ <- getSuffix x
- , Right (ops', vs') <- pushSuffix ops vs x = ho ops' vs' xs
- | Right _ <- getInfix x
- , Right (ops', vs') <- pushInfix ops vs x = wo ops' vs' xs
- | isOperand x = ho ops vs (Literal "" : xs') -- app (see below)
- | Right _ <- getPrefix x = ho ops vs (Literal "" : xs') -- also app!
- | otherwise = err "expected infix or suffix operator"
- {- incoming operand; there's an app between -}
+ ho ops vs xs'@(Literal x:xs) =
+ resolve
+ [ do getSuffix x
+ (ops', vs') <- pushSuffix ops vs x
+ ho ops' vs' xs
+ , do getInfix x
+ (ops', vs') <- pushInfix ops vs x
+ wo ops' vs' xs
+ , do getOperand x
+ ho ops vs (Literal "" : xs') -- app (see below)
+ , do getPrefix x
+ ho ops vs (Literal "" : xs') -- also app!
+ , err "expected infix or suffix operator"
+ ]
+ {- incoming non-literal operand; there must be an app in between -}
ho ops vs xs@(_:_) = ho ops vs (Literal "" : xs)
{- the last operand was last, pop until finished -}
ho [] [res] [] = pure res
- ho ops vs [] = do (ops', vs') <- pop ops vs
- ho ops' vs' []
+ ho ops vs [] = do
+ (ops', vs') <- pop ops vs
+ ho ops' vs' []
{- recurse to delimited subexpression -}
rec :: AST -> PrlgResult
- rec = ast2prlg optable
+ rec = ast2prlg' optable
{- pop a level, possibly uncovering a higher prio -}
pop ((x, Op _ (Infix _ _)):ops) (r:l:vs) = pure (ops, (CallS x [l, r] : vs))
pop ((x, Op _ (Prefix _)):ops) (p:vs) = pure (ops, (CallS x [p] : vs))
@@ -288,7 +288,9 @@ shunt optable = start
getPrefix x = uniq [op | (s, op@(Op _ (Prefix _))) <- optable, s == x]
getSuffix x = uniq [op | (s, op@(Op _ (Suffix _))) <- optable, s == x]
getInfix x = uniq [op | (s, op@(Op _ (Infix _ _))) <- optable, s == x]
- isOperand x = null [op | (s, op) <- optable, s == x]
+ getOperand x
+ | null [op | (s, op) <- optable, s == x] = pure ()
+ | otherwise = err "expected an operand"
{- actual pushery -}
canPush :: Ops -> Op -> Either PrlgError Bool
canPush [] op = pure True
@@ -336,5 +338,6 @@ shunt optable = start
cp <- canPush ops op
if cp
then pure ((x, op) : ops, vs)
- else do (ops', vs') <- pop ops vs
- shunt1 ops' vs' x op --prefix would behave differently here but that's impossible by canPush
+ else do
+ (ops', vs') <- pop ops vs
+ shunt1 ops' vs' x op --prefix would behave differently here but that's impossible by canPush
diff --git a/prlg.cabal b/prlg.cabal
index 83d527d..bd4ea19 100644
--- a/prlg.cabal
+++ b/prlg.cabal
@@ -25,10 +25,10 @@ executable prlg
main-is: Main.hs
-- Modules included in this executable, other than Main.
- other-modules: Interpreter, Compiler, Parser
+ other-modules: Interpreter, Compiler, Parser, Frontend
-- LANGUAGE extensions used by modules in this package.
-- other-extensions:
- build-depends: base >=4.16, containers, megaparsec, haskeline, pretty-simple, split
+ build-depends: base >=4.16, containers, megaparsec, haskeline, pretty-simple, split, transformers
hs-source-dirs: app
default-language: Haskell2010