src/HOL/Tools/Nitpick/nitpick.ML
author blanchet
Thu, 04 Feb 2010 16:03:15 +0100
changeset 35070 96136eb6218f
parent 34998 5e492a862b34
child 35075 888802be2019
permissions -rw-r--r--
split "nitpick_hol.ML" into two files to make it more manageable; more refactoring to come
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
33192
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
    11
  type params = {
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
    12
    cards_assigns: (typ option * int list) list,
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
    13
    maxes_assigns: (styp option * int list) list,
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
    14
    iters_assigns: (styp option * int list) list,
34124
c4628a1dcf75 added support for binary nat/int representation to Nitpick
blanchet
parents: 34123
diff changeset
    15
    bitss: int list,
33192
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
    16
    bisim_depths: int list,
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
    17
    boxes: (typ option * bool option) list,
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
    18
    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
    19
    stds: (typ option * bool) list,
33192
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
    20
    wfs: (styp option * bool option) list,
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
    21
    sat_solver: string,
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
    22
    blocking: bool,
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
    23
    falsify: bool,
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
    24
    debug: bool,
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
    25
    verbose: bool,
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
    26
    overlord: bool,
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
    27
    user_axioms: bool option,
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
    28
    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
    29
    merge_type_vars: bool,
34124
c4628a1dcf75 added support for binary nat/int representation to Nitpick
blanchet
parents: 34123
diff changeset
    30
    binary_ints: bool option,
33192
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
    31
    destroy_constrs: bool,
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
    32
    specialize: bool,
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
    33
    skolemize: bool,
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
    34
    star_linear_preds: bool,
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
    35
    uncurry: bool,
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
    36
    fast_descrs: bool,
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
    37
    peephole_optim: bool,
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
    38
    timeout: Time.time option,
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
    39
    tac_timeout: Time.time option,
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
    40
    sym_break: int,
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
    41
    sharing_depth: int,
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
    42
    flatten_props: bool,
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
    43
    max_threads: int,
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
    44
    show_skolems: bool,
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
    45
    show_datatypes: bool,
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
    46
    show_consts: bool,
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
    47
    evals: term list,
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
    48
    formats: (term option * int list) list,
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
    49
    max_potential: int,
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
    50
    max_genuine: int,
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
    51
    check_potential: bool,
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
    52
    check_genuine: bool,
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
    53
    batch_size: int,
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
    54
    expect: string}
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
    55
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
    56
  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
    57
  val unregister_frac_type : string -> theory -> theory
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
    58
  val register_codatatype : typ -> string -> styp list -> theory -> theory
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
    59
  val unregister_codatatype : typ -> theory -> theory
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
    60
  val pick_nits_in_term :
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
    61
    Proof.state -> params -> bool -> int -> int -> int -> term list -> term
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
    62
    -> string * Proof.state
33192
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
    63
  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
    64
    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
    65
end;
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
    66
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
    67
structure Nitpick : NITPICK =
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
    68
struct
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
    69
33232
f93390060bbe internal renaming in Nitpick and fixed Kodkodi invokation on Linux;
blanchet
parents: 33192
diff changeset
    70
open Nitpick_Util
f93390060bbe internal renaming in Nitpick and fixed Kodkodi invokation on Linux;
blanchet
parents: 33192
diff changeset
    71
open Nitpick_HOL
35070
96136eb6218f split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents: 34998
diff changeset
    72
open Nitpick_Preproc
33232
f93390060bbe internal renaming in Nitpick and fixed Kodkodi invokation on Linux;
blanchet
parents: 33192
diff changeset
    73
open Nitpick_Mono
f93390060bbe internal renaming in Nitpick and fixed Kodkodi invokation on Linux;
blanchet
parents: 33192
diff changeset
    74
open Nitpick_Scope
f93390060bbe internal renaming in Nitpick and fixed Kodkodi invokation on Linux;
blanchet
parents: 33192
diff changeset
    75
open Nitpick_Peephole
f93390060bbe internal renaming in Nitpick and fixed Kodkodi invokation on Linux;
blanchet
parents: 33192
diff changeset
    76
open Nitpick_Rep
f93390060bbe internal renaming in Nitpick and fixed Kodkodi invokation on Linux;
blanchet
parents: 33192
diff changeset
    77
open Nitpick_Nut
f93390060bbe internal renaming in Nitpick and fixed Kodkodi invokation on Linux;
blanchet
parents: 33192
diff changeset
    78
open Nitpick_Kodkod
f93390060bbe internal renaming in Nitpick and fixed Kodkodi invokation on Linux;
blanchet
parents: 33192
diff changeset
    79
open Nitpick_Model
33192
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
    80
34126
8a2c5d7aff51 polished Nitpick's binary integer support etc.;
blanchet
parents: 34124
diff changeset
    81
structure KK = Kodkod
8a2c5d7aff51 polished Nitpick's binary integer support etc.;
blanchet
parents: 34124
diff changeset
    82
33192
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
    83
type params = {
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
    84
  cards_assigns: (typ option * int list) list,
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
    85
  maxes_assigns: (styp option * int list) list,
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
    86
  iters_assigns: (styp option * int list) list,
34124
c4628a1dcf75 added support for binary nat/int representation to Nitpick
blanchet
parents: 34123
diff changeset
    87
  bitss: int list,
33192
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
    88
  bisim_depths: int list,
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
    89
  boxes: (typ option * bool option) list,
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
    90
  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
    91
  stds: (typ option * bool) list,
33192
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
    92
  wfs: (styp option * bool option) list,
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
    93
  sat_solver: string,
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
    94
  blocking: bool,
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
    95
  falsify: bool,
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
    96
  debug: bool,
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
    97
  verbose: bool,
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
    98
  overlord: bool,
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
    99
  user_axioms: bool option,
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   100
  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
   101
  merge_type_vars: bool,
34124
c4628a1dcf75 added support for binary nat/int representation to Nitpick
blanchet
parents: 34123
diff changeset
   102
  binary_ints: bool option,
33192
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   103
  destroy_constrs: bool,
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   104
  specialize: bool,
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   105
  skolemize: bool,
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   106
  star_linear_preds: bool,
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   107
  uncurry: bool,
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   108
  fast_descrs: bool,
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   109
  peephole_optim: bool,
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   110
  timeout: Time.time option,
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   111
  tac_timeout: Time.time option,
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   112
  sym_break: int,
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   113
  sharing_depth: int,
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   114
  flatten_props: bool,
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   115
  max_threads: int,
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   116
  show_skolems: bool,
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   117
  show_datatypes: bool,
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   118
  show_consts: bool,
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   119
  evals: term list,
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   120
  formats: (term option * int list) list,
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   121
  max_potential: int,
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   122
  max_genuine: int,
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   123
  check_potential: bool,
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   124
  check_genuine: bool,
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   125
  batch_size: int,
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   126
  expect: string}
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   127
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   128
type problem_extension = {
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   129
  free_names: nut list,
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   130
  sel_names: nut list,
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   131
  nonsel_names: nut list,
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   132
  rel_table: nut NameTable.table,
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   133
  liberal: bool,
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   134
  scope: scope,
34126
8a2c5d7aff51 polished Nitpick's binary integer support etc.;
blanchet
parents: 34124
diff changeset
   135
  core: KK.formula,
8a2c5d7aff51 polished Nitpick's binary integer support etc.;
blanchet
parents: 34124
diff changeset
   136
  defs: KK.formula list}
33192
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   137
34126
8a2c5d7aff51 polished Nitpick's binary integer support etc.;
blanchet
parents: 34124
diff changeset
   138
type rich_problem = KK.problem * problem_extension
33192
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   139
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   140
(* Proof.context -> string -> term list -> Pretty.T list *)
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   141
fun pretties_for_formulas _ _ [] = []
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   142
  | pretties_for_formulas ctxt s ts =
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   143
    [Pretty.str (s ^ plural_s_for_list ts ^ ":"),
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   144
     Pretty.indent indent_size (Pretty.chunks
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   145
         (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
   146
                   Pretty.block [t |> shorten_names_in_term
33192
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   147
                                   |> Syntax.pretty_term ctxt,
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   148
                                 Pretty.str (if j = 1 then "." else ";")])
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   149
               (length ts downto 1) ts))]
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   150
33568
532b915afa14 don't run Nitpick at all if Kodkodi is not installed (as indicated by the $KODKODI variable)
blanchet
parents: 33566
diff changeset
   151
(* unit -> string *)
532b915afa14 don't run Nitpick at all if Kodkodi is not installed (as indicated by the $KODKODI variable)
blanchet
parents: 33566
diff changeset
   152
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
   153
  "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
   154
  \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
   155
  \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
   156
  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
   157
      (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
   158
       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
   159
33192
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   160
val max_liberal_delay_ms = 200
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   161
val max_liberal_delay_percent = 2
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   162
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   163
(* Time.time option -> int *)
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   164
fun liberal_delay_for_timeout NONE = max_liberal_delay_ms
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   165
  | liberal_delay_for_timeout (SOME timeout) =
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   166
    Int.max (0, Int.min (max_liberal_delay_ms,
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   167
                         Time.toMilliseconds timeout
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   168
                         * max_liberal_delay_percent div 100))
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 -> bool *)
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   171
fun passed_deadline NONE = false
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   172
  | 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
   173
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   174
(* ('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
   175
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
   176
34038
a2736debeabd make Nitpick output the message "Hint: Maybe you forgot a type constraint?" only for syntactic classes
blanchet
parents: 33982
diff changeset
   177
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
   178
  @{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
   179
  @{sort number}
a2736debeabd make Nitpick output the message "Hint: Maybe you forgot a type constraint?" only for syntactic classes
blanchet
parents: 33982
diff changeset
   180
(* typ -> bool *)
a2736debeabd make Nitpick output the message "Hint: Maybe you forgot a type constraint?" only for syntactic classes
blanchet
parents: 33982
diff changeset
   181
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
   182
    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
   183
  | 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
   184
(* term -> bool *)
a2736debeabd make Nitpick output the message "Hint: Maybe you forgot a type constraint?" only for syntactic classes
blanchet
parents: 33982
diff changeset
   185
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
   186
33568
532b915afa14 don't run Nitpick at all if Kodkodi is not installed (as indicated by the $KODKODI variable)
blanchet
parents: 33566
diff changeset
   187
(* (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
   188
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
   189
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
   190
(* Time.time -> Proof.state -> params -> bool -> int -> int -> int -> term
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
   191
   -> 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
   192
fun pick_them_nits_in_term deadline state (params : params) auto i n step
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
   193
                           orig_assm_ts orig_t =
33192
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   194
  let
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   195
    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
   196
    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
   197
    val ctxt = Proof.context_of 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
   198
(* FIXME: reintroduce code before new release
34039
1fba360b5443 made Nitpick work also for people who import "Plain" instead of "Main"
blanchet
parents: 34038
diff changeset
   199
    val nitpick_thy = ThyInfo.get_theory "Nitpick"
34936
c4f04bee79f3 some work on Nitpick's support for quotient types;
blanchet
parents: 34935
diff changeset
   200
    val _ = Theory.subthy (nitpick_thy, thy) orelse
c4f04bee79f3 some work on Nitpick's support for quotient types;
blanchet
parents: 34935
diff changeset
   201
            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
   202
*)
34124
c4628a1dcf75 added support for binary nat/int representation to Nitpick
blanchet
parents: 34123
diff changeset
   203
    val {cards_assigns, maxes_assigns, iters_assigns, bitss, bisim_depths,
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
   204
         boxes, monos, stds, wfs, sat_solver, blocking, falsify, debug, verbose,
34124
c4628a1dcf75 added support for binary nat/int representation to Nitpick
blanchet
parents: 34123
diff changeset
   205
         overlord, user_axioms, assms, merge_type_vars, binary_ints,
c4628a1dcf75 added support for binary nat/int representation to Nitpick
blanchet
parents: 34123
diff changeset
   206
         destroy_constrs, specialize, skolemize, star_linear_preds, uncurry,
c4628a1dcf75 added support for binary nat/int representation to Nitpick
blanchet
parents: 34123
diff changeset
   207
         fast_descrs, peephole_optim, tac_timeout, sym_break, sharing_depth,
c4628a1dcf75 added support for binary nat/int representation to Nitpick
blanchet
parents: 34123
diff changeset
   208
         flatten_props, max_threads, show_skolems, show_datatypes, show_consts,
c4628a1dcf75 added support for binary nat/int representation to Nitpick
blanchet
parents: 34123
diff changeset
   209
         evals, formats, max_potential, max_genuine, check_potential,
c4628a1dcf75 added support for binary nat/int representation to Nitpick
blanchet
parents: 34123
diff changeset
   210
         check_genuine, batch_size, ...} =
33192
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   211
      params
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   212
    val state_ref = Unsynchronized.ref state
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   213
    (* Pretty.T -> unit *)
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   214
    val pprint =
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   215
      if auto then
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   216
        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
   217
        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
   218
        o Pretty.mark Markup.hilite
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   219
      else
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   220
        priority o Pretty.string_of
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   221
    (* (unit -> Pretty.T) -> unit *)
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   222
    fun pprint_m f = () |> not auto ? pprint o f
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   223
    fun pprint_v f = () |> verbose ? pprint o f
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   224
    fun pprint_d f = () |> debug ? pprint o f
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   225
    (* string -> unit *)
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   226
    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
   227
    (* (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
   228
    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
   229
    val print_v = pprint_v 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
   230
    val print_d = pprint_d o K o plazy
33192
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   231
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   232
    (* unit -> unit *)
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   233
    fun check_deadline () =
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   234
      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
   235
      else ()
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   236
    (* unit -> 'a *)
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   237
    fun do_interrupted () =
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   238
      if passed_deadline deadline then raise TimeLimit.TimeOut
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   239
      else raise Interrupt
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   240
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
   241
    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
   242
      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
   243
        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
   244
      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
   245
        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
   246
            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
   247
                (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
   248
                   "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
   249
                 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
   250
                   "goal")) [orig_t]))
33192
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   251
    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
   252
                else orig_t
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   253
    val assms_t = if assms orelse auto then
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   254
                    Logic.mk_conjunction_list (neg_t :: orig_assm_ts)
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   255
                  else
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   256
                    neg_t
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   257
    val (assms_t, evals) =
33705
947184dc75c9 removed a few global names in Nitpick (styp, nat_less, pairf)
blanchet
parents: 33580
diff changeset
   258
      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
   259
                       |> pairf hd tl
33192
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   260
    val original_max_potential = max_potential
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   261
    val original_max_genuine = max_genuine
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   262
(*
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   263
    val _ = priority ("*** " ^ Syntax.string_of_term ctxt orig_t)
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   264
    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
   265
                     orig_assm_ts
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   266
*)
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   267
    val max_bisim_depth = fold Integer.max bisim_depths ~1
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   268
    val case_names = case_const_names thy
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   269
    val (defs, built_in_nondefs, user_nondefs) = all_axioms_of thy
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   270
    val def_table = const_def_table ctxt defs
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   271
    val nondef_table = const_nondef_table (built_in_nondefs @ user_nondefs)
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   272
    val simp_table = Unsynchronized.ref (const_simp_table ctxt)
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   273
    val psimp_table = const_psimp_table ctxt
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   274
    val intro_table = inductive_intro_table ctxt def_table
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   275
    val ground_thm_table = ground_theorem_table thy
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   276
    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
   277
    val (hol_ctxt as {wf_cache, ...}) =
33192
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   278
      {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
   279
       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
   280
       binary_ints = binary_ints, destroy_constrs = destroy_constrs,
c4628a1dcf75 added support for binary nat/int representation to Nitpick
blanchet
parents: 34123
diff changeset
   281
       specialize = specialize, skolemize = skolemize,
c4628a1dcf75 added support for binary nat/int representation to Nitpick
blanchet
parents: 34123
diff changeset
   282
       star_linear_preds = star_linear_preds, uncurry = uncurry,
c4628a1dcf75 added support for binary nat/int representation to Nitpick
blanchet
parents: 34123
diff changeset
   283
       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
   284
       case_names = case_names, def_table = def_table,
33192
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   285
       nondef_table = nondef_table, user_nondefs = user_nondefs,
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   286
       simp_table = simp_table, psimp_table = psimp_table,
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   287
       intro_table = intro_table, ground_thm_table = ground_thm_table,
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   288
       ersatz_table = ersatz_table, skolems = Unsynchronized.ref [],
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   289
       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
   290
       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
   291
       constr_cache = Unsynchronized.ref []}
33192
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   292
    val frees = Term.add_frees assms_t []
34936
c4f04bee79f3 some work on Nitpick's support for quotient types;
blanchet
parents: 34935
diff changeset
   293
    val _ = null (Term.add_tvars assms_t []) orelse
c4f04bee79f3 some work on Nitpick's support for quotient types;
blanchet
parents: 34935
diff changeset
   294
            raise NOT_SUPPORTED "schematic type variables"
33192
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   295
    val (((def_ts, nondef_ts), (got_all_mono_user_axioms, no_poly_user_axioms)),
35070
96136eb6218f split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents: 34998
diff changeset
   296
         core_t) = preprocess_term hol_ctxt assms_t
33192
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   297
    val got_all_user_axioms =
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   298
      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
   299
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   300
    (* styp * (bool * bool) -> unit *)
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   301
    fun print_wf (x, (gfp, wf)) =
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   302
      pprint (Pretty.blk (0,
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   303
          pstrs ("The " ^ (if gfp then "co" else "") ^ "inductive predicate \"")
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   304
          @ Syntax.pretty_term ctxt (Const x) ::
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   305
          pstrs (if wf then
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   306
                   "\" was proved well-founded. Nitpick can compute it \
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   307
                   \efficiently."
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   308
                 else
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   309
                   "\" 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
   310
                   \unroll it.")))
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   311
    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
   312
    val _ =
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   313
      pprint_d (fn () =>
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   314
          Pretty.chunks
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   315
              (pretties_for_formulas ctxt "Preprocessed formula" [core_t] @
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   316
               pretties_for_formulas ctxt "Relevant definitional axiom" def_ts @
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   317
               pretties_for_formulas ctxt "Relevant nondefinitional axiom"
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   318
                                     nondef_ts))
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   319
    val _ = List.app (ignore o Term.type_of) (core_t :: def_ts @ nondef_ts)
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   320
            handle TYPE (_, Ts, ts) =>
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   321
                   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
   322
35070
96136eb6218f split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents: 34998
diff changeset
   323
    val core_u = nut_from_term hol_ctxt Eq core_t
96136eb6218f split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents: 34998
diff changeset
   324
    val def_us = map (nut_from_term hol_ctxt DefEq) def_ts
96136eb6218f split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents: 34998
diff changeset
   325
    val nondef_us = map (nut_from_term hol_ctxt Eq) nondef_ts
33558
a2db56854b83 optimized Nitpick's encoding and rendering of datatypes whose constructors don't appear in the problem
blanchet
parents: 33556
diff changeset
   326
    val (free_names, const_names) =
a2db56854b83 optimized Nitpick's encoding and rendering of datatypes whose constructors don't appear in the problem
blanchet
parents: 33556
diff changeset
   327
      fold add_free_and_const_names (core_u :: def_us @ nondef_us) ([], [])
a2db56854b83 optimized Nitpick's encoding and rendering of datatypes whose constructors don't appear in the problem
blanchet
parents: 33556
diff changeset
   328
    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
   329
      List.partition (is_sel o nickname_of) const_names
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
   330
    val genuine_means_genuine = got_all_user_axioms andalso none_true wfs
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
   331
    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
   332
(*
a2db56854b83 optimized Nitpick's encoding and rendering of datatypes whose constructors don't appear in the problem
blanchet
parents: 33556
diff changeset
   333
    val _ = List.app (priority o string_for_nut ctxt)
a2db56854b83 optimized Nitpick's encoding and rendering of datatypes whose constructors don't appear in the problem
blanchet
parents: 33556
diff changeset
   334
                     (core_u :: def_us @ nondef_us)
a2db56854b83 optimized Nitpick's encoding and rendering of datatypes whose constructors don't appear in the problem
blanchet
parents: 33556
diff changeset
   335
*)
a2db56854b83 optimized Nitpick's encoding and rendering of datatypes whose constructors don't appear in the problem
blanchet
parents: 33556
diff changeset
   336
34121
5e831d805118 get rid of polymorphic equality in Nitpick's code + a few minor cleanups
blanchet
parents: 34039
diff changeset
   337
    val unique_scope = forall (curry (op =) 1 o length o snd) cards_assigns
33192
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   338
    (* typ -> bool *)
34936
c4f04bee79f3 some work on Nitpick's support for quotient types;
blanchet
parents: 34935
diff changeset
   339
    fun is_type_always_monotonic T =
34938
f4d3daddac42 fix issues with previous Nitpick change
blanchet
parents: 34936
diff changeset
   340
      (is_datatype thy T andalso not (is_quot_type thy T) andalso
f4d3daddac42 fix issues with previous Nitpick change
blanchet
parents: 34936
diff changeset
   341
       (not (is_pure_typedef thy T) orelse is_univ_typedef thy T)) orelse
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
   342
      is_number_type thy T orelse is_bit_type T orelse T = @{typ \<xi>}
34936
c4f04bee79f3 some work on Nitpick's support for quotient types;
blanchet
parents: 34935
diff changeset
   343
    fun is_type_monotonic T =
33192
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   344
      unique_scope orelse
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   345
      case triple_lookup (type_match thy) monos T of
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   346
        SOME (SOME b) => b
34936
c4f04bee79f3 some work on Nitpick's support for quotient types;
blanchet
parents: 34935
diff changeset
   347
      | _ => is_type_always_monotonic T orelse
35070
96136eb6218f split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents: 34998
diff changeset
   348
             formulas_monotonic hol_ctxt T Plus def_ts nondef_ts core_t
34936
c4f04bee79f3 some work on Nitpick's support for quotient types;
blanchet
parents: 34935
diff changeset
   349
    fun is_deep_datatype T =
c4f04bee79f3 some work on Nitpick's support for quotient types;
blanchet
parents: 34935
diff changeset
   350
      is_datatype thy T andalso
c4f04bee79f3 some work on Nitpick's support for quotient types;
blanchet
parents: 34935
diff changeset
   351
      (is_word_type T orelse
c4f04bee79f3 some work on Nitpick's support for quotient types;
blanchet
parents: 34935
diff changeset
   352
       exists (curry (op =) T o domain_type o type_of) sel_names)
35070
96136eb6218f split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents: 34998
diff changeset
   353
    val all_Ts = ground_types_in_terms hol_ctxt (core_t :: def_ts @ nondef_ts)
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
   354
                 |> sort TermOrd.typ_ord
34936
c4f04bee79f3 some work on Nitpick's support for quotient types;
blanchet
parents: 34935
diff changeset
   355
    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
   356
               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
   357
              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
   358
                         \of the presence of rationals, reals, \"Suc\", \
8a2c5d7aff51 polished Nitpick's binary integer support etc.;
blanchet
parents: 34124
diff changeset
   359
                         \\"gcd\", or \"lcm\" in the problem.")
34124
c4628a1dcf75 added support for binary nat/int representation to Nitpick
blanchet
parents: 34123
diff changeset
   360
            else
c4628a1dcf75 added support for binary nat/int representation to Nitpick
blanchet
parents: 34123
diff changeset
   361
              ()
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
   362
    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
   363
    val _ =
34936
c4f04bee79f3 some work on Nitpick's support for quotient types;
blanchet
parents: 34935
diff changeset
   364
      if verbose andalso not unique_scope then
c4f04bee79f3 some work on Nitpick's support for quotient types;
blanchet
parents: 34935
diff changeset
   365
        case filter_out is_type_always_monotonic mono_Ts of
c4f04bee79f3 some work on Nitpick's support for quotient types;
blanchet
parents: 34935
diff changeset
   366
          [] => ()
c4f04bee79f3 some work on Nitpick's support for quotient types;
blanchet
parents: 34935
diff changeset
   367
        | interesting_mono_Ts =>
c4f04bee79f3 some work on Nitpick's support for quotient types;
blanchet
parents: 34935
diff changeset
   368
          print_v (fn () =>
c4f04bee79f3 some work on Nitpick's support for quotient types;
blanchet
parents: 34935
diff changeset
   369
                      let
c4f04bee79f3 some work on Nitpick's support for quotient types;
blanchet
parents: 34935
diff changeset
   370
                        val ss = map (quote o string_for_type ctxt)
c4f04bee79f3 some work on Nitpick's support for quotient types;
blanchet
parents: 34935
diff changeset
   371
                                     interesting_mono_Ts
c4f04bee79f3 some work on Nitpick's support for quotient types;
blanchet
parents: 34935
diff changeset
   372
                      in
c4f04bee79f3 some work on Nitpick's support for quotient types;
blanchet
parents: 34935
diff changeset
   373
                        "The type" ^ plural_s_for_list ss ^ " " ^
c4f04bee79f3 some work on Nitpick's support for quotient types;
blanchet
parents: 34935
diff changeset
   374
                        space_implode " " (serial_commas "and" ss) ^ " " ^
c4f04bee79f3 some work on Nitpick's support for quotient types;
blanchet
parents: 34935
diff changeset
   375
                        (if none_true monos then
c4f04bee79f3 some work on Nitpick's support for quotient types;
blanchet
parents: 34935
diff changeset
   376
                           "passed the monotonicity test"
c4f04bee79f3 some work on Nitpick's support for quotient types;
blanchet
parents: 34935
diff changeset
   377
                         else
c4f04bee79f3 some work on Nitpick's support for quotient types;
blanchet
parents: 34935
diff changeset
   378
                           (if length ss = 1 then "is" else "are") ^
c4f04bee79f3 some work on Nitpick's support for quotient types;
blanchet
parents: 34935
diff changeset
   379
                           " considered monotonic") ^
c4f04bee79f3 some work on Nitpick's support for quotient types;
blanchet
parents: 34935
diff changeset
   380
                        ". Nitpick might be able to skip some scopes."
c4f04bee79f3 some work on Nitpick's support for quotient types;
blanchet
parents: 34935
diff changeset
   381
                      end)
33192
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   382
      else
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   383
        ()
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
   384
    val deep_dataTs = filter is_deep_datatype all_Ts
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
   385
    (* FIXME: Implement proper detection of induction datatypes. *)
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
   386
    (* string * (Rule_Cases.T * bool) -> bool *)
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
    fun is_inductive_case (_, (Rule_Cases.Case {fixes, assumes, ...}, _)) =
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
   388
      false
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
   389
(*
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
   390
      not (null fixes) andalso exists (String.isSuffix ".hyps" o fst) assumes
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
   391
*)
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
   392
    (* unit -> typ list *)
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
   393
    val induct_dataTs =
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
      if exists is_inductive_case (ProofContext.cases_of ctxt) 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
   395
        filter (is_datatype thy) all_Ts
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
   396
      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
   397
        []
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
   398
    val _ = if standard andalso not (null induct_dataTs) 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
   399
              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
   400
                  pstrs "Hint: To check that the induction hypothesis is \
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
   401
                        \general enough, try the following command: " @
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
   402
                  [Pretty.mark Markup.sendback (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
   403
                       pstrs ("nitpick [" ^
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
   404
                              commas (map (prefix "non_std " o maybe_quote
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
   405
                                           o unyxml o string_for_type ctxt)
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
   406
                                          induct_dataTs) ^
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
   407
                              ", show_consts]")))] @ pstrs "."))
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
   408
            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
   409
              ()
33192
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   410
(*
34936
c4f04bee79f3 some work on Nitpick's support for quotient types;
blanchet
parents: 34935
diff changeset
   411
    val _ = priority "Monotonic types:"
c4f04bee79f3 some work on Nitpick's support for quotient types;
blanchet
parents: 34935
diff changeset
   412
    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
   413
    val _ = priority "Nonmonotonic types:"
c4f04bee79f3 some work on Nitpick's support for quotient types;
blanchet
parents: 34935
diff changeset
   414
    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
   415
*)
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   416
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   417
    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
   418
    val effective_sat_solver =
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   419
      if sat_solver <> "smart" then
34936
c4f04bee79f3 some work on Nitpick's support for quotient types;
blanchet
parents: 34935
diff changeset
   420
        if need_incremental andalso
c4f04bee79f3 some work on Nitpick's support for quotient types;
blanchet
parents: 34935
diff changeset
   421
           not (member (op =) (Kodkod_SAT.configured_sat_solvers true)
c4f04bee79f3 some work on Nitpick's support for quotient types;
blanchet
parents: 34935
diff changeset
   422
                      sat_solver) then
33192
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   423
          (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
   424
                       \be used instead of " ^ quote sat_solver ^ "."));
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   425
           "SAT4J")
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   426
        else
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   427
          sat_solver
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   428
      else
33232
f93390060bbe internal renaming in Nitpick and fixed Kodkodi invokation on Linux;
blanchet
parents: 33192
diff changeset
   429
        Kodkod_SAT.smart_sat_solver_name need_incremental
33192
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   430
    val _ =
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   431
      if sat_solver = "smart" then
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   432
        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
   433
                          ". The following" ^
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   434
                          (if need_incremental then " incremental " else " ") ^
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   435
                          "solvers are configured: " ^
33232
f93390060bbe internal renaming in Nitpick and fixed Kodkodi invokation on Linux;
blanchet
parents: 33192
diff changeset
   436
                          commas (map quote (Kodkod_SAT.configured_sat_solvers
33192
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   437
                                                       need_incremental)) ^ ".")
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   438
      else
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
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   441
    val too_big_scopes = Unsynchronized.ref []
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   442
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   443
    (* bool -> scope -> rich_problem option *)
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   444
    fun problem_for_scope liberal
34124
c4628a1dcf75 added support for binary nat/int representation to Nitpick
blanchet
parents: 34123
diff changeset
   445
            (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
   446
      let
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   447
        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
   448
                            (!too_big_scopes)) orelse
c4f04bee79f3 some work on Nitpick's support for quotient types;
blanchet
parents: 34935
diff changeset
   449
                raise TOO_LARGE ("Nitpick.pick_them_nits_in_term.\
c4f04bee79f3 some work on Nitpick's support for quotient types;
blanchet
parents: 34935
diff changeset
   450
                                 \problem_for_scope", "too large scope")
33192
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   451
(*
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   452
        val _ = priority "Offsets:"
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   453
        val _ = List.app (fn (T, j0) =>
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   454
                             priority (string_for_type ctxt T ^ " = " ^
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   455
                                       string_of_int j0))
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   456
                         (Typtab.dest ofs)
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   457
*)
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
   458
        val all_exact = forall (is_exact_type datatypes) all_Ts
33192
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   459
        (* 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
   460
        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
   461
        val main_j0 = offset_of_type ofs bool_T
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   462
        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
   463
        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
   464
        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
   465
                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
   466
                           "bad offsets")
33192
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   467
        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
   468
        val (free_names, rep_table) =
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   469
          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
   470
        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
   471
        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
   472
        val min_highest_arity =
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   473
          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
   474
        val min_univ_card =
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   475
          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
   476
                         (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
   477
        val _ = check_arity min_univ_card min_highest_arity
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   478
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   479
        val core_u = choose_reps_in_nut scope liberal rep_table false core_u
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   480
        val def_us = map (choose_reps_in_nut scope liberal rep_table true)
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   481
                         def_us
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   482
        val nondef_us = map (choose_reps_in_nut scope liberal rep_table false)
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   483
                            nondef_us
33745
daf236998f82 comment out debugging code in Nitpick
blanchet
parents: 33744
diff changeset
   484
(*
33192
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   485
        val _ = List.app (priority o string_for_nut ctxt)
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   486
                         (free_names @ sel_names @ nonsel_names @
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   487
                          core_u :: def_us @ nondef_us)
33745
daf236998f82 comment out debugging code in Nitpick
blanchet
parents: 33744
diff changeset
   488
*)
33192
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   489
        val (free_rels, pool, rel_table) =
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   490
          rename_free_vars free_names initial_pool NameTable.empty
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   491
        val (sel_rels, pool, rel_table) =
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   492
          rename_free_vars sel_names pool rel_table
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   493
        val (other_rels, pool, rel_table) =
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   494
          rename_free_vars nonsel_names pool rel_table
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   495
        val core_u = rename_vars_in_nut pool rel_table core_u
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   496
        val def_us = map (rename_vars_in_nut pool rel_table) def_us
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   497
        val nondef_us = map (rename_vars_in_nut pool rel_table) nondef_us
34126
8a2c5d7aff51 polished Nitpick's binary integer support etc.;
blanchet
parents: 34124
diff changeset
   498
        (* nut -> KK.formula *)
34124
c4628a1dcf75 added support for binary nat/int representation to Nitpick
blanchet
parents: 34123
diff changeset
   499
        val to_f = kodkod_formula_from_nut bits ofs liberal kk
33192
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   500
        val core_f = to_f core_u
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   501
        val def_fs = map to_f def_us
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   502
        val nondef_fs = map to_f nondef_us
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   503
        val formula = fold (fold s_and) [def_fs, nondef_fs] core_f
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   504
        val comment = (if liberal then "liberal" else "conservative") ^ "\n" ^
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   505
                      PrintMode.setmp [] multiline_string_for_scope scope
34998
5e492a862b34 four changes to Nitpick:
blanchet
parents: 34982
diff changeset
   506
        val kodkod_sat_solver =
5e492a862b34 four changes to Nitpick:
blanchet
parents: 34982
diff changeset
   507
          Kodkod_SAT.sat_solver_spec overlord effective_sat_solver |> snd
34124
c4628a1dcf75 added support for binary nat/int representation to Nitpick
blanchet
parents: 34123
diff changeset
   508
        val bit_width = if bits = 0 then 16 else bits + 1
33192
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   509
        val delay = if liberal then
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   510
                      Option.map (fn time => Time.- (time, Time.now ()))
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   511
                                 deadline
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   512
                      |> liberal_delay_for_timeout
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   513
                    else
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   514
                      0
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   515
        val settings = [("solver", commas (map quote kodkod_sat_solver)),
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   516
                        ("skolem_depth", "-1"),
34124
c4628a1dcf75 added support for binary nat/int representation to Nitpick
blanchet
parents: 34123
diff changeset
   517
                        ("bit_width", string_of_int bit_width),
33192
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   518
                        ("symmetry_breaking", signed_string_of_int sym_break),
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   519
                        ("sharing", signed_string_of_int sharing_depth),
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   520
                        ("flatten", Bool.toString flatten_props),
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   521
                        ("delay", signed_string_of_int delay)]
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   522
        val plain_rels = free_rels @ other_rels
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   523
        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
   524
        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
   525
        val sel_bounds = map (bound_for_sel_rel ctxt debug datatypes) sel_rels
35070
96136eb6218f split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents: 34998
diff changeset
   526
        val dtype_axioms = declarative_axioms_for_datatypes hol_ctxt bits ofs kk
33192
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   527
                                                            rel_table datatypes
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   528
        val declarative_axioms = plain_axioms @ dtype_axioms
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   529
        val univ_card = univ_card nat_card int_card main_j0
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   530
                                  (plain_bounds @ sel_bounds) formula
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   531
        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
   532
                                  univ_card nat_card int_card main_j0 formula
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   533
        val bounds = built_in_bounds @ plain_bounds @ sel_bounds
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   534
                     |> not debug ? merge_bounds
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   535
        val highest_arity =
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   536
          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
   537
        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
   538
        val _ = if bits = 0 then () else check_bits bits formula
34126
8a2c5d7aff51 polished Nitpick's binary integer support etc.;
blanchet
parents: 34124
diff changeset
   539
        val _ = if formula = KK.False then ()
33192
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   540
                else check_arity univ_card highest_arity
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   541
      in
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   542
        SOME ({comment = comment, settings = settings, univ_card = univ_card,
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   543
               tuple_assigns = [], bounds = bounds,
34124
c4628a1dcf75 added support for binary nat/int representation to Nitpick
blanchet
parents: 34123
diff changeset
   544
               int_bounds =
c4628a1dcf75 added support for binary nat/int representation to Nitpick
blanchet
parents: 34123
diff changeset
   545
                   if bits = 0 then sequential_int_bounds univ_card
c4628a1dcf75 added support for binary nat/int representation to Nitpick
blanchet
parents: 34123
diff changeset
   546
                   else pow_of_two_int_bounds bits main_j0 univ_card,
33192
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   547
               expr_assigns = [], formula = formula},
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   548
              {free_names = free_names, sel_names = sel_names,
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   549
               nonsel_names = nonsel_names, rel_table = rel_table,
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   550
               liberal = liberal, scope = scope, core = core_f,
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   551
               defs = nondef_fs @ def_fs @ declarative_axioms})
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   552
      end
34124
c4628a1dcf75 added support for binary nat/int representation to Nitpick
blanchet
parents: 34123
diff changeset
   553
      handle TOO_LARGE (loc, msg) =>
34936
c4f04bee79f3 some work on Nitpick's support for quotient types;
blanchet
parents: 34935
diff changeset
   554
             if loc = "Nitpick_Kodkod.check_arity" andalso
c4f04bee79f3 some work on Nitpick's support for quotient types;
blanchet
parents: 34935
diff changeset
   555
                not (Typtab.is_empty ofs) then
33192
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   556
               problem_for_scope liberal
35070
96136eb6218f split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents: 34998
diff changeset
   557
                   {hol_ctxt = hol_ctxt, card_assigns = card_assigns,
34124
c4628a1dcf75 added support for binary nat/int representation to Nitpick
blanchet
parents: 34123
diff changeset
   558
                    bits = bits, bisim_depth = bisim_depth,
c4628a1dcf75 added support for binary nat/int representation to Nitpick
blanchet
parents: 34123
diff changeset
   559
                    datatypes = datatypes, ofs = Typtab.empty}
33192
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   560
             else if loc = "Nitpick.pick_them_nits_in_term.\
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   561
                           \problem_for_scope" then
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   562
               NONE
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   563
             else
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   564
               (Unsynchronized.change too_big_scopes (cons scope);
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   565
                print_v (fn () => ("Limit reached: " ^ msg ^
34124
c4628a1dcf75 added support for binary nat/int representation to Nitpick
blanchet
parents: 34123
diff changeset
   566
                                   ". Skipping " ^ (if liberal then "potential"
33192
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   567
                                                    else "genuine") ^
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   568
                                   " component of scope."));
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   569
                NONE)
34124
c4628a1dcf75 added support for binary nat/int representation to Nitpick
blanchet
parents: 34123
diff changeset
   570
           | TOO_SMALL (loc, msg) =>
c4628a1dcf75 added support for binary nat/int representation to Nitpick
blanchet
parents: 34123
diff changeset
   571
             (print_v (fn () => ("Limit reached: " ^ msg ^
c4628a1dcf75 added support for binary nat/int representation to Nitpick
blanchet
parents: 34123
diff changeset
   572
                                 ". Skipping " ^ (if liberal then "potential"
c4628a1dcf75 added support for binary nat/int representation to Nitpick
blanchet
parents: 34123
diff changeset
   573
                                                  else "genuine") ^
c4628a1dcf75 added support for binary nat/int representation to Nitpick
blanchet
parents: 34123
diff changeset
   574
                                 " component of scope."));
c4628a1dcf75 added support for binary nat/int representation to Nitpick
blanchet
parents: 34123
diff changeset
   575
              NONE)
33192
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   576
34126
8a2c5d7aff51 polished Nitpick's binary integer support etc.;
blanchet
parents: 34124
diff changeset
   577
    (* int -> (''a * int list list) list -> ''a -> KK.tuple_set *)
33192
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   578
    fun tuple_set_for_rel univ_card =
34126
8a2c5d7aff51 polished Nitpick's binary integer support etc.;
blanchet
parents: 34124
diff changeset
   579
      KK.TupleSet o map (kk_tuple debug univ_card) o the oo AList.lookup (op =)
33192
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   580
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
   581
    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
   582
      (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
   583
      |> not standard ? prefix "nonstandard "
33192
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   584
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   585
    val scopes = Unsynchronized.ref []
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   586
    val generated_scopes = Unsynchronized.ref []
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   587
    val generated_problems = Unsynchronized.ref []
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   588
    val checked_problems = Unsynchronized.ref (SOME [])
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   589
    val met_potential = Unsynchronized.ref 0
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   590
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   591
    (* rich_problem list -> int list -> unit *)
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   592
    fun update_checked_problems problems =
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   593
      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
   594
                o nth problems)
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   595
34126
8a2c5d7aff51 polished Nitpick's binary integer support etc.;
blanchet
parents: 34124
diff changeset
   596
    (* bool -> KK.raw_bound list -> problem_extension -> bool option *)
33192
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   597
    fun print_and_check_model genuine bounds
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   598
            ({free_names, sel_names, nonsel_names, rel_table, scope, ...}
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   599
             : problem_extension) =
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   600
      let
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   601
        val (reconstructed_model, codatatypes_ok) =
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   602
          reconstruct_hol_model {show_skolems = show_skolems,
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   603
                                 show_datatypes = show_datatypes,
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   604
                                 show_consts = show_consts}
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   605
              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
   606
              bounds
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
   607
        val genuine_means_genuine = genuine_means_genuine andalso codatatypes_ok
33192
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   608
      in
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   609
        pprint (Pretty.chunks
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   610
            [Pretty.blk (0,
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   611
                 (pstrs ("Nitpick found a" ^
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   612
                         (if not genuine then " potential "
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
   613
                          else 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
   614
                          else " likely genuine ") ^ das_wort_model) @
33192
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   615
                  (case pretties_for_scope scope verbose of
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   616
                     [] => []
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   617
                   | pretties => pstrs " for " @ pretties) @
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   618
                  [Pretty.str ":\n"])),
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   619
             Pretty.indent indent_size reconstructed_model]);
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   620
        if genuine 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
   621
          (if check_genuine andalso standard then
33192
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   622
             (case prove_hol_model scope tac_timeout free_names sel_names
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   623
                                   rel_table bounds assms_t of
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   624
                SOME true => print ("Confirmation by \"auto\": The above " ^
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
   625
                                    das_wort_model ^ " is really genuine.")
33192
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   626
              | 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
   627
                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
   628
                  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
   629
                         \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
   630
                         \happen.\nPlease send a bug report to blanchet\
33192
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   631
                         \te@in.tum.de.")
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   632
                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
   633
                  print ("Refutation by \"auto\": The above " ^ das_wort_model ^
33192
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   634
                         " is spurious.")
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   635
              | NONE => print "No confirmation by \"auto\".")
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   636
           else
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   637
             ();
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
   638
           if not standard andalso not (null induct_dataTs) 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
   639
             print "The existence of a nonstandard model suggests that the \
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
   640
                   \induction hypothesis is not general enough or perhaps even \
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
   641
                   \wrong. See the \"Inductive Properties\" section of the \
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
   642
                   \Nitpick manual for details (\"isabelle doc nitpick\")."
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
   643
           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
   644
             ();
34038
a2736debeabd make Nitpick output the message "Hint: Maybe you forgot a type constraint?" only for syntactic classes
blanchet
parents: 33982
diff changeset
   645
           if has_syntactic_sorts orig_t then
33192
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   646
             print "Hint: Maybe you forgot a type constraint?"
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   647
           else
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   648
             ();
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
   649
           if not genuine_means_genuine then
33192
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   650
             if no_poly_user_axioms then
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   651
               let
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   652
                 val options =
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   653
                   [] |> not got_all_mono_user_axioms
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   654
                         ? cons ("user_axioms", "\"true\"")
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   655
                      |> not (none_true wfs)
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   656
                         ? cons ("wf", "\"smart\" or \"false\"")
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   657
                      |> not codatatypes_ok
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   658
                         ? cons ("bisim_depth", "a nonnegative value")
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   659
                 val ss =
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   660
                   map (fn (name, value) => quote name ^ " set to " ^ value)
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   661
                       options
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   662
               in
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   663
                 print ("Try again with " ^
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   664
                        space_implode " " (serial_commas "and" ss) ^
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
   665
                        " to confirm that the " ^ 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
   666
                        " is genuine.")
33192
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   667
               end
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   668
             else
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   669
               print ("Nitpick is unable to guarantee the authenticity of \
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
   670
                      \the " ^ das_wort_model ^ " in the presence 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
   671
                      \polymorphic axioms.")
33192
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   672
           else
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   673
             ();
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   674
           NONE)
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   675
        else
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   676
          if not genuine then
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   677
            (Unsynchronized.inc met_potential;
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   678
             if check_potential then
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   679
               let
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   680
                 val status = prove_hol_model scope tac_timeout free_names
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   681
                                              sel_names rel_table bounds assms_t
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   682
               in
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   683
                 (case status of
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   684
                    SOME true => print ("Confirmation by \"auto\": The above " ^
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
   685
                                        das_wort_model ^ " is genuine.")
33192
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   686
                  | SOME false => print ("Refutation by \"auto\": The above " ^
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
   687
                                         das_wort_model ^ " is spurious.")
33192
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   688
                  | NONE => print "No confirmation by \"auto\".");
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   689
                 status
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   690
               end
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   691
             else
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   692
               NONE)
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   693
          else
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   694
            NONE
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   695
      end
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   696
    (* int -> int -> int -> bool -> rich_problem list -> int * int * int *)
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   697
    fun solve_any_problem max_potential max_genuine donno first_time problems =
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   698
      let
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   699
        val max_potential = Int.max (0, max_potential)
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   700
        val max_genuine = Int.max (0, max_genuine)
34126
8a2c5d7aff51 polished Nitpick's binary integer support etc.;
blanchet
parents: 34124
diff changeset
   701
        (* bool -> int * KK.raw_bound list -> bool option *)
33192
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   702
        fun print_and_check genuine (j, bounds) =
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   703
          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
   704
        val max_solutions = max_potential + max_genuine
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   705
                            |> not need_incremental ? curry Int.min 1
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   706
      in
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   707
        if max_solutions <= 0 then
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   708
          (0, 0, donno)
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   709
        else
34126
8a2c5d7aff51 polished Nitpick's binary integer support etc.;
blanchet
parents: 34124
diff changeset
   710
          case KK.solve_any_problem overlord deadline max_threads max_solutions
8a2c5d7aff51 polished Nitpick's binary integer support etc.;
blanchet
parents: 34124
diff changeset
   711
                                    (map fst problems) of
8a2c5d7aff51 polished Nitpick's binary integer support etc.;
blanchet
parents: 34124
diff changeset
   712
            KK.NotInstalled =>
33568
532b915afa14 don't run Nitpick at all if Kodkodi is not installed (as indicated by the $KODKODI variable)
blanchet
parents: 33566
diff changeset
   713
            (print_m install_kodkodi_message;
33233
f9ff11344ec4 added friendly error message when Kodkodi is not available
blanchet
parents: 33232
diff changeset
   714
             (max_potential, max_genuine, donno + 1))
34126
8a2c5d7aff51 polished Nitpick's binary integer support etc.;
blanchet
parents: 34124
diff changeset
   715
          | KK.Normal ([], unsat_js) =>
33192
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   716
            (update_checked_problems problems unsat_js;
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   717
             (max_potential, max_genuine, donno))
34126
8a2c5d7aff51 polished Nitpick's binary integer support etc.;
blanchet
parents: 34124
diff changeset
   718
          | KK.Normal (sat_ps, unsat_js) =>
33192
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   719
            let
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   720
              val (lib_ps, con_ps) =
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   721
                List.partition (#liberal o snd o nth problems o fst) sat_ps
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   722
            in
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   723
              update_checked_problems problems (unsat_js @ map fst lib_ps);
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   724
              if null con_ps then
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   725
                let
33955
fff6f11b1f09 curried take/drop
haftmann
parents: 33877
diff changeset
   726
                  val num_genuine = take max_potential lib_ps
33192
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   727
                                    |> map (print_and_check false)
34121
5e831d805118 get rid of polymorphic equality in Nitpick's code + a few minor cleanups
blanchet
parents: 34039
diff changeset
   728
                                    |> filter (curry (op =) (SOME true))
5e831d805118 get rid of polymorphic equality in Nitpick's code + a few minor cleanups
blanchet
parents: 34039
diff changeset
   729
                                    |> length
33192
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   730
                  val max_genuine = max_genuine - num_genuine
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   731
                  val max_potential = max_potential
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   732
                                      - (length lib_ps - num_genuine)
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   733
                in
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   734
                  if max_genuine <= 0 then
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   735
                    (0, 0, donno)
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   736
                  else
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   737
                    let
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   738
                      (* "co_js" is the list of conservative problems whose
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   739
                         liberal pendants couldn't be satisfied and hence that
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   740
                         most probably can't be satisfied themselves. *)
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   741
                      val co_js =
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   742
                        map (fn j => j - 1) unsat_js
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   743
                        |> filter (fn j =>
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   744
                                      j >= 0 andalso
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   745
                                      scopes_equivalent
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   746
                                          (#scope (snd (nth problems j)))
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   747
                                          (#scope (snd (nth problems (j + 1)))))
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   748
                      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
   749
                                                          unsat_js @ co_js)
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   750
                      val problems =
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   751
                        problems |> filter_out_indices bye_js
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   752
                                 |> max_potential <= 0
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   753
                                    ? filter_out (#liberal o snd)
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   754
                    in
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   755
                      solve_any_problem max_potential max_genuine donno false
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   756
                                        problems
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   757
                    end
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   758
                end
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   759
              else
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   760
                let
33955
fff6f11b1f09 curried take/drop
haftmann
parents: 33877
diff changeset
   761
                  val _ = take max_genuine con_ps
33192
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   762
                          |> List.app (ignore o print_and_check true)
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   763
                  val max_genuine = max_genuine - length con_ps
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   764
                in
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   765
                  if max_genuine <= 0 orelse not first_time then
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   766
                    (0, max_genuine, donno)
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   767
                  else
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   768
                    let
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   769
                      val bye_js = sort_distinct int_ord
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   770
                                                 (map fst sat_ps @ unsat_js)
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   771
                      val problems =
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   772
                        problems |> filter_out_indices bye_js
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   773
                                 |> filter_out (#liberal o snd)
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   774
                    in solve_any_problem 0 max_genuine donno false problems end
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   775
                end
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   776
            end
34126
8a2c5d7aff51 polished Nitpick's binary integer support etc.;
blanchet
parents: 34124
diff changeset
   777
          | KK.TimedOut unsat_js =>
33192
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   778
            (update_checked_problems problems unsat_js; raise TimeLimit.TimeOut)
34126
8a2c5d7aff51 polished Nitpick's binary integer support etc.;
blanchet
parents: 34124
diff changeset
   779
          | KK.Interrupted NONE => (checked_problems := NONE; do_interrupted ())
8a2c5d7aff51 polished Nitpick's binary integer support etc.;
blanchet
parents: 34124
diff changeset
   780
          | KK.Interrupted (SOME unsat_js) =>
33192
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   781
            (update_checked_problems problems unsat_js; do_interrupted ())
34126
8a2c5d7aff51 polished Nitpick's binary integer support etc.;
blanchet
parents: 34124
diff changeset
   782
          | KK.Error (s, unsat_js) =>
33192
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   783
            (update_checked_problems problems unsat_js;
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   784
             print_v (K ("Kodkod error: " ^ s ^ "."));
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   785
             (max_potential, max_genuine, donno + 1))
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   786
      end
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   787
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   788
    (* int -> int -> scope list -> int * int * int -> int * int * int *)
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   789
    fun run_batch j n scopes (max_potential, max_genuine, donno) =
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   790
      let
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   791
        val _ =
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   792
          if null scopes then
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   793
            print_m (K "The scope specification is inconsistent.")
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   794
          else if verbose then
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   795
            pprint (Pretty.chunks
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   796
                [Pretty.blk (0,
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   797
                     pstrs ((if n > 1 then
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   798
                               "Batch " ^ string_of_int (j + 1) ^ " of " ^
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   799
                               signed_string_of_int n ^ ": "
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   800
                             else
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   801
                               "") ^
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   802
                            "Trying " ^ string_of_int (length scopes) ^
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   803
                            " scope" ^ plural_s_for_list scopes ^ ":")),
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   804
                 Pretty.indent indent_size
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   805
                     (Pretty.chunks (map2
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   806
                          (fn j => fn scope =>
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   807
                              Pretty.block (
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   808
                                  (case pretties_for_scope scope true of
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   809
                                     [] => [Pretty.str "Empty"]
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   810
                                   | pretties => pretties) @
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   811
                                  [Pretty.str (if j = 1 then "." else ";")]))
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   812
                          (length scopes downto 1) scopes))])
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   813
          else
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   814
            ()
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   815
        (* scope * bool -> rich_problem list * bool
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   816
           -> rich_problem list * bool *)
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   817
        fun add_problem_for_scope (scope as {datatypes, ...}, liberal)
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   818
                                  (problems, donno) =
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   819
          (check_deadline ();
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   820
           case problem_for_scope liberal scope of
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   821
             SOME problem =>
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   822
             (problems
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   823
              |> (null problems orelse
34126
8a2c5d7aff51 polished Nitpick's binary integer support etc.;
blanchet
parents: 34124
diff changeset
   824
                  not (KK.problems_equivalent (fst problem)
8a2c5d7aff51 polished Nitpick's binary integer support etc.;
blanchet
parents: 34124
diff changeset
   825
                                              (fst (hd problems))))
33192
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   826
                  ? cons problem, donno)
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   827
           | NONE => (problems, donno + 1))
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   828
        val (problems, donno) =
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   829
          fold add_problem_for_scope
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   830
               (map_product pair scopes
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   831
                    ((if max_genuine > 0 then [false] else []) @
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   832
                     (if max_potential > 0 then [true] else [])))
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   833
               ([], donno)
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   834
        val _ = Unsynchronized.change generated_problems (append problems)
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   835
        val _ = Unsynchronized.change generated_scopes (append scopes)
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   836
      in
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   837
        solve_any_problem max_potential max_genuine donno true (rev problems)
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   838
      end
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   839
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   840
    (* rich_problem list -> scope -> int *)
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   841
    fun scope_count (problems : rich_problem list) scope =
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   842
      length (filter (scopes_equivalent scope o #scope o snd) problems)
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   843
    (* string -> string *)
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   844
    fun excipit did_so_and_so =
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   845
      let
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   846
        (* rich_problem list -> rich_problem list *)
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   847
        val do_filter =
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   848
          if !met_potential = max_potential then filter_out (#liberal o snd)
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   849
          else I
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   850
        val total = length (!scopes)
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   851
        val unsat =
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   852
          fold (fn scope =>
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   853
                   case scope_count (do_filter (!generated_problems)) scope of
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   854
                     0 => I
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   855
                   | 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
   856
                     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
   857
                                 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
   858
                     ? Integer.add 1) (!generated_scopes) 0
33192
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   859
      in
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   860
        "Nitpick " ^ did_so_and_so ^
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   861
        (if is_some (!checked_problems) andalso total > 0 then
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   862
           " after checking " ^
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   863
           string_of_int (Int.min (total - 1, unsat)) ^ " of " ^
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   864
           string_of_int total ^ " scope" ^ plural_s total
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   865
         else
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   866
           "") ^ "."
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   867
      end
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   868
34126
8a2c5d7aff51 polished Nitpick's binary integer support etc.;
blanchet
parents: 34124
diff changeset
   869
    (* int -> int -> scope list -> int * int * int -> KK.outcome *)
33192
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   870
    fun run_batches _ _ [] (max_potential, max_genuine, donno) =
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   871
        if donno > 0 andalso max_genuine > 0 then
34124
c4628a1dcf75 added support for binary nat/int representation to Nitpick
blanchet
parents: 34123
diff changeset
   872
          (print_m (fn () => excipit "ran out of some resource"); "unknown")
33192
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   873
        else if max_genuine = original_max_genuine then
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   874
          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
   875
            (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
   876
                 "Nitpick found no " ^ 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
   877
                 (if not standard andalso not (null induct_dataTs) 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
   878
                    " 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
   879
                    \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
   880
                  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
   881
                    "")); "none")
33192
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   882
          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
   883
            (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
   884
                 "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
   885
                 (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
   886
                  else "ny better " ^ das_wort_model ^ "s.")); "potential")
33192
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   887
        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
   888
          if genuine_means_genuine then "genuine" else "likely_genuine"
33192
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   889
      | run_batches j n (batch :: batches) z =
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   890
        let val (z as (_, max_genuine, _)) = run_batch j n batch z in
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   891
          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
   892
        end
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   893
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
   894
    val (skipped, the_scopes) =
35070
96136eb6218f split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents: 34998
diff changeset
   895
      all_scopes hol_ctxt sym_break cards_assigns maxes_assigns iters_assigns
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
   896
                 bitss bisim_depths mono_Ts nonmono_Ts deep_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
   897
    val _ = if skipped > 0 then
34124
c4628a1dcf75 added support for binary nat/int representation to Nitpick
blanchet
parents: 34123
diff changeset
   898
              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
   899
                                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
   900
                                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
   901
                                ". (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
   902
                                \\"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
   903
            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
   904
              ()
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
   905
    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
   906
33192
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   907
    val batches = batch_list batch_size (!scopes)
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   908
    val outcome_code =
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   909
      (run_batches 0 (length batches) batches (max_potential, max_genuine, 0)
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   910
       handle Exn.Interrupt => do_interrupted ())
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   911
      handle TimeLimit.TimeOut =>
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   912
             (print_m (fn () => excipit "ran out of time");
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   913
              if !met_potential > 0 then "potential" else "unknown")
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   914
           | Exn.Interrupt => if auto orelse debug then raise Interrupt
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   915
                              else error (excipit "was interrupted")
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   916
    val _ = print_v (fn () => "Total time: " ^
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   917
                              signed_string_of_int (Time.toMilliseconds
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   918
                                    (Timer.checkRealTimer timer)) ^ " ms.")
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   919
  in (outcome_code, !state_ref) end
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   920
  handle Exn.Interrupt =>
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   921
         if auto orelse #debug params then
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   922
           raise Interrupt
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   923
         else
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   924
           if passed_deadline deadline then
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   925
             (priority "Nitpick ran out of time."; ("unknown", state))
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   926
           else
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   927
             error "Nitpick was interrupted."
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   928
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
   929
(* Proof.state -> params -> bool -> int -> int -> int -> term
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
   930
   -> 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
   931
fun pick_nits_in_term state (params as {debug, timeout, expect, ...}) auto i 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
   932
                      step 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
   933
  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
   934
    (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
   935
     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
   936
     ("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
   937
  else
532b915afa14 don't run Nitpick at all if Kodkodi is not installed (as indicated by the $KODKODI variable)
blanchet
parents: 33566
diff changeset
   938
    let
532b915afa14 don't run Nitpick at all if Kodkodi is not installed (as indicated by the $KODKODI variable)
blanchet
parents: 33566
diff changeset
   939
      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
   940
      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
   941
        time_limit (if debug then NONE else timeout)
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
   942
            (pick_them_nits_in_term deadline state params auto i n step
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
                                    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
   944
    in
532b915afa14 don't run Nitpick at all if Kodkodi is not installed (as indicated by the $KODKODI variable)
blanchet
parents: 33566
diff changeset
   945
      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
   946
      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
   947
    end
33192
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   948
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
   949
(* 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
   950
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
   951
  let
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   952
    val ctxt = Proof.context_of state
33292
affe60b3d864 renamed raw Proof.get_goal to Proof.raw_goal;
wenzelm
parents: 33233
diff changeset
   953
    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
   954
  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
   955
    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
   956
      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
   957
    | n =>
33192
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   958
      let
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   959
        val assms = map term_of (Assumption.all_assms_of ctxt)
34121
5e831d805118 get rid of polymorphic equality in Nitpick's code + a few minor cleanups
blanchet
parents: 34039
diff changeset
   960
        val (t, frees) = Logic.goal_params t i
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
   961
      in
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
   962
        pick_nits_in_term state params auto i n step assms
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
   963
                          (subst_bounds (frees, t))
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
   964
      end
33192
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   965
  end
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   966
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   967
end;