packages feed

jukebox 0.2.14 → 0.2.15

raw patch · 10 files changed

+209/−67 lines, 10 files

Files

jukebox.cabal view
@@ -1,5 +1,5 @@ Name: jukebox-Version: 0.2.14+Version: 0.2.15 Cabal-version: >= 1.8 Build-type: Simple Author: Nick Smallbone
src/Jukebox/Clausify.hs view
@@ -35,18 +35,21 @@     do return (toCNF (reverse theory) (reverse obligs))      clausifyInputs theory obligs (inp:inps) | kind inp == Axiom =-    do cs <- clausForm (tag inp) (what inp)+    do cs <- clausForm inp        clausifyInputs (cs ++ theory) obligs inps    clausifyInputs theory obligs (inp:inps) | kind inp `elem` [Conjecture, Question] =-    do clausifyObligs theory obligs (tag inp) (split' (what inp)) inps+    do clausifyObligs theory obligs inp (split' (what inp)) inps    clausifyObligs theory obligs _ [] inps =     do clausifyInputs theory obligs inps   -  clausifyObligs theory obligs s (a:as) inps =-    do cs <- clausForm s (nt a)-       clausifyObligs theory (cs:obligs) s as inps+  clausifyObligs theory obligs inp (a:as) inps =+    do cs <-+         clausForm inp {+           what = nt a,+           source = Inference "negate_conjecture" "cth" [inp] }+       clausifyObligs theory (cs:obligs) inp as inps    split' a | splitting flags = if null split_a then [true] else split_a     where split_a = split a@@ -99,18 +102,19 @@ ---------------------------------------------------------------------- -- core clausification algorithm -clausForm :: String -> Form -> M [Input Clause]-clausForm s p =-  withName s $-    do miniscoped      <- miniscope . check . simplify         . check $ p+clausForm :: Input Form -> M [Input Clause]+clausForm inp =+  withName (tag inp) $+    do miniscoped      <- miniscope . check . simplify         . check $ what inp        noEquivPs       <- removeEquiv                          . check $ miniscoped        noExistsPs      <- mapM removeExists                    . check $ noEquivPs        noExpensiveOrPs <- fmap concat . mapM removeExpensiveOr . check $ noExistsPs        noForAllPs      <- lift . mapM uniqueNames              . check $ noExpensiveOrPs-       let !cnf_        = concatMap cnf                        . check $ noForAllPs+       let !thm         = Input "skolemised" Axiom (Inference "clausify" "esa" [inp]) (And noForAllPs)+           !cnf_        = concatMap cnf                        . check $ noForAllPs            !simp        = simplifyCNF                          . check $ cnf_            cs           = fmap clause                                  $ simp-           inps         = [ Input (s ++ i) Axiom c+           inps         = [ Input (tag inp ++ i) Axiom (Inference "clausify" "thm" [thm]) c                           | (c, i) <- zip cs ("":                                         [ '_':show i | i <- [1..] ]) ]        return $! force . check                                         $ inps
src/Jukebox/Form.hs view
@@ -167,9 +167,11 @@     -- Just exists so that parsing followed by pretty-printing is     -- somewhat lossless; the simplify function will get rid of it   | Connective Connective Form Form+  deriving (Eq, Ord)  -- Miscellaneous connectives that exist in TPTP data Connective = Implies | Follows | Xor | Nor | Nand+  deriving (Eq, Ord)  connective :: Connective -> Form -> Form -> Form connective Implies t u = nt t \/ u@@ -179,6 +181,7 @@ connective Nand t u = nt (t /\ u)  data Bind a = Bind (Set Variable) a+  deriving (Eq, Ord)  true, false :: Form true = And []@@ -290,6 +293,15 @@ toLiterals :: Clause -> [Literal] toLiterals (Clause (Bind _ ls)) = ls +toClause :: Form -> Maybe Clause+toClause (ForAll (Bind _ f)) = toClause f+toClause f = clause <$> cl f+  where+    cl (Or fs) = concat <$> mapM cl fs+    cl (Literal l) = Just [l]+    cl (Not (Literal l)) = Just [neg l]+    cl _ = Nothing+ ---------------------------------------------------------------------- -- Problems @@ -308,10 +320,16 @@ data NoAnswerReason = GaveUp | Timeout deriving (Eq, Ord, Show)  data Input a = Input-  { tag ::  Tag,-    kind :: Kind,-    what :: a }+  { tag    :: Tag,+    kind   :: Kind,+    source :: InputSource,+    what   :: a } +data InputSource =+    Unknown+  | FromFile String Int+  | Inference String String [Input Form]+ type Problem a = [Input a]  instance Functor Input where@@ -404,7 +422,7 @@   rep' (x:xs) = Binary (:) x xs  instance Symbolic a => Unpack (Input a) where-  rep' (Input tag kind what) = Unary (Input tag kind) what+  rep' (Input tag kind info what) = Unary (Input tag kind info) what  instance Unpack CNF where   rep' (CNF ax conj s1 s2) =@@ -543,6 +561,19 @@ functions = usort . termsAndBinders term mempty where   term (f :@: _) = return f   term _ = mempty++funOcc :: Symbolic a => Function -> a -> Int+funOcc f x = getSum (occ x)+  where+    occ :: Symbolic a => a -> Sum Int+    occ x = collect occ x `mappend` occ1 x++    occ1 :: Symbolic a => a -> Sum Int+    occ1 x+      | Term <- typeOf x,+        g :@: _ <- x,+        f == g = Sum 1+      | otherwise = mempty  isFof :: Symbolic a => a -> Bool isFof f = length (types' f) <= 1
src/Jukebox/GuessModel.hs view
@@ -57,8 +57,8 @@   let withExpansive f func = f func (base (name func) `elem` expansive) answer   (constructors, prelude) <- universe univ i   program <- fmap concat (mapM (withExpansive (function constructors)) (functions forms))-  return (map (Input "adt" Axiom) prelude ++-          map (Input "program" Axiom) program +++  return (map (Input "adt" Axiom Unknown) prelude +++          map (Input "program" Axiom Unknown) program ++           forms)  ind :: Symbolic a => a -> Type
src/Jukebox/Monotonox/ToFOF.hs view
@@ -25,7 +25,7 @@   }  guard :: Scheme1 -> (Type -> Bool) -> Input Form -> Input Form-guard scheme mono (Input t k f) = Input t k (aux (pos k) f)+guard scheme mono (Input t k info f) = Input t k info (aux (pos k) f)   where aux pos (ForAll (Bind vs f))           | pos = forAll scheme (Bind vs (aux pos f))           | otherwise = Not (exists scheme (Bind vs (Not (aux pos f))))@@ -65,18 +65,25 @@         map (simplify . ForAll . bind) . split . simplify . foldr (/\) true $           funcAxioms ++ typeAxioms   return $-    [ Input ("types" ++ show i) Axiom axiom | (axiom, i) <- zip axioms [1..] ] +++    [ Input ("types" ++ show i) Axiom (Inference "type_axiom" "esa" []) axiom | (axiom, i) <- zip axioms [1..] ] ++     map (guard scheme1' mono') inps  translate scheme mono f =   let f' =         Form.run f $ \inps -> do-          forM inps $ \(Input tag kind f) -> do+          forM inps $ \inp@(Input tag kind _ f) -> do             let prepare f = fmap (foldr (/\) true) (run (withName tag (removeEquiv (simplify f))))-            fmap (Input tag kind) $-              case kind of-                Axiom -> prepare f-                Conjecture -> fmap notInwards (prepare (nt f))+            case kind of+              Axiom ->+                fmap (Input tag kind (Inference "type_encoding" "esa" [inp])) $+                  prepare f+              Conjecture ->+                let+                  neg_inp =+                    Input tag Axiom+                      (Inference "negate_conjecture" "cth" [inp]) (nt f) in+                fmap (Input tag kind (Inference "type_encoding" "esa" [neg_inp])) $+                fmap notInwards (prepare (nt f))       typeI = Type (name "$i") (Finite 0) Infinite       trType O = O       trType ty = typeI
src/Jukebox/Provers/E.hs view
@@ -88,7 +88,7 @@           , suffix == suffix' ]         parse xs =           let toks = scan xs-          in case run_ parser (UserState initialState toks) of+          in case run_ parser (UserState (initialState Nothing) toks) of             Ok _ ts -> ts             _ -> error "runE: couldn't parse result from E"         parser =
src/Jukebox/TPTP/Parse/Core.hs view
@@ -31,7 +31,8 @@ -- The parser monad  data ParseState =-  MkState ![Input Form]            -- problem being constructed, inputs are in reverse order+  MkState (Maybe String)           -- filename+          ![Input Form]            -- problem being constructed, inputs are in reverse order           !(Map String Type)       -- types in scope           !(Map String [Function]) -- functions in scope           !(Map String Variable)   -- variables in scope, for CNF@@ -43,9 +44,9 @@ data IncludeStatement = Include String (Maybe [Tag]) deriving Show  -- The initial parser state.-initialState :: ParseState-initialState =-  initialStateFrom []+initialState :: Maybe String -> ParseState+initialState mfile =+  initialStateFrom mfile []     (Map.fromList [(show (name ty), ty) | ty <- [int, rat, real]])     (Map.fromList        [ (fun,@@ -77,8 +78,8 @@        fun ["$to_rat"]  (\ty -> FunType [ty] rat) ++        fun ["$to_real"] (\ty -> FunType [ty] real) -initialStateFrom :: [Name] -> Map String Type -> Map String [Function] -> ParseState-initialStateFrom xs tys fs = MkState [] tys fs Map.empty n+initialStateFrom :: Maybe String -> [Name] -> Map String Type -> Map String [Function] -> ParseState+initialStateFrom mfile xs tys fs = MkState mfile [] tys fs Map.empty n   where     n = maximum (0:[succ m | Unique m _ _ <- xs]) @@ -117,7 +118,7 @@   Location file (fromIntegral row) (fromIntegral col)  parseProblem :: FilePath -> String -> ParseResult [Input Form]-parseProblem name contents = parseProblemFrom initialState name contents+parseProblem name contents = parseProblemFrom (initialState (Just name)) name contents  parseProblemFrom :: ParseState -> FilePath -> String -> ParseResult [Input Form] parseProblemFrom state name contents =@@ -155,11 +156,11 @@     merge (Just xs) (Just ys) = Just (xs `intersect` ys)      finalise :: ParseState -> Problem Form-    finalise (MkState p _ _ _ _) = check (reverse p)+    finalise (MkState _ p _ _ _ _) = check (reverse p)  -- Wee function for testing. testParser :: Parser a -> String -> Either [String] a-testParser p s = snd (run (const []) p (UserState initialState (scan s)))+testParser p s = snd (run (const []) p (UserState (initialState Nothing) (scan s)))  -- Primitive parsers. @@ -250,17 +251,25 @@  -- A TPTP kind. kind :: Parser (Tag -> Form -> Input Form)-kind = axiom Axiom <|> axiom Hypothesis <|> axiom Definition <|>-       axiom Assumption <|> axiom Lemma <|> axiom Theorem <|>-       general Conjecture Form.Conjecture <|>-       general NegatedConjecture Form.Axiom <|>-       general Question Form.Question-  where axiom t = general t Form.Axiom-        general k kind = keyword k >> return (mk kind)-        mk kind tag form =-          Input { Form.tag = tag,-                  Form.kind = kind,-                  Form.what = form }+kind = do+  MkState mfile _ _ _ _ _ <- getState+  UserState _ (At (L.Pos n _) _) <- getPosition+  let+    axiom t = general t Form.Axiom+    general k kind = keyword k >> return (mk kind)+    mk kind tag form =+      Input { Form.tag = tag,+              Form.kind = kind,+              Form.what = form,+              Form.source =+                case mfile of+                  Nothing -> Form.Unknown+                  Just file -> FromFile file (fromIntegral n) }+  axiom Axiom <|> axiom Hypothesis <|> axiom Definition <|>+    axiom Assumption <|> axiom Lemma <|> axiom Theorem <|>+    general Conjecture Form.Conjecture <|>+    general NegatedConjecture Form.Axiom <|>+    general Question Form.Question  -- A formula name. tag :: Parser Tag@@ -282,8 +291,8 @@  newFormula :: Input Form -> Parser () newFormula input = do-  MkState p t f v n <- getState-  putState (MkState (input:p) t f v n)+  MkState mfile p t f v n <- getState+  putState (MkState mfile (input:p) t f v n)    newFunction :: String -> FunType -> Parser Function newFunction name ty = do@@ -325,22 +334,22 @@ {-# INLINE lookupType #-} lookupType :: String -> Parser Type lookupType xs = do-  MkState p t f v n <- getState+  MkState mfile p t f v n <- getState   case Map.lookup xs t of     Nothing -> do       let ty = Type (name xs) Infinite Infinite-      putState (MkState p (Map.insert xs ty t) f v n)+      putState (MkState mfile p (Map.insert xs ty t) f v n)       return ty     Just ty -> return ty  {-# INLINE lookupFunction #-} lookupFunction :: FunType -> String -> Parser [Name ::: FunType] lookupFunction def x = do-  MkState p t f v n <- getState+  MkState mfile p t f v n <- getState   case Map.lookup x f of     Nothing -> do       let decl = name x ::: def-      putState (MkState p t (Map.insert x [decl] f) v n)+      putState (MkState mfile p t (Map.insert x [decl] f) v n)       return [decl]     Just fs -> return fs @@ -352,10 +361,10 @@  cnf, tff, fof :: Parser Form cnf = do-  MkState p t f _ n <- getState-  putState (MkState p t f Map.empty n)+  MkState mfile p t f _ n <- getState+  putState (MkState mfile p t f Map.empty n)   form <- formula NoQuantification __-  MkState _ _ _ vs _ <- getState+  MkState _ _ _ _ vs _ <- getState   return (ForAll (Bind (Set.fromList (Map.elems vs)) form)) tff = formula Typed Map.empty fof = formula Untyped Map.empty@@ -424,12 +433,12 @@   {-# INLINE var #-}   var NoQuantification _ = do     x <- variable-    MkState p t f ctx n <- getState+    MkState mfile p t f ctx n <- getState     case Map.lookup x ctx of       Just v -> return (Var v)       Nothing -> do         let v = Unique (n+1) x defaultRenamer ::: individual-        putState (MkState p t f (Map.insert x v ctx) (n+1))+        putState (MkState mfile p t f (Map.insert x v ctx) (n+1))         return (Var v)   var _ ctx = do     x <- variable@@ -562,8 +571,8 @@                Untyped ->                  fatalError "Used a typed quantification in an untyped formula" };              type_ } <|> return individual-  MkState p t f v n <- getState-  putState (MkState p t f v (n+1))+  MkState mfile p t f v n <- getState+  putState (MkState mfile p t f v (n+1))   return (Unique n x defaultRenamer ::: ty)  -- Parse a type
src/Jukebox/TPTP/ParseSnippet.hs view
@@ -21,8 +21,8 @@ form :: Symbolic a => Parser a -> [(String, Type)] -> [(String, Function)] -> String -> a form parser types funs0 str =   case run_ (parser <* eof)-            (UserState (MkState [] (Map.delete "$i" (Map.fromList types)) (Map.fromList funs) Map.empty 0) (scan str)) of-    Ok (UserState (MkState _ types' funs' _ _) (At _ (Cons Eof _))) res+            (UserState (MkState Nothing [] (Map.delete "$i" (Map.fromList types)) (Map.fromList funs) Map.empty 0) (scan str)) of+    Ok (UserState (MkState _ _ types' funs' _ _) (At _ (Cons Eof _))) res       | Map.insert "$i" individual (Map.fromList types) /=         Map.insert "$i" individual types' ->         error $ "ParseSnippet: type implicitly defined: " ++
src/Jukebox/TPTP/Parsec.hs view
@@ -173,3 +173,7 @@ {-# INLINE putState #-} putState :: state -> Parsec (UserState state a) () putState state = Parsec (\ok err UserState{userStream = stream} exp -> ok () err (UserState state stream) exp)++{-# INLINE getPosition #-}+getPosition :: Stream a b => Parsec a (Position a)+getPosition = Parsec (\ok err inp exp -> ok (position inp) err inp exp)
src/Jukebox/TPTP/Print.hs view
@@ -1,10 +1,11 @@ -- Pretty-printing of formulae. WARNING: icky code inside!-{-# LANGUAGE FlexibleContexts, TypeSynonymInstances, TypeOperators, FlexibleInstances, CPP, GADTs #-}-module Jukebox.TPTP.Print(prettyShow, prettyNames, showClauses, pPrintClauses, showProblem, pPrintProblem)+{-# LANGUAGE FlexibleContexts, TypeSynonymInstances, TypeOperators, FlexibleInstances, CPP, GADTs, PatternGuards #-}+module Jukebox.TPTP.Print(prettyShow, prettyNames, showClauses, pPrintClauses, showProblem, pPrintProblem, pPrintProof)        where  #include "errors.h" import Data.Char+import Data.Maybe import Text.PrettyPrint.HughesPJ import qualified Jukebox.TPTP.Lexer as L import Jukebox.Form@@ -33,6 +34,92 @@   where     prob = prettyNames prob0 +-- Print a problem together with all source/derivation information.+pPrintProof :: Problem Form -> Doc+pPrintProof prob =+  pPrintAnnotProof (reverse (annot 1 Set.empty Map.empty (reverse prob)))+  where+    fun f [] = text f+    fun f xs = text f <> parens (fsep (punctuate comma xs))+    list = brackets . fsep . punctuate comma++    clause n = "c" ++ show n++    info inp = (kind inp, what inp)++    -- We maintain: the set of formulas printed so far,+    -- the set of formulas which have been given a clause number so far,+    -- and the highest number given so far.+    -- The clauses come out in reverse dependency order.+    annot :: Int -> Set (Kind, Form) -> Map (Kind, Form) Int -> [Input Form] -> [(Input Form, (String, [Doc]))]+    annot _ _ _ [] = []+    annot m seen named (inp:inps)+        -- Already processed this formula+      | Set.member (kind inp, what inp) seen =+          annot m seen named inps+        -- Formula is identical to its parent+      | Inference _ _ [inp'] <- source inp,+        let [p, q] = prettyNames [what inp, what inp'] in+        kind inp == kind inp' &&+        -- I have NO idea why this doesn't work without show here :(+        show p == show q =+          annot m seen named (inp { source = source inp' }:inps)+      | otherwise =+        case Map.lookup (info inp) named of+          Nothing ->+            -- Give the formula a name+            annot (m+1) seen (Map.insert (info inp) m named) (inp:inps)+          Just n ->+            -- A new formula - print it out+            let+              (k, m', named', new, stuff) =+                case source inp of+                  Unknown ->+                    ("plain", m, named, [], [])+                  FromFile file _ ->+                    (show (kind inp), m, named, [],+                     [fun "file" [text (escapeAtom file), text (escapeAtom (tag inp))]])+                  Inference name status parents ->+                    -- Give any unnamed parents a name+                    let+                      unnamed = [inp | inp <- parents, not (info inp `Map.member` named)]+                      named' =+                        named `Map.union`+                        Map.fromList (zip (map info parents) [m..])+                    in+                      ("plain", m+length unnamed, named', parents,+                       [fun "inference" [+                         text name, list [fun "status" [text status]],+                         list [text (clause (fromJust (Map.lookup (info inp) named'))) | inp <- parents]]])+            in+              (inp { tag = clause n }, (k, stuff)):+              annot m' (Set.insert (info inp) seen) named' (new++inps)++pPrintAnnotProof :: [(Input Form, (String, [Doc]))] -> Doc+pPrintAnnotProof annots0 =+  vcat $+    [ vcat (pPrintDecls inps) | not (isReallyFof inps) ] +++    [ pPrintClause (family x) (tag inp) k (pp x:rest)+    | (inp, (k, rest)) <- annots,+      let x = what inp ]+  where+    inps0 = map fst annots0+    inps = prettyNames inps0+    annots = zip inps (map snd annots0)++    family x+      | isReallyFof x && isJust (toClause x) = "cnf"+      | isReallyFof x = "fof"+      | otherwise = "tff"++    pp x+      | isReallyFof x =+        case toClause x of+          Nothing -> pPrintFof 0 x+          Just cl -> pPrint cl+      | otherwise =+        pPrintTff 0 x+ showProblem :: Problem Form -> String showProblem = show . pPrintProblem @@ -57,7 +144,7 @@     funcDecl (f ::: ty) = typeClause f (pPrint ty)     typeClause name ty =       pPrintClause "tff" "type" "type"-        (text (escapeAtom (show name)) <> colon <+> ty)+        [text (escapeAtom (show name)) <> colon <+> ty]  instance Pretty a => Pretty (Input a) where   pPrint = pPrintInput "tff" pPrint@@ -66,11 +153,11 @@  pPrintInput :: String -> (a -> Doc) -> Input a -> Doc pPrintInput family pp i =-  pPrintClause family (tag i) (show (kind i)) (pp (what i))+  pPrintClause family (tag i) (show (kind i)) [pp (what i)] -pPrintClause :: String -> String -> String -> Doc -> Doc+pPrintClause :: String -> String -> String -> [Doc] -> Doc pPrintClause family name kind rest =-  text family <> parens (sep [text (escapeAtom name) <> comma <+> text kind <> comma, rest]) <> text "."+  text family <> parens (sep (punctuate comma ([text (escapeAtom name), text kind] ++ rest))) <> text "."  instance Pretty Clause where   pPrint (Clause (Bind _ ts)) =