jukebox 0.5.3 → 0.5.4
raw patch · 5 files changed
+104/−45 lines, 5 files
Files
- jukebox.cabal +1/−1
- src/Jukebox/Form.hs +67/−8
- src/Jukebox/TPTP/Print.hs +30/−30
- src/Jukebox/Tools/Clausify.hs +3/−3
- src/Jukebox/Tools/EncodeTypes.hs +3/−3
jukebox.cabal view
@@ -1,5 +1,5 @@ Name: jukebox-Version: 0.5.3+Version: 0.5.4 Cabal-version: >= 1.10 Build-type: Simple Author: Nick Smallbone
src/Jukebox/Form.hs view
@@ -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) ->
src/Jukebox/TPTP/Print.hs view
@@ -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 =
src/Jukebox/Tools/Clausify.hs view
@@ -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
src/Jukebox/Tools/EncodeTypes.hs view
@@ -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