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

equal deleted inserted replaced

-:475aef44d5fb
+:7b8c366e34a2
 (*  Title:      HOL/Tools/Nitpick/nitpick_model.ML
 Author:     Jasmin Blanchette, TU Muenchen
-Copyright   2009
+Copyright   2009, 2010
 Model reconstruction for Nitpick.
 *)
 signature NITPICK_MODEL =
 val unrep = "\<dots>"
 val maybe_mixfix = "_\<^sup>?"
 val base_mixfix = "_\<^bsub>base\<^esub>"
 val step_mixfix = "_\<^bsub>step\<^esub>"
 val abs_mixfix = "\<guillemotleft>_\<guillemotright>"
-val non_opt_name = nitpick_prefix ^ "non_opt"
+val opt_flag = nitpick_prefix ^ "opt"
+val non_opt_flag = nitpick_prefix ^ "non_opt"
 (* string -> int -> string *)
 fun atom_suffix s j =
 nat_subscript (j + 1)
 |> (s <> "" andalso Symbol.is_ascii_digit (List.last (explode s)))
 ? prefix "\<^isub>,"
 (* string -> typ -> int -> string *)
 fun atom_name prefix (T as Type (s, _)) j =
-prefix ^ substring (shortest_name s, 0, 1) ^ atom_suffix s j
+let val s' = shortest_name s in
+prefix ^ (if String.isPrefix "\\" s' then s' else substring (s', 0, 1)) ^
+atom_suffix s j
+end
 | atom_name prefix (T as TFree (s, _)) j =
 prefix ^ perhaps (try (unprefix "'")) s ^ atom_suffix s j
 | atom_name _ T _ = raise TYPE ("Nitpick_Model.atom_name", [T], [])
 (* bool -> typ -> int -> term *)
 fun atom for_auto T j =
 (* bool -> typ -> typ -> (term * term) list -> term *)
 fun make_plain_fun maybe_opt T1 T2 =
 let
 (* typ -> typ -> (term * term) list -> term *)
 fun aux T1 T2 [] =
-Const (if maybe_opt orelse T2 <> bool_T then @{const_name undefined}
+Const (if maybe_opt then opt_flag else non_opt_flag, T1 --> T2)
-else non_opt_name, T1 --> T2)
 | aux T1 T2 ((t1, t2) :: ps) =
 Const (@{const_name fun_upd}, (T1 --> T2) --> T1 --> T2 --> T1 --> T2)
 $ aux T1 T2 ps $ t1 $ t2
 in aux T1 T2 o rev end
 (* term -> bool *)
-fun is_plain_fun (Const (s, _)) =
+fun is_plain_fun (Const (s, _)) = (s = opt_flag orelse s = non_opt_flag)
-(s = @{const_name undefined} orelse s = non_opt_name)
 | is_plain_fun (Const (@{const_name fun_upd}, _) $ t0 $ _ $ _) =
 is_plain_fun t0
 | is_plain_fun _ = false
 (* term -> bool * (term list * term list) *)
 val dest_plain_fun =
 let
-(* term -> term list * term list *)
+(* term -> bool * (term list * term list) *)
-fun aux (Const (s, _)) = (s <> non_opt_name, ([], []))
+fun aux (Const (s, _)) = (s <> non_opt_flag, ([], []))
 | 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 ("Nitpick_Model.dest_plain_fun", [t])
 in apsnd (pairself rev) o aux end
 $ (Const (@{const_name Some}, T2' --> T2) $ Const (unknown, T2'))
 else
 aux' ps
 in aux end
 (* typ list -> term -> term *)
-fun setify_mapify_funs Ts t =
+fun polish_funs Ts t =
 (case fastype_of1 (Ts, t) of
 Type ("fun", [T1, T2]) =>
 if is_plain_fun t then
 case T2 of
 @{typ bool} =>
 let
 val (maybe_opt, ts_pair) =
-dest_plain_fun t ||> pairself (map (setify_mapify_funs Ts))
+dest_plain_fun t ||> pairself (map (polish_funs Ts))
 in
 make_set maybe_opt T1 T2
 (sort_wrt (truth_const_sort_key o snd) (op ~~ ts_pair))
 end
 | Type (@{type_name option}, [T2']) =>
 let
 val ts_pair = snd (dest_plain_fun t)
-|> pairself (map (setify_mapify_funs Ts))
+|> pairself (map (polish_funs Ts))
 in make_map T1 T2 T2' (rev (op ~~ ts_pair)) end
 | _ => raise SAME ()
 else
 raise SAME ()
 | _ => raise SAME ())
 handle SAME () =>
 case t of
-t1 $ t2 => setify_mapify_funs Ts t1 $ setify_mapify_funs Ts t2
+(t1 as Const (@{const_name fun_upd}, _) $ t11 $ _)
-| Abs (s, T, t') => Abs (s, T, setify_mapify_funs (T :: Ts) t')
+$ (t2 as Const (s, _)) =>
-| _ => t
+if s = unknown then polish_funs Ts t11
+else polish_funs Ts t1 $ polish_funs Ts t2
+| t1 $ t2 => polish_funs Ts t1 $ polish_funs Ts t2
+| Abs (s, T, t') => Abs (s, T, polish_funs (T :: Ts) t')
+| Const (s, Type ("fun", [T1, T2])) =>
+if s = opt_flag orelse s = non_opt_flag then
+Abs ("x", T1, Const (unknown, T2))
+else
+t
+| t => t
 (* bool -> typ -> typ -> typ -> term list -> term list -> term *)
 fun make_fun maybe_opt T1 T2 T' ts1 ts2 =
 ts1 ~~ ts2 |> sort (nice_term_ord o pairself fst)
 |> make_plain_fun (maybe_opt andalso not for_auto) T1 T2
 |> unbit_and_unbox_term
 HOLogic.mk_number nat_T (card_of_type card_assigns T - j - 1)
 else if T = @{typ bisim_iterator} then
 HOLogic.mk_number nat_T j
 else case datatype_spec datatypes T of
 NONE => atom for_auto T j
-| SOME {shallow = true, ...} => atom for_auto T j
+| SOME {deep = false, ...} => atom for_auto T j
 | SOME {co, constrs, ...} =>
 let
 (* styp -> int list *)
 fun tuples_for_const (s, T) =
 tuple_list_for_name rel_table bounds (ConstName (s, T, Any))
 | n1 => case HOLogic.dest_number t2 |> snd of
 1 => mk_num n1
 | n2 => Const (@{const_name Algebras.divide},
 num_T --> num_T --> num_T)
 $ mk_num n1 $ mk_num n2)
-| _ => raise TERM ("Nitpick_Model.reconstruct_term.term_\
+| _ => raise TERM ("Nitpick_Model.reconstruct_term.\
-\for_atom (Abs_Frac)", ts)
+\term_for_atom (Abs_Frac)", ts)
 end
 else if not for_auto andalso
 (is_abs_fun thy constr_x orelse
 constr_s = @{const_name Quot}) then
 Const (abs_name, constr_T) $ the_single ts
+else if not for_auto andalso
+constr_s = @{const_name NonStd} then
+Const (fst (dest_Const (the_single ts)), T)
 else
 list_comb (Const constr_x, ts)
 in
 if co then
 let val var = var () in
 | term_for_rep seen T _ R jss =
 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 unbit_and_unbox_term
+(not for_auto ? polish_funs []) o unbit_and_unbox_term oooo term_for_rep []
-oooo term_for_rep []
 end
 (* scope -> nut list -> nut NameTable.table -> KK.raw_bound list -> nut
 -> term *)
 fun term_for_name scope sel_names rel_table bounds name =
 tuple_list_for_name rel_table bounds name
 |> reconstruct_term ("", "", "", "") scope sel_names rel_table bounds T T
 (rep_of name)
 end
-(* Proof.context
+(* Proof.context -> (string * string * string * string) * Proof.context *)
--> (string * string * string * string * string) * Proof.context *)
 fun add_wacky_syntax ctxt =
 let
 (* term -> string *)
 val name_of = fst o dest_Const
 val thy = ProofContext.theory_of ctxt |> Context.reject_draft
 (* params -> scope -> (term option * int list) list -> styp list -> nut list
 -> nut list -> nut list -> nut NameTable.table -> KK.raw_bound list
 -> Pretty.T * bool *)
 fun reconstruct_hol_model {show_skolems, show_datatypes, show_consts}
-({ext_ctxt as {thy, ctxt, max_bisim_depth, boxes, wfs, user_axioms,
+({ext_ctxt as {thy, ctxt, max_bisim_depth, boxes, stds, wfs,
-debug, binary_ints, destroy_constrs, specialize,
+user_axioms, debug, binary_ints, destroy_constrs,
-skolemize, star_linear_preds, uncurry, fast_descrs,
+specialize, skolemize, star_linear_preds, uncurry,
-tac_timeout, evals, case_names, def_table, nondef_table,
+fast_descrs, tac_timeout, evals, case_names, def_table,
-user_nondefs, simp_table, psimp_table, intro_table,
+nondef_table, user_nondefs, simp_table, psimp_table,
-ground_thm_table, ersatz_table, skolems, special_funs,
+intro_table, ground_thm_table, ersatz_table, skolems,
-unrolled_preds, wf_cache, constr_cache},
+special_funs, unrolled_preds, wf_cache, constr_cache},
 card_assigns, bits, bisim_depth, datatypes, ofs} : scope)
 formats all_frees free_names sel_names nonsel_names rel_table bounds =
 let
 val (wacky_names as (_, base_name, step_name, _), ctxt) =
 add_wacky_syntax ctxt
 val ext_ctxt =
 {thy = thy, ctxt = ctxt, max_bisim_depth = max_bisim_depth, boxes = boxes,
-wfs = wfs, user_axioms = user_axioms, debug = debug,
+stds = stds, wfs = wfs, user_axioms = user_axioms, debug = debug,
 binary_ints = binary_ints, destroy_constrs = destroy_constrs,
 specialize = specialize, skolemize = skolemize,
 star_linear_preds = star_linear_preds, uncurry = uncurry,
 fast_descrs = fast_descrs, tac_timeout = tac_timeout, evals = evals,
 case_names = case_names, def_table = def_table,
 (* dtype_spec -> Pretty.T *)
 fun pretty_for_datatype ({typ, card, complete, ...} : dtype_spec) =
 Pretty.block (Pretty.breaks
 [Syntax.pretty_typ ctxt (unbit_and_unbox_type typ), Pretty.str "=",
 Pretty.enum "," "{" "}"
-(map (Syntax.pretty_term ctxt) (all_values_of_type card typ)
+(map (Syntax.pretty_term ctxt) (all_values_of_type card typ) @
-@ (if complete then [] else [Pretty.str unrep]))])
+(if complete then [] else [Pretty.str unrep]))])
 (* typ -> dtype_spec list *)
 fun integer_datatype T =
 [{typ = T, card = card_of_type card_assigns T, co = false,
-complete = false, concrete = true, shallow = false, constrs = []}]
+complete = false, concrete = true, deep = true, constrs = []}]
 handle TYPE ("Nitpick_HOL.card_of_type", _, _) => []
 val (codatatypes, datatypes) =
-datatypes |> filter_out #shallow
+datatypes |> filter #deep |> List.partition #co
-|> List.partition #co
 ||> append (integer_datatype nat_T @ integer_datatype int_T)
 val block_of_datatypes =
 if show_datatypes andalso not (null datatypes) then
 [Pretty.big_list ("Datatype" ^ plural_s_for_list datatypes ^ ":")
 (map pretty_for_datatype datatypes)]

changeset 34969	7b8c366e34a2
parent 34961	18b41bba42b5
child 34985	5e492a862b34