# HG changeset patch # User blanchet # Date 1256650824 -3600 # Node ID f93390060bbe0a3209828bcffdfcbeed16a6986c # Parent 1711610c5b7d7020d2dbbe836ba9f3c01063061f internal renaming in Nitpick and fixed Kodkodi invokation on Linux; renamed Nitpick's ML structures from NitpickXxx to Nitpick_Xxx and added KODKODI_JAVA_LIBRARY_PATH to LD_LIBRARY_PATH before invoking Kodkodi diff -r 1711610c5b7d -r f93390060bbe doc-src/Nitpick/nitpick.tex --- a/doc-src/Nitpick/nitpick.tex Tue Oct 27 12:16:26 2009 +0100 +++ b/doc-src/Nitpick/nitpick.tex Tue Oct 27 14:40:24 2009 +0100 @@ -2381,7 +2381,7 @@ (``genuine'', ``likely\_genuine'', ``potential'', ``none'', or ``unknown''). The \textit{params} type is a large record that lets you set Nitpick's options. The current default options can be retrieved by calling the following function -defined in the \textit{NitpickIsar} structure: +defined in the \textit{Nitpick\_Isar} structure: \prew $\textbf{val}\,~\textit{default\_params} :\, @@ -2392,7 +2392,7 @@ put into a \textit{params} record. Here is an example: \prew -$\textbf{val}\,~\textit{params} = \textit{NitpickIsar.default\_params}~\textit{thy}~[(\textrm{``}\textrm{timeout}\textrm{''},\, \textrm{``}\textrm{none}\textrm{''})]$ \\ +$\textbf{val}\,~\textit{params} = \textit{Nitpick\_Isar.default\_params}~\textit{thy}~[(\textrm{``}\textrm{timeout}\textrm{''},\, \textrm{``}\textrm{none}\textrm{''})]$ \\ $\textbf{val}\,~(\textit{outcome},\, \textit{state}') = \textit{Nitpick.pick\_nits\_in\_subgoal}~\begin{aligned}[t] & \textit{state}~\textit{params}~\textit{false} \\[-2pt] & \textit{subgoal}\end{aligned}$ diff -r 1711610c5b7d -r f93390060bbe src/HOL/Nitpick_Examples/Mono_Nits.thy --- a/src/HOL/Nitpick_Examples/Mono_Nits.thy Tue Oct 27 12:16:26 2009 +0100 +++ b/src/HOL/Nitpick_Examples/Mono_Nits.thy Tue Oct 27 14:40:24 2009 +0100 @@ -14,8 +14,8 @@ ML {* exception FAIL -val defs = NitpickHOL.all_axioms_of @{theory} |> #1 -val def_table = NitpickHOL.const_def_table @{context} defs +val defs = Nitpick_HOL.all_axioms_of @{theory} |> #1 +val def_table = Nitpick_HOL.const_def_table @{context} defs val ext_ctxt = {thy = @{theory}, ctxt = @{context}, max_bisim_depth = ~1, boxes = [], user_axioms = NONE, debug = false, wfs = [], destroy_constrs = false, diff -r 1711610c5b7d -r f93390060bbe src/HOL/Nitpick_Examples/Tests_Nits.thy --- a/src/HOL/Nitpick_Examples/Tests_Nits.thy Tue Oct 27 12:16:26 2009 +0100 +++ b/src/HOL/Nitpick_Examples/Tests_Nits.thy Tue Oct 27 14:40:24 2009 +0100 @@ -11,6 +11,6 @@ imports Main begin -ML {* NitpickTests.run_all_tests () *} +ML {* Nitpick_Tests.run_all_tests () *} end diff -r 1711610c5b7d -r f93390060bbe src/HOL/Tools/Nitpick/kodkod.ML --- a/src/HOL/Tools/Nitpick/kodkod.ML Tue Oct 27 12:16:26 2009 +0100 +++ b/src/HOL/Tools/Nitpick/kodkod.ML Tue Oct 27 14:40:24 2009 +0100 @@ -1044,7 +1044,10 @@ val code = system ("env CLASSPATH=\"$KODKODI_CLASSPATH:$CLASSPATH\" \ \JAVA_LIBRARY_PATH=\"$KODKODI_JAVA_LIBRARY_PATH:\ - \$JAVA_LIBRARY_PATH\" \"$ISABELLE_TOOL\" java \ + \$JAVA_LIBRARY_PATH\" \ + \LD_LIBRARY_PATH=\"$KODKODI_JAVA_LIBRARY_PATH:\ + \$LD_LIBRARY_PATH\" \ + \\"$ISABELLE_TOOL\" java \ \de.tum.in.isabelle.Kodkodi.Kodkodi" ^ (if ms >= 0 then " -max-msecs " ^ Int.toString ms else "") ^ diff -r 1711610c5b7d -r f93390060bbe src/HOL/Tools/Nitpick/kodkod_sat.ML --- a/src/HOL/Tools/Nitpick/kodkod_sat.ML Tue Oct 27 12:16:26 2009 +0100 +++ b/src/HOL/Tools/Nitpick/kodkod_sat.ML Tue Oct 27 14:40:24 2009 +0100 @@ -12,7 +12,7 @@ val sat_solver_spec : string -> string * string list end; -structure KodkodSAT : KODKOD_SAT = +structure Kodkod_SAT : KODKOD_SAT = struct datatype sink = ToStdout | ToFile diff -r 1711610c5b7d -r f93390060bbe src/HOL/Tools/Nitpick/minipick.ML --- a/src/HOL/Tools/Nitpick/minipick.ML Tue Oct 27 12:16:26 2009 +0100 +++ b/src/HOL/Tools/Nitpick/minipick.ML Tue Oct 27 14:40:24 2009 +0100 @@ -14,10 +14,10 @@ struct open Kodkod -open NitpickUtil -open NitpickHOL -open NitpickPeephole -open NitpickKodkod +open Nitpick_Util +open Nitpick_HOL +open Nitpick_Peephole +open Nitpick_Kodkod (* theory -> typ -> unit *) fun check_type ctxt (Type ("fun", Ts)) = List.app (check_type ctxt) Ts diff -r 1711610c5b7d -r f93390060bbe src/HOL/Tools/Nitpick/nitpick.ML --- a/src/HOL/Tools/Nitpick/nitpick.ML Tue Oct 27 12:16:26 2009 +0100 +++ b/src/HOL/Tools/Nitpick/nitpick.ML Tue Oct 27 14:40:24 2009 +0100 @@ -62,15 +62,15 @@ structure Nitpick : NITPICK = struct -open NitpickUtil -open NitpickHOL -open NitpickMono -open NitpickScope -open NitpickPeephole -open NitpickRep -open NitpickNut -open NitpickKodkod -open NitpickModel +open Nitpick_Util +open Nitpick_HOL +open Nitpick_Mono +open Nitpick_Scope +open Nitpick_Peephole +open Nitpick_Rep +open Nitpick_Nut +open Nitpick_Kodkod +open Nitpick_Model type params = { cards_assigns: (typ option * int list) list, @@ -355,21 +355,21 @@ val effective_sat_solver = if sat_solver <> "smart" then if need_incremental andalso - not (sat_solver mem KodkodSAT.configured_sat_solvers true) then + not (sat_solver mem Kodkod_SAT.configured_sat_solvers true) then (print_m (K ("An incremental SAT solver is required: \"SAT4J\" will \ \be used instead of " ^ quote sat_solver ^ ".")); "SAT4J") else sat_solver else - KodkodSAT.smart_sat_solver_name need_incremental + Kodkod_SAT.smart_sat_solver_name need_incremental val _ = if sat_solver = "smart" then print_v (fn () => "Using SAT solver " ^ quote effective_sat_solver ^ ". The following" ^ (if need_incremental then " incremental " else " ") ^ "solvers are configured: " ^ - commas (map quote (KodkodSAT.configured_sat_solvers + commas (map quote (Kodkod_SAT.configured_sat_solvers need_incremental)) ^ ".") else () @@ -439,7 +439,7 @@ val formula = fold (fold s_and) [def_fs, nondef_fs] core_f val comment = (if liberal then "liberal" else "conservative") ^ "\n" ^ PrintMode.setmp [] multiline_string_for_scope scope - val kodkod_sat_solver = KodkodSAT.sat_solver_spec effective_sat_solver + val kodkod_sat_solver = Kodkod_SAT.sat_solver_spec effective_sat_solver |> snd val delay = if liberal then Option.map (fn time => Time.- (time, Time.now ())) @@ -483,7 +483,7 @@ defs = nondef_fs @ def_fs @ declarative_axioms}) end handle LIMIT (loc, msg) => - if loc = "NitpickKodkod.check_arity" + if loc = "Nitpick_Kodkod.check_arity" andalso not (Typtab.is_empty ofs) then problem_for_scope liberal {ext_ctxt = ext_ctxt, card_assigns = card_assigns, diff -r 1711610c5b7d -r f93390060bbe src/HOL/Tools/Nitpick/nitpick_hol.ML --- a/src/HOL/Tools/Nitpick/nitpick_hol.ML Tue Oct 27 12:16:26 2009 +0100 +++ b/src/HOL/Tools/Nitpick/nitpick_hol.ML Tue Oct 27 14:40:24 2009 +0100 @@ -139,10 +139,10 @@ extended_context -> term -> ((term list * term list) * (bool * bool)) * term end; -structure NitpickHOL : NITPICK_HOL = +structure Nitpick_HOL : NITPICK_HOL = struct -open NitpickUtil +open Nitpick_Util type const_table = term list Symtab.table type special_fun = (styp * int list * term list) * styp @@ -263,7 +263,7 @@ val after_name_sep = snd o strip_first_name_sep (* When you add constants to these lists, make sure to handle them in - "NitpickNut.nut_from_term", and perhaps in "NitpickMono.consider_term" as + "Nitpick_Nut.nut_from_term", and perhaps in "Nitpick_Mono.consider_term" as well. *) val built_in_consts = [(@{const_name all}, 1), @@ -405,7 +405,7 @@ (* typ -> styp *) fun const_for_iterator_type (Type (s, Ts)) = (after_name_sep s, Ts ---> bool_T) | const_for_iterator_type T = - raise TYPE ("NitpickHOL.const_for_iterator_type", [T], []) + raise TYPE ("Nitpick_HOL.const_for_iterator_type", [T], []) (* int -> typ -> typ * typ *) fun strip_n_binders 0 T = ([], T) @@ -413,7 +413,7 @@ strip_n_binders (n - 1) T2 |>> cons T1 | strip_n_binders n (Type (@{type_name fun_box}, Ts)) = strip_n_binders n (Type ("fun", Ts)) - | strip_n_binders _ T = raise TYPE ("NitpickHOL.strip_n_binders", [T], []) + | strip_n_binders _ T = raise TYPE ("Nitpick_HOL.strip_n_binders", [T], []) (* typ -> typ *) val nth_range_type = snd oo strip_n_binders @@ -432,7 +432,7 @@ fun mk_flat_tuple _ [t] = t | mk_flat_tuple (Type ("*", [T1, T2])) (t :: ts) = HOLogic.pair_const T1 T2 $ t $ (mk_flat_tuple T2 ts) - | mk_flat_tuple T ts = raise TYPE ("NitpickHOL.mk_flat_tuple", [T], ts) + | mk_flat_tuple T ts = raise TYPE ("Nitpick_HOL.mk_flat_tuple", [T], ts) (* int -> term -> term list *) fun dest_n_tuple 1 t = [t] | dest_n_tuple n t = HOLogic.dest_prod t ||> dest_n_tuple (n - 1) |> op :: @@ -441,7 +441,8 @@ fun dest_n_tuple_type 1 T = [T] | dest_n_tuple_type n (Type (_, [T1, T2])) = T1 :: dest_n_tuple_type (n - 1) T2 - | dest_n_tuple_type _ T = raise TYPE ("NitpickHOL.dest_n_tuple_type", [T], []) + | dest_n_tuple_type _ T = + raise TYPE ("Nitpick_HOL.dest_n_tuple_type", [T], []) (* (typ * typ) list -> typ -> typ *) fun typ_subst [] T = T @@ -460,7 +461,7 @@ (Sign.typ_match thy (Logic.varifyT T1, T1') Vartab.empty)) (Logic.varifyT T2) handle Type.TYPE_MATCH => - raise TYPE ("NitpickHOL.instantiate_type", [T1, T1'], []) + raise TYPE ("Nitpick_HOL.instantiate_type", [T1, T1'], []) (* theory -> typ -> typ -> styp *) fun repair_constr_type thy body_T' T = @@ -483,7 +484,7 @@ val (co_s, co_Ts) = dest_Type co_T val _ = if forall is_TFree co_Ts andalso not (has_duplicates (op =) co_Ts) then () - else raise TYPE ("NitpickHOL.register_codatatype", [co_T], []) + else raise TYPE ("Nitpick_HOL.register_codatatype", [co_T], []) val codatatypes = AList.update (op =) (co_s, (case_name, constr_xs)) codatatypes in TheoryData.put {frac_types = frac_types, codatatypes = codatatypes} thy end @@ -586,8 +587,8 @@ fun mate_of_rep_fun thy (x as (_, Type ("fun", [T1 as Type (s', _), T2]))) = (case typedef_info thy s' of SOME {Abs_name, ...} => (Abs_name, Type ("fun", [T2, T1])) - | NONE => raise TERM ("NitpickHOL.mate_of_rep_fun", [Const x])) - | mate_of_rep_fun _ x = raise TERM ("NitpickHOL.mate_of_rep_fun", [Const x]) + | NONE => raise TERM ("Nitpick_HOL.mate_of_rep_fun", [Const x])) + | mate_of_rep_fun _ x = raise TERM ("Nitpick_HOL.mate_of_rep_fun", [Const x]) (* theory -> styp -> bool *) fun is_coconstr thy (s, T) = @@ -874,7 +875,7 @@ case AList.lookup (op =) asgns T of SOME k => k | NONE => if T = @{typ bisim_iterator} then 0 - else raise TYPE ("NitpickHOL.card_of_type", [T], []) + else raise TYPE ("Nitpick_HOL.card_of_type", [T], []) (* int -> (typ * int) list -> typ -> int *) fun bounded_card_of_type max default_card asgns (Type ("fun", [T1, T2])) = let @@ -894,7 +895,7 @@ card_of_type asgns T else card_of_type asgns T - handle TYPE ("NitpickHOL.card_of_type", _, _) => + handle TYPE ("Nitpick_HOL.card_of_type", _, _) => default_card) (* theory -> int -> (typ * int) list -> typ -> int *) fun bounded_precise_card_of_type thy max default_card asgns T = @@ -1110,13 +1111,13 @@ (* term -> term *) fun aux (v as Var _) t = lambda v t | aux (c as Const (@{const_name TYPE}, T)) t = lambda c t - | aux _ _ = raise TERM ("NitpickHOL.normalized_rhs_of", [t]) + | aux _ _ = raise TERM ("Nitpick_HOL.normalized_rhs_of", [t]) val (lhs, rhs) = case t of Const (@{const_name "=="}, _) $ t1 $ t2 => (t1, t2) | @{const Trueprop} $ (Const (@{const_name "op ="}, _) $ t1 $ t2) => (t1, t2) - | _ => raise TERM ("NitpickHOL.normalized_rhs_of", [t]) + | _ => raise TERM ("Nitpick_HOL.normalized_rhs_of", [t]) val args = strip_comb lhs |> snd in fold_rev aux args rhs end @@ -1170,7 +1171,7 @@ case term_under_def t of Const (s, _) => (s, t) | Free _ => raise NOT_SUPPORTED "local definitions" - | t' => raise TERM ("NitpickHOL.pair_for_prop", [t, t']) + | t' => raise TERM ("Nitpick_HOL.pair_for_prop", [t, t']) (* (Proof.context -> term list) -> Proof.context -> const_table *) fun table_for get ctxt = @@ -1308,7 +1309,7 @@ |> fold_rev (curry absdummy) (func_Ts @ [dataT]) end -val redefined_in_NitpickDefs_thy = +val redefined_in_Nitpick_thy = [@{const_name option_case}, @{const_name nat_case}, @{const_name list_case}, @{const_name list_size}] @@ -1325,7 +1326,8 @@ select_nth_constr_arg thy constr_x t j res_T |> optimized_record_get thy s rec_T' res_T end - | _ => raise TYPE ("NitpickHOL.optimized_record_get", [rec_T], [])) + | _ => raise TYPE ("Nitpick_HOL.optimized_record_get", [rec_T], + [])) | j => select_nth_constr_arg thy constr_x t j res_T end (* theory -> string -> typ -> term -> term -> term *) @@ -1380,7 +1382,7 @@ (is_real_equational_fun ext_ctxt orf is_real_inductive_pred ext_ctxt orf (String.isPrefix ubfp_prefix orf String.isPrefix lbfp_prefix) o fst) andf (not o has_trivial_definition thy def_table) - andf (not o member (op =) redefined_in_NitpickDefs_thy o fst) + andf (not o member (op =) redefined_in_Nitpick_thy o fst) (* term * term -> term *) fun s_betapply (Const (@{const_name If}, _) $ @{const True} $ t, _) = t @@ -1532,7 +1534,7 @@ else case def_of_const thy def_table x of SOME def => if depth > unfold_max_depth then - raise LIMIT ("NitpickHOL.unfold_defs_in_term", + raise LIMIT ("Nitpick_HOL.unfold_defs_in_term", "too many nested definitions (" ^ string_of_int depth ^ ") while expanding " ^ quote s) @@ -1640,7 +1642,8 @@ ({thy, ctxt, debug, fast_descrs, tac_timeout, intro_table, ...} : extended_context) (x as (_, T)) = case def_props_for_const thy fast_descrs intro_table x of - [] => raise TERM ("NitpickHOL.is_is_well_founded_inductive_pred", [Const x]) + [] => raise TERM ("Nitpick_HOL.is_is_well_founded_inductive_pred", + [Const x]) | intro_ts => (case map (triple_for_intro_rule thy x) intro_ts |> filter_out (null o #2) of @@ -1772,7 +1775,7 @@ |> ap_split tuple_T bool_T)) end | aux t = - raise TERM ("NitpickHOL.linear_pred_base_and_step_rhss.aux", [t]) + raise TERM ("Nitpick_HOL.linear_pred_base_and_step_rhss.aux", [t]) in aux end (* extended_context -> styp -> term -> term *) @@ -1834,8 +1837,8 @@ val rhs = case fp_app of Const _ $ t => betapply (t, list_comb (Const x', next :: outer_bounds)) - | _ => raise TERM ("NitpickHOL.unrolled_inductive_pred_const", - [fp_app]) + | _ => raise TERM ("Nitpick_HOL.unrolled_inductive_pred_\ + \const", [fp_app]) val (inner, naked_rhs) = strip_abs rhs val all = outer @ inner val bounds = map Bound (length all - 1 downto 0) @@ -1854,7 +1857,7 @@ val outer_bounds = map Bound (length outer - 1 downto 0) val rhs = case fp_app of Const _ $ t => betapply (t, list_comb (Const x, outer_bounds)) - | _ => raise TERM ("NitpickHOL.raw_inductive_pred_axiom", + | _ => raise TERM ("Nitpick_HOL.raw_inductive_pred_axiom", [fp_app]) val (inner, naked_rhs) = strip_abs rhs val all = outer @ inner @@ -1876,7 +1879,7 @@ (* extended_context -> styp -> term list *) fun raw_equational_fun_axioms (ext_ctxt as {thy, fast_descrs, simp_table, psimp_table, ...}) (x as (s, _)) = - if s mem redefined_in_NitpickDefs_thy then + if s mem redefined_in_Nitpick_thy then [] else case def_props_for_const thy fast_descrs (!simp_table) x of [] => (case def_props_for_const thy fast_descrs psimp_table x of @@ -2329,7 +2332,7 @@ ts (* (term * int list) list -> term *) fun mk_connection [] = - raise ARG ("NitpickHOL.push_quantifiers_inward.aux.\ + raise ARG ("Nitpick_HOL.push_quantifiers_inward.aux.\ \mk_connection", "") | mk_connection ts_cum_bounds = ts_cum_bounds |> map fst @@ -2720,7 +2723,7 @@ |> new_s <> "fun" ? construct_value thy (@{const_name FunBox}, Type ("fun", new_Ts) --> new_T) o single - | t' => raise TERM ("NitpickHOL.box_fun_and_pair_in_term.\ + | t' => raise TERM ("Nitpick_HOL.box_fun_and_pair_in_term.\ \coerce_term", [t'])) | (Type (new_s, new_Ts as [new_T1, new_T2]), Type (old_s, old_Ts as [old_T1, old_T2])) => @@ -2740,7 +2743,7 @@ else @{const_name PairBox}, new_Ts ---> new_T) [coerce_term Ts new_T1 old_T1 t1, coerce_term Ts new_T2 old_T2 t2] - | t' => raise TERM ("NitpickHOL.box_fun_and_pair_in_term.\ + | t' => raise TERM ("Nitpick_HOL.box_fun_and_pair_in_term.\ \coerce_term", [t']) else raise TYPE ("coerce_term", [new_T, old_T], [t]) @@ -2753,7 +2756,7 @@ (case T' of Type (_, [T1, T2]) => fold (add_boxed_types_for_var z) [(T1, t1), (T2, t2)] - | _ => raise TYPE ("NitpickHOL.box_fun_and_pair_in_term.\ + | _ => raise TYPE ("Nitpick_HOL.box_fun_and_pair_in_term.\ \add_boxed_types_for_var", [T'], [])) | _ => exists_subterm (equal (Var z)) t' ? insert (op =) T (* typ list -> typ list -> term -> indexname * typ -> typ *) @@ -3008,7 +3011,7 @@ else let val accum as (xs, _) = (x :: xs, axs) in if depth > axioms_max_depth then - raise LIMIT ("NitpickHOL.axioms_for_term.add_axioms_for_term", + raise LIMIT ("Nitpick_HOL.axioms_for_term.add_axioms_for_term", "too many nested axioms (" ^ string_of_int depth ^ ")") else if Refute.is_const_of_class thy x then @@ -3081,7 +3084,7 @@ [] => t | [(x, S)] => Refute.monomorphic_term (Vartab.make [(x, (S, T))]) t - | _ => raise TERM ("NitpickHOL.axioms_for_term.\ + | _ => raise TERM ("Nitpick_HOL.axioms_for_term.\ \add_axioms_for_sort", [t])) class_axioms in fold (add_nondef_axiom depth) monomorphic_class_axioms end diff -r 1711610c5b7d -r f93390060bbe src/HOL/Tools/Nitpick/nitpick_isar.ML --- a/src/HOL/Tools/Nitpick/nitpick_isar.ML Tue Oct 27 12:16:26 2009 +0100 +++ b/src/HOL/Tools/Nitpick/nitpick_isar.ML Tue Oct 27 14:40:24 2009 +0100 @@ -13,13 +13,13 @@ val default_params : theory -> (string * string) list -> params end -structure NitpickIsar : NITPICK_ISAR = +structure Nitpick_Isar : NITPICK_ISAR = struct -open NitpickUtil -open NitpickHOL -open NitpickRep -open NitpickNut +open Nitpick_Util +open Nitpick_HOL +open Nitpick_Rep +open Nitpick_Nut open Nitpick type raw_param = string * string list diff -r 1711610c5b7d -r f93390060bbe src/HOL/Tools/Nitpick/nitpick_kodkod.ML --- a/src/HOL/Tools/Nitpick/nitpick_kodkod.ML Tue Oct 27 12:16:26 2009 +0100 +++ b/src/HOL/Tools/Nitpick/nitpick_kodkod.ML Tue Oct 27 14:40:24 2009 +0100 @@ -7,10 +7,10 @@ signature NITPICK_KODKOD = sig - type extended_context = NitpickHOL.extended_context - type dtype_spec = NitpickScope.dtype_spec - type kodkod_constrs = NitpickPeephole.kodkod_constrs - type nut = NitpickNut.nut + type extended_context = Nitpick_HOL.extended_context + type dtype_spec = Nitpick_Scope.dtype_spec + type kodkod_constrs = Nitpick_Peephole.kodkod_constrs + type nut = Nitpick_Nut.nut type nfa_transition = Kodkod.rel_expr * typ type nfa_entry = typ * nfa_transition list type nfa_table = nfa_entry list @@ -37,15 +37,15 @@ int Typtab.table -> bool -> kodkod_constrs -> nut -> Kodkod.formula end; -structure NitpickKodkod : NITPICK_KODKOD = +structure Nitpick_Kodkod : NITPICK_KODKOD = struct -open NitpickUtil -open NitpickHOL -open NitpickScope -open NitpickPeephole -open NitpickRep -open NitpickNut +open Nitpick_Util +open Nitpick_HOL +open Nitpick_Scope +open Nitpick_Peephole +open Nitpick_Rep +open Nitpick_Nut type nfa_transition = Kodkod.rel_expr * typ type nfa_entry = typ * nfa_transition list @@ -89,7 +89,7 @@ (* int -> int -> unit *) fun check_arity univ_card n = if n > Kodkod.max_arity univ_card then - raise LIMIT ("NitpickKodkod.check_arity", + raise LIMIT ("Nitpick_Kodkod.check_arity", "arity " ^ string_of_int n ^ " too large for universe of \ \cardinality " ^ string_of_int univ_card) else @@ -132,7 +132,7 @@ (* int -> unit *) fun check_table_size k = if k > max_table_size then - raise LIMIT ("NitpickKodkod.check_table_size", + raise LIMIT ("Nitpick_Kodkod.check_table_size", "precomputed table too large (" ^ string_of_int k ^ ")") else () @@ -245,7 +245,7 @@ ("norm_frac", tabulate_int_op2_2 debug univ_card (int_card, j0) isa_norm_frac) else - raise ARG ("NitpickKodkod.tabulate_built_in_rel", "unknown relation")) + raise ARG ("Nitpick_Kodkod.tabulate_built_in_rel", "unknown relation")) (* bool -> int -> int -> int -> int -> int * int -> Kodkod.rel_expr -> Kodkod.bound *) @@ -266,11 +266,11 @@ if nick = @{const_name bisim_iterator_max} then case R of Atom (k, j0) => [Kodkod.TupleSet [Kodkod.Tuple [k - 1 + j0]]] - | _ => raise NUT ("NitpickKodkod.bound_for_plain_rel", [u]) + | _ => raise NUT ("Nitpick_Kodkod.bound_for_plain_rel", [u]) else [Kodkod.TupleSet [], upper_bound_for_rep R]) | bound_for_plain_rel _ _ u = - raise NUT ("NitpickKodkod.bound_for_plain_rel", [u]) + raise NUT ("Nitpick_Kodkod.bound_for_plain_rel", [u]) (* Proof.context -> bool -> dtype_spec list -> nut -> Kodkod.bound *) fun bound_for_sel_rel ctxt debug dtypes @@ -293,7 +293,7 @@ end) end | bound_for_sel_rel _ _ _ u = - raise NUT ("NitpickKodkod.bound_for_sel_rel", [u]) + raise NUT ("Nitpick_Kodkod.bound_for_sel_rel", [u]) (* Kodkod.bound list -> Kodkod.bound list *) fun merge_bounds bs = @@ -320,7 +320,7 @@ if is_lone_rep R then all_combinations_for_rep R |> map singleton_from_combination else - raise REP ("NitpickKodkod.all_singletons_for_rep", [R]) + raise REP ("Nitpick_Kodkod.all_singletons_for_rep", [R]) (* Kodkod.rel_expr -> Kodkod.rel_expr list *) fun unpack_products (Kodkod.Product (r1, r2)) = @@ -333,7 +333,7 @@ val empty_rel_for_rep = empty_n_ary_rel o arity_of_rep fun full_rel_for_rep R = case atom_schema_of_rep R of - [] => raise REP ("NitpickKodkod.full_rel_for_rep", [R]) + [] => raise REP ("Nitpick_Kodkod.full_rel_for_rep", [R]) | schema => foldl1 Kodkod.Product (map Kodkod.AtomSeq schema) (* int -> int list -> Kodkod.decl list *) @@ -424,7 +424,7 @@ fun rel_expr_from_formula kk R f = case unopt_rep R of Atom (2, j0) => atom_from_formula kk j0 f - | _ => raise REP ("NitpickKodkod.rel_expr_from_formula", [R]) + | _ => raise REP ("Nitpick_Kodkod.rel_expr_from_formula", [R]) (* kodkod_cotrs -> int -> int -> Kodkod.rel_expr -> Kodkod.rel_expr list *) fun unpack_vect_in_chunks ({kk_project_seq, ...} : kodkod_constrs) chunk_arity @@ -471,13 +471,13 @@ if is_lone_rep old_R andalso is_lone_rep new_R andalso card = card_of_rep new_R then if card >= lone_rep_fallback_max_card then - raise LIMIT ("NitpickKodkod.lone_rep_fallback", + raise LIMIT ("Nitpick_Kodkod.lone_rep_fallback", "too high cardinality (" ^ string_of_int card ^ ")") else kk_case_switch kk old_R new_R r (all_singletons_for_rep old_R) (all_singletons_for_rep new_R) else - raise REP ("NitpickKodkod.lone_rep_fallback", [old_R, new_R]) + raise REP ("Nitpick_Kodkod.lone_rep_fallback", [old_R, new_R]) end (* kodkod_constrs -> int * int -> rep -> Kodkod.rel_expr -> Kodkod.rel_expr *) and atom_from_rel_expr kk (x as (k, j0)) old_R r = @@ -490,7 +490,7 @@ atom_from_rel_expr kk x (Vect (dom_card, R2')) (vect_from_rel_expr kk dom_card R2' old_R r) end - | Opt _ => raise REP ("NitpickKodkod.atom_from_rel_expr", [old_R]) + | Opt _ => raise REP ("Nitpick_Kodkod.atom_from_rel_expr", [old_R]) | _ => lone_rep_fallback kk (Atom x) old_R r (* kodkod_constrs -> rep list -> rep -> Kodkod.rel_expr -> Kodkod.rel_expr *) and struct_from_rel_expr kk Rs old_R r = @@ -515,7 +515,7 @@ else lone_rep_fallback kk (Struct Rs) old_R r end - | _ => raise REP ("NitpickKodkod.struct_from_rel_expr", [old_R]) + | _ => raise REP ("Nitpick_Kodkod.struct_from_rel_expr", [old_R]) (* kodkod_constrs -> int -> rep -> rep -> Kodkod.rel_expr -> Kodkod.rel_expr *) and vect_from_rel_expr kk k R old_R r = case old_R of @@ -530,7 +530,7 @@ rel_expr_from_formula kk R (#kk_subset kk arg_r r)) (all_singletons_for_rep R1)) else - raise REP ("NitpickKodkod.vect_from_rel_expr", [old_R]) + raise REP ("Nitpick_Kodkod.vect_from_rel_expr", [old_R]) | Func (Unit, R2) => rel_expr_from_rel_expr kk R R2 r | Func (R1, R2) => fold1 (#kk_product kk) @@ -538,7 +538,7 @@ rel_expr_from_rel_expr kk R R2 (kk_n_fold_join kk true R1 R2 arg_r r)) (all_singletons_for_rep R1)) - | _ => raise REP ("NitpickKodkod.vect_from_rel_expr", [old_R]) + | _ => raise REP ("Nitpick_Kodkod.vect_from_rel_expr", [old_R]) (* kodkod_constrs -> rep -> rep -> rep -> Kodkod.rel_expr -> Kodkod.rel_expr *) and func_from_no_opt_rel_expr kk R1 R2 (Atom x) r = let @@ -555,12 +555,12 @@ | Func (Atom (1, _), Formula Neut) => (case unopt_rep R2 of Atom (2, j0) => atom_from_formula kk j0 (#kk_some kk r) - | _ => raise REP ("NitpickKodkod.func_from_no_opt_rel_expr", + | _ => raise REP ("Nitpick_Kodkod.func_from_no_opt_rel_expr", [old_R, Func (Unit, R2)])) | Func (R1', R2') => rel_expr_from_rel_expr kk R2 R2' (#kk_project_seq kk r (arity_of_rep R1') (arity_of_rep R2')) - | _ => raise REP ("NitpickKodkod.func_from_no_opt_rel_expr", + | _ => raise REP ("Nitpick_Kodkod.func_from_no_opt_rel_expr", [old_R, Func (Unit, R2)])) | func_from_no_opt_rel_expr kk R1 (Formula Neut) old_R r = (case old_R of @@ -592,7 +592,7 @@ | Func (R1', Atom (2, j0)) => func_from_no_opt_rel_expr kk R1 (Formula Neut) (Func (R1', Formula Neut)) (#kk_join kk r (Kodkod.Atom (j0 + 1))) - | _ => raise REP ("NitpickKodkod.func_from_no_opt_rel_expr", + | _ => raise REP ("Nitpick_Kodkod.func_from_no_opt_rel_expr", [old_R, Func (R1, Formula Neut)])) | func_from_no_opt_rel_expr kk R1 R2 old_R r = case old_R of @@ -621,7 +621,7 @@ (#kk_rel_eq kk r2 r3) end end - | _ => raise REP ("NitpickKodkod.func_from_no_opt_rel_expr", + | _ => raise REP ("Nitpick_Kodkod.func_from_no_opt_rel_expr", [old_R, Func (R1, R2)])) | Func (Unit, R2') => let val j0 = some_j0 in @@ -648,7 +648,7 @@ (dom_schema @ ran_schema)) (#kk_subset kk ran_prod app) end - | _ => raise REP ("NitpickKodkod.func_from_no_opt_rel_expr", + | _ => raise REP ("Nitpick_Kodkod.func_from_no_opt_rel_expr", [old_R, Func (R1, R2)]) (* kodkod_constrs -> rep -> rep -> Kodkod.rel_expr -> Kodkod.rel_expr *) and rel_expr_from_rel_expr kk new_R old_R r = @@ -657,7 +657,7 @@ val unopt_new_R = unopt_rep new_R in if unopt_old_R <> old_R andalso unopt_new_R = new_R then - raise REP ("NitpickKodkod.rel_expr_from_rel_expr", [old_R, new_R]) + raise REP ("Nitpick_Kodkod.rel_expr_from_rel_expr", [old_R, new_R]) else if unopt_new_R = unopt_old_R then r else @@ -666,7 +666,7 @@ | Struct Rs => struct_from_rel_expr kk Rs | Vect (k, R') => vect_from_rel_expr kk k R' | Func (R1, R2) => func_from_no_opt_rel_expr kk R1 R2 - | _ => raise REP ("NitpickKodkod.rel_expr_from_rel_expr", + | _ => raise REP ("Nitpick_Kodkod.rel_expr_from_rel_expr", [old_R, new_R])) unopt_old_R r end @@ -683,13 +683,13 @@ else if is_lone_rep R andalso card_of_rep R > 1 then kk_lone (Kodkod.Rel x) else Kodkod.True | declarative_axiom_for_plain_rel _ u = - raise NUT ("NitpickKodkod.declarative_axiom_for_plain_rel", [u]) + raise NUT ("Nitpick_Kodkod.declarative_axiom_for_plain_rel", [u]) (* nut NameTable.table -> styp -> Kodkod.rel_expr * rep * int *) fun const_triple rel_table (x as (s, T)) = case the_name rel_table (ConstName (s, T, Any)) of FreeRel ((n, j), _, R, _) => (Kodkod.Rel (n, j), R, n) - | _ => raise TERM ("NitpickKodkod.const_triple", [Const x]) + | _ => raise TERM ("Nitpick_Kodkod.const_triple", [Const x]) (* nut NameTable.table -> styp -> Kodkod.rel_expr *) fun discr_rel_expr rel_table = #1 o const_triple rel_table o discr_for_constr @@ -849,7 +849,8 @@ (~1 upto num_sels - 1) val j0 = case triples |> hd |> #2 of Func (Atom (_, j0), _) => j0 - | R => raise REP ("NitpickKodkod.uniqueness_axiom_for_constr", [R]) + | R => raise REP ("Nitpick_Kodkod.uniqueness_axiom_for_constr", + [R]) val set_r = triples |> hd |> #1 in if num_sels = 0 then @@ -960,7 +961,7 @@ let val opt1 = is_opt_rep (rep_of u1) in case polar of Neut => if opt1 then - raise NUT ("NitpickKodkod.to_f (Finite)", [u]) + raise NUT ("Nitpick_Kodkod.to_f (Finite)", [u]) else Kodkod.True | Pos => formula_for_bool (not opt1) @@ -992,7 +993,7 @@ if not (is_opt_rep ran_R) then to_set_bool_op kk_implies kk_subset u1 u2 else if polar = Neut then - raise NUT ("NitpickKodkod.to_f (Subset)", [u]) + raise NUT ("Nitpick_Kodkod.to_f (Subset)", [u]) else let (* bool -> nut -> Kodkod.rel_expr *) @@ -1102,16 +1103,16 @@ | Op3 (If, _, _, u1, u2, u3) => kk_formula_if (to_f u1) (to_f u2) (to_f u3) | FormulaReg (j, _, _) => Kodkod.FormulaReg j - | _ => raise NUT ("NitpickKodkod.to_f", [u])) + | _ => raise NUT ("Nitpick_Kodkod.to_f", [u])) | Atom (2, j0) => formula_from_atom j0 (to_r u) - | _ => raise NUT ("NitpickKodkod.to_f", [u]) + | _ => raise NUT ("Nitpick_Kodkod.to_f", [u]) (* polarity -> nut -> Kodkod.formula *) and to_f_with_polarity polar u = case rep_of u of Formula _ => to_f u | Atom (2, j0) => formula_from_atom j0 (to_r u) | Opt (Atom (2, j0)) => formula_from_opt_atom polar j0 (to_r u) - | _ => raise NUT ("NitpickKodkod.to_f_with_polarity", [u]) + | _ => raise NUT ("Nitpick_Kodkod.to_f_with_polarity", [u]) (* nut -> Kodkod.rel_expr *) and to_r u = case u of @@ -1142,12 +1143,12 @@ | Cst (Num j, @{typ int}, R) => (case atom_for_int (card_of_rep R, offset_of_type ofs int_T) j of ~1 => if is_opt_rep R then Kodkod.None - else raise NUT ("NitpickKodkod.to_r (Num)", [u]) + else raise NUT ("Nitpick_Kodkod.to_r (Num)", [u]) | j' => Kodkod.Atom j') | Cst (Num j, T, R) => if j < card_of_rep R then Kodkod.Atom (j + offset_of_type ofs T) else if is_opt_rep R then Kodkod.None - else raise NUT ("NitpickKodkod.to_r", [u]) + else raise NUT ("Nitpick_Kodkod.to_r", [u]) | Cst (Unknown, _, R) => empty_rel_for_rep R | Cst (Unrep, _, R) => empty_rel_for_rep R | Cst (Suc, T, Func (Atom x, _)) => @@ -1177,7 +1178,7 @@ (kk_product (Kodkod.AtomSeq (max_int_for_card int_k + 1, nat_j0)) Kodkod.Univ) else - raise BAD ("NitpickKodkod.to_r (NatToInt)", "\"nat_j0 <> int_j0\"") + raise BAD ("Nitpick_Kodkod.to_r (NatToInt)", "\"nat_j0 <> int_j0\"") | Cst (IntToNat, _, Func (Atom (int_k, int_j0), nat_R)) => let val abs_card = max_int_for_card int_k + 1 @@ -1192,7 +1193,7 @@ (kk_product (Kodkod.AtomSeq (overlap, int_j0)) Kodkod.Univ)) else - raise BAD ("NitpickKodkod.to_r (IntToNat)", "\"nat_j0 <> int_j0\"") + raise BAD ("Nitpick_Kodkod.to_r (IntToNat)", "\"nat_j0 <> int_j0\"") end | Op1 (Not, _, R, u1) => kk_not3 (to_rep R u1) | Op1 (Finite, _, Opt (Atom _), _) => Kodkod.None @@ -1204,10 +1205,10 @@ Func (Struct [R1, R2], _) => (R1, R2) | Func (R1, _) => if card_of_rep R1 <> 1 then - raise REP ("NitpickKodkod.to_r (Converse)", [R]) + raise REP ("Nitpick_Kodkod.to_r (Converse)", [R]) else pairself (Atom o pair 1 o offset_of_type ofs) (b_T, a_T) - | _ => raise REP ("NitpickKodkod.to_r (Converse)", [R]) + | _ => raise REP ("Nitpick_Kodkod.to_r (Converse)", [R]) val body_R = body_rep R val a_arity = arity_of_rep a_R val b_arity = arity_of_rep b_R @@ -1257,7 +1258,7 @@ (rel_expr_to_func kk R1 bool_atom_R (Func (R1, Formula Neut)) r)) (to_opt R1 u1) - | _ => raise NUT ("NitpickKodkod.to_r (SingletonSet)", [u])) + | _ => raise NUT ("Nitpick_Kodkod.to_r (SingletonSet)", [u])) | Op1 (Tha, T, R, u1) => if is_opt_rep R then kk_join (to_rep (Func (unopt_rep R, Opt bool_atom_R)) u1) true_atom @@ -1384,7 +1385,7 @@ kk_product (kk_join (do_nut r a_R b_R u2) (do_nut r b_R c_R u1)) r in kk_union (do_term true_atom) (do_term false_atom) end - | _ => raise NUT ("NitpickKodkod.to_r (Composition)", [u])) + | _ => raise NUT ("Nitpick_Kodkod.to_r (Composition)", [u])) |> rel_expr_from_rel_expr kk R (Func (Struct [a_R, c_R], body_R)) end | Op2 (Product, T, R, u1, u2) => @@ -1408,7 +1409,7 @@ fun do_term r = kk_product (kk_product (do_nut r a_R u1) (do_nut r b_R u2)) r in kk_union (do_term true_atom) (do_term false_atom) end - | _ => raise NUT ("NitpickKodkod.to_r (Product)", [u])) + | _ => raise NUT ("Nitpick_Kodkod.to_r (Product)", [u])) |> rel_expr_from_rel_expr kk R (Func (Struct [a_R, b_R], body_R)) end | Op2 (Image, T, R, u1, u2) => @@ -1437,8 +1438,8 @@ rel_expr_from_rel_expr kk R core_R core_r end else - raise NUT ("NitpickKodkod.to_r (Image)", [u1, u2]) - | _ => raise NUT ("NitpickKodkod.to_r (Image)", [u1, u2])) + raise NUT ("Nitpick_Kodkod.to_r (Image)", [u1, u2]) + | _ => raise NUT ("Nitpick_Kodkod.to_r (Image)", [u1, u2])) | Op2 (Apply, @{typ nat}, _, Op2 (Apply, _, _, Cst (Subtract, _, _), u1), u2) => if is_Cst Unrep u2 andalso not (is_opt_rep (rep_of u1)) then @@ -1492,7 +1493,7 @@ | us' => kk_rel_if (kk_some (fold1 kk_product (map to_r us'))) (Kodkod.Atom j0) Kodkod.None) - | _ => raise NUT ("NitpickKodkod.to_r (Tuple)", [u])) + | _ => raise NUT ("Nitpick_Kodkod.to_r (Tuple)", [u])) | Construct ([u'], _, _, []) => to_r u' | Construct (_ :: sel_us, T, R, arg_us) => let @@ -1516,23 +1517,23 @@ | BoundRel (x, _, _, _) => Kodkod.Var x | FreeRel (x, _, _, _) => Kodkod.Rel x | RelReg (j, _, R) => Kodkod.RelReg (arity_of_rep R, j) - | u => raise NUT ("NitpickKodkod.to_r", [u]) + | u => raise NUT ("Nitpick_Kodkod.to_r", [u]) (* nut -> Kodkod.decl *) and to_decl (BoundRel (x, _, R, _)) = Kodkod.DeclOne (x, Kodkod.AtomSeq (the_single (atom_schema_of_rep R))) - | to_decl u = raise NUT ("NitpickKodkod.to_decl", [u]) + | to_decl u = raise NUT ("Nitpick_Kodkod.to_decl", [u]) (* nut -> Kodkod.expr_assign *) and to_expr_assign (FormulaReg (j, _, R)) u = Kodkod.AssignFormulaReg (j, to_f u) | to_expr_assign (RelReg (j, _, R)) u = Kodkod.AssignRelReg ((arity_of_rep R, j), to_r u) - | to_expr_assign u1 _ = raise NUT ("NitpickKodkod.to_expr_assign", [u1]) + | to_expr_assign u1 _ = raise NUT ("Nitpick_Kodkod.to_expr_assign", [u1]) (* int * int -> nut -> Kodkod.rel_expr *) and to_atom (x as (k, j0)) u = case rep_of u of Formula _ => atom_from_formula kk j0 (to_f u) | Unit => if k = 1 then Kodkod.Atom j0 - else raise NUT ("NitpickKodkod.to_atom", [u]) + else raise NUT ("Nitpick_Kodkod.to_atom", [u]) | R => atom_from_rel_expr kk x R (to_r u) (* rep list -> nut -> Kodkod.rel_expr *) and to_struct Rs u = @@ -1563,7 +1564,7 @@ | to_rep (Vect (k, R)) u = to_vect k R u | to_rep (Func (R1, R2)) u = to_func R1 R2 u | to_rep (Opt R) u = to_opt R u - | to_rep R _ = raise REP ("NitpickKodkod.to_rep", [R]) + | to_rep R _ = raise REP ("Nitpick_Kodkod.to_rep", [R]) (* nut -> Kodkod.rel_expr *) and to_integer u = to_opt (one_rep ofs (type_of u) (rep_of u)) u (* nut list -> rep -> Kodkod.rel_expr -> Kodkod.rel_expr *) @@ -1593,7 +1594,7 @@ (* rep list -> nut list -> Kodkod.rel_expr *) and to_product Rs us = case map (uncurry to_opt) (filter (not_equal Unit o fst) (Rs ~~ us)) of - [] => raise REP ("NitpickKodkod.to_product", Rs) + [] => raise REP ("Nitpick_Kodkod.to_product", Rs) | rs => fold1 kk_product rs (* int -> typ -> rep -> nut -> Kodkod.rel_expr *) and to_nth_pair_sel n res_T res_R u = @@ -1639,7 +1640,7 @@ connective (formula_from_atom j0 r1) (formula_from_atom j0 r2) | Func (R1, Atom _) => set_oper (kk_join r1 true_atom) (kk_join r2 true_atom) - | _ => raise REP ("NitpickKodkod.to_set_bool_op", [min_R]) + | _ => raise REP ("Nitpick_Kodkod.to_set_bool_op", [min_R]) end (* (Kodkod.formula -> Kodkod.formula -> Kodkod.formula) -> (Kodkod.rel_expr -> Kodkod.rel_expr -> Kodkod.rel_expr) @@ -1676,7 +1677,7 @@ neg_second))) false_atom)) r1 r2 - | _ => raise REP ("NitpickKodkod.to_set_op", [min_R])) + | _ => raise REP ("Nitpick_Kodkod.to_set_op", [min_R])) end (* rep -> rep -> Kodkod.rel_expr -> nut -> Kodkod.rel_expr *) and to_apply res_R func_u arg_u = @@ -1713,7 +1714,7 @@ rel_expr_from_rel_expr kk res_R R2 (kk_n_fold_join kk true R1 R2 (to_opt R1 arg_u) (to_r func_u)) |> body_rep R2 = Formula Neut ? to_guard [arg_u] res_R - | _ => raise NUT ("NitpickKodkod.to_apply", [func_u]) + | _ => raise NUT ("Nitpick_Kodkod.to_apply", [func_u]) (* int -> rep -> rep -> Kodkod.rel_expr -> nut *) and to_apply_vect k R' res_R func_r arg_u = let diff -r 1711610c5b7d -r f93390060bbe src/HOL/Tools/Nitpick/nitpick_model.ML --- a/src/HOL/Tools/Nitpick/nitpick_model.ML Tue Oct 27 12:16:26 2009 +0100 +++ b/src/HOL/Tools/Nitpick/nitpick_model.ML Tue Oct 27 14:40:24 2009 +0100 @@ -7,9 +7,9 @@ signature NITPICK_MODEL = sig - type scope = NitpickScope.scope - type rep = NitpickRep.rep - type nut = NitpickNut.nut + type scope = Nitpick_Scope.scope + type rep = Nitpick_Rep.rep + type nut = Nitpick_Nut.nut type params = { show_skolems: bool, @@ -29,15 +29,15 @@ -> Kodkod.raw_bound list -> term -> bool option end; -structure NitpickModel : NITPICK_MODEL = +structure Nitpick_Model : NITPICK_MODEL = struct -open NitpickUtil -open NitpickHOL -open NitpickScope -open NitpickPeephole -open NitpickRep -open NitpickNut +open Nitpick_Util +open Nitpick_HOL +open Nitpick_Scope +open Nitpick_Peephole +open Nitpick_Rep +open Nitpick_Nut type params = { show_skolems: bool, @@ -57,7 +57,7 @@ prefix ^ substring (short_name s, 0, 1) ^ nat_subscript (j + 1) | atom_name prefix (T as TFree (s, _)) j = prefix ^ perhaps (try (unprefix "'")) s ^ nat_subscript (j + 1) - | atom_name _ T _ = raise TYPE ("NitpickModel.atom_name", [T], []) + | atom_name _ T _ = raise TYPE ("Nitpick_Model.atom_name", [T], []) (* bool -> typ -> int -> term *) fun atom for_auto T j = if for_auto then @@ -130,7 +130,7 @@ fun aux (Const (s, _)) = (s <> non_opt_name, ([], [])) | aux (Const (@{const_name fun_upd}, _) $ t0 $ t1 $ t2) = let val (s, (ts1, ts2)) = aux t0 in (s, (t1 :: ts1, t2 :: ts2)) end - | aux t = raise TERM ("NitpickModel.dest_plain_fun", [t]) + | aux t = raise TERM ("Nitpick_Model.dest_plain_fun", [t]) in apsnd (pairself rev) o aux end (* typ -> term -> term list * term *) @@ -138,7 +138,7 @@ (Const (@{const_name Pair}, _) $ t1 $ t2) = break_in_two T2 t2 |>> cons t1 | break_in_two _ (Const (@{const_name Pair}, _) $ t1 $ t2) = ([t1], t2) - | break_in_two _ t = raise TERM ("NitpickModel.break_in_two", [t]) + | break_in_two _ t = raise TERM ("Nitpick_Model.break_in_two", [t]) (* typ -> term -> term -> term *) fun pair_up (Type ("*", [T1', T2'])) (t1 as Const (@{const_name Pair}, @@ -180,7 +180,7 @@ [T1' --> T2', T1', T2'] ---> T1' --> T2') $ do_arrow T1' T2' T1 T2 t0 $ do_term T1' T1 t1 $ do_term T2' T2 t2 | do_arrow _ _ _ _ t = - raise TERM ("NitpickModel.typecast_fun.do_arrow", [t]) + raise TERM ("Nitpick_Model.typecast_fun.do_arrow", [t]) and do_fun T1' T2' T1 T2 t = case factor_out_types T1' T1 of ((_, NONE), (_, NONE)) => t |> do_arrow T1' T2' T1 T2 @@ -188,7 +188,7 @@ t |> do_curry T1a T1b T2 |> do_arrow T1' T2' T1a (T1b --> T2) | ((T1a', SOME T1b'), (_, NONE)) => t |> do_arrow T1a' (T1b' --> T2') T1 T2 |> do_uncurry T1' T2' - | _ => raise TYPE ("NitpickModel.typecast_fun.do_fun", [T1, T1'], []) + | _ => raise TYPE ("Nitpick_Model.typecast_fun.do_fun", [T1, T1'], []) (* typ -> typ -> term -> term *) and do_term (Type ("fun", [T1', T2'])) (Type ("fun", [T1, T2])) t = do_fun T1' T2' T1 T2 t @@ -198,9 +198,9 @@ $ do_term T1' T1 t1 $ do_term T2' T2 t2 | do_term T' T t = if T = T' then t - else raise TYPE ("NitpickModel.typecast_fun.do_term", [T, T'], []) + else raise TYPE ("Nitpick_Model.typecast_fun.do_term", [T, T'], []) in if T1' = T1 andalso T2' = T2 then t else do_fun T1' T2' T1 T2 t end - | typecast_fun T' _ _ _ = raise TYPE ("NitpickModel.typecast_fun", [T'], []) + | typecast_fun T' _ _ _ = raise TYPE ("Nitpick_Model.typecast_fun", [T'], []) (* term -> string *) fun truth_const_sort_key @{const True} = "0" @@ -302,7 +302,7 @@ term_for_rep seen T T' (Vect (k1, Atom (k2, 0))) [nth_combination (replicate k1 (k2, 0)) j] handle General.Subscript => - raise ARG ("NitpickModel.reconstruct_term.term_for_atom", + raise ARG ("Nitpick_Model.reconstruct_term.term_for_atom", signed_string_of_int j ^ " for " ^ string_for_rep (Vect (k1, Atom (k2, 0)))) end @@ -350,7 +350,7 @@ map (fn x => get_first (fn ConstName (s', T', R) => if (s', T') = x then SOME R else NONE - | u => raise NUT ("NitpickModel.reconstruct_\ + | u => raise NUT ("Nitpick_Model.reconstruct_\ \term.term_for_atom", [u])) sel_names |> the) sel_xs val arg_Rs = map (snd o dest_Func) sel_Rs @@ -389,7 +389,7 @@ | n2 => Const (@{const_name HOL.divide}, [num_T, num_T] ---> num_T) $ mk_num n1 $ mk_num n2) - | _ => raise TERM ("NitpickModel.reconstruct_term.term_\ + | _ => raise TERM ("Nitpick_Model.reconstruct_term.term_\ \for_atom (Abs_Frac)", ts) end else if not for_auto andalso is_abs_fun thy constr_x then @@ -421,7 +421,7 @@ and term_for_rep seen T T' Unit [[]] = term_for_atom seen T T' 0 | term_for_rep seen T T' (R as Atom (k, j0)) [[j]] = if j >= j0 andalso j < j0 + k then term_for_atom seen T T' (j - j0) - else raise REP ("NitpickModel.reconstruct_term.term_for_rep", [R]) + else raise REP ("Nitpick_Model.reconstruct_term.term_for_rep", [R]) | term_for_rep seen (Type ("*", [T1, T2])) _ (Struct [R1, R2]) [js] = let val arity1 = arity_of_rep R1 @@ -454,7 +454,7 @@ | term_for_rep seen T T' (Opt R) jss = if null jss then Const (unknown, T) else term_for_rep seen T T' R jss | term_for_rep seen T _ R jss = - raise ARG ("NitpickModel.reconstruct_term.term_for_rep", + raise ARG ("Nitpick_Model.reconstruct_term.term_for_rep", Refute.string_of_typ T ^ " " ^ string_for_rep R ^ " " ^ string_of_int (length jss)) in @@ -576,7 +576,7 @@ (assign_operator_for_const (s, T), user_friendly_const ext_ctxt (base_name, step_name) formats (s, T), T) - | _ => raise NUT ("NitpickModel.reconstruct_hol_model.\ + | _ => raise NUT ("Nitpick_Model.reconstruct_hol_model.\ \pretty_for_assign", [name]) val t2 = if rep_of name = Any then Const (@{const_name undefined}, T') @@ -601,7 +601,7 @@ fun integer_datatype T = [{typ = T, card = card_of_type card_assigns T, co = false, precise = false, constrs = []}] - handle TYPE ("NitpickHOL.card_of_type", _, _) => [] + handle TYPE ("Nitpick_HOL.card_of_type", _, _) => [] val (codatatypes, datatypes) = List.partition #co datatypes ||> append (integer_datatype nat_T @ integer_datatype int_T) @@ -637,7 +637,7 @@ free_names of [name] => name | [] => FreeName (s, T, Any) - | _ => raise TERM ("NitpickModel.reconstruct_hol_model", + | _ => raise TERM ("Nitpick_Model.reconstruct_hol_model", [Const x])) all_frees val chunks = block_of_names true "Free variable" free_names @ block_of_names show_skolems "Skolem constant" skolem_names @ diff -r 1711610c5b7d -r f93390060bbe src/HOL/Tools/Nitpick/nitpick_mono.ML --- a/src/HOL/Tools/Nitpick/nitpick_mono.ML Tue Oct 27 12:16:26 2009 +0100 +++ b/src/HOL/Tools/Nitpick/nitpick_mono.ML Tue Oct 27 14:40:24 2009 +0100 @@ -7,17 +7,17 @@ signature NITPICK_MONO = sig - type extended_context = NitpickHOL.extended_context + type extended_context = Nitpick_HOL.extended_context val formulas_monotonic : extended_context -> typ -> term list -> term list -> term -> bool end; -structure NitpickMono : NITPICK_MONO = +structure Nitpick_Mono : NITPICK_MONO = struct -open NitpickUtil -open NitpickHOL +open Nitpick_Util +open Nitpick_HOL type var = int @@ -363,11 +363,11 @@ accum = (accum |> fold (uncurry (do_ctype_comp cmp xs)) [(C11, C21), (C12, C22)] handle Library.UnequalLengths => - raise CTYPE ("NitpickMono.do_ctype_comp", [C1, C2])) + raise CTYPE ("Nitpick_Mono.do_ctype_comp", [C1, C2])) | do_ctype_comp cmp xs (CType _) (CType _) accum = accum (* no need to compare them thanks to the cache *) | do_ctype_comp _ _ C1 C2 _ = - raise CTYPE ("NitpickMono.do_ctype_comp", [C1, C2]) + raise CTYPE ("Nitpick_Mono.do_ctype_comp", [C1, C2]) (* comp_op -> ctype -> ctype -> constraint_set -> constraint_set *) fun add_ctype_comp _ _ _ UnsolvableCSet = UnsolvableCSet @@ -413,7 +413,7 @@ | do_notin_ctype_fv sn sexp (CType (_, Cs)) accum = accum |> fold (do_notin_ctype_fv sn sexp) Cs | do_notin_ctype_fv _ _ C _ = - raise CTYPE ("NitpickMono.do_notin_ctype_fv", [C]) + raise CTYPE ("Nitpick_Mono.do_notin_ctype_fv", [C]) (* sign -> ctype -> constraint_set -> constraint_set *) fun add_notin_ctype_fv _ _ UnsolvableCSet = UnsolvableCSet @@ -584,13 +584,13 @@ case ctype_for (nth_range_type 2 T) of C as CPair (a_C, b_C) => (CFun (a_C, S Neg, CFun (b_C, S Neg, C)), accum) - | C => raise CTYPE ("NitpickMono.consider_term.do_pair_constr", [C]) + | C => raise CTYPE ("Nitpick_Mono.consider_term.do_pair_constr", [C]) (* int -> typ -> accumulator -> ctype * accumulator *) fun do_nth_pair_sel n T = case ctype_for (domain_type T) of C as CPair (a_C, b_C) => pair (CFun (C, S Neg, if n = 0 then a_C else b_C)) - | C => raise CTYPE ("NitpickMono.consider_term.do_nth_pair_sel", [C]) + | C => raise CTYPE ("Nitpick_Mono.consider_term.do_nth_pair_sel", [C]) val unsolvable = (CType ("unsolvable", []), unsolvable_accum) (* typ -> term -> accumulator -> ctype * accumulator *) fun do_bounded_quantifier abs_T bound_t body_t accum = @@ -770,7 +770,7 @@ | _ => case C1 of CFun (C11, _, C12) => (C12, accum ||> add_is_sub_ctype C2 C11) - | _ => raise CTYPE ("NitpickMono.consider_term.do_term \ + | _ => raise CTYPE ("Nitpick_Mono.consider_term.do_term \ \(op $)", [C1]) end) |> tap (fn (C, _) => @@ -906,7 +906,7 @@ | Const (@{const_name "op ="}, _) $ t1 $ t2 => do_equals t1 t2 accum | @{const "op &"} $ t1 $ t2 => accum |> do_formula t1 |> do_formula t2 | @{const "op -->"} $ t1 $ t2 => do_implies t1 t2 accum - | _ => raise TERM ("NitpickMono.consider_definitional_axiom.\ + | _ => raise TERM ("Nitpick_Mono.consider_definitional_axiom.\ \do_formula", [t]) in do_formula t end diff -r 1711610c5b7d -r f93390060bbe src/HOL/Tools/Nitpick/nitpick_nut.ML --- a/src/HOL/Tools/Nitpick/nitpick_nut.ML Tue Oct 27 12:16:26 2009 +0100 +++ b/src/HOL/Tools/Nitpick/nitpick_nut.ML Tue Oct 27 14:40:24 2009 +0100 @@ -7,11 +7,11 @@ signature NITPICK_NUT = sig - type special_fun = NitpickHOL.special_fun - type extended_context = NitpickHOL.extended_context - type scope = NitpickScope.scope - type name_pool = NitpickPeephole.name_pool - type rep = NitpickRep.rep + type special_fun = Nitpick_HOL.special_fun + type extended_context = Nitpick_HOL.extended_context + type scope = Nitpick_Scope.scope + type name_pool = Nitpick_Peephole.name_pool + type rep = Nitpick_Rep.rep datatype cst = Unity | @@ -121,14 +121,14 @@ val rename_vars_in_nut : name_pool -> nut NameTable.table -> nut -> nut end; -structure NitpickNut : NITPICK_NUT = +structure Nitpick_Nut : NITPICK_NUT = struct -open NitpickUtil -open NitpickHOL -open NitpickScope -open NitpickPeephole -open NitpickRep +open Nitpick_Util +open Nitpick_HOL +open Nitpick_Scope +open Nitpick_Peephole +open Nitpick_Rep datatype cst = Unity | @@ -357,16 +357,16 @@ | nickname_of (ConstName (s, _, _)) = s | nickname_of (BoundRel (_, _, _, nick)) = nick | nickname_of (FreeRel (_, _, _, nick)) = nick - | nickname_of u = raise NUT ("NitpickNut.nickname_of", [u]) + | nickname_of u = raise NUT ("Nitpick_Nut.nickname_of", [u]) (* nut -> bool *) fun is_skolem_name u = space_explode name_sep (nickname_of u) |> exists (String.isPrefix skolem_prefix) - handle NUT ("NitpickNut.nickname_of", _) => false + handle NUT ("Nitpick_Nut.nickname_of", _) => false fun is_eval_name u = String.isPrefix eval_prefix (nickname_of u) - handle NUT ("NitpickNut.nickname_of", _) => false + handle NUT ("Nitpick_Nut.nickname_of", _) => false (* cst -> nut -> bool *) fun is_Cst cst (Cst (cst', _, _)) = (cst = cst') | is_Cst _ _ = false @@ -407,7 +407,7 @@ (case fast_string_ord (s1, s2) of EQUAL => TermOrd.typ_ord (T1, T2) | ord => ord) - | name_ord (u1, u2) = raise NUT ("NitpickNut.name_ord", [u1, u2]) + | name_ord (u1, u2) = raise NUT ("Nitpick_Nut.name_ord", [u1, u2]) (* nut -> nut -> int *) fun num_occs_in_nut needle_u stack_u = @@ -430,7 +430,7 @@ fun modify_name_rep (BoundName (j, T, _, nick)) R = BoundName (j, T, R, nick) | modify_name_rep (FreeName (s, T, _)) R = FreeName (s, T, R) | modify_name_rep (ConstName (s, T, _)) R = ConstName (s, T, R) - | modify_name_rep u _ = raise NUT ("NitpickNut.modify_name_rep", [u]) + | modify_name_rep u _ = raise NUT ("Nitpick_Nut.modify_name_rep", [u]) structure NameTable = Table(type key = nut val ord = name_ord) @@ -438,12 +438,12 @@ fun the_name table name = case NameTable.lookup table name of SOME u => u - | NONE => raise NUT ("NitpickNut.the_name", [name]) + | NONE => raise NUT ("Nitpick_Nut.the_name", [name]) (* nut NameTable.table -> nut -> Kodkod.n_ary_index *) fun the_rel table name = case the_name table name of FreeRel (x, _, _, _) => x - | u => raise NUT ("NitpickNut.the_rel", [u]) + | u => raise NUT ("Nitpick_Nut.the_rel", [u]) (* typ * term -> typ * term *) fun mk_fst (_, Const (@{const_name Pair}, T) $ t1 $ _) = (domain_type T, t1) @@ -669,13 +669,13 @@ (case arity_of_built_in_const fast_descrs x of SOME n => (case n - length ts of - 0 => raise TERM ("NitpickNut.nut_from_term.aux", [t]) + 0 => raise TERM ("Nitpick_Nut.nut_from_term.aux", [t]) | k => if k > 0 then sub (eta_expand Ts t k) else do_apply t0 ts) | NONE => if null ts then ConstName (s, T, Any) else do_apply t0 ts) | (Free (s, T), []) => FreeName (s, T, Any) - | (Var _, []) => raise TERM ("NitpickNut.nut_from_term", [t]) + | (Var _, []) => raise TERM ("Nitpick_Nut.nut_from_term", [t]) | (Bound j, []) => BoundName (length Ts - j - 1, nth Ts j, Any, nth ss j) | (Abs (s, T, t1), []) => @@ -1106,7 +1106,7 @@ else unopt_rep R in s_op2 Lambda T R u1' u2' end - | R => raise NUT ("NitpickNut.aux.choose_reps_in_nut", [u])) + | R => raise NUT ("Nitpick_Nut.aux.choose_reps_in_nut", [u])) | Op2 (oper, T, _, u1, u2) => if oper mem [All, Exist] then let @@ -1274,9 +1274,9 @@ | shape_tuple (T as Type ("fun", [_, T2])) (R as Vect (k, R')) us = Tuple (T, R, map (shape_tuple T2 R') (batch_list (length us div k) us)) | shape_tuple T R [u] = - if type_of u = T then u else raise NUT ("NitpickNut.shape_tuple", [u]) + if type_of u = T then u else raise NUT ("Nitpick_Nut.shape_tuple", [u]) | shape_tuple T Unit [] = Cst (Unity, T, Unit) - | shape_tuple _ _ us = raise NUT ("NitpickNut.shape_tuple", us) + | shape_tuple _ _ us = raise NUT ("Nitpick_Nut.shape_tuple", us) (* bool -> nut -> nut list * name_pool * nut NameTable.table -> nut list * name_pool * nut NameTable.table *) diff -r 1711610c5b7d -r f93390060bbe src/HOL/Tools/Nitpick/nitpick_peephole.ML --- a/src/HOL/Tools/Nitpick/nitpick_peephole.ML Tue Oct 27 12:16:26 2009 +0100 +++ b/src/HOL/Tools/Nitpick/nitpick_peephole.ML Tue Oct 27 14:40:24 2009 +0100 @@ -86,11 +86,11 @@ val kodkod_constrs : bool -> int -> int -> int -> kodkod_constrs end; -structure NitpickPeephole : NITPICK_PEEPHOLE = +structure Nitpick_Peephole : NITPICK_PEEPHOLE = struct open Kodkod -open NitpickUtil +open Nitpick_Util type name_pool = { rels: n_ary_index list, @@ -188,20 +188,20 @@ if is_none_product r1 orelse is_none_product r2 then SOME false else NONE (* int -> rel_expr *) -fun empty_n_ary_rel 0 = raise ARG ("NitpickPeephole.empty_n_ary_rel", "0") +fun empty_n_ary_rel 0 = raise ARG ("Nitpick_Peephole.empty_n_ary_rel", "0") | empty_n_ary_rel n = funpow (n - 1) (curry Product None) None (* decl -> rel_expr *) fun decl_one_set (DeclOne (_, r)) = r | decl_one_set _ = - raise ARG ("NitpickPeephole.decl_one_set", "not \"DeclOne\"") + raise ARG ("Nitpick_Peephole.decl_one_set", "not \"DeclOne\"") (* int_expr -> bool *) fun is_Num (Num _) = true | is_Num _ = false (* int_expr -> int *) fun dest_Num (Num k) = k - | dest_Num _ = raise ARG ("NitpickPeephole.dest_Num", "not \"Num\"") + | dest_Num _ = raise ARG ("Nitpick_Peephole.dest_Num", "not \"Num\"") (* int -> int -> int_expr list *) fun num_seq j0 n = map Num (index_seq j0 n) diff -r 1711610c5b7d -r f93390060bbe src/HOL/Tools/Nitpick/nitpick_rep.ML --- a/src/HOL/Tools/Nitpick/nitpick_rep.ML Tue Oct 27 12:16:26 2009 +0100 +++ b/src/HOL/Tools/Nitpick/nitpick_rep.ML Tue Oct 27 14:40:24 2009 +0100 @@ -7,8 +7,8 @@ signature NITPICK_REP = sig - type polarity = NitpickUtil.polarity - type scope = NitpickScope.scope + type polarity = Nitpick_Util.polarity + type scope = Nitpick_Scope.scope datatype rep = Any | @@ -58,12 +58,12 @@ val all_combinations_for_reps : rep list -> int list list end; -structure NitpickRep : NITPICK_REP = +structure Nitpick_Rep : NITPICK_REP = struct -open NitpickUtil -open NitpickHOL -open NitpickScope +open Nitpick_Util +open Nitpick_HOL +open Nitpick_Scope datatype rep = Any | @@ -111,7 +111,7 @@ | is_opt_rep _ = false (* rep -> int *) -fun card_of_rep Any = raise REP ("NitpickRep.card_of_rep", [Any]) +fun card_of_rep Any = raise REP ("Nitpick_Rep.card_of_rep", [Any]) | card_of_rep (Formula _) = 2 | card_of_rep Unit = 1 | card_of_rep (Atom (k, _)) = k @@ -120,7 +120,7 @@ | card_of_rep (Func (R1, R2)) = reasonable_power (card_of_rep R2) (card_of_rep R1) | card_of_rep (Opt R) = card_of_rep R -fun arity_of_rep Any = raise REP ("NitpickRep.arity_of_rep", [Any]) +fun arity_of_rep Any = raise REP ("Nitpick_Rep.arity_of_rep", [Any]) | arity_of_rep (Formula _) = 0 | arity_of_rep Unit = 0 | arity_of_rep (Atom _) = 1 @@ -129,7 +129,7 @@ | arity_of_rep (Func (R1, R2)) = arity_of_rep R1 + arity_of_rep R2 | arity_of_rep (Opt R) = arity_of_rep R fun min_univ_card_of_rep Any = - raise REP ("NitpickRep.min_univ_card_of_rep", [Any]) + raise REP ("Nitpick_Rep.min_univ_card_of_rep", [Any]) | min_univ_card_of_rep (Formula _) = 0 | min_univ_card_of_rep Unit = 0 | min_univ_card_of_rep (Atom (k, j0)) = k + j0 + 1 @@ -151,7 +151,7 @@ (* rep -> rep * rep *) fun dest_Func (Func z) = z - | dest_Func R = raise REP ("NitpickRep.dest_Func", [R]) + | dest_Func R = raise REP ("Nitpick_Rep.dest_Func", [R]) (* int Typtab.table -> typ -> (unit -> int) -> rep -> rep *) fun smart_range_rep _ _ _ Unit = Unit | smart_range_rep _ _ _ (Vect (_, R)) = R @@ -162,7 +162,7 @@ Atom (1, offset_of_type ofs T2) | smart_range_rep ofs (Type ("fun", [_, T2])) ran_card (Atom _) = Atom (ran_card (), offset_of_type ofs T2) - | smart_range_rep _ _ _ R = raise REP ("NitpickRep.smart_range_rep", [R]) + | smart_range_rep _ _ _ R = raise REP ("Nitpick_Rep.smart_range_rep", [R]) (* rep -> rep list *) fun binder_reps (Func (R1, R2)) = R1 :: binder_reps R2 @@ -177,7 +177,7 @@ | flip_rep_polarity R = R (* int Typtab.table -> rep -> rep *) -fun one_rep _ _ Any = raise REP ("NitpickRep.one_rep", [Any]) +fun one_rep _ _ Any = raise REP ("Nitpick_Rep.one_rep", [Any]) | one_rep _ _ (Atom x) = Atom x | one_rep _ _ (Struct Rs) = Struct Rs | one_rep _ _ (Vect z) = Vect z @@ -203,7 +203,7 @@ else if polar2 = Neut then polar1 else - raise ARG ("NitpickRep.min_polarity", + raise ARG ("Nitpick_Rep.min_polarity", commas (map (quote o string_for_polarity) [polar1, polar2])) (* It's important that Func is before Vect, because if the range is Opt we @@ -236,7 +236,7 @@ if k1 < k2 then Vect (k1, R1) else if k1 > k2 then Vect (k2, R2) else Vect (k1, min_rep R1 R2) - | min_rep R1 R2 = raise REP ("NitpickRep.min_rep", [R1, R2]) + | min_rep R1 R2 = raise REP ("Nitpick_Rep.min_rep", [R1, R2]) (* rep list -> rep list -> rep list *) and min_reps [] _ = [] | min_reps _ [] = [] @@ -253,7 +253,7 @@ | Vect (k, _) => k | Func (R1, _) => card_of_rep R1 | Opt R => card_of_domain_from_rep ran_card R - | _ => raise REP ("NitpickRep.card_of_domain_from_rep", [R]) + | _ => raise REP ("Nitpick_Rep.card_of_domain_from_rep", [R]) (* int Typtab.table -> typ -> rep -> rep *) fun rep_to_binary_rel_rep ofs T R = @@ -306,10 +306,10 @@ (optable_rep ofs T1 (best_one_rep_for_type scope T1), optable_rep ofs T2 (best_one_rep_for_type scope T2)) | best_non_opt_symmetric_reps_for_fun_type _ T = - raise TYPE ("NitpickRep.best_non_opt_symmetric_reps_for_fun_type", [T], []) + raise TYPE ("Nitpick_Rep.best_non_opt_symmetric_reps_for_fun_type", [T], []) (* rep -> (int * int) list *) -fun atom_schema_of_rep Any = raise REP ("NitpickRep.atom_schema_of_rep", [Any]) +fun atom_schema_of_rep Any = raise REP ("Nitpick_Rep.atom_schema_of_rep", [Any]) | atom_schema_of_rep (Formula _) = [] | atom_schema_of_rep Unit = [] | atom_schema_of_rep (Atom x) = [x] @@ -332,7 +332,7 @@ | type_schema_of_rep (Type ("fun", [T1, T2])) (Func (R1, R2)) = type_schema_of_rep T1 R1 @ type_schema_of_rep T2 R2 | type_schema_of_rep T (Opt R) = type_schema_of_rep T R - | type_schema_of_rep T R = raise REP ("NitpickRep.type_schema_of_rep", [R]) + | type_schema_of_rep T R = raise REP ("Nitpick_Rep.type_schema_of_rep", [R]) (* typ list -> rep list -> typ list *) and type_schema_of_reps Ts Rs = flat (map2 type_schema_of_rep Ts Rs) diff -r 1711610c5b7d -r f93390060bbe src/HOL/Tools/Nitpick/nitpick_scope.ML --- a/src/HOL/Tools/Nitpick/nitpick_scope.ML Tue Oct 27 12:16:26 2009 +0100 +++ b/src/HOL/Tools/Nitpick/nitpick_scope.ML Tue Oct 27 14:40:24 2009 +0100 @@ -7,7 +7,7 @@ signature NITPICK_SCOPE = sig - type extended_context = NitpickHOL.extended_context + type extended_context = Nitpick_HOL.extended_context type constr_spec = { const: styp, @@ -47,11 +47,11 @@ -> int list -> typ list -> typ list -> scope list end; -structure NitpickScope : NITPICK_SCOPE = +structure Nitpick_Scope : NITPICK_SCOPE = struct -open NitpickUtil -open NitpickHOL +open Nitpick_Util +open Nitpick_HOL type constr_spec = { const: styp, @@ -85,7 +85,7 @@ List.find (equal T o #typ) dtypes (* dtype_spec list -> styp -> constr_spec *) -fun constr_spec [] x = raise TERM ("NitpickScope.constr_spec", [Const x]) +fun constr_spec [] x = raise TERM ("Nitpick_Scope.constr_spec", [Const x]) | constr_spec ({constrs, ...} :: dtypes : dtype_spec list) (x as (s, T)) = case List.find (equal (s, body_type T) o (apsnd body_type o #const)) constrs of @@ -115,7 +115,7 @@ (* scope -> typ -> int * int *) fun spec_of_type ({card_assigns, ofs, ...} : scope) T = (card_of_type card_assigns T - handle TYPE ("NitpickHOL.card_of_type", _, _) => ~1, offset_of_type ofs T) + handle TYPE ("Nitpick_HOL.card_of_type", _, _) => ~1, offset_of_type ofs T) (* (string -> string) -> scope -> string list * string list * string list * string list * string list *) @@ -205,17 +205,17 @@ fun lookup_ints_assign eq asgns key = case triple_lookup eq asgns key of SOME ks => ks - | NONE => raise ARG ("NitpickScope.lookup_ints_assign", "") + | NONE => raise ARG ("Nitpick_Scope.lookup_ints_assign", "") (* theory -> (typ option * int list) list -> typ -> int list *) fun lookup_type_ints_assign thy asgns T = map (curry Int.max 1) (lookup_ints_assign (type_match thy) asgns T) - handle ARG ("NitpickScope.lookup_ints_assign", _) => - raise TYPE ("NitpickScope.lookup_type_ints_assign", [T], []) + handle ARG ("Nitpick_Scope.lookup_ints_assign", _) => + raise TYPE ("Nitpick_Scope.lookup_type_ints_assign", [T], []) (* theory -> (styp option * int list) list -> styp -> int list *) fun lookup_const_ints_assign thy asgns x = lookup_ints_assign (const_match thy) asgns x - handle ARG ("NitpickScope.lookup_ints_assign", _) => - raise TERM ("NitpickScope.lookup_const_ints_assign", [Const x]) + handle ARG ("Nitpick_Scope.lookup_ints_assign", _) => + raise TERM ("Nitpick_Scope.lookup_const_ints_assign", [Const x]) (* theory -> (styp option * int list) list -> styp -> row option *) fun row_for_constr thy maxes_asgns constr = @@ -315,7 +315,7 @@ max < k orelse (forall (not_equal 0) precise_cards andalso doms_card () < k) end - handle TYPE ("NitpickHOL.card_of_type", _, _) => false + handle TYPE ("Nitpick_HOL.card_of_type", _, _) => false (* theory -> scope_desc -> bool *) fun is_surely_inconsistent_scope_description thy (desc as (card_asgns, _)) = diff -r 1711610c5b7d -r f93390060bbe src/HOL/Tools/Nitpick/nitpick_tests.ML --- a/src/HOL/Tools/Nitpick/nitpick_tests.ML Tue Oct 27 12:16:26 2009 +0100 +++ b/src/HOL/Tools/Nitpick/nitpick_tests.ML Tue Oct 27 14:40:24 2009 +0100 @@ -10,15 +10,14 @@ val run_all_tests : unit -> unit end -structure NitpickTests = +structure Nitpick_Tests = struct -open NitpickUtil -open NitpickPeephole -open NitpickRep -open NitpickNut -open NitpickKodkod -open Nitpick +open Nitpick_Util +open Nitpick_Peephole +open Nitpick_Rep +open Nitpick_Nut +open Nitpick_Kodkod val settings = [("solver", "\"zChaff\""), diff -r 1711610c5b7d -r f93390060bbe src/HOL/Tools/Nitpick/nitpick_util.ML --- a/src/HOL/Tools/Nitpick/nitpick_util.ML Tue Oct 27 12:16:26 2009 +0100 +++ b/src/HOL/Tools/Nitpick/nitpick_util.ML Tue Oct 27 14:40:24 2009 +0100 @@ -72,7 +72,7 @@ val maybe_quote : string -> string end -structure NitpickUtil : NITPICK_UTIL = +structure Nitpick_Util : NITPICK_UTIL = struct type styp = string * typ @@ -107,7 +107,7 @@ | reasonable_power 1 _ = 1 | reasonable_power a b = if b < 0 orelse b > max_exponent then - raise LIMIT ("NitpickUtil.reasonable_power", + raise LIMIT ("Nitpick_Util.reasonable_power", "too large exponent (" ^ signed_string_of_int b ^ ")") else let @@ -123,7 +123,7 @@ if reasonable_power m r = n then r else - raise ARG ("NitpickUtil.exact_log", + raise ARG ("Nitpick_Util.exact_log", commas (map signed_string_of_int [m, n])) end @@ -133,7 +133,7 @@ if reasonable_power r m = n then r else - raise ARG ("NitpickUtil.exact_root", + raise ARG ("Nitpick_Util.exact_root", commas (map signed_string_of_int [m, n])) end @@ -156,7 +156,7 @@ fun aux _ [] _ = [] | aux i (j :: js) (x :: xs) = if i = j then x :: aux (i + 1) js xs else aux (i + 1) (j :: js) xs - | aux _ _ _ = raise ARG ("NitpickUtil.filter_indices", + | aux _ _ _ = raise ARG ("Nitpick_Util.filter_indices", "indices unordered or out of range") in aux 0 js xs end fun filter_out_indices js xs = @@ -165,7 +165,7 @@ fun aux _ [] xs = xs | aux i (j :: js) (x :: xs) = if i = j then aux (i + 1) js xs else x :: aux (i + 1) (j :: js) xs - | aux _ _ _ = raise ARG ("NitpickUtil.filter_out_indices", + | aux _ _ _ = raise ARG ("Nitpick_Util.filter_out_indices", "indices unordered or out of range") in aux 0 js xs end @@ -303,5 +303,5 @@ end; -structure BasicNitpickUtil : BASIC_NITPICK_UTIL = NitpickUtil; -open BasicNitpickUtil; +structure Basic_Nitpick_Util : BASIC_NITPICK_UTIL = Nitpick_Util; +open Basic_Nitpick_Util;