# HG changeset patch # User blanchet # Date 1392674078 -3600 # Node ID 0819931d652d13df5e0ecccddfa3cba66693153c # Parent 6a5986170c1db79ec1e51ba02ac13c73cdd82e4d simplified data structure by reducing the incidence of clumsy indices diff -r 6a5986170c1d -r 0819931d652d src/HOL/Nitpick.thy --- a/src/HOL/Nitpick.thy Mon Feb 17 18:18:27 2014 +0100 +++ b/src/HOL/Nitpick.thy Mon Feb 17 22:54:38 2014 +0100 @@ -9,7 +9,9 @@ theory Nitpick imports BNF_FP_Base Map Record Sledgehammer -keywords "nitpick" :: diag and "nitpick_params" :: thy_decl +keywords + "nitpick" :: diag and + "nitpick_params" :: thy_decl begin typedecl bisim_iterator diff -r 6a5986170c1d -r 0819931d652d src/HOL/Tools/BNF/bnf_fp_def_sugar.ML --- a/src/HOL/Tools/BNF/bnf_fp_def_sugar.ML Mon Feb 17 18:18:27 2014 +0100 +++ b/src/HOL/Tools/BNF/bnf_fp_def_sugar.ML Mon Feb 17 22:54:38 2014 +0100 @@ -10,22 +10,21 @@ type fp_sugar = {T: typ, fp: BNF_FP_Util.fp_kind, - index: int, - pre_bnfs: BNF_Def.bnf list, + fp_res_index: int, + fp_res: BNF_FP_Util.fp_result, + pre_bnf: BNF_Def.bnf, nested_bnfs: BNF_Def.bnf list, nesting_bnfs: BNF_Def.bnf list, - fp_res: BNF_FP_Util.fp_result, - ctr_defss: thm list list, - ctr_sugars: Ctr_Sugar.ctr_sugar list, - co_iterss: term list list, - mapss: thm list list, + ctr_defs: thm list, + ctr_sugar: Ctr_Sugar.ctr_sugar, + co_iters: term list, + maps: thm list, + common_co_inducts: thm list, co_inducts: thm list, - co_inductss: thm list list, - co_iter_thmsss: thm list list list, - disc_co_itersss: thm list list list, - sel_co_iterssss: thm list list list list}; + co_iter_thmss: thm list list, + disc_co_iterss: thm list list, + sel_co_itersss: thm list list list}; - val of_fp_sugar: (fp_sugar -> 'a list) -> fp_sugar -> 'a val morph_fp_sugar: morphism -> fp_sugar -> fp_sugar val transfer_fp_sugar: Proof.context -> fp_sugar -> fp_sugar val fp_sugar_of: Proof.context -> string -> fp_sugar option @@ -122,38 +121,40 @@ type fp_sugar = {T: typ, fp: fp_kind, - index: int, - pre_bnfs: bnf list, + fp_res_index: int, + fp_res: fp_result, + pre_bnf: bnf, nested_bnfs: bnf list, nesting_bnfs: bnf list, - fp_res: fp_result, - ctr_defss: thm list list, - ctr_sugars: ctr_sugar list, - co_iterss: term list list, - mapss: thm list list, + ctr_defs: thm list, + ctr_sugar: Ctr_Sugar.ctr_sugar, + co_iters: term list, + maps: thm list, + common_co_inducts: thm list, co_inducts: thm list, - co_inductss: thm list list, - co_iter_thmsss: thm list list list, - disc_co_itersss: thm list list list, - sel_co_iterssss: thm list list list list}; - -fun of_fp_sugar f (fp_sugar as ({index, ...}: fp_sugar)) = nth (f fp_sugar) index; + co_iter_thmss: thm list list, + disc_co_iterss: thm list list, + sel_co_itersss: thm list list list}; -fun morph_fp_sugar phi ({T, fp, index, pre_bnfs, nested_bnfs, nesting_bnfs, fp_res, ctr_defss, - ctr_sugars, co_iterss, mapss, co_inducts, co_inductss, co_iter_thmsss, disc_co_itersss, - sel_co_iterssss} : fp_sugar) = - {T = Morphism.typ phi T, fp = fp, index = index, pre_bnfs = map (morph_bnf phi) pre_bnfs, - nested_bnfs = map (morph_bnf phi) nested_bnfs, nesting_bnfs = map (morph_bnf phi) nesting_bnfs, +fun morph_fp_sugar phi ({T, fp, fp_res, fp_res_index, pre_bnf, nested_bnfs, nesting_bnfs, ctr_defs, + ctr_sugar, co_iters, maps, common_co_inducts, co_inducts, co_iter_thmss, disc_co_iterss, + sel_co_itersss} : fp_sugar) = + {T = Morphism.typ phi T, + fp = fp, fp_res = morph_fp_result phi fp_res, - ctr_defss = map (map (Morphism.thm phi)) ctr_defss, - ctr_sugars = map (morph_ctr_sugar phi) ctr_sugars, - co_iterss = map (map (Morphism.term phi)) co_iterss, - mapss = map (map (Morphism.thm phi)) mapss, + fp_res_index = fp_res_index, + pre_bnf = morph_bnf phi pre_bnf, + nested_bnfs = map (morph_bnf phi) nested_bnfs, + nesting_bnfs = map (morph_bnf phi) nesting_bnfs, + ctr_defs = map (Morphism.thm phi) ctr_defs, + ctr_sugar = morph_ctr_sugar phi ctr_sugar, + co_iters = map (Morphism.term phi) co_iters, + maps = map (Morphism.thm phi) maps, + common_co_inducts = map (Morphism.thm phi) common_co_inducts, co_inducts = map (Morphism.thm phi) co_inducts, - co_inductss = map (map (Morphism.thm phi)) co_inductss, - co_iter_thmsss = map (map (map (Morphism.thm phi))) co_iter_thmsss, - disc_co_itersss = map (map (map (Morphism.thm phi))) disc_co_itersss, - sel_co_iterssss = map (map (map (map (Morphism.thm phi)))) sel_co_iterssss}; + co_iter_thmss = map (map (Morphism.thm phi)) co_iter_thmss, + disc_co_iterss = map (map (Morphism.thm phi)) disc_co_iterss, + sel_co_itersss = map (map (map (Morphism.thm phi))) sel_co_itersss}; val transfer_fp_sugar = morph_fp_sugar o Morphism.transfer_morphism o Proof_Context.theory_of; @@ -183,15 +184,16 @@ (fn phi => Data.map (Symtab.update (key, morph_fp_sugar phi fp_sugar))); fun register_fp_sugars fp pre_bnfs nested_bnfs nesting_bnfs (fp_res as {Ts, ...}) ctr_defss - ctr_sugars co_iterss mapss co_inducts co_inductss co_iter_thmsss disc_co_itersss + ctr_sugars co_iterss mapss common_co_inducts co_inductss co_iter_thmsss disc_co_itersss sel_co_iterssss lthy = (0, lthy) |> fold (fn T as Type (s, _) => fn (kk, lthy) => (kk + 1, - register_fp_sugar s {T = T, fp = fp, index = kk, pre_bnfs = pre_bnfs, nested_bnfs = nested_bnfs, - nesting_bnfs = nesting_bnfs, fp_res = fp_res, ctr_defss = ctr_defss, - ctr_sugars = ctr_sugars, co_iterss = co_iterss, mapss = mapss, co_inducts = co_inducts, - co_inductss = co_inductss, co_iter_thmsss = co_iter_thmsss, - disc_co_itersss = disc_co_itersss, sel_co_iterssss = sel_co_iterssss} + register_fp_sugar s {T = T, fp = fp, fp_res = fp_res, fp_res_index = kk, + pre_bnf = nth pre_bnfs kk, nested_bnfs = nested_bnfs, nesting_bnfs = nesting_bnfs, + ctr_defs = nth ctr_defss kk, ctr_sugar = nth ctr_sugars kk, co_iters = nth co_iterss kk, + maps = nth mapss kk, common_co_inducts = common_co_inducts, co_inducts = nth co_inductss kk, + co_iter_thmss = nth co_iter_thmsss kk, disc_co_iterss = nth disc_co_itersss kk, + sel_co_itersss = nth sel_co_iterssss kk} lthy)) Ts |> snd; @@ -1407,8 +1409,8 @@ |> Spec_Rules.add Spec_Rules.Equational (map co_rec_of iterss, flat rec_thmss) |> Local_Theory.notes (common_notes @ notes) |> snd |> register_fp_sugars Least_FP pre_bnfs nested_bnfs nesting_bnfs fp_res ctr_defss ctr_sugars - iterss mapss [induct_thm] (transpose [induct_thms]) (transpose [fold_thmss, rec_thmss]) - [] [] + iterss mapss [induct_thm] (map single induct_thms) (transpose [fold_thmss, rec_thmss]) + (replicate nn []) (replicate nn []) end; fun derive_note_coinduct_coiters_thms_for_types diff -r 6a5986170c1d -r 0819931d652d src/HOL/Tools/BNF/bnf_fp_n2m.ML --- a/src/HOL/Tools/BNF/bnf_fp_n2m.ML Mon Feb 17 18:18:27 2014 +0100 +++ b/src/HOL/Tools/BNF/bnf_fp_n2m.ML Mon Feb 17 22:54:38 2014 +0100 @@ -47,7 +47,8 @@ fun construct_mutualized_fp fp fpTs fp_sugars bs resBs (resDs, Dss) bnfs lthy = let - fun steal get = map (of_fp_sugar (get o #fp_res)) fp_sugars; + fun steal_fp_res get = + map (fn {fp_res, fp_res_index, ...} => nth (get fp_res) fp_res_index) fp_sugars; val n = length bnfs; val deads = fold (union (op =)) Dss resDs; @@ -77,8 +78,8 @@ val ((ctors, dtors), (xtor's, xtors)) = let - val ctors = map2 (force_typ names_lthy o (fn T => dummyT --> T)) fpTs (steal #ctors); - val dtors = map2 (force_typ names_lthy o (fn T => T --> dummyT)) fpTs (steal #dtors); + val ctors = map2 (force_typ names_lthy o (fn T => dummyT --> T)) fpTs (steal_fp_res #ctors); + val dtors = map2 (force_typ names_lthy o (fn T => T --> dummyT)) fpTs (steal_fp_res #dtors); in ((ctors, dtors), `(map (Term.subst_atomic_types theta)) (fp_case fp ctors dtors)) end; @@ -92,9 +93,8 @@ ||>> mk_Frees "x" xTs ||>> mk_Frees "y" yTs; - val fp_bnfs = steal #bnfs; - val pre_bnfs = map (of_fp_sugar #pre_bnfs) fp_sugars; - val pre_bnfss = map #pre_bnfs fp_sugars; + val fp_bnfs = steal_fp_res #bnfs; + val pre_bnfs = map #pre_bnf fp_sugars; val nesty_bnfss = map (fn sugar => #nested_bnfs sugar @ #nesting_bnfs sugar) fp_sugars; val fp_nesty_bnfss = fp_bnfs :: nesty_bnfss; val fp_nesty_bnfs = distinct (op = o pairself T_of_bnf) (flat fp_nesty_bnfss); @@ -126,9 +126,9 @@ val pre_rels = map2 (fn Ds => mk_rel_of_bnf Ds (As @ fpTs) (Bs @ fpTs')) Dss bnfs; - val rel_unfoldss = map (maps (fn bnf => no_refl [rel_def_of_bnf bnf])) pre_bnfss; - val rel_xtor_co_inducts = steal (split_conj_thm o #rel_xtor_co_induct_thm) - |> map2 (fn unfs => unfold_thms lthy (id_apply :: unfs)) rel_unfoldss; + val rel_unfolds = maps (no_refl o single o rel_def_of_bnf) pre_bnfs; + val rel_xtor_co_inducts = steal_fp_res (split_conj_thm o #rel_xtor_co_induct_thm) + |> map (unfold_thms lthy (id_apply :: rel_unfolds)); val rel_defs = map rel_def_of_bnf bnfs; val rel_monos = map rel_mono_of_bnf bnfs; @@ -185,11 +185,13 @@ |> mk_Frees' "s" fold_strTs ||>> mk_Frees' "s" rec_strTs; - val co_iters = steal #xtor_co_iterss; - val ns = map (length o #pre_bnfs) fp_sugars; + val co_iters = steal_fp_res #xtor_co_iterss; + val ns = map (length o #Ts o #fp_res) fp_sugars; + fun substT rho (Type (@{type_name "fun"}, [T, U])) = substT rho T --> substT rho U | substT rho (Type (s, Ts)) = Type (s, map (typ_subst_nonatomic rho) Ts) | substT _ T = T; + fun force_iter is_rec i TU TU_rec raw_iters = let val approx_fold = un_fold_of raw_iters @@ -325,14 +327,14 @@ val pre_map_defs = no_refl (map map_def_of_bnf bnfs); val fp_pre_map_defs = no_refl (map map_def_of_bnf pre_bnfs); - val map_unfoldss = map (maps (fn bnf => no_refl [map_def_of_bnf bnf])) pre_bnfss; - val unfold_map = map2 (fn unfs => unfold_thms lthy (id_apply :: unfs)) map_unfoldss; + val map_unfolds = maps (fn bnf => no_refl [map_def_of_bnf bnf]) pre_bnfs; + val unfold_map = map (unfold_thms lthy (id_apply :: map_unfolds)); - val fp_xtor_co_iterss = steal #xtor_co_iter_thmss; + val fp_xtor_co_iterss = steal_fp_res #xtor_co_iter_thmss; val fp_xtor_un_folds = map (mk_pointfree lthy o un_fold_of) fp_xtor_co_iterss |> unfold_map; val fp_xtor_co_recs = map (mk_pointfree lthy o co_rec_of) fp_xtor_co_iterss |> unfold_map; - val fp_co_iter_o_mapss = steal #xtor_co_iter_o_map_thmss; + val fp_co_iter_o_mapss = steal_fp_res #xtor_co_iter_o_map_thmss; val fp_fold_o_maps = map un_fold_of fp_co_iter_o_mapss |> unfold_map; val fp_rec_o_maps = map co_rec_of fp_co_iter_o_mapss |> unfold_map; val fold_thms = fp_case fp @{thm comp_assoc} @{thm comp_assoc[symmetric]} :: @{thms id_apply @@ -358,20 +360,21 @@ used by "primrec", "primcorecursive", and "datatype_compat". *) val fp_res = ({Ts = fpTs, - bnfs = steal #bnfs, + bnfs = steal_fp_res #bnfs, dtors = dtors, ctors = ctors, xtor_co_iterss = transpose [un_folds, co_recs], xtor_co_induct = xtor_co_induct_thm, - dtor_ctors = steal #dtor_ctors (*too general types*), - ctor_dtors = steal #ctor_dtors (*too general types*), - ctor_injects = steal #ctor_injects (*too general types*), - dtor_injects = steal #dtor_injects (*too general types*), - xtor_map_thms = steal #xtor_map_thms (*too general types and terms*), - xtor_set_thmss = steal #xtor_set_thmss (*too general types and terms*), - xtor_rel_thms = steal #xtor_rel_thms (*too general types and terms*), + dtor_ctors = steal_fp_res #dtor_ctors (*too general types*), + ctor_dtors = steal_fp_res #ctor_dtors (*too general types*), + ctor_injects = steal_fp_res #ctor_injects (*too general types*), + dtor_injects = steal_fp_res #dtor_injects (*too general types*), + xtor_map_thms = steal_fp_res #xtor_map_thms (*too general types and terms*), + xtor_set_thmss = steal_fp_res #xtor_set_thmss (*too general types and terms*), + xtor_rel_thms = steal_fp_res #xtor_rel_thms (*too general types and terms*), xtor_co_iter_thmss = transpose [xtor_un_fold_thms, xtor_co_rec_thms], - xtor_co_iter_o_map_thmss = steal #xtor_co_iter_o_map_thmss (*theorem about old constant*), + xtor_co_iter_o_map_thmss = steal_fp_res #xtor_co_iter_o_map_thmss + (*theorem about old constant*), rel_xtor_co_induct_thm = rel_xtor_co_induct_thm} |> morph_fp_result (Morphism.term_morphism "BNF" (singleton (Variable.polymorphic lthy)))); in diff -r 6a5986170c1d -r 0819931d652d src/HOL/Tools/BNF/bnf_fp_n2m_sugar.ML --- a/src/HOL/Tools/BNF/bnf_fp_n2m_sugar.ML Mon Feb 17 18:18:27 2014 +0100 +++ b/src/HOL/Tools/BNF/bnf_fp_n2m_sugar.ML Mon Feb 17 22:54:38 2014 +0100 @@ -119,17 +119,18 @@ val fp_b_names = map base_name_of_typ fpTs; val nn = length fpTs; + val kks = 0 upto nn - 1; - fun target_ctr_sugar_of_fp_sugar fpT ({T, index, ctr_sugars, ...} : fp_sugar) = + fun target_ctr_sugar_of_fp_sugar fpT ({T, ctr_sugar, ...} : fp_sugar) = let val rho = Vartab.fold (cons o apsnd snd) (Sign.typ_match thy (T, fpT) Vartab.empty) []; val phi = Morphism.term_morphism "BNF" (Term.subst_TVars rho); in - morph_ctr_sugar phi (nth ctr_sugars index) + morph_ctr_sugar phi ctr_sugar end; - val ctr_defss = map (of_fp_sugar #ctr_defss) fp_sugars0; - val mapss = map (of_fp_sugar #mapss) fp_sugars0; + val ctr_defss = map #ctr_defs fp_sugars0; + val mapss = map #maps fp_sugars0; val ctr_sugars = map2 target_ctr_sugar_of_fp_sugar fpTs fp_sugars0; val ctrss = map #ctrs ctr_sugars; @@ -215,14 +216,15 @@ (mk_binding b) fpTs Cs) fp_bs xtor_co_iterss lthy |>> split_list; - val ((co_inducts, co_inductss, un_fold_thmss, co_rec_thmss, disc_unfold_thmss, + val ((common_co_inducts, co_inductss, un_fold_thmss, co_rec_thmss, disc_unfold_thmss, disc_corec_thmss, sel_unfold_thmsss, sel_corec_thmsss), fp_sugar_thms) = if fp = Least_FP then derive_induct_iters_thms_for_types pre_bnfs (the iters_args_types) xtor_co_induct xtor_co_iter_thmss nesting_bnfs nested_bnfs fpTs Cs Xs ctrXs_Tsss ctrss ctr_defss co_iterss co_iter_defss lthy |> `(fn ((inducts, induct, _), (fold_thmss, rec_thmss, _)) => - ([induct], [inducts], fold_thmss, rec_thmss, [], [], [], [])) + ([induct], [inducts], fold_thmss, rec_thmss, replicate nn [], + replicate nn [], replicate nn [], replicate nn [])) ||> (fn info => (SOME info, NONE)) else derive_coinduct_coiters_thms_for_types pre_bnfs (the coiters_args_types) xtor_co_induct @@ -232,32 +234,38 @@ |> `(fn ((coinduct_thms_pairs, _), (unfold_thmss, corec_thmss, _), (disc_unfold_thmss, disc_corec_thmss, _), _, (sel_unfold_thmsss, sel_corec_thmsss, _)) => - (map snd coinduct_thms_pairs, map fst coinduct_thms_pairs, unfold_thmss, corec_thmss, - disc_unfold_thmss, disc_corec_thmss, sel_unfold_thmsss, sel_corec_thmsss)) + (map snd coinduct_thms_pairs, map fst coinduct_thms_pairs, unfold_thmss, + corec_thmss, disc_unfold_thmss, disc_corec_thmss, sel_unfold_thmsss, + sel_corec_thmsss)) ||> (fn info => (NONE, SOME info)); val phi = Proof_Context.export_morphism no_defs_lthy no_defs_lthy0; - fun mk_target_fp_sugar (kk, T) = - {T = T, fp = fp, index = kk, pre_bnfs = pre_bnfs, nested_bnfs = nested_bnfs, - nesting_bnfs = nesting_bnfs, fp_res = fp_res, ctr_defss = ctr_defss, - ctr_sugars = ctr_sugars, co_iterss = co_iterss, mapss = mapss, co_inducts = co_inducts, - co_inductss = transpose co_inductss, - co_iter_thmsss = transpose [un_fold_thmss, co_rec_thmss], - disc_co_itersss = transpose [disc_unfold_thmss, disc_corec_thmss], - sel_co_iterssss = transpose [sel_unfold_thmsss, sel_corec_thmsss]} + fun mk_target_fp_sugar T kk pre_bnf ctr_defs ctr_sugar co_iters maps co_inducts un_fold_thms + co_rec_thms disc_unfold_thms disc_corec_thms sel_unfold_thmss sel_corec_thmss = + {T = T, fp = fp, fp_res = fp_res, fp_res_index = kk, pre_bnf = pre_bnf, + nested_bnfs = nested_bnfs, nesting_bnfs = nesting_bnfs, ctr_defs = ctr_defs, + ctr_sugar = ctr_sugar, co_iters = co_iters, maps = maps, + common_co_inducts = common_co_inducts, co_inducts = co_inducts, + co_iter_thmss = [un_fold_thms, co_rec_thms], + disc_co_iterss = [disc_unfold_thms, disc_corec_thms], + sel_co_itersss = [sel_unfold_thmss, sel_corec_thmss]} |> morph_fp_sugar phi; - val n2m_sugar = (map_index mk_target_fp_sugar fpTs, fp_sugar_thms); + val target_fp_sugars = + map14 mk_target_fp_sugar fpTs kks pre_bnfs ctr_defss ctr_sugars co_iterss mapss + (transpose co_inductss) un_fold_thmss co_rec_thmss disc_unfold_thmss disc_corec_thmss + sel_unfold_thmsss sel_corec_thmsss; + + val n2m_sugar = (target_fp_sugars, fp_sugar_thms); in (n2m_sugar, lthy |> register_n2m_sugar key n2m_sugar) end) end; (* TODO: needed? *) -fun indexify_callsss fp_sugar callsss = +fun indexify_callsss (fp_sugar as {ctr_sugar = {ctrs, ...}, ...} : fp_sugar) callsss = let - val {ctrs, ...} = of_fp_sugar #ctr_sugars fp_sugar; fun indexify_ctr ctr = (case AList.lookup Term.aconv_untyped callsss ctr of NONE => replicate (num_binder_types (fastype_of ctr)) [] diff -r 6a5986170c1d -r 0819931d652d src/HOL/Tools/BNF/bnf_gfp_rec_sugar.ML --- a/src/HOL/Tools/BNF/bnf_gfp_rec_sugar.ML Mon Feb 17 18:18:27 2014 +0100 +++ b/src/HOL/Tools/BNF/bnf_gfp_rec_sugar.ML Mon Feb 17 22:54:38 2014 +0100 @@ -367,9 +367,7 @@ | _ => not_codatatype ctxt res_T); fun map_thms_of_typ ctxt (Type (s, _)) = - (case fp_sugar_of ctxt s of - SOME {index, mapss, ...} => nth mapss index - | NONE => []) + (case fp_sugar_of ctxt s of SOME {maps, ...} => maps | NONE => []) | map_thms_of_typ _ _ = []; fun corec_specs_of bs arg_Ts res_Ts get_indices callssss0 lthy0 = @@ -378,15 +376,15 @@ val ((missing_res_Ts, perm0_kks, fp_sugars as {nested_bnfs, fp_res = {xtor_co_iterss = dtor_coiters1 :: _, ...}, - co_inducts = coinduct_thms, ...} :: _, (_, gfp_sugar_thms)), lthy) = + common_co_inducts = common_coinduct_thms, ...} :: _, (_, gfp_sugar_thms)), lthy) = nested_to_mutual_fps Greatest_FP bs res_Ts get_indices callssss0 lthy0; - val perm_fp_sugars = sort (int_ord o pairself #index) fp_sugars; + val perm_fp_sugars = sort (int_ord o pairself #fp_res_index) fp_sugars; - val indices = map #index fp_sugars; - val perm_indices = map #index perm_fp_sugars; + val indices = map #fp_res_index fp_sugars; + val perm_indices = map #fp_res_index perm_fp_sugars; - val perm_ctrss = map (#ctrs o of_fp_sugar #ctr_sugars) perm_fp_sugars; + val perm_ctrss = map (#ctrs o #ctr_sugar) perm_fp_sugars; val perm_ctr_Tsss = map (map (binder_types o fastype_of)) perm_ctrss; val perm_gfpTs = map (body_type o fastype_of o hd) perm_ctrss; @@ -395,8 +393,8 @@ val kks = 0 upto nn - 1; val perm_ns = map length perm_ctr_Tsss; - val perm_Cs = map (domain_type o body_fun_type o fastype_of o co_rec_of o - of_fp_sugar (#xtor_co_iterss o #fp_res)) perm_fp_sugars; + val perm_Cs = map (fn {fp_res, fp_res_index, ...} => domain_type (body_fun_type (fastype_of + (co_rec_of (nth (#xtor_co_iterss fp_res) fp_res_index))))) perm_fp_sugars; val (perm_p_Tss, (perm_q_Tssss, _, perm_f_Tssss, _)) = mk_coiter_fun_arg_types perm_ctr_Tsss perm_Cs perm_ns (co_rec_of dtor_coiters1); @@ -410,7 +408,7 @@ fun unpermute0 perm0_xs = permute_like_unique (op =) perm0_kks kks perm0_xs; fun unpermute perm_xs = permute_like_unique (op =) perm_indices indices perm_xs; - val coinduct_thmss = map (unpermute0 o conj_dests nn) coinduct_thms; + val coinduct_thmss = map (unpermute0 o conj_dests nn) common_coinduct_thms; val p_iss = map (map (find_index_eq fun_arg_hs)) (unpermute perm_p_hss); val q_issss = map (map (map (map (find_index_eq fun_arg_hs)))) (unpermute perm_q_hssss); @@ -444,35 +442,32 @@ disc_corec = disc_corec, sel_corecs = sel_corecs} end; - fun mk_ctr_specs index ctr_sugars p_is q_isss f_isss f_Tsss coiter_thmsss disc_coitersss - sel_coiterssss = + fun mk_ctr_specs ({ctrs, discs, selss, discIs, sel_thmss, disc_excludesss, collapses, ...} + : ctr_sugar) p_is q_isss f_isss f_Tsss coiter_thmss disc_coiterss sel_coitersss = let - val {ctrs, discs, selss, discIs, sel_thmss, disc_excludesss, collapses, ...} : ctr_sugar = - nth ctr_sugars index; val p_ios = map SOME p_is @ [NONE]; - val discIs = #discIs (nth ctr_sugars index); - val corec_thms = co_rec_of (nth coiter_thmsss index); - val disc_corecs = co_rec_of (nth disc_coitersss index); - val sel_corecss = co_rec_of (nth sel_coiterssss index); + val corec_thms = co_rec_of coiter_thmss; + val disc_corecs = co_rec_of disc_coiterss; + val sel_corecss = co_rec_of sel_coitersss; in map14 mk_ctr_spec ctrs discs selss p_ios q_isss f_isss f_Tsss discIs sel_thmss disc_excludesss collapses corec_thms disc_corecs sel_corecss end; - fun mk_spec ({T, index, ctr_sugars, co_iterss = coiterss, co_iter_thmsss = coiter_thmsss, - disc_co_itersss = disc_coitersss, sel_co_iterssss = sel_coiterssss, ...} : fp_sugar) - p_is q_isss f_isss f_Tsss = - {corec = mk_co_iter thy Greatest_FP (substAT T) perm_Cs' (co_rec_of (nth coiterss index)), - disc_exhausts = #disc_exhausts (nth ctr_sugars index), + fun mk_spec ({T, ctr_sugar as {disc_exhausts, ...}, co_iters = coiters, + co_iter_thmss = coiter_thmss, disc_co_iterss = disc_coiterss, + sel_co_itersss = sel_coitersss, ...} : fp_sugar) p_is q_isss f_isss f_Tsss = + {corec = mk_co_iter thy Greatest_FP (substAT T) perm_Cs' (co_rec_of coiters), + disc_exhausts = disc_exhausts, nested_maps = maps (map_thms_of_typ lthy o T_of_bnf) nested_bnfs, nested_map_idents = map (unfold_thms lthy @{thms id_def} o map_id0_of_bnf) nested_bnfs, nested_map_comps = map map_comp_of_bnf nested_bnfs, - ctr_specs = mk_ctr_specs index ctr_sugars p_is q_isss f_isss f_Tsss coiter_thmsss - disc_coitersss sel_coiterssss}; + ctr_specs = mk_ctr_specs ctr_sugar p_is q_isss f_isss f_Tsss coiter_thmss disc_coiterss + sel_coitersss}; in ((is_some gfp_sugar_thms, map5 mk_spec fp_sugars p_iss q_issss f_issss f_Tssss, missing_res_Ts, - co_induct_of coinduct_thms, strong_co_induct_of coinduct_thms, co_induct_of coinduct_thmss, - strong_co_induct_of coinduct_thmss), lthy) + co_induct_of common_coinduct_thms, strong_co_induct_of common_coinduct_thms, + co_induct_of coinduct_thmss, strong_co_induct_of coinduct_thmss), lthy) end; val undef_const = Const (@{const_name undefined}, dummyT); diff -r 6a5986170c1d -r 0819931d652d src/HOL/Tools/BNF/bnf_lfp_compat.ML --- a/src/HOL/Tools/BNF/bnf_lfp_compat.ML Mon Feb 17 18:18:27 2014 +0100 +++ b/src/HOL/Tools/BNF/bnf_lfp_compat.ML Mon Feb 17 22:54:38 2014 +0100 @@ -2,7 +2,7 @@ Author: Jasmin Blanchette, TU Muenchen Copyright 2013 -Compatibility layer with the old datatype package. +Compatibility layer with the old datatype package ("datatype_compat"). *) signature BNF_LFP_COMPAT = @@ -32,7 +32,7 @@ fun not_mutually_recursive ss = error ("{" ^ commas ss ^ "} is not a complete set of mutually recursive new-style datatypes"); - val (fpT_names as fpT_name1 :: _) = + val fpT_names = map (fst o dest_Type o Proof_Context.read_type_name_proper lthy false) raw_fpT_names; fun lfp_sugar_of s = @@ -40,7 +40,7 @@ SOME (fp_sugar as {fp = Least_FP, ...}) => fp_sugar | _ => not_datatype s); - val {ctr_sugars = fp_ctr_sugars, ...} = lfp_sugar_of fpT_name1; + val fp_ctr_sugars = map (#ctr_sugar o lfp_sugar_of) fpT_names; val fpTs0 as Type (_, var_As) :: _ = map (body_type o fastype_of o hd o #ctrs) fp_ctr_sugars; val fpT_names' = map (fst o dest_Type) fpTs0; @@ -52,7 +52,7 @@ fun nested_Tparentss_indicessss_of parent_Tkks (T as Type (s, _)) kk = (case try lfp_sugar_of s of - SOME ({T = T0, fp_res = {Ts = mutual_Ts0, ...}, ctr_sugars, ...}) => + SOME ({T = T0, fp_res = {Ts = mutual_Ts0, ...}, ...}) => let val rho = Vartab.fold (cons o apsnd snd) (Sign.typ_match thy (T0, T) Vartab.empty) []; val substT = Term.typ_subst_TVars rho; @@ -88,7 +88,7 @@ #>> pair parent_Tkks' end; - val ctrss = map #ctrs ctr_sugars; + val ctrss = map (#ctrs o #ctr_sugar o lfp_sugar_of o fst o dest_Type) mutual_Ts; val ctr_Tsss = map (map (binder_types o substT o fastype_of)) ctrss; in ([], kk + mutual_nn) @@ -107,7 +107,7 @@ val kkssss = map snd Tparentss_kkssss; val fp_sugars0 = map (lfp_sugar_of o fst o dest_Type) Ts; - val ctrss0 = map (#ctrs o of_fp_sugar #ctr_sugars) fp_sugars0; + val ctrss0 = map (#ctrs o #ctr_sugar) fp_sugars0; val ctr_Tsss0 = map (map (binder_types o fastype_of)) ctrss0; fun apply_comps n kk = @@ -132,9 +132,8 @@ else ((fp_sugars0, (NONE, NONE)), lthy); - val {ctr_sugars, co_inducts = [induct], co_inductss = inductss, co_iterss, - co_iter_thmsss = iter_thmsss, ...} :: _ = fp_sugars; - val inducts = map the_single inductss; + val {co_inducts = [induct], ...} :: _ = fp_sugars; + val inducts = map (the_single o #co_inducts) fp_sugars; fun mk_dtyp [] (TFree a) = Datatype_Aux.DtTFree a | mk_dtyp [] (Type (s, Ts)) = Datatype_Aux.DtType (s, map (mk_dtyp []) Ts) @@ -148,23 +147,19 @@ (kk, (T_name, map (mk_dtyp (map snd (take 1 parents))) Ts, map2 (mk_ctr_descr Ts) kksss ctrs0)); val descr = map3 mk_typ_descr kkssss Tparentss ctrss0; - val recs = map (fst o dest_Const o co_rec_of) co_iterss; - val rec_thms = flat (map co_rec_of iter_thmsss); + val recs = map (fst o dest_Const o co_rec_of o #co_iters) fp_sugars; + val rec_thms = maps (co_rec_of o #co_iter_thmss) fp_sugars; - fun mk_info ({T = Type (T_name0, _), index, ...} : fp_sugar) = - let - val {casex, exhaust, nchotomy, injects, distincts, case_thms, case_cong, weak_case_cong, - split, split_asm, ...} = nth ctr_sugars index; - in - (T_name0, - {index = index, descr = descr, inject = injects, distinct = distincts, induct = induct, - inducts = inducts, exhaust = exhaust, nchotomy = nchotomy, rec_names = recs, - rec_rewrites = rec_thms, case_name = fst (dest_Const casex), case_rewrites = case_thms, - case_cong = case_cong, weak_case_cong = weak_case_cong, split = split, - split_asm = split_asm}) - end; + fun mk_info (kk, {T = Type (T_name0, _), ctr_sugar as {casex, exhaust, nchotomy, injects, + distincts, case_thms, case_cong, weak_case_cong, split, split_asm, ...}, ...} : fp_sugar) = + (T_name0, + {index = kk, descr = descr, inject = injects, distinct = distincts, induct = induct, + inducts = inducts, exhaust = exhaust, nchotomy = nchotomy, rec_names = recs, + rec_rewrites = rec_thms, case_name = fst (dest_Const casex), case_rewrites = case_thms, + case_cong = case_cong, weak_case_cong = weak_case_cong, split = split, + split_asm = split_asm}); - val infos = map mk_info (take nn_fp fp_sugars); + val infos = map_index mk_info (take nn_fp fp_sugars); val all_notes = (case lfp_sugar_thms of diff -r 6a5986170c1d -r 0819931d652d src/HOL/Tools/BNF/bnf_lfp_rec_sugar.ML --- a/src/HOL/Tools/BNF/bnf_lfp_rec_sugar.ML Mon Feb 17 18:18:27 2014 +0100 +++ b/src/HOL/Tools/BNF/bnf_lfp_rec_sugar.ML Mon Feb 17 22:54:38 2014 +0100 @@ -136,20 +136,17 @@ type basic_lfp_sugar = {T: typ, - index: int, - ctor_iterss: term list list, - ctr_defss: thm list list, - ctr_sugars: Ctr_Sugar.ctr_sugar list, - iterss: term list list, - iter_thmsss: thm list list list}; + fp_res_index: int, + ctor_iters: term list, + ctr_defs: thm list, + ctr_sugar: ctr_sugar, + iters: term list, + iter_thmss: thm list list}; -fun basic_lfp_sugar_of ({T, index, fp_res = {xtor_co_iterss = ctor_iterss, ...}, ctr_defss, - ctr_sugars, co_iterss = iterss, co_iter_thmsss = iter_thmsss, ...} : fp_sugar) = - {T = T, index = index, ctor_iterss = ctor_iterss, ctr_defss = ctr_defss, - ctr_sugars = ctr_sugars, iterss = iterss, iter_thmsss = iter_thmsss}; - -fun of_basic_lfp_sugar f (basic_lfp_sugar as ({index, ...} : basic_lfp_sugar)) = - nth (f basic_lfp_sugar) index; +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_iters = nth ctor_iterss fp_res_index, + ctr_defs = ctr_defs, ctr_sugar = ctr_sugar, iters = iters, iter_thmss = iter_thmss}; fun get_basic_lfp_sugars bs arg_Ts get_indices callssss0 lthy0 = let @@ -172,23 +169,24 @@ ctor_iters1, induct_thm, lfp_sugar_thms, lthy) = get_basic_lfp_sugars bs arg_Ts get_indices callssss0 lthy0; - val perm_basic_lfp_sugars = sort (int_ord o pairself #index) basic_lfp_sugars; + val perm_basic_lfp_sugars = sort (int_ord o pairself #fp_res_index) basic_lfp_sugars; - val indices = map #index basic_lfp_sugars; - val perm_indices = map #index perm_basic_lfp_sugars; + val indices = map #fp_res_index basic_lfp_sugars; + val perm_indices = map #fp_res_index perm_basic_lfp_sugars; - val perm_ctrss = map (#ctrs o of_basic_lfp_sugar #ctr_sugars) perm_basic_lfp_sugars; + val perm_ctrss = map (#ctrs o #ctr_sugar) perm_basic_lfp_sugars; val perm_ctr_Tsss = map (map (binder_types o fastype_of)) perm_ctrss; - val perm_lfpTs = map (body_type o fastype_of o hd) perm_ctrss; val nn0 = length arg_Ts; - val nn = length perm_lfpTs; + val nn = length perm_ctrss; val kks = 0 upto nn - 1; + val perm_ns = map length perm_ctr_Tsss; val perm_mss = map (map length) perm_ctr_Tsss; + val perm_ctr_offsets = map (fn kk => Integer.sum (map length (take kk perm_ctrss))) kks; - val perm_Cs = map (body_type o fastype_of o co_rec_of o of_basic_lfp_sugar #ctor_iterss) - perm_basic_lfp_sugars; + val perm_lfpTs = map (body_type o fastype_of o hd) perm_ctrss; + val perm_Cs = map (body_type o fastype_of o co_rec_of o #ctor_iters) perm_basic_lfp_sugars; val perm_fun_arg_Tssss = mk_iter_fun_arg_types perm_ctr_Tsss perm_ns perm_mss (co_rec_of ctor_iters1); @@ -199,6 +197,7 @@ val lfpTs = unpermute perm_lfpTs; val Cs = unpermute perm_Cs; + val ctr_offsets = unpermute perm_ctr_offsets; val As_rho = tvar_subst thy (take nn0 lfpTs) arg_Ts; val Cs_rho = map (fst o dest_TVar) Cs ~~ pad_list HOLogic.unitT nn res_Ts; @@ -210,10 +209,6 @@ val perm_Cs' = map substCT perm_Cs; - fun offset_of_ctr 0 _ = 0 - | offset_of_ctr n (({ctrs, ...} : ctr_sugar) :: ctr_sugars) = - length ctrs + offset_of_ctr (n - 1) ctr_sugars; - fun call_of [i] [T] = (if exists_subtype_in Cs T then Nested_Rec else No_Rec) (i, substACT T) | call_of [i, i'] [T, T'] = Mutual_Rec ((i, substACT T), (i', substACT T')); @@ -227,22 +222,17 @@ rec_thm = rec_thm} end; - fun mk_ctr_specs index (ctr_sugars : ctr_sugar list) iter_thmsss = - let - val ctrs = #ctrs (nth ctr_sugars index); - val rec_thms = co_rec_of (nth iter_thmsss index); - val k = offset_of_ctr index ctr_sugars; - val n = length ctrs; - in - map4 mk_ctr_spec ctrs (k upto k + n - 1) (nth perm_fun_arg_Tssss index) rec_thms - end; + fun mk_ctr_specs fp_res_index k ctrs rec_thms = + map4 mk_ctr_spec ctrs (k upto k + length ctrs - 1) (nth perm_fun_arg_Tssss fp_res_index) + rec_thms; - fun mk_spec ({T, index, ctr_sugars, iterss, iter_thmsss, ...} : basic_lfp_sugar) = - {recx = mk_co_iter thy Least_FP (substAT T) perm_Cs' (co_rec_of (nth iterss index)), + fun mk_spec ctr_offset + ({T, fp_res_index, ctr_sugar = {ctrs, ...}, iters, iter_thmss, ...} : basic_lfp_sugar) = + {recx = mk_co_iter thy Least_FP (substAT T) perm_Cs' (co_rec_of iters), nested_map_idents = nested_map_idents, nested_map_comps = nested_map_comps, - ctr_specs = mk_ctr_specs index ctr_sugars iter_thmsss}; + ctr_specs = mk_ctr_specs fp_res_index ctr_offset ctrs (co_rec_of iter_thmss)}; in - ((is_some lfp_sugar_thms, map mk_spec basic_lfp_sugars, missing_arg_Ts, induct_thm, + ((is_some lfp_sugar_thms, map2 mk_spec ctr_offsets basic_lfp_sugars, missing_arg_Ts, induct_thm, induct_thms), lthy) end; @@ -529,10 +519,11 @@ val actual_nn = length funs_data; - val _ = let val ctrs = (maps (map #ctr o #ctr_specs) rec_specs) in + val ctrs = maps (map #ctr o #ctr_specs) rec_specs; + val _ = map (fn {ctr, user_eqn, ...} => member (op =) ctrs ctr orelse primrec_error_eqn ("argument " ^ quote (Syntax.string_of_term lthy ctr) ^ - " is not a constructor in left-hand side") user_eqn) eqns_data end; + " is not a constructor in left-hand side") user_eqn) eqns_data; val defs = build_defs lthy bs mxs funs_data rec_specs has_call; diff -r 6a5986170c1d -r 0819931d652d src/HOL/Tools/Nitpick/nitpick.ML --- a/src/HOL/Tools/Nitpick/nitpick.ML Mon Feb 17 18:18:27 2014 +0100 +++ b/src/HOL/Tools/Nitpick/nitpick.ML Mon Feb 17 22:54:38 2014 +0100 @@ -1059,8 +1059,8 @@ (* Give the inner timeout a chance. *) val timeout_bonus = seconds 1.0 -fun pick_nits_in_term state (params as {debug, timeout, expect, ...}) mode i n - step subst def_assm_ts nondef_assm_ts orig_t = +fun pick_nits_in_term state (params as {timeout, expect, ...}) mode i n step + subst def_assm_ts nondef_assm_ts orig_t = let val print_nt = if is_mode_nt mode then Output.urgent_message else K () val print_t = if mode = TPTP then Output.urgent_message else K () diff -r 6a5986170c1d -r 0819931d652d src/HOL/Tools/Nitpick/nitpick_hol.ML --- a/src/HOL/Tools/Nitpick/nitpick_hol.ML Mon Feb 17 18:18:27 2014 +0100 +++ b/src/HOL/Tools/Nitpick/nitpick_hol.ML Mon Feb 17 22:54:38 2014 +0100 @@ -791,8 +791,7 @@ val ctrs2 = (case BNF_FP_Def_Sugar.fp_sugar_of ctxt co_s of SOME (fp_sugar as {fp = BNF_FP_Util.Greatest_FP, ...}) => - map dest_Const - (#ctrs (BNF_FP_Def_Sugar.of_fp_sugar #ctr_sugars fp_sugar)) + map dest_Const (#ctrs (#ctr_sugar fp_sugar)) | _ => []) in exists (fn (s', T') => s = s' andalso repair_constr_type coT T' = T) @@ -937,7 +936,7 @@ (case BNF_FP_Def_Sugar.fp_sugar_of ctxt s of SOME (fp_sugar as {fp = BNF_FP_Util.Greatest_FP, ...}) => map (apsnd (repair_constr_type T) o dest_Const) - (#ctrs (BNF_FP_Def_Sugar.of_fp_sugar #ctr_sugars fp_sugar)) + (#ctrs (#ctr_sugar fp_sugar)) | _ => if is_frac_type ctxt T then case typedef_info ctxt s of @@ -1465,12 +1464,12 @@ |> the |> #3 |> length)) (Datatype.get_all thy) [] @ map (apsnd length o snd) (#codatatypes (Data.get (Context.Proof ctxt))) @ - maps (fn {fp, ctr_sugars, ...} => - if fp = BNF_FP_Util.Greatest_FP then - map (apsnd num_binder_types o dest_Const o #casex) ctr_sugars - else - []) - (BNF_FP_Def_Sugar.fp_sugars_of ctxt) + map_filter (fn {fp, ctr_sugar = {casex, ...}, ...} => + if fp = BNF_FP_Util.Greatest_FP then + SOME (apsnd num_binder_types (dest_Const casex)) + else + NONE) + (BNF_FP_Def_Sugar.fp_sugars_of ctxt) end fun fixpoint_kind_of_const thy table x = diff -r 6a5986170c1d -r 0819931d652d src/HOL/Tools/Nitpick/nitpick_tests.ML --- a/src/HOL/Tools/Nitpick/nitpick_tests.ML Mon Feb 17 18:18:27 2014 +0100 +++ b/src/HOL/Tools/Nitpick/nitpick_tests.ML Mon Feb 17 22:54:38 2014 +0100 @@ -31,7 +31,6 @@ val atom16_v1 = FreeName ("atom16_v1", dummy_T, Atom (16, 0)) val atom24_v1 = FreeName ("atom24_v1", dummy_T, Atom (24, 0)) val atom36_v1 = FreeName ("atom36_v1", dummy_T, Atom (36, 0)) -val atom81_v1 = FreeName ("atom81_v1", dummy_T, Atom (81, 0)) val struct_atom1_atom1_v1 = FreeName ("struct_atom1_atom1_v1", dummy_T, Struct [Atom (1, 0), Atom (1, 0)])