# HG changeset patch # User blanchet # Date 1304267844 -7200 # Node ID a14b602fb3d55716902b66e6cf3aa9220bbfdd00 # Parent 75cb06eee990a6c4595f788b4a0db4ae9028f1fe minor cleanup diff -r 75cb06eee990 -r a14b602fb3d5 src/HOL/Tools/Sledgehammer/sledgehammer_atp_translate.ML --- a/src/HOL/Tools/Sledgehammer/sledgehammer_atp_translate.ML Sun May 01 18:37:24 2011 +0200 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_atp_translate.ML Sun May 01 18:37:24 2011 +0200 @@ -529,7 +529,6 @@ CombConst (name as (s, s'), _, ty_args) => (case AList.lookup (op =) fname_table s of SOME (n, fname) => -(*### FIXME: do earlier? *) (if top_level andalso length args = n then case s of "c_False" => ("$false", s') @@ -584,13 +583,13 @@ (* Each fact is given a unique fact number to avoid name clashes (e.g., because of monomorphization). The TPTP explicitly forbids name clashes, and some of the remote provers might care. *) -fun problem_line_for_fact ctxt prefix type_sys +fun formula_line_for_fact ctxt prefix type_sys (j, formula as {name, kind, ...}) = Formula (logic_for_type_sys type_sys, prefix ^ string_of_int j ^ "_" ^ ascii_of name, kind, formula_for_fact ctxt type_sys formula, NONE, NONE) -fun problem_line_for_class_rel_clause (ClassRelClause {name, subclass, +fun formula_line_for_class_rel_clause (ClassRelClause {name, subclass, superclass, ...}) = let val ty_arg = ATerm (`I "T", []) in Formula (Fof, class_rel_clause_prefix ^ ascii_of name, Axiom, @@ -604,7 +603,7 @@ | fo_literal_for_arity_literal (TVarLit (c, sort)) = (false, ATerm (c, [ATerm (sort, [])])) -fun problem_line_for_arity_clause (ArityClause {name, conclLit, premLits, +fun formula_line_for_arity_clause (ArityClause {name, conclLit, premLits, ...}) = Formula (Fof, arity_clause_prefix ^ ascii_of name, Axiom, mk_ahorn (map (formula_for_fo_literal o apfst not @@ -613,7 +612,7 @@ (fo_literal_for_arity_literal conclLit)) |> close_formula_universally, NONE, NONE) -fun problem_line_for_conjecture ctxt type_sys +fun formula_line_for_conjecture ctxt type_sys ({name, kind, combformula, ...} : translated_formula) = Formula (logic_for_type_sys type_sys, conjecture_prefix ^ name, kind, formula_for_combformula ctxt type_sys @@ -624,14 +623,14 @@ ctypes_sorts |> atp_type_literals_for_types type_sys Conjecture |> map fo_literal_for_type_literal -fun problem_line_for_free_type j lit = +fun formula_line_for_free_type j lit = Formula (Fof, tfree_prefix ^ string_of_int j, Hypothesis, formula_for_fo_literal lit, NONE, NONE) -fun problem_lines_for_free_types type_sys facts = +fun formula_lines_for_free_types type_sys facts = let val litss = map (free_type_literals type_sys) facts val lits = fold (union (op =)) litss [] - in map2 problem_line_for_free_type (0 upto length lits - 1) lits end + in map2 formula_line_for_free_type (0 upto length lits - 1) lits end (** "hBOOL" and "hAPP" **) @@ -660,15 +659,12 @@ formula_fold (consider_combterm_for_repair true) combformula (* The "equal" entry is needed for helper facts if the problem otherwise does - not involve equality. The "hBOOL" and "hAPP" entries are needed for symbol - declarations. *) + not involve equality. The "hBOOL" entry is needed to ensure that no "hAPP"s + are introduced for passing arguments to it. *) val default_entries = [("equal", {pred_sym = true, min_arity = 2, max_arity = 2}), (make_fixed_const boolify_base, - {pred_sym = true, min_arity = 1, max_arity = 1}), - (make_fixed_const explicit_app_base, - {pred_sym = false, min_arity = 2, max_arity = 2})] -(* FIXME: last two entries needed? ### *) + {pred_sym = true, min_arity = 1, max_arity = 1})] fun sym_table_for_facts explicit_apply facts = if explicit_apply then @@ -767,6 +763,7 @@ ({combformula, ...} : translated_formula) = formula_fold (consider_combterm_consts type_sys sym_tab) combformula +(* FIXME: needed? *) fun const_table_for_facts type_sys sym_tab facts = Symtab.empty |> member (op =) [Many_Typed, Args true, Mangled true] type_sys ? fold (consider_fact_consts type_sys sym_tab) facts @@ -779,7 +776,7 @@ | _ => ([], f ty)) | strip_and_map_combtyp _ _ _ = raise Fail "unexpected non-function" -fun sym_decl_line_for_const_entry ctxt type_sys sym_tab s (s', ty_args, ty) = +fun problem_line_for_const_entry ctxt type_sys sym_tab s (s', ty_args, ty) = let val thy = Proof_Context.theory_of ctxt val arity = min_arity_of thy type_sys sym_tab s @@ -810,8 +807,8 @@ NONE, NONE) end end -fun sym_decl_lines_for_const ctxt type_sys sym_tab (s, xs) = - map (sym_decl_line_for_const_entry ctxt type_sys sym_tab s) xs +fun problem_lines_for_const ctxt type_sys sym_tab (s, xs) = + map (problem_line_for_const_entry ctxt type_sys sym_tab s) xs fun add_tff_types_in_formula (AQuant (_, xs, phi)) = union (op =) (map_filter snd xs) #> add_tff_types_in_formula phi @@ -827,7 +824,7 @@ fun tff_types_in_problem problem = fold (fold add_tff_types_in_problem_line o snd) problem [] -fun problem_line_for_tff_type (s, s') = +fun decl_line_for_tff_type (s, s') = Decl (type_decl_prefix ^ ascii_of s, (s, s'), [], `I tff_type_of_types) val type_declsN = "Types" @@ -859,13 +856,13 @@ val problem = [(type_declsN, []), (sym_declsN, []), - (factsN, map (problem_line_for_fact ctxt fact_prefix type_sys) + (factsN, map (formula_line_for_fact ctxt fact_prefix type_sys) (0 upto length facts - 1 ~~ facts)), - (class_relsN, map problem_line_for_class_rel_clause class_rel_clauses), - (aritiesN, map problem_line_for_arity_clause arity_clauses), + (class_relsN, map formula_line_for_class_rel_clause class_rel_clauses), + (aritiesN, map formula_line_for_arity_clause arity_clauses), (helpersN, []), - (conjsN, map (problem_line_for_conjecture ctxt type_sys) conjs), - (free_typesN, problem_lines_for_free_types type_sys (facts @ conjs))] + (conjsN, map (formula_line_for_conjecture ctxt type_sys) conjs), + (free_typesN, formula_lines_for_free_types type_sys (facts @ conjs))] val helper_facts = problem |> maps (map_filter (fn Formula (_, _, _, phi, _, _) => SOME phi | _ => NONE) o snd) @@ -873,11 +870,11 @@ |>> map (repair_fact thy type_sys sym_tab) val const_tab = const_table_for_facts type_sys sym_tab (conjs @ facts) val sym_decl_lines = - Symtab.fold_rev (append o sym_decl_lines_for_const ctxt type_sys sym_tab) + Symtab.fold_rev (append o problem_lines_for_const ctxt type_sys sym_tab) const_tab [] val helper_lines = helper_facts - |>> map (pair 0 #> problem_line_for_fact ctxt helper_prefix type_sys) + |>> map (pair 0 #> formula_line_for_fact ctxt helper_prefix type_sys) |> op @ val problem = problem |> fold (AList.update (op =)) @@ -885,7 +882,7 @@ (helpersN, helper_lines)] val type_decl_lines = if type_sys = Many_Typed then - problem |> tff_types_in_problem |> map problem_line_for_tff_type + problem |> tff_types_in_problem |> map decl_line_for_tff_type else [] val (problem, pool) =