summaryrefslogtreecommitdiff
diff options
context:
space:
mode:
authorMirek Kratochvil <exa.exa@gmail.com>2022-11-12 17:47:51 +0100
committerMirek Kratochvil <exa.exa@gmail.com>2022-11-12 17:47:51 +0100
commitb9633a33182f5b381e912366273709e59f469bb9 (patch)
tree0b7eb7f1e67792253cfaf9caee3a92570ab60407
parentfe6666d204c0728b4556574ddc184bc46013b193 (diff)
downloadprlg-b9633a33182f5b381e912366273709e59f469bb9.tar.gz
prlg-b9633a33182f5b381e912366273709e59f469bb9.tar.bz2
reorg.
-rw-r--r--app/Builtins.hs31
-rw-r--r--app/Code.hs56
-rw-r--r--app/Compiler.hs18
-rw-r--r--app/Env.hs33
-rw-r--r--app/Frontend.hs66
-rw-r--r--app/IR.hs33
-rw-r--r--app/Interpreter.hs73
-rw-r--r--app/Main.hs2
-rw-r--r--app/Operators.hs42
-rw-r--r--app/Parser.hs83
-rw-r--r--prlg.cabal2
11 files changed, 244 insertions, 195 deletions
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)
-
-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)]
-
-type PrlgError = String
+type ShuntError = String
-type PrlgResult = Either PrlgError PrlgStr
+type ShuntResult = Either ShuntError 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: