# HG changeset patch # User blanchet # Date 1306852716 -7200 # Node ID e88e974c4846a0d18d7f20fcd7cdaa34959a11eb # Parent 69251cad0da039695fe4fcd1e07aa6e84b22883a proper handling of type variable classes in new Metis diff -r 69251cad0da0 -r e88e974c4846 src/HOL/Tools/ATP/atp_problem.ML --- a/src/HOL/Tools/ATP/atp_problem.ML Tue May 31 16:38:36 2011 +0200 +++ b/src/HOL/Tools/ATP/atp_problem.ML Tue May 31 16:38:36 2011 +0200 @@ -143,6 +143,17 @@ fun is_tptp_variable s = Char.isUpper (String.sub (s, 0)) val is_tptp_user_symbol = not o (is_tptp_variable orf is_built_in_tptp_symbol) +fun raw_polarities_of_conn ANot = (SOME false, NONE) + | raw_polarities_of_conn AAnd = (SOME true, SOME true) + | raw_polarities_of_conn AOr = (SOME true, SOME true) + | raw_polarities_of_conn AImplies = (SOME false, SOME true) + | raw_polarities_of_conn AIf = (SOME true, SOME false) + | raw_polarities_of_conn AIff = (NONE, NONE) + | raw_polarities_of_conn ANotIff = (NONE, NONE) +fun polarities_of_conn NONE = K (NONE, NONE) + | polarities_of_conn (SOME pos) = + raw_polarities_of_conn #> not pos ? pairself (Option.map not) + fun mk_anot (AConn (ANot, [phi])) = phi | mk_anot phi = AConn (ANot, [phi]) fun mk_aconn c phi1 phi2 = AConn (c, [phi1, phi2]) @@ -286,7 +297,7 @@ problem -(** CNF UEQ (Waldmeister) **) +(** CNF (Metis) and CNF UEQ (Waldmeister) **) fun is_problem_line_negated (Formula (_, _, AConn (ANot, _), _, _)) = true | is_problem_line_negated _ = false @@ -298,9 +309,17 @@ fun open_conjecture_term (ATerm ((s, s'), tms)) = ATerm (if is_tptp_variable s then (s |> Name.desymbolize false, s') else (s, s'), tms |> map open_conjecture_term) -fun open_formula conj (AQuant (AForall, _, phi)) = open_formula conj phi - | open_formula true (AAtom t) = AAtom (open_conjecture_term t) - | open_formula _ phi = phi +fun open_formula conj = + let + fun opn (pos as SOME true) (AQuant (AForall, xs, phi)) = opn pos phi + | opn (pos as SOME false) (AQuant (AExists, xs, phi)) = opn pos phi + | opn pos (AConn (ANot, [phi])) = mk_anot (opn (Option.map not pos) phi) + | opn pos (AConn (c, [phi1, phi2])) = + let val (pos1, pos2) = polarities_of_conn pos c in + AConn (c, [opn pos1 phi1, opn pos2 phi2]) + end + | opn _ (AAtom t) = AAtom (t |> conj ? open_conjecture_term) + in opn (SOME (not conj)) end fun open_formula_line (Formula (ident, kind, phi, source, info)) = Formula (ident, kind, open_formula (kind = Conjecture) phi, source, info) | open_formula_line line = line @@ -309,7 +328,31 @@ Formula (ident, Hypothesis, mk_anot phi, source, info) | negate_conjecture_line line = line -fun ensure_cnf_problem problem = problem |> map (apsnd (map open_formula_line)) +exception CLAUSIFY of unit + +fun clausify_formula pos (phi as AAtom _) = phi |> not pos ? mk_anot + | clausify_formula pos (AConn (ANot, [phi])) = clausify_formula (not pos) phi + | clausify_formula false (AConn (AAnd, phis)) = + AConn (AOr, map (clausify_formula false) phis) + | clausify_formula true (AConn (AOr, phis)) = + AConn (AOr, map (clausify_formula true) phis) + | clausify_formula true (AConn (AImplies, [phi1, phi2])) = + AConn (AOr, [clausify_formula false phi1, clausify_formula true phi2]) + | clausify_formula true (AConn (AIf, phis)) = + clausify_formula true (AConn (AImplies, rev phis)) + | clausify_formula _ _ = raise CLAUSIFY () + +fun clausify_formula_line (Formula (ident, kind, phi, source, info)) = + (case try (clausify_formula true) phi of + SOME phi => SOME (Formula (ident, kind, phi, source, info)) + | NONE => NONE) + | clausify_formula_line _ = NONE + +fun ensure_cnf_problem_line line = + line |> open_formula_line |> negate_conjecture_line |> clausify_formula_line + +fun ensure_cnf_problem problem = + problem |> map (apsnd (map_filter ensure_cnf_problem_line)) fun filter_cnf_ueq_problem problem = problem diff -r 69251cad0da0 -r e88e974c4846 src/HOL/Tools/ATP/atp_translate.ML --- a/src/HOL/Tools/ATP/atp_translate.ML Tue May 31 16:38:36 2011 +0200 +++ b/src/HOL/Tools/ATP/atp_translate.ML Tue May 31 16:38:36 2011 +0200 @@ -618,9 +618,9 @@ general_type_arg_policy type_sys (*Make literals for sorted type variables*) -fun sorts_on_typs_aux (_, []) = [] - | sorts_on_typs_aux ((x, i), s :: ss) = - sorts_on_typs_aux ((x, i), ss) +fun generic_sorts_on_type (_, []) = [] + | generic_sorts_on_type ((x, i), s :: ss) = + generic_sorts_on_type ((x, i), ss) |> (if s = the_single @{sort HOL.type} then I else if i = ~1 then @@ -628,21 +628,18 @@ else cons (TyLitVar (`make_type_class s, (make_schematic_type_var (x, i), x)))) - -fun sorts_on_typs (TFree (a, s)) = sorts_on_typs_aux ((a, ~1), s) - | sorts_on_typs (TVar (v, s)) = sorts_on_typs_aux (v, s) - | sorts_on_typs _ = raise Fail "expected \"TVar\" or \"TFree\"" - -(*Given a list of sorted type variables, return a list of type literals.*) -val raw_type_literals_for_types = union_all o map sorts_on_typs +fun sorts_on_tfree (TFree (s, S)) = generic_sorts_on_type ((s, ~1), S) + | sorts_on_tfree _ = [] +fun sorts_on_tvar (TVar z) = generic_sorts_on_type z + | sorts_on_tvar _ = [] -fun type_literals_for_types format type_sys kind Ts = - if level_of_type_sys type_sys = No_Types orelse format = CNF_UEQ then - [] - else - Ts |> raw_type_literals_for_types - |> filter (fn TyLitVar _ => kind <> Conjecture - | TyLitFree _ => kind = Conjecture) +(* Given a list of sorted type variables, return a list of type literals. *) +fun raw_type_literals_for_types Ts = + union_all (map sorts_on_tfree Ts @ map sorts_on_tvar Ts) + +fun type_literals_for_types type_sys sorts_on_typ Ts = + if level_of_type_sys type_sys = No_Types then [] + else union_all (map sorts_on_typ Ts) fun mk_aconns c phis = let val (phis', phi') = split_last phis in @@ -893,7 +890,6 @@ |> extensionalize_term ctxt |> presimp ? presimplify_term ctxt |> introduce_combinators_in_term ctxt kind - |> kind <> Axiom ? freeze_term end (* making fact and conjecture formulas *) @@ -933,7 +929,7 @@ if prem_kind = Conjecture then update_combformula mk_anot else I) in - t |> preproc ? preprocess_prop ctxt true kind + t |> preproc ? (preprocess_prop ctxt true kind #> freeze_term) |> make_formula thy format type_sys true (string_of_int j) General kind |> maybe_negate @@ -1458,9 +1454,9 @@ | do_formula _ (AAtom tm) = AAtom (do_term tm) in do_formula o SOME end -fun bound_atomic_types format type_sys Ts = +fun bound_tvars type_sys Ts = mk_ahorn (map (formula_from_fo_literal o fo_literal_from_type_literal) - (type_literals_for_types format type_sys Axiom Ts)) + (type_literals_for_types type_sys sorts_on_tvar Ts)) fun formula_for_fact ctxt format nonmono_Ts type_sys ({combformula, atomic_types, ...} : translated_formula) = @@ -1468,7 +1464,7 @@ |> close_combformula_universally |> formula_from_combformula ctxt format nonmono_Ts type_sys is_var_nonmonotonic_in_formula true - |> bound_atomic_types format type_sys atomic_types + |> bound_tvars type_sys atomic_types |> close_formula_universally (* Each fact is given a unique fact number to avoid name clashes (e.g., because @@ -1510,24 +1506,24 @@ |> close_formula_universally, intro_info, NONE) fun formula_line_for_conjecture ctxt format nonmono_Ts type_sys - ({name, kind, combformula, ...} : translated_formula) = + ({name, kind, combformula, atomic_types, ...} : translated_formula) = Formula (conjecture_prefix ^ name, kind, formula_from_combformula ctxt format nonmono_Ts type_sys is_var_nonmonotonic_in_formula false (close_combformula_universally combformula) + |> bound_tvars type_sys atomic_types |> close_formula_universally, NONE, NONE) -fun free_type_literals format type_sys - ({atomic_types, ...} : translated_formula) = - atomic_types |> type_literals_for_types format type_sys Conjecture +fun free_type_literals type_sys ({atomic_types, ...} : translated_formula) = + atomic_types |> type_literals_for_types type_sys sorts_on_tfree |> map fo_literal_from_type_literal fun formula_line_for_free_type j lit = Formula (tfree_clause_prefix ^ string_of_int j, Hypothesis, formula_from_fo_literal lit, NONE, NONE) -fun formula_lines_for_free_types format type_sys facts = +fun formula_lines_for_free_types type_sys facts = let - val litss = map (free_type_literals format type_sys) facts + val litss = map (free_type_literals type_sys) facts val lits = fold (union (op =)) litss [] in map2 formula_line_for_free_type (0 upto length lits - 1) lits end @@ -1636,7 +1632,7 @@ |> AAtom |> mk_aquant AForall (bound_names ~~ bound_Ts) |> formula_from_combformula ctxt format nonmono_Ts type_sys (K (K (K (K true)))) true - |> n > 1 ? bound_atomic_types format type_sys (atyps_of T) + |> n > 1 ? bound_tvars type_sys (atyps_of T) |> close_formula_universally |> maybe_negate, intro_info, NONE) @@ -1659,7 +1655,7 @@ fun eq tms = (if pred_sym then AConn (AIff, map AAtom tms) else AAtom (ATerm (`I tptp_equal, tms))) - |> bound_atomic_types format type_sys atomic_Ts + |> bound_tvars type_sys atomic_Ts |> close_formula_universally |> maybe_negate val should_encode = should_encode_type ctxt nonmono_Ts All_Types @@ -1802,8 +1798,7 @@ (conjsN, map (formula_line_for_conjecture ctxt format nonmono_Ts type_sys) conjs), - (free_typesN, - formula_lines_for_free_types format type_sys (facts @ conjs))] + (free_typesN, formula_lines_for_free_types type_sys (facts @ conjs))] val problem = problem |> (case format of diff -r 69251cad0da0 -r e88e974c4846 src/HOL/Tools/Metis/metis_translate.ML --- a/src/HOL/Tools/Metis/metis_translate.ML Tue May 31 16:38:36 2011 +0200 +++ b/src/HOL/Tools/Metis/metis_translate.ML Tue May 31 16:38:36 2011 +0200 @@ -299,11 +299,11 @@ uncurry (union (op =)) (pairself metis_literals_from_atp (phi1, phi2)) | metis_literals_from_atp phi = [metis_literal_from_atp phi] fun metis_axiom_from_atp clauses (Formula (ident, _, phi, _, _)) = - let val j = ident |> unprefix conjecture_prefix |> Int.fromString |> the in - (phi |> metis_literals_from_atp |> Metis_LiteralSet.fromList - |> Metis_Thm.axiom, - Meson.make_meta_clause (nth clauses j)) - end + (phi |> metis_literals_from_atp |> Metis_LiteralSet.fromList + |> Metis_Thm.axiom, + case try (unprefix conjecture_prefix) ident of + SOME s => Meson.make_meta_clause (nth clauses (the (Int.fromString s))) + | NONE => TrueI) | metis_axiom_from_atp _ _ = raise Fail "not CNF -- expected formula" (* Function to generate metis clauses, including comb and type clauses *) @@ -313,9 +313,8 @@ val explicit_apply = NONE val clauses = conj_clauses @ fact_clauses val (atp_problem, _, _, _, _, _, sym_tab) = - prepare_atp_problem ctxt CNF Hypothesis Axiom type_sys - explicit_apply false false (map prop_of clauses) - @{prop False} [] + prepare_atp_problem ctxt CNF Hypothesis Axiom type_sys explicit_apply + false false (map prop_of clauses) @{prop False} [] val axioms = atp_problem |> maps (map_filter (try (metis_axiom_from_atp clauses)) o snd)