# HG changeset patch # User blanchet # Date 1409581067 -7200 # Node ID 62765d39539f8e0580fed1f2159e0a57bc2fdd4f # Parent eaac3e01158a9c1bd4b02cf5eaf087a02cb4089f implemented compatibility definition of datatype diff -r eaac3e01158a -r 62765d39539f src/HOL/BNF_LFP.thy --- a/src/HOL/BNF_LFP.thy Mon Sep 01 16:17:47 2014 +0200 +++ b/src/HOL/BNF_LFP.thy Mon Sep 01 16:17:47 2014 +0200 @@ -193,30 +193,6 @@ ML_file "Tools/BNF/bnf_lfp_compat.ML" ML_file "Tools/BNF/bnf_lfp_rec_sugar_more.ML" -datatype_new 'a l = N | C 'a "'a l" -datatype_compat l - -datatype_new 'a m = P | D 'a "'a m l" -and 'a n = Q -datatype_compat l -datatype_compat m n - -declare [[ML_exception_trace]] -ML \ -BNF_LFP_Compat.Datatype_Data.get_all @{theory} true -|> Symtab.dest |> (fn xs => nth xs 4) |> snd |> #descr -\ - -ML \ -BNF_LFP_Compat.Datatype_Data.get_info @{theory} true @{type_name m} -|> the |> #descr -\ - - -ML \ -BNF_FP_Def_Sugar.fp_sugars_of @{context} |> tl |> hd |> #fp_res_index -\ - hide_fact (open) id_transfer end diff -r eaac3e01158a -r 62765d39539f src/HOL/Tools/BNF/bnf_lfp_compat.ML --- a/src/HOL/Tools/BNF/bnf_lfp_compat.ML Mon Sep 01 16:17:47 2014 +0200 +++ b/src/HOL/Tools/BNF/bnf_lfp_compat.ML Mon Sep 01 16:17:47 2014 +0200 @@ -10,19 +10,20 @@ signature BNF_LFP_COMPAT = sig - val get_all: theory -> bool -> Old_Datatype_Aux.info Symtab.table - val get_info: theory -> bool -> string -> Old_Datatype_Aux.info option - val the_info: theory -> bool -> string -> Old_Datatype_Aux.info - val the_spec: theory -> bool -> string -> (string * sort) list * (string * typ list) list - val the_descr: theory -> bool -> string list -> + datatype nesting_mode = Keep_Nesting | Unfold_Nesting_if_Possible | Always_Unfold_Nesting + + val get_all: theory -> nesting_mode -> Old_Datatype_Aux.info Symtab.table + val get_info: theory -> nesting_mode -> string -> Old_Datatype_Aux.info option + val the_info: theory -> nesting_mode -> string -> Old_Datatype_Aux.info + val the_spec: theory -> nesting_mode -> string -> (string * sort) list * (string * typ list) list + val the_descr: theory -> nesting_mode -> string list -> Old_Datatype_Aux.descr * (string * sort) list * string list * string * (string list * string list) * (typ list * typ list) - val get_constrs: theory -> bool -> string -> (string * typ) list option - val interpretation: bool -> (Old_Datatype_Aux.config -> string list -> theory -> theory) -> - theory -> theory - val add_datatype: Old_Datatype_Aux.config -> Old_Datatype_Aux.spec list -> theory -> - string list * theory + val get_constrs: theory -> nesting_mode -> string -> (string * typ) list option + val interpretation: nesting_mode -> + (Old_Datatype_Aux.config -> string list -> theory -> theory) -> theory -> theory val datatype_compat_cmd: string list -> local_theory -> local_theory + val add_datatype: nesting_mode -> Old_Datatype_Aux.spec list -> theory -> string list * theory end; structure BNF_LFP_Compat : BNF_LFP_COMPAT = @@ -33,9 +34,12 @@ open BNF_FP_Util open BNF_FP_Def_Sugar open BNF_FP_N2M_Sugar +open BNF_LFP val compatN = "compat_"; +datatype nesting_mode = Keep_Nesting | Unfold_Nesting_if_Possible | Always_Unfold_Nesting; + fun reindex_desc desc = let val kks = map fst desc; @@ -53,7 +57,7 @@ map (fn (_, (s, Ds, sDss)) => (s, map perm_dtyp Ds, map (apsnd (map perm_dtyp)) sDss)) desc end; -fun mk_infos_of_mutually_recursive_new_datatypes unfold_nesting need_co_inducts_recs check_names +fun mk_infos_of_mutually_recursive_new_datatypes nesting_mode need_co_inducts_recs check_names raw_fpT_names0 lthy = let val thy = Proof_Context.theory_of lthy; @@ -92,10 +96,10 @@ val orig_descr = map3 mk_typ_descr (0 upto nn_fp - 1) fpTs fp_ctr_sugars; val all_infos = Old_Datatype_Data.get_all thy; val (orig_descr' :: nested_descrs) = - if unfold_nesting then - fst (Old_Datatype_Aux.unfold_datatypes lthy orig_descr all_infos orig_descr nn_fp) + if nesting_mode = Keep_Nesting then + [orig_descr] else - [orig_descr]; + fst (Old_Datatype_Aux.unfold_datatypes lthy orig_descr all_infos orig_descr nn_fp); fun cliquify_descr [] = [] | cliquify_descr [entry] = [[entry]] @@ -168,52 +172,56 @@ (nn, b_names, compat_b_names, lfp_sugar_thms, infos, lthy') end; -fun infos_of_new_datatype_mutual_cluster lthy unfold_nesting raw_fpt_names01 = - mk_infos_of_mutually_recursive_new_datatypes unfold_nesting false subset [raw_fpt_names01] lthy +fun infos_of_new_datatype_mutual_cluster lthy nesting_mode raw_fpt_names01 = + mk_infos_of_mutually_recursive_new_datatypes nesting_mode false subset [raw_fpt_names01] lthy |> #5; -fun get_all thy unfold_nesting = +fun get_all thy nesting_mode = let val lthy = Named_Target.theory_init thy; val old_info_tab = Old_Datatype_Data.get_all thy; val new_T_names = BNF_FP_Def_Sugar.fp_sugars_of_global thy |> map_filter (try (fn {T = Type (s, _), fp_res_index = 0, ...} => s)); - val new_infos = maps (infos_of_new_datatype_mutual_cluster lthy unfold_nesting) new_T_names; + val new_infos = maps (infos_of_new_datatype_mutual_cluster lthy nesting_mode) new_T_names; in - fold (if unfold_nesting then Symtab.default else Symtab.update) new_infos old_info_tab + fold (if nesting_mode = Keep_Nesting then Symtab.update else Symtab.default) new_infos + old_info_tab end; -fun get_one get_old get_new thy unfold_nesting x = - let val (get_fst, get_snd) = (get_new thy unfold_nesting, get_old thy) |> unfold_nesting ? swap in +fun get_one get_old get_new thy nesting_mode x = + let + val (get_fst, get_snd) = + (get_old thy, get_new thy nesting_mode) |> nesting_mode = Keep_Nesting ? swap + in (case get_fst x of NONE => get_snd x | res => res) end; -fun get_info_of_new_datatype thy unfold_nesting T_name = +fun get_info_of_new_datatype thy nesting_mode T_name = let val lthy = Named_Target.theory_init thy in - AList.lookup (op =) (infos_of_new_datatype_mutual_cluster lthy unfold_nesting T_name) T_name + AList.lookup (op =) (infos_of_new_datatype_mutual_cluster lthy nesting_mode T_name) T_name end; val get_info = get_one Old_Datatype_Data.get_info get_info_of_new_datatype; -fun the_info thy unfold_nesting T_name = - (case get_info thy unfold_nesting T_name of +fun the_info thy nesting_mode T_name = + (case get_info thy nesting_mode T_name of SOME info => info | NONE => error ("Unknown datatype " ^ quote T_name)); -fun the_spec thy unfold_nesting T_name = +fun the_spec thy nesting_mode T_name = let - val {descr, index, ...} = the_info thy unfold_nesting T_name; + val {descr, index, ...} = the_info thy nesting_mode T_name; val (_, Ds, ctrs0) = the (AList.lookup (op =) descr index); val Ts = map Old_Datatype_Aux.dest_DtTFree Ds; val ctrs = map (apsnd (map (Old_Datatype_Aux.typ_of_dtyp descr))) ctrs0; in (Ts, ctrs) end; -fun the_descr thy unfold_nesting (T_names0 as T_name01 :: _) = +fun the_descr thy nesting_mode (T_names0 as T_name01 :: _) = let fun not_mutually_recursive ss = error ("{" ^ commas ss ^ "} is not a complete set of mutually recursive datatypes"); - val info = the_info thy unfold_nesting T_name01; + val info = the_info thy nesting_mode T_name01; val descr = #descr info; val (_, Ds, _) = the (AList.lookup (op =) descr (#index info)); @@ -240,8 +248,8 @@ (descr, vs, T_names, prefix, (names, auxnames), (Ts, Us)) end; -fun get_constrs thy unfold_nesting T_name = - try (the_spec thy unfold_nesting) T_name +fun get_constrs thy nesting_mode T_name = + try (the_spec thy nesting_mode) T_name |> Option.map (fn (tfrees, ctrs) => let fun varify_tfree (s, S) = TVar ((s, 0), S); @@ -255,32 +263,32 @@ map (apsnd mk_ctr_typ) ctrs end); -fun old_interpretation_of unfold_nesting f config T_names thy = - if not unfold_nesting orelse exists (is_none o fp_sugar_of_global thy) T_names then +fun old_interpretation_of nesting_mode f config T_names thy = + if nesting_mode <> Keep_Nesting orelse exists (is_none o fp_sugar_of_global thy) T_names then f config T_names thy else thy; -fun new_interpretation_of unfold_nesting f fp_sugars thy = +fun new_interpretation_of nesting_mode f fp_sugars thy = let val T_names = map (fst o dest_Type o #T) fp_sugars in - if unfold_nesting orelse exists (is_none o Old_Datatype_Data.get_info thy) T_names then - f {strict = true, quiet = true} T_names thy + if nesting_mode = Keep_Nesting orelse + exists (is_none o Old_Datatype_Data.get_info thy) T_names then + f Old_Datatype_Aux.default_config T_names thy else thy end; -fun interpretation unfold_nesting f = - Old_Datatype_Data.interpretation (old_interpretation_of unfold_nesting f) - #> fp_sugar_interpretation (new_interpretation_of unfold_nesting f); - -fun add_datatype config specs thy = ([], thy); +fun interpretation nesting_mode f = + Old_Datatype_Data.interpretation (old_interpretation_of nesting_mode f) + #> fp_sugar_interpretation (new_interpretation_of nesting_mode f); val code_nitpicksimp_simp_attrs = Code.add_default_eqn_attrib :: @{attributes [nitpick_simp, simp]}; -fun datatype_compat_cmd raw_fpT_names0 lthy = +fun datatype_compat_cmd fpT_names lthy = let val (nn, b_names, compat_b_names, lfp_sugar_thms, infos, lthy') = - mk_infos_of_mutually_recursive_new_datatypes true true eq_set raw_fpT_names0 lthy; + mk_infos_of_mutually_recursive_new_datatypes Unfold_Nesting_if_Possible true eq_set fpT_names + lthy; val all_notes = (case lfp_sugar_thms of @@ -320,6 +328,27 @@ |> snd end; +fun add_datatype nesting_mode old_specs thy = + let + val fpT_names = map (Sign.full_name thy o #1 o fst) old_specs; + + fun new_type_args_of (s, S) = (SOME Binding.empty, (TFree (s, @{sort type}), S)); + fun new_ctr_spec_of (b, Ts, mx) = (((Binding.empty, b), map (pair Binding.empty) Ts), mx); + + fun new_spec_of ((b, old_tyargs, mx), old_ctr_specs) = + (((((map new_type_args_of old_tyargs, b), mx), map new_ctr_spec_of old_ctr_specs), + (Binding.empty, Binding.empty)), []); + + val new_specs = map new_spec_of old_specs; + in + (fpT_names, + thy + |> Named_Target.theory_init + |> co_datatypes Least_FP construct_lfp ((false, false), new_specs) + |> nesting_mode <> Keep_Nesting ? datatype_compat_cmd fpT_names + |> Named_Target.exit) + end; + val _ = Outer_Syntax.local_theory @{command_spec "datatype_compat"} "register new-style datatypes as old-style datatypes"