1 (* Title: HOL/Tools/Nitpick/nitpick_model.ML
2 Author: Jasmin Blanchette, TU Muenchen
5 Model reconstruction for Nitpick.
8 signature NITPICK_MODEL =
10 type styp = Nitpick_Util.styp
11 type scope = Nitpick_Scope.scope
12 type rep = Nitpick_Rep.rep
13 type nut = Nitpick_Nut.nut
16 {show_datatypes: bool,
19 type term_postprocessor =
20 Proof.context -> string -> (typ -> term list) -> typ -> term -> term
22 structure NameTable : TABLE
24 val irrelevant : string
27 val register_term_postprocessor :
28 typ -> term_postprocessor -> theory -> theory
29 val unregister_term_postprocessor : typ -> theory -> theory
30 val tuple_list_for_name :
31 nut NameTable.table -> Kodkod.raw_bound list -> nut -> int list list
32 val dest_plain_fun : term -> bool * (term list * term list)
33 val reconstruct_hol_model :
34 params -> scope -> (term option * int list) list -> styp list -> nut list
35 -> nut list -> nut list -> nut NameTable.table -> Kodkod.raw_bound list
38 scope -> Time.time option -> nut list -> nut list -> nut NameTable.table
39 -> Kodkod.raw_bound list -> term -> bool option
42 structure Nitpick_Model : NITPICK_MODEL =
55 {show_datatypes: bool,
58 type term_postprocessor =
59 Proof.context -> string -> (typ -> term list) -> typ -> term -> term
61 structure Data = Theory_Data(
62 type T = (typ * term_postprocessor) list
65 fun merge (x, y) = AList.merge (op =) (K true) (x, y))
70 val maybe_mixfix = "_\<^sup>?"
71 val base_mixfix = "_\<^bsub>base\<^esub>"
72 val step_mixfix = "_\<^bsub>step\<^esub>"
73 val abs_mixfix = "\<guillemotleft>_\<guillemotright>"
74 val arg_var_prefix = "x"
75 val cyclic_co_val_name = "\<omega>"
76 val cyclic_const_prefix = "\<xi>"
77 val cyclic_type_name = nitpick_prefix ^ cyclic_const_prefix
78 val opt_flag = nitpick_prefix ^ "opt"
79 val non_opt_flag = nitpick_prefix ^ "non_opt"
81 type atom_pool = ((string * int) * int list) list
83 fun add_wacky_syntax ctxt =
85 val name_of = fst o dest_Const
86 val thy = ProofContext.theory_of ctxt |> Context.reject_draft
88 Sign.declare_const ((@{binding nitpick_maybe}, @{typ "'a => 'a"}),
89 Mixfix (maybe_mixfix, [1000], 1000)) thy
91 Sign.declare_const ((@{binding nitpick_abs}, @{typ "'a => 'b"}),
92 Mixfix (abs_mixfix, [40], 40)) thy
94 Sign.declare_const ((@{binding nitpick_base}, @{typ "'a => 'a"}),
95 Mixfix (base_mixfix, [1000], 1000)) thy
97 Sign.declare_const ((@{binding nitpick_step}, @{typ "'a => 'a"}),
98 Mixfix (step_mixfix, [1000], 1000)) thy
100 (pairself (pairself name_of) ((maybe_t, abs_t), (base_t, step_t)),
101 ProofContext.transfer_syntax thy ctxt)
104 (** Term reconstruction **)
106 fun nth_atom_suffix pool s j k =
107 (case AList.lookup (op =) (!pool) (s, k) of
109 (case find_index (curry (op =) j) js of
110 ~1 => (Unsynchronized.change pool (cons ((s, k), j :: js));
112 | n => length js - n)
113 | NONE => (Unsynchronized.change pool (cons ((s, k), [j])); 1))
115 |> (s <> "" andalso Symbol.is_ascii_digit (List.last (explode s)))
117 fun nth_atom_name pool prefix (Type (s, _)) j k =
118 let val s' = shortest_name s in
119 prefix ^ (if String.isPrefix "\\" s' then s' else substring (s', 0, 1)) ^
120 nth_atom_suffix pool s j k
122 | nth_atom_name pool prefix (TFree (s, _)) j k =
123 prefix ^ perhaps (try (unprefix "'")) s ^ nth_atom_suffix pool s j k
124 | nth_atom_name _ _ T _ _ =
125 raise TYPE ("Nitpick_Model.nth_atom_name", [T], [])
126 fun nth_atom pool for_auto T j k =
128 Free (nth_atom_name pool (hd (space_explode "." nitpick_prefix)) T j k, T)
130 Const (nth_atom_name pool "" T j k, T)
132 fun extract_real_number (Const (@{const_name divide}, _) $ t1 $ t2) =
133 real (snd (HOLogic.dest_number t1)) / real (snd (HOLogic.dest_number t2))
134 | extract_real_number t = real (snd (HOLogic.dest_number t))
135 fun nice_term_ord (Abs (_, _, t1), Abs (_, _, t2)) = nice_term_ord (t1, t2)
136 | nice_term_ord tp = Real.compare (pairself extract_real_number tp)
137 handle TERM ("dest_number", _) =>
139 (t11 $ t12, t21 $ t22) =>
140 (case nice_term_ord (t11, t21) of
141 EQUAL => nice_term_ord (t12, t22)
143 | _ => Term_Ord.fast_term_ord tp
145 fun register_term_postprocessor T p = Data.map (cons (T, p))
146 fun unregister_term_postprocessor T = Data.map (AList.delete (op =) T)
148 fun tuple_list_for_name rel_table bounds name =
149 the (AList.lookup (op =) bounds (the_rel rel_table name)) handle NUT _ => [[]]
151 fun unarize_unbox_etc_term (Const (@{const_name FinFun}, _) $ t1) =
152 unarize_unbox_etc_term t1
153 | unarize_unbox_etc_term (Const (@{const_name FunBox}, _) $ t1) =
154 unarize_unbox_etc_term t1
155 | unarize_unbox_etc_term
156 (Const (@{const_name PairBox},
157 Type (@{type_name fun}, [T1, Type (@{type_name fun}, [T2, _])]))
159 let val Ts = map uniterize_unarize_unbox_etc_type [T1, T2] in
160 Const (@{const_name Pair}, Ts ---> Type (@{type_name "*"}, Ts))
161 $ unarize_unbox_etc_term t1 $ unarize_unbox_etc_term t2
163 | unarize_unbox_etc_term (Const (s, T)) =
164 Const (s, uniterize_unarize_unbox_etc_type T)
165 | unarize_unbox_etc_term (t1 $ t2) =
166 unarize_unbox_etc_term t1 $ unarize_unbox_etc_term t2
167 | unarize_unbox_etc_term (Free (s, T)) =
168 Free (s, uniterize_unarize_unbox_etc_type T)
169 | unarize_unbox_etc_term (Var (x, T)) =
170 Var (x, uniterize_unarize_unbox_etc_type T)
171 | unarize_unbox_etc_term (Bound j) = Bound j
172 | unarize_unbox_etc_term (Abs (s, T, t')) =
173 Abs (s, uniterize_unarize_unbox_etc_type T, unarize_unbox_etc_term t')
175 fun factor_out_types (T1 as Type (@{type_name "*"}, [T11, T12]))
176 (T2 as Type (@{type_name "*"}, [T21, T22])) =
177 let val (n1, n2) = pairself num_factors_in_type (T11, T21) in
180 val ((T11', opt_T12'), (T21', opt_T22')) = factor_out_types T12 T22
182 ((Type (@{type_name "*"}, [T11, T11']), opt_T12'),
183 (Type (@{type_name "*"}, [T21, T21']), opt_T22'))
186 case factor_out_types T1 T21 of
187 (p1, (T21', NONE)) => (p1, (T21', SOME T22))
188 | (p1, (T21', SOME T22')) =>
189 (p1, (T21', SOME (Type (@{type_name "*"}, [T22', T22]))))
191 swap (factor_out_types T2 T1)
193 | factor_out_types (Type (@{type_name "*"}, [T11, T12])) T2 =
194 ((T11, SOME T12), (T2, NONE))
195 | factor_out_types T1 (Type (@{type_name "*"}, [T21, T22])) =
196 ((T1, NONE), (T21, SOME T22))
197 | factor_out_types T1 T2 = ((T1, NONE), (T2, NONE))
199 fun make_plain_fun maybe_opt T1 T2 =
202 Const (if maybe_opt then opt_flag else non_opt_flag, T1 --> T2)
203 | aux T1 T2 ((t1, t2) :: tps) =
204 Const (@{const_name fun_upd}, (T1 --> T2) --> T1 --> T2 --> T1 --> T2)
205 $ aux T1 T2 tps $ t1 $ t2
206 in aux T1 T2 o rev end
207 fun is_plain_fun (Const (s, _)) = (s = opt_flag orelse s = non_opt_flag)
208 | is_plain_fun (Const (@{const_name fun_upd}, _) $ t0 $ _ $ _) =
210 | is_plain_fun _ = false
213 fun aux (Abs (_, _, Const (s, _))) = (s <> irrelevant, ([], []))
214 | aux (Const (s, _)) = (s <> non_opt_flag, ([], []))
215 | aux (Const (@{const_name fun_upd}, _) $ t0 $ t1 $ t2) =
216 let val (maybe_opt, (ts1, ts2)) = aux t0 in
217 (maybe_opt, (t1 :: ts1, t2 :: ts2))
219 | aux t = raise TERM ("Nitpick_Model.dest_plain_fun", [t])
220 in apsnd (pairself rev) o aux end
222 fun break_in_two T T1 T2 t =
224 val ps = HOLogic.flat_tupleT_paths T
225 val cut = length (HOLogic.strip_tupleT T1)
226 val (ps1, ps2) = pairself HOLogic.flat_tupleT_paths (T1, T2)
227 val (ts1, ts2) = t |> HOLogic.strip_ptuple ps |> chop cut
228 in (HOLogic.mk_ptuple ps1 T1 ts1, HOLogic.mk_ptuple ps2 T2 ts2) end
229 fun pair_up (Type (@{type_name "*"}, [T1', T2']))
230 (t1 as Const (@{const_name Pair},
231 Type (@{type_name fun},
232 [_, Type (@{type_name fun}, [_, T1])]))
234 if T1 = T1' then HOLogic.mk_prod (t1, t2)
235 else HOLogic.mk_prod (t11, pair_up T2' t12 t2)
236 | pair_up _ t1 t2 = HOLogic.mk_prod (t1, t2)
237 fun multi_pair_up T1 t1 (ts2, ts3) = map2 (pair o pair_up T1 t1) ts2 ts3
239 fun typecast_fun (Type (@{type_name fun}, [T1', T2'])) T1 T2 t =
241 fun do_curry T1 T1a T1b T2 t =
243 val (maybe_opt, tsp) = dest_plain_fun t
245 tsp |>> map (break_in_two T1 T1a T1b)
246 |> uncurry (map2 (fn (t1a, t1b) => fn t2 => (t1a, (t1b, t2))))
247 |> AList.coalesce (op =)
248 |> map (apsnd (make_plain_fun maybe_opt T1b T2))
249 in make_plain_fun maybe_opt T1a (T1b --> T2) tps end
250 and do_uncurry T1 T2 t =
252 val (maybe_opt, tsp) = dest_plain_fun t
255 |> maps (fn (t1, t2) =>
256 multi_pair_up T1 t1 (snd (dest_plain_fun t2)))
257 in make_plain_fun maybe_opt T1 T2 tps end
258 and do_arrow T1' T2' _ _ (Const (s, _)) = Const (s, T1' --> T2')
259 | do_arrow T1' T2' T1 T2
260 (Const (@{const_name fun_upd}, _) $ t0 $ t1 $ t2) =
261 Const (@{const_name fun_upd},
262 (T1' --> T2') --> T1' --> T2' --> T1' --> T2')
263 $ do_arrow T1' T2' T1 T2 t0 $ do_term T1' T1 t1 $ do_term T2' T2 t2
264 | do_arrow _ _ _ _ t =
265 raise TERM ("Nitpick_Model.typecast_fun.do_arrow", [t])
266 and do_fun T1' T2' T1 T2 t =
267 case factor_out_types T1' T1 of
268 ((_, NONE), (_, NONE)) => t |> do_arrow T1' T2' T1 T2
269 | ((_, NONE), (T1a, SOME T1b)) =>
270 t |> do_curry T1 T1a T1b T2 |> do_arrow T1' T2' T1a (T1b --> T2)
271 | ((T1a', SOME T1b'), (_, NONE)) =>
272 t |> do_arrow T1a' (T1b' --> T2') T1 T2 |> do_uncurry T1' T2'
273 | _ => raise TYPE ("Nitpick_Model.typecast_fun.do_fun", [T1, T1'], [])
274 and do_term (Type (@{type_name fun}, [T1', T2']))
275 (Type (@{type_name fun}, [T1, T2])) t =
276 do_fun T1' T2' T1 T2 t
277 | do_term (T' as Type (@{type_name "*"}, Ts' as [T1', T2']))
278 (Type (@{type_name "*"}, [T1, T2]))
279 (Const (@{const_name Pair}, _) $ t1 $ t2) =
280 Const (@{const_name Pair}, Ts' ---> T')
281 $ do_term T1' T1 t1 $ do_term T2' T2 t2
284 else raise TYPE ("Nitpick_Model.typecast_fun.do_term", [T, T'], [])
285 in if T1' = T1 andalso T2' = T2 then t else do_fun T1' T2' T1 T2 t end
286 | typecast_fun T' _ _ _ =
287 raise TYPE ("Nitpick_Model.typecast_fun", [T'], [])
289 fun truth_const_sort_key @{const True} = "0"
290 | truth_const_sort_key @{const False} = "2"
291 | truth_const_sort_key _ = "1"
293 fun mk_tuple (Type (@{type_name "*"}, [T1, T2])) ts =
294 HOLogic.mk_prod (mk_tuple T1 ts,
295 mk_tuple T2 (List.drop (ts, length (HOLogic.flatten_tupleT T1))))
296 | mk_tuple _ (t :: _) = t
297 | mk_tuple T [] = raise TYPE ("Nitpick_Model.mk_tuple", [T], [])
299 fun varified_type_match thy (candid_T, pat_T) =
300 strict_type_match thy (candid_T, Logic.varifyT_global pat_T)
302 fun all_values_of_type pool wacky_names (scope as {card_assigns, ...} : scope)
303 sel_names rel_table bounds card T =
305 val card = if card = 0 then card_of_type card_assigns T else card
306 fun nth_value_of_type n =
309 reconstruct_term unfold pool wacky_names scope sel_names rel_table
310 bounds T T (Atom (card, 0)) [[n]]
314 if String.isPrefix cyclic_const_prefix s then
315 HOLogic.mk_eq (t, term true)
320 in index_seq 0 card |> map nth_value_of_type |> sort nice_term_ord end
321 and reconstruct_term unfold pool (wacky_names as ((maybe_name, abs_name), _))
322 (scope as {hol_ctxt as {thy, ctxt, stds, ...}, binarize, card_assigns,
323 bits, datatypes, ofs, ...}) sel_names rel_table bounds =
325 val for_auto = (maybe_name = "")
326 fun value_of_bits jss =
328 val j0 = offset_of_type ofs @{typ unsigned_bit}
329 val js = map (Integer.add (~ j0) o the_single) jss
331 fold (fn j => Integer.add (reasonable_power 2 j |> j = bits ? op ~))
335 all_values_of_type pool wacky_names scope sel_names rel_table bounds 0
336 fun postprocess_term (Type (@{type_name fun}, _)) = I
337 | postprocess_term T =
338 if null (Data.get thy) then
340 else case AList.lookup (varified_type_match thy) (Data.get thy) T of
341 SOME postproc => postproc ctxt maybe_name all_values T
343 fun postprocess_subterms Ts (t1 $ t2) =
344 let val t = postprocess_subterms Ts t1 $ postprocess_subterms Ts t2 in
345 postprocess_term (fastype_of1 (Ts, t)) t
347 | postprocess_subterms Ts (Abs (s, T, t')) =
348 Abs (s, T, postprocess_subterms (T :: Ts) t')
349 | postprocess_subterms Ts t = postprocess_term (fastype_of1 (Ts, t)) t
350 fun make_set maybe_opt T1 T2 tps =
352 val empty_const = Const (@{const_abbrev Set.empty}, T1 --> T2)
353 val insert_const = Const (@{const_name insert},
354 T1 --> (T1 --> T2) --> T1 --> T2)
356 if maybe_opt andalso not (is_complete_type datatypes false T1) then
357 insert_const $ Const (unrep, T1) $ empty_const
360 | aux ((t1, t2) :: zs) =
362 |> t2 <> @{const False}
365 $ (t1 |> t2 <> @{const True}
367 (Const (maybe_name, T1 --> T1))))
369 if forall (fn (_, t) => t <> @{const True} andalso t <> @{const False})
371 Const (unknown, T1 --> T2)
375 fun make_map maybe_opt T1 T2 T2' =
377 val update_const = Const (@{const_name fun_upd},
378 (T1 --> T2) --> T1 --> T2 --> T1 --> T2)
379 fun aux' [] = Const (@{const_abbrev Map.empty}, T1 --> T2)
380 | aux' ((t1, t2) :: tps) =
382 Const (@{const_name None}, _) => aux' tps
383 | _ => update_const $ aux' tps $ t1 $ t2)
385 if maybe_opt andalso not (is_complete_type datatypes false T1) then
386 update_const $ aux' tps $ Const (unrep, T1)
387 $ (Const (@{const_name Some}, T2' --> T2) $ Const (unknown, T2'))
391 fun polish_funs Ts t =
392 (case fastype_of1 (Ts, t) of
393 Type (@{type_name fun}, [T1, T2]) =>
394 if is_plain_fun t then
398 val (maybe_opt, ts_pair) =
399 dest_plain_fun t ||> pairself (map (polish_funs Ts))
401 make_set maybe_opt T1 T2
402 (sort_wrt (truth_const_sort_key o snd) (op ~~ ts_pair))
404 | Type (@{type_name option}, [T2']) =>
406 val (maybe_opt, ts_pair) =
407 dest_plain_fun t ||> pairself (map (polish_funs Ts))
408 in make_map maybe_opt T1 T2 T2' (rev (op ~~ ts_pair)) end
412 | _ => raise SAME ())
415 (t1 as Const (@{const_name fun_upd}, _) $ t11 $ _)
416 $ (t2 as Const (s, _)) =>
417 if s = unknown then polish_funs Ts t11
418 else polish_funs Ts t1 $ polish_funs Ts t2
419 | t1 $ t2 => polish_funs Ts t1 $ polish_funs Ts t2
420 | Abs (s, T, t') => Abs (s, T, polish_funs (T :: Ts) t')
421 | Const (s, Type (@{type_name fun}, [T1, T2])) =>
422 if s = opt_flag orelse s = non_opt_flag then
424 Const (if is_complete_type datatypes false T1 then
431 fun make_fun maybe_opt T1 T2 T' ts1 ts2 =
432 ts1 ~~ ts2 |> sort (nice_term_ord o pairself fst)
433 |> make_plain_fun maybe_opt T1 T2
434 |> unarize_unbox_etc_term
435 |> typecast_fun (uniterize_unarize_unbox_etc_type T')
436 (uniterize_unarize_unbox_etc_type T1)
437 (uniterize_unarize_unbox_etc_type T2)
438 fun term_for_atom seen (T as Type (@{type_name fun}, [T1, T2])) T' j _ =
440 val k1 = card_of_type card_assigns T1
441 val k2 = card_of_type card_assigns T2
443 term_for_rep true seen T T' (Vect (k1, Atom (k2, 0)))
444 [nth_combination (replicate k1 (k2, 0)) j]
445 handle General.Subscript =>
446 raise ARG ("Nitpick_Model.reconstruct_term.term_for_atom",
447 signed_string_of_int j ^ " for " ^
448 string_for_rep (Vect (k1, Atom (k2, 0))))
450 | term_for_atom seen (Type (@{type_name "*"}, [T1, T2])) _ j k =
452 val k1 = card_of_type card_assigns T1
455 list_comb (HOLogic.pair_const T1 T2,
456 map3 (fn T => term_for_atom seen T T) [T1, T2]
457 [j div k2, j mod k2] [k1, k2]) (* ### k2 or k1? FIXME *)
459 | term_for_atom seen @{typ prop} _ j k =
460 HOLogic.mk_Trueprop (term_for_atom seen bool_T bool_T j k)
461 | term_for_atom _ @{typ bool} _ j _ =
462 if j = 0 then @{const False} else @{const True}
463 | term_for_atom _ @{typ unit} _ _ _ = @{const Unity}
464 | term_for_atom seen T _ j k =
465 if T = nat_T andalso is_standard_datatype thy stds nat_T then
466 HOLogic.mk_number nat_T j
467 else if T = int_T then
468 HOLogic.mk_number int_T (int_for_atom (k, 0) j)
469 else if is_fp_iterator_type T then
470 HOLogic.mk_number nat_T (k - j - 1)
471 else if T = @{typ bisim_iterator} then
472 HOLogic.mk_number nat_T j
473 else case datatype_spec datatypes T of
474 NONE => nth_atom pool for_auto T j k
475 | SOME {deep = false, ...} => nth_atom pool for_auto T j k
476 | SOME {co, standard, constrs, ...} =>
478 fun tuples_for_const (s, T) =
479 tuple_list_for_name rel_table bounds (ConstName (s, T, Any))
481 nth_atom pool for_auto (Type (cyclic_type_name, [])) j k
482 fun cyclic_var () = Var ((nth_atom_name pool "" T j k, 0), T)
484 val discr_jsss = map (tuples_for_const o discr_for_constr o #const)
486 val real_j = j + offset_of_type ofs T
487 val constr_x as (constr_s, constr_T) =
488 get_first (fn (jss, {const, ...}) =>
489 if member (op =) jss [real_j] then SOME const
491 (discr_jsss ~~ constrs) |> the
492 val arg_Ts = curried_binder_types constr_T
494 map (binarized_and_boxed_nth_sel_for_constr hol_ctxt binarize
496 (index_seq 0 (length arg_Ts))
498 map (fn x => get_first
499 (fn ConstName (s', T', R) =>
500 if (s', T') = x then SOME R else NONE
501 | u => raise NUT ("Nitpick_Model.reconstruct_\
502 \term.term_for_atom", [u]))
503 sel_names |> the) sel_xs
504 val arg_Rs = map (snd o dest_Func) sel_Rs
505 val sel_jsss = map tuples_for_const sel_xs
507 map (map_filter (fn js => if hd js = real_j then SOME (tl js)
509 val uncur_arg_Ts = binder_types constr_T
510 val maybe_cyclic = co orelse not standard
512 if maybe_cyclic andalso not (null seen) andalso
513 member (op =) (seen |> unfold ? (fst o split_last)) (T, j) then
515 else if constr_s = @{const_name Word} then
517 (if T = @{typ "unsigned_bit word"} then nat_T else int_T)
518 (value_of_bits (the_single arg_jsss))
521 val seen = seen |> maybe_cyclic ? cons (T, j)
523 if length arg_Ts = 0 then
527 term_for_rep (constr_s <> @{const_name FinFun})
528 seen Ts Ts) arg_Ts arg_Rs arg_jsss
529 |> mk_tuple (HOLogic.mk_tupleT uncur_arg_Ts)
530 |> dest_n_tuple (length uncur_arg_Ts)
532 if constr_s = @{const_name Abs_Frac} then
534 [Const (@{const_name Pair}, _) $ t1 $ t2] =>
535 frac_from_term_pair (body_type T) t1 t2
536 | _ => raise TERM ("Nitpick_Model.reconstruct_term.\
537 \term_for_atom (Abs_Frac)", ts)
538 else if not for_auto andalso
539 (is_abs_fun ctxt constr_x orelse
540 constr_s = @{const_name Quot}) then
541 Const (abs_name, constr_T) $ the_single ts
543 list_comb (Const constr_x, ts)
546 let val var = cyclic_var () in
547 if unfold andalso not standard andalso
548 length seen = 1 andalso
549 exists_subterm (fn Const (s, _) =>
550 String.isPrefix cyclic_const_prefix s
551 | t' => t' = var) t then
552 subst_atomic [(var, cyclic_atom ())] t
553 else if exists_subterm (curry (op =) var) t then
555 Const (@{const_name The}, (T --> bool_T) --> T)
556 $ Abs (cyclic_co_val_name, T,
557 Const (@{const_name "op ="}, T --> T --> bool_T)
558 $ Bound 0 $ abstract_over (var, t))
568 and term_for_vect seen k R T1 T2 T' js =
569 make_fun true T1 T2 T'
570 (map (fn j => term_for_atom seen T1 T1 j k) (index_seq 0 k))
571 (map (term_for_rep true seen T2 T2 R o single)
572 (batch_list (arity_of_rep R) js))
573 and term_for_rep _ seen T T' Unit [[]] = term_for_atom seen T T' 0 1
574 | term_for_rep _ seen T T' (R as Atom (k, j0)) [[j]] =
575 if j >= j0 andalso j < j0 + k then term_for_atom seen T T' (j - j0) k
576 else raise REP ("Nitpick_Model.reconstruct_term.term_for_rep", [R])
577 | term_for_rep _ seen (Type (@{type_name "*"}, [T1, T2])) _
578 (Struct [R1, R2]) [js] =
580 val arity1 = arity_of_rep R1
581 val (js1, js2) = chop arity1 js
583 list_comb (HOLogic.pair_const T1 T2,
584 map3 (fn T => term_for_rep true seen T T) [T1, T2] [R1, R2]
587 | term_for_rep _ seen (Type (@{type_name fun}, [T1, T2])) T'
588 (Vect (k, R')) [js] =
589 term_for_vect seen k R' T1 T2 T' js
590 | term_for_rep maybe_opt seen (Type (@{type_name fun}, [T1, T2])) T'
591 (Func (R1, Formula Neut)) jss =
593 val jss1 = all_combinations_for_rep R1
594 val ts1 = map (term_for_rep true seen T1 T1 R1 o single) jss1
596 map (fn js => term_for_rep true seen T2 T2 (Atom (2, 0))
597 [[int_from_bool (member (op =) jss js)]])
599 in make_fun maybe_opt T1 T2 T' ts1 ts2 end
600 | term_for_rep maybe_opt seen (Type (@{type_name fun}, [T1, T2])) T'
601 (Func (R1, R2)) jss =
603 val arity1 = arity_of_rep R1
604 val jss1 = all_combinations_for_rep R1
605 val ts1 = map (term_for_rep false seen T1 T1 R1 o single) jss1
606 val grouped_jss2 = AList.group (op =) (map (chop arity1) jss)
607 val ts2 = map (term_for_rep false seen T2 T2 R2 o the_default []
608 o AList.lookup (op =) grouped_jss2) jss1
609 in make_fun maybe_opt T1 T2 T' ts1 ts2 end
610 | term_for_rep _ seen T T' (Opt R) jss =
611 if null jss then Const (unknown, T)
612 else term_for_rep true seen T T' R jss
613 | term_for_rep _ _ T _ R jss =
614 raise ARG ("Nitpick_Model.reconstruct_term.term_for_rep",
615 Refute.string_of_typ T ^ " " ^ string_for_rep R ^ " " ^
616 string_of_int (length jss))
618 postprocess_subterms [] o polish_funs [] o unarize_unbox_etc_term
619 oooo term_for_rep true []
622 (** Constant postprocessing **)
624 fun dest_n_tuple_type 1 T = [T]
625 | dest_n_tuple_type n (Type (_, [T1, T2])) =
626 T1 :: dest_n_tuple_type (n - 1) T2
627 | dest_n_tuple_type _ T =
628 raise TYPE ("Nitpick_Model.dest_n_tuple_type", [T], [])
630 fun const_format thy def_table (x as (s, T)) =
631 if String.isPrefix unrolled_prefix s then
632 const_format thy def_table (original_name s, range_type T)
633 else if String.isPrefix skolem_prefix s then
635 val k = unprefix skolem_prefix s
636 |> strip_first_name_sep |> fst |> space_explode "@"
637 |> hd |> Int.fromString |> the
638 in [k, num_binder_types T - k] end
639 else if original_name s <> s then
641 else case def_of_const thy def_table x of
642 SOME t' => if fixpoint_kind_of_rhs t' <> NoFp then
643 let val k = length (strip_abs_vars t') in
644 [k, num_binder_types T - k]
648 | NONE => [num_binder_types T]
649 fun intersect_formats _ [] = []
650 | intersect_formats [] _ = []
651 | intersect_formats ks1 ks2 =
652 let val ((ks1', k1), (ks2', k2)) = pairself split_last (ks1, ks2) in
653 intersect_formats (ks1' @ (if k1 > k2 then [k1 - k2] else []))
654 (ks2' @ (if k2 > k1 then [k2 - k1] else [])) @
658 fun lookup_format thy def_table formats t =
659 case AList.lookup (fn (SOME x, SOME y) =>
660 (term_match thy) (x, y) | _ => false)
662 SOME format => format
663 | NONE => let val format = the (AList.lookup (op =) formats NONE) in
665 Const x => intersect_formats format
666 (const_format thy def_table x)
670 fun format_type default_format format T =
672 val T = uniterize_unarize_unbox_etc_type T
673 val format = format |> filter (curry (op <) 0)
675 if forall (curry (op =) 1) format then
679 val (binder_Ts, body_T) = strip_type T
682 |> map (format_type default_format default_format)
683 |> rev |> chunk_list_unevenly (rev format)
684 |> map (HOLogic.mk_tupleT o rev)
685 in List.foldl (op -->) body_T batched end
687 fun format_term_type thy def_table formats t =
688 format_type (the (AList.lookup (op =) formats NONE))
689 (lookup_format thy def_table formats t) (fastype_of t)
691 fun repair_special_format js m format =
692 m - 1 downto 0 |> chunk_list_unevenly (rev format)
693 |> map (rev o filter_out (member (op =) js))
694 |> filter_out null |> map length |> rev
696 fun user_friendly_const ({thy, evals, def_table, skolems, special_funs, ...}
697 : hol_context) (base_name, step_name) formats =
699 val default_format = the (AList.lookup (op =) formats NONE)
700 fun do_const (x as (s, T)) =
701 (if String.isPrefix special_prefix s then
703 val do_term = map_aterms (fn Const x => fst (do_const x) | t' => t')
704 val (x' as (_, T'), js, ts) =
705 AList.find (op =) (!special_funs) (s, unarize_unbox_etc_type T)
707 val max_j = List.last js
708 val Ts = List.take (binder_types T', max_j + 1)
709 val missing_js = filter_out (member (op =) js) (0 upto max_j)
710 val missing_Ts = filter_indices missing_js Ts
711 fun nth_missing_var n =
712 ((arg_var_prefix ^ nat_subscript (n + 1), 0), nth missing_Ts n)
713 val missing_vars = map nth_missing_var (0 upto length missing_js - 1)
714 val vars = special_bounds ts @ missing_vars
717 case AList.lookup (op =) (js ~~ ts) j of
720 Var (nth missing_vars
721 (find_index (curry (op =) j) missing_js)))
723 val t = do_const x' |> fst
725 case AList.lookup (fn (SOME t1, SOME t2) => term_match thy (t1, t2)
726 | _ => false) formats (SOME t) of
728 repair_special_format js (num_binder_types T') format
730 const_format thy def_table x'
731 |> repair_special_format js (num_binder_types T')
732 |> intersect_formats default_format
734 (list_comb (t, ts') |> fold_rev abs_var vars,
735 format_type default_format format T)
737 else if String.isPrefix uncurry_prefix s then
739 val (ss, s') = unprefix uncurry_prefix s
740 |> strip_first_name_sep |>> space_explode "@"
742 if String.isPrefix step_prefix s' then
746 val k = the (Int.fromString (hd ss))
747 val j = the (Int.fromString (List.last ss))
748 val (before_Ts, (tuple_T, rest_T)) =
749 strip_n_binders j T ||> (strip_n_binders 1 #>> hd)
750 val T' = before_Ts ---> dest_n_tuple_type k tuple_T ---> rest_T
751 in do_const (s', T') end
753 else if String.isPrefix unrolled_prefix s then
754 let val t = Const (original_name s, range_type T) in
755 (lambda (Free (iter_var_prefix, nat_T)) t,
756 format_type default_format
757 (lookup_format thy def_table formats t) T)
759 else if String.isPrefix base_prefix s then
760 (Const (base_name, T --> T) $ Const (unprefix base_prefix s, T),
761 format_type default_format default_format T)
762 else if String.isPrefix step_prefix s then
763 (Const (step_name, T --> T) $ Const (unprefix step_prefix s, T),
764 format_type default_format default_format T)
765 else if String.isPrefix quot_normal_prefix s then
766 let val t = Const (nitpick_prefix ^ "normalize quotient type", T) in
767 (t, format_term_type thy def_table formats t)
769 else if String.isPrefix skolem_prefix s then
771 val ss = the (AList.lookup (op =) (!skolems) s)
772 val (Ts, Ts') = chop (length ss) (binder_types T)
773 val frees = map Free (ss ~~ Ts)
774 val s' = original_name s
776 (fold lambda frees (Const (s', Ts' ---> T)),
777 format_type default_format
778 (lookup_format thy def_table formats (Const x)) T)
780 else if String.isPrefix eval_prefix s then
782 val t = nth evals (the (Int.fromString (unprefix eval_prefix s)))
783 in (t, format_term_type thy def_table formats t) end
784 else if s = @{const_name undefined_fast_The} then
785 (Const (nitpick_prefix ^ "The fallback", T),
786 format_type default_format
787 (lookup_format thy def_table formats
788 (Const (@{const_name The}, (T --> bool_T) --> T))) T)
789 else if s = @{const_name undefined_fast_Eps} then
790 (Const (nitpick_prefix ^ "Eps fallback", T),
791 format_type default_format
792 (lookup_format thy def_table formats
793 (Const (@{const_name Eps}, (T --> bool_T) --> T))) T)
795 let val t = Const (original_name s, T) in
796 (t, format_term_type thy def_table formats t)
798 |>> map_types uniterize_unarize_unbox_etc_type
799 |>> shorten_names_in_term |>> Term.map_abs_vars shortest_name
802 fun assign_operator_for_const (s, T) =
803 if String.isPrefix ubfp_prefix s then
804 if is_fun_type T then "\<subseteq>" else "\<le>"
805 else if String.isPrefix lbfp_prefix s then
806 if is_fun_type T then "\<supseteq>" else "\<ge>"
807 else if original_name s <> s then
808 assign_operator_for_const (strip_first_name_sep s |> snd, T)
812 (** Model reconstruction **)
814 fun term_for_name pool scope sel_names rel_table bounds name =
815 let val T = type_of name in
816 tuple_list_for_name rel_table bounds name
817 |> reconstruct_term false pool (("", ""), ("", "")) scope sel_names
818 rel_table bounds T T (rep_of name)
821 fun unfold_outer_the_binders (t as Const (@{const_name The}, _)
822 $ Abs (s, T, Const (@{const_name "op ="}, _)
824 betapply (Abs (s, T, t'), t) |> unfold_outer_the_binders
825 | unfold_outer_the_binders t = t
826 fun bisimilar_values _ 0 _ = true
827 | bisimilar_values coTs max_depth (t1, t2) =
828 let val T = fastype_of t1 in
829 if exists_subtype (member (op =) coTs) T then
831 val ((head1, args1), (head2, args2)) =
832 pairself (strip_comb o unfold_outer_the_binders) (t1, t2)
833 val max_depth = max_depth - (if member (op =) coTs T then 1 else 0)
835 head1 = head2 andalso
836 forall (bisimilar_values coTs max_depth) (args1 ~~ args2)
842 fun reconstruct_hol_model {show_datatypes, show_consts}
843 ({hol_ctxt = {thy, ctxt, max_bisim_depth, boxes, stds, wfs, user_axioms,
844 debug, binary_ints, destroy_constrs, specialize,
845 star_linear_preds, fast_descrs, tac_timeout, evals,
846 case_names, def_table, nondef_table, user_nondefs,
847 simp_table, psimp_table, choice_spec_table, intro_table,
848 ground_thm_table, ersatz_table, skolems, special_funs,
849 unrolled_preds, wf_cache, constr_cache},
850 binarize, card_assigns, bits, bisim_depth, datatypes, ofs} : scope)
851 formats all_frees free_names sel_names nonsel_names rel_table bounds =
853 val pool = Unsynchronized.ref []
854 val (wacky_names as (_, base_step_names), ctxt) =
855 add_wacky_syntax ctxt
857 {thy = thy, ctxt = ctxt, max_bisim_depth = max_bisim_depth, boxes = boxes,
858 stds = stds, wfs = wfs, user_axioms = user_axioms, debug = debug,
859 binary_ints = binary_ints, destroy_constrs = destroy_constrs,
860 specialize = specialize, star_linear_preds = star_linear_preds,
861 fast_descrs = fast_descrs, tac_timeout = tac_timeout, evals = evals,
862 case_names = case_names, def_table = def_table,
863 nondef_table = nondef_table, user_nondefs = user_nondefs,
864 simp_table = simp_table, psimp_table = psimp_table,
865 choice_spec_table = choice_spec_table, intro_table = intro_table,
866 ground_thm_table = ground_thm_table, ersatz_table = ersatz_table,
867 skolems = skolems, special_funs = special_funs,
868 unrolled_preds = unrolled_preds, wf_cache = wf_cache,
869 constr_cache = constr_cache}
871 {hol_ctxt = hol_ctxt, binarize = binarize, card_assigns = card_assigns,
872 bits = bits, bisim_depth = bisim_depth, datatypes = datatypes, ofs = ofs}
873 fun term_for_rep unfold =
874 reconstruct_term unfold pool wacky_names scope sel_names rel_table bounds
875 fun nth_value_of_type card T n =
877 fun aux unfold = term_for_rep unfold T T (Atom (card, 0)) [[n]]
881 if String.isPrefix cyclic_const_prefix s then
882 HOLogic.mk_eq (t, aux true)
888 all_values_of_type pool wacky_names scope sel_names rel_table bounds
889 fun is_codatatype_wellformed (cos : dtype_spec list)
890 ({typ, card, ...} : dtype_spec) =
892 val ts = all_values card typ
893 val max_depth = Integer.sum (map #card cos)
895 forall (not o bisimilar_values (map #typ cos) max_depth)
896 (all_distinct_unordered_pairs_of ts)
898 fun pretty_for_assign name =
900 val (oper, (t1, T'), T) =
902 FreeName (s, T, _) =>
903 let val t = Free (s, uniterize_unarize_unbox_etc_type T) in
904 ("=", (t, format_term_type thy def_table formats t), T)
906 | ConstName (s, T, _) =>
907 (assign_operator_for_const (s, T),
908 user_friendly_const hol_ctxt base_step_names formats (s, T), T)
909 | _ => raise NUT ("Nitpick_Model.reconstruct_hol_model.\
910 \pretty_for_assign", [name])
911 val t2 = if rep_of name = Any then
912 Const (@{const_name undefined}, T')
914 tuple_list_for_name rel_table bounds name
915 |> term_for_rep false T T' (rep_of name)
917 Pretty.block (Pretty.breaks
918 [setmp_show_all_types (Syntax.pretty_term ctxt) t1,
919 Pretty.str oper, Syntax.pretty_term ctxt t2])
921 fun pretty_for_datatype ({typ, card, complete, ...} : dtype_spec) =
922 Pretty.block (Pretty.breaks
923 (Syntax.pretty_typ ctxt (uniterize_unarize_unbox_etc_type typ) ::
925 Type (@{type_name fin_fun}, _) => [Pretty.str "[finite]"]
926 | Type (@{type_name fun_box}, _) => [Pretty.str "[boxed]"]
927 | Type (@{type_name pair_box}, _) => [Pretty.str "[boxed]"]
930 Pretty.enum "," "{" "}"
931 (map (Syntax.pretty_term ctxt) (all_values card typ) @
932 (if fun_from_pair complete false then []
933 else [Pretty.str unrep]))]))
934 fun integer_datatype T =
935 [{typ = T, card = card_of_type card_assigns T, co = false,
936 standard = true, complete = (false, false), concrete = (true, true),
937 deep = true, constrs = []}]
938 handle TYPE ("Nitpick_HOL.card_of_type", _, _) => []
939 val (codatatypes, datatypes) =
940 datatypes |> filter #deep |> List.partition #co
941 ||> append (integer_datatype int_T
942 |> is_standard_datatype thy stds nat_T
943 ? append (integer_datatype nat_T))
944 val block_of_datatypes =
945 if show_datatypes andalso not (null datatypes) then
946 [Pretty.big_list ("Datatype" ^ plural_s_for_list datatypes ^ ":")
947 (map pretty_for_datatype datatypes)]
950 val block_of_codatatypes =
951 if show_datatypes andalso not (null codatatypes) then
952 [Pretty.big_list ("Codatatype" ^ plural_s_for_list codatatypes ^ ":")
953 (map pretty_for_datatype codatatypes)]
956 fun block_of_names show title names =
957 if show andalso not (null names) then
958 Pretty.str (title ^ plural_s_for_list names ^ ":")
959 :: map (Pretty.indent indent_size o pretty_for_assign)
960 (sort_wrt (original_name o nickname_of) names)
963 val (skolem_names, nonskolem_nonsel_names) =
964 List.partition is_skolem_name nonsel_names
965 val (eval_names, noneval_nonskolem_nonsel_names) =
966 List.partition (String.isPrefix eval_prefix o nickname_of)
967 nonskolem_nonsel_names
968 ||> filter_out (member (op =) [@{const_name bisim},
969 @{const_name bisim_iterator_max}]
972 map (fn x as (s, T) =>
973 case filter (curry (op =) x
975 (uniterize_unarize_unbox_etc_type o type_of))
978 | [] => FreeName (s, T, Any)
979 | _ => raise TERM ("Nitpick_Model.reconstruct_hol_model",
980 [Const x])) all_frees
981 val chunks = block_of_names true "Free variable" free_names @
982 block_of_names true "Skolem constant" skolem_names @
983 block_of_names true "Evaluated term" eval_names @
984 block_of_datatypes @ block_of_codatatypes @
985 block_of_names show_consts "Constant"
986 noneval_nonskolem_nonsel_names
988 (Pretty.chunks (if null chunks then [Pretty.str "Empty assignment"]
990 bisim_depth >= 0 orelse
991 forall (is_codatatype_wellformed codatatypes) codatatypes)
994 fun prove_hol_model (scope as {hol_ctxt = {thy, ctxt, debug, ...},
996 auto_timeout free_names sel_names rel_table bounds prop =
998 val pool = Unsynchronized.ref []
999 fun free_type_assm (T, k) =
1001 fun atom j = nth_atom pool true T j k
1002 fun equation_for_atom j = HOLogic.eq_const T $ Bound 0 $ atom j
1003 val eqs = map equation_for_atom (index_seq 0 k)
1005 Const (@{const_name All}, (T --> bool_T) --> bool_T)
1006 $ Abs ("x", T, foldl1 HOLogic.mk_disj eqs)
1007 val distinct_assm = distinctness_formula T (map atom (index_seq 0 k))
1008 in s_conj (compreh_assm, distinct_assm) end
1009 fun free_name_assm name =
1010 HOLogic.mk_eq (Free (nickname_of name, type_of name),
1011 term_for_name pool scope sel_names rel_table bounds name)
1012 val freeT_assms = map free_type_assm (filter (is_TFree o fst) card_assigns)
1013 val model_assms = map free_name_assm free_names
1014 val assm = foldr1 s_conj (freeT_assms @ model_assms)
1015 fun try_out negate =
1017 val concl = (negate ? curry (op $) @{const Not})
1018 (Object_Logic.atomize_term thy prop)
1019 val prop = HOLogic.mk_Trueprop (HOLogic.mk_imp (assm, concl))
1020 |> map_types (map_type_tfree
1021 (fn (s, []) => TFree (s, HOLogic.typeS)
1023 val _ = if debug then
1024 priority ((if negate then "Genuineness" else "Spuriousness") ^
1025 " goal: " ^ Syntax.string_of_term ctxt prop ^ ".")
1028 val goal = prop |> cterm_of thy |> Goal.init
1030 (goal |> SINGLE (DETERM_TIMEOUT auto_timeout
1031 (auto_tac (clasimpset_of ctxt)))
1032 |> the |> Goal.finish ctxt; true)
1033 handle THM _ => false
1034 | TimeLimit.TimeOut => false
1037 if try_out false then SOME true
1038 else if try_out true then SOME false