blanchet@37578
|
1 |
(* Title: HOL/Tools/Sledgehammer/metis_clauses.ML
|
wenzelm@33319
|
2 |
Author: Jia Meng, Cambridge University Computer Laboratory
|
blanchet@36393
|
3 |
Author: Jasmin Blanchette, TU Muenchen
|
paulson@15347
|
4 |
|
wenzelm@33319
|
5 |
Storing/printing FOL clauses and arity clauses. Typed equality is
|
wenzelm@33319
|
6 |
treated differently.
|
paulson@15347
|
7 |
*)
|
paulson@15347
|
8 |
|
blanchet@37578
|
9 |
signature METIS_CLAUSES =
|
wenzelm@24310
|
10 |
sig
|
blanchet@37577
|
11 |
type name = string * string
|
blanchet@37577
|
12 |
datatype kind = Axiom | Conjecture
|
blanchet@37577
|
13 |
datatype type_literal =
|
blanchet@37577
|
14 |
TyLitVar of string * name |
|
blanchet@37577
|
15 |
TyLitFree of string * name
|
blanchet@37577
|
16 |
datatype arLit =
|
blanchet@37577
|
17 |
TConsLit of class * string * string list
|
blanchet@37577
|
18 |
| TVarLit of class * string
|
blanchet@37577
|
19 |
datatype arity_clause = ArityClause of
|
blanchet@37577
|
20 |
{axiom_name: string, conclLit: arLit, premLits: arLit list}
|
blanchet@37577
|
21 |
datatype classrel_clause = ClassrelClause of
|
blanchet@37577
|
22 |
{axiom_name: string, subclass: class, superclass: class}
|
blanchet@37577
|
23 |
datatype combtyp =
|
blanchet@37577
|
24 |
TyVar of name |
|
blanchet@37577
|
25 |
TyFree of name |
|
blanchet@37577
|
26 |
TyConstr of name * combtyp list
|
blanchet@37577
|
27 |
datatype combterm =
|
blanchet@37577
|
28 |
CombConst of name * combtyp * combtyp list (* Const and Free *) |
|
blanchet@37577
|
29 |
CombVar of name * combtyp |
|
blanchet@37577
|
30 |
CombApp of combterm * combterm
|
blanchet@37577
|
31 |
datatype literal = Literal of bool * combterm
|
blanchet@37577
|
32 |
datatype hol_clause =
|
blanchet@37577
|
33 |
HOLClause of {clause_id: int, axiom_name: string, th: thm, kind: kind,
|
blanchet@37577
|
34 |
literals: literal list, ctypes_sorts: typ list}
|
blanchet@37577
|
35 |
|
blanchet@37509
|
36 |
val type_wrapper_name : string
|
wenzelm@24310
|
37 |
val schematic_var_prefix: string
|
wenzelm@24310
|
38 |
val fixed_var_prefix: string
|
wenzelm@24310
|
39 |
val tvar_prefix: string
|
wenzelm@24310
|
40 |
val tfree_prefix: string
|
wenzelm@24310
|
41 |
val const_prefix: string
|
wenzelm@24310
|
42 |
val tconst_prefix: string
|
wenzelm@24310
|
43 |
val class_prefix: string
|
wenzelm@24310
|
44 |
val union_all: ''a list list -> ''a list
|
blanchet@37572
|
45 |
val invert_const: string -> string
|
wenzelm@24310
|
46 |
val ascii_of: string -> string
|
wenzelm@24310
|
47 |
val undo_ascii_of: string -> string
|
blanchet@37572
|
48 |
val strip_prefix: string -> string -> string option
|
wenzelm@24310
|
49 |
val make_schematic_var : string * int -> string
|
wenzelm@24310
|
50 |
val make_fixed_var : string -> string
|
wenzelm@24310
|
51 |
val make_schematic_type_var : string * int -> string
|
wenzelm@24310
|
52 |
val make_fixed_type_var : string -> string
|
blanchet@37498
|
53 |
val make_fixed_const : string -> string
|
blanchet@37498
|
54 |
val make_fixed_type_const : string -> string
|
wenzelm@24310
|
55 |
val make_type_class : string -> string
|
blanchet@37618
|
56 |
val skolem_theory_name: string
|
blanchet@37618
|
57 |
val skolem_prefix: string
|
blanchet@37618
|
58 |
val skolem_infix: string
|
blanchet@37618
|
59 |
val is_skolem_const_name: string -> bool
|
blanchet@37618
|
60 |
val num_type_args: theory -> string -> int
|
blanchet@36959
|
61 |
val type_literals_for_types : typ list -> type_literal list
|
blanchet@35865
|
62 |
val make_classrel_clauses: theory -> class list -> class list -> classrel_clause list
|
blanchet@35865
|
63 |
val make_arity_clauses: theory -> string list -> class list -> class list * arity_clause list
|
blanchet@37577
|
64 |
val type_of_combterm : combterm -> combtyp
|
blanchet@37577
|
65 |
val strip_combterm_comb : combterm -> combterm * combterm list
|
blanchet@37577
|
66 |
val literals_of_term : theory -> term -> literal list * typ list
|
blanchet@37625
|
67 |
val conceal_skolem_terms :
|
blanchet@37577
|
68 |
int -> (string * term) list -> term -> (string * term) list * term
|
blanchet@37632
|
69 |
val reveal_skolem_terms : (string * term) list -> term -> term
|
blanchet@37577
|
70 |
val tfree_classes_of_terms : term list -> string list
|
blanchet@37577
|
71 |
val tvar_classes_of_terms : term list -> string list
|
blanchet@37577
|
72 |
val type_consts_of_terms : theory -> term list -> string list
|
wenzelm@24310
|
73 |
end
|
paulson@15347
|
74 |
|
blanchet@37578
|
75 |
structure Metis_Clauses : METIS_CLAUSES =
|
paulson@15347
|
76 |
struct
|
paulson@15347
|
77 |
|
blanchet@37577
|
78 |
open Clausifier
|
blanchet@37577
|
79 |
|
blanchet@37509
|
80 |
val type_wrapper_name = "ti"
|
blanchet@37509
|
81 |
|
paulson@15347
|
82 |
val schematic_var_prefix = "V_";
|
paulson@15347
|
83 |
val fixed_var_prefix = "v_";
|
paulson@15347
|
84 |
|
paulson@17230
|
85 |
val tvar_prefix = "T_";
|
paulson@17230
|
86 |
val tfree_prefix = "t_";
|
paulson@15347
|
87 |
|
blanchet@37509
|
88 |
val classrel_clause_prefix = "clsrel_";
|
paulson@15347
|
89 |
|
paulson@17230
|
90 |
val const_prefix = "c_";
|
wenzelm@24310
|
91 |
val tconst_prefix = "tc_";
|
wenzelm@24310
|
92 |
val class_prefix = "class_";
|
paulson@15347
|
93 |
|
blanchet@36218
|
94 |
fun union_all xss = fold (union (op =)) xss []
|
paulson@17775
|
95 |
|
blanchet@36489
|
96 |
(* Readable names for the more common symbolic functions. Do not mess with the
|
blanchet@37454
|
97 |
last nine entries of the table unless you know what you are doing. *)
|
paulson@15347
|
98 |
val const_trans_table =
|
blanchet@35865
|
99 |
Symtab.make [(@{const_name "op ="}, "equal"),
|
blanchet@35865
|
100 |
(@{const_name "op &"}, "and"),
|
blanchet@35865
|
101 |
(@{const_name "op |"}, "or"),
|
blanchet@35865
|
102 |
(@{const_name "op -->"}, "implies"),
|
blanchet@36489
|
103 |
(@{const_name "op :"}, "in"),
|
blanchet@36489
|
104 |
(@{const_name fequal}, "fequal"),
|
blanchet@36489
|
105 |
(@{const_name COMBI}, "COMBI"),
|
blanchet@36489
|
106 |
(@{const_name COMBK}, "COMBK"),
|
blanchet@36489
|
107 |
(@{const_name COMBB}, "COMBB"),
|
blanchet@36489
|
108 |
(@{const_name COMBC}, "COMBC"),
|
blanchet@37454
|
109 |
(@{const_name COMBS}, "COMBS"),
|
blanchet@37454
|
110 |
(@{const_name True}, "True"),
|
blanchet@37454
|
111 |
(@{const_name False}, "False"),
|
blanchet@37572
|
112 |
(@{const_name If}, "If"),
|
blanchet@37572
|
113 |
(@{type_name "*"}, "prod"),
|
blanchet@37572
|
114 |
(@{type_name "+"}, "sum")]
|
paulson@15347
|
115 |
|
blanchet@37572
|
116 |
(* Invert the table of translations between Isabelle and ATPs. *)
|
blanchet@37572
|
117 |
val const_trans_table_inv =
|
blanchet@37572
|
118 |
Symtab.update ("fequal", @{const_name "op ="})
|
blanchet@37572
|
119 |
(Symtab.make (map swap (Symtab.dest const_trans_table)))
|
blanchet@37572
|
120 |
|
blanchet@37572
|
121 |
val invert_const = perhaps (Symtab.lookup const_trans_table_inv)
|
paulson@15347
|
122 |
|
paulson@15610
|
123 |
(*Escaping of special characters.
|
paulson@15610
|
124 |
Alphanumeric characters are left unchanged.
|
paulson@15610
|
125 |
The character _ goes to __
|
paulson@15610
|
126 |
Characters in the range ASCII space to / go to _A to _P, respectively.
|
paulson@24183
|
127 |
Other printing characters go to _nnn where nnn is the decimal ASCII code.*)
|
paulson@24183
|
128 |
val A_minus_space = Char.ord #"A" - Char.ord #" ";
|
paulson@15610
|
129 |
|
paulson@24183
|
130 |
fun stringN_of_int 0 _ = ""
|
paulson@24183
|
131 |
| stringN_of_int k n = stringN_of_int (k-1) (n div 10) ^ Int.toString (n mod 10);
|
paulson@15610
|
132 |
|
paulson@15347
|
133 |
fun ascii_of_c c =
|
paulson@15610
|
134 |
if Char.isAlphaNum c then String.str c
|
paulson@15610
|
135 |
else if c = #"_" then "__"
|
wenzelm@24310
|
136 |
else if #" " <= c andalso c <= #"/"
|
paulson@15610
|
137 |
then "_" ^ String.str (Char.chr (Char.ord c + A_minus_space))
|
wenzelm@24310
|
138 |
else if Char.isPrint c
|
paulson@24183
|
139 |
then ("_" ^ stringN_of_int 3 (Char.ord c)) (*fixed width, in case more digits follow*)
|
paulson@15610
|
140 |
else ""
|
paulson@15347
|
141 |
|
paulson@15610
|
142 |
val ascii_of = String.translate ascii_of_c;
|
paulson@15610
|
143 |
|
paulson@24183
|
144 |
(** Remove ASCII armouring from names in proof files **)
|
paulson@24183
|
145 |
|
paulson@24183
|
146 |
(*We don't raise error exceptions because this code can run inside the watcher.
|
paulson@24183
|
147 |
Also, the errors are "impossible" (hah!)*)
|
paulson@24183
|
148 |
fun undo_ascii_aux rcs [] = String.implode(rev rcs)
|
paulson@24183
|
149 |
| undo_ascii_aux rcs [#"_"] = undo_ascii_aux (#"_"::rcs) [] (*ERROR*)
|
paulson@24183
|
150 |
(*Three types of _ escapes: __, _A to _P, _nnn*)
|
paulson@24183
|
151 |
| undo_ascii_aux rcs (#"_" :: #"_" :: cs) = undo_ascii_aux (#"_"::rcs) cs
|
wenzelm@24310
|
152 |
| undo_ascii_aux rcs (#"_" :: c :: cs) =
|
paulson@24183
|
153 |
if #"A" <= c andalso c<= #"P" (*translation of #" " to #"/"*)
|
paulson@24183
|
154 |
then undo_ascii_aux (Char.chr(Char.ord c - A_minus_space) :: rcs) cs
|
wenzelm@24310
|
155 |
else
|
paulson@24183
|
156 |
let val digits = List.take (c::cs, 3) handle Subscript => []
|
wenzelm@24310
|
157 |
in
|
paulson@24183
|
158 |
case Int.fromString (String.implode digits) of
|
paulson@24183
|
159 |
NONE => undo_ascii_aux (c:: #"_"::rcs) cs (*ERROR*)
|
paulson@24183
|
160 |
| SOME n => undo_ascii_aux (Char.chr n :: rcs) (List.drop (cs, 2))
|
paulson@24183
|
161 |
end
|
paulson@24183
|
162 |
| undo_ascii_aux rcs (c::cs) = undo_ascii_aux (c::rcs) cs;
|
paulson@24183
|
163 |
|
paulson@24183
|
164 |
val undo_ascii_of = undo_ascii_aux [] o String.explode;
|
paulson@15347
|
165 |
|
blanchet@37572
|
166 |
(* If string s has the prefix s1, return the result of deleting it,
|
blanchet@37572
|
167 |
un-ASCII'd. *)
|
blanchet@37572
|
168 |
fun strip_prefix s1 s =
|
blanchet@37572
|
169 |
if String.isPrefix s1 s then
|
blanchet@37572
|
170 |
SOME (undo_ascii_of (String.extract (s, size s1, NONE)))
|
blanchet@37572
|
171 |
else
|
blanchet@37572
|
172 |
NONE
|
blanchet@37572
|
173 |
|
paulson@16925
|
174 |
(*Remove the initial ' character from a type variable, if it is present*)
|
paulson@16925
|
175 |
fun trim_type_var s =
|
paulson@16925
|
176 |
if s <> "" andalso String.sub(s,0) = #"'" then String.extract(s,1,NONE)
|
paulson@16925
|
177 |
else error ("trim_type: Malformed type variable encountered: " ^ s);
|
paulson@16925
|
178 |
|
paulson@16903
|
179 |
fun ascii_of_indexname (v,0) = ascii_of v
|
paulson@17525
|
180 |
| ascii_of_indexname (v,i) = ascii_of v ^ "_" ^ Int.toString i;
|
paulson@15347
|
181 |
|
paulson@17230
|
182 |
fun make_schematic_var v = schematic_var_prefix ^ (ascii_of_indexname v);
|
paulson@15347
|
183 |
fun make_fixed_var x = fixed_var_prefix ^ (ascii_of x);
|
paulson@15347
|
184 |
|
wenzelm@24310
|
185 |
fun make_schematic_type_var (x,i) =
|
paulson@16925
|
186 |
tvar_prefix ^ (ascii_of_indexname (trim_type_var x,i));
|
paulson@16925
|
187 |
fun make_fixed_type_var x = tfree_prefix ^ (ascii_of (trim_type_var x));
|
paulson@15347
|
188 |
|
blanchet@37498
|
189 |
fun lookup_const c =
|
blanchet@37498
|
190 |
case Symtab.lookup const_trans_table c of
|
blanchet@37498
|
191 |
SOME c' => c'
|
blanchet@37498
|
192 |
| NONE => ascii_of c
|
blanchet@36378
|
193 |
|
blanchet@36062
|
194 |
(* "op =" MUST BE "equal" because it's built into ATPs. *)
|
blanchet@37498
|
195 |
fun make_fixed_const @{const_name "op ="} = "equal"
|
blanchet@37498
|
196 |
| make_fixed_const c = const_prefix ^ lookup_const c
|
paulson@18411
|
197 |
|
blanchet@37572
|
198 |
fun make_fixed_type_const c = tconst_prefix ^ lookup_const c
|
quigley@17150
|
199 |
|
wenzelm@17261
|
200 |
fun make_type_class clas = class_prefix ^ ascii_of clas;
|
quigley@17150
|
201 |
|
blanchet@37618
|
202 |
val skolem_theory_name = "Sledgehammer" ^ Long_Name.separator ^ "Sko"
|
blanchet@37618
|
203 |
val skolem_prefix = "sko_"
|
blanchet@37618
|
204 |
val skolem_infix = "$"
|
blanchet@37618
|
205 |
|
blanchet@37618
|
206 |
(* Hack: Could return false positives (e.g., a user happens to declare a
|
blanchet@37618
|
207 |
constant called "SomeTheory.sko_means_shoe_in_$wedish". *)
|
blanchet@37618
|
208 |
val is_skolem_const_name =
|
blanchet@37618
|
209 |
Long_Name.base_name
|
blanchet@37618
|
210 |
#> String.isPrefix skolem_prefix andf String.isSubstring skolem_infix
|
blanchet@37618
|
211 |
|
blanchet@37618
|
212 |
(* The number of type arguments of a constant, zero if it's monomorphic. For
|
blanchet@37618
|
213 |
(instances of) Skolem pseudoconstants, this information is encoded in the
|
blanchet@37618
|
214 |
constant name. *)
|
blanchet@37618
|
215 |
fun num_type_args thy s =
|
blanchet@37618
|
216 |
if String.isPrefix skolem_theory_name s then
|
blanchet@37618
|
217 |
s |> unprefix skolem_theory_name
|
blanchet@37618
|
218 |
|> space_explode skolem_infix |> hd
|
blanchet@37618
|
219 |
|> space_explode "_" |> List.last |> Int.fromString |> the
|
blanchet@37618
|
220 |
else
|
blanchet@37618
|
221 |
(s, Sign.the_const_type thy s) |> Sign.const_typargs thy |> length
|
quigley@17150
|
222 |
|
blanchet@37624
|
223 |
(**** Definitions and functions for FOL clauses for TPTP format output ****)
|
blanchet@37624
|
224 |
|
blanchet@36169
|
225 |
type name = string * string
|
paulson@15347
|
226 |
|
blanchet@37577
|
227 |
datatype kind = Axiom | Conjecture
|
paulson@23385
|
228 |
|
paulson@15347
|
229 |
(**** Isabelle FOL clauses ****)
|
paulson@15347
|
230 |
|
blanchet@36554
|
231 |
(* The first component is the type class; the second is a TVar or TFree. *)
|
blanchet@36554
|
232 |
datatype type_literal =
|
blanchet@36554
|
233 |
TyLitVar of string * name |
|
blanchet@36554
|
234 |
TyLitFree of string * name
|
paulson@15347
|
235 |
|
paulson@17404
|
236 |
exception CLAUSE of string * term;
|
paulson@15347
|
237 |
|
wenzelm@24310
|
238 |
(*Make literals for sorted type variables*)
|
paulson@24940
|
239 |
fun sorts_on_typs_aux (_, []) = []
|
paulson@24940
|
240 |
| sorts_on_typs_aux ((x,i), s::ss) =
|
paulson@24940
|
241 |
let val sorts = sorts_on_typs_aux ((x,i), ss)
|
paulson@22643
|
242 |
in
|
paulson@22643
|
243 |
if s = "HOL.type" then sorts
|
blanchet@36554
|
244 |
else if i = ~1 then TyLitFree (make_type_class s, `make_fixed_type_var x) :: sorts
|
blanchet@36554
|
245 |
else TyLitVar (make_type_class s, (make_schematic_type_var (x,i), x)) :: sorts
|
paulson@22643
|
246 |
end;
|
quigley@17150
|
247 |
|
paulson@24940
|
248 |
fun sorts_on_typs (TFree (a,s)) = sorts_on_typs_aux ((a,~1),s)
|
paulson@24940
|
249 |
| sorts_on_typs (TVar (v,s)) = sorts_on_typs_aux (v,s);
|
paulson@24940
|
250 |
|
paulson@24937
|
251 |
(*Given a list of sorted type variables, return a list of type literals.*)
|
blanchet@36959
|
252 |
fun type_literals_for_types Ts =
|
blanchet@36959
|
253 |
fold (union (op =)) (map sorts_on_typs Ts) []
|
mengj@20015
|
254 |
|
mengj@20015
|
255 |
(** make axiom and conjecture clauses. **)
|
mengj@20015
|
256 |
|
paulson@15347
|
257 |
(**** Isabelle arities ****)
|
paulson@15347
|
258 |
|
wenzelm@24310
|
259 |
datatype arLit = TConsLit of class * string * string list
|
paulson@22643
|
260 |
| TVarLit of class * string;
|
wenzelm@24310
|
261 |
|
blanchet@35865
|
262 |
datatype arity_clause =
|
blanchet@37500
|
263 |
ArityClause of {axiom_name: string, conclLit: arLit, premLits: arLit list}
|
paulson@15347
|
264 |
|
paulson@15347
|
265 |
|
paulson@18798
|
266 |
fun gen_TVars 0 = []
|
paulson@18798
|
267 |
| gen_TVars n = ("T_" ^ Int.toString n) :: gen_TVars (n-1);
|
paulson@15347
|
268 |
|
paulson@18411
|
269 |
fun pack_sort(_,[]) = []
|
paulson@18411
|
270 |
| pack_sort(tvar, "HOL.type"::srt) = pack_sort(tvar, srt) (*IGNORE sort "type"*)
|
paulson@22643
|
271 |
| pack_sort(tvar, cls::srt) = (cls, tvar) :: pack_sort(tvar, srt);
|
wenzelm@24310
|
272 |
|
paulson@18411
|
273 |
(*Arity of type constructor tcon :: (arg1,...,argN)res*)
|
blanchet@37498
|
274 |
fun make_axiom_arity_clause (tcons, axiom_name, (cls,args)) =
|
paulson@21560
|
275 |
let val tvars = gen_TVars (length args)
|
paulson@17845
|
276 |
val tvars_srts = ListPair.zip (tvars,args)
|
paulson@17845
|
277 |
in
|
blanchet@37498
|
278 |
ArityClause {axiom_name = axiom_name,
|
blanchet@37498
|
279 |
conclLit = TConsLit (cls, make_fixed_type_const tcons, tvars),
|
blanchet@37498
|
280 |
premLits = map TVarLit (union_all(map pack_sort tvars_srts))}
|
paulson@17845
|
281 |
end;
|
paulson@15347
|
282 |
|
paulson@15347
|
283 |
|
paulson@15347
|
284 |
(**** Isabelle class relations ****)
|
paulson@15347
|
285 |
|
blanchet@35865
|
286 |
datatype classrel_clause =
|
blanchet@37500
|
287 |
ClassrelClause of {axiom_name: string, subclass: class, superclass: class}
|
wenzelm@24310
|
288 |
|
paulson@21290
|
289 |
(*Generate all pairs (sub,super) such that sub is a proper subclass of super in theory thy.*)
|
blanchet@37498
|
290 |
fun class_pairs _ [] _ = []
|
paulson@21432
|
291 |
| class_pairs thy subs supers =
|
blanchet@36218
|
292 |
let
|
blanchet@36218
|
293 |
val class_less = Sorts.class_less (Sign.classes_of thy)
|
blanchet@36218
|
294 |
fun add_super sub super = class_less (sub, super) ? cons (sub, super)
|
blanchet@36218
|
295 |
fun add_supers sub = fold (add_super sub) supers
|
blanchet@36218
|
296 |
in fold add_supers subs [] end
|
paulson@15347
|
297 |
|
blanchet@35865
|
298 |
fun make_classrel_clause (sub,super) =
|
blanchet@37509
|
299 |
ClassrelClause {axiom_name = classrel_clause_prefix ^ ascii_of sub ^ "_" ^
|
blanchet@37509
|
300 |
ascii_of super,
|
wenzelm@24310
|
301 |
subclass = make_type_class sub,
|
paulson@21290
|
302 |
superclass = make_type_class super};
|
paulson@15347
|
303 |
|
paulson@21290
|
304 |
fun make_classrel_clauses thy subs supers =
|
blanchet@35865
|
305 |
map make_classrel_clause (class_pairs thy subs supers);
|
paulson@18868
|
306 |
|
paulson@18868
|
307 |
|
paulson@18868
|
308 |
(** Isabelle arities **)
|
paulson@17845
|
309 |
|
blanchet@37498
|
310 |
fun arity_clause _ _ (_, []) = []
|
blanchet@37498
|
311 |
| arity_clause seen n (tcons, ("HOL.type",_)::ars) = (*ignore*)
|
blanchet@37498
|
312 |
arity_clause seen n (tcons,ars)
|
blanchet@37498
|
313 |
| arity_clause seen n (tcons, (ar as (class,_)) :: ars) =
|
haftmann@36677
|
314 |
if member (op =) seen class then (*multiple arities for the same tycon, class pair*)
|
blanchet@37572
|
315 |
make_axiom_arity_clause (tcons, lookup_const tcons ^ "_" ^ class ^ "_" ^ Int.toString n, ar) ::
|
blanchet@37498
|
316 |
arity_clause seen (n+1) (tcons,ars)
|
paulson@21373
|
317 |
else
|
blanchet@37572
|
318 |
make_axiom_arity_clause (tcons, lookup_const tcons ^ "_" ^ class, ar) ::
|
blanchet@37498
|
319 |
arity_clause (class::seen) n (tcons,ars)
|
paulson@17845
|
320 |
|
blanchet@37498
|
321 |
fun multi_arity_clause [] = []
|
blanchet@37498
|
322 |
| multi_arity_clause ((tcons, ars) :: tc_arlists) =
|
blanchet@37498
|
323 |
arity_clause [] 1 (tcons, ars) @ multi_arity_clause tc_arlists
|
paulson@17845
|
324 |
|
paulson@22643
|
325 |
(*Generate all pairs (tycon,class,sorts) such that tycon belongs to class in theory thy
|
paulson@22643
|
326 |
provided its arguments have the corresponding sorts.*)
|
paulson@21373
|
327 |
fun type_class_pairs thy tycons classes =
|
paulson@21373
|
328 |
let val alg = Sign.classes_of thy
|
blanchet@36218
|
329 |
fun domain_sorts tycon = Sorts.mg_domain alg tycon o single
|
blanchet@36218
|
330 |
fun add_class tycon class =
|
blanchet@36218
|
331 |
cons (class, domain_sorts tycon class)
|
blanchet@36218
|
332 |
handle Sorts.CLASS_ERROR _ => I
|
blanchet@36218
|
333 |
fun try_classes tycon = (tycon, fold (add_class tycon) classes [])
|
paulson@21373
|
334 |
in map try_classes tycons end;
|
paulson@21373
|
335 |
|
paulson@22643
|
336 |
(*Proving one (tycon, class) membership may require proving others, so iterate.*)
|
blanchet@37498
|
337 |
fun iter_type_class_pairs _ _ [] = ([], [])
|
paulson@22643
|
338 |
| iter_type_class_pairs thy tycons classes =
|
paulson@22643
|
339 |
let val cpairs = type_class_pairs thy tycons classes
|
haftmann@33040
|
340 |
val newclasses = union_all (union_all (union_all (map (map #2 o #2) cpairs)))
|
haftmann@33040
|
341 |
|> subtract (op =) classes |> subtract (op =) HOLogic.typeS
|
wenzelm@24310
|
342 |
val (classes', cpairs') = iter_type_class_pairs thy tycons newclasses
|
haftmann@33042
|
343 |
in (union (op =) classes' classes, union (op =) cpairs' cpairs) end;
|
wenzelm@24310
|
344 |
|
blanchet@37498
|
345 |
fun make_arity_clauses thy tycons classes =
|
wenzelm@24310
|
346 |
let val (classes', cpairs) = iter_type_class_pairs thy tycons classes
|
blanchet@37498
|
347 |
in (classes', multi_arity_clause cpairs) end;
|
paulson@18863
|
348 |
|
blanchet@37577
|
349 |
datatype combtyp =
|
blanchet@37577
|
350 |
TyVar of name |
|
blanchet@37577
|
351 |
TyFree of name |
|
blanchet@37577
|
352 |
TyConstr of name * combtyp list
|
blanchet@37577
|
353 |
|
blanchet@37577
|
354 |
datatype combterm =
|
blanchet@37577
|
355 |
CombConst of name * combtyp * combtyp list (* Const and Free *) |
|
blanchet@37577
|
356 |
CombVar of name * combtyp |
|
blanchet@37577
|
357 |
CombApp of combterm * combterm
|
blanchet@37577
|
358 |
|
blanchet@37577
|
359 |
datatype literal = Literal of bool * combterm
|
blanchet@37577
|
360 |
|
blanchet@37577
|
361 |
datatype hol_clause =
|
blanchet@37577
|
362 |
HOLClause of {clause_id: int, axiom_name: string, th: thm, kind: kind,
|
blanchet@37577
|
363 |
literals: literal list, ctypes_sorts: typ list}
|
blanchet@37577
|
364 |
|
blanchet@37577
|
365 |
(*********************************************************************)
|
blanchet@37577
|
366 |
(* convert a clause with type Term.term to a clause with type clause *)
|
blanchet@37577
|
367 |
(*********************************************************************)
|
blanchet@37577
|
368 |
|
blanchet@37577
|
369 |
(*Result of a function type; no need to check that the argument type matches.*)
|
blanchet@37577
|
370 |
fun result_type (TyConstr (_, [_, tp2])) = tp2
|
blanchet@37577
|
371 |
| result_type _ = raise Fail "non-function type"
|
blanchet@37577
|
372 |
|
blanchet@37577
|
373 |
fun type_of_combterm (CombConst (_, tp, _)) = tp
|
blanchet@37577
|
374 |
| type_of_combterm (CombVar (_, tp)) = tp
|
blanchet@37577
|
375 |
| type_of_combterm (CombApp (t1, _)) = result_type (type_of_combterm t1)
|
blanchet@37577
|
376 |
|
blanchet@37577
|
377 |
(*gets the head of a combinator application, along with the list of arguments*)
|
blanchet@37577
|
378 |
fun strip_combterm_comb u =
|
blanchet@37577
|
379 |
let fun stripc (CombApp(t,u), ts) = stripc (t, u::ts)
|
blanchet@37577
|
380 |
| stripc x = x
|
blanchet@37577
|
381 |
in stripc(u,[]) end
|
blanchet@37577
|
382 |
|
blanchet@37577
|
383 |
fun type_of (Type (a, Ts)) =
|
blanchet@37577
|
384 |
let val (folTypes,ts) = types_of Ts in
|
blanchet@37577
|
385 |
(TyConstr (`make_fixed_type_const a, folTypes), ts)
|
blanchet@37577
|
386 |
end
|
blanchet@37577
|
387 |
| type_of (tp as TFree (a, _)) = (TyFree (`make_fixed_type_var a), [tp])
|
blanchet@37577
|
388 |
| type_of (tp as TVar (x, _)) =
|
blanchet@37577
|
389 |
(TyVar (make_schematic_type_var x, string_of_indexname x), [tp])
|
blanchet@37577
|
390 |
and types_of Ts =
|
blanchet@37577
|
391 |
let val (folTyps, ts) = ListPair.unzip (map type_of Ts) in
|
blanchet@37577
|
392 |
(folTyps, union_all ts)
|
blanchet@37577
|
393 |
end
|
blanchet@37577
|
394 |
|
blanchet@37577
|
395 |
(* same as above, but no gathering of sort information *)
|
blanchet@37577
|
396 |
fun simp_type_of (Type (a, Ts)) =
|
blanchet@37577
|
397 |
TyConstr (`make_fixed_type_const a, map simp_type_of Ts)
|
blanchet@37577
|
398 |
| simp_type_of (TFree (a, _)) = TyFree (`make_fixed_type_var a)
|
blanchet@37577
|
399 |
| simp_type_of (TVar (x, _)) =
|
blanchet@37577
|
400 |
TyVar (make_schematic_type_var x, string_of_indexname x)
|
blanchet@37577
|
401 |
|
blanchet@37577
|
402 |
(* convert a Term.term (with combinators) into a combterm, also accummulate sort info *)
|
blanchet@37577
|
403 |
fun combterm_of thy (Const (c, T)) =
|
blanchet@37577
|
404 |
let
|
blanchet@37577
|
405 |
val (tp, ts) = type_of T
|
blanchet@37577
|
406 |
val tvar_list =
|
blanchet@37577
|
407 |
(if String.isPrefix skolem_theory_name c then
|
blanchet@37577
|
408 |
[] |> Term.add_tvarsT T |> map TVar
|
blanchet@37577
|
409 |
else
|
blanchet@37577
|
410 |
(c, T) |> Sign.const_typargs thy)
|
blanchet@37577
|
411 |
|> map simp_type_of
|
blanchet@37577
|
412 |
val c' = CombConst (`make_fixed_const c, tp, tvar_list)
|
blanchet@37577
|
413 |
in (c',ts) end
|
blanchet@37577
|
414 |
| combterm_of _ (Free(v, T)) =
|
blanchet@37577
|
415 |
let val (tp,ts) = type_of T
|
blanchet@37577
|
416 |
val v' = CombConst (`make_fixed_var v, tp, [])
|
blanchet@37577
|
417 |
in (v',ts) end
|
blanchet@37577
|
418 |
| combterm_of _ (Var(v, T)) =
|
blanchet@37577
|
419 |
let val (tp,ts) = type_of T
|
blanchet@37577
|
420 |
val v' = CombVar ((make_schematic_var v, string_of_indexname v), tp)
|
blanchet@37577
|
421 |
in (v',ts) end
|
blanchet@37577
|
422 |
| combterm_of thy (P $ Q) =
|
blanchet@37577
|
423 |
let val (P', tsP) = combterm_of thy P
|
blanchet@37577
|
424 |
val (Q', tsQ) = combterm_of thy Q
|
blanchet@37577
|
425 |
in (CombApp (P', Q'), union (op =) tsP tsQ) end
|
blanchet@37623
|
426 |
| combterm_of _ (Abs _) = raise Fail "HOL clause: Abs"
|
blanchet@37577
|
427 |
|
blanchet@37577
|
428 |
fun predicate_of thy ((@{const Not} $ P), pos) = predicate_of thy (P, not pos)
|
blanchet@37577
|
429 |
| predicate_of thy (t, pos) = (combterm_of thy (Envir.eta_contract t), pos)
|
blanchet@37577
|
430 |
|
blanchet@37577
|
431 |
fun literals_of_term1 args thy (@{const Trueprop} $ P) =
|
blanchet@37577
|
432 |
literals_of_term1 args thy P
|
blanchet@37577
|
433 |
| literals_of_term1 args thy (@{const "op |"} $ P $ Q) =
|
blanchet@37577
|
434 |
literals_of_term1 (literals_of_term1 args thy P) thy Q
|
blanchet@37577
|
435 |
| literals_of_term1 (lits, ts) thy P =
|
blanchet@37577
|
436 |
let val ((pred, ts'), pol) = predicate_of thy (P, true) in
|
blanchet@37577
|
437 |
(Literal (pol, pred) :: lits, union (op =) ts ts')
|
blanchet@37577
|
438 |
end
|
blanchet@37577
|
439 |
val literals_of_term = literals_of_term1 ([], [])
|
blanchet@37577
|
440 |
|
blanchet@37577
|
441 |
fun skolem_name i j num_T_args =
|
blanchet@37577
|
442 |
skolem_prefix ^ (space_implode "_" (map Int.toString [i, j, num_T_args])) ^
|
blanchet@37577
|
443 |
skolem_infix ^ "g"
|
blanchet@37577
|
444 |
|
blanchet@37625
|
445 |
fun conceal_skolem_terms i skolems t =
|
blanchet@37577
|
446 |
if exists_Const (curry (op =) @{const_name skolem_id} o fst) t then
|
blanchet@37577
|
447 |
let
|
blanchet@37625
|
448 |
fun aux skolems
|
blanchet@37577
|
449 |
(t as (Const (@{const_name skolem_id}, Type (_, [_, T])) $ _)) =
|
blanchet@37577
|
450 |
let
|
blanchet@37625
|
451 |
val (skolems, s) =
|
blanchet@37577
|
452 |
if i = ~1 then
|
blanchet@37625
|
453 |
(skolems, @{const_name undefined})
|
blanchet@37625
|
454 |
else case AList.find (op aconv) skolems t of
|
blanchet@37625
|
455 |
s :: _ => (skolems, s)
|
blanchet@37577
|
456 |
| [] =>
|
blanchet@37577
|
457 |
let
|
blanchet@37577
|
458 |
val s = skolem_theory_name ^ "." ^
|
blanchet@37625
|
459 |
skolem_name i (length skolems)
|
blanchet@37577
|
460 |
(length (Term.add_tvarsT T []))
|
blanchet@37625
|
461 |
in ((s, t) :: skolems, s) end
|
blanchet@37625
|
462 |
in (skolems, Const (s, T)) end
|
blanchet@37625
|
463 |
| aux skolems (t1 $ t2) =
|
blanchet@37577
|
464 |
let
|
blanchet@37625
|
465 |
val (skolems, t1) = aux skolems t1
|
blanchet@37625
|
466 |
val (skolems, t2) = aux skolems t2
|
blanchet@37625
|
467 |
in (skolems, t1 $ t2) end
|
blanchet@37625
|
468 |
| aux skolems (Abs (s, T, t')) =
|
blanchet@37625
|
469 |
let val (skolems, t') = aux skolems t' in
|
blanchet@37625
|
470 |
(skolems, Abs (s, T, t'))
|
blanchet@37577
|
471 |
end
|
blanchet@37625
|
472 |
| aux skolems t = (skolems, t)
|
blanchet@37625
|
473 |
in aux skolems t end
|
blanchet@37577
|
474 |
else
|
blanchet@37625
|
475 |
(skolems, t)
|
blanchet@37577
|
476 |
|
blanchet@37632
|
477 |
fun reveal_skolem_terms skolems =
|
blanchet@37632
|
478 |
map_aterms (fn t as Const (s, _) =>
|
blanchet@37632
|
479 |
if String.isPrefix skolem_theory_name s then
|
blanchet@37632
|
480 |
AList.lookup (op =) skolems s |> the
|
blanchet@37632
|
481 |
|> map_types Type_Infer.paramify_vars
|
blanchet@37632
|
482 |
else
|
blanchet@37632
|
483 |
t
|
blanchet@37632
|
484 |
| t => t)
|
blanchet@37632
|
485 |
|
blanchet@37577
|
486 |
|
blanchet@37577
|
487 |
(***************************************************************)
|
blanchet@37577
|
488 |
(* Type Classes Present in the Axiom or Conjecture Clauses *)
|
blanchet@37577
|
489 |
(***************************************************************)
|
blanchet@37577
|
490 |
|
blanchet@37577
|
491 |
fun set_insert (x, s) = Symtab.update (x, ()) s
|
blanchet@37577
|
492 |
|
blanchet@37577
|
493 |
fun add_classes (sorts, cset) = List.foldl set_insert cset (flat sorts)
|
blanchet@37577
|
494 |
|
blanchet@37577
|
495 |
(*Remove this trivial type class*)
|
blanchet@37577
|
496 |
fun delete_type cset = Symtab.delete_safe (the_single @{sort HOL.type}) cset;
|
blanchet@37577
|
497 |
|
blanchet@37577
|
498 |
fun tfree_classes_of_terms ts =
|
blanchet@37577
|
499 |
let val sorts_list = map (map #2 o OldTerm.term_tfrees) ts
|
blanchet@37577
|
500 |
in Symtab.keys (delete_type (List.foldl add_classes Symtab.empty sorts_list)) end;
|
blanchet@37577
|
501 |
|
blanchet@37577
|
502 |
fun tvar_classes_of_terms ts =
|
blanchet@37577
|
503 |
let val sorts_list = map (map #2 o OldTerm.term_tvars) ts
|
blanchet@37577
|
504 |
in Symtab.keys (delete_type (List.foldl add_classes Symtab.empty sorts_list)) end;
|
blanchet@37577
|
505 |
|
blanchet@37577
|
506 |
(*fold type constructors*)
|
blanchet@37577
|
507 |
fun fold_type_consts f (Type (a, Ts)) x = fold (fold_type_consts f) Ts (f (a,x))
|
blanchet@37577
|
508 |
| fold_type_consts _ _ x = x;
|
blanchet@37577
|
509 |
|
blanchet@37577
|
510 |
(*Type constructors used to instantiate overloaded constants are the only ones needed.*)
|
blanchet@37577
|
511 |
fun add_type_consts_in_term thy =
|
blanchet@37577
|
512 |
let
|
blanchet@37577
|
513 |
val const_typargs = Sign.const_typargs thy
|
blanchet@37577
|
514 |
fun aux (Const x) = fold (fold_type_consts set_insert) (const_typargs x)
|
blanchet@37577
|
515 |
| aux (Abs (_, _, u)) = aux u
|
blanchet@37577
|
516 |
| aux (Const (@{const_name skolem_id}, _) $ _) = I
|
blanchet@37577
|
517 |
| aux (t $ u) = aux t #> aux u
|
blanchet@37577
|
518 |
| aux _ = I
|
blanchet@37577
|
519 |
in aux end
|
blanchet@37577
|
520 |
|
blanchet@37577
|
521 |
fun type_consts_of_terms thy ts =
|
blanchet@37577
|
522 |
Symtab.keys (fold (add_type_consts_in_term thy) ts Symtab.empty);
|
blanchet@37577
|
523 |
|
paulson@15347
|
524 |
end;
|