equal
deleted
inserted
replaced
303 preprocess_formulas hol_ctxt nondef_assm_ts neg_t |
303 preprocess_formulas hol_ctxt nondef_assm_ts neg_t |
304 val got_all_user_axioms = |
304 val got_all_user_axioms = |
305 got_all_mono_user_axioms andalso no_poly_user_axioms |
305 got_all_mono_user_axioms andalso no_poly_user_axioms |
306 |
306 |
307 fun print_wf (x, (gfp, wf)) = |
307 fun print_wf (x, (gfp, wf)) = |
308 pprint_nt (fn () => Pretty.blk (0, |
308 pprint_nt (fn () => Pretty.block0 |
309 Pretty.text ("The " ^ (if gfp then "co" else "") ^ "inductive predicate") @ |
309 (Pretty.text ("The " ^ (if gfp then "co" else "") ^ "inductive predicate") @ |
310 [Pretty.brk 1, Pretty.quote (Syntax.pretty_term ctxt (Const x)), Pretty.brk 1] @ |
310 [Pretty.brk 1, Pretty.quote (Syntax.pretty_term ctxt (Const x)), Pretty.brk 1] @ |
311 Pretty.text (if wf then |
311 Pretty.text (if wf then |
312 "was proved well-founded; Nitpick can compute it \ |
312 "was proved well-founded; Nitpick can compute it \ |
313 \efficiently" |
313 \efficiently" |
314 else |
314 else |
340 *) |
340 *) |
341 |
341 |
342 val unique_scope = forall (curry (op =) 1 o length o snd) cards_assigns |
342 val unique_scope = forall (curry (op =) 1 o length o snd) cards_assigns |
343 fun monotonicity_message Ts extra = |
343 fun monotonicity_message Ts extra = |
344 let val pretties = map (pretty_maybe_quote ctxt o pretty_for_type ctxt) Ts in |
344 let val pretties = map (pretty_maybe_quote ctxt o pretty_for_type ctxt) Ts in |
345 Pretty.blk (0, |
345 Pretty.block0 |
346 Pretty.text ("The type" ^ plural_s_for_list pretties) @ [Pretty.brk 1] @ |
346 (Pretty.text ("The type" ^ plural_s_for_list pretties) @ [Pretty.brk 1] @ |
347 pretty_serial_commas "and" pretties @ [Pretty.brk 1] @ |
347 pretty_serial_commas "and" pretties @ [Pretty.brk 1] @ |
348 Pretty.text ( |
348 Pretty.text ( |
349 (if none_true monos then |
349 (if none_true monos then |
350 "passed the monotonicity test" |
350 "passed the monotonicity test" |
351 else |
351 else |
629 got_all_user_axioms andalso none_true wfs andalso |
629 got_all_user_axioms andalso none_true wfs andalso |
630 sound_finitizes andalso total_consts <> SOME true andalso |
630 sound_finitizes andalso total_consts <> SOME true andalso |
631 codatatypes_ok |
631 codatatypes_ok |
632 in |
632 in |
633 (pprint_a (Pretty.chunks |
633 (pprint_a (Pretty.chunks |
634 [Pretty.blk (0, |
634 [Pretty.block0 |
635 (Pretty.text ((if mode = Auto_Try then "Auto " else "") ^ |
635 ((Pretty.text ((if mode = Auto_Try then "Auto " else "") ^ |
636 "Nitpick found a" ^ |
636 "Nitpick found a" ^ |
637 (if not genuine then " potentially spurious " |
637 (if not genuine then " potentially spurious " |
638 else if genuine_means_genuine then " " |
638 else if genuine_means_genuine then " " |
639 else " quasi genuine ") ^ das_wort_model) @ |
639 else " quasi genuine ") ^ das_wort_model) @ |
640 (case pretties_for_scope scope verbose of |
640 (case pretties_for_scope scope verbose of |
789 val _ = |
789 val _ = |
790 if null scopes then |
790 if null scopes then |
791 print_nt (K "The scope specification is inconsistent") |
791 print_nt (K "The scope specification is inconsistent") |
792 else if verbose then |
792 else if verbose then |
793 pprint_nt (fn () => Pretty.chunks |
793 pprint_nt (fn () => Pretty.chunks |
794 [Pretty.blk (0, |
794 [Pretty.block0 |
795 Pretty.text ((if n > 1 then |
795 (Pretty.text ((if n > 1 then |
796 "Batch " ^ string_of_int (j + 1) ^ " of " ^ |
796 "Batch " ^ string_of_int (j + 1) ^ " of " ^ |
797 signed_string_of_int n ^ ": " |
797 signed_string_of_int n ^ ": " |
798 else |
798 else |
799 "") ^ |
799 "") ^ |
800 "Trying " ^ string_of_int (length scopes) ^ |
800 "Trying " ^ string_of_int (length scopes) ^ |