# HG changeset patch # User haftmann # Date 1169799875 -3600 # Node ID a63889770d576fadabf374c4dfa011cea5174261 # Parent a2c4861363d5d453d120b0cfc03130e0d36ab596 adjusted manual to improved treatment of overloaded constants diff -r a2c4861363d5 -r a63889770d57 doc-src/IsarAdvanced/Codegen/Thy/Codegen.thy --- 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 \ 'a \ bool" ("(_/ \<^loc>\ _)" [50, 51] 50) - fixes less :: "'a \ 'a \ bool" ("(_/ \<^loc>< _)" [50, 51] 50) -(*>*) - instance * :: (ord, ord) ord "p1 < p2 \ let (x1 \ 'a\ord, y1 \ 'b\ord) = p1; (x2, y2) = p2 in x1 < x2 \ (x1 = x2 \ y1 < y2)" - "p1 \ p2 \ p1 < p2 \ (p1 \ 'a\ord \ 'b\ord) = p2" .. + "p1 \ p2 \ let (x1 \ 'a\ord, y1 \ 'b\ord) = p1; (x2, y2) = p2 in + x1 < x2 \ (x1 = x2 \ y1 \ y2)" .. -(*<*) -hide "class" ord -hide const less_eq less -setup {* Sign.parent_path *} -(*>*) +lemma ord_prod [code func]: + "(x1 \ 'a\ord, y1 \ 'b\ord) < (x2, y2) \ x1 < x2 \ (x1 = x2 \ y1 < y2)" + "(x1 \ 'a\ord, y1 \ 'b\ord) \ (x2, y2) \ x1 < x2 \ (x1 = x2 \ y1 \ 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 \ let (x1 \ 'a\{eq, ord}, y1 \ 'b\{eq, ord}) = p1; (x2, y2) = p2 in - x1 < x2 \ (x1 = x2 \ y1 < y2)" - "p1 \ p2 \ p1 < p2 \ (p1 \ 'a\{eq, ord} \ 'b\{eq, ord}) = p2" .. +(*<*) +declare ord_prod [code del] +(*>*) + +lemma ord_prod_code [code func]: + "(x1 \ 'a\{ord, eq}, y1 \ 'b\ord) < (x2, y2) \ x1 < x2 \ (x1 = x2 \ y1 < y2)" + "(x1 \ 'a\{ord, eq}, y1 \ 'b\ord) \ (x2, y2) \ x1 < x2 \ (x1 = x2 \ y1 \ y2)" + unfolding ord_prod by rule+ text {* Then code generation succeeds: *} -code_gen "op \ \ 'a\{eq, ord} \ 'b\{eq, ord} \ 'a \ 'b \ bool" +code_gen "op \ \ 'a\{eq, ord} \ 'b\ord \ 'a \ 'b \ 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 "\"}: + The code generator would produce + an additional instance, which of course is rejected. + To suppress this additional instance, use + @{text "\"}: *} code_instance %tt bar :: eq diff -r a2c4861363d5 -r a63889770d57 doc-src/IsarAdvanced/Codegen/Thy/document/Codegen.tex --- 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% diff -r a2c4861363d5 -r a63889770d57 doc-src/IsarAdvanced/Codegen/Thy/examples/Codegen.hs --- 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 { diff -r a2c4861363d5 -r a63889770d57 doc-src/IsarAdvanced/Codegen/Thy/examples/class.ML --- 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]; diff -r a2c4861363d5 -r a63889770d57 doc-src/IsarAdvanced/Codegen/Thy/examples/collect_duplicates.ML --- 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*) diff -r a2c4861363d5 -r a63889770d57 doc-src/IsarAdvanced/Codegen/Thy/examples/lexicographic.ML --- 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*)