|
1 (* Title: HOL/Tools/Datatype/datatype_selectors.ML |
|
2 Author: Sascha Boehme, TU Muenchen |
|
3 |
|
4 Selector functions for datatype constructor arguments. |
|
5 *) |
|
6 |
|
7 signature DATATYPE_SELECTORS = |
|
8 sig |
|
9 val add_selector: ((string * typ) * int) * (string * typ) -> |
|
10 Context.generic -> Context.generic |
|
11 val lookup_selector: Proof.context -> string * int -> string option |
|
12 val setup: theory -> theory |
|
13 end |
|
14 |
|
15 structure Datatype_Selectors: DATATYPE_SELECTORS = |
|
16 struct |
|
17 |
|
18 structure Stringinttab = Table |
|
19 ( |
|
20 type key = string * int |
|
21 val ord = prod_ord fast_string_ord int_ord |
|
22 ) |
|
23 |
|
24 structure Data = Generic_Data |
|
25 ( |
|
26 type T = string Stringinttab.table |
|
27 val empty = Stringinttab.empty |
|
28 val extend = I |
|
29 val merge = Stringinttab.merge (K true) |
|
30 ) |
|
31 |
|
32 fun pretty_term context = Syntax.pretty_term (Context.proof_of context) |
|
33 |
|
34 fun sanity_check context (((con as (n, _), i), sel as (m, _))) = |
|
35 let |
|
36 val thy = Context.theory_of context |
|
37 val varify_const = |
|
38 Const #> Type.varify_global [] #> snd #> Term.dest_Const #> |
|
39 snd #> Term.strip_type |
|
40 |
|
41 val (Ts, T) = varify_const con |
|
42 val (Us, U) = varify_const sel |
|
43 val _ = (0 < i andalso i <= length Ts) orelse |
|
44 error (Pretty.string_of (Pretty.block [ |
|
45 Pretty.str "The constructor ", |
|
46 Pretty.quote (pretty_term context (Const con)), |
|
47 Pretty.str " has no argument position ", |
|
48 Pretty.str (string_of_int i), |
|
49 Pretty.str "."])) |
|
50 val _ = length Us = 1 orelse |
|
51 error (Pretty.string_of (Pretty.block [ |
|
52 Pretty.str "The term ", Pretty.quote (pretty_term context (Const sel)), |
|
53 Pretty.str " might not be a selector ", |
|
54 Pretty.str "(it accepts more than one argument)."])) |
|
55 val _ = |
|
56 (Sign.typ_equiv thy (T, hd Us) andalso |
|
57 Sign.typ_equiv thy (nth Ts (i-1), U)) orelse |
|
58 error (Pretty.string_of (Pretty.block [ |
|
59 Pretty.str "The types of the constructor ", |
|
60 Pretty.quote (pretty_term context (Const con)), |
|
61 Pretty.str " and of the selector ", |
|
62 Pretty.quote (pretty_term context (Const sel)), |
|
63 Pretty.str " do not fit to each other."])) |
|
64 in ((n, i), m) end |
|
65 |
|
66 fun add_selector (entry as ((con as (n, _), i), (_, T))) context = |
|
67 (case Stringinttab.lookup (Data.get context) (n, i) of |
|
68 NONE => Data.map (Stringinttab.update (sanity_check context entry)) context |
|
69 | SOME c => error (Pretty.string_of (Pretty.block [ |
|
70 Pretty.str "There is already a selector assigned to constructor ", |
|
71 Pretty.quote (pretty_term context (Const con)), Pretty.str ", namely ", |
|
72 Pretty.quote (pretty_term context (Const (c, T))), Pretty.str "."]))) |
|
73 |
|
74 fun lookup_selector ctxt = Stringinttab.lookup (Data.get (Context.Proof ctxt)) |
|
75 |
|
76 val setup = |
|
77 Attrib.setup @{binding selector} |
|
78 ((Args.term >> Term.dest_Const) -- Scan.lift (Parse.nat) --| |
|
79 Scan.lift (Parse.$$$ "=") -- (Args.term >> Term.dest_Const) >> |
|
80 (Thm.declaration_attribute o K o add_selector)) |
|
81 "assign a selector function to a datatype constructor argument" |
|
82 |
|
83 end |