--- a/doc-src/Codegen/Thy/Further.thy Mon May 31 17:20:41 2010 +0200
+++ b/doc-src/Codegen/Thy/Further.thy Mon May 31 17:41:06 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.
--- a/doc-src/Codegen/Thy/ML.thy Mon May 31 17:20:41 2010 +0200
+++ b/doc-src/Codegen/Thy/ML.thy Mon May 31 17:41:06 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
--- a/doc-src/Codegen/Thy/Program.thy Mon May 31 17:20:41 2010 +0200
+++ b/doc-src/Codegen/Thy/Program.thy Mon May 31 17:41:06 2010 +0200
@@ -172,22 +172,22 @@
\item replacing non-executable constructs by executable ones:
*}
-lemma %quote [code_inline]:
- "x \<in> set xs \<longleftrightarrow> x mem xs" by (induct xs) simp_all
+lemma %quote [code_unfold]:
+ "x \<in> set xs \<longleftrightarrow> member xs x" by (fact in_set_code)
text {*
\item eliminating superfluous constants:
*}
-lemma %quote [code_inline]:
- "1 = Suc 0" by simp
+lemma %quote [code_unfold]:
+ "1 = Suc 0" by (fact One_nat_def)
text {*
\item replacing executable but inconvenient constructs:
*}
-lemma %quote [code_inline]:
- "xs = [] \<longleftrightarrow> List.null xs" by (induct xs) simp_all
+lemma %quote [code_unfold]:
+ "xs = [] \<longleftrightarrow> List.null xs" by (fact empty_null)
text_raw {*
\end{itemize}
--- a/doc-src/Codegen/Thy/document/ML.tex Mon May 31 17:20:41 2010 +0200
+++ b/doc-src/Codegen/Thy/document/ML.tex Mon May 31 17:41:06 2010 +0200
@@ -60,9 +60,9 @@
\verb| -> theory -> theory| \\
\indexdef{}{ML}{Code\_Preproc.del\_functrans}\verb|Code_Preproc.del_functrans: string -> theory -> theory| \\
\indexdef{}{ML}{Code.add\_datatype}\verb|Code.add_datatype: (string * typ) list -> theory -> theory| \\
- \indexdef{}{ML}{Code.get\_datatype}\verb|Code.get_datatype: theory -> string|\isasep\isanewline%
+ \indexdef{}{ML}{Code.get\_type}\verb|Code.get_type: theory -> string|\isasep\isanewline%
\verb| -> (string * sort) list * (string * typ list) list| \\
- \indexdef{}{ML}{Code.get\_datatype\_of\_constr}\verb|Code.get_datatype_of_constr: theory -> string -> string option|
+ \indexdef{}{ML}{Code.get\_type\_of\_constr\_or\_abstr}\verb|Code.get_type_of_constr_or_abstr: theory -> string -> (string * bool) option|
\end{mldecls}
\begin{description}
@@ -91,7 +91,7 @@
a datatype to executable content, with generation
set \isa{cs}.
- \item \verb|Code.get_datatype_of_constr|~\isa{thy}~\isa{const}
+ \item \verb|Code.get_type_of_constr_or_abstr|~\isa{thy}~\isa{const}
returns type constructor corresponding to
constructor \isa{const}; returns \isa{NONE}
if \isa{const} is no constructor.
@@ -163,7 +163,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 \verb|CodeDataFun|; on instantiation
+ data slot \verb|Code_Data|; on instantiation
of this functor, the following types and operations
are required:
@@ -189,7 +189,7 @@
\end{description}
- \noindent An instance of \verb|CodeDataFun| provides the following
+ \noindent An instance of \verb|Code_Data| provides the following
interface:
\medskip
--- a/doc-src/Codegen/Thy/document/Program.tex Mon May 31 17:20:41 2010 +0200
+++ b/doc-src/Codegen/Thy/document/Program.tex Mon May 31 17:41:06 2010 +0200
@@ -432,9 +432,9 @@
%
\isatagquote
\isacommand{lemma}\isamarkupfalse%
-\ {\isacharbrackleft}code{\isacharunderscore}inline{\isacharbrackright}{\isacharcolon}\isanewline
-\ \ {\isachardoublequoteopen}x\ {\isasymin}\ set\ xs\ {\isasymlongleftrightarrow}\ x\ mem\ xs{\isachardoublequoteclose}\ \isacommand{by}\isamarkupfalse%
-\ {\isacharparenleft}induct\ xs{\isacharparenright}\ simp{\isacharunderscore}all%
+\ {\isacharbrackleft}code{\isacharunderscore}unfold{\isacharbrackright}{\isacharcolon}\isanewline
+\ \ {\isachardoublequoteopen}x\ {\isasymin}\ set\ xs\ {\isasymlongleftrightarrow}\ member\ xs\ x{\isachardoublequoteclose}\ \isacommand{by}\isamarkupfalse%
+\ {\isacharparenleft}fact\ in{\isacharunderscore}set{\isacharunderscore}code{\isacharparenright}%
\endisatagquote
{\isafoldquote}%
%
@@ -453,9 +453,9 @@
%
\isatagquote
\isacommand{lemma}\isamarkupfalse%
-\ {\isacharbrackleft}code{\isacharunderscore}inline{\isacharbrackright}{\isacharcolon}\isanewline
+\ {\isacharbrackleft}code{\isacharunderscore}unfold{\isacharbrackright}{\isacharcolon}\isanewline
\ \ {\isachardoublequoteopen}{\isadigit{1}}\ {\isacharequal}\ Suc\ {\isadigit{0}}{\isachardoublequoteclose}\ \isacommand{by}\isamarkupfalse%
-\ simp%
+\ {\isacharparenleft}fact\ One{\isacharunderscore}nat{\isacharunderscore}def{\isacharparenright}%
\endisatagquote
{\isafoldquote}%
%
@@ -474,9 +474,9 @@
%
\isatagquote
\isacommand{lemma}\isamarkupfalse%
-\ {\isacharbrackleft}code{\isacharunderscore}inline{\isacharbrackright}{\isacharcolon}\isanewline
+\ {\isacharbrackleft}code{\isacharunderscore}unfold{\isacharbrackright}{\isacharcolon}\isanewline
\ \ {\isachardoublequoteopen}xs\ {\isacharequal}\ {\isacharbrackleft}{\isacharbrackright}\ {\isasymlongleftrightarrow}\ List{\isachardot}null\ xs{\isachardoublequoteclose}\ \isacommand{by}\isamarkupfalse%
-\ {\isacharparenleft}induct\ xs{\isacharparenright}\ simp{\isacharunderscore}all%
+\ {\isacharparenleft}fact\ empty{\isacharunderscore}null{\isacharparenright}%
\endisatagquote
{\isafoldquote}%
%
@@ -763,7 +763,7 @@
%
\begin{isamarkuptext}%
\noindent The membership test during preprocessing is rewritten,
- resulting in \isa{op\ mem}, which itself
+ resulting in \isa{member}, which itself
performs an explicit equality check.%
\end{isamarkuptext}%
\isamarkuptrue%
@@ -781,7 +781,7 @@
\hspace*{0pt} ~type 'a eq\\
\hspace*{0pt} ~val eq :~'a eq -> 'a -> 'a -> bool\\
\hspace*{0pt} ~val eqa :~'a eq -> 'a -> 'a -> bool\\
-\hspace*{0pt} ~val member :~'a eq -> 'a -> 'a list -> bool\\
+\hspace*{0pt} ~val member :~'a eq -> 'a list -> 'a -> bool\\
\hspace*{0pt} ~val collect{\char95}duplicates :\\
\hspace*{0pt} ~~~'a eq -> 'a list -> 'a list -> 'a list -> 'a list\\
\hspace*{0pt}end = struct\\
@@ -791,13 +791,13 @@
\hspace*{0pt}\\
\hspace*{0pt}fun eqa A{\char95}~a b = eq A{\char95}~a b;\\
\hspace*{0pt}\\
-\hspace*{0pt}fun member A{\char95}~x [] = false\\
-\hspace*{0pt} ~| member A{\char95}~x (y ::~ys) = eqa A{\char95}~x y orelse member A{\char95}~x ys;\\
+\hspace*{0pt}fun member A{\char95}~[] y = false\\
+\hspace*{0pt} ~| member A{\char95}~(x ::~xs) y = eqa A{\char95}~x y orelse member A{\char95}~xs y;\\
\hspace*{0pt}\\
\hspace*{0pt}fun collect{\char95}duplicates A{\char95}~xs ys [] = xs\\
\hspace*{0pt} ~| collect{\char95}duplicates A{\char95}~xs ys (z ::~zs) =\\
-\hspace*{0pt} ~~~(if member A{\char95}~z xs\\
-\hspace*{0pt} ~~~~~then (if member A{\char95}~z ys then collect{\char95}duplicates A{\char95}~xs ys zs\\
+\hspace*{0pt} ~~~(if member A{\char95}~xs z\\
+\hspace*{0pt} ~~~~~then (if member A{\char95}~ys z then collect{\char95}duplicates A{\char95}~xs ys zs\\
\hspace*{0pt} ~~~~~~~~~~~~else collect{\char95}duplicates A{\char95}~xs (z ::~ys) zs)\\
\hspace*{0pt} ~~~~~else collect{\char95}duplicates A{\char95}~(z ::~xs) (z ::~ys) zs);\\
\hspace*{0pt}\\
@@ -968,11 +968,10 @@
\hspace*{0pt}empty{\char95}queue ::~forall a.~a;\\
\hspace*{0pt}empty{\char95}queue = error {\char34}empty{\char95}queue{\char34};\\
\hspace*{0pt}\\
-\hspace*{0pt}strict{\char95}dequeue' ::~forall a.~Queue a -> (a,~Queue a);\\
-\hspace*{0pt}strict{\char95}dequeue' (AQueue xs (y :~ys)) = (y,~AQueue xs ys);\\
-\hspace*{0pt}strict{\char95}dequeue' (AQueue xs []) =\\
-\hspace*{0pt} ~(if nulla xs then empty{\char95}queue\\
-\hspace*{0pt} ~~~else strict{\char95}dequeue' (AQueue [] (rev xs)));%
+\hspace*{0pt}strict{\char95}dequeue ::~forall a.~Queue a -> (a,~Queue a);\\
+\hspace*{0pt}strict{\char95}dequeue (AQueue xs (y :~ys)) = (y,~AQueue xs ys);\\
+\hspace*{0pt}strict{\char95}dequeue (AQueue xs []) =\\
+\hspace*{0pt} ~(if nulla xs then empty{\char95}queue else strict{\char95}dequeue (AQueue [] (rev xs)));%
\end{isamarkuptext}%
\isamarkuptrue%
%
@@ -1290,7 +1289,7 @@
%
\begin{isamarkuptext}%
\begin{isabelle}%
-lexord\ r\ {\isasymequiv}\isanewline
+lexord\ r\ {\isacharequal}\isanewline
{\isacharbraceleft}{\isacharparenleft}x{\isacharcomma}\ y{\isacharparenright}{\isachardot}\isanewline
\isaindent{\ }{\isasymexists}a\ v{\isachardot}\ y\ {\isacharequal}\ x\ {\isacharat}\ a\ {\isacharhash}\ v\ {\isasymor}\isanewline
\isaindent{\ {\isasymexists}a\ v{\isachardot}\ }{\isacharparenleft}{\isasymexists}u\ a\ b\ v\ w{\isachardot}\ {\isacharparenleft}a{\isacharcomma}\ b{\isacharparenright}\ {\isasymin}\ r\ {\isasymand}\ x\ {\isacharequal}\ u\ {\isacharat}\ a\ {\isacharhash}\ v\ {\isasymand}\ y\ {\isacharequal}\ u\ {\isacharat}\ b\ {\isacharhash}\ w{\isacharparenright}{\isacharbraceright}%