# HG changeset patch # User blanchet # Date 1392761339 -3600 # Node ID a6153343c44f9b95217039f15e865682018c9a07 # Parent 853b82488fdab5d461aa77305634dab7c749c0dc prepare two-stage 'primrec' setup diff -r 853b82488fda -r a6153343c44f src/HOL/BNF_FP_Base.thy --- 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" diff -r 853b82488fda -r a6153343c44f src/HOL/BNF_LFP.thy --- 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 diff -r 853b82488fda -r a6153343c44f src/HOL/Tools/BNF/bnf_fp_def_sugar.ML --- 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; diff -r 853b82488fda -r a6153343c44f src/HOL/Tools/BNF/bnf_fp_rec_sugar_util.ML --- 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; diff -r 853b82488fda -r a6153343c44f src/HOL/Tools/BNF/bnf_gfp_rec_sugar.ML --- 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; diff -r 853b82488fda -r a6153343c44f src/HOL/Tools/BNF/bnf_lfp_compat.ML --- 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); diff -r 853b82488fda -r a6153343c44f src/HOL/Tools/BNF/bnf_lfp_rec_sugar.ML --- 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; diff -r 853b82488fda -r a6153343c44f src/HOL/Tools/BNF/bnf_lfp_rec_sugar_more.ML --- /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; diff -r 853b82488fda -r a6153343c44f src/HOL/Tools/BNF/bnf_util.ML --- 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 =