11 exception NotFound |
11 exception NotFound |
12 |
12 |
13 type maps_info = {mapfun: string, relmap: string} |
13 type maps_info = {mapfun: string, relmap: string} |
14 val maps_defined: theory -> string -> bool |
14 val maps_defined: theory -> string -> bool |
15 val maps_lookup: theory -> string -> maps_info (* raises NotFound *) |
15 val maps_lookup: theory -> string -> maps_info (* raises NotFound *) |
16 val maps_update_thy: string -> maps_info -> theory -> theory |
16 val maps_update_thy: string -> maps_info -> theory -> theory |
17 val maps_update: string -> maps_info -> Proof.context -> Proof.context |
17 val maps_update: string -> maps_info -> Proof.context -> Proof.context |
18 val print_mapsinfo: Proof.context -> unit |
18 val print_mapsinfo: Proof.context -> unit |
19 |
19 |
20 type quotdata_info = {qtyp: typ, rtyp: typ, equiv_rel: term, equiv_thm: thm} |
20 type quotdata_info = {qtyp: typ, rtyp: typ, equiv_rel: term, equiv_thm: thm} |
21 val transform_quotdata: morphism -> quotdata_info -> quotdata_info |
21 val transform_quotdata: morphism -> quotdata_info -> quotdata_info |
22 val quotdata_lookup_raw: theory -> string -> quotdata_info option |
22 val quotdata_lookup_raw: theory -> string -> quotdata_info option |
34 val qconsts_dest: Proof.context -> qconsts_info list |
34 val qconsts_dest: Proof.context -> qconsts_info list |
35 val print_qconstinfo: Proof.context -> unit |
35 val print_qconstinfo: Proof.context -> unit |
36 |
36 |
37 val equiv_rules_get: Proof.context -> thm list |
37 val equiv_rules_get: Proof.context -> thm list |
38 val equiv_rules_add: attribute |
38 val equiv_rules_add: attribute |
39 val rsp_rules_get: Proof.context -> thm list |
39 val rsp_rules_get: Proof.context -> thm list |
40 val prs_rules_get: Proof.context -> thm list |
40 val prs_rules_get: Proof.context -> thm list |
41 val id_simps_get: Proof.context -> thm list |
41 val id_simps_get: Proof.context -> thm list |
42 val quotient_rules_get: Proof.context -> thm list |
42 val quotient_rules_get: Proof.context -> thm list |
43 val quotient_rules_add: attribute |
43 val quotient_rules_add: attribute |
44 end; |
44 end; |
45 |
45 |
59 (type T = maps_info Symtab.table |
59 (type T = maps_info Symtab.table |
60 val empty = Symtab.empty |
60 val empty = Symtab.empty |
61 val extend = I |
61 val extend = I |
62 val merge = Symtab.merge (K true)) |
62 val merge = Symtab.merge (K true)) |
63 |
63 |
64 fun maps_defined thy s = |
64 fun maps_defined thy s = |
65 Symtab.defined (MapsData.get thy) s |
65 Symtab.defined (MapsData.get thy) s |
66 |
66 |
67 fun maps_lookup thy s = |
67 fun maps_lookup thy s = |
68 case (Symtab.lookup (MapsData.get thy) s) of |
68 case (Symtab.lookup (MapsData.get thy) s) of |
69 SOME map_fun => map_fun |
69 SOME map_fun => map_fun |
70 | NONE => raise NotFound |
70 | NONE => raise NotFound |
71 |
71 |
72 fun maps_update_thy k minfo = MapsData.map (Symtab.update (k, minfo)) |
72 fun maps_update_thy k minfo = MapsData.map (Symtab.update (k, minfo)) |
73 fun maps_update k minfo = ProofContext.theory (maps_update_thy k minfo) |
73 fun maps_update k minfo = ProofContext.theory (maps_update_thy k minfo) |
74 |
74 |
75 fun maps_attribute_aux s minfo = Thm.declaration_attribute |
75 fun maps_attribute_aux s minfo = Thm.declaration_attribute |
76 (fn _ => Context.mapping (maps_update_thy s minfo) (maps_update s minfo)) |
76 (fn _ => Context.mapping (maps_update_thy s minfo) (maps_update s minfo)) |
77 |
77 |
78 (* attribute to be used in declare statements *) |
78 (* attribute to be used in declare statements *) |
79 fun maps_attribute (ctxt, (tystr, (mapstr, relstr))) = |
79 fun maps_attribute (ctxt, (tystr, (mapstr, relstr))) = |
80 let |
80 let |
81 val thy = ProofContext.theory_of ctxt |
81 val thy = ProofContext.theory_of ctxt |
82 val tyname = Sign.intern_type thy tystr |
82 val tyname = Sign.intern_type thy tystr |
83 val mapname = Sign.intern_const thy mapstr |
83 val mapname = Sign.intern_const thy mapstr |
84 val relname = Sign.intern_const thy relstr |
84 val relname = Sign.intern_const thy relstr |
85 |
85 |
87 val _ = List.app sanity_check [mapname, relname] |
87 val _ = List.app sanity_check [mapname, relname] |
88 in |
88 in |
89 maps_attribute_aux tyname {mapfun = mapname, relmap = relname} |
89 maps_attribute_aux tyname {mapfun = mapname, relmap = relname} |
90 end |
90 end |
91 |
91 |
92 val maps_attr_parser = |
92 val maps_attr_parser = |
93 Args.context -- Scan.lift |
93 Args.context -- Scan.lift |
94 ((Args.name --| OuterParse.$$$ "=") -- |
94 ((Args.name --| OuterParse.$$$ "=") -- |
95 (OuterParse.$$$ "(" |-- Args.name --| OuterParse.$$$ "," -- |
95 (OuterParse.$$$ "(" |-- Args.name --| OuterParse.$$$ "," -- |
96 Args.name --| OuterParse.$$$ ")")) |
96 Args.name --| OuterParse.$$$ ")")) |
97 |
97 |
98 val _ = Context.>> (Context.map_theory |
98 val _ = Context.>> (Context.map_theory |
99 (Attrib.setup @{binding "map"} (maps_attr_parser >> maps_attribute) |
99 (Attrib.setup @{binding "map"} (maps_attr_parser >> maps_attribute) |
100 "declaration of map information")) |
100 "declaration of map information")) |
101 |
101 |
102 fun print_mapsinfo ctxt = |
102 fun print_mapsinfo ctxt = |
103 let |
103 let |
104 fun prt_map (ty_name, {mapfun, relmap}) = |
104 fun prt_map (ty_name, {mapfun, relmap}) = |
105 Pretty.block (Library.separate (Pretty.brk 2) |
105 Pretty.block (Library.separate (Pretty.brk 2) |
106 (map Pretty.str |
106 (map Pretty.str |
107 ["type:", ty_name, |
107 ["type:", ty_name, |
108 "map:", mapfun, |
108 "map:", mapfun, |
109 "relation map:", relmap])) |
109 "relation map:", relmap])) |
110 in |
110 in |
111 MapsData.get (ProofContext.theory_of ctxt) |
111 MapsData.get (ProofContext.theory_of ctxt) |
112 |> Symtab.dest |
112 |> Symtab.dest |
113 |> map (prt_map) |
113 |> map (prt_map) |
114 |> Pretty.big_list "maps for type constructors:" |
114 |> Pretty.big_list "maps for type constructors:" |
115 |> Pretty.writeln |
115 |> Pretty.writeln |
116 end |
116 end |
117 |
117 |
118 |
118 |
119 (* info about quotient types *) |
119 (* info about quotient types *) |
120 type quotdata_info = {qtyp: typ, rtyp: typ, equiv_rel: term, equiv_thm: thm} |
120 type quotdata_info = {qtyp: typ, rtyp: typ, equiv_rel: term, equiv_thm: thm} |
121 |
121 |
122 structure QuotData = Theory_Data |
122 structure QuotData = Theory_Data |
123 (type T = quotdata_info Symtab.table |
123 (type T = quotdata_info Symtab.table |
124 val empty = Symtab.empty |
124 val empty = Symtab.empty |
125 val extend = I |
125 val extend = I |
126 val merge = Symtab.merge (K true)) |
126 val merge = Symtab.merge (K true)) |
127 |
127 |
128 fun transform_quotdata phi {qtyp, rtyp, equiv_rel, equiv_thm} = |
128 fun transform_quotdata phi {qtyp, rtyp, equiv_rel, equiv_thm} = |
129 {qtyp = Morphism.typ phi qtyp, |
129 {qtyp = Morphism.typ phi qtyp, |
130 rtyp = Morphism.typ phi rtyp, |
130 rtyp = Morphism.typ phi rtyp, |
131 equiv_rel = Morphism.term phi equiv_rel, |
131 equiv_rel = Morphism.term phi equiv_rel, |