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 *) |
|
16 val quotdata_update_thy: string -> quotdata_info -> theory -> theory |
15 val quotdata_update_thy: string -> quotdata_info -> theory -> theory |
17 val quotdata_update_gen: string -> quotdata_info -> Context.generic -> Context.generic |
16 val quotdata_update_gen: string -> quotdata_info -> Context.generic -> Context.generic |
18 val print_quotinfo: Proof.context -> unit |
17 val print_quotinfo: Proof.context -> unit |
19 |
18 |
20 type qconsts_info = {qconst: term, rconst: term, def: thm} |
19 type qconsts_info = {qconst: term, rconst: term, def: thm} |
156 SOME qinfo => qinfo |
155 SOME qinfo => qinfo |
157 | NONE => raise NotFound |
156 | NONE => raise NotFound |
158 |
157 |
159 fun quotdata_update_thy str qinfo = QuotData.map (Symtab.update (str, qinfo)) |
158 fun quotdata_update_thy str qinfo = QuotData.map (Symtab.update (str, qinfo)) |
160 fun quotdata_update_gen str qinfo = Context.mapping (quotdata_update_thy str qinfo) I |
159 fun quotdata_update_gen str qinfo = Context.mapping (quotdata_update_thy str qinfo) I |
161 |
|
162 fun quotdata_lookup_type thy qty = |
|
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 |
|
171 |
160 |
172 fun print_quotinfo ctxt = |
161 fun print_quotinfo ctxt = |
173 let |
162 let |
174 fun prt_quot {qtyp, rtyp, equiv_rel, equiv_thm} = |
163 fun prt_quot {qtyp, rtyp, equiv_rel, equiv_thm} = |
175 Pretty.block (Library.separate (Pretty.brk 2) |
164 Pretty.block (Library.separate (Pretty.brk 2) |