# HG changeset patch # User haftmann # Date 1163428978 -3600 # Node ID 74ab7c0980c7ef31a5575b9dee2c2b608bcb9f51 # Parent 26f64e7a67b572953dc1982b427c987f06119629 tuned diff -r 26f64e7a67b5 -r 74ab7c0980c7 doc-src/IsarAdvanced/Codegen/Thy/Codegen.thy --- a/doc-src/IsarAdvanced/Codegen/Thy/Codegen.thy Mon Nov 13 15:42:57 2006 +0100 +++ b/doc-src/IsarAdvanced/Codegen/Thy/Codegen.thy Mon Nov 13 15:42:58 2006 +0100 @@ -156,7 +156,7 @@ code_gen fac (SML "examples/fac.ML") text {* - The \isasymCODEGEN command takes a space-separated list of + The @{text "\"} command takes a space-separated list of constants together with \qn{serialization directives} in parentheses. These start with a \qn{target language} identifier, followed by arguments, their semantics @@ -231,7 +231,7 @@ text {* The list of all function equations in a theory may be inspected - using the \isasymPRINTCODETHMS command: + using the @{text "\"} command: *} print_codethms @@ -245,8 +245,9 @@ whether it provides one. The typical HOL tools are already set up in a way that - function definitions introduced by \isasymFUN, \isasymFUNCTION, - \isasymPRIMREC, \isasymRECDEF are implicitly propagated + function definitions introduced by @{text "\"}, + @{text "\"}, @{text "\"} + @{text "\"} are implicitly propagated to this function equation table. Specific theorems may be selected using an attribute: \emph{code func}. As example, a weight selector function: @@ -392,14 +393,14 @@ 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 \isasymCODEGEN: either the list of constants or the + 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 reasons, an extended version of the - \isasymCODEGEN command may prove useful: + For explorative purpose, an extended version of the + @{text "\"} command may prove useful: *} print_codethms () @@ -442,15 +443,15 @@ \begin{description} - \item[ExecutableSet] allows to generate code + \item[@{theory "ExecutableSet"}] allows to generate code for finite sets using lists. - \item[ExecutableRat] \label{exec_rat} implements rational + \item[@{theory "ExecutableRat"}] \label{exec_rat} implements rational numbers as triples @{text "(sign, enumerator, denominator)"}. - \item[EfficientNat] \label{eff_nat} implements natural numbers by integers, + \item[@{theory "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. - \item[MLString] provides an additional datatype @{text "mlstring"}; + \item[@{theory "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 mapped to strings in SML. @@ -506,7 +507,7 @@ text {* The current set of inline theorems may be inspected using - the \isasymPRINTCODETHMS command. + the @{text "\"} command. \emph{Inline procedures} are a generalized version of inline theorems written in ML -- rewrite rules are generated dependent @@ -519,7 +520,8 @@ transforming a list of function theorems to another list of function theorems, provided that neither the heading constant nor its type change. The @{const "0\nat"} / @{const Suc} - pattern elimination implemented in \secref{eff_nat} uses this + pattern elimination implemented in + theory @{theory "EfficientNat"} (\secref{eff_nat}) uses this interface. \begin{warn} @@ -550,16 +552,16 @@ (*>*) (*<*) -code_type bool +code_type %tt bool (SML) -code_const True and False and "op \" and Not +code_const %tt True and False and "op \" and Not (SML and and and) (*>*) -code_gen in_interval (SML "examples/bool1.ML") +code_gen in_interval (SML "examples/bool_literal.ML") text {* - \lstsml{Thy/examples/bool1.ML} + \lstsml{Thy/examples/bool_literal.ML} Though this is correct code, it is a little bit unsatisfactory: boolean values and operators are materialized as distinguished @@ -572,19 +574,19 @@ \qn{custom serializations}: *} -code_type bool +code_type %tt bool (SML "bool") -code_const True and False and "op \" +code_const %tt True and False and "op \" (SML "true" and "false" and "_ andalso _") text {* - The \isasymCODETYPE commad takes a type constructor + The @{text "\"} commad takes a type constructor as arguments together with a list of custom serializations. Each custom serialization starts with a target language identifier followed by an expression, which during code serialization is inserted whenever the type constructor - would occur. For constants, \isasymCODECONST implements - the corresponding mechanism. Each \qt{\_} in + would occur. For constants, @{text "\"} implements + the corresponding mechanism. Each ``@{verbatim "_"}'' in a serialization expression is treated as a placeholder for the type constructor's (the constant's) arguments. *} @@ -594,33 +596,34 @@ text {* To assert that the existing \qt{bool}, \qt{true} and \qt{false} - is not used for generated code, we use \isasymCODERESERVED. + is not used for generated code, we use @{text "\"}. After this setup, code looks quite more readable: *} -code_gen in_interval (SML "examples/bool2.ML") +code_gen in_interval (SML "examples/bool_mlbool.ML") text {* - \lstsml{Thy/examples/bool2.ML} + \lstsml{Thy/examples/bool_mlbool.ML} This still is not perfect: the parentheses - around \qt{andalso} are superfluous. Though the serializer + around the \qt{andalso} expression are superfluous. + Though the serializer by no means attempts to imitate the rich Isabelle syntax framework, it provides some common idioms, notably associative infixes with precedences which may be used here: *} -code_const "op \" +code_const %tt "op \" (SML infixl 1 "andalso") -code_gen in_interval (SML "examples/bool3.ML") +code_gen in_interval (SML "examples/bool_infix.ML") text {* - \lstsml{Thy/examples/bool3.ML} + \lstsml{Thy/examples/bool_infix.ML} Next, we try to map HOL pairs to SML pairs, using the - infix \qt{ * } type constructor and parentheses: + infix ``@{verbatim "*"}'' type constructor and parentheses: *} (*<*) @@ -630,18 +633,18 @@ (SML) (*>*) -code_type * +code_type %tt * (SML infix 2 "*") -code_const Pair +code_const %tt Pair (SML "!((_),/ (_))") text {* - The initial bang \qt{!} tells the serializer to never put + The initial bang ``@{verbatim "!"}'' tells the serializer to never put parentheses around the whole expression (they are already present), while the parentheses around argument place holders tell not to put parentheses around the arguments. - The slash \qt{/} (followed by arbitrary white space) + The slash ``@{verbatim "/"}'' (followed by arbitrary white space) inserts a space which may be used as a break if necessary during pretty printing. @@ -666,10 +669,10 @@ integers: *} -code_type int +code_type %tt int (SML "IntInf.int") -code_const "op + \ int \ int \ int" +code_const %tt "op + \ int \ int \ int" and "op * \ int \ int \ int" (SML "IntInf.+ (_, _)" and "IntInf.* (_, _)") @@ -690,9 +693,10 @@ A further noteworthy details is that any special character in a custom serialization may be quoted - using \qt{'}; thus, in \qt{fn '\_ => \_} the first - \qt{'\_} is a proper underscore while the - second \qt{\_} is a placeholder. + using ``@{verbatim "'"}''; thus, in + ``@{verbatim "fn '_ => _"}'' the first + ``@{verbatim "_"}'' is a proper underscore while the + second ``@{verbatim "_"}'' is a placeholder. The HOL theories provide further examples for custom serializations and form @@ -778,7 +782,7 @@ Examine the following: *} -code_const "op = \ int \ int \ bool" +code_const %tt "op = \ int \ int \ bool" (SML "!(_ : IntInf.int = _)") text {* @@ -789,7 +793,7 @@ by using the overloaded constant @{const "Code_Generator.eq"}: *} -code_const "Code_Generator.eq \ int \ int \ bool" +code_const %tt "Code_Generator.eq \ int \ int \ bool" (SML "!(_ : IntInf.int = _)") subsubsection {* typedecls interpreted by customary serializations *} @@ -810,7 +814,7 @@ lemmas [code func] = lookup.simps (*>*) -code_type key +code_type %tt key (SML "string") text {* @@ -822,7 +826,7 @@ instance key :: eq .. -code_const "Code_Generator.eq \ key \ key \ bool" +code_const %tt "Code_Generator.eq \ key \ key \ bool" (SML "!(_ : string = _)") text {* @@ -896,7 +900,7 @@ For convenience, the default HOL setup for Haskell maps the @{text eq} class to its counterpart in Haskell, giving custom serializations - for the class (\isasymCODECLASS) and its operation: + for the class (@{text "\"}) and its operation: *} (*<*) @@ -904,10 +908,10 @@ class eq = fixes eq :: "'a \ 'a \ bool" (*>*) -code_class eq +code_class %tt eq (Haskell "Eq" where eq \ "(==)") -code_const eq +code_const %tt eq (Haskell infixl 4 "==") (*<*) @@ -927,17 +931,17 @@ instance bar :: eq .. -code_type bar +code_type %tt bar (Haskell "Integer") text {* The code generator would produce an additional instance, which of course is rejected. To suppress this additional instance, use - \isasymCODEINSTANCE: + @{text "\"}: *} -code_instance bar :: eq +code_instance %tt bar :: eq (Haskell -) subsection {* Types matter *} @@ -947,10 +951,10 @@ some kind of sets as lists in SML: *} -code_type set +code_type %tt set (SML "_ list") -code_const "{}" and insert +code_const %tt "{}" and insert (SML "![]" and infixl 7 "::") definition @@ -1059,8 +1063,8 @@ By brute force: *} -axioms - arbitrary_option: "arbitrary = None" +axiomatization where + "arbitrary = None" text {* However this has to be considered harmful since this axiom, @@ -1097,7 +1101,7 @@ "None' = None" text {* - Then finally we are enabled to use \isasymCODEAXIOMS: + Then finally we are enabled to use @{text "\"}: *} code_axioms @@ -1123,7 +1127,7 @@ Another axiomatic extension is code generation for abstracted types. For this, the - \emph{ExecutableRat} (see \secref{exec_rat}) + @{theory "ExecutableRat"} (see \secref{exec_rat}) forms a good example. *} @@ -1146,7 +1150,7 @@ text %mlref {* \begin{mldecls} - @{index_ML_type CodegenConsts.const} \\ + @{index_ML_type CodegenConsts.const: "string * typ list"} \\ @{index_ML CodegenConsts.norm_of_typ: "theory -> string * typ -> CodegenConsts.const"} \\ @{index_ML CodegenConsts.typ_of_inst: "theory -> CodegenConsts.const -> string * typ"} \\ \end{mldecls} @@ -1180,17 +1184,13 @@ text %mlref {* \begin{mldecls} - @{index_ML_type CodegenData.lthms} \\ @{index_ML CodegenData.lazy: "(unit -> thm list) -> CodegenData.lthms"} \end{mldecls} \begin{description} - \item @{ML_type CodegenData.lthms} is an abstract view - on suspended theorems. Suspensions are evaluated on demand. - \item @{ML CodegenData.lazy}~@{text f} turns an abstract - theorem computation @{text f} into suspended theorems. + theorem computation @{text f} into a suspension of theorems. \end{description} *} @@ -1199,7 +1199,6 @@ text %mlref {* \begin{mldecls} - @{index_ML_type CodegenData.lthms} \\ @{index_ML CodegenData.add_func: "thm -> theory -> theory"} \\ @{index_ML CodegenData.del_func: "thm -> theory -> theory"} \\ @{index_ML CodegenData.add_funcl: "CodegenConsts.const * CodegenData.lthms -> theory -> theory"} \\ @@ -1416,14 +1415,21 @@ text %mlref {* \begin{mldecls} - @{index_ML_type DatatypeHooks.hook} \\ + @{index_ML_type DatatypeHooks.hook: "string list -> theory -> theory"} \\ @{index_ML DatatypeHooks.add: "DatatypeHooks.hook -> theory -> theory"} \end{mldecls} *} text %mlref {* \begin{mldecls} - @{index_ML_type TypecopyPackage.info} \\ + @{index_ML_type TypecopyPackage.info: "{ + vs: (string * sort) list, + constr: string, + typ: typ, + inject: thm, + proj: string * typ, + proj_def: thm + }"} \\ @{index_ML TypecopyPackage.add_typecopy: " bstring * string list -> typ -> (bstring * bstring) option -> theory -> (string * TypecopyPackage.info) * theory"} \\ @@ -1439,7 +1445,8 @@ text %mlref {* \begin{mldecls} - @{index_ML_type DatatypeCodegen.hook} \\ + @{index_ML_type DatatypeCodegen.hook: "(string * (bool * ((string * sort) list * (string * typ list) list))) list + -> theory -> theory"} \\ @{index_ML DatatypeCodegen.add_codetypes_hook_bootstrap: " DatatypeCodegen.hook -> theory -> theory"} \end{mldecls} diff -r 26f64e7a67b5 -r 74ab7c0980c7 src/HOL/Library/ExecutableSet.thy --- a/src/HOL/Library/ExecutableSet.thy Mon Nov 13 15:42:57 2006 +0100 +++ b/src/HOL/Library/ExecutableSet.thy Mon Nov 13 15:42:58 2006 +0100 @@ -9,19 +9,21 @@ imports Main begin -section {* Definitional equality rewrites *} +section {* Definitional rewrites *} instance set :: (eq) eq .. lemma [code target: Set]: - "(A = B) = (A \ B \ B \ A)" + "(A = B) \ (A \ B \ B \ A)" by blast lemma [code func]: - "Code_Generator.eq A B = (A \ B \ B \ A)" + "Code_Generator.eq A B \ (A \ B \ B \ A)" unfolding eq_def by blast -declare bex_triv_one_point1 [symmetric, standard, code] +lemma [code]: + "a \ A \ (\x\A. x = a)" + unfolding bex_triv_one_point1 .. section {* HOL definitions *}