# HG changeset patch # User huffman # Date 1288792929 25200 # Node ID 3b7f570723f9908e5b29662b04c508359817bd66 # Parent 73f2b99b549d6e59da4b0a8f0f4720fa0f5ac48c# Parent abc52faa7761eabb46a4c141b7e04dd55608222a merged diff -r 73f2b99b549d -r 3b7f570723f9 NEWS --- 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. diff -r 73f2b99b549d -r 3b7f570723f9 doc-src/IsarImplementation/Thy/ML.thy --- 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 {* diff -r 73f2b99b549d -r 3b7f570723f9 doc-src/IsarImplementation/Thy/Prelim.thy --- 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]] diff -r 73f2b99b549d -r 3b7f570723f9 doc-src/IsarImplementation/Thy/document/ML.tex --- 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% diff -r 73f2b99b549d -r 3b7f570723f9 doc-src/IsarImplementation/Thy/document/Prelim.tex --- 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}% } diff -r 73f2b99b549d -r 3b7f570723f9 doc-src/IsarRef/Thy/Outer_Syntax.thy --- 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}. *} diff -r 73f2b99b549d -r 3b7f570723f9 doc-src/IsarRef/Thy/document/Outer_Syntax.tex --- 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% % diff -r 73f2b99b549d -r 3b7f570723f9 src/HOL/Algebra/Congruence.thy --- 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 \ carrier S \ x .= x" and sym [sym]: "\ x .= y; x \ carrier S; y \ carrier S \ \ y .= x" - and trans [trans]: "\ x .= y; y .= z; x \ carrier S; y \ carrier S; z \ carrier S \ \ x .= z" + and trans [trans]: + "\ x .= y; y .= z; x \ carrier S; y \ carrier S; z \ carrier S \ \ x .= z" (* Lemmas by Stephan Hohe *) diff -r 73f2b99b549d -r 3b7f570723f9 src/HOL/Algebra/Lattice.thy --- 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 \ y; y \ z; x \ carrier L; y \ carrier L; z \ carrier L |] ==> x \ z" and le_cong: - "\ x .= y; z .= w; x \ carrier L; y \ carrier L; z \ carrier L; w \ carrier L \ \ x \ z \ y \ w" + "\ x .= y; z .= w; x \ carrier L; y \ carrier L; z \ carrier L; w \ carrier L \ \ + x \ z \ y \ w" definition lless :: "[_, 'a, 'a] => bool" (infixl "\\" 50) diff -r 73f2b99b549d -r 3b7f570723f9 src/HOL/Finite_Set.thy --- 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) \ card A > card(f ` A) \ ~ inj_on f A " +lemma pigeonhole: "card A > card(f ` A) \ ~ inj_on f A " by (auto dest: card_image less_irrefl_nat) lemma pigeonhole_infinite: diff -r 73f2b99b549d -r 3b7f570723f9 src/HOL/Library/Multiset.thy --- 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 "\k \ f ` set ys. filter (\x. k = f x) ys = filter (\x. k = f x) xs" + and "\k. k \ set ys \ filter (\x. f k = f x) ys = filter (\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 - "\k \ f ` set ys. filter (\x. k = f x) (remove1 x ys) = filter (\x. k = f x) xs" + "\k \ set ys. filter (\x. f k = f x) (remove1 x ys) = filter (\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 "\k. replicate (length (filter (\y. k = y) ys)) k = replicate (length (filter (\x. k = x) xs)) k" by simp - then show "\k \ (\x. x) ` set ys. filter (\y. k = y) ys = filter (\x. k = x) xs" + then show "\k. k \ set ys \ filter (\y. k = y) ys = filter (\x. k = x) xs" by (simp add: replicate_length_filter) qed +lemma sort_key_by_quicksort: + "sort_key f xs = sort_key f [x\xs. f x < f (xs ! (length xs div 2))] + @ [x\xs. f x = f (xs ! (length xs div 2))] + @ sort_key f [x\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 \ set ?rhs" + have *: "\x P. P (f x) \ f l = f x \ P (f l) \ f l = f x" by auto + have **: "\x. f l = f x \ f x = f l" by auto + have "[x \ sort_key f xs . f x = f l] = [x \ xs. f x = f l]" + unfolding filter_sort by (rule properties_for_sort_key) (auto intro: sorted_map_same) + with ** have [simp]: "[x \ sort_key f xs . f l = f x] = [x \ xs. f l = f x]" by simp + let ?pivot = "f (xs ! (length xs div 2))" + show "[x \ ?rhs. f l = f x] = [x \ ?lhs. f l = f x]" + proof (cases "f l" ?pivot rule: linorder_cases) + case less then moreover have "f l \ ?pivot" and "\ 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 \ ?pivot" and "\ 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\xs. x < xs ! (length xs div 2)] + @ [x\xs. x = xs ! (length xs div 2)] + @ sort [x\xs. x > xs ! (length xs div 2)]" (is "sort ?lhs = ?rhs") + using sort_key_by_quicksort [of "\x. x", symmetric] by simp + end lemma multiset_of_remdups_le: "multiset_of (remdups xs) \ multiset_of xs" diff -r 73f2b99b549d -r 3b7f570723f9 src/HOL/List.thy --- 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\xs. x = f xs]" -proof (induct xs arbitrary: f) +lemma sorted_map_same: + "sorted (map f [x\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\xs . y = (\xs. x) xs]" . - moreover from Cons have "sorted [y\xs . y = (f \ Cons x) xs]" . + then have "sorted (map f [y\xs . f y = (\xs. f x) xs])" . + moreover from Cons have "sorted (map f [y\xs . f y = (g \ Cons x) xs])" . ultimately show ?case by (simp_all add: sorted_Cons) qed +lemma sorted_same: + "sorted [x\xs. x = g xs]" + using sorted_map_same [of "\x. x"] by simp + lemma remove1_insort [simp]: "remove1 x (insort x xs) = xs" by (induct xs) simp_all diff -r 73f2b99b549d -r 3b7f570723f9 src/HOL/Matrix/Cplex_tools.ML --- 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 = diff -r 73f2b99b549d -r 3b7f570723f9 src/HOL/Matrix/matrixlp.ML --- 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 diff -r 73f2b99b549d -r 3b7f570723f9 src/HOL/Mirabelle/Tools/mirabelle_sledgehammer.ML --- 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 diff -r 73f2b99b549d -r 3b7f570723f9 src/HOL/Mutabelle/mutabelle_extra.ML --- 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) diff -r 73f2b99b549d -r 3b7f570723f9 src/HOL/Predicate_Compile_Examples/Context_Free_Grammar_Example.thy --- 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}) *} diff -r 73f2b99b549d -r 3b7f570723f9 src/HOL/Tools/Predicate_Compile/code_prolog.ML --- 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}) = diff -r 73f2b99b549d -r 3b7f570723f9 src/HOL/Tools/Predicate_Compile/predicate_compile_core.ML --- 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" diff -r 73f2b99b549d -r 3b7f570723f9 src/HOL/Tools/async_manager.ML --- 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 diff -r 73f2b99b549d -r 3b7f570723f9 src/HOL/Tools/try.ML --- 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 diff -r 73f2b99b549d -r 3b7f570723f9 src/HOL/ex/Coercion_Examples.thy --- 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 \ int) \ nat" consts arg :: "int \ nat" @@ -36,6 +36,8 @@ term "[1::int] = func" *) +(* Coercion/type maps definitions *) + primrec nat_of_bool :: "bool \ 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 \ 'b) \ ('c \ 'd) \ ('b \ 'c) \ ('a \ 'd)" where "map_fun f g h = g o h o f" -declare [[map_function "\ f g h . g o h o f"]] +declare [[coercion_map "\ f g h . g o h o f"]] primrec map_pair :: "('a \ 'c) \ ('b \ 'd) \ ('a * 'b) \ ('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 *) diff -r 73f2b99b549d -r 3b7f570723f9 src/Pure/Concurrent/future.ML --- 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 diff -r 73f2b99b549d -r 3b7f570723f9 src/Pure/Isar/parse.ML --- 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); diff -r 73f2b99b549d -r 3b7f570723f9 src/Pure/ML-Systems/multithreading_polyml.ML --- 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*) diff -r 73f2b99b549d -r 3b7f570723f9 src/Pure/ML-Systems/timing.ML --- 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 (); diff -r 73f2b99b549d -r 3b7f570723f9 src/Pure/ProofGeneral/pgip_types.ML --- 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 diff -r 73f2b99b549d -r 3b7f570723f9 src/Pure/ProofGeneral/preferences.ML --- 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)); diff -r 73f2b99b549d -r 3b7f570723f9 src/Pure/System/isabelle_process.ML --- 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 !? *) diff -r 73f2b99b549d -r 3b7f570723f9 src/Tools/Code/code_runtime.ML --- 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; diff -r 73f2b99b549d -r 3b7f570723f9 src/Tools/subtyping.ML --- 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";