author | blanchet |
Tue, 22 Jun 2010 14:28:22 +0200 | |
changeset 37498 | b426cbdb5a23 |
parent 37496 | 9ae78e12e126 |
child 37500 | 7587b6e63454 |
permissions | -rw-r--r-- |
36375
2482446a604c
move the minimizer to the Sledgehammer directory
blanchet
parents:
36237
diff
changeset
|
1 |
(* Title: HOL/Tools/Sledgehammer/sledgehammer_hol_clause.ML |
33311 | 2 |
Author: Jia Meng, NICTA |
36375
2482446a604c
move the minimizer to the Sledgehammer directory
blanchet
parents:
36237
diff
changeset
|
3 |
Author: Jasmin Blanchette, TU Muenchen |
17998
0a869029ca58
A new file that defines datatypes representing FOL clauses that are derived from HOL formulae. This file also has functions that convert lambda terms to combinator expressions, and functions that convert clauses to TPTP format.
mengj
parents:
diff
changeset
|
4 |
|
24311 | 5 |
FOL clauses translated from HOL formulae. |
17998
0a869029ca58
A new file that defines datatypes representing FOL clauses that are derived from HOL formulae. This file also has functions that convert lambda terms to combinator expressions, and functions that convert clauses to TPTP format.
mengj
parents:
diff
changeset
|
6 |
*) |
0a869029ca58
A new file that defines datatypes representing FOL clauses that are derived from HOL formulae. This file also has functions that convert lambda terms to combinator expressions, and functions that convert clauses to TPTP format.
mengj
parents:
diff
changeset
|
7 |
|
35826 | 8 |
signature SLEDGEHAMMER_HOL_CLAUSE = |
24311 | 9 |
sig |
36170
0cdb76723c88
added original constant names to Sledgehammer internal terms + output short names if "debug" is set (for increased readability)
blanchet
parents:
36169
diff
changeset
|
10 |
type name = Sledgehammer_FOL_Clause.name |
36393
be73a2b2443b
support readable names even when Isar proof reconstruction is enabled -- useful for debugging
blanchet
parents:
36375
diff
changeset
|
11 |
type name_pool = Sledgehammer_FOL_Clause.name_pool |
35865 | 12 |
type kind = Sledgehammer_FOL_Clause.kind |
13 |
type fol_type = Sledgehammer_FOL_Clause.fol_type |
|
14 |
type classrel_clause = Sledgehammer_FOL_Clause.classrel_clause |
|
15 |
type arity_clause = Sledgehammer_FOL_Clause.arity_clause |
|
24311 | 16 |
type axiom_name = string |
17 |
type polarity = bool |
|
35865 | 18 |
type hol_clause_id = int |
19 |
||
24311 | 20 |
datatype combterm = |
36170
0cdb76723c88
added original constant names to Sledgehammer internal terms + output short names if "debug" is set (for increased readability)
blanchet
parents:
36169
diff
changeset
|
21 |
CombConst of name * fol_type * fol_type list (* Const and Free *) | |
0cdb76723c88
added original constant names to Sledgehammer internal terms + output short names if "debug" is set (for increased readability)
blanchet
parents:
36169
diff
changeset
|
22 |
CombVar of name * fol_type | |
35865 | 23 |
CombApp of combterm * combterm |
24311 | 24 |
datatype literal = Literal of polarity * combterm |
35865 | 25 |
datatype hol_clause = |
26 |
HOLClause of {clause_id: hol_clause_id, axiom_name: axiom_name, th: thm, |
|
27 |
kind: kind, literals: literal list, ctypes_sorts: typ list} |
|
28 |
||
29 |
val type_of_combterm : combterm -> fol_type |
|
30 |
val strip_combterm_comb : combterm -> combterm * combterm list |
|
31 |
val literals_of_term : theory -> term -> literal list * typ list |
|
37410
2bf7e6136047
adjusted the polymorphism handling of Skolem constants so that proof reconstruction doesn't fail in "equality_inf"
blanchet
parents:
37399
diff
changeset
|
32 |
val conceal_skolem_somes : |
2bf7e6136047
adjusted the polymorphism handling of Skolem constants so that proof reconstruction doesn't fail in "equality_inf"
blanchet
parents:
37399
diff
changeset
|
33 |
int -> (string * term) list -> term -> (string * term) list * term |
35865 | 34 |
exception TRIVIAL |
37498
b426cbdb5a23
removed Sledgehammer's support for the DFG syntax;
blanchet
parents:
37496
diff
changeset
|
35 |
val make_conjecture_clauses : theory -> thm list -> hol_clause list |
b426cbdb5a23
removed Sledgehammer's support for the DFG syntax;
blanchet
parents:
37496
diff
changeset
|
36 |
val make_axiom_clauses : |
b426cbdb5a23
removed Sledgehammer's support for the DFG syntax;
blanchet
parents:
37496
diff
changeset
|
37 |
theory -> (thm * (axiom_name * hol_clause_id)) list |
b426cbdb5a23
removed Sledgehammer's support for the DFG syntax;
blanchet
parents:
37496
diff
changeset
|
38 |
-> (axiom_name * hol_clause) list |
36909
7d5587f6d5f7
made Sledgehammer's full-typed proof reconstruction work for the first time;
blanchet
parents:
36565
diff
changeset
|
39 |
val type_wrapper_name : string |
37399
34f080a12063
proper polymorphic Skolemization of uncached facts + synchronization of caching and relevance filter
blanchet
parents:
36966
diff
changeset
|
40 |
val get_helper_clauses : |
37498
b426cbdb5a23
removed Sledgehammer's support for the DFG syntax;
blanchet
parents:
37496
diff
changeset
|
41 |
theory -> bool -> bool -> hol_clause list |
b426cbdb5a23
removed Sledgehammer's support for the DFG syntax;
blanchet
parents:
37496
diff
changeset
|
42 |
-> (thm * (axiom_name * hol_clause_id)) list -> hol_clause list |
36235
61159615a0c5
added "explicit_apply" option to Sledgehammer, to control whether an explicit apply function should be used as much or as little as possible (replaces a previous global variable)
blanchet
parents:
36233
diff
changeset
|
43 |
val write_tptp_file : bool -> bool -> bool -> Path.T -> |
35865 | 44 |
hol_clause list * hol_clause list * hol_clause list * hol_clause list * |
36402
1b20805974c7
introduced direct proof reconstruction code, eliminating the need for the "neg_clausify" method;
blanchet
parents:
36393
diff
changeset
|
45 |
classrel_clause list * arity_clause list -> name_pool option * int |
24311 | 46 |
end |
17998
0a869029ca58
A new file that defines datatypes representing FOL clauses that are derived from HOL formulae. This file also has functions that convert lambda terms to combinator expressions, and functions that convert clauses to TPTP format.
mengj
parents:
diff
changeset
|
47 |
|
35826 | 48 |
structure Sledgehammer_HOL_Clause : SLEDGEHAMMER_HOL_CLAUSE = |
17998
0a869029ca58
A new file that defines datatypes representing FOL clauses that are derived from HOL formulae. This file also has functions that convert lambda terms to combinator expressions, and functions that convert clauses to TPTP format.
mengj
parents:
diff
changeset
|
49 |
struct |
0a869029ca58
A new file that defines datatypes representing FOL clauses that are derived from HOL formulae. This file also has functions that convert lambda terms to combinator expressions, and functions that convert clauses to TPTP format.
mengj
parents:
diff
changeset
|
50 |
|
36167
c1a35be8e476
make Sledgehammer's output more debugging friendly
blanchet
parents:
35963
diff
changeset
|
51 |
open Sledgehammer_Util |
35865 | 52 |
open Sledgehammer_FOL_Clause |
53 |
open Sledgehammer_Fact_Preprocessor |
|
22825
bd774e01d6d5
Fixing bugs in the partial-typed and fully-typed translations
paulson
parents:
22130
diff
changeset
|
54 |
|
37479
f6b1ee5b420b
try to improve Sledgehammer/Metis's behavior in full_types mode, e.g. by handing True, False, and If better
blanchet
parents:
37436
diff
changeset
|
55 |
fun min_arity_of const_min_arity c = |
f6b1ee5b420b
try to improve Sledgehammer/Metis's behavior in full_types mode, e.g. by handing True, False, and If better
blanchet
parents:
37436
diff
changeset
|
56 |
the_default 0 (Symtab.lookup const_min_arity c) |
22064 | 57 |
|
22825
bd774e01d6d5
Fixing bugs in the partial-typed and fully-typed translations
paulson
parents:
22130
diff
changeset
|
58 |
(*True if the constant ever appears outside of the top-level position in literals. |
bd774e01d6d5
Fixing bugs in the partial-typed and fully-typed translations
paulson
parents:
22130
diff
changeset
|
59 |
If false, the constant always receives all of its arguments and is used as a predicate.*) |
36235
61159615a0c5
added "explicit_apply" option to Sledgehammer, to control whether an explicit apply function should be used as much or as little as possible (replaces a previous global variable)
blanchet
parents:
36233
diff
changeset
|
60 |
fun needs_hBOOL explicit_apply const_needs_hBOOL c = |
37479
f6b1ee5b420b
try to improve Sledgehammer/Metis's behavior in full_types mode, e.g. by handing True, False, and If better
blanchet
parents:
37436
diff
changeset
|
61 |
explicit_apply orelse the_default false (Symtab.lookup const_needs_hBOOL c) |
22064 | 62 |
|
19198
e6f1ff40ba99
Added tptp_write_file to write all necessary ATP input clauses to one file.
mengj
parents:
19130
diff
changeset
|
63 |
|
17998
0a869029ca58
A new file that defines datatypes representing FOL clauses that are derived from HOL formulae. This file also has functions that convert lambda terms to combinator expressions, and functions that convert clauses to TPTP format.
mengj
parents:
diff
changeset
|
64 |
(******************************************************) |
0a869029ca58
A new file that defines datatypes representing FOL clauses that are derived from HOL formulae. This file also has functions that convert lambda terms to combinator expressions, and functions that convert clauses to TPTP format.
mengj
parents:
diff
changeset
|
65 |
(* data types for typed combinator expressions *) |
0a869029ca58
A new file that defines datatypes representing FOL clauses that are derived from HOL formulae. This file also has functions that convert lambda terms to combinator expressions, and functions that convert clauses to TPTP format.
mengj
parents:
diff
changeset
|
66 |
(******************************************************) |
0a869029ca58
A new file that defines datatypes representing FOL clauses that are derived from HOL formulae. This file also has functions that convert lambda terms to combinator expressions, and functions that convert clauses to TPTP format.
mengj
parents:
diff
changeset
|
67 |
|
0a869029ca58
A new file that defines datatypes representing FOL clauses that are derived from HOL formulae. This file also has functions that convert lambda terms to combinator expressions, and functions that convert clauses to TPTP format.
mengj
parents:
diff
changeset
|
68 |
type axiom_name = string; |
0a869029ca58
A new file that defines datatypes representing FOL clauses that are derived from HOL formulae. This file also has functions that convert lambda terms to combinator expressions, and functions that convert clauses to TPTP format.
mengj
parents:
diff
changeset
|
69 |
type polarity = bool; |
35865 | 70 |
type hol_clause_id = int; |
17998
0a869029ca58
A new file that defines datatypes representing FOL clauses that are derived from HOL formulae. This file also has functions that convert lambda terms to combinator expressions, and functions that convert clauses to TPTP format.
mengj
parents:
diff
changeset
|
71 |
|
35865 | 72 |
datatype combterm = |
36170
0cdb76723c88
added original constant names to Sledgehammer internal terms + output short names if "debug" is set (for increased readability)
blanchet
parents:
36169
diff
changeset
|
73 |
CombConst of name * fol_type * fol_type list (* Const and Free *) | |
0cdb76723c88
added original constant names to Sledgehammer internal terms + output short names if "debug" is set (for increased readability)
blanchet
parents:
36169
diff
changeset
|
74 |
CombVar of name * fol_type | |
35865 | 75 |
CombApp of combterm * combterm |
24311 | 76 |
|
17998
0a869029ca58
A new file that defines datatypes representing FOL clauses that are derived from HOL formulae. This file also has functions that convert lambda terms to combinator expressions, and functions that convert clauses to TPTP format.
mengj
parents:
diff
changeset
|
77 |
datatype literal = Literal of polarity * combterm; |
0a869029ca58
A new file that defines datatypes representing FOL clauses that are derived from HOL formulae. This file also has functions that convert lambda terms to combinator expressions, and functions that convert clauses to TPTP format.
mengj
parents:
diff
changeset
|
78 |
|
35865 | 79 |
datatype hol_clause = |
80 |
HOLClause of {clause_id: hol_clause_id, axiom_name: axiom_name, th: thm, |
|
81 |
kind: kind, literals: literal list, ctypes_sorts: typ list}; |
|
17998
0a869029ca58
A new file that defines datatypes representing FOL clauses that are derived from HOL formulae. This file also has functions that convert lambda terms to combinator expressions, and functions that convert clauses to TPTP format.
mengj
parents:
diff
changeset
|
82 |
|
0a869029ca58
A new file that defines datatypes representing FOL clauses that are derived from HOL formulae. This file also has functions that convert lambda terms to combinator expressions, and functions that convert clauses to TPTP format.
mengj
parents:
diff
changeset
|
83 |
|
0a869029ca58
A new file that defines datatypes representing FOL clauses that are derived from HOL formulae. This file also has functions that convert lambda terms to combinator expressions, and functions that convert clauses to TPTP format.
mengj
parents:
diff
changeset
|
84 |
(*********************************************************************) |
0a869029ca58
A new file that defines datatypes representing FOL clauses that are derived from HOL formulae. This file also has functions that convert lambda terms to combinator expressions, and functions that convert clauses to TPTP format.
mengj
parents:
diff
changeset
|
85 |
(* convert a clause with type Term.term to a clause with type clause *) |
0a869029ca58
A new file that defines datatypes representing FOL clauses that are derived from HOL formulae. This file also has functions that convert lambda terms to combinator expressions, and functions that convert clauses to TPTP format.
mengj
parents:
diff
changeset
|
86 |
(*********************************************************************) |
0a869029ca58
A new file that defines datatypes representing FOL clauses that are derived from HOL formulae. This file also has functions that convert lambda terms to combinator expressions, and functions that convert clauses to TPTP format.
mengj
parents:
diff
changeset
|
87 |
|
36170
0cdb76723c88
added original constant names to Sledgehammer internal terms + output short names if "debug" is set (for increased readability)
blanchet
parents:
36169
diff
changeset
|
88 |
fun isFalse (Literal (pol, CombConst ((c, _), _, _))) = |
35865 | 89 |
(pol andalso c = "c_False") orelse (not pol andalso c = "c_True") |
17998
0a869029ca58
A new file that defines datatypes representing FOL clauses that are derived from HOL formulae. This file also has functions that convert lambda terms to combinator expressions, and functions that convert clauses to TPTP format.
mengj
parents:
diff
changeset
|
90 |
| isFalse _ = false; |
0a869029ca58
A new file that defines datatypes representing FOL clauses that are derived from HOL formulae. This file also has functions that convert lambda terms to combinator expressions, and functions that convert clauses to TPTP format.
mengj
parents:
diff
changeset
|
91 |
|
36170
0cdb76723c88
added original constant names to Sledgehammer internal terms + output short names if "debug" is set (for increased readability)
blanchet
parents:
36169
diff
changeset
|
92 |
fun isTrue (Literal (pol, CombConst ((c, _), _, _))) = |
17998
0a869029ca58
A new file that defines datatypes representing FOL clauses that are derived from HOL formulae. This file also has functions that convert lambda terms to combinator expressions, and functions that convert clauses to TPTP format.
mengj
parents:
diff
changeset
|
93 |
(pol andalso c = "c_True") orelse |
0a869029ca58
A new file that defines datatypes representing FOL clauses that are derived from HOL formulae. This file also has functions that convert lambda terms to combinator expressions, and functions that convert clauses to TPTP format.
mengj
parents:
diff
changeset
|
94 |
(not pol andalso c = "c_False") |
0a869029ca58
A new file that defines datatypes representing FOL clauses that are derived from HOL formulae. This file also has functions that convert lambda terms to combinator expressions, and functions that convert clauses to TPTP format.
mengj
parents:
diff
changeset
|
95 |
| isTrue _ = false; |
24311 | 96 |
|
35865 | 97 |
fun isTaut (HOLClause {literals,...}) = exists isTrue literals; |
17998
0a869029ca58
A new file that defines datatypes representing FOL clauses that are derived from HOL formulae. This file also has functions that convert lambda terms to combinator expressions, and functions that convert clauses to TPTP format.
mengj
parents:
diff
changeset
|
98 |
|
37498
b426cbdb5a23
removed Sledgehammer's support for the DFG syntax;
blanchet
parents:
37496
diff
changeset
|
99 |
fun type_of (Type (a, Ts)) = |
b426cbdb5a23
removed Sledgehammer's support for the DFG syntax;
blanchet
parents:
37496
diff
changeset
|
100 |
let val (folTypes,ts) = types_of Ts in |
b426cbdb5a23
removed Sledgehammer's support for the DFG syntax;
blanchet
parents:
37496
diff
changeset
|
101 |
(TyConstr (`make_fixed_type_const a, folTypes), ts) |
36169
27b1cc58715e
store nonmangled names along with mangled type names in Sledgehammer for debugging purposes
blanchet
parents:
36168
diff
changeset
|
102 |
end |
37498
b426cbdb5a23
removed Sledgehammer's support for the DFG syntax;
blanchet
parents:
37496
diff
changeset
|
103 |
| type_of (tp as TFree (a, _)) = (TyFree (`make_fixed_type_var a), [tp]) |
b426cbdb5a23
removed Sledgehammer's support for the DFG syntax;
blanchet
parents:
37496
diff
changeset
|
104 |
| type_of (tp as TVar (x, _)) = |
36169
27b1cc58715e
store nonmangled names along with mangled type names in Sledgehammer for debugging purposes
blanchet
parents:
36168
diff
changeset
|
105 |
(TyVar (make_schematic_type_var x, string_of_indexname x), [tp]) |
37498
b426cbdb5a23
removed Sledgehammer's support for the DFG syntax;
blanchet
parents:
37496
diff
changeset
|
106 |
and types_of Ts = |
b426cbdb5a23
removed Sledgehammer's support for the DFG syntax;
blanchet
parents:
37496
diff
changeset
|
107 |
let val (folTyps, ts) = ListPair.unzip (map type_of Ts) in |
b426cbdb5a23
removed Sledgehammer's support for the DFG syntax;
blanchet
parents:
37496
diff
changeset
|
108 |
(folTyps, union_all ts) |
b426cbdb5a23
removed Sledgehammer's support for the DFG syntax;
blanchet
parents:
37496
diff
changeset
|
109 |
end |
17998
0a869029ca58
A new file that defines datatypes representing FOL clauses that are derived from HOL formulae. This file also has functions that convert lambda terms to combinator expressions, and functions that convert clauses to TPTP format.
mengj
parents:
diff
changeset
|
110 |
|
0a869029ca58
A new file that defines datatypes representing FOL clauses that are derived from HOL formulae. This file also has functions that convert lambda terms to combinator expressions, and functions that convert clauses to TPTP format.
mengj
parents:
diff
changeset
|
111 |
(* same as above, but no gathering of sort information *) |
37498
b426cbdb5a23
removed Sledgehammer's support for the DFG syntax;
blanchet
parents:
37496
diff
changeset
|
112 |
fun simp_type_of (Type (a, Ts)) = |
b426cbdb5a23
removed Sledgehammer's support for the DFG syntax;
blanchet
parents:
37496
diff
changeset
|
113 |
TyConstr (`make_fixed_type_const a, map simp_type_of Ts) |
b426cbdb5a23
removed Sledgehammer's support for the DFG syntax;
blanchet
parents:
37496
diff
changeset
|
114 |
| simp_type_of (TFree (a, _)) = TyFree (`make_fixed_type_var a) |
b426cbdb5a23
removed Sledgehammer's support for the DFG syntax;
blanchet
parents:
37496
diff
changeset
|
115 |
| simp_type_of (TVar (x, _)) = |
b426cbdb5a23
removed Sledgehammer's support for the DFG syntax;
blanchet
parents:
37496
diff
changeset
|
116 |
TyVar (make_schematic_type_var x, string_of_indexname x) |
18440
72ee07f4b56b
Literals in clauses are sorted now. Added functions for clause equivalence tests and hashing clauses to words.
mengj
parents:
18356
diff
changeset
|
117 |
|
18356
443717b3a9ad
Added new type embedding methods for translating HOL clauses.
mengj
parents:
18276
diff
changeset
|
118 |
|
17998
0a869029ca58
A new file that defines datatypes representing FOL clauses that are derived from HOL formulae. This file also has functions that convert lambda terms to combinator expressions, and functions that convert clauses to TPTP format.
mengj
parents:
diff
changeset
|
119 |
(* convert a Term.term (with combinators) into a combterm, also accummulate sort info *) |
37498
b426cbdb5a23
removed Sledgehammer's support for the DFG syntax;
blanchet
parents:
37496
diff
changeset
|
120 |
fun combterm_of thy (Const (c, T)) = |
37399
34f080a12063
proper polymorphic Skolemization of uncached facts + synchronization of caching and relevance filter
blanchet
parents:
36966
diff
changeset
|
121 |
let |
37498
b426cbdb5a23
removed Sledgehammer's support for the DFG syntax;
blanchet
parents:
37496
diff
changeset
|
122 |
val (tp, ts) = type_of T |
37399
34f080a12063
proper polymorphic Skolemization of uncached facts + synchronization of caching and relevance filter
blanchet
parents:
36966
diff
changeset
|
123 |
val tvar_list = |
37410
2bf7e6136047
adjusted the polymorphism handling of Skolem constants so that proof reconstruction doesn't fail in "equality_inf"
blanchet
parents:
37399
diff
changeset
|
124 |
(if String.isPrefix skolem_theory_name c then |
37399
34f080a12063
proper polymorphic Skolemization of uncached facts + synchronization of caching and relevance filter
blanchet
parents:
36966
diff
changeset
|
125 |
[] |> Term.add_tvarsT T |> map TVar |
34f080a12063
proper polymorphic Skolemization of uncached facts + synchronization of caching and relevance filter
blanchet
parents:
36966
diff
changeset
|
126 |
else |
34f080a12063
proper polymorphic Skolemization of uncached facts + synchronization of caching and relevance filter
blanchet
parents:
36966
diff
changeset
|
127 |
(c, T) |> Sign.const_typargs thy) |
37498
b426cbdb5a23
removed Sledgehammer's support for the DFG syntax;
blanchet
parents:
37496
diff
changeset
|
128 |
|> map simp_type_of |
b426cbdb5a23
removed Sledgehammer's support for the DFG syntax;
blanchet
parents:
37496
diff
changeset
|
129 |
val c' = CombConst (`make_fixed_const c, tp, tvar_list) |
22078
5084f53cef39
Streamlining: removing the type argument of CombApp; abbreviating ResClause as RC
paulson
parents:
22064
diff
changeset
|
130 |
in (c',ts) end |
37498
b426cbdb5a23
removed Sledgehammer's support for the DFG syntax;
blanchet
parents:
37496
diff
changeset
|
131 |
| combterm_of _ (Free(v, T)) = |
b426cbdb5a23
removed Sledgehammer's support for the DFG syntax;
blanchet
parents:
37496
diff
changeset
|
132 |
let val (tp,ts) = type_of T |
36170
0cdb76723c88
added original constant names to Sledgehammer internal terms + output short names if "debug" is set (for increased readability)
blanchet
parents:
36169
diff
changeset
|
133 |
val v' = CombConst (`make_fixed_var v, tp, []) |
22078
5084f53cef39
Streamlining: removing the type argument of CombApp; abbreviating ResClause as RC
paulson
parents:
22064
diff
changeset
|
134 |
in (v',ts) end |
37498
b426cbdb5a23
removed Sledgehammer's support for the DFG syntax;
blanchet
parents:
37496
diff
changeset
|
135 |
| combterm_of _ (Var(v, T)) = |
b426cbdb5a23
removed Sledgehammer's support for the DFG syntax;
blanchet
parents:
37496
diff
changeset
|
136 |
let val (tp,ts) = type_of T |
36170
0cdb76723c88
added original constant names to Sledgehammer internal terms + output short names if "debug" is set (for increased readability)
blanchet
parents:
36169
diff
changeset
|
137 |
val v' = CombVar ((make_schematic_var v, string_of_indexname v), tp) |
22078
5084f53cef39
Streamlining: removing the type argument of CombApp; abbreviating ResClause as RC
paulson
parents:
22064
diff
changeset
|
138 |
in (v',ts) end |
37498
b426cbdb5a23
removed Sledgehammer's support for the DFG syntax;
blanchet
parents:
37496
diff
changeset
|
139 |
| combterm_of thy (P $ Q) = |
b426cbdb5a23
removed Sledgehammer's support for the DFG syntax;
blanchet
parents:
37496
diff
changeset
|
140 |
let val (P', tsP) = combterm_of thy P |
b426cbdb5a23
removed Sledgehammer's support for the DFG syntax;
blanchet
parents:
37496
diff
changeset
|
141 |
val (Q', tsQ) = combterm_of thy Q |
b426cbdb5a23
removed Sledgehammer's support for the DFG syntax;
blanchet
parents:
37496
diff
changeset
|
142 |
in (CombApp (P', Q'), union (op =) tsP tsQ) end |
b426cbdb5a23
removed Sledgehammer's support for the DFG syntax;
blanchet
parents:
37496
diff
changeset
|
143 |
| combterm_of _ (t as Abs _) = raise CLAUSE ("HOL clause", t) |
17998
0a869029ca58
A new file that defines datatypes representing FOL clauses that are derived from HOL formulae. This file also has functions that convert lambda terms to combinator expressions, and functions that convert clauses to TPTP format.
mengj
parents:
diff
changeset
|
144 |
|
37498
b426cbdb5a23
removed Sledgehammer's support for the DFG syntax;
blanchet
parents:
37496
diff
changeset
|
145 |
fun predicate_of thy ((@{const Not} $ P), polarity) = |
b426cbdb5a23
removed Sledgehammer's support for the DFG syntax;
blanchet
parents:
37496
diff
changeset
|
146 |
predicate_of thy (P, not polarity) |
b426cbdb5a23
removed Sledgehammer's support for the DFG syntax;
blanchet
parents:
37496
diff
changeset
|
147 |
| predicate_of thy (t, polarity) = |
b426cbdb5a23
removed Sledgehammer's support for the DFG syntax;
blanchet
parents:
37496
diff
changeset
|
148 |
(combterm_of thy (Envir.eta_contract t), polarity) |
17998
0a869029ca58
A new file that defines datatypes representing FOL clauses that are derived from HOL formulae. This file also has functions that convert lambda terms to combinator expressions, and functions that convert clauses to TPTP format.
mengj
parents:
diff
changeset
|
149 |
|
37498
b426cbdb5a23
removed Sledgehammer's support for the DFG syntax;
blanchet
parents:
37496
diff
changeset
|
150 |
fun literals_of_term1 args thy (@{const Trueprop} $ P) = |
b426cbdb5a23
removed Sledgehammer's support for the DFG syntax;
blanchet
parents:
37496
diff
changeset
|
151 |
literals_of_term1 args thy P |
b426cbdb5a23
removed Sledgehammer's support for the DFG syntax;
blanchet
parents:
37496
diff
changeset
|
152 |
| literals_of_term1 args thy (@{const "op |"} $ P $ Q) = |
b426cbdb5a23
removed Sledgehammer's support for the DFG syntax;
blanchet
parents:
37496
diff
changeset
|
153 |
literals_of_term1 (literals_of_term1 args thy P) thy Q |
b426cbdb5a23
removed Sledgehammer's support for the DFG syntax;
blanchet
parents:
37496
diff
changeset
|
154 |
| literals_of_term1 (lits, ts) thy P = |
b426cbdb5a23
removed Sledgehammer's support for the DFG syntax;
blanchet
parents:
37496
diff
changeset
|
155 |
let val ((pred, ts'), pol) = predicate_of thy (P, true) in |
b426cbdb5a23
removed Sledgehammer's support for the DFG syntax;
blanchet
parents:
37496
diff
changeset
|
156 |
(Literal (pol, pred) :: lits, union (op =) ts ts') |
b426cbdb5a23
removed Sledgehammer's support for the DFG syntax;
blanchet
parents:
37496
diff
changeset
|
157 |
end |
b426cbdb5a23
removed Sledgehammer's support for the DFG syntax;
blanchet
parents:
37496
diff
changeset
|
158 |
val literals_of_term = literals_of_term1 ([], []) |
17998
0a869029ca58
A new file that defines datatypes representing FOL clauses that are derived from HOL formulae. This file also has functions that convert lambda terms to combinator expressions, and functions that convert clauses to TPTP format.
mengj
parents:
diff
changeset
|
159 |
|
37399
34f080a12063
proper polymorphic Skolemization of uncached facts + synchronization of caching and relevance filter
blanchet
parents:
36966
diff
changeset
|
160 |
fun skolem_name i j num_T_args = |
34f080a12063
proper polymorphic Skolemization of uncached facts + synchronization of caching and relevance filter
blanchet
parents:
36966
diff
changeset
|
161 |
skolem_prefix ^ (space_implode "_" (map Int.toString [i, j, num_T_args])) ^ |
34f080a12063
proper polymorphic Skolemization of uncached facts + synchronization of caching and relevance filter
blanchet
parents:
36966
diff
changeset
|
162 |
skolem_infix ^ "g" |
34f080a12063
proper polymorphic Skolemization of uncached facts + synchronization of caching and relevance filter
blanchet
parents:
36966
diff
changeset
|
163 |
|
37410
2bf7e6136047
adjusted the polymorphism handling of Skolem constants so that proof reconstruction doesn't fail in "equality_inf"
blanchet
parents:
37399
diff
changeset
|
164 |
fun conceal_skolem_somes i skolem_somes t = |
2bf7e6136047
adjusted the polymorphism handling of Skolem constants so that proof reconstruction doesn't fail in "equality_inf"
blanchet
parents:
37399
diff
changeset
|
165 |
if exists_Const (curry (op =) @{const_name skolem_id} o fst) t then |
37399
34f080a12063
proper polymorphic Skolemization of uncached facts + synchronization of caching and relevance filter
blanchet
parents:
36966
diff
changeset
|
166 |
let |
34f080a12063
proper polymorphic Skolemization of uncached facts + synchronization of caching and relevance filter
blanchet
parents:
36966
diff
changeset
|
167 |
fun aux skolem_somes |
37410
2bf7e6136047
adjusted the polymorphism handling of Skolem constants so that proof reconstruction doesn't fail in "equality_inf"
blanchet
parents:
37399
diff
changeset
|
168 |
(t as (Const (@{const_name skolem_id}, Type (_, [_, T])) $ _)) = |
37399
34f080a12063
proper polymorphic Skolemization of uncached facts + synchronization of caching and relevance filter
blanchet
parents:
36966
diff
changeset
|
169 |
let |
37496
9ae78e12e126
reintroduce new Sledgehammer polymorphic handling code;
blanchet
parents:
37479
diff
changeset
|
170 |
val t = Envir.beta_eta_contract t |
37399
34f080a12063
proper polymorphic Skolemization of uncached facts + synchronization of caching and relevance filter
blanchet
parents:
36966
diff
changeset
|
171 |
val (skolem_somes, s) = |
34f080a12063
proper polymorphic Skolemization of uncached facts + synchronization of caching and relevance filter
blanchet
parents:
36966
diff
changeset
|
172 |
if i = ~1 then |
34f080a12063
proper polymorphic Skolemization of uncached facts + synchronization of caching and relevance filter
blanchet
parents:
36966
diff
changeset
|
173 |
(skolem_somes, @{const_name undefined}) |
37410
2bf7e6136047
adjusted the polymorphism handling of Skolem constants so that proof reconstruction doesn't fail in "equality_inf"
blanchet
parents:
37399
diff
changeset
|
174 |
else case AList.find (op aconv) skolem_somes t of |
37399
34f080a12063
proper polymorphic Skolemization of uncached facts + synchronization of caching and relevance filter
blanchet
parents:
36966
diff
changeset
|
175 |
s :: _ => (skolem_somes, s) |
37436 | 176 |
| [] => |
37399
34f080a12063
proper polymorphic Skolemization of uncached facts + synchronization of caching and relevance filter
blanchet
parents:
36966
diff
changeset
|
177 |
let |
37410
2bf7e6136047
adjusted the polymorphism handling of Skolem constants so that proof reconstruction doesn't fail in "equality_inf"
blanchet
parents:
37399
diff
changeset
|
178 |
val s = skolem_theory_name ^ "." ^ |
37399
34f080a12063
proper polymorphic Skolemization of uncached facts + synchronization of caching and relevance filter
blanchet
parents:
36966
diff
changeset
|
179 |
skolem_name i (length skolem_somes) |
34f080a12063
proper polymorphic Skolemization of uncached facts + synchronization of caching and relevance filter
blanchet
parents:
36966
diff
changeset
|
180 |
(length (Term.add_tvarsT T [])) |
37410
2bf7e6136047
adjusted the polymorphism handling of Skolem constants so that proof reconstruction doesn't fail in "equality_inf"
blanchet
parents:
37399
diff
changeset
|
181 |
in ((s, t) :: skolem_somes, s) end |
2bf7e6136047
adjusted the polymorphism handling of Skolem constants so that proof reconstruction doesn't fail in "equality_inf"
blanchet
parents:
37399
diff
changeset
|
182 |
in (skolem_somes, Const (s, T)) end |
37399
34f080a12063
proper polymorphic Skolemization of uncached facts + synchronization of caching and relevance filter
blanchet
parents:
36966
diff
changeset
|
183 |
| aux skolem_somes (t1 $ t2) = |
34f080a12063
proper polymorphic Skolemization of uncached facts + synchronization of caching and relevance filter
blanchet
parents:
36966
diff
changeset
|
184 |
let |
34f080a12063
proper polymorphic Skolemization of uncached facts + synchronization of caching and relevance filter
blanchet
parents:
36966
diff
changeset
|
185 |
val (skolem_somes, t1) = aux skolem_somes t1 |
34f080a12063
proper polymorphic Skolemization of uncached facts + synchronization of caching and relevance filter
blanchet
parents:
36966
diff
changeset
|
186 |
val (skolem_somes, t2) = aux skolem_somes t2 |
34f080a12063
proper polymorphic Skolemization of uncached facts + synchronization of caching and relevance filter
blanchet
parents:
36966
diff
changeset
|
187 |
in (skolem_somes, t1 $ t2) end |
34f080a12063
proper polymorphic Skolemization of uncached facts + synchronization of caching and relevance filter
blanchet
parents:
36966
diff
changeset
|
188 |
| aux skolem_somes (Abs (s, T, t')) = |
34f080a12063
proper polymorphic Skolemization of uncached facts + synchronization of caching and relevance filter
blanchet
parents:
36966
diff
changeset
|
189 |
let val (skolem_somes, t') = aux skolem_somes t' in |
34f080a12063
proper polymorphic Skolemization of uncached facts + synchronization of caching and relevance filter
blanchet
parents:
36966
diff
changeset
|
190 |
(skolem_somes, Abs (s, T, t')) |
34f080a12063
proper polymorphic Skolemization of uncached facts + synchronization of caching and relevance filter
blanchet
parents:
36966
diff
changeset
|
191 |
end |
34f080a12063
proper polymorphic Skolemization of uncached facts + synchronization of caching and relevance filter
blanchet
parents:
36966
diff
changeset
|
192 |
| aux skolem_somes t = (skolem_somes, t) |
34f080a12063
proper polymorphic Skolemization of uncached facts + synchronization of caching and relevance filter
blanchet
parents:
36966
diff
changeset
|
193 |
in aux skolem_somes t end |
34f080a12063
proper polymorphic Skolemization of uncached facts + synchronization of caching and relevance filter
blanchet
parents:
36966
diff
changeset
|
194 |
else |
34f080a12063
proper polymorphic Skolemization of uncached facts + synchronization of caching and relevance filter
blanchet
parents:
36966
diff
changeset
|
195 |
(skolem_somes, t) |
34f080a12063
proper polymorphic Skolemization of uncached facts + synchronization of caching and relevance filter
blanchet
parents:
36966
diff
changeset
|
196 |
|
35865 | 197 |
(* Trivial problem, which resolution cannot handle (empty clause) *) |
198 |
exception TRIVIAL; |
|
28835 | 199 |
|
17998
0a869029ca58
A new file that defines datatypes representing FOL clauses that are derived from HOL formulae. This file also has functions that convert lambda terms to combinator expressions, and functions that convert clauses to TPTP format.
mengj
parents:
diff
changeset
|
200 |
(* making axiom and conjecture clauses *) |
37498
b426cbdb5a23
removed Sledgehammer's support for the DFG syntax;
blanchet
parents:
37496
diff
changeset
|
201 |
fun make_clause thy (clause_id, axiom_name, kind, th) skolem_somes = |
37399
34f080a12063
proper polymorphic Skolemization of uncached facts + synchronization of caching and relevance filter
blanchet
parents:
36966
diff
changeset
|
202 |
let |
34f080a12063
proper polymorphic Skolemization of uncached facts + synchronization of caching and relevance filter
blanchet
parents:
36966
diff
changeset
|
203 |
val (skolem_somes, t) = |
37410
2bf7e6136047
adjusted the polymorphism handling of Skolem constants so that proof reconstruction doesn't fail in "equality_inf"
blanchet
parents:
37399
diff
changeset
|
204 |
th |> prop_of |> conceal_skolem_somes clause_id skolem_somes |
37498
b426cbdb5a23
removed Sledgehammer's support for the DFG syntax;
blanchet
parents:
37496
diff
changeset
|
205 |
val (lits, ctypes_sorts) = literals_of_term thy t |
37399
34f080a12063
proper polymorphic Skolemization of uncached facts + synchronization of caching and relevance filter
blanchet
parents:
36966
diff
changeset
|
206 |
in |
34f080a12063
proper polymorphic Skolemization of uncached facts + synchronization of caching and relevance filter
blanchet
parents:
36966
diff
changeset
|
207 |
if forall isFalse lits then |
34f080a12063
proper polymorphic Skolemization of uncached facts + synchronization of caching and relevance filter
blanchet
parents:
36966
diff
changeset
|
208 |
raise TRIVIAL |
34f080a12063
proper polymorphic Skolemization of uncached facts + synchronization of caching and relevance filter
blanchet
parents:
36966
diff
changeset
|
209 |
else |
34f080a12063
proper polymorphic Skolemization of uncached facts + synchronization of caching and relevance filter
blanchet
parents:
36966
diff
changeset
|
210 |
(skolem_somes, |
34f080a12063
proper polymorphic Skolemization of uncached facts + synchronization of caching and relevance filter
blanchet
parents:
36966
diff
changeset
|
211 |
HOLClause {clause_id = clause_id, axiom_name = axiom_name, th = th, |
34f080a12063
proper polymorphic Skolemization of uncached facts + synchronization of caching and relevance filter
blanchet
parents:
36966
diff
changeset
|
212 |
kind = kind, literals = lits, ctypes_sorts = ctypes_sorts}) |
36218
0e4a01f3e7d3
get rid of "List.foldl" + add timestamp to SPASS
blanchet
parents:
36186
diff
changeset
|
213 |
end |
19354 | 214 |
|
37498
b426cbdb5a23
removed Sledgehammer's support for the DFG syntax;
blanchet
parents:
37496
diff
changeset
|
215 |
fun add_axiom_clause thy (th, (name, id)) (skolem_somes, clss) = |
37399
34f080a12063
proper polymorphic Skolemization of uncached facts + synchronization of caching and relevance filter
blanchet
parents:
36966
diff
changeset
|
216 |
let |
37498
b426cbdb5a23
removed Sledgehammer's support for the DFG syntax;
blanchet
parents:
37496
diff
changeset
|
217 |
val (skolem_somes, cls) = make_clause thy (id, name, Axiom, th) skolem_somes |
37399
34f080a12063
proper polymorphic Skolemization of uncached facts + synchronization of caching and relevance filter
blanchet
parents:
36966
diff
changeset
|
218 |
in (skolem_somes, clss |> not (isTaut cls) ? cons (name, cls)) end |
34f080a12063
proper polymorphic Skolemization of uncached facts + synchronization of caching and relevance filter
blanchet
parents:
36966
diff
changeset
|
219 |
|
37498
b426cbdb5a23
removed Sledgehammer's support for the DFG syntax;
blanchet
parents:
37496
diff
changeset
|
220 |
fun make_axiom_clauses thy clauses = |
b426cbdb5a23
removed Sledgehammer's support for the DFG syntax;
blanchet
parents:
37496
diff
changeset
|
221 |
([], []) |> fold (add_axiom_clause thy) clauses |> snd |
19354 | 222 |
|
37498
b426cbdb5a23
removed Sledgehammer's support for the DFG syntax;
blanchet
parents:
37496
diff
changeset
|
223 |
fun make_conjecture_clauses thy = |
37399
34f080a12063
proper polymorphic Skolemization of uncached facts + synchronization of caching and relevance filter
blanchet
parents:
36966
diff
changeset
|
224 |
let |
34f080a12063
proper polymorphic Skolemization of uncached facts + synchronization of caching and relevance filter
blanchet
parents:
36966
diff
changeset
|
225 |
fun aux _ _ [] = [] |
34f080a12063
proper polymorphic Skolemization of uncached facts + synchronization of caching and relevance filter
blanchet
parents:
36966
diff
changeset
|
226 |
| aux n skolem_somes (th :: ths) = |
34f080a12063
proper polymorphic Skolemization of uncached facts + synchronization of caching and relevance filter
blanchet
parents:
36966
diff
changeset
|
227 |
let |
34f080a12063
proper polymorphic Skolemization of uncached facts + synchronization of caching and relevance filter
blanchet
parents:
36966
diff
changeset
|
228 |
val (skolem_somes, cls) = |
37498
b426cbdb5a23
removed Sledgehammer's support for the DFG syntax;
blanchet
parents:
37496
diff
changeset
|
229 |
make_clause thy (n, "conjecture", Conjecture, th) skolem_somes |
37399
34f080a12063
proper polymorphic Skolemization of uncached facts + synchronization of caching and relevance filter
blanchet
parents:
36966
diff
changeset
|
230 |
in cls :: aux (n + 1) skolem_somes ths end |
34f080a12063
proper polymorphic Skolemization of uncached facts + synchronization of caching and relevance filter
blanchet
parents:
36966
diff
changeset
|
231 |
in aux 0 [] end |
17998
0a869029ca58
A new file that defines datatypes representing FOL clauses that are derived from HOL formulae. This file also has functions that convert lambda terms to combinator expressions, and functions that convert clauses to TPTP format.
mengj
parents:
diff
changeset
|
232 |
|
0a869029ca58
A new file that defines datatypes representing FOL clauses that are derived from HOL formulae. This file also has functions that convert lambda terms to combinator expressions, and functions that convert clauses to TPTP format.
mengj
parents:
diff
changeset
|
233 |
(**********************************************************************) |
37498
b426cbdb5a23
removed Sledgehammer's support for the DFG syntax;
blanchet
parents:
37496
diff
changeset
|
234 |
(* convert clause into TPTP format *) |
17998
0a869029ca58
A new file that defines datatypes representing FOL clauses that are derived from HOL formulae. This file also has functions that convert lambda terms to combinator expressions, and functions that convert clauses to TPTP format.
mengj
parents:
diff
changeset
|
235 |
(**********************************************************************) |
0a869029ca58
A new file that defines datatypes representing FOL clauses that are derived from HOL formulae. This file also has functions that convert lambda terms to combinator expressions, and functions that convert clauses to TPTP format.
mengj
parents:
diff
changeset
|
236 |
|
22078
5084f53cef39
Streamlining: removing the type argument of CombApp; abbreviating ResClause as RC
paulson
parents:
22064
diff
changeset
|
237 |
(*Result of a function type; no need to check that the argument type matches.*) |
36909
7d5587f6d5f7
made Sledgehammer's full-typed proof reconstruction work for the first time;
blanchet
parents:
36565
diff
changeset
|
238 |
fun result_type (TyConstr (_, [_, tp2])) = tp2 |
7d5587f6d5f7
made Sledgehammer's full-typed proof reconstruction work for the first time;
blanchet
parents:
36565
diff
changeset
|
239 |
| result_type _ = raise Fail "non-function type" |
22078
5084f53cef39
Streamlining: removing the type argument of CombApp; abbreviating ResClause as RC
paulson
parents:
22064
diff
changeset
|
240 |
|
32994 | 241 |
fun type_of_combterm (CombConst (_, tp, _)) = tp |
242 |
| type_of_combterm (CombVar (_, tp)) = tp |
|
243 |
| type_of_combterm (CombApp (t1, _)) = result_type (type_of_combterm t1); |
|
17998
0a869029ca58
A new file that defines datatypes representing FOL clauses that are derived from HOL formulae. This file also has functions that convert lambda terms to combinator expressions, and functions that convert clauses to TPTP format.
mengj
parents:
diff
changeset
|
244 |
|
22064 | 245 |
(*gets the head of a combinator application, along with the list of arguments*) |
35865 | 246 |
fun strip_combterm_comb u = |
22078
5084f53cef39
Streamlining: removing the type argument of CombApp; abbreviating ResClause as RC
paulson
parents:
22064
diff
changeset
|
247 |
let fun stripc (CombApp(t,u), ts) = stripc (t, u::ts) |
22064 | 248 |
| stripc x = x |
249 |
in stripc(u,[]) end; |
|
250 |
||
36909
7d5587f6d5f7
made Sledgehammer's full-typed proof reconstruction work for the first time;
blanchet
parents:
36565
diff
changeset
|
251 |
val type_wrapper_name = "ti" |
22851
7b7d6e1c70b6
First-order variant of the fully-typed translation
paulson
parents:
22825
diff
changeset
|
252 |
|
36235
61159615a0c5
added "explicit_apply" option to Sledgehammer, to control whether an explicit apply function should be used as much or as little as possible (replaces a previous global variable)
blanchet
parents:
36233
diff
changeset
|
253 |
fun head_needs_hBOOL explicit_apply const_needs_hBOOL |
61159615a0c5
added "explicit_apply" option to Sledgehammer, to control whether an explicit apply function should be used as much or as little as possible (replaces a previous global variable)
blanchet
parents:
36233
diff
changeset
|
254 |
(CombConst ((c, _), _, _)) = |
61159615a0c5
added "explicit_apply" option to Sledgehammer, to control whether an explicit apply function should be used as much or as little as possible (replaces a previous global variable)
blanchet
parents:
36233
diff
changeset
|
255 |
needs_hBOOL explicit_apply const_needs_hBOOL c |
61159615a0c5
added "explicit_apply" option to Sledgehammer, to control whether an explicit apply function should be used as much or as little as possible (replaces a previous global variable)
blanchet
parents:
36233
diff
changeset
|
256 |
| head_needs_hBOOL _ _ _ = true |
22851
7b7d6e1c70b6
First-order variant of the fully-typed translation
paulson
parents:
22825
diff
changeset
|
257 |
|
36170
0cdb76723c88
added original constant names to Sledgehammer internal terms + output short names if "debug" is set (for increased readability)
blanchet
parents:
36169
diff
changeset
|
258 |
fun wrap_type full_types (s, ty) pool = |
0cdb76723c88
added original constant names to Sledgehammer internal terms + output short names if "debug" is set (for increased readability)
blanchet
parents:
36169
diff
changeset
|
259 |
if full_types then |
0cdb76723c88
added original constant names to Sledgehammer internal terms + output short names if "debug" is set (for increased readability)
blanchet
parents:
36169
diff
changeset
|
260 |
let val (s', pool) = string_of_fol_type ty pool in |
36909
7d5587f6d5f7
made Sledgehammer's full-typed proof reconstruction work for the first time;
blanchet
parents:
36565
diff
changeset
|
261 |
(type_wrapper_name ^ paren_pack [s, s'], pool) |
36170
0cdb76723c88
added original constant names to Sledgehammer internal terms + output short names if "debug" is set (for increased readability)
blanchet
parents:
36169
diff
changeset
|
262 |
end |
0cdb76723c88
added original constant names to Sledgehammer internal terms + output short names if "debug" is set (for increased readability)
blanchet
parents:
36169
diff
changeset
|
263 |
else |
0cdb76723c88
added original constant names to Sledgehammer internal terms + output short names if "debug" is set (for increased readability)
blanchet
parents:
36169
diff
changeset
|
264 |
(s, pool) |
0cdb76723c88
added original constant names to Sledgehammer internal terms + output short names if "debug" is set (for increased readability)
blanchet
parents:
36169
diff
changeset
|
265 |
|
36235
61159615a0c5
added "explicit_apply" option to Sledgehammer, to control whether an explicit apply function should be used as much or as little as possible (replaces a previous global variable)
blanchet
parents:
36233
diff
changeset
|
266 |
fun wrap_type_if full_types explicit_apply cnh (head, s, tp) = |
61159615a0c5
added "explicit_apply" option to Sledgehammer, to control whether an explicit apply function should be used as much or as little as possible (replaces a previous global variable)
blanchet
parents:
36233
diff
changeset
|
267 |
if head_needs_hBOOL explicit_apply cnh head then |
61159615a0c5
added "explicit_apply" option to Sledgehammer, to control whether an explicit apply function should be used as much or as little as possible (replaces a previous global variable)
blanchet
parents:
36233
diff
changeset
|
268 |
wrap_type full_types (s, tp) |
61159615a0c5
added "explicit_apply" option to Sledgehammer, to control whether an explicit apply function should be used as much or as little as possible (replaces a previous global variable)
blanchet
parents:
36233
diff
changeset
|
269 |
else |
61159615a0c5
added "explicit_apply" option to Sledgehammer, to control whether an explicit apply function should be used as much or as little as possible (replaces a previous global variable)
blanchet
parents:
36233
diff
changeset
|
270 |
pair s |
24311 | 271 |
|
35865 | 272 |
fun apply ss = "hAPP" ^ paren_pack ss; |
22851
7b7d6e1c70b6
First-order variant of the fully-typed translation
paulson
parents:
22825
diff
changeset
|
273 |
|
22064 | 274 |
fun rev_apply (v, []) = v |
22851
7b7d6e1c70b6
First-order variant of the fully-typed translation
paulson
parents:
22825
diff
changeset
|
275 |
| rev_apply (v, arg::args) = apply [rev_apply (v, args), arg]; |
22064 | 276 |
|
277 |
fun string_apply (v, args) = rev_apply (v, rev args); |
|
278 |
||
36170
0cdb76723c88
added original constant names to Sledgehammer internal terms + output short names if "debug" is set (for increased readability)
blanchet
parents:
36169
diff
changeset
|
279 |
(* Apply an operator to the argument strings, using either the "apply" operator |
0cdb76723c88
added original constant names to Sledgehammer internal terms + output short names if "debug" is set (for increased readability)
blanchet
parents:
36169
diff
changeset
|
280 |
or direct function application. *) |
0cdb76723c88
added original constant names to Sledgehammer internal terms + output short names if "debug" is set (for increased readability)
blanchet
parents:
36169
diff
changeset
|
281 |
fun string_of_application full_types cma (CombConst ((s, s'), _, tvars), args) |
0cdb76723c88
added original constant names to Sledgehammer internal terms + output short names if "debug" is set (for increased readability)
blanchet
parents:
36169
diff
changeset
|
282 |
pool = |
0cdb76723c88
added original constant names to Sledgehammer internal terms + output short names if "debug" is set (for increased readability)
blanchet
parents:
36169
diff
changeset
|
283 |
let |
0cdb76723c88
added original constant names to Sledgehammer internal terms + output short names if "debug" is set (for increased readability)
blanchet
parents:
36169
diff
changeset
|
284 |
val s = if s = "equal" then "c_fequal" else s |
0cdb76723c88
added original constant names to Sledgehammer internal terms + output short names if "debug" is set (for increased readability)
blanchet
parents:
36169
diff
changeset
|
285 |
val nargs = min_arity_of cma s |
0cdb76723c88
added original constant names to Sledgehammer internal terms + output short names if "debug" is set (for increased readability)
blanchet
parents:
36169
diff
changeset
|
286 |
val args1 = List.take (args, nargs) |
0cdb76723c88
added original constant names to Sledgehammer internal terms + output short names if "debug" is set (for increased readability)
blanchet
parents:
36169
diff
changeset
|
287 |
handle Subscript => |
0cdb76723c88
added original constant names to Sledgehammer internal terms + output short names if "debug" is set (for increased readability)
blanchet
parents:
36169
diff
changeset
|
288 |
raise Fail (quote s ^ " has arity " ^ Int.toString nargs ^ |
0cdb76723c88
added original constant names to Sledgehammer internal terms + output short names if "debug" is set (for increased readability)
blanchet
parents:
36169
diff
changeset
|
289 |
" but is applied to " ^ commas (map quote args)) |
0cdb76723c88
added original constant names to Sledgehammer internal terms + output short names if "debug" is set (for increased readability)
blanchet
parents:
36169
diff
changeset
|
290 |
val args2 = List.drop (args, nargs) |
0cdb76723c88
added original constant names to Sledgehammer internal terms + output short names if "debug" is set (for increased readability)
blanchet
parents:
36169
diff
changeset
|
291 |
val (targs, pool) = if full_types then ([], pool) |
0cdb76723c88
added original constant names to Sledgehammer internal terms + output short names if "debug" is set (for increased readability)
blanchet
parents:
36169
diff
changeset
|
292 |
else pool_map string_of_fol_type tvars pool |
0cdb76723c88
added original constant names to Sledgehammer internal terms + output short names if "debug" is set (for increased readability)
blanchet
parents:
36169
diff
changeset
|
293 |
val (s, pool) = nice_name (s, s') pool |
0cdb76723c88
added original constant names to Sledgehammer internal terms + output short names if "debug" is set (for increased readability)
blanchet
parents:
36169
diff
changeset
|
294 |
in (string_apply (s ^ paren_pack (args1 @ targs), args2), pool) end |
0cdb76723c88
added original constant names to Sledgehammer internal terms + output short names if "debug" is set (for increased readability)
blanchet
parents:
36169
diff
changeset
|
295 |
| string_of_application _ _ (CombVar (name, _), args) pool = |
0cdb76723c88
added original constant names to Sledgehammer internal terms + output short names if "debug" is set (for increased readability)
blanchet
parents:
36169
diff
changeset
|
296 |
nice_name name pool |>> (fn s => string_apply (s, args)) |
24311 | 297 |
|
36235
61159615a0c5
added "explicit_apply" option to Sledgehammer, to control whether an explicit apply function should be used as much or as little as possible (replaces a previous global variable)
blanchet
parents:
36233
diff
changeset
|
298 |
fun string_of_combterm (params as (full_types, explicit_apply, cma, cnh)) t |
61159615a0c5
added "explicit_apply" option to Sledgehammer, to control whether an explicit apply function should be used as much or as little as possible (replaces a previous global variable)
blanchet
parents:
36233
diff
changeset
|
299 |
pool = |
36170
0cdb76723c88
added original constant names to Sledgehammer internal terms + output short names if "debug" is set (for increased readability)
blanchet
parents:
36169
diff
changeset
|
300 |
let |
0cdb76723c88
added original constant names to Sledgehammer internal terms + output short names if "debug" is set (for increased readability)
blanchet
parents:
36169
diff
changeset
|
301 |
val (head, args) = strip_combterm_comb t |
0cdb76723c88
added original constant names to Sledgehammer internal terms + output short names if "debug" is set (for increased readability)
blanchet
parents:
36169
diff
changeset
|
302 |
val (ss, pool) = pool_map (string_of_combterm params) args pool |
0cdb76723c88
added original constant names to Sledgehammer internal terms + output short names if "debug" is set (for increased readability)
blanchet
parents:
36169
diff
changeset
|
303 |
val (s, pool) = string_of_application full_types cma (head, ss) pool |
36235
61159615a0c5
added "explicit_apply" option to Sledgehammer, to control whether an explicit apply function should be used as much or as little as possible (replaces a previous global variable)
blanchet
parents:
36233
diff
changeset
|
304 |
in |
61159615a0c5
added "explicit_apply" option to Sledgehammer, to control whether an explicit apply function should be used as much or as little as possible (replaces a previous global variable)
blanchet
parents:
36233
diff
changeset
|
305 |
wrap_type_if full_types explicit_apply cnh (head, s, type_of_combterm t) |
61159615a0c5
added "explicit_apply" option to Sledgehammer, to control whether an explicit apply function should be used as much or as little as possible (replaces a previous global variable)
blanchet
parents:
36233
diff
changeset
|
306 |
pool |
61159615a0c5
added "explicit_apply" option to Sledgehammer, to control whether an explicit apply function should be used as much or as little as possible (replaces a previous global variable)
blanchet
parents:
36233
diff
changeset
|
307 |
end |
18356
443717b3a9ad
Added new type embedding methods for translating HOL clauses.
mengj
parents:
18276
diff
changeset
|
308 |
|
22064 | 309 |
(*Boolean-valued terms are here converted to literals.*) |
36170
0cdb76723c88
added original constant names to Sledgehammer internal terms + output short names if "debug" is set (for increased readability)
blanchet
parents:
36169
diff
changeset
|
310 |
fun boolify params c = |
0cdb76723c88
added original constant names to Sledgehammer internal terms + output short names if "debug" is set (for increased readability)
blanchet
parents:
36169
diff
changeset
|
311 |
string_of_combterm params c #>> prefix "hBOOL" o paren_pack o single |
22064 | 312 |
|
36235
61159615a0c5
added "explicit_apply" option to Sledgehammer, to control whether an explicit apply function should be used as much or as little as possible (replaces a previous global variable)
blanchet
parents:
36233
diff
changeset
|
313 |
fun string_of_predicate (params as (_, explicit_apply, _, cnh)) t = |
37498
b426cbdb5a23
removed Sledgehammer's support for the DFG syntax;
blanchet
parents:
37496
diff
changeset
|
314 |
case #1 (strip_combterm_comb t) of |
b426cbdb5a23
removed Sledgehammer's support for the DFG syntax;
blanchet
parents:
37496
diff
changeset
|
315 |
CombConst ((s, _), _, _) => |
b426cbdb5a23
removed Sledgehammer's support for the DFG syntax;
blanchet
parents:
37496
diff
changeset
|
316 |
(if needs_hBOOL explicit_apply cnh s then boolify else string_of_combterm) |
b426cbdb5a23
removed Sledgehammer's support for the DFG syntax;
blanchet
parents:
37496
diff
changeset
|
317 |
params t |
b426cbdb5a23
removed Sledgehammer's support for the DFG syntax;
blanchet
parents:
37496
diff
changeset
|
318 |
| _ => boolify params t |
18356
443717b3a9ad
Added new type embedding methods for translating HOL clauses.
mengj
parents:
18276
diff
changeset
|
319 |
|
17998
0a869029ca58
A new file that defines datatypes representing FOL clauses that are derived from HOL formulae. This file also has functions that convert lambda terms to combinator expressions, and functions that convert clauses to TPTP format.
mengj
parents:
diff
changeset
|
320 |
|
36170
0cdb76723c88
added original constant names to Sledgehammer internal terms + output short names if "debug" is set (for increased readability)
blanchet
parents:
36169
diff
changeset
|
321 |
(*** TPTP format ***) |
19720 | 322 |
|
36170
0cdb76723c88
added original constant names to Sledgehammer internal terms + output short names if "debug" is set (for increased readability)
blanchet
parents:
36169
diff
changeset
|
323 |
fun tptp_of_equality params pos (t1, t2) = |
0cdb76723c88
added original constant names to Sledgehammer internal terms + output short names if "debug" is set (for increased readability)
blanchet
parents:
36169
diff
changeset
|
324 |
pool_map (string_of_combterm params) [t1, t2] |
0cdb76723c88
added original constant names to Sledgehammer internal terms + output short names if "debug" is set (for increased readability)
blanchet
parents:
36169
diff
changeset
|
325 |
#>> space_implode (if pos then " = " else " != ") |
24311 | 326 |
|
36170
0cdb76723c88
added original constant names to Sledgehammer internal terms + output short names if "debug" is set (for increased readability)
blanchet
parents:
36169
diff
changeset
|
327 |
fun tptp_literal params |
0cdb76723c88
added original constant names to Sledgehammer internal terms + output short names if "debug" is set (for increased readability)
blanchet
parents:
36169
diff
changeset
|
328 |
(Literal (pos, CombApp (CombApp (CombConst (("equal", _), _, _), t1), |
0cdb76723c88
added original constant names to Sledgehammer internal terms + output short names if "debug" is set (for increased readability)
blanchet
parents:
36169
diff
changeset
|
329 |
t2))) = |
0cdb76723c88
added original constant names to Sledgehammer internal terms + output short names if "debug" is set (for increased readability)
blanchet
parents:
36169
diff
changeset
|
330 |
tptp_of_equality params pos (t1, t2) |
0cdb76723c88
added original constant names to Sledgehammer internal terms + output short names if "debug" is set (for increased readability)
blanchet
parents:
36169
diff
changeset
|
331 |
| tptp_literal params (Literal (pos, pred)) = |
0cdb76723c88
added original constant names to Sledgehammer internal terms + output short names if "debug" is set (for increased readability)
blanchet
parents:
36169
diff
changeset
|
332 |
string_of_predicate params pred #>> tptp_sign pos |
0cdb76723c88
added original constant names to Sledgehammer internal terms + output short names if "debug" is set (for increased readability)
blanchet
parents:
36169
diff
changeset
|
333 |
|
0cdb76723c88
added original constant names to Sledgehammer internal terms + output short names if "debug" is set (for increased readability)
blanchet
parents:
36169
diff
changeset
|
334 |
(* Given a clause, returns its literals paired with a list of literals |
0cdb76723c88
added original constant names to Sledgehammer internal terms + output short names if "debug" is set (for increased readability)
blanchet
parents:
36169
diff
changeset
|
335 |
concerning TFrees; the latter should only occur in conjecture clauses. *) |
36556
81dc2c20f052
use readable names in "debug" mode for type vars + don't pipe facts using "using" but rather give them directly to metis (works better with type variables)
blanchet
parents:
36481
diff
changeset
|
336 |
fun tptp_type_literals params pos (HOLClause {literals, ctypes_sorts, ...}) |
81dc2c20f052
use readable names in "debug" mode for type vars + don't pipe facts using "using" but rather give them directly to metis (works better with type variables)
blanchet
parents:
36481
diff
changeset
|
337 |
pool = |
81dc2c20f052
use readable names in "debug" mode for type vars + don't pipe facts using "using" but rather give them directly to metis (works better with type variables)
blanchet
parents:
36481
diff
changeset
|
338 |
let |
81dc2c20f052
use readable names in "debug" mode for type vars + don't pipe facts using "using" but rather give them directly to metis (works better with type variables)
blanchet
parents:
36481
diff
changeset
|
339 |
val (lits, pool) = pool_map (tptp_literal params) literals pool |
81dc2c20f052
use readable names in "debug" mode for type vars + don't pipe facts using "using" but rather give them directly to metis (works better with type variables)
blanchet
parents:
36481
diff
changeset
|
340 |
val (tylits, pool) = pool_map (tptp_of_type_literal pos) |
36966
adc11fb3f3aa
generate proper arity declarations for TFrees for SPASS's DFG format;
blanchet
parents:
36922
diff
changeset
|
341 |
(type_literals_for_types ctypes_sorts) pool |
36556
81dc2c20f052
use readable names in "debug" mode for type vars + don't pipe facts using "using" but rather give them directly to metis (works better with type variables)
blanchet
parents:
36481
diff
changeset
|
342 |
in ((lits, tylits), pool) end |
24311 | 343 |
|
36170
0cdb76723c88
added original constant names to Sledgehammer internal terms + output short names if "debug" is set (for increased readability)
blanchet
parents:
36169
diff
changeset
|
344 |
fun tptp_clause params (cls as HOLClause {axiom_name, clause_id, kind, ...}) |
0cdb76723c88
added original constant names to Sledgehammer internal terms + output short names if "debug" is set (for increased readability)
blanchet
parents:
36169
diff
changeset
|
345 |
pool = |
37498
b426cbdb5a23
removed Sledgehammer's support for the DFG syntax;
blanchet
parents:
37496
diff
changeset
|
346 |
let |
36170
0cdb76723c88
added original constant names to Sledgehammer internal terms + output short names if "debug" is set (for increased readability)
blanchet
parents:
36169
diff
changeset
|
347 |
val ((lits, tylits), pool) = |
0cdb76723c88
added original constant names to Sledgehammer internal terms + output short names if "debug" is set (for increased readability)
blanchet
parents:
36169
diff
changeset
|
348 |
tptp_type_literals params (kind = Conjecture) cls pool |
24937
340523598914
context-based treatment of generalization; also handling TFrees in axiom clauses
paulson
parents:
24385
diff
changeset
|
349 |
in |
36170
0cdb76723c88
added original constant names to Sledgehammer internal terms + output short names if "debug" is set (for increased readability)
blanchet
parents:
36169
diff
changeset
|
350 |
((gen_tptp_cls (clause_id, axiom_name, kind, lits, tylits), tylits), pool) |
0cdb76723c88
added original constant names to Sledgehammer internal terms + output short names if "debug" is set (for increased readability)
blanchet
parents:
36169
diff
changeset
|
351 |
end |
17998
0a869029ca58
A new file that defines datatypes representing FOL clauses that are derived from HOL formulae. This file also has functions that convert lambda terms to combinator expressions, and functions that convert clauses to TPTP format.
mengj
parents:
diff
changeset
|
352 |
|
0a869029ca58
A new file that defines datatypes representing FOL clauses that are derived from HOL formulae. This file also has functions that convert lambda terms to combinator expressions, and functions that convert clauses to TPTP format.
mengj
parents:
diff
changeset
|
353 |
|
18440
72ee07f4b56b
Literals in clauses are sorted now. Added functions for clause equivalence tests and hashing clauses to words.
mengj
parents:
18356
diff
changeset
|
354 |
(**********************************************************************) |
19198
e6f1ff40ba99
Added tptp_write_file to write all necessary ATP input clauses to one file.
mengj
parents:
19130
diff
changeset
|
355 |
(* write clauses to files *) |
e6f1ff40ba99
Added tptp_write_file to write all necessary ATP input clauses to one file.
mengj
parents:
19130
diff
changeset
|
356 |
(**********************************************************************) |
e6f1ff40ba99
Added tptp_write_file to write all necessary ATP input clauses to one file.
mengj
parents:
19130
diff
changeset
|
357 |
|
36218
0e4a01f3e7d3
get rid of "List.foldl" + add timestamp to SPASS
blanchet
parents:
36186
diff
changeset
|
358 |
fun count_combterm (CombConst ((c, _), _, _)) = |
0e4a01f3e7d3
get rid of "List.foldl" + add timestamp to SPASS
blanchet
parents:
36186
diff
changeset
|
359 |
Symtab.map_entry c (Integer.add 1) |
0e4a01f3e7d3
get rid of "List.foldl" + add timestamp to SPASS
blanchet
parents:
36186
diff
changeset
|
360 |
| count_combterm (CombVar _) = I |
0e4a01f3e7d3
get rid of "List.foldl" + add timestamp to SPASS
blanchet
parents:
36186
diff
changeset
|
361 |
| count_combterm (CombApp (t1, t2)) = count_combterm t1 #> count_combterm t2 |
21573
8a7a68c0096c
Removed the references for counting combinators. Instead they are counted in actual clauses.
paulson
parents:
21561
diff
changeset
|
362 |
|
36218
0e4a01f3e7d3
get rid of "List.foldl" + add timestamp to SPASS
blanchet
parents:
36186
diff
changeset
|
363 |
fun count_literal (Literal (_, t)) = count_combterm t |
21573
8a7a68c0096c
Removed the references for counting combinators. Instead they are counted in actual clauses.
paulson
parents:
21561
diff
changeset
|
364 |
|
36218
0e4a01f3e7d3
get rid of "List.foldl" + add timestamp to SPASS
blanchet
parents:
36186
diff
changeset
|
365 |
fun count_clause (HOLClause {literals, ...}) = fold count_literal literals |
21573
8a7a68c0096c
Removed the references for counting combinators. Instead they are counted in actual clauses.
paulson
parents:
21561
diff
changeset
|
366 |
|
37479
f6b1ee5b420b
try to improve Sledgehammer/Metis's behavior in full_types mode, e.g. by handing True, False, and If better
blanchet
parents:
37436
diff
changeset
|
367 |
val raw_cnf_rules_pairs = map (fn (name, thm) => (thm, (name, 0))) |
f6b1ee5b420b
try to improve Sledgehammer/Metis's behavior in full_types mode, e.g. by handing True, False, and If better
blanchet
parents:
37436
diff
changeset
|
368 |
fun cnf_helper_thms thy raw = |
f6b1ee5b420b
try to improve Sledgehammer/Metis's behavior in full_types mode, e.g. by handing True, False, and If better
blanchet
parents:
37436
diff
changeset
|
369 |
map (`Thm.get_name_hint) |
f6b1ee5b420b
try to improve Sledgehammer/Metis's behavior in full_types mode, e.g. by handing True, False, and If better
blanchet
parents:
37436
diff
changeset
|
370 |
#> (if raw then raw_cnf_rules_pairs else cnf_rules_pairs thy) |
f6b1ee5b420b
try to improve Sledgehammer/Metis's behavior in full_types mode, e.g. by handing True, False, and If better
blanchet
parents:
37436
diff
changeset
|
371 |
|
f6b1ee5b420b
try to improve Sledgehammer/Metis's behavior in full_types mode, e.g. by handing True, False, and If better
blanchet
parents:
37436
diff
changeset
|
372 |
val optional_helpers = |
f6b1ee5b420b
try to improve Sledgehammer/Metis's behavior in full_types mode, e.g. by handing True, False, and If better
blanchet
parents:
37436
diff
changeset
|
373 |
[(["c_COMBI", "c_COMBK"], (false, @{thms COMBI_def COMBK_def})), |
f6b1ee5b420b
try to improve Sledgehammer/Metis's behavior in full_types mode, e.g. by handing True, False, and If better
blanchet
parents:
37436
diff
changeset
|
374 |
(["c_COMBB", "c_COMBC"], (false, @{thms COMBB_def COMBC_def})), |
f6b1ee5b420b
try to improve Sledgehammer/Metis's behavior in full_types mode, e.g. by handing True, False, and If better
blanchet
parents:
37436
diff
changeset
|
375 |
(["c_COMBS"], (false, @{thms COMBS_def}))] |
f6b1ee5b420b
try to improve Sledgehammer/Metis's behavior in full_types mode, e.g. by handing True, False, and If better
blanchet
parents:
37436
diff
changeset
|
376 |
val optional_typed_helpers = |
f6b1ee5b420b
try to improve Sledgehammer/Metis's behavior in full_types mode, e.g. by handing True, False, and If better
blanchet
parents:
37436
diff
changeset
|
377 |
[(["c_True", "c_False"], (true, @{thms True_or_False})), |
f6b1ee5b420b
try to improve Sledgehammer/Metis's behavior in full_types mode, e.g. by handing True, False, and If better
blanchet
parents:
37436
diff
changeset
|
378 |
(["c_If"], (true, @{thms if_True if_False True_or_False}))] |
f6b1ee5b420b
try to improve Sledgehammer/Metis's behavior in full_types mode, e.g. by handing True, False, and If better
blanchet
parents:
37436
diff
changeset
|
379 |
val mandatory_helpers = @{thms fequal_imp_equal equal_imp_fequal} |
20644 | 380 |
|
37479
f6b1ee5b420b
try to improve Sledgehammer/Metis's behavior in full_types mode, e.g. by handing True, False, and If better
blanchet
parents:
37436
diff
changeset
|
381 |
val init_counters = |
f6b1ee5b420b
try to improve Sledgehammer/Metis's behavior in full_types mode, e.g. by handing True, False, and If better
blanchet
parents:
37436
diff
changeset
|
382 |
Symtab.make (maps (maps (map (rpair 0) o fst)) |
f6b1ee5b420b
try to improve Sledgehammer/Metis's behavior in full_types mode, e.g. by handing True, False, and If better
blanchet
parents:
37436
diff
changeset
|
383 |
[optional_helpers, optional_typed_helpers]) |
f6b1ee5b420b
try to improve Sledgehammer/Metis's behavior in full_types mode, e.g. by handing True, False, and If better
blanchet
parents:
37436
diff
changeset
|
384 |
|
37498
b426cbdb5a23
removed Sledgehammer's support for the DFG syntax;
blanchet
parents:
37496
diff
changeset
|
385 |
fun get_helper_clauses thy is_FO full_types conjectures axcls = |
37479
f6b1ee5b420b
try to improve Sledgehammer/Metis's behavior in full_types mode, e.g. by handing True, False, and If better
blanchet
parents:
37436
diff
changeset
|
386 |
let |
37498
b426cbdb5a23
removed Sledgehammer's support for the DFG syntax;
blanchet
parents:
37496
diff
changeset
|
387 |
val axclauses = map snd (make_axiom_clauses thy axcls) |
37479
f6b1ee5b420b
try to improve Sledgehammer/Metis's behavior in full_types mode, e.g. by handing True, False, and If better
blanchet
parents:
37436
diff
changeset
|
388 |
val ct = fold (fold count_clause) [conjectures, axclauses] init_counters |
f6b1ee5b420b
try to improve Sledgehammer/Metis's behavior in full_types mode, e.g. by handing True, False, and If better
blanchet
parents:
37436
diff
changeset
|
389 |
fun is_needed c = the (Symtab.lookup ct c) > 0 |
f6b1ee5b420b
try to improve Sledgehammer/Metis's behavior in full_types mode, e.g. by handing True, False, and If better
blanchet
parents:
37436
diff
changeset
|
390 |
val cnfs = |
f6b1ee5b420b
try to improve Sledgehammer/Metis's behavior in full_types mode, e.g. by handing True, False, and If better
blanchet
parents:
37436
diff
changeset
|
391 |
(optional_helpers |
f6b1ee5b420b
try to improve Sledgehammer/Metis's behavior in full_types mode, e.g. by handing True, False, and If better
blanchet
parents:
37436
diff
changeset
|
392 |
|> full_types ? append optional_typed_helpers |
f6b1ee5b420b
try to improve Sledgehammer/Metis's behavior in full_types mode, e.g. by handing True, False, and If better
blanchet
parents:
37436
diff
changeset
|
393 |
|> maps (fn (ss, (raw, ths)) => |
f6b1ee5b420b
try to improve Sledgehammer/Metis's behavior in full_types mode, e.g. by handing True, False, and If better
blanchet
parents:
37436
diff
changeset
|
394 |
if exists is_needed ss then cnf_helper_thms thy raw ths |
f6b1ee5b420b
try to improve Sledgehammer/Metis's behavior in full_types mode, e.g. by handing True, False, and If better
blanchet
parents:
37436
diff
changeset
|
395 |
else [])) |
f6b1ee5b420b
try to improve Sledgehammer/Metis's behavior in full_types mode, e.g. by handing True, False, and If better
blanchet
parents:
37436
diff
changeset
|
396 |
@ (if is_FO then [] else cnf_helper_thms thy false mandatory_helpers) |
37498
b426cbdb5a23
removed Sledgehammer's support for the DFG syntax;
blanchet
parents:
37496
diff
changeset
|
397 |
in map snd (make_axiom_clauses thy cnfs) end |
20791
497e1c9d4a9f
Combinator axioms are now from Isabelle theorems, no need to use helper files.
mengj
parents:
20660
diff
changeset
|
398 |
|
22064 | 399 |
(*Find the minimal arity of each function mentioned in the term. Also, note which uses |
400 |
are not at top level, to see if hBOOL is needed.*) |
|
30150 | 401 |
fun count_constants_term toplev t (const_min_arity, const_needs_hBOOL) = |
35865 | 402 |
let val (head, args) = strip_combterm_comb t |
22064 | 403 |
val n = length args |
36233 | 404 |
val (const_min_arity, const_needs_hBOOL) = |
405 |
(const_min_arity, const_needs_hBOOL) |
|
406 |
|> fold (count_constants_term false) args |
|
22064 | 407 |
in |
408 |
case head of |
|
36170
0cdb76723c88
added original constant names to Sledgehammer internal terms + output short names if "debug" is set (for increased readability)
blanchet
parents:
36169
diff
changeset
|
409 |
CombConst ((a, _),_,_) => (*predicate or function version of "equal"?*) |
24311 | 410 |
let val a = if a="equal" andalso not toplev then "c_fequal" else a |
411 |
in |
|
36233 | 412 |
(const_min_arity |> Symtab.map_default (a, n) (Integer.min n), |
413 |
const_needs_hBOOL |> not toplev ? Symtab.update (a, true)) |
|
24311 | 414 |
end |
32994 | 415 |
| _ => (const_min_arity, const_needs_hBOOL) |
22064 | 416 |
end; |
417 |
||
418 |
(*A literal is a top-level term*) |
|
30150 | 419 |
fun count_constants_lit (Literal (_,t)) (const_min_arity, const_needs_hBOOL) = |
420 |
count_constants_term true t (const_min_arity, const_needs_hBOOL); |
|
22064 | 421 |
|
35865 | 422 |
fun count_constants_clause (HOLClause {literals, ...}) |
423 |
(const_min_arity, const_needs_hBOOL) = |
|
30150 | 424 |
fold count_constants_lit literals (const_min_arity, const_needs_hBOOL); |
22064 | 425 |
|
37498
b426cbdb5a23
removed Sledgehammer's support for the DFG syntax;
blanchet
parents:
37496
diff
changeset
|
426 |
fun display_arity explicit_apply const_needs_hBOOL (c, n) = |
35865 | 427 |
trace_msg (fn () => "Constant: " ^ c ^ |
35826 | 428 |
" arity:\t" ^ Int.toString n ^ |
36235
61159615a0c5
added "explicit_apply" option to Sledgehammer, to control whether an explicit apply function should be used as much or as little as possible (replaces a previous global variable)
blanchet
parents:
36233
diff
changeset
|
429 |
(if needs_hBOOL explicit_apply const_needs_hBOOL c then |
61159615a0c5
added "explicit_apply" option to Sledgehammer, to control whether an explicit apply function should be used as much or as little as possible (replaces a previous global variable)
blanchet
parents:
36233
diff
changeset
|
430 |
" needs hBOOL" |
61159615a0c5
added "explicit_apply" option to Sledgehammer, to control whether an explicit apply function should be used as much or as little as possible (replaces a previous global variable)
blanchet
parents:
36233
diff
changeset
|
431 |
else |
61159615a0c5
added "explicit_apply" option to Sledgehammer, to control whether an explicit apply function should be used as much or as little as possible (replaces a previous global variable)
blanchet
parents:
36233
diff
changeset
|
432 |
"")) |
22064 | 433 |
|
36235
61159615a0c5
added "explicit_apply" option to Sledgehammer, to control whether an explicit apply function should be used as much or as little as possible (replaces a previous global variable)
blanchet
parents:
36233
diff
changeset
|
434 |
fun count_constants explicit_apply |
61159615a0c5
added "explicit_apply" option to Sledgehammer, to control whether an explicit apply function should be used as much or as little as possible (replaces a previous global variable)
blanchet
parents:
36233
diff
changeset
|
435 |
(conjectures, _, extra_clauses, helper_clauses, _, _) = |
61159615a0c5
added "explicit_apply" option to Sledgehammer, to control whether an explicit apply function should be used as much or as little as possible (replaces a previous global variable)
blanchet
parents:
36233
diff
changeset
|
436 |
if not explicit_apply then |
30150 | 437 |
let val (const_min_arity, const_needs_hBOOL) = |
438 |
fold count_constants_clause conjectures (Symtab.empty, Symtab.empty) |
|
31865
5e97c4abd18e
fixed: count constants with supplementary lemmas
immler@in.tum.de
parents:
31839
diff
changeset
|
439 |
|> fold count_constants_clause extra_clauses |
30149 | 440 |
|> fold count_constants_clause helper_clauses |
36481
af99c98121d6
make Sledgehammer more friendly if no subgoal is left
blanchet
parents:
36402
diff
changeset
|
441 |
val _ = app (display_arity explicit_apply const_needs_hBOOL) |
af99c98121d6
make Sledgehammer more friendly if no subgoal is left
blanchet
parents:
36402
diff
changeset
|
442 |
(Symtab.dest (const_min_arity)) |
30150 | 443 |
in (const_min_arity, const_needs_hBOOL) end |
444 |
else (Symtab.empty, Symtab.empty); |
|
22064 | 445 |
|
35865 | 446 |
(* TPTP format *) |
31749 | 447 |
|
36235
61159615a0c5
added "explicit_apply" option to Sledgehammer, to control whether an explicit apply function should be used as much or as little as possible (replaces a previous global variable)
blanchet
parents:
36233
diff
changeset
|
448 |
fun write_tptp_file readable_names full_types explicit_apply file clauses = |
31409
d8537ba165b5
split preparing clauses and writing problemfile;
immler@in.tum.de
parents:
30242
diff
changeset
|
449 |
let |
36167
c1a35be8e476
make Sledgehammer's output more debugging friendly
blanchet
parents:
35963
diff
changeset
|
450 |
fun section _ [] = [] |
36393
be73a2b2443b
support readable names even when Isar proof reconstruction is enabled -- useful for debugging
blanchet
parents:
36375
diff
changeset
|
451 |
| section name ss = |
be73a2b2443b
support readable names even when Isar proof reconstruction is enabled -- useful for debugging
blanchet
parents:
36375
diff
changeset
|
452 |
"\n% " ^ name ^ plural_s (length ss) ^ " (" ^ Int.toString (length ss) ^ |
be73a2b2443b
support readable names even when Isar proof reconstruction is enabled -- useful for debugging
blanchet
parents:
36375
diff
changeset
|
453 |
")\n" :: ss |
36222
0e3e49bd658d
don't use readable names if proof reconstruction is needed, because it uses the structure of names
blanchet
parents:
36219
diff
changeset
|
454 |
val pool = empty_name_pool readable_names |
31865
5e97c4abd18e
fixed: count constants with supplementary lemmas
immler@in.tum.de
parents:
31839
diff
changeset
|
455 |
val (conjectures, axclauses, _, helper_clauses, |
5e97c4abd18e
fixed: count constants with supplementary lemmas
immler@in.tum.de
parents:
31839
diff
changeset
|
456 |
classrel_clauses, arity_clauses) = clauses |
36235
61159615a0c5
added "explicit_apply" option to Sledgehammer, to control whether an explicit apply function should be used as much or as little as possible (replaces a previous global variable)
blanchet
parents:
36233
diff
changeset
|
457 |
val (cma, cnh) = count_constants explicit_apply clauses |
61159615a0c5
added "explicit_apply" option to Sledgehammer, to control whether an explicit apply function should be used as much or as little as possible (replaces a previous global variable)
blanchet
parents:
36233
diff
changeset
|
458 |
val params = (full_types, explicit_apply, cma, cnh) |
36170
0cdb76723c88
added original constant names to Sledgehammer internal terms + output short names if "debug" is set (for increased readability)
blanchet
parents:
36169
diff
changeset
|
459 |
val ((conjecture_clss, tfree_litss), pool) = |
0cdb76723c88
added original constant names to Sledgehammer internal terms + output short names if "debug" is set (for increased readability)
blanchet
parents:
36169
diff
changeset
|
460 |
pool_map (tptp_clause params) conjectures pool |>> ListPair.unzip |
36218
0e4a01f3e7d3
get rid of "List.foldl" + add timestamp to SPASS
blanchet
parents:
36186
diff
changeset
|
461 |
val tfree_clss = map tptp_tfree_clause (fold (union (op =)) tfree_litss []) |
36170
0cdb76723c88
added original constant names to Sledgehammer internal terms + output short names if "debug" is set (for increased readability)
blanchet
parents:
36169
diff
changeset
|
462 |
val (ax_clss, pool) = pool_map (apfst fst oo tptp_clause params) axclauses |
0cdb76723c88
added original constant names to Sledgehammer internal terms + output short names if "debug" is set (for increased readability)
blanchet
parents:
36169
diff
changeset
|
463 |
pool |
0cdb76723c88
added original constant names to Sledgehammer internal terms + output short names if "debug" is set (for increased readability)
blanchet
parents:
36169
diff
changeset
|
464 |
val classrel_clss = map tptp_classrel_clause classrel_clauses |
0cdb76723c88
added original constant names to Sledgehammer internal terms + output short names if "debug" is set (for increased readability)
blanchet
parents:
36169
diff
changeset
|
465 |
val arity_clss = map tptp_arity_clause arity_clauses |
0cdb76723c88
added original constant names to Sledgehammer internal terms + output short names if "debug" is set (for increased readability)
blanchet
parents:
36169
diff
changeset
|
466 |
val (helper_clss, pool) = pool_map (apfst fst oo tptp_clause params) |
0cdb76723c88
added original constant names to Sledgehammer internal terms + output short names if "debug" is set (for increased readability)
blanchet
parents:
36169
diff
changeset
|
467 |
helper_clauses pool |
36402
1b20805974c7
introduced direct proof reconstruction code, eliminating the need for the "neg_clausify" method;
blanchet
parents:
36393
diff
changeset
|
468 |
val conjecture_offset = |
1b20805974c7
introduced direct proof reconstruction code, eliminating the need for the "neg_clausify" method;
blanchet
parents:
36393
diff
changeset
|
469 |
length ax_clss + length classrel_clss + length arity_clss |
1b20805974c7
introduced direct proof reconstruction code, eliminating the need for the "neg_clausify" method;
blanchet
parents:
36393
diff
changeset
|
470 |
+ length helper_clss |
36393
be73a2b2443b
support readable names even when Isar proof reconstruction is enabled -- useful for debugging
blanchet
parents:
36375
diff
changeset
|
471 |
val _ = |
be73a2b2443b
support readable names even when Isar proof reconstruction is enabled -- useful for debugging
blanchet
parents:
36375
diff
changeset
|
472 |
File.write_list file |
37498
b426cbdb5a23
removed Sledgehammer's support for the DFG syntax;
blanchet
parents:
37496
diff
changeset
|
473 |
("% This file was generated by Isabelle (most likely Sledgehammer)\n\ |
b426cbdb5a23
removed Sledgehammer's support for the DFG syntax;
blanchet
parents:
37496
diff
changeset
|
474 |
\% " ^ timestamp () ^ "\n" :: |
36393
be73a2b2443b
support readable names even when Isar proof reconstruction is enabled -- useful for debugging
blanchet
parents:
36375
diff
changeset
|
475 |
section "Relevant fact" ax_clss @ |
36402
1b20805974c7
introduced direct proof reconstruction code, eliminating the need for the "neg_clausify" method;
blanchet
parents:
36393
diff
changeset
|
476 |
section "Class relationship" classrel_clss @ |
1b20805974c7
introduced direct proof reconstruction code, eliminating the need for the "neg_clausify" method;
blanchet
parents:
36393
diff
changeset
|
477 |
section "Arity declaration" arity_clss @ |
36393
be73a2b2443b
support readable names even when Isar proof reconstruction is enabled -- useful for debugging
blanchet
parents:
36375
diff
changeset
|
478 |
section "Helper fact" helper_clss @ |
be73a2b2443b
support readable names even when Isar proof reconstruction is enabled -- useful for debugging
blanchet
parents:
36375
diff
changeset
|
479 |
section "Conjecture" conjecture_clss @ |
36402
1b20805974c7
introduced direct proof reconstruction code, eliminating the need for the "neg_clausify" method;
blanchet
parents:
36393
diff
changeset
|
480 |
section "Type variable" tfree_clss) |
1b20805974c7
introduced direct proof reconstruction code, eliminating the need for the "neg_clausify" method;
blanchet
parents:
36393
diff
changeset
|
481 |
in (pool, conjecture_offset) end |
19720 | 482 |
|
33311 | 483 |
end; |