interpreter interprets.

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
+compileClause :: Id -> Id -> PrlgInt -> Code
-compileRule proveop andop = go
+compileClause proveop andop = go
   where
     go :: PrlgInt -> Code
     go h@(CallI x args)

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})

app/Main.hs

@@ -1,46 +1,8 @@
 module Main where
 
-import qualified Compiler as C
+import Control.Monad
-import Control.Monad.IO.Class
-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 Frontend (interpreter)
-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
 
 main :: IO ()
-main =
+main = runInputT defaultSettings interpreter
-  runInputT defaultSettings loop
-  where
-    loop :: InputT IO ()
-    loop = do
-      minput <- getInputLine "prlg> "
-      case minput of
-        Nothing -> return ()
-        Just input -> do
-          liftIO $ interpret input
-          loop

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 = ast2prlg' (("", Op 0 $ Infix X Y) : ot)
-ast2prlg ot (Seq ss) = shunt ot ss
+
-ast2prlg ot (Literal s) = pure (LiteralS s)
+ast2prlg' :: Ops -> AST -> PrlgResult
-ast2prlg ot (Call fn ss) = CallS fn <$> traverse (shunt ot) ss
+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)
+    wo ops vs (l@(Literal x):xs) =
-      | Right _ <- getPrefix x
+      resolve
-      , Right (ops', vs') <- pushPrefix ops vs x = wo ops' vs' xs
+        [ do getPrefix x
-      | isOperand x = do l' <- rec l
+             (ops', vs') <- pushPrefix ops vs x
-                         ho ops (l' : vs) xs
+             wo ops' vs' xs
-      | otherwise = err "expected operand"
+        , 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
+    wo ops vs (x:xs) = do
-                          ho ops (x' : vs) xs
+      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)
+    ho ops vs xs'@(Literal x:xs) =
-      | Right _ <- getSuffix x
+      resolve
-      , Right (ops', vs') <- pushSuffix ops vs x = ho ops' vs' xs
+        [ do getSuffix x
-      | Right _ <- getInfix x
+             (ops', vs') <- pushSuffix ops vs x
-      , Right (ops', vs') <- pushInfix ops vs x = wo ops' vs' xs
+             ho ops' vs' xs
-      | isOperand x = ho ops vs (Literal "" : xs') -- app (see below)
+        , do getInfix x
-      | Right _ <- getPrefix x = ho ops vs (Literal "" : xs') -- also app!
+             (ops', vs') <- pushInfix ops vs x
-      | otherwise = err "expected infix or suffix operator"
+             wo ops' vs' xs
-    {- incoming operand; there's an app between -}
+        , 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 [] = do
-                      ho ops' vs' []
+      (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
+        else do
-                shunt1 ops' vs' x op --prefix would behave differently here but that's impossible by canPush
+          (ops', vs') <- pop ops vs
+          shunt1 ops' vs' x op --prefix would behave differently here but that's impossible by canPush

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