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
--- 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}$
--- 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,
--- 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
--- 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 "") ^
--- 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
--- 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
--- 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,
--- 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
--- 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
--- 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
--- 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 @
--- 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
--- 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 *)
--- 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)
--- 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)
--- 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, _)) =
--- 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\""),
--- 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;