# HG changeset patch # User haftmann # Date 1177067507 -7200 # Node ID 1bfd75c1f232dd211551e3ba8a4ec41b72f8beda # Parent bff5d59de79bd9f4ece10c1690d3fc7abfd413ab updated diff -r bff5d59de79b -r 1bfd75c1f232 doc-src/IsarAdvanced/Codegen/Thy/Codegen.thy --- a/doc-src/IsarAdvanced/Codegen/Thy/Codegen.thy Fri Apr 20 11:21:53 2007 +0200 +++ b/doc-src/IsarAdvanced/Codegen/Thy/Codegen.thy Fri Apr 20 13:11:47 2007 +0200 @@ -280,14 +280,11 @@ text {* \noindent which displays a table of constant with corresponding defining equations (the additional stuff displayed - shall not bother us for the moment). If this table does - not provide at least one defining - equation for a particular constant, the table of primitive - definitions is searched - whether it provides one. + shall not bother us for the moment). The typical HOL tools are already set up in a way that - function definitions introduced by @{text "\"}, + function definitions introduced by @{text "\"}, + @{text "\"}, @{text "\"}, @{text "\"} @{text "\"} are implicitly propagated to this defining equation table. Specific theorems may be @@ -861,15 +858,17 @@ *} instance * :: (ord, ord) ord - "p1 < p2 \ let (x1 \ 'a\ord, y1 \ 'b\ord) = p1; (x2, y2) = p2 in + less_prod_def: "p1 < p2 \ let (x1 \ 'a\ord, y1 \ 'b\ord) = p1; (x2, y2) = p2 in x1 < x2 \ (x1 = x2 \ y1 < y2)" - "p1 \ p2 \ let (x1 \ 'a\ord, y1 \ 'b\ord) = p1; (x2, y2) = p2 in + less_eq_prod_def: "p1 \ p2 \ let (x1 \ 'a\ord, y1 \ 'b\ord) = p1; (x2, y2) = p2 in x1 < x2 \ (x1 = x2 \ y1 \ y2)" .. +lemmas [code nofunc] = less_prod_def less_eq_prod_def + 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 + unfolding less_prod_def less_eq_prod_def by simp_all text {* Then code generation will fail. Why? The definition @@ -883,7 +882,7 @@ *} (*<*) -declare ord_prod [code del] +lemmas [code nofunc] = ord_prod (*>*) lemma ord_prod_code [code func]: @@ -907,7 +906,10 @@ 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. + are rejected immediately. Consequently, it might be necessary + to delete disturbing theorems in the code theorem table, + as we have done here with the original definitions @{text less_prod_def} + and @{text less_eq_prod_def}. *} subsubsection {* Haskell serialization *} @@ -1002,7 +1004,7 @@ expects dictionaries (namely an \emph{eq} dictionary) but has also been given a customary serialization. - The solution to this dilemma: + \fixme[needs rewrite] The solution to this dilemma: *} lemma [code func]: @@ -1013,9 +1015,7 @@ text {* \lstsml{Thy/examples/dirty_set.ML} - Reflexive defining equations by convention are dropped. - But their presence prevents primitive definitions to be - used as defining equations: + Reflexive defining equations by convention are dropped: *} code_thms insert @@ -1201,12 +1201,12 @@ text %mlref {* \begin{mldecls} - @{index_ML CodegenData.lazy: "(unit -> thm list) -> thm list Susp.T"} + @{index_ML CodegenData.lazy_thms: "(unit -> thm list) -> thm list Susp.T"} \end{mldecls} \begin{description} - \item @{ML CodegenData.lazy}~@{text f} turns an abstract + \item @{ML CodegenData.lazy_thms}~@{text f} turns an abstract theorem computation @{text f} into a suspension of theorems. \end{description} @@ -1294,7 +1294,7 @@ @{index_ML CodegenConsts.eq_const: "CodegenConsts.const * CodegenConsts.const -> bool"} \\ @{index_ML CodegenConsts.read_const: "theory -> string -> CodegenConsts.const"} \\ @{index_ML_structure CodegenConsts.Consttab} \\ - @{index_ML CodegenFunc.typ_func: "thm -> typ"} \\ + @{index_ML CodegenFunc.head_func: "thm -> CodegenConsts.const * typ"} \\ @{index_ML CodegenFunc.rewrite_func: "thm list -> thm -> thm"} \\ \end{mldecls} @@ -1309,8 +1309,8 @@ \item @{ML CodegenConsts.read_const}~@{text thy}~@{text s} reads a constant as a concrete term expression @{text s}. - \item @{ML CodegenFunc.typ_func}~@{text thm} - extracts the type of a constant in a defining equation @{text thm}. + \item @{ML CodegenFunc.head_func}~@{text thm} + extracts the constant and its type from a defining equation @{text thm}. \item @{ML CodegenFunc.rewrite_func}~@{text rews}~@{text thm} rewrites a defining equation @{text thm} with a set of rewrite diff -r bff5d59de79b -r 1bfd75c1f232 doc-src/IsarAdvanced/Codegen/Thy/document/Codegen.tex --- a/doc-src/IsarAdvanced/Codegen/Thy/document/Codegen.tex Fri Apr 20 11:21:53 2007 +0200 +++ b/doc-src/IsarAdvanced/Codegen/Thy/document/Codegen.tex Fri Apr 20 13:11:47 2007 +0200 @@ -332,14 +332,11 @@ \begin{isamarkuptext}% \noindent which displays a table of constant with corresponding defining equations (the additional stuff displayed - shall not bother us for the moment). If this table does - not provide at least one defining - equation for a particular constant, the table of primitive - definitions is searched - whether it provides one. + shall not bother us for the moment). The typical HOL tools are already set up in a way that - function definitions introduced by \isa{{\isasymFUN}}, + function definitions introduced by \isa{{\isasymDEFINITION}}, + \isa{{\isasymFUN}}, \isa{{\isasymFUNCTION}}, \isa{{\isasymPRIMREC}} \isa{{\isasymRECDEF}} are implicitly propagated to this defining equation table. Specific theorems may be @@ -1154,9 +1151,9 @@ \isamarkuptrue% \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 +\ \ less{\isacharunderscore}prod{\isacharunderscore}def{\isacharcolon}\ {\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}\ 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 +\ \ less{\isacharunderscore}eq{\isacharunderscore}prod{\isacharunderscore}def{\isacharcolon}\ {\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 \ % @@ -1173,6 +1170,9 @@ \endisadelimproof \isanewline \isanewline +\isacommand{lemmas}\isamarkupfalse% +\ {\isacharbrackleft}code\ nofunc{\isacharbrackright}\ {\isacharequal}\ less{\isacharunderscore}prod{\isacharunderscore}def\ less{\isacharunderscore}eq{\isacharunderscore}prod{\isacharunderscore}def\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 @@ -1184,7 +1184,7 @@ % \isatagproof \isacommand{unfolding}\isamarkupfalse% -\ {\isachardoublequoteopen}less{\isacharunderscore}eq{\isacharunderscore}{\isacharasterisk}{\isacharunderscore}def{\isachardoublequoteclose}\ {\isachardoublequoteopen}less{\isacharunderscore}{\isacharasterisk}{\isacharunderscore}def{\isachardoublequoteclose}\ \isacommand{by}\isamarkupfalse% +\ less{\isacharunderscore}prod{\isacharunderscore}def\ less{\isacharunderscore}eq{\isacharunderscore}prod{\isacharunderscore}def\ \isacommand{by}\isamarkupfalse% \ simp{\isacharunderscore}all% \endisatagproof {\isafoldproof}% @@ -1242,7 +1242,10 @@ 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.% + are rejected immediately. Consequently, it might be necessary + to delete disturbing theorems in the code theorem table, + as we have done here with the original definitions \isa{less{\isacharunderscore}prod{\isacharunderscore}def} + and \isa{less{\isacharunderscore}eq{\isacharunderscore}prod{\isacharunderscore}def}.% \end{isamarkuptext}% \isamarkuptrue% % @@ -1430,7 +1433,7 @@ expects dictionaries (namely an \emph{eq} dictionary) but has also been given a customary serialization. - The solution to this dilemma:% + \fixme[needs rewrite] The solution to this dilemma:% \end{isamarkuptext}% \isamarkuptrue% \isacommand{lemma}\isamarkupfalse% @@ -1456,9 +1459,7 @@ \begin{isamarkuptext}% \lstsml{Thy/examples/dirty_set.ML} - Reflexive defining equations by convention are dropped. - But their presence prevents primitive definitions to be - used as defining equations:% + Reflexive defining equations by convention are dropped:% \end{isamarkuptext}% \isamarkuptrue% \isacommand{code{\isacharunderscore}thms}\isamarkupfalse% @@ -1697,12 +1698,12 @@ % \begin{isamarkuptext}% \begin{mldecls} - \indexml{CodegenData.lazy}\verb|CodegenData.lazy: (unit -> thm list) -> thm list Susp.T| + \indexml{CodegenData.lazy-thms}\verb|CodegenData.lazy_thms: (unit -> thm list) -> thm list Susp.T| \end{mldecls} \begin{description} - \item \verb|CodegenData.lazy|~\isa{f} turns an abstract + \item \verb|CodegenData.lazy_thms|~\isa{f} turns an abstract theorem computation \isa{f} into a suspension of theorems. \end{description}% @@ -1822,7 +1823,7 @@ \indexml{CodegenConsts.eq-const}\verb|CodegenConsts.eq_const: CodegenConsts.const * CodegenConsts.const -> bool| \\ \indexml{CodegenConsts.read-const}\verb|CodegenConsts.read_const: theory -> string -> CodegenConsts.const| \\ \indexmlstructure{CodegenConsts.Consttab}\verb|structure CodegenConsts.Consttab| \\ - \indexml{CodegenFunc.typ-func}\verb|CodegenFunc.typ_func: thm -> typ| \\ + \indexml{CodegenFunc.head-func}\verb|CodegenFunc.head_func: thm -> CodegenConsts.const * typ| \\ \indexml{CodegenFunc.rewrite-func}\verb|CodegenFunc.rewrite_func: thm list -> thm -> thm| \\ \end{mldecls} @@ -1837,8 +1838,8 @@ \item \verb|CodegenConsts.read_const|~\isa{thy}~\isa{s} reads a constant as a concrete term expression \isa{s}. - \item \verb|CodegenFunc.typ_func|~\isa{thm} - extracts the type of a constant in a defining equation \isa{thm}. + \item \verb|CodegenFunc.head_func|~\isa{thm} + extracts the constant and its type from a defining equation \isa{thm}. \item \verb|CodegenFunc.rewrite_func|~\isa{rews}~\isa{thm} rewrites a defining equation \isa{thm} with a set of rewrite diff -r bff5d59de79b -r 1bfd75c1f232 doc-src/IsarAdvanced/Codegen/Thy/document/isabelle.sty --- a/doc-src/IsarAdvanced/Codegen/Thy/document/isabelle.sty Fri Apr 20 11:21:53 2007 +0200 +++ b/doc-src/IsarAdvanced/Codegen/Thy/document/isabelle.sty Fri Apr 20 13:11:47 2007 +0200 @@ -31,6 +31,7 @@ \newcommand{\isactrlesup}{\egroup\egroup\end{math}\egroup} \newcommand{\isactrlbold}[1]{{\bfseries\upshape\boldmath#1}} \newcommand{\isactrlloc}[1]{{\bfseries\upshape\boldmath#1}} +\newenvironment{isaantiq}{{\isacharat\isacharbraceleft}}{{\isacharbraceright}} \newdimen\isa@parindent\newdimen\isa@parskip diff -r bff5d59de79b -r 1bfd75c1f232 doc-src/IsarAdvanced/Codegen/Thy/examples/Codegen.hs --- a/doc-src/IsarAdvanced/Codegen/Thy/examples/Codegen.hs Fri Apr 20 11:21:53 2007 +0200 +++ b/doc-src/IsarAdvanced/Codegen/Thy/examples/Codegen.hs Fri Apr 20 13:11:47 2007 +0200 @@ -7,7 +7,7 @@ }; heada :: (Codegen.Null a) => [a] -> a; -heada (y : xs) = y; +heada (x : xs) = x; heada [] = Codegen.nulla; null_option :: Maybe a; diff -r bff5d59de79b -r 1bfd75c1f232 doc-src/IsarAdvanced/Codegen/Thy/examples/bool_literal.ML --- a/doc-src/IsarAdvanced/Codegen/Thy/examples/bool_literal.ML Fri Apr 20 11:21:53 2007 +0200 +++ b/doc-src/IsarAdvanced/Codegen/Thy/examples/bool_literal.ML Fri Apr 20 13:11:47 2007 +0200 @@ -6,9 +6,9 @@ datatype boola = True | False; -fun op_and y True = y +fun op_and x True = x | op_and x False = False - | op_and True y = y + | op_and True x = x | op_and False x = False; end; (*struct HOL*) diff -r bff5d59de79b -r 1bfd75c1f232 doc-src/IsarAdvanced/Codegen/Thy/examples/class.ML --- a/doc-src/IsarAdvanced/Codegen/Thy/examples/class.ML Fri Apr 20 11:21:53 2007 +0200 +++ b/doc-src/IsarAdvanced/Codegen/Thy/examples/class.ML Fri Apr 20 13:11:47 2007 +0200 @@ -14,7 +14,7 @@ type 'a null = {null : 'a}; fun null (A_:'a null) = #null A_; -fun head A_ (y :: xs) = y +fun head A_ (x :: xs) = x | head A_ [] = null A_; val null_option : 'a option = NONE; diff -r bff5d59de79b -r 1bfd75c1f232 doc-src/IsarAdvanced/Codegen/Thy/examples/class.ocaml --- a/doc-src/IsarAdvanced/Codegen/Thy/examples/class.ocaml Fri Apr 20 11:21:53 2007 +0200 +++ b/doc-src/IsarAdvanced/Codegen/Thy/examples/class.ocaml Fri Apr 20 13:11:47 2007 +0200 @@ -14,7 +14,7 @@ type 'a null = {null : 'a};; let null _A = _A.null;; -let rec head _A = function y :: xs -> y +let rec head _A = function x :: xs -> x | [] -> null _A;; let rec null_option = None;; diff -r bff5d59de79b -r 1bfd75c1f232 doc-src/IsarAdvanced/Codegen/Thy/examples/collect_duplicates.ML --- a/doc-src/IsarAdvanced/Codegen/Thy/examples/collect_duplicates.ML Fri Apr 20 11:21:53 2007 +0200 +++ b/doc-src/IsarAdvanced/Codegen/Thy/examples/collect_duplicates.ML Fri Apr 20 13:11:47 2007 +0200 @@ -26,7 +26,7 @@ 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_ y ys [] = y; + | collect_duplicates A_ xs ys [] = xs; end; (*struct Codegen*) diff -r bff5d59de79b -r 1bfd75c1f232 doc-src/IsarAdvanced/Codegen/Thy/examples/fac.ML --- a/doc-src/IsarAdvanced/Codegen/Thy/examples/fac.ML Fri Apr 20 11:21:53 2007 +0200 +++ b/doc-src/IsarAdvanced/Codegen/Thy/examples/fac.ML Fri Apr 20 13:11:47 2007 +0200 @@ -7,7 +7,7 @@ datatype nat = Zero_nat | Suc of nat; fun plus_nat (Suc m) n = plus_nat m (Suc n) - | plus_nat Zero_nat y = y; + | plus_nat Zero_nat n = n; fun times_nat (Suc m) n = plus_nat n (times_nat m n) | times_nat Zero_nat n = Zero_nat; diff -r bff5d59de79b -r 1bfd75c1f232 doc-src/IsarAdvanced/Codegen/Thy/examples/fac_case.ML --- a/doc-src/IsarAdvanced/Codegen/Thy/examples/fac_case.ML Fri Apr 20 11:21:53 2007 +0200 +++ b/doc-src/IsarAdvanced/Codegen/Thy/examples/fac_case.ML Fri Apr 20 13:11:47 2007 +0200 @@ -7,7 +7,7 @@ datatype nat = Zero_nat | Suc of nat; fun plus_nat (Suc m) n = plus_nat m (Suc n) - | plus_nat Zero_nat y = y; + | plus_nat Zero_nat n = n; fun times_nat (Suc m) n = plus_nat n (times_nat m n) | times_nat Zero_nat n = Zero_nat; diff -r bff5d59de79b -r 1bfd75c1f232 doc-src/IsarAdvanced/Codegen/Thy/examples/pick1.ML --- a/doc-src/IsarAdvanced/Codegen/Thy/examples/pick1.ML Fri Apr 20 11:21:53 2007 +0200 +++ b/doc-src/IsarAdvanced/Codegen/Thy/examples/pick1.ML Fri Apr 20 13:11:47 2007 +0200 @@ -13,7 +13,7 @@ fun minus_nat (Suc m) (Suc n) = minus_nat m n | minus_nat Zero_nat n = Zero_nat - | minus_nat y Zero_nat = y; + | minus_nat m Zero_nat = m; end; (*struct Nat*) diff -r bff5d59de79b -r 1bfd75c1f232 doc-src/IsarAdvanced/Codegen/Thy/examples/pick2.ML --- a/doc-src/IsarAdvanced/Codegen/Thy/examples/pick2.ML Fri Apr 20 11:21:53 2007 +0200 +++ b/doc-src/IsarAdvanced/Codegen/Thy/examples/pick2.ML Fri Apr 20 13:11:47 2007 +0200 @@ -13,7 +13,7 @@ fun minus_nat (Suc m) (Suc n) = minus_nat m n | minus_nat Zero_nat n = Zero_nat - | minus_nat y Zero_nat = y; + | minus_nat m Zero_nat = m; end; (*struct Nat*)