1.1 --- a/src/HOL/Tools/Nitpick/nitpick_model.ML Mon Feb 01 14:12:12 2010 +0100
1.2 +++ b/src/HOL/Tools/Nitpick/nitpick_model.ML Tue Feb 02 11:38:38 2010 +0100
1.3 @@ -1,6 +1,6 @@
1.4 (* Title: HOL/Tools/Nitpick/nitpick_model.ML
1.5 Author: Jasmin Blanchette, TU Muenchen
1.6 - Copyright 2009
1.7 + Copyright 2009, 2010
1.8
1.9 Model reconstruction for Nitpick.
1.10 *)
1.11 @@ -53,7 +53,8 @@
1.12 val base_mixfix = "_\<^bsub>base\<^esub>"
1.13 val step_mixfix = "_\<^bsub>step\<^esub>"
1.14 val abs_mixfix = "\<guillemotleft>_\<guillemotright>"
1.15 -val non_opt_name = nitpick_prefix ^ "non_opt"
1.16 +val opt_flag = nitpick_prefix ^ "opt"
1.17 +val non_opt_flag = nitpick_prefix ^ "non_opt"
1.18
1.19 (* string -> int -> string *)
1.20 fun atom_suffix s j =
1.21 @@ -62,7 +63,10 @@
1.22 ? prefix "\<^isub>,"
1.23 (* string -> typ -> int -> string *)
1.24 fun atom_name prefix (T as Type (s, _)) j =
1.25 - prefix ^ substring (shortest_name s, 0, 1) ^ atom_suffix s j
1.26 + let val s' = shortest_name s in
1.27 + prefix ^ (if String.isPrefix "\\" s' then s' else substring (s', 0, 1)) ^
1.28 + atom_suffix s j
1.29 + end
1.30 | atom_name prefix (T as TFree (s, _)) j =
1.31 prefix ^ perhaps (try (unprefix "'")) s ^ atom_suffix s j
1.32 | atom_name _ T _ = raise TYPE ("Nitpick_Model.atom_name", [T], [])
1.33 @@ -139,23 +143,21 @@
1.34 let
1.35 (* typ -> typ -> (term * term) list -> term *)
1.36 fun aux T1 T2 [] =
1.37 - Const (if maybe_opt orelse T2 <> bool_T then @{const_name undefined}
1.38 - else non_opt_name, T1 --> T2)
1.39 + Const (if maybe_opt then opt_flag else non_opt_flag, T1 --> T2)
1.40 | aux T1 T2 ((t1, t2) :: ps) =
1.41 Const (@{const_name fun_upd}, (T1 --> T2) --> T1 --> T2 --> T1 --> T2)
1.42 $ aux T1 T2 ps $ t1 $ t2
1.43 in aux T1 T2 o rev end
1.44 (* term -> bool *)
1.45 -fun is_plain_fun (Const (s, _)) =
1.46 - (s = @{const_name undefined} orelse s = non_opt_name)
1.47 +fun is_plain_fun (Const (s, _)) = (s = opt_flag orelse s = non_opt_flag)
1.48 | is_plain_fun (Const (@{const_name fun_upd}, _) $ t0 $ _ $ _) =
1.49 is_plain_fun t0
1.50 | is_plain_fun _ = false
1.51 (* term -> bool * (term list * term list) *)
1.52 val dest_plain_fun =
1.53 let
1.54 - (* term -> term list * term list *)
1.55 - fun aux (Const (s, _)) = (s <> non_opt_name, ([], []))
1.56 + (* term -> bool * (term list * term list) *)
1.57 + fun aux (Const (s, _)) = (s <> non_opt_flag, ([], []))
1.58 | aux (Const (@{const_name fun_upd}, _) $ t0 $ t1 $ t2) =
1.59 let val (s, (ts1, ts2)) = aux t0 in (s, (t1 :: ts1, t2 :: ts2)) end
1.60 | aux t = raise TERM ("Nitpick_Model.dest_plain_fun", [t])
1.61 @@ -300,7 +302,7 @@
1.62 aux' ps
1.63 in aux end
1.64 (* typ list -> term -> term *)
1.65 - fun setify_mapify_funs Ts t =
1.66 + fun polish_funs Ts t =
1.67 (case fastype_of1 (Ts, t) of
1.68 Type ("fun", [T1, T2]) =>
1.69 if is_plain_fun t then
1.70 @@ -308,7 +310,7 @@
1.71 @{typ bool} =>
1.72 let
1.73 val (maybe_opt, ts_pair) =
1.74 - dest_plain_fun t ||> pairself (map (setify_mapify_funs Ts))
1.75 + dest_plain_fun t ||> pairself (map (polish_funs Ts))
1.76 in
1.77 make_set maybe_opt T1 T2
1.78 (sort_wrt (truth_const_sort_key o snd) (op ~~ ts_pair))
1.79 @@ -316,7 +318,7 @@
1.80 | Type (@{type_name option}, [T2']) =>
1.81 let
1.82 val ts_pair = snd (dest_plain_fun t)
1.83 - |> pairself (map (setify_mapify_funs Ts))
1.84 + |> pairself (map (polish_funs Ts))
1.85 in make_map T1 T2 T2' (rev (op ~~ ts_pair)) end
1.86 | _ => raise SAME ()
1.87 else
1.88 @@ -324,9 +326,18 @@
1.89 | _ => raise SAME ())
1.90 handle SAME () =>
1.91 case t of
1.92 - t1 $ t2 => setify_mapify_funs Ts t1 $ setify_mapify_funs Ts t2
1.93 - | Abs (s, T, t') => Abs (s, T, setify_mapify_funs (T :: Ts) t')
1.94 - | _ => t
1.95 + (t1 as Const (@{const_name fun_upd}, _) $ t11 $ _)
1.96 + $ (t2 as Const (s, _)) =>
1.97 + if s = unknown then polish_funs Ts t11
1.98 + else polish_funs Ts t1 $ polish_funs Ts t2
1.99 + | t1 $ t2 => polish_funs Ts t1 $ polish_funs Ts t2
1.100 + | Abs (s, T, t') => Abs (s, T, polish_funs (T :: Ts) t')
1.101 + | Const (s, Type ("fun", [T1, T2])) =>
1.102 + if s = opt_flag orelse s = non_opt_flag then
1.103 + Abs ("x", T1, Const (unknown, T2))
1.104 + else
1.105 + t
1.106 + | t => t
1.107 (* bool -> typ -> typ -> typ -> term list -> term list -> term *)
1.108 fun make_fun maybe_opt T1 T2 T' ts1 ts2 =
1.109 ts1 ~~ ts2 |> sort (nice_term_ord o pairself fst)
1.110 @@ -371,7 +382,7 @@
1.111 HOLogic.mk_number nat_T j
1.112 else case datatype_spec datatypes T of
1.113 NONE => atom for_auto T j
1.114 - | SOME {shallow = true, ...} => atom for_auto T j
1.115 + | SOME {deep = false, ...} => atom for_auto T j
1.116 | SOME {co, constrs, ...} =>
1.117 let
1.118 (* styp -> int list *)
1.119 @@ -437,13 +448,16 @@
1.120 | n2 => Const (@{const_name Algebras.divide},
1.121 num_T --> num_T --> num_T)
1.122 $ mk_num n1 $ mk_num n2)
1.123 - | _ => raise TERM ("Nitpick_Model.reconstruct_term.term_\
1.124 - \for_atom (Abs_Frac)", ts)
1.125 + | _ => raise TERM ("Nitpick_Model.reconstruct_term.\
1.126 + \term_for_atom (Abs_Frac)", ts)
1.127 end
1.128 else if not for_auto andalso
1.129 (is_abs_fun thy constr_x orelse
1.130 constr_s = @{const_name Quot}) then
1.131 Const (abs_name, constr_T) $ the_single ts
1.132 + else if not for_auto andalso
1.133 + constr_s = @{const_name NonStd} then
1.134 + Const (fst (dest_Const (the_single ts)), T)
1.135 else
1.136 list_comb (Const constr_x, ts)
1.137 in
1.138 @@ -509,8 +523,7 @@
1.139 Refute.string_of_typ T ^ " " ^ string_for_rep R ^ " " ^
1.140 string_of_int (length jss))
1.141 in
1.142 - (not for_auto ? setify_mapify_funs []) o unbit_and_unbox_term
1.143 - oooo term_for_rep []
1.144 + (not for_auto ? polish_funs []) o unbit_and_unbox_term oooo term_for_rep []
1.145 end
1.146
1.147 (* scope -> nut list -> nut NameTable.table -> KK.raw_bound list -> nut
1.148 @@ -522,8 +535,7 @@
1.149 (rep_of name)
1.150 end
1.151
1.152 -(* Proof.context
1.153 - -> (string * string * string * string * string) * Proof.context *)
1.154 +(* Proof.context -> (string * string * string * string) * Proof.context *)
1.155 fun add_wacky_syntax ctxt =
1.156 let
1.157 (* term -> string *)
1.158 @@ -573,13 +585,13 @@
1.159 -> nut list -> nut list -> nut NameTable.table -> KK.raw_bound list
1.160 -> Pretty.T * bool *)
1.161 fun reconstruct_hol_model {show_skolems, show_datatypes, show_consts}
1.162 - ({ext_ctxt as {thy, ctxt, max_bisim_depth, boxes, wfs, user_axioms,
1.163 - debug, binary_ints, destroy_constrs, specialize,
1.164 - skolemize, star_linear_preds, uncurry, fast_descrs,
1.165 - tac_timeout, evals, case_names, def_table, nondef_table,
1.166 - user_nondefs, simp_table, psimp_table, intro_table,
1.167 - ground_thm_table, ersatz_table, skolems, special_funs,
1.168 - unrolled_preds, wf_cache, constr_cache},
1.169 + ({ext_ctxt as {thy, ctxt, max_bisim_depth, boxes, stds, wfs,
1.170 + user_axioms, debug, binary_ints, destroy_constrs,
1.171 + specialize, skolemize, star_linear_preds, uncurry,
1.172 + fast_descrs, tac_timeout, evals, case_names, def_table,
1.173 + nondef_table, user_nondefs, simp_table, psimp_table,
1.174 + intro_table, ground_thm_table, ersatz_table, skolems,
1.175 + special_funs, unrolled_preds, wf_cache, constr_cache},
1.176 card_assigns, bits, bisim_depth, datatypes, ofs} : scope)
1.177 formats all_frees free_names sel_names nonsel_names rel_table bounds =
1.178 let
1.179 @@ -587,7 +599,7 @@
1.180 add_wacky_syntax ctxt
1.181 val ext_ctxt =
1.182 {thy = thy, ctxt = ctxt, max_bisim_depth = max_bisim_depth, boxes = boxes,
1.183 - wfs = wfs, user_axioms = user_axioms, debug = debug,
1.184 + stds = stds, wfs = wfs, user_axioms = user_axioms, debug = debug,
1.185 binary_ints = binary_ints, destroy_constrs = destroy_constrs,
1.186 specialize = specialize, skolemize = skolemize,
1.187 star_linear_preds = star_linear_preds, uncurry = uncurry,
1.188 @@ -650,16 +662,15 @@
1.189 Pretty.block (Pretty.breaks
1.190 [Syntax.pretty_typ ctxt (unbit_and_unbox_type typ), Pretty.str "=",
1.191 Pretty.enum "," "{" "}"
1.192 - (map (Syntax.pretty_term ctxt) (all_values_of_type card typ)
1.193 - @ (if complete then [] else [Pretty.str unrep]))])
1.194 + (map (Syntax.pretty_term ctxt) (all_values_of_type card typ) @
1.195 + (if complete then [] else [Pretty.str unrep]))])
1.196 (* typ -> dtype_spec list *)
1.197 fun integer_datatype T =
1.198 [{typ = T, card = card_of_type card_assigns T, co = false,
1.199 - complete = false, concrete = true, shallow = false, constrs = []}]
1.200 + complete = false, concrete = true, deep = true, constrs = []}]
1.201 handle TYPE ("Nitpick_HOL.card_of_type", _, _) => []
1.202 val (codatatypes, datatypes) =
1.203 - datatypes |> filter_out #shallow
1.204 - |> List.partition #co
1.205 + datatypes |> filter #deep |> List.partition #co
1.206 ||> append (integer_datatype nat_T @ integer_datatype int_T)
1.207 val block_of_datatypes =
1.208 if show_datatypes andalso not (null datatypes) then