author | blanchet |
Wed, 24 Sep 2014 15:45:55 +0200 | |
changeset 58425 | 246985c6b20b |
parent 58256 | 08c0f0d4b9f4 |
child 58661 | 2b9485a2d152 |
permissions | -rw-r--r-- |
58112
8081087096ad
renamed modules defining old datatypes, as a step towards having 'datatype_new' take 'datatype's place
blanchet
parents:
58111
diff
changeset
|
1 |
(* Title: HOL/Tools/Old_Datatype/old_datatype_data.ML |
11539 | 2 |
Author: Stefan Berghofer, TU Muenchen |
5177 | 3 |
|
45890 | 4 |
Datatype package bookkeeping. |
5177 | 5 |
*) |
6 |
||
58112
8081087096ad
renamed modules defining old datatypes, as a step towards having 'datatype_new' take 'datatype's place
blanchet
parents:
58111
diff
changeset
|
7 |
signature OLD_DATATYPE_DATA = |
6360 | 8 |
sig |
58112
8081087096ad
renamed modules defining old datatypes, as a step towards having 'datatype_new' take 'datatype's place
blanchet
parents:
58111
diff
changeset
|
9 |
include OLD_DATATYPE_COMMON |
58111 | 10 |
|
45890 | 11 |
val get_all : theory -> info Symtab.table |
33970 | 12 |
val get_info : theory -> string -> info option |
13 |
val the_info : theory -> string -> info |
|
45890 | 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 |
|
45701 | 19 |
val the_descr : theory -> string list -> |
20 |
descr * (string * sort) list * string list * string * |
|
21 |
(string list * string list) * (typ list * typ list) |
|
33970 | 22 |
val all_distincts : theory -> typ list -> thm list list |
23 |
val get_constrs : theory -> string -> (string * typ) list option |
|
45890 | 24 |
val mk_case_names_induct: descr -> attribute |
25 |
val mk_case_names_exhausts: descr -> string list -> attribute list |
|
33970 | 26 |
val interpretation : (config -> string list -> theory -> theory) -> theory -> theory |
45890 | 27 |
val interpretation_data : config * string list -> 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 |
|
58112
8081087096ad
renamed modules defining old datatypes, as a step towards having 'datatype_new' take 'datatype's place
blanchet
parents:
58111
diff
changeset
|
30 |
structure Old_Datatype_Data: OLD_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 = |
|
58112
8081087096ad
renamed modules defining old datatypes, as a step towards having 'datatype_new' take 'datatype's place
blanchet
parents:
58111
diff
changeset
|
40 |
{types: Old_Datatype_Aux.info Symtab.table, |
8081087096ad
renamed modules defining old datatypes, as a step towards having 'datatype_new' take 'datatype's place
blanchet
parents:
58111
diff
changeset
|
41 |
constrs: (string * Old_Datatype_Aux.info) list Symtab.table, |
8081087096ad
renamed modules defining old datatypes, as a step towards having 'datatype_new' take 'datatype's place
blanchet
parents:
58111
diff
changeset
|
42 |
cases: Old_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 |
|
58255 | 61 |
| NONE => error ("Unknown old-style 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 |
|
54400 | 89 |
fun ctrs_of_exhaust exhaust = |
90 |
Logic.strip_imp_prems (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 |
||
94 |
fun case_of_case_rewrite case_rewrite = |
|
95 |
head_of (fst (HOLogic.dest_eq (HOLogic.dest_Trueprop (prop_of case_rewrite)))); |
|
96 |
||
97 |
fun ctr_sugar_of_info ({exhaust, nchotomy, inject, distinct, case_rewrites, case_cong, |
|
58112
8081087096ad
renamed modules defining old datatypes, as a step towards having 'datatype_new' take 'datatype's place
blanchet
parents:
58111
diff
changeset
|
98 |
case_cong_weak, split, split_asm, ...} : Old_Datatype_Aux.info) = |
58187
d2ddd401d74d
fixed infinite loops in 'register' functions + more uniform API
blanchet
parents:
58112
diff
changeset
|
99 |
let val ctrs as ctr1 :: _ = ctrs_of_exhaust exhaust in |
d2ddd401d74d
fixed infinite loops in 'register' functions + more uniform API
blanchet
parents:
58112
diff
changeset
|
100 |
{T = body_type (fastype_of ctr1), |
d2ddd401d74d
fixed infinite loops in 'register' functions + more uniform API
blanchet
parents:
58112
diff
changeset
|
101 |
ctrs = ctrs, |
d2ddd401d74d
fixed infinite loops in 'register' functions + more uniform API
blanchet
parents:
58112
diff
changeset
|
102 |
casex = case_of_case_rewrite (hd case_rewrites), |
d2ddd401d74d
fixed infinite loops in 'register' functions + more uniform API
blanchet
parents:
58112
diff
changeset
|
103 |
discs = [], |
d2ddd401d74d
fixed infinite loops in 'register' functions + more uniform API
blanchet
parents:
58112
diff
changeset
|
104 |
selss = [], |
d2ddd401d74d
fixed infinite loops in 'register' functions + more uniform API
blanchet
parents:
58112
diff
changeset
|
105 |
exhaust = exhaust, |
d2ddd401d74d
fixed infinite loops in 'register' functions + more uniform API
blanchet
parents:
58112
diff
changeset
|
106 |
nchotomy = nchotomy, |
d2ddd401d74d
fixed infinite loops in 'register' functions + more uniform API
blanchet
parents:
58112
diff
changeset
|
107 |
injects = inject, |
d2ddd401d74d
fixed infinite loops in 'register' functions + more uniform API
blanchet
parents:
58112
diff
changeset
|
108 |
distincts = distinct, |
d2ddd401d74d
fixed infinite loops in 'register' functions + more uniform API
blanchet
parents:
58112
diff
changeset
|
109 |
case_thms = case_rewrites, |
d2ddd401d74d
fixed infinite loops in 'register' functions + more uniform API
blanchet
parents:
58112
diff
changeset
|
110 |
case_cong = case_cong, |
d2ddd401d74d
fixed infinite loops in 'register' functions + more uniform API
blanchet
parents:
58112
diff
changeset
|
111 |
case_cong_weak = case_cong_weak, |
d2ddd401d74d
fixed infinite loops in 'register' functions + more uniform API
blanchet
parents:
58112
diff
changeset
|
112 |
split = split, |
d2ddd401d74d
fixed infinite loops in 'register' functions + more uniform API
blanchet
parents:
58112
diff
changeset
|
113 |
split_asm = split_asm, |
d2ddd401d74d
fixed infinite loops in 'register' functions + more uniform API
blanchet
parents:
58112
diff
changeset
|
114 |
disc_defs = [], |
d2ddd401d74d
fixed infinite loops in 'register' functions + more uniform API
blanchet
parents:
58112
diff
changeset
|
115 |
disc_thmss = [], |
d2ddd401d74d
fixed infinite loops in 'register' functions + more uniform API
blanchet
parents:
58112
diff
changeset
|
116 |
discIs = [], |
d2ddd401d74d
fixed infinite loops in 'register' functions + more uniform API
blanchet
parents:
58112
diff
changeset
|
117 |
sel_defs = [], |
d2ddd401d74d
fixed infinite loops in 'register' functions + more uniform API
blanchet
parents:
58112
diff
changeset
|
118 |
sel_thmss = [], |
d2ddd401d74d
fixed infinite loops in 'register' functions + more uniform API
blanchet
parents:
58112
diff
changeset
|
119 |
distinct_discsss = [], |
d2ddd401d74d
fixed infinite loops in 'register' functions + more uniform API
blanchet
parents:
58112
diff
changeset
|
120 |
exhaust_discs = [], |
d2ddd401d74d
fixed infinite loops in 'register' functions + more uniform API
blanchet
parents:
58112
diff
changeset
|
121 |
exhaust_sels = [], |
d2ddd401d74d
fixed infinite loops in 'register' functions + more uniform API
blanchet
parents:
58112
diff
changeset
|
122 |
collapses = [], |
d2ddd401d74d
fixed infinite loops in 'register' functions + more uniform API
blanchet
parents:
58112
diff
changeset
|
123 |
expands = [], |
d2ddd401d74d
fixed infinite loops in 'register' functions + more uniform API
blanchet
parents:
58112
diff
changeset
|
124 |
split_sels = [], |
d2ddd401d74d
fixed infinite loops in 'register' functions + more uniform API
blanchet
parents:
58112
diff
changeset
|
125 |
split_sel_asms = [], |
d2ddd401d74d
fixed infinite loops in 'register' functions + more uniform API
blanchet
parents:
58112
diff
changeset
|
126 |
case_eq_ifs = []} |
d2ddd401d74d
fixed infinite loops in 'register' functions + more uniform API
blanchet
parents:
58112
diff
changeset
|
127 |
end; |
54400 | 128 |
|
129 |
fun register dt_infos = |
|
45890 | 130 |
Data.map (fn {types, constrs, cases} => |
33970 | 131 |
{types = types |> fold Symtab.update dt_infos, |
132 |
constrs = constrs |> fold (fn (constr, dtname_info) => |
|
133 |
Symtab.map_default (constr, []) (cons dtname_info)) |
|
134 |
(maps (fn (dtname, info as {descr, index, ...}) => |
|
54400 | 135 |
map (rpair (dtname, info) o fst) (#3 (the (AList.lookup op = descr index)))) dt_infos), |
33970 | 136 |
cases = cases |> fold Symtab.update |
54400 | 137 |
(map (fn (_, info as {case_name, ...}) => (case_name, info)) dt_infos)}) #> |
58188 | 138 |
fold (Ctr_Sugar.default_register_ctr_sugar_global (K true) o ctr_sugar_of_info o snd) dt_infos; |
33970 | 139 |
|
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
|
140 |
|
33970 | 141 |
(* complex queries *) |
142 |
||
143 |
fun the_spec thy dtco = |
|
144 |
let |
|
45822 | 145 |
val {descr, index, ...} = the_info thy dtco; |
45821 | 146 |
val (_, dtys, raw_cos) = the (AList.lookup (op =) descr index); |
58112
8081087096ad
renamed modules defining old datatypes, as a step towards having 'datatype_new' take 'datatype's place
blanchet
parents:
58111
diff
changeset
|
147 |
val args = map Old_Datatype_Aux.dest_DtTFree dtys; |
8081087096ad
renamed modules defining old datatypes, as a step towards having 'datatype_new' take 'datatype's place
blanchet
parents:
58111
diff
changeset
|
148 |
val cos = map (fn (co, tys) => (co, map (Old_Datatype_Aux.typ_of_dtyp descr) tys)) raw_cos; |
45822 | 149 |
in (args, cos) end; |
33970 | 150 |
|
151 |
fun the_descr thy (raw_tycos as raw_tyco :: _) = |
|
152 |
let |
|
153 |
val info = the_info thy raw_tyco; |
|
154 |
val descr = #descr info; |
|
155 |
||
45822 | 156 |
val (_, dtys, _) = the (AList.lookup (op =) descr (#index info)); |
58112
8081087096ad
renamed modules defining old datatypes, as a step towards having 'datatype_new' take 'datatype's place
blanchet
parents:
58111
diff
changeset
|
157 |
val vs = map Old_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
|
158 |
|
58112
8081087096ad
renamed modules defining old datatypes, as a step towards having 'datatype_new' take 'datatype's place
blanchet
parents:
58111
diff
changeset
|
159 |
fun is_DtTFree (Old_Datatype_Aux.DtTFree _) = true |
45700 | 160 |
| is_DtTFree _ = false; |
33970 | 161 |
val k = find_index (fn (_, (_, dTs, _)) => not (forall is_DtTFree dTs)) descr; |
41423 | 162 |
val protoTs as (dataTs, _) = |
163 |
chop k descr |
|
164 |
|> (pairself o map) |
|
58112
8081087096ad
renamed modules defining old datatypes, as a step towards having 'datatype_new' take 'datatype's place
blanchet
parents:
58111
diff
changeset
|
165 |
(fn (_, (tyco, dTs, _)) => (tyco, map (Old_Datatype_Aux.typ_of_dtyp descr) dTs)); |
45700 | 166 |
|
33970 | 167 |
val tycos = map fst dataTs; |
45430 | 168 |
val _ = |
169 |
if eq_set (op =) (tycos, raw_tycos) then () |
|
45700 | 170 |
else |
171 |
error ("Type constructors " ^ commas_quote raw_tycos ^ |
|
58255 | 172 |
" do not belong exhaustively to one mutually recursive old-style datatype"); |
33970 | 173 |
|
174 |
val (Ts, Us) = (pairself o map) Type protoTs; |
|
175 |
||
45701 | 176 |
val names = map Long_Name.base_name tycos; |
45700 | 177 |
val (auxnames, _) = |
178 |
Name.make_context names |
|
58112
8081087096ad
renamed modules defining old datatypes, as a step towards having 'datatype_new' take 'datatype's place
blanchet
parents:
58111
diff
changeset
|
179 |
|> fold_map (Name.variant o Old_Datatype_Aux.name_of_typ) Us; |
33970 | 180 |
val prefix = space_implode "_" names; |
181 |
||
182 |
in (descr, vs, tycos, prefix, (names, auxnames), (Ts, Us)) end; |
|
183 |
||
184 |
fun all_distincts thy Ts = |
|
185 |
let |
|
186 |
fun add_tycos (Type (tyco, Ts)) = insert (op =) tyco #> fold add_tycos Ts |
|
187 |
| add_tycos _ = I; |
|
188 |
val tycos = fold add_tycos Ts []; |
|
189 |
in map_filter (Option.map #distinct o get_info thy) tycos end; |
|
190 |
||
191 |
fun get_constrs thy dtco = |
|
45700 | 192 |
(case try (the_spec thy) dtco of |
45822 | 193 |
SOME (args, cos) => |
45700 | 194 |
let |
195 |
fun subst (v, sort) = TVar ((v, 0), sort); |
|
196 |
fun subst_ty (TFree v) = subst v |
|
197 |
| subst_ty ty = ty; |
|
45822 | 198 |
val dty = Type (dtco, map subst args); |
45700 | 199 |
fun mk_co (co, tys) = (co, map (Term.map_atyps subst_ty) tys ---> dty); |
200 |
in SOME (map mk_co cos) end |
|
201 |
| 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
|
202 |
|
f94fb13ecbb3
modernized structures and tuned headers of datatype package modules; joined former datatype.ML and datatype_rep_proofs.ML
haftmann
parents:
33963
diff
changeset
|
203 |
|
f94fb13ecbb3
modernized structures and tuned headers of datatype package modules; joined former datatype.ML and datatype_rep_proofs.ML
haftmann
parents:
33963
diff
changeset
|
204 |
|
33970 | 205 |
(** 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
|
206 |
|
33970 | 207 |
(* case names *) |
208 |
||
209 |
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
|
210 |
|
58112
8081087096ad
renamed modules defining old datatypes, as a step towards having 'datatype_new' take 'datatype's place
blanchet
parents:
58111
diff
changeset
|
211 |
fun dt_recs (Old_Datatype_Aux.DtTFree _) = [] |
8081087096ad
renamed modules defining old datatypes, as a step towards having 'datatype_new' take 'datatype's place
blanchet
parents:
58111
diff
changeset
|
212 |
| dt_recs (Old_Datatype_Aux.DtType (_, dts)) = maps dt_recs dts |
8081087096ad
renamed modules defining old datatypes, as a step towards having 'datatype_new' take 'datatype's place
blanchet
parents:
58111
diff
changeset
|
213 |
| dt_recs (Old_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
|
214 |
|
58112
8081087096ad
renamed modules defining old datatypes, as a step towards having 'datatype_new' take 'datatype's place
blanchet
parents:
58111
diff
changeset
|
215 |
fun dt_cases (descr: Old_Datatype_Aux.descr) (_, args, constrs) = |
33970 | 216 |
let |
217 |
fun the_bname i = Long_Name.base_name (#1 (the (AList.lookup (op =) descr i))); |
|
218 |
val bnames = map the_bname (distinct (op =) (maps dt_recs args)); |
|
219 |
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
|
220 |
|
33970 | 221 |
fun induct_cases descr = |
58112
8081087096ad
renamed modules defining old datatypes, as a step towards having 'datatype_new' take 'datatype's place
blanchet
parents:
58111
diff
changeset
|
222 |
Old_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
|
223 |
|
33970 | 224 |
fun exhaust_cases descr i = dt_cases descr (the (AList.lookup (op =) descr i)); |
225 |
||
226 |
in |
|
227 |
||
228 |
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
|
229 |
|
33970 | 230 |
fun mk_case_names_exhausts descr new = |
231 |
map (Rule_Cases.case_names o exhaust_cases descr o #1) |
|
232 |
(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
|
233 |
|
33970 | 234 |
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
|
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 |
|
f94fb13ecbb3
modernized structures and tuned headers of datatype package modules; joined former datatype.ML and datatype_rep_proofs.ML
haftmann
parents:
33963
diff
changeset
|
237 |
|
33970 | 238 |
(** 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
|
239 |
|
33970 | 240 |
structure Datatype_Interpretation = Interpretation |
45700 | 241 |
( |
58112
8081087096ad
renamed modules defining old datatypes, as a step towards having 'datatype_new' take 'datatype's place
blanchet
parents:
58111
diff
changeset
|
242 |
type T = Old_Datatype_Aux.config * string list; |
45700 | 243 |
val eq: T * T -> bool = eq_snd (op =); |
244 |
); |
|
56375
32e0da92c786
use same idiom as used for datatype 'size' function to name constants and theorems emerging from various type interpretations -- reduces the chances of name clashes on theory merges
blanchet
parents:
55952
diff
changeset
|
245 |
|
32e0da92c786
use same idiom as used for datatype 'size' function to name constants and theorems emerging from various type interpretations -- reduces the chances of name clashes on theory merges
blanchet
parents:
55952
diff
changeset
|
246 |
fun with_repaired_path f config (type_names as name :: _) thy = |
32e0da92c786
use same idiom as used for datatype 'size' function to name constants and theorems emerging from various type interpretations -- reduces the chances of name clashes on theory merges
blanchet
parents:
55952
diff
changeset
|
247 |
thy |
32e0da92c786
use same idiom as used for datatype 'size' function to name constants and theorems emerging from various type interpretations -- reduces the chances of name clashes on theory merges
blanchet
parents:
55952
diff
changeset
|
248 |
|> Sign.root_path |
32e0da92c786
use same idiom as used for datatype 'size' function to name constants and theorems emerging from various type interpretations -- reduces the chances of name clashes on theory merges
blanchet
parents:
55952
diff
changeset
|
249 |
|> Sign.add_path (Long_Name.qualifier name) |
32e0da92c786
use same idiom as used for datatype 'size' function to name constants and theorems emerging from various type interpretations -- reduces the chances of name clashes on theory merges
blanchet
parents:
55952
diff
changeset
|
250 |
|> f config type_names |
32e0da92c786
use same idiom as used for datatype 'size' function to name constants and theorems emerging from various type interpretations -- reduces the chances of name clashes on theory merges
blanchet
parents:
55952
diff
changeset
|
251 |
|> Sign.restore_naming thy; |
32e0da92c786
use same idiom as used for datatype 'size' function to name constants and theorems emerging from various type interpretations -- reduces the chances of name clashes on theory merges
blanchet
parents:
55952
diff
changeset
|
252 |
|
32e0da92c786
use same idiom as used for datatype 'size' function to name constants and theorems emerging from various type interpretations -- reduces the chances of name clashes on theory merges
blanchet
parents:
55952
diff
changeset
|
253 |
fun interpretation f = Datatype_Interpretation.interpretation (uncurry (with_repaired_path f)); |
45890 | 254 |
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
|
255 |
|
f94fb13ecbb3
modernized structures and tuned headers of datatype package modules; joined former datatype.ML and datatype_rep_proofs.ML
haftmann
parents:
33963
diff
changeset
|
256 |
|
f94fb13ecbb3
modernized structures and tuned headers of datatype package modules; joined former datatype.ML and datatype_rep_proofs.ML
haftmann
parents:
33963
diff
changeset
|
257 |
|
45890 | 258 |
(** setup theory **) |
33970 | 259 |
|
58256
08c0f0d4b9f4
generalized 'datatype' LaTeX antiquotation and added 'codatatype'
blanchet
parents:
58255
diff
changeset
|
260 |
val _ = Theory.setup Datatype_Interpretation.init; |
33970 | 261 |
|
58112
8081087096ad
renamed modules defining old datatypes, as a step towards having 'datatype_new' take 'datatype's place
blanchet
parents:
58111
diff
changeset
|
262 |
open Old_Datatype_Aux; |
41423 | 263 |
|
30391
d930432adb13
adapted to simplified ThyOutput.antiquotation interface;
wenzelm
parents:
30364
diff
changeset
|
264 |
end; |