|
1 (* Author: Christian Urban |
|
2 |
|
3 data about nominal datatypes |
|
4 *) |
|
5 |
|
6 signature NOMINAL_DT_DATA = |
|
7 sig |
|
8 type info = |
|
9 {inject : thm list, |
|
10 distinct : thm list, |
|
11 strong_inducts : thm list, |
|
12 strong_exhaust : thm list} |
|
13 |
|
14 val get_all_info: Proof.context -> (string * info) list |
|
15 val get_info: Proof.context -> string -> info option |
|
16 val the_info: Proof.context -> string -> info |
|
17 val register_info: (string * info) -> Context.generic -> Context.generic |
|
18 val mk_infos: string list -> thm list -> thm list -> thm list -> thm list -> (string * info) list |
|
19 end |
|
20 |
|
21 structure Nominal_Dt_Data: NOMINAL_DT_DATA = |
|
22 struct |
|
23 |
|
24 (* information generated by nominal_datatype *) |
|
25 type info = |
|
26 {inject : thm list, |
|
27 distinct : thm list, |
|
28 strong_inducts : thm list, |
|
29 strong_exhaust : thm list} |
|
30 |
|
31 structure NominalData = Generic_Data |
|
32 (type T = info Symtab.table |
|
33 val empty = Symtab.empty |
|
34 val extend = I |
|
35 val merge = Symtab.merge (K true)) |
|
36 |
|
37 val get_all_info = Symtab.dest o NominalData.get o Context.Proof |
|
38 val get_info = Symtab.lookup o NominalData.get o Context.Proof |
|
39 val register_info = NominalData.map o Symtab.update |
|
40 |
|
41 fun the_info thy name = |
|
42 (case get_info thy name of |
|
43 SOME info => info |
|
44 | NONE => error ("Unknown nominal datatype " ^ quote name)) |
|
45 |
|
46 fun mk_infos ty_names inject distinct strong_inducts strong_exhaust = |
|
47 let |
|
48 fun aux ty_name = |
|
49 (ty_name, {inject = inject, |
|
50 distinct = distinct, |
|
51 strong_inducts = strong_inducts, |
|
52 strong_exhaust = strong_exhaust |
|
53 }) |
|
54 in |
|
55 map aux ty_names |
|
56 end |
|
57 |
|
58 |
|
59 end |