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, relmap: string} |
5 type maps_info = {mapfun: string, relmap: string} |
6 val maps_exists: theory -> string -> bool |
6 val maps_defined: theory -> string -> bool |
7 val maps_lookup: theory -> string -> maps_info (* raises NotFound *) |
7 val maps_lookup: theory -> string -> maps_info (* raises NotFound *) |
8 val maps_update_thy: string -> maps_info -> theory -> theory |
8 val maps_update_thy: string -> maps_info -> theory -> theory |
9 val maps_update: string -> maps_info -> Proof.context -> Proof.context |
9 val maps_update: string -> maps_info -> Proof.context -> Proof.context |
10 val print_mapsinfo: Proof.context -> unit |
10 val print_mapsinfo: Proof.context -> unit |
11 |
11 |
75 (type T = maps_info Symtab.table |
75 (type T = maps_info Symtab.table |
76 val empty = Symtab.empty |
76 val empty = Symtab.empty |
77 val extend = I |
77 val extend = I |
78 val merge = Symtab.merge (K true)) |
78 val merge = Symtab.merge (K true)) |
79 |
79 |
80 fun maps_exists thy s = |
80 fun maps_defined thy s = |
81 case (Symtab.lookup (MapsData.get thy) s) of |
81 Symtab.defined (MapsData.get thy) s |
82 SOME _ => true |
|
83 | NONE => false |
|
84 |
82 |
85 fun maps_lookup thy s = |
83 fun maps_lookup thy s = |
86 case (Symtab.lookup (MapsData.get thy) s) of |
84 case (Symtab.lookup (MapsData.get thy) s) of |
87 SOME map_fun => map_fun |
85 SOME map_fun => map_fun |
88 | NONE => raise NotFound |
86 | NONE => raise NotFound |
99 val thy = ProofContext.theory_of ctxt |
97 val thy = ProofContext.theory_of ctxt |
100 val tyname = Sign.intern_type thy tystr |
98 val tyname = Sign.intern_type thy tystr |
101 val mapname = Sign.intern_const thy mapstr |
99 val mapname = Sign.intern_const thy mapstr |
102 val relname = Sign.intern_const thy relstr |
100 val relname = Sign.intern_const thy relstr |
103 |
101 |
104 fun sanity_check s = (Const (s, dummyT) |> Syntax.check_term ctxt) |
102 fun sanity_check s = (Const (s, dummyT) |> Syntax.check_term ctxt; ()) |
105 val _ = map sanity_check [mapname, relname] |
103 val _ = List.app sanity_check [mapname, relname] |
106 in |
104 in |
107 maps_attribute_aux tyname {mapfun = mapname, relmap = relname} |
105 maps_attribute_aux tyname {mapfun = mapname, relmap = relname} |
108 end |
106 end |
109 |
107 |
110 val maps_attr_parser = |
108 val maps_attr_parser = |