blanchet@35826
|
1 |
(* Title: HOL/Tools/Sledgehammer/sledgehammer_fol_clause.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@35826
|
9 |
signature SLEDGEHAMMER_FOL_CLAUSE =
|
wenzelm@24310
|
10 |
sig
|
blanchet@37577
|
11 |
type cnf_thm = Clausifier.cnf_thm
|
blanchet@37577
|
12 |
type name = string * string
|
blanchet@37577
|
13 |
type name_pool = string Symtab.table * string Symtab.table
|
blanchet@37577
|
14 |
datatype kind = Axiom | Conjecture
|
blanchet@37577
|
15 |
datatype type_literal =
|
blanchet@37577
|
16 |
TyLitVar of string * name |
|
blanchet@37577
|
17 |
TyLitFree of string * name
|
blanchet@37577
|
18 |
datatype arLit =
|
blanchet@37577
|
19 |
TConsLit of class * string * string list
|
blanchet@37577
|
20 |
| TVarLit of class * string
|
blanchet@37577
|
21 |
datatype arity_clause = ArityClause of
|
blanchet@37577
|
22 |
{axiom_name: string, conclLit: arLit, premLits: arLit list}
|
blanchet@37577
|
23 |
datatype classrel_clause = ClassrelClause of
|
blanchet@37577
|
24 |
{axiom_name: string, subclass: class, superclass: class}
|
blanchet@37577
|
25 |
datatype combtyp =
|
blanchet@37577
|
26 |
TyVar of name |
|
blanchet@37577
|
27 |
TyFree of name |
|
blanchet@37577
|
28 |
TyConstr of name * combtyp list
|
blanchet@37577
|
29 |
datatype combterm =
|
blanchet@37577
|
30 |
CombConst of name * combtyp * combtyp list (* Const and Free *) |
|
blanchet@37577
|
31 |
CombVar of name * combtyp |
|
blanchet@37577
|
32 |
CombApp of combterm * combterm
|
blanchet@37577
|
33 |
datatype literal = Literal of bool * combterm
|
blanchet@37577
|
34 |
datatype hol_clause =
|
blanchet@37577
|
35 |
HOLClause of {clause_id: int, axiom_name: string, th: thm, kind: kind,
|
blanchet@37577
|
36 |
literals: literal list, ctypes_sorts: typ list}
|
blanchet@37577
|
37 |
exception TRIVIAL of unit
|
blanchet@37577
|
38 |
|
blanchet@37509
|
39 |
val type_wrapper_name : string
|
wenzelm@24310
|
40 |
val schematic_var_prefix: string
|
wenzelm@24310
|
41 |
val fixed_var_prefix: string
|
wenzelm@24310
|
42 |
val tvar_prefix: string
|
wenzelm@24310
|
43 |
val tfree_prefix: string
|
wenzelm@24310
|
44 |
val const_prefix: string
|
wenzelm@24310
|
45 |
val tconst_prefix: string
|
wenzelm@24310
|
46 |
val class_prefix: string
|
wenzelm@24310
|
47 |
val union_all: ''a list list -> ''a list
|
blanchet@37572
|
48 |
val invert_const: string -> string
|
wenzelm@24310
|
49 |
val ascii_of: string -> string
|
wenzelm@24310
|
50 |
val undo_ascii_of: string -> string
|
blanchet@37572
|
51 |
val strip_prefix: string -> string -> string option
|
wenzelm@24310
|
52 |
val make_schematic_var : string * int -> string
|
wenzelm@24310
|
53 |
val make_fixed_var : string -> string
|
wenzelm@24310
|
54 |
val make_schematic_type_var : string * int -> string
|
wenzelm@24310
|
55 |
val make_fixed_type_var : string -> string
|
blanchet@37498
|
56 |
val make_fixed_const : string -> string
|
blanchet@37498
|
57 |
val make_fixed_type_const : string -> string
|
wenzelm@24310
|
58 |
val make_type_class : string -> string
|
blanchet@36169
|
59 |
val empty_name_pool : bool -> name_pool option
|
blanchet@36169
|
60 |
val pool_map : ('a -> 'b -> 'c * 'b) -> 'a list -> 'b -> 'c list * 'b
|
blanchet@36169
|
61 |
val nice_name : name -> name_pool option -> string * name_pool option
|
blanchet@36959
|
62 |
val type_literals_for_types : typ list -> type_literal list
|
blanchet@35865
|
63 |
val make_classrel_clauses: theory -> class list -> class list -> classrel_clause list
|
blanchet@35865
|
64 |
val make_arity_clauses: theory -> string list -> class list -> class list * arity_clause list
|
blanchet@37577
|
65 |
val type_of_combterm : combterm -> combtyp
|
blanchet@37577
|
66 |
val strip_combterm_comb : combterm -> combterm * combterm list
|
blanchet@37577
|
67 |
val literals_of_term : theory -> term -> literal list * typ list
|
blanchet@37577
|
68 |
val conceal_skolem_somes :
|
blanchet@37577
|
69 |
int -> (string * term) list -> term -> (string * term) list * term
|
blanchet@37577
|
70 |
val is_quasi_fol_theorem : theory -> thm -> bool
|
blanchet@37577
|
71 |
val make_clause_table : (thm * 'a) list -> (thm * 'a) Termtab.table
|
blanchet@37577
|
72 |
val tfree_classes_of_terms : term list -> string list
|
blanchet@37577
|
73 |
val tvar_classes_of_terms : term list -> string list
|
blanchet@37577
|
74 |
val type_consts_of_terms : theory -> term list -> string list
|
blanchet@37577
|
75 |
val prepare_clauses :
|
blanchet@37577
|
76 |
bool -> thm list -> cnf_thm list -> cnf_thm list -> theory
|
blanchet@37577
|
77 |
-> string vector
|
blanchet@37577
|
78 |
* (hol_clause list * hol_clause list * hol_clause list * hol_clause list
|
blanchet@37577
|
79 |
* classrel_clause list * arity_clause list)
|
wenzelm@24310
|
80 |
end
|
paulson@15347
|
81 |
|
blanchet@35826
|
82 |
structure Sledgehammer_FOL_Clause : SLEDGEHAMMER_FOL_CLAUSE =
|
paulson@15347
|
83 |
struct
|
paulson@15347
|
84 |
|
blanchet@37577
|
85 |
open Clausifier
|
blanchet@37577
|
86 |
|
blanchet@37509
|
87 |
val type_wrapper_name = "ti"
|
blanchet@37509
|
88 |
|
paulson@15347
|
89 |
val schematic_var_prefix = "V_";
|
paulson@15347
|
90 |
val fixed_var_prefix = "v_";
|
paulson@15347
|
91 |
|
paulson@17230
|
92 |
val tvar_prefix = "T_";
|
paulson@17230
|
93 |
val tfree_prefix = "t_";
|
paulson@15347
|
94 |
|
blanchet@37509
|
95 |
val classrel_clause_prefix = "clsrel_";
|
paulson@15347
|
96 |
|
paulson@17230
|
97 |
val const_prefix = "c_";
|
wenzelm@24310
|
98 |
val tconst_prefix = "tc_";
|
wenzelm@24310
|
99 |
val class_prefix = "class_";
|
paulson@15347
|
100 |
|
blanchet@36218
|
101 |
fun union_all xss = fold (union (op =)) xss []
|
paulson@17775
|
102 |
|
blanchet@36489
|
103 |
(* Readable names for the more common symbolic functions. Do not mess with the
|
blanchet@37454
|
104 |
last nine entries of the table unless you know what you are doing. *)
|
paulson@15347
|
105 |
val const_trans_table =
|
blanchet@35865
|
106 |
Symtab.make [(@{const_name "op ="}, "equal"),
|
blanchet@35865
|
107 |
(@{const_name "op &"}, "and"),
|
blanchet@35865
|
108 |
(@{const_name "op |"}, "or"),
|
blanchet@35865
|
109 |
(@{const_name "op -->"}, "implies"),
|
blanchet@36489
|
110 |
(@{const_name "op :"}, "in"),
|
blanchet@36489
|
111 |
(@{const_name fequal}, "fequal"),
|
blanchet@36489
|
112 |
(@{const_name COMBI}, "COMBI"),
|
blanchet@36489
|
113 |
(@{const_name COMBK}, "COMBK"),
|
blanchet@36489
|
114 |
(@{const_name COMBB}, "COMBB"),
|
blanchet@36489
|
115 |
(@{const_name COMBC}, "COMBC"),
|
blanchet@37454
|
116 |
(@{const_name COMBS}, "COMBS"),
|
blanchet@37454
|
117 |
(@{const_name True}, "True"),
|
blanchet@37454
|
118 |
(@{const_name False}, "False"),
|
blanchet@37572
|
119 |
(@{const_name If}, "If"),
|
blanchet@37572
|
120 |
(@{type_name "*"}, "prod"),
|
blanchet@37572
|
121 |
(@{type_name "+"}, "sum")]
|
paulson@15347
|
122 |
|
blanchet@37572
|
123 |
(* Invert the table of translations between Isabelle and ATPs. *)
|
blanchet@37572
|
124 |
val const_trans_table_inv =
|
blanchet@37572
|
125 |
Symtab.update ("fequal", @{const_name "op ="})
|
blanchet@37572
|
126 |
(Symtab.make (map swap (Symtab.dest const_trans_table)))
|
blanchet@37572
|
127 |
|
blanchet@37572
|
128 |
val invert_const = perhaps (Symtab.lookup const_trans_table_inv)
|
paulson@15347
|
129 |
|
paulson@15610
|
130 |
(*Escaping of special characters.
|
paulson@15610
|
131 |
Alphanumeric characters are left unchanged.
|
paulson@15610
|
132 |
The character _ goes to __
|
paulson@15610
|
133 |
Characters in the range ASCII space to / go to _A to _P, respectively.
|
paulson@24183
|
134 |
Other printing characters go to _nnn where nnn is the decimal ASCII code.*)
|
paulson@24183
|
135 |
val A_minus_space = Char.ord #"A" - Char.ord #" ";
|
paulson@15610
|
136 |
|
paulson@24183
|
137 |
fun stringN_of_int 0 _ = ""
|
paulson@24183
|
138 |
| stringN_of_int k n = stringN_of_int (k-1) (n div 10) ^ Int.toString (n mod 10);
|
paulson@15610
|
139 |
|
paulson@15347
|
140 |
fun ascii_of_c c =
|
paulson@15610
|
141 |
if Char.isAlphaNum c then String.str c
|
paulson@15610
|
142 |
else if c = #"_" then "__"
|
wenzelm@24310
|
143 |
else if #" " <= c andalso c <= #"/"
|
paulson@15610
|
144 |
then "_" ^ String.str (Char.chr (Char.ord c + A_minus_space))
|
wenzelm@24310
|
145 |
else if Char.isPrint c
|
paulson@24183
|
146 |
then ("_" ^ stringN_of_int 3 (Char.ord c)) (*fixed width, in case more digits follow*)
|
paulson@15610
|
147 |
else ""
|
paulson@15347
|
148 |
|
paulson@15610
|
149 |
val ascii_of = String.translate ascii_of_c;
|
paulson@15610
|
150 |
|
paulson@24183
|
151 |
(** Remove ASCII armouring from names in proof files **)
|
paulson@24183
|
152 |
|
paulson@24183
|
153 |
(*We don't raise error exceptions because this code can run inside the watcher.
|
paulson@24183
|
154 |
Also, the errors are "impossible" (hah!)*)
|
paulson@24183
|
155 |
fun undo_ascii_aux rcs [] = String.implode(rev rcs)
|
paulson@24183
|
156 |
| undo_ascii_aux rcs [#"_"] = undo_ascii_aux (#"_"::rcs) [] (*ERROR*)
|
paulson@24183
|
157 |
(*Three types of _ escapes: __, _A to _P, _nnn*)
|
paulson@24183
|
158 |
| undo_ascii_aux rcs (#"_" :: #"_" :: cs) = undo_ascii_aux (#"_"::rcs) cs
|
wenzelm@24310
|
159 |
| undo_ascii_aux rcs (#"_" :: c :: cs) =
|
paulson@24183
|
160 |
if #"A" <= c andalso c<= #"P" (*translation of #" " to #"/"*)
|
paulson@24183
|
161 |
then undo_ascii_aux (Char.chr(Char.ord c - A_minus_space) :: rcs) cs
|
wenzelm@24310
|
162 |
else
|
paulson@24183
|
163 |
let val digits = List.take (c::cs, 3) handle Subscript => []
|
wenzelm@24310
|
164 |
in
|
paulson@24183
|
165 |
case Int.fromString (String.implode digits) of
|
paulson@24183
|
166 |
NONE => undo_ascii_aux (c:: #"_"::rcs) cs (*ERROR*)
|
paulson@24183
|
167 |
| SOME n => undo_ascii_aux (Char.chr n :: rcs) (List.drop (cs, 2))
|
paulson@24183
|
168 |
end
|
paulson@24183
|
169 |
| undo_ascii_aux rcs (c::cs) = undo_ascii_aux (c::rcs) cs;
|
paulson@24183
|
170 |
|
paulson@24183
|
171 |
val undo_ascii_of = undo_ascii_aux [] o String.explode;
|
paulson@15347
|
172 |
|
blanchet@37572
|
173 |
(* If string s has the prefix s1, return the result of deleting it,
|
blanchet@37572
|
174 |
un-ASCII'd. *)
|
blanchet@37572
|
175 |
fun strip_prefix s1 s =
|
blanchet@37572
|
176 |
if String.isPrefix s1 s then
|
blanchet@37572
|
177 |
SOME (undo_ascii_of (String.extract (s, size s1, NONE)))
|
blanchet@37572
|
178 |
else
|
blanchet@37572
|
179 |
NONE
|
blanchet@37572
|
180 |
|
paulson@16925
|
181 |
(*Remove the initial ' character from a type variable, if it is present*)
|
paulson@16925
|
182 |
fun trim_type_var s =
|
paulson@16925
|
183 |
if s <> "" andalso String.sub(s,0) = #"'" then String.extract(s,1,NONE)
|
paulson@16925
|
184 |
else error ("trim_type: Malformed type variable encountered: " ^ s);
|
paulson@16925
|
185 |
|
paulson@16903
|
186 |
fun ascii_of_indexname (v,0) = ascii_of v
|
paulson@17525
|
187 |
| ascii_of_indexname (v,i) = ascii_of v ^ "_" ^ Int.toString i;
|
paulson@15347
|
188 |
|
paulson@17230
|
189 |
fun make_schematic_var v = schematic_var_prefix ^ (ascii_of_indexname v);
|
paulson@15347
|
190 |
fun make_fixed_var x = fixed_var_prefix ^ (ascii_of x);
|
paulson@15347
|
191 |
|
wenzelm@24310
|
192 |
fun make_schematic_type_var (x,i) =
|
paulson@16925
|
193 |
tvar_prefix ^ (ascii_of_indexname (trim_type_var x,i));
|
paulson@16925
|
194 |
fun make_fixed_type_var x = tfree_prefix ^ (ascii_of (trim_type_var x));
|
paulson@15347
|
195 |
|
blanchet@37498
|
196 |
fun lookup_const c =
|
blanchet@37498
|
197 |
case Symtab.lookup const_trans_table c of
|
blanchet@37498
|
198 |
SOME c' => c'
|
blanchet@37498
|
199 |
| NONE => ascii_of c
|
blanchet@36378
|
200 |
|
blanchet@36062
|
201 |
(* "op =" MUST BE "equal" because it's built into ATPs. *)
|
blanchet@37498
|
202 |
fun make_fixed_const @{const_name "op ="} = "equal"
|
blanchet@37498
|
203 |
| make_fixed_const c = const_prefix ^ lookup_const c
|
paulson@18411
|
204 |
|
blanchet@37572
|
205 |
fun make_fixed_type_const c = tconst_prefix ^ lookup_const c
|
quigley@17150
|
206 |
|
wenzelm@17261
|
207 |
fun make_type_class clas = class_prefix ^ ascii_of clas;
|
quigley@17150
|
208 |
|
quigley@17150
|
209 |
|
blanchet@36169
|
210 |
(**** name pool ****)
|
blanchet@36169
|
211 |
|
blanchet@36169
|
212 |
type name = string * string
|
blanchet@36169
|
213 |
type name_pool = string Symtab.table * string Symtab.table
|
blanchet@36169
|
214 |
|
blanchet@36222
|
215 |
fun empty_name_pool readable_names =
|
blanchet@36222
|
216 |
if readable_names then SOME (`I Symtab.empty) else NONE
|
blanchet@36169
|
217 |
|
blanchet@36554
|
218 |
fun pool_fold f xs z = pair z #> fold_rev (fn x => uncurry (f x)) xs
|
blanchet@36169
|
219 |
fun pool_map f xs =
|
blanchet@36554
|
220 |
pool_fold (fn x => fn ys => fn pool => f x pool |>> (fn y => y :: ys)) xs []
|
blanchet@36169
|
221 |
|
blanchet@36169
|
222 |
fun add_nice_name full_name nice_prefix j the_pool =
|
blanchet@36169
|
223 |
let
|
blanchet@36169
|
224 |
val nice_name = nice_prefix ^ (if j = 0 then "" else "_" ^ Int.toString j)
|
blanchet@36169
|
225 |
in
|
blanchet@36169
|
226 |
case Symtab.lookup (snd the_pool) nice_name of
|
blanchet@36169
|
227 |
SOME full_name' =>
|
blanchet@36169
|
228 |
if full_name = full_name' then (nice_name, the_pool)
|
blanchet@36169
|
229 |
else add_nice_name full_name nice_prefix (j + 1) the_pool
|
blanchet@36169
|
230 |
| NONE =>
|
blanchet@36169
|
231 |
(nice_name, (Symtab.update_new (full_name, nice_name) (fst the_pool),
|
blanchet@36169
|
232 |
Symtab.update_new (nice_name, full_name) (snd the_pool)))
|
blanchet@36169
|
233 |
end
|
blanchet@36169
|
234 |
|
blanchet@36169
|
235 |
fun translate_first_char f s =
|
blanchet@36169
|
236 |
String.str (f (String.sub (s, 0))) ^ String.extract (s, 1, NONE)
|
blanchet@36169
|
237 |
|
blanchet@36222
|
238 |
fun readable_name full_name s =
|
blanchet@36169
|
239 |
let
|
blanchet@37575
|
240 |
val s = s |> Long_Name.base_name |> Name.desymbolize false
|
blanchet@36169
|
241 |
val s' = s |> explode |> rev |> dropwhile (curry (op =) "'")
|
blanchet@36169
|
242 |
val s' =
|
blanchet@36169
|
243 |
(s' |> rev
|
blanchet@36169
|
244 |
|> implode
|
blanchet@36169
|
245 |
|> String.translate
|
blanchet@36221
|
246 |
(fn c => if Char.isAlphaNum c orelse c = #"_" then String.str c
|
blanchet@36221
|
247 |
else ""))
|
blanchet@36169
|
248 |
^ replicate_string (String.size s - length s') "_"
|
blanchet@36169
|
249 |
val s' =
|
blanchet@36169
|
250 |
if s' = "" orelse not (Char.isAlpha (String.sub (s', 0))) then "X" ^ s'
|
blanchet@36169
|
251 |
else s'
|
blanchet@36472
|
252 |
(* Avoid "equal", since it's built into ATPs; and "op" is very ambiguous
|
blanchet@36472
|
253 |
("op &", "op |", etc.). *)
|
blanchet@36472
|
254 |
val s' = if s' = "equal" orelse s' = "op" then full_name else s'
|
blanchet@36169
|
255 |
in
|
blanchet@36169
|
256 |
case (Char.isLower (String.sub (full_name, 0)),
|
blanchet@36169
|
257 |
Char.isLower (String.sub (s', 0))) of
|
blanchet@36169
|
258 |
(true, false) => translate_first_char Char.toLower s'
|
blanchet@36169
|
259 |
| (false, true) => translate_first_char Char.toUpper s'
|
blanchet@36169
|
260 |
| _ => s'
|
blanchet@36169
|
261 |
end
|
blanchet@36169
|
262 |
|
blanchet@36169
|
263 |
fun nice_name (full_name, _) NONE = (full_name, NONE)
|
blanchet@36169
|
264 |
| nice_name (full_name, desired_name) (SOME the_pool) =
|
blanchet@36169
|
265 |
case Symtab.lookup (fst the_pool) full_name of
|
blanchet@36169
|
266 |
SOME nice_name => (nice_name, SOME the_pool)
|
blanchet@36222
|
267 |
| NONE => add_nice_name full_name (readable_name full_name desired_name) 0
|
blanchet@36222
|
268 |
the_pool
|
blanchet@36169
|
269 |
|> apsnd SOME
|
blanchet@36169
|
270 |
|
blanchet@37498
|
271 |
(**** Definitions and functions for FOL clauses for TPTP format output ****)
|
paulson@15347
|
272 |
|
blanchet@37577
|
273 |
datatype kind = Axiom | Conjecture
|
paulson@23385
|
274 |
|
paulson@15347
|
275 |
(**** Isabelle FOL clauses ****)
|
paulson@15347
|
276 |
|
blanchet@36554
|
277 |
(* The first component is the type class; the second is a TVar or TFree. *)
|
blanchet@36554
|
278 |
datatype type_literal =
|
blanchet@36554
|
279 |
TyLitVar of string * name |
|
blanchet@36554
|
280 |
TyLitFree of string * name
|
paulson@15347
|
281 |
|
paulson@17404
|
282 |
exception CLAUSE of string * term;
|
paulson@15347
|
283 |
|
wenzelm@24310
|
284 |
(*Make literals for sorted type variables*)
|
paulson@24940
|
285 |
fun sorts_on_typs_aux (_, []) = []
|
paulson@24940
|
286 |
| sorts_on_typs_aux ((x,i), s::ss) =
|
paulson@24940
|
287 |
let val sorts = sorts_on_typs_aux ((x,i), ss)
|
paulson@22643
|
288 |
in
|
paulson@22643
|
289 |
if s = "HOL.type" then sorts
|
blanchet@36554
|
290 |
else if i = ~1 then TyLitFree (make_type_class s, `make_fixed_type_var x) :: sorts
|
blanchet@36554
|
291 |
else TyLitVar (make_type_class s, (make_schematic_type_var (x,i), x)) :: sorts
|
paulson@22643
|
292 |
end;
|
quigley@17150
|
293 |
|
paulson@24940
|
294 |
fun sorts_on_typs (TFree (a,s)) = sorts_on_typs_aux ((a,~1),s)
|
paulson@24940
|
295 |
| sorts_on_typs (TVar (v,s)) = sorts_on_typs_aux (v,s);
|
paulson@24940
|
296 |
|
paulson@24937
|
297 |
(*Given a list of sorted type variables, return a list of type literals.*)
|
blanchet@36959
|
298 |
fun type_literals_for_types Ts =
|
blanchet@36959
|
299 |
fold (union (op =)) (map sorts_on_typs Ts) []
|
mengj@20015
|
300 |
|
mengj@20015
|
301 |
(** make axiom and conjecture clauses. **)
|
mengj@20015
|
302 |
|
paulson@15347
|
303 |
(**** Isabelle arities ****)
|
paulson@15347
|
304 |
|
wenzelm@24310
|
305 |
datatype arLit = TConsLit of class * string * string list
|
paulson@22643
|
306 |
| TVarLit of class * string;
|
wenzelm@24310
|
307 |
|
blanchet@35865
|
308 |
datatype arity_clause =
|
blanchet@37500
|
309 |
ArityClause of {axiom_name: string, conclLit: arLit, premLits: arLit list}
|
paulson@15347
|
310 |
|
paulson@15347
|
311 |
|
paulson@18798
|
312 |
fun gen_TVars 0 = []
|
paulson@18798
|
313 |
| gen_TVars n = ("T_" ^ Int.toString n) :: gen_TVars (n-1);
|
paulson@15347
|
314 |
|
paulson@18411
|
315 |
fun pack_sort(_,[]) = []
|
paulson@18411
|
316 |
| pack_sort(tvar, "HOL.type"::srt) = pack_sort(tvar, srt) (*IGNORE sort "type"*)
|
paulson@22643
|
317 |
| pack_sort(tvar, cls::srt) = (cls, tvar) :: pack_sort(tvar, srt);
|
wenzelm@24310
|
318 |
|
paulson@18411
|
319 |
(*Arity of type constructor tcon :: (arg1,...,argN)res*)
|
blanchet@37498
|
320 |
fun make_axiom_arity_clause (tcons, axiom_name, (cls,args)) =
|
paulson@21560
|
321 |
let val tvars = gen_TVars (length args)
|
paulson@17845
|
322 |
val tvars_srts = ListPair.zip (tvars,args)
|
paulson@17845
|
323 |
in
|
blanchet@37498
|
324 |
ArityClause {axiom_name = axiom_name,
|
blanchet@37498
|
325 |
conclLit = TConsLit (cls, make_fixed_type_const tcons, tvars),
|
blanchet@37498
|
326 |
premLits = map TVarLit (union_all(map pack_sort tvars_srts))}
|
paulson@17845
|
327 |
end;
|
paulson@15347
|
328 |
|
paulson@15347
|
329 |
|
paulson@15347
|
330 |
(**** Isabelle class relations ****)
|
paulson@15347
|
331 |
|
blanchet@35865
|
332 |
datatype classrel_clause =
|
blanchet@37500
|
333 |
ClassrelClause of {axiom_name: string, subclass: class, superclass: class}
|
wenzelm@24310
|
334 |
|
paulson@21290
|
335 |
(*Generate all pairs (sub,super) such that sub is a proper subclass of super in theory thy.*)
|
blanchet@37498
|
336 |
fun class_pairs _ [] _ = []
|
paulson@21432
|
337 |
| class_pairs thy subs supers =
|
blanchet@36218
|
338 |
let
|
blanchet@36218
|
339 |
val class_less = Sorts.class_less (Sign.classes_of thy)
|
blanchet@36218
|
340 |
fun add_super sub super = class_less (sub, super) ? cons (sub, super)
|
blanchet@36218
|
341 |
fun add_supers sub = fold (add_super sub) supers
|
blanchet@36218
|
342 |
in fold add_supers subs [] end
|
paulson@15347
|
343 |
|
blanchet@35865
|
344 |
fun make_classrel_clause (sub,super) =
|
blanchet@37509
|
345 |
ClassrelClause {axiom_name = classrel_clause_prefix ^ ascii_of sub ^ "_" ^
|
blanchet@37509
|
346 |
ascii_of super,
|
wenzelm@24310
|
347 |
subclass = make_type_class sub,
|
paulson@21290
|
348 |
superclass = make_type_class super};
|
paulson@15347
|
349 |
|
paulson@21290
|
350 |
fun make_classrel_clauses thy subs supers =
|
blanchet@35865
|
351 |
map make_classrel_clause (class_pairs thy subs supers);
|
paulson@18868
|
352 |
|
paulson@18868
|
353 |
|
paulson@18868
|
354 |
(** Isabelle arities **)
|
paulson@17845
|
355 |
|
blanchet@37498
|
356 |
fun arity_clause _ _ (_, []) = []
|
blanchet@37498
|
357 |
| arity_clause seen n (tcons, ("HOL.type",_)::ars) = (*ignore*)
|
blanchet@37498
|
358 |
arity_clause seen n (tcons,ars)
|
blanchet@37498
|
359 |
| arity_clause seen n (tcons, (ar as (class,_)) :: ars) =
|
haftmann@36677
|
360 |
if member (op =) seen class then (*multiple arities for the same tycon, class pair*)
|
blanchet@37572
|
361 |
make_axiom_arity_clause (tcons, lookup_const tcons ^ "_" ^ class ^ "_" ^ Int.toString n, ar) ::
|
blanchet@37498
|
362 |
arity_clause seen (n+1) (tcons,ars)
|
paulson@21373
|
363 |
else
|
blanchet@37572
|
364 |
make_axiom_arity_clause (tcons, lookup_const tcons ^ "_" ^ class, ar) ::
|
blanchet@37498
|
365 |
arity_clause (class::seen) n (tcons,ars)
|
paulson@17845
|
366 |
|
blanchet@37498
|
367 |
fun multi_arity_clause [] = []
|
blanchet@37498
|
368 |
| multi_arity_clause ((tcons, ars) :: tc_arlists) =
|
blanchet@37498
|
369 |
arity_clause [] 1 (tcons, ars) @ multi_arity_clause tc_arlists
|
paulson@17845
|
370 |
|
paulson@22643
|
371 |
(*Generate all pairs (tycon,class,sorts) such that tycon belongs to class in theory thy
|
paulson@22643
|
372 |
provided its arguments have the corresponding sorts.*)
|
paulson@21373
|
373 |
fun type_class_pairs thy tycons classes =
|
paulson@21373
|
374 |
let val alg = Sign.classes_of thy
|
blanchet@36218
|
375 |
fun domain_sorts tycon = Sorts.mg_domain alg tycon o single
|
blanchet@36218
|
376 |
fun add_class tycon class =
|
blanchet@36218
|
377 |
cons (class, domain_sorts tycon class)
|
blanchet@36218
|
378 |
handle Sorts.CLASS_ERROR _ => I
|
blanchet@36218
|
379 |
fun try_classes tycon = (tycon, fold (add_class tycon) classes [])
|
paulson@21373
|
380 |
in map try_classes tycons end;
|
paulson@21373
|
381 |
|
paulson@22643
|
382 |
(*Proving one (tycon, class) membership may require proving others, so iterate.*)
|
blanchet@37498
|
383 |
fun iter_type_class_pairs _ _ [] = ([], [])
|
paulson@22643
|
384 |
| iter_type_class_pairs thy tycons classes =
|
paulson@22643
|
385 |
let val cpairs = type_class_pairs thy tycons classes
|
haftmann@33040
|
386 |
val newclasses = union_all (union_all (union_all (map (map #2 o #2) cpairs)))
|
haftmann@33040
|
387 |
|> subtract (op =) classes |> subtract (op =) HOLogic.typeS
|
wenzelm@24310
|
388 |
val (classes', cpairs') = iter_type_class_pairs thy tycons newclasses
|
haftmann@33042
|
389 |
in (union (op =) classes' classes, union (op =) cpairs' cpairs) end;
|
wenzelm@24310
|
390 |
|
blanchet@37498
|
391 |
fun make_arity_clauses thy tycons classes =
|
wenzelm@24310
|
392 |
let val (classes', cpairs) = iter_type_class_pairs thy tycons classes
|
blanchet@37498
|
393 |
in (classes', multi_arity_clause cpairs) end;
|
paulson@18863
|
394 |
|
blanchet@37577
|
395 |
datatype combtyp =
|
blanchet@37577
|
396 |
TyVar of name |
|
blanchet@37577
|
397 |
TyFree of name |
|
blanchet@37577
|
398 |
TyConstr of name * combtyp list
|
blanchet@37577
|
399 |
|
blanchet@37577
|
400 |
datatype combterm =
|
blanchet@37577
|
401 |
CombConst of name * combtyp * combtyp list (* Const and Free *) |
|
blanchet@37577
|
402 |
CombVar of name * combtyp |
|
blanchet@37577
|
403 |
CombApp of combterm * combterm
|
blanchet@37577
|
404 |
|
blanchet@37577
|
405 |
datatype literal = Literal of bool * combterm
|
blanchet@37577
|
406 |
|
blanchet@37577
|
407 |
datatype hol_clause =
|
blanchet@37577
|
408 |
HOLClause of {clause_id: int, axiom_name: string, th: thm, kind: kind,
|
blanchet@37577
|
409 |
literals: literal list, ctypes_sorts: typ list}
|
blanchet@37577
|
410 |
|
blanchet@37577
|
411 |
(*********************************************************************)
|
blanchet@37577
|
412 |
(* convert a clause with type Term.term to a clause with type clause *)
|
blanchet@37577
|
413 |
(*********************************************************************)
|
blanchet@37577
|
414 |
|
blanchet@37577
|
415 |
(*Result of a function type; no need to check that the argument type matches.*)
|
blanchet@37577
|
416 |
fun result_type (TyConstr (_, [_, tp2])) = tp2
|
blanchet@37577
|
417 |
| result_type _ = raise Fail "non-function type"
|
blanchet@37577
|
418 |
|
blanchet@37577
|
419 |
fun type_of_combterm (CombConst (_, tp, _)) = tp
|
blanchet@37577
|
420 |
| type_of_combterm (CombVar (_, tp)) = tp
|
blanchet@37577
|
421 |
| type_of_combterm (CombApp (t1, _)) = result_type (type_of_combterm t1)
|
blanchet@37577
|
422 |
|
blanchet@37577
|
423 |
(*gets the head of a combinator application, along with the list of arguments*)
|
blanchet@37577
|
424 |
fun strip_combterm_comb u =
|
blanchet@37577
|
425 |
let fun stripc (CombApp(t,u), ts) = stripc (t, u::ts)
|
blanchet@37577
|
426 |
| stripc x = x
|
blanchet@37577
|
427 |
in stripc(u,[]) end
|
blanchet@37577
|
428 |
|
blanchet@37577
|
429 |
fun isFalse (Literal (pol, CombConst ((c, _), _, _))) =
|
blanchet@37577
|
430 |
(pol andalso c = "c_False") orelse (not pol andalso c = "c_True")
|
blanchet@37577
|
431 |
| isFalse _ = false;
|
blanchet@37577
|
432 |
|
blanchet@37577
|
433 |
fun isTrue (Literal (pol, CombConst ((c, _), _, _))) =
|
blanchet@37577
|
434 |
(pol andalso c = "c_True") orelse
|
blanchet@37577
|
435 |
(not pol andalso c = "c_False")
|
blanchet@37577
|
436 |
| isTrue _ = false;
|
blanchet@37577
|
437 |
|
blanchet@37577
|
438 |
fun isTaut (HOLClause {literals,...}) = exists isTrue literals;
|
blanchet@37577
|
439 |
|
blanchet@37577
|
440 |
fun type_of (Type (a, Ts)) =
|
blanchet@37577
|
441 |
let val (folTypes,ts) = types_of Ts in
|
blanchet@37577
|
442 |
(TyConstr (`make_fixed_type_const a, folTypes), ts)
|
blanchet@37577
|
443 |
end
|
blanchet@37577
|
444 |
| type_of (tp as TFree (a, _)) = (TyFree (`make_fixed_type_var a), [tp])
|
blanchet@37577
|
445 |
| type_of (tp as TVar (x, _)) =
|
blanchet@37577
|
446 |
(TyVar (make_schematic_type_var x, string_of_indexname x), [tp])
|
blanchet@37577
|
447 |
and types_of Ts =
|
blanchet@37577
|
448 |
let val (folTyps, ts) = ListPair.unzip (map type_of Ts) in
|
blanchet@37577
|
449 |
(folTyps, union_all ts)
|
blanchet@37577
|
450 |
end
|
blanchet@37577
|
451 |
|
blanchet@37577
|
452 |
(* same as above, but no gathering of sort information *)
|
blanchet@37577
|
453 |
fun simp_type_of (Type (a, Ts)) =
|
blanchet@37577
|
454 |
TyConstr (`make_fixed_type_const a, map simp_type_of Ts)
|
blanchet@37577
|
455 |
| simp_type_of (TFree (a, _)) = TyFree (`make_fixed_type_var a)
|
blanchet@37577
|
456 |
| simp_type_of (TVar (x, _)) =
|
blanchet@37577
|
457 |
TyVar (make_schematic_type_var x, string_of_indexname x)
|
blanchet@37577
|
458 |
|
blanchet@37577
|
459 |
(* convert a Term.term (with combinators) into a combterm, also accummulate sort info *)
|
blanchet@37577
|
460 |
fun combterm_of thy (Const (c, T)) =
|
blanchet@37577
|
461 |
let
|
blanchet@37577
|
462 |
val (tp, ts) = type_of T
|
blanchet@37577
|
463 |
val tvar_list =
|
blanchet@37577
|
464 |
(if String.isPrefix skolem_theory_name c then
|
blanchet@37577
|
465 |
[] |> Term.add_tvarsT T |> map TVar
|
blanchet@37577
|
466 |
else
|
blanchet@37577
|
467 |
(c, T) |> Sign.const_typargs thy)
|
blanchet@37577
|
468 |
|> map simp_type_of
|
blanchet@37577
|
469 |
val c' = CombConst (`make_fixed_const c, tp, tvar_list)
|
blanchet@37577
|
470 |
in (c',ts) end
|
blanchet@37577
|
471 |
| combterm_of _ (Free(v, T)) =
|
blanchet@37577
|
472 |
let val (tp,ts) = type_of T
|
blanchet@37577
|
473 |
val v' = CombConst (`make_fixed_var v, tp, [])
|
blanchet@37577
|
474 |
in (v',ts) end
|
blanchet@37577
|
475 |
| combterm_of _ (Var(v, T)) =
|
blanchet@37577
|
476 |
let val (tp,ts) = type_of T
|
blanchet@37577
|
477 |
val v' = CombVar ((make_schematic_var v, string_of_indexname v), tp)
|
blanchet@37577
|
478 |
in (v',ts) end
|
blanchet@37577
|
479 |
| combterm_of thy (P $ Q) =
|
blanchet@37577
|
480 |
let val (P', tsP) = combterm_of thy P
|
blanchet@37577
|
481 |
val (Q', tsQ) = combterm_of thy Q
|
blanchet@37577
|
482 |
in (CombApp (P', Q'), union (op =) tsP tsQ) end
|
blanchet@37577
|
483 |
| combterm_of _ (t as Abs _) = raise Fail "HOL clause: Abs"
|
blanchet@37577
|
484 |
|
blanchet@37577
|
485 |
fun predicate_of thy ((@{const Not} $ P), pos) = predicate_of thy (P, not pos)
|
blanchet@37577
|
486 |
| predicate_of thy (t, pos) = (combterm_of thy (Envir.eta_contract t), pos)
|
blanchet@37577
|
487 |
|
blanchet@37577
|
488 |
fun literals_of_term1 args thy (@{const Trueprop} $ P) =
|
blanchet@37577
|
489 |
literals_of_term1 args thy P
|
blanchet@37577
|
490 |
| literals_of_term1 args thy (@{const "op |"} $ P $ Q) =
|
blanchet@37577
|
491 |
literals_of_term1 (literals_of_term1 args thy P) thy Q
|
blanchet@37577
|
492 |
| literals_of_term1 (lits, ts) thy P =
|
blanchet@37577
|
493 |
let val ((pred, ts'), pol) = predicate_of thy (P, true) in
|
blanchet@37577
|
494 |
(Literal (pol, pred) :: lits, union (op =) ts ts')
|
blanchet@37577
|
495 |
end
|
blanchet@37577
|
496 |
val literals_of_term = literals_of_term1 ([], [])
|
blanchet@37577
|
497 |
|
blanchet@37577
|
498 |
fun skolem_name i j num_T_args =
|
blanchet@37577
|
499 |
skolem_prefix ^ (space_implode "_" (map Int.toString [i, j, num_T_args])) ^
|
blanchet@37577
|
500 |
skolem_infix ^ "g"
|
blanchet@37577
|
501 |
|
blanchet@37577
|
502 |
fun conceal_skolem_somes i skolem_somes t =
|
blanchet@37577
|
503 |
if exists_Const (curry (op =) @{const_name skolem_id} o fst) t then
|
blanchet@37577
|
504 |
let
|
blanchet@37577
|
505 |
fun aux skolem_somes
|
blanchet@37577
|
506 |
(t as (Const (@{const_name skolem_id}, Type (_, [_, T])) $ _)) =
|
blanchet@37577
|
507 |
let
|
blanchet@37577
|
508 |
val (skolem_somes, s) =
|
blanchet@37577
|
509 |
if i = ~1 then
|
blanchet@37577
|
510 |
(skolem_somes, @{const_name undefined})
|
blanchet@37577
|
511 |
else case AList.find (op aconv) skolem_somes t of
|
blanchet@37577
|
512 |
s :: _ => (skolem_somes, s)
|
blanchet@37577
|
513 |
| [] =>
|
blanchet@37577
|
514 |
let
|
blanchet@37577
|
515 |
val s = skolem_theory_name ^ "." ^
|
blanchet@37577
|
516 |
skolem_name i (length skolem_somes)
|
blanchet@37577
|
517 |
(length (Term.add_tvarsT T []))
|
blanchet@37577
|
518 |
in ((s, t) :: skolem_somes, s) end
|
blanchet@37577
|
519 |
in (skolem_somes, Const (s, T)) end
|
blanchet@37577
|
520 |
| aux skolem_somes (t1 $ t2) =
|
blanchet@37577
|
521 |
let
|
blanchet@37577
|
522 |
val (skolem_somes, t1) = aux skolem_somes t1
|
blanchet@37577
|
523 |
val (skolem_somes, t2) = aux skolem_somes t2
|
blanchet@37577
|
524 |
in (skolem_somes, t1 $ t2) end
|
blanchet@37577
|
525 |
| aux skolem_somes (Abs (s, T, t')) =
|
blanchet@37577
|
526 |
let val (skolem_somes, t') = aux skolem_somes t' in
|
blanchet@37577
|
527 |
(skolem_somes, Abs (s, T, t'))
|
blanchet@37577
|
528 |
end
|
blanchet@37577
|
529 |
| aux skolem_somes t = (skolem_somes, t)
|
blanchet@37577
|
530 |
in aux skolem_somes t end
|
blanchet@37577
|
531 |
else
|
blanchet@37577
|
532 |
(skolem_somes, t)
|
blanchet@37577
|
533 |
|
blanchet@37577
|
534 |
fun is_quasi_fol_theorem thy =
|
blanchet@37577
|
535 |
Meson.is_fol_term thy o snd o conceal_skolem_somes ~1 [] o prop_of
|
blanchet@37577
|
536 |
|
blanchet@37577
|
537 |
(* Trivial problem, which resolution cannot handle (empty clause) *)
|
blanchet@37577
|
538 |
exception TRIVIAL of unit
|
blanchet@37577
|
539 |
|
blanchet@37577
|
540 |
(* making axiom and conjecture clauses *)
|
blanchet@37577
|
541 |
fun make_clause thy (clause_id, axiom_name, kind, th) skolem_somes =
|
blanchet@37577
|
542 |
let
|
blanchet@37577
|
543 |
val (skolem_somes, t) =
|
blanchet@37577
|
544 |
th |> prop_of |> conceal_skolem_somes clause_id skolem_somes
|
blanchet@37577
|
545 |
val (lits, ctypes_sorts) = literals_of_term thy t
|
blanchet@37577
|
546 |
in
|
blanchet@37577
|
547 |
if forall isFalse lits then
|
blanchet@37577
|
548 |
raise TRIVIAL ()
|
blanchet@37577
|
549 |
else
|
blanchet@37577
|
550 |
(skolem_somes,
|
blanchet@37577
|
551 |
HOLClause {clause_id = clause_id, axiom_name = axiom_name, th = th,
|
blanchet@37577
|
552 |
kind = kind, literals = lits, ctypes_sorts = ctypes_sorts})
|
blanchet@37577
|
553 |
end
|
blanchet@37577
|
554 |
|
blanchet@37577
|
555 |
fun add_axiom_clause thy (th, ((name, id), _ : thm)) (skolem_somes, clss) =
|
blanchet@37577
|
556 |
let
|
blanchet@37577
|
557 |
val (skolem_somes, cls) = make_clause thy (id, name, Axiom, th) skolem_somes
|
blanchet@37577
|
558 |
in (skolem_somes, clss |> not (isTaut cls) ? cons (name, cls)) end
|
blanchet@37577
|
559 |
|
blanchet@37577
|
560 |
fun make_axiom_clauses thy clauses =
|
blanchet@37577
|
561 |
([], []) |> fold_rev (add_axiom_clause thy) clauses |> snd
|
blanchet@37577
|
562 |
|
blanchet@37577
|
563 |
fun make_conjecture_clauses thy =
|
blanchet@37577
|
564 |
let
|
blanchet@37577
|
565 |
fun aux _ _ [] = []
|
blanchet@37577
|
566 |
| aux n skolem_somes (th :: ths) =
|
blanchet@37577
|
567 |
let
|
blanchet@37577
|
568 |
val (skolem_somes, cls) =
|
blanchet@37577
|
569 |
make_clause thy (n, "conjecture", Conjecture, th) skolem_somes
|
blanchet@37577
|
570 |
in cls :: aux (n + 1) skolem_somes ths end
|
blanchet@37577
|
571 |
in aux 0 [] end
|
blanchet@37577
|
572 |
|
blanchet@37577
|
573 |
(** Helper clauses **)
|
blanchet@37577
|
574 |
|
blanchet@37577
|
575 |
fun count_combterm (CombConst ((c, _), _, _)) =
|
blanchet@37577
|
576 |
Symtab.map_entry c (Integer.add 1)
|
blanchet@37577
|
577 |
| count_combterm (CombVar _) = I
|
blanchet@37577
|
578 |
| count_combterm (CombApp (t1, t2)) = count_combterm t1 #> count_combterm t2
|
blanchet@37577
|
579 |
fun count_literal (Literal (_, t)) = count_combterm t
|
blanchet@37577
|
580 |
fun count_clause (HOLClause {literals, ...}) = fold count_literal literals
|
blanchet@37577
|
581 |
|
blanchet@37577
|
582 |
fun raw_cnf_rules_pairs ps = map (fn (name, thm) => (thm, ((name, 0), thm))) ps
|
blanchet@37577
|
583 |
fun cnf_helper_thms thy raw =
|
blanchet@37577
|
584 |
map (`Thm.get_name_hint)
|
blanchet@37577
|
585 |
#> (if raw then raw_cnf_rules_pairs else cnf_rules_pairs thy)
|
blanchet@37577
|
586 |
|
blanchet@37577
|
587 |
val optional_helpers =
|
blanchet@37577
|
588 |
[(["c_COMBI", "c_COMBK"], (false, @{thms COMBI_def COMBK_def})),
|
blanchet@37577
|
589 |
(["c_COMBB", "c_COMBC"], (false, @{thms COMBB_def COMBC_def})),
|
blanchet@37577
|
590 |
(["c_COMBS"], (false, @{thms COMBS_def}))]
|
blanchet@37577
|
591 |
val optional_typed_helpers =
|
blanchet@37577
|
592 |
[(["c_True", "c_False"], (true, @{thms True_or_False})),
|
blanchet@37577
|
593 |
(["c_If"], (true, @{thms if_True if_False True_or_False}))]
|
blanchet@37577
|
594 |
val mandatory_helpers = @{thms fequal_imp_equal equal_imp_fequal}
|
blanchet@37577
|
595 |
|
blanchet@37577
|
596 |
val init_counters =
|
blanchet@37577
|
597 |
Symtab.make (maps (maps (map (rpair 0) o fst))
|
blanchet@37577
|
598 |
[optional_helpers, optional_typed_helpers])
|
blanchet@37577
|
599 |
|
blanchet@37577
|
600 |
fun get_helper_clauses thy is_FO full_types conjectures axcls =
|
blanchet@37577
|
601 |
let
|
blanchet@37577
|
602 |
val axclauses = map snd (make_axiom_clauses thy axcls)
|
blanchet@37577
|
603 |
val ct = fold (fold count_clause) [conjectures, axclauses] init_counters
|
blanchet@37577
|
604 |
fun is_needed c = the (Symtab.lookup ct c) > 0
|
blanchet@37577
|
605 |
val cnfs =
|
blanchet@37577
|
606 |
(optional_helpers
|
blanchet@37577
|
607 |
|> full_types ? append optional_typed_helpers
|
blanchet@37577
|
608 |
|> maps (fn (ss, (raw, ths)) =>
|
blanchet@37577
|
609 |
if exists is_needed ss then cnf_helper_thms thy raw ths
|
blanchet@37577
|
610 |
else []))
|
blanchet@37577
|
611 |
@ (if is_FO then [] else cnf_helper_thms thy false mandatory_helpers)
|
blanchet@37577
|
612 |
in map snd (make_axiom_clauses thy cnfs) end
|
blanchet@37577
|
613 |
|
blanchet@37577
|
614 |
fun make_clause_table xs =
|
blanchet@37577
|
615 |
fold (Termtab.update o `(prop_of o fst)) xs Termtab.empty
|
blanchet@37577
|
616 |
|
blanchet@37577
|
617 |
|
blanchet@37577
|
618 |
(***************************************************************)
|
blanchet@37577
|
619 |
(* Type Classes Present in the Axiom or Conjecture Clauses *)
|
blanchet@37577
|
620 |
(***************************************************************)
|
blanchet@37577
|
621 |
|
blanchet@37577
|
622 |
fun set_insert (x, s) = Symtab.update (x, ()) s
|
blanchet@37577
|
623 |
|
blanchet@37577
|
624 |
fun add_classes (sorts, cset) = List.foldl set_insert cset (flat sorts)
|
blanchet@37577
|
625 |
|
blanchet@37577
|
626 |
(*Remove this trivial type class*)
|
blanchet@37577
|
627 |
fun delete_type cset = Symtab.delete_safe (the_single @{sort HOL.type}) cset;
|
blanchet@37577
|
628 |
|
blanchet@37577
|
629 |
fun tfree_classes_of_terms ts =
|
blanchet@37577
|
630 |
let val sorts_list = map (map #2 o OldTerm.term_tfrees) ts
|
blanchet@37577
|
631 |
in Symtab.keys (delete_type (List.foldl add_classes Symtab.empty sorts_list)) end;
|
blanchet@37577
|
632 |
|
blanchet@37577
|
633 |
fun tvar_classes_of_terms ts =
|
blanchet@37577
|
634 |
let val sorts_list = map (map #2 o OldTerm.term_tvars) ts
|
blanchet@37577
|
635 |
in Symtab.keys (delete_type (List.foldl add_classes Symtab.empty sorts_list)) end;
|
blanchet@37577
|
636 |
|
blanchet@37577
|
637 |
(*fold type constructors*)
|
blanchet@37577
|
638 |
fun fold_type_consts f (Type (a, Ts)) x = fold (fold_type_consts f) Ts (f (a,x))
|
blanchet@37577
|
639 |
| fold_type_consts _ _ x = x;
|
blanchet@37577
|
640 |
|
blanchet@37577
|
641 |
(*Type constructors used to instantiate overloaded constants are the only ones needed.*)
|
blanchet@37577
|
642 |
fun add_type_consts_in_term thy =
|
blanchet@37577
|
643 |
let
|
blanchet@37577
|
644 |
val const_typargs = Sign.const_typargs thy
|
blanchet@37577
|
645 |
fun aux (Const x) = fold (fold_type_consts set_insert) (const_typargs x)
|
blanchet@37577
|
646 |
| aux (Abs (_, _, u)) = aux u
|
blanchet@37577
|
647 |
| aux (Const (@{const_name skolem_id}, _) $ _) = I
|
blanchet@37577
|
648 |
| aux (t $ u) = aux t #> aux u
|
blanchet@37577
|
649 |
| aux _ = I
|
blanchet@37577
|
650 |
in aux end
|
blanchet@37577
|
651 |
|
blanchet@37577
|
652 |
fun type_consts_of_terms thy ts =
|
blanchet@37577
|
653 |
Symtab.keys (fold (add_type_consts_in_term thy) ts Symtab.empty);
|
blanchet@37577
|
654 |
|
blanchet@37577
|
655 |
(* Remove existing axiom clauses from the conjecture clauses, as this can
|
blanchet@37577
|
656 |
dramatically boost an ATP's performance (for some reason). *)
|
blanchet@37577
|
657 |
fun subtract_cls ax_clauses =
|
blanchet@37577
|
658 |
filter_out (Termtab.defined (make_clause_table ax_clauses) o prop_of)
|
blanchet@37577
|
659 |
|
blanchet@37577
|
660 |
(* prepare for passing to writer,
|
blanchet@37577
|
661 |
create additional clauses based on the information from extra_cls *)
|
blanchet@37577
|
662 |
fun prepare_clauses full_types goal_cls axcls extra_cls thy =
|
blanchet@37577
|
663 |
let
|
blanchet@37577
|
664 |
val is_FO = forall (Meson.is_fol_term thy o prop_of) goal_cls
|
blanchet@37577
|
665 |
val ccls = subtract_cls extra_cls goal_cls
|
blanchet@37577
|
666 |
val _ = app (fn th => trace_msg (fn _ => Display.string_of_thm_global thy th)) ccls
|
blanchet@37577
|
667 |
val ccltms = map prop_of ccls
|
blanchet@37577
|
668 |
and axtms = map (prop_of o #1) extra_cls
|
blanchet@37577
|
669 |
val subs = tfree_classes_of_terms ccltms
|
blanchet@37577
|
670 |
and supers = tvar_classes_of_terms axtms
|
blanchet@37577
|
671 |
and tycons = type_consts_of_terms thy (ccltms @ axtms)
|
blanchet@37577
|
672 |
(*TFrees in conjecture clauses; TVars in axiom clauses*)
|
blanchet@37577
|
673 |
val conjectures = make_conjecture_clauses thy ccls
|
blanchet@37577
|
674 |
val (_, extra_clauses) = ListPair.unzip (make_axiom_clauses thy extra_cls)
|
blanchet@37577
|
675 |
val (clnames, axiom_clauses) = ListPair.unzip (make_axiom_clauses thy axcls)
|
blanchet@37577
|
676 |
val helper_clauses =
|
blanchet@37577
|
677 |
get_helper_clauses thy is_FO full_types conjectures extra_cls
|
blanchet@37577
|
678 |
val (supers', arity_clauses) = make_arity_clauses thy tycons supers
|
blanchet@37577
|
679 |
val classrel_clauses = make_classrel_clauses thy subs supers'
|
blanchet@37577
|
680 |
in
|
blanchet@37577
|
681 |
(Vector.fromList clnames,
|
blanchet@37577
|
682 |
(conjectures, axiom_clauses, extra_clauses, helper_clauses, classrel_clauses, arity_clauses))
|
blanchet@37577
|
683 |
end
|
blanchet@37577
|
684 |
|
paulson@15347
|
685 |
end;
|