From c318a983e078b6c729425f21526c6896ba55df09 Mon Sep 17 00:00:00 2001 From: Emilio Jesus Gallego Arias Date: Mon, 13 Mar 2017 18:06:29 +0100 Subject: [future] Use eager evaluation for chaining values. The current future system is lazy when "chaining" (*) a resolved future, which implies that chaining with a resolved future will produce a non-resolved one. This misfeature interacts badly with the "purification" optimization, which in turn provokes a swarm of spurious state setting calls in real use. To solve this problem, we revert to the more natural semantics of respecting the evaluation semantics when mapping over a future, indeed respecting the previous resolution status. This commit solves a kind of _critical_ bug in the current system, with the particular bad path origination in `Future.split2` due to the following accumulation of circumstances: ``` split2 x -> chain x (fun x -> fst x) => let y = chain ~pure x (fun x -> fst x) in if is_over x && greedy then ignore(force ~pure y); y => [y <- Closure (fun x -> fst x)] ignore(force (Closure (fun x -> fst x))) => purify_future (force ~pure) (Closure (fun x -> fst x)) ``` and then, the test in `purify_future` fails, triggering the spurious state reset operation. This problem was first noted at https://sympa.inria.fr/sympa/arc/coqdev/2016-02/msg00081.html , and seems related to https://coq.inria.fr/bugs/show_bug.cgi?id=5382 We fix the problem by making chaining eager, but other solutions would be possible. Given that the main user of `chain` is `split2` which does `snd/fst`, I recommend this solution. The difference in calls to `unfreeze_state` is dramatic: ``` | File | Freeze Calls After | Freeze Calls Before | |----------------------------------------+--------------------+---------------------| | theories/Init/Notations.v | 0 | 0 | | theories/Init/Logic.v | 57 | 614 | | theories/Init/Datatypes.v | 13 | 132 | | theories/Init/Logic_Type.v | 7 | 57 | | theories/Init/Specif.v | 5 | 35 | | theories/Init/Nat.v | 0 | 0 | | theories/Init/Peano.v | 22 | 264 | | theories/Init/Wf.v | 8 | 89 | | theories/Init/Tactics.v | 2 | 24 | | theories/Init/Tauto.v | 0 | 0 | | theories/Init/Prelude.v | 0 | 0 | | Bool/Bool.v | 104 | 1220 | | Program/Basics.v | 0 | 0 | | Classes/Init.v | 0 | 0 | | Program/Tactics.v | 0 | 0 | | Relations/Relation_Definitions.v | 0 | 0 | | Classes/RelationClasses.v | 21 | 341 | | Classes/Morphisms.v | 47 | 689 | | Classes/CRelationClasses.v | 18 | 245 | | Classes/CMorphisms.v | 50 | 587 | | Classes/Morphisms_Prop.v | 3 | 127 | | Classes/Equivalence.v | 6 | 105 | | Classes/SetoidTactics.v | 0 | 0 | | Setoids/Setoid.v | 4 | 33 | | Structures/Equalities.v | 8 | 93 | | Relations/Relation_Operators.v | 0 | 0 | | Relations/Operators_Properties.v | 35 | 627 | | Relations/Relations.v | 2 | 24 | | Structures/Orders.v | 12 | 148 | | Numbers/NumPrelude.v | 0 | 0 | | Structures/OrdersTac.v | 13 | 234 | | Structures/OrdersFacts.v | 73 | 931 | | Structures/GenericMinMax.v | 82 | 1294 | | Numbers/NatInt/NZAxioms.v | 0 | 0 | | Numbers/NatInt/NZBase.v | 7 | 87 | | Numbers/NatInt/NZAdd.v | 14 | 168 | | Numbers/NatInt/NZMul.v | 12 | 144 | | Logic/Decidable.v | 28 | 336 | | Numbers/NatInt/NZOrder.v | 81 | 1174 | | Numbers/NatInt/NZAddOrder.v | 24 | 288 | | Numbers/NatInt/NZMulOrder.v | 46 | 552 | | Numbers/NatInt/NZParity.v | 35 | 420 | | Numbers/NatInt/NZPow.v | 29 | 348 | | Numbers/NatInt/NZSqrt.v | 54 | 673 | | Numbers/NatInt/NZLog.v | 64 | 797 | | Numbers/NatInt/NZDiv.v | 49 | 588 | | Numbers/NatInt/NZGcd.v | 36 | 432 | | Numbers/NatInt/NZBits.v | 0 | 0 | | Numbers/Natural/Abstract/NAxioms.v | 0 | 0 | | Numbers/NatInt/NZProperties.v | 0 | 0 | | Numbers/Natural/Abstract/NBase.v | 14 | 177 | | Numbers/Natural/Abstract/NAdd.v | 6 | 72 | | Numbers/Natural/Abstract/NOrder.v | 29 | 349 | | Numbers/Natural/Abstract/NAddOrder.v | 5 | 60 | | Numbers/Natural/Abstract/NMulOrder.v | 8 | 96 | | Numbers/Natural/Abstract/NSub.v | 36 | 432 | | Numbers/Natural/Abstract/NMaxMin.v | 18 | 216 | | Numbers/Natural/Abstract/NParity.v | 4 | 48 | | Numbers/Natural/Abstract/NPow.v | 26 | 312 | | Numbers/Natural/Abstract/NSqrt.v | 9 | 108 | | Numbers/Natural/Abstract/NLog.v | 0 | 0 | | Numbers/Natural/Abstract/NDiv.v | 50 | 600 | | Numbers/Natural/Abstract/NGcd.v | 14 | 168 | | Numbers/Natural/Abstract/NLcm.v | 29 | 348 | | Numbers/Natural/Abstract/NBits.v | 168 | 2016 | | Numbers/Natural/Abstract/NProperties.v | 0 | 0 | | Arith/PeanoNat.v | 77 | 990 | | Arith/Le.v | 2 | 57 | | Arith/Lt.v | 14 | 168 | | Arith/Plus.v | 20 | 269 | | Arith/Gt.v | 17 | 248 | | Arith/Minus.v | 11 | 132 | | Arith/Mult.v | 14 | 168 | | Arith/Between.v | 19 | 299 | | Logic/EqdepFacts.v | 26 | 539 | | Logic/Eqdep_dec.v | 13 | 361 | | Arith/Peano_dec.v | 3 | 26 | | Arith/Compare_dec.v | 35 | 360 | | Arith/Factorial.v | 3 | 36 | | Arith/EqNat.v | 10 | 111 | | Arith/Wf_nat.v | 18 | 173 | | Arith/Arith_base.v | 0 | 0 | | Numbers/BinNums.v | 0 | 0 | | PArith/BinPosDef.v | 0 | 0 | | PArith/BinPos.v | 229 | 2810 | | NArith/BinNatDef.v | 0 | 0 | | NArith/BinNat.v | 107 | 1330 | | PArith/Pnat.v | 51 | 688 | | NArith/Nnat.v | 30 | 360 | | setoid_ring/Ring_theory.v | 43 | 756 | | Lists/List.v | 195 | 2908 | | setoid_ring/BinList.v | 6 | 90 | | Numbers/Integer/Abstract/ZAxioms.v | 0 | 0 | | Numbers/Integer/Abstract/ZBase.v | 3 | 36 | | Numbers/Integer/Abstract/ZAdd.v | 46 | 552 | | Numbers/Integer/Abstract/ZMul.v | 8 | 96 | | Numbers/Integer/Abstract/ZLt.v | 21 | 252 | | Numbers/Integer/Abstract/ZAddOrder.v | 45 | 543 | | Numbers/Integer/Abstract/ZMulOrder.v | 24 | 288 | | Numbers/Integer/Abstract/ZMaxMin.v | 22 | 264 | | Numbers/Integer/Abstract/ZSgnAbs.v | 41 | 492 | | Numbers/Integer/Abstract/ZParity.v | 6 | 72 | | Numbers/Integer/Abstract/ZPow.v | 10 | 120 | | Numbers/Integer/Abstract/ZDivTrunc.v | 68 | 816 | | Numbers/Integer/Abstract/ZDivFloor.v | 70 | 840 | | Numbers/Integer/Abstract/ZGcd.v | 29 | 348 | | Numbers/Integer/Abstract/ZLcm.v | 50 | 600 | | Numbers/Integer/Abstract/ZBits.v | 205 | 2460 | | Numbers/Integer/Abstract/ZProperties.v | 0 | 0 | | ZArith/BinIntDef.v | 0 | 0 | | ZArith/BinInt.v | 212 | 2839 | |----------------------------------------+--------------------+---------------------| ``` (*) I would call it `Future.map` better than chain. --- lib/future.ml | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/lib/future.ml b/lib/future.ml index ea0382a63..ca73d5e39 100644 --- a/lib/future.ml +++ b/lib/future.ml @@ -151,8 +151,8 @@ let chain ~pure ck f = create ~uuid ~name fix_exn (match !c with | Closure _ | Delegated _ -> Closure (fun () -> f (force ~pure ck)) | Exn _ as x -> x - | Val (v, None) when pure -> Closure (fun () -> f v) - | Val (v, Some _) when pure -> Closure (fun () -> f v) + | Val (v, None) when pure -> Val (f v, None) + | Val (v, Some _) when pure -> Val (f v, None) | Val (v, Some state) -> Closure (fun () -> !unfreeze state; f v) | Val (v, None) -> match !ck with -- cgit v1.2.3 From ea8185d872f242f8ebf4274ebe550ed81107150a Mon Sep 17 00:00:00 2001 From: Pierre-Marie Pédrot Date: Sun, 12 Mar 2017 19:57:48 +0100 Subject: Making the side_effects type opaque. We move it from Entries to Term_typing and export the few functions needed to manipulate it in this module. --- kernel/entries.mli | 2 -- kernel/safe_typing.ml | 12 ++++++------ kernel/safe_typing.mli | 2 +- kernel/term_typing.ml | 17 ++++++++++++----- kernel/term_typing.mli | 7 ++++++- 5 files changed, 25 insertions(+), 15 deletions(-) diff --git a/kernel/entries.mli b/kernel/entries.mli index ea7c266bc..5287a009e 100644 --- a/kernel/entries.mli +++ b/kernel/entries.mli @@ -113,5 +113,3 @@ type side_effect = { from_env : Declarations.structure_body CEphemeron.key; eff : side_eff; } - -type side_effects = side_effect list diff --git a/kernel/safe_typing.ml b/kernel/safe_typing.ml index bc1cb63d8..e3b87bbe1 100644 --- a/kernel/safe_typing.ml +++ b/kernel/safe_typing.ml @@ -206,19 +206,19 @@ let get_opaque_body env cbo = Opaqueproof.force_constraints (Environ.opaque_tables env) opaque) type private_constant = Entries.side_effect -type private_constants = private_constant list +type private_constants = Term_typing.side_effects type private_constant_role = Term_typing.side_effect_role = | Subproof | Schema of inductive * string -let empty_private_constants = [] -let add_private x xs = if List.mem_f Term_typing.equal_eff x xs then xs else x :: xs -let concat_private xs ys = List.fold_right add_private xs ys +let empty_private_constants = Term_typing.empty_seff +let add_private = Term_typing.add_seff +let concat_private = Term_typing.concat_seff let mk_pure_proof = Term_typing.mk_pure_proof let inline_private_constants_in_constr = Term_typing.inline_side_effects let inline_private_constants_in_definition_entry = Term_typing.inline_entry_side_effects -let side_effects_of_private_constants x = Term_typing.uniq_seff (List.rev x) +let side_effects_of_private_constants = Term_typing.uniq_seff let private_con_of_con env c = let cbo = Environ.lookup_constant c env.env in @@ -248,7 +248,7 @@ let universes_of_private eff = | Entries.SEsubproof (c, cb, e) -> if cb.const_polymorphic then acc else Univ.ContextSet.of_context cb.const_universes :: acc) - [] eff + [] (Term_typing.uniq_seff eff) let env_of_safe_env senv = senv.env let env_of_senv = env_of_safe_env diff --git a/kernel/safe_typing.mli b/kernel/safe_typing.mli index 15ebc7d88..8bc47d6ce 100644 --- a/kernel/safe_typing.mli +++ b/kernel/safe_typing.mli @@ -47,7 +47,7 @@ type private_constant_role = | Schema of inductive * string val side_effects_of_private_constants : - private_constants -> Entries.side_effects + private_constants -> Entries.side_effect list val empty_private_constants : private_constants val add_private : private_constant -> private_constants -> private_constants diff --git a/kernel/term_typing.ml b/kernel/term_typing.ml index b7597ba7f..24da308b4 100644 --- a/kernel/term_typing.ml +++ b/kernel/term_typing.ml @@ -37,13 +37,20 @@ let equal_eff e1 e2 = cl1 cl2 | _ -> false -let rec uniq_seff = function +type side_effects = side_effect list + +let rec uniq_seff_aux = function | [] -> [] - | x :: xs -> x :: uniq_seff (List.filter (fun y -> not (equal_eff x y)) xs) + | x :: xs -> x :: uniq_seff_aux (List.filter (fun y -> not (equal_eff x y)) xs) (* The list of side effects is in reverse order (most recent first). * To keep the "topological" order between effects we have to uniq-ize from * the tail *) -let uniq_seff l = List.rev (uniq_seff (List.rev l)) +let uniq_seff_rev l = List.rev (uniq_seff_aux (List.rev l)) +let uniq_seff l = List.rev (uniq_seff_aux l) + +let empty_seff = [] +let add_seff x xs = if List.mem_f equal_eff x xs then xs else x :: xs +let concat_seff xs ys = List.fold_right add_seff xs ys let inline_side_effects env body ctx side_eff = let handle_sideff (t,ctx,sl) { eff = se; from_env = mb } = @@ -97,7 +104,7 @@ let inline_side_effects env body ctx side_eff = t, ctx, (mb,List.length cbl) :: sl in (* CAVEAT: we assure a proper order *) - List.fold_left handle_sideff (body,ctx,[]) (uniq_seff side_eff) + List.fold_left handle_sideff (body,ctx,[]) (uniq_seff_rev side_eff) (* Given the list of signatures of side effects, checks if they match. * I.e. if they are ordered descendants of the current revstruct *) @@ -427,7 +434,7 @@ let export_side_effects mb env ce = let cbl = List.filter not_exists cbl in if cbl = [] then acc, sl else cbl :: acc, (mb,List.length cbl) :: sl in - let seff, signatures = List.fold_left aux ([],[]) (uniq_seff eff) in + let seff, signatures = List.fold_left aux ([],[]) (uniq_seff_rev eff) in let trusted = check_signatures mb signatures in let push_seff env = function | kn, cb, `Nothing, _ -> diff --git a/kernel/term_typing.mli b/kernel/term_typing.mli index 89b5fc40e..5330fb32b 100644 --- a/kernel/term_typing.mli +++ b/kernel/term_typing.mli @@ -12,6 +12,8 @@ open Environ open Declarations open Entries +type side_effects + val translate_local_def : structure_body -> env -> Id.t -> side_effects definition_entry -> constant_def * types * constant_universes @@ -29,7 +31,10 @@ val inline_entry_side_effects : {!Entries.const_entry_body} field. It is meant to get a term out of a not yet type checked proof. *) -val uniq_seff : side_effects -> side_effects +val empty_seff : side_effects +val add_seff : side_effect -> side_effects -> side_effects +val concat_seff : side_effects -> side_effects -> side_effects +val uniq_seff : side_effects -> side_effect list val equal_eff : side_effect -> side_effect -> bool val translate_constant : -- cgit v1.2.3 From ee1546dc6686e888cc8da5f9442bcf788544dd0e Mon Sep 17 00:00:00 2001 From: Pierre-Marie Pédrot Date: Sun, 12 Mar 2017 20:16:43 +0100 Subject: Using a dedicated datastructure for side effect ordering. We were doing fishy things in the Term_typing file, where side-effects were not considered in the right uniquization order because of the uniq_seff_rev function. It probably did not matter after a9b76df because effects were (mostly) uniquize upfront, but this is not clear because of the use of the transparente API in the module. Now everything has to go through the opaque API, so that a proper dependence order is ensured. --- kernel/term_typing.ml | 66 ++++++++++++++++++++++++++++++++++++++------------- 1 file changed, 49 insertions(+), 17 deletions(-) diff --git a/kernel/term_typing.ml b/kernel/term_typing.ml index 24da308b4..6ce14c853 100644 --- a/kernel/term_typing.ml +++ b/kernel/term_typing.ml @@ -24,8 +24,6 @@ open Fast_typeops (* Insertion of constants and parameters in environment. *) -let mk_pure_proof c = (c, Univ.ContextSet.empty), [] - let equal_eff e1 e2 = let open Entries in match e1, e2 with @@ -37,20 +35,54 @@ let equal_eff e1 e2 = cl1 cl2 | _ -> false -type side_effects = side_effect list +module SideEffects : +sig + type t + val repr : t -> side_effect list + val empty : t + val add : side_effect -> t -> t + val concat : t -> t -> t +end = +struct + +let compare_seff e1 e2 = match e1, e2 with +| SEsubproof (c1, _, _), SEsubproof (c2, _, _) -> Constant.CanOrd.compare c1 c2 +| SEscheme (cl1, _), SEscheme (cl2, _) -> + let cmp (_, c1, _, _) (_, c2, _, _) = Constant.CanOrd.compare c1 c2 in + CList.compare cmp cl1 cl2 +| SEsubproof _, SEscheme _ -> -1 +| SEscheme _, SEsubproof _ -> 1 + +module SeffOrd = struct +type t = side_effect +let compare e1 e2 = compare_seff e1.eff e2.eff +end + +module SeffSet = Set.Make(SeffOrd) + +type t = { seff : side_effect list; elts : SeffSet.t } +(** Invariant: [seff] is a permutation of the elements of [elts] *) + +let repr eff = eff.seff +let empty = { seff = []; elts = SeffSet.empty } +let add x es = + if SeffSet.mem x es.elts then es + else { seff = x :: es.seff; elts = SeffSet.add x es.elts } +let concat xes yes = + List.fold_right add xes.seff yes + +end + +type side_effects = SideEffects.t + +let uniq_seff_rev = SideEffects.repr +let uniq_seff l = List.rev (SideEffects.repr l) -let rec uniq_seff_aux = function - | [] -> [] - | x :: xs -> x :: uniq_seff_aux (List.filter (fun y -> not (equal_eff x y)) xs) -(* The list of side effects is in reverse order (most recent first). - * To keep the "topological" order between effects we have to uniq-ize from - * the tail *) -let uniq_seff_rev l = List.rev (uniq_seff_aux (List.rev l)) -let uniq_seff l = List.rev (uniq_seff_aux l) +let empty_seff = SideEffects.empty +let add_seff = SideEffects.add +let concat_seff = SideEffects.concat -let empty_seff = [] -let add_seff x xs = if List.mem_f equal_eff x xs then xs else x :: xs -let concat_seff xs ys = List.fold_right add_seff xs ys +let mk_pure_proof c = (c, Univ.ContextSet.empty), empty_seff let inline_side_effects env body ctx side_eff = let handle_sideff (t,ctx,sl) { eff = se; from_env = mb } = @@ -388,7 +420,7 @@ let constant_entry_of_side_effect cb u = | Def b, `Nothing -> Mod_subst.force_constr b, Univ.ContextSet.empty | _ -> assert false in DefinitionEntry { - const_entry_body = Future.from_val (pt, []); + const_entry_body = Future.from_val (pt, empty_seff); const_entry_secctx = None; const_entry_feedback = None; const_entry_type = @@ -422,7 +454,7 @@ let export_side_effects mb env ce = let _, eff = Future.force body in let ce = DefinitionEntry { c with const_entry_body = Future.chain ~greedy:true ~pure:true body - (fun (b_ctx, _) -> b_ctx, []) } in + (fun (b_ctx, _) -> b_ctx, empty_seff) } in let not_exists (c,_,_,_) = try ignore(Environ.lookup_constant c env); false with Not_found -> true in @@ -507,7 +539,7 @@ let inline_entry_side_effects env ce = { ce with const_entry_body = Future.chain ~greedy:true ~pure:true ce.const_entry_body (fun ((body, ctx), side_eff) -> let body, ctx',_ = inline_side_effects env body ctx side_eff in - (body, ctx'), []); + (body, ctx'), empty_seff); } let inline_side_effects env body side_eff = -- cgit v1.2.3 From 91dbe4af7b2a435142dcf40902082f90f07cc8be Mon Sep 17 00:00:00 2001 From: Pierre-Marie Pédrot Date: Mon, 20 Mar 2017 08:48:22 +0100 Subject: Documenting the API of side-effects. --- kernel/safe_typing.mli | 7 +++++++ kernel/term_typing.mli | 5 +++++ 2 files changed, 12 insertions(+) diff --git a/kernel/safe_typing.mli b/kernel/safe_typing.mli index 8bc47d6ce..efeb98bd2 100644 --- a/kernel/safe_typing.mli +++ b/kernel/safe_typing.mli @@ -48,10 +48,17 @@ type private_constant_role = val side_effects_of_private_constants : private_constants -> Entries.side_effect list +(** Return the list of individual side-effects in the order of their + creation. *) val empty_private_constants : private_constants val add_private : private_constant -> private_constants -> private_constants +(** Add a constant to a list of private constants. The former must be more + recent than all constants appearing in the latter, i.e. one should not + create a dependency cycle. *) val concat_private : private_constants -> private_constants -> private_constants +(** [concat_private e1 e2] adds the constants of [e1] to [e2], i.e. constants in + [e1] must be more recent than those of [e2]. *) val private_con_of_con : safe_environment -> constant -> private_constant val private_con_of_scheme : kind:string -> safe_environment -> (inductive * constant) list -> private_constant diff --git a/kernel/term_typing.mli b/kernel/term_typing.mli index 5330fb32b..075389ea5 100644 --- a/kernel/term_typing.mli +++ b/kernel/term_typing.mli @@ -34,7 +34,12 @@ val inline_entry_side_effects : val empty_seff : side_effects val add_seff : side_effect -> side_effects -> side_effects val concat_seff : side_effects -> side_effects -> side_effects +(** [concat_seff e1 e2] adds the side-effects of [e1] to [e2], i.e. effects in + [e1] must be more recent than those of [e2]. *) val uniq_seff : side_effects -> side_effect list +(** Return the list of individual side-effects in the order of their + creation. *) + val equal_eff : side_effect -> side_effect -> bool val translate_constant : -- cgit v1.2.3