--- a/doc-src/Classes/Thy/document/Classes.tex Wed Apr 01 16:03:00 2009 +0200
+++ b/doc-src/Classes/Thy/document/Classes.tex Wed Apr 01 16:03:18 2009 +0200
@@ -1191,7 +1191,7 @@
\hspace*{0pt}\\
\hspace*{0pt}pow{\char95}nat ::~forall a.~(Monoid a) => Nat -> a -> a;\\
\hspace*{0pt}pow{\char95}nat Zero{\char95}nat x = neutral;\\
-\hspace*{0pt}pow{\char95}nat (Suc n) xa = mult xa (pow{\char95}nat n xa);\\
+\hspace*{0pt}pow{\char95}nat (Suc n) x = mult x (pow{\char95}nat n x);\\
\hspace*{0pt}\\
\hspace*{0pt}pow{\char95}int ::~forall a.~(Group a) => Integer -> a -> a;\\
\hspace*{0pt}pow{\char95}int k x =\\
@@ -1272,8 +1272,8 @@
\hspace*{0pt} ~IntInf.int group;\\
\hspace*{0pt}\\
\hspace*{0pt}fun pow{\char95}nat A{\char95}~Zero{\char95}nat x = neutral (monoidl{\char95}monoid A{\char95})\\
-\hspace*{0pt} ~| pow{\char95}nat A{\char95}~(Suc n) xa =\\
-\hspace*{0pt} ~~~mult ((semigroup{\char95}monoidl o monoidl{\char95}monoid) A{\char95}) xa (pow{\char95}nat A{\char95}~n xa);\\
+\hspace*{0pt} ~| pow{\char95}nat A{\char95}~(Suc n) x =\\
+\hspace*{0pt} ~~~mult ((semigroup{\char95}monoidl o monoidl{\char95}monoid) A{\char95}) x (pow{\char95}nat A{\char95}~n x);\\
\hspace*{0pt}\\
\hspace*{0pt}fun pow{\char95}int A{\char95}~k x =\\
\hspace*{0pt} ~(if IntInf.<= ((0 :~IntInf.int),~k)\\
--- a/doc-src/Codegen/Thy/Adaption.thy Wed Apr 01 16:03:00 2009 +0200
+++ b/doc-src/Codegen/Thy/Adaption.thy Wed Apr 01 16:03:18 2009 +0200
@@ -59,42 +59,7 @@
supposed to be:
\begin{figure}[here]
- \begin{tikzpicture}[scale = 0.5]
- \tikzstyle water=[color = blue, thick]
- \tikzstyle ice=[color = black, very thick, cap = round, join = round, fill = white]
- \tikzstyle process=[color = green, semithick, ->]
- \tikzstyle adaption=[color = red, semithick, ->]
- \tikzstyle target=[color = black]
- \foreach \x in {0, ..., 24}
- \draw[style=water] (\x, 0.25) sin + (0.25, 0.25) cos + (0.25, -0.25) sin
- + (0.25, -0.25) cos + (0.25, 0.25);
- \draw[style=ice] (1, 0) --
- (3, 6) node[above, fill=white] {logic} -- (5, 0) -- cycle;
- \draw[style=ice] (9, 0) --
- (11, 6) node[above, fill=white] {intermediate language} -- (13, 0) -- cycle;
- \draw[style=ice] (15, -6) --
- (19, 6) node[above, fill=white] {target language} -- (23, -6) -- cycle;
- \draw[style=process]
- (3.5, 3) .. controls (7, 5) .. node[fill=white] {translation} (10.5, 3);
- \draw[style=process]
- (11.5, 3) .. controls (15, 5) .. node[fill=white] (serialisation) {serialisation} (18.5, 3);
- \node (adaption) at (11, -2) [style=adaption] {adaption};
- \node at (19, 3) [rotate=90] {generated};
- \node at (19.5, -5) {language};
- \node at (19.5, -3) {library};
- \node (includes) at (19.5, -1) {includes};
- \node (reserved) at (16.5, -3) [rotate=72] {reserved}; % proper 71.57
- \draw[style=process]
- (includes) -- (serialisation);
- \draw[style=process]
- (reserved) -- (serialisation);
- \draw[style=adaption]
- (adaption) -- (serialisation);
- \draw[style=adaption]
- (adaption) -- (includes);
- \draw[style=adaption]
- (adaption) -- (reserved);
- \end{tikzpicture}
+ \includegraphics{Thy/pictures/adaption}
\caption{The adaption principle}
\label{fig:adaption}
\end{figure}
--- a/doc-src/Codegen/Thy/Introduction.thy Wed Apr 01 16:03:00 2009 +0200
+++ b/doc-src/Codegen/Thy/Introduction.thy Wed Apr 01 16:03:18 2009 +0200
@@ -121,29 +121,7 @@
how it works.
\begin{figure}[h]
- \begin{tikzpicture}[x = 4.2cm, y = 1cm]
- \tikzstyle entity=[rounded corners, draw, thick, color = black, fill = white];
- \tikzstyle process=[ellipse, draw, thick, color = green, fill = white];
- \tikzstyle process_arrow=[->, semithick, color = green];
- \node (HOL) at (0, 4) [style=entity] {@{text "Isabelle/HOL"} theory};
- \node (eqn) at (2, 2) [style=entity] {code equations};
- \node (iml) at (2, 0) [style=entity] {intermediate language};
- \node (seri) at (1, 0) [style=process] {serialisation};
- \node (SML) at (0, 3) [style=entity] {@{text SML}};
- \node (OCaml) at (0, 2) [style=entity] {@{text OCaml}};
- \node (further) at (0, 1) [style=entity] {@{text "\<dots>"}};
- \node (Haskell) at (0, 0) [style=entity] {@{text Haskell}};
- \draw [style=process_arrow] (HOL) .. controls (2, 4) ..
- node [style=process, near start] {selection}
- node [style=process, near end] {preprocessing}
- (eqn);
- \draw [style=process_arrow] (eqn) -- node (transl) [style=process] {translation} (iml);
- \draw [style=process_arrow] (iml) -- (seri);
- \draw [style=process_arrow] (seri) -- (SML);
- \draw [style=process_arrow] (seri) -- (OCaml);
- \draw [style=process_arrow, dashed] (seri) -- (further);
- \draw [style=process_arrow] (seri) -- (Haskell);
- \end{tikzpicture}
+ \includegraphics{Thy/pictures/architecture}
\caption{Code generator architecture}
\label{fig:arch}
\end{figure}
@@ -164,35 +142,29 @@
\begin{itemize}
- \item Out of the vast collection of theorems proven in a
- \qn{theory}, a reasonable subset modelling
- code equations is \qn{selected}.
-
- \item On those selected theorems, certain
- transformations are carried out
- (\qn{preprocessing}). Their purpose is to turn theorems
- representing non- or badly executable
- specifications into equivalent but executable counterparts.
- The result is a structured collection of \qn{code theorems}.
+ \item Starting point is a collection of raw code equations in a
+ theory; due to proof irrelevance it is not relevant where they
+ stem from but typically they are either descendant of specification
+ tools or explicit proofs by the user.
+
+ \item Before these raw code equations are continued
+ with, they can be subjected to theorem transformations. This
+ \qn{preprocessor} is an interface which allows to apply the full
+ expressiveness of ML-based theorem transformations to code
+ generation. The result of the preprocessing step is a
+ structured collection of code equations.
- \item Before the selected code equations are continued with,
- they can be \qn{preprocessed}, i.e. subjected to theorem
- transformations. This \qn{preprocessor} is an interface which
- allows to apply
- the full expressiveness of ML-based theorem transformations
- to code generation; motivating examples are shown below, see
- \secref{sec:preproc}.
- The result of the preprocessing step is a structured collection
- of code equations.
-
- \item These code equations are \qn{translated} to a program
- in an abstract intermediate language. Think of it as a kind
+ \item These code equations are \qn{translated} to a program in an
+ abstract intermediate language. Think of it as a kind
of \qt{Mini-Haskell} with four \qn{statements}: @{text data}
(for datatypes), @{text fun} (stemming from code equations),
also @{text class} and @{text inst} (for type classes).
\item Finally, the abstract program is \qn{serialised} into concrete
source code of a target language.
+ This step only produces concrete syntax but does not change the
+ program in essence; all conceptual transformations occur in the
+ translation step.
\end{itemize}
--- a/doc-src/Codegen/Thy/document/Adaption.tex Wed Apr 01 16:03:00 2009 +0200
+++ b/doc-src/Codegen/Thy/document/Adaption.tex Wed Apr 01 16:03:18 2009 +0200
@@ -96,42 +96,7 @@
supposed to be:
\begin{figure}[here]
- \begin{tikzpicture}[scale = 0.5]
- \tikzstyle water=[color = blue, thick]
- \tikzstyle ice=[color = black, very thick, cap = round, join = round, fill = white]
- \tikzstyle process=[color = green, semithick, ->]
- \tikzstyle adaption=[color = red, semithick, ->]
- \tikzstyle target=[color = black]
- \foreach \x in {0, ..., 24}
- \draw[style=water] (\x, 0.25) sin + (0.25, 0.25) cos + (0.25, -0.25) sin
- + (0.25, -0.25) cos + (0.25, 0.25);
- \draw[style=ice] (1, 0) --
- (3, 6) node[above, fill=white] {logic} -- (5, 0) -- cycle;
- \draw[style=ice] (9, 0) --
- (11, 6) node[above, fill=white] {intermediate language} -- (13, 0) -- cycle;
- \draw[style=ice] (15, -6) --
- (19, 6) node[above, fill=white] {target language} -- (23, -6) -- cycle;
- \draw[style=process]
- (3.5, 3) .. controls (7, 5) .. node[fill=white] {translation} (10.5, 3);
- \draw[style=process]
- (11.5, 3) .. controls (15, 5) .. node[fill=white] (serialisation) {serialisation} (18.5, 3);
- \node (adaption) at (11, -2) [style=adaption] {adaption};
- \node at (19, 3) [rotate=90] {generated};
- \node at (19.5, -5) {language};
- \node at (19.5, -3) {library};
- \node (includes) at (19.5, -1) {includes};
- \node (reserved) at (16.5, -3) [rotate=72] {reserved}; % proper 71.57
- \draw[style=process]
- (includes) -- (serialisation);
- \draw[style=process]
- (reserved) -- (serialisation);
- \draw[style=adaption]
- (adaption) -- (serialisation);
- \draw[style=adaption]
- (adaption) -- (includes);
- \draw[style=adaption]
- (adaption) -- (reserved);
- \end{tikzpicture}
+ \includegraphics{Thy/pictures/adaption}
\caption{The adaption principle}
\label{fig:adaption}
\end{figure}
--- a/doc-src/Codegen/Thy/document/Introduction.tex Wed Apr 01 16:03:00 2009 +0200
+++ b/doc-src/Codegen/Thy/document/Introduction.tex Wed Apr 01 16:03:18 2009 +0200
@@ -284,29 +284,7 @@
how it works.
\begin{figure}[h]
- \begin{tikzpicture}[x = 4.2cm, y = 1cm]
- \tikzstyle entity=[rounded corners, draw, thick, color = black, fill = white];
- \tikzstyle process=[ellipse, draw, thick, color = green, fill = white];
- \tikzstyle process_arrow=[->, semithick, color = green];
- \node (HOL) at (0, 4) [style=entity] {\isa{Isabelle{\isacharslash}HOL} theory};
- \node (eqn) at (2, 2) [style=entity] {code equations};
- \node (iml) at (2, 0) [style=entity] {intermediate language};
- \node (seri) at (1, 0) [style=process] {serialisation};
- \node (SML) at (0, 3) [style=entity] {\isa{SML}};
- \node (OCaml) at (0, 2) [style=entity] {\isa{OCaml}};
- \node (further) at (0, 1) [style=entity] {\isa{{\isasymdots}}};
- \node (Haskell) at (0, 0) [style=entity] {\isa{Haskell}};
- \draw [style=process_arrow] (HOL) .. controls (2, 4) ..
- node [style=process, near start] {selection}
- node [style=process, near end] {preprocessing}
- (eqn);
- \draw [style=process_arrow] (eqn) -- node (transl) [style=process] {translation} (iml);
- \draw [style=process_arrow] (iml) -- (seri);
- \draw [style=process_arrow] (seri) -- (SML);
- \draw [style=process_arrow] (seri) -- (OCaml);
- \draw [style=process_arrow, dashed] (seri) -- (further);
- \draw [style=process_arrow] (seri) -- (Haskell);
- \end{tikzpicture}
+ \includegraphics{Thy/pictures/architecture}
\caption{Code generator architecture}
\label{fig:arch}
\end{figure}
@@ -327,35 +305,29 @@
\begin{itemize}
- \item Out of the vast collection of theorems proven in a
- \qn{theory}, a reasonable subset modelling
- code equations is \qn{selected}.
-
- \item On those selected theorems, certain
- transformations are carried out
- (\qn{preprocessing}). Their purpose is to turn theorems
- representing non- or badly executable
- specifications into equivalent but executable counterparts.
- The result is a structured collection of \qn{code theorems}.
+ \item Starting point is a collection of raw code equations in a
+ theory; due to proof irrelevance it is not relevant where they
+ stem from but typically they are either descendant of specification
+ tools or explicit proofs by the user.
+
+ \item Before these raw code equations are continued
+ with, they can be subjected to theorem transformations. This
+ \qn{preprocessor} is an interface which allows to apply the full
+ expressiveness of ML-based theorem transformations to code
+ generation. The result of the preprocessing step is a
+ structured collection of code equations.
- \item Before the selected code equations are continued with,
- they can be \qn{preprocessed}, i.e. subjected to theorem
- transformations. This \qn{preprocessor} is an interface which
- allows to apply
- the full expressiveness of ML-based theorem transformations
- to code generation; motivating examples are shown below, see
- \secref{sec:preproc}.
- The result of the preprocessing step is a structured collection
- of code equations.
-
- \item These code equations are \qn{translated} to a program
- in an abstract intermediate language. Think of it as a kind
+ \item These code equations are \qn{translated} to a program in an
+ abstract intermediate language. Think of it as a kind
of \qt{Mini-Haskell} with four \qn{statements}: \isa{data}
(for datatypes), \isa{fun} (stemming from code equations),
also \isa{class} and \isa{inst} (for type classes).
\item Finally, the abstract program is \qn{serialised} into concrete
source code of a target language.
+ This step only produces concrete syntax but does not change the
+ program in essence; all conceptual transformations occur in the
+ translation step.
\end{itemize}
--- a/doc-src/Codegen/Thy/pictures/adaption.tex Wed Apr 01 16:03:00 2009 +0200
+++ b/doc-src/Codegen/Thy/pictures/adaption.tex Wed Apr 01 16:03:18 2009 +0200
@@ -1,7 +1,5 @@
\documentclass[12pt]{article}
-\usepackage{pgf}
-\usepackage{pgflibraryshapes}
\usepackage{tikz}
\begin{document}
@@ -10,7 +8,7 @@
\setlength{\fboxrule}{0.01pt}
\setlength{\fboxsep}{4pt}
-\fbox{
+\fcolorbox{white}{white}{
\begin{tikzpicture}[scale = 0.5]
\tikzstyle water=[color = blue, thick]
--- a/doc-src/Codegen/Thy/pictures/architecture.tex Wed Apr 01 16:03:00 2009 +0200
+++ b/doc-src/Codegen/Thy/pictures/architecture.tex Wed Apr 01 16:03:18 2009 +0200
@@ -1,8 +1,8 @@
\documentclass[12pt]{article}
-\usepackage{pgf}
-\usepackage{pgflibraryshapes}
\usepackage{tikz}
+\usetikzlibrary{shapes}
+\usetikzlibrary{arrows}
\begin{document}
@@ -10,30 +10,39 @@
\setlength{\fboxrule}{0.01pt}
\setlength{\fboxsep}{4pt}
-\fbox{
+\fcolorbox{white}{white}{
+
+\newcommand{\sys}[1]{\emph{#1}}
-\begin{tikzpicture}[x = 4.2cm, y = 1cm]
- \tikzstyle entity=[rounded corners, draw, thick, color = black, fill = white];
- \tikzstyle process=[ellipse, draw, thick, color = green, fill = white];
- \tikzstyle process_arrow=[->, semithick, color = green];
- \node (HOL) at (0, 4) [style=entity] {Isabelle/HOL theory};
- \node (eqn) at (2, 2) [style=entity] {code equations};
- \node (iml) at (2, 0) [style=entity] {intermediate language};
- \node (seri) at (1, 0) [style=process] {serialisation};
- \node (SML) at (0, 3) [style=entity] {SML};
- \node (OCaml) at (0, 2) [style=entity] {OCaml};
- \node (further) at (0, 1) [style=entity] {\ldots};
- \node (Haskell) at (0, 0) [style=entity] {Haskell};
- \draw [style=process_arrow] (HOL) .. controls (2, 4) ..
- node [style=process, near start] {selection}
- node [style=process, near end] {preprocessing}
- (eqn);
- \draw [style=process_arrow] (eqn) -- node (transl) [style=process] {translation} (iml);
- \draw [style=process_arrow] (iml) -- (seri);
- \draw [style=process_arrow] (seri) -- (SML);
- \draw [style=process_arrow] (seri) -- (OCaml);
- \draw [style=process_arrow, dashed] (seri) -- (further);
- \draw [style=process_arrow] (seri) -- (Haskell);
+\begin{tikzpicture}[x = 4cm, y = 1cm]
+ \tikzstyle positive=[color = black, fill = white];
+ \tikzstyle negative=[color = white, fill = black];
+ \tikzstyle entity=[rounded corners, draw, thick];
+ \tikzstyle process=[ellipse, draw, thick];
+ \tikzstyle arrow=[-stealth, semithick];
+ \node (spec) at (0, 3) [entity, positive] {specification tools};
+ \node (user) at (1, 3) [entity, positive] {user proofs};
+ \node (spec_user_join) at (0.5, 3) [shape=coordinate] {};
+ \node (raw) at (0.5, 4) [entity, positive] {raw code equations};
+ \node (pre) at (1.5, 4) [process, positive] {preprocessing};
+ \node (eqn) at (2.5, 4) [entity, positive] {code equations};
+ \node (iml) at (0.5, 0) [entity, positive] {intermediate program};
+ \node (seri) at (1.5, 0) [process, positive] {serialisation};
+ \node (SML) at (2.5, 3) [entity, positive] {\sys{SML}};
+ \node (OCaml) at (2.5, 2) [entity, positive] {\sys{OCaml}};
+ \node (further) at (2.5, 1) [entity, positive] {(\ldots)};
+ \node (Haskell) at (2.5, 0) [entity, positive] {\sys{Haskell}};
+ \draw [semithick] (spec) -- (spec_user_join);
+ \draw [semithick] (user) -- (spec_user_join);
+ \draw [-diamond, semithick] (spec_user_join) -- (raw);
+ \draw [arrow] (raw) -- (pre);
+ \draw [arrow] (pre) -- (eqn);
+ \draw [arrow] (eqn) -- node (transl) [process, positive] {translation} (iml);
+ \draw [arrow] (iml) -- (seri);
+ \draw [arrow] (seri) -- (SML);
+ \draw [arrow] (seri) -- (OCaml);
+ \draw [arrow, dashed] (seri) -- (further);
+ \draw [arrow] (seri) -- (Haskell);
\end{tikzpicture}
}
--- a/doc-src/Codegen/codegen.tex Wed Apr 01 16:03:00 2009 +0200
+++ b/doc-src/Codegen/codegen.tex Wed Apr 01 16:03:18 2009 +0200
@@ -5,9 +5,6 @@
\usepackage{../iman,../extra,../isar,../proof}
\usepackage{../isabelle,../isabellesym}
\usepackage{style}
-\usepackage{pgf}
-\usepackage{pgflibraryshapes}
-\usepackage{tikz}
\usepackage{../pdfsetup}
\hyphenation{Isabelle}
--- a/src/HOL/Tools/atp_manager.ML Wed Apr 01 16:03:00 2009 +0200
+++ b/src/HOL/Tools/atp_manager.ML Wed Apr 01 16:03:18 2009 +0200
@@ -85,36 +85,25 @@
(* state of thread manager *)
datatype T = State of
- {timeout_heap: ThreadHeap.T,
+ {managing_thread: Thread.thread option,
+ timeout_heap: ThreadHeap.T,
oldest_heap: ThreadHeap.T,
active: (Thread.thread * (Time.time * Time.time * string)) list,
cancelling: (Thread.thread * (Time.time * Time.time * string)) list,
messages: string list,
store: string list};
-fun make_state timeout_heap oldest_heap active cancelling messages store =
- State {timeout_heap = timeout_heap, oldest_heap = oldest_heap,
+fun make_state managing_thread timeout_heap oldest_heap active cancelling messages store =
+ State {managing_thread = managing_thread, timeout_heap = timeout_heap, oldest_heap = oldest_heap,
active = active, cancelling = cancelling, messages = messages, store = store};
-fun empty_state state =
- let
- val State {active = active, cancelling = cancelling, messages = messages, ...} =
- Synchronized.value state
- in (null active) andalso (null cancelling) andalso (null messages) end;
-
-val state = Synchronized.var "atp_manager" (make_state ThreadHeap.empty ThreadHeap.empty [] [] [] []);
-
-
-(* the managing thread *)
-
-(*watches over running threads and interrupts them if required*)
-val managing_thread = ref (NONE: Thread.thread option);
-
+val state = Synchronized.var "atp_manager"
+ (make_state NONE ThreadHeap.empty ThreadHeap.empty [] [] [] []);
(* unregister thread *)
fun unregister (success, message) thread = Synchronized.change state
- (fn state as State {timeout_heap, oldest_heap, active, cancelling, messages, store} =>
+ (fn state as State {managing_thread, timeout_heap, oldest_heap, active, cancelling, messages, store} =>
(case lookup_thread active thread of
SOME (birthtime, _, description) =>
let
@@ -132,7 +121,9 @@
val store' = message' ::
(if length store <= message_store_limit then store
else #1 (chop message_store_limit store))
- in make_state timeout_heap oldest_heap active' cancelling' (message' :: messages) store' end
+ in make_state
+ managing_thread timeout_heap oldest_heap active' cancelling' (message' :: messages) store'
+ end
| NONE => state));
@@ -147,12 +138,13 @@
fun kill_oldest () =
let exception Unchanged in
Synchronized.change_result state
- (fn State {timeout_heap, oldest_heap, active, cancelling, messages, store} =>
+ (fn State {managing_thread, timeout_heap, oldest_heap, active, cancelling, messages, store} =>
if ThreadHeap.is_empty oldest_heap orelse not (excessive_atps active)
then raise Unchanged
else
let val ((_, oldest_thread), oldest_heap') = ThreadHeap.min_elem oldest_heap
- in (oldest_thread, make_state timeout_heap oldest_heap' active cancelling messages store) end)
+ in (oldest_thread,
+ make_state managing_thread timeout_heap oldest_heap' active cancelling messages store) end)
|> unregister (false, "Interrupted (maximum number of ATPs exceeded)")
handle Unchanged => ()
end;
@@ -167,8 +159,8 @@
fun print_new_messages () =
let val to_print = Synchronized.change_result state
- (fn State {timeout_heap, oldest_heap, active, cancelling, messages, store} =>
- (messages, make_state timeout_heap oldest_heap active cancelling [] store))
+ (fn State {managing_thread, timeout_heap, oldest_heap, active, cancelling, messages, store} =>
+ (messages, make_state managing_thread timeout_heap oldest_heap active cancelling [] store))
in
if null to_print then ()
else priority ("Sledgehammer: " ^ space_implode "\n\n" to_print)
@@ -177,55 +169,66 @@
(* start a watching thread -- only one may exist *)
-fun check_thread_manager () = CRITICAL (fn () =>
- if (case ! managing_thread of SOME thread => Thread.isActive thread | NONE => false)
- then () else managing_thread := SOME (SimpleThread.fork false (fn () =>
- let
- val min_wait_time = Time.fromMilliseconds 300
- val max_wait_time = Time.fromSeconds 10
+fun check_thread_manager () = Synchronized.change state
+ (fn State {managing_thread, timeout_heap, oldest_heap, active, cancelling, messages, store} =>
+ if (case managing_thread of SOME thread => Thread.isActive thread | NONE => false)
+ then make_state managing_thread timeout_heap oldest_heap active cancelling messages store
+ else let val managing_thread = SOME (SimpleThread.fork false (fn () =>
+ let
+ val min_wait_time = Time.fromMilliseconds 300
+ val max_wait_time = Time.fromSeconds 10
- (* wait for next thread to cancel, or maximum*)
- fun time_limit (State {timeout_heap, ...}) =
- (case try ThreadHeap.min timeout_heap of
- NONE => SOME (Time.+ (Time.now (), max_wait_time))
- | SOME (time, _) => SOME time)
+ (* wait for next thread to cancel, or maximum*)
+ fun time_limit (State {timeout_heap, ...}) =
+ (case try ThreadHeap.min timeout_heap of
+ NONE => SOME (Time.+ (Time.now (), max_wait_time))
+ | SOME (time, _) => SOME time)
- (* action: find threads whose timeout is reached, and interrupt cancelling threads *)
- fun action (State {timeout_heap, oldest_heap, active, cancelling, messages, store}) =
- let val (timeout_threads, timeout_heap') =
- ThreadHeap.upto (Time.now (), Thread.self ()) timeout_heap
- in
- if null timeout_threads andalso null cancelling andalso not (excessive_atps active)
- then NONE
- else
- let
- val _ = List.app (SimpleThread.interrupt o #1) cancelling
- val cancelling' = filter (Thread.isActive o #1) cancelling
- val state' = make_state timeout_heap' oldest_heap active cancelling' messages store
- in SOME (map #2 timeout_threads, state') end
- end
- in
- while not (empty_state state) do
- (Synchronized.timed_access state time_limit action
- |> these
- |> List.app (unregister (false, "Interrupted (reached timeout)"));
- kill_excessive ();
- print_new_messages ();
- (*give threads time to respond to interrupt*)
- OS.Process.sleep min_wait_time)
- end)));
+ (* action: find threads whose timeout is reached, and interrupt cancelling threads *)
+ fun action (State {managing_thread, timeout_heap, oldest_heap, active, cancelling,
+ messages, store}) =
+ let val (timeout_threads, timeout_heap') =
+ ThreadHeap.upto (Time.now (), Thread.self ()) timeout_heap
+ in
+ if null timeout_threads andalso null cancelling andalso not (excessive_atps active)
+ then NONE
+ else
+ let
+ val _ = List.app (SimpleThread.interrupt o #1) cancelling
+ val cancelling' = filter (Thread.isActive o #1) cancelling
+ val state' = make_state
+ managing_thread timeout_heap' oldest_heap active cancelling' messages store
+ in SOME (map #2 timeout_threads, state') end
+ end
+ in
+ while Synchronized.change_result state
+ (fn st as
+ State {managing_thread, timeout_heap, oldest_heap, active, cancelling, messages, store} =>
+ if (null active) andalso (null cancelling) andalso (null messages)
+ then (false, make_state NONE timeout_heap oldest_heap active cancelling messages store)
+ else (true, st))
+ do
+ (Synchronized.timed_access state time_limit action
+ |> these
+ |> List.app (unregister (false, "Interrupted (reached timeout)"));
+ kill_excessive ();
+ print_new_messages ();
+ (*give threads time to respond to interrupt*)
+ OS.Process.sleep min_wait_time)
+ end))
+ in make_state managing_thread timeout_heap oldest_heap active cancelling messages store end);
(* thread is registered here by sledgehammer *)
fun register birthtime deadtime (thread, desc) =
(Synchronized.change state
- (fn State {timeout_heap, oldest_heap, active, cancelling, messages, store} =>
+ (fn State {managing_thread, timeout_heap, oldest_heap, active, cancelling, messages, store} =>
let
val timeout_heap' = ThreadHeap.insert (deadtime, thread) timeout_heap
val oldest_heap' = ThreadHeap.insert (birthtime, thread) oldest_heap
val active' = update_thread (thread, (birthtime, deadtime, desc)) active
- in make_state timeout_heap' oldest_heap' active' cancelling messages store end);
+ in make_state managing_thread timeout_heap' oldest_heap' active' cancelling messages store end);
check_thread_manager ());
@@ -235,9 +238,11 @@
(* kill: move all threads to cancelling *)
fun kill () = Synchronized.change state
- (fn State {timeout_heap, oldest_heap, active, cancelling, messages, store} =>
+ (fn State {managing_thread, timeout_heap, oldest_heap, active, cancelling, messages, store} =>
let val formerly_active = map (fn (th, (tb, _, desc)) => (th, (tb, Time.now (), desc))) active
- in make_state timeout_heap oldest_heap [] (formerly_active @ cancelling) messages store end);
+ in make_state
+ managing_thread timeout_heap oldest_heap [] (formerly_active @ cancelling) messages store
+ end);
(* ATP info *)
--- a/src/HOL/Tools/function_package/fundef_common.ML Wed Apr 01 16:03:00 2009 +0200
+++ b/src/HOL/Tools/function_package/fundef_common.ML Wed Apr 01 16:03:18 2009 +0200
@@ -246,6 +246,8 @@
("Head symbol of left hand side must be "
^ plural "" "one out of " fnames ^ commas_quote fnames)
+ val _ = length args > 0 orelse input_error "Function has no arguments:"
+
fun add_bvs t is = add_loose_bnos (t, 0, is)
val rvs = (add_bvs rhs [] \\ fold add_bvs args [])
|> map (fst o nth (rev qs))
--- a/src/Pure/README Wed Apr 01 16:03:00 2009 +0200
+++ b/src/Pure/README Wed Apr 01 16:03:18 2009 +0200
@@ -15,7 +15,6 @@
Now the Pure session may be compiled interactively as follows:
- isabelle-process -u RAW
+ isabelle tty -l RAW
+ use "ROOT.ML";
-See ROOT.ML for further information.
-
--- a/src/Pure/ROOT.ML Wed Apr 01 16:03:00 2009 +0200
+++ b/src/Pure/ROOT.ML Wed Apr 01 16:03:18 2009 +0200
@@ -1,7 +1,4 @@
-(* Title: Pure/ROOT.ML
-
-Pure Isabelle.
-*)
+(* Pure Isabelle *)
structure Distribution = (*filled-in by makedist*)
struct