From ae3238eabe38a32688127fe851244343c9f33f8d Mon Sep 17 00:00:00 2001 From: Humza Shahid Date: Thu, 13 Feb 2025 08:26:48 +0000 Subject: [PATCH] minor adjustments to gap_vector.sml to make functor fit GAP_VECTOR signature --- src/gap_vector.sml | 11 ++++++++--- 1 file changed, 8 insertions(+), 3 deletions(-) diff --git a/src/gap_vector.sml b/src/gap_vector.sml index f093d2a..16fdc2e 100644 --- a/src/gap_vector.sml +++ b/src/gap_vector.sml @@ -21,8 +21,10 @@ sig val deleteMany: int * int * t -> t end -functor MakeGapVector(Fn: GAP_VECTOR_INPUT) = +functor MakeGapVector(Fn: GAP_VECTOR_INPUT): GAP_VECTOR = struct + structure Fn = Fn + type t = {idx: int, left: Fn.elem vector list, right: Fn.elem vector list} val empty = {idx = 0, left = [], right = []} @@ -280,9 +282,12 @@ struct insRight (nextIdx, idx, newVector, curIdx, left, hd, tail) end - fun insert (idx, newVector, buffer: t) = + fun insertMany (idx, newVector, buffer: t) = ins (idx, newVector, #idx buffer, #left buffer, #right buffer) + fun insert (idx, elem, buffer) = + insertMany (idx, Vector.fromList [elem], buffer) + fun deleteRightFromHere (curIdx, finish, right) = case right of hd :: tail => @@ -497,7 +502,7 @@ struct , right = deleteRightFromHere (curIdx, finish, right) } - fun delete (start, length, buffer: t) = + fun deleteMany (start, length, buffer: t) = if length > 0 then del (start, start + length, #idx buffer, #left buffer, #right buffer) else