wneuper/isa: comparison src/HOL/Tools/Nitpick/nitpick

equal deleted inserted replaced

-:1711610c5b7d
+:f93390060bbe
 Model reconstruction for Nitpick.
 *)
 signature NITPICK_MODEL =
 sig
-type scope = NitpickScope.scope
+type scope = Nitpick_Scope.scope
-type rep = NitpickRep.rep
+type rep = Nitpick_Rep.rep
-type nut = NitpickNut.nut
+type nut = Nitpick_Nut.nut
 type params = {
 show_skolems: bool,
 show_datatypes: bool,
 show_consts: bool}
 val prove_hol_model :
 scope -> Time.time option -> nut list -> nut list -> nut NameTable.table
 -> Kodkod.raw_bound list -> term -> bool option
 end;
-structure NitpickModel : NITPICK_MODEL =
+structure Nitpick_Model : NITPICK_MODEL =
 struct
-open NitpickUtil
+open Nitpick_Util
-open NitpickHOL
+open Nitpick_HOL
-open NitpickScope
+open Nitpick_Scope
-open NitpickPeephole
+open Nitpick_Peephole
-open NitpickRep
+open Nitpick_Rep
-open NitpickNut
+open Nitpick_Nut
 type params = {
 show_skolems: bool,
 show_datatypes: bool,
 show_consts: bool}
 (* string -> typ -> int -> string *)
 fun atom_name prefix (T as Type (s, _)) j =
 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
 Free (atom_name (hd (space_explode "." nitpick_prefix)) T j, T)
 else
 let
 (* term -> term list * term list *)
 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 *)
 fun break_in_two (Type ("*", [T1, T2]))
 (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},
 Type ("fun", [_, Type ("fun", [_, T1])])) $ t11 $ t12)
 t2 =
 (Const (@{const_name fun_upd}, _) $ t0 $ t1 $ t2) =
 Const (@{const_name fun_upd},
 [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
 | ((_, NONE), (T1a, SOME T1b)) =>
 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
 | do_term (T' as Type ("*", Ts' as [T1', T2'])) (Type ("*", [T1, T2]))
 (Const (@{const_name Pair}, _) $ t1 $ t2) =
 Const (@{const_name Pair}, Ts' ---> T')
 $ 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"
 | truth_const_sort_key @{const False} = "2"
 | truth_const_sort_key _ = "1"
 val k2 = card_of_type card_assigns T2
 in
 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
 | term_for_atom seen (Type ("*", [T1, T2])) _ j =
 let val k1 = card_of_type card_assigns T1 in
 (index_seq 0 (length arg_Ts))
 val sel_Rs =
 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
 val sel_jsss = map tuples_for_const sel_xs
 val arg_jsss =
 | n1 => case HOLogic.dest_number t2 |> snd of
 1 => mk_num n1
 | 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
 Const (abs_name, constr_T) $ the_single ts
 else
 (batch_list (arity_of_rep R) js))
 (* (typ * int) list -> typ -> typ -> rep -> int list list -> term *)
 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
 val (js1, js2) = chop arity1 js
 in
 o AList.lookup (op =) grouped_jss2) jss1
 in make_fun true T1 T2 T' ts1 ts2 end
 | 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
 (not for_auto ? setify_mapify_funs []) o unbox_term oooo term_for_rep []
 end
 end
 | ConstName (s, T, _) =>
 (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')
 else
 tuple_list_for_name rel_table bounds name
 (if precise then [] else [Pretty.str unrep]))])
 (* typ -> dtype_spec list *)
 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)
 val block_of_datatypes =
 if show_datatypes andalso not (null datatypes) then
 map (fn x as (s, T) =>
 case filter (equal x o nickname_of pairf (unbox_type o type_of))
 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 @
 block_of_names true "Evaluated term" eval_names @
 block_of_datatypes @ block_of_codatatypes @

changeset 33224	f93390060bbe
parent 33202	0183ab3ca7b4
child 33549	a2db56854b83