5 val maps_update_thy: string -> maps_info -> theory -> theory |
5 val maps_update_thy: string -> maps_info -> theory -> theory |
6 val maps_update: string -> maps_info -> Proof.context -> Proof.context |
6 val maps_update: string -> maps_info -> Proof.context -> Proof.context |
7 |
7 |
8 type quotient_info = {qtyp: typ, rtyp: typ, rel: term, equiv_thm: thm} |
8 type quotient_info = {qtyp: typ, rtyp: typ, rel: term, equiv_thm: thm} |
9 val print_quotinfo: Proof.context -> unit |
9 val print_quotinfo: Proof.context -> unit |
10 val quotdata_lookup_thy: theory -> quotient_info list |
10 val quotdata_lookup_thy: theory -> string -> quotient_info option |
11 val quotdata_lookup: Proof.context -> quotient_info list |
11 val quotdata_lookup: Proof.context -> string -> quotient_info option |
12 val quotdata_update_thy: (typ * typ * term * thm) -> theory -> theory |
12 val quotdata_update_thy: string -> (typ * typ * term * thm) -> theory -> theory |
13 val quotdata_update: (typ * typ * term * thm) -> Proof.context -> Proof.context |
13 val quotdata_update: string -> (typ * typ * term * thm) -> Proof.context -> Proof.context |
14 |
14 |
15 type qenv = (typ * typ) list |
15 type qenv = (typ * typ) list |
16 val mk_qenv: Proof.context -> qenv |
16 val mk_qenv: Proof.context -> qenv |
17 val lookup_qenv: ((typ * typ) -> bool) -> qenv -> typ -> (typ * typ) option |
17 val lookup_qenv: ((typ * typ) -> bool) -> qenv -> typ -> (typ * typ) option |
18 |
18 |
38 val empty = Symtab.empty |
38 val empty = Symtab.empty |
39 val extend = I |
39 val extend = I |
40 val merge = Symtab.merge (K true)) |
40 val merge = Symtab.merge (K true)) |
41 |
41 |
42 val maps_lookup = Symtab.lookup o MapsData.get |
42 val maps_lookup = Symtab.lookup o MapsData.get |
43 |
|
44 |
43 |
45 fun maps_update_thy k minfo = MapsData.map (Symtab.update (k, minfo)) |
44 fun maps_update_thy k minfo = MapsData.map (Symtab.update (k, minfo)) |
46 fun maps_update k minfo = ProofContext.theory (maps_update_thy k minfo) |
45 fun maps_update k minfo = ProofContext.theory (maps_update_thy k minfo) |
47 |
46 |
48 fun maps_attribute_aux s minfo = Thm.declaration_attribute |
47 fun maps_attribute_aux s minfo = Thm.declaration_attribute |
72 |
71 |
73 (* info about the quotient types *) |
72 (* info about the quotient types *) |
74 type quotient_info = {qtyp: typ, rtyp: typ, rel: term, equiv_thm: thm} |
73 type quotient_info = {qtyp: typ, rtyp: typ, rel: term, equiv_thm: thm} |
75 |
74 |
76 structure QuotData = Theory_Data |
75 structure QuotData = Theory_Data |
77 (type T = quotient_info list |
76 (type T = quotient_info Symtab.table |
78 val empty = [] |
77 val empty = Symtab.empty |
79 val extend = I |
78 val extend = I |
80 val merge = (op @)) (* FIXME: is this the correct merging function for the list? *) |
79 val merge = Symtab.merge (K true)) |
81 |
80 |
82 val quotdata_lookup_thy = QuotData.get |
81 val quotdata_lookup_thy = Symtab.lookup o QuotData.get |
83 val quotdata_lookup = QuotData.get o ProofContext.theory_of |
82 val quotdata_lookup = quotdata_lookup_thy o ProofContext.theory_of |
84 |
83 |
85 fun quotdata_update_thy (qty, rty, rel, equiv_thm) thy = |
84 fun quotdata_update_thy qty_name (qty, rty, rel, equiv_thm) = |
86 QuotData.map (fn ls => {qtyp = qty, rtyp = rty, rel = rel, equiv_thm = equiv_thm}::ls) thy |
85 QuotData.map (Symtab.update (qty_name, {qtyp = qty, rtyp = rty, rel = rel, equiv_thm = equiv_thm})) |
87 |
86 |
88 fun quotdata_update (qty, rty, rel, equiv_thm) ctxt = |
87 fun quotdata_update qty_name (qty, rty, rel, equiv_thm) = |
89 ProofContext.theory (quotdata_update_thy (qty, rty, rel, equiv_thm)) ctxt |
88 ProofContext.theory (quotdata_update_thy qty_name (qty, rty, rel, equiv_thm)) |
90 |
89 |
91 fun print_quotinfo ctxt = |
90 fun print_quotinfo ctxt = |
92 let |
91 let |
93 fun prt_quot {qtyp, rtyp, rel, equiv_thm} = |
92 fun prt_quot {qtyp, rtyp, rel, equiv_thm} = |
94 Pretty.block (Library.separate (Pretty.brk 2) |
93 Pretty.block (Library.separate (Pretty.brk 2) |
100 Syntax.pretty_term ctxt rel, |
99 Syntax.pretty_term ctxt rel, |
101 Pretty.str ("equiv. thm:"), |
100 Pretty.str ("equiv. thm:"), |
102 Syntax.pretty_term ctxt (prop_of equiv_thm)]) |
101 Syntax.pretty_term ctxt (prop_of equiv_thm)]) |
103 in |
102 in |
104 QuotData.get (ProofContext.theory_of ctxt) |
103 QuotData.get (ProofContext.theory_of ctxt) |
105 |> map prt_quot |
104 |> Symtab.dest |
|
105 |> map (prt_quot o snd) |
106 |> Pretty.big_list "quotients:" |
106 |> Pretty.big_list "quotients:" |
107 |> Pretty.writeln |
107 |> Pretty.writeln |
108 end |
108 end |
109 |
109 |
110 val _ = |
110 val _ = |
115 (* environments of quotient and raw types *) |
115 (* environments of quotient and raw types *) |
116 type qenv = (typ * typ) list |
116 type qenv = (typ * typ) list |
117 |
117 |
118 fun mk_qenv ctxt = |
118 fun mk_qenv ctxt = |
119 let |
119 let |
120 val qinfo = quotdata_lookup ctxt |
120 val thy = ProofContext.theory_of ctxt |
|
121 val qinfo = (QuotData.get thy) |> Symtab.dest |> map snd |
121 in |
122 in |
122 map (fn {qtyp, rtyp, ...} => (qtyp, rtyp)) qinfo |
123 map (fn {qtyp, rtyp, ...} => (qtyp, rtyp)) qinfo |
123 end |
124 end |
124 |
125 |
125 fun lookup_qenv _ [] _ = NONE |
126 fun lookup_qenv _ [] _ = NONE |