jukebox 0.5.7 → 0.5.8

raw patch · 3 files changed

+10/−5 lines, 3 files

Files

jukebox.cabal +1/−1
src/Jukebox/Form.hs +5/−0
src/Jukebox/TPTP/Print.hs +4/−4

jukebox.cabal view

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

src/Jukebox/Form.hs view

@@ -327,6 +327,11 @@ type Tag = String  data Kind = Ax AxKind | Conj ConjKind deriving (Eq, Ord)++isAxiom :: Kind -> Bool+isAxiom (Ax _) = True+isAxiom (Conj _) = False+ data AxKind =   Axiom | Hypothesis | Definition | Assumption | Lemma | TheoremKind |   NegatedConjecture deriving (Eq, Ord)

src/Jukebox/TPTP/Print.hs view

@@ -19,6 +19,7 @@ import Text.PrettyPrint.HughesPJClass import Control.Monad.Trans.State.Strict import Data.Symbol+import Control.Monad  pPrintClauses :: Problem Clause -> Doc pPrintClauses prob0@@ -88,11 +89,10 @@       | Inference _ _ [InputPlus{inputValue = inp'}] <- source inp,           let p = prettyNames (what inp)               q = prettyNames (what inp') in-          kind inp == kind inp' &&+          isAxiom (kind inp) == isAxiom (kind inp') &&           -- I have NO idea why this doesn't work without show here :(-          show p == show q &&-          (isJust (ident inp) || not (isJust (ident inp'))) = -- don't lose an ident-            annot inp { source = source inp' }+          show p == show q =+          annot inp { source = source inp', ident = ident inp `mplus` ident inp' }     annot inp = do       mn <- findNumber inp       case mn of