# HG changeset patch # User blanchet # Date 1275394442 -7200 # Node ID 8a89fd40ed0bca963b39d4336db7f77acb8b9f33 # Parent dde817e6dfb1b779689409d428140e730a314197 honor xsymbols in Nitpick diff -r dde817e6dfb1 -r 8a89fd40ed0b src/HOL/Library/Multiset.thy --- a/src/HOL/Library/Multiset.thy Tue Jun 01 12:20:08 2010 +0200 +++ b/src/HOL/Library/Multiset.thy Tue Jun 01 14:14:02 2010 +0200 @@ -1711,7 +1711,8 @@ | NONE => [Const (maybe_name, elem_T --> elem_T) $ t] in case maps elems_for (all_values elem_T) @ - (if maybe_opt then [Const (Nitpick_Model.unrep, elem_T)] else []) of + (if maybe_opt then [Const (Nitpick_Model.unrep (), elem_T)] + else []) of [] => Const (@{const_name zero_class.zero}, T) | ts => foldl1 (fn (t1, t2) => Const (@{const_name plus_class.plus}, T --> T --> T) diff -r dde817e6dfb1 -r 8a89fd40ed0b src/HOL/Tools/Nitpick/nitpick_hol.ML --- a/src/HOL/Tools/Nitpick/nitpick_hol.ML Tue Jun 01 12:20:08 2010 +0200 +++ b/src/HOL/Tools/Nitpick/nitpick_hol.ML Tue Jun 01 14:14:02 2010 +0200 @@ -829,7 +829,7 @@ | eta_expand Ts (Abs (s, T, t')) n = Abs (s, T, eta_expand (T :: Ts) t' (n - 1)) | eta_expand Ts t n = - fold_rev (curry3 Abs ("x\<^isub>\" ^ nat_subscript n)) + fold_rev (curry3 Abs ("x" ^ nat_subscript n)) (List.take (binder_types (fastype_of1 (Ts, t)), n)) (list_comb (incr_boundvars n t, map Bound (n - 1 downto 0))) diff -r dde817e6dfb1 -r 8a89fd40ed0b src/HOL/Tools/Nitpick/nitpick_model.ML --- a/src/HOL/Tools/Nitpick/nitpick_model.ML Tue Jun 01 12:20:08 2010 +0200 +++ b/src/HOL/Tools/Nitpick/nitpick_model.ML Tue Jun 01 14:14:02 2010 +0200 @@ -23,7 +23,7 @@ val irrelevant : string val unknown : string - val unrep : string + val unrep : unit -> string val register_term_postprocessor : typ -> term_postprocessor -> theory -> theory val unregister_term_postprocessor : typ -> theory -> theory @@ -65,17 +65,19 @@ val extend = I fun merge (x, y) = AList.merge (op =) (K true) (x, y)) +fun xsym s s' () = if print_mode_active Symbol.xsymbolsN then s else s' + val irrelevant = "_" val unknown = "?" -val unrep = "\" -val maybe_mixfix = "_\<^sup>?" -val base_mixfix = "_\<^bsub>base\<^esub>" -val step_mixfix = "_\<^bsub>step\<^esub>" -val abs_mixfix = "\_\" +val unrep = xsym "\" "..." +val maybe_mixfix = xsym "_\<^sup>?" "_?" +val base_mixfix = xsym "_\<^bsub>base\<^esub>" "_.base" +val step_mixfix = xsym "_\<^bsub>step\<^esub>" "_.step" +val abs_mixfix = xsym "\_\" "\"_\"" val arg_var_prefix = "x" -val cyclic_co_val_name = "\" -val cyclic_const_prefix = "\" -val cyclic_type_name = nitpick_prefix ^ cyclic_const_prefix +val cyclic_co_val_name = xsym "\" "w" +val cyclic_const_prefix = xsym "\" "X" +fun cyclic_type_name () = nitpick_prefix ^ cyclic_const_prefix () val opt_flag = nitpick_prefix ^ "opt" val non_opt_flag = nitpick_prefix ^ "non_opt" @@ -87,16 +89,16 @@ val thy = ProofContext.theory_of ctxt |> Context.reject_draft val (maybe_t, thy) = Sign.declare_const ((@{binding nitpick_maybe}, @{typ "'a => 'a"}), - Mixfix (maybe_mixfix, [1000], 1000)) thy + Mixfix (maybe_mixfix (), [1000], 1000)) thy val (abs_t, thy) = Sign.declare_const ((@{binding nitpick_abs}, @{typ "'a => 'b"}), - Mixfix (abs_mixfix, [40], 40)) thy + Mixfix (abs_mixfix (), [40], 40)) thy val (base_t, thy) = Sign.declare_const ((@{binding nitpick_base}, @{typ "'a => 'a"}), - Mixfix (base_mixfix, [1000], 1000)) thy + Mixfix (base_mixfix (), [1000], 1000)) thy val (step_t, thy) = Sign.declare_const ((@{binding nitpick_step}, @{typ "'a => 'a"}), - Mixfix (step_mixfix, [1000], 1000)) thy + Mixfix (step_mixfix (), [1000], 1000)) thy in (pairself (pairself name_of) ((maybe_t, abs_t), (base_t, step_t)), ProofContext.transfer_syntax thy ctxt) @@ -322,7 +324,7 @@ in case term false of t as Const (s, _) => - if String.isPrefix cyclic_const_prefix s then + if String.isPrefix (cyclic_const_prefix ()) s then HOLogic.mk_eq (t, term true) else t @@ -367,7 +369,7 @@ T1 --> (T1 --> T2) --> T1 --> T2) fun aux [] = if maybe_opt andalso not (is_complete_type datatypes false T1) then - insert_const $ Const (unrep, T1) $ empty_const + insert_const $ Const (unrep (), T1) $ empty_const else empty_const | aux ((t1, t2) :: zs) = @@ -396,7 +398,7 @@ | _ => update_const $ aux' tps $ t1 $ t2) fun aux tps = if maybe_opt andalso not (is_complete_type datatypes false T1) then - update_const $ aux' tps $ Const (unrep, T1) + update_const $ aux' tps $ Const (unrep (), T1) $ (Const (@{const_name Some}, T2' --> T2) $ Const (unknown, T2')) else aux' tps @@ -491,7 +493,8 @@ fun tuples_for_const (s, T) = tuple_list_for_name rel_table bounds (ConstName (s, T, Any)) fun cyclic_atom () = - nth_atom thy atomss pool for_auto (Type (cyclic_type_name, [])) j + nth_atom thy atomss pool for_auto (Type (cyclic_type_name (), [])) + j fun cyclic_var () = Var ((nth_atom_name thy atomss pool "" T j, 0), T) val discr_jsss = map (tuples_for_const o discr_for_constr o #const) @@ -559,14 +562,15 @@ let val var = cyclic_var () in if unfold andalso not standard andalso length seen = 1 andalso - exists_subterm (fn Const (s, _) => - String.isPrefix cyclic_const_prefix s - | t' => t' = var) t then + exists_subterm + (fn Const (s, _) => + String.isPrefix (cyclic_const_prefix ()) s + | t' => t' = var) t then subst_atomic [(var, cyclic_atom ())] t else if exists_subterm (curry (op =) var) t then if co then Const (@{const_name The}, (T --> bool_T) --> T) - $ Abs (cyclic_co_val_name, T, + $ Abs (cyclic_co_val_name (), T, Const (@{const_name "op ="}, T --> T --> bool_T) $ Bound 0 $ abstract_over (var, t)) else @@ -814,9 +818,11 @@ fun assign_operator_for_const (s, T) = if String.isPrefix ubfp_prefix s then - if is_fun_type T then "\" else "\" + if is_fun_type T then xsym "\" "<=" () + else xsym "\" "<=" () else if String.isPrefix lbfp_prefix s then - if is_fun_type T then "\" else "\" + if is_fun_type T then xsym "\" ">=" () + else xsym "\" ">=" () else if original_name s <> s then assign_operator_for_const (strip_first_name_sep s |> snd, T) else @@ -891,7 +897,7 @@ let fun aux unfold = term_for_rep unfold T T (Atom (card, 0)) [[n]] in case aux false of t as Const (s, _) => - if String.isPrefix cyclic_const_prefix s then + if String.isPrefix (cyclic_const_prefix ()) s then HOLogic.mk_eq (t, aux true) else t @@ -944,7 +950,7 @@ Pretty.enum "," "{" "}" (map (Syntax.pretty_term ctxt) (all_values card typ) @ (if fun_from_pair complete false then [] - else [Pretty.str unrep]))])) + else [Pretty.str (unrep ())]))])) fun integer_datatype T = [{typ = T, card = card_of_type card_assigns T, co = false, standard = true, complete = (false, false), concrete = (true, true), diff -r dde817e6dfb1 -r 8a89fd40ed0b src/HOL/Tools/Nitpick/nitpick_util.ML --- a/src/HOL/Tools/Nitpick/nitpick_util.ML Tue Jun 01 12:20:08 2010 +0200 +++ b/src/HOL/Tools/Nitpick/nitpick_util.ML Tue Jun 01 14:14:02 2010 +0200 @@ -244,12 +244,17 @@ val monomorphic_term = Sledgehammer_Util.monomorphic_term val specialize_type = Sledgehammer_Util.specialize_type -val subscript = implode o map (prefix "\<^isub>") o explode +val i_subscript = implode o map (prefix "\<^isub>") o explode +fun be_subscript s = "\<^bsub>" ^ s ^ "\<^esub>" fun nat_subscript n = - (* cheap trick to ensure proper alphanumeric ordering for one- and two-digit - numbers *) - if n <= 9 then "\<^bsub>" ^ signed_string_of_int n ^ "\<^esub>" - else subscript (string_of_int n) + let val s = signed_string_of_int n in + if print_mode_active Symbol.xsymbolsN then + (* cheap trick to ensure proper alphanumeric ordering for one- and + two-digit numbers *) + (if n <= 9 then be_subscript else i_subscript) s + else + s + end fun time_limit NONE = I | time_limit (SOME delay) = TimeLimit.timeLimit delay