jukebox 0.5.11 → 0.5.12

raw patch · 4 files changed

+14/−11 lines, 4 filesPVP: major bump suggested

API removals or changes: PVP suggests a major version bump

API changes (from Hackage documentation)

+ Jukebox.Form: inference' :: Maybe Kind -> String -> String -> [Input Form] -> InputSource

- Jukebox.Form: Inference :: String -> String -> [InputPlus Form] -> InputSource

+ Jukebox.Form: Inference :: Maybe Kind -> String -> String -> [InputPlus Form] -> InputSource

jukebox.cabal view

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

src/Jukebox/Form.hs view

@@ -390,11 +390,14 @@ data InputSource =     Unknown   | FromFile String Int-  | Inference String String [InputPlus Form]+  | Inference (Maybe Kind) String String [InputPlus Form]  inference :: String -> String -> [Input Form] -> InputSource-inference name status parents = Inference name status (map inputPlus parents)+inference = inference' Nothing +inference' :: Maybe Kind -> String -> String -> [Input Form] -> InputSource+inference' role name status parents = Inference role name status (map inputPlus parents)+ data InputPlus a = InputPlus   { inputNames     :: [Name],     inputFunctions :: [Function],@@ -633,7 +636,7 @@   inp (Input ident _ _ source _) =     maybeToList ident ++     case source of-      Inference _ _ inps ->+      Inference _ _ _ inps ->         concatMap inputNames inps       _ -> [] @@ -676,7 +679,7 @@   inp :: Symbolic a => Input a -> [Function]   inp (Input _ _ _ source _) =     case source of-      Inference _ _ inps ->+      Inference _ _ _ inps ->         concatMap inputFunctions inps       _ -> [] @@ -806,8 +809,8 @@       where         source' =           case source of-            Inference inf status forms ->-              Inference inf status (map inputPlus forms)+            Inference mkind inf status forms ->+              Inference mkind inf status (map inputPlus forms)             _ -> source      inputPlus  :: InputPlus Form -> InputPlus Form

src/Jukebox/TPTP/Print.hs view

@@ -86,7 +86,7 @@     annot :: Input Form -> PrintProofState Int     annot inp       -- Formula is identical to its parent-      | Inference _ _ [InputPlus{inputValue = inp'}] <- source inp,+      | Inference Nothing _ _ [InputPlus{inputValue = inp'}] <- source inp,           let p = prettyNames (what inp)               q = prettyNames (what inp') in           isAxiom (kind inp) == isAxiom (kind inp') &&@@ -111,10 +111,10 @@             FromFile file _ ->               ret (show (kind inp))                 [fun "file" [text (escapeAtom file), text (escapeAtom (tag inp))]]-            Inference name status parents -> do+            Inference mkind name status parents -> do               -- Process all parents first               nums <- mapM (annot . inputValue) parents-              ret "plain"+              ret (case mkind of { Nothing -> "plain"; Just kind -> show kind })                 [fun "inference" [                   text name, list [fun "status" [text status]],                   list [text (clause n) | n <- nums]]]

src/Jukebox/Tools/Clausify.hs view

@@ -63,7 +63,7 @@     do cs <-          clausForm NegatedConjecture inp {            what = nt a,-           source = inference "negate_conjecture" "cth" [inp] }+           source = inference' (Just (Ax NegatedConjecture)) "negate_conjecture" "cth" [inp] }        clausifyObligs theory (cs:obligs) inp as inps    split' a | splitting flags = if null split_a then [true] else split_a