1.1 --- a/src/HOL/Tools/Nitpick/nitpick_kodkod.ML Tue Oct 27 12:16:26 2009 +0100
1.2 +++ b/src/HOL/Tools/Nitpick/nitpick_kodkod.ML Tue Oct 27 14:40:24 2009 +0100
1.3 @@ -7,10 +7,10 @@
1.4
1.5 signature NITPICK_KODKOD =
1.6 sig
1.7 - type extended_context = NitpickHOL.extended_context
1.8 - type dtype_spec = NitpickScope.dtype_spec
1.9 - type kodkod_constrs = NitpickPeephole.kodkod_constrs
1.10 - type nut = NitpickNut.nut
1.11 + type extended_context = Nitpick_HOL.extended_context
1.12 + type dtype_spec = Nitpick_Scope.dtype_spec
1.13 + type kodkod_constrs = Nitpick_Peephole.kodkod_constrs
1.14 + type nut = Nitpick_Nut.nut
1.15 type nfa_transition = Kodkod.rel_expr * typ
1.16 type nfa_entry = typ * nfa_transition list
1.17 type nfa_table = nfa_entry list
1.18 @@ -37,15 +37,15 @@
1.19 int Typtab.table -> bool -> kodkod_constrs -> nut -> Kodkod.formula
1.20 end;
1.21
1.22 -structure NitpickKodkod : NITPICK_KODKOD =
1.23 +structure Nitpick_Kodkod : NITPICK_KODKOD =
1.24 struct
1.25
1.26 -open NitpickUtil
1.27 -open NitpickHOL
1.28 -open NitpickScope
1.29 -open NitpickPeephole
1.30 -open NitpickRep
1.31 -open NitpickNut
1.32 +open Nitpick_Util
1.33 +open Nitpick_HOL
1.34 +open Nitpick_Scope
1.35 +open Nitpick_Peephole
1.36 +open Nitpick_Rep
1.37 +open Nitpick_Nut
1.38
1.39 type nfa_transition = Kodkod.rel_expr * typ
1.40 type nfa_entry = typ * nfa_transition list
1.41 @@ -89,7 +89,7 @@
1.42 (* int -> int -> unit *)
1.43 fun check_arity univ_card n =
1.44 if n > Kodkod.max_arity univ_card then
1.45 - raise LIMIT ("NitpickKodkod.check_arity",
1.46 + raise LIMIT ("Nitpick_Kodkod.check_arity",
1.47 "arity " ^ string_of_int n ^ " too large for universe of \
1.48 \cardinality " ^ string_of_int univ_card)
1.49 else
1.50 @@ -132,7 +132,7 @@
1.51 (* int -> unit *)
1.52 fun check_table_size k =
1.53 if k > max_table_size then
1.54 - raise LIMIT ("NitpickKodkod.check_table_size",
1.55 + raise LIMIT ("Nitpick_Kodkod.check_table_size",
1.56 "precomputed table too large (" ^ string_of_int k ^ ")")
1.57 else
1.58 ()
1.59 @@ -245,7 +245,7 @@
1.60 ("norm_frac", tabulate_int_op2_2 debug univ_card (int_card, j0)
1.61 isa_norm_frac)
1.62 else
1.63 - raise ARG ("NitpickKodkod.tabulate_built_in_rel", "unknown relation"))
1.64 + raise ARG ("Nitpick_Kodkod.tabulate_built_in_rel", "unknown relation"))
1.65
1.66 (* bool -> int -> int -> int -> int -> int * int -> Kodkod.rel_expr
1.67 -> Kodkod.bound *)
1.68 @@ -266,11 +266,11 @@
1.69 if nick = @{const_name bisim_iterator_max} then
1.70 case R of
1.71 Atom (k, j0) => [Kodkod.TupleSet [Kodkod.Tuple [k - 1 + j0]]]
1.72 - | _ => raise NUT ("NitpickKodkod.bound_for_plain_rel", [u])
1.73 + | _ => raise NUT ("Nitpick_Kodkod.bound_for_plain_rel", [u])
1.74 else
1.75 [Kodkod.TupleSet [], upper_bound_for_rep R])
1.76 | bound_for_plain_rel _ _ u =
1.77 - raise NUT ("NitpickKodkod.bound_for_plain_rel", [u])
1.78 + raise NUT ("Nitpick_Kodkod.bound_for_plain_rel", [u])
1.79
1.80 (* Proof.context -> bool -> dtype_spec list -> nut -> Kodkod.bound *)
1.81 fun bound_for_sel_rel ctxt debug dtypes
1.82 @@ -293,7 +293,7 @@
1.83 end)
1.84 end
1.85 | bound_for_sel_rel _ _ _ u =
1.86 - raise NUT ("NitpickKodkod.bound_for_sel_rel", [u])
1.87 + raise NUT ("Nitpick_Kodkod.bound_for_sel_rel", [u])
1.88
1.89 (* Kodkod.bound list -> Kodkod.bound list *)
1.90 fun merge_bounds bs =
1.91 @@ -320,7 +320,7 @@
1.92 if is_lone_rep R then
1.93 all_combinations_for_rep R |> map singleton_from_combination
1.94 else
1.95 - raise REP ("NitpickKodkod.all_singletons_for_rep", [R])
1.96 + raise REP ("Nitpick_Kodkod.all_singletons_for_rep", [R])
1.97
1.98 (* Kodkod.rel_expr -> Kodkod.rel_expr list *)
1.99 fun unpack_products (Kodkod.Product (r1, r2)) =
1.100 @@ -333,7 +333,7 @@
1.101 val empty_rel_for_rep = empty_n_ary_rel o arity_of_rep
1.102 fun full_rel_for_rep R =
1.103 case atom_schema_of_rep R of
1.104 - [] => raise REP ("NitpickKodkod.full_rel_for_rep", [R])
1.105 + [] => raise REP ("Nitpick_Kodkod.full_rel_for_rep", [R])
1.106 | schema => foldl1 Kodkod.Product (map Kodkod.AtomSeq schema)
1.107
1.108 (* int -> int list -> Kodkod.decl list *)
1.109 @@ -424,7 +424,7 @@
1.110 fun rel_expr_from_formula kk R f =
1.111 case unopt_rep R of
1.112 Atom (2, j0) => atom_from_formula kk j0 f
1.113 - | _ => raise REP ("NitpickKodkod.rel_expr_from_formula", [R])
1.114 + | _ => raise REP ("Nitpick_Kodkod.rel_expr_from_formula", [R])
1.115
1.116 (* kodkod_cotrs -> int -> int -> Kodkod.rel_expr -> Kodkod.rel_expr list *)
1.117 fun unpack_vect_in_chunks ({kk_project_seq, ...} : kodkod_constrs) chunk_arity
1.118 @@ -471,13 +471,13 @@
1.119 if is_lone_rep old_R andalso is_lone_rep new_R
1.120 andalso card = card_of_rep new_R then
1.121 if card >= lone_rep_fallback_max_card then
1.122 - raise LIMIT ("NitpickKodkod.lone_rep_fallback",
1.123 + raise LIMIT ("Nitpick_Kodkod.lone_rep_fallback",
1.124 "too high cardinality (" ^ string_of_int card ^ ")")
1.125 else
1.126 kk_case_switch kk old_R new_R r (all_singletons_for_rep old_R)
1.127 (all_singletons_for_rep new_R)
1.128 else
1.129 - raise REP ("NitpickKodkod.lone_rep_fallback", [old_R, new_R])
1.130 + raise REP ("Nitpick_Kodkod.lone_rep_fallback", [old_R, new_R])
1.131 end
1.132 (* kodkod_constrs -> int * int -> rep -> Kodkod.rel_expr -> Kodkod.rel_expr *)
1.133 and atom_from_rel_expr kk (x as (k, j0)) old_R r =
1.134 @@ -490,7 +490,7 @@
1.135 atom_from_rel_expr kk x (Vect (dom_card, R2'))
1.136 (vect_from_rel_expr kk dom_card R2' old_R r)
1.137 end
1.138 - | Opt _ => raise REP ("NitpickKodkod.atom_from_rel_expr", [old_R])
1.139 + | Opt _ => raise REP ("Nitpick_Kodkod.atom_from_rel_expr", [old_R])
1.140 | _ => lone_rep_fallback kk (Atom x) old_R r
1.141 (* kodkod_constrs -> rep list -> rep -> Kodkod.rel_expr -> Kodkod.rel_expr *)
1.142 and struct_from_rel_expr kk Rs old_R r =
1.143 @@ -515,7 +515,7 @@
1.144 else
1.145 lone_rep_fallback kk (Struct Rs) old_R r
1.146 end
1.147 - | _ => raise REP ("NitpickKodkod.struct_from_rel_expr", [old_R])
1.148 + | _ => raise REP ("Nitpick_Kodkod.struct_from_rel_expr", [old_R])
1.149 (* kodkod_constrs -> int -> rep -> rep -> Kodkod.rel_expr -> Kodkod.rel_expr *)
1.150 and vect_from_rel_expr kk k R old_R r =
1.151 case old_R of
1.152 @@ -530,7 +530,7 @@
1.153 rel_expr_from_formula kk R (#kk_subset kk arg_r r))
1.154 (all_singletons_for_rep R1))
1.155 else
1.156 - raise REP ("NitpickKodkod.vect_from_rel_expr", [old_R])
1.157 + raise REP ("Nitpick_Kodkod.vect_from_rel_expr", [old_R])
1.158 | Func (Unit, R2) => rel_expr_from_rel_expr kk R R2 r
1.159 | Func (R1, R2) =>
1.160 fold1 (#kk_product kk)
1.161 @@ -538,7 +538,7 @@
1.162 rel_expr_from_rel_expr kk R R2
1.163 (kk_n_fold_join kk true R1 R2 arg_r r))
1.164 (all_singletons_for_rep R1))
1.165 - | _ => raise REP ("NitpickKodkod.vect_from_rel_expr", [old_R])
1.166 + | _ => raise REP ("Nitpick_Kodkod.vect_from_rel_expr", [old_R])
1.167 (* kodkod_constrs -> rep -> rep -> rep -> Kodkod.rel_expr -> Kodkod.rel_expr *)
1.168 and func_from_no_opt_rel_expr kk R1 R2 (Atom x) r =
1.169 let
1.170 @@ -555,12 +555,12 @@
1.171 | Func (Atom (1, _), Formula Neut) =>
1.172 (case unopt_rep R2 of
1.173 Atom (2, j0) => atom_from_formula kk j0 (#kk_some kk r)
1.174 - | _ => raise REP ("NitpickKodkod.func_from_no_opt_rel_expr",
1.175 + | _ => raise REP ("Nitpick_Kodkod.func_from_no_opt_rel_expr",
1.176 [old_R, Func (Unit, R2)]))
1.177 | Func (R1', R2') =>
1.178 rel_expr_from_rel_expr kk R2 R2' (#kk_project_seq kk r (arity_of_rep R1')
1.179 (arity_of_rep R2'))
1.180 - | _ => raise REP ("NitpickKodkod.func_from_no_opt_rel_expr",
1.181 + | _ => raise REP ("Nitpick_Kodkod.func_from_no_opt_rel_expr",
1.182 [old_R, Func (Unit, R2)]))
1.183 | func_from_no_opt_rel_expr kk R1 (Formula Neut) old_R r =
1.184 (case old_R of
1.185 @@ -592,7 +592,7 @@
1.186 | Func (R1', Atom (2, j0)) =>
1.187 func_from_no_opt_rel_expr kk R1 (Formula Neut)
1.188 (Func (R1', Formula Neut)) (#kk_join kk r (Kodkod.Atom (j0 + 1)))
1.189 - | _ => raise REP ("NitpickKodkod.func_from_no_opt_rel_expr",
1.190 + | _ => raise REP ("Nitpick_Kodkod.func_from_no_opt_rel_expr",
1.191 [old_R, Func (R1, Formula Neut)]))
1.192 | func_from_no_opt_rel_expr kk R1 R2 old_R r =
1.193 case old_R of
1.194 @@ -621,7 +621,7 @@
1.195 (#kk_rel_eq kk r2 r3)
1.196 end
1.197 end
1.198 - | _ => raise REP ("NitpickKodkod.func_from_no_opt_rel_expr",
1.199 + | _ => raise REP ("Nitpick_Kodkod.func_from_no_opt_rel_expr",
1.200 [old_R, Func (R1, R2)]))
1.201 | Func (Unit, R2') =>
1.202 let val j0 = some_j0 in
1.203 @@ -648,7 +648,7 @@
1.204 (dom_schema @ ran_schema))
1.205 (#kk_subset kk ran_prod app)
1.206 end
1.207 - | _ => raise REP ("NitpickKodkod.func_from_no_opt_rel_expr",
1.208 + | _ => raise REP ("Nitpick_Kodkod.func_from_no_opt_rel_expr",
1.209 [old_R, Func (R1, R2)])
1.210 (* kodkod_constrs -> rep -> rep -> Kodkod.rel_expr -> Kodkod.rel_expr *)
1.211 and rel_expr_from_rel_expr kk new_R old_R r =
1.212 @@ -657,7 +657,7 @@
1.213 val unopt_new_R = unopt_rep new_R
1.214 in
1.215 if unopt_old_R <> old_R andalso unopt_new_R = new_R then
1.216 - raise REP ("NitpickKodkod.rel_expr_from_rel_expr", [old_R, new_R])
1.217 + raise REP ("Nitpick_Kodkod.rel_expr_from_rel_expr", [old_R, new_R])
1.218 else if unopt_new_R = unopt_old_R then
1.219 r
1.220 else
1.221 @@ -666,7 +666,7 @@
1.222 | Struct Rs => struct_from_rel_expr kk Rs
1.223 | Vect (k, R') => vect_from_rel_expr kk k R'
1.224 | Func (R1, R2) => func_from_no_opt_rel_expr kk R1 R2
1.225 - | _ => raise REP ("NitpickKodkod.rel_expr_from_rel_expr",
1.226 + | _ => raise REP ("Nitpick_Kodkod.rel_expr_from_rel_expr",
1.227 [old_R, new_R]))
1.228 unopt_old_R r
1.229 end
1.230 @@ -683,13 +683,13 @@
1.231 else if is_lone_rep R andalso card_of_rep R > 1 then kk_lone (Kodkod.Rel x)
1.232 else Kodkod.True
1.233 | declarative_axiom_for_plain_rel _ u =
1.234 - raise NUT ("NitpickKodkod.declarative_axiom_for_plain_rel", [u])
1.235 + raise NUT ("Nitpick_Kodkod.declarative_axiom_for_plain_rel", [u])
1.236
1.237 (* nut NameTable.table -> styp -> Kodkod.rel_expr * rep * int *)
1.238 fun const_triple rel_table (x as (s, T)) =
1.239 case the_name rel_table (ConstName (s, T, Any)) of
1.240 FreeRel ((n, j), _, R, _) => (Kodkod.Rel (n, j), R, n)
1.241 - | _ => raise TERM ("NitpickKodkod.const_triple", [Const x])
1.242 + | _ => raise TERM ("Nitpick_Kodkod.const_triple", [Const x])
1.243
1.244 (* nut NameTable.table -> styp -> Kodkod.rel_expr *)
1.245 fun discr_rel_expr rel_table = #1 o const_triple rel_table o discr_for_constr
1.246 @@ -849,7 +849,8 @@
1.247 (~1 upto num_sels - 1)
1.248 val j0 = case triples |> hd |> #2 of
1.249 Func (Atom (_, j0), _) => j0
1.250 - | R => raise REP ("NitpickKodkod.uniqueness_axiom_for_constr", [R])
1.251 + | R => raise REP ("Nitpick_Kodkod.uniqueness_axiom_for_constr",
1.252 + [R])
1.253 val set_r = triples |> hd |> #1
1.254 in
1.255 if num_sels = 0 then
1.256 @@ -960,7 +961,7 @@
1.257 let val opt1 = is_opt_rep (rep_of u1) in
1.258 case polar of
1.259 Neut => if opt1 then
1.260 - raise NUT ("NitpickKodkod.to_f (Finite)", [u])
1.261 + raise NUT ("Nitpick_Kodkod.to_f (Finite)", [u])
1.262 else
1.263 Kodkod.True
1.264 | Pos => formula_for_bool (not opt1)
1.265 @@ -992,7 +993,7 @@
1.266 if not (is_opt_rep ran_R) then
1.267 to_set_bool_op kk_implies kk_subset u1 u2
1.268 else if polar = Neut then
1.269 - raise NUT ("NitpickKodkod.to_f (Subset)", [u])
1.270 + raise NUT ("Nitpick_Kodkod.to_f (Subset)", [u])
1.271 else
1.272 let
1.273 (* bool -> nut -> Kodkod.rel_expr *)
1.274 @@ -1102,16 +1103,16 @@
1.275 | Op3 (If, _, _, u1, u2, u3) =>
1.276 kk_formula_if (to_f u1) (to_f u2) (to_f u3)
1.277 | FormulaReg (j, _, _) => Kodkod.FormulaReg j
1.278 - | _ => raise NUT ("NitpickKodkod.to_f", [u]))
1.279 + | _ => raise NUT ("Nitpick_Kodkod.to_f", [u]))
1.280 | Atom (2, j0) => formula_from_atom j0 (to_r u)
1.281 - | _ => raise NUT ("NitpickKodkod.to_f", [u])
1.282 + | _ => raise NUT ("Nitpick_Kodkod.to_f", [u])
1.283 (* polarity -> nut -> Kodkod.formula *)
1.284 and to_f_with_polarity polar u =
1.285 case rep_of u of
1.286 Formula _ => to_f u
1.287 | Atom (2, j0) => formula_from_atom j0 (to_r u)
1.288 | Opt (Atom (2, j0)) => formula_from_opt_atom polar j0 (to_r u)
1.289 - | _ => raise NUT ("NitpickKodkod.to_f_with_polarity", [u])
1.290 + | _ => raise NUT ("Nitpick_Kodkod.to_f_with_polarity", [u])
1.291 (* nut -> Kodkod.rel_expr *)
1.292 and to_r u =
1.293 case u of
1.294 @@ -1142,12 +1143,12 @@
1.295 | Cst (Num j, @{typ int}, R) =>
1.296 (case atom_for_int (card_of_rep R, offset_of_type ofs int_T) j of
1.297 ~1 => if is_opt_rep R then Kodkod.None
1.298 - else raise NUT ("NitpickKodkod.to_r (Num)", [u])
1.299 + else raise NUT ("Nitpick_Kodkod.to_r (Num)", [u])
1.300 | j' => Kodkod.Atom j')
1.301 | Cst (Num j, T, R) =>
1.302 if j < card_of_rep R then Kodkod.Atom (j + offset_of_type ofs T)
1.303 else if is_opt_rep R then Kodkod.None
1.304 - else raise NUT ("NitpickKodkod.to_r", [u])
1.305 + else raise NUT ("Nitpick_Kodkod.to_r", [u])
1.306 | Cst (Unknown, _, R) => empty_rel_for_rep R
1.307 | Cst (Unrep, _, R) => empty_rel_for_rep R
1.308 | Cst (Suc, T, Func (Atom x, _)) =>
1.309 @@ -1177,7 +1178,7 @@
1.310 (kk_product (Kodkod.AtomSeq (max_int_for_card int_k + 1, nat_j0))
1.311 Kodkod.Univ)
1.312 else
1.313 - raise BAD ("NitpickKodkod.to_r (NatToInt)", "\"nat_j0 <> int_j0\"")
1.314 + raise BAD ("Nitpick_Kodkod.to_r (NatToInt)", "\"nat_j0 <> int_j0\"")
1.315 | Cst (IntToNat, _, Func (Atom (int_k, int_j0), nat_R)) =>
1.316 let
1.317 val abs_card = max_int_for_card int_k + 1
1.318 @@ -1192,7 +1193,7 @@
1.319 (kk_product (Kodkod.AtomSeq (overlap, int_j0))
1.320 Kodkod.Univ))
1.321 else
1.322 - raise BAD ("NitpickKodkod.to_r (IntToNat)", "\"nat_j0 <> int_j0\"")
1.323 + raise BAD ("Nitpick_Kodkod.to_r (IntToNat)", "\"nat_j0 <> int_j0\"")
1.324 end
1.325 | Op1 (Not, _, R, u1) => kk_not3 (to_rep R u1)
1.326 | Op1 (Finite, _, Opt (Atom _), _) => Kodkod.None
1.327 @@ -1204,10 +1205,10 @@
1.328 Func (Struct [R1, R2], _) => (R1, R2)
1.329 | Func (R1, _) =>
1.330 if card_of_rep R1 <> 1 then
1.331 - raise REP ("NitpickKodkod.to_r (Converse)", [R])
1.332 + raise REP ("Nitpick_Kodkod.to_r (Converse)", [R])
1.333 else
1.334 pairself (Atom o pair 1 o offset_of_type ofs) (b_T, a_T)
1.335 - | _ => raise REP ("NitpickKodkod.to_r (Converse)", [R])
1.336 + | _ => raise REP ("Nitpick_Kodkod.to_r (Converse)", [R])
1.337 val body_R = body_rep R
1.338 val a_arity = arity_of_rep a_R
1.339 val b_arity = arity_of_rep b_R
1.340 @@ -1257,7 +1258,7 @@
1.341 (rel_expr_to_func kk R1 bool_atom_R
1.342 (Func (R1, Formula Neut)) r))
1.343 (to_opt R1 u1)
1.344 - | _ => raise NUT ("NitpickKodkod.to_r (SingletonSet)", [u]))
1.345 + | _ => raise NUT ("Nitpick_Kodkod.to_r (SingletonSet)", [u]))
1.346 | Op1 (Tha, T, R, u1) =>
1.347 if is_opt_rep R then
1.348 kk_join (to_rep (Func (unopt_rep R, Opt bool_atom_R)) u1) true_atom
1.349 @@ -1384,7 +1385,7 @@
1.350 kk_product (kk_join (do_nut r a_R b_R u2)
1.351 (do_nut r b_R c_R u1)) r
1.352 in kk_union (do_term true_atom) (do_term false_atom) end
1.353 - | _ => raise NUT ("NitpickKodkod.to_r (Composition)", [u]))
1.354 + | _ => raise NUT ("Nitpick_Kodkod.to_r (Composition)", [u]))
1.355 |> rel_expr_from_rel_expr kk R (Func (Struct [a_R, c_R], body_R))
1.356 end
1.357 | Op2 (Product, T, R, u1, u2) =>
1.358 @@ -1408,7 +1409,7 @@
1.359 fun do_term r =
1.360 kk_product (kk_product (do_nut r a_R u1) (do_nut r b_R u2)) r
1.361 in kk_union (do_term true_atom) (do_term false_atom) end
1.362 - | _ => raise NUT ("NitpickKodkod.to_r (Product)", [u]))
1.363 + | _ => raise NUT ("Nitpick_Kodkod.to_r (Product)", [u]))
1.364 |> rel_expr_from_rel_expr kk R (Func (Struct [a_R, b_R], body_R))
1.365 end
1.366 | Op2 (Image, T, R, u1, u2) =>
1.367 @@ -1437,8 +1438,8 @@
1.368 rel_expr_from_rel_expr kk R core_R core_r
1.369 end
1.370 else
1.371 - raise NUT ("NitpickKodkod.to_r (Image)", [u1, u2])
1.372 - | _ => raise NUT ("NitpickKodkod.to_r (Image)", [u1, u2]))
1.373 + raise NUT ("Nitpick_Kodkod.to_r (Image)", [u1, u2])
1.374 + | _ => raise NUT ("Nitpick_Kodkod.to_r (Image)", [u1, u2]))
1.375 | Op2 (Apply, @{typ nat}, _,
1.376 Op2 (Apply, _, _, Cst (Subtract, _, _), u1), u2) =>
1.377 if is_Cst Unrep u2 andalso not (is_opt_rep (rep_of u1)) then
1.378 @@ -1492,7 +1493,7 @@
1.379 | us' =>
1.380 kk_rel_if (kk_some (fold1 kk_product (map to_r us')))
1.381 (Kodkod.Atom j0) Kodkod.None)
1.382 - | _ => raise NUT ("NitpickKodkod.to_r (Tuple)", [u]))
1.383 + | _ => raise NUT ("Nitpick_Kodkod.to_r (Tuple)", [u]))
1.384 | Construct ([u'], _, _, []) => to_r u'
1.385 | Construct (_ :: sel_us, T, R, arg_us) =>
1.386 let
1.387 @@ -1516,23 +1517,23 @@
1.388 | BoundRel (x, _, _, _) => Kodkod.Var x
1.389 | FreeRel (x, _, _, _) => Kodkod.Rel x
1.390 | RelReg (j, _, R) => Kodkod.RelReg (arity_of_rep R, j)
1.391 - | u => raise NUT ("NitpickKodkod.to_r", [u])
1.392 + | u => raise NUT ("Nitpick_Kodkod.to_r", [u])
1.393 (* nut -> Kodkod.decl *)
1.394 and to_decl (BoundRel (x, _, R, _)) =
1.395 Kodkod.DeclOne (x, Kodkod.AtomSeq (the_single (atom_schema_of_rep R)))
1.396 - | to_decl u = raise NUT ("NitpickKodkod.to_decl", [u])
1.397 + | to_decl u = raise NUT ("Nitpick_Kodkod.to_decl", [u])
1.398 (* nut -> Kodkod.expr_assign *)
1.399 and to_expr_assign (FormulaReg (j, _, R)) u =
1.400 Kodkod.AssignFormulaReg (j, to_f u)
1.401 | to_expr_assign (RelReg (j, _, R)) u =
1.402 Kodkod.AssignRelReg ((arity_of_rep R, j), to_r u)
1.403 - | to_expr_assign u1 _ = raise NUT ("NitpickKodkod.to_expr_assign", [u1])
1.404 + | to_expr_assign u1 _ = raise NUT ("Nitpick_Kodkod.to_expr_assign", [u1])
1.405 (* int * int -> nut -> Kodkod.rel_expr *)
1.406 and to_atom (x as (k, j0)) u =
1.407 case rep_of u of
1.408 Formula _ => atom_from_formula kk j0 (to_f u)
1.409 | Unit => if k = 1 then Kodkod.Atom j0
1.410 - else raise NUT ("NitpickKodkod.to_atom", [u])
1.411 + else raise NUT ("Nitpick_Kodkod.to_atom", [u])
1.412 | R => atom_from_rel_expr kk x R (to_r u)
1.413 (* rep list -> nut -> Kodkod.rel_expr *)
1.414 and to_struct Rs u =
1.415 @@ -1563,7 +1564,7 @@
1.416 | to_rep (Vect (k, R)) u = to_vect k R u
1.417 | to_rep (Func (R1, R2)) u = to_func R1 R2 u
1.418 | to_rep (Opt R) u = to_opt R u
1.419 - | to_rep R _ = raise REP ("NitpickKodkod.to_rep", [R])
1.420 + | to_rep R _ = raise REP ("Nitpick_Kodkod.to_rep", [R])
1.421 (* nut -> Kodkod.rel_expr *)
1.422 and to_integer u = to_opt (one_rep ofs (type_of u) (rep_of u)) u
1.423 (* nut list -> rep -> Kodkod.rel_expr -> Kodkod.rel_expr *)
1.424 @@ -1593,7 +1594,7 @@
1.425 (* rep list -> nut list -> Kodkod.rel_expr *)
1.426 and to_product Rs us =
1.427 case map (uncurry to_opt) (filter (not_equal Unit o fst) (Rs ~~ us)) of
1.428 - [] => raise REP ("NitpickKodkod.to_product", Rs)
1.429 + [] => raise REP ("Nitpick_Kodkod.to_product", Rs)
1.430 | rs => fold1 kk_product rs
1.431 (* int -> typ -> rep -> nut -> Kodkod.rel_expr *)
1.432 and to_nth_pair_sel n res_T res_R u =
1.433 @@ -1639,7 +1640,7 @@
1.434 connective (formula_from_atom j0 r1) (formula_from_atom j0 r2)
1.435 | Func (R1, Atom _) => set_oper (kk_join r1 true_atom)
1.436 (kk_join r2 true_atom)
1.437 - | _ => raise REP ("NitpickKodkod.to_set_bool_op", [min_R])
1.438 + | _ => raise REP ("Nitpick_Kodkod.to_set_bool_op", [min_R])
1.439 end
1.440 (* (Kodkod.formula -> Kodkod.formula -> Kodkod.formula)
1.441 -> (Kodkod.rel_expr -> Kodkod.rel_expr -> Kodkod.rel_expr)
1.442 @@ -1676,7 +1677,7 @@
1.443 neg_second)))
1.444 false_atom))
1.445 r1 r2
1.446 - | _ => raise REP ("NitpickKodkod.to_set_op", [min_R]))
1.447 + | _ => raise REP ("Nitpick_Kodkod.to_set_op", [min_R]))
1.448 end
1.449 (* rep -> rep -> Kodkod.rel_expr -> nut -> Kodkod.rel_expr *)
1.450 and to_apply res_R func_u arg_u =
1.451 @@ -1713,7 +1714,7 @@
1.452 rel_expr_from_rel_expr kk res_R R2
1.453 (kk_n_fold_join kk true R1 R2 (to_opt R1 arg_u) (to_r func_u))
1.454 |> body_rep R2 = Formula Neut ? to_guard [arg_u] res_R
1.455 - | _ => raise NUT ("NitpickKodkod.to_apply", [func_u])
1.456 + | _ => raise NUT ("Nitpick_Kodkod.to_apply", [func_u])
1.457 (* int -> rep -> rep -> Kodkod.rel_expr -> nut *)
1.458 and to_apply_vect k R' res_R func_r arg_u =
1.459 let