author | blanchet |
Tue, 29 Jun 2010 09:19:16 +0200 | |
changeset 37624 | 3ee568334813 |
parent 37623 | 295f3a9b44b6 |
child 37625 | 35eeb95c5bee |
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 |
33311 | 2 |
Author: Jia Meng, Cambridge University Computer Laboratory |
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 kind = Axiom | Conjecture |
5379f41a1322
merge "Sledgehammer_{F,H}OL_Clause", as requested by a FIXME
blanchet
parents:
37575
diff
changeset
|
13 |
datatype type_literal = |
5379f41a1322
merge "Sledgehammer_{F,H}OL_Clause", as requested by a FIXME
blanchet
parents:
37575
diff
changeset
|
14 |
TyLitVar of string * name | |
5379f41a1322
merge "Sledgehammer_{F,H}OL_Clause", as requested by a FIXME
blanchet
parents:
37575
diff
changeset
|
15 |
TyLitFree of string * name |
5379f41a1322
merge "Sledgehammer_{F,H}OL_Clause", as requested by a FIXME
blanchet
parents:
37575
diff
changeset
|
16 |
datatype arLit = |
5379f41a1322
merge "Sledgehammer_{F,H}OL_Clause", as requested by a FIXME
blanchet
parents:
37575
diff
changeset
|
17 |
TConsLit of class * string * string list |
5379f41a1322
merge "Sledgehammer_{F,H}OL_Clause", as requested by a FIXME
blanchet
parents:
37575
diff
changeset
|
18 |
| TVarLit of class * string |
5379f41a1322
merge "Sledgehammer_{F,H}OL_Clause", as requested by a FIXME
blanchet
parents:
37575
diff
changeset
|
19 |
datatype arity_clause = ArityClause of |
5379f41a1322
merge "Sledgehammer_{F,H}OL_Clause", as requested by a FIXME
blanchet
parents:
37575
diff
changeset
|
20 |
{axiom_name: string, conclLit: arLit, premLits: arLit list} |
5379f41a1322
merge "Sledgehammer_{F,H}OL_Clause", as requested by a FIXME
blanchet
parents:
37575
diff
changeset
|
21 |
datatype classrel_clause = ClassrelClause of |
5379f41a1322
merge "Sledgehammer_{F,H}OL_Clause", as requested by a FIXME
blanchet
parents:
37575
diff
changeset
|
22 |
{axiom_name: string, subclass: class, superclass: class} |
5379f41a1322
merge "Sledgehammer_{F,H}OL_Clause", as requested by a FIXME
blanchet
parents:
37575
diff
changeset
|
23 |
datatype combtyp = |
5379f41a1322
merge "Sledgehammer_{F,H}OL_Clause", as requested by a FIXME
blanchet
parents:
37575
diff
changeset
|
24 |
TyVar of name | |
5379f41a1322
merge "Sledgehammer_{F,H}OL_Clause", as requested by a FIXME
blanchet
parents:
37575
diff
changeset
|
25 |
TyFree of name | |
5379f41a1322
merge "Sledgehammer_{F,H}OL_Clause", as requested by a FIXME
blanchet
parents:
37575
diff
changeset
|
26 |
TyConstr of name * combtyp list |
5379f41a1322
merge "Sledgehammer_{F,H}OL_Clause", as requested by a FIXME
blanchet
parents:
37575
diff
changeset
|
27 |
datatype combterm = |
5379f41a1322
merge "Sledgehammer_{F,H}OL_Clause", as requested by a FIXME
blanchet
parents:
37575
diff
changeset
|
28 |
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
|
29 |
CombVar of name * combtyp | |
5379f41a1322
merge "Sledgehammer_{F,H}OL_Clause", as requested by a FIXME
blanchet
parents:
37575
diff
changeset
|
30 |
CombApp of combterm * combterm |
5379f41a1322
merge "Sledgehammer_{F,H}OL_Clause", as requested by a FIXME
blanchet
parents:
37575
diff
changeset
|
31 |
datatype literal = Literal of bool * combterm |
5379f41a1322
merge "Sledgehammer_{F,H}OL_Clause", as requested by a FIXME
blanchet
parents:
37575
diff
changeset
|
32 |
datatype hol_clause = |
5379f41a1322
merge "Sledgehammer_{F,H}OL_Clause", as requested by a FIXME
blanchet
parents:
37575
diff
changeset
|
33 |
HOLClause of {clause_id: int, axiom_name: string, th: thm, kind: kind, |
5379f41a1322
merge "Sledgehammer_{F,H}OL_Clause", as requested by a FIXME
blanchet
parents:
37575
diff
changeset
|
34 |
literals: literal list, ctypes_sorts: typ list} |
5379f41a1322
merge "Sledgehammer_{F,H}OL_Clause", as requested by a FIXME
blanchet
parents:
37575
diff
changeset
|
35 |
|
37509
f39464d971c4
factor out TPTP format output into file of its own, to facilitate further changes
blanchet
parents:
37500
diff
changeset
|
36 |
val type_wrapper_name : string |
24310 | 37 |
val schematic_var_prefix: string |
38 |
val fixed_var_prefix: string |
|
39 |
val tvar_prefix: string |
|
40 |
val tfree_prefix: string |
|
41 |
val const_prefix: string |
|
42 |
val tconst_prefix: string |
|
43 |
val class_prefix: string |
|
44 |
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
|
45 |
val invert_const: string -> string |
24310 | 46 |
val ascii_of: string -> string |
47 |
val undo_ascii_of: string -> string |
|
37572
a899f9506f39
more intra-module dependency cleanup + merge "const" and "type_const" tables, since this is safe
blanchet
parents:
37570
diff
changeset
|
48 |
val strip_prefix: string -> string -> string option |
24310 | 49 |
val make_schematic_var : string * int -> string |
18868 | 50 |
val make_fixed_var : string -> string |
51 |
val make_schematic_type_var : string * int -> string |
|
24310 | 52 |
val make_fixed_type_var : string -> string |
37498
b426cbdb5a23
removed Sledgehammer's support for the DFG syntax;
blanchet
parents:
37479
diff
changeset
|
53 |
val make_fixed_const : string -> string |
b426cbdb5a23
removed Sledgehammer's support for the DFG syntax;
blanchet
parents:
37479
diff
changeset
|
54 |
val make_fixed_type_const : string -> string |
18868 | 55 |
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
|
56 |
val skolem_theory_name: string |
fa57a87f92a0
get rid of Skolem cache by performing CNF-conversion after fact selection
blanchet
parents:
37616
diff
changeset
|
57 |
val skolem_prefix: string |
fa57a87f92a0
get rid of Skolem cache by performing CNF-conversion after fact selection
blanchet
parents:
37616
diff
changeset
|
58 |
val skolem_infix: string |
fa57a87f92a0
get rid of Skolem cache by performing CNF-conversion after fact selection
blanchet
parents:
37616
diff
changeset
|
59 |
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
|
60 |
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
|
61 |
val type_literals_for_types : typ list -> type_literal list |
35865 | 62 |
val make_classrel_clauses: theory -> class list -> class list -> classrel_clause list |
63 |
val make_arity_clauses: theory -> string list -> class list -> class list * arity_clause list |
|
37577
5379f41a1322
merge "Sledgehammer_{F,H}OL_Clause", as requested by a FIXME
blanchet
parents:
37575
diff
changeset
|
64 |
val type_of_combterm : combterm -> combtyp |
5379f41a1322
merge "Sledgehammer_{F,H}OL_Clause", as requested by a FIXME
blanchet
parents:
37575
diff
changeset
|
65 |
val strip_combterm_comb : combterm -> combterm * combterm list |
5379f41a1322
merge "Sledgehammer_{F,H}OL_Clause", as requested by a FIXME
blanchet
parents:
37575
diff
changeset
|
66 |
val literals_of_term : theory -> term -> literal list * typ list |
5379f41a1322
merge "Sledgehammer_{F,H}OL_Clause", as requested by a FIXME
blanchet
parents:
37575
diff
changeset
|
67 |
val conceal_skolem_somes : |
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 |
5379f41a1322
merge "Sledgehammer_{F,H}OL_Clause", as requested by a FIXME
blanchet
parents:
37575
diff
changeset
|
69 |
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
|
70 |
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
|
71 |
val type_consts_of_terms : theory -> term list -> string list |
24310 | 72 |
end |
15347 | 73 |
|
37578
9367cb36b1c4
renamed "Sledgehammer_FOL_Clauses" to "Metis_Clauses", so that Metis doesn't depend on Sledgehammer
blanchet
parents:
37577
diff
changeset
|
74 |
structure Metis_Clauses : METIS_CLAUSES = |
15347 | 75 |
struct |
76 |
||
37577
5379f41a1322
merge "Sledgehammer_{F,H}OL_Clause", as requested by a FIXME
blanchet
parents:
37575
diff
changeset
|
77 |
open Clausifier |
5379f41a1322
merge "Sledgehammer_{F,H}OL_Clause", as requested by a FIXME
blanchet
parents:
37575
diff
changeset
|
78 |
|
37509
f39464d971c4
factor out TPTP format output into file of its own, to facilitate further changes
blanchet
parents:
37500
diff
changeset
|
79 |
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
|
80 |
|
15347 | 81 |
val schematic_var_prefix = "V_"; |
82 |
val fixed_var_prefix = "v_"; |
|
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 |
|
37509
f39464d971c4
factor out TPTP format output into file of its own, to facilitate further changes
blanchet
parents:
37500
diff
changeset
|
87 |
val classrel_clause_prefix = "clsrel_"; |
15347 | 88 |
|
17230
77e93bf303a5
fixed arities and restored changes that had gone missing
paulson
parents:
17150
diff
changeset
|
89 |
val const_prefix = "c_"; |
24310 | 90 |
val tconst_prefix = "tc_"; |
91 |
val class_prefix = "class_"; |
|
15347 | 92 |
|
36218
0e4a01f3e7d3
get rid of "List.foldl" + add timestamp to SPASS
blanchet
parents:
36170
diff
changeset
|
93 |
fun union_all xss = fold (union (op =)) xss [] |
17775 | 94 |
|
36493
a3357a631b96
reintroduced short names for HOL->FOL constants; other parts of the code rely on these
blanchet
parents:
36491
diff
changeset
|
95 |
(* 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
|
96 |
last nine entries of the table unless you know what you are doing. *) |
15347 | 97 |
val const_trans_table = |
35865 | 98 |
Symtab.make [(@{const_name "op ="}, "equal"), |
99 |
(@{const_name "op &"}, "and"), |
|
100 |
(@{const_name "op |"}, "or"), |
|
101 |
(@{const_name "op -->"}, "implies"), |
|
36493
a3357a631b96
reintroduced short names for HOL->FOL constants; other parts of the code rely on these
blanchet
parents:
36491
diff
changeset
|
102 |
(@{const_name "op :"}, "in"), |
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"), |
37572
a899f9506f39
more intra-module dependency cleanup + merge "const" and "type_const" tables, since this is safe
blanchet
parents:
37570
diff
changeset
|
111 |
(@{const_name If}, "If"), |
a899f9506f39
more intra-module dependency cleanup + merge "const" and "type_const" tables, since this is safe
blanchet
parents:
37570
diff
changeset
|
112 |
(@{type_name "*"}, "prod"), |
a899f9506f39
more intra-module dependency cleanup + merge "const" and "type_const" tables, since this is safe
blanchet
parents:
37570
diff
changeset
|
113 |
(@{type_name "+"}, "sum")] |
15347 | 114 |
|
37572
a899f9506f39
more intra-module dependency cleanup + merge "const" and "type_const" tables, since this is safe
blanchet
parents:
37570
diff
changeset
|
115 |
(* 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
|
116 |
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
|
117 |
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
|
118 |
(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
|
119 |
|
a899f9506f39
more intra-module dependency cleanup + merge "const" and "type_const" tables, since this is safe
blanchet
parents:
37570
diff
changeset
|
120 |
val invert_const = perhaps (Symtab.lookup const_trans_table_inv) |
15347 | 121 |
|
15610 | 122 |
(*Escaping of special characters. |
123 |
Alphanumeric characters are left unchanged. |
|
124 |
The character _ goes to __ |
|
125 |
Characters in the range ASCII space to / go to _A to _P, respectively. |
|
24183 | 126 |
Other printing characters go to _nnn where nnn is the decimal ASCII code.*) |
127 |
val A_minus_space = Char.ord #"A" - Char.ord #" "; |
|
15610 | 128 |
|
24183 | 129 |
fun stringN_of_int 0 _ = "" |
130 |
| stringN_of_int k n = stringN_of_int (k-1) (n div 10) ^ Int.toString (n mod 10); |
|
15610 | 131 |
|
15347 | 132 |
fun ascii_of_c c = |
15610 | 133 |
if Char.isAlphaNum c then String.str c |
134 |
else if c = #"_" then "__" |
|
24310 | 135 |
else if #" " <= c andalso c <= #"/" |
15610 | 136 |
then "_" ^ String.str (Char.chr (Char.ord c + A_minus_space)) |
24310 | 137 |
else if Char.isPrint c |
24183 | 138 |
then ("_" ^ stringN_of_int 3 (Char.ord c)) (*fixed width, in case more digits follow*) |
15610 | 139 |
else "" |
15347 | 140 |
|
15610 | 141 |
val ascii_of = String.translate ascii_of_c; |
142 |
||
24183 | 143 |
(** Remove ASCII armouring from names in proof files **) |
144 |
||
145 |
(*We don't raise error exceptions because this code can run inside the watcher. |
|
146 |
Also, the errors are "impossible" (hah!)*) |
|
147 |
fun undo_ascii_aux rcs [] = String.implode(rev rcs) |
|
148 |
| undo_ascii_aux rcs [#"_"] = undo_ascii_aux (#"_"::rcs) [] (*ERROR*) |
|
149 |
(*Three types of _ escapes: __, _A to _P, _nnn*) |
|
150 |
| undo_ascii_aux rcs (#"_" :: #"_" :: cs) = undo_ascii_aux (#"_"::rcs) cs |
|
24310 | 151 |
| undo_ascii_aux rcs (#"_" :: c :: cs) = |
24183 | 152 |
if #"A" <= c andalso c<= #"P" (*translation of #" " to #"/"*) |
153 |
then undo_ascii_aux (Char.chr(Char.ord c - A_minus_space) :: rcs) cs |
|
24310 | 154 |
else |
24183 | 155 |
let val digits = List.take (c::cs, 3) handle Subscript => [] |
24310 | 156 |
in |
24183 | 157 |
case Int.fromString (String.implode digits) of |
158 |
NONE => undo_ascii_aux (c:: #"_"::rcs) cs (*ERROR*) |
|
159 |
| SOME n => undo_ascii_aux (Char.chr n :: rcs) (List.drop (cs, 2)) |
|
160 |
end |
|
161 |
| undo_ascii_aux rcs (c::cs) = undo_ascii_aux (c::rcs) cs; |
|
162 |
||
163 |
val undo_ascii_of = undo_ascii_aux [] o String.explode; |
|
15347 | 164 |
|
37572
a899f9506f39
more intra-module dependency cleanup + merge "const" and "type_const" tables, since this is safe
blanchet
parents:
37570
diff
changeset
|
165 |
(* 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
|
166 |
un-ASCII'd. *) |
a899f9506f39
more intra-module dependency cleanup + merge "const" and "type_const" tables, since this is safe
blanchet
parents:
37570
diff
changeset
|
167 |
fun strip_prefix s1 s = |
a899f9506f39
more intra-module dependency cleanup + merge "const" and "type_const" tables, since this is safe
blanchet
parents:
37570
diff
changeset
|
168 |
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
|
169 |
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
|
170 |
else |
a899f9506f39
more intra-module dependency cleanup + merge "const" and "type_const" tables, since this is safe
blanchet
parents:
37570
diff
changeset
|
171 |
NONE |
a899f9506f39
more intra-module dependency cleanup + merge "const" and "type_const" tables, since this is safe
blanchet
parents:
37570
diff
changeset
|
172 |
|
16925
0fd7b1438d28
simpler variable names, and no types for monomorphic constants
paulson
parents:
16903
diff
changeset
|
173 |
(*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
|
174 |
fun trim_type_var s = |
0fd7b1438d28
simpler variable names, and no types for monomorphic constants
paulson
parents:
16903
diff
changeset
|
175 |
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
|
176 |
else error ("trim_type: Malformed type variable encountered: " ^ s); |
0fd7b1438d28
simpler variable names, and no types for monomorphic constants
paulson
parents:
16903
diff
changeset
|
177 |
|
16903 | 178 |
fun ascii_of_indexname (v,0) = ascii_of v |
17525
ae5bb6001afb
tidying, and support for axclass/classrel clauses
paulson
parents:
17422
diff
changeset
|
179 |
| ascii_of_indexname (v,i) = ascii_of v ^ "_" ^ Int.toString i; |
15347 | 180 |
|
17230
77e93bf303a5
fixed arities and restored changes that had gone missing
paulson
parents:
17150
diff
changeset
|
181 |
fun make_schematic_var v = schematic_var_prefix ^ (ascii_of_indexname v); |
15347 | 182 |
fun make_fixed_var x = fixed_var_prefix ^ (ascii_of x); |
183 |
||
24310 | 184 |
fun make_schematic_type_var (x,i) = |
16925
0fd7b1438d28
simpler variable names, and no types for monomorphic constants
paulson
parents:
16903
diff
changeset
|
185 |
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
|
186 |
fun make_fixed_type_var x = tfree_prefix ^ (ascii_of (trim_type_var x)); |
15347 | 187 |
|
37498
b426cbdb5a23
removed Sledgehammer's support for the DFG syntax;
blanchet
parents:
37479
diff
changeset
|
188 |
fun lookup_const c = |
b426cbdb5a23
removed Sledgehammer's support for the DFG syntax;
blanchet
parents:
37479
diff
changeset
|
189 |
case Symtab.lookup const_trans_table c of |
b426cbdb5a23
removed Sledgehammer's support for the DFG syntax;
blanchet
parents:
37479
diff
changeset
|
190 |
SOME c' => c' |
b426cbdb5a23
removed Sledgehammer's support for the DFG syntax;
blanchet
parents:
37479
diff
changeset
|
191 |
| NONE => ascii_of c |
23075 | 192 |
|
36062 | 193 |
(* "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
|
194 |
fun make_fixed_const @{const_name "op ="} = "equal" |
b426cbdb5a23
removed Sledgehammer's support for the DFG syntax;
blanchet
parents:
37479
diff
changeset
|
195 |
| 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
|
196 |
|
37572
a899f9506f39
more intra-module dependency cleanup + merge "const" and "type_const" tables, since this is safe
blanchet
parents:
37570
diff
changeset
|
197 |
fun make_fixed_type_const c = tconst_prefix ^ lookup_const c |
17150
ce2a1aeb42aa
DFG output now works for untyped rules (ML "ResClause.untyped();")
quigley
parents:
16976
diff
changeset
|
198 |
|
17261 | 199 |
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
|
200 |
|
37618
fa57a87f92a0
get rid of Skolem cache by performing CNF-conversion after fact selection
blanchet
parents:
37616
diff
changeset
|
201 |
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
|
202 |
val skolem_prefix = "sko_" |
fa57a87f92a0
get rid of Skolem cache by performing CNF-conversion after fact selection
blanchet
parents:
37616
diff
changeset
|
203 |
val skolem_infix = "$" |
fa57a87f92a0
get rid of Skolem cache by performing CNF-conversion after fact selection
blanchet
parents:
37616
diff
changeset
|
204 |
|
fa57a87f92a0
get rid of Skolem cache by performing CNF-conversion after fact selection
blanchet
parents:
37616
diff
changeset
|
205 |
(* 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
|
206 |
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
|
207 |
val is_skolem_const_name = |
fa57a87f92a0
get rid of Skolem cache by performing CNF-conversion after fact selection
blanchet
parents:
37616
diff
changeset
|
208 |
Long_Name.base_name |
fa57a87f92a0
get rid of Skolem cache by performing CNF-conversion after fact selection
blanchet
parents:
37616
diff
changeset
|
209 |
#> 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
|
210 |
|
fa57a87f92a0
get rid of Skolem cache by performing CNF-conversion after fact selection
blanchet
parents:
37616
diff
changeset
|
211 |
(* 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
|
212 |
(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
|
213 |
constant name. *) |
fa57a87f92a0
get rid of Skolem cache by performing CNF-conversion after fact selection
blanchet
parents:
37616
diff
changeset
|
214 |
fun num_type_args thy s = |
fa57a87f92a0
get rid of Skolem cache by performing CNF-conversion after fact selection
blanchet
parents:
37616
diff
changeset
|
215 |
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
|
216 |
s |> unprefix skolem_theory_name |
fa57a87f92a0
get rid of Skolem cache by performing CNF-conversion after fact selection
blanchet
parents:
37616
diff
changeset
|
217 |
|> space_explode skolem_infix |> hd |
fa57a87f92a0
get rid of Skolem cache by performing CNF-conversion after fact selection
blanchet
parents:
37616
diff
changeset
|
218 |
|> 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
|
219 |
else |
fa57a87f92a0
get rid of Skolem cache by performing CNF-conversion after fact selection
blanchet
parents:
37616
diff
changeset
|
220 |
(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
|
221 |
|
37624 | 222 |
(**** 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
|
223 |
|
37624 | 224 |
type name = string * string |
15347 | 225 |
|
37577
5379f41a1322
merge "Sledgehammer_{F,H}OL_Clause", as requested by a FIXME
blanchet
parents:
37575
diff
changeset
|
226 |
datatype kind = Axiom | Conjecture |
23385 | 227 |
|
15347 | 228 |
(**** Isabelle FOL clauses ****) |
229 |
||
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
|
230 |
(* 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
|
231 |
datatype type_literal = |
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
|
232 |
TyLitVar of string * name | |
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
|
233 |
TyLitFree of string * name |
15347 | 234 |
|
17404
d16c3a62c396
the experimental tagging system, and the usual tidying
paulson
parents:
17375
diff
changeset
|
235 |
exception CLAUSE of string * term; |
15347 | 236 |
|
24310 | 237 |
(*Make literals for sorted type variables*) |
24940 | 238 |
fun sorts_on_typs_aux (_, []) = [] |
239 |
| sorts_on_typs_aux ((x,i), s::ss) = |
|
240 |
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
|
241 |
in |
bc3bb8e9594a
Improved and simplified the treatment of classrel/arity clauses
paulson
parents:
22383
diff
changeset
|
242 |
if s = "HOL.type" then sorts |
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
|
243 |
else if i = ~1 then TyLitFree (make_type_class s, `make_fixed_type_var x) :: 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:
36493
diff
changeset
|
244 |
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
|
245 |
end; |
17150
ce2a1aeb42aa
DFG output now works for untyped rules (ML "ResClause.untyped();")
quigley
parents:
16976
diff
changeset
|
246 |
|
24940 | 247 |
fun sorts_on_typs (TFree (a,s)) = sorts_on_typs_aux ((a,~1),s) |
248 |
| sorts_on_typs (TVar (v,s)) = sorts_on_typs_aux (v,s); |
|
249 |
||
24937
340523598914
context-based treatment of generalization; also handling TFrees in axiom clauses
paulson
parents:
24322
diff
changeset
|
250 |
(*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
|
251 |
fun type_literals_for_types Ts = |
adc11fb3f3aa
generate proper arity declarations for TFrees for SPASS's DFG format;
blanchet
parents:
36692
diff
changeset
|
252 |
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
|
253 |
|
1ffcf4802802
Literals aren't sorted any more. Output overloaded constants' type var instantiations.
mengj
parents:
19719
diff
changeset
|
254 |
(** make axiom and conjecture clauses. **) |
1ffcf4802802
Literals aren't sorted any more. Output overloaded constants' type var instantiations.
mengj
parents:
19719
diff
changeset
|
255 |
|
15347 | 256 |
(**** Isabelle arities ****) |
257 |
||
24310 | 258 |
datatype arLit = TConsLit of class * string * string list |
22643
bc3bb8e9594a
Improved and simplified the treatment of classrel/arity clauses
paulson
parents:
22383
diff
changeset
|
259 |
| TVarLit of class * string; |
24310 | 260 |
|
35865 | 261 |
datatype arity_clause = |
37500
7587b6e63454
thread original theorem along with CNF theorem, as a step toward killing the Skolem cache
blanchet
parents:
37498
diff
changeset
|
262 |
ArityClause of {axiom_name: string, conclLit: arLit, premLits: arLit list} |
15347 | 263 |
|
264 |
||
18798 | 265 |
fun gen_TVars 0 = [] |
266 |
| gen_TVars n = ("T_" ^ Int.toString n) :: gen_TVars (n-1); |
|
15347 | 267 |
|
18411
2d3165a0fb40
No axiom, arity or classrel clauses contain HOL.type. Negative occurrences are
paulson
parents:
18409
diff
changeset
|
268 |
fun pack_sort(_,[]) = [] |
2d3165a0fb40
No axiom, arity or classrel clauses contain HOL.type. Negative occurrences are
paulson
parents:
18409
diff
changeset
|
269 |
| pack_sort(tvar, "HOL.type"::srt) = pack_sort(tvar, srt) (*IGNORE sort "type"*) |
22643
bc3bb8e9594a
Improved and simplified the treatment of classrel/arity clauses
paulson
parents:
22383
diff
changeset
|
270 |
| pack_sort(tvar, cls::srt) = (cls, tvar) :: pack_sort(tvar, srt); |
24310 | 271 |
|
18411
2d3165a0fb40
No axiom, arity or classrel clauses contain HOL.type. Negative occurrences are
paulson
parents:
18409
diff
changeset
|
272 |
(*Arity of type constructor tcon :: (arg1,...,argN)res*) |
37498
b426cbdb5a23
removed Sledgehammer's support for the DFG syntax;
blanchet
parents:
37479
diff
changeset
|
273 |
fun make_axiom_arity_clause (tcons, axiom_name, (cls,args)) = |
21560 | 274 |
let val tvars = gen_TVars (length args) |
17845
1438291d57f0
deletion of Tools/res_types_sorts; removal of absolute numbering of clauses
paulson
parents:
17775
diff
changeset
|
275 |
val tvars_srts = ListPair.zip (tvars,args) |
1438291d57f0
deletion of Tools/res_types_sorts; removal of absolute numbering of clauses
paulson
parents:
17775
diff
changeset
|
276 |
in |
37498
b426cbdb5a23
removed Sledgehammer's support for the DFG syntax;
blanchet
parents:
37479
diff
changeset
|
277 |
ArityClause {axiom_name = axiom_name, |
b426cbdb5a23
removed Sledgehammer's support for the DFG syntax;
blanchet
parents:
37479
diff
changeset
|
278 |
conclLit = TConsLit (cls, make_fixed_type_const tcons, tvars), |
b426cbdb5a23
removed Sledgehammer's support for the DFG syntax;
blanchet
parents:
37479
diff
changeset
|
279 |
premLits = map TVarLit (union_all(map pack_sort tvars_srts))} |
17845
1438291d57f0
deletion of Tools/res_types_sorts; removal of absolute numbering of clauses
paulson
parents:
17775
diff
changeset
|
280 |
end; |
15347 | 281 |
|
282 |
||
283 |
(**** Isabelle class relations ****) |
|
284 |
||
35865 | 285 |
datatype classrel_clause = |
37500
7587b6e63454
thread original theorem along with CNF theorem, as a step toward killing the Skolem cache
blanchet
parents:
37498
diff
changeset
|
286 |
ClassrelClause of {axiom_name: string, subclass: class, superclass: class} |
24310 | 287 |
|
21290
33b6bb5d6ab8
Improvement to classrel clauses: now outputs the minimum needed.
paulson
parents:
21254
diff
changeset
|
288 |
(*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
|
289 |
fun class_pairs _ [] _ = [] |
21432
625797c592b2
Optimized class_pairs for the common case of no subclasses
paulson
parents:
21416
diff
changeset
|
290 |
| class_pairs thy subs supers = |
36218
0e4a01f3e7d3
get rid of "List.foldl" + add timestamp to SPASS
blanchet
parents:
36170
diff
changeset
|
291 |
let |
0e4a01f3e7d3
get rid of "List.foldl" + add timestamp to SPASS
blanchet
parents:
36170
diff
changeset
|
292 |
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
|
293 |
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
|
294 |
fun add_supers sub = fold (add_super sub) supers |
0e4a01f3e7d3
get rid of "List.foldl" + add timestamp to SPASS
blanchet
parents:
36170
diff
changeset
|
295 |
in fold add_supers subs [] end |
15347 | 296 |
|
35865 | 297 |
fun make_classrel_clause (sub,super) = |
37509
f39464d971c4
factor out TPTP format output into file of its own, to facilitate further changes
blanchet
parents:
37500
diff
changeset
|
298 |
ClassrelClause {axiom_name = classrel_clause_prefix ^ ascii_of sub ^ "_" ^ |
f39464d971c4
factor out TPTP format output into file of its own, to facilitate further changes
blanchet
parents:
37500
diff
changeset
|
299 |
ascii_of super, |
24310 | 300 |
subclass = make_type_class sub, |
21290
33b6bb5d6ab8
Improvement to classrel clauses: now outputs the minimum needed.
paulson
parents:
21254
diff
changeset
|
301 |
superclass = make_type_class super}; |
15347 | 302 |
|
21290
33b6bb5d6ab8
Improvement to classrel clauses: now outputs the minimum needed.
paulson
parents:
21254
diff
changeset
|
303 |
fun make_classrel_clauses thy subs supers = |
35865 | 304 |
map make_classrel_clause (class_pairs thy subs supers); |
18868 | 305 |
|
306 |
||
307 |
(** Isabelle arities **) |
|
17845
1438291d57f0
deletion of Tools/res_types_sorts; removal of absolute numbering of clauses
paulson
parents:
17775
diff
changeset
|
308 |
|
37498
b426cbdb5a23
removed Sledgehammer's support for the DFG syntax;
blanchet
parents:
37479
diff
changeset
|
309 |
fun arity_clause _ _ (_, []) = [] |
b426cbdb5a23
removed Sledgehammer's support for the DFG syntax;
blanchet
parents:
37479
diff
changeset
|
310 |
| arity_clause seen n (tcons, ("HOL.type",_)::ars) = (*ignore*) |
b426cbdb5a23
removed Sledgehammer's support for the DFG syntax;
blanchet
parents:
37479
diff
changeset
|
311 |
arity_clause seen n (tcons,ars) |
b426cbdb5a23
removed Sledgehammer's support for the DFG syntax;
blanchet
parents:
37479
diff
changeset
|
312 |
| 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
|
313 |
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
|
314 |
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
|
315 |
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
|
316 |
else |
37572
a899f9506f39
more intra-module dependency cleanup + merge "const" and "type_const" tables, since this is safe
blanchet
parents:
37570
diff
changeset
|
317 |
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
|
318 |
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
|
319 |
|
37498
b426cbdb5a23
removed Sledgehammer's support for the DFG syntax;
blanchet
parents:
37479
diff
changeset
|
320 |
fun multi_arity_clause [] = [] |
b426cbdb5a23
removed Sledgehammer's support for the DFG syntax;
blanchet
parents:
37479
diff
changeset
|
321 |
| multi_arity_clause ((tcons, ars) :: tc_arlists) = |
b426cbdb5a23
removed Sledgehammer's support for the DFG syntax;
blanchet
parents:
37479
diff
changeset
|
322 |
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
|
323 |
|
22643
bc3bb8e9594a
Improved and simplified the treatment of classrel/arity clauses
paulson
parents:
22383
diff
changeset
|
324 |
(*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
|
325 |
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
|
326 |
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
|
327 |
let val alg = Sign.classes_of thy |
36218
0e4a01f3e7d3
get rid of "List.foldl" + add timestamp to SPASS
blanchet
parents:
36170
diff
changeset
|
328 |
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
|
329 |
fun add_class tycon class = |
0e4a01f3e7d3
get rid of "List.foldl" + add timestamp to SPASS
blanchet
parents:
36170
diff
changeset
|
330 |
cons (class, domain_sorts tycon class) |
0e4a01f3e7d3
get rid of "List.foldl" + add timestamp to SPASS
blanchet
parents:
36170
diff
changeset
|
331 |
handle Sorts.CLASS_ERROR _ => I |
0e4a01f3e7d3
get rid of "List.foldl" + add timestamp to SPASS
blanchet
parents:
36170
diff
changeset
|
332 |
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
|
333 |
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
|
334 |
|
22643
bc3bb8e9594a
Improved and simplified the treatment of classrel/arity clauses
paulson
parents:
22383
diff
changeset
|
335 |
(*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
|
336 |
fun iter_type_class_pairs _ _ [] = ([], []) |
22643
bc3bb8e9594a
Improved and simplified the treatment of classrel/arity clauses
paulson
parents:
22383
diff
changeset
|
337 |
| iter_type_class_pairs thy tycons classes = |
bc3bb8e9594a
Improved and simplified the treatment of classrel/arity clauses
paulson
parents:
22383
diff
changeset
|
338 |
let val cpairs = type_class_pairs thy tycons classes |
33040 | 339 |
val newclasses = union_all (union_all (union_all (map (map #2 o #2) cpairs))) |
340 |
|> subtract (op =) classes |> subtract (op =) HOLogic.typeS |
|
24310 | 341 |
val (classes', cpairs') = iter_type_class_pairs thy tycons newclasses |
33042 | 342 |
in (union (op =) classes' classes, union (op =) cpairs' cpairs) end; |
24310 | 343 |
|
37498
b426cbdb5a23
removed Sledgehammer's support for the DFG syntax;
blanchet
parents:
37479
diff
changeset
|
344 |
fun make_arity_clauses thy tycons classes = |
24310 | 345 |
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
|
346 |
in (classes', multi_arity_clause cpairs) end; |
18863 | 347 |
|
37577
5379f41a1322
merge "Sledgehammer_{F,H}OL_Clause", as requested by a FIXME
blanchet
parents:
37575
diff
changeset
|
348 |
datatype combtyp = |
5379f41a1322
merge "Sledgehammer_{F,H}OL_Clause", as requested by a FIXME
blanchet
parents:
37575
diff
changeset
|
349 |
TyVar of name | |
5379f41a1322
merge "Sledgehammer_{F,H}OL_Clause", as requested by a FIXME
blanchet
parents:
37575
diff
changeset
|
350 |
TyFree of name | |
5379f41a1322
merge "Sledgehammer_{F,H}OL_Clause", as requested by a FIXME
blanchet
parents:
37575
diff
changeset
|
351 |
TyConstr of name * combtyp list |
5379f41a1322
merge "Sledgehammer_{F,H}OL_Clause", as requested by a FIXME
blanchet
parents:
37575
diff
changeset
|
352 |
|
5379f41a1322
merge "Sledgehammer_{F,H}OL_Clause", as requested by a FIXME
blanchet
parents:
37575
diff
changeset
|
353 |
datatype combterm = |
5379f41a1322
merge "Sledgehammer_{F,H}OL_Clause", as requested by a FIXME
blanchet
parents:
37575
diff
changeset
|
354 |
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
|
355 |
CombVar of name * combtyp | |
5379f41a1322
merge "Sledgehammer_{F,H}OL_Clause", as requested by a FIXME
blanchet
parents:
37575
diff
changeset
|
356 |
CombApp of combterm * combterm |
5379f41a1322
merge "Sledgehammer_{F,H}OL_Clause", as requested by a FIXME
blanchet
parents:
37575
diff
changeset
|
357 |
|
5379f41a1322
merge "Sledgehammer_{F,H}OL_Clause", as requested by a FIXME
blanchet
parents:
37575
diff
changeset
|
358 |
datatype literal = Literal of bool * combterm |
5379f41a1322
merge "Sledgehammer_{F,H}OL_Clause", as requested by a FIXME
blanchet
parents:
37575
diff
changeset
|
359 |
|
5379f41a1322
merge "Sledgehammer_{F,H}OL_Clause", as requested by a FIXME
blanchet
parents:
37575
diff
changeset
|
360 |
datatype hol_clause = |
5379f41a1322
merge "Sledgehammer_{F,H}OL_Clause", as requested by a FIXME
blanchet
parents:
37575
diff
changeset
|
361 |
HOLClause of {clause_id: int, axiom_name: string, th: thm, kind: kind, |
5379f41a1322
merge "Sledgehammer_{F,H}OL_Clause", as requested by a FIXME
blanchet
parents:
37575
diff
changeset
|
362 |
literals: literal list, ctypes_sorts: typ list} |
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 |
(* 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
|
366 |
(*********************************************************************) |
5379f41a1322
merge "Sledgehammer_{F,H}OL_Clause", as requested by a FIXME
blanchet
parents:
37575
diff
changeset
|
367 |
|
5379f41a1322
merge "Sledgehammer_{F,H}OL_Clause", as requested by a FIXME
blanchet
parents:
37575
diff
changeset
|
368 |
(*Result of a function type; no need to check that the argument type matches.*) |
5379f41a1322
merge "Sledgehammer_{F,H}OL_Clause", as requested by a FIXME
blanchet
parents:
37575
diff
changeset
|
369 |
fun result_type (TyConstr (_, [_, tp2])) = tp2 |
5379f41a1322
merge "Sledgehammer_{F,H}OL_Clause", as requested by a FIXME
blanchet
parents:
37575
diff
changeset
|
370 |
| result_type _ = raise Fail "non-function type" |
5379f41a1322
merge "Sledgehammer_{F,H}OL_Clause", as requested by a FIXME
blanchet
parents:
37575
diff
changeset
|
371 |
|
5379f41a1322
merge "Sledgehammer_{F,H}OL_Clause", as requested by a FIXME
blanchet
parents:
37575
diff
changeset
|
372 |
fun type_of_combterm (CombConst (_, tp, _)) = tp |
5379f41a1322
merge "Sledgehammer_{F,H}OL_Clause", as requested by a FIXME
blanchet
parents:
37575
diff
changeset
|
373 |
| type_of_combterm (CombVar (_, tp)) = tp |
5379f41a1322
merge "Sledgehammer_{F,H}OL_Clause", as requested by a FIXME
blanchet
parents:
37575
diff
changeset
|
374 |
| type_of_combterm (CombApp (t1, _)) = result_type (type_of_combterm t1) |
5379f41a1322
merge "Sledgehammer_{F,H}OL_Clause", as requested by a FIXME
blanchet
parents:
37575
diff
changeset
|
375 |
|
5379f41a1322
merge "Sledgehammer_{F,H}OL_Clause", as requested by a FIXME
blanchet
parents:
37575
diff
changeset
|
376 |
(*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
|
377 |
fun strip_combterm_comb u = |
5379f41a1322
merge "Sledgehammer_{F,H}OL_Clause", as requested by a FIXME
blanchet
parents:
37575
diff
changeset
|
378 |
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
|
379 |
| stripc x = x |
5379f41a1322
merge "Sledgehammer_{F,H}OL_Clause", as requested by a FIXME
blanchet
parents:
37575
diff
changeset
|
380 |
in stripc(u,[]) end |
5379f41a1322
merge "Sledgehammer_{F,H}OL_Clause", as requested by a FIXME
blanchet
parents:
37575
diff
changeset
|
381 |
|
5379f41a1322
merge "Sledgehammer_{F,H}OL_Clause", as requested by a FIXME
blanchet
parents:
37575
diff
changeset
|
382 |
fun type_of (Type (a, Ts)) = |
5379f41a1322
merge "Sledgehammer_{F,H}OL_Clause", as requested by a FIXME
blanchet
parents:
37575
diff
changeset
|
383 |
let val (folTypes,ts) = types_of Ts in |
5379f41a1322
merge "Sledgehammer_{F,H}OL_Clause", as requested by a FIXME
blanchet
parents:
37575
diff
changeset
|
384 |
(TyConstr (`make_fixed_type_const a, folTypes), ts) |
5379f41a1322
merge "Sledgehammer_{F,H}OL_Clause", as requested by a FIXME
blanchet
parents:
37575
diff
changeset
|
385 |
end |
5379f41a1322
merge "Sledgehammer_{F,H}OL_Clause", as requested by a FIXME
blanchet
parents:
37575
diff
changeset
|
386 |
| type_of (tp as TFree (a, _)) = (TyFree (`make_fixed_type_var a), [tp]) |
5379f41a1322
merge "Sledgehammer_{F,H}OL_Clause", as requested by a FIXME
blanchet
parents:
37575
diff
changeset
|
387 |
| type_of (tp as TVar (x, _)) = |
5379f41a1322
merge "Sledgehammer_{F,H}OL_Clause", as requested by a FIXME
blanchet
parents:
37575
diff
changeset
|
388 |
(TyVar (make_schematic_type_var x, string_of_indexname x), [tp]) |
5379f41a1322
merge "Sledgehammer_{F,H}OL_Clause", as requested by a FIXME
blanchet
parents:
37575
diff
changeset
|
389 |
and types_of Ts = |
5379f41a1322
merge "Sledgehammer_{F,H}OL_Clause", as requested by a FIXME
blanchet
parents:
37575
diff
changeset
|
390 |
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
|
391 |
(folTyps, union_all ts) |
5379f41a1322
merge "Sledgehammer_{F,H}OL_Clause", as requested by a FIXME
blanchet
parents:
37575
diff
changeset
|
392 |
end |
5379f41a1322
merge "Sledgehammer_{F,H}OL_Clause", as requested by a FIXME
blanchet
parents:
37575
diff
changeset
|
393 |
|
5379f41a1322
merge "Sledgehammer_{F,H}OL_Clause", as requested by a FIXME
blanchet
parents:
37575
diff
changeset
|
394 |
(* 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
|
395 |
fun simp_type_of (Type (a, Ts)) = |
5379f41a1322
merge "Sledgehammer_{F,H}OL_Clause", as requested by a FIXME
blanchet
parents:
37575
diff
changeset
|
396 |
TyConstr (`make_fixed_type_const a, map simp_type_of Ts) |
5379f41a1322
merge "Sledgehammer_{F,H}OL_Clause", as requested by a FIXME
blanchet
parents:
37575
diff
changeset
|
397 |
| simp_type_of (TFree (a, _)) = TyFree (`make_fixed_type_var a) |
5379f41a1322
merge "Sledgehammer_{F,H}OL_Clause", as requested by a FIXME
blanchet
parents:
37575
diff
changeset
|
398 |
| simp_type_of (TVar (x, _)) = |
5379f41a1322
merge "Sledgehammer_{F,H}OL_Clause", as requested by a FIXME
blanchet
parents:
37575
diff
changeset
|
399 |
TyVar (make_schematic_type_var x, string_of_indexname x) |
5379f41a1322
merge "Sledgehammer_{F,H}OL_Clause", as requested by a FIXME
blanchet
parents:
37575
diff
changeset
|
400 |
|
5379f41a1322
merge "Sledgehammer_{F,H}OL_Clause", as requested by a FIXME
blanchet
parents:
37575
diff
changeset
|
401 |
(* convert a Term.term (with combinators) into a combterm, also accummulate sort info *) |
5379f41a1322
merge "Sledgehammer_{F,H}OL_Clause", as requested by a FIXME
blanchet
parents:
37575
diff
changeset
|
402 |
fun combterm_of thy (Const (c, T)) = |
5379f41a1322
merge "Sledgehammer_{F,H}OL_Clause", as requested by a FIXME
blanchet
parents:
37575
diff
changeset
|
403 |
let |
5379f41a1322
merge "Sledgehammer_{F,H}OL_Clause", as requested by a FIXME
blanchet
parents:
37575
diff
changeset
|
404 |
val (tp, ts) = type_of T |
5379f41a1322
merge "Sledgehammer_{F,H}OL_Clause", as requested by a FIXME
blanchet
parents:
37575
diff
changeset
|
405 |
val tvar_list = |
5379f41a1322
merge "Sledgehammer_{F,H}OL_Clause", as requested by a FIXME
blanchet
parents:
37575
diff
changeset
|
406 |
(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
|
407 |
[] |> Term.add_tvarsT T |> map TVar |
5379f41a1322
merge "Sledgehammer_{F,H}OL_Clause", as requested by a FIXME
blanchet
parents:
37575
diff
changeset
|
408 |
else |
5379f41a1322
merge "Sledgehammer_{F,H}OL_Clause", as requested by a FIXME
blanchet
parents:
37575
diff
changeset
|
409 |
(c, T) |> Sign.const_typargs thy) |
5379f41a1322
merge "Sledgehammer_{F,H}OL_Clause", as requested by a FIXME
blanchet
parents:
37575
diff
changeset
|
410 |
|> map simp_type_of |
5379f41a1322
merge "Sledgehammer_{F,H}OL_Clause", as requested by a FIXME
blanchet
parents:
37575
diff
changeset
|
411 |
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
|
412 |
in (c',ts) end |
5379f41a1322
merge "Sledgehammer_{F,H}OL_Clause", as requested by a FIXME
blanchet
parents:
37575
diff
changeset
|
413 |
| combterm_of _ (Free(v, T)) = |
5379f41a1322
merge "Sledgehammer_{F,H}OL_Clause", as requested by a FIXME
blanchet
parents:
37575
diff
changeset
|
414 |
let val (tp,ts) = type_of T |
5379f41a1322
merge "Sledgehammer_{F,H}OL_Clause", as requested by a FIXME
blanchet
parents:
37575
diff
changeset
|
415 |
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
|
416 |
in (v',ts) end |
5379f41a1322
merge "Sledgehammer_{F,H}OL_Clause", as requested by a FIXME
blanchet
parents:
37575
diff
changeset
|
417 |
| combterm_of _ (Var(v, T)) = |
5379f41a1322
merge "Sledgehammer_{F,H}OL_Clause", as requested by a FIXME
blanchet
parents:
37575
diff
changeset
|
418 |
let val (tp,ts) = type_of T |
5379f41a1322
merge "Sledgehammer_{F,H}OL_Clause", as requested by a FIXME
blanchet
parents:
37575
diff
changeset
|
419 |
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
|
420 |
in (v',ts) end |
5379f41a1322
merge "Sledgehammer_{F,H}OL_Clause", as requested by a FIXME
blanchet
parents:
37575
diff
changeset
|
421 |
| combterm_of thy (P $ Q) = |
5379f41a1322
merge "Sledgehammer_{F,H}OL_Clause", as requested by a FIXME
blanchet
parents:
37575
diff
changeset
|
422 |
let val (P', tsP) = combterm_of thy P |
5379f41a1322
merge "Sledgehammer_{F,H}OL_Clause", as requested by a FIXME
blanchet
parents:
37575
diff
changeset
|
423 |
val (Q', tsQ) = combterm_of thy Q |
5379f41a1322
merge "Sledgehammer_{F,H}OL_Clause", as requested by a FIXME
blanchet
parents:
37575
diff
changeset
|
424 |
in (CombApp (P', Q'), union (op =) tsP tsQ) end |
37623
295f3a9b44b6
move functions not needed by Metis out of "Metis_Clauses"
blanchet
parents:
37620
diff
changeset
|
425 |
| combterm_of _ (Abs _) = raise Fail "HOL clause: Abs" |
37577
5379f41a1322
merge "Sledgehammer_{F,H}OL_Clause", as requested by a FIXME
blanchet
parents:
37575
diff
changeset
|
426 |
|
5379f41a1322
merge "Sledgehammer_{F,H}OL_Clause", as requested by a FIXME
blanchet
parents:
37575
diff
changeset
|
427 |
fun predicate_of thy ((@{const Not} $ P), pos) = predicate_of thy (P, not pos) |
5379f41a1322
merge "Sledgehammer_{F,H}OL_Clause", as requested by a FIXME
blanchet
parents:
37575
diff
changeset
|
428 |
| predicate_of thy (t, pos) = (combterm_of thy (Envir.eta_contract t), pos) |
5379f41a1322
merge "Sledgehammer_{F,H}OL_Clause", as requested by a FIXME
blanchet
parents:
37575
diff
changeset
|
429 |
|
5379f41a1322
merge "Sledgehammer_{F,H}OL_Clause", as requested by a FIXME
blanchet
parents:
37575
diff
changeset
|
430 |
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
|
431 |
literals_of_term1 args thy P |
5379f41a1322
merge "Sledgehammer_{F,H}OL_Clause", as requested by a FIXME
blanchet
parents:
37575
diff
changeset
|
432 |
| 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
|
433 |
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
|
434 |
| literals_of_term1 (lits, ts) thy P = |
5379f41a1322
merge "Sledgehammer_{F,H}OL_Clause", as requested by a FIXME
blanchet
parents:
37575
diff
changeset
|
435 |
let val ((pred, ts'), pol) = predicate_of thy (P, true) in |
5379f41a1322
merge "Sledgehammer_{F,H}OL_Clause", as requested by a FIXME
blanchet
parents:
37575
diff
changeset
|
436 |
(Literal (pol, pred) :: lits, union (op =) ts ts') |
5379f41a1322
merge "Sledgehammer_{F,H}OL_Clause", as requested by a FIXME
blanchet
parents:
37575
diff
changeset
|
437 |
end |
5379f41a1322
merge "Sledgehammer_{F,H}OL_Clause", as requested by a FIXME
blanchet
parents:
37575
diff
changeset
|
438 |
val literals_of_term = literals_of_term1 ([], []) |
5379f41a1322
merge "Sledgehammer_{F,H}OL_Clause", as requested by a FIXME
blanchet
parents:
37575
diff
changeset
|
439 |
|
5379f41a1322
merge "Sledgehammer_{F,H}OL_Clause", as requested by a FIXME
blanchet
parents:
37575
diff
changeset
|
440 |
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
|
441 |
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
|
442 |
skolem_infix ^ "g" |
5379f41a1322
merge "Sledgehammer_{F,H}OL_Clause", as requested by a FIXME
blanchet
parents:
37575
diff
changeset
|
443 |
|
5379f41a1322
merge "Sledgehammer_{F,H}OL_Clause", as requested by a FIXME
blanchet
parents:
37575
diff
changeset
|
444 |
fun conceal_skolem_somes i skolem_somes t = |
5379f41a1322
merge "Sledgehammer_{F,H}OL_Clause", as requested by a FIXME
blanchet
parents:
37575
diff
changeset
|
445 |
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
|
446 |
let |
5379f41a1322
merge "Sledgehammer_{F,H}OL_Clause", as requested by a FIXME
blanchet
parents:
37575
diff
changeset
|
447 |
fun aux skolem_somes |
5379f41a1322
merge "Sledgehammer_{F,H}OL_Clause", as requested by a FIXME
blanchet
parents:
37575
diff
changeset
|
448 |
(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
|
449 |
let |
5379f41a1322
merge "Sledgehammer_{F,H}OL_Clause", as requested by a FIXME
blanchet
parents:
37575
diff
changeset
|
450 |
val (skolem_somes, s) = |
5379f41a1322
merge "Sledgehammer_{F,H}OL_Clause", as requested by a FIXME
blanchet
parents:
37575
diff
changeset
|
451 |
if i = ~1 then |
5379f41a1322
merge "Sledgehammer_{F,H}OL_Clause", as requested by a FIXME
blanchet
parents:
37575
diff
changeset
|
452 |
(skolem_somes, @{const_name undefined}) |
5379f41a1322
merge "Sledgehammer_{F,H}OL_Clause", as requested by a FIXME
blanchet
parents:
37575
diff
changeset
|
453 |
else case AList.find (op aconv) skolem_somes t of |
5379f41a1322
merge "Sledgehammer_{F,H}OL_Clause", as requested by a FIXME
blanchet
parents:
37575
diff
changeset
|
454 |
s :: _ => (skolem_somes, s) |
5379f41a1322
merge "Sledgehammer_{F,H}OL_Clause", as requested by a FIXME
blanchet
parents:
37575
diff
changeset
|
455 |
| [] => |
5379f41a1322
merge "Sledgehammer_{F,H}OL_Clause", as requested by a FIXME
blanchet
parents:
37575
diff
changeset
|
456 |
let |
5379f41a1322
merge "Sledgehammer_{F,H}OL_Clause", as requested by a FIXME
blanchet
parents:
37575
diff
changeset
|
457 |
val s = skolem_theory_name ^ "." ^ |
5379f41a1322
merge "Sledgehammer_{F,H}OL_Clause", as requested by a FIXME
blanchet
parents:
37575
diff
changeset
|
458 |
skolem_name i (length skolem_somes) |
5379f41a1322
merge "Sledgehammer_{F,H}OL_Clause", as requested by a FIXME
blanchet
parents:
37575
diff
changeset
|
459 |
(length (Term.add_tvarsT T [])) |
5379f41a1322
merge "Sledgehammer_{F,H}OL_Clause", as requested by a FIXME
blanchet
parents:
37575
diff
changeset
|
460 |
in ((s, t) :: skolem_somes, s) end |
5379f41a1322
merge "Sledgehammer_{F,H}OL_Clause", as requested by a FIXME
blanchet
parents:
37575
diff
changeset
|
461 |
in (skolem_somes, Const (s, T)) end |
5379f41a1322
merge "Sledgehammer_{F,H}OL_Clause", as requested by a FIXME
blanchet
parents:
37575
diff
changeset
|
462 |
| aux skolem_somes (t1 $ t2) = |
5379f41a1322
merge "Sledgehammer_{F,H}OL_Clause", as requested by a FIXME
blanchet
parents:
37575
diff
changeset
|
463 |
let |
5379f41a1322
merge "Sledgehammer_{F,H}OL_Clause", as requested by a FIXME
blanchet
parents:
37575
diff
changeset
|
464 |
val (skolem_somes, t1) = aux skolem_somes t1 |
5379f41a1322
merge "Sledgehammer_{F,H}OL_Clause", as requested by a FIXME
blanchet
parents:
37575
diff
changeset
|
465 |
val (skolem_somes, t2) = aux skolem_somes t2 |
5379f41a1322
merge "Sledgehammer_{F,H}OL_Clause", as requested by a FIXME
blanchet
parents:
37575
diff
changeset
|
466 |
in (skolem_somes, t1 $ t2) end |
5379f41a1322
merge "Sledgehammer_{F,H}OL_Clause", as requested by a FIXME
blanchet
parents:
37575
diff
changeset
|
467 |
| aux skolem_somes (Abs (s, T, t')) = |
5379f41a1322
merge "Sledgehammer_{F,H}OL_Clause", as requested by a FIXME
blanchet
parents:
37575
diff
changeset
|
468 |
let val (skolem_somes, t') = aux skolem_somes t' in |
5379f41a1322
merge "Sledgehammer_{F,H}OL_Clause", as requested by a FIXME
blanchet
parents:
37575
diff
changeset
|
469 |
(skolem_somes, Abs (s, T, t')) |
5379f41a1322
merge "Sledgehammer_{F,H}OL_Clause", as requested by a FIXME
blanchet
parents:
37575
diff
changeset
|
470 |
end |
5379f41a1322
merge "Sledgehammer_{F,H}OL_Clause", as requested by a FIXME
blanchet
parents:
37575
diff
changeset
|
471 |
| aux skolem_somes t = (skolem_somes, t) |
5379f41a1322
merge "Sledgehammer_{F,H}OL_Clause", as requested by a FIXME
blanchet
parents:
37575
diff
changeset
|
472 |
in aux skolem_somes t end |
5379f41a1322
merge "Sledgehammer_{F,H}OL_Clause", as requested by a FIXME
blanchet
parents:
37575
diff
changeset
|
473 |
else |
5379f41a1322
merge "Sledgehammer_{F,H}OL_Clause", as requested by a FIXME
blanchet
parents:
37575
diff
changeset
|
474 |
(skolem_somes, t) |
5379f41a1322
merge "Sledgehammer_{F,H}OL_Clause", as requested by a FIXME
blanchet
parents:
37575
diff
changeset
|
475 |
|
5379f41a1322
merge "Sledgehammer_{F,H}OL_Clause", as requested by a FIXME
blanchet
parents:
37575
diff
changeset
|
476 |
|
5379f41a1322
merge "Sledgehammer_{F,H}OL_Clause", as requested by a FIXME
blanchet
parents:
37575
diff
changeset
|
477 |
(***************************************************************) |
5379f41a1322
merge "Sledgehammer_{F,H}OL_Clause", as requested by a FIXME
blanchet
parents:
37575
diff
changeset
|
478 |
(* 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
|
479 |
(***************************************************************) |
5379f41a1322
merge "Sledgehammer_{F,H}OL_Clause", as requested by a FIXME
blanchet
parents:
37575
diff
changeset
|
480 |
|
5379f41a1322
merge "Sledgehammer_{F,H}OL_Clause", as requested by a FIXME
blanchet
parents:
37575
diff
changeset
|
481 |
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
|
482 |
|
5379f41a1322
merge "Sledgehammer_{F,H}OL_Clause", as requested by a FIXME
blanchet
parents:
37575
diff
changeset
|
483 |
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
|
484 |
|
5379f41a1322
merge "Sledgehammer_{F,H}OL_Clause", as requested by a FIXME
blanchet
parents:
37575
diff
changeset
|
485 |
(*Remove this trivial type class*) |
5379f41a1322
merge "Sledgehammer_{F,H}OL_Clause", as requested by a FIXME
blanchet
parents:
37575
diff
changeset
|
486 |
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
|
487 |
|
5379f41a1322
merge "Sledgehammer_{F,H}OL_Clause", as requested by a FIXME
blanchet
parents:
37575
diff
changeset
|
488 |
fun tfree_classes_of_terms ts = |
5379f41a1322
merge "Sledgehammer_{F,H}OL_Clause", as requested by a FIXME
blanchet
parents:
37575
diff
changeset
|
489 |
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
|
490 |
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
|
491 |
|
5379f41a1322
merge "Sledgehammer_{F,H}OL_Clause", as requested by a FIXME
blanchet
parents:
37575
diff
changeset
|
492 |
fun tvar_classes_of_terms ts = |
5379f41a1322
merge "Sledgehammer_{F,H}OL_Clause", as requested by a FIXME
blanchet
parents:
37575
diff
changeset
|
493 |
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
|
494 |
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
|
495 |
|
5379f41a1322
merge "Sledgehammer_{F,H}OL_Clause", as requested by a FIXME
blanchet
parents:
37575
diff
changeset
|
496 |
(*fold type constructors*) |
5379f41a1322
merge "Sledgehammer_{F,H}OL_Clause", as requested by a FIXME
blanchet
parents:
37575
diff
changeset
|
497 |
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
|
498 |
| fold_type_consts _ _ x = x; |
5379f41a1322
merge "Sledgehammer_{F,H}OL_Clause", as requested by a FIXME
blanchet
parents:
37575
diff
changeset
|
499 |
|
5379f41a1322
merge "Sledgehammer_{F,H}OL_Clause", as requested by a FIXME
blanchet
parents:
37575
diff
changeset
|
500 |
(*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
|
501 |
fun add_type_consts_in_term thy = |
5379f41a1322
merge "Sledgehammer_{F,H}OL_Clause", as requested by a FIXME
blanchet
parents:
37575
diff
changeset
|
502 |
let |
5379f41a1322
merge "Sledgehammer_{F,H}OL_Clause", as requested by a FIXME
blanchet
parents:
37575
diff
changeset
|
503 |
val const_typargs = Sign.const_typargs thy |
5379f41a1322
merge "Sledgehammer_{F,H}OL_Clause", as requested by a FIXME
blanchet
parents:
37575
diff
changeset
|
504 |
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
|
505 |
| aux (Abs (_, _, u)) = aux u |
5379f41a1322
merge "Sledgehammer_{F,H}OL_Clause", as requested by a FIXME
blanchet
parents:
37575
diff
changeset
|
506 |
| aux (Const (@{const_name skolem_id}, _) $ _) = I |
5379f41a1322
merge "Sledgehammer_{F,H}OL_Clause", as requested by a FIXME
blanchet
parents:
37575
diff
changeset
|
507 |
| aux (t $ u) = aux t #> aux u |
5379f41a1322
merge "Sledgehammer_{F,H}OL_Clause", as requested by a FIXME
blanchet
parents:
37575
diff
changeset
|
508 |
| aux _ = I |
5379f41a1322
merge "Sledgehammer_{F,H}OL_Clause", as requested by a FIXME
blanchet
parents:
37575
diff
changeset
|
509 |
in aux end |
5379f41a1322
merge "Sledgehammer_{F,H}OL_Clause", as requested by a FIXME
blanchet
parents:
37575
diff
changeset
|
510 |
|
5379f41a1322
merge "Sledgehammer_{F,H}OL_Clause", as requested by a FIXME
blanchet
parents:
37575
diff
changeset
|
511 |
fun type_consts_of_terms thy ts = |
5379f41a1322
merge "Sledgehammer_{F,H}OL_Clause", as requested by a FIXME
blanchet
parents:
37575
diff
changeset
|
512 |
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
|
513 |
|
15347 | 514 |
end; |