# HG changeset patch # User blanchet # Date 1304267844 -7200 # Node ID 024920b65ce2683feecd8e1159178cc6faf8a8d2 # Parent 8938507b205421143d6e9918b4977540706754fb perform constant mangling and/or removal of its type args in an earlier phase, so that the rest of the code doesn't need to worry about it diff -r 8938507b2054 -r 024920b65ce2 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 @@ -26,10 +26,10 @@ val is_type_system_sound : type_system -> bool val type_system_types_dangerous_types : type_system -> bool val num_atp_type_args : theory -> type_system -> string -> int + val unmangled_const : string -> string * string fo_term list val translate_atp_fact : - Proof.context -> bool -> (string * 'a) * thm + Proof.context -> type_system -> bool -> (string * 'a) * thm -> translated_formula option * ((string * 'a) * thm) - val unmangled_const : string -> string * string fo_term list val prepare_atp_problem : Proof.context -> bool -> type_system -> bool -> term list -> term -> (translated_formula option * ((string * 'a) * thm)) list @@ -55,7 +55,7 @@ val boolify_name = "hBOOL" val explicit_app_name = "hAPP" -val is_base = "is" +val type_pred_base = "is" val type_prefix = "ty_" fun make_type ty = type_prefix ^ ascii_of ty @@ -72,6 +72,11 @@ combformula: (name, combtyp, combterm) formula, ctypes_sorts: typ list} +fun map_combformula f + ({name, kind, combformula, ctypes_sorts} : translated_formula) = + {name = name, kind = kind, combformula = f combformula, + ctypes_sorts = ctypes_sorts} : translated_formula + datatype type_system = Many_Typed | Tags of bool | @@ -89,8 +94,8 @@ | type_system_types_dangerous_types type_sys = is_type_system_sound type_sys fun dont_need_type_args type_sys s = - s <> is_base andalso - (member (op =) [@{const_name HOL.eq}, @{const_name Metis.fequal}] s orelse + s <> type_pred_base andalso + (member (op =) [@{const_name HOL.eq}] s orelse case type_sys of Many_Typed => false | Tags full_types => full_types @@ -111,7 +116,7 @@ fun num_atp_type_args thy type_sys s = if type_arg_policy type_sys s = Explicit_Type_Args then - if s = is_base then 1 else num_type_args thy s + if s = type_pred_base then 1 else num_type_args thy s else 0 @@ -156,10 +161,74 @@ #> fold term_vars tms val close_formula_universally = close_universally term_vars -fun combformula_for_prop thy eq_as_iff = +(* We are crossing our fingers that it doesn't clash with anything else. *) +val mangled_type_sep = "\000" + +fun mangled_combtyp_component f (CombTFree name) = f name + | mangled_combtyp_component f (CombTVar name) = + f name (* FIXME: shouldn't happen *) + (* raise Fail "impossible schematic type variable" *) + | mangled_combtyp_component f (CombType (name, tys)) = + f name ^ "(" ^ commas (map (mangled_combtyp_component f) tys) ^ ")" + +fun mangled_combtyp ty = + (make_type (mangled_combtyp_component fst ty), + mangled_combtyp_component snd ty) + +fun mangled_type_suffix f g tys = + fold_rev (curry (op ^) o g o prefix mangled_type_sep + o mangled_combtyp_component f) tys "" + +fun mangled_const_name_fst ty_args s = + s ^ mangled_type_suffix fst ascii_of ty_args +fun mangled_const_name_snd ty_args s' = s' ^ mangled_type_suffix snd I ty_args +fun mangled_const_name ty_args (s, s') = + (mangled_const_name_fst ty_args s, mangled_const_name_snd ty_args s') + +val parse_mangled_ident = + Scan.many1 (not o member (op =) ["(", ")", ","]) >> implode + +fun parse_mangled_type x = + (parse_mangled_ident + -- Scan.optional ($$ "(" |-- Scan.optional parse_mangled_types [] --| $$ ")") + [] >> ATerm) x +and parse_mangled_types x = + (parse_mangled_type ::: Scan.repeat ($$ "," |-- parse_mangled_type)) x + +fun unmangled_type s = + s |> suffix ")" |> raw_explode + |> Scan.finite Symbol.stopper + (Scan.error (!! (fn _ => raise Fail ("unrecognized mangled type " ^ + quote s)) parse_mangled_type)) + |> fst + +fun unmangled_const s = + let val ss = space_explode mangled_type_sep s in + (hd ss, map unmangled_type (tl ss)) + end + +fun repair_combterm_consts type_sys = + let + fun aux (CombApp tmp) = CombApp (pairself aux tmp) + | aux (CombConst (name as (s, _), ty, ty_args)) = + (case strip_prefix_and_unascii const_prefix s of + NONE => (name, ty_args) + | SOME s'' => + let val s'' = invert_const s'' in + case type_arg_policy type_sys s'' of + No_Type_Args => (name, []) + | Explicit_Type_Args => (name, ty_args) + | Mangled_Types => (mangled_const_name ty_args name, []) + end) + |> (fn (name, ty_args) => CombConst (name, ty, ty_args)) + | aux tm = tm + in aux end + +fun combformula_for_prop thy type_sys eq_as_iff = let fun do_term bs t ts = combterm_from_term thy bs (Envir.eta_contract t) + |>> repair_combterm_consts type_sys |>> AAtom ||> union (op =) ts fun do_quant bs q s T t' = let val s = Name.variant (map fst bs) s in @@ -265,7 +334,7 @@ in t |> exists_subterm is_Var t ? aux end (* making fact and conjecture formulas *) -fun make_formula ctxt eq_as_iff presimp name kind t = +fun make_formula ctxt type_sys eq_as_iff presimp name kind t = let val thy = Proof_Context.theory_of ctxt val t = t |> Envir.beta_eta_contract @@ -278,41 +347,46 @@ |> perhaps (try (HOLogic.dest_Trueprop)) |> introduce_combinators_in_term ctxt kind |> kind <> Axiom ? freeze_term - val (combformula, ctypes_sorts) = combformula_for_prop thy eq_as_iff t [] + val (combformula, ctypes_sorts) = + combformula_for_prop thy type_sys eq_as_iff t [] in {name = name, combformula = combformula, kind = kind, ctypes_sorts = ctypes_sorts} end -fun make_fact ctxt keep_trivial eq_as_iff presimp ((name, _), th) = +fun make_fact ctxt type_sys keep_trivial eq_as_iff presimp ((name, _), th) = case (keep_trivial, - make_formula ctxt eq_as_iff presimp name Axiom (prop_of th)) of + make_formula ctxt type_sys eq_as_iff presimp name Axiom (prop_of th)) of (false, {combformula = AAtom (CombConst (("c_True", _), _, _)), ...}) => NONE | (_, formula) => SOME formula -fun make_conjecture ctxt ts = +fun make_conjecture ctxt type_sys ts = let val last = length ts - 1 in - map2 (fn j => make_formula ctxt true true (string_of_int j) + map2 (fn j => make_formula ctxt type_sys true true (string_of_int j) (if j = last then Conjecture else Hypothesis)) (0 upto last) ts end (** Helper facts **) -fun fold_formula f (AQuant (_, _, phi)) = fold_formula f phi - | fold_formula f (AConn (_, phis)) = fold (fold_formula f) phis - | fold_formula f (AAtom tm) = f tm +fun formula_map f (AQuant (q, xs, phi)) = AQuant (q, xs, formula_map f phi) + | formula_map f (AConn (c, phis)) = AConn (c, map (formula_map f) phis) + | formula_map f (AAtom tm) = AAtom (f tm) + +fun formula_fold f (AQuant (_, _, phi)) = formula_fold f phi + | formula_fold f (AConn (_, phis)) = fold (formula_fold f) phis + | formula_fold f (AAtom tm) = f tm fun count_term (ATerm ((s, _), tms)) = - (if is_atp_variable s then I - else Symtab.map_entry s (Integer.add 1)) + (if is_atp_variable s then I else Symtab.map_entry s (Integer.add 1)) #> fold count_term tms -fun count_formula x = fold_formula count_term x +fun count_formula x = formula_fold count_term x val init_counters = metis_helpers |> map fst |> sort_distinct string_ord |> map (rpair 0) |> Symtab.make +(* ### FIXME: do this on repaired combterms *) fun get_helper_facts ctxt type_sys formulas = let val no_dangerous_types = type_system_types_dangerous_types type_sys @@ -321,7 +395,8 @@ fun dub c needs_full_types (th, j) = ((c ^ "_" ^ string_of_int j ^ (if needs_full_types then "ft" else ""), false), th) - fun make_facts eq_as_iff = map_filter (make_fact ctxt false eq_as_iff false) + fun make_facts eq_as_iff = + map_filter (make_fact ctxt type_sys false eq_as_iff false) in (metis_helpers |> filter (is_used o fst) @@ -346,8 +421,8 @@ []) end -fun translate_atp_fact ctxt keep_trivial = - `(make_fact ctxt keep_trivial true true) +fun translate_atp_fact ctxt type_sys keep_trivial = + `(make_fact ctxt type_sys keep_trivial true true) fun translate_formulas ctxt type_sys hyp_ts concl_t rich_facts = let @@ -366,7 +441,7 @@ val subs = tfree_classes_of_terms all_ts val supers = tvar_classes_of_terms all_ts val tycons = type_consts_of_terms thy all_ts - val conjs = make_conjecture ctxt (hyp_ts @ [concl_t]) + val conjs = make_conjecture ctxt type_sys (hyp_ts @ [concl_t]) val (supers', arity_clauses) = if type_sys = No_Types then ([], []) else make_arity_clauses thy tycons supers @@ -433,59 +508,15 @@ ("c_implies", (2, ("c_fimplies", @{const_name Metis.fimplies}))), ("equal", (2, ("c_fequal", @{const_name Metis.fequal})))] -(* We are crossing our fingers that it doesn't clash with anything else. *) -val mangled_type_sep = "\000" - -fun mangled_combtyp_component f (CombTFree name) = f name - | mangled_combtyp_component f (CombTVar name) = - f name (* FIXME: shouldn't happen *) - (* raise Fail "impossible schematic type variable" *) - | mangled_combtyp_component f (CombType (name, tys)) = - f name ^ "(" ^ commas (map (mangled_combtyp_component f) tys) ^ ")" - -fun mangled_combtyp ty = - (make_type (mangled_combtyp_component fst ty), - mangled_combtyp_component snd ty) - -fun mangled_type_suffix f g tys = - fold_rev (curry (op ^) o g o prefix mangled_type_sep - o mangled_combtyp_component f) tys "" - -fun mangled_const_fst ty_args s = s ^ mangled_type_suffix fst ascii_of ty_args -fun mangled_const_snd ty_args s' = s' ^ mangled_type_suffix snd I ty_args -fun mangled_const ty_args (s, s') = - (mangled_const_fst ty_args s, mangled_const_snd ty_args s') - -val parse_mangled_ident = - Scan.many1 (not o member (op =) ["(", ")", ","]) >> implode - -fun parse_mangled_type x = - (parse_mangled_ident - -- Scan.optional ($$ "(" |-- Scan.optional parse_mangled_types [] --| $$ ")") - [] >> ATerm) x -and parse_mangled_types x = - (parse_mangled_type ::: Scan.repeat ($$ "," |-- parse_mangled_type)) x - -fun unmangled_type s = - s |> suffix ")" |> raw_explode - |> Scan.finite Symbol.stopper - (Scan.error (!! (fn _ => raise Fail ("unrecognized mangled type " ^ - quote s)) parse_mangled_type)) - |> fst - -fun unmangled_const s = - let val ss = space_explode mangled_type_sep s in - (hd ss, map unmangled_type (tl ss)) - end - fun pred_combtyp ty = case combtyp_from_typ @{typ "unit => bool"} of CombType (name, [_, bool_ty]) => CombType (name, [ty, bool_ty]) | _ => raise Fail "expected two-argument type constructor" -fun has_type_combatom ty tm = - CombApp (CombConst ((const_prefix ^ is_base, is_base), pred_combtyp ty, [ty]), - tm) +fun type_pred_combatom type_sys ty tm = + CombApp (CombConst ((const_prefix ^ type_pred_base, type_pred_base), + pred_combtyp ty, [ty]), tm) + |> repair_combterm_consts type_sys |> AAtom fun formula_for_combformula ctxt type_sys = @@ -498,6 +529,7 @@ 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') @@ -505,16 +537,7 @@ | _ => name else fname, []) - | NONE => - case strip_prefix_and_unascii const_prefix s of - NONE => (name, ty_args) - | SOME s'' => - let val s'' = invert_const s'' in - case type_arg_policy type_sys s'' of - No_Type_Args => (name, []) - | Explicit_Type_Args => (name, ty_args) - | Mangled_Types => (mangled_const ty_args name, []) - end) + | NONE => (name, ty_args)) | CombVar (name, _) => (name, []) | CombApp _ => raise Fail "impossible \"CombApp\"" val t = ATerm (x, map fo_term_for_combtyp ty_args @ @@ -531,7 +554,7 @@ val do_out_of_bound_type = if member (op =) [Args true, Mangled true] type_sys then (fn (s, ty) => - has_type_combatom ty (CombVar (s, ty)) + type_pred_combatom type_sys ty (CombVar (s, ty)) |> formula_for_combformula ctxt type_sys |> SOME) else K NONE @@ -553,6 +576,7 @@ (atp_type_literals_for_types type_sys Axiom ctypes_sorts)) (formula_for_combformula ctxt type_sys (close_combformula_universally combformula)) + |> close_formula_universally fun logic_for_type_sys Many_Typed = Tff | logic_for_type_sys _ = Fof @@ -568,11 +592,11 @@ fun problem_line_for_class_rel_clause (ClassRelClause {name, subclass, superclass, ...}) = - let val ty_arg = ATerm (("T", "T"), []) in + let val ty_arg = ATerm (`I "T", []) in Formula (Fof, class_rel_clause_prefix ^ ascii_of name, Axiom, AConn (AImplies, [AAtom (ATerm (subclass, [ty_arg])), - AAtom (ATerm (superclass, [ty_arg]))]), - NONE, NONE) + AAtom (ATerm (superclass, [ty_arg]))]) + |> close_formula_universally, NONE, NONE) end fun fo_literal_for_arity_literal (TConsLit (c, t, args)) = @@ -586,14 +610,15 @@ mk_ahorn (map (formula_for_fo_literal o apfst not o fo_literal_for_arity_literal) premLits) (formula_for_fo_literal - (fo_literal_for_arity_literal conclLit)), NONE, NONE) + (fo_literal_for_arity_literal conclLit)) + |> close_formula_universally, NONE, NONE) fun problem_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 - (close_combformula_universally combformula), - NONE, NONE) + (close_combformula_universally combformula) + |> close_formula_universally, NONE, NONE) fun free_type_literals type_sys ({ctypes_sorts, ...} : translated_formula) = ctypes_sorts |> atp_type_literals_for_types type_sys Conjecture @@ -610,40 +635,42 @@ (** "hBOOL" and "hAPP" **) -type sym_info = {min_arity: int, max_arity: int, fun_sym: bool} +type hrepair_info = {min_arity: int, max_arity: int, pred_sym: bool} -fun consider_term_syms top_level (ATerm ((s, _), ts)) = - (if is_atp_variable s then - I - else - let val n = length ts in - Symtab.map_default - (s, {min_arity = n, max_arity = 0, fun_sym = false}) - (fn {min_arity, max_arity, fun_sym} => - {min_arity = Int.min (n, min_arity), - max_arity = Int.max (n, max_arity), - fun_sym = fun_sym orelse not top_level}) - end) - #> fold (consider_term_syms (top_level andalso s = type_tag_name)) ts -val consider_formula_syms = fold_formula (consider_term_syms true) +fun consider_combterm_for_hrepair top_level tm = + let val (head, args) = strip_combterm_comb tm in + (case head of + CombConst ((s, _), _, _) => + if String.isPrefix bound_var_prefix s then + I + else + let val n = length args in + Symtab.map_default + (s, {min_arity = n, max_arity = 0, pred_sym = true}) + (fn {min_arity, max_arity, pred_sym} => + {min_arity = Int.min (n, min_arity), + max_arity = Int.max (n, max_arity), + pred_sym = pred_sym andalso top_level}) + end + | _ => I) + #> fold (consider_combterm_for_hrepair false) args + end -fun consider_problem_line_syms (Type_Decl _) = I - | consider_problem_line_syms (Formula (_, _, _, phi, _, _)) = - consider_formula_syms phi -fun consider_problem_syms problem = - fold (fold consider_problem_line_syms o snd) problem +fun consider_fact_for_hrepair ({combformula, ...} : translated_formula) = + formula_fold (consider_combterm_for_hrepair true) combformula (* The "equal" entry is needed for helper facts if the problem otherwise does not involve equality. *) val default_entries = - [("equal", {min_arity = 2, max_arity = 2, fun_sym = false})] + [("equal", {min_arity = 2, max_arity = 2, pred_sym = true}), + (boolify_name, {min_arity = 1, max_arity = 1, pred_sym = true})] -fun sym_table_for_problem explicit_apply problem = +fun hrepair_table_for_facts explicit_apply facts = if explicit_apply then NONE else SOME (Symtab.empty |> fold Symtab.default default_entries - |> consider_problem_syms problem) + |> fold consider_fact_for_hrepair facts) fun min_arity_of thy type_sys NONE s = (if s = "equal" orelse s = type_tag_name orelse @@ -654,9 +681,9 @@ SOME s' => s' |> unmangled_const |> fst |> invert_const |> num_atp_type_args thy type_sys | NONE => 0) - | min_arity_of _ _ (SOME sym_tab) s = - case Symtab.lookup sym_tab s of - SOME ({min_arity, ...} : sym_info) => min_arity + | min_arity_of _ _ (SOME hrepairs) s = + case Symtab.lookup hrepairs s of + SOME ({min_arity, ...} : hrepair_info) => min_arity | NONE => 0 fun full_type_of (ATerm ((s, _), [ty, _])) = @@ -676,7 +703,7 @@ end | NONE => list_hAPP_rev NONE t1 (t2 :: ts2) -fun repair_applications_in_term thy type_sys sym_tab = +fun hrepair_applications_in_term thy type_sys hrepairs = let fun aux opt_ty (ATerm (name as (s, _), ts)) = if s = type_tag_name then @@ -686,12 +713,10 @@ else let val ts = map (aux NONE) ts - val (ts1, ts2) = chop (min_arity_of thy type_sys sym_tab s) ts + val (ts1, ts2) = chop (min_arity_of thy type_sys hrepairs s) ts in list_hAPP_rev opt_ty (ATerm (name, ts1)) (rev ts2) end in aux NONE end -fun boolify t = ATerm (`I boolify_name, [t]) - (* True if the constant ever appears outside of the top-level position in literals, or if it appears with different arities (e.g., because of different type instantiations). If false, the constant always receives all of its @@ -699,63 +724,52 @@ fun is_pred_sym NONE s = s = "equal" orelse s = "$false" orelse s = "$true" orelse String.isPrefix type_const_prefix s orelse String.isPrefix class_prefix s - | is_pred_sym (SOME sym_tab) s = - case Symtab.lookup sym_tab s of - SOME {min_arity, max_arity, fun_sym} => - not fun_sym andalso min_arity = max_arity + | is_pred_sym (SOME hrepairs) s = + case Symtab.lookup hrepairs s of + SOME {min_arity, max_arity, pred_sym} => + pred_sym andalso min_arity = max_arity | NONE => false -fun repair_predicates_in_term pred_sym_tab (t as ATerm ((s, _), ts)) = - if s = type_tag_name then - case ts of - [_, t' as ATerm ((s', _), _)] => - if is_pred_sym pred_sym_tab s' then t' else boolify t - | _ => raise Fail "malformed type tag" - else - t |> not (is_pred_sym pred_sym_tab s) ? boolify +val boolify_combconst = + CombConst (`I boolify_name, combtyp_from_typ @{typ "bool => bool"}, []) +fun boolify tm = CombApp (boolify_combconst, tm) + +fun hrepair_pred_syms_in_combterm hrepairs tm = + case strip_combterm_comb tm of + (CombConst ((s, _), _, _), _) => + if is_pred_sym hrepairs s then tm else boolify tm + | _ => boolify tm + +fun hrepair_apps_in_combterm hrepairs tm = tm -fun repair_formula thy type_sys sym_tab = - let - val pred_sym_tab = case type_sys of Tags _ => NONE | _ => sym_tab - fun aux (AQuant (q, xs, phi)) = AQuant (q, xs, aux phi) - | aux (AConn (c, phis)) = AConn (c, map aux phis) - | aux (AAtom tm) = - AAtom (tm |> repair_applications_in_term thy type_sys sym_tab - |> repair_predicates_in_term pred_sym_tab) - in aux #> close_formula_universally end +fun hrepair_combterm type_sys hrepairs = + (case type_sys of Tags _ => I | _ => hrepair_pred_syms_in_combterm hrepairs) + #> hrepair_apps_in_combterm hrepairs +val hrepair_combformula = formula_map oo hrepair_combterm +val hrepair_fact = map_combformula oo hrepair_combformula -fun repair_problem_line thy type_sys sym_tab - (Formula (logic, ident, kind, phi, source, useful_info)) = - Formula (logic, ident, kind, repair_formula thy type_sys sym_tab phi, - source, useful_info) - | repair_problem_line _ _ _ _ = raise Fail "unexpected non-formula" -fun repair_problem thy = map o apsnd o map oo repair_problem_line thy +fun is_const_relevant type_sys hrepairs s = + not (String.isPrefix bound_var_prefix s) andalso s <> "equal" andalso + (type_sys = Many_Typed orelse not (is_pred_sym hrepairs s)) -fun is_const_relevant type_sys sym_tab unmangled_s s = - not (String.isPrefix bound_var_prefix unmangled_s) andalso - unmangled_s <> "equal" andalso - (type_sys = Many_Typed orelse not (is_pred_sym sym_tab s)) - -fun consider_combterm_consts type_sys sym_tab tm = +fun consider_combterm_consts type_sys hrepairs tm = let val (head, args) = strip_combterm_comb tm in (case head of CombConst ((s, s'), ty, ty_args) => (* FIXME: exploit type subsumption *) - is_const_relevant type_sys sym_tab s - (s |> member (op =) [Many_Typed, Mangled true] type_sys - ? mangled_const_fst ty_args) + is_const_relevant type_sys hrepairs s ? Symtab.insert_list (op =) (s, (s', ty_args, ty)) | _ => I) (* FIXME: hAPP on var *) - #> fold (consider_combterm_consts type_sys sym_tab) args + #> fold (consider_combterm_consts type_sys hrepairs) args end -fun consider_fact_consts type_sys sym_tab +fun consider_fact_consts type_sys hrepairs ({combformula, ...} : translated_formula) = - fold_formula (consider_combterm_consts type_sys sym_tab) combformula + formula_fold (consider_combterm_consts type_sys hrepairs) combformula -fun const_table_for_facts type_sys sym_tab facts = +fun const_table_for_facts type_sys hrepairs facts = Symtab.empty |> member (op =) [Many_Typed, Args true, Mangled true] type_sys - ? fold (consider_fact_consts type_sys sym_tab) facts + ? fold (consider_fact_consts type_sys hrepairs) facts fun strip_and_map_combtyp f (ty as CombType ((s, _), tys)) = (case (strip_prefix_and_unascii type_const_prefix s, tys) of @@ -764,14 +778,14 @@ | _ => ([], f ty)) | strip_and_map_combtyp f ty = ([], f ty) -fun type_decl_line_for_const_entry ctxt type_sys sym_tab s (s', ty_args, ty) = +fun type_decl_line_for_const_entry ctxt type_sys hrepairs s (s', ty_args, ty) = if type_sys = Many_Typed then let val (arg_tys, res_ty) = strip_and_map_combtyp mangled_combtyp ty - val (s, s') = (s, s') |> mangled_const ty_args + val (s, s') = (s, s') |> mangled_const_name ty_args in Type_Decl (type_decl_prefix ^ ascii_of s, (s, s'), arg_tys, - if is_pred_sym sym_tab s then `I tff_bool_type else res_ty) + if is_pred_sym hrepairs s then `I tff_bool_type else res_ty) end else let @@ -783,21 +797,15 @@ map (fn (name, ty) => CombConst (name, the ty, [])) bounds in Formula (Fof, type_decl_prefix ^ ascii_of s, Axiom, - mk_aquant AForall bounds - (has_type_combatom res_ty - (fold (curry (CombApp o swap)) bound_tms - (CombConst ((s, s'), ty, ty_args)))) + CombConst ((s, s'), ty, ty_args) + |> fold (curry (CombApp o swap)) bound_tms + |> type_pred_combatom type_sys res_ty + |> mk_aquant AForall bounds |> formula_for_combformula ctxt type_sys, NONE, NONE) end -fun type_decl_lines_for_const ctxt type_sys sym_tab (s, xs) = - map (type_decl_line_for_const_entry ctxt type_sys sym_tab s) xs - -fun add_extra_type_decl_lines Many_Typed = - cons (Type_Decl (type_decl_prefix ^ boolify_name, `I boolify_name, - [mangled_combtyp (combtyp_from_typ @{typ bool})], - `I tff_bool_type)) - | add_extra_type_decl_lines _ = I +fun type_decl_lines_for_const ctxt type_sys hrepairs (s, xs) = + map (type_decl_line_for_const_entry ctxt type_sys hrepairs s) xs val type_declsN = "Type declarations" val factsN = "Relevant facts" @@ -815,9 +823,11 @@ fun prepare_atp_problem ctxt readable_names type_sys explicit_apply hyp_ts concl_t facts = let - val thy = Proof_Context.theory_of ctxt val (fact_names, (conjs, facts, class_rel_clauses, arity_clauses)) = translate_formulas ctxt type_sys hyp_ts concl_t facts + val hrepairs = hrepair_table_for_facts explicit_apply (conjs @ facts) + val conjs = map (hrepair_fact type_sys hrepairs) conjs + val facts = map (hrepair_fact type_sys hrepairs) facts (* Reordering these might confuse the proof reconstruction code or the SPASS Flotter hack. *) val problem = @@ -829,22 +839,19 @@ (helpersN, []), (conjsN, map (problem_line_for_conjecture ctxt type_sys) conjs), (free_typesN, problem_lines_for_free_types type_sys (facts @ conjs))] - val sym_tab = sym_table_for_problem explicit_apply problem - val problem = problem |> repair_problem thy type_sys sym_tab val helper_facts = problem |> maps (map_filter (fn Formula (_, _, _, phi, _, _) => SOME phi | _ => NONE) o snd) |> get_helper_facts ctxt type_sys - val const_tab = const_table_for_facts type_sys sym_tab (conjs @ facts) + |>> map (hrepair_fact type_sys hrepairs) + val const_tab = const_table_for_facts type_sys hrepairs (conjs @ facts) val type_decl_lines = - Symtab.fold_rev (append o type_decl_lines_for_const ctxt type_sys sym_tab) + Symtab.fold_rev (append o type_decl_lines_for_const ctxt type_sys + hrepairs) const_tab [] - |> add_extra_type_decl_lines type_sys val helper_lines = helper_facts - |>> map (pair 0 - #> problem_line_for_fact ctxt helper_prefix type_sys - #> repair_problem_line thy type_sys sym_tab) + |>> map (pair 0 #> problem_line_for_fact ctxt helper_prefix type_sys) |> op @ val (problem, pool) = problem |> fold (AList.update (op =)) @@ -868,7 +875,7 @@ (not (is_atp_variable s) andalso s <> "equal") ? Symtab.default (s, weight) #> fold (add_term_weights weight) tms fun add_problem_line_weights weight (Formula (_, _, _, phi, _, _)) = - fold_formula (add_term_weights weight) phi + formula_fold (add_term_weights weight) phi | add_problem_line_weights _ _ = I fun add_conjectures_weights [] = I diff -r 8938507b2054 -r 024920b65ce2 src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML --- a/src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML Sun May 01 18:37:24 2011 +0200 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML Sun May 01 18:37:24 2011 +0200 @@ -313,9 +313,9 @@ fun untranslated_fact (Untranslated_Fact p) = p | untranslated_fact (ATP_Translated_Fact (_, p)) = p | untranslated_fact (SMT_Weighted_Fact (info, (_, th))) = (info, th) -fun atp_translated_fact _ (ATP_Translated_Fact p) = p - | atp_translated_fact ctxt fact = - translate_atp_fact ctxt false (untranslated_fact fact) +fun atp_translated_fact _ _ (ATP_Translated_Fact p) = p + | atp_translated_fact ctxt type_sys fact = + translate_atp_fact ctxt type_sys false (untranslated_fact fact) fun smt_weighted_fact _ _ (SMT_Weighted_Fact p, _) = p | smt_weighted_fact thy num_facts (fact, j) = (untranslated_fact fact, j) |> weight_smt_fact thy num_facts @@ -415,7 +415,7 @@ ? filter_out (member (op =) blacklist o fst o untranslated_fact) |> monomorphize ? monomorphize_facts - |> map (atp_translated_fact ctxt) + |> map (atp_translated_fact ctxt type_sys) val real_ms = Real.fromInt o Time.toMilliseconds val slice_timeout = ((real_ms time_left diff -r 8938507b2054 -r 024920b65ce2 src/HOL/Tools/Sledgehammer/sledgehammer_run.ML --- a/src/HOL/Tools/Sledgehammer/sledgehammer_run.ML Sun May 01 18:37:24 2011 +0200 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_run.ML Sun May 01 18:37:24 2011 +0200 @@ -250,7 +250,8 @@ (if monomorphize then K (Untranslated_Fact o fst) else - ATP_Translated_Fact oo K (translate_atp_fact ctxt false o fst)) + ATP_Translated_Fact + oo K (translate_atp_fact ctxt type_sys false o fst)) (K (K NONE)) atps fun launch_smts accum = if null smts then