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 lazy -> theory -> theory"} \\

   @{index_ML Code_Preproc.map_pre: "(simpset -> simpset) -> theory -> theory"} \\

   @{index_ML Code_Preproc.map_post: "(simpset -> simpset) -> theory -> theory"} \\

   @{index_ML Code_Preproc.add_functrans: "string * (theory -> (thm * bool) list -> (thm * bool) list option)

     -> theory -> theory"} \\

   @{index_ML Code_Preproc.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 code equations @{text lthms} for constant

      @{text const} to executable content.

   \item @{ML Code_Preproc.map_pre}~@{text "f"}~@{text "thy"} changes

      the preprocessor simpset.

   \item @{ML Code_Preproc.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 code 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 code equations.

   \item @{ML Code_Preproc.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.read_const: "theory -> string -> string"} \\

   @{index_ML Code.rewrite_eqn: "simpset -> thm -> thm"} \\

   \end{mldecls}

   \begin{description}

   \item @{ML Code.read_const}~@{text thy}~@{text s}

      reads a constant as a concrete term expression @{text s}.

   \item @{ML Code.rewrite_eqn}~@{text ss}~@{text thm}

      rewrites a code equation @{text thm} with a simpset @{text ss};

      only arguments and right hand side are rewritten,

      not the head of the code 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> string 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