Commits

Sébastien Ferré  committed ab36342

Git

  • Participants
  • Parent commits 8a39944

Comments (0)

Files changed (3)

File persintset.ml

 
 open Persindex
 
-module Make (Intset2 : Intset.T) =
+module type PARAM =
+  sig
+    val chunk : int
+  end
+
+module DefaultParam : PARAM =
   struct
     let chunk = 1024
+  end
 
+module Make (Param : PARAM) (Intset2 : Intset.T) =
+  struct
     let lazy_val = Lazy.lazy_from_val
     let force = Lazy.force
 
       struct
 	type t = (int * Intset2.t Lazy.t) list
 	      (* sorted in decreasing order of first part *)
-	      (* the second part contains only integers x, s.t. x/chunk = first part *)
+	      (* the second part contains only integers x mod Param.chunk, s.t. x/Param.chunk = first part *)
 	      (* trying to avoid empty intsets as second part *)
 	      
 	let empty = []
 	    0 e
 
 	let mem x =
-	  let x1 = x / chunk in
+	  let x1, x2 = x / Param.chunk, x mod Param.chunk in
 	  let rec aux = function
 	    | [] -> false
 	    | (p,e2)::l ->
 		if x1 < p then aux l
-		else if x1 = p then Intset2.mem x (force e2)
+		else if x1 = p then Intset2.mem x2 (force e2)
 		else (* x1 > p *) false
 	  in
 	  aux
 
 	let singleton x =
-	  let e2 = Intset2.singleton x in
-	  [(x / chunk, lazy_val e2)]
+	  let e2 = Intset2.singleton (x mod Param.chunk) in
+	  [(x / Param.chunk, lazy_val e2)]
 
 	let add x =
-	  let x1 = x / chunk in
+	  let x1, x2 = x / Param.chunk, x mod Param.chunk in
 	  let rec aux pe =
 	    match pe with
-	    | [] -> [(x1,lazy_val (Intset2.singleton x))]
+	    | [] -> [(x1,lazy_val (Intset2.singleton x2))]
 	    | (pos,e2 as pe2)::l ->
 		if x1 < pos then pe2 :: aux l
 		else if x1 = pos then
-		  (pos,lazy_val (Intset2.add x (force e2)))::l
+		  (pos,lazy_val (Intset2.add x2 (force e2)))::l
 		else (* x1 > pos *)
-		  (x1,lazy_val (Intset2.singleton x))::pe
+		  (x1,lazy_val (Intset2.singleton x2))::pe
 	  in
 	  aux
 	    
 	let remove x =
-	  let x1 = x / chunk in
+	  let x1, x2 = x / Param.chunk, x mod Param.chunk in
 	  let rec aux pe =
 	    match pe with
 	    | [] -> []
 		if x1 < pos then
 		  pe2 :: aux l
 		else if x1 = pos then
-		  let new_e2 = Intset2.remove x (force e2) in
+		  let new_e2 = Intset2.remove x2 (force e2) in
 		  if Intset2.is_empty new_e2
 		  then l
 		  else (pos,lazy_val (new_e2))::l
 
 	let rec fold f acc = function
 	  | [] -> acc
-	  | (pos,e2)::l ->
-	      fold f (Intset2.fold f acc (force e2)) l
+	  | (x1,e2)::l ->
+	      fold f (Intset2.fold (fun acc2 x2 -> f acc2 (x1*Param.chunk + x2)) acc (force e2)) l
 
 	let map f =
 	  let rec aux acc = function
 	    | [] -> acc
-	    | (pos,e2)::l ->
-		aux (Intset2.fold (fun res x -> f x::res) acc (force e2)) l
+	    | (x1,e2)::l ->
+		aux (Intset2.fold (fun res x2 -> f (x1*Param.chunk + x2) :: res) acc (force e2)) l
 	  in
 	  aux []
 
 	let rec iter f = function
 	  | [] -> ()
-	  | (pos,e2)::l ->
-	      Intset2.iter f (force e2);
+	  | (x1,e2)::l ->
+	      Intset2.iter (fun x2 -> f (x1*Param.chunk + x2)) (force e2);
 	      iter f l
 
 	let rec filter f = function
 	  | [] -> []
-	  | (pos,e2)::l ->
-	      let new_e2 = Intset2.filter f (force e2) in
+	  | (x1,e2)::l ->
+	      let new_e2 = Intset2.filter (fun x2 -> f (x1*Param.chunk + x2)) (force e2) in
 	      if Intset2.is_empty new_e2
 	      then filter f l
-	      else (pos,lazy_val new_e2)::filter f l
+	      else (x1,lazy_val new_e2)::filter f l
 
 	let rec elements = function
 	  | [] -> LSet.empty ()
-	  | (pos,e2)::l ->
-	      LSet.union (Intset2.elements (force e2)) (elements l)
+	  | (x1,e2)::l ->
+	      LSet.union (List.map (fun x2 -> x1*Param.chunk + x2) (Intset2.elements (force e2))) (elements l)
 
       end
 
     class c (name : string) (db : database) =
       object (self)
 	val genid = new Genid.genid (name ^ ".genid") db
-	val id2ext : (extid,Intset2.t) index = new varray_vector_opt 13 chunk (fun id -> Intset2.empty) db
+	val id2ext : (extid,Intset2.t) index = new varray_vector_opt 13 Param.chunk (fun id -> Intset2.empty) db
 
 	initializer
 	  id2ext # locate (name ^ "_extid") name "id2ext"
 
 	method mem : int -> t -> bool =
 	  fun x ->
-	    let x1 = x / chunk in
+	    let x1, x2 = x / Param.chunk, x mod Param.chunk in
 	    let rec aux = function
 	      | [] -> false
 	      | (p,id)::l ->
 		  if x1 < p then aux l
-		  else if x1 = p then Intset2.mem x (id2ext # get id)
+		  else if x1 = p then Intset2.mem x2 (id2ext # get id)
 		  else (* x1 > p *) false
 	    in
 	    aux
 
 	method add : int -> t -> t =
 	  fun x ->
-	    let x1 = x / chunk in
+	    let x1, x2 = x / Param.chunk, x mod Param.chunk in
 	    let rec aux pe =
 	      match pe with
 	      | [] ->
 		  let new_id = genid # alloc in
-		  id2ext # set new_id (Intset2.singleton x);
+		  id2ext # set new_id (Intset2.singleton x2);
 		  (x1,new_id)::[]
 	      | (p,id as pid)::l ->
 		  if x1 < p then
 		    pid::aux l
 		  else if x1 = p then begin 
-		    id2ext # update id (Intset2.add x);
+		    id2ext # update id (Intset2.add x2);
 		    pe end
 		  else (* x1 > p *) begin
 		    let new_id = genid # alloc in
-		    id2ext # set new_id (Intset2.singleton x);
+		    id2ext # set new_id (Intset2.singleton x2);
 		    (x1,new_id)::pe end
 	    in
 	    aux
 
 	method remove : int -> t -> t =
 	  fun x ->
-	    let x1 = x / chunk in
+	    let x1, x2 = x / Param.chunk, x mod Param.chunk in
 	    let rec aux pe =
 	      match pe with
 	      | [] -> []
 		  if x1 < p then
 		    pid::aux l
 		  else if x1 = p then
-		    let ext = Intset2.remove x (id2ext # get id) in
+		    let ext = Intset2.remove x2 (id2ext # get id) in
 		    if Intset2.is_empty ext
 		    then begin id2ext # reset id; genid # free id; l end
 		    else begin id2ext # set id ext; pe end
 
 type t_list = Tokens.t list
 
+type decimal = int * int (* fraction and exponent *)
+
 open Tokens
 
 (* forbidden idents in syntax of logics *)
 
 open Format
 
+(*
 let rec power10 : int -> float =
       function
       | 0 -> 1.
       | p -> if p > 0
              then power10 (p-1) *. 10.
              else power10 (p+1) /. 10.
+*)
 
 let string_escaped : string -> string =
   fun s ->
     let s = string_of_int n in
     list_of_stream (from_string s)
 
-let toks_of_float : (float * int) -> t_list =
+let float_of_decimal : decimal -> float =
+  fun (frac,expo) ->
+    float_of_string (string_of_int frac ^ "e" ^ string_of_int expo)
+
+let toks_of_decimal : decimal -> t_list =
+  fun (frac,expo) ->
+    let sign, abs_frac =
+      if frac < 0
+      then "-", -frac
+      else "", frac in
+    let s_abs_frac = string_of_int abs_frac in
+    let l = String.length s_abs_frac in
+    let s =
+      if expo > 0 then 
+	sign ^ s_abs_frac ^ ".e" ^ string_of_int expo
+      else if expo = 0 then
+	sign ^ s_abs_frac ^ "."
+      else if expo >= (-l + 1) && expo <= (-1) then
+	sign ^ String.sub s_abs_frac 0 (l - (-expo)) ^ "." ^ String.sub s_abs_frac (l - (-expo)) (-expo)
+      else if expo = -l then
+	sign ^ "0." ^ s_abs_frac
+      else if expo <= -l then
+	sign ^ "0." ^ s_abs_frac ^ "e" ^ string_of_int (expo + l)
+      else assert false in
+    list_of_stream (from_string s)
+
+(*
+let toks_of_float : (int * int) -> t_list =
   fun (f,p) ->
     let sm = if f=0. then "" else string_of_int (int_of_float ((abs_float f) *. (power10 (-p)))) in
     let l = String.length sm in
         if l >= 3 & p+l <> 0 then String.sub sm 0 3 ^ "." ^ String.sub sm 3 (l-3) ^ exp (p+l-3)
         else "0." ^ sm ^ exp (p + l) in
     list_of_stream (from_string s)
+*)
 
 (* messages d'erreur syntaxique *)
 
   | [<'Nat n>] -> n
   | [<'MinusNat n>] -> (- n)
 
+(* get the fraction and exponent (integers) of a float number from its writing *)
+let decimal_of_sfloat : string -> decimal =
+  fun s ->
+      let l = String.length s in
+      let i_e, p =
+        try
+          let i_e = String.index s 'e' in
+          i_e,
+          int_of_string (String.sub s (i_e+1) (l-(i_e+1)))
+        with Not_found -> l, 0 in
+      let i_dot, frac, expo =
+        try 
+	  let i_dot = String.index s '.' in
+	  i_dot,
+	  int_of_string (String.sub s 0 i_dot ^ String.sub s (i_dot+1) (i_e - i_dot - 1)),
+	  p - (i_e - i_dot - 1)
+	with Not_found ->
+	  i_e,
+	  int_of_string (String.sub s 0 i_e),
+	  p in
+      frac, expo
+
 (* parsing a float *)
-let rec parse_float : t_stream -> float * int = parser
-  | [<s = parse_float0>] -> (float_of_string s, prec_of_sfloat s)
-and parse_float0 = parser
-(*  | [<'Dot; m2 = parse_float_decimal; s = parse_float4>] -> "." ^ m2 ^ s *)
-  | [<'Nat m1; s = parse_float2>] -> string_of_int m1 ^ s
-  | [<'MinusNat m1; s = parse_float2>] -> "-" ^ string_of_int m1 ^ s
-(*  | [<'Symbol "-"; 'Dot; m2 = parse_float_decimal; s = parse_float4>] -> "-." ^ m2 ^ s *)
-and parse_float2 = parser
-  | [<'Dot; s = parse_float3>] -> "." ^ s
-  | [<exp = parse_float4>] -> "." ^ exp
-and parse_float3 = parser
-  | [<m2 = parse_float_decimal; s = parse_float4>] -> m2 ^ s
-  | [<e = parse_float_e; s = parse_float5>] -> e ^ s
-  | [<exp = parse_float_exp>] -> exp
+let rec parse_decimal : t_stream -> decimal = parser
+  | [<s = parse_decimal0>] -> decimal_of_sfloat s (*float_of_string s, prec_of_sfloat s*)
+and parse_decimal0 = parser
+(*  | [<'Dot; m2 = parse_decimal_decimal; s = parse_decimal4>] -> "." ^ m2 ^ s *)
+  | [<'Nat m1; s = parse_decimal2>] -> string_of_int m1 ^ s
+  | [<'MinusNat m1; s = parse_decimal2>] -> "-" ^ string_of_int m1 ^ s
+(*  | [<'Symbol "-"; 'Dot; m2 = parse_decimal_decimal; s = parse_decimal4>] -> "-." ^ m2 ^ s *)
+and parse_decimal2 = parser
+  | [<'Dot; s = parse_decimal3>] -> "." ^ s
+  | [<exp = parse_decimal4>] -> "." ^ exp
+and parse_decimal3 = parser
+  | [<m2 = parse_decimal_decimal; s = parse_decimal4>] -> m2 ^ s
+  | [<e = parse_decimal_e; s = parse_decimal5>] -> e ^ s
+  | [<exp = parse_decimal_exp>] -> exp
   | [<>] -> ""
-and parse_float4 = parser
-  | [<e = parse_float_e; s = parse_float5>] -> e ^ s
-  | [<exp = parse_float_exp>] -> exp
+and parse_decimal4 = parser
+  | [<e = parse_decimal_e; s = parse_decimal5>] -> e ^ s
+  | [<exp = parse_decimal_exp>] -> exp
   | [<>] -> ""
-and parse_float5 = parser
-  | [<p = parse_float_decimal>] -> p
-  | [<p = parse_float_minus_decimal>] -> p
-and parse_float_decimal = parser
-  | [<'Nat 0; d = parse_float_decimal2>] -> "0" ^ d
+and parse_decimal5 = parser
+  | [<p = parse_decimal_decimal>] -> p
+  | [<p = parse_decimal_minus_decimal>] -> p
+and parse_decimal_decimal = parser
+  | [<'Nat 0; d = parse_decimal_decimal2>] -> "0" ^ d
   | [<'Nat d>] -> string_of_int d
-and parse_float_minus_decimal = parser
-  | [<'MinusNat 0; d = parse_float_decimal2>] -> "-0" ^ d
+and parse_decimal_minus_decimal = parser
+  | [<'MinusNat 0; d = parse_decimal_decimal2>] -> "-0" ^ d
   | [<'MinusNat d>] -> "-" ^ string_of_int d
-and parse_float_decimal2 = parser
-  | [<'Nat 0; d = parse_float_decimal2>] -> "0" ^ d
+and parse_decimal_decimal2 = parser
+  | [<'Nat 0; d = parse_decimal_decimal2>] -> "0" ^ d
   | [<'Nat d>] -> string_of_int d
   | [<>] -> ""
-and parse_float_e = parser
+and parse_decimal_e = parser
   | [<'Symbol "e">] -> "e"
   | [<'Symbol "E">] -> "e"
-and parse_float_exp = parser
+and parse_decimal_exp = parser
   | [<'Symbol exp when Str.string_match (Str.regexp "e[0-9]+$") exp 0>] -> exp
   | [<'Symbol exp when Str.string_match (Str.regexp "E[0-9]+$") exp 0>] -> exp
 
 (* parsing a number *)
-type num = Int of int | Float of (float * int)
+type num = Int of int | Float of decimal
 
 let rec parse_num : t_stream -> num = parser
-  | [<i,s = parse_num0>] ->
+  | [<i, s = parse_num0>] ->
       if i
       then Int (int_of_string s)
-      else Float (float_of_string s, prec_of_sfloat s)
+      else Float (decimal_of_sfloat s) (*float_of_string s, prec_of_sfloat s*)
 and parse_num0 = parser
 (*  | [<'Dot; m2 = parse_num_decimal; s = parse_num4>] -> false, "." ^ m2 ^ s *)
   | [<'Nat m1; i,s = parse_num2>] -> i, string_of_int m1 ^ s
 | [<>] -> default
 
 let parse_option_float ? (default=0.) n = parser
-| [<'Symbol "-"; 'Symbol s when s=n ?? wrong_option_name n; (x,_) = parse_float ?? "Syntax error: float expected after option -"^n>] -> x
+| [<'Symbol "-"; 'Symbol s when s=n ?? wrong_option_name n; dec = parse_decimal ?? "Syntax error: float expected after option -"^n>] -> float_of_decimal dec
 | [<>] -> default
 
 let parse_option_string ?(default="") n = parser
 type t =
     BackQuote | Tilda | Exclam | At | Sharp | Dollar | Percent | Hat | Et | Star
   | LeftPar | RightPar | Minus | Plus | Equal | LeftAcc | RightAcc | LeftBra | RightBra
-  | Pipe | BackSlash | Slash | Interro | LT | GT | Comma | DotDot | Dot | Colon | SemiColon
+  | Pipe | BackSlash | Slash | Interro | LT | GT | Comma | Dot | Colon | SemiColon
   | DoubleQuote | Quote
-  | Ident of string | Int of int | Float of float * int | Char of char | String of string | Term of string
+  | Ident of string
+  | Nat of int
+  | Char of char | String of string | Term of string
   | PP_tilda | PP_space | PP_cut | PP_break of int * int | PP_newline
 
 (* predicate filtering PP_* tokens *)