# HG changeset patch # User haftmann # Date 1177587175 -7200 # Node ID e3962371f568cab8c4c13ed0f046cacc260a7d32 # Parent 4b77a43f7f587a0b4fa3d6fb4bd3ea96b7aa448d updated doc diff -r 4b77a43f7f58 -r e3962371f568 doc-src/IsarAdvanced/Codegen/Thy/Codegen.thy --- a/doc-src/IsarAdvanced/Codegen/Thy/Codegen.thy Thu Apr 26 12:00:12 2007 +0200 +++ b/doc-src/IsarAdvanced/Codegen/Thy/Codegen.thy Thu Apr 26 13:32:55 2007 +0200 @@ -168,7 +168,7 @@ \emph{type classes}. A defining equation as a first approximation is a theorem of the form @{text "f t\<^isub>1 t\<^isub>2 \ t\<^isub>n \ t"} (an equation headed by a constant @{text f} with arguments - @{text "t\<^isub>1 t\<^isub>2 \ t\<^isub>n"} and right hand side @{text t}. + @{text "t\<^isub>1 t\<^isub>2 \ t\<^isub>n"} and right hand side @{text t}). Code generation aims to turn defining equations into a functional program by running through a process (see figure \ref{fig:process}): @@ -245,15 +245,12 @@ a defining equation (e.g.~the Hilbert choice operation @{text "SOME"}): *} - (*<*) setup {* Sign.add_path "foo" *} (*>*) - definition pick_some :: "'a list \ 'a" where "pick_some xs = (SOME x. x \ set xs)" - (*<*) hide const pick_some @@ -263,7 +260,6 @@ pick_some :: "'a list \ 'a" where "pick_some = hd" (*>*) - code_gen pick_some (SML "examples/fail_const.ML") text {* \noindent will fail. *} @@ -285,7 +281,7 @@ The typical HOL tools are already set up in a way that function definitions introduced by @{text "\"}, @{text "\"}, - @{text "\"}, @{text "\"} + @{text "\"}, @{text "\"}, @{text "\"} are implicitly propagated to this defining equation table. Specific theorems may be selected using an attribute: \emph{code func}. As example, @@ -300,7 +296,7 @@ if n < k then v else pick xs (n - k))" text {* - We want to eliminate the explicit destruction + \noindent We want to eliminate the explicit destruction of @{term x} to @{term "(k, v)"}: *} @@ -311,11 +307,11 @@ code_gen pick (*<*)(SML #)(*>*)(SML "examples/pick1.ML") text {* - This theorem is now added to the defining equation table: + \noindent This theorem now is used for generating code: \lstsml{Thy/examples/pick1.ML} - It might be convenient to remove the pointless original + \noindent It might be convenient to remove the pointless original equation, using the \emph{nofunc} attribute: *} @@ -326,7 +322,7 @@ text {* \lstsml{Thy/examples/pick2.ML} - Syntactic redundancies are implicitly dropped. For example, + \noindent Syntactic redundancies are implicitly dropped. For example, using a modified version of the @{const fac} function as defining equation, the then redundant (since syntactically subsumed) original defining equations @@ -358,7 +354,7 @@ here we just illustrate its impact on code generation. In a target language, type classes may be represented - natively (as in the case of Haskell). For languages + natively (as in the case of Haskell). For languages like SML, they are implemented using \emph{dictionaries}. Our following example specifies a class \qt{null}, assigning to each of its inhabitants a \qt{null} value: @@ -367,12 +363,11 @@ class null = type + fixes null :: 'a -consts +fun head :: "'a\null list \ 'a" - -primrec +where "head [] = null" - "head (x#xs) = x" + | "head (x#xs) = x" text {* We provide some instances for our @{text null}: @@ -406,8 +401,9 @@ text {* \lsthaskell{Thy/examples/Codegen.hs} + \noindent (we have left out all other modules). - (we have left out all other modules). + \medskip The whole code in SML with explicit dictionary passing: *} @@ -416,51 +412,21 @@ text {* \lstsml{Thy/examples/class.ML} -*} -text {* - or in OCaml: + \medskip + + \noindent or in OCaml: *} code_gen dummy (OCaml "examples/class.ocaml") text {* \lstsml{Thy/examples/class.ocaml} + + \medskip The explicit association of constants + to classes can be inspected using the @{text "\"} *} -subsection {* Incremental code generation *} - -text {* - Code generation is \emph{incremental}: theorems - and abstract intermediate code are cached and extended on demand. - The cache may be partially or fully dropped if the underlying - executable content of the theory changes. - Implementation of caching is supposed to transparently - hid away the details from the user. Anyway, caching - reaches the surface by using a slightly more general form - of the @{text "\"}: either the list of constants or the - list of serialization expressions may be dropped. If no - serialization expressions are given, only abstract code - is generated and cached; if no constants are given, the - current cache is serialized. - - For explorative purpose, the - @{text "\"} command may prove useful: -*} - -code_thms - -text {* - \noindent print all cached defining equations (i.e.~\emph{after} - any applied transformation). A - list of constants may be given; their function - equations are added to the cache if not already present. - - Similarly, the @{text "\"} command shows a graph - visualizing dependencies between defining equations. -*} - - section {* Recipes and advanced topics \label{sec:advanced} *} @@ -481,7 +447,7 @@ \end{itemize} *} -subsection {* Library theories *} +subsection {* Library theories \label{sec:library} *} text {* The HOL \emph{Main} theory already provides a code generator setup @@ -492,6 +458,13 @@ \begin{description} + \item[@{text "Pretty_Int"}] represents HOL integers by big + integer literals in target languages. + \item[@{text "Pretty_Char"}] represents HOL characters by + character literals in target languages. + \item[@{text "Pretty_Char_chr"}] like @{text "Pretty_Char_chr"}, + but also offers treatment of character codes; includes + @{text "Pretty_Int"}. \item[@{text "ExecutableSet"}] allows to generate code for finite sets using lists. \item[@{text "ExecutableRat"}] \label{exec_rat} implements rational @@ -499,10 +472,10 @@ \item[@{text "EfficientNat"}] \label{eff_nat} implements natural numbers by integers, which in general will result in higher efficency; pattern matching with @{const "0\nat"} / @{const "Suc"} - is eliminated. + is eliminated; includes @{text "Pretty_Int"}. \item[@{text "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 + of HOL characters in SML; values of type @{text "mlstring"} are mapped to strings in SML. \end{description} @@ -524,7 +497,6 @@ 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 respectively. - Some common applications: *} @@ -585,8 +557,148 @@ \end{warn} *} + +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)" + +text {* + The membership test during preprocessing is rewritten, + resulting in @{const List.memberl}, which itself + performs an explicit equality check. +*} + +code_gen collect_duplicates (*<*)(SML #)(*>*)(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" *} +consts "op =" :: "'a" +(*>*) +class eq (attach "op =") = type + +text {* + This merely introduces a class @{text eq} with corresponding + operation @{text "op ="}; + the preprocessing framework does the rest. + For datatypes, instances of @{text eq} are implicitly derived + when possible. + + Though this @{text eq} class is designed to get rarely in + the way, a subtlety + enters the stage when definitions of overloaded constants + are dependent on operational equality. For example, let + us define a lexicographic ordering on tuples: +*} +(*<*) +hide (open) "class" eq +hide (open) const "op =" +setup {* Sign.parent_path *} +(*>*) +instance * :: (ord, ord) ord + less_prod_def: + "p1 < p2 \ let (x1 \ 'a\ord, y1 \ 'b\ord) = p1; (x2, y2) = p2 in + x1 < x2 \ (x1 = x2 \ y1 < y2)" + 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(*<*), code nofunc(*>*)]: + "(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_prod_def less_eq_prod_def by simp_all + +text {* + Then code generation will fail. Why? The definition + of @{const "op \"} depends on equality on both arguments, + which are polymorphic and impose an additional @{text eq} + class constraint, thus violating the type discipline + for class operations. + + The solution is to add @{text eq} explicitly to the first sort arguments in the + code theorems: +*} + +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 {* + \noindent Then code generation succeeds: +*} + +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. 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}. +*} + + +subsection {* Programs as sets of theorems *} + +text {* + As told in \secref{sec:concept}, code generation is based + on a structured collection of code theorems. + For explorative purpose, this collection + may be inspected using the @{text "\"} command: +*} + +code_thms "op mod :: nat \ nat \ nat" + +text {* + \noindent prints a table with \emph{all} defining equations + for @{const "op mod :: nat \ nat \ nat"}, including + \emph{all} defining equations those equations depend + on recursivly. @{text "\"} provides a convenient + mechanism to inspect the impact of a preprocessor setup + on defining equations. + + Similarly, the @{text "\"} command shows a graph + visualizing dependencies between defining equations. +*} + + subsection {* Customizing serialization *} +subsubsection {* Basics *} + text {* Consider the following function and its corresponding SML code: @@ -595,20 +707,18 @@ fun in_interval :: "nat \ nat \ nat \ bool" where "in_interval (k, l) n \ k \ n \ n \ l" - (*<*) code_type %tt bool (SML) code_const %tt True and False and "op \" and Not (SML and and and) (*>*) - code_gen in_interval (*<*)(SML #)(*>*)(SML "examples/bool_literal.ML") text {* \lstsml{Thy/examples/bool_literal.ML} - Though this is correct code, it is a little bit unsatisfactory: + \noindent 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; @@ -651,7 +761,7 @@ text {* \lstsml{Thy/examples/bool_mlbool.ML} - This still is not perfect: the parentheses + \noindent This still is not perfect: the parentheses around the \qt{andalso} expression are superfluous. Though the serializer by no means attempts to imitate the rich Isabelle syntax @@ -667,20 +777,19 @@ text {* \lstsml{Thy/examples/bool_infix.ML} + \medskip + Next, we try to map HOL pairs to SML pairs, using the infix ``@{verbatim "*"}'' type constructor and parentheses: *} - (*<*) code_type * (SML) code_const Pair (SML) (*>*) - code_type %tt * (SML infix 2 "*") - code_const %tt Pair (SML "!((_),/ (_))") @@ -693,44 +802,7 @@ inserts a space which may be used as a break if necessary during pretty printing. - So far, we did only provide more idiomatic serializations for - constructs which would be executable on their own. Target-specific - serializations may also be used to \emph{implement} constructs - which have no explicit notion of executability. For example, - take the HOL integers: -*} - -definition - double_inc :: "int \ int" where - "double_inc k = 2 * k + 1" - -code_gen double_inc (SML "examples/integers.ML") - -text {* - will fail: @{typ int} in HOL is implemented using a quotient - type, which does not provide any notion of executability. - \footnote{Eventually, we also want to provide executability - for quotients.}. However, we could use the SML builtin - integers: -*} - -code_type %tt int - (SML "IntInf.int") - -code_const %tt "op + \ int \ int \ int" - and "op * \ int \ int \ int" - (SML "IntInf.+ (_, _)" and "IntInf.* (_, _)") - -code_gen double_inc (*<*)(SML #)(*>*)(SML "examples/integers.ML") - -text {* - resulting in: - - \lstsml{Thy/examples/integers.ML} -*} - -text {* - These examples give a glimpse what powerful mechanisms + These examples give a glimpse what mechanisms custom serializations provide; however their usage requires careful thinking in order not to introduce inconsistencies -- or, in other words: @@ -748,169 +820,6 @@ a recommended tutorial on how to use them properly. *} -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)" - -text {* - The membership test during preprocessing is rewritten, - resulting in @{const List.memberl}, which itself - performs an explicit equality check. -*} - -code_gen collect_duplicates (*<*)(SML #)(*>*)(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" *} -consts "op =" :: "'a" -(*>*) - -class eq (attach "op =") = type - -text {* - This merely introduces a class @{text eq} with corresponding - operation @{text "op ="}; - the preprocessing framework does the rest. -*} - -(*<*) -hide (open) "class" eq -hide (open) const "op =" -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: -*} - -subsubsection {* typedecls interpreted by customary serializations *} - -text {* - 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)" - -code_type %tt key - (SML "string") - -text {* - 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 "op ="}: -*} - -instance key :: eq .. - -code_const %tt "op = \ key \ key \ bool" - (SML "!((_ : string) = _)") - -text {* - Then everything goes fine: -*} - -code_gen lookup (*<*)(SML #)(*>*)(SML "examples/lookup.ML") - -text {* - \lstsml{Thy/examples/lookup.ML} -*} - -subsubsection {* lexicographic orderings *} - -text {* - Another subtlety - enters the stage when definitions of overloaded constants - are dependent on operational equality. For example, let - us define a lexicographic ordering on tuples: -*} - -instance * :: (ord, ord) ord - less_prod_def: "p1 < p2 \ let (x1 \ 'a\ord, y1 \ 'b\ord) = p1; (x2, y2) = p2 in - x1 < x2 \ (x1 = x2 \ y1 < y2)" - 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_prod_def less_eq_prod_def by simp_all - -text {* - Then code generation will fail. Why? The definition - of @{const "op \"} depends on equality on both arguments, - which are polymorphic and impose an additional @{text eq} - class constraint, thus violating the type discipline - for class operations. - - The solution is to add @{text eq} explicitly to the first sort arguments in the - code theorems: -*} - -(*<*) -lemmas [code nofunc] = ord_prod -(*>*) - -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\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. 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 *} @@ -921,23 +830,12 @@ for the class (@{text "\"}) and its operation: *} -(*<*) -setup {* Sign.add_path "bar" *} -class eq = type + fixes eq :: "'a \ 'a \ bool" -(*>*) - code_class %tt eq - (Haskell "Eq" where eq \ "(==)") + (Haskell "Eq" where "op =" \ "(==)") -code_const %tt eq +code_const %tt "op =" (Haskell infixl 4 "==") -(*<*) -hide "class" eq -hide const eq -setup {* Sign.parent_path *} -(*>*) - text {* A problem now occurs whenever a type which is an instance of @{text eq} in HOL is mapped @@ -962,86 +860,57 @@ code_instance %tt bar :: eq (Haskell -) -subsection {* Types matter *} -text {* - Imagine the following quick-and-dirty setup for implementing - some kind of sets as lists in SML: -*} - -code_type %tt set - (SML "_ list") - -code_const %tt "{}" and insert - (SML "![]" and infixl 7 "::") - -definition - dummy_set :: "(nat \ nat) set" where - "dummy_set = {Suc}" - -text {* - Then code generation for @{const dummy_set} will fail. - Why? A glimpse at the defining equations will offer: -*} - -code_thms insert +subsubsection {* Pretty printing *} text {* - This reveals the defining equation @{thm insert_def} - for @{const insert}, which is operationally meaningless - but forces an equality constraint on the set members - (which is not satisfiable if the set members are functions). - Even when using set of natural numbers (which are an instance - of \emph{eq}), we run into a problem: -*} - -definition - foobar_set :: "nat set" where - "foobar_set = {0, 1, 2}" - -text {* - In this case the serializer would complain that @{const insert} - expects dictionaries (namely an \emph{eq} dictionary) but - has also been given a customary serialization. - - \fixme[needs rewrite] The solution to this dilemma: + The serializer provides ML interfaces to set up + pretty serializations for expressions like lists, numerals + and characters; these are + monolithic stubs and should only be used with the + theories introduces in \secref{sec:library}. *} -lemma [code func]: - "insert = insert" .. - -code_gen dummy_set foobar_set (*<*)(SML #)(*>*)(SML "examples/dirty_set.ML") - -text {* - \lstsml{Thy/examples/dirty_set.ML} - - Reflexive defining equations by convention are dropped: -*} - -code_thms insert - -text {* - will show \emph{no} defining equations for insert. - - Note that the sort constraints of reflexive equations - are considered; so -*} - -lemma [code func]: - "(insert \ 'a\eq \ 'a set \ 'a set) = insert" .. - -text {* - would mean nothing else than to introduce the evil - sort constraint by hand. -*} - - subsection {* Constructor sets for datatypes *} text {* - \fixme + Conceptually, any datatype is spanned by a set of + \emph{constructors} of type @{text "\ = \ \ \ \\<^isub>1 \ \\<^isub>n"} + where @{text "{\\<^isub>1, \, \\<^isub>n}"} is excactly the set of \emph{all} + type variables in @{text "\"}. The HOL datatype package + by default registers any new datatype in the table + of datatypes, which may be inspected using + the @{text "\"} command. + + In some cases, it may be convenient to alter or + extend this table; as an example, we show + how to implement finite sets by lists + using the conversion @{term [source] "set \ 'a list \ 'a set"} + as constructor: *} +code_datatype set + +lemma [code func]: "{} = set []" by simp + +lemma [code func]: "insert x (set xs) = set (x#xs)" by simp + +lemma [code func]: "x \ set xs \ x mem xs" by (induct xs) simp_all + +lemma [code func]: "xs \ set ys = foldr insert ys xs" by (induct ys) simp_all + +lemma [code func]: "\set xs = foldr (op \) xs {}" by (induct xs) simp_all + +code_gen "{}" insert "op \" "op \" "Union" (*<*)(SML #)(*>*)(SML "examples/set_list.ML") + +text {* + \lstsml{Thy/examples/set_list.ML} + + \medskip + + Changing the representation of existing datatypes requires + some care with respect to pattern matching and such. +*} subsection {* Cyclic module dependencies *} @@ -1069,6 +938,22 @@ at serialization time. *} +subsection {* Incremental code generation *} + +text {* + Code generation is \emph{incremental}: theorems + and abstract intermediate code are cached and extended on demand. + The cache may be partially or fully dropped if the underlying + executable content of the theory changes. + Implementation of caching is supposed to transparently + hid away the details from the user. Anyway, caching + reaches the surface by using a slightly more general form + of the @{text "\"}, @{text "\"} + and @{text "\"} commands: the list of constants + may be omitted. Then, all constants with code theorems + in the current cache are referred to. +*} + subsection {* Axiomatic extensions *} text {* @@ -1145,6 +1030,8 @@ text {* \lstsml{Thy/examples/arbitrary.ML} + \medskip + Another axiomatic extension is code generation for abstracted types. For this, the @{text "ExecutableRat"} (see \secref{exec_rat}) @@ -1370,13 +1257,13 @@ \item @{text merge} merging two data slots. - \item @{text purge}~@{text thy}~@{text cs} propagates changes in executable content; + \item @{text purge}~@{text thy}~@{text consts} propagates changes in executable content; if possible, the current theory context is handed over as argument @{text thy} (if there is no current theory context (e.g.~during - theory merge, @{ML NONE}); @{text cs} indicates the kind + theory merge, @{ML NONE}); @{text consts} indicates the kind of change: @{ML NONE} stands for a fundamental change - which invalidates any existing code, @{text "SOME cs"} - hints that executable content for constants @{text cs} + which invalidates any existing code, @{text "SOME consts"} + hints that executable content for constants @{text consts} has changed. \end{description} @@ -1406,19 +1293,61 @@ \end{description} *} -(* subsubsection {* Building implementable systems fo defining equations *} +subsubsection {* Building implementable systems fo defining equations *} text {* Out of the executable content of a theory, a normalized defining equation systems may be constructed containing function definitions for constants. The system is cached until its underlying executable content changes. + + Defining equations are retrieved by instantiation + of the functor @{ML_functor CodegenFuncgrRetrieval} + which takes two arguments: + + \medskip + \begin{tabular}{l} + @{text "val name: string"} \\ + @{text "val rewrites: theory \ thm list"} + \end{tabular} + + \begin{description} + + \item @{text name} is a system-wide unique name identifying + this particular system of defining equations. + + \item @{text rewrites} specifies a set of theory-dependent + rewrite rules which are added to the preprocessor setup; + if no additional preprocessing is required, pass + a function returning an empty list. + + \end{description} + + An instance of @{ML_functor CodegenFuncgrRetrieval} in essence + provides the following interface: + + \medskip + \begin{tabular}{l} + @{text "make: theory \ CodegenConsts.const list \ CodegenFuncgr.T"} \\ + \end{tabular} + + \begin{description} + + \item @{text make}~@{text thy}~@{text consts} returns + a system of defining equations which is guaranteed + to contain all defining equations for constants @{text consts} + including all defining equations any defining equation + for any constant in @{text consts} depends on. + + \end{description} + + Systems of defining equations are graphs accesible by the + following operations: *} text %mlref {* \begin{mldecls} @{index_ML_type CodegenFuncgr.T} \\ - @{index_ML CodegenFuncgr.make: "theory -> CodegenConsts.const list -> CodegenFuncgr.T"} \\ @{index_ML CodegenFuncgr.funcs: "CodegenFuncgr.T -> CodegenConsts.const -> thm list"} \\ @{index_ML CodegenFuncgr.typ: "CodegenFuncgr.T -> CodegenConsts.const -> typ"} \\ @{index_ML CodegenFuncgr.deps: "CodegenFuncgr.T @@ -1431,20 +1360,15 @@ \item @{ML_type CodegenFuncgr.T} represents a normalized defining equation system. - \item @{ML CodegenFuncgr.make}~@{text thy}~@{text cs} - returns a normalized defining equation system, - with the assertion that it contains any function - definition for constants @{text cs} (if existing). + \item @{ML CodegenFuncgr.funcs}~@{text funcgr}~@{text const} + retrieves defining equiations for constant @{text const}. - \item @{ML CodegenFuncgr.funcs}~@{text funcgr}~@{text c} - retrieves function definition for constant @{text c}. + \item @{ML CodegenFuncgr.typ}~@{text funcgr}~@{text const} + retrieves function type for constant @{text const}. - \item @{ML CodegenFuncgr.typ}~@{text funcgr}~@{text c} - retrieves function type for constant @{text c}. - - \item @{ML CodegenFuncgr.deps}~@{text funcgr}~@{text cs} + \item @{ML CodegenFuncgr.deps}~@{text funcgr}~@{text consts} returns the transitive closure of dependencies for - constants @{text cs} as a partitioning where each partition + constants @{text consts} as a partitioning where each partition corresponds to a strongly connected component of dependencies and any partition does \emph{not} depend on partitions further left. @@ -1453,7 +1377,7 @@ returns all currently represented constants. \end{description} -*} *) +*} subsubsection {* Datatype hooks *} diff -r 4b77a43f7f58 -r e3962371f568 doc-src/IsarAdvanced/Codegen/Thy/document/Codegen.tex --- a/doc-src/IsarAdvanced/Codegen/Thy/document/Codegen.tex Thu Apr 26 12:00:12 2007 +0200 +++ b/doc-src/IsarAdvanced/Codegen/Thy/document/Codegen.tex Thu Apr 26 13:32:55 2007 +0200 @@ -198,7 +198,7 @@ \emph{type classes}. A defining equation as a first approximation is a theorem of the form \isa{f\ t\isactrlisub {\isadigit{1}}\ t\isactrlisub {\isadigit{2}}\ {\isasymdots}\ t\isactrlisub n\ {\isasymequiv}\ t} (an equation headed by a constant \isa{f} with arguments - \isa{t\isactrlisub {\isadigit{1}}\ t\isactrlisub {\isadigit{2}}\ {\isasymdots}\ t\isactrlisub n} and right hand side \isa{t}. + \isa{t\isactrlisub {\isadigit{1}}\ t\isactrlisub {\isadigit{2}}\ {\isasymdots}\ t\isactrlisub n} and right hand side \isa{t}). Code generation aims to turn defining equations into a functional program by running through a process (see figure \ref{fig:process}): @@ -290,14 +290,12 @@ {\isafoldML}% % \isadelimML -\isanewline % \endisadelimML \isacommand{definition}\isamarkupfalse% \isanewline \ \ pick{\isacharunderscore}some\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequoteopen}{\isacharprime}a\ list\ {\isasymRightarrow}\ {\isacharprime}a{\isachardoublequoteclose}\ \isakeyword{where}\isanewline -\ \ {\isachardoublequoteopen}pick{\isacharunderscore}some\ xs\ {\isacharequal}\ {\isacharparenleft}SOME\ x{\isachardot}\ x\ {\isasymin}\ set\ xs{\isacharparenright}{\isachardoublequoteclose}\isanewline -% +\ \ {\isachardoublequoteopen}pick{\isacharunderscore}some\ xs\ {\isacharequal}\ {\isacharparenleft}SOME\ x{\isachardot}\ x\ {\isasymin}\ set\ xs{\isacharparenright}{\isachardoublequoteclose}% \isadelimML % \endisadelimML @@ -310,7 +308,6 @@ \isadelimML % \endisadelimML -\isanewline \isacommand{code{\isacharunderscore}gen}\isamarkupfalse% \ pick{\isacharunderscore}some\ {\isacharparenleft}SML\ {\isachardoublequoteopen}examples{\isacharslash}fail{\isacharunderscore}const{\isachardot}ML{\isachardoublequoteclose}{\isacharparenright}% \begin{isamarkuptext}% @@ -337,7 +334,7 @@ The typical HOL tools are already set up in a way that function definitions introduced by \isa{{\isasymDEFINITION}}, \isa{{\isasymFUN}}, - \isa{{\isasymFUNCTION}}, \isa{{\isasymPRIMREC}} + \isa{{\isasymFUNCTION}}, \isa{{\isasymPRIMREC}}, \isa{{\isasymRECDEF}} are implicitly propagated to this defining equation table. Specific theorems may be selected using an attribute: \emph{code func}. As example, @@ -353,7 +350,7 @@ \ \ {\isachardoublequoteopen}pick\ {\isacharparenleft}x{\isacharhash}xs{\isacharparenright}\ n\ {\isacharequal}\ {\isacharparenleft}let\ {\isacharparenleft}k{\isacharcomma}\ v{\isacharparenright}\ {\isacharequal}\ x\ in\isanewline \ \ \ \ if\ n\ {\isacharless}\ k\ then\ v\ else\ pick\ xs\ {\isacharparenleft}n\ {\isacharminus}\ k{\isacharparenright}{\isacharparenright}{\isachardoublequoteclose}% \begin{isamarkuptext}% -We want to eliminate the explicit destruction +\noindent We want to eliminate the explicit destruction of \isa{x} to \isa{{\isacharparenleft}k{\isacharcomma}\ v{\isacharparenright}}:% \end{isamarkuptext}% \isamarkuptrue% @@ -379,11 +376,11 @@ \isacommand{code{\isacharunderscore}gen}\isamarkupfalse% \ pick\ {\isacharparenleft}SML\ {\isachardoublequoteopen}examples{\isacharslash}pick{\isadigit{1}}{\isachardot}ML{\isachardoublequoteclose}{\isacharparenright}% \begin{isamarkuptext}% -This theorem is now added to the defining equation table: +\noindent This theorem now is used for generating code: \lstsml{Thy/examples/pick1.ML} - It might be convenient to remove the pointless original + \noindent It might be convenient to remove the pointless original equation, using the \emph{nofunc} attribute:% \end{isamarkuptext}% \isamarkuptrue% @@ -395,7 +392,7 @@ \begin{isamarkuptext}% \lstsml{Thy/examples/pick2.ML} - Syntactic redundancies are implicitly dropped. For example, + \noindent Syntactic redundancies are implicitly dropped. For example, using a modified version of the \isa{fac} function as defining equation, the then redundant (since syntactically subsumed) original defining equations @@ -445,7 +442,7 @@ here we just illustrate its impact on code generation. In a target language, type classes may be represented - natively (as in the case of Haskell). For languages + natively (as in the case of Haskell). For languages like SML, they are implemented using \emph{dictionaries}. Our following example specifies a class \qt{null}, assigning to each of its inhabitants a \qt{null} value:% @@ -455,14 +452,12 @@ \ null\ {\isacharequal}\ type\ {\isacharplus}\isanewline \ \ \isakeyword{fixes}\ null\ {\isacharcolon}{\isacharcolon}\ {\isacharprime}a\isanewline \isanewline -\isacommand{consts}\isamarkupfalse% +\isacommand{fun}\isamarkupfalse% \isanewline \ \ head\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequoteopen}{\isacharprime}a{\isasymColon}null\ list\ {\isasymRightarrow}\ {\isacharprime}a{\isachardoublequoteclose}\isanewline -\isanewline -\isacommand{primrec}\isamarkupfalse% -\isanewline +\isakeyword{where}\isanewline \ \ {\isachardoublequoteopen}head\ {\isacharbrackleft}{\isacharbrackright}\ {\isacharequal}\ null{\isachardoublequoteclose}\isanewline -\ \ {\isachardoublequoteopen}head\ {\isacharparenleft}x{\isacharhash}xs{\isacharparenright}\ {\isacharequal}\ x{\isachardoublequoteclose}% +\ \ {\isacharbar}\ {\isachardoublequoteopen}head\ {\isacharparenleft}x{\isacharhash}xs{\isacharparenright}\ {\isacharequal}\ x{\isachardoublequoteclose}% \begin{isamarkuptext}% We provide some instances for our \isa{null}:% \end{isamarkuptext}% @@ -522,8 +517,9 @@ \ dummy\ {\isacharparenleft}Haskell\ {\isachardoublequoteopen}examples{\isacharslash}{\isachardoublequoteclose}{\isacharparenright}% \begin{isamarkuptext}% \lsthaskell{Thy/examples/Codegen.hs} + \noindent (we have left out all other modules). - (we have left out all other modules). + \medskip The whole code in SML with explicit dictionary passing:% \end{isamarkuptext}% @@ -531,53 +527,20 @@ \isacommand{code{\isacharunderscore}gen}\isamarkupfalse% \ dummy\ {\isacharparenleft}SML\ {\isachardoublequoteopen}examples{\isacharslash}class{\isachardot}ML{\isachardoublequoteclose}{\isacharparenright}% \begin{isamarkuptext}% -\lstsml{Thy/examples/class.ML}% -\end{isamarkuptext}% -\isamarkuptrue% -% -\begin{isamarkuptext}% -or in OCaml:% +\lstsml{Thy/examples/class.ML} + + \medskip + + \noindent or in OCaml:% \end{isamarkuptext}% \isamarkuptrue% \isacommand{code{\isacharunderscore}gen}\isamarkupfalse% \ dummy\ {\isacharparenleft}OCaml\ {\isachardoublequoteopen}examples{\isacharslash}class{\isachardot}ocaml{\isachardoublequoteclose}{\isacharparenright}% \begin{isamarkuptext}% -\lstsml{Thy/examples/class.ocaml}% -\end{isamarkuptext}% -\isamarkuptrue% -% -\isamarkupsubsection{Incremental code generation% -} -\isamarkuptrue% -% -\begin{isamarkuptext}% -Code generation is \emph{incremental}: theorems - and abstract intermediate code are cached and extended on demand. - The cache may be partially or fully dropped if the underlying - executable content of the theory changes. - Implementation of caching is supposed to transparently - hid away the details from the user. Anyway, caching - reaches the surface by using a slightly more general form - of the \isa{{\isasymCODEGEN}}: either the list of constants or the - list of serialization expressions may be dropped. If no - serialization expressions are given, only abstract code - is generated and cached; if no constants are given, the - current cache is serialized. +\lstsml{Thy/examples/class.ocaml} - For explorative purpose, the - \isa{{\isasymCODETHMS}} command may prove useful:% -\end{isamarkuptext}% -\isamarkuptrue% -\isacommand{code{\isacharunderscore}thms}\isamarkupfalse% -% -\begin{isamarkuptext}% -\noindent print all cached defining equations (i.e.~\emph{after} - any applied transformation). A - list of constants may be given; their function - equations are added to the cache if not already present. - - Similarly, the \isa{{\isasymCODEDEPS}} command shows a graph - visualizing dependencies between defining equations.% + \medskip The explicit association of constants + to classes can be inspected using the \isa{{\isasymPRINTCLASSES}}% \end{isamarkuptext}% \isamarkuptrue% % @@ -603,7 +566,7 @@ \end{isamarkuptext}% \isamarkuptrue% % -\isamarkupsubsection{Library theories% +\isamarkupsubsection{Library theories \label{sec:library}% } \isamarkuptrue% % @@ -616,6 +579,13 @@ \begin{description} + \item[\isa{Pretty{\isacharunderscore}Int}] represents HOL integers by big + integer literals in target languages. + \item[\isa{Pretty{\isacharunderscore}Char}] represents HOL characters by + character literals in target languages. + \item[\isa{Pretty{\isacharunderscore}Char{\isacharunderscore}chr}] like \isa{Pretty{\isacharunderscore}Char{\isacharunderscore}chr}, + but also offers treatment of character codes; includes + \isa{Pretty{\isacharunderscore}Int}. \item[\isa{ExecutableSet}] allows to generate code for finite sets using lists. \item[\isa{ExecutableRat}] \label{exec_rat} implements rational @@ -623,10 +593,10 @@ \item[\isa{EfficientNat}] \label{eff_nat} implements natural numbers by integers, which in general will result in higher efficency; pattern matching with \isa{{\isadigit{0}}} / \isa{Suc} - is eliminated. + is eliminated; includes \isa{Pretty{\isacharunderscore}Int}. \item[\isa{MLString}] provides an additional datatype \isa{mlstring}; in the HOL default setup, strings in HOL are mapped to list - of chars in SML; values of type \isa{mlstring} are + of HOL characters in SML; values of type \isa{mlstring} are mapped to strings in SML. \end{description}% @@ -651,7 +621,6 @@ 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 respectively. - Some common applications:% \end{isamarkuptext}% \isamarkuptrue% @@ -745,10 +714,222 @@ \end{isamarkuptext}% \isamarkuptrue% % +\isamarkupsubsection{Concerning operational equality% +} +\isamarkuptrue% +% +\begin{isamarkuptext}% +Surely you have already noticed how equality is treated + by the code generator:% +\end{isamarkuptext}% +\isamarkuptrue% +\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 +\ \ {\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 + performs an explicit equality check.% +\end{isamarkuptext}% +\isamarkuptrue% +\isacommand{code{\isacharunderscore}gen}\isamarkupfalse% +\ collect{\isacharunderscore}duplicates\ {\isacharparenleft}SML\ {\isachardoublequoteopen}examples{\isacharslash}collect{\isacharunderscore}duplicates{\isachardot}ML{\isachardoublequoteclose}{\isacharparenright}% +\begin{isamarkuptext}% +\lstsml{Thy/examples/collect_duplicates.ML}% +\end{isamarkuptext}% +\isamarkuptrue% +% +\begin{isamarkuptext}% +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:% +\end{isamarkuptext}% +\isamarkuptrue% +% +\isadelimML +% +\endisadelimML +% +\isatagML +% +\endisatagML +{\isafoldML}% +% +\isadelimML +% +\endisadelimML +\isacommand{class}\isamarkupfalse% +\ 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}}; + the preprocessing framework does the rest. + For datatypes, instances of \isa{eq} are implicitly derived + when possible. + + Though this \isa{eq} class is designed to get rarely in + the way, a subtlety + enters the stage when definitions of overloaded constants + are dependent on operational equality. For example, let + us define a lexicographic ordering on tuples:% +\end{isamarkuptext}% +\isamarkuptrue% +% +\isadelimML +% +\endisadelimML +% +\isatagML +% +\endisatagML +{\isafoldML}% +% +\isadelimML +% +\endisadelimML +\isacommand{instance}\isamarkupfalse% +\ {\isacharasterisk}\ {\isacharcolon}{\isacharcolon}\ {\isacharparenleft}ord{\isacharcomma}\ ord{\isacharparenright}\ ord\isanewline +\ \ less{\isacharunderscore}prod{\isacharunderscore}def{\isacharcolon}\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 +\ \ less{\isacharunderscore}eq{\isacharunderscore}prod{\isacharunderscore}def{\isacharcolon}\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 +\ \ \ \ 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 +% +\isatagproof +\isacommand{{\isachardot}{\isachardot}}\isamarkupfalse% +% +\endisatagproof +{\isafoldproof}% +% +\isadelimproof +% +\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 +\ \ {\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% +\ less{\isacharunderscore}prod{\isacharunderscore}def\ less{\isacharunderscore}eq{\isacharunderscore}prod{\isacharunderscore}def\ \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% +\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}\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}{\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}\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}\isanewline +% +\isadelimproof +\ \ % +\endisadelimproof +% +\isatagproof +\isacommand{unfolding}\isamarkupfalse% +\ ord{\isacharunderscore}prod\ \isacommand{by}\isamarkupfalse% +\ rule{\isacharplus}% +\endisatagproof +{\isafoldproof}% +% +\isadelimproof +% +\endisadelimproof +% +\begin{isamarkuptext}% +\noindent 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}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. 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% +% +\isamarkupsubsection{Programs as sets of theorems% +} +\isamarkuptrue% +% +\begin{isamarkuptext}% +As told in \secref{sec:concept}, code generation is based + on a structured collection of code theorems. + For explorative purpose, this collection + may be inspected using the \isa{{\isasymCODETHMS}} command:% +\end{isamarkuptext}% +\isamarkuptrue% +\isacommand{code{\isacharunderscore}thms}\isamarkupfalse% +\ {\isachardoublequoteopen}op\ mod\ {\isacharcolon}{\isacharcolon}\ nat\ {\isasymRightarrow}\ nat\ {\isasymRightarrow}\ nat{\isachardoublequoteclose}% +\begin{isamarkuptext}% +\noindent prints a table with \emph{all} defining equations + for \isa{op\ mod}, including + \emph{all} defining equations those equations depend + on recursivly. \isa{{\isasymCODETHMS}} provides a convenient + mechanism to inspect the impact of a preprocessor setup + on defining equations. + + Similarly, the \isa{{\isasymCODEDEPS}} command shows a graph + visualizing dependencies between defining equations.% +\end{isamarkuptext}% +\isamarkuptrue% +% \isamarkupsubsection{Customizing serialization% } \isamarkuptrue% % +\isamarkupsubsubsection{Basics% +} +\isamarkuptrue% +% \begin{isamarkuptext}% Consider the following function and its corresponding SML code:% @@ -757,8 +938,7 @@ \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}\isanewline -% +\ \ {\isachardoublequoteopen}in{\isacharunderscore}interval\ {\isacharparenleft}k{\isacharcomma}\ l{\isacharparenright}\ n\ {\isasymlongleftrightarrow}\ k\ {\isasymle}\ n\ {\isasymand}\ n\ {\isasymle}\ l{\isachardoublequoteclose}% \isadelimtt % \endisadelimtt @@ -769,7 +949,6 @@ {\isafoldtt}% % \isadelimtt -\isanewline % \endisadelimtt \isacommand{code{\isacharunderscore}gen}\isamarkupfalse% @@ -777,7 +956,7 @@ \begin{isamarkuptext}% \lstsml{Thy/examples/bool_literal.ML} - Though this is correct code, it is a little bit unsatisfactory: + \noindent 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; @@ -834,7 +1013,7 @@ \begin{isamarkuptext}% \lstsml{Thy/examples/bool_mlbool.ML} - This still is not perfect: the parentheses + \noindent This still is not perfect: the parentheses around the \qt{andalso} expression are superfluous. Though the serializer by no means attempts to imitate the rich Isabelle syntax @@ -864,11 +1043,12 @@ \begin{isamarkuptext}% \lstsml{Thy/examples/bool_infix.ML} + \medskip + Next, we try to map HOL pairs to SML pairs, using the infix ``\verb|*|'' type constructor and parentheses:% \end{isamarkuptext}% \isamarkuptrue% -\isanewline % \isadelimtt % @@ -878,7 +1058,6 @@ \isacommand{code{\isacharunderscore}type}\isamarkupfalse% \ {\isacharasterisk}\isanewline \ \ {\isacharparenleft}SML\ \isakeyword{infix}\ {\isadigit{2}}\ {\isachardoublequoteopen}{\isacharasterisk}{\isachardoublequoteclose}{\isacharparenright}\isanewline -\isanewline \isacommand{code{\isacharunderscore}const}\isamarkupfalse% \ Pair\isanewline \ \ {\isacharparenleft}SML\ {\isachardoublequoteopen}{\isacharbang}{\isacharparenleft}{\isacharparenleft}{\isacharunderscore}{\isacharparenright}{\isacharcomma}{\isacharslash}\ {\isacharparenleft}{\isacharunderscore}{\isacharparenright}{\isacharparenright}{\isachardoublequoteclose}{\isacharparenright}% @@ -898,61 +1077,7 @@ inserts a space which may be used as a break if necessary during pretty printing. - So far, we did only provide more idiomatic serializations for - constructs which would be executable on their own. Target-specific - serializations may also be used to \emph{implement} constructs - which have no explicit notion of executability. For example, - take the HOL integers:% -\end{isamarkuptext}% -\isamarkuptrue% -\isacommand{definition}\isamarkupfalse% -\isanewline -\ \ double{\isacharunderscore}inc\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequoteopen}int\ {\isasymRightarrow}\ int{\isachardoublequoteclose}\ \isakeyword{where}\isanewline -\ \ {\isachardoublequoteopen}double{\isacharunderscore}inc\ k\ {\isacharequal}\ {\isadigit{2}}\ {\isacharasterisk}\ k\ {\isacharplus}\ {\isadigit{1}}{\isachardoublequoteclose}\isanewline -\isanewline -\isacommand{code{\isacharunderscore}gen}\isamarkupfalse% -\ double{\isacharunderscore}inc\ {\isacharparenleft}SML\ {\isachardoublequoteopen}examples{\isacharslash}integers{\isachardot}ML{\isachardoublequoteclose}{\isacharparenright}% -\begin{isamarkuptext}% -will fail: \isa{int} in HOL is implemented using a quotient - type, which does not provide any notion of executability. - \footnote{Eventually, we also want to provide executability - for quotients.}. However, we could use the SML builtin - integers:% -\end{isamarkuptext}% -\isamarkuptrue% -% -\isadelimtt -% -\endisadelimtt -% -\isatagtt -\isacommand{code{\isacharunderscore}type}\isamarkupfalse% -\ int\isanewline -\ \ {\isacharparenleft}SML\ {\isachardoublequoteopen}IntInf{\isachardot}int{\isachardoublequoteclose}{\isacharparenright}\isanewline -\isanewline -\isacommand{code{\isacharunderscore}const}\isamarkupfalse% -\ {\isachardoublequoteopen}op\ {\isacharplus}\ {\isasymColon}\ int\ {\isasymRightarrow}\ int\ {\isasymRightarrow}\ int{\isachardoublequoteclose}\isanewline -\ \ \ \ \isakeyword{and}\ {\isachardoublequoteopen}op\ {\isacharasterisk}\ {\isasymColon}\ int\ {\isasymRightarrow}\ int\ {\isasymRightarrow}\ int{\isachardoublequoteclose}\isanewline -\ \ {\isacharparenleft}SML\ {\isachardoublequoteopen}IntInf{\isachardot}{\isacharplus}\ {\isacharparenleft}{\isacharunderscore}{\isacharcomma}\ {\isacharunderscore}{\isacharparenright}{\isachardoublequoteclose}\ \isakeyword{and}\ {\isachardoublequoteopen}IntInf{\isachardot}{\isacharasterisk}\ {\isacharparenleft}{\isacharunderscore}{\isacharcomma}\ {\isacharunderscore}{\isacharparenright}{\isachardoublequoteclose}{\isacharparenright}% -\endisatagtt -{\isafoldtt}% -% -\isadelimtt -% -\endisadelimtt -\isanewline -\isanewline -\isacommand{code{\isacharunderscore}gen}\isamarkupfalse% -\ double{\isacharunderscore}inc\ {\isacharparenleft}SML\ {\isachardoublequoteopen}examples{\isacharslash}integers{\isachardot}ML{\isachardoublequoteclose}{\isacharparenright}% -\begin{isamarkuptext}% -resulting in: - - \lstsml{Thy/examples/integers.ML}% -\end{isamarkuptext}% -\isamarkuptrue% -% -\begin{isamarkuptext}% -These examples give a glimpse what powerful mechanisms + These examples give a glimpse what mechanisms custom serializations provide; however their usage requires careful thinking in order not to introduce inconsistencies -- or, in other words: @@ -971,284 +1096,6 @@ \end{isamarkuptext}% \isamarkuptrue% % -\isamarkupsubsection{Concerning operational equality% -} -\isamarkuptrue% -% -\begin{isamarkuptext}% -Surely you have already noticed how equality is treated - by the code generator:% -\end{isamarkuptext}% -\isamarkuptrue% -\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 -\ \ {\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 - performs an explicit equality check.% -\end{isamarkuptext}% -\isamarkuptrue% -\isacommand{code{\isacharunderscore}gen}\isamarkupfalse% -\ collect{\isacharunderscore}duplicates\ {\isacharparenleft}SML\ {\isachardoublequoteopen}examples{\isacharslash}collect{\isacharunderscore}duplicates{\isachardot}ML{\isachardoublequoteclose}{\isacharparenright}% -\begin{isamarkuptext}% -\lstsml{Thy/examples/collect_duplicates.ML}% -\end{isamarkuptext}% -\isamarkuptrue% -% -\begin{isamarkuptext}% -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:% -\end{isamarkuptext}% -\isamarkuptrue% -% -\isadelimML -% -\endisadelimML -% -\isatagML -% -\endisatagML -{\isafoldML}% -% -\isadelimML -% -\endisadelimML -\isanewline -\isacommand{class}\isamarkupfalse% -\ 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}}; - the preprocessing framework does the rest.% -\end{isamarkuptext}% -\isamarkuptrue% -% -\isadelimML -% -\endisadelimML -% -\isatagML -% -\endisatagML -{\isafoldML}% -% -\isadelimML -% -\endisadelimML -% -\begin{isamarkuptext}% -For datatypes, instances of \isa{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:% -\end{isamarkuptext}% -\isamarkuptrue% -% -\isamarkupsubsubsection{typedecls interpreted by customary serializations% -} -\isamarkuptrue% -% -\begin{isamarkuptext}% -A common idiom is to use unspecified types for formalizations - and interpret them for a specific target language:% -\end{isamarkuptext}% -\isamarkuptrue% -\isacommand{typedecl}\isamarkupfalse% -\ key\isanewline -\isanewline -\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 -\ \ {\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 -% -\isatagtt -\isacommand{code{\isacharunderscore}type}\isamarkupfalse% -\ key\isanewline -\ \ {\isacharparenleft}SML\ {\isachardoublequoteopen}string{\isachardoublequoteclose}{\isacharparenright}% -\endisatagtt -{\isafoldtt}% -% -\isadelimtt -% -\endisadelimtt -% -\begin{isamarkuptext}% -This, though, is not sufficient: \isa{key} is no instance - of \isa{eq} since \isa{key} is no datatype; the instance - has to be declared manually, including a serialization - for the particular instance of \isa{op\ {\isacharequal}}:% -\end{isamarkuptext}% -\isamarkuptrue% -\isacommand{instance}\isamarkupfalse% -\ key\ {\isacharcolon}{\isacharcolon}\ eq% -\isadelimproof -\ % -\endisadelimproof -% -\isatagproof -\isacommand{{\isachardot}{\isachardot}}\isamarkupfalse% -% -\endisatagproof -{\isafoldproof}% -% -\isadelimproof -% -\endisadelimproof -\isanewline -% -\isadelimtt -\isanewline -% -\endisadelimtt -% -\isatagtt -\isacommand{code{\isacharunderscore}const}\isamarkupfalse% -\ {\isachardoublequoteopen}op\ {\isacharequal}\ {\isasymColon}\ key\ {\isasymRightarrow}\ key\ {\isasymRightarrow}\ bool{\isachardoublequoteclose}\isanewline -\ \ {\isacharparenleft}SML\ {\isachardoublequoteopen}{\isacharbang}{\isacharparenleft}{\isacharparenleft}{\isacharunderscore}\ {\isacharcolon}\ string{\isacharparenright}\ {\isacharequal}\ {\isacharunderscore}{\isacharparenright}{\isachardoublequoteclose}{\isacharparenright}% -\endisatagtt -{\isafoldtt}% -% -\isadelimtt -% -\endisadelimtt -% -\begin{isamarkuptext}% -Then everything goes fine:% -\end{isamarkuptext}% -\isamarkuptrue% -\isacommand{code{\isacharunderscore}gen}\isamarkupfalse% -\ lookup\ {\isacharparenleft}SML\ {\isachardoublequoteopen}examples{\isacharslash}lookup{\isachardot}ML{\isachardoublequoteclose}{\isacharparenright}% -\begin{isamarkuptext}% -\lstsml{Thy/examples/lookup.ML}% -\end{isamarkuptext}% -\isamarkuptrue% -% -\isamarkupsubsubsection{lexicographic orderings% -} -\isamarkuptrue% -% -\begin{isamarkuptext}% -Another subtlety - enters the stage when definitions of overloaded constants - are dependent on operational equality. For example, let - us define a lexicographic ordering on tuples:% -\end{isamarkuptext}% -\isamarkuptrue% -\isacommand{instance}\isamarkupfalse% -\ {\isacharasterisk}\ {\isacharcolon}{\isacharcolon}\ {\isacharparenleft}ord{\isacharcomma}\ ord{\isacharparenright}\ ord\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 -\ \ 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 -\ % -\endisadelimproof -% -\isatagproof -\isacommand{{\isachardot}{\isachardot}}\isamarkupfalse% -% -\endisatagproof -{\isafoldproof}% -% -\isadelimproof -% -\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 -\ \ {\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% -\ less{\isacharunderscore}prod{\isacharunderscore}def\ less{\isacharunderscore}eq{\isacharunderscore}prod{\isacharunderscore}def\ \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}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. 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% -% \isamarkupsubsubsection{Haskell serialization% } \isamarkuptrue% @@ -1261,20 +1108,6 @@ \end{isamarkuptext}% \isamarkuptrue% % -\isadelimML -% -\endisadelimML -% -\isatagML -% -\endisatagML -{\isafoldML}% -% -\isadelimML -% -\endisadelimML -\isanewline -% \isadelimtt % \endisadelimtt @@ -1282,12 +1115,11 @@ \isatagtt \isacommand{code{\isacharunderscore}class}\isamarkupfalse% \ eq\isanewline -\ \ {\isacharparenleft}Haskell\ {\isachardoublequoteopen}Eq{\isachardoublequoteclose}\ \isakeyword{where}\ eq\ {\isasymequiv}\ {\isachardoublequoteopen}{\isacharparenleft}{\isacharequal}{\isacharequal}{\isacharparenright}{\isachardoublequoteclose}{\isacharparenright}\isanewline +\ \ {\isacharparenleft}Haskell\ {\isachardoublequoteopen}Eq{\isachardoublequoteclose}\ \isakeyword{where}\ {\isachardoublequoteopen}op\ {\isacharequal}{\isachardoublequoteclose}\ {\isasymequiv}\ {\isachardoublequoteopen}{\isacharparenleft}{\isacharequal}{\isacharequal}{\isacharparenright}{\isachardoublequoteclose}{\isacharparenright}\isanewline \isanewline \isacommand{code{\isacharunderscore}const}\isamarkupfalse% -\ eq\isanewline -\ \ {\isacharparenleft}Haskell\ \isakeyword{infixl}\ {\isadigit{4}}\ {\isachardoublequoteopen}{\isacharequal}{\isacharequal}{\isachardoublequoteclose}{\isacharparenright}\isanewline -% +\ {\isachardoublequoteopen}op\ {\isacharequal}{\isachardoublequoteclose}\isanewline +\ \ {\isacharparenleft}Haskell\ \isakeyword{infixl}\ {\isadigit{4}}\ {\isachardoublequoteopen}{\isacharequal}{\isacharequal}{\isachardoublequoteclose}{\isacharparenright}% \endisatagtt {\isafoldtt}% % @@ -1295,19 +1127,6 @@ % \endisadelimtt % -\isadelimML -% -\endisadelimML -% -\isatagML -% -\endisatagML -{\isafoldML}% -% -\isadelimML -% -\endisadelimML -% \begin{isamarkuptext}% A problem now occurs whenever a type which is an instance of \isa{eq} in HOL is mapped @@ -1374,78 +1193,119 @@ % \endisadelimtt % -\isamarkupsubsection{Types matter% +\isamarkupsubsubsection{Pretty printing% +} +\isamarkuptrue% +% +\begin{isamarkuptext}% +The serializer provides ML interfaces to set up + pretty serializations for expressions like lists, numerals + and characters; these are + monolithic stubs and should only be used with the + theories introduces in \secref{sec:library}.% +\end{isamarkuptext}% +\isamarkuptrue% +% +\isamarkupsubsection{Constructor sets for datatypes% } \isamarkuptrue% % \begin{isamarkuptext}% -Imagine the following quick-and-dirty setup for implementing - some kind of sets as lists in SML:% +Conceptually, any datatype is spanned by a set of + \emph{constructors} of type \isa{{\isasymtau}\ {\isacharequal}\ {\isasymdots}\ {\isasymRightarrow}\ {\isasymkappa}\ {\isasymalpha}\isactrlisub {\isadigit{1}}\ {\isasymdots}\ {\isasymalpha}\isactrlisub n} + where \isa{{\isacharbraceleft}{\isasymalpha}\isactrlisub {\isadigit{1}}{\isacharcomma}\ {\isasymdots}{\isacharcomma}\ {\isasymalpha}\isactrlisub n{\isacharbraceright}} is excactly the set of \emph{all} + type variables in \isa{{\isasymtau}}. The HOL datatype package + by default registers any new datatype in the table + of datatypes, which may be inspected using + the \isa{{\isasymPRINTCODESETUP}} command. + + In some cases, it may be convenient to alter or + extend this table; as an example, we show + how to implement finite sets by lists + using the conversion \isa{{\isachardoublequote}set\ {\isasymColon}\ {\isacharprime}a\ list\ {\isasymRightarrow}\ {\isacharprime}a\ set{\isachardoublequote}} + as constructor:% \end{isamarkuptext}% \isamarkuptrue% -% -\isadelimtt -% -\endisadelimtt -% -\isatagtt -\isacommand{code{\isacharunderscore}type}\isamarkupfalse% +\isacommand{code{\isacharunderscore}datatype}\isamarkupfalse% \ set\isanewline -\ \ {\isacharparenleft}SML\ {\isachardoublequoteopen}{\isacharunderscore}\ list{\isachardoublequoteclose}{\isacharparenright}\isanewline -\isanewline -\isacommand{code{\isacharunderscore}const}\isamarkupfalse% -\ {\isachardoublequoteopen}{\isacharbraceleft}{\isacharbraceright}{\isachardoublequoteclose}\ \isakeyword{and}\ insert\isanewline -\ \ {\isacharparenleft}SML\ {\isachardoublequoteopen}{\isacharbang}{\isacharbrackleft}{\isacharbrackright}{\isachardoublequoteclose}\ \isakeyword{and}\ \isakeyword{infixl}\ {\isadigit{7}}\ {\isachardoublequoteopen}{\isacharcolon}{\isacharcolon}{\isachardoublequoteclose}{\isacharparenright}% -\endisatagtt -{\isafoldtt}% -% -\isadelimtt -% -\endisadelimtt -\isanewline -\isanewline -\isacommand{definition}\isamarkupfalse% \isanewline -\ \ dummy{\isacharunderscore}set\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequoteopen}{\isacharparenleft}nat\ {\isasymRightarrow}\ nat{\isacharparenright}\ set{\isachardoublequoteclose}\ \isakeyword{where}\isanewline -\ \ {\isachardoublequoteopen}dummy{\isacharunderscore}set\ {\isacharequal}\ {\isacharbraceleft}Suc{\isacharbraceright}{\isachardoublequoteclose}% -\begin{isamarkuptext}% -Then code generation for \isa{dummy{\isacharunderscore}set} will fail. - Why? A glimpse at the defining equations will offer:% -\end{isamarkuptext}% -\isamarkuptrue% -\isacommand{code{\isacharunderscore}thms}\isamarkupfalse% -\ insert% -\begin{isamarkuptext}% -This reveals the defining equation \isa{insert\ {\isacharquery}a\ {\isacharquery}B\ {\isasymequiv}\ {\isacharbraceleft}x{\isachardot}\ x\ {\isacharequal}\ {\isacharquery}a{\isacharbraceright}\ {\isasymunion}\ {\isacharquery}B} - for \isa{insert}, which is operationally meaningless - but forces an equality constraint on the set members - (which is not satisfiable if the set members are functions). - Even when using set of natural numbers (which are an instance - of \emph{eq}), we run into a problem:% -\end{isamarkuptext}% -\isamarkuptrue% -\isacommand{definition}\isamarkupfalse% -\isanewline -\ \ foobar{\isacharunderscore}set\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequoteopen}nat\ set{\isachardoublequoteclose}\ \isakeyword{where}\isanewline -\ \ {\isachardoublequoteopen}foobar{\isacharunderscore}set\ {\isacharequal}\ {\isacharbraceleft}{\isadigit{0}}{\isacharcomma}\ {\isadigit{1}}{\isacharcomma}\ {\isadigit{2}}{\isacharbraceright}{\isachardoublequoteclose}% -\begin{isamarkuptext}% -In this case the serializer would complain that \isa{insert} - expects dictionaries (namely an \emph{eq} dictionary) but - has also been given a customary serialization. - - \fixme[needs rewrite] The solution to this dilemma:% -\end{isamarkuptext}% -\isamarkuptrue% \isacommand{lemma}\isamarkupfalse% -\ {\isacharbrackleft}code\ func{\isacharbrackright}{\isacharcolon}\isanewline -\ \ {\isachardoublequoteopen}insert\ {\isacharequal}\ insert{\isachardoublequoteclose}% +\ {\isacharbrackleft}code\ func{\isacharbrackright}{\isacharcolon}\ {\isachardoublequoteopen}{\isacharbraceleft}{\isacharbraceright}\ {\isacharequal}\ set\ {\isacharbrackleft}{\isacharbrackright}{\isachardoublequoteclose}% \isadelimproof \ % \endisadelimproof % \isatagproof -\isacommand{{\isachardot}{\isachardot}}\isamarkupfalse% +\isacommand{by}\isamarkupfalse% +\ simp% +\endisatagproof +{\isafoldproof}% +% +\isadelimproof +% +\endisadelimproof +\isanewline +\isanewline +\isacommand{lemma}\isamarkupfalse% +\ {\isacharbrackleft}code\ func{\isacharbrackright}{\isacharcolon}\ {\isachardoublequoteopen}insert\ x\ {\isacharparenleft}set\ xs{\isacharparenright}\ {\isacharequal}\ set\ {\isacharparenleft}x{\isacharhash}xs{\isacharparenright}{\isachardoublequoteclose}% +\isadelimproof +\ % +\endisadelimproof +% +\isatagproof +\isacommand{by}\isamarkupfalse% +\ simp% +\endisatagproof +{\isafoldproof}% +% +\isadelimproof +% +\endisadelimproof +\isanewline +\isanewline +\isacommand{lemma}\isamarkupfalse% +\ {\isacharbrackleft}code\ func{\isacharbrackright}{\isacharcolon}\ {\isachardoublequoteopen}x\ {\isasymin}\ set\ xs\ {\isasymlongleftrightarrow}\ x\ mem\ xs{\isachardoublequoteclose}% +\isadelimproof +\ % +\endisadelimproof % +\isatagproof +\isacommand{by}\isamarkupfalse% +\ {\isacharparenleft}induct\ xs{\isacharparenright}\ simp{\isacharunderscore}all% +\endisatagproof +{\isafoldproof}% +% +\isadelimproof +% +\endisadelimproof +\isanewline +\isanewline +\isacommand{lemma}\isamarkupfalse% +\ {\isacharbrackleft}code\ func{\isacharbrackright}{\isacharcolon}\ {\isachardoublequoteopen}xs\ {\isasymunion}\ set\ ys\ {\isacharequal}\ foldr\ insert\ ys\ xs{\isachardoublequoteclose}% +\isadelimproof +\ % +\endisadelimproof +% +\isatagproof +\isacommand{by}\isamarkupfalse% +\ {\isacharparenleft}induct\ ys{\isacharparenright}\ simp{\isacharunderscore}all% +\endisatagproof +{\isafoldproof}% +% +\isadelimproof +% +\endisadelimproof +\isanewline +\isanewline +\isacommand{lemma}\isamarkupfalse% +\ {\isacharbrackleft}code\ func{\isacharbrackright}{\isacharcolon}\ {\isachardoublequoteopen}{\isasymUnion}set\ xs\ {\isacharequal}\ foldr\ {\isacharparenleft}op\ {\isasymunion}{\isacharparenright}\ xs\ {\isacharbraceleft}{\isacharbraceright}{\isachardoublequoteclose}% +\isadelimproof +\ % +\endisadelimproof +% +\isatagproof +\isacommand{by}\isamarkupfalse% +\ {\isacharparenleft}induct\ xs{\isacharparenright}\ simp{\isacharunderscore}all% \endisatagproof {\isafoldproof}% % @@ -1455,51 +1315,14 @@ \isanewline \isanewline \isacommand{code{\isacharunderscore}gen}\isamarkupfalse% -\ dummy{\isacharunderscore}set\ foobar{\isacharunderscore}set\ {\isacharparenleft}SML\ {\isachardoublequoteopen}examples{\isacharslash}dirty{\isacharunderscore}set{\isachardot}ML{\isachardoublequoteclose}{\isacharparenright}% +\ {\isachardoublequoteopen}{\isacharbraceleft}{\isacharbraceright}{\isachardoublequoteclose}\ insert\ {\isachardoublequoteopen}op\ {\isasymin}{\isachardoublequoteclose}\ {\isachardoublequoteopen}op\ {\isasymunion}{\isachardoublequoteclose}\ {\isachardoublequoteopen}Union{\isachardoublequoteclose}\ {\isacharparenleft}SML\ {\isachardoublequoteopen}examples{\isacharslash}set{\isacharunderscore}list{\isachardot}ML{\isachardoublequoteclose}{\isacharparenright}% \begin{isamarkuptext}% -\lstsml{Thy/examples/dirty_set.ML} - - Reflexive defining equations by convention are dropped:% -\end{isamarkuptext}% -\isamarkuptrue% -\isacommand{code{\isacharunderscore}thms}\isamarkupfalse% -\ insert% -\begin{isamarkuptext}% -will show \emph{no} defining equations for insert. +\lstsml{Thy/examples/set_list.ML} - Note that the sort constraints of reflexive equations - are considered; so% -\end{isamarkuptext}% -\isamarkuptrue% -\isacommand{lemma}\isamarkupfalse% -\ {\isacharbrackleft}code\ func{\isacharbrackright}{\isacharcolon}\isanewline -\ \ {\isachardoublequoteopen}{\isacharparenleft}insert\ {\isasymColon}\ {\isacharprime}a{\isasymColon}eq\ {\isasymRightarrow}\ {\isacharprime}a\ set\ {\isasymRightarrow}\ {\isacharprime}a\ set{\isacharparenright}\ {\isacharequal}\ insert{\isachardoublequoteclose}% -\isadelimproof -\ % -\endisadelimproof -% -\isatagproof -\isacommand{{\isachardot}{\isachardot}}\isamarkupfalse% -% -\endisatagproof -{\isafoldproof}% -% -\isadelimproof -% -\endisadelimproof -% -\begin{isamarkuptext}% -would mean nothing else than to introduce the evil - sort constraint by hand.% -\end{isamarkuptext}% -\isamarkuptrue% -% -\isamarkupsubsection{Constructor sets for datatypes% -} -\isamarkuptrue% -% -\begin{isamarkuptext}% -\fixme% + \medskip + + Changing the representation of existing datatypes requires + some care with respect to pattern matching and such.% \end{isamarkuptext}% \isamarkuptrue% % @@ -1532,6 +1355,25 @@ \end{isamarkuptext}% \isamarkuptrue% % +\isamarkupsubsection{Incremental code generation% +} +\isamarkuptrue% +% +\begin{isamarkuptext}% +Code generation is \emph{incremental}: theorems + and abstract intermediate code are cached and extended on demand. + The cache may be partially or fully dropped if the underlying + executable content of the theory changes. + Implementation of caching is supposed to transparently + hid away the details from the user. Anyway, caching + reaches the surface by using a slightly more general form + of the \isa{{\isasymCODETHMS}}, \isa{{\isasymCODEDEPS}} + and \isa{{\isasymCODEGEN}} commands: the list of constants + may be omitted. Then, all constants with code theorems + in the current cache are referred to.% +\end{isamarkuptext}% +\isamarkuptrue% +% \isamarkupsubsection{Axiomatic extensions% } \isamarkuptrue% @@ -1611,6 +1453,8 @@ \begin{isamarkuptext}% \lstsml{Thy/examples/arbitrary.ML} + \medskip + Another axiomatic extension is code generation for abstracted types. For this, the \isa{ExecutableRat} (see \secref{exec_rat}) @@ -1911,13 +1755,13 @@ \item \isa{merge} merging two data slots. - \item \isa{purge}~\isa{thy}~\isa{cs} propagates changes in executable content; + \item \isa{purge}~\isa{thy}~\isa{consts} propagates changes in executable content; if possible, the current theory context is handed over as argument \isa{thy} (if there is no current theory context (e.g.~during - theory merge, \verb|NONE|); \isa{cs} indicates the kind + theory merge, \verb|NONE|); \isa{consts} indicates the kind of change: \verb|NONE| stands for a fundamental change - which invalidates any existing code, \isa{SOME\ cs} - hints that executable content for constants \isa{cs} + which invalidates any existing code, \isa{SOME\ consts} + hints that executable content for constants \isa{consts} has changed. \end{description} @@ -1948,6 +1792,109 @@ \end{isamarkuptext}% \isamarkuptrue% % +\isamarkupsubsubsection{Building implementable systems fo defining equations% +} +\isamarkuptrue% +% +\begin{isamarkuptext}% +Out of the executable content of a theory, a normalized + defining equation systems may be constructed containing + function definitions for constants. The system is cached + until its underlying executable content changes. + + Defining equations are retrieved by instantiation + of the functor \verb|CodegenFuncgrRetrieval| + which takes two arguments: + + \medskip + \begin{tabular}{l} + \isa{val\ name{\isacharcolon}\ string} \\ + \isa{val\ rewrites{\isacharcolon}\ theory\ {\isasymrightarrow}\ thm\ list} + \end{tabular} + + \begin{description} + + \item \isa{name} is a system-wide unique name identifying + this particular system of defining equations. + + \item \isa{rewrites} specifies a set of theory-dependent + rewrite rules which are added to the preprocessor setup; + if no additional preprocessing is required, pass + a function returning an empty list. + + \end{description} + + An instance of \verb|CodegenFuncgrRetrieval| in essence + provides the following interface: + + \medskip + \begin{tabular}{l} + \isa{make{\isacharcolon}\ theory\ {\isasymrightarrow}\ CodegenConsts{\isachardot}const\ list\ {\isasymrightarrow}\ CodegenFuncgr{\isachardot}T} \\ + \end{tabular} + + \begin{description} + + \item \isa{make}~\isa{thy}~\isa{consts} returns + a system of defining equations which is guaranteed + to contain all defining equations for constants \isa{consts} + including all defining equations any defining equation + for any constant in \isa{consts} depends on. + + \end{description} + + Systems of defining equations are graphs accesible by the + following operations:% +\end{isamarkuptext}% +\isamarkuptrue% +% +\isadelimmlref +% +\endisadelimmlref +% +\isatagmlref +% +\begin{isamarkuptext}% +\begin{mldecls} + \indexmltype{CodegenFuncgr.T}\verb|type CodegenFuncgr.T| \\ + \indexml{CodegenFuncgr.funcs}\verb|CodegenFuncgr.funcs: CodegenFuncgr.T -> CodegenConsts.const -> thm list| \\ + \indexml{CodegenFuncgr.typ}\verb|CodegenFuncgr.typ: CodegenFuncgr.T -> CodegenConsts.const -> typ| \\ + \indexml{CodegenFuncgr.deps}\verb|CodegenFuncgr.deps: CodegenFuncgr.T|\isasep\isanewline% +\verb| -> CodegenConsts.const list -> CodegenConsts.const list list| \\ + \indexml{CodegenFuncgr.all}\verb|CodegenFuncgr.all: CodegenFuncgr.T -> CodegenConsts.const list| + \end{mldecls} + + \begin{description} + + \item \verb|CodegenFuncgr.T| represents + a normalized defining equation system. + + \item \verb|CodegenFuncgr.funcs|~\isa{funcgr}~\isa{const} + retrieves defining equiations for constant \isa{const}. + + \item \verb|CodegenFuncgr.typ|~\isa{funcgr}~\isa{const} + retrieves function type for constant \isa{const}. + + \item \verb|CodegenFuncgr.deps|~\isa{funcgr}~\isa{consts} + returns the transitive closure of dependencies for + constants \isa{consts} as a partitioning where each partition + corresponds to a strongly connected component of + dependencies and any partition does \emph{not} + depend on partitions further left. + + \item \verb|CodegenFuncgr.all|~\isa{funcgr} + returns all currently represented constants. + + \end{description}% +\end{isamarkuptext}% +\isamarkuptrue% +% +\endisatagmlref +{\isafoldmlref}% +% +\isadelimmlref +% +\endisadelimmlref +% \isamarkupsubsubsection{Datatype hooks% } \isamarkuptrue% diff -r 4b77a43f7f58 -r e3962371f568 doc-src/IsarAdvanced/Codegen/Thy/examples/Codegen.hs --- a/doc-src/IsarAdvanced/Codegen/Thy/examples/Codegen.hs Thu Apr 26 12:00:12 2007 +0200 +++ b/doc-src/IsarAdvanced/Codegen/Thy/examples/Codegen.hs Thu Apr 26 13:32:55 2007 +0200 @@ -6,7 +6,7 @@ nulla :: a; }; -heada :: (Codegen.Null a) => [a] -> a; +heada :: (Codegen.Null b) => [b] -> b; heada (x : xs) = x; heada [] = Codegen.nulla; diff -r 4b77a43f7f58 -r e3962371f568 doc-src/IsarAdvanced/Codegen/Thy/examples/class.ML --- a/doc-src/IsarAdvanced/Codegen/Thy/examples/class.ML Thu Apr 26 12:00:12 2007 +0200 +++ b/doc-src/IsarAdvanced/Codegen/Thy/examples/class.ML Thu Apr 26 13:32:55 2007 +0200 @@ -14,8 +14,8 @@ type 'a null = {null : 'a}; fun null (A_:'a null) = #null A_; -fun head A_ (x :: xs) = x - | head A_ [] = null A_; +fun head B_ (x :: xs) = x + | head B_ [] = null B_; val null_option : 'a option = NONE; diff -r 4b77a43f7f58 -r e3962371f568 doc-src/IsarAdvanced/Codegen/Thy/examples/class.ocaml --- a/doc-src/IsarAdvanced/Codegen/Thy/examples/class.ocaml Thu Apr 26 12:00:12 2007 +0200 +++ b/doc-src/IsarAdvanced/Codegen/Thy/examples/class.ocaml Thu Apr 26 13:32:55 2007 +0200 @@ -14,8 +14,8 @@ type 'a null = {null : 'a};; let null _A = _A.null;; -let rec head _A = function x :: xs -> x - | [] -> null _A;; +let rec head _B = function x :: xs -> x + | [] -> null _B;; let rec null_option = None;; diff -r 4b77a43f7f58 -r e3962371f568 doc-src/IsarAdvanced/Codegen/Thy/examples/collect_duplicates.ML --- a/doc-src/IsarAdvanced/Codegen/Thy/examples/collect_duplicates.ML Thu Apr 26 12:00:12 2007 +0200 +++ b/doc-src/IsarAdvanced/Codegen/Thy/examples/collect_duplicates.ML Thu Apr 26 13:32:55 2007 +0200 @@ -21,12 +21,12 @@ structure Codegen = struct -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_ xs ys [] = xs; +fun collect_duplicates B_ xs ys (z :: zs) = + (if List.memberl B_ z xs + then (if List.memberl B_ z ys then collect_duplicates B_ xs ys zs + else collect_duplicates B_ xs (z :: ys) zs) + else collect_duplicates B_ (z :: xs) (z :: ys) zs) + | collect_duplicates B_ xs ys [] = xs; end; (*struct Codegen*) diff -r 4b77a43f7f58 -r e3962371f568 doc-src/IsarAdvanced/Codegen/Thy/examples/dirty_set.ML --- a/doc-src/IsarAdvanced/Codegen/Thy/examples/dirty_set.ML Thu Apr 26 12:00:12 2007 +0200 +++ b/doc-src/IsarAdvanced/Codegen/Thy/examples/dirty_set.ML Thu Apr 26 13:32:55 2007 +0200 @@ -11,9 +11,73 @@ structure Integer = struct +datatype bit = B0 | B1; + +datatype int = Pls | Min | Bit of int * bit | Number_of_int of int; + +fun pred (Bit (k, B0)) = Bit (pred k, B1) + | pred (Bit (k, B1)) = Bit (k, B0) + | pred Min = Bit (Min, B0) + | pred Pls = Min; + +fun uminus_int (Number_of_int w) = Number_of_int (uminus_int w) + | uminus_int (Bit (k, B0)) = Bit (uminus_int k, B0) + | uminus_int (Bit (k, B1)) = Bit (pred (uminus_int k), B1) + | uminus_int Min = Bit (Pls, B1) + | uminus_int Pls = Pls; + +fun succ (Bit (k, B0)) = Bit (k, B1) + | succ (Bit (k, B1)) = Bit (succ k, B0) + | succ Min = Pls + | succ Pls = Bit (Pls, B1); + +fun plus_int (Number_of_int v) (Number_of_int w) = + Number_of_int (plus_int v w) + | plus_int k Min = pred k + | plus_int k Pls = k + | plus_int (Bit (k, B1)) (Bit (l, B1)) = Bit (plus_int k (succ l), B0) + | plus_int (Bit (k, B1)) (Bit (l, B0)) = Bit (plus_int k l, B1) + | plus_int (Bit (k, B0)) (Bit (l, b)) = Bit (plus_int k l, b) + | plus_int Min k = pred k + | plus_int Pls k = k; + +fun minus_int (Number_of_int v) (Number_of_int w) = + Number_of_int (plus_int v (uminus_int w)) + | minus_int z w = plus_int z (uminus_int w); + +fun less_eq_int (Number_of_int k) (Number_of_int l) = less_eq_int k l + | less_eq_int (Bit (k1, B1)) (Bit (k2, B0)) = less_int k1 k2 + | less_eq_int (Bit (k1, v)) (Bit (k2, B1)) = less_eq_int k1 k2 + | less_eq_int (Bit (k1, B0)) (Bit (k2, v)) = less_eq_int k1 k2 + | less_eq_int (Bit (k, v)) Min = less_eq_int k Min + | less_eq_int (Bit (k, B1)) Pls = less_int k Pls + | less_eq_int (Bit (k, B0)) Pls = less_eq_int k Pls + | less_eq_int Min (Bit (k, B1)) = less_eq_int Min k + | less_eq_int Min (Bit (k, B0)) = less_int Min k + | less_eq_int Min Min = true + | less_eq_int Min Pls = true + | less_eq_int Pls (Bit (k, v)) = less_eq_int Pls k + | less_eq_int Pls Min = false + | less_eq_int Pls Pls = true +and less_int (Number_of_int k) (Number_of_int l) = less_int k l + | less_int (Bit (k1, B0)) (Bit (k2, B1)) = less_eq_int k1 k2 + | less_int (Bit (k1, B1)) (Bit (k2, v)) = less_int k1 k2 + | less_int (Bit (k1, v)) (Bit (k2, B0)) = less_int k1 k2 + | less_int (Bit (k, B1)) Min = less_int k Min + | less_int (Bit (k, B0)) Min = less_eq_int k Min + | less_int (Bit (k, v)) Pls = less_int k Pls + | less_int Min (Bit (k, v)) = less_int Min k + | less_int Min Min = false + | less_int Min Pls = true + | less_int Pls (Bit (k, B1)) = less_eq_int Pls k + | less_int Pls (Bit (k, B0)) = less_int Pls k + | less_int Pls Min = false + | less_int Pls Pls = false; + fun nat_aux n i = - (if IntInf.<= (i, (0 : IntInf.int)) then n - else nat_aux (Nat.Suc n) (IntInf.- (i, (1 : IntInf.int)))); + (if less_eq_int i (Number_of_int Pls) then n + else nat_aux (Nat.Suc n) + (minus_int i (Number_of_int (Bit (Pls, B1))))); fun nat i = nat_aux Nat.Zero_nat i; @@ -26,7 +90,12 @@ val foobar_set : Nat.nat list = Nat.Zero_nat :: - (Nat.Suc Nat.Zero_nat :: (Integer.nat (2 : IntInf.int) :: [])); + (Nat.Suc Nat.Zero_nat :: + (Integer.nat + (Integer.Number_of_int + (Integer.Bit + (Integer.Bit (Integer.Pls, Integer.B1), Integer.B0))) + :: [])); end; (*struct Codegen*) diff -r 4b77a43f7f58 -r e3962371f568 doc-src/IsarAdvanced/Codegen/Thy/examples/integers.ML --- a/doc-src/IsarAdvanced/Codegen/Thy/examples/integers.ML Thu Apr 26 12:00:12 2007 +0200 +++ b/doc-src/IsarAdvanced/Codegen/Thy/examples/integers.ML Thu Apr 26 13:32:55 2007 +0200 @@ -1,11 +1,58 @@ structure ROOT = struct +structure Integer = +struct + +datatype bit = B0 | B1; + +datatype int = Pls | Min | Bit of int * bit | Number_of_int of int; + +fun pred (Bit (k, B0)) = Bit (pred k, B1) + | pred (Bit (k, B1)) = Bit (k, B0) + | pred Min = Bit (Min, B0) + | pred Pls = Min; + +fun succ (Bit (k, B0)) = Bit (k, B1) + | succ (Bit (k, B1)) = Bit (succ k, B0) + | succ Min = Pls + | succ Pls = Bit (Pls, B1); + +fun plus_int (Number_of_int v) (Number_of_int w) = + Number_of_int (plus_int v w) + | plus_int k Min = pred k + | plus_int k Pls = k + | plus_int (Bit (k, B1)) (Bit (l, B1)) = Bit (plus_int k (succ l), B0) + | plus_int (Bit (k, B1)) (Bit (l, B0)) = Bit (plus_int k l, B1) + | plus_int (Bit (k, B0)) (Bit (l, b)) = Bit (plus_int k l, b) + | plus_int Min k = pred k + | plus_int Pls k = k; + +fun uminus_int (Number_of_int w) = Number_of_int (uminus_int w) + | uminus_int (Bit (k, B0)) = Bit (uminus_int k, B0) + | uminus_int (Bit (k, B1)) = Bit (pred (uminus_int k), B1) + | uminus_int Min = Bit (Pls, B1) + | uminus_int Pls = Pls; + +fun times_int (Number_of_int v) (Number_of_int w) = + Number_of_int (times_int v w) + | times_int (Bit (k, B0)) l = Bit (times_int k l, B0) + | times_int (Bit (k, B1)) l = plus_int (Bit (times_int k l, B0)) l + | times_int Min k = uminus_int k + | times_int Pls w = Pls; + +end; (*struct Integer*) + structure Codegen = struct fun double_inc k = - IntInf.+ ((IntInf.* ((2 : IntInf.int), k)), (1 : IntInf.int)); + Integer.plus_int + (Integer.times_int + (Integer.Number_of_int + (Integer.Bit (Integer.Bit (Integer.Pls, Integer.B1), Integer.B0))) + k) + (Integer.Number_of_int (Integer.Bit (Integer.Pls, Integer.B1))); end; (*struct Codegen*) diff -r 4b77a43f7f58 -r e3962371f568 doc-src/IsarAdvanced/Codegen/Thy/examples/set_list.ML --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/doc-src/IsarAdvanced/Codegen/Thy/examples/set_list.ML Thu Apr 26 13:32:55 2007 +0200 @@ -0,0 +1,41 @@ +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 List = +struct + +fun foldr f (x :: xs) a = f x (foldr f xs a) + | foldr f [] a = a; + +fun memberl A_ x (y :: ys) = + Code_Generator.op_eq A_ x y orelse memberl A_ x ys + | memberl A_ x [] = false; + +end; (*struct List*) + +structure Set = +struct + +datatype 'a set = Set of 'a list; + +fun opa A_ x (Set xs) = List.memberl A_ x xs; + +val empty : 'a set = Set []; + +fun insert x (Set xs) = Set (x :: xs); + +fun op_Un xs (Set ys) = List.foldr insert ys xs; + +fun union (Set xs) = List.foldr op_Un xs empty; + +end; (*struct Set*) + +end; (*struct ROOT*) diff -r 4b77a43f7f58 -r e3962371f568 doc-src/IsarAdvanced/Codegen/Thy/examples/tree.ML --- a/doc-src/IsarAdvanced/Codegen/Thy/examples/tree.ML Thu Apr 26 12:00:12 2007 +0200 +++ b/doc-src/IsarAdvanced/Codegen/Thy/examples/tree.ML Thu Apr 26 13:32:55 2007 +0200 @@ -47,6 +47,8 @@ Nibble5 | Nibble6 | Nibble7 | Nibble8 | Nibble9 | NibbleA | NibbleB | NibbleC | NibbleD | NibbleE | NibbleF; +datatype char = Char of nibble * nibble; + end; (*struct List*) structure Codegen = @@ -55,19 +57,26 @@ datatype ('a, 'b) searchtree = Leaf of 'a * 'b | Branch of ('a, 'b) searchtree * 'a * ('a, 'b) searchtree; -fun update (A1_, A2_) (it, entry) (Branch (t1, key, t2)) = - (if Orderings.less_eq A2_ it key - then Branch (update (A1_, A2_) (it, entry) t1, key, t2) - else Branch (t1, key, update (A1_, A2_) (it, entry) t2)) - | update (A1_, A2_) (it, entry) (Leaf (key, vala)) = - (if Code_Generator.op_eq A1_ it key then Leaf (key, entry) - else (if Orderings.less_eq A2_ it key +fun update (C1_, C2_) (it, entry) (Branch (t1, key, t2)) = + (if Orderings.less_eq C2_ it key + then Branch (update (C1_, C2_) (it, entry) t1, key, t2) + else Branch (t1, key, update (C1_, C2_) (it, entry) t2)) + | update (C1_, C2_) (it, entry) (Leaf (key, vala)) = + (if Code_Generator.op_eq C1_ it key then Leaf (key, entry) + else (if Orderings.less_eq C2_ it key then Branch (Leaf (it, entry), it, Leaf (key, vala)) else Branch (Leaf (key, vala), it, Leaf (it, entry)))); fun example n = - update (Nat.eq_nat, Nat.ord_nat) (n, [#"b", #"a", #"r"]) - (Leaf (Nat.Zero_nat, [#"f", #"o", #"o"])); + update (Nat.eq_nat, Nat.ord_nat) + (n, [List.Char (List.Nibble6, List.Nibble2), + List.Char (List.Nibble6, List.Nibble1), + List.Char (List.Nibble7, List.Nibble2)]) + (Leaf + (Nat.Zero_nat, + [List.Char (List.Nibble6, List.Nibble6), + List.Char (List.Nibble6, List.NibbleF), + List.Char (List.Nibble6, List.NibbleF)])); end; (*struct Codegen*) diff -r 4b77a43f7f58 -r e3962371f568 doc-src/IsarAdvanced/Codegen/codegen.tex --- a/doc-src/IsarAdvanced/Codegen/codegen.tex Thu Apr 26 12:00:12 2007 +0200 +++ b/doc-src/IsarAdvanced/Codegen/codegen.tex Thu Apr 26 13:32:55 2007 +0200 @@ -44,6 +44,7 @@ \newcommand{\isasymCODEAXIOMS}{\cmd{code\_axioms}} \newcommand{\isasymCODEABSTYPE}{\cmd{code\_abstype}} \newcommand{\isasymPRINTCODESETUP}{\cmd{print\_codesetup}} +\newcommand{\isasymPRINTCLASSES}{\cmd{print\_classes}} \newcommand{\isasymCODETHMS}{\cmd{code\_thms}} \newcommand{\isasymCODEDEPS}{\cmd{code\_deps}} \newcommand{\isasymFUN}{\cmd{fun}}