From 5c45ef7ec49481960fc3eb44aa6f41ab37aa0027 Mon Sep 17 00:00:00 2001 From: Vesa Karvonen Date: Sat, 6 Jan 2024 20:02:21 +0200 Subject: [PATCH] Use a tagged GADT in `Dllist` --- src/kcas_data/dllist.ml | 275 +++++++++++++++++++++------------------- 1 file changed, 148 insertions(+), 127 deletions(-) diff --git a/src/kcas_data/dllist.ml b/src/kcas_data/dllist.ml index 9bf0b10a..b3eda822 100644 --- a/src/kcas_data/dllist.ml +++ b/src/kcas_data/dllist.ml @@ -1,190 +1,210 @@ open Kcas -type 'a t = { - lhs : 'a t Loc.t; - (** [lhs] points to the rightmost node of a list or the list itself. *) - rhs : 'a t Loc.t; - (** [rhs] points to the leftmost node of a list or the list itself. *) -} - -type 'a node = { - node_lhs : 'a t Loc.t; - (** [node_lhs] or [lhs] points to the node on the left side of this node - or to the list if this node is the leftmost node. *) - node_rhs : 'a t Loc.t; - (** [node_rhs] or [rhs] points to the node on the right side of this node - or to the list if this node is the rightmost node. *) - value : 'a; -} - -external as_list : 'a node -> 'a t = "%identity" -external as_node : 'a t -> 'a node = "%identity" - -let[@inline] get { value; _ } = value +(** Tagged GADT for representing doubly-linked lists. *) +type ('a, _) tdt = + | List : { + lhs : 'a cursor Loc.t; + (** [lhs] points to the rightmost node of a list or the list + itself. *) + rhs : 'a cursor Loc.t; + (** [rhs] points to the leftmost node of a list or the list itself. *) + } + -> ('a, [> `List ]) tdt + | Node : { + lhs : 'a cursor Loc.t; + (** [lhs] points to the node on the left side of this node or to the + list if this node is the leftmost node. *) + rhs : 'a cursor Loc.t; + (** [rhs] points to the node on the right side of this node or to the + list if this node is the rightmost node. *) + value : 'a; + } + -> ('a, [> `Node ]) tdt + +and 'a cursor = At : ('a, [< `List | `Node ]) tdt -> 'a cursor [@@unboxed] + +type 'a t = ('a, [ `List ]) tdt +type 'a node = ('a, [ `Node ]) tdt + +external as_list : ('a, _) tdt -> 'a t = "%identity" +external as_node : ('a, _) tdt -> 'a node = "%identity" + +let[@inline] get (Node { value; _ } : 'a node) = value + +let[@inline] lhs_of list_or_node = + let (List list_r) = as_list list_or_node in + list_r.lhs + +let[@inline] rhs_of list_or_node = + let (List list_r) = as_list list_or_node in + list_r.rhs + +let[@inline] value_of (Node node_r : 'a node) = node_r.value let create () = - let lhs = Loc.make ~padded:true (Obj.magic ()) - and rhs = Loc.make ~padded:true (Obj.magic ()) in - let list = Multicore_magic.copy_as_padded { lhs; rhs } in - Loc.set lhs list; - Loc.set rhs list; + let lhs = Loc.make ~padded:true (Obj.magic ()) in + let rhs = Loc.make ~padded:true (Obj.magic ()) in + let list = Multicore_magic.copy_as_padded (List { lhs; rhs }) in + Loc.set lhs (At list); + Loc.set rhs (At list); list let create_node value = let node = - let node_lhs = Loc.make (Obj.magic ()) - and node_rhs = Loc.make (Obj.magic ()) in - { node_lhs; node_rhs; value } + let lhs = Loc.make (Obj.magic ()) in + let rhs = Loc.make (Obj.magic ()) in + Node { lhs; rhs; value } in - Loc.set node.node_lhs (as_list node); - Loc.set node.node_rhs (as_list node); + Loc.set (lhs_of node) (At node); + Loc.set (rhs_of node) (At node); node let create_node_with ~lhs ~rhs value = - { node_lhs = Loc.make lhs; node_rhs = Loc.make rhs; value } + Node { lhs = Loc.make (At lhs); rhs = Loc.make (At rhs); value } module Xt = struct let remove ~xt node = - let list = as_list node in - let rhs = Xt.exchange ~xt list.rhs list in - if rhs != list then begin - let lhs = Xt.exchange ~xt list.lhs list in - Xt.set ~xt rhs.lhs lhs; - Xt.set ~xt lhs.rhs rhs + let (At rhs) = Xt.exchange ~xt (rhs_of node) (At node) in + if At rhs != At node then begin + let (At lhs) = Xt.exchange ~xt (lhs_of node) (At node) in + Xt.set ~xt (lhs_of rhs) (At lhs); + Xt.set ~xt (rhs_of lhs) (At rhs) end - let is_empty ~xt list = Xt.get ~xt list.lhs == list + let is_empty ~xt list = Xt.get ~xt (lhs_of list) == At list let add_node_l ~xt node list = - let rhs = Xt.get ~xt list.rhs in - assert (Loc.fenceless_get node.node_lhs == list); - Loc.set node.node_rhs rhs; - Xt.set ~xt list.rhs (as_list node); - Xt.set ~xt rhs.lhs (as_list node); + let (At rhs) = Xt.get ~xt (rhs_of list) in + assert (Loc.fenceless_get (lhs_of node) == At list); + Loc.set (rhs_of node) (At rhs); + Xt.set ~xt (rhs_of list) (At node); + Xt.set ~xt (lhs_of rhs) (At node); node let add_l ~xt value list = - let rhs = Xt.get ~xt list.rhs in + let (At rhs) = Xt.get ~xt (rhs_of list) in let node = create_node_with ~lhs:list ~rhs value in - Xt.set ~xt list.rhs (as_list node); - Xt.set ~xt rhs.lhs (as_list node); + Xt.set ~xt (rhs_of list) (At node); + Xt.set ~xt (lhs_of rhs) (At node); node let add_node_r ~xt node list = - let lhs = Xt.get ~xt list.lhs in - Loc.set node.node_lhs lhs; - assert (Loc.fenceless_get node.node_rhs == list); - Xt.set ~xt list.lhs (as_list node); - Xt.set ~xt lhs.rhs (as_list node); + let (At lhs) = Xt.get ~xt (lhs_of list) in + Loc.set (lhs_of node) (At lhs); + assert (Loc.fenceless_get (rhs_of node) == At list); + Xt.set ~xt (lhs_of list) (At node); + Xt.set ~xt (rhs_of lhs) (At node); node let add_r ~xt value list = - let lhs = Xt.get ~xt list.lhs in + let (At lhs) = Xt.get ~xt (lhs_of list) in let node = create_node_with ~lhs ~rhs:list value in - Xt.set ~xt list.lhs (as_list node); - Xt.set ~xt lhs.rhs (as_list node); + Xt.set ~xt (lhs_of list) (At node); + Xt.set ~xt (rhs_of lhs) (At node); node let move_l ~xt node list = - let node = as_list node in - let list_rhs = Xt.exchange ~xt list.rhs node in - if list_rhs != node then begin - let node_lhs = Xt.exchange ~xt node.lhs list in - let node_rhs = Xt.exchange ~xt node.rhs list_rhs in - if node_lhs != node then begin - Xt.set ~xt node_lhs.rhs node_rhs; - Xt.set ~xt node_rhs.lhs node_lhs + let (At list_rhs) = Xt.exchange ~xt (rhs_of list) (At node) in + if At list_rhs != At node then begin + let (At node_lhs) = Xt.exchange ~xt (lhs_of node) (At list) in + let (At node_rhs) = Xt.exchange ~xt (rhs_of node) (At list_rhs) in + if At node_lhs != At node then begin + Xt.set ~xt (rhs_of node_lhs) (At node_rhs); + Xt.set ~xt (lhs_of node_rhs) (At node_lhs) end; - Xt.set ~xt list_rhs.lhs node + Xt.set ~xt (lhs_of list_rhs) (At node) end let move_r ~xt node list = - let node = as_list node in - let list_lhs = Xt.exchange ~xt list.lhs node in - if list_lhs != node then begin - let node_rhs = Xt.exchange ~xt node.rhs list in - let node_lhs = Xt.exchange ~xt node.lhs list_lhs in - if node_rhs != node then begin - Xt.set ~xt node_lhs.rhs node_rhs; - Xt.set ~xt node_rhs.lhs node_lhs + let (At list_lhs) = Xt.exchange ~xt (lhs_of list) (At node) in + if At list_lhs != At node then begin + let (At node_rhs) = Xt.exchange ~xt (rhs_of node) (At list) in + let (At node_lhs) = Xt.exchange ~xt (lhs_of node) (At list_lhs) in + if At node_rhs != At node then begin + Xt.set ~xt (rhs_of node_lhs) (At node_rhs); + Xt.set ~xt (lhs_of node_rhs) (At node_lhs) end; - Xt.set ~xt list_lhs.rhs node + Xt.set ~xt (rhs_of list_lhs) (At node) end let take_opt_l ~xt list = - let rhs = Xt.get ~xt list.rhs in - if rhs == list then None + let (At rhs) = Xt.get ~xt (rhs_of list) in + if At rhs == At list then None else let node = as_node rhs in remove ~xt node; - Some node.value + Some (value_of node) let take_opt_r ~xt list = - let lhs = Xt.get ~xt list.lhs in - if lhs == list then None + let (At lhs) = Xt.get ~xt (lhs_of list) in + if At lhs == At list then None else let node = as_node lhs in remove ~xt node; - Some node.value + Some (value_of node) let take_blocking_l ~xt list = Xt.to_blocking ~xt (take_opt_l list) let take_blocking_r ~xt list = Xt.to_blocking ~xt (take_opt_r list) let transfer_l ~xt t1 t2 = - let t1_rhs = Xt.exchange ~xt t1.rhs t1 in - if t1_rhs != t1 then begin - let t1_lhs = Xt.exchange ~xt t1.lhs t1 in - let t2_rhs = Xt.exchange ~xt t2.rhs t1_rhs in - Xt.set ~xt t2_rhs.lhs t1_lhs; - Xt.set ~xt t1_rhs.lhs t2; - Xt.set ~xt t1_lhs.rhs t2_rhs + let (At t1_rhs) = Xt.exchange ~xt (rhs_of t1) (At t1) in + if At t1_rhs != At t1 then begin + let (At t1_lhs) = Xt.exchange ~xt (lhs_of t1) (At t1) in + let (At t2_rhs) = Xt.exchange ~xt (rhs_of t2) (At t1_rhs) in + Xt.set ~xt (lhs_of t2_rhs) (At t1_lhs); + Xt.set ~xt (lhs_of t1_rhs) (At t2); + Xt.set ~xt (rhs_of t1_lhs) (At t2_rhs) end let transfer_r ~xt t1 t2 = - let t1_rhs = Xt.exchange ~xt t1.rhs t1 in - if t1_rhs != t1 then begin - let t1_lhs = Xt.exchange ~xt t1.lhs t1 in - let t2_lhs = Xt.exchange ~xt t2.lhs t1_lhs in - Xt.set ~xt t2_lhs.rhs t1_rhs; - Xt.set ~xt t1_lhs.rhs t2; - Xt.set ~xt t1_rhs.lhs t2_lhs + let (At t1_rhs) = Xt.exchange ~xt (rhs_of t1) (At t1) in + if At t1_rhs != At t1 then begin + let (At t1_lhs) = Xt.exchange ~xt (lhs_of t1) (At t1) in + let (At t2_lhs) = Xt.exchange ~xt (lhs_of t2) (At t1_lhs) in + Xt.set ~xt (rhs_of t2_lhs) (At t1_rhs); + Xt.set ~xt (rhs_of t1_lhs) (At t2); + Xt.set ~xt (lhs_of t1_rhs) (At t2_lhs) end let swap ~xt t1 t2 = - let t1_rhs = Xt.get ~xt t1.rhs in - if t1_rhs == t1 then transfer_l ~xt t2 t1 + let (At t1_rhs) = Xt.get ~xt (rhs_of t1) in + if At t1_rhs == At t1 then transfer_l ~xt t2 t1 else - let t2_lhs = Xt.get ~xt t2.lhs in - if t2_lhs == t2 then transfer_l ~xt t1 t2 + let (At t2_lhs) = Xt.get ~xt (lhs_of t2) in + if At t2_lhs == At t2 then transfer_l ~xt t1 t2 else - let t1_lhs = Xt.exchange ~xt t1.lhs t2_lhs - and t2_rhs = Xt.exchange ~xt t2.rhs t1_rhs in - Xt.set ~xt t2.lhs t1_lhs; - Xt.set ~xt t1.rhs t2_rhs; - Xt.set ~xt t2_rhs.lhs t1; - Xt.set ~xt t2_lhs.rhs t1; - Xt.set ~xt t1_rhs.lhs t2; - Xt.set ~xt t1_lhs.rhs t2 - - let[@tail_mod_cons] rec to_list_as_l ~xt f list node = - if node == list then [] - else f (as_node node) :: to_list_as_l ~xt f list (Xt.get ~xt node.rhs) - - let to_list_as_l ~xt f list = to_list_as_l ~xt f list (Xt.get ~xt list.rhs) + let (At t1_lhs) = Xt.exchange ~xt (lhs_of t1) (At t2_lhs) in + let (At t2_rhs) = Xt.exchange ~xt (rhs_of t2) (At t1_rhs) in + Xt.set ~xt (lhs_of t2) (At t1_lhs); + Xt.set ~xt (rhs_of t1) (At t2_rhs); + Xt.set ~xt (lhs_of t2_rhs) (At t1); + Xt.set ~xt (rhs_of t2_lhs) (At t1); + Xt.set ~xt (lhs_of t1_rhs) (At t2); + Xt.set ~xt (rhs_of t1_lhs) (At t2) + + let[@tail_mod_cons] rec to_list_as_l ~xt f list (At at) = + if At at == At list then [] + else f (as_node at) :: to_list_as_l ~xt f list (Xt.get ~xt (rhs_of at)) + + let to_list_as_l ~xt f list = + to_list_as_l ~xt f list (Xt.get ~xt (rhs_of list)) + let to_list_l ~xt list = to_list_as_l ~xt get list let to_nodes_l ~xt list = to_list_as_l ~xt Fun.id list - let[@tail_mod_cons] rec to_list_as_r ~xt f list node = - if node == list then [] - else f (as_node node) :: to_list_as_r ~xt f list (Xt.get ~xt node.lhs) + let[@tail_mod_cons] rec to_list_as_r ~xt f list (At at) = + if At at == At list then [] + else f (as_node at) :: to_list_as_r ~xt f list (Xt.get ~xt (lhs_of at)) + + let to_list_as_r ~xt f list = + to_list_as_r ~xt f list (Xt.get ~xt (lhs_of list)) - let to_list_as_r ~xt f list = to_list_as_r ~xt f list (Xt.get ~xt list.lhs) let to_list_r ~xt list = to_list_as_r ~xt get list let to_nodes_r ~xt list = to_list_as_r ~xt Fun.id list end let remove node = Kcas.Xt.commit { tx = Xt.remove node } -let is_empty list = Loc.get list.lhs == list +let is_empty list = Loc.get (lhs_of list) == At list let add_l value list = let node = create_node_with ~lhs:list ~rhs:list value in @@ -220,22 +240,23 @@ let take_r list = match take_opt_r list with None -> raise Empty | Some v -> v let take_all list = let copy = - Multicore_magic.copy_as_padded - { lhs = Loc.make ~padded:true list; rhs = Loc.make ~padded:true list } + let lhs = Loc.make ~padded:true (At list) in + let rhs = Loc.make ~padded:true (At list) in + List { lhs; rhs } |> Multicore_magic.copy_as_padded in let open Kcas in let tx ~xt = - let lhs = Xt.exchange ~xt list.lhs list in - if lhs == list then begin - Loc.set copy.lhs copy; - Loc.set copy.rhs copy + let (At lhs) = Xt.exchange ~xt (lhs_of list) (At list) in + if At lhs == At list then begin + Loc.set (lhs_of copy) (At copy); + Loc.set (rhs_of copy) (At copy) end else - let rhs = Xt.exchange ~xt list.rhs list in - Xt.set ~xt lhs.rhs copy; - Xt.set ~xt rhs.lhs copy; - Loc.set copy.lhs lhs; - Loc.set copy.rhs rhs + let (At rhs) = Xt.exchange ~xt (rhs_of list) (At list) in + Xt.set ~xt (rhs_of lhs) (At copy); + Xt.set ~xt (lhs_of rhs) (At copy); + Loc.set (lhs_of copy) (At lhs); + Loc.set (rhs_of copy) (At rhs) in Xt.commit { tx }; copy