jukebox 0.5.12 → 0.5.13

raw patch · 5 files changed

+15/−8 lines, 5 filesPVP: major bump suggested

API removals or changes: PVP suggests a major version bump

API changes (from Hackage documentation)

+ Jukebox.Form: derivedClause :: String -> String -> Input Form -> a -> Input a

- Jukebox.Form: FromFile :: String -> Int -> InputSource

+ Jukebox.Form: FromFile :: String -> String -> Int -> InputSource

jukebox.cabal view

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

src/Jukebox/Form.hs view

@@ -313,6 +313,8 @@ toLiterals (Clause (Bind _ ls)) = ls  toClause :: Form -> Maybe Clause+toClause (And [c]) = toClause c+toClause (Or [c]) = toClause c toClause (ForAll (Bind _ f)) = toClause f toClause f = clause <$> cl f   where@@ -389,7 +391,7 @@  data InputSource =     Unknown-  | FromFile String Int+  | FromFile String String Int   | Inference (Maybe Kind) String String [InputPlus Form]  inference :: String -> String -> [Input Form] -> InputSource@@ -397,6 +399,10 @@  inference' :: Maybe Kind -> String -> String -> [Input Form] -> InputSource inference' role name status parents = Inference role name status (map inputPlus parents)++derivedClause :: String -> String -> Input Form -> a -> Input a+derivedClause name status parent clause =+  Input Nothing (tag parent) (kind parent) (inference name status [parent]) clause  data InputPlus a = InputPlus   { inputNames     :: [Name],

src/Jukebox/TPTP/Parse/Core.hs view

@@ -275,7 +275,7 @@               Form.source =                 case mfile of                   Nothing -> Form.Unknown-                  Just file -> FromFile file (fromIntegral n) }+                  Just file -> FromFile file tag (fromIntegral n) }   axiom L.Axiom Axiom <|>     axiom L.Hypothesis Hypothesis <|>     axiom L.Definition Definition <|>

src/Jukebox/TPTP/Print.hs view

@@ -108,9 +108,9 @@            case source inp of             Unknown -> ret "plain" []-            FromFile file _ ->+            FromFile file tag _ ->               ret (show (kind inp))-                [fun "file" [text (escapeAtom file), text (escapeAtom (tag inp))]]+                [fun "file" [text (escapeAtom file), text (escapeAtom tag)]]             Inference mkind name status parents -> do               -- Process all parents first               nums <- mapM (annot . inputValue) parents

src/Jukebox/Tools/HornToUnit.hs view

@@ -127,7 +127,8 @@       elim inp         | (null poss && length negs /= 1 && not (allowConjunctiveConjectures flags)) ||           (not (null poss) && length negs > 1 && multi flags) =-          inp{what = clause (Neg ((tuple tys :@: ts) :=: (tuple tys :@: us)):poss)}+          derivedClause "tupling" "esa" (fmap toForm inp) $+            clause (Neg ((tuple tys :@: ts) :=: (tuple tys :@: us)):poss)         where           (poss, negs) = partition pos (toLiterals (what inp))           ts = [t | l <- negs, let Neg (t :=: _) = l]@@ -194,7 +195,7 @@         ([], _) -> return [c]         ([Pos l], ls) -> do           l <- foldM (encode (tag c)) l ls-          return [c { what = clause [Pos l] }]+          return [derivedClause "ifeq_intro" "esa" (fmap toForm c) (clause [Pos l])]         _ ->           if dropNonHorn flags then             return []@@ -282,7 +283,7 @@         ident = Nothing,         tag = tag,         kind = Ax Axiom,-        source = Unknown,+        source = inference "ifeq_elim" "esa" [],         what = clause [Pos l] }      (ifeqName, freshName, passiveName, xvar, yvar, zvar) = run_ prob $ do