--- a/CONTRIBUTORS Tue Aug 17 16:49:51 2010 +0200
+++ b/CONTRIBUTORS Tue Aug 17 17:01:31 2010 +0200
@@ -6,6 +6,9 @@
Contributions to this Isabelle version
--------------------------------------
+* July 2010: Florian Haftmann, TUM
+ Reworking and extension of the Isabelle/HOL framework.
+
Contributions to Isabelle2009-2
--------------------------------------
--- a/NEWS Tue Aug 17 16:49:51 2010 +0200
+++ b/NEWS Tue Aug 17 17:01:31 2010 +0200
@@ -35,11 +35,17 @@
*** HOL ***
+* Session Imperative_HOL: revamped, corrected dozens of inadequacies.
+INCOMPATIBILITY.
+
+* Quickcheck in locales considers interpretations of that locale for
+counter example search.
+
* Theory Library/Monad_Syntax provides do-syntax for monad types. Syntax
in Library/State_Monad has been changed to avoid ambiguities.
INCOMPATIBILITY.
-* code generator: export_code without explicit file declaration prints
+* Code generator: export_code without explicit file declaration prints
to standard output. INCOMPATIBILITY.
* Abolished symbol type names: "prod" and "sum" replace "*" and "+"
@@ -121,8 +127,8 @@
INCOMPATIBILITY.
* Inductive package: offers new command "inductive_simps" to automatically
- derive instantiated and simplified equations for inductive predicates,
- similar to inductive_cases.
+derive instantiated and simplified equations for inductive predicates,
+similar to inductive_cases.
*** ML ***
--- a/doc-src/Codegen/Thy/Foundations.thy Tue Aug 17 16:49:51 2010 +0200
+++ b/doc-src/Codegen/Thy/Foundations.thy Tue Aug 17 17:01:31 2010 +0200
@@ -7,7 +7,6 @@
subsection {* Code generator architecture \label{sec:architecture} *}
text {*
-
The code generator is actually a framework consisting of different
components which can be customised individually.
--- a/doc-src/Codegen/Thy/Refinement.thy Tue Aug 17 16:49:51 2010 +0200
+++ b/doc-src/Codegen/Thy/Refinement.thy Tue Aug 17 17:01:31 2010 +0200
@@ -70,23 +70,17 @@
text %quote {*@{code_stmts fib (consts) fib fib_step (Haskell)}*}
-subsection {* Datatypes \label{sec:datatypes} *}
+subsection {* Datatype refinement *}
text {*
- Conceptually, any datatype is spanned by a set of
- \emph{constructors} of type @{text "\<tau> = \<dots> \<Rightarrow> \<kappa> \<alpha>\<^isub>1 \<dots> \<alpha>\<^isub>n"} where @{text
- "{\<alpha>\<^isub>1, \<dots>, \<alpha>\<^isub>n}"} is exactly the set of \emph{all} type variables in
- @{text "\<tau>"}. 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:queue_example}. 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:
+ Selecting specific code equations \emph{and} datatype constructors
+ leads to datatype refinement. As an example, we will develop an
+ alternative representation of the queue example given in
+ \secref{sec:queue_example}. 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"
@@ -115,7 +109,18 @@
\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
+ to be.
+
+ The prerequisite for datatype constructors is only syntactical: a
+ constructor must be of type @{text "\<tau> = \<dots> \<Rightarrow> \<kappa> \<alpha>\<^isub>1 \<dots> \<alpha>\<^isub>n"} where @{text
+ "{\<alpha>\<^isub>1, \<dots>, \<alpha>\<^isub>n}"} is exactly the set of \emph{all} type variables in
+ @{text "\<tau>"}; then @{text "\<kappa>"} is its corresponding datatype. The
+ HOL datatype package by default registers any new datatype with its
+ constructors, but this may be changed using @{command
+ code_datatype}; the currently chosen constructors can be inspected
+ using the @{command print_codesetup} command.
+
+ 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:
*}
@@ -151,28 +156,21 @@
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.
+ The same techniques can also be applied to types which are not
+ specified as datatypes, e.g.~type @{typ int} is originally specified
+ as quotient type by means of @{command typedef}, but for code
+ generation constants allowing construction of binary numeral values
+ are used as constructors for @{typ int}.
- \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.
+ This approach however fails if the representation of a type demands
+ invariants; this issue is discussed in the next section.
+*}
+
- \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.
+subsection {* Datatype refinement involving invariants *}
- \end{itemize}
+text {*
+ FIXME
*}
end
--- a/doc-src/Codegen/Thy/Setup.thy Tue Aug 17 16:49:51 2010 +0200
+++ b/doc-src/Codegen/Thy/Setup.thy Tue Aug 17 17:01:31 2010 +0200
@@ -1,5 +1,5 @@
theory Setup
-imports Complex_Main
+imports Complex_Main More_List
uses
"../../antiquote_setup.ML"
"../../more_antiquote.ML"
--- a/doc-src/Codegen/Thy/document/Introduction.tex Tue Aug 17 16:49:51 2010 +0200
+++ b/doc-src/Codegen/Thy/document/Introduction.tex Tue Aug 17 17:01:31 2010 +0200
@@ -141,7 +141,8 @@
\isatypewriter%
\noindent%
\hspace*{0pt}structure Example :~sig\\
-\hspace*{0pt} ~val foldl :~('a -> 'b -> 'a) -> 'a -> 'b list -> 'a\\
+\hspace*{0pt} ~val id :~'a -> 'a\\
+\hspace*{0pt} ~val fold :~('a -> 'b -> 'b) -> 'a list -> 'b -> 'b\\
\hspace*{0pt} ~val rev :~'a list -> 'a list\\
\hspace*{0pt} ~datatype 'a queue = AQueue of 'a list * 'a list\\
\hspace*{0pt} ~val empty :~'a queue\\
@@ -149,10 +150,12 @@
\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}fun id x = (fn xa => xa) x;\\
\hspace*{0pt}\\
-\hspace*{0pt}fun rev xs = foldl (fn xsa => fn x => x ::~xsa) [] xs;\\
+\hspace*{0pt}fun fold f [] = id\\
+\hspace*{0pt} ~| fold f (x ::~xs) = fold f xs o f x;\\
+\hspace*{0pt}\\
+\hspace*{0pt}fun rev xs = fold (fn a => fn b => a ::~b) xs [];\\
\hspace*{0pt}\\
\hspace*{0pt}datatype 'a queue = AQueue of 'a list * 'a list;\\
\hspace*{0pt}\\
--- a/doc-src/Codegen/Thy/document/Refinement.tex Tue Aug 17 16:49:51 2010 +0200
+++ b/doc-src/Codegen/Thy/document/Refinement.tex Tue Aug 17 17:01:31 2010 +0200
@@ -191,24 +191,19 @@
%
\endisadelimquote
%
-\isamarkupsubsection{Datatypes \label{sec:datatypes}%
+\isamarkupsubsection{Datatype refinement%
}
\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:queue_example}. 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:%
+Selecting specific code equations \emph{and} datatype constructors
+ leads to datatype refinement. As an example, we will develop an
+ alternative representation of the queue example given in
+ \secref{sec:queue_example}. 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%
%
@@ -267,7 +262,16 @@
\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
+ to be.
+
+ The prerequisite for datatype constructors is only syntactical: a
+ 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
+ \isa{{\isasymtau}}; then \isa{{\isasymkappa}} is its corresponding datatype. The
+ HOL datatype package by default registers any new datatype with its
+ constructors, but this may be changed using \hyperlink{command.code-datatype}{\mbox{\isa{\isacommand{code{\isacharunderscore}datatype}}}}; the currently chosen constructors can be inspected
+ using the \hyperlink{command.print-codesetup}{\mbox{\isa{\isacommand{print{\isacharunderscore}codesetup}}}} command.
+
+ 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}%
@@ -347,7 +351,8 @@
\isatypewriter%
\noindent%
\hspace*{0pt}structure Example :~sig\\
-\hspace*{0pt} ~val foldl :~('a -> 'b -> 'a) -> 'a -> 'b list -> 'a\\
+\hspace*{0pt} ~val id :~'a -> 'a\\
+\hspace*{0pt} ~val fold :~('a -> 'b -> 'b) -> 'a list -> 'b -> 'b\\
\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\\
@@ -356,10 +361,12 @@
\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}fun id x = (fn xa => xa) x;\\
\hspace*{0pt}\\
-\hspace*{0pt}fun rev xs = foldl (fn xsa => fn x => x ::~xsa) [] xs;\\
+\hspace*{0pt}fun fold f [] = id\\
+\hspace*{0pt} ~| fold f (x ::~xs) = fold f xs o f x;\\
+\hspace*{0pt}\\
+\hspace*{0pt}fun rev xs = fold (fn a => fn b => a ::~b) xs [];\\
\hspace*{0pt}\\
\hspace*{0pt}fun null [] = true\\
\hspace*{0pt} ~| null (x ::~xs) = false;\\
@@ -387,28 +394,23 @@
\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.
+The same techniques can also be applied to types which are not
+ specified as datatypes, e.g.~type \isa{int} is originally specified
+ as quotient type by means of \hyperlink{command.typedef}{\mbox{\isa{\isacommand{typedef}}}}, but for code
+ generation constants allowing construction of binary numeral values
+ are used as constructors for \isa{int}.
- \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}%
+ This approach however fails if the representation of a type demands
+ invariants; this issue is discussed in the next section.%
+\end{isamarkuptext}%
+\isamarkuptrue%
+%
+\isamarkupsubsection{Datatype refinement involving invariants%
+}
+\isamarkuptrue%
+%
+\begin{isamarkuptext}%
+FIXME%
\end{isamarkuptext}%
\isamarkuptrue%
%
--- a/doc-src/Codegen/Thy/examples/example.ML Tue Aug 17 16:49:51 2010 +0200
+++ b/doc-src/Codegen/Thy/examples/example.ML Tue Aug 17 17:01:31 2010 +0200
@@ -1,5 +1,6 @@
structure Example : sig
- val foldl : ('a -> 'b -> 'a) -> 'a -> 'b list -> 'a
+ val id : 'a -> 'a
+ val fold : ('a -> 'b -> 'b) -> 'a list -> 'b -> 'b
val rev : 'a list -> 'a list
datatype 'a queue = AQueue of 'a list * 'a list
val empty : 'a queue
@@ -7,10 +8,12 @@
val enqueue : 'a -> 'a queue -> 'a queue
end = struct
-fun foldl f a [] = a
- | foldl f a (x :: xs) = foldl f (f a x) xs;
+fun id x = (fn xa => xa) x;
-fun rev xs = foldl (fn xsa => fn x => x :: xsa) [] xs;
+fun fold f [] = id
+ | fold f (x :: xs) = fold f xs o f x;
+
+fun rev xs = fold (fn a => fn b => a :: b) xs [];
datatype 'a queue = AQueue of 'a list * 'a list;
--- a/doc-src/IsarRef/Thy/HOL_Specific.thy Tue Aug 17 16:49:51 2010 +0200
+++ b/doc-src/IsarRef/Thy/HOL_Specific.thy Tue Aug 17 17:01:31 2010 +0200
@@ -1018,7 +1018,7 @@
target: 'OCaml' | 'SML' | 'Haskell'
;
- 'code' ( 'del' ) ?
+ 'code' ( 'del' | 'abstype' | 'abstract' ) ?
;
'code\_abort' ( const + )
@@ -1104,9 +1104,11 @@
declaration.
\item @{attribute (HOL) code} explicitly selects (or with option
- ``@{text "del"}'' deselects) a code equation for code
- generation. Usually packages introducing code equations provide
- a reasonable default setup for selection.
+ ``@{text "del"}'' deselects) a code equation for code generation.
+ Usually packages introducing code equations provide a reasonable
+ default setup for selection. Variants @{text "code abstype"} and
+ @{text "code abstract"} declare abstract datatype certificates or
+ code equations on abstract datatype representations respectively.
\item @{command (HOL) "code_abort"} declares constants which are not
required to have a definition by means of code equations; if
--- a/doc-src/IsarRef/Thy/document/HOL_Specific.tex Tue Aug 17 16:49:51 2010 +0200
+++ b/doc-src/IsarRef/Thy/document/HOL_Specific.tex Tue Aug 17 17:01:31 2010 +0200
@@ -1034,7 +1034,7 @@
target: 'OCaml' | 'SML' | 'Haskell'
;
- 'code' ( 'del' ) ?
+ 'code' ( 'del' | 'abstype' | 'abstract' ) ?
;
'code\_abort' ( const + )
@@ -1117,9 +1117,11 @@
declaration.
\item \hyperlink{attribute.HOL.code}{\mbox{\isa{code}}} explicitly selects (or with option
- ``\isa{{\isachardoublequote}del{\isachardoublequote}}'' deselects) a code equation for code
- generation. Usually packages introducing code equations provide
- a reasonable default setup for selection.
+ ``\isa{{\isachardoublequote}del{\isachardoublequote}}'' deselects) a code equation for code generation.
+ Usually packages introducing code equations provide a reasonable
+ default setup for selection. Variants \isa{{\isachardoublequote}code\ abstype{\isachardoublequote}} and
+ \isa{{\isachardoublequote}code\ abstract{\isachardoublequote}} declare abstract datatype certificates or
+ code equations on abstract datatype representations respectively.
\item \hyperlink{command.HOL.code-abort}{\mbox{\isa{\isacommand{code{\isacharunderscore}abort}}}} declares constants which are not
required to have a definition by means of code equations; if
--- a/src/HOL/Tools/ATP/atp_systems.ML Tue Aug 17 16:49:51 2010 +0200
+++ b/src/HOL/Tools/ATP/atp_systems.ML Tue Aug 17 17:01:31 2010 +0200
@@ -8,7 +8,9 @@
signature ATP_SYSTEMS =
sig
datatype failure =
- Unprovable | IncompleteUnprovable | MalformedOutput | UnknownError
+ Unprovable | IncompleteUnprovable | CantConnect | TimedOut | OutOfResources |
+ OldSpass | OldVampire | NoPerl | NoLibwwwPerl | MalformedInput |
+ MalformedOutput | UnknownError
type prover_config =
{exec: string * string,
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Pure/General/linear_set.ML Tue Aug 17 17:01:31 2010 +0200
@@ -0,0 +1,142 @@
+(* Title: Pure/General/linear_set.ML
+ Author: Makarius
+
+Sets with canonical linear order, or immutable linked-lists.
+*)
+
+signature LINEAR_SET =
+sig
+ type key
+ type 'a T
+ exception DUPLICATE of key
+ exception UNDEFINED of key
+ exception NEXT_UNDEFINED of key option
+ val empty: 'a T
+ val is_empty: 'a T -> bool
+ val defined: 'a T -> key -> bool
+ val lookup: 'a T -> key -> 'a option
+ val update: key * 'a -> 'a T -> 'a T
+ val fold: key option ->
+ ((key option * key) * 'a -> 'b -> 'b) -> 'a T -> 'b -> 'b
+ val get_first: key option ->
+ ((key option * key) * 'a -> bool) -> 'a T -> ((key option * key) * 'a) option
+ val get_after: 'a T -> key option -> key option
+ val insert_after: key option -> key * 'a -> 'a T -> 'a T
+ val delete_after: key option -> 'a T -> 'a T
+end;
+
+functor Linear_Set(Key: KEY): LINEAR_SET =
+struct
+
+(* type key *)
+
+type key = Key.key;
+structure Table = Table(Key);
+
+exception DUPLICATE of key;
+exception UNDEFINED of key;
+exception NEXT_UNDEFINED of key option;
+
+
+(* raw entries *)
+
+fun the_entry entries key =
+ (case Table.lookup entries key of
+ NONE => raise UNDEFINED key
+ | SOME entry => entry);
+
+fun next_entry entries key = snd (the_entry entries key);
+
+fun put_entry entry entries = Table.update entry entries;
+
+fun new_entry entry entries = Table.update_new entry entries
+ handle Table.DUP key => raise DUPLICATE key;
+
+fun del_entry key entries = Table.delete_safe key entries;
+
+
+(* set representation and basic operations *)
+
+datatype 'a T = Set of {start: key option, entries: ('a * key option) Table.table};
+
+fun make_set (start, entries) = Set {start = start, entries = entries};
+fun map_set f (Set {start, entries}) = make_set (f (start, entries));
+
+fun start_of (Set {start, ...}) = start;
+fun entries_of (Set {entries, ...}) = entries;
+
+val empty = Set {start = NONE, entries = Table.empty};
+fun is_empty set = is_none (start_of set);
+
+fun defined set key = Table.defined (entries_of set) key;
+
+fun lookup set key = Option.map fst (Table.lookup (entries_of set) key);
+
+fun update (key, x) = map_set (fn (start, entries) =>
+ (start, put_entry (key, (x, next_entry entries key)) entries));
+
+
+(* iterate entries *)
+
+fun optional_start set NONE = start_of set
+ | optional_start _ some = some;
+
+fun fold opt_start f set =
+ let
+ val entries = entries_of set;
+ fun apply _ NONE y = y
+ | apply prev (SOME key) y =
+ let
+ val (x, next) = the_entry entries key;
+ val item = ((prev, key), x);
+ in apply (SOME key) next (f item y) end;
+ in apply NONE (optional_start set opt_start) end;
+
+fun get_first opt_start P set =
+ let
+ val entries = entries_of set;
+ fun first _ NONE = NONE
+ | first prev (SOME key) =
+ let
+ val (x, next) = the_entry entries key;
+ val item = ((prev, key), x);
+ in if P item then SOME item else first (SOME key) next end;
+ in first NONE (optional_start set opt_start) end;
+
+
+(* relative addressing *)
+
+fun get_after set hook =
+ (case hook of
+ NONE => start_of set
+ | SOME key => next_entry (entries_of set) key);
+
+fun insert_after hook (key, x) = map_set (fn (start, entries) =>
+ (case hook of
+ NONE => (SOME key, new_entry (key, (x, start)) entries)
+ | SOME key1 =>
+ let
+ val (x1, next) = the_entry entries key1;
+ val entries' = entries
+ |> put_entry (key1, (x1, SOME key))
+ |> new_entry (key, (x, next));
+ in (start, entries') end));
+
+fun delete_after hook set = set |> map_set (fn (start, entries) =>
+ (case hook of
+ NONE =>
+ (case start of
+ NONE => raise NEXT_UNDEFINED NONE
+ | SOME key1 => (next_entry entries key1, del_entry key1 entries))
+ | SOME key1 =>
+ (case the_entry entries key1 of
+ (_, NONE) => raise NEXT_UNDEFINED (SOME key1)
+ | (x1, SOME key2) =>
+ let
+ val entries' = entries
+ |> put_entry (key1, (x1, next_entry entries key2))
+ |> del_entry key2;
+ in (start, entries') end)));
+
+end;
+
--- a/src/Pure/General/linear_set.scala Tue Aug 17 16:49:51 2010 +0200
+++ b/src/Pure/General/linear_set.scala Tue Aug 17 17:01:31 2010 +0200
@@ -25,8 +25,9 @@
implicit def canBuildFrom[A]: CanBuildFrom[Coll, A, Linear_Set[A]] = setCanBuildFrom[A]
override def empty[A] = new Linear_Set[A]
- class Duplicate(s: String) extends Exception(s)
- class Undefined(s: String) extends Exception(s)
+ class Duplicate[A](x: A) extends Exception
+ class Undefined[A](x: A) extends Exception
+ class Next_Undefined[A](x: Option[A]) extends Exception
}
@@ -43,19 +44,22 @@
protected val rep = Linear_Set.empty_rep[A]
- /* auxiliary operations */
+ /* relative addressing */
+ // FIXME check definedness??
def next(elem: A): Option[A] = rep.nexts.get(elem)
def prev(elem: A): Option[A] = rep.prevs.get(elem)
def get_after(hook: Option[A]): Option[A] =
hook match {
case None => rep.start
- case Some(elem) => next(elem)
+ case Some(elem) =>
+ if (!contains(elem)) throw new Linear_Set.Undefined(elem)
+ next(elem)
}
def insert_after(hook: Option[A], elem: A): Linear_Set[A] =
- if (contains(elem)) throw new Linear_Set.Duplicate(elem.toString)
+ if (contains(elem)) throw new Linear_Set.Duplicate(elem)
else
hook match {
case None =>
@@ -66,7 +70,7 @@
rep.nexts + (elem -> elem1), rep.prevs + (elem1 -> elem))
}
case Some(elem1) =>
- if (!contains(elem1)) throw new Linear_Set.Undefined(elem1.toString)
+ if (!contains(elem1)) throw new Linear_Set.Undefined(elem1)
else
rep.nexts.get(elem1) match {
case None =>
@@ -83,7 +87,7 @@
hook match {
case None =>
rep.start match {
- case None => throw new Linear_Set.Undefined("")
+ case None => throw new Linear_Set.Next_Undefined[A](None)
case Some(elem1) =>
rep.nexts.get(elem1) match {
case None => empty
@@ -92,10 +96,10 @@
}
}
case Some(elem1) =>
- if (!contains(elem1)) throw new Linear_Set.Undefined(elem1.toString)
+ if (!contains(elem1)) throw new Linear_Set.Undefined(elem1)
else
rep.nexts.get(elem1) match {
- case None => throw new Linear_Set.Undefined("")
+ case None => throw new Linear_Set.Next_Undefined(Some(elem1))
case Some(elem2) =>
rep.nexts.get(elem2) match {
case None =>
@@ -153,15 +157,15 @@
def iterator(elem: A): Iterator[A] =
if (contains(elem)) make_iterator(Some(elem), rep.nexts)
- else throw new Linear_Set.Undefined(elem.toString)
+ else throw new Linear_Set.Undefined(elem)
def reverse_iterator(elem: A): Iterator[A] =
if (contains(elem)) make_iterator(Some(elem), rep.prevs)
- else throw new Linear_Set.Undefined(elem.toString)
+ else throw new Linear_Set.Undefined(elem)
def + (elem: A): Linear_Set[A] = insert_after(rep.end, elem)
def - (elem: A): Linear_Set[A] =
- if (!contains(elem)) throw new Linear_Set.Undefined(elem.toString)
+ if (!contains(elem)) throw new Linear_Set.Undefined(elem)
else delete_after(prev(elem))
}
\ No newline at end of file
--- a/src/Pure/IsaMakefile Tue Aug 17 16:49:51 2010 +0200
+++ b/src/Pure/IsaMakefile Tue Aug 17 17:01:31 2010 +0200
@@ -80,6 +80,7 @@
General/graph.ML \
General/heap.ML \
General/integer.ML \
+ General/linear_set.ML \
General/long_name.ML \
General/markup.ML \
General/name_space.ML \
--- a/src/Pure/PIDE/document.ML Tue Aug 17 16:49:51 2010 +0200
+++ b/src/Pure/PIDE/document.ML Tue Aug 17 17:01:31 2010 +0200
@@ -15,7 +15,7 @@
val new_id: unit -> id
val parse_id: string -> id
val print_id: id -> string
- type edit = string * ((command_id * command_id option) list) option
+ type edit = string * ((command_id option * command_id option) list) option
type state
val init_state: state
val define_command: command_id -> string -> state -> state
@@ -55,82 +55,43 @@
(** document structure **)
-abstype entry = Entry of {next: command_id option, exec: exec_id option}
- and node = Node of entry Inttab.table (*unique entries indexed by command_id, start with no_id*)
+structure Entries = Linear_Set(type key = command_id val ord = int_ord);
+
+abstype node = Node of exec_id option Entries.T (*command entries with excecutions*)
and version = Version of node Graph.T (*development graph wrt. static imports*)
with
-
-(* command entries *)
-
-fun make_entry next exec = Entry {next = next, exec = exec};
-
-fun the_entry (Node entries) (id: command_id) =
- (case Inttab.lookup entries id of
- NONE => err_undef "command entry" id
- | SOME (Entry entry) => entry);
+val empty_node = Node Entries.empty;
+val empty_version = Version Graph.empty;
-fun put_entry (id: command_id, entry: entry) (Node entries) =
- Node (Inttab.update (id, entry) entries);
-
-fun put_entry_exec (id: command_id) exec node =
- let val {next, ...} = the_entry node id
- in put_entry (id, make_entry next exec) node end;
-
-fun reset_entry_exec id = put_entry_exec id NONE;
-fun set_entry_exec (id, exec_id) = put_entry_exec id (SOME exec_id);
+fun fold_entries start f (Node entries) = Entries.fold start f entries;
+fun first_entry start P (Node entries) = Entries.get_first start P entries;
-(* iterate entries *)
-
-fun fold_entries id0 f (node as Node entries) =
- let
- fun apply NONE x = x
- | apply (SOME id) x =
- let val entry = the_entry node id
- in apply (#next entry) (f (id, entry) x) end;
- in if Inttab.defined entries id0 then apply (SOME id0) else I end;
-
-fun first_entry P node =
- let
- fun first _ NONE = NONE
- | first prev (SOME id) =
- let val entry = the_entry node id
- in if P (id, entry) then SOME (prev, id, entry) else first (SOME id) (#next entry) end;
- in first NONE (SOME no_id) end;
-
-
-(* modify entries *)
-
-fun insert_after (id: command_id) (id2: command_id) node =
- let val {next, exec} = the_entry node id in
- node
- |> put_entry (id, make_entry (SOME id2) exec)
- |> put_entry (id2, make_entry next NONE)
- end;
-
-fun delete_after (id: command_id) node =
- let val {next, exec} = the_entry node id in
- (case next of
- NONE => error ("No next entry to delete: " ^ print_id id)
- | SOME id2 =>
- node |>
- (case #next (the_entry node id2) of
- NONE => put_entry (id, make_entry NONE exec)
- | SOME id3 => put_entry (id, make_entry (SOME id3) exec) #> reset_entry_exec id3))
- end;
-
-
-(* node edits *)
+(* node edits and associated executions *)
type edit =
- string * (*node name*)
- ((command_id * command_id option) list) option; (*NONE: remove, SOME: insert/remove commands*)
+ string *
+ (*NONE: remove node, SOME: insert/remove commands*)
+ ((command_id option * command_id option) list) option;
+
+fun the_entry (Node entries) id =
+ (case Entries.lookup entries id of
+ NONE => err_undef "command entry" id
+ | SOME entry => entry);
-val empty_node = Node (Inttab.make [(no_id, make_entry NONE (SOME no_id))]);
+fun update_entry (id, exec_id) (Node entries) =
+ Node (Entries.update (id, SOME exec_id) entries);
-fun edit_node (id, SOME id2) = insert_after id id2
- | edit_node (id, NONE) = delete_after id;
+fun reset_after id entries =
+ (case Entries.get_after entries id of
+ NONE => entries
+ | SOME next => Entries.update (next, NONE) entries);
+
+fun edit_node (hook, SOME id2) (Node entries) =
+ Node (Entries.insert_after hook (id2, NONE) entries)
+ | edit_node (hook, NONE) (Node entries) =
+ Node (entries |> Entries.delete_after hook |> reset_after hook);
(* version operations *)
@@ -138,19 +99,18 @@
fun nodes_of (Version nodes) = nodes;
val node_names_of = Graph.keys o nodes_of;
+fun get_node version name = Graph.get_node (nodes_of version) name
+ handle Graph.UNDEF _ => empty_node;
+
fun edit_nodes (name, SOME edits) (Version nodes) =
Version (nodes
|> Graph.default_node (name, empty_node)
|> Graph.map_node name (fold edit_node edits))
- | edit_nodes (name, NONE) (Version nodes) = Version (Graph.del_node name nodes);
-
-val empty_version = Version Graph.empty;
-
-fun the_node version name =
- Graph.get_node (nodes_of version) name handle Graph.UNDEF _ => empty_node;
+ | edit_nodes (name, NONE) (Version nodes) =
+ Version (Graph.del_node name nodes);
fun put_node name node (Version nodes) =
- Version (Graph.map_node name (K node) nodes); (* FIXME Graph.UNDEF !? *)
+ Version (Graph.map_node name (K node) nodes);
end;
@@ -238,22 +198,22 @@
local
-fun is_changed node' (id, {next = _, exec}) =
+fun is_changed node' ((_, id), exec) =
(case try (the_entry node') id of
NONE => true
- | SOME {next = _, exec = exec'} => exec' <> exec);
+ | SOME exec' => exec' <> exec);
fun new_exec name (id: command_id) (exec_id, updates, state) =
let
val exec = the_exec state exec_id;
val exec_id' = new_id ();
- val tr = the_command state id;
+ val future_tr = the_command state id;
val exec' =
Lazy.lazy (fn () =>
(case Lazy.force exec of
NONE => NONE
| SOME st =>
- let val exec_tr = Toplevel.put_id (print_id exec_id') (Future.join tr)
+ let val exec_tr = Toplevel.put_id (print_id exec_id') (Future.join future_tr)
in Toplevel.run_command name exec_tr st end));
val state' = define_exec exec_id' exec' state;
in (exec_id', (id, exec_id') :: updates, state') end;
@@ -266,15 +226,18 @@
val new_version = fold edit_nodes edits old_version;
fun update_node name (rev_updates, version, st) =
- let val node = the_node version name in
- (case first_entry (is_changed (the_node old_version name)) node of
+ let val node = get_node version name in
+ (case first_entry NONE (is_changed (get_node old_version name)) node of
NONE => (rev_updates, version, st)
- | SOME (prev, id, _) =>
+ | SOME ((prev, id), _) =>
let
- val prev_exec = the (#exec (the_entry node (the prev)));
+ val prev_exec =
+ (case prev of
+ NONE => no_id
+ | SOME prev_id => the_default no_id (the_entry node prev_id));
val (_, rev_upds, st') =
- fold_entries id (new_exec name o #1) node (prev_exec, [], st);
- val node' = fold set_entry_exec rev_upds node;
+ fold_entries (SOME id) (new_exec name o #2 o #1) node (prev_exec, [], st);
+ val node' = fold update_entry rev_upds node;
in (rev_upds @ rev_updates, put_node name node' version, st') end)
end;
@@ -306,8 +269,8 @@
node_names_of version |> map (fn name =>
Future.fork_pri 1 (fn () =>
(await_cancellation ();
- fold_entries no_id (fn (_, {exec, ...}) => fn () => force_exec exec)
- (the_node version name) ())));
+ fold_entries NONE (fn (_, exec) => fn () => force_exec exec)
+ (get_node version name) ())));
in (versions, commands, execs, execution') end);
end;
--- a/src/Pure/ROOT.ML Tue Aug 17 16:49:51 2010 +0200
+++ b/src/Pure/ROOT.ML Tue Aug 17 17:01:31 2010 +0200
@@ -42,6 +42,7 @@
use "General/ord_list.ML";
use "General/balanced_tree.ML";
use "General/graph.ML";
+use "General/linear_set.ML";
use "General/long_name.ML";
use "General/binding.ML";
use "General/name_space.ML";
--- a/src/Pure/System/isar_document.ML Tue Aug 17 16:49:51 2010 +0200
+++ b/src/Pure/System/isar_document.ML Tue Aug 17 17:01:31 2010 +0200
@@ -21,10 +21,14 @@
val old_id = Document.parse_id old_id_string;
val new_id = Document.parse_id new_id_string;
val edits =
- XML_Data.dest_list (XML_Data.dest_pair XML_Data.dest_string
- (XML_Data.dest_option (XML_Data.dest_list
- (XML_Data.dest_pair XML_Data.dest_int
- (XML_Data.dest_option XML_Data.dest_int))))) (YXML.parse_body edits_yxml);
+ XML_Data.dest_list
+ (XML_Data.dest_pair
+ XML_Data.dest_string
+ (XML_Data.dest_option
+ (XML_Data.dest_list
+ (XML_Data.dest_pair
+ (XML_Data.dest_option XML_Data.dest_int)
+ (XML_Data.dest_option XML_Data.dest_int))))) (YXML.parse_body edits_yxml);
val (updates, state') = Document.edit old_id new_id edits state;
val _ =
--- a/src/Pure/System/isar_document.scala Tue Aug 17 16:49:51 2010 +0200
+++ b/src/Pure/System/isar_document.scala Tue Aug 17 17:01:31 2010 +0200
@@ -51,14 +51,13 @@
def edit_version(old_id: Document.Version_ID, new_id: Document.Version_ID,
edits: List[Document.Edit[Document.Command_ID]])
{
- def make_id1(id1: Option[Document.Command_ID]): XML.Body =
- XML_Data.make_long(id1 getOrElse Document.NO_ID)
-
val arg =
XML_Data.make_list(
XML_Data.make_pair(XML_Data.make_string)(
XML_Data.make_option(XML_Data.make_list(
- XML_Data.make_pair(make_id1)(XML_Data.make_option(XML_Data.make_long))))))(edits)
+ XML_Data.make_pair(
+ XML_Data.make_option(XML_Data.make_long))(
+ XML_Data.make_option(XML_Data.make_long))))))(edits)
input("Isar_Document.edit_version",
Document.ID(old_id), Document.ID(new_id), YXML.string_of_body(arg))