]> matita.cs.unibo.it Git - helm.git/blobdiff - helm/DEVEL/pxp/netstring/netbuffer.ml
Initial revision
[helm.git] / helm / DEVEL / pxp / netstring / netbuffer.ml
diff --git a/helm/DEVEL/pxp/netstring/netbuffer.ml b/helm/DEVEL/pxp/netstring/netbuffer.ml
new file mode 100644 (file)
index 0000000..d6fc40f
--- /dev/null
@@ -0,0 +1,145 @@
+(* $Id$
+ * ----------------------------------------------------------------------
+ *
+ *)
+
+type t = 
+    { mutable buffer : string;
+      mutable length : int;
+    }
+
+(* To help the garbage collector:
+ * The 'buffer' has a minimum length of 31 bytes. This minimum can still
+ * be stored in the minor heap.
+ * The 'buffer' has a length which is always near a multiple of two. This
+ * limits the number of different bucket sizes, and simplifies reallocation
+ * of freed memory.
+ *)
+
+(* Optimal string length:
+ * Every string takes: 1 word for the header, enough words for the 
+ * contents + 1 Null byte (for C compatibility).
+ * If the buffer grows, it is best to use a new string length such
+ * that the number of words is exactly twice as large as for the previous
+ * string.
+ * n:              length of the previous string in bytes
+ * w:              storage size of the previous string in words
+ * n':             length of the new string in bytes
+ * w' = 2*w:       storage size of the new string in words
+ *
+ * w = (n+1) / word_length + 1
+ *            [it is assumed that (n+1) is always a multiple of word_length]
+ *
+ * n' = (2*w - 1) * word_length - 1
+ *
+ * n' = [2 * ( [n+1] / word_length + 1) - 1] * word_length - 1
+ *    = ...
+ *    = (2*n + 2) + word_length - 1
+ *    = 2 * n + word_length + 1
+ *
+ * n'+1 is again a multiple of word_length:
+ * n'+1 = 2*n + 2 + word_length
+ *      = 2*(n+1) + word_length
+ *      = a multiple of word_length because n+1 is a multiple of word_length
+ *)
+
+let word_length = Sys.word_size / 8       (* in bytes *)
+
+let create n =
+  { buffer = String.create (max n 31); length = 0; }
+
+let contents b =
+  String.sub b.buffer 0 b.length
+    
+let sub b ~pos:k ~len:n =
+  if k+n > b.length then
+    raise (Invalid_argument "Netbuffer.sub");
+  String.sub b.buffer k n
+    
+let unsafe_buffer b =
+  b.buffer
+
+let length b =
+  b.length
+
+let add_string b s =
+  let l = String.length s in
+  if l + b.length > String.length b.buffer then begin
+    let l' = l + b.length in
+    let rec new_size s =
+      if s >= l' then s else new_size(2*s + word_length + 1)
+    in
+    let buffer' = String.create (new_size (String.length b.buffer)) in
+    String.blit b.buffer 0 buffer' 0 b.length;
+    b.buffer <- buffer'
+  end;
+  String.blit s 0 b.buffer b.length l;
+  b.length <- b.length + l
+    
+let add_sub_string b s ~pos:k ~len:l =
+  if l + b.length > String.length b.buffer then begin
+    let l' = l + b.length in
+    let rec new_size s =
+      if s >= l' then s else new_size(2*s + word_length + 1)
+    in
+    let buffer' = String.create (new_size (String.length b.buffer)) in
+    String.blit b.buffer 0 buffer' 0 b.length;
+    b.buffer <- buffer'
+  end;
+  String.blit s k b.buffer b.length l;
+  b.length <- b.length + l
+    
+let delete b ~pos:k ~len:l =
+  (* deletes l bytes at position k in b *)
+  let n = String.length b.buffer in
+  if k+l <> n & k <> n then
+    String.blit b.buffer (k+l) b.buffer k (n-l-k);
+  b.length <- b.length - l;
+  ()
+
+let try_shrinking b =
+  (* If the buffer size decreases drastically, reallocate the buffer *)
+  if b.length < (String.length b.buffer / 2) then begin
+    let rec new_size s =
+      if s >= b.length then s else new_size(2*s + word_length + 1)
+    in
+    let buffer' = String.create (new_size 31) in
+    String.blit b.buffer 0 buffer' 0 b.length;
+    b.buffer <- buffer'
+  end 
+
+let clear b =
+  delete b 0 (b.length)
+  
+let index_from b k c =
+  if k > b.length then
+    raise (Invalid_argument "Netbuffer.index_from");
+  let p = String.index_from b.buffer k c in
+  if p >= b.length then raise Not_found;
+  p
+
+let print_buffer b =
+  Format.printf
+    "<NETBUFFER: %d/%d>"
+    b.length
+    (String.length b.buffer)
+;;
+
+(* ======================================================================
+ * History:
+ * 
+ * $Log$
+ * Revision 1.1  2000/11/17 09:57:27  lpadovan
+ * Initial revision
+ *
+ * Revision 1.3  2000/06/25 22:34:43  gerd
+ *     Added labels to arguments.
+ *
+ * Revision 1.2  2000/06/24 20:20:33  gerd
+ *     Added the toploop printer.
+ *
+ * Revision 1.1  2000/04/15 13:07:48  gerd
+ *     Initial revision.
+ *
+ * 
+ *)