# HG changeset patch # User wenzelm # Date 1281785046 -7200 # Node ID 001f2f44984ccd5271726710c52f03ff7cc07cde # Parent 8e4058f4848c309bbae2cb08d6b05c27704154cf# Parent 7eb0f6991e2582e936b73e7fc80d5d1716a806ff merged diff -r 7eb0f6991e25 -r 001f2f44984c doc-src/Codegen/Thy/Foundations.thy --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/doc-src/Codegen/Thy/Foundations.thy Sat Aug 14 13:24:06 2010 +0200 @@ -0,0 +1,432 @@ +theory Foundations +imports Introduction +begin + +section {* Code generation foundations \label{sec:program} *} + +subsection {* The @{text "Isabelle/HOL"} default setup *} + +text {* + We have already seen how by default equations stemming from + @{command definition}, @{command primrec} and @{command fun} + statements are used for code generation. This default behaviour + can be changed, e.g.\ by providing different code equations. + The customisations shown in this section are \emph{safe} + as regards correctness: all programs that can be generated are partially + correct. +*} + +subsection {* Selecting code equations *} + +text {* + Coming back to our introductory example, we + could provide an alternative code equations for @{const dequeue} + explicitly: +*} + +lemma %quote [code]: + "dequeue (AQueue xs []) = + (if xs = [] then (None, AQueue [] []) + else dequeue (AQueue [] (rev xs)))" + "dequeue (AQueue xs (y # ys)) = + (Some y, AQueue xs ys)" + by (cases xs, simp_all) (cases "rev xs", simp_all) + +text {* + \noindent The annotation @{text "[code]"} is an @{text Isar} + @{text attribute} which states that the given theorems should be + considered as code equations for a @{text fun} statement -- + the corresponding constant is determined syntactically. The resulting code: +*} + +text %quote {*@{code_stmts dequeue (consts) dequeue (Haskell)}*} + +text {* + \noindent You may note that the equality test @{term "xs = []"} has been + replaced by the predicate @{term "null xs"}. This is due to the default + setup in the \qn{preprocessor} to be discussed further below (\secref{sec:preproc}). + + Changing the default constructor set of datatypes is also + possible. See \secref{sec:datatypes} for an example. + + As told in \secref{sec:concept}, code generation is based + on a structured collection of code theorems. + This collection + may be inspected using the @{command code_thms} command: +*} + +code_thms %quote dequeue + +text {* + \noindent prints a table with \emph{all} code equations + for @{const dequeue}, including + \emph{all} code equations those equations depend + on recursively. + + Similarly, the @{command code_deps} command shows a graph + visualising dependencies between code equations. +*} + +subsection {* @{text class} and @{text instantiation} *} + +text {* + Concerning type classes and code generation, let us examine an example + from abstract algebra: +*} + +class %quote semigroup = + fixes mult :: "'a \ 'a \ 'a" (infixl "\" 70) + assumes assoc: "(x \ y) \ z = x \ (y \ z)" + +class %quote monoid = semigroup + + fixes neutral :: 'a ("\") + assumes neutl: "\ \ x = x" + and neutr: "x \ \ = x" + +instantiation %quote nat :: monoid +begin + +primrec %quote mult_nat where + "0 \ n = (0\nat)" + | "Suc m \ n = n + m \ n" + +definition %quote neutral_nat where + "\ = Suc 0" + +lemma %quote add_mult_distrib: + fixes n m q :: nat + shows "(n + m) \ q = n \ q + m \ q" + by (induct n) simp_all + +instance %quote proof + fix m n q :: nat + show "m \ n \ q = m \ (n \ q)" + by (induct m) (simp_all add: add_mult_distrib) + show "\ \ n = n" + by (simp add: neutral_nat_def) + show "m \ \ = m" + by (induct m) (simp_all add: neutral_nat_def) +qed + +end %quote + +text {* + \noindent We define the natural operation of the natural numbers + on monoids: +*} + +primrec %quote (in monoid) pow :: "nat \ 'a \ 'a" where + "pow 0 a = \" + | "pow (Suc n) a = a \ pow n a" + +text {* + \noindent This we use to define the discrete exponentiation function: +*} + +definition %quote bexp :: "nat \ nat" where + "bexp n = pow n (Suc (Suc 0))" + +text {* + \noindent The corresponding code in Haskell uses that language's native classes: +*} + +text %quote {*@{code_stmts bexp (Haskell)}*} + +text {* + \noindent This is a convenient place to show how explicit dictionary construction + manifests in generated code (here, the same example in @{text SML}) + \cite{Haftmann-Nipkow:2010:code}: +*} + +text %quote {*@{code_stmts bexp (SML)}*} + +text {* + \noindent Note the parameters with trailing underscore (@{verbatim "A_"}), + which are the dictionary parameters. +*} + +subsection {* The preprocessor \label{sec:preproc} *} + +text {* + Before selected function theorems are turned into abstract + code, a chain of definitional transformation steps is carried + out: \emph{preprocessing}. In essence, the preprocessor + consists of two components: a \emph{simpset} and \emph{function transformers}. + + The \emph{simpset} can apply the full generality of the + Isabelle simplifier. Due to the interpretation of theorems as code + equations, rewrites are applied to the right hand side and the + arguments of the left hand side of an equation, but never to the + constant heading the left hand side. An important special case are + \emph{unfold theorems}, which may be declared and removed using + the @{attribute code_unfold} or \emph{@{attribute code_unfold} del} + attribute, respectively. + + Some common applications: +*} + +text_raw {* + \begin{itemize} +*} + +text {* + \item replacing non-executable constructs by executable ones: +*} + +lemma %quote [code_unfold]: + "x \ set xs \ List.member xs x" by (fact in_set_member) + +text {* + \item eliminating superfluous constants: +*} + +lemma %quote [code_unfold]: + "1 = Suc 0" by (fact One_nat_def) + +text {* + \item replacing executable but inconvenient constructs: +*} + +lemma %quote [code_unfold]: + "xs = [] \ List.null xs" by (fact eq_Nil_null) + +text_raw {* + \end{itemize} +*} + +text {* + \noindent \emph{Function transformers} provide a very general interface, + transforming a list of function theorems to another + list of function theorems, provided that neither the heading + constant nor its type change. The @{term "0\nat"} / @{const Suc} + pattern elimination implemented in + theory @{text Efficient_Nat} (see \secref{eff_nat}) uses this + interface. + + \noindent The current setup of the preprocessor may be inspected using + the @{command print_codeproc} command. + @{command code_thms} provides a convenient + mechanism to inspect the impact of a preprocessor setup + on code equations. + + \begin{warn} + + Attribute @{attribute code_unfold} also applies to the + preprocessor of the ancient @{text "SML code generator"}; in case + this is not what you intend, use @{attribute code_inline} instead. + \end{warn} +*} + +subsection {* Datatypes \label{sec:datatypes} *} + +text {* + 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 exactly 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 + @{command print_codesetup} command. + + In some cases, it is appropriate to alter or extend this table. As + an example, we will develop an alternative representation of the + queue example given in \secref{sec:intro}. The amortised + representation is convenient for generating code but exposes its + \qt{implementation} details, which may be cumbersome when proving + theorems about it. Therefore, here is a simple, straightforward + representation of queues: +*} + +datatype %quote 'a queue = Queue "'a list" + +definition %quote empty :: "'a queue" where + "empty = Queue []" + +primrec %quote enqueue :: "'a \ 'a queue \ 'a queue" where + "enqueue x (Queue xs) = Queue (xs @ [x])" + +fun %quote dequeue :: "'a queue \ 'a option \ 'a queue" where + "dequeue (Queue []) = (None, Queue [])" + | "dequeue (Queue (x # xs)) = (Some x, Queue xs)" + +text {* + \noindent This we can use directly for proving; for executing, + we provide an alternative characterisation: +*} + +definition %quote AQueue :: "'a list \ 'a list \ 'a queue" where + "AQueue xs ys = Queue (ys @ rev xs)" + +code_datatype %quote AQueue + +text {* + \noindent Here we define a \qt{constructor} @{const "AQueue"} which + is defined in terms of @{text "Queue"} and interprets its arguments + according to what the \emph{content} of an amortised queue is supposed + to be. Equipped with this, we are able to prove the following equations + for our primitive queue operations which \qt{implement} the simple + queues in an amortised fashion: +*} + +lemma %quote empty_AQueue [code]: + "empty = AQueue [] []" + unfolding AQueue_def empty_def by simp + +lemma %quote enqueue_AQueue [code]: + "enqueue x (AQueue xs ys) = AQueue (x # xs) ys" + unfolding AQueue_def by simp + +lemma %quote dequeue_AQueue [code]: + "dequeue (AQueue xs []) = + (if xs = [] then (None, AQueue [] []) + else dequeue (AQueue [] (rev xs)))" + "dequeue (AQueue xs (y # ys)) = (Some y, AQueue xs ys)" + unfolding AQueue_def by simp_all + +text {* + \noindent For completeness, we provide a substitute for the + @{text case} combinator on queues: +*} + +lemma %quote queue_case_AQueue [code]: + "queue_case f (AQueue xs ys) = f (ys @ rev xs)" + unfolding AQueue_def by simp + +text {* + \noindent The resulting code looks as expected: +*} + +text %quote {*@{code_stmts empty enqueue dequeue (SML)}*} + +text {* + \noindent From this example, it can be glimpsed that using own + constructor sets is a little delicate since it changes the set of + valid patterns for values of that type. Without going into much + detail, here some practical hints: + + \begin{itemize} + + \item When changing the constructor set for datatypes, take care + to provide alternative equations for the @{text case} combinator. + + \item Values in the target language need not to be normalised -- + different values in the target language may represent the same + value in the logic. + + \item Usually, a good methodology to deal with the subtleties of + pattern matching is to see the type as an abstract type: provide + a set of operations which operate on the concrete representation + of the type, and derive further operations by combinations of + these primitive ones, without relying on a particular + representation. + + \end{itemize} +*} + + +subsection {* Equality *} + +text {* + Surely you have already noticed how equality is treated + by the code generator: +*} + +primrec %quote 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 {* + \noindent During preprocessing, the membership test is rewritten, + resulting in @{const List.member}, which itself + performs an explicit equality check. +*} + +text %quote {*@{code_stmts collect_duplicates (SML)}*} + +text {* + \noindent Obviously, polymorphic equality is implemented the Haskell + way using a type class. How is this achieved? HOL introduces + an explicit class @{class eq} with a corresponding operation + @{const eq_class.eq} such that @{thm eq [no_vars]}. + The preprocessing framework does the rest by propagating the + @{class eq} constraints through all dependent code equations. + For datatypes, instances of @{class eq} are implicitly derived + when possible. For other types, you may instantiate @{text eq} + manually like any other type class. +*} + + +subsection {* Explicit partiality *} + +text {* + Partiality usually enters the game by partial patterns, as + in the following example, again for amortised queues: +*} + +definition %quote strict_dequeue :: "'a queue \ 'a \ 'a queue" where + "strict_dequeue q = (case dequeue q + of (Some x, q') \ (x, q'))" + +lemma %quote strict_dequeue_AQueue [code]: + "strict_dequeue (AQueue xs (y # ys)) = (y, AQueue xs ys)" + "strict_dequeue (AQueue xs []) = + (case rev xs of y # ys \ (y, AQueue [] ys))" + by (simp_all add: strict_dequeue_def dequeue_AQueue split: list.splits) + +text {* + \noindent In the corresponding code, there is no equation + for the pattern @{term "AQueue [] []"}: +*} + +text %quote {*@{code_stmts strict_dequeue (consts) strict_dequeue (Haskell)}*} + +text {* + \noindent In some cases it is desirable to have this + pseudo-\qt{partiality} more explicitly, e.g.~as follows: +*} + +axiomatization %quote empty_queue :: 'a + +definition %quote strict_dequeue' :: "'a queue \ 'a \ 'a queue" where + "strict_dequeue' q = (case dequeue q of (Some x, q') \ (x, q') | _ \ empty_queue)" + +lemma %quote strict_dequeue'_AQueue [code]: + "strict_dequeue' (AQueue xs []) = (if xs = [] then empty_queue + else strict_dequeue' (AQueue [] (rev xs)))" + "strict_dequeue' (AQueue xs (y # ys)) = + (y, AQueue xs ys)" + by (simp_all add: strict_dequeue'_def dequeue_AQueue split: list.splits) + +text {* + Observe that on the right hand side of the definition of @{const + "strict_dequeue'"}, the unspecified constant @{const empty_queue} occurs. + + Normally, if constants without any code equations occur in a + program, the code generator complains (since in most cases this is + indeed an error). But such constants can also be thought + of as function definitions which always fail, + since there is never a successful pattern match on the left hand + side. In order to categorise a constant into that category + explicitly, use @{command "code_abort"}: +*} + +code_abort %quote empty_queue + +text {* + \noindent Then the code generator will just insert an error or + exception at the appropriate position: +*} + +text %quote {*@{code_stmts strict_dequeue' (consts) empty_queue strict_dequeue' (Haskell)}*} + +text {* + \noindent This feature however is rarely needed in practice. + Note also that the @{text HOL} default setup already declares + @{const undefined} as @{command "code_abort"}, which is most + likely to be used in such situations. +*} + +end diff -r 7eb0f6991e25 -r 001f2f44984c doc-src/Codegen/Thy/Further.thy --- a/doc-src/Codegen/Thy/Further.thy Sat Aug 14 12:01:50 2010 +0200 +++ b/doc-src/Codegen/Thy/Further.thy Sat Aug 14 13:24:06 2010 +0200 @@ -191,4 +191,140 @@ the framework described there is available in theory @{theory Imperative_HOL}. *} + +subsection {* ML system interfaces \label{sec:ml} *} + +text {* + Since the code generator framework not only aims to provide + a nice Isar interface but also to form a base for + code-generation-based applications, here a short + description of the most important ML interfaces. +*} + +subsubsection {* Managing executable content *} + +text %mlref {* + \begin{mldecls} + @{index_ML Code.add_eqn: "thm -> theory -> theory"} \\ + @{index_ML Code.del_eqn: "thm -> theory -> theory"} \\ + @{index_ML Code_Preproc.map_pre: "(simpset -> simpset) -> theory -> theory"} \\ + @{index_ML Code_Preproc.map_post: "(simpset -> simpset) -> theory -> theory"} \\ + @{index_ML Code_Preproc.add_functrans: "string * (theory -> (thm * bool) list -> (thm * bool) list option) + -> theory -> theory"} \\ + @{index_ML Code_Preproc.del_functrans: "string -> theory -> theory"} \\ + @{index_ML Code.add_datatype: "(string * typ) list -> theory -> theory"} \\ + @{index_ML Code.get_type: "theory -> string + -> (string * sort) list * ((string * string list) * typ list) list"} \\ + @{index_ML Code.get_type_of_constr_or_abstr: "theory -> string -> (string * bool) option"} + \end{mldecls} + + \begin{description} + + \item @{ML Code.add_eqn}~@{text "thm"}~@{text "thy"} adds function + theorem @{text "thm"} to executable content. + + \item @{ML Code.del_eqn}~@{text "thm"}~@{text "thy"} removes function + theorem @{text "thm"} from executable content, if present. + + \item @{ML Code_Preproc.map_pre}~@{text "f"}~@{text "thy"} changes + the preprocessor simpset. + + \item @{ML Code_Preproc.add_functrans}~@{text "(name, f)"}~@{text "thy"} adds + function transformer @{text f} (named @{text name}) to executable content; + @{text f} is a transformer of the code equations belonging + to a certain function definition, depending on the + current theory context. Returning @{text NONE} indicates that no + transformation took place; otherwise, the whole process will be iterated + with the new code equations. + + \item @{ML Code_Preproc.del_functrans}~@{text "name"}~@{text "thy"} removes + function transformer named @{text name} from executable content. + + \item @{ML Code.add_datatype}~@{text cs}~@{text thy} adds + a datatype to executable content, with generation + set @{text cs}. + + \item @{ML Code.get_type_of_constr_or_abstr}~@{text "thy"}~@{text "const"} + returns type constructor corresponding to + constructor @{text const}; returns @{text NONE} + if @{text const} is no constructor. + + \end{description} +*} + +subsubsection {* Auxiliary *} + +text %mlref {* + \begin{mldecls} + @{index_ML Code.read_const: "theory -> string -> string"} + \end{mldecls} + + \begin{description} + + \item @{ML Code.read_const}~@{text thy}~@{text s} + reads a constant as a concrete term expression @{text s}. + + \end{description} + +*} + +subsubsection {* Data depending on the theory's executable content *} + +text {* + Implementing code generator applications on top + of the framework set out so far usually not only + involves using those primitive interfaces + but also storing code-dependent data and various + other things. + + Due to incrementality of code generation, changes in the + theory's executable content have to be propagated in a + certain fashion. Additionally, such changes may occur + not only during theory extension but also during theory + merge, which is a little bit nasty from an implementation + point of view. The framework provides a solution + to this technical challenge by providing a functorial + data slot @{ML_functor Code_Data}; on instantiation + of this functor, the following types and operations + are required: + + \medskip + \begin{tabular}{l} + @{text "type T"} \\ + @{text "val empty: T"} \\ + \end{tabular} + + \begin{description} + + \item @{text T} the type of data to store. + + \item @{text empty} initial (empty) data. + + \end{description} + + \noindent An instance of @{ML_functor Code_Data} provides the following + interface: + + \medskip + \begin{tabular}{l} + @{text "change: theory \ (T \ T) \ T"} \\ + @{text "change_yield: theory \ (T \ 'a * T) \ 'a * T"} + \end{tabular} + + \begin{description} + + \item @{text change} update of current data (cached!) + by giving a continuation. + + \item @{text change_yield} update with side result. + + \end{description} +*} + +text {* + \bigskip + + \emph{Happy proving, happy hacking!} +*} + end diff -r 7eb0f6991e25 -r 001f2f44984c doc-src/Codegen/Thy/Inductive_Predicate.thy --- a/doc-src/Codegen/Thy/Inductive_Predicate.thy Sat Aug 14 12:01:50 2010 +0200 +++ b/doc-src/Codegen/Thy/Inductive_Predicate.thy Sat Aug 14 13:24:06 2010 +0200 @@ -2,7 +2,7 @@ imports Setup begin -subsection {* Inductive Predicates *} +section {* Inductive Predicates *} (*<*) hide_const append diff -r 7eb0f6991e25 -r 001f2f44984c doc-src/Codegen/Thy/Introduction.thy --- a/doc-src/Codegen/Thy/Introduction.thy Sat Aug 14 12:01:50 2010 +0200 +++ b/doc-src/Codegen/Thy/Introduction.thy Sat Aug 14 13:24:06 2010 +0200 @@ -2,7 +2,17 @@ imports Setup begin -section {* Introduction and Overview *} +section {* Introduction *} + +subsection {* Code generation fundamental: shallow embedding *} + +subsection {* A quick start with the @{text "Isabelle/HOL"} toolbox *} + +subsection {* Type classes *} + +subsection {* How to continue from here *} + +subsection {* If something goes utterly wrong *} text {* This tutorial introduces a generic code generator for the @@ -111,6 +121,29 @@ for more details see \secref{sec:further}. *} +subsection {* If something utterly fails *} + +text {* + Under certain circumstances, the code generator fails to produce + code entirely. + + \begin{description} + + \ditem{generate only one module} + + \ditem{check with a different target language} + + \ditem{inspect code equations} + + \ditem{inspect preprocessor setup} + + \ditem{generate exceptions} + + \ditem{remove offending code equations} + + \end{description} +*} + subsection {* Code generator architecture \label{sec:concept} *} text {* diff -r 7eb0f6991e25 -r 001f2f44984c doc-src/Codegen/Thy/ML.thy --- a/doc-src/Codegen/Thy/ML.thy Sat Aug 14 12:01:50 2010 +0200 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,162 +0,0 @@ -theory "ML" -imports Setup -begin - -section {* ML system interfaces \label{sec:ml} *} - -text {* - Since the code generator framework not only aims to provide - a nice Isar interface but also to form a base for - code-generation-based applications, here a short - description of the most important ML interfaces. -*} - -subsection {* Executable theory content: @{text Code} *} - -text {* - This Pure module implements the core notions of - executable content of a theory. -*} - -subsubsection {* Managing executable content *} - -text %mlref {* - \begin{mldecls} - @{index_ML Code.add_eqn: "thm -> theory -> theory"} \\ - @{index_ML Code.del_eqn: "thm -> theory -> theory"} \\ - @{index_ML Code_Preproc.map_pre: "(simpset -> simpset) -> theory -> theory"} \\ - @{index_ML Code_Preproc.map_post: "(simpset -> simpset) -> theory -> theory"} \\ - @{index_ML Code_Preproc.add_functrans: "string * (theory -> (thm * bool) list -> (thm * bool) list option) - -> theory -> theory"} \\ - @{index_ML Code_Preproc.del_functrans: "string -> theory -> theory"} \\ - @{index_ML Code.add_datatype: "(string * typ) list -> theory -> theory"} \\ - @{index_ML Code.get_type: "theory -> string - -> (string * sort) list * ((string * string list) * typ list) list"} \\ - @{index_ML Code.get_type_of_constr_or_abstr: "theory -> string -> (string * bool) option"} - \end{mldecls} - - \begin{description} - - \item @{ML Code.add_eqn}~@{text "thm"}~@{text "thy"} adds function - theorem @{text "thm"} to executable content. - - \item @{ML Code.del_eqn}~@{text "thm"}~@{text "thy"} removes function - theorem @{text "thm"} from executable content, if present. - - \item @{ML Code_Preproc.map_pre}~@{text "f"}~@{text "thy"} changes - the preprocessor simpset. - - \item @{ML Code_Preproc.add_functrans}~@{text "(name, f)"}~@{text "thy"} adds - function transformer @{text f} (named @{text name}) to executable content; - @{text f} is a transformer of the code equations belonging - to a certain function definition, depending on the - current theory context. Returning @{text NONE} indicates that no - transformation took place; otherwise, the whole process will be iterated - with the new code equations. - - \item @{ML Code_Preproc.del_functrans}~@{text "name"}~@{text "thy"} removes - function transformer named @{text name} from executable content. - - \item @{ML Code.add_datatype}~@{text cs}~@{text thy} adds - a datatype to executable content, with generation - set @{text cs}. - - \item @{ML Code.get_type_of_constr_or_abstr}~@{text "thy"}~@{text "const"} - returns type constructor corresponding to - constructor @{text const}; returns @{text NONE} - if @{text const} is no constructor. - - \end{description} -*} - -subsection {* Auxiliary *} - -text %mlref {* - \begin{mldecls} - @{index_ML Code.read_const: "theory -> string -> string"} - \end{mldecls} - - \begin{description} - - \item @{ML Code.read_const}~@{text thy}~@{text s} - reads a constant as a concrete term expression @{text s}. - - \end{description} - -*} - -subsection {* Implementing code generator applications *} - -text {* - Implementing code generator applications on top - of the framework set out so far usually not only - involves using those primitive interfaces - but also storing code-dependent data and various - other things. -*} - -subsubsection {* Data depending on the theory's executable content *} - -text {* - Due to incrementality of code generation, changes in the - theory's executable content have to be propagated in a - certain fashion. Additionally, such changes may occur - not only during theory extension but also during theory - merge, which is a little bit nasty from an implementation - point of view. The framework provides a solution - to this technical challenge by providing a functorial - data slot @{ML_functor Code_Data}; on instantiation - of this functor, the following types and operations - are required: - - \medskip - \begin{tabular}{l} - @{text "type T"} \\ - @{text "val empty: T"} \\ - @{text "val purge: theory \ string list option \ T \ T"} - \end{tabular} - - \begin{description} - - \item @{text T} the type of data to store. - - \item @{text empty} initial (empty) data. - - \item @{text purge}~@{text thy}~@{text consts} propagates changes in executable content; - @{text consts} indicates the kind - of change: @{ML NONE} stands for a fundamental change - which invalidates any existing code, @{text "SOME consts"} - hints that executable content for constants @{text consts} - has changed. - - \end{description} - - \noindent An instance of @{ML_functor Code_Data} provides the following - interface: - - \medskip - \begin{tabular}{l} - @{text "get: theory \ T"} \\ - @{text "change: theory \ (T \ T) \ T"} \\ - @{text "change_yield: theory \ (T \ 'a * T) \ 'a * T"} - \end{tabular} - - \begin{description} - - \item @{text get} retrieval of the current data. - - \item @{text change} update of current data (cached!) - by giving a continuation. - - \item @{text change_yield} update with side result. - - \end{description} -*} - -text {* - \bigskip - - \emph{Happy proving, happy hacking!} -*} - -end diff -r 7eb0f6991e25 -r 001f2f44984c doc-src/Codegen/Thy/Program.thy --- a/doc-src/Codegen/Thy/Program.thy Sat Aug 14 12:01:50 2010 +0200 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,432 +0,0 @@ -theory Program -imports Introduction -begin - -section {* Turning Theories into Programs \label{sec:program} *} - -subsection {* The @{text "Isabelle/HOL"} default setup *} - -text {* - We have already seen how by default equations stemming from - @{command definition}, @{command primrec} and @{command fun} - statements are used for code generation. This default behaviour - can be changed, e.g.\ by providing different code equations. - The customisations shown in this section are \emph{safe} - as regards correctness: all programs that can be generated are partially - correct. -*} - -subsection {* Selecting code equations *} - -text {* - Coming back to our introductory example, we - could provide an alternative code equations for @{const dequeue} - explicitly: -*} - -lemma %quote [code]: - "dequeue (AQueue xs []) = - (if xs = [] then (None, AQueue [] []) - else dequeue (AQueue [] (rev xs)))" - "dequeue (AQueue xs (y # ys)) = - (Some y, AQueue xs ys)" - by (cases xs, simp_all) (cases "rev xs", simp_all) - -text {* - \noindent The annotation @{text "[code]"} is an @{text Isar} - @{text attribute} which states that the given theorems should be - considered as code equations for a @{text fun} statement -- - the corresponding constant is determined syntactically. The resulting code: -*} - -text %quote {*@{code_stmts dequeue (consts) dequeue (Haskell)}*} - -text {* - \noindent You may note that the equality test @{term "xs = []"} has been - replaced by the predicate @{term "null xs"}. This is due to the default - setup in the \qn{preprocessor} to be discussed further below (\secref{sec:preproc}). - - Changing the default constructor set of datatypes is also - possible. See \secref{sec:datatypes} for an example. - - As told in \secref{sec:concept}, code generation is based - on a structured collection of code theorems. - This collection - may be inspected using the @{command code_thms} command: -*} - -code_thms %quote dequeue - -text {* - \noindent prints a table with \emph{all} code equations - for @{const dequeue}, including - \emph{all} code equations those equations depend - on recursively. - - Similarly, the @{command code_deps} command shows a graph - visualising dependencies between code equations. -*} - -subsection {* @{text class} and @{text instantiation} *} - -text {* - Concerning type classes and code generation, let us examine an example - from abstract algebra: -*} - -class %quote semigroup = - fixes mult :: "'a \ 'a \ 'a" (infixl "\" 70) - assumes assoc: "(x \ y) \ z = x \ (y \ z)" - -class %quote monoid = semigroup + - fixes neutral :: 'a ("\") - assumes neutl: "\ \ x = x" - and neutr: "x \ \ = x" - -instantiation %quote nat :: monoid -begin - -primrec %quote mult_nat where - "0 \ n = (0\nat)" - | "Suc m \ n = n + m \ n" - -definition %quote neutral_nat where - "\ = Suc 0" - -lemma %quote add_mult_distrib: - fixes n m q :: nat - shows "(n + m) \ q = n \ q + m \ q" - by (induct n) simp_all - -instance %quote proof - fix m n q :: nat - show "m \ n \ q = m \ (n \ q)" - by (induct m) (simp_all add: add_mult_distrib) - show "\ \ n = n" - by (simp add: neutral_nat_def) - show "m \ \ = m" - by (induct m) (simp_all add: neutral_nat_def) -qed - -end %quote - -text {* - \noindent We define the natural operation of the natural numbers - on monoids: -*} - -primrec %quote (in monoid) pow :: "nat \ 'a \ 'a" where - "pow 0 a = \" - | "pow (Suc n) a = a \ pow n a" - -text {* - \noindent This we use to define the discrete exponentiation function: -*} - -definition %quote bexp :: "nat \ nat" where - "bexp n = pow n (Suc (Suc 0))" - -text {* - \noindent The corresponding code in Haskell uses that language's native classes: -*} - -text %quote {*@{code_stmts bexp (Haskell)}*} - -text {* - \noindent This is a convenient place to show how explicit dictionary construction - manifests in generated code (here, the same example in @{text SML}) - \cite{Haftmann-Nipkow:2010:code}: -*} - -text %quote {*@{code_stmts bexp (SML)}*} - -text {* - \noindent Note the parameters with trailing underscore (@{verbatim "A_"}), - which are the dictionary parameters. -*} - -subsection {* The preprocessor \label{sec:preproc} *} - -text {* - Before selected function theorems are turned into abstract - code, a chain of definitional transformation steps is carried - out: \emph{preprocessing}. In essence, the preprocessor - consists of two components: a \emph{simpset} and \emph{function transformers}. - - The \emph{simpset} can apply the full generality of the - Isabelle simplifier. Due to the interpretation of theorems as code - equations, rewrites are applied to the right hand side and the - arguments of the left hand side of an equation, but never to the - constant heading the left hand side. An important special case are - \emph{unfold theorems}, which may be declared and removed using - the @{attribute code_unfold} or \emph{@{attribute code_unfold} del} - attribute, respectively. - - Some common applications: -*} - -text_raw {* - \begin{itemize} -*} - -text {* - \item replacing non-executable constructs by executable ones: -*} - -lemma %quote [code_unfold]: - "x \ set xs \ List.member xs x" by (fact in_set_member) - -text {* - \item eliminating superfluous constants: -*} - -lemma %quote [code_unfold]: - "1 = Suc 0" by (fact One_nat_def) - -text {* - \item replacing executable but inconvenient constructs: -*} - -lemma %quote [code_unfold]: - "xs = [] \ List.null xs" by (fact eq_Nil_null) - -text_raw {* - \end{itemize} -*} - -text {* - \noindent \emph{Function transformers} provide a very general interface, - transforming a list of function theorems to another - list of function theorems, provided that neither the heading - constant nor its type change. The @{term "0\nat"} / @{const Suc} - pattern elimination implemented in - theory @{text Efficient_Nat} (see \secref{eff_nat}) uses this - interface. - - \noindent The current setup of the preprocessor may be inspected using - the @{command print_codeproc} command. - @{command code_thms} provides a convenient - mechanism to inspect the impact of a preprocessor setup - on code equations. - - \begin{warn} - - Attribute @{attribute code_unfold} also applies to the - preprocessor of the ancient @{text "SML code generator"}; in case - this is not what you intend, use @{attribute code_inline} instead. - \end{warn} -*} - -subsection {* Datatypes \label{sec:datatypes} *} - -text {* - 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 exactly 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 - @{command print_codesetup} command. - - In some cases, it is appropriate to alter or extend this table. As - an example, we will develop an alternative representation of the - queue example given in \secref{sec:intro}. The amortised - representation is convenient for generating code but exposes its - \qt{implementation} details, which may be cumbersome when proving - theorems about it. Therefore, here is a simple, straightforward - representation of queues: -*} - -datatype %quote 'a queue = Queue "'a list" - -definition %quote empty :: "'a queue" where - "empty = Queue []" - -primrec %quote enqueue :: "'a \ 'a queue \ 'a queue" where - "enqueue x (Queue xs) = Queue (xs @ [x])" - -fun %quote dequeue :: "'a queue \ 'a option \ 'a queue" where - "dequeue (Queue []) = (None, Queue [])" - | "dequeue (Queue (x # xs)) = (Some x, Queue xs)" - -text {* - \noindent This we can use directly for proving; for executing, - we provide an alternative characterisation: -*} - -definition %quote AQueue :: "'a list \ 'a list \ 'a queue" where - "AQueue xs ys = Queue (ys @ rev xs)" - -code_datatype %quote AQueue - -text {* - \noindent Here we define a \qt{constructor} @{const "AQueue"} which - is defined in terms of @{text "Queue"} and interprets its arguments - according to what the \emph{content} of an amortised queue is supposed - to be. Equipped with this, we are able to prove the following equations - for our primitive queue operations which \qt{implement} the simple - queues in an amortised fashion: -*} - -lemma %quote empty_AQueue [code]: - "empty = AQueue [] []" - unfolding AQueue_def empty_def by simp - -lemma %quote enqueue_AQueue [code]: - "enqueue x (AQueue xs ys) = AQueue (x # xs) ys" - unfolding AQueue_def by simp - -lemma %quote dequeue_AQueue [code]: - "dequeue (AQueue xs []) = - (if xs = [] then (None, AQueue [] []) - else dequeue (AQueue [] (rev xs)))" - "dequeue (AQueue xs (y # ys)) = (Some y, AQueue xs ys)" - unfolding AQueue_def by simp_all - -text {* - \noindent For completeness, we provide a substitute for the - @{text case} combinator on queues: -*} - -lemma %quote queue_case_AQueue [code]: - "queue_case f (AQueue xs ys) = f (ys @ rev xs)" - unfolding AQueue_def by simp - -text {* - \noindent The resulting code looks as expected: -*} - -text %quote {*@{code_stmts empty enqueue dequeue (SML)}*} - -text {* - \noindent From this example, it can be glimpsed that using own - constructor sets is a little delicate since it changes the set of - valid patterns for values of that type. Without going into much - detail, here some practical hints: - - \begin{itemize} - - \item When changing the constructor set for datatypes, take care - to provide alternative equations for the @{text case} combinator. - - \item Values in the target language need not to be normalised -- - different values in the target language may represent the same - value in the logic. - - \item Usually, a good methodology to deal with the subtleties of - pattern matching is to see the type as an abstract type: provide - a set of operations which operate on the concrete representation - of the type, and derive further operations by combinations of - these primitive ones, without relying on a particular - representation. - - \end{itemize} -*} - - -subsection {* Equality *} - -text {* - Surely you have already noticed how equality is treated - by the code generator: -*} - -primrec %quote 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 {* - \noindent During preprocessing, the membership test is rewritten, - resulting in @{const List.member}, which itself - performs an explicit equality check. -*} - -text %quote {*@{code_stmts collect_duplicates (SML)}*} - -text {* - \noindent Obviously, polymorphic equality is implemented the Haskell - way using a type class. How is this achieved? HOL introduces - an explicit class @{class eq} with a corresponding operation - @{const eq_class.eq} such that @{thm eq [no_vars]}. - The preprocessing framework does the rest by propagating the - @{class eq} constraints through all dependent code equations. - For datatypes, instances of @{class eq} are implicitly derived - when possible. For other types, you may instantiate @{text eq} - manually like any other type class. -*} - - -subsection {* Explicit partiality *} - -text {* - Partiality usually enters the game by partial patterns, as - in the following example, again for amortised queues: -*} - -definition %quote strict_dequeue :: "'a queue \ 'a \ 'a queue" where - "strict_dequeue q = (case dequeue q - of (Some x, q') \ (x, q'))" - -lemma %quote strict_dequeue_AQueue [code]: - "strict_dequeue (AQueue xs (y # ys)) = (y, AQueue xs ys)" - "strict_dequeue (AQueue xs []) = - (case rev xs of y # ys \ (y, AQueue [] ys))" - by (simp_all add: strict_dequeue_def dequeue_AQueue split: list.splits) - -text {* - \noindent In the corresponding code, there is no equation - for the pattern @{term "AQueue [] []"}: -*} - -text %quote {*@{code_stmts strict_dequeue (consts) strict_dequeue (Haskell)}*} - -text {* - \noindent In some cases it is desirable to have this - pseudo-\qt{partiality} more explicitly, e.g.~as follows: -*} - -axiomatization %quote empty_queue :: 'a - -definition %quote strict_dequeue' :: "'a queue \ 'a \ 'a queue" where - "strict_dequeue' q = (case dequeue q of (Some x, q') \ (x, q') | _ \ empty_queue)" - -lemma %quote strict_dequeue'_AQueue [code]: - "strict_dequeue' (AQueue xs []) = (if xs = [] then empty_queue - else strict_dequeue' (AQueue [] (rev xs)))" - "strict_dequeue' (AQueue xs (y # ys)) = - (y, AQueue xs ys)" - by (simp_all add: strict_dequeue'_def dequeue_AQueue split: list.splits) - -text {* - Observe that on the right hand side of the definition of @{const - "strict_dequeue'"}, the unspecified constant @{const empty_queue} occurs. - - Normally, if constants without any code equations occur in a - program, the code generator complains (since in most cases this is - indeed an error). But such constants can also be thought - of as function definitions which always fail, - since there is never a successful pattern match on the left hand - side. In order to categorise a constant into that category - explicitly, use @{command "code_abort"}: -*} - -code_abort %quote empty_queue - -text {* - \noindent Then the code generator will just insert an error or - exception at the appropriate position: -*} - -text %quote {*@{code_stmts strict_dequeue' (consts) empty_queue strict_dequeue' (Haskell)}*} - -text {* - \noindent This feature however is rarely needed in practice. - Note also that the @{text HOL} default setup already declares - @{const undefined} as @{command "code_abort"}, which is most - likely to be used in such situations. -*} - -end diff -r 7eb0f6991e25 -r 001f2f44984c doc-src/Codegen/Thy/ROOT.ML --- a/doc-src/Codegen/Thy/ROOT.ML Sat Aug 14 12:01:50 2010 +0200 +++ b/doc-src/Codegen/Thy/ROOT.ML Sat Aug 14 13:24:06 2010 +0200 @@ -1,10 +1,9 @@ no_document use_thy "Setup"; -no_document use_thys ["Efficient_Nat"]; use_thy "Introduction"; -use_thy "Program"; +use_thy "Foundations"; +use_thy "Refinement"; use_thy "Inductive_Predicate"; use_thy "Adaptation"; use_thy "Further"; -use_thy "ML"; diff -r 7eb0f6991e25 -r 001f2f44984c doc-src/Codegen/Thy/Refinement.thy --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/doc-src/Codegen/Thy/Refinement.thy Sat Aug 14 13:24:06 2010 +0200 @@ -0,0 +1,7 @@ +theory Refinement +imports Setup +begin + +section {* Program and datatype refinement \label{sec:refinement} *} + +end diff -r 7eb0f6991e25 -r 001f2f44984c doc-src/Codegen/Thy/document/Foundations.tex --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/doc-src/Codegen/Thy/document/Foundations.tex Sat Aug 14 13:24:06 2010 +0200 @@ -0,0 +1,1013 @@ +% +\begin{isabellebody}% +\def\isabellecontext{Foundations}% +% +\isadelimtheory +% +\endisadelimtheory +% +\isatagtheory +\isacommand{theory}\isamarkupfalse% +\ Foundations\isanewline +\isakeyword{imports}\ Introduction\isanewline +\isakeyword{begin}% +\endisatagtheory +{\isafoldtheory}% +% +\isadelimtheory +% +\endisadelimtheory +% +\isamarkupsection{Code generation foundations \label{sec:program}% +} +\isamarkuptrue% +% +\isamarkupsubsection{The \isa{Isabelle{\isacharslash}HOL} default setup% +} +\isamarkuptrue% +% +\begin{isamarkuptext}% +We have already seen how by default equations stemming from + \hyperlink{command.definition}{\mbox{\isa{\isacommand{definition}}}}, \hyperlink{command.primrec}{\mbox{\isa{\isacommand{primrec}}}} and \hyperlink{command.fun}{\mbox{\isa{\isacommand{fun}}}} + statements are used for code generation. This default behaviour + can be changed, e.g.\ by providing different code equations. + The customisations shown in this section are \emph{safe} + as regards correctness: all programs that can be generated are partially + correct.% +\end{isamarkuptext}% +\isamarkuptrue% +% +\isamarkupsubsection{Selecting code equations% +} +\isamarkuptrue% +% +\begin{isamarkuptext}% +Coming back to our introductory example, we + could provide an alternative code equations for \isa{dequeue} + explicitly:% +\end{isamarkuptext}% +\isamarkuptrue% +% +\isadelimquote +% +\endisadelimquote +% +\isatagquote +\isacommand{lemma}\isamarkupfalse% +\ {\isacharbrackleft}code{\isacharbrackright}{\isacharcolon}\isanewline +\ \ {\isachardoublequoteopen}dequeue\ {\isacharparenleft}AQueue\ xs\ {\isacharbrackleft}{\isacharbrackright}{\isacharparenright}\ {\isacharequal}\isanewline +\ \ \ \ \ {\isacharparenleft}if\ xs\ {\isacharequal}\ {\isacharbrackleft}{\isacharbrackright}\ then\ {\isacharparenleft}None{\isacharcomma}\ AQueue\ {\isacharbrackleft}{\isacharbrackright}\ {\isacharbrackleft}{\isacharbrackright}{\isacharparenright}\isanewline +\ \ \ \ \ \ \ else\ dequeue\ {\isacharparenleft}AQueue\ {\isacharbrackleft}{\isacharbrackright}\ {\isacharparenleft}rev\ xs{\isacharparenright}{\isacharparenright}{\isacharparenright}{\isachardoublequoteclose}\isanewline +\ \ {\isachardoublequoteopen}dequeue\ {\isacharparenleft}AQueue\ xs\ {\isacharparenleft}y\ {\isacharhash}\ ys{\isacharparenright}{\isacharparenright}\ {\isacharequal}\isanewline +\ \ \ \ \ {\isacharparenleft}Some\ y{\isacharcomma}\ AQueue\ xs\ ys{\isacharparenright}{\isachardoublequoteclose}\isanewline +\ \ \isacommand{by}\isamarkupfalse% +\ {\isacharparenleft}cases\ xs{\isacharcomma}\ simp{\isacharunderscore}all{\isacharparenright}\ {\isacharparenleft}cases\ {\isachardoublequoteopen}rev\ xs{\isachardoublequoteclose}{\isacharcomma}\ simp{\isacharunderscore}all{\isacharparenright}% +\endisatagquote +{\isafoldquote}% +% +\isadelimquote +% +\endisadelimquote +% +\begin{isamarkuptext}% +\noindent The annotation \isa{{\isacharbrackleft}code{\isacharbrackright}} is an \isa{Isar} + \isa{attribute} which states that the given theorems should be + considered as code equations for a \isa{fun} statement -- + the corresponding constant is determined syntactically. The resulting code:% +\end{isamarkuptext}% +\isamarkuptrue% +% +\isadelimquote +% +\endisadelimquote +% +\isatagquote +% +\begin{isamarkuptext}% +\isatypewriter% +\noindent% +\hspace*{0pt}dequeue ::~forall a.~Queue a -> (Maybe a,~Queue a);\\ +\hspace*{0pt}dequeue (AQueue xs (y :~ys)) = (Just y,~AQueue xs ys);\\ +\hspace*{0pt}dequeue (AQueue xs []) =\\ +\hspace*{0pt} ~(if null xs then (Nothing,~AQueue [] [])\\ +\hspace*{0pt} ~~~else dequeue (AQueue [] (reverse xs)));% +\end{isamarkuptext}% +\isamarkuptrue% +% +\endisatagquote +{\isafoldquote}% +% +\isadelimquote +% +\endisadelimquote +% +\begin{isamarkuptext}% +\noindent You may note that the equality test \isa{xs\ {\isacharequal}\ {\isacharbrackleft}{\isacharbrackright}} has been + replaced by the predicate \isa{null\ xs}. This is due to the default + setup in the \qn{preprocessor} to be discussed further below (\secref{sec:preproc}). + + Changing the default constructor set of datatypes is also + possible. See \secref{sec:datatypes} for an example. + + As told in \secref{sec:concept}, code generation is based + on a structured collection of code theorems. + This collection + may be inspected using the \hyperlink{command.code-thms}{\mbox{\isa{\isacommand{code{\isacharunderscore}thms}}}} command:% +\end{isamarkuptext}% +\isamarkuptrue% +% +\isadelimquote +% +\endisadelimquote +% +\isatagquote +\isacommand{code{\isacharunderscore}thms}\isamarkupfalse% +\ dequeue% +\endisatagquote +{\isafoldquote}% +% +\isadelimquote +% +\endisadelimquote +% +\begin{isamarkuptext}% +\noindent prints a table with \emph{all} code equations + for \isa{dequeue}, including + \emph{all} code equations those equations depend + on recursively. + + Similarly, the \hyperlink{command.code-deps}{\mbox{\isa{\isacommand{code{\isacharunderscore}deps}}}} command shows a graph + visualising dependencies between code equations.% +\end{isamarkuptext}% +\isamarkuptrue% +% +\isamarkupsubsection{\isa{class} and \isa{instantiation}% +} +\isamarkuptrue% +% +\begin{isamarkuptext}% +Concerning type classes and code generation, let us examine an example + from abstract algebra:% +\end{isamarkuptext}% +\isamarkuptrue% +% +\isadelimquote +% +\endisadelimquote +% +\isatagquote +\isacommand{class}\isamarkupfalse% +\ semigroup\ {\isacharequal}\isanewline +\ \ \isakeyword{fixes}\ mult\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequoteopen}{\isacharprime}a\ {\isasymRightarrow}\ {\isacharprime}a\ {\isasymRightarrow}\ {\isacharprime}a{\isachardoublequoteclose}\ {\isacharparenleft}\isakeyword{infixl}\ {\isachardoublequoteopen}{\isasymotimes}{\isachardoublequoteclose}\ {\isadigit{7}}{\isadigit{0}}{\isacharparenright}\isanewline +\ \ \isakeyword{assumes}\ assoc{\isacharcolon}\ {\isachardoublequoteopen}{\isacharparenleft}x\ {\isasymotimes}\ y{\isacharparenright}\ {\isasymotimes}\ z\ {\isacharequal}\ x\ {\isasymotimes}\ {\isacharparenleft}y\ {\isasymotimes}\ z{\isacharparenright}{\isachardoublequoteclose}\isanewline +\isanewline +\isacommand{class}\isamarkupfalse% +\ monoid\ {\isacharequal}\ semigroup\ {\isacharplus}\isanewline +\ \ \isakeyword{fixes}\ neutral\ {\isacharcolon}{\isacharcolon}\ {\isacharprime}a\ {\isacharparenleft}{\isachardoublequoteopen}{\isasymone}{\isachardoublequoteclose}{\isacharparenright}\isanewline +\ \ \isakeyword{assumes}\ neutl{\isacharcolon}\ {\isachardoublequoteopen}{\isasymone}\ {\isasymotimes}\ x\ {\isacharequal}\ x{\isachardoublequoteclose}\isanewline +\ \ \ \ \isakeyword{and}\ neutr{\isacharcolon}\ {\isachardoublequoteopen}x\ {\isasymotimes}\ {\isasymone}\ {\isacharequal}\ x{\isachardoublequoteclose}\isanewline +\isanewline +\isacommand{instantiation}\isamarkupfalse% +\ nat\ {\isacharcolon}{\isacharcolon}\ monoid\isanewline +\isakeyword{begin}\isanewline +\isanewline +\isacommand{primrec}\isamarkupfalse% +\ mult{\isacharunderscore}nat\ \isakeyword{where}\isanewline +\ \ \ \ {\isachardoublequoteopen}{\isadigit{0}}\ {\isasymotimes}\ n\ {\isacharequal}\ {\isacharparenleft}{\isadigit{0}}{\isasymColon}nat{\isacharparenright}{\isachardoublequoteclose}\isanewline +\ \ {\isacharbar}\ {\isachardoublequoteopen}Suc\ m\ {\isasymotimes}\ n\ {\isacharequal}\ n\ {\isacharplus}\ m\ {\isasymotimes}\ n{\isachardoublequoteclose}\isanewline +\isanewline +\isacommand{definition}\isamarkupfalse% +\ neutral{\isacharunderscore}nat\ \isakeyword{where}\isanewline +\ \ {\isachardoublequoteopen}{\isasymone}\ {\isacharequal}\ Suc\ {\isadigit{0}}{\isachardoublequoteclose}\isanewline +\isanewline +\isacommand{lemma}\isamarkupfalse% +\ add{\isacharunderscore}mult{\isacharunderscore}distrib{\isacharcolon}\isanewline +\ \ \isakeyword{fixes}\ n\ m\ q\ {\isacharcolon}{\isacharcolon}\ nat\isanewline +\ \ \isakeyword{shows}\ {\isachardoublequoteopen}{\isacharparenleft}n\ {\isacharplus}\ m{\isacharparenright}\ {\isasymotimes}\ q\ {\isacharequal}\ n\ {\isasymotimes}\ q\ {\isacharplus}\ m\ {\isasymotimes}\ q{\isachardoublequoteclose}\isanewline +\ \ \isacommand{by}\isamarkupfalse% +\ {\isacharparenleft}induct\ n{\isacharparenright}\ simp{\isacharunderscore}all\isanewline +\isanewline +\isacommand{instance}\isamarkupfalse% +\ \isacommand{proof}\isamarkupfalse% +\isanewline +\ \ \isacommand{fix}\isamarkupfalse% +\ m\ n\ q\ {\isacharcolon}{\isacharcolon}\ nat\isanewline +\ \ \isacommand{show}\isamarkupfalse% +\ {\isachardoublequoteopen}m\ {\isasymotimes}\ n\ {\isasymotimes}\ q\ {\isacharequal}\ m\ {\isasymotimes}\ {\isacharparenleft}n\ {\isasymotimes}\ q{\isacharparenright}{\isachardoublequoteclose}\isanewline +\ \ \ \ \isacommand{by}\isamarkupfalse% +\ {\isacharparenleft}induct\ m{\isacharparenright}\ {\isacharparenleft}simp{\isacharunderscore}all\ add{\isacharcolon}\ add{\isacharunderscore}mult{\isacharunderscore}distrib{\isacharparenright}\isanewline +\ \ \isacommand{show}\isamarkupfalse% +\ {\isachardoublequoteopen}{\isasymone}\ {\isasymotimes}\ n\ {\isacharequal}\ n{\isachardoublequoteclose}\isanewline +\ \ \ \ \isacommand{by}\isamarkupfalse% +\ {\isacharparenleft}simp\ add{\isacharcolon}\ neutral{\isacharunderscore}nat{\isacharunderscore}def{\isacharparenright}\isanewline +\ \ \isacommand{show}\isamarkupfalse% +\ {\isachardoublequoteopen}m\ {\isasymotimes}\ {\isasymone}\ {\isacharequal}\ m{\isachardoublequoteclose}\isanewline +\ \ \ \ \isacommand{by}\isamarkupfalse% +\ {\isacharparenleft}induct\ m{\isacharparenright}\ {\isacharparenleft}simp{\isacharunderscore}all\ add{\isacharcolon}\ neutral{\isacharunderscore}nat{\isacharunderscore}def{\isacharparenright}\isanewline +\isacommand{qed}\isamarkupfalse% +\isanewline +\isanewline +\isacommand{end}\isamarkupfalse% +% +\endisatagquote +{\isafoldquote}% +% +\isadelimquote +% +\endisadelimquote +% +\begin{isamarkuptext}% +\noindent We define the natural operation of the natural numbers + on monoids:% +\end{isamarkuptext}% +\isamarkuptrue% +% +\isadelimquote +% +\endisadelimquote +% +\isatagquote +\isacommand{primrec}\isamarkupfalse% +\ {\isacharparenleft}\isakeyword{in}\ monoid{\isacharparenright}\ pow\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequoteopen}nat\ {\isasymRightarrow}\ {\isacharprime}a\ {\isasymRightarrow}\ {\isacharprime}a{\isachardoublequoteclose}\ \isakeyword{where}\isanewline +\ \ \ \ {\isachardoublequoteopen}pow\ {\isadigit{0}}\ a\ {\isacharequal}\ {\isasymone}{\isachardoublequoteclose}\isanewline +\ \ {\isacharbar}\ {\isachardoublequoteopen}pow\ {\isacharparenleft}Suc\ n{\isacharparenright}\ a\ {\isacharequal}\ a\ {\isasymotimes}\ pow\ n\ a{\isachardoublequoteclose}% +\endisatagquote +{\isafoldquote}% +% +\isadelimquote +% +\endisadelimquote +% +\begin{isamarkuptext}% +\noindent This we use to define the discrete exponentiation function:% +\end{isamarkuptext}% +\isamarkuptrue% +% +\isadelimquote +% +\endisadelimquote +% +\isatagquote +\isacommand{definition}\isamarkupfalse% +\ bexp\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequoteopen}nat\ {\isasymRightarrow}\ nat{\isachardoublequoteclose}\ \isakeyword{where}\isanewline +\ \ {\isachardoublequoteopen}bexp\ n\ {\isacharequal}\ pow\ n\ {\isacharparenleft}Suc\ {\isacharparenleft}Suc\ {\isadigit{0}}{\isacharparenright}{\isacharparenright}{\isachardoublequoteclose}% +\endisatagquote +{\isafoldquote}% +% +\isadelimquote +% +\endisadelimquote +% +\begin{isamarkuptext}% +\noindent The corresponding code in Haskell uses that language's native classes:% +\end{isamarkuptext}% +\isamarkuptrue% +% +\isadelimquote +% +\endisadelimquote +% +\isatagquote +% +\begin{isamarkuptext}% +\isatypewriter% +\noindent% +\hspace*{0pt}module Example where {\char123}\\ +\hspace*{0pt}\\ +\hspace*{0pt}data Nat = Zero{\char95}nat | Suc Nat;\\ +\hspace*{0pt}\\ +\hspace*{0pt}plus{\char95}nat ::~Nat -> Nat -> Nat;\\ +\hspace*{0pt}plus{\char95}nat (Suc m) n = plus{\char95}nat m (Suc n);\\ +\hspace*{0pt}plus{\char95}nat Zero{\char95}nat n = n;\\ +\hspace*{0pt}\\ +\hspace*{0pt}class Semigroup a where {\char123}\\ +\hspace*{0pt} ~mult ::~a -> a -> a;\\ +\hspace*{0pt}{\char125};\\ +\hspace*{0pt}\\ +\hspace*{0pt}class (Semigroup a) => Monoid a where {\char123}\\ +\hspace*{0pt} ~neutral ::~a;\\ +\hspace*{0pt}{\char125};\\ +\hspace*{0pt}\\ +\hspace*{0pt}pow ::~forall a.~(Monoid a) => Nat -> a -> a;\\ +\hspace*{0pt}pow Zero{\char95}nat a = neutral;\\ +\hspace*{0pt}pow (Suc n) a = mult a (pow n a);\\ +\hspace*{0pt}\\ +\hspace*{0pt}mult{\char95}nat ::~Nat -> Nat -> Nat;\\ +\hspace*{0pt}mult{\char95}nat Zero{\char95}nat n = Zero{\char95}nat;\\ +\hspace*{0pt}mult{\char95}nat (Suc m) n = plus{\char95}nat n (mult{\char95}nat m n);\\ +\hspace*{0pt}\\ +\hspace*{0pt}neutral{\char95}nat ::~Nat;\\ +\hspace*{0pt}neutral{\char95}nat = Suc Zero{\char95}nat;\\ +\hspace*{0pt}\\ +\hspace*{0pt}instance Semigroup Nat where {\char123}\\ +\hspace*{0pt} ~mult = mult{\char95}nat;\\ +\hspace*{0pt}{\char125};\\ +\hspace*{0pt}\\ +\hspace*{0pt}instance Monoid Nat where {\char123}\\ +\hspace*{0pt} ~neutral = neutral{\char95}nat;\\ +\hspace*{0pt}{\char125};\\ +\hspace*{0pt}\\ +\hspace*{0pt}bexp ::~Nat -> Nat;\\ +\hspace*{0pt}bexp n = pow n (Suc (Suc Zero{\char95}nat));\\ +\hspace*{0pt}\\ +\hspace*{0pt}{\char125}% +\end{isamarkuptext}% +\isamarkuptrue% +% +\endisatagquote +{\isafoldquote}% +% +\isadelimquote +% +\endisadelimquote +% +\begin{isamarkuptext}% +\noindent This is a convenient place to show how explicit dictionary construction + manifests in generated code (here, the same example in \isa{SML}) + \cite{Haftmann-Nipkow:2010:code}:% +\end{isamarkuptext}% +\isamarkuptrue% +% +\isadelimquote +% +\endisadelimquote +% +\isatagquote +% +\begin{isamarkuptext}% +\isatypewriter% +\noindent% +\hspace*{0pt}structure Example :~sig\\ +\hspace*{0pt} ~datatype nat = Zero{\char95}nat | Suc of nat\\ +\hspace*{0pt} ~val plus{\char95}nat :~nat -> nat -> nat\\ +\hspace*{0pt} ~type 'a semigroup\\ +\hspace*{0pt} ~val mult :~'a semigroup -> 'a -> 'a -> 'a\\ +\hspace*{0pt} ~type 'a monoid\\ +\hspace*{0pt} ~val semigroup{\char95}monoid :~'a monoid -> 'a semigroup\\ +\hspace*{0pt} ~val neutral :~'a monoid -> 'a\\ +\hspace*{0pt} ~val pow :~'a monoid -> nat -> 'a -> 'a\\ +\hspace*{0pt} ~val mult{\char95}nat :~nat -> nat -> nat\\ +\hspace*{0pt} ~val neutral{\char95}nat :~nat\\ +\hspace*{0pt} ~val semigroup{\char95}nat :~nat semigroup\\ +\hspace*{0pt} ~val monoid{\char95}nat :~nat monoid\\ +\hspace*{0pt} ~val bexp :~nat -> nat\\ +\hspace*{0pt}end = struct\\ +\hspace*{0pt}\\ +\hspace*{0pt}datatype nat = Zero{\char95}nat | Suc of nat;\\ +\hspace*{0pt}\\ +\hspace*{0pt}fun plus{\char95}nat (Suc m) n = plus{\char95}nat m (Suc n)\\ +\hspace*{0pt} ~| plus{\char95}nat Zero{\char95}nat n = n;\\ +\hspace*{0pt}\\ +\hspace*{0pt}type 'a semigroup = {\char123}mult :~'a -> 'a -> 'a{\char125};\\ +\hspace*{0pt}val mult = {\char35}mult :~'a semigroup -> 'a -> 'a -> 'a;\\ +\hspace*{0pt}\\ +\hspace*{0pt}type 'a monoid = {\char123}semigroup{\char95}monoid :~'a semigroup,~neutral :~'a{\char125};\\ +\hspace*{0pt}val semigroup{\char95}monoid = {\char35}semigroup{\char95}monoid :~'a monoid -> 'a semigroup;\\ +\hspace*{0pt}val neutral = {\char35}neutral :~'a monoid -> 'a;\\ +\hspace*{0pt}\\ +\hspace*{0pt}fun pow A{\char95}~Zero{\char95}nat a = neutral A{\char95}\\ +\hspace*{0pt} ~| pow A{\char95}~(Suc n) a = mult (semigroup{\char95}monoid A{\char95}) a (pow A{\char95}~n a);\\ +\hspace*{0pt}\\ +\hspace*{0pt}fun mult{\char95}nat Zero{\char95}nat n = Zero{\char95}nat\\ +\hspace*{0pt} ~| mult{\char95}nat (Suc m) n = plus{\char95}nat n (mult{\char95}nat m n);\\ +\hspace*{0pt}\\ +\hspace*{0pt}val neutral{\char95}nat :~nat = Suc Zero{\char95}nat;\\ +\hspace*{0pt}\\ +\hspace*{0pt}val semigroup{\char95}nat = {\char123}mult = mult{\char95}nat{\char125}~:~nat semigroup;\\ +\hspace*{0pt}\\ +\hspace*{0pt}val monoid{\char95}nat = {\char123}semigroup{\char95}monoid = semigroup{\char95}nat,~neutral = neutral{\char95}nat{\char125}\\ +\hspace*{0pt} ~:~nat monoid;\\ +\hspace*{0pt}\\ +\hspace*{0pt}fun bexp n = pow monoid{\char95}nat n (Suc (Suc Zero{\char95}nat));\\ +\hspace*{0pt}\\ +\hspace*{0pt}end;~(*struct Example*)% +\end{isamarkuptext}% +\isamarkuptrue% +% +\endisatagquote +{\isafoldquote}% +% +\isadelimquote +% +\endisadelimquote +% +\begin{isamarkuptext}% +\noindent Note the parameters with trailing underscore (\verb|A_|), + which are the dictionary parameters.% +\end{isamarkuptext}% +\isamarkuptrue% +% +\isamarkupsubsection{The preprocessor \label{sec:preproc}% +} +\isamarkuptrue% +% +\begin{isamarkuptext}% +Before selected function theorems are turned into abstract + code, a chain of definitional transformation steps is carried + out: \emph{preprocessing}. In essence, the preprocessor + consists of two components: a \emph{simpset} and \emph{function transformers}. + + The \emph{simpset} can apply the full generality of the + Isabelle simplifier. Due to the interpretation of theorems as code + equations, rewrites are applied to the right hand side and the + arguments of the left hand side of an equation, but never to the + constant heading the left hand side. An important special case are + \emph{unfold theorems}, which may be declared and removed using + the \hyperlink{attribute.code-unfold}{\mbox{\isa{code{\isacharunderscore}unfold}}} or \emph{\hyperlink{attribute.code-unfold}{\mbox{\isa{code{\isacharunderscore}unfold}}} del} + attribute, respectively. + + Some common applications:% +\end{isamarkuptext}% +\isamarkuptrue% +% +\begin{itemize} +% +\begin{isamarkuptext}% +\item replacing non-executable constructs by executable ones:% +\end{isamarkuptext}% +\isamarkuptrue% +% +\isadelimquote +% +\endisadelimquote +% +\isatagquote +\isacommand{lemma}\isamarkupfalse% +\ {\isacharbrackleft}code{\isacharunderscore}unfold{\isacharbrackright}{\isacharcolon}\isanewline +\ \ {\isachardoublequoteopen}x\ {\isasymin}\ set\ xs\ {\isasymlongleftrightarrow}\ List{\isachardot}member\ xs\ x{\isachardoublequoteclose}\ \isacommand{by}\isamarkupfalse% +\ {\isacharparenleft}fact\ in{\isacharunderscore}set{\isacharunderscore}member{\isacharparenright}% +\endisatagquote +{\isafoldquote}% +% +\isadelimquote +% +\endisadelimquote +% +\begin{isamarkuptext}% +\item eliminating superfluous constants:% +\end{isamarkuptext}% +\isamarkuptrue% +% +\isadelimquote +% +\endisadelimquote +% +\isatagquote +\isacommand{lemma}\isamarkupfalse% +\ {\isacharbrackleft}code{\isacharunderscore}unfold{\isacharbrackright}{\isacharcolon}\isanewline +\ \ {\isachardoublequoteopen}{\isadigit{1}}\ {\isacharequal}\ Suc\ {\isadigit{0}}{\isachardoublequoteclose}\ \isacommand{by}\isamarkupfalse% +\ {\isacharparenleft}fact\ One{\isacharunderscore}nat{\isacharunderscore}def{\isacharparenright}% +\endisatagquote +{\isafoldquote}% +% +\isadelimquote +% +\endisadelimquote +% +\begin{isamarkuptext}% +\item replacing executable but inconvenient constructs:% +\end{isamarkuptext}% +\isamarkuptrue% +% +\isadelimquote +% +\endisadelimquote +% +\isatagquote +\isacommand{lemma}\isamarkupfalse% +\ {\isacharbrackleft}code{\isacharunderscore}unfold{\isacharbrackright}{\isacharcolon}\isanewline +\ \ {\isachardoublequoteopen}xs\ {\isacharequal}\ {\isacharbrackleft}{\isacharbrackright}\ {\isasymlongleftrightarrow}\ List{\isachardot}null\ xs{\isachardoublequoteclose}\ \isacommand{by}\isamarkupfalse% +\ {\isacharparenleft}fact\ eq{\isacharunderscore}Nil{\isacharunderscore}null{\isacharparenright}% +\endisatagquote +{\isafoldquote}% +% +\isadelimquote +% +\endisadelimquote +% +\end{itemize} +% +\begin{isamarkuptext}% +\noindent \emph{Function transformers} provide a very general interface, + transforming a list of function theorems to another + list of function theorems, provided that neither the heading + constant nor its type change. The \isa{{\isadigit{0}}} / \isa{Suc} + pattern elimination implemented in + theory \isa{Efficient{\isacharunderscore}Nat} (see \secref{eff_nat}) uses this + interface. + + \noindent The current setup of the preprocessor may be inspected using + the \hyperlink{command.print-codeproc}{\mbox{\isa{\isacommand{print{\isacharunderscore}codeproc}}}} command. + \hyperlink{command.code-thms}{\mbox{\isa{\isacommand{code{\isacharunderscore}thms}}}} provides a convenient + mechanism to inspect the impact of a preprocessor setup + on code equations. + + \begin{warn} + + Attribute \hyperlink{attribute.code-unfold}{\mbox{\isa{code{\isacharunderscore}unfold}}} also applies to the + preprocessor of the ancient \isa{SML\ code\ generator}; in case + this is not what you intend, use \hyperlink{attribute.code-inline}{\mbox{\isa{code{\isacharunderscore}inline}}} instead. + \end{warn}% +\end{isamarkuptext}% +\isamarkuptrue% +% +\isamarkupsubsection{Datatypes \label{sec:datatypes}% +} +\isamarkuptrue% +% +\begin{isamarkuptext}% +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 exactly 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 + \hyperlink{command.print-codesetup}{\mbox{\isa{\isacommand{print{\isacharunderscore}codesetup}}}} command. + + In some cases, it is appropriate to alter or extend this table. As + an example, we will develop an alternative representation of the + queue example given in \secref{sec:intro}. The amortised + representation is convenient for generating code but exposes its + \qt{implementation} details, which may be cumbersome when proving + theorems about it. Therefore, here is a simple, straightforward + representation of queues:% +\end{isamarkuptext}% +\isamarkuptrue% +% +\isadelimquote +% +\endisadelimquote +% +\isatagquote +\isacommand{datatype}\isamarkupfalse% +\ {\isacharprime}a\ queue\ {\isacharequal}\ Queue\ {\isachardoublequoteopen}{\isacharprime}a\ list{\isachardoublequoteclose}\isanewline +\isanewline +\isacommand{definition}\isamarkupfalse% +\ empty\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequoteopen}{\isacharprime}a\ queue{\isachardoublequoteclose}\ \isakeyword{where}\isanewline +\ \ {\isachardoublequoteopen}empty\ {\isacharequal}\ Queue\ {\isacharbrackleft}{\isacharbrackright}{\isachardoublequoteclose}\isanewline +\isanewline +\isacommand{primrec}\isamarkupfalse% +\ enqueue\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequoteopen}{\isacharprime}a\ {\isasymRightarrow}\ {\isacharprime}a\ queue\ {\isasymRightarrow}\ {\isacharprime}a\ queue{\isachardoublequoteclose}\ \isakeyword{where}\isanewline +\ \ {\isachardoublequoteopen}enqueue\ x\ {\isacharparenleft}Queue\ xs{\isacharparenright}\ {\isacharequal}\ Queue\ {\isacharparenleft}xs\ {\isacharat}\ {\isacharbrackleft}x{\isacharbrackright}{\isacharparenright}{\isachardoublequoteclose}\isanewline +\isanewline +\isacommand{fun}\isamarkupfalse% +\ dequeue\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequoteopen}{\isacharprime}a\ queue\ {\isasymRightarrow}\ {\isacharprime}a\ option\ {\isasymtimes}\ {\isacharprime}a\ queue{\isachardoublequoteclose}\ \isakeyword{where}\isanewline +\ \ \ \ {\isachardoublequoteopen}dequeue\ {\isacharparenleft}Queue\ {\isacharbrackleft}{\isacharbrackright}{\isacharparenright}\ {\isacharequal}\ {\isacharparenleft}None{\isacharcomma}\ Queue\ {\isacharbrackleft}{\isacharbrackright}{\isacharparenright}{\isachardoublequoteclose}\isanewline +\ \ {\isacharbar}\ {\isachardoublequoteopen}dequeue\ {\isacharparenleft}Queue\ {\isacharparenleft}x\ {\isacharhash}\ xs{\isacharparenright}{\isacharparenright}\ {\isacharequal}\ {\isacharparenleft}Some\ x{\isacharcomma}\ Queue\ xs{\isacharparenright}{\isachardoublequoteclose}% +\endisatagquote +{\isafoldquote}% +% +\isadelimquote +% +\endisadelimquote +% +\begin{isamarkuptext}% +\noindent This we can use directly for proving; for executing, + we provide an alternative characterisation:% +\end{isamarkuptext}% +\isamarkuptrue% +% +\isadelimquote +% +\endisadelimquote +% +\isatagquote +\isacommand{definition}\isamarkupfalse% +\ AQueue\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequoteopen}{\isacharprime}a\ list\ {\isasymRightarrow}\ {\isacharprime}a\ list\ {\isasymRightarrow}\ {\isacharprime}a\ queue{\isachardoublequoteclose}\ \isakeyword{where}\isanewline +\ \ {\isachardoublequoteopen}AQueue\ xs\ ys\ {\isacharequal}\ Queue\ {\isacharparenleft}ys\ {\isacharat}\ rev\ xs{\isacharparenright}{\isachardoublequoteclose}\isanewline +\isanewline +\isacommand{code{\isacharunderscore}datatype}\isamarkupfalse% +\ AQueue% +\endisatagquote +{\isafoldquote}% +% +\isadelimquote +% +\endisadelimquote +% +\begin{isamarkuptext}% +\noindent Here we define a \qt{constructor} \isa{AQueue} which + is defined in terms of \isa{Queue} and interprets its arguments + according to what the \emph{content} of an amortised queue is supposed + to be. Equipped with this, we are able to prove the following equations + for our primitive queue operations which \qt{implement} the simple + queues in an amortised fashion:% +\end{isamarkuptext}% +\isamarkuptrue% +% +\isadelimquote +% +\endisadelimquote +% +\isatagquote +\isacommand{lemma}\isamarkupfalse% +\ empty{\isacharunderscore}AQueue\ {\isacharbrackleft}code{\isacharbrackright}{\isacharcolon}\isanewline +\ \ {\isachardoublequoteopen}empty\ {\isacharequal}\ AQueue\ {\isacharbrackleft}{\isacharbrackright}\ {\isacharbrackleft}{\isacharbrackright}{\isachardoublequoteclose}\isanewline +\ \ \isacommand{unfolding}\isamarkupfalse% +\ AQueue{\isacharunderscore}def\ empty{\isacharunderscore}def\ \isacommand{by}\isamarkupfalse% +\ simp\isanewline +\isanewline +\isacommand{lemma}\isamarkupfalse% +\ enqueue{\isacharunderscore}AQueue\ {\isacharbrackleft}code{\isacharbrackright}{\isacharcolon}\isanewline +\ \ {\isachardoublequoteopen}enqueue\ x\ {\isacharparenleft}AQueue\ xs\ ys{\isacharparenright}\ {\isacharequal}\ AQueue\ {\isacharparenleft}x\ {\isacharhash}\ xs{\isacharparenright}\ ys{\isachardoublequoteclose}\isanewline +\ \ \isacommand{unfolding}\isamarkupfalse% +\ AQueue{\isacharunderscore}def\ \isacommand{by}\isamarkupfalse% +\ simp\isanewline +\isanewline +\isacommand{lemma}\isamarkupfalse% +\ dequeue{\isacharunderscore}AQueue\ {\isacharbrackleft}code{\isacharbrackright}{\isacharcolon}\isanewline +\ \ {\isachardoublequoteopen}dequeue\ {\isacharparenleft}AQueue\ xs\ {\isacharbrackleft}{\isacharbrackright}{\isacharparenright}\ {\isacharequal}\isanewline +\ \ \ \ {\isacharparenleft}if\ xs\ {\isacharequal}\ {\isacharbrackleft}{\isacharbrackright}\ then\ {\isacharparenleft}None{\isacharcomma}\ AQueue\ {\isacharbrackleft}{\isacharbrackright}\ {\isacharbrackleft}{\isacharbrackright}{\isacharparenright}\isanewline +\ \ \ \ else\ dequeue\ {\isacharparenleft}AQueue\ {\isacharbrackleft}{\isacharbrackright}\ {\isacharparenleft}rev\ xs{\isacharparenright}{\isacharparenright}{\isacharparenright}{\isachardoublequoteclose}\isanewline +\ \ {\isachardoublequoteopen}dequeue\ {\isacharparenleft}AQueue\ xs\ {\isacharparenleft}y\ {\isacharhash}\ ys{\isacharparenright}{\isacharparenright}\ {\isacharequal}\ {\isacharparenleft}Some\ y{\isacharcomma}\ AQueue\ xs\ ys{\isacharparenright}{\isachardoublequoteclose}\isanewline +\ \ \isacommand{unfolding}\isamarkupfalse% +\ AQueue{\isacharunderscore}def\ \isacommand{by}\isamarkupfalse% +\ simp{\isacharunderscore}all% +\endisatagquote +{\isafoldquote}% +% +\isadelimquote +% +\endisadelimquote +% +\begin{isamarkuptext}% +\noindent For completeness, we provide a substitute for the + \isa{case} combinator on queues:% +\end{isamarkuptext}% +\isamarkuptrue% +% +\isadelimquote +% +\endisadelimquote +% +\isatagquote +\isacommand{lemma}\isamarkupfalse% +\ queue{\isacharunderscore}case{\isacharunderscore}AQueue\ {\isacharbrackleft}code{\isacharbrackright}{\isacharcolon}\isanewline +\ \ {\isachardoublequoteopen}queue{\isacharunderscore}case\ f\ {\isacharparenleft}AQueue\ xs\ ys{\isacharparenright}\ {\isacharequal}\ f\ {\isacharparenleft}ys\ {\isacharat}\ rev\ xs{\isacharparenright}{\isachardoublequoteclose}\isanewline +\ \ \isacommand{unfolding}\isamarkupfalse% +\ AQueue{\isacharunderscore}def\ \isacommand{by}\isamarkupfalse% +\ simp% +\endisatagquote +{\isafoldquote}% +% +\isadelimquote +% +\endisadelimquote +% +\begin{isamarkuptext}% +\noindent The resulting code looks as expected:% +\end{isamarkuptext}% +\isamarkuptrue% +% +\isadelimquote +% +\endisadelimquote +% +\isatagquote +% +\begin{isamarkuptext}% +\isatypewriter% +\noindent% +\hspace*{0pt}structure Example :~sig\\ +\hspace*{0pt} ~val foldl :~('a -> 'b -> 'a) -> 'a -> 'b list -> 'a\\ +\hspace*{0pt} ~val rev :~'a list -> 'a list\\ +\hspace*{0pt} ~val null :~'a list -> bool\\ +\hspace*{0pt} ~datatype 'a queue = AQueue of 'a list * 'a list\\ +\hspace*{0pt} ~val empty :~'a queue\\ +\hspace*{0pt} ~val dequeue :~'a queue -> 'a option * 'a queue\\ +\hspace*{0pt} ~val enqueue :~'a -> 'a queue -> 'a queue\\ +\hspace*{0pt}end = struct\\ +\hspace*{0pt}\\ +\hspace*{0pt}fun foldl f a [] = a\\ +\hspace*{0pt} ~| foldl f a (x ::~xs) = foldl f (f a x) xs;\\ +\hspace*{0pt}\\ +\hspace*{0pt}fun rev xs = foldl (fn xsa => fn x => x ::~xsa) [] xs;\\ +\hspace*{0pt}\\ +\hspace*{0pt}fun null [] = true\\ +\hspace*{0pt} ~| null (x ::~xs) = false;\\ +\hspace*{0pt}\\ +\hspace*{0pt}datatype 'a queue = AQueue of 'a list * 'a list;\\ +\hspace*{0pt}\\ +\hspace*{0pt}val empty :~'a queue = AQueue ([],~[]);\\ +\hspace*{0pt}\\ +\hspace*{0pt}fun dequeue (AQueue (xs,~y ::~ys)) = (SOME y,~AQueue (xs,~ys))\\ +\hspace*{0pt} ~| dequeue (AQueue (xs,~[])) =\\ +\hspace*{0pt} ~~~(if null xs then (NONE,~AQueue ([],~[]))\\ +\hspace*{0pt} ~~~~~else dequeue (AQueue ([],~rev xs)));\\ +\hspace*{0pt}\\ +\hspace*{0pt}fun enqueue x (AQueue (xs,~ys)) = AQueue (x ::~xs,~ys);\\ +\hspace*{0pt}\\ +\hspace*{0pt}end;~(*struct Example*)% +\end{isamarkuptext}% +\isamarkuptrue% +% +\endisatagquote +{\isafoldquote}% +% +\isadelimquote +% +\endisadelimquote +% +\begin{isamarkuptext}% +\noindent From this example, it can be glimpsed that using own + constructor sets is a little delicate since it changes the set of + valid patterns for values of that type. Without going into much + detail, here some practical hints: + + \begin{itemize} + + \item When changing the constructor set for datatypes, take care + to provide alternative equations for the \isa{case} combinator. + + \item Values in the target language need not to be normalised -- + different values in the target language may represent the same + value in the logic. + + \item Usually, a good methodology to deal with the subtleties of + pattern matching is to see the type as an abstract type: provide + a set of operations which operate on the concrete representation + of the type, and derive further operations by combinations of + these primitive ones, without relying on a particular + representation. + + \end{itemize}% +\end{isamarkuptext}% +\isamarkuptrue% +% +\isamarkupsubsection{Equality% +} +\isamarkuptrue% +% +\begin{isamarkuptext}% +Surely you have already noticed how equality is treated + by the code generator:% +\end{isamarkuptext}% +\isamarkuptrue% +% +\isadelimquote +% +\endisadelimquote +% +\isatagquote +\isacommand{primrec}\isamarkupfalse% +\ 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}% +\endisatagquote +{\isafoldquote}% +% +\isadelimquote +% +\endisadelimquote +% +\begin{isamarkuptext}% +\noindent During preprocessing, the membership test is rewritten, + resulting in \isa{List{\isachardot}member}, which itself + performs an explicit equality check.% +\end{isamarkuptext}% +\isamarkuptrue% +% +\isadelimquote +% +\endisadelimquote +% +\isatagquote +% +\begin{isamarkuptext}% +\isatypewriter% +\noindent% +\hspace*{0pt}structure Example :~sig\\ +\hspace*{0pt} ~type 'a eq\\ +\hspace*{0pt} ~val eq :~'a eq -> 'a -> 'a -> bool\\ +\hspace*{0pt} ~val eqa :~'a eq -> 'a -> 'a -> bool\\ +\hspace*{0pt} ~val member :~'a eq -> 'a list -> 'a -> bool\\ +\hspace*{0pt} ~val collect{\char95}duplicates :\\ +\hspace*{0pt} ~~~'a eq -> 'a list -> 'a list -> 'a list -> 'a list\\ +\hspace*{0pt}end = struct\\ +\hspace*{0pt}\\ +\hspace*{0pt}type 'a eq = {\char123}eq :~'a -> 'a -> bool{\char125};\\ +\hspace*{0pt}val eq = {\char35}eq :~'a eq -> 'a -> 'a -> bool;\\ +\hspace*{0pt}\\ +\hspace*{0pt}fun eqa A{\char95}~a b = eq A{\char95}~a b;\\ +\hspace*{0pt}\\ +\hspace*{0pt}fun member A{\char95}~[] y = false\\ +\hspace*{0pt} ~| member A{\char95}~(x ::~xs) y = eqa A{\char95}~x y orelse member A{\char95}~xs y;\\ +\hspace*{0pt}\\ +\hspace*{0pt}fun collect{\char95}duplicates A{\char95}~xs ys [] = xs\\ +\hspace*{0pt} ~| collect{\char95}duplicates A{\char95}~xs ys (z ::~zs) =\\ +\hspace*{0pt} ~~~(if member A{\char95}~xs z\\ +\hspace*{0pt} ~~~~~then (if member A{\char95}~ys z then collect{\char95}duplicates A{\char95}~xs ys zs\\ +\hspace*{0pt} ~~~~~~~~~~~~else collect{\char95}duplicates A{\char95}~xs (z ::~ys) zs)\\ +\hspace*{0pt} ~~~~~else collect{\char95}duplicates A{\char95}~(z ::~xs) (z ::~ys) zs);\\ +\hspace*{0pt}\\ +\hspace*{0pt}end;~(*struct Example*)% +\end{isamarkuptext}% +\isamarkuptrue% +% +\endisatagquote +{\isafoldquote}% +% +\isadelimquote +% +\endisadelimquote +% +\begin{isamarkuptext}% +\noindent Obviously, polymorphic equality is implemented the Haskell + way using a type class. How is this achieved? HOL introduces + an explicit class \isa{eq} with a corresponding operation + \isa{eq{\isacharunderscore}class{\isachardot}eq} such that \isa{eq{\isacharunderscore}class{\isachardot}eq\ {\isacharequal}\ op\ {\isacharequal}}. + The preprocessing framework does the rest by propagating the + \isa{eq} constraints through all dependent code equations. + For datatypes, instances of \isa{eq} are implicitly derived + when possible. For other types, you may instantiate \isa{eq} + manually like any other type class.% +\end{isamarkuptext}% +\isamarkuptrue% +% +\isamarkupsubsection{Explicit partiality% +} +\isamarkuptrue% +% +\begin{isamarkuptext}% +Partiality usually enters the game by partial patterns, as + in the following example, again for amortised queues:% +\end{isamarkuptext}% +\isamarkuptrue% +% +\isadelimquote +% +\endisadelimquote +% +\isatagquote +\isacommand{definition}\isamarkupfalse% +\ strict{\isacharunderscore}dequeue\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequoteopen}{\isacharprime}a\ queue\ {\isasymRightarrow}\ {\isacharprime}a\ {\isasymtimes}\ {\isacharprime}a\ queue{\isachardoublequoteclose}\ \isakeyword{where}\isanewline +\ \ {\isachardoublequoteopen}strict{\isacharunderscore}dequeue\ q\ {\isacharequal}\ {\isacharparenleft}case\ dequeue\ q\isanewline +\ \ \ \ of\ {\isacharparenleft}Some\ x{\isacharcomma}\ q{\isacharprime}{\isacharparenright}\ {\isasymRightarrow}\ {\isacharparenleft}x{\isacharcomma}\ q{\isacharprime}{\isacharparenright}{\isacharparenright}{\isachardoublequoteclose}\isanewline +\isanewline +\isacommand{lemma}\isamarkupfalse% +\ strict{\isacharunderscore}dequeue{\isacharunderscore}AQueue\ {\isacharbrackleft}code{\isacharbrackright}{\isacharcolon}\isanewline +\ \ {\isachardoublequoteopen}strict{\isacharunderscore}dequeue\ {\isacharparenleft}AQueue\ xs\ {\isacharparenleft}y\ {\isacharhash}\ ys{\isacharparenright}{\isacharparenright}\ {\isacharequal}\ {\isacharparenleft}y{\isacharcomma}\ AQueue\ xs\ ys{\isacharparenright}{\isachardoublequoteclose}\isanewline +\ \ {\isachardoublequoteopen}strict{\isacharunderscore}dequeue\ {\isacharparenleft}AQueue\ xs\ {\isacharbrackleft}{\isacharbrackright}{\isacharparenright}\ {\isacharequal}\isanewline +\ \ \ \ {\isacharparenleft}case\ rev\ xs\ of\ y\ {\isacharhash}\ ys\ {\isasymRightarrow}\ {\isacharparenleft}y{\isacharcomma}\ AQueue\ {\isacharbrackleft}{\isacharbrackright}\ ys{\isacharparenright}{\isacharparenright}{\isachardoublequoteclose}\isanewline +\ \ \isacommand{by}\isamarkupfalse% +\ {\isacharparenleft}simp{\isacharunderscore}all\ add{\isacharcolon}\ strict{\isacharunderscore}dequeue{\isacharunderscore}def\ dequeue{\isacharunderscore}AQueue\ split{\isacharcolon}\ list{\isachardot}splits{\isacharparenright}% +\endisatagquote +{\isafoldquote}% +% +\isadelimquote +% +\endisadelimquote +% +\begin{isamarkuptext}% +\noindent In the corresponding code, there is no equation + for the pattern \isa{AQueue\ {\isacharbrackleft}{\isacharbrackright}\ {\isacharbrackleft}{\isacharbrackright}}:% +\end{isamarkuptext}% +\isamarkuptrue% +% +\isadelimquote +% +\endisadelimquote +% +\isatagquote +% +\begin{isamarkuptext}% +\isatypewriter% +\noindent% +\hspace*{0pt}strict{\char95}dequeue ::~forall a.~Queue a -> (a,~Queue a);\\ +\hspace*{0pt}strict{\char95}dequeue (AQueue xs []) =\\ +\hspace*{0pt} ~let {\char123}\\ +\hspace*{0pt} ~~~(y :~ys) = reverse xs;\\ +\hspace*{0pt} ~{\char125}~in (y,~AQueue [] ys);\\ +\hspace*{0pt}strict{\char95}dequeue (AQueue xs (y :~ys)) = (y,~AQueue xs ys);% +\end{isamarkuptext}% +\isamarkuptrue% +% +\endisatagquote +{\isafoldquote}% +% +\isadelimquote +% +\endisadelimquote +% +\begin{isamarkuptext}% +\noindent In some cases it is desirable to have this + pseudo-\qt{partiality} more explicitly, e.g.~as follows:% +\end{isamarkuptext}% +\isamarkuptrue% +% +\isadelimquote +% +\endisadelimquote +% +\isatagquote +\isacommand{axiomatization}\isamarkupfalse% +\ empty{\isacharunderscore}queue\ {\isacharcolon}{\isacharcolon}\ {\isacharprime}a\isanewline +\isanewline +\isacommand{definition}\isamarkupfalse% +\ strict{\isacharunderscore}dequeue{\isacharprime}\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequoteopen}{\isacharprime}a\ queue\ {\isasymRightarrow}\ {\isacharprime}a\ {\isasymtimes}\ {\isacharprime}a\ queue{\isachardoublequoteclose}\ \isakeyword{where}\isanewline +\ \ {\isachardoublequoteopen}strict{\isacharunderscore}dequeue{\isacharprime}\ q\ {\isacharequal}\ {\isacharparenleft}case\ dequeue\ q\ of\ {\isacharparenleft}Some\ x{\isacharcomma}\ q{\isacharprime}{\isacharparenright}\ {\isasymRightarrow}\ {\isacharparenleft}x{\isacharcomma}\ q{\isacharprime}{\isacharparenright}\ {\isacharbar}\ {\isacharunderscore}\ {\isasymRightarrow}\ empty{\isacharunderscore}queue{\isacharparenright}{\isachardoublequoteclose}\isanewline +\isanewline +\isacommand{lemma}\isamarkupfalse% +\ strict{\isacharunderscore}dequeue{\isacharprime}{\isacharunderscore}AQueue\ {\isacharbrackleft}code{\isacharbrackright}{\isacharcolon}\isanewline +\ \ {\isachardoublequoteopen}strict{\isacharunderscore}dequeue{\isacharprime}\ {\isacharparenleft}AQueue\ xs\ {\isacharbrackleft}{\isacharbrackright}{\isacharparenright}\ {\isacharequal}\ {\isacharparenleft}if\ xs\ {\isacharequal}\ {\isacharbrackleft}{\isacharbrackright}\ then\ empty{\isacharunderscore}queue\isanewline +\ \ \ \ \ else\ strict{\isacharunderscore}dequeue{\isacharprime}\ {\isacharparenleft}AQueue\ {\isacharbrackleft}{\isacharbrackright}\ {\isacharparenleft}rev\ xs{\isacharparenright}{\isacharparenright}{\isacharparenright}{\isachardoublequoteclose}\isanewline +\ \ {\isachardoublequoteopen}strict{\isacharunderscore}dequeue{\isacharprime}\ {\isacharparenleft}AQueue\ xs\ {\isacharparenleft}y\ {\isacharhash}\ ys{\isacharparenright}{\isacharparenright}\ {\isacharequal}\isanewline +\ \ \ \ \ {\isacharparenleft}y{\isacharcomma}\ AQueue\ xs\ ys{\isacharparenright}{\isachardoublequoteclose}\isanewline +\ \ \isacommand{by}\isamarkupfalse% +\ {\isacharparenleft}simp{\isacharunderscore}all\ add{\isacharcolon}\ strict{\isacharunderscore}dequeue{\isacharprime}{\isacharunderscore}def\ dequeue{\isacharunderscore}AQueue\ split{\isacharcolon}\ list{\isachardot}splits{\isacharparenright}% +\endisatagquote +{\isafoldquote}% +% +\isadelimquote +% +\endisadelimquote +% +\begin{isamarkuptext}% +Observe that on the right hand side of the definition of \isa{strict{\isacharunderscore}dequeue{\isacharprime}}, the unspecified constant \isa{empty{\isacharunderscore}queue} occurs. + + Normally, if constants without any code equations occur in a + program, the code generator complains (since in most cases this is + indeed an error). But such constants can also be thought + of as function definitions which always fail, + since there is never a successful pattern match on the left hand + side. In order to categorise a constant into that category + explicitly, use \hyperlink{command.code-abort}{\mbox{\isa{\isacommand{code{\isacharunderscore}abort}}}}:% +\end{isamarkuptext}% +\isamarkuptrue% +% +\isadelimquote +% +\endisadelimquote +% +\isatagquote +\isacommand{code{\isacharunderscore}abort}\isamarkupfalse% +\ empty{\isacharunderscore}queue% +\endisatagquote +{\isafoldquote}% +% +\isadelimquote +% +\endisadelimquote +% +\begin{isamarkuptext}% +\noindent Then the code generator will just insert an error or + exception at the appropriate position:% +\end{isamarkuptext}% +\isamarkuptrue% +% +\isadelimquote +% +\endisadelimquote +% +\isatagquote +% +\begin{isamarkuptext}% +\isatypewriter% +\noindent% +\hspace*{0pt}empty{\char95}queue ::~forall a.~a;\\ +\hspace*{0pt}empty{\char95}queue = error {\char34}empty{\char95}queue{\char34};\\ +\hspace*{0pt}\\ +\hspace*{0pt}strict{\char95}dequeue ::~forall a.~Queue a -> (a,~Queue a);\\ +\hspace*{0pt}strict{\char95}dequeue (AQueue xs (y :~ys)) = (y,~AQueue xs ys);\\ +\hspace*{0pt}strict{\char95}dequeue (AQueue xs []) =\\ +\hspace*{0pt} ~(if null xs then empty{\char95}queue\\ +\hspace*{0pt} ~~~else strict{\char95}dequeue (AQueue [] (reverse xs)));% +\end{isamarkuptext}% +\isamarkuptrue% +% +\endisatagquote +{\isafoldquote}% +% +\isadelimquote +% +\endisadelimquote +% +\begin{isamarkuptext}% +\noindent This feature however is rarely needed in practice. + Note also that the \isa{HOL} default setup already declares + \isa{undefined} as \hyperlink{command.code-abort}{\mbox{\isa{\isacommand{code{\isacharunderscore}abort}}}}, which is most + likely to be used in such situations.% +\end{isamarkuptext}% +\isamarkuptrue% +% +\isadelimtheory +% +\endisadelimtheory +% +\isatagtheory +\isacommand{end}\isamarkupfalse% +% +\endisatagtheory +{\isafoldtheory}% +% +\isadelimtheory +% +\endisadelimtheory +\isanewline +\end{isabellebody}% +%%% Local Variables: +%%% mode: latex +%%% TeX-master: "root" +%%% End: diff -r 7eb0f6991e25 -r 001f2f44984c doc-src/Codegen/Thy/document/Further.tex --- a/doc-src/Codegen/Thy/document/Further.tex Sat Aug 14 12:01:50 2010 +0200 +++ b/doc-src/Codegen/Thy/document/Further.tex Sat Aug 14 13:24:06 2010 +0200 @@ -389,6 +389,179 @@ \end{isamarkuptext}% \isamarkuptrue% % +\isamarkupsubsection{ML system interfaces \label{sec:ml}% +} +\isamarkuptrue% +% +\begin{isamarkuptext}% +Since the code generator framework not only aims to provide + a nice Isar interface but also to form a base for + code-generation-based applications, here a short + description of the most important ML interfaces.% +\end{isamarkuptext}% +\isamarkuptrue% +% +\isamarkupsubsubsection{Managing executable content% +} +\isamarkuptrue% +% +\isadelimmlref +% +\endisadelimmlref +% +\isatagmlref +% +\begin{isamarkuptext}% +\begin{mldecls} + \indexdef{}{ML}{Code.add\_eqn}\verb|Code.add_eqn: thm -> theory -> theory| \\ + \indexdef{}{ML}{Code.del\_eqn}\verb|Code.del_eqn: thm -> theory -> theory| \\ + \indexdef{}{ML}{Code\_Preproc.map\_pre}\verb|Code_Preproc.map_pre: (simpset -> simpset) -> theory -> theory| \\ + \indexdef{}{ML}{Code\_Preproc.map\_post}\verb|Code_Preproc.map_post: (simpset -> simpset) -> theory -> theory| \\ + \indexdef{}{ML}{Code\_Preproc.add\_functrans}\verb|Code_Preproc.add_functrans: string * (theory -> (thm * bool) list -> (thm * bool) list option)|\isasep\isanewline% +\verb| -> theory -> theory| \\ + \indexdef{}{ML}{Code\_Preproc.del\_functrans}\verb|Code_Preproc.del_functrans: string -> theory -> theory| \\ + \indexdef{}{ML}{Code.add\_datatype}\verb|Code.add_datatype: (string * typ) list -> theory -> theory| \\ + \indexdef{}{ML}{Code.get\_type}\verb|Code.get_type: theory -> string|\isasep\isanewline% +\verb| -> (string * sort) list * ((string * string list) * typ list) list| \\ + \indexdef{}{ML}{Code.get\_type\_of\_constr\_or\_abstr}\verb|Code.get_type_of_constr_or_abstr: theory -> string -> (string * bool) option| + \end{mldecls} + + \begin{description} + + \item \verb|Code.add_eqn|~\isa{thm}~\isa{thy} adds function + theorem \isa{thm} to executable content. + + \item \verb|Code.del_eqn|~\isa{thm}~\isa{thy} removes function + theorem \isa{thm} from executable content, if present. + + \item \verb|Code_Preproc.map_pre|~\isa{f}~\isa{thy} changes + the preprocessor simpset. + + \item \verb|Code_Preproc.add_functrans|~\isa{{\isacharparenleft}name{\isacharcomma}\ f{\isacharparenright}}~\isa{thy} adds + function transformer \isa{f} (named \isa{name}) to executable content; + \isa{f} is a transformer of the code equations belonging + to a certain function definition, depending on the + current theory context. Returning \isa{NONE} indicates that no + transformation took place; otherwise, the whole process will be iterated + with the new code equations. + + \item \verb|Code_Preproc.del_functrans|~\isa{name}~\isa{thy} removes + function transformer named \isa{name} from executable content. + + \item \verb|Code.add_datatype|~\isa{cs}~\isa{thy} adds + a datatype to executable content, with generation + set \isa{cs}. + + \item \verb|Code.get_type_of_constr_or_abstr|~\isa{thy}~\isa{const} + returns type constructor corresponding to + constructor \isa{const}; returns \isa{NONE} + if \isa{const} is no constructor. + + \end{description}% +\end{isamarkuptext}% +\isamarkuptrue% +% +\endisatagmlref +{\isafoldmlref}% +% +\isadelimmlref +% +\endisadelimmlref +% +\isamarkupsubsubsection{Auxiliary% +} +\isamarkuptrue% +% +\isadelimmlref +% +\endisadelimmlref +% +\isatagmlref +% +\begin{isamarkuptext}% +\begin{mldecls} + \indexdef{}{ML}{Code.read\_const}\verb|Code.read_const: theory -> string -> string| + \end{mldecls} + + \begin{description} + + \item \verb|Code.read_const|~\isa{thy}~\isa{s} + reads a constant as a concrete term expression \isa{s}. + + \end{description}% +\end{isamarkuptext}% +\isamarkuptrue% +% +\endisatagmlref +{\isafoldmlref}% +% +\isadelimmlref +% +\endisadelimmlref +% +\isamarkupsubsubsection{Data depending on the theory's executable content% +} +\isamarkuptrue% +% +\begin{isamarkuptext}% +Implementing code generator applications on top + of the framework set out so far usually not only + involves using those primitive interfaces + but also storing code-dependent data and various + other things. + + Due to incrementality of code generation, changes in the + theory's executable content have to be propagated in a + certain fashion. Additionally, such changes may occur + not only during theory extension but also during theory + merge, which is a little bit nasty from an implementation + point of view. The framework provides a solution + to this technical challenge by providing a functorial + data slot \verb|Code_Data|; on instantiation + of this functor, the following types and operations + are required: + + \medskip + \begin{tabular}{l} + \isa{type\ T} \\ + \isa{val\ empty{\isacharcolon}\ T} \\ + \end{tabular} + + \begin{description} + + \item \isa{T} the type of data to store. + + \item \isa{empty} initial (empty) data. + + \end{description} + + \noindent An instance of \verb|Code_Data| provides the following + interface: + + \medskip + \begin{tabular}{l} + \isa{change{\isacharcolon}\ theory\ {\isasymrightarrow}\ {\isacharparenleft}T\ {\isasymrightarrow}\ T{\isacharparenright}\ {\isasymrightarrow}\ T} \\ + \isa{change{\isacharunderscore}yield{\isacharcolon}\ theory\ {\isasymrightarrow}\ {\isacharparenleft}T\ {\isasymrightarrow}\ {\isacharprime}a\ {\isacharasterisk}\ T{\isacharparenright}\ {\isasymrightarrow}\ {\isacharprime}a\ {\isacharasterisk}\ T} + \end{tabular} + + \begin{description} + + \item \isa{change} update of current data (cached!) + by giving a continuation. + + \item \isa{change{\isacharunderscore}yield} update with side result. + + \end{description}% +\end{isamarkuptext}% +\isamarkuptrue% +% +\begin{isamarkuptext}% +\bigskip + + \emph{Happy proving, happy hacking!}% +\end{isamarkuptext}% +\isamarkuptrue% +% \isadelimtheory % \endisadelimtheory diff -r 7eb0f6991e25 -r 001f2f44984c doc-src/Codegen/Thy/document/Inductive_Predicate.tex --- a/doc-src/Codegen/Thy/document/Inductive_Predicate.tex Sat Aug 14 12:01:50 2010 +0200 +++ b/doc-src/Codegen/Thy/document/Inductive_Predicate.tex Sat Aug 14 13:24:06 2010 +0200 @@ -18,7 +18,7 @@ % \endisadelimtheory % -\isamarkupsubsection{Inductive Predicates% +\isamarkupsection{Inductive Predicates% } \isamarkuptrue% % diff -r 7eb0f6991e25 -r 001f2f44984c doc-src/Codegen/Thy/document/Introduction.tex --- a/doc-src/Codegen/Thy/document/Introduction.tex Sat Aug 14 12:01:50 2010 +0200 +++ b/doc-src/Codegen/Thy/document/Introduction.tex Sat Aug 14 13:24:06 2010 +0200 @@ -18,7 +18,27 @@ % \endisadelimtheory % -\isamarkupsection{Introduction and Overview% +\isamarkupsection{Introduction% +} +\isamarkuptrue% +% +\isamarkupsubsection{Code generation fundamental: shallow embedding% +} +\isamarkuptrue% +% +\isamarkupsubsection{A quick start with the \isa{Isabelle{\isacharslash}HOL} toolbox% +} +\isamarkuptrue% +% +\isamarkupsubsection{Type classes% +} +\isamarkuptrue% +% +\isamarkupsubsection{How to continue from here% +} +\isamarkuptrue% +% +\isamarkupsubsection{If something goes utterly wrong% } \isamarkuptrue% % @@ -263,6 +283,32 @@ \end{isamarkuptext}% \isamarkuptrue% % +\isamarkupsubsection{If something utterly fails% +} +\isamarkuptrue% +% +\begin{isamarkuptext}% +Under certain circumstances, the code generator fails to produce + code entirely. + + \begin{description} + + \ditem{generate only one module} + + \ditem{check with a different target language} + + \ditem{inspect code equations} + + \ditem{inspect preprocessor setup} + + \ditem{generate exceptions} + + \ditem{remove offending code equations} + + \end{description}% +\end{isamarkuptext}% +\isamarkuptrue% +% \isamarkupsubsection{Code generator architecture \label{sec:concept}% } \isamarkuptrue% diff -r 7eb0f6991e25 -r 001f2f44984c doc-src/Codegen/Thy/document/ML.tex --- a/doc-src/Codegen/Thy/document/ML.tex Sat Aug 14 12:01:50 2010 +0200 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,240 +0,0 @@ -% -\begin{isabellebody}% -\def\isabellecontext{ML}% -% -\isadelimtheory -% -\endisadelimtheory -% -\isatagtheory -\isacommand{theory}\isamarkupfalse% -\ {\isachardoublequoteopen}ML{\isachardoublequoteclose}\isanewline -\isakeyword{imports}\ Setup\isanewline -\isakeyword{begin}% -\endisatagtheory -{\isafoldtheory}% -% -\isadelimtheory -% -\endisadelimtheory -% -\isamarkupsection{ML system interfaces \label{sec:ml}% -} -\isamarkuptrue% -% -\begin{isamarkuptext}% -Since the code generator framework not only aims to provide - a nice Isar interface but also to form a base for - code-generation-based applications, here a short - description of the most important ML interfaces.% -\end{isamarkuptext}% -\isamarkuptrue% -% -\isamarkupsubsection{Executable theory content: \isa{Code}% -} -\isamarkuptrue% -% -\begin{isamarkuptext}% -This Pure module implements the core notions of - executable content of a theory.% -\end{isamarkuptext}% -\isamarkuptrue% -% -\isamarkupsubsubsection{Managing executable content% -} -\isamarkuptrue% -% -\isadelimmlref -% -\endisadelimmlref -% -\isatagmlref -% -\begin{isamarkuptext}% -\begin{mldecls} - \indexdef{}{ML}{Code.add\_eqn}\verb|Code.add_eqn: thm -> theory -> theory| \\ - \indexdef{}{ML}{Code.del\_eqn}\verb|Code.del_eqn: thm -> theory -> theory| \\ - \indexdef{}{ML}{Code\_Preproc.map\_pre}\verb|Code_Preproc.map_pre: (simpset -> simpset) -> theory -> theory| \\ - \indexdef{}{ML}{Code\_Preproc.map\_post}\verb|Code_Preproc.map_post: (simpset -> simpset) -> theory -> theory| \\ - \indexdef{}{ML}{Code\_Preproc.add\_functrans}\verb|Code_Preproc.add_functrans: string * (theory -> (thm * bool) list -> (thm * bool) list option)|\isasep\isanewline% -\verb| -> theory -> theory| \\ - \indexdef{}{ML}{Code\_Preproc.del\_functrans}\verb|Code_Preproc.del_functrans: string -> theory -> theory| \\ - \indexdef{}{ML}{Code.add\_datatype}\verb|Code.add_datatype: (string * typ) list -> theory -> theory| \\ - \indexdef{}{ML}{Code.get\_type}\verb|Code.get_type: theory -> string|\isasep\isanewline% -\verb| -> (string * sort) list * ((string * string list) * typ list) list| \\ - \indexdef{}{ML}{Code.get\_type\_of\_constr\_or\_abstr}\verb|Code.get_type_of_constr_or_abstr: theory -> string -> (string * bool) option| - \end{mldecls} - - \begin{description} - - \item \verb|Code.add_eqn|~\isa{thm}~\isa{thy} adds function - theorem \isa{thm} to executable content. - - \item \verb|Code.del_eqn|~\isa{thm}~\isa{thy} removes function - theorem \isa{thm} from executable content, if present. - - \item \verb|Code_Preproc.map_pre|~\isa{f}~\isa{thy} changes - the preprocessor simpset. - - \item \verb|Code_Preproc.add_functrans|~\isa{{\isacharparenleft}name{\isacharcomma}\ f{\isacharparenright}}~\isa{thy} adds - function transformer \isa{f} (named \isa{name}) to executable content; - \isa{f} is a transformer of the code equations belonging - to a certain function definition, depending on the - current theory context. Returning \isa{NONE} indicates that no - transformation took place; otherwise, the whole process will be iterated - with the new code equations. - - \item \verb|Code_Preproc.del_functrans|~\isa{name}~\isa{thy} removes - function transformer named \isa{name} from executable content. - - \item \verb|Code.add_datatype|~\isa{cs}~\isa{thy} adds - a datatype to executable content, with generation - set \isa{cs}. - - \item \verb|Code.get_type_of_constr_or_abstr|~\isa{thy}~\isa{const} - returns type constructor corresponding to - constructor \isa{const}; returns \isa{NONE} - if \isa{const} is no constructor. - - \end{description}% -\end{isamarkuptext}% -\isamarkuptrue% -% -\endisatagmlref -{\isafoldmlref}% -% -\isadelimmlref -% -\endisadelimmlref -% -\isamarkupsubsection{Auxiliary% -} -\isamarkuptrue% -% -\isadelimmlref -% -\endisadelimmlref -% -\isatagmlref -% -\begin{isamarkuptext}% -\begin{mldecls} - \indexdef{}{ML}{Code.read\_const}\verb|Code.read_const: theory -> string -> string| - \end{mldecls} - - \begin{description} - - \item \verb|Code.read_const|~\isa{thy}~\isa{s} - reads a constant as a concrete term expression \isa{s}. - - \end{description}% -\end{isamarkuptext}% -\isamarkuptrue% -% -\endisatagmlref -{\isafoldmlref}% -% -\isadelimmlref -% -\endisadelimmlref -% -\isamarkupsubsection{Implementing code generator applications% -} -\isamarkuptrue% -% -\begin{isamarkuptext}% -Implementing code generator applications on top - of the framework set out so far usually not only - involves using those primitive interfaces - but also storing code-dependent data and various - other things.% -\end{isamarkuptext}% -\isamarkuptrue% -% -\isamarkupsubsubsection{Data depending on the theory's executable content% -} -\isamarkuptrue% -% -\begin{isamarkuptext}% -Due to incrementality of code generation, changes in the - theory's executable content have to be propagated in a - certain fashion. Additionally, such changes may occur - not only during theory extension but also during theory - merge, which is a little bit nasty from an implementation - point of view. The framework provides a solution - to this technical challenge by providing a functorial - data slot \verb|Code_Data|; on instantiation - of this functor, the following types and operations - are required: - - \medskip - \begin{tabular}{l} - \isa{type\ T} \\ - \isa{val\ empty{\isacharcolon}\ T} \\ - \isa{val\ purge{\isacharcolon}\ theory\ {\isasymrightarrow}\ string\ list\ option\ {\isasymrightarrow}\ T\ {\isasymrightarrow}\ T} - \end{tabular} - - \begin{description} - - \item \isa{T} the type of data to store. - - \item \isa{empty} initial (empty) data. - - \item \isa{purge}~\isa{thy}~\isa{consts} propagates changes in executable content; - \isa{consts} indicates the kind - of change: \verb|NONE| stands for a fundamental change - which invalidates any existing code, \isa{SOME\ consts} - hints that executable content for constants \isa{consts} - has changed. - - \end{description} - - \noindent An instance of \verb|Code_Data| provides the following - interface: - - \medskip - \begin{tabular}{l} - \isa{get{\isacharcolon}\ theory\ {\isasymrightarrow}\ T} \\ - \isa{change{\isacharcolon}\ theory\ {\isasymrightarrow}\ {\isacharparenleft}T\ {\isasymrightarrow}\ T{\isacharparenright}\ {\isasymrightarrow}\ T} \\ - \isa{change{\isacharunderscore}yield{\isacharcolon}\ theory\ {\isasymrightarrow}\ {\isacharparenleft}T\ {\isasymrightarrow}\ {\isacharprime}a\ {\isacharasterisk}\ T{\isacharparenright}\ {\isasymrightarrow}\ {\isacharprime}a\ {\isacharasterisk}\ T} - \end{tabular} - - \begin{description} - - \item \isa{get} retrieval of the current data. - - \item \isa{change} update of current data (cached!) - by giving a continuation. - - \item \isa{change{\isacharunderscore}yield} update with side result. - - \end{description}% -\end{isamarkuptext}% -\isamarkuptrue% -% -\begin{isamarkuptext}% -\bigskip - - \emph{Happy proving, happy hacking!}% -\end{isamarkuptext}% -\isamarkuptrue% -% -\isadelimtheory -% -\endisadelimtheory -% -\isatagtheory -\isacommand{end}\isamarkupfalse% -% -\endisatagtheory -{\isafoldtheory}% -% -\isadelimtheory -% -\endisadelimtheory -\isanewline -\end{isabellebody}% -%%% Local Variables: -%%% mode: latex -%%% TeX-master: "root" -%%% End: diff -r 7eb0f6991e25 -r 001f2f44984c doc-src/Codegen/Thy/document/Program.tex --- a/doc-src/Codegen/Thy/document/Program.tex Sat Aug 14 12:01:50 2010 +0200 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,1013 +0,0 @@ -% -\begin{isabellebody}% -\def\isabellecontext{Program}% -% -\isadelimtheory -% -\endisadelimtheory -% -\isatagtheory -\isacommand{theory}\isamarkupfalse% -\ Program\isanewline -\isakeyword{imports}\ Introduction\isanewline -\isakeyword{begin}% -\endisatagtheory -{\isafoldtheory}% -% -\isadelimtheory -% -\endisadelimtheory -% -\isamarkupsection{Turning Theories into Programs \label{sec:program}% -} -\isamarkuptrue% -% -\isamarkupsubsection{The \isa{Isabelle{\isacharslash}HOL} default setup% -} -\isamarkuptrue% -% -\begin{isamarkuptext}% -We have already seen how by default equations stemming from - \hyperlink{command.definition}{\mbox{\isa{\isacommand{definition}}}}, \hyperlink{command.primrec}{\mbox{\isa{\isacommand{primrec}}}} and \hyperlink{command.fun}{\mbox{\isa{\isacommand{fun}}}} - statements are used for code generation. This default behaviour - can be changed, e.g.\ by providing different code equations. - The customisations shown in this section are \emph{safe} - as regards correctness: all programs that can be generated are partially - correct.% -\end{isamarkuptext}% -\isamarkuptrue% -% -\isamarkupsubsection{Selecting code equations% -} -\isamarkuptrue% -% -\begin{isamarkuptext}% -Coming back to our introductory example, we - could provide an alternative code equations for \isa{dequeue} - explicitly:% -\end{isamarkuptext}% -\isamarkuptrue% -% -\isadelimquote -% -\endisadelimquote -% -\isatagquote -\isacommand{lemma}\isamarkupfalse% -\ {\isacharbrackleft}code{\isacharbrackright}{\isacharcolon}\isanewline -\ \ {\isachardoublequoteopen}dequeue\ {\isacharparenleft}AQueue\ xs\ {\isacharbrackleft}{\isacharbrackright}{\isacharparenright}\ {\isacharequal}\isanewline -\ \ \ \ \ {\isacharparenleft}if\ xs\ {\isacharequal}\ {\isacharbrackleft}{\isacharbrackright}\ then\ {\isacharparenleft}None{\isacharcomma}\ AQueue\ {\isacharbrackleft}{\isacharbrackright}\ {\isacharbrackleft}{\isacharbrackright}{\isacharparenright}\isanewline -\ \ \ \ \ \ \ else\ dequeue\ {\isacharparenleft}AQueue\ {\isacharbrackleft}{\isacharbrackright}\ {\isacharparenleft}rev\ xs{\isacharparenright}{\isacharparenright}{\isacharparenright}{\isachardoublequoteclose}\isanewline -\ \ {\isachardoublequoteopen}dequeue\ {\isacharparenleft}AQueue\ xs\ {\isacharparenleft}y\ {\isacharhash}\ ys{\isacharparenright}{\isacharparenright}\ {\isacharequal}\isanewline -\ \ \ \ \ {\isacharparenleft}Some\ y{\isacharcomma}\ AQueue\ xs\ ys{\isacharparenright}{\isachardoublequoteclose}\isanewline -\ \ \isacommand{by}\isamarkupfalse% -\ {\isacharparenleft}cases\ xs{\isacharcomma}\ simp{\isacharunderscore}all{\isacharparenright}\ {\isacharparenleft}cases\ {\isachardoublequoteopen}rev\ xs{\isachardoublequoteclose}{\isacharcomma}\ simp{\isacharunderscore}all{\isacharparenright}% -\endisatagquote -{\isafoldquote}% -% -\isadelimquote -% -\endisadelimquote -% -\begin{isamarkuptext}% -\noindent The annotation \isa{{\isacharbrackleft}code{\isacharbrackright}} is an \isa{Isar} - \isa{attribute} which states that the given theorems should be - considered as code equations for a \isa{fun} statement -- - the corresponding constant is determined syntactically. The resulting code:% -\end{isamarkuptext}% -\isamarkuptrue% -% -\isadelimquote -% -\endisadelimquote -% -\isatagquote -% -\begin{isamarkuptext}% -\isatypewriter% -\noindent% -\hspace*{0pt}dequeue ::~forall a.~Queue a -> (Maybe a,~Queue a);\\ -\hspace*{0pt}dequeue (AQueue xs (y :~ys)) = (Just y,~AQueue xs ys);\\ -\hspace*{0pt}dequeue (AQueue xs []) =\\ -\hspace*{0pt} ~(if null xs then (Nothing,~AQueue [] [])\\ -\hspace*{0pt} ~~~else dequeue (AQueue [] (reverse xs)));% -\end{isamarkuptext}% -\isamarkuptrue% -% -\endisatagquote -{\isafoldquote}% -% -\isadelimquote -% -\endisadelimquote -% -\begin{isamarkuptext}% -\noindent You may note that the equality test \isa{xs\ {\isacharequal}\ {\isacharbrackleft}{\isacharbrackright}} has been - replaced by the predicate \isa{null\ xs}. This is due to the default - setup in the \qn{preprocessor} to be discussed further below (\secref{sec:preproc}). - - Changing the default constructor set of datatypes is also - possible. See \secref{sec:datatypes} for an example. - - As told in \secref{sec:concept}, code generation is based - on a structured collection of code theorems. - This collection - may be inspected using the \hyperlink{command.code-thms}{\mbox{\isa{\isacommand{code{\isacharunderscore}thms}}}} command:% -\end{isamarkuptext}% -\isamarkuptrue% -% -\isadelimquote -% -\endisadelimquote -% -\isatagquote -\isacommand{code{\isacharunderscore}thms}\isamarkupfalse% -\ dequeue% -\endisatagquote -{\isafoldquote}% -% -\isadelimquote -% -\endisadelimquote -% -\begin{isamarkuptext}% -\noindent prints a table with \emph{all} code equations - for \isa{dequeue}, including - \emph{all} code equations those equations depend - on recursively. - - Similarly, the \hyperlink{command.code-deps}{\mbox{\isa{\isacommand{code{\isacharunderscore}deps}}}} command shows a graph - visualising dependencies between code equations.% -\end{isamarkuptext}% -\isamarkuptrue% -% -\isamarkupsubsection{\isa{class} and \isa{instantiation}% -} -\isamarkuptrue% -% -\begin{isamarkuptext}% -Concerning type classes and code generation, let us examine an example - from abstract algebra:% -\end{isamarkuptext}% -\isamarkuptrue% -% -\isadelimquote -% -\endisadelimquote -% -\isatagquote -\isacommand{class}\isamarkupfalse% -\ semigroup\ {\isacharequal}\isanewline -\ \ \isakeyword{fixes}\ mult\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequoteopen}{\isacharprime}a\ {\isasymRightarrow}\ {\isacharprime}a\ {\isasymRightarrow}\ {\isacharprime}a{\isachardoublequoteclose}\ {\isacharparenleft}\isakeyword{infixl}\ {\isachardoublequoteopen}{\isasymotimes}{\isachardoublequoteclose}\ {\isadigit{7}}{\isadigit{0}}{\isacharparenright}\isanewline -\ \ \isakeyword{assumes}\ assoc{\isacharcolon}\ {\isachardoublequoteopen}{\isacharparenleft}x\ {\isasymotimes}\ y{\isacharparenright}\ {\isasymotimes}\ z\ {\isacharequal}\ x\ {\isasymotimes}\ {\isacharparenleft}y\ {\isasymotimes}\ z{\isacharparenright}{\isachardoublequoteclose}\isanewline -\isanewline -\isacommand{class}\isamarkupfalse% -\ monoid\ {\isacharequal}\ semigroup\ {\isacharplus}\isanewline -\ \ \isakeyword{fixes}\ neutral\ {\isacharcolon}{\isacharcolon}\ {\isacharprime}a\ {\isacharparenleft}{\isachardoublequoteopen}{\isasymone}{\isachardoublequoteclose}{\isacharparenright}\isanewline -\ \ \isakeyword{assumes}\ neutl{\isacharcolon}\ {\isachardoublequoteopen}{\isasymone}\ {\isasymotimes}\ x\ {\isacharequal}\ x{\isachardoublequoteclose}\isanewline -\ \ \ \ \isakeyword{and}\ neutr{\isacharcolon}\ {\isachardoublequoteopen}x\ {\isasymotimes}\ {\isasymone}\ {\isacharequal}\ x{\isachardoublequoteclose}\isanewline -\isanewline -\isacommand{instantiation}\isamarkupfalse% -\ nat\ {\isacharcolon}{\isacharcolon}\ monoid\isanewline -\isakeyword{begin}\isanewline -\isanewline -\isacommand{primrec}\isamarkupfalse% -\ mult{\isacharunderscore}nat\ \isakeyword{where}\isanewline -\ \ \ \ {\isachardoublequoteopen}{\isadigit{0}}\ {\isasymotimes}\ n\ {\isacharequal}\ {\isacharparenleft}{\isadigit{0}}{\isasymColon}nat{\isacharparenright}{\isachardoublequoteclose}\isanewline -\ \ {\isacharbar}\ {\isachardoublequoteopen}Suc\ m\ {\isasymotimes}\ n\ {\isacharequal}\ n\ {\isacharplus}\ m\ {\isasymotimes}\ n{\isachardoublequoteclose}\isanewline -\isanewline -\isacommand{definition}\isamarkupfalse% -\ neutral{\isacharunderscore}nat\ \isakeyword{where}\isanewline -\ \ {\isachardoublequoteopen}{\isasymone}\ {\isacharequal}\ Suc\ {\isadigit{0}}{\isachardoublequoteclose}\isanewline -\isanewline -\isacommand{lemma}\isamarkupfalse% -\ add{\isacharunderscore}mult{\isacharunderscore}distrib{\isacharcolon}\isanewline -\ \ \isakeyword{fixes}\ n\ m\ q\ {\isacharcolon}{\isacharcolon}\ nat\isanewline -\ \ \isakeyword{shows}\ {\isachardoublequoteopen}{\isacharparenleft}n\ {\isacharplus}\ m{\isacharparenright}\ {\isasymotimes}\ q\ {\isacharequal}\ n\ {\isasymotimes}\ q\ {\isacharplus}\ m\ {\isasymotimes}\ q{\isachardoublequoteclose}\isanewline -\ \ \isacommand{by}\isamarkupfalse% -\ {\isacharparenleft}induct\ n{\isacharparenright}\ simp{\isacharunderscore}all\isanewline -\isanewline -\isacommand{instance}\isamarkupfalse% -\ \isacommand{proof}\isamarkupfalse% -\isanewline -\ \ \isacommand{fix}\isamarkupfalse% -\ m\ n\ q\ {\isacharcolon}{\isacharcolon}\ nat\isanewline -\ \ \isacommand{show}\isamarkupfalse% -\ {\isachardoublequoteopen}m\ {\isasymotimes}\ n\ {\isasymotimes}\ q\ {\isacharequal}\ m\ {\isasymotimes}\ {\isacharparenleft}n\ {\isasymotimes}\ q{\isacharparenright}{\isachardoublequoteclose}\isanewline -\ \ \ \ \isacommand{by}\isamarkupfalse% -\ {\isacharparenleft}induct\ m{\isacharparenright}\ {\isacharparenleft}simp{\isacharunderscore}all\ add{\isacharcolon}\ add{\isacharunderscore}mult{\isacharunderscore}distrib{\isacharparenright}\isanewline -\ \ \isacommand{show}\isamarkupfalse% -\ {\isachardoublequoteopen}{\isasymone}\ {\isasymotimes}\ n\ {\isacharequal}\ n{\isachardoublequoteclose}\isanewline -\ \ \ \ \isacommand{by}\isamarkupfalse% -\ {\isacharparenleft}simp\ add{\isacharcolon}\ neutral{\isacharunderscore}nat{\isacharunderscore}def{\isacharparenright}\isanewline -\ \ \isacommand{show}\isamarkupfalse% -\ {\isachardoublequoteopen}m\ {\isasymotimes}\ {\isasymone}\ {\isacharequal}\ m{\isachardoublequoteclose}\isanewline -\ \ \ \ \isacommand{by}\isamarkupfalse% -\ {\isacharparenleft}induct\ m{\isacharparenright}\ {\isacharparenleft}simp{\isacharunderscore}all\ add{\isacharcolon}\ neutral{\isacharunderscore}nat{\isacharunderscore}def{\isacharparenright}\isanewline -\isacommand{qed}\isamarkupfalse% -\isanewline -\isanewline -\isacommand{end}\isamarkupfalse% -% -\endisatagquote -{\isafoldquote}% -% -\isadelimquote -% -\endisadelimquote -% -\begin{isamarkuptext}% -\noindent We define the natural operation of the natural numbers - on monoids:% -\end{isamarkuptext}% -\isamarkuptrue% -% -\isadelimquote -% -\endisadelimquote -% -\isatagquote -\isacommand{primrec}\isamarkupfalse% -\ {\isacharparenleft}\isakeyword{in}\ monoid{\isacharparenright}\ pow\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequoteopen}nat\ {\isasymRightarrow}\ {\isacharprime}a\ {\isasymRightarrow}\ {\isacharprime}a{\isachardoublequoteclose}\ \isakeyword{where}\isanewline -\ \ \ \ {\isachardoublequoteopen}pow\ {\isadigit{0}}\ a\ {\isacharequal}\ {\isasymone}{\isachardoublequoteclose}\isanewline -\ \ {\isacharbar}\ {\isachardoublequoteopen}pow\ {\isacharparenleft}Suc\ n{\isacharparenright}\ a\ {\isacharequal}\ a\ {\isasymotimes}\ pow\ n\ a{\isachardoublequoteclose}% -\endisatagquote -{\isafoldquote}% -% -\isadelimquote -% -\endisadelimquote -% -\begin{isamarkuptext}% -\noindent This we use to define the discrete exponentiation function:% -\end{isamarkuptext}% -\isamarkuptrue% -% -\isadelimquote -% -\endisadelimquote -% -\isatagquote -\isacommand{definition}\isamarkupfalse% -\ bexp\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequoteopen}nat\ {\isasymRightarrow}\ nat{\isachardoublequoteclose}\ \isakeyword{where}\isanewline -\ \ {\isachardoublequoteopen}bexp\ n\ {\isacharequal}\ pow\ n\ {\isacharparenleft}Suc\ {\isacharparenleft}Suc\ {\isadigit{0}}{\isacharparenright}{\isacharparenright}{\isachardoublequoteclose}% -\endisatagquote -{\isafoldquote}% -% -\isadelimquote -% -\endisadelimquote -% -\begin{isamarkuptext}% -\noindent The corresponding code in Haskell uses that language's native classes:% -\end{isamarkuptext}% -\isamarkuptrue% -% -\isadelimquote -% -\endisadelimquote -% -\isatagquote -% -\begin{isamarkuptext}% -\isatypewriter% -\noindent% -\hspace*{0pt}module Example where {\char123}\\ -\hspace*{0pt}\\ -\hspace*{0pt}data Nat = Zero{\char95}nat | Suc Nat;\\ -\hspace*{0pt}\\ -\hspace*{0pt}class Semigroup a where {\char123}\\ -\hspace*{0pt} ~mult ::~a -> a -> a;\\ -\hspace*{0pt}{\char125};\\ -\hspace*{0pt}\\ -\hspace*{0pt}class (Semigroup a) => Monoid a where {\char123}\\ -\hspace*{0pt} ~neutral ::~a;\\ -\hspace*{0pt}{\char125};\\ -\hspace*{0pt}\\ -\hspace*{0pt}pow ::~forall a.~(Monoid a) => Nat -> a -> a;\\ -\hspace*{0pt}pow Zero{\char95}nat a = neutral;\\ -\hspace*{0pt}pow (Suc n) a = mult a (pow n a);\\ -\hspace*{0pt}\\ -\hspace*{0pt}plus{\char95}nat ::~Nat -> Nat -> Nat;\\ -\hspace*{0pt}plus{\char95}nat (Suc m) n = plus{\char95}nat m (Suc n);\\ -\hspace*{0pt}plus{\char95}nat Zero{\char95}nat n = n;\\ -\hspace*{0pt}\\ -\hspace*{0pt}mult{\char95}nat ::~Nat -> Nat -> Nat;\\ -\hspace*{0pt}mult{\char95}nat Zero{\char95}nat n = Zero{\char95}nat;\\ -\hspace*{0pt}mult{\char95}nat (Suc m) n = plus{\char95}nat n (mult{\char95}nat m n);\\ -\hspace*{0pt}\\ -\hspace*{0pt}neutral{\char95}nat ::~Nat;\\ -\hspace*{0pt}neutral{\char95}nat = Suc Zero{\char95}nat;\\ -\hspace*{0pt}\\ -\hspace*{0pt}instance Semigroup Nat where {\char123}\\ -\hspace*{0pt} ~mult = mult{\char95}nat;\\ -\hspace*{0pt}{\char125};\\ -\hspace*{0pt}\\ -\hspace*{0pt}instance Monoid Nat where {\char123}\\ -\hspace*{0pt} ~neutral = neutral{\char95}nat;\\ -\hspace*{0pt}{\char125};\\ -\hspace*{0pt}\\ -\hspace*{0pt}bexp ::~Nat -> Nat;\\ -\hspace*{0pt}bexp n = pow n (Suc (Suc Zero{\char95}nat));\\ -\hspace*{0pt}\\ -\hspace*{0pt}{\char125}% -\end{isamarkuptext}% -\isamarkuptrue% -% -\endisatagquote -{\isafoldquote}% -% -\isadelimquote -% -\endisadelimquote -% -\begin{isamarkuptext}% -\noindent This is a convenient place to show how explicit dictionary construction - manifests in generated code (here, the same example in \isa{SML}) - \cite{Haftmann-Nipkow:2010:code}:% -\end{isamarkuptext}% -\isamarkuptrue% -% -\isadelimquote -% -\endisadelimquote -% -\isatagquote -% -\begin{isamarkuptext}% -\isatypewriter% -\noindent% -\hspace*{0pt}structure Example :~sig\\ -\hspace*{0pt} ~datatype nat = Zero{\char95}nat | Suc of nat\\ -\hspace*{0pt} ~type 'a semigroup\\ -\hspace*{0pt} ~val mult :~'a semigroup -> 'a -> 'a -> 'a\\ -\hspace*{0pt} ~type 'a monoid\\ -\hspace*{0pt} ~val semigroup{\char95}monoid :~'a monoid -> 'a semigroup\\ -\hspace*{0pt} ~val neutral :~'a monoid -> 'a\\ -\hspace*{0pt} ~val pow :~'a monoid -> nat -> 'a -> 'a\\ -\hspace*{0pt} ~val plus{\char95}nat :~nat -> nat -> nat\\ -\hspace*{0pt} ~val mult{\char95}nat :~nat -> nat -> nat\\ -\hspace*{0pt} ~val neutral{\char95}nat :~nat\\ -\hspace*{0pt} ~val semigroup{\char95}nat :~nat semigroup\\ -\hspace*{0pt} ~val monoid{\char95}nat :~nat monoid\\ -\hspace*{0pt} ~val bexp :~nat -> nat\\ -\hspace*{0pt}end = struct\\ -\hspace*{0pt}\\ -\hspace*{0pt}datatype nat = Zero{\char95}nat | Suc of nat;\\ -\hspace*{0pt}\\ -\hspace*{0pt}type 'a semigroup = {\char123}mult :~'a -> 'a -> 'a{\char125};\\ -\hspace*{0pt}val mult = {\char35}mult :~'a semigroup -> 'a -> 'a -> 'a;\\ -\hspace*{0pt}\\ -\hspace*{0pt}type 'a monoid = {\char123}semigroup{\char95}monoid :~'a semigroup,~neutral :~'a{\char125};\\ -\hspace*{0pt}val semigroup{\char95}monoid = {\char35}semigroup{\char95}monoid :~'a monoid -> 'a semigroup;\\ -\hspace*{0pt}val neutral = {\char35}neutral :~'a monoid -> 'a;\\ -\hspace*{0pt}\\ -\hspace*{0pt}fun pow A{\char95}~Zero{\char95}nat a = neutral A{\char95}\\ -\hspace*{0pt} ~| pow A{\char95}~(Suc n) a = mult (semigroup{\char95}monoid A{\char95}) a (pow A{\char95}~n a);\\ -\hspace*{0pt}\\ -\hspace*{0pt}fun plus{\char95}nat (Suc m) n = plus{\char95}nat m (Suc n)\\ -\hspace*{0pt} ~| plus{\char95}nat Zero{\char95}nat n = n;\\ -\hspace*{0pt}\\ -\hspace*{0pt}fun mult{\char95}nat Zero{\char95}nat n = Zero{\char95}nat\\ -\hspace*{0pt} ~| mult{\char95}nat (Suc m) n = plus{\char95}nat n (mult{\char95}nat m n);\\ -\hspace*{0pt}\\ -\hspace*{0pt}val neutral{\char95}nat :~nat = Suc Zero{\char95}nat;\\ -\hspace*{0pt}\\ -\hspace*{0pt}val semigroup{\char95}nat = {\char123}mult = mult{\char95}nat{\char125}~:~nat semigroup;\\ -\hspace*{0pt}\\ -\hspace*{0pt}val monoid{\char95}nat = {\char123}semigroup{\char95}monoid = semigroup{\char95}nat,~neutral = neutral{\char95}nat{\char125}\\ -\hspace*{0pt} ~:~nat monoid;\\ -\hspace*{0pt}\\ -\hspace*{0pt}fun bexp n = pow monoid{\char95}nat n (Suc (Suc Zero{\char95}nat));\\ -\hspace*{0pt}\\ -\hspace*{0pt}end;~(*struct Example*)% -\end{isamarkuptext}% -\isamarkuptrue% -% -\endisatagquote -{\isafoldquote}% -% -\isadelimquote -% -\endisadelimquote -% -\begin{isamarkuptext}% -\noindent Note the parameters with trailing underscore (\verb|A_|), - which are the dictionary parameters.% -\end{isamarkuptext}% -\isamarkuptrue% -% -\isamarkupsubsection{The preprocessor \label{sec:preproc}% -} -\isamarkuptrue% -% -\begin{isamarkuptext}% -Before selected function theorems are turned into abstract - code, a chain of definitional transformation steps is carried - out: \emph{preprocessing}. In essence, the preprocessor - consists of two components: a \emph{simpset} and \emph{function transformers}. - - The \emph{simpset} can apply the full generality of the - Isabelle simplifier. Due to the interpretation of theorems as code - equations, rewrites are applied to the right hand side and the - arguments of the left hand side of an equation, but never to the - constant heading the left hand side. An important special case are - \emph{unfold theorems}, which may be declared and removed using - the \hyperlink{attribute.code-unfold}{\mbox{\isa{code{\isacharunderscore}unfold}}} or \emph{\hyperlink{attribute.code-unfold}{\mbox{\isa{code{\isacharunderscore}unfold}}} del} - attribute, respectively. - - Some common applications:% -\end{isamarkuptext}% -\isamarkuptrue% -% -\begin{itemize} -% -\begin{isamarkuptext}% -\item replacing non-executable constructs by executable ones:% -\end{isamarkuptext}% -\isamarkuptrue% -% -\isadelimquote -% -\endisadelimquote -% -\isatagquote -\isacommand{lemma}\isamarkupfalse% -\ {\isacharbrackleft}code{\isacharunderscore}unfold{\isacharbrackright}{\isacharcolon}\isanewline -\ \ {\isachardoublequoteopen}x\ {\isasymin}\ set\ xs\ {\isasymlongleftrightarrow}\ List{\isachardot}member\ xs\ x{\isachardoublequoteclose}\ \isacommand{by}\isamarkupfalse% -\ {\isacharparenleft}fact\ in{\isacharunderscore}set{\isacharunderscore}member{\isacharparenright}% -\endisatagquote -{\isafoldquote}% -% -\isadelimquote -% -\endisadelimquote -% -\begin{isamarkuptext}% -\item eliminating superfluous constants:% -\end{isamarkuptext}% -\isamarkuptrue% -% -\isadelimquote -% -\endisadelimquote -% -\isatagquote -\isacommand{lemma}\isamarkupfalse% -\ {\isacharbrackleft}code{\isacharunderscore}unfold{\isacharbrackright}{\isacharcolon}\isanewline -\ \ {\isachardoublequoteopen}{\isadigit{1}}\ {\isacharequal}\ Suc\ {\isadigit{0}}{\isachardoublequoteclose}\ \isacommand{by}\isamarkupfalse% -\ {\isacharparenleft}fact\ One{\isacharunderscore}nat{\isacharunderscore}def{\isacharparenright}% -\endisatagquote -{\isafoldquote}% -% -\isadelimquote -% -\endisadelimquote -% -\begin{isamarkuptext}% -\item replacing executable but inconvenient constructs:% -\end{isamarkuptext}% -\isamarkuptrue% -% -\isadelimquote -% -\endisadelimquote -% -\isatagquote -\isacommand{lemma}\isamarkupfalse% -\ {\isacharbrackleft}code{\isacharunderscore}unfold{\isacharbrackright}{\isacharcolon}\isanewline -\ \ {\isachardoublequoteopen}xs\ {\isacharequal}\ {\isacharbrackleft}{\isacharbrackright}\ {\isasymlongleftrightarrow}\ List{\isachardot}null\ xs{\isachardoublequoteclose}\ \isacommand{by}\isamarkupfalse% -\ {\isacharparenleft}fact\ eq{\isacharunderscore}Nil{\isacharunderscore}null{\isacharparenright}% -\endisatagquote -{\isafoldquote}% -% -\isadelimquote -% -\endisadelimquote -% -\end{itemize} -% -\begin{isamarkuptext}% -\noindent \emph{Function transformers} provide a very general interface, - transforming a list of function theorems to another - list of function theorems, provided that neither the heading - constant nor its type change. The \isa{{\isadigit{0}}} / \isa{Suc} - pattern elimination implemented in - theory \isa{Efficient{\isacharunderscore}Nat} (see \secref{eff_nat}) uses this - interface. - - \noindent The current setup of the preprocessor may be inspected using - the \hyperlink{command.print-codeproc}{\mbox{\isa{\isacommand{print{\isacharunderscore}codeproc}}}} command. - \hyperlink{command.code-thms}{\mbox{\isa{\isacommand{code{\isacharunderscore}thms}}}} provides a convenient - mechanism to inspect the impact of a preprocessor setup - on code equations. - - \begin{warn} - - Attribute \hyperlink{attribute.code-unfold}{\mbox{\isa{code{\isacharunderscore}unfold}}} also applies to the - preprocessor of the ancient \isa{SML\ code\ generator}; in case - this is not what you intend, use \hyperlink{attribute.code-inline}{\mbox{\isa{code{\isacharunderscore}inline}}} instead. - \end{warn}% -\end{isamarkuptext}% -\isamarkuptrue% -% -\isamarkupsubsection{Datatypes \label{sec:datatypes}% -} -\isamarkuptrue% -% -\begin{isamarkuptext}% -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 exactly 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 - \hyperlink{command.print-codesetup}{\mbox{\isa{\isacommand{print{\isacharunderscore}codesetup}}}} command. - - In some cases, it is appropriate to alter or extend this table. As - an example, we will develop an alternative representation of the - queue example given in \secref{sec:intro}. The amortised - representation is convenient for generating code but exposes its - \qt{implementation} details, which may be cumbersome when proving - theorems about it. Therefore, here is a simple, straightforward - representation of queues:% -\end{isamarkuptext}% -\isamarkuptrue% -% -\isadelimquote -% -\endisadelimquote -% -\isatagquote -\isacommand{datatype}\isamarkupfalse% -\ {\isacharprime}a\ queue\ {\isacharequal}\ Queue\ {\isachardoublequoteopen}{\isacharprime}a\ list{\isachardoublequoteclose}\isanewline -\isanewline -\isacommand{definition}\isamarkupfalse% -\ empty\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequoteopen}{\isacharprime}a\ queue{\isachardoublequoteclose}\ \isakeyword{where}\isanewline -\ \ {\isachardoublequoteopen}empty\ {\isacharequal}\ Queue\ {\isacharbrackleft}{\isacharbrackright}{\isachardoublequoteclose}\isanewline -\isanewline -\isacommand{primrec}\isamarkupfalse% -\ enqueue\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequoteopen}{\isacharprime}a\ {\isasymRightarrow}\ {\isacharprime}a\ queue\ {\isasymRightarrow}\ {\isacharprime}a\ queue{\isachardoublequoteclose}\ \isakeyword{where}\isanewline -\ \ {\isachardoublequoteopen}enqueue\ x\ {\isacharparenleft}Queue\ xs{\isacharparenright}\ {\isacharequal}\ Queue\ {\isacharparenleft}xs\ {\isacharat}\ {\isacharbrackleft}x{\isacharbrackright}{\isacharparenright}{\isachardoublequoteclose}\isanewline -\isanewline -\isacommand{fun}\isamarkupfalse% -\ dequeue\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequoteopen}{\isacharprime}a\ queue\ {\isasymRightarrow}\ {\isacharprime}a\ option\ {\isasymtimes}\ {\isacharprime}a\ queue{\isachardoublequoteclose}\ \isakeyword{where}\isanewline -\ \ \ \ {\isachardoublequoteopen}dequeue\ {\isacharparenleft}Queue\ {\isacharbrackleft}{\isacharbrackright}{\isacharparenright}\ {\isacharequal}\ {\isacharparenleft}None{\isacharcomma}\ Queue\ {\isacharbrackleft}{\isacharbrackright}{\isacharparenright}{\isachardoublequoteclose}\isanewline -\ \ {\isacharbar}\ {\isachardoublequoteopen}dequeue\ {\isacharparenleft}Queue\ {\isacharparenleft}x\ {\isacharhash}\ xs{\isacharparenright}{\isacharparenright}\ {\isacharequal}\ {\isacharparenleft}Some\ x{\isacharcomma}\ Queue\ xs{\isacharparenright}{\isachardoublequoteclose}% -\endisatagquote -{\isafoldquote}% -% -\isadelimquote -% -\endisadelimquote -% -\begin{isamarkuptext}% -\noindent This we can use directly for proving; for executing, - we provide an alternative characterisation:% -\end{isamarkuptext}% -\isamarkuptrue% -% -\isadelimquote -% -\endisadelimquote -% -\isatagquote -\isacommand{definition}\isamarkupfalse% -\ AQueue\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequoteopen}{\isacharprime}a\ list\ {\isasymRightarrow}\ {\isacharprime}a\ list\ {\isasymRightarrow}\ {\isacharprime}a\ queue{\isachardoublequoteclose}\ \isakeyword{where}\isanewline -\ \ {\isachardoublequoteopen}AQueue\ xs\ ys\ {\isacharequal}\ Queue\ {\isacharparenleft}ys\ {\isacharat}\ rev\ xs{\isacharparenright}{\isachardoublequoteclose}\isanewline -\isanewline -\isacommand{code{\isacharunderscore}datatype}\isamarkupfalse% -\ AQueue% -\endisatagquote -{\isafoldquote}% -% -\isadelimquote -% -\endisadelimquote -% -\begin{isamarkuptext}% -\noindent Here we define a \qt{constructor} \isa{AQueue} which - is defined in terms of \isa{Queue} and interprets its arguments - according to what the \emph{content} of an amortised queue is supposed - to be. Equipped with this, we are able to prove the following equations - for our primitive queue operations which \qt{implement} the simple - queues in an amortised fashion:% -\end{isamarkuptext}% -\isamarkuptrue% -% -\isadelimquote -% -\endisadelimquote -% -\isatagquote -\isacommand{lemma}\isamarkupfalse% -\ empty{\isacharunderscore}AQueue\ {\isacharbrackleft}code{\isacharbrackright}{\isacharcolon}\isanewline -\ \ {\isachardoublequoteopen}empty\ {\isacharequal}\ AQueue\ {\isacharbrackleft}{\isacharbrackright}\ {\isacharbrackleft}{\isacharbrackright}{\isachardoublequoteclose}\isanewline -\ \ \isacommand{unfolding}\isamarkupfalse% -\ AQueue{\isacharunderscore}def\ empty{\isacharunderscore}def\ \isacommand{by}\isamarkupfalse% -\ simp\isanewline -\isanewline -\isacommand{lemma}\isamarkupfalse% -\ enqueue{\isacharunderscore}AQueue\ {\isacharbrackleft}code{\isacharbrackright}{\isacharcolon}\isanewline -\ \ {\isachardoublequoteopen}enqueue\ x\ {\isacharparenleft}AQueue\ xs\ ys{\isacharparenright}\ {\isacharequal}\ AQueue\ {\isacharparenleft}x\ {\isacharhash}\ xs{\isacharparenright}\ ys{\isachardoublequoteclose}\isanewline -\ \ \isacommand{unfolding}\isamarkupfalse% -\ AQueue{\isacharunderscore}def\ \isacommand{by}\isamarkupfalse% -\ simp\isanewline -\isanewline -\isacommand{lemma}\isamarkupfalse% -\ dequeue{\isacharunderscore}AQueue\ {\isacharbrackleft}code{\isacharbrackright}{\isacharcolon}\isanewline -\ \ {\isachardoublequoteopen}dequeue\ {\isacharparenleft}AQueue\ xs\ {\isacharbrackleft}{\isacharbrackright}{\isacharparenright}\ {\isacharequal}\isanewline -\ \ \ \ {\isacharparenleft}if\ xs\ {\isacharequal}\ {\isacharbrackleft}{\isacharbrackright}\ then\ {\isacharparenleft}None{\isacharcomma}\ AQueue\ {\isacharbrackleft}{\isacharbrackright}\ {\isacharbrackleft}{\isacharbrackright}{\isacharparenright}\isanewline -\ \ \ \ else\ dequeue\ {\isacharparenleft}AQueue\ {\isacharbrackleft}{\isacharbrackright}\ {\isacharparenleft}rev\ xs{\isacharparenright}{\isacharparenright}{\isacharparenright}{\isachardoublequoteclose}\isanewline -\ \ {\isachardoublequoteopen}dequeue\ {\isacharparenleft}AQueue\ xs\ {\isacharparenleft}y\ {\isacharhash}\ ys{\isacharparenright}{\isacharparenright}\ {\isacharequal}\ {\isacharparenleft}Some\ y{\isacharcomma}\ AQueue\ xs\ ys{\isacharparenright}{\isachardoublequoteclose}\isanewline -\ \ \isacommand{unfolding}\isamarkupfalse% -\ AQueue{\isacharunderscore}def\ \isacommand{by}\isamarkupfalse% -\ simp{\isacharunderscore}all% -\endisatagquote -{\isafoldquote}% -% -\isadelimquote -% -\endisadelimquote -% -\begin{isamarkuptext}% -\noindent For completeness, we provide a substitute for the - \isa{case} combinator on queues:% -\end{isamarkuptext}% -\isamarkuptrue% -% -\isadelimquote -% -\endisadelimquote -% -\isatagquote -\isacommand{lemma}\isamarkupfalse% -\ queue{\isacharunderscore}case{\isacharunderscore}AQueue\ {\isacharbrackleft}code{\isacharbrackright}{\isacharcolon}\isanewline -\ \ {\isachardoublequoteopen}queue{\isacharunderscore}case\ f\ {\isacharparenleft}AQueue\ xs\ ys{\isacharparenright}\ {\isacharequal}\ f\ {\isacharparenleft}ys\ {\isacharat}\ rev\ xs{\isacharparenright}{\isachardoublequoteclose}\isanewline -\ \ \isacommand{unfolding}\isamarkupfalse% -\ AQueue{\isacharunderscore}def\ \isacommand{by}\isamarkupfalse% -\ simp% -\endisatagquote -{\isafoldquote}% -% -\isadelimquote -% -\endisadelimquote -% -\begin{isamarkuptext}% -\noindent The resulting code looks as expected:% -\end{isamarkuptext}% -\isamarkuptrue% -% -\isadelimquote -% -\endisadelimquote -% -\isatagquote -% -\begin{isamarkuptext}% -\isatypewriter% -\noindent% -\hspace*{0pt}structure Example :~sig\\ -\hspace*{0pt} ~val foldl :~('a -> 'b -> 'a) -> 'a -> 'b list -> 'a\\ -\hspace*{0pt} ~val rev :~'a list -> 'a list\\ -\hspace*{0pt} ~val null :~'a list -> bool\\ -\hspace*{0pt} ~datatype 'a queue = AQueue of 'a list * 'a list\\ -\hspace*{0pt} ~val empty :~'a queue\\ -\hspace*{0pt} ~val dequeue :~'a queue -> 'a option * 'a queue\\ -\hspace*{0pt} ~val enqueue :~'a -> 'a queue -> 'a queue\\ -\hspace*{0pt}end = struct\\ -\hspace*{0pt}\\ -\hspace*{0pt}fun foldl f a [] = a\\ -\hspace*{0pt} ~| foldl f a (x ::~xs) = foldl f (f a x) xs;\\ -\hspace*{0pt}\\ -\hspace*{0pt}fun rev xs = foldl (fn xsa => fn x => x ::~xsa) [] xs;\\ -\hspace*{0pt}\\ -\hspace*{0pt}fun null [] = true\\ -\hspace*{0pt} ~| null (x ::~xs) = false;\\ -\hspace*{0pt}\\ -\hspace*{0pt}datatype 'a queue = AQueue of 'a list * 'a list;\\ -\hspace*{0pt}\\ -\hspace*{0pt}val empty :~'a queue = AQueue ([],~[]);\\ -\hspace*{0pt}\\ -\hspace*{0pt}fun dequeue (AQueue (xs,~y ::~ys)) = (SOME y,~AQueue (xs,~ys))\\ -\hspace*{0pt} ~| dequeue (AQueue (xs,~[])) =\\ -\hspace*{0pt} ~~~(if null xs then (NONE,~AQueue ([],~[]))\\ -\hspace*{0pt} ~~~~~else dequeue (AQueue ([],~rev xs)));\\ -\hspace*{0pt}\\ -\hspace*{0pt}fun enqueue x (AQueue (xs,~ys)) = AQueue (x ::~xs,~ys);\\ -\hspace*{0pt}\\ -\hspace*{0pt}end;~(*struct Example*)% -\end{isamarkuptext}% -\isamarkuptrue% -% -\endisatagquote -{\isafoldquote}% -% -\isadelimquote -% -\endisadelimquote -% -\begin{isamarkuptext}% -\noindent From this example, it can be glimpsed that using own - constructor sets is a little delicate since it changes the set of - valid patterns for values of that type. Without going into much - detail, here some practical hints: - - \begin{itemize} - - \item When changing the constructor set for datatypes, take care - to provide alternative equations for the \isa{case} combinator. - - \item Values in the target language need not to be normalised -- - different values in the target language may represent the same - value in the logic. - - \item Usually, a good methodology to deal with the subtleties of - pattern matching is to see the type as an abstract type: provide - a set of operations which operate on the concrete representation - of the type, and derive further operations by combinations of - these primitive ones, without relying on a particular - representation. - - \end{itemize}% -\end{isamarkuptext}% -\isamarkuptrue% -% -\isamarkupsubsection{Equality% -} -\isamarkuptrue% -% -\begin{isamarkuptext}% -Surely you have already noticed how equality is treated - by the code generator:% -\end{isamarkuptext}% -\isamarkuptrue% -% -\isadelimquote -% -\endisadelimquote -% -\isatagquote -\isacommand{primrec}\isamarkupfalse% -\ 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}% -\endisatagquote -{\isafoldquote}% -% -\isadelimquote -% -\endisadelimquote -% -\begin{isamarkuptext}% -\noindent During preprocessing, the membership test is rewritten, - resulting in \isa{List{\isachardot}member}, which itself - performs an explicit equality check.% -\end{isamarkuptext}% -\isamarkuptrue% -% -\isadelimquote -% -\endisadelimquote -% -\isatagquote -% -\begin{isamarkuptext}% -\isatypewriter% -\noindent% -\hspace*{0pt}structure Example :~sig\\ -\hspace*{0pt} ~type 'a eq\\ -\hspace*{0pt} ~val eq :~'a eq -> 'a -> 'a -> bool\\ -\hspace*{0pt} ~val eqa :~'a eq -> 'a -> 'a -> bool\\ -\hspace*{0pt} ~val member :~'a eq -> 'a list -> 'a -> bool\\ -\hspace*{0pt} ~val collect{\char95}duplicates :\\ -\hspace*{0pt} ~~~'a eq -> 'a list -> 'a list -> 'a list -> 'a list\\ -\hspace*{0pt}end = struct\\ -\hspace*{0pt}\\ -\hspace*{0pt}type 'a eq = {\char123}eq :~'a -> 'a -> bool{\char125};\\ -\hspace*{0pt}val eq = {\char35}eq :~'a eq -> 'a -> 'a -> bool;\\ -\hspace*{0pt}\\ -\hspace*{0pt}fun eqa A{\char95}~a b = eq A{\char95}~a b;\\ -\hspace*{0pt}\\ -\hspace*{0pt}fun member A{\char95}~[] y = false\\ -\hspace*{0pt} ~| member A{\char95}~(x ::~xs) y = eqa A{\char95}~x y orelse member A{\char95}~xs y;\\ -\hspace*{0pt}\\ -\hspace*{0pt}fun collect{\char95}duplicates A{\char95}~xs ys [] = xs\\ -\hspace*{0pt} ~| collect{\char95}duplicates A{\char95}~xs ys (z ::~zs) =\\ -\hspace*{0pt} ~~~(if member A{\char95}~xs z\\ -\hspace*{0pt} ~~~~~then (if member A{\char95}~ys z then collect{\char95}duplicates A{\char95}~xs ys zs\\ -\hspace*{0pt} ~~~~~~~~~~~~else collect{\char95}duplicates A{\char95}~xs (z ::~ys) zs)\\ -\hspace*{0pt} ~~~~~else collect{\char95}duplicates A{\char95}~(z ::~xs) (z ::~ys) zs);\\ -\hspace*{0pt}\\ -\hspace*{0pt}end;~(*struct Example*)% -\end{isamarkuptext}% -\isamarkuptrue% -% -\endisatagquote -{\isafoldquote}% -% -\isadelimquote -% -\endisadelimquote -% -\begin{isamarkuptext}% -\noindent Obviously, polymorphic equality is implemented the Haskell - way using a type class. How is this achieved? HOL introduces - an explicit class \isa{eq} with a corresponding operation - \isa{eq{\isacharunderscore}class{\isachardot}eq} such that \isa{eq{\isacharunderscore}class{\isachardot}eq\ {\isacharequal}\ op\ {\isacharequal}}. - The preprocessing framework does the rest by propagating the - \isa{eq} constraints through all dependent code equations. - For datatypes, instances of \isa{eq} are implicitly derived - when possible. For other types, you may instantiate \isa{eq} - manually like any other type class.% -\end{isamarkuptext}% -\isamarkuptrue% -% -\isamarkupsubsection{Explicit partiality% -} -\isamarkuptrue% -% -\begin{isamarkuptext}% -Partiality usually enters the game by partial patterns, as - in the following example, again for amortised queues:% -\end{isamarkuptext}% -\isamarkuptrue% -% -\isadelimquote -% -\endisadelimquote -% -\isatagquote -\isacommand{definition}\isamarkupfalse% -\ strict{\isacharunderscore}dequeue\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequoteopen}{\isacharprime}a\ queue\ {\isasymRightarrow}\ {\isacharprime}a\ {\isasymtimes}\ {\isacharprime}a\ queue{\isachardoublequoteclose}\ \isakeyword{where}\isanewline -\ \ {\isachardoublequoteopen}strict{\isacharunderscore}dequeue\ q\ {\isacharequal}\ {\isacharparenleft}case\ dequeue\ q\isanewline -\ \ \ \ of\ {\isacharparenleft}Some\ x{\isacharcomma}\ q{\isacharprime}{\isacharparenright}\ {\isasymRightarrow}\ {\isacharparenleft}x{\isacharcomma}\ q{\isacharprime}{\isacharparenright}{\isacharparenright}{\isachardoublequoteclose}\isanewline -\isanewline -\isacommand{lemma}\isamarkupfalse% -\ strict{\isacharunderscore}dequeue{\isacharunderscore}AQueue\ {\isacharbrackleft}code{\isacharbrackright}{\isacharcolon}\isanewline -\ \ {\isachardoublequoteopen}strict{\isacharunderscore}dequeue\ {\isacharparenleft}AQueue\ xs\ {\isacharparenleft}y\ {\isacharhash}\ ys{\isacharparenright}{\isacharparenright}\ {\isacharequal}\ {\isacharparenleft}y{\isacharcomma}\ AQueue\ xs\ ys{\isacharparenright}{\isachardoublequoteclose}\isanewline -\ \ {\isachardoublequoteopen}strict{\isacharunderscore}dequeue\ {\isacharparenleft}AQueue\ xs\ {\isacharbrackleft}{\isacharbrackright}{\isacharparenright}\ {\isacharequal}\isanewline -\ \ \ \ {\isacharparenleft}case\ rev\ xs\ of\ y\ {\isacharhash}\ ys\ {\isasymRightarrow}\ {\isacharparenleft}y{\isacharcomma}\ AQueue\ {\isacharbrackleft}{\isacharbrackright}\ ys{\isacharparenright}{\isacharparenright}{\isachardoublequoteclose}\isanewline -\ \ \isacommand{by}\isamarkupfalse% -\ {\isacharparenleft}simp{\isacharunderscore}all\ add{\isacharcolon}\ strict{\isacharunderscore}dequeue{\isacharunderscore}def\ dequeue{\isacharunderscore}AQueue\ split{\isacharcolon}\ list{\isachardot}splits{\isacharparenright}% -\endisatagquote -{\isafoldquote}% -% -\isadelimquote -% -\endisadelimquote -% -\begin{isamarkuptext}% -\noindent In the corresponding code, there is no equation - for the pattern \isa{AQueue\ {\isacharbrackleft}{\isacharbrackright}\ {\isacharbrackleft}{\isacharbrackright}}:% -\end{isamarkuptext}% -\isamarkuptrue% -% -\isadelimquote -% -\endisadelimquote -% -\isatagquote -% -\begin{isamarkuptext}% -\isatypewriter% -\noindent% -\hspace*{0pt}strict{\char95}dequeue ::~forall a.~Queue a -> (a,~Queue a);\\ -\hspace*{0pt}strict{\char95}dequeue (AQueue xs []) =\\ -\hspace*{0pt} ~let {\char123}\\ -\hspace*{0pt} ~~~(y :~ys) = reverse xs;\\ -\hspace*{0pt} ~{\char125}~in (y,~AQueue [] ys);\\ -\hspace*{0pt}strict{\char95}dequeue (AQueue xs (y :~ys)) = (y,~AQueue xs ys);% -\end{isamarkuptext}% -\isamarkuptrue% -% -\endisatagquote -{\isafoldquote}% -% -\isadelimquote -% -\endisadelimquote -% -\begin{isamarkuptext}% -\noindent In some cases it is desirable to have this - pseudo-\qt{partiality} more explicitly, e.g.~as follows:% -\end{isamarkuptext}% -\isamarkuptrue% -% -\isadelimquote -% -\endisadelimquote -% -\isatagquote -\isacommand{axiomatization}\isamarkupfalse% -\ empty{\isacharunderscore}queue\ {\isacharcolon}{\isacharcolon}\ {\isacharprime}a\isanewline -\isanewline -\isacommand{definition}\isamarkupfalse% -\ strict{\isacharunderscore}dequeue{\isacharprime}\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequoteopen}{\isacharprime}a\ queue\ {\isasymRightarrow}\ {\isacharprime}a\ {\isasymtimes}\ {\isacharprime}a\ queue{\isachardoublequoteclose}\ \isakeyword{where}\isanewline -\ \ {\isachardoublequoteopen}strict{\isacharunderscore}dequeue{\isacharprime}\ q\ {\isacharequal}\ {\isacharparenleft}case\ dequeue\ q\ of\ {\isacharparenleft}Some\ x{\isacharcomma}\ q{\isacharprime}{\isacharparenright}\ {\isasymRightarrow}\ {\isacharparenleft}x{\isacharcomma}\ q{\isacharprime}{\isacharparenright}\ {\isacharbar}\ {\isacharunderscore}\ {\isasymRightarrow}\ empty{\isacharunderscore}queue{\isacharparenright}{\isachardoublequoteclose}\isanewline -\isanewline -\isacommand{lemma}\isamarkupfalse% -\ strict{\isacharunderscore}dequeue{\isacharprime}{\isacharunderscore}AQueue\ {\isacharbrackleft}code{\isacharbrackright}{\isacharcolon}\isanewline -\ \ {\isachardoublequoteopen}strict{\isacharunderscore}dequeue{\isacharprime}\ {\isacharparenleft}AQueue\ xs\ {\isacharbrackleft}{\isacharbrackright}{\isacharparenright}\ {\isacharequal}\ {\isacharparenleft}if\ xs\ {\isacharequal}\ {\isacharbrackleft}{\isacharbrackright}\ then\ empty{\isacharunderscore}queue\isanewline -\ \ \ \ \ else\ strict{\isacharunderscore}dequeue{\isacharprime}\ {\isacharparenleft}AQueue\ {\isacharbrackleft}{\isacharbrackright}\ {\isacharparenleft}rev\ xs{\isacharparenright}{\isacharparenright}{\isacharparenright}{\isachardoublequoteclose}\isanewline -\ \ {\isachardoublequoteopen}strict{\isacharunderscore}dequeue{\isacharprime}\ {\isacharparenleft}AQueue\ xs\ {\isacharparenleft}y\ {\isacharhash}\ ys{\isacharparenright}{\isacharparenright}\ {\isacharequal}\isanewline -\ \ \ \ \ {\isacharparenleft}y{\isacharcomma}\ AQueue\ xs\ ys{\isacharparenright}{\isachardoublequoteclose}\isanewline -\ \ \isacommand{by}\isamarkupfalse% -\ {\isacharparenleft}simp{\isacharunderscore}all\ add{\isacharcolon}\ strict{\isacharunderscore}dequeue{\isacharprime}{\isacharunderscore}def\ dequeue{\isacharunderscore}AQueue\ split{\isacharcolon}\ list{\isachardot}splits{\isacharparenright}% -\endisatagquote -{\isafoldquote}% -% -\isadelimquote -% -\endisadelimquote -% -\begin{isamarkuptext}% -Observe that on the right hand side of the definition of \isa{strict{\isacharunderscore}dequeue{\isacharprime}}, the unspecified constant \isa{empty{\isacharunderscore}queue} occurs. - - Normally, if constants without any code equations occur in a - program, the code generator complains (since in most cases this is - indeed an error). But such constants can also be thought - of as function definitions which always fail, - since there is never a successful pattern match on the left hand - side. In order to categorise a constant into that category - explicitly, use \hyperlink{command.code-abort}{\mbox{\isa{\isacommand{code{\isacharunderscore}abort}}}}:% -\end{isamarkuptext}% -\isamarkuptrue% -% -\isadelimquote -% -\endisadelimquote -% -\isatagquote -\isacommand{code{\isacharunderscore}abort}\isamarkupfalse% -\ empty{\isacharunderscore}queue% -\endisatagquote -{\isafoldquote}% -% -\isadelimquote -% -\endisadelimquote -% -\begin{isamarkuptext}% -\noindent Then the code generator will just insert an error or - exception at the appropriate position:% -\end{isamarkuptext}% -\isamarkuptrue% -% -\isadelimquote -% -\endisadelimquote -% -\isatagquote -% -\begin{isamarkuptext}% -\isatypewriter% -\noindent% -\hspace*{0pt}empty{\char95}queue ::~forall a.~a;\\ -\hspace*{0pt}empty{\char95}queue = error {\char34}empty{\char95}queue{\char34};\\ -\hspace*{0pt}\\ -\hspace*{0pt}strict{\char95}dequeue ::~forall a.~Queue a -> (a,~Queue a);\\ -\hspace*{0pt}strict{\char95}dequeue (AQueue xs (y :~ys)) = (y,~AQueue xs ys);\\ -\hspace*{0pt}strict{\char95}dequeue (AQueue xs []) =\\ -\hspace*{0pt} ~(if null xs then empty{\char95}queue\\ -\hspace*{0pt} ~~~else strict{\char95}dequeue (AQueue [] (reverse xs)));% -\end{isamarkuptext}% -\isamarkuptrue% -% -\endisatagquote -{\isafoldquote}% -% -\isadelimquote -% -\endisadelimquote -% -\begin{isamarkuptext}% -\noindent This feature however is rarely needed in practice. - Note also that the \isa{HOL} default setup already declares - \isa{undefined} as \hyperlink{command.code-abort}{\mbox{\isa{\isacommand{code{\isacharunderscore}abort}}}}, which is most - likely to be used in such situations.% -\end{isamarkuptext}% -\isamarkuptrue% -% -\isadelimtheory -% -\endisadelimtheory -% -\isatagtheory -\isacommand{end}\isamarkupfalse% -% -\endisatagtheory -{\isafoldtheory}% -% -\isadelimtheory -% -\endisadelimtheory -\isanewline -\end{isabellebody}% -%%% Local Variables: -%%% mode: latex -%%% TeX-master: "root" -%%% End: diff -r 7eb0f6991e25 -r 001f2f44984c doc-src/Codegen/Thy/document/Refinement.tex --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/doc-src/Codegen/Thy/document/Refinement.tex Sat Aug 14 13:24:06 2010 +0200 @@ -0,0 +1,43 @@ +% +\begin{isabellebody}% +\def\isabellecontext{Refinement}% +% +\isadelimtheory +% +\endisadelimtheory +% +\isatagtheory +\isacommand{theory}\isamarkupfalse% +\ Refinement\isanewline +\isakeyword{imports}\ Setup\isanewline +\isakeyword{begin}% +\endisatagtheory +{\isafoldtheory}% +% +\isadelimtheory +% +\endisadelimtheory +% +\isamarkupsection{Program and datatype refinement \label{sec:refinement}% +} +\isamarkuptrue% +% +\isadelimtheory +% +\endisadelimtheory +% +\isatagtheory +\isacommand{end}\isamarkupfalse% +% +\endisatagtheory +{\isafoldtheory}% +% +\isadelimtheory +% +\endisadelimtheory +\isanewline +\end{isabellebody}% +%%% Local Variables: +%%% mode: latex +%%% TeX-master: "root" +%%% End: diff -r 7eb0f6991e25 -r 001f2f44984c doc-src/Codegen/codegen.tex --- a/doc-src/Codegen/codegen.tex Sat Aug 14 12:01:50 2010 +0200 +++ b/doc-src/Codegen/codegen.tex Sat Aug 14 13:24:06 2010 +0200 @@ -20,9 +20,9 @@ \maketitle \begin{abstract} - \noindent This tutorial gives an introduction to a generic code generator framework in Isabelle - for generating executable code in functional programming languages from logical - specifications in Isabelle/HOL. + \noindent This tutorial introduces the code generator facilities of Isabelle/HOL. + They empower the user to turn HOL specifications into corresponding executable + programs in the languages SML, OCaml and Haskell. \end{abstract} \thispagestyle{empty}\clearpage @@ -31,11 +31,11 @@ \clearfirst \input{Thy/document/Introduction.tex} -\input{Thy/document/Program.tex} +\input{Thy/document/Foundations.tex} +\input{Thy/document/Refinement.tex} \input{Thy/document/Inductive_Predicate.tex} \input{Thy/document/Adaptation.tex} \input{Thy/document/Further.tex} -\input{Thy/document/ML.tex} \begingroup \bibliographystyle{plain} \small\raggedright\frenchspacing diff -r 7eb0f6991e25 -r 001f2f44984c doc-src/Codegen/style.sty --- a/doc-src/Codegen/style.sty Sat Aug 14 12:01:50 2010 +0200 +++ b/doc-src/Codegen/style.sty Sat Aug 14 13:24:06 2010 +0200 @@ -15,6 +15,7 @@ %% typographic conventions \newcommand{\qt}[1]{``{#1}''} +\newcommand{\ditem}[1]{\item[\isastyletext #1]} %% verbatim text \newcommand{\isatypewriter}{\fontsize{9pt}{0pt}\tt\renewcommand{\baselinestretch}{1}\setlength{\baselineskip}{9pt}} diff -r 7eb0f6991e25 -r 001f2f44984c src/HOL/Finite_Set.thy --- a/src/HOL/Finite_Set.thy Sat Aug 14 12:01:50 2010 +0200 +++ b/src/HOL/Finite_Set.thy Sat Aug 14 13:24:06 2010 +0200 @@ -6,7 +6,7 @@ header {* Finite sets *} theory Finite_Set -imports Power Option +imports Option Power begin subsection {* Predicate for finite sets *} diff -r 7eb0f6991e25 -r 001f2f44984c src/HOL/Imperative_HOL/Heap.thy --- a/src/HOL/Imperative_HOL/Heap.thy Sat Aug 14 12:01:50 2010 +0200 +++ b/src/HOL/Imperative_HOL/Heap.thy Sat Aug 14 13:24:06 2010 +0200 @@ -14,6 +14,10 @@ class heap = typerep + countable +instance unit :: heap .. + +instance bool :: heap .. + instance nat :: heap .. instance prod :: (heap, heap) heap .. diff -r 7eb0f6991e25 -r 001f2f44984c src/HOL/Imperative_HOL/Heap_Monad.thy --- a/src/HOL/Imperative_HOL/Heap_Monad.thy Sat Aug 14 12:01:50 2010 +0200 +++ b/src/HOL/Imperative_HOL/Heap_Monad.thy Sat Aug 14 13:24:06 2010 +0200 @@ -274,6 +274,11 @@ "execute f h = None \ execute (f \= g) h = None" by (simp_all add: bind_def) +lemma execute_bind_case: + "execute (f \= g) h = (case (execute f h) of + Some (x, h') \ execute (g x) h' | None \ None)" + by (simp add: bind_def) + lemma execute_bind_success: "success f h \ execute (f \= g) h = execute (g (fst (the (execute f h)))) (snd (the (execute f h)))" by (cases f h rule: Heap_cases) (auto elim!: successE simp add: bind_def) @@ -536,18 +541,18 @@ fun force (t as IConst (c, _) `$ t') = if is_return c then t' else t `$ unitt | force t = t `$ unitt; - fun tr_bind' [(t1, _), (t2, ty2)] = + fun tr_bind'' [(t1, _), (t2, ty2)] = let val ((v, ty), t) = dest_abs (t2, ty2); - in ICase (((force t1, ty), [(IVar v, tr_bind'' t)]), dummy_case_term) end - and tr_bind'' t = case unfold_app t - of (IConst (c, (_, ty1 :: ty2 :: _)), [x1, x2]) => if is_bind c - then tr_bind' [(x1, ty1), (x2, ty2)] - else force t - | _ => force t; + in ICase (((force t1, ty), [(IVar v, tr_bind' t)]), dummy_case_term) end + and tr_bind' t = case unfold_app t + of (IConst (c, (_, ty1 :: ty2 :: _)), [x1, x2]) => if is_bind c + then tr_bind'' [(x1, ty1), (x2, ty2)] + else force t + | _ => force t; fun imp_monad_bind'' ts = (SOME dummy_name, unitT) `|=> ICase (((IVar (SOME dummy_name), unitT), - [(unitt, tr_bind' ts)]), dummy_case_term) - and imp_monad_bind' (const as (c, (_, tys))) ts = if is_bind c then case (ts, tys) + [(unitt, tr_bind'' ts)]), dummy_case_term) + fun imp_monad_bind' (const as (c, (_, tys))) ts = if is_bind c then case (ts, tys) of ([t1, t2], ty1 :: ty2 :: _) => imp_monad_bind'' [(t1, ty1), (t2, ty2)] | ([t1, t2, t3], ty1 :: ty2 :: _) => imp_monad_bind'' [(t1, ty1), (t2, ty2)] `$ t3 | (ts, _) => imp_monad_bind (eta_expand 2 (const, ts)) diff -r 7eb0f6991e25 -r 001f2f44984c src/HOL/Imperative_HOL/ex/Linked_Lists.thy --- a/src/HOL/Imperative_HOL/ex/Linked_Lists.thy Sat Aug 14 12:01:50 2010 +0200 +++ b/src/HOL/Imperative_HOL/ex/Linked_Lists.thy Sat Aug 14 13:24:06 2010 +0200 @@ -648,8 +648,9 @@ from refs_def Node have refs_of'_ps: "refs_of' h ps refs" by (auto simp add: refs_of'_def'[symmetric]) from validHeap refs_def have all_ref_present: "\r\set refs. Ref.present h r" by simp - from init refs_of'_ps Node this have heap_eq: "\refs. refs_of' h ps refs \ (\ref\set refs. Ref.present h ref \ Ref.present h2 ref \ Ref.get h ref = Ref.get h2 ref)" - by (fastsimp elim!: crel_ref dest: refs_of'_is_fun) + from init refs_of'_ps this + have heap_eq: "\refs. refs_of' h ps refs \ (\ref\set refs. Ref.present h ref \ Ref.present h2 ref \ Ref.get h ref = Ref.get h2 ref)" + by (auto elim!: crel_ref [where ?'a="'a node", where ?'b="'a node", where ?'c="'a node"] dest: refs_of'_is_fun) from refs_of'_invariant[OF refs_of'_ps this] have "refs_of' h2 ps refs" . with init have refs_of_p: "refs_of' h2 p (p#refs)" by (auto elim!: crel_refE simp add: refs_of'_def') diff -r 7eb0f6991e25 -r 001f2f44984c src/HOL/IsaMakefile --- a/src/HOL/IsaMakefile Sat Aug 14 12:01:50 2010 +0200 +++ b/src/HOL/IsaMakefile Sat Aug 14 13:24:06 2010 +0200 @@ -207,14 +207,12 @@ Tools/old_primrec.ML \ Tools/primrec.ML \ Tools/prop_logic.ML \ - Tools/record.ML \ Tools/refute.ML \ Tools/refute_isar.ML \ Tools/rewrite_hol_proof.ML \ Tools/sat_funcs.ML \ Tools/sat_solver.ML \ Tools/split_rule.ML \ - Tools/typecopy.ML \ Tools/typedef_codegen.ML \ Tools/typedef.ML \ Transitive_Closure.thy \ @@ -305,6 +303,7 @@ Tools/Predicate_Compile/predicate_compile_specialisation.ML \ Tools/Predicate_Compile/predicate_compile_pred.ML \ Tools/quickcheck_generators.ML \ + Tools/quickcheck_record.ML \ Tools/Qelim/cooper.ML \ Tools/Qelim/cooper_procedure.ML \ Tools/Qelim/qelim.ML \ @@ -314,6 +313,7 @@ Tools/Quotient/quotient_term.ML \ Tools/Quotient/quotient_typ.ML \ Tools/recdef.ML \ + Tools/record.ML \ Tools/semiring_normalizer.ML \ Tools/Sledgehammer/clausifier.ML \ Tools/Sledgehammer/meson_tactic.ML \ @@ -343,6 +343,7 @@ Tools/string_code.ML \ Tools/string_syntax.ML \ Tools/transfer.ML \ + Tools/typecopy.ML \ Tools/TFL/casesplit.ML \ Tools/TFL/dcterm.ML \ Tools/TFL/post.ML \ diff -r 7eb0f6991e25 -r 001f2f44984c src/HOL/Main.thy --- a/src/HOL/Main.thy Sat Aug 14 12:01:50 2010 +0200 +++ b/src/HOL/Main.thy Sat Aug 14 13:24:06 2010 +0200 @@ -1,7 +1,7 @@ header {* Main HOL *} theory Main -imports Plain Predicate_Compile Nitpick SMT +imports Plain Record Predicate_Compile Nitpick SMT begin text {* diff -r 7eb0f6991e25 -r 001f2f44984c src/HOL/Nitpick.thy --- a/src/HOL/Nitpick.thy Sat Aug 14 12:01:50 2010 +0200 +++ b/src/HOL/Nitpick.thy Sat Aug 14 13:24:06 2010 +0200 @@ -8,7 +8,7 @@ header {* Nitpick: Yet Another Counterexample Generator for Isabelle/HOL *} theory Nitpick -imports Map Quotient SAT +imports Map Quotient SAT Record uses ("Tools/Nitpick/kodkod.ML") ("Tools/Nitpick/kodkod_sat.ML") ("Tools/Nitpick/nitpick_util.ML") diff -r 7eb0f6991e25 -r 001f2f44984c src/HOL/Plain.thy --- a/src/HOL/Plain.thy Sat Aug 14 12:01:50 2010 +0200 +++ b/src/HOL/Plain.thy Sat Aug 14 13:24:06 2010 +0200 @@ -1,7 +1,7 @@ header {* Plain HOL *} theory Plain -imports Datatype Record FunDef Extraction +imports Datatype FunDef Extraction begin text {* diff -r 7eb0f6991e25 -r 001f2f44984c src/HOL/Record.thy --- a/src/HOL/Record.thy Sat Aug 14 12:01:50 2010 +0200 +++ b/src/HOL/Record.thy Sat Aug 14 13:24:06 2010 +0200 @@ -9,8 +9,8 @@ header {* Extensible records with structural subtyping *} theory Record -imports Datatype -uses ("Tools/record.ML") +imports Plain Quickcheck +uses ("Tools/typecopy.ML") ("Tools/record.ML") ("Tools/quickcheck_record.ML") begin subsection {* Introduction *} @@ -123,67 +123,67 @@ definition iso_tuple_update_accessor_cong_assist :: "(('b \ 'b) \ ('a \ 'a)) \ ('a \ 'b) \ bool" where - "iso_tuple_update_accessor_cong_assist upd acc \ - (\f v. upd (\x. f (acc v)) v = upd f v) \ (\v. upd id v = v)" + "iso_tuple_update_accessor_cong_assist upd ac \ + (\f v. upd (\x. f (ac v)) v = upd f v) \ (\v. upd id v = v)" definition iso_tuple_update_accessor_eq_assist :: "(('b \ 'b) \ ('a \ 'a)) \ ('a \ 'b) \ 'a \ ('b \ 'b) \ 'a \ 'b \ bool" where - "iso_tuple_update_accessor_eq_assist upd acc v f v' x \ - upd f v = v' \ acc v = x \ iso_tuple_update_accessor_cong_assist upd acc" + "iso_tuple_update_accessor_eq_assist upd ac v f v' x \ + upd f v = v' \ ac v = x \ iso_tuple_update_accessor_cong_assist upd ac" lemma update_accessor_congruence_foldE: - assumes uac: "iso_tuple_update_accessor_cong_assist upd acc" - and r: "r = r'" and v: "acc r' = v'" + assumes uac: "iso_tuple_update_accessor_cong_assist upd ac" + and r: "r = r'" and v: "ac r' = v'" and f: "\v. v' = v \ f v = f' v" shows "upd f r = upd f' r'" using uac r v [symmetric] - apply (subgoal_tac "upd (\x. f (acc r')) r' = upd (\x. f' (acc r')) r'") + apply (subgoal_tac "upd (\x. f (ac r')) r' = upd (\x. f' (ac r')) r'") apply (simp add: iso_tuple_update_accessor_cong_assist_def) apply (simp add: f) done lemma update_accessor_congruence_unfoldE: - "iso_tuple_update_accessor_cong_assist upd acc \ - r = r' \ acc r' = v' \ (\v. v = v' \ f v = f' v) \ + "iso_tuple_update_accessor_cong_assist upd ac \ + r = r' \ ac r' = v' \ (\v. v = v' \ f v = f' v) \ upd f r = upd f' r'" apply (erule(2) update_accessor_congruence_foldE) apply simp done lemma iso_tuple_update_accessor_cong_assist_id: - "iso_tuple_update_accessor_cong_assist upd acc \ upd id = id" + "iso_tuple_update_accessor_cong_assist upd ac \ upd id = id" by rule (simp add: iso_tuple_update_accessor_cong_assist_def) lemma update_accessor_noopE: - assumes uac: "iso_tuple_update_accessor_cong_assist upd acc" - and acc: "f (acc x) = acc x" + assumes uac: "iso_tuple_update_accessor_cong_assist upd ac" + and ac: "f (ac x) = ac x" shows "upd f x = x" using uac - by (simp add: acc iso_tuple_update_accessor_cong_assist_id [OF uac, unfolded id_def] + by (simp add: ac iso_tuple_update_accessor_cong_assist_id [OF uac, unfolded id_def] cong: update_accessor_congruence_unfoldE [OF uac]) lemma update_accessor_noop_compE: - assumes uac: "iso_tuple_update_accessor_cong_assist upd acc" - and acc: "f (acc x) = acc x" + assumes uac: "iso_tuple_update_accessor_cong_assist upd ac" + and ac: "f (ac x) = ac x" shows "upd (g \ f) x = upd g x" - by (simp add: acc cong: update_accessor_congruence_unfoldE[OF uac]) + by (simp add: ac cong: update_accessor_congruence_unfoldE[OF uac]) lemma update_accessor_cong_assist_idI: "iso_tuple_update_accessor_cong_assist id id" by (simp add: iso_tuple_update_accessor_cong_assist_def) lemma update_accessor_cong_assist_triv: - "iso_tuple_update_accessor_cong_assist upd acc \ - iso_tuple_update_accessor_cong_assist upd acc" + "iso_tuple_update_accessor_cong_assist upd ac \ + iso_tuple_update_accessor_cong_assist upd ac" by assumption lemma update_accessor_accessor_eqE: - "iso_tuple_update_accessor_eq_assist upd acc v f v' x \ acc v = x" + "iso_tuple_update_accessor_eq_assist upd ac v f v' x \ ac v = x" by (simp add: iso_tuple_update_accessor_eq_assist_def) lemma update_accessor_updator_eqE: - "iso_tuple_update_accessor_eq_assist upd acc v f v' x \ upd f v = v'" + "iso_tuple_update_accessor_eq_assist upd ac v f v' x \ upd f v = v'" by (simp add: iso_tuple_update_accessor_eq_assist_def) lemma iso_tuple_update_accessor_eq_assist_idI: @@ -191,13 +191,13 @@ by (simp add: iso_tuple_update_accessor_eq_assist_def update_accessor_cong_assist_idI) lemma iso_tuple_update_accessor_eq_assist_triv: - "iso_tuple_update_accessor_eq_assist upd acc v f v' x \ - iso_tuple_update_accessor_eq_assist upd acc v f v' x" + "iso_tuple_update_accessor_eq_assist upd ac v f v' x \ + iso_tuple_update_accessor_eq_assist upd ac v f v' x" by assumption lemma iso_tuple_update_accessor_cong_from_eq: - "iso_tuple_update_accessor_eq_assist upd acc v f v' x \ - iso_tuple_update_accessor_cong_assist upd acc" + "iso_tuple_update_accessor_eq_assist upd ac v f v' x \ + iso_tuple_update_accessor_cong_assist upd ac" by (simp add: iso_tuple_update_accessor_eq_assist_def) lemma iso_tuple_surjective_proof_assistI: @@ -452,8 +452,9 @@ subsection {* Record package *} -use "Tools/record.ML" -setup Record.setup +use "Tools/typecopy.ML" setup Typecopy.setup +use "Tools/record.ML" setup Record.setup +use "Tools/quickcheck_record.ML" setup Quickcheck_Record.setup hide_const (open) Tuple_Isomorphism repr abst iso_tuple_fst iso_tuple_snd iso_tuple_fst_update iso_tuple_snd_update iso_tuple_cons diff -r 7eb0f6991e25 -r 001f2f44984c src/HOL/Statespace/state_space.ML --- a/src/HOL/Statespace/state_space.ML Sat Aug 14 12:01:50 2010 +0200 +++ b/src/HOL/Statespace/state_space.ML Sat Aug 14 13:24:06 2010 +0200 @@ -466,7 +466,7 @@ (suffix valuetypesN full_name,(("",false),Expression.Named []))],[]) fixestate |> ProofContext.theory_of |> fold interprete_parent parents - |> add_declaration (SOME full_name) (declare_declinfo components') + |> add_declaration full_name (declare_declinfo components') end; diff -r 7eb0f6991e25 -r 001f2f44984c src/HOL/Tools/Quotient/quotient_typ.ML --- a/src/HOL/Tools/Quotient/quotient_typ.ML Sat Aug 14 12:01:50 2010 +0200 +++ b/src/HOL/Tools/Quotient/quotient_typ.ML Sat Aug 14 13:24:06 2010 +0200 @@ -101,7 +101,6 @@ rtac rep_inj]) 1 end - (* proves the quot_type theorem for the new type *) fun typedef_quot_type_thm (rel, abs, rep, equiv_thm, typedef_info) lthy = let @@ -114,25 +113,6 @@ (K (typedef_quot_type_tac equiv_thm typedef_info)) end -(* proves the quotient theorem for the new type *) -fun typedef_quotient_thm (rel, abs, rep, abs_def, rep_def, quot_type_thm) lthy = -let - val quotient_const = Const (@{const_name "Quotient"}, dummyT) - val goal = - HOLogic.mk_Trueprop (quotient_const $ rel $ abs $ rep) - |> Syntax.check_term lthy - - val typedef_quotient_thm_tac = - EVERY1 [ - K (rewrite_goals_tac [abs_def, rep_def]), - rtac @{thm quot_type.Quotient}, - rtac quot_type_thm] -in - Goal.prove lthy [] [] goal - (K typedef_quotient_thm_tac) -end - - (* main function for constructing a quotient type *) fun add_quotient_type (((vs, qty_name, mx), (rty, rel, partial)), equiv_thm) lthy = let @@ -160,15 +140,17 @@ val abs_name = Binding.prefix_name "abs_" qty_name val rep_name = Binding.prefix_name "rep_" qty_name - val ((abs, abs_def), lthy2) = define (abs_name, NoSyn, abs_trm) lthy1 - val ((rep, rep_def), lthy3) = define (rep_name, NoSyn, rep_trm) lthy2 + val ((_, abs_def), lthy2) = define (abs_name, NoSyn, abs_trm) lthy1 + val ((_, rep_def), lthy3) = define (rep_name, NoSyn, rep_trm) lthy2 (* quot_type theorem *) val quot_thm = typedef_quot_type_thm (rel, Abs_const, Rep_const, part_equiv, typedef_info) lthy3 (* quotient theorem *) - val quotient_thm = typedef_quotient_thm (rel, abs, rep, abs_def, rep_def, quot_thm) lthy3 val quotient_thm_name = Binding.prefix_name "Quotient_" qty_name + val quotient_thm = + (quot_thm RS @{thm quot_type.Quotient}) + |> fold_rule [abs_def, rep_def] (* name equivalence theorem *) val equiv_thm_name = Binding.suffix_name "_equivp" qty_name diff -r 7eb0f6991e25 -r 001f2f44984c src/HOL/Tools/Sledgehammer/sledgehammer_fact_filter.ML --- a/src/HOL/Tools/Sledgehammer/sledgehammer_fact_filter.ML Sat Aug 14 12:01:50 2010 +0200 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_fact_filter.ML Sat Aug 14 13:24:06 2010 +0200 @@ -511,8 +511,6 @@ clearly inconsistent facts such as X = a | X = b, though it by no means guarantees soundness. *) -fun is_record_type T = not (null (Record.dest_recTs T)) - (* Unwanted equalities are those between a (bound or schematic) variable that does not properly occur in the second operand. *) fun too_general_eqterms (Var z) t = diff -r 7eb0f6991e25 -r 001f2f44984c src/HOL/Tools/inductive.ML --- a/src/HOL/Tools/inductive.ML Sat Aug 14 12:01:50 2010 +0200 +++ b/src/HOL/Tools/inductive.ML Sat Aug 14 13:24:06 2010 +0200 @@ -998,7 +998,7 @@ let val name = Sign.full_name thy (fst (fst (hd cnames_syn))); val ctxt' = thy - |> Named_Target.init NONE + |> Named_Target.theory_init |> add_inductive_i flags cnames_syn pnames pre_intros monos |> snd |> Local_Theory.exit; val info = #2 (the_inductive ctxt' name); diff -r 7eb0f6991e25 -r 001f2f44984c src/HOL/Tools/primrec.ML --- a/src/HOL/Tools/primrec.ML Sat Aug 14 12:01:50 2010 +0200 +++ b/src/HOL/Tools/primrec.ML Sat Aug 14 13:24:06 2010 +0200 @@ -292,7 +292,7 @@ fun add_primrec_global fixes specs thy = let - val lthy = Named_Target.init NONE thy; + val lthy = Named_Target.theory_init thy; val ((ts, simps), lthy') = add_primrec fixes specs lthy; val simps' = ProofContext.export lthy' lthy simps; in ((ts, simps'), Local_Theory.exit_global lthy') end; diff -r 7eb0f6991e25 -r 001f2f44984c src/HOL/Tools/quickcheck_generators.ML --- a/src/HOL/Tools/quickcheck_generators.ML Sat Aug 14 12:01:50 2010 +0200 +++ b/src/HOL/Tools/quickcheck_generators.ML Sat Aug 14 13:24:06 2010 +0200 @@ -10,7 +10,6 @@ val random_fun: typ -> typ -> ('a -> 'a -> bool) -> ('a -> term) -> (seed -> ('b * (unit -> term)) * seed) -> (seed -> seed * seed) -> seed -> (('a -> 'b) * (unit -> term)) * seed - val ensure_random_typecopy: string -> theory -> theory val random_aux_specification: string -> string -> term list -> local_theory -> local_theory val mk_random_aux_eqs: theory -> Datatype.descr -> (string * sort) list -> string list -> string list * string list -> typ list * typ list @@ -65,53 +64,10 @@ in ((random_fun', term_fun'), seed''') end; -(** type copies **) - -fun mk_random_typecopy tyco vs constr T' thy = - let - val mk_const = curry (Sign.mk_const thy); - val Ts = map TFree vs; - val T = Type (tyco, Ts); - val Tm = termifyT T; - val Tm' = termifyT T'; - val v = "x"; - val t_v = Free (v, Tm'); - val t_constr = Const (constr, T' --> T); - val lhs = HOLogic.mk_random T size; - val rhs = HOLogic.mk_ST [((HOLogic.mk_random T' size, @{typ Random.seed}), SOME (v, Tm'))] - (HOLogic.mk_return Tm @{typ Random.seed} - (mk_const "Code_Evaluation.valapp" [T', T] - $ HOLogic.mk_prod (t_constr, Abs ("u", @{typ unit}, HOLogic.reflect_term t_constr)) $ t_v)) - @{typ Random.seed} (SOME Tm, @{typ Random.seed}); - val eq = HOLogic.mk_Trueprop (HOLogic.mk_eq (lhs, rhs)); - in - thy - |> Class.instantiation ([tyco], vs, @{sort random}) - |> `(fn lthy => Syntax.check_term lthy eq) - |-> (fn eq => Specification.definition (NONE, (apfst Binding.conceal Attrib.empty_binding, eq))) - |> snd - |> Class.prove_instantiation_exit (K (Class.intro_classes_tac [])) - end; - -fun ensure_random_typecopy tyco thy = - let - val SOME { vs = raw_vs, constr, typ = raw_T, ... } = - Typecopy.get_info thy tyco; - val constrain = curry (Sorts.inter_sort (Sign.classes_of thy)); - val T = map_atyps (fn TFree (v, sort) => - TFree (v, constrain sort @{sort random})) raw_T; - val vs' = Term.add_tfreesT T []; - val vs = map (fn (v, sort) => - (v, the_default (constrain sort @{sort typerep}) (AList.lookup (op =) vs' v))) raw_vs; - val can_inst = Sign.of_sort thy (T, @{sort random}); - in if can_inst then mk_random_typecopy tyco vs constr T thy else thy end; - - (** datatypes **) (* definitional scheme for random instances on datatypes *) -(*FIXME avoid this low-level proving*) local fun dest_ctyp_nth k cT = nth (Thm.dest_ctyp cT) k; @@ -450,8 +406,8 @@ (** setup **) -val setup = Typecopy.interpretation ensure_random_typecopy - #> Datatype.interpretation ensure_random_datatype +val setup = + Datatype.interpretation ensure_random_datatype #> Code_Target.extend_target (target, (Code_Eval.target, K I)) #> Quickcheck.add_generator ("code", compile_generator_expr o ProofContext.theory_of); diff -r 7eb0f6991e25 -r 001f2f44984c src/HOL/Tools/quickcheck_record.ML --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/HOL/Tools/quickcheck_record.ML Sat Aug 14 13:24:06 2010 +0200 @@ -0,0 +1,60 @@ +(* Title: HOL/Tools/quickcheck_record.ML + Author: Florian Haftmann, TU Muenchen + +Quickcheck generators for records. +*) + +signature QUICKCHECK_RECORD = +sig + val ensure_random_typecopy: string -> theory -> theory + val setup: theory -> theory +end; + +structure Quickcheck_Record : QUICKCHECK_RECORD = +struct + +fun termifyT T = HOLogic.mk_prodT (T, @{typ "unit => term"}) +val size = @{term "i::code_numeral"}; + +fun mk_random_typecopy tyco vs constr T' thy = + let + val mk_const = curry (Sign.mk_const thy); + val Ts = map TFree vs; + val T = Type (tyco, Ts); + val Tm = termifyT T; + val Tm' = termifyT T'; + val v = "x"; + val t_v = Free (v, Tm'); + val t_constr = Const (constr, T' --> T); + val lhs = HOLogic.mk_random T size; + val rhs = HOLogic.mk_ST [((HOLogic.mk_random T' size, @{typ Random.seed}), SOME (v, Tm'))] + (HOLogic.mk_return Tm @{typ Random.seed} + (mk_const "Code_Evaluation.valapp" [T', T] + $ HOLogic.mk_prod (t_constr, Abs ("u", @{typ unit}, HOLogic.reflect_term t_constr)) $ t_v)) + @{typ Random.seed} (SOME Tm, @{typ Random.seed}); + val eq = HOLogic.mk_Trueprop (HOLogic.mk_eq (lhs, rhs)); + in + thy + |> Class.instantiation ([tyco], vs, @{sort random}) + |> `(fn lthy => Syntax.check_term lthy eq) + |-> (fn eq => Specification.definition (NONE, (apfst Binding.conceal Attrib.empty_binding, eq))) + |> snd + |> Class.prove_instantiation_exit (K (Class.intro_classes_tac [])) + end; + +fun ensure_random_typecopy tyco thy = + let + val SOME { vs = raw_vs, constr, typ = raw_T, ... } = + Typecopy.get_info thy tyco; + val constrain = curry (Sorts.inter_sort (Sign.classes_of thy)); + val T = map_atyps (fn TFree (v, sort) => + TFree (v, constrain sort @{sort random})) raw_T; + val vs' = Term.add_tfreesT T []; + val vs = map (fn (v, sort) => + (v, the_default (constrain sort @{sort typerep}) (AList.lookup (op =) vs' v))) raw_vs; + val can_inst = Sign.of_sort thy (T, @{sort random}); + in if can_inst then mk_random_typecopy tyco vs constr T thy else thy end; + +val setup = Typecopy.interpretation ensure_random_typecopy; + +end; diff -r 7eb0f6991e25 -r 001f2f44984c src/HOL/Tools/record.ML --- a/src/HOL/Tools/record.ML Sat Aug 14 12:01:50 2010 +0200 +++ b/src/HOL/Tools/record.ML Sat Aug 14 13:24:06 2010 +0200 @@ -1217,7 +1217,7 @@ fun get_upd_acc_cong_thm upd acc thy simpset = let - val insts = [("upd", cterm_of thy upd), ("acc", cterm_of thy acc)]; + val insts = [("upd", cterm_of thy upd), ("ac", cterm_of thy acc)]; val prop = Thm.concl_of (named_cterm_instantiate insts updacc_cong_triv); in Goal.prove (ProofContext.init_global thy) [] [] prop diff -r 7eb0f6991e25 -r 001f2f44984c src/HOL/Tools/typedef.ML --- a/src/HOL/Tools/typedef.ML Sat Aug 14 12:01:50 2010 +0200 +++ b/src/HOL/Tools/typedef.ML Sat Aug 14 13:24:06 2010 +0200 @@ -268,7 +268,7 @@ in typedef_result inhabited lthy' end; fun add_typedef_global def opt_name typ set opt_morphs tac = - Named_Target.init NONE + Named_Target.theory_init #> add_typedef def opt_name typ set opt_morphs tac #> Local_Theory.exit_result_global (apsnd o transform_info); diff -r 7eb0f6991e25 -r 001f2f44984c src/HOL/Typedef.thy --- a/src/HOL/Typedef.thy Sat Aug 14 12:01:50 2010 +0200 +++ b/src/HOL/Typedef.thy Sat Aug 14 13:24:06 2010 +0200 @@ -8,7 +8,6 @@ imports Set uses ("Tools/typedef.ML") - ("Tools/typecopy.ML") ("Tools/typedef_codegen.ML") begin @@ -116,7 +115,6 @@ end use "Tools/typedef.ML" setup Typedef.setup -use "Tools/typecopy.ML" setup Typecopy.setup use "Tools/typedef_codegen.ML" setup TypedefCodegen.setup end diff -r 7eb0f6991e25 -r 001f2f44984c src/Pure/IsaMakefile --- a/src/Pure/IsaMakefile Sat Aug 14 12:01:50 2010 +0200 +++ b/src/Pure/IsaMakefile Sat Aug 14 13:24:06 2010 +0200 @@ -111,7 +111,7 @@ Isar/auto_bind.ML \ Isar/calculation.ML \ Isar/class.ML \ - Isar/class_target.ML \ + Isar/class_declaration.ML \ Isar/code.ML \ Isar/constdefs.ML \ Isar/context_rules.ML \ diff -r 7eb0f6991e25 -r 001f2f44984c src/Pure/Isar/class.ML --- a/src/Pure/Isar/class.ML Sat Aug 14 12:01:50 2010 +0200 +++ b/src/Pure/Isar/class.ML Sat Aug 14 13:24:06 2010 +0200 @@ -1,351 +1,640 @@ (* Title: Pure/Isar/class.ML Author: Florian Haftmann, TU Muenchen -Type classes derived from primitive axclasses and locales -- interfaces. +Type classes derived from primitive axclasses and locales. *) signature CLASS = sig - include CLASS_TARGET - (*FIXME the split into class_target.ML, named_target.ML and - class.ML is artificial*) + (*classes*) + val is_class: theory -> class -> bool + val these_params: theory -> sort -> (string * (class * (string * typ))) list + val base_sort: theory -> class -> sort + val rules: theory -> class -> thm option * thm + val these_defs: theory -> sort -> thm list + val these_operations: theory -> sort + -> (string * (class * (typ * term))) list + val print_classes: theory -> unit + val init: class -> theory -> Proof.context + val begin: class list -> sort -> Proof.context -> Proof.context + val const: class -> (binding * mixfix) * (term list * term) -> theory -> theory + val abbrev: class -> Syntax.mode -> (binding * mixfix) * term -> theory -> theory + val refresh_syntax: class -> Proof.context -> Proof.context + val redeclare_operations: theory -> sort -> Proof.context -> Proof.context + val class_prefix: string -> string + val register: class -> class list -> ((string * typ) * (string * typ)) list + -> sort -> morphism -> morphism -> thm option -> thm option -> thm + -> theory -> theory - val class: binding -> class list -> Element.context_i list - -> theory -> string * local_theory - val class_cmd: binding -> xstring list -> Element.context list - -> theory -> string * local_theory - val prove_subclass: tactic -> class -> local_theory -> local_theory - val subclass: class -> local_theory -> Proof.state - val subclass_cmd: xstring -> local_theory -> Proof.state + (*instances*) + val instantiation: string list * (string * sort) list * sort -> theory -> local_theory + val instantiation_instance: (local_theory -> local_theory) + -> local_theory -> Proof.state + val prove_instantiation_instance: (Proof.context -> tactic) + -> local_theory -> local_theory + val prove_instantiation_exit: (Proof.context -> tactic) + -> local_theory -> theory + val prove_instantiation_exit_result: (morphism -> 'a -> 'b) + -> (Proof.context -> 'b -> tactic) -> 'a -> local_theory -> 'b * theory + val read_multi_arity: theory -> xstring list * xstring list * xstring + -> string list * (string * sort) list * sort + val type_name: string -> string + val instantiation_cmd: xstring list * xstring list * xstring -> theory -> local_theory + val instance_arity_cmd: xstring list * xstring list * xstring -> theory -> Proof.state + + (*subclasses*) + val classrel: class * class -> theory -> Proof.state + val classrel_cmd: xstring * xstring -> theory -> Proof.state + val register_subclass: class * class -> morphism option -> Element.witness option + -> morphism -> theory -> theory + + (*tactics*) + val intro_classes_tac: thm list -> tactic + val default_intro_tac: Proof.context -> thm list -> tactic end; -structure Class : CLASS = +structure Class: CLASS = struct -open Class_Target; +(** class data **) + +datatype class_data = ClassData of { + + (* static part *) + consts: (string * string) list + (*locale parameter ~> constant name*), + base_sort: sort, + base_morph: morphism + (*static part of canonical morphism*), + export_morph: morphism, + assm_intro: thm option, + of_class: thm, + axiom: thm option, + + (* dynamic part *) + defs: thm list, + operations: (string * (class * (typ * term))) list + +}; + +fun make_class_data ((consts, base_sort, base_morph, export_morph, assm_intro, of_class, axiom), + (defs, operations)) = + ClassData { consts = consts, base_sort = base_sort, + base_morph = base_morph, export_morph = export_morph, assm_intro = assm_intro, + of_class = of_class, axiom = axiom, defs = defs, operations = operations }; +fun map_class_data f (ClassData { consts, base_sort, base_morph, export_morph, assm_intro, + of_class, axiom, defs, operations }) = + make_class_data (f ((consts, base_sort, base_morph, export_morph, assm_intro, of_class, axiom), + (defs, operations))); +fun merge_class_data _ (ClassData { consts = consts, + base_sort = base_sort, base_morph = base_morph, export_morph = export_morph, assm_intro = assm_intro, + of_class = of_class, axiom = axiom, defs = defs1, operations = operations1 }, + ClassData { consts = _, base_sort = _, base_morph = _, export_morph = _, assm_intro = _, + of_class = _, axiom = _, defs = defs2, operations = operations2 }) = + make_class_data ((consts, base_sort, base_morph, export_morph, assm_intro, of_class, axiom), + (Thm.merge_thms (defs1, defs2), + AList.merge (op =) (K true) (operations1, operations2))); + +structure ClassData = Theory_Data +( + type T = class_data Graph.T + val empty = Graph.empty; + val extend = I; + val merge = Graph.join merge_class_data; +); + + +(* queries *) + +fun lookup_class_data thy class = case try (Graph.get_node (ClassData.get thy)) class + of SOME (ClassData data) => SOME data + | NONE => NONE; + +fun the_class_data thy class = case lookup_class_data thy class + of NONE => error ("Undeclared class " ^ quote class) + | SOME data => data; + +val is_class = is_some oo lookup_class_data; + +val ancestry = Graph.all_succs o ClassData.get; +val heritage = Graph.all_preds o ClassData.get; + +fun these_params thy = + let + fun params class = + let + val const_typs = (#params o AxClass.get_info thy) class; + val const_names = (#consts o the_class_data thy) class; + in + (map o apsnd) + (fn c => (class, (c, (the o AList.lookup (op =) const_typs) c))) const_names + end; + in maps params o ancestry thy end; + +val base_sort = #base_sort oo the_class_data; + +fun rules thy class = + let val { axiom, of_class, ... } = the_class_data thy class + in (axiom, of_class) end; + +fun all_assm_intros thy = + Graph.fold (fn (_, (ClassData { assm_intro, ... }, _)) => fold (insert Thm.eq_thm) + (the_list assm_intro)) (ClassData.get thy) []; + +fun these_defs thy = maps (#defs o the_class_data thy) o ancestry thy; +fun these_operations thy = maps (#operations o the_class_data thy) o ancestry thy; + +val base_morphism = #base_morph oo the_class_data; +fun morphism thy class = case Element.eq_morphism thy (these_defs thy [class]) + of SOME eq_morph => base_morphism thy class $> eq_morph + | NONE => base_morphism thy class; +val export_morphism = #export_morph oo the_class_data; + +fun print_classes thy = + let + val ctxt = ProofContext.init_global thy; + val algebra = Sign.classes_of thy; + val arities = + Symtab.empty + |> Symtab.fold (fn (tyco, arities) => fold (fn (class, _) => + Symtab.map_default (class, []) (insert (op =) tyco)) arities) + (Sorts.arities_of algebra); + val the_arities = these o Symtab.lookup arities; + fun mk_arity class tyco = + let + val Ss = Sorts.mg_domain algebra tyco [class]; + in Syntax.pretty_arity ctxt (tyco, Ss, [class]) end; + fun mk_param (c, ty) = Pretty.str (Sign.extern_const thy c ^ " :: " + ^ setmp_CRITICAL show_sorts false (Syntax.string_of_typ ctxt o Type.strip_sorts) ty); + fun mk_entry class = (Pretty.block o Pretty.fbreaks o map_filter I) [ + (SOME o Pretty.str) ("class " ^ Sign.extern_class thy class ^ ":"), + (SOME o Pretty.block) [Pretty.str "supersort: ", + (Syntax.pretty_sort ctxt o Sign.minimize_sort thy o Sign.super_classes thy) class], + ((fn [] => NONE | ps => (SOME o Pretty.block o Pretty.fbreaks) + (Pretty.str "parameters:" :: ps)) o map mk_param + o these o Option.map #params o try (AxClass.get_info thy)) class, + (SOME o Pretty.block o Pretty.breaks) [ + Pretty.str "instances:", + Pretty.list "" "" (map (mk_arity class) (the_arities class)) + ] + ] + in + (Pretty.writeln o Pretty.chunks o separate (Pretty.str "") + o map mk_entry o Sorts.all_classes) algebra + end; + + +(* updaters *) + +fun register class sups params base_sort base_morph export_morph + axiom assm_intro of_class thy = + let + val operations = map (fn (v_ty as (_, ty), (c, _)) => + (c, (class, (ty, Free v_ty)))) params; + val add_class = Graph.new_node (class, + make_class_data (((map o pairself) fst params, base_sort, + base_morph, export_morph, assm_intro, of_class, axiom), ([], operations))) + #> fold (curry Graph.add_edge class) sups; + in ClassData.map add_class thy end; + +fun activate_defs class thms thy = case Element.eq_morphism thy thms + of SOME eq_morph => fold (fn cls => fn thy => + Context.theory_map (Locale.amend_registration (cls, base_morphism thy cls) + (eq_morph, true) (export_morphism thy cls)) thy) (heritage thy [class]) thy + | NONE => thy; -(** class definitions **) +fun register_operation class (c, (t, some_def)) thy = + let + val base_sort = base_sort thy class; + val prep_typ = map_type_tfree + (fn (v, sort) => if Name.aT = v + then TFree (v, base_sort) else TVar ((v, 0), sort)); + val t' = map_types prep_typ t; + val ty' = Term.fastype_of t'; + in + thy + |> (ClassData.map o Graph.map_node class o map_class_data o apsnd) + (fn (defs, operations) => + (fold cons (the_list some_def) defs, + (c, (class, (ty', t'))) :: operations)) + |> activate_defs class (the_list some_def) + end; + +fun register_subclass (sub, sup) some_dep_morph some_wit export thy = + let + val intros = (snd o rules thy) sup :: map_filter I + [Option.map (Drule.export_without_context_open o Element.conclude_witness) some_wit, + (fst o rules thy) sub]; + val tac = EVERY (map (TRYALL o Tactic.rtac) intros); + val classrel = Skip_Proof.prove_global thy [] [] (Logic.mk_classrel (sub, sup)) + (K tac); + val diff_sort = Sign.complete_sort thy [sup] + |> subtract (op =) (Sign.complete_sort thy [sub]) + |> filter (is_class thy); + val add_dependency = case some_dep_morph + of SOME dep_morph => Locale.add_dependency sub + (sup, dep_morph $> Element.satisfy_morphism (the_list some_wit)) export + | NONE => I + in + thy + |> AxClass.add_classrel classrel + |> ClassData.map (Graph.add_edge (sub, sup)) + |> activate_defs sub (these_defs thy diff_sort) + |> add_dependency + end; + + +(** classes and class target **) + +(* class context syntax *) + +fun these_unchecks thy = map (fn (c, (_, (ty, t))) => (t, Const (c, ty))) + o these_operations thy; + +fun redeclare_const thy c = + let val b = Long_Name.base_name c + in Sign.intern_const thy b = c ? Variable.declare_const (b, c) end; + +fun synchronize_class_syntax sort base_sort ctxt = + let + val thy = ProofContext.theory_of ctxt; + val algebra = Sign.classes_of thy; + val operations = these_operations thy sort; + fun subst_class_typ sort = map_type_tfree (K (TVar ((Name.aT, 0), sort))); + val primary_constraints = + (map o apsnd) (subst_class_typ base_sort o fst o snd) operations; + val secondary_constraints = + (map o apsnd) (fn (class, (ty, _)) => subst_class_typ [class] ty) operations; + fun improve (c, ty) = (case AList.lookup (op =) primary_constraints c + of SOME ty' => (case try (Type.raw_match (ty', ty)) Vartab.empty + of SOME tyenv => (case Vartab.lookup tyenv (Name.aT, 0) + of SOME (_, ty' as TVar (vi, sort)) => + if Type_Infer.is_param vi + andalso Sorts.sort_le algebra (base_sort, sort) + then SOME (ty', TFree (Name.aT, base_sort)) + else NONE + | _ => NONE) + | NONE => NONE) + | NONE => NONE) + fun subst (c, ty) = Option.map snd (AList.lookup (op =) operations c); + val unchecks = these_unchecks thy sort; + in + ctxt + |> fold (redeclare_const thy o fst) primary_constraints + |> Overloading.map_improvable_syntax (K (((primary_constraints, secondary_constraints), + (((improve, subst), true), unchecks)), false)) + |> Overloading.set_primary_constraints + end; + +fun refresh_syntax class ctxt = + let + val thy = ProofContext.theory_of ctxt; + val base_sort = base_sort thy class; + in synchronize_class_syntax [class] base_sort ctxt end; + +fun redeclare_operations thy sort = + fold (redeclare_const thy o fst) (these_operations thy sort); + +fun begin sort base_sort ctxt = + ctxt + |> Variable.declare_term + (Logic.mk_type (TFree (Name.aT, base_sort))) + |> synchronize_class_syntax sort base_sort + |> Overloading.add_improvable_syntax; + +fun init class thy = + thy + |> Locale.init class + |> begin [class] (base_sort thy class); + + +(* class target *) + +val class_prefix = Logic.const_of_class o Long_Name.base_name; + +fun const class ((c, mx), (type_params, dict)) thy = + let + val morph = morphism thy class; + val b = Morphism.binding morph c; + val b_def = Morphism.binding morph (Binding.suffix_name "_dict" b); + val c' = Sign.full_name thy b; + val dict' = Morphism.term morph dict; + val ty' = map Term.fastype_of type_params ---> Term.fastype_of dict'; + val def_eq = Logic.mk_equals (list_comb (Const (c', ty'), type_params), dict') + |> map_types Type.strip_sorts; + in + thy + |> Sign.declare_const ((b, Type.strip_sorts ty'), mx) + |> snd + |> Thm.add_def false false (b_def, def_eq) + |>> apsnd Thm.varifyT_global + |-> (fn (_, def_thm) => PureThy.store_thm (b_def, def_thm) + #> snd + #> null type_params ? register_operation class (c', (dict', SOME (Thm.symmetric def_thm)))) + |> Sign.add_const_constraint (c', SOME ty') + end; + +fun abbrev class prmode ((c, mx), rhs) thy = + let + val morph = morphism thy class; + val unchecks = these_unchecks thy [class]; + val b = Morphism.binding morph c; + val c' = Sign.full_name thy b; + val rhs' = Pattern.rewrite_term thy unchecks [] rhs; + val ty' = Term.fastype_of rhs'; + val rhs'' = map_types Logic.varifyT_global rhs'; + in + thy + |> Sign.add_abbrev (#1 prmode) (b, rhs'') + |> snd + |> Sign.add_const_constraint (c', SOME ty') + |> Sign.notation true prmode [(Const (c', ty'), mx)] + |> not (#1 prmode = Print_Mode.input) ? register_operation class (c', (rhs', NONE)) + end; + + +(* simple subclasses *) local -(* calculating class-related rules including canonical interpretation *) - -fun calculate thy class sups base_sort param_map assm_axiom = - let - val empty_ctxt = ProofContext.init_global thy; - - (* instantiation of canonical interpretation *) - val aT = TFree (Name.aT, base_sort); - val param_map_const = (map o apsnd) Const param_map; - val param_map_inst = (map o apsnd) - (Const o apsnd (map_atyps (K aT))) param_map; - val const_morph = Element.inst_morphism thy - (Symtab.empty, Symtab.make param_map_inst); - val typ_morph = Element.inst_morphism thy - (Symtab.empty |> Symtab.update (Name.aT, TFree (Name.aT, [class])), Symtab.empty); - val (([raw_props], [(_, raw_inst_morph)], export_morph), _) = empty_ctxt - |> Expression.cert_goal_expression ([(class, (("", false), - Expression.Named param_map_const))], []); - val (props, inst_morph) = if null param_map - then (raw_props |> map (Morphism.term typ_morph), - raw_inst_morph $> typ_morph) - else (raw_props, raw_inst_morph); (*FIXME proper handling in - locale.ML / expression.ML would be desirable*) - - (* witness for canonical interpretation *) - val prop = try the_single props; - val wit = Option.map (fn prop => let - val sup_axioms = map_filter (fst o rules thy) sups; - val loc_intro_tac = case Locale.intros_of thy class - of (_, NONE) => all_tac - | (_, SOME intro) => ALLGOALS (Tactic.rtac intro); - val tac = loc_intro_tac - THEN ALLGOALS (ProofContext.fact_tac (sup_axioms @ the_list assm_axiom)) - in Element.prove_witness empty_ctxt prop tac end) prop; - val axiom = Option.map Element.conclude_witness wit; - - (* canonical interpretation *) - val base_morph = inst_morph - $> Morphism.binding_morphism (Binding.prefix false (class_prefix class)) - $> Element.satisfy_morphism (the_list wit); - val eq_morph = Element.eq_morphism thy (these_defs thy sups); - - (* assm_intro *) - fun prove_assm_intro thm = - let - val ((_, [thm']), _) = Variable.import true [thm] empty_ctxt; - val const_eq_morph = case eq_morph - of SOME eq_morph => const_morph $> eq_morph - | NONE => const_morph - val thm'' = Morphism.thm const_eq_morph thm'; - val tac = ALLGOALS (ProofContext.fact_tac [thm'']); - in Skip_Proof.prove_global thy [] [] (Thm.prop_of thm'') (K tac) end; - val assm_intro = Option.map prove_assm_intro - (fst (Locale.intros_of thy class)); - - (* of_class *) - val of_class_prop_concl = Logic.mk_of_class (aT, class); - val of_class_prop = case prop of NONE => of_class_prop_concl - | SOME prop => Logic.mk_implies (Morphism.term const_morph - ((map_types o map_atyps) (K aT) prop), of_class_prop_concl); - val sup_of_classes = map (snd o rules thy) sups; - val loc_axiom_intros = map Drule.export_without_context_open (Locale.axioms_of thy class); - val axclass_intro = #intro (AxClass.get_info thy class); - val base_sort_trivs = Thm.of_sort (Thm.ctyp_of thy aT, base_sort); - val tac = REPEAT (SOMEGOAL - (Tactic.match_tac (axclass_intro :: sup_of_classes - @ loc_axiom_intros @ base_sort_trivs) - ORELSE' Tactic.assume_tac)); - val of_class = Skip_Proof.prove_global thy [] [] of_class_prop (K tac); - - in (base_morph, eq_morph, export_morph, axiom, assm_intro, of_class) end; - - -(* reading and processing class specifications *) - -fun prep_class_elems prep_decl thy sups raw_elems = +fun gen_classrel mk_prop classrel thy = let - - (* user space type system: only permits 'a type variable, improves towards 'a *) - val algebra = Sign.classes_of thy; - val inter_sort = curry (Sorts.inter_sort algebra); - val proto_base_sort = if null sups then Sign.defaultS thy - else fold inter_sort (map (base_sort thy) sups) []; - val base_constraints = (map o apsnd) - (map_type_tfree (K (TVar ((Name.aT, 0), proto_base_sort))) o fst o snd) - (these_operations thy sups); - val reject_bcd_etc = (map o map_atyps) (fn T as TFree (v, sort) => - if v = Name.aT then T - else error ("No type variable other than " ^ Name.aT ^ " allowed in class specification") - | T => T); - fun singleton_fixate Ts = - let - fun extract f = (fold o fold_atyps) f Ts []; - val tfrees = extract - (fn TFree (v, sort) => insert (op =) (v, sort) | _ => I); - val inferred_sort = extract - (fn TVar (_, sort) => inter_sort sort | _ => I); - val fixate_sort = if null tfrees then inferred_sort - else case tfrees - of [(_, a_sort)] => if Sorts.sort_le algebra (a_sort, inferred_sort) - then inter_sort a_sort inferred_sort - else error ("Type inference imposes additional sort constraint " - ^ Syntax.string_of_sort_global thy inferred_sort - ^ " of type parameter " ^ Name.aT ^ " of sort " - ^ Syntax.string_of_sort_global thy a_sort ^ ".") - | _ => error "Multiple type variables in class specification."; - in (map o map_atyps) (K (TFree (Name.aT, fixate_sort))) Ts end; - fun add_typ_check level name f = Context.proof_map - (Syntax.add_typ_check level name (fn xs => fn ctxt => - let val xs' = f xs in if eq_list (op =) (xs, xs') then NONE else SOME (xs', ctxt) end)); - - (* preprocessing elements, retrieving base sort from type-checked elements *) - val init_class_body = fold (ProofContext.add_const_constraint o apsnd SOME) base_constraints - #> redeclare_operations thy sups - #> add_typ_check 10 "reject_bcd_etc" reject_bcd_etc - #> add_typ_check ~10 "singleton_fixate" singleton_fixate; - val raw_supexpr = (map (fn sup => (sup, (("", false), - Expression.Positional []))) sups, []); - val ((raw_supparams, _, inferred_elems), _) = ProofContext.init_global thy - |> prep_decl raw_supexpr init_class_body raw_elems; - fun fold_element_types f (Element.Fixes fxs) = fold (fn (_, SOME T, _) => f T) fxs - | fold_element_types f (Element.Constrains cnstrs) = fold (f o snd) cnstrs - | fold_element_types f (Element.Assumes assms) = fold (fold (fn (t, ts) => - fold_types f t #> (fold o fold_types) f ts) o snd) assms - | fold_element_types f (Element.Defines _) = - error ("\"defines\" element not allowed in class specification.") - | fold_element_types f (Element.Notes _) = - error ("\"notes\" element not allowed in class specification."); - val base_sort = if null inferred_elems then proto_base_sort else - case (fold o fold_element_types) Term.add_tfreesT inferred_elems [] - of [] => error "No type variable in class specification" - | [(_, sort)] => sort - | _ => error "Multiple type variables in class specification"; - val supparams = map (fn ((c, T), _) => - (c, map_atyps (K (TFree (Name.aT, base_sort))) T)) raw_supparams; - val supparam_names = map fst supparams; - fun mk_param ((c, _), _) = Free (c, (the o AList.lookup (op =) supparams) c); - val supexpr = (map (fn sup => (sup, (("", false), - Expression.Positional (map (SOME o mk_param) (Locale.params_of thy sup))))) sups, - map (fn (c, T) => (Binding.name c, SOME T, NoSyn)) supparams); - - in (base_sort, supparam_names, supexpr, inferred_elems) end; - -val cert_class_elems = prep_class_elems Expression.cert_declaration; -val read_class_elems = prep_class_elems Expression.cert_read_declaration; - -fun prep_class_spec prep_class prep_class_elems thy raw_supclasses raw_elems = - let - - (* prepare import *) - val inter_sort = curry (Sorts.inter_sort (Sign.classes_of thy)); - val sups = map (prep_class thy) raw_supclasses - |> Sign.minimize_sort thy; - val _ = case filter_out (is_class thy) sups - of [] => () - | no_classes => error ("No (proper) classes: " ^ commas (map quote no_classes)); - val raw_supparams = (map o apsnd) (snd o snd) (these_params thy sups); - val raw_supparam_names = map fst raw_supparams; - val _ = if has_duplicates (op =) raw_supparam_names - then error ("Duplicate parameter(s) in superclasses: " - ^ (commas o map quote o duplicates (op =)) raw_supparam_names) - else (); - - (* infer types and base sort *) - val (base_sort, supparam_names, supexpr, inferred_elems) = - prep_class_elems thy sups raw_elems; - val sup_sort = inter_sort base_sort sups; - - (* process elements as class specification *) - val class_ctxt = begin sups base_sort (ProofContext.init_global thy); - val ((_, _, syntax_elems), _) = class_ctxt - |> Expression.cert_declaration supexpr I inferred_elems; - fun check_vars e vs = if null vs - then error ("No type variable in part of specification element " - ^ (Pretty.string_of o Pretty.chunks) (Element.pretty_ctxt class_ctxt e)) - else (); - fun check_element (e as Element.Fixes fxs) = - map (fn (_, SOME T, _) => check_vars e (Term.add_tfreesT T [])) fxs - | check_element (e as Element.Assumes assms) = - maps (fn (_, ts_pss) => map - (fn (t, _) => check_vars e (Term.add_tfrees t [])) ts_pss) assms - | check_element e = [()]; - val _ = map check_element syntax_elems; - fun fork_syn (Element.Fixes xs) = - fold_map (fn (c, ty, syn) => cons (c, syn) #> pair (c, ty, NoSyn)) xs - #>> Element.Fixes - | fork_syn x = pair x; - val (elems, global_syntax) = fold_map fork_syn syntax_elems []; - - in (((sups, supparam_names), (sup_sort, base_sort, supexpr)), (elems, global_syntax)) end; - -val cert_class_spec = prep_class_spec (K I) cert_class_elems; -val read_class_spec = prep_class_spec Sign.intern_class read_class_elems; - - -(* class establishment *) - -fun add_consts class base_sort sups supparam_names global_syntax thy = - let - (*FIXME simplify*) - val supconsts = supparam_names - |> AList.make (snd o the o AList.lookup (op =) (these_params thy sups)) - |> (map o apsnd o apsnd o map_atyps o K o TFree) (Name.aT, [class]); - val all_params = Locale.params_of thy class; - val raw_params = (snd o chop (length supparam_names)) all_params; - fun add_const ((raw_c, raw_ty), _) thy = - let - val b = Binding.name raw_c; - val c = Sign.full_name thy b; - val ty = map_atyps (K (TFree (Name.aT, base_sort))) raw_ty; - val ty0 = Type.strip_sorts ty; - val ty' = map_atyps (K (TFree (Name.aT, [class]))) ty0; - val syn = (the_default NoSyn o AList.lookup Binding.eq_name global_syntax) b; - in - thy - |> Sign.declare_const ((b, ty0), syn) - |> snd - |> pair ((Name.of_binding b, ty), (c, ty')) - end; + fun after_qed results = + ProofContext.theory ((fold o fold) AxClass.add_classrel results); in thy - |> Sign.add_path (class_prefix class) - |> fold_map add_const raw_params - ||> Sign.restore_naming thy - |-> (fn params => pair (supconsts @ (map o apfst) fst params, params)) - end; - -fun adjungate_axclass bname class base_sort sups supsort supparam_names global_syntax thy = - let - (*FIXME simplify*) - fun globalize param_map = map_aterms - (fn Free (v, ty) => Const ((fst o the o AList.lookup (op =) param_map) v, ty) - | t => t); - val raw_pred = Locale.intros_of thy class - |> fst - |> Option.map (Logic.unvarify_global o Logic.strip_imp_concl o Thm.prop_of); - fun get_axiom thy = case (#axioms o AxClass.get_info thy) class - of [] => NONE - | [thm] => SOME thm; - in - thy - |> add_consts class base_sort sups supparam_names global_syntax - |-> (fn (param_map, params) => AxClass.define_class (bname, supsort) - (map (fst o snd) params) - [(Thm.empty_binding, Option.map (globalize param_map) raw_pred |> the_list)] - #> snd - #> `get_axiom - #-> (fn assm_axiom => fold (Sign.add_const_constraint o apsnd SOME o snd) params - #> pair (param_map, params, assm_axiom))) - end; - -fun gen_class prep_class_spec b raw_supclasses raw_elems thy = - let - val class = Sign.full_name thy b; - val (((sups, supparam_names), (supsort, base_sort, supexpr)), (elems, global_syntax)) = - prep_class_spec thy raw_supclasses raw_elems; - in - thy - |> Expression.add_locale b (Binding.qualify true "class" b) supexpr elems - |> snd |> Local_Theory.exit_global - |> adjungate_axclass b class base_sort sups supsort supparam_names global_syntax - ||> Theory.checkpoint - |-> (fn (param_map, params, assm_axiom) => - `(fn thy => calculate thy class sups base_sort param_map assm_axiom) - #-> (fn (base_morph, eq_morph, export_morph, axiom, assm_intro, of_class) => - Context.theory_map (Locale.add_registration (class, base_morph) - (Option.map (rpair true) eq_morph) export_morph) - #> register class sups params base_sort base_morph export_morph axiom assm_intro of_class)) - |> Named_Target.init (SOME class) - |> pair class + |> ProofContext.init_global + |> Proof.theorem NONE after_qed [[(mk_prop thy classrel, [])]] end; in -val class = gen_class cert_class_spec; -val class_cmd = gen_class read_class_spec; +val classrel = + gen_classrel (Logic.mk_classrel oo AxClass.cert_classrel); +val classrel_cmd = + gen_classrel (Logic.mk_classrel oo AxClass.read_classrel); end; (*local*) -(** subclass relations **) +(** instantiation target **) + +(* bookkeeping *) + +datatype instantiation = Instantiation of { + arities: string list * (string * sort) list * sort, + params: ((string * string) * (string * typ)) list + (*(instantiation parameter, type constructor), (local instantiation parameter, typ)*) +} + +structure Instantiation = Proof_Data +( + type T = instantiation + fun init _ = Instantiation { arities = ([], [], []), params = [] }; +); + +fun mk_instantiation (arities, params) = + Instantiation { arities = arities, params = params }; +fun get_instantiation lthy = case Instantiation.get (Local_Theory.target_of lthy) + of Instantiation data => data; +fun map_instantiation f = (Local_Theory.target o Instantiation.map) + (fn Instantiation { arities, params } => mk_instantiation (f (arities, params))); -local +fun the_instantiation lthy = case get_instantiation lthy + of { arities = ([], [], []), ... } => error "No instantiation target" + | data => data; + +val instantiation_params = #params o get_instantiation; + +fun instantiation_param lthy b = instantiation_params lthy + |> find_first (fn (_, (v, _)) => Binding.name_of b = v) + |> Option.map (fst o fst); -fun gen_subclass prep_class do_proof raw_sup lthy = +fun read_multi_arity thy (raw_tycos, raw_sorts, raw_sort) = + let + val ctxt = ProofContext.init_global thy; + val all_arities = map (fn raw_tyco => ProofContext.read_arity ctxt + (raw_tyco, raw_sorts, raw_sort)) raw_tycos; + val tycos = map #1 all_arities; + val (_, sorts, sort) = hd all_arities; + val vs = Name.names Name.context Name.aT sorts; + in (tycos, vs, sort) end; + + +(* syntax *) + +fun synchronize_inst_syntax ctxt = let + val Instantiation { params, ... } = Instantiation.get ctxt; + + val lookup_inst_param = AxClass.lookup_inst_param + (Sign.consts_of (ProofContext.theory_of ctxt)) params; + fun subst (c, ty) = case lookup_inst_param (c, ty) + of SOME (v_ty as (_, ty)) => SOME (ty, Free v_ty) + | NONE => NONE; + val unchecks = + map (fn ((c, _), v_ty as (_, ty)) => (Free v_ty, Const (c, ty))) params; + in + ctxt + |> Overloading.map_improvable_syntax + (fn (((primary_constraints, _), (((improve, _), _), _)), _) => + (((primary_constraints, []), (((improve, subst), false), unchecks)), false)) + end; + +fun resort_terms pp algebra consts constraints ts = + let + fun matchings (Const (c_ty as (c, _))) = (case constraints c + of NONE => I + | SOME sorts => fold2 (curry (Sorts.meet_sort algebra)) + (Consts.typargs consts c_ty) sorts) + | matchings _ = I + val tvartab = (fold o fold_aterms) matchings ts Vartab.empty + handle Sorts.CLASS_ERROR e => error (Sorts.class_error pp e); + val inst = map_type_tvar + (fn (vi, sort) => TVar (vi, the_default sort (Vartab.lookup tvartab vi))); + in if Vartab.is_empty tvartab then NONE else SOME ((map o map_types) inst ts) end; + + +(* target *) + +val sanitize_name = (*necessary as long as "dirty" type identifiers are permitted*) + let + fun is_valid s = Symbol.is_ascii_letter s orelse Symbol.is_ascii_digit s + orelse s = "'" orelse s = "_"; + val is_junk = not o is_valid andf Symbol.is_regular; + val junk = Scan.many is_junk; + val scan_valids = Symbol.scanner "Malformed input" + ((junk |-- + (Scan.optional (Scan.one Symbol.is_ascii_letter) "x" ^^ (Scan.many is_valid >> implode) + --| junk)) + ::: Scan.repeat ((Scan.many1 is_valid >> implode) --| junk)); + in + explode #> scan_valids #> implode + end; + +val type_name = sanitize_name o Long_Name.base_name; + +fun define_overloaded (c, U) v (b_def, rhs) = Local_Theory.theory_result + (AxClass.declare_overloaded (c, U) ##>> AxClass.define_overloaded b_def (c, rhs)) + ##> (map_instantiation o apsnd) (filter_out (fn (_, (v', _)) => v' = v)) + ##> Local_Theory.target synchronize_inst_syntax; + +fun foundation (((b, U), mx), (b_def, rhs)) (type_params, term_params) lthy = + case instantiation_param lthy b + of SOME c => if mx <> NoSyn then error ("Illegal mixfix syntax for overloaded constant " ^ quote c) + else lthy |> define_overloaded (c, U) (Binding.name_of b) (b_def, rhs) + | NONE => lthy |> + Generic_Target.theory_foundation (((b, U), mx), (b_def, rhs)) (type_params, term_params); + +fun pretty lthy = + let + val { arities = (tycos, vs, sort), params } = the_instantiation lthy; val thy = ProofContext.theory_of lthy; - val proto_sup = prep_class thy raw_sup; - val proto_sub = case Named_Target.peek lthy - of {is_class = false, ...} => error "Not in a class context" - | {target, ...} => target; - val (sub, sup) = AxClass.cert_classrel thy (proto_sub, proto_sup); + fun pr_arity tyco = Syntax.pretty_arity lthy (tyco, map snd vs, sort); + fun pr_param ((c, _), (v, ty)) = + (Pretty.block o Pretty.breaks) [Pretty.str v, Pretty.str "==", + (Pretty.str o Sign.extern_const thy) c, Pretty.str "::", Syntax.pretty_typ_global thy ty]; + in Pretty.str "instantiation" :: map pr_arity tycos @ map pr_param params end; + +fun conclude lthy = + let + val (tycos, vs, sort) = (#arities o the_instantiation) lthy; + val thy = ProofContext.theory_of lthy; + val _ = map (fn tyco => if Sign.of_sort thy + (Type (tyco, map TFree vs), sort) + then () else error ("Missing instance proof for type " ^ quote (Sign.extern_type thy tyco))) + tycos; + in lthy end; - val expr = ([(sup, (("", false), Expression.Positional []))], []); - val (([props], deps, export), goal_ctxt) = - Expression.cert_goal_expression expr lthy; - val some_prop = try the_single props; - val some_dep_morph = try the_single (map snd deps); - fun after_qed some_wit = - ProofContext.theory (register_subclass (sub, sup) - some_dep_morph some_wit export) - #> ProofContext.theory_of #> Named_Target.init (SOME sub); - in do_proof after_qed some_prop goal_ctxt end; +fun instantiation (tycos, vs, sort) thy = + let + val _ = if null tycos then error "At least one arity must be given" else (); + val class_params = these_params thy (filter (can (AxClass.get_info thy)) sort); + fun get_param tyco (param, (_, (c, ty))) = + if can (AxClass.param_of_inst thy) (c, tyco) + then NONE else SOME ((c, tyco), + (param ^ "_" ^ type_name tyco, map_atyps (K (Type (tyco, map TFree vs))) ty)); + val params = map_product get_param tycos class_params |> map_filter I; + val primary_constraints = map (apsnd + (map_atyps (K (TVar ((Name.aT, 0), [])))) o snd o snd) class_params; + val pp = Syntax.pp_global thy; + val algebra = Sign.classes_of thy + |> fold (fn tyco => Sorts.add_arities pp + (tyco, map (fn class => (class, map snd vs)) sort)) tycos; + val consts = Sign.consts_of thy; + val improve_constraints = AList.lookup (op =) + (map (fn (_, (class, (c, _))) => (c, [[class]])) class_params); + fun resort_check ts ctxt = case resort_terms (Syntax.pp ctxt) algebra consts improve_constraints ts + of NONE => NONE + | SOME ts' => SOME (ts', ctxt); + val lookup_inst_param = AxClass.lookup_inst_param consts params; + val typ_instance = Type.typ_instance (Sign.tsig_of thy); + fun improve (c, ty) = case lookup_inst_param (c, ty) + of SOME (_, ty') => if typ_instance (ty', ty) then SOME (ty, ty') else NONE + | NONE => NONE; + in + thy + |> Theory.checkpoint + |> ProofContext.init_global + |> Instantiation.put (mk_instantiation ((tycos, vs, sort), params)) + |> fold (Variable.declare_typ o TFree) vs + |> fold (Variable.declare_names o Free o snd) params + |> (Overloading.map_improvable_syntax o apfst) + (K ((primary_constraints, []), (((improve, K NONE), false), []))) + |> Overloading.add_improvable_syntax + |> Context.proof_map (Syntax.add_term_check 0 "resorting" resort_check) + |> synchronize_inst_syntax + |> Local_Theory.init NONE "" + {define = Generic_Target.define foundation, + notes = Generic_Target.notes + (fn kind => fn global_facts => fn _ => Generic_Target.theory_notes kind global_facts), + abbrev = Generic_Target.abbrev + (fn prmode => fn (b, mx) => fn (t, _) => fn _ => Generic_Target.theory_abbrev prmode ((b, mx), t)), + declaration = K Generic_Target.theory_declaration, + syntax_declaration = K Generic_Target.theory_declaration, + pretty = pretty, + exit = Local_Theory.target_of o conclude} + end; + +fun instantiation_cmd arities thy = + instantiation (read_multi_arity thy arities) thy; + +fun gen_instantiation_instance do_proof after_qed lthy = + let + val (tycos, vs, sort) = (#arities o the_instantiation) lthy; + val arities_proof = maps (fn tyco => Logic.mk_arities (tyco, map snd vs, sort)) tycos; + fun after_qed' results = + Local_Theory.theory (fold (AxClass.add_arity o Thm.varifyT_global) results) + #> after_qed; + in + lthy + |> do_proof after_qed' arities_proof + end; -fun user_proof after_qed some_prop = - Element.witness_proof (after_qed o try the_single o the_single) - [the_list some_prop]; +val instantiation_instance = gen_instantiation_instance (fn after_qed => fn ts => + Proof.theorem NONE (after_qed o map the_single) (map (fn t => [(t, [])]) ts)); + +fun prove_instantiation_instance tac = gen_instantiation_instance (fn after_qed => + fn ts => fn lthy => after_qed (map (fn t => Goal.prove lthy [] [] t + (fn {context, ...} => tac context)) ts) lthy) I; + +fun prove_instantiation_exit tac = prove_instantiation_instance tac + #> Local_Theory.exit_global; -fun tactic_proof tac after_qed some_prop ctxt = - after_qed (Option.map - (fn prop => Element.prove_witness ctxt prop tac) some_prop) ctxt; +fun prove_instantiation_exit_result f tac x lthy = + let + val morph = ProofContext.export_morphism lthy + (ProofContext.init_global (ProofContext.theory_of lthy)); + val y = f morph x; + in + lthy + |> prove_instantiation_exit (fn ctxt => tac ctxt y) + |> pair y + end; + + +(* simplified instantiation interface with no class parameter *) -in +fun instance_arity_cmd raw_arities thy = + let + val (tycos, vs, sort) = read_multi_arity thy raw_arities; + val sorts = map snd vs; + val arities = maps (fn tyco => Logic.mk_arities (tyco, sorts, sort)) tycos; + fun after_qed results = ProofContext.theory + ((fold o fold) AxClass.add_arity results); + in + thy + |> ProofContext.init_global + |> Proof.theorem NONE after_qed (map (fn t => [(t, [])]) arities) + end; + + +(** tactics and methods **) -val subclass = gen_subclass (K I) user_proof; -fun prove_subclass tac = gen_subclass (K I) (tactic_proof tac); -val subclass_cmd = gen_subclass (ProofContext.read_class o ProofContext.init_global) user_proof; +fun intro_classes_tac facts st = + let + val thy = Thm.theory_of_thm st; + val classes = Sign.all_classes thy; + val class_trivs = map (Thm.class_triv thy) classes; + val class_intros = map_filter (try (#intro o AxClass.get_info thy)) classes; + val assm_intros = all_assm_intros thy; + in + Method.intros_tac (class_trivs @ class_intros @ assm_intros) facts st + end; -end; (*local*) +fun default_intro_tac ctxt [] = + intro_classes_tac [] ORELSE Locale.intro_locales_tac true ctxt [] + | default_intro_tac _ _ = no_tac; + +fun default_tac rules ctxt facts = + HEADGOAL (Method.some_rule_tac rules ctxt facts) ORELSE + default_intro_tac ctxt facts; + +val _ = Context.>> (Context.map_theory + (Method.setup (Binding.name "intro_classes") (Scan.succeed (K (METHOD intro_classes_tac))) + "back-chain introduction rules of classes" #> + Method.setup (Binding.name "default") (Attrib.thms >> (METHOD oo default_tac)) + "apply some intro/elim rule")); end; + diff -r 7eb0f6991e25 -r 001f2f44984c src/Pure/Isar/class_declaration.ML --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/Pure/Isar/class_declaration.ML Sat Aug 14 13:24:06 2010 +0200 @@ -0,0 +1,345 @@ +(* Title: Pure/Isar/class_declaration.ML + Author: Florian Haftmann, TU Muenchen + +Declaring classes and subclass relations. +*) + +signature CLASS_DECLARATION = +sig + val class: binding -> class list -> Element.context_i list + -> theory -> string * local_theory + val class_cmd: binding -> xstring list -> Element.context list + -> theory -> string * local_theory + val prove_subclass: tactic -> class -> local_theory -> local_theory + val subclass: class -> local_theory -> Proof.state + val subclass_cmd: xstring -> local_theory -> Proof.state +end; + +structure Class_Declaration: CLASS_DECLARATION = +struct + +(** class definitions **) + +local + +(* calculating class-related rules including canonical interpretation *) + +fun calculate thy class sups base_sort param_map assm_axiom = + let + val empty_ctxt = ProofContext.init_global thy; + + (* instantiation of canonical interpretation *) + val aT = TFree (Name.aT, base_sort); + val param_map_const = (map o apsnd) Const param_map; + val param_map_inst = (map o apsnd) + (Const o apsnd (map_atyps (K aT))) param_map; + val const_morph = Element.inst_morphism thy + (Symtab.empty, Symtab.make param_map_inst); + val typ_morph = Element.inst_morphism thy + (Symtab.empty |> Symtab.update (Name.aT, TFree (Name.aT, [class])), Symtab.empty); + val (([raw_props], [(_, raw_inst_morph)], export_morph), _) = empty_ctxt + |> Expression.cert_goal_expression ([(class, (("", false), + Expression.Named param_map_const))], []); + val (props, inst_morph) = if null param_map + then (raw_props |> map (Morphism.term typ_morph), + raw_inst_morph $> typ_morph) + else (raw_props, raw_inst_morph); (*FIXME proper handling in + locale.ML / expression.ML would be desirable*) + + (* witness for canonical interpretation *) + val prop = try the_single props; + val wit = Option.map (fn prop => let + val sup_axioms = map_filter (fst o Class.rules thy) sups; + val loc_intro_tac = case Locale.intros_of thy class + of (_, NONE) => all_tac + | (_, SOME intro) => ALLGOALS (Tactic.rtac intro); + val tac = loc_intro_tac + THEN ALLGOALS (ProofContext.fact_tac (sup_axioms @ the_list assm_axiom)) + in Element.prove_witness empty_ctxt prop tac end) prop; + val axiom = Option.map Element.conclude_witness wit; + + (* canonical interpretation *) + val base_morph = inst_morph + $> Morphism.binding_morphism (Binding.prefix false (Class.class_prefix class)) + $> Element.satisfy_morphism (the_list wit); + val eq_morph = Element.eq_morphism thy (Class.these_defs thy sups); + + (* assm_intro *) + fun prove_assm_intro thm = + let + val ((_, [thm']), _) = Variable.import true [thm] empty_ctxt; + val const_eq_morph = case eq_morph + of SOME eq_morph => const_morph $> eq_morph + | NONE => const_morph + val thm'' = Morphism.thm const_eq_morph thm'; + val tac = ALLGOALS (ProofContext.fact_tac [thm'']); + in Skip_Proof.prove_global thy [] [] (Thm.prop_of thm'') (K tac) end; + val assm_intro = Option.map prove_assm_intro + (fst (Locale.intros_of thy class)); + + (* of_class *) + val of_class_prop_concl = Logic.mk_of_class (aT, class); + val of_class_prop = case prop of NONE => of_class_prop_concl + | SOME prop => Logic.mk_implies (Morphism.term const_morph + ((map_types o map_atyps) (K aT) prop), of_class_prop_concl); + val sup_of_classes = map (snd o Class.rules thy) sups; + val loc_axiom_intros = map Drule.export_without_context_open (Locale.axioms_of thy class); + val axclass_intro = #intro (AxClass.get_info thy class); + val base_sort_trivs = Thm.of_sort (Thm.ctyp_of thy aT, base_sort); + val tac = REPEAT (SOMEGOAL + (Tactic.match_tac (axclass_intro :: sup_of_classes + @ loc_axiom_intros @ base_sort_trivs) + ORELSE' Tactic.assume_tac)); + val of_class = Skip_Proof.prove_global thy [] [] of_class_prop (K tac); + + in (base_morph, eq_morph, export_morph, axiom, assm_intro, of_class) end; + + +(* reading and processing class specifications *) + +fun prep_class_elems prep_decl thy sups raw_elems = + let + + (* user space type system: only permits 'a type variable, improves towards 'a *) + val algebra = Sign.classes_of thy; + val inter_sort = curry (Sorts.inter_sort algebra); + val proto_base_sort = if null sups then Sign.defaultS thy + else fold inter_sort (map (Class.base_sort thy) sups) []; + val base_constraints = (map o apsnd) + (map_type_tfree (K (TVar ((Name.aT, 0), proto_base_sort))) o fst o snd) + (Class.these_operations thy sups); + val reject_bcd_etc = (map o map_atyps) (fn T as TFree (v, sort) => + if v = Name.aT then T + else error ("No type variable other than " ^ Name.aT ^ " allowed in class specification") + | T => T); + fun singleton_fixate Ts = + let + fun extract f = (fold o fold_atyps) f Ts []; + val tfrees = extract + (fn TFree (v, sort) => insert (op =) (v, sort) | _ => I); + val inferred_sort = extract + (fn TVar (_, sort) => inter_sort sort | _ => I); + val fixate_sort = if null tfrees then inferred_sort + else case tfrees + of [(_, a_sort)] => if Sorts.sort_le algebra (a_sort, inferred_sort) + then inter_sort a_sort inferred_sort + else error ("Type inference imposes additional sort constraint " + ^ Syntax.string_of_sort_global thy inferred_sort + ^ " of type parameter " ^ Name.aT ^ " of sort " + ^ Syntax.string_of_sort_global thy a_sort ^ ".") + | _ => error "Multiple type variables in class specification."; + in (map o map_atyps) (K (TFree (Name.aT, fixate_sort))) Ts end; + fun add_typ_check level name f = Context.proof_map + (Syntax.add_typ_check level name (fn xs => fn ctxt => + let val xs' = f xs in if eq_list (op =) (xs, xs') then NONE else SOME (xs', ctxt) end)); + + (* preprocessing elements, retrieving base sort from type-checked elements *) + val init_class_body = fold (ProofContext.add_const_constraint o apsnd SOME) base_constraints + #> Class.redeclare_operations thy sups + #> add_typ_check 10 "reject_bcd_etc" reject_bcd_etc + #> add_typ_check ~10 "singleton_fixate" singleton_fixate; + val raw_supexpr = (map (fn sup => (sup, (("", false), + Expression.Positional []))) sups, []); + val ((raw_supparams, _, inferred_elems), _) = ProofContext.init_global thy + |> prep_decl raw_supexpr init_class_body raw_elems; + fun fold_element_types f (Element.Fixes fxs) = fold (fn (_, SOME T, _) => f T) fxs + | fold_element_types f (Element.Constrains cnstrs) = fold (f o snd) cnstrs + | fold_element_types f (Element.Assumes assms) = fold (fold (fn (t, ts) => + fold_types f t #> (fold o fold_types) f ts) o snd) assms + | fold_element_types f (Element.Defines _) = + error ("\"defines\" element not allowed in class specification.") + | fold_element_types f (Element.Notes _) = + error ("\"notes\" element not allowed in class specification."); + val base_sort = if null inferred_elems then proto_base_sort else + case (fold o fold_element_types) Term.add_tfreesT inferred_elems [] + of [] => error "No type variable in class specification" + | [(_, sort)] => sort + | _ => error "Multiple type variables in class specification"; + val supparams = map (fn ((c, T), _) => + (c, map_atyps (K (TFree (Name.aT, base_sort))) T)) raw_supparams; + val supparam_names = map fst supparams; + fun mk_param ((c, _), _) = Free (c, (the o AList.lookup (op =) supparams) c); + val supexpr = (map (fn sup => (sup, (("", false), + Expression.Positional (map (SOME o mk_param) (Locale.params_of thy sup))))) sups, + map (fn (c, T) => (Binding.name c, SOME T, NoSyn)) supparams); + + in (base_sort, supparam_names, supexpr, inferred_elems) end; + +val cert_class_elems = prep_class_elems Expression.cert_declaration; +val read_class_elems = prep_class_elems Expression.cert_read_declaration; + +fun prep_class_spec prep_class prep_class_elems thy raw_supclasses raw_elems = + let + + (* prepare import *) + val inter_sort = curry (Sorts.inter_sort (Sign.classes_of thy)); + val sups = map (prep_class thy) raw_supclasses + |> Sign.minimize_sort thy; + val _ = case filter_out (Class.is_class thy) sups + of [] => () + | no_classes => error ("No (proper) classes: " ^ commas (map quote no_classes)); + val raw_supparams = (map o apsnd) (snd o snd) (Class.these_params thy sups); + val raw_supparam_names = map fst raw_supparams; + val _ = if has_duplicates (op =) raw_supparam_names + then error ("Duplicate parameter(s) in superclasses: " + ^ (commas o map quote o duplicates (op =)) raw_supparam_names) + else (); + + (* infer types and base sort *) + val (base_sort, supparam_names, supexpr, inferred_elems) = + prep_class_elems thy sups raw_elems; + val sup_sort = inter_sort base_sort sups; + + (* process elements as class specification *) + val class_ctxt = Class.begin sups base_sort (ProofContext.init_global thy); + val ((_, _, syntax_elems), _) = class_ctxt + |> Expression.cert_declaration supexpr I inferred_elems; + fun check_vars e vs = if null vs + then error ("No type variable in part of specification element " + ^ (Pretty.string_of o Pretty.chunks) (Element.pretty_ctxt class_ctxt e)) + else (); + fun check_element (e as Element.Fixes fxs) = + map (fn (_, SOME T, _) => check_vars e (Term.add_tfreesT T [])) fxs + | check_element (e as Element.Assumes assms) = + maps (fn (_, ts_pss) => map + (fn (t, _) => check_vars e (Term.add_tfrees t [])) ts_pss) assms + | check_element e = [()]; + val _ = map check_element syntax_elems; + fun fork_syn (Element.Fixes xs) = + fold_map (fn (c, ty, syn) => cons (c, syn) #> pair (c, ty, NoSyn)) xs + #>> Element.Fixes + | fork_syn x = pair x; + val (elems, global_syntax) = fold_map fork_syn syntax_elems []; + + in (((sups, supparam_names), (sup_sort, base_sort, supexpr)), (elems, global_syntax)) end; + +val cert_class_spec = prep_class_spec (K I) cert_class_elems; +val read_class_spec = prep_class_spec Sign.intern_class read_class_elems; + + +(* class establishment *) + +fun add_consts class base_sort sups supparam_names global_syntax thy = + let + (*FIXME simplify*) + val supconsts = supparam_names + |> AList.make (snd o the o AList.lookup (op =) (Class.these_params thy sups)) + |> (map o apsnd o apsnd o map_atyps o K o TFree) (Name.aT, [class]); + val all_params = Locale.params_of thy class; + val raw_params = (snd o chop (length supparam_names)) all_params; + fun add_const ((raw_c, raw_ty), _) thy = + let + val b = Binding.name raw_c; + val c = Sign.full_name thy b; + val ty = map_atyps (K (TFree (Name.aT, base_sort))) raw_ty; + val ty0 = Type.strip_sorts ty; + val ty' = map_atyps (K (TFree (Name.aT, [class]))) ty0; + val syn = (the_default NoSyn o AList.lookup Binding.eq_name global_syntax) b; + in + thy + |> Sign.declare_const ((b, ty0), syn) + |> snd + |> pair ((Name.of_binding b, ty), (c, ty')) + end; + in + thy + |> Sign.add_path (Class.class_prefix class) + |> fold_map add_const raw_params + ||> Sign.restore_naming thy + |-> (fn params => pair (supconsts @ (map o apfst) fst params, params)) + end; + +fun adjungate_axclass bname class base_sort sups supsort supparam_names global_syntax thy = + let + (*FIXME simplify*) + fun globalize param_map = map_aterms + (fn Free (v, ty) => Const ((fst o the o AList.lookup (op =) param_map) v, ty) + | t => t); + val raw_pred = Locale.intros_of thy class + |> fst + |> Option.map (Logic.unvarify_global o Logic.strip_imp_concl o Thm.prop_of); + fun get_axiom thy = case (#axioms o AxClass.get_info thy) class + of [] => NONE + | [thm] => SOME thm; + in + thy + |> add_consts class base_sort sups supparam_names global_syntax + |-> (fn (param_map, params) => AxClass.define_class (bname, supsort) + (map (fst o snd) params) + [(Thm.empty_binding, Option.map (globalize param_map) raw_pred |> the_list)] + #> snd + #> `get_axiom + #-> (fn assm_axiom => fold (Sign.add_const_constraint o apsnd SOME o snd) params + #> pair (param_map, params, assm_axiom))) + end; + +fun gen_class prep_class_spec b raw_supclasses raw_elems thy = + let + val class = Sign.full_name thy b; + val (((sups, supparam_names), (supsort, base_sort, supexpr)), (elems, global_syntax)) = + prep_class_spec thy raw_supclasses raw_elems; + in + thy + |> Expression.add_locale b (Binding.qualify true "class" b) supexpr elems + |> snd |> Local_Theory.exit_global + |> adjungate_axclass b class base_sort sups supsort supparam_names global_syntax + ||> Theory.checkpoint + |-> (fn (param_map, params, assm_axiom) => + `(fn thy => calculate thy class sups base_sort param_map assm_axiom) + #-> (fn (base_morph, eq_morph, export_morph, axiom, assm_intro, of_class) => + Context.theory_map (Locale.add_registration (class, base_morph) + (Option.map (rpair true) eq_morph) export_morph) + #> Class.register class sups params base_sort base_morph export_morph axiom assm_intro of_class)) + |> Named_Target.init class + |> pair class + end; + +in + +val class = gen_class cert_class_spec; +val class_cmd = gen_class read_class_spec; + +end; (*local*) + + +(** subclass relations **) + +local + +fun gen_subclass prep_class do_proof raw_sup lthy = + let + val thy = ProofContext.theory_of lthy; + val proto_sup = prep_class thy raw_sup; + val proto_sub = case Named_Target.peek lthy + of SOME {target, is_class = true, ...} => target + | _ => error "Not in a class target"; + val (sub, sup) = AxClass.cert_classrel thy (proto_sub, proto_sup); + + val expr = ([(sup, (("", false), Expression.Positional []))], []); + val (([props], deps, export), goal_ctxt) = + Expression.cert_goal_expression expr lthy; + val some_prop = try the_single props; + val some_dep_morph = try the_single (map snd deps); + fun after_qed some_wit = + ProofContext.theory (Class.register_subclass (sub, sup) + some_dep_morph some_wit export) + #> ProofContext.theory_of #> Named_Target.init sub; + in do_proof after_qed some_prop goal_ctxt end; + +fun user_proof after_qed some_prop = + Element.witness_proof (after_qed o try the_single o the_single) + [the_list some_prop]; + +fun tactic_proof tac after_qed some_prop ctxt = + after_qed (Option.map + (fn prop => Element.prove_witness ctxt prop tac) some_prop) ctxt; + +in + +val subclass = gen_subclass (K I) user_proof; +fun prove_subclass tac = gen_subclass (K I) (tactic_proof tac); +val subclass_cmd = gen_subclass (ProofContext.read_class o ProofContext.init_global) user_proof; + +end; (*local*) + +end; diff -r 7eb0f6991e25 -r 001f2f44984c src/Pure/Isar/class_target.ML --- a/src/Pure/Isar/class_target.ML Sat Aug 14 12:01:50 2010 +0200 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,659 +0,0 @@ -(* Title: Pure/Isar/class_target.ML - Author: Florian Haftmann, TU Muenchen - -Type classes derived from primitive axclasses and locales -- mechanisms. -*) - -signature CLASS_TARGET = -sig - (*classes*) - val register: class -> class list -> ((string * typ) * (string * typ)) list - -> sort -> morphism -> morphism -> thm option -> thm option -> thm - -> theory -> theory - - val is_class: theory -> class -> bool - val base_sort: theory -> class -> sort - val rules: theory -> class -> thm option * thm - val these_params: theory -> sort -> (string * (class * (string * typ))) list - val these_defs: theory -> sort -> thm list - val these_operations: theory -> sort - -> (string * (class * (typ * term))) list - val print_classes: theory -> unit - - val begin: class list -> sort -> Proof.context -> Proof.context - val init: class -> theory -> Proof.context - val declare: class -> (binding * mixfix) * (term list * term) -> theory -> theory - val abbrev: class -> Syntax.mode -> (binding * mixfix) * term -> theory -> theory - val class_prefix: string -> string - val refresh_syntax: class -> Proof.context -> Proof.context - val redeclare_operations: theory -> sort -> Proof.context -> Proof.context - - (*instances*) - val init_instantiation: string list * (string * sort) list * sort - -> theory -> Proof.context - val instance_arity_cmd: xstring list * xstring list * xstring -> theory -> Proof.state - val instantiation_instance: (local_theory -> local_theory) - -> local_theory -> Proof.state - val prove_instantiation_instance: (Proof.context -> tactic) - -> local_theory -> local_theory - val prove_instantiation_exit: (Proof.context -> tactic) - -> local_theory -> theory - val prove_instantiation_exit_result: (morphism -> 'a -> 'b) - -> (Proof.context -> 'b -> tactic) -> 'a -> local_theory -> 'b * theory - val conclude_instantiation: local_theory -> local_theory - val instantiation_param: local_theory -> binding -> string option - val confirm_declaration: binding -> local_theory -> local_theory - val pretty_instantiation: local_theory -> Pretty.T - val read_multi_arity: theory -> xstring list * xstring list * xstring - -> string list * (string * sort) list * sort - val type_name: string -> string - val instantiation: string list * (string * sort) list * sort -> theory -> local_theory - val instantiation_cmd: xstring list * xstring list * xstring -> theory -> local_theory - - (*subclasses*) - val register_subclass: class * class -> morphism option -> Element.witness option - -> morphism -> theory -> theory - val classrel: class * class -> theory -> Proof.state - val classrel_cmd: xstring * xstring -> theory -> Proof.state - - (*tactics*) - val intro_classes_tac: thm list -> tactic - val default_intro_tac: Proof.context -> thm list -> tactic -end; - -structure Class_Target : CLASS_TARGET = -struct - -(** class data **) - -datatype class_data = ClassData of { - - (* static part *) - consts: (string * string) list - (*locale parameter ~> constant name*), - base_sort: sort, - base_morph: morphism - (*static part of canonical morphism*), - export_morph: morphism, - assm_intro: thm option, - of_class: thm, - axiom: thm option, - - (* dynamic part *) - defs: thm list, - operations: (string * (class * (typ * term))) list - -}; - -fun make_class_data ((consts, base_sort, base_morph, export_morph, assm_intro, of_class, axiom), - (defs, operations)) = - ClassData { consts = consts, base_sort = base_sort, - base_morph = base_morph, export_morph = export_morph, assm_intro = assm_intro, - of_class = of_class, axiom = axiom, defs = defs, operations = operations }; -fun map_class_data f (ClassData { consts, base_sort, base_morph, export_morph, assm_intro, - of_class, axiom, defs, operations }) = - make_class_data (f ((consts, base_sort, base_morph, export_morph, assm_intro, of_class, axiom), - (defs, operations))); -fun merge_class_data _ (ClassData { consts = consts, - base_sort = base_sort, base_morph = base_morph, export_morph = export_morph, assm_intro = assm_intro, - of_class = of_class, axiom = axiom, defs = defs1, operations = operations1 }, - ClassData { consts = _, base_sort = _, base_morph = _, export_morph = _, assm_intro = _, - of_class = _, axiom = _, defs = defs2, operations = operations2 }) = - make_class_data ((consts, base_sort, base_morph, export_morph, assm_intro, of_class, axiom), - (Thm.merge_thms (defs1, defs2), - AList.merge (op =) (K true) (operations1, operations2))); - -structure ClassData = Theory_Data -( - type T = class_data Graph.T - val empty = Graph.empty; - val extend = I; - val merge = Graph.join merge_class_data; -); - - -(* queries *) - -fun lookup_class_data thy class = case try (Graph.get_node (ClassData.get thy)) class - of SOME (ClassData data) => SOME data - | NONE => NONE; - -fun the_class_data thy class = case lookup_class_data thy class - of NONE => error ("Undeclared class " ^ quote class) - | SOME data => data; - -val is_class = is_some oo lookup_class_data; - -val ancestry = Graph.all_succs o ClassData.get; -val heritage = Graph.all_preds o ClassData.get; - -fun these_params thy = - let - fun params class = - let - val const_typs = (#params o AxClass.get_info thy) class; - val const_names = (#consts o the_class_data thy) class; - in - (map o apsnd) - (fn c => (class, (c, (the o AList.lookup (op =) const_typs) c))) const_names - end; - in maps params o ancestry thy end; - -val base_sort = #base_sort oo the_class_data; - -fun rules thy class = - let val { axiom, of_class, ... } = the_class_data thy class - in (axiom, of_class) end; - -fun all_assm_intros thy = - Graph.fold (fn (_, (ClassData { assm_intro, ... }, _)) => fold (insert Thm.eq_thm) - (the_list assm_intro)) (ClassData.get thy) []; - -fun these_defs thy = maps (#defs o the_class_data thy) o ancestry thy; -fun these_operations thy = maps (#operations o the_class_data thy) o ancestry thy; - -val base_morphism = #base_morph oo the_class_data; -fun morphism thy class = case Element.eq_morphism thy (these_defs thy [class]) - of SOME eq_morph => base_morphism thy class $> eq_morph - | NONE => base_morphism thy class; -val export_morphism = #export_morph oo the_class_data; - -fun print_classes thy = - let - val ctxt = ProofContext.init_global thy; - val algebra = Sign.classes_of thy; - val arities = - Symtab.empty - |> Symtab.fold (fn (tyco, arities) => fold (fn (class, _) => - Symtab.map_default (class, []) (insert (op =) tyco)) arities) - (Sorts.arities_of algebra); - val the_arities = these o Symtab.lookup arities; - fun mk_arity class tyco = - let - val Ss = Sorts.mg_domain algebra tyco [class]; - in Syntax.pretty_arity ctxt (tyco, Ss, [class]) end; - fun mk_param (c, ty) = Pretty.str (Sign.extern_const thy c ^ " :: " - ^ setmp_CRITICAL show_sorts false (Syntax.string_of_typ ctxt o Type.strip_sorts) ty); - fun mk_entry class = (Pretty.block o Pretty.fbreaks o map_filter I) [ - (SOME o Pretty.str) ("class " ^ Sign.extern_class thy class ^ ":"), - (SOME o Pretty.block) [Pretty.str "supersort: ", - (Syntax.pretty_sort ctxt o Sign.minimize_sort thy o Sign.super_classes thy) class], - ((fn [] => NONE | ps => (SOME o Pretty.block o Pretty.fbreaks) - (Pretty.str "parameters:" :: ps)) o map mk_param - o these o Option.map #params o try (AxClass.get_info thy)) class, - (SOME o Pretty.block o Pretty.breaks) [ - Pretty.str "instances:", - Pretty.list "" "" (map (mk_arity class) (the_arities class)) - ] - ] - in - (Pretty.writeln o Pretty.chunks o separate (Pretty.str "") - o map mk_entry o Sorts.all_classes) algebra - end; - - -(* updaters *) - -fun register class sups params base_sort base_morph export_morph - axiom assm_intro of_class thy = - let - val operations = map (fn (v_ty as (_, ty), (c, _)) => - (c, (class, (ty, Free v_ty)))) params; - val add_class = Graph.new_node (class, - make_class_data (((map o pairself) fst params, base_sort, - base_morph, export_morph, assm_intro, of_class, axiom), ([], operations))) - #> fold (curry Graph.add_edge class) sups; - in ClassData.map add_class thy end; - -fun activate_defs class thms thy = case Element.eq_morphism thy thms - of SOME eq_morph => fold (fn cls => fn thy => - Context.theory_map (Locale.amend_registration (cls, base_morphism thy cls) - (eq_morph, true) (export_morphism thy cls)) thy) (heritage thy [class]) thy - | NONE => thy; - -fun register_operation class (c, (t, some_def)) thy = - let - val base_sort = base_sort thy class; - val prep_typ = map_type_tfree - (fn (v, sort) => if Name.aT = v - then TFree (v, base_sort) else TVar ((v, 0), sort)); - val t' = map_types prep_typ t; - val ty' = Term.fastype_of t'; - in - thy - |> (ClassData.map o Graph.map_node class o map_class_data o apsnd) - (fn (defs, operations) => - (fold cons (the_list some_def) defs, - (c, (class, (ty', t'))) :: operations)) - |> activate_defs class (the_list some_def) - end; - -fun register_subclass (sub, sup) some_dep_morph some_wit export thy = - let - val intros = (snd o rules thy) sup :: map_filter I - [Option.map (Drule.export_without_context_open o Element.conclude_witness) some_wit, - (fst o rules thy) sub]; - val tac = EVERY (map (TRYALL o Tactic.rtac) intros); - val classrel = Skip_Proof.prove_global thy [] [] (Logic.mk_classrel (sub, sup)) - (K tac); - val diff_sort = Sign.complete_sort thy [sup] - |> subtract (op =) (Sign.complete_sort thy [sub]) - |> filter (is_class thy); - val add_dependency = case some_dep_morph - of SOME dep_morph => Locale.add_dependency sub - (sup, dep_morph $> Element.satisfy_morphism (the_list some_wit)) export - | NONE => I - in - thy - |> AxClass.add_classrel classrel - |> ClassData.map (Graph.add_edge (sub, sup)) - |> activate_defs sub (these_defs thy diff_sort) - |> add_dependency - end; - - -(** classes and class target **) - -(* class context syntax *) - -fun these_unchecks thy = map (fn (c, (_, (ty, t))) => (t, Const (c, ty))) - o these_operations thy; - -fun redeclare_const thy c = - let val b = Long_Name.base_name c - in Sign.intern_const thy b = c ? Variable.declare_const (b, c) end; - -fun synchronize_class_syntax sort base_sort ctxt = - let - val thy = ProofContext.theory_of ctxt; - val algebra = Sign.classes_of thy; - val operations = these_operations thy sort; - fun subst_class_typ sort = map_type_tfree (K (TVar ((Name.aT, 0), sort))); - val primary_constraints = - (map o apsnd) (subst_class_typ base_sort o fst o snd) operations; - val secondary_constraints = - (map o apsnd) (fn (class, (ty, _)) => subst_class_typ [class] ty) operations; - fun improve (c, ty) = (case AList.lookup (op =) primary_constraints c - of SOME ty' => (case try (Type.raw_match (ty', ty)) Vartab.empty - of SOME tyenv => (case Vartab.lookup tyenv (Name.aT, 0) - of SOME (_, ty' as TVar (vi, sort)) => - if Type_Infer.is_param vi - andalso Sorts.sort_le algebra (base_sort, sort) - then SOME (ty', TFree (Name.aT, base_sort)) - else NONE - | _ => NONE) - | NONE => NONE) - | NONE => NONE) - fun subst (c, ty) = Option.map snd (AList.lookup (op =) operations c); - val unchecks = these_unchecks thy sort; - in - ctxt - |> fold (redeclare_const thy o fst) primary_constraints - |> Overloading.map_improvable_syntax (K (((primary_constraints, secondary_constraints), - (((improve, subst), true), unchecks)), false)) - |> Overloading.set_primary_constraints - end; - -fun refresh_syntax class ctxt = - let - val thy = ProofContext.theory_of ctxt; - val base_sort = base_sort thy class; - in synchronize_class_syntax [class] base_sort ctxt end; - -fun redeclare_operations thy sort = - fold (redeclare_const thy o fst) (these_operations thy sort); - -fun begin sort base_sort ctxt = - ctxt - |> Variable.declare_term - (Logic.mk_type (TFree (Name.aT, base_sort))) - |> synchronize_class_syntax sort base_sort - |> Overloading.add_improvable_syntax; - -fun init class thy = - thy - |> Locale.init class - |> begin [class] (base_sort thy class); - - -(* class target *) - -val class_prefix = Logic.const_of_class o Long_Name.base_name; - -fun declare class ((c, mx), (type_params, dict)) thy = - let - val morph = morphism thy class; - val b = Morphism.binding morph c; - val b_def = Morphism.binding morph (Binding.suffix_name "_dict" b); - val c' = Sign.full_name thy b; - val dict' = Morphism.term morph dict; - val ty' = map Term.fastype_of type_params ---> Term.fastype_of dict'; - val def_eq = Logic.mk_equals (list_comb (Const (c', ty'), type_params), dict') - |> map_types Type.strip_sorts; - in - thy - |> Sign.declare_const ((b, Type.strip_sorts ty'), mx) - |> snd - |> Thm.add_def false false (b_def, def_eq) - |>> apsnd Thm.varifyT_global - |-> (fn (_, def_thm) => PureThy.store_thm (b_def, def_thm) - #> snd - #> null type_params ? register_operation class (c', (dict', SOME (Thm.symmetric def_thm)))) - |> Sign.add_const_constraint (c', SOME ty') - end; - -fun abbrev class prmode ((c, mx), rhs) thy = - let - val morph = morphism thy class; - val unchecks = these_unchecks thy [class]; - val b = Morphism.binding morph c; - val c' = Sign.full_name thy b; - val rhs' = Pattern.rewrite_term thy unchecks [] rhs; - val ty' = Term.fastype_of rhs'; - val rhs'' = map_types Logic.varifyT_global rhs'; - in - thy - |> Sign.add_abbrev (#1 prmode) (b, rhs'') - |> snd - |> Sign.add_const_constraint (c', SOME ty') - |> Sign.notation true prmode [(Const (c', ty'), mx)] - |> not (#1 prmode = Print_Mode.input) ? register_operation class (c', (rhs', NONE)) - end; - - -(* simple subclasses *) - -local - -fun gen_classrel mk_prop classrel thy = - let - fun after_qed results = - ProofContext.theory ((fold o fold) AxClass.add_classrel results); - in - thy - |> ProofContext.init_global - |> Proof.theorem NONE after_qed [[(mk_prop thy classrel, [])]] - end; - -in - -val classrel = - gen_classrel (Logic.mk_classrel oo AxClass.cert_classrel); -val classrel_cmd = - gen_classrel (Logic.mk_classrel oo AxClass.read_classrel); - -end; (*local*) - - -(** instantiation target **) - -(* bookkeeping *) - -datatype instantiation = Instantiation of { - arities: string list * (string * sort) list * sort, - params: ((string * string) * (string * typ)) list - (*(instantiation parameter, type constructor), (local instantiation parameter, typ)*) -} - -structure Instantiation = Proof_Data -( - type T = instantiation - fun init _ = Instantiation { arities = ([], [], []), params = [] }; -); - -fun mk_instantiation (arities, params) = - Instantiation { arities = arities, params = params }; -fun get_instantiation lthy = case Instantiation.get (Local_Theory.target_of lthy) - of Instantiation data => data; -fun map_instantiation f = (Local_Theory.target o Instantiation.map) - (fn Instantiation { arities, params } => mk_instantiation (f (arities, params))); - -fun the_instantiation lthy = case get_instantiation lthy - of { arities = ([], [], []), ... } => error "No instantiation target" - | data => data; - -val instantiation_params = #params o get_instantiation; - -fun instantiation_param lthy b = instantiation_params lthy - |> find_first (fn (_, (v, _)) => Binding.name_of b = v) - |> Option.map (fst o fst); - -fun read_multi_arity thy (raw_tycos, raw_sorts, raw_sort) = - let - val ctxt = ProofContext.init_global thy; - val all_arities = map (fn raw_tyco => ProofContext.read_arity ctxt - (raw_tyco, raw_sorts, raw_sort)) raw_tycos; - val tycos = map #1 all_arities; - val (_, sorts, sort) = hd all_arities; - val vs = Name.names Name.context Name.aT sorts; - in (tycos, vs, sort) end; - - -(* syntax *) - -fun synchronize_inst_syntax ctxt = - let - val Instantiation { params, ... } = Instantiation.get ctxt; - - val lookup_inst_param = AxClass.lookup_inst_param - (Sign.consts_of (ProofContext.theory_of ctxt)) params; - fun subst (c, ty) = case lookup_inst_param (c, ty) - of SOME (v_ty as (_, ty)) => SOME (ty, Free v_ty) - | NONE => NONE; - val unchecks = - map (fn ((c, _), v_ty as (_, ty)) => (Free v_ty, Const (c, ty))) params; - in - ctxt - |> Overloading.map_improvable_syntax - (fn (((primary_constraints, _), (((improve, _), _), _)), _) => - (((primary_constraints, []), (((improve, subst), false), unchecks)), false)) - end; - - -(* target *) - -val sanitize_name = (*necessary as long as "dirty" type identifiers are permitted*) - let - fun is_valid s = Symbol.is_ascii_letter s orelse Symbol.is_ascii_digit s - orelse s = "'" orelse s = "_"; - val is_junk = not o is_valid andf Symbol.is_regular; - val junk = Scan.many is_junk; - val scan_valids = Symbol.scanner "Malformed input" - ((junk |-- - (Scan.optional (Scan.one Symbol.is_ascii_letter) "x" ^^ (Scan.many is_valid >> implode) - --| junk)) - ::: Scan.repeat ((Scan.many1 is_valid >> implode) --| junk)); - in - explode #> scan_valids #> implode - end; - -val type_name = sanitize_name o Long_Name.base_name; - -fun resort_terms pp algebra consts constraints ts = - let - fun matchings (Const (c_ty as (c, _))) = (case constraints c - of NONE => I - | SOME sorts => fold2 (curry (Sorts.meet_sort algebra)) - (Consts.typargs consts c_ty) sorts) - | matchings _ = I - val tvartab = (fold o fold_aterms) matchings ts Vartab.empty - handle Sorts.CLASS_ERROR e => error (Sorts.class_error pp e); - val inst = map_type_tvar - (fn (vi, sort) => TVar (vi, the_default sort (Vartab.lookup tvartab vi))); - in if Vartab.is_empty tvartab then NONE else SOME ((map o map_types) inst ts) end; - -fun init_instantiation (tycos, vs, sort) thy = - let - val _ = if null tycos then error "At least one arity must be given" else (); - val class_params = these_params thy (filter (can (AxClass.get_info thy)) sort); - fun get_param tyco (param, (_, (c, ty))) = - if can (AxClass.param_of_inst thy) (c, tyco) - then NONE else SOME ((c, tyco), - (param ^ "_" ^ type_name tyco, map_atyps (K (Type (tyco, map TFree vs))) ty)); - val params = map_product get_param tycos class_params |> map_filter I; - val primary_constraints = map (apsnd - (map_atyps (K (TVar ((Name.aT, 0), [])))) o snd o snd) class_params; - val pp = Syntax.pp_global thy; - val algebra = Sign.classes_of thy - |> fold (fn tyco => Sorts.add_arities pp - (tyco, map (fn class => (class, map snd vs)) sort)) tycos; - val consts = Sign.consts_of thy; - val improve_constraints = AList.lookup (op =) - (map (fn (_, (class, (c, _))) => (c, [[class]])) class_params); - fun resort_check ts ctxt = case resort_terms (Syntax.pp ctxt) algebra consts improve_constraints ts - of NONE => NONE - | SOME ts' => SOME (ts', ctxt); - val lookup_inst_param = AxClass.lookup_inst_param consts params; - val typ_instance = Type.typ_instance (Sign.tsig_of thy); - fun improve (c, ty) = case lookup_inst_param (c, ty) - of SOME (_, ty') => if typ_instance (ty', ty) then SOME (ty, ty') else NONE - | NONE => NONE; - in - thy - |> Theory.checkpoint - |> ProofContext.init_global - |> Instantiation.put (mk_instantiation ((tycos, vs, sort), params)) - |> fold (Variable.declare_typ o TFree) vs - |> fold (Variable.declare_names o Free o snd) params - |> (Overloading.map_improvable_syntax o apfst) - (K ((primary_constraints, []), (((improve, K NONE), false), []))) - |> Overloading.add_improvable_syntax - |> Context.proof_map (Syntax.add_term_check 0 "resorting" resort_check) - |> synchronize_inst_syntax - end; - -fun confirm_declaration b = (map_instantiation o apsnd) - (filter_out (fn (_, (c', _)) => c' = Binding.name_of b)) - #> Local_Theory.target synchronize_inst_syntax - -fun gen_instantiation_instance do_proof after_qed lthy = - let - val (tycos, vs, sort) = (#arities o the_instantiation) lthy; - val arities_proof = maps (fn tyco => Logic.mk_arities (tyco, map snd vs, sort)) tycos; - fun after_qed' results = - Local_Theory.theory (fold (AxClass.add_arity o Thm.varifyT_global) results) - #> after_qed; - in - lthy - |> do_proof after_qed' arities_proof - end; - -val instantiation_instance = gen_instantiation_instance (fn after_qed => fn ts => - Proof.theorem NONE (after_qed o map the_single) (map (fn t => [(t, [])]) ts)); - -fun prove_instantiation_instance tac = gen_instantiation_instance (fn after_qed => - fn ts => fn lthy => after_qed (map (fn t => Goal.prove lthy [] [] t - (fn {context, ...} => tac context)) ts) lthy) I; - -fun prove_instantiation_exit tac = prove_instantiation_instance tac - #> Local_Theory.exit_global; - -fun prove_instantiation_exit_result f tac x lthy = - let - val morph = ProofContext.export_morphism lthy - (ProofContext.init_global (ProofContext.theory_of lthy)); - val y = f morph x; - in - lthy - |> prove_instantiation_exit (fn ctxt => tac ctxt y) - |> pair y - end; - -fun conclude_instantiation lthy = - let - val (tycos, vs, sort) = (#arities o the_instantiation) lthy; - val thy = ProofContext.theory_of lthy; - val _ = map (fn tyco => if Sign.of_sort thy - (Type (tyco, map TFree vs), sort) - then () else error ("Missing instance proof for type " ^ quote (Sign.extern_type thy tyco))) - tycos; - in lthy end; - -fun pretty_instantiation lthy = - let - val { arities = (tycos, vs, sort), params } = the_instantiation lthy; - val thy = ProofContext.theory_of lthy; - fun pr_arity tyco = Syntax.pretty_arity lthy (tyco, map snd vs, sort); - fun pr_param ((c, _), (v, ty)) = - (Pretty.block o Pretty.breaks) [Pretty.str v, Pretty.str "==", - (Pretty.str o Sign.extern_const thy) c, Pretty.str "::", Syntax.pretty_typ_global thy ty]; - in - (Pretty.block o Pretty.fbreaks) - (Pretty.str "instantiation" :: map pr_arity tycos @ map pr_param params) - end; - -fun syntax_error c = error ("Illegal mixfix syntax for overloaded constant " ^ quote c); - -fun instantiation_foundation (((b, U), mx), (b_def, rhs)) (type_params, term_params) lthy = - case instantiation_param lthy b - of SOME c => if mx <> NoSyn then syntax_error c - else lthy |> Local_Theory.theory_result (AxClass.declare_overloaded (c, U) - ##>> AxClass.define_overloaded b_def (c, rhs)) - ||> confirm_declaration b - | NONE => lthy |> - Generic_Target.theory_foundation (((b, U), mx), (b_def, rhs)) (type_params, term_params); - -fun instantiation arities thy = - thy - |> init_instantiation arities - |> Local_Theory.init NONE "" - {define = Generic_Target.define instantiation_foundation, - notes = Generic_Target.notes - (fn kind => fn global_facts => fn _ => Generic_Target.theory_notes kind global_facts), - abbrev = Generic_Target.abbrev - (fn prmode => fn (b, mx) => fn (t, _) => fn _ => Generic_Target.theory_abbrev prmode ((b, mx), t)), - declaration = K Generic_Target.theory_declaration, - syntax_declaration = K Generic_Target.theory_declaration, - pretty = single o pretty_instantiation, - reinit = instantiation arities o ProofContext.theory_of, - exit = Local_Theory.target_of o conclude_instantiation}; - -fun instantiation_cmd arities thy = - instantiation (read_multi_arity thy arities) thy; - - -(* simplified instantiation interface with no class parameter *) - -fun instance_arity_cmd raw_arities thy = - let - val (tycos, vs, sort) = read_multi_arity thy raw_arities; - val sorts = map snd vs; - val arities = maps (fn tyco => Logic.mk_arities (tyco, sorts, sort)) tycos; - fun after_qed results = ProofContext.theory - ((fold o fold) AxClass.add_arity results); - in - thy - |> ProofContext.init_global - |> Proof.theorem NONE after_qed (map (fn t => [(t, [])]) arities) - end; - - -(** tactics and methods **) - -fun intro_classes_tac facts st = - let - val thy = Thm.theory_of_thm st; - val classes = Sign.all_classes thy; - val class_trivs = map (Thm.class_triv thy) classes; - val class_intros = map_filter (try (#intro o AxClass.get_info thy)) classes; - val assm_intros = all_assm_intros thy; - in - Method.intros_tac (class_trivs @ class_intros @ assm_intros) facts st - end; - -fun default_intro_tac ctxt [] = - intro_classes_tac [] ORELSE Locale.intro_locales_tac true ctxt [] - | default_intro_tac _ _ = no_tac; - -fun default_tac rules ctxt facts = - HEADGOAL (Method.some_rule_tac rules ctxt facts) ORELSE - default_intro_tac ctxt facts; - -val _ = Context.>> (Context.map_theory - (Method.setup (Binding.name "intro_classes") (Scan.succeed (K (METHOD intro_classes_tac))) - "back-chain introduction rules of classes" #> - Method.setup (Binding.name "default") (Attrib.thms >> (METHOD oo default_tac)) - "apply some intro/elim rule")); - -end; - diff -r 7eb0f6991e25 -r 001f2f44984c src/Pure/Isar/expression.ML --- a/src/Pure/Isar/expression.ML Sat Aug 14 12:01:50 2010 +0200 +++ b/src/Pure/Isar/expression.ML Sat Aug 14 13:24:06 2010 +0200 @@ -775,7 +775,7 @@ val loc_ctxt = thy' |> Locale.register_locale binding (extraTs, params) (asm, rev defs) (a_intro, b_intro) axioms [] (rev notes) (rev deps') - |> Named_Target.init (SOME name) + |> Named_Target.init name |> fold (fn (kind, facts) => Local_Theory.notes_kind kind facts #> snd) notes'; in (name, loc_ctxt) end; @@ -870,7 +870,7 @@ fun gen_sublocale prep_expr intern raw_target expression thy = let val target = intern thy raw_target; - val target_ctxt = Named_Target.init (SOME target) thy; + val target_ctxt = Named_Target.init target thy; val ((propss, deps, export), goal_ctxt) = prep_expr expression target_ctxt; fun after_qed witss = ProofContext.theory (fold (fn ((dep, morph), wits) => Locale.add_dependency diff -r 7eb0f6991e25 -r 001f2f44984c src/Pure/Isar/isar_syn.ML --- a/src/Pure/Isar/isar_syn.ML Sat Aug 14 12:01:50 2010 +0200 +++ b/src/Pure/Isar/isar_syn.ML Sat Aug 14 13:24:06 2010 +0200 @@ -462,11 +462,11 @@ (Parse.binding -- Scan.optional (Parse.$$$ "=" |-- class_val) ([], []) -- Parse.opt_begin >> (fn ((name, (supclasses, elems)), begin) => (begin ? Toplevel.print) o Toplevel.begin_local_theory begin - (Class.class_cmd name supclasses elems #> snd))); + (Class_Declaration.class_cmd name supclasses elems #> snd))); val _ = Outer_Syntax.local_theory_to_proof "subclass" "prove a subclass relation" Keyword.thy_goal - (Parse.xname >> Class.subclass_cmd); + (Parse.xname >> Class_Declaration.subclass_cmd); val _ = Outer_Syntax.command "instantiation" "instantiate and prove type arity" Keyword.thy_decl diff -r 7eb0f6991e25 -r 001f2f44984c src/Pure/Isar/local_theory.ML --- a/src/Pure/Isar/local_theory.ML Sat Aug 14 12:01:50 2010 +0200 +++ b/src/Pure/Isar/local_theory.ML Sat Aug 14 13:24:06 2010 +0200 @@ -50,7 +50,6 @@ val const_alias: binding -> string -> local_theory -> local_theory val init: serial option -> string -> operations -> Proof.context -> local_theory val restore: local_theory -> local_theory - val reinit: local_theory -> local_theory val exit: local_theory -> Proof.context val exit_global: local_theory -> theory val exit_result: (morphism -> 'a -> 'b) -> 'a * local_theory -> 'b * Proof.context @@ -75,7 +74,6 @@ declaration: bool -> declaration -> local_theory -> local_theory, syntax_declaration: bool -> declaration -> local_theory -> local_theory, pretty: local_theory -> Pretty.T list, - reinit: local_theory -> local_theory, exit: local_theory -> Proof.context}; datatype lthy = LThy of @@ -260,8 +258,6 @@ let val {naming, theory_prefix, operations, target} = get_lthy lthy in init (Name_Space.get_group naming) theory_prefix operations target end; -val reinit = checkpoint o operation #reinit; - (* exit *) diff -r 7eb0f6991e25 -r 001f2f44984c src/Pure/Isar/named_target.ML --- a/src/Pure/Isar/named_target.ML Sat Aug 14 12:01:50 2010 +0200 +++ b/src/Pure/Isar/named_target.ML Sat Aug 14 13:24:06 2010 +0200 @@ -7,9 +7,11 @@ signature NAMED_TARGET = sig - val peek: local_theory -> {target: string, is_locale: bool, is_class: bool} - val init: string option -> theory -> local_theory + val init: string -> theory -> local_theory + val theory_init: theory -> local_theory + val reinit: local_theory -> local_theory -> local_theory val context_cmd: xstring -> theory -> local_theory + val peek: local_theory -> {target: string, is_locale: bool, is_class: bool} option end; structure Named_Target: NAMED_TARGET = @@ -22,15 +24,21 @@ fun make_target target is_locale is_class = Target {target = target, is_locale = is_locale, is_class = is_class}; -val global_target = make_target "" false false; +val global_target = Target {target = "", is_locale = false, is_class = false}; + +fun named_target _ "" = global_target + | named_target thy locale = + if Locale.defined thy locale + then Target {target = locale, is_locale = true, is_class = Class.is_class thy locale} + else error ("No such locale: " ^ quote locale); structure Data = Proof_Data ( - type T = target; - fun init _ = global_target; + type T = target option; + fun init _ = NONE; ); -val peek = (fn Target args => args) o Data.get; +val peek = Option.map (fn Target args => args) o Data.get; (* generic declarations *) @@ -63,7 +71,7 @@ val is_canonical_class = is_class andalso (Binding.eq_name (b, b') andalso not (null prefix') - andalso List.last prefix' = (Class_Target.class_prefix target, false) + andalso List.last prefix' = (Class.class_prefix target, false) orelse same_shape); in not is_canonical_class ? @@ -82,7 +90,7 @@ fun class_target (Target {target, ...}) f = Local_Theory.raw_theory f #> - Local_Theory.target (Class_Target.refresh_syntax target); + Local_Theory.target (Class.refresh_syntax target); (* define *) @@ -96,7 +104,7 @@ (((b, U), mx), (b_def, rhs)) (type_params, term_params) = Generic_Target.theory_foundation (((b, U), NoSyn), (b_def, rhs)) (type_params, term_params) #-> (fn (lhs, def) => locale_const_declaration ta Syntax.mode_default ((b, NoSyn), lhs) - #> class_target ta (Class_Target.declare target ((b, mx), (type_params, lhs))) + #> class_target ta (Class.const target ((b, mx), (type_params, lhs))) #> pair (lhs, def)) fun target_foundation (ta as Target {target, is_locale, is_class, ...}) = @@ -135,7 +143,7 @@ if is_locale then lthy |> locale_abbrev ta prmode ((b, if is_class then NoSyn else mx), global_rhs) xs - |> is_class ? class_target ta (Class_Target.abbrev target prmode ((b, mx), t')) + |> is_class ? class_target ta (Class.abbrev target prmode ((b, mx), t')) else lthy |> Generic_Target.theory_abbrev prmode ((b, mx), global_rhs); @@ -168,19 +176,19 @@ pretty_thy ctxt target is_class; -(* init various targets *) +(* init *) local -fun init_data (Target {target, is_locale, is_class}) = +fun init_context (Target {target, is_locale, is_class}) = if not is_locale then ProofContext.init_global else if not is_class then Locale.init target - else Class_Target.init target; + else Class.init target; fun init_target (ta as Target {target, ...}) thy = thy - |> init_data ta - |> Data.put ta + |> init_context ta + |> Data.put (SOME ta) |> Local_Theory.init NONE (Long_Name.base_name target) {define = Generic_Target.define (target_foundation ta), notes = Generic_Target.notes (target_notes ta), @@ -190,21 +198,20 @@ syntax_declaration = fn pervasive => target_declaration ta { syntax = true, pervasive = pervasive }, pretty = pretty ta, - reinit = init_target ta o ProofContext.theory_of, exit = Local_Theory.target_of}; -fun named_target _ NONE = global_target - | named_target thy (SOME target) = - if Locale.defined thy target - then make_target target true (Class_Target.is_class thy target) - else error ("No such locale: " ^ quote target); - in fun init target thy = init_target (named_target thy target) thy; -fun context_cmd "-" thy = init NONE thy - | context_cmd target thy = init (SOME (Locale.intern thy target)) thy; +fun reinit lthy = case peek lthy + of SOME {target, ...} => init target o Local_Theory.exit_global + | NONE => error "Not in a named target"; + +val theory_init = init_target global_target; + +fun context_cmd "-" thy = init "" thy + | context_cmd target thy = init (Locale.intern thy target) thy; end; diff -r 7eb0f6991e25 -r 001f2f44984c src/Pure/Isar/overloading.ML --- a/src/Pure/Isar/overloading.ML Sat Aug 14 12:01:50 2010 +0200 +++ b/src/Pure/Isar/overloading.ML Sat Aug 14 13:24:06 2010 +0200 @@ -6,14 +6,6 @@ signature OVERLOADING = sig - val init: (string * (string * typ) * bool) list -> theory -> Proof.context - val conclude: local_theory -> local_theory - val declare: string * typ -> theory -> term * theory - val confirm: binding -> local_theory -> local_theory - val define: bool -> binding -> string * term -> theory -> thm * theory - val operation: Proof.context -> binding -> (string * bool) option - val pretty: Proof.context -> Pretty.T - type improvable_syntax val add_improvable_syntax: Proof.context -> Proof.context val map_improvable_syntax: (improvable_syntax -> improvable_syntax) @@ -121,27 +113,22 @@ (** overloading target **) -(* bookkeeping *) - -structure OverloadingData = Proof_Data +structure Data = Proof_Data ( type T = ((string * typ) * (string * bool)) list; fun init _ = []; ); -val get_overloading = OverloadingData.get o Local_Theory.target_of; -val map_overloading = Local_Theory.target o OverloadingData.map; +val get_overloading = Data.get o Local_Theory.target_of; +val map_overloading = Local_Theory.target o Data.map; fun operation lthy b = get_overloading lthy |> get_first (fn ((c, _), (v, checked)) => - if Binding.name_of b = v then SOME (c, checked) else NONE); - - -(* target *) + if Binding.name_of b = v then SOME (c, (v, checked)) else NONE); fun synchronize_syntax ctxt = let - val overloading = OverloadingData.get ctxt; + val overloading = Data.get ctxt; fun subst (c, ty) = case AList.lookup (op =) overloading (c, ty) of SOME (v, _) => SOME (ty, Free (v, ty)) | NONE => NONE; @@ -152,38 +139,20 @@ |> map_improvable_syntax (K ((([], []), (((K NONE, subst), false), unchecks)), false)) end -fun init raw_overloading thy = - let - val _ = if null raw_overloading then error "At least one parameter must be given" else (); - val overloading = map (fn (v, c_ty, checked) => (c_ty, (v, checked))) raw_overloading; - in - thy - |> Theory.checkpoint - |> ProofContext.init_global - |> OverloadingData.put overloading - |> fold (fn ((_, ty), (v, _)) => Variable.declare_names (Free (v, ty))) overloading - |> add_improvable_syntax - |> synchronize_syntax - end; - -fun declare c_ty = pair (Const c_ty); +fun define_overloaded (c, U) (v, checked) (b_def, rhs) = + Local_Theory.theory_result + (Thm.add_def (not checked) true (b_def, Logic.mk_equals (Const (c, Term.fastype_of rhs), rhs))) + ##> map_overloading (filter_out (fn (_, (v', _)) => v' = v)) + ##> Local_Theory.target synchronize_syntax + #-> (fn (_, def) => pair (Const (c, U), def)) -fun define checked b (c, t) = - Thm.add_def (not checked) true (b, Logic.mk_equals (Const (c, Term.fastype_of t), t)) - #>> snd; - -fun confirm b = map_overloading (filter_out (fn (_, (c', _)) => c' = Binding.name_of b)) - #> Local_Theory.target synchronize_syntax - -fun conclude lthy = - let - val overloading = get_overloading lthy; - val _ = if null overloading then () else - error ("Missing definition(s) for parameter(s) " ^ commas (map (quote - o Syntax.string_of_term lthy o Const o fst) overloading)); - in - lthy - end; +fun foundation (((b, U), mx), (b_def, rhs)) (type_params, term_params) lthy = + case operation lthy b + of SOME (c, (v, checked)) => if mx <> NoSyn + then error ("Illegal mixfix syntax for overloaded constant " ^ quote c) + else lthy |> define_overloaded (c, U) (v, checked) (b_def, rhs) + | NONE => lthy |> + Generic_Target.theory_foundation (((b, U), mx), (b_def, rhs)) (type_params, term_params); fun pretty lthy = let @@ -192,32 +161,32 @@ fun pr_operation ((c, ty), (v, _)) = (Pretty.block o Pretty.breaks) [Pretty.str v, Pretty.str "==", Pretty.str (Sign.extern_const thy c), Pretty.str "::", Syntax.pretty_typ lthy ty]; - in - (Pretty.block o Pretty.fbreaks) - (Pretty.str "overloading" :: map pr_operation overloading) - end; - -fun syntax_error c = error ("Illegal mixfix syntax for overloaded constant " ^ quote c); + in Pretty.str "overloading" :: map pr_operation overloading end; -fun overloading_foundation (((b, U), mx), (b_def, rhs)) (type_params, term_params) lthy = - case operation lthy b - of SOME (c, checked) => if mx <> NoSyn then syntax_error c - else lthy |> Local_Theory.theory_result (declare (c, U) - ##>> define checked b_def (c, rhs)) - ||> confirm b - | NONE => lthy |> - Generic_Target.theory_foundation (((b, U), mx), (b_def, rhs)) (type_params, term_params); +fun conclude lthy = + let + val overloading = get_overloading lthy; + val _ = if null overloading then () else + error ("Missing definition(s) for parameter(s) " ^ commas (map (quote + o Syntax.string_of_term lthy o Const o fst) overloading)); + in lthy end; -fun gen_overloading prep_const raw_ops thy = +fun gen_overloading prep_const raw_overloading thy = let val ctxt = ProofContext.init_global thy; - val ops = raw_ops |> map (fn (name, const, checked) => - (name, Term.dest_Const (prep_const ctxt const), checked)); + val _ = if null raw_overloading then error "At least one parameter must be given" else (); + val overloading = raw_overloading |> map (fn (v, const, checked) => + (Term.dest_Const (prep_const ctxt const), (v, checked))); in thy - |> init ops + |> Theory.checkpoint + |> ProofContext.init_global + |> Data.put overloading + |> fold (fn ((_, ty), (v, _)) => Variable.declare_names (Free (v, ty))) overloading + |> add_improvable_syntax + |> synchronize_syntax |> Local_Theory.init NONE "" - {define = Generic_Target.define overloading_foundation, + {define = Generic_Target.define foundation, notes = Generic_Target.notes (fn kind => fn global_facts => fn _ => Generic_Target.theory_notes kind global_facts), abbrev = Generic_Target.abbrev @@ -225,8 +194,7 @@ Generic_Target.theory_abbrev prmode ((b, mx), t)), declaration = K Generic_Target.theory_declaration, syntax_declaration = K Generic_Target.theory_declaration, - pretty = single o pretty, - reinit = gen_overloading prep_const raw_ops o ProofContext.theory_of, + pretty = pretty, exit = Local_Theory.target_of o conclude} end; diff -r 7eb0f6991e25 -r 001f2f44984c src/Pure/Isar/specification.ML --- a/src/Pure/Isar/specification.ML Sat Aug 14 12:01:50 2010 +0200 +++ b/src/Pure/Isar/specification.ML Sat Aug 14 13:24:06 2010 +0200 @@ -185,7 +185,7 @@ (*facts*) val (facts, facts_lthy) = axioms_thy - |> Named_Target.init NONE + |> Named_Target.theory_init |> Spec_Rules.add Spec_Rules.Unknown (consts, maps (maps #1 o #2) axioms) |> Local_Theory.notes axioms; diff -r 7eb0f6991e25 -r 001f2f44984c src/Pure/Isar/toplevel.ML --- a/src/Pure/Isar/toplevel.ML Sat Aug 14 12:01:50 2010 +0200 +++ b/src/Pure/Isar/toplevel.ML Sat Aug 14 13:24:06 2010 +0200 @@ -107,12 +107,11 @@ fun loc_begin loc (Context.Theory thy) = loc_init (the_default "-" loc) thy | loc_begin NONE (Context.Proof lthy) = lthy - | loc_begin (SOME loc) (Context.Proof lthy) = loc_init loc (loc_exit lthy); + | loc_begin (SOME loc) (Context.Proof lthy) = (loc_init loc o loc_exit) lthy; fun loc_finish _ (Context.Theory _) = Context.Theory o loc_exit | loc_finish NONE (Context.Proof _) = Context.Proof o Local_Theory.restore - | loc_finish (SOME _) (Context.Proof lthy) = fn lthy' => - Context.Proof (Local_Theory.reinit (Local_Theory.raw_theory (K (loc_exit lthy')) lthy)); + | loc_finish (SOME _) (Context.Proof lthy) = Context.Proof o Named_Target.reinit lthy; (* datatype node *) @@ -191,7 +190,7 @@ (* print state *) -val pretty_context = Local_Theory.pretty o Context.cases (Named_Target.init NONE) I; +val pretty_context = Local_Theory.pretty o Context.cases (Named_Target.theory_init) I; fun print_state_context state = (case try node_of state of diff -r 7eb0f6991e25 -r 001f2f44984c src/Pure/Isar/typedecl.ML --- a/src/Pure/Isar/typedecl.ML Sat Aug 14 12:01:50 2010 +0200 +++ b/src/Pure/Isar/typedecl.ML Sat Aug 14 13:24:06 2010 +0200 @@ -75,7 +75,7 @@ end; fun typedecl_global decl = - Named_Target.init NONE + Named_Target.theory_init #> typedecl decl #> Local_Theory.exit_result_global Morphism.typ; @@ -115,7 +115,7 @@ end; fun abbrev_global decl rhs = - Named_Target.init NONE + Named_Target.theory_init #> abbrev decl rhs #> Local_Theory.exit_result_global (K I); diff -r 7eb0f6991e25 -r 001f2f44984c src/Pure/ROOT.ML --- a/src/Pure/ROOT.ML Sat Aug 14 12:01:50 2010 +0200 +++ b/src/Pure/ROOT.ML Sat Aug 14 13:24:06 2010 +0200 @@ -209,10 +209,10 @@ use "Isar/generic_target.ML"; use "Isar/overloading.ML"; use "axclass.ML"; -use "Isar/class_target.ML"; +use "Isar/class.ML"; use "Isar/named_target.ML"; use "Isar/expression.ML"; -use "Isar/class.ML"; +use "Isar/class_declaration.ML"; use "simplifier.ML"; diff -r 7eb0f6991e25 -r 001f2f44984c src/Pure/axclass.ML --- a/src/Pure/axclass.ML Sat Aug 14 12:01:50 2010 +0200 +++ b/src/Pure/axclass.ML Sat Aug 14 13:24:06 2010 +0200 @@ -406,7 +406,7 @@ in thy |> Thm.add_def false false (b', prop) - |>> (fn (_, thm) => Drule.transitive_thm OF [eq, thm]) + |>> (fn (_, thm) => Drule.transitive_thm OF [eq, thm]) end; diff -r 7eb0f6991e25 -r 001f2f44984c src/Tools/quickcheck.ML --- a/src/Tools/quickcheck.ML Sat Aug 14 12:01:50 2010 +0200 +++ b/src/Tools/quickcheck.ML Sat Aug 14 13:24:06 2010 +0200 @@ -219,9 +219,10 @@ | strip t = t; val {goal = st, ...} = Proof.raw_goal state; val (gi, frees) = Logic.goal_params (prop_of st) i; - val some_locale = case (#target o Named_Target.peek) lthy - of "" => NONE - | locale => SOME locale; + val some_locale = case (Option.map #target o Named_Target.peek) lthy + of NONE => NONE + | SOME "" => NONE + | SOME locale => SOME locale; val assms = if no_assms then [] else case some_locale of NONE => Assumption.all_assms_of lthy | SOME locale => Assumption.local_assms_of lthy (Locale.init locale thy);