From ce31491c3d7109f8e9756d7e06a70a14b2fe4370 Mon Sep 17 00:00:00 2001 From: Vesa Karvonen Date: Wed, 24 Jan 2024 18:00:50 +0200 Subject: [PATCH] Use GADT to avoid a bit of code duplication --- src/kcas/kcas.ml | 47 +++++++++++++++++++++++------------------------ 1 file changed, 23 insertions(+), 24 deletions(-) diff --git a/src/kcas/kcas.ml b/src/kcas/kcas.ml index 32f7b7a8..799e12cc 100644 --- a/src/kcas/kcas.ml +++ b/src/kcas/kcas.ml @@ -772,40 +772,39 @@ module Xt = struct let post_commit ~xt:(Xt xt_r : _ t) action = xt_r.post_commit <- Action.append action xt_r.post_commit - let validate ~xt loc = - let loc = Loc.to_loc loc in - let x = loc.id in - match !(tree_as_ref xt) with - | T Leaf -> () - | T (Node { loc = a; lt = T Leaf; _ }) when x < a.id -> () - | T (Node { loc = a; gt = T Leaf; _ }) when a.id < x -> () - | T (Node { loc = a; state; _ }) when Obj.magic a == loc -> - validate_one xt a state - | tree -> begin - match splay ~hit_parent:true x tree with - | lt, T (Node node_r), gt -> - tree_as_ref xt := T (Node { node_r with lt; gt; awaiters = [] }); - if Obj.magic node_r.loc == loc then - validate_one xt node_r.loc node_r.state - | _, T Leaf, _ -> impossible () - end + type _ op = Validate : unit op | Is_in_log : bool op - let is_in_log ~xt loc = + let do_op : type r. xt:'x t -> 'a Loc.t -> r op -> r = + fun ~xt loc op -> let loc = Loc.to_loc loc in let x = loc.id in match !(tree_as_ref xt) with - | T Leaf -> false - | T (Node { loc = a; lt = T Leaf; _ }) when x < a.id -> false - | T (Node { loc = a; gt = T Leaf; _ }) when a.id < x -> false - | T (Node { loc = a; _ }) when Obj.magic a == loc -> true + | T Leaf -> begin match op with Validate -> () | Is_in_log -> false end + | T (Node { loc = a; lt = T Leaf; _ }) when x < a.id -> begin + match op with Validate -> () | Is_in_log -> false + end + | T (Node { loc = a; gt = T Leaf; _ }) when a.id < x -> begin + match op with Validate -> () | Is_in_log -> false + end + | T (Node { loc = a; state; _ }) when Obj.magic a == loc -> begin + match op with Validate -> validate_one xt a state | Is_in_log -> true + end | tree -> begin match splay ~hit_parent:true x tree with - | lt, T (Node node_r), gt -> + | lt, T (Node node_r), gt -> begin tree_as_ref xt := T (Node { node_r with lt; gt; awaiters = [] }); - Obj.magic node_r.loc == loc + match op with + | Validate -> + if Obj.magic node_r.loc == loc then + validate_one xt node_r.loc node_r.state + | Is_in_log -> Obj.magic node_r.loc == loc + end | _, T Leaf, _ -> impossible () end + let[@inline] validate ~xt loc = do_op ~xt loc Validate + let[@inline] is_in_log ~xt loc = do_op ~xt loc Is_in_log + let rec rollback which tree_snap tree = if tree_snap == tree then tree else