1(* Title: HOL/Tools/Old_Datatype/old_datatype_data.ML 2 Author: Stefan Berghofer, TU Muenchen 3 4Datatype package bookkeeping. 5*) 6 7signature OLD_DATATYPE_DATA = 8sig 9 include OLD_DATATYPE_COMMON 10 11 val get_all : theory -> info Symtab.table 12 val get_info : theory -> string -> info option 13 val the_info : theory -> string -> info 14 val info_of_constr : theory -> string * typ -> info option 15 val info_of_constr_permissive : theory -> string * typ -> info option 16 val info_of_case : theory -> string -> info option 17 val register: (string * info) list -> theory -> theory 18 val the_spec : theory -> string -> (string * sort) list * (string * typ list) list 19 val the_descr : theory -> string list -> 20 descr * (string * sort) list * string list * string * 21 (string list * string list) * (typ list * typ list) 22 val all_distincts : theory -> typ list -> thm list list 23 val get_constrs : theory -> string -> (string * typ) list option 24 val mk_case_names_induct: descr -> attribute 25 val mk_case_names_exhausts: descr -> string list -> attribute list 26 val interpretation : (config -> string list -> theory -> theory) -> theory -> theory 27 val interpretation_data : config * string list -> theory -> theory 28end; 29 30structure Old_Datatype_Data: OLD_DATATYPE_DATA = 31struct 32 33(** theory data **) 34 35(* data management *) 36 37structure Data = Theory_Data 38( 39 type T = 40 {types: Old_Datatype_Aux.info Symtab.table, 41 constrs: (string * Old_Datatype_Aux.info) list Symtab.table, 42 cases: Old_Datatype_Aux.info Symtab.table}; 43 44 val empty = 45 {types = Symtab.empty, constrs = Symtab.empty, cases = Symtab.empty}; 46 val extend = I; 47 fun merge 48 ({types = types1, constrs = constrs1, cases = cases1}, 49 {types = types2, constrs = constrs2, cases = cases2}) : T = 50 {types = Symtab.merge (K true) (types1, types2), 51 constrs = Symtab.join (K (AList.merge (op =) (K true))) (constrs1, constrs2), 52 cases = Symtab.merge (K true) (cases1, cases2)}; 53); 54 55val get_all = #types o Data.get; 56val get_info = Symtab.lookup o get_all; 57 58fun the_info thy name = 59 (case get_info thy name of 60 SOME info => info 61 | NONE => error ("Unknown old-style datatype " ^ quote name)); 62 63fun info_of_constr thy (c, T) = 64 let 65 val tab = Symtab.lookup_list (#constrs (Data.get thy)) c; 66 in 67 (case body_type T of 68 Type (tyco, _) => AList.lookup (op =) tab tyco 69 | _ => NONE) 70 end; 71 72fun info_of_constr_permissive thy (c, T) = 73 let 74 val tab = Symtab.lookup_list (#constrs (Data.get thy)) c; 75 val hint = (case body_type T of Type (tyco, _) => SOME tyco | _ => NONE); 76 val default = if null tab then NONE else SOME (snd (List.last tab)); 77 (*conservative wrt. overloaded constructors*) 78 in 79 (case hint of 80 NONE => default 81 | SOME tyco => 82 (case AList.lookup (op =) tab tyco of 83 NONE => default (*permissive*) 84 | SOME info => SOME info)) 85 end; 86 87val info_of_case = Symtab.lookup o #cases o Data.get; 88 89fun ctrs_of_exhaust exhaust = 90 Logic.strip_imp_prems (Thm.prop_of exhaust) |> 91 map (head_of o snd o HOLogic.dest_eq o HOLogic.dest_Trueprop o the_single 92 o Logic.strip_assums_hyp); 93 94fun case_of_case_rewrite case_rewrite = 95 head_of (fst (HOLogic.dest_eq (HOLogic.dest_Trueprop (Thm.prop_of case_rewrite)))); 96 97fun ctr_sugar_of_info ({exhaust, nchotomy, inject, distinct, case_rewrites, case_cong, 98 case_cong_weak, split, split_asm, ...} : Old_Datatype_Aux.info) = 99 let val ctrs as ctr1 :: _ = ctrs_of_exhaust exhaust in 100 {kind = Ctr_Sugar.Datatype, 101 T = body_type (fastype_of ctr1), 102 ctrs = ctrs, 103 casex = case_of_case_rewrite (hd case_rewrites), 104 discs = [], 105 selss = [], 106 exhaust = exhaust, 107 nchotomy = nchotomy, 108 injects = inject, 109 distincts = distinct, 110 case_thms = case_rewrites, 111 case_cong = case_cong, 112 case_cong_weak = case_cong_weak, 113 case_distribs = [], 114 split = split, 115 split_asm = split_asm, 116 disc_defs = [], 117 disc_thmss = [], 118 discIs = [], 119 disc_eq_cases = [], 120 sel_defs = [], 121 sel_thmss = [], 122 distinct_discsss = [], 123 exhaust_discs = [], 124 exhaust_sels = [], 125 collapses = [], 126 expands = [], 127 split_sels = [], 128 split_sel_asms = [], 129 case_eq_ifs = []} 130 end; 131 132fun register dt_infos = 133 Data.map (fn {types, constrs, cases} => 134 {types = types |> fold Symtab.update dt_infos, 135 constrs = constrs |> fold (fn (constr, dtname_info) => 136 Symtab.map_default (constr, []) (cons dtname_info)) 137 (maps (fn (dtname, info as {descr, index, ...}) => 138 map (rpair (dtname, info) o fst) (#3 (the (AList.lookup op = descr index)))) dt_infos), 139 cases = cases |> fold Symtab.update 140 (map (fn (_, info as {case_name, ...}) => (case_name, info)) dt_infos)}) #> 141 fold (Ctr_Sugar.default_register_ctr_sugar_global (K true) o ctr_sugar_of_info o snd) dt_infos; 142 143 144(* complex queries *) 145 146fun the_spec thy dtco = 147 let 148 val {descr, index, ...} = the_info thy dtco; 149 val (_, dtys, raw_cos) = the (AList.lookup (op =) descr index); 150 val args = map Old_Datatype_Aux.dest_DtTFree dtys; 151 val cos = map (fn (co, tys) => (co, map (Old_Datatype_Aux.typ_of_dtyp descr) tys)) raw_cos; 152 in (args, cos) end; 153 154fun the_descr thy (raw_tycos as raw_tyco :: _) = 155 let 156 val info = the_info thy raw_tyco; 157 val descr = #descr info; 158 159 val (_, dtys, _) = the (AList.lookup (op =) descr (#index info)); 160 val vs = map Old_Datatype_Aux.dest_DtTFree dtys; 161 162 fun is_DtTFree (Old_Datatype_Aux.DtTFree _) = true 163 | is_DtTFree _ = false; 164 val k = find_index (fn (_, (_, dTs, _)) => not (forall is_DtTFree dTs)) descr; 165 val protoTs as (dataTs, _) = 166 chop k descr 167 |> (apply2 o map) 168 (fn (_, (tyco, dTs, _)) => (tyco, map (Old_Datatype_Aux.typ_of_dtyp descr) dTs)); 169 170 val tycos = map fst dataTs; 171 val _ = 172 if eq_set (op =) (tycos, raw_tycos) then () 173 else 174 error ("Type constructors " ^ commas_quote raw_tycos ^ 175 " do not belong exhaustively to one mutually recursive old-style datatype"); 176 177 val (Ts, Us) = apply2 (map Type) protoTs; 178 179 val names = map Long_Name.base_name tycos; 180 val (auxnames, _) = 181 Name.make_context names 182 |> fold_map (Name.variant o Old_Datatype_Aux.name_of_typ) Us; 183 val prefix = space_implode "_" names; 184 185 in (descr, vs, tycos, prefix, (names, auxnames), (Ts, Us)) end; 186 187fun all_distincts thy Ts = 188 let 189 fun add_tycos (Type (tyco, Ts)) = insert (op =) tyco #> fold add_tycos Ts 190 | add_tycos _ = I; 191 val tycos = fold add_tycos Ts []; 192 in map_filter (Option.map #distinct o get_info thy) tycos end; 193 194fun get_constrs thy dtco = 195 (case try (the_spec thy) dtco of 196 SOME (args, cos) => 197 let 198 fun subst (v, sort) = TVar ((v, 0), sort); 199 fun subst_ty (TFree v) = subst v 200 | subst_ty ty = ty; 201 val dty = Type (dtco, map subst args); 202 fun mk_co (co, tys) = (co, map (Term.map_atyps subst_ty) tys ---> dty); 203 in SOME (map mk_co cos) end 204 | NONE => NONE); 205 206 207 208(** various auxiliary **) 209 210(* case names *) 211 212local 213 214fun dt_recs (Old_Datatype_Aux.DtTFree _) = [] 215 | dt_recs (Old_Datatype_Aux.DtType (_, dts)) = maps dt_recs dts 216 | dt_recs (Old_Datatype_Aux.DtRec i) = [i]; 217 218fun dt_cases (descr: Old_Datatype_Aux.descr) (_, args, constrs) = 219 let 220 fun the_bname i = Long_Name.base_name (#1 (the (AList.lookup (op =) descr i))); 221 val bnames = map the_bname (distinct (op =) (maps dt_recs args)); 222 in map (fn (c, _) => space_implode "_" (Long_Name.base_name c :: bnames)) constrs end; 223 224fun induct_cases descr = 225 Old_Datatype_Prop.indexify_names (maps (dt_cases descr) (map #2 descr)); 226 227fun exhaust_cases descr i = dt_cases descr (the (AList.lookup (op =) descr i)); 228 229in 230 231fun mk_case_names_induct descr = Rule_Cases.case_names (induct_cases descr); 232 233fun mk_case_names_exhausts descr new = 234 map (Rule_Cases.case_names o exhaust_cases descr o #1) 235 (filter (fn ((_, (name, _, _))) => member (op =) new name) descr); 236 237end; 238 239 240 241(** abstract theory extensions relative to a datatype characterisation **) 242 243structure Old_Datatype_Plugin = Plugin(type T = Old_Datatype_Aux.config * string list); 244 245val old_datatype_plugin = Plugin_Name.declare_setup \<^binding>\<open>old_datatype\<close>; 246 247fun interpretation f = 248 Old_Datatype_Plugin.interpretation old_datatype_plugin 249 (fn (config, type_names as name :: _) => 250 Local_Theory.background_theory (fn thy => 251 thy 252 |> Sign.root_path 253 |> Sign.add_path (Long_Name.qualifier name) 254 |> f config type_names 255 |> Sign.restore_naming thy)); 256 257val interpretation_data = Named_Target.theory_map o Old_Datatype_Plugin.data_default; 258 259 260open Old_Datatype_Aux; 261 262end; 263