--- a/NEWS Sat Oct 30 15:13:11 2010 -0700
+++ b/NEWS Wed Nov 03 07:02:09 2010 -0700
@@ -60,6 +60,8 @@
floating-point notation that coincides with the inner syntax for
float_token.
+* Support for real valued preferences (with approximative PGIP type).
+
* Interpretation command 'interpret' accepts a list of equations like
'interpretation' does.
@@ -157,6 +159,9 @@
* Abolished symbol type names: "prod" and "sum" replace "*" and "+"
respectively. INCOMPATIBILITY.
+* Name "Plus" of disjoint sum operator "<+>" is now hidden.
+ Write Sum_Type.Plus.
+
* Constant "split" has been merged with constant "prod_case"; names
of ML functions, facts etc. involving split have been retained so far,
though. INCOMPATIBILITY.
--- a/doc-src/IsarImplementation/Thy/ML.thy Sat Oct 30 15:13:11 2010 -0700
+++ b/doc-src/IsarImplementation/Thy/ML.thy Wed Nov 03 07:02:09 2010 -0700
@@ -262,6 +262,22 @@
@{ML_text lhs} (not @{ML_text lhs_tm}). Or a term that is known
to be a variable can be called @{ML_text v} or @{ML_text x}.
+ \item Tactics (\secref{sec:tactics}) are sufficiently important to
+ have specific naming conventions. The name of a basic tactic
+ definition always has a @{ML_text "_tac"} suffix, the subgoal index
+ (if applicable) is always called @{ML_text i}, and the goal state
+ (if made explicit) is usually called @{ML_text st} instead of the
+ somewhat misleading @{ML_text thm}. Any other arguments are given
+ before the latter two, and the general context is given first.
+ Example:
+
+ \begin{verbatim}
+ fun my_tac ctxt arg1 arg2 i st = ...
+ \end{verbatim}
+
+ Note that the goal state @{ML_text st} above is rarely made
+ explicit, if tactic combinators (tacticals) are used as usual.
+
\end{itemize}
*}
@@ -1274,6 +1290,30 @@
*}
+subsection {* Time *}
+
+text %mlref {*
+ \begin{mldecls}
+ @{index_ML_type Time.time} \\
+ @{index_ML seconds: "real -> Time.time"} \\
+ \end{mldecls}
+
+ \begin{description}
+
+ \item Type @{ML_type Time.time} represents time abstractly according
+ to the SML97 basis library definition. This is adequate for
+ internal ML operations, but awkward in concrete time specifications.
+
+ \item @{ML seconds}~@{text "s"} turns the concrete scalar @{text
+ "s"} (measured in seconds) into an abstract time value. Floating
+ point numbers are easy to use as context parameters (e.g.\ via
+ configuration options, see \secref{sec:config-options}) or
+ preferences that are maintained by external tools as well.
+
+ \end{description}
+*}
+
+
subsection {* Options *}
text %mlref {*
--- a/doc-src/IsarImplementation/Thy/Prelim.thy Sat Oct 30 15:13:11 2010 -0700
+++ b/doc-src/IsarImplementation/Thy/Prelim.thy Wed Nov 03 07:02:09 2010 -0700
@@ -663,6 +663,7 @@
*}
setup airspeed_velocity_setup
+declare [[airspeed_velocity = 10]]
declare [[airspeed_velocity = 9.9]]
--- a/doc-src/IsarImplementation/Thy/document/ML.tex Sat Oct 30 15:13:11 2010 -0700
+++ b/doc-src/IsarImplementation/Thy/document/ML.tex Wed Nov 03 07:02:09 2010 -0700
@@ -281,6 +281,22 @@
\verb|lhs| (not \verb|lhs_tm|). Or a term that is known
to be a variable can be called \verb|v| or \verb|x|.
+ \item Tactics (\secref{sec:tactics}) are sufficiently important to
+ have specific naming conventions. The name of a basic tactic
+ definition always has a \verb|_tac| suffix, the subgoal index
+ (if applicable) is always called \verb|i|, and the goal state
+ (if made explicit) is usually called \verb|st| instead of the
+ somewhat misleading \verb|thm|. Any other arguments are given
+ before the latter two, and the general context is given first.
+ Example:
+
+ \begin{verbatim}
+ fun my_tac ctxt arg1 arg2 i st = ...
+ \end{verbatim}
+
+ Note that the goal state \verb|st| above is rarely made
+ explicit, if tactic combinators (tacticals) are used as usual.
+
\end{itemize}%
\end{isamarkuptext}%
\isamarkuptrue%
@@ -1643,6 +1659,44 @@
%
\endisadelimmlref
%
+\isamarkupsubsection{Time%
+}
+\isamarkuptrue%
+%
+\isadelimmlref
+%
+\endisadelimmlref
+%
+\isatagmlref
+%
+\begin{isamarkuptext}%
+\begin{mldecls}
+ \indexdef{}{ML type}{Time.time}\verb|type Time.time| \\
+ \indexdef{}{ML}{seconds}\verb|seconds: real -> Time.time| \\
+ \end{mldecls}
+
+ \begin{description}
+
+ \item Type \verb|Time.time| represents time abstractly according
+ to the SML97 basis library definition. This is adequate for
+ internal ML operations, but awkward in concrete time specifications.
+
+ \item \verb|seconds|~\isa{s} turns the concrete scalar \isa{s} (measured in seconds) into an abstract time value. Floating
+ point numbers are easy to use as context parameters (e.g.\ via
+ configuration options, see \secref{sec:config-options}) or
+ preferences that are maintained by external tools as well.
+
+ \end{description}%
+\end{isamarkuptext}%
+\isamarkuptrue%
+%
+\endisatagmlref
+{\isafoldmlref}%
+%
+\isadelimmlref
+%
+\endisadelimmlref
+%
\isamarkupsubsection{Options%
}
\isamarkuptrue%
--- a/doc-src/IsarImplementation/Thy/document/Prelim.tex Sat Oct 30 15:13:11 2010 -0700
+++ b/doc-src/IsarImplementation/Thy/document/Prelim.tex Wed Nov 03 07:02:09 2010 -0700
@@ -1047,6 +1047,8 @@
\isanewline
\isanewline
\isacommand{declare}\isamarkupfalse%
+\ {\isacharbrackleft}{\isacharbrackleft}airspeed{\isacharunderscore}velocity\ {\isacharequal}\ {\isadigit{1}}{\isadigit{0}}{\isacharbrackright}{\isacharbrackright}\isanewline
+\isacommand{declare}\isamarkupfalse%
\ {\isacharbrackleft}{\isacharbrackleft}airspeed{\isacharunderscore}velocity\ {\isacharequal}\ {\isadigit{9}}{\isachardot}{\isadigit{9}}{\isacharbrackright}{\isacharbrackright}%
\isamarkupsection{Names \label{sec:names}%
}
--- a/doc-src/IsarRef/Thy/Outer_Syntax.thy Sat Oct 30 15:13:11 2010 -0700
+++ b/doc-src/IsarRef/Thy/Outer_Syntax.thy Wed Nov 03 07:02:09 2010 -0700
@@ -197,7 +197,6 @@
\railqtok{nameref}.
\indexoutertoken{name}\indexoutertoken{parname}\indexoutertoken{nameref}
- \indexoutertoken{int}
\begin{rail}
name: ident | symident | string | nat
;
@@ -205,9 +204,26 @@
;
nameref: name | longident
;
+ \end{rail}
+*}
+
+
+subsection {* Numbers *}
+
+text {* The outer lexical syntax (\secref{sec:outer-lex}) admits
+ natural numbers and floating point numbers. These are combined as
+ @{syntax int} and @{syntax real} as follows.
+
+ \indexoutertoken{int}\indexoutertoken{real}
+ \begin{rail}
int: nat | '-' nat
;
+ real: float | int
+ ;
\end{rail}
+
+ Note that there is an overlap with the category \railqtok{name},
+ which also includes @{syntax nat}.
*}
--- a/doc-src/IsarRef/Thy/document/Outer_Syntax.tex Sat Oct 30 15:13:11 2010 -0700
+++ b/doc-src/IsarRef/Thy/document/Outer_Syntax.tex Wed Nov 03 07:02:09 2010 -0700
@@ -216,7 +216,6 @@
\railqtok{nameref}.
\indexoutertoken{name}\indexoutertoken{parname}\indexoutertoken{nameref}
- \indexoutertoken{int}
\begin{rail}
name: ident | symident | string | nat
;
@@ -224,9 +223,29 @@
;
nameref: name | longident
;
+ \end{rail}%
+\end{isamarkuptext}%
+\isamarkuptrue%
+%
+\isamarkupsubsection{Numbers%
+}
+\isamarkuptrue%
+%
+\begin{isamarkuptext}%
+The outer lexical syntax (\secref{sec:outer-lex}) admits
+ natural numbers and floating point numbers. These are combined as
+ \hyperlink{syntax.int}{\mbox{\isa{int}}} and \hyperlink{syntax.real}{\mbox{\isa{real}}} as follows.
+
+ \indexoutertoken{int}\indexoutertoken{real}
+ \begin{rail}
int: nat | '-' nat
;
- \end{rail}%
+ real: float | int
+ ;
+ \end{rail}
+
+ Note that there is an overlap with the category \railqtok{name},
+ which also includes \hyperlink{syntax.nat}{\mbox{\isa{nat}}}.%
\end{isamarkuptext}%
\isamarkuptrue%
%
--- a/src/HOL/Algebra/Congruence.thy Sat Oct 30 15:13:11 2010 -0700
+++ b/src/HOL/Algebra/Congruence.thy Wed Nov 03 07:02:09 2010 -0700
@@ -56,7 +56,8 @@
fixes S (structure)
assumes refl [simp, intro]: "x \<in> carrier S \<Longrightarrow> x .= x"
and sym [sym]: "\<lbrakk> x .= y; x \<in> carrier S; y \<in> carrier S \<rbrakk> \<Longrightarrow> y .= x"
- and trans [trans]: "\<lbrakk> x .= y; y .= z; x \<in> carrier S; y \<in> carrier S; z \<in> carrier S \<rbrakk> \<Longrightarrow> x .= z"
+ and trans [trans]:
+ "\<lbrakk> x .= y; y .= z; x \<in> carrier S; y \<in> carrier S; z \<in> carrier S \<rbrakk> \<Longrightarrow> x .= z"
(* Lemmas by Stephan Hohe *)
--- a/src/HOL/Algebra/Lattice.thy Sat Oct 30 15:13:11 2010 -0700
+++ b/src/HOL/Algebra/Lattice.thy Wed Nov 03 07:02:09 2010 -0700
@@ -24,7 +24,8 @@
and le_trans [trans]:
"[| x \<sqsubseteq> y; y \<sqsubseteq> z; x \<in> carrier L; y \<in> carrier L; z \<in> carrier L |] ==> x \<sqsubseteq> z"
and le_cong:
- "\<lbrakk> x .= y; z .= w; x \<in> carrier L; y \<in> carrier L; z \<in> carrier L; w \<in> carrier L \<rbrakk> \<Longrightarrow> x \<sqsubseteq> z \<longleftrightarrow> y \<sqsubseteq> w"
+ "\<lbrakk> x .= y; z .= w; x \<in> carrier L; y \<in> carrier L; z \<in> carrier L; w \<in> carrier L \<rbrakk> \<Longrightarrow>
+ x \<sqsubseteq> z \<longleftrightarrow> y \<sqsubseteq> w"
definition
lless :: "[_, 'a, 'a] => bool" (infixl "\<sqsubset>\<index>" 50)
--- a/src/HOL/Finite_Set.thy Sat Oct 30 15:13:11 2010 -0700
+++ b/src/HOL/Finite_Set.thy Wed Nov 03 07:02:09 2010 -0700
@@ -2182,7 +2182,7 @@
subsubsection {* Pigeonhole Principles *}
-lemma pigeonhole: "finite(A) \<Longrightarrow> card A > card(f ` A) \<Longrightarrow> ~ inj_on f A "
+lemma pigeonhole: "card A > card(f ` A) \<Longrightarrow> ~ inj_on f A "
by (auto dest: card_image less_irrefl_nat)
lemma pigeonhole_infinite:
--- a/src/HOL/Library/Multiset.thy Sat Oct 30 15:13:11 2010 -0700
+++ b/src/HOL/Library/Multiset.thy Wed Nov 03 07:02:09 2010 -0700
@@ -735,6 +735,10 @@
"multiset_of (xs @ ys) = multiset_of xs + multiset_of ys"
by (induct xs arbitrary: ys) (auto simp: add_ac)
+lemma multiset_of_filter:
+ "multiset_of (filter P xs) = {#x :# multiset_of xs. P x #}"
+ by (induct xs) simp_all
+
lemma surj_multiset_of: "surj multiset_of"
apply (unfold surj_def)
apply (rule allI)
@@ -852,7 +856,7 @@
lemma properties_for_sort_key:
assumes "multiset_of ys = multiset_of xs"
- and "\<forall>k \<in> f ` set ys. filter (\<lambda>x. k = f x) ys = filter (\<lambda>x. k = f x) xs"
+ and "\<And>k. k \<in> set ys \<Longrightarrow> filter (\<lambda>x. f k = f x) ys = filter (\<lambda>x. f k = f x) xs"
and "sorted (map f ys)"
shows "sort_key f xs = ys"
using assms proof (induct xs arbitrary: ys)
@@ -860,7 +864,7 @@
next
case (Cons x xs)
from Cons.prems(2) have
- "\<forall>k \<in> f ` set ys. filter (\<lambda>x. k = f x) (remove1 x ys) = filter (\<lambda>x. k = f x) xs"
+ "\<forall>k \<in> set ys. filter (\<lambda>x. f k = f x) (remove1 x ys) = filter (\<lambda>x. f k = f x) xs"
by (simp add: filter_remove1)
with Cons.prems have "sort_key f xs = remove1 x ys"
by (auto intro!: Cons.hyps simp add: sorted_map_remove1)
@@ -880,10 +884,56 @@
by (rule multiset_of_eq_length_filter)
then have "\<And>k. replicate (length (filter (\<lambda>y. k = y) ys)) k = replicate (length (filter (\<lambda>x. k = x) xs)) k"
by simp
- then show "\<forall>k \<in> (\<lambda>x. x) ` set ys. filter (\<lambda>y. k = y) ys = filter (\<lambda>x. k = x) xs"
+ then show "\<And>k. k \<in> set ys \<Longrightarrow> filter (\<lambda>y. k = y) ys = filter (\<lambda>x. k = x) xs"
by (simp add: replicate_length_filter)
qed
+lemma sort_key_by_quicksort:
+ "sort_key f xs = sort_key f [x\<leftarrow>xs. f x < f (xs ! (length xs div 2))]
+ @ [x\<leftarrow>xs. f x = f (xs ! (length xs div 2))]
+ @ sort_key f [x\<leftarrow>xs. f x > f (xs ! (length xs div 2))]" (is "sort_key f ?lhs = ?rhs")
+proof (rule properties_for_sort_key)
+ show "multiset_of ?rhs = multiset_of ?lhs"
+ by (rule multiset_eqI) (auto simp add: multiset_of_filter)
+next
+ show "sorted (map f ?rhs)"
+ by (auto simp add: sorted_append intro: sorted_map_same)
+next
+ fix l
+ assume "l \<in> set ?rhs"
+ have *: "\<And>x P. P (f x) \<and> f l = f x \<longleftrightarrow> P (f l) \<and> f l = f x" by auto
+ have **: "\<And>x. f l = f x \<longleftrightarrow> f x = f l" by auto
+ have "[x \<leftarrow> sort_key f xs . f x = f l] = [x \<leftarrow> xs. f x = f l]"
+ unfolding filter_sort by (rule properties_for_sort_key) (auto intro: sorted_map_same)
+ with ** have [simp]: "[x \<leftarrow> sort_key f xs . f l = f x] = [x \<leftarrow> xs. f l = f x]" by simp
+ let ?pivot = "f (xs ! (length xs div 2))"
+ show "[x \<leftarrow> ?rhs. f l = f x] = [x \<leftarrow> ?lhs. f l = f x]"
+ proof (cases "f l" ?pivot rule: linorder_cases)
+ case less then moreover have "f l \<noteq> ?pivot" and "\<not> f l > ?pivot" by auto
+ ultimately show ?thesis
+ apply (auto simp add: filter_sort [symmetric])
+ apply (subst *) apply simp
+ apply (subst *) apply simp
+ done
+ next
+ case equal then show ?thesis
+ by (auto simp add: ** less_le)
+ next
+ case greater then moreover have "f l \<noteq> ?pivot" and "\<not> f l < ?pivot" by auto
+ ultimately show ?thesis
+ apply (auto simp add: filter_sort [symmetric])
+ apply (subst *) apply simp
+ apply (subst *) apply simp
+ done
+ qed
+qed
+
+lemma sort_by_quicksort:
+ "sort xs = sort [x\<leftarrow>xs. x < xs ! (length xs div 2)]
+ @ [x\<leftarrow>xs. x = xs ! (length xs div 2)]
+ @ sort [x\<leftarrow>xs. x > xs ! (length xs div 2)]" (is "sort ?lhs = ?rhs")
+ using sort_key_by_quicksort [of "\<lambda>x. x", symmetric] by simp
+
end
lemma multiset_of_remdups_le: "multiset_of (remdups xs) \<le> multiset_of xs"
--- a/src/HOL/List.thy Sat Oct 30 15:13:11 2010 -0700
+++ b/src/HOL/List.thy Wed Nov 03 07:02:09 2010 -0700
@@ -3949,17 +3949,21 @@
"filter P (sort_key f xs) = sort_key f (filter P xs)"
by (induct xs) (simp_all add: filter_insort_triv filter_insort)
-lemma sorted_same [simp]:
- "sorted [x\<leftarrow>xs. x = f xs]"
-proof (induct xs arbitrary: f)
+lemma sorted_map_same:
+ "sorted (map f [x\<leftarrow>xs. f x = g xs])"
+proof (induct xs arbitrary: g)
case Nil then show ?case by simp
next
case (Cons x xs)
- then have "sorted [y\<leftarrow>xs . y = (\<lambda>xs. x) xs]" .
- moreover from Cons have "sorted [y\<leftarrow>xs . y = (f \<circ> Cons x) xs]" .
+ then have "sorted (map f [y\<leftarrow>xs . f y = (\<lambda>xs. f x) xs])" .
+ moreover from Cons have "sorted (map f [y\<leftarrow>xs . f y = (g \<circ> Cons x) xs])" .
ultimately show ?case by (simp_all add: sorted_Cons)
qed
+lemma sorted_same:
+ "sorted [x\<leftarrow>xs. x = g xs]"
+ using sorted_map_same [of "\<lambda>x. x"] by simp
+
lemma remove1_insort [simp]:
"remove1 x (insort x xs) = xs"
by (induct xs) simp_all
--- a/src/HOL/Matrix/Cplex_tools.ML Sat Oct 30 15:13:11 2010 -0700
+++ b/src/HOL/Matrix/Cplex_tools.ML Wed Nov 03 07:02:09 2010 -0700
@@ -977,7 +977,6 @@
end
handle (Tokenize s) => raise (Load_cplexResult ("Tokenize: "^s))
| Option => raise (Load_cplexResult "Option")
- | x => raise x
fun load_cplexResult name =
let
@@ -1127,7 +1126,6 @@
end
handle (Tokenize s) => raise (Load_cplexResult ("Tokenize: "^s))
| Option => raise (Load_cplexResult "Option")
- | x => raise x
exception Execute of string;
@@ -1153,7 +1151,7 @@
result
end
handle (Load_cplexResult s) => raise (Execute ("Load_cplexResult: "^s^"\nExecute: "^answer))
- | _ => raise (Execute answer)
+ | _ => raise (Execute answer) (* FIXME avoid handle _ *)
end
fun solve_cplex prog =
--- a/src/HOL/Matrix/matrixlp.ML Sat Oct 30 15:13:11 2010 -0700
+++ b/src/HOL/Matrix/matrixlp.ML Wed Nov 03 07:02:09 2010 -0700
@@ -82,7 +82,7 @@
let
val simp_th = matrix_compute (cprop_of th)
val th = Thm.strip_shyps (Thm.equal_elim simp_th th)
- fun removeTrue th = removeTrue (Thm.implies_elim th TrueI) handle _ => th (* FIXME avoid handle _ *)
+ fun removeTrue th = removeTrue (Thm.implies_elim th TrueI) handle THM _ => th
in
removeTrue th
end
--- a/src/HOL/Mirabelle/Tools/mirabelle_sledgehammer.ML Sat Oct 30 15:13:11 2010 -0700
+++ b/src/HOL/Mirabelle/Tools/mirabelle_sledgehammer.ML Wed Nov 03 07:02:09 2010 -0700
@@ -497,8 +497,8 @@
|> snd
end
-val try_inner_timeout = Time.fromSeconds 5
-val try_outer_timeout = Time.fromSeconds 30
+val try_inner_timeout = seconds 5.0
+val try_outer_timeout = seconds 30.0
fun sledgehammer_action args id (st as {pre, name, ...}: Mirabelle.run_args) =
let val goal = Thm.major_prem_of (#goal (Proof.goal pre)) in
--- a/src/HOL/Mutabelle/mutabelle_extra.ML Sat Oct 30 15:13:11 2010 -0700
+++ b/src/HOL/Mutabelle/mutabelle_extra.ML Wed Nov 03 07:02:09 2010 -0700
@@ -248,7 +248,7 @@
end
fun is_executable_term thy t =
- can (TimeLimit.timeLimit (Time.fromMilliseconds 2000)
+ can (TimeLimit.timeLimit (seconds 2.0)
(Quickcheck.test_term
(Context.proof_map (Quickcheck.map_test_params (apfst (K (1, 0)))) (ProofContext.init_global thy))
(SOME "SML"))) (preprocess thy [] t)
--- a/src/HOL/Predicate_Compile_Examples/Context_Free_Grammar_Example.thy Sat Oct 30 15:13:11 2010 -0700
+++ b/src/HOL/Predicate_Compile_Examples/Context_Free_Grammar_Example.thy Wed Nov 03 07:02:09 2010 -0700
@@ -125,7 +125,7 @@
limited_predicates = [],
replacing = [],
manual_reorder = [],
- timeout = Time.fromSeconds 10,
+ timeout = seconds 10.0,
prolog_system = Code_Prolog.SWI_PROLOG}) *}
--- a/src/HOL/Tools/Predicate_Compile/code_prolog.ML Sat Oct 30 15:13:11 2010 -0700
+++ b/src/HOL/Tools/Predicate_Compile/code_prolog.ML Wed Nov 03 07:02:09 2010 -0700
@@ -120,7 +120,7 @@
structure System_Config = Generic_Data
(
type T = system_configuration
- val empty = {timeout = Time.fromSeconds 10, prolog_system = SWI_PROLOG}
+ val empty = {timeout = seconds 10.0, prolog_system = SWI_PROLOG}
val extend = I;
fun merge ({timeout = timeout1, prolog_system = prolog_system1},
{timeout = timeout2, prolog_system = prolog_system2}) =
--- a/src/HOL/Tools/Predicate_Compile/predicate_compile_core.ML Sat Oct 30 15:13:11 2010 -0700
+++ b/src/HOL/Tools/Predicate_Compile/predicate_compile_core.ML Wed Nov 03 07:02:09 2010 -0700
@@ -1809,7 +1809,7 @@
let
val [nrandom, size, depth] = arguments
in
- rpair NONE (TimeLimit.timeLimit (Time.fromSeconds 20) (fn () => fst (DSequence.yieldn k
+ rpair NONE (TimeLimit.timeLimit (seconds 20.0) (fn () => fst (DSequence.yieldn k
(Code_Runtime.dynamic_value_strict (Dseq_Random_Result.get, put_dseq_random_result, "Predicate_Compile_Core.put_dseq_random_result")
thy NONE (fn proc => fn g => fn nrandom => fn size => fn s => g nrandom size s |>> DSequence.map proc)
t' [] nrandom size
@@ -1817,14 +1817,14 @@
depth true)) ())
end
| DSeq =>
- rpair NONE (TimeLimit.timeLimit (Time.fromSeconds 20) (fn () => fst (DSequence.yieldn k
+ rpair NONE (TimeLimit.timeLimit (seconds 20.0) (fn () => fst (DSequence.yieldn k
(Code_Runtime.dynamic_value_strict (Dseq_Result.get, put_dseq_result, "Predicate_Compile_Core.put_dseq_result")
thy NONE DSequence.map t' []) (the_single arguments) true)) ())
| Pos_Generator_DSeq =>
let
val depth = (the_single arguments)
in
- rpair NONE (TimeLimit.timeLimit (Time.fromSeconds 20) (fn () => fst (Lazy_Sequence.yieldn k
+ rpair NONE (TimeLimit.timeLimit (seconds 20.0) (fn () => fst (Lazy_Sequence.yieldn k
(Code_Runtime.dynamic_value_strict (New_Dseq_Result.get, put_new_dseq_result, "Predicate_Compile_Core.put_new_dseq_result")
thy NONE (fn proc => fn g => fn depth => g depth |> Lazy_Sequence.mapa proc)
t' [] depth))) ())
@@ -1835,7 +1835,7 @@
val seed = Random_Engine.next_seed ()
in
if stats then
- apsnd (SOME o accumulate) (split_list (TimeLimit.timeLimit (Time.fromSeconds 20)
+ apsnd (SOME o accumulate) (split_list (TimeLimit.timeLimit (seconds 20.0)
(fn () => fst (Lazy_Sequence.yieldn k
(Code_Runtime.dynamic_value_strict
(Lseq_Random_Stats_Result.get, put_lseq_random_stats_result, "Predicate_Compile_Core.put_lseq_random_stats_result")
@@ -1844,7 +1844,7 @@
|> Lazy_Sequence.mapa (apfst proc))
t' [] nrandom size seed depth))) ()))
else rpair NONE
- (TimeLimit.timeLimit (Time.fromSeconds 20) (fn () => fst (Lazy_Sequence.yieldn k
+ (TimeLimit.timeLimit (seconds 20.0) (fn () => fst (Lazy_Sequence.yieldn k
(Code_Runtime.dynamic_value_strict
(Lseq_Random_Result.get, put_lseq_random_result, "Predicate_Compile_Core.put_lseq_random_result")
thy NONE
@@ -1853,7 +1853,7 @@
t' [] nrandom size seed depth))) ())
end
| _ =>
- rpair NONE (TimeLimit.timeLimit (Time.fromSeconds 20) (fn () => fst (Predicate.yieldn k
+ rpair NONE (TimeLimit.timeLimit (seconds 20.0) (fn () => fst (Predicate.yieldn k
(Code_Runtime.dynamic_value_strict (Pred_Result.get, put_pred_result, "Predicate_Compile_Core.put_pred_result")
thy NONE Predicate.map t' []))) ()))
handle TimeLimit.TimeOut => error "Reached timeout during execution of values"
--- a/src/HOL/Tools/async_manager.ML Sat Oct 30 15:13:11 2010 -0700
+++ b/src/HOL/Tools/async_manager.ML Wed Nov 03 07:02:09 2010 -0700
@@ -80,8 +80,8 @@
(* main manager thread -- only one may exist *)
-val min_wait_time = Time.fromMilliseconds 300;
-val max_wait_time = Time.fromSeconds 10;
+val min_wait_time = seconds 0.3;
+val max_wait_time = seconds 10.0;
fun replace_all bef aft =
let
--- a/src/HOL/Tools/try.ML Sat Oct 30 15:13:11 2010 -0700
+++ b/src/HOL/Tools/try.ML Wed Nov 03 07:02:09 2010 -0700
@@ -20,7 +20,7 @@
ProofGeneralPgip.add_preference Preferences.category_tracing
(Preferences.bool_pref auto "auto-try" "Try standard proof methods.")
-val default_timeout = Time.fromSeconds 5
+val default_timeout = seconds 5.0
fun can_apply timeout_opt pre post tac st =
let val {goal, ...} = Proof.goal st in
--- a/src/HOL/ex/Coercion_Examples.thy Sat Oct 30 15:13:11 2010 -0700
+++ b/src/HOL/ex/Coercion_Examples.thy Wed Nov 03 07:02:09 2010 -0700
@@ -11,7 +11,7 @@
setup Subtyping.setup
-(* Coercion/type maps definitions*)
+(* Error messages test *)
consts func :: "(nat \<Rightarrow> int) \<Rightarrow> nat"
consts arg :: "int \<Rightarrow> nat"
@@ -36,6 +36,8 @@
term "[1::int] = func"
*)
+(* Coercion/type maps definitions *)
+
primrec nat_of_bool :: "bool \<Rightarrow> nat"
where
"nat_of_bool False = 0"
@@ -45,17 +47,17 @@
declare [[coercion int]]
-declare [[map_function map]]
+declare [[coercion_map map]]
definition map_fun :: "('a \<Rightarrow> 'b) \<Rightarrow> ('c \<Rightarrow> 'd) \<Rightarrow> ('b \<Rightarrow> 'c) \<Rightarrow> ('a \<Rightarrow> 'd)" where
"map_fun f g h = g o h o f"
-declare [[map_function "\<lambda> f g h . g o h o f"]]
+declare [[coercion_map "\<lambda> f g h . g o h o f"]]
primrec map_pair :: "('a \<Rightarrow> 'c) \<Rightarrow> ('b \<Rightarrow> 'd) \<Rightarrow> ('a * 'b) \<Rightarrow> ('c * 'd)" where
"map_pair f g (x,y) = (f x, g y)"
-declare [[map_function map_pair]]
+declare [[coercion_map map_pair]]
(* Examples taken from the haskell draft implementation *)
--- a/src/Pure/Concurrent/future.ML Sat Oct 30 15:13:11 2010 -0700
+++ b/src/Pure/Concurrent/future.ML Wed Nov 03 07:02:09 2010 -0700
@@ -253,7 +253,7 @@
val status_ticks = Unsynchronized.ref 0;
val last_round = Unsynchronized.ref Time.zeroTime;
-val next_round = Time.fromMilliseconds 50;
+val next_round = seconds 0.05;
fun scheduler_next () = (*requires SYNCHRONIZED*)
let
--- a/src/Pure/Isar/parse.ML Sat Oct 30 15:13:11 2010 -0700
+++ b/src/Pure/Isar/parse.ML Wed Nov 03 07:02:09 2010 -0700
@@ -195,7 +195,7 @@
val nat = number >> (#1 o Library.read_int o Symbol.explode);
val int = Scan.optional (minus >> K ~1) 1 -- nat >> op *;
-val real = float_number >> (the o Real.fromString);
+val real = float_number >> (the o Real.fromString) || int >> Real.fromInt;
val tag_name = group "tag name" (short_ident || string);
val tags = Scan.repeat ($$$ "%" |-- !!! tag_name);
--- a/src/Pure/ML-Systems/multithreading_polyml.ML Sat Oct 30 15:13:11 2010 -0700
+++ b/src/Pure/ML-Systems/multithreading_polyml.ML Wed Nov 03 07:02:09 2010 -0700
@@ -120,10 +120,10 @@
fun tracing_time detailed time =
tracing
(if not detailed then 5
- else if Time.>= (time, Time.fromMilliseconds 1000) then 1
- else if Time.>= (time, Time.fromMilliseconds 100) then 2
- else if Time.>= (time, Time.fromMilliseconds 10) then 3
- else if Time.>= (time, Time.fromMilliseconds 1) then 4 else 5);
+ else if Time.>= (time, seconds 1.0) then 1
+ else if Time.>= (time, seconds 0.1) then 2
+ else if Time.>= (time, seconds 0.01) then 3
+ else if Time.>= (time, seconds 0.001) then 4 else 5);
fun real_time f x =
let
@@ -202,13 +202,13 @@
Posix.Signal.int)
| NONE => ())
handle OS.SysErr _ => () | IO.Io _ =>
- (OS.Process.sleep (Time.fromMilliseconds 100); if n > 0 then kill (n - 1) else ());
+ (OS.Process.sleep (seconds 0.1); if n > 0 then kill (n - 1) else ());
val _ =
while ! result = Wait do
let val res =
sync_wait (SOME orig_atts)
- (SOME (Time.+ (Time.now (), Time.fromMilliseconds 100))) cond lock
+ (SOME (Time.+ (Time.now (), seconds 0.1))) cond lock
in if Exn.is_interrupt_exn res then kill 10 else () end;
(*cleanup*)
--- a/src/Pure/ML-Systems/timing.ML Sat Oct 30 15:13:11 2010 -0700
+++ b/src/Pure/ML-Systems/timing.ML Wed Nov 03 07:02:09 2010 -0700
@@ -1,9 +1,11 @@
(* Title: Pure/ML-Systems/timing.ML
Author: Makarius
-Compiler-independent timing functions.
+Basic support for timing.
*)
+fun seconds s = Time.fromNanoseconds (Real.ceil (s * 1E9));
+
fun start_timing () =
let
val real_timer = Timer.startRealTimer ();
--- a/src/Pure/ProofGeneral/pgip_types.ML Sat Oct 30 15:13:11 2010 -0700
+++ b/src/Pure/ProofGeneral/pgip_types.ML Wed Nov 03 07:02:09 2010 -0700
@@ -22,8 +22,9 @@
(* Types and values (used for preferences and dialogs) *)
- datatype pgiptype = Pgipnull | Pgipbool | Pgipint of int option * int option | Pgipnat
- | Pgipstring | Pgipconst of string | Pgipchoice of pgipdtype list
+ datatype pgiptype =
+ Pgipnull | Pgipbool | Pgipint of int option * int option | Pgipnat | Pgipreal
+ | Pgipstring | Pgipconst of string | Pgipchoice of pgipdtype list
and pgipdtype = Pgipdtype of string option * pgiptype (* type with opt. description *)
@@ -70,7 +71,9 @@
val read_pgipint : (int option * int option) -> string -> int (* raises PGIP *)
val read_pgipnat : string -> int (* raises PGIP *)
val read_pgipbool : string -> bool (* raises PGIP *)
+ val read_pgipreal : string -> real (* raises PGIP *)
val read_pgipstring : string -> string (* raises PGIP *)
+ val real_to_pgstring : real -> string
val int_to_pgstring : int -> string
val bool_to_pgstring : bool -> string
val string_to_pgstring : string -> string
@@ -203,6 +206,11 @@
else raise PGIP ("Invalid natural number: " ^ quote s)
| NONE => raise PGIP ("Invalid natural number: " ^ quote s))
+fun read_pgipreal s =
+ (case Real.fromString s of
+ SOME x => x
+ | NONE => raise PGIP ("Invalid floating-point number: " ^ quote s))
+
(* NB: we can maybe do without xml decode/encode here. *)
fun read_pgipstring s = (* non-empty strings, XML escapes decoded *)
(case XML.parse_string s of
@@ -212,6 +220,8 @@
val int_to_pgstring = signed_string_of_int
+val real_to_pgstring = signed_string_of_real
+
fun string_to_pgstring s = XML.text s
fun bool_to_pgstring b = if b then "true" else "false"
@@ -238,6 +248,7 @@
| Pgipbool (* booleans: "true" or "false" *)
| Pgipint of int option * int option (* ranged integers, should be XSD canonical *)
| Pgipnat (* naturals: non-negative integers (convenience) *)
+ | Pgipreal (* floating-point numbers *)
| Pgipstring (* non-empty strings *)
| Pgipconst of string (* singleton type *)
| Pgipchoice of pgipdtype list (* union type *)
@@ -246,8 +257,9 @@
and pgipdtype = Pgipdtype of string option * pgiptype
-datatype pgipuval = Pgvalnull | Pgvalbool of bool | Pgvalint of int | Pgvalnat of int
- | Pgvalstring of string | Pgvalconst of string
+datatype pgipuval =
+ Pgvalnull | Pgvalbool of bool | Pgvalint of int | Pgvalnat of int | Pgvalreal of real
+ | Pgvalstring of string | Pgvalconst of string
type pgipval = pgiptype * pgipuval (* type-safe values *)
@@ -260,6 +272,7 @@
| Pgipbool => "pgipbool"
| Pgipint _ => "pgipint"
| Pgipnat => "pgipint"
+ | Pgipreal => "pgipint" (* FIXME sic? *)
| Pgipstring => "pgipstring"
| Pgipconst _ => "pgipconst"
| Pgipchoice _ => "pgipchoice"
@@ -291,6 +304,7 @@
| read_pguval Pgipbool s = Pgvalbool (read_pgipbool s)
| read_pguval (Pgipint range) s = Pgvalint (read_pgipint range s)
| read_pguval Pgipnat s = Pgvalnat (read_pgipnat s)
+ | read_pguval Pgipreal s = Pgvalreal (read_pgipreal s)
| read_pguval (Pgipconst c) s =
if c=s then Pgvalconst c
else raise PGIP ("Given string: "^quote s^" doesn't match expected string: "^quote c)
@@ -315,6 +329,7 @@
| pgval_to_string (_, Pgvalbool b) = bool_to_pgstring b
| pgval_to_string (_, Pgvalnat n) = int_to_pgstring n
| pgval_to_string (_, Pgvalint i) = int_to_pgstring i
+ | pgval_to_string (_, Pgvalreal x) = real_to_pgstring x
| pgval_to_string (_, Pgvalconst c) = string_to_pgstring c
| pgval_to_string (_, Pgvalstring s) = string_to_pgstring s
--- a/src/Pure/ProofGeneral/preferences.ML Sat Oct 30 15:13:11 2010 -0700
+++ b/src/Pure/ProofGeneral/preferences.ML Wed Nov 03 07:02:09 2010 -0700
@@ -20,6 +20,7 @@
val generic_pref: ('a -> string) -> (string -> 'a) -> PgipTypes.pgiptype ->
'a Unsynchronized.ref -> string -> string -> preference
val string_pref: string Unsynchronized.ref -> string -> string -> preference
+ val real_pref: real Unsynchronized.ref -> string -> string -> preference
val int_pref: int Unsynchronized.ref -> string -> string -> preference
val nat_pref: int Unsynchronized.ref -> string -> string -> preference
val bool_pref: bool Unsynchronized.ref -> string -> string -> preference
@@ -65,6 +66,9 @@
val string_pref = generic_pref I I PgipTypes.Pgipstring;
+val real_pref =
+ generic_pref PgipTypes.real_to_pgstring PgipTypes.read_pgipreal PgipTypes.Pgipreal;
+
val int_pref =
generic_pref PgipTypes.int_to_pgstring (PgipTypes.read_pgipint (NONE, NONE))
(PgipTypes.Pgipint (NONE, NONE));
--- a/src/Pure/System/isabelle_process.ML Sat Oct 30 15:13:11 2010 -0700
+++ b/src/Pure/System/isabelle_process.ML Wed Nov 03 07:02:09 2010 -0700
@@ -81,7 +81,7 @@
(case receive mbox of
SOME msg =>
(List.app (fn s => TextIO.output (out_stream, s)) msg;
- loop (Mailbox.receive_timeout (Time.fromMilliseconds 20)))
+ loop (Mailbox.receive_timeout (seconds 0.02)))
| NONE => (try TextIO.flushOut out_stream; loop (SOME o Mailbox.receive)));
in fn () => loop (SOME o Mailbox.receive) end;
@@ -165,7 +165,7 @@
fun init in_fifo out_fifo = ignore (Simple_Thread.fork false (fn () =>
let
- val _ = OS.Process.sleep (Time.fromMilliseconds 500); (*yield to raw ML toplevel*)
+ val _ = OS.Process.sleep (seconds 0.5); (*yield to raw ML toplevel*)
val _ = Output.raw_stdout Symbol.STX;
val _ = quick_and_dirty := true; (* FIXME !? *)
--- a/src/Tools/Code/code_runtime.ML Sat Oct 30 15:13:11 2010 -0700
+++ b/src/Tools/Code/code_runtime.ML Wed Nov 03 07:02:09 2010 -0700
@@ -418,8 +418,7 @@
(0, Path.implode filepath) false (File.read filepath);
val thy'' = (Context.the_theory o the) (Context.thread_data ());
val names = Loaded_Values.get thy'';
- val thy''' = Thy_Load.provide_file filepath thy'';
- in (names, thy''') end;
+ in (names, thy'') end;
end;
--- a/src/Tools/subtyping.ML Sat Oct 30 15:13:11 2010 -0700
+++ b/src/Tools/subtyping.ML Wed Nov 03 07:02:09 2010 -0700
@@ -762,7 +762,7 @@
Attrib.setup @{binding coercion}
(Args.term >> (fn t => Thm.declaration_attribute (K (add_coercion t))))
"declaration of new coercions" #>
- Attrib.setup @{binding map_function}
+ Attrib.setup @{binding coercion_map}
(Args.term >> (fn t => Thm.declaration_attribute (K (add_type_map t))))
"declaration of new map functions";