--- 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