# HG changeset patch # User blanchet # Date 1392190556 -3600 # Node ID 54b09e82b9e1f8841aeb641e66432fd7a3fc0f74 # Parent b742489618193243ff15e1fb14f95e03c26002f3 killed 'rep_compat' option diff -r b74248961819 -r 54b09e82b9e1 src/Doc/Datatypes/Datatypes.thy --- a/src/Doc/Datatypes/Datatypes.thy Wed Feb 12 08:35:56 2014 +0100 +++ b/src/Doc/Datatypes/Datatypes.thy Wed Feb 12 08:35:56 2014 +0100 @@ -470,7 +470,7 @@ @@{command datatype_new} target? @{syntax dt_options}? \ (@{syntax dt_name} '=' (@{syntax ctor} + '|') + @'and') ; - @{syntax_def dt_options}: '(' (('no_discs_sels' | 'no_code' | 'rep_compat') + ',') ')' + @{syntax_def dt_options}: '(' (('no_discs_sels' | 'no_code') + ',') ')' \} \medskip @@ -492,12 +492,6 @@ \item The @{text "no_code"} option indicates that the datatype should not be registered for code generation. - -\item -The @{text "rep_compat"} option indicates that the generated names should -contain optional (and normally not displayed) ``@{text "new."}'' components to -prevent clashes with a later call to \keyw{rep\_datatype}. See -Section~\ref{ssec:datatype-compatibility-issues} for details. \end{itemize} The left-hand sides of the datatype equations specify the name of the type to @@ -2563,7 +2557,7 @@ % old \keyw{datatype} % % * @{command wrap_free_constructors} -% * @{text "no_discs_sels"}, @{text "no_code"}, @{text "rep_compat"} +% * @{text "no_discs_sels"}, @{text "no_code"} % * hack to have both co and nonco view via locale (cf. ext nats) % * code generator % * eq, refl, simps @@ -2601,7 +2595,7 @@ \medskip -% options: no_discs_sels no_code rep_compat +% options: no_discs_sels no_code \noindent Section~\ref{ssec:datatype-generated-theorems} lists the generated theorems. diff -r b74248961819 -r 54b09e82b9e1 src/HOL/Tools/BNF/bnf_fp_def_sugar.ML --- a/src/HOL/Tools/BNF/bnf_fp_def_sugar.ML Wed Feb 12 08:35:56 2014 +0100 +++ b/src/HOL/Tools/BNF/bnf_fp_def_sugar.ML Wed Feb 12 08:35:56 2014 +0100 @@ -95,7 +95,7 @@ val co_datatypes: BNF_FP_Util.fp_kind -> (mixfix list -> binding list -> binding list -> binding list list -> binding list -> (string * sort) list -> typ list * typ list list -> BNF_Def.bnf list -> local_theory -> BNF_FP_Util.fp_result * local_theory) -> - (bool * (bool * bool)) * (((((binding * (typ * sort)) list * binding) * (binding * binding)) + (bool * bool) * (((((binding * (typ * sort)) list * binding) * (binding * binding)) * mixfix) * ((((binding * binding) * (binding * typ) list) * (binding * term) list) * mixfix) list) list -> local_theory -> local_theory @@ -978,7 +978,7 @@ end; fun define_co_datatypes prepare_constraint prepare_typ prepare_term fp construct_fp - (wrap_opts as (no_discs_sels, (_, rep_compat)), specs) no_defs_lthy0 = + (wrap_opts as (no_discs_sels, _), specs) no_defs_lthy0 = let (* TODO: sanity checks on arguments *) @@ -987,9 +987,6 @@ else (); - fun qualify mandatory fp_b_name = - Binding.qualify mandatory fp_b_name o (rep_compat ? Binding.qualify false rep_compat_prefix); - val nn = length specs; val fp_bs = map type_binding_of specs; val fp_b_names = map Binding.name_of fp_bs; @@ -1041,7 +1038,7 @@ val disc_bindingss = map (map disc_of) ctr_specss; val ctr_bindingss = - map2 (fn fp_b_name => map (qualify false fp_b_name o ctr_of)) fp_b_names ctr_specss; + map2 (fn fp_b_name => map (Binding.qualify false fp_b_name o ctr_of)) fp_b_names ctr_specss; val ctr_argsss = map (map args_of) ctr_specss; val ctr_mixfixess = map (map ctr_mixfix_of) ctr_specss; @@ -1150,12 +1147,12 @@ fun massage_simple_notes base = filter_out (null o #2) #> map (fn (thmN, thms, attrs) => - ((qualify true base (Binding.name thmN), attrs), [(thms, [])])); + ((Binding.qualify true base (Binding.name thmN), attrs), [(thms, [])])); val massage_multi_notes = maps (fn (thmN, thmss, attrs) => map3 (fn fp_b_name => fn Type (T_name, _) => fn thms => - ((qualify true fp_b_name (Binding.name thmN), attrs T_name), [(thms, [])])) + ((Binding.qualify true fp_b_name (Binding.name thmN), attrs T_name), [(thms, [])])) fp_b_names fpTs thmss) #> filter_out (null o fst o hd o snd); @@ -1346,7 +1343,7 @@ lthy |> Local_Theory.notes (anonymous_notes @ notes) |> snd) end; - fun mk_binding pre = qualify false fp_b_name (Binding.prefix_name (pre ^ "_") fp_b); + fun mk_binding pre = Binding.qualify false fp_b_name (Binding.prefix_name (pre ^ "_") fp_b); fun massage_res (((maps_sets_rels, ctr_sugar), co_iter_res), lthy) = (((maps_sets_rels, (ctrs, xss, ctr_defs, ctr_sugar)), co_iter_res), lthy); diff -r b74248961819 -r 54b09e82b9e1 src/HOL/Tools/Ctr_Sugar/ctr_sugar.ML --- a/src/HOL/Tools/Ctr_Sugar/ctr_sugar.ML Wed Feb 12 08:35:56 2014 +0100 +++ b/src/HOL/Tools/Ctr_Sugar/ctr_sugar.ML Wed Feb 12 08:35:56 2014 +0100 @@ -41,8 +41,6 @@ val register_ctr_sugar: string -> ctr_sugar -> local_theory -> local_theory val register_ctr_sugar_global: string -> ctr_sugar -> theory -> theory - val rep_compat_prefix: string - val mk_half_pairss: 'a list * 'a list -> ('a * 'a) list list val join_halves: int -> 'a list list -> 'a list list -> 'a list * 'a list list list @@ -56,10 +54,10 @@ (ctr_sugar * term list * term list) option val wrap_free_constructors: ({prems: thm list, context: Proof.context} -> tactic) list list -> - (((bool * (bool * bool)) * term list) * binding) * + (((bool * bool) * term list) * binding) * (binding list * (binding list list * (binding * term) list list)) -> local_theory -> ctr_sugar * local_theory - val parse_wrap_free_constructors_options: (bool * (bool * bool)) parser + val parse_wrap_free_constructors_options: (bool * bool) parser val parse_bound_term: (binding * string) parser end; @@ -153,8 +151,6 @@ fun register_ctr_sugar_global key ctr_sugar = Context.theory_map (Data.map (Symtab.default (key, ctr_sugar))); -val rep_compat_prefix = "new"; - val isN = "is_"; val unN = "un_"; fun mk_unN 1 1 suf = unN ^ suf @@ -282,7 +278,7 @@ fun eta_expand_arg xs f_xs = fold_rev Term.lambda xs f_xs; -fun prepare_wrap_free_constructors prep_term ((((no_discs_sels, (no_code, rep_compat)), raw_ctrs), +fun prepare_wrap_free_constructors prep_term ((((no_discs_sels, no_code), raw_ctrs), raw_case_binding), (raw_disc_bindings, (raw_sel_bindingss, raw_sel_defaultss))) no_defs_lthy = let (* TODO: sanity checks on arguments *) @@ -300,8 +296,7 @@ val fc_b_name = Long_Name.base_name fcT_name; val fc_b = Binding.name fc_b_name; - fun qualify mandatory = - Binding.qualify mandatory fc_b_name o (rep_compat ? Binding.qualify false rep_compat_prefix); + fun qualify mandatory = Binding.qualify mandatory fc_b_name; fun dest_TFree_or_TVar (TFree sS) = sS | dest_TFree_or_TVar (TVar ((s, _), S)) = (s, S) @@ -929,8 +924,7 @@ in (ctr_sugar, lthy - |> not rep_compat ? - Local_Theory.declaration {syntax = false, pervasive = true} + |> Local_Theory.declaration {syntax = false, pervasive = true} (fn phi => Case_Translation.register (Morphism.term phi casex) (map (Morphism.term phi) ctrs)) |> Local_Theory.background_theory (fold (fold Code.del_eqn) [disc_defs, sel_defs]) @@ -967,10 +961,10 @@ val parse_wrap_free_constructors_options = Scan.optional (@{keyword "("} |-- Parse.list1 - (Parse.reserved "no_discs_sels" >> K 0 || Parse.reserved "no_code" >> K 1 || - Parse.reserved "rep_compat" >> K 2) --| @{keyword ")"} - >> (fn js => (member (op =) js 0, (member (op =) js 1, member (op =) js 2)))) - (false, (false, false)); + (Parse.reserved "no_discs_sels" >> K 0 || Parse.reserved "no_code" >> K 1) --| + @{keyword ")"} + >> (fn js => (member (op =) js 0, member (op =) js 1))) + (false, false); val _ = Outer_Syntax.local_theory_to_proof @{command_spec "wrap_free_constructors"}