packages feed

jukebox 0.2.15 → 0.2.16

raw patch · 8 files changed

+73/−72 lines, 8 files

Files

jukebox.cabal view
@@ -1,5 +1,5 @@ Name: jukebox-Version: 0.2.15+Version: 0.2.16 Cabal-version: >= 1.8 Build-type: Simple Author: Nick Smallbone
src/Jukebox/Clausify.hs view
@@ -1,4 +1,4 @@-{-# LANGUAGE TypeOperators, BangPatterns, CPP #-}+{-# LANGUAGE TypeOperators, BangPatterns, CPP, PatternGuards #-} module Jukebox.Clausify where  import Jukebox.Form hiding (run)@@ -34,8 +34,9 @@   clausifyInputs theory obligs [] =     do return (toCNF (reverse theory) (reverse obligs))   -  clausifyInputs theory obligs (inp:inps) | kind inp == Axiom =-    do cs <- clausForm inp+  clausifyInputs theory obligs (inp:inps)+    | Axiom axiom <- kind inp =+    do cs <- clausForm axiom inp        clausifyInputs (cs ++ theory) obligs inps    clausifyInputs theory obligs (inp:inps) | kind inp `elem` [Conjecture, Question] =@@ -46,7 +47,7 @@      clausifyObligs theory obligs inp (a:as) inps =     do cs <--         clausForm inp {+         clausForm "negated_conjecture" inp {            what = nt a,            source = Inference "negate_conjecture" "cth" [inp] }        clausifyObligs theory (cs:obligs) inp as inps@@ -102,19 +103,19 @@ ---------------------------------------------------------------------- -- core clausification algorithm -clausForm :: Input Form -> M [Input Clause]-clausForm inp =+clausForm :: String -> Input Form -> M [Input Clause]+clausForm kind 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 !thm         = Input "skolemised" Axiom (Inference "clausify" "esa" [inp]) (And noForAllPs)+       let !thm         = Input "skolemised" (Axiom kind) (Inference "clausify" "esa" [inp]) (And noForAllPs)            !cnf_        = concatMap cnf                        . check $ noForAllPs            !simp        = simplifyCNF                          . check $ cnf_            cs           = fmap clause                                  $ simp-           inps         = [ Input (tag inp ++ i) Axiom (Inference "clausify" "thm" [thm]) c+           inps         = [ Input (tag inp ++ i) (Axiom kind) (Inference "clausify" "thm" [thm]) c                           | (c, i) <- zip cs ("":                                         [ '_':show i | i <- [1..] ]) ]        return $! force . check                                         $ inps
src/Jukebox/Form.hs view
@@ -307,7 +307,7 @@  type Tag = String -data Kind = Axiom | Conjecture | Question deriving (Eq, Ord)+data Kind = Axiom String | Conjecture | Question deriving (Eq, Ord)  data Answer = Satisfiable | Unsatisfiable | NoAnswer NoAnswerReason   deriving (Eq, Ord)
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 Unknown) prelude ++-          map (Input "program" Axiom Unknown) program +++  return (map (Input "adt" (Axiom "axiom") Unknown) prelude +++          map (Input "program" (Axiom "axiom") Unknown) program ++           forms)  ind :: Symbolic a => a -> Type
src/Jukebox/Monotonox/ToFOF.hs view
@@ -28,10 +28,10 @@ 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))))+          | otherwise = notInwards (exists scheme (Bind vs (Not (aux pos f))))         aux pos (Exists (Bind vs f))           | pos = exists scheme (Bind vs (aux pos f))-          | otherwise = Not (forAll scheme (Bind vs (Not (aux pos f))))+          | otherwise = notInwards (forAll scheme (Bind vs (Not (aux pos f))))         aux _pos (Literal (Pos (t :=: u)))           | not (mono (typ t)) = equals scheme t u         aux _pos (Literal (Neg (t :=: u)))@@ -42,7 +42,7 @@         aux pos (Or fs) = Or (fmap (aux pos) fs)         aux _pos (Equiv _ _) = error "ToFOF.guard: equiv should have been eliminated"         aux _pos (Connective _ _ _) = error "ToFOF.guard: connective should have been eliminated"-        pos Axiom = True+        pos Axiom{} = True         pos Conjecture = False  translate, translate1 :: Scheme -> (Type -> Bool) -> Problem Form -> Problem Form@@ -65,7 +65,7 @@         map (simplify . ForAll . bind) . split . simplify . foldr (/\) true $           funcAxioms ++ typeAxioms   return $-    [ Input ("types" ++ show i) Axiom (Inference "type_axiom" "esa" []) axiom | (axiom, i) <- zip axioms [1..] ] +++    [ Input ("types" ++ show i) (Axiom "axiom") (Inference "type_axiom" "esa" []) axiom | (axiom, i) <- zip axioms [1..] ] ++     map (guard scheme1' mono') inps  translate scheme mono f =@@ -74,16 +74,12 @@           forM inps $ \inp@(Input tag kind _ f) -> do             let prepare f = fmap (foldr (/\) true) (run (withName tag (removeEquiv (simplify f))))             case kind of-              Axiom ->+              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))+                fmap (Input tag kind (Inference "type_encoding" "esa" [inp])) $+                fmap notInwards $ prepare $ nt f       typeI = Type (name "$i") (Finite 0) Infinite       trType O = O       trType ty = typeI
src/Jukebox/SMTLIB.hs view
@@ -183,7 +183,7 @@ pPrintType ty = pPrintName (name ty)  pPrintInput :: Input Form -> Doc-pPrintInput Input{kind = Axiom, what = form} =+pPrintInput Input{kind = Axiom _, what = form} =   sexp ["assert", pPrintForm form] pPrintInput Input{kind = Conjecture, what = form} =   sexp ["assert", sexp ["not", pPrintForm form]]
src/Jukebox/TPTP/Parse/Core.hs view
@@ -255,7 +255,7 @@   MkState mfile _ _ _ _ _ <- getState   UserState _ (At (L.Pos n _) _) <- getPosition   let-    axiom t = general t Form.Axiom+    axiom t = general t (Form.Axiom (show t))     general k kind = keyword k >> return (mk kind)     mk kind tag form =       Input { Form.tag = tag,@@ -267,8 +267,8 @@                   Just file -> FromFile file (fromIntegral n) }   axiom Axiom <|> axiom Hypothesis <|> axiom Definition <|>     axiom Assumption <|> axiom Lemma <|> axiom Theorem <|>+    axiom NegatedConjecture <|>     general Conjecture Form.Conjecture <|>-    general NegatedConjecture Form.Axiom <|>     general Question Form.Question  -- A formula name.
src/Jukebox/TPTP/Print.hs view
@@ -16,6 +16,7 @@ import Jukebox.Name import Jukebox.Utils import Text.PrettyPrint.HughesPJClass+import Control.Monad.Trans.State.Strict  pPrintClauses :: Problem Clause -> Doc pPrintClauses prob0@@ -37,7 +38,7 @@ -- 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)))+  pPrintAnnotProof (evalState (concat <$> mapM annot prob) (1, Map.empty))   where     fun f [] = text f     fun f xs = text f <> parens (fsep (punctuate comma xs))@@ -48,53 +49,56 @@     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+    findNumber :: Input Form -> State (Int, Map (Kind, Form) Int) (Maybe Int)+    findNumber inp =+      gets (Map.lookup (info inp) . snd)++    newNumber :: Input Form -> State (Int, Map (Kind, Form) Int) (Maybe Int)+    newNumber inp = do+      (n, map) <- get+      case Map.lookup (info inp) map of+        Nothing -> do+          put (n+1, Map.insert (info inp) n map)+          return (Just n)+        Just _ -> return Nothing++    annot :: Input Form -> State (Int, Map (Kind, Form) Int) [(Input Form, (String, [Doc]))]+    annot inp+      -- 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)+          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 inp { source = source inp' }+      | otherwise = do+          mn <- newNumber inp+          case mn of+            Nothing ->+              -- Already processed this formula+              return []+            Just n -> do+              let+                ret k stuff =+                  return [(inp { tag = clause n }, (k, stuff))] +              case source inp of+                Unknown -> ret "plain" []+                FromFile file _ ->+                  ret (show (kind inp))+                    [fun "file" [text (escapeAtom file), text (escapeAtom (tag inp))]]+                Inference name status parents -> do+                  -- Process all parents first+                  rest <- mapM annot parents+                  nums <- map fromJust <$> mapM findNumber parents++                  fmap (concat rest ++) $+                    ret "plain"+                      [fun "inference" [+                        text name, list [fun "status" [text status]],+                        list [text (clause n) | n <- nums]]]+ pPrintAnnotProof :: [(Input Form, (String, [Doc]))] -> Doc pPrintAnnotProof annots0 =   vcat $@@ -285,7 +289,7 @@       nest 2 (pPrintForm bind 1 f)]  instance Show Kind where-  show Axiom = "axiom"+  show (Axiom kind) = kind   show Conjecture = "conjecture"   show Question = "question"