# HG changeset patch # User blanchet # Date 1304267845 -7200 # Node ID 0864acec9f72e567d2097c59592b60213c345b1f # Parent 744215c3e90cd8b98973c6bc3bf1be8206d75a68 tuning diff -r 744215c3e90c -r 0864acec9f72 src/HOL/Tools/Sledgehammer/sledgehammer_atp_translate.ML --- a/src/HOL/Tools/Sledgehammer/sledgehammer_atp_translate.ML Sun May 01 18:37:25 2011 +0200 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_atp_translate.ML Sun May 01 18:37:25 2011 +0200 @@ -114,9 +114,13 @@ fun type_system_types_dangerous_types (Tags _) = true | type_system_types_dangerous_types type_sys = is_type_system_sound type_sys -fun should_introduce_type_preds (Mangled true) = true - | should_introduce_type_preds (Args true) = true - | should_introduce_type_preds _ = false +fun type_system_introduces_type_preds (Mangled true) = true + | type_system_introduces_type_preds (Args true) = true + | type_system_introduces_type_preds _ = false + +fun type_system_declares_sym_types Many_Typed = true + | type_system_declares_sym_types type_sys = + type_system_introduces_type_preds type_sys val boring_consts = [explicit_app_base, @{const_name Metis.fequal}] @@ -177,7 +181,7 @@ fun combterm_vars (CombApp (tm1, tm2)) = fold combterm_vars [tm1, tm2] | combterm_vars (CombConst _) = I - | combterm_vars (CombVar (name, ty)) = insert (op =) (name, SOME ty) + | combterm_vars (CombVar (name, T)) = insert (op =) (name, SOME T) val close_combformula_universally = close_universally combterm_vars fun term_vars (ATerm (name as (s, _), tms)) = @@ -203,9 +207,9 @@ #> (fn ty => (make_tff_type (generic_mangled_type_name fst ty), generic_mangled_type_name snd ty)) -fun generic_mangled_type_suffix f g tys = +fun generic_mangled_type_suffix f g Ts = fold_rev (curry (op ^) o g o prefix mangled_type_sep - o generic_mangled_type_name f) tys "" + o generic_mangled_type_name f) Ts "" fun mangled_const_name T_args (s, s') = let val ty_args = map fo_term_from_typ T_args in (s ^ generic_mangled_type_suffix fst ascii_of ty_args, @@ -239,7 +243,7 @@ let fun aux top_level (CombApp (tm1, tm2)) = CombApp (aux top_level tm1, aux false tm2) - | aux top_level (CombConst (name as (s, s'), ty, ty_args)) = + | aux top_level (CombConst (name as (s, s'), T, T_args)) = (case proxify_const s of SOME proxy_base => if top_level then @@ -248,9 +252,9 @@ | "c_True" => (tptp_true, s') | _ => name, []) else - (proxy_base |>> prefix const_prefix, ty_args) - | NONE => (name, ty_args)) - |> (fn (name, ty_args) => CombConst (name, ty, ty_args)) + (proxy_base |>> prefix const_prefix, T_args) + | NONE => (name, T_args)) + |> (fn (name, T_args) => CombConst (name, T, T_args)) | aux _ tm = tm in aux true end @@ -399,10 +403,10 @@ (** "hBOOL" and "hAPP" **) -type sym_table_info = +type sym_info = {pred_sym : bool, min_ary : int, max_ary : int, typ : typ option} -fun add_combterm_to_sym_table explicit_apply = +fun add_combterm_syms_to_table explicit_apply = let fun aux top_level tm = let val (head, args) = strip_combterm_comb tm in @@ -426,8 +430,8 @@ #> fold (aux false) args end in aux true end - -val add_fact_to_sym_table = fact_lift o formula_fold o add_combterm_to_sym_table +val add_fact_syms_to_table = + fact_lift o formula_fold o add_combterm_syms_to_table val default_sym_table_entries = [("equal", {pred_sym = true, min_ary = 2, max_ary = 2, typ = NONE}), @@ -438,11 +442,11 @@ fun sym_table_for_facts explicit_apply facts = Symtab.empty |> fold Symtab.default default_sym_table_entries - |> fold (add_fact_to_sym_table explicit_apply) facts + |> fold (add_fact_syms_to_table explicit_apply) facts fun min_arity_of sym_tab s = case Symtab.lookup sym_tab s of - SOME ({min_ary, ...} : sym_table_info) => min_ary + SOME ({min_ary, ...} : sym_info) => min_ary | NONE => case strip_prefix_and_unascii const_prefix s of SOME s => @@ -460,7 +464,8 @@ arguments and is used as a predicate. *) fun is_pred_sym sym_tab s = case Symtab.lookup sym_tab s of - SOME {pred_sym, min_ary, max_ary, ...} => pred_sym andalso min_ary = max_ary + SOME ({pred_sym, min_ary, max_ary, ...} : sym_info) => + pred_sym andalso min_ary = max_ary | NONE => false val predicator_combconst = @@ -500,17 +505,17 @@ fun impose_type_arg_policy_in_combterm type_sys = let fun aux (CombApp tmp) = CombApp (pairself aux tmp) - | aux (CombConst (name as (s, _), ty, ty_args)) = + | aux (CombConst (name as (s, _), T, T_args)) = (case strip_prefix_and_unascii const_prefix s of - NONE => (name, ty_args) + NONE => (name, T_args) | SOME s'' => let val s'' = invert_const s'' in case type_arg_policy type_sys s'' of No_Type_Args => (name, []) - | Mangled_Types => (mangled_const_name ty_args name, []) - | Explicit_Type_Args => (name, ty_args) + | Mangled_Types => (mangled_const_name T_args name, []) + | Explicit_Type_Args => (name, T_args) end) - |> (fn (name, ty_args) => CombConst (name, ty, ty_args)) + |> (fn (name, T_args) => CombConst (name, T, T_args)) | aux tm = tm in aux end @@ -532,7 +537,7 @@ |> close_formula_universally, NONE, NONE) end -fun helper_facts_for_sym ctxt type_sys (s, {typ, ...} : sym_table_info) = +fun helper_facts_for_sym ctxt type_sys (s, {typ, ...} : sym_info) = case strip_prefix_and_unascii const_prefix s of SOME mangled_s => let @@ -595,7 +600,7 @@ (fact_names |> map single, (conjs, facts, class_rel_clauses, arity_clauses)) end -fun tag_with_type ty t = ATerm (`I type_tag_name, [ty, t]) +fun tag_with_type ty tm = ATerm (`I type_tag_name, [ty, tm]) fun fo_literal_from_type_literal (TyLitVar (class, name)) = (true, ATerm (class, [ATerm (name, [])])) @@ -643,36 +648,35 @@ fun do_term top_level u = let val (head, args) = strip_combterm_comb u - val (x, ty_args) = + val (x, T_args) = case head of - CombConst (name, _, ty_args) => (name, ty_args) + CombConst (name, _, T_args) => (name, T_args) | CombVar (name, _) => (name, []) | CombApp _ => raise Fail "impossible \"CombApp\"" - val t = ATerm (x, map fo_term_from_typ ty_args @ + val t = ATerm (x, map fo_term_from_typ T_args @ map (do_term false) args) - val ty = combtyp_of u + val T = combtyp_of u in - t |> (if not top_level andalso - should_tag_with_type ctxt type_sys ty then - tag_with_type (fo_term_from_typ ty) + t |> (if not top_level andalso should_tag_with_type ctxt type_sys T then + tag_with_type (fo_term_from_typ T) else I) end val do_bound_type = if type_sys = Many_Typed then SOME o mangled_type_name else K NONE fun do_out_of_bound_type (s, T) = - if should_introduce_type_preds type_sys then + if type_system_introduces_type_preds type_sys then type_pred_combatom type_sys T (CombVar (s, T)) |> do_formula |> SOME else NONE and do_formula (AQuant (q, xs, phi)) = AQuant (q, xs |> map (apsnd (fn NONE => NONE - | SOME ty => do_bound_type ty)), + | SOME T => do_bound_type T)), (if q = AForall then mk_ahorn else fold_rev (mk_aconn AAnd)) (map_filter (fn (_, NONE) => NONE - | (s, SOME ty) => do_out_of_bound_type (s, ty)) xs) + | (s, SOME T) => do_out_of_bound_type (s, T)) xs) (do_formula phi)) | do_formula (AConn (c, phis)) = AConn (c, map do_formula phis) | do_formula (AAtom tm) = AAtom (do_term true tm) @@ -743,70 +747,74 @@ (** Symbol declarations **) -fun is_const_relevant type_sys sym_tab s = +fun should_declare_sym type_sys pred_sym s = not (String.isPrefix bound_var_prefix s) andalso s <> "equal" andalso - (type_sys = Many_Typed orelse not (is_pred_sym sym_tab s)) + (type_sys = Many_Typed orelse not pred_sym) -fun consider_combterm_consts type_sys sym_tab 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 - ? Symtab.insert_list (op =) (s, (s', ty_args, ty)) - | _ => I) - #> fold (consider_combterm_consts type_sys sym_tab) args - end +fun add_combterm_syms_to_decl_table type_sys repaired_sym_tab = + let + fun aux tm = + let val (head, args) = strip_combterm_comb tm in + (case head of + CombConst ((s, s'), T, T_args) => + let val pred_sym = is_pred_sym repaired_sym_tab s in + if should_declare_sym type_sys pred_sym s then + Symtab.insert_list (op =) + (s, (s', T_args, T, pred_sym, length args)) + else + I + end + | _ => I) + #> fold aux args + end + in aux end +fun add_fact_syms_to_decl_table type_sys repaired_sym_tab = + fact_lift (formula_fold + (add_combterm_syms_to_decl_table type_sys repaired_sym_tab)) +fun sym_decl_table_for_facts type_sys repaired_sym_tab facts = + Symtab.empty |> type_system_declares_sym_types type_sys + ? fold (add_fact_syms_to_decl_table type_sys repaired_sym_tab) + facts -fun consider_fact_consts type_sys sym_tab = - fact_lift (formula_fold (consider_combterm_consts type_sys sym_tab)) - -(* FIXME: needed? *) -fun typed_const_table_for_facts type_sys sym_tab facts = - Symtab.empty |> member (op =) [Many_Typed, Mangled true, Args true] type_sys - ? fold (consider_fact_consts type_sys sym_tab) facts - -fun strip_and_map_type 0 f T = ([], f T) - | strip_and_map_type n f (Type (@{type_name fun}, [dom_T, ran_T])) = - strip_and_map_type (n - 1) f ran_T |>> cons (f dom_T) - | strip_and_map_type _ _ _ = raise Fail "unexpected non-function" +fun n_ary_strip_type 0 T = ([], T) + | n_ary_strip_type n (Type (@{type_name fun}, [dom_T, ran_T])) = + n_ary_strip_type (n - 1) ran_T |>> cons dom_T + | n_ary_strip_type _ _ = raise Fail "unexpected non-function" -fun problem_line_for_typed_const ctxt type_sys sym_tab s n j (s', ty_args, T) = - let val ary = min_arity_of sym_tab s in - if type_sys = Many_Typed then - let val (arg_Ts, res_T) = strip_and_map_type ary mangled_type_name T in - Decl (sym_decl_prefix ^ ascii_of s, (s, s'), arg_Ts, - (* ### FIXME: put that in typed_const_tab *) - if is_pred_sym sym_tab s then `I tptp_tff_bool_type else res_T) - end - else - let - val (arg_Ts, res_T) = strip_and_map_type ary I T - val bound_names = - 1 upto length arg_Ts |> map (`I o make_bound_var o string_of_int) - val bound_tms = - bound_names ~~ arg_Ts |> map (fn (name, T) => CombConst (name, T, [])) - val bound_Ts = arg_Ts |> map (if n > 1 then SOME else K NONE) - val freshener = - case type_sys of Args _ => string_of_int j ^ "_" | _ => "" - in - Formula (Fof, sym_decl_prefix ^ freshener ^ "_" ^ ascii_of s, Axiom, - CombConst ((s, s'), T, ty_args) - |> fold (curry (CombApp o swap)) bound_tms - |> type_pred_combatom type_sys res_T - |> mk_aquant AForall (bound_names ~~ bound_Ts) - |> formula_from_combformula ctxt type_sys, - NONE, NONE) - end +fun problem_line_for_sym_decl ctxt type_sys s n j + (s', T_args, T, pred_sym, ary) = + if type_sys = Many_Typed then + let val (arg_Ts, res_T) = n_ary_strip_type ary T in + Decl (sym_decl_prefix ^ ascii_of s, (s, s'), + map mangled_type_name arg_Ts, + if pred_sym then `I tptp_tff_bool_type else mangled_type_name res_T) + end + else + let + val (arg_Ts, res_T) = n_ary_strip_type ary T + val bound_names = + 1 upto length arg_Ts |> map (`I o make_bound_var o string_of_int) + val bound_tms = + bound_names ~~ arg_Ts |> map (fn (name, T) => CombConst (name, T, [])) + val bound_Ts = arg_Ts |> map (if n > 1 then SOME else K NONE) + val freshener = + case type_sys of Args _ => string_of_int j ^ "_" | _ => "" + in + Formula (Fof, sym_decl_prefix ^ freshener ^ "_" ^ ascii_of s, Axiom, + CombConst ((s, s'), T, T_args) + |> fold (curry (CombApp o swap)) bound_tms + |> type_pred_combatom type_sys res_T + |> mk_aquant AForall (bound_names ~~ bound_Ts) + |> formula_from_combformula ctxt type_sys, + NONE, NONE) + end +fun problem_lines_for_sym_decls ctxt type_sys (s, decls) = + let val n = length decls in + map2 (problem_line_for_sym_decl ctxt type_sys s n) (0 upto n - 1) decls end -fun problem_lines_for_sym_decl ctxt type_sys sym_tab (s, xs) = - let val n = length xs in - map2 (problem_line_for_typed_const ctxt type_sys sym_tab s n) - (0 upto n - 1) xs - end -fun problem_lines_for_sym_decls ctxt type_sys sym_tab typed_const_tab = - Symtab.fold_rev (append o problem_lines_for_sym_decl ctxt type_sys sym_tab) - typed_const_tab [] +fun problem_lines_for_sym_decl_table ctxt type_sys sym_decl_tab = + Symtab.fold_rev (append o problem_lines_for_sym_decls ctxt type_sys) + sym_decl_tab [] fun add_tff_types_in_formula (AQuant (_, xs, phi)) = union (op =) (map_filter snd xs) #> add_tff_types_in_formula phi @@ -847,11 +855,10 @@ val (conjs, facts) = (conjs, facts) |> pairself (map (repair_fact type_sys sym_tab)) val repaired_sym_tab = conjs @ facts |> sym_table_for_facts false - val typed_const_tab = - conjs @ facts |> typed_const_table_for_facts type_sys repaired_sym_tab val sym_decl_lines = - typed_const_tab - |> problem_lines_for_sym_decls ctxt type_sys repaired_sym_tab + conjs @ facts + |> sym_decl_table_for_facts type_sys repaired_sym_tab + |> problem_lines_for_sym_decl_table ctxt type_sys val helpers = helper_facts_for_sym_table ctxt type_sys repaired_sym_tab |> map (repair_fact type_sys sym_tab)