--- 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"