54 fun merge data = Symtab.merge (K true) data |
54 fun merge data = Symtab.merge (K true) data |
55 ) |
55 ) |
56 |
56 |
57 val lookup_quotmaps = Symtab.lookup o Quotmaps.get o Context.Proof |
57 val lookup_quotmaps = Symtab.lookup o Quotmaps.get o Context.Proof |
58 |
58 |
59 fun quotmaps_attribute (ctxt, (tystr, (mapstr, relstr))) = |
59 (* FIXME export proper internal update operation!? *) |
60 let |
60 |
61 val thy = Proof_Context.theory_of ctxt (* FIXME proper local context *) |
61 val quotmaps_attribute_setup = |
62 val tyname = Sign.intern_type thy tystr (* FIXME pass proper internal names via syntax *) |
62 Attrib.setup @{binding map} |
63 val mapname = Sign.intern_const thy mapstr |
63 ((Args.type_name false --| Scan.lift (Parse.$$$ "=")) -- (* FIXME Args.type_name true (requires "set" type) *) |
64 val relname = Sign.intern_const thy relstr |
64 (Scan.lift (Parse.$$$ "(") |-- Args.const_proper true --| Scan.lift (Parse.$$$ ",") -- |
65 |
65 Args.const_proper true --| Scan.lift (Parse.$$$ ")")) >> |
66 fun sanity_check s = (Const (s, dummyT) |> Syntax.check_term ctxt; ()) |
66 (fn (tyname, (mapname, relname)) => |
67 val _ = List.app sanity_check [mapname, relname] |
67 let val minfo = {mapfun = mapname, relmap = relname} |
68 val minfo = {mapfun = mapname, relmap = relname} |
68 in Thm.declaration_attribute (fn _ => Quotmaps.map (Symtab.update (tyname, minfo))) end)) |
69 in |
69 "declaration of map information" |
70 Thm.declaration_attribute (fn _ => Quotmaps.map (Symtab.update (tyname, minfo))) |
|
71 end |
|
72 |
|
73 val quotmaps_attr_parser = |
|
74 Args.context -- Scan.lift |
|
75 ((Args.name --| Parse.$$$ "=") -- |
|
76 (Parse.$$$ "(" |-- Args.name --| Parse.$$$ "," -- |
|
77 Args.name --| Parse.$$$ ")")) |
|
78 |
70 |
79 fun print_quotmaps ctxt = |
71 fun print_quotmaps ctxt = |
80 let |
72 let |
81 fun prt_map (ty_name, {mapfun, relmap}) = |
73 fun prt_map (ty_name, {mapfun, relmap}) = |
82 Pretty.block (separate (Pretty.brk 2) |
74 Pretty.block (separate (Pretty.brk 2) |