--- a/src/HOL/BNF_FP_Base.thy Tue Feb 18 23:08:58 2014 +0100
+++ b/src/HOL/BNF_FP_Base.thy Tue Feb 18 23:08:59 2014 +0100
@@ -149,6 +149,7 @@
unfolding Grp_def by rule auto
ML_file "Tools/BNF/bnf_fp_util.ML"
+ML_file "Tools/BNF/bnf_fp_rec_sugar_util.ML"
ML_file "Tools/BNF/bnf_fp_def_sugar_tactics.ML"
ML_file "Tools/BNF/bnf_fp_def_sugar.ML"
ML_file "Tools/BNF/bnf_fp_n2m_tactics.ML"
--- a/src/HOL/BNF_LFP.thy Tue Feb 18 23:08:58 2014 +0100
+++ b/src/HOL/BNF_LFP.thy Tue Feb 18 23:08:59 2014 +0100
@@ -241,8 +241,8 @@
ML_file "Tools/BNF/bnf_lfp_tactics.ML"
ML_file "Tools/BNF/bnf_lfp.ML"
ML_file "Tools/BNF/bnf_lfp_compat.ML"
-ML_file "Tools/BNF/bnf_fp_rec_sugar_util.ML"
ML_file "Tools/BNF/bnf_lfp_rec_sugar.ML"
+ML_file "Tools/BNF/bnf_lfp_rec_sugar_more.ML"
hide_fact (open) id_transfer
--- a/src/HOL/Tools/BNF/bnf_fp_def_sugar.ML Tue Feb 18 23:08:58 2014 +0100
+++ b/src/HOL/Tools/BNF/bnf_fp_def_sugar.ML Tue Feb 18 23:08:59 2014 +0100
@@ -33,16 +33,12 @@
val co_induct_of: 'a list -> 'a
val strong_co_induct_of: 'a list -> 'a
- val tvar_subst: theory -> typ list -> typ list -> ((string * int) * typ) list
- val flat_rec_arg_args: 'a list list -> 'a list
val flat_corec_preds_predsss_gettersss: 'a list -> 'a list list list -> 'a list list list ->
'a list
- val mk_co_iter: theory -> BNF_FP_Util.fp_kind -> typ -> typ list -> term -> term
val nesty_bnfs: Proof.context -> typ list list list -> typ list -> BNF_Def.bnf list
type lfp_sugar_thms =
- (thm list * thm * Args.src list)
- * (thm list list * thm list list * Args.src list)
+ (thm list * thm * Args.src list) * (thm list list * thm list list * Args.src list)
val morph_lfp_sugar_thms: morphism -> lfp_sugar_thms -> lfp_sugar_thms
val transfer_lfp_sugar_thms: Proof.context -> lfp_sugar_thms -> lfp_sugar_thms
@@ -65,8 +61,6 @@
* (string * term list * term list list
* ((term list list * term list list list) * typ list) list) option)
* Proof.context
- val mk_iter_fun_arg_types: typ list list list -> int list -> int list list -> typ ->
- typ list list list list
val mk_coiter_fun_arg_types: typ list list list -> typ list -> int list -> term ->
typ list list
* (typ list list list list * typ list list list * typ list list list list * typ list)
@@ -110,6 +104,7 @@
struct
open Ctr_Sugar
+open BNF_FP_Rec_Sugar_Util
open BNF_Util
open BNF_Comp
open BNF_Def
@@ -219,17 +214,8 @@
val code_nitpicksimp_attrs = Code.add_default_eqn_attrib :: nitpicksimp_attrs;
val simp_attrs = @{attributes [simp]};
-fun tvar_subst thy Ts Us =
- Vartab.fold (cons o apsnd snd) (fold (Sign.typ_match thy) (Ts ~~ Us) Vartab.empty) [];
-
val lists_bmoc = fold (fn xs => fn t => Term.list_comb (t, xs));
-fun flat_rec_arg_args xss =
- (* FIXME (once the old datatype package is phased out): The first line below gives the preferred
- order. The second line is for compatibility with the old datatype package. *)
- (* flat xss *)
- map hd xss @ maps tl xss;
-
fun flat_corec_predss_getterss qss fss = maps (op @) (qss ~~ fss);
fun flat_corec_preds_predsss_gettersss [] [qss] [fss] = flat_corec_predss_getterss qss fss
@@ -262,16 +248,6 @@
val mk_ctor = mk_ctor_or_dtor range_type;
val mk_dtor = mk_ctor_or_dtor domain_type;
-fun mk_co_iter thy fp fpT Cs t =
- let
- val (f_Cs, Type (_, [prebody, body])) = strip_fun_type (fastype_of t);
- val fpT0 = fp_case fp prebody body;
- val Cs0 = distinct (op =) (map (fp_case fp body_type domain_type) f_Cs);
- val rho = tvar_subst thy (fpT0 :: Cs0) (fpT :: Cs);
- in
- Term.subst_TVars rho t
- end;
-
fun mk_co_iters thy fp fpTs Cs ts0 =
let
val nn = length fpTs;
@@ -283,10 +259,6 @@
map (Term.subst_TVars rho) ts0
end;
-fun unzip_recT (Type (@{type_name prod}, _)) T = [T]
- | unzip_recT _ (Type (@{type_name prod}, Ts)) = Ts
- | unzip_recT _ T = [T];
-
fun unzip_corecT (Type (@{type_name sum}, _)) T = [T]
| unzip_corecT _ (Type (@{type_name sum}, Ts)) = Ts
| unzip_corecT _ T = [T];
@@ -333,8 +305,7 @@
fun indexify proj xs f p = f (find_index (curry (op =) (proj p)) xs) p;
type lfp_sugar_thms =
- (thm list * thm * Args.src list)
- * (thm list list * thm list list * Args.src list)
+ (thm list * thm * Args.src list) * (thm list list * thm list list * Args.src list)
fun morph_lfp_sugar_thms phi ((inducts, induct, induct_attrs), (foldss, recss, iter_attrs)) =
((map (Morphism.thm phi) inducts, Morphism.thm phi induct, induct_attrs),
@@ -368,13 +339,6 @@
val transfer_gfp_sugar_thms =
morph_gfp_sugar_thms o Morphism.transfer_morphism o Proof_Context.theory_of;
-fun mk_iter_fun_arg_types0 n ms = map2 dest_tupleT ms o dest_sumTN_balanced n o domain_type;
-
-fun mk_iter_fun_arg_types ctr_Tsss ns mss =
- binder_fun_types
- #> map3 mk_iter_fun_arg_types0 ns mss
- #> map2 (map2 (map2 unzip_recT)) ctr_Tsss;
-
fun mk_iters_args_types ctr_Tsss Cs ns mss ctor_iter_fun_Tss lthy =
let
val Css = map2 replicate ns Cs;
--- a/src/HOL/Tools/BNF/bnf_fp_rec_sugar_util.ML Tue Feb 18 23:08:58 2014 +0100
+++ b/src/HOL/Tools/BNF/bnf_fp_rec_sugar_util.ML Tue Feb 18 23:08:59 2014 +0100
@@ -15,14 +15,27 @@
val find_index_eq: ''a list -> ''a -> int
val finds: ('a * 'b -> bool) -> 'a list -> 'b list -> ('a * 'b list) list * 'b list
+ val tvar_subst: theory -> typ list -> typ list -> ((string * int) * typ) list
+
val drop_all: term -> term
- val get_indices: ((binding * typ) * 'a) list -> term -> int list
+ val get_free_indices: ((binding * typ) * 'a) list -> term -> int list
+
+ (* needed here for bootstrapping; would be more at home in "bnf_fp_def_sugar.ML" *)
+ val unzip_recT: typ -> typ -> typ list
+ val mk_iter_fun_arg_types0: int -> int list -> typ -> typ list list
+ val mk_iter_fun_arg_types: typ list list list -> int list -> int list list -> typ ->
+ typ list list list list
+ val flat_rec_arg_args: 'a list list -> 'a list
+ val mk_co_iter: theory -> BNF_FP_Util.fp_kind -> typ -> typ list -> term -> term
end;
structure BNF_FP_Rec_Sugar_Util : BNF_FP_REC_SUGAR_UTIL =
struct
+open BNF_Util
+open BNF_FP_Util
+
fun indexe _ h = (h, h + 1);
fun indexed xs = fold_map indexe xs;
fun indexedd xss = fold_map indexed xss;
@@ -33,12 +46,42 @@
fun finds eq = fold_map (fn x => List.partition (curry eq x) #>> pair x);
+fun tvar_subst thy Ts Us =
+ Vartab.fold (cons o apsnd snd) (fold (Sign.typ_match thy) (Ts ~~ Us) Vartab.empty) [];
+
fun drop_all t =
subst_bounds (strip_qnt_vars @{const_name all} t |> map Free |> rev,
strip_qnt_body @{const_name all} t);
-fun get_indices fixes t = map (fst #>> Binding.name_of #> Free) fixes
+fun get_free_indices fixes t = map (fst #>> Binding.name_of #> Free) fixes
|> map_index (fn (i, v) => if exists_subterm (equal v) t then SOME i else NONE)
|> map_filter I;
+fun unzip_recT (Type (@{type_name prod}, _)) T = [T]
+ | unzip_recT _ (Type (@{type_name prod}, Ts)) = Ts
+ | unzip_recT _ T = [T];
+
+fun mk_iter_fun_arg_types0 n ms = map2 dest_tupleT ms o dest_sumTN_balanced n o domain_type;
+
+fun mk_iter_fun_arg_types ctr_Tsss ns mss =
+ binder_fun_types
+ #> map3 mk_iter_fun_arg_types0 ns mss
+ #> map2 (map2 (map2 unzip_recT)) ctr_Tsss;
+
+fun flat_rec_arg_args xss =
+ (* FIXME (once the old datatype package is phased out): The first line below gives the preferred
+ order. The second line is for compatibility with the old datatype package. *)
+ (* flat xss *)
+ map hd xss @ maps tl xss;
+
+fun mk_co_iter thy fp fpT Cs t =
+ let
+ val (f_Cs, Type (_, [prebody, body])) = strip_fun_type (fastype_of t);
+ val fpT0 = fp_case fp prebody body;
+ val Cs0 = distinct (op =) (map (fp_case fp body_type domain_type) f_Cs);
+ val rho = tvar_subst thy (fpT0 :: Cs0) (fpT :: Cs);
+ in
+ Term.subst_TVars rho t
+ end;
+
end;
--- a/src/HOL/Tools/BNF/bnf_gfp_rec_sugar.ML Tue Feb 18 23:08:58 2014 +0100
+++ b/src/HOL/Tools/BNF/bnf_gfp_rec_sugar.ML Tue Feb 18 23:08:59 2014 +0100
@@ -936,7 +936,7 @@
val ((n2m, corec_specs', _, coinduct_thm, strong_coinduct_thm, coinduct_thms,
strong_coinduct_thms), lthy') =
- corec_specs_of bs arg_Ts res_Ts (get_indices fixes) callssss lthy;
+ corec_specs_of bs arg_Ts res_Ts (get_free_indices fixes) callssss lthy;
val corec_specs = take actual_nn corec_specs';
val ctr_specss = map #ctr_specs corec_specs;
--- a/src/HOL/Tools/BNF/bnf_lfp_compat.ML Tue Feb 18 23:08:58 2014 +0100
+++ b/src/HOL/Tools/BNF/bnf_lfp_compat.ML Tue Feb 18 23:08:59 2014 +0100
@@ -99,7 +99,7 @@
| NONE => error ("Unsupported recursion via type constructor " ^ quote s ^
" not corresponding to new-style datatype (cf. \"datatype_new\")"));
- fun get_indices (Var ((_, kk), _)) = [kk];
+ fun get_var_indices (Var ((_, kk), _)) = [kk];
val (Tparentss_kkssss, _) = nested_Tparentss_indicessss_of [] fpT1 0;
val Tparentss = map fst Tparentss_kkssss;
@@ -128,7 +128,7 @@
val ((fp_sugars, (lfp_sugar_thms, _)), lthy) =
if nn > nn_fp then
- mutualize_fp_sugars Least_FP compat_bs Ts get_indices callssss fp_sugars0 lthy
+ mutualize_fp_sugars Least_FP compat_bs Ts get_var_indices callssss fp_sugars0 lthy
else
((fp_sugars0, (NONE, NONE)), lthy);
--- a/src/HOL/Tools/BNF/bnf_lfp_rec_sugar.ML Tue Feb 18 23:08:58 2014 +0100
+++ b/src/HOL/Tools/BNF/bnf_lfp_rec_sugar.ML Tue Feb 18 23:08:59 2014 +0100
@@ -8,6 +8,25 @@
signature BNF_LFP_REC_SUGAR =
sig
+ type basic_lfp_sugar =
+ {T: typ,
+ fp_res_index: int,
+ ctor_recT: typ,
+ ctr_defs: thm list,
+ ctr_sugar: Ctr_Sugar.ctr_sugar,
+ recx: term,
+ rec_thms: thm list};
+
+ type lfp_rec_extension =
+ {is_new_datatype: Proof.context -> string -> bool,
+ get_basic_lfp_sugars: binding list -> typ list -> (term -> int list) ->
+ (term * term list list) list list -> local_theory ->
+ typ list * int list * basic_lfp_sugar list * thm list * thm list * thm * bool * local_theory,
+ massage_nested_rec_call: Proof.context -> (term -> bool) -> (typ -> typ -> term -> term) ->
+ typ list -> term -> term -> term -> term};
+
+ val register_lfp_rec_extension: lfp_rec_extension -> theory -> theory
+
val add_primrec: (binding * typ option * mixfix) list ->
(Attrib.binding * term) list -> local_theory -> (term list * thm list list) * local_theory
val add_primrec_cmd: (binding * string option * mixfix) list ->
@@ -27,10 +46,8 @@
open Ctr_Sugar
open BNF_Util
open BNF_Tactics
-open BNF_Def
open BNF_FP_Util
open BNF_FP_Def_Sugar
-open BNF_FP_N2M_Sugar
open BNF_FP_Rec_Sugar_Util
val nitpicksimp_attrs = @{attributes [nitpick_simp]};
@@ -61,79 +78,6 @@
nested_map_comps: thm list,
ctr_specs: rec_ctr_spec list};
-exception NOT_A_MAP of term;
-
-fun ill_formed_rec_call ctxt t =
- error ("Ill-formed recursive call: " ^ quote (Syntax.string_of_term ctxt t));
-fun invalid_map ctxt t =
- error ("Invalid map function in " ^ quote (Syntax.string_of_term ctxt t));
-fun unexpected_rec_call ctxt t =
- error ("Unexpected recursive call: " ^ quote (Syntax.string_of_term ctxt t));
-
-fun massage_nested_rec_call ctxt has_call raw_massage_fun bound_Ts y y' =
- let
- fun check_no_call t = if has_call t then unexpected_rec_call ctxt t else ();
-
- val typof = curry fastype_of1 bound_Ts;
- val build_map_fst = build_map ctxt (fst_const o fst);
-
- val yT = typof y;
- val yU = typof y';
-
- fun y_of_y' () = build_map_fst (yU, yT) $ y';
- val elim_y = Term.map_aterms (fn t => if t = y then y_of_y' () else t);
-
- fun massage_mutual_fun U T t =
- (case t of
- Const (@{const_name comp}, _) $ t1 $ t2 =>
- mk_comp bound_Ts (tap check_no_call t1, massage_mutual_fun U T t2)
- | _ =>
- if has_call t then
- (case try HOLogic.dest_prodT U of
- SOME (U1, U2) => if U1 = T then raw_massage_fun T U2 t else invalid_map ctxt t
- | NONE => invalid_map ctxt t)
- else
- mk_comp bound_Ts (t, build_map_fst (U, T)));
-
- fun massage_map (Type (_, Us)) (Type (s, Ts)) t =
- (case try (dest_map ctxt s) t of
- SOME (map0, fs) =>
- let
- val Type (_, ran_Ts) = range_type (typof t);
- val map' = mk_map (length fs) Us ran_Ts map0;
- val fs' = map_flattened_map_args ctxt s (map3 massage_map_or_map_arg Us Ts) fs;
- in
- Term.list_comb (map', fs')
- end
- | NONE => raise NOT_A_MAP t)
- | massage_map _ _ t = raise NOT_A_MAP t
- and massage_map_or_map_arg U T t =
- if T = U then
- tap check_no_call t
- else
- massage_map U T t
- handle NOT_A_MAP _ => massage_mutual_fun U T t;
-
- fun massage_call (t as t1 $ t2) =
- if has_call t then
- if t2 = y then
- massage_map yU yT (elim_y t1) $ y'
- handle NOT_A_MAP t' => invalid_map ctxt t'
- else
- let val (g, xs) = Term.strip_comb t2 in
- if g = y then
- if exists has_call xs then unexpected_rec_call ctxt t2
- else Term.list_comb (massage_call (mk_compN (length xs) bound_Ts (t1, y)), xs)
- else
- ill_formed_rec_call ctxt t
- end
- else
- elim_y t
- | massage_call t = if t = y then y_of_y' () else ill_formed_rec_call ctxt t;
- in
- massage_call
- end;
-
type basic_lfp_sugar =
{T: typ,
fp_res_index: int,
@@ -143,31 +87,44 @@
recx: term,
rec_thms: thm list};
-fun basic_lfp_sugar_of ({T, fp_res = {xtor_co_iterss = ctor_iterss, ...}, fp_res_index, ctr_defs,
- ctr_sugar, co_iters = iters, co_iter_thmss = iter_thmss, ...} : fp_sugar) =
- {T = T, fp_res_index = fp_res_index,
- ctor_recT = fastype_of (co_rec_of (nth ctor_iterss fp_res_index)), ctr_defs = ctr_defs,
- ctr_sugar = ctr_sugar, recx = co_rec_of iters, rec_thms = co_rec_of iter_thmss};
+type lfp_rec_extension =
+ {is_new_datatype: Proof.context -> string -> bool,
+ get_basic_lfp_sugars: binding list -> typ list -> (term -> int list) ->
+ (term * term list list) list list -> local_theory ->
+ typ list * int list * basic_lfp_sugar list * thm list * thm list * thm * bool * local_theory,
+ massage_nested_rec_call: Proof.context -> (term -> bool) -> (typ -> typ -> term -> term) ->
+ typ list -> term -> term -> term -> term};
+
+structure Data = Theory_Data
+(
+ type T = lfp_rec_extension option;
+ val empty = NONE;
+ val extend = I;
+ val merge = merge_options;
+);
-fun get_basic_lfp_sugars bs arg_Ts get_indices callssss0 lthy0 =
- let
- val ((missing_arg_Ts, perm0_kks,
- fp_sugars as {nested_bnfs, co_inducts = [induct_thm], ...} :: _, (lfp_sugar_thms, _)),
- lthy) =
- nested_to_mutual_fps Least_FP bs arg_Ts get_indices callssss0 lthy0;
- val nested_map_idents = map (unfold_thms lthy @{thms id_def} o map_id0_of_bnf) nested_bnfs;
- val nested_map_comps = map map_comp_of_bnf nested_bnfs;
- in
- (missing_arg_Ts, perm0_kks, map basic_lfp_sugar_of fp_sugars, nested_map_idents,
- nested_map_comps, induct_thm, lfp_sugar_thms, lthy)
- end;
+val register_lfp_rec_extension = Data.put o SOME;
+
+fun is_new_datatype ctxt =
+ (case Data.get (Proof_Context.theory_of ctxt) of
+ SOME {is_new_datatype, ...} => is_new_datatype ctxt
+ | NONE => K false);
+
+fun get_basic_lfp_sugars bs arg_Ts get_indices callssss lthy =
+ (case Data.get (Proof_Context.theory_of lthy) of
+ SOME {get_basic_lfp_sugars, ...} => get_basic_lfp_sugars bs arg_Ts get_indices callssss lthy
+ | NONE => error "Not implemented yet");
+
+fun massage_nested_rec_call ctxt =
+ (case Data.get (Proof_Context.theory_of ctxt) of
+ SOME {massage_nested_rec_call, ...} => massage_nested_rec_call ctxt);
fun rec_specs_of bs arg_Ts res_Ts get_indices callssss0 lthy0 =
let
val thy = Proof_Context.theory_of lthy0;
val (missing_arg_Ts, perm0_kks, basic_lfp_sugars, nested_map_idents, nested_map_comps,
- induct_thm, lfp_sugar_thms, lthy) =
+ induct_thm, n2m, lthy) =
get_basic_lfp_sugars bs arg_Ts get_indices callssss0 lthy0;
val perm_basic_lfp_sugars = sort (int_ord o pairself #fp_res_index) basic_lfp_sugars;
@@ -233,8 +190,8 @@
nested_map_idents = nested_map_idents, nested_map_comps = nested_map_comps,
ctr_specs = mk_ctr_specs fp_res_index ctr_offset ctrs rec_thms};
in
- ((is_some lfp_sugar_thms, map2 mk_spec ctr_offsets basic_lfp_sugars, missing_arg_Ts, induct_thm,
- induct_thms), lthy)
+ ((n2m, map2 mk_spec ctr_offsets basic_lfp_sugars, missing_arg_Ts, induct_thm, induct_thms),
+ lthy)
end;
val undef_const = Const (@{const_name undefined}, dummyT);
@@ -496,8 +453,7 @@
|> partition_eq ((op =) o pairself #fun_name)
|> finds (fn (x, y) => x = #fun_name (hd y)) fun_names |> fst
|> map (fn (x, y) => the_single y
- handle List.Empty =>
- primrec_error ("missing equations for function " ^ quote x));
+ handle List.Empty => primrec_error ("missing equations for function " ^ quote x));
val has_call = exists_subterm (map (fst #>> Binding.name_of #> Free) fixes |> member (op =));
val arg_Ts = map (#rec_type o hd) funs_data;
@@ -507,7 +463,7 @@
|> map (maps (map_filter (find_rec_calls has_call)));
fun is_only_old_datatype (Type (s, _)) =
- is_none (fp_sugar_of lthy0 s) andalso is_some (Datatype_Data.get_info thy s)
+ is_some (Datatype_Data.get_info thy s) andalso not (is_new_datatype lthy0 s)
| is_only_old_datatype _ = false;
val _ = if exists is_only_old_datatype arg_Ts then raise OLD_PRIMREC () else ();
@@ -516,7 +472,7 @@
| (b, _) :: _ => primrec_error ("type of " ^ Binding.print b ^ " contains top sort"));
val ((n2m, rec_specs, _, induct_thm, induct_thms), lthy) =
- rec_specs_of bs arg_Ts res_Ts (get_indices fixes) callssss lthy0;
+ rec_specs_of bs arg_Ts res_Ts (get_free_indices fixes) callssss lthy0;
val actual_nn = length funs_data;
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Tools/BNF/bnf_lfp_rec_sugar_more.ML Tue Feb 18 23:08:59 2014 +0100
@@ -0,0 +1,118 @@
+(* Title: HOL/Tools/BNF/bnf_lfp_rec_sugar_more.ML
+ Author: Lorenz Panny, TU Muenchen
+ Author: Jasmin Blanchette, TU Muenchen
+ Copyright 2013
+
+More recursor sugar.
+*)
+
+structure BNF_LFP_Rec_Sugar_More : sig end =
+struct
+
+open BNF_Util
+open BNF_Def
+open BNF_FP_Util
+open BNF_FP_Def_Sugar
+open BNF_FP_N2M_Sugar
+open BNF_LFP_Rec_Sugar
+
+fun is_new_datatype ctxt s =
+ (case fp_sugar_of ctxt s of SOME {fp = Least_FP, ...} => true | _ => false);
+
+fun basic_lfp_sugar_of ({T, fp_res = {xtor_co_iterss = ctor_iterss, ...}, fp_res_index, ctr_defs,
+ ctr_sugar, co_iters = iters, co_iter_thmss = iter_thmss, ...} : fp_sugar) =
+ {T = T, fp_res_index = fp_res_index,
+ ctor_recT = fastype_of (co_rec_of (nth ctor_iterss fp_res_index)), ctr_defs = ctr_defs,
+ ctr_sugar = ctr_sugar, recx = co_rec_of iters, rec_thms = co_rec_of iter_thmss};
+
+fun get_basic_lfp_sugars bs arg_Ts get_indices callssss0 lthy0 =
+ let
+ val ((missing_arg_Ts, perm0_kks,
+ fp_sugars as {nested_bnfs, co_inducts = [induct_thm], ...} :: _, (lfp_sugar_thms, _)),
+ lthy) =
+ nested_to_mutual_fps Least_FP bs arg_Ts get_indices callssss0 lthy0;
+ val nested_map_idents = map (unfold_thms lthy @{thms id_def} o map_id0_of_bnf) nested_bnfs;
+ val nested_map_comps = map map_comp_of_bnf nested_bnfs;
+ in
+ (missing_arg_Ts, perm0_kks, map basic_lfp_sugar_of fp_sugars, nested_map_idents,
+ nested_map_comps, induct_thm, is_some lfp_sugar_thms, lthy)
+ end;
+
+exception NOT_A_MAP of term;
+
+fun ill_formed_rec_call ctxt t =
+ error ("Ill-formed recursive call: " ^ quote (Syntax.string_of_term ctxt t));
+fun invalid_map ctxt t =
+ error ("Invalid map function in " ^ quote (Syntax.string_of_term ctxt t));
+fun unexpected_rec_call ctxt t =
+ error ("Unexpected recursive call: " ^ quote (Syntax.string_of_term ctxt t));
+
+fun massage_nested_rec_call ctxt has_call raw_massage_fun bound_Ts y y' =
+ let
+ fun check_no_call t = if has_call t then unexpected_rec_call ctxt t else ();
+
+ val typof = curry fastype_of1 bound_Ts;
+ val build_map_fst = build_map ctxt (fst_const o fst);
+
+ val yT = typof y;
+ val yU = typof y';
+
+ fun y_of_y' () = build_map_fst (yU, yT) $ y';
+ val elim_y = Term.map_aterms (fn t => if t = y then y_of_y' () else t);
+
+ fun massage_mutual_fun U T t =
+ (case t of
+ Const (@{const_name comp}, _) $ t1 $ t2 =>
+ mk_comp bound_Ts (tap check_no_call t1, massage_mutual_fun U T t2)
+ | _ =>
+ if has_call t then
+ (case try HOLogic.dest_prodT U of
+ SOME (U1, U2) => if U1 = T then raw_massage_fun T U2 t else invalid_map ctxt t
+ | NONE => invalid_map ctxt t)
+ else
+ mk_comp bound_Ts (t, build_map_fst (U, T)));
+
+ fun massage_map (Type (_, Us)) (Type (s, Ts)) t =
+ (case try (dest_map ctxt s) t of
+ SOME (map0, fs) =>
+ let
+ val Type (_, ran_Ts) = range_type (typof t);
+ val map' = mk_map (length fs) Us ran_Ts map0;
+ val fs' = map_flattened_map_args ctxt s (map3 massage_map_or_map_arg Us Ts) fs;
+ in
+ Term.list_comb (map', fs')
+ end
+ | NONE => raise NOT_A_MAP t)
+ | massage_map _ _ t = raise NOT_A_MAP t
+ and massage_map_or_map_arg U T t =
+ if T = U then
+ tap check_no_call t
+ else
+ massage_map U T t
+ handle NOT_A_MAP _ => massage_mutual_fun U T t;
+
+ fun massage_call (t as t1 $ t2) =
+ if has_call t then
+ if t2 = y then
+ massage_map yU yT (elim_y t1) $ y'
+ handle NOT_A_MAP t' => invalid_map ctxt t'
+ else
+ let val (g, xs) = Term.strip_comb t2 in
+ if g = y then
+ if exists has_call xs then unexpected_rec_call ctxt t2
+ else Term.list_comb (massage_call (mk_compN (length xs) bound_Ts (t1, y)), xs)
+ else
+ ill_formed_rec_call ctxt t
+ end
+ else
+ elim_y t
+ | massage_call t = if t = y then y_of_y' () else ill_formed_rec_call ctxt t;
+ in
+ massage_call
+ end;
+
+val _ = Theory.setup (register_lfp_rec_extension
+ {is_new_datatype = is_new_datatype, get_basic_lfp_sugars = get_basic_lfp_sugars,
+ massage_nested_rec_call = massage_nested_rec_call});
+
+end;
--- a/src/HOL/Tools/BNF/bnf_util.ML Tue Feb 18 23:08:58 2014 +0100
+++ b/src/HOL/Tools/BNF/bnf_util.ML Tue Feb 18 23:08:59 2014 +0100
@@ -419,7 +419,7 @@
val AT = fst (dest_relT T);
in
Const (@{const_name card_order_on}, HOLogic.mk_setT AT --> T --> HOLogic.boolT) $
- (HOLogic.mk_UNIV AT) $ bd
+ HOLogic.mk_UNIV AT $ bd
end;
fun mk_Card_order bd =