killed 'rep_compat' option
authorblanchet
Wed Feb 12 08:35:56 2014 +0100 (2014-02-12)
changeset 5541054b09e82b9e1
parent 55409 b74248961819
child 55411 27de2c976d90
killed 'rep_compat' option
src/Doc/Datatypes/Datatypes.thy
src/HOL/Tools/BNF/bnf_fp_def_sugar.ML
src/HOL/Tools/Ctr_Sugar/ctr_sugar.ML
     1.1 --- a/src/Doc/Datatypes/Datatypes.thy	Wed Feb 12 08:35:56 2014 +0100
     1.2 +++ b/src/Doc/Datatypes/Datatypes.thy	Wed Feb 12 08:35:56 2014 +0100
     1.3 @@ -470,7 +470,7 @@
     1.4    @@{command datatype_new} target? @{syntax dt_options}? \<newline>
     1.5      (@{syntax dt_name} '=' (@{syntax ctor} + '|') + @'and')
     1.6    ;
     1.7 -  @{syntax_def dt_options}: '(' (('no_discs_sels' | 'no_code' | 'rep_compat') + ',') ')'
     1.8 +  @{syntax_def dt_options}: '(' (('no_discs_sels' | 'no_code') + ',') ')'
     1.9  \<close>}
    1.10  
    1.11  \medskip
    1.12 @@ -492,12 +492,6 @@
    1.13  \item
    1.14  The @{text "no_code"} option indicates that the datatype should not be
    1.15  registered for code generation.
    1.16 -
    1.17 -\item
    1.18 -The @{text "rep_compat"} option indicates that the generated names should
    1.19 -contain optional (and normally not displayed) ``@{text "new."}'' components to
    1.20 -prevent clashes with a later call to \keyw{rep\_datatype}. See
    1.21 -Section~\ref{ssec:datatype-compatibility-issues} for details.
    1.22  \end{itemize}
    1.23  
    1.24  The left-hand sides of the datatype equations specify the name of the type to
    1.25 @@ -2563,7 +2557,7 @@
    1.26  %    old \keyw{datatype}
    1.27  %
    1.28  %  * @{command wrap_free_constructors}
    1.29 -%    * @{text "no_discs_sels"}, @{text "no_code"}, @{text "rep_compat"}
    1.30 +%    * @{text "no_discs_sels"}, @{text "no_code"}
    1.31  %    * hack to have both co and nonco view via locale (cf. ext nats)
    1.32  %  * code generator
    1.33  %     * eq, refl, simps
    1.34 @@ -2601,7 +2595,7 @@
    1.35  
    1.36  \medskip
    1.37  
    1.38 -% options: no_discs_sels no_code rep_compat
    1.39 +% options: no_discs_sels no_code
    1.40  
    1.41  \noindent
    1.42  Section~\ref{ssec:datatype-generated-theorems} lists the generated theorems.
     2.1 --- a/src/HOL/Tools/BNF/bnf_fp_def_sugar.ML	Wed Feb 12 08:35:56 2014 +0100
     2.2 +++ b/src/HOL/Tools/BNF/bnf_fp_def_sugar.ML	Wed Feb 12 08:35:56 2014 +0100
     2.3 @@ -95,7 +95,7 @@
     2.4    val co_datatypes: BNF_FP_Util.fp_kind -> (mixfix list -> binding list -> binding list ->
     2.5        binding list list -> binding list -> (string * sort) list -> typ list * typ list list ->
     2.6        BNF_Def.bnf list -> local_theory -> BNF_FP_Util.fp_result * local_theory) ->
     2.7 -    (bool * (bool * bool)) * (((((binding * (typ * sort)) list * binding) * (binding * binding))
     2.8 +    (bool * bool) * (((((binding * (typ * sort)) list * binding) * (binding * binding))
     2.9        * mixfix) * ((((binding * binding) * (binding * typ) list) * (binding * term) list) *
    2.10          mixfix) list) list ->
    2.11      local_theory -> local_theory
    2.12 @@ -978,7 +978,7 @@
    2.13    end;
    2.14  
    2.15  fun define_co_datatypes prepare_constraint prepare_typ prepare_term fp construct_fp
    2.16 -    (wrap_opts as (no_discs_sels, (_, rep_compat)), specs) no_defs_lthy0 =
    2.17 +    (wrap_opts as (no_discs_sels, _), specs) no_defs_lthy0 =
    2.18    let
    2.19      (* TODO: sanity checks on arguments *)
    2.20  
    2.21 @@ -987,9 +987,6 @@
    2.22        else
    2.23          ();
    2.24  
    2.25 -    fun qualify mandatory fp_b_name =
    2.26 -      Binding.qualify mandatory fp_b_name o (rep_compat ? Binding.qualify false rep_compat_prefix);
    2.27 -
    2.28      val nn = length specs;
    2.29      val fp_bs = map type_binding_of specs;
    2.30      val fp_b_names = map Binding.name_of fp_bs;
    2.31 @@ -1041,7 +1038,7 @@
    2.32  
    2.33      val disc_bindingss = map (map disc_of) ctr_specss;
    2.34      val ctr_bindingss =
    2.35 -      map2 (fn fp_b_name => map (qualify false fp_b_name o ctr_of)) fp_b_names ctr_specss;
    2.36 +      map2 (fn fp_b_name => map (Binding.qualify false fp_b_name o ctr_of)) fp_b_names ctr_specss;
    2.37      val ctr_argsss = map (map args_of) ctr_specss;
    2.38      val ctr_mixfixess = map (map ctr_mixfix_of) ctr_specss;
    2.39  
    2.40 @@ -1150,12 +1147,12 @@
    2.41      fun massage_simple_notes base =
    2.42        filter_out (null o #2)
    2.43        #> map (fn (thmN, thms, attrs) =>
    2.44 -        ((qualify true base (Binding.name thmN), attrs), [(thms, [])]));
    2.45 +        ((Binding.qualify true base (Binding.name thmN), attrs), [(thms, [])]));
    2.46  
    2.47      val massage_multi_notes =
    2.48        maps (fn (thmN, thmss, attrs) =>
    2.49          map3 (fn fp_b_name => fn Type (T_name, _) => fn thms =>
    2.50 -            ((qualify true fp_b_name (Binding.name thmN), attrs T_name), [(thms, [])]))
    2.51 +            ((Binding.qualify true fp_b_name (Binding.name thmN), attrs T_name), [(thms, [])]))
    2.52            fp_b_names fpTs thmss)
    2.53        #> filter_out (null o fst o hd o snd);
    2.54  
    2.55 @@ -1346,7 +1343,7 @@
    2.56                 lthy |> Local_Theory.notes (anonymous_notes @ notes) |> snd)
    2.57              end;
    2.58  
    2.59 -        fun mk_binding pre = qualify false fp_b_name (Binding.prefix_name (pre ^ "_") fp_b);
    2.60 +        fun mk_binding pre = Binding.qualify false fp_b_name (Binding.prefix_name (pre ^ "_") fp_b);
    2.61  
    2.62          fun massage_res (((maps_sets_rels, ctr_sugar), co_iter_res), lthy) =
    2.63            (((maps_sets_rels, (ctrs, xss, ctr_defs, ctr_sugar)), co_iter_res), lthy);
     3.1 --- a/src/HOL/Tools/Ctr_Sugar/ctr_sugar.ML	Wed Feb 12 08:35:56 2014 +0100
     3.2 +++ b/src/HOL/Tools/Ctr_Sugar/ctr_sugar.ML	Wed Feb 12 08:35:56 2014 +0100
     3.3 @@ -41,8 +41,6 @@
     3.4    val register_ctr_sugar: string -> ctr_sugar -> local_theory -> local_theory
     3.5    val register_ctr_sugar_global: string -> ctr_sugar -> theory -> theory
     3.6  
     3.7 -  val rep_compat_prefix: string
     3.8 -
     3.9    val mk_half_pairss: 'a list * 'a list -> ('a * 'a) list list
    3.10    val join_halves: int -> 'a list list -> 'a list list -> 'a list * 'a list list list
    3.11  
    3.12 @@ -56,10 +54,10 @@
    3.13      (ctr_sugar * term list * term list) option
    3.14  
    3.15    val wrap_free_constructors: ({prems: thm list, context: Proof.context} -> tactic) list list ->
    3.16 -    (((bool * (bool * bool)) * term list) * binding) *
    3.17 +    (((bool * bool) * term list) * binding) *
    3.18        (binding list * (binding list list * (binding * term) list list)) -> local_theory ->
    3.19      ctr_sugar * local_theory
    3.20 -  val parse_wrap_free_constructors_options: (bool * (bool * bool)) parser
    3.21 +  val parse_wrap_free_constructors_options: (bool * bool) parser
    3.22    val parse_bound_term: (binding * string) parser
    3.23  end;
    3.24  
    3.25 @@ -153,8 +151,6 @@
    3.26  fun register_ctr_sugar_global key ctr_sugar =
    3.27    Context.theory_map (Data.map (Symtab.default (key, ctr_sugar)));
    3.28  
    3.29 -val rep_compat_prefix = "new";
    3.30 -
    3.31  val isN = "is_";
    3.32  val unN = "un_";
    3.33  fun mk_unN 1 1 suf = unN ^ suf
    3.34 @@ -282,7 +278,7 @@
    3.35  
    3.36  fun eta_expand_arg xs f_xs = fold_rev Term.lambda xs f_xs;
    3.37  
    3.38 -fun prepare_wrap_free_constructors prep_term ((((no_discs_sels, (no_code, rep_compat)), raw_ctrs),
    3.39 +fun prepare_wrap_free_constructors prep_term ((((no_discs_sels, no_code), raw_ctrs),
    3.40      raw_case_binding), (raw_disc_bindings, (raw_sel_bindingss, raw_sel_defaultss))) no_defs_lthy =
    3.41    let
    3.42      (* TODO: sanity checks on arguments *)
    3.43 @@ -300,8 +296,7 @@
    3.44      val fc_b_name = Long_Name.base_name fcT_name;
    3.45      val fc_b = Binding.name fc_b_name;
    3.46  
    3.47 -    fun qualify mandatory =
    3.48 -      Binding.qualify mandatory fc_b_name o (rep_compat ? Binding.qualify false rep_compat_prefix);
    3.49 +    fun qualify mandatory = Binding.qualify mandatory fc_b_name;
    3.50  
    3.51      fun dest_TFree_or_TVar (TFree sS) = sS
    3.52        | dest_TFree_or_TVar (TVar ((s, _), S)) = (s, S)
    3.53 @@ -929,8 +924,7 @@
    3.54        in
    3.55          (ctr_sugar,
    3.56           lthy
    3.57 -         |> not rep_compat ?
    3.58 -            Local_Theory.declaration {syntax = false, pervasive = true}
    3.59 +         |> Local_Theory.declaration {syntax = false, pervasive = true}
    3.60                (fn phi => Case_Translation.register
    3.61                   (Morphism.term phi casex) (map (Morphism.term phi) ctrs))
    3.62           |> Local_Theory.background_theory (fold (fold Code.del_eqn) [disc_defs, sel_defs])
    3.63 @@ -967,10 +961,10 @@
    3.64  
    3.65  val parse_wrap_free_constructors_options =
    3.66    Scan.optional (@{keyword "("} |-- Parse.list1
    3.67 -        (Parse.reserved "no_discs_sels" >> K 0 || Parse.reserved "no_code" >> K 1 ||
    3.68 -         Parse.reserved "rep_compat" >> K 2) --| @{keyword ")"}
    3.69 -      >> (fn js => (member (op =) js 0, (member (op =) js 1, member (op =) js 2))))
    3.70 -    (false, (false, false));
    3.71 +        (Parse.reserved "no_discs_sels" >> K 0 || Parse.reserved "no_code" >> K 1) --|
    3.72 +      @{keyword ")"}
    3.73 +      >> (fn js => (member (op =) js 0, member (op =) js 1)))
    3.74 +    (false, false);
    3.75  
    3.76  val _ =
    3.77    Outer_Syntax.local_theory_to_proof @{command_spec "wrap_free_constructors"}