author | wenzelm |
Thu, 15 Dec 2011 18:08:40 +0100 | |
changeset 45891 | d73605c829cc |
parent 45890 | 5f70aaecae26 |
child 54400 | 418a183fbe21 |
permissions | -rw-r--r-- |
33970 | 1 |
(* Title: HOL/Tools/Datatype/datatype_data.ML |
11539 | 2 |
Author: Stefan Berghofer, TU Muenchen |
5177 | 3 |
|
45890 | 4 |
Datatype package bookkeeping. |
5177 | 5 |
*) |
6 |
||
33970 | 7 |
signature DATATYPE_DATA = |
6360 | 8 |
sig |
33970 | 9 |
include DATATYPE_COMMON |
45890 | 10 |
val get_all : theory -> info Symtab.table |
33970 | 11 |
val get_info : theory -> string -> info option |
12 |
val the_info : theory -> string -> info |
|
45890 | 13 |
val info_of_constr : theory -> string * typ -> info option |
14 |
val info_of_constr_permissive : theory -> string * typ -> info option |
|
15 |
val info_of_case : theory -> string -> info option |
|
16 |
val register: (string * info) list -> theory -> theory |
|
17 |
val the_spec : theory -> string -> (string * sort) list * (string * typ list) list |
|
45701 | 18 |
val the_descr : theory -> string list -> |
19 |
descr * (string * sort) list * string list * string * |
|
20 |
(string list * string list) * (typ list * typ list) |
|
33970 | 21 |
val all_distincts : theory -> typ list -> thm list list |
22 |
val get_constrs : theory -> string -> (string * typ) list option |
|
45890 | 23 |
val mk_case_names_induct: descr -> attribute |
24 |
val mk_case_names_exhausts: descr -> string list -> attribute list |
|
33970 | 25 |
val interpretation : (config -> string list -> theory -> theory) -> theory -> theory |
45890 | 26 |
val interpretation_data : config * string list -> theory -> theory |
33970 | 27 |
val setup: theory -> theory |
32717
0e787c721fa3
re-established reasonable inner outline for module
haftmann
parents:
32712
diff
changeset
|
28 |
end; |
0e787c721fa3
re-established reasonable inner outline for module
haftmann
parents:
32712
diff
changeset
|
29 |
|
33970 | 30 |
structure Datatype_Data: DATATYPE_DATA = |
33963
977b94b64905
renamed former datatype.ML to datatype_data.ML; datatype.ML provides uniform view on datatype.ML and datatype_rep_proofs.ML
haftmann
parents:
33959
diff
changeset
|
31 |
struct |
5177 | 32 |
|
33970 | 33 |
(** theory data **) |
34 |
||
35 |
(* data management *) |
|
36 |
||
45890 | 37 |
structure Data = Theory_Data |
33970 | 38 |
( |
39 |
type T = |
|
41423 | 40 |
{types: Datatype_Aux.info Symtab.table, |
41 |
constrs: (string * Datatype_Aux.info) list Symtab.table, |
|
42 |
cases: Datatype_Aux.info Symtab.table}; |
|
33968
f94fb13ecbb3
modernized structures and tuned headers of datatype package modules; joined former datatype.ML and datatype_rep_proofs.ML
haftmann
parents:
33963
diff
changeset
|
43 |
|
33970 | 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 |
||
45890 | 55 |
val get_all = #types o Data.get; |
33970 | 56 |
val get_info = Symtab.lookup o get_all; |
33968
f94fb13ecbb3
modernized structures and tuned headers of datatype package modules; joined former datatype.ML and datatype_rep_proofs.ML
haftmann
parents:
33963
diff
changeset
|
57 |
|
33970 | 58 |
fun the_info thy name = |
59 |
(case get_info thy name of |
|
60 |
SOME info => info |
|
61 |
| NONE => error ("Unknown datatype " ^ quote name)); |
|
33968
f94fb13ecbb3
modernized structures and tuned headers of datatype package modules; joined former datatype.ML and datatype_rep_proofs.ML
haftmann
parents:
33963
diff
changeset
|
62 |
|
33970 | 63 |
fun info_of_constr thy (c, T) = |
64 |
let |
|
45890 | 65 |
val tab = Symtab.lookup_list (#constrs (Data.get thy)) c; |
43580
023a1d1f97bd
new Datatype.info_of_constr with strict behaviour wrt. to overloaded constructors -- side effect: function package correctly identifies 0::int as a non-constructor;
krauss
parents:
43329
diff
changeset
|
66 |
in |
45700 | 67 |
(case body_type T of |
43580
023a1d1f97bd
new Datatype.info_of_constr with strict behaviour wrt. to overloaded constructors -- side effect: function package correctly identifies 0::int as a non-constructor;
krauss
parents:
43329
diff
changeset
|
68 |
Type (tyco, _) => AList.lookup (op =) tab tyco |
45700 | 69 |
| _ => NONE) |
43580
023a1d1f97bd
new Datatype.info_of_constr with strict behaviour wrt. to overloaded constructors -- side effect: function package correctly identifies 0::int as a non-constructor;
krauss
parents:
43329
diff
changeset
|
70 |
end; |
023a1d1f97bd
new Datatype.info_of_constr with strict behaviour wrt. to overloaded constructors -- side effect: function package correctly identifies 0::int as a non-constructor;
krauss
parents:
43329
diff
changeset
|
71 |
|
023a1d1f97bd
new Datatype.info_of_constr with strict behaviour wrt. to overloaded constructors -- side effect: function package correctly identifies 0::int as a non-constructor;
krauss
parents:
43329
diff
changeset
|
72 |
fun info_of_constr_permissive thy (c, T) = |
023a1d1f97bd
new Datatype.info_of_constr with strict behaviour wrt. to overloaded constructors -- side effect: function package correctly identifies 0::int as a non-constructor;
krauss
parents:
43329
diff
changeset
|
73 |
let |
45890 | 74 |
val tab = Symtab.lookup_list (#constrs (Data.get thy)) c; |
45700 | 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)) |
|
33970 | 85 |
end; |
86 |
||
45890 | 87 |
val info_of_case = Symtab.lookup o #cases o Data.get; |
33970 | 88 |
|
41423 | 89 |
fun register (dt_infos : (string * Datatype_Aux.info) list) = |
45890 | 90 |
Data.map (fn {types, constrs, cases} => |
33970 | 91 |
{types = types |> fold Symtab.update dt_infos, |
92 |
constrs = constrs |> fold (fn (constr, dtname_info) => |
|
93 |
Symtab.map_default (constr, []) (cons dtname_info)) |
|
94 |
(maps (fn (dtname, info as {descr, index, ...}) => |
|
95 |
map (rpair (dtname, info) o fst) |
|
96 |
(#3 (the (AList.lookup op = descr index)))) dt_infos), |
|
97 |
cases = cases |> fold Symtab.update |
|
98 |
(map (fn (_, info as {case_name, ...}) => (case_name, info)) dt_infos)}); |
|
99 |
||
33968
f94fb13ecbb3
modernized structures and tuned headers of datatype package modules; joined former datatype.ML and datatype_rep_proofs.ML
haftmann
parents:
33963
diff
changeset
|
100 |
|
33970 | 101 |
(* complex queries *) |
102 |
||
103 |
fun the_spec thy dtco = |
|
104 |
let |
|
45822 | 105 |
val {descr, index, ...} = the_info thy dtco; |
45821 | 106 |
val (_, dtys, raw_cos) = the (AList.lookup (op =) descr index); |
45822 | 107 |
val args = map Datatype_Aux.dest_DtTFree dtys; |
108 |
val cos = map (fn (co, tys) => (co, map (Datatype_Aux.typ_of_dtyp descr) tys)) raw_cos; |
|
109 |
in (args, cos) end; |
|
33970 | 110 |
|
111 |
fun the_descr thy (raw_tycos as raw_tyco :: _) = |
|
112 |
let |
|
113 |
val info = the_info thy raw_tyco; |
|
114 |
val descr = #descr info; |
|
115 |
||
45822 | 116 |
val (_, dtys, _) = the (AList.lookup (op =) descr (#index info)); |
117 |
val vs = map Datatype_Aux.dest_DtTFree dtys; |
|
33968
f94fb13ecbb3
modernized structures and tuned headers of datatype package modules; joined former datatype.ML and datatype_rep_proofs.ML
haftmann
parents:
33963
diff
changeset
|
118 |
|
41423 | 119 |
fun is_DtTFree (Datatype_Aux.DtTFree _) = true |
45700 | 120 |
| is_DtTFree _ = false; |
33970 | 121 |
val k = find_index (fn (_, (_, dTs, _)) => not (forall is_DtTFree dTs)) descr; |
41423 | 122 |
val protoTs as (dataTs, _) = |
123 |
chop k descr |
|
124 |
|> (pairself o map) |
|
45822 | 125 |
(fn (_, (tyco, dTs, _)) => (tyco, map (Datatype_Aux.typ_of_dtyp descr) dTs)); |
45700 | 126 |
|
33970 | 127 |
val tycos = map fst dataTs; |
45430 | 128 |
val _ = |
129 |
if eq_set (op =) (tycos, raw_tycos) then () |
|
45700 | 130 |
else |
131 |
error ("Type constructors " ^ commas_quote raw_tycos ^ |
|
132 |
" do not belong exhaustively to one mutual recursive datatype"); |
|
33970 | 133 |
|
134 |
val (Ts, Us) = (pairself o map) Type protoTs; |
|
135 |
||
45701 | 136 |
val names = map Long_Name.base_name tycos; |
45700 | 137 |
val (auxnames, _) = |
138 |
Name.make_context names |
|
43326
47cf4bc789aa
simplified Name.variant -- discontinued builtin fold_map;
wenzelm
parents:
43253
diff
changeset
|
139 |
|> fold_map (Name.variant o Datatype_Aux.name_of_typ) Us; |
33970 | 140 |
val prefix = space_implode "_" names; |
141 |
||
142 |
in (descr, vs, tycos, prefix, (names, auxnames), (Ts, Us)) end; |
|
143 |
||
144 |
fun all_distincts thy Ts = |
|
145 |
let |
|
146 |
fun add_tycos (Type (tyco, Ts)) = insert (op =) tyco #> fold add_tycos Ts |
|
147 |
| add_tycos _ = I; |
|
148 |
val tycos = fold add_tycos Ts []; |
|
149 |
in map_filter (Option.map #distinct o get_info thy) tycos end; |
|
150 |
||
151 |
fun get_constrs thy dtco = |
|
45700 | 152 |
(case try (the_spec thy) dtco of |
45822 | 153 |
SOME (args, cos) => |
45700 | 154 |
let |
155 |
fun subst (v, sort) = TVar ((v, 0), sort); |
|
156 |
fun subst_ty (TFree v) = subst v |
|
157 |
| subst_ty ty = ty; |
|
45822 | 158 |
val dty = Type (dtco, map subst args); |
45700 | 159 |
fun mk_co (co, tys) = (co, map (Term.map_atyps subst_ty) tys ---> dty); |
160 |
in SOME (map mk_co cos) end |
|
161 |
| NONE => NONE); |
|
33968
f94fb13ecbb3
modernized structures and tuned headers of datatype package modules; joined former datatype.ML and datatype_rep_proofs.ML
haftmann
parents:
33963
diff
changeset
|
162 |
|
f94fb13ecbb3
modernized structures and tuned headers of datatype package modules; joined former datatype.ML and datatype_rep_proofs.ML
haftmann
parents:
33963
diff
changeset
|
163 |
|
f94fb13ecbb3
modernized structures and tuned headers of datatype package modules; joined former datatype.ML and datatype_rep_proofs.ML
haftmann
parents:
33963
diff
changeset
|
164 |
|
33970 | 165 |
(** various auxiliary **) |
33968
f94fb13ecbb3
modernized structures and tuned headers of datatype package modules; joined former datatype.ML and datatype_rep_proofs.ML
haftmann
parents:
33963
diff
changeset
|
166 |
|
33970 | 167 |
(* case names *) |
168 |
||
169 |
local |
|
33968
f94fb13ecbb3
modernized structures and tuned headers of datatype package modules; joined former datatype.ML and datatype_rep_proofs.ML
haftmann
parents:
33963
diff
changeset
|
170 |
|
41423 | 171 |
fun dt_recs (Datatype_Aux.DtTFree _) = [] |
172 |
| dt_recs (Datatype_Aux.DtType (_, dts)) = maps dt_recs dts |
|
173 |
| dt_recs (Datatype_Aux.DtRec i) = [i]; |
|
33968
f94fb13ecbb3
modernized structures and tuned headers of datatype package modules; joined former datatype.ML and datatype_rep_proofs.ML
haftmann
parents:
33963
diff
changeset
|
174 |
|
41423 | 175 |
fun dt_cases (descr: Datatype_Aux.descr) (_, args, constrs) = |
33970 | 176 |
let |
177 |
fun the_bname i = Long_Name.base_name (#1 (the (AList.lookup (op =) descr i))); |
|
178 |
val bnames = map the_bname (distinct (op =) (maps dt_recs args)); |
|
179 |
in map (fn (c, _) => space_implode "_" (Long_Name.base_name c :: bnames)) constrs end; |
|
33968
f94fb13ecbb3
modernized structures and tuned headers of datatype package modules; joined former datatype.ML and datatype_rep_proofs.ML
haftmann
parents:
33963
diff
changeset
|
180 |
|
33970 | 181 |
fun induct_cases descr = |
182 |
Datatype_Prop.indexify_names (maps (dt_cases descr) (map #2 descr)); |
|
33968
f94fb13ecbb3
modernized structures and tuned headers of datatype package modules; joined former datatype.ML and datatype_rep_proofs.ML
haftmann
parents:
33963
diff
changeset
|
183 |
|
33970 | 184 |
fun exhaust_cases descr i = dt_cases descr (the (AList.lookup (op =) descr i)); |
185 |
||
186 |
in |
|
187 |
||
188 |
fun mk_case_names_induct descr = Rule_Cases.case_names (induct_cases descr); |
|
33968
f94fb13ecbb3
modernized structures and tuned headers of datatype package modules; joined former datatype.ML and datatype_rep_proofs.ML
haftmann
parents:
33963
diff
changeset
|
189 |
|
33970 | 190 |
fun mk_case_names_exhausts descr new = |
191 |
map (Rule_Cases.case_names o exhaust_cases descr o #1) |
|
192 |
(filter (fn ((_, (name, _, _))) => member (op =) new name) descr); |
|
33968
f94fb13ecbb3
modernized structures and tuned headers of datatype package modules; joined former datatype.ML and datatype_rep_proofs.ML
haftmann
parents:
33963
diff
changeset
|
193 |
|
33970 | 194 |
end; |
33968
f94fb13ecbb3
modernized structures and tuned headers of datatype package modules; joined former datatype.ML and datatype_rep_proofs.ML
haftmann
parents:
33963
diff
changeset
|
195 |
|
f94fb13ecbb3
modernized structures and tuned headers of datatype package modules; joined former datatype.ML and datatype_rep_proofs.ML
haftmann
parents:
33963
diff
changeset
|
196 |
|
f94fb13ecbb3
modernized structures and tuned headers of datatype package modules; joined former datatype.ML and datatype_rep_proofs.ML
haftmann
parents:
33963
diff
changeset
|
197 |
|
33970 | 198 |
(** document antiquotation **) |
33968
f94fb13ecbb3
modernized structures and tuned headers of datatype package modules; joined former datatype.ML and datatype_rep_proofs.ML
haftmann
parents:
33963
diff
changeset
|
199 |
|
43564
9864182c6bad
document antiquotations are managed as theory data, with proper name space and entity markup;
wenzelm
parents:
43329
diff
changeset
|
200 |
val antiq_setup = |
9864182c6bad
document antiquotations are managed as theory data, with proper name space and entity markup;
wenzelm
parents:
43329
diff
changeset
|
201 |
Thy_Output.antiquotation @{binding datatype} (Args.type_name true) |
9864182c6bad
document antiquotations are managed as theory data, with proper name space and entity markup;
wenzelm
parents:
43329
diff
changeset
|
202 |
(fn {source = src, context = ctxt, ...} => fn dtco => |
9864182c6bad
document antiquotations are managed as theory data, with proper name space and entity markup;
wenzelm
parents:
43329
diff
changeset
|
203 |
let |
9864182c6bad
document antiquotations are managed as theory data, with proper name space and entity markup;
wenzelm
parents:
43329
diff
changeset
|
204 |
val thy = Proof_Context.theory_of ctxt; |
9864182c6bad
document antiquotations are managed as theory data, with proper name space and entity markup;
wenzelm
parents:
43329
diff
changeset
|
205 |
val (vs, cos) = the_spec thy dtco; |
9864182c6bad
document antiquotations are managed as theory data, with proper name space and entity markup;
wenzelm
parents:
43329
diff
changeset
|
206 |
val ty = Type (dtco, map TFree vs); |
9864182c6bad
document antiquotations are managed as theory data, with proper name space and entity markup;
wenzelm
parents:
43329
diff
changeset
|
207 |
val pretty_typ_bracket = Syntax.pretty_typ (Config.put pretty_priority 1001 ctxt); |
9864182c6bad
document antiquotations are managed as theory data, with proper name space and entity markup;
wenzelm
parents:
43329
diff
changeset
|
208 |
fun pretty_constr (co, tys) = |
9864182c6bad
document antiquotations are managed as theory data, with proper name space and entity markup;
wenzelm
parents:
43329
diff
changeset
|
209 |
Pretty.block (Pretty.breaks |
9864182c6bad
document antiquotations are managed as theory data, with proper name space and entity markup;
wenzelm
parents:
43329
diff
changeset
|
210 |
(Syntax.pretty_term ctxt (Const (co, tys ---> ty)) :: |
9864182c6bad
document antiquotations are managed as theory data, with proper name space and entity markup;
wenzelm
parents:
43329
diff
changeset
|
211 |
map pretty_typ_bracket tys)); |
9864182c6bad
document antiquotations are managed as theory data, with proper name space and entity markup;
wenzelm
parents:
43329
diff
changeset
|
212 |
val pretty_datatype = |
9864182c6bad
document antiquotations are managed as theory data, with proper name space and entity markup;
wenzelm
parents:
43329
diff
changeset
|
213 |
Pretty.block |
9864182c6bad
document antiquotations are managed as theory data, with proper name space and entity markup;
wenzelm
parents:
43329
diff
changeset
|
214 |
(Pretty.command "datatype" :: Pretty.brk 1 :: |
9864182c6bad
document antiquotations are managed as theory data, with proper name space and entity markup;
wenzelm
parents:
43329
diff
changeset
|
215 |
Syntax.pretty_typ ctxt ty :: |
9864182c6bad
document antiquotations are managed as theory data, with proper name space and entity markup;
wenzelm
parents:
43329
diff
changeset
|
216 |
Pretty.str " =" :: Pretty.brk 1 :: |
9864182c6bad
document antiquotations are managed as theory data, with proper name space and entity markup;
wenzelm
parents:
43329
diff
changeset
|
217 |
flat (separate [Pretty.brk 1, Pretty.str "| "] (map (single o pretty_constr) cos))); |
9864182c6bad
document antiquotations are managed as theory data, with proper name space and entity markup;
wenzelm
parents:
43329
diff
changeset
|
218 |
in |
9864182c6bad
document antiquotations are managed as theory data, with proper name space and entity markup;
wenzelm
parents:
43329
diff
changeset
|
219 |
Thy_Output.output ctxt |
9864182c6bad
document antiquotations are managed as theory data, with proper name space and entity markup;
wenzelm
parents:
43329
diff
changeset
|
220 |
(Thy_Output.maybe_pretty_source (K (K pretty_datatype)) ctxt src [()]) |
9864182c6bad
document antiquotations are managed as theory data, with proper name space and entity markup;
wenzelm
parents:
43329
diff
changeset
|
221 |
end); |
33968
f94fb13ecbb3
modernized structures and tuned headers of datatype package modules; joined former datatype.ML and datatype_rep_proofs.ML
haftmann
parents:
33963
diff
changeset
|
222 |
|
f94fb13ecbb3
modernized structures and tuned headers of datatype package modules; joined former datatype.ML and datatype_rep_proofs.ML
haftmann
parents:
33963
diff
changeset
|
223 |
|
f94fb13ecbb3
modernized structures and tuned headers of datatype package modules; joined former datatype.ML and datatype_rep_proofs.ML
haftmann
parents:
33963
diff
changeset
|
224 |
|
33970 | 225 |
(** abstract theory extensions relative to a datatype characterisation **) |
33968
f94fb13ecbb3
modernized structures and tuned headers of datatype package modules; joined former datatype.ML and datatype_rep_proofs.ML
haftmann
parents:
33963
diff
changeset
|
226 |
|
33970 | 227 |
structure Datatype_Interpretation = Interpretation |
45700 | 228 |
( |
229 |
type T = Datatype_Aux.config * string list; |
|
230 |
val eq: T * T -> bool = eq_snd (op =); |
|
231 |
); |
|
33970 | 232 |
fun interpretation f = Datatype_Interpretation.interpretation (uncurry f); |
45890 | 233 |
val interpretation_data = Datatype_Interpretation.data; |
33968
f94fb13ecbb3
modernized structures and tuned headers of datatype package modules; joined former datatype.ML and datatype_rep_proofs.ML
haftmann
parents:
33963
diff
changeset
|
234 |
|
f94fb13ecbb3
modernized structures and tuned headers of datatype package modules; joined former datatype.ML and datatype_rep_proofs.ML
haftmann
parents:
33963
diff
changeset
|
235 |
|
f94fb13ecbb3
modernized structures and tuned headers of datatype package modules; joined former datatype.ML and datatype_rep_proofs.ML
haftmann
parents:
33963
diff
changeset
|
236 |
|
45890 | 237 |
(** setup theory **) |
33970 | 238 |
|
239 |
val setup = |
|
43564
9864182c6bad
document antiquotations are managed as theory data, with proper name space and entity markup;
wenzelm
parents:
43329
diff
changeset
|
240 |
antiq_setup #> |
33970 | 241 |
Datatype_Interpretation.init; |
242 |
||
41423 | 243 |
open Datatype_Aux; |
244 |
||
30391
d930432adb13
adapted to simplified ThyOutput.antiquotation interface;
wenzelm
parents:
30364
diff
changeset
|
245 |
end; |