src/HOL/Tools/Nitpick/nitpick.ML
author blanchet
Tue, 13 Apr 2010 11:43:11 +0200
changeset 36126 00d550b6cfd4
parent 35968 b7f98ff9c7d9
child 36128 a3d8d5329438
permissions -rw-r--r--
cosmetics
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
33982
1ae222745c4a fixed paths in Nitpick's ML file headers
blanchet
parents: 33955
diff changeset
     1
(*  Title:      HOL/Tools/Nitpick/nitpick.ML
33192
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
     2
    Author:     Jasmin Blanchette, TU Muenchen
34982
7b8c366e34a2 added support for nonstandard models to Nitpick (based on an idea by Koen Claessen) and did other fixes to Nitpick
blanchet
parents: 34938
diff changeset
     3
    Copyright   2008, 2009, 2010
33192
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
     4
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
     5
Finite model generation for HOL formulas using Kodkod.
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
     6
*)
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
     7
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
     8
signature NITPICK =
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
     9
sig
33705
947184dc75c9 removed a few global names in Nitpick (styp, nat_less, pairf)
blanchet
parents: 33580
diff changeset
    10
  type styp = Nitpick_Util.styp
35711
548d3f16404b added term postprocessor to Nitpick, to provide custom syntax for typedefs
blanchet
parents: 35696
diff changeset
    11
  type term_postprocessor = Nitpick_Model.term_postprocessor
33192
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
    12
  type params = {
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
    13
    cards_assigns: (typ option * int list) list,
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
    14
    maxes_assigns: (styp option * int list) list,
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
    15
    iters_assigns: (styp option * int list) list,
34124
c4628a1dcf75 added support for binary nat/int representation to Nitpick
blanchet
parents: 34123
diff changeset
    16
    bitss: int list,
33192
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
    17
    bisim_depths: int list,
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
    18
    boxes: (typ option * bool option) list,
35665
ff2bf50505ab added "finitize" option to Nitpick + remove dependency on "Coinductive_List"
blanchet
parents: 35408
diff changeset
    19
    finitizes: (typ option * bool option) list,
33192
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
    20
    monos: (typ option * bool option) list,
34982
7b8c366e34a2 added support for nonstandard models to Nitpick (based on an idea by Koen Claessen) and did other fixes to Nitpick
blanchet
parents: 34938
diff changeset
    21
    stds: (typ option * bool) list,
33192
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
    22
    wfs: (styp option * bool option) list,
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
    23
    sat_solver: string,
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
    24
    blocking: bool,
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
    25
    falsify: bool,
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
    26
    debug: bool,
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
    27
    verbose: bool,
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
    28
    overlord: bool,
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
    29
    user_axioms: bool option,
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
    30
    assms: bool,
33556
cba22e2999d5 renamed Nitpick option "coalesce_type_vars" to "merge_type_vars" (shorter) and cleaned up old hacks that are no longer necessary
blanchet
parents: 33233
diff changeset
    31
    merge_type_vars: bool,
34124
c4628a1dcf75 added support for binary nat/int representation to Nitpick
blanchet
parents: 34123
diff changeset
    32
    binary_ints: bool option,
33192
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
    33
    destroy_constrs: bool,
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
    34
    specialize: bool,
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
    35
    skolemize: bool,
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
    36
    star_linear_preds: bool,
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
    37
    uncurry: bool,
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
    38
    fast_descrs: bool,
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
    39
    peephole_optim: bool,
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
    40
    timeout: Time.time option,
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
    41
    tac_timeout: Time.time option,
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
    42
    sym_break: int,
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
    43
    sharing_depth: int,
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
    44
    flatten_props: bool,
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
    45
    max_threads: int,
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
    46
    show_skolems: bool,
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
    47
    show_datatypes: bool,
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
    48
    show_consts: bool,
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
    49
    evals: term list,
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
    50
    formats: (term option * int list) list,
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
    51
    max_potential: int,
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
    52
    max_genuine: int,
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
    53
    check_potential: bool,
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
    54
    check_genuine: bool,
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
    55
    batch_size: int,
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
    56
    expect: string}
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
    57
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
    58
  val register_frac_type : string -> (string * string) list -> theory -> theory
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
    59
  val unregister_frac_type : string -> theory -> theory
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
    60
  val register_codatatype : typ -> string -> styp list -> theory -> theory
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
    61
  val unregister_codatatype : typ -> theory -> theory
35711
548d3f16404b added term postprocessor to Nitpick, to provide custom syntax for typedefs
blanchet
parents: 35696
diff changeset
    62
  val register_term_postprocessor :
548d3f16404b added term postprocessor to Nitpick, to provide custom syntax for typedefs
blanchet
parents: 35696
diff changeset
    63
    typ -> term_postprocessor -> theory -> theory
548d3f16404b added term postprocessor to Nitpick, to provide custom syntax for typedefs
blanchet
parents: 35696
diff changeset
    64
  val unregister_term_postprocessor : typ -> theory -> theory
33192
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
    65
  val pick_nits_in_term :
35335
f715cfde056a support local definitions in Nitpick
blanchet
parents: 35334
diff changeset
    66
    Proof.state -> params -> bool -> int -> int -> int -> (term * term) list
f715cfde056a support local definitions in Nitpick
blanchet
parents: 35334
diff changeset
    67
    -> term list -> term -> string * Proof.state
33192
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
    68
  val pick_nits_in_subgoal :
34982
7b8c366e34a2 added support for nonstandard models to Nitpick (based on an idea by Koen Claessen) and did other fixes to Nitpick
blanchet
parents: 34938
diff changeset
    69
    Proof.state -> params -> bool -> int -> int -> string * Proof.state
33192
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
    70
end;
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
    71
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
    72
structure Nitpick : NITPICK =
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
    73
struct
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
    74
33232
f93390060bbe internal renaming in Nitpick and fixed Kodkodi invokation on Linux;
blanchet
parents: 33192
diff changeset
    75
open Nitpick_Util
f93390060bbe internal renaming in Nitpick and fixed Kodkodi invokation on Linux;
blanchet
parents: 33192
diff changeset
    76
open Nitpick_HOL
35070
96136eb6218f split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents: 34998
diff changeset
    77
open Nitpick_Preproc
33232
f93390060bbe internal renaming in Nitpick and fixed Kodkodi invokation on Linux;
blanchet
parents: 33192
diff changeset
    78
open Nitpick_Mono
f93390060bbe internal renaming in Nitpick and fixed Kodkodi invokation on Linux;
blanchet
parents: 33192
diff changeset
    79
open Nitpick_Scope
f93390060bbe internal renaming in Nitpick and fixed Kodkodi invokation on Linux;
blanchet
parents: 33192
diff changeset
    80
open Nitpick_Peephole
f93390060bbe internal renaming in Nitpick and fixed Kodkodi invokation on Linux;
blanchet
parents: 33192
diff changeset
    81
open Nitpick_Rep
f93390060bbe internal renaming in Nitpick and fixed Kodkodi invokation on Linux;
blanchet
parents: 33192
diff changeset
    82
open Nitpick_Nut
f93390060bbe internal renaming in Nitpick and fixed Kodkodi invokation on Linux;
blanchet
parents: 33192
diff changeset
    83
open Nitpick_Kodkod
f93390060bbe internal renaming in Nitpick and fixed Kodkodi invokation on Linux;
blanchet
parents: 33192
diff changeset
    84
open Nitpick_Model
33192
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
    85
34126
8a2c5d7aff51 polished Nitpick's binary integer support etc.;
blanchet
parents: 34124
diff changeset
    86
structure KK = Kodkod
8a2c5d7aff51 polished Nitpick's binary integer support etc.;
blanchet
parents: 34124
diff changeset
    87
33192
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
    88
type params = {
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
    89
  cards_assigns: (typ option * int list) list,
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
    90
  maxes_assigns: (styp option * int list) list,
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
    91
  iters_assigns: (styp option * int list) list,
34124
c4628a1dcf75 added support for binary nat/int representation to Nitpick
blanchet
parents: 34123
diff changeset
    92
  bitss: int list,
33192
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
    93
  bisim_depths: int list,
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
    94
  boxes: (typ option * bool option) list,
35665
ff2bf50505ab added "finitize" option to Nitpick + remove dependency on "Coinductive_List"
blanchet
parents: 35408
diff changeset
    95
  finitizes: (typ option * bool option) list,
33192
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
    96
  monos: (typ option * bool option) list,
34982
7b8c366e34a2 added support for nonstandard models to Nitpick (based on an idea by Koen Claessen) and did other fixes to Nitpick
blanchet
parents: 34938
diff changeset
    97
  stds: (typ option * bool) list,
33192
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
    98
  wfs: (styp option * bool option) list,
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
    99
  sat_solver: string,
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   100
  blocking: bool,
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   101
  falsify: bool,
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   102
  debug: bool,
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   103
  verbose: bool,
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   104
  overlord: bool,
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   105
  user_axioms: bool option,
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   106
  assms: bool,
33556
cba22e2999d5 renamed Nitpick option "coalesce_type_vars" to "merge_type_vars" (shorter) and cleaned up old hacks that are no longer necessary
blanchet
parents: 33233
diff changeset
   107
  merge_type_vars: bool,
34124
c4628a1dcf75 added support for binary nat/int representation to Nitpick
blanchet
parents: 34123
diff changeset
   108
  binary_ints: bool option,
33192
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   109
  destroy_constrs: bool,
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   110
  specialize: bool,
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   111
  skolemize: bool,
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   112
  star_linear_preds: bool,
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   113
  uncurry: bool,
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   114
  fast_descrs: bool,
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   115
  peephole_optim: bool,
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   116
  timeout: Time.time option,
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   117
  tac_timeout: Time.time option,
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   118
  sym_break: int,
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   119
  sharing_depth: int,
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   120
  flatten_props: bool,
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   121
  max_threads: int,
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   122
  show_skolems: bool,
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   123
  show_datatypes: bool,
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   124
  show_consts: bool,
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   125
  evals: term list,
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   126
  formats: (term option * int list) list,
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   127
  max_potential: int,
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   128
  max_genuine: int,
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   129
  check_potential: bool,
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   130
  check_genuine: bool,
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   131
  batch_size: int,
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   132
  expect: string}
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   133
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   134
type problem_extension = {
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   135
  free_names: nut list,
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   136
  sel_names: nut list,
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   137
  nonsel_names: nut list,
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   138
  rel_table: nut NameTable.table,
35185
9b8f351cced6 added yet another hint to Nitpick's output, this time warning about problems for which nothing was effectively tested
blanchet
parents: 35183
diff changeset
   139
  unsound: bool,
35386
45a4e19d3ebd more work on the new monotonicity stuff in Nitpick
blanchet
parents: 35385
diff changeset
   140
  scope: scope}
33192
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   141
34126
8a2c5d7aff51 polished Nitpick's binary integer support etc.;
blanchet
parents: 34124
diff changeset
   142
type rich_problem = KK.problem * problem_extension
33192
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   143
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   144
(* Proof.context -> string -> term list -> Pretty.T list *)
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   145
fun pretties_for_formulas _ _ [] = []
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   146
  | pretties_for_formulas ctxt s ts =
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   147
    [Pretty.str (s ^ plural_s_for_list ts ^ ":"),
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   148
     Pretty.indent indent_size (Pretty.chunks
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   149
         (map2 (fn j => fn t =>
34121
5e831d805118 get rid of polymorphic equality in Nitpick's code + a few minor cleanups
blanchet
parents: 34039
diff changeset
   150
                   Pretty.block [t |> shorten_names_in_term
33192
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   151
                                   |> Syntax.pretty_term ctxt,
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   152
                                 Pretty.str (if j = 1 then "." else ";")])
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   153
               (length ts downto 1) ts))]
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   154
33568
532b915afa14 don't run Nitpick at all if Kodkodi is not installed (as indicated by the $KODKODI variable)
blanchet
parents: 33566
diff changeset
   155
(* unit -> string *)
35696
17ae461d6133 show nice error message in Nitpick when "java" is not available
blanchet
parents: 35671
diff changeset
   156
fun install_java_message () =
17ae461d6133 show nice error message in Nitpick when "java" is not available
blanchet
parents: 35671
diff changeset
   157
  "Nitpick requires a Java 1.5 virtual machine called \"java\"."
17ae461d6133 show nice error message in Nitpick when "java" is not available
blanchet
parents: 35671
diff changeset
   158
(* unit -> string *)
33568
532b915afa14 don't run Nitpick at all if Kodkodi is not installed (as indicated by the $KODKODI variable)
blanchet
parents: 33566
diff changeset
   159
fun install_kodkodi_message () =
532b915afa14 don't run Nitpick at all if Kodkodi is not installed (as indicated by the $KODKODI variable)
blanchet
parents: 33566
diff changeset
   160
  "Nitpick requires the external Java program Kodkodi. To install it, download \
532b915afa14 don't run Nitpick at all if Kodkodi is not installed (as indicated by the $KODKODI variable)
blanchet
parents: 33566
diff changeset
   161
  \the package from Isabelle's web page and add the \"kodkodi-x.y.z\" \
532b915afa14 don't run Nitpick at all if Kodkodi is not installed (as indicated by the $KODKODI variable)
blanchet
parents: 33566
diff changeset
   162
  \directory's full path to \"" ^
532b915afa14 don't run Nitpick at all if Kodkodi is not installed (as indicated by the $KODKODI variable)
blanchet
parents: 33566
diff changeset
   163
  Path.implode (Path.expand (Path.appends
532b915afa14 don't run Nitpick at all if Kodkodi is not installed (as indicated by the $KODKODI variable)
blanchet
parents: 33566
diff changeset
   164
      (Path.variable "ISABELLE_HOME_USER" ::
532b915afa14 don't run Nitpick at all if Kodkodi is not installed (as indicated by the $KODKODI variable)
blanchet
parents: 33566
diff changeset
   165
       map Path.basic ["etc", "components"]))) ^ "\"."
532b915afa14 don't run Nitpick at all if Kodkodi is not installed (as indicated by the $KODKODI variable)
blanchet
parents: 33566
diff changeset
   166
35185
9b8f351cced6 added yet another hint to Nitpick's output, this time warning about problems for which nothing was effectively tested
blanchet
parents: 35183
diff changeset
   167
val max_unsound_delay_ms = 200
9b8f351cced6 added yet another hint to Nitpick's output, this time warning about problems for which nothing was effectively tested
blanchet
parents: 35183
diff changeset
   168
val max_unsound_delay_percent = 2
33192
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   169
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   170
(* Time.time option -> int *)
35185
9b8f351cced6 added yet another hint to Nitpick's output, this time warning about problems for which nothing was effectively tested
blanchet
parents: 35183
diff changeset
   171
fun unsound_delay_for_timeout NONE = max_unsound_delay_ms
9b8f351cced6 added yet another hint to Nitpick's output, this time warning about problems for which nothing was effectively tested
blanchet
parents: 35183
diff changeset
   172
  | unsound_delay_for_timeout (SOME timeout) =
9b8f351cced6 added yet another hint to Nitpick's output, this time warning about problems for which nothing was effectively tested
blanchet
parents: 35183
diff changeset
   173
    Int.max (0, Int.min (max_unsound_delay_ms,
33192
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   174
                         Time.toMilliseconds timeout
35185
9b8f351cced6 added yet another hint to Nitpick's output, this time warning about problems for which nothing was effectively tested
blanchet
parents: 35183
diff changeset
   175
                         * max_unsound_delay_percent div 100))
33192
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   176
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   177
(* Time.time option -> bool *)
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   178
fun passed_deadline NONE = false
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   179
  | passed_deadline (SOME time) = Time.compare (Time.now (), time) <> LESS
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   180
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   181
(* ('a * bool option) list -> bool *)
34123
c4988215a691 distinguish better between "complete" (vs. incomplete) types and "concrete" (vs. abstract) types in Nitpick;
blanchet
parents: 34121
diff changeset
   182
fun none_true assigns = forall (not_equal (SOME true) o snd) assigns
33192
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   183
34038
a2736debeabd make Nitpick output the message "Hint: Maybe you forgot a type constraint?" only for syntactic classes
blanchet
parents: 33982
diff changeset
   184
val syntactic_sorts =
a2736debeabd make Nitpick output the message "Hint: Maybe you forgot a type constraint?" only for syntactic classes
blanchet
parents: 33982
diff changeset
   185
  @{sort "{default,zero,one,plus,minus,uminus,times,inverse,abs,sgn,ord,eq}"} @
a2736debeabd make Nitpick output the message "Hint: Maybe you forgot a type constraint?" only for syntactic classes
blanchet
parents: 33982
diff changeset
   186
  @{sort number}
a2736debeabd make Nitpick output the message "Hint: Maybe you forgot a type constraint?" only for syntactic classes
blanchet
parents: 33982
diff changeset
   187
(* typ -> bool *)
a2736debeabd make Nitpick output the message "Hint: Maybe you forgot a type constraint?" only for syntactic classes
blanchet
parents: 33982
diff changeset
   188
fun has_tfree_syntactic_sort (TFree (_, S as _ :: _)) =
a2736debeabd make Nitpick output the message "Hint: Maybe you forgot a type constraint?" only for syntactic classes
blanchet
parents: 33982
diff changeset
   189
    subset (op =) (S, syntactic_sorts)
a2736debeabd make Nitpick output the message "Hint: Maybe you forgot a type constraint?" only for syntactic classes
blanchet
parents: 33982
diff changeset
   190
  | has_tfree_syntactic_sort _ = false
a2736debeabd make Nitpick output the message "Hint: Maybe you forgot a type constraint?" only for syntactic classes
blanchet
parents: 33982
diff changeset
   191
(* term -> bool *)
a2736debeabd make Nitpick output the message "Hint: Maybe you forgot a type constraint?" only for syntactic classes
blanchet
parents: 33982
diff changeset
   192
val has_syntactic_sorts = exists_type (exists_subtype has_tfree_syntactic_sort)
33192
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   193
33568
532b915afa14 don't run Nitpick at all if Kodkodi is not installed (as indicated by the $KODKODI variable)
blanchet
parents: 33566
diff changeset
   194
(* (unit -> string) -> Pretty.T *)
532b915afa14 don't run Nitpick at all if Kodkodi is not installed (as indicated by the $KODKODI variable)
blanchet
parents: 33566
diff changeset
   195
fun plazy f = Pretty.blk (0, pstrs (f ()))
532b915afa14 don't run Nitpick at all if Kodkodi is not installed (as indicated by the $KODKODI variable)
blanchet
parents: 33566
diff changeset
   196
35335
f715cfde056a support local definitions in Nitpick
blanchet
parents: 35334
diff changeset
   197
(* Time.time -> Proof.state -> params -> bool -> int -> int -> int
f715cfde056a support local definitions in Nitpick
blanchet
parents: 35334
diff changeset
   198
   -> (term * term) list -> term list -> term -> string * Proof.state *)
34982
7b8c366e34a2 added support for nonstandard models to Nitpick (based on an idea by Koen Claessen) and did other fixes to Nitpick
blanchet
parents: 34938
diff changeset
   199
fun pick_them_nits_in_term deadline state (params : params) auto i n step
35335
f715cfde056a support local definitions in Nitpick
blanchet
parents: 35334
diff changeset
   200
                           subst orig_assm_ts orig_t =
33192
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   201
  let
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   202
    val timer = Timer.startRealTimer ()
34935
cb011ba38950 removed the Nitpick code that loaded the "Nitpick" theory explicitly if it's not already loaded, because this didn't work properly and is of doubtful value
blanchet
parents: 34126
diff changeset
   203
    val thy = Proof.theory_of state
cb011ba38950 removed the Nitpick code that loaded the "Nitpick" theory explicitly if it's not already loaded, because this didn't work properly and is of doubtful value
blanchet
parents: 34126
diff changeset
   204
    val ctxt = Proof.context_of state
35386
45a4e19d3ebd more work on the new monotonicity stuff in Nitpick
blanchet
parents: 35385
diff changeset
   205
(* FIXME: reintroduce code before new release:
45a4e19d3ebd more work on the new monotonicity stuff in Nitpick
blanchet
parents: 35385
diff changeset
   206
34039
1fba360b5443 made Nitpick work also for people who import "Plain" instead of "Main"
blanchet
parents: 34038
diff changeset
   207
    val nitpick_thy = ThyInfo.get_theory "Nitpick"
34936
c4f04bee79f3 some work on Nitpick's support for quotient types;
blanchet
parents: 34935
diff changeset
   208
    val _ = Theory.subthy (nitpick_thy, thy) orelse
c4f04bee79f3 some work on Nitpick's support for quotient types;
blanchet
parents: 34935
diff changeset
   209
            error "You must import the theory \"Nitpick\" to use Nitpick"
34982
7b8c366e34a2 added support for nonstandard models to Nitpick (based on an idea by Koen Claessen) and did other fixes to Nitpick
blanchet
parents: 34938
diff changeset
   210
*)
34124
c4628a1dcf75 added support for binary nat/int representation to Nitpick
blanchet
parents: 34123
diff changeset
   211
    val {cards_assigns, maxes_assigns, iters_assigns, bitss, bisim_depths,
35665
ff2bf50505ab added "finitize" option to Nitpick + remove dependency on "Coinductive_List"
blanchet
parents: 35408
diff changeset
   212
         boxes, finitizes, monos, stds, wfs, sat_solver, falsify, debug,
ff2bf50505ab added "finitize" option to Nitpick + remove dependency on "Coinductive_List"
blanchet
parents: 35408
diff changeset
   213
         verbose, overlord, user_axioms, assms, merge_type_vars, binary_ints,
ff2bf50505ab added "finitize" option to Nitpick + remove dependency on "Coinductive_List"
blanchet
parents: 35408
diff changeset
   214
         destroy_constrs, specialize, skolemize, star_linear_preds, uncurry,
ff2bf50505ab added "finitize" option to Nitpick + remove dependency on "Coinductive_List"
blanchet
parents: 35408
diff changeset
   215
         fast_descrs, peephole_optim, tac_timeout, sym_break, sharing_depth,
ff2bf50505ab added "finitize" option to Nitpick + remove dependency on "Coinductive_List"
blanchet
parents: 35408
diff changeset
   216
         flatten_props, max_threads, show_skolems, show_datatypes, show_consts,
ff2bf50505ab added "finitize" option to Nitpick + remove dependency on "Coinductive_List"
blanchet
parents: 35408
diff changeset
   217
         evals, formats, max_potential, max_genuine, check_potential,
ff2bf50505ab added "finitize" option to Nitpick + remove dependency on "Coinductive_List"
blanchet
parents: 35408
diff changeset
   218
         check_genuine, batch_size, ...} =
33192
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   219
      params
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   220
    val state_ref = Unsynchronized.ref state
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   221
    (* Pretty.T -> unit *)
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   222
    val pprint =
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   223
      if auto then
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   224
        Unsynchronized.change state_ref o Proof.goal_message o K
33561
ab01b72715ef introduced Auto Nitpick in addition to Auto Quickcheck;
blanchet
parents: 33558
diff changeset
   225
        o Pretty.chunks o cons (Pretty.str "") o single
33192
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   226
        o Pretty.mark Markup.hilite
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   227
      else
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   228
        priority o Pretty.string_of
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   229
    (* (unit -> Pretty.T) -> unit *)
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   230
    fun pprint_m f = () |> not auto ? pprint o f
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   231
    fun pprint_v f = () |> verbose ? pprint o f
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   232
    fun pprint_d f = () |> debug ? pprint o f
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   233
    (* string -> unit *)
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   234
    val print = pprint o curry Pretty.blk 0 o pstrs
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   235
    (* (unit -> string) -> unit *)
33568
532b915afa14 don't run Nitpick at all if Kodkodi is not installed (as indicated by the $KODKODI variable)
blanchet
parents: 33566
diff changeset
   236
    val print_m = pprint_m o K o plazy
532b915afa14 don't run Nitpick at all if Kodkodi is not installed (as indicated by the $KODKODI variable)
blanchet
parents: 33566
diff changeset
   237
    val print_v = pprint_v o K o plazy
33192
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   238
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   239
    (* unit -> unit *)
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   240
    fun check_deadline () =
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   241
      if debug andalso passed_deadline deadline then raise TimeLimit.TimeOut
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   242
      else ()
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   243
    (* unit -> 'a *)
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   244
    fun do_interrupted () =
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   245
      if passed_deadline deadline then raise TimeLimit.TimeOut
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   246
      else raise Interrupt
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   247
35335
f715cfde056a support local definitions in Nitpick
blanchet
parents: 35334
diff changeset
   248
    val orig_assm_ts = if assms orelse auto then orig_assm_ts else []
34982
7b8c366e34a2 added support for nonstandard models to Nitpick (based on an idea by Koen Claessen) and did other fixes to Nitpick
blanchet
parents: 34938
diff changeset
   249
    val _ =
7b8c366e34a2 added support for nonstandard models to Nitpick (based on an idea by Koen Claessen) and did other fixes to Nitpick
blanchet
parents: 34938
diff changeset
   250
      if step = 0 then
7b8c366e34a2 added support for nonstandard models to Nitpick (based on an idea by Koen Claessen) and did other fixes to Nitpick
blanchet
parents: 34938
diff changeset
   251
        print_m (fn () => "Nitpicking formula...")
7b8c366e34a2 added support for nonstandard models to Nitpick (based on an idea by Koen Claessen) and did other fixes to Nitpick
blanchet
parents: 34938
diff changeset
   252
      else
7b8c366e34a2 added support for nonstandard models to Nitpick (based on an idea by Koen Claessen) and did other fixes to Nitpick
blanchet
parents: 34938
diff changeset
   253
        pprint_m (fn () => Pretty.chunks (
7b8c366e34a2 added support for nonstandard models to Nitpick (based on an idea by Koen Claessen) and did other fixes to Nitpick
blanchet
parents: 34938
diff changeset
   254
            pretties_for_formulas ctxt ("Nitpicking " ^
7b8c366e34a2 added support for nonstandard models to Nitpick (based on an idea by Koen Claessen) and did other fixes to Nitpick
blanchet
parents: 34938
diff changeset
   255
                (if i <> 1 orelse n <> 1 then
7b8c366e34a2 added support for nonstandard models to Nitpick (based on an idea by Koen Claessen) and did other fixes to Nitpick
blanchet
parents: 34938
diff changeset
   256
                   "subgoal " ^ string_of_int i ^ " of " ^ string_of_int n
7b8c366e34a2 added support for nonstandard models to Nitpick (based on an idea by Koen Claessen) and did other fixes to Nitpick
blanchet
parents: 34938
diff changeset
   257
                 else
35181
92d857a4e5e0 synchronize Nitpick's wellfoundedness formulas caching
blanchet
parents: 35177
diff changeset
   258
                   "goal")) [Logic.list_implies (orig_assm_ts, orig_t)]))
33192
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   259
    val neg_t = if falsify then Logic.mk_implies (orig_t, @{prop False})
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   260
                else orig_t
35335
f715cfde056a support local definitions in Nitpick
blanchet
parents: 35334
diff changeset
   261
    val assms_t = Logic.mk_conjunction_list (neg_t :: orig_assm_ts)
33192
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   262
    val (assms_t, evals) =
33705
947184dc75c9 removed a few global names in Nitpick (styp, nat_less, pairf)
blanchet
parents: 33580
diff changeset
   263
      assms_t :: evals |> merge_type_vars ? merge_type_vars_in_terms
947184dc75c9 removed a few global names in Nitpick (styp, nat_less, pairf)
blanchet
parents: 33580
diff changeset
   264
                       |> pairf hd tl
33192
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   265
    val original_max_potential = max_potential
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   266
    val original_max_genuine = max_genuine
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   267
(*
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   268
    val _ = priority ("*** " ^ Syntax.string_of_term ctxt orig_t)
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   269
    val _ = List.app (fn t => priority ("*** " ^ Syntax.string_of_term ctxt t))
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   270
                     orig_assm_ts
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   271
*)
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   272
    val max_bisim_depth = fold Integer.max bisim_depths ~1
35220
2bcdae5f4fdb added support for nonstandard "nat"s to Nitpick and fixed bugs in binary "nat"s and "int"s
blanchet
parents: 35190
diff changeset
   273
    val case_names = case_const_names thy stds
35335
f715cfde056a support local definitions in Nitpick
blanchet
parents: 35334
diff changeset
   274
    val (defs, built_in_nondefs, user_nondefs) = all_axioms_of thy subst
f715cfde056a support local definitions in Nitpick
blanchet
parents: 35334
diff changeset
   275
    val def_table = const_def_table ctxt subst defs
33192
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   276
    val nondef_table = const_nondef_table (built_in_nondefs @ user_nondefs)
35335
f715cfde056a support local definitions in Nitpick
blanchet
parents: 35334
diff changeset
   277
    val simp_table = Unsynchronized.ref (const_simp_table ctxt subst)
f715cfde056a support local definitions in Nitpick
blanchet
parents: 35334
diff changeset
   278
    val psimp_table = const_psimp_table ctxt subst
35807
e4d1b5cbd429 added support for "specification" and "ax_specification" constructs to Nitpick
blanchet
parents: 35711
diff changeset
   279
    val choice_spec_table = const_choice_spec_table ctxt subst
e4d1b5cbd429 added support for "specification" and "ax_specification" constructs to Nitpick
blanchet
parents: 35711
diff changeset
   280
    val user_nondefs =
e4d1b5cbd429 added support for "specification" and "ax_specification" constructs to Nitpick
blanchet
parents: 35711
diff changeset
   281
      user_nondefs |> filter_out (is_choice_spec_axiom thy choice_spec_table)
35335
f715cfde056a support local definitions in Nitpick
blanchet
parents: 35334
diff changeset
   282
    val intro_table = inductive_intro_table ctxt subst def_table
33192
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   283
    val ground_thm_table = ground_theorem_table thy
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   284
    val ersatz_table = ersatz_table thy
35070
96136eb6218f split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents: 34998
diff changeset
   285
    val (hol_ctxt as {wf_cache, ...}) =
33192
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   286
      {thy = thy, ctxt = ctxt, max_bisim_depth = max_bisim_depth, boxes = boxes,
34982
7b8c366e34a2 added support for nonstandard models to Nitpick (based on an idea by Koen Claessen) and did other fixes to Nitpick
blanchet
parents: 34938
diff changeset
   287
       stds = stds, wfs = wfs, user_axioms = user_axioms, debug = debug,
34124
c4628a1dcf75 added support for binary nat/int representation to Nitpick
blanchet
parents: 34123
diff changeset
   288
       binary_ints = binary_ints, destroy_constrs = destroy_constrs,
c4628a1dcf75 added support for binary nat/int representation to Nitpick
blanchet
parents: 34123
diff changeset
   289
       specialize = specialize, skolemize = skolemize,
c4628a1dcf75 added support for binary nat/int representation to Nitpick
blanchet
parents: 34123
diff changeset
   290
       star_linear_preds = star_linear_preds, uncurry = uncurry,
c4628a1dcf75 added support for binary nat/int representation to Nitpick
blanchet
parents: 34123
diff changeset
   291
       fast_descrs = fast_descrs, tac_timeout = tac_timeout, evals = evals,
c4628a1dcf75 added support for binary nat/int representation to Nitpick
blanchet
parents: 34123
diff changeset
   292
       case_names = case_names, def_table = def_table,
33192
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   293
       nondef_table = nondef_table, user_nondefs = user_nondefs,
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   294
       simp_table = simp_table, psimp_table = psimp_table,
35807
e4d1b5cbd429 added support for "specification" and "ax_specification" constructs to Nitpick
blanchet
parents: 35711
diff changeset
   295
       choice_spec_table = choice_spec_table, intro_table = intro_table,
e4d1b5cbd429 added support for "specification" and "ax_specification" constructs to Nitpick
blanchet
parents: 35711
diff changeset
   296
       ground_thm_table = ground_thm_table, ersatz_table = ersatz_table,
e4d1b5cbd429 added support for "specification" and "ax_specification" constructs to Nitpick
blanchet
parents: 35711
diff changeset
   297
       skolems = Unsynchronized.ref [], special_funs = Unsynchronized.ref [],
33580
45c33e97cb86 added datatype constructor cache in Nitpick (to speed up the scope enumeration) and never test more than 4096 scopes
blanchet
parents: 33568
diff changeset
   298
       unrolled_preds = Unsynchronized.ref [], wf_cache = Unsynchronized.ref [],
45c33e97cb86 added datatype constructor cache in Nitpick (to speed up the scope enumeration) and never test more than 4096 scopes
blanchet
parents: 33568
diff changeset
   299
       constr_cache = Unsynchronized.ref []}
33192
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   300
    val frees = Term.add_frees assms_t []
34936
c4f04bee79f3 some work on Nitpick's support for quotient types;
blanchet
parents: 34935
diff changeset
   301
    val _ = null (Term.add_tvars assms_t []) orelse
c4f04bee79f3 some work on Nitpick's support for quotient types;
blanchet
parents: 34935
diff changeset
   302
            raise NOT_SUPPORTED "schematic type variables"
35386
45a4e19d3ebd more work on the new monotonicity stuff in Nitpick
blanchet
parents: 35385
diff changeset
   303
    val (nondef_ts, def_ts, got_all_mono_user_axioms, no_poly_user_axioms,
35665
ff2bf50505ab added "finitize" option to Nitpick + remove dependency on "Coinductive_List"
blanchet
parents: 35408
diff changeset
   304
         binarize) = preprocess_term hol_ctxt finitizes monos assms_t
33192
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   305
    val got_all_user_axioms =
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   306
      got_all_mono_user_axioms andalso no_poly_user_axioms
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   307
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   308
    (* styp * (bool * bool) -> unit *)
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   309
    fun print_wf (x, (gfp, wf)) =
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   310
      pprint (Pretty.blk (0,
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   311
          pstrs ("The " ^ (if gfp then "co" else "") ^ "inductive predicate \"")
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   312
          @ Syntax.pretty_term ctxt (Const x) ::
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   313
          pstrs (if wf then
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   314
                   "\" was proved well-founded. Nitpick can compute it \
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   315
                   \efficiently."
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   316
                 else
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   317
                   "\" could not be proved well-founded. Nitpick might need to \
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   318
                   \unroll it.")))
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   319
    val _ = if verbose then List.app print_wf (!wf_cache) else ()
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   320
    val _ =
35386
45a4e19d3ebd more work on the new monotonicity stuff in Nitpick
blanchet
parents: 35385
diff changeset
   321
      pprint_d (fn () => Pretty.chunks
45a4e19d3ebd more work on the new monotonicity stuff in Nitpick
blanchet
parents: 35385
diff changeset
   322
          (pretties_for_formulas ctxt "Preprocessed formula" [hd nondef_ts] @
45a4e19d3ebd more work on the new monotonicity stuff in Nitpick
blanchet
parents: 35385
diff changeset
   323
           pretties_for_formulas ctxt "Relevant definitional axiom" def_ts @
45a4e19d3ebd more work on the new monotonicity stuff in Nitpick
blanchet
parents: 35385
diff changeset
   324
           pretties_for_formulas ctxt "Relevant nondefinitional axiom"
45a4e19d3ebd more work on the new monotonicity stuff in Nitpick
blanchet
parents: 35385
diff changeset
   325
                                 (tl nondef_ts)))
45a4e19d3ebd more work on the new monotonicity stuff in Nitpick
blanchet
parents: 35385
diff changeset
   326
    val _ = List.app (ignore o Term.type_of) (nondef_ts @ def_ts)
33192
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   327
            handle TYPE (_, Ts, ts) =>
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   328
                   raise TYPE ("Nitpick.pick_them_nits_in_term", Ts, ts)
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   329
35386
45a4e19d3ebd more work on the new monotonicity stuff in Nitpick
blanchet
parents: 35385
diff changeset
   330
    val nondef_us = map (nut_from_term hol_ctxt Eq) nondef_ts
35070
96136eb6218f split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents: 34998
diff changeset
   331
    val def_us = map (nut_from_term hol_ctxt DefEq) def_ts
33558
a2db56854b83 optimized Nitpick's encoding and rendering of datatypes whose constructors don't appear in the problem
blanchet
parents: 33556
diff changeset
   332
    val (free_names, const_names) =
35386
45a4e19d3ebd more work on the new monotonicity stuff in Nitpick
blanchet
parents: 35385
diff changeset
   333
      fold add_free_and_const_names (nondef_us @ def_us) ([], [])
33558
a2db56854b83 optimized Nitpick's encoding and rendering of datatypes whose constructors don't appear in the problem
blanchet
parents: 33556
diff changeset
   334
    val (sel_names, nonsel_names) =
a2db56854b83 optimized Nitpick's encoding and rendering of datatypes whose constructors don't appear in the problem
blanchet
parents: 33556
diff changeset
   335
      List.partition (is_sel o nickname_of) const_names
35665
ff2bf50505ab added "finitize" option to Nitpick + remove dependency on "Coinductive_List"
blanchet
parents: 35408
diff changeset
   336
    val sound_finitizes =
ff2bf50505ab added "finitize" option to Nitpick + remove dependency on "Coinductive_List"
blanchet
parents: 35408
diff changeset
   337
      none_true (filter_out (fn (SOME (Type (@{type_name fun}, _)), _) => true
ff2bf50505ab added "finitize" option to Nitpick + remove dependency on "Coinductive_List"
blanchet
parents: 35408
diff changeset
   338
                          | _ => false) finitizes)
34982
7b8c366e34a2 added support for nonstandard models to Nitpick (based on an idea by Koen Claessen) and did other fixes to Nitpick
blanchet
parents: 34938
diff changeset
   339
    val standard = forall snd stds
33558
a2db56854b83 optimized Nitpick's encoding and rendering of datatypes whose constructors don't appear in the problem
blanchet
parents: 33556
diff changeset
   340
(*
35386
45a4e19d3ebd more work on the new monotonicity stuff in Nitpick
blanchet
parents: 35385
diff changeset
   341
    val _ = List.app (priority o string_for_nut ctxt) (nondef_us @ def_us)
33558
a2db56854b83 optimized Nitpick's encoding and rendering of datatypes whose constructors don't appear in the problem
blanchet
parents: 33556
diff changeset
   342
*)
a2db56854b83 optimized Nitpick's encoding and rendering of datatypes whose constructors don't appear in the problem
blanchet
parents: 33556
diff changeset
   343
34121
5e831d805118 get rid of polymorphic equality in Nitpick's code + a few minor cleanups
blanchet
parents: 34039
diff changeset
   344
    val unique_scope = forall (curry (op =) 1 o length o snd) cards_assigns
35385
29f81babefd7 improved precision of infinite "shallow" datatypes in Nitpick;
blanchet
parents: 35384
diff changeset
   345
    (* typ list -> string -> string *)
29f81babefd7 improved precision of infinite "shallow" datatypes in Nitpick;
blanchet
parents: 35384
diff changeset
   346
    fun monotonicity_message Ts extra =
29f81babefd7 improved precision of infinite "shallow" datatypes in Nitpick;
blanchet
parents: 35384
diff changeset
   347
      let val ss = map (quote o string_for_type ctxt) Ts in
29f81babefd7 improved precision of infinite "shallow" datatypes in Nitpick;
blanchet
parents: 35384
diff changeset
   348
        "The type" ^ plural_s_for_list ss ^ " " ^
35968
b7f98ff9c7d9 simplify Nitpick parameter parsing code a little bit + make compile
blanchet
parents: 35814
diff changeset
   349
        space_implode " " (Sledgehammer_Util.serial_commas "and" ss) ^ " " ^
35385
29f81babefd7 improved precision of infinite "shallow" datatypes in Nitpick;
blanchet
parents: 35384
diff changeset
   350
        (if none_true monos then
29f81babefd7 improved precision of infinite "shallow" datatypes in Nitpick;
blanchet
parents: 35384
diff changeset
   351
           "passed the monotonicity test"
29f81babefd7 improved precision of infinite "shallow" datatypes in Nitpick;
blanchet
parents: 35384
diff changeset
   352
         else
29f81babefd7 improved precision of infinite "shallow" datatypes in Nitpick;
blanchet
parents: 35384
diff changeset
   353
           (if length ss = 1 then "is" else "are") ^ " considered monotonic") ^
29f81babefd7 improved precision of infinite "shallow" datatypes in Nitpick;
blanchet
parents: 35384
diff changeset
   354
        ". " ^ extra
29f81babefd7 improved precision of infinite "shallow" datatypes in Nitpick;
blanchet
parents: 35384
diff changeset
   355
      end
33192
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   356
    (* typ -> bool *)
35665
ff2bf50505ab added "finitize" option to Nitpick + remove dependency on "Coinductive_List"
blanchet
parents: 35408
diff changeset
   357
    fun is_type_fundamentally_monotonic T =
35220
2bcdae5f4fdb added support for nonstandard "nat"s to Nitpick and fixed bugs in binary "nat"s and "int"s
blanchet
parents: 35190
diff changeset
   358
      (is_datatype thy stds T andalso not (is_quot_type thy T) andalso
34938
f4d3daddac42 fix issues with previous Nitpick change
blanchet
parents: 34936
diff changeset
   359
       (not (is_pure_typedef thy T) orelse is_univ_typedef thy T)) orelse
35075
888802be2019 handle Nitpick's nonstandard model enumeration in a cleaner way;
blanchet
parents: 35070
diff changeset
   360
      is_number_type thy T orelse is_bit_type T
35385
29f81babefd7 improved precision of infinite "shallow" datatypes in Nitpick;
blanchet
parents: 35384
diff changeset
   361
    fun is_type_actually_monotonic T =
35386
45a4e19d3ebd more work on the new monotonicity stuff in Nitpick
blanchet
parents: 35385
diff changeset
   362
      formulas_monotonic hol_ctxt binarize T (nondef_ts, def_ts)
35665
ff2bf50505ab added "finitize" option to Nitpick + remove dependency on "Coinductive_List"
blanchet
parents: 35408
diff changeset
   363
    fun is_type_kind_of_monotonic T =
ff2bf50505ab added "finitize" option to Nitpick + remove dependency on "Coinductive_List"
blanchet
parents: 35408
diff changeset
   364
      case triple_lookup (type_match thy) monos T of
ff2bf50505ab added "finitize" option to Nitpick + remove dependency on "Coinductive_List"
blanchet
parents: 35408
diff changeset
   365
        SOME (SOME false) => false
ff2bf50505ab added "finitize" option to Nitpick + remove dependency on "Coinductive_List"
blanchet
parents: 35408
diff changeset
   366
      | _ => is_type_actually_monotonic T
34936
c4f04bee79f3 some work on Nitpick's support for quotient types;
blanchet
parents: 34935
diff changeset
   367
    fun is_type_monotonic T =
33192
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   368
      unique_scope orelse
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   369
      case triple_lookup (type_match thy) monos T of
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   370
        SOME (SOME b) => b
35665
ff2bf50505ab added "finitize" option to Nitpick + remove dependency on "Coinductive_List"
blanchet
parents: 35408
diff changeset
   371
      | _ => is_type_fundamentally_monotonic T orelse
ff2bf50505ab added "finitize" option to Nitpick + remove dependency on "Coinductive_List"
blanchet
parents: 35408
diff changeset
   372
             is_type_actually_monotonic T
ff2bf50505ab added "finitize" option to Nitpick + remove dependency on "Coinductive_List"
blanchet
parents: 35408
diff changeset
   373
    fun is_shallow_datatype_finitizable (T as Type (@{type_name fin_fun}, _)) =
ff2bf50505ab added "finitize" option to Nitpick + remove dependency on "Coinductive_List"
blanchet
parents: 35408
diff changeset
   374
        is_type_kind_of_monotonic T
ff2bf50505ab added "finitize" option to Nitpick + remove dependency on "Coinductive_List"
blanchet
parents: 35408
diff changeset
   375
      | is_shallow_datatype_finitizable (T as Type (@{type_name fun_box}, _)) =
ff2bf50505ab added "finitize" option to Nitpick + remove dependency on "Coinductive_List"
blanchet
parents: 35408
diff changeset
   376
        is_type_kind_of_monotonic T
ff2bf50505ab added "finitize" option to Nitpick + remove dependency on "Coinductive_List"
blanchet
parents: 35408
diff changeset
   377
      | is_shallow_datatype_finitizable T =
ff2bf50505ab added "finitize" option to Nitpick + remove dependency on "Coinductive_List"
blanchet
parents: 35408
diff changeset
   378
        case triple_lookup (type_match thy) finitizes T of
ff2bf50505ab added "finitize" option to Nitpick + remove dependency on "Coinductive_List"
blanchet
parents: 35408
diff changeset
   379
          SOME (SOME b) => b
ff2bf50505ab added "finitize" option to Nitpick + remove dependency on "Coinductive_List"
blanchet
parents: 35408
diff changeset
   380
        | _ => is_type_kind_of_monotonic T
35385
29f81babefd7 improved precision of infinite "shallow" datatypes in Nitpick;
blanchet
parents: 35384
diff changeset
   381
    fun is_datatype_deep T =
29f81babefd7 improved precision of infinite "shallow" datatypes in Nitpick;
blanchet
parents: 35384
diff changeset
   382
      not standard orelse T = nat_T orelse is_word_type T orelse
29f81babefd7 improved precision of infinite "shallow" datatypes in Nitpick;
blanchet
parents: 35384
diff changeset
   383
      exists (curry (op =) T o domain_type o type_of) sel_names
35386
45a4e19d3ebd more work on the new monotonicity stuff in Nitpick
blanchet
parents: 35385
diff changeset
   384
    val all_Ts = ground_types_in_terms hol_ctxt binarize (nondef_ts @ def_ts)
35408
b48ab741683b modernized structure Term_Ord;
wenzelm
parents: 35386
diff changeset
   385
                 |> sort Term_Ord.typ_ord
34936
c4f04bee79f3 some work on Nitpick's support for quotient types;
blanchet
parents: 34935
diff changeset
   386
    val _ = if verbose andalso binary_ints = SOME true andalso
34982
7b8c366e34a2 added support for nonstandard models to Nitpick (based on an idea by Koen Claessen) and did other fixes to Nitpick
blanchet
parents: 34938
diff changeset
   387
               exists (member (op =) [nat_T, int_T]) all_Ts then
34124
c4628a1dcf75 added support for binary nat/int representation to Nitpick
blanchet
parents: 34123
diff changeset
   388
              print_v (K "The option \"binary_ints\" will be ignored because \
34126
8a2c5d7aff51 polished Nitpick's binary integer support etc.;
blanchet
parents: 34124
diff changeset
   389
                         \of the presence of rationals, reals, \"Suc\", \
35386
45a4e19d3ebd more work on the new monotonicity stuff in Nitpick
blanchet
parents: 35385
diff changeset
   390
                         \\"gcd\", or \"lcm\" in the problem or because of the \
45a4e19d3ebd more work on the new monotonicity stuff in Nitpick
blanchet
parents: 35385
diff changeset
   391
                         \\"non_std\" option.")
34124
c4628a1dcf75 added support for binary nat/int representation to Nitpick
blanchet
parents: 34123
diff changeset
   392
            else
c4628a1dcf75 added support for binary nat/int representation to Nitpick
blanchet
parents: 34123
diff changeset
   393
              ()
34982
7b8c366e34a2 added support for nonstandard models to Nitpick (based on an idea by Koen Claessen) and did other fixes to Nitpick
blanchet
parents: 34938
diff changeset
   394
    val (mono_Ts, nonmono_Ts) = List.partition is_type_monotonic all_Ts
33192
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   395
    val _ =
34936
c4f04bee79f3 some work on Nitpick's support for quotient types;
blanchet
parents: 34935
diff changeset
   396
      if verbose andalso not unique_scope then
35665
ff2bf50505ab added "finitize" option to Nitpick + remove dependency on "Coinductive_List"
blanchet
parents: 35408
diff changeset
   397
        case filter_out is_type_fundamentally_monotonic mono_Ts of
34936
c4f04bee79f3 some work on Nitpick's support for quotient types;
blanchet
parents: 34935
diff changeset
   398
          [] => ()
c4f04bee79f3 some work on Nitpick's support for quotient types;
blanchet
parents: 34935
diff changeset
   399
        | interesting_mono_Ts =>
35385
29f81babefd7 improved precision of infinite "shallow" datatypes in Nitpick;
blanchet
parents: 35384
diff changeset
   400
          print_v (K (monotonicity_message interesting_mono_Ts
29f81babefd7 improved precision of infinite "shallow" datatypes in Nitpick;
blanchet
parents: 35384
diff changeset
   401
                         "Nitpick might be able to skip some scopes."))
33192
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   402
      else
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   403
        ()
35385
29f81babefd7 improved precision of infinite "shallow" datatypes in Nitpick;
blanchet
parents: 35384
diff changeset
   404
    val (deep_dataTs, shallow_dataTs) =
29f81babefd7 improved precision of infinite "shallow" datatypes in Nitpick;
blanchet
parents: 35384
diff changeset
   405
      all_Ts |> filter (is_datatype thy stds) |> List.partition is_datatype_deep
29f81babefd7 improved precision of infinite "shallow" datatypes in Nitpick;
blanchet
parents: 35384
diff changeset
   406
    val finitizable_dataTs =
29f81babefd7 improved precision of infinite "shallow" datatypes in Nitpick;
blanchet
parents: 35384
diff changeset
   407
      shallow_dataTs |> filter_out (is_finite_type hol_ctxt)
35665
ff2bf50505ab added "finitize" option to Nitpick + remove dependency on "Coinductive_List"
blanchet
parents: 35408
diff changeset
   408
                     |> filter is_shallow_datatype_finitizable
35385
29f81babefd7 improved precision of infinite "shallow" datatypes in Nitpick;
blanchet
parents: 35384
diff changeset
   409
    val _ =
29f81babefd7 improved precision of infinite "shallow" datatypes in Nitpick;
blanchet
parents: 35384
diff changeset
   410
      if verbose andalso not (null finitizable_dataTs) then
29f81babefd7 improved precision of infinite "shallow" datatypes in Nitpick;
blanchet
parents: 35384
diff changeset
   411
        print_v (K (monotonicity_message finitizable_dataTs
29f81babefd7 improved precision of infinite "shallow" datatypes in Nitpick;
blanchet
parents: 35384
diff changeset
   412
                        "Nitpick can use a more precise finite encoding."))
29f81babefd7 improved precision of infinite "shallow" datatypes in Nitpick;
blanchet
parents: 35384
diff changeset
   413
      else
29f81babefd7 improved precision of infinite "shallow" datatypes in Nitpick;
blanchet
parents: 35384
diff changeset
   414
        ()
35183
8580ba651489 reintroduce structural induction hint in Nitpick
blanchet
parents: 35181
diff changeset
   415
    (* This detection code is an ugly hack. Fortunately, it is used only to
8580ba651489 reintroduce structural induction hint in Nitpick
blanchet
parents: 35181
diff changeset
   416
       provide a hint to the user. *)
34982
7b8c366e34a2 added support for nonstandard models to Nitpick (based on an idea by Koen Claessen) and did other fixes to Nitpick
blanchet
parents: 34938
diff changeset
   417
    (* string * (Rule_Cases.T * bool) -> bool *)
35183
8580ba651489 reintroduce structural induction hint in Nitpick
blanchet
parents: 35181
diff changeset
   418
    fun is_struct_induct_step (name, (Rule_Cases.Case {fixes, assumes, ...}, _)) =
8580ba651489 reintroduce structural induction hint in Nitpick
blanchet
parents: 35181
diff changeset
   419
      not (null fixes) andalso
8580ba651489 reintroduce structural induction hint in Nitpick
blanchet
parents: 35181
diff changeset
   420
      exists (String.isSuffix ".hyps" o fst) assumes andalso
8580ba651489 reintroduce structural induction hint in Nitpick
blanchet
parents: 35181
diff changeset
   421
      exists (exists (curry (op =) name o shortest_name o fst)
8580ba651489 reintroduce structural induction hint in Nitpick
blanchet
parents: 35181
diff changeset
   422
              o datatype_constrs hol_ctxt) deep_dataTs
8580ba651489 reintroduce structural induction hint in Nitpick
blanchet
parents: 35181
diff changeset
   423
    val likely_in_struct_induct_step =
8580ba651489 reintroduce structural induction hint in Nitpick
blanchet
parents: 35181
diff changeset
   424
      exists is_struct_induct_step (ProofContext.cases_of ctxt)
8580ba651489 reintroduce structural induction hint in Nitpick
blanchet
parents: 35181
diff changeset
   425
    val _ = if standard andalso likely_in_struct_induct_step then
34982
7b8c366e34a2 added support for nonstandard models to Nitpick (based on an idea by Koen Claessen) and did other fixes to Nitpick
blanchet
parents: 34938
diff changeset
   426
              pprint_m (fn () => Pretty.blk (0,
7b8c366e34a2 added support for nonstandard models to Nitpick (based on an idea by Koen Claessen) and did other fixes to Nitpick
blanchet
parents: 34938
diff changeset
   427
                  pstrs "Hint: To check that the induction hypothesis is \
35177
168041f24f80 various cosmetic changes to Nitpick
blanchet
parents: 35075
diff changeset
   428
                        \general enough, try this command: " @
34982
7b8c366e34a2 added support for nonstandard models to Nitpick (based on an idea by Koen Claessen) and did other fixes to Nitpick
blanchet
parents: 34938
diff changeset
   429
                  [Pretty.mark Markup.sendback (Pretty.blk (0,
35183
8580ba651489 reintroduce structural induction hint in Nitpick
blanchet
parents: 35181
diff changeset
   430
                       pstrs ("nitpick [non_std, show_all]")))] @ pstrs "."))
34982
7b8c366e34a2 added support for nonstandard models to Nitpick (based on an idea by Koen Claessen) and did other fixes to Nitpick
blanchet
parents: 34938
diff changeset
   431
            else
7b8c366e34a2 added support for nonstandard models to Nitpick (based on an idea by Koen Claessen) and did other fixes to Nitpick
blanchet
parents: 34938
diff changeset
   432
              ()
33192
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   433
(*
34936
c4f04bee79f3 some work on Nitpick's support for quotient types;
blanchet
parents: 34935
diff changeset
   434
    val _ = priority "Monotonic types:"
c4f04bee79f3 some work on Nitpick's support for quotient types;
blanchet
parents: 34935
diff changeset
   435
    val _ = List.app (priority o string_for_type ctxt) mono_Ts
c4f04bee79f3 some work on Nitpick's support for quotient types;
blanchet
parents: 34935
diff changeset
   436
    val _ = priority "Nonmonotonic types:"
c4f04bee79f3 some work on Nitpick's support for quotient types;
blanchet
parents: 34935
diff changeset
   437
    val _ = List.app (priority o string_for_type ctxt) nonmono_Ts
33192
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   438
*)
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   439
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   440
    val need_incremental = Int.max (max_potential, max_genuine) >= 2
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   441
    val effective_sat_solver =
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   442
      if sat_solver <> "smart" then
34936
c4f04bee79f3 some work on Nitpick's support for quotient types;
blanchet
parents: 34935
diff changeset
   443
        if need_incremental andalso
c4f04bee79f3 some work on Nitpick's support for quotient types;
blanchet
parents: 34935
diff changeset
   444
           not (member (op =) (Kodkod_SAT.configured_sat_solvers true)
35333
f61de25f71f9 distinguish between Kodkodi warnings and errors in Nitpick;
blanchet
parents: 35280
diff changeset
   445
                       sat_solver) then
33192
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   446
          (print_m (K ("An incremental SAT solver is required: \"SAT4J\" will \
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   447
                       \be used instead of " ^ quote sat_solver ^ "."));
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   448
           "SAT4J")
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   449
        else
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   450
          sat_solver
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   451
      else
33232
f93390060bbe internal renaming in Nitpick and fixed Kodkodi invokation on Linux;
blanchet
parents: 33192
diff changeset
   452
        Kodkod_SAT.smart_sat_solver_name need_incremental
33192
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   453
    val _ =
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   454
      if sat_solver = "smart" then
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   455
        print_v (fn () => "Using SAT solver " ^ quote effective_sat_solver ^
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   456
                          ". The following" ^
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   457
                          (if need_incremental then " incremental " else " ") ^
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   458
                          "solvers are configured: " ^
33232
f93390060bbe internal renaming in Nitpick and fixed Kodkodi invokation on Linux;
blanchet
parents: 33192
diff changeset
   459
                          commas (map quote (Kodkod_SAT.configured_sat_solvers
33192
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   460
                                                       need_incremental)) ^ ".")
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   461
      else
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   462
        ()
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   463
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   464
    val too_big_scopes = Unsynchronized.ref []
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   465
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   466
    (* bool -> scope -> rich_problem option *)
35185
9b8f351cced6 added yet another hint to Nitpick's output, this time warning about problems for which nothing was effectively tested
blanchet
parents: 35183
diff changeset
   467
    fun problem_for_scope unsound
34124
c4628a1dcf75 added support for binary nat/int representation to Nitpick
blanchet
parents: 34123
diff changeset
   468
            (scope as {card_assigns, bits, bisim_depth, datatypes, ofs, ...}) =
33192
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   469
      let
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   470
        val _ = not (exists (fn other => scope_less_eq other scope)
34936
c4f04bee79f3 some work on Nitpick's support for quotient types;
blanchet
parents: 34935
diff changeset
   471
                            (!too_big_scopes)) orelse
c4f04bee79f3 some work on Nitpick's support for quotient types;
blanchet
parents: 34935
diff changeset
   472
                raise TOO_LARGE ("Nitpick.pick_them_nits_in_term.\
c4f04bee79f3 some work on Nitpick's support for quotient types;
blanchet
parents: 34935
diff changeset
   473
                                 \problem_for_scope", "too large scope")
33192
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   474
(*
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   475
        val _ = priority "Offsets:"
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   476
        val _ = List.app (fn (T, j0) =>
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   477
                             priority (string_for_type ctxt T ^ " = " ^
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   478
                                       string_of_int j0))
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   479
                         (Typtab.dest ofs)
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   480
*)
35385
29f81babefd7 improved precision of infinite "shallow" datatypes in Nitpick;
blanchet
parents: 35384
diff changeset
   481
        val all_exact = forall (is_exact_type datatypes true) all_Ts
33192
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   482
        (* nut list -> rep NameTable.table -> nut list * rep NameTable.table *)
34123
c4988215a691 distinguish better between "complete" (vs. incomplete) types and "concrete" (vs. abstract) types in Nitpick;
blanchet
parents: 34121
diff changeset
   483
        val repify_consts = choose_reps_for_consts scope all_exact
33192
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   484
        val main_j0 = offset_of_type ofs bool_T
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   485
        val (nat_card, nat_j0) = spec_of_type scope nat_T
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   486
        val (int_card, int_j0) = spec_of_type scope int_T
34936
c4f04bee79f3 some work on Nitpick's support for quotient types;
blanchet
parents: 34935
diff changeset
   487
        val _ = (nat_j0 = main_j0 andalso int_j0 = main_j0) orelse
c4f04bee79f3 some work on Nitpick's support for quotient types;
blanchet
parents: 34935
diff changeset
   488
                raise BAD ("Nitpick.pick_them_nits_in_term.problem_for_scope",
c4f04bee79f3 some work on Nitpick's support for quotient types;
blanchet
parents: 34935
diff changeset
   489
                           "bad offsets")
33192
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   490
        val kk = kodkod_constrs peephole_optim nat_card int_card main_j0
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   491
        val (free_names, rep_table) =
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   492
          choose_reps_for_free_vars scope free_names NameTable.empty
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   493
        val (sel_names, rep_table) = choose_reps_for_all_sels scope rep_table
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   494
        val (nonsel_names, rep_table) = repify_consts nonsel_names rep_table
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   495
        val min_highest_arity =
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   496
          NameTable.fold (curry Int.max o arity_of_rep o snd) rep_table 1
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   497
        val min_univ_card =
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   498
          NameTable.fold (curry Int.max o min_univ_card_of_rep o snd) rep_table
34126
8a2c5d7aff51 polished Nitpick's binary integer support etc.;
blanchet
parents: 34124
diff changeset
   499
                         (univ_card nat_card int_card main_j0 [] KK.True)
33192
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   500
        val _ = check_arity min_univ_card min_highest_arity
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   501
35185
9b8f351cced6 added yet another hint to Nitpick's output, this time warning about problems for which nothing was effectively tested
blanchet
parents: 35183
diff changeset
   502
        val def_us = map (choose_reps_in_nut scope unsound rep_table true)
33192
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   503
                         def_us
35185
9b8f351cced6 added yet another hint to Nitpick's output, this time warning about problems for which nothing was effectively tested
blanchet
parents: 35183
diff changeset
   504
        val nondef_us = map (choose_reps_in_nut scope unsound rep_table false)
33192
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   505
                            nondef_us
33745
daf236998f82 comment out debugging code in Nitpick
blanchet
parents: 33744
diff changeset
   506
(*
33192
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   507
        val _ = List.app (priority o string_for_nut ctxt)
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   508
                         (free_names @ sel_names @ nonsel_names @
35386
45a4e19d3ebd more work on the new monotonicity stuff in Nitpick
blanchet
parents: 35385
diff changeset
   509
                          nondef_us @ def_us)
33745
daf236998f82 comment out debugging code in Nitpick
blanchet
parents: 33744
diff changeset
   510
*)
33192
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   511
        val (free_rels, pool, rel_table) =
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   512
          rename_free_vars free_names initial_pool NameTable.empty
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   513
        val (sel_rels, pool, rel_table) =
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   514
          rename_free_vars sel_names pool rel_table
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   515
        val (other_rels, pool, rel_table) =
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   516
          rename_free_vars nonsel_names pool rel_table
35386
45a4e19d3ebd more work on the new monotonicity stuff in Nitpick
blanchet
parents: 35385
diff changeset
   517
        val nondef_us = map (rename_vars_in_nut pool rel_table) nondef_us
33192
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   518
        val def_us = map (rename_vars_in_nut pool rel_table) def_us
35386
45a4e19d3ebd more work on the new monotonicity stuff in Nitpick
blanchet
parents: 35385
diff changeset
   519
        val nondef_fs = map (kodkod_formula_from_nut ofs kk) nondef_us
35280
54ab4921f826 fixed a few bugs in Nitpick and removed unreferenced variables
blanchet
parents: 35220
diff changeset
   520
        val def_fs = map (kodkod_formula_from_nut ofs kk) def_us
35386
45a4e19d3ebd more work on the new monotonicity stuff in Nitpick
blanchet
parents: 35385
diff changeset
   521
        val formula = fold (fold s_and) [def_fs, nondef_fs] KK.True
35185
9b8f351cced6 added yet another hint to Nitpick's output, this time warning about problems for which nothing was effectively tested
blanchet
parents: 35183
diff changeset
   522
        val comment = (if unsound then "unsound" else "sound") ^ "\n" ^
33192
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   523
                      PrintMode.setmp [] multiline_string_for_scope scope
34998
5e492a862b34 four changes to Nitpick:
blanchet
parents: 34982
diff changeset
   524
        val kodkod_sat_solver =
35177
168041f24f80 various cosmetic changes to Nitpick
blanchet
parents: 35075
diff changeset
   525
          Kodkod_SAT.sat_solver_spec effective_sat_solver |> snd
34124
c4628a1dcf75 added support for binary nat/int representation to Nitpick
blanchet
parents: 34123
diff changeset
   526
        val bit_width = if bits = 0 then 16 else bits + 1
35185
9b8f351cced6 added yet another hint to Nitpick's output, this time warning about problems for which nothing was effectively tested
blanchet
parents: 35183
diff changeset
   527
        val delay = if unsound then
33192
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   528
                      Option.map (fn time => Time.- (time, Time.now ()))
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   529
                                 deadline
35185
9b8f351cced6 added yet another hint to Nitpick's output, this time warning about problems for which nothing was effectively tested
blanchet
parents: 35183
diff changeset
   530
                      |> unsound_delay_for_timeout
33192
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   531
                    else
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   532
                      0
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   533
        val settings = [("solver", commas (map quote kodkod_sat_solver)),
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   534
                        ("skolem_depth", "-1"),
34124
c4628a1dcf75 added support for binary nat/int representation to Nitpick
blanchet
parents: 34123
diff changeset
   535
                        ("bit_width", string_of_int bit_width),
33192
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   536
                        ("symmetry_breaking", signed_string_of_int sym_break),
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   537
                        ("sharing", signed_string_of_int sharing_depth),
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   538
                        ("flatten", Bool.toString flatten_props),
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   539
                        ("delay", signed_string_of_int delay)]
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   540
        val plain_rels = free_rels @ other_rels
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   541
        val plain_bounds = map (bound_for_plain_rel ctxt debug) plain_rels
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   542
        val plain_axioms = map (declarative_axiom_for_plain_rel kk) plain_rels
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   543
        val sel_bounds = map (bound_for_sel_rel ctxt debug datatypes) sel_rels
35190
ce653cc27a94 make sure that Nitpick uses binary notation consistently if "binary_ints" is enabled
blanchet
parents: 35185
diff changeset
   544
        val dtype_axioms =
ce653cc27a94 make sure that Nitpick uses binary notation consistently if "binary_ints" is enabled
blanchet
parents: 35185
diff changeset
   545
          declarative_axioms_for_datatypes hol_ctxt binarize bits ofs kk
ce653cc27a94 make sure that Nitpick uses binary notation consistently if "binary_ints" is enabled
blanchet
parents: 35185
diff changeset
   546
                                           rel_table datatypes
33192
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   547
        val declarative_axioms = plain_axioms @ dtype_axioms
35220
2bcdae5f4fdb added support for nonstandard "nat"s to Nitpick and fixed bugs in binary "nat"s and "int"s
blanchet
parents: 35190
diff changeset
   548
        val univ_card = Int.max (univ_card nat_card int_card main_j0
2bcdae5f4fdb added support for nonstandard "nat"s to Nitpick and fixed bugs in binary "nat"s and "int"s
blanchet
parents: 35190
diff changeset
   549
                                     (plain_bounds @ sel_bounds) formula,
2bcdae5f4fdb added support for nonstandard "nat"s to Nitpick and fixed bugs in binary "nat"s and "int"s
blanchet
parents: 35190
diff changeset
   550
                                 main_j0 |> bits > 0 ? Integer.add (bits + 1))
33192
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   551
        val built_in_bounds = bounds_for_built_in_rels_in_formula debug
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   552
                                  univ_card nat_card int_card main_j0 formula
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   553
        val bounds = built_in_bounds @ plain_bounds @ sel_bounds
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   554
                     |> not debug ? merge_bounds
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   555
        val highest_arity =
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   556
          fold Integer.max (map (fst o fst) (maps fst bounds)) 0
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   557
        val formula = fold_rev s_and declarative_axioms formula
34124
c4628a1dcf75 added support for binary nat/int representation to Nitpick
blanchet
parents: 34123
diff changeset
   558
        val _ = if bits = 0 then () else check_bits bits formula
34126
8a2c5d7aff51 polished Nitpick's binary integer support etc.;
blanchet
parents: 34124
diff changeset
   559
        val _ = if formula = KK.False then ()
33192
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   560
                else check_arity univ_card highest_arity
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   561
      in
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   562
        SOME ({comment = comment, settings = settings, univ_card = univ_card,
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   563
               tuple_assigns = [], bounds = bounds,
35280
54ab4921f826 fixed a few bugs in Nitpick and removed unreferenced variables
blanchet
parents: 35220
diff changeset
   564
               int_bounds = if bits = 0 then sequential_int_bounds univ_card
54ab4921f826 fixed a few bugs in Nitpick and removed unreferenced variables
blanchet
parents: 35220
diff changeset
   565
                            else pow_of_two_int_bounds bits main_j0,
33192
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   566
               expr_assigns = [], formula = formula},
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   567
              {free_names = free_names, sel_names = sel_names,
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   568
               nonsel_names = nonsel_names, rel_table = rel_table,
35386
45a4e19d3ebd more work on the new monotonicity stuff in Nitpick
blanchet
parents: 35385
diff changeset
   569
               unsound = unsound, scope = scope})
33192
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   570
      end
34124
c4628a1dcf75 added support for binary nat/int representation to Nitpick
blanchet
parents: 34123
diff changeset
   571
      handle TOO_LARGE (loc, msg) =>
34936
c4f04bee79f3 some work on Nitpick's support for quotient types;
blanchet
parents: 34935
diff changeset
   572
             if loc = "Nitpick_Kodkod.check_arity" andalso
c4f04bee79f3 some work on Nitpick's support for quotient types;
blanchet
parents: 34935
diff changeset
   573
                not (Typtab.is_empty ofs) then
35185
9b8f351cced6 added yet another hint to Nitpick's output, this time warning about problems for which nothing was effectively tested
blanchet
parents: 35183
diff changeset
   574
               problem_for_scope unsound
35190
ce653cc27a94 make sure that Nitpick uses binary notation consistently if "binary_ints" is enabled
blanchet
parents: 35185
diff changeset
   575
                   {hol_ctxt = hol_ctxt, binarize = binarize,
ce653cc27a94 make sure that Nitpick uses binary notation consistently if "binary_ints" is enabled
blanchet
parents: 35185
diff changeset
   576
                    card_assigns = card_assigns, bits = bits,
ce653cc27a94 make sure that Nitpick uses binary notation consistently if "binary_ints" is enabled
blanchet
parents: 35185
diff changeset
   577
                    bisim_depth = bisim_depth, datatypes = datatypes,
ce653cc27a94 make sure that Nitpick uses binary notation consistently if "binary_ints" is enabled
blanchet
parents: 35185
diff changeset
   578
                    ofs = Typtab.empty}
33192
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   579
             else if loc = "Nitpick.pick_them_nits_in_term.\
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   580
                           \problem_for_scope" then
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   581
               NONE
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   582
             else
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   583
               (Unsynchronized.change too_big_scopes (cons scope);
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   584
                print_v (fn () => ("Limit reached: " ^ msg ^
35185
9b8f351cced6 added yet another hint to Nitpick's output, this time warning about problems for which nothing was effectively tested
blanchet
parents: 35183
diff changeset
   585
                                   ". Skipping " ^ (if unsound then "potential"
33192
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   586
                                                    else "genuine") ^
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   587
                                   " component of scope."));
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   588
                NONE)
35280
54ab4921f826 fixed a few bugs in Nitpick and removed unreferenced variables
blanchet
parents: 35220
diff changeset
   589
           | TOO_SMALL (_, msg) =>
34124
c4628a1dcf75 added support for binary nat/int representation to Nitpick
blanchet
parents: 34123
diff changeset
   590
             (print_v (fn () => ("Limit reached: " ^ msg ^
35185
9b8f351cced6 added yet another hint to Nitpick's output, this time warning about problems for which nothing was effectively tested
blanchet
parents: 35183
diff changeset
   591
                                 ". Skipping " ^ (if unsound then "potential"
34124
c4628a1dcf75 added support for binary nat/int representation to Nitpick
blanchet
parents: 34123
diff changeset
   592
                                                  else "genuine") ^
c4628a1dcf75 added support for binary nat/int representation to Nitpick
blanchet
parents: 34123
diff changeset
   593
                                 " component of scope."));
c4628a1dcf75 added support for binary nat/int representation to Nitpick
blanchet
parents: 34123
diff changeset
   594
              NONE)
33192
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   595
34982
7b8c366e34a2 added support for nonstandard models to Nitpick (based on an idea by Koen Claessen) and did other fixes to Nitpick
blanchet
parents: 34938
diff changeset
   596
    val das_wort_model =
7b8c366e34a2 added support for nonstandard models to Nitpick (based on an idea by Koen Claessen) and did other fixes to Nitpick
blanchet
parents: 34938
diff changeset
   597
      (if falsify then "counterexample" else "model")
7b8c366e34a2 added support for nonstandard models to Nitpick (based on an idea by Koen Claessen) and did other fixes to Nitpick
blanchet
parents: 34938
diff changeset
   598
      |> not standard ? prefix "nonstandard "
33192
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   599
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   600
    val scopes = Unsynchronized.ref []
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   601
    val generated_scopes = Unsynchronized.ref []
35185
9b8f351cced6 added yet another hint to Nitpick's output, this time warning about problems for which nothing was effectively tested
blanchet
parents: 35183
diff changeset
   602
    val generated_problems = Unsynchronized.ref ([] : rich_problem list)
33192
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   603
    val checked_problems = Unsynchronized.ref (SOME [])
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   604
    val met_potential = Unsynchronized.ref 0
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   605
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   606
    (* rich_problem list -> int list -> unit *)
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   607
    fun update_checked_problems problems =
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   608
      List.app (Unsynchronized.change checked_problems o Option.map o cons
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   609
                o nth problems)
35333
f61de25f71f9 distinguish between Kodkodi warnings and errors in Nitpick;
blanchet
parents: 35280
diff changeset
   610
    (* string -> unit *)
f61de25f71f9 distinguish between Kodkodi warnings and errors in Nitpick;
blanchet
parents: 35280
diff changeset
   611
    fun show_kodkod_warning "" = ()
35334
b83b9f2a4b92 show Kodkod warning message even in non-verbose mode
blanchet
parents: 35333
diff changeset
   612
      | show_kodkod_warning s = print_m (fn () => "Kodkod warning: " ^ s ^ ".")
33192
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   613
35671
ed2c3830d881 improved Nitpick's precision for "card" and "setsum" + fix incorrect outcome code w.r.t. "bisim_depth = -1"
blanchet
parents: 35665
diff changeset
   614
    (* bool -> KK.raw_bound list -> problem_extension -> bool * bool option *)
33192
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   615
    fun print_and_check_model genuine bounds
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   616
            ({free_names, sel_names, nonsel_names, rel_table, scope, ...}
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   617
             : problem_extension) =
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   618
      let
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   619
        val (reconstructed_model, codatatypes_ok) =
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   620
          reconstruct_hol_model {show_skolems = show_skolems,
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   621
                                 show_datatypes = show_datatypes,
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   622
                                 show_consts = show_consts}
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   623
              scope formats frees free_names sel_names nonsel_names rel_table
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   624
              bounds
35671
ed2c3830d881 improved Nitpick's precision for "card" and "setsum" + fix incorrect outcome code w.r.t. "bisim_depth = -1"
blanchet
parents: 35665
diff changeset
   625
        val genuine_means_genuine =
ed2c3830d881 improved Nitpick's precision for "card" and "setsum" + fix incorrect outcome code w.r.t. "bisim_depth = -1"
blanchet
parents: 35665
diff changeset
   626
          got_all_user_axioms andalso none_true wfs andalso
ed2c3830d881 improved Nitpick's precision for "card" and "setsum" + fix incorrect outcome code w.r.t. "bisim_depth = -1"
blanchet
parents: 35665
diff changeset
   627
          sound_finitizes andalso codatatypes_ok
33192
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   628
      in
35671
ed2c3830d881 improved Nitpick's precision for "card" and "setsum" + fix incorrect outcome code w.r.t. "bisim_depth = -1"
blanchet
parents: 35665
diff changeset
   629
        (pprint (Pretty.chunks
ed2c3830d881 improved Nitpick's precision for "card" and "setsum" + fix incorrect outcome code w.r.t. "bisim_depth = -1"
blanchet
parents: 35665
diff changeset
   630
             [Pretty.blk (0,
ed2c3830d881 improved Nitpick's precision for "card" and "setsum" + fix incorrect outcome code w.r.t. "bisim_depth = -1"
blanchet
parents: 35665
diff changeset
   631
                  (pstrs ("Nitpick found a" ^
ed2c3830d881 improved Nitpick's precision for "card" and "setsum" + fix incorrect outcome code w.r.t. "bisim_depth = -1"
blanchet
parents: 35665
diff changeset
   632
                          (if not genuine then " potential "
ed2c3830d881 improved Nitpick's precision for "card" and "setsum" + fix incorrect outcome code w.r.t. "bisim_depth = -1"
blanchet
parents: 35665
diff changeset
   633
                           else if genuine_means_genuine then " "
ed2c3830d881 improved Nitpick's precision for "card" and "setsum" + fix incorrect outcome code w.r.t. "bisim_depth = -1"
blanchet
parents: 35665
diff changeset
   634
                           else " quasi genuine ") ^ das_wort_model) @
ed2c3830d881 improved Nitpick's precision for "card" and "setsum" + fix incorrect outcome code w.r.t. "bisim_depth = -1"
blanchet
parents: 35665
diff changeset
   635
                   (case pretties_for_scope scope verbose of
ed2c3830d881 improved Nitpick's precision for "card" and "setsum" + fix incorrect outcome code w.r.t. "bisim_depth = -1"
blanchet
parents: 35665
diff changeset
   636
                      [] => []
ed2c3830d881 improved Nitpick's precision for "card" and "setsum" + fix incorrect outcome code w.r.t. "bisim_depth = -1"
blanchet
parents: 35665
diff changeset
   637
                    | pretties => pstrs " for " @ pretties) @
ed2c3830d881 improved Nitpick's precision for "card" and "setsum" + fix incorrect outcome code w.r.t. "bisim_depth = -1"
blanchet
parents: 35665
diff changeset
   638
                   [Pretty.str ":\n"])),
ed2c3830d881 improved Nitpick's precision for "card" and "setsum" + fix incorrect outcome code w.r.t. "bisim_depth = -1"
blanchet
parents: 35665
diff changeset
   639
              Pretty.indent indent_size reconstructed_model]);
ed2c3830d881 improved Nitpick's precision for "card" and "setsum" + fix incorrect outcome code w.r.t. "bisim_depth = -1"
blanchet
parents: 35665
diff changeset
   640
         if genuine then
ed2c3830d881 improved Nitpick's precision for "card" and "setsum" + fix incorrect outcome code w.r.t. "bisim_depth = -1"
blanchet
parents: 35665
diff changeset
   641
           (if check_genuine andalso standard then
ed2c3830d881 improved Nitpick's precision for "card" and "setsum" + fix incorrect outcome code w.r.t. "bisim_depth = -1"
blanchet
parents: 35665
diff changeset
   642
              case prove_hol_model scope tac_timeout free_names sel_names
33192
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   643
                                   rel_table bounds assms_t of
35671
ed2c3830d881 improved Nitpick's precision for "card" and "setsum" + fix incorrect outcome code w.r.t. "bisim_depth = -1"
blanchet
parents: 35665
diff changeset
   644
                SOME true =>
ed2c3830d881 improved Nitpick's precision for "card" and "setsum" + fix incorrect outcome code w.r.t. "bisim_depth = -1"
blanchet
parents: 35665
diff changeset
   645
                print ("Confirmation by \"auto\": The above " ^
ed2c3830d881 improved Nitpick's precision for "card" and "setsum" + fix incorrect outcome code w.r.t. "bisim_depth = -1"
blanchet
parents: 35665
diff changeset
   646
                       das_wort_model ^ " is really genuine.")
33192
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   647
              | SOME false =>
34982
7b8c366e34a2 added support for nonstandard models to Nitpick (based on an idea by Koen Claessen) and did other fixes to Nitpick
blanchet
parents: 34938
diff changeset
   648
                if genuine_means_genuine then
7b8c366e34a2 added support for nonstandard models to Nitpick (based on an idea by Koen Claessen) and did other fixes to Nitpick
blanchet
parents: 34938
diff changeset
   649
                  error ("A supposedly genuine " ^ das_wort_model ^ " was \
7b8c366e34a2 added support for nonstandard models to Nitpick (based on an idea by Koen Claessen) and did other fixes to Nitpick
blanchet
parents: 34938
diff changeset
   650
                         \shown to be spurious by \"auto\".\nThis should never \
7b8c366e34a2 added support for nonstandard models to Nitpick (based on an idea by Koen Claessen) and did other fixes to Nitpick
blanchet
parents: 34938
diff changeset
   651
                         \happen.\nPlease send a bug report to blanchet\
33192
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   652
                         \te@in.tum.de.")
35671
ed2c3830d881 improved Nitpick's precision for "card" and "setsum" + fix incorrect outcome code w.r.t. "bisim_depth = -1"
blanchet
parents: 35665
diff changeset
   653
                 else
ed2c3830d881 improved Nitpick's precision for "card" and "setsum" + fix incorrect outcome code w.r.t. "bisim_depth = -1"
blanchet
parents: 35665
diff changeset
   654
                   print ("Refutation by \"auto\": The above " ^
ed2c3830d881 improved Nitpick's precision for "card" and "setsum" + fix incorrect outcome code w.r.t. "bisim_depth = -1"
blanchet
parents: 35665
diff changeset
   655
                          das_wort_model ^ " is spurious.")
ed2c3830d881 improved Nitpick's precision for "card" and "setsum" + fix incorrect outcome code w.r.t. "bisim_depth = -1"
blanchet
parents: 35665
diff changeset
   656
               | NONE => print "No confirmation by \"auto\"."
ed2c3830d881 improved Nitpick's precision for "card" and "setsum" + fix incorrect outcome code w.r.t. "bisim_depth = -1"
blanchet
parents: 35665
diff changeset
   657
            else
ed2c3830d881 improved Nitpick's precision for "card" and "setsum" + fix incorrect outcome code w.r.t. "bisim_depth = -1"
blanchet
parents: 35665
diff changeset
   658
              ();
ed2c3830d881 improved Nitpick's precision for "card" and "setsum" + fix incorrect outcome code w.r.t. "bisim_depth = -1"
blanchet
parents: 35665
diff changeset
   659
            if not standard andalso likely_in_struct_induct_step then
ed2c3830d881 improved Nitpick's precision for "card" and "setsum" + fix incorrect outcome code w.r.t. "bisim_depth = -1"
blanchet
parents: 35665
diff changeset
   660
              print "The existence of a nonstandard model suggests that the \
36126
00d550b6cfd4 cosmetics
blanchet
parents: 35968
diff changeset
   661
                    \induction hypothesis is not general enough or may even be \
00d550b6cfd4 cosmetics
blanchet
parents: 35968
diff changeset
   662
                    \wrong. See the Nitpick manual's \"Inductive Properties\" \
00d550b6cfd4 cosmetics
blanchet
parents: 35968
diff changeset
   663
                    \section for details (\"isabelle doc nitpick\")."
35671
ed2c3830d881 improved Nitpick's precision for "card" and "setsum" + fix incorrect outcome code w.r.t. "bisim_depth = -1"
blanchet
parents: 35665
diff changeset
   664
            else
ed2c3830d881 improved Nitpick's precision for "card" and "setsum" + fix incorrect outcome code w.r.t. "bisim_depth = -1"
blanchet
parents: 35665
diff changeset
   665
              ();
ed2c3830d881 improved Nitpick's precision for "card" and "setsum" + fix incorrect outcome code w.r.t. "bisim_depth = -1"
blanchet
parents: 35665
diff changeset
   666
            if has_syntactic_sorts orig_t then
ed2c3830d881 improved Nitpick's precision for "card" and "setsum" + fix incorrect outcome code w.r.t. "bisim_depth = -1"
blanchet
parents: 35665
diff changeset
   667
              print "Hint: Maybe you forgot a type constraint?"
ed2c3830d881 improved Nitpick's precision for "card" and "setsum" + fix incorrect outcome code w.r.t. "bisim_depth = -1"
blanchet
parents: 35665
diff changeset
   668
            else
ed2c3830d881 improved Nitpick's precision for "card" and "setsum" + fix incorrect outcome code w.r.t. "bisim_depth = -1"
blanchet
parents: 35665
diff changeset
   669
              ();
ed2c3830d881 improved Nitpick's precision for "card" and "setsum" + fix incorrect outcome code w.r.t. "bisim_depth = -1"
blanchet
parents: 35665
diff changeset
   670
            if not genuine_means_genuine then
ed2c3830d881 improved Nitpick's precision for "card" and "setsum" + fix incorrect outcome code w.r.t. "bisim_depth = -1"
blanchet
parents: 35665
diff changeset
   671
              if no_poly_user_axioms then
ed2c3830d881 improved Nitpick's precision for "card" and "setsum" + fix incorrect outcome code w.r.t. "bisim_depth = -1"
blanchet
parents: 35665
diff changeset
   672
                let
ed2c3830d881 improved Nitpick's precision for "card" and "setsum" + fix incorrect outcome code w.r.t. "bisim_depth = -1"
blanchet
parents: 35665
diff changeset
   673
                  val options =
ed2c3830d881 improved Nitpick's precision for "card" and "setsum" + fix incorrect outcome code w.r.t. "bisim_depth = -1"
blanchet
parents: 35665
diff changeset
   674
                    [] |> not got_all_mono_user_axioms
ed2c3830d881 improved Nitpick's precision for "card" and "setsum" + fix incorrect outcome code w.r.t. "bisim_depth = -1"
blanchet
parents: 35665
diff changeset
   675
                          ? cons ("user_axioms", "\"true\"")
ed2c3830d881 improved Nitpick's precision for "card" and "setsum" + fix incorrect outcome code w.r.t. "bisim_depth = -1"
blanchet
parents: 35665
diff changeset
   676
                       |> not (none_true wfs)
ed2c3830d881 improved Nitpick's precision for "card" and "setsum" + fix incorrect outcome code w.r.t. "bisim_depth = -1"
blanchet
parents: 35665
diff changeset
   677
                          ? cons ("wf", "\"smart\" or \"false\"")
ed2c3830d881 improved Nitpick's precision for "card" and "setsum" + fix incorrect outcome code w.r.t. "bisim_depth = -1"
blanchet
parents: 35665
diff changeset
   678
                       |> not sound_finitizes
ed2c3830d881 improved Nitpick's precision for "card" and "setsum" + fix incorrect outcome code w.r.t. "bisim_depth = -1"
blanchet
parents: 35665
diff changeset
   679
                          ? cons ("finitize", "\"smart\" or \"false\"")
ed2c3830d881 improved Nitpick's precision for "card" and "setsum" + fix incorrect outcome code w.r.t. "bisim_depth = -1"
blanchet
parents: 35665
diff changeset
   680
                       |> not codatatypes_ok
ed2c3830d881 improved Nitpick's precision for "card" and "setsum" + fix incorrect outcome code w.r.t. "bisim_depth = -1"
blanchet
parents: 35665
diff changeset
   681
                          ? cons ("bisim_depth", "a nonnegative value")
ed2c3830d881 improved Nitpick's precision for "card" and "setsum" + fix incorrect outcome code w.r.t. "bisim_depth = -1"
blanchet
parents: 35665
diff changeset
   682
                  val ss =
ed2c3830d881 improved Nitpick's precision for "card" and "setsum" + fix incorrect outcome code w.r.t. "bisim_depth = -1"
blanchet
parents: 35665
diff changeset
   683
                    map (fn (name, value) => quote name ^ " set to " ^ value)
ed2c3830d881 improved Nitpick's precision for "card" and "setsum" + fix incorrect outcome code w.r.t. "bisim_depth = -1"
blanchet
parents: 35665
diff changeset
   684
                        options
ed2c3830d881 improved Nitpick's precision for "card" and "setsum" + fix incorrect outcome code w.r.t. "bisim_depth = -1"
blanchet
parents: 35665
diff changeset
   685
                in
ed2c3830d881 improved Nitpick's precision for "card" and "setsum" + fix incorrect outcome code w.r.t. "bisim_depth = -1"
blanchet
parents: 35665
diff changeset
   686
                  print ("Try again with " ^
35968
b7f98ff9c7d9 simplify Nitpick parameter parsing code a little bit + make compile
blanchet
parents: 35814
diff changeset
   687
                         space_implode " "
b7f98ff9c7d9 simplify Nitpick parameter parsing code a little bit + make compile
blanchet
parents: 35814
diff changeset
   688
                             (Sledgehammer_Util.serial_commas "and" ss) ^
35671
ed2c3830d881 improved Nitpick's precision for "card" and "setsum" + fix incorrect outcome code w.r.t. "bisim_depth = -1"
blanchet
parents: 35665
diff changeset
   689
                         " to confirm that the " ^ das_wort_model ^
ed2c3830d881 improved Nitpick's precision for "card" and "setsum" + fix incorrect outcome code w.r.t. "bisim_depth = -1"
blanchet
parents: 35665
diff changeset
   690
                         " is genuine.")
ed2c3830d881 improved Nitpick's precision for "card" and "setsum" + fix incorrect outcome code w.r.t. "bisim_depth = -1"
blanchet
parents: 35665
diff changeset
   691
                end
ed2c3830d881 improved Nitpick's precision for "card" and "setsum" + fix incorrect outcome code w.r.t. "bisim_depth = -1"
blanchet
parents: 35665
diff changeset
   692
              else
ed2c3830d881 improved Nitpick's precision for "card" and "setsum" + fix incorrect outcome code w.r.t. "bisim_depth = -1"
blanchet
parents: 35665
diff changeset
   693
                print ("Nitpick is unable to guarantee the authenticity of \
ed2c3830d881 improved Nitpick's precision for "card" and "setsum" + fix incorrect outcome code w.r.t. "bisim_depth = -1"
blanchet
parents: 35665
diff changeset
   694
                       \the " ^ das_wort_model ^ " in the presence of \
ed2c3830d881 improved Nitpick's precision for "card" and "setsum" + fix incorrect outcome code w.r.t. "bisim_depth = -1"
blanchet
parents: 35665
diff changeset
   695
                       \polymorphic axioms.")
ed2c3830d881 improved Nitpick's precision for "card" and "setsum" + fix incorrect outcome code w.r.t. "bisim_depth = -1"
blanchet
parents: 35665
diff changeset
   696
            else
ed2c3830d881 improved Nitpick's precision for "card" and "setsum" + fix incorrect outcome code w.r.t. "bisim_depth = -1"
blanchet
parents: 35665
diff changeset
   697
              ();
ed2c3830d881 improved Nitpick's precision for "card" and "setsum" + fix incorrect outcome code w.r.t. "bisim_depth = -1"
blanchet
parents: 35665
diff changeset
   698
            NONE)
ed2c3830d881 improved Nitpick's precision for "card" and "setsum" + fix incorrect outcome code w.r.t. "bisim_depth = -1"
blanchet
parents: 35665
diff changeset
   699
         else
ed2c3830d881 improved Nitpick's precision for "card" and "setsum" + fix incorrect outcome code w.r.t. "bisim_depth = -1"
blanchet
parents: 35665
diff changeset
   700
           if not genuine then
ed2c3830d881 improved Nitpick's precision for "card" and "setsum" + fix incorrect outcome code w.r.t. "bisim_depth = -1"
blanchet
parents: 35665
diff changeset
   701
             (Unsynchronized.inc met_potential;
ed2c3830d881 improved Nitpick's precision for "card" and "setsum" + fix incorrect outcome code w.r.t. "bisim_depth = -1"
blanchet
parents: 35665
diff changeset
   702
              if check_potential then
ed2c3830d881 improved Nitpick's precision for "card" and "setsum" + fix incorrect outcome code w.r.t. "bisim_depth = -1"
blanchet
parents: 35665
diff changeset
   703
                let
ed2c3830d881 improved Nitpick's precision for "card" and "setsum" + fix incorrect outcome code w.r.t. "bisim_depth = -1"
blanchet
parents: 35665
diff changeset
   704
                  val status = prove_hol_model scope tac_timeout free_names
ed2c3830d881 improved Nitpick's precision for "card" and "setsum" + fix incorrect outcome code w.r.t. "bisim_depth = -1"
blanchet
parents: 35665
diff changeset
   705
                                              sel_names rel_table bounds assms_t
ed2c3830d881 improved Nitpick's precision for "card" and "setsum" + fix incorrect outcome code w.r.t. "bisim_depth = -1"
blanchet
parents: 35665
diff changeset
   706
                in
ed2c3830d881 improved Nitpick's precision for "card" and "setsum" + fix incorrect outcome code w.r.t. "bisim_depth = -1"
blanchet
parents: 35665
diff changeset
   707
                  (case status of
ed2c3830d881 improved Nitpick's precision for "card" and "setsum" + fix incorrect outcome code w.r.t. "bisim_depth = -1"
blanchet
parents: 35665
diff changeset
   708
                     SOME true => print ("Confirmation by \"auto\": The \
ed2c3830d881 improved Nitpick's precision for "card" and "setsum" + fix incorrect outcome code w.r.t. "bisim_depth = -1"
blanchet
parents: 35665
diff changeset
   709
                                         \above " ^ das_wort_model ^
ed2c3830d881 improved Nitpick's precision for "card" and "setsum" + fix incorrect outcome code w.r.t. "bisim_depth = -1"
blanchet
parents: 35665
diff changeset
   710
                                         " is genuine.")
ed2c3830d881 improved Nitpick's precision for "card" and "setsum" + fix incorrect outcome code w.r.t. "bisim_depth = -1"
blanchet
parents: 35665
diff changeset
   711
                   | SOME false => print ("Refutation by \"auto\": The above " ^
ed2c3830d881 improved Nitpick's precision for "card" and "setsum" + fix incorrect outcome code w.r.t. "bisim_depth = -1"
blanchet
parents: 35665
diff changeset
   712
                                          das_wort_model ^ " is spurious.")
ed2c3830d881 improved Nitpick's precision for "card" and "setsum" + fix incorrect outcome code w.r.t. "bisim_depth = -1"
blanchet
parents: 35665
diff changeset
   713
                   | NONE => print "No confirmation by \"auto\".");
ed2c3830d881 improved Nitpick's precision for "card" and "setsum" + fix incorrect outcome code w.r.t. "bisim_depth = -1"
blanchet
parents: 35665
diff changeset
   714
                  status
ed2c3830d881 improved Nitpick's precision for "card" and "setsum" + fix incorrect outcome code w.r.t. "bisim_depth = -1"
blanchet
parents: 35665
diff changeset
   715
                end
ed2c3830d881 improved Nitpick's precision for "card" and "setsum" + fix incorrect outcome code w.r.t. "bisim_depth = -1"
blanchet
parents: 35665
diff changeset
   716
              else
ed2c3830d881 improved Nitpick's precision for "card" and "setsum" + fix incorrect outcome code w.r.t. "bisim_depth = -1"
blanchet
parents: 35665
diff changeset
   717
                NONE)
33192
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   718
           else
35671
ed2c3830d881 improved Nitpick's precision for "card" and "setsum" + fix incorrect outcome code w.r.t. "bisim_depth = -1"
blanchet
parents: 35665
diff changeset
   719
             NONE)
ed2c3830d881 improved Nitpick's precision for "card" and "setsum" + fix incorrect outcome code w.r.t. "bisim_depth = -1"
blanchet
parents: 35665
diff changeset
   720
        |> pair genuine_means_genuine
33192
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   721
      end
35671
ed2c3830d881 improved Nitpick's precision for "card" and "setsum" + fix incorrect outcome code w.r.t. "bisim_depth = -1"
blanchet
parents: 35665
diff changeset
   722
    (* bool * int * int * int -> bool -> rich_problem list
ed2c3830d881 improved Nitpick's precision for "card" and "setsum" + fix incorrect outcome code w.r.t. "bisim_depth = -1"
blanchet
parents: 35665
diff changeset
   723
       -> bool * int * int * int *)
ed2c3830d881 improved Nitpick's precision for "card" and "setsum" + fix incorrect outcome code w.r.t. "bisim_depth = -1"
blanchet
parents: 35665
diff changeset
   724
    fun solve_any_problem (found_really_genuine, max_potential, max_genuine,
ed2c3830d881 improved Nitpick's precision for "card" and "setsum" + fix incorrect outcome code w.r.t. "bisim_depth = -1"
blanchet
parents: 35665
diff changeset
   725
                           donno) first_time problems =
33192
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   726
      let
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   727
        val max_potential = Int.max (0, max_potential)
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   728
        val max_genuine = Int.max (0, max_genuine)
35671
ed2c3830d881 improved Nitpick's precision for "card" and "setsum" + fix incorrect outcome code w.r.t. "bisim_depth = -1"
blanchet
parents: 35665
diff changeset
   729
        (* bool -> int * KK.raw_bound list -> bool * bool option *)
33192
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   730
        fun print_and_check genuine (j, bounds) =
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   731
          print_and_check_model genuine bounds (snd (nth problems j))
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   732
        val max_solutions = max_potential + max_genuine
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   733
                            |> not need_incremental ? curry Int.min 1
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   734
      in
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   735
        if max_solutions <= 0 then
35671
ed2c3830d881 improved Nitpick's precision for "card" and "setsum" + fix incorrect outcome code w.r.t. "bisim_depth = -1"
blanchet
parents: 35665
diff changeset
   736
          (found_really_genuine, 0, 0, donno)
33192
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   737
        else
34126
8a2c5d7aff51 polished Nitpick's binary integer support etc.;
blanchet
parents: 34124
diff changeset
   738
          case KK.solve_any_problem overlord deadline max_threads max_solutions
8a2c5d7aff51 polished Nitpick's binary integer support etc.;
blanchet
parents: 34124
diff changeset
   739
                                    (map fst problems) of
35696
17ae461d6133 show nice error message in Nitpick when "java" is not available
blanchet
parents: 35671
diff changeset
   740
            KK.JavaNotInstalled =>
17ae461d6133 show nice error message in Nitpick when "java" is not available
blanchet
parents: 35671
diff changeset
   741
            (print_m install_java_message;
17ae461d6133 show nice error message in Nitpick when "java" is not available
blanchet
parents: 35671
diff changeset
   742
             (found_really_genuine, max_potential, max_genuine, donno + 1))
17ae461d6133 show nice error message in Nitpick when "java" is not available
blanchet
parents: 35671
diff changeset
   743
          | KK.KodkodiNotInstalled =>
33568
532b915afa14 don't run Nitpick at all if Kodkodi is not installed (as indicated by the $KODKODI variable)
blanchet
parents: 33566
diff changeset
   744
            (print_m install_kodkodi_message;
35671
ed2c3830d881 improved Nitpick's precision for "card" and "setsum" + fix incorrect outcome code w.r.t. "bisim_depth = -1"
blanchet
parents: 35665
diff changeset
   745
             (found_really_genuine, max_potential, max_genuine, donno + 1))
35333
f61de25f71f9 distinguish between Kodkodi warnings and errors in Nitpick;
blanchet
parents: 35280
diff changeset
   746
          | KK.Normal ([], unsat_js, s) =>
f61de25f71f9 distinguish between Kodkodi warnings and errors in Nitpick;
blanchet
parents: 35280
diff changeset
   747
            (update_checked_problems problems unsat_js; show_kodkod_warning s;
35671
ed2c3830d881 improved Nitpick's precision for "card" and "setsum" + fix incorrect outcome code w.r.t. "bisim_depth = -1"
blanchet
parents: 35665
diff changeset
   748
             (found_really_genuine, max_potential, max_genuine, donno))
35333
f61de25f71f9 distinguish between Kodkodi warnings and errors in Nitpick;
blanchet
parents: 35280
diff changeset
   749
          | KK.Normal (sat_ps, unsat_js, s) =>
33192
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   750
            let
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   751
              val (lib_ps, con_ps) =
35185
9b8f351cced6 added yet another hint to Nitpick's output, this time warning about problems for which nothing was effectively tested
blanchet
parents: 35183
diff changeset
   752
                List.partition (#unsound o snd o nth problems o fst) sat_ps
33192
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   753
            in
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   754
              update_checked_problems problems (unsat_js @ map fst lib_ps);
35333
f61de25f71f9 distinguish between Kodkodi warnings and errors in Nitpick;
blanchet
parents: 35280
diff changeset
   755
              show_kodkod_warning s;
33192
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   756
              if null con_ps then
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   757
                let
35671
ed2c3830d881 improved Nitpick's precision for "card" and "setsum" + fix incorrect outcome code w.r.t. "bisim_depth = -1"
blanchet
parents: 35665
diff changeset
   758
                  val genuine_codes =
ed2c3830d881 improved Nitpick's precision for "card" and "setsum" + fix incorrect outcome code w.r.t. "bisim_depth = -1"
blanchet
parents: 35665
diff changeset
   759
                    lib_ps |> take max_potential
ed2c3830d881 improved Nitpick's precision for "card" and "setsum" + fix incorrect outcome code w.r.t. "bisim_depth = -1"
blanchet
parents: 35665
diff changeset
   760
                           |> map (print_and_check false)
ed2c3830d881 improved Nitpick's precision for "card" and "setsum" + fix incorrect outcome code w.r.t. "bisim_depth = -1"
blanchet
parents: 35665
diff changeset
   761
                           |> filter (curry (op =) (SOME true) o snd)
ed2c3830d881 improved Nitpick's precision for "card" and "setsum" + fix incorrect outcome code w.r.t. "bisim_depth = -1"
blanchet
parents: 35665
diff changeset
   762
                  val found_really_genuine =
ed2c3830d881 improved Nitpick's precision for "card" and "setsum" + fix incorrect outcome code w.r.t. "bisim_depth = -1"
blanchet
parents: 35665
diff changeset
   763
                    found_really_genuine orelse exists fst genuine_codes
ed2c3830d881 improved Nitpick's precision for "card" and "setsum" + fix incorrect outcome code w.r.t. "bisim_depth = -1"
blanchet
parents: 35665
diff changeset
   764
                  val num_genuine = length genuine_codes
33192
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   765
                  val max_genuine = max_genuine - num_genuine
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   766
                  val max_potential = max_potential
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   767
                                      - (length lib_ps - num_genuine)
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   768
                in
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   769
                  if max_genuine <= 0 then
35671
ed2c3830d881 improved Nitpick's precision for "card" and "setsum" + fix incorrect outcome code w.r.t. "bisim_depth = -1"
blanchet
parents: 35665
diff changeset
   770
                    (found_really_genuine, 0, 0, donno)
33192
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   771
                  else
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   772
                    let
35185
9b8f351cced6 added yet another hint to Nitpick's output, this time warning about problems for which nothing was effectively tested
blanchet
parents: 35183
diff changeset
   773
                      (* "co_js" is the list of sound problems whose unsound
9b8f351cced6 added yet another hint to Nitpick's output, this time warning about problems for which nothing was effectively tested
blanchet
parents: 35183
diff changeset
   774
                         pendants couldn't be satisfied and hence that most
9b8f351cced6 added yet another hint to Nitpick's output, this time warning about problems for which nothing was effectively tested
blanchet
parents: 35183
diff changeset
   775
                         probably can't be satisfied themselves. *)
33192
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   776
                      val co_js =
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   777
                        map (fn j => j - 1) unsat_js
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   778
                        |> filter (fn j =>
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   779
                                      j >= 0 andalso
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   780
                                      scopes_equivalent
35814
234eaa508359 added one-entry cache around Kodkod invocation
blanchet
parents: 35807
diff changeset
   781
                                          (#scope (snd (nth problems j)),
234eaa508359 added one-entry cache around Kodkod invocation
blanchet
parents: 35807
diff changeset
   782
                                           #scope (snd (nth problems (j + 1)))))
33192
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   783
                      val bye_js = sort_distinct int_ord (map fst sat_ps @
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   784
                                                          unsat_js @ co_js)
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   785
                      val problems =
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   786
                        problems |> filter_out_indices bye_js
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   787
                                 |> max_potential <= 0
35185
9b8f351cced6 added yet another hint to Nitpick's output, this time warning about problems for which nothing was effectively tested
blanchet
parents: 35183
diff changeset
   788
                                    ? filter_out (#unsound o snd)
33192
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   789
                    in
35671
ed2c3830d881 improved Nitpick's precision for "card" and "setsum" + fix incorrect outcome code w.r.t. "bisim_depth = -1"
blanchet
parents: 35665
diff changeset
   790
                      solve_any_problem (found_really_genuine, max_potential,
ed2c3830d881 improved Nitpick's precision for "card" and "setsum" + fix incorrect outcome code w.r.t. "bisim_depth = -1"
blanchet
parents: 35665
diff changeset
   791
                                         max_genuine, donno) false problems
33192
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   792
                    end
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   793
                end
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   794
              else
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   795
                let
35671
ed2c3830d881 improved Nitpick's precision for "card" and "setsum" + fix incorrect outcome code w.r.t. "bisim_depth = -1"
blanchet
parents: 35665
diff changeset
   796
                  val genuine_codes =
ed2c3830d881 improved Nitpick's precision for "card" and "setsum" + fix incorrect outcome code w.r.t. "bisim_depth = -1"
blanchet
parents: 35665
diff changeset
   797
                    con_ps |> take max_genuine
ed2c3830d881 improved Nitpick's precision for "card" and "setsum" + fix incorrect outcome code w.r.t. "bisim_depth = -1"
blanchet
parents: 35665
diff changeset
   798
                           |> map (print_and_check true)
ed2c3830d881 improved Nitpick's precision for "card" and "setsum" + fix incorrect outcome code w.r.t. "bisim_depth = -1"
blanchet
parents: 35665
diff changeset
   799
                  val max_genuine = max_genuine - length genuine_codes
ed2c3830d881 improved Nitpick's precision for "card" and "setsum" + fix incorrect outcome code w.r.t. "bisim_depth = -1"
blanchet
parents: 35665
diff changeset
   800
                  val found_really_genuine =
ed2c3830d881 improved Nitpick's precision for "card" and "setsum" + fix incorrect outcome code w.r.t. "bisim_depth = -1"
blanchet
parents: 35665
diff changeset
   801
                    found_really_genuine orelse exists fst genuine_codes
33192
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   802
                in
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   803
                  if max_genuine <= 0 orelse not first_time then
35671
ed2c3830d881 improved Nitpick's precision for "card" and "setsum" + fix incorrect outcome code w.r.t. "bisim_depth = -1"
blanchet
parents: 35665
diff changeset
   804
                    (found_really_genuine, 0, max_genuine, donno)
33192
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   805
                  else
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   806
                    let
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   807
                      val bye_js = sort_distinct int_ord
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   808
                                                 (map fst sat_ps @ unsat_js)
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   809
                      val problems =
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   810
                        problems |> filter_out_indices bye_js
35185
9b8f351cced6 added yet another hint to Nitpick's output, this time warning about problems for which nothing was effectively tested
blanchet
parents: 35183
diff changeset
   811
                                 |> filter_out (#unsound o snd)
35671
ed2c3830d881 improved Nitpick's precision for "card" and "setsum" + fix incorrect outcome code w.r.t. "bisim_depth = -1"
blanchet
parents: 35665
diff changeset
   812
                    in
ed2c3830d881 improved Nitpick's precision for "card" and "setsum" + fix incorrect outcome code w.r.t. "bisim_depth = -1"
blanchet
parents: 35665
diff changeset
   813
                      solve_any_problem (found_really_genuine, 0, max_genuine,
ed2c3830d881 improved Nitpick's precision for "card" and "setsum" + fix incorrect outcome code w.r.t. "bisim_depth = -1"
blanchet
parents: 35665
diff changeset
   814
                                         donno) false problems
ed2c3830d881 improved Nitpick's precision for "card" and "setsum" + fix incorrect outcome code w.r.t. "bisim_depth = -1"
blanchet
parents: 35665
diff changeset
   815
                    end
33192
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   816
                end
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   817
            end
34126
8a2c5d7aff51 polished Nitpick's binary integer support etc.;
blanchet
parents: 34124
diff changeset
   818
          | KK.TimedOut unsat_js =>
33192
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   819
            (update_checked_problems problems unsat_js; raise TimeLimit.TimeOut)
34126
8a2c5d7aff51 polished Nitpick's binary integer support etc.;
blanchet
parents: 34124
diff changeset
   820
          | KK.Interrupted NONE => (checked_problems := NONE; do_interrupted ())
8a2c5d7aff51 polished Nitpick's binary integer support etc.;
blanchet
parents: 34124
diff changeset
   821
          | KK.Interrupted (SOME unsat_js) =>
33192
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   822
            (update_checked_problems problems unsat_js; do_interrupted ())
34126
8a2c5d7aff51 polished Nitpick's binary integer support etc.;
blanchet
parents: 34124
diff changeset
   823
          | KK.Error (s, unsat_js) =>
33192
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   824
            (update_checked_problems problems unsat_js;
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   825
             print_v (K ("Kodkod error: " ^ s ^ "."));
35671
ed2c3830d881 improved Nitpick's precision for "card" and "setsum" + fix incorrect outcome code w.r.t. "bisim_depth = -1"
blanchet
parents: 35665
diff changeset
   826
             (found_really_genuine, max_potential, max_genuine, donno + 1))
33192
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   827
      end
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   828
35671
ed2c3830d881 improved Nitpick's precision for "card" and "setsum" + fix incorrect outcome code w.r.t. "bisim_depth = -1"
blanchet
parents: 35665
diff changeset
   829
    (* int -> int -> scope list -> bool * int * int * int
ed2c3830d881 improved Nitpick's precision for "card" and "setsum" + fix incorrect outcome code w.r.t. "bisim_depth = -1"
blanchet
parents: 35665
diff changeset
   830
       -> bool * int * int * int *)
ed2c3830d881 improved Nitpick's precision for "card" and "setsum" + fix incorrect outcome code w.r.t. "bisim_depth = -1"
blanchet
parents: 35665
diff changeset
   831
    fun run_batch j n scopes (found_really_genuine, max_potential, max_genuine,
ed2c3830d881 improved Nitpick's precision for "card" and "setsum" + fix incorrect outcome code w.r.t. "bisim_depth = -1"
blanchet
parents: 35665
diff changeset
   832
                              donno) =
33192
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   833
      let
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   834
        val _ =
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   835
          if null scopes then
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   836
            print_m (K "The scope specification is inconsistent.")
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   837
          else if verbose then
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   838
            pprint (Pretty.chunks
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   839
                [Pretty.blk (0,
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   840
                     pstrs ((if n > 1 then
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   841
                               "Batch " ^ string_of_int (j + 1) ^ " of " ^
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   842
                               signed_string_of_int n ^ ": "
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   843
                             else
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   844
                               "") ^
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   845
                            "Trying " ^ string_of_int (length scopes) ^
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   846
                            " scope" ^ plural_s_for_list scopes ^ ":")),
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   847
                 Pretty.indent indent_size
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   848
                     (Pretty.chunks (map2
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   849
                          (fn j => fn scope =>
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   850
                              Pretty.block (
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   851
                                  (case pretties_for_scope scope true of
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   852
                                     [] => [Pretty.str "Empty"]
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   853
                                   | pretties => pretties) @
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   854
                                  [Pretty.str (if j = 1 then "." else ";")]))
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   855
                          (length scopes downto 1) scopes))])
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   856
          else
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   857
            ()
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   858
        (* scope * bool -> rich_problem list * bool
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   859
           -> rich_problem list * bool *)
35280
54ab4921f826 fixed a few bugs in Nitpick and removed unreferenced variables
blanchet
parents: 35220
diff changeset
   860
        fun add_problem_for_scope (scope, unsound) (problems, donno) =
33192
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   861
          (check_deadline ();
35185
9b8f351cced6 added yet another hint to Nitpick's output, this time warning about problems for which nothing was effectively tested
blanchet
parents: 35183
diff changeset
   862
           case problem_for_scope unsound scope of
33192
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   863
             SOME problem =>
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   864
             (problems
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   865
              |> (null problems orelse
35814
234eaa508359 added one-entry cache around Kodkod invocation
blanchet
parents: 35807
diff changeset
   866
                  not (KK.problems_equivalent (fst problem, fst (hd problems))))
33192
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   867
                  ? cons problem, donno)
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   868
           | NONE => (problems, donno + 1))
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   869
        val (problems, donno) =
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   870
          fold add_problem_for_scope
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   871
               (map_product pair scopes
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   872
                    ((if max_genuine > 0 then [false] else []) @
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   873
                     (if max_potential > 0 then [true] else [])))
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   874
               ([], donno)
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   875
        val _ = Unsynchronized.change generated_problems (append problems)
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   876
        val _ = Unsynchronized.change generated_scopes (append scopes)
35185
9b8f351cced6 added yet another hint to Nitpick's output, this time warning about problems for which nothing was effectively tested
blanchet
parents: 35183
diff changeset
   877
        val _ =
9b8f351cced6 added yet another hint to Nitpick's output, this time warning about problems for which nothing was effectively tested
blanchet
parents: 35183
diff changeset
   878
          if j + 1 = n then
9b8f351cced6 added yet another hint to Nitpick's output, this time warning about problems for which nothing was effectively tested
blanchet
parents: 35183
diff changeset
   879
            let
9b8f351cced6 added yet another hint to Nitpick's output, this time warning about problems for which nothing was effectively tested
blanchet
parents: 35183
diff changeset
   880
              val (unsound_problems, sound_problems) =
9b8f351cced6 added yet another hint to Nitpick's output, this time warning about problems for which nothing was effectively tested
blanchet
parents: 35183
diff changeset
   881
                List.partition (#unsound o snd) (!generated_problems)
9b8f351cced6 added yet another hint to Nitpick's output, this time warning about problems for which nothing was effectively tested
blanchet
parents: 35183
diff changeset
   882
            in
9b8f351cced6 added yet another hint to Nitpick's output, this time warning about problems for which nothing was effectively tested
blanchet
parents: 35183
diff changeset
   883
              if not (null sound_problems) andalso
9b8f351cced6 added yet another hint to Nitpick's output, this time warning about problems for which nothing was effectively tested
blanchet
parents: 35183
diff changeset
   884
                 forall (KK.is_problem_trivially_false o fst)
9b8f351cced6 added yet another hint to Nitpick's output, this time warning about problems for which nothing was effectively tested
blanchet
parents: 35183
diff changeset
   885
                        sound_problems then
9b8f351cced6 added yet another hint to Nitpick's output, this time warning about problems for which nothing was effectively tested
blanchet
parents: 35183
diff changeset
   886
                print_m (fn () =>
35220
2bcdae5f4fdb added support for nonstandard "nat"s to Nitpick and fixed bugs in binary "nat"s and "int"s
blanchet
parents: 35190
diff changeset
   887
                    "Warning: The conjecture either trivially holds for the \
35384
88dbcfe75c45 cosmetics
blanchet
parents: 35335
diff changeset
   888
                    \given scopes or lies outside Nitpick's supported \
88dbcfe75c45 cosmetics
blanchet
parents: 35335
diff changeset
   889
                    \fragment." ^
35185
9b8f351cced6 added yet another hint to Nitpick's output, this time warning about problems for which nothing was effectively tested
blanchet
parents: 35183
diff changeset
   890
                    (if exists (not o KK.is_problem_trivially_false o fst)
9b8f351cced6 added yet another hint to Nitpick's output, this time warning about problems for which nothing was effectively tested
blanchet
parents: 35183
diff changeset
   891
                               unsound_problems then
9b8f351cced6 added yet another hint to Nitpick's output, this time warning about problems for which nothing was effectively tested
blanchet
parents: 35183
diff changeset
   892
                       " Only potential counterexamples may be found."
9b8f351cced6 added yet another hint to Nitpick's output, this time warning about problems for which nothing was effectively tested
blanchet
parents: 35183
diff changeset
   893
                     else
9b8f351cced6 added yet another hint to Nitpick's output, this time warning about problems for which nothing was effectively tested
blanchet
parents: 35183
diff changeset
   894
                       ""))
9b8f351cced6 added yet another hint to Nitpick's output, this time warning about problems for which nothing was effectively tested
blanchet
parents: 35183
diff changeset
   895
              else
9b8f351cced6 added yet another hint to Nitpick's output, this time warning about problems for which nothing was effectively tested
blanchet
parents: 35183
diff changeset
   896
                ()
9b8f351cced6 added yet another hint to Nitpick's output, this time warning about problems for which nothing was effectively tested
blanchet
parents: 35183
diff changeset
   897
            end
9b8f351cced6 added yet another hint to Nitpick's output, this time warning about problems for which nothing was effectively tested
blanchet
parents: 35183
diff changeset
   898
          else
9b8f351cced6 added yet another hint to Nitpick's output, this time warning about problems for which nothing was effectively tested
blanchet
parents: 35183
diff changeset
   899
            ()
33192
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   900
      in
35671
ed2c3830d881 improved Nitpick's precision for "card" and "setsum" + fix incorrect outcome code w.r.t. "bisim_depth = -1"
blanchet
parents: 35665
diff changeset
   901
        solve_any_problem (found_really_genuine, max_potential, max_genuine,
ed2c3830d881 improved Nitpick's precision for "card" and "setsum" + fix incorrect outcome code w.r.t. "bisim_depth = -1"
blanchet
parents: 35665
diff changeset
   902
                           donno) true (rev problems)
33192
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   903
      end
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   904
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   905
    (* rich_problem list -> scope -> int *)
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   906
    fun scope_count (problems : rich_problem list) scope =
35814
234eaa508359 added one-entry cache around Kodkod invocation
blanchet
parents: 35807
diff changeset
   907
      length (filter (curry scopes_equivalent scope o #scope o snd) problems)
33192
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   908
    (* string -> string *)
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   909
    fun excipit did_so_and_so =
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   910
      let
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   911
        (* rich_problem list -> rich_problem list *)
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   912
        val do_filter =
35185
9b8f351cced6 added yet another hint to Nitpick's output, this time warning about problems for which nothing was effectively tested
blanchet
parents: 35183
diff changeset
   913
          if !met_potential = max_potential then filter_out (#unsound o snd)
33192
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   914
          else I
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   915
        val total = length (!scopes)
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   916
        val unsat =
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   917
          fold (fn scope =>
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   918
                   case scope_count (do_filter (!generated_problems)) scope of
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   919
                     0 => I
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   920
                   | n =>
33556
cba22e2999d5 renamed Nitpick option "coalesce_type_vars" to "merge_type_vars" (shorter) and cleaned up old hacks that are no longer necessary
blanchet
parents: 33233
diff changeset
   921
                     scope_count (do_filter (these (!checked_problems)))
cba22e2999d5 renamed Nitpick option "coalesce_type_vars" to "merge_type_vars" (shorter) and cleaned up old hacks that are no longer necessary
blanchet
parents: 33233
diff changeset
   922
                                 scope = n
cba22e2999d5 renamed Nitpick option "coalesce_type_vars" to "merge_type_vars" (shorter) and cleaned up old hacks that are no longer necessary
blanchet
parents: 33233
diff changeset
   923
                     ? Integer.add 1) (!generated_scopes) 0
33192
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   924
      in
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   925
        "Nitpick " ^ did_so_and_so ^
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   926
        (if is_some (!checked_problems) andalso total > 0 then
35696
17ae461d6133 show nice error message in Nitpick when "java" is not available
blanchet
parents: 35671
diff changeset
   927
           " " ^ string_of_int (Int.min (total - 1, unsat)) ^ " of " ^
33192
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   928
           string_of_int total ^ " scope" ^ plural_s total
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   929
         else
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   930
           "") ^ "."
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   931
      end
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   932
35671
ed2c3830d881 improved Nitpick's precision for "card" and "setsum" + fix incorrect outcome code w.r.t. "bisim_depth = -1"
blanchet
parents: 35665
diff changeset
   933
    (* int -> int -> scope list -> bool * int * int * int -> KK.outcome *)
ed2c3830d881 improved Nitpick's precision for "card" and "setsum" + fix incorrect outcome code w.r.t. "bisim_depth = -1"
blanchet
parents: 35665
diff changeset
   934
    fun run_batches _ _ []
ed2c3830d881 improved Nitpick's precision for "card" and "setsum" + fix incorrect outcome code w.r.t. "bisim_depth = -1"
blanchet
parents: 35665
diff changeset
   935
                    (found_really_genuine, max_potential, max_genuine, donno) =
33192
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   936
        if donno > 0 andalso max_genuine > 0 then
35696
17ae461d6133 show nice error message in Nitpick when "java" is not available
blanchet
parents: 35671
diff changeset
   937
          (print_m (fn () => excipit "checked"); "unknown")
33192
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   938
        else if max_genuine = original_max_genuine then
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   939
          if max_potential = original_max_potential then
34982
7b8c366e34a2 added support for nonstandard models to Nitpick (based on an idea by Koen Claessen) and did other fixes to Nitpick
blanchet
parents: 34938
diff changeset
   940
            (print_m (fn () =>
7b8c366e34a2 added support for nonstandard models to Nitpick (based on an idea by Koen Claessen) and did other fixes to Nitpick
blanchet
parents: 34938
diff changeset
   941
                 "Nitpick found no " ^ das_wort_model ^ "." ^
35183
8580ba651489 reintroduce structural induction hint in Nitpick
blanchet
parents: 35181
diff changeset
   942
                 (if not standard andalso likely_in_struct_induct_step then
34982
7b8c366e34a2 added support for nonstandard models to Nitpick (based on an idea by Koen Claessen) and did other fixes to Nitpick
blanchet
parents: 34938
diff changeset
   943
                    " This suggests that the induction hypothesis might be \
7b8c366e34a2 added support for nonstandard models to Nitpick (based on an idea by Koen Claessen) and did other fixes to Nitpick
blanchet
parents: 34938
diff changeset
   944
                    \general enough to prove this subgoal."
7b8c366e34a2 added support for nonstandard models to Nitpick (based on an idea by Koen Claessen) and did other fixes to Nitpick
blanchet
parents: 34938
diff changeset
   945
                  else
7b8c366e34a2 added support for nonstandard models to Nitpick (based on an idea by Koen Claessen) and did other fixes to Nitpick
blanchet
parents: 34938
diff changeset
   946
                    "")); "none")
33192
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   947
          else
34982
7b8c366e34a2 added support for nonstandard models to Nitpick (based on an idea by Koen Claessen) and did other fixes to Nitpick
blanchet
parents: 34938
diff changeset
   948
            (print_m (fn () =>
7b8c366e34a2 added support for nonstandard models to Nitpick (based on an idea by Koen Claessen) and did other fixes to Nitpick
blanchet
parents: 34938
diff changeset
   949
                 "Nitpick could not find a" ^
7b8c366e34a2 added support for nonstandard models to Nitpick (based on an idea by Koen Claessen) and did other fixes to Nitpick
blanchet
parents: 34938
diff changeset
   950
                 (if max_genuine = 1 then " better " ^ das_wort_model ^ "."
7b8c366e34a2 added support for nonstandard models to Nitpick (based on an idea by Koen Claessen) and did other fixes to Nitpick
blanchet
parents: 34938
diff changeset
   951
                  else "ny better " ^ das_wort_model ^ "s.")); "potential")
35671
ed2c3830d881 improved Nitpick's precision for "card" and "setsum" + fix incorrect outcome code w.r.t. "bisim_depth = -1"
blanchet
parents: 35665
diff changeset
   952
        else if found_really_genuine then
ed2c3830d881 improved Nitpick's precision for "card" and "setsum" + fix incorrect outcome code w.r.t. "bisim_depth = -1"
blanchet
parents: 35665
diff changeset
   953
          "genuine"
33192
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   954
        else
35671
ed2c3830d881 improved Nitpick's precision for "card" and "setsum" + fix incorrect outcome code w.r.t. "bisim_depth = -1"
blanchet
parents: 35665
diff changeset
   955
          "quasi_genuine"
33192
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   956
      | run_batches j n (batch :: batches) z =
35671
ed2c3830d881 improved Nitpick's precision for "card" and "setsum" + fix incorrect outcome code w.r.t. "bisim_depth = -1"
blanchet
parents: 35665
diff changeset
   957
        let val (z as (_, _, max_genuine, _)) = run_batch j n batch z in
33192
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   958
          run_batches (j + 1) n (if max_genuine > 0 then batches else []) z
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   959
        end
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   960
33580
45c33e97cb86 added datatype constructor cache in Nitpick (to speed up the scope enumeration) and never test more than 4096 scopes
blanchet
parents: 33568
diff changeset
   961
    val (skipped, the_scopes) =
35190
ce653cc27a94 make sure that Nitpick uses binary notation consistently if "binary_ints" is enabled
blanchet
parents: 35185
diff changeset
   962
      all_scopes hol_ctxt binarize sym_break cards_assigns maxes_assigns
ce653cc27a94 make sure that Nitpick uses binary notation consistently if "binary_ints" is enabled
blanchet
parents: 35185
diff changeset
   963
                 iters_assigns bitss bisim_depths mono_Ts nonmono_Ts deep_dataTs
35385
29f81babefd7 improved precision of infinite "shallow" datatypes in Nitpick;
blanchet
parents: 35384
diff changeset
   964
                 finitizable_dataTs
33580
45c33e97cb86 added datatype constructor cache in Nitpick (to speed up the scope enumeration) and never test more than 4096 scopes
blanchet
parents: 33568
diff changeset
   965
    val _ = if skipped > 0 then
34124
c4628a1dcf75 added support for binary nat/int representation to Nitpick
blanchet
parents: 34123
diff changeset
   966
              print_m (fn () => "Too many scopes. Skipping " ^
33580
45c33e97cb86 added datatype constructor cache in Nitpick (to speed up the scope enumeration) and never test more than 4096 scopes
blanchet
parents: 33568
diff changeset
   967
                                string_of_int skipped ^ " scope" ^
45c33e97cb86 added datatype constructor cache in Nitpick (to speed up the scope enumeration) and never test more than 4096 scopes
blanchet
parents: 33568
diff changeset
   968
                                plural_s skipped ^
45c33e97cb86 added datatype constructor cache in Nitpick (to speed up the scope enumeration) and never test more than 4096 scopes
blanchet
parents: 33568
diff changeset
   969
                                ". (Consider using \"mono\" or \
45c33e97cb86 added datatype constructor cache in Nitpick (to speed up the scope enumeration) and never test more than 4096 scopes
blanchet
parents: 33568
diff changeset
   970
                                \\"merge_type_vars\" to prevent this.)")
45c33e97cb86 added datatype constructor cache in Nitpick (to speed up the scope enumeration) and never test more than 4096 scopes
blanchet
parents: 33568
diff changeset
   971
            else
45c33e97cb86 added datatype constructor cache in Nitpick (to speed up the scope enumeration) and never test more than 4096 scopes
blanchet
parents: 33568
diff changeset
   972
              ()
45c33e97cb86 added datatype constructor cache in Nitpick (to speed up the scope enumeration) and never test more than 4096 scopes
blanchet
parents: 33568
diff changeset
   973
    val _ = scopes := the_scopes
45c33e97cb86 added datatype constructor cache in Nitpick (to speed up the scope enumeration) and never test more than 4096 scopes
blanchet
parents: 33568
diff changeset
   974
33192
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   975
    val batches = batch_list batch_size (!scopes)
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   976
    val outcome_code =
35671
ed2c3830d881 improved Nitpick's precision for "card" and "setsum" + fix incorrect outcome code w.r.t. "bisim_depth = -1"
blanchet
parents: 35665
diff changeset
   977
      (run_batches 0 (length batches) batches
ed2c3830d881 improved Nitpick's precision for "card" and "setsum" + fix incorrect outcome code w.r.t. "bisim_depth = -1"
blanchet
parents: 35665
diff changeset
   978
                   (false, max_potential, max_genuine, 0)
33192
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   979
       handle Exn.Interrupt => do_interrupted ())
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   980
      handle TimeLimit.TimeOut =>
35696
17ae461d6133 show nice error message in Nitpick when "java" is not available
blanchet
parents: 35671
diff changeset
   981
             (print_m (fn () => excipit "ran out of time after checking");
33192
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   982
              if !met_potential > 0 then "potential" else "unknown")
35696
17ae461d6133 show nice error message in Nitpick when "java" is not available
blanchet
parents: 35671
diff changeset
   983
           | Exn.Interrupt =>
17ae461d6133 show nice error message in Nitpick when "java" is not available
blanchet
parents: 35671
diff changeset
   984
             if auto orelse debug then raise Interrupt
17ae461d6133 show nice error message in Nitpick when "java" is not available
blanchet
parents: 35671
diff changeset
   985
             else error (excipit "was interrupted after checking")
33192
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   986
    val _ = print_v (fn () => "Total time: " ^
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   987
                              signed_string_of_int (Time.toMilliseconds
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   988
                                    (Timer.checkRealTimer timer)) ^ " ms.")
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   989
  in (outcome_code, !state_ref) end
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   990
  handle Exn.Interrupt =>
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   991
         if auto orelse #debug params then
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   992
           raise Interrupt
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   993
         else
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   994
           if passed_deadline deadline then
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   995
             (priority "Nitpick ran out of time."; ("unknown", state))
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   996
           else
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   997
             error "Nitpick was interrupted."
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   998
35335
f715cfde056a support local definitions in Nitpick
blanchet
parents: 35334
diff changeset
   999
(* Proof.state -> params -> bool -> int -> int -> int -> (term * term) list
f715cfde056a support local definitions in Nitpick
blanchet
parents: 35334
diff changeset
  1000
   -> term list -> term -> string * Proof.state *)
34982
7b8c366e34a2 added support for nonstandard models to Nitpick (based on an idea by Koen Claessen) and did other fixes to Nitpick
blanchet
parents: 34938
diff changeset
  1001
fun pick_nits_in_term state (params as {debug, timeout, expect, ...}) auto i n
35335
f715cfde056a support local definitions in Nitpick
blanchet
parents: 35334
diff changeset
  1002
                      step subst orig_assm_ts orig_t =
33568
532b915afa14 don't run Nitpick at all if Kodkodi is not installed (as indicated by the $KODKODI variable)
blanchet
parents: 33566
diff changeset
  1003
  if getenv "KODKODI" = "" then
532b915afa14 don't run Nitpick at all if Kodkodi is not installed (as indicated by the $KODKODI variable)
blanchet
parents: 33566
diff changeset
  1004
    (if auto then ()
532b915afa14 don't run Nitpick at all if Kodkodi is not installed (as indicated by the $KODKODI variable)
blanchet
parents: 33566
diff changeset
  1005
     else warning (Pretty.string_of (plazy install_kodkodi_message));
532b915afa14 don't run Nitpick at all if Kodkodi is not installed (as indicated by the $KODKODI variable)
blanchet
parents: 33566
diff changeset
  1006
     ("unknown", state))
532b915afa14 don't run Nitpick at all if Kodkodi is not installed (as indicated by the $KODKODI variable)
blanchet
parents: 33566
diff changeset
  1007
  else
532b915afa14 don't run Nitpick at all if Kodkodi is not installed (as indicated by the $KODKODI variable)
blanchet
parents: 33566
diff changeset
  1008
    let
532b915afa14 don't run Nitpick at all if Kodkodi is not installed (as indicated by the $KODKODI variable)
blanchet
parents: 33566
diff changeset
  1009
      val deadline = Option.map (curry Time.+ (Time.now ())) timeout
532b915afa14 don't run Nitpick at all if Kodkodi is not installed (as indicated by the $KODKODI variable)
blanchet
parents: 33566
diff changeset
  1010
      val outcome as (outcome_code, _) =
532b915afa14 don't run Nitpick at all if Kodkodi is not installed (as indicated by the $KODKODI variable)
blanchet
parents: 33566
diff changeset
  1011
        time_limit (if debug then NONE else timeout)
35335
f715cfde056a support local definitions in Nitpick
blanchet
parents: 35334
diff changeset
  1012
            (pick_them_nits_in_term deadline state params auto i n step subst
34982
7b8c366e34a2 added support for nonstandard models to Nitpick (based on an idea by Koen Claessen) and did other fixes to Nitpick
blanchet
parents: 34938
diff changeset
  1013
                                    orig_assm_ts) orig_t
33568
532b915afa14 don't run Nitpick at all if Kodkodi is not installed (as indicated by the $KODKODI variable)
blanchet
parents: 33566
diff changeset
  1014
    in
532b915afa14 don't run Nitpick at all if Kodkodi is not installed (as indicated by the $KODKODI variable)
blanchet
parents: 33566
diff changeset
  1015
      if expect = "" orelse outcome_code = expect then outcome
532b915afa14 don't run Nitpick at all if Kodkodi is not installed (as indicated by the $KODKODI variable)
blanchet
parents: 33566
diff changeset
  1016
      else error ("Unexpected outcome: " ^ quote outcome_code ^ ".")
532b915afa14 don't run Nitpick at all if Kodkodi is not installed (as indicated by the $KODKODI variable)
blanchet
parents: 33566
diff changeset
  1017
    end
33192
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
  1018
35335
f715cfde056a support local definitions in Nitpick
blanchet
parents: 35334
diff changeset
  1019
(* string list -> term -> bool *)
f715cfde056a support local definitions in Nitpick
blanchet
parents: 35334
diff changeset
  1020
fun is_fixed_equation fixes
f715cfde056a support local definitions in Nitpick
blanchet
parents: 35334
diff changeset
  1021
                      (Const (@{const_name "=="}, _) $ Free (s, _) $ Const _) =
f715cfde056a support local definitions in Nitpick
blanchet
parents: 35334
diff changeset
  1022
    member (op =) fixes s
f715cfde056a support local definitions in Nitpick
blanchet
parents: 35334
diff changeset
  1023
  | is_fixed_equation _ _ = false
f715cfde056a support local definitions in Nitpick
blanchet
parents: 35334
diff changeset
  1024
(* Proof.context -> term list * term -> (term * term) list * term list * term *)
f715cfde056a support local definitions in Nitpick
blanchet
parents: 35334
diff changeset
  1025
fun extract_fixed_frees ctxt (assms, t) =
f715cfde056a support local definitions in Nitpick
blanchet
parents: 35334
diff changeset
  1026
  let
f715cfde056a support local definitions in Nitpick
blanchet
parents: 35334
diff changeset
  1027
    val fixes = Variable.fixes_of ctxt |> map snd
f715cfde056a support local definitions in Nitpick
blanchet
parents: 35334
diff changeset
  1028
    val (subst, other_assms) =
f715cfde056a support local definitions in Nitpick
blanchet
parents: 35334
diff changeset
  1029
      List.partition (is_fixed_equation fixes) assms
f715cfde056a support local definitions in Nitpick
blanchet
parents: 35334
diff changeset
  1030
      |>> map Logic.dest_equals
f715cfde056a support local definitions in Nitpick
blanchet
parents: 35334
diff changeset
  1031
  in (subst, other_assms, subst_atomic subst t) end
f715cfde056a support local definitions in Nitpick
blanchet
parents: 35334
diff changeset
  1032
34982
7b8c366e34a2 added support for nonstandard models to Nitpick (based on an idea by Koen Claessen) and did other fixes to Nitpick
blanchet
parents: 34938
diff changeset
  1033
(* Proof.state -> params -> bool -> int -> int -> string * Proof.state *)
7b8c366e34a2 added support for nonstandard models to Nitpick (based on an idea by Koen Claessen) and did other fixes to Nitpick
blanchet
parents: 34938
diff changeset
  1034
fun pick_nits_in_subgoal state params auto i step =
33192
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
  1035
  let
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
  1036
    val ctxt = Proof.context_of state
33292
affe60b3d864 renamed raw Proof.get_goal to Proof.raw_goal;
wenzelm
parents: 33233
diff changeset
  1037
    val t = state |> Proof.raw_goal |> #goal |> prop_of
33192
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
  1038
  in
34982
7b8c366e34a2 added support for nonstandard models to Nitpick (based on an idea by Koen Claessen) and did other fixes to Nitpick
blanchet
parents: 34938
diff changeset
  1039
    case Logic.count_prems t of
7b8c366e34a2 added support for nonstandard models to Nitpick (based on an idea by Koen Claessen) and did other fixes to Nitpick
blanchet
parents: 34938
diff changeset
  1040
      0 => (priority "No subgoal!"; ("none", state))
7b8c366e34a2 added support for nonstandard models to Nitpick (based on an idea by Koen Claessen) and did other fixes to Nitpick
blanchet
parents: 34938
diff changeset
  1041
    | n =>
33192
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
  1042
      let
35335
f715cfde056a support local definitions in Nitpick
blanchet
parents: 35334
diff changeset
  1043
        val (t, frees) = Logic.goal_params t i
f715cfde056a support local definitions in Nitpick
blanchet
parents: 35334
diff changeset
  1044
        val t = subst_bounds (frees, t)
33192
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
  1045
        val assms = map term_of (Assumption.all_assms_of ctxt)
35335
f715cfde056a support local definitions in Nitpick
blanchet
parents: 35334
diff changeset
  1046
        val (subst, assms, t) = extract_fixed_frees ctxt (assms, t)
f715cfde056a support local definitions in Nitpick
blanchet
parents: 35334
diff changeset
  1047
      in pick_nits_in_term state params auto i n step subst assms t end
33192
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
  1048
  end
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
  1049
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
  1050
end;