diff --git a/jukebox.cabal b/jukebox.cabal --- a/jukebox.cabal +++ b/jukebox.cabal @@ -1,5 +1,5 @@ Name: jukebox -Version: 0.5.3 +Version: 0.5.4 Cabal-version: >= 1.10 Build-type: Simple Author: Nick Smallbone diff --git a/src/Jukebox/Form.hs b/src/Jukebox/Form.hs --- a/src/Jukebox/Form.hs +++ b/src/Jukebox/Form.hs @@ -383,8 +383,25 @@ data InputSource = Unknown | FromFile String Int - | Inference String String [Input Form] + | Inference String String [InputPlus Form] +inference :: String -> String -> [Input Form] -> InputSource +inference name status parents = Inference name status (map inputPlus parents) + +data InputPlus a = InputPlus + { inputNames :: [Name], + inputFunctions :: [Function], + inputTypes :: [Type], + inputValue :: Input a } + +inputPlus :: Symbolic a => Input a -> InputPlus a +inputPlus x = + InputPlus { + inputNames = names x, + inputFunctions = functions x, + inputTypes = types' x, + inputValue = x } + type Problem a = [Input a] ---------------------------------------------------------------------- @@ -580,23 +597,32 @@ Symbolic a => (Term -> DList b) -> (forall a. Symbolic a => Bind a -> [b]) -> + (forall a. Symbolic a => Input a -> [b]) -> a -> [b] -termsAndBinders term bind = DList.toList . aux where +termsAndBinders term bind inp = DList.toList . aux where aux :: Symbolic c => c -> DList b aux t = collect aux t `mplus` case typeOf t of Term -> term t Bind_ -> DList.fromList (bind t) + Input_ -> DList.fromList (inp t) _ -> mzero names :: Symbolic a => a -> [Name] -names = usort . termsAndBinders term bind where +names = usort . termsAndBinders term bind inp where term t = DList.fromList (allNames t) `mappend` DList.fromList (allNames (typ t)) bind :: Symbolic a => Bind a -> [Name] bind (Bind vs _) = map name (Set.toList vs) + inp :: Symbolic a => Input a -> [Name] + inp (Input _ _ source _) = + case source of + Inference _ _ inps -> + concatMap inputNames inps + _ -> [] + run :: Symbolic a => a -> (a -> NameM b) -> b run x f = runNameM (names x) (f x) @@ -604,21 +630,28 @@ run_ x mx = run x (const mx) types :: Symbolic a => a -> [Type] -types = usort . termsAndBinders term bind where +types = usort . termsAndBinders term bind inp where term t = return (typ t) bind :: Symbolic a => Bind a -> [Type] bind (Bind vs _) = map typ (Set.toList vs) + inp :: Symbolic a => Input a -> [Type] + inp (Input _ _ source _) = + case source of + Inference _ _ inps -> + concatMap inputTypes inps + _ -> [] + types' :: Symbolic a => a -> [Type] types' = filter (/= O) . types terms :: Symbolic a => a -> [Term] -terms = usort . termsAndBinders term mempty where +terms = usort . termsAndBinders term mempty mempty where term t = return t vars :: Symbolic a => a -> [Variable] -vars = usort . termsAndBinders term bind where +vars = usort . termsAndBinders term bind mempty where term (Var x) = return x term _ = mempty @@ -626,10 +659,17 @@ bind (Bind vs _) = Set.toList vs functions :: Symbolic a => a -> [Function] -functions = usort . termsAndBinders term mempty where +functions = usort . termsAndBinders term mempty inp where term (f :@: _) = return f term _ = mempty + inp :: Symbolic a => Input a -> [Function] + inp (Input _ _ source _) = + case source of + Inference _ _ inps -> + concatMap inputFunctions inps + _ -> [] + funOcc :: Symbolic a => Function -> a -> Int funOcc f x = getSum (occ x) where @@ -645,7 +685,7 @@ funsOcc :: Symbolic a => a -> Map Function Int funsOcc = - Map.fromList . map f . group . sort . termsAndBinders term mempty + Map.fromList . map f . group . sort . termsAndBinders term mempty mempty where term (f :@: _) = return f term _ = mempty @@ -742,12 +782,31 @@ case typeOf t of Term -> term t Bind_ -> bind t + Input_ -> input t _ -> recursively rename t bind :: Symbolic a => Bind a -> Bind a bind (Bind vs t) = Bind (Set.map var vs) (rename t) term (f :@: ts) = fun f :@: map term ts 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) + where + source' = + case source of + Inference inf status forms -> + Inference inf status (map inputPlus forms) + _ -> source + + inputPlus :: InputPlus Form -> InputPlus Form + inputPlus inp = + InputPlus { + inputNames = map f (inputNames inp), + inputFunctions = map fun (inputFunctions inp), + inputTypes = map type_ (inputTypes inp), + inputValue = input (inputValue inp) } var = memo $ \(x ::: ty) -> f x ::: type_ ty fun = memo $ \(x ::: FunType args res) -> diff --git a/src/Jukebox/TPTP/Print.hs b/src/Jukebox/TPTP/Print.hs --- a/src/Jukebox/TPTP/Print.hs +++ b/src/Jukebox/TPTP/Print.hs @@ -69,43 +69,43 @@ 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, + | Inference _ _ [InputPlus{inputValue = 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 inp { source = source inp' } - | otherwise = do - mn <- findNumber inp - case mn of - Just _ -> - -- Already processed this formula - return [] - Nothing -> do - let - ret k stuff = do - res <- newNumber inp - case res of - Just n -> - return [(inp { tag = clause n }, (k, stuff))] - Nothing -> - return [] + annot inp = do + mn <- findNumber inp + case mn of + Just _ -> + -- Already processed this formula + return [] + Nothing -> do + let + ret k stuff = do + res <- newNumber inp + case res of + Just n -> + return [(inp { tag = clause n }, (k, stuff))] + Nothing -> + return [] - 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 + 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 . 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]]] + 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 = diff --git a/src/Jukebox/Tools/Clausify.hs b/src/Jukebox/Tools/Clausify.hs --- a/src/Jukebox/Tools/Clausify.hs +++ b/src/Jukebox/Tools/Clausify.hs @@ -63,7 +63,7 @@ do cs <- clausForm NegatedConjecture inp { what = nt a, - source = Inference "negate_conjecture" "cth" [inp] } + 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 @@ -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 "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 (tag inp ++ i) (Ax kind) (inference "clausify" "thm" [thm]) c | (c, i) <- zip cs ("": [ '_':show i | i <- [1..] ]) ] return $! force . check $ inps diff --git a/src/Jukebox/Tools/EncodeTypes.hs b/src/Jukebox/Tools/EncodeTypes.hs --- a/src/Jukebox/Tools/EncodeTypes.hs +++ b/src/Jukebox/Tools/EncodeTypes.hs @@ -65,7 +65,7 @@ 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 ("types" ++ show i) (Ax Axiom) (inference "type_axiom" "esa" []) axiom | (axiom, i) <- zip axioms [1..] ] ++ map (guard scheme1' mono') inps translate scheme mono f = @@ -75,10 +75,10 @@ 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 tag kind (inference "type_encoding" "esa" [inp])) $ prepare f Conj{} -> - fmap (Input tag kind (Inference "type_encoding" "esa" [inp])) $ + fmap (Input tag kind (inference "type_encoding" "esa" [inp])) $ fmap notInwards $ prepare $ nt f trType O = O trType _ = indType