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