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/term_typing.ml | 17 ++++++++++++----- 1 file changed, 12 insertions(+), 5 deletions(-) (limited to 'kernel/term_typing.ml') 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, _ -> -- 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(-) (limited to 'kernel/term_typing.ml') 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