X-Git-Url: http://matita.cs.unibo.it/gitweb/?p=helm.git;a=blobdiff_plain;f=helm%2FDEVEL%2Fpxp%2Fnetstring%2Fnetbuffer.ml;fp=helm%2FDEVEL%2Fpxp%2Fnetstring%2Fnetbuffer.ml;h=0000000000000000000000000000000000000000;hp=d6fc40ff77920131b27648a3bd9148e802f975ed;hb=3ef089a4c58fbe429dd539af6215991ecbe11ee2;hpb=1c7fb836e2af4f2f3d18afd0396701f2094265ff

diff --git a/helm/DEVEL/pxp/netstring/netbuffer.ml b/helm/DEVEL/pxp/netstring/netbuffer.ml
deleted file mode 100644
index d6fc40ff7..000000000
--- a/helm/DEVEL/pxp/netstring/netbuffer.ml
+++ /dev/null
@@ -1,145 +0,0 @@
-(* $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.
- *
- * 
- *)