|
1 signature QUOTIENT_INFO = |
|
2 sig |
|
3 type maps_info = {mapfun: string, relfun: string} |
|
4 val maps_lookup: theory -> string -> maps_info option |
|
5 val maps_update_thy: string -> maps_info -> theory -> theory |
|
6 val maps_update: string -> maps_info -> Proof.context -> Proof.context |
|
7 |
|
8 type quotient_info = {qtyp: typ, rtyp: typ, rel: term, equiv_thm: thm} |
|
9 val print_quotdata: Proof.context -> unit |
|
10 val quotdata_lookup_thy: theory -> quotient_info list |
|
11 val quotdata_lookup: Proof.context -> quotient_info list |
|
12 val quotdata_update_thy: (typ * typ * term * thm) -> theory -> theory |
|
13 val quotdata_update: (typ * typ * term * thm) -> Proof.context -> Proof.context |
|
14 end; |
|
15 |
|
16 structure Quotient_Info: QUOTIENT_INFO = |
|
17 struct |
|
18 |
|
19 (* data containers *) |
|
20 (*******************) |
|
21 |
|
22 (* info about map- and rel-functions *) |
|
23 type maps_info = {mapfun: string, relfun: string} |
|
24 |
|
25 structure MapsData = TheoryDataFun |
|
26 (type T = maps_info Symtab.table |
|
27 val empty = Symtab.empty |
|
28 val copy = I |
|
29 val extend = I |
|
30 fun merge _ = Symtab.merge (K true)) |
|
31 |
|
32 val maps_lookup = Symtab.lookup o MapsData.get |
|
33 |
|
34 |
|
35 fun maps_update_thy k minfo = MapsData.map (Symtab.update (k, minfo)) |
|
36 fun maps_update k minfo = ProofContext.theory (maps_update_thy k minfo) |
|
37 |
|
38 fun maps_attribute_aux s minfo = Thm.declaration_attribute |
|
39 (fn thm => Context.mapping (maps_update_thy s minfo) (maps_update s minfo)) |
|
40 |
|
41 (* attribute to be used in declare statements *) |
|
42 fun maps_attribute (ctxt, (tystr, (mapstr, relstr))) = |
|
43 let |
|
44 val thy = ProofContext.theory_of ctxt |
|
45 val tyname = Sign.intern_type thy tystr |
|
46 val mapname = Sign.intern_const thy mapstr |
|
47 val relname = Sign.intern_const thy relstr |
|
48 in |
|
49 maps_attribute_aux tyname {mapfun = mapname, relfun = relname} |
|
50 end |
|
51 |
|
52 val maps_attr_parser = |
|
53 Args.context -- Scan.lift |
|
54 ((Args.name --| OuterParse.$$$ "=") -- |
|
55 (OuterParse.$$$ "(" |-- Args.name --| OuterParse.$$$ "," -- |
|
56 Args.name --| OuterParse.$$$ ")")) |
|
57 |
|
58 val _ = Context.>> (Context.map_theory |
|
59 (Attrib.setup @{binding "map"} (maps_attr_parser >> maps_attribute) |
|
60 "declaration of map information")) |
|
61 |
|
62 |
|
63 (* info about the quotient types *) |
|
64 type quotient_info = {qtyp: typ, rtyp: typ, rel: term, equiv_thm: thm} |
|
65 |
|
66 structure QuotData = TheoryDataFun |
|
67 (type T = quotient_info list |
|
68 val empty = [] |
|
69 val copy = I |
|
70 val extend = I |
|
71 fun merge _ = (op @)) (* FIXME: is this the correct merging function for the list? *) |
|
72 |
|
73 val quotdata_lookup_thy = QuotData.get |
|
74 val quotdata_lookup = QuotData.get o ProofContext.theory_of |
|
75 |
|
76 fun quotdata_update_thy (qty, rty, rel, equiv_thm) thy = |
|
77 QuotData.map (fn ls => {qtyp = qty, rtyp = rty, rel = rel, equiv_thm = equiv_thm}::ls) thy |
|
78 |
|
79 fun quotdata_update (qty, rty, rel, equiv_thm) ctxt = |
|
80 ProofContext.theory (quotdata_update_thy (qty, rty, rel, equiv_thm)) ctxt |
|
81 |
|
82 fun print_quotdata ctxt = |
|
83 let |
|
84 fun prt_quot {qtyp, rtyp, rel, equiv_thm} = |
|
85 Pretty.block (Library.separate (Pretty.brk 2) |
|
86 [Pretty.str ("quotient type:"), |
|
87 Syntax.pretty_typ ctxt qtyp, |
|
88 Pretty.str ("raw type:"), |
|
89 Syntax.pretty_typ ctxt rtyp, |
|
90 Pretty.str ("relation:"), |
|
91 Syntax.pretty_term ctxt rel, |
|
92 Pretty.str ("equiv. thm:"), |
|
93 Syntax.pretty_term ctxt (prop_of equiv_thm)]) |
|
94 in |
|
95 QuotData.get (ProofContext.theory_of ctxt) |
|
96 |> map prt_quot |
|
97 |> Pretty.big_list "quotients:" |
|
98 |> Pretty.writeln |
|
99 end |
|
100 |
|
101 val _ = |
|
102 OuterSyntax.improper_command "print_quotients" "print out all quotients" |
|
103 OuterKeyword.diag (Scan.succeed (Toplevel.keep (print_quotdata o Toplevel.context_of))) |
|
104 |
|
105 end; (* structure *) |
|
106 |
|
107 open Quotient_Info |