author | wenzelm |
Mon, 18 Aug 2014 12:17:31 +0200 | |
changeset 57978 | 8f4a332500e4 |
parent 57055 | df3a26987a8d |
child 58634 | 9f10d82e8188 |
permissions | -rw-r--r-- |
33982 | 1 |
(* Title: HOL/Tools/Nitpick/nitpick_util.ML |
33192 | 2 |
Author: Jasmin Blanchette, TU Muenchen |
34982
7b8c366e34a2
added support for nonstandard models to Nitpick (based on an idea by Koen Claessen) and did other fixes to Nitpick
blanchet
parents:
34936
diff
changeset
|
3 |
Copyright 2008, 2009, 2010 |
33192 | 4 |
|
5 |
General-purpose functions used by the Nitpick modules. |
|
6 |
*) |
|
7 |
||
33705
947184dc75c9
removed a few global names in Nitpick (styp, nat_less, pairf)
blanchet
parents:
33232
diff
changeset
|
8 |
signature NITPICK_UTIL = |
33192 | 9 |
sig |
10 |
datatype polarity = Pos | Neg | Neut |
|
11 |
||
12 |
exception ARG of string * string |
|
13 |
exception BAD of string * string |
|
34124
c4628a1dcf75
added support for binary nat/int representation to Nitpick
blanchet
parents:
34039
diff
changeset
|
14 |
exception TOO_SMALL of string * string |
c4628a1dcf75
added support for binary nat/int representation to Nitpick
blanchet
parents:
34039
diff
changeset
|
15 |
exception TOO_LARGE of string * string |
33192 | 16 |
exception NOT_SUPPORTED of string |
17 |
exception SAME of unit |
|
18 |
||
19 |
val nitpick_prefix : string |
|
20 |
val curry3 : ('a * 'b * 'c -> 'd) -> 'a -> 'b -> 'c -> 'd |
|
33705
947184dc75c9
removed a few global names in Nitpick (styp, nat_less, pairf)
blanchet
parents:
33232
diff
changeset
|
21 |
val pairf : ('a -> 'b) -> ('a -> 'c) -> 'a -> 'b * 'c |
35385
29f81babefd7
improved precision of infinite "shallow" datatypes in Nitpick;
blanchet
parents:
35280
diff
changeset
|
22 |
val pair_from_fun : (bool -> 'a) -> 'a * 'a |
29f81babefd7
improved precision of infinite "shallow" datatypes in Nitpick;
blanchet
parents:
35280
diff
changeset
|
23 |
val fun_from_pair : 'a * 'a -> bool -> 'a |
29f81babefd7
improved precision of infinite "shallow" datatypes in Nitpick;
blanchet
parents:
35280
diff
changeset
|
24 |
val int_from_bool : bool -> int |
33705
947184dc75c9
removed a few global names in Nitpick (styp, nat_less, pairf)
blanchet
parents:
33232
diff
changeset
|
25 |
val nat_minus : int -> int -> int |
33192 | 26 |
val reasonable_power : int -> int -> int |
27 |
val exact_log : int -> int -> int |
|
28 |
val exact_root : int -> int -> int |
|
29 |
val offset_list : int list -> int list |
|
30 |
val index_seq : int -> int -> int list |
|
31 |
val filter_indices : int list -> 'a list -> 'a list |
|
32 |
val filter_out_indices : int list -> 'a list -> 'a list |
|
33 |
val fold1 : ('a -> 'a -> 'a) -> 'a list -> 'a |
|
34 |
val replicate_list : int -> 'a list -> 'a list |
|
35 |
val n_fold_cartesian_product : 'a list list -> 'a list list |
|
36 |
val all_distinct_unordered_pairs_of : ''a list -> (''a * ''a) list |
|
37 |
val nth_combination : (int * int) list -> int -> int list |
|
38 |
val all_combinations : (int * int) list -> int list list |
|
39 |
val all_permutations : 'a list -> 'a list list |
|
48323 | 40 |
val chunk_list : int -> 'a list -> 'a list list |
33192 | 41 |
val chunk_list_unevenly : int list -> 'a list -> 'a list list |
42 |
val map3 : ('a -> 'b -> 'c -> 'd) -> 'a list -> 'b list -> 'c list -> 'd list |
|
43 |
val double_lookup : |
|
44 |
('a * 'a -> bool) -> ('a option * 'b) list -> 'a -> 'b option |
|
45 |
val triple_lookup : |
|
46 |
(''a * ''a -> bool) -> (''a option * 'b) list -> ''a -> 'b option |
|
47 |
val is_substring_of : string -> string -> bool |
|
48 |
val plural_s : int -> string |
|
49 |
val plural_s_for_list : 'a list -> string |
|
36380
1e8fcaccb3e8
stop referring to Sledgehammer_Util stuff all over Nitpick code; instead, redeclare any needed function in Nitpick_Util as synonym for the Sledgehammer_Util function of the same name
blanchet
parents:
35964
diff
changeset
|
50 |
val serial_commas : string -> string list -> string list |
38188 | 51 |
val pretty_serial_commas : string -> Pretty.T list -> Pretty.T list |
36380
1e8fcaccb3e8
stop referring to Sledgehammer_Util stuff all over Nitpick code; instead, redeclare any needed function in Nitpick_Util as synonym for the Sledgehammer_Util function of the same name
blanchet
parents:
35964
diff
changeset
|
52 |
val parse_bool_option : bool -> string -> string -> bool option |
54816
10d48c2a3e32
made timeouts in Sledgehammer not be 'option's -- simplified lots of code
blanchet
parents:
54696
diff
changeset
|
53 |
val parse_time : string -> string -> Time.time |
52031
9a9238342963
tuning -- renamed '_from_' to '_of_' in Sledgehammer
blanchet
parents:
50557
diff
changeset
|
54 |
val string_of_time : Time.time -> string |
38652
e063be321438
perform eta-expansion of quantifier bodies in Sledgehammer translation when needed + transform elim rules later;
blanchet
parents:
38240
diff
changeset
|
55 |
val nat_subscript : int -> string |
33192 | 56 |
val flip_polarity : polarity -> polarity |
57 |
val prop_T : typ |
|
58 |
val bool_T : typ |
|
59 |
val nat_T : typ |
|
60 |
val int_T : typ |
|
37260
dde817e6dfb1
added "atoms" option to Nitpick (request from Karlsruhe) + wrap Refute. functions to "nitpick_util.ML"
blanchet
parents:
36555
diff
changeset
|
61 |
val simple_string_of_typ : typ -> string |
55080 | 62 |
val num_binder_types : typ -> int |
42697 | 63 |
val varify_type : Proof.context -> typ -> typ |
64 |
val instantiate_type : theory -> typ -> typ -> typ -> typ |
|
65 |
val varify_and_instantiate_type : Proof.context -> typ -> typ -> typ -> typ |
|
53806
de4653037e0d
don't generalize w.r.t. wrong context -- better overgeneralize (since the instantiation phase will compensate for it)
blanchet
parents:
53802
diff
changeset
|
66 |
val varify_and_instantiate_type_global : theory -> typ -> typ -> typ -> typ |
37260
dde817e6dfb1
added "atoms" option to Nitpick (request from Karlsruhe) + wrap Refute. functions to "nitpick_util.ML"
blanchet
parents:
36555
diff
changeset
|
67 |
val is_of_class_const : theory -> string * typ -> bool |
dde817e6dfb1
added "atoms" option to Nitpick (request from Karlsruhe) + wrap Refute. functions to "nitpick_util.ML"
blanchet
parents:
36555
diff
changeset
|
68 |
val get_class_def : theory -> string -> (string * term) option |
36555
8ff45c2076da
expand combinators in Isar proofs constructed by Sledgehammer;
blanchet
parents:
36483
diff
changeset
|
69 |
val monomorphic_term : Type.tyenv -> term -> term |
37260
dde817e6dfb1
added "atoms" option to Nitpick (request from Karlsruhe) + wrap Refute. functions to "nitpick_util.ML"
blanchet
parents:
36555
diff
changeset
|
70 |
val specialize_type : theory -> string * typ -> term -> term |
38652
e063be321438
perform eta-expansion of quantifier bodies in Sledgehammer translation when needed + transform elim rules later;
blanchet
parents:
38240
diff
changeset
|
71 |
val eta_expand : typ list -> term -> int -> term |
54816
10d48c2a3e32
made timeouts in Sledgehammer not be 'option's -- simplified lots of code
blanchet
parents:
54696
diff
changeset
|
72 |
val DETERM_TIMEOUT : Time.time -> tactic -> tactic |
33192 | 73 |
val indent_size : int |
74 |
val pstrs : string -> Pretty.T list |
|
34982
7b8c366e34a2
added support for nonstandard models to Nitpick (based on an idea by Koen Claessen) and did other fixes to Nitpick
blanchet
parents:
34936
diff
changeset
|
75 |
val unyxml : string -> string |
38188 | 76 |
val pretty_maybe_quote : Pretty.T -> Pretty.T |
43827
62d64709af3b
added option to control which lambda translation to use (for experiments)
blanchet
parents:
43085
diff
changeset
|
77 |
val hash_term : term -> int |
53815
e8aa538e959e
encode goal digest in spying log (to detect duplicates)
blanchet
parents:
53806
diff
changeset
|
78 |
val spying : bool -> (unit -> Proof.state * int * string) -> unit |
35866
513074557e06
move the Sledgehammer Isar commands together into one file;
blanchet
parents:
35807
diff
changeset
|
79 |
end; |
33192 | 80 |
|
33232
f93390060bbe
internal renaming in Nitpick and fixed Kodkodi invokation on Linux;
blanchet
parents:
33192
diff
changeset
|
81 |
structure Nitpick_Util : NITPICK_UTIL = |
33192 | 82 |
struct |
83 |
||
84 |
datatype polarity = Pos | Neg | Neut |
|
85 |
||
86 |
exception ARG of string * string |
|
87 |
exception BAD of string * string |
|
34124
c4628a1dcf75
added support for binary nat/int representation to Nitpick
blanchet
parents:
34039
diff
changeset
|
88 |
exception TOO_SMALL of string * string |
c4628a1dcf75
added support for binary nat/int representation to Nitpick
blanchet
parents:
34039
diff
changeset
|
89 |
exception TOO_LARGE of string * string |
33192 | 90 |
exception NOT_SUPPORTED of string |
91 |
exception SAME of unit |
|
92 |
||
46711
f745bcc4a1e5
more explicit Long_Name operations (NB: analyzing qualifiers is inherently fragile);
wenzelm
parents:
45896
diff
changeset
|
93 |
val nitpick_prefix = "Nitpick" ^ Long_Name.separator |
33192 | 94 |
|
53802 | 95 |
val timestamp = ATP_Util.timestamp |
96 |
||
33192 | 97 |
fun curry3 f = fn x => fn y => fn z => f (x, y, z) |
98 |
||
33705
947184dc75c9
removed a few global names in Nitpick (styp, nat_less, pairf)
blanchet
parents:
33232
diff
changeset
|
99 |
fun pairf f g x = (f x, g x) |
33192 | 100 |
|
35385
29f81babefd7
improved precision of infinite "shallow" datatypes in Nitpick;
blanchet
parents:
35280
diff
changeset
|
101 |
fun pair_from_fun f = (f false, f true) |
29f81babefd7
improved precision of infinite "shallow" datatypes in Nitpick;
blanchet
parents:
35280
diff
changeset
|
102 |
fun fun_from_pair (f, t) b = if b then t else f |
29f81babefd7
improved precision of infinite "shallow" datatypes in Nitpick;
blanchet
parents:
35280
diff
changeset
|
103 |
|
29f81babefd7
improved precision of infinite "shallow" datatypes in Nitpick;
blanchet
parents:
35280
diff
changeset
|
104 |
fun int_from_bool b = if b then 1 else 0 |
33705
947184dc75c9
removed a few global names in Nitpick (styp, nat_less, pairf)
blanchet
parents:
33232
diff
changeset
|
105 |
fun nat_minus i j = if i > j then i - j else 0 |
33192 | 106 |
|
107 |
val max_exponent = 16384 |
|
108 |
||
35280
54ab4921f826
fixed a few bugs in Nitpick and removed unreferenced variables
blanchet
parents:
35220
diff
changeset
|
109 |
fun reasonable_power _ 0 = 1 |
33192 | 110 |
| reasonable_power a 1 = a |
111 |
| reasonable_power 0 _ = 0 |
|
112 |
| reasonable_power 1 _ = 1 |
|
113 |
| reasonable_power a b = |
|
34124
c4628a1dcf75
added support for binary nat/int representation to Nitpick
blanchet
parents:
34039
diff
changeset
|
114 |
if b < 0 then |
c4628a1dcf75
added support for binary nat/int representation to Nitpick
blanchet
parents:
34039
diff
changeset
|
115 |
raise ARG ("Nitpick_Util.reasonable_power", |
c4628a1dcf75
added support for binary nat/int representation to Nitpick
blanchet
parents:
34039
diff
changeset
|
116 |
"negative exponent (" ^ signed_string_of_int b ^ ")") |
c4628a1dcf75
added support for binary nat/int representation to Nitpick
blanchet
parents:
34039
diff
changeset
|
117 |
else if b > max_exponent then |
c4628a1dcf75
added support for binary nat/int representation to Nitpick
blanchet
parents:
34039
diff
changeset
|
118 |
raise TOO_LARGE ("Nitpick_Util.reasonable_power", |
47667
b4f71d8aecd6
handle exception (needed to solve TPTP problem SEU880^5)
blanchet
parents:
46711
diff
changeset
|
119 |
"too large exponent (" ^ signed_string_of_int a ^ " ^ " ^ |
b4f71d8aecd6
handle exception (needed to solve TPTP problem SEU880^5)
blanchet
parents:
46711
diff
changeset
|
120 |
signed_string_of_int b ^ ")") |
33192 | 121 |
else |
34124
c4628a1dcf75
added support for binary nat/int representation to Nitpick
blanchet
parents:
34039
diff
changeset
|
122 |
let val c = reasonable_power a (b div 2) in |
c4628a1dcf75
added support for binary nat/int representation to Nitpick
blanchet
parents:
34039
diff
changeset
|
123 |
c * c * reasonable_power a (b mod 2) |
c4628a1dcf75
added support for binary nat/int representation to Nitpick
blanchet
parents:
34039
diff
changeset
|
124 |
end |
33192 | 125 |
|
126 |
fun exact_log m n = |
|
127 |
let |
|
128 |
val r = Math.ln (Real.fromInt n) / Math.ln (Real.fromInt m) |> Real.round |
|
129 |
in |
|
130 |
if reasonable_power m r = n then |
|
131 |
r |
|
132 |
else |
|
33232
f93390060bbe
internal renaming in Nitpick and fixed Kodkodi invokation on Linux;
blanchet
parents:
33192
diff
changeset
|
133 |
raise ARG ("Nitpick_Util.exact_log", |
33192 | 134 |
commas (map signed_string_of_int [m, n])) |
135 |
end |
|
136 |
||
137 |
fun exact_root m n = |
|
138 |
let val r = Math.pow (Real.fromInt n, 1.0 / (Real.fromInt m)) |> Real.round in |
|
139 |
if reasonable_power r m = n then |
|
140 |
r |
|
141 |
else |
|
33232
f93390060bbe
internal renaming in Nitpick and fixed Kodkodi invokation on Linux;
blanchet
parents:
33192
diff
changeset
|
142 |
raise ARG ("Nitpick_Util.exact_root", |
33192 | 143 |
commas (map signed_string_of_int [m, n])) |
144 |
end |
|
145 |
||
146 |
fun fold1 f = foldl1 (uncurry f) |
|
147 |
||
148 |
fun replicate_list 0 _ = [] |
|
149 |
| replicate_list n xs = xs @ replicate_list (n - 1) xs |
|
150 |
||
151 |
fun offset_list ns = rev (tl (fold (fn x => fn xs => (x + hd xs) :: xs) ns [0])) |
|
55889 | 152 |
|
33192 | 153 |
fun index_seq j0 n = if j0 < 0 then j0 downto j0 - n + 1 else j0 upto j0 + n - 1 |
154 |
||
155 |
fun filter_indices js xs = |
|
156 |
let |
|
157 |
fun aux _ [] _ = [] |
|
158 |
| aux i (j :: js) (x :: xs) = |
|
159 |
if i = j then x :: aux (i + 1) js xs else aux (i + 1) (j :: js) xs |
|
33232
f93390060bbe
internal renaming in Nitpick and fixed Kodkodi invokation on Linux;
blanchet
parents:
33192
diff
changeset
|
160 |
| aux _ _ _ = raise ARG ("Nitpick_Util.filter_indices", |
33192 | 161 |
"indices unordered or out of range") |
162 |
in aux 0 js xs end |
|
55889 | 163 |
|
33192 | 164 |
fun filter_out_indices js xs = |
165 |
let |
|
166 |
fun aux _ [] xs = xs |
|
167 |
| aux i (j :: js) (x :: xs) = |
|
168 |
if i = j then aux (i + 1) js xs else x :: aux (i + 1) (j :: js) xs |
|
33232
f93390060bbe
internal renaming in Nitpick and fixed Kodkodi invokation on Linux;
blanchet
parents:
33192
diff
changeset
|
169 |
| aux _ _ _ = raise ARG ("Nitpick_Util.filter_out_indices", |
33192 | 170 |
"indices unordered or out of range") |
171 |
in aux 0 js xs end |
|
172 |
||
57055
df3a26987a8d
reverted '|' features in MaSh -- these sounded like a good idea but never really worked
blanchet
parents:
55891
diff
changeset
|
173 |
fun cartesian_product [] _ = [] |
df3a26987a8d
reverted '|' features in MaSh -- these sounded like a good idea but never really worked
blanchet
parents:
55891
diff
changeset
|
174 |
| cartesian_product (x :: xs) yss = map (cons x) yss @ cartesian_product xs yss |
df3a26987a8d
reverted '|' features in MaSh -- these sounded like a good idea but never really worked
blanchet
parents:
55891
diff
changeset
|
175 |
|
df3a26987a8d
reverted '|' features in MaSh -- these sounded like a good idea but never really worked
blanchet
parents:
55891
diff
changeset
|
176 |
fun n_fold_cartesian_product xss = fold_rev cartesian_product xss [[]] |
54695 | 177 |
|
33192 | 178 |
fun all_distinct_unordered_pairs_of [] = [] |
179 |
| all_distinct_unordered_pairs_of (x :: xs) = |
|
180 |
map (pair x) xs @ all_distinct_unordered_pairs_of xs |
|
181 |
||
182 |
val nth_combination = |
|
183 |
let |
|
184 |
fun aux [] n = ([], n) |
|
185 |
| aux ((k, j0) :: xs) n = |
|
186 |
let val (js, n) = aux xs n in ((n mod k) + j0 :: js, n div k) end |
|
187 |
in fst oo aux end |
|
188 |
||
189 |
val all_combinations = n_fold_cartesian_product o map (uncurry index_seq o swap) |
|
190 |
||
191 |
fun all_permutations [] = [[]] |
|
192 |
| all_permutations xs = |
|
193 |
maps (fn j => map (cons (nth xs j)) (all_permutations (nth_drop j xs))) |
|
194 |
(index_seq 0 (length xs)) |
|
195 |
||
49206 | 196 |
(* FIXME: use "Library.chop_groups" *) |
48323 | 197 |
val chunk_list = ATP_Util.chunk_list |
33192 | 198 |
|
49206 | 199 |
(* FIXME: use "Library.unflat" *) |
33192 | 200 |
fun chunk_list_unevenly _ [] = [] |
48323 | 201 |
| chunk_list_unevenly [] xs = map single xs |
202 |
| chunk_list_unevenly (k :: ks) xs = |
|
203 |
let val (xs1, xs2) = chop k xs in xs1 :: chunk_list_unevenly ks xs2 end |
|
33192 | 204 |
|
205 |
fun map3 _ [] [] [] = [] |
|
206 |
| map3 f (x :: xs) (y :: ys) (z :: zs) = f x y z :: map3 f xs ys zs |
|
40722
441260986b63
make two copies (!) of Library.UnequalLengths coincide with ListPair.UnequalLengths;
wenzelm
parents:
40627
diff
changeset
|
207 |
| map3 _ _ _ _ = raise ListPair.UnequalLengths |
33192 | 208 |
|
209 |
fun double_lookup eq ps key = |
|
210 |
case AList.lookup (fn (SOME x, SOME y) => eq (x, y) | _ => false) ps |
|
211 |
(SOME key) of |
|
212 |
SOME z => SOME z |
|
213 |
| NONE => ps |> find_first (is_none o fst) |> Option.map snd |
|
55889 | 214 |
|
35220
2bcdae5f4fdb
added support for nonstandard "nat"s to Nitpick and fixed bugs in binary "nat"s and "int"s
blanchet
parents:
34982
diff
changeset
|
215 |
fun triple_lookup _ [(NONE, z)] _ = SOME z |
2bcdae5f4fdb
added support for nonstandard "nat"s to Nitpick and fixed bugs in binary "nat"s and "int"s
blanchet
parents:
34982
diff
changeset
|
216 |
| triple_lookup eq ps key = |
2bcdae5f4fdb
added support for nonstandard "nat"s to Nitpick and fixed bugs in binary "nat"s and "int"s
blanchet
parents:
34982
diff
changeset
|
217 |
case AList.lookup (op =) ps (SOME key) of |
2bcdae5f4fdb
added support for nonstandard "nat"s to Nitpick and fixed bugs in binary "nat"s and "int"s
blanchet
parents:
34982
diff
changeset
|
218 |
SOME z => SOME z |
2bcdae5f4fdb
added support for nonstandard "nat"s to Nitpick and fixed bugs in binary "nat"s and "int"s
blanchet
parents:
34982
diff
changeset
|
219 |
| NONE => double_lookup eq ps key |
33192 | 220 |
|
221 |
fun is_substring_of needle stack = |
|
222 |
not (Substring.isEmpty (snd (Substring.position needle |
|
223 |
(Substring.full stack)))) |
|
224 |
||
36380
1e8fcaccb3e8
stop referring to Sledgehammer_Util stuff all over Nitpick code; instead, redeclare any needed function in Nitpick_Util as synonym for the Sledgehammer_Util function of the same name
blanchet
parents:
35964
diff
changeset
|
225 |
val plural_s = Sledgehammer_Util.plural_s |
33192 | 226 |
fun plural_s_for_list xs = plural_s (length xs) |
227 |
||
43029
3e060b1c844b
use helpers and tweak Quickcheck's priority to it comes second (to give Solve Direct slightly more time before another prover runs)
blanchet
parents:
42697
diff
changeset
|
228 |
val serial_commas = Try.serial_commas |
36380
1e8fcaccb3e8
stop referring to Sledgehammer_Util stuff all over Nitpick code; instead, redeclare any needed function in Nitpick_Util as synonym for the Sledgehammer_Util function of the same name
blanchet
parents:
35964
diff
changeset
|
229 |
|
38188 | 230 |
fun pretty_serial_commas _ [] = [] |
231 |
| pretty_serial_commas _ [p] = [p] |
|
232 |
| pretty_serial_commas conj [p1, p2] = |
|
233 |
[p1, Pretty.brk 1, Pretty.str conj, Pretty.brk 1, p2] |
|
234 |
| pretty_serial_commas conj [p1, p2, p3] = |
|
235 |
[p1, Pretty.str ",", Pretty.brk 1, p2, Pretty.str ",", Pretty.brk 1, |
|
236 |
Pretty.str conj, Pretty.brk 1, p3] |
|
237 |
| pretty_serial_commas conj (p :: ps) = |
|
238 |
p :: Pretty.str "," :: Pretty.brk 1 :: pretty_serial_commas conj ps |
|
239 |
||
36380
1e8fcaccb3e8
stop referring to Sledgehammer_Util stuff all over Nitpick code; instead, redeclare any needed function in Nitpick_Util as synonym for the Sledgehammer_Util function of the same name
blanchet
parents:
35964
diff
changeset
|
240 |
val parse_bool_option = Sledgehammer_Util.parse_bool_option |
54816
10d48c2a3e32
made timeouts in Sledgehammer not be 'option's -- simplified lots of code
blanchet
parents:
54696
diff
changeset
|
241 |
val parse_time = Sledgehammer_Util.parse_time |
52031
9a9238342963
tuning -- renamed '_from_' to '_of_' in Sledgehammer
blanchet
parents:
50557
diff
changeset
|
242 |
val string_of_time = ATP_Util.string_of_time |
36380
1e8fcaccb3e8
stop referring to Sledgehammer_Util stuff all over Nitpick code; instead, redeclare any needed function in Nitpick_Util as synonym for the Sledgehammer_Util function of the same name
blanchet
parents:
35964
diff
changeset
|
243 |
|
53021
d0fa3f446b9d
discontinued special treatment of \<^isub> and \<^isup> in rendering or editor front-end;
wenzelm
parents:
53015
diff
changeset
|
244 |
val subscript = implode o map (prefix "\<^sub>") o Symbol.explode |
55889 | 245 |
|
38652
e063be321438
perform eta-expansion of quantifier bodies in Sledgehammer translation when needed + transform elim rules later;
blanchet
parents:
38240
diff
changeset
|
246 |
fun nat_subscript n = |
53021
d0fa3f446b9d
discontinued special treatment of \<^isub> and \<^isup> in rendering or editor front-end;
wenzelm
parents:
53015
diff
changeset
|
247 |
n |> signed_string_of_int |> print_mode_active Symbol.xsymbolsN ? subscript |
38652
e063be321438
perform eta-expansion of quantifier bodies in Sledgehammer translation when needed + transform elim rules later;
blanchet
parents:
38240
diff
changeset
|
248 |
|
33192 | 249 |
fun flip_polarity Pos = Neg |
250 |
| flip_polarity Neg = Pos |
|
251 |
| flip_polarity Neut = Neut |
|
252 |
||
253 |
val prop_T = @{typ prop} |
|
254 |
val bool_T = @{typ bool} |
|
255 |
val nat_T = @{typ nat} |
|
256 |
val int_T = @{typ int} |
|
257 |
||
55080 | 258 |
fun simple_string_of_typ (Type (s, _)) = s |
259 |
| simple_string_of_typ (TFree (s, _)) = s |
|
49985
5b4b0e4e5205
moved Refute to "HOL/Library" to speed up building "Main" even more
blanchet
parents:
49206
diff
changeset
|
260 |
| simple_string_of_typ (TVar ((s, _), _)) = s |
5b4b0e4e5205
moved Refute to "HOL/Library" to speed up building "Main" even more
blanchet
parents:
49206
diff
changeset
|
261 |
|
55080 | 262 |
val num_binder_types = BNF_Util.num_binder_types |
263 |
||
43085
0a2f5b86bdd7
first step in sharing more code between ATP and Metis translation
blanchet
parents:
43029
diff
changeset
|
264 |
val varify_type = ATP_Util.varify_type |
0a2f5b86bdd7
first step in sharing more code between ATP and Metis translation
blanchet
parents:
43029
diff
changeset
|
265 |
val instantiate_type = ATP_Util.instantiate_type |
0a2f5b86bdd7
first step in sharing more code between ATP and Metis translation
blanchet
parents:
43029
diff
changeset
|
266 |
val varify_and_instantiate_type = ATP_Util.varify_and_instantiate_type |
49985
5b4b0e4e5205
moved Refute to "HOL/Library" to speed up building "Main" even more
blanchet
parents:
49206
diff
changeset
|
267 |
|
53806
de4653037e0d
don't generalize w.r.t. wrong context -- better overgeneralize (since the instantiation phase will compensate for it)
blanchet
parents:
53802
diff
changeset
|
268 |
fun varify_and_instantiate_type_global thy T1 T1' T2 = |
de4653037e0d
don't generalize w.r.t. wrong context -- better overgeneralize (since the instantiation phase will compensate for it)
blanchet
parents:
53802
diff
changeset
|
269 |
instantiate_type thy (Logic.varifyT_global T1) T1' (Logic.varifyT_global T2) |
de4653037e0d
don't generalize w.r.t. wrong context -- better overgeneralize (since the instantiation phase will compensate for it)
blanchet
parents:
53802
diff
changeset
|
270 |
|
49985
5b4b0e4e5205
moved Refute to "HOL/Library" to speed up building "Main" even more
blanchet
parents:
49206
diff
changeset
|
271 |
fun is_of_class_const thy (s, _) = |
5b4b0e4e5205
moved Refute to "HOL/Library" to speed up building "Main" even more
blanchet
parents:
49206
diff
changeset
|
272 |
member (op =) (map Logic.const_of_class (Sign.all_classes thy)) s |
5b4b0e4e5205
moved Refute to "HOL/Library" to speed up building "Main" even more
blanchet
parents:
49206
diff
changeset
|
273 |
|
5b4b0e4e5205
moved Refute to "HOL/Library" to speed up building "Main" even more
blanchet
parents:
49206
diff
changeset
|
274 |
fun get_class_def thy class = |
5b4b0e4e5205
moved Refute to "HOL/Library" to speed up building "Main" even more
blanchet
parents:
49206
diff
changeset
|
275 |
let val axname = class ^ "_class_def" in |
5b4b0e4e5205
moved Refute to "HOL/Library" to speed up building "Main" even more
blanchet
parents:
49206
diff
changeset
|
276 |
Option.map (pair axname) |
5b4b0e4e5205
moved Refute to "HOL/Library" to speed up building "Main" even more
blanchet
parents:
49206
diff
changeset
|
277 |
(AList.lookup (op =) (Theory.all_axioms_of thy) axname) |
5b4b0e4e5205
moved Refute to "HOL/Library" to speed up building "Main" even more
blanchet
parents:
49206
diff
changeset
|
278 |
end; |
5b4b0e4e5205
moved Refute to "HOL/Library" to speed up building "Main" even more
blanchet
parents:
49206
diff
changeset
|
279 |
|
43085
0a2f5b86bdd7
first step in sharing more code between ATP and Metis translation
blanchet
parents:
43029
diff
changeset
|
280 |
val monomorphic_term = ATP_Util.monomorphic_term |
0a2f5b86bdd7
first step in sharing more code between ATP and Metis translation
blanchet
parents:
43029
diff
changeset
|
281 |
val specialize_type = ATP_Util.specialize_type |
0a2f5b86bdd7
first step in sharing more code between ATP and Metis translation
blanchet
parents:
43029
diff
changeset
|
282 |
val eta_expand = ATP_Util.eta_expand |
33192 | 283 |
|
284 |
fun DETERM_TIMEOUT delay tac st = |
|
54816
10d48c2a3e32
made timeouts in Sledgehammer not be 'option's -- simplified lots of code
blanchet
parents:
54696
diff
changeset
|
285 |
Seq.of_list (the_list (TimeLimit.timeLimit delay (fn () => SINGLE tac st) ())) |
33192 | 286 |
|
287 |
val indent_size = 2 |
|
288 |
||
289 |
val pstrs = Pretty.breaks o map Pretty.str o space_explode " " |
|
290 |
||
43085
0a2f5b86bdd7
first step in sharing more code between ATP and Metis translation
blanchet
parents:
43029
diff
changeset
|
291 |
val unyxml = ATP_Util.unyxml |
38188 | 292 |
|
43085
0a2f5b86bdd7
first step in sharing more code between ATP and Metis translation
blanchet
parents:
43029
diff
changeset
|
293 |
val maybe_quote = ATP_Util.maybe_quote |
55889 | 294 |
|
38188 | 295 |
fun pretty_maybe_quote pretty = |
296 |
let val s = Pretty.str_of pretty in |
|
297 |
if maybe_quote s = s then pretty else Pretty.enum "" "\"" "\"" [pretty] |
|
298 |
end |
|
33192 | 299 |
|
53802 | 300 |
val hashw = ATP_Util.hashw |
301 |
val hashw_string = ATP_Util.hashw_string |
|
302 |
||
303 |
fun hashw_term (t1 $ t2) = hashw (hashw_term t1, hashw_term t2) |
|
304 |
| hashw_term (Const (s, _)) = hashw_string (s, 0w0) |
|
305 |
| hashw_term (Free (s, _)) = hashw_string (s, 0w0) |
|
53505 | 306 |
| hashw_term _ = 0w0 |
307 |
||
308 |
val hash_term = Word.toInt o hashw_term |
|
36380
1e8fcaccb3e8
stop referring to Sledgehammer_Util stuff all over Nitpick code; instead, redeclare any needed function in Nitpick_Util as synonym for the Sledgehammer_Util function of the same name
blanchet
parents:
35964
diff
changeset
|
309 |
|
53815
e8aa538e959e
encode goal digest in spying log (to detect duplicates)
blanchet
parents:
53806
diff
changeset
|
310 |
val hackish_string_of_term = Sledgehammer_Util.hackish_string_of_term |
e8aa538e959e
encode goal digest in spying log (to detect duplicates)
blanchet
parents:
53806
diff
changeset
|
311 |
|
e8aa538e959e
encode goal digest in spying log (to detect duplicates)
blanchet
parents:
53806
diff
changeset
|
312 |
val spying_version = "b" |
e8aa538e959e
encode goal digest in spying log (to detect duplicates)
blanchet
parents:
53806
diff
changeset
|
313 |
|
e8aa538e959e
encode goal digest in spying log (to detect duplicates)
blanchet
parents:
53806
diff
changeset
|
314 |
fun spying false _ = () |
e8aa538e959e
encode goal digest in spying log (to detect duplicates)
blanchet
parents:
53806
diff
changeset
|
315 |
| spying true f = |
e8aa538e959e
encode goal digest in spying log (to detect duplicates)
blanchet
parents:
53806
diff
changeset
|
316 |
let |
e8aa538e959e
encode goal digest in spying log (to detect duplicates)
blanchet
parents:
53806
diff
changeset
|
317 |
val (state, i, message) = f () |
e8aa538e959e
encode goal digest in spying log (to detect duplicates)
blanchet
parents:
53806
diff
changeset
|
318 |
val ctxt = Proof.context_of state |
e8aa538e959e
encode goal digest in spying log (to detect duplicates)
blanchet
parents:
53806
diff
changeset
|
319 |
val goal = Logic.get_goal (prop_of (#goal (Proof.goal state))) i |
e8aa538e959e
encode goal digest in spying log (to detect duplicates)
blanchet
parents:
53806
diff
changeset
|
320 |
val hash = String.substring (SHA1.rep (SHA1.digest (hackish_string_of_term ctxt goal)), 0, 12) |
e8aa538e959e
encode goal digest in spying log (to detect duplicates)
blanchet
parents:
53806
diff
changeset
|
321 |
in |
e8aa538e959e
encode goal digest in spying log (to detect duplicates)
blanchet
parents:
53806
diff
changeset
|
322 |
File.append (Path.explode "$ISABELLE_HOME_USER/spy_nitpick") |
e8aa538e959e
encode goal digest in spying log (to detect duplicates)
blanchet
parents:
53806
diff
changeset
|
323 |
(spying_version ^ " " ^ timestamp () ^ ": " ^ hash ^ ": " ^ message ^ "\n") |
e8aa538e959e
encode goal digest in spying log (to detect duplicates)
blanchet
parents:
53806
diff
changeset
|
324 |
end |
e8aa538e959e
encode goal digest in spying log (to detect duplicates)
blanchet
parents:
53806
diff
changeset
|
325 |
|
33192 | 326 |
end; |