atoms.ml 10.4 KB
Newer Older
1
open Encodings
2

3 4
module Symbol = Pool.Make(Utf8)

5 6 7 8 9 10
module V = struct

include Custom.Dummy

type t = Ns.t * Symbol.t
let compare (ns1,x1) (ns2,x2) =
11
  let c = Ns.compare ns1 ns2 in if c <> 0 then c else Symbol.compare x1 x2
12
let hash (ns,x) = ns + 17 * x
13 14 15 16 17 18 19 20 21 22 23 24 25 26 27

let atom_table = Hashtbl.create 63


(* Hash-consing: only to reduce memory usage *)
let mk ns x =
  let a = (ns, x) in
  try Hashtbl.find atom_table a 
  with Not_found ->
    let b = (ns, Symbol.mk x) in
    Hashtbl.add atom_table a b;
    b

let mk_ascii s = mk Ns.empty (Utf8.mk s)

28
let value (ns,x) = (ns, Symbol.value x)
29

30
let print ppf (ns,x) = 
31
  Format.fprintf ppf "%s" (Ns.InternalPrinter.tag (ns, Symbol.value x))
32 33

let print_any_in_ns ppf ns =
34
  Format.fprintf ppf "%s" (Ns.InternalPrinter.any_ns ns)
35

36 37 38 39
let print_quote ppf a = 
  Format.fprintf ppf "`%a" print a

end
40 41

module SymbolSet = struct
42 43
  module SList = SortedList.Make(Symbol)
  type t = Finite of SList.t | Cofinite of SList.t
44 45 46 47 48 49 50 51 52 53 54 55

  let hash = function
    | Finite l -> SList.hash l
    | Cofinite l -> 17 * SList.hash l + 1

  let compare l1 l2 =
    match (l1,l2) with
      | Finite l1, Finite l2 
      | Cofinite l1, Cofinite l2 -> SList.compare l1 l2
      | Finite _, Cofinite _ -> -1
      | _ -> 1

56 57 58 59 60 61 62 63 64 65 66 67 68 69 70 71 72 73 74
  let equal l1 l2 = compare l1 l2 = 0

  let serialize t = function
    | Finite s -> Serialize.Put.bool t true; SList.serialize t s
    | Cofinite s -> Serialize.Put.bool t false; SList.serialize t s

   let deserialize t = 
    if Serialize.Get.bool t
    then Finite (SList.deserialize t)
    else Cofinite (SList.deserialize t)

   let check = function
    | Finite s | Cofinite s -> SList.check s

  let dump ppf = function
    | Finite s -> Format.fprintf ppf "Finite[%a]" SList.dump s
    | Cofinite s -> Format.fprintf ppf "Cofinite[%a]" SList.dump s


75 76 77 78 79 80 81 82 83 84 85 86 87 88 89 90 91 92 93 94 95 96 97 98 99 100 101 102 103 104 105 106 107 108 109 110 111 112 113 114 115 116 117 118 119 120 121 122 123 124 125 126 127
  let empty = Finite []
  let any = Cofinite []
  let atom x = Finite [x]

  let cup s t =
    match (s,t) with
      | (Finite s, Finite t) -> Finite (SList.cup s t)
      | (Finite s, Cofinite t) -> Cofinite (SList.diff t s)
      | (Cofinite s, Finite t) -> Cofinite (SList.diff s t)
      | (Cofinite s, Cofinite t) -> Cofinite (SList.cap s t)

  let cap s t =
    match (s,t) with
      | (Finite s, Finite t) -> Finite (SList.cap s t)
      | (Finite s, Cofinite t) -> Finite (SList.diff s t)
      | (Cofinite s, Finite t) -> Finite (SList.diff t s)
      | (Cofinite s, Cofinite t) -> Cofinite (SList.cup s t)

  let diff s t =
    match (s,t) with
      | (Finite s, Cofinite t) -> Finite (SList.cap s t)
      | (Finite s, Finite t) -> Finite (SList.diff s t)
      | (Cofinite s, Cofinite t) -> Finite (SList.diff t s)
      | (Cofinite s, Finite t) -> Cofinite (SList.cup s t)

  let neg = function
      | Finite s -> Cofinite s
      | Cofinite s -> Finite s
	
  let contains x = function
    | Finite s -> SList.mem s x
    | Cofinite s -> not (SList.mem s x)
	
  let disjoint s t =
    match (s,t) with
      | (Finite s, Finite t) -> SList.disjoint s t
      | (Finite s, Cofinite t) -> SList.subset s t
      | (Cofinite s, Finite t) -> SList.subset t s
      | (Cofinite s, Cofinite t) -> false

  let rec iter_sep sep f = function
    | [] -> ()
    | [ h ] -> f h
    | h :: t -> f h; sep (); iter_sep sep f t

(* Atom 
   bla:*   bla:x
   :* :x *)

  let print ns ppf = function
    | Finite l -> 
	iter_sep 
	  (fun () -> Format.fprintf ppf " |@ ") 
128
	  (fun x -> V.print_quote ppf (ns,x)) l
129
    | Cofinite t ->
130 131
	Format.fprintf ppf "@[`%a" V.print_any_in_ns ns;
	List.iter (fun x -> Format.fprintf ppf " \@ %a" V.print_quote (ns,x)) t;
132 133 134
	Format.fprintf ppf "@]"
end

135
module T0 = SortedList.Make(Ns)
136
module TMap = T0.MakeMap(SymbolSet)
137
module T = T0.Map
138 139 140 141 142 143 144 145 146 147 148 149 150
type t = Finite of TMap.t | Cofinite of TMap.t
include Custom.Dummy

let serialize t = function
  | Finite s -> Serialize.Put.bool t true; TMap.serialize t s
  | Cofinite s -> Serialize.Put.bool t false; TMap.serialize t s

let deserialize t = 
  if Serialize.Get.bool t
  then Finite (TMap.deserialize t)
  else Cofinite (TMap.deserialize t)


151

152 153 154
let empty = Finite T.empty
let any   = Cofinite T.empty
let any_in_ns ns = Finite (T.singleton ns SymbolSet.any)
155

156 157 158 159 160 161 162 163 164 165 166 167 168 169 170 171
let finite l =
  let l = 
    T.filter 
      (fun _ x -> match x with SymbolSet.Finite [] -> false | _ -> true)
      l in
  Finite l

let cofinite l =
  let l = 
    T.filter 
      (fun _ x -> match x with SymbolSet.Cofinite [] -> false | _ -> true)
      l in
  Cofinite l
  

let atom (ns,x) = Finite (T.singleton ns (SymbolSet.atom x))
172 173 174

let cup s t =
  match (s,t) with
175 176 177 178
    | (Finite s, Finite t) -> finite (T.merge SymbolSet.cup s t)
    | (Finite s, Cofinite t) -> cofinite (T.sub SymbolSet.diff t s)
    | (Cofinite s, Finite t) -> cofinite (T.sub SymbolSet.diff s t)
    | (Cofinite s, Cofinite t) -> cofinite (T.cap SymbolSet.cap s t)
179 180 181

let cap s t =
  match (s,t) with
182 183 184 185
    | (Finite s, Finite t) -> finite (T.cap SymbolSet.cap s t)
    | (Finite s, Cofinite t) -> finite (T.sub SymbolSet.diff s t)
    | (Cofinite s, Finite t) -> finite (T.sub SymbolSet.diff t s)
    | (Cofinite s, Cofinite t) -> cofinite (T.merge SymbolSet.cup s t)
186
	
187
let diff s t =
188
  match (s,t) with
189 190 191 192
    | (Finite s, Cofinite t) -> finite (T.cap SymbolSet.cap s t)
    | (Finite s, Finite t) -> finite (T.sub SymbolSet.diff s t)
    | (Cofinite s, Cofinite t) -> finite (T.sub SymbolSet.diff t s)
    | (Cofinite s, Finite t) -> cofinite (T.merge SymbolSet.cup s t)
193

194
let is_empty = function
195
  | Finite l -> T.is_empty l
196
  | _ -> false
197

198 199 200 201
let print_tag = function
  | Finite l ->
      (match T.get l with 
	| [ns, SymbolSet.Finite [a]] -> 
202
	    Some (fun ppf -> V.print ppf (ns,a))
203
	| [ns, SymbolSet.Cofinite []] -> 
204
	    Some (fun ppf -> Format.fprintf ppf "%a" V.print_any_in_ns ns)
205 206 207 208 209 210
	| _ -> None)
  | Cofinite l ->
      (match T.get l with
	 | [] -> 
	     Some (fun ppf -> Format.fprintf ppf "_")
	 | _ -> None)
211

212 213 214 215 216 217 218 219 220 221 222 223 224 225
let symbol_set ns = function
  | Finite s ->
      (try T.assoc ns s with Not_found -> SymbolSet.empty)
  | Cofinite s ->
      (try SymbolSet.neg (T.assoc ns s) with Not_found -> SymbolSet.any)

let contains (ns,x) = function
  | Finite s -> 
      (try SymbolSet.contains x (T.assoc ns s) with Not_found -> false)
  | Cofinite s -> 
      (try not (SymbolSet.contains x (T.assoc ns s)) with Not_found -> true)
	
let disjoint s t = 
  is_empty (cap t s) (* TODO: OPT *)
226

227
let print = function
228 229 230 231 232 233 234 235 236 237 238 239
  | Finite l -> 
      List.map (fun (ns,s) ppf -> SymbolSet.print ns ppf s) (T.get l)
  | Cofinite l -> 
      match T.get l with
	| [] -> [ fun ppf -> Format.fprintf ppf "Atom" ]
	| l ->
	    [ fun ppf ->
		Format.fprintf ppf "Atom";
		List.iter 
		  (fun (ns,s) -> 
		     Format.fprintf ppf " \@ (%a)" (SymbolSet.print ns) s)
		  l ]
240

241

242 243 244
let hash = function
  | Finite l -> 1 + 17 * (TMap.hash l)
  | Cofinite l -> 2 +  17 * (TMap.hash l)
245

246
let compare l1 l2 =
247
  match (l1,l2) with
248
    | Finite l1, Finite l2 
249
    | Cofinite l1, Cofinite l2 -> TMap.compare l1 l2
250
    | Finite _, Cofinite _ -> -1
251 252
    | _ -> 1

253 254
let equal t1 t2 = 
  compare t1 t2 = 0
255

256 257 258 259
(* Optimize lookup:
   - decision tree
   - merge adjacent segment with same result
*)
260

261 262 263 264 265
(*
type 'a map = v -> 'a

let rec mk_map l v = 
  match l with
266
    | [] -> assert false
267 268 269 270 271 272 273 274 275 276 277 278 279
    | (x,y) :: rem -> if (contains v x) then y else mk_map rem v

let get_map v m = m v
*)


(* Patricia trees; code adapted from http://www.lri.fr/~filliatr/ftp/ocaml/misc/ptmap.ml *)

module IMap = struct
  type 'a t =
    | Empty
    | Leaf of int * 'a
    | Branch of int * int * 'a t * 'a t
280 281 282 283 284 285

  type 'a s =
    | DError
    | DReturn of 'a
    | DLeaf of int * 'a * 'a
    | DBranch of int * int * 'a s * 'a s
286 287 288 289 290 291 292
	
  let zero_bit k m = (k land m) == 0
  let lowest_bit x = x land (-x)
  let branching_bit p0 p1 = lowest_bit (p0 lxor p1)
  let mask p m = p land (m-1)
  let match_prefix k p m = (mask k m) == p

293 294 295 296 297 298 299 300 301 302 303 304 305 306 307 308 309 310
  let rec prepare_def y = function
    | Empty -> DReturn y
    | Leaf (k,x) -> DLeaf (k,x,y)
    | Branch (p,m,t0,t1) -> 
	DBranch (p,m,prepare_def y t0, prepare_def y t1)

  let rec prepare_nodef = function
    | Empty -> DError
    | Leaf (k,x) -> DReturn x
    | Branch (p,m,t0,t1) ->
	match (prepare_nodef t0, prepare_nodef t1) with
	  | (DReturn x0, DReturn x1) when x0 == x1 -> DReturn x0
	  | (t0,t1) -> DBranch (p,m,t0,t1)

  let prepare def y =
    match def with 
      | None -> prepare_nodef y
      | Some def -> prepare_def def y
311 312

  let rec find k = function
313 314 315 316
    | DError -> assert false
    | DReturn y -> y
    | DLeaf (j,x,y) -> if k == j then x else y
    | DBranch (_, m, l, r) -> find k (if zero_bit k m then l else r)
317 318 319 320 321 322 323 324 325 326 327 328 329 330 331 332 333 334 335 336

  let join p0 t0 p1 t1 =
    let m = branching_bit p0 p1 in
    if zero_bit p0 m 
    then Branch (mask p0 m, m, t0, t1)
    else Branch (mask p0 m, m, t1, t0)

  let rec add k x = function
    | Empty -> Leaf (k,x)
    | Leaf (j,_) as t -> 
	if j == k then Leaf (k,x) else join k (Leaf (k,x)) j t
    | Branch (p,m,t0,t1) as t ->
	if match_prefix k p m 
	then
	  if zero_bit k m 
	  then Branch (p, m, add k x t0, t1)
	  else Branch (p, m, t0, add k x t1)
	else
	  join k (Leaf (k,x)) p t

337 338 339 340 341 342 343 344
  let rec dump f ppf = function
    | DError -> Format.fprintf ppf "Error" 
    | DReturn x -> Format.fprintf ppf "Return %a" f x 
    | DLeaf(j,x,y) -> Format.fprintf ppf "Leaf(%i,%a,%a)" j f x f y
    | DBranch (p,m,t0,t1) -> 
	Format.fprintf ppf "B(%i,%i,%a,%a)" p m (dump f) t0 (dump f) t1
	
end
345

346
type 'a map = 'a IMap.s IMap.s
347

348
let get_map (ns,x) m = IMap.find x (IMap.find ns m)
349

350 351
module IntSet = 
  Set.Make(struct type t = int let compare (x:int) y = Pervasives.compare x y end)
352 353

let mk_map l =
354
  let all_ns = ref IntSet.empty in
355 356 357 358
  let def = ref None in
  List.iter 
    (function
       | (Finite s, _) -> 
359 360 361 362 363 364
	   List.iter (fun (ns,_) -> all_ns := IntSet.add ns !all_ns) (T.get s)
       | (Cofinite _, y) -> def := Some (IMap.DReturn y)) l;

  let one_ns ns =
    let def = ref None in
    let t = 
365 366 367 368 369 370
      List.fold_left
        (fun accu (s, y) -> 
	   match (symbol_set ns s) with
	     | SymbolSet.Finite syms ->
		 List.fold_left (fun accu x -> IMap.add x y accu) accu syms
	     | SymbolSet.Cofinite syms ->
371
		 def := Some y; accu)
372
        IMap.Empty 
373 374 375 376 377 378 379 380 381 382 383 384 385 386 387 388 389 390 391 392 393 394 395 396 397 398 399 400
        l in
    IMap.prepare !def t
  in

  let t = 
    List.fold_left (fun accu ns -> IMap.add ns (one_ns ns) accu)
      IMap.Empty 
      (IntSet.elements !all_ns) in
  let t = IMap.prepare !def t in

(*
  let rec rank y i = function
    | (_,x)::_ when x == y -> i
    | _::r -> rank y (succ i) r
    | [] -> assert false in

  let dump_ns =
    IMap.dump (fun ppf y -> Format.fprintf ppf "[%i]" (rank y 0 l)) in

  Format.fprintf Format.std_formatter "table: %a@." 
    (IMap.dump (fun ppf y -> Format.fprintf ppf "[%a]" dump_ns y)) t;
*)

  t




401