equal
deleted
inserted
replaced
10 val print_mapsinfo: Proof.context -> unit |
10 val print_mapsinfo: Proof.context -> unit |
11 |
11 |
12 type quotdata_info = {qtyp: typ, rtyp: typ, equiv_rel: term, equiv_thm: thm} |
12 type quotdata_info = {qtyp: typ, rtyp: typ, equiv_rel: term, equiv_thm: thm} |
13 val transform_quotdata: morphism -> quotdata_info -> quotdata_info |
13 val transform_quotdata: morphism -> quotdata_info -> quotdata_info |
14 val quotdata_lookup: theory -> string -> quotdata_info (* raises NotFound *) |
14 val quotdata_lookup: theory -> string -> quotdata_info (* raises NotFound *) |
|
15 val quotdata_lookup_type: theory -> typ -> quotdata_info (* raises NotFound *) |
15 val quotdata_update_thy: string -> quotdata_info -> theory -> theory |
16 val quotdata_update_thy: string -> quotdata_info -> theory -> theory |
16 val quotdata_update_gen: string -> quotdata_info -> Context.generic -> Context.generic |
17 val quotdata_update_gen: string -> quotdata_info -> Context.generic -> Context.generic |
17 val print_quotinfo: Proof.context -> unit |
18 val print_quotinfo: Proof.context -> unit |
18 |
19 |
19 type qconsts_info = {qconst: term, rconst: term, def: thm} |
20 type qconsts_info = {qconst: term, rconst: term, def: thm} |
156 | NONE => raise NotFound |
157 | NONE => raise NotFound |
157 |
158 |
158 fun quotdata_update_thy str qinfo = QuotData.map (Symtab.update (str, qinfo)) |
159 fun quotdata_update_thy str qinfo = QuotData.map (Symtab.update (str, qinfo)) |
159 fun quotdata_update_gen str qinfo = Context.mapping (quotdata_update_thy str qinfo) I |
160 fun quotdata_update_gen str qinfo = Context.mapping (quotdata_update_thy str qinfo) I |
160 |
161 |
161 fun quotdata_dest thy = |
162 fun quotdata_lookup_type thy qty = |
162 map snd (Symtab.dest (QuotData.get thy)) |
163 let |
|
164 val smt = Symtab.dest (QuotData.get thy); |
|
165 fun matches (_, x) = Sign.typ_instance thy (qty, (#qtyp x)) |
|
166 in |
|
167 case (find_first matches smt) of |
|
168 SOME (_, x) => x |
|
169 | _ => raise NotFound |
|
170 end |
163 |
171 |
164 fun print_quotinfo ctxt = |
172 fun print_quotinfo ctxt = |
165 let |
173 let |
166 fun prt_quot {qtyp, rtyp, equiv_rel, equiv_thm} = |
174 fun prt_quot {qtyp, rtyp, equiv_rel, equiv_thm} = |
167 Pretty.block (Library.separate (Pretty.brk 2) |
175 Pretty.block (Library.separate (Pretty.brk 2) |