File ‹derive_manager.ML›
signature DERIVE_MANAGER =
sig
val register_derive : string -> string -> (string -> string -> theory -> theory) -> theory -> theory
val derive : string -> string -> string -> theory -> theory
val derive_cmd : string -> string -> string -> theory -> theory
val print_info : theory -> unit
end
structure Derive_Manager : DERIVE_MANAGER =
struct
structure Derive_Data = Theory_Data
(
type T =
(string * (string -> string -> theory -> theory)) Symtab.table
val empty = Symtab.empty
val merge = Symtab.merge (K true)
)
val derive_options =
Derive_Data.get #> Symtab.dest #> map (fn (id, (descr, _)) => (id, descr))
fun print_info thy =
let
val _ = writeln "The following sorts can be derived"
val _ = derive_options thy |> sort_by fst |> map (fn (id,descr) => writeln (id ^ ": " ^ descr))
in () end
fun register_derive id descr f thy =
if Symtab.defined (Derive_Data.get thy) id then
error ("Identifier " ^ quote id ^ " already in use for " ^ quote "deriving")
else
Derive_Data.map (Symtab.update_new (id, (descr, f))) thy
fun gen_derive prep id dtname param thy =
(case Symtab.lookup (Derive_Data.get thy) id of
NONE => error ("No handler to derive sort " ^ quote id ^
" is registered. Try " ^ quote "print_derives" ^ " to see available sorts.")
| SOME (_, f) => f (prep thy dtname) param thy)
val derive = gen_derive (K I)
fun derive_cmd id param dtname = gen_derive
(fn thy => fst o dest_Type o Syntax.parse_typ (Proof_Context.init_global thy)) id dtname param
val _ =
Outer_Syntax.command @{command_keyword print_derives} "lists all registered sorts which can be derived"
(Scan.succeed (Toplevel.theory (tap print_info)))
val _ =
Outer_Syntax.command @{command_keyword derive} "derives some sort"
(Parse.parname -- Parse.name -- Scan.repeat1 Parse.type_const >> (fn ((param, s), tycons) =>
Toplevel.theory (fold (derive_cmd s param) tycons)))
end