src/HOL/Tools/Nitpick/nitpick.ML
changeset 55889 6bfbec3dff62
parent 55888 cac1add157e8
child 55890 bd7927cca152
     1.1 --- a/src/HOL/Tools/Nitpick/nitpick.ML	Mon Mar 03 22:33:22 2014 +0100
     1.2 +++ b/src/HOL/Tools/Nitpick/nitpick.ML	Mon Mar 03 22:33:22 2014 +0100
     1.3 @@ -7,21 +7,20 @@
     1.4  
     1.5  signature NITPICK =
     1.6  sig
     1.7 -  type styp = Nitpick_Util.styp
     1.8    type term_postprocessor = Nitpick_Model.term_postprocessor
     1.9  
    1.10    datatype mode = Auto_Try | Try | Normal | TPTP
    1.11  
    1.12    type params =
    1.13      {cards_assigns: (typ option * int list) list,
    1.14 -     maxes_assigns: (styp option * int list) list,
    1.15 -     iters_assigns: (styp option * int list) list,
    1.16 +     maxes_assigns: ((string * typ) option * int list) list,
    1.17 +     iters_assigns: ((string * typ) option * int list) list,
    1.18       bitss: int list,
    1.19       bisim_depths: int list,
    1.20       boxes: (typ option * bool option) list,
    1.21       finitizes: (typ option * bool option) list,
    1.22       monos: (typ option * bool option) list,
    1.23 -     wfs: (styp option * bool option) list,
    1.24 +     wfs: ((string * typ) option * bool option) list,
    1.25       sat_solver: string,
    1.26       blocking: bool,
    1.27       falsify: bool,
    1.28 @@ -45,7 +44,7 @@
    1.29       timeout: Time.time,
    1.30       tac_timeout: Time.time,
    1.31       max_threads: int,
    1.32 -     show_datatypes: bool,
    1.33 +     show_types: bool,
    1.34       show_skolems: bool,
    1.35       show_consts: bool,
    1.36       evals: term list,
    1.37 @@ -65,7 +64,8 @@
    1.38    val unknownN : string
    1.39    val register_frac_type : string -> (string * string) list -> theory -> theory
    1.40    val unregister_frac_type : string -> theory -> theory
    1.41 -  val register_codatatype : typ -> string -> styp list -> theory -> theory
    1.42 +  val register_codatatype : typ -> string -> (string * typ) list -> theory ->
    1.43 +    theory
    1.44    val unregister_codatatype : typ -> theory -> theory
    1.45    val register_term_postprocessor :
    1.46      typ -> term_postprocessor -> theory -> theory
    1.47 @@ -99,14 +99,14 @@
    1.48  
    1.49  type params =
    1.50    {cards_assigns: (typ option * int list) list,
    1.51 -   maxes_assigns: (styp option * int list) list,
    1.52 -   iters_assigns: (styp option * int list) list,
    1.53 +   maxes_assigns: ((string * typ) option * int list) list,
    1.54 +   iters_assigns: ((string * typ) option * int list) list,
    1.55     bitss: int list,
    1.56     bisim_depths: int list,
    1.57     boxes: (typ option * bool option) list,
    1.58     finitizes: (typ option * bool option) list,
    1.59     monos: (typ option * bool option) list,
    1.60 -   wfs: (styp option * bool option) list,
    1.61 +   wfs: ((string * typ) option * bool option) list,
    1.62     sat_solver: string,
    1.63     blocking: bool,
    1.64     falsify: bool,
    1.65 @@ -130,7 +130,7 @@
    1.66     timeout: Time.time,
    1.67     tac_timeout: Time.time,
    1.68     max_threads: int,
    1.69 -   show_datatypes: bool,
    1.70 +   show_types: bool,
    1.71     show_skolems: bool,
    1.72     show_consts: bool,
    1.73     evals: term list,
    1.74 @@ -181,13 +181,14 @@
    1.75  
    1.76  val isabelle_wrong_message =
    1.77    "Something appears to be wrong with your Isabelle installation."
    1.78 -fun java_not_found_message () =
    1.79 +val java_not_found_message =
    1.80    "Java could not be launched. " ^ isabelle_wrong_message
    1.81 -fun java_too_old_message () =
    1.82 +val java_too_old_message =
    1.83    "The Java version is too old. " ^ isabelle_wrong_message
    1.84 -fun kodkodi_not_installed_message () =
    1.85 +val kodkodi_not_installed_message =
    1.86    "Nitpick requires the external Java program Kodkodi."
    1.87 -fun kodkodi_too_old_message () = "The installed Kodkodi version is too old."
    1.88 +val kodkodi_too_old_message = "The installed Kodkodi version is too old."
    1.89 +
    1.90  val max_unsound_delay_ms = 200
    1.91  val max_unsound_delay_percent = 2
    1.92  
    1.93 @@ -205,6 +206,7 @@
    1.94  val syntactic_sorts =
    1.95    @{sort "{default,zero,one,plus,minus,uminus,times,inverse,abs,sgn,ord,equal}"} @
    1.96    @{sort numeral}
    1.97 +
    1.98  fun has_tfree_syntactic_sort (TFree (_, S as _ :: _)) =
    1.99      subset (op =) (S, syntactic_sorts)
   1.100    | has_tfree_syntactic_sort _ = false
   1.101 @@ -229,9 +231,9 @@
   1.102           overlord, spy, user_axioms, assms, whacks, merge_type_vars,
   1.103           binary_ints, destroy_constrs, specialize, star_linear_preds,
   1.104           total_consts, needs, peephole_optim, datatype_sym_break,
   1.105 -         kodkod_sym_break, tac_timeout, max_threads, show_datatypes,
   1.106 -         show_skolems, show_consts, evals, formats, atomss, max_potential,
   1.107 -         max_genuine, check_potential, check_genuine, batch_size, ...} = params
   1.108 +         kodkod_sym_break, tac_timeout, max_threads, show_types, show_skolems,
   1.109 +         show_consts, evals, formats, atomss, max_potential, max_genuine,
   1.110 +         check_potential, check_genuine, batch_size, ...} = params
   1.111      val state_ref = Unsynchronized.ref state
   1.112      fun pprint print =
   1.113        if mode = Auto_Try then
   1.114 @@ -652,7 +654,7 @@
   1.115                 "% SZS output start FiniteModel")
   1.116          val (reconstructed_model, codatatypes_ok) =
   1.117            reconstruct_hol_model
   1.118 -              {show_datatypes = show_datatypes, show_skolems = show_skolems,
   1.119 +              {show_types = show_types, show_skolems = show_skolems,
   1.120                 show_consts = show_consts}
   1.121                scope formats atomss real_frees pseudo_frees free_names sel_names
   1.122                nonsel_names rel_table bounds
   1.123 @@ -771,16 +773,16 @@
   1.124            case KK.solve_any_problem debug overlord deadline max_threads
   1.125                                      max_solutions (map fst problems) of
   1.126              KK.JavaNotFound =>
   1.127 -            (print_nt java_not_found_message;
   1.128 +            (print_nt (K java_not_found_message);
   1.129               (found_really_genuine, max_potential, max_genuine, donno + 1))
   1.130            | KK.JavaTooOld =>
   1.131 -            (print_nt java_too_old_message;
   1.132 +            (print_nt (K java_too_old_message);
   1.133               (found_really_genuine, max_potential, max_genuine, donno + 1))
   1.134            | KK.KodkodiNotInstalled =>
   1.135 -            (print_nt kodkodi_not_installed_message;
   1.136 +            (print_nt (K kodkodi_not_installed_message);
   1.137               (found_really_genuine, max_potential, max_genuine, donno + 1))
   1.138            | KK.KodkodiTooOld =>
   1.139 -            (print_nt kodkodi_too_old_message;
   1.140 +            (print_nt (K kodkodi_too_old_message);
   1.141               (found_really_genuine, max_potential, max_genuine, donno + 1))
   1.142            | KK.Normal ([], unsat_js, s) =>
   1.143              (update_checked_problems problems unsat_js; show_kodkod_warning s;
   1.144 @@ -1029,7 +1031,7 @@
   1.145      if getenv "KODKODI" = "" then
   1.146        (* The "expect" argument is deliberately ignored if Kodkodi is missing so
   1.147           that the "Nitpick_Examples" can be processed on any machine. *)
   1.148 -      (print_nt (Pretty.string_of (plazy kodkodi_not_installed_message));
   1.149 +      (print_nt (Pretty.string_of (plazy (K kodkodi_not_installed_message)));
   1.150         ("no_kodkodi", state))
   1.151      else
   1.152        let
   1.153 @@ -1062,6 +1064,7 @@
   1.154                        (Const (@{const_name "=="}, _) $ Free (s, _) $ Const _) =
   1.155      Variable.is_fixed ctxt s
   1.156    | is_fixed_equation _ _ = false
   1.157 +
   1.158  fun extract_fixed_frees ctxt (assms, t) =
   1.159    let
   1.160      val (subst, other_assms) =