# HG changeset patch # User haftmann # Date 1275319766 -7200 # Node ID 1f1f9cbd23ae39520cbf9079a3edc0416c1510d4 # Parent c40c9b05952c0e276da2bb4a2486046ce79b86ec adjusted diff -r c40c9b05952c -r 1f1f9cbd23ae doc-src/Codegen/Thy/Further.thy --- a/doc-src/Codegen/Thy/Further.thy Mon May 31 10:29:04 2010 +0200 +++ b/doc-src/Codegen/Thy/Further.thy Mon May 31 17:29:26 2010 +0200 @@ -94,7 +94,7 @@ whole @{text SML} is read, the necessary code is generated transparently and the corresponding constant names are inserted. This technique also allows to use pattern matching on constructors stemming from compiled - @{text datatypes}. + @{text "datatypes"}. For a less simplistic example, theory @{theory Ferrack} is a good reference. diff -r c40c9b05952c -r 1f1f9cbd23ae doc-src/Codegen/Thy/ML.thy --- a/doc-src/Codegen/Thy/ML.thy Mon May 31 10:29:04 2010 +0200 +++ b/doc-src/Codegen/Thy/ML.thy Mon May 31 17:29:26 2010 +0200 @@ -30,9 +30,9 @@ -> 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 + @{index_ML Code.get_type: "theory -> string -> (string * sort) list * (string * typ list) list"} \\ - @{index_ML Code.get_datatype_of_constr: "theory -> string -> string option"} + @{index_ML Code.get_type_of_constr_or_abstr: "theory -> string -> (string * bool) option"} \end{mldecls} \begin{description} @@ -61,7 +61,7 @@ a datatype to executable content, with generation set @{text cs}. - \item @{ML Code.get_datatype_of_constr}~@{text "thy"}~@{text "const"} + \item @{ML Code.get_type_of_constr_or_abstr}~@{text "thy"}~@{text "const"} returns type constructor corresponding to constructor @{text const}; returns @{text NONE} if @{text const} is no constructor. @@ -105,7 +105,7 @@ 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 + data slot @{ML_functor Code_Data}; on instantiation of this functor, the following types and operations are required: @@ -131,7 +131,7 @@ \end{description} - \noindent An instance of @{ML_functor CodeDataFun} provides the following + \noindent An instance of @{ML_functor Code_Data} provides the following interface: \medskip