equal
deleted
inserted
replaced
1 signature QUOTIENT_INFO = |
1 signature QUOTIENT_INFO = |
2 sig |
2 sig |
3 exception NotFound |
3 exception NotFound |
4 |
4 |
5 type maps_info = {mapfun: string, relfun: string} |
5 type maps_info = {mapfun: string, relfun: string} |
6 val maps_lookup: theory -> string -> maps_info option |
6 val maps_lookup: theory -> string -> maps_info (* raises NotFound *) |
7 val maps_update_thy: string -> maps_info -> theory -> theory |
7 val maps_update_thy: string -> maps_info -> theory -> theory |
8 val maps_update: string -> maps_info -> Proof.context -> Proof.context |
8 val maps_update: string -> maps_info -> Proof.context -> Proof.context |
9 val print_mapsinfo: Proof.context -> unit |
9 val print_mapsinfo: Proof.context -> unit |
10 |
10 |
11 type quotient_info = {qtyp: typ, rtyp: typ, rel: term, equiv_thm: thm} |
11 type quotient_info = {qtyp: typ, rtyp: typ, rel: term, equiv_thm: thm} |
16 val quotdata_dest: theory -> quotient_info list |
16 val quotdata_dest: theory -> quotient_info list |
17 val print_quotinfo: Proof.context -> unit |
17 val print_quotinfo: Proof.context -> unit |
18 |
18 |
19 type qconsts_info = {qconst: term, rconst: term, def: thm} |
19 type qconsts_info = {qconst: term, rconst: term, def: thm} |
20 val qconsts_transfer: morphism -> qconsts_info -> qconsts_info |
20 val qconsts_transfer: morphism -> qconsts_info -> qconsts_info |
21 val qconsts_lookup: theory -> term -> qconsts_info |
21 val qconsts_lookup: theory -> term -> qconsts_info (* raises NotFound *) |
22 val qconsts_update_thy: string -> qconsts_info -> theory -> theory |
22 val qconsts_update_thy: string -> qconsts_info -> theory -> theory |
23 val qconsts_update_gen: string -> qconsts_info -> Context.generic -> Context.generic |
23 val qconsts_update_gen: string -> qconsts_info -> Context.generic -> Context.generic |
24 val qconsts_dest: theory -> qconsts_info list |
24 val qconsts_dest: theory -> qconsts_info list |
25 val print_qconstinfo: Proof.context -> unit |
25 val print_qconstinfo: Proof.context -> unit |
26 |
26 |
48 (type T = maps_info Symtab.table |
48 (type T = maps_info Symtab.table |
49 val empty = Symtab.empty |
49 val empty = Symtab.empty |
50 val extend = I |
50 val extend = I |
51 val merge = Symtab.merge (K true)) |
51 val merge = Symtab.merge (K true)) |
52 |
52 |
53 val maps_lookup = Symtab.lookup o MapsData.get |
53 fun maps_lookup thy s = |
|
54 case (Symtab.lookup (MapsData.get thy) s) of |
|
55 SOME map_fun => map_fun |
|
56 | NONE => raise NotFound |
54 |
57 |
55 fun maps_update_thy k minfo = MapsData.map (Symtab.update (k, minfo)) |
58 fun maps_update_thy k minfo = MapsData.map (Symtab.update (k, minfo)) |
56 fun maps_update k minfo = ProofContext.theory (maps_update_thy k minfo) |
59 fun maps_update k minfo = ProofContext.theory (maps_update_thy k minfo) |
57 |
60 |
58 fun maps_attribute_aux s minfo = Thm.declaration_attribute |
61 fun maps_attribute_aux s minfo = Thm.declaration_attribute |
186 case (find_first matches smt) of |
189 case (find_first matches smt) of |
187 SOME (_, x) => x |
190 SOME (_, x) => x |
188 | _ => raise NotFound |
191 | _ => raise NotFound |
189 end |
192 end |
190 |
193 |
191 (* We omit printing the definition *) |
|
192 fun print_qconstinfo ctxt = |
194 fun print_qconstinfo ctxt = |
193 let |
195 let |
194 fun prt_qconst {qconst, rconst, def} = |
196 fun prt_qconst {qconst, rconst, def} = |
195 Pretty.block (separate (Pretty.brk 1) |
197 Pretty.block (separate (Pretty.brk 1) |
196 [Syntax.pretty_term ctxt qconst, |
198 [Syntax.pretty_term ctxt qconst, |
197 Pretty.str ":=", |
199 Pretty.str ":=", |
198 Syntax.pretty_term ctxt rconst]) |
200 Syntax.pretty_term ctxt rconst, |
|
201 Pretty.str "as", |
|
202 Syntax.pretty_term ctxt (prop_of def)]) |
199 in |
203 in |
200 QConstsData.get (ProofContext.theory_of ctxt) |
204 QConstsData.get (ProofContext.theory_of ctxt) |
201 |> Symtab.dest |
205 |> Symtab.dest |
202 |> map (prt_qconst o snd) |
206 |> map (prt_qconst o snd) |
203 |> Pretty.big_list "quotient constants:" |
207 |> Pretty.big_list "quotient constants:" |