doc-src/IsarAdvanced/Codegen/Thy/ML.thy

fixed

theory "ML"
imports Setup
begin

section {* ML system interfaces \label{sec:ml} *}

text {*
  Since the code generator framework not only aims to provide
  a nice Isar interface but also to form a base for
  code-generation-based applications, here a short
  description of the most important ML interfaces.
*}

subsection {* Executable theory content: @{text Code} *}

text {*
  This Pure module implements the core notions of
  executable content of a theory.
*}

subsubsection {* Managing executable content *}

text %mlref {*
  \begin{mldecls}
  @{index_ML Code.add_eqn: "thm -> theory -> theory"} \\
  @{index_ML Code.del_eqn: "thm -> theory -> theory"} \\
  @{index_ML Code.add_eqnl: "string * (thm * bool) list Susp.T -> theory -> theory"} \\
  @{index_ML Code.map_pre: "(MetaSimplifier.simpset -> MetaSimplifier.simpset) -> theory -> theory"} \\
  @{index_ML Code.map_post: "(MetaSimplifier.simpset -> MetaSimplifier.simpset) -> theory -> theory"} \\
  @{index_ML Code.add_functrans: "string * (theory -> (thm * bool) list -> (thm * bool) list option)
    -> theory -> theory"} \\
  @{index_ML Code.del_functrans: "string -> theory -> theory"} \\
  @{index_ML Code.add_datatype: "(string * typ) list -> theory -> theory"} \\
  @{index_ML Code.get_datatype: "theory -> string
    -> (string * sort) list * (string * typ list) list"} \\
  @{index_ML Code.get_datatype_of_constr: "theory -> string -> string option"}
  \end{mldecls}

  \begin{description}

  \item @{ML Code.add_eqn}~@{text "thm"}~@{text "thy"} adds function
     theorem @{text "thm"} to executable content.

  \item @{ML Code.del_eqn}~@{text "thm"}~@{text "thy"} removes function
     theorem @{text "thm"} from executable content, if present.

  \item @{ML Code.add_eqnl}~@{text "(const, lthms)"}~@{text "thy"} adds
     suspended defining equations @{text lthms} for constant
     @{text const} to executable content.

  \item @{ML Code.map_pre}~@{text "f"}~@{text "thy"} changes
     the preprocessor simpset.

  \item @{ML Code.add_functrans}~@{text "(name, f)"}~@{text "thy"} adds
     function transformer @{text f} (named @{text name}) to executable content;
     @{text f} is a transformer of the defining equations belonging
     to a certain function definition, depending on the
     current theory context.  Returning @{text NONE} indicates that no
     transformation took place;  otherwise, the whole process will be iterated
     with the new defining equations.

  \item @{ML Code.del_functrans}~@{text "name"}~@{text "thy"} removes
     function transformer named @{text name} from executable content.

  \item @{ML Code.add_datatype}~@{text cs}~@{text thy} adds
     a datatype to executable content, with generation
     set @{text cs}.

  \item @{ML Code.get_datatype_of_constr}~@{text "thy"}~@{text "const"}
     returns type constructor corresponding to
     constructor @{text const}; returns @{text NONE}
     if @{text const} is no constructor.

  \end{description}
*}

subsection {* Auxiliary *}

text %mlref {*
  \begin{mldecls}
  @{index_ML Code_Unit.read_const: "theory -> string -> string"} \\
  @{index_ML Code_Unit.head_eqn: "theory -> thm -> string * ((string * sort) list * typ)"} \\
  @{index_ML Code_Unit.rewrite_eqn: "MetaSimplifier.simpset -> thm -> thm"} \\
  \end{mldecls}

  \begin{description}

  \item @{ML Code_Unit.read_const}~@{text thy}~@{text s}
     reads a constant as a concrete term expression @{text s}.

  \item @{ML Code_Unit.head_eqn}~@{text thy}~@{text thm}
     extracts the constant and its type from a defining equation @{text thm}.

  \item @{ML Code_Unit.rewrite_eqn}~@{text ss}~@{text thm}
     rewrites a defining equation @{text thm} with a simpset @{text ss};
     only arguments and right hand side are rewritten,
     not the head of the defining equation.

  \end{description}

*}

subsection {* Implementing code generator applications *}

text {*
  Implementing code generator applications on top
  of the framework set out so far usually not only
  involves using those primitive interfaces
  but also storing code-dependent data and various
  other things.
*}

subsubsection {* Data depending on the theory's executable content *}

text {*
  Due to incrementality of code generation, changes in the
  theory's executable content have to be propagated in a
  certain fashion.  Additionally, such changes may occur
  not only during theory extension but also during theory
  merge, which is a little bit nasty from an implementation
  point of view.  The framework provides a solution
  to this technical challenge by providing a functorial
  data slot @{ML_functor CodeDataFun}; on instantiation
  of this functor, the following types and operations
  are required:

  \medskip
  \begin{tabular}{l}
  @{text "type T"} \\
  @{text "val empty: T"} \\
  @{text "val purge: theory \<rightarrow> CodeUnit.const list option \<rightarrow> T \<rightarrow> T"}
  \end{tabular}

  \begin{description}

  \item @{text T} the type of data to store.

  \item @{text empty} initial (empty) data.

  \item @{text purge}~@{text thy}~@{text consts} propagates changes in executable content;
    @{text consts} indicates the kind
    of change: @{ML NONE} stands for a fundamental change
    which invalidates any existing code, @{text "SOME consts"}
    hints that executable content for constants @{text consts}
    has changed.

  \end{description}

  \noindent An instance of @{ML_functor CodeDataFun} provides the following
  interface:

  \medskip
  \begin{tabular}{l}
  @{text "get: theory \<rightarrow> T"} \\
  @{text "change: theory \<rightarrow> (T \<rightarrow> T) \<rightarrow> T"} \\
  @{text "change_yield: theory \<rightarrow> (T \<rightarrow> 'a * T) \<rightarrow> 'a * T"}
  \end{tabular}

  \begin{description}

  \item @{text get} retrieval of the current data.

  \item @{text change} update of current data (cached!)
    by giving a continuation.

  \item @{text change_yield} update with side result.

  \end{description}
*}

text {*
  \bigskip

  \emph{Happy proving, happy hacking!}
*}

end