4 val maps_lookup: theory -> string -> maps_info option |
4 val maps_lookup: theory -> string -> maps_info option |
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_quotdata: 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 -> quotient_info list |
11 val quotdata_lookup: Proof.context -> quotient_info list |
11 val quotdata_lookup: Proof.context -> quotient_info list |
12 val quotdata_update_thy: (typ * typ * term * thm) -> theory -> theory |
12 val quotdata_update_thy: (typ * typ * term * thm) -> theory -> theory |
13 val quotdata_update: (typ * typ * term * thm) -> Proof.context -> Proof.context |
13 val quotdata_update: (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 |
|
19 type qconsts_info = {qconst: term, rconst: term} |
|
20 val qconsts_lookup: theory -> string -> qconsts_info option |
|
21 val qconsts_update_thy: string -> qconsts_info -> theory -> theory |
|
22 val qconsts_update: string -> qconsts_info -> Proof.context -> Proof.context |
|
23 val print_qconstinfo: Proof.context -> unit |
18 end; |
24 end; |
19 |
25 |
20 structure Quotient_Info: QUOTIENT_INFO = |
26 structure Quotient_Info: QUOTIENT_INFO = |
21 struct |
27 struct |
22 |
28 |
80 QuotData.map (fn ls => {qtyp = qty, rtyp = rty, rel = rel, equiv_thm = equiv_thm}::ls) thy |
86 QuotData.map (fn ls => {qtyp = qty, rtyp = rty, rel = rel, equiv_thm = equiv_thm}::ls) thy |
81 |
87 |
82 fun quotdata_update (qty, rty, rel, equiv_thm) ctxt = |
88 fun quotdata_update (qty, rty, rel, equiv_thm) ctxt = |
83 ProofContext.theory (quotdata_update_thy (qty, rty, rel, equiv_thm)) ctxt |
89 ProofContext.theory (quotdata_update_thy (qty, rty, rel, equiv_thm)) ctxt |
84 |
90 |
85 fun print_quotdata ctxt = |
91 fun print_quotinfo ctxt = |
86 let |
92 let |
87 fun prt_quot {qtyp, rtyp, rel, equiv_thm} = |
93 fun prt_quot {qtyp, rtyp, rel, equiv_thm} = |
88 Pretty.block (Library.separate (Pretty.brk 2) |
94 Pretty.block (Library.separate (Pretty.brk 2) |
89 [Pretty.str ("quotient type:"), |
95 [Pretty.str ("quotient type:"), |
90 Syntax.pretty_typ ctxt qtyp, |
96 Syntax.pretty_typ ctxt qtyp, |
119 fun lookup_qenv _ [] _ = NONE |
125 fun lookup_qenv _ [] _ = NONE |
120 | lookup_qenv eq ((qty, rty)::xs) qty' = |
126 | lookup_qenv eq ((qty, rty)::xs) qty' = |
121 if eq (qty', qty) then SOME (qty, rty) |
127 if eq (qty', qty) then SOME (qty, rty) |
122 else lookup_qenv eq xs qty' |
128 else lookup_qenv eq xs qty' |
123 |
129 |
|
130 (* information about quotient constants *) |
|
131 type qconsts_info = {qconst: term, rconst: term} |
|
132 |
|
133 structure QConstsData = Theory_Data |
|
134 (type T = qconsts_info Symtab.table |
|
135 val empty = Symtab.empty |
|
136 val extend = I |
|
137 val merge = Symtab.merge (K true)) |
|
138 |
|
139 val qconsts_lookup = Symtab.lookup o QConstsData.get |
|
140 |
|
141 fun qconsts_update_thy k qcinfo = QConstsData.map (Symtab.update (k, qcinfo)) |
|
142 fun qconsts_update k qcinfo = ProofContext.theory (qconsts_update_thy k qcinfo) |
|
143 |
|
144 fun print_qconstinfo ctxt = |
|
145 let |
|
146 fun prt_qconst {qconst, rconst} = |
|
147 Pretty.block (Library.separate (Pretty.brk 2) |
|
148 [Syntax.pretty_term ctxt qconst, |
|
149 Pretty.str (" := "), |
|
150 Syntax.pretty_term ctxt rconst]) |
|
151 in |
|
152 QConstsData.get (ProofContext.theory_of ctxt) |
|
153 |> Symtab.dest |
|
154 |> map (prt_qconst o snd) |
|
155 |> Pretty.big_list "quotient constants:" |
|
156 |> Pretty.writeln |
|
157 end |
|
158 |
|
159 val _ = |
|
160 OuterSyntax.improper_command "print_quotconsts" "print out all quotient constants" |
|
161 OuterKeyword.diag (Scan.succeed (Toplevel.keep (print_qconstinfo o Toplevel.context_of))) |
|
162 |
|
163 |
124 end; (* structure *) |
164 end; (* structure *) |
125 |
165 |
126 open Quotient_Info |
166 open Quotient_Info |