# HG changeset patch # User haftmann # Date 1258365794 -3600 # Node ID 68841fb382e0c2ff0d4c69d5c19b6f740d02ad58 # Parent 7017aee615d69376c89c473c6f791dfcd291a630 dropped obsolete documentation; updated generated sources diff -r 7017aee615d6 -r 68841fb382e0 doc-src/Codegen/Thy/ML.thy --- 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. diff -r 7017aee615d6 -r 68841fb382e0 doc-src/Codegen/Thy/Program.thy --- 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) \ - eq_class.eq tyco1 tyco2 \ 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 \ 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) \ - eq_class.eq tyco1 tyco2 \ list_all2 eq_class.eq typargs1 typargs2" - by (simp add: eq list_all2_eq [symmetric]) - -text {* - \noindent does not depend on instance @{text "monotype \ eq"}: -*} - -text %quote {*@{code_stmts "eq_class.eq :: monotype \ monotype \ bool" (SML)}*} - subsection {* Explicit partiality *} diff -r 7017aee615d6 -r 68841fb382e0 doc-src/Codegen/Thy/document/Adaptation.tex --- 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\\ diff -r 7017aee615d6 -r 68841fb382e0 doc-src/Codegen/Thy/document/Introduction.tex --- 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))\\ diff -r 7017aee615d6 -r 68841fb382e0 doc-src/Codegen/Thy/document/ML.tex --- 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. diff -r 7017aee615d6 -r 68841fb382e0 doc-src/Codegen/Thy/document/Program.tex --- 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% diff -r 7017aee615d6 -r 68841fb382e0 doc-src/Codegen/Thy/examples/example.ML --- 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))