# HG changeset patch # User blanchet # Date 1292408788 -3600 # Node ID 30bedf58b177e0532906309c1bd80a5eed3d0850 # Parent 8c5d44c7e8af86863f3f1ddc183fece6d93c2d1e implemented new type system encoding "overload_args", which is more lightweight than "const_args" (the unsound default) and hopefully almost as sound diff -r 8c5d44c7e8af -r 30bedf58b177 src/HOL/Tools/Sledgehammer/sledgehammer_atp_reconstruct.ML --- a/src/HOL/Tools/Sledgehammer/sledgehammer_atp_reconstruct.ML Wed Dec 15 11:26:28 2010 +0100 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_atp_reconstruct.ML Wed Dec 15 11:26:28 2010 +0100 @@ -9,10 +9,11 @@ signature SLEDGEHAMMER_ATP_RECONSTRUCT = sig type locality = Sledgehammer_Filter.locality + type type_system = Sledgehammer_ATP_Translate.type_system type minimize_command = string list -> string type metis_params = - string * bool * minimize_command * string * (string * locality) list vector - * thm * int + string * type_system * minimize_command * string + * (string * locality) list vector * thm * int type isar_params = string Symtab.table * bool * int * Proof.context * int list list type text_result = string * (string * locality) list @@ -43,8 +44,8 @@ type minimize_command = string list -> string type metis_params = - string * bool * minimize_command * string * (string * locality) list vector - * thm * int + string * type_system * minimize_command * string + * (string * locality) list vector * thm * int type isar_params = string Symtab.table * bool * int * Proof.context * int list list type text_result = string * (string * locality) list @@ -125,12 +126,12 @@ fun using_labels [] = "" | using_labels ls = "using " ^ space_implode " " (map string_for_label ls) ^ " " -fun metis_name full_types = if full_types then "metisFT" else "metis" -fun metis_call full_types ss = command_call (metis_name full_types) ss -fun metis_command full_types i n (ls, ss) = - using_labels ls ^ apply_on_subgoal i n ^ metis_call full_types ss -fun metis_line banner full_types i n ss = - try_command_line banner (metis_command full_types i n ([], ss)) +fun metis_name type_sys = if is_fully_typed type_sys then "metisFT" else "metis" +fun metis_call type_sys ss = command_call (metis_name type_sys) ss +fun metis_command type_sys i n (ls, ss) = + using_labels ls ^ apply_on_subgoal i n ^ metis_call type_sys ss +fun metis_line banner type_sys i n ss = + try_command_line banner (metis_command type_sys i n ([], ss)) fun minimize_line _ [] = "" | minimize_line minimize_command ss = case minimize_command ss of @@ -165,14 +166,14 @@ List.partition (curry (op =) Chained o snd) #> pairself (sort_distinct (string_ord o pairself fst)) -fun metis_proof_text (banner, full_types, minimize_command, - tstplike_proof, fact_names, goal, i) = +fun metis_proof_text (banner, type_sys, minimize_command, tstplike_proof, + fact_names, goal, i) = let val (chained_lemmas, other_lemmas) = split_used_facts (used_facts_in_tstplike_proof fact_names tstplike_proof) val n = Logic.count_prems (prop_of goal) in - (metis_line banner full_types i n (map fst other_lemmas) ^ + (metis_line banner type_sys i n (map fst other_lemmas) ^ minimize_line minimize_command (map fst (other_lemmas @ chained_lemmas)), other_lemmas @ chained_lemmas) end @@ -303,7 +304,7 @@ (* First-order translation. No types are known for variables. "HOLogic.typeT" should allow them to be inferred. *) -fun raw_term_from_pred thy full_types tfrees = +fun raw_term_from_pred thy type_sys tfrees = let fun aux opt_T extra_us u = case u of @@ -327,25 +328,26 @@ | SOME b => let val c = invert_const b - val num_type_args = num_type_args thy c - val (type_us, term_us) = - chop (if full_types then 0 else num_type_args) us + val num_ty_args = num_atp_type_args thy type_sys c + val (type_us, term_us) = chop num_ty_args us (* Extra args from "hAPP" come after any arguments given directly to the constant. *) val term_ts = map (aux NONE []) term_us val extra_ts = map (aux NONE []) extra_us val t = - Const (c, if full_types then + Const (c, if is_fully_typed type_sys then case opt_T of SOME T => map fastype_of term_ts ---> T | NONE => - if num_type_args = 0 then + if num_type_args thy c = 0 then Sign.const_instance thy (c, []) else raise Fail ("no type information for " ^ quote c) - else + else if num_type_args thy c = length type_us then Sign.const_instance thy (c, - map (type_from_fo_term tfrees) type_us)) + map (type_from_fo_term tfrees) type_us) + else + HOLogic.typeT) in list_comb (t, term_ts @ extra_ts) end | NONE => (* a free or schematic variable *) let @@ -366,12 +368,12 @@ in list_comb (t, ts) end in aux (SOME HOLogic.boolT) [] end -fun term_from_pred thy full_types tfrees pos (u as ATerm (s, _)) = +fun term_from_pred thy type_sys tfrees pos (u as ATerm (s, _)) = if String.isPrefix class_prefix s then add_type_constraint (type_constraint_from_term pos tfrees u) #> pair @{const True} else - pair (raw_term_from_pred thy full_types tfrees u) + pair (raw_term_from_pred thy type_sys tfrees u) val combinator_table = [(@{const_name Meson.COMBI}, @{thm Meson.COMBI_def_raw}), @@ -412,7 +414,7 @@ (* Interpret an ATP formula as a HOL term, extracting sort constraints as they appear in the formula. *) -fun prop_from_formula thy full_types tfrees phi = +fun prop_from_formula thy type_sys tfrees phi = let fun do_formula pos phi = case phi of @@ -435,7 +437,7 @@ | AIff => s_iff | ANotIff => s_not o s_iff | _ => raise Fail "unexpected connective") - | AAtom tm => term_from_pred thy full_types tfrees pos tm + | AAtom tm => term_from_pred thy type_sys tfrees pos tm | _ => raise FORMULA [phi] in repair_tvar_sorts (do_formula true phi Vartab.empty) end @@ -449,14 +451,14 @@ fun unvarify_term (Var ((s, 0), T)) = Free (s, T) | unvarify_term t = raise TERM ("unvarify_term: non-Var", [t]) -fun decode_line full_types tfrees (Definition (name, phi1, phi2)) ctxt = +fun decode_line type_sys tfrees (Definition (name, phi1, phi2)) ctxt = let val thy = ProofContext.theory_of ctxt - val t1 = prop_from_formula thy full_types tfrees phi1 + val t1 = prop_from_formula thy type_sys tfrees phi1 val vars = snd (strip_comb t1) val frees = map unvarify_term vars val unvarify_args = subst_atomic (vars ~~ frees) - val t2 = prop_from_formula thy full_types tfrees phi2 + val t2 = prop_from_formula thy type_sys tfrees phi2 val (t1, t2) = HOLogic.eq_const HOLogic.typeT $ t1 $ t2 |> unvarify_args |> uncombine_term |> check_formula ctxt @@ -465,17 +467,17 @@ (Definition (name, t1, t2), fold Variable.declare_term (maps OldTerm.term_frees [t1, t2]) ctxt) end - | decode_line full_types tfrees (Inference (name, u, deps)) ctxt = + | decode_line type_sys tfrees (Inference (name, u, deps)) ctxt = let val thy = ProofContext.theory_of ctxt - val t = u |> prop_from_formula thy full_types tfrees + val t = u |> prop_from_formula thy type_sys tfrees |> uncombine_term |> check_formula ctxt in (Inference (name, t, deps), fold Variable.declare_term (OldTerm.term_frees t) ctxt) end -fun decode_lines ctxt full_types tfrees lines = - fst (fold_map (decode_line full_types tfrees) lines ctxt) +fun decode_lines ctxt type_sys tfrees lines = + fst (fold_map (decode_line type_sys tfrees) lines ctxt) fun is_same_inference _ (Definition _) = false | is_same_inference t (Inference (_, t', _)) = t aconv t' @@ -605,16 +607,15 @@ else s -fun isar_proof_from_tstplike_proof pool ctxt full_types tfrees - isar_shrink_factor tstplike_proof conjecture_shape fact_names params - frees = +fun isar_proof_from_tstplike_proof pool ctxt type_sys tfrees isar_shrink_factor + tstplike_proof conjecture_shape fact_names params frees = let val lines = tstplike_proof |> atp_proof_from_tstplike_string |> nasty_atp_proof pool |> map_term_names_in_atp_proof repair_name - |> decode_lines ctxt full_types tfrees + |> decode_lines ctxt type_sys tfrees |> rpair [] |-> fold_rev (add_line conjecture_shape fact_names) |> rpair [] |-> fold_rev add_nontrivial_line |> rpair (0, []) |-> fold_rev (add_desired_line isar_shrink_factor @@ -857,7 +858,7 @@ step :: aux subst depth nextp proof in aux [] 0 (1, 1) end -fun string_for_proof ctxt0 full_types i n = +fun string_for_proof ctxt0 type_sys i n = let val ctxt = ctxt0 |> Config.put show_free_types false @@ -879,7 +880,7 @@ if member (op =) qs Show then "show" else "have") val do_term = maybe_quote o fix_print_mode (Syntax.string_of_term ctxt) fun do_facts (ls, ss) = - metis_command full_types 1 1 + metis_command type_sys 1 1 (ls |> sort_distinct (prod_ord string_ord int_ord), ss |> sort_distinct string_ord) and do_step ind (Fix xs) = @@ -914,7 +915,7 @@ in do_proof end fun isar_proof_text (pool, debug, isar_shrink_factor, ctxt, conjecture_shape) - (metis_params as (_, full_types, _, tstplike_proof, + (metis_params as (_, type_sys, _, tstplike_proof, fact_names, goal, i)) = let val (params, hyp_ts, concl_t) = strip_subgoal goal i @@ -923,7 +924,7 @@ val n = Logic.count_prems (prop_of goal) val (one_line_proof, lemma_names) = metis_proof_text metis_params fun isar_proof_for () = - case isar_proof_from_tstplike_proof pool ctxt full_types tfrees + case isar_proof_from_tstplike_proof pool ctxt type_sys tfrees isar_shrink_factor tstplike_proof conjecture_shape fact_names params frees |> redirect_proof hyp_ts concl_t @@ -931,7 +932,7 @@ |> then_chain_proof |> kill_useless_labels_in_proof |> relabel_proof - |> string_for_proof ctxt full_types i n of + |> string_for_proof ctxt type_sys i n of "" => "\nNo structured proof available." | proof => "\n\nStructured proof:\n" ^ Markup.markup Markup.sendback proof val isar_proof = diff -r 8c5d44c7e8af -r 30bedf58b177 src/HOL/Tools/Sledgehammer/sledgehammer_atp_translate.ML --- a/src/HOL/Tools/Sledgehammer/sledgehammer_atp_translate.ML Wed Dec 15 11:26:28 2010 +0100 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_atp_translate.ML Wed Dec 15 11:26:28 2010 +0100 @@ -20,6 +20,8 @@ val fact_prefix : string val conjecture_prefix : string + val is_fully_typed : type_system -> bool + val num_atp_type_args : theory -> type_system -> string -> int val translate_atp_fact : Proof.context -> (string * 'a) * thm -> translated_formula option * ((string * 'a) * thm) @@ -63,6 +65,24 @@ | is_fully_typed (Preds full_types) = full_types | is_fully_typed _ = false +(* This is an approximation. If it returns "true" for a constant that isn't + overloaded (i.e., that has one uniform definition), needless clutter is + generated; if it returns "false" for an overloaded constant, the ATP gets a + license to do unsound reasoning if the type system is "overloaded_args". *) +fun is_overloaded thy s = + length (Defs.specifications_of (Theory.defs_of thy) s) > 1 + +fun needs_type_args thy type_sys s = + case type_sys of + Tags full_types => not full_types + | Preds full_types => not full_types + | Const_Args => true + | Overload_Args => is_overloaded thy s + | No_Types => false + +fun num_atp_type_args thy type_sys s = + if needs_type_args thy type_sys s then num_type_args thy s else 0 + fun mk_anot phi = AConn (ANot, [phi]) fun mk_aconn c phi1 phi2 = AConn (c, [phi1, phi2]) fun mk_ahorn [] phi = phi @@ -308,7 +328,7 @@ fun formula_for_fo_literal (pos, t) = AAtom t |> not pos ? mk_anot -fun fo_term_for_combterm type_sys = +fun fo_term_for_combterm thy type_sys = let fun aux top_level u = let @@ -316,18 +336,27 @@ val (x, ty_args) = case head of CombConst (name as (s, s'), _, ty_args) => - let val ty_args = if is_fully_typed type_sys then [] else ty_args in - if s = "equal" then - if top_level andalso length args = 2 then (name, []) - else (("c_fequal", @{const_name Metis.fequal}), ty_args) - else if top_level then - case s of - "c_False" => (("$false", s'), []) - | "c_True" => (("$true", s'), []) - | _ => (name, ty_args) - else - (name, ty_args) - end + (case strip_prefix_and_unascii const_prefix s of + NONE => + if s = "equal" then + if top_level andalso length args = 2 then (name, []) + else (("c_fequal", @{const_name Metis.fequal}), ty_args) + else + (name, ty_args) + | SOME s'' => + let + val s'' = invert_const s'' + val ty_args = + if needs_type_args thy type_sys s'' then ty_args else [] + in + if top_level then + case s of + "c_False" => (("$false", s'), []) + | "c_True" => (("$true", s'), []) + | _ => (name, ty_args) + else + (name, ty_args) + end) | CombVar (name, _) => (name, []) | CombApp _ => raise Fail "impossible \"CombApp\"" val t = ATerm (x, map fo_term_for_combtyp ty_args @ @@ -340,21 +369,21 @@ end in aux true end -fun formula_for_combformula type_sys = +fun formula_for_combformula thy type_sys = let fun aux (AQuant (q, xs, phi)) = AQuant (q, xs, aux phi) | aux (AConn (c, phis)) = AConn (c, map aux phis) - | aux (AAtom tm) = AAtom (fo_term_for_combterm type_sys tm) + | aux (AAtom tm) = AAtom (fo_term_for_combterm thy type_sys tm) in aux end -fun formula_for_fact type_sys +fun formula_for_fact thy type_sys ({combformula, ctypes_sorts, ...} : translated_formula) = mk_ahorn (map (formula_for_fo_literal o fo_literal_for_type_literal) (type_literals_for_types ctypes_sorts)) - (formula_for_combformula type_sys combformula) + (formula_for_combformula thy type_sys combformula) -fun problem_line_for_fact prefix type_sys (formula as {name, kind, ...}) = - Fof (prefix ^ ascii_of name, kind, formula_for_fact type_sys formula) +fun problem_line_for_fact thy prefix type_sys (formula as {name, kind, ...}) = + Fof (prefix ^ ascii_of name, kind, formula_for_fact thy type_sys formula) fun problem_line_for_class_rel_clause (ClassRelClause {name, subclass, superclass, ...}) = @@ -377,10 +406,10 @@ (formula_for_fo_literal (fo_literal_for_arity_literal conclLit))) -fun problem_line_for_conjecture type_sys +fun problem_line_for_conjecture thy type_sys ({name, kind, combformula, ...} : translated_formula) = Fof (conjecture_prefix ^ name, kind, - formula_for_combformula type_sys combformula) + formula_for_combformula thy type_sys combformula) fun free_type_literals_for_conjecture ({ctypes_sorts, ...} : translated_formula) = @@ -427,10 +456,8 @@ String.isPrefix type_const_prefix s orelse String.isPrefix class_prefix s then 16383 (* large number *) - else if is_fully_typed type_sys then - 0 else case strip_prefix_and_unascii const_prefix s of - SOME s' => num_type_args thy (invert_const s') + SOME s' => num_atp_type_args thy type_sys (invert_const s') | NONE => 0) | min_arity_of _ _ (SOME the_const_tab) s = case Symtab.lookup the_const_tab s of @@ -528,11 +555,11 @@ val (fact_names, (conjectures, facts, helper_facts, class_rel_clauses, arity_clauses)) = translate_formulas ctxt type_sys hyp_ts concl_t facts - val fact_lines = map (problem_line_for_fact fact_prefix type_sys) facts + val fact_lines = map (problem_line_for_fact thy fact_prefix type_sys) facts val helper_lines = - map (problem_line_for_fact helper_prefix type_sys) helper_facts + map (problem_line_for_fact thy helper_prefix type_sys) helper_facts val conjecture_lines = - map (problem_line_for_conjecture type_sys) conjectures + map (problem_line_for_conjecture thy type_sys) conjectures val tfree_lines = problem_lines_for_free_types conjectures val class_rel_lines = map problem_line_for_class_rel_clause class_rel_clauses diff -r 8c5d44c7e8af -r 30bedf58b177 src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML --- a/src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML Wed Dec 15 11:26:28 2010 +0100 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML Wed Dec 15 11:26:28 2010 +0100 @@ -99,7 +99,7 @@ ("no_isar_proof", "isar_proof")] val params_for_minimize = - ["debug", "verbose", "overlord", "full_types", "type_sys", "isar_proof", + ["debug", "verbose", "overlord", "type_sys", "full_types", "isar_proof", "isar_shrink_factor", "timeout"] val property_dependent_params = ["provers", "full_types", "timeout"] @@ -221,8 +221,8 @@ val overlord = lookup_bool "overlord" val provers = lookup_string "provers" |> space_explode " " |> auto ? single o hd + val type_sys = lookup_string "type_sys" val full_types = lookup_bool "full_types" - val type_sys = lookup_string "type_sys" val explicit_apply = lookup_bool "explicit_apply" val relevance_thresholds = lookup_real_pair "relevance_thresholds" val max_relevant = lookup_int_option "max_relevant" @@ -232,7 +232,7 @@ val expect = lookup_string "expect" in {blocking = blocking, debug = debug, verbose = verbose, overlord = overlord, - provers = provers, full_types = full_types, type_sys = type_sys, + provers = provers, type_sys = type_sys, full_types = full_types, explicit_apply = explicit_apply, relevance_thresholds = relevance_thresholds, max_relevant = max_relevant, isar_proof = isar_proof, isar_shrink_factor = isar_shrink_factor, diff -r 8c5d44c7e8af -r 30bedf58b177 src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML --- a/src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML Wed Dec 15 11:26:28 2010 +0100 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML Wed Dec 15 11:26:28 2010 +0100 @@ -20,8 +20,8 @@ verbose: bool, overlord: bool, provers: string list, + type_sys: string, full_types: bool, - type_sys: string, explicit_apply: bool, relevance_thresholds: real * real, max_relevant: int option, @@ -204,8 +204,8 @@ verbose: bool, overlord: bool, provers: string list, + type_sys: string, full_types: bool, - type_sys: string, explicit_apply: bool, relevance_thresholds: real * real, max_relevant: int option, @@ -271,7 +271,7 @@ fun run_atp auto atp_name ({exec, required_execs, arguments, has_incomplete_mode, proof_delims, known_failures, explicit_forall, use_conjecture_for_hypotheses, ...} : atp_config) - ({debug, verbose, overlord, full_types, type_sys, explicit_apply, + ({debug, verbose, overlord, type_sys, full_types, explicit_apply, isar_proof, isar_shrink_factor, timeout, ...} : params) minimize_command ({state, goal, subgoal, facts, ...} : prover_problem) = let @@ -398,7 +398,7 @@ NONE => proof_text isar_proof (pool, debug, isar_shrink_factor, ctxt, conjecture_shape) - (proof_banner auto, full_types, minimize_command, tstplike_proof, + (proof_banner auto, type_sys, minimize_command, tstplike_proof, fact_names, goal, subgoal) |>> (fn message => message ^