author | blanchet |
Fri, 30 Jul 2010 00:02:25 +0200 | |
changeset 38105 | 373351f5f834 |
parent 38028 | 22dcaec5fa77 |
child 38653 | 78d0f18d5b36 |
permissions | -rw-r--r-- |
37578
9367cb36b1c4
renamed "Sledgehammer_FOL_Clauses" to "Metis_Clauses", so that Metis doesn't depend on Sledgehammer
blanchet
parents:
37577
diff
changeset
|
1 |
(* Title: HOL/Tools/Sledgehammer/metis_clauses.ML |
38027 | 2 |
Author: Jia Meng, Cambridge University Computer Laboratory and NICTA |
36393
be73a2b2443b
support readable names even when Isar proof reconstruction is enabled -- useful for debugging
blanchet
parents:
36378
diff
changeset
|
3 |
Author: Jasmin Blanchette, TU Muenchen |
15347 | 4 |
|
33311 | 5 |
Storing/printing FOL clauses and arity clauses. Typed equality is |
6 |
treated differently. |
|
15347 | 7 |
*) |
8 |
||
37578
9367cb36b1c4
renamed "Sledgehammer_FOL_Clauses" to "Metis_Clauses", so that Metis doesn't depend on Sledgehammer
blanchet
parents:
37577
diff
changeset
|
9 |
signature METIS_CLAUSES = |
24310 | 10 |
sig |
37577
5379f41a1322
merge "Sledgehammer_{F,H}OL_Clause", as requested by a FIXME
blanchet
parents:
37575
diff
changeset
|
11 |
type name = string * string |
5379f41a1322
merge "Sledgehammer_{F,H}OL_Clause", as requested by a FIXME
blanchet
parents:
37575
diff
changeset
|
12 |
datatype type_literal = |
37643
f576af716aa6
rewrote the TPTP problem generation code more or less from scratch;
blanchet
parents:
37632
diff
changeset
|
13 |
TyLitVar of name * name | |
f576af716aa6
rewrote the TPTP problem generation code more or less from scratch;
blanchet
parents:
37632
diff
changeset
|
14 |
TyLitFree of name * name |
37577
5379f41a1322
merge "Sledgehammer_{F,H}OL_Clause", as requested by a FIXME
blanchet
parents:
37575
diff
changeset
|
15 |
datatype arLit = |
37643
f576af716aa6
rewrote the TPTP problem generation code more or less from scratch;
blanchet
parents:
37632
diff
changeset
|
16 |
TConsLit of name * name * name list | |
f576af716aa6
rewrote the TPTP problem generation code more or less from scratch;
blanchet
parents:
37632
diff
changeset
|
17 |
TVarLit of name * name |
38028 | 18 |
datatype arity_clause = |
38105
373351f5f834
don't choke on synonyms when parsing SPASS's Flotter output + renamings;
blanchet
parents:
38028
diff
changeset
|
19 |
ArityClause of {name: string, conclLit: arLit, premLits: arLit list} |
38028 | 20 |
datatype class_rel_clause = |
38105
373351f5f834
don't choke on synonyms when parsing SPASS's Flotter output + renamings;
blanchet
parents:
38028
diff
changeset
|
21 |
ClassRelClause of {name: string, subclass: name, superclass: name} |
37577
5379f41a1322
merge "Sledgehammer_{F,H}OL_Clause", as requested by a FIXME
blanchet
parents:
37575
diff
changeset
|
22 |
datatype combtyp = |
37924 | 23 |
CombTVar of name | |
24 |
CombTFree of name | |
|
25 |
CombType of name * combtyp list |
|
37577
5379f41a1322
merge "Sledgehammer_{F,H}OL_Clause", as requested by a FIXME
blanchet
parents:
37575
diff
changeset
|
26 |
datatype combterm = |
5379f41a1322
merge "Sledgehammer_{F,H}OL_Clause", as requested by a FIXME
blanchet
parents:
37575
diff
changeset
|
27 |
CombConst of name * combtyp * combtyp list (* Const and Free *) | |
5379f41a1322
merge "Sledgehammer_{F,H}OL_Clause", as requested by a FIXME
blanchet
parents:
37575
diff
changeset
|
28 |
CombVar of name * combtyp | |
5379f41a1322
merge "Sledgehammer_{F,H}OL_Clause", as requested by a FIXME
blanchet
parents:
37575
diff
changeset
|
29 |
CombApp of combterm * combterm |
37923 | 30 |
datatype fol_literal = FOLLiteral of bool * combterm |
37577
5379f41a1322
merge "Sledgehammer_{F,H}OL_Clause", as requested by a FIXME
blanchet
parents:
37575
diff
changeset
|
31 |
|
37509
f39464d971c4
factor out TPTP format output into file of its own, to facilitate further changes
blanchet
parents:
37500
diff
changeset
|
32 |
val type_wrapper_name : string |
37995
06f02b15ef8a
generate full first-order formulas (FOF) in Sledgehammer
blanchet
parents:
37994
diff
changeset
|
33 |
val bound_var_prefix : string |
24310 | 34 |
val schematic_var_prefix: string |
35 |
val fixed_var_prefix: string |
|
36 |
val tvar_prefix: string |
|
37 |
val tfree_prefix: string |
|
38 |
val const_prefix: string |
|
37643
f576af716aa6
rewrote the TPTP problem generation code more or less from scratch;
blanchet
parents:
37632
diff
changeset
|
39 |
val type_const_prefix: string |
24310 | 40 |
val class_prefix: string |
41 |
val union_all: ''a list list -> ''a list |
|
37572
a899f9506f39
more intra-module dependency cleanup + merge "const" and "type_const" tables, since this is safe
blanchet
parents:
37570
diff
changeset
|
42 |
val invert_const: string -> string |
24310 | 43 |
val ascii_of: string -> string |
44 |
val undo_ascii_of: string -> string |
|
37992 | 45 |
val strip_prefix_and_undo_ascii: string -> string -> string option |
37995
06f02b15ef8a
generate full first-order formulas (FOF) in Sledgehammer
blanchet
parents:
37994
diff
changeset
|
46 |
val make_bound_var : string -> string |
24310 | 47 |
val make_schematic_var : string * int -> string |
18868 | 48 |
val make_fixed_var : string -> string |
49 |
val make_schematic_type_var : string * int -> string |
|
24310 | 50 |
val make_fixed_type_var : string -> string |
37498
b426cbdb5a23
removed Sledgehammer's support for the DFG syntax;
blanchet
parents:
37479
diff
changeset
|
51 |
val make_fixed_const : string -> string |
b426cbdb5a23
removed Sledgehammer's support for the DFG syntax;
blanchet
parents:
37479
diff
changeset
|
52 |
val make_fixed_type_const : string -> string |
18868 | 53 |
val make_type_class : string -> string |
37618
fa57a87f92a0
get rid of Skolem cache by performing CNF-conversion after fact selection
blanchet
parents:
37616
diff
changeset
|
54 |
val skolem_theory_name: string |
fa57a87f92a0
get rid of Skolem cache by performing CNF-conversion after fact selection
blanchet
parents:
37616
diff
changeset
|
55 |
val skolem_prefix: string |
fa57a87f92a0
get rid of Skolem cache by performing CNF-conversion after fact selection
blanchet
parents:
37616
diff
changeset
|
56 |
val skolem_infix: string |
fa57a87f92a0
get rid of Skolem cache by performing CNF-conversion after fact selection
blanchet
parents:
37616
diff
changeset
|
57 |
val is_skolem_const_name: string -> bool |
fa57a87f92a0
get rid of Skolem cache by performing CNF-conversion after fact selection
blanchet
parents:
37616
diff
changeset
|
58 |
val num_type_args: theory -> string -> int |
36966
adc11fb3f3aa
generate proper arity declarations for TFrees for SPASS's DFG format;
blanchet
parents:
36692
diff
changeset
|
59 |
val type_literals_for_types : typ list -> type_literal list |
37925 | 60 |
val make_class_rel_clauses: theory -> class list -> class list -> class_rel_clause list |
35865 | 61 |
val make_arity_clauses: theory -> string list -> class list -> class list * arity_clause list |
37994
b04307085a09
make TPTP generator accept full first-order formulas
blanchet
parents:
37992
diff
changeset
|
62 |
val combtyp_of : combterm -> combtyp |
37577
5379f41a1322
merge "Sledgehammer_{F,H}OL_Clause", as requested by a FIXME
blanchet
parents:
37575
diff
changeset
|
63 |
val strip_combterm_comb : combterm -> combterm * combterm list |
37995
06f02b15ef8a
generate full first-order formulas (FOF) in Sledgehammer
blanchet
parents:
37994
diff
changeset
|
64 |
val combterm_from_term : |
06f02b15ef8a
generate full first-order formulas (FOF) in Sledgehammer
blanchet
parents:
37994
diff
changeset
|
65 |
theory -> (string * typ) list -> term -> combterm * typ list |
37923 | 66 |
val literals_of_term : theory -> term -> fol_literal list * typ list |
37625
35eeb95c5bee
rename "skolem_somes" to "skolems", now that there's only one flavor of Skolems
blanchet
parents:
37624
diff
changeset
|
67 |
val conceal_skolem_terms : |
37577
5379f41a1322
merge "Sledgehammer_{F,H}OL_Clause", as requested by a FIXME
blanchet
parents:
37575
diff
changeset
|
68 |
int -> (string * term) list -> term -> (string * term) list * term |
37632 | 69 |
val reveal_skolem_terms : (string * term) list -> term -> term |
37577
5379f41a1322
merge "Sledgehammer_{F,H}OL_Clause", as requested by a FIXME
blanchet
parents:
37575
diff
changeset
|
70 |
val tfree_classes_of_terms : term list -> string list |
5379f41a1322
merge "Sledgehammer_{F,H}OL_Clause", as requested by a FIXME
blanchet
parents:
37575
diff
changeset
|
71 |
val tvar_classes_of_terms : term list -> string list |
5379f41a1322
merge "Sledgehammer_{F,H}OL_Clause", as requested by a FIXME
blanchet
parents:
37575
diff
changeset
|
72 |
val type_consts_of_terms : theory -> term list -> string list |
24310 | 73 |
end |
15347 | 74 |
|
37578
9367cb36b1c4
renamed "Sledgehammer_FOL_Clauses" to "Metis_Clauses", so that Metis doesn't depend on Sledgehammer
blanchet
parents:
37577
diff
changeset
|
75 |
structure Metis_Clauses : METIS_CLAUSES = |
15347 | 76 |
struct |
77 |
||
37509
f39464d971c4
factor out TPTP format output into file of its own, to facilitate further changes
blanchet
parents:
37500
diff
changeset
|
78 |
val type_wrapper_name = "ti" |
f39464d971c4
factor out TPTP format output into file of its own, to facilitate further changes
blanchet
parents:
37500
diff
changeset
|
79 |
|
37995
06f02b15ef8a
generate full first-order formulas (FOF) in Sledgehammer
blanchet
parents:
37994
diff
changeset
|
80 |
val bound_var_prefix = "B_" |
06f02b15ef8a
generate full first-order formulas (FOF) in Sledgehammer
blanchet
parents:
37994
diff
changeset
|
81 |
val schematic_var_prefix = "V_" |
06f02b15ef8a
generate full first-order formulas (FOF) in Sledgehammer
blanchet
parents:
37994
diff
changeset
|
82 |
val fixed_var_prefix = "v_" |
15347 | 83 |
|
17230
77e93bf303a5
fixed arities and restored changes that had gone missing
paulson
parents:
17150
diff
changeset
|
84 |
val tvar_prefix = "T_"; |
77e93bf303a5
fixed arities and restored changes that had gone missing
paulson
parents:
17150
diff
changeset
|
85 |
val tfree_prefix = "t_"; |
15347 | 86 |
|
17230
77e93bf303a5
fixed arities and restored changes that had gone missing
paulson
parents:
17150
diff
changeset
|
87 |
val const_prefix = "c_"; |
37643
f576af716aa6
rewrote the TPTP problem generation code more or less from scratch;
blanchet
parents:
37632
diff
changeset
|
88 |
val type_const_prefix = "tc_"; |
24310 | 89 |
val class_prefix = "class_"; |
15347 | 90 |
|
36218
0e4a01f3e7d3
get rid of "List.foldl" + add timestamp to SPASS
blanchet
parents:
36170
diff
changeset
|
91 |
fun union_all xss = fold (union (op =)) xss [] |
17775 | 92 |
|
36493
a3357a631b96
reintroduced short names for HOL->FOL constants; other parts of the code rely on these
blanchet
parents:
36491
diff
changeset
|
93 |
(* Readable names for the more common symbolic functions. Do not mess with the |
37479
f6b1ee5b420b
try to improve Sledgehammer/Metis's behavior in full_types mode, e.g. by handing True, False, and If better
blanchet
parents:
37414
diff
changeset
|
94 |
last nine entries of the table unless you know what you are doing. *) |
15347 | 95 |
val const_trans_table = |
37678
0040bafffdef
"prod" and "sum" replace "*" and "+" respectively
haftmann
parents:
37643
diff
changeset
|
96 |
Symtab.make [(@{type_name Product_Type.prod}, "prod"), |
0040bafffdef
"prod" and "sum" replace "*" and "+" respectively
haftmann
parents:
37643
diff
changeset
|
97 |
(@{type_name Sum_Type.sum}, "sum"), |
37643
f576af716aa6
rewrote the TPTP problem generation code more or less from scratch;
blanchet
parents:
37632
diff
changeset
|
98 |
(@{const_name "op ="}, "equal"), |
35865 | 99 |
(@{const_name "op &"}, "and"), |
100 |
(@{const_name "op |"}, "or"), |
|
101 |
(@{const_name "op -->"}, "implies"), |
|
37678
0040bafffdef
"prod" and "sum" replace "*" and "+" respectively
haftmann
parents:
37643
diff
changeset
|
102 |
(@{const_name Set.member}, "in"), |
36493
a3357a631b96
reintroduced short names for HOL->FOL constants; other parts of the code rely on these
blanchet
parents:
36491
diff
changeset
|
103 |
(@{const_name fequal}, "fequal"), |
a3357a631b96
reintroduced short names for HOL->FOL constants; other parts of the code rely on these
blanchet
parents:
36491
diff
changeset
|
104 |
(@{const_name COMBI}, "COMBI"), |
a3357a631b96
reintroduced short names for HOL->FOL constants; other parts of the code rely on these
blanchet
parents:
36491
diff
changeset
|
105 |
(@{const_name COMBK}, "COMBK"), |
a3357a631b96
reintroduced short names for HOL->FOL constants; other parts of the code rely on these
blanchet
parents:
36491
diff
changeset
|
106 |
(@{const_name COMBB}, "COMBB"), |
a3357a631b96
reintroduced short names for HOL->FOL constants; other parts of the code rely on these
blanchet
parents:
36491
diff
changeset
|
107 |
(@{const_name COMBC}, "COMBC"), |
37479
f6b1ee5b420b
try to improve Sledgehammer/Metis's behavior in full_types mode, e.g. by handing True, False, and If better
blanchet
parents:
37414
diff
changeset
|
108 |
(@{const_name COMBS}, "COMBS"), |
f6b1ee5b420b
try to improve Sledgehammer/Metis's behavior in full_types mode, e.g. by handing True, False, and If better
blanchet
parents:
37414
diff
changeset
|
109 |
(@{const_name True}, "True"), |
f6b1ee5b420b
try to improve Sledgehammer/Metis's behavior in full_types mode, e.g. by handing True, False, and If better
blanchet
parents:
37414
diff
changeset
|
110 |
(@{const_name False}, "False"), |
37643
f576af716aa6
rewrote the TPTP problem generation code more or less from scratch;
blanchet
parents:
37632
diff
changeset
|
111 |
(@{const_name If}, "If")] |
15347 | 112 |
|
37572
a899f9506f39
more intra-module dependency cleanup + merge "const" and "type_const" tables, since this is safe
blanchet
parents:
37570
diff
changeset
|
113 |
(* Invert the table of translations between Isabelle and ATPs. *) |
a899f9506f39
more intra-module dependency cleanup + merge "const" and "type_const" tables, since this is safe
blanchet
parents:
37570
diff
changeset
|
114 |
val const_trans_table_inv = |
a899f9506f39
more intra-module dependency cleanup + merge "const" and "type_const" tables, since this is safe
blanchet
parents:
37570
diff
changeset
|
115 |
Symtab.update ("fequal", @{const_name "op ="}) |
a899f9506f39
more intra-module dependency cleanup + merge "const" and "type_const" tables, since this is safe
blanchet
parents:
37570
diff
changeset
|
116 |
(Symtab.make (map swap (Symtab.dest const_trans_table))) |
a899f9506f39
more intra-module dependency cleanup + merge "const" and "type_const" tables, since this is safe
blanchet
parents:
37570
diff
changeset
|
117 |
|
a899f9506f39
more intra-module dependency cleanup + merge "const" and "type_const" tables, since this is safe
blanchet
parents:
37570
diff
changeset
|
118 |
val invert_const = perhaps (Symtab.lookup const_trans_table_inv) |
15347 | 119 |
|
15610 | 120 |
(*Escaping of special characters. |
121 |
Alphanumeric characters are left unchanged. |
|
122 |
The character _ goes to __ |
|
123 |
Characters in the range ASCII space to / go to _A to _P, respectively. |
|
24183 | 124 |
Other printing characters go to _nnn where nnn is the decimal ASCII code.*) |
125 |
val A_minus_space = Char.ord #"A" - Char.ord #" "; |
|
15610 | 126 |
|
24183 | 127 |
fun stringN_of_int 0 _ = "" |
128 |
| stringN_of_int k n = stringN_of_int (k-1) (n div 10) ^ Int.toString (n mod 10); |
|
15610 | 129 |
|
15347 | 130 |
fun ascii_of_c c = |
15610 | 131 |
if Char.isAlphaNum c then String.str c |
132 |
else if c = #"_" then "__" |
|
24310 | 133 |
else if #" " <= c andalso c <= #"/" |
15610 | 134 |
then "_" ^ String.str (Char.chr (Char.ord c + A_minus_space)) |
24310 | 135 |
else if Char.isPrint c |
24183 | 136 |
then ("_" ^ stringN_of_int 3 (Char.ord c)) (*fixed width, in case more digits follow*) |
15610 | 137 |
else "" |
15347 | 138 |
|
15610 | 139 |
val ascii_of = String.translate ascii_of_c; |
140 |
||
24183 | 141 |
(** Remove ASCII armouring from names in proof files **) |
142 |
||
143 |
(*We don't raise error exceptions because this code can run inside the watcher. |
|
144 |
Also, the errors are "impossible" (hah!)*) |
|
145 |
fun undo_ascii_aux rcs [] = String.implode(rev rcs) |
|
146 |
| undo_ascii_aux rcs [#"_"] = undo_ascii_aux (#"_"::rcs) [] (*ERROR*) |
|
147 |
(*Three types of _ escapes: __, _A to _P, _nnn*) |
|
148 |
| undo_ascii_aux rcs (#"_" :: #"_" :: cs) = undo_ascii_aux (#"_"::rcs) cs |
|
24310 | 149 |
| undo_ascii_aux rcs (#"_" :: c :: cs) = |
24183 | 150 |
if #"A" <= c andalso c<= #"P" (*translation of #" " to #"/"*) |
151 |
then undo_ascii_aux (Char.chr(Char.ord c - A_minus_space) :: rcs) cs |
|
24310 | 152 |
else |
24183 | 153 |
let val digits = List.take (c::cs, 3) handle Subscript => [] |
24310 | 154 |
in |
24183 | 155 |
case Int.fromString (String.implode digits) of |
156 |
NONE => undo_ascii_aux (c:: #"_"::rcs) cs (*ERROR*) |
|
157 |
| SOME n => undo_ascii_aux (Char.chr n :: rcs) (List.drop (cs, 2)) |
|
158 |
end |
|
159 |
| undo_ascii_aux rcs (c::cs) = undo_ascii_aux (c::rcs) cs; |
|
160 |
||
161 |
val undo_ascii_of = undo_ascii_aux [] o String.explode; |
|
15347 | 162 |
|
37572
a899f9506f39
more intra-module dependency cleanup + merge "const" and "type_const" tables, since this is safe
blanchet
parents:
37570
diff
changeset
|
163 |
(* If string s has the prefix s1, return the result of deleting it, |
a899f9506f39
more intra-module dependency cleanup + merge "const" and "type_const" tables, since this is safe
blanchet
parents:
37570
diff
changeset
|
164 |
un-ASCII'd. *) |
37992 | 165 |
fun strip_prefix_and_undo_ascii s1 s = |
37572
a899f9506f39
more intra-module dependency cleanup + merge "const" and "type_const" tables, since this is safe
blanchet
parents:
37570
diff
changeset
|
166 |
if String.isPrefix s1 s then |
a899f9506f39
more intra-module dependency cleanup + merge "const" and "type_const" tables, since this is safe
blanchet
parents:
37570
diff
changeset
|
167 |
SOME (undo_ascii_of (String.extract (s, size s1, NONE))) |
a899f9506f39
more intra-module dependency cleanup + merge "const" and "type_const" tables, since this is safe
blanchet
parents:
37570
diff
changeset
|
168 |
else |
a899f9506f39
more intra-module dependency cleanup + merge "const" and "type_const" tables, since this is safe
blanchet
parents:
37570
diff
changeset
|
169 |
NONE |
a899f9506f39
more intra-module dependency cleanup + merge "const" and "type_const" tables, since this is safe
blanchet
parents:
37570
diff
changeset
|
170 |
|
16925
0fd7b1438d28
simpler variable names, and no types for monomorphic constants
paulson
parents:
16903
diff
changeset
|
171 |
(*Remove the initial ' character from a type variable, if it is present*) |
0fd7b1438d28
simpler variable names, and no types for monomorphic constants
paulson
parents:
16903
diff
changeset
|
172 |
fun trim_type_var s = |
0fd7b1438d28
simpler variable names, and no types for monomorphic constants
paulson
parents:
16903
diff
changeset
|
173 |
if s <> "" andalso String.sub(s,0) = #"'" then String.extract(s,1,NONE) |
0fd7b1438d28
simpler variable names, and no types for monomorphic constants
paulson
parents:
16903
diff
changeset
|
174 |
else error ("trim_type: Malformed type variable encountered: " ^ s); |
0fd7b1438d28
simpler variable names, and no types for monomorphic constants
paulson
parents:
16903
diff
changeset
|
175 |
|
16903 | 176 |
fun ascii_of_indexname (v,0) = ascii_of v |
17525
ae5bb6001afb
tidying, and support for axclass/classrel clauses
paulson
parents:
17422
diff
changeset
|
177 |
| ascii_of_indexname (v,i) = ascii_of v ^ "_" ^ Int.toString i; |
15347 | 178 |
|
37995
06f02b15ef8a
generate full first-order formulas (FOF) in Sledgehammer
blanchet
parents:
37994
diff
changeset
|
179 |
fun make_bound_var x = bound_var_prefix ^ ascii_of x |
06f02b15ef8a
generate full first-order formulas (FOF) in Sledgehammer
blanchet
parents:
37994
diff
changeset
|
180 |
fun make_schematic_var v = schematic_var_prefix ^ ascii_of_indexname v |
06f02b15ef8a
generate full first-order formulas (FOF) in Sledgehammer
blanchet
parents:
37994
diff
changeset
|
181 |
fun make_fixed_var x = fixed_var_prefix ^ ascii_of x |
15347 | 182 |
|
24310 | 183 |
fun make_schematic_type_var (x,i) = |
16925
0fd7b1438d28
simpler variable names, and no types for monomorphic constants
paulson
parents:
16903
diff
changeset
|
184 |
tvar_prefix ^ (ascii_of_indexname (trim_type_var x,i)); |
0fd7b1438d28
simpler variable names, and no types for monomorphic constants
paulson
parents:
16903
diff
changeset
|
185 |
fun make_fixed_type_var x = tfree_prefix ^ (ascii_of (trim_type_var x)); |
15347 | 186 |
|
37498
b426cbdb5a23
removed Sledgehammer's support for the DFG syntax;
blanchet
parents:
37479
diff
changeset
|
187 |
fun lookup_const c = |
b426cbdb5a23
removed Sledgehammer's support for the DFG syntax;
blanchet
parents:
37479
diff
changeset
|
188 |
case Symtab.lookup const_trans_table c of |
b426cbdb5a23
removed Sledgehammer's support for the DFG syntax;
blanchet
parents:
37479
diff
changeset
|
189 |
SOME c' => c' |
b426cbdb5a23
removed Sledgehammer's support for the DFG syntax;
blanchet
parents:
37479
diff
changeset
|
190 |
| NONE => ascii_of c |
23075 | 191 |
|
36062 | 192 |
(* "op =" MUST BE "equal" because it's built into ATPs. *) |
37498
b426cbdb5a23
removed Sledgehammer's support for the DFG syntax;
blanchet
parents:
37479
diff
changeset
|
193 |
fun make_fixed_const @{const_name "op ="} = "equal" |
b426cbdb5a23
removed Sledgehammer's support for the DFG syntax;
blanchet
parents:
37479
diff
changeset
|
194 |
| make_fixed_const c = const_prefix ^ lookup_const c |
18411
2d3165a0fb40
No axiom, arity or classrel clauses contain HOL.type. Negative occurrences are
paulson
parents:
18409
diff
changeset
|
195 |
|
37643
f576af716aa6
rewrote the TPTP problem generation code more or less from scratch;
blanchet
parents:
37632
diff
changeset
|
196 |
fun make_fixed_type_const c = type_const_prefix ^ lookup_const c |
17150
ce2a1aeb42aa
DFG output now works for untyped rules (ML "ResClause.untyped();")
quigley
parents:
16976
diff
changeset
|
197 |
|
17261 | 198 |
fun make_type_class clas = class_prefix ^ ascii_of clas; |
17150
ce2a1aeb42aa
DFG output now works for untyped rules (ML "ResClause.untyped();")
quigley
parents:
16976
diff
changeset
|
199 |
|
37618
fa57a87f92a0
get rid of Skolem cache by performing CNF-conversion after fact selection
blanchet
parents:
37616
diff
changeset
|
200 |
val skolem_theory_name = "Sledgehammer" ^ Long_Name.separator ^ "Sko" |
fa57a87f92a0
get rid of Skolem cache by performing CNF-conversion after fact selection
blanchet
parents:
37616
diff
changeset
|
201 |
val skolem_prefix = "sko_" |
fa57a87f92a0
get rid of Skolem cache by performing CNF-conversion after fact selection
blanchet
parents:
37616
diff
changeset
|
202 |
val skolem_infix = "$" |
fa57a87f92a0
get rid of Skolem cache by performing CNF-conversion after fact selection
blanchet
parents:
37616
diff
changeset
|
203 |
|
fa57a87f92a0
get rid of Skolem cache by performing CNF-conversion after fact selection
blanchet
parents:
37616
diff
changeset
|
204 |
(* Hack: Could return false positives (e.g., a user happens to declare a |
fa57a87f92a0
get rid of Skolem cache by performing CNF-conversion after fact selection
blanchet
parents:
37616
diff
changeset
|
205 |
constant called "SomeTheory.sko_means_shoe_in_$wedish". *) |
fa57a87f92a0
get rid of Skolem cache by performing CNF-conversion after fact selection
blanchet
parents:
37616
diff
changeset
|
206 |
val is_skolem_const_name = |
fa57a87f92a0
get rid of Skolem cache by performing CNF-conversion after fact selection
blanchet
parents:
37616
diff
changeset
|
207 |
Long_Name.base_name |
fa57a87f92a0
get rid of Skolem cache by performing CNF-conversion after fact selection
blanchet
parents:
37616
diff
changeset
|
208 |
#> String.isPrefix skolem_prefix andf String.isSubstring skolem_infix |
fa57a87f92a0
get rid of Skolem cache by performing CNF-conversion after fact selection
blanchet
parents:
37616
diff
changeset
|
209 |
|
fa57a87f92a0
get rid of Skolem cache by performing CNF-conversion after fact selection
blanchet
parents:
37616
diff
changeset
|
210 |
(* The number of type arguments of a constant, zero if it's monomorphic. For |
fa57a87f92a0
get rid of Skolem cache by performing CNF-conversion after fact selection
blanchet
parents:
37616
diff
changeset
|
211 |
(instances of) Skolem pseudoconstants, this information is encoded in the |
fa57a87f92a0
get rid of Skolem cache by performing CNF-conversion after fact selection
blanchet
parents:
37616
diff
changeset
|
212 |
constant name. *) |
fa57a87f92a0
get rid of Skolem cache by performing CNF-conversion after fact selection
blanchet
parents:
37616
diff
changeset
|
213 |
fun num_type_args thy s = |
fa57a87f92a0
get rid of Skolem cache by performing CNF-conversion after fact selection
blanchet
parents:
37616
diff
changeset
|
214 |
if String.isPrefix skolem_theory_name s then |
fa57a87f92a0
get rid of Skolem cache by performing CNF-conversion after fact selection
blanchet
parents:
37616
diff
changeset
|
215 |
s |> unprefix skolem_theory_name |
fa57a87f92a0
get rid of Skolem cache by performing CNF-conversion after fact selection
blanchet
parents:
37616
diff
changeset
|
216 |
|> space_explode skolem_infix |> hd |
fa57a87f92a0
get rid of Skolem cache by performing CNF-conversion after fact selection
blanchet
parents:
37616
diff
changeset
|
217 |
|> space_explode "_" |> List.last |> Int.fromString |> the |
fa57a87f92a0
get rid of Skolem cache by performing CNF-conversion after fact selection
blanchet
parents:
37616
diff
changeset
|
218 |
else |
fa57a87f92a0
get rid of Skolem cache by performing CNF-conversion after fact selection
blanchet
parents:
37616
diff
changeset
|
219 |
(s, Sign.the_const_type thy s) |> Sign.const_typargs thy |> length |
17150
ce2a1aeb42aa
DFG output now works for untyped rules (ML "ResClause.untyped();")
quigley
parents:
16976
diff
changeset
|
220 |
|
37624 | 221 |
(**** Definitions and functions for FOL clauses for TPTP format output ****) |
36169
27b1cc58715e
store nonmangled names along with mangled type names in Sledgehammer for debugging purposes
blanchet
parents:
36168
diff
changeset
|
222 |
|
37624 | 223 |
type name = string * string |
15347 | 224 |
|
225 |
(**** Isabelle FOL clauses ****) |
|
226 |
||
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:
36493
diff
changeset
|
227 |
(* The first component is the type class; the second is a TVar or TFree. *) |
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:
36493
diff
changeset
|
228 |
datatype type_literal = |
37643
f576af716aa6
rewrote the TPTP problem generation code more or less from scratch;
blanchet
parents:
37632
diff
changeset
|
229 |
TyLitVar of name * name | |
f576af716aa6
rewrote the TPTP problem generation code more or less from scratch;
blanchet
parents:
37632
diff
changeset
|
230 |
TyLitFree of name * name |
15347 | 231 |
|
17404
d16c3a62c396
the experimental tagging system, and the usual tidying
paulson
parents:
17375
diff
changeset
|
232 |
exception CLAUSE of string * term; |
15347 | 233 |
|
24310 | 234 |
(*Make literals for sorted type variables*) |
24940 | 235 |
fun sorts_on_typs_aux (_, []) = [] |
236 |
| sorts_on_typs_aux ((x,i), s::ss) = |
|
237 |
let val sorts = sorts_on_typs_aux ((x,i), ss) |
|
22643
bc3bb8e9594a
Improved and simplified the treatment of classrel/arity clauses
paulson
parents:
22383
diff
changeset
|
238 |
in |
bc3bb8e9594a
Improved and simplified the treatment of classrel/arity clauses
paulson
parents:
22383
diff
changeset
|
239 |
if s = "HOL.type" then sorts |
37643
f576af716aa6
rewrote the TPTP problem generation code more or less from scratch;
blanchet
parents:
37632
diff
changeset
|
240 |
else if i = ~1 then TyLitFree (`make_type_class s, `make_fixed_type_var x) :: sorts |
f576af716aa6
rewrote the TPTP problem generation code more or less from scratch;
blanchet
parents:
37632
diff
changeset
|
241 |
else TyLitVar (`make_type_class s, (make_schematic_type_var (x,i), x)) :: sorts |
22643
bc3bb8e9594a
Improved and simplified the treatment of classrel/arity clauses
paulson
parents:
22383
diff
changeset
|
242 |
end; |
17150
ce2a1aeb42aa
DFG output now works for untyped rules (ML "ResClause.untyped();")
quigley
parents:
16976
diff
changeset
|
243 |
|
24940 | 244 |
fun sorts_on_typs (TFree (a,s)) = sorts_on_typs_aux ((a,~1),s) |
245 |
| sorts_on_typs (TVar (v,s)) = sorts_on_typs_aux (v,s); |
|
246 |
||
24937
340523598914
context-based treatment of generalization; also handling TFrees in axiom clauses
paulson
parents:
24322
diff
changeset
|
247 |
(*Given a list of sorted type variables, return a list of type literals.*) |
36966
adc11fb3f3aa
generate proper arity declarations for TFrees for SPASS's DFG format;
blanchet
parents:
36692
diff
changeset
|
248 |
fun type_literals_for_types Ts = |
adc11fb3f3aa
generate proper arity declarations for TFrees for SPASS's DFG format;
blanchet
parents:
36692
diff
changeset
|
249 |
fold (union (op =)) (map sorts_on_typs Ts) [] |
20015
1ffcf4802802
Literals aren't sorted any more. Output overloaded constants' type var instantiations.
mengj
parents:
19719
diff
changeset
|
250 |
|
1ffcf4802802
Literals aren't sorted any more. Output overloaded constants' type var instantiations.
mengj
parents:
19719
diff
changeset
|
251 |
(** make axiom and conjecture clauses. **) |
1ffcf4802802
Literals aren't sorted any more. Output overloaded constants' type var instantiations.
mengj
parents:
19719
diff
changeset
|
252 |
|
15347 | 253 |
(**** Isabelle arities ****) |
254 |
||
37643
f576af716aa6
rewrote the TPTP problem generation code more or less from scratch;
blanchet
parents:
37632
diff
changeset
|
255 |
datatype arLit = |
f576af716aa6
rewrote the TPTP problem generation code more or less from scratch;
blanchet
parents:
37632
diff
changeset
|
256 |
TConsLit of name * name * name list | |
f576af716aa6
rewrote the TPTP problem generation code more or less from scratch;
blanchet
parents:
37632
diff
changeset
|
257 |
TVarLit of name * name |
24310 | 258 |
|
35865 | 259 |
datatype arity_clause = |
38105
373351f5f834
don't choke on synonyms when parsing SPASS's Flotter output + renamings;
blanchet
parents:
38028
diff
changeset
|
260 |
ArityClause of {name: string, conclLit: arLit, premLits: arLit list} |
15347 | 261 |
|
262 |
||
18798 | 263 |
fun gen_TVars 0 = [] |
264 |
| gen_TVars n = ("T_" ^ Int.toString n) :: gen_TVars (n-1); |
|
15347 | 265 |
|
18411
2d3165a0fb40
No axiom, arity or classrel clauses contain HOL.type. Negative occurrences are
paulson
parents:
18409
diff
changeset
|
266 |
fun pack_sort(_,[]) = [] |
37643
f576af716aa6
rewrote the TPTP problem generation code more or less from scratch;
blanchet
parents:
37632
diff
changeset
|
267 |
| pack_sort(tvar, "HOL.type"::srt) = pack_sort (tvar, srt) (*IGNORE sort "type"*) |
f576af716aa6
rewrote the TPTP problem generation code more or less from scratch;
blanchet
parents:
37632
diff
changeset
|
268 |
| pack_sort(tvar, cls::srt) = |
f576af716aa6
rewrote the TPTP problem generation code more or less from scratch;
blanchet
parents:
37632
diff
changeset
|
269 |
(`make_type_class cls, (tvar, tvar)) :: pack_sort (tvar, srt) |
24310 | 270 |
|
18411
2d3165a0fb40
No axiom, arity or classrel clauses contain HOL.type. Negative occurrences are
paulson
parents:
18409
diff
changeset
|
271 |
(*Arity of type constructor tcon :: (arg1,...,argN)res*) |
38105
373351f5f834
don't choke on synonyms when parsing SPASS's Flotter output + renamings;
blanchet
parents:
38028
diff
changeset
|
272 |
fun make_axiom_arity_clause (tcons, name, (cls,args)) = |
37643
f576af716aa6
rewrote the TPTP problem generation code more or less from scratch;
blanchet
parents:
37632
diff
changeset
|
273 |
let |
f576af716aa6
rewrote the TPTP problem generation code more or less from scratch;
blanchet
parents:
37632
diff
changeset
|
274 |
val tvars = gen_TVars (length args) |
f576af716aa6
rewrote the TPTP problem generation code more or less from scratch;
blanchet
parents:
37632
diff
changeset
|
275 |
val tvars_srts = ListPair.zip (tvars, args) |
f576af716aa6
rewrote the TPTP problem generation code more or less from scratch;
blanchet
parents:
37632
diff
changeset
|
276 |
in |
38105
373351f5f834
don't choke on synonyms when parsing SPASS's Flotter output + renamings;
blanchet
parents:
38028
diff
changeset
|
277 |
ArityClause {name = name, |
37643
f576af716aa6
rewrote the TPTP problem generation code more or less from scratch;
blanchet
parents:
37632
diff
changeset
|
278 |
conclLit = TConsLit (`make_type_class cls, |
f576af716aa6
rewrote the TPTP problem generation code more or less from scratch;
blanchet
parents:
37632
diff
changeset
|
279 |
`make_fixed_type_const tcons, |
f576af716aa6
rewrote the TPTP problem generation code more or less from scratch;
blanchet
parents:
37632
diff
changeset
|
280 |
tvars ~~ tvars), |
f576af716aa6
rewrote the TPTP problem generation code more or less from scratch;
blanchet
parents:
37632
diff
changeset
|
281 |
premLits = map TVarLit (union_all (map pack_sort tvars_srts))} |
f576af716aa6
rewrote the TPTP problem generation code more or less from scratch;
blanchet
parents:
37632
diff
changeset
|
282 |
end |
15347 | 283 |
|
284 |
||
285 |
(**** Isabelle class relations ****) |
|
286 |
||
37925 | 287 |
datatype class_rel_clause = |
38105
373351f5f834
don't choke on synonyms when parsing SPASS's Flotter output + renamings;
blanchet
parents:
38028
diff
changeset
|
288 |
ClassRelClause of {name: string, subclass: name, superclass: name} |
24310 | 289 |
|
21290
33b6bb5d6ab8
Improvement to classrel clauses: now outputs the minimum needed.
paulson
parents:
21254
diff
changeset
|
290 |
(*Generate all pairs (sub,super) such that sub is a proper subclass of super in theory thy.*) |
37498
b426cbdb5a23
removed Sledgehammer's support for the DFG syntax;
blanchet
parents:
37479
diff
changeset
|
291 |
fun class_pairs _ [] _ = [] |
21432
625797c592b2
Optimized class_pairs for the common case of no subclasses
paulson
parents:
21416
diff
changeset
|
292 |
| class_pairs thy subs supers = |
36218
0e4a01f3e7d3
get rid of "List.foldl" + add timestamp to SPASS
blanchet
parents:
36170
diff
changeset
|
293 |
let |
0e4a01f3e7d3
get rid of "List.foldl" + add timestamp to SPASS
blanchet
parents:
36170
diff
changeset
|
294 |
val class_less = Sorts.class_less (Sign.classes_of thy) |
0e4a01f3e7d3
get rid of "List.foldl" + add timestamp to SPASS
blanchet
parents:
36170
diff
changeset
|
295 |
fun add_super sub super = class_less (sub, super) ? cons (sub, super) |
0e4a01f3e7d3
get rid of "List.foldl" + add timestamp to SPASS
blanchet
parents:
36170
diff
changeset
|
296 |
fun add_supers sub = fold (add_super sub) supers |
0e4a01f3e7d3
get rid of "List.foldl" + add timestamp to SPASS
blanchet
parents:
36170
diff
changeset
|
297 |
in fold add_supers subs [] end |
15347 | 298 |
|
37925 | 299 |
fun make_class_rel_clause (sub,super) = |
38105
373351f5f834
don't choke on synonyms when parsing SPASS's Flotter output + renamings;
blanchet
parents:
38028
diff
changeset
|
300 |
ClassRelClause {name = sub ^ "_" ^ super, |
37643
f576af716aa6
rewrote the TPTP problem generation code more or less from scratch;
blanchet
parents:
37632
diff
changeset
|
301 |
subclass = `make_type_class sub, |
38105
373351f5f834
don't choke on synonyms when parsing SPASS's Flotter output + renamings;
blanchet
parents:
38028
diff
changeset
|
302 |
superclass = `make_type_class super} |
15347 | 303 |
|
37925 | 304 |
fun make_class_rel_clauses thy subs supers = |
305 |
map make_class_rel_clause (class_pairs thy subs supers); |
|
18868 | 306 |
|
307 |
||
308 |
(** Isabelle arities **) |
|
17845
1438291d57f0
deletion of Tools/res_types_sorts; removal of absolute numbering of clauses
paulson
parents:
17775
diff
changeset
|
309 |
|
37498
b426cbdb5a23
removed Sledgehammer's support for the DFG syntax;
blanchet
parents:
37479
diff
changeset
|
310 |
fun arity_clause _ _ (_, []) = [] |
b426cbdb5a23
removed Sledgehammer's support for the DFG syntax;
blanchet
parents:
37479
diff
changeset
|
311 |
| arity_clause seen n (tcons, ("HOL.type",_)::ars) = (*ignore*) |
b426cbdb5a23
removed Sledgehammer's support for the DFG syntax;
blanchet
parents:
37479
diff
changeset
|
312 |
arity_clause seen n (tcons,ars) |
b426cbdb5a23
removed Sledgehammer's support for the DFG syntax;
blanchet
parents:
37479
diff
changeset
|
313 |
| arity_clause seen n (tcons, (ar as (class,_)) :: ars) = |
36692
54b64d4ad524
farewell to old-style mem infixes -- type inference in situations with mem_int and mem_string should provide enough information to resolve the type of (op =)
haftmann
parents:
36556
diff
changeset
|
314 |
if member (op =) seen class then (*multiple arities for the same tycon, class pair*) |
37572
a899f9506f39
more intra-module dependency cleanup + merge "const" and "type_const" tables, since this is safe
blanchet
parents:
37570
diff
changeset
|
315 |
make_axiom_arity_clause (tcons, lookup_const tcons ^ "_" ^ class ^ "_" ^ Int.toString n, ar) :: |
37498
b426cbdb5a23
removed Sledgehammer's support for the DFG syntax;
blanchet
parents:
37479
diff
changeset
|
316 |
arity_clause seen (n+1) (tcons,ars) |
21373
18f519614978
Arity clauses are now produced only for types and type classes actually used.
paulson
parents:
21290
diff
changeset
|
317 |
else |
37572
a899f9506f39
more intra-module dependency cleanup + merge "const" and "type_const" tables, since this is safe
blanchet
parents:
37570
diff
changeset
|
318 |
make_axiom_arity_clause (tcons, lookup_const tcons ^ "_" ^ class, ar) :: |
37498
b426cbdb5a23
removed Sledgehammer's support for the DFG syntax;
blanchet
parents:
37479
diff
changeset
|
319 |
arity_clause (class::seen) n (tcons,ars) |
17845
1438291d57f0
deletion of Tools/res_types_sorts; removal of absolute numbering of clauses
paulson
parents:
17775
diff
changeset
|
320 |
|
37498
b426cbdb5a23
removed Sledgehammer's support for the DFG syntax;
blanchet
parents:
37479
diff
changeset
|
321 |
fun multi_arity_clause [] = [] |
b426cbdb5a23
removed Sledgehammer's support for the DFG syntax;
blanchet
parents:
37479
diff
changeset
|
322 |
| multi_arity_clause ((tcons, ars) :: tc_arlists) = |
b426cbdb5a23
removed Sledgehammer's support for the DFG syntax;
blanchet
parents:
37479
diff
changeset
|
323 |
arity_clause [] 1 (tcons, ars) @ multi_arity_clause tc_arlists |
17845
1438291d57f0
deletion of Tools/res_types_sorts; removal of absolute numbering of clauses
paulson
parents:
17775
diff
changeset
|
324 |
|
22643
bc3bb8e9594a
Improved and simplified the treatment of classrel/arity clauses
paulson
parents:
22383
diff
changeset
|
325 |
(*Generate all pairs (tycon,class,sorts) such that tycon belongs to class in theory thy |
bc3bb8e9594a
Improved and simplified the treatment of classrel/arity clauses
paulson
parents:
22383
diff
changeset
|
326 |
provided its arguments have the corresponding sorts.*) |
21373
18f519614978
Arity clauses are now produced only for types and type classes actually used.
paulson
parents:
21290
diff
changeset
|
327 |
fun type_class_pairs thy tycons classes = |
18f519614978
Arity clauses are now produced only for types and type classes actually used.
paulson
parents:
21290
diff
changeset
|
328 |
let val alg = Sign.classes_of thy |
36218
0e4a01f3e7d3
get rid of "List.foldl" + add timestamp to SPASS
blanchet
parents:
36170
diff
changeset
|
329 |
fun domain_sorts tycon = Sorts.mg_domain alg tycon o single |
0e4a01f3e7d3
get rid of "List.foldl" + add timestamp to SPASS
blanchet
parents:
36170
diff
changeset
|
330 |
fun add_class tycon class = |
0e4a01f3e7d3
get rid of "List.foldl" + add timestamp to SPASS
blanchet
parents:
36170
diff
changeset
|
331 |
cons (class, domain_sorts tycon class) |
0e4a01f3e7d3
get rid of "List.foldl" + add timestamp to SPASS
blanchet
parents:
36170
diff
changeset
|
332 |
handle Sorts.CLASS_ERROR _ => I |
0e4a01f3e7d3
get rid of "List.foldl" + add timestamp to SPASS
blanchet
parents:
36170
diff
changeset
|
333 |
fun try_classes tycon = (tycon, fold (add_class tycon) classes []) |
21373
18f519614978
Arity clauses are now produced only for types and type classes actually used.
paulson
parents:
21290
diff
changeset
|
334 |
in map try_classes tycons end; |
18f519614978
Arity clauses are now produced only for types and type classes actually used.
paulson
parents:
21290
diff
changeset
|
335 |
|
22643
bc3bb8e9594a
Improved and simplified the treatment of classrel/arity clauses
paulson
parents:
22383
diff
changeset
|
336 |
(*Proving one (tycon, class) membership may require proving others, so iterate.*) |
37498
b426cbdb5a23
removed Sledgehammer's support for the DFG syntax;
blanchet
parents:
37479
diff
changeset
|
337 |
fun iter_type_class_pairs _ _ [] = ([], []) |
22643
bc3bb8e9594a
Improved and simplified the treatment of classrel/arity clauses
paulson
parents:
22383
diff
changeset
|
338 |
| iter_type_class_pairs thy tycons classes = |
bc3bb8e9594a
Improved and simplified the treatment of classrel/arity clauses
paulson
parents:
22383
diff
changeset
|
339 |
let val cpairs = type_class_pairs thy tycons classes |
33040 | 340 |
val newclasses = union_all (union_all (union_all (map (map #2 o #2) cpairs))) |
341 |
|> subtract (op =) classes |> subtract (op =) HOLogic.typeS |
|
24310 | 342 |
val (classes', cpairs') = iter_type_class_pairs thy tycons newclasses |
33042 | 343 |
in (union (op =) classes' classes, union (op =) cpairs' cpairs) end; |
24310 | 344 |
|
37498
b426cbdb5a23
removed Sledgehammer's support for the DFG syntax;
blanchet
parents:
37479
diff
changeset
|
345 |
fun make_arity_clauses thy tycons classes = |
24310 | 346 |
let val (classes', cpairs) = iter_type_class_pairs thy tycons classes |
37498
b426cbdb5a23
removed Sledgehammer's support for the DFG syntax;
blanchet
parents:
37479
diff
changeset
|
347 |
in (classes', multi_arity_clause cpairs) end; |
18863 | 348 |
|
37577
5379f41a1322
merge "Sledgehammer_{F,H}OL_Clause", as requested by a FIXME
blanchet
parents:
37575
diff
changeset
|
349 |
datatype combtyp = |
37924 | 350 |
CombTVar of name | |
351 |
CombTFree of name | |
|
352 |
CombType of name * combtyp list |
|
37577
5379f41a1322
merge "Sledgehammer_{F,H}OL_Clause", as requested by a FIXME
blanchet
parents:
37575
diff
changeset
|
353 |
|
5379f41a1322
merge "Sledgehammer_{F,H}OL_Clause", as requested by a FIXME
blanchet
parents:
37575
diff
changeset
|
354 |
datatype combterm = |
5379f41a1322
merge "Sledgehammer_{F,H}OL_Clause", as requested by a FIXME
blanchet
parents:
37575
diff
changeset
|
355 |
CombConst of name * combtyp * combtyp list (* Const and Free *) | |
5379f41a1322
merge "Sledgehammer_{F,H}OL_Clause", as requested by a FIXME
blanchet
parents:
37575
diff
changeset
|
356 |
CombVar of name * combtyp | |
5379f41a1322
merge "Sledgehammer_{F,H}OL_Clause", as requested by a FIXME
blanchet
parents:
37575
diff
changeset
|
357 |
CombApp of combterm * combterm |
5379f41a1322
merge "Sledgehammer_{F,H}OL_Clause", as requested by a FIXME
blanchet
parents:
37575
diff
changeset
|
358 |
|
37923 | 359 |
datatype fol_literal = FOLLiteral of bool * combterm |
37577
5379f41a1322
merge "Sledgehammer_{F,H}OL_Clause", as requested by a FIXME
blanchet
parents:
37575
diff
changeset
|
360 |
|
5379f41a1322
merge "Sledgehammer_{F,H}OL_Clause", as requested by a FIXME
blanchet
parents:
37575
diff
changeset
|
361 |
(*********************************************************************) |
5379f41a1322
merge "Sledgehammer_{F,H}OL_Clause", as requested by a FIXME
blanchet
parents:
37575
diff
changeset
|
362 |
(* convert a clause with type Term.term to a clause with type clause *) |
5379f41a1322
merge "Sledgehammer_{F,H}OL_Clause", as requested by a FIXME
blanchet
parents:
37575
diff
changeset
|
363 |
(*********************************************************************) |
5379f41a1322
merge "Sledgehammer_{F,H}OL_Clause", as requested by a FIXME
blanchet
parents:
37575
diff
changeset
|
364 |
|
5379f41a1322
merge "Sledgehammer_{F,H}OL_Clause", as requested by a FIXME
blanchet
parents:
37575
diff
changeset
|
365 |
(*Result of a function type; no need to check that the argument type matches.*) |
37924 | 366 |
fun result_type (CombType (_, [_, tp2])) = tp2 |
37577
5379f41a1322
merge "Sledgehammer_{F,H}OL_Clause", as requested by a FIXME
blanchet
parents:
37575
diff
changeset
|
367 |
| result_type _ = raise Fail "non-function type" |
5379f41a1322
merge "Sledgehammer_{F,H}OL_Clause", as requested by a FIXME
blanchet
parents:
37575
diff
changeset
|
368 |
|
37994
b04307085a09
make TPTP generator accept full first-order formulas
blanchet
parents:
37992
diff
changeset
|
369 |
fun combtyp_of (CombConst (_, tp, _)) = tp |
b04307085a09
make TPTP generator accept full first-order formulas
blanchet
parents:
37992
diff
changeset
|
370 |
| combtyp_of (CombVar (_, tp)) = tp |
b04307085a09
make TPTP generator accept full first-order formulas
blanchet
parents:
37992
diff
changeset
|
371 |
| combtyp_of (CombApp (t1, _)) = result_type (combtyp_of t1) |
37577
5379f41a1322
merge "Sledgehammer_{F,H}OL_Clause", as requested by a FIXME
blanchet
parents:
37575
diff
changeset
|
372 |
|
5379f41a1322
merge "Sledgehammer_{F,H}OL_Clause", as requested by a FIXME
blanchet
parents:
37575
diff
changeset
|
373 |
(*gets the head of a combinator application, along with the list of arguments*) |
5379f41a1322
merge "Sledgehammer_{F,H}OL_Clause", as requested by a FIXME
blanchet
parents:
37575
diff
changeset
|
374 |
fun strip_combterm_comb u = |
5379f41a1322
merge "Sledgehammer_{F,H}OL_Clause", as requested by a FIXME
blanchet
parents:
37575
diff
changeset
|
375 |
let fun stripc (CombApp(t,u), ts) = stripc (t, u::ts) |
5379f41a1322
merge "Sledgehammer_{F,H}OL_Clause", as requested by a FIXME
blanchet
parents:
37575
diff
changeset
|
376 |
| stripc x = x |
5379f41a1322
merge "Sledgehammer_{F,H}OL_Clause", as requested by a FIXME
blanchet
parents:
37575
diff
changeset
|
377 |
in stripc(u,[]) end |
5379f41a1322
merge "Sledgehammer_{F,H}OL_Clause", as requested by a FIXME
blanchet
parents:
37575
diff
changeset
|
378 |
|
5379f41a1322
merge "Sledgehammer_{F,H}OL_Clause", as requested by a FIXME
blanchet
parents:
37575
diff
changeset
|
379 |
fun type_of (Type (a, Ts)) = |
5379f41a1322
merge "Sledgehammer_{F,H}OL_Clause", as requested by a FIXME
blanchet
parents:
37575
diff
changeset
|
380 |
let val (folTypes,ts) = types_of Ts in |
37924 | 381 |
(CombType (`make_fixed_type_const a, folTypes), ts) |
37577
5379f41a1322
merge "Sledgehammer_{F,H}OL_Clause", as requested by a FIXME
blanchet
parents:
37575
diff
changeset
|
382 |
end |
37924 | 383 |
| type_of (tp as TFree (a, _)) = (CombTFree (`make_fixed_type_var a), [tp]) |
37577
5379f41a1322
merge "Sledgehammer_{F,H}OL_Clause", as requested by a FIXME
blanchet
parents:
37575
diff
changeset
|
384 |
| type_of (tp as TVar (x, _)) = |
37924 | 385 |
(CombTVar (make_schematic_type_var x, string_of_indexname x), [tp]) |
37577
5379f41a1322
merge "Sledgehammer_{F,H}OL_Clause", as requested by a FIXME
blanchet
parents:
37575
diff
changeset
|
386 |
and types_of Ts = |
5379f41a1322
merge "Sledgehammer_{F,H}OL_Clause", as requested by a FIXME
blanchet
parents:
37575
diff
changeset
|
387 |
let val (folTyps, ts) = ListPair.unzip (map type_of Ts) in |
5379f41a1322
merge "Sledgehammer_{F,H}OL_Clause", as requested by a FIXME
blanchet
parents:
37575
diff
changeset
|
388 |
(folTyps, union_all ts) |
5379f41a1322
merge "Sledgehammer_{F,H}OL_Clause", as requested by a FIXME
blanchet
parents:
37575
diff
changeset
|
389 |
end |
5379f41a1322
merge "Sledgehammer_{F,H}OL_Clause", as requested by a FIXME
blanchet
parents:
37575
diff
changeset
|
390 |
|
5379f41a1322
merge "Sledgehammer_{F,H}OL_Clause", as requested by a FIXME
blanchet
parents:
37575
diff
changeset
|
391 |
(* same as above, but no gathering of sort information *) |
5379f41a1322
merge "Sledgehammer_{F,H}OL_Clause", as requested by a FIXME
blanchet
parents:
37575
diff
changeset
|
392 |
fun simp_type_of (Type (a, Ts)) = |
37924 | 393 |
CombType (`make_fixed_type_const a, map simp_type_of Ts) |
394 |
| simp_type_of (TFree (a, _)) = CombTFree (`make_fixed_type_var a) |
|
37577
5379f41a1322
merge "Sledgehammer_{F,H}OL_Clause", as requested by a FIXME
blanchet
parents:
37575
diff
changeset
|
395 |
| simp_type_of (TVar (x, _)) = |
37924 | 396 |
CombTVar (make_schematic_type_var x, string_of_indexname x) |
37577
5379f41a1322
merge "Sledgehammer_{F,H}OL_Clause", as requested by a FIXME
blanchet
parents:
37575
diff
changeset
|
397 |
|
37995
06f02b15ef8a
generate full first-order formulas (FOF) in Sledgehammer
blanchet
parents:
37994
diff
changeset
|
398 |
(* Converts a term (with combinators) into a combterm. Also accummulates sort |
06f02b15ef8a
generate full first-order formulas (FOF) in Sledgehammer
blanchet
parents:
37994
diff
changeset
|
399 |
infomation. *) |
06f02b15ef8a
generate full first-order formulas (FOF) in Sledgehammer
blanchet
parents:
37994
diff
changeset
|
400 |
fun combterm_from_term thy bs (P $ Q) = |
06f02b15ef8a
generate full first-order formulas (FOF) in Sledgehammer
blanchet
parents:
37994
diff
changeset
|
401 |
let val (P', tsP) = combterm_from_term thy bs P |
06f02b15ef8a
generate full first-order formulas (FOF) in Sledgehammer
blanchet
parents:
37994
diff
changeset
|
402 |
val (Q', tsQ) = combterm_from_term thy bs Q |
06f02b15ef8a
generate full first-order formulas (FOF) in Sledgehammer
blanchet
parents:
37994
diff
changeset
|
403 |
in (CombApp (P', Q'), union (op =) tsP tsQ) end |
06f02b15ef8a
generate full first-order formulas (FOF) in Sledgehammer
blanchet
parents:
37994
diff
changeset
|
404 |
| combterm_from_term thy _ (Const (c, T)) = |
37577
5379f41a1322
merge "Sledgehammer_{F,H}OL_Clause", as requested by a FIXME
blanchet
parents:
37575
diff
changeset
|
405 |
let |
5379f41a1322
merge "Sledgehammer_{F,H}OL_Clause", as requested by a FIXME
blanchet
parents:
37575
diff
changeset
|
406 |
val (tp, ts) = type_of T |
5379f41a1322
merge "Sledgehammer_{F,H}OL_Clause", as requested by a FIXME
blanchet
parents:
37575
diff
changeset
|
407 |
val tvar_list = |
5379f41a1322
merge "Sledgehammer_{F,H}OL_Clause", as requested by a FIXME
blanchet
parents:
37575
diff
changeset
|
408 |
(if String.isPrefix skolem_theory_name c then |
5379f41a1322
merge "Sledgehammer_{F,H}OL_Clause", as requested by a FIXME
blanchet
parents:
37575
diff
changeset
|
409 |
[] |> Term.add_tvarsT T |> map TVar |
5379f41a1322
merge "Sledgehammer_{F,H}OL_Clause", as requested by a FIXME
blanchet
parents:
37575
diff
changeset
|
410 |
else |
5379f41a1322
merge "Sledgehammer_{F,H}OL_Clause", as requested by a FIXME
blanchet
parents:
37575
diff
changeset
|
411 |
(c, T) |> Sign.const_typargs thy) |
5379f41a1322
merge "Sledgehammer_{F,H}OL_Clause", as requested by a FIXME
blanchet
parents:
37575
diff
changeset
|
412 |
|> map simp_type_of |
5379f41a1322
merge "Sledgehammer_{F,H}OL_Clause", as requested by a FIXME
blanchet
parents:
37575
diff
changeset
|
413 |
val c' = CombConst (`make_fixed_const c, tp, tvar_list) |
5379f41a1322
merge "Sledgehammer_{F,H}OL_Clause", as requested by a FIXME
blanchet
parents:
37575
diff
changeset
|
414 |
in (c',ts) end |
37995
06f02b15ef8a
generate full first-order formulas (FOF) in Sledgehammer
blanchet
parents:
37994
diff
changeset
|
415 |
| combterm_from_term _ _ (Free (v, T)) = |
37577
5379f41a1322
merge "Sledgehammer_{F,H}OL_Clause", as requested by a FIXME
blanchet
parents:
37575
diff
changeset
|
416 |
let val (tp,ts) = type_of T |
5379f41a1322
merge "Sledgehammer_{F,H}OL_Clause", as requested by a FIXME
blanchet
parents:
37575
diff
changeset
|
417 |
val v' = CombConst (`make_fixed_var v, tp, []) |
5379f41a1322
merge "Sledgehammer_{F,H}OL_Clause", as requested by a FIXME
blanchet
parents:
37575
diff
changeset
|
418 |
in (v',ts) end |
37995
06f02b15ef8a
generate full first-order formulas (FOF) in Sledgehammer
blanchet
parents:
37994
diff
changeset
|
419 |
| combterm_from_term _ _ (Var (v, T)) = |
37577
5379f41a1322
merge "Sledgehammer_{F,H}OL_Clause", as requested by a FIXME
blanchet
parents:
37575
diff
changeset
|
420 |
let val (tp,ts) = type_of T |
5379f41a1322
merge "Sledgehammer_{F,H}OL_Clause", as requested by a FIXME
blanchet
parents:
37575
diff
changeset
|
421 |
val v' = CombVar ((make_schematic_var v, string_of_indexname v), tp) |
5379f41a1322
merge "Sledgehammer_{F,H}OL_Clause", as requested by a FIXME
blanchet
parents:
37575
diff
changeset
|
422 |
in (v',ts) end |
37995
06f02b15ef8a
generate full first-order formulas (FOF) in Sledgehammer
blanchet
parents:
37994
diff
changeset
|
423 |
| combterm_from_term _ bs (Bound j) = |
06f02b15ef8a
generate full first-order formulas (FOF) in Sledgehammer
blanchet
parents:
37994
diff
changeset
|
424 |
let |
06f02b15ef8a
generate full first-order formulas (FOF) in Sledgehammer
blanchet
parents:
37994
diff
changeset
|
425 |
val (s, T) = nth bs j |
06f02b15ef8a
generate full first-order formulas (FOF) in Sledgehammer
blanchet
parents:
37994
diff
changeset
|
426 |
val (tp, ts) = type_of T |
06f02b15ef8a
generate full first-order formulas (FOF) in Sledgehammer
blanchet
parents:
37994
diff
changeset
|
427 |
val v' = CombConst (`make_bound_var s, tp, []) |
06f02b15ef8a
generate full first-order formulas (FOF) in Sledgehammer
blanchet
parents:
37994
diff
changeset
|
428 |
in (v', ts) end |
06f02b15ef8a
generate full first-order formulas (FOF) in Sledgehammer
blanchet
parents:
37994
diff
changeset
|
429 |
| combterm_from_term _ _ (Abs _) = raise Fail "HOL clause: Abs" |
37577
5379f41a1322
merge "Sledgehammer_{F,H}OL_Clause", as requested by a FIXME
blanchet
parents:
37575
diff
changeset
|
430 |
|
5379f41a1322
merge "Sledgehammer_{F,H}OL_Clause", as requested by a FIXME
blanchet
parents:
37575
diff
changeset
|
431 |
fun predicate_of thy ((@{const Not} $ P), pos) = predicate_of thy (P, not pos) |
37995
06f02b15ef8a
generate full first-order formulas (FOF) in Sledgehammer
blanchet
parents:
37994
diff
changeset
|
432 |
| predicate_of thy (t, pos) = |
06f02b15ef8a
generate full first-order formulas (FOF) in Sledgehammer
blanchet
parents:
37994
diff
changeset
|
433 |
(combterm_from_term thy [] (Envir.eta_contract t), pos) |
37577
5379f41a1322
merge "Sledgehammer_{F,H}OL_Clause", as requested by a FIXME
blanchet
parents:
37575
diff
changeset
|
434 |
|
5379f41a1322
merge "Sledgehammer_{F,H}OL_Clause", as requested by a FIXME
blanchet
parents:
37575
diff
changeset
|
435 |
fun literals_of_term1 args thy (@{const Trueprop} $ P) = |
5379f41a1322
merge "Sledgehammer_{F,H}OL_Clause", as requested by a FIXME
blanchet
parents:
37575
diff
changeset
|
436 |
literals_of_term1 args thy P |
5379f41a1322
merge "Sledgehammer_{F,H}OL_Clause", as requested by a FIXME
blanchet
parents:
37575
diff
changeset
|
437 |
| literals_of_term1 args thy (@{const "op |"} $ P $ Q) = |
5379f41a1322
merge "Sledgehammer_{F,H}OL_Clause", as requested by a FIXME
blanchet
parents:
37575
diff
changeset
|
438 |
literals_of_term1 (literals_of_term1 args thy P) thy Q |
5379f41a1322
merge "Sledgehammer_{F,H}OL_Clause", as requested by a FIXME
blanchet
parents:
37575
diff
changeset
|
439 |
| literals_of_term1 (lits, ts) thy P = |
5379f41a1322
merge "Sledgehammer_{F,H}OL_Clause", as requested by a FIXME
blanchet
parents:
37575
diff
changeset
|
440 |
let val ((pred, ts'), pol) = predicate_of thy (P, true) in |
37923 | 441 |
(FOLLiteral (pol, pred) :: lits, union (op =) ts ts') |
37577
5379f41a1322
merge "Sledgehammer_{F,H}OL_Clause", as requested by a FIXME
blanchet
parents:
37575
diff
changeset
|
442 |
end |
5379f41a1322
merge "Sledgehammer_{F,H}OL_Clause", as requested by a FIXME
blanchet
parents:
37575
diff
changeset
|
443 |
val literals_of_term = literals_of_term1 ([], []) |
5379f41a1322
merge "Sledgehammer_{F,H}OL_Clause", as requested by a FIXME
blanchet
parents:
37575
diff
changeset
|
444 |
|
5379f41a1322
merge "Sledgehammer_{F,H}OL_Clause", as requested by a FIXME
blanchet
parents:
37575
diff
changeset
|
445 |
fun skolem_name i j num_T_args = |
5379f41a1322
merge "Sledgehammer_{F,H}OL_Clause", as requested by a FIXME
blanchet
parents:
37575
diff
changeset
|
446 |
skolem_prefix ^ (space_implode "_" (map Int.toString [i, j, num_T_args])) ^ |
5379f41a1322
merge "Sledgehammer_{F,H}OL_Clause", as requested by a FIXME
blanchet
parents:
37575
diff
changeset
|
447 |
skolem_infix ^ "g" |
5379f41a1322
merge "Sledgehammer_{F,H}OL_Clause", as requested by a FIXME
blanchet
parents:
37575
diff
changeset
|
448 |
|
37625
35eeb95c5bee
rename "skolem_somes" to "skolems", now that there's only one flavor of Skolems
blanchet
parents:
37624
diff
changeset
|
449 |
fun conceal_skolem_terms i skolems t = |
37577
5379f41a1322
merge "Sledgehammer_{F,H}OL_Clause", as requested by a FIXME
blanchet
parents:
37575
diff
changeset
|
450 |
if exists_Const (curry (op =) @{const_name skolem_id} o fst) t then |
5379f41a1322
merge "Sledgehammer_{F,H}OL_Clause", as requested by a FIXME
blanchet
parents:
37575
diff
changeset
|
451 |
let |
37625
35eeb95c5bee
rename "skolem_somes" to "skolems", now that there's only one flavor of Skolems
blanchet
parents:
37624
diff
changeset
|
452 |
fun aux skolems |
37577
5379f41a1322
merge "Sledgehammer_{F,H}OL_Clause", as requested by a FIXME
blanchet
parents:
37575
diff
changeset
|
453 |
(t as (Const (@{const_name skolem_id}, Type (_, [_, T])) $ _)) = |
5379f41a1322
merge "Sledgehammer_{F,H}OL_Clause", as requested by a FIXME
blanchet
parents:
37575
diff
changeset
|
454 |
let |
37625
35eeb95c5bee
rename "skolem_somes" to "skolems", now that there's only one flavor of Skolems
blanchet
parents:
37624
diff
changeset
|
455 |
val (skolems, s) = |
37577
5379f41a1322
merge "Sledgehammer_{F,H}OL_Clause", as requested by a FIXME
blanchet
parents:
37575
diff
changeset
|
456 |
if i = ~1 then |
37625
35eeb95c5bee
rename "skolem_somes" to "skolems", now that there's only one flavor of Skolems
blanchet
parents:
37624
diff
changeset
|
457 |
(skolems, @{const_name undefined}) |
35eeb95c5bee
rename "skolem_somes" to "skolems", now that there's only one flavor of Skolems
blanchet
parents:
37624
diff
changeset
|
458 |
else case AList.find (op aconv) skolems t of |
35eeb95c5bee
rename "skolem_somes" to "skolems", now that there's only one flavor of Skolems
blanchet
parents:
37624
diff
changeset
|
459 |
s :: _ => (skolems, s) |
37577
5379f41a1322
merge "Sledgehammer_{F,H}OL_Clause", as requested by a FIXME
blanchet
parents:
37575
diff
changeset
|
460 |
| [] => |
5379f41a1322
merge "Sledgehammer_{F,H}OL_Clause", as requested by a FIXME
blanchet
parents:
37575
diff
changeset
|
461 |
let |
5379f41a1322
merge "Sledgehammer_{F,H}OL_Clause", as requested by a FIXME
blanchet
parents:
37575
diff
changeset
|
462 |
val s = skolem_theory_name ^ "." ^ |
37625
35eeb95c5bee
rename "skolem_somes" to "skolems", now that there's only one flavor of Skolems
blanchet
parents:
37624
diff
changeset
|
463 |
skolem_name i (length skolems) |
37577
5379f41a1322
merge "Sledgehammer_{F,H}OL_Clause", as requested by a FIXME
blanchet
parents:
37575
diff
changeset
|
464 |
(length (Term.add_tvarsT T [])) |
37625
35eeb95c5bee
rename "skolem_somes" to "skolems", now that there's only one flavor of Skolems
blanchet
parents:
37624
diff
changeset
|
465 |
in ((s, t) :: skolems, s) end |
35eeb95c5bee
rename "skolem_somes" to "skolems", now that there's only one flavor of Skolems
blanchet
parents:
37624
diff
changeset
|
466 |
in (skolems, Const (s, T)) end |
35eeb95c5bee
rename "skolem_somes" to "skolems", now that there's only one flavor of Skolems
blanchet
parents:
37624
diff
changeset
|
467 |
| aux skolems (t1 $ t2) = |
37577
5379f41a1322
merge "Sledgehammer_{F,H}OL_Clause", as requested by a FIXME
blanchet
parents:
37575
diff
changeset
|
468 |
let |
37625
35eeb95c5bee
rename "skolem_somes" to "skolems", now that there's only one flavor of Skolems
blanchet
parents:
37624
diff
changeset
|
469 |
val (skolems, t1) = aux skolems t1 |
35eeb95c5bee
rename "skolem_somes" to "skolems", now that there's only one flavor of Skolems
blanchet
parents:
37624
diff
changeset
|
470 |
val (skolems, t2) = aux skolems t2 |
35eeb95c5bee
rename "skolem_somes" to "skolems", now that there's only one flavor of Skolems
blanchet
parents:
37624
diff
changeset
|
471 |
in (skolems, t1 $ t2) end |
35eeb95c5bee
rename "skolem_somes" to "skolems", now that there's only one flavor of Skolems
blanchet
parents:
37624
diff
changeset
|
472 |
| aux skolems (Abs (s, T, t')) = |
35eeb95c5bee
rename "skolem_somes" to "skolems", now that there's only one flavor of Skolems
blanchet
parents:
37624
diff
changeset
|
473 |
let val (skolems, t') = aux skolems t' in |
35eeb95c5bee
rename "skolem_somes" to "skolems", now that there's only one flavor of Skolems
blanchet
parents:
37624
diff
changeset
|
474 |
(skolems, Abs (s, T, t')) |
37577
5379f41a1322
merge "Sledgehammer_{F,H}OL_Clause", as requested by a FIXME
blanchet
parents:
37575
diff
changeset
|
475 |
end |
37625
35eeb95c5bee
rename "skolem_somes" to "skolems", now that there's only one flavor of Skolems
blanchet
parents:
37624
diff
changeset
|
476 |
| aux skolems t = (skolems, t) |
35eeb95c5bee
rename "skolem_somes" to "skolems", now that there's only one flavor of Skolems
blanchet
parents:
37624
diff
changeset
|
477 |
in aux skolems t end |
37577
5379f41a1322
merge "Sledgehammer_{F,H}OL_Clause", as requested by a FIXME
blanchet
parents:
37575
diff
changeset
|
478 |
else |
37625
35eeb95c5bee
rename "skolem_somes" to "skolems", now that there's only one flavor of Skolems
blanchet
parents:
37624
diff
changeset
|
479 |
(skolems, t) |
37577
5379f41a1322
merge "Sledgehammer_{F,H}OL_Clause", as requested by a FIXME
blanchet
parents:
37575
diff
changeset
|
480 |
|
37632 | 481 |
fun reveal_skolem_terms skolems = |
482 |
map_aterms (fn t as Const (s, _) => |
|
483 |
if String.isPrefix skolem_theory_name s then |
|
484 |
AList.lookup (op =) skolems s |> the |
|
485 |
|> map_types Type_Infer.paramify_vars |
|
486 |
else |
|
487 |
t |
|
488 |
| t => t) |
|
489 |
||
37577
5379f41a1322
merge "Sledgehammer_{F,H}OL_Clause", as requested by a FIXME
blanchet
parents:
37575
diff
changeset
|
490 |
|
5379f41a1322
merge "Sledgehammer_{F,H}OL_Clause", as requested by a FIXME
blanchet
parents:
37575
diff
changeset
|
491 |
(***************************************************************) |
5379f41a1322
merge "Sledgehammer_{F,H}OL_Clause", as requested by a FIXME
blanchet
parents:
37575
diff
changeset
|
492 |
(* Type Classes Present in the Axiom or Conjecture Clauses *) |
5379f41a1322
merge "Sledgehammer_{F,H}OL_Clause", as requested by a FIXME
blanchet
parents:
37575
diff
changeset
|
493 |
(***************************************************************) |
5379f41a1322
merge "Sledgehammer_{F,H}OL_Clause", as requested by a FIXME
blanchet
parents:
37575
diff
changeset
|
494 |
|
5379f41a1322
merge "Sledgehammer_{F,H}OL_Clause", as requested by a FIXME
blanchet
parents:
37575
diff
changeset
|
495 |
fun set_insert (x, s) = Symtab.update (x, ()) s |
5379f41a1322
merge "Sledgehammer_{F,H}OL_Clause", as requested by a FIXME
blanchet
parents:
37575
diff
changeset
|
496 |
|
5379f41a1322
merge "Sledgehammer_{F,H}OL_Clause", as requested by a FIXME
blanchet
parents:
37575
diff
changeset
|
497 |
fun add_classes (sorts, cset) = List.foldl set_insert cset (flat sorts) |
5379f41a1322
merge "Sledgehammer_{F,H}OL_Clause", as requested by a FIXME
blanchet
parents:
37575
diff
changeset
|
498 |
|
5379f41a1322
merge "Sledgehammer_{F,H}OL_Clause", as requested by a FIXME
blanchet
parents:
37575
diff
changeset
|
499 |
(*Remove this trivial type class*) |
5379f41a1322
merge "Sledgehammer_{F,H}OL_Clause", as requested by a FIXME
blanchet
parents:
37575
diff
changeset
|
500 |
fun delete_type cset = Symtab.delete_safe (the_single @{sort HOL.type}) cset; |
5379f41a1322
merge "Sledgehammer_{F,H}OL_Clause", as requested by a FIXME
blanchet
parents:
37575
diff
changeset
|
501 |
|
5379f41a1322
merge "Sledgehammer_{F,H}OL_Clause", as requested by a FIXME
blanchet
parents:
37575
diff
changeset
|
502 |
fun tfree_classes_of_terms ts = |
5379f41a1322
merge "Sledgehammer_{F,H}OL_Clause", as requested by a FIXME
blanchet
parents:
37575
diff
changeset
|
503 |
let val sorts_list = map (map #2 o OldTerm.term_tfrees) ts |
5379f41a1322
merge "Sledgehammer_{F,H}OL_Clause", as requested by a FIXME
blanchet
parents:
37575
diff
changeset
|
504 |
in Symtab.keys (delete_type (List.foldl add_classes Symtab.empty sorts_list)) end; |
5379f41a1322
merge "Sledgehammer_{F,H}OL_Clause", as requested by a FIXME
blanchet
parents:
37575
diff
changeset
|
505 |
|
5379f41a1322
merge "Sledgehammer_{F,H}OL_Clause", as requested by a FIXME
blanchet
parents:
37575
diff
changeset
|
506 |
fun tvar_classes_of_terms ts = |
5379f41a1322
merge "Sledgehammer_{F,H}OL_Clause", as requested by a FIXME
blanchet
parents:
37575
diff
changeset
|
507 |
let val sorts_list = map (map #2 o OldTerm.term_tvars) ts |
5379f41a1322
merge "Sledgehammer_{F,H}OL_Clause", as requested by a FIXME
blanchet
parents:
37575
diff
changeset
|
508 |
in Symtab.keys (delete_type (List.foldl add_classes Symtab.empty sorts_list)) end; |
5379f41a1322
merge "Sledgehammer_{F,H}OL_Clause", as requested by a FIXME
blanchet
parents:
37575
diff
changeset
|
509 |
|
5379f41a1322
merge "Sledgehammer_{F,H}OL_Clause", as requested by a FIXME
blanchet
parents:
37575
diff
changeset
|
510 |
(*fold type constructors*) |
5379f41a1322
merge "Sledgehammer_{F,H}OL_Clause", as requested by a FIXME
blanchet
parents:
37575
diff
changeset
|
511 |
fun fold_type_consts f (Type (a, Ts)) x = fold (fold_type_consts f) Ts (f (a,x)) |
5379f41a1322
merge "Sledgehammer_{F,H}OL_Clause", as requested by a FIXME
blanchet
parents:
37575
diff
changeset
|
512 |
| fold_type_consts _ _ x = x; |
5379f41a1322
merge "Sledgehammer_{F,H}OL_Clause", as requested by a FIXME
blanchet
parents:
37575
diff
changeset
|
513 |
|
5379f41a1322
merge "Sledgehammer_{F,H}OL_Clause", as requested by a FIXME
blanchet
parents:
37575
diff
changeset
|
514 |
(*Type constructors used to instantiate overloaded constants are the only ones needed.*) |
5379f41a1322
merge "Sledgehammer_{F,H}OL_Clause", as requested by a FIXME
blanchet
parents:
37575
diff
changeset
|
515 |
fun add_type_consts_in_term thy = |
5379f41a1322
merge "Sledgehammer_{F,H}OL_Clause", as requested by a FIXME
blanchet
parents:
37575
diff
changeset
|
516 |
let |
5379f41a1322
merge "Sledgehammer_{F,H}OL_Clause", as requested by a FIXME
blanchet
parents:
37575
diff
changeset
|
517 |
val const_typargs = Sign.const_typargs thy |
5379f41a1322
merge "Sledgehammer_{F,H}OL_Clause", as requested by a FIXME
blanchet
parents:
37575
diff
changeset
|
518 |
fun aux (Const x) = fold (fold_type_consts set_insert) (const_typargs x) |
5379f41a1322
merge "Sledgehammer_{F,H}OL_Clause", as requested by a FIXME
blanchet
parents:
37575
diff
changeset
|
519 |
| aux (Abs (_, _, u)) = aux u |
5379f41a1322
merge "Sledgehammer_{F,H}OL_Clause", as requested by a FIXME
blanchet
parents:
37575
diff
changeset
|
520 |
| aux (Const (@{const_name skolem_id}, _) $ _) = I |
5379f41a1322
merge "Sledgehammer_{F,H}OL_Clause", as requested by a FIXME
blanchet
parents:
37575
diff
changeset
|
521 |
| aux (t $ u) = aux t #> aux u |
5379f41a1322
merge "Sledgehammer_{F,H}OL_Clause", as requested by a FIXME
blanchet
parents:
37575
diff
changeset
|
522 |
| aux _ = I |
5379f41a1322
merge "Sledgehammer_{F,H}OL_Clause", as requested by a FIXME
blanchet
parents:
37575
diff
changeset
|
523 |
in aux end |
5379f41a1322
merge "Sledgehammer_{F,H}OL_Clause", as requested by a FIXME
blanchet
parents:
37575
diff
changeset
|
524 |
|
5379f41a1322
merge "Sledgehammer_{F,H}OL_Clause", as requested by a FIXME
blanchet
parents:
37575
diff
changeset
|
525 |
fun type_consts_of_terms thy ts = |
5379f41a1322
merge "Sledgehammer_{F,H}OL_Clause", as requested by a FIXME
blanchet
parents:
37575
diff
changeset
|
526 |
Symtab.keys (fold (add_type_consts_in_term thy) ts Symtab.empty); |
5379f41a1322
merge "Sledgehammer_{F,H}OL_Clause", as requested by a FIXME
blanchet
parents:
37575
diff
changeset
|
527 |
|
15347 | 528 |
end; |