doc-src/Codegen/Thy/ML.thy
author haftmann
Tue Jul 14 10:54:21 2009 +0200 (2009-07-14)
changeset 31999 cb1f26c0de5b
parent 31156 90fed3d4430f
child 33707 68841fb382e0
permissions -rw-r--r--
updated to changes in sources; tuned
     1 theory "ML"
     2 imports Setup
     3 begin
     4 
     5 section {* ML system interfaces \label{sec:ml} *}
     6 
     7 text {*
     8   Since the code generator framework not only aims to provide
     9   a nice Isar interface but also to form a base for
    10   code-generation-based applications, here a short
    11   description of the most important ML interfaces.
    12 *}
    13 
    14 subsection {* Executable theory content: @{text Code} *}
    15 
    16 text {*
    17   This Pure module implements the core notions of
    18   executable content of a theory.
    19 *}
    20 
    21 subsubsection {* Managing executable content *}
    22 
    23 text %mlref {*
    24   \begin{mldecls}
    25   @{index_ML Code.add_eqn: "thm -> theory -> theory"} \\
    26   @{index_ML Code.del_eqn: "thm -> theory -> theory"} \\
    27   @{index_ML Code.add_eqnl: "string * (thm * bool) list lazy -> theory -> theory"} \\
    28   @{index_ML Code_Preproc.map_pre: "(simpset -> simpset) -> theory -> theory"} \\
    29   @{index_ML Code_Preproc.map_post: "(simpset -> simpset) -> theory -> theory"} \\
    30   @{index_ML Code_Preproc.add_functrans: "string * (theory -> (thm * bool) list -> (thm * bool) list option)
    31     -> theory -> theory"} \\
    32   @{index_ML Code_Preproc.del_functrans: "string -> theory -> theory"} \\
    33   @{index_ML Code.add_datatype: "(string * typ) list -> theory -> theory"} \\
    34   @{index_ML Code.get_datatype: "theory -> string
    35     -> (string * sort) list * (string * typ list) list"} \\
    36   @{index_ML Code.get_datatype_of_constr: "theory -> string -> string option"}
    37   \end{mldecls}
    38 
    39   \begin{description}
    40 
    41   \item @{ML Code.add_eqn}~@{text "thm"}~@{text "thy"} adds function
    42      theorem @{text "thm"} to executable content.
    43 
    44   \item @{ML Code.del_eqn}~@{text "thm"}~@{text "thy"} removes function
    45      theorem @{text "thm"} from executable content, if present.
    46 
    47   \item @{ML Code.add_eqnl}~@{text "(const, lthms)"}~@{text "thy"} adds
    48      suspended code equations @{text lthms} for constant
    49      @{text const} to executable content.
    50 
    51   \item @{ML Code_Preproc.map_pre}~@{text "f"}~@{text "thy"} changes
    52      the preprocessor simpset.
    53 
    54   \item @{ML Code_Preproc.add_functrans}~@{text "(name, f)"}~@{text "thy"} adds
    55      function transformer @{text f} (named @{text name}) to executable content;
    56      @{text f} is a transformer of the code equations belonging
    57      to a certain function definition, depending on the
    58      current theory context.  Returning @{text NONE} indicates that no
    59      transformation took place;  otherwise, the whole process will be iterated
    60      with the new code equations.
    61 
    62   \item @{ML Code_Preproc.del_functrans}~@{text "name"}~@{text "thy"} removes
    63      function transformer named @{text name} from executable content.
    64 
    65   \item @{ML Code.add_datatype}~@{text cs}~@{text thy} adds
    66      a datatype to executable content, with generation
    67      set @{text cs}.
    68 
    69   \item @{ML Code.get_datatype_of_constr}~@{text "thy"}~@{text "const"}
    70      returns type constructor corresponding to
    71      constructor @{text const}; returns @{text NONE}
    72      if @{text const} is no constructor.
    73 
    74   \end{description}
    75 *}
    76 
    77 subsection {* Auxiliary *}
    78 
    79 text %mlref {*
    80   \begin{mldecls}
    81   @{index_ML Code.read_const: "theory -> string -> string"}
    82   \end{mldecls}
    83 
    84   \begin{description}
    85 
    86   \item @{ML Code.read_const}~@{text thy}~@{text s}
    87      reads a constant as a concrete term expression @{text s}.
    88 
    89   \end{description}
    90 
    91 *}
    92 
    93 subsection {* Implementing code generator applications *}
    94 
    95 text {*
    96   Implementing code generator applications on top
    97   of the framework set out so far usually not only
    98   involves using those primitive interfaces
    99   but also storing code-dependent data and various
   100   other things.
   101 *}
   102 
   103 subsubsection {* Data depending on the theory's executable content *}
   104 
   105 text {*
   106   Due to incrementality of code generation, changes in the
   107   theory's executable content have to be propagated in a
   108   certain fashion.  Additionally, such changes may occur
   109   not only during theory extension but also during theory
   110   merge, which is a little bit nasty from an implementation
   111   point of view.  The framework provides a solution
   112   to this technical challenge by providing a functorial
   113   data slot @{ML_functor CodeDataFun}; on instantiation
   114   of this functor, the following types and operations
   115   are required:
   116 
   117   \medskip
   118   \begin{tabular}{l}
   119   @{text "type T"} \\
   120   @{text "val empty: T"} \\
   121   @{text "val purge: theory \<rightarrow> string list option \<rightarrow> T \<rightarrow> T"}
   122   \end{tabular}
   123 
   124   \begin{description}
   125 
   126   \item @{text T} the type of data to store.
   127 
   128   \item @{text empty} initial (empty) data.
   129 
   130   \item @{text purge}~@{text thy}~@{text consts} propagates changes in executable content;
   131     @{text consts} indicates the kind
   132     of change: @{ML NONE} stands for a fundamental change
   133     which invalidates any existing code, @{text "SOME consts"}
   134     hints that executable content for constants @{text consts}
   135     has changed.
   136 
   137   \end{description}
   138 
   139   \noindent An instance of @{ML_functor CodeDataFun} provides the following
   140   interface:
   141 
   142   \medskip
   143   \begin{tabular}{l}
   144   @{text "get: theory \<rightarrow> T"} \\
   145   @{text "change: theory \<rightarrow> (T \<rightarrow> T) \<rightarrow> T"} \\
   146   @{text "change_yield: theory \<rightarrow> (T \<rightarrow> 'a * T) \<rightarrow> 'a * T"}
   147   \end{tabular}
   148 
   149   \begin{description}
   150 
   151   \item @{text get} retrieval of the current data.
   152 
   153   \item @{text change} update of current data (cached!)
   154     by giving a continuation.
   155 
   156   \item @{text change_yield} update with side result.
   157 
   158   \end{description}
   159 *}
   160 
   161 text {*
   162   \bigskip
   163 
   164   \emph{Happy proving, happy hacking!}
   165 *}
   166 
   167 end