Theory Derive_Manager

(*  Title:       Deriving class instances for datatypes
    Author:      Christian Sternagel and René Thiemann  <christian.sternagel|rene.thiemann@uibk.ac.at>
    Maintainer:  Christian Sternagel and René Thiemann 
    License:     LGPL
*)
section ‹Derive Manager›

theory Derive_Manager
imports Main
keywords "print_derives" :: diag and "derive" :: thy_decl
begin

text ‹
  The derive manager allows the user to register various derive-hooks, e.g., for orders,
  pretty-printers, hash-functions, etc. All registered hooks are accessible via the derive command.

  @{rail ‹
    @'derive' ('(' param ')')? sort (datatype+)
  ›}

  \begin{description}
  \item @{text "❙d❙e❙r❙i❙v❙e (param) sort datatype"} calls the hook for deriving @{text sort} (that
  may depend on the optional @{text param}) on @{text datatype} (if such a hook is registered).

  E.g., @{text "❙d❙e❙r❙i❙v❙e compare_order list"} will derive a comparator for datatype @{type list}
  which is also used to define a linear order on @{type list}s.
  \end{description}

  There is also the diagnostic command @{text "❙p❙r❙i❙n❙t❙_❙d❙e❙r❙i❙v❙e❙s"} that shows the list of currently
  registered hooks.
›

ML_file "derive_manager.ML"

end