jukebox 0.5 → 0.5.1

raw patch · 2 files changed

+42/−8 lines, 2 files

Files

• jukebox.cabal +1/−1
• src/Jukebox/TPTP/Parse/Core.hs +41/−7

@@ -1,5 +1,5 @@ Name: jukebox-Version: 0.5+Version: 0.5.1 Cabal-version: >= 1.10 Build-type: Simple Author: Nick Smallbone

@@ -175,7 +175,7 @@ {-# 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 @@       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,21 +505,50 @@  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