--- a/doc-src/Codegen/Thy/ML.thy Mon Nov 16 10:03:58 2009 +0100
+++ b/doc-src/Codegen/Thy/ML.thy Mon Nov 16 11:03:14 2009 +0100
@@ -24,7 +24,6 @@
\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)
@@ -44,10 +43,6 @@
\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.
--- a/doc-src/Codegen/Thy/Program.thy Mon Nov 16 10:03:58 2009 +0100
+++ b/doc-src/Codegen/Thy/Program.thy Mon Nov 16 11:03:14 2009 +0100
@@ -356,47 +356,8 @@
For datatypes, instances of @{class eq} are implicitly derived
when possible. For other types, you may instantiate @{text eq}
manually like any other type class.
-
- Though this @{text eq} class is designed to get rarely in
- the way, in some cases the automatically derived code equations
- for equality on a particular type may not be appropriate.
- As example, watch the following datatype representing
- monomorphic parametric types (where type constructors
- are referred to by natural numbers):
*}
-datatype %quote monotype = Mono nat "monotype list"
-(*<*)
-lemma monotype_eq:
- "eq_class.eq (Mono tyco1 typargs1) (Mono tyco2 typargs2) \<equiv>
- eq_class.eq tyco1 tyco2 \<and> eq_class.eq typargs1 typargs2" by (simp add: eq)
-(*>*)
-
-text {*
- \noindent Then code generation for SML would fail with a message
- that the generated code contains illegal mutual dependencies:
- the theorem @{thm monotype_eq [no_vars]} already requires the
- instance @{text "monotype \<Colon> eq"}, which itself requires
- @{thm monotype_eq [no_vars]}; Haskell has no problem with mutually
- recursive @{text instance} and @{text function} definitions,
- but the SML serialiser does not support this.
-
- In such cases, you have to provide your own equality equations
- involving auxiliary constants. In our case,
- @{const [show_types] list_all2} can do the job:
-*}
-
-lemma %quote monotype_eq_list_all2 [code]:
- "eq_class.eq (Mono tyco1 typargs1) (Mono tyco2 typargs2) \<longleftrightarrow>
- eq_class.eq tyco1 tyco2 \<and> list_all2 eq_class.eq typargs1 typargs2"
- by (simp add: eq list_all2_eq [symmetric])
-
-text {*
- \noindent does not depend on instance @{text "monotype \<Colon> eq"}:
-*}
-
-text %quote {*@{code_stmts "eq_class.eq :: monotype \<Rightarrow> monotype \<Rightarrow> bool" (SML)}*}
-
subsection {* Explicit partiality *}
--- a/doc-src/Codegen/Thy/document/Adaptation.tex Mon Nov 16 10:03:58 2009 +0100
+++ b/doc-src/Codegen/Thy/document/Adaptation.tex Mon Nov 16 11:03:14 2009 +0100
@@ -236,10 +236,10 @@
\hspace*{0pt}\\
\hspace*{0pt}datatype boola = True | False;\\
\hspace*{0pt}\\
-\hspace*{0pt}fun anda x True = x\\
-\hspace*{0pt} ~| anda x False = False\\
-\hspace*{0pt} ~| anda True x = x\\
-\hspace*{0pt} ~| anda False x = False;\\
+\hspace*{0pt}fun anda p True = p\\
+\hspace*{0pt} ~| anda p False = False\\
+\hspace*{0pt} ~| anda True p = p\\
+\hspace*{0pt} ~| anda False p = False;\\
\hspace*{0pt}\\
\hspace*{0pt}fun less{\char95}nat m (Suc n) = less{\char95}eq{\char95}nat m n\\
\hspace*{0pt} ~| less{\char95}nat n Zero{\char95}nat = False\\
--- a/doc-src/Codegen/Thy/document/Introduction.tex Mon Nov 16 10:03:58 2009 +0100
+++ b/doc-src/Codegen/Thy/document/Introduction.tex Mon Nov 16 11:03:14 2009 +0100
@@ -160,7 +160,7 @@
\hspace*{0pt}\\
\hspace*{0pt}datatype 'a queue = AQueue of 'a list * 'a list;\\
\hspace*{0pt}\\
-\hspace*{0pt}val empty :~'a queue = AQueue ([],~[])\\
+\hspace*{0pt}val empty :~'a queue = AQueue ([],~[]);\\
\hspace*{0pt}\\
\hspace*{0pt}fun dequeue (AQueue ([],~[])) = (NONE,~AQueue ([],~[]))\\
\hspace*{0pt} ~| dequeue (AQueue (xs,~y ::~ys)) = (SOME y,~AQueue (xs,~ys))\\
--- a/doc-src/Codegen/Thy/document/ML.tex Mon Nov 16 10:03:58 2009 +0100
+++ b/doc-src/Codegen/Thy/document/ML.tex Mon Nov 16 11:03:14 2009 +0100
@@ -54,7 +54,6 @@
\begin{mldecls}
\indexdef{}{ML}{Code.add\_eqn}\verb|Code.add_eqn: thm -> theory -> theory| \\
\indexdef{}{ML}{Code.del\_eqn}\verb|Code.del_eqn: thm -> theory -> theory| \\
- \indexdef{}{ML}{Code.add\_eqnl}\verb|Code.add_eqnl: string * (thm * bool) list lazy -> theory -> theory| \\
\indexdef{}{ML}{Code\_Preproc.map\_pre}\verb|Code_Preproc.map_pre: (simpset -> simpset) -> theory -> theory| \\
\indexdef{}{ML}{Code\_Preproc.map\_post}\verb|Code_Preproc.map_post: (simpset -> simpset) -> theory -> theory| \\
\indexdef{}{ML}{Code\_Preproc.add\_functrans}\verb|Code_Preproc.add_functrans: string * (theory -> (thm * bool) list -> (thm * bool) list option)|\isasep\isanewline%
@@ -74,10 +73,6 @@
\item \verb|Code.del_eqn|~\isa{thm}~\isa{thy} removes function
theorem \isa{thm} from executable content, if present.
- \item \verb|Code.add_eqnl|~\isa{{\isacharparenleft}const{\isacharcomma}\ lthms{\isacharparenright}}~\isa{thy} adds
- suspended code equations \isa{lthms} for constant
- \isa{const} to executable content.
-
\item \verb|Code_Preproc.map_pre|~\isa{f}~\isa{thy} changes
the preprocessor simpset.
--- a/doc-src/Codegen/Thy/document/Program.tex Mon Nov 16 10:03:58 2009 +0100
+++ b/doc-src/Codegen/Thy/document/Program.tex Mon Nov 16 11:03:14 2009 +0100
@@ -356,7 +356,7 @@
\hspace*{0pt}fun plus{\char95}nat (Suc m) n = plus{\char95}nat m (Suc n)\\
\hspace*{0pt} ~| plus{\char95}nat Zero{\char95}nat n = n;\\
\hspace*{0pt}\\
-\hspace*{0pt}val neutral{\char95}nat :~nat = Suc Zero{\char95}nat\\
+\hspace*{0pt}val neutral{\char95}nat :~nat = Suc Zero{\char95}nat;\\
\hspace*{0pt}\\
\hspace*{0pt}fun mult{\char95}nat Zero{\char95}nat n = Zero{\char95}nat\\
\hspace*{0pt} ~| mult{\char95}nat (Suc m) n = plus{\char95}nat n (mult{\char95}nat m n);\\
@@ -667,7 +667,7 @@
\hspace*{0pt}\\
\hspace*{0pt}datatype 'a queue = AQueue of 'a list * 'a list;\\
\hspace*{0pt}\\
-\hspace*{0pt}val empty :~'a queue = AQueue ([],~[])\\
+\hspace*{0pt}val empty :~'a queue = AQueue ([],~[]);\\
\hspace*{0pt}\\
\hspace*{0pt}fun dequeue (AQueue (xs,~y ::~ys)) = (SOME y,~AQueue (xs,~ys))\\
\hspace*{0pt} ~| dequeue (AQueue (xs,~[])) =\\
@@ -797,124 +797,10 @@
\isa{eq} constraints through all dependent code equations.
For datatypes, instances of \isa{eq} are implicitly derived
when possible. For other types, you may instantiate \isa{eq}
- manually like any other type class.
-
- Though this \isa{eq} class is designed to get rarely in
- the way, in some cases the automatically derived code equations
- for equality on a particular type may not be appropriate.
- As example, watch the following datatype representing
- monomorphic parametric types (where type constructors
- are referred to by natural numbers):%
-\end{isamarkuptext}%
-\isamarkuptrue%
-%
-\isadelimquote
-%
-\endisadelimquote
-%
-\isatagquote
-\isacommand{datatype}\isamarkupfalse%
-\ monotype\ {\isacharequal}\ Mono\ nat\ {\isachardoublequoteopen}monotype\ list{\isachardoublequoteclose}%
-\endisatagquote
-{\isafoldquote}%
-%
-\isadelimquote
-%
-\endisadelimquote
-%
-\isadelimproof
-%
-\endisadelimproof
-%
-\isatagproof
-%
-\endisatagproof
-{\isafoldproof}%
-%
-\isadelimproof
-%
-\endisadelimproof
-%
-\begin{isamarkuptext}%
-\noindent Then code generation for SML would fail with a message
- that the generated code contains illegal mutual dependencies:
- the theorem \isa{eq{\isacharunderscore}class{\isachardot}eq\ {\isacharparenleft}Mono\ tyco{\isadigit{1}}\ typargs{\isadigit{1}}{\isacharparenright}\ {\isacharparenleft}Mono\ tyco{\isadigit{2}}\ typargs{\isadigit{2}}{\isacharparenright}\ {\isasymequiv}\ eq{\isacharunderscore}class{\isachardot}eq\ tyco{\isadigit{1}}\ tyco{\isadigit{2}}\ {\isasymand}\ eq{\isacharunderscore}class{\isachardot}eq\ typargs{\isadigit{1}}\ typargs{\isadigit{2}}} already requires the
- instance \isa{monotype\ {\isasymColon}\ eq}, which itself requires
- \isa{eq{\isacharunderscore}class{\isachardot}eq\ {\isacharparenleft}Mono\ tyco{\isadigit{1}}\ typargs{\isadigit{1}}{\isacharparenright}\ {\isacharparenleft}Mono\ tyco{\isadigit{2}}\ typargs{\isadigit{2}}{\isacharparenright}\ {\isasymequiv}\ eq{\isacharunderscore}class{\isachardot}eq\ tyco{\isadigit{1}}\ tyco{\isadigit{2}}\ {\isasymand}\ eq{\isacharunderscore}class{\isachardot}eq\ typargs{\isadigit{1}}\ typargs{\isadigit{2}}}; Haskell has no problem with mutually
- recursive \isa{instance} and \isa{function} definitions,
- but the SML serialiser does not support this.
-
- In such cases, you have to provide your own equality equations
- involving auxiliary constants. In our case,
- \isa{list{\isacharunderscore}all{\isadigit{2}}} can do the job:%
+ manually like any other type class.%
\end{isamarkuptext}%
\isamarkuptrue%
%
-\isadelimquote
-%
-\endisadelimquote
-%
-\isatagquote
-\isacommand{lemma}\isamarkupfalse%
-\ monotype{\isacharunderscore}eq{\isacharunderscore}list{\isacharunderscore}all{\isadigit{2}}\ {\isacharbrackleft}code{\isacharbrackright}{\isacharcolon}\isanewline
-\ \ {\isachardoublequoteopen}eq{\isacharunderscore}class{\isachardot}eq\ {\isacharparenleft}Mono\ tyco{\isadigit{1}}\ typargs{\isadigit{1}}{\isacharparenright}\ {\isacharparenleft}Mono\ tyco{\isadigit{2}}\ typargs{\isadigit{2}}{\isacharparenright}\ {\isasymlongleftrightarrow}\isanewline
-\ \ \ \ \ eq{\isacharunderscore}class{\isachardot}eq\ tyco{\isadigit{1}}\ tyco{\isadigit{2}}\ {\isasymand}\ list{\isacharunderscore}all{\isadigit{2}}\ eq{\isacharunderscore}class{\isachardot}eq\ typargs{\isadigit{1}}\ typargs{\isadigit{2}}{\isachardoublequoteclose}\isanewline
-\ \ \isacommand{by}\isamarkupfalse%
-\ {\isacharparenleft}simp\ add{\isacharcolon}\ eq\ list{\isacharunderscore}all{\isadigit{2}}{\isacharunderscore}eq\ {\isacharbrackleft}symmetric{\isacharbrackright}{\isacharparenright}%
-\endisatagquote
-{\isafoldquote}%
-%
-\isadelimquote
-%
-\endisadelimquote
-%
-\begin{isamarkuptext}%
-\noindent does not depend on instance \isa{monotype\ {\isasymColon}\ eq}:%
-\end{isamarkuptext}%
-\isamarkuptrue%
-%
-\isadelimquote
-%
-\endisadelimquote
-%
-\isatagquote
-%
-\begin{isamarkuptext}%
-\isatypewriter%
-\noindent%
-\hspace*{0pt}structure Example = \\
-\hspace*{0pt}struct\\
-\hspace*{0pt}\\
-\hspace*{0pt}datatype nat = Zero{\char95}nat | Suc of nat;\\
-\hspace*{0pt}\\
-\hspace*{0pt}fun null [] = true\\
-\hspace*{0pt} ~| null (x ::~xs) = false;\\
-\hspace*{0pt}\\
-\hspace*{0pt}fun eq{\char95}nat (Suc nat') Zero{\char95}nat = false\\
-\hspace*{0pt} ~| eq{\char95}nat Zero{\char95}nat (Suc nat') = false\\
-\hspace*{0pt} ~| eq{\char95}nat (Suc nat) (Suc nat') = eq{\char95}nat nat nat'\\
-\hspace*{0pt} ~| eq{\char95}nat Zero{\char95}nat Zero{\char95}nat = true;\\
-\hspace*{0pt}\\
-\hspace*{0pt}datatype monotype = Mono of nat * monotype list;\\
-\hspace*{0pt}\\
-\hspace*{0pt}fun list{\char95}all2 p (x ::~xs) (y ::~ys) = p x y andalso list{\char95}all2 p xs ys\\
-\hspace*{0pt} ~| list{\char95}all2 p xs [] = null xs\\
-\hspace*{0pt} ~| list{\char95}all2 p [] ys = null ys;\\
-\hspace*{0pt}\\
-\hspace*{0pt}fun eq{\char95}monotype (Mono (tyco1,~typargs1)) (Mono (tyco2,~typargs2)) =\\
-\hspace*{0pt} ~eq{\char95}nat tyco1 tyco2 andalso list{\char95}all2 eq{\char95}monotype typargs1 typargs2;\\
-\hspace*{0pt}\\
-\hspace*{0pt}end;~(*struct Example*)%
-\end{isamarkuptext}%
-\isamarkuptrue%
-%
-\endisatagquote
-{\isafoldquote}%
-%
-\isadelimquote
-%
-\endisadelimquote
-%
\isamarkupsubsection{Explicit partiality%
}
\isamarkuptrue%
--- a/doc-src/Codegen/Thy/examples/example.ML Mon Nov 16 10:03:58 2009 +0100
+++ b/doc-src/Codegen/Thy/examples/example.ML Mon Nov 16 11:03:14 2009 +0100
@@ -11,7 +11,7 @@
datatype 'a queue = AQueue of 'a list * 'a list;
-val empty : 'a queue = AQueue ([], [])
+val empty : 'a queue = AQueue ([], []);
fun dequeue (AQueue ([], [])) = (NONE, AQueue ([], []))
| dequeue (AQueue (xs, y :: ys)) = (SOME y, AQueue (xs, ys))