69 if for_auto then |
69 if for_auto then |
70 Free (atom_name (hd (space_explode "." nitpick_prefix)) T j, T) |
70 Free (atom_name (hd (space_explode "." nitpick_prefix)) T j, T) |
71 else |
71 else |
72 Const (atom_name "" T j, T) |
72 Const (atom_name "" T j, T) |
73 |
73 |
|
74 (* term * term -> order *) |
|
75 fun nice_term_ord (Abs (_, _, t1), Abs (_, _, t2)) = nice_term_ord (t1, t2) |
|
76 | nice_term_ord (t1, t2) = |
|
77 int_ord (snd (HOLogic.dest_number t1), snd (HOLogic.dest_number t2)) |
|
78 handle TERM ("dest_number", _) => |
|
79 case (t1, t2) of |
|
80 (t11 $ t12, t21 $ t22) => |
|
81 (case nice_term_ord (t11, t21) of |
|
82 EQUAL => nice_term_ord (t12, t22) |
|
83 | ord => ord) |
|
84 | _ => TermOrd.term_ord (t1, t2) |
|
85 |
74 (* nut NameTable.table -> Kodkod.raw_bound list -> nut -> int list list *) |
86 (* nut NameTable.table -> Kodkod.raw_bound list -> nut -> int list list *) |
75 fun tuple_list_for_name rel_table bounds name = |
87 fun tuple_list_for_name rel_table bounds name = |
76 the (AList.lookup (op =) bounds (the_rel rel_table name)) handle NUT _ => [[]] |
88 the (AList.lookup (op =) bounds (the_rel rel_table name)) handle NUT _ => [[]] |
77 |
89 |
78 (* term -> term *) |
90 (* term -> term *) |
79 fun unbox_term (Const (@{const_name FunBox}, _) $ t1) = unbox_term t1 |
91 fun unbit_and_unbox_term (Const (@{const_name FunBox}, _) $ t1) = |
80 | unbox_term (Const (@{const_name PairBox}, |
92 unbit_and_unbox_term t1 |
81 Type ("fun", [T1, Type ("fun", [T2, T3])])) $ t1 $ t2) = |
93 | unbit_and_unbox_term (Const (@{const_name PairBox}, |
82 let val Ts = map unbox_type [T1, T2] in |
94 Type ("fun", [T1, Type ("fun", [T2, T3])])) |
|
95 $ t1 $ t2) = |
|
96 let val Ts = map unbit_and_unbox_type [T1, T2] in |
83 Const (@{const_name Pair}, Ts ---> Type ("*", Ts)) |
97 Const (@{const_name Pair}, Ts ---> Type ("*", Ts)) |
84 $ unbox_term t1 $ unbox_term t2 |
98 $ unbit_and_unbox_term t1 $ unbit_and_unbox_term t2 |
85 end |
99 end |
86 | unbox_term (Const (s, T)) = Const (s, unbox_type T) |
100 | unbit_and_unbox_term (Const (s, T)) = Const (s, unbit_and_unbox_type T) |
87 | unbox_term (t1 $ t2) = unbox_term t1 $ unbox_term t2 |
101 | unbit_and_unbox_term (t1 $ t2) = |
88 | unbox_term (Free (s, T)) = Free (s, unbox_type T) |
102 unbit_and_unbox_term t1 $ unbit_and_unbox_term t2 |
89 | unbox_term (Var (x, T)) = Var (x, unbox_type T) |
103 | unbit_and_unbox_term (Free (s, T)) = Free (s, unbit_and_unbox_type T) |
90 | unbox_term (Bound j) = Bound j |
104 | unbit_and_unbox_term (Var (x, T)) = Var (x, unbit_and_unbox_type T) |
91 | unbox_term (Abs (s, T, t')) = Abs (s, unbox_type T, unbox_term t') |
105 | unbit_and_unbox_term (Bound j) = Bound j |
|
106 | unbit_and_unbox_term (Abs (s, T, t')) = |
|
107 Abs (s, unbit_and_unbox_type T, unbit_and_unbox_term t') |
92 |
108 |
93 (* typ -> typ -> (typ * typ) * (typ * typ) *) |
109 (* typ -> typ -> (typ * typ) * (typ * typ) *) |
94 fun factor_out_types (T1 as Type ("*", [T11, T12])) |
110 fun factor_out_types (T1 as Type ("*", [T11, T12])) |
95 (T2 as Type ("*", [T21, T22])) = |
111 (T2 as Type ("*", [T21, T22])) = |
96 let val (n1, n2) = pairself num_factors_in_type (T11, T21) in |
112 let val (n1, n2) = pairself num_factors_in_type (T11, T21) in |
219 (* typ -> term list -> term *) |
235 (* typ -> term list -> term *) |
220 fun mk_tuple (Type ("*", [T1, T2])) ts = |
236 fun mk_tuple (Type ("*", [T1, T2])) ts = |
221 HOLogic.mk_prod (mk_tuple T1 ts, |
237 HOLogic.mk_prod (mk_tuple T1 ts, |
222 mk_tuple T2 (List.drop (ts, length (HOLogic.flatten_tupleT T1)))) |
238 mk_tuple T2 (List.drop (ts, length (HOLogic.flatten_tupleT T1)))) |
223 | mk_tuple _ (t :: _) = t |
239 | mk_tuple _ (t :: _) = t |
|
240 | mk_tuple T [] = raise TYPE ("Nitpick_Model.mk_tuple", [T], []) |
224 |
241 |
225 (* string * string * string * string -> scope -> nut list -> nut list |
242 (* string * string * string * string -> scope -> nut list -> nut list |
226 -> nut list -> nut NameTable.table -> Kodkod.raw_bound list -> typ -> typ |
243 -> nut list -> nut NameTable.table -> Kodkod.raw_bound list -> typ -> typ |
227 -> rep -> int list list -> term *) |
244 -> rep -> int list list -> term *) |
228 fun reconstruct_term (maybe_name, base_name, step_name, abs_name) |
245 fun reconstruct_term (maybe_name, base_name, step_name, abs_name) |
229 ({ext_ctxt as {thy, ctxt, ...}, card_assigns, datatypes, ofs, ...} |
246 ({ext_ctxt as {thy, ctxt, ...}, card_assigns, bits, datatypes, ofs, ...} |
230 : scope) sel_names rel_table bounds = |
247 : scope) sel_names rel_table bounds = |
231 let |
248 let |
232 val for_auto = (maybe_name = "") |
249 val for_auto = (maybe_name = "") |
|
250 (* int list list -> int *) |
|
251 fun value_of_bits jss = |
|
252 let |
|
253 val j0 = offset_of_type ofs @{typ unsigned_bit} |
|
254 val js = map (Integer.add (~ j0) o the_single) jss |
|
255 in |
|
256 fold (fn j => Integer.add (reasonable_power 2 j |> j = bits ? op ~)) |
|
257 js 0 |
|
258 end |
233 (* bool -> typ -> typ -> (term * term) list -> term *) |
259 (* bool -> typ -> typ -> (term * term) list -> term *) |
234 fun make_set maybe_opt T1 T2 = |
260 fun make_set maybe_opt T1 T2 = |
235 let |
261 let |
236 val empty_const = Const (@{const_name Set.empty}, T1 --> T2) |
262 val empty_const = Const (@{const_name Set.empty}, T1 --> T2) |
237 val insert_const = Const (@{const_name insert}, |
263 val insert_const = Const (@{const_name insert}, |
238 [T1, T1 --> T2] ---> T1 --> T2) |
264 T1 --> (T1 --> T2) --> T1 --> T2) |
239 (* (term * term) list -> term *) |
265 (* (term * term) list -> term *) |
240 fun aux [] = |
266 fun aux [] = |
241 if maybe_opt andalso not (is_complete_type datatypes T1) then |
267 if maybe_opt andalso not (is_complete_type datatypes T1) then |
242 insert_const $ Const (unrep, T1) $ empty_const |
268 insert_const $ Const (unrep, T1) $ empty_const |
243 else |
269 else |
531 |
564 |
532 (* params -> scope -> (term option * int list) list -> styp list -> nut list |
565 (* params -> scope -> (term option * int list) list -> styp list -> nut list |
533 -> nut list -> nut list -> nut NameTable.table -> Kodkod.raw_bound list |
566 -> nut list -> nut list -> nut NameTable.table -> Kodkod.raw_bound list |
534 -> Pretty.T * bool *) |
567 -> Pretty.T * bool *) |
535 fun reconstruct_hol_model {show_skolems, show_datatypes, show_consts} |
568 fun reconstruct_hol_model {show_skolems, show_datatypes, show_consts} |
536 ({ext_ctxt as {thy, ctxt, max_bisim_depth, boxes, user_axioms, debug, |
569 ({ext_ctxt as {thy, ctxt, max_bisim_depth, boxes, wfs, user_axioms, |
537 wfs, destroy_constrs, specialize, skolemize, |
570 debug, binary_ints, destroy_constrs, specialize, |
538 star_linear_preds, uncurry, fast_descrs, tac_timeout, |
571 skolemize, star_linear_preds, uncurry, fast_descrs, |
539 evals, case_names, def_table, nondef_table, user_nondefs, |
572 tac_timeout, evals, case_names, def_table, nondef_table, |
540 simp_table, psimp_table, intro_table, ground_thm_table, |
573 user_nondefs, simp_table, psimp_table, intro_table, |
541 ersatz_table, skolems, special_funs, unrolled_preds, |
574 ground_thm_table, ersatz_table, skolems, special_funs, |
542 wf_cache, constr_cache}, |
575 unrolled_preds, wf_cache, constr_cache}, |
543 card_assigns, bisim_depth, datatypes, ofs} : scope) formats all_frees |
576 card_assigns, bits, bisim_depth, datatypes, ofs} : scope) |
544 free_names sel_names nonsel_names rel_table bounds = |
577 formats all_frees free_names sel_names nonsel_names rel_table bounds = |
545 let |
578 let |
546 val (wacky_names as (_, base_name, step_name, _), ctxt) = |
579 val (wacky_names as (_, base_name, step_name, _), ctxt) = |
547 add_wacky_syntax ctxt |
580 add_wacky_syntax ctxt |
548 val ext_ctxt = |
581 val ext_ctxt = |
549 {thy = thy, ctxt = ctxt, max_bisim_depth = max_bisim_depth, boxes = boxes, |
582 {thy = thy, ctxt = ctxt, max_bisim_depth = max_bisim_depth, boxes = boxes, |
550 wfs = wfs, user_axioms = user_axioms, debug = debug, |
583 wfs = wfs, user_axioms = user_axioms, debug = debug, |
551 destroy_constrs = destroy_constrs, specialize = specialize, |
584 binary_ints = binary_ints, destroy_constrs = destroy_constrs, |
552 skolemize = skolemize, star_linear_preds = star_linear_preds, |
585 specialize = specialize, skolemize = skolemize, |
553 uncurry = uncurry, fast_descrs = fast_descrs, tac_timeout = tac_timeout, |
586 star_linear_preds = star_linear_preds, uncurry = uncurry, |
554 evals = evals, case_names = case_names, def_table = def_table, |
587 fast_descrs = fast_descrs, tac_timeout = tac_timeout, evals = evals, |
|
588 case_names = case_names, def_table = def_table, |
555 nondef_table = nondef_table, user_nondefs = user_nondefs, |
589 nondef_table = nondef_table, user_nondefs = user_nondefs, |
556 simp_table = simp_table, psimp_table = psimp_table, |
590 simp_table = simp_table, psimp_table = psimp_table, |
557 intro_table = intro_table, ground_thm_table = ground_thm_table, |
591 intro_table = intro_table, ground_thm_table = ground_thm_table, |
558 ersatz_table = ersatz_table, skolems = skolems, |
592 ersatz_table = ersatz_table, skolems = skolems, |
559 special_funs = special_funs, unrolled_preds = unrolled_preds, |
593 special_funs = special_funs, unrolled_preds = unrolled_preds, |
560 wf_cache = wf_cache, constr_cache = constr_cache} |
594 wf_cache = wf_cache, constr_cache = constr_cache} |
561 val scope = {ext_ctxt = ext_ctxt, card_assigns = card_assigns, |
595 val scope = {ext_ctxt = ext_ctxt, card_assigns = card_assigns, |
562 bisim_depth = bisim_depth, datatypes = datatypes, ofs = ofs} |
596 bits = bits, bisim_depth = bisim_depth, datatypes = datatypes, |
|
597 ofs = ofs} |
563 (* typ -> typ -> rep -> int list list -> term *) |
598 (* typ -> typ -> rep -> int list list -> term *) |
564 val term_for_rep = reconstruct_term wacky_names scope sel_names rel_table |
599 val term_for_rep = reconstruct_term wacky_names scope sel_names rel_table |
565 bounds |
600 bounds |
566 (* typ -> typ -> typ *) |
601 (* nat -> typ -> nat -> typ *) |
567 fun nth_value_of_type T card n = term_for_rep T T (Atom (card, 0)) [[n]] |
602 fun nth_value_of_type card T n = term_for_rep T T (Atom (card, 0)) [[n]] |
|
603 (* nat -> typ -> typ list *) |
|
604 fun all_values_of_type card T = |
|
605 index_seq 0 card |> map (nth_value_of_type card T) |> sort nice_term_ord |
568 (* dtype_spec list -> dtype_spec -> bool *) |
606 (* dtype_spec list -> dtype_spec -> bool *) |
569 fun is_codatatype_wellformed (cos : dtype_spec list) |
607 fun is_codatatype_wellformed (cos : dtype_spec list) |
570 ({typ, card, ...} : dtype_spec) = |
608 ({typ, card, ...} : dtype_spec) = |
571 let |
609 let |
572 val ts = map (nth_value_of_type typ card) (index_seq 0 card) |
610 val ts = all_values_of_type card typ |
573 val max_depth = Integer.sum (map #card cos) |
611 val max_depth = Integer.sum (map #card cos) |
574 in |
612 in |
575 forall (not o bisimilar_values (map #typ cos) max_depth) |
613 forall (not o bisimilar_values (map #typ cos) max_depth) |
576 (all_distinct_unordered_pairs_of ts) |
614 (all_distinct_unordered_pairs_of ts) |
577 end |
615 end |
601 Pretty.str oper, Syntax.pretty_term ctxt t2]) |
639 Pretty.str oper, Syntax.pretty_term ctxt t2]) |
602 end |
640 end |
603 (* dtype_spec -> Pretty.T *) |
641 (* dtype_spec -> Pretty.T *) |
604 fun pretty_for_datatype ({typ, card, complete, ...} : dtype_spec) = |
642 fun pretty_for_datatype ({typ, card, complete, ...} : dtype_spec) = |
605 Pretty.block (Pretty.breaks |
643 Pretty.block (Pretty.breaks |
606 [Syntax.pretty_typ ctxt (unbox_type typ), Pretty.str "=", |
644 [Syntax.pretty_typ ctxt (unbit_and_unbox_type typ), Pretty.str "=", |
607 Pretty.enum "," "{" "}" |
645 Pretty.enum "," "{" "}" |
608 (map (Syntax.pretty_term ctxt o nth_value_of_type typ card) |
646 (map (Syntax.pretty_term ctxt) (all_values_of_type card typ) |
609 (index_seq 0 card) @ |
647 @ (if complete then [] else [Pretty.str unrep]))]) |
610 (if complete then [] else [Pretty.str unrep]))]) |
|
611 (* typ -> dtype_spec list *) |
648 (* typ -> dtype_spec list *) |
612 fun integer_datatype T = |
649 fun integer_datatype T = |
613 [{typ = T, card = card_of_type card_assigns T, co = false, |
650 [{typ = T, card = card_of_type card_assigns T, co = false, |
614 complete = false, concrete = true, shallow = false, constrs = []}] |
651 complete = false, concrete = true, shallow = false, constrs = []}] |
615 handle TYPE ("Nitpick_HOL.card_of_type", _, _) => [] |
652 handle TYPE ("Nitpick_HOL.card_of_type", _, _) => [] |