# HG changeset patch # User blanchet # Date 1328142028 -3600 # Node ID 676a4b4b6e736243b2580c61c8cf77c1eddbe722 # Parent 8d8d3c1f1854c8bacb33bc05f7d71fcd2e7956a0 implemented partial application aliases (for SPASS mainly) diff -r 8d8d3c1f1854 -r 676a4b4b6e73 src/HOL/Tools/ATP/atp_problem_generate.ML --- a/src/HOL/Tools/ATP/atp_problem_generate.ML Wed Feb 01 17:16:55 2012 +0100 +++ b/src/HOL/Tools/ATP/atp_problem_generate.ML Thu Feb 02 01:20:28 2012 +0100 @@ -96,7 +96,7 @@ val mk_aconns : connective -> ('a, 'b, 'c) formula list -> ('a, 'b, 'c) formula val unmangled_const : string -> string * (string, 'b) ho_term list - val unmangled_const_name : string -> string + val unmangled_const_name : string -> string list val helper_table : ((string * bool) * thm list) list val trans_lams_from_string : Proof.context -> type_enc -> string -> term list -> term list * term list @@ -149,13 +149,14 @@ val class_prefix = "cl_" (* Freshness almost guaranteed! *) +val atp_prefix = "ATP" ^ Long_Name.separator val atp_weak_prefix = "ATP:" val lam_lifted_prefix = atp_weak_prefix ^ "Lam" val lam_lifted_mono_prefix = lam_lifted_prefix ^ "m" val lam_lifted_poly_prefix = lam_lifted_prefix ^ "p" -val skolem_const_prefix = "ATP" ^ Long_Name.separator ^ "Sko" +val skolem_const_prefix = atp_prefix ^ "Sko" val old_skolem_const_prefix = skolem_const_prefix ^ "o" val new_skolem_const_prefix = skolem_const_prefix ^ "n" @@ -165,6 +166,7 @@ val sym_decl_prefix = "sy_" val guards_sym_formula_prefix = "gsy_" val tags_sym_formula_prefix = "tsy_" +val app_op_alias_eq_prefix = "aa_" val fact_prefix = "fact_" val conjecture_prefix = "conj_" val helper_prefix = "help_" @@ -873,7 +875,10 @@ if T = dummyT then NONE else SOME (ho_term_from_typ format type_enc T) (* This shouldn't clash with anything else. *) -val mangled_type_sep = "\000" +val app_op_alias_sep = "\000" +val mangled_type_sep = "\001" + +val ascii_of_app_op_alias_sep = ascii_of app_op_alias_sep fun generic_mangled_type_name f (ATerm (name, [])) = f name | generic_mangled_type_name f (ATerm (name, tys)) = @@ -914,13 +919,23 @@ ho_type_from_ho_term type_enc pred_sym ary o ho_term_from_typ format type_enc -fun mangled_const_name format type_enc T_args (s, s') = +fun aliased_app_op ary (s, s') = + (s ^ ascii_of_app_op_alias_sep ^ string_of_int ary, s' ^ string_of_int ary) +fun unaliased_app_op (s, s') = + case space_explode app_op_alias_sep s of + [_] => (s, s') + | [s1, s2] => (s1, unsuffix s2 s') + | _ => raise Fail "ill-formed explicit application alias" + +fun raw_mangled_const_name type_name ty_args (s, s') = let - val ty_args = T_args |> map_filter (ho_term_for_type_arg format type_enc) fun type_suffix f g = - fold_rev (curry (op ^) o g o prefix mangled_type_sep - o generic_mangled_type_name f) ty_args "" + fold_rev (curry (op ^) o g o prefix mangled_type_sep o type_name f) + ty_args "" in (s ^ type_suffix fst ascii_of, s' ^ type_suffix snd I) end +fun mangled_const_name format type_enc = + map_filter (ho_term_for_type_arg format type_enc) + #> raw_mangled_const_name generic_mangled_type_name val parse_mangled_ident = Scan.many1 (not o member (op =) ["(", ")", ","]) >> implode @@ -939,9 +954,10 @@ quote s)) parse_mangled_type)) |> fst -val unmangled_const_name = space_explode mangled_type_sep #> hd +fun unmangled_const_name s = + (s, s) |> unaliased_app_op |> fst |> space_explode mangled_type_sep fun unmangled_const s = - let val ss = space_explode mangled_type_sep s in + let val ss = unmangled_const_name s in (hd ss, map unmangled_type (tl ss)) end @@ -992,19 +1008,21 @@ | intro _ _ tm = tm in intro true [] end +fun mangle_type_args_in_const format type_enc (name as (s, _)) T_args = + case unprefix_and_unascii const_prefix s of + NONE => (name, T_args) + | SOME s'' => + case type_arg_policy [] type_enc (invert_const s'') of + Mangled_Type_Args => (mangled_const_name format type_enc T_args name, []) + | _ => (name, T_args) fun mangle_type_args_in_iterm format type_enc = if polymorphism_of_type_enc type_enc = Mangled_Monomorphic then let fun mangle (IApp (tm1, tm2)) = IApp (mangle tm1, mangle tm2) | mangle (tm as IConst (_, _, [])) = tm - | mangle (tm as IConst (name as (s, _), T, T_args)) = - (case unprefix_and_unascii const_prefix s of - NONE => tm - | SOME s'' => - case type_arg_policy [] type_enc (invert_const s'') of - Mangled_Type_Args => - IConst (mangled_const_name format type_enc T_args name, T, []) - | _ => tm) + | mangle (IConst (name, T, T_args)) = + mangle_type_args_in_const format type_enc name T_args + |> (fn (name, T_args) => IConst (name, T, T_args)) | mangle (IAbs (bound, tm)) = IAbs (bound, mangle tm) | mangle tm = tm in mangle end @@ -1029,31 +1047,30 @@ end handle TYPE _ => T_args +fun filter_type_args_in_const _ _ _ _ _ [] = [] + | filter_type_args_in_const thy monom_constrs type_enc ary s T_args = + case unprefix_and_unascii const_prefix s of + NONE => + if level_of_type_enc type_enc = No_Types orelse s = tptp_choice then [] + else T_args + | SOME s'' => + let + val s'' = invert_const s'' + fun filter_T_args false = T_args + | filter_T_args true = filter_const_type_args thy s'' ary T_args + in + case type_arg_policy monom_constrs type_enc s'' of + Explicit_Type_Args infer_from_term_args => + filter_T_args infer_from_term_args + | No_Type_Args => [] + | Mangled_Type_Args => raise Fail "unexpected (un)mangled symbol" + end fun filter_type_args_in_iterm thy monom_constrs type_enc = let fun filt ary (IApp (tm1, tm2)) = IApp (filt (ary + 1) tm1, filt 0 tm2) - | filt _ (tm as IConst (_, _, [])) = tm | filt ary (IConst (name as (s, _), T, T_args)) = - (case unprefix_and_unascii const_prefix s of - NONE => - (name, - if level_of_type_enc type_enc = No_Types orelse s = tptp_choice then - [] - else - T_args) - | SOME s'' => - let - val s'' = invert_const s'' - fun filter_T_args false = T_args - | filter_T_args true = filter_const_type_args thy s'' ary T_args - in - case type_arg_policy monom_constrs type_enc s'' of - Explicit_Type_Args infer_from_term_args => - (name, filter_T_args infer_from_term_args) - | No_Type_Args => (name, []) - | Mangled_Type_Args => raise Fail "unexpected (un)mangled symbol" - end) - |> (fn (name, T_args) => IConst (name, T, T_args)) + filter_type_args_in_const thy monom_constrs type_enc ary s T_args + |> (fn T_args => IConst (name, T, T_args)) | filt _ (IAbs (bound, tm)) = IAbs (bound, filt 0 tm) | filt _ tm = tm in filt 0 end @@ -1064,8 +1081,7 @@ fun do_term bs t atomic_Ts = iterm_from_term thy format bs (Envir.eta_contract t) |>> (introduce_proxies_in_iterm type_enc - #> mangle_type_args_in_iterm format type_enc - #> AAtom) + #> mangle_type_args_in_iterm format type_enc #> AAtom) ||> union (op =) atomic_Ts fun do_quant bs q pos s T t' = let @@ -1377,9 +1393,9 @@ {pred_sym = true, min_ary = 1, max_ary = 1, types = [], in_conj = false}) -datatype explicit_apply = Incomplete_Apply | Sufficient_Apply | Full_Apply +datatype app_op_level = Incomplete_Apply | Sufficient_Apply | Full_Apply -fun sym_table_for_facts ctxt type_enc explicit_apply conjs facts = +fun sym_table_for_facts ctxt type_enc app_op_level conjs facts = let fun consider_var_ary const_T var_T max_ary = let @@ -1391,7 +1407,7 @@ iter (ary + 1) (range_type T) in iter 0 const_T end fun add_universal_var T (accum as ((bool_vars, fun_var_Ts), sym_tab)) = - if explicit_apply = Sufficient_Apply andalso + if app_op_level = Sufficient_Apply andalso (can dest_funT T orelse T = @{typ bool}) then let val bool_vars' = bool_vars orelse body_type T = @{typ bool} @@ -1410,64 +1426,63 @@ end else accum + fun add_iterm_syms conj_fact top_level tm + (accum as ((bool_vars, fun_var_Ts), sym_tab)) = + let val (head, args) = strip_iterm_comb tm in + (case head of + IConst ((s, _), T, _) => + if String.isPrefix bound_var_prefix s orelse + String.isPrefix all_bound_var_prefix s then + add_universal_var T accum + else if String.isPrefix exist_bound_var_prefix s then + accum + else + let val ary = length args in + ((bool_vars, fun_var_Ts), + case Symtab.lookup sym_tab s of + SOME {pred_sym, min_ary, max_ary, types, in_conj} => + let + val pred_sym = + pred_sym andalso top_level andalso not bool_vars + val types' = types |> insert_type ctxt I T + val in_conj = in_conj orelse conj_fact + val min_ary = + if app_op_level = Sufficient_Apply andalso + not (pointer_eq (types', types)) then + fold (consider_var_ary T) fun_var_Ts min_ary + else + min_ary + in + Symtab.update (s, {pred_sym = pred_sym, + min_ary = Int.min (ary, min_ary), + max_ary = Int.max (ary, max_ary), + types = types', in_conj = in_conj}) + sym_tab + end + | NONE => + let + val pred_sym = top_level andalso not bool_vars + val min_ary = + case app_op_level of + Incomplete_Apply => ary + | Sufficient_Apply => + fold (consider_var_ary T) fun_var_Ts ary + | Full_Apply => 0 + in + Symtab.update_new (s, + {pred_sym = pred_sym, min_ary = min_ary, + max_ary = ary, types = [T], in_conj = conj_fact}) + sym_tab + end) + end + | IVar (_, T) => add_universal_var T accum + | IAbs ((_, T), tm) => + accum |> add_universal_var T |> add_iterm_syms conj_fact false tm + | _ => accum) + |> fold (add_iterm_syms conj_fact false) args + end fun add_fact_syms conj_fact = - let - fun add_iterm_syms top_level tm - (accum as ((bool_vars, fun_var_Ts), sym_tab)) = - let val (head, args) = strip_iterm_comb tm in - (case head of - IConst ((s, _), T, _) => - if String.isPrefix bound_var_prefix s orelse - String.isPrefix all_bound_var_prefix s then - add_universal_var T accum - else if String.isPrefix exist_bound_var_prefix s then - accum - else - let val ary = length args in - ((bool_vars, fun_var_Ts), - case Symtab.lookup sym_tab s of - SOME {pred_sym, min_ary, max_ary, types, in_conj} => - let - val pred_sym = - pred_sym andalso top_level andalso not bool_vars - val types' = types |> insert_type ctxt I T - val in_conj = in_conj orelse conj_fact - val min_ary = - if explicit_apply = Sufficient_Apply andalso - not (pointer_eq (types', types)) then - fold (consider_var_ary T) fun_var_Ts min_ary - else - min_ary - in - Symtab.update (s, {pred_sym = pred_sym, - min_ary = Int.min (ary, min_ary), - max_ary = Int.max (ary, max_ary), - types = types', in_conj = in_conj}) - sym_tab - end - | NONE => - let - val pred_sym = top_level andalso not bool_vars - val min_ary = - case explicit_apply of - Incomplete_Apply => ary - | Sufficient_Apply => - fold (consider_var_ary T) fun_var_Ts ary - | Full_Apply => 0 - in - Symtab.update_new (s, - {pred_sym = pred_sym, min_ary = min_ary, - max_ary = ary, types = [T], in_conj = conj_fact}) - sym_tab - end) - end - | IVar (_, T) => add_universal_var T accum - | IAbs ((_, T), tm) => - accum |> add_universal_var T |> add_iterm_syms false tm - | _ => accum) - |> fold (add_iterm_syms false) args - end - in K (add_iterm_syms true) |> formula_fold NONE |> fact_lift end + K (add_iterm_syms conj_fact true) |> formula_fold NONE |> fact_lift in ((false, []), Symtab.empty) |> fold (add_fact_syms true) conjs @@ -1482,7 +1497,7 @@ | NONE => case unprefix_and_unascii const_prefix s of SOME s => - let val s = s |> unmangled_const_name |> invert_const in + let val s = s |> unmangled_const_name |> hd |> invert_const in if s = predicator_name then 1 else if s = app_op_name then 2 else if s = type_guard_name then 1 @@ -1507,25 +1522,34 @@ fun list_app head args = fold (curry (IApp o swap)) args head fun predicator tm = IApp (predicator_combconst, tm) -fun firstorderize_fact thy monom_constrs format type_enc sym_tab = +fun do_app_op format type_enc head arg = let - fun do_app arg head = - let - val head_T = ityp_of head - val (arg_T, res_T) = dest_funT head_T - val app = - IConst (app_op, head_T --> head_T, [arg_T, res_T]) - |> mangle_type_args_in_iterm format type_enc - in list_app app [head, arg] end + val head_T = ityp_of head + val (arg_T, res_T) = dest_funT head_T + val app = + IConst (app_op, head_T --> head_T, [arg_T, res_T]) + |> mangle_type_args_in_iterm format type_enc + in list_app app [head, arg] end + +fun firstorderize_fact thy monom_constrs format type_enc app_op_aliases + sym_tab = + let + fun do_app arg head = do_app_op format type_enc head arg fun list_app_ops head args = fold do_app args head fun introduce_app_ops tm = - case strip_iterm_comb tm of - (head as IConst ((s, _), _, _), args) => - args |> map introduce_app_ops - |> chop (min_ary_of sym_tab s) - |>> list_app head - |-> list_app_ops - | (head, args) => list_app_ops head (map introduce_app_ops args) + let val (head, args) = tm |> strip_iterm_comb ||> map introduce_app_ops in + case head of + IConst (name as (s, _), T, T_args) => + if app_op_aliases then + let + val ary = length args + val name = name |> ary > min_ary_of sym_tab s ? aliased_app_op ary + in list_app (IConst (name, T, T_args)) args end + else + args |> chop (min_ary_of sym_tab s) + |>> list_app head |-> list_app_ops + | _ => list_app_ops head args + end fun introduce_predicators tm = case strip_iterm_comb tm of (IConst ((s, _), _, _), _) => @@ -1590,9 +1614,10 @@ atype_of_type_vars type_enc) | _ => NONE) Ts) -fun eq_formula type_enc atomic_Ts pred_sym tm1 tm2 = +fun eq_formula type_enc atomic_Ts bounds pred_sym tm1 tm2 = (if pred_sym then AConn (AIff, [AAtom tm1, AAtom tm2]) else AAtom (ATerm (`I tptp_equal, [tm1, tm2]))) + |> mk_aquant AForall bounds |> close_formula_universally |> bound_tvars type_enc true atomic_Ts @@ -1605,7 +1630,7 @@ val tagged_var = tag (var "X") in Formula (type_tag_idempotence_helper_name, Axiom, - eq_formula type_enc [] false (tag tagged_var) tagged_var, + eq_formula type_enc [] [] false (tag tagged_var) tagged_var, NONE, isabelle_info format eqN) end @@ -1619,7 +1644,7 @@ SOME mangled_s => let val thy = Proof_Context.theory_of ctxt - val unmangled_s = mangled_s |> unmangled_const_name + val unmangled_s = mangled_s |> unmangled_const_name |> hd fun dub needs_fairly_sound j k = unmangled_s ^ "_" ^ string_of_int j ^ "_" ^ string_of_int k ^ (if mangled_s = unmangled_s then "" else "_" ^ ascii_of mangled_s) ^ @@ -1829,6 +1854,13 @@ fun mk_aterm format type_enc name T_args args = ATerm (name, map_filter (ho_term_for_type_arg format type_enc) T_args @ args) +fun do_bound_type ctxt format mono type_enc = + case type_enc of + Simple_Types (_, _, level) => + fused_type ctxt mono level 0 + #> ho_type_from_typ format type_enc false 0 #> SOME + | _ => K NONE + fun tag_with_type ctxt format mono type_enc pos T tm = IConst (type_tag, T --> T, [T]) |> mangle_type_args_in_iterm format type_enc @@ -1873,11 +1905,6 @@ val thy = Proof_Context.theory_of ctxt val level = level_of_type_enc type_enc val do_term = ho_term_from_iterm ctxt format mono type_enc - val do_bound_type = - case type_enc of - Simple_Types _ => fused_type ctxt mono level 0 - #> ho_type_from_typ format type_enc false 0 #> SOME - | _ => K NONE fun do_out_of_bound_type pos phi universal (name, T) = if should_guard_type ctxt mono type_enc (fn () => should_guard_var thy polym_constrs level pos phi @@ -1896,6 +1923,7 @@ let val phi = phi |> do_formula pos val universal = Option.map (q = AExists ? not) pos + val do_bound_type = do_bound_type ctxt format mono type_enc in AQuant (q, xs |> map (apsnd (fn NONE => NONE | SOME T => do_bound_type T)), @@ -1995,7 +2023,8 @@ map (decl_line_for_class order) classes | _ => [] -fun sym_decl_table_for_facts ctxt format type_enc sym_tab (conjs, facts) = +fun sym_decl_table_for_facts ctxt format type_enc sym_tab + (conjs, facts, extra_tms) = let fun add_iterm_syms tm = let val (head, args) = strip_iterm_comb tm in @@ -2055,6 +2084,7 @@ Symtab.empty |> is_type_enc_fairly_sound type_enc ? (fold (fold add_fact_syms) [conjs, facts] + #> fold add_iterm_syms extra_tms #> (case type_enc of Simple_Types (First_Order, Polymorphic, _) => if avoid_first_order_ghost_type_vars then add_TYPE_const () @@ -2168,7 +2198,7 @@ Formula (tags_sym_formula_prefix ^ ascii_of (mangled_type format type_enc T), Axiom, - eq_formula type_enc (atomic_types_of T) false + eq_formula type_enc (atomic_types_of T) [] false (tag_with_type ctxt format mono type_enc NONE T x_var) x_var, NONE, isabelle_info format eqN) end @@ -2202,13 +2232,15 @@ ? curry ATyAbs (map (tvar_name o fst o dest_TVar) T_args)) end +fun honor_conj_sym_kind in_conj conj_sym_kind = + if in_conj then (conj_sym_kind, conj_sym_kind = Conjecture ? mk_anot) + else (Axiom, I) + fun formula_line_for_guards_sym_decl ctxt format conj_sym_kind mono type_enc n s j (s', T_args, T, _, ary, in_conj) = let val thy = Proof_Context.theory_of ctxt - val (kind, maybe_negate) = - if in_conj then (conj_sym_kind, conj_sym_kind = Conjecture ? mk_anot) - else (Axiom, I) + val (kind, maybe_negate) = honor_conj_sym_kind in_conj conj_sym_kind val (arg_Ts, res_T) = chop_fun ary T val bound_names = 1 upto ary |> map (`I o make_bound_var o string_of_int) val bounds = @@ -2251,14 +2283,12 @@ val ident_base = tags_sym_formula_prefix ^ s ^ (if n > 1 then "_" ^ string_of_int j else "") - val (kind, maybe_negate) = - if in_conj then (conj_sym_kind, conj_sym_kind = Conjecture ? mk_anot) - else (Axiom, I) + val (kind, maybe_negate) = honor_conj_sym_kind in_conj conj_sym_kind val (arg_Ts, res_T) = chop_fun ary T val bound_names = 1 upto ary |> map (`I o make_bound_var o string_of_int) val bounds = bound_names |> map (fn name => ATerm (name, [])) val cst = mk_aterm format type_enc (s, s') T_args - val eq = maybe_negate oo eq_formula type_enc (atomic_types_of T) pred_sym + val eq = maybe_negate oo eq_formula type_enc (atomic_types_of T) [] pred_sym val should_encode = should_encode_type ctxt mono level val tag_with = tag_with_type ctxt format mono type_enc NONE val add_formula_for_res = @@ -2351,6 +2381,74 @@ syms [] in mono_lines @ decl_lines end +fun pair_append (xs1, xs2) (ys1, ys2) = (xs1 @ ys1, xs2 @ ys2) + +fun do_app_op_alias_lines_for_sym ctxt monom_constrs format conj_sym_kind mono + type_enc sym_tab base_s0 types in_conj = + let + fun do_alias ary = + let + val thy = Proof_Context.theory_of ctxt + val (kind, maybe_negate) = honor_conj_sym_kind in_conj conj_sym_kind + val base_name = base_s0 |> `(make_fixed_const (SOME format)) + val T = case types of [T] => T | _ => robust_const_type thy base_s0 + val T_args = robust_const_typargs thy (base_s0, T) + val (base_name as (base_s, _), T_args) = + mangle_type_args_in_const format type_enc base_name T_args + val base_ary = min_ary_of sym_tab base_s + val T_args = + T_args |> filter_type_args_in_const thy monom_constrs type_enc + base_ary base_s + fun do_const name = IConst (name, T, T_args) + val do_term = ho_term_from_iterm ctxt format mono type_enc (SOME true) + val name1 as (s1, _) = + base_name |> ary - 1 > base_ary ? aliased_app_op (ary - 1) + val name2 as (s2, _) = base_name |> aliased_app_op ary + val (arg_Ts, _) = chop_fun ary T + val bound_names = + 1 upto ary |> map (`I o make_bound_var o string_of_int) + val bounds = bound_names ~~ arg_Ts + val (first_bounds, last_bound) = + bounds |> map (fn (name, T) => IConst (name, T, [])) |> split_last + val tm1 = + do_app_op format type_enc (list_app (do_const name1) first_bounds) + last_bound + val tm2 = list_app (do_const name2) (first_bounds @ [last_bound]) + val do_bound_type = do_bound_type ctxt format mono type_enc + val eq = + eq_formula type_enc (atomic_types_of T) + (map (apsnd do_bound_type) bounds) false + (do_term tm1) (do_term tm2) + in + ([tm1, tm2], + [Formula (app_op_alias_eq_prefix ^ s2, kind, eq |> maybe_negate, NONE, + isabelle_info format eqN)]) + |> (if ary - 1 = base_ary orelse Symtab.defined sym_tab s1 then I + else pair_append (do_alias (ary - 1))) + end + in do_alias end +fun app_op_alias_lines_for_sym ctxt monom_constrs format conj_sym_kind mono + type_enc sym_tab (s, {min_ary, types, in_conj, ...} : sym_info) = + case unprefix_and_unascii const_prefix s of + SOME mangled_s => + if String.isSubstring app_op_alias_sep mangled_s then + let + val base_s0 = mangled_s |> unmangled_const_name |> hd |> invert_const + in + do_app_op_alias_lines_for_sym ctxt monom_constrs format conj_sym_kind + mono type_enc sym_tab base_s0 types in_conj min_ary + end + else + ([], []) + | NONE => ([], []) +fun app_op_alias_lines_for_sym_table ctxt monom_constrs format conj_sym_kind + mono type_enc app_op_aliases sym_tab = + ([], []) + |> app_op_aliases + ? Symtab.fold_rev (pair_append + o app_op_alias_lines_for_sym ctxt monom_constrs format + conj_sym_kind mono type_enc sym_tab) sym_tab + fun needs_type_tag_idempotence ctxt (Tags (poly, level)) = Config.get ctxt type_tag_idempotence andalso is_type_level_monotonicity_based level andalso @@ -2359,6 +2457,7 @@ val implicit_declsN = "Should-be-implicit typings" val explicit_declsN = "Explicit typings" +val app_op_alias_eqsN = "Application aliases" val factsN = "Relevant facts" val class_relsN = "Class relationships" val aritiesN = "Arities" @@ -2388,17 +2487,18 @@ fun undeclared_syms_in_problem type_enc problem = let val declared = declared_syms_in_problem problem - fun do_sym name ty = - if member (op =) declared name then I else AList.default (op =) (name, ty) - fun do_type (AType (name as (s, _), tys)) = - is_tptp_user_symbol s - ? do_sym name (fn () => nary_type_constr_type (length tys)) + fun do_sym (name as (s, _)) ty = + if is_tptp_user_symbol s andalso not (member (op =) declared name) then + AList.default (op =) (name, ty) + else + I + fun do_type (AType (name, tys)) = + do_sym name (fn () => nary_type_constr_type (length tys)) #> fold do_type tys | do_type (AFun (ty1, ty2)) = do_type ty1 #> do_type ty2 | do_type (ATyAbs (_, ty)) = do_type ty fun do_term pred_sym (ATerm (name as (s, _), tms)) = - is_tptp_user_symbol s - ? do_sym name (fn _ => default_type type_enc pred_sym s (length tms)) + do_sym name (fn _ => default_type type_enc pred_sym s (length tms)) #> fold (do_term false) tms | do_term _ (AAbs ((_, ty), tm)) = do_type ty #> do_term false tm fun do_formula (AQuant (_, xs, phi)) = @@ -2439,7 +2539,7 @@ |> List.partition is_poly_constr |> pairself (map fst) -val explicit_apply_threshold = 50 +val app_op_threshold = 50 fun prepare_atp_problem ctxt format conj_sym_kind prem_kind type_enc exporter lam_trans readable_names preproc hyp_ts concl_t facts = @@ -2450,12 +2550,13 @@ because it takes only one existential variable ranging over "'a => 'b" to ruin everything. Hence we do it only if there are few facts (which is normally the case for "metis" and the minimizer). *) - val explicit_apply = + val app_op_level = if polymorphism_of_type_enc type_enc = Polymorphic andalso - length facts >= explicit_apply_threshold then + length facts >= app_op_threshold then Incomplete_Apply else Sufficient_Apply + val app_op_aliases = (format = DFG DFG_Sorted) val lam_trans = if lam_trans = keep_lamsN andalso not (is_type_enc_higher_order type_enc) then @@ -2467,13 +2568,14 @@ lifted) = translate_formulas ctxt format prem_kind type_enc lam_trans preproc hyp_ts concl_t facts - val sym_tab = sym_table_for_facts ctxt type_enc explicit_apply conjs facts + val sym_tab = sym_table_for_facts ctxt type_enc app_op_level conjs facts val mono = conjs @ facts |> mononotonicity_info_for_facts ctxt type_enc val (polym_constrs, monom_constrs) = all_constrs_of_polymorphic_datatypes thy |>> map (make_fixed_const (SOME format)) val firstorderize = - firstorderize_fact thy monom_constrs format type_enc sym_tab + firstorderize_fact thy monom_constrs format type_enc app_op_aliases + sym_tab val (conjs, facts) = (conjs, facts) |> pairself (map firstorderize) val sym_tab = sym_table_for_facts ctxt type_enc Incomplete_Apply conjs facts val helpers = @@ -2482,8 +2584,11 @@ val mono_Ts = helpers @ conjs @ facts |> monotonic_types_for_facts ctxt mono type_enc val class_decl_lines = decl_lines_for_classes type_enc classes + val (app_op_alias_eq_tms, app_op_alias_eq_lines) = + app_op_alias_lines_for_sym_table ctxt monom_constrs format conj_sym_kind + mono type_enc app_op_aliases sym_tab val sym_decl_lines = - (conjs, helpers @ facts) + (conjs, helpers @ facts, app_op_alias_eq_tms) |> sym_decl_table_for_facts ctxt format type_enc sym_tab |> problem_lines_for_sym_decl_table ctxt format conj_sym_kind mono type_enc mono_Ts @@ -2499,6 +2604,7 @@ FLOTTER hack. *) val problem = [(explicit_declsN, class_decl_lines @ sym_decl_lines), + (app_op_alias_eqsN, app_op_alias_eq_lines), (factsN, map (formula_line_for_fact ctxt polym_constrs format fact_prefix ascii_of (not exporter) (not exporter) mono type_enc) diff -r 8d8d3c1f1854 -r 676a4b4b6e73 src/HOL/Tools/Metis/metis_reconstruct.ML --- a/src/HOL/Tools/Metis/metis_reconstruct.ML Wed Feb 01 17:16:55 2012 +0100 +++ b/src/HOL/Tools/Metis/metis_reconstruct.ML Thu Feb 02 01:20:28 2012 +0100 @@ -337,7 +337,7 @@ let val s = s |> Metis_Name.toString |> perhaps (try (unprefix_and_unascii const_prefix - #> the #> unmangled_const_name)) + #> the #> unmangled_const_name #> hd)) in if s = metis_predicator orelse s = predicator_name orelse s = metis_systematic_type_tag orelse s = metis_ad_hoc_type_tag