atoms.ml 9.5 KB
Newer Older
1
open Encodings
2

3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 18 19 20 21 22 23
module Symbol = Pool.Make(Utf8)

type v = Ns.t * Symbol.t
let vcompare (ns1,x1) (ns2,x2) =
  let c = Ns.compare ns1 ns2 in if c <> 0 then c else Symbol.compare x1 x2
let vhash (ns,x) = ns + 17 * x

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)

24
let value (ns,x) = (ns, Symbol.value x)
25

26 27
let vprint ppf (ns,x) = 
  Format.fprintf ppf "%s" (Ns.InternalPrinter.tag (ns, Symbol.value x))
28 29

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

let print_v ppf a = 
  Format.fprintf ppf "`%a" vprint a

module SymbolSet = struct
36 37
  module SList = SortedList.Make(Symbol)
  type t = Finite of SList.t | Cofinite of SList.t
38 39 40 41 42 43 44 45 46 47 48 49 50 51 52 53 54 55 56 57 58 59 60 61 62 63 64 65 66 67 68 69 70 71 72 73 74 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

  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

  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 " |@ ") 
	  (fun x -> print_v ppf (ns,x)) l
    | Cofinite t ->
	Format.fprintf ppf "@[`%a" print_any_in_ns ns;
	List.iter (fun x -> Format.fprintf ppf " \@ %a" print_v (ns,x)) t;
	Format.fprintf ppf "@]"
end

110
module T0 = SortedList.Make(Ns)
111
module T = T0.Map
112
type t = Finite of SymbolSet.t T.map | Cofinite of SymbolSet.t T.map
113

114 115 116
let empty = Finite T.empty
let any   = Cofinite T.empty
let any_in_ns ns = Finite (T.singleton ns SymbolSet.any)
117

118 119 120 121 122 123 124 125 126 127 128 129 130 131 132 133
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))
134 135 136

let cup s t =
  match (s,t) with
137 138 139 140
    | (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)
141 142 143

let cap s t =
  match (s,t) with
144 145 146 147
    | (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)
148
	
149
let diff s t =
150
  match (s,t) with
151 152 153 154
    | (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)
155

156
let is_empty = function
157
  | Finite l -> T.is_empty l
158
  | _ -> false
159

160 161 162 163 164 165 166 167 168 169 170 171 172
let print_tag = function
  | Finite l ->
      (match T.get l with 
	| [ns, SymbolSet.Finite [a]] -> 
	    Some (fun ppf -> vprint ppf (ns,a))
	| [ns, SymbolSet.Cofinite []] -> 
	    Some (fun ppf -> Format.fprintf ppf "%a" print_any_in_ns ns)
	| _ -> None)
  | Cofinite l ->
      (match T.get l with
	 | [] -> 
	     Some (fun ppf -> Format.fprintf ppf "_")
	 | _ -> None)
173

174 175 176 177 178 179 180 181 182 183 184 185 186 187
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 *)
188

189
let print = function
190 191 192 193 194 195 196 197 198 199 200 201
  | 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 ]
202

203

204 205 206
let hash accu = function
  | Finite l -> 17 * accu + (T.hash SymbolSet.hash l)
  | Cofinite l -> 17 * (accu + 2) +  (T.hash SymbolSet.hash l)
207

208
let compare l1 l2 =
209
  match (l1,l2) with
210 211 212
    | Finite l1, Finite l2 
    | Cofinite l1, Cofinite l2 -> T.compare SymbolSet.compare l1 l2
    | Finite _, Cofinite _ -> -1
213 214
    | _ -> 1

215 216
let equal t1 t2 = 
  compare t1 t2 = 0
217

218 219 220 221
(* Optimize lookup:
   - decision tree
   - merge adjacent segment with same result
*)
222

223 224 225 226 227
(*
type 'a map = v -> 'a

let rec mk_map l v = 
  match l with
228
    | [] -> assert false
229 230 231 232 233 234 235 236 237 238 239 240 241
    | (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
242 243 244 245 246 247

  type 'a s =
    | DError
    | DReturn of 'a
    | DLeaf of int * 'a * 'a
    | DBranch of int * int * 'a s * 'a s
248 249 250 251 252 253 254
	
  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

255 256 257 258 259 260 261 262 263 264 265 266 267 268 269 270 271 272
  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
273 274

  let rec find k = function
275 276 277 278
    | 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)
279 280 281 282 283 284 285 286 287 288 289 290 291 292 293 294 295 296 297 298

  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

299 300 301 302 303 304 305 306
  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
307

308
type 'a map = 'a IMap.s IMap.s
309

310
let get_map (ns,x) m = IMap.find x (IMap.find ns m)
311

312 313
module IntSet = 
  Set.Make(struct type t = int let compare (x:int) y = Pervasives.compare x y end)
314 315

let mk_map l =
316
  let all_ns = ref IntSet.empty in
317 318 319 320
  let def = ref None in
  List.iter 
    (function
       | (Finite s, _) -> 
321 322 323 324 325 326
	   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 = 
327 328 329 330 331 332
      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 ->
333
		 def := Some y; accu)
334
        IMap.Empty 
335 336 337 338 339 340 341 342 343 344 345 346 347 348 349 350 351 352 353 354 355 356 357 358 359 360 361 362
        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




363