1.1 --- a/doc-src/Nitpick/nitpick.tex Tue Oct 27 12:16:26 2009 +0100
1.2 +++ b/doc-src/Nitpick/nitpick.tex Tue Oct 27 14:40:24 2009 +0100
1.3 @@ -2381,7 +2381,7 @@
1.4 (``genuine'', ``likely\_genuine'', ``potential'', ``none'', or ``unknown''). The
1.5 \textit{params} type is a large record that lets you set Nitpick's options. The
1.6 current default options can be retrieved by calling the following function
1.7 -defined in the \textit{NitpickIsar} structure:
1.8 +defined in the \textit{Nitpick\_Isar} structure:
1.9
1.10 \prew
1.11 $\textbf{val}\,~\textit{default\_params} :\,
1.12 @@ -2392,7 +2392,7 @@
1.13 put into a \textit{params} record. Here is an example:
1.14
1.15 \prew
1.16 -$\textbf{val}\,~\textit{params} = \textit{NitpickIsar.default\_params}~\textit{thy}~[(\textrm{``}\textrm{timeout}\textrm{''},\, \textrm{``}\textrm{none}\textrm{''})]$ \\
1.17 +$\textbf{val}\,~\textit{params} = \textit{Nitpick\_Isar.default\_params}~\textit{thy}~[(\textrm{``}\textrm{timeout}\textrm{''},\, \textrm{``}\textrm{none}\textrm{''})]$ \\
1.18 $\textbf{val}\,~(\textit{outcome},\, \textit{state}') = \textit{Nitpick.pick\_nits\_in\_subgoal}~\begin{aligned}[t]
1.19 & \textit{state}~\textit{params}~\textit{false} \\[-2pt]
1.20 & \textit{subgoal}\end{aligned}$
2.1 --- a/src/HOL/Nitpick_Examples/Mono_Nits.thy Tue Oct 27 12:16:26 2009 +0100
2.2 +++ b/src/HOL/Nitpick_Examples/Mono_Nits.thy Tue Oct 27 14:40:24 2009 +0100
2.3 @@ -14,8 +14,8 @@
2.4 ML {*
2.5 exception FAIL
2.6
2.7 -val defs = NitpickHOL.all_axioms_of @{theory} |> #1
2.8 -val def_table = NitpickHOL.const_def_table @{context} defs
2.9 +val defs = Nitpick_HOL.all_axioms_of @{theory} |> #1
2.10 +val def_table = Nitpick_HOL.const_def_table @{context} defs
2.11 val ext_ctxt =
2.12 {thy = @{theory}, ctxt = @{context}, max_bisim_depth = ~1, boxes = [],
2.13 user_axioms = NONE, debug = false, wfs = [], destroy_constrs = false,
3.1 --- a/src/HOL/Nitpick_Examples/Tests_Nits.thy Tue Oct 27 12:16:26 2009 +0100
3.2 +++ b/src/HOL/Nitpick_Examples/Tests_Nits.thy Tue Oct 27 14:40:24 2009 +0100
3.3 @@ -11,6 +11,6 @@
3.4 imports Main
3.5 begin
3.6
3.7 -ML {* NitpickTests.run_all_tests () *}
3.8 +ML {* Nitpick_Tests.run_all_tests () *}
3.9
3.10 end
4.1 --- a/src/HOL/Tools/Nitpick/kodkod.ML Tue Oct 27 12:16:26 2009 +0100
4.2 +++ b/src/HOL/Tools/Nitpick/kodkod.ML Tue Oct 27 14:40:24 2009 +0100
4.3 @@ -1044,7 +1044,10 @@
4.4 val code =
4.5 system ("env CLASSPATH=\"$KODKODI_CLASSPATH:$CLASSPATH\" \
4.6 \JAVA_LIBRARY_PATH=\"$KODKODI_JAVA_LIBRARY_PATH:\
4.7 - \$JAVA_LIBRARY_PATH\" \"$ISABELLE_TOOL\" java \
4.8 + \$JAVA_LIBRARY_PATH\" \
4.9 + \LD_LIBRARY_PATH=\"$KODKODI_JAVA_LIBRARY_PATH:\
4.10 + \$LD_LIBRARY_PATH\" \
4.11 + \\"$ISABELLE_TOOL\" java \
4.12 \de.tum.in.isabelle.Kodkodi.Kodkodi" ^
4.13 (if ms >= 0 then " -max-msecs " ^ Int.toString ms
4.14 else "") ^
5.1 --- a/src/HOL/Tools/Nitpick/kodkod_sat.ML Tue Oct 27 12:16:26 2009 +0100
5.2 +++ b/src/HOL/Tools/Nitpick/kodkod_sat.ML Tue Oct 27 14:40:24 2009 +0100
5.3 @@ -12,7 +12,7 @@
5.4 val sat_solver_spec : string -> string * string list
5.5 end;
5.6
5.7 -structure KodkodSAT : KODKOD_SAT =
5.8 +structure Kodkod_SAT : KODKOD_SAT =
5.9 struct
5.10
5.11 datatype sink = ToStdout | ToFile
6.1 --- a/src/HOL/Tools/Nitpick/minipick.ML Tue Oct 27 12:16:26 2009 +0100
6.2 +++ b/src/HOL/Tools/Nitpick/minipick.ML Tue Oct 27 14:40:24 2009 +0100
6.3 @@ -14,10 +14,10 @@
6.4 struct
6.5
6.6 open Kodkod
6.7 -open NitpickUtil
6.8 -open NitpickHOL
6.9 -open NitpickPeephole
6.10 -open NitpickKodkod
6.11 +open Nitpick_Util
6.12 +open Nitpick_HOL
6.13 +open Nitpick_Peephole
6.14 +open Nitpick_Kodkod
6.15
6.16 (* theory -> typ -> unit *)
6.17 fun check_type ctxt (Type ("fun", Ts)) = List.app (check_type ctxt) Ts
7.1 --- a/src/HOL/Tools/Nitpick/nitpick.ML Tue Oct 27 12:16:26 2009 +0100
7.2 +++ b/src/HOL/Tools/Nitpick/nitpick.ML Tue Oct 27 14:40:24 2009 +0100
7.3 @@ -62,15 +62,15 @@
7.4 structure Nitpick : NITPICK =
7.5 struct
7.6
7.7 -open NitpickUtil
7.8 -open NitpickHOL
7.9 -open NitpickMono
7.10 -open NitpickScope
7.11 -open NitpickPeephole
7.12 -open NitpickRep
7.13 -open NitpickNut
7.14 -open NitpickKodkod
7.15 -open NitpickModel
7.16 +open Nitpick_Util
7.17 +open Nitpick_HOL
7.18 +open Nitpick_Mono
7.19 +open Nitpick_Scope
7.20 +open Nitpick_Peephole
7.21 +open Nitpick_Rep
7.22 +open Nitpick_Nut
7.23 +open Nitpick_Kodkod
7.24 +open Nitpick_Model
7.25
7.26 type params = {
7.27 cards_assigns: (typ option * int list) list,
7.28 @@ -355,21 +355,21 @@
7.29 val effective_sat_solver =
7.30 if sat_solver <> "smart" then
7.31 if need_incremental andalso
7.32 - not (sat_solver mem KodkodSAT.configured_sat_solvers true) then
7.33 + not (sat_solver mem Kodkod_SAT.configured_sat_solvers true) then
7.34 (print_m (K ("An incremental SAT solver is required: \"SAT4J\" will \
7.35 \be used instead of " ^ quote sat_solver ^ "."));
7.36 "SAT4J")
7.37 else
7.38 sat_solver
7.39 else
7.40 - KodkodSAT.smart_sat_solver_name need_incremental
7.41 + Kodkod_SAT.smart_sat_solver_name need_incremental
7.42 val _ =
7.43 if sat_solver = "smart" then
7.44 print_v (fn () => "Using SAT solver " ^ quote effective_sat_solver ^
7.45 ". The following" ^
7.46 (if need_incremental then " incremental " else " ") ^
7.47 "solvers are configured: " ^
7.48 - commas (map quote (KodkodSAT.configured_sat_solvers
7.49 + commas (map quote (Kodkod_SAT.configured_sat_solvers
7.50 need_incremental)) ^ ".")
7.51 else
7.52 ()
7.53 @@ -439,7 +439,7 @@
7.54 val formula = fold (fold s_and) [def_fs, nondef_fs] core_f
7.55 val comment = (if liberal then "liberal" else "conservative") ^ "\n" ^
7.56 PrintMode.setmp [] multiline_string_for_scope scope
7.57 - val kodkod_sat_solver = KodkodSAT.sat_solver_spec effective_sat_solver
7.58 + val kodkod_sat_solver = Kodkod_SAT.sat_solver_spec effective_sat_solver
7.59 |> snd
7.60 val delay = if liberal then
7.61 Option.map (fn time => Time.- (time, Time.now ()))
7.62 @@ -483,7 +483,7 @@
7.63 defs = nondef_fs @ def_fs @ declarative_axioms})
7.64 end
7.65 handle LIMIT (loc, msg) =>
7.66 - if loc = "NitpickKodkod.check_arity"
7.67 + if loc = "Nitpick_Kodkod.check_arity"
7.68 andalso not (Typtab.is_empty ofs) then
7.69 problem_for_scope liberal
7.70 {ext_ctxt = ext_ctxt, card_assigns = card_assigns,
8.1 --- a/src/HOL/Tools/Nitpick/nitpick_hol.ML Tue Oct 27 12:16:26 2009 +0100
8.2 +++ b/src/HOL/Tools/Nitpick/nitpick_hol.ML Tue Oct 27 14:40:24 2009 +0100
8.3 @@ -139,10 +139,10 @@
8.4 extended_context -> term -> ((term list * term list) * (bool * bool)) * term
8.5 end;
8.6
8.7 -structure NitpickHOL : NITPICK_HOL =
8.8 +structure Nitpick_HOL : NITPICK_HOL =
8.9 struct
8.10
8.11 -open NitpickUtil
8.12 +open Nitpick_Util
8.13
8.14 type const_table = term list Symtab.table
8.15 type special_fun = (styp * int list * term list) * styp
8.16 @@ -263,7 +263,7 @@
8.17 val after_name_sep = snd o strip_first_name_sep
8.18
8.19 (* When you add constants to these lists, make sure to handle them in
8.20 - "NitpickNut.nut_from_term", and perhaps in "NitpickMono.consider_term" as
8.21 + "Nitpick_Nut.nut_from_term", and perhaps in "Nitpick_Mono.consider_term" as
8.22 well. *)
8.23 val built_in_consts =
8.24 [(@{const_name all}, 1),
8.25 @@ -405,7 +405,7 @@
8.26 (* typ -> styp *)
8.27 fun const_for_iterator_type (Type (s, Ts)) = (after_name_sep s, Ts ---> bool_T)
8.28 | const_for_iterator_type T =
8.29 - raise TYPE ("NitpickHOL.const_for_iterator_type", [T], [])
8.30 + raise TYPE ("Nitpick_HOL.const_for_iterator_type", [T], [])
8.31
8.32 (* int -> typ -> typ * typ *)
8.33 fun strip_n_binders 0 T = ([], T)
8.34 @@ -413,7 +413,7 @@
8.35 strip_n_binders (n - 1) T2 |>> cons T1
8.36 | strip_n_binders n (Type (@{type_name fun_box}, Ts)) =
8.37 strip_n_binders n (Type ("fun", Ts))
8.38 - | strip_n_binders _ T = raise TYPE ("NitpickHOL.strip_n_binders", [T], [])
8.39 + | strip_n_binders _ T = raise TYPE ("Nitpick_HOL.strip_n_binders", [T], [])
8.40 (* typ -> typ *)
8.41 val nth_range_type = snd oo strip_n_binders
8.42
8.43 @@ -432,7 +432,7 @@
8.44 fun mk_flat_tuple _ [t] = t
8.45 | mk_flat_tuple (Type ("*", [T1, T2])) (t :: ts) =
8.46 HOLogic.pair_const T1 T2 $ t $ (mk_flat_tuple T2 ts)
8.47 - | mk_flat_tuple T ts = raise TYPE ("NitpickHOL.mk_flat_tuple", [T], ts)
8.48 + | mk_flat_tuple T ts = raise TYPE ("Nitpick_HOL.mk_flat_tuple", [T], ts)
8.49 (* int -> term -> term list *)
8.50 fun dest_n_tuple 1 t = [t]
8.51 | dest_n_tuple n t = HOLogic.dest_prod t ||> dest_n_tuple (n - 1) |> op ::
8.52 @@ -441,7 +441,8 @@
8.53 fun dest_n_tuple_type 1 T = [T]
8.54 | dest_n_tuple_type n (Type (_, [T1, T2])) =
8.55 T1 :: dest_n_tuple_type (n - 1) T2
8.56 - | dest_n_tuple_type _ T = raise TYPE ("NitpickHOL.dest_n_tuple_type", [T], [])
8.57 + | dest_n_tuple_type _ T =
8.58 + raise TYPE ("Nitpick_HOL.dest_n_tuple_type", [T], [])
8.59
8.60 (* (typ * typ) list -> typ -> typ *)
8.61 fun typ_subst [] T = T
8.62 @@ -460,7 +461,7 @@
8.63 (Sign.typ_match thy (Logic.varifyT T1, T1') Vartab.empty))
8.64 (Logic.varifyT T2)
8.65 handle Type.TYPE_MATCH =>
8.66 - raise TYPE ("NitpickHOL.instantiate_type", [T1, T1'], [])
8.67 + raise TYPE ("Nitpick_HOL.instantiate_type", [T1, T1'], [])
8.68
8.69 (* theory -> typ -> typ -> styp *)
8.70 fun repair_constr_type thy body_T' T =
8.71 @@ -483,7 +484,7 @@
8.72 val (co_s, co_Ts) = dest_Type co_T
8.73 val _ =
8.74 if forall is_TFree co_Ts andalso not (has_duplicates (op =) co_Ts) then ()
8.75 - else raise TYPE ("NitpickHOL.register_codatatype", [co_T], [])
8.76 + else raise TYPE ("Nitpick_HOL.register_codatatype", [co_T], [])
8.77 val codatatypes = AList.update (op =) (co_s, (case_name, constr_xs))
8.78 codatatypes
8.79 in TheoryData.put {frac_types = frac_types, codatatypes = codatatypes} thy end
8.80 @@ -586,8 +587,8 @@
8.81 fun mate_of_rep_fun thy (x as (_, Type ("fun", [T1 as Type (s', _), T2]))) =
8.82 (case typedef_info thy s' of
8.83 SOME {Abs_name, ...} => (Abs_name, Type ("fun", [T2, T1]))
8.84 - | NONE => raise TERM ("NitpickHOL.mate_of_rep_fun", [Const x]))
8.85 - | mate_of_rep_fun _ x = raise TERM ("NitpickHOL.mate_of_rep_fun", [Const x])
8.86 + | NONE => raise TERM ("Nitpick_HOL.mate_of_rep_fun", [Const x]))
8.87 + | mate_of_rep_fun _ x = raise TERM ("Nitpick_HOL.mate_of_rep_fun", [Const x])
8.88
8.89 (* theory -> styp -> bool *)
8.90 fun is_coconstr thy (s, T) =
8.91 @@ -874,7 +875,7 @@
8.92 case AList.lookup (op =) asgns T of
8.93 SOME k => k
8.94 | NONE => if T = @{typ bisim_iterator} then 0
8.95 - else raise TYPE ("NitpickHOL.card_of_type", [T], [])
8.96 + else raise TYPE ("Nitpick_HOL.card_of_type", [T], [])
8.97 (* int -> (typ * int) list -> typ -> int *)
8.98 fun bounded_card_of_type max default_card asgns (Type ("fun", [T1, T2])) =
8.99 let
8.100 @@ -894,7 +895,7 @@
8.101 card_of_type asgns T
8.102 else
8.103 card_of_type asgns T
8.104 - handle TYPE ("NitpickHOL.card_of_type", _, _) =>
8.105 + handle TYPE ("Nitpick_HOL.card_of_type", _, _) =>
8.106 default_card)
8.107 (* theory -> int -> (typ * int) list -> typ -> int *)
8.108 fun bounded_precise_card_of_type thy max default_card asgns T =
8.109 @@ -1110,13 +1111,13 @@
8.110 (* term -> term *)
8.111 fun aux (v as Var _) t = lambda v t
8.112 | aux (c as Const (@{const_name TYPE}, T)) t = lambda c t
8.113 - | aux _ _ = raise TERM ("NitpickHOL.normalized_rhs_of", [t])
8.114 + | aux _ _ = raise TERM ("Nitpick_HOL.normalized_rhs_of", [t])
8.115 val (lhs, rhs) =
8.116 case t of
8.117 Const (@{const_name "=="}, _) $ t1 $ t2 => (t1, t2)
8.118 | @{const Trueprop} $ (Const (@{const_name "op ="}, _) $ t1 $ t2) =>
8.119 (t1, t2)
8.120 - | _ => raise TERM ("NitpickHOL.normalized_rhs_of", [t])
8.121 + | _ => raise TERM ("Nitpick_HOL.normalized_rhs_of", [t])
8.122 val args = strip_comb lhs |> snd
8.123 in fold_rev aux args rhs end
8.124
8.125 @@ -1170,7 +1171,7 @@
8.126 case term_under_def t of
8.127 Const (s, _) => (s, t)
8.128 | Free _ => raise NOT_SUPPORTED "local definitions"
8.129 - | t' => raise TERM ("NitpickHOL.pair_for_prop", [t, t'])
8.130 + | t' => raise TERM ("Nitpick_HOL.pair_for_prop", [t, t'])
8.131
8.132 (* (Proof.context -> term list) -> Proof.context -> const_table *)
8.133 fun table_for get ctxt =
8.134 @@ -1308,7 +1309,7 @@
8.135 |> fold_rev (curry absdummy) (func_Ts @ [dataT])
8.136 end
8.137
8.138 -val redefined_in_NitpickDefs_thy =
8.139 +val redefined_in_Nitpick_thy =
8.140 [@{const_name option_case}, @{const_name nat_case}, @{const_name list_case},
8.141 @{const_name list_size}]
8.142
8.143 @@ -1325,7 +1326,8 @@
8.144 select_nth_constr_arg thy constr_x t j res_T
8.145 |> optimized_record_get thy s rec_T' res_T
8.146 end
8.147 - | _ => raise TYPE ("NitpickHOL.optimized_record_get", [rec_T], []))
8.148 + | _ => raise TYPE ("Nitpick_HOL.optimized_record_get", [rec_T],
8.149 + []))
8.150 | j => select_nth_constr_arg thy constr_x t j res_T
8.151 end
8.152 (* theory -> string -> typ -> term -> term -> term *)
8.153 @@ -1380,7 +1382,7 @@
8.154 (is_real_equational_fun ext_ctxt orf is_real_inductive_pred ext_ctxt
8.155 orf (String.isPrefix ubfp_prefix orf String.isPrefix lbfp_prefix) o fst)
8.156 andf (not o has_trivial_definition thy def_table)
8.157 - andf (not o member (op =) redefined_in_NitpickDefs_thy o fst)
8.158 + andf (not o member (op =) redefined_in_Nitpick_thy o fst)
8.159
8.160 (* term * term -> term *)
8.161 fun s_betapply (Const (@{const_name If}, _) $ @{const True} $ t, _) = t
8.162 @@ -1532,7 +1534,7 @@
8.163 else case def_of_const thy def_table x of
8.164 SOME def =>
8.165 if depth > unfold_max_depth then
8.166 - raise LIMIT ("NitpickHOL.unfold_defs_in_term",
8.167 + raise LIMIT ("Nitpick_HOL.unfold_defs_in_term",
8.168 "too many nested definitions (" ^
8.169 string_of_int depth ^ ") while expanding " ^
8.170 quote s)
8.171 @@ -1640,7 +1642,8 @@
8.172 ({thy, ctxt, debug, fast_descrs, tac_timeout, intro_table, ...}
8.173 : extended_context) (x as (_, T)) =
8.174 case def_props_for_const thy fast_descrs intro_table x of
8.175 - [] => raise TERM ("NitpickHOL.is_is_well_founded_inductive_pred", [Const x])
8.176 + [] => raise TERM ("Nitpick_HOL.is_is_well_founded_inductive_pred",
8.177 + [Const x])
8.178 | intro_ts =>
8.179 (case map (triple_for_intro_rule thy x) intro_ts
8.180 |> filter_out (null o #2) of
8.181 @@ -1772,7 +1775,7 @@
8.182 |> ap_split tuple_T bool_T))
8.183 end
8.184 | aux t =
8.185 - raise TERM ("NitpickHOL.linear_pred_base_and_step_rhss.aux", [t])
8.186 + raise TERM ("Nitpick_HOL.linear_pred_base_and_step_rhss.aux", [t])
8.187 in aux end
8.188
8.189 (* extended_context -> styp -> term -> term *)
8.190 @@ -1834,8 +1837,8 @@
8.191 val rhs = case fp_app of
8.192 Const _ $ t =>
8.193 betapply (t, list_comb (Const x', next :: outer_bounds))
8.194 - | _ => raise TERM ("NitpickHOL.unrolled_inductive_pred_const",
8.195 - [fp_app])
8.196 + | _ => raise TERM ("Nitpick_HOL.unrolled_inductive_pred_\
8.197 + \const", [fp_app])
8.198 val (inner, naked_rhs) = strip_abs rhs
8.199 val all = outer @ inner
8.200 val bounds = map Bound (length all - 1 downto 0)
8.201 @@ -1854,7 +1857,7 @@
8.202 val outer_bounds = map Bound (length outer - 1 downto 0)
8.203 val rhs = case fp_app of
8.204 Const _ $ t => betapply (t, list_comb (Const x, outer_bounds))
8.205 - | _ => raise TERM ("NitpickHOL.raw_inductive_pred_axiom",
8.206 + | _ => raise TERM ("Nitpick_HOL.raw_inductive_pred_axiom",
8.207 [fp_app])
8.208 val (inner, naked_rhs) = strip_abs rhs
8.209 val all = outer @ inner
8.210 @@ -1876,7 +1879,7 @@
8.211 (* extended_context -> styp -> term list *)
8.212 fun raw_equational_fun_axioms (ext_ctxt as {thy, fast_descrs, simp_table,
8.213 psimp_table, ...}) (x as (s, _)) =
8.214 - if s mem redefined_in_NitpickDefs_thy then
8.215 + if s mem redefined_in_Nitpick_thy then
8.216 []
8.217 else case def_props_for_const thy fast_descrs (!simp_table) x of
8.218 [] => (case def_props_for_const thy fast_descrs psimp_table x of
8.219 @@ -2329,7 +2332,7 @@
8.220 ts
8.221 (* (term * int list) list -> term *)
8.222 fun mk_connection [] =
8.223 - raise ARG ("NitpickHOL.push_quantifiers_inward.aux.\
8.224 + raise ARG ("Nitpick_HOL.push_quantifiers_inward.aux.\
8.225 \mk_connection", "")
8.226 | mk_connection ts_cum_bounds =
8.227 ts_cum_bounds |> map fst
8.228 @@ -2720,7 +2723,7 @@
8.229 |> new_s <> "fun"
8.230 ? construct_value thy (@{const_name FunBox},
8.231 Type ("fun", new_Ts) --> new_T) o single
8.232 - | t' => raise TERM ("NitpickHOL.box_fun_and_pair_in_term.\
8.233 + | t' => raise TERM ("Nitpick_HOL.box_fun_and_pair_in_term.\
8.234 \coerce_term", [t']))
8.235 | (Type (new_s, new_Ts as [new_T1, new_T2]),
8.236 Type (old_s, old_Ts as [old_T1, old_T2])) =>
8.237 @@ -2740,7 +2743,7 @@
8.238 else @{const_name PairBox}, new_Ts ---> new_T)
8.239 [coerce_term Ts new_T1 old_T1 t1,
8.240 coerce_term Ts new_T2 old_T2 t2]
8.241 - | t' => raise TERM ("NitpickHOL.box_fun_and_pair_in_term.\
8.242 + | t' => raise TERM ("Nitpick_HOL.box_fun_and_pair_in_term.\
8.243 \coerce_term", [t'])
8.244 else
8.245 raise TYPE ("coerce_term", [new_T, old_T], [t])
8.246 @@ -2753,7 +2756,7 @@
8.247 (case T' of
8.248 Type (_, [T1, T2]) =>
8.249 fold (add_boxed_types_for_var z) [(T1, t1), (T2, t2)]
8.250 - | _ => raise TYPE ("NitpickHOL.box_fun_and_pair_in_term.\
8.251 + | _ => raise TYPE ("Nitpick_HOL.box_fun_and_pair_in_term.\
8.252 \add_boxed_types_for_var", [T'], []))
8.253 | _ => exists_subterm (equal (Var z)) t' ? insert (op =) T
8.254 (* typ list -> typ list -> term -> indexname * typ -> typ *)
8.255 @@ -3008,7 +3011,7 @@
8.256 else
8.257 let val accum as (xs, _) = (x :: xs, axs) in
8.258 if depth > axioms_max_depth then
8.259 - raise LIMIT ("NitpickHOL.axioms_for_term.add_axioms_for_term",
8.260 + raise LIMIT ("Nitpick_HOL.axioms_for_term.add_axioms_for_term",
8.261 "too many nested axioms (" ^ string_of_int depth ^
8.262 ")")
8.263 else if Refute.is_const_of_class thy x then
8.264 @@ -3081,7 +3084,7 @@
8.265 [] => t
8.266 | [(x, S)] =>
8.267 Refute.monomorphic_term (Vartab.make [(x, (S, T))]) t
8.268 - | _ => raise TERM ("NitpickHOL.axioms_for_term.\
8.269 + | _ => raise TERM ("Nitpick_HOL.axioms_for_term.\
8.270 \add_axioms_for_sort", [t]))
8.271 class_axioms
8.272 in fold (add_nondef_axiom depth) monomorphic_class_axioms end
9.1 --- a/src/HOL/Tools/Nitpick/nitpick_isar.ML Tue Oct 27 12:16:26 2009 +0100
9.2 +++ b/src/HOL/Tools/Nitpick/nitpick_isar.ML Tue Oct 27 14:40:24 2009 +0100
9.3 @@ -13,13 +13,13 @@
9.4 val default_params : theory -> (string * string) list -> params
9.5 end
9.6
9.7 -structure NitpickIsar : NITPICK_ISAR =
9.8 +structure Nitpick_Isar : NITPICK_ISAR =
9.9 struct
9.10
9.11 -open NitpickUtil
9.12 -open NitpickHOL
9.13 -open NitpickRep
9.14 -open NitpickNut
9.15 +open Nitpick_Util
9.16 +open Nitpick_HOL
9.17 +open Nitpick_Rep
9.18 +open Nitpick_Nut
9.19 open Nitpick
9.20
9.21 type raw_param = string * string list
10.1 --- a/src/HOL/Tools/Nitpick/nitpick_kodkod.ML Tue Oct 27 12:16:26 2009 +0100
10.2 +++ b/src/HOL/Tools/Nitpick/nitpick_kodkod.ML Tue Oct 27 14:40:24 2009 +0100
10.3 @@ -7,10 +7,10 @@
10.4
10.5 signature NITPICK_KODKOD =
10.6 sig
10.7 - type extended_context = NitpickHOL.extended_context
10.8 - type dtype_spec = NitpickScope.dtype_spec
10.9 - type kodkod_constrs = NitpickPeephole.kodkod_constrs
10.10 - type nut = NitpickNut.nut
10.11 + type extended_context = Nitpick_HOL.extended_context
10.12 + type dtype_spec = Nitpick_Scope.dtype_spec
10.13 + type kodkod_constrs = Nitpick_Peephole.kodkod_constrs
10.14 + type nut = Nitpick_Nut.nut
10.15 type nfa_transition = Kodkod.rel_expr * typ
10.16 type nfa_entry = typ * nfa_transition list
10.17 type nfa_table = nfa_entry list
10.18 @@ -37,15 +37,15 @@
10.19 int Typtab.table -> bool -> kodkod_constrs -> nut -> Kodkod.formula
10.20 end;
10.21
10.22 -structure NitpickKodkod : NITPICK_KODKOD =
10.23 +structure Nitpick_Kodkod : NITPICK_KODKOD =
10.24 struct
10.25
10.26 -open NitpickUtil
10.27 -open NitpickHOL
10.28 -open NitpickScope
10.29 -open NitpickPeephole
10.30 -open NitpickRep
10.31 -open NitpickNut
10.32 +open Nitpick_Util
10.33 +open Nitpick_HOL
10.34 +open Nitpick_Scope
10.35 +open Nitpick_Peephole
10.36 +open Nitpick_Rep
10.37 +open Nitpick_Nut
10.38
10.39 type nfa_transition = Kodkod.rel_expr * typ
10.40 type nfa_entry = typ * nfa_transition list
10.41 @@ -89,7 +89,7 @@
10.42 (* int -> int -> unit *)
10.43 fun check_arity univ_card n =
10.44 if n > Kodkod.max_arity univ_card then
10.45 - raise LIMIT ("NitpickKodkod.check_arity",
10.46 + raise LIMIT ("Nitpick_Kodkod.check_arity",
10.47 "arity " ^ string_of_int n ^ " too large for universe of \
10.48 \cardinality " ^ string_of_int univ_card)
10.49 else
10.50 @@ -132,7 +132,7 @@
10.51 (* int -> unit *)
10.52 fun check_table_size k =
10.53 if k > max_table_size then
10.54 - raise LIMIT ("NitpickKodkod.check_table_size",
10.55 + raise LIMIT ("Nitpick_Kodkod.check_table_size",
10.56 "precomputed table too large (" ^ string_of_int k ^ ")")
10.57 else
10.58 ()
10.59 @@ -245,7 +245,7 @@
10.60 ("norm_frac", tabulate_int_op2_2 debug univ_card (int_card, j0)
10.61 isa_norm_frac)
10.62 else
10.63 - raise ARG ("NitpickKodkod.tabulate_built_in_rel", "unknown relation"))
10.64 + raise ARG ("Nitpick_Kodkod.tabulate_built_in_rel", "unknown relation"))
10.65
10.66 (* bool -> int -> int -> int -> int -> int * int -> Kodkod.rel_expr
10.67 -> Kodkod.bound *)
10.68 @@ -266,11 +266,11 @@
10.69 if nick = @{const_name bisim_iterator_max} then
10.70 case R of
10.71 Atom (k, j0) => [Kodkod.TupleSet [Kodkod.Tuple [k - 1 + j0]]]
10.72 - | _ => raise NUT ("NitpickKodkod.bound_for_plain_rel", [u])
10.73 + | _ => raise NUT ("Nitpick_Kodkod.bound_for_plain_rel", [u])
10.74 else
10.75 [Kodkod.TupleSet [], upper_bound_for_rep R])
10.76 | bound_for_plain_rel _ _ u =
10.77 - raise NUT ("NitpickKodkod.bound_for_plain_rel", [u])
10.78 + raise NUT ("Nitpick_Kodkod.bound_for_plain_rel", [u])
10.79
10.80 (* Proof.context -> bool -> dtype_spec list -> nut -> Kodkod.bound *)
10.81 fun bound_for_sel_rel ctxt debug dtypes
10.82 @@ -293,7 +293,7 @@
10.83 end)
10.84 end
10.85 | bound_for_sel_rel _ _ _ u =
10.86 - raise NUT ("NitpickKodkod.bound_for_sel_rel", [u])
10.87 + raise NUT ("Nitpick_Kodkod.bound_for_sel_rel", [u])
10.88
10.89 (* Kodkod.bound list -> Kodkod.bound list *)
10.90 fun merge_bounds bs =
10.91 @@ -320,7 +320,7 @@
10.92 if is_lone_rep R then
10.93 all_combinations_for_rep R |> map singleton_from_combination
10.94 else
10.95 - raise REP ("NitpickKodkod.all_singletons_for_rep", [R])
10.96 + raise REP ("Nitpick_Kodkod.all_singletons_for_rep", [R])
10.97
10.98 (* Kodkod.rel_expr -> Kodkod.rel_expr list *)
10.99 fun unpack_products (Kodkod.Product (r1, r2)) =
10.100 @@ -333,7 +333,7 @@
10.101 val empty_rel_for_rep = empty_n_ary_rel o arity_of_rep
10.102 fun full_rel_for_rep R =
10.103 case atom_schema_of_rep R of
10.104 - [] => raise REP ("NitpickKodkod.full_rel_for_rep", [R])
10.105 + [] => raise REP ("Nitpick_Kodkod.full_rel_for_rep", [R])
10.106 | schema => foldl1 Kodkod.Product (map Kodkod.AtomSeq schema)
10.107
10.108 (* int -> int list -> Kodkod.decl list *)
10.109 @@ -424,7 +424,7 @@
10.110 fun rel_expr_from_formula kk R f =
10.111 case unopt_rep R of
10.112 Atom (2, j0) => atom_from_formula kk j0 f
10.113 - | _ => raise REP ("NitpickKodkod.rel_expr_from_formula", [R])
10.114 + | _ => raise REP ("Nitpick_Kodkod.rel_expr_from_formula", [R])
10.115
10.116 (* kodkod_cotrs -> int -> int -> Kodkod.rel_expr -> Kodkod.rel_expr list *)
10.117 fun unpack_vect_in_chunks ({kk_project_seq, ...} : kodkod_constrs) chunk_arity
10.118 @@ -471,13 +471,13 @@
10.119 if is_lone_rep old_R andalso is_lone_rep new_R
10.120 andalso card = card_of_rep new_R then
10.121 if card >= lone_rep_fallback_max_card then
10.122 - raise LIMIT ("NitpickKodkod.lone_rep_fallback",
10.123 + raise LIMIT ("Nitpick_Kodkod.lone_rep_fallback",
10.124 "too high cardinality (" ^ string_of_int card ^ ")")
10.125 else
10.126 kk_case_switch kk old_R new_R r (all_singletons_for_rep old_R)
10.127 (all_singletons_for_rep new_R)
10.128 else
10.129 - raise REP ("NitpickKodkod.lone_rep_fallback", [old_R, new_R])
10.130 + raise REP ("Nitpick_Kodkod.lone_rep_fallback", [old_R, new_R])
10.131 end
10.132 (* kodkod_constrs -> int * int -> rep -> Kodkod.rel_expr -> Kodkod.rel_expr *)
10.133 and atom_from_rel_expr kk (x as (k, j0)) old_R r =
10.134 @@ -490,7 +490,7 @@
10.135 atom_from_rel_expr kk x (Vect (dom_card, R2'))
10.136 (vect_from_rel_expr kk dom_card R2' old_R r)
10.137 end
10.138 - | Opt _ => raise REP ("NitpickKodkod.atom_from_rel_expr", [old_R])
10.139 + | Opt _ => raise REP ("Nitpick_Kodkod.atom_from_rel_expr", [old_R])
10.140 | _ => lone_rep_fallback kk (Atom x) old_R r
10.141 (* kodkod_constrs -> rep list -> rep -> Kodkod.rel_expr -> Kodkod.rel_expr *)
10.142 and struct_from_rel_expr kk Rs old_R r =
10.143 @@ -515,7 +515,7 @@
10.144 else
10.145 lone_rep_fallback kk (Struct Rs) old_R r
10.146 end
10.147 - | _ => raise REP ("NitpickKodkod.struct_from_rel_expr", [old_R])
10.148 + | _ => raise REP ("Nitpick_Kodkod.struct_from_rel_expr", [old_R])
10.149 (* kodkod_constrs -> int -> rep -> rep -> Kodkod.rel_expr -> Kodkod.rel_expr *)
10.150 and vect_from_rel_expr kk k R old_R r =
10.151 case old_R of
10.152 @@ -530,7 +530,7 @@
10.153 rel_expr_from_formula kk R (#kk_subset kk arg_r r))
10.154 (all_singletons_for_rep R1))
10.155 else
10.156 - raise REP ("NitpickKodkod.vect_from_rel_expr", [old_R])
10.157 + raise REP ("Nitpick_Kodkod.vect_from_rel_expr", [old_R])
10.158 | Func (Unit, R2) => rel_expr_from_rel_expr kk R R2 r
10.159 | Func (R1, R2) =>
10.160 fold1 (#kk_product kk)
10.161 @@ -538,7 +538,7 @@
10.162 rel_expr_from_rel_expr kk R R2
10.163 (kk_n_fold_join kk true R1 R2 arg_r r))
10.164 (all_singletons_for_rep R1))
10.165 - | _ => raise REP ("NitpickKodkod.vect_from_rel_expr", [old_R])
10.166 + | _ => raise REP ("Nitpick_Kodkod.vect_from_rel_expr", [old_R])
10.167 (* kodkod_constrs -> rep -> rep -> rep -> Kodkod.rel_expr -> Kodkod.rel_expr *)
10.168 and func_from_no_opt_rel_expr kk R1 R2 (Atom x) r =
10.169 let
10.170 @@ -555,12 +555,12 @@
10.171 | Func (Atom (1, _), Formula Neut) =>
10.172 (case unopt_rep R2 of
10.173 Atom (2, j0) => atom_from_formula kk j0 (#kk_some kk r)
10.174 - | _ => raise REP ("NitpickKodkod.func_from_no_opt_rel_expr",
10.175 + | _ => raise REP ("Nitpick_Kodkod.func_from_no_opt_rel_expr",
10.176 [old_R, Func (Unit, R2)]))
10.177 | Func (R1', R2') =>
10.178 rel_expr_from_rel_expr kk R2 R2' (#kk_project_seq kk r (arity_of_rep R1')
10.179 (arity_of_rep R2'))
10.180 - | _ => raise REP ("NitpickKodkod.func_from_no_opt_rel_expr",
10.181 + | _ => raise REP ("Nitpick_Kodkod.func_from_no_opt_rel_expr",
10.182 [old_R, Func (Unit, R2)]))
10.183 | func_from_no_opt_rel_expr kk R1 (Formula Neut) old_R r =
10.184 (case old_R of
10.185 @@ -592,7 +592,7 @@
10.186 | Func (R1', Atom (2, j0)) =>
10.187 func_from_no_opt_rel_expr kk R1 (Formula Neut)
10.188 (Func (R1', Formula Neut)) (#kk_join kk r (Kodkod.Atom (j0 + 1)))
10.189 - | _ => raise REP ("NitpickKodkod.func_from_no_opt_rel_expr",
10.190 + | _ => raise REP ("Nitpick_Kodkod.func_from_no_opt_rel_expr",
10.191 [old_R, Func (R1, Formula Neut)]))
10.192 | func_from_no_opt_rel_expr kk R1 R2 old_R r =
10.193 case old_R of
10.194 @@ -621,7 +621,7 @@
10.195 (#kk_rel_eq kk r2 r3)
10.196 end
10.197 end
10.198 - | _ => raise REP ("NitpickKodkod.func_from_no_opt_rel_expr",
10.199 + | _ => raise REP ("Nitpick_Kodkod.func_from_no_opt_rel_expr",
10.200 [old_R, Func (R1, R2)]))
10.201 | Func (Unit, R2') =>
10.202 let val j0 = some_j0 in
10.203 @@ -648,7 +648,7 @@
10.204 (dom_schema @ ran_schema))
10.205 (#kk_subset kk ran_prod app)
10.206 end
10.207 - | _ => raise REP ("NitpickKodkod.func_from_no_opt_rel_expr",
10.208 + | _ => raise REP ("Nitpick_Kodkod.func_from_no_opt_rel_expr",
10.209 [old_R, Func (R1, R2)])
10.210 (* kodkod_constrs -> rep -> rep -> Kodkod.rel_expr -> Kodkod.rel_expr *)
10.211 and rel_expr_from_rel_expr kk new_R old_R r =
10.212 @@ -657,7 +657,7 @@
10.213 val unopt_new_R = unopt_rep new_R
10.214 in
10.215 if unopt_old_R <> old_R andalso unopt_new_R = new_R then
10.216 - raise REP ("NitpickKodkod.rel_expr_from_rel_expr", [old_R, new_R])
10.217 + raise REP ("Nitpick_Kodkod.rel_expr_from_rel_expr", [old_R, new_R])
10.218 else if unopt_new_R = unopt_old_R then
10.219 r
10.220 else
10.221 @@ -666,7 +666,7 @@
10.222 | Struct Rs => struct_from_rel_expr kk Rs
10.223 | Vect (k, R') => vect_from_rel_expr kk k R'
10.224 | Func (R1, R2) => func_from_no_opt_rel_expr kk R1 R2
10.225 - | _ => raise REP ("NitpickKodkod.rel_expr_from_rel_expr",
10.226 + | _ => raise REP ("Nitpick_Kodkod.rel_expr_from_rel_expr",
10.227 [old_R, new_R]))
10.228 unopt_old_R r
10.229 end
10.230 @@ -683,13 +683,13 @@
10.231 else if is_lone_rep R andalso card_of_rep R > 1 then kk_lone (Kodkod.Rel x)
10.232 else Kodkod.True
10.233 | declarative_axiom_for_plain_rel _ u =
10.234 - raise NUT ("NitpickKodkod.declarative_axiom_for_plain_rel", [u])
10.235 + raise NUT ("Nitpick_Kodkod.declarative_axiom_for_plain_rel", [u])
10.236
10.237 (* nut NameTable.table -> styp -> Kodkod.rel_expr * rep * int *)
10.238 fun const_triple rel_table (x as (s, T)) =
10.239 case the_name rel_table (ConstName (s, T, Any)) of
10.240 FreeRel ((n, j), _, R, _) => (Kodkod.Rel (n, j), R, n)
10.241 - | _ => raise TERM ("NitpickKodkod.const_triple", [Const x])
10.242 + | _ => raise TERM ("Nitpick_Kodkod.const_triple", [Const x])
10.243
10.244 (* nut NameTable.table -> styp -> Kodkod.rel_expr *)
10.245 fun discr_rel_expr rel_table = #1 o const_triple rel_table o discr_for_constr
10.246 @@ -849,7 +849,8 @@
10.247 (~1 upto num_sels - 1)
10.248 val j0 = case triples |> hd |> #2 of
10.249 Func (Atom (_, j0), _) => j0
10.250 - | R => raise REP ("NitpickKodkod.uniqueness_axiom_for_constr", [R])
10.251 + | R => raise REP ("Nitpick_Kodkod.uniqueness_axiom_for_constr",
10.252 + [R])
10.253 val set_r = triples |> hd |> #1
10.254 in
10.255 if num_sels = 0 then
10.256 @@ -960,7 +961,7 @@
10.257 let val opt1 = is_opt_rep (rep_of u1) in
10.258 case polar of
10.259 Neut => if opt1 then
10.260 - raise NUT ("NitpickKodkod.to_f (Finite)", [u])
10.261 + raise NUT ("Nitpick_Kodkod.to_f (Finite)", [u])
10.262 else
10.263 Kodkod.True
10.264 | Pos => formula_for_bool (not opt1)
10.265 @@ -992,7 +993,7 @@
10.266 if not (is_opt_rep ran_R) then
10.267 to_set_bool_op kk_implies kk_subset u1 u2
10.268 else if polar = Neut then
10.269 - raise NUT ("NitpickKodkod.to_f (Subset)", [u])
10.270 + raise NUT ("Nitpick_Kodkod.to_f (Subset)", [u])
10.271 else
10.272 let
10.273 (* bool -> nut -> Kodkod.rel_expr *)
10.274 @@ -1102,16 +1103,16 @@
10.275 | Op3 (If, _, _, u1, u2, u3) =>
10.276 kk_formula_if (to_f u1) (to_f u2) (to_f u3)
10.277 | FormulaReg (j, _, _) => Kodkod.FormulaReg j
10.278 - | _ => raise NUT ("NitpickKodkod.to_f", [u]))
10.279 + | _ => raise NUT ("Nitpick_Kodkod.to_f", [u]))
10.280 | Atom (2, j0) => formula_from_atom j0 (to_r u)
10.281 - | _ => raise NUT ("NitpickKodkod.to_f", [u])
10.282 + | _ => raise NUT ("Nitpick_Kodkod.to_f", [u])
10.283 (* polarity -> nut -> Kodkod.formula *)
10.284 and to_f_with_polarity polar u =
10.285 case rep_of u of
10.286 Formula _ => to_f u
10.287 | Atom (2, j0) => formula_from_atom j0 (to_r u)
10.288 | Opt (Atom (2, j0)) => formula_from_opt_atom polar j0 (to_r u)
10.289 - | _ => raise NUT ("NitpickKodkod.to_f_with_polarity", [u])
10.290 + | _ => raise NUT ("Nitpick_Kodkod.to_f_with_polarity", [u])
10.291 (* nut -> Kodkod.rel_expr *)
10.292 and to_r u =
10.293 case u of
10.294 @@ -1142,12 +1143,12 @@
10.295 | Cst (Num j, @{typ int}, R) =>
10.296 (case atom_for_int (card_of_rep R, offset_of_type ofs int_T) j of
10.297 ~1 => if is_opt_rep R then Kodkod.None
10.298 - else raise NUT ("NitpickKodkod.to_r (Num)", [u])
10.299 + else raise NUT ("Nitpick_Kodkod.to_r (Num)", [u])
10.300 | j' => Kodkod.Atom j')
10.301 | Cst (Num j, T, R) =>
10.302 if j < card_of_rep R then Kodkod.Atom (j + offset_of_type ofs T)
10.303 else if is_opt_rep R then Kodkod.None
10.304 - else raise NUT ("NitpickKodkod.to_r", [u])
10.305 + else raise NUT ("Nitpick_Kodkod.to_r", [u])
10.306 | Cst (Unknown, _, R) => empty_rel_for_rep R
10.307 | Cst (Unrep, _, R) => empty_rel_for_rep R
10.308 | Cst (Suc, T, Func (Atom x, _)) =>
10.309 @@ -1177,7 +1178,7 @@
10.310 (kk_product (Kodkod.AtomSeq (max_int_for_card int_k + 1, nat_j0))
10.311 Kodkod.Univ)
10.312 else
10.313 - raise BAD ("NitpickKodkod.to_r (NatToInt)", "\"nat_j0 <> int_j0\"")
10.314 + raise BAD ("Nitpick_Kodkod.to_r (NatToInt)", "\"nat_j0 <> int_j0\"")
10.315 | Cst (IntToNat, _, Func (Atom (int_k, int_j0), nat_R)) =>
10.316 let
10.317 val abs_card = max_int_for_card int_k + 1
10.318 @@ -1192,7 +1193,7 @@
10.319 (kk_product (Kodkod.AtomSeq (overlap, int_j0))
10.320 Kodkod.Univ))
10.321 else
10.322 - raise BAD ("NitpickKodkod.to_r (IntToNat)", "\"nat_j0 <> int_j0\"")
10.323 + raise BAD ("Nitpick_Kodkod.to_r (IntToNat)", "\"nat_j0 <> int_j0\"")
10.324 end
10.325 | Op1 (Not, _, R, u1) => kk_not3 (to_rep R u1)
10.326 | Op1 (Finite, _, Opt (Atom _), _) => Kodkod.None
10.327 @@ -1204,10 +1205,10 @@
10.328 Func (Struct [R1, R2], _) => (R1, R2)
10.329 | Func (R1, _) =>
10.330 if card_of_rep R1 <> 1 then
10.331 - raise REP ("NitpickKodkod.to_r (Converse)", [R])
10.332 + raise REP ("Nitpick_Kodkod.to_r (Converse)", [R])
10.333 else
10.334 pairself (Atom o pair 1 o offset_of_type ofs) (b_T, a_T)
10.335 - | _ => raise REP ("NitpickKodkod.to_r (Converse)", [R])
10.336 + | _ => raise REP ("Nitpick_Kodkod.to_r (Converse)", [R])
10.337 val body_R = body_rep R
10.338 val a_arity = arity_of_rep a_R
10.339 val b_arity = arity_of_rep b_R
10.340 @@ -1257,7 +1258,7 @@
10.341 (rel_expr_to_func kk R1 bool_atom_R
10.342 (Func (R1, Formula Neut)) r))
10.343 (to_opt R1 u1)
10.344 - | _ => raise NUT ("NitpickKodkod.to_r (SingletonSet)", [u]))
10.345 + | _ => raise NUT ("Nitpick_Kodkod.to_r (SingletonSet)", [u]))
10.346 | Op1 (Tha, T, R, u1) =>
10.347 if is_opt_rep R then
10.348 kk_join (to_rep (Func (unopt_rep R, Opt bool_atom_R)) u1) true_atom
10.349 @@ -1384,7 +1385,7 @@
10.350 kk_product (kk_join (do_nut r a_R b_R u2)
10.351 (do_nut r b_R c_R u1)) r
10.352 in kk_union (do_term true_atom) (do_term false_atom) end
10.353 - | _ => raise NUT ("NitpickKodkod.to_r (Composition)", [u]))
10.354 + | _ => raise NUT ("Nitpick_Kodkod.to_r (Composition)", [u]))
10.355 |> rel_expr_from_rel_expr kk R (Func (Struct [a_R, c_R], body_R))
10.356 end
10.357 | Op2 (Product, T, R, u1, u2) =>
10.358 @@ -1408,7 +1409,7 @@
10.359 fun do_term r =
10.360 kk_product (kk_product (do_nut r a_R u1) (do_nut r b_R u2)) r
10.361 in kk_union (do_term true_atom) (do_term false_atom) end
10.362 - | _ => raise NUT ("NitpickKodkod.to_r (Product)", [u]))
10.363 + | _ => raise NUT ("Nitpick_Kodkod.to_r (Product)", [u]))
10.364 |> rel_expr_from_rel_expr kk R (Func (Struct [a_R, b_R], body_R))
10.365 end
10.366 | Op2 (Image, T, R, u1, u2) =>
10.367 @@ -1437,8 +1438,8 @@
10.368 rel_expr_from_rel_expr kk R core_R core_r
10.369 end
10.370 else
10.371 - raise NUT ("NitpickKodkod.to_r (Image)", [u1, u2])
10.372 - | _ => raise NUT ("NitpickKodkod.to_r (Image)", [u1, u2]))
10.373 + raise NUT ("Nitpick_Kodkod.to_r (Image)", [u1, u2])
10.374 + | _ => raise NUT ("Nitpick_Kodkod.to_r (Image)", [u1, u2]))
10.375 | Op2 (Apply, @{typ nat}, _,
10.376 Op2 (Apply, _, _, Cst (Subtract, _, _), u1), u2) =>
10.377 if is_Cst Unrep u2 andalso not (is_opt_rep (rep_of u1)) then
10.378 @@ -1492,7 +1493,7 @@
10.379 | us' =>
10.380 kk_rel_if (kk_some (fold1 kk_product (map to_r us')))
10.381 (Kodkod.Atom j0) Kodkod.None)
10.382 - | _ => raise NUT ("NitpickKodkod.to_r (Tuple)", [u]))
10.383 + | _ => raise NUT ("Nitpick_Kodkod.to_r (Tuple)", [u]))
10.384 | Construct ([u'], _, _, []) => to_r u'
10.385 | Construct (_ :: sel_us, T, R, arg_us) =>
10.386 let
10.387 @@ -1516,23 +1517,23 @@
10.388 | BoundRel (x, _, _, _) => Kodkod.Var x
10.389 | FreeRel (x, _, _, _) => Kodkod.Rel x
10.390 | RelReg (j, _, R) => Kodkod.RelReg (arity_of_rep R, j)
10.391 - | u => raise NUT ("NitpickKodkod.to_r", [u])
10.392 + | u => raise NUT ("Nitpick_Kodkod.to_r", [u])
10.393 (* nut -> Kodkod.decl *)
10.394 and to_decl (BoundRel (x, _, R, _)) =
10.395 Kodkod.DeclOne (x, Kodkod.AtomSeq (the_single (atom_schema_of_rep R)))
10.396 - | to_decl u = raise NUT ("NitpickKodkod.to_decl", [u])
10.397 + | to_decl u = raise NUT ("Nitpick_Kodkod.to_decl", [u])
10.398 (* nut -> Kodkod.expr_assign *)
10.399 and to_expr_assign (FormulaReg (j, _, R)) u =
10.400 Kodkod.AssignFormulaReg (j, to_f u)
10.401 | to_expr_assign (RelReg (j, _, R)) u =
10.402 Kodkod.AssignRelReg ((arity_of_rep R, j), to_r u)
10.403 - | to_expr_assign u1 _ = raise NUT ("NitpickKodkod.to_expr_assign", [u1])
10.404 + | to_expr_assign u1 _ = raise NUT ("Nitpick_Kodkod.to_expr_assign", [u1])
10.405 (* int * int -> nut -> Kodkod.rel_expr *)
10.406 and to_atom (x as (k, j0)) u =
10.407 case rep_of u of
10.408 Formula _ => atom_from_formula kk j0 (to_f u)
10.409 | Unit => if k = 1 then Kodkod.Atom j0
10.410 - else raise NUT ("NitpickKodkod.to_atom", [u])
10.411 + else raise NUT ("Nitpick_Kodkod.to_atom", [u])
10.412 | R => atom_from_rel_expr kk x R (to_r u)
10.413 (* rep list -> nut -> Kodkod.rel_expr *)
10.414 and to_struct Rs u =
10.415 @@ -1563,7 +1564,7 @@
10.416 | to_rep (Vect (k, R)) u = to_vect k R u
10.417 | to_rep (Func (R1, R2)) u = to_func R1 R2 u
10.418 | to_rep (Opt R) u = to_opt R u
10.419 - | to_rep R _ = raise REP ("NitpickKodkod.to_rep", [R])
10.420 + | to_rep R _ = raise REP ("Nitpick_Kodkod.to_rep", [R])
10.421 (* nut -> Kodkod.rel_expr *)
10.422 and to_integer u = to_opt (one_rep ofs (type_of u) (rep_of u)) u
10.423 (* nut list -> rep -> Kodkod.rel_expr -> Kodkod.rel_expr *)
10.424 @@ -1593,7 +1594,7 @@
10.425 (* rep list -> nut list -> Kodkod.rel_expr *)
10.426 and to_product Rs us =
10.427 case map (uncurry to_opt) (filter (not_equal Unit o fst) (Rs ~~ us)) of
10.428 - [] => raise REP ("NitpickKodkod.to_product", Rs)
10.429 + [] => raise REP ("Nitpick_Kodkod.to_product", Rs)
10.430 | rs => fold1 kk_product rs
10.431 (* int -> typ -> rep -> nut -> Kodkod.rel_expr *)
10.432 and to_nth_pair_sel n res_T res_R u =
10.433 @@ -1639,7 +1640,7 @@
10.434 connective (formula_from_atom j0 r1) (formula_from_atom j0 r2)
10.435 | Func (R1, Atom _) => set_oper (kk_join r1 true_atom)
10.436 (kk_join r2 true_atom)
10.437 - | _ => raise REP ("NitpickKodkod.to_set_bool_op", [min_R])
10.438 + | _ => raise REP ("Nitpick_Kodkod.to_set_bool_op", [min_R])
10.439 end
10.440 (* (Kodkod.formula -> Kodkod.formula -> Kodkod.formula)
10.441 -> (Kodkod.rel_expr -> Kodkod.rel_expr -> Kodkod.rel_expr)
10.442 @@ -1676,7 +1677,7 @@
10.443 neg_second)))
10.444 false_atom))
10.445 r1 r2
10.446 - | _ => raise REP ("NitpickKodkod.to_set_op", [min_R]))
10.447 + | _ => raise REP ("Nitpick_Kodkod.to_set_op", [min_R]))
10.448 end
10.449 (* rep -> rep -> Kodkod.rel_expr -> nut -> Kodkod.rel_expr *)
10.450 and to_apply res_R func_u arg_u =
10.451 @@ -1713,7 +1714,7 @@
10.452 rel_expr_from_rel_expr kk res_R R2
10.453 (kk_n_fold_join kk true R1 R2 (to_opt R1 arg_u) (to_r func_u))
10.454 |> body_rep R2 = Formula Neut ? to_guard [arg_u] res_R
10.455 - | _ => raise NUT ("NitpickKodkod.to_apply", [func_u])
10.456 + | _ => raise NUT ("Nitpick_Kodkod.to_apply", [func_u])
10.457 (* int -> rep -> rep -> Kodkod.rel_expr -> nut *)
10.458 and to_apply_vect k R' res_R func_r arg_u =
10.459 let
11.1 --- a/src/HOL/Tools/Nitpick/nitpick_model.ML Tue Oct 27 12:16:26 2009 +0100
11.2 +++ b/src/HOL/Tools/Nitpick/nitpick_model.ML Tue Oct 27 14:40:24 2009 +0100
11.3 @@ -7,9 +7,9 @@
11.4
11.5 signature NITPICK_MODEL =
11.6 sig
11.7 - type scope = NitpickScope.scope
11.8 - type rep = NitpickRep.rep
11.9 - type nut = NitpickNut.nut
11.10 + type scope = Nitpick_Scope.scope
11.11 + type rep = Nitpick_Rep.rep
11.12 + type nut = Nitpick_Nut.nut
11.13
11.14 type params = {
11.15 show_skolems: bool,
11.16 @@ -29,15 +29,15 @@
11.17 -> Kodkod.raw_bound list -> term -> bool option
11.18 end;
11.19
11.20 -structure NitpickModel : NITPICK_MODEL =
11.21 +structure Nitpick_Model : NITPICK_MODEL =
11.22 struct
11.23
11.24 -open NitpickUtil
11.25 -open NitpickHOL
11.26 -open NitpickScope
11.27 -open NitpickPeephole
11.28 -open NitpickRep
11.29 -open NitpickNut
11.30 +open Nitpick_Util
11.31 +open Nitpick_HOL
11.32 +open Nitpick_Scope
11.33 +open Nitpick_Peephole
11.34 +open Nitpick_Rep
11.35 +open Nitpick_Nut
11.36
11.37 type params = {
11.38 show_skolems: bool,
11.39 @@ -57,7 +57,7 @@
11.40 prefix ^ substring (short_name s, 0, 1) ^ nat_subscript (j + 1)
11.41 | atom_name prefix (T as TFree (s, _)) j =
11.42 prefix ^ perhaps (try (unprefix "'")) s ^ nat_subscript (j + 1)
11.43 - | atom_name _ T _ = raise TYPE ("NitpickModel.atom_name", [T], [])
11.44 + | atom_name _ T _ = raise TYPE ("Nitpick_Model.atom_name", [T], [])
11.45 (* bool -> typ -> int -> term *)
11.46 fun atom for_auto T j =
11.47 if for_auto then
11.48 @@ -130,7 +130,7 @@
11.49 fun aux (Const (s, _)) = (s <> non_opt_name, ([], []))
11.50 | aux (Const (@{const_name fun_upd}, _) $ t0 $ t1 $ t2) =
11.51 let val (s, (ts1, ts2)) = aux t0 in (s, (t1 :: ts1, t2 :: ts2)) end
11.52 - | aux t = raise TERM ("NitpickModel.dest_plain_fun", [t])
11.53 + | aux t = raise TERM ("Nitpick_Model.dest_plain_fun", [t])
11.54 in apsnd (pairself rev) o aux end
11.55
11.56 (* typ -> term -> term list * term *)
11.57 @@ -138,7 +138,7 @@
11.58 (Const (@{const_name Pair}, _) $ t1 $ t2) =
11.59 break_in_two T2 t2 |>> cons t1
11.60 | break_in_two _ (Const (@{const_name Pair}, _) $ t1 $ t2) = ([t1], t2)
11.61 - | break_in_two _ t = raise TERM ("NitpickModel.break_in_two", [t])
11.62 + | break_in_two _ t = raise TERM ("Nitpick_Model.break_in_two", [t])
11.63 (* typ -> term -> term -> term *)
11.64 fun pair_up (Type ("*", [T1', T2']))
11.65 (t1 as Const (@{const_name Pair},
11.66 @@ -180,7 +180,7 @@
11.67 [T1' --> T2', T1', T2'] ---> T1' --> T2')
11.68 $ do_arrow T1' T2' T1 T2 t0 $ do_term T1' T1 t1 $ do_term T2' T2 t2
11.69 | do_arrow _ _ _ _ t =
11.70 - raise TERM ("NitpickModel.typecast_fun.do_arrow", [t])
11.71 + raise TERM ("Nitpick_Model.typecast_fun.do_arrow", [t])
11.72 and do_fun T1' T2' T1 T2 t =
11.73 case factor_out_types T1' T1 of
11.74 ((_, NONE), (_, NONE)) => t |> do_arrow T1' T2' T1 T2
11.75 @@ -188,7 +188,7 @@
11.76 t |> do_curry T1a T1b T2 |> do_arrow T1' T2' T1a (T1b --> T2)
11.77 | ((T1a', SOME T1b'), (_, NONE)) =>
11.78 t |> do_arrow T1a' (T1b' --> T2') T1 T2 |> do_uncurry T1' T2'
11.79 - | _ => raise TYPE ("NitpickModel.typecast_fun.do_fun", [T1, T1'], [])
11.80 + | _ => raise TYPE ("Nitpick_Model.typecast_fun.do_fun", [T1, T1'], [])
11.81 (* typ -> typ -> term -> term *)
11.82 and do_term (Type ("fun", [T1', T2'])) (Type ("fun", [T1, T2])) t =
11.83 do_fun T1' T2' T1 T2 t
11.84 @@ -198,9 +198,9 @@
11.85 $ do_term T1' T1 t1 $ do_term T2' T2 t2
11.86 | do_term T' T t =
11.87 if T = T' then t
11.88 - else raise TYPE ("NitpickModel.typecast_fun.do_term", [T, T'], [])
11.89 + else raise TYPE ("Nitpick_Model.typecast_fun.do_term", [T, T'], [])
11.90 in if T1' = T1 andalso T2' = T2 then t else do_fun T1' T2' T1 T2 t end
11.91 - | typecast_fun T' _ _ _ = raise TYPE ("NitpickModel.typecast_fun", [T'], [])
11.92 + | typecast_fun T' _ _ _ = raise TYPE ("Nitpick_Model.typecast_fun", [T'], [])
11.93
11.94 (* term -> string *)
11.95 fun truth_const_sort_key @{const True} = "0"
11.96 @@ -302,7 +302,7 @@
11.97 term_for_rep seen T T' (Vect (k1, Atom (k2, 0)))
11.98 [nth_combination (replicate k1 (k2, 0)) j]
11.99 handle General.Subscript =>
11.100 - raise ARG ("NitpickModel.reconstruct_term.term_for_atom",
11.101 + raise ARG ("Nitpick_Model.reconstruct_term.term_for_atom",
11.102 signed_string_of_int j ^ " for " ^
11.103 string_for_rep (Vect (k1, Atom (k2, 0))))
11.104 end
11.105 @@ -350,7 +350,7 @@
11.106 map (fn x => get_first
11.107 (fn ConstName (s', T', R) =>
11.108 if (s', T') = x then SOME R else NONE
11.109 - | u => raise NUT ("NitpickModel.reconstruct_\
11.110 + | u => raise NUT ("Nitpick_Model.reconstruct_\
11.111 \term.term_for_atom", [u]))
11.112 sel_names |> the) sel_xs
11.113 val arg_Rs = map (snd o dest_Func) sel_Rs
11.114 @@ -389,7 +389,7 @@
11.115 | n2 => Const (@{const_name HOL.divide},
11.116 [num_T, num_T] ---> num_T)
11.117 $ mk_num n1 $ mk_num n2)
11.118 - | _ => raise TERM ("NitpickModel.reconstruct_term.term_\
11.119 + | _ => raise TERM ("Nitpick_Model.reconstruct_term.term_\
11.120 \for_atom (Abs_Frac)", ts)
11.121 end
11.122 else if not for_auto andalso is_abs_fun thy constr_x then
11.123 @@ -421,7 +421,7 @@
11.124 and term_for_rep seen T T' Unit [[]] = term_for_atom seen T T' 0
11.125 | term_for_rep seen T T' (R as Atom (k, j0)) [[j]] =
11.126 if j >= j0 andalso j < j0 + k then term_for_atom seen T T' (j - j0)
11.127 - else raise REP ("NitpickModel.reconstruct_term.term_for_rep", [R])
11.128 + else raise REP ("Nitpick_Model.reconstruct_term.term_for_rep", [R])
11.129 | term_for_rep seen (Type ("*", [T1, T2])) _ (Struct [R1, R2]) [js] =
11.130 let
11.131 val arity1 = arity_of_rep R1
11.132 @@ -454,7 +454,7 @@
11.133 | term_for_rep seen T T' (Opt R) jss =
11.134 if null jss then Const (unknown, T) else term_for_rep seen T T' R jss
11.135 | term_for_rep seen T _ R jss =
11.136 - raise ARG ("NitpickModel.reconstruct_term.term_for_rep",
11.137 + raise ARG ("Nitpick_Model.reconstruct_term.term_for_rep",
11.138 Refute.string_of_typ T ^ " " ^ string_for_rep R ^ " " ^
11.139 string_of_int (length jss))
11.140 in
11.141 @@ -576,7 +576,7 @@
11.142 (assign_operator_for_const (s, T),
11.143 user_friendly_const ext_ctxt (base_name, step_name) formats (s, T),
11.144 T)
11.145 - | _ => raise NUT ("NitpickModel.reconstruct_hol_model.\
11.146 + | _ => raise NUT ("Nitpick_Model.reconstruct_hol_model.\
11.147 \pretty_for_assign", [name])
11.148 val t2 = if rep_of name = Any then
11.149 Const (@{const_name undefined}, T')
11.150 @@ -601,7 +601,7 @@
11.151 fun integer_datatype T =
11.152 [{typ = T, card = card_of_type card_assigns T, co = false,
11.153 precise = false, constrs = []}]
11.154 - handle TYPE ("NitpickHOL.card_of_type", _, _) => []
11.155 + handle TYPE ("Nitpick_HOL.card_of_type", _, _) => []
11.156 val (codatatypes, datatypes) =
11.157 List.partition #co datatypes
11.158 ||> append (integer_datatype nat_T @ integer_datatype int_T)
11.159 @@ -637,7 +637,7 @@
11.160 free_names of
11.161 [name] => name
11.162 | [] => FreeName (s, T, Any)
11.163 - | _ => raise TERM ("NitpickModel.reconstruct_hol_model",
11.164 + | _ => raise TERM ("Nitpick_Model.reconstruct_hol_model",
11.165 [Const x])) all_frees
11.166 val chunks = block_of_names true "Free variable" free_names @
11.167 block_of_names show_skolems "Skolem constant" skolem_names @
12.1 --- a/src/HOL/Tools/Nitpick/nitpick_mono.ML Tue Oct 27 12:16:26 2009 +0100
12.2 +++ b/src/HOL/Tools/Nitpick/nitpick_mono.ML Tue Oct 27 14:40:24 2009 +0100
12.3 @@ -7,17 +7,17 @@
12.4
12.5 signature NITPICK_MONO =
12.6 sig
12.7 - type extended_context = NitpickHOL.extended_context
12.8 + type extended_context = Nitpick_HOL.extended_context
12.9
12.10 val formulas_monotonic :
12.11 extended_context -> typ -> term list -> term list -> term -> bool
12.12 end;
12.13
12.14 -structure NitpickMono : NITPICK_MONO =
12.15 +structure Nitpick_Mono : NITPICK_MONO =
12.16 struct
12.17
12.18 -open NitpickUtil
12.19 -open NitpickHOL
12.20 +open Nitpick_Util
12.21 +open Nitpick_HOL
12.22
12.23 type var = int
12.24
12.25 @@ -363,11 +363,11 @@
12.26 accum =
12.27 (accum |> fold (uncurry (do_ctype_comp cmp xs)) [(C11, C21), (C12, C22)]
12.28 handle Library.UnequalLengths =>
12.29 - raise CTYPE ("NitpickMono.do_ctype_comp", [C1, C2]))
12.30 + raise CTYPE ("Nitpick_Mono.do_ctype_comp", [C1, C2]))
12.31 | do_ctype_comp cmp xs (CType _) (CType _) accum =
12.32 accum (* no need to compare them thanks to the cache *)
12.33 | do_ctype_comp _ _ C1 C2 _ =
12.34 - raise CTYPE ("NitpickMono.do_ctype_comp", [C1, C2])
12.35 + raise CTYPE ("Nitpick_Mono.do_ctype_comp", [C1, C2])
12.36
12.37 (* comp_op -> ctype -> ctype -> constraint_set -> constraint_set *)
12.38 fun add_ctype_comp _ _ _ UnsolvableCSet = UnsolvableCSet
12.39 @@ -413,7 +413,7 @@
12.40 | do_notin_ctype_fv sn sexp (CType (_, Cs)) accum =
12.41 accum |> fold (do_notin_ctype_fv sn sexp) Cs
12.42 | do_notin_ctype_fv _ _ C _ =
12.43 - raise CTYPE ("NitpickMono.do_notin_ctype_fv", [C])
12.44 + raise CTYPE ("Nitpick_Mono.do_notin_ctype_fv", [C])
12.45
12.46 (* sign -> ctype -> constraint_set -> constraint_set *)
12.47 fun add_notin_ctype_fv _ _ UnsolvableCSet = UnsolvableCSet
12.48 @@ -584,13 +584,13 @@
12.49 case ctype_for (nth_range_type 2 T) of
12.50 C as CPair (a_C, b_C) =>
12.51 (CFun (a_C, S Neg, CFun (b_C, S Neg, C)), accum)
12.52 - | C => raise CTYPE ("NitpickMono.consider_term.do_pair_constr", [C])
12.53 + | C => raise CTYPE ("Nitpick_Mono.consider_term.do_pair_constr", [C])
12.54 (* int -> typ -> accumulator -> ctype * accumulator *)
12.55 fun do_nth_pair_sel n T =
12.56 case ctype_for (domain_type T) of
12.57 C as CPair (a_C, b_C) =>
12.58 pair (CFun (C, S Neg, if n = 0 then a_C else b_C))
12.59 - | C => raise CTYPE ("NitpickMono.consider_term.do_nth_pair_sel", [C])
12.60 + | C => raise CTYPE ("Nitpick_Mono.consider_term.do_nth_pair_sel", [C])
12.61 val unsolvable = (CType ("unsolvable", []), unsolvable_accum)
12.62 (* typ -> term -> accumulator -> ctype * accumulator *)
12.63 fun do_bounded_quantifier abs_T bound_t body_t accum =
12.64 @@ -770,7 +770,7 @@
12.65 | _ => case C1 of
12.66 CFun (C11, _, C12) =>
12.67 (C12, accum ||> add_is_sub_ctype C2 C11)
12.68 - | _ => raise CTYPE ("NitpickMono.consider_term.do_term \
12.69 + | _ => raise CTYPE ("Nitpick_Mono.consider_term.do_term \
12.70 \(op $)", [C1])
12.71 end)
12.72 |> tap (fn (C, _) =>
12.73 @@ -906,7 +906,7 @@
12.74 | Const (@{const_name "op ="}, _) $ t1 $ t2 => do_equals t1 t2 accum
12.75 | @{const "op &"} $ t1 $ t2 => accum |> do_formula t1 |> do_formula t2
12.76 | @{const "op -->"} $ t1 $ t2 => do_implies t1 t2 accum
12.77 - | _ => raise TERM ("NitpickMono.consider_definitional_axiom.\
12.78 + | _ => raise TERM ("Nitpick_Mono.consider_definitional_axiom.\
12.79 \do_formula", [t])
12.80 in do_formula t end
12.81
13.1 --- a/src/HOL/Tools/Nitpick/nitpick_nut.ML Tue Oct 27 12:16:26 2009 +0100
13.2 +++ b/src/HOL/Tools/Nitpick/nitpick_nut.ML Tue Oct 27 14:40:24 2009 +0100
13.3 @@ -7,11 +7,11 @@
13.4
13.5 signature NITPICK_NUT =
13.6 sig
13.7 - type special_fun = NitpickHOL.special_fun
13.8 - type extended_context = NitpickHOL.extended_context
13.9 - type scope = NitpickScope.scope
13.10 - type name_pool = NitpickPeephole.name_pool
13.11 - type rep = NitpickRep.rep
13.12 + type special_fun = Nitpick_HOL.special_fun
13.13 + type extended_context = Nitpick_HOL.extended_context
13.14 + type scope = Nitpick_Scope.scope
13.15 + type name_pool = Nitpick_Peephole.name_pool
13.16 + type rep = Nitpick_Rep.rep
13.17
13.18 datatype cst =
13.19 Unity |
13.20 @@ -121,14 +121,14 @@
13.21 val rename_vars_in_nut : name_pool -> nut NameTable.table -> nut -> nut
13.22 end;
13.23
13.24 -structure NitpickNut : NITPICK_NUT =
13.25 +structure Nitpick_Nut : NITPICK_NUT =
13.26 struct
13.27
13.28 -open NitpickUtil
13.29 -open NitpickHOL
13.30 -open NitpickScope
13.31 -open NitpickPeephole
13.32 -open NitpickRep
13.33 +open Nitpick_Util
13.34 +open Nitpick_HOL
13.35 +open Nitpick_Scope
13.36 +open Nitpick_Peephole
13.37 +open Nitpick_Rep
13.38
13.39 datatype cst =
13.40 Unity |
13.41 @@ -357,16 +357,16 @@
13.42 | nickname_of (ConstName (s, _, _)) = s
13.43 | nickname_of (BoundRel (_, _, _, nick)) = nick
13.44 | nickname_of (FreeRel (_, _, _, nick)) = nick
13.45 - | nickname_of u = raise NUT ("NitpickNut.nickname_of", [u])
13.46 + | nickname_of u = raise NUT ("Nitpick_Nut.nickname_of", [u])
13.47
13.48 (* nut -> bool *)
13.49 fun is_skolem_name u =
13.50 space_explode name_sep (nickname_of u)
13.51 |> exists (String.isPrefix skolem_prefix)
13.52 - handle NUT ("NitpickNut.nickname_of", _) => false
13.53 + handle NUT ("Nitpick_Nut.nickname_of", _) => false
13.54 fun is_eval_name u =
13.55 String.isPrefix eval_prefix (nickname_of u)
13.56 - handle NUT ("NitpickNut.nickname_of", _) => false
13.57 + handle NUT ("Nitpick_Nut.nickname_of", _) => false
13.58 (* cst -> nut -> bool *)
13.59 fun is_Cst cst (Cst (cst', _, _)) = (cst = cst')
13.60 | is_Cst _ _ = false
13.61 @@ -407,7 +407,7 @@
13.62 (case fast_string_ord (s1, s2) of
13.63 EQUAL => TermOrd.typ_ord (T1, T2)
13.64 | ord => ord)
13.65 - | name_ord (u1, u2) = raise NUT ("NitpickNut.name_ord", [u1, u2])
13.66 + | name_ord (u1, u2) = raise NUT ("Nitpick_Nut.name_ord", [u1, u2])
13.67
13.68 (* nut -> nut -> int *)
13.69 fun num_occs_in_nut needle_u stack_u =
13.70 @@ -430,7 +430,7 @@
13.71 fun modify_name_rep (BoundName (j, T, _, nick)) R = BoundName (j, T, R, nick)
13.72 | modify_name_rep (FreeName (s, T, _)) R = FreeName (s, T, R)
13.73 | modify_name_rep (ConstName (s, T, _)) R = ConstName (s, T, R)
13.74 - | modify_name_rep u _ = raise NUT ("NitpickNut.modify_name_rep", [u])
13.75 + | modify_name_rep u _ = raise NUT ("Nitpick_Nut.modify_name_rep", [u])
13.76
13.77 structure NameTable = Table(type key = nut val ord = name_ord)
13.78
13.79 @@ -438,12 +438,12 @@
13.80 fun the_name table name =
13.81 case NameTable.lookup table name of
13.82 SOME u => u
13.83 - | NONE => raise NUT ("NitpickNut.the_name", [name])
13.84 + | NONE => raise NUT ("Nitpick_Nut.the_name", [name])
13.85 (* nut NameTable.table -> nut -> Kodkod.n_ary_index *)
13.86 fun the_rel table name =
13.87 case the_name table name of
13.88 FreeRel (x, _, _, _) => x
13.89 - | u => raise NUT ("NitpickNut.the_rel", [u])
13.90 + | u => raise NUT ("Nitpick_Nut.the_rel", [u])
13.91
13.92 (* typ * term -> typ * term *)
13.93 fun mk_fst (_, Const (@{const_name Pair}, T) $ t1 $ _) = (domain_type T, t1)
13.94 @@ -669,13 +669,13 @@
13.95 (case arity_of_built_in_const fast_descrs x of
13.96 SOME n =>
13.97 (case n - length ts of
13.98 - 0 => raise TERM ("NitpickNut.nut_from_term.aux", [t])
13.99 + 0 => raise TERM ("Nitpick_Nut.nut_from_term.aux", [t])
13.100 | k => if k > 0 then sub (eta_expand Ts t k)
13.101 else do_apply t0 ts)
13.102 | NONE => if null ts then ConstName (s, T, Any)
13.103 else do_apply t0 ts)
13.104 | (Free (s, T), []) => FreeName (s, T, Any)
13.105 - | (Var _, []) => raise TERM ("NitpickNut.nut_from_term", [t])
13.106 + | (Var _, []) => raise TERM ("Nitpick_Nut.nut_from_term", [t])
13.107 | (Bound j, []) =>
13.108 BoundName (length Ts - j - 1, nth Ts j, Any, nth ss j)
13.109 | (Abs (s, T, t1), []) =>
13.110 @@ -1106,7 +1106,7 @@
13.111 else
13.112 unopt_rep R
13.113 in s_op2 Lambda T R u1' u2' end
13.114 - | R => raise NUT ("NitpickNut.aux.choose_reps_in_nut", [u]))
13.115 + | R => raise NUT ("Nitpick_Nut.aux.choose_reps_in_nut", [u]))
13.116 | Op2 (oper, T, _, u1, u2) =>
13.117 if oper mem [All, Exist] then
13.118 let
13.119 @@ -1274,9 +1274,9 @@
13.120 | shape_tuple (T as Type ("fun", [_, T2])) (R as Vect (k, R')) us =
13.121 Tuple (T, R, map (shape_tuple T2 R') (batch_list (length us div k) us))
13.122 | shape_tuple T R [u] =
13.123 - if type_of u = T then u else raise NUT ("NitpickNut.shape_tuple", [u])
13.124 + if type_of u = T then u else raise NUT ("Nitpick_Nut.shape_tuple", [u])
13.125 | shape_tuple T Unit [] = Cst (Unity, T, Unit)
13.126 - | shape_tuple _ _ us = raise NUT ("NitpickNut.shape_tuple", us)
13.127 + | shape_tuple _ _ us = raise NUT ("Nitpick_Nut.shape_tuple", us)
13.128
13.129 (* bool -> nut -> nut list * name_pool * nut NameTable.table
13.130 -> nut list * name_pool * nut NameTable.table *)
14.1 --- a/src/HOL/Tools/Nitpick/nitpick_peephole.ML Tue Oct 27 12:16:26 2009 +0100
14.2 +++ b/src/HOL/Tools/Nitpick/nitpick_peephole.ML Tue Oct 27 14:40:24 2009 +0100
14.3 @@ -86,11 +86,11 @@
14.4 val kodkod_constrs : bool -> int -> int -> int -> kodkod_constrs
14.5 end;
14.6
14.7 -structure NitpickPeephole : NITPICK_PEEPHOLE =
14.8 +structure Nitpick_Peephole : NITPICK_PEEPHOLE =
14.9 struct
14.10
14.11 open Kodkod
14.12 -open NitpickUtil
14.13 +open Nitpick_Util
14.14
14.15 type name_pool = {
14.16 rels: n_ary_index list,
14.17 @@ -188,20 +188,20 @@
14.18 if is_none_product r1 orelse is_none_product r2 then SOME false else NONE
14.19
14.20 (* int -> rel_expr *)
14.21 -fun empty_n_ary_rel 0 = raise ARG ("NitpickPeephole.empty_n_ary_rel", "0")
14.22 +fun empty_n_ary_rel 0 = raise ARG ("Nitpick_Peephole.empty_n_ary_rel", "0")
14.23 | empty_n_ary_rel n = funpow (n - 1) (curry Product None) None
14.24
14.25 (* decl -> rel_expr *)
14.26 fun decl_one_set (DeclOne (_, r)) = r
14.27 | decl_one_set _ =
14.28 - raise ARG ("NitpickPeephole.decl_one_set", "not \"DeclOne\"")
14.29 + raise ARG ("Nitpick_Peephole.decl_one_set", "not \"DeclOne\"")
14.30
14.31 (* int_expr -> bool *)
14.32 fun is_Num (Num _) = true
14.33 | is_Num _ = false
14.34 (* int_expr -> int *)
14.35 fun dest_Num (Num k) = k
14.36 - | dest_Num _ = raise ARG ("NitpickPeephole.dest_Num", "not \"Num\"")
14.37 + | dest_Num _ = raise ARG ("Nitpick_Peephole.dest_Num", "not \"Num\"")
14.38 (* int -> int -> int_expr list *)
14.39 fun num_seq j0 n = map Num (index_seq j0 n)
14.40
15.1 --- a/src/HOL/Tools/Nitpick/nitpick_rep.ML Tue Oct 27 12:16:26 2009 +0100
15.2 +++ b/src/HOL/Tools/Nitpick/nitpick_rep.ML Tue Oct 27 14:40:24 2009 +0100
15.3 @@ -7,8 +7,8 @@
15.4
15.5 signature NITPICK_REP =
15.6 sig
15.7 - type polarity = NitpickUtil.polarity
15.8 - type scope = NitpickScope.scope
15.9 + type polarity = Nitpick_Util.polarity
15.10 + type scope = Nitpick_Scope.scope
15.11
15.12 datatype rep =
15.13 Any |
15.14 @@ -58,12 +58,12 @@
15.15 val all_combinations_for_reps : rep list -> int list list
15.16 end;
15.17
15.18 -structure NitpickRep : NITPICK_REP =
15.19 +structure Nitpick_Rep : NITPICK_REP =
15.20 struct
15.21
15.22 -open NitpickUtil
15.23 -open NitpickHOL
15.24 -open NitpickScope
15.25 +open Nitpick_Util
15.26 +open Nitpick_HOL
15.27 +open Nitpick_Scope
15.28
15.29 datatype rep =
15.30 Any |
15.31 @@ -111,7 +111,7 @@
15.32 | is_opt_rep _ = false
15.33
15.34 (* rep -> int *)
15.35 -fun card_of_rep Any = raise REP ("NitpickRep.card_of_rep", [Any])
15.36 +fun card_of_rep Any = raise REP ("Nitpick_Rep.card_of_rep", [Any])
15.37 | card_of_rep (Formula _) = 2
15.38 | card_of_rep Unit = 1
15.39 | card_of_rep (Atom (k, _)) = k
15.40 @@ -120,7 +120,7 @@
15.41 | card_of_rep (Func (R1, R2)) =
15.42 reasonable_power (card_of_rep R2) (card_of_rep R1)
15.43 | card_of_rep (Opt R) = card_of_rep R
15.44 -fun arity_of_rep Any = raise REP ("NitpickRep.arity_of_rep", [Any])
15.45 +fun arity_of_rep Any = raise REP ("Nitpick_Rep.arity_of_rep", [Any])
15.46 | arity_of_rep (Formula _) = 0
15.47 | arity_of_rep Unit = 0
15.48 | arity_of_rep (Atom _) = 1
15.49 @@ -129,7 +129,7 @@
15.50 | arity_of_rep (Func (R1, R2)) = arity_of_rep R1 + arity_of_rep R2
15.51 | arity_of_rep (Opt R) = arity_of_rep R
15.52 fun min_univ_card_of_rep Any =
15.53 - raise REP ("NitpickRep.min_univ_card_of_rep", [Any])
15.54 + raise REP ("Nitpick_Rep.min_univ_card_of_rep", [Any])
15.55 | min_univ_card_of_rep (Formula _) = 0
15.56 | min_univ_card_of_rep Unit = 0
15.57 | min_univ_card_of_rep (Atom (k, j0)) = k + j0 + 1
15.58 @@ -151,7 +151,7 @@
15.59
15.60 (* rep -> rep * rep *)
15.61 fun dest_Func (Func z) = z
15.62 - | dest_Func R = raise REP ("NitpickRep.dest_Func", [R])
15.63 + | dest_Func R = raise REP ("Nitpick_Rep.dest_Func", [R])
15.64 (* int Typtab.table -> typ -> (unit -> int) -> rep -> rep *)
15.65 fun smart_range_rep _ _ _ Unit = Unit
15.66 | smart_range_rep _ _ _ (Vect (_, R)) = R
15.67 @@ -162,7 +162,7 @@
15.68 Atom (1, offset_of_type ofs T2)
15.69 | smart_range_rep ofs (Type ("fun", [_, T2])) ran_card (Atom _) =
15.70 Atom (ran_card (), offset_of_type ofs T2)
15.71 - | smart_range_rep _ _ _ R = raise REP ("NitpickRep.smart_range_rep", [R])
15.72 + | smart_range_rep _ _ _ R = raise REP ("Nitpick_Rep.smart_range_rep", [R])
15.73
15.74 (* rep -> rep list *)
15.75 fun binder_reps (Func (R1, R2)) = R1 :: binder_reps R2
15.76 @@ -177,7 +177,7 @@
15.77 | flip_rep_polarity R = R
15.78
15.79 (* int Typtab.table -> rep -> rep *)
15.80 -fun one_rep _ _ Any = raise REP ("NitpickRep.one_rep", [Any])
15.81 +fun one_rep _ _ Any = raise REP ("Nitpick_Rep.one_rep", [Any])
15.82 | one_rep _ _ (Atom x) = Atom x
15.83 | one_rep _ _ (Struct Rs) = Struct Rs
15.84 | one_rep _ _ (Vect z) = Vect z
15.85 @@ -203,7 +203,7 @@
15.86 else if polar2 = Neut then
15.87 polar1
15.88 else
15.89 - raise ARG ("NitpickRep.min_polarity",
15.90 + raise ARG ("Nitpick_Rep.min_polarity",
15.91 commas (map (quote o string_for_polarity) [polar1, polar2]))
15.92
15.93 (* It's important that Func is before Vect, because if the range is Opt we
15.94 @@ -236,7 +236,7 @@
15.95 if k1 < k2 then Vect (k1, R1)
15.96 else if k1 > k2 then Vect (k2, R2)
15.97 else Vect (k1, min_rep R1 R2)
15.98 - | min_rep R1 R2 = raise REP ("NitpickRep.min_rep", [R1, R2])
15.99 + | min_rep R1 R2 = raise REP ("Nitpick_Rep.min_rep", [R1, R2])
15.100 (* rep list -> rep list -> rep list *)
15.101 and min_reps [] _ = []
15.102 | min_reps _ [] = []
15.103 @@ -253,7 +253,7 @@
15.104 | Vect (k, _) => k
15.105 | Func (R1, _) => card_of_rep R1
15.106 | Opt R => card_of_domain_from_rep ran_card R
15.107 - | _ => raise REP ("NitpickRep.card_of_domain_from_rep", [R])
15.108 + | _ => raise REP ("Nitpick_Rep.card_of_domain_from_rep", [R])
15.109
15.110 (* int Typtab.table -> typ -> rep -> rep *)
15.111 fun rep_to_binary_rel_rep ofs T R =
15.112 @@ -306,10 +306,10 @@
15.113 (optable_rep ofs T1 (best_one_rep_for_type scope T1),
15.114 optable_rep ofs T2 (best_one_rep_for_type scope T2))
15.115 | best_non_opt_symmetric_reps_for_fun_type _ T =
15.116 - raise TYPE ("NitpickRep.best_non_opt_symmetric_reps_for_fun_type", [T], [])
15.117 + raise TYPE ("Nitpick_Rep.best_non_opt_symmetric_reps_for_fun_type", [T], [])
15.118
15.119 (* rep -> (int * int) list *)
15.120 -fun atom_schema_of_rep Any = raise REP ("NitpickRep.atom_schema_of_rep", [Any])
15.121 +fun atom_schema_of_rep Any = raise REP ("Nitpick_Rep.atom_schema_of_rep", [Any])
15.122 | atom_schema_of_rep (Formula _) = []
15.123 | atom_schema_of_rep Unit = []
15.124 | atom_schema_of_rep (Atom x) = [x]
15.125 @@ -332,7 +332,7 @@
15.126 | type_schema_of_rep (Type ("fun", [T1, T2])) (Func (R1, R2)) =
15.127 type_schema_of_rep T1 R1 @ type_schema_of_rep T2 R2
15.128 | type_schema_of_rep T (Opt R) = type_schema_of_rep T R
15.129 - | type_schema_of_rep T R = raise REP ("NitpickRep.type_schema_of_rep", [R])
15.130 + | type_schema_of_rep T R = raise REP ("Nitpick_Rep.type_schema_of_rep", [R])
15.131 (* typ list -> rep list -> typ list *)
15.132 and type_schema_of_reps Ts Rs = flat (map2 type_schema_of_rep Ts Rs)
15.133
16.1 --- a/src/HOL/Tools/Nitpick/nitpick_scope.ML Tue Oct 27 12:16:26 2009 +0100
16.2 +++ b/src/HOL/Tools/Nitpick/nitpick_scope.ML Tue Oct 27 14:40:24 2009 +0100
16.3 @@ -7,7 +7,7 @@
16.4
16.5 signature NITPICK_SCOPE =
16.6 sig
16.7 - type extended_context = NitpickHOL.extended_context
16.8 + type extended_context = Nitpick_HOL.extended_context
16.9
16.10 type constr_spec = {
16.11 const: styp,
16.12 @@ -47,11 +47,11 @@
16.13 -> int list -> typ list -> typ list -> scope list
16.14 end;
16.15
16.16 -structure NitpickScope : NITPICK_SCOPE =
16.17 +structure Nitpick_Scope : NITPICK_SCOPE =
16.18 struct
16.19
16.20 -open NitpickUtil
16.21 -open NitpickHOL
16.22 +open Nitpick_Util
16.23 +open Nitpick_HOL
16.24
16.25 type constr_spec = {
16.26 const: styp,
16.27 @@ -85,7 +85,7 @@
16.28 List.find (equal T o #typ) dtypes
16.29
16.30 (* dtype_spec list -> styp -> constr_spec *)
16.31 -fun constr_spec [] x = raise TERM ("NitpickScope.constr_spec", [Const x])
16.32 +fun constr_spec [] x = raise TERM ("Nitpick_Scope.constr_spec", [Const x])
16.33 | constr_spec ({constrs, ...} :: dtypes : dtype_spec list) (x as (s, T)) =
16.34 case List.find (equal (s, body_type T) o (apsnd body_type o #const))
16.35 constrs of
16.36 @@ -115,7 +115,7 @@
16.37 (* scope -> typ -> int * int *)
16.38 fun spec_of_type ({card_assigns, ofs, ...} : scope) T =
16.39 (card_of_type card_assigns T
16.40 - handle TYPE ("NitpickHOL.card_of_type", _, _) => ~1, offset_of_type ofs T)
16.41 + handle TYPE ("Nitpick_HOL.card_of_type", _, _) => ~1, offset_of_type ofs T)
16.42
16.43 (* (string -> string) -> scope
16.44 -> string list * string list * string list * string list * string list *)
16.45 @@ -205,17 +205,17 @@
16.46 fun lookup_ints_assign eq asgns key =
16.47 case triple_lookup eq asgns key of
16.48 SOME ks => ks
16.49 - | NONE => raise ARG ("NitpickScope.lookup_ints_assign", "")
16.50 + | NONE => raise ARG ("Nitpick_Scope.lookup_ints_assign", "")
16.51 (* theory -> (typ option * int list) list -> typ -> int list *)
16.52 fun lookup_type_ints_assign thy asgns T =
16.53 map (curry Int.max 1) (lookup_ints_assign (type_match thy) asgns T)
16.54 - handle ARG ("NitpickScope.lookup_ints_assign", _) =>
16.55 - raise TYPE ("NitpickScope.lookup_type_ints_assign", [T], [])
16.56 + handle ARG ("Nitpick_Scope.lookup_ints_assign", _) =>
16.57 + raise TYPE ("Nitpick_Scope.lookup_type_ints_assign", [T], [])
16.58 (* theory -> (styp option * int list) list -> styp -> int list *)
16.59 fun lookup_const_ints_assign thy asgns x =
16.60 lookup_ints_assign (const_match thy) asgns x
16.61 - handle ARG ("NitpickScope.lookup_ints_assign", _) =>
16.62 - raise TERM ("NitpickScope.lookup_const_ints_assign", [Const x])
16.63 + handle ARG ("Nitpick_Scope.lookup_ints_assign", _) =>
16.64 + raise TERM ("Nitpick_Scope.lookup_const_ints_assign", [Const x])
16.65
16.66 (* theory -> (styp option * int list) list -> styp -> row option *)
16.67 fun row_for_constr thy maxes_asgns constr =
16.68 @@ -315,7 +315,7 @@
16.69 max < k
16.70 orelse (forall (not_equal 0) precise_cards andalso doms_card () < k)
16.71 end
16.72 - handle TYPE ("NitpickHOL.card_of_type", _, _) => false
16.73 + handle TYPE ("Nitpick_HOL.card_of_type", _, _) => false
16.74
16.75 (* theory -> scope_desc -> bool *)
16.76 fun is_surely_inconsistent_scope_description thy (desc as (card_asgns, _)) =
17.1 --- a/src/HOL/Tools/Nitpick/nitpick_tests.ML Tue Oct 27 12:16:26 2009 +0100
17.2 +++ b/src/HOL/Tools/Nitpick/nitpick_tests.ML Tue Oct 27 14:40:24 2009 +0100
17.3 @@ -10,15 +10,14 @@
17.4 val run_all_tests : unit -> unit
17.5 end
17.6
17.7 -structure NitpickTests =
17.8 +structure Nitpick_Tests =
17.9 struct
17.10
17.11 -open NitpickUtil
17.12 -open NitpickPeephole
17.13 -open NitpickRep
17.14 -open NitpickNut
17.15 -open NitpickKodkod
17.16 -open Nitpick
17.17 +open Nitpick_Util
17.18 +open Nitpick_Peephole
17.19 +open Nitpick_Rep
17.20 +open Nitpick_Nut
17.21 +open Nitpick_Kodkod
17.22
17.23 val settings =
17.24 [("solver", "\"zChaff\""),
18.1 --- a/src/HOL/Tools/Nitpick/nitpick_util.ML Tue Oct 27 12:16:26 2009 +0100
18.2 +++ b/src/HOL/Tools/Nitpick/nitpick_util.ML Tue Oct 27 14:40:24 2009 +0100
18.3 @@ -72,7 +72,7 @@
18.4 val maybe_quote : string -> string
18.5 end
18.6
18.7 -structure NitpickUtil : NITPICK_UTIL =
18.8 +structure Nitpick_Util : NITPICK_UTIL =
18.9 struct
18.10
18.11 type styp = string * typ
18.12 @@ -107,7 +107,7 @@
18.13 | reasonable_power 1 _ = 1
18.14 | reasonable_power a b =
18.15 if b < 0 orelse b > max_exponent then
18.16 - raise LIMIT ("NitpickUtil.reasonable_power",
18.17 + raise LIMIT ("Nitpick_Util.reasonable_power",
18.18 "too large exponent (" ^ signed_string_of_int b ^ ")")
18.19 else
18.20 let
18.21 @@ -123,7 +123,7 @@
18.22 if reasonable_power m r = n then
18.23 r
18.24 else
18.25 - raise ARG ("NitpickUtil.exact_log",
18.26 + raise ARG ("Nitpick_Util.exact_log",
18.27 commas (map signed_string_of_int [m, n]))
18.28 end
18.29
18.30 @@ -133,7 +133,7 @@
18.31 if reasonable_power r m = n then
18.32 r
18.33 else
18.34 - raise ARG ("NitpickUtil.exact_root",
18.35 + raise ARG ("Nitpick_Util.exact_root",
18.36 commas (map signed_string_of_int [m, n]))
18.37 end
18.38
18.39 @@ -156,7 +156,7 @@
18.40 fun aux _ [] _ = []
18.41 | aux i (j :: js) (x :: xs) =
18.42 if i = j then x :: aux (i + 1) js xs else aux (i + 1) (j :: js) xs
18.43 - | aux _ _ _ = raise ARG ("NitpickUtil.filter_indices",
18.44 + | aux _ _ _ = raise ARG ("Nitpick_Util.filter_indices",
18.45 "indices unordered or out of range")
18.46 in aux 0 js xs end
18.47 fun filter_out_indices js xs =
18.48 @@ -165,7 +165,7 @@
18.49 fun aux _ [] xs = xs
18.50 | aux i (j :: js) (x :: xs) =
18.51 if i = j then aux (i + 1) js xs else x :: aux (i + 1) (j :: js) xs
18.52 - | aux _ _ _ = raise ARG ("NitpickUtil.filter_out_indices",
18.53 + | aux _ _ _ = raise ARG ("Nitpick_Util.filter_out_indices",
18.54 "indices unordered or out of range")
18.55 in aux 0 js xs end
18.56
18.57 @@ -303,5 +303,5 @@
18.58
18.59 end;
18.60
18.61 -structure BasicNitpickUtil : BASIC_NITPICK_UTIL = NitpickUtil;
18.62 -open BasicNitpickUtil;
18.63 +structure Basic_Nitpick_Util : BASIC_NITPICK_UTIL = Nitpick_Util;
18.64 +open Basic_Nitpick_Util;