jukebox 0.5.4 → 0.5.5

raw patch · 3 files changed

+19/−20 lines, 3 filesdep ~transformers

Dependency ranges changed: transformers

Files

• jukebox.cabal +1/−1
• src/Jukebox/TPTP/Lexer.x +9/−9
• src/Jukebox/Tools/HornToUnit.hs +9/−10

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

@@ -19,7 +19,7 @@ import Data.Char import Data.Ratio import Codec.Binary.UTF8.String-import Data.Symbol+import qualified Data.Symbol as S }  $alpha = [a-zA-Z0-9_]@@ -98,10 +98,10 @@  { data Pos = Pos {-# UNPACK #-} !Word {-# UNPACK #-} !Word deriving Show-data Token = Atom { keyword :: !Keyword, tokenName :: {-# UNPACK #-} !Symbol }+data Token = Atom { keyword :: !Keyword, tokenName :: {-# UNPACK #-} !S.Symbol }            | Defined { defined :: !Defined  }-           | Var { tokenName :: {-# UNPACK #-} !Symbol }-           | DistinctObject { tokenName :: {-# UNPACK #-} !Symbol }+           | Var { tokenName :: {-# UNPACK #-} !S.Symbol }+           | DistinctObject { tokenName :: {-# UNPACK #-} !S.Symbol }            | Number { value :: !Integer }            | Rational { ratValue :: !Rational }            | Real { ratValue :: !Rational }@@ -147,10 +147,10 @@            | Or | And | Not | Iff | Implies | Follows | Xor | Nor | Nand            | Eq | Neq | ForAll | Exists | Let | LetTerm -- FOF            | Colon | Times | Plus | FunArrow -- TFF-           | Other {-# UNPACK #-} !Symbol -- user-defined+           | Other {-# UNPACK #-} !S.Symbol -- user-defined              deriving (Eq, Ord) -showPunct :: Punct -> Symbol+showPunct :: Punct -> S.Symbol showPunct x =   case x of {     LParen -> "("; RParen -> ")"; LBrack -> "["; RBrack -> "]";@@ -161,14 +161,14 @@     FunArrow -> ">"; LetTerm -> ":-"; Other x -> x }  instance Show Punct where-  show = unintern . showPunct+  show = S.unintern . showPunct  p x = const (Punct x) k x = Atom x . copy d x = const (Defined x) -copy :: String -> Symbol-copy = intern+copy :: String -> S.Symbol+copy = S.intern  unquote :: String -> String unquote (_:x)

@@ -33,7 +33,6 @@ import qualified Data.Set as Set import qualified Data.Map.Strict as Map import Control.Monad.Trans.RWS-import Control.Monad.Trans.List import Control.Monad.Trans.Class  data HornFlags =@@ -176,7 +175,7 @@   (prob, funs) <- evalRWST (mapM elim1 prob) () 0   return (map toInput (usort funs) ++ concat prob)   where-    fresh base = lift $ do+    fresh base = do       n <- get       put $! n+1       return (variant base [name (show n)])@@ -193,16 +192,16 @@     elim1 c =       case partition pos (toLiterals (what c)) of         ([], _) -> return [c]-        ([Pos l], ls) -> runListT $ do+        ([Pos l], ls) -> do           l <- foldM (encode (tag c)) l ls-          return c { what = clause [Pos l] }+          return [c { what = clause [Pos l] }]         _ ->           if dropNonHorn flags then             return []           else             lift $ Left c -    encode :: String -> Atomic -> Literal -> ListT (RWST () [(String, Atomic)] Int (Either (Input Clause))) Atomic+    encode :: String -> Atomic -> Literal -> RWST () [(String, Atomic)] Int (Either (Input Clause)) Atomic     encode tag (c :=: d) (Neg (a :=: b)) =       let         ty1 = typ a@@ -226,7 +225,7 @@         -- ifeq(a, b, c, d) = d         Asymmetric1 -> do           ifeq <- passiveFresh (variant ifeqName [name ty1, name ty2] ::: FunType [ty1, ty1, ty2, ty2] ty2)-          (c :=: d) <- return (swap size (c :=: d))+          ~(c :=: d) <- return (swap size (c :=: d))           if passivise flags then do             axiom ("ifeq_axiom", ifeq :@: [x, x, passive c, y] :=: c)             return (ifeq :@: [a, b, passive c, passive d] :=: d)@@ -238,8 +237,8 @@         -- where sigma = FV(a, b, c, d)         Asymmetric2 -> do           ifeqName <- fresh freshName-          (a :=: b) <- return (swap size (a :=: b))-          (c :=: d) <- return (swap size (c :=: d))+          ~(a :=: b) <- return (swap size (a :=: b))+          ~(c :=: d) <- return (swap size (c :=: d))           let             vs =               if passivise flags then@@ -259,7 +258,7 @@         -- where sigma = FV(c, d)         Asymmetric3 -> do           ifeqName <- fresh freshName-          (c :=: d) <- return (swap size (c :=: d))+          ~(c :=: d) <- return (swap size (c :=: d))           let             vs =               if passivise flags then@@ -276,7 +275,7 @@       (\(t :=: u) -> if smaller flags then u :=: t else t :=: u) $       if f t >= f u then (t :=: u) else (u :=: t) -    axiom l = lift $ tell [l]+    axiom l = tell [l]      toInput (tag, l) =       Input {