remove "show_skolems" option and change style of record declarations
authorblanchet
Sun Apr 25 00:25:44 2010 +0200 (2010-04-25)
changeset 36390eee4ee6a5cbe
parent 36389 8228b3a4a2ba
child 36391 8f81c060cf12
remove "show_skolems" option and change style of record declarations
doc-src/Nitpick/nitpick.tex
src/HOL/Tools/Nitpick/HISTORY
src/HOL/Tools/Nitpick/kodkod.ML
src/HOL/Tools/Nitpick/nitpick.ML
src/HOL/Tools/Nitpick/nitpick_hol.ML
src/HOL/Tools/Nitpick/nitpick_isar.ML
src/HOL/Tools/Nitpick/nitpick_model.ML
src/HOL/Tools/Nitpick/nitpick_peephole.ML
src/HOL/Tools/Nitpick/nitpick_scope.ML
     1.1 --- a/doc-src/Nitpick/nitpick.tex	Sun Apr 25 00:10:30 2010 +0200
     1.2 +++ b/doc-src/Nitpick/nitpick.tex	Sun Apr 25 00:25:44 2010 +0200
     1.3 @@ -2190,12 +2190,6 @@
     1.4  {\small See also \textit{overlord} (\S\ref{mode-of-operation}) and
     1.5  \textit{batch\_size} (\S\ref{optimizations}).}
     1.6  
     1.7 -\optrue{show\_skolems}{hide\_skolem}
     1.8 -Specifies whether the values of Skolem constants should be displayed as part of
     1.9 -counterexamples. Skolem constants correspond to bound variables in the original
    1.10 -formula and usually help us to understand why the counterexample falsifies the
    1.11 -formula.
    1.12 -
    1.13  \opfalse{show\_datatypes}{hide\_datatypes}
    1.14  Specifies whether the subsets used to approximate (co)in\-duc\-tive datatypes should
    1.15  be displayed as part of counterexamples. Such subsets are sometimes helpful when
    1.16 @@ -2209,8 +2203,8 @@
    1.17  genuine, but they can clutter the output.
    1.18  
    1.19  \opfalse{show\_all}{dont\_show\_all}
    1.20 -Enabling this option effectively enables \textit{show\_skolems},
    1.21 -\textit{show\_datatypes}, and \textit{show\_consts}.
    1.22 +Enabling this option effectively enables \textit{show\_datatypes} and
    1.23 +\textit{show\_consts}.
    1.24  
    1.25  \opdefault{max\_potential}{int}{$\mathbf{1}$}
    1.26  Specifies the maximum number of potential counterexamples to display. Setting
     2.1 --- a/src/HOL/Tools/Nitpick/HISTORY	Sun Apr 25 00:10:30 2010 +0200
     2.2 +++ b/src/HOL/Tools/Nitpick/HISTORY	Sun Apr 25 00:25:44 2010 +0200
     2.3 @@ -17,8 +17,8 @@
     2.4    * Added cache to speed up repeated Kodkod invocations on the same problems
     2.5    * Renamed "MiniSatJNI", "zChaffJNI", "BerkMinAlloy", and "SAT4JLight" to
     2.6      "MiniSat_JNI", "zChaff_JNI", "BerkMin_Alloy", and "SAT4J_Light"
     2.7 -  * Removed "skolemize", "uncurry", "sym_break", "flatten_prop", and
     2.8 -    "sharing_depth" options
     2.9 +  * Removed "skolemize", "uncurry", "sym_break", "flatten_prop",
    2.10 +    "sharing_depth", and "show_skolems" options
    2.11  
    2.12  Version 2009-1
    2.13  
     3.1 --- a/src/HOL/Tools/Nitpick/kodkod.ML	Sun Apr 25 00:10:30 2010 +0200
     3.2 +++ b/src/HOL/Tools/Nitpick/kodkod.ML	Sun Apr 25 00:25:44 2010 +0200
     3.3 @@ -120,11 +120,10 @@
     3.4      AssignRelReg of n_ary_index * rel_expr |
     3.5      AssignIntReg of int * int_expr
     3.6  
     3.7 -  type 'a fold_expr_funcs = {
     3.8 -    formula_func: formula -> 'a -> 'a,
     3.9 -    rel_expr_func: rel_expr -> 'a -> 'a,
    3.10 -    int_expr_func: int_expr -> 'a -> 'a
    3.11 -  }
    3.12 +  type 'a fold_expr_funcs =
    3.13 +    {formula_func: formula -> 'a -> 'a,
    3.14 +     rel_expr_func: rel_expr -> 'a -> 'a,
    3.15 +     int_expr_func: int_expr -> 'a -> 'a}
    3.16  
    3.17    val fold_formula : 'a fold_expr_funcs -> formula -> 'a -> 'a
    3.18    val fold_rel_expr : 'a fold_expr_funcs -> rel_expr -> 'a -> 'a
    3.19 @@ -132,10 +131,9 @@
    3.20    val fold_decl : 'a fold_expr_funcs -> decl -> 'a -> 'a
    3.21    val fold_expr_assign : 'a fold_expr_funcs -> expr_assign -> 'a -> 'a
    3.22  
    3.23 -  type 'a fold_tuple_funcs = {
    3.24 -    tuple_func: tuple -> 'a -> 'a,
    3.25 -    tuple_set_func: tuple_set -> 'a -> 'a
    3.26 -  }
    3.27 +  type 'a fold_tuple_funcs =
    3.28 +    {tuple_func: tuple -> 'a -> 'a,
    3.29 +     tuple_set_func: tuple_set -> 'a -> 'a}
    3.30  
    3.31    val fold_tuple : 'a fold_tuple_funcs -> tuple -> 'a -> 'a
    3.32    val fold_tuple_set : 'a fold_tuple_funcs -> tuple_set -> 'a -> 'a
    3.33 @@ -144,15 +142,15 @@
    3.34        'a fold_expr_funcs -> 'a fold_tuple_funcs -> bound -> 'a -> 'a
    3.35    val fold_int_bound : 'a fold_tuple_funcs -> int_bound -> 'a -> 'a
    3.36  
    3.37 -  type problem = {
    3.38 -    comment: string,
    3.39 -    settings: setting list,
    3.40 -    univ_card: int,
    3.41 -    tuple_assigns: tuple_assign list,
    3.42 -    bounds: bound list,
    3.43 -    int_bounds: int_bound list,
    3.44 -    expr_assigns: expr_assign list,
    3.45 -    formula: formula}
    3.46 +  type problem =
    3.47 +    {comment: string,
    3.48 +     settings: setting list,
    3.49 +     univ_card: int,
    3.50 +     tuple_assigns: tuple_assign list,
    3.51 +     bounds: bound list,
    3.52 +     int_bounds: int_bound list,
    3.53 +     expr_assigns: expr_assign list,
    3.54 +     formula: formula}
    3.55  
    3.56    type raw_bound = n_ary_index * int list list
    3.57  
    3.58 @@ -291,15 +289,15 @@
    3.59    AssignRelReg of n_ary_index * rel_expr |
    3.60    AssignIntReg of int * int_expr
    3.61  
    3.62 -type problem = {
    3.63 -  comment: string,
    3.64 -  settings: setting list,
    3.65 -  univ_card: int,
    3.66 -  tuple_assigns: tuple_assign list,
    3.67 -  bounds: bound list,
    3.68 -  int_bounds: int_bound list,
    3.69 -  expr_assigns: expr_assign list,
    3.70 -  formula: formula}
    3.71 +type problem =
    3.72 +  {comment: string,
    3.73 +   settings: setting list,
    3.74 +   univ_card: int,
    3.75 +   tuple_assigns: tuple_assign list,
    3.76 +   bounds: bound list,
    3.77 +   int_bounds: int_bound list,
    3.78 +   expr_assigns: expr_assign list,
    3.79 +   formula: formula}
    3.80  
    3.81  type raw_bound = n_ary_index * int list list
    3.82  
    3.83 @@ -313,11 +311,10 @@
    3.84  
    3.85  exception SYNTAX of string * string
    3.86  
    3.87 -type 'a fold_expr_funcs = {
    3.88 -  formula_func: formula -> 'a -> 'a,
    3.89 -  rel_expr_func: rel_expr -> 'a -> 'a,
    3.90 -  int_expr_func: int_expr -> 'a -> 'a
    3.91 -}
    3.92 +type 'a fold_expr_funcs =
    3.93 +  {formula_func: formula -> 'a -> 'a,
    3.94 +   rel_expr_func: rel_expr -> 'a -> 'a,
    3.95 +   int_expr_func: int_expr -> 'a -> 'a}
    3.96  
    3.97  (** Auxiliary functions on ML representation of Kodkod problems **)
    3.98  
    3.99 @@ -419,10 +416,9 @@
   3.100    | AssignRelReg (x, r) => fold_rel_expr F (RelReg x) #> fold_rel_expr F r
   3.101    | AssignIntReg (x, i) => fold_int_expr F (IntReg x) #> fold_int_expr F i
   3.102  
   3.103 -type 'a fold_tuple_funcs = {
   3.104 -  tuple_func: tuple -> 'a -> 'a,
   3.105 -  tuple_set_func: tuple_set -> 'a -> 'a
   3.106 -}
   3.107 +type 'a fold_tuple_funcs =
   3.108 +  {tuple_func: tuple -> 'a -> 'a,
   3.109 +   tuple_set_func: tuple_set -> 'a -> 'a}
   3.110  
   3.111  fun fold_tuple (F : 'a fold_tuple_funcs) = #tuple_func F
   3.112  fun fold_tuple_set F tuple_set =
     4.1 --- a/src/HOL/Tools/Nitpick/nitpick.ML	Sun Apr 25 00:10:30 2010 +0200
     4.2 +++ b/src/HOL/Tools/Nitpick/nitpick.ML	Sun Apr 25 00:25:44 2010 +0200
     4.3 @@ -9,46 +9,45 @@
     4.4  sig
     4.5    type styp = Nitpick_Util.styp
     4.6    type term_postprocessor = Nitpick_Model.term_postprocessor
     4.7 -  type params = {
     4.8 -    cards_assigns: (typ option * int list) list,
     4.9 -    maxes_assigns: (styp option * int list) list,
    4.10 -    iters_assigns: (styp option * int list) list,
    4.11 -    bitss: int list,
    4.12 -    bisim_depths: int list,
    4.13 -    boxes: (typ option * bool option) list,
    4.14 -    finitizes: (typ option * bool option) list,
    4.15 -    monos: (typ option * bool option) list,
    4.16 -    stds: (typ option * bool) list,
    4.17 -    wfs: (styp option * bool option) list,
    4.18 -    sat_solver: string,
    4.19 -    blocking: bool,
    4.20 -    falsify: bool,
    4.21 -    debug: bool,
    4.22 -    verbose: bool,
    4.23 -    overlord: bool,
    4.24 -    user_axioms: bool option,
    4.25 -    assms: bool,
    4.26 -    merge_type_vars: bool,
    4.27 -    binary_ints: bool option,
    4.28 -    destroy_constrs: bool,
    4.29 -    specialize: bool,
    4.30 -    star_linear_preds: bool,
    4.31 -    fast_descrs: bool,
    4.32 -    peephole_optim: bool,
    4.33 -    timeout: Time.time option,
    4.34 -    tac_timeout: Time.time option,
    4.35 -    max_threads: int,
    4.36 -    show_skolems: bool,
    4.37 -    show_datatypes: bool,
    4.38 -    show_consts: bool,
    4.39 -    evals: term list,
    4.40 -    formats: (term option * int list) list,
    4.41 -    max_potential: int,
    4.42 -    max_genuine: int,
    4.43 -    check_potential: bool,
    4.44 -    check_genuine: bool,
    4.45 -    batch_size: int,
    4.46 -    expect: string}
    4.47 +  type params =
    4.48 +    {cards_assigns: (typ option * int list) list,
    4.49 +     maxes_assigns: (styp option * int list) list,
    4.50 +     iters_assigns: (styp option * int list) list,
    4.51 +     bitss: int list,
    4.52 +     bisim_depths: int list,
    4.53 +     boxes: (typ option * bool option) list,
    4.54 +     finitizes: (typ option * bool option) list,
    4.55 +     monos: (typ option * bool option) list,
    4.56 +     stds: (typ option * bool) list,
    4.57 +     wfs: (styp option * bool option) list,
    4.58 +     sat_solver: string,
    4.59 +     blocking: bool,
    4.60 +     falsify: bool,
    4.61 +     debug: bool,
    4.62 +     verbose: bool,
    4.63 +     overlord: bool,
    4.64 +     user_axioms: bool option,
    4.65 +     assms: bool,
    4.66 +     merge_type_vars: bool,
    4.67 +     binary_ints: bool option,
    4.68 +     destroy_constrs: bool,
    4.69 +     specialize: bool,
    4.70 +     star_linear_preds: bool,
    4.71 +     fast_descrs: bool,
    4.72 +     peephole_optim: bool,
    4.73 +     timeout: Time.time option,
    4.74 +     tac_timeout: Time.time option,
    4.75 +     max_threads: int,
    4.76 +     show_datatypes: bool,
    4.77 +     show_consts: bool,
    4.78 +     evals: term list,
    4.79 +     formats: (term option * int list) list,
    4.80 +     max_potential: int,
    4.81 +     max_genuine: int,
    4.82 +     check_potential: bool,
    4.83 +     check_genuine: bool,
    4.84 +     batch_size: int,
    4.85 +     expect: string}
    4.86  
    4.87    val register_frac_type : string -> (string * string) list -> theory -> theory
    4.88    val unregister_frac_type : string -> theory -> theory
    4.89 @@ -80,55 +79,54 @@
    4.90  
    4.91  structure KK = Kodkod
    4.92  
    4.93 -type params = {
    4.94 -  cards_assigns: (typ option * int list) list,
    4.95 -  maxes_assigns: (styp option * int list) list,
    4.96 -  iters_assigns: (styp option * int list) list,
    4.97 -  bitss: int list,
    4.98 -  bisim_depths: int list,
    4.99 -  boxes: (typ option * bool option) list,
   4.100 -  finitizes: (typ option * bool option) list,
   4.101 -  monos: (typ option * bool option) list,
   4.102 -  stds: (typ option * bool) list,
   4.103 -  wfs: (styp option * bool option) list,
   4.104 -  sat_solver: string,
   4.105 -  blocking: bool,
   4.106 -  falsify: bool,
   4.107 -  debug: bool,
   4.108 -  verbose: bool,
   4.109 -  overlord: bool,
   4.110 -  user_axioms: bool option,
   4.111 -  assms: bool,
   4.112 -  merge_type_vars: bool,
   4.113 -  binary_ints: bool option,
   4.114 -  destroy_constrs: bool,
   4.115 -  specialize: bool,
   4.116 -  star_linear_preds: bool,
   4.117 -  fast_descrs: bool,
   4.118 -  peephole_optim: bool,
   4.119 -  timeout: Time.time option,
   4.120 -  tac_timeout: Time.time option,
   4.121 -  max_threads: int,
   4.122 -  show_skolems: bool,
   4.123 -  show_datatypes: bool,
   4.124 -  show_consts: bool,
   4.125 -  evals: term list,
   4.126 -  formats: (term option * int list) list,
   4.127 -  max_potential: int,
   4.128 -  max_genuine: int,
   4.129 -  check_potential: bool,
   4.130 -  check_genuine: bool,
   4.131 -  batch_size: int,
   4.132 -  expect: string}
   4.133 +type params =
   4.134 +  {cards_assigns: (typ option * int list) list,
   4.135 +   maxes_assigns: (styp option * int list) list,
   4.136 +   iters_assigns: (styp option * int list) list,
   4.137 +   bitss: int list,
   4.138 +   bisim_depths: int list,
   4.139 +   boxes: (typ option * bool option) list,
   4.140 +   finitizes: (typ option * bool option) list,
   4.141 +   monos: (typ option * bool option) list,
   4.142 +   stds: (typ option * bool) list,
   4.143 +   wfs: (styp option * bool option) list,
   4.144 +   sat_solver: string,
   4.145 +   blocking: bool,
   4.146 +   falsify: bool,
   4.147 +   debug: bool,
   4.148 +   verbose: bool,
   4.149 +   overlord: bool,
   4.150 +   user_axioms: bool option,
   4.151 +   assms: bool,
   4.152 +   merge_type_vars: bool,
   4.153 +   binary_ints: bool option,
   4.154 +   destroy_constrs: bool,
   4.155 +   specialize: bool,
   4.156 +   star_linear_preds: bool,
   4.157 +   fast_descrs: bool,
   4.158 +   peephole_optim: bool,
   4.159 +   timeout: Time.time option,
   4.160 +   tac_timeout: Time.time option,
   4.161 +   max_threads: int,
   4.162 +   show_datatypes: bool,
   4.163 +   show_consts: bool,
   4.164 +   evals: term list,
   4.165 +   formats: (term option * int list) list,
   4.166 +   max_potential: int,
   4.167 +   max_genuine: int,
   4.168 +   check_potential: bool,
   4.169 +   check_genuine: bool,
   4.170 +   batch_size: int,
   4.171 +   expect: string}
   4.172  
   4.173 -type problem_extension = {
   4.174 -  free_names: nut list,
   4.175 -  sel_names: nut list,
   4.176 -  nonsel_names: nut list,
   4.177 -  rel_table: nut NameTable.table,
   4.178 -  unsound: bool,
   4.179 -  scope: scope}
   4.180 -
   4.181 +type problem_extension =
   4.182 +  {free_names: nut list,
   4.183 +   sel_names: nut list,
   4.184 +   nonsel_names: nut list,
   4.185 +   rel_table: nut NameTable.table,
   4.186 +   unsound: bool,
   4.187 +   scope: scope}
   4.188 + 
   4.189  type rich_problem = KK.problem * problem_extension
   4.190  
   4.191  fun pretties_for_formulas _ _ [] = []
   4.192 @@ -191,10 +189,9 @@
   4.193           boxes, finitizes, monos, stds, wfs, sat_solver, falsify, debug,
   4.194           verbose, overlord, user_axioms, assms, merge_type_vars, binary_ints,
   4.195           destroy_constrs, specialize, star_linear_preds, fast_descrs,
   4.196 -         peephole_optim, tac_timeout, max_threads, show_skolems, show_datatypes,
   4.197 -         show_consts, evals, formats, max_potential, max_genuine,
   4.198 -         check_potential, check_genuine, batch_size, ...} =
   4.199 -      params
   4.200 +         peephole_optim, tac_timeout, max_threads, show_datatypes, show_consts,
   4.201 +         evals, formats, max_potential, max_genuine, check_potential,
   4.202 +         check_genuine, batch_size, ...} = params
   4.203      val state_ref = Unsynchronized.ref state
   4.204      val pprint =
   4.205        if auto then
   4.206 @@ -580,8 +577,7 @@
   4.207               : problem_extension) =
   4.208        let
   4.209          val (reconstructed_model, codatatypes_ok) =
   4.210 -          reconstruct_hol_model {show_skolems = show_skolems,
   4.211 -                                 show_datatypes = show_datatypes,
   4.212 +          reconstruct_hol_model {show_datatypes = show_datatypes,
   4.213                                   show_consts = show_consts}
   4.214                scope formats frees free_names sel_names nonsel_names rel_table
   4.215                bounds
     5.1 --- a/src/HOL/Tools/Nitpick/nitpick_hol.ML	Sun Apr 25 00:10:30 2010 +0200
     5.2 +++ b/src/HOL/Tools/Nitpick/nitpick_hol.ML	Sun Apr 25 00:25:44 2010 +0200
     5.3 @@ -13,37 +13,37 @@
     5.4    type unrolled = styp * styp
     5.5    type wf_cache = (styp * (bool * bool)) list
     5.6  
     5.7 -  type hol_context = {
     5.8 -    thy: theory,
     5.9 -    ctxt: Proof.context,
    5.10 -    max_bisim_depth: int,
    5.11 -    boxes: (typ option * bool option) list,
    5.12 -    stds: (typ option * bool) list,
    5.13 -    wfs: (styp option * bool option) list,
    5.14 -    user_axioms: bool option,
    5.15 -    debug: bool,
    5.16 -    binary_ints: bool option,
    5.17 -    destroy_constrs: bool,
    5.18 -    specialize: bool,
    5.19 -    star_linear_preds: bool,
    5.20 -    fast_descrs: bool,
    5.21 -    tac_timeout: Time.time option,
    5.22 -    evals: term list,
    5.23 -    case_names: (string * int) list,
    5.24 -    def_table: const_table,
    5.25 -    nondef_table: const_table,
    5.26 -    user_nondefs: term list,
    5.27 -    simp_table: const_table Unsynchronized.ref,
    5.28 -    psimp_table: const_table,
    5.29 -    choice_spec_table: const_table,
    5.30 -    intro_table: const_table,
    5.31 -    ground_thm_table: term list Inttab.table,
    5.32 -    ersatz_table: (string * string) list,
    5.33 -    skolems: (string * string list) list Unsynchronized.ref,
    5.34 -    special_funs: special_fun list Unsynchronized.ref,
    5.35 -    unrolled_preds: unrolled list Unsynchronized.ref,
    5.36 -    wf_cache: wf_cache Unsynchronized.ref,
    5.37 -    constr_cache: (typ * styp list) list Unsynchronized.ref}
    5.38 +  type hol_context =
    5.39 +    {thy: theory,
    5.40 +     ctxt: Proof.context,
    5.41 +     max_bisim_depth: int,
    5.42 +     boxes: (typ option * bool option) list,
    5.43 +     stds: (typ option * bool) list,
    5.44 +     wfs: (styp option * bool option) list,
    5.45 +     user_axioms: bool option,
    5.46 +     debug: bool,
    5.47 +     binary_ints: bool option,
    5.48 +     destroy_constrs: bool,
    5.49 +     specialize: bool,
    5.50 +     star_linear_preds: bool,
    5.51 +     fast_descrs: bool,
    5.52 +     tac_timeout: Time.time option,
    5.53 +     evals: term list,
    5.54 +     case_names: (string * int) list,
    5.55 +     def_table: const_table,
    5.56 +     nondef_table: const_table,
    5.57 +     user_nondefs: term list,
    5.58 +     simp_table: const_table Unsynchronized.ref,
    5.59 +     psimp_table: const_table,
    5.60 +     choice_spec_table: const_table,
    5.61 +     intro_table: const_table,
    5.62 +     ground_thm_table: term list Inttab.table,
    5.63 +     ersatz_table: (string * string) list,
    5.64 +     skolems: (string * string list) list Unsynchronized.ref,
    5.65 +     special_funs: special_fun list Unsynchronized.ref,
    5.66 +     unrolled_preds: unrolled list Unsynchronized.ref,
    5.67 +     wf_cache: wf_cache Unsynchronized.ref,
    5.68 +     constr_cache: (typ * styp list) list Unsynchronized.ref}
    5.69  
    5.70    datatype fixpoint_kind = Lfp | Gfp | NoFp
    5.71    datatype boxability =
    5.72 @@ -222,37 +222,37 @@
    5.73  type unrolled = styp * styp
    5.74  type wf_cache = (styp * (bool * bool)) list
    5.75  
    5.76 -type hol_context = {
    5.77 -  thy: theory,
    5.78 -  ctxt: Proof.context,
    5.79 -  max_bisim_depth: int,
    5.80 -  boxes: (typ option * bool option) list,
    5.81 -  stds: (typ option * bool) list,
    5.82 -  wfs: (styp option * bool option) list,
    5.83 -  user_axioms: bool option,
    5.84 -  debug: bool,
    5.85 -  binary_ints: bool option,
    5.86 -  destroy_constrs: bool,
    5.87 -  specialize: bool,
    5.88 -  star_linear_preds: bool,
    5.89 -  fast_descrs: bool,
    5.90 -  tac_timeout: Time.time option,
    5.91 -  evals: term list,
    5.92 -  case_names: (string * int) list,
    5.93 -  def_table: const_table,
    5.94 -  nondef_table: const_table,
    5.95 -  user_nondefs: term list,
    5.96 -  simp_table: const_table Unsynchronized.ref,
    5.97 -  psimp_table: const_table,
    5.98 -  choice_spec_table: const_table,
    5.99 -  intro_table: const_table,
   5.100 -  ground_thm_table: term list Inttab.table,
   5.101 -  ersatz_table: (string * string) list,
   5.102 -  skolems: (string * string list) list Unsynchronized.ref,
   5.103 -  special_funs: special_fun list Unsynchronized.ref,
   5.104 -  unrolled_preds: unrolled list Unsynchronized.ref,
   5.105 -  wf_cache: wf_cache Unsynchronized.ref,
   5.106 -  constr_cache: (typ * styp list) list Unsynchronized.ref}
   5.107 +type hol_context =
   5.108 +  {thy: theory,
   5.109 +   ctxt: Proof.context,
   5.110 +   max_bisim_depth: int,
   5.111 +   boxes: (typ option * bool option) list,
   5.112 +   stds: (typ option * bool) list,
   5.113 +   wfs: (styp option * bool option) list,
   5.114 +   user_axioms: bool option,
   5.115 +   debug: bool,
   5.116 +   binary_ints: bool option,
   5.117 +   destroy_constrs: bool,
   5.118 +   specialize: bool,
   5.119 +   star_linear_preds: bool,
   5.120 +   fast_descrs: bool,
   5.121 +   tac_timeout: Time.time option,
   5.122 +   evals: term list,
   5.123 +   case_names: (string * int) list,
   5.124 +   def_table: const_table,
   5.125 +   nondef_table: const_table,
   5.126 +   user_nondefs: term list,
   5.127 +   simp_table: const_table Unsynchronized.ref,
   5.128 +   psimp_table: const_table,
   5.129 +   choice_spec_table: const_table,
   5.130 +   intro_table: const_table,
   5.131 +   ground_thm_table: term list Inttab.table,
   5.132 +   ersatz_table: (string * string) list,
   5.133 +   skolems: (string * string list) list Unsynchronized.ref,
   5.134 +   special_funs: special_fun list Unsynchronized.ref,
   5.135 +   unrolled_preds: unrolled list Unsynchronized.ref,
   5.136 +   wf_cache: wf_cache Unsynchronized.ref,
   5.137 +   constr_cache: (typ * styp list) list Unsynchronized.ref}
   5.138  
   5.139  datatype fixpoint_kind = Lfp | Gfp | NoFp
   5.140  datatype boxability =
     6.1 --- a/src/HOL/Tools/Nitpick/nitpick_isar.ML	Sun Apr 25 00:10:30 2010 +0200
     6.2 +++ b/src/HOL/Tools/Nitpick/nitpick_isar.ML	Sun Apr 25 00:25:44 2010 +0200
     6.3 @@ -65,7 +65,6 @@
     6.4     ("verbose", "false"),
     6.5     ("overlord", "false"),
     6.6     ("show_all", "false"),
     6.7 -   ("show_skolems", "true"),
     6.8     ("show_datatypes", "false"),
     6.9     ("show_consts", "false"),
    6.10     ("format", "1"),
    6.11 @@ -95,7 +94,6 @@
    6.12     ("quiet", "verbose"),
    6.13     ("no_overlord", "overlord"),
    6.14     ("dont_show_all", "show_all"),
    6.15 -   ("hide_skolems", "show_skolems"),
    6.16     ("hide_datatypes", "show_datatypes"),
    6.17     ("hide_consts", "show_consts"),
    6.18     ("trust_potential", "check_potential"),
    6.19 @@ -255,7 +253,6 @@
    6.20      val tac_timeout = lookup_time "tac_timeout"
    6.21      val max_threads = Int.max (0, lookup_int "max_threads")
    6.22      val show_all = debug orelse lookup_bool "show_all"
    6.23 -    val show_skolems = show_all orelse lookup_bool "show_skolems"
    6.24      val show_datatypes = show_all orelse lookup_bool "show_datatypes"
    6.25      val show_consts = show_all orelse lookup_bool "show_consts"
    6.26      val formats = lookup_ints_assigns read_term_polymorphic "format" 0
    6.27 @@ -265,9 +262,10 @@
    6.28      val max_genuine = Int.max (0, lookup_int "max_genuine")
    6.29      val check_potential = lookup_bool "check_potential"
    6.30      val check_genuine = lookup_bool "check_genuine"
    6.31 -    val batch_size = case lookup_int_option "batch_size" of
    6.32 -                       SOME n => Int.max (1, n)
    6.33 -                     | NONE => if debug then 1 else 64
    6.34 +    val batch_size =
    6.35 +      case lookup_int_option "batch_size" of
    6.36 +        SOME n => Int.max (1, n)
    6.37 +      | NONE => if debug then 1 else 64
    6.38      val expect = lookup_string "expect"
    6.39    in
    6.40      {cards_assigns = cards_assigns, maxes_assigns = maxes_assigns,
    6.41 @@ -281,11 +279,10 @@
    6.42       star_linear_preds = star_linear_preds, fast_descrs = fast_descrs,
    6.43       peephole_optim = peephole_optim, timeout = timeout,
    6.44       tac_timeout = tac_timeout, max_threads = max_threads,
    6.45 -     show_skolems = show_skolems, show_datatypes = show_datatypes,
    6.46 -     show_consts = show_consts, formats = formats, evals = evals,
    6.47 -     max_potential = max_potential, max_genuine = max_genuine,
    6.48 -     check_potential = check_potential, check_genuine = check_genuine,
    6.49 -     batch_size = batch_size, expect = expect}
    6.50 +     show_datatypes = show_datatypes, show_consts = show_consts,
    6.51 +     formats = formats, evals = evals, max_potential = max_potential,
    6.52 +     max_genuine = max_genuine, check_potential = check_potential,
    6.53 +     check_genuine = check_genuine, batch_size = batch_size, expect = expect}
    6.54    end
    6.55  
    6.56  fun default_params thy =
    6.57 @@ -382,7 +379,7 @@
    6.58  val parse_nitpick_params_command = parse_params #>> nitpick_params_trans
    6.59  
    6.60  val _ = OuterSyntax.improper_command "nitpick"
    6.61 -            "try to find a counterexample for a given subgoal using Kodkod"
    6.62 +            "try to find a counterexample for a given subgoal using Nitpick"
    6.63              K.diag parse_nitpick_command
    6.64  val _ = OuterSyntax.command "nitpick_params"
    6.65              "set and display the default parameters for Nitpick"
     7.1 --- a/src/HOL/Tools/Nitpick/nitpick_model.ML	Sun Apr 25 00:10:30 2010 +0200
     7.2 +++ b/src/HOL/Tools/Nitpick/nitpick_model.ML	Sun Apr 25 00:25:44 2010 +0200
     7.3 @@ -12,10 +12,10 @@
     7.4    type rep = Nitpick_Rep.rep
     7.5    type nut = Nitpick_Nut.nut
     7.6  
     7.7 -  type params = {
     7.8 -    show_skolems: bool,
     7.9 -    show_datatypes: bool,
    7.10 -    show_consts: bool}
    7.11 +  type params =
    7.12 +    {show_datatypes: bool,
    7.13 +     show_consts: bool}
    7.14 +
    7.15    type term_postprocessor =
    7.16      Proof.context -> string -> (typ -> term list) -> typ -> term -> term
    7.17  
    7.18 @@ -51,10 +51,9 @@
    7.19  
    7.20  structure KK = Kodkod
    7.21  
    7.22 -type params = {
    7.23 -  show_skolems: bool,
    7.24 -  show_datatypes: bool,
    7.25 -  show_consts: bool}
    7.26 +type params =
    7.27 +  {show_datatypes: bool,
    7.28 +   show_consts: bool}
    7.29  
    7.30  type term_postprocessor =
    7.31    Proof.context -> string -> (typ -> term list) -> typ -> term -> term
    7.32 @@ -840,7 +839,7 @@
    7.33          t1 = t2
    7.34      end
    7.35  
    7.36 -fun reconstruct_hol_model {show_skolems, show_datatypes, show_consts}
    7.37 +fun reconstruct_hol_model {show_datatypes, show_consts}
    7.38          ({hol_ctxt = {thy, ctxt, max_bisim_depth, boxes, stds, wfs, user_axioms,
    7.39                        debug, binary_ints, destroy_constrs, specialize,
    7.40                        star_linear_preds, fast_descrs, tac_timeout, evals,
    7.41 @@ -980,7 +979,7 @@
    7.42                | _ => raise TERM ("Nitpick_Model.reconstruct_hol_model",
    7.43                                   [Const x])) all_frees
    7.44      val chunks = block_of_names true "Free variable" free_names @
    7.45 -                 block_of_names show_skolems "Skolem constant" skolem_names @
    7.46 +                 block_of_names true "Skolem constant" skolem_names @
    7.47                   block_of_names true "Evaluated term" eval_names @
    7.48                   block_of_datatypes @ block_of_codatatypes @
    7.49                   block_of_names show_consts "Constant"
     8.1 --- a/src/HOL/Tools/Nitpick/nitpick_peephole.ML	Sun Apr 25 00:10:30 2010 +0200
     8.2 +++ b/src/HOL/Tools/Nitpick/nitpick_peephole.ML	Sun Apr 25 00:25:44 2010 +0200
     8.3 @@ -14,11 +14,11 @@
     8.4    type decl = Kodkod.decl
     8.5    type expr_assign = Kodkod.expr_assign
     8.6  
     8.7 -  type name_pool = {
     8.8 -    rels: n_ary_index list,
     8.9 -    vars: n_ary_index list,
    8.10 -    formula_reg: int,
    8.11 -    rel_reg: int}
    8.12 +  type name_pool =
    8.13 +    {rels: n_ary_index list,
    8.14 +     vars: n_ary_index list,
    8.15 +     formula_reg: int,
    8.16 +     rel_reg: int}
    8.17  
    8.18    val initial_pool : name_pool
    8.19    val not3_rel : n_ary_index
    8.20 @@ -51,39 +51,38 @@
    8.21    val num_seq : int -> int -> int_expr list
    8.22    val s_and : formula -> formula -> formula
    8.23  
    8.24 -  type kodkod_constrs = {
    8.25 -    kk_all: decl list -> formula -> formula,
    8.26 -    kk_exist: decl list -> formula -> formula,
    8.27 -    kk_formula_let: expr_assign list -> formula -> formula,
    8.28 -    kk_formula_if: formula -> formula -> formula -> formula,
    8.29 -    kk_or: formula -> formula -> formula,
    8.30 -    kk_not: formula -> formula,
    8.31 -    kk_iff: formula -> formula -> formula,
    8.32 -    kk_implies: formula -> formula -> formula,
    8.33 -    kk_and: formula -> formula -> formula,
    8.34 -    kk_subset: rel_expr -> rel_expr -> formula,
    8.35 -    kk_rel_eq: rel_expr -> rel_expr -> formula,
    8.36 -    kk_no: rel_expr -> formula,
    8.37 -    kk_lone: rel_expr -> formula,
    8.38 -    kk_one: rel_expr -> formula,
    8.39 -    kk_some: rel_expr -> formula,
    8.40 -    kk_rel_let: expr_assign list -> rel_expr -> rel_expr,
    8.41 -    kk_rel_if: formula -> rel_expr -> rel_expr -> rel_expr,
    8.42 -    kk_union: rel_expr -> rel_expr -> rel_expr,
    8.43 -    kk_difference: rel_expr -> rel_expr -> rel_expr,
    8.44 -    kk_override: rel_expr -> rel_expr -> rel_expr,
    8.45 -    kk_intersect: rel_expr -> rel_expr -> rel_expr,
    8.46 -    kk_product: rel_expr -> rel_expr -> rel_expr,
    8.47 -    kk_join: rel_expr -> rel_expr -> rel_expr,
    8.48 -    kk_closure: rel_expr -> rel_expr,
    8.49 -    kk_reflexive_closure: rel_expr -> rel_expr,
    8.50 -    kk_comprehension: decl list -> formula -> rel_expr,
    8.51 -    kk_project: rel_expr -> int_expr list -> rel_expr,
    8.52 -    kk_project_seq: rel_expr -> int -> int -> rel_expr,
    8.53 -    kk_not3: rel_expr -> rel_expr,
    8.54 -    kk_nat_less: rel_expr -> rel_expr -> rel_expr,
    8.55 -    kk_int_less: rel_expr -> rel_expr -> rel_expr
    8.56 -  }
    8.57 +  type kodkod_constrs =
    8.58 +    {kk_all: decl list -> formula -> formula,
    8.59 +     kk_exist: decl list -> formula -> formula,
    8.60 +     kk_formula_let: expr_assign list -> formula -> formula,
    8.61 +     kk_formula_if: formula -> formula -> formula -> formula,
    8.62 +     kk_or: formula -> formula -> formula,
    8.63 +     kk_not: formula -> formula,
    8.64 +     kk_iff: formula -> formula -> formula,
    8.65 +     kk_implies: formula -> formula -> formula,
    8.66 +     kk_and: formula -> formula -> formula,
    8.67 +     kk_subset: rel_expr -> rel_expr -> formula,
    8.68 +     kk_rel_eq: rel_expr -> rel_expr -> formula,
    8.69 +     kk_no: rel_expr -> formula,
    8.70 +     kk_lone: rel_expr -> formula,
    8.71 +     kk_one: rel_expr -> formula,
    8.72 +     kk_some: rel_expr -> formula,
    8.73 +     kk_rel_let: expr_assign list -> rel_expr -> rel_expr,
    8.74 +     kk_rel_if: formula -> rel_expr -> rel_expr -> rel_expr,
    8.75 +     kk_union: rel_expr -> rel_expr -> rel_expr,
    8.76 +     kk_difference: rel_expr -> rel_expr -> rel_expr,
    8.77 +     kk_override: rel_expr -> rel_expr -> rel_expr,
    8.78 +     kk_intersect: rel_expr -> rel_expr -> rel_expr,
    8.79 +     kk_product: rel_expr -> rel_expr -> rel_expr,
    8.80 +     kk_join: rel_expr -> rel_expr -> rel_expr,
    8.81 +     kk_closure: rel_expr -> rel_expr,
    8.82 +     kk_reflexive_closure: rel_expr -> rel_expr,
    8.83 +     kk_comprehension: decl list -> formula -> rel_expr,
    8.84 +     kk_project: rel_expr -> int_expr list -> rel_expr,
    8.85 +     kk_project_seq: rel_expr -> int -> int -> rel_expr,
    8.86 +     kk_not3: rel_expr -> rel_expr,
    8.87 +     kk_nat_less: rel_expr -> rel_expr -> rel_expr,
    8.88 +     kk_int_less: rel_expr -> rel_expr -> rel_expr}
    8.89  
    8.90    val kodkod_constrs : bool -> int -> int -> int -> kodkod_constrs
    8.91  end;
    8.92 @@ -94,11 +93,11 @@
    8.93  open Kodkod
    8.94  open Nitpick_Util
    8.95  
    8.96 -type name_pool = {
    8.97 -  rels: n_ary_index list,
    8.98 -  vars: n_ary_index list,
    8.99 -  formula_reg: int,
   8.100 -  rel_reg: int}
   8.101 +type name_pool =
   8.102 +  {rels: n_ary_index list,
   8.103 +   vars: n_ary_index list,
   8.104 +   formula_reg: int,
   8.105 +   rel_reg: int}
   8.106  
   8.107  (* If you add new built-in relations, make sure to increment the counters here
   8.108     as well to avoid name clashes (which fortunately would be detected by
   8.109 @@ -204,39 +203,38 @@
   8.110    | s_and _ False = False
   8.111    | s_and f1 f2 = And (f1, f2)
   8.112  
   8.113 -type kodkod_constrs = {
   8.114 -  kk_all: decl list -> formula -> formula,
   8.115 -  kk_exist: decl list -> formula -> formula,
   8.116 -  kk_formula_let: expr_assign list -> formula -> formula,
   8.117 -  kk_formula_if: formula -> formula -> formula -> formula,
   8.118 -  kk_or: formula -> formula -> formula,
   8.119 -  kk_not: formula -> formula,
   8.120 -  kk_iff: formula -> formula -> formula,
   8.121 -  kk_implies: formula -> formula -> formula,
   8.122 -  kk_and: formula -> formula -> formula,
   8.123 -  kk_subset: rel_expr -> rel_expr -> formula,
   8.124 -  kk_rel_eq: rel_expr -> rel_expr -> formula,
   8.125 -  kk_no: rel_expr -> formula,
   8.126 -  kk_lone: rel_expr -> formula,
   8.127 -  kk_one: rel_expr -> formula,
   8.128 -  kk_some: rel_expr -> formula,
   8.129 -  kk_rel_let: expr_assign list -> rel_expr -> rel_expr,
   8.130 -  kk_rel_if: formula -> rel_expr -> rel_expr -> rel_expr,
   8.131 -  kk_union: rel_expr -> rel_expr -> rel_expr,
   8.132 -  kk_difference: rel_expr -> rel_expr -> rel_expr,
   8.133 -  kk_override: rel_expr -> rel_expr -> rel_expr,
   8.134 -  kk_intersect: rel_expr -> rel_expr -> rel_expr,
   8.135 -  kk_product: rel_expr -> rel_expr -> rel_expr,
   8.136 -  kk_join: rel_expr -> rel_expr -> rel_expr,
   8.137 -  kk_closure: rel_expr -> rel_expr,
   8.138 -  kk_reflexive_closure: rel_expr -> rel_expr,
   8.139 -  kk_comprehension: decl list -> formula -> rel_expr,
   8.140 -  kk_project: rel_expr -> int_expr list -> rel_expr,
   8.141 -  kk_project_seq: rel_expr -> int -> int -> rel_expr,
   8.142 -  kk_not3: rel_expr -> rel_expr,
   8.143 -  kk_nat_less: rel_expr -> rel_expr -> rel_expr,
   8.144 -  kk_int_less: rel_expr -> rel_expr -> rel_expr
   8.145 -}
   8.146 +type kodkod_constrs =
   8.147 +  {kk_all: decl list -> formula -> formula,
   8.148 +   kk_exist: decl list -> formula -> formula,
   8.149 +   kk_formula_let: expr_assign list -> formula -> formula,
   8.150 +   kk_formula_if: formula -> formula -> formula -> formula,
   8.151 +   kk_or: formula -> formula -> formula,
   8.152 +   kk_not: formula -> formula,
   8.153 +   kk_iff: formula -> formula -> formula,
   8.154 +   kk_implies: formula -> formula -> formula,
   8.155 +   kk_and: formula -> formula -> formula,
   8.156 +   kk_subset: rel_expr -> rel_expr -> formula,
   8.157 +   kk_rel_eq: rel_expr -> rel_expr -> formula,
   8.158 +   kk_no: rel_expr -> formula,
   8.159 +   kk_lone: rel_expr -> formula,
   8.160 +   kk_one: rel_expr -> formula,
   8.161 +   kk_some: rel_expr -> formula,
   8.162 +   kk_rel_let: expr_assign list -> rel_expr -> rel_expr,
   8.163 +   kk_rel_if: formula -> rel_expr -> rel_expr -> rel_expr,
   8.164 +   kk_union: rel_expr -> rel_expr -> rel_expr,
   8.165 +   kk_difference: rel_expr -> rel_expr -> rel_expr,
   8.166 +   kk_override: rel_expr -> rel_expr -> rel_expr,
   8.167 +   kk_intersect: rel_expr -> rel_expr -> rel_expr,
   8.168 +   kk_product: rel_expr -> rel_expr -> rel_expr,
   8.169 +   kk_join: rel_expr -> rel_expr -> rel_expr,
   8.170 +   kk_closure: rel_expr -> rel_expr,
   8.171 +   kk_reflexive_closure: rel_expr -> rel_expr,
   8.172 +   kk_comprehension: decl list -> formula -> rel_expr,
   8.173 +   kk_project: rel_expr -> int_expr list -> rel_expr,
   8.174 +   kk_project_seq: rel_expr -> int -> int -> rel_expr,
   8.175 +   kk_not3: rel_expr -> rel_expr,
   8.176 +   kk_nat_less: rel_expr -> rel_expr -> rel_expr,
   8.177 +   kk_int_less: rel_expr -> rel_expr -> rel_expr}
   8.178  
   8.179  (* We assume throughout that Kodkod variables have a "one" constraint. This is
   8.180     always the case if Kodkod's skolemization is disabled. *)
     9.1 --- a/src/HOL/Tools/Nitpick/nitpick_scope.ML	Sun Apr 25 00:10:30 2010 +0200
     9.2 +++ b/src/HOL/Tools/Nitpick/nitpick_scope.ML	Sun Apr 25 00:25:44 2010 +0200
     9.3 @@ -10,32 +10,32 @@
     9.4    type styp = Nitpick_Util.styp
     9.5    type hol_context = Nitpick_HOL.hol_context
     9.6  
     9.7 -  type constr_spec = {
     9.8 -    const: styp,
     9.9 -    delta: int,
    9.10 -    epsilon: int,
    9.11 -    exclusive: bool,
    9.12 -    explicit_max: int,
    9.13 -    total: bool}
    9.14 +  type constr_spec =
    9.15 +    {const: styp,
    9.16 +     delta: int,
    9.17 +     epsilon: int,
    9.18 +     exclusive: bool,
    9.19 +     explicit_max: int,
    9.20 +     total: bool}
    9.21  
    9.22 -  type dtype_spec = {
    9.23 -    typ: typ,
    9.24 -    card: int,
    9.25 -    co: bool,
    9.26 -    standard: bool,
    9.27 -    complete: bool * bool,
    9.28 -    concrete: bool * bool,
    9.29 -    deep: bool,
    9.30 -    constrs: constr_spec list}
    9.31 +  type dtype_spec =
    9.32 +    {typ: typ,
    9.33 +     card: int,
    9.34 +     co: bool,
    9.35 +     standard: bool,
    9.36 +     complete: bool * bool,
    9.37 +     concrete: bool * bool,
    9.38 +     deep: bool,
    9.39 +     constrs: constr_spec list}
    9.40  
    9.41 -  type scope = {
    9.42 -    hol_ctxt: hol_context,
    9.43 -    binarize: bool,
    9.44 -    card_assigns: (typ * int) list,
    9.45 -    bits: int,
    9.46 -    bisim_depth: int,
    9.47 -    datatypes: dtype_spec list,
    9.48 -    ofs: int Typtab.table}
    9.49 +  type scope =
    9.50 +    {hol_ctxt: hol_context,
    9.51 +     binarize: bool,
    9.52 +     card_assigns: (typ * int) list,
    9.53 +     bits: int,
    9.54 +     bisim_depth: int,
    9.55 +     datatypes: dtype_spec list,
    9.56 +     ofs: int Typtab.table}
    9.57  
    9.58    val datatype_spec : dtype_spec list -> typ -> dtype_spec option
    9.59    val constr_spec : dtype_spec list -> styp -> constr_spec
    9.60 @@ -61,32 +61,32 @@
    9.61  open Nitpick_Util
    9.62  open Nitpick_HOL
    9.63  
    9.64 -type constr_spec = {
    9.65 -  const: styp,
    9.66 -  delta: int,
    9.67 -  epsilon: int,
    9.68 -  exclusive: bool,
    9.69 -  explicit_max: int,
    9.70 -  total: bool}
    9.71 +type constr_spec =
    9.72 +  {const: styp,
    9.73 +   delta: int,
    9.74 +   epsilon: int,
    9.75 +   exclusive: bool,
    9.76 +   explicit_max: int,
    9.77 +   total: bool}
    9.78  
    9.79 -type dtype_spec = {
    9.80 -  typ: typ,
    9.81 -  card: int,
    9.82 -  co: bool,
    9.83 -  standard: bool,
    9.84 -  complete: bool * bool,
    9.85 -  concrete: bool * bool,
    9.86 -  deep: bool,
    9.87 -  constrs: constr_spec list}
    9.88 +type dtype_spec =
    9.89 +  {typ: typ,
    9.90 +   card: int,
    9.91 +   co: bool,
    9.92 +   standard: bool,
    9.93 +   complete: bool * bool,
    9.94 +   concrete: bool * bool,
    9.95 +   deep: bool,
    9.96 +   constrs: constr_spec list}
    9.97  
    9.98 -type scope = {
    9.99 -  hol_ctxt: hol_context,
   9.100 -  binarize: bool,
   9.101 -  card_assigns: (typ * int) list,
   9.102 -  bits: int,
   9.103 -  bisim_depth: int,
   9.104 -  datatypes: dtype_spec list,
   9.105 -  ofs: int Typtab.table}
   9.106 +type scope =
   9.107 +  {hol_ctxt: hol_context,
   9.108 +   binarize: bool,
   9.109 +   card_assigns: (typ * int) list,
   9.110 +   bits: int,
   9.111 +   bisim_depth: int,
   9.112 +   datatypes: dtype_spec list,
   9.113 +   ofs: int Typtab.table}
   9.114  
   9.115  datatype row_kind = Card of typ | Max of styp
   9.116