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 ‹❙d❙e❙r❙i❙v❙e (param) sort datatype› calls the hook for deriving ‹sort› (that
  may depend on the optional ‹param›) on ‹datatype› (if such a hook is registered).

  E.g., ‹❙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 ‹❙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