src/HOL/Tools/Nitpick/nitpick.ML
author blanchet
Tue, 24 Apr 2012 09:47:40 +0200
changeset 47715 04400144c6fc
parent 47670 24babc4b1925
child 47716 dc9c8ce4aac5
permissions -rw-r--r--
handle TPTP definitions as definitions in Nitpick rather than as axioms
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
33982
1ae222745c4a fixed paths in Nitpick's ML file headers
blanchet
parents: 33955
diff changeset
     1
(*  Title:      HOL/Tools/Nitpick/nitpick.ML
33192
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
     2
    Author:     Jasmin Blanchette, TU Muenchen
34982
7b8c366e34a2 added support for nonstandard models to Nitpick (based on an idea by Koen Claessen) and did other fixes to Nitpick
blanchet
parents: 34938
diff changeset
     3
    Copyright   2008, 2009, 2010
33192
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
     4
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
     5
Finite model generation for HOL formulas using Kodkod.
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
     6
*)
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
     7
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
     8
signature NITPICK =
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
     9
sig
33705
947184dc75c9 removed a few global names in Nitpick (styp, nat_less, pairf)
blanchet
parents: 33580
diff changeset
    10
  type styp = Nitpick_Util.styp
35711
548d3f16404b added term postprocessor to Nitpick, to provide custom syntax for typedefs
blanchet
parents: 35696
diff changeset
    11
  type term_postprocessor = Nitpick_Model.term_postprocessor
43022
7d3ce43d9464 handle non-auto try case gracefully in Nitpick
blanchet
parents: 43020
diff changeset
    12
47560
e30323bfc93c added SZS status wrappers in TPTP mode
blanchet
parents: 47559
diff changeset
    13
  datatype mode = Auto_Try | Try | Normal | TPTP
43022
7d3ce43d9464 handle non-auto try case gracefully in Nitpick
blanchet
parents: 43020
diff changeset
    14
36390
eee4ee6a5cbe remove "show_skolems" option and change style of record declarations
blanchet
parents: 36389
diff changeset
    15
  type params =
eee4ee6a5cbe remove "show_skolems" option and change style of record declarations
blanchet
parents: 36389
diff changeset
    16
    {cards_assigns: (typ option * int list) list,
eee4ee6a5cbe remove "show_skolems" option and change style of record declarations
blanchet
parents: 36389
diff changeset
    17
     maxes_assigns: (styp option * int list) list,
eee4ee6a5cbe remove "show_skolems" option and change style of record declarations
blanchet
parents: 36389
diff changeset
    18
     iters_assigns: (styp option * int list) list,
eee4ee6a5cbe remove "show_skolems" option and change style of record declarations
blanchet
parents: 36389
diff changeset
    19
     bitss: int list,
eee4ee6a5cbe remove "show_skolems" option and change style of record declarations
blanchet
parents: 36389
diff changeset
    20
     bisim_depths: int list,
eee4ee6a5cbe remove "show_skolems" option and change style of record declarations
blanchet
parents: 36389
diff changeset
    21
     boxes: (typ option * bool option) list,
eee4ee6a5cbe remove "show_skolems" option and change style of record declarations
blanchet
parents: 36389
diff changeset
    22
     finitizes: (typ option * bool option) list,
eee4ee6a5cbe remove "show_skolems" option and change style of record declarations
blanchet
parents: 36389
diff changeset
    23
     monos: (typ option * bool option) list,
eee4ee6a5cbe remove "show_skolems" option and change style of record declarations
blanchet
parents: 36389
diff changeset
    24
     stds: (typ option * bool) list,
eee4ee6a5cbe remove "show_skolems" option and change style of record declarations
blanchet
parents: 36389
diff changeset
    25
     wfs: (styp option * bool option) list,
eee4ee6a5cbe remove "show_skolems" option and change style of record declarations
blanchet
parents: 36389
diff changeset
    26
     sat_solver: string,
eee4ee6a5cbe remove "show_skolems" option and change style of record declarations
blanchet
parents: 36389
diff changeset
    27
     blocking: bool,
eee4ee6a5cbe remove "show_skolems" option and change style of record declarations
blanchet
parents: 36389
diff changeset
    28
     falsify: bool,
eee4ee6a5cbe remove "show_skolems" option and change style of record declarations
blanchet
parents: 36389
diff changeset
    29
     debug: bool,
eee4ee6a5cbe remove "show_skolems" option and change style of record declarations
blanchet
parents: 36389
diff changeset
    30
     verbose: bool,
eee4ee6a5cbe remove "show_skolems" option and change style of record declarations
blanchet
parents: 36389
diff changeset
    31
     overlord: bool,
eee4ee6a5cbe remove "show_skolems" option and change style of record declarations
blanchet
parents: 36389
diff changeset
    32
     user_axioms: bool option,
eee4ee6a5cbe remove "show_skolems" option and change style of record declarations
blanchet
parents: 36389
diff changeset
    33
     assms: bool,
38209
3d1d928dce50 added "whack"
blanchet
parents: 38188
diff changeset
    34
     whacks: term list,
36390
eee4ee6a5cbe remove "show_skolems" option and change style of record declarations
blanchet
parents: 36389
diff changeset
    35
     merge_type_vars: bool,
eee4ee6a5cbe remove "show_skolems" option and change style of record declarations
blanchet
parents: 36389
diff changeset
    36
     binary_ints: bool option,
eee4ee6a5cbe remove "show_skolems" option and change style of record declarations
blanchet
parents: 36389
diff changeset
    37
     destroy_constrs: bool,
eee4ee6a5cbe remove "show_skolems" option and change style of record declarations
blanchet
parents: 36389
diff changeset
    38
     specialize: bool,
eee4ee6a5cbe remove "show_skolems" option and change style of record declarations
blanchet
parents: 36389
diff changeset
    39
     star_linear_preds: bool,
41856
7244589c8ccc added "total_consts" option
blanchet
parents: 41803
diff changeset
    40
     total_consts: bool option,
41876
03f699556955 simplify "need" option's syntax
blanchet
parents: 41875
diff changeset
    41
     needs: term list option,
36390
eee4ee6a5cbe remove "show_skolems" option and change style of record declarations
blanchet
parents: 36389
diff changeset
    42
     peephole_optim: bool,
38124
6538e25cf5dd started implementation of custom sym break
blanchet
parents: 38123
diff changeset
    43
     datatype_sym_break: int,
6538e25cf5dd started implementation of custom sym break
blanchet
parents: 38123
diff changeset
    44
     kodkod_sym_break: int,
36390
eee4ee6a5cbe remove "show_skolems" option and change style of record declarations
blanchet
parents: 36389
diff changeset
    45
     timeout: Time.time option,
eee4ee6a5cbe remove "show_skolems" option and change style of record declarations
blanchet
parents: 36389
diff changeset
    46
     tac_timeout: Time.time option,
eee4ee6a5cbe remove "show_skolems" option and change style of record declarations
blanchet
parents: 36389
diff changeset
    47
     max_threads: int,
eee4ee6a5cbe remove "show_skolems" option and change style of record declarations
blanchet
parents: 36389
diff changeset
    48
     show_datatypes: bool,
41993
bd6296de1432 reintroduced "show_skolems" option -- useful when too many Skolems are displayed
blanchet
parents: 41992
diff changeset
    49
     show_skolems: bool,
36390
eee4ee6a5cbe remove "show_skolems" option and change style of record declarations
blanchet
parents: 36389
diff changeset
    50
     show_consts: bool,
eee4ee6a5cbe remove "show_skolems" option and change style of record declarations
blanchet
parents: 36389
diff changeset
    51
     evals: term list,
eee4ee6a5cbe remove "show_skolems" option and change style of record declarations
blanchet
parents: 36389
diff changeset
    52
     formats: (term option * int list) list,
37260
dde817e6dfb1 added "atoms" option to Nitpick (request from Karlsruhe) + wrap Refute. functions to "nitpick_util.ML"
blanchet
parents: 37257
diff changeset
    53
     atomss: (typ option * string list) list,
36390
eee4ee6a5cbe remove "show_skolems" option and change style of record declarations
blanchet
parents: 36389
diff changeset
    54
     max_potential: int,
eee4ee6a5cbe remove "show_skolems" option and change style of record declarations
blanchet
parents: 36389
diff changeset
    55
     max_genuine: int,
eee4ee6a5cbe remove "show_skolems" option and change style of record declarations
blanchet
parents: 36389
diff changeset
    56
     check_potential: bool,
eee4ee6a5cbe remove "show_skolems" option and change style of record declarations
blanchet
parents: 36389
diff changeset
    57
     check_genuine: bool,
eee4ee6a5cbe remove "show_skolems" option and change style of record declarations
blanchet
parents: 36389
diff changeset
    58
     batch_size: int,
eee4ee6a5cbe remove "show_skolems" option and change style of record declarations
blanchet
parents: 36389
diff changeset
    59
     expect: string}
33192
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
    60
43020
abb5d1f907e4 added "try" command, to launch Solve Direct, Quickcheck, Nitpick, Sledgehammer, and Try Methods
blanchet
parents: 42959
diff changeset
    61
  val genuineN : string
abb5d1f907e4 added "try" command, to launch Solve Direct, Quickcheck, Nitpick, Sledgehammer, and Try Methods
blanchet
parents: 42959
diff changeset
    62
  val quasi_genuineN : string
abb5d1f907e4 added "try" command, to launch Solve Direct, Quickcheck, Nitpick, Sledgehammer, and Try Methods
blanchet
parents: 42959
diff changeset
    63
  val potentialN : string
abb5d1f907e4 added "try" command, to launch Solve Direct, Quickcheck, Nitpick, Sledgehammer, and Try Methods
blanchet
parents: 42959
diff changeset
    64
  val noneN : string
abb5d1f907e4 added "try" command, to launch Solve Direct, Quickcheck, Nitpick, Sledgehammer, and Try Methods
blanchet
parents: 42959
diff changeset
    65
  val unknownN : string
33192
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
    66
  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
    67
  val unregister_frac_type : string -> theory -> theory
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
    68
  val register_codatatype : typ -> string -> styp list -> theory -> theory
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
    69
  val unregister_codatatype : typ -> theory -> theory
35711
548d3f16404b added term postprocessor to Nitpick, to provide custom syntax for typedefs
blanchet
parents: 35696
diff changeset
    70
  val register_term_postprocessor :
548d3f16404b added term postprocessor to Nitpick, to provide custom syntax for typedefs
blanchet
parents: 35696
diff changeset
    71
    typ -> term_postprocessor -> theory -> theory
548d3f16404b added term postprocessor to Nitpick, to provide custom syntax for typedefs
blanchet
parents: 35696
diff changeset
    72
  val unregister_term_postprocessor : typ -> theory -> theory
33192
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
    73
  val pick_nits_in_term :
43022
7d3ce43d9464 handle non-auto try case gracefully in Nitpick
blanchet
parents: 43020
diff changeset
    74
    Proof.state -> params -> mode -> int -> int -> int -> (term * term) list
47715
04400144c6fc handle TPTP definitions as definitions in Nitpick rather than as axioms
blanchet
parents: 47670
diff changeset
    75
    -> term list -> term list -> term -> string * Proof.state
33192
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
    76
  val pick_nits_in_subgoal :
43022
7d3ce43d9464 handle non-auto try case gracefully in Nitpick
blanchet
parents: 43020
diff changeset
    77
    Proof.state -> params -> mode -> int -> int -> string * Proof.state
33192
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
    78
end;
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
    79
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
    80
structure Nitpick : NITPICK =
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
    81
struct
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
    82
33232
f93390060bbe internal renaming in Nitpick and fixed Kodkodi invokation on Linux;
blanchet
parents: 33192
diff changeset
    83
open Nitpick_Util
f93390060bbe internal renaming in Nitpick and fixed Kodkodi invokation on Linux;
blanchet
parents: 33192
diff changeset
    84
open Nitpick_HOL
35070
96136eb6218f split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents: 34998
diff changeset
    85
open Nitpick_Preproc
33232
f93390060bbe internal renaming in Nitpick and fixed Kodkodi invokation on Linux;
blanchet
parents: 33192
diff changeset
    86
open Nitpick_Mono
f93390060bbe internal renaming in Nitpick and fixed Kodkodi invokation on Linux;
blanchet
parents: 33192
diff changeset
    87
open Nitpick_Scope
f93390060bbe internal renaming in Nitpick and fixed Kodkodi invokation on Linux;
blanchet
parents: 33192
diff changeset
    88
open Nitpick_Peephole
f93390060bbe internal renaming in Nitpick and fixed Kodkodi invokation on Linux;
blanchet
parents: 33192
diff changeset
    89
open Nitpick_Rep
f93390060bbe internal renaming in Nitpick and fixed Kodkodi invokation on Linux;
blanchet
parents: 33192
diff changeset
    90
open Nitpick_Nut
f93390060bbe internal renaming in Nitpick and fixed Kodkodi invokation on Linux;
blanchet
parents: 33192
diff changeset
    91
open Nitpick_Kodkod
f93390060bbe internal renaming in Nitpick and fixed Kodkodi invokation on Linux;
blanchet
parents: 33192
diff changeset
    92
open Nitpick_Model
33192
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
    93
34126
8a2c5d7aff51 polished Nitpick's binary integer support etc.;
blanchet
parents: 34124
diff changeset
    94
structure KK = Kodkod
8a2c5d7aff51 polished Nitpick's binary integer support etc.;
blanchet
parents: 34124
diff changeset
    95
47560
e30323bfc93c added SZS status wrappers in TPTP mode
blanchet
parents: 47559
diff changeset
    96
datatype mode = Auto_Try | Try | Normal | TPTP
e30323bfc93c added SZS status wrappers in TPTP mode
blanchet
parents: 47559
diff changeset
    97
e30323bfc93c added SZS status wrappers in TPTP mode
blanchet
parents: 47559
diff changeset
    98
fun is_mode_nt mode = (mode = Normal orelse mode = TPTP)
43022
7d3ce43d9464 handle non-auto try case gracefully in Nitpick
blanchet
parents: 43020
diff changeset
    99
36390
eee4ee6a5cbe remove "show_skolems" option and change style of record declarations
blanchet
parents: 36389
diff changeset
   100
type params =
eee4ee6a5cbe remove "show_skolems" option and change style of record declarations
blanchet
parents: 36389
diff changeset
   101
  {cards_assigns: (typ option * int list) list,
eee4ee6a5cbe remove "show_skolems" option and change style of record declarations
blanchet
parents: 36389
diff changeset
   102
   maxes_assigns: (styp option * int list) list,
eee4ee6a5cbe remove "show_skolems" option and change style of record declarations
blanchet
parents: 36389
diff changeset
   103
   iters_assigns: (styp option * int list) list,
eee4ee6a5cbe remove "show_skolems" option and change style of record declarations
blanchet
parents: 36389
diff changeset
   104
   bitss: int list,
eee4ee6a5cbe remove "show_skolems" option and change style of record declarations
blanchet
parents: 36389
diff changeset
   105
   bisim_depths: int list,
eee4ee6a5cbe remove "show_skolems" option and change style of record declarations
blanchet
parents: 36389
diff changeset
   106
   boxes: (typ option * bool option) list,
eee4ee6a5cbe remove "show_skolems" option and change style of record declarations
blanchet
parents: 36389
diff changeset
   107
   finitizes: (typ option * bool option) list,
eee4ee6a5cbe remove "show_skolems" option and change style of record declarations
blanchet
parents: 36389
diff changeset
   108
   monos: (typ option * bool option) list,
eee4ee6a5cbe remove "show_skolems" option and change style of record declarations
blanchet
parents: 36389
diff changeset
   109
   stds: (typ option * bool) list,
eee4ee6a5cbe remove "show_skolems" option and change style of record declarations
blanchet
parents: 36389
diff changeset
   110
   wfs: (styp option * bool option) list,
eee4ee6a5cbe remove "show_skolems" option and change style of record declarations
blanchet
parents: 36389
diff changeset
   111
   sat_solver: string,
eee4ee6a5cbe remove "show_skolems" option and change style of record declarations
blanchet
parents: 36389
diff changeset
   112
   blocking: bool,
eee4ee6a5cbe remove "show_skolems" option and change style of record declarations
blanchet
parents: 36389
diff changeset
   113
   falsify: bool,
eee4ee6a5cbe remove "show_skolems" option and change style of record declarations
blanchet
parents: 36389
diff changeset
   114
   debug: bool,
eee4ee6a5cbe remove "show_skolems" option and change style of record declarations
blanchet
parents: 36389
diff changeset
   115
   verbose: bool,
eee4ee6a5cbe remove "show_skolems" option and change style of record declarations
blanchet
parents: 36389
diff changeset
   116
   overlord: bool,
eee4ee6a5cbe remove "show_skolems" option and change style of record declarations
blanchet
parents: 36389
diff changeset
   117
   user_axioms: bool option,
eee4ee6a5cbe remove "show_skolems" option and change style of record declarations
blanchet
parents: 36389
diff changeset
   118
   assms: bool,
38209
3d1d928dce50 added "whack"
blanchet
parents: 38188
diff changeset
   119
   whacks: term list,
36390
eee4ee6a5cbe remove "show_skolems" option and change style of record declarations
blanchet
parents: 36389
diff changeset
   120
   merge_type_vars: bool,
eee4ee6a5cbe remove "show_skolems" option and change style of record declarations
blanchet
parents: 36389
diff changeset
   121
   binary_ints: bool option,
eee4ee6a5cbe remove "show_skolems" option and change style of record declarations
blanchet
parents: 36389
diff changeset
   122
   destroy_constrs: bool,
eee4ee6a5cbe remove "show_skolems" option and change style of record declarations
blanchet
parents: 36389
diff changeset
   123
   specialize: bool,
eee4ee6a5cbe remove "show_skolems" option and change style of record declarations
blanchet
parents: 36389
diff changeset
   124
   star_linear_preds: bool,
41856
7244589c8ccc added "total_consts" option
blanchet
parents: 41803
diff changeset
   125
   total_consts: bool option,
41876
03f699556955 simplify "need" option's syntax
blanchet
parents: 41875
diff changeset
   126
   needs: term list option,
36390
eee4ee6a5cbe remove "show_skolems" option and change style of record declarations
blanchet
parents: 36389
diff changeset
   127
   peephole_optim: bool,
38124
6538e25cf5dd started implementation of custom sym break
blanchet
parents: 38123
diff changeset
   128
   datatype_sym_break: int,
6538e25cf5dd started implementation of custom sym break
blanchet
parents: 38123
diff changeset
   129
   kodkod_sym_break: int,
36390
eee4ee6a5cbe remove "show_skolems" option and change style of record declarations
blanchet
parents: 36389
diff changeset
   130
   timeout: Time.time option,
eee4ee6a5cbe remove "show_skolems" option and change style of record declarations
blanchet
parents: 36389
diff changeset
   131
   tac_timeout: Time.time option,
eee4ee6a5cbe remove "show_skolems" option and change style of record declarations
blanchet
parents: 36389
diff changeset
   132
   max_threads: int,
eee4ee6a5cbe remove "show_skolems" option and change style of record declarations
blanchet
parents: 36389
diff changeset
   133
   show_datatypes: bool,
41993
bd6296de1432 reintroduced "show_skolems" option -- useful when too many Skolems are displayed
blanchet
parents: 41992
diff changeset
   134
   show_skolems: bool,
36390
eee4ee6a5cbe remove "show_skolems" option and change style of record declarations
blanchet
parents: 36389
diff changeset
   135
   show_consts: bool,
eee4ee6a5cbe remove "show_skolems" option and change style of record declarations
blanchet
parents: 36389
diff changeset
   136
   evals: term list,
eee4ee6a5cbe remove "show_skolems" option and change style of record declarations
blanchet
parents: 36389
diff changeset
   137
   formats: (term option * int list) list,
37260
dde817e6dfb1 added "atoms" option to Nitpick (request from Karlsruhe) + wrap Refute. functions to "nitpick_util.ML"
blanchet
parents: 37257
diff changeset
   138
   atomss: (typ option * string list) list,
36390
eee4ee6a5cbe remove "show_skolems" option and change style of record declarations
blanchet
parents: 36389
diff changeset
   139
   max_potential: int,
eee4ee6a5cbe remove "show_skolems" option and change style of record declarations
blanchet
parents: 36389
diff changeset
   140
   max_genuine: int,
eee4ee6a5cbe remove "show_skolems" option and change style of record declarations
blanchet
parents: 36389
diff changeset
   141
   check_potential: bool,
eee4ee6a5cbe remove "show_skolems" option and change style of record declarations
blanchet
parents: 36389
diff changeset
   142
   check_genuine: bool,
eee4ee6a5cbe remove "show_skolems" option and change style of record declarations
blanchet
parents: 36389
diff changeset
   143
   batch_size: int,
eee4ee6a5cbe remove "show_skolems" option and change style of record declarations
blanchet
parents: 36389
diff changeset
   144
   expect: string}
33192
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   145
43020
abb5d1f907e4 added "try" command, to launch Solve Direct, Quickcheck, Nitpick, Sledgehammer, and Try Methods
blanchet
parents: 42959
diff changeset
   146
val genuineN = "genuine"
abb5d1f907e4 added "try" command, to launch Solve Direct, Quickcheck, Nitpick, Sledgehammer, and Try Methods
blanchet
parents: 42959
diff changeset
   147
val quasi_genuineN = "quasi_genuine"
abb5d1f907e4 added "try" command, to launch Solve Direct, Quickcheck, Nitpick, Sledgehammer, and Try Methods
blanchet
parents: 42959
diff changeset
   148
val potentialN = "potential"
abb5d1f907e4 added "try" command, to launch Solve Direct, Quickcheck, Nitpick, Sledgehammer, and Try Methods
blanchet
parents: 42959
diff changeset
   149
val noneN = "none"
abb5d1f907e4 added "try" command, to launch Solve Direct, Quickcheck, Nitpick, Sledgehammer, and Try Methods
blanchet
parents: 42959
diff changeset
   150
val unknownN = "unknown"
abb5d1f907e4 added "try" command, to launch Solve Direct, Quickcheck, Nitpick, Sledgehammer, and Try Methods
blanchet
parents: 42959
diff changeset
   151
38240
a44d108a8d39 local versions of Nitpick.register_xxx functions
blanchet
parents: 38214
diff changeset
   152
(* TODO: eliminate these historical aliases *)
a44d108a8d39 local versions of Nitpick.register_xxx functions
blanchet
parents: 38214
diff changeset
   153
val register_frac_type = Nitpick_HOL.register_frac_type_global
a44d108a8d39 local versions of Nitpick.register_xxx functions
blanchet
parents: 38214
diff changeset
   154
val unregister_frac_type = Nitpick_HOL.unregister_frac_type_global
a44d108a8d39 local versions of Nitpick.register_xxx functions
blanchet
parents: 38214
diff changeset
   155
val register_codatatype = Nitpick_HOL.register_codatatype_global
a44d108a8d39 local versions of Nitpick.register_xxx functions
blanchet
parents: 38214
diff changeset
   156
val unregister_codatatype = Nitpick_HOL.unregister_codatatype_global
a44d108a8d39 local versions of Nitpick.register_xxx functions
blanchet
parents: 38214
diff changeset
   157
val register_term_postprocessor =
a44d108a8d39 local versions of Nitpick.register_xxx functions
blanchet
parents: 38214
diff changeset
   158
  Nitpick_Model.register_term_postprocessor_global
a44d108a8d39 local versions of Nitpick.register_xxx functions
blanchet
parents: 38214
diff changeset
   159
val unregister_term_postprocessor =
a44d108a8d39 local versions of Nitpick.register_xxx functions
blanchet
parents: 38214
diff changeset
   160
  Nitpick_Model.unregister_term_postprocessor_global
a44d108a8d39 local versions of Nitpick.register_xxx functions
blanchet
parents: 38214
diff changeset
   161
36390
eee4ee6a5cbe remove "show_skolems" option and change style of record declarations
blanchet
parents: 36389
diff changeset
   162
type problem_extension =
eee4ee6a5cbe remove "show_skolems" option and change style of record declarations
blanchet
parents: 36389
diff changeset
   163
  {free_names: nut list,
eee4ee6a5cbe remove "show_skolems" option and change style of record declarations
blanchet
parents: 36389
diff changeset
   164
   sel_names: nut list,
eee4ee6a5cbe remove "show_skolems" option and change style of record declarations
blanchet
parents: 36389
diff changeset
   165
   nonsel_names: nut list,
eee4ee6a5cbe remove "show_skolems" option and change style of record declarations
blanchet
parents: 36389
diff changeset
   166
   rel_table: nut NameTable.table,
eee4ee6a5cbe remove "show_skolems" option and change style of record declarations
blanchet
parents: 36389
diff changeset
   167
   unsound: bool,
eee4ee6a5cbe remove "show_skolems" option and change style of record declarations
blanchet
parents: 36389
diff changeset
   168
   scope: scope}
39316
b6c4385ab400 change defaults of Auto Nitpick so that it consumes less resources (time and Kodkod threads)
blanchet
parents: 38857
diff changeset
   169
34126
8a2c5d7aff51 polished Nitpick's binary integer support etc.;
blanchet
parents: 34124
diff changeset
   170
type rich_problem = KK.problem * problem_extension
33192
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   171
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   172
fun pretties_for_formulas _ _ [] = []
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   173
  | pretties_for_formulas ctxt s ts =
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   174
    [Pretty.str (s ^ plural_s_for_list ts ^ ":"),
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   175
     Pretty.indent indent_size (Pretty.chunks
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   176
         (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
   177
                   Pretty.block [t |> shorten_names_in_term
33192
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   178
                                   |> Syntax.pretty_term ctxt,
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   179
                                 Pretty.str (if j = 1 then "." else ";")])
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   180
               (length ts downto 1) ts))]
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   181
35696
17ae461d6133 show nice error message in Nitpick when "java" is not available
blanchet
parents: 35671
diff changeset
   182
fun install_java_message () =
47490
f4348634595b more precise handling of java failure, due to missing ISABELLE_JDK_HOME;
wenzelm
parents: 47108
diff changeset
   183
  "Nitpick requires Java Development Kit 1.6/1.7 via ISABELLE_JDK_HOME setting."
33568
532b915afa14 don't run Nitpick at all if Kodkodi is not installed (as indicated by the $KODKODI variable)
blanchet
parents: 33566
diff changeset
   184
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
   185
  "Nitpick requires the external Java program Kodkodi. To install it, download \
46243
4b1b43ab7c62 updated message
blanchet
parents: 46114
diff changeset
   186
  \the package from \"http://www21.in.tum.de/~blanchet/#software\" and add the \
4b1b43ab7c62 updated message
blanchet
parents: 46114
diff changeset
   187
  \\"kodkodi-x.y.z\" directory's full path to " ^
43602
8c89a1fb30f2 standardized use of Path operations;
wenzelm
parents: 43022
diff changeset
   188
  Path.print (Path.expand (Path.explode "$ISABELLE_HOME_USER/etc/components")) ^
8c89a1fb30f2 standardized use of Path operations;
wenzelm
parents: 43022
diff changeset
   189
  " on a line of its own."
33568
532b915afa14 don't run Nitpick at all if Kodkodi is not installed (as indicated by the $KODKODI variable)
blanchet
parents: 33566
diff changeset
   190
35185
9b8f351cced6 added yet another hint to Nitpick's output, this time warning about problems for which nothing was effectively tested
blanchet
parents: 35183
diff changeset
   191
val max_unsound_delay_ms = 200
9b8f351cced6 added yet another hint to Nitpick's output, this time warning about problems for which nothing was effectively tested
blanchet
parents: 35183
diff changeset
   192
val max_unsound_delay_percent = 2
33192
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   193
35185
9b8f351cced6 added yet another hint to Nitpick's output, this time warning about problems for which nothing was effectively tested
blanchet
parents: 35183
diff changeset
   194
fun unsound_delay_for_timeout NONE = max_unsound_delay_ms
9b8f351cced6 added yet another hint to Nitpick's output, this time warning about problems for which nothing was effectively tested
blanchet
parents: 35183
diff changeset
   195
  | unsound_delay_for_timeout (SOME timeout) =
9b8f351cced6 added yet another hint to Nitpick's output, this time warning about problems for which nothing was effectively tested
blanchet
parents: 35183
diff changeset
   196
    Int.max (0, Int.min (max_unsound_delay_ms,
33192
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   197
                         Time.toMilliseconds timeout
35185
9b8f351cced6 added yet another hint to Nitpick's output, this time warning about problems for which nothing was effectively tested
blanchet
parents: 35183
diff changeset
   198
                         * max_unsound_delay_percent div 100))
33192
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   199
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   200
fun passed_deadline NONE = false
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   201
  | 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
   202
34123
c4988215a691 distinguish better between "complete" (vs. incomplete) types and "concrete" (vs. abstract) types in Nitpick;
blanchet
parents: 34121
diff changeset
   203
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
   204
41048
d5ebe94248ad added a hint when the user obviously just forgot a colon after the lemma's name
blanchet
parents: 41007
diff changeset
   205
fun has_lonely_bool_var (@{const Pure.conjunction}
d5ebe94248ad added a hint when the user obviously just forgot a colon after the lemma's name
blanchet
parents: 41007
diff changeset
   206
                         $ (@{const Trueprop} $ Free _) $ _) = true
d5ebe94248ad added a hint when the user obviously just forgot a colon after the lemma's name
blanchet
parents: 41007
diff changeset
   207
  | has_lonely_bool_var _ = false
d5ebe94248ad added a hint when the user obviously just forgot a colon after the lemma's name
blanchet
parents: 41007
diff changeset
   208
34038
a2736debeabd make Nitpick output the message "Hint: Maybe you forgot a type constraint?" only for syntactic classes
blanchet
parents: 33982
diff changeset
   209
val syntactic_sorts =
38857
97775f3e8722 renamed class/constant eq to equal; tuned some instantiations
haftmann
parents: 38517
diff changeset
   210
  @{sort "{default,zero,one,plus,minus,uminus,times,inverse,abs,sgn,ord,equal}"} @
47108
2a1953f0d20d merged fork with new numeral representation (see NEWS)
huffman
parents: 46243
diff changeset
   211
  @{sort numeral}
34038
a2736debeabd make Nitpick output the message "Hint: Maybe you forgot a type constraint?" only for syntactic classes
blanchet
parents: 33982
diff changeset
   212
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
   213
    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
   214
  | 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
   215
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
   216
33568
532b915afa14 don't run Nitpick at all if Kodkodi is not installed (as indicated by the $KODKODI variable)
blanchet
parents: 33566
diff changeset
   217
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
   218
43022
7d3ce43d9464 handle non-auto try case gracefully in Nitpick
blanchet
parents: 43020
diff changeset
   219
fun pick_them_nits_in_term deadline state (params : params) mode i n step
47715
04400144c6fc handle TPTP definitions as definitions in Nitpick rather than as axioms
blanchet
parents: 47670
diff changeset
   220
                           subst def_assm_ts nondef_assm_ts orig_t =
33192
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   221
  let
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   222
    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
   223
    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
   224
    val ctxt = Proof.context_of state
35386
45a4e19d3ebd more work on the new monotonicity stuff in Nitpick
blanchet
parents: 35385
diff changeset
   225
(* FIXME: reintroduce code before new release:
45a4e19d3ebd more work on the new monotonicity stuff in Nitpick
blanchet
parents: 35385
diff changeset
   226
37216
3165bc303f66 modernized some structure names, keeping a few legacy aliases;
wenzelm
parents: 37213
diff changeset
   227
    val nitpick_thy = Thy_Info.get_theory "Nitpick"
34936
c4f04bee79f3 some work on Nitpick's support for quotient types;
blanchet
parents: 34935
diff changeset
   228
    val _ = Theory.subthy (nitpick_thy, thy) orelse
c4f04bee79f3 some work on Nitpick's support for quotient types;
blanchet
parents: 34935
diff changeset
   229
            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
   230
*)
34124
c4628a1dcf75 added support for binary nat/int representation to Nitpick
blanchet
parents: 34123
diff changeset
   231
    val {cards_assigns, maxes_assigns, iters_assigns, bitss, bisim_depths,
35665
ff2bf50505ab added "finitize" option to Nitpick + remove dependency on "Coinductive_List"
blanchet
parents: 35408
diff changeset
   232
         boxes, finitizes, monos, stds, wfs, sat_solver, falsify, debug,
38209
3d1d928dce50 added "whack"
blanchet
parents: 38188
diff changeset
   233
         verbose, overlord, user_axioms, assms, whacks, merge_type_vars,
3d1d928dce50 added "whack"
blanchet
parents: 38188
diff changeset
   234
         binary_ints, destroy_constrs, specialize, star_linear_preds,
41875
e3cd0dce9b1a renamed "preconstr" option "need"
blanchet
parents: 41872
diff changeset
   235
         total_consts, needs, peephole_optim, datatype_sym_break,
41856
7244589c8ccc added "total_consts" option
blanchet
parents: 41803
diff changeset
   236
         kodkod_sym_break, tac_timeout, max_threads, show_datatypes,
41993
bd6296de1432 reintroduced "show_skolems" option -- useful when too many Skolems are displayed
blanchet
parents: 41992
diff changeset
   237
         show_skolems, show_consts, evals, formats, atomss, max_potential,
bd6296de1432 reintroduced "show_skolems" option -- useful when too many Skolems are displayed
blanchet
parents: 41992
diff changeset
   238
         max_genuine, check_potential, check_genuine, batch_size, ...} = params
33192
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   239
    val state_ref = Unsynchronized.ref state
46086
096697aec8a7 rationalized output (a bit)
blanchet
parents: 45666
diff changeset
   240
    fun pprint print =
43022
7d3ce43d9464 handle non-auto try case gracefully in Nitpick
blanchet
parents: 43020
diff changeset
   241
      if mode = Auto_Try then
33192
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   242
        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
   243
        o Pretty.chunks o cons (Pretty.str "") o single
45666
d83797ef0d2d separate module for concrete Isabelle markup;
wenzelm
parents: 44395
diff changeset
   244
        o Pretty.mark Isabelle_Markup.hilite
33192
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   245
      else
46086
096697aec8a7 rationalized output (a bit)
blanchet
parents: 45666
diff changeset
   246
        print o Pretty.string_of
47559
366838a5e235 fixed Auto Nitpick's output
blanchet
parents: 47490
diff changeset
   247
    val pprint_a = pprint Output.urgent_message
47560
e30323bfc93c added SZS status wrappers in TPTP mode
blanchet
parents: 47559
diff changeset
   248
    fun pprint_nt f = () |> is_mode_nt mode ? pprint Output.urgent_message o f
46086
096697aec8a7 rationalized output (a bit)
blanchet
parents: 45666
diff changeset
   249
    fun pprint_v f = () |> verbose ? pprint Output.urgent_message o f
096697aec8a7 rationalized output (a bit)
blanchet
parents: 45666
diff changeset
   250
    fun pprint_d f = () |> debug ? pprint tracing o f
096697aec8a7 rationalized output (a bit)
blanchet
parents: 45666
diff changeset
   251
    val print = pprint Output.urgent_message o curry Pretty.blk 0 o pstrs
47560
e30323bfc93c added SZS status wrappers in TPTP mode
blanchet
parents: 47559
diff changeset
   252
    fun print_t f = () |> mode = TPTP ? print o f
39345
062c10ff848c remove unreferenced identifiers
blanchet
parents: 39316
diff changeset
   253
(*
46086
096697aec8a7 rationalized output (a bit)
blanchet
parents: 45666
diff changeset
   254
    val print_g = pprint tracing o Pretty.str
39345
062c10ff848c remove unreferenced identifiers
blanchet
parents: 39316
diff changeset
   255
*)
47560
e30323bfc93c added SZS status wrappers in TPTP mode
blanchet
parents: 47559
diff changeset
   256
    val print_nt = pprint_nt o K o plazy
33568
532b915afa14 don't run Nitpick at all if Kodkodi is not installed (as indicated by the $KODKODI variable)
blanchet
parents: 33566
diff changeset
   257
    val print_v = pprint_v o K o plazy
33192
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   258
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   259
    fun check_deadline () =
41051
2ed1b971fc20 give the inner timeout mechanism a chance, since it gives more precise information to the user
blanchet
parents: 41048
diff changeset
   260
      if passed_deadline deadline then raise TimeLimit.TimeOut else ()
33192
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   261
47715
04400144c6fc handle TPTP definitions as definitions in Nitpick rather than as axioms
blanchet
parents: 47670
diff changeset
   262
    val (def_assm_ts, nondef_assm_ts) =
04400144c6fc handle TPTP definitions as definitions in Nitpick rather than as axioms
blanchet
parents: 47670
diff changeset
   263
      if assms orelse mode <> Normal then (def_assm_ts, nondef_assm_ts)
04400144c6fc handle TPTP definitions as definitions in Nitpick rather than as axioms
blanchet
parents: 47670
diff changeset
   264
      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
   265
    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
   266
      if step = 0 then
47560
e30323bfc93c added SZS status wrappers in TPTP mode
blanchet
parents: 47559
diff changeset
   267
        print_nt (fn () => "Nitpicking formula...")
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
   268
      else
47560
e30323bfc93c added SZS status wrappers in TPTP mode
blanchet
parents: 47559
diff changeset
   269
        pprint_nt (fn () => Pretty.chunks (
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
   270
            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
   271
                (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
   272
                   "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
   273
                 else
47715
04400144c6fc handle TPTP definitions as definitions in Nitpick rather than as axioms
blanchet
parents: 47670
diff changeset
   274
                   "goal")) [Logic.list_implies (nondef_assm_ts, orig_t)]))
41278
8e1cde88aae6 added a timestamp to Nitpick in verbose mode for debugging purposes;
blanchet
parents: 41052
diff changeset
   275
    val _ = print_v (enclose "Timestamp: " "." o Date.fmt "%H:%M:%S"
8e1cde88aae6 added a timestamp to Nitpick in verbose mode for debugging purposes;
blanchet
parents: 41052
diff changeset
   276
                     o Date.fromTimeLocal o Time.now)
33192
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   277
    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
   278
                else orig_t
47715
04400144c6fc handle TPTP definitions as definitions in Nitpick rather than as axioms
blanchet
parents: 47670
diff changeset
   279
    val conj_ts = neg_t :: def_assm_ts @ nondef_assm_ts @ evals @ these needs
38169
b51784515471 optimize local "def"s by treating them as definitions
blanchet
parents: 38126
diff changeset
   280
    val tfree_table =
41869
9e367f1c9570 robust handling of types occurring in "eval" and "preconstr" options but not in the goal
blanchet
parents: 41868
diff changeset
   281
      if merge_type_vars then merged_type_var_table_for_terms thy conj_ts
9e367f1c9570 robust handling of types occurring in "eval" and "preconstr" options but not in the goal
blanchet
parents: 41868
diff changeset
   282
      else []
9e367f1c9570 robust handling of types occurring in "eval" and "preconstr" options but not in the goal
blanchet
parents: 41868
diff changeset
   283
    val merge_tfrees = merge_type_vars_in_term thy merge_type_vars tfree_table
9e367f1c9570 robust handling of types occurring in "eval" and "preconstr" options but not in the goal
blanchet
parents: 41868
diff changeset
   284
    val neg_t = neg_t |> merge_tfrees
47715
04400144c6fc handle TPTP definitions as definitions in Nitpick rather than as axioms
blanchet
parents: 47670
diff changeset
   285
    val def_assm_ts = def_assm_ts |> map merge_tfrees
04400144c6fc handle TPTP definitions as definitions in Nitpick rather than as axioms
blanchet
parents: 47670
diff changeset
   286
    val nondef_assm_ts = nondef_assm_ts |> map merge_tfrees
41869
9e367f1c9570 robust handling of types occurring in "eval" and "preconstr" options but not in the goal
blanchet
parents: 41868
diff changeset
   287
    val evals = evals |> map merge_tfrees
41876
03f699556955 simplify "need" option's syntax
blanchet
parents: 41875
diff changeset
   288
    val needs = needs |> Option.map (map merge_tfrees)
47715
04400144c6fc handle TPTP definitions as definitions in Nitpick rather than as axioms
blanchet
parents: 47670
diff changeset
   289
    val conj_ts = neg_t :: def_assm_ts @ nondef_assm_ts @ evals @ these needs
33192
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   290
    val original_max_potential = max_potential
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   291
    val original_max_genuine = max_genuine
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   292
    val max_bisim_depth = fold Integer.max bisim_depths ~1
38240
a44d108a8d39 local versions of Nitpick.register_xxx functions
blanchet
parents: 38214
diff changeset
   293
    val case_names = case_const_names ctxt stds
47715
04400144c6fc handle TPTP definitions as definitions in Nitpick rather than as axioms
blanchet
parents: 47670
diff changeset
   294
    val defs = def_assm_ts @ all_defs_of thy subst
42415
10accf397ab6 use "Spec_Rules" for finding axioms -- more reliable and cleaner
blanchet
parents: 42361
diff changeset
   295
    val nondefs = all_nondefs_of ctxt subst
41791
01d722707a36 always unfold constant defitions marked with "nitpick_def" -- to prevent unfolding, there's already "nitpick_simp"
blanchet
parents: 41789
diff changeset
   296
    val def_tables = const_def_tables ctxt subst defs
42415
10accf397ab6 use "Spec_Rules" for finding axioms -- more reliable and cleaner
blanchet
parents: 42361
diff changeset
   297
    val nondef_table = const_nondef_table nondefs
35335
f715cfde056a support local definitions in Nitpick
blanchet
parents: 35334
diff changeset
   298
    val simp_table = Unsynchronized.ref (const_simp_table ctxt subst)
f715cfde056a support local definitions in Nitpick
blanchet
parents: 35334
diff changeset
   299
    val psimp_table = const_psimp_table ctxt subst
35807
e4d1b5cbd429 added support for "specification" and "ax_specification" constructs to Nitpick
blanchet
parents: 35711
diff changeset
   300
    val choice_spec_table = const_choice_spec_table ctxt subst
42415
10accf397ab6 use "Spec_Rules" for finding axioms -- more reliable and cleaner
blanchet
parents: 42361
diff changeset
   301
    val nondefs =
10accf397ab6 use "Spec_Rules" for finding axioms -- more reliable and cleaner
blanchet
parents: 42361
diff changeset
   302
      nondefs |> filter_out (is_choice_spec_axiom thy choice_spec_table)
41791
01d722707a36 always unfold constant defitions marked with "nitpick_def" -- to prevent unfolding, there's already "nitpick_simp"
blanchet
parents: 41789
diff changeset
   303
    val intro_table = inductive_intro_table ctxt subst def_tables
33192
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   304
    val ground_thm_table = ground_theorem_table thy
38240
a44d108a8d39 local versions of Nitpick.register_xxx functions
blanchet
parents: 38214
diff changeset
   305
    val ersatz_table = ersatz_table ctxt
41007
75275c796b46 use ML SAT solvers up to a certain time limit, then switch to faster solvers with a timeout -- this becomes necessary with the new, more powerful monotonicity calculus
blanchet
parents: 41001
diff changeset
   306
    val hol_ctxt as {wf_cache, ...} =
33192
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   307
      {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
   308
       stds = stds, wfs = wfs, user_axioms = user_axioms, debug = debug,
38209
3d1d928dce50 added "whack"
blanchet
parents: 38188
diff changeset
   309
       whacks = whacks, binary_ints = binary_ints,
3d1d928dce50 added "whack"
blanchet
parents: 38188
diff changeset
   310
       destroy_constrs = destroy_constrs, specialize = specialize,
41871
394eef237bd1 lower threshold for implicitly using "nitpick_simp" for predicate definitions when "total_consts" is on
blanchet
parents: 41869
diff changeset
   311
       star_linear_preds = star_linear_preds, total_consts = total_consts,
41875
e3cd0dce9b1a renamed "preconstr" option "need"
blanchet
parents: 41872
diff changeset
   312
       needs = needs, tac_timeout = tac_timeout, evals = evals,
41871
394eef237bd1 lower threshold for implicitly using "nitpick_simp" for predicate definitions when "total_consts" is on
blanchet
parents: 41869
diff changeset
   313
       case_names = case_names, def_tables = def_tables,
42415
10accf397ab6 use "Spec_Rules" for finding axioms -- more reliable and cleaner
blanchet
parents: 42361
diff changeset
   314
       nondef_table = nondef_table, nondefs = nondefs, simp_table = simp_table,
10accf397ab6 use "Spec_Rules" for finding axioms -- more reliable and cleaner
blanchet
parents: 42361
diff changeset
   315
       psimp_table = psimp_table, choice_spec_table = choice_spec_table,
10accf397ab6 use "Spec_Rules" for finding axioms -- more reliable and cleaner
blanchet
parents: 42361
diff changeset
   316
       intro_table = intro_table, ground_thm_table = ground_thm_table,
10accf397ab6 use "Spec_Rules" for finding axioms -- more reliable and cleaner
blanchet
parents: 42361
diff changeset
   317
       ersatz_table = ersatz_table, skolems = Unsynchronized.ref [],
10accf397ab6 use "Spec_Rules" for finding axioms -- more reliable and cleaner
blanchet
parents: 42361
diff changeset
   318
       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
   319
       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
   320
       constr_cache = Unsynchronized.ref []}
41789
7c7b68b06c1a don't distinguish between "fixes" and other free variables -- this confuses users
blanchet
parents: 41772
diff changeset
   321
    val pseudo_frees = []
41869
9e367f1c9570 robust handling of types occurring in "eval" and "preconstr" options but not in the goal
blanchet
parents: 41868
diff changeset
   322
    val real_frees = fold Term.add_frees conj_ts []
9e367f1c9570 robust handling of types occurring in "eval" and "preconstr" options but not in the goal
blanchet
parents: 41868
diff changeset
   323
    val _ = null (fold Term.add_tvars conj_ts []) orelse
9e367f1c9570 robust handling of types occurring in "eval" and "preconstr" options but not in the goal
blanchet
parents: 41868
diff changeset
   324
            error "Nitpick cannot handle goals with schematic type variables."
41875
e3cd0dce9b1a renamed "preconstr" option "need"
blanchet
parents: 41872
diff changeset
   325
    val (nondef_ts, def_ts, need_ts, got_all_mono_user_axioms,
41803
ef13e3b7cbaf more work on "fix_datatype_vals" optimization (renamed "preconstruct")
blanchet
parents: 41802
diff changeset
   326
         no_poly_user_axioms, binarize) =
47715
04400144c6fc handle TPTP definitions as definitions in Nitpick rather than as axioms
blanchet
parents: 47670
diff changeset
   327
      preprocess_formulas hol_ctxt nondef_assm_ts neg_t
33192
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   328
    val got_all_user_axioms =
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   329
      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
   330
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   331
    fun print_wf (x, (gfp, wf)) =
47560
e30323bfc93c added SZS status wrappers in TPTP mode
blanchet
parents: 47559
diff changeset
   332
      pprint_nt (fn () => Pretty.blk (0,
33192
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   333
          pstrs ("The " ^ (if gfp then "co" else "") ^ "inductive predicate \"")
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   334
          @ Syntax.pretty_term ctxt (Const x) ::
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   335
          pstrs (if wf then
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   336
                   "\" was proved well-founded. Nitpick can compute it \
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   337
                   \efficiently."
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   338
                 else
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   339
                   "\" 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
   340
                   \unroll it.")))
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   341
    val _ = if verbose then List.app print_wf (!wf_cache) else ()
38171
5f2ea92319e0 fix soundness bug w.r.t. "Suc" with "binary_ints"
blanchet
parents: 38170
diff changeset
   342
    val das_wort_formula = if falsify then "Negated conjecture" else "Formula"
33192
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   343
    val _ =
35386
45a4e19d3ebd more work on the new monotonicity stuff in Nitpick
blanchet
parents: 35385
diff changeset
   344
      pprint_d (fn () => Pretty.chunks
38171
5f2ea92319e0 fix soundness bug w.r.t. "Suc" with "binary_ints"
blanchet
parents: 38170
diff changeset
   345
          (pretties_for_formulas ctxt das_wort_formula [hd nondef_ts] @
35386
45a4e19d3ebd more work on the new monotonicity stuff in Nitpick
blanchet
parents: 35385
diff changeset
   346
           pretties_for_formulas ctxt "Relevant definitional axiom" def_ts @
45a4e19d3ebd more work on the new monotonicity stuff in Nitpick
blanchet
parents: 35385
diff changeset
   347
           pretties_for_formulas ctxt "Relevant nondefinitional axiom"
45a4e19d3ebd more work on the new monotonicity stuff in Nitpick
blanchet
parents: 35385
diff changeset
   348
                                 (tl nondef_ts)))
45a4e19d3ebd more work on the new monotonicity stuff in Nitpick
blanchet
parents: 35385
diff changeset
   349
    val _ = List.app (ignore o Term.type_of) (nondef_ts @ def_ts)
33192
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   350
            handle TYPE (_, Ts, ts) =>
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   351
                   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
   352
41801
ed77524f3429 first steps in implementing "fix_datatype_vals" optimization
blanchet
parents: 41793
diff changeset
   353
    val nondef_us = nondef_ts |> map (nut_from_term hol_ctxt Eq)
ed77524f3429 first steps in implementing "fix_datatype_vals" optimization
blanchet
parents: 41793
diff changeset
   354
    val def_us = def_ts |> map (nut_from_term hol_ctxt DefEq)
41875
e3cd0dce9b1a renamed "preconstr" option "need"
blanchet
parents: 41872
diff changeset
   355
    val need_us = need_ts |> map (nut_from_term hol_ctxt Eq)
33558
a2db56854b83 optimized Nitpick's encoding and rendering of datatypes whose constructors don't appear in the problem
blanchet
parents: 33556
diff changeset
   356
    val (free_names, const_names) =
41888
79f837c2e33b don't forget to look for constants appearing only in "need" option -- otherwise we get exceptions in "the_name" later on
blanchet
parents: 41876
diff changeset
   357
      fold add_free_and_const_names (nondef_us @ def_us @ need_us) ([], [])
33558
a2db56854b83 optimized Nitpick's encoding and rendering of datatypes whose constructors don't appear in the problem
blanchet
parents: 33556
diff changeset
   358
    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
   359
      List.partition (is_sel o nickname_of) const_names
46114
e6d33b200f42 remove subtlety whose justification got lost in time -- the new code is possibly less precise but sounder
blanchet
parents: 46103
diff changeset
   360
    val sound_finitizes = none_true finitizes
34982
7b8c366e34a2 added support for nonstandard models to Nitpick (based on an idea by Koen Claessen) and did other fixes to Nitpick
blanchet
parents: 34938
diff changeset
   361
    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
   362
(*
41888
79f837c2e33b don't forget to look for constants appearing only in "need" option -- otherwise we get exceptions in "the_name" later on
blanchet
parents: 41876
diff changeset
   363
    val _ =
79f837c2e33b don't forget to look for constants appearing only in "need" option -- otherwise we get exceptions in "the_name" later on
blanchet
parents: 41876
diff changeset
   364
      List.app (print_g o string_for_nut ctxt) (nondef_us @ def_us @ need_us)
33558
a2db56854b83 optimized Nitpick's encoding and rendering of datatypes whose constructors don't appear in the problem
blanchet
parents: 33556
diff changeset
   365
*)
a2db56854b83 optimized Nitpick's encoding and rendering of datatypes whose constructors don't appear in the problem
blanchet
parents: 33556
diff changeset
   366
34121
5e831d805118 get rid of polymorphic equality in Nitpick's code + a few minor cleanups
blanchet
parents: 34039
diff changeset
   367
    val unique_scope = forall (curry (op =) 1 o length o snd) cards_assigns
35385
29f81babefd7 improved precision of infinite "shallow" datatypes in Nitpick;
blanchet
parents: 35384
diff changeset
   368
    fun monotonicity_message Ts extra =
38188
7f12a03c513c better "Pretty" handling
blanchet
parents: 38182
diff changeset
   369
      let val pretties = map (pretty_maybe_quote o pretty_for_type ctxt) Ts in
7f12a03c513c better "Pretty" handling
blanchet
parents: 38182
diff changeset
   370
        Pretty.blk (0,
7f12a03c513c better "Pretty" handling
blanchet
parents: 38182
diff changeset
   371
          pstrs ("The type" ^ plural_s_for_list pretties ^ " ") @
7f12a03c513c better "Pretty" handling
blanchet
parents: 38182
diff changeset
   372
          pretty_serial_commas "and" pretties @
7f12a03c513c better "Pretty" handling
blanchet
parents: 38182
diff changeset
   373
          pstrs (" " ^
42959
ee829022381d use \<emdash> rather than \<midarrow>
blanchet
parents: 42486
diff changeset
   374
                 (if none_true monos then
ee829022381d use \<emdash> rather than \<midarrow>
blanchet
parents: 42486
diff changeset
   375
                    "passed the monotonicity test"
ee829022381d use \<emdash> rather than \<midarrow>
blanchet
parents: 42486
diff changeset
   376
                  else
ee829022381d use \<emdash> rather than \<midarrow>
blanchet
parents: 42486
diff changeset
   377
                    (if length pretties = 1 then "is" else "are") ^
ee829022381d use \<emdash> rather than \<midarrow>
blanchet
parents: 42486
diff changeset
   378
                    " considered monotonic") ^
ee829022381d use \<emdash> rather than \<midarrow>
blanchet
parents: 42486
diff changeset
   379
                 ". " ^ extra))
35385
29f81babefd7 improved precision of infinite "shallow" datatypes in Nitpick;
blanchet
parents: 35384
diff changeset
   380
      end
35665
ff2bf50505ab added "finitize" option to Nitpick + remove dependency on "Coinductive_List"
blanchet
parents: 35408
diff changeset
   381
    fun is_type_fundamentally_monotonic T =
38240
a44d108a8d39 local versions of Nitpick.register_xxx functions
blanchet
parents: 38214
diff changeset
   382
      (is_datatype ctxt stds T andalso not (is_quot_type ctxt T) andalso
37256
0dca1ec52999 thread along context instead of theory for typedef lookup
blanchet
parents: 37213
diff changeset
   383
       (not (is_pure_typedef ctxt T) orelse is_univ_typedef ctxt T)) orelse
38240
a44d108a8d39 local versions of Nitpick.register_xxx functions
blanchet
parents: 38214
diff changeset
   384
      is_number_type ctxt T orelse is_bit_type T
35385
29f81babefd7 improved precision of infinite "shallow" datatypes in Nitpick;
blanchet
parents: 35384
diff changeset
   385
    fun is_type_actually_monotonic T =
41001
11715564e2ad removed old baggage from monotonicity calculus -- the "calculus" option didn't really work anyway because of on-the-fly simplifications
blanchet
parents: 40993
diff changeset
   386
      formulas_monotonic hol_ctxt binarize T (nondef_ts, def_ts)
35665
ff2bf50505ab added "finitize" option to Nitpick + remove dependency on "Coinductive_List"
blanchet
parents: 35408
diff changeset
   387
    fun is_type_kind_of_monotonic T =
ff2bf50505ab added "finitize" option to Nitpick + remove dependency on "Coinductive_List"
blanchet
parents: 35408
diff changeset
   388
      case triple_lookup (type_match thy) monos T of
ff2bf50505ab added "finitize" option to Nitpick + remove dependency on "Coinductive_List"
blanchet
parents: 35408
diff changeset
   389
        SOME (SOME false) => false
ff2bf50505ab added "finitize" option to Nitpick + remove dependency on "Coinductive_List"
blanchet
parents: 35408
diff changeset
   390
      | _ => is_type_actually_monotonic T
34936
c4f04bee79f3 some work on Nitpick's support for quotient types;
blanchet
parents: 34935
diff changeset
   391
    fun is_type_monotonic T =
33192
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   392
      unique_scope orelse
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   393
      case triple_lookup (type_match thy) monos T of
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   394
        SOME (SOME b) => b
35665
ff2bf50505ab added "finitize" option to Nitpick + remove dependency on "Coinductive_List"
blanchet
parents: 35408
diff changeset
   395
      | _ => is_type_fundamentally_monotonic T orelse
ff2bf50505ab added "finitize" option to Nitpick + remove dependency on "Coinductive_List"
blanchet
parents: 35408
diff changeset
   396
             is_type_actually_monotonic T
41793
c7a2669ae75d tweaked Nitpick based on C++ memory model example
blanchet
parents: 41791
diff changeset
   397
    fun is_deep_datatype_finitizable T =
c7a2669ae75d tweaked Nitpick based on C++ memory model example
blanchet
parents: 41791
diff changeset
   398
      triple_lookup (type_match thy) finitizes T = SOME (SOME true)
41052
3db267a01c1d remove the "fin_fun" optimization in Nitpick -- it was always a hack and didn't help much
blanchet
parents: 41051
diff changeset
   399
    fun is_shallow_datatype_finitizable (T as Type (@{type_name fun_box}, _)) =
35665
ff2bf50505ab added "finitize" option to Nitpick + remove dependency on "Coinductive_List"
blanchet
parents: 35408
diff changeset
   400
        is_type_kind_of_monotonic T
ff2bf50505ab added "finitize" option to Nitpick + remove dependency on "Coinductive_List"
blanchet
parents: 35408
diff changeset
   401
      | is_shallow_datatype_finitizable T =
ff2bf50505ab added "finitize" option to Nitpick + remove dependency on "Coinductive_List"
blanchet
parents: 35408
diff changeset
   402
        case triple_lookup (type_match thy) finitizes T of
ff2bf50505ab added "finitize" option to Nitpick + remove dependency on "Coinductive_List"
blanchet
parents: 35408
diff changeset
   403
          SOME (SOME b) => b
ff2bf50505ab added "finitize" option to Nitpick + remove dependency on "Coinductive_List"
blanchet
parents: 35408
diff changeset
   404
        | _ => is_type_kind_of_monotonic T
35385
29f81babefd7 improved precision of infinite "shallow" datatypes in Nitpick;
blanchet
parents: 35384
diff changeset
   405
    fun is_datatype_deep T =
46103
1e35730bd869 always treat "unit" as a deep datatype, so that we get a good interaction with the record syntax (2.7 of the Nitpick manual)
blanchet
parents: 46086
diff changeset
   406
      not standard orelse T = @{typ unit} orelse T = nat_T orelse
1e35730bd869 always treat "unit" as a deep datatype, so that we get a good interaction with the record syntax (2.7 of the Nitpick manual)
blanchet
parents: 46086
diff changeset
   407
      is_word_type T orelse
35385
29f81babefd7 improved precision of infinite "shallow" datatypes in Nitpick;
blanchet
parents: 35384
diff changeset
   408
      exists (curry (op =) T o domain_type o type_of) sel_names
35386
45a4e19d3ebd more work on the new monotonicity stuff in Nitpick
blanchet
parents: 35385
diff changeset
   409
    val all_Ts = ground_types_in_terms hol_ctxt binarize (nondef_ts @ def_ts)
35408
b48ab741683b modernized structure Term_Ord;
wenzelm
parents: 35386
diff changeset
   410
                 |> sort Term_Ord.typ_ord
38214
8164c91039ea added a friendly warning
blanchet
parents: 38212
diff changeset
   411
    val _ =
8164c91039ea added a friendly warning
blanchet
parents: 38212
diff changeset
   412
      if verbose andalso binary_ints = SOME true andalso
8164c91039ea added a friendly warning
blanchet
parents: 38212
diff changeset
   413
         exists (member (op =) [nat_T, int_T]) all_Ts then
8164c91039ea added a friendly warning
blanchet
parents: 38212
diff changeset
   414
        print_v (K "The option \"binary_ints\" will be ignored because of the \
8164c91039ea added a friendly warning
blanchet
parents: 38212
diff changeset
   415
                   \presence of rationals, reals, \"Suc\", \"gcd\", or \"lcm\" \
8164c91039ea added a friendly warning
blanchet
parents: 38212
diff changeset
   416
                   \in the problem or because of the \"non_std\" option.")
8164c91039ea added a friendly warning
blanchet
parents: 38212
diff changeset
   417
      else
8164c91039ea added a friendly warning
blanchet
parents: 38212
diff changeset
   418
        ()
8164c91039ea added a friendly warning
blanchet
parents: 38212
diff changeset
   419
    val _ =
43022
7d3ce43d9464 handle non-auto try case gracefully in Nitpick
blanchet
parents: 43020
diff changeset
   420
      if mode = Normal andalso
38214
8164c91039ea added a friendly warning
blanchet
parents: 38212
diff changeset
   421
         exists (fn Type (@{type_name Datatype.node}, _) => true | _ => false)
8164c91039ea added a friendly warning
blanchet
parents: 38212
diff changeset
   422
                all_Ts then
47560
e30323bfc93c added SZS status wrappers in TPTP mode
blanchet
parents: 47559
diff changeset
   423
        print_nt (K ("Warning: The problem involves directly or indirectly the \
e30323bfc93c added SZS status wrappers in TPTP mode
blanchet
parents: 47559
diff changeset
   424
                     \internal type " ^ quote @{type_name Datatype.node} ^
e30323bfc93c added SZS status wrappers in TPTP mode
blanchet
parents: 47559
diff changeset
   425
                     ". This type is very Nitpick-unfriendly, and its presence \
e30323bfc93c added SZS status wrappers in TPTP mode
blanchet
parents: 47559
diff changeset
   426
                     \usually indicates either a failure of abstraction or a \
e30323bfc93c added SZS status wrappers in TPTP mode
blanchet
parents: 47559
diff changeset
   427
                     \quirk in Nitpick."))
38214
8164c91039ea added a friendly warning
blanchet
parents: 38212
diff changeset
   428
      else
8164c91039ea added a friendly warning
blanchet
parents: 38212
diff changeset
   429
        ()
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
   430
    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
   431
    val _ =
34936
c4f04bee79f3 some work on Nitpick's support for quotient types;
blanchet
parents: 34935
diff changeset
   432
      if verbose andalso not unique_scope then
35665
ff2bf50505ab added "finitize" option to Nitpick + remove dependency on "Coinductive_List"
blanchet
parents: 35408
diff changeset
   433
        case filter_out is_type_fundamentally_monotonic mono_Ts of
34936
c4f04bee79f3 some work on Nitpick's support for quotient types;
blanchet
parents: 34935
diff changeset
   434
          [] => ()
c4f04bee79f3 some work on Nitpick's support for quotient types;
blanchet
parents: 34935
diff changeset
   435
        | interesting_mono_Ts =>
38188
7f12a03c513c better "Pretty" handling
blanchet
parents: 38182
diff changeset
   436
          pprint_v (K (monotonicity_message interesting_mono_Ts
7f12a03c513c better "Pretty" handling
blanchet
parents: 38182
diff changeset
   437
                          "Nitpick might be able to skip some scopes."))
33192
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
        ()
35385
29f81babefd7 improved precision of infinite "shallow" datatypes in Nitpick;
blanchet
parents: 35384
diff changeset
   440
    val (deep_dataTs, shallow_dataTs) =
37256
0dca1ec52999 thread along context instead of theory for typedef lookup
blanchet
parents: 37213
diff changeset
   441
      all_Ts |> filter (is_datatype ctxt stds)
0dca1ec52999 thread along context instead of theory for typedef lookup
blanchet
parents: 37213
diff changeset
   442
             |> List.partition is_datatype_deep
35385
29f81babefd7 improved precision of infinite "shallow" datatypes in Nitpick;
blanchet
parents: 35384
diff changeset
   443
    val finitizable_dataTs =
41793
c7a2669ae75d tweaked Nitpick based on C++ memory model example
blanchet
parents: 41791
diff changeset
   444
      (deep_dataTs |> filter_out (is_finite_type hol_ctxt)
c7a2669ae75d tweaked Nitpick based on C++ memory model example
blanchet
parents: 41791
diff changeset
   445
                   |> filter is_deep_datatype_finitizable) @
c7a2669ae75d tweaked Nitpick based on C++ memory model example
blanchet
parents: 41791
diff changeset
   446
      (shallow_dataTs |> filter_out (is_finite_type hol_ctxt)
c7a2669ae75d tweaked Nitpick based on C++ memory model example
blanchet
parents: 41791
diff changeset
   447
                      |> filter is_shallow_datatype_finitizable)
35385
29f81babefd7 improved precision of infinite "shallow" datatypes in Nitpick;
blanchet
parents: 35384
diff changeset
   448
    val _ =
29f81babefd7 improved precision of infinite "shallow" datatypes in Nitpick;
blanchet
parents: 35384
diff changeset
   449
      if verbose andalso not (null finitizable_dataTs) then
38188
7f12a03c513c better "Pretty" handling
blanchet
parents: 38182
diff changeset
   450
        pprint_v (K (monotonicity_message finitizable_dataTs
7f12a03c513c better "Pretty" handling
blanchet
parents: 38182
diff changeset
   451
                         "Nitpick can use a more precise finite encoding."))
35385
29f81babefd7 improved precision of infinite "shallow" datatypes in Nitpick;
blanchet
parents: 35384
diff changeset
   452
      else
29f81babefd7 improved precision of infinite "shallow" datatypes in Nitpick;
blanchet
parents: 35384
diff changeset
   453
        ()
35183
8580ba651489 reintroduce structural induction hint in Nitpick
blanchet
parents: 35181
diff changeset
   454
    (* This detection code is an ugly hack. Fortunately, it is used only to
8580ba651489 reintroduce structural induction hint in Nitpick
blanchet
parents: 35181
diff changeset
   455
       provide a hint to the user. *)
8580ba651489 reintroduce structural induction hint in Nitpick
blanchet
parents: 35181
diff changeset
   456
    fun is_struct_induct_step (name, (Rule_Cases.Case {fixes, assumes, ...}, _)) =
8580ba651489 reintroduce structural induction hint in Nitpick
blanchet
parents: 35181
diff changeset
   457
      not (null fixes) andalso
8580ba651489 reintroduce structural induction hint in Nitpick
blanchet
parents: 35181
diff changeset
   458
      exists (String.isSuffix ".hyps" o fst) assumes andalso
8580ba651489 reintroduce structural induction hint in Nitpick
blanchet
parents: 35181
diff changeset
   459
      exists (exists (curry (op =) name o shortest_name o fst)
8580ba651489 reintroduce structural induction hint in Nitpick
blanchet
parents: 35181
diff changeset
   460
              o datatype_constrs hol_ctxt) deep_dataTs
8580ba651489 reintroduce structural induction hint in Nitpick
blanchet
parents: 35181
diff changeset
   461
    val likely_in_struct_induct_step =
42361
23f352990944 modernized structure Proof_Context;
wenzelm
parents: 41995
diff changeset
   462
      exists is_struct_induct_step (Proof_Context.cases_of ctxt)
35183
8580ba651489 reintroduce structural induction hint in Nitpick
blanchet
parents: 35181
diff changeset
   463
    val _ = if standard andalso likely_in_struct_induct_step then
47560
e30323bfc93c added SZS status wrappers in TPTP mode
blanchet
parents: 47559
diff changeset
   464
              pprint_nt (fn () => Pretty.blk (0,
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
   465
                  pstrs "Hint: To check that the induction hypothesis is \
35177
168041f24f80 various cosmetic changes to Nitpick
blanchet
parents: 35075
diff changeset
   466
                        \general enough, try this command: " @
45666
d83797ef0d2d separate module for concrete Isabelle markup;
wenzelm
parents: 44395
diff changeset
   467
                  [Pretty.mark Isabelle_Markup.sendback (Pretty.blk (0,
35183
8580ba651489 reintroduce structural induction hint in Nitpick
blanchet
parents: 35181
diff changeset
   468
                       pstrs ("nitpick [non_std, show_all]")))] @ pstrs "."))
34982
7b8c366e34a2 added support for nonstandard models to Nitpick (based on an idea by Koen Claessen) and did other fixes to Nitpick
blanchet
parents: 34938
diff changeset
   469
            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
   470
              ()
33192
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   471
(*
36128
a3d8d5329438 make Nitpick output everything to tracing in debug mode;
blanchet
parents: 36126
diff changeset
   472
    val _ = print_g "Monotonic types:"
a3d8d5329438 make Nitpick output everything to tracing in debug mode;
blanchet
parents: 36126
diff changeset
   473
    val _ = List.app (print_g o string_for_type ctxt) mono_Ts
a3d8d5329438 make Nitpick output everything to tracing in debug mode;
blanchet
parents: 36126
diff changeset
   474
    val _ = print_g "Nonmonotonic types:"
a3d8d5329438 make Nitpick output everything to tracing in debug mode;
blanchet
parents: 36126
diff changeset
   475
    val _ = List.app (print_g o string_for_type ctxt) nonmono_Ts
33192
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   476
*)
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   477
36384
76d5fd5a45fb cosmetics
blanchet
parents: 36380
diff changeset
   478
    val incremental = Int.max (max_potential, max_genuine) >= 2
76d5fd5a45fb cosmetics
blanchet
parents: 36380
diff changeset
   479
    val actual_sat_solver =
33192
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   480
      if sat_solver <> "smart" then
36384
76d5fd5a45fb cosmetics
blanchet
parents: 36380
diff changeset
   481
        if incremental andalso
34936
c4f04bee79f3 some work on Nitpick's support for quotient types;
blanchet
parents: 34935
diff changeset
   482
           not (member (op =) (Kodkod_SAT.configured_sat_solvers true)
35333
f61de25f71f9 distinguish between Kodkodi warnings and errors in Nitpick;
blanchet
parents: 35280
diff changeset
   483
                       sat_solver) then
47560
e30323bfc93c added SZS status wrappers in TPTP mode
blanchet
parents: 47559
diff changeset
   484
          (print_nt (K ("An incremental SAT solver is required: \"SAT4J\" will \
e30323bfc93c added SZS status wrappers in TPTP mode
blanchet
parents: 47559
diff changeset
   485
                        \be used instead of " ^ quote sat_solver ^ "."));
33192
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   486
           "SAT4J")
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   487
        else
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   488
          sat_solver
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   489
      else
36384
76d5fd5a45fb cosmetics
blanchet
parents: 36380
diff changeset
   490
        Kodkod_SAT.smart_sat_solver_name incremental
33192
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   491
    val _ =
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   492
      if sat_solver = "smart" then
36384
76d5fd5a45fb cosmetics
blanchet
parents: 36380
diff changeset
   493
        print_v (fn () =>
76d5fd5a45fb cosmetics
blanchet
parents: 36380
diff changeset
   494
            "Using SAT solver " ^ quote actual_sat_solver ^ ". The following" ^
76d5fd5a45fb cosmetics
blanchet
parents: 36380
diff changeset
   495
            (if incremental then " incremental " else " ") ^
76d5fd5a45fb cosmetics
blanchet
parents: 36380
diff changeset
   496
            "solvers are configured: " ^
76d5fd5a45fb cosmetics
blanchet
parents: 36380
diff changeset
   497
            commas_quote (Kodkod_SAT.configured_sat_solvers incremental) ^ ".")
33192
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   498
      else
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   499
        ()
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   500
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   501
    val too_big_scopes = Unsynchronized.ref []
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   502
35185
9b8f351cced6 added yet another hint to Nitpick's output, this time warning about problems for which nothing was effectively tested
blanchet
parents: 35183
diff changeset
   503
    fun problem_for_scope unsound
34124
c4628a1dcf75 added support for binary nat/int representation to Nitpick
blanchet
parents: 34123
diff changeset
   504
            (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
   505
      let
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   506
        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
   507
                            (!too_big_scopes)) orelse
c4f04bee79f3 some work on Nitpick's support for quotient types;
blanchet
parents: 34935
diff changeset
   508
                raise TOO_LARGE ("Nitpick.pick_them_nits_in_term.\
c4f04bee79f3 some work on Nitpick's support for quotient types;
blanchet
parents: 34935
diff changeset
   509
                                 \problem_for_scope", "too large scope")
33192
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   510
(*
36128
a3d8d5329438 make Nitpick output everything to tracing in debug mode;
blanchet
parents: 36126
diff changeset
   511
        val _ = print_g "Offsets:"
33192
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   512
        val _ = List.app (fn (T, j0) =>
36128
a3d8d5329438 make Nitpick output everything to tracing in debug mode;
blanchet
parents: 36126
diff changeset
   513
                             print_g (string_for_type ctxt T ^ " = " ^
a3d8d5329438 make Nitpick output everything to tracing in debug mode;
blanchet
parents: 36126
diff changeset
   514
                                    string_of_int j0))
33192
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   515
                         (Typtab.dest ofs)
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   516
*)
41858
37ce158d6266 if "total_consts" is set, report cex's as quasi-genuine
blanchet
parents: 41856
diff changeset
   517
        val effective_total_consts =
41856
7244589c8ccc added "total_consts" option
blanchet
parents: 41803
diff changeset
   518
          case total_consts of
7244589c8ccc added "total_consts" option
blanchet
parents: 41803
diff changeset
   519
            SOME b => b
7244589c8ccc added "total_consts" option
blanchet
parents: 41803
diff changeset
   520
          | NONE => forall (is_exact_type datatypes true) all_Ts
33192
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   521
        val main_j0 = offset_of_type ofs bool_T
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   522
        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
   523
        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
   524
        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
   525
                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
   526
                           "bad offsets")
33192
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   527
        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
   528
        val (free_names, rep_table) =
38170
d74b66ec02ce handle free variables even more gracefully;
blanchet
parents: 38169
diff changeset
   529
          choose_reps_for_free_vars scope pseudo_frees free_names
d74b66ec02ce handle free variables even more gracefully;
blanchet
parents: 38169
diff changeset
   530
                                    NameTable.empty
33192
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   531
        val (sel_names, rep_table) = choose_reps_for_all_sels scope rep_table
38170
d74b66ec02ce handle free variables even more gracefully;
blanchet
parents: 38169
diff changeset
   532
        val (nonsel_names, rep_table) =
41858
37ce158d6266 if "total_consts" is set, report cex's as quasi-genuine
blanchet
parents: 41856
diff changeset
   533
          choose_reps_for_consts scope effective_total_consts nonsel_names
37ce158d6266 if "total_consts" is set, report cex's as quasi-genuine
blanchet
parents: 41856
diff changeset
   534
                                 rep_table
38182
747f8077b09a more helpful message
blanchet
parents: 38171
diff changeset
   535
        val (guiltiest_party, min_highest_arity) =
747f8077b09a more helpful message
blanchet
parents: 38171
diff changeset
   536
          NameTable.fold (fn (name, R) => fn (s, n) =>
747f8077b09a more helpful message
blanchet
parents: 38171
diff changeset
   537
                             let val n' = arity_of_rep R in
747f8077b09a more helpful message
blanchet
parents: 38171
diff changeset
   538
                               if n' > n then (nickname_of name, n') else (s, n)
747f8077b09a more helpful message
blanchet
parents: 38171
diff changeset
   539
                             end) rep_table ("", 1)
33192
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   540
        val min_univ_card =
36384
76d5fd5a45fb cosmetics
blanchet
parents: 36380
diff changeset
   541
          NameTable.fold (Integer.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
   542
                         (univ_card nat_card int_card main_j0 [] KK.True)
41897
c24e7fd17464 perform no arity check in debug mode so that we get to see the Kodkod problem
blanchet
parents: 41888
diff changeset
   543
        val _ = if debug then ()
c24e7fd17464 perform no arity check in debug mode so that we get to see the Kodkod problem
blanchet
parents: 41888
diff changeset
   544
                else check_arity guiltiest_party min_univ_card min_highest_arity
33192
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   545
41802
7592a165fa0b more work on "fix_datatype_vals"
blanchet
parents: 41801
diff changeset
   546
        val def_us =
7592a165fa0b more work on "fix_datatype_vals"
blanchet
parents: 41801
diff changeset
   547
          def_us |> map (choose_reps_in_nut scope unsound rep_table true)
7592a165fa0b more work on "fix_datatype_vals"
blanchet
parents: 41801
diff changeset
   548
        val nondef_us =
7592a165fa0b more work on "fix_datatype_vals"
blanchet
parents: 41801
diff changeset
   549
          nondef_us |> map (choose_reps_in_nut scope unsound rep_table false)
41875
e3cd0dce9b1a renamed "preconstr" option "need"
blanchet
parents: 41872
diff changeset
   550
        val need_us =
e3cd0dce9b1a renamed "preconstr" option "need"
blanchet
parents: 41872
diff changeset
   551
          need_us |> map (choose_reps_in_nut scope unsound rep_table false)
33745
daf236998f82 comment out debugging code in Nitpick
blanchet
parents: 33744
diff changeset
   552
(*
36128
a3d8d5329438 make Nitpick output everything to tracing in debug mode;
blanchet
parents: 36126
diff changeset
   553
        val _ = List.app (print_g o string_for_nut ctxt)
33192
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   554
                         (free_names @ sel_names @ nonsel_names @
41888
79f837c2e33b don't forget to look for constants appearing only in "need" option -- otherwise we get exceptions in "the_name" later on
blanchet
parents: 41876
diff changeset
   555
                          nondef_us @ def_us @ need_us)
33745
daf236998f82 comment out debugging code in Nitpick
blanchet
parents: 33744
diff changeset
   556
*)
33192
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   557
        val (free_rels, pool, rel_table) =
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   558
          rename_free_vars free_names initial_pool NameTable.empty
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   559
        val (sel_rels, pool, rel_table) =
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   560
          rename_free_vars sel_names pool rel_table
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   561
        val (other_rels, pool, rel_table) =
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   562
          rename_free_vars nonsel_names pool rel_table
41802
7592a165fa0b more work on "fix_datatype_vals"
blanchet
parents: 41801
diff changeset
   563
        val nondef_us = nondef_us |> map (rename_vars_in_nut pool rel_table)
7592a165fa0b more work on "fix_datatype_vals"
blanchet
parents: 41801
diff changeset
   564
        val def_us = def_us |> map (rename_vars_in_nut pool rel_table)
41875
e3cd0dce9b1a renamed "preconstr" option "need"
blanchet
parents: 41872
diff changeset
   565
        val need_us = need_us |> map (rename_vars_in_nut pool rel_table)
35386
45a4e19d3ebd more work on the new monotonicity stuff in Nitpick
blanchet
parents: 35385
diff changeset
   566
        val nondef_fs = map (kodkod_formula_from_nut ofs kk) nondef_us
35280
54ab4921f826 fixed a few bugs in Nitpick and removed unreferenced variables
blanchet
parents: 35220
diff changeset
   567
        val def_fs = map (kodkod_formula_from_nut ofs kk) def_us
35386
45a4e19d3ebd more work on the new monotonicity stuff in Nitpick
blanchet
parents: 35385
diff changeset
   568
        val formula = fold (fold s_and) [def_fs, nondef_fs] KK.True
35185
9b8f351cced6 added yet another hint to Nitpick's output, this time warning about problems for which nothing was effectively tested
blanchet
parents: 35183
diff changeset
   569
        val comment = (if unsound then "unsound" else "sound") ^ "\n" ^
37146
f652333bbf8e renamed structure PrintMode to Print_Mode, keeping the old name as legacy alias for some time;
wenzelm
parents: 36913
diff changeset
   570
                      Print_Mode.setmp [] multiline_string_for_scope scope
34998
5e492a862b34 four changes to Nitpick:
blanchet
parents: 34982
diff changeset
   571
        val kodkod_sat_solver =
36384
76d5fd5a45fb cosmetics
blanchet
parents: 36380
diff changeset
   572
          Kodkod_SAT.sat_solver_spec actual_sat_solver |> snd
34124
c4628a1dcf75 added support for binary nat/int representation to Nitpick
blanchet
parents: 34123
diff changeset
   573
        val bit_width = if bits = 0 then 16 else bits + 1
36384
76d5fd5a45fb cosmetics
blanchet
parents: 36380
diff changeset
   574
        val delay =
76d5fd5a45fb cosmetics
blanchet
parents: 36380
diff changeset
   575
          if unsound then
76d5fd5a45fb cosmetics
blanchet
parents: 36380
diff changeset
   576
            Option.map (fn time => Time.- (time, Time.now ())) deadline
76d5fd5a45fb cosmetics
blanchet
parents: 36380
diff changeset
   577
            |> unsound_delay_for_timeout
76d5fd5a45fb cosmetics
blanchet
parents: 36380
diff changeset
   578
          else
76d5fd5a45fb cosmetics
blanchet
parents: 36380
diff changeset
   579
            0
76d5fd5a45fb cosmetics
blanchet
parents: 36380
diff changeset
   580
        val settings = [("solver", commas_quote kodkod_sat_solver),
34124
c4628a1dcf75 added support for binary nat/int representation to Nitpick
blanchet
parents: 34123
diff changeset
   581
                        ("bit_width", string_of_int bit_width),
38124
6538e25cf5dd started implementation of custom sym break
blanchet
parents: 38123
diff changeset
   582
                        ("symmetry_breaking", string_of_int kodkod_sym_break),
36386
2132f15b366f Fruhjahrsputz: remove three mostly useless Nitpick options
blanchet
parents: 36385
diff changeset
   583
                        ("sharing", "3"),
2132f15b366f Fruhjahrsputz: remove three mostly useless Nitpick options
blanchet
parents: 36385
diff changeset
   584
                        ("flatten", "false"),
33192
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   585
                        ("delay", signed_string_of_int delay)]
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   586
        val plain_rels = free_rels @ other_rels
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   587
        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
   588
        val plain_axioms = map (declarative_axiom_for_plain_rel kk) plain_rels
41995
03c2d29ec790 optimize Kodkod bounds when "need" is specified
blanchet
parents: 41993
diff changeset
   589
        val need_vals =
03c2d29ec790 optimize Kodkod bounds when "need" is specified
blanchet
parents: 41993
diff changeset
   590
          map (fn dtype as {typ, ...} =>
03c2d29ec790 optimize Kodkod bounds when "need" is specified
blanchet
parents: 41993
diff changeset
   591
                  (typ, needed_values_for_datatype need_us ofs dtype)) datatypes
03c2d29ec790 optimize Kodkod bounds when "need" is specified
blanchet
parents: 41993
diff changeset
   592
        val sel_bounds =
03c2d29ec790 optimize Kodkod bounds when "need" is specified
blanchet
parents: 41993
diff changeset
   593
          map (bound_for_sel_rel ctxt debug need_vals datatypes) sel_rels
35190
ce653cc27a94 make sure that Nitpick uses binary notation consistently if "binary_ints" is enabled
blanchet
parents: 35185
diff changeset
   594
        val dtype_axioms =
41995
03c2d29ec790 optimize Kodkod bounds when "need" is specified
blanchet
parents: 41993
diff changeset
   595
          declarative_axioms_for_datatypes hol_ctxt binarize need_us need_vals
41801
ed77524f3429 first steps in implementing "fix_datatype_vals" optimization
blanchet
parents: 41793
diff changeset
   596
              datatype_sym_break bits ofs kk rel_table datatypes
33192
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   597
        val declarative_axioms = plain_axioms @ dtype_axioms
35220
2bcdae5f4fdb added support for nonstandard "nat"s to Nitpick and fixed bugs in binary "nat"s and "int"s
blanchet
parents: 35190
diff changeset
   598
        val univ_card = Int.max (univ_card nat_card int_card main_j0
2bcdae5f4fdb added support for nonstandard "nat"s to Nitpick and fixed bugs in binary "nat"s and "int"s
blanchet
parents: 35190
diff changeset
   599
                                     (plain_bounds @ sel_bounds) formula,
2bcdae5f4fdb added support for nonstandard "nat"s to Nitpick and fixed bugs in binary "nat"s and "int"s
blanchet
parents: 35190
diff changeset
   600
                                 main_j0 |> bits > 0 ? Integer.add (bits + 1))
38126
8031d099379a added manual symmetry breaking for datatypes
blanchet
parents: 38124
diff changeset
   601
        val (built_in_bounds, built_in_axioms) =
39345
062c10ff848c remove unreferenced identifiers
blanchet
parents: 39316
diff changeset
   602
          bounds_and_axioms_for_built_in_rels_in_formulas debug univ_card
062c10ff848c remove unreferenced identifiers
blanchet
parents: 39316
diff changeset
   603
              nat_card int_card main_j0 (formula :: declarative_axioms)
33192
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   604
        val bounds = built_in_bounds @ plain_bounds @ sel_bounds
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   605
                     |> not debug ? merge_bounds
38126
8031d099379a added manual symmetry breaking for datatypes
blanchet
parents: 38124
diff changeset
   606
        val axioms = built_in_axioms @ declarative_axioms
33192
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   607
        val highest_arity =
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   608
          fold Integer.max (map (fst o fst) (maps fst bounds)) 0
38126
8031d099379a added manual symmetry breaking for datatypes
blanchet
parents: 38124
diff changeset
   609
        val formula = fold_rev s_and axioms formula
34124
c4628a1dcf75 added support for binary nat/int representation to Nitpick
blanchet
parents: 34123
diff changeset
   610
        val _ = if bits = 0 then () else check_bits bits formula
41897
c24e7fd17464 perform no arity check in debug mode so that we get to see the Kodkod problem
blanchet
parents: 41888
diff changeset
   611
        val _ = if debug orelse formula = KK.False then ()
38182
747f8077b09a more helpful message
blanchet
parents: 38171
diff changeset
   612
                else check_arity "" univ_card highest_arity
33192
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   613
      in
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   614
        SOME ({comment = comment, settings = settings, univ_card = univ_card,
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   615
               tuple_assigns = [], bounds = bounds,
35280
54ab4921f826 fixed a few bugs in Nitpick and removed unreferenced variables
blanchet
parents: 35220
diff changeset
   616
               int_bounds = if bits = 0 then sequential_int_bounds univ_card
54ab4921f826 fixed a few bugs in Nitpick and removed unreferenced variables
blanchet
parents: 35220
diff changeset
   617
                            else pow_of_two_int_bounds bits main_j0,
33192
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   618
               expr_assigns = [], formula = formula},
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   619
              {free_names = free_names, sel_names = sel_names,
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   620
               nonsel_names = nonsel_names, rel_table = rel_table,
35386
45a4e19d3ebd more work on the new monotonicity stuff in Nitpick
blanchet
parents: 35385
diff changeset
   621
               unsound = unsound, scope = scope})
33192
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   622
      end
34124
c4628a1dcf75 added support for binary nat/int representation to Nitpick
blanchet
parents: 34123
diff changeset
   623
      handle TOO_LARGE (loc, msg) =>
34936
c4f04bee79f3 some work on Nitpick's support for quotient types;
blanchet
parents: 34935
diff changeset
   624
             if loc = "Nitpick_Kodkod.check_arity" andalso
c4f04bee79f3 some work on Nitpick's support for quotient types;
blanchet
parents: 34935
diff changeset
   625
                not (Typtab.is_empty ofs) then
35185
9b8f351cced6 added yet another hint to Nitpick's output, this time warning about problems for which nothing was effectively tested
blanchet
parents: 35183
diff changeset
   626
               problem_for_scope unsound
35190
ce653cc27a94 make sure that Nitpick uses binary notation consistently if "binary_ints" is enabled
blanchet
parents: 35185
diff changeset
   627
                   {hol_ctxt = hol_ctxt, binarize = binarize,
ce653cc27a94 make sure that Nitpick uses binary notation consistently if "binary_ints" is enabled
blanchet
parents: 35185
diff changeset
   628
                    card_assigns = card_assigns, bits = bits,
ce653cc27a94 make sure that Nitpick uses binary notation consistently if "binary_ints" is enabled
blanchet
parents: 35185
diff changeset
   629
                    bisim_depth = bisim_depth, datatypes = datatypes,
ce653cc27a94 make sure that Nitpick uses binary notation consistently if "binary_ints" is enabled
blanchet
parents: 35185
diff changeset
   630
                    ofs = Typtab.empty}
33192
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   631
             else if loc = "Nitpick.pick_them_nits_in_term.\
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   632
                           \problem_for_scope" then
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   633
               NONE
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   634
             else
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   635
               (Unsynchronized.change too_big_scopes (cons scope);
41992
0e4716fa330a reword Nitpick's wording concerning potential counterexamples
blanchet
parents: 41985
diff changeset
   636
                print_v (fn () =>
0e4716fa330a reword Nitpick's wording concerning potential counterexamples
blanchet
parents: 41985
diff changeset
   637
                    "Limit reached: " ^ msg ^ ". Skipping " ^
0e4716fa330a reword Nitpick's wording concerning potential counterexamples
blanchet
parents: 41985
diff changeset
   638
                    (if unsound then "potential component of " else "") ^
0e4716fa330a reword Nitpick's wording concerning potential counterexamples
blanchet
parents: 41985
diff changeset
   639
                    "scope.");
33192
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   640
                NONE)
35280
54ab4921f826 fixed a few bugs in Nitpick and removed unreferenced variables
blanchet
parents: 35220
diff changeset
   641
           | TOO_SMALL (_, msg) =>
41992
0e4716fa330a reword Nitpick's wording concerning potential counterexamples
blanchet
parents: 41985
diff changeset
   642
             (print_v (fn () =>
0e4716fa330a reword Nitpick's wording concerning potential counterexamples
blanchet
parents: 41985
diff changeset
   643
                  "Limit reached: " ^ msg ^ ". Skipping " ^
0e4716fa330a reword Nitpick's wording concerning potential counterexamples
blanchet
parents: 41985
diff changeset
   644
                  (if unsound then "potential component of " else "") ^
0e4716fa330a reword Nitpick's wording concerning potential counterexamples
blanchet
parents: 41985
diff changeset
   645
                  "scope.");
34124
c4628a1dcf75 added support for binary nat/int representation to Nitpick
blanchet
parents: 34123
diff changeset
   646
              NONE)
33192
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   647
34982
7b8c366e34a2 added support for nonstandard models to Nitpick (based on an idea by Koen Claessen) and did other fixes to Nitpick
blanchet
parents: 34938
diff changeset
   648
    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
   649
      (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
   650
      |> not standard ? prefix "nonstandard "
33192
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   651
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   652
    val scopes = Unsynchronized.ref []
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   653
    val generated_scopes = Unsynchronized.ref []
35185
9b8f351cced6 added yet another hint to Nitpick's output, this time warning about problems for which nothing was effectively tested
blanchet
parents: 35183
diff changeset
   654
    val generated_problems = Unsynchronized.ref ([] : rich_problem list)
33192
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   655
    val checked_problems = Unsynchronized.ref (SOME [])
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   656
    val met_potential = Unsynchronized.ref 0
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   657
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   658
    fun update_checked_problems problems =
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   659
      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
   660
                o nth problems)
35333
f61de25f71f9 distinguish between Kodkodi warnings and errors in Nitpick;
blanchet
parents: 35280
diff changeset
   661
    fun show_kodkod_warning "" = ()
47560
e30323bfc93c added SZS status wrappers in TPTP mode
blanchet
parents: 47559
diff changeset
   662
      | show_kodkod_warning s = print_nt (fn () => "Kodkod warning: " ^ s ^ ".")
33192
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   663
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   664
    fun print_and_check_model genuine bounds
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   665
            ({free_names, sel_names, nonsel_names, rel_table, scope, ...}
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   666
             : problem_extension) =
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   667
      let
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   668
        val (reconstructed_model, codatatypes_ok) =
41993
bd6296de1432 reintroduced "show_skolems" option -- useful when too many Skolems are displayed
blanchet
parents: 41992
diff changeset
   669
          reconstruct_hol_model
bd6296de1432 reintroduced "show_skolems" option -- useful when too many Skolems are displayed
blanchet
parents: 41992
diff changeset
   670
              {show_datatypes = show_datatypes, show_skolems = show_skolems,
bd6296de1432 reintroduced "show_skolems" option -- useful when too many Skolems are displayed
blanchet
parents: 41992
diff changeset
   671
               show_consts = show_consts}
38170
d74b66ec02ce handle free variables even more gracefully;
blanchet
parents: 38169
diff changeset
   672
              scope formats atomss real_frees pseudo_frees free_names sel_names
d74b66ec02ce handle free variables even more gracefully;
blanchet
parents: 38169
diff changeset
   673
              nonsel_names rel_table bounds
35671
ed2c3830d881 improved Nitpick's precision for "card" and "setsum" + fix incorrect outcome code w.r.t. "bisim_depth = -1"
blanchet
parents: 35665
diff changeset
   674
        val genuine_means_genuine =
ed2c3830d881 improved Nitpick's precision for "card" and "setsum" + fix incorrect outcome code w.r.t. "bisim_depth = -1"
blanchet
parents: 35665
diff changeset
   675
          got_all_user_axioms andalso none_true wfs andalso
41858
37ce158d6266 if "total_consts" is set, report cex's as quasi-genuine
blanchet
parents: 41856
diff changeset
   676
          sound_finitizes andalso total_consts <> SOME true andalso
37ce158d6266 if "total_consts" is set, report cex's as quasi-genuine
blanchet
parents: 41856
diff changeset
   677
          codatatypes_ok
47715
04400144c6fc handle TPTP definitions as definitions in Nitpick rather than as axioms
blanchet
parents: 47670
diff changeset
   678
        fun assms_prop () =
04400144c6fc handle TPTP definitions as definitions in Nitpick rather than as axioms
blanchet
parents: 47670
diff changeset
   679
          Logic.mk_conjunction_list (neg_t :: def_assm_ts @ nondef_assm_ts)
33192
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   680
      in
47560
e30323bfc93c added SZS status wrappers in TPTP mode
blanchet
parents: 47559
diff changeset
   681
        (print_t (fn () =>
e30323bfc93c added SZS status wrappers in TPTP mode
blanchet
parents: 47559
diff changeset
   682
             "% SZS status " ^
e30323bfc93c added SZS status wrappers in TPTP mode
blanchet
parents: 47559
diff changeset
   683
             (if genuine then
e30323bfc93c added SZS status wrappers in TPTP mode
blanchet
parents: 47559
diff changeset
   684
                if falsify then "CounterSatisfiable" else "Satisfiable"
e30323bfc93c added SZS status wrappers in TPTP mode
blanchet
parents: 47559
diff changeset
   685
              else
e30323bfc93c added SZS status wrappers in TPTP mode
blanchet
parents: 47559
diff changeset
   686
                "Unknown") ^ "\n" ^
47562
a72239723ae8 tuned SZS status output
blanchet
parents: 47560
diff changeset
   687
             "% SZS output start FiniteModel");
47560
e30323bfc93c added SZS status wrappers in TPTP mode
blanchet
parents: 47559
diff changeset
   688
         pprint_a (Pretty.chunks
35671
ed2c3830d881 improved Nitpick's precision for "card" and "setsum" + fix incorrect outcome code w.r.t. "bisim_depth = -1"
blanchet
parents: 35665
diff changeset
   689
             [Pretty.blk (0,
43022
7d3ce43d9464 handle non-auto try case gracefully in Nitpick
blanchet
parents: 43020
diff changeset
   690
                  (pstrs ((if mode = Auto_Try then "Auto " else "") ^
7d3ce43d9464 handle non-auto try case gracefully in Nitpick
blanchet
parents: 43020
diff changeset
   691
                          "Nitpick found a" ^
41992
0e4716fa330a reword Nitpick's wording concerning potential counterexamples
blanchet
parents: 41985
diff changeset
   692
                          (if not genuine then " potentially spurious "
35671
ed2c3830d881 improved Nitpick's precision for "card" and "setsum" + fix incorrect outcome code w.r.t. "bisim_depth = -1"
blanchet
parents: 35665
diff changeset
   693
                           else if genuine_means_genuine then " "
ed2c3830d881 improved Nitpick's precision for "card" and "setsum" + fix incorrect outcome code w.r.t. "bisim_depth = -1"
blanchet
parents: 35665
diff changeset
   694
                           else " quasi genuine ") ^ das_wort_model) @
ed2c3830d881 improved Nitpick's precision for "card" and "setsum" + fix incorrect outcome code w.r.t. "bisim_depth = -1"
blanchet
parents: 35665
diff changeset
   695
                   (case pretties_for_scope scope verbose of
ed2c3830d881 improved Nitpick's precision for "card" and "setsum" + fix incorrect outcome code w.r.t. "bisim_depth = -1"
blanchet
parents: 35665
diff changeset
   696
                      [] => []
ed2c3830d881 improved Nitpick's precision for "card" and "setsum" + fix incorrect outcome code w.r.t. "bisim_depth = -1"
blanchet
parents: 35665
diff changeset
   697
                    | pretties => pstrs " for " @ pretties) @
ed2c3830d881 improved Nitpick's precision for "card" and "setsum" + fix incorrect outcome code w.r.t. "bisim_depth = -1"
blanchet
parents: 35665
diff changeset
   698
                   [Pretty.str ":\n"])),
ed2c3830d881 improved Nitpick's precision for "card" and "setsum" + fix incorrect outcome code w.r.t. "bisim_depth = -1"
blanchet
parents: 35665
diff changeset
   699
              Pretty.indent indent_size reconstructed_model]);
47564
8074b18d8d76 more standard SZS output
blanchet
parents: 47562
diff changeset
   700
         print_t (K "% SZS output end FiniteModel");
35671
ed2c3830d881 improved Nitpick's precision for "card" and "setsum" + fix incorrect outcome code w.r.t. "bisim_depth = -1"
blanchet
parents: 35665
diff changeset
   701
         if genuine then
ed2c3830d881 improved Nitpick's precision for "card" and "setsum" + fix incorrect outcome code w.r.t. "bisim_depth = -1"
blanchet
parents: 35665
diff changeset
   702
           (if check_genuine andalso standard then
ed2c3830d881 improved Nitpick's precision for "card" and "setsum" + fix incorrect outcome code w.r.t. "bisim_depth = -1"
blanchet
parents: 35665
diff changeset
   703
              case prove_hol_model scope tac_timeout free_names sel_names
38169
b51784515471 optimize local "def"s by treating them as definitions
blanchet
parents: 38126
diff changeset
   704
                                   rel_table bounds (assms_prop ()) of
35671
ed2c3830d881 improved Nitpick's precision for "card" and "setsum" + fix incorrect outcome code w.r.t. "bisim_depth = -1"
blanchet
parents: 35665
diff changeset
   705
                SOME true =>
ed2c3830d881 improved Nitpick's precision for "card" and "setsum" + fix incorrect outcome code w.r.t. "bisim_depth = -1"
blanchet
parents: 35665
diff changeset
   706
                print ("Confirmation by \"auto\": The above " ^
ed2c3830d881 improved Nitpick's precision for "card" and "setsum" + fix incorrect outcome code w.r.t. "bisim_depth = -1"
blanchet
parents: 35665
diff changeset
   707
                       das_wort_model ^ " is really genuine.")
33192
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   708
              | 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
   709
                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
   710
                  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
   711
                         \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
   712
                         \happen.\nPlease send a bug report to blanchet\
33192
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   713
                         \te@in.tum.de.")
35671
ed2c3830d881 improved Nitpick's precision for "card" and "setsum" + fix incorrect outcome code w.r.t. "bisim_depth = -1"
blanchet
parents: 35665
diff changeset
   714
                 else
ed2c3830d881 improved Nitpick's precision for "card" and "setsum" + fix incorrect outcome code w.r.t. "bisim_depth = -1"
blanchet
parents: 35665
diff changeset
   715
                   print ("Refutation by \"auto\": The above " ^
ed2c3830d881 improved Nitpick's precision for "card" and "setsum" + fix incorrect outcome code w.r.t. "bisim_depth = -1"
blanchet
parents: 35665
diff changeset
   716
                          das_wort_model ^ " is spurious.")
ed2c3830d881 improved Nitpick's precision for "card" and "setsum" + fix incorrect outcome code w.r.t. "bisim_depth = -1"
blanchet
parents: 35665
diff changeset
   717
               | NONE => print "No confirmation by \"auto\"."
ed2c3830d881 improved Nitpick's precision for "card" and "setsum" + fix incorrect outcome code w.r.t. "bisim_depth = -1"
blanchet
parents: 35665
diff changeset
   718
            else
ed2c3830d881 improved Nitpick's precision for "card" and "setsum" + fix incorrect outcome code w.r.t. "bisim_depth = -1"
blanchet
parents: 35665
diff changeset
   719
              ();
ed2c3830d881 improved Nitpick's precision for "card" and "setsum" + fix incorrect outcome code w.r.t. "bisim_depth = -1"
blanchet
parents: 35665
diff changeset
   720
            if not standard andalso likely_in_struct_induct_step then
ed2c3830d881 improved Nitpick's precision for "card" and "setsum" + fix incorrect outcome code w.r.t. "bisim_depth = -1"
blanchet
parents: 35665
diff changeset
   721
              print "The existence of a nonstandard model suggests that the \
36126
00d550b6cfd4 cosmetics
blanchet
parents: 35968
diff changeset
   722
                    \induction hypothesis is not general enough or may even be \
00d550b6cfd4 cosmetics
blanchet
parents: 35968
diff changeset
   723
                    \wrong. See the Nitpick manual's \"Inductive Properties\" \
00d550b6cfd4 cosmetics
blanchet
parents: 35968
diff changeset
   724
                    \section for details (\"isabelle doc nitpick\")."
35671
ed2c3830d881 improved Nitpick's precision for "card" and "setsum" + fix incorrect outcome code w.r.t. "bisim_depth = -1"
blanchet
parents: 35665
diff changeset
   725
            else
ed2c3830d881 improved Nitpick's precision for "card" and "setsum" + fix incorrect outcome code w.r.t. "bisim_depth = -1"
blanchet
parents: 35665
diff changeset
   726
              ();
41048
d5ebe94248ad added a hint when the user obviously just forgot a colon after the lemma's name
blanchet
parents: 41007
diff changeset
   727
            if has_lonely_bool_var orig_t then
d5ebe94248ad added a hint when the user obviously just forgot a colon after the lemma's name
blanchet
parents: 41007
diff changeset
   728
              print "Hint: Maybe you forgot a colon after the lemma's name?"
d5ebe94248ad added a hint when the user obviously just forgot a colon after the lemma's name
blanchet
parents: 41007
diff changeset
   729
            else if has_syntactic_sorts orig_t then
35671
ed2c3830d881 improved Nitpick's precision for "card" and "setsum" + fix incorrect outcome code w.r.t. "bisim_depth = -1"
blanchet
parents: 35665
diff changeset
   730
              print "Hint: Maybe you forgot a type constraint?"
ed2c3830d881 improved Nitpick's precision for "card" and "setsum" + fix incorrect outcome code w.r.t. "bisim_depth = -1"
blanchet
parents: 35665
diff changeset
   731
            else
ed2c3830d881 improved Nitpick's precision for "card" and "setsum" + fix incorrect outcome code w.r.t. "bisim_depth = -1"
blanchet
parents: 35665
diff changeset
   732
              ();
ed2c3830d881 improved Nitpick's precision for "card" and "setsum" + fix incorrect outcome code w.r.t. "bisim_depth = -1"
blanchet
parents: 35665
diff changeset
   733
            if not genuine_means_genuine then
ed2c3830d881 improved Nitpick's precision for "card" and "setsum" + fix incorrect outcome code w.r.t. "bisim_depth = -1"
blanchet
parents: 35665
diff changeset
   734
              if no_poly_user_axioms then
ed2c3830d881 improved Nitpick's precision for "card" and "setsum" + fix incorrect outcome code w.r.t. "bisim_depth = -1"
blanchet
parents: 35665
diff changeset
   735
                let
ed2c3830d881 improved Nitpick's precision for "card" and "setsum" + fix incorrect outcome code w.r.t. "bisim_depth = -1"
blanchet
parents: 35665
diff changeset
   736
                  val options =
ed2c3830d881 improved Nitpick's precision for "card" and "setsum" + fix incorrect outcome code w.r.t. "bisim_depth = -1"
blanchet
parents: 35665
diff changeset
   737
                    [] |> not got_all_mono_user_axioms
ed2c3830d881 improved Nitpick's precision for "card" and "setsum" + fix incorrect outcome code w.r.t. "bisim_depth = -1"
blanchet
parents: 35665
diff changeset
   738
                          ? cons ("user_axioms", "\"true\"")
ed2c3830d881 improved Nitpick's precision for "card" and "setsum" + fix incorrect outcome code w.r.t. "bisim_depth = -1"
blanchet
parents: 35665
diff changeset
   739
                       |> not (none_true wfs)
ed2c3830d881 improved Nitpick's precision for "card" and "setsum" + fix incorrect outcome code w.r.t. "bisim_depth = -1"
blanchet
parents: 35665
diff changeset
   740
                          ? cons ("wf", "\"smart\" or \"false\"")
ed2c3830d881 improved Nitpick's precision for "card" and "setsum" + fix incorrect outcome code w.r.t. "bisim_depth = -1"
blanchet
parents: 35665
diff changeset
   741
                       |> not sound_finitizes
ed2c3830d881 improved Nitpick's precision for "card" and "setsum" + fix incorrect outcome code w.r.t. "bisim_depth = -1"
blanchet
parents: 35665
diff changeset
   742
                          ? cons ("finitize", "\"smart\" or \"false\"")
41858
37ce158d6266 if "total_consts" is set, report cex's as quasi-genuine
blanchet
parents: 41856
diff changeset
   743
                       |> total_consts = SOME true
37ce158d6266 if "total_consts" is set, report cex's as quasi-genuine
blanchet
parents: 41856
diff changeset
   744
                          ? cons ("total_consts", "\"smart\" or \"false\"")
35671
ed2c3830d881 improved Nitpick's precision for "card" and "setsum" + fix incorrect outcome code w.r.t. "bisim_depth = -1"
blanchet
parents: 35665
diff changeset
   745
                       |> not codatatypes_ok
ed2c3830d881 improved Nitpick's precision for "card" and "setsum" + fix incorrect outcome code w.r.t. "bisim_depth = -1"
blanchet
parents: 35665
diff changeset
   746
                          ? cons ("bisim_depth", "a nonnegative value")
ed2c3830d881 improved Nitpick's precision for "card" and "setsum" + fix incorrect outcome code w.r.t. "bisim_depth = -1"
blanchet
parents: 35665
diff changeset
   747
                  val ss =
ed2c3830d881 improved Nitpick's precision for "card" and "setsum" + fix incorrect outcome code w.r.t. "bisim_depth = -1"
blanchet
parents: 35665
diff changeset
   748
                    map (fn (name, value) => quote name ^ " set to " ^ value)
ed2c3830d881 improved Nitpick's precision for "card" and "setsum" + fix incorrect outcome code w.r.t. "bisim_depth = -1"
blanchet
parents: 35665
diff changeset
   749
                        options
ed2c3830d881 improved Nitpick's precision for "card" and "setsum" + fix incorrect outcome code w.r.t. "bisim_depth = -1"
blanchet
parents: 35665
diff changeset
   750
                in
ed2c3830d881 improved Nitpick's precision for "card" and "setsum" + fix incorrect outcome code w.r.t. "bisim_depth = -1"
blanchet
parents: 35665
diff changeset
   751
                  print ("Try again with " ^
41872
10fd9e5d58ba added missing spaces in output
blanchet
parents: 41871
diff changeset
   752
                         space_implode " " (serial_commas "and" ss) ^
35671
ed2c3830d881 improved Nitpick's precision for "card" and "setsum" + fix incorrect outcome code w.r.t. "bisim_depth = -1"
blanchet
parents: 35665
diff changeset
   753
                         " to confirm that the " ^ das_wort_model ^
ed2c3830d881 improved Nitpick's precision for "card" and "setsum" + fix incorrect outcome code w.r.t. "bisim_depth = -1"
blanchet
parents: 35665
diff changeset
   754
                         " is genuine.")
ed2c3830d881 improved Nitpick's precision for "card" and "setsum" + fix incorrect outcome code w.r.t. "bisim_depth = -1"
blanchet
parents: 35665
diff changeset
   755
                end
ed2c3830d881 improved Nitpick's precision for "card" and "setsum" + fix incorrect outcome code w.r.t. "bisim_depth = -1"
blanchet
parents: 35665
diff changeset
   756
              else
ed2c3830d881 improved Nitpick's precision for "card" and "setsum" + fix incorrect outcome code w.r.t. "bisim_depth = -1"
blanchet
parents: 35665
diff changeset
   757
                print ("Nitpick is unable to guarantee the authenticity of \
ed2c3830d881 improved Nitpick's precision for "card" and "setsum" + fix incorrect outcome code w.r.t. "bisim_depth = -1"
blanchet
parents: 35665
diff changeset
   758
                       \the " ^ das_wort_model ^ " in the presence of \
ed2c3830d881 improved Nitpick's precision for "card" and "setsum" + fix incorrect outcome code w.r.t. "bisim_depth = -1"
blanchet
parents: 35665
diff changeset
   759
                       \polymorphic axioms.")
ed2c3830d881 improved Nitpick's precision for "card" and "setsum" + fix incorrect outcome code w.r.t. "bisim_depth = -1"
blanchet
parents: 35665
diff changeset
   760
            else
ed2c3830d881 improved Nitpick's precision for "card" and "setsum" + fix incorrect outcome code w.r.t. "bisim_depth = -1"
blanchet
parents: 35665
diff changeset
   761
              ();
ed2c3830d881 improved Nitpick's precision for "card" and "setsum" + fix incorrect outcome code w.r.t. "bisim_depth = -1"
blanchet
parents: 35665
diff changeset
   762
            NONE)
ed2c3830d881 improved Nitpick's precision for "card" and "setsum" + fix incorrect outcome code w.r.t. "bisim_depth = -1"
blanchet
parents: 35665
diff changeset
   763
         else
ed2c3830d881 improved Nitpick's precision for "card" and "setsum" + fix incorrect outcome code w.r.t. "bisim_depth = -1"
blanchet
parents: 35665
diff changeset
   764
           if not genuine then
ed2c3830d881 improved Nitpick's precision for "card" and "setsum" + fix incorrect outcome code w.r.t. "bisim_depth = -1"
blanchet
parents: 35665
diff changeset
   765
             (Unsynchronized.inc met_potential;
ed2c3830d881 improved Nitpick's precision for "card" and "setsum" + fix incorrect outcome code w.r.t. "bisim_depth = -1"
blanchet
parents: 35665
diff changeset
   766
              if check_potential then
ed2c3830d881 improved Nitpick's precision for "card" and "setsum" + fix incorrect outcome code w.r.t. "bisim_depth = -1"
blanchet
parents: 35665
diff changeset
   767
                let
ed2c3830d881 improved Nitpick's precision for "card" and "setsum" + fix incorrect outcome code w.r.t. "bisim_depth = -1"
blanchet
parents: 35665
diff changeset
   768
                  val status = prove_hol_model scope tac_timeout free_names
38169
b51784515471 optimize local "def"s by treating them as definitions
blanchet
parents: 38126
diff changeset
   769
                                               sel_names rel_table bounds
b51784515471 optimize local "def"s by treating them as definitions
blanchet
parents: 38126
diff changeset
   770
                                               (assms_prop ())
35671
ed2c3830d881 improved Nitpick's precision for "card" and "setsum" + fix incorrect outcome code w.r.t. "bisim_depth = -1"
blanchet
parents: 35665
diff changeset
   771
                in
ed2c3830d881 improved Nitpick's precision for "card" and "setsum" + fix incorrect outcome code w.r.t. "bisim_depth = -1"
blanchet
parents: 35665
diff changeset
   772
                  (case status of
ed2c3830d881 improved Nitpick's precision for "card" and "setsum" + fix incorrect outcome code w.r.t. "bisim_depth = -1"
blanchet
parents: 35665
diff changeset
   773
                     SOME true => print ("Confirmation by \"auto\": The \
ed2c3830d881 improved Nitpick's precision for "card" and "setsum" + fix incorrect outcome code w.r.t. "bisim_depth = -1"
blanchet
parents: 35665
diff changeset
   774
                                         \above " ^ das_wort_model ^
ed2c3830d881 improved Nitpick's precision for "card" and "setsum" + fix incorrect outcome code w.r.t. "bisim_depth = -1"
blanchet
parents: 35665
diff changeset
   775
                                         " is genuine.")
ed2c3830d881 improved Nitpick's precision for "card" and "setsum" + fix incorrect outcome code w.r.t. "bisim_depth = -1"
blanchet
parents: 35665
diff changeset
   776
                   | SOME false => print ("Refutation by \"auto\": The above " ^
ed2c3830d881 improved Nitpick's precision for "card" and "setsum" + fix incorrect outcome code w.r.t. "bisim_depth = -1"
blanchet
parents: 35665
diff changeset
   777
                                          das_wort_model ^ " is spurious.")
ed2c3830d881 improved Nitpick's precision for "card" and "setsum" + fix incorrect outcome code w.r.t. "bisim_depth = -1"
blanchet
parents: 35665
diff changeset
   778
                   | NONE => print "No confirmation by \"auto\".");
ed2c3830d881 improved Nitpick's precision for "card" and "setsum" + fix incorrect outcome code w.r.t. "bisim_depth = -1"
blanchet
parents: 35665
diff changeset
   779
                  status
ed2c3830d881 improved Nitpick's precision for "card" and "setsum" + fix incorrect outcome code w.r.t. "bisim_depth = -1"
blanchet
parents: 35665
diff changeset
   780
                end
ed2c3830d881 improved Nitpick's precision for "card" and "setsum" + fix incorrect outcome code w.r.t. "bisim_depth = -1"
blanchet
parents: 35665
diff changeset
   781
              else
ed2c3830d881 improved Nitpick's precision for "card" and "setsum" + fix incorrect outcome code w.r.t. "bisim_depth = -1"
blanchet
parents: 35665
diff changeset
   782
                NONE)
33192
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   783
           else
35671
ed2c3830d881 improved Nitpick's precision for "card" and "setsum" + fix incorrect outcome code w.r.t. "bisim_depth = -1"
blanchet
parents: 35665
diff changeset
   784
             NONE)
ed2c3830d881 improved Nitpick's precision for "card" and "setsum" + fix incorrect outcome code w.r.t. "bisim_depth = -1"
blanchet
parents: 35665
diff changeset
   785
        |> pair genuine_means_genuine
33192
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   786
      end
35671
ed2c3830d881 improved Nitpick's precision for "card" and "setsum" + fix incorrect outcome code w.r.t. "bisim_depth = -1"
blanchet
parents: 35665
diff changeset
   787
    fun solve_any_problem (found_really_genuine, max_potential, max_genuine,
ed2c3830d881 improved Nitpick's precision for "card" and "setsum" + fix incorrect outcome code w.r.t. "bisim_depth = -1"
blanchet
parents: 35665
diff changeset
   788
                           donno) first_time problems =
33192
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   789
      let
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   790
        val max_potential = Int.max (0, max_potential)
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   791
        val max_genuine = Int.max (0, max_genuine)
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   792
        fun print_and_check genuine (j, bounds) =
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   793
          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
   794
        val max_solutions = max_potential + max_genuine
36384
76d5fd5a45fb cosmetics
blanchet
parents: 36380
diff changeset
   795
                            |> not incremental ? Integer.min 1
33192
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   796
      in
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   797
        if max_solutions <= 0 then
35671
ed2c3830d881 improved Nitpick's precision for "card" and "setsum" + fix incorrect outcome code w.r.t. "bisim_depth = -1"
blanchet
parents: 35665
diff changeset
   798
          (found_really_genuine, 0, 0, donno)
33192
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   799
        else
41793
c7a2669ae75d tweaked Nitpick based on C++ memory model example
blanchet
parents: 41791
diff changeset
   800
          case KK.solve_any_problem debug overlord deadline max_threads
c7a2669ae75d tweaked Nitpick based on C++ memory model example
blanchet
parents: 41791
diff changeset
   801
                                    max_solutions (map fst problems) of
35696
17ae461d6133 show nice error message in Nitpick when "java" is not available
blanchet
parents: 35671
diff changeset
   802
            KK.JavaNotInstalled =>
47560
e30323bfc93c added SZS status wrappers in TPTP mode
blanchet
parents: 47559
diff changeset
   803
            (print_nt install_java_message;
35696
17ae461d6133 show nice error message in Nitpick when "java" is not available
blanchet
parents: 35671
diff changeset
   804
             (found_really_genuine, max_potential, max_genuine, donno + 1))
38516
307669429dc1 gracefully handle the case where the JVM is too old in Nitpick
blanchet
parents: 38240
diff changeset
   805
          | KK.JavaTooOld =>
47560
e30323bfc93c added SZS status wrappers in TPTP mode
blanchet
parents: 47559
diff changeset
   806
            (print_nt install_java_message;
38516
307669429dc1 gracefully handle the case where the JVM is too old in Nitpick
blanchet
parents: 38240
diff changeset
   807
             (found_really_genuine, max_potential, max_genuine, donno + 1))
35696
17ae461d6133 show nice error message in Nitpick when "java" is not available
blanchet
parents: 35671
diff changeset
   808
          | KK.KodkodiNotInstalled =>
47560
e30323bfc93c added SZS status wrappers in TPTP mode
blanchet
parents: 47559
diff changeset
   809
            (print_nt install_kodkodi_message;
35671
ed2c3830d881 improved Nitpick's precision for "card" and "setsum" + fix incorrect outcome code w.r.t. "bisim_depth = -1"
blanchet
parents: 35665
diff changeset
   810
             (found_really_genuine, max_potential, max_genuine, donno + 1))
35333
f61de25f71f9 distinguish between Kodkodi warnings and errors in Nitpick;
blanchet
parents: 35280
diff changeset
   811
          | KK.Normal ([], unsat_js, s) =>
f61de25f71f9 distinguish between Kodkodi warnings and errors in Nitpick;
blanchet
parents: 35280
diff changeset
   812
            (update_checked_problems problems unsat_js; show_kodkod_warning s;
35671
ed2c3830d881 improved Nitpick's precision for "card" and "setsum" + fix incorrect outcome code w.r.t. "bisim_depth = -1"
blanchet
parents: 35665
diff changeset
   813
             (found_really_genuine, max_potential, max_genuine, donno))
35333
f61de25f71f9 distinguish between Kodkodi warnings and errors in Nitpick;
blanchet
parents: 35280
diff changeset
   814
          | KK.Normal (sat_ps, unsat_js, s) =>
33192
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   815
            let
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   816
              val (lib_ps, con_ps) =
35185
9b8f351cced6 added yet another hint to Nitpick's output, this time warning about problems for which nothing was effectively tested
blanchet
parents: 35183
diff changeset
   817
                List.partition (#unsound o snd o nth problems o fst) sat_ps
33192
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   818
            in
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   819
              update_checked_problems problems (unsat_js @ map fst lib_ps);
35333
f61de25f71f9 distinguish between Kodkodi warnings and errors in Nitpick;
blanchet
parents: 35280
diff changeset
   820
              show_kodkod_warning s;
33192
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   821
              if null con_ps then
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   822
                let
35671
ed2c3830d881 improved Nitpick's precision for "card" and "setsum" + fix incorrect outcome code w.r.t. "bisim_depth = -1"
blanchet
parents: 35665
diff changeset
   823
                  val genuine_codes =
ed2c3830d881 improved Nitpick's precision for "card" and "setsum" + fix incorrect outcome code w.r.t. "bisim_depth = -1"
blanchet
parents: 35665
diff changeset
   824
                    lib_ps |> take max_potential
ed2c3830d881 improved Nitpick's precision for "card" and "setsum" + fix incorrect outcome code w.r.t. "bisim_depth = -1"
blanchet
parents: 35665
diff changeset
   825
                           |> map (print_and_check false)
ed2c3830d881 improved Nitpick's precision for "card" and "setsum" + fix incorrect outcome code w.r.t. "bisim_depth = -1"
blanchet
parents: 35665
diff changeset
   826
                           |> filter (curry (op =) (SOME true) o snd)
ed2c3830d881 improved Nitpick's precision for "card" and "setsum" + fix incorrect outcome code w.r.t. "bisim_depth = -1"
blanchet
parents: 35665
diff changeset
   827
                  val found_really_genuine =
ed2c3830d881 improved Nitpick's precision for "card" and "setsum" + fix incorrect outcome code w.r.t. "bisim_depth = -1"
blanchet
parents: 35665
diff changeset
   828
                    found_really_genuine orelse exists fst genuine_codes
ed2c3830d881 improved Nitpick's precision for "card" and "setsum" + fix incorrect outcome code w.r.t. "bisim_depth = -1"
blanchet
parents: 35665
diff changeset
   829
                  val num_genuine = length genuine_codes
33192
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   830
                  val max_genuine = max_genuine - num_genuine
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   831
                  val max_potential = max_potential
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   832
                                      - (length lib_ps - num_genuine)
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   833
                in
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   834
                  if max_genuine <= 0 then
35671
ed2c3830d881 improved Nitpick's precision for "card" and "setsum" + fix incorrect outcome code w.r.t. "bisim_depth = -1"
blanchet
parents: 35665
diff changeset
   835
                    (found_really_genuine, 0, 0, donno)
33192
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   836
                  else
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   837
                    let
35185
9b8f351cced6 added yet another hint to Nitpick's output, this time warning about problems for which nothing was effectively tested
blanchet
parents: 35183
diff changeset
   838
                      (* "co_js" is the list of sound problems whose unsound
9b8f351cced6 added yet another hint to Nitpick's output, this time warning about problems for which nothing was effectively tested
blanchet
parents: 35183
diff changeset
   839
                         pendants couldn't be satisfied and hence that most
9b8f351cced6 added yet another hint to Nitpick's output, this time warning about problems for which nothing was effectively tested
blanchet
parents: 35183
diff changeset
   840
                         probably can't be satisfied themselves. *)
33192
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   841
                      val co_js =
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   842
                        map (fn j => j - 1) unsat_js
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   843
                        |> filter (fn j =>
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   844
                                      j >= 0 andalso
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   845
                                      scopes_equivalent
35814
234eaa508359 added one-entry cache around Kodkod invocation
blanchet
parents: 35807
diff changeset
   846
                                          (#scope (snd (nth problems j)),
234eaa508359 added one-entry cache around Kodkod invocation
blanchet
parents: 35807
diff changeset
   847
                                           #scope (snd (nth problems (j + 1)))))
33192
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   848
                      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
   849
                                                          unsat_js @ co_js)
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   850
                      val problems =
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   851
                        problems |> filter_out_indices bye_js
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   852
                                 |> max_potential <= 0
35185
9b8f351cced6 added yet another hint to Nitpick's output, this time warning about problems for which nothing was effectively tested
blanchet
parents: 35183
diff changeset
   853
                                    ? filter_out (#unsound o snd)
33192
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   854
                    in
35671
ed2c3830d881 improved Nitpick's precision for "card" and "setsum" + fix incorrect outcome code w.r.t. "bisim_depth = -1"
blanchet
parents: 35665
diff changeset
   855
                      solve_any_problem (found_really_genuine, max_potential,
ed2c3830d881 improved Nitpick's precision for "card" and "setsum" + fix incorrect outcome code w.r.t. "bisim_depth = -1"
blanchet
parents: 35665
diff changeset
   856
                                         max_genuine, donno) false problems
33192
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   857
                    end
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   858
                end
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   859
              else
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   860
                let
35671
ed2c3830d881 improved Nitpick's precision for "card" and "setsum" + fix incorrect outcome code w.r.t. "bisim_depth = -1"
blanchet
parents: 35665
diff changeset
   861
                  val genuine_codes =
ed2c3830d881 improved Nitpick's precision for "card" and "setsum" + fix incorrect outcome code w.r.t. "bisim_depth = -1"
blanchet
parents: 35665
diff changeset
   862
                    con_ps |> take max_genuine
ed2c3830d881 improved Nitpick's precision for "card" and "setsum" + fix incorrect outcome code w.r.t. "bisim_depth = -1"
blanchet
parents: 35665
diff changeset
   863
                           |> map (print_and_check true)
ed2c3830d881 improved Nitpick's precision for "card" and "setsum" + fix incorrect outcome code w.r.t. "bisim_depth = -1"
blanchet
parents: 35665
diff changeset
   864
                  val max_genuine = max_genuine - length genuine_codes
ed2c3830d881 improved Nitpick's precision for "card" and "setsum" + fix incorrect outcome code w.r.t. "bisim_depth = -1"
blanchet
parents: 35665
diff changeset
   865
                  val found_really_genuine =
ed2c3830d881 improved Nitpick's precision for "card" and "setsum" + fix incorrect outcome code w.r.t. "bisim_depth = -1"
blanchet
parents: 35665
diff changeset
   866
                    found_really_genuine orelse exists fst genuine_codes
33192
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   867
                in
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   868
                  if max_genuine <= 0 orelse not first_time then
35671
ed2c3830d881 improved Nitpick's precision for "card" and "setsum" + fix incorrect outcome code w.r.t. "bisim_depth = -1"
blanchet
parents: 35665
diff changeset
   869
                    (found_really_genuine, 0, max_genuine, donno)
33192
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   870
                  else
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   871
                    let
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   872
                      val bye_js = sort_distinct int_ord
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   873
                                                 (map fst sat_ps @ unsat_js)
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   874
                      val problems =
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   875
                        problems |> filter_out_indices bye_js
35185
9b8f351cced6 added yet another hint to Nitpick's output, this time warning about problems for which nothing was effectively tested
blanchet
parents: 35183
diff changeset
   876
                                 |> filter_out (#unsound o snd)
35671
ed2c3830d881 improved Nitpick's precision for "card" and "setsum" + fix incorrect outcome code w.r.t. "bisim_depth = -1"
blanchet
parents: 35665
diff changeset
   877
                    in
ed2c3830d881 improved Nitpick's precision for "card" and "setsum" + fix incorrect outcome code w.r.t. "bisim_depth = -1"
blanchet
parents: 35665
diff changeset
   878
                      solve_any_problem (found_really_genuine, 0, max_genuine,
ed2c3830d881 improved Nitpick's precision for "card" and "setsum" + fix incorrect outcome code w.r.t. "bisim_depth = -1"
blanchet
parents: 35665
diff changeset
   879
                                         donno) false problems
ed2c3830d881 improved Nitpick's precision for "card" and "setsum" + fix incorrect outcome code w.r.t. "bisim_depth = -1"
blanchet
parents: 35665
diff changeset
   880
                    end
33192
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   881
                end
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   882
            end
34126
8a2c5d7aff51 polished Nitpick's binary integer support etc.;
blanchet
parents: 34124
diff changeset
   883
          | KK.TimedOut unsat_js =>
33192
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   884
            (update_checked_problems problems unsat_js; raise TimeLimit.TimeOut)
34126
8a2c5d7aff51 polished Nitpick's binary integer support etc.;
blanchet
parents: 34124
diff changeset
   885
          | KK.Error (s, unsat_js) =>
33192
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   886
            (update_checked_problems problems unsat_js;
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   887
             print_v (K ("Kodkod error: " ^ s ^ "."));
35671
ed2c3830d881 improved Nitpick's precision for "card" and "setsum" + fix incorrect outcome code w.r.t. "bisim_depth = -1"
blanchet
parents: 35665
diff changeset
   888
             (found_really_genuine, max_potential, max_genuine, donno + 1))
33192
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   889
      end
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   890
35671
ed2c3830d881 improved Nitpick's precision for "card" and "setsum" + fix incorrect outcome code w.r.t. "bisim_depth = -1"
blanchet
parents: 35665
diff changeset
   891
    fun run_batch j n scopes (found_really_genuine, max_potential, max_genuine,
ed2c3830d881 improved Nitpick's precision for "card" and "setsum" + fix incorrect outcome code w.r.t. "bisim_depth = -1"
blanchet
parents: 35665
diff changeset
   892
                              donno) =
33192
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   893
      let
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   894
        val _ =
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   895
          if null scopes then
47560
e30323bfc93c added SZS status wrappers in TPTP mode
blanchet
parents: 47559
diff changeset
   896
            print_nt (K "The scope specification is inconsistent.")
33192
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   897
          else if verbose then
47560
e30323bfc93c added SZS status wrappers in TPTP mode
blanchet
parents: 47559
diff changeset
   898
            pprint_nt (fn () => Pretty.chunks
33192
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   899
                [Pretty.blk (0,
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   900
                     pstrs ((if n > 1 then
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   901
                               "Batch " ^ string_of_int (j + 1) ^ " of " ^
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   902
                               signed_string_of_int n ^ ": "
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   903
                             else
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   904
                               "") ^
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   905
                            "Trying " ^ string_of_int (length scopes) ^
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   906
                            " scope" ^ plural_s_for_list scopes ^ ":")),
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   907
                 Pretty.indent indent_size
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   908
                     (Pretty.chunks (map2
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   909
                          (fn j => fn scope =>
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   910
                              Pretty.block (
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   911
                                  (case pretties_for_scope scope true of
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   912
                                     [] => [Pretty.str "Empty"]
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   913
                                   | pretties => pretties) @
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   914
                                  [Pretty.str (if j = 1 then "." else ";")]))
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   915
                          (length scopes downto 1) scopes))])
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   916
          else
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   917
            ()
35280
54ab4921f826 fixed a few bugs in Nitpick and removed unreferenced variables
blanchet
parents: 35220
diff changeset
   918
        fun add_problem_for_scope (scope, unsound) (problems, donno) =
33192
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   919
          (check_deadline ();
35185
9b8f351cced6 added yet another hint to Nitpick's output, this time warning about problems for which nothing was effectively tested
blanchet
parents: 35183
diff changeset
   920
           case problem_for_scope unsound scope of
33192
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   921
             SOME problem =>
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   922
             (problems
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   923
              |> (null problems orelse
35814
234eaa508359 added one-entry cache around Kodkod invocation
blanchet
parents: 35807
diff changeset
   924
                  not (KK.problems_equivalent (fst problem, fst (hd problems))))
33192
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   925
                  ? cons problem, donno)
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   926
           | NONE => (problems, donno + 1))
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   927
        val (problems, donno) =
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   928
          fold add_problem_for_scope
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   929
               (map_product pair scopes
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   930
                    ((if max_genuine > 0 then [false] else []) @
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   931
                     (if max_potential > 0 then [true] else [])))
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   932
               ([], donno)
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   933
        val _ = Unsynchronized.change generated_problems (append problems)
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   934
        val _ = Unsynchronized.change generated_scopes (append scopes)
35185
9b8f351cced6 added yet another hint to Nitpick's output, this time warning about problems for which nothing was effectively tested
blanchet
parents: 35183
diff changeset
   935
        val _ =
9b8f351cced6 added yet another hint to Nitpick's output, this time warning about problems for which nothing was effectively tested
blanchet
parents: 35183
diff changeset
   936
          if j + 1 = n then
9b8f351cced6 added yet another hint to Nitpick's output, this time warning about problems for which nothing was effectively tested
blanchet
parents: 35183
diff changeset
   937
            let
9b8f351cced6 added yet another hint to Nitpick's output, this time warning about problems for which nothing was effectively tested
blanchet
parents: 35183
diff changeset
   938
              val (unsound_problems, sound_problems) =
9b8f351cced6 added yet another hint to Nitpick's output, this time warning about problems for which nothing was effectively tested
blanchet
parents: 35183
diff changeset
   939
                List.partition (#unsound o snd) (!generated_problems)
9b8f351cced6 added yet another hint to Nitpick's output, this time warning about problems for which nothing was effectively tested
blanchet
parents: 35183
diff changeset
   940
            in
9b8f351cced6 added yet another hint to Nitpick's output, this time warning about problems for which nothing was effectively tested
blanchet
parents: 35183
diff changeset
   941
              if not (null sound_problems) andalso
9b8f351cced6 added yet another hint to Nitpick's output, this time warning about problems for which nothing was effectively tested
blanchet
parents: 35183
diff changeset
   942
                 forall (KK.is_problem_trivially_false o fst)
9b8f351cced6 added yet another hint to Nitpick's output, this time warning about problems for which nothing was effectively tested
blanchet
parents: 35183
diff changeset
   943
                        sound_problems then
47560
e30323bfc93c added SZS status wrappers in TPTP mode
blanchet
parents: 47559
diff changeset
   944
                print_nt (fn () =>
44395
d39aedffba08 more precise warning
blanchet
parents: 43602
diff changeset
   945
                    "Warning: The conjecture " ^
d39aedffba08 more precise warning
blanchet
parents: 43602
diff changeset
   946
                    (if falsify then "either trivially holds"
d39aedffba08 more precise warning
blanchet
parents: 43602
diff changeset
   947
                     else "is either trivially unsatisfiable") ^
d39aedffba08 more precise warning
blanchet
parents: 43602
diff changeset
   948
                    " for the given scopes or lies outside Nitpick's supported \
35384
88dbcfe75c45 cosmetics
blanchet
parents: 35335
diff changeset
   949
                    \fragment." ^
35185
9b8f351cced6 added yet another hint to Nitpick's output, this time warning about problems for which nothing was effectively tested
blanchet
parents: 35183
diff changeset
   950
                    (if exists (not o KK.is_problem_trivially_false o fst)
9b8f351cced6 added yet another hint to Nitpick's output, this time warning about problems for which nothing was effectively tested
blanchet
parents: 35183
diff changeset
   951
                               unsound_problems then
41992
0e4716fa330a reword Nitpick's wording concerning potential counterexamples
blanchet
parents: 41985
diff changeset
   952
                       " Only potentially spurious " ^ das_wort_model ^
0e4716fa330a reword Nitpick's wording concerning potential counterexamples
blanchet
parents: 41985
diff changeset
   953
                       "s may be found."
35185
9b8f351cced6 added yet another hint to Nitpick's output, this time warning about problems for which nothing was effectively tested
blanchet
parents: 35183
diff changeset
   954
                     else
9b8f351cced6 added yet another hint to Nitpick's output, this time warning about problems for which nothing was effectively tested
blanchet
parents: 35183
diff changeset
   955
                       ""))
9b8f351cced6 added yet another hint to Nitpick's output, this time warning about problems for which nothing was effectively tested
blanchet
parents: 35183
diff changeset
   956
              else
9b8f351cced6 added yet another hint to Nitpick's output, this time warning about problems for which nothing was effectively tested
blanchet
parents: 35183
diff changeset
   957
                ()
9b8f351cced6 added yet another hint to Nitpick's output, this time warning about problems for which nothing was effectively tested
blanchet
parents: 35183
diff changeset
   958
            end
9b8f351cced6 added yet another hint to Nitpick's output, this time warning about problems for which nothing was effectively tested
blanchet
parents: 35183
diff changeset
   959
          else
9b8f351cced6 added yet another hint to Nitpick's output, this time warning about problems for which nothing was effectively tested
blanchet
parents: 35183
diff changeset
   960
            ()
33192
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   961
      in
35671
ed2c3830d881 improved Nitpick's precision for "card" and "setsum" + fix incorrect outcome code w.r.t. "bisim_depth = -1"
blanchet
parents: 35665
diff changeset
   962
        solve_any_problem (found_really_genuine, max_potential, max_genuine,
ed2c3830d881 improved Nitpick's precision for "card" and "setsum" + fix incorrect outcome code w.r.t. "bisim_depth = -1"
blanchet
parents: 35665
diff changeset
   963
                           donno) true (rev problems)
33192
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   964
      end
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   965
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   966
    fun scope_count (problems : rich_problem list) scope =
35814
234eaa508359 added one-entry cache around Kodkod invocation
blanchet
parents: 35807
diff changeset
   967
      length (filter (curry scopes_equivalent scope o #scope o snd) problems)
33192
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   968
    fun excipit did_so_and_so =
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   969
      let
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   970
        val do_filter =
35185
9b8f351cced6 added yet another hint to Nitpick's output, this time warning about problems for which nothing was effectively tested
blanchet
parents: 35183
diff changeset
   971
          if !met_potential = max_potential then filter_out (#unsound o snd)
33192
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   972
          else I
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   973
        val total = length (!scopes)
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   974
        val unsat =
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   975
          fold (fn scope =>
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   976
                   case scope_count (do_filter (!generated_problems)) scope of
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   977
                     0 => I
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   978
                   | 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
   979
                     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
   980
                                 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
   981
                     ? Integer.add 1) (!generated_scopes) 0
33192
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   982
      in
47560
e30323bfc93c added SZS status wrappers in TPTP mode
blanchet
parents: 47559
diff changeset
   983
        (if mode = TPTP then "% SZS status Unknown\n" else "") ^
33192
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   984
        "Nitpick " ^ did_so_and_so ^
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   985
        (if is_some (!checked_problems) andalso total > 0 then
39361
blanchet
parents: 39359
diff changeset
   986
           " " ^ string_of_int unsat ^ " of " ^ string_of_int total ^ " scope"
blanchet
parents: 39359
diff changeset
   987
           ^ plural_s total
33192
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   988
         else
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   989
           "") ^ "."
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   990
      end
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   991
37704
c6161bee8486 adapt Nitpick to "prod_case" and "*" -> "sum" renaming;
blanchet
parents: 37497
diff changeset
   992
    val (skipped, the_scopes) =
c6161bee8486 adapt Nitpick to "prod_case" and "*" -> "sum" renaming;
blanchet
parents: 37497
diff changeset
   993
      all_scopes hol_ctxt binarize cards_assigns maxes_assigns iters_assigns
c6161bee8486 adapt Nitpick to "prod_case" and "*" -> "sum" renaming;
blanchet
parents: 37497
diff changeset
   994
                 bitss bisim_depths mono_Ts nonmono_Ts deep_dataTs
c6161bee8486 adapt Nitpick to "prod_case" and "*" -> "sum" renaming;
blanchet
parents: 37497
diff changeset
   995
                 finitizable_dataTs
c6161bee8486 adapt Nitpick to "prod_case" and "*" -> "sum" renaming;
blanchet
parents: 37497
diff changeset
   996
    val _ = if skipped > 0 then
47560
e30323bfc93c added SZS status wrappers in TPTP mode
blanchet
parents: 47559
diff changeset
   997
              print_nt (fn () => "Too many scopes. Skipping " ^
e30323bfc93c added SZS status wrappers in TPTP mode
blanchet
parents: 47559
diff changeset
   998
                                 string_of_int skipped ^ " scope" ^
e30323bfc93c added SZS status wrappers in TPTP mode
blanchet
parents: 47559
diff changeset
   999
                                 plural_s skipped ^
e30323bfc93c added SZS status wrappers in TPTP mode
blanchet
parents: 47559
diff changeset
  1000
                                 ". (Consider using \"mono\" or \
e30323bfc93c added SZS status wrappers in TPTP mode
blanchet
parents: 47559
diff changeset
  1001
                                 \\"merge_type_vars\" to prevent this.)")
37704
c6161bee8486 adapt Nitpick to "prod_case" and "*" -> "sum" renaming;
blanchet
parents: 37497
diff changeset
  1002
            else
c6161bee8486 adapt Nitpick to "prod_case" and "*" -> "sum" renaming;
blanchet
parents: 37497
diff changeset
  1003
              ()
c6161bee8486 adapt Nitpick to "prod_case" and "*" -> "sum" renaming;
blanchet
parents: 37497
diff changeset
  1004
    val _ = scopes := the_scopes
c6161bee8486 adapt Nitpick to "prod_case" and "*" -> "sum" renaming;
blanchet
parents: 37497
diff changeset
  1005
35671
ed2c3830d881 improved Nitpick's precision for "card" and "setsum" + fix incorrect outcome code w.r.t. "bisim_depth = -1"
blanchet
parents: 35665
diff changeset
  1006
    fun run_batches _ _ []
ed2c3830d881 improved Nitpick's precision for "card" and "setsum" + fix incorrect outcome code w.r.t. "bisim_depth = -1"
blanchet
parents: 35665
diff changeset
  1007
                    (found_really_genuine, max_potential, max_genuine, donno) =
33192
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
  1008
        if donno > 0 andalso max_genuine > 0 then
47560
e30323bfc93c added SZS status wrappers in TPTP mode
blanchet
parents: 47559
diff changeset
  1009
          (print_nt (fn () => excipit "checked"); unknownN)
33192
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
  1010
        else if max_genuine = original_max_genuine then
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
  1011
          if max_potential = original_max_potential then
47562
a72239723ae8 tuned SZS status output
blanchet
parents: 47560
diff changeset
  1012
            (print_t (K "% SZS status Unknown");
47560
e30323bfc93c added SZS status wrappers in TPTP mode
blanchet
parents: 47559
diff changeset
  1013
             print_nt (fn () =>
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
  1014
                 "Nitpick found no " ^ das_wort_model ^ "." ^
35183
8580ba651489 reintroduce structural induction hint in Nitpick
blanchet
parents: 35181
diff changeset
  1015
                 (if not standard andalso likely_in_struct_induct_step then
34982
7b8c366e34a2 added support for nonstandard models to Nitpick (based on an idea by Koen Claessen) and did other fixes to Nitpick
blanchet
parents: 34938
diff changeset
  1016
                    " 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
  1017
                    \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
  1018
                  else
43020
abb5d1f907e4 added "try" command, to launch Solve Direct, Quickcheck, Nitpick, Sledgehammer, and Try Methods
blanchet
parents: 42959
diff changeset
  1019
                    "")); if skipped > 0 then unknownN else noneN)
33192
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
  1020
          else
47560
e30323bfc93c added SZS status wrappers in TPTP mode
blanchet
parents: 47559
diff changeset
  1021
            (print_nt (fn () =>
38123
36f649db4a6c clarify Nitpick's output in case of a potential counterexample
blanchet
parents: 37928
diff changeset
  1022
                 excipit ("could not find a" ^
36f649db4a6c clarify Nitpick's output in case of a potential counterexample
blanchet
parents: 37928
diff changeset
  1023
                          (if max_genuine = 1 then
36f649db4a6c clarify Nitpick's output in case of a potential counterexample
blanchet
parents: 37928
diff changeset
  1024
                             " better " ^ das_wort_model ^ "."
36f649db4a6c clarify Nitpick's output in case of a potential counterexample
blanchet
parents: 37928
diff changeset
  1025
                           else
36f649db4a6c clarify Nitpick's output in case of a potential counterexample
blanchet
parents: 37928
diff changeset
  1026
                             "ny better " ^ das_wort_model ^ "s.") ^
36f649db4a6c clarify Nitpick's output in case of a potential counterexample
blanchet
parents: 37928
diff changeset
  1027
                          " It checked"));
43020
abb5d1f907e4 added "try" command, to launch Solve Direct, Quickcheck, Nitpick, Sledgehammer, and Try Methods
blanchet
parents: 42959
diff changeset
  1028
             potentialN)
35671
ed2c3830d881 improved Nitpick's precision for "card" and "setsum" + fix incorrect outcome code w.r.t. "bisim_depth = -1"
blanchet
parents: 35665
diff changeset
  1029
        else if found_really_genuine then
43020
abb5d1f907e4 added "try" command, to launch Solve Direct, Quickcheck, Nitpick, Sledgehammer, and Try Methods
blanchet
parents: 42959
diff changeset
  1030
          genuineN
33192
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
  1031
        else
43020
abb5d1f907e4 added "try" command, to launch Solve Direct, Quickcheck, Nitpick, Sledgehammer, and Try Methods
blanchet
parents: 42959
diff changeset
  1032
          quasi_genuineN
33192
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
  1033
      | run_batches j n (batch :: batches) z =
35671
ed2c3830d881 improved Nitpick's precision for "card" and "setsum" + fix incorrect outcome code w.r.t. "bisim_depth = -1"
blanchet
parents: 35665
diff changeset
  1034
        let val (z as (_, _, max_genuine, _)) = run_batch j n batch z in
33192
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
  1035
          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
  1036
        end
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
  1037
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
  1038
    val batches = batch_list batch_size (!scopes)
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
  1039
    val outcome_code =
40411
36b7ed41ca9f removed explicit "Interrupt" handling for conformity with async model -- unfortunately the user loses the information about how many scopes were checked, but this needs to be retought with the new interface anyway
blanchet
parents: 40381
diff changeset
  1040
      run_batches 0 (length batches) batches
36b7ed41ca9f removed explicit "Interrupt" handling for conformity with async model -- unfortunately the user loses the information about how many scopes were checked, but this needs to be retought with the new interface anyway
blanchet
parents: 40381
diff changeset
  1041
                  (false, max_potential, max_genuine, 0)
33192
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
  1042
      handle TimeLimit.TimeOut =>
47560
e30323bfc93c added SZS status wrappers in TPTP mode
blanchet
parents: 47559
diff changeset
  1043
             (print_nt (fn () => excipit "ran out of time after checking");
43020
abb5d1f907e4 added "try" command, to launch Solve Direct, Quickcheck, Nitpick, Sledgehammer, and Try Methods
blanchet
parents: 42959
diff changeset
  1044
              if !met_potential > 0 then potentialN else unknownN)
40341
03156257040f standardize on seconds for Nitpick and Sledgehammer timeouts
blanchet
parents: 40223
diff changeset
  1045
    val _ = print_v (fn () =>
03156257040f standardize on seconds for Nitpick and Sledgehammer timeouts
blanchet
parents: 40223
diff changeset
  1046
                "Total time: " ^ string_from_time (Timer.checkRealTimer timer) ^
03156257040f standardize on seconds for Nitpick and Sledgehammer timeouts
blanchet
parents: 40223
diff changeset
  1047
                ".")
33192
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
  1048
  in (outcome_code, !state_ref) end
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
  1049
41051
2ed1b971fc20 give the inner timeout mechanism a chance, since it gives more precise information to the user
blanchet
parents: 41048
diff changeset
  1050
(* Give the inner timeout a chance. *)
41772
27d4c768cf20 make Nitpick's timeout mechanism somewhat more reliable/friendly;
blanchet
parents: 41278
diff changeset
  1051
val timeout_bonus = seconds 1.0
41051
2ed1b971fc20 give the inner timeout mechanism a chance, since it gives more precise information to the user
blanchet
parents: 41048
diff changeset
  1052
43022
7d3ce43d9464 handle non-auto try case gracefully in Nitpick
blanchet
parents: 43020
diff changeset
  1053
fun pick_nits_in_term state (params as {debug, timeout, expect, ...}) mode i n
47715
04400144c6fc handle TPTP definitions as definitions in Nitpick rather than as axioms
blanchet
parents: 47670
diff changeset
  1054
                      step subst def_assm_ts nondef_assm_ts orig_t =
47670
24babc4b1925 added timeout argument to TPTP tools
blanchet
parents: 47564
diff changeset
  1055
  let
24babc4b1925 added timeout argument to TPTP tools
blanchet
parents: 47564
diff changeset
  1056
    val print_nt = if is_mode_nt mode then Output.urgent_message else K ()
24babc4b1925 added timeout argument to TPTP tools
blanchet
parents: 47564
diff changeset
  1057
    val print_t = if mode = TPTP then Output.urgent_message else K ()
24babc4b1925 added timeout argument to TPTP tools
blanchet
parents: 47564
diff changeset
  1058
  in
37213
efcad7594872 fix handling of "split" w.r.t. new definition + fix exception handling w.r.t. "expect" option
blanchet
parents: 37146
diff changeset
  1059
    if getenv "KODKODI" = "" then
37497
71fdbffe3275 distinguish between "unknown" and "no Kodkodi installed" errors
blanchet
parents: 37273
diff changeset
  1060
      (* The "expect" argument is deliberately ignored if Kodkodi is missing so
71fdbffe3275 distinguish between "unknown" and "no Kodkodi installed" errors
blanchet
parents: 37273
diff changeset
  1061
         that the "Nitpick_Examples" can be processed on any machine. *)
47560
e30323bfc93c added SZS status wrappers in TPTP mode
blanchet
parents: 47559
diff changeset
  1062
      (print_nt (Pretty.string_of (plazy install_kodkodi_message));
37497
71fdbffe3275 distinguish between "unknown" and "no Kodkodi installed" errors
blanchet
parents: 37273
diff changeset
  1063
       ("no_kodkodi", state))
37213
efcad7594872 fix handling of "split" w.r.t. new definition + fix exception handling w.r.t. "expect" option
blanchet
parents: 37146
diff changeset
  1064
    else
efcad7594872 fix handling of "split" w.r.t. new definition + fix exception handling w.r.t. "expect" option
blanchet
parents: 37146
diff changeset
  1065
      let
43020
abb5d1f907e4 added "try" command, to launch Solve Direct, Quickcheck, Nitpick, Sledgehammer, and Try Methods
blanchet
parents: 42959
diff changeset
  1066
        val unknown_outcome = (unknownN, state)
37213
efcad7594872 fix handling of "split" w.r.t. new definition + fix exception handling w.r.t. "expect" option
blanchet
parents: 37146
diff changeset
  1067
        val deadline = Option.map (curry Time.+ (Time.now ())) timeout
efcad7594872 fix handling of "split" w.r.t. new definition + fix exception handling w.r.t. "expect" option
blanchet
parents: 37146
diff changeset
  1068
        val outcome as (outcome_code, _) =
41051
2ed1b971fc20 give the inner timeout mechanism a chance, since it gives more precise information to the user
blanchet
parents: 41048
diff changeset
  1069
          time_limit (if debug orelse is_none timeout then NONE
2ed1b971fc20 give the inner timeout mechanism a chance, since it gives more precise information to the user
blanchet
parents: 41048
diff changeset
  1070
                      else SOME (Time.+ (the timeout, timeout_bonus)))
43022
7d3ce43d9464 handle non-auto try case gracefully in Nitpick
blanchet
parents: 43020
diff changeset
  1071
              (pick_them_nits_in_term deadline state params mode i n step subst
47715
04400144c6fc handle TPTP definitions as definitions in Nitpick rather than as axioms
blanchet
parents: 47670
diff changeset
  1072
                                      def_assm_ts nondef_assm_ts) orig_t
37213
efcad7594872 fix handling of "split" w.r.t. new definition + fix exception handling w.r.t. "expect" option
blanchet
parents: 37146
diff changeset
  1073
          handle TOO_LARGE (_, details) =>
47670
24babc4b1925 added timeout argument to TPTP tools
blanchet
parents: 47564
diff changeset
  1074
                 (print_t "% SZS status Unknown";
24babc4b1925 added timeout argument to TPTP tools
blanchet
parents: 47564
diff changeset
  1075
                  print_nt ("Limit reached: " ^ details ^ "."); unknown_outcome)
37213
efcad7594872 fix handling of "split" w.r.t. new definition + fix exception handling w.r.t. "expect" option
blanchet
parents: 37146
diff changeset
  1076
               | TOO_SMALL (_, details) =>
47670
24babc4b1925 added timeout argument to TPTP tools
blanchet
parents: 47564
diff changeset
  1077
                 (print_t "% SZS status Unknown";
24babc4b1925 added timeout argument to TPTP tools
blanchet
parents: 47564
diff changeset
  1078
                  print_nt ("Limit reached: " ^ details ^ "."); unknown_outcome)
37213
efcad7594872 fix handling of "split" w.r.t. new definition + fix exception handling w.r.t. "expect" option
blanchet
parents: 37146
diff changeset
  1079
               | Kodkod.SYNTAX (_, details) =>
47670
24babc4b1925 added timeout argument to TPTP tools
blanchet
parents: 47564
diff changeset
  1080
                 (print_t "% SZS status Unknown";
24babc4b1925 added timeout argument to TPTP tools
blanchet
parents: 47564
diff changeset
  1081
                  print_nt ("Malformed Kodkodi output: " ^ details ^ ".");
37213
efcad7594872 fix handling of "split" w.r.t. new definition + fix exception handling w.r.t. "expect" option
blanchet
parents: 37146
diff changeset
  1082
                  unknown_outcome)
41772
27d4c768cf20 make Nitpick's timeout mechanism somewhat more reliable/friendly;
blanchet
parents: 41278
diff changeset
  1083
               | TimeLimit.TimeOut =>
47670
24babc4b1925 added timeout argument to TPTP tools
blanchet
parents: 47564
diff changeset
  1084
                 (print_t "% SZS status TimedOut";
24babc4b1925 added timeout argument to TPTP tools
blanchet
parents: 47564
diff changeset
  1085
                  print_nt "Nitpick ran out of time."; unknown_outcome)
37213
efcad7594872 fix handling of "split" w.r.t. new definition + fix exception handling w.r.t. "expect" option
blanchet
parents: 37146
diff changeset
  1086
      in
efcad7594872 fix handling of "split" w.r.t. new definition + fix exception handling w.r.t. "expect" option
blanchet
parents: 37146
diff changeset
  1087
        if expect = "" orelse outcome_code = expect then outcome
efcad7594872 fix handling of "split" w.r.t. new definition + fix exception handling w.r.t. "expect" option
blanchet
parents: 37146
diff changeset
  1088
        else error ("Unexpected outcome: " ^ quote outcome_code ^ ".")
efcad7594872 fix handling of "split" w.r.t. new definition + fix exception handling w.r.t. "expect" option
blanchet
parents: 37146
diff changeset
  1089
      end
efcad7594872 fix handling of "split" w.r.t. new definition + fix exception handling w.r.t. "expect" option
blanchet
parents: 37146
diff changeset
  1090
  end
33192
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
  1091
42486
01b03a124b81 direct use of Variable.is_fixed;
wenzelm
parents: 42415
diff changeset
  1092
fun is_fixed_equation ctxt
35335
f715cfde056a support local definitions in Nitpick
blanchet
parents: 35334
diff changeset
  1093
                      (Const (@{const_name "=="}, _) $ Free (s, _) $ Const _) =
42486
01b03a124b81 direct use of Variable.is_fixed;
wenzelm
parents: 42415
diff changeset
  1094
    Variable.is_fixed ctxt s
35335
f715cfde056a support local definitions in Nitpick
blanchet
parents: 35334
diff changeset
  1095
  | is_fixed_equation _ _ = false
f715cfde056a support local definitions in Nitpick
blanchet
parents: 35334
diff changeset
  1096
fun extract_fixed_frees ctxt (assms, t) =
f715cfde056a support local definitions in Nitpick
blanchet
parents: 35334
diff changeset
  1097
  let
f715cfde056a support local definitions in Nitpick
blanchet
parents: 35334
diff changeset
  1098
    val (subst, other_assms) =
42486
01b03a124b81 direct use of Variable.is_fixed;
wenzelm
parents: 42415
diff changeset
  1099
      List.partition (is_fixed_equation ctxt) assms
35335
f715cfde056a support local definitions in Nitpick
blanchet
parents: 35334
diff changeset
  1100
      |>> map Logic.dest_equals
f715cfde056a support local definitions in Nitpick
blanchet
parents: 35334
diff changeset
  1101
  in (subst, other_assms, subst_atomic subst t) end
f715cfde056a support local definitions in Nitpick
blanchet
parents: 35334
diff changeset
  1102
43022
7d3ce43d9464 handle non-auto try case gracefully in Nitpick
blanchet
parents: 43020
diff changeset
  1103
fun pick_nits_in_subgoal state params mode i step =
33192
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
  1104
  let
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
  1105
    val ctxt = Proof.context_of state
33292
affe60b3d864 renamed raw Proof.get_goal to Proof.raw_goal;
wenzelm
parents: 33233
diff changeset
  1106
    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
  1107
  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
  1108
    case Logic.count_prems t of
43020
abb5d1f907e4 added "try" command, to launch Solve Direct, Quickcheck, Nitpick, Sledgehammer, and Try Methods
blanchet
parents: 42959
diff changeset
  1109
      0 => (Output.urgent_message "No subgoal!"; (noneN, 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
  1110
    | n =>
33192
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
  1111
      let
36406
0a2d5138b77c fixes 2a5c6e7b55cb;
blanchet
parents: 36397
diff changeset
  1112
        val t = Logic.goal_params t i |> fst
33192
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
  1113
        val assms = map term_of (Assumption.all_assms_of ctxt)
35335
f715cfde056a support local definitions in Nitpick
blanchet
parents: 35334
diff changeset
  1114
        val (subst, assms, t) = extract_fixed_frees ctxt (assms, t)
47715
04400144c6fc handle TPTP definitions as definitions in Nitpick rather than as axioms
blanchet
parents: 47670
diff changeset
  1115
      in pick_nits_in_term state params mode i n step subst [] assms t end
33192
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
  1116
  end
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
  1117
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
  1118
end;