# HG changeset patch # User haftmann # Date 1174382611 -3600 # Node ID de15ea8fb348bdadf99971f0ac32d630079f3ff0 # Parent 110f7f6f8a5dc938a5ff7301e4f6a7e3f7cea1a6 updated code generation sections diff -r 110f7f6f8a5d -r de15ea8fb348 doc-src/IsarAdvanced/Classes/Thy/Classes.thy --- a/doc-src/IsarAdvanced/Classes/Thy/Classes.thy Tue Mar 20 08:27:23 2007 +0100 +++ b/doc-src/IsarAdvanced/Classes/Thy/Classes.thy Tue Mar 20 10:23:31 2007 +0100 @@ -12,17 +12,17 @@ syntax "_alpha" :: "type" ("\") - "_alpha_ofsort" :: "sort \ type" ("\()::_" [0] 1000) + "_alpha_ofsort" :: "sort \ type" ("\()\_" [0] 1000) "_beta" :: "type" ("\") - "_beta_ofsort" :: "sort \ type" ("\()::_" [0] 1000) + "_beta_ofsort" :: "sort \ type" ("\()\_" [0] 1000) "_gamma" :: "type" ("\") - "_gamma_ofsort" :: "sort \ type" ("\()::_" [0] 1000) + "_gamma_ofsort" :: "sort \ type" ("\()\_" [0] 1000) "_alpha_f" :: "type" ("\\<^sub>f") - "_alpha_f_ofsort" :: "sort \ type" ("\\<^sub>f()::_" [0] 1000) + "_alpha_f_ofsort" :: "sort \ type" ("\\<^sub>f()\_" [0] 1000) "_beta_f" :: "type" ("\\<^sub>f") - "_beta_f_ofsort" :: "sort \ type" ("\\<^sub>f()::_" [0] 1000) + "_beta_f_ofsort" :: "sort \ type" ("\\<^sub>f()\_" [0] 1000) "_gamma_f" :: "type" ("\\<^sub>f") - "_gamma_ofsort_f" :: "sort \ type" ("\\<^sub>f()::_" [0] 1000) + "_gamma_ofsort_f" :: "sort \ type" ("\\<^sub>f()\_" [0] 1000) parse_ast_translation {* let @@ -171,9 +171,9 @@ "\"}), the \qn{logical} part specifies properties on them (@{text "\"}). The local @{text "\"} and @{text "\"} are lifted to the theory toplevel, yielding the global - operation @{term [source] "mult :: \::semigroup \ \ \ \"} and the + operation @{term [source] "mult \ \\semigroup \ \ \ \"} and the global theorem @{text "semigroup.assoc:"}~@{prop [source] "\x y - z::\::semigroup. (x \ y) \ z = x \ (y \ z)"}. + z \ \\semigroup. (x \ y) \ z = x \ (y \ z)"}. *} @@ -186,7 +186,7 @@ *} instance int :: semigroup - mult_int_def: "\i j :: int. i \ j \ i + j" + mult_int_def: "\i j \ int. i \ j \ i + j" proof fix i j k :: int have "(i + j) + k = i + (j + k)" by simp then show "(i \ j) \ k = i \ (j \ k)" unfolding mult_int_def . @@ -365,7 +365,7 @@ text {* This give you at hand the full power of the Isabelle module system; conclusions in locale @{text idem} are implicitly propagated - to class @{idem}. + to class @{text idem}. *} subsection {* Abstract reasoning *} @@ -392,10 +392,10 @@ \noindent Here the \qt{@{text "\ group"}} target specification indicates that the result is recorded within that context for later use. This local theorem is also lifted to the global one @{text - "group.left_cancel:"} @{prop [source] "\x y z::\::group. x \ y = x \ + "group.left_cancel:"} @{prop [source] "\x y z \ \\group. x \ y = x \ z \ y = z"}. Since type @{text "int"} has been made an instance of @{text "group"} before, we may refer to that fact as well: @{prop - [source] "\x y z::int. x \ y = x \ z \ y = z"}. + [source] "\x y z \ int. x \ y = x \ z \ y = z"}. *} @@ -439,7 +439,7 @@ fun pow_nat :: "nat \ \\monoidl \ \\monoidl" where "pow_nat 0 x = \" - "pow_nat (Suc n) x = x \ pow_nat n x" + | "pow_nat (Suc n) x = x \ pow_nat n x" definition pow_int :: "int \ \\group \ \\group" where @@ -478,8 +478,7 @@ text {* -(* subsection {* Syntactic classes *} -*) +subsection {* Syntactic classes *} *} *) diff -r 110f7f6f8a5d -r de15ea8fb348 doc-src/IsarAdvanced/Classes/Thy/code_examples/classes.ML --- a/doc-src/IsarAdvanced/Classes/Thy/code_examples/classes.ML Tue Mar 20 08:27:23 2007 +0100 +++ b/doc-src/IsarAdvanced/Classes/Thy/code_examples/classes.ML Tue Mar 20 10:23:31 2007 +0100 @@ -17,28 +17,22 @@ fun nat i = nat_aux Nat.Zero_nat i; -fun op_eq_bit false false = true - | op_eq_bit true true = true - | op_eq_bit false true = false - | op_eq_bit true false = false; - end; (*struct Integer*) structure Classes = struct -type 'a semigroup = {Classes__mult : 'a -> 'a -> 'a}; -fun mult (A_:'a semigroup) = #Classes__mult A_; +type 'a semigroup = {mult : 'a -> 'a -> 'a}; +fun mult (A_:'a semigroup) = #mult A_; type 'a monoidl = - {Classes__monoidl_semigroup : 'a semigroup, Classes__neutral : 'a}; + {Classes__monoidl_semigroup : 'a semigroup, neutral : 'a}; fun monoidl_semigroup (A_:'a monoidl) = #Classes__monoidl_semigroup A_; -fun neutral (A_:'a monoidl) = #Classes__neutral A_; +fun neutral (A_:'a monoidl) = #neutral A_; -type 'a group = - {Classes__group_monoidl : 'a monoidl, Classes__inverse : 'a -> 'a}; +type 'a group = {Classes__group_monoidl : 'a monoidl, inverse : 'a -> 'a}; fun group_monoidl (A_:'a group) = #Classes__group_monoidl A_; -fun inverse (A_:'a group) = #Classes__inverse A_; +fun inverse (A_:'a group) = #inverse A_; fun inverse_int i = IntInf.~ i; @@ -46,15 +40,14 @@ fun mult_int i j = IntInf.+ (i, j); -val semigroup_int = {Classes__mult = mult_int} : IntInf.int semigroup; +val semigroup_int = {mult = mult_int} : IntInf.int semigroup; val monoidl_int = - {Classes__monoidl_semigroup = semigroup_int, - Classes__neutral = neutral_int} - : IntInf.int monoidl; + {Classes__monoidl_semigroup = semigroup_int, neutral = neutral_int} : + IntInf.int monoidl; val group_int = - {Classes__group_monoidl = monoidl_int, Classes__inverse = inverse_int} : + {Classes__group_monoidl = monoidl_int, inverse = inverse_int} : IntInf.int group; fun pow_nat A_ (Nat.Suc n) x = diff -r 110f7f6f8a5d -r de15ea8fb348 doc-src/IsarAdvanced/Classes/Thy/document/Classes.tex --- a/doc-src/IsarAdvanced/Classes/Thy/document/Classes.tex Tue Mar 20 08:27:23 2007 +0100 +++ b/doc-src/IsarAdvanced/Classes/Thy/document/Classes.tex Tue Mar 20 10:23:31 2007 +0100 @@ -5,33 +5,23 @@ \isadelimtheory \isanewline \isanewline -\isanewline % \endisadelimtheory % \isatagtheory -\isacommand{theory}\isamarkupfalse% -\ Classes\isanewline -\isakeyword{imports}\ Main\isanewline -\isakeyword{begin}% +% \endisatagtheory {\isafoldtheory}% % \isadelimtheory -\isanewline % \endisadelimtheory % \isadelimML -\isanewline % \endisadelimML % \isatagML -\isacommand{ML}\isamarkupfalse% -\ {\isacharverbatimopen}\isanewline -CodegenSerializer{\isachardot}code{\isacharunderscore}width\ {\isacharcolon}{\isacharequal}\ {\isadigit{7}}{\isadigit{4}}{\isacharsemicolon}\isanewline -{\isacharverbatimclose}\isanewline % \endisatagML {\isafoldML}% @@ -112,7 +102,7 @@ \hspace*{4ex}\isa{trans{\isacharcolon}\ eq\ x\ y\ {\isasymand}\ eq\ y\ z\ {\isasymlongrightarrow}\ eq\ x\ z} \medskip From a theoretic point of view, type classes are leightweight - modules; indeed, Haskell type classes may be emulated by + modules; Haskell type classes may be emulated by SML functors \cite{classes_modules}. Isabelle/Isar offers a discipline of type classes which brings all those aspects together: @@ -155,15 +145,15 @@ \end{isamarkuptext}% \isamarkuptrue% \ \ \ \ \isacommand{class}\isamarkupfalse% -\ semigroup\ {\isacharequal}\isanewline +\ semigroup\ {\isacharequal}\ type\ {\isacharplus}\isanewline \ \ \ \ \ \ \isakeyword{fixes}\ mult\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequoteopen}{\isasymalpha}\ {\isasymRightarrow}\ {\isasymalpha}\ {\isasymRightarrow}\ {\isasymalpha}{\isachardoublequoteclose}\ \ \ \ {\isacharparenleft}\isakeyword{infixl}\ {\isachardoublequoteopen}\isactrlloc {\isasymotimes}{\isachardoublequoteclose}\ {\isadigit{7}}{\isadigit{0}}{\isacharparenright}\isanewline \ \ \ \ \ \ \isakeyword{assumes}\ assoc{\isacharcolon}\ {\isachardoublequoteopen}{\isacharparenleft}x\ \isactrlloc {\isasymotimes}\ y{\isacharparenright}\ \isactrlloc {\isasymotimes}\ z\ {\isacharequal}\ x\ \isactrlloc {\isasymotimes}\ {\isacharparenleft}y\ \isactrlloc {\isasymotimes}\ z{\isacharparenright}{\isachardoublequoteclose}% \begin{isamarkuptext}% \noindent This \isa{{\isasymCLASS}} specification consists of two parts: the \qn{operational} part names the class operation (\isa{{\isasymFIXES}}), the \qn{logical} part specifies properties on them (\isa{{\isasymASSUMES}}). The local \isa{{\isasymFIXES}} and \isa{{\isasymASSUMES}} are lifted to the theory toplevel, yielding the global - operation \isa{{\isachardoublequote}mult\ {\isacharcolon}{\isacharcolon}\ {\isasymalpha}{\isacharcolon}{\isacharcolon}semigroup\ {\isasymRightarrow}\ {\isasymalpha}\ {\isasymRightarrow}\ {\isasymalpha}{\isachardoublequote}} and the - global theorem \isa{semigroup{\isachardot}assoc{\isacharcolon}}~\isa{{\isachardoublequote}{\isasymAnd}x\ y\ z{\isacharcolon}{\isacharcolon}{\isasymalpha}{\isacharcolon}{\isacharcolon}semigroup{\isachardot}\ {\isacharparenleft}x\ {\isasymotimes}\ y{\isacharparenright}\ {\isasymotimes}\ z\ {\isacharequal}\ x\ {\isasymotimes}\ {\isacharparenleft}y\ {\isasymotimes}\ z{\isacharparenright}{\isachardoublequote}}.% + operation \isa{{\isachardoublequote}mult\ {\isasymColon}\ {\isasymalpha}{\isasymColon}semigroup\ {\isasymRightarrow}\ {\isasymalpha}\ {\isasymRightarrow}\ {\isasymalpha}{\isachardoublequote}} and the + global theorem \isa{semigroup{\isachardot}assoc{\isacharcolon}}~\isa{{\isachardoublequote}{\isasymAnd}x\ y\ z\ {\isasymColon}\ {\isasymalpha}{\isasymColon}semigroup{\isachardot}\ {\isacharparenleft}x\ {\isasymotimes}\ y{\isacharparenright}\ {\isasymotimes}\ z\ {\isacharequal}\ x\ {\isasymotimes}\ {\isacharparenleft}y\ {\isasymotimes}\ z{\isacharparenright}{\isachardoublequote}}.% \end{isamarkuptext}% \isamarkuptrue% % @@ -179,7 +169,7 @@ \isamarkuptrue% \ \ \ \ \isacommand{instance}\isamarkupfalse% \ int\ {\isacharcolon}{\isacharcolon}\ semigroup\isanewline -\ \ \ \ \ \ mult{\isacharunderscore}int{\isacharunderscore}def{\isacharcolon}\ {\isachardoublequoteopen}{\isasymAnd}i\ j\ {\isacharcolon}{\isacharcolon}\ int{\isachardot}\ i\ {\isasymotimes}\ j\ {\isasymequiv}\ i\ {\isacharplus}\ j{\isachardoublequoteclose}\isanewline +\ \ \ \ \ \ mult{\isacharunderscore}int{\isacharunderscore}def{\isacharcolon}\ {\isachardoublequoteopen}{\isasymAnd}i\ j\ {\isasymColon}\ int{\isachardot}\ i\ {\isasymotimes}\ j\ {\isasymequiv}\ i\ {\isacharplus}\ j{\isachardoublequoteclose}\isanewline % \isadelimproof \ \ \ \ % @@ -380,7 +370,7 @@ \ {\isacharminus}\isanewline \ \ \ \ \ \ \ \ \isacommand{from}\isamarkupfalse% \ mult{\isacharunderscore}list{\isacharunderscore}def\ \isacommand{have}\isamarkupfalse% -\ {\isachardoublequoteopen}{\isasymAnd}xs\ ys{\isasymColon}{\isacharprime}a\ list{\isachardot}\ xs\ {\isasymotimes}\ ys\ {\isasymequiv}\ xs\ {\isacharat}\ ys{\isachardoublequoteclose}\ \isacommand{{\isachardot}}\isamarkupfalse% +\ {\isachardoublequoteopen}{\isasymAnd}xs\ ys{\isasymColon}{\isasymalpha}\ list{\isachardot}\ xs\ {\isasymotimes}\ ys\ {\isasymequiv}\ xs\ {\isacharat}\ ys{\isachardoublequoteclose}\ \isacommand{{\isachardot}}\isamarkupfalse% \isanewline \ \ \ \ \ \ \ \ \isacommand{moreover}\isamarkupfalse% \ \isacommand{from}\isamarkupfalse% @@ -454,7 +444,7 @@ \ \ \ \ \ \ \ \ \isacommand{moreover}\isamarkupfalse% \ \isacommand{from}\isamarkupfalse% \ mult{\isacharunderscore}list{\isacharunderscore}def\ neutral{\isacharunderscore}list{\isacharunderscore}def\ \isacommand{have}\isamarkupfalse% -\ {\isachardoublequoteopen}{\isasymone}\ {\isasymequiv}\ {\isacharbrackleft}{\isacharbrackright}{\isasymColon}{\isacharprime}a\ list{\isachardoublequoteclose}\ \isacommand{by}\isamarkupfalse% +\ {\isachardoublequoteopen}{\isasymone}\ {\isasymequiv}\ {\isacharbrackleft}{\isacharbrackright}{\isasymColon}{\isasymalpha}\ list{\isachardoublequoteclose}\ \isacommand{by}\isamarkupfalse% \ simp\isanewline \ \ \ \ \ \ \ \ \isacommand{ultimately}\isamarkupfalse% \ \isacommand{show}\isamarkupfalse% @@ -520,7 +510,88 @@ \isamarkuptrue% % \begin{isamarkuptext}% +The example above gives an impression how Isar type classes work + in practice. As stated in the introduction, classes also provide + a link to Isar's locale system. Indeed, the logical core of a class + is nothing else than a locale:% +\end{isamarkuptext}% +\isamarkuptrue% +\isacommand{class}\isamarkupfalse% +\ idem\ {\isacharequal}\ type\ {\isacharplus}\isanewline +\ \ \isakeyword{fixes}\ f\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequoteopen}{\isasymalpha}\ {\isasymRightarrow}\ {\isasymalpha}{\isachardoublequoteclose}\isanewline +\ \ \isakeyword{assumes}\ idem{\isacharcolon}\ {\isachardoublequoteopen}f\ {\isacharparenleft}f\ x{\isacharparenright}\ {\isacharequal}\ f\ x{\isachardoublequoteclose}% +\begin{isamarkuptext}% +\noindent essentially introduces the locale% +\end{isamarkuptext}% +\isamarkuptrue% % +\isadelimML +% +\endisadelimML +% +\isatagML +% +\endisatagML +{\isafoldML}% +% +\isadelimML +% +\endisadelimML +\isanewline +\isacommand{locale}\isamarkupfalse% +\ idem\ {\isacharequal}\isanewline +\ \ \isakeyword{fixes}\ f\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequoteopen}{\isasymalpha}\ {\isasymRightarrow}\ {\isasymalpha}{\isachardoublequoteclose}\isanewline +\ \ \isakeyword{assumes}\ idem{\isacharcolon}\ {\isachardoublequoteopen}f\ {\isacharparenleft}f\ x{\isacharparenright}\ {\isacharequal}\ f\ x{\isachardoublequoteclose}% +\begin{isamarkuptext}% +\noindent together with corresponding constant(s) and axclass% +\end{isamarkuptext}% +\isamarkuptrue% +\isacommand{consts}\isamarkupfalse% +\ f\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequoteopen}{\isasymalpha}\ {\isasymRightarrow}\ {\isasymalpha}{\isachardoublequoteclose}\isanewline +\isanewline +\isacommand{axclass}\isamarkupfalse% +\ idem\ {\isacharless}\ type\isanewline +\ \ idem{\isacharcolon}\ {\isachardoublequoteopen}f\ {\isacharparenleft}f\ x{\isacharparenright}\ {\isacharequal}\ f\ x{\isachardoublequoteclose}% +\begin{isamarkuptext}% +This axclass is coupled to the locale by means of an interpretation:% +\end{isamarkuptext}% +\isamarkuptrue% +\isacommand{interpretation}\isamarkupfalse% +\ idem{\isacharunderscore}class{\isacharcolon}\isanewline +\ \ idem\ {\isacharbrackleft}{\isachardoublequoteopen}f\ {\isasymColon}\ {\isacharparenleft}{\isacharprime}a{\isasymColon}idem{\isacharparenright}\ {\isasymRightarrow}\ {\isasymalpha}{\isachardoublequoteclose}{\isacharbrackright}\isanewline +% +\isadelimproof +% +\endisadelimproof +% +\isatagproof +\isacommand{by}\isamarkupfalse% +\ unfold{\isacharunderscore}locales\ {\isacharparenleft}rule\ idem{\isacharparenright}\isanewline +% +\endisatagproof +{\isafoldproof}% +% +\isadelimproof +% +\endisadelimproof +% +\isadelimML +% +\endisadelimML +% +\isatagML +% +\endisatagML +{\isafoldML}% +% +\isadelimML +% +\endisadelimML +% +\begin{isamarkuptext}% +This give you at hand the full power of the Isabelle module system; + conclusions in locale \isa{idem} are implicitly propagated + to class \isa{idem}.% \end{isamarkuptext}% \isamarkuptrue% % @@ -529,7 +600,7 @@ \isamarkuptrue% % \begin{isamarkuptext}% -Abstract theories enable reasoning at a general level, while results +Isabelle locales enable reasoning at a general level, while results are implicitly transferred to all instances. For example, we can now establish the \isa{left{\isacharunderscore}cancel} lemma for groups, which states that the function \isa{{\isacharparenleft}x\ {\isasymcirc}{\isacharparenright}} is injective:% @@ -547,16 +618,16 @@ \isanewline \ \ \ \ \isacommand{assume}\isamarkupfalse% \ {\isachardoublequoteopen}x\ \isactrlloc {\isasymotimes}\ y\ {\isacharequal}\ x\ \isactrlloc {\isasymotimes}\ z{\isachardoublequoteclose}\isanewline -\ \ \ \ \ \ \ \ \isacommand{then}\isamarkupfalse% +\ \ \ \ \ \ \isacommand{then}\isamarkupfalse% \ \isacommand{have}\isamarkupfalse% \ {\isachardoublequoteopen}x\isactrlloc {\isasymdiv}\ \isactrlloc {\isasymotimes}\ {\isacharparenleft}x\ \isactrlloc {\isasymotimes}\ y{\isacharparenright}\ {\isacharequal}\ x\isactrlloc {\isasymdiv}\ \isactrlloc {\isasymotimes}\ {\isacharparenleft}x\ \isactrlloc {\isasymotimes}\ z{\isacharparenright}{\isachardoublequoteclose}\ \isacommand{by}\isamarkupfalse% \ simp\isanewline -\ \ \ \ \ \ \ \ \isacommand{then}\isamarkupfalse% +\ \ \ \ \ \ \isacommand{then}\isamarkupfalse% \ \isacommand{have}\isamarkupfalse% \ {\isachardoublequoteopen}{\isacharparenleft}x\isactrlloc {\isasymdiv}\ \isactrlloc {\isasymotimes}\ x{\isacharparenright}\ \isactrlloc {\isasymotimes}\ y\ {\isacharequal}\ {\isacharparenleft}x\isactrlloc {\isasymdiv}\ \isactrlloc {\isasymotimes}\ x{\isacharparenright}\ \isactrlloc {\isasymotimes}\ z{\isachardoublequoteclose}\ \isacommand{using}\isamarkupfalse% \ assoc\ \isacommand{by}\isamarkupfalse% \ simp\isanewline -\ \ \ \ \ \ \ \ \isacommand{then}\isamarkupfalse% +\ \ \ \ \ \ \isacommand{then}\isamarkupfalse% \ \isacommand{show}\isamarkupfalse% \ {\isachardoublequoteopen}y\ {\isacharequal}\ z{\isachardoublequoteclose}\ \isacommand{using}\isamarkupfalse% \ neutl\ \isakeyword{and}\ invl\ \isacommand{by}\isamarkupfalse% @@ -565,7 +636,7 @@ \isanewline \ \ \ \ \isacommand{assume}\isamarkupfalse% \ {\isachardoublequoteopen}y\ {\isacharequal}\ z{\isachardoublequoteclose}\isanewline -\ \ \ \ \ \ \ \ \isacommand{then}\isamarkupfalse% +\ \ \ \ \ \ \isacommand{then}\isamarkupfalse% \ \isacommand{show}\isamarkupfalse% \ {\isachardoublequoteopen}x\ \isactrlloc {\isasymotimes}\ y\ {\isacharequal}\ x\ \isactrlloc {\isasymotimes}\ z{\isachardoublequoteclose}\ \isacommand{by}\isamarkupfalse% \ simp\isanewline @@ -581,8 +652,8 @@ \begin{isamarkuptext}% \noindent Here the \qt{\isa{{\isasymIN}\ group}} target specification indicates that the result is recorded within that context for later - use. This local theorem is also lifted to the global one \isa{group{\isachardot}left{\isacharunderscore}cancel{\isacharcolon}} \isa{{\isachardoublequote}{\isasymAnd}x\ y\ z{\isacharcolon}{\isacharcolon}{\isasymalpha}{\isacharcolon}{\isacharcolon}group{\isachardot}\ x\ {\isasymotimes}\ y\ {\isacharequal}\ x\ {\isasymotimes}\ z\ {\isasymlongleftrightarrow}\ y\ {\isacharequal}\ z{\isachardoublequote}}. Since type \isa{int} has been made an instance of - \isa{group} before, we may refer to that fact as well: \isa{{\isachardoublequote}{\isasymAnd}x\ y\ z{\isacharcolon}{\isacharcolon}int{\isachardot}\ x\ {\isasymotimes}\ y\ {\isacharequal}\ x\ {\isasymotimes}\ z\ {\isasymlongleftrightarrow}\ y\ {\isacharequal}\ z{\isachardoublequote}}.% + use. This local theorem is also lifted to the global one \isa{group{\isachardot}left{\isacharunderscore}cancel{\isacharcolon}} \isa{{\isachardoublequote}{\isasymAnd}x\ y\ z\ {\isasymColon}\ {\isasymalpha}{\isasymColon}group{\isachardot}\ x\ {\isasymotimes}\ y\ {\isacharequal}\ x\ {\isasymotimes}\ z\ {\isasymlongleftrightarrow}\ y\ {\isacharequal}\ z{\isachardoublequote}}. Since type \isa{int} has been made an instance of + \isa{group} before, we may refer to that fact as well: \isa{{\isachardoublequote}{\isasymAnd}x\ y\ z\ {\isasymColon}\ int{\isachardot}\ x\ {\isasymotimes}\ y\ {\isacharequal}\ x\ {\isasymotimes}\ z\ {\isasymlongleftrightarrow}\ y\ {\isacharequal}\ z{\isachardoublequote}}.% \end{isamarkuptext}% \isamarkuptrue% % @@ -608,13 +679,13 @@ \isamarkuptrue% \ \ \ \ \isacommand{fun}\isamarkupfalse% \isanewline -\ \ \ \ \ \ pow{\isacharunderscore}nat\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequoteopen}nat\ {\isasymRightarrow}\ {\isacharprime}a{\isasymColon}monoidl\ {\isasymRightarrow}\ {\isacharprime}a{\isasymColon}monoidl{\isachardoublequoteclose}\ \isakeyword{where}\isanewline +\ \ \ \ \ \ pow{\isacharunderscore}nat\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequoteopen}nat\ {\isasymRightarrow}\ {\isasymalpha}{\isasymColon}monoidl\ {\isasymRightarrow}\ {\isasymalpha}{\isasymColon}monoidl{\isachardoublequoteclose}\ \isakeyword{where}\isanewline \ \ \ \ \ \ {\isachardoublequoteopen}pow{\isacharunderscore}nat\ {\isadigit{0}}\ x\ {\isacharequal}\ {\isasymone}{\isachardoublequoteclose}\isanewline -\ \ \ \ \ \ {\isachardoublequoteopen}pow{\isacharunderscore}nat\ {\isacharparenleft}Suc\ n{\isacharparenright}\ x\ {\isacharequal}\ x\ {\isasymotimes}\ pow{\isacharunderscore}nat\ n\ x{\isachardoublequoteclose}\isanewline +\ \ \ \ \ \ {\isacharbar}\ {\isachardoublequoteopen}pow{\isacharunderscore}nat\ {\isacharparenleft}Suc\ n{\isacharparenright}\ x\ {\isacharequal}\ x\ {\isasymotimes}\ pow{\isacharunderscore}nat\ n\ x{\isachardoublequoteclose}\isanewline \isanewline \ \ \ \ \isacommand{definition}\isamarkupfalse% \isanewline -\ \ \ \ \ \ pow{\isacharunderscore}int\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequoteopen}int\ {\isasymRightarrow}\ {\isacharprime}a{\isasymColon}group\ {\isasymRightarrow}\ {\isacharprime}a{\isasymColon}group{\isachardoublequoteclose}\ \isakeyword{where}\isanewline +\ \ \ \ \ \ pow{\isacharunderscore}int\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequoteopen}int\ {\isasymRightarrow}\ {\isasymalpha}{\isasymColon}group\ {\isasymRightarrow}\ {\isasymalpha}{\isasymColon}group{\isachardoublequoteclose}\ \isakeyword{where}\isanewline \ \ \ \ \ \ {\isachardoublequoteopen}pow{\isacharunderscore}int\ k\ x\ {\isacharequal}\ {\isacharparenleft}if\ k\ {\isachargreater}{\isacharequal}\ {\isadigit{0}}\isanewline \ \ \ \ \ \ \ \ then\ pow{\isacharunderscore}nat\ {\isacharparenleft}nat\ k{\isacharparenright}\ x\isanewline \ \ \ \ \ \ \ \ else\ {\isacharparenleft}pow{\isacharunderscore}nat\ {\isacharparenleft}nat\ {\isacharparenleft}{\isacharminus}\ k{\isacharparenright}{\isacharparenright}\ x{\isacharparenright}{\isasymdiv}{\isacharparenright}{\isachardoublequoteclose}\isanewline diff -r 110f7f6f8a5d -r de15ea8fb348 doc-src/IsarAdvanced/Codegen/Thy/Codegen.thy --- a/doc-src/IsarAdvanced/Codegen/Thy/Codegen.thy Tue Mar 20 08:27:23 2007 +0100 +++ b/doc-src/IsarAdvanced/Codegen/Thy/Codegen.thy Tue Mar 20 10:23:31 2007 +0100 @@ -80,6 +80,40 @@ *} +subsection {* An exmaple: a simple theory of search trees *} + +datatype ('a, 'b) searchtree = Leaf "'a\linorder" 'b + | Branch "('a, 'b) searchtree" "'a" "('a, 'b) searchtree" + +fun + find :: "('a\linorder, 'b) searchtree \ 'a \ 'b option" where + "find (Leaf key val) it = (if it = key then Some val else None)" + | "find (Branch t1 key t2) it = (if it \ key then find t1 it else find t2 it)" + +fun + update :: "'a\linorder \ 'b \ ('a, 'b) searchtree \ ('a, 'b) searchtree" where + "update (it, entry) (Leaf key val) = ( + if it = key then Leaf key entry + else if it \ key + then Branch (Leaf it entry) it (Leaf key val) + else Branch (Leaf key val) it (Leaf it entry) + )" + | "update (it, entry) (Branch t1 key t2) = ( + if it \ key + then (Branch (update (it, entry) t1) key t2) + else (Branch t1 key (update (it, entry) t2)) + )" + +fun + example :: "nat \ (nat, string) searchtree" where + "example n = update (n, ''bar'') (Leaf 0 ''foo'')" + +code_gen example (*<*)(SML #)(*>*)(SML "examples/tree.ML") + +text {* + \lstsml{Thy/examples/tree.ML} +*} + subsection {* Code generation process *} text {* @@ -115,7 +149,7 @@ specifications into equivalent but executable counterparts. The result is a structured collection of \qn{code theorems}. - \item These \qn{code theorems} then are extracted + \item These \qn{code theorems} then are \qn{translated} into an Haskell-like intermediate language. @@ -1175,9 +1209,8 @@ @{index_ML CodegenData.del_preproc: "string -> theory -> theory"} \\ @{index_ML CodegenData.add_datatype: "string * ((string * sort) list * (string * typ list) list) -> theory -> theory"} \\ - @{index_ML CodegenData.del_datatype: "string -> theory -> theory"} \\ @{index_ML CodegenData.get_datatype: "theory -> string - -> ((string * sort) list * (string * typ list) list) option"} \\ + -> (string * sort) list * (string * typ list) list"} \\ @{index_ML CodegenData.get_datatype_of_constr: "theory -> CodegenConsts.const -> string option"} \end{mldecls} @@ -1225,9 +1258,6 @@ constraints and a list of constructors with name and types of arguments. - \item @{ML CodegenData.del_datatype}~@{text "name"}~@{text "thy"} - remove a datatype from executable content, if present. - \item @{ML CodegenData.get_datatype_of_constr}~@{text "thy"}~@{text "const"} returns type constructor corresponding to constructor @{text const}; returns @{text NONE} diff -r 110f7f6f8a5d -r de15ea8fb348 doc-src/IsarAdvanced/Codegen/Thy/document/Codegen.tex --- a/doc-src/IsarAdvanced/Codegen/Thy/document/Codegen.tex Tue Mar 20 08:27:23 2007 +0100 +++ b/doc-src/IsarAdvanced/Codegen/Thy/document/Codegen.tex Tue Mar 20 10:23:31 2007 +0100 @@ -105,6 +105,46 @@ \end{isamarkuptext}% \isamarkuptrue% % +\isamarkupsubsection{An exmaple: a simple theory of search trees% +} +\isamarkuptrue% +\isacommand{datatype}\isamarkupfalse% +\ {\isacharparenleft}{\isacharprime}a{\isacharcomma}\ {\isacharprime}b{\isacharparenright}\ searchtree\ {\isacharequal}\ Leaf\ {\isachardoublequoteopen}{\isacharprime}a{\isasymColon}linorder{\isachardoublequoteclose}\ {\isacharprime}b\isanewline +\ \ {\isacharbar}\ Branch\ {\isachardoublequoteopen}{\isacharparenleft}{\isacharprime}a{\isacharcomma}\ {\isacharprime}b{\isacharparenright}\ searchtree{\isachardoublequoteclose}\ {\isachardoublequoteopen}{\isacharprime}a{\isachardoublequoteclose}\ {\isachardoublequoteopen}{\isacharparenleft}{\isacharprime}a{\isacharcomma}\ {\isacharprime}b{\isacharparenright}\ searchtree{\isachardoublequoteclose}\isanewline +\isanewline +\isacommand{fun}\isamarkupfalse% +\isanewline +\ \ find\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequoteopen}{\isacharparenleft}{\isacharprime}a{\isasymColon}linorder{\isacharcomma}\ {\isacharprime}b{\isacharparenright}\ searchtree\ {\isasymRightarrow}\ {\isacharprime}a\ {\isasymRightarrow}\ {\isacharprime}b\ option{\isachardoublequoteclose}\ \isakeyword{where}\isanewline +\ \ {\isachardoublequoteopen}find\ {\isacharparenleft}Leaf\ key\ val{\isacharparenright}\ it\ {\isacharequal}\ {\isacharparenleft}if\ it\ {\isacharequal}\ key\ then\ Some\ val\ else\ None{\isacharparenright}{\isachardoublequoteclose}\isanewline +\ \ {\isacharbar}\ {\isachardoublequoteopen}find\ {\isacharparenleft}Branch\ t{\isadigit{1}}\ key\ t{\isadigit{2}}{\isacharparenright}\ it\ {\isacharequal}\ {\isacharparenleft}if\ it\ {\isasymle}\ key\ then\ find\ t{\isadigit{1}}\ it\ else\ find\ t{\isadigit{2}}\ it{\isacharparenright}{\isachardoublequoteclose}\isanewline +\isanewline +\isacommand{fun}\isamarkupfalse% +\isanewline +\ \ update\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequoteopen}{\isacharprime}a{\isasymColon}linorder\ {\isasymtimes}\ {\isacharprime}b\ {\isasymRightarrow}\ {\isacharparenleft}{\isacharprime}a{\isacharcomma}\ {\isacharprime}b{\isacharparenright}\ searchtree\ {\isasymRightarrow}\ {\isacharparenleft}{\isacharprime}a{\isacharcomma}\ {\isacharprime}b{\isacharparenright}\ searchtree{\isachardoublequoteclose}\ \isakeyword{where}\isanewline +\ \ {\isachardoublequoteopen}update\ {\isacharparenleft}it{\isacharcomma}\ entry{\isacharparenright}\ {\isacharparenleft}Leaf\ key\ val{\isacharparenright}\ {\isacharequal}\ {\isacharparenleft}\isanewline +\ \ \ \ if\ it\ {\isacharequal}\ key\ then\ Leaf\ key\ entry\isanewline +\ \ \ \ \ \ else\ if\ it\ {\isasymle}\ key\isanewline +\ \ \ \ \ \ then\ Branch\ {\isacharparenleft}Leaf\ it\ entry{\isacharparenright}\ it\ {\isacharparenleft}Leaf\ key\ val{\isacharparenright}\isanewline +\ \ \ \ \ \ else\ Branch\ {\isacharparenleft}Leaf\ key\ val{\isacharparenright}\ it\ {\isacharparenleft}Leaf\ it\ entry{\isacharparenright}\isanewline +\ \ \ {\isacharparenright}{\isachardoublequoteclose}\isanewline +\ \ {\isacharbar}\ {\isachardoublequoteopen}update\ {\isacharparenleft}it{\isacharcomma}\ entry{\isacharparenright}\ {\isacharparenleft}Branch\ t{\isadigit{1}}\ key\ t{\isadigit{2}}{\isacharparenright}\ {\isacharequal}\ {\isacharparenleft}\isanewline +\ \ \ \ if\ it\ {\isasymle}\ key\isanewline +\ \ \ \ \ \ then\ {\isacharparenleft}Branch\ {\isacharparenleft}update\ {\isacharparenleft}it{\isacharcomma}\ entry{\isacharparenright}\ t{\isadigit{1}}{\isacharparenright}\ key\ t{\isadigit{2}}{\isacharparenright}\isanewline +\ \ \ \ \ \ else\ {\isacharparenleft}Branch\ t{\isadigit{1}}\ key\ {\isacharparenleft}update\ {\isacharparenleft}it{\isacharcomma}\ entry{\isacharparenright}\ t{\isadigit{2}}{\isacharparenright}{\isacharparenright}\isanewline +\ \ \ {\isacharparenright}{\isachardoublequoteclose}\isanewline +\isanewline +\isacommand{fun}\isamarkupfalse% +\isanewline +\ \ example\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequoteopen}nat\ {\isasymRightarrow}\ {\isacharparenleft}nat{\isacharcomma}\ string{\isacharparenright}\ searchtree{\isachardoublequoteclose}\ \isakeyword{where}\isanewline +\ \ {\isachardoublequoteopen}example\ n\ {\isacharequal}\ update\ {\isacharparenleft}n{\isacharcomma}\ {\isacharprime}{\isacharprime}bar{\isacharprime}{\isacharprime}{\isacharparenright}\ {\isacharparenleft}Leaf\ {\isadigit{0}}\ {\isacharprime}{\isacharprime}foo{\isacharprime}{\isacharprime}{\isacharparenright}{\isachardoublequoteclose}\isanewline +\isanewline +\isacommand{code{\isacharunderscore}gen}\isamarkupfalse% +\ example\ {\isacharparenleft}SML\ {\isachardoublequoteopen}examples{\isacharslash}tree{\isachardot}ML{\isachardoublequoteclose}{\isacharparenright}% +\begin{isamarkuptext}% +\lstsml{Thy/examples/tree.ML}% +\end{isamarkuptext}% +\isamarkuptrue% +% \isamarkupsubsection{Code generation process% } \isamarkuptrue% @@ -142,7 +182,7 @@ specifications into equivalent but executable counterparts. The result is a structured collection of \qn{code theorems}. - \item These \qn{code theorems} then are extracted + \item These \qn{code theorems} then are \qn{translated} into an Haskell-like intermediate language. @@ -171,14 +211,11 @@ most cases code generation proceeds without further ado:% \end{isamarkuptext}% \isamarkuptrue% -\isacommand{consts}\isamarkupfalse% -\isanewline -\ \ fac\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequoteopen}nat\ {\isasymRightarrow}\ nat{\isachardoublequoteclose}\isanewline +\isacommand{fun}\isamarkupfalse% \isanewline -\isacommand{primrec}\isamarkupfalse% -\isanewline -\ \ {\isachardoublequoteopen}fac\ {\isadigit{0}}\ {\isacharequal}\ {\isadigit{1}}{\isachardoublequoteclose}\isanewline -\ \ {\isachardoublequoteopen}fac\ {\isacharparenleft}Suc\ n{\isacharparenright}\ {\isacharequal}\ Suc\ n\ {\isacharasterisk}\ fac\ n{\isachardoublequoteclose}% +\ \ fac\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequoteopen}nat\ {\isasymRightarrow}\ nat{\isachardoublequoteclose}\ \isakeyword{where}\isanewline +\ \ \ \ {\isachardoublequoteopen}fac\ {\isadigit{0}}\ {\isacharequal}\ {\isadigit{1}}{\isachardoublequoteclose}\isanewline +\ \ {\isacharbar}\ {\isachardoublequoteopen}fac\ {\isacharparenleft}Suc\ n{\isacharparenright}\ {\isacharequal}\ Suc\ n\ {\isacharasterisk}\ fac\ n{\isachardoublequoteclose}% \begin{isamarkuptext}% This executable specification is now turned to SML code:% \end{isamarkuptext}% @@ -419,7 +456,7 @@ \end{isamarkuptext}% \isamarkuptrue% \isacommand{class}\isamarkupfalse% -\ null\ {\isacharequal}\isanewline +\ null\ {\isacharequal}\ type\ {\isacharplus}\isanewline \ \ \isakeyword{fixes}\ null\ {\isacharcolon}{\isacharcolon}\ {\isacharprime}a\isanewline \isanewline \isacommand{consts}\isamarkupfalse% @@ -721,7 +758,8 @@ \isacommand{fun}\isamarkupfalse% \isanewline \ \ in{\isacharunderscore}interval\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequoteopen}nat\ {\isasymtimes}\ nat\ {\isasymRightarrow}\ nat\ {\isasymRightarrow}\ bool{\isachardoublequoteclose}\ \isakeyword{where}\isanewline -\ \ {\isachardoublequoteopen}in{\isacharunderscore}interval\ {\isacharparenleft}k{\isacharcomma}\ l{\isacharparenright}\ n\ {\isasymlongleftrightarrow}\ k\ {\isasymle}\ n\ {\isasymand}\ n\ {\isasymle}\ l{\isachardoublequoteclose}% +\ \ {\isachardoublequoteopen}in{\isacharunderscore}interval\ {\isacharparenleft}k{\isacharcomma}\ l{\isacharparenright}\ n\ {\isasymlongleftrightarrow}\ k\ {\isasymle}\ n\ {\isasymand}\ n\ {\isasymle}\ l{\isachardoublequoteclose}\isanewline +% \isadelimtt % \endisadelimtt @@ -946,12 +984,12 @@ \isacommand{fun}\isamarkupfalse% \isanewline \ \ collect{\isacharunderscore}duplicates\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequoteopen}{\isacharprime}a\ list\ {\isasymRightarrow}\ {\isacharprime}a\ list\ {\isasymRightarrow}\ {\isacharprime}a\ list\ {\isasymRightarrow}\ {\isacharprime}a\ list{\isachardoublequoteclose}\ \isakeyword{where}\isanewline -\ \ {\isachardoublequoteopen}collect{\isacharunderscore}duplicates\ xs\ ys\ {\isacharbrackleft}{\isacharbrackright}\ {\isacharequal}\ xs{\isachardoublequoteclose}\isanewline -\ \ {\isachardoublequoteopen}collect{\isacharunderscore}duplicates\ xs\ ys\ {\isacharparenleft}z{\isacharhash}zs{\isacharparenright}\ {\isacharequal}\ {\isacharparenleft}if\ z\ {\isasymin}\ set\ xs\isanewline -\ \ \ \ then\ if\ z\ {\isasymin}\ set\ ys\isanewline -\ \ \ \ \ \ then\ collect{\isacharunderscore}duplicates\ xs\ ys\ zs\isanewline -\ \ \ \ \ \ else\ collect{\isacharunderscore}duplicates\ xs\ {\isacharparenleft}z{\isacharhash}ys{\isacharparenright}\ zs\isanewline -\ \ \ \ else\ collect{\isacharunderscore}duplicates\ {\isacharparenleft}z{\isacharhash}xs{\isacharparenright}\ {\isacharparenleft}z{\isacharhash}ys{\isacharparenright}\ zs{\isacharparenright}{\isachardoublequoteclose}% +\ \ \ \ {\isachardoublequoteopen}collect{\isacharunderscore}duplicates\ xs\ ys\ {\isacharbrackleft}{\isacharbrackright}\ {\isacharequal}\ xs{\isachardoublequoteclose}\isanewline +\ \ {\isacharbar}\ {\isachardoublequoteopen}collect{\isacharunderscore}duplicates\ xs\ ys\ {\isacharparenleft}z{\isacharhash}zs{\isacharparenright}\ {\isacharequal}\ {\isacharparenleft}if\ z\ {\isasymin}\ set\ xs\isanewline +\ \ \ \ \ \ then\ if\ z\ {\isasymin}\ set\ ys\isanewline +\ \ \ \ \ \ \ \ then\ collect{\isacharunderscore}duplicates\ xs\ ys\ zs\isanewline +\ \ \ \ \ \ \ \ else\ collect{\isacharunderscore}duplicates\ xs\ {\isacharparenleft}z{\isacharhash}ys{\isacharparenright}\ zs\isanewline +\ \ \ \ \ \ else\ collect{\isacharunderscore}duplicates\ {\isacharparenleft}z{\isacharhash}xs{\isacharparenright}\ {\isacharparenleft}z{\isacharhash}ys{\isacharparenright}\ zs{\isacharparenright}{\isachardoublequoteclose}% \begin{isamarkuptext}% The membership test during preprocessing is rewritten, resulting in \isa{op\ mem}, which itself @@ -986,7 +1024,7 @@ \endisadelimML \isanewline \isacommand{class}\isamarkupfalse% -\ eq\ {\isacharparenleft}\isakeyword{attach}\ {\isachardoublequoteopen}op\ {\isacharequal}{\isachardoublequoteclose}{\isacharparenright}\ {\isacharequal}\ \isakeyword{notes}\ reflexive% +\ eq\ {\isacharparenleft}\isakeyword{attach}\ {\isachardoublequoteopen}op\ {\isacharequal}{\isachardoublequoteclose}{\isacharparenright}\ {\isacharequal}\ type% \begin{isamarkuptext}% This merely introduces a class \isa{eq} with corresponding operation \isa{op\ {\isacharequal}}; @@ -1031,10 +1069,11 @@ \isacommand{fun}\isamarkupfalse% \isanewline \ \ lookup\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequoteopen}{\isacharparenleft}key\ {\isasymtimes}\ {\isacharprime}a{\isacharparenright}\ list\ {\isasymRightarrow}\ key\ {\isasymRightarrow}\ {\isacharprime}a\ option{\isachardoublequoteclose}\ \isakeyword{where}\isanewline -\ \ {\isachardoublequoteopen}lookup\ {\isacharbrackleft}{\isacharbrackright}\ l\ {\isacharequal}\ None{\isachardoublequoteclose}\isanewline -\ \ {\isachardoublequoteopen}lookup\ {\isacharparenleft}{\isacharparenleft}k{\isacharcomma}\ v{\isacharparenright}\ {\isacharhash}\ xs{\isacharparenright}\ l\ {\isacharequal}\ {\isacharparenleft}if\ k\ {\isacharequal}\ l\ then\ Some\ v\ else\ lookup\ xs\ l{\isacharparenright}{\isachardoublequoteclose}\isanewline +\ \ \ \ {\isachardoublequoteopen}lookup\ {\isacharbrackleft}{\isacharbrackright}\ l\ {\isacharequal}\ None{\isachardoublequoteclose}\isanewline +\ \ {\isacharbar}\ {\isachardoublequoteopen}lookup\ {\isacharparenleft}{\isacharparenleft}k{\isacharcomma}\ v{\isacharparenright}\ {\isacharhash}\ xs{\isacharparenright}\ l\ {\isacharequal}\ {\isacharparenleft}if\ k\ {\isacharequal}\ l\ then\ Some\ v\ else\ lookup\ xs\ l{\isacharparenright}{\isachardoublequoteclose}\isanewline % \isadelimtt +\isanewline % \endisadelimtt % @@ -1552,8 +1591,9 @@ \isacommand{fun}\isamarkupfalse% \isanewline \ \ dummy{\isacharunderscore}option\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequoteopen}{\isacharprime}a\ list\ {\isasymRightarrow}\ {\isacharprime}a\ option{\isachardoublequoteclose}\ \isakeyword{where}\isanewline -\ \ {\isachardoublequoteopen}dummy{\isacharunderscore}option\ {\isacharparenleft}x{\isacharhash}xs{\isacharparenright}\ {\isacharequal}\ Some\ x{\isachardoublequoteclose}\isanewline -\ \ {\isachardoublequoteopen}dummy{\isacharunderscore}option\ {\isacharbrackleft}{\isacharbrackright}\ {\isacharequal}\ arbitrary{\isachardoublequoteclose}\isanewline +\ \ \ \ {\isachardoublequoteopen}dummy{\isacharunderscore}option\ {\isacharparenleft}x{\isacharhash}xs{\isacharparenright}\ {\isacharequal}\ Some\ x{\isachardoublequoteclose}\isanewline +\ \ {\isacharbar}\ {\isachardoublequoteopen}dummy{\isacharunderscore}option\ {\isacharbrackleft}{\isacharbrackright}\ {\isacharequal}\ arbitrary{\isachardoublequoteclose}\isanewline +\isanewline \isacommand{code{\isacharunderscore}gen}\isamarkupfalse% \ dummy{\isacharunderscore}option\ {\isacharparenleft}SML\ {\isachardoublequoteopen}examples{\isacharslash}arbitrary{\isachardot}ML{\isachardoublequoteclose}{\isacharparenright}% \begin{isamarkuptext}% @@ -1691,11 +1731,10 @@ \indexml{CodegenData.add-preproc}\verb|CodegenData.add_preproc: string * (theory -> thm list -> thm list)|\isasep\isanewline% \verb| -> theory -> theory| \\ \indexml{CodegenData.del-preproc}\verb|CodegenData.del_preproc: string -> theory -> theory| \\ - \indexml{CodegenData.add-datatype}\verb|CodegenData.add_datatype: string * (((string * sort) list * (string * typ list) list)|\isasep\isanewline% -\verb| * thm list Susp.T) -> theory -> theory| \\ - \indexml{CodegenData.del-datatype}\verb|CodegenData.del_datatype: string -> theory -> theory| \\ + \indexml{CodegenData.add-datatype}\verb|CodegenData.add_datatype: string * ((string * sort) list * (string * typ list) list)|\isasep\isanewline% +\verb| -> theory -> theory| \\ \indexml{CodegenData.get-datatype}\verb|CodegenData.get_datatype: theory -> string|\isasep\isanewline% -\verb| -> ((string * sort) list * (string * typ list) list) option| \\ +\verb| -> (string * sort) list * (string * typ list) list| \\ \indexml{CodegenData.get-datatype-of-constr}\verb|CodegenData.get_datatype_of_constr: theory -> CodegenConsts.const -> string option| \end{mldecls} @@ -1736,17 +1775,12 @@ \item \verb|CodegenData.del_preproc|~\isa{name}~\isa{thy} removes generic preprcoessor named \isa{name} from executable content. - \item \verb|CodegenData.add_datatype|~\isa{{\isacharparenleft}name{\isacharcomma}\ {\isacharparenleft}spec{\isacharcomma}\ cert{\isacharparenright}{\isacharparenright}}~\isa{thy} adds + \item \verb|CodegenData.add_datatype|~\isa{{\isacharparenleft}name{\isacharcomma}\ spec{\isacharparenright}}~\isa{thy} adds a datatype to executable content, with type constructor \isa{name} and specification \isa{spec}; \isa{spec} is a pair consisting of a list of type variable with sort constraints and a list of constructors with name - and types of arguments. The addition as datatype - has to be justified giving a certificate of suspended - theorems as witnesses for injectiveness and distinctness. - - \item \verb|CodegenData.del_datatype|~\isa{name}~\isa{thy} - remove a datatype from executable content, if present. + and types of arguments. \item \verb|CodegenData.get_datatype_of_constr|~\isa{thy}~\isa{const} returns type constructor corresponding to diff -r 110f7f6f8a5d -r de15ea8fb348 doc-src/IsarAdvanced/Codegen/Thy/examples/bool_literal.ML --- a/doc-src/IsarAdvanced/Codegen/Thy/examples/bool_literal.ML Tue Mar 20 08:27:23 2007 +0100 +++ b/doc-src/IsarAdvanced/Codegen/Thy/examples/bool_literal.ML Tue Mar 20 10:23:31 2007 +0100 @@ -6,10 +6,10 @@ datatype boola = True | False; -fun op_conj y True = y - | op_conj x False = False - | op_conj True y = y - | op_conj False x = False; +fun op_and y True = y + | op_and x False = False + | op_and True y = y + | op_and False x = False; end; (*struct HOL*) @@ -29,7 +29,7 @@ struct fun in_interval (k, l) n = - HOL.op_conj (Nat.less_eq_nat k n) (Nat.less_eq_nat n l); + HOL.op_and (Nat.less_eq_nat k n) (Nat.less_eq_nat n l); end; (*struct Codegen*) diff -r 110f7f6f8a5d -r de15ea8fb348 doc-src/IsarAdvanced/Codegen/Thy/examples/lexicographic.ML --- a/doc-src/IsarAdvanced/Codegen/Thy/examples/lexicographic.ML Tue Mar 20 08:27:23 2007 +0100 +++ b/doc-src/IsarAdvanced/Codegen/Thy/examples/lexicographic.ML Tue Mar 20 10:23:31 2007 +0100 @@ -21,7 +21,7 @@ structure Codegen = struct -fun less_eq_prod (A1_, A2_) B_ (x1, y1) (x2, y2) = +fun less_eq_times (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;