# HG changeset patch # User blanchet # Date 1304267845 -7200 # Node ID 744215c3e90cd8b98973c6bc3bf1be8206d75a68 # Parent 0c9a947b43fcf97924011cc189cd8c9a9630093e got rid of one "sym_table" in "prepare_atp_problem" now that proxies are always handled first, and tuned accordingly diff -r 0c9a947b43fc -r 744215c3e90c 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 @@ -77,6 +77,14 @@ (* Freshness almost guaranteed! *) val sledgehammer_weak_prefix = "Sledgehammer:" +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 + type translated_formula = {name: string, kind: formula_kind, @@ -106,6 +114,10 @@ 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 + val boring_consts = [explicit_app_base, @{const_name Metis.fequal}] fun should_omit_type_args type_sys s = @@ -385,260 +397,11 @@ (0 upto last) ts end -(** Helper facts **) - -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 +(** "hBOOL" and "hAPP" **) type sym_table_info = {pred_sym : bool, min_ary : int, max_ary : int, typ : typ option} -fun ti_ti_helper_fact () = - let - fun var s = ATerm (`I s, []) - fun tag tm = ATerm (`I type_tag_name, [var "X", tm]) - in - Formula (Fof, helper_prefix ^ ascii_of "ti_ti", Axiom, - AAtom (ATerm (`I "equal", [tag (tag (var "Y")), tag (var "Y")])) - |> close_formula_universally, NONE, NONE) - end - -fun helper_facts_for_sym ctxt type_sys (s, {typ, ...} : sym_table_info) = - case strip_prefix_and_unascii const_prefix s of - SOME mangled_s => - let - val thy = Proof_Context.theory_of ctxt - val unmangled_s = mangled_s |> unmangled_const_name - fun dub_and_inst c needs_full_types (th, j) = - ((c ^ "_" ^ string_of_int j ^ (if needs_full_types then "ft" else ""), - false), - let val t = th |> prop_of in - t |> (general_type_arg_policy type_sys = Mangled_Types andalso - not (null (Term.hidden_polymorphism t))) - ? (case typ of - SOME T => specialize_type thy (invert_const unmangled_s, T) - | NONE => I) - end) - fun make_facts eq_as_iff = - map_filter (make_fact ctxt false eq_as_iff false) - in - metis_helpers - |> maps (fn (metis_s, (needs_full_types, ths)) => - if metis_s <> unmangled_s orelse - (needs_full_types andalso - not (type_system_types_dangerous_types type_sys)) then - [] - else - ths ~~ (1 upto length ths) - |> map (dub_and_inst mangled_s needs_full_types) - |> make_facts (not needs_full_types)) - end - | NONE => [] -fun helper_facts_for_sym_table ctxt type_sys sym_tab = - Symtab.fold_rev (append o helper_facts_for_sym ctxt type_sys) sym_tab [] - -fun translate_atp_fact ctxt keep_trivial = - `(make_fact ctxt keep_trivial true true o apsnd prop_of) - -fun translate_formulas ctxt type_sys hyp_ts concl_t rich_facts = - let - val thy = Proof_Context.theory_of ctxt - val fact_ts = map (prop_of o snd o snd) rich_facts - val (facts, fact_names) = - rich_facts - |> map_filter (fn (NONE, _) => NONE - | (SOME fact, (name, _)) => SOME (fact, name)) - |> ListPair.unzip - (* Remove existing facts from the conjecture, as this can dramatically - boost an ATP's performance (for some reason). *) - val hyp_ts = hyp_ts |> filter_out (member (op aconv) fact_ts) - val goal_t = Logic.list_implies (hyp_ts, concl_t) - val all_ts = goal_t :: fact_ts - 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 (supers', arity_clauses) = - if type_sys = No_Types then ([], []) - else make_arity_clauses thy tycons supers - val class_rel_clauses = make_class_rel_clauses thy subs supers' - in - (fact_names |> map single, (conjs, facts, class_rel_clauses, arity_clauses)) - end - -fun impose_type_arg_policy 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, []) - | Mangled_Types => (mangled_const_name ty_args name, []) - | Explicit_Type_Args => (name, ty_args) - end) - |> (fn (name, ty_args) => CombConst (name, ty, ty_args)) - | aux tm = tm - in aux end -val impose_type_arg_policy_on_fact = - update_combformula o formula_map o impose_type_arg_policy - -fun tag_with_type ty t = ATerm (`I type_tag_name, [ty, t]) - -fun fo_literal_from_type_literal (TyLitVar (class, name)) = - (true, ATerm (class, [ATerm (name, [])])) - | fo_literal_from_type_literal (TyLitFree (class, name)) = - (true, ATerm (class, [ATerm (name, [])])) - -fun formula_from_fo_literal (pos, t) = AAtom t |> not pos ? mk_anot - -(* Finite types such as "unit", "bool", "bool * bool", and "bool => bool" are - considered dangerous because their "exhaust" properties can easily lead to - unsound ATP proofs. The checks below are an (unsound) approximation of - finiteness. *) - -fun is_dtyp_dangerous _ (Datatype_Aux.DtTFree _) = true - | is_dtyp_dangerous ctxt (Datatype_Aux.DtType (s, Us)) = - is_type_constr_dangerous ctxt s andalso forall (is_dtyp_dangerous ctxt) Us - | is_dtyp_dangerous _ (Datatype_Aux.DtRec _) = false -and is_type_dangerous ctxt (Type (s, Ts)) = - is_type_constr_dangerous ctxt s andalso forall (is_type_dangerous ctxt) Ts - | is_type_dangerous _ _ = false -and is_type_constr_dangerous ctxt s = - let val thy = Proof_Context.theory_of ctxt in - case Datatype_Data.get_info thy s of - SOME {descr, ...} => - forall (fn (_, (_, _, constrs)) => - forall (forall (is_dtyp_dangerous ctxt) o snd) constrs) descr - | NONE => - case Typedef.get_info ctxt s of - ({rep_type, ...}, _) :: _ => is_type_dangerous ctxt rep_type - | [] => true - end - -fun should_tag_with_type ctxt (Tags full_types) T = - full_types orelse is_type_dangerous ctxt T - | should_tag_with_type _ _ _ = false - -fun type_pred_combatom type_sys T tm = - CombApp (CombConst (`make_fixed_const type_pred_base, T --> @{typ bool}, [T]), - tm) - |> impose_type_arg_policy type_sys - |> AAtom - -fun formula_from_combformula ctxt type_sys = - let - fun do_term top_level u = - let - val (head, args) = strip_combterm_comb u - val (x, ty_args) = - case head of - CombConst (name, _, ty_args) => (name, ty_args) - | CombVar (name, _) => (name, []) - | CombApp _ => raise Fail "impossible \"CombApp\"" - val t = ATerm (x, map fo_term_from_typ ty_args @ - map (do_term false) args) - val ty = 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) - else - I) - end - val do_bound_type = - if type_sys = Many_Typed then SOME o mangled_type_name else K NONE - val do_out_of_bound_type = - if member (op =) [Mangled true, Args true] type_sys then - (fn (s, ty) => - type_pred_combatom type_sys ty (CombVar (s, ty)) - |> formula_from_combformula ctxt type_sys |> SOME) - else - K NONE - fun do_formula (AQuant (q, xs, phi)) = - AQuant (q, xs |> map (apsnd (fn NONE => NONE - | SOME ty => do_bound_type ty)), - (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) - (do_formula phi)) - | do_formula (AConn (c, phis)) = AConn (c, map do_formula phis) - | do_formula (AAtom tm) = AAtom (do_term true tm) - in do_formula end - -fun formula_for_fact ctxt type_sys - ({combformula, atomic_types, ...} : translated_formula) = - mk_ahorn (map (formula_from_fo_literal o fo_literal_from_type_literal) - (atp_type_literals_for_types type_sys Axiom atomic_types)) - (formula_from_combformula ctxt type_sys - (close_combformula_universally combformula)) - |> close_formula_universally - -fun logic_for_type_sys Many_Typed = Tff - | logic_for_type_sys _ = Fof - -(* 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 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 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, - AConn (AImplies, [AAtom (ATerm (subclass, [ty_arg])), - AAtom (ATerm (superclass, [ty_arg]))]) - |> close_formula_universally, NONE, NONE) - end - -fun fo_literal_from_arity_literal (TConsLit (c, t, args)) = - (true, ATerm (c, [ATerm (t, map (fn arg => ATerm (arg, [])) args)])) - | fo_literal_from_arity_literal (TVarLit (c, sort)) = - (false, ATerm (c, [ATerm (sort, [])])) - -fun formula_line_for_arity_clause (ArityClause {name, conclLit, premLits, - ...}) = - Formula (Fof, arity_clause_prefix ^ ascii_of name, Axiom, - mk_ahorn (map (formula_from_fo_literal o apfst not - o fo_literal_from_arity_literal) premLits) - (formula_from_fo_literal - (fo_literal_from_arity_literal conclLit)) - |> close_formula_universally, NONE, NONE) - -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_from_combformula ctxt type_sys - (close_combformula_universally combformula) - |> close_formula_universally, NONE, NONE) - -fun free_type_literals type_sys ({atomic_types, ...} : translated_formula) = - atomic_types |> atp_type_literals_for_types type_sys Conjecture - |> map fo_literal_from_type_literal - -fun formula_line_for_free_type j lit = - Formula (Fof, tfree_prefix ^ string_of_int j, Hypothesis, - formula_from_fo_literal lit, NONE, NONE) -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 formula_line_for_free_type (0 upto length lits - 1) lits end - -(** "hBOOL" and "hAPP" **) - fun add_combterm_to_sym_table explicit_apply = let fun aux top_level tm = @@ -734,11 +497,251 @@ | (head, args) => list_explicit_app head (map aux args) in aux end -fun firstorderize_combterm sym_tab = +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)) = + (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, []) + | Mangled_Types => (mangled_const_name ty_args name, []) + | Explicit_Type_Args => (name, ty_args) + end) + |> (fn (name, ty_args) => CombConst (name, ty, ty_args)) + | aux tm = tm + in aux end + +fun repair_combterm type_sys sym_tab = introduce_explicit_apps_in_combterm sym_tab #> introduce_predicators_in_combterm sym_tab -val firstorderize_fact = - update_combformula o formula_map o firstorderize_combterm + #> impose_type_arg_policy_in_combterm type_sys +val repair_fact = update_combformula o formula_map oo repair_combterm + +(** Helper facts **) + +fun ti_ti_helper_fact () = + let + fun var s = ATerm (`I s, []) + fun tag tm = ATerm (`I type_tag_name, [var "X", tm]) + in + Formula (Fof, helper_prefix ^ ascii_of "ti_ti", Axiom, + AAtom (ATerm (`I "equal", [tag (tag (var "Y")), tag (var "Y")])) + |> close_formula_universally, NONE, NONE) + end + +fun helper_facts_for_sym ctxt type_sys (s, {typ, ...} : sym_table_info) = + case strip_prefix_and_unascii const_prefix s of + SOME mangled_s => + let + val thy = Proof_Context.theory_of ctxt + val unmangled_s = mangled_s |> unmangled_const_name + fun dub_and_inst c needs_full_types (th, j) = + ((c ^ "_" ^ string_of_int j ^ (if needs_full_types then "ft" else ""), + false), + let val t = th |> prop_of in + t |> (general_type_arg_policy type_sys = Mangled_Types andalso + not (null (Term.hidden_polymorphism t))) + ? (case typ of + SOME T => specialize_type thy (invert_const unmangled_s, T) + | NONE => I) + end) + fun make_facts eq_as_iff = + map_filter (make_fact ctxt false eq_as_iff false) + in + metis_helpers + |> maps (fn (metis_s, (needs_full_types, ths)) => + if metis_s <> unmangled_s orelse + (needs_full_types andalso + not (type_system_types_dangerous_types type_sys)) then + [] + else + ths ~~ (1 upto length ths) + |> map (dub_and_inst mangled_s needs_full_types) + |> make_facts (not needs_full_types)) + end + | NONE => [] +fun helper_facts_for_sym_table ctxt type_sys sym_tab = + Symtab.fold_rev (append o helper_facts_for_sym ctxt type_sys) sym_tab [] + +fun translate_atp_fact ctxt keep_trivial = + `(make_fact ctxt keep_trivial true true o apsnd prop_of) + +fun translate_formulas ctxt type_sys hyp_ts concl_t rich_facts = + let + val thy = Proof_Context.theory_of ctxt + val fact_ts = map (prop_of o snd o snd) rich_facts + val (facts, fact_names) = + rich_facts + |> map_filter (fn (NONE, _) => NONE + | (SOME fact, (name, _)) => SOME (fact, name)) + |> ListPair.unzip + (* Remove existing facts from the conjecture, as this can dramatically + boost an ATP's performance (for some reason). *) + val hyp_ts = hyp_ts |> filter_out (member (op aconv) fact_ts) + val goal_t = Logic.list_implies (hyp_ts, concl_t) + val all_ts = goal_t :: fact_ts + 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 (supers', arity_clauses) = + if type_sys = No_Types then ([], []) + else make_arity_clauses thy tycons supers + val class_rel_clauses = make_class_rel_clauses thy subs supers' + in + (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 fo_literal_from_type_literal (TyLitVar (class, name)) = + (true, ATerm (class, [ATerm (name, [])])) + | fo_literal_from_type_literal (TyLitFree (class, name)) = + (true, ATerm (class, [ATerm (name, [])])) + +fun formula_from_fo_literal (pos, t) = AAtom t |> not pos ? mk_anot + +(* Finite types such as "unit", "bool", "bool * bool", and "bool => bool" are + considered dangerous because their "exhaust" properties can easily lead to + unsound ATP proofs. The checks below are an (unsound) approximation of + finiteness. *) + +fun is_dtyp_dangerous _ (Datatype_Aux.DtTFree _) = true + | is_dtyp_dangerous ctxt (Datatype_Aux.DtType (s, Us)) = + is_type_constr_dangerous ctxt s andalso forall (is_dtyp_dangerous ctxt) Us + | is_dtyp_dangerous _ (Datatype_Aux.DtRec _) = false +and is_type_dangerous ctxt (Type (s, Ts)) = + is_type_constr_dangerous ctxt s andalso forall (is_type_dangerous ctxt) Ts + | is_type_dangerous _ _ = false +and is_type_constr_dangerous ctxt s = + let val thy = Proof_Context.theory_of ctxt in + case Datatype_Data.get_info thy s of + SOME {descr, ...} => + forall (fn (_, (_, _, constrs)) => + forall (forall (is_dtyp_dangerous ctxt) o snd) constrs) descr + | NONE => + case Typedef.get_info ctxt s of + ({rep_type, ...}, _) :: _ => is_type_dangerous ctxt rep_type + | [] => true + end + +fun should_tag_with_type ctxt (Tags full_types) T = + full_types orelse is_type_dangerous ctxt T + | should_tag_with_type _ _ _ = false + +fun type_pred_combatom type_sys T tm = + CombApp (CombConst (`make_fixed_const type_pred_base, T --> @{typ bool}, [T]), + tm) + |> impose_type_arg_policy_in_combterm type_sys + |> AAtom + +fun formula_from_combformula ctxt type_sys = + let + fun do_term top_level u = + let + val (head, args) = strip_combterm_comb u + val (x, ty_args) = + case head of + CombConst (name, _, ty_args) => (name, ty_args) + | CombVar (name, _) => (name, []) + | CombApp _ => raise Fail "impossible \"CombApp\"" + val t = ATerm (x, map fo_term_from_typ ty_args @ + map (do_term false) args) + val ty = 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) + 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 + 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)), + (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) + (do_formula phi)) + | do_formula (AConn (c, phis)) = AConn (c, map do_formula phis) + | do_formula (AAtom tm) = AAtom (do_term true tm) + in do_formula end + +fun formula_for_fact ctxt type_sys + ({combformula, atomic_types, ...} : translated_formula) = + mk_ahorn (map (formula_from_fo_literal o fo_literal_from_type_literal) + (atp_type_literals_for_types type_sys Axiom atomic_types)) + (formula_from_combformula ctxt type_sys + (close_combformula_universally combformula)) + |> close_formula_universally + +fun logic_for_type_sys Many_Typed = Tff + | logic_for_type_sys _ = Fof + +(* 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 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 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, + AConn (AImplies, [AAtom (ATerm (subclass, [ty_arg])), + AAtom (ATerm (superclass, [ty_arg]))]) + |> close_formula_universally, NONE, NONE) + end + +fun fo_literal_from_arity_literal (TConsLit (c, t, args)) = + (true, ATerm (c, [ATerm (t, map (fn arg => ATerm (arg, [])) args)])) + | fo_literal_from_arity_literal (TVarLit (c, sort)) = + (false, ATerm (c, [ATerm (sort, [])])) + +fun formula_line_for_arity_clause (ArityClause {name, conclLit, premLits, + ...}) = + Formula (Fof, arity_clause_prefix ^ ascii_of name, Axiom, + mk_ahorn (map (formula_from_fo_literal o apfst not + o fo_literal_from_arity_literal) premLits) + (formula_from_fo_literal + (fo_literal_from_arity_literal conclLit)) + |> close_formula_universally, NONE, NONE) + +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_from_combformula ctxt type_sys + (close_combformula_universally combformula) + |> close_formula_universally, NONE, NONE) + +fun free_type_literals type_sys ({atomic_types, ...} : translated_formula) = + atomic_types |> atp_type_literals_for_types type_sys Conjecture + |> map fo_literal_from_type_literal + +fun formula_line_for_free_type j lit = + Formula (Fof, tfree_prefix ^ string_of_int j, Hypothesis, + formula_from_fo_literal lit, NONE, NONE) +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 formula_line_for_free_type (0 upto length lits - 1) lits end + +(** Symbol declarations **) fun is_const_relevant type_sys sym_tab s = not (String.isPrefix bound_var_prefix s) andalso s <> "equal" andalso @@ -842,18 +845,16 @@ translate_formulas ctxt type_sys hyp_ts concl_t facts val sym_tab = conjs @ facts |> sym_table_for_facts explicit_apply val (conjs, facts) = - (conjs, facts) |> pairself (map (firstorderize_fact sym_tab)) - val sym_tab = conjs @ facts |> sym_table_for_facts explicit_apply - val (conjs, facts) = - (conjs, facts) |> pairself (map (impose_type_arg_policy_on_fact type_sys)) - val sym_tab' = conjs @ facts |> sym_table_for_facts false + (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 sym_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 sym_tab' - val helpers = helper_facts_for_sym_table ctxt type_sys sym_tab' - |> map (firstorderize_fact sym_tab - #> impose_type_arg_policy_on_fact type_sys) + typed_const_tab + |> problem_lines_for_sym_decls ctxt type_sys repaired_sym_tab + val helpers = + helper_facts_for_sym_table ctxt type_sys repaired_sym_tab + |> map (repair_fact type_sys sym_tab) (* Reordering these might confuse the proof reconstruction code or the SPASS Flotter hack. *) val problem =