merged
authorhaftmann
Tue Aug 17 14:33:44 2010 +0200 (2010-08-17)
changeset 384630e4565062017
parent 38457 b8760b6e7c65
parent 38462 34d3de1254cd
child 38464 e0b8b1733689
child 38493 95a41e6ef5a8
child 38528 bbaaaf6f1cbe
merged
     1.1 --- a/CONTRIBUTORS	Tue Aug 17 13:10:58 2010 +0200
     1.2 +++ b/CONTRIBUTORS	Tue Aug 17 14:33:44 2010 +0200
     1.3 @@ -6,6 +6,9 @@
     1.4  Contributions to this Isabelle version
     1.5  --------------------------------------
     1.6  
     1.7 +* July 2010: Florian Haftmann, TUM
     1.8 +  Reworking and extension of the Isabelle/HOL framework.
     1.9 +
    1.10  
    1.11  Contributions to Isabelle2009-2
    1.12  --------------------------------------
     2.1 --- a/NEWS	Tue Aug 17 13:10:58 2010 +0200
     2.2 +++ b/NEWS	Tue Aug 17 14:33:44 2010 +0200
     2.3 @@ -35,11 +35,17 @@
     2.4  
     2.5  *** HOL ***
     2.6  
     2.7 +* Session Imperative_HOL: revamped, corrected dozens of inadequacies.
     2.8 +INCOMPATIBILITY.
     2.9 +
    2.10 +* Quickcheck in locales considers interpretations of that locale for
    2.11 +counter example search.
    2.12 +
    2.13  * Theory Library/Monad_Syntax provides do-syntax for monad types.  Syntax
    2.14  in Library/State_Monad has been changed to avoid ambiguities.
    2.15  INCOMPATIBILITY.
    2.16  
    2.17 -* code generator: export_code without explicit file declaration prints
    2.18 +* Code generator: export_code without explicit file declaration prints
    2.19  to standard output.  INCOMPATIBILITY.
    2.20  
    2.21  * Abolished symbol type names:  "prod" and "sum" replace "*" and "+"
    2.22 @@ -121,8 +127,8 @@
    2.23  INCOMPATIBILITY.
    2.24  
    2.25  * Inductive package: offers new command "inductive_simps" to automatically
    2.26 -  derive instantiated and simplified equations for inductive predicates,
    2.27 -  similar to inductive_cases.
    2.28 +derive instantiated and simplified equations for inductive predicates,
    2.29 +similar to inductive_cases.
    2.30  
    2.31  
    2.32  *** ML ***
     3.1 --- a/doc-src/Codegen/Thy/Foundations.thy	Tue Aug 17 13:10:58 2010 +0200
     3.2 +++ b/doc-src/Codegen/Thy/Foundations.thy	Tue Aug 17 14:33:44 2010 +0200
     3.3 @@ -7,7 +7,6 @@
     3.4  subsection {* Code generator architecture \label{sec:architecture} *}
     3.5  
     3.6  text {*
     3.7 -
     3.8    The code generator is actually a framework consisting of different
     3.9    components which can be customised individually.
    3.10  
     4.1 --- a/doc-src/Codegen/Thy/Refinement.thy	Tue Aug 17 13:10:58 2010 +0200
     4.2 +++ b/doc-src/Codegen/Thy/Refinement.thy	Tue Aug 17 14:33:44 2010 +0200
     4.3 @@ -70,23 +70,17 @@
     4.4  text %quote {*@{code_stmts fib (consts) fib fib_step (Haskell)}*}
     4.5  
     4.6  
     4.7 -subsection {* Datatypes \label{sec:datatypes} *}
     4.8 +subsection {* Datatype refinement *}
     4.9  
    4.10  text {*
    4.11 -  Conceptually, any datatype is spanned by a set of
    4.12 -  \emph{constructors} of type @{text "\<tau> = \<dots> \<Rightarrow> \<kappa> \<alpha>\<^isub>1 \<dots> \<alpha>\<^isub>n"} where @{text
    4.13 -  "{\<alpha>\<^isub>1, \<dots>, \<alpha>\<^isub>n}"} is exactly the set of \emph{all} type variables in
    4.14 -  @{text "\<tau>"}.  The HOL datatype package by default registers any new
    4.15 -  datatype in the table of datatypes, which may be inspected using the
    4.16 -  @{command print_codesetup} command.
    4.17 -
    4.18 -  In some cases, it is appropriate to alter or extend this table.  As
    4.19 -  an example, we will develop an alternative representation of the
    4.20 -  queue example given in \secref{sec:queue_example}.  The amortised
    4.21 -  representation is convenient for generating code but exposes its
    4.22 -  \qt{implementation} details, which may be cumbersome when proving
    4.23 -  theorems about it.  Therefore, here is a simple, straightforward
    4.24 -  representation of queues:
    4.25 +  Selecting specific code equations \emph{and} datatype constructors
    4.26 +  leads to datatype refinement.  As an example, we will develop an
    4.27 +  alternative representation of the queue example given in
    4.28 +  \secref{sec:queue_example}.  The amortised representation is
    4.29 +  convenient for generating code but exposes its \qt{implementation}
    4.30 +  details, which may be cumbersome when proving theorems about it.
    4.31 +  Therefore, here is a simple, straightforward representation of
    4.32 +  queues:
    4.33  *}
    4.34  
    4.35  datatype %quote 'a queue = Queue "'a list"
    4.36 @@ -115,7 +109,18 @@
    4.37    \noindent Here we define a \qt{constructor} @{const "AQueue"} which
    4.38    is defined in terms of @{text "Queue"} and interprets its arguments
    4.39    according to what the \emph{content} of an amortised queue is supposed
    4.40 -  to be.  Equipped with this, we are able to prove the following equations
    4.41 +  to be.
    4.42 +
    4.43 +  The prerequisite for datatype constructors is only syntactical: a
    4.44 +  constructor must be of type @{text "\<tau> = \<dots> \<Rightarrow> \<kappa> \<alpha>\<^isub>1 \<dots> \<alpha>\<^isub>n"} where @{text
    4.45 +  "{\<alpha>\<^isub>1, \<dots>, \<alpha>\<^isub>n}"} is exactly the set of \emph{all} type variables in
    4.46 +  @{text "\<tau>"}; then @{text "\<kappa>"} is its corresponding datatype.  The
    4.47 +  HOL datatype package by default registers any new datatype with its
    4.48 +  constructors, but this may be changed using @{command
    4.49 +  code_datatype}; the currently chosen constructors can be inspected
    4.50 +  using the @{command print_codesetup} command.
    4.51 +
    4.52 +  Equipped with this, we are able to prove the following equations
    4.53    for our primitive queue operations which \qt{implement} the simple
    4.54    queues in an amortised fashion:
    4.55  *}
    4.56 @@ -151,28 +156,21 @@
    4.57  text %quote {*@{code_stmts empty enqueue dequeue (SML)}*}
    4.58  
    4.59  text {*
    4.60 -  \noindent From this example, it can be glimpsed that using own
    4.61 -  constructor sets is a little delicate since it changes the set of
    4.62 -  valid patterns for values of that type.  Without going into much
    4.63 -  detail, here some practical hints:
    4.64 -
    4.65 -  \begin{itemize}
    4.66 -
    4.67 -    \item When changing the constructor set for datatypes, take care
    4.68 -      to provide alternative equations for the @{text case} combinator.
    4.69 +  The same techniques can also be applied to types which are not
    4.70 +  specified as datatypes, e.g.~type @{typ int} is originally specified
    4.71 +  as quotient type by means of @{command typedef}, but for code
    4.72 +  generation constants allowing construction of binary numeral values
    4.73 +  are used as constructors for @{typ int}.
    4.74  
    4.75 -    \item Values in the target language need not to be normalised --
    4.76 -      different values in the target language may represent the same
    4.77 -      value in the logic.
    4.78 +  This approach however fails if the representation of a type demands
    4.79 +  invariants; this issue is discussed in the next section.
    4.80 +*}
    4.81 +
    4.82  
    4.83 -    \item Usually, a good methodology to deal with the subtleties of
    4.84 -      pattern matching is to see the type as an abstract type: provide
    4.85 -      a set of operations which operate on the concrete representation
    4.86 -      of the type, and derive further operations by combinations of
    4.87 -      these primitive ones, without relying on a particular
    4.88 -      representation.
    4.89 +subsection {* Datatype refinement involving invariants *}
    4.90  
    4.91 -  \end{itemize}
    4.92 +text {*
    4.93 +  FIXME
    4.94  *}
    4.95  
    4.96  end
     5.1 --- a/doc-src/Codegen/Thy/Setup.thy	Tue Aug 17 13:10:58 2010 +0200
     5.2 +++ b/doc-src/Codegen/Thy/Setup.thy	Tue Aug 17 14:33:44 2010 +0200
     5.3 @@ -1,5 +1,5 @@
     5.4  theory Setup
     5.5 -imports Complex_Main
     5.6 +imports Complex_Main More_List
     5.7  uses
     5.8    "../../antiquote_setup.ML"
     5.9    "../../more_antiquote.ML"
     6.1 --- a/doc-src/Codegen/Thy/document/Introduction.tex	Tue Aug 17 13:10:58 2010 +0200
     6.2 +++ b/doc-src/Codegen/Thy/document/Introduction.tex	Tue Aug 17 14:33:44 2010 +0200
     6.3 @@ -141,7 +141,8 @@
     6.4  \isatypewriter%
     6.5  \noindent%
     6.6  \hspace*{0pt}structure Example :~sig\\
     6.7 -\hspace*{0pt} ~val foldl :~('a -> 'b -> 'a) -> 'a -> 'b list -> 'a\\
     6.8 +\hspace*{0pt} ~val id :~'a -> 'a\\
     6.9 +\hspace*{0pt} ~val fold :~('a -> 'b -> 'b) -> 'a list -> 'b -> 'b\\
    6.10  \hspace*{0pt} ~val rev :~'a list -> 'a list\\
    6.11  \hspace*{0pt} ~datatype 'a queue = AQueue of 'a list * 'a list\\
    6.12  \hspace*{0pt} ~val empty :~'a queue\\
    6.13 @@ -149,10 +150,12 @@
    6.14  \hspace*{0pt} ~val enqueue :~'a -> 'a queue -> 'a queue\\
    6.15  \hspace*{0pt}end = struct\\
    6.16  \hspace*{0pt}\\
    6.17 -\hspace*{0pt}fun foldl f a [] = a\\
    6.18 -\hspace*{0pt} ~| foldl f a (x ::~xs) = foldl f (f a x) xs;\\
    6.19 +\hspace*{0pt}fun id x = (fn xa => xa) x;\\
    6.20  \hspace*{0pt}\\
    6.21 -\hspace*{0pt}fun rev xs = foldl (fn xsa => fn x => x ::~xsa) [] xs;\\
    6.22 +\hspace*{0pt}fun fold f [] = id\\
    6.23 +\hspace*{0pt} ~| fold f (x ::~xs) = fold f xs o f x;\\
    6.24 +\hspace*{0pt}\\
    6.25 +\hspace*{0pt}fun rev xs = fold (fn a => fn b => a ::~b) xs [];\\
    6.26  \hspace*{0pt}\\
    6.27  \hspace*{0pt}datatype 'a queue = AQueue of 'a list * 'a list;\\
    6.28  \hspace*{0pt}\\
     7.1 --- a/doc-src/Codegen/Thy/document/Refinement.tex	Tue Aug 17 13:10:58 2010 +0200
     7.2 +++ b/doc-src/Codegen/Thy/document/Refinement.tex	Tue Aug 17 14:33:44 2010 +0200
     7.3 @@ -191,24 +191,19 @@
     7.4  %
     7.5  \endisadelimquote
     7.6  %
     7.7 -\isamarkupsubsection{Datatypes \label{sec:datatypes}%
     7.8 +\isamarkupsubsection{Datatype refinement%
     7.9  }
    7.10  \isamarkuptrue%
    7.11  %
    7.12  \begin{isamarkuptext}%
    7.13 -Conceptually, any datatype is spanned by a set of
    7.14 -  \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
    7.15 -  \isa{{\isasymtau}}.  The HOL datatype package by default registers any new
    7.16 -  datatype in the table of datatypes, which may be inspected using the
    7.17 -  \hyperlink{command.print-codesetup}{\mbox{\isa{\isacommand{print{\isacharunderscore}codesetup}}}} command.
    7.18 -
    7.19 -  In some cases, it is appropriate to alter or extend this table.  As
    7.20 -  an example, we will develop an alternative representation of the
    7.21 -  queue example given in \secref{sec:queue_example}.  The amortised
    7.22 -  representation is convenient for generating code but exposes its
    7.23 -  \qt{implementation} details, which may be cumbersome when proving
    7.24 -  theorems about it.  Therefore, here is a simple, straightforward
    7.25 -  representation of queues:%
    7.26 +Selecting specific code equations \emph{and} datatype constructors
    7.27 +  leads to datatype refinement.  As an example, we will develop an
    7.28 +  alternative representation of the queue example given in
    7.29 +  \secref{sec:queue_example}.  The amortised representation is
    7.30 +  convenient for generating code but exposes its \qt{implementation}
    7.31 +  details, which may be cumbersome when proving theorems about it.
    7.32 +  Therefore, here is a simple, straightforward representation of
    7.33 +  queues:%
    7.34  \end{isamarkuptext}%
    7.35  \isamarkuptrue%
    7.36  %
    7.37 @@ -267,7 +262,16 @@
    7.38  \noindent Here we define a \qt{constructor} \isa{AQueue} which
    7.39    is defined in terms of \isa{Queue} and interprets its arguments
    7.40    according to what the \emph{content} of an amortised queue is supposed
    7.41 -  to be.  Equipped with this, we are able to prove the following equations
    7.42 +  to be.
    7.43 +
    7.44 +  The prerequisite for datatype constructors is only syntactical: a
    7.45 +  constructor must be 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
    7.46 +  \isa{{\isasymtau}}; then \isa{{\isasymkappa}} is its corresponding datatype.  The
    7.47 +  HOL datatype package by default registers any new datatype with its
    7.48 +  constructors, but this may be changed using \hyperlink{command.code-datatype}{\mbox{\isa{\isacommand{code{\isacharunderscore}datatype}}}}; the currently chosen constructors can be inspected
    7.49 +  using the \hyperlink{command.print-codesetup}{\mbox{\isa{\isacommand{print{\isacharunderscore}codesetup}}}} command.
    7.50 +
    7.51 +  Equipped with this, we are able to prove the following equations
    7.52    for our primitive queue operations which \qt{implement} the simple
    7.53    queues in an amortised fashion:%
    7.54  \end{isamarkuptext}%
    7.55 @@ -347,7 +351,8 @@
    7.56  \isatypewriter%
    7.57  \noindent%
    7.58  \hspace*{0pt}structure Example :~sig\\
    7.59 -\hspace*{0pt} ~val foldl :~('a -> 'b -> 'a) -> 'a -> 'b list -> 'a\\
    7.60 +\hspace*{0pt} ~val id :~'a -> 'a\\
    7.61 +\hspace*{0pt} ~val fold :~('a -> 'b -> 'b) -> 'a list -> 'b -> 'b\\
    7.62  \hspace*{0pt} ~val rev :~'a list -> 'a list\\
    7.63  \hspace*{0pt} ~val null :~'a list -> bool\\
    7.64  \hspace*{0pt} ~datatype 'a queue = AQueue of 'a list * 'a list\\
    7.65 @@ -356,10 +361,12 @@
    7.66  \hspace*{0pt} ~val enqueue :~'a -> 'a queue -> 'a queue\\
    7.67  \hspace*{0pt}end = struct\\
    7.68  \hspace*{0pt}\\
    7.69 -\hspace*{0pt}fun foldl f a [] = a\\
    7.70 -\hspace*{0pt} ~| foldl f a (x ::~xs) = foldl f (f a x) xs;\\
    7.71 +\hspace*{0pt}fun id x = (fn xa => xa) x;\\
    7.72  \hspace*{0pt}\\
    7.73 -\hspace*{0pt}fun rev xs = foldl (fn xsa => fn x => x ::~xsa) [] xs;\\
    7.74 +\hspace*{0pt}fun fold f [] = id\\
    7.75 +\hspace*{0pt} ~| fold f (x ::~xs) = fold f xs o f x;\\
    7.76 +\hspace*{0pt}\\
    7.77 +\hspace*{0pt}fun rev xs = fold (fn a => fn b => a ::~b) xs [];\\
    7.78  \hspace*{0pt}\\
    7.79  \hspace*{0pt}fun null [] = true\\
    7.80  \hspace*{0pt} ~| null (x ::~xs) = false;\\
    7.81 @@ -387,28 +394,23 @@
    7.82  \endisadelimquote
    7.83  %
    7.84  \begin{isamarkuptext}%
    7.85 -\noindent From this example, it can be glimpsed that using own
    7.86 -  constructor sets is a little delicate since it changes the set of
    7.87 -  valid patterns for values of that type.  Without going into much
    7.88 -  detail, here some practical hints:
    7.89 -
    7.90 -  \begin{itemize}
    7.91 -
    7.92 -    \item When changing the constructor set for datatypes, take care
    7.93 -      to provide alternative equations for the \isa{case} combinator.
    7.94 +The same techniques can also be applied to types which are not
    7.95 +  specified as datatypes, e.g.~type \isa{int} is originally specified
    7.96 +  as quotient type by means of \hyperlink{command.typedef}{\mbox{\isa{\isacommand{typedef}}}}, but for code
    7.97 +  generation constants allowing construction of binary numeral values
    7.98 +  are used as constructors for \isa{int}.
    7.99  
   7.100 -    \item Values in the target language need not to be normalised --
   7.101 -      different values in the target language may represent the same
   7.102 -      value in the logic.
   7.103 -
   7.104 -    \item Usually, a good methodology to deal with the subtleties of
   7.105 -      pattern matching is to see the type as an abstract type: provide
   7.106 -      a set of operations which operate on the concrete representation
   7.107 -      of the type, and derive further operations by combinations of
   7.108 -      these primitive ones, without relying on a particular
   7.109 -      representation.
   7.110 -
   7.111 -  \end{itemize}%
   7.112 +  This approach however fails if the representation of a type demands
   7.113 +  invariants; this issue is discussed in the next section.%
   7.114 +\end{isamarkuptext}%
   7.115 +\isamarkuptrue%
   7.116 +%
   7.117 +\isamarkupsubsection{Datatype refinement involving invariants%
   7.118 +}
   7.119 +\isamarkuptrue%
   7.120 +%
   7.121 +\begin{isamarkuptext}%
   7.122 +FIXME%
   7.123  \end{isamarkuptext}%
   7.124  \isamarkuptrue%
   7.125  %
     8.1 --- a/doc-src/Codegen/Thy/examples/example.ML	Tue Aug 17 13:10:58 2010 +0200
     8.2 +++ b/doc-src/Codegen/Thy/examples/example.ML	Tue Aug 17 14:33:44 2010 +0200
     8.3 @@ -1,5 +1,6 @@
     8.4  structure Example : sig
     8.5 -  val foldl : ('a -> 'b -> 'a) -> 'a -> 'b list -> 'a
     8.6 +  val id : 'a -> 'a
     8.7 +  val fold : ('a -> 'b -> 'b) -> 'a list -> 'b -> 'b
     8.8    val rev : 'a list -> 'a list
     8.9    datatype 'a queue = AQueue of 'a list * 'a list
    8.10    val empty : 'a queue
    8.11 @@ -7,10 +8,12 @@
    8.12    val enqueue : 'a -> 'a queue -> 'a queue
    8.13  end = struct
    8.14  
    8.15 -fun foldl f a [] = a
    8.16 -  | foldl f a (x :: xs) = foldl f (f a x) xs;
    8.17 +fun id x = (fn xa => xa) x;
    8.18  
    8.19 -fun rev xs = foldl (fn xsa => fn x => x :: xsa) [] xs;
    8.20 +fun fold f [] = id
    8.21 +  | fold f (x :: xs) = fold f xs o f x;
    8.22 +
    8.23 +fun rev xs = fold (fn a => fn b => a :: b) xs [];
    8.24  
    8.25  datatype 'a queue = AQueue of 'a list * 'a list;
    8.26  
     9.1 --- a/doc-src/IsarRef/Thy/HOL_Specific.thy	Tue Aug 17 13:10:58 2010 +0200
     9.2 +++ b/doc-src/IsarRef/Thy/HOL_Specific.thy	Tue Aug 17 14:33:44 2010 +0200
     9.3 @@ -1018,7 +1018,7 @@
     9.4      target: 'OCaml' | 'SML' | 'Haskell'
     9.5      ;
     9.6  
     9.7 -    'code' ( 'del' ) ?
     9.8 +    'code' ( 'del' | 'abstype' | 'abstract' ) ?
     9.9      ;
    9.10  
    9.11      'code\_abort' ( const + )
    9.12 @@ -1104,9 +1104,11 @@
    9.13    declaration.
    9.14  
    9.15    \item @{attribute (HOL) code} explicitly selects (or with option
    9.16 -  ``@{text "del"}'' deselects) a code equation for code
    9.17 -  generation.  Usually packages introducing code equations provide
    9.18 -  a reasonable default setup for selection.
    9.19 +  ``@{text "del"}'' deselects) a code equation for code generation.
    9.20 +  Usually packages introducing code equations provide a reasonable
    9.21 +  default setup for selection.  Variants @{text "code abstype"} and
    9.22 +  @{text "code abstract"} declare abstract datatype certificates or
    9.23 +  code equations on abstract datatype representations respectively.
    9.24  
    9.25    \item @{command (HOL) "code_abort"} declares constants which are not
    9.26    required to have a definition by means of code equations; if
    10.1 --- a/doc-src/IsarRef/Thy/document/HOL_Specific.tex	Tue Aug 17 13:10:58 2010 +0200
    10.2 +++ b/doc-src/IsarRef/Thy/document/HOL_Specific.tex	Tue Aug 17 14:33:44 2010 +0200
    10.3 @@ -1034,7 +1034,7 @@
    10.4      target: 'OCaml' | 'SML' | 'Haskell'
    10.5      ;
    10.6  
    10.7 -    'code' ( 'del' ) ?
    10.8 +    'code' ( 'del' | 'abstype' | 'abstract' ) ?
    10.9      ;
   10.10  
   10.11      'code\_abort' ( const + )
   10.12 @@ -1117,9 +1117,11 @@
   10.13    declaration.
   10.14  
   10.15    \item \hyperlink{attribute.HOL.code}{\mbox{\isa{code}}} explicitly selects (or with option
   10.16 -  ``\isa{{\isachardoublequote}del{\isachardoublequote}}'' deselects) a code equation for code
   10.17 -  generation.  Usually packages introducing code equations provide
   10.18 -  a reasonable default setup for selection.
   10.19 +  ``\isa{{\isachardoublequote}del{\isachardoublequote}}'' deselects) a code equation for code generation.
   10.20 +  Usually packages introducing code equations provide a reasonable
   10.21 +  default setup for selection.  Variants \isa{{\isachardoublequote}code\ abstype{\isachardoublequote}} and
   10.22 +  \isa{{\isachardoublequote}code\ abstract{\isachardoublequote}} declare abstract datatype certificates or
   10.23 +  code equations on abstract datatype representations respectively.
   10.24  
   10.25    \item \hyperlink{command.HOL.code-abort}{\mbox{\isa{\isacommand{code{\isacharunderscore}abort}}}} declares constants which are not
   10.26    required to have a definition by means of code equations; if