1(* Title: HOL/Tools/BNF/bnf_lfp_compat.ML 2 Author: Jasmin Blanchette, TU Muenchen 3 Copyright 2013, 2014 4 5Compatibility layer with the old datatype package. Partly based on 6 7 Title: HOL/Tools/Old_Datatype/old_datatype_data.ML 8 Author: Stefan Berghofer, TU Muenchen 9*) 10 11signature BNF_LFP_COMPAT = 12sig 13 datatype preference = Keep_Nesting | Include_GFPs | Kill_Type_Args 14 15 val get_all: theory -> preference list -> Old_Datatype_Aux.info Symtab.table 16 val get_info: theory -> preference list -> string -> Old_Datatype_Aux.info option 17 val the_info: theory -> preference list -> string -> Old_Datatype_Aux.info 18 val the_spec: theory -> string -> (string * sort) list * (string * typ list) list 19 val the_descr: theory -> preference list -> string list -> 20 Old_Datatype_Aux.descr * (string * sort) list * string list * string 21 * (string list * string list) * (typ list * typ list) 22 val get_constrs: theory -> string -> (string * typ) list option 23 val interpretation: string -> preference list -> 24 (Old_Datatype_Aux.config -> string list -> theory -> theory) -> theory -> theory 25 val datatype_compat: string list -> local_theory -> local_theory 26 val datatype_compat_global: string list -> theory -> theory 27 val datatype_compat_cmd: string list -> local_theory -> local_theory 28 val add_datatype: preference list -> Old_Datatype_Aux.spec list -> theory -> string list * theory 29 val primrec: (binding * typ option * mixfix) list -> Specification.multi_specs -> 30 local_theory -> (term list * thm list) * local_theory 31 val primrec_global: (binding * typ option * mixfix) list -> 32 Specification.multi_specs -> theory -> (term list * thm list) * theory 33 val primrec_overloaded: (string * (string * typ) * bool) list -> 34 (binding * typ option * mixfix) list -> Specification.multi_specs -> theory -> 35 (term list * thm list) * theory 36 val primrec_simple: ((binding * typ) * mixfix) list -> term list -> 37 local_theory -> (string list * (term list * thm list)) * local_theory 38end; 39 40structure BNF_LFP_Compat : BNF_LFP_COMPAT = 41struct 42 43open Ctr_Sugar 44open BNF_Util 45open BNF_Tactics 46open BNF_FP_Util 47open BNF_FP_Def_Sugar 48open BNF_FP_N2M_Sugar 49open BNF_LFP 50 51val compat_N = "compat_"; 52val rec_split_N = "rec_split_"; 53 54datatype preference = Keep_Nesting | Include_GFPs | Kill_Type_Args; 55 56fun mk_split_rec_rhs ctxt fpTs Cs (recs as rec1 :: _) = 57 let 58 fun repair_rec_arg_args [] [] = [] 59 | repair_rec_arg_args ((g_T as Type (\<^type_name>\<open>fun\<close>, _)) :: g_Ts) (g :: gs) = 60 let 61 val (x_Ts, body_T) = strip_type g_T; 62 in 63 (case try HOLogic.dest_prodT body_T of 64 NONE => [g] 65 | SOME (fst_T, _) => 66 if member (op =) fpTs fst_T then 67 let val (xs, _) = mk_Frees "x" x_Ts ctxt in 68 map (fn mk_proj => fold_rev Term.lambda xs (mk_proj (Term.list_comb (g, xs)))) 69 [HOLogic.mk_fst, HOLogic.mk_snd] 70 end 71 else 72 [g]) 73 :: repair_rec_arg_args g_Ts gs 74 end 75 | repair_rec_arg_args (g_T :: g_Ts) (g :: gs) = 76 if member (op =) fpTs g_T then 77 let 78 val j = find_index (member (op =) Cs) g_Ts; 79 val h = nth gs j; 80 val g_Ts' = nth_drop j g_Ts; 81 val gs' = nth_drop j gs; 82 in 83 [g, h] :: repair_rec_arg_args g_Ts' gs' 84 end 85 else 86 [g] :: repair_rec_arg_args g_Ts gs; 87 88 fun repair_back_rec_arg f_T f' = 89 let 90 val g_Ts = Term.binder_types f_T; 91 val (gs, _) = mk_Frees "g" g_Ts ctxt; 92 in 93 fold_rev Term.lambda gs (Term.list_comb (f', 94 flat_rec_arg_args (repair_rec_arg_args g_Ts gs))) 95 end; 96 97 val f_Ts = binder_fun_types (fastype_of rec1); 98 val (fs', _) = mk_Frees "f" (replicate (length f_Ts) Term.dummyT) ctxt; 99 100 fun mk_rec' recx = 101 fold_rev Term.lambda fs' (Term.list_comb (recx, map2 repair_back_rec_arg f_Ts fs')) 102 |> Syntax.check_term ctxt; 103 in 104 map mk_rec' recs 105 end; 106 107fun define_split_recs fpTs Cs recs lthy = 108 let 109 val b_names = Name.variant_list [] (map base_name_of_typ fpTs); 110 111 fun mk_binding b_name = 112 Binding.qualify true (compat_N ^ b_name) 113 (Binding.prefix_name rec_split_N (Binding.name b_name)); 114 115 val bs = map mk_binding b_names; 116 val rhss = mk_split_rec_rhs lthy fpTs Cs recs; 117 in 118 @{fold_map 3} (define_co_rec_as Least_FP Cs) fpTs bs rhss lthy 119 end; 120 121fun mk_split_rec_thmss ctxt Xs ctrXs_Tsss ctrss rec0_thmss (recs as rec1 :: _) rec_defs = 122 let 123 val f_Ts = binder_fun_types (fastype_of rec1); 124 val (fs, _) = mk_Frees "f" f_Ts ctxt; 125 val frecs = map (fn recx => Term.list_comb (recx, fs)) recs; 126 127 val Xs_frecs = Xs ~~ frecs; 128 val fss = unflat ctrss fs; 129 130 fun mk_rec_call g n (Type (\<^type_name>\<open>fun\<close>, [_, ran_T])) = 131 Abs (Name.uu, Term.dummyT, mk_rec_call g (n + 1) ran_T) 132 | mk_rec_call g n X = 133 let 134 val frec = the (AList.lookup (op =) Xs_frecs X); 135 val xg = Term.list_comb (g, map Bound (n - 1 downto 0)); 136 in frec $ xg end; 137 138 fun mk_rec_arg_arg ctrXs_T g = 139 g :: (if member (op =) Xs (body_type ctrXs_T) then [mk_rec_call g 0 ctrXs_T] else []); 140 141 fun mk_goal frec ctrXs_Ts ctr f = 142 let 143 val ctr_Ts = binder_types (fastype_of ctr); 144 val (gs, _) = mk_Frees "g" ctr_Ts ctxt; 145 val gctr = Term.list_comb (ctr, gs); 146 val fgs = flat_rec_arg_args (map2 mk_rec_arg_arg ctrXs_Ts gs); 147 in 148 fold_rev (fold_rev Logic.all) [fs, gs] 149 (mk_Trueprop_eq (frec $ gctr, Term.list_comb (f, fgs))) 150 |> Syntax.check_term ctxt 151 end; 152 153 val goalss = @{map 4} (@{map 3} o mk_goal) frecs ctrXs_Tsss ctrss fss; 154 155 fun tac ctxt = 156 unfold_thms_tac ctxt (@{thms o_apply fst_conv snd_conv} @ rec_defs @ flat rec0_thmss) THEN 157 HEADGOAL (rtac ctxt refl); 158 159 fun prove goal = 160 Goal.prove_sorry ctxt [] [] goal (tac o #context) 161 |> Thm.close_derivation \<^here>; 162 in 163 map (map prove) goalss 164 end; 165 166fun define_split_rec_derive_induct_rec_thms Xs fpTs ctrXs_Tsss ctrss inducts induct recs0 rec_thmss 167 lthy = 168 let 169 val thy = Proof_Context.theory_of lthy; 170 171 (* imperfect: will not yield the expected theorem for functions taking a large number of 172 arguments *) 173 val repair_induct = unfold_thms lthy @{thms all_mem_range}; 174 175 val inducts' = map repair_induct inducts; 176 val induct' = repair_induct induct; 177 178 val Cs = map ((fn TVar ((s, _), S) => TFree (s, S)) o body_type o fastype_of) recs0; 179 val recs = map2 (mk_co_rec thy Least_FP Cs) fpTs recs0; 180 val ((recs', rec'_defs), lthy') = define_split_recs fpTs Cs recs lthy |>> split_list; 181 val rec'_thmss = mk_split_rec_thmss lthy' Xs ctrXs_Tsss ctrss rec_thmss recs' rec'_defs; 182 in 183 ((inducts', induct', recs', rec'_thmss), lthy') 184 end; 185 186fun body_rec_indices (Old_Datatype_Aux.DtRec kk) = [kk] 187 | body_rec_indices (Old_Datatype_Aux.DtType (\<^type_name>\<open>fun\<close>, [_, D])) = body_rec_indices D 188 | body_rec_indices _ = []; 189 190fun reindex_desc desc = 191 let 192 val kks = map fst desc; 193 val perm_kks = sort int_ord kks; 194 195 fun perm_dtyp (Old_Datatype_Aux.DtType (s, Ds)) = Old_Datatype_Aux.DtType (s, map perm_dtyp Ds) 196 | perm_dtyp (Old_Datatype_Aux.DtRec kk) = 197 Old_Datatype_Aux.DtRec (find_index (curry (op =) kk) kks) 198 | perm_dtyp D = D; 199 in 200 if perm_kks = kks then 201 desc 202 else 203 perm_kks ~~ 204 map (fn (_, (s, Ds, sDss)) => (s, map perm_dtyp Ds, map (apsnd (map perm_dtyp)) sDss)) desc 205 end; 206 207fun mk_infos_of_mutually_recursive_new_datatypes prefs check_names fpT_names0 lthy = 208 let 209 val thy = Proof_Context.theory_of lthy; 210 211 fun not_datatype_name s = 212 error (quote s ^ " is not a datatype"); 213 fun not_mutually_recursive ss = 214 error ("{" ^ commas ss ^ "} is not a complete set of mutually recursive datatypes"); 215 216 fun checked_fp_sugar_of s = 217 (case fp_sugar_of lthy s of 218 SOME (fp_sugar as {fp, fp_co_induct_sugar = SOME _, ...}) => 219 if member (op =) prefs Include_GFPs orelse fp = Least_FP then fp_sugar 220 else not_datatype_name s 221 | _ => not_datatype_name s); 222 223 val fpTs0 as Type (_, var_As) :: _ = 224 map (#T o checked_fp_sugar_of o fst o dest_Type) 225 (#Ts (#fp_res (checked_fp_sugar_of (hd fpT_names0)))); 226 val fpT_names as fpT_name1 :: _ = map (fst o dest_Type) fpTs0; 227 228 val _ = check_names (op =) (fpT_names0, fpT_names) orelse not_mutually_recursive fpT_names0; 229 230 val (As_names, _) = Variable.variant_fixes (map (fn TVar ((s, _), _) => s) var_As) lthy; 231 val As = map2 (fn s => fn TVar (_, S) => TFree (s, S)) As_names var_As; 232 val fpTs = map (fn s => Type (s, As)) fpT_names; 233 234 val nn_fp = length fpTs; 235 236 val mk_dtyp = Old_Datatype_Aux.dtyp_of_typ (map (apsnd (map Term.dest_TFree) o dest_Type) fpTs); 237 238 fun mk_ctr_descr Ts = mk_ctr Ts #> dest_Const ##> (binder_types #> map mk_dtyp); 239 fun mk_typ_descr index (Type (T_name, Ts)) ({ctrs, ...} : ctr_sugar) = 240 (index, (T_name, map mk_dtyp Ts, map (mk_ctr_descr Ts) ctrs)); 241 242 val fp_sugars as {fp, ...} :: _ = map checked_fp_sugar_of fpT_names; 243 val fp_ctr_sugars = map (#ctr_sugar o #fp_ctr_sugar) fp_sugars; 244 val orig_descr = @{map 3} mk_typ_descr (0 upto nn_fp - 1) fpTs fp_ctr_sugars; 245 val all_infos = Old_Datatype_Data.get_all thy; 246 val (orig_descr' :: nested_descrs) = 247 if member (op =) prefs Keep_Nesting then [orig_descr] 248 else fst (Old_Datatype_Aux.unfold_datatypes lthy orig_descr all_infos orig_descr nn_fp); 249 250 fun cliquify_descr [] = [] 251 | cliquify_descr [entry] = [[entry]] 252 | cliquify_descr (full_descr as (_, (T_name1, _, _)) :: _) = 253 let 254 val nn = 255 if member (op =) fpT_names T_name1 then 256 nn_fp 257 else 258 (case Symtab.lookup all_infos T_name1 of 259 SOME {descr, ...} => 260 length (filter_out (exists Old_Datatype_Aux.is_rec_type o #2 o snd) descr) 261 | NONE => raise Fail "unknown old-style datatype"); 262 in 263 chop nn full_descr ||> cliquify_descr |> op :: 264 end; 265 266 (* put nested types before the types that nest them, as needed for N2M *) 267 val descrs = burrow reindex_desc (orig_descr' :: rev nested_descrs); 268 val (mutual_cliques, descr) = 269 split_list (flat (map_index (fn (i, descr) => map (pair i) descr) 270 (maps cliquify_descr descrs))); 271 272 val fpTs' = Old_Datatype_Aux.get_rec_types descr; 273 val nn = length fpTs'; 274 275 val fp_sugars = map (checked_fp_sugar_of o fst o dest_Type) fpTs'; 276 val ctr_Tsss = map (map (map (Old_Datatype_Aux.typ_of_dtyp descr) o snd) o #3 o snd) descr; 277 val kkssss = map (map (map body_rec_indices o snd) o #3 o snd) descr; 278 279 val callers = map (fn kk => Var ((Name.uu, kk), \<^typ>\<open>unit => unit\<close>)) (0 upto nn - 1); 280 281 fun apply_comps n kk = 282 mk_partial_compN n (replicate n HOLogic.unitT ---> HOLogic.unitT) (nth callers kk); 283 284 val callssss = map2 (map2 (map2 (map o apply_comps o num_binder_types))) ctr_Tsss kkssss; 285 286 val b_names = Name.variant_list [] (map base_name_of_typ fpTs'); 287 val compat_b_names = map (prefix compat_N) b_names; 288 val compat_bs = map Binding.name compat_b_names; 289 290 val ((fp_sugars', (lfp_sugar_thms', _)), lthy') = 291 if nn > nn_fp then 292 mutualize_fp_sugars (K true) Least_FP mutual_cliques compat_bs fpTs' callers callssss 293 fp_sugars lthy 294 else 295 ((fp_sugars, (NONE, NONE)), lthy); 296 297 fun mk_ctr_of ({fp_ctr_sugar = {ctr_sugar = {ctrs, ...}, ...}, ...} : fp_sugar) (Type (_, Ts)) = 298 map (mk_ctr Ts) ctrs; 299 val substAT = Term.typ_subst_atomic (var_As ~~ As); 300 301 val Xs' = map #X fp_sugars'; 302 val ctrXs_Tsss' = map (map (map substAT) o #ctrXs_Tss o #fp_ctr_sugar) fp_sugars'; 303 val ctrss' = map2 mk_ctr_of fp_sugars' fpTs'; 304 val {fp_co_induct_sugar = SOME {common_co_inducts = induct :: _, ...}, ...} :: _ = fp_sugars'; 305 val inducts = map (hd o #co_inducts o the o #fp_co_induct_sugar) fp_sugars'; 306 val recs = map (#co_rec o the o #fp_co_induct_sugar) fp_sugars'; 307 val rec_thmss = map (#co_rec_thms o the o #fp_co_induct_sugar) fp_sugars'; 308 309 fun is_nested_rec_type (Type (\<^type_name>\<open>fun\<close>, [_, T])) = member (op =) Xs' (body_type T) 310 | is_nested_rec_type _ = false; 311 312 val ((lfp_sugar_thms'', (inducts', induct', recs', rec'_thmss)), lthy'') = 313 if member (op =) prefs Keep_Nesting orelse 314 not (exists (exists (exists is_nested_rec_type)) ctrXs_Tsss') then 315 ((lfp_sugar_thms', (inducts, induct, recs, rec_thmss)), lthy') 316 else if fp = Least_FP then 317 define_split_rec_derive_induct_rec_thms Xs' fpTs' ctrXs_Tsss' ctrss' inducts induct recs 318 rec_thmss lthy' 319 |>> `(fn (inducts', induct', _, rec'_thmss) => 320 SOME ((inducts', induct', mk_induct_attrs ctrss'), (rec'_thmss, []))) 321 else 322 not_datatype_name fpT_name1; 323 324 val rec'_names = map (fst o dest_Const) recs'; 325 val rec'_thms = flat rec'_thmss; 326 327 fun mk_info (kk, {T = Type (T_name0, _), fp_ctr_sugar = {ctr_sugar = {casex, exhaust, nchotomy, 328 injects, distincts, case_thms, case_cong, case_cong_weak, split, 329 split_asm, ...}, ...}, ...} : fp_sugar) = 330 (T_name0, 331 {index = kk, descr = descr, inject = injects, distinct = distincts, induct = induct', 332 inducts = inducts', exhaust = exhaust, nchotomy = nchotomy, rec_names = rec'_names, 333 rec_rewrites = rec'_thms, case_name = fst (dest_Const casex), case_rewrites = case_thms, 334 case_cong = case_cong, case_cong_weak = case_cong_weak, split = split, 335 split_asm = split_asm}); 336 337 val infos = map_index mk_info (take nn_fp fp_sugars'); 338 in 339 (nn, b_names, compat_b_names, lfp_sugar_thms'', infos, lthy'') 340 end; 341 342fun infos_of_new_datatype_mutual_cluster lthy prefs fpT_name = 343 let 344 fun get prefs = 345 #5 (mk_infos_of_mutually_recursive_new_datatypes prefs subset [fpT_name] lthy) 346 handle ERROR _ => []; 347 in 348 (case get prefs of 349 [] => if member (op =) prefs Keep_Nesting then [] else get (Keep_Nesting :: prefs) 350 | infos => infos) 351 end; 352 353fun get_all thy prefs = 354 let 355 val ctxt = Proof_Context.init_global thy; 356 val old_info_tab = Old_Datatype_Data.get_all thy; 357 val new_T_names = BNF_FP_Def_Sugar.fp_sugars_of_global thy 358 |> map_filter (try (fn {T = Type (s, _), fp_res_index = 0, ...} => s)); 359 val new_infos = 360 maps (infos_of_new_datatype_mutual_cluster ctxt (insert (op =) Keep_Nesting prefs)) 361 new_T_names; 362 in 363 fold (if member (op =) prefs Keep_Nesting then Symtab.update else Symtab.default) new_infos 364 old_info_tab 365 end; 366 367fun get_one get_old get_new thy prefs x = 368 let 369 val (get_fst, get_snd) = (get_old thy, get_new thy) |> member (op =) prefs Keep_Nesting ? swap; 370 in 371 (case get_fst x of NONE => get_snd x | res => res) 372 end; 373 374fun get_info_of_new_datatype prefs thy T_name = 375 let val ctxt = Proof_Context.init_global thy in 376 AList.lookup (op =) (infos_of_new_datatype_mutual_cluster ctxt prefs T_name) T_name 377 end; 378 379fun get_info thy prefs = 380 get_one Old_Datatype_Data.get_info (get_info_of_new_datatype prefs) thy prefs; 381 382fun the_info thy prefs T_name = 383 (case get_info thy prefs T_name of 384 SOME info => info 385 | NONE => error ("Unknown datatype " ^ quote T_name)); 386 387fun the_spec thy T_name = 388 let 389 val {descr, index, ...} = the_info thy [Keep_Nesting, Include_GFPs] T_name; 390 val (_, Ds, ctrs0) = the (AList.lookup (op =) descr index); 391 val tfrees = map Old_Datatype_Aux.dest_DtTFree Ds; 392 val ctrs = map (apsnd (map (Old_Datatype_Aux.typ_of_dtyp descr))) ctrs0; 393 in (tfrees, ctrs) end; 394 395fun the_descr thy prefs (T_names0 as T_name01 :: _) = 396 let 397 fun not_mutually_recursive ss = 398 error ("{" ^ commas ss ^ "} is not a complete set of mutually recursive datatypes"); 399 400 val info = the_info thy prefs T_name01; 401 val descr = #descr info; 402 403 val (_, Ds, _) = the (AList.lookup (op =) descr (#index info)); 404 val vs = map Old_Datatype_Aux.dest_DtTFree Ds; 405 406 fun is_DtTFree (Old_Datatype_Aux.DtTFree _) = true 407 | is_DtTFree _ = false; 408 409 val k = find_index (fn (_, (_, dTs, _)) => not (forall is_DtTFree dTs)) descr; 410 val protoTs as (dataTs, _) = chop k descr 411 |> (apply2 o map) 412 (fn (_, (T_name, Ds, _)) => (T_name, map (Old_Datatype_Aux.typ_of_dtyp descr) Ds)); 413 414 val T_names = map fst dataTs; 415 val _ = eq_set (op =) (T_names, T_names0) orelse not_mutually_recursive T_names0 416 417 val (Ts, Us) = apply2 (map Type) protoTs; 418 419 val names = map Long_Name.base_name T_names; 420 val (auxnames, _) = Name.make_context names 421 |> fold_map (Name.variant o Old_Datatype_Aux.name_of_typ) Us; 422 val prefix = space_implode "_" names; 423 in 424 (descr, vs, T_names, prefix, (names, auxnames), (Ts, Us)) 425 end; 426 427fun get_constrs thy T_name = 428 try (the_spec thy) T_name 429 |> Option.map (fn (tfrees, ctrs) => 430 let 431 fun varify_tfree (s, S) = TVar ((s, 0), S); 432 fun varify_typ (TFree x) = varify_tfree x 433 | varify_typ T = T; 434 435 val dataT = Type (T_name, map varify_tfree tfrees); 436 437 fun mk_ctr_typ Ts = map (Term.map_atyps varify_typ) Ts ---> dataT; 438 in 439 map (apsnd mk_ctr_typ) ctrs 440 end); 441 442fun old_interpretation_of prefs f config T_names thy = 443 if not (member (op =) prefs Keep_Nesting) orelse 444 exists (is_none o fp_sugar_of_global thy) T_names then 445 f config T_names thy 446 else 447 thy; 448 449fun new_interpretation_of prefs f (fp_sugars : fp_sugar list) thy = 450 let val T_names = map (fst o dest_Type o #T) fp_sugars in 451 if (member (op =) prefs Include_GFPs orelse forall (curry (op =) Least_FP o #fp) fp_sugars) 452 andalso (member (op =) prefs Keep_Nesting orelse 453 exists (is_none o Old_Datatype_Data.get_info thy) T_names) then 454 f Old_Datatype_Aux.default_config T_names thy 455 else 456 thy 457 end; 458 459fun interpretation name prefs f = 460 Old_Datatype_Data.interpretation (old_interpretation_of prefs f) 461 #> fp_sugars_interpretation name (Local_Theory.background_theory o new_interpretation_of prefs f); 462 463val nitpicksimp_simp_attrs = @{attributes [nitpick_simp, simp]}; 464 465fun datatype_compat fpT_names lthy = 466 let 467 val (nn, b_names, compat_b_names, lfp_sugar_thms, infos, lthy') = 468 mk_infos_of_mutually_recursive_new_datatypes [] eq_set fpT_names lthy; 469 470 val (all_notes, rec_thmss) = 471 (case lfp_sugar_thms of 472 NONE => ([], []) 473 | SOME ((inducts, induct, induct_attrs), (rec_thmss, _)) => 474 let 475 val common_name = compat_N ^ mk_common_name b_names; 476 477 val common_notes = 478 (if nn > 1 then [(inductN, [induct], induct_attrs)] else []) 479 |> filter_out (null o #2) 480 |> map (fn (thmN, thms, attrs) => 481 ((Binding.qualify true common_name (Binding.name thmN), attrs), [(thms, [])])); 482 483 val notes = 484 [(inductN, map single inducts, induct_attrs), 485 (recN, rec_thmss, nitpicksimp_simp_attrs)] 486 |> filter_out (null o #2) 487 |> maps (fn (thmN, thmss, attrs) => 488 if forall null thmss then 489 [] 490 else 491 map2 (fn b_name => fn thms => 492 ((Binding.qualify true b_name (Binding.name thmN), attrs), [(thms, [])])) 493 compat_b_names thmss); 494 in 495 (common_notes @ notes, rec_thmss) 496 end); 497 498 val register_interpret = 499 Old_Datatype_Data.register infos 500 #> Old_Datatype_Data.interpretation_data (Old_Datatype_Aux.default_config, map fst infos); 501 in 502 lthy' 503 |> Local_Theory.raw_theory register_interpret 504 |> Local_Theory.notes all_notes 505 |> snd 506 |> Code.declare_default_eqns (map (rpair true) (flat rec_thmss)) 507 end; 508 509val datatype_compat_global = Named_Target.theory_map o datatype_compat; 510 511fun datatype_compat_cmd raw_fpT_names lthy = 512 let 513 val fpT_names = 514 map (fst o dest_Type o Proof_Context.read_type_name {proper = true, strict = false} lthy) 515 raw_fpT_names; 516 in 517 datatype_compat fpT_names lthy 518 end; 519 520fun add_datatype prefs old_specs thy = 521 let 522 val fpT_names = map (Sign.full_name thy o #1 o fst) old_specs; 523 524 fun new_type_args_of (s, S) = 525 (if member (op =) prefs Kill_Type_Args then NONE else SOME Binding.empty, 526 (TFree (s, \<^sort>\<open>type\<close>), S)); 527 fun new_ctr_spec_of (b, Ts, mx) = (((Binding.empty, b), map (pair Binding.empty) Ts), mx); 528 529 fun new_spec_of ((b, old_tyargs, mx), old_ctr_specs) = 530 (((((map new_type_args_of old_tyargs, b), mx), map new_ctr_spec_of old_ctr_specs), 531 (Binding.empty, Binding.empty, Binding.empty)), []); 532 533 val new_specs = map new_spec_of old_specs; 534 in 535 (fpT_names, 536 thy 537 |> Named_Target.theory_map 538 (co_datatypes Least_FP construct_lfp (default_ctr_options, new_specs)) 539 |> not (member (op =) prefs Keep_Nesting) ? perhaps (try (datatype_compat_global fpT_names))) 540 end; 541 542fun old_of_new f (ts, _, simpss) = (ts, f simpss); 543 544val primrec = apfst (old_of_new flat) ooo BNF_LFP_Rec_Sugar.primrec false []; 545val primrec_global = apfst (old_of_new flat) ooo BNF_LFP_Rec_Sugar.primrec_global false []; 546val primrec_overloaded = apfst (old_of_new flat) oooo BNF_LFP_Rec_Sugar.primrec_overloaded false []; 547val primrec_simple = apfst (apfst fst o apsnd (old_of_new (flat o snd))) ooo 548 BNF_LFP_Rec_Sugar.primrec_simple false; 549 550val _ = 551 Outer_Syntax.local_theory \<^command_keyword>\<open>datatype_compat\<close> 552 "register datatypes as old-style datatypes and derive old-style properties" 553 (Scan.repeat1 Parse.type_const >> datatype_compat_cmd); 554 555end; 556