summaryrefslogtreecommitdiff
diff options
context:
space:
mode:
authorNickSmallbone <>2020-07-29 12:45:00 (GMT)
committerhdiff <hdiff@hdiff.luite.com>2020-07-29 12:45:00 (GMT)
commit1739c752f83905e71fb81259fb42f3174884675d (patch)
tree2d5cfa8a0290e73d09f4595c857a58b7ae1fe87d
parent1f9b922def78c7729f8d1b752582109c79eb05ac (diff)
version 0.5.10.5.1
-rw-r--r--jukebox.cabal2
-rw-r--r--src/Jukebox/TPTP/Parse/Core.hs48
2 files changed, 42 insertions, 8 deletions
diff --git a/jukebox.cabal b/jukebox.cabal
index 75e85e5..3bc85cc 100644
--- a/jukebox.cabal
+++ b/jukebox.cabal
@@ -1,5 +1,5 @@
Name: jukebox
-Version: 0.5
+Version: 0.5.1
Cabal-version: >= 1.10
Build-type: Simple
Author: Nick Smallbone
diff --git a/src/Jukebox/TPTP/Parse/Core.hs b/src/Jukebox/TPTP/Parse/Core.hs
index 98251e5..81bc73f 100644
--- a/src/Jukebox/TPTP/Parse/Core.hs
+++ b/src/Jukebox/TPTP/Parse/Core.hs
@@ -175,7 +175,7 @@ punct' p = satisfy p'
{-# INLINE punct #-}
punct k = punct' (== k) <?> "'" ++ show k ++ "'"
{-# INLINE operator #-}
-operator = punct' p <?> "operator"
+operator q = punct' (\x -> p x && q x) <?> "operator"
where
p Dot = True
p Colon = True
@@ -367,6 +367,11 @@ lookupFunction def x = do
return [decl]
Just fs -> return fs
+getFunctions :: Parser (Map Symbol [Function])
+getFunctions = do
+ MkState _ _ _ f _ _ <- getState
+ return f
+
-- Parsing formulae.
cnf, tff, fof :: Parser Form
@@ -500,22 +505,51 @@ atomic mode ctx = function <|> var mode ctx <|> num <|> parens (parser mode ctx)
unary :: TermLike a => Mode -> Map Symbol Variable -> Parser a
unary mode ctx =
- atomic mode ctx <|> do
- Punct p <- operator
- arg <- atomic mode ctx :: Parser Term
- fromThing (Apply (showPunct p) [arg])
+ prefix <|> do
+ t <- atomic mode ctx :: Parser Thing
+ maybePostfix t
+ where
+ prefix :: TermLike a => Parser a
+ prefix = do
+ p <- prefixOperator
+ arg <- prefix <|> atomic mode ctx :: Parser Term
+ fromThing (Apply p [arg])
+ maybePostfix, postfix :: TermLike a => Thing -> Parser a
+ maybePostfix t = postfix t <|> fromThing t
+ postfix t = do
+ p <- postfixOperator
+ arg <- fromThing t :: Parser Term
+ maybePostfix (Apply p [arg])
term :: TermLike a => Mode -> Map Symbol Variable -> Parser a
term mode ctx = do
t <- unary mode ctx :: Parser Thing
let
binop = do
- Punct p <- operator
+ p <- infixOperator
lhs <- fromThing t :: Parser Term
rhs <- unary mode ctx :: Parser Term
- fromThing (Apply (showPunct p) [lhs, rhs])
+ fromThing (Apply p [lhs, rhs])
binop <|> fromThing t
+postfixOperator :: Parser Symbol
+postfixOperator = do
+ funcs <- getFunctions
+ Punct p <- operator (isPostfix funcs)
+ return (intern ('_':show p))
+
+prefixOperator :: Parser Symbol
+prefixOperator = do
+ funcs <- getFunctions
+ Punct p <- operator (not . isPostfix funcs)
+ return (showPunct p)
+
+infixOperator :: Parser Symbol
+infixOperator = prefixOperator -- we don't syntactically distinguish them
+
+isPostfix :: Map Symbol [Function] -> Punct -> Bool
+isPostfix ctx p = intern ('_':show p) `Map.member` ctx
+
literal, unitary, quantified, formula ::
TermLike a => Mode -> Map Symbol Variable -> Parser a
{-# INLINE literal #-}