32 val helper_prefix : string |
32 val helper_prefix : string |
33 val typed_helper_suffix : string |
33 val typed_helper_suffix : string |
34 val predicator_base : string |
34 val predicator_base : string |
35 val explicit_app_base : string |
35 val explicit_app_base : string |
36 val type_pred_base : string |
36 val type_pred_base : string |
37 val tff_type_prefix : string |
37 val simple_type_prefix : string |
38 val type_sys_from_string : string -> type_system |
38 val type_sys_from_string : string -> type_system |
39 val polymorphism_of_type_sys : type_system -> polymorphism |
39 val polymorphism_of_type_sys : type_system -> polymorphism |
40 val level_of_type_sys : type_system -> type_level |
40 val level_of_type_sys : type_system -> type_level |
41 val is_type_sys_virtually_sound : type_system -> bool |
41 val is_type_sys_virtually_sound : type_system -> bool |
42 val is_type_sys_fairly_sound : type_system -> bool |
42 val is_type_sys_fairly_sound : type_system -> bool |
43 val unmangled_const : string -> string * string fo_term list |
43 val unmangled_const : string -> string * string fo_term list |
44 val translate_atp_fact : |
44 val translate_atp_fact : |
45 Proof.context -> bool -> (string * locality) * thm |
45 Proof.context -> format -> bool -> (string * locality) * thm |
46 -> translated_formula option * ((string * locality) * thm) |
46 -> translated_formula option * ((string * locality) * thm) |
47 val prepare_atp_problem : |
47 val prepare_atp_problem : |
48 Proof.context -> format -> formula_kind -> formula_kind -> type_system |
48 Proof.context -> format -> formula_kind -> formula_kind -> type_system |
49 -> bool -> term list -> term |
49 -> bool -> term list -> term |
50 -> (translated_formula option * ((string * 'a) * thm)) list |
50 -> (translated_formula option * ((string * 'a) * thm)) list |
277 fun term_vars (ATerm (name as (s, _), tms)) = |
278 fun term_vars (ATerm (name as (s, _), tms)) = |
278 is_atp_variable s ? insert (op =) (name, NONE) |
279 is_atp_variable s ? insert (op =) (name, NONE) |
279 #> fold term_vars tms |
280 #> fold term_vars tms |
280 fun close_formula_universally phi = close_universally term_vars phi |
281 fun close_formula_universally phi = close_universally term_vars phi |
281 |
282 |
282 fun fo_term_from_typ (Type (s, Ts)) = |
283 fun fo_term_from_typ format (Type (s, Ts)) = |
283 ATerm (`make_fixed_type_const s, map fo_term_from_typ Ts) |
284 ATerm (if format = THF andalso s = @{type_name bool} then `I tptp_bool_type |
284 | fo_term_from_typ (TFree (s, _)) = |
285 else `make_fixed_type_const s, |
285 ATerm (`make_fixed_type_var s, []) |
286 map (fo_term_from_typ format) Ts) |
286 | fo_term_from_typ (TVar ((x as (s, _)), _)) = |
287 | fo_term_from_typ _ (TFree (s, _)) = ATerm (`make_fixed_type_var s, []) |
|
288 | fo_term_from_typ _ (TVar ((x as (s, _)), _)) = |
287 ATerm ((make_schematic_type_var x, s), []) |
289 ATerm ((make_schematic_type_var x, s), []) |
288 |
290 |
289 (* This shouldn't clash with anything else. *) |
291 (* This shouldn't clash with anything else. *) |
290 val mangled_type_sep = "\000" |
292 val mangled_type_sep = "\000" |
291 |
293 |
292 fun generic_mangled_type_name f (ATerm (name, [])) = f name |
294 fun generic_mangled_type_name f (ATerm (name, [])) = f name |
293 | generic_mangled_type_name f (ATerm (name, tys)) = |
295 | generic_mangled_type_name f (ATerm (name, tys)) = |
294 f name ^ "(" ^ space_implode "," (map (generic_mangled_type_name f) tys) |
296 f name ^ "(" ^ space_implode "," (map (generic_mangled_type_name f) tys) |
295 ^ ")" |
297 ^ ")" |
296 val mangled_type_name = |
298 fun mangled_type_name format = |
297 fo_term_from_typ |
299 fo_term_from_typ format |
298 #> (fn ty => (make_tff_type (generic_mangled_type_name fst ty), |
300 #> (fn ty => (make_simple_type (generic_mangled_type_name fst ty), |
299 generic_mangled_type_name snd ty)) |
301 generic_mangled_type_name snd ty)) |
300 |
302 |
301 fun generic_mangled_type_suffix f g Ts = |
303 fun generic_mangled_type_suffix f g Ts = |
302 fold_rev (curry (op ^) o g o prefix mangled_type_sep |
304 fold_rev (curry (op ^) o g o prefix mangled_type_sep |
303 o generic_mangled_type_name f) Ts "" |
305 o generic_mangled_type_name f) Ts "" |
304 fun mangled_const_name T_args (s, s') = |
306 fun mangled_const_name format T_args (s, s') = |
305 let val ty_args = map fo_term_from_typ T_args in |
307 let val ty_args = map (fo_term_from_typ format) T_args in |
306 (s ^ generic_mangled_type_suffix fst ascii_of ty_args, |
308 (s ^ generic_mangled_type_suffix fst ascii_of ty_args, |
307 s' ^ generic_mangled_type_suffix snd I ty_args) |
309 s' ^ generic_mangled_type_suffix snd I ty_args) |
308 end |
310 end |
309 |
311 |
310 val parse_mangled_ident = |
312 val parse_mangled_ident = |
328 fun unmangled_const s = |
330 fun unmangled_const s = |
329 let val ss = space_explode mangled_type_sep s in |
331 let val ss = space_explode mangled_type_sep s in |
330 (hd ss, map unmangled_type (tl ss)) |
332 (hd ss, map unmangled_type (tl ss)) |
331 end |
333 end |
332 |
334 |
333 fun introduce_proxies tm = |
335 fun introduce_proxies format tm = |
334 let |
336 let |
335 fun aux top_level (CombApp (tm1, tm2)) = |
337 fun aux top_level (CombApp (tm1, tm2)) = |
336 CombApp (aux top_level tm1, aux false tm2) |
338 CombApp (aux top_level tm1, aux false tm2) |
337 | aux top_level (CombConst (name as (s, s'), T, T_args)) = |
339 | aux top_level (CombConst (name as (s, s'), T, T_args)) = |
338 (case proxify_const s of |
340 (case proxify_const s of |
339 SOME proxy_base => |
341 SOME proxy_base => |
340 if top_level then |
342 if top_level orelse format = THF then |
341 (case s of |
343 (case s of |
342 "c_False" => (tptp_false, s') |
344 "c_False" => (tptp_false, s') |
343 | "c_True" => (tptp_true, s') |
345 | "c_True" => (tptp_true, s') |
344 | _ => name, []) |
346 | _ => name, []) |
345 else |
347 else |
347 | NONE => (name, T_args)) |
349 | NONE => (name, T_args)) |
348 |> (fn (name, T_args) => CombConst (name, T, T_args)) |
350 |> (fn (name, T_args) => CombConst (name, T, T_args)) |
349 | aux _ tm = tm |
351 | aux _ tm = tm |
350 in aux true tm end |
352 in aux true tm end |
351 |
353 |
352 fun combformula_from_prop thy eq_as_iff = |
354 fun combformula_from_prop thy format eq_as_iff = |
353 let |
355 let |
354 fun do_term bs t atomic_types = |
356 fun do_term bs t atomic_types = |
355 combterm_from_term thy bs (Envir.eta_contract t) |
357 combterm_from_term thy bs (Envir.eta_contract t) |
356 |>> (introduce_proxies #> AAtom) |
358 |>> (introduce_proxies format #> AAtom) |
357 ||> union (op =) atomic_types |
359 ||> union (op =) atomic_types |
358 fun do_quant bs q s T t' = |
360 fun do_quant bs q s T t' = |
359 let val s = Name.variant (map fst bs) s in |
361 let val s = Name.variant (map fst bs) s in |
360 do_formula ((s, T) :: bs) t' |
362 do_formula ((s, T) :: bs) t' |
361 #>> mk_aquant q [(`make_bound_var s, SOME T)] |
363 #>> mk_aquant q [(`make_bound_var s, SOME T)] |
462 |> extensionalize_term ctxt |
464 |> extensionalize_term ctxt |
463 |> presimp ? presimplify_term ctxt |
465 |> presimp ? presimplify_term ctxt |
464 |> perhaps (try (HOLogic.dest_Trueprop)) |
466 |> perhaps (try (HOLogic.dest_Trueprop)) |
465 |> introduce_combinators_in_term ctxt kind |
467 |> introduce_combinators_in_term ctxt kind |
466 |> kind <> Axiom ? freeze_term |
468 |> kind <> Axiom ? freeze_term |
467 val (combformula, atomic_types) = combformula_from_prop thy eq_as_iff t [] |
469 val (combformula, atomic_types) = |
|
470 combformula_from_prop thy format eq_as_iff t [] |
468 in |
471 in |
469 {name = name, locality = loc, kind = kind, combformula = combformula, |
472 {name = name, locality = loc, kind = kind, combformula = combformula, |
470 atomic_types = atomic_types} |
473 atomic_types = atomic_types} |
471 end |
474 end |
472 |
475 |
473 fun make_fact ctxt keep_trivial eq_as_iff presimp ((name, loc), t) = |
476 fun make_fact ctxt format keep_trivial eq_as_iff presimp ((name, loc), t) = |
474 case (keep_trivial, make_formula ctxt eq_as_iff presimp name loc Axiom t) of |
477 case (keep_trivial, |
|
478 make_formula ctxt format eq_as_iff presimp name loc Axiom t) of |
475 (false, {combformula = AAtom (CombConst (("c_True", _), _, _)), ...}) => |
479 (false, {combformula = AAtom (CombConst (("c_True", _), _, _)), ...}) => |
476 NONE |
480 NONE |
477 | (_, formula) => SOME formula |
481 | (_, formula) => SOME formula |
478 |
482 |
479 fun make_conjecture ctxt prem_kind ts = |
483 fun make_conjecture ctxt format prem_kind ts = |
480 let val last = length ts - 1 in |
484 let val last = length ts - 1 in |
481 map2 (fn j => fn t => |
485 map2 (fn j => fn t => |
482 let |
486 let |
483 val (kind, maybe_negate) = |
487 val (kind, maybe_negate) = |
484 if j = last then |
488 if j = last then |
704 in |
709 in |
705 case type_arg_policy type_sys s'' of |
710 case type_arg_policy type_sys s'' of |
706 Explicit_Type_Args drop_args => |
711 Explicit_Type_Args drop_args => |
707 (name, filtered_T_args drop_args) |
712 (name, filtered_T_args drop_args) |
708 | Mangled_Type_Args drop_args => |
713 | Mangled_Type_Args drop_args => |
709 (mangled_const_name (filtered_T_args drop_args) name, []) |
714 (mangled_const_name format (filtered_T_args drop_args) name, |
|
715 []) |
710 | No_Type_Args => (name, []) |
716 | No_Type_Args => (name, []) |
711 end) |
717 end) |
712 |> (fn (name, T_args) => CombConst (name, T, T_args)) |
718 |> (fn (name, T_args) => CombConst (name, T, T_args)) |
713 end |
719 end |
714 | aux _ tm = tm |
720 | aux _ tm = tm |
715 in aux 0 end |
721 in aux 0 end |
716 |
722 |
717 fun repair_combterm ctxt nonmono_Ts type_sys sym_tab = |
723 fun repair_combterm ctxt format nonmono_Ts type_sys sym_tab = |
718 introduce_explicit_apps_in_combterm sym_tab |
724 format <> THF ? (introduce_explicit_apps_in_combterm sym_tab |
719 #> introduce_predicators_in_combterm sym_tab |
725 #> introduce_predicators_in_combterm sym_tab) |
720 #> enforce_type_arg_policy_in_combterm ctxt nonmono_Ts type_sys |
726 #> enforce_type_arg_policy_in_combterm ctxt format nonmono_Ts type_sys |
721 fun repair_fact ctxt nonmono_Ts type_sys sym_tab = |
727 fun repair_fact ctxt format nonmono_Ts type_sys sym_tab = |
722 update_combformula (formula_map |
728 update_combformula (formula_map |
723 (repair_combterm ctxt nonmono_Ts type_sys sym_tab)) |
729 (repair_combterm ctxt format nonmono_Ts type_sys sym_tab)) |
724 |
730 |
725 (** Helper facts **) |
731 (** Helper facts **) |
726 |
732 |
727 fun ti_ti_helper_fact () = |
733 fun ti_ti_helper_fact () = |
728 let |
734 let |
732 Formula (helper_prefix ^ "ti_ti", Axiom, |
738 Formula (helper_prefix ^ "ti_ti", Axiom, |
733 AAtom (ATerm (`I "equal", [tag (tag (var "Y")), tag (var "Y")])) |
739 AAtom (ATerm (`I "equal", [tag (tag (var "Y")), tag (var "Y")])) |
734 |> close_formula_universally, simp_info, NONE) |
740 |> close_formula_universally, simp_info, NONE) |
735 end |
741 end |
736 |
742 |
737 fun helper_facts_for_sym ctxt type_sys (s, {typ, ...} : sym_info) = |
743 fun helper_facts_for_sym ctxt format type_sys (s, {typ, ...} : sym_info) = |
738 case strip_prefix_and_unascii const_prefix s of |
744 case strip_prefix_and_unascii const_prefix s of |
739 SOME mangled_s => |
745 SOME mangled_s => |
740 let |
746 let |
741 val thy = Proof_Context.theory_of ctxt |
747 val thy = Proof_Context.theory_of ctxt |
742 val unmangled_s = mangled_s |> unmangled_const_name |
748 val unmangled_s = mangled_s |> unmangled_const_name |
767 ths ~~ (1 upto length ths) |
773 ths ~~ (1 upto length ths) |
768 |> map (dub_and_inst mangled_s needs_fairly_sound) |
774 |> map (dub_and_inst mangled_s needs_fairly_sound) |
769 |> make_facts (not needs_fairly_sound)) |
775 |> make_facts (not needs_fairly_sound)) |
770 end |
776 end |
771 | NONE => [] |
777 | NONE => [] |
772 fun helper_facts_for_sym_table ctxt type_sys sym_tab = |
778 fun helper_facts_for_sym_table ctxt format type_sys sym_tab = |
773 Symtab.fold_rev (append o helper_facts_for_sym ctxt type_sys) sym_tab [] |
779 Symtab.fold_rev (append o helper_facts_for_sym ctxt format type_sys) sym_tab |
774 |
780 [] |
775 fun translate_atp_fact ctxt keep_trivial = |
781 |
776 `(make_fact ctxt keep_trivial true true o apsnd prop_of) |
782 fun translate_atp_fact ctxt format keep_trivial = |
777 |
783 `(make_fact ctxt format keep_trivial true true o apsnd prop_of) |
778 fun translate_formulas ctxt prem_kind type_sys hyp_ts concl_t rich_facts = |
784 |
|
785 fun translate_formulas ctxt format prem_kind type_sys hyp_ts concl_t |
|
786 rich_facts = |
779 let |
787 let |
780 val thy = Proof_Context.theory_of ctxt |
788 val thy = Proof_Context.theory_of ctxt |
781 val fact_ts = map (prop_of o snd o snd) rich_facts |
789 val fact_ts = map (prop_of o snd o snd) rich_facts |
782 val (facts, fact_names) = |
790 val (facts, fact_names) = |
783 rich_facts |
791 rich_facts |
790 val goal_t = Logic.list_implies (hyp_ts, concl_t) |
798 val goal_t = Logic.list_implies (hyp_ts, concl_t) |
791 val all_ts = goal_t :: fact_ts |
799 val all_ts = goal_t :: fact_ts |
792 val subs = tfree_classes_of_terms all_ts |
800 val subs = tfree_classes_of_terms all_ts |
793 val supers = tvar_classes_of_terms all_ts |
801 val supers = tvar_classes_of_terms all_ts |
794 val tycons = type_consts_of_terms thy all_ts |
802 val tycons = type_consts_of_terms thy all_ts |
795 val conjs = make_conjecture ctxt prem_kind (hyp_ts @ [concl_t]) |
803 val conjs = make_conjecture ctxt format prem_kind (hyp_ts @ [concl_t]) |
796 val (supers', arity_clauses) = |
804 val (supers', arity_clauses) = |
797 if level_of_type_sys type_sys = No_Types then ([], []) |
805 if level_of_type_sys type_sys = No_Types then ([], []) |
798 else make_arity_clauses thy tycons supers |
806 else make_arity_clauses thy tycons supers |
799 val class_rel_clauses = make_class_rel_clauses thy subs supers' |
807 val class_rel_clauses = make_class_rel_clauses thy subs supers' |
800 in |
808 in |
806 | fo_literal_from_type_literal (TyLitFree (class, name)) = |
814 | fo_literal_from_type_literal (TyLitFree (class, name)) = |
807 (true, ATerm (class, [ATerm (name, [])])) |
815 (true, ATerm (class, [ATerm (name, [])])) |
808 |
816 |
809 fun formula_from_fo_literal (pos, t) = AAtom t |> not pos ? mk_anot |
817 fun formula_from_fo_literal (pos, t) = AAtom t |> not pos ? mk_anot |
810 |
818 |
811 fun type_pred_combterm ctxt nonmono_Ts type_sys T tm = |
819 fun type_pred_combterm ctxt format nonmono_Ts type_sys T tm = |
812 CombApp (CombConst (`make_fixed_const type_pred_base, T --> @{typ bool}, [T]) |
820 CombApp (CombConst (`make_fixed_const type_pred_base, T --> @{typ bool}, [T]) |
813 |> enforce_type_arg_policy_in_combterm ctxt nonmono_Ts type_sys, |
821 |> enforce_type_arg_policy_in_combterm ctxt format nonmono_Ts |
|
822 type_sys, |
814 tm) |
823 tm) |
815 |
824 |
816 fun var_occurs_positively_naked_in_term _ (SOME false) _ accum = accum |
825 fun var_occurs_positively_naked_in_term _ (SOME false) _ accum = accum |
817 | var_occurs_positively_naked_in_term name _ (ATerm ((s, _), tms)) accum = |
826 | var_occurs_positively_naked_in_term name _ (ATerm ((s, _), tms)) accum = |
818 accum orelse (s = "equal" andalso member (op =) tms (ATerm (name, []))) |
827 accum orelse (s = "equal" andalso member (op =) tms (ATerm (name, []))) |
819 fun is_var_nonmonotonic_in_formula _ _ (SOME false) _ = false |
828 fun is_var_nonmonotonic_in_formula _ _ (SOME false) _ = false |
820 | is_var_nonmonotonic_in_formula pos phi _ name = |
829 | is_var_nonmonotonic_in_formula pos phi _ name = |
821 formula_fold pos (var_occurs_positively_naked_in_term name) phi false |
830 formula_fold pos (var_occurs_positively_naked_in_term name) phi false |
822 |
831 |
823 fun tag_with_type ctxt nonmono_Ts type_sys T tm = |
832 fun tag_with_type ctxt format nonmono_Ts type_sys T tm = |
824 CombConst (`make_fixed_const type_tag_name, T --> T, [T]) |
833 CombConst (`make_fixed_const type_tag_name, T --> T, [T]) |
825 |> enforce_type_arg_policy_in_combterm ctxt nonmono_Ts type_sys |
834 |> enforce_type_arg_policy_in_combterm ctxt format nonmono_Ts type_sys |
826 |> term_from_combterm ctxt nonmono_Ts type_sys Top_Level |
835 |> term_from_combterm ctxt format nonmono_Ts type_sys Top_Level |
827 |> (fn ATerm (s, tms) => ATerm (s, tms @ [tm])) |
836 |> (fn ATerm (s, tms) => ATerm (s, tms @ [tm])) |
828 and term_from_combterm ctxt nonmono_Ts type_sys site u = |
837 and term_from_combterm ctxt format nonmono_Ts type_sys = |
829 let |
838 let |
830 val (head, args) = strip_combterm_comb u |
839 fun aux site u = |
831 val (x as (s, _), T_args) = |
840 let |
832 case head of |
841 val (head, args) = strip_combterm_comb u |
833 CombConst (name, _, T_args) => (name, T_args) |
842 val (x as (s, _), T_args) = |
834 | CombVar (name, _) => (name, []) |
843 case head of |
835 | CombApp _ => raise Fail "impossible \"CombApp\"" |
844 CombConst (name, _, T_args) => (name, T_args) |
836 val arg_site = if site = Top_Level andalso s = "equal" then Eq_Arg |
845 | CombVar (name, _) => (name, []) |
837 else Elsewhere |
846 | CombApp _ => raise Fail "impossible \"CombApp\"" |
838 val t = ATerm (x, map fo_term_from_typ T_args @ |
847 val arg_site = if site = Top_Level andalso s = "equal" then Eq_Arg |
839 map (term_from_combterm ctxt nonmono_Ts type_sys arg_site) |
848 else Elsewhere |
840 args) |
849 val t = ATerm (x, map (fo_term_from_typ format) T_args @ |
841 val T = combtyp_of u |
850 map (aux arg_site) args) |
842 in |
851 val T = combtyp_of u |
843 t |> (if should_tag_with_type ctxt nonmono_Ts type_sys site u T then |
852 in |
844 tag_with_type ctxt nonmono_Ts type_sys T |
853 t |> (if should_tag_with_type ctxt nonmono_Ts type_sys site u T then |
845 else |
854 tag_with_type ctxt format nonmono_Ts type_sys T |
846 I) |
855 else |
847 end |
856 I) |
848 and formula_from_combformula ctxt nonmono_Ts type_sys should_predicate_on_var = |
857 end |
849 let |
858 in aux end |
850 val do_term = term_from_combterm ctxt nonmono_Ts type_sys Top_Level |
859 and formula_from_combformula ctxt format nonmono_Ts type_sys |
|
860 should_predicate_on_var = |
|
861 let |
|
862 val do_term = term_from_combterm ctxt format nonmono_Ts type_sys Top_Level |
851 val do_bound_type = |
863 val do_bound_type = |
852 case type_sys of |
864 case type_sys of |
853 Simple_Types level => |
865 Simple_Types level => |
854 SOME o mangled_type_name o homogenized_type ctxt nonmono_Ts level |
866 SOME o mangled_type_name format o homogenized_type ctxt nonmono_Ts level |
855 | _ => K NONE |
867 | _ => K NONE |
856 fun do_out_of_bound_type pos phi universal (name, T) = |
868 fun do_out_of_bound_type pos phi universal (name, T) = |
857 if should_predicate_on_type ctxt nonmono_Ts type_sys |
869 if should_predicate_on_type ctxt nonmono_Ts type_sys |
858 (fn () => should_predicate_on_var pos phi universal name) T then |
870 (fn () => should_predicate_on_var pos phi universal name) T then |
859 CombVar (name, T) |
871 CombVar (name, T) |
860 |> type_pred_combterm ctxt nonmono_Ts type_sys T |
872 |> type_pred_combterm ctxt format nonmono_Ts type_sys T |
861 |> do_term |> AAtom |> SOME |
873 |> do_term |> AAtom |> SOME |
862 else |
874 else |
863 NONE |
875 NONE |
864 fun do_formula pos (AQuant (q, xs, phi)) = |
876 fun do_formula pos (AQuant (q, xs, phi)) = |
865 let |
877 let |
929 o fo_literal_from_arity_literal) prem_lits) |
941 o fo_literal_from_arity_literal) prem_lits) |
930 (formula_from_fo_literal |
942 (formula_from_fo_literal |
931 (fo_literal_from_arity_literal concl_lits)) |
943 (fo_literal_from_arity_literal concl_lits)) |
932 |> close_formula_universally, intro_info, NONE) |
944 |> close_formula_universally, intro_info, NONE) |
933 |
945 |
934 fun formula_line_for_conjecture ctxt nonmono_Ts type_sys |
946 fun formula_line_for_conjecture ctxt format nonmono_Ts type_sys |
935 ({name, kind, combformula, ...} : translated_formula) = |
947 ({name, kind, combformula, ...} : translated_formula) = |
936 Formula (conjecture_prefix ^ name, kind, |
948 Formula (conjecture_prefix ^ name, kind, |
937 formula_from_combformula ctxt nonmono_Ts type_sys |
949 formula_from_combformula ctxt format nonmono_Ts type_sys |
938 is_var_nonmonotonic_in_formula false |
950 is_var_nonmonotonic_in_formula false |
939 (close_combformula_universally combformula) |
951 (close_combformula_universally combformula) |
940 |> close_formula_universally, NONE, NONE) |
952 |> close_formula_universally, NONE, NONE) |
941 |
953 |
942 fun free_type_literals format type_sys |
954 fun free_type_literals format type_sys |
1025 |> insert_type ctxt I @{typ bool} |
1037 |> insert_type ctxt I @{typ bool} |
1026 else |
1038 else |
1027 [] |
1039 [] |
1028 end |
1040 end |
1029 |
1041 |
1030 fun decl_line_for_sym ctxt nonmono_Ts level s (s', _, T, pred_sym, ary, _) = |
1042 fun decl_line_for_sym ctxt format nonmono_Ts level s |
|
1043 (s', _, T, pred_sym, ary, _) = |
1031 let |
1044 let |
1032 val translate_type = |
1045 val translate_type = |
1033 mangled_type_name o homogenized_type ctxt nonmono_Ts level |
1046 mangled_type_name format o homogenized_type ctxt nonmono_Ts level |
1034 val (arg_tys, res_ty) = |
1047 val (arg_tys, res_ty) = |
1035 T |> chop_fun ary |>> map translate_type ||> translate_type |
1048 T |> chop_fun ary |>> map translate_type ||> translate_type |
1036 in |
1049 in |
1037 Decl (sym_decl_prefix ^ s, (s, s'), arg_tys, |
1050 Decl (sym_decl_prefix ^ s, (s, s'), arg_tys, |
1038 if pred_sym then `I tptp_tff_bool_type else res_ty) |
1051 if pred_sym then `I tptp_bool_type else res_ty) |
1039 end |
1052 end |
1040 |
1053 |
1041 fun is_polymorphic_type T = fold_atyps (fn TVar _ => K true | _ => I) T false |
1054 fun is_polymorphic_type T = fold_atyps (fn TVar _ => K true | _ => I) T false |
1042 |
1055 |
1043 fun formula_line_for_pred_sym_decl ctxt format conj_sym_kind nonmono_Ts type_sys |
1056 fun formula_line_for_pred_sym_decl ctxt format conj_sym_kind nonmono_Ts type_sys |
1057 in |
1070 in |
1058 Formula (sym_decl_prefix ^ s ^ |
1071 Formula (sym_decl_prefix ^ s ^ |
1059 (if n > 1 then "_" ^ string_of_int j else ""), kind, |
1072 (if n > 1 then "_" ^ string_of_int j else ""), kind, |
1060 CombConst ((s, s'), T, T_args) |
1073 CombConst ((s, s'), T, T_args) |
1061 |> fold (curry (CombApp o swap)) bounds |
1074 |> fold (curry (CombApp o swap)) bounds |
1062 |> type_pred_combterm ctxt nonmono_Ts type_sys res_T |
1075 |> type_pred_combterm ctxt format nonmono_Ts type_sys res_T |
1063 |> AAtom |
1076 |> AAtom |
1064 |> mk_aquant AForall (bound_names ~~ bound_Ts) |
1077 |> mk_aquant AForall (bound_names ~~ bound_Ts) |
1065 |> formula_from_combformula ctxt nonmono_Ts type_sys |
1078 |> formula_from_combformula ctxt format nonmono_Ts type_sys |
1066 (K (K (K (K true)))) true |
1079 (K (K (K (K true)))) true |
1067 |> n > 1 ? bound_atomic_types format type_sys (atyps_of T) |
1080 |> n > 1 ? bound_atomic_types format type_sys (atyps_of T) |
1068 |> close_formula_universally |
1081 |> close_formula_universally |
1069 |> maybe_negate, |
1082 |> maybe_negate, |
1070 intro_info, NONE) |
1083 intro_info, NONE) |
1080 else (Axiom, I) |
1093 else (Axiom, I) |
1081 val (arg_Ts, res_T) = chop_fun ary T |
1094 val (arg_Ts, res_T) = chop_fun ary T |
1082 val bound_names = |
1095 val bound_names = |
1083 1 upto length arg_Ts |> map (`I o make_bound_var o string_of_int) |
1096 1 upto length arg_Ts |> map (`I o make_bound_var o string_of_int) |
1084 val bounds = bound_names |> map (fn name => ATerm (name, [])) |
1097 val bounds = bound_names |> map (fn name => ATerm (name, [])) |
1085 fun const args = ATerm ((s, s'), map fo_term_from_typ T_args @ args) |
1098 fun const args = |
|
1099 ATerm ((s, s'), map (fo_term_from_typ format) T_args @ args) |
1086 val atomic_Ts = atyps_of T |
1100 val atomic_Ts = atyps_of T |
1087 fun eq tms = |
1101 fun eq tms = |
1088 (if pred_sym then AConn (AIff, map AAtom tms) |
1102 (if pred_sym then AConn (AIff, map AAtom tms) |
1089 else AAtom (ATerm (`I "equal", tms))) |
1103 else AAtom (ATerm (`I "equal", tms))) |
1090 |> bound_atomic_types format type_sys atomic_Ts |
1104 |> bound_atomic_types format type_sys atomic_Ts |
1091 |> close_formula_universally |
1105 |> close_formula_universally |
1092 |> maybe_negate |
1106 |> maybe_negate |
1093 val should_encode = should_encode_type ctxt nonmono_Ts All_Types |
1107 val should_encode = should_encode_type ctxt nonmono_Ts All_Types |
1094 val tag_with = tag_with_type ctxt nonmono_Ts type_sys |
1108 val tag_with = tag_with_type ctxt format nonmono_Ts type_sys |
1095 val add_formula_for_res = |
1109 val add_formula_for_res = |
1096 if should_encode res_T then |
1110 if should_encode res_T then |
1097 cons (Formula (ident_base ^ "_res", kind, |
1111 cons (Formula (ident_base ^ "_res", kind, |
1098 eq [tag_with res_T (const bounds), const bounds], |
1112 eq [tag_with res_T (const bounds), const bounds], |
1099 simp_info, NONE)) |
1113 simp_info, NONE)) |
1162 Symtab.fold_rev |
1177 Symtab.fold_rev |
1163 (append o problem_lines_for_sym_decls ctxt format conj_sym_kind nonmono_Ts |
1178 (append o problem_lines_for_sym_decls ctxt format conj_sym_kind nonmono_Ts |
1164 type_sys) |
1179 type_sys) |
1165 sym_decl_tab [] |
1180 sym_decl_tab [] |
1166 |
1181 |
1167 fun add_tff_types_in_formula (AQuant (_, xs, phi)) = |
1182 fun add_simple_types_in_formula (AQuant (_, xs, phi)) = |
1168 union (op =) (map_filter snd xs) #> add_tff_types_in_formula phi |
1183 union (op =) (map_filter snd xs) #> add_simple_types_in_formula phi |
1169 | add_tff_types_in_formula (AConn (_, phis)) = |
1184 | add_simple_types_in_formula (AConn (_, phis)) = |
1170 fold add_tff_types_in_formula phis |
1185 fold add_simple_types_in_formula phis |
1171 | add_tff_types_in_formula (AAtom _) = I |
1186 | add_simple_types_in_formula (AAtom _) = I |
1172 |
1187 |
1173 fun add_tff_types_in_problem_line (Decl (_, _, arg_Ts, res_T)) = |
1188 fun add_simple_types_in_problem_line (Decl (_, _, arg_Ts, res_T)) = |
1174 union (op =) (res_T :: arg_Ts) |
1189 union (op =) (res_T :: arg_Ts) |
1175 | add_tff_types_in_problem_line (Formula (_, _, phi, _, _)) = |
1190 | add_simple_types_in_problem_line (Formula (_, _, phi, _, _)) = |
1176 add_tff_types_in_formula phi |
1191 add_simple_types_in_formula phi |
1177 |
1192 |
1178 fun tff_types_in_problem problem = |
1193 fun simple_types_in_problem problem = |
1179 fold (fold add_tff_types_in_problem_line o snd) problem [] |
1194 fold (fold add_simple_types_in_problem_line o snd) problem [] |
1180 |
1195 |> filter_out (String.isPrefix tptp_special_prefix o fst) |
1181 fun decl_line_for_tff_type (s, s') = |
1196 |
1182 Decl (type_decl_prefix ^ ascii_of s, (s, s'), [], `I tptp_tff_type_of_types) |
1197 fun decl_line_for_simple_type (s, s') = |
|
1198 Decl (type_decl_prefix ^ ascii_of s, (s, s'), [], `I tptp_type_of_types) |
1183 |
1199 |
1184 fun should_add_ti_ti_helper (Tags (Polymorphic, level, Heavy)) = |
1200 fun should_add_ti_ti_helper (Tags (Polymorphic, level, Heavy)) = |
1185 level = Nonmonotonic_Types orelse level = Finite_Types |
1201 level = Nonmonotonic_Types orelse level = Finite_Types |
1186 | should_add_ti_ti_helper _ = false |
1202 | should_add_ti_ti_helper _ = false |
1187 |
1203 |
1201 |
1217 |
1202 fun prepare_atp_problem ctxt format conj_sym_kind prem_kind type_sys |
1218 fun prepare_atp_problem ctxt format conj_sym_kind prem_kind type_sys |
1203 explicit_apply hyp_ts concl_t facts = |
1219 explicit_apply hyp_ts concl_t facts = |
1204 let |
1220 let |
1205 val (fact_names, (conjs, facts, class_rel_clauses, arity_clauses)) = |
1221 val (fact_names, (conjs, facts, class_rel_clauses, arity_clauses)) = |
1206 translate_formulas ctxt prem_kind type_sys hyp_ts concl_t facts |
1222 translate_formulas ctxt format prem_kind type_sys hyp_ts concl_t facts |
1207 val sym_tab = conjs @ facts |> sym_table_for_facts explicit_apply |
1223 val sym_tab = conjs @ facts |> sym_table_for_facts explicit_apply |
1208 val nonmono_Ts = conjs @ facts |> nonmonotonic_types_for_facts ctxt type_sys |
1224 val nonmono_Ts = conjs @ facts |> nonmonotonic_types_for_facts ctxt type_sys |
1209 val repair = repair_fact ctxt nonmono_Ts type_sys sym_tab |
1225 val repair = repair_fact ctxt format nonmono_Ts type_sys sym_tab |
1210 val (conjs, facts) = (conjs, facts) |> pairself (map repair) |
1226 val (conjs, facts) = (conjs, facts) |> pairself (map repair) |
1211 val repaired_sym_tab = conjs @ facts |> sym_table_for_facts false |
1227 val repaired_sym_tab = conjs @ facts |> sym_table_for_facts false |
1212 val helpers = |
1228 val helpers = |
1213 repaired_sym_tab |> helper_facts_for_sym_table ctxt type_sys |> map repair |
1229 repaired_sym_tab |> helper_facts_for_sym_table ctxt format type_sys |
|
1230 |> map repair |
1214 val lavish_nonmono_Ts = |
1231 val lavish_nonmono_Ts = |
1215 if null nonmono_Ts orelse |
1232 if null nonmono_Ts orelse |
1216 polymorphism_of_type_sys type_sys <> Polymorphic then |
1233 polymorphism_of_type_sys type_sys <> Polymorphic then |
1217 nonmono_Ts |
1234 nonmono_Ts |
1218 else |
1235 else |
1236 map (formula_line_for_fact ctxt format fact_prefix nonmono_Ts type_sys) |
1253 map (formula_line_for_fact ctxt format fact_prefix nonmono_Ts type_sys) |
1237 (0 upto length facts - 1 ~~ facts)), |
1254 (0 upto length facts - 1 ~~ facts)), |
1238 (class_relsN, map formula_line_for_class_rel_clause class_rel_clauses), |
1255 (class_relsN, map formula_line_for_class_rel_clause class_rel_clauses), |
1239 (aritiesN, map formula_line_for_arity_clause arity_clauses), |
1256 (aritiesN, map formula_line_for_arity_clause arity_clauses), |
1240 (helpersN, helper_lines), |
1257 (helpersN, helper_lines), |
1241 (conjsN, map (formula_line_for_conjecture ctxt nonmono_Ts type_sys) |
1258 (conjsN, |
1242 conjs), |
1259 map (formula_line_for_conjecture ctxt format nonmono_Ts type_sys) |
|
1260 conjs), |
1243 (free_typesN, |
1261 (free_typesN, |
1244 formula_lines_for_free_types format type_sys (facts @ conjs))] |
1262 formula_lines_for_free_types format type_sys (facts @ conjs))] |
1245 val problem = |
1263 val problem = |
1246 problem |
1264 problem |
1247 |> (case type_sys of |
1265 |> (case type_sys of |
1248 Simple_Types _ => |
1266 Simple_Types _ => |
1249 cons (type_declsN, |
1267 cons (type_declsN, problem |> simple_types_in_problem |
1250 map decl_line_for_tff_type (tff_types_in_problem problem)) |
1268 |> map decl_line_for_simple_type) |
1251 | _ => I) |
1269 | _ => I) |
1252 val problem = |
1270 val problem = |
1253 problem |> (if format = CNF_UEQ then filter_cnf_ueq_problem else I) |
1271 problem |> (if format = CNF_UEQ then filter_cnf_ueq_problem else I) |
1254 val (problem, pool) = |
1272 val (problem, pool) = |
1255 problem |> nice_atp_problem (Config.get ctxt readable_names) |
1273 problem |> nice_atp_problem (Config.get ctxt readable_names) |