9 signature ATP_TRANSLATE = |
9 signature ATP_TRANSLATE = |
10 sig |
10 sig |
11 type ('a, 'b) ho_term = ('a, 'b) ATP_Problem.ho_term |
11 type ('a, 'b) ho_term = ('a, 'b) ATP_Problem.ho_term |
12 type connective = ATP_Problem.connective |
12 type connective = ATP_Problem.connective |
13 type ('a, 'b, 'c) formula = ('a, 'b, 'c) ATP_Problem.formula |
13 type ('a, 'b, 'c) formula = ('a, 'b, 'c) ATP_Problem.formula |
14 type tptp_format = ATP_Problem.tptp_format |
14 type atp_format = ATP_Problem.atp_format |
15 type formula_kind = ATP_Problem.formula_kind |
15 type formula_kind = ATP_Problem.formula_kind |
16 type 'a problem = 'a ATP_Problem.problem |
16 type 'a problem = 'a ATP_Problem.problem |
17 |
17 |
18 datatype locality = |
18 datatype locality = |
19 General | Helper | Induction | Intro | Elim | Simp | Local | Assum | Chained |
19 General | Helper | Induction | Intro | Elim | Simp | Local | Assum | Chained |
84 val polymorphism_of_type_enc : type_enc -> polymorphism |
84 val polymorphism_of_type_enc : type_enc -> polymorphism |
85 val level_of_type_enc : type_enc -> type_level |
85 val level_of_type_enc : type_enc -> type_level |
86 val is_type_enc_quasi_sound : type_enc -> bool |
86 val is_type_enc_quasi_sound : type_enc -> bool |
87 val is_type_enc_fairly_sound : type_enc -> bool |
87 val is_type_enc_fairly_sound : type_enc -> bool |
88 val type_enc_from_string : soundness -> string -> type_enc |
88 val type_enc_from_string : soundness -> string -> type_enc |
89 val adjust_type_enc : tptp_format -> type_enc -> type_enc |
89 val adjust_type_enc : atp_format -> type_enc -> type_enc |
90 val mk_aconns : |
90 val mk_aconns : |
91 connective -> ('a, 'b, 'c) formula list -> ('a, 'b, 'c) formula |
91 connective -> ('a, 'b, 'c) formula list -> ('a, 'b, 'c) formula |
92 val unmangled_const : string -> string * (string, 'b) ho_term list |
92 val unmangled_const : string -> string * (string, 'b) ho_term list |
93 val unmangled_const_name : string -> string |
93 val unmangled_const_name : string -> string |
94 val helper_table : ((string * bool) * thm list) list |
94 val helper_table : ((string * bool) * thm list) list |
95 val factsN : string |
95 val factsN : string |
96 val prepare_atp_problem : |
96 val prepare_atp_problem : |
97 Proof.context -> tptp_format -> formula_kind -> formula_kind -> type_enc |
97 Proof.context -> atp_format -> formula_kind -> formula_kind -> type_enc |
98 -> bool -> string -> bool -> bool -> term list -> term |
98 -> bool -> string -> bool -> bool -> term list -> term |
99 -> ((string * locality) * term) list |
99 -> ((string * locality) * term) list |
100 -> string problem * string Symtab.table * int * int |
100 -> string problem * string Symtab.table * int * int |
101 * (string * locality) list vector * int list * int Symtab.table |
101 * (string * locality) list vector * int list * int Symtab.table |
102 val atp_problem_weights : string problem -> (string * real) list |
102 val atp_problem_weights : string problem -> (string * real) list |
121 val combinatorsN = "combinators" |
121 val combinatorsN = "combinators" |
122 val hybridN = "hybrid" |
122 val hybridN = "hybrid" |
123 val lambdasN = "lambdas" |
123 val lambdasN = "lambdas" |
124 val smartN = "smart" |
124 val smartN = "smart" |
125 |
125 |
126 val generate_info = false (* experimental *) |
|
127 |
|
128 fun isabelle_info s = |
|
129 if generate_info then SOME (ATerm ("[]", [ATerm ("isabelle_" ^ s, [])])) |
|
130 else NONE |
|
131 |
|
132 val introN = "intro" |
|
133 val elimN = "elim" |
|
134 val simpN = "simp" |
|
135 |
|
136 (* TFF1 is still in development, and it is still unclear whether symbols will be |
126 (* TFF1 is still in development, and it is still unclear whether symbols will be |
137 allowed to have types like "$tType > $o" (i.e., "![A : $tType] : $o"), with |
127 allowed to have types like "$tType > $o" (i.e., "![A : $tType] : $o"), with |
138 "dummy" type variables. *) |
128 ghost type variables. *) |
139 val avoid_first_order_dummy_type_vars = true |
129 val avoid_first_order_ghost_type_vars = true |
140 |
130 |
141 val bound_var_prefix = "B_" |
131 val bound_var_prefix = "B_" |
142 val all_bound_var_prefix = "BA_" |
132 val all_bound_var_prefix = "BA_" |
143 val exist_bound_var_prefix = "BE_" |
133 val exist_bound_var_prefix = "BE_" |
144 val schematic_var_prefix = "V_" |
134 val schematic_var_prefix = "V_" |
311 |
301 |
312 fun make_schematic_type_var (x, i) = |
302 fun make_schematic_type_var (x, i) = |
313 tvar_prefix ^ (ascii_of_indexname (unprefix "'" x, i)) |
303 tvar_prefix ^ (ascii_of_indexname (unprefix "'" x, i)) |
314 fun make_fixed_type_var x = tfree_prefix ^ (ascii_of (unprefix "'" x)) |
304 fun make_fixed_type_var x = tfree_prefix ^ (ascii_of (unprefix "'" x)) |
315 |
305 |
316 (* "HOL.eq" and Choice are mapped to the ATP's equivalents *) |
306 (* "HOL.eq" and choice are mapped to the ATP's equivalents *) |
317 local |
307 local |
318 val choice_const = (fst o dest_Const o HOLogic.choice_const) Term.dummyT |
308 val choice_const = (fst o dest_Const o HOLogic.choice_const) Term.dummyT |
319 fun default c = const_prefix ^ lookup_const c |
309 fun default c = const_prefix ^ lookup_const c |
320 in |
310 in |
321 fun make_fixed_const _ @{const_name HOL.eq} = tptp_old_equal |
311 fun make_fixed_const _ @{const_name HOL.eq} = tptp_old_equal |
648 (Simple_Types (order, _, level)) = |
638 (Simple_Types (order, _, level)) = |
649 Simple_Types (order, Mangled_Monomorphic, level) |
639 Simple_Types (order, Mangled_Monomorphic, level) |
650 | adjust_type_enc (THF _) type_enc = type_enc |
640 | adjust_type_enc (THF _) type_enc = type_enc |
651 | adjust_type_enc (TFF (TPTP_Monomorphic, _)) (Simple_Types (_, _, level)) = |
641 | adjust_type_enc (TFF (TPTP_Monomorphic, _)) (Simple_Types (_, _, level)) = |
652 Simple_Types (First_Order, Mangled_Monomorphic, level) |
642 Simple_Types (First_Order, Mangled_Monomorphic, level) |
|
643 | adjust_type_enc DFG_Sorted (Simple_Types (_, _, level)) = |
|
644 Simple_Types (First_Order, Mangled_Monomorphic, level) |
653 | adjust_type_enc (TFF _) (Simple_Types (_, poly, level)) = |
645 | adjust_type_enc (TFF _) (Simple_Types (_, poly, level)) = |
654 Simple_Types (First_Order, poly, level) |
646 Simple_Types (First_Order, poly, level) |
655 | adjust_type_enc format (Simple_Types (_, poly, level)) = |
647 | adjust_type_enc format (Simple_Types (_, poly, level)) = |
656 adjust_type_enc format (Guards (poly, level)) |
648 adjust_type_enc format (Guards (poly, level)) |
657 | adjust_type_enc CNF_UEQ (type_enc as Guards stuff) = |
649 | adjust_type_enc CNF_UEQ (type_enc as Guards stuff) = |
753 |
745 |
754 fun type_class_formula type_enc class arg = |
746 fun type_class_formula type_enc class arg = |
755 AAtom (ATerm (class, arg :: |
747 AAtom (ATerm (class, arg :: |
756 (case type_enc of |
748 (case type_enc of |
757 Simple_Types (First_Order, Polymorphic, _) => |
749 Simple_Types (First_Order, Polymorphic, _) => |
758 if avoid_first_order_dummy_type_vars then [ATerm (TYPE_name, [arg])] |
750 if avoid_first_order_ghost_type_vars then [ATerm (TYPE_name, [arg])] |
759 else [] |
751 else [] |
760 | _ => []))) |
752 | _ => []))) |
761 fun formulas_for_types type_enc add_sorts_on_typ Ts = |
753 fun formulas_for_types type_enc add_sorts_on_typ Ts = |
762 [] |> level_of_type_enc type_enc <> No_Types ? fold add_sorts_on_typ Ts |
754 [] |> level_of_type_enc type_enc <> No_Types ? fold add_sorts_on_typ Ts |
763 |> map (fn (class, name) => |
755 |> map (fn (class, name) => |
1543 |> bound_tvars type_enc atomic_Ts |
1535 |> bound_tvars type_enc atomic_Ts |
1544 |> close_formula_universally type_enc |
1536 |> close_formula_universally type_enc |
1545 |
1537 |
1546 val type_tag = `(make_fixed_const NONE) type_tag_name |
1538 val type_tag = `(make_fixed_const NONE) type_tag_name |
1547 |
1539 |
1548 fun type_tag_idempotence_fact type_enc = |
1540 fun type_tag_idempotence_fact format type_enc = |
1549 let |
1541 let |
1550 fun var s = ATerm (`I s, []) |
1542 fun var s = ATerm (`I s, []) |
1551 fun tag tm = ATerm (type_tag, [var "A", tm]) |
1543 fun tag tm = ATerm (type_tag, [var "A", tm]) |
1552 val tagged_var = tag (var "X") |
1544 val tagged_var = tag (var "X") |
1553 in |
1545 in |
1554 Formula (type_tag_idempotence_helper_name, Axiom, |
1546 Formula (type_tag_idempotence_helper_name, Axiom, |
1555 eq_formula type_enc [] false (tag tagged_var) tagged_var, |
1547 eq_formula type_enc [] false (tag tagged_var) tagged_var, |
1556 isabelle_info simpN, NONE) |
1548 isabelle_info format simpN, NONE) |
1557 end |
1549 end |
1558 |
1550 |
1559 fun should_specialize_helper type_enc t = |
1551 fun should_specialize_helper type_enc t = |
1560 polymorphism_of_type_enc type_enc <> Polymorphic andalso |
1552 polymorphism_of_type_enc type_enc <> Polymorphic andalso |
1561 level_of_type_enc type_enc <> No_Types andalso |
1553 level_of_type_enc type_enc <> No_Types andalso |
1831 (if pos then SOME true else NONE) |
1823 (if pos then SOME true else NONE) |
1832 |> bound_tvars type_enc atomic_types |
1824 |> bound_tvars type_enc atomic_types |
1833 |> close_formula_universally type_enc, |
1825 |> close_formula_universally type_enc, |
1834 NONE, |
1826 NONE, |
1835 case locality of |
1827 case locality of |
1836 Intro => isabelle_info introN |
1828 Intro => isabelle_info format introN |
1837 | Elim => isabelle_info elimN |
1829 | Elim => isabelle_info format elimN |
1838 | Simp => isabelle_info simpN |
1830 | Simp => isabelle_info format simpN |
1839 | _ => NONE) |
1831 | _ => NONE) |
1840 |> Formula |
1832 |> Formula |
1841 |
1833 |
1842 fun formula_line_for_class_rel_clause type_enc |
1834 fun formula_line_for_class_rel_clause format type_enc |
1843 ({name, subclass, superclass, ...} : class_rel_clause) = |
1835 ({name, subclass, superclass, ...} : class_rel_clause) = |
1844 let val ty_arg = ATerm (tvar_a_name, []) in |
1836 let val ty_arg = ATerm (tvar_a_name, []) in |
1845 Formula (class_rel_clause_prefix ^ ascii_of name, Axiom, |
1837 Formula (class_rel_clause_prefix ^ ascii_of name, Axiom, |
1846 AConn (AImplies, |
1838 AConn (AImplies, |
1847 [type_class_formula type_enc subclass ty_arg, |
1839 [type_class_formula type_enc subclass ty_arg, |
1848 type_class_formula type_enc superclass ty_arg]) |
1840 type_class_formula type_enc superclass ty_arg]) |
1849 |> close_formula_universally type_enc, isabelle_info introN, NONE) |
1841 |> close_formula_universally type_enc, |
|
1842 isabelle_info format introN, NONE) |
1850 end |
1843 end |
1851 |
1844 |
1852 fun formula_from_arity_atom type_enc (class, t, args) = |
1845 fun formula_from_arity_atom type_enc (class, t, args) = |
1853 ATerm (t, map (fn arg => ATerm (arg, [])) args) |
1846 ATerm (t, map (fn arg => ATerm (arg, [])) args) |
1854 |> type_class_formula type_enc class |
1847 |> type_class_formula type_enc class |
1855 |
1848 |
1856 fun formula_line_for_arity_clause type_enc |
1849 fun formula_line_for_arity_clause format type_enc |
1857 ({name, prem_atoms, concl_atom, ...} : arity_clause) = |
1850 ({name, prem_atoms, concl_atom, ...} : arity_clause) = |
1858 Formula (arity_clause_prefix ^ name, Axiom, |
1851 Formula (arity_clause_prefix ^ name, Axiom, |
1859 mk_ahorn (map (formula_from_arity_atom type_enc) prem_atoms) |
1852 mk_ahorn (map (formula_from_arity_atom type_enc) prem_atoms) |
1860 (formula_from_arity_atom type_enc concl_atom) |
1853 (formula_from_arity_atom type_enc concl_atom) |
1861 |> close_formula_universally type_enc, isabelle_info introN, NONE) |
1854 |> close_formula_universally type_enc, |
|
1855 isabelle_info format introN, NONE) |
1862 |
1856 |
1863 fun formula_line_for_conjecture ctxt format mono type_enc |
1857 fun formula_line_for_conjecture ctxt format mono type_enc |
1864 ({name, kind, iformula, atomic_types, ...} : translated_formula) = |
1858 ({name, kind, iformula, atomic_types, ...} : translated_formula) = |
1865 Formula (conjecture_prefix ^ name, kind, |
1859 Formula (conjecture_prefix ^ name, kind, |
1866 formula_from_iformula ctxt format mono type_enc |
1860 formula_from_iformula ctxt format mono type_enc |
1881 (** Symbol declarations **) |
1875 (** Symbol declarations **) |
1882 |
1876 |
1883 fun decl_line_for_class order s = |
1877 fun decl_line_for_class order s = |
1884 let val name as (s, _) = `make_type_class s in |
1878 let val name as (s, _) = `make_type_class s in |
1885 Decl (sym_decl_prefix ^ s, name, |
1879 Decl (sym_decl_prefix ^ s, name, |
1886 if order = First_Order andalso avoid_first_order_dummy_type_vars then |
1880 if order = First_Order andalso avoid_first_order_ghost_type_vars then |
1887 ATyAbs ([tvar_a_name], AFun (a_itself_atype, bool_atype)) |
1881 ATyAbs ([tvar_a_name], AFun (a_itself_atype, bool_atype)) |
1888 else |
1882 else |
1889 AFun (atype_of_types, bool_atype)) |
1883 AFun (atype_of_types, bool_atype)) |
1890 end |
1884 end |
1891 |
1885 |
2057 |> AAtom |
2051 |> AAtom |
2058 |> formula_from_iformula ctxt format mono type_enc |
2052 |> formula_from_iformula ctxt format mono type_enc |
2059 (K (K (K (K (K (K true)))))) (SOME true) |
2053 (K (K (K (K (K (K true)))))) (SOME true) |
2060 |> bound_tvars type_enc (atyps_of T) |
2054 |> bound_tvars type_enc (atyps_of T) |
2061 |> close_formula_universally type_enc, |
2055 |> close_formula_universally type_enc, |
2062 isabelle_info introN, NONE) |
2056 isabelle_info format introN, NONE) |
2063 |
2057 |
2064 fun formula_line_for_tags_mono_type ctxt format mono type_enc T = |
2058 fun formula_line_for_tags_mono_type ctxt format mono type_enc T = |
2065 let val x_var = ATerm (`make_bound_var "X", []) in |
2059 let val x_var = ATerm (`make_bound_var "X", []) in |
2066 Formula (tags_sym_formula_prefix ^ |
2060 Formula (tags_sym_formula_prefix ^ |
2067 ascii_of (mangled_type format type_enc T), |
2061 ascii_of (mangled_type format type_enc T), |
2068 Axiom, |
2062 Axiom, |
2069 eq_formula type_enc (atyps_of T) false |
2063 eq_formula type_enc (atyps_of T) false |
2070 (tag_with_type ctxt format mono type_enc NONE T x_var) |
2064 (tag_with_type ctxt format mono type_enc NONE T x_var) |
2071 x_var, |
2065 x_var, |
2072 isabelle_info simpN, NONE) |
2066 isabelle_info format simpN, NONE) |
2073 end |
2067 end |
2074 |
2068 |
2075 fun problem_lines_for_mono_types ctxt format mono type_enc Ts = |
2069 fun problem_lines_for_mono_types ctxt format mono type_enc Ts = |
2076 case type_enc of |
2070 case type_enc of |
2077 Simple_Types _ => [] |
2071 Simple_Types _ => [] |
2141 |> formula_from_iformula ctxt format mono type_enc |
2135 |> formula_from_iformula ctxt format mono type_enc |
2142 (K (K (K (K (K (K true)))))) (SOME true) |
2136 (K (K (K (K (K (K true)))))) (SOME true) |
2143 |> n > 1 ? bound_tvars type_enc (atyps_of T) |
2137 |> n > 1 ? bound_tvars type_enc (atyps_of T) |
2144 |> close_formula_universally type_enc |
2138 |> close_formula_universally type_enc |
2145 |> maybe_negate, |
2139 |> maybe_negate, |
2146 isabelle_info introN, NONE) |
2140 isabelle_info format introN, NONE) |
2147 end |
2141 end |
2148 |
2142 |
2149 fun formula_lines_for_tags_sym_decl ctxt format conj_sym_kind mono type_enc n s |
2143 fun formula_lines_for_tags_sym_decl ctxt format conj_sym_kind mono type_enc n s |
2150 (j, (s', T_args, T, pred_sym, ary, in_conj)) = |
2144 (j, (s', T_args, T, pred_sym, ary, in_conj)) = |
2151 let |
2145 let |
2353 (factsN, |
2347 (factsN, |
2354 map (formula_line_for_fact ctxt format fact_prefix ascii_of |
2348 map (formula_line_for_fact ctxt format fact_prefix ascii_of |
2355 (not exporter) (not exporter) mono type_enc) |
2349 (not exporter) (not exporter) mono type_enc) |
2356 (0 upto length facts - 1 ~~ facts)), |
2350 (0 upto length facts - 1 ~~ facts)), |
2357 (class_relsN, |
2351 (class_relsN, |
2358 map (formula_line_for_class_rel_clause type_enc) class_rel_clauses), |
2352 map (formula_line_for_class_rel_clause format type_enc) |
2359 (aritiesN, map (formula_line_for_arity_clause type_enc) arity_clauses), |
2353 class_rel_clauses), |
|
2354 (aritiesN, |
|
2355 map (formula_line_for_arity_clause format type_enc) arity_clauses), |
2360 (helpersN, helper_lines), |
2356 (helpersN, helper_lines), |
2361 (conjsN, |
2357 (conjsN, |
2362 map (formula_line_for_conjecture ctxt format mono type_enc) conjs), |
2358 map (formula_line_for_conjecture ctxt format mono type_enc) conjs), |
2363 (free_typesN, formula_lines_for_free_types type_enc (facts @ conjs))] |
2359 (free_typesN, formula_lines_for_free_types type_enc (facts @ conjs))] |
2364 val problem = |
2360 val problem = |