# HG changeset patch # User haftmann # Date 1162560153 -3600 # Node ID 737a94f047e35949a595bf8ec3e0cf050b26f314 # Parent c6f103e57c941d698cc4586ef9fe79fb1ffdae47 continued tutorial diff -r c6f103e57c94 -r 737a94f047e3 doc-src/IsarAdvanced/Codegen/Thy/Codegen.thy --- a/doc-src/IsarAdvanced/Codegen/Thy/Codegen.thy Fri Nov 03 14:22:31 2006 +0100 +++ b/doc-src/IsarAdvanced/Codegen/Thy/Codegen.thy Fri Nov 03 14:22:33 2006 +0100 @@ -1,10 +1,18 @@ (* $Id$ *) +(*<*) theory Codegen imports Main +uses "../../../IsarImplementation/Thy/setup.ML" begin +ML {* +CodegenSerializer.sml_code_width := 74; +*} + +(*>*) + chapter {* Code generation from Isabelle theories *} section {* Introduction *} @@ -48,7 +56,7 @@ The code generator aims to be usable with no further ado in most cases while allowing for detailed customization. This manifests in the structure of this tutorial: this introduction - continous with a short introduction of concepts. Section + continues with a short introduction of concepts. Section \secref{sec:basics} explains how to use the framework naivly, presuming a reasonable default setup. Then, section \secref{sec:advanced} deals with advanced topics, @@ -60,7 +68,7 @@ Ultimately, the code generator which this tutorial deals with is supposed to replace the already established code generator by Stefan Berghofer \cite{Berghofer-Nipkow:2002}. - So, for the momennt, there are two distinct code generators + So, for the moment, there are two distinct code generators in Isabelle. Also note that while the framework itself is largely object-logic independent, only HOL provides a reasonable @@ -307,12 +315,12 @@ text {* Type classes enter the game via the Isar class package. For a short introduction how to use it, see \cite{isabelle-classes}; - here we just illustrate its relation on code generation. + here we just illustrate its impact on code generation. In a target language, type classes may be represented nativly (as in the case of Haskell). For languages like SML, they are implemented using \emph{dictionaries}. - Our following example specified a class \qt{null}, + Our following example specifiedsa class \qt{null}, assigning to each of its inhabitants a \qt{null} value: *} @@ -353,7 +361,8 @@ *} code_gen dummy (Haskell "examples/") - (* NOTE: you may use Haskell only once in this document *) + (* NOTE: you may use Haskell only once in this document, otherwise + you have to work in distinct subdirectories *) text {* \lsthaskell{Thy/examples/Codegen.hs} @@ -436,7 +445,7 @@ \item[EfficientNat] implements natural numbers by integers, which in geneal will result in higher efficency; pattern matching with @{const "0\nat"} / @{const "Suc"} - is eliminated. + is eliminated. \label{eff_nat} \item[MLString] provides an additional datatype @{text "mlstring"}; in the HOL default setup, strings in HOL are mapped to list of chars in SML; values of type @{text "mlstring"} are @@ -448,24 +457,507 @@ subsection {* Preprocessing *} text {* - + Before selected function theorems are turned into abstract + code, a chain of definitional transformation steps is carried + out: \emph{preprocessing}. There are three possibilites + to customize preprocessing: \emph{inline theorems}, + \emph{inline procedures} and \emph{generic preprocessors}. + + \emph{Inline theorems} are rewriting rules applied to each + function equation. Due to the interpretation of theorems + of function equations, rewrites are applied to the right + hand side and the arguments of the left hand side of an + equation, but never to the constant heading the left hand side. + Inline theorems may be declared an undeclared using the + \emph{code inline} or \emph{code noinline} attribute respectivly. + + Some common applications: +*} + +text_raw {* + \begin{itemize} + \item replacing non-executable constructs by executable ones: \\ +*} + +lemma [code inline]: + "x \ set xs \ x mem xs" by (induct xs) simp_all + +text_raw {* + \item eliminating superfluous constants: \\ +*} + +lemma [code inline]: + "1 = Suc 0" by simp + +text_raw {* + \item replacing executable but inconvenient constructs: \\ *} -(* preprocessing, print_codethms () *) +lemma [code inline]: + "xs = [] \ List.null xs" by (induct xs) simp_all + +text_raw {* + \end{itemize} +*} + +text {* + The current set of inline theorems may be inspected using + the \isasymPRINTCODETHMS command. + + \emph{Inline procedures} are a generalized version of inline + theorems written in ML -- rewrite rules are generated dependent + on the function theorems for a certain function. One + application is the implicit expanding of @{typ nat} numerals + to @{const "0\nat"} / @{const Suc} representation. See further + \secref{sec:ml} + + \emph{Generic preprocessors} provide a most general interface, + transforming a list of function theorems to another + list of function theorems, provided that neither the heading + constant nor its type change. The @{const "0\nat"} / @{const Suc} + pattern elimination implemented in \secref{eff_nat} uses this + interface. + + \begin{warn} + The order in which single preprocessing steps are carried + out currently is not specified; in particular, preprocessing + is \emph{no} fixpoint process. Keep this in mind when + setting up the preprocessor. + + Further, the attribute \emph{code unfold} + associated with the existing code generator also applies to + the new one: \emph{code unfold} implies \emph{code inline}. + \end{warn} +*} subsection {* Customizing serialization *} -(* code_reserved *) -(* existing libraries, understanding the type game, reflexive equations, code inline code_constsubst, code_abstype*) +text {* + Consider the following function and its corresponding + SML code: +*} + +fun + in_interval :: "nat \ nat \ nat \ bool" where + "in_interval (k, l) n \ k \ n \ n \ l" +termination by (auto_term "{}") +(*<*) +declare in_interval.simps [code func] +(*>*) + +(*<*) +code_type bool + (SML) +code_const True and False and "op \" and Not + (SML and and and) +(*>*) + +code_gen in_interval (SML "examples/bool1.ML") + +text {* + \lstsml{Thy/examples/bool1.ML} + + Though this is correct code, it is a little bit unsatisfactory: + boolean values and operators are materialized as distinguished + entities with have nothing to do with the SML-builtin notion + of \qt{bool}. This results in less readable code; + additionally, eager evaluation may cause programs to + loop or break which would perfectly terminate when + the existing SML \qt{bool} would be used. To map + the HOL \qt{bool} on SML \qt{bool}, we may use + \qn{custom serializations}: +*} + +code_type bool + (SML "bool") +code_const True and False and "op \" + (SML "true" and "false" and "_ andalso _") + +text {* + The \isasymCODETYPE commad takes a type constructor + as arguments together with a list of custom serializations. + Each custom serialization starts with a target language + identifier followed by an expression, which during + code serialization is inserted whenever the type constructor + would occur. For constants, \isasymCODECONST implements + the corresponding mechanism. Each \qt{\_} in + a serialization expression is treated as a placeholder + for the type constructor's (the constant's) arguments. +*} + +code_reserved SML + bool true false + +text {* + To assert that the existing \qt{bool}, \qt{true} and \qt{false} + is not used for generated code, we use \isasymCODERESERVED. + + After this setup, code looks quite more readable: +*} + +code_gen in_interval (SML "examples/bool2.ML") + +text {* + \lstsml{Thy/examples/bool2.ML} + + This still is not perfect: the parentheses + around \qt{andalso} are superfluos. Though the serializer + by no means attempts to imitate the rich Isabelle syntax + framework, it provides some common idioms, notably + associative infixes with precedences which may be used here: +*} + +code_const "op \" + (SML infixl 1 "andalso") + +code_gen in_interval (SML "examples/bool3.ML") + +text {* + \lstsml{Thy/examples/bool3.ML} + + Next, we try to map HOL pairs to SML pairs, using the + infix \qt{ * } type constructor and parentheses: +*} + +(*<*) +code_type * + (SML) +code_const Pair + (SML) +(*>*) + +code_type * + (SML infix 2 "*") + +code_const Pair + (SML "!((_),/ (_))") + +text {* + The initial bang \qt{!} tells the serializer to never put + parentheses around the whole expression (they are already present), + while the parentheses around argument place holders + tell not to put parentheses around the arguments. + The slash \qt{/} (followed by arbitrary white space) + inserts a space which may be used as a break if necessary + during pretty printing. + + So far, +*} + +code_type int + (SML "IntInf.int") + (Haskell "Integer") + +code_const "op + \ int \ int \ int" + and "op - \ int \ int \ int" + and "op * \ int \ int \ int" + (SML "IntInf.+ (_, _)" and "IntInf.- (_, _)" and "IntInf.* (_, _)") + (Haskell infixl 6 "+" and infixl 6 "-" and infixl 7 "*") + +(* quote with ' HOL Setup, careful *) + + +(* Better ops, code_moduleprolog *) +(* code_modulename *) + + +subsection {* Types matter *} + +(* shadowing by user-defined serilizations, understanding the type game, +reflexive equations, dangerous equations *) + +subsection {* Concerning operational equality *} + +text {* + Surely you have already noticed how equality is treated + by the code generator: +*} + +fun + collect_duplicates :: "'a list \ 'a list \ 'a list \ 'a list" where + "collect_duplicates xs ys [] = xs" + "collect_duplicates xs ys (z#zs) = (if z \ set xs + then if z \ set ys + then collect_duplicates xs ys zs + else collect_duplicates xs (z#ys) zs + else collect_duplicates (z#xs) (z#ys) zs)" +termination by (auto_term "measure (length o snd o snd)") +(*<*) +lemmas [code func] = collect_duplicates.simps +(*>*) + +text {* + The membership test during preprocessing is rewritting, + resulting in @{const List.memberl}, which itself + performs an explicit equality check. +*} + +code_gen collect_duplicates (SML "examples/collect_duplicates.ML") + +text {* + \lstsml{Thy/examples/collect_duplicates.ML} +*} + +text {* + Obviously, polymorphic equality is implemented the Haskell + way using a type class. How is this achieved? By an + almost trivial definition in the HOL setup: +*} + +(*<*) +setup {* Sign.add_path "foo" *} +(*>*) + +class eq = + fixes eq :: "'a \ 'a \ bool" + +defs + eq [symmetric(*, code inline, code func*)]: "eq \ (op =)" + +text {* + This merely introduces a class @{text eq} with corresponding + operation @{const eq}, which by definition is isomorphic + to @{const "op ="}; the preprocessing framework does the rest. +*} + +(*<*) +lemmas [code noinline] = eq + +hide (open) "class" eq +hide (open) const eq + +lemmas [symmetric, code func] = eq_def + +setup {* Sign.parent_path *} +(*>*) + +text {* + For datatypes, instances of @{text eq} are implicitly derived + when possible. + + Though this class is designed to get rarely in the way, there + are some cases when it suddenly comes to surface: +*} + +text_raw {* + \begin {description} + \item[code lemmas and customary serializations for equality] + Examine the following: \\ +*} + +code_const "op = \ int \ int \ bool" + (SML "!(_ : IntInf.int = _)") + +text_raw {* + \\ What is wrong here? Since @{const "op ="} is nothing else then + a plain constant, this customary serialization will refer + to polymorphic equality @{const "op = \ 'a \ 'a \ bool"}. + Instead, we want the specific equality on @{typ int}, + by using the overloaded constant @{const "Code_Generator.eq"}: \\ +*} + +code_const "Code_Generator.eq \ int \ int \ bool" + (SML "!(_ : IntInf.int = _)") + +text_raw {* + \\ \item[typedecls interpretated by customary serializations] A + common idiom is to use unspecified types for formalizations + and interpret them for a specific target language: \\ +*} + +typedecl key + +fun + lookup :: "(key \ 'a) list \ key \ 'a option" where + "lookup [] l = None" + "lookup ((k, v) # xs) l = (if k = l then Some v else lookup xs l)" +termination by (auto_term "measure (length o fst)") +(*<*) +lemmas [code func] = lookup.simps +(*>*) + +code_type key + (SML "string") + +text_raw {* + \\ This, though, is not sufficient: @{typ key} is no instance + of @{text eq} since @{typ key} is no datatype; the instance + has to be declared manually, including a serialization + for the particular instance of @{const "Code_Generator.eq"}: \\ +*} + +instance key :: eq .. + +code_const "Code_Generator.eq \ key \ key \ bool" + (SML "!(_ : string = _)") + +text_raw {* + \\ Then everything goes fine: \\ +*} + +code_gen lookup (SML "examples/lookup.ML") + +text {* + \lstsml{Thy/examples/lookup.ML} +*} + +text_raw {* + \item[lexicographic orderings and corregularity] Another sublety + enters the stage when definitions of overloaded constants + are dependent on operational equality. For example, let + us define a lexicographic ordering on tuples: \\ +*} + +(*<*) +(*setup {* Sign.add_path "foo" *} + +class ord = ord*) +(*>*) + +(* +instance * :: ("{eq, ord}", ord) ord + "p1 < p2 \ let (x1, y1) = p1; (x2, y2) = p2 in + x1 < x2 \ (x1 = x2 \ y1 < y2)" + "p1 \ p2 \ p1 < p2 \ p1 = p2" .. +*) + +(*<*) +(*hide (open) "class" ord +setup {* Sign.parent_path *}*) +(*>*) + +text_raw {* + \\ Then code generation will fail. Why? The definition + of @{const "op \"} depends on equality on both arguments, + which are polymorhpic and impose an additional @{text eq} + class constraint, thus violating the type discipline + for class operations. + + The solution is to add @{text eq} to both sort arguments: \\ +*} + +instance * :: ("{eq, ord}", "{eq, ord}") ord + "p1 < p2 \ let (x1, y1) = p1; (x2, y2) = p2 in + x1 < x2 \ (x1 = x2 \ y1 < y2)" + "p1 \ p2 \ p1 < p2 \ p1 = p2" .. + +text_raw {* + \\ Then code generation succeeds: \\ +*} + +code_gen "op \ \ 'a\{eq, ord} \ 'b\{eq, ord} \ 'a \ 'b \ bool" + (SML "examples/lexicographic.ML") + +text {* + \lstsml{Thy/examples/lexicographic.ML} +*} + +text_raw {* + \item[Haskell serialization] +*} + +text_raw {* + \end {description} +*} + + +subsection {* Axiomatic extensions *} + +text {* + \begin{warn} + The extensions introduced in this section, though working + in practice, are not the cream of the crop. They will + eventually be replaced by more mature approaches. + \end{warn} +*} + +(* existing libraries, code inline code_constsubst, code_abstype*) section {* ML interfaces \label{sec:ml} *} -(* under developement *) +subsection {* Constants with type discipline: codegen\_consts.ML *} + +text %mlref {* + \begin{mldecls} + @{index_ML_type CodegenConsts.const} \\ + @{index_ML CodegenConsts.inst_of_typ: "theory -> string * typ -> CodegenConsts.const"} \\ + @{index_ML CodegenConsts.typ_of_inst: "theory -> CodegenConsts.const -> string * typ"} \\ + @{index_ML CodegenConsts.norm: "theory -> CodegenConsts.const -> CodegenConsts.const"} \\ + @{index_ML CodegenConsts.norm_of_typ: "theory -> string * typ -> CodegenConsts.const"} + \end{mldecls} +*} + +subsection {* Executable theory content: codegen\_data.ML *} + +text {* + This Pure module implements the core notions of + executable content of a theory. +*} + +subsubsection {* Suspended theorems *} + +text %mlref {* + \begin{mldecls} + @{index_ML_type CodegenData.lthms} \\ + @{index_ML CodegenData.lazy: "(unit -> thm list) -> CodegenData.lthms"} + \end{mldecls} +*} + +subsubsection {* Executable content *} -subsection {* codegen\_data.ML *} +text %mlref {* + \begin{mldecls} + @{index_ML CodegenData.add_func: "thm -> theory -> theory"} \\ + @{index_ML CodegenData.del_func: "thm -> theory -> theory"} \\ + @{index_ML CodegenData.add_funcl: "CodegenConsts.const * CodegenData.lthms -> theory -> theory"} \\ + @{index_ML CodegenData.add_datatype: "string * (((string * sort) list * (string * typ list) list) * CodegenData.lthms) -> theory -> theory"} \\ + @{index_ML CodegenData.del_datatype: "string -> theory -> theory"} \\ + @{index_ML CodegenData.add_inline: "thm -> theory -> theory"} \\ + @{index_ML CodegenData.del_inline: "thm -> theory -> theory"} \\ + @{index_ML CodegenData.add_inline_proc: "(theory -> cterm list -> thm list) -> theory -> theory"} \\ + @{index_ML CodegenData.add_preproc: "(theory -> thm list -> thm list) -> theory -> theory"} \\ + @{index_ML CodegenData.these_funcs: "theory -> CodegenConsts.const -> thm list"} \\ + @{index_ML CodegenData.get_datatype: "theory -> string -> ((string * sort) list * (string * typ list) list) option"} \\ + @{index_ML CodegenData.get_datatype_of_constr: "theory -> CodegenConsts.const -> string option"} + \end{mldecls} + + \begin{description} + + \item @{ML CodegenData.add_func}~@{text "thm"} + + \end{description} +*} + +subsection {* Further auxiliary *} + +text %mlref {* + \begin{mldecls} + @{index_ML CodegenConsts.const_ord: "CodegenConsts.const * CodegenConsts.const -> order"} \\ + @{index_ML CodegenConsts.eq_const: "CodegenConsts.const * CodegenConsts.const -> bool"} \\ + @{index_ML CodegenConsts.consts_of: "theory -> term -> CodegenConsts.const list"} \\ + @{index_ML CodegenConsts.read_const: "theory -> string -> CodegenConsts.const"} \\ + @{index_ML_structure CodegenConsts.Consttab} \\ + @{index_ML CodegenData.typ_func: "theory -> thm -> typ"} \\ + @{index_ML CodegenData.rewrite_func: "thm list -> thm -> thm"} \\ + \end{mldecls} +*} subsection {* Implementing code generator applications *} -(* hooks *) +text {* + \begin{warn} + Some interfaces discussed here have not reached + a final state yet. + Changes likely to occur in future. + \end{warn} +*} + +subsubsection {* Data depending on the theory's executable content *} + +subsubsection {* Datatype hooks *} + +text {* + \emph{Happy proving, happy hacking!} +*} end diff -r c6f103e57c94 -r 737a94f047e3 doc-src/IsarAdvanced/Codegen/Thy/ROOT.ML --- a/doc-src/IsarAdvanced/Codegen/Thy/ROOT.ML Fri Nov 03 14:22:31 2006 +0100 +++ b/doc-src/IsarAdvanced/Codegen/Thy/ROOT.ML Fri Nov 03 14:22:33 2006 +0100 @@ -1,8 +1,4 @@ (* $Id$ *) -CodegenSerializer.sml_code_width := 74; - -CodegenSerializer.sml_code_width := 74; - use_thy "Codegen"; diff -r c6f103e57c94 -r 737a94f047e3 doc-src/IsarAdvanced/Codegen/Thy/examples/Codegen.hs --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/doc-src/IsarAdvanced/Codegen/Thy/examples/Codegen.hs Fri Nov 03 14:22:33 2006 +0100 @@ -0,0 +1,18 @@ +module Codegen where +import qualified IntDef + +class Null a where + null :: a + +head :: (Codegen.Null a_1) => [a_1] -> a_1 +head (y : xs) = y +head [] = Codegen.null + +null_option :: Maybe b +null_option = Nothing + +instance Codegen.Null (Maybe b) where + null = Codegen.null_option + +dummy :: Maybe IntDef.Nat +dummy = Codegen.head [Just (IntDef.Succ_nat IntDef.Zero_nat), Nothing] diff -r c6f103e57c94 -r 737a94f047e3 doc-src/IsarAdvanced/Codegen/Thy/examples/bool1.ML --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/doc-src/IsarAdvanced/Codegen/Thy/examples/bool1.ML Fri Nov 03 14:22:33 2006 +0100 @@ -0,0 +1,40 @@ +structure ROOT = +struct + +structure HOL = +struct + +datatype boola = True | False; + +fun nota False = True + | nota True = False; + +fun op_conj y True = y + | op_conj x False = False + | op_conj True ya = ya + | op_conj False xa = False; + +end; (*struct HOL*) + +structure IntDef = +struct + +datatype nat = Zero_nat | Succ_nat of nat; + +fun less_nat Zero_nat (Succ_nat n) = HOL.True + | less_nat na Zero_nat = HOL.False + | less_nat (Succ_nat m) (Succ_nat nb) = less_nat m nb; + +fun less_eq_nat m n = HOL.nota (less_nat n m); + +end; (*struct IntDef*) + +structure Codegen = +struct + +fun in_interval (k, l) n = + HOL.op_conj (IntDef.less_eq_nat k n) (IntDef.less_eq_nat n l); + +end; (*struct Codegen*) + +end; (*struct ROOT*) diff -r c6f103e57c94 -r 737a94f047e3 doc-src/IsarAdvanced/Codegen/Thy/examples/bool2.ML --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/doc-src/IsarAdvanced/Codegen/Thy/examples/bool2.ML Fri Nov 03 14:22:33 2006 +0100 @@ -0,0 +1,33 @@ +structure ROOT = +struct + +structure HOL = +struct + +fun nota false = true + | nota true = false; + +end; (*struct HOL*) + +structure IntDef = +struct + +datatype nat = Zero_nat | Succ_nat of nat; + +fun less_nat Zero_nat (Succ_nat n) = true + | less_nat na Zero_nat = false + | less_nat (Succ_nat m) (Succ_nat nb) = less_nat m nb; + +fun less_eq_nat m n = HOL.nota (less_nat n m); + +end; (*struct IntDef*) + +structure Codegen = +struct + +fun in_interval (k, l) n = + (IntDef.less_eq_nat k n) andalso (IntDef.less_eq_nat n l); + +end; (*struct Codegen*) + +end; (*struct ROOT*) diff -r c6f103e57c94 -r 737a94f047e3 doc-src/IsarAdvanced/Codegen/Thy/examples/bool3.ML --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/doc-src/IsarAdvanced/Codegen/Thy/examples/bool3.ML Fri Nov 03 14:22:33 2006 +0100 @@ -0,0 +1,33 @@ +structure ROOT = +struct + +structure HOL = +struct + +fun nota false = true + | nota true = false; + +end; (*struct HOL*) + +structure IntDef = +struct + +datatype nat = Zero_nat | Succ_nat of nat; + +fun less_nat Zero_nat (Succ_nat n) = true + | less_nat na Zero_nat = false + | less_nat (Succ_nat m) (Succ_nat nb) = less_nat m nb; + +fun less_eq_nat m n = HOL.nota (less_nat n m); + +end; (*struct IntDef*) + +structure Codegen = +struct + +fun in_interval (k, l) n = + IntDef.less_eq_nat k n andalso IntDef.less_eq_nat n l; + +end; (*struct Codegen*) + +end; (*struct ROOT*) diff -r c6f103e57c94 -r 737a94f047e3 doc-src/IsarAdvanced/Codegen/Thy/examples/class.ML --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/doc-src/IsarAdvanced/Codegen/Thy/examples/class.ML Fri Nov 03 14:22:33 2006 +0100 @@ -0,0 +1,29 @@ +structure ROOT = +struct + +structure IntDef = +struct + +datatype nat = Zero_nat | Succ_nat of nat; + +end; (*struct IntDef*) + +structure Codegen = +struct + +type 'a null = {null_ : 'a}; +fun Null (A_:'a null) = #null_ A_; + +fun head (A_1_:'a_1 null) (y :: xs) = y + | head (A_1_:'a_1 null) [] = Null A_1_; + +val null_option : 'b option = NONE; + +fun null_optiona () = {null_ = null_option} : ('b option) null + +val dummy : IntDef.nat option = + head (null_optiona ()) [SOME (IntDef.Succ_nat IntDef.Zero_nat), NONE]; + +end; (*struct Codegen*) + +end; (*struct ROOT*) diff -r c6f103e57c94 -r 737a94f047e3 doc-src/IsarAdvanced/Codegen/Thy/examples/collect_duplicates.ML --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/doc-src/IsarAdvanced/Codegen/Thy/examples/collect_duplicates.ML Fri Nov 03 14:22:33 2006 +0100 @@ -0,0 +1,40 @@ +structure ROOT = +struct + +structure Code_Generator = +struct + +type 'a eq = {eq_ : 'a -> 'a -> bool}; +fun Eq (A_:'a eq) = #eq_ A_; + +end; (*struct Code_Generator*) + +structure HOL = +struct + +fun op_eq (A_:'a Code_Generator.eq) a b = Code_Generator.Eq A_ a b; + +end; (*struct HOL*) + +structure List = +struct + +fun memberl (A_1_:'a_1 Code_Generator.eq) x (y :: ys) = + HOL.op_eq A_1_ x y orelse memberl A_1_ x ys + | memberl (A_1_:'a_1 Code_Generator.eq) xa [] = false; + +end; (*struct List*) + +structure Codegen = +struct + +fun collect_duplicates (A_:'a Code_Generator.eq) 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 ysa [] = y; + +end; (*struct Codegen*) + +end; (*struct ROOT*) diff -r c6f103e57c94 -r 737a94f047e3 doc-src/IsarAdvanced/Codegen/Thy/examples/fac.ML --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/doc-src/IsarAdvanced/Codegen/Thy/examples/fac.ML Fri Nov 03 14:22:33 2006 +0100 @@ -0,0 +1,25 @@ +structure ROOT = +struct + +structure IntDef = +struct + +datatype nat = Zero_nat | Succ_nat of nat; + +fun plus_nat (Succ_nat m) n = plus_nat m (Succ_nat n) + | plus_nat Zero_nat y = y; + +fun times_nat (Succ_nat m) n = plus_nat n (times_nat m n) + | times_nat Zero_nat na = Zero_nat; + +end; (*struct IntDef*) + +structure Codegen = +struct + +fun fac (IntDef.Succ_nat n) = IntDef.times_nat (IntDef.Succ_nat n) (fac n) + | fac IntDef.Zero_nat = IntDef.Succ_nat IntDef.Zero_nat; + +end; (*struct Codegen*) + +end; (*struct ROOT*) diff -r c6f103e57c94 -r 737a94f047e3 doc-src/IsarAdvanced/Codegen/Thy/examples/fac_case.ML --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/doc-src/IsarAdvanced/Codegen/Thy/examples/fac_case.ML Fri Nov 03 14:22:33 2006 +0100 @@ -0,0 +1,26 @@ +structure ROOT = +struct + +structure IntDef = +struct + +datatype nat = Zero_nat | Succ_nat of nat; + +fun plus_nat (Succ_nat m) n = plus_nat m (Succ_nat n) + | plus_nat Zero_nat y = y; + +fun times_nat (Succ_nat m) n = plus_nat n (times_nat m n) + | times_nat Zero_nat na = Zero_nat; + +end; (*struct IntDef*) + +structure Codegen = +struct + +fun fac n = + (case n of IntDef.Zero_nat => IntDef.Succ_nat IntDef.Zero_nat + | IntDef.Succ_nat ma => IntDef.times_nat n (fac ma)); + +end; (*struct Codegen*) + +end; (*struct ROOT*) diff -r c6f103e57c94 -r 737a94f047e3 doc-src/IsarAdvanced/Codegen/Thy/examples/lexicographic.ML --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/doc-src/IsarAdvanced/Codegen/Thy/examples/lexicographic.ML Fri Nov 03 14:22:33 2006 +0100 @@ -0,0 +1,51 @@ +structure ROOT = +struct + +structure Code_Generator = +struct + +type 'a eq = {eq_ : 'a -> 'a -> bool}; +fun Eq (A_:'a eq) = #eq_ A_; + +end; (*struct Code_Generator*) + +structure Product_Type = +struct + +fun eq_prod (A_:'a Code_Generator.eq) (B_:'b Code_Generator.eq) (x1, y1) + (x2, y2) = Code_Generator.Eq A_ x1 x2 andalso Code_Generator.Eq B_ y1 y2; + +end; (*struct Product_Type*) + +structure Orderings = +struct + +type 'a ord = + {Code_Generator__eq : 'a Code_Generator.eq, 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_; + +end; (*struct Orderings*) + +structure Codegen = +struct + +fun less_prod (B_:'b Orderings.ord) (C_:'c Orderings.ord) p1 p2 = + let + val (x1a, y1a) = p1; + val (x2a, y2a) = p2; + in + Orderings.Less B_ x1a x2a orelse + Code_Generator.Eq (#Code_Generator__eq B_) x1a x2a andalso + Orderings.Less C_ y1a y2a + end; + +fun less_eq_prod (B_:'b Orderings.ord) (C_:'c Orderings.ord) p1 p2 = + less_prod B_ C_ p1 p2 orelse + Product_Type.eq_prod (#Code_Generator__eq B_) (#Code_Generator__eq C_) + p1 p2; + +end; (*struct Codegen*) + +end; (*struct ROOT*) diff -r c6f103e57c94 -r 737a94f047e3 doc-src/IsarAdvanced/Codegen/Thy/examples/lookup.ML --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/doc-src/IsarAdvanced/Codegen/Thy/examples/lookup.ML Fri Nov 03 14:22:33 2006 +0100 @@ -0,0 +1,13 @@ +structure ROOT = +struct + +structure Codegen = +struct + +fun lookup ((k, v) :: xs) l = + (if (k : string = l) then SOME v else lookup xs l) + | lookup [] la = NONE; + +end; (*struct Codegen*) + +end; (*struct ROOT*) diff -r c6f103e57c94 -r 737a94f047e3 doc-src/IsarAdvanced/Codegen/Thy/examples/pick1.ML --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/doc-src/IsarAdvanced/Codegen/Thy/examples/pick1.ML Fri Nov 03 14:22:33 2006 +0100 @@ -0,0 +1,34 @@ +structure ROOT = +struct + +structure IntDef = +struct + +datatype nat = Zero_nat | Succ_nat of nat; + +fun less_nat Zero_nat (Succ_nat n) = true + | less_nat na Zero_nat = false + | less_nat (Succ_nat m) (Succ_nat nb) = less_nat m nb; + +fun minus_nat (Succ_nat m) (Succ_nat n) = minus_nat m n + | minus_nat Zero_nat na = Zero_nat + | minus_nat y Zero_nat = y; + +end; (*struct IntDef*) + +structure Codegen = +struct + +fun pick ((k, v) :: xs) n = + (if IntDef.less_nat n k then v else pick xs (IntDef.minus_nat n k)) + | pick (x :: xsa) na = + let + val (ka, va) = x; + in + (if IntDef.less_nat na ka then va + else pick xsa (IntDef.minus_nat na ka)) + end; + +end; (*struct Codegen*) + +end; (*struct ROOT*) diff -r c6f103e57c94 -r 737a94f047e3 doc-src/IsarAdvanced/Codegen/Thy/examples/pick2.ML --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/doc-src/IsarAdvanced/Codegen/Thy/examples/pick2.ML Fri Nov 03 14:22:33 2006 +0100 @@ -0,0 +1,27 @@ +structure ROOT = +struct + +structure IntDef = +struct + +datatype nat = Zero_nat | Succ_nat of nat; + +fun less_nat Zero_nat (Succ_nat n) = true + | less_nat na Zero_nat = false + | less_nat (Succ_nat m) (Succ_nat nb) = less_nat m nb; + +fun minus_nat (Succ_nat m) (Succ_nat n) = minus_nat m n + | minus_nat Zero_nat na = Zero_nat + | minus_nat y Zero_nat = y; + +end; (*struct IntDef*) + +structure Codegen = +struct + +fun pick ((k, v) :: xs) n = + (if IntDef.less_nat n k then v else pick xs (IntDef.minus_nat n k)); + +end; (*struct Codegen*) + +end; (*struct ROOT*)