--- a/doc-src/IsarAdvanced/Codegen/Thy/Codegen.thy Thu Jan 25 16:57:57 2007 +0100
+++ b/doc-src/IsarAdvanced/Codegen/Thy/Codegen.thy Fri Jan 26 09:24:35 2007 +0100
@@ -1,4 +1,3 @@
-
(* $Id$ *)
(*<*)
@@ -365,6 +364,7 @@
the file system, with root given by the user.
*}
+ML {* set Toplevel.debug *}
code_gen dummy (Haskell "examples/")
(* NOTE: you may use Haskell only once in this document, otherwise
you have to work in distinct subdirectories *)
@@ -809,7 +809,7 @@
\lstsml{Thy/examples/lookup.ML}
*}
-subsubsection {* lexicographic orderings and coregularity *}
+subsubsection {* lexicographic orderings *}
text {*
Another subtlety
@@ -818,23 +818,16 @@
us define a lexicographic ordering on tuples:
*}
-(*<*)
-setup {* Sign.add_path "foobar" *}
-class ord =
- fixes less_eq :: "'a \<Rightarrow> 'a \<Rightarrow> bool" ("(_/ \<^loc>\<le> _)" [50, 51] 50)
- fixes less :: "'a \<Rightarrow> 'a \<Rightarrow> bool" ("(_/ \<^loc>< _)" [50, 51] 50)
-(*>*)
-
instance * :: (ord, ord) ord
"p1 < p2 \<equiv> let (x1 \<Colon> 'a\<Colon>ord, y1 \<Colon> 'b\<Colon>ord) = p1; (x2, y2) = p2 in
x1 < x2 \<or> (x1 = x2 \<and> y1 < y2)"
- "p1 \<le> p2 \<equiv> p1 < p2 \<or> (p1 \<Colon> 'a\<Colon>ord \<times> 'b\<Colon>ord) = p2" ..
+ "p1 \<le> p2 \<equiv> let (x1 \<Colon> 'a\<Colon>ord, y1 \<Colon> 'b\<Colon>ord) = p1; (x2, y2) = p2 in
+ x1 < x2 \<or> (x1 = x2 \<and> y1 \<le> y2)" ..
-(*<*)
-hide "class" ord
-hide const less_eq less
-setup {* Sign.parent_path *}
-(*>*)
+lemma ord_prod [code func]:
+ "(x1 \<Colon> 'a\<Colon>ord, y1 \<Colon> 'b\<Colon>ord) < (x2, y2) \<longleftrightarrow> x1 < x2 \<or> (x1 = x2 \<and> y1 < y2)"
+ "(x1 \<Colon> 'a\<Colon>ord, y1 \<Colon> 'b\<Colon>ord) \<le> (x2, y2) \<longleftrightarrow> x1 < x2 \<or> (x1 = x2 \<and> y1 \<le> y2)"
+ unfolding "less_eq_*_def" "less_*_def" by simp_all
text {*
Then code generation will fail. Why? The definition
@@ -843,25 +836,38 @@
class constraint, thus violating the type discipline
for class operations.
- The solution is to add @{text eq} to both sort arguments:
+ The solution is to add @{text eq} explicitly to the first sort arguments in the
+ code theorems:
*}
-instance * :: ("{eq, ord}", "{eq, ord}") ord
- "p1 < p2 \<equiv> let (x1 \<Colon> 'a\<Colon>{eq, ord}, y1 \<Colon> 'b\<Colon>{eq, ord}) = p1; (x2, y2) = p2 in
- x1 < x2 \<or> (x1 = x2 \<and> y1 < y2)"
- "p1 \<le> p2 \<equiv> p1 < p2 \<or> (p1 \<Colon> 'a\<Colon>{eq, ord} \<times> 'b\<Colon>{eq, ord}) = p2" ..
+(*<*)
+declare ord_prod [code del]
+(*>*)
+
+lemma ord_prod_code [code func]:
+ "(x1 \<Colon> 'a\<Colon>{ord, eq}, y1 \<Colon> 'b\<Colon>ord) < (x2, y2) \<longleftrightarrow> x1 < x2 \<or> (x1 = x2 \<and> y1 < y2)"
+ "(x1 \<Colon> 'a\<Colon>{ord, eq}, y1 \<Colon> 'b\<Colon>ord) \<le> (x2, y2) \<longleftrightarrow> x1 < x2 \<or> (x1 = x2 \<and> y1 \<le> y2)"
+ unfolding ord_prod by rule+
text {*
Then code generation succeeds:
*}
-code_gen "op \<le> \<Colon> 'a\<Colon>{eq, ord} \<times> 'b\<Colon>{eq, ord} \<Rightarrow> 'a \<times> 'b \<Rightarrow> bool"
+code_gen "op \<le> \<Colon> 'a\<Colon>{eq, ord} \<times> 'b\<Colon>ord \<Rightarrow> 'a \<times> 'b \<Rightarrow> bool"
(*<*)(SML #)(*>*)(SML "examples/lexicographic.ML")
text {*
\lstsml{Thy/examples/lexicographic.ML}
*}
+text {*
+ In general, code theorems for overloaded constants may have more
+ restrictive sort constraints than the underlying instance relation
+ between class and type constructor as long as the whole system of
+ constraints is coregular; code theorems violating coregularity
+ are rejected immediately.
+*}
+
subsubsection {* Haskell serialization *}
text {*
@@ -903,10 +909,10 @@
(Haskell "Integer")
text {*
- The code generator would produce
- an additional instance, which of course is rejected.
- To suppress this additional instance, use
- @{text "\<CODEINSTANCE>"}:
+ The code generator would produce
+ an additional instance, which of course is rejected.
+ To suppress this additional instance, use
+ @{text "\<CODEINSTANCE>"}:
*}
code_instance %tt bar :: eq
--- a/doc-src/IsarAdvanced/Codegen/Thy/document/Codegen.tex Thu Jan 25 16:57:57 2007 +0100
+++ b/doc-src/IsarAdvanced/Codegen/Thy/document/Codegen.tex Fri Jan 26 09:24:35 2007 +0100
@@ -4,7 +4,6 @@
%
\isadelimtheory
\isanewline
-\isanewline
%
\endisadelimtheory
%
@@ -490,6 +489,21 @@
the file system, with root given by the user.%
\end{isamarkuptext}%
\isamarkuptrue%
+%
+\isadelimML
+%
+\endisadelimML
+%
+\isatagML
+\isacommand{ML}\isamarkupfalse%
+\ {\isacharverbatimopen}\ set\ Toplevel{\isachardot}debug\ {\isacharverbatimclose}%
+\endisatagML
+{\isafoldML}%
+%
+\isadelimML
+%
+\endisadelimML
+\isanewline
\isacommand{code{\isacharunderscore}gen}\isamarkupfalse%
\ dummy\ {\isacharparenleft}Haskell\ {\isachardoublequoteopen}examples{\isacharslash}{\isachardoublequoteclose}{\isacharparenright}%
\begin{isamarkuptext}%
@@ -1095,7 +1109,7 @@
\end{isamarkuptext}%
\isamarkuptrue%
%
-\isamarkupsubsubsection{lexicographic orderings and coregularity%
+\isamarkupsubsubsection{lexicographic orderings%
}
\isamarkuptrue%
%
@@ -1106,68 +1120,12 @@
us define a lexicographic ordering on tuples:%
\end{isamarkuptext}%
\isamarkuptrue%
-%
-\isadelimML
-%
-\endisadelimML
-%
-\isatagML
-%
-\endisatagML
-{\isafoldML}%
-%
-\isadelimML
-%
-\endisadelimML
-\isanewline
\isacommand{instance}\isamarkupfalse%
\ {\isacharasterisk}\ {\isacharcolon}{\isacharcolon}\ {\isacharparenleft}ord{\isacharcomma}\ ord{\isacharparenright}\ ord\isanewline
\ \ {\isachardoublequoteopen}p{\isadigit{1}}\ {\isacharless}\ p{\isadigit{2}}\ {\isasymequiv}\ let\ {\isacharparenleft}x{\isadigit{1}}\ {\isasymColon}\ {\isacharprime}a{\isasymColon}ord{\isacharcomma}\ y{\isadigit{1}}\ {\isasymColon}\ {\isacharprime}b{\isasymColon}ord{\isacharparenright}\ {\isacharequal}\ p{\isadigit{1}}{\isacharsemicolon}\ {\isacharparenleft}x{\isadigit{2}}{\isacharcomma}\ y{\isadigit{2}}{\isacharparenright}\ {\isacharequal}\ p{\isadigit{2}}\ in\isanewline
\ \ \ \ x{\isadigit{1}}\ {\isacharless}\ x{\isadigit{2}}\ {\isasymor}\ {\isacharparenleft}x{\isadigit{1}}\ {\isacharequal}\ x{\isadigit{2}}\ {\isasymand}\ y{\isadigit{1}}\ {\isacharless}\ y{\isadigit{2}}{\isacharparenright}{\isachardoublequoteclose}\isanewline
-\ \ {\isachardoublequoteopen}p{\isadigit{1}}\ {\isasymle}\ p{\isadigit{2}}\ {\isasymequiv}\ p{\isadigit{1}}\ {\isacharless}\ p{\isadigit{2}}\ {\isasymor}\ {\isacharparenleft}p{\isadigit{1}}\ {\isasymColon}\ {\isacharprime}a{\isasymColon}ord\ {\isasymtimes}\ {\isacharprime}b{\isasymColon}ord{\isacharparenright}\ \ {\isacharequal}\ p{\isadigit{2}}{\isachardoublequoteclose}%
-\isadelimproof
-\ %
-\endisadelimproof
-%
-\isatagproof
-\isacommand{{\isachardot}{\isachardot}}\isamarkupfalse%
-\isanewline
-%
-\endisatagproof
-{\isafoldproof}%
-%
-\isadelimproof
-%
-\endisadelimproof
-%
-\isadelimML
-%
-\endisadelimML
-%
-\isatagML
-%
-\endisatagML
-{\isafoldML}%
-%
-\isadelimML
-%
-\endisadelimML
-%
-\begin{isamarkuptext}%
-Then code generation will fail. Why? The definition
- of \isa{op\ {\isasymle}} depends on equality on both arguments,
- which are polymorphic and impose an additional \isa{eq}
- class constraint, thus violating the type discipline
- for class operations.
-
- The solution is to add \isa{eq} to both sort arguments:%
-\end{isamarkuptext}%
-\isamarkuptrue%
-\isacommand{instance}\isamarkupfalse%
-\ {\isacharasterisk}\ {\isacharcolon}{\isacharcolon}\ {\isacharparenleft}{\isachardoublequoteopen}{\isacharbraceleft}eq{\isacharcomma}\ ord{\isacharbraceright}{\isachardoublequoteclose}{\isacharcomma}\ {\isachardoublequoteopen}{\isacharbraceleft}eq{\isacharcomma}\ ord{\isacharbraceright}{\isachardoublequoteclose}{\isacharparenright}\ ord\isanewline
-\ \ {\isachardoublequoteopen}p{\isadigit{1}}\ {\isacharless}\ p{\isadigit{2}}\ {\isasymequiv}\ let\ {\isacharparenleft}x{\isadigit{1}}\ {\isasymColon}\ {\isacharprime}a{\isasymColon}{\isacharbraceleft}eq{\isacharcomma}\ ord{\isacharbraceright}{\isacharcomma}\ y{\isadigit{1}}\ {\isasymColon}\ {\isacharprime}b{\isasymColon}{\isacharbraceleft}eq{\isacharcomma}\ ord{\isacharbraceright}{\isacharparenright}\ {\isacharequal}\ p{\isadigit{1}}{\isacharsemicolon}\ {\isacharparenleft}x{\isadigit{2}}{\isacharcomma}\ y{\isadigit{2}}{\isacharparenright}\ {\isacharequal}\ p{\isadigit{2}}\ in\isanewline
-\ \ \ \ x{\isadigit{1}}\ {\isacharless}\ x{\isadigit{2}}\ {\isasymor}\ {\isacharparenleft}x{\isadigit{1}}\ {\isacharequal}\ x{\isadigit{2}}\ {\isasymand}\ y{\isadigit{1}}\ {\isacharless}\ y{\isadigit{2}}{\isacharparenright}{\isachardoublequoteclose}\isanewline
-\ \ {\isachardoublequoteopen}p{\isadigit{1}}\ {\isasymle}\ p{\isadigit{2}}\ {\isasymequiv}\ p{\isadigit{1}}\ {\isacharless}\ p{\isadigit{2}}\ {\isasymor}\ {\isacharparenleft}p{\isadigit{1}}\ {\isasymColon}\ {\isacharprime}a{\isasymColon}{\isacharbraceleft}eq{\isacharcomma}\ ord{\isacharbraceright}\ {\isasymtimes}\ {\isacharprime}b{\isasymColon}{\isacharbraceleft}eq{\isacharcomma}\ ord{\isacharbraceright}{\isacharparenright}\ \ {\isacharequal}\ p{\isadigit{2}}{\isachardoublequoteclose}%
+\ \ {\isachardoublequoteopen}p{\isadigit{1}}\ {\isasymle}\ p{\isadigit{2}}\ {\isasymequiv}\ let\ {\isacharparenleft}x{\isadigit{1}}\ {\isasymColon}\ {\isacharprime}a{\isasymColon}ord{\isacharcomma}\ y{\isadigit{1}}\ {\isasymColon}\ {\isacharprime}b{\isasymColon}ord{\isacharparenright}\ {\isacharequal}\ p{\isadigit{1}}{\isacharsemicolon}\ {\isacharparenleft}x{\isadigit{2}}{\isacharcomma}\ y{\isadigit{2}}{\isacharparenright}\ {\isacharequal}\ p{\isadigit{2}}\ in\isanewline
+\ \ \ \ x{\isadigit{1}}\ {\isacharless}\ x{\isadigit{2}}\ {\isasymor}\ {\isacharparenleft}x{\isadigit{1}}\ {\isacharequal}\ x{\isadigit{2}}\ {\isasymand}\ y{\isadigit{1}}\ {\isasymle}\ y{\isadigit{2}}{\isacharparenright}{\isachardoublequoteclose}%
\isadelimproof
\ %
\endisadelimproof
@@ -1181,19 +1139,81 @@
\isadelimproof
%
\endisadelimproof
+\isanewline
+\isanewline
+\isacommand{lemma}\isamarkupfalse%
+\ ord{\isacharunderscore}prod\ {\isacharbrackleft}code\ func{\isacharbrackright}{\isacharcolon}\isanewline
+\ \ {\isachardoublequoteopen}{\isacharparenleft}x{\isadigit{1}}\ {\isasymColon}\ {\isacharprime}a{\isasymColon}ord{\isacharcomma}\ y{\isadigit{1}}\ {\isasymColon}\ {\isacharprime}b{\isasymColon}ord{\isacharparenright}\ {\isacharless}\ {\isacharparenleft}x{\isadigit{2}}{\isacharcomma}\ y{\isadigit{2}}{\isacharparenright}\ {\isasymlongleftrightarrow}\ x{\isadigit{1}}\ {\isacharless}\ x{\isadigit{2}}\ {\isasymor}\ {\isacharparenleft}x{\isadigit{1}}\ {\isacharequal}\ x{\isadigit{2}}\ {\isasymand}\ y{\isadigit{1}}\ {\isacharless}\ y{\isadigit{2}}{\isacharparenright}{\isachardoublequoteclose}\isanewline
+\ \ {\isachardoublequoteopen}{\isacharparenleft}x{\isadigit{1}}\ {\isasymColon}\ {\isacharprime}a{\isasymColon}ord{\isacharcomma}\ y{\isadigit{1}}\ {\isasymColon}\ {\isacharprime}b{\isasymColon}ord{\isacharparenright}\ {\isasymle}\ {\isacharparenleft}x{\isadigit{2}}{\isacharcomma}\ y{\isadigit{2}}{\isacharparenright}\ {\isasymlongleftrightarrow}\ x{\isadigit{1}}\ {\isacharless}\ x{\isadigit{2}}\ {\isasymor}\ {\isacharparenleft}x{\isadigit{1}}\ {\isacharequal}\ x{\isadigit{2}}\ {\isasymand}\ y{\isadigit{1}}\ {\isasymle}\ y{\isadigit{2}}{\isacharparenright}{\isachardoublequoteclose}\isanewline
+%
+\isadelimproof
+\ \ %
+\endisadelimproof
+%
+\isatagproof
+\isacommand{unfolding}\isamarkupfalse%
+\ {\isachardoublequoteopen}less{\isacharunderscore}eq{\isacharunderscore}{\isacharasterisk}{\isacharunderscore}def{\isachardoublequoteclose}\ {\isachardoublequoteopen}less{\isacharunderscore}{\isacharasterisk}{\isacharunderscore}def{\isachardoublequoteclose}\ \isacommand{by}\isamarkupfalse%
+\ simp{\isacharunderscore}all%
+\endisatagproof
+{\isafoldproof}%
+%
+\isadelimproof
+%
+\endisadelimproof
+%
+\begin{isamarkuptext}%
+Then code generation will fail. Why? The definition
+ of \isa{op\ {\isasymle}} depends on equality on both arguments,
+ which are polymorphic and impose an additional \isa{eq}
+ class constraint, thus violating the type discipline
+ for class operations.
+
+ The solution is to add \isa{eq} explicitly to the first sort arguments in the
+ code theorems:%
+\end{isamarkuptext}%
+\isamarkuptrue%
+\isanewline
+\isacommand{lemma}\isamarkupfalse%
+\ ord{\isacharunderscore}prod{\isacharunderscore}code\ {\isacharbrackleft}code\ func{\isacharbrackright}{\isacharcolon}\isanewline
+\ \ {\isachardoublequoteopen}{\isacharparenleft}x{\isadigit{1}}\ {\isasymColon}\ {\isacharprime}a{\isasymColon}{\isacharbraceleft}ord{\isacharcomma}\ eq{\isacharbraceright}{\isacharcomma}\ y{\isadigit{1}}\ {\isasymColon}\ {\isacharprime}b{\isasymColon}ord{\isacharparenright}\ {\isacharless}\ {\isacharparenleft}x{\isadigit{2}}{\isacharcomma}\ y{\isadigit{2}}{\isacharparenright}\ {\isasymlongleftrightarrow}\ x{\isadigit{1}}\ {\isacharless}\ x{\isadigit{2}}\ {\isasymor}\ {\isacharparenleft}x{\isadigit{1}}\ {\isacharequal}\ x{\isadigit{2}}\ {\isasymand}\ y{\isadigit{1}}\ {\isacharless}\ y{\isadigit{2}}{\isacharparenright}{\isachardoublequoteclose}\isanewline
+\ \ {\isachardoublequoteopen}{\isacharparenleft}x{\isadigit{1}}\ {\isasymColon}\ {\isacharprime}a{\isasymColon}{\isacharbraceleft}ord{\isacharcomma}\ eq{\isacharbraceright}{\isacharcomma}\ y{\isadigit{1}}\ {\isasymColon}\ {\isacharprime}b{\isasymColon}ord{\isacharparenright}\ {\isasymle}\ {\isacharparenleft}x{\isadigit{2}}{\isacharcomma}\ y{\isadigit{2}}{\isacharparenright}\ {\isasymlongleftrightarrow}\ x{\isadigit{1}}\ {\isacharless}\ x{\isadigit{2}}\ {\isasymor}\ {\isacharparenleft}x{\isadigit{1}}\ {\isacharequal}\ x{\isadigit{2}}\ {\isasymand}\ y{\isadigit{1}}\ {\isasymle}\ y{\isadigit{2}}{\isacharparenright}{\isachardoublequoteclose}\isanewline
+%
+\isadelimproof
+\ \ %
+\endisadelimproof
+%
+\isatagproof
+\isacommand{unfolding}\isamarkupfalse%
+\ ord{\isacharunderscore}prod\ \isacommand{by}\isamarkupfalse%
+\ rule{\isacharplus}%
+\endisatagproof
+{\isafoldproof}%
+%
+\isadelimproof
+%
+\endisadelimproof
%
\begin{isamarkuptext}%
Then code generation succeeds:%
\end{isamarkuptext}%
\isamarkuptrue%
\isacommand{code{\isacharunderscore}gen}\isamarkupfalse%
-\ {\isachardoublequoteopen}op\ {\isasymle}\ {\isasymColon}\ {\isacharprime}a{\isasymColon}{\isacharbraceleft}eq{\isacharcomma}\ ord{\isacharbraceright}\ {\isasymtimes}\ {\isacharprime}b{\isasymColon}{\isacharbraceleft}eq{\isacharcomma}\ ord{\isacharbraceright}\ {\isasymRightarrow}\ {\isacharprime}a\ {\isasymtimes}\ {\isacharprime}b\ {\isasymRightarrow}\ bool{\isachardoublequoteclose}\isanewline
+\ {\isachardoublequoteopen}op\ {\isasymle}\ {\isasymColon}\ {\isacharprime}a{\isasymColon}{\isacharbraceleft}eq{\isacharcomma}\ ord{\isacharbraceright}\ {\isasymtimes}\ {\isacharprime}b{\isasymColon}ord\ {\isasymRightarrow}\ {\isacharprime}a\ {\isasymtimes}\ {\isacharprime}b\ {\isasymRightarrow}\ bool{\isachardoublequoteclose}\isanewline
\ \ {\isacharparenleft}SML\ {\isachardoublequoteopen}examples{\isacharslash}lexicographic{\isachardot}ML{\isachardoublequoteclose}{\isacharparenright}%
\begin{isamarkuptext}%
\lstsml{Thy/examples/lexicographic.ML}%
\end{isamarkuptext}%
\isamarkuptrue%
%
+\begin{isamarkuptext}%
+In general, code theorems for overloaded constants may have more
+ restrictive sort constraints than the underlying instance relation
+ between class and type constructor as long as the whole system of
+ constraints is coregular; code theorems violating coregularity
+ are rejected immediately.%
+\end{isamarkuptext}%
+\isamarkuptrue%
+%
\isamarkupsubsubsection{Haskell serialization%
}
\isamarkuptrue%
@@ -1298,9 +1318,9 @@
%
\begin{isamarkuptext}%
The code generator would produce
- an additional instance, which of course is rejected.
- To suppress this additional instance, use
- \isa{{\isasymCODEINSTANCE}}:%
+ an additional instance, which of course is rejected.
+ To suppress this additional instance, use
+ \isa{{\isasymCODEINSTANCE}}:%
\end{isamarkuptext}%
\isamarkuptrue%
%
@@ -1521,7 +1541,7 @@
For technical reasons, we further have to provide a
synonym for \isa{None} which in code generator view
- is a function rather than a datatype constructor:%
+ is a function rather than a term constructor:%
\end{isamarkuptext}%
\isamarkuptrue%
\isacommand{definition}\isamarkupfalse%
--- a/doc-src/IsarAdvanced/Codegen/Thy/examples/Codegen.hs Thu Jan 25 16:57:57 2007 +0100
+++ b/doc-src/IsarAdvanced/Codegen/Thy/examples/Codegen.hs Fri Jan 26 09:24:35 2007 +0100
@@ -10,7 +10,7 @@
heada (y : xs) = y;
heada [] = Codegen.nulla;
-null_option :: Maybe b;
+null_option :: Maybe a;
null_option = Nothing;
instance Codegen.Null (Maybe b) where {
--- a/doc-src/IsarAdvanced/Codegen/Thy/examples/class.ML Thu Jan 25 16:57:57 2007 +0100
+++ b/doc-src/IsarAdvanced/Codegen/Thy/examples/class.ML Fri Jan 26 09:24:35 2007 +0100
@@ -11,15 +11,15 @@
structure Codegen =
struct
-type 'a null = {null_ : 'a};
-fun null (A_:'a null) = #null_ A_;
+type 'a null = {Codegen__null : 'a};
+fun null (A_:'a null) = #Codegen__null A_;
-fun head (A_:'a null) (y :: xs) = y
- | head (A_:'a null) [] = null A_;
+fun head A_ (y :: xs) = y
+ | head A_ [] = null A_;
-val null_option : 'b option = NONE;
+val null_option : 'a option = NONE;
-fun null_optiona () = {null_ = null_option} : ('b option) null ;;
+fun null_optiona () = {Codegen__null = null_option} : ('b option) null;
val dummy : Nat.nat option =
head (null_optiona ()) [SOME (Nat.Suc Nat.Zero_nat), NONE];
--- a/doc-src/IsarAdvanced/Codegen/Thy/examples/collect_duplicates.ML Thu Jan 25 16:57:57 2007 +0100
+++ b/doc-src/IsarAdvanced/Codegen/Thy/examples/collect_duplicates.ML Fri Jan 26 09:24:35 2007 +0100
@@ -4,29 +4,29 @@
structure Code_Generator =
struct
-type 'a eq = {op_eq_ : 'a -> 'a -> bool};
-fun op_eq (A_:'a eq) = #op_eq_ A_;
+type 'a eq = {Code_Generator__op_eq : 'a -> 'a -> bool};
+fun op_eq (A_:'a eq) = #Code_Generator__op_eq A_;
end; (*struct Code_Generator*)
structure List =
struct
-fun memberl (A_:'a Code_Generator.eq) x (y :: ys) =
+fun memberl A_ x (y :: ys) =
Code_Generator.op_eq A_ x y orelse memberl A_ x ys
- | memberl (A_:'a Code_Generator.eq) x [] = false;
+ | memberl A_ x [] = false;
end; (*struct List*)
structure Codegen =
struct
-fun collect_duplicates (A_:'a Code_Generator.eq) xs ys (z :: zs) =
+fun collect_duplicates A_ xs ys (z :: zs) =
(if List.memberl A_ z xs
then (if List.memberl A_ z ys then collect_duplicates A_ xs ys zs
else collect_duplicates A_ xs (z :: ys) zs)
else collect_duplicates A_ (z :: xs) (z :: ys) zs)
- | collect_duplicates (A_:'a Code_Generator.eq) y ys [] = y;
+ | collect_duplicates A_ y ys [] = y;
end; (*struct Codegen*)
--- a/doc-src/IsarAdvanced/Codegen/Thy/examples/lexicographic.ML Thu Jan 25 16:57:57 2007 +0100
+++ b/doc-src/IsarAdvanced/Codegen/Thy/examples/lexicographic.ML Fri Jan 26 09:24:35 2007 +0100
@@ -1,50 +1,31 @@
structure ROOT =
struct
-structure Code_Generator =
-struct
-
-type 'a eq = {op_eq_ : 'a -> 'a -> bool};
-fun op_eq (A_:'a eq) = #op_eq_ A_;
-
-end; (*struct Code_Generator*)
-
-structure Product_Type =
-struct
-
-fun op_eq_prod (A_:'a Code_Generator.eq) (B_:'b Code_Generator.eq)
- (x1, y1) (x2, y2) =
- Code_Generator.op_eq A_ x1 x2 andalso Code_Generator.op_eq B_ y1 y2;
-
-end; (*struct Product_Type*)
-
structure Orderings =
struct
-type 'a ord = {less_eq_ : 'a -> 'a -> bool, less_ : 'a -> 'a -> bool};
-fun less_eq (A_:'a ord) = #less_eq_ A_;
-fun less (A_:'a ord) = #less_ A_;
+type 'a ord =
+ {Orderings__less_eq : 'a -> 'a -> bool,
+ Orderings__less : 'a -> 'a -> bool};
+fun less_eq (A_:'a ord) = #Orderings__less_eq A_;
+fun less (A_:'a ord) = #Orderings__less A_;
end; (*struct Orderings*)
+structure Code_Generator =
+struct
+
+type 'a eq = {Code_Generator__op_eq : 'a -> 'a -> bool};
+fun op_eq (A_:'a eq) = #Code_Generator__op_eq A_;
+
+end; (*struct Code_Generator*)
+
structure Codegen =
struct
-fun less_prod (B_:'b Code_Generator.eq * 'b Orderings.ord)
- (C_:'c Code_Generator.eq * 'c Orderings.ord) p1 p2 =
- let
- val (x1, y1) = p1;
- val (x2, y2) = p2;
- in
- Orderings.less (#2 B_) x1 x2 orelse
- Code_Generator.op_eq (#1 B_) x1 x2 andalso
- Orderings.less (#2 C_) y1 y2
- end;
-
-fun less_eq_prod (B_:'b Code_Generator.eq * 'b Orderings.ord)
- (C_:'c Code_Generator.eq * 'c Orderings.ord) p1 p2 =
- less_prod ((#1 B_), (#2 B_)) ((#1 C_), (#2 C_)) p1 p2 orelse
- Product_Type.op_eq_prod (#1 B_) (#1 C_) p1 p2;
+fun less_eq_prod (A1_, A2_) B_ (x1, y1) (x2, y2) =
+ Orderings.less A2_ x1 x2 orelse
+ Code_Generator.op_eq A1_ x1 x2 andalso Orderings.less_eq B_ y1 y2;
end; (*struct Codegen*)