diff options
| -rw-r--r-- | app/Compiler.hs | 4 | ||||
| -rw-r--r-- | app/Frontend.hs | 128 | ||||
| -rw-r--r-- | app/Main.hs | 44 | ||||
| -rw-r--r-- | app/Parser.hs | 99 | ||||
| -rw-r--r-- | prlg.cabal | 4 |
5 files changed, 186 insertions, 93 deletions
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 @@ -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 |