jukebox 0.5.13 → 0.5.14

raw patch · 4 files changed

+14/−7 lines, 4 filesPVP ok

version bump matches the API change (PVP)

API changes (from Hackage documentation)

Files

• jukebox.cabal +1/−1
• src/Jukebox/TPTP/Print.hs +1/−1
• src/Jukebox/Tools/Clausify.hs +3/−0
• src/Jukebox/Tools/HornToUnit.hs +9/−5

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

@@ -86,7 +86,7 @@     annot :: Input Form -> PrintProofState Int     annot inp       -- Formula is identical to its parent-      | Inference Nothing _ _ [InputPlus{inputValue = inp'}] <- source inp,+      | Inference _ _ _ [InputPlus{inputValue = inp'}] <- source inp,           let p = prettyNames (what inp)               q = prettyNames (what inp') in           isAxiom (kind inp) == isAxiom (kind inp') &&

@@ -118,6 +118,9 @@ -- core clausification algorithm  clausForm :: AxKind -> Input Form -> M [Input Clause]+clausForm _ inp+  | Just clause <- toClause (what inp) =+    return [fmap (const clause) inp] clausForm kind inp =   withName (tag inp) $     do miniscoped      <- miniscope . check . simplify         . check $ what inp

@@ -107,9 +107,11 @@  eliminatePredicates :: Problem Clause -> Problem Clause eliminatePredicates prob =-  map (fmap elim) prob+  map elim prob   where-    elim = clause . map (fmap elim1) . toLiterals+    elim inp =+      derivedClause "true_elimination" "esa" (fmap toForm inp) $+        clause . map (fmap elim1) . toLiterals $ what inp     elim1 (t :=: u) = t :=: u     elim1 (Tru ((p ::: FunType tys _) :@: ts)) =       ((p ::: FunType tys bool) :@: ts) :=: true@@ -127,8 +129,9 @@       elim inp         | (null poss && length negs /= 1 && not (allowConjunctiveConjectures flags)) ||           (not (null poss) && length negs > 1 && multi flags) =+          let conj = null poss in           derivedClause "tupling" "esa" (fmap toForm inp) $-            clause (Neg ((tuple tys :@: ts) :=: (tuple tys :@: us)):poss)+            clause (Neg ((tuple conj tys :@: ts) :=: (tuple conj tys :@: us)):poss)         where           (poss, negs) = partition pos (toLiterals (what inp))           ts = [t | l <- negs, let Neg (t :=: _) = l]@@ -139,8 +142,9 @@       tuple = run_ prob $ do         tupleType <- newName (withLabel "tuple" (name "tuple"))         tuple <- newName (withLabel "tuple" (name "tuple"))-        return $ \args ->-          variant tuple args :::+        conjectureTuple <- newName (withLabel "conjecture_tuple" (name "tuple"))+        return $ \conj args ->+          variant (if conj then conjectureTuple else tuple) args :::           FunType args (Type (variant tupleType args))  eliminateUnsuitableConjectures :: HornFlags -> Problem Clause -> Problem Clause