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