# HG changeset patch # User paulson # Date 1192111171 -7200 # Node ID ff15f76741bd6bad0b7ab7ced28c2932cd207dea # Parent 50959112a4e1018e8ef624af3fec7fe991b30148 rationalized redundant code diff -r 50959112a4e1 -r ff15f76741bd src/HOL/Tools/cnf_funcs.ML --- a/src/HOL/Tools/cnf_funcs.ML Thu Oct 11 15:57:29 2007 +0200 +++ b/src/HOL/Tools/cnf_funcs.ML Thu Oct 11 15:59:31 2007 +0200 @@ -4,6 +4,8 @@ Author: Tjark Weber Copyright 2005-2006 + FIXME: major overlaps with the code in meson.ML + Description: This file contains functions and tactics to transform a formula into Conjunctive Normal Form (CNF). @@ -122,9 +124,6 @@ fun clause_is_trivial c = let - (* Term.term -> Term.term list -> Term.term list *) - fun collect_literals (Const ("op |", _) $ x $ y) ls = collect_literals x (collect_literals y ls) - | collect_literals x ls = x :: ls (* Term.term -> Term.term *) fun dual (Const ("Not", _) $ x) = x | dual x = HOLogic.Not $ x @@ -132,7 +131,7 @@ fun has_duals [] = false | has_duals (x::xs) = (dual x) mem xs orelse has_duals xs in - has_duals (collect_literals c []) + has_duals (HOLogic.disjuncts c) end; (* ------------------------------------------------------------------------- *) diff -r 50959112a4e1 -r ff15f76741bd src/HOL/Tools/metis_tools.ML --- a/src/HOL/Tools/metis_tools.ML Thu Oct 11 15:57:29 2007 +0200 +++ b/src/HOL/Tools/metis_tools.ML Thu Oct 11 15:59:31 2007 +0200 @@ -529,9 +529,11 @@ tfrees = tfrees}; (* Function to generate metis clauses, including comb and type clauses *) - fun build_map mode thy ctxt cls ths = - let val isFO = (mode = ResAtp.Fol) orelse - (mode <> ResAtp.Hol andalso ResAtp.is_fol_thms (cls @ ths)) + fun build_map mode ctxt cls ths = + let val thy = ProofContext.theory_of ctxt + val all_thms_FO = forall (Meson.is_fol_term thy o prop_of) + val isFO = (mode = ResAtp.Fol) orelse + (mode <> ResAtp.Hol andalso all_thms_FO (cls @ ths)) val lmap0 = foldl (add_thm true ctxt) {isFO = isFO, axioms = [], tfrees = init_tfrees ctxt} cls val lmap = foldl (add_thm false ctxt) (add_tfrees lmap0) ths @@ -559,8 +561,7 @@ (* Main function to start metis prove and reconstruction *) fun FOL_SOLVE mode ctxt cls ths0 = - let val thy = ProofContext.theory_of ctxt - val th_cls_pairs = map (fn th => (PureThy.get_name_hint th, ResAxioms.cnf_axiom th)) ths0 + let val th_cls_pairs = map (fn th => (PureThy.get_name_hint th, ResAxioms.cnf_axiom th)) ths0 val ths = List.concat (map #2 th_cls_pairs) val _ = if exists(is_false o prop_of) cls then error "problem contains the empty clause" else (); @@ -568,7 +569,7 @@ val _ = app (fn th => Output.debug (fn () => string_of_thm th)) cls val _ = Output.debug (fn () => "THEOREM CLAUSES") val _ = app (fn th => Output.debug (fn () => string_of_thm th)) ths - val {isFO,axioms,tfrees} = build_map mode thy ctxt cls ths + val {isFO,axioms,tfrees} = build_map mode ctxt cls ths val _ = if null tfrees then () else (Output.debug (fn () => "TFREE CLAUSES"); app (fn tf => Output.debug (fn _ => ResClause.tptp_of_typeLit true tf)) tfrees) diff -r 50959112a4e1 -r ff15f76741bd src/HOL/Tools/res_atp.ML --- a/src/HOL/Tools/res_atp.ML Thu Oct 11 15:57:29 2007 +0200 +++ b/src/HOL/Tools/res_atp.ML Thu Oct 11 15:59:31 2007 +0200 @@ -36,7 +36,6 @@ val rm_simpset : unit -> unit val rm_atpset : unit -> unit val rm_clasimp : unit -> unit - val is_fol_thms : thm list -> bool val tvar_classes_of_terms : term list -> string list val tfree_classes_of_terms : term list -> string list val type_consts_of_terms : theory -> term list -> string list @@ -137,128 +136,9 @@ fun add_atpset() = include_atpset:=true; fun rm_atpset() = include_atpset:=false; - -(******************************************************************) -(* detect whether a given problem (clauses) is FOL/HOL/HOLC/HOLCS *) -(******************************************************************) - -datatype logic = FOL | HOL | HOLC | HOLCS; - -fun string_of_logic FOL = "FOL" - | string_of_logic HOL = "HOL" - | string_of_logic HOLC = "HOLC" - | string_of_logic HOLCS = "HOLCS"; - -fun is_fol_logic FOL = true - | is_fol_logic _ = false - -(*HOLCS will not occur here*) -fun upgrade_lg HOLC _ = HOLC - | upgrade_lg HOL HOLC = HOLC - | upgrade_lg HOL _ = HOL - | upgrade_lg FOL lg = lg; - -(* check types *) -fun has_bool_hfn (Type("bool",_)) = true - | has_bool_hfn (Type("fun",_)) = true - | has_bool_hfn (Type(_, Ts)) = exists has_bool_hfn Ts - | has_bool_hfn _ = false; - -fun is_hol_fn tp = - let val (targs,tr) = strip_type tp - in - exists (has_bool_hfn) (tr::targs) - end; - -fun is_hol_pred tp = - let val (targs,tr) = strip_type tp - in - exists (has_bool_hfn) targs - end; - -exception FN_LG of term; - -fun fn_lg (t as Const(f,tp)) (lg,seen) = - if is_hol_fn tp then (upgrade_lg HOL lg, insert (op =) t seen) else (lg, insert (op =) t seen) - | fn_lg (t as Free(f,tp)) (lg,seen) = - if is_hol_fn tp then (upgrade_lg HOL lg, insert (op =) t seen) else (lg, insert (op =) t seen) - | fn_lg (t as Var(f,tp)) (lg,seen) = - if is_hol_fn tp then (upgrade_lg HOL lg,insert (op =) t seen) else (lg,insert (op =) t seen) - | fn_lg (t as Abs(_,_,_)) (lg,seen) = (upgrade_lg HOLC lg,insert (op =) t seen) - | fn_lg f _ = raise FN_LG(f); - +fun strip_Trueprop (Const("Trueprop",_) $ t) = t + | strip_Trueprop t = t; -fun term_lg [] (lg,seen) = (lg,seen) - | term_lg (tm::tms) (FOL,seen) = - let val (f,args) = strip_comb tm - val (lg',seen') = if f mem seen then (FOL,seen) - else fn_lg f (FOL,seen) - in - if is_fol_logic lg' then () - else Output.debug (fn () => ("Found a HOL term: " ^ Display.raw_string_of_term f)); - term_lg (args@tms) (lg',seen') - end - | term_lg _ (lg,seen) = (lg,seen) - -exception PRED_LG of term; - -fun pred_lg (t as Const(P,tp)) (lg,seen)= - if is_hol_pred tp then (upgrade_lg HOL lg, insert (op =) t seen) - else (lg,insert (op =) t seen) - | pred_lg (t as Free(P,tp)) (lg,seen) = - if is_hol_pred tp then (upgrade_lg HOL lg, insert (op =) t seen) - else (lg,insert (op =) t seen) - | pred_lg (t as Var(_,_)) (lg,seen) = (upgrade_lg HOL lg, insert (op =) t seen) - | pred_lg P _ = raise PRED_LG(P); - - -fun lit_lg (Const("Not",_) $ P) (lg,seen) = lit_lg P (lg,seen) - | lit_lg P (lg,seen) = - let val (pred,args) = strip_comb P - val (lg',seen') = if pred mem seen then (lg,seen) - else pred_lg pred (lg,seen) - in - if is_fol_logic lg' then () - else Output.debug (fn () => ("Found a HOL predicate: " ^ Display.raw_string_of_term pred)); - term_lg args (lg',seen') - end; - -fun lits_lg [] (lg,seen) = (lg,seen) - | lits_lg (lit::lits) (FOL,seen) = - let val (lg,seen') = lit_lg lit (FOL,seen) - in - if is_fol_logic lg then () - else Output.debug (fn () => ("Found a HOL literal: " ^ Display.raw_string_of_term lit)); - lits_lg lits (lg,seen') - end - | lits_lg lits (lg,seen) = (lg,seen); - -fun dest_disj_aux (Const("Trueprop",_) $ t) disjs = dest_disj_aux t disjs - | dest_disj_aux (Const ("op |", _) $ t $ t') disjs = dest_disj_aux t (dest_disj_aux t' disjs) - | dest_disj_aux t disjs = t::disjs; - -fun dest_disj t = dest_disj_aux t []; - -fun logic_of_clause tm = lits_lg (dest_disj tm); - -fun logic_of_clauses [] (lg,seen) = (lg,seen) - | logic_of_clauses (cls::clss) (FOL,seen) = - let val (lg,seen') = logic_of_clause cls (FOL,seen) - val _ = - if is_fol_logic lg then () - else Output.debug (fn () => ("Found a HOL clause: " ^ Display.raw_string_of_term cls)) - in - logic_of_clauses clss (lg,seen') - end - | logic_of_clauses (cls::clss) (lg,seen) = (lg,seen); - -fun problem_logic_goals_aux [] (lg,seen) = lg - | problem_logic_goals_aux (subgoal::subgoals) (lg,seen) = - problem_logic_goals_aux subgoals (logic_of_clauses subgoal (lg,seen)); - -fun problem_logic_goals subgoals = problem_logic_goals_aux subgoals (FOL,[]); - -fun is_fol_thms ths = ((fst(logic_of_clauses (map prop_of ths) (FOL,[]))) = FOL); (***************************************************************) (* Relevance Filtering *) @@ -544,7 +424,7 @@ fun hash_literal (Const("Not",_)$P) = Word.notb(hashw_term(P,0w0)) | hash_literal P = hashw_term(P,0w0); -fun hash_term t = Word.toIntX (xor_words (map hash_literal (dest_disj t))); +fun hash_term t = Word.toIntX (xor_words (map hash_literal (HOLogic.disjuncts (strip_Trueprop t)))); fun equal_thm (thm1,thm2) = Term.aconv(prop_of thm1, prop_of thm2); @@ -705,9 +585,8 @@ val linkup_logic_mode = ref Auto; (*Ensures that no higher-order theorems "leak out"*) -fun restrict_to_logic thy logic cls = - if is_fol_logic logic then filter (Meson.is_fol_term thy o prop_of o fst) cls - else cls; +fun restrict_to_logic thy true cls = filter (Meson.is_fol_term thy o prop_of o fst) cls + | restrict_to_logic thy false cls = cls; (**** Predicates to detect unwanted clauses (prolific or likely to cause unsoundness) ****) @@ -752,17 +631,13 @@ val unwanted_types = ["Product_Type.unit","bool"]; fun unwanted t = - is_taut t orelse has_typed_var unwanted_types t orelse - forall too_general_equality (dest_disj t); + is_taut t orelse has_typed_var unwanted_types t orelse + forall too_general_equality (HOLogic.disjuncts (strip_Trueprop t)); (*Clauses containing variables of type "unit" or "bool" are unlikely to be useful and likely to lead to unsound proofs.*) fun remove_unwanted_clauses cls = filter (not o unwanted o prop_of o fst) cls; -fun tptp_writer thy logic = ResHolClause.tptp_write_file thy (logic=FOL); - -fun dfg_writer thy logic = ResHolClause.dfg_write_file thy (logic=FOL); - (*Called by the oracle-based methods declared in res_atp_methods.ML*) fun write_subgoal_file dfg mode ctxt conjectures user_thms n = let val conj_cls = Meson.make_clauses conjectures @@ -771,14 +646,14 @@ val goal_cls = conj_cls@hyp_cls val goal_tms = map prop_of goal_cls val thy = ProofContext.theory_of ctxt - val logic = case mode of - Auto => problem_logic_goals [goal_tms] - | Fol => FOL - | Hol => HOL + val isFO = case mode of + Auto => forall (Meson.is_fol_term thy) goal_tms + | Fol => true + | Hol => false val (included_thms,user_rules) = get_clasimp_atp_lemmas ctxt user_thms val cla_simp_atp_clauses = included_thms |> ResAxioms.cnf_rules_pairs |> make_unique - |> restrict_to_logic thy logic + |> restrict_to_logic thy isFO |> remove_unwanted_clauses val user_cls = ResAxioms.cnf_rules_pairs user_rules val axclauses = make_unique (user_cls @ relevance_filter thy cla_simp_atp_clauses goal_tms) @@ -789,11 +664,11 @@ (*TFrees in conjecture clauses; TVars in axiom clauses*) val (supers',arity_clauses) = ResClause.make_arity_clauses thy tycons supers val classrel_clauses = ResClause.make_classrel_clauses thy subs supers' - val writer = if dfg then dfg_writer else tptp_writer + val writer = if dfg then ResHolClause.dfg_write_file else ResHolClause.tptp_write_file and file = atp_input_file() and user_lemmas_names = map #1 user_rules in - writer thy logic goal_cls file (axclauses,classrel_clauses,arity_clauses) user_lemmas_names; + writer thy isFO goal_cls file (axclauses,classrel_clauses,arity_clauses) user_lemmas_names; Output.debug (fn () => "Writing to " ^ file); file end; @@ -866,13 +741,13 @@ | get_neg_subgoals (gl::gls) n = #1 (ResAxioms.neg_conjecture_clauses th n) :: get_neg_subgoals gls (n+1) val goal_cls = get_neg_subgoals goals 1 - val logic = case !linkup_logic_mode of - Auto => problem_logic_goals (map (map prop_of) goal_cls) - | Fol => FOL - | Hol => HOL + val isFO = case !linkup_logic_mode of + Auto => forall (Meson.is_fol_term thy) (map prop_of (List.concat goal_cls)) + | Fol => true + | Hol => false val (included_thms,white_thms) = get_clasimp_atp_lemmas ctxt chain_ths val included_cls = included_thms |> ResAxioms.cnf_rules_pairs |> make_unique - |> restrict_to_logic thy logic + |> restrict_to_logic thy isFO |> remove_unwanted_clauses val _ = Output.debug (fn () => "included clauses = " ^ Int.toString(length included_cls)) val white_cls = ResAxioms.cnf_rules_pairs white_thms @@ -880,7 +755,7 @@ val axcls_list = map (fn ngcls => white_cls @ relevance_filter thy included_cls (map prop_of ngcls)) goal_cls val _ = app (fn axcls => Output.debug (fn () => "filtered clauses = " ^ Int.toString(length axcls))) axcls_list - val writer = if !prover = Recon.SPASS then dfg_writer else tptp_writer + val writer = if !prover = Recon.SPASS then ResHolClause.dfg_write_file else ResHolClause.tptp_write_file fun write_all [] [] _ = [] | write_all (ccls::ccls_list) (axcls::axcls_list) k = let val fname = probfile k @@ -901,7 +776,7 @@ val _ = Output.debug (fn () => "arity clauses = " ^ Int.toString (length arity_clauses)) val classrel_clauses = ResClause.make_classrel_clauses thy subs supers' val _ = Output.debug (fn () => "classrel clauses = " ^ Int.toString (length classrel_clauses)) - val clnames = writer thy logic ccls fname (axcls,classrel_clauses,arity_clauses) [] + val clnames = writer thy isFO ccls fname (axcls,classrel_clauses,arity_clauses) [] val thm_names = Vector.fromList clnames val _ = if !Output.debugging then trace_vector fname thm_names else () in (thm_names,fname) :: write_all ccls_list axcls_list (k+1) end diff -r 50959112a4e1 -r ff15f76741bd src/HOL/Tools/res_reconstruct.ML --- a/src/HOL/Tools/res_reconstruct.ML Thu Oct 11 15:57:29 2007 +0200 +++ b/src/HOL/Tools/res_reconstruct.ML Thu Oct 11 15:59:31 2007 +0200 @@ -282,12 +282,6 @@ let val vt0 = tfree_constraints_of_clauses Vartab.empty (map #3 tuples) in map (decode_tstp ctxt vt0) tuples end; -(*FIXME: simmilar function in res_atp. Move to HOLogic?*) -fun dest_disj_aux (Const ("op |", _) $ t $ t') disjs = dest_disj_aux t (dest_disj_aux t' disjs) - | dest_disj_aux t disjs = t::disjs; - -fun dest_disj t = dest_disj_aux t []; - (** Finding a matching assumption. The literals may be permuted, and variable names may disagree. We have to try all combinations of literals (quadratic!) and match up the variable names consistently. **) @@ -339,10 +333,10 @@ matches_aux [] (map Envir.eta_contract lits1) (map Envir.eta_contract lits2); fun permuted_clause t = - let val lits = dest_disj t + let val lits = HOLogic.disjuncts t fun perm [] = NONE | perm (ctm::ctms) = - if matches (lits, dest_disj (HOLogic.dest_Trueprop (strip_alls ctm))) + if matches (lits, HOLogic.disjuncts (HOLogic.dest_Trueprop (strip_alls ctm))) then SOME ctm else perm ctms in perm end; diff -r 50959112a4e1 -r ff15f76741bd src/HOL/hologic.ML --- a/src/HOL/hologic.ML Thu Oct 11 15:57:29 2007 +0200 +++ b/src/HOL/hologic.ML Thu Oct 11 15:59:31 2007 +0200 @@ -31,6 +31,7 @@ val mk_not: term -> term val dest_conj: term -> term list val dest_disj: term -> term list + val disjuncts: term -> term list val dest_imp: term -> term * term val dest_not: term -> term val dest_concls: term -> term list @@ -184,6 +185,12 @@ fun dest_disj (Const ("op |", _) $ t $ t') = t :: dest_disj t' | dest_disj t = [t]; +(*Like dest_disj, but flattens disjunctions however nested*) +fun disjuncts_aux (Const ("op |", _) $ t $ t') disjs = disjuncts_aux t (disjuncts_aux t' disjs) + | disjuncts_aux t disjs = t::disjs; + +fun disjuncts t = disjuncts_aux t []; + fun dest_imp (Const("op -->",_) $ A $ B) = (A, B) | dest_imp t = raise TERM ("dest_imp", [t]);