|
1 (* Title: HOL/Tools/Nitpick/nitpick_preproc.ML |
|
2 Author: Jasmin Blanchette, TU Muenchen |
|
3 Copyright 2008, 2009, 2010 |
|
4 |
|
5 Nitpick's HOL preprocessor. |
|
6 *) |
|
7 |
|
8 signature NITPICK_PREPROC = |
|
9 sig |
|
10 type hol_context = Nitpick_HOL.hol_context |
|
11 val preprocess_term : |
|
12 hol_context -> term -> ((term list * term list) * (bool * bool)) * term |
|
13 end |
|
14 |
|
15 structure Nitpick_Preproc : NITPICK_PREPROC = |
|
16 struct |
|
17 |
|
18 open Nitpick_Util |
|
19 open Nitpick_HOL |
|
20 |
|
21 (* polarity -> string -> bool *) |
|
22 fun is_positive_existential polar quant_s = |
|
23 (polar = Pos andalso quant_s = @{const_name Ex}) orelse |
|
24 (polar = Neg andalso quant_s <> @{const_name Ex}) |
|
25 |
|
26 (** Binary coding of integers **) |
|
27 |
|
28 (* If a formula contains a numeral whose absolute value is more than this |
|
29 threshold, the unary coding is likely not to work well and we prefer the |
|
30 binary coding. *) |
|
31 val binary_int_threshold = 3 |
|
32 |
|
33 (* term -> bool *) |
|
34 fun may_use_binary_ints (t1 $ t2) = |
|
35 may_use_binary_ints t1 andalso may_use_binary_ints t2 |
|
36 | may_use_binary_ints (t as Const (s, _)) = |
|
37 t <> @{const Suc} andalso |
|
38 not (member (op =) [@{const_name Abs_Frac}, @{const_name Rep_Frac}, |
|
39 @{const_name nat_gcd}, @{const_name nat_lcm}, |
|
40 @{const_name Frac}, @{const_name norm_frac}] s) |
|
41 | may_use_binary_ints (Abs (_, _, t')) = may_use_binary_ints t' |
|
42 | may_use_binary_ints _ = true |
|
43 fun should_use_binary_ints (t1 $ t2) = |
|
44 should_use_binary_ints t1 orelse should_use_binary_ints t2 |
|
45 | should_use_binary_ints (Const (s, _)) = |
|
46 member (op =) [@{const_name times_nat_inst.times_nat}, |
|
47 @{const_name div_nat_inst.div_nat}, |
|
48 @{const_name times_int_inst.times_int}, |
|
49 @{const_name div_int_inst.div_int}] s orelse |
|
50 (String.isPrefix numeral_prefix s andalso |
|
51 let val n = the (Int.fromString (unprefix numeral_prefix s)) in |
|
52 n < ~ binary_int_threshold orelse n > binary_int_threshold |
|
53 end) |
|
54 | should_use_binary_ints (Abs (_, _, t')) = should_use_binary_ints t' |
|
55 | should_use_binary_ints _ = false |
|
56 |
|
57 (* typ -> typ *) |
|
58 fun binarize_nat_and_int_in_type @{typ nat} = @{typ "unsigned_bit word"} |
|
59 | binarize_nat_and_int_in_type @{typ int} = @{typ "signed_bit word"} |
|
60 | binarize_nat_and_int_in_type (Type (s, Ts)) = |
|
61 Type (s, map binarize_nat_and_int_in_type Ts) |
|
62 | binarize_nat_and_int_in_type T = T |
|
63 (* term -> term *) |
|
64 val binarize_nat_and_int_in_term = map_types binarize_nat_and_int_in_type |
|
65 |
|
66 (** Uncurrying **) |
|
67 |
|
68 (* theory -> term -> int Termtab.tab -> int Termtab.tab *) |
|
69 fun add_to_uncurry_table thy t = |
|
70 let |
|
71 (* term -> term list -> int Termtab.tab -> int Termtab.tab *) |
|
72 fun aux (t1 $ t2) args table = |
|
73 let val table = aux t2 [] table in aux t1 (t2 :: args) table end |
|
74 | aux (Abs (_, _, t')) _ table = aux t' [] table |
|
75 | aux (t as Const (x as (s, _))) args table = |
|
76 if is_built_in_const true x orelse is_constr_like thy x orelse |
|
77 is_sel s orelse s = @{const_name Sigma} then |
|
78 table |
|
79 else |
|
80 Termtab.map_default (t, 65536) (curry Int.min (length args)) table |
|
81 | aux _ _ table = table |
|
82 in aux t [] end |
|
83 |
|
84 (* int -> int -> string *) |
|
85 fun uncurry_prefix_for k j = |
|
86 uncurry_prefix ^ string_of_int k ^ "@" ^ string_of_int j ^ name_sep |
|
87 |
|
88 (* int Termtab.tab term -> term *) |
|
89 fun uncurry_term table t = |
|
90 let |
|
91 (* term -> term list -> term *) |
|
92 fun aux (t1 $ t2) args = aux t1 (aux t2 [] :: args) |
|
93 | aux (Abs (s, T, t')) args = betapplys (Abs (s, T, aux t' []), args) |
|
94 | aux (t as Const (s, T)) args = |
|
95 (case Termtab.lookup table t of |
|
96 SOME n => |
|
97 if n >= 2 then |
|
98 let |
|
99 val (arg_Ts, rest_T) = strip_n_binders n T |
|
100 val j = |
|
101 if hd arg_Ts = @{typ bisim_iterator} orelse |
|
102 is_fp_iterator_type (hd arg_Ts) then |
|
103 1 |
|
104 else case find_index (not_equal bool_T) arg_Ts of |
|
105 ~1 => n |
|
106 | j => j |
|
107 val ((before_args, tuple_args), after_args) = |
|
108 args |> chop n |>> chop j |
|
109 val ((before_arg_Ts, tuple_arg_Ts), rest_T) = |
|
110 T |> strip_n_binders n |>> chop j |
|
111 val tuple_T = HOLogic.mk_tupleT tuple_arg_Ts |
|
112 in |
|
113 if n - j < 2 then |
|
114 betapplys (t, args) |
|
115 else |
|
116 betapplys (Const (uncurry_prefix_for (n - j) j ^ s, |
|
117 before_arg_Ts ---> tuple_T --> rest_T), |
|
118 before_args @ [mk_flat_tuple tuple_T tuple_args] @ |
|
119 after_args) |
|
120 end |
|
121 else |
|
122 betapplys (t, args) |
|
123 | NONE => betapplys (t, args)) |
|
124 | aux t args = betapplys (t, args) |
|
125 in aux t [] end |
|
126 |
|
127 (** Boxing **) |
|
128 |
|
129 (* hol_context -> typ -> term -> term *) |
|
130 fun constr_expand (hol_ctxt as {thy, ...}) T t = |
|
131 (case head_of t of |
|
132 Const x => if is_constr_like thy x then t else raise SAME () |
|
133 | _ => raise SAME ()) |
|
134 handle SAME () => |
|
135 let |
|
136 val x' as (_, T') = |
|
137 if is_pair_type T then |
|
138 let val (T1, T2) = HOLogic.dest_prodT T in |
|
139 (@{const_name Pair}, T1 --> T2 --> T) |
|
140 end |
|
141 else |
|
142 datatype_constrs hol_ctxt T |> hd |
|
143 val arg_Ts = binder_types T' |
|
144 in |
|
145 list_comb (Const x', map2 (select_nth_constr_arg thy x' t) |
|
146 (index_seq 0 (length arg_Ts)) arg_Ts) |
|
147 end |
|
148 |
|
149 (* hol_context -> bool -> term -> term *) |
|
150 fun box_fun_and_pair_in_term (hol_ctxt as {thy, fast_descrs, ...}) def orig_t = |
|
151 let |
|
152 (* typ -> typ *) |
|
153 fun box_relational_operator_type (Type ("fun", Ts)) = |
|
154 Type ("fun", map box_relational_operator_type Ts) |
|
155 | box_relational_operator_type (Type ("*", Ts)) = |
|
156 Type ("*", map (box_type hol_ctxt InPair) Ts) |
|
157 | box_relational_operator_type T = T |
|
158 (* (term -> term) -> int -> term -> term *) |
|
159 fun coerce_bound_no f j t = |
|
160 case t of |
|
161 t1 $ t2 => coerce_bound_no f j t1 $ coerce_bound_no f j t2 |
|
162 | Abs (s, T, t') => Abs (s, T, coerce_bound_no f (j + 1) t') |
|
163 | Bound j' => if j' = j then f t else t |
|
164 | _ => t |
|
165 (* typ -> typ -> term -> term *) |
|
166 fun coerce_bound_0_in_term new_T old_T = |
|
167 old_T <> new_T ? coerce_bound_no (coerce_term [new_T] old_T new_T) 0 |
|
168 (* typ list -> typ -> term -> term *) |
|
169 and coerce_term Ts new_T old_T t = |
|
170 if old_T = new_T then |
|
171 t |
|
172 else |
|
173 case (new_T, old_T) of |
|
174 (Type (new_s, new_Ts as [new_T1, new_T2]), |
|
175 Type ("fun", [old_T1, old_T2])) => |
|
176 (case eta_expand Ts t 1 of |
|
177 Abs (s, _, t') => |
|
178 Abs (s, new_T1, |
|
179 t' |> coerce_bound_0_in_term new_T1 old_T1 |
|
180 |> coerce_term (new_T1 :: Ts) new_T2 old_T2) |
|
181 |> Envir.eta_contract |
|
182 |> new_s <> "fun" |
|
183 ? construct_value thy (@{const_name FunBox}, |
|
184 Type ("fun", new_Ts) --> new_T) o single |
|
185 | t' => raise TERM ("Nitpick_Preproc.box_fun_and_pair_in_term.\ |
|
186 \coerce_term", [t'])) |
|
187 | (Type (new_s, new_Ts as [new_T1, new_T2]), |
|
188 Type (old_s, old_Ts as [old_T1, old_T2])) => |
|
189 if old_s = @{type_name fun_box} orelse |
|
190 old_s = @{type_name pair_box} orelse old_s = "*" then |
|
191 case constr_expand hol_ctxt old_T t of |
|
192 Const (@{const_name FunBox}, _) $ t1 => |
|
193 if new_s = "fun" then |
|
194 coerce_term Ts new_T (Type ("fun", old_Ts)) t1 |
|
195 else |
|
196 construct_value thy |
|
197 (@{const_name FunBox}, Type ("fun", new_Ts) --> new_T) |
|
198 [coerce_term Ts (Type ("fun", new_Ts)) |
|
199 (Type ("fun", old_Ts)) t1] |
|
200 | Const _ $ t1 $ t2 => |
|
201 construct_value thy |
|
202 (if new_s = "*" then @{const_name Pair} |
|
203 else @{const_name PairBox}, new_Ts ---> new_T) |
|
204 [coerce_term Ts new_T1 old_T1 t1, |
|
205 coerce_term Ts new_T2 old_T2 t2] |
|
206 | t' => raise TERM ("Nitpick_Preproc.box_fun_and_pair_in_term.\ |
|
207 \coerce_term", [t']) |
|
208 else |
|
209 raise TYPE ("coerce_term", [new_T, old_T], [t]) |
|
210 | _ => raise TYPE ("coerce_term", [new_T, old_T], [t]) |
|
211 (* indexname * typ -> typ * term -> typ option list -> typ option list *) |
|
212 fun add_boxed_types_for_var (z as (_, T)) (T', t') = |
|
213 case t' of |
|
214 Var z' => z' = z ? insert (op =) T' |
|
215 | Const (@{const_name Pair}, _) $ t1 $ t2 => |
|
216 (case T' of |
|
217 Type (_, [T1, T2]) => |
|
218 fold (add_boxed_types_for_var z) [(T1, t1), (T2, t2)] |
|
219 | _ => raise TYPE ("Nitpick_Preproc.box_fun_and_pair_in_term.\ |
|
220 \add_boxed_types_for_var", [T'], [])) |
|
221 | _ => exists_subterm (curry (op =) (Var z)) t' ? insert (op =) T |
|
222 (* typ list -> typ list -> term -> indexname * typ -> typ *) |
|
223 fun box_var_in_def new_Ts old_Ts t (z as (_, T)) = |
|
224 case t of |
|
225 @{const Trueprop} $ t1 => box_var_in_def new_Ts old_Ts t1 z |
|
226 | Const (s0, _) $ t1 $ _ => |
|
227 if s0 = @{const_name "=="} orelse s0 = @{const_name "op ="} then |
|
228 let |
|
229 val (t', args) = strip_comb t1 |
|
230 val T' = fastype_of1 (new_Ts, do_term new_Ts old_Ts Neut t') |
|
231 in |
|
232 case fold (add_boxed_types_for_var z) |
|
233 (fst (strip_n_binders (length args) T') ~~ args) [] of |
|
234 [T''] => T'' |
|
235 | _ => T |
|
236 end |
|
237 else |
|
238 T |
|
239 | _ => T |
|
240 (* typ list -> typ list -> polarity -> string -> typ -> string -> typ |
|
241 -> term -> term *) |
|
242 and do_quantifier new_Ts old_Ts polar quant_s quant_T abs_s abs_T t = |
|
243 let |
|
244 val abs_T' = |
|
245 if polar = Neut orelse is_positive_existential polar quant_s then |
|
246 box_type hol_ctxt InFunLHS abs_T |
|
247 else |
|
248 abs_T |
|
249 val body_T = body_type quant_T |
|
250 in |
|
251 Const (quant_s, (abs_T' --> body_T) --> body_T) |
|
252 $ Abs (abs_s, abs_T', |
|
253 t |> do_term (abs_T' :: new_Ts) (abs_T :: old_Ts) polar) |
|
254 end |
|
255 (* typ list -> typ list -> string -> typ -> term -> term -> term *) |
|
256 and do_equals new_Ts old_Ts s0 T0 t1 t2 = |
|
257 let |
|
258 val (t1, t2) = pairself (do_term new_Ts old_Ts Neut) (t1, t2) |
|
259 val (T1, T2) = pairself (curry fastype_of1 new_Ts) (t1, t2) |
|
260 val T = [T1, T2] |> sort TermOrd.typ_ord |> List.last |
|
261 in |
|
262 list_comb (Const (s0, T --> T --> body_type T0), |
|
263 map2 (coerce_term new_Ts T) [T1, T2] [t1, t2]) |
|
264 end |
|
265 (* string -> typ -> term *) |
|
266 and do_description_operator s T = |
|
267 let val T1 = box_type hol_ctxt InFunLHS (range_type T) in |
|
268 Const (s, (T1 --> bool_T) --> T1) |
|
269 end |
|
270 (* typ list -> typ list -> polarity -> term -> term *) |
|
271 and do_term new_Ts old_Ts polar t = |
|
272 case t of |
|
273 Const (s0 as @{const_name all}, T0) $ Abs (s1, T1, t1) => |
|
274 do_quantifier new_Ts old_Ts polar s0 T0 s1 T1 t1 |
|
275 | Const (s0 as @{const_name "=="}, T0) $ t1 $ t2 => |
|
276 do_equals new_Ts old_Ts s0 T0 t1 t2 |
|
277 | @{const "==>"} $ t1 $ t2 => |
|
278 @{const "==>"} $ do_term new_Ts old_Ts (flip_polarity polar) t1 |
|
279 $ do_term new_Ts old_Ts polar t2 |
|
280 | @{const Pure.conjunction} $ t1 $ t2 => |
|
281 @{const Pure.conjunction} $ do_term new_Ts old_Ts polar t1 |
|
282 $ do_term new_Ts old_Ts polar t2 |
|
283 | @{const Trueprop} $ t1 => |
|
284 @{const Trueprop} $ do_term new_Ts old_Ts polar t1 |
|
285 | @{const Not} $ t1 => |
|
286 @{const Not} $ do_term new_Ts old_Ts (flip_polarity polar) t1 |
|
287 | Const (s0 as @{const_name All}, T0) $ Abs (s1, T1, t1) => |
|
288 do_quantifier new_Ts old_Ts polar s0 T0 s1 T1 t1 |
|
289 | Const (s0 as @{const_name Ex}, T0) $ Abs (s1, T1, t1) => |
|
290 do_quantifier new_Ts old_Ts polar s0 T0 s1 T1 t1 |
|
291 | Const (s0 as @{const_name "op ="}, T0) $ t1 $ t2 => |
|
292 do_equals new_Ts old_Ts s0 T0 t1 t2 |
|
293 | @{const "op &"} $ t1 $ t2 => |
|
294 @{const "op &"} $ do_term new_Ts old_Ts polar t1 |
|
295 $ do_term new_Ts old_Ts polar t2 |
|
296 | @{const "op |"} $ t1 $ t2 => |
|
297 @{const "op |"} $ do_term new_Ts old_Ts polar t1 |
|
298 $ do_term new_Ts old_Ts polar t2 |
|
299 | @{const "op -->"} $ t1 $ t2 => |
|
300 @{const "op -->"} $ do_term new_Ts old_Ts (flip_polarity polar) t1 |
|
301 $ do_term new_Ts old_Ts polar t2 |
|
302 | Const (s as @{const_name The}, T) => do_description_operator s T |
|
303 | Const (s as @{const_name Eps}, T) => do_description_operator s T |
|
304 | Const (@{const_name quot_normal}, Type ("fun", [_, T2])) => |
|
305 let val T' = box_type hol_ctxt InSel T2 in |
|
306 Const (@{const_name quot_normal}, T' --> T') |
|
307 end |
|
308 | Const (s as @{const_name Tha}, T) => do_description_operator s T |
|
309 | Const (x as (s, T)) => |
|
310 Const (s, if s = @{const_name converse} orelse |
|
311 s = @{const_name trancl} then |
|
312 box_relational_operator_type T |
|
313 else if is_built_in_const fast_descrs x orelse |
|
314 s = @{const_name Sigma} then |
|
315 T |
|
316 else if is_constr_like thy x then |
|
317 box_type hol_ctxt InConstr T |
|
318 else if is_sel s |
|
319 orelse is_rep_fun thy x then |
|
320 box_type hol_ctxt InSel T |
|
321 else |
|
322 box_type hol_ctxt InExpr T) |
|
323 | t1 $ Abs (s, T, t2') => |
|
324 let |
|
325 val t1 = do_term new_Ts old_Ts Neut t1 |
|
326 val T1 = fastype_of1 (new_Ts, t1) |
|
327 val (s1, Ts1) = dest_Type T1 |
|
328 val T' = hd (snd (dest_Type (hd Ts1))) |
|
329 val t2 = Abs (s, T', do_term (T' :: new_Ts) (T :: old_Ts) Neut t2') |
|
330 val T2 = fastype_of1 (new_Ts, t2) |
|
331 val t2 = coerce_term new_Ts (hd Ts1) T2 t2 |
|
332 in |
|
333 betapply (if s1 = "fun" then |
|
334 t1 |
|
335 else |
|
336 select_nth_constr_arg thy |
|
337 (@{const_name FunBox}, Type ("fun", Ts1) --> T1) t1 0 |
|
338 (Type ("fun", Ts1)), t2) |
|
339 end |
|
340 | t1 $ t2 => |
|
341 let |
|
342 val t1 = do_term new_Ts old_Ts Neut t1 |
|
343 val T1 = fastype_of1 (new_Ts, t1) |
|
344 val (s1, Ts1) = dest_Type T1 |
|
345 val t2 = do_term new_Ts old_Ts Neut t2 |
|
346 val T2 = fastype_of1 (new_Ts, t2) |
|
347 val t2 = coerce_term new_Ts (hd Ts1) T2 t2 |
|
348 in |
|
349 betapply (if s1 = "fun" then |
|
350 t1 |
|
351 else |
|
352 select_nth_constr_arg thy |
|
353 (@{const_name FunBox}, Type ("fun", Ts1) --> T1) t1 0 |
|
354 (Type ("fun", Ts1)), t2) |
|
355 end |
|
356 | Free (s, T) => Free (s, box_type hol_ctxt InExpr T) |
|
357 | Var (z as (x, T)) => |
|
358 Var (x, if def then box_var_in_def new_Ts old_Ts orig_t z |
|
359 else box_type hol_ctxt InExpr T) |
|
360 | Bound _ => t |
|
361 | Abs (s, T, t') => |
|
362 Abs (s, T, do_term (T :: new_Ts) (T :: old_Ts) Neut t') |
|
363 in do_term [] [] Pos orig_t end |
|
364 |
|
365 (** Destruction of constructors **) |
|
366 |
|
367 val val_var_prefix = nitpick_prefix ^ "v" |
|
368 |
|
369 (* typ list -> int -> int -> int -> term -> term *) |
|
370 fun fresh_value_var Ts k n j t = |
|
371 Var ((val_var_prefix ^ nat_subscript (n - j), k), fastype_of1 (Ts, t)) |
|
372 |
|
373 (* typ list -> int -> term -> bool *) |
|
374 fun has_heavy_bounds_or_vars Ts level t = |
|
375 let |
|
376 (* typ list -> bool *) |
|
377 fun aux [] = false |
|
378 | aux [T] = is_fun_type T orelse is_pair_type T |
|
379 | aux _ = true |
|
380 in aux (map snd (Term.add_vars t []) @ map (nth Ts) (loose_bnos t)) end |
|
381 |
|
382 (* theory -> typ list -> bool -> int -> int -> term -> term list -> term list |
|
383 -> term * term list *) |
|
384 fun pull_out_constr_comb thy Ts relax k level t args seen = |
|
385 let val t_comb = list_comb (t, args) in |
|
386 case t of |
|
387 Const x => |
|
388 if not relax andalso is_constr thy x andalso |
|
389 not (is_fun_type (fastype_of1 (Ts, t_comb))) andalso |
|
390 has_heavy_bounds_or_vars Ts level t_comb andalso |
|
391 not (loose_bvar (t_comb, level)) then |
|
392 let |
|
393 val (j, seen) = case find_index (curry (op =) t_comb) seen of |
|
394 ~1 => (0, t_comb :: seen) |
|
395 | j => (j, seen) |
|
396 in (fresh_value_var Ts k (length seen) j t_comb, seen) end |
|
397 else |
|
398 (t_comb, seen) |
|
399 | _ => (t_comb, seen) |
|
400 end |
|
401 |
|
402 (* (term -> term) -> typ list -> int -> term list -> term list *) |
|
403 fun equations_for_pulled_out_constrs mk_eq Ts k seen = |
|
404 let val n = length seen in |
|
405 map2 (fn j => fn t => mk_eq (fresh_value_var Ts k n j t, t)) |
|
406 (index_seq 0 n) seen |
|
407 end |
|
408 |
|
409 (* theory -> bool -> term -> term *) |
|
410 fun pull_out_universal_constrs thy def t = |
|
411 let |
|
412 val k = maxidx_of_term t + 1 |
|
413 (* typ list -> bool -> term -> term list -> term list -> term * term list *) |
|
414 fun do_term Ts def t args seen = |
|
415 case t of |
|
416 (t0 as Const (@{const_name "=="}, _)) $ t1 $ t2 => |
|
417 do_eq_or_imp Ts true def t0 t1 t2 seen |
|
418 | (t0 as @{const "==>"}) $ t1 $ t2 => |
|
419 if def then (t, []) else do_eq_or_imp Ts false def t0 t1 t2 seen |
|
420 | (t0 as Const (@{const_name "op ="}, _)) $ t1 $ t2 => |
|
421 do_eq_or_imp Ts true def t0 t1 t2 seen |
|
422 | (t0 as @{const "op -->"}) $ t1 $ t2 => |
|
423 do_eq_or_imp Ts false def t0 t1 t2 seen |
|
424 | Abs (s, T, t') => |
|
425 let val (t', seen) = do_term (T :: Ts) def t' [] seen in |
|
426 (list_comb (Abs (s, T, t'), args), seen) |
|
427 end |
|
428 | t1 $ t2 => |
|
429 let val (t2, seen) = do_term Ts def t2 [] seen in |
|
430 do_term Ts def t1 (t2 :: args) seen |
|
431 end |
|
432 | _ => pull_out_constr_comb thy Ts def k 0 t args seen |
|
433 (* typ list -> bool -> bool -> term -> term -> term -> term list |
|
434 -> term * term list *) |
|
435 and do_eq_or_imp Ts eq def t0 t1 t2 seen = |
|
436 let |
|
437 val (t2, seen) = if eq andalso def then (t2, seen) |
|
438 else do_term Ts false t2 [] seen |
|
439 val (t1, seen) = do_term Ts false t1 [] seen |
|
440 in (t0 $ t1 $ t2, seen) end |
|
441 val (concl, seen) = do_term [] def t [] [] |
|
442 in |
|
443 Logic.list_implies (equations_for_pulled_out_constrs Logic.mk_equals [] k |
|
444 seen, concl) |
|
445 end |
|
446 |
|
447 (* term -> term -> term *) |
|
448 fun mk_exists v t = |
|
449 HOLogic.exists_const (fastype_of v) $ lambda v (incr_boundvars 1 t) |
|
450 |
|
451 (* theory -> term -> term *) |
|
452 fun pull_out_existential_constrs thy t = |
|
453 let |
|
454 val k = maxidx_of_term t + 1 |
|
455 (* typ list -> int -> term -> term list -> term list -> term * term list *) |
|
456 fun aux Ts num_exists t args seen = |
|
457 case t of |
|
458 (t0 as Const (@{const_name Ex}, _)) $ Abs (s1, T1, t1) => |
|
459 let |
|
460 val (t1, seen') = aux (T1 :: Ts) (num_exists + 1) t1 [] [] |
|
461 val n = length seen' |
|
462 (* unit -> term list *) |
|
463 fun vars () = map2 (fresh_value_var Ts k n) (index_seq 0 n) seen' |
|
464 in |
|
465 (equations_for_pulled_out_constrs HOLogic.mk_eq Ts k seen' |
|
466 |> List.foldl s_conj t1 |> fold mk_exists (vars ()) |
|
467 |> curry3 Abs s1 T1 |> curry (op $) t0, seen) |
|
468 end |
|
469 | t1 $ t2 => |
|
470 let val (t2, seen) = aux Ts num_exists t2 [] seen in |
|
471 aux Ts num_exists t1 (t2 :: args) seen |
|
472 end |
|
473 | Abs (s, T, t') => |
|
474 let |
|
475 val (t', seen) = aux (T :: Ts) 0 t' [] (map (incr_boundvars 1) seen) |
|
476 in (list_comb (Abs (s, T, t'), args), map (incr_boundvars ~1) seen) end |
|
477 | _ => |
|
478 if num_exists > 0 then |
|
479 pull_out_constr_comb thy Ts false k num_exists t args seen |
|
480 else |
|
481 (list_comb (t, args), seen) |
|
482 in aux [] 0 t [] [] |> fst end |
|
483 |
|
484 (* hol_context -> bool -> term -> term *) |
|
485 fun destroy_pulled_out_constrs (hol_ctxt as {thy, ...}) axiom t = |
|
486 let |
|
487 (* styp -> int *) |
|
488 val num_occs_of_var = |
|
489 fold_aterms (fn Var z => (fn f => fn z' => f z' |> z = z' ? Integer.add 1) |
|
490 | _ => I) t (K 0) |
|
491 (* bool -> term -> term *) |
|
492 fun aux careful ((t0 as Const (@{const_name "=="}, _)) $ t1 $ t2) = |
|
493 aux_eq careful true t0 t1 t2 |
|
494 | aux careful ((t0 as @{const "==>"}) $ t1 $ t2) = |
|
495 t0 $ aux false t1 $ aux careful t2 |
|
496 | aux careful ((t0 as Const (@{const_name "op ="}, _)) $ t1 $ t2) = |
|
497 aux_eq careful true t0 t1 t2 |
|
498 | aux careful ((t0 as @{const "op -->"}) $ t1 $ t2) = |
|
499 t0 $ aux false t1 $ aux careful t2 |
|
500 | aux careful (Abs (s, T, t')) = Abs (s, T, aux careful t') |
|
501 | aux careful (t1 $ t2) = aux careful t1 $ aux careful t2 |
|
502 | aux _ t = t |
|
503 (* bool -> bool -> term -> term -> term -> term *) |
|
504 and aux_eq careful pass1 t0 t1 t2 = |
|
505 ((if careful then |
|
506 raise SAME () |
|
507 else if axiom andalso is_Var t2 andalso |
|
508 num_occs_of_var (dest_Var t2) = 1 then |
|
509 @{const True} |
|
510 else case strip_comb t2 of |
|
511 (* The first case is not as general as it could be. *) |
|
512 (Const (@{const_name PairBox}, _), |
|
513 [Const (@{const_name fst}, _) $ Var z1, |
|
514 Const (@{const_name snd}, _) $ Var z2]) => |
|
515 if z1 = z2 andalso num_occs_of_var z1 = 2 then @{const True} |
|
516 else raise SAME () |
|
517 | (Const (x as (s, T)), args) => |
|
518 let val arg_Ts = binder_types T in |
|
519 if length arg_Ts = length args andalso |
|
520 (is_constr thy x orelse s = @{const_name Pair} orelse |
|
521 x = (@{const_name Suc}, nat_T --> nat_T)) andalso |
|
522 (not careful orelse not (is_Var t1) orelse |
|
523 String.isPrefix val_var_prefix (fst (fst (dest_Var t1)))) then |
|
524 discriminate_value hol_ctxt x t1 :: |
|
525 map3 (sel_eq x t1) (index_seq 0 (length args)) arg_Ts args |
|
526 |> foldr1 s_conj |
|
527 else |
|
528 raise SAME () |
|
529 end |
|
530 | _ => raise SAME ()) |
|
531 |> body_type (type_of t0) = prop_T ? HOLogic.mk_Trueprop) |
|
532 handle SAME () => if pass1 then aux_eq careful false t0 t2 t1 |
|
533 else t0 $ aux false t2 $ aux false t1 |
|
534 (* styp -> term -> int -> typ -> term -> term *) |
|
535 and sel_eq x t n nth_T nth_t = |
|
536 HOLogic.eq_const nth_T $ nth_t $ select_nth_constr_arg thy x t n nth_T |
|
537 |> aux false |
|
538 in aux axiom t end |
|
539 |
|
540 (** Destruction of universal and existential equalities **) |
|
541 |
|
542 (* term -> term *) |
|
543 fun curry_assms (@{const "==>"} $ (@{const Trueprop} |
|
544 $ (@{const "op &"} $ t1 $ t2)) $ t3) = |
|
545 curry_assms (Logic.list_implies ([t1, t2] |> map HOLogic.mk_Trueprop, t3)) |
|
546 | curry_assms (@{const "==>"} $ t1 $ t2) = |
|
547 @{const "==>"} $ curry_assms t1 $ curry_assms t2 |
|
548 | curry_assms t = t |
|
549 |
|
550 (* term -> term *) |
|
551 val destroy_universal_equalities = |
|
552 let |
|
553 (* term list -> (indexname * typ) list -> term -> term *) |
|
554 fun aux prems zs t = |
|
555 case t of |
|
556 @{const "==>"} $ t1 $ t2 => aux_implies prems zs t1 t2 |
|
557 | _ => Logic.list_implies (rev prems, t) |
|
558 (* term list -> (indexname * typ) list -> term -> term -> term *) |
|
559 and aux_implies prems zs t1 t2 = |
|
560 case t1 of |
|
561 Const (@{const_name "=="}, _) $ Var z $ t' => aux_eq prems zs z t' t1 t2 |
|
562 | @{const Trueprop} $ (Const (@{const_name "op ="}, _) $ Var z $ t') => |
|
563 aux_eq prems zs z t' t1 t2 |
|
564 | @{const Trueprop} $ (Const (@{const_name "op ="}, _) $ t' $ Var z) => |
|
565 aux_eq prems zs z t' t1 t2 |
|
566 | _ => aux (t1 :: prems) (Term.add_vars t1 zs) t2 |
|
567 (* term list -> (indexname * typ) list -> indexname * typ -> term -> term |
|
568 -> term -> term *) |
|
569 and aux_eq prems zs z t' t1 t2 = |
|
570 if not (member (op =) zs z) andalso |
|
571 not (exists_subterm (curry (op =) (Var z)) t') then |
|
572 aux prems zs (subst_free [(Var z, t')] t2) |
|
573 else |
|
574 aux (t1 :: prems) (Term.add_vars t1 zs) t2 |
|
575 in aux [] [] end |
|
576 |
|
577 (* theory -> int -> term list -> term list -> (term * term list) option *) |
|
578 fun find_bound_assign _ _ _ [] = NONE |
|
579 | find_bound_assign thy j seen (t :: ts) = |
|
580 let |
|
581 (* bool -> term -> term -> (term * term list) option *) |
|
582 fun aux pass1 t1 t2 = |
|
583 (if loose_bvar1 (t2, j) then |
|
584 if pass1 then aux false t2 t1 else raise SAME () |
|
585 else case t1 of |
|
586 Bound j' => if j' = j then SOME (t2, ts @ seen) else raise SAME () |
|
587 | Const (s, Type ("fun", [T1, T2])) $ Bound j' => |
|
588 if j' = j andalso |
|
589 s = nth_sel_name_for_constr_name @{const_name FunBox} 0 then |
|
590 SOME (construct_value thy (@{const_name FunBox}, T2 --> T1) [t2], |
|
591 ts @ seen) |
|
592 else |
|
593 raise SAME () |
|
594 | _ => raise SAME ()) |
|
595 handle SAME () => find_bound_assign thy j (t :: seen) ts |
|
596 in |
|
597 case t of |
|
598 Const (@{const_name "op ="}, _) $ t1 $ t2 => aux true t1 t2 |
|
599 | _ => find_bound_assign thy j (t :: seen) ts |
|
600 end |
|
601 |
|
602 (* int -> term -> term -> term *) |
|
603 fun subst_one_bound j arg t = |
|
604 let |
|
605 fun aux (Bound i, lev) = |
|
606 if i < lev then raise SAME () |
|
607 else if i = lev then incr_boundvars (lev - j) arg |
|
608 else Bound (i - 1) |
|
609 | aux (Abs (a, T, body), lev) = Abs (a, T, aux (body, lev + 1)) |
|
610 | aux (f $ t, lev) = |
|
611 (aux (f, lev) $ (aux (t, lev) handle SAME () => t) |
|
612 handle SAME () => f $ aux (t, lev)) |
|
613 | aux _ = raise SAME () |
|
614 in aux (t, j) handle SAME () => t end |
|
615 |
|
616 (* theory -> term -> term *) |
|
617 fun destroy_existential_equalities thy = |
|
618 let |
|
619 (* string list -> typ list -> term list -> term *) |
|
620 fun kill [] [] ts = foldr1 s_conj ts |
|
621 | kill (s :: ss) (T :: Ts) ts = |
|
622 (case find_bound_assign thy (length ss) [] ts of |
|
623 SOME (_, []) => @{const True} |
|
624 | SOME (arg_t, ts) => |
|
625 kill ss Ts (map (subst_one_bound (length ss) |
|
626 (incr_bv (~1, length ss + 1, arg_t))) ts) |
|
627 | NONE => |
|
628 Const (@{const_name Ex}, (T --> bool_T) --> bool_T) |
|
629 $ Abs (s, T, kill ss Ts ts)) |
|
630 | kill _ _ _ = raise UnequalLengths |
|
631 (* string list -> typ list -> term -> term *) |
|
632 fun gather ss Ts ((t0 as Const (@{const_name Ex}, _)) $ Abs (s1, T1, t1)) = |
|
633 gather (ss @ [s1]) (Ts @ [T1]) t1 |
|
634 | gather [] [] (Abs (s, T, t1)) = Abs (s, T, gather [] [] t1) |
|
635 | gather [] [] (t1 $ t2) = gather [] [] t1 $ gather [] [] t2 |
|
636 | gather [] [] t = t |
|
637 | gather ss Ts t = kill ss Ts (conjuncts_of (gather [] [] t)) |
|
638 in gather [] [] end |
|
639 |
|
640 (** Skolemization **) |
|
641 |
|
642 (* int -> int -> string *) |
|
643 fun skolem_prefix_for k j = |
|
644 skolem_prefix ^ string_of_int k ^ "@" ^ string_of_int j ^ name_sep |
|
645 |
|
646 (* hol_context -> int -> term -> term *) |
|
647 fun skolemize_term_and_more (hol_ctxt as {thy, def_table, skolems, ...}) |
|
648 skolem_depth = |
|
649 let |
|
650 (* int list -> int list *) |
|
651 val incrs = map (Integer.add 1) |
|
652 (* string list -> typ list -> int list -> int -> polarity -> term -> term *) |
|
653 fun aux ss Ts js depth polar t = |
|
654 let |
|
655 (* string -> typ -> string -> typ -> term -> term *) |
|
656 fun do_quantifier quant_s quant_T abs_s abs_T t = |
|
657 if not (loose_bvar1 (t, 0)) then |
|
658 aux ss Ts js depth polar (incr_boundvars ~1 t) |
|
659 else if depth <= skolem_depth andalso |
|
660 is_positive_existential polar quant_s then |
|
661 let |
|
662 val j = length (!skolems) + 1 |
|
663 val sko_s = skolem_prefix_for (length js) j ^ abs_s |
|
664 val _ = Unsynchronized.change skolems (cons (sko_s, ss)) |
|
665 val sko_t = list_comb (Const (sko_s, rev Ts ---> abs_T), |
|
666 map Bound (rev js)) |
|
667 val abs_t = Abs (abs_s, abs_T, aux ss Ts (incrs js) depth polar t) |
|
668 in |
|
669 if null js then betapply (abs_t, sko_t) |
|
670 else Const (@{const_name Let}, abs_T --> quant_T) $ sko_t $ abs_t |
|
671 end |
|
672 else |
|
673 Const (quant_s, quant_T) |
|
674 $ Abs (abs_s, abs_T, |
|
675 if is_higher_order_type abs_T then |
|
676 t |
|
677 else |
|
678 aux (abs_s :: ss) (abs_T :: Ts) (0 :: incrs js) |
|
679 (depth + 1) polar t) |
|
680 in |
|
681 case t of |
|
682 Const (s0 as @{const_name all}, T0) $ Abs (s1, T1, t1) => |
|
683 do_quantifier s0 T0 s1 T1 t1 |
|
684 | @{const "==>"} $ t1 $ t2 => |
|
685 @{const "==>"} $ aux ss Ts js depth (flip_polarity polar) t1 |
|
686 $ aux ss Ts js depth polar t2 |
|
687 | @{const Pure.conjunction} $ t1 $ t2 => |
|
688 @{const Pure.conjunction} $ aux ss Ts js depth polar t1 |
|
689 $ aux ss Ts js depth polar t2 |
|
690 | @{const Trueprop} $ t1 => |
|
691 @{const Trueprop} $ aux ss Ts js depth polar t1 |
|
692 | @{const Not} $ t1 => |
|
693 @{const Not} $ aux ss Ts js depth (flip_polarity polar) t1 |
|
694 | Const (s0 as @{const_name All}, T0) $ Abs (s1, T1, t1) => |
|
695 do_quantifier s0 T0 s1 T1 t1 |
|
696 | Const (s0 as @{const_name Ex}, T0) $ Abs (s1, T1, t1) => |
|
697 do_quantifier s0 T0 s1 T1 t1 |
|
698 | @{const "op &"} $ t1 $ t2 => |
|
699 @{const "op &"} $ aux ss Ts js depth polar t1 |
|
700 $ aux ss Ts js depth polar t2 |
|
701 | @{const "op |"} $ t1 $ t2 => |
|
702 @{const "op |"} $ aux ss Ts js depth polar t1 |
|
703 $ aux ss Ts js depth polar t2 |
|
704 | @{const "op -->"} $ t1 $ t2 => |
|
705 @{const "op -->"} $ aux ss Ts js depth (flip_polarity polar) t1 |
|
706 $ aux ss Ts js depth polar t2 |
|
707 | (t0 as Const (@{const_name Let}, T0)) $ t1 $ t2 => |
|
708 t0 $ t1 $ aux ss Ts js depth polar t2 |
|
709 | Const (x as (s, T)) => |
|
710 if is_inductive_pred hol_ctxt x andalso |
|
711 not (is_well_founded_inductive_pred hol_ctxt x) then |
|
712 let |
|
713 val gfp = (fixpoint_kind_of_const thy def_table x = Gfp) |
|
714 val (pref, connective, set_oper) = |
|
715 if gfp then |
|
716 (lbfp_prefix, |
|
717 @{const "op |"}, |
|
718 @{const_name upper_semilattice_fun_inst.sup_fun}) |
|
719 else |
|
720 (ubfp_prefix, |
|
721 @{const "op &"}, |
|
722 @{const_name lower_semilattice_fun_inst.inf_fun}) |
|
723 (* unit -> term *) |
|
724 fun pos () = unrolled_inductive_pred_const hol_ctxt gfp x |
|
725 |> aux ss Ts js depth polar |
|
726 fun neg () = Const (pref ^ s, T) |
|
727 in |
|
728 (case polar |> gfp ? flip_polarity of |
|
729 Pos => pos () |
|
730 | Neg => neg () |
|
731 | Neut => |
|
732 if is_fun_type T then |
|
733 let |
|
734 val ((trunk_arg_Ts, rump_arg_T), body_T) = |
|
735 T |> strip_type |>> split_last |
|
736 val set_T = rump_arg_T --> body_T |
|
737 (* (unit -> term) -> term *) |
|
738 fun app f = |
|
739 list_comb (f (), |
|
740 map Bound (length trunk_arg_Ts - 1 downto 0)) |
|
741 in |
|
742 List.foldr absdummy |
|
743 (Const (set_oper, set_T --> set_T --> set_T) |
|
744 $ app pos $ app neg) trunk_arg_Ts |
|
745 end |
|
746 else |
|
747 connective $ pos () $ neg ()) |
|
748 end |
|
749 else |
|
750 Const x |
|
751 | t1 $ t2 => |
|
752 betapply (aux ss Ts [] (skolem_depth + 1) polar t1, |
|
753 aux ss Ts [] depth Neut t2) |
|
754 | Abs (s, T, t1) => Abs (s, T, aux ss Ts (incrs js) depth polar t1) |
|
755 | _ => t |
|
756 end |
|
757 in aux [] [] [] 0 Pos end |
|
758 |
|
759 (** Function specialization **) |
|
760 |
|
761 (* term -> term list *) |
|
762 fun params_in_equation (@{const "==>"} $ _ $ t2) = params_in_equation t2 |
|
763 | params_in_equation (@{const Trueprop} $ t1) = params_in_equation t1 |
|
764 | params_in_equation (Const (@{const_name "op ="}, _) $ t1 $ _) = |
|
765 snd (strip_comb t1) |
|
766 | params_in_equation _ = [] |
|
767 |
|
768 (* styp -> styp -> int list -> term list -> term list -> term -> term *) |
|
769 fun specialize_fun_axiom x x' fixed_js fixed_args extra_args t = |
|
770 let |
|
771 val k = fold Integer.max (map maxidx_of_term (fixed_args @ extra_args)) 0 |
|
772 + 1 |
|
773 val t = map_aterms (fn Var ((s, i), T) => Var ((s, k + i), T) | t' => t') t |
|
774 val fixed_params = filter_indices fixed_js (params_in_equation t) |
|
775 (* term list -> term -> term *) |
|
776 fun aux args (Abs (s, T, t)) = list_comb (Abs (s, T, aux [] t), args) |
|
777 | aux args (t1 $ t2) = aux (aux [] t2 :: args) t1 |
|
778 | aux args t = |
|
779 if t = Const x then |
|
780 list_comb (Const x', extra_args @ filter_out_indices fixed_js args) |
|
781 else |
|
782 let val j = find_index (curry (op =) t) fixed_params in |
|
783 list_comb (if j >= 0 then nth fixed_args j else t, args) |
|
784 end |
|
785 in aux [] t end |
|
786 |
|
787 (* hol_context -> styp -> (int * term option) list *) |
|
788 fun static_args_in_term ({ersatz_table, ...} : hol_context) x t = |
|
789 let |
|
790 (* term -> term list -> term list -> term list list *) |
|
791 fun fun_calls (Abs (_, _, t)) _ = fun_calls t [] |
|
792 | fun_calls (t1 $ t2) args = fun_calls t2 [] #> fun_calls t1 (t2 :: args) |
|
793 | fun_calls t args = |
|
794 (case t of |
|
795 Const (x' as (s', T')) => |
|
796 x = x' orelse (case AList.lookup (op =) ersatz_table s' of |
|
797 SOME s'' => x = (s'', T') |
|
798 | NONE => false) |
|
799 | _ => false) ? cons args |
|
800 (* term list list -> term list list -> term list -> term list list *) |
|
801 fun call_sets [] [] vs = [vs] |
|
802 | call_sets [] uss vs = vs :: call_sets uss [] [] |
|
803 | call_sets ([] :: _) _ _ = [] |
|
804 | call_sets ((t :: ts) :: tss) uss vs = |
|
805 OrdList.insert TermOrd.term_ord t vs |> call_sets tss (ts :: uss) |
|
806 val sets = call_sets (fun_calls t [] []) [] [] |
|
807 val indexed_sets = sets ~~ (index_seq 0 (length sets)) |
|
808 in |
|
809 fold_rev (fn (set, j) => |
|
810 case set of |
|
811 [Var _] => AList.lookup (op =) indexed_sets set = SOME j |
|
812 ? cons (j, NONE) |
|
813 | [t as Const _] => cons (j, SOME t) |
|
814 | [t as Free _] => cons (j, SOME t) |
|
815 | _ => I) indexed_sets [] |
|
816 end |
|
817 (* hol_context -> styp -> term list -> (int * term option) list *) |
|
818 fun static_args_in_terms hol_ctxt x = |
|
819 map (static_args_in_term hol_ctxt x) |
|
820 #> fold1 (OrdList.inter (prod_ord int_ord (option_ord TermOrd.term_ord))) |
|
821 |
|
822 (* (int * term option) list -> (int * term) list -> int list *) |
|
823 fun overlapping_indices [] _ = [] |
|
824 | overlapping_indices _ [] = [] |
|
825 | overlapping_indices (ps1 as (j1, t1) :: ps1') (ps2 as (j2, t2) :: ps2') = |
|
826 if j1 < j2 then overlapping_indices ps1' ps2 |
|
827 else if j1 > j2 then overlapping_indices ps1 ps2' |
|
828 else overlapping_indices ps1' ps2' |> the_default t2 t1 = t2 ? cons j1 |
|
829 |
|
830 (* typ list -> term -> bool *) |
|
831 fun is_eligible_arg Ts t = |
|
832 let val bad_Ts = map snd (Term.add_vars t []) @ map (nth Ts) (loose_bnos t) in |
|
833 null bad_Ts orelse |
|
834 (is_higher_order_type (fastype_of1 (Ts, t)) andalso |
|
835 forall (not o is_higher_order_type) bad_Ts) |
|
836 end |
|
837 |
|
838 (* int -> string *) |
|
839 fun special_prefix_for j = special_prefix ^ string_of_int j ^ name_sep |
|
840 |
|
841 (* If a constant's definition is picked up deeper than this threshold, we |
|
842 prevent excessive specialization by not specializing it. *) |
|
843 val special_max_depth = 20 |
|
844 |
|
845 val bound_var_prefix = "b" |
|
846 |
|
847 (* hol_context -> int -> term -> term *) |
|
848 fun specialize_consts_in_term (hol_ctxt as {thy, specialize, simp_table, |
|
849 special_funs, ...}) depth t = |
|
850 if not specialize orelse depth > special_max_depth then |
|
851 t |
|
852 else |
|
853 let |
|
854 val blacklist = if depth = 0 then [] |
|
855 else case term_under_def t of Const x => [x] | _ => [] |
|
856 (* term list -> typ list -> term -> term *) |
|
857 fun aux args Ts (Const (x as (s, T))) = |
|
858 ((if not (member (op =) blacklist x) andalso not (null args) andalso |
|
859 not (String.isPrefix special_prefix s) andalso |
|
860 is_equational_fun hol_ctxt x then |
|
861 let |
|
862 val eligible_args = filter (is_eligible_arg Ts o snd) |
|
863 (index_seq 0 (length args) ~~ args) |
|
864 val _ = not (null eligible_args) orelse raise SAME () |
|
865 val old_axs = equational_fun_axioms hol_ctxt x |
|
866 |> map (destroy_existential_equalities thy) |
|
867 val static_params = static_args_in_terms hol_ctxt x old_axs |
|
868 val fixed_js = overlapping_indices static_params eligible_args |
|
869 val _ = not (null fixed_js) orelse raise SAME () |
|
870 val fixed_args = filter_indices fixed_js args |
|
871 val vars = fold Term.add_vars fixed_args [] |
|
872 |> sort (TermOrd.fast_indexname_ord o pairself fst) |
|
873 val bound_js = fold (fn t => fn js => add_loose_bnos (t, 0, js)) |
|
874 fixed_args [] |
|
875 |> sort int_ord |
|
876 val live_args = filter_out_indices fixed_js args |
|
877 val extra_args = map Var vars @ map Bound bound_js @ live_args |
|
878 val extra_Ts = map snd vars @ filter_indices bound_js Ts |
|
879 val k = maxidx_of_term t + 1 |
|
880 (* int -> term *) |
|
881 fun var_for_bound_no j = |
|
882 Var ((bound_var_prefix ^ |
|
883 nat_subscript (find_index (curry (op =) j) bound_js |
|
884 + 1), k), |
|
885 nth Ts j) |
|
886 val fixed_args_in_axiom = |
|
887 map (curry subst_bounds |
|
888 (map var_for_bound_no (index_seq 0 (length Ts)))) |
|
889 fixed_args |
|
890 in |
|
891 case AList.lookup (op =) (!special_funs) |
|
892 (x, fixed_js, fixed_args_in_axiom) of |
|
893 SOME x' => list_comb (Const x', extra_args) |
|
894 | NONE => |
|
895 let |
|
896 val extra_args_in_axiom = |
|
897 map Var vars @ map var_for_bound_no bound_js |
|
898 val x' as (s', _) = |
|
899 (special_prefix_for (length (!special_funs) + 1) ^ s, |
|
900 extra_Ts @ filter_out_indices fixed_js (binder_types T) |
|
901 ---> body_type T) |
|
902 val new_axs = |
|
903 map (specialize_fun_axiom x x' fixed_js |
|
904 fixed_args_in_axiom extra_args_in_axiom) old_axs |
|
905 val _ = |
|
906 Unsynchronized.change special_funs |
|
907 (cons ((x, fixed_js, fixed_args_in_axiom), x')) |
|
908 val _ = add_simps simp_table s' new_axs |
|
909 in list_comb (Const x', extra_args) end |
|
910 end |
|
911 else |
|
912 raise SAME ()) |
|
913 handle SAME () => list_comb (Const x, args)) |
|
914 | aux args Ts (Abs (s, T, t)) = |
|
915 list_comb (Abs (s, T, aux [] (T :: Ts) t), args) |
|
916 | aux args Ts (t1 $ t2) = aux (aux [] Ts t2 :: args) Ts t1 |
|
917 | aux args _ t = list_comb (t, args) |
|
918 in aux [] [] t end |
|
919 |
|
920 type special_triple = int list * term list * styp |
|
921 |
|
922 val cong_var_prefix = "c" |
|
923 |
|
924 (* styp -> special_triple -> special_triple -> term *) |
|
925 fun special_congruence_axiom (s, T) (js1, ts1, x1) (js2, ts2, x2) = |
|
926 let |
|
927 val (bounds1, bounds2) = pairself (map Var o special_bounds) (ts1, ts2) |
|
928 val Ts = binder_types T |
|
929 val max_j = fold (fold Integer.max) [js1, js2] ~1 |
|
930 val (eqs, (args1, args2)) = |
|
931 fold (fn j => case pairself (fn ps => AList.lookup (op =) ps j) |
|
932 (js1 ~~ ts1, js2 ~~ ts2) of |
|
933 (SOME t1, SOME t2) => apfst (cons (t1, t2)) |
|
934 | (SOME t1, NONE) => apsnd (apsnd (cons t1)) |
|
935 | (NONE, SOME t2) => apsnd (apfst (cons t2)) |
|
936 | (NONE, NONE) => |
|
937 let val v = Var ((cong_var_prefix ^ nat_subscript j, 0), |
|
938 nth Ts j) in |
|
939 apsnd (pairself (cons v)) |
|
940 end) (max_j downto 0) ([], ([], [])) |
|
941 in |
|
942 Logic.list_implies (eqs |> filter_out (op =) |> distinct (op =) |
|
943 |> map Logic.mk_equals, |
|
944 Logic.mk_equals (list_comb (Const x1, bounds1 @ args1), |
|
945 list_comb (Const x2, bounds2 @ args2))) |
|
946 |> Refute.close_form (* TODO: needed? *) |
|
947 end |
|
948 |
|
949 (* hol_context -> styp list -> term list *) |
|
950 fun special_congruence_axioms (hol_ctxt as {special_funs, ...}) xs = |
|
951 let |
|
952 val groups = |
|
953 !special_funs |
|
954 |> map (fn ((x, js, ts), x') => (x, (js, ts, x'))) |
|
955 |> AList.group (op =) |
|
956 |> filter_out (is_equational_fun_surely_complete hol_ctxt o fst) |
|
957 |> map (fn (x, zs) => (x, zs |> member (op =) xs x ? cons ([], [], x))) |
|
958 (* special_triple -> int *) |
|
959 fun generality (js, _, _) = ~(length js) |
|
960 (* special_triple -> special_triple -> bool *) |
|
961 fun is_more_specific (j1, t1, x1) (j2, t2, x2) = |
|
962 x1 <> x2 andalso OrdList.subset (prod_ord int_ord TermOrd.term_ord) |
|
963 (j2 ~~ t2, j1 ~~ t1) |
|
964 (* styp -> special_triple list -> special_triple list -> special_triple list |
|
965 -> term list -> term list *) |
|
966 fun do_pass_1 _ [] [_] [_] = I |
|
967 | do_pass_1 x skipped _ [] = do_pass_2 x skipped |
|
968 | do_pass_1 x skipped all (z :: zs) = |
|
969 case filter (is_more_specific z) all |
|
970 |> sort (int_ord o pairself generality) of |
|
971 [] => do_pass_1 x (z :: skipped) all zs |
|
972 | (z' :: _) => cons (special_congruence_axiom x z z') |
|
973 #> do_pass_1 x skipped all zs |
|
974 (* styp -> special_triple list -> term list -> term list *) |
|
975 and do_pass_2 _ [] = I |
|
976 | do_pass_2 x (z :: zs) = |
|
977 fold (cons o special_congruence_axiom x z) zs #> do_pass_2 x zs |
|
978 in fold (fn (x, zs) => do_pass_1 x [] zs zs) groups [] end |
|
979 |
|
980 (** Axiom selection **) |
|
981 |
|
982 (* Similar to "Refute.specialize_type" but returns all matches rather than only |
|
983 the first (preorder) match. *) |
|
984 (* theory -> styp -> term -> term list *) |
|
985 fun multi_specialize_type thy slack (x as (s, T)) t = |
|
986 let |
|
987 (* term -> (typ * term) list -> (typ * term) list *) |
|
988 fun aux (Const (s', T')) ys = |
|
989 if s = s' then |
|
990 ys |> (if AList.defined (op =) ys T' then |
|
991 I |
|
992 else |
|
993 cons (T', Refute.monomorphic_term |
|
994 (Sign.typ_match thy (T', T) Vartab.empty) t) |
|
995 handle Type.TYPE_MATCH => I |
|
996 | Refute.REFUTE _ => |
|
997 if slack then |
|
998 I |
|
999 else |
|
1000 raise NOT_SUPPORTED ("too much polymorphism in \ |
|
1001 \axiom involving " ^ quote s)) |
|
1002 else |
|
1003 ys |
|
1004 | aux _ ys = ys |
|
1005 in map snd (fold_aterms aux t []) end |
|
1006 |
|
1007 (* theory -> bool -> const_table -> styp -> term list *) |
|
1008 fun nondef_props_for_const thy slack table (x as (s, _)) = |
|
1009 these (Symtab.lookup table s) |> maps (multi_specialize_type thy slack x) |
|
1010 |
|
1011 (* 'a Symtab.table -> 'a list *) |
|
1012 fun all_table_entries table = Symtab.fold (append o snd) table [] |
|
1013 (* const_table -> string -> const_table *) |
|
1014 fun extra_table table s = Symtab.make [(s, all_table_entries table)] |
|
1015 |
|
1016 (* int -> term -> term *) |
|
1017 fun eval_axiom_for_term j t = |
|
1018 Logic.mk_equals (Const (eval_prefix ^ string_of_int j, fastype_of t), t) |
|
1019 |
|
1020 (* term -> bool *) |
|
1021 val is_trivial_equation = the_default false o try (op aconv o Logic.dest_equals) |
|
1022 |
|
1023 (* Prevents divergence in case of cyclic or infinite axiom dependencies. *) |
|
1024 val axioms_max_depth = 255 |
|
1025 |
|
1026 (* hol_context -> term -> (term list * term list) * (bool * bool) *) |
|
1027 fun axioms_for_term |
|
1028 (hol_ctxt as {thy, max_bisim_depth, user_axioms, fast_descrs, evals, |
|
1029 def_table, nondef_table, user_nondefs, ...}) t = |
|
1030 let |
|
1031 type accumulator = styp list * (term list * term list) |
|
1032 (* (term list * term list -> term list) |
|
1033 -> ((term list -> term list) -> term list * term list |
|
1034 -> term list * term list) |
|
1035 -> int -> term -> accumulator -> accumulator *) |
|
1036 fun add_axiom get app depth t (accum as (xs, axs)) = |
|
1037 let |
|
1038 val t = t |> unfold_defs_in_term hol_ctxt |
|
1039 |> skolemize_term_and_more hol_ctxt ~1 |
|
1040 in |
|
1041 if is_trivial_equation t then |
|
1042 accum |
|
1043 else |
|
1044 let val t' = t |> specialize_consts_in_term hol_ctxt depth in |
|
1045 if exists (member (op aconv) (get axs)) [t, t'] then accum |
|
1046 else add_axioms_for_term (depth + 1) t' (xs, app (cons t') axs) |
|
1047 end |
|
1048 end |
|
1049 (* int -> term -> accumulator -> accumulator *) |
|
1050 and add_def_axiom depth = add_axiom fst apfst depth |
|
1051 and add_nondef_axiom depth = add_axiom snd apsnd depth |
|
1052 and add_maybe_def_axiom depth t = |
|
1053 (if head_of t <> @{const "==>"} then add_def_axiom |
|
1054 else add_nondef_axiom) depth t |
|
1055 and add_eq_axiom depth t = |
|
1056 (if is_constr_pattern_formula thy t then add_def_axiom |
|
1057 else add_nondef_axiom) depth t |
|
1058 (* int -> term -> accumulator -> accumulator *) |
|
1059 and add_axioms_for_term depth t (accum as (xs, axs)) = |
|
1060 case t of |
|
1061 t1 $ t2 => accum |> fold (add_axioms_for_term depth) [t1, t2] |
|
1062 | Const (x as (s, T)) => |
|
1063 (if member (op =) xs x orelse is_built_in_const fast_descrs x then |
|
1064 accum |
|
1065 else |
|
1066 let val accum as (xs, _) = (x :: xs, axs) in |
|
1067 if depth > axioms_max_depth then |
|
1068 raise TOO_LARGE ("Nitpick_Preproc.axioms_for_term.\ |
|
1069 \add_axioms_for_term", |
|
1070 "too many nested axioms (" ^ |
|
1071 string_of_int depth ^ ")") |
|
1072 else if Refute.is_const_of_class thy x then |
|
1073 let |
|
1074 val class = Logic.class_of_const s |
|
1075 val of_class = Logic.mk_of_class (TVar (("'a", 0), [class]), |
|
1076 class) |
|
1077 val ax1 = try (Refute.specialize_type thy x) of_class |
|
1078 val ax2 = Option.map (Refute.specialize_type thy x o snd) |
|
1079 (Refute.get_classdef thy class) |
|
1080 in |
|
1081 fold (add_maybe_def_axiom depth) (map_filter I [ax1, ax2]) |
|
1082 accum |
|
1083 end |
|
1084 else if is_constr thy x then |
|
1085 accum |
|
1086 else if is_equational_fun hol_ctxt x then |
|
1087 fold (add_eq_axiom depth) (equational_fun_axioms hol_ctxt x) |
|
1088 accum |
|
1089 else if is_abs_fun thy x then |
|
1090 if is_quot_type thy (range_type T) then |
|
1091 raise NOT_SUPPORTED "\"Abs_\" function of quotient type" |
|
1092 else |
|
1093 accum |> fold (add_nondef_axiom depth) |
|
1094 (nondef_props_for_const thy false nondef_table x) |
|
1095 |> is_funky_typedef thy (range_type T) |
|
1096 ? fold (add_maybe_def_axiom depth) |
|
1097 (nondef_props_for_const thy true |
|
1098 (extra_table def_table s) x) |
|
1099 else if is_rep_fun thy x then |
|
1100 if is_quot_type thy (domain_type T) then |
|
1101 raise NOT_SUPPORTED "\"Rep_\" function of quotient type" |
|
1102 else |
|
1103 accum |> fold (add_nondef_axiom depth) |
|
1104 (nondef_props_for_const thy false nondef_table x) |
|
1105 |> is_funky_typedef thy (range_type T) |
|
1106 ? fold (add_maybe_def_axiom depth) |
|
1107 (nondef_props_for_const thy true |
|
1108 (extra_table def_table s) x) |
|
1109 |> add_axioms_for_term depth |
|
1110 (Const (mate_of_rep_fun thy x)) |
|
1111 |> fold (add_def_axiom depth) |
|
1112 (inverse_axioms_for_rep_fun thy x) |
|
1113 else |
|
1114 accum |> user_axioms <> SOME false |
|
1115 ? fold (add_nondef_axiom depth) |
|
1116 (nondef_props_for_const thy false nondef_table x) |
|
1117 end) |
|
1118 |> add_axioms_for_type depth T |
|
1119 | Free (_, T) => add_axioms_for_type depth T accum |
|
1120 | Var (_, T) => add_axioms_for_type depth T accum |
|
1121 | Bound _ => accum |
|
1122 | Abs (_, T, t) => accum |> add_axioms_for_term depth t |
|
1123 |> add_axioms_for_type depth T |
|
1124 (* int -> typ -> accumulator -> accumulator *) |
|
1125 and add_axioms_for_type depth T = |
|
1126 case T of |
|
1127 Type ("fun", Ts) => fold (add_axioms_for_type depth) Ts |
|
1128 | Type ("*", Ts) => fold (add_axioms_for_type depth) Ts |
|
1129 | @{typ prop} => I |
|
1130 | @{typ bool} => I |
|
1131 | @{typ unit} => I |
|
1132 | TFree (_, S) => add_axioms_for_sort depth T S |
|
1133 | TVar (_, S) => add_axioms_for_sort depth T S |
|
1134 | Type (z as (s, Ts)) => |
|
1135 fold (add_axioms_for_type depth) Ts |
|
1136 #> (if is_pure_typedef thy T then |
|
1137 fold (add_maybe_def_axiom depth) (optimized_typedef_axioms thy z) |
|
1138 else if is_quot_type thy T then |
|
1139 fold (add_def_axiom depth) (optimized_quot_type_axioms thy z) |
|
1140 else if max_bisim_depth >= 0 andalso is_codatatype thy T then |
|
1141 fold (add_maybe_def_axiom depth) |
|
1142 (codatatype_bisim_axioms hol_ctxt T) |
|
1143 else |
|
1144 I) |
|
1145 (* int -> typ -> sort -> accumulator -> accumulator *) |
|
1146 and add_axioms_for_sort depth T S = |
|
1147 let |
|
1148 val supers = Sign.complete_sort thy S |
|
1149 val class_axioms = |
|
1150 maps (fn class => map prop_of (AxClass.get_info thy class |> #axioms |
|
1151 handle ERROR _ => [])) supers |
|
1152 val monomorphic_class_axioms = |
|
1153 map (fn t => case Term.add_tvars t [] of |
|
1154 [] => t |
|
1155 | [(x, S)] => |
|
1156 Refute.monomorphic_term (Vartab.make [(x, (S, T))]) t |
|
1157 | _ => raise TERM ("Nitpick_Preproc.axioms_for_term.\ |
|
1158 \add_axioms_for_sort", [t])) |
|
1159 class_axioms |
|
1160 in fold (add_nondef_axiom depth) monomorphic_class_axioms end |
|
1161 val (mono_user_nondefs, poly_user_nondefs) = |
|
1162 List.partition (null o Term.hidden_polymorphism) user_nondefs |
|
1163 val eval_axioms = map2 eval_axiom_for_term (index_seq 0 (length evals)) |
|
1164 evals |
|
1165 val (xs, (defs, nondefs)) = |
|
1166 ([], ([], [])) |> add_axioms_for_term 1 t |
|
1167 |> fold_rev (add_def_axiom 1) eval_axioms |
|
1168 |> user_axioms = SOME true |
|
1169 ? fold (add_nondef_axiom 1) mono_user_nondefs |
|
1170 val defs = defs @ special_congruence_axioms hol_ctxt xs |
|
1171 in |
|
1172 ((defs, nondefs), (user_axioms = SOME true orelse null mono_user_nondefs, |
|
1173 null poly_user_nondefs)) |
|
1174 end |
|
1175 |
|
1176 (** Simplification of constructor/selector terms **) |
|
1177 |
|
1178 (* theory -> term -> term *) |
|
1179 fun simplify_constrs_and_sels thy t = |
|
1180 let |
|
1181 (* term -> int -> term *) |
|
1182 fun is_nth_sel_on t' n (Const (s, _) $ t) = |
|
1183 (t = t' andalso is_sel_like_and_no_discr s andalso |
|
1184 sel_no_from_name s = n) |
|
1185 | is_nth_sel_on _ _ _ = false |
|
1186 (* term -> term list -> term *) |
|
1187 fun do_term (Const (@{const_name Rep_Frac}, _) |
|
1188 $ (Const (@{const_name Abs_Frac}, _) $ t1)) [] = do_term t1 [] |
|
1189 | do_term (Const (@{const_name Abs_Frac}, _) |
|
1190 $ (Const (@{const_name Rep_Frac}, _) $ t1)) [] = do_term t1 [] |
|
1191 | do_term (t1 $ t2) args = do_term t1 (do_term t2 [] :: args) |
|
1192 | do_term (t as Const (x as (s, T))) (args as _ :: _) = |
|
1193 ((if is_constr_like thy x then |
|
1194 if length args = num_binder_types T then |
|
1195 case hd args of |
|
1196 Const (x' as (_, T')) $ t' => |
|
1197 if domain_type T' = body_type T andalso |
|
1198 forall (uncurry (is_nth_sel_on t')) |
|
1199 (index_seq 0 (length args) ~~ args) then |
|
1200 t' |
|
1201 else |
|
1202 raise SAME () |
|
1203 | _ => raise SAME () |
|
1204 else |
|
1205 raise SAME () |
|
1206 else if is_sel_like_and_no_discr s then |
|
1207 case strip_comb (hd args) of |
|
1208 (Const (x' as (s', T')), ts') => |
|
1209 if is_constr_like thy x' andalso |
|
1210 constr_name_for_sel_like s = s' andalso |
|
1211 not (exists is_pair_type (binder_types T')) then |
|
1212 list_comb (nth ts' (sel_no_from_name s), tl args) |
|
1213 else |
|
1214 raise SAME () |
|
1215 | _ => raise SAME () |
|
1216 else |
|
1217 raise SAME ()) |
|
1218 handle SAME () => betapplys (t, args)) |
|
1219 | do_term (Abs (s, T, t')) args = |
|
1220 betapplys (Abs (s, T, do_term t' []), args) |
|
1221 | do_term t args = betapplys (t, args) |
|
1222 in do_term t [] end |
|
1223 |
|
1224 (** Quantifier massaging: Distributing quantifiers **) |
|
1225 |
|
1226 (* term -> term *) |
|
1227 fun distribute_quantifiers t = |
|
1228 case t of |
|
1229 (t0 as Const (@{const_name All}, T0)) $ Abs (s, T1, t1) => |
|
1230 (case t1 of |
|
1231 (t10 as @{const "op &"}) $ t11 $ t12 => |
|
1232 t10 $ distribute_quantifiers (t0 $ Abs (s, T1, t11)) |
|
1233 $ distribute_quantifiers (t0 $ Abs (s, T1, t12)) |
|
1234 | (t10 as @{const Not}) $ t11 => |
|
1235 t10 $ distribute_quantifiers (Const (@{const_name Ex}, T0) |
|
1236 $ Abs (s, T1, t11)) |
|
1237 | t1 => |
|
1238 if not (loose_bvar1 (t1, 0)) then |
|
1239 distribute_quantifiers (incr_boundvars ~1 t1) |
|
1240 else |
|
1241 t0 $ Abs (s, T1, distribute_quantifiers t1)) |
|
1242 | (t0 as Const (@{const_name Ex}, T0)) $ Abs (s, T1, t1) => |
|
1243 (case distribute_quantifiers t1 of |
|
1244 (t10 as @{const "op |"}) $ t11 $ t12 => |
|
1245 t10 $ distribute_quantifiers (t0 $ Abs (s, T1, t11)) |
|
1246 $ distribute_quantifiers (t0 $ Abs (s, T1, t12)) |
|
1247 | (t10 as @{const "op -->"}) $ t11 $ t12 => |
|
1248 t10 $ distribute_quantifiers (Const (@{const_name All}, T0) |
|
1249 $ Abs (s, T1, t11)) |
|
1250 $ distribute_quantifiers (t0 $ Abs (s, T1, t12)) |
|
1251 | (t10 as @{const Not}) $ t11 => |
|
1252 t10 $ distribute_quantifiers (Const (@{const_name All}, T0) |
|
1253 $ Abs (s, T1, t11)) |
|
1254 | t1 => |
|
1255 if not (loose_bvar1 (t1, 0)) then |
|
1256 distribute_quantifiers (incr_boundvars ~1 t1) |
|
1257 else |
|
1258 t0 $ Abs (s, T1, distribute_quantifiers t1)) |
|
1259 | t1 $ t2 => distribute_quantifiers t1 $ distribute_quantifiers t2 |
|
1260 | Abs (s, T, t') => Abs (s, T, distribute_quantifiers t') |
|
1261 | _ => t |
|
1262 |
|
1263 (** Quantifier massaging: Pushing quantifiers inward **) |
|
1264 |
|
1265 (* int -> int -> (int -> int) -> term -> term *) |
|
1266 fun renumber_bounds j n f t = |
|
1267 case t of |
|
1268 t1 $ t2 => renumber_bounds j n f t1 $ renumber_bounds j n f t2 |
|
1269 | Abs (s, T, t') => Abs (s, T, renumber_bounds (j + 1) n f t') |
|
1270 | Bound j' => |
|
1271 Bound (if j' >= j andalso j' < j + n then f (j' - j) + j else j') |
|
1272 | _ => t |
|
1273 |
|
1274 (* Maximum number of quantifiers in a cluster for which the exponential |
|
1275 algorithm is used. Larger clusters use a heuristic inspired by Claessen & |
|
1276 Sörensson's polynomial binary splitting procedure (p. 5 of their MODEL 2003 |
|
1277 paper). *) |
|
1278 val quantifier_cluster_threshold = 7 |
|
1279 |
|
1280 (* theory -> term -> term *) |
|
1281 fun push_quantifiers_inward thy = |
|
1282 let |
|
1283 (* string -> string list -> typ list -> term -> term *) |
|
1284 fun aux quant_s ss Ts t = |
|
1285 (case t of |
|
1286 (t0 as Const (s0, _)) $ Abs (s1, T1, t1 as _ $ _) => |
|
1287 if s0 = quant_s then |
|
1288 aux s0 (s1 :: ss) (T1 :: Ts) t1 |
|
1289 else if quant_s = "" andalso |
|
1290 (s0 = @{const_name All} orelse s0 = @{const_name Ex}) then |
|
1291 aux s0 [s1] [T1] t1 |
|
1292 else |
|
1293 raise SAME () |
|
1294 | _ => raise SAME ()) |
|
1295 handle SAME () => |
|
1296 case t of |
|
1297 t1 $ t2 => |
|
1298 if quant_s = "" then |
|
1299 aux "" [] [] t1 $ aux "" [] [] t2 |
|
1300 else |
|
1301 let |
|
1302 val typical_card = 4 |
|
1303 (* ('a -> ''b list) -> 'a list -> ''b list *) |
|
1304 fun big_union proj ps = |
|
1305 fold (fold (insert (op =)) o proj) ps [] |
|
1306 val (ts, connective) = strip_any_connective t |
|
1307 val T_costs = |
|
1308 map (bounded_card_of_type 65536 typical_card []) Ts |
|
1309 val t_costs = map size_of_term ts |
|
1310 val num_Ts = length Ts |
|
1311 (* int -> int *) |
|
1312 val flip = curry (op -) (num_Ts - 1) |
|
1313 val t_boundss = map (map flip o loose_bnos) ts |
|
1314 (* (int list * int) list -> int list |
|
1315 -> (int list * int) list *) |
|
1316 fun merge costly_boundss [] = costly_boundss |
|
1317 | merge costly_boundss (j :: js) = |
|
1318 let |
|
1319 val (yeas, nays) = |
|
1320 List.partition (fn (bounds, _) => |
|
1321 member (op =) bounds j) |
|
1322 costly_boundss |
|
1323 val yeas_bounds = big_union fst yeas |
|
1324 val yeas_cost = Integer.sum (map snd yeas) |
|
1325 * nth T_costs j |
|
1326 in merge ((yeas_bounds, yeas_cost) :: nays) js end |
|
1327 (* (int list * int) list -> int list -> int *) |
|
1328 val cost = Integer.sum o map snd oo merge |
|
1329 (* (int list * int) list -> int list -> int list *) |
|
1330 fun heuristically_best_permutation _ [] = [] |
|
1331 | heuristically_best_permutation costly_boundss js = |
|
1332 let |
|
1333 val (costly_boundss, (j, js)) = |
|
1334 js |> map (`(merge costly_boundss o single)) |
|
1335 |> sort (int_ord |
|
1336 o pairself (Integer.sum o map snd o fst)) |
|
1337 |> split_list |>> hd ||> pairf hd tl |
|
1338 in |
|
1339 j :: heuristically_best_permutation costly_boundss js |
|
1340 end |
|
1341 val js = |
|
1342 if length Ts <= quantifier_cluster_threshold then |
|
1343 all_permutations (index_seq 0 num_Ts) |
|
1344 |> map (`(cost (t_boundss ~~ t_costs))) |
|
1345 |> sort (int_ord o pairself fst) |> hd |> snd |
|
1346 else |
|
1347 heuristically_best_permutation (t_boundss ~~ t_costs) |
|
1348 (index_seq 0 num_Ts) |
|
1349 val back_js = map (fn j => find_index (curry (op =) j) js) |
|
1350 (index_seq 0 num_Ts) |
|
1351 val ts = map (renumber_bounds 0 num_Ts (nth back_js o flip)) |
|
1352 ts |
|
1353 (* (term * int list) list -> term *) |
|
1354 fun mk_connection [] = |
|
1355 raise ARG ("Nitpick_Preproc.push_quantifiers_inward.aux.\ |
|
1356 \mk_connection", "") |
|
1357 | mk_connection ts_cum_bounds = |
|
1358 ts_cum_bounds |> map fst |
|
1359 |> foldr1 (fn (t1, t2) => connective $ t1 $ t2) |
|
1360 (* (term * int list) list -> int list -> term *) |
|
1361 fun build ts_cum_bounds [] = ts_cum_bounds |> mk_connection |
|
1362 | build ts_cum_bounds (j :: js) = |
|
1363 let |
|
1364 val (yeas, nays) = |
|
1365 List.partition (fn (_, bounds) => |
|
1366 member (op =) bounds j) |
|
1367 ts_cum_bounds |
|
1368 ||> map (apfst (incr_boundvars ~1)) |
|
1369 in |
|
1370 if null yeas then |
|
1371 build nays js |
|
1372 else |
|
1373 let val T = nth Ts (flip j) in |
|
1374 build ((Const (quant_s, (T --> bool_T) --> bool_T) |
|
1375 $ Abs (nth ss (flip j), T, |
|
1376 mk_connection yeas), |
|
1377 big_union snd yeas) :: nays) js |
|
1378 end |
|
1379 end |
|
1380 in build (ts ~~ t_boundss) js end |
|
1381 | Abs (s, T, t') => Abs (s, T, aux "" [] [] t') |
|
1382 | _ => t |
|
1383 in aux "" [] [] end |
|
1384 |
|
1385 (** Preprocessor entry point **) |
|
1386 |
|
1387 (* hol_context -> term -> ((term list * term list) * (bool * bool)) * term *) |
|
1388 fun preprocess_term (hol_ctxt as {thy, binary_ints, destroy_constrs, boxes, |
|
1389 skolemize, uncurry, ...}) t = |
|
1390 let |
|
1391 val skolem_depth = if skolemize then 4 else ~1 |
|
1392 val (((def_ts, nondef_ts), (got_all_mono_user_axioms, no_poly_user_axioms)), |
|
1393 core_t) = t |> unfold_defs_in_term hol_ctxt |
|
1394 |> Refute.close_form |
|
1395 |> skolemize_term_and_more hol_ctxt skolem_depth |
|
1396 |> specialize_consts_in_term hol_ctxt 0 |
|
1397 |> `(axioms_for_term hol_ctxt) |
|
1398 val binarize = |
|
1399 case binary_ints of |
|
1400 SOME false => false |
|
1401 | _ => |
|
1402 forall may_use_binary_ints (core_t :: def_ts @ nondef_ts) andalso |
|
1403 (binary_ints = SOME true orelse |
|
1404 exists should_use_binary_ints (core_t :: def_ts @ nondef_ts)) |
|
1405 val box = exists (not_equal (SOME false) o snd) boxes |
|
1406 val table = |
|
1407 Termtab.empty |> uncurry |
|
1408 ? fold (add_to_uncurry_table thy) (core_t :: def_ts @ nondef_ts) |
|
1409 (* bool -> bool -> term -> term *) |
|
1410 fun do_rest def core = |
|
1411 binarize ? binarize_nat_and_int_in_term |
|
1412 #> uncurry ? uncurry_term table |
|
1413 #> box ? box_fun_and_pair_in_term hol_ctxt def |
|
1414 #> destroy_constrs ? (pull_out_universal_constrs thy def |
|
1415 #> pull_out_existential_constrs thy |
|
1416 #> destroy_pulled_out_constrs hol_ctxt def) |
|
1417 #> curry_assms |
|
1418 #> destroy_universal_equalities |
|
1419 #> destroy_existential_equalities thy |
|
1420 #> simplify_constrs_and_sels thy |
|
1421 #> distribute_quantifiers |
|
1422 #> push_quantifiers_inward thy |
|
1423 #> not core ? Refute.close_form |
|
1424 #> Term.map_abs_vars shortest_name |
|
1425 in |
|
1426 (((map (do_rest true false) def_ts, map (do_rest false false) nondef_ts), |
|
1427 (got_all_mono_user_axioms, no_poly_user_axioms)), |
|
1428 do_rest false true core_t) |
|
1429 end |
|
1430 |
|
1431 end; |