1284 end |
1284 end |
1285 |
1285 |
1286 fun is_format_with_defs (THF _) = true |
1286 fun is_format_with_defs (THF _) = true |
1287 | is_format_with_defs _ = false |
1287 | is_format_with_defs _ = false |
1288 |
1288 |
1289 fun make_fact ctxt format type_enc iff_for_eq |
1289 fun make_fact ctxt format type_enc iff_for_eq ((name, stature as (_, status)), t) = |
1290 ((name, stature as (_, status)), t) = |
|
1291 let |
1290 let |
1292 val role = |
1291 val role = |
1293 if is_format_with_defs format andalso status = Non_Rec_Def andalso |
1292 if is_format_with_defs format andalso status = Non_Rec_Def andalso |
1294 is_legitimate_tptp_def t then |
1293 is_legitimate_tptp_def t then |
1295 Definition |
1294 Definition |
1740 not (is_type_enc_polymorphic type_enc) andalso level_of_type_enc type_enc <> No_Types |
1739 not (is_type_enc_polymorphic type_enc) andalso level_of_type_enc type_enc <> No_Types |
1741 |
1740 |
1742 fun should_specialize_helper type_enc t = |
1741 fun should_specialize_helper type_enc t = |
1743 could_specialize_helpers type_enc andalso not (null (Term.hidden_polymorphism t)) |
1742 could_specialize_helpers type_enc andalso not (null (Term.hidden_polymorphism t)) |
1744 |
1743 |
1745 fun add_helper_facts_of_sym ctxt format type_enc completish |
1744 fun add_helper_facts_of_sym ctxt format type_enc completish (s, {types, ...} : sym_info) = |
1746 (s, {types, ...} : sym_info) = |
|
1747 (case unprefix_and_unascii const_prefix s of |
1745 (case unprefix_and_unascii const_prefix s of |
1748 SOME mangled_s => |
1746 SOME mangled_s => |
1749 let |
1747 let |
1750 val thy = Proof_Context.theory_of ctxt |
1748 val thy = Proof_Context.theory_of ctxt |
1751 val unmangled_s = mangled_s |> unmangled_const_name |> hd |
1749 val unmangled_s = mangled_s |> unmangled_const_name |> hd |
1783 |> union (op = o pairself #iformula)) |
1781 |> union (op = o pairself #iformula)) |
1784 (if completish then completish_helper_table else helper_table) |
1782 (if completish then completish_helper_table else helper_table) |
1785 end |
1783 end |
1786 | NONE => I) |
1784 | NONE => I) |
1787 fun helper_facts_of_sym_table ctxt format type_enc completish sym_tab = |
1785 fun helper_facts_of_sym_table ctxt format type_enc completish sym_tab = |
1788 Symtab.fold_rev (add_helper_facts_of_sym ctxt format type_enc completish) |
1786 Symtab.fold_rev (add_helper_facts_of_sym ctxt format type_enc completish) sym_tab [] |
1789 sym_tab [] |
|
1790 |
1787 |
1791 (***************************************************************) |
1788 (***************************************************************) |
1792 (* Type Classes Present in the Axiom or Conjecture Clauses *) |
1789 (* Type Classes Present in the Axiom or Conjecture Clauses *) |
1793 (***************************************************************) |
1790 (***************************************************************) |
1794 |
1791 |
2436 val syms = sym_decl_tab |> Symtab.dest |> sort_wrt fst |
2433 val syms = sym_decl_tab |> Symtab.dest |> sort_wrt fst |
2437 val mono_lines = lines_of_mono_types ctxt mono type_enc mono_Ts |
2434 val mono_lines = lines_of_mono_types ctxt mono type_enc mono_Ts |
2438 val decl_lines = maps (lines_of_sym_decls ctxt mono type_enc) syms |
2435 val decl_lines = maps (lines_of_sym_decls ctxt mono type_enc) syms |
2439 in mono_lines @ decl_lines end |
2436 in mono_lines @ decl_lines end |
2440 |
2437 |
2441 fun datatypes_of_sym_table ctxt ctrss (DFG Polymorphic) (type_enc as Native _) |
2438 fun datatypes_of_sym_table ctxt ctrss (DFG Polymorphic) (type_enc as Native _) uncurried_aliases |
2442 uncurried_aliases sym_tab = |
2439 sym_tab = |
2443 if is_type_enc_polymorphic type_enc then |
2440 if is_type_enc_polymorphic type_enc then |
2444 let |
2441 let |
2445 val thy = Proof_Context.theory_of ctxt |
2442 val thy = Proof_Context.theory_of ctxt |
|
2443 |
2446 fun do_ctr (s, T) = |
2444 fun do_ctr (s, T) = |
2447 let |
2445 let |
2448 val s' = make_fixed_const (SOME type_enc) s |
2446 val s' = make_fixed_const (SOME type_enc) s |
2449 val ary = ary_of T |
2447 val ary = ary_of T |
2450 fun mk name = mk_aterm type_enc name (robust_const_type_args thy (s, T)) [] |
2448 fun mk name = SOME (mk_aterm type_enc name (robust_const_type_args thy (s, T)) []) |
2451 in |
2449 in |
2452 (case Symtab.lookup sym_tab s' of |
2450 if T = HOLogic.boolT then |
2453 NONE => NONE |
2451 (case proxify_const s' of |
2454 | SOME ({min_ary, ...} : sym_info) => |
2452 SOME proxy_base => mk (proxy_base |>> prefix const_prefix) |
2455 if ary = min_ary then SOME (mk (s', s)) |
2453 | NONE => NONE) |
2456 else if uncurried_aliases then SOME (mk (aliased_uncurried ary (s', s))) |
2454 else |
2457 else NONE) |
2455 (case Symtab.lookup sym_tab s' of |
|
2456 NONE => NONE |
|
2457 | SOME ({min_ary, ...} : sym_info) => |
|
2458 if ary = min_ary then mk (s', s) |
|
2459 else if uncurried_aliases then mk (aliased_uncurried ary (s', s)) |
|
2460 else NONE) |
2458 end |
2461 end |
|
2462 |
2459 fun datatype_of_ctrs (ctrs as (_, T1) :: _) = |
2463 fun datatype_of_ctrs (ctrs as (_, T1) :: _) = |
2460 let val ctrs' = map do_ctr ctrs in |
2464 let val ctrs' = map do_ctr ctrs in |
2461 if forall is_some ctrs' then |
2465 if forall is_some ctrs' then |
2462 SOME (native_atp_type_of_typ type_enc false 0 (body_type T1), map_filter I ctrs') |
2466 SOME (native_atp_type_of_typ type_enc false 0 (body_type T1), map_filter I ctrs') |
2463 else |
2467 else |
2608 | (s, (ty, ary)) => cons (Type_Decl (type_decl_prefix ^ s, ty, ary))) tys [] @ |
2612 | (s, (ty, ary)) => cons (Type_Decl (type_decl_prefix ^ s, ty, ary))) tys [] @ |
2609 Symtab.fold (fn (_, (("", ""), _)) => I (* already declared *) |
2613 Symtab.fold (fn (_, (("", ""), _)) => I (* already declared *) |
2610 | (s, (sym, ty)) => cons (Sym_Decl (sym_decl_prefix ^ s, sym, ty ()))) syms [] |
2614 | (s, (sym, ty)) => cons (Sym_Decl (sym_decl_prefix ^ s, sym, ty ()))) syms [] |
2611 in (heading, decls) :: problem end |
2615 in (heading, decls) :: problem end |
2612 |
2616 |
2613 fun all_ctrss_of_datatypes ctxt = |
2617 val all_ctrss_of_datatypes = map (map_filter (try dest_Const) o #ctrs) o Ctr_Sugar.ctr_sugars_of |
2614 map (map_filter (try dest_Const) o #ctrs) (Ctr_Sugar.ctr_sugars_of ctxt) |
|
2615 |
2618 |
2616 val app_op_and_predicator_threshold = 45 |
2619 val app_op_and_predicator_threshold = 45 |
2617 |
2620 |
2618 fun prepare_atp_problem ctxt format prem_role type_enc mode lam_trans uncurried_aliases |
2621 fun prepare_atp_problem ctxt format prem_role type_enc mode lam_trans uncurried_aliases |
2619 readable_names presimp hyp_ts concl_t facts = |
2622 readable_names presimp hyp_ts concl_t facts = |