--- a/etc/options Tue Aug 27 17:08:51 2019 +0200
+++ b/etc/options Tue Aug 27 19:22:57 2019 +0200
@@ -216,6 +216,9 @@
option headless_commit_cleanup_delay : real = 60
-- "delay for cleanup of already imported theories (seconds, 0 = disabled)"
+option execution_eager : bool = false
+ -- "prefer theories with shorter stack of decendants"
+
section "Miscellaneous Tools"
--- a/src/HOL/Analysis/Interval_Integral.thy Tue Aug 27 17:08:51 2019 +0200
+++ b/src/HOL/Analysis/Interval_Integral.thy Tue Aug 27 19:22:57 2019 +0200
@@ -8,10 +8,6 @@
imports Equivalence_Lebesgue_Henstock_Integration
begin
-lemma continuous_on_vector_derivative:
- "(\<And>x. x \<in> S \<Longrightarrow> (f has_vector_derivative f' x) (at x within S)) \<Longrightarrow> continuous_on S f"
- by (auto simp: continuous_on_eq_continuous_within intro!: has_vector_derivative_continuous)
-
definition "einterval a b = {x. a < ereal x \<and> ereal x < b}"
lemma einterval_eq[simp]:
--- a/src/HOL/Deriv.thy Tue Aug 27 17:08:51 2019 +0200
+++ b/src/HOL/Deriv.thy Tue Aug 27 19:22:57 2019 +0200
@@ -797,6 +797,10 @@
"(f has_vector_derivative D) (at x within s) \<Longrightarrow> continuous (at x within s) f"
by (auto intro: has_derivative_continuous simp: has_vector_derivative_def)
+lemma continuous_on_vector_derivative:
+ "(\<And>x. x \<in> S \<Longrightarrow> (f has_vector_derivative f' x) (at x within S)) \<Longrightarrow> continuous_on S f"
+ by (auto simp: continuous_on_eq_continuous_within intro!: has_vector_derivative_continuous)
+
lemma has_vector_derivative_mult_right[derivative_intros]:
fixes a :: "'a::real_normed_algebra"
shows "(f has_vector_derivative x) F \<Longrightarrow> ((\<lambda>x. a * f x) has_vector_derivative (a * x)) F"
--- a/src/HOL/Tools/Function/function.ML Tue Aug 27 17:08:51 2019 +0200
+++ b/src/HOL/Tools/Function/function.ML Tue Aug 27 19:22:57 2019 +0200
@@ -59,7 +59,7 @@
|> map (apfst (apsnd (fn ats => moreatts @ ats)))
|> map (apfst (apfst extra_qualify))
- val (saved_spec_simps, lthy) =
+ val (saved_spec_simps, lthy') =
fold_map Local_Theory.note spec lthy
val saved_simps = maps snd saved_spec_simps
@@ -67,7 +67,7 @@
fun note fname simps =
Local_Theory.note ((mod_binding (derived_name fname label), []), simps) #> snd
- in (saved_simps, fold2 note fnames simps_by_f lthy) end
+ in (saved_simps, fold2 note fnames simps_by_f lthy') end
fun prepare_function do_print prep fixspec eqns config lthy =
let
@@ -88,20 +88,20 @@
val ((goal_state, cont), lthy') =
Function_Mutual.prepare_function_mutual config defname fixes0 eqs lthy
- fun afterqed [[proof]] lthy =
+ fun afterqed [[proof]] lthy1 =
let
- val result = cont lthy (Thm.close_derivation \<^here> proof)
+ val result = cont lthy1 (Thm.close_derivation \<^here> proof)
val FunctionResult {fs, R, dom, psimps, simple_pinducts,
termination, domintros, cases, ...} = result
- val pelims = Function_Elims.mk_partial_elim_rules lthy result
+ val pelims = Function_Elims.mk_partial_elim_rules lthy1 result
val concealed_partial = if partials then I else Binding.concealed
val addsmps = add_simps fnames post sort_cont
- val (((((psimps', [pinducts']), [termination']), cases'), pelims'), lthy) =
- lthy
+ val (((((psimps', [pinducts']), [termination']), cases'), pelims'), lthy2) =
+ lthy1
|> addsmps (concealed_partial o Binding.qualify false "partial")
"psimps" concealed_partial psimp_attribs psimps
||>> Local_Theory.notes [((concealed_partial (derived_name defname "pinduct"), []),
@@ -125,11 +125,11 @@
pelims=pelims',elims=NONE}
val _ =
- Proof_Display.print_consts do_print (Position.thread_data ()) lthy
+ Proof_Display.print_consts do_print (Position.thread_data ()) lthy2
(K false) (map fst fixes)
in
(info,
- lthy |> Local_Theory.declaration {syntax = false, pervasive = false}
+ lthy2 |> Local_Theory.declaration {syntax = false, pervasive = false}
(fn phi => add_function_data (transform_function_data phi info)))
end
in
@@ -165,7 +165,7 @@
val function = gen_function false Specification.check_multi_specs
fun function_cmd a b c int = gen_function int Specification.read_multi_specs a b c
-fun prepare_termination_proof mod_binding prep_term raw_term_opt lthy =
+fun prepare_termination_proof prep_binding prep_term raw_term_opt lthy =
let
val term_opt = Option.map (prep_term lthy) raw_term_opt
val info =
@@ -183,32 +183,32 @@
pinducts, defname, fnames, cases, dom, pelims, ...} = info
val domT = domain_type (fastype_of R)
val goal = HOLogic.mk_Trueprop (HOLogic.mk_all ("x", domT, mk_acc domT R $ Free ("x", domT)))
- fun afterqed [[totality]] lthy =
+ fun afterqed [[raw_totality]] lthy1 =
let
- val totality = Thm.close_derivation \<^here> totality
+ val totality = Thm.close_derivation \<^here> raw_totality
val remove_domain_condition =
- full_simplify (put_simpset HOL_basic_ss lthy
+ full_simplify (put_simpset HOL_basic_ss lthy1
addsimps [totality, @{thm True_implies_equals}])
val tsimps = map remove_domain_condition psimps
val tinduct = map remove_domain_condition pinducts
val telims = map (map remove_domain_condition) pelims
in
- lthy
- |> add_simps I "simps" mod_binding simp_attribs tsimps
+ lthy1
+ |> add_simps prep_binding "simps" prep_binding simp_attribs tsimps
||> Code.declare_default_eqns (map (rpair true) tsimps)
||>> Local_Theory.note
- ((mod_binding (derived_name defname "induct"), [Attrib.case_names case_names]), tinduct)
+ ((prep_binding (derived_name defname "induct"), [Attrib.case_names case_names]), tinduct)
||>> fold_map (note_derived ("elims", [Attrib.consumes 1, Attrib.constraints 1]))
- (map mod_binding fnames ~~ telims)
- |-> (fn ((simps,(_,inducts)), elims) => fn lthy =>
+ (map prep_binding fnames ~~ telims)
+ |-> (fn ((simps,(_,inducts)), elims) => fn lthy2 =>
let val info' = { is_partial=false, defname=defname, fnames=fnames, add_simps=add_simps,
case_names=case_names, fs=fs, R=R, dom=dom, psimps=psimps, pinducts=pinducts,
simps=SOME simps, inducts=SOME inducts, termination=termination, totality=SOME totality,
cases=cases, pelims=pelims, elims=SOME elims}
- |> transform_function_data (Morphism.binding_morphism "" mod_binding)
+ |> transform_function_data (Morphism.binding_morphism "" prep_binding)
in
(info',
- lthy
+ lthy2
|> Local_Theory.declaration {syntax = false, pervasive = false}
(fn phi => add_function_data (transform_function_data phi info'))
|> Spec_Rules.add Spec_Rules.equational_recdef (fs, tsimps))
--- a/src/Pure/General/graph.ML Tue Aug 27 17:08:51 2019 +0200
+++ b/src/Pure/General/graph.ML Tue Aug 27 19:22:57 2019 +0200
@@ -41,6 +41,7 @@
val is_minimal: 'a T -> key -> bool
val is_maximal: 'a T -> key -> bool
val is_isolated: 'a T -> key -> bool
+ val maximal_descendants: 'a T -> key -> int option
val new_node: key * 'a -> 'a T -> 'a T (*exception DUP*)
val default_node: key * 'a -> 'a T -> 'a T
val del_node: key -> 'a T -> 'a T (*exception UNDEF*)
@@ -180,6 +181,16 @@
fun is_isolated G x = is_minimal G x andalso is_maximal G x;
+(*longest path to some maximal element*)
+fun maximal_descendants G =
+ let
+ val next = imm_preds G;
+ fun reach depth x R =
+ if (case Table.lookup R x of SOME d => d >= depth | NONE => false) then R
+ else Keys.fold_rev (reach (depth + 1)) (next x) (Table.update (x, depth) R);
+ val result = fold (reach 0) (maximals G) Table.empty;
+ in Table.lookup result end;
+
(* node operations *)
--- a/src/Pure/PIDE/document.ML Tue Aug 27 17:08:51 2019 +0200
+++ b/src/Pure/PIDE/document.ML Tue Aug 27 19:22:57 2019 +0200
@@ -493,6 +493,27 @@
Symtab.update (a, ())) all_visible all_required
end;
+structure Eager_Graph = Graph(type key = int * string val ord = prod_ord int_ord string_ord);
+
+fun schedule_execution f nodes =
+ if Options.default_bool \<^system_option>\<open>execution_eager\<close>
+ then
+ let
+ val decorate = the o String_Graph.maximal_descendants nodes;
+ fun add_node (d, a) = Eager_Graph.default_node ((d, a), String_Graph.get_node nodes a);
+ in
+ (nodes, Eager_Graph.empty) |-> String_Graph.fold (fn (a, (_, (preds, _))) =>
+ let
+ val a' = `decorate a;
+ val bs' = String_Graph.Keys.fold (cons o `decorate) preds [];
+ in
+ fold add_node (a' :: bs')
+ #> fold (fn b' => Eager_Graph.add_edge (b', a')) bs'
+ end)
+ |> Eager_Graph.schedule (fn deps => fn ((_, x), y) => f (map (apfst #2) deps) (x, y))
+ end
+ else String_Graph.schedule f nodes;
+
fun start_execution state = state |> map_state (fn (versions, blobs, commands, execution) =>
timeit "Document.start_execution" (fn () =>
let
@@ -513,7 +534,7 @@
val nodes = nodes_of (the_version state version_id);
val required = make_required nodes;
val _ =
- nodes |> String_Graph.schedule
+ nodes |> schedule_execution
(fn deps => fn (name, node) =>
if Symtab.defined required name orelse visible_node node orelse pending_result node then
let