packages feed

jukebox 0.5.5 → 0.5.6

raw patch · 9 files changed

+71/−51 lines, 9 files

Files

jukebox.cabal view
@@ -1,5 +1,5 @@ Name: jukebox-Version: 0.5.5+Version: 0.5.6 Cabal-version: >= 1.10 Build-type: Simple Author: Nick Smallbone
src/Jukebox/Form.hs view
@@ -16,6 +16,7 @@ import Control.Monad.Trans.Class import Control.Monad.Trans.State.Strict import Data.List+import Data.Maybe import Jukebox.Utils import Data.Typeable(Typeable) import Data.Monoid@@ -374,7 +375,8 @@ answerJustification _ = Nothing  data Input a = Input-  { tag    :: Tag,+  { ident  :: Maybe Name,+    tag    :: Tag,     kind   :: Kind,     source :: InputSource,     what   :: a }@@ -491,7 +493,7 @@   rep' (x:xs) = Binary (:) x xs  instance Symbolic a => Unpack (Input a) where-  rep' (Input tag kind info what) = Unary (Input tag kind info) what+  rep' (Input ident tag kind info what) = Unary (Input ident tag kind info) what  instance Unpack CNF where   rep' (CNF ax conj s1 s2) =@@ -617,7 +619,8 @@   bind (Bind vs _) = map name (Set.toList vs)    inp :: Symbolic a => Input a -> [Name]-  inp (Input _ _ source _) =+  inp (Input ident _ _ source _) =+    maybeToList ident ++     case source of       Inference _ _ inps ->         concatMap inputNames inps@@ -637,7 +640,7 @@   bind (Bind vs _) = map typ (Set.toList vs)    inp :: Symbolic a => Input a -> [Type]-  inp (Input _ _ source _) =+  inp (Input _ _ _ source _) =     case source of       Inference _ _ inps ->         concatMap inputTypes inps@@ -664,7 +667,7 @@   term _ = mempty    inp :: Symbolic a => Input a -> [Function]-  inp (Input _ _ source _) =+  inp (Input _ _ _ source _) =     case source of       Inference _ _ inps ->         concatMap inputFunctions inps@@ -791,8 +794,8 @@     term (Var x) = Var (var x)      input :: Symbolic a => Input a -> Input a-    input (Input name kind source what) =-      Input name kind source' (rename what)+    input (Input id name kind source what) =+      Input (fmap f id) name kind source' (rename what)       where         source' =           case source of
src/Jukebox/Name.hs view
@@ -171,4 +171,7 @@   let idx' = idx+1   when (idx' < 0) $ error "Name.newName: too many names"   put $! idx'-  return $! Unique idx' (intern (base x)) (label x) (renamer x)+  return $! unique x idx'++unique :: Named a => a -> Int64 -> Name+unique x n = Unique n (intern (base x)) (label x) (renamer x)
src/Jukebox/TPTP/Parse/Core.hs view
@@ -268,7 +268,8 @@     axiom t kind = general t (Form.Ax kind)     conjecture t kind = general t (Form.Conj kind)     mk kind tag form =-      Input { Form.tag = tag,+      Input { Form.ident = Nothing,+              Form.tag = tag,               Form.kind = kind,               Form.what = form,               Form.source =
src/Jukebox/TPTP/Print.hs view
@@ -38,58 +38,73 @@   where     prob = prettyNames prob0 +type PrintProofState a = State (Int, Map Name Int, [(Input Form, (String, [Doc]))]) a+ -- Print a problem together with all source/derivation information. pPrintProof :: Problem Form -> Doc pPrintProof prob =-  pPrintAnnotProof (evalState (concat <$> mapM annot prob) (1, Map.empty))+  pPrintAnnotProof (reverse out)   where+    (_, _, out) = execState (mapM_ annot prob) (1, Map.empty, [])+     fun f [] = text f     fun f xs = text f <> parens (hsep (punctuate comma xs))     list = brackets . hsep . punctuate comma      clause n = "c" ++ show n -    info inp = (kind inp, what inp)-     -- We maintain: the set of formulas printed so far,     -- and the highest number given so far.-    findNumber :: Input Form -> State (Int, Map (Kind, Form) Int) (Maybe Int)+    findNumber :: Input Form -> PrintProofState (Maybe Int)     findNumber inp =-      gets (Map.lookup (info inp) . snd)+      case ident inp of+        Nothing -> return Nothing+        Just id -> do+          (_, map, _) <- get+          return (Map.lookup id map) -    newNumber :: Input Form -> State (Int, Map (Kind, Form) Int) (Maybe Int)+    newNumber :: Input Form -> PrintProofState Int     newNumber inp = do-      (n, map) <- get-      case Map.lookup (info inp) map of+      (n, map, out) <- get+      case ident inp of         Nothing -> do-          put (n+1, Map.insert (info inp) n map)-          return (Just n)-        Just _ -> return Nothing+          put (n+1, map, out)+          return n+        Just id ->+          case Map.lookup id map of+            Nothing -> do+              put (n+1, Map.insert id n map, out)+              return n+            Just _ -> error "newNumber: already present" -    annot :: Input Form -> State (Int, Map (Kind, Form) Int) [(Input Form, (String, [Doc]))]+    emit :: Input Form -> String -> [Doc] -> PrintProofState ()+    emit form k xs = do+      (n, map, out) <- get+      put (n, map, (form, (k, xs)):out)++    annot :: Input Form -> PrintProofState Int     annot inp       -- Formula is identical to its parent       | Inference _ _ [InputPlus{inputValue = inp'}] <- source inp,-          let [p, q] = prettyNames [what inp, what inp'] in+          let p = prettyNames (what inp)+              q = prettyNames (what inp') in           kind inp == kind inp' &&           -- I have NO idea why this doesn't work without show here :(-          show p == show q =+          show p == show q &&+          (isJust (ident inp) || not (isJust (ident inp'))) = -- don't lose an ident             annot inp { source = source inp' }     annot inp = do       mn <- findNumber inp       case mn of-        Just _ ->+        Just n -> do           -- Already processed this formula-          return []+          return n         Nothing -> do           let             ret k stuff = do-              res <- newNumber inp-              case res of-                Just n ->-                  return [(inp { tag = clause n }, (k, stuff))]-                Nothing ->-                  return []+              n <- newNumber inp+              emit inp { tag = clause n } k stuff+              return n            case source inp of             Unknown -> ret "plain" []@@ -98,20 +113,17 @@                 [fun "file" [text (escapeAtom file), text (escapeAtom (tag inp))]]             Inference name status parents -> do               -- Process all parents first-              rest <- mapM (annot . inputValue) parents-              nums <- map fromJust <$> mapM (findNumber . inputValue) parents--              fmap (concat rest ++) $-                ret "plain"-                  [fun "inference" [-                    text name, list [fun "status" [text status]],-                    list [text (clause n) | n <- nums]]]+              nums <- mapM (annot . inputValue) parents+              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 $     [ vcat (pPrintDecls "tff" inps) | not (isReallyFof inps) ] ++-    [ pPrintClause (family x) (tag inp) k (pp x:rest)+    [ pPrintClause (family x) (tag inp) k (pp x:rest) <+> text (show (ident inp))     | (inp, (k, rest)) <- annots,       let x = what inp ]   where
src/Jukebox/Tools/Clausify.hs view
@@ -125,11 +125,11 @@        noExistsPs      <- mapM removeExists                    . check $ noEquivPs        noExpensiveOrPs <- fmap concat . mapM removeExpensiveOr . check $ noExistsPs        noForAllPs      <- lift . mapM uniqueNames              . check $ noExpensiveOrPs-       let !thm         = Input "skolemised" (Ax kind) (inference "clausify" "esa" [inp]) (And noForAllPs)+       let !thm         = Input Nothing "skolemised" (Ax 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) (Ax kind) (inference "clausify" "thm" [thm]) c+           inps         = [ Input Nothing (tag inp ++ i) (Ax kind) (inference "clausify" "thm" [thm]) c                           | (c, i) <- zip cs ("":                                         [ '_':show i | i <- [1..] ]) ]        return $! force . check                                         $ inps
src/Jukebox/Tools/EncodeTypes.hs view
@@ -25,7 +25,7 @@   }  guard :: Scheme1 -> (Type -> Bool) -> Input Form -> Input Form-guard scheme mono (Input t k info f) = Input t k info (aux (pos k) f)+guard scheme mono (Input _ t k info f) = Input Nothing t k info (aux (pos k) f)   where aux pos (ForAll (Bind vs f))           | pos = forAll scheme (Bind vs (aux pos f))           | otherwise = notInwards (exists scheme (Bind vs (Not (aux pos f))))@@ -65,20 +65,20 @@         map (simplify . ForAll . bind) . split . simplify . foldr (/\) true $           funcAxioms ++ typeAxioms   return $-    [ Input ("types" ++ show i) (Ax Axiom) (inference "type_axiom" "esa" []) axiom | (axiom, i) <- zip axioms [1..] ] +++    [ Input Nothing ("types" ++ show i) (Ax 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 $ \inp@(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))))             case kind of               Ax{} ->-                fmap (Input tag kind (inference "type_encoding" "esa" [inp])) $+                fmap (Input Nothing tag kind (inference "type_encoding" "esa" [inp])) $                   prepare f               Conj{} ->-                fmap (Input tag kind (inference "type_encoding" "esa" [inp])) $+                fmap (Input Nothing tag kind (inference "type_encoding" "esa" [inp])) $                 fmap notInwards $ prepare $ nt f       trType O = O       trType _ = indType
src/Jukebox/Tools/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" (Ax Axiom) Unknown) prelude ++-          map (Input "program" (Ax Axiom) Unknown) program +++  return (map (Input Nothing "adt" (Ax Axiom) Unknown) prelude +++          map (Input Nothing "program" (Ax Axiom) Unknown) program ++           forms)  ind :: Symbolic a => a -> Type
src/Jukebox/Tools/HornToUnit.hs view
@@ -147,7 +147,7 @@   | null bad = prob   | otherwise =     good ++ map (fmap addConjecture) bad ++-    [Input { tag = "goal", kind = Ax NegatedConjecture, source = Unknown,+    [Input { ident = Nothing, tag = "goal", kind = Ax NegatedConjecture, source = Unknown,              what = clause [Neg (a :=: b)] }]   where     (bad, good) = partition unsuitable prob@@ -279,6 +279,7 @@      toInput (tag, l) =       Input {+        ident = Nothing,         tag = tag,         kind = Ax Axiom,         source = Unknown,