From b9633a33182f5b381e912366273709e59f469bb9 Mon Sep 17 00:00:00 2001 From: Mirek Kratochvil Date: Sat, 12 Nov 2022 17:47:51 +0100 Subject: [PATCH] reorg. --- app/Builtins.hs | 31 +++++++++++++++++ app/Code.hs | 56 +++++++++++++++++++++++++++++++ app/Compiler.hs | 18 +++------- app/Env.hs | 33 ++++++++++++++++++ app/Frontend.hs | 66 +++++------------------------------- app/IR.hs | 33 ++++++++++++++++++ app/Interpreter.hs | 73 ++-------------------------------------- app/Main.hs | 2 +- app/Operators.hs | 42 +++++++++++++++++++++++ app/Parser.hs | 83 +++++++++++++++++----------------------------- prlg.cabal | 2 +- 11 files changed, 244 insertions(+), 195 deletions(-) create mode 100644 app/Builtins.hs create mode 100644 app/Code.hs create mode 100644 app/Env.hs create mode 100644 app/IR.hs create mode 100644 app/Operators.hs diff --git a/app/Builtins.hs b/app/Builtins.hs new file mode 100644 index 0000000..272eca2 --- /dev/null +++ b/app/Builtins.hs @@ -0,0 +1,31 @@ +module Builtins where + +import Code hiding (defs) +import Control.Monad.Trans.State.Lazy +import qualified Data.Map as M +import Env +import qualified Operators as O + +addBuiltins :: PrlgEnv () +addBuiltins = do + a1 <- findStruct "a" 1 + a <- findAtom "a" + b <- findAtom "b" + c <- findAtom "c" + b0 <- findStruct "b" 0 + any <- findStruct "any" 1 + eq <- findStruct "=" 2 + modify $ \s -> + s + { defs = + M.fromList + [ (eq, [[U (LocalRef 0), U (LocalRef 0), NoGoal]]) + , (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] + ]) + , (any, [[U VoidRef, NoGoal]]) + ] + , ops = [(O.xfy "," 1000), (O.xfx "=" 700)] + } diff --git a/app/Code.hs b/app/Code.hs new file mode 100644 index 0000000..3488f0b --- /dev/null +++ b/app/Code.hs @@ -0,0 +1,56 @@ +module Code where + +import qualified Data.Map as M +import IR (Id(..)) + +data Datum + = Atom Int -- unifies a constant + | Struct Id -- unifies a structure with arity + | VoidRef -- unifies with anything + | LocalRef Int -- code-local variable idx (should not occur on heap) + | HeapRef Int -- heap structure idx + deriving (Show, Eq, Ord) + +data Instr + = U Datum -- something unifiable + | NoGoal -- trivial goal + | Goal -- we start a new goal, set up backtracking etc + | Call -- all seems okay, call the goal + | LastCall -- tail call the goal + | Cut -- remove all alternative clauses of the current goal + deriving (Show) + +type Code = [Instr] + +type Defs = M.Map Id [Code] + +data Heap = + Heap Int (M.Map Int Datum) + deriving (Show) + +emptyHeap = Heap 0 M.empty + +type Scope = M.Map Int Int + +emptyScope :: Scope +emptyScope = M.empty + +data Cho = + Cho + { hed :: Code -- head pointer + , hvar :: Scope -- variables unified in head (so far) + , gol :: Code -- goal pointer + , gvar :: Scope -- variables unified in the goal + , heap :: Heap -- a snapshot of the heap (there's no trail; we rely on CoW copies in other choicepoints) + , stk :: [(Code, Scope, [Cho])] -- remaining goals together with their vars and cuts + , cut :: [Cho] -- snapshot of choicepoints before entering + } + deriving (Show) + +data Interp = + Interp + { defs :: Defs -- global definitions for lookup (TODO can we externalize?) + , cur :: Cho -- the choice that is being evaluated right now + , cho :: [Cho] -- remaining choice points + } + deriving (Show) diff --git a/app/Compiler.hs b/app/Compiler.hs index 4f94637..b3294a1 100644 --- a/app/Compiler.hs +++ b/app/Compiler.hs @@ -3,19 +3,9 @@ module Compiler where import Data.Char (isUpper) import Data.Containers.ListUtils (nubOrd) import Data.List -import Interpreter (Code, Datum(..), Id(..), Instr(..), StrTable, strtablize) -data PrlgStr - = CallS String [PrlgStr] - | LiteralS String - deriving (Show) - -data PrlgInt - = CallI Id [PrlgInt] - | LiteralI Int - | VarI Int Int - | VoidI - deriving (Show) +import Code (Code, Datum(..), Instr(..)) +import IR (Id(..), PrlgInt(..), PrlgStr(..), StrTable, strtablize) varname :: String -> Bool varname ('_':_) = True @@ -28,8 +18,8 @@ varnames (LiteralS x) | varname x = [x] | otherwise = [] -strtablizePrlg :: [String] -> StrTable -> PrlgStr -> (StrTable, PrlgInt) -strtablizePrlg stab = go +internPrlg :: [String] -> StrTable -> PrlgStr -> (StrTable, PrlgInt) +internPrlg stab = go where go t (LiteralS str) | str == "_" = (t, VoidI) diff --git a/app/Env.hs b/app/Env.hs new file mode 100644 index 0000000..7ede4c2 --- /dev/null +++ b/app/Env.hs @@ -0,0 +1,33 @@ +module Env where + +import qualified Code +import Control.Monad.IO.Class +import Control.Monad.Trans.State.Lazy +import qualified IR +import qualified Operators +import System.Console.Haskeline + +data PrlgState = + PrlgState + { defs :: Code.Defs + , ops :: Operators.Ops + , strtable :: IR.StrTable + } + deriving (Show) + +type PrlgEnv a = StateT PrlgState (InputT IO) a + +withStrTable :: (IR.StrTable -> (IR.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 IR.Id +findStruct str arity = do + stri <- findAtom str + return IR.Id {IR.str = stri, IR.arity = arity} + +findAtom :: String -> PrlgEnv Int +findAtom = withStrTable . flip IR.strtablize diff --git a/app/Frontend.hs b/app/Frontend.hs index 2c92e1f..a17a85c 100644 --- a/app/Frontend.hs +++ b/app/Frontend.hs @@ -1,27 +1,21 @@ module Frontend where +import Builtins +import qualified Code 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 Env +import qualified IR 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 $ @@ -34,21 +28,6 @@ ppr x = } 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 @@ -59,15 +38,14 @@ interpret = (>> return True) . lex 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 + Right asts -> traverse_ shunt asts + shunt ast = do o <- gets ops - case P.ast2prlg o ast of + case P.shuntPrlg o ast of Left err -> liftIO $ putStrLn $ "expression parsing: " ++ err Right prlg -> intern prlg intern prlgs = do - prlgi <- - withStrTable $ \st -> C.strtablizePrlg (C.varnames prlgs) st prlgs + prlgi <- withStrTable $ \st -> C.internPrlg (C.varnames prlgs) st prlgs compile prlgi compile prlgi {- TODO: switch between prove goal/compile clause here -} @@ -87,32 +65,6 @@ interpret = (>> return True) . lex then "yes." else "no proof." -addBuiltins = do - a1 <- findStruct "a" 1 - a <- findAtom "a" - b <- findAtom "b" - c <- findAtom "c" - b0 <- findStruct "b" 0 - any <- findStruct "any" 1 - eq <- findStruct "=" 2 - modify $ \s -> - s - { defs = - M.fromList - [ (eq, [[I.U (I.LocalRef 0),I.U (I.LocalRef 0), I.NoGoal]]) - , (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] - ]) - , (any, [[I.U I.VoidRef, I.NoGoal]]) - ] - , ops = - [ (",", P.Op 1000 $ P.Infix P.X P.Y) - , ("=", P.Op 700 $ P.Infix P.X P.X) - ] - } - interpreterStart :: PrlgEnv () interpreterStart = do addBuiltins @@ -133,4 +85,4 @@ interpreter :: InputT IO () interpreter = evalStateT interpreterStart - (PrlgState {defs = M.empty, ops = [], strtable = I.emptystrtable}) + (PrlgState {defs = M.empty, ops = [], strtable = IR.emptystrtable}) diff --git a/app/IR.hs b/app/IR.hs new file mode 100644 index 0000000..50c7493 --- /dev/null +++ b/app/IR.hs @@ -0,0 +1,33 @@ +module IR where + +import qualified Data.Map as M + +data PrlgStr + = CallS String [PrlgStr] + | LiteralS String + deriving (Show) + +data Id = + Id + { str :: Int + , arity :: Int + } + deriving (Show, Eq, Ord) + +data PrlgInt + = CallI Id [PrlgInt] + | LiteralI Int + | VarI Int Int + | VoidI + deriving (Show) + +data StrTable = + StrTable Int (M.Map String Int) (M.Map Int String) + deriving (Show) + +emptystrtable = StrTable 0 M.empty M.empty + +strtablize t@(StrTable nxt fwd rev) str = + case fwd M.!? str of + Just i -> (t, i) + _ -> (StrTable (nxt + 1) (M.insert str nxt fwd) (M.insert nxt str rev), nxt) diff --git a/app/Interpreter.hs b/app/Interpreter.hs index b42f079..c29b701 100644 --- a/app/Interpreter.hs +++ b/app/Interpreter.hs @@ -1,78 +1,11 @@ {- VAM 2P, done the lazy way -} module Interpreter where -import Data.Function +--import Data.Function import qualified Data.Map as M -data StrTable = - StrTable Int (M.Map String Int) (M.Map Int String) - deriving (Show) - -emptystrtable = StrTable 0 M.empty M.empty - -strtablize t@(StrTable nxt fwd rev) str = - case fwd M.!? str of - Just i -> (t, i) - _ -> (StrTable (nxt + 1) (M.insert str nxt fwd) (M.insert nxt str rev), nxt) - -data Id = - Id - { str :: Int - , arity :: Int - } - deriving (Show, Eq, Ord) - -data Datum - = Atom Int -- unifies a constant - | Struct Id -- unifies a structure with arity - | VoidRef -- in code this unifies with anything; everywhere else this is an unbound variable - | LocalRef Int -- local variable idx - | HeapRef Int -- heap structure idx - deriving (Show, Eq, Ord) - -data Instr - = U Datum -- something unifiable - | NoGoal -- trivial goal - | Goal -- we start a new goal, set up backtracking etc - | Call -- all seems okay, call the goal - | LastCall -- tail call the goal - | Cut -- remove all alternative clauses of the current goal - deriving (Show) - -type Code = [Instr] - -type Defs = M.Map Id [Code] - -data Heap = - Heap Int (M.Map Int Datum) - deriving (Show) - -emptyHeap = Heap 0 M.empty - -type Scope = M.Map Int Int - -emptyScope :: Scope -emptyScope = M.empty - -data Cho = - Cho - { hed :: Code -- head pointer - , hvar :: Scope -- variables unified in head (so far) - , gol :: Code -- goal pointer - , gvar :: Scope -- variables unified in the goal - , heap :: Heap -- a snapshot of the heap (there's no trail; we rely on CoW copies in other choicepoints) - , stk :: [(Code, Scope, [Cho])] -- remaining goals together with their vars and cuts - , cut :: [Cho] -- snapshot of choicepoints before entering - } - deriving (Show) - -data Interp = - Interp - { defs :: Defs -- global definitions for lookup (TODO can we externalize?) - , cur :: Cho -- the choice that is being evaluated right now - , cho :: [Cho] -- remaining choice points - } - deriving (Show) +import Code +import IR (Id(..)) prove :: Code -> Defs -> (Interp, Either String Bool) prove g ds = diff --git a/app/Main.hs b/app/Main.hs index 2222450..1e639d2 100644 --- a/app/Main.hs +++ b/app/Main.hs @@ -1,8 +1,8 @@ module Main where import Control.Monad -import System.Console.Haskeline import Frontend (interpreter) +import System.Console.Haskeline main :: IO () main = runInputT defaultSettings interpreter diff --git a/app/Operators.hs b/app/Operators.hs new file mode 100644 index 0000000..8bf7c1e --- /dev/null +++ b/app/Operators.hs @@ -0,0 +1,42 @@ +module Operators where + +data Op = + Op Int Fixity + deriving (Show, Eq) + +data ArgKind + = X + | Y + deriving (Show, Eq) + +data Fixity + = Infix ArgKind ArgKind + | Prefix ArgKind + | Suffix ArgKind + deriving (Show, Eq) + +isPrefix (Prefix _) = True +isPrefix _ = False + +numArgs :: Op -> Int +numArgs (Op _ f) = go f + where + go (Infix _ _) = 2 + go _ = 1 + +type Ops = [(String, Op)] + +xfx, xfy, yfx, fx, fy, xf, yf :: String -> Int -> (String, Op) +xfx o p = (o, Op p (Infix X X)) + +xfy o p = (o, Op p (Infix X Y)) + +yfx o p = (o, Op p (Infix Y X)) + +fx o p = (o, Op p (Prefix X)) + +fy o p = (o, Op p (Prefix Y)) + +xf o p = (o, Op p (Suffix X)) + +yf o p = (o, Op p (Suffix Y)) diff --git a/app/Parser.hs b/app/Parser.hs index 302194e..de6af9c 100644 --- a/app/Parser.hs +++ b/app/Parser.hs @@ -1,6 +1,10 @@ {-# LANGUAGE FlexibleInstances #-} -module Parser where +module Parser + ( lexPrlg + , parsePrlg + , shuntPrlg + ) where import Control.Applicative (liftA2) import Control.Monad (void) @@ -12,7 +16,8 @@ import Data.Void import Text.Megaparsec import Text.Megaparsec.Char -import Compiler (PrlgStr(..)) +import IR (PrlgStr(..)) +import Operators singleToks = ",;|()[]" @@ -113,10 +118,10 @@ instance TraversableStream [Lexeme] where } } -data AST - = Call String [[AST]] - | Seq [AST] - | List [AST] (Maybe [AST]) +data PAST + = Call String [[PAST]] + | Seq [PAST] + | List [PAST] (Maybe [PAST]) | Literal String deriving (Show, Eq) @@ -138,7 +143,7 @@ isNormalTok _ = False unTok (Tok t) = t unTok (QTok t _) = t -literal :: Parser AST +literal :: Parser PAST literal = Literal . unTok <$> free (satisfy isNormalTok <* notFollowedBy lParen) call = do @@ -177,64 +182,38 @@ listTail = simpleTok "|" rBracket = simpleTok "]" -clause :: Parser AST +clause :: Parser PAST clause = Seq <$> some (free seqItem) <* free comma -parsePrlg :: Parser [AST] +parsePrlg :: Parser [PAST] parsePrlg = ws *> many clause <* eof -data Op = - Op Int Fixity - deriving (Show, Eq) +type ShuntError = String -data ArgKind - = X - | Y - deriving (Show, Eq) +type ShuntResult = Either ShuntError PrlgStr -data Fixity - = Infix ArgKind ArgKind - | Prefix ArgKind - | Suffix ArgKind - deriving (Show, Eq) - -isPrefix (Prefix _) = True -isPrefix _ = False - -numArgs :: Op -> Int -numArgs (Op _ f) = go f - where - go (Infix _ _) = 2 - go _ = 1 - -type Ops = [(String, Op)] - -type PrlgError = String - -type PrlgResult = Either PrlgError PrlgStr - -err :: PrlgError -> Either PrlgError a +err :: ShuntError -> Either ShuntError a err = Left -ast2prlg :: Ops -> AST -> PrlgResult -ast2prlg ot = ast2prlg' (("", Op 0 $ Infix X Y) : ot) +shuntPrlg :: Ops -> PAST -> ShuntResult +shuntPrlg ot = shuntPrlg' (("", 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 +shuntPrlg' :: Ops -> PAST -> ShuntResult +shuntPrlg' ot (List _ _) = err "no lists yet" +shuntPrlg' ot (Seq ss) = shunt ot ss +shuntPrlg' ot (Literal s) = pure (LiteralS s) +shuntPrlg' ot (Call fn ss) = CallS fn <$> traverse (shunt ot) ss -shunt :: Ops -> [AST] -> PrlgResult +shunt :: Ops -> [PAST] -> ShuntResult shunt optable = start where - start :: [AST] -> PrlgResult + start :: [PAST] -> ShuntResult 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 -> [PrlgStr] -> [PAST] -> ShuntResult wo ops vs (l@(Literal x):xs) = resolve [ do getPrefix x @@ -252,7 +231,7 @@ shunt optable = start {- end of stream, but the operand is missing -} wo ops vs [] = err "expected final operand" {- "have operand" state, expecting an operator -} - ho :: Ops -> [PrlgStr] -> [AST] -> PrlgResult + ho :: Ops -> [PrlgStr] -> [PAST] -> ShuntResult ho ops vs xs'@(Literal x:xs) = resolve [ do getSuffix x @@ -275,8 +254,8 @@ shunt optable = start (ops', vs') <- pop ops vs ho ops' vs' [] {- recurse to delimited subexpression -} - rec :: AST -> PrlgResult - rec = ast2prlg' optable + rec :: PAST -> ShuntResult + rec = shuntPrlg' 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)) @@ -292,7 +271,7 @@ shunt optable = start | null [op | (s, op) <- optable, s == x] = pure () | otherwise = err "expected an operand" {- actual pushery -} - canPush :: Ops -> Op -> Either PrlgError Bool + canPush :: Ops -> Op -> Either ShuntError Bool canPush [] op = pure True canPush ((_, Op p f):ops) (Op np nf) = go p f np nf {- helper -} diff --git a/prlg.cabal b/prlg.cabal index bd4ea19..f46dd84 100644 --- a/prlg.cabal +++ b/prlg.cabal @@ -25,7 +25,7 @@ executable prlg main-is: Main.hs -- Modules included in this executable, other than Main. - other-modules: Interpreter, Compiler, Parser, Frontend + other-modules: Interpreter, Compiler, Parser, Frontend, IR, Operators, Code, Builtins, Env -- LANGUAGE extensions used by modules in this package. -- other-extensions: