patterns.ml 71.5 KB
Newer Older
1
exception Error of string
2
open Ident
3

4 5 6 7 8
let print_lab ppf l = 
  if (l == LabelPool.dummy_max) 
  then Format.fprintf ppf "<dummy_max>"
  else Label.print ppf (LabelPool.value l)

9 10 11
(*
To be sure not to use generic comparison ...
*)
12 13 14 15 16 17
let (=) : int -> int -> bool = (==)
let (<) : int -> int -> bool = (<)
let (<=) : int -> int -> bool = (<=)
let (<>) : int -> int -> bool = (<>)
let compare = 1

18

19
(* Syntactic algebra *)
20
(* Constraint: any node except Constr has fv<>[] ... *)
21
type d =
22
  | Constr of Types.t
23
  | Cup of descr * descr
24
  | Cap of descr * descr
25
  | Times of node * node
26
  | Xml of node * node
27
  | Record of label * node
28 29
  | Capture of id
  | Constant of id * Types.const
30
  | Dummy
31 32
and node = {
  id : int;
33
  mutable descr : descr;
34
  accept : Types.Node.t;
35
  fv : fv
36 37 38
} and descr = Types.t * fv * d


39

40
let id x = x.id
41
let descr x = x.descr
42 43
let fv x = x.fv
let accept x = Types.internalize x.accept
44 45 46

let printed = ref []
let to_print = ref []
47
let rec print ppf (a,_,d) = 
48
  match d with
49
    | Constr t -> Types.Print.print ppf t
50 51 52 53 54 55 56 57 58
    | Cup (p1,p2) -> Format.fprintf ppf "(%a | %a)" print p1 print p2
    | Cap (p1,p2) -> Format.fprintf ppf "(%a & %a)" print p1 print p2
    | Times (n1,n2) -> 
	Format.fprintf ppf "(P%i,P%i)" n1.id n2.id;
	to_print := n1 :: n2 :: !to_print
    | Xml (n1,n2) -> 
	Format.fprintf ppf "XML(P%i,P%i)" n1.id n2.id;
	to_print := n1 :: n2 :: !to_print
    | Record (l,n) -> 
59
	Format.fprintf ppf "{ %a =  P%i }" Label.print (LabelPool.value l) n.id;
60 61
	to_print := n :: !to_print
    | Capture x ->
62
	Format.fprintf ppf "%a" Ident.print x
63
    | Constant (x,c) ->
64
	Format.fprintf ppf "(%a := %a)" Ident.print x
65
	  Types.Print.print_const c
66 67
    | Dummy ->
	Format.fprintf ppf "*DUMMY*"
68

69
let dump_print ppf =
70
  while !to_print != [] do
71 72 73 74 75 76 77 78 79 80 81
    let p = List.hd !to_print in
    to_print := List.tl !to_print;
    if not (List.mem p.id !printed) then
      ( printed := p.id :: !printed;
	Format.fprintf ppf "P%i:=%a\n" p.id print (descr p)
      )
  done

let print ppf d =
  Format.fprintf ppf "%a@\n" print d;
  dump_print ppf
82

83 84 85 86 87
let print_node ppf n =
  Format.fprintf ppf "P%i" n.id;
  to_print := n :: !to_print;
  dump_print ppf

88

89 90
let counter = State.ref "Patterns.counter" 0

91
let dummy = (Types.empty,IdSet.empty,Dummy)
92 93
let make fv =
  incr counter;
94
  { id = !counter; descr = dummy; accept = Types.make (); fv = fv }
95 96

let define x ((accept,fv,_) as d) =
97
  (* assert (x.fv = fv); *)
98
  Types.define x.accept accept;
99
  x.descr <- d
100

101 102 103 104 105
let cons fv d =
  let q = make fv in
  define q d;
  q

106
let constr x = (x,IdSet.empty,Constr x)
107
let cup ((acc1,fv1,_) as x1) ((acc2,fv2,_) as x2) = 
108 109 110 111 112
  if not (IdSet.equal fv1 fv2) then (
    let x = match IdSet.pick (IdSet.diff fv1 fv2) with
      | Some x -> x
      | None -> match IdSet.pick (IdSet.diff fv2 fv1) with Some x -> x 
	  | None -> assert false
113 114 115
    in
    raise 
      (Error 
116
	 ("The capture variable " ^ (Ident.to_string x) ^ 
117 118
	  " should appear on both side of this | pattern"))
  );
119
  (Types.cup acc1 acc2, IdSet.cup fv1 fv2, Cup (x1,x2))
120
let cap ((acc1,fv1,_) as x1) ((acc2,fv2,_) as x2) = 
121 122 123
  if not (IdSet.disjoint fv1 fv2) then (
    match IdSet.pick (IdSet.cap fv1 fv2) with
      | Some x -> 
124 125
	  raise 
	  (Error 
126
	     ("The capture variable " ^ (Ident.to_string x) ^ 
127
	      " cannot appear on both side of this & pattern"))
128
      | None -> assert false
129
  );
130
  (Types.cap acc1 acc2, IdSet.cup fv1 fv2, Cap (x1,x2))
131
let times x y =
132
  (Types.times x.accept y.accept, IdSet.cup x.fv y.fv, Times (x,y))
133
let xml x y =
134
  (Types.xml x.accept y.accept, IdSet.cup x.fv y.fv, Xml (x,y))
135
let record l x = 
136
  (Types.record l x.accept, x.fv, Record (l,x))
137 138
let capture x = (Types.any, IdSet.singleton x, Capture x)
let constant x c = (Types.any, IdSet.singleton x, Constant (x,c))
139

140

141 142 143 144 145 146
module Node = struct
  type t = node
  let compare n1 n2 = n1.id - n2.id
  let equal n1 n2 = n1.id == n2.id
  let hash n = n.id

147
  let check n = ()
148
  let dump = print_node
149

150 151 152 153 154 155 156 157 158 159 160 161 162 163 164 165 166 167 168 169 170 171 172 173 174 175 176 177 178 179 180 181 182 183 184 185 186 187 188 189 190 191 192 193 194 195 196 197 198 199 200 201 202 203 204 205 206

  module SMemo = Set.Make(Custom.Int)
  let memo = Serialize.Put.mk_property (fun t -> ref SMemo.empty)
  let rec serialize t n = 
    let l = Serialize.Put.get_property memo t in
    Serialize.Put.int t n.id;
    if not (SMemo.mem n.id !l) then (
      l := SMemo.add n.id !l;
      Types.Node.serialize t n.accept;
      IdSet.serialize t n.fv;
      serialize_descr t n.descr
    )
  and serialize_descr s (_,_,d) =
    serialize_d s d
  and serialize_d s = function
    | Constr t ->
	Serialize.Put.bits 3 s 0;
	Types.serialize s t
    | Cup (p1,p2) ->
	Serialize.Put.bits 3 s 1;
	serialize_descr s p1; 
	serialize_descr s p2
    | Cap (p1,p2) ->
	Serialize.Put.bits 3 s 2;
	serialize_descr s p1; 
	serialize_descr s p2
    | Times (p1,p2) ->
	Serialize.Put.bits 3 s 3;
	serialize s p1;
	serialize s p2
    | Xml (p1,p2) ->
	Serialize.Put.bits 3 s 4;
	serialize s p1;
	serialize s p2
    | Record (l,p) ->
	Serialize.Put.bits 3 s 5;
	LabelPool.serialize s l;
	serialize s p
    | Capture x ->
	Serialize.Put.bits 3 s 6;
	Id.serialize s x
    | Constant (x,c) ->
	Serialize.Put.bits 3 s 7;
	Id.serialize s x;
	Types.Const.serialize s c
    | Dummy -> assert false

  module DMemo = Map.Make(Custom.Int)
  let memo = Serialize.Get.mk_property (fun t -> ref DMemo.empty)
  let rec deserialize t = 
    let l = Serialize.Get.get_property memo t in
    let id = Serialize.Get.int t in
    try DMemo.find id !l
    with Not_found ->
      let accept = Types.Node.deserialize t in
      let fv = IdSet.deserialize t in
      incr counter;
207
      let n = { id = !counter; descr = dummy; accept = accept; fv = fv } in
208 209 210 211 212 213 214 215 216 217 218 219 220 221 222 223 224 225 226 227 228 229 230 231 232 233 234 235 236 237 238 239 240 241 242 243
      l := DMemo.add id n !l;
      n.descr <- deserialize_descr t;
      n
  and deserialize_descr s =
    match Serialize.Get.bits 3 s with
      | 0 -> constr (Types.deserialize s)
      | 1 ->
	  (* Avoid unnecessary tests *)
	  let (acc1,fv1,_) as x1 = deserialize_descr s in
	  let (acc2,fv2,_) as x2 = deserialize_descr s in
	  (Types.cup acc1 acc2, IdSet.cup fv1 fv2, Cup (x1,x2))
      | 2 ->
	  let (acc1,fv1,_) as x1 = deserialize_descr s in
	  let (acc2,fv2,_) as x2 = deserialize_descr s in
	  (Types.cap acc1 acc2, IdSet.cup fv1 fv2, Cap (x1,x2))
      | 3 ->
	  let x = deserialize s in
	  let y = deserialize s in
	  times x y
      | 4 ->
	  let x = deserialize s in
	  let y = deserialize s in
	  xml x y
      | 5 ->
	  let l = LabelPool.deserialize s in
	  let x = deserialize s in
	  record l x
      | 6 -> capture (Id.deserialize s)
      | 7 ->
	  let x = Id.deserialize s in
	  let c = Types.Const.deserialize s in
	  constant x c
      | _ -> assert false


end
244

245 246
(* Pretty-print *)

247
module Pat = struct
248
  type t = descr
249
  let rec compare (_,_,d1) (_,_,d2) = if d1 == d2 then 0 else
250 251 252 253 254 255 256 257 258 259 260 261 262 263 264 265 266 267 268 269 270 271 272 273 274 275 276 277 278 279 280
    match (d1,d2) with
      | Constr t1, Constr t2 -> Types.compare t1 t2
      | Constr _, _ -> -1 | _, Constr _ -> 1

      | Cup (x1,y1), Cup (x2,y2) | Cap (x1,y1), Cap (x2,y2) ->
	  let c = compare x1 x2 in if c <> 0 then c 
	  else compare y1 y2
      | Cup _, _ -> -1 | _, Cup _ -> 1
      | Cap _, _ -> -1 | _, Cap _ -> 1

      | Times (x1,y1), Times (x2,y2) | Xml (x1,y1), Xml (x2,y2) ->
	  let c = Node.compare x1 x2 in if c <> 0 then c
	  else Node.compare y1 y2
      | Times _, _ -> -1 | _, Times _ -> 1
      | Xml _, _ -> -1 | _, Xml _ -> 1

      | Record (x1,y1), Record (x2,y2) ->
	  let c = LabelPool.compare x1 x2 in if c <> 0 then c
	  else Node.compare y1 y2
      | Record _, _ -> -1 | _, Record _ -> 1

      | Capture x1, Capture x2 ->
	  Id.compare x1 x2
      | Capture _, _ -> -1 | _, Capture _ -> 1

      | Constant (x1,y1), Constant (x2,y2) ->
	  let c = Id.compare x1 x2 in if c <> 0 then c
	  else Types.Const.compare y1 y2
      | Constant _, _ -> -1 | _, Constant _ -> 1

      | Dummy, Dummy -> assert false
281 282 283 284 285 286 287 288 289 290 291 292 293

  let equal p1 p2 = compare p1 p2 == 0

  let rec hash (_,_,d) = match d with
    | Constr t -> 1 + 17 * (Types.hash t)
    | Cup (p1,p2) -> 2 + 17 * (hash p1) + 257 * (hash p2)
    | Cap (p1,p2) -> 3 + 17 * (hash p1) + 257 * (hash p2)
    | Times (q1,q2) -> 4 + 17 * q1.id + 257 * q2.id
    | Xml (q1,q2) -> 5 + 17 * q1.id + 257 * q2.id
    | Record (l,q) -> 6 + 17 * (LabelPool.hash l) + 257 * q.id
    | Capture x -> 7 + (Id.hash x)
    | Constant (x,c) -> 8 + 17 * (Id.hash x) + 257 * (Types.Const.hash c)
    | Dummy -> assert false
294 295 296 297 298

  let serialize _ _ = assert false
  let deserialize _ = assert false
  let check _ = assert false
  let dump _ = assert false
299 300 301
end

module Print = struct
302 303
  module M = Map.Make(Pat)
  module S = Set.Make(Pat)
304 305 306 307 308 309 310 311 312 313 314 315 316 317 318 319 320 321 322 323 324 325 326 327 328 329 330 331 332 333 334 335 336 337 338 339

  let names = ref M.empty
  let printed = ref S.empty
  let toprint = Queue.create ()
  let id = ref 0

  let rec mark seen ((_,_,d) as p) =
    if (M.mem p !names) then ()
    else if (S.mem p seen) then
      (incr id;
       names := M.add p !id !names;
       Queue.add p toprint)
    else 
      let seen = S.add p seen in
      match d with
	| Cup (p1,p2) | Cap (p1,p2) -> mark seen p1; mark seen p2
	| Times (q1,q2) | Xml (q1,q2) -> mark seen q1.descr; mark seen q2.descr
	| Record (_,q) -> mark seen q.descr
	| _ -> ()

  let rec print ppf p =
    try 
      let i = M.find p !names in
      Format.fprintf ppf "P%i" i
    with Not_found ->
      real_print ppf p
  and real_print ppf (_,_,d) =  match d with
    | Constr t ->
	Types.Print.print ppf t
    | Cup (p1,p2) ->
	Format.fprintf ppf "(%a | %a)" print p1 print p2
    | Cap (p1,p2) ->
	Format.fprintf ppf "(%a & %a)" print p1 print p2
    | Times (q1,q2) ->
	Format.fprintf ppf "(%a,%a)" print q1.descr print q2.descr
    | Xml (q1,{ descr = (_,_,Times(q2,q3)) }) ->
340
	Format.fprintf ppf "<(%a) (%a)>(%a)" print q1.descr print q2.descr print q3.descr
341 342 343 344 345 346 347 348 349 350 351 352 353 354 355 356 357 358 359 360 361 362 363 364 365 366
    | Xml _ -> assert false
    | Record (l,q) ->
	Format.fprintf ppf "{%a=%a}" Label.print (LabelPool.value l) print q.descr
    | Capture x ->
	Format.fprintf ppf "%a" Ident.print x
    | Constant (x,c) ->
	Format.fprintf ppf "(%a:=%a)" Ident.print x Types.Print.print_const c
    | Dummy -> assert false
      
  let print ppf p =
    mark S.empty p;
    print ppf p;
    let first = ref true in
    (try while true do
       let p = Queue.pop toprint in
       if not (S.mem p !printed) then 
	 ( printed := S.add p !printed;
	   Format.fprintf ppf " %s@ @[%a=%a@]"
	     (if !first then (first := false; "where") else "and")
	     print p
	     real_print p
	);
     done with Queue.Empty -> ());
    id := 0;
    names := M.empty;
    printed := S.empty
367 368 369 370 371 372 373 374 375 376 377


  let print_xs ppf xs =
    Format.fprintf ppf "{";
    let rec aux = function
      | [] -> ()
      | [x] -> Ident.print ppf x
      | x::q -> Ident.print ppf x; Format.fprintf ppf ","; aux q
    in
    aux xs;
    Format.fprintf ppf "}"
378 379 380
end


381 382 383 384

(* Static semantics *)

let cup_res v1 v2 = Types.Positive.cup [v1;v2]
385
let empty_res fv = IdMap.constant (Types.Positive.ty Types.empty) fv
386 387
let times_res v1 v2 = Types.Positive.times v1 v2

388
(* Try with a hash-table *)
389
module MemoFilter = Map.Make 
390
  (struct 
391
     type t = Types.t * node 
392 393
     let compare (t1,n1) (t2,n2) = 
       if n1.id < n2.id then -1 else if n1.id > n2.id then 1 else
394
       Types.compare t1 t2
395
   end)
396 397 398

let memo_filter = ref MemoFilter.empty

399
let rec filter_descr t (_,fv,d) : Types.Positive.v id_map =
400
(* TODO: avoid is_empty t when t is not changing (Cap) *)
401 402 403 404
  if Types.is_empty t 
  then empty_res fv
  else
    match d with
405
      | Constr _ -> IdMap.empty
406
      | Cup ((a,_,_) as d1,d2) ->
407
	  IdMap.merge cup_res
408 409
	    (filter_descr (Types.cap t a) d1)
	    (filter_descr (Types.diff t a) d2)
410
      | Cap (d1,d2) ->
411
	  IdMap.merge cup_res (filter_descr t d1) (filter_descr t d2)
412 413
      | Times (p1,p2) -> filter_prod fv p1 p2 t
      | Xml (p1,p2) -> filter_prod ~kind:`XML fv p1 p2 t
414 415 416
      | Record (l,p) ->
	  filter_node (Types.Record.project t l) p
      | Capture c ->
417
	  IdMap.singleton c (Types.Positive.ty t)
418
      | Constant (c, cst) ->
419
	  IdMap.singleton c (Types.Positive.ty (Types.constant cst))
420
      | Dummy -> assert false
421

422 423 424 425
and filter_prod ?kind fv p1 p2 t =
  List.fold_left 
    (fun accu (d1,d2) ->
       let term = 
426
	 IdMap.merge times_res (filter_node d1 p1) (filter_node d2 p2)
427
       in
428
       IdMap.merge cup_res accu term
429 430 431 432 433
    )
    (empty_res fv)
    (Types.Product.normal ?kind t)


434
and filter_node t p : Types.Positive.v id_map =
435 436
  try MemoFilter.find (t,p) !memo_filter
  with Not_found ->
437
    let (_,fv,_) as d = descr p in
438
    let res = IdMap.map_from_slist (fun _ -> Types.Positive.forward ()) fv in
439 440
    memo_filter := MemoFilter.add (t,p) res !memo_filter;
    let r = filter_descr t (descr p) in
441
    IdMap.collide Types.Positive.define res r;
442 443 444 445 446
    r

let filter t p =
  let r = filter_node t p in
  memo_filter :=  MemoFilter.empty;
447
  IdMap.map Types.Positive.solve r
448 449 450 451 452
let filter_descr t p =
  let r = filter_descr t p in
  memo_filter :=  MemoFilter.empty;
  IdMap.get (IdMap.map Types.Positive.solve r)

453

454 455 456
(* Factorization of capture variables and constant patterns *)

module Factorize = struct
457 458
  module NodeTypeSet = Set.Make(Custom.Pair(Node)(Types))

459 460 461 462 463 464 465 466 467 468 469 470 471 472
  let pi1 ~kind t = Types.Product.pi1 (Types.Product.get ~kind t)
  let pi2 ~kind t = Types.Product.pi2 (Types.Product.get ~kind t)

(* Note: this is incomplete because of non-atomic constant patterns:
# debug approx (_,(x:=(1,2))) (1,2);;
[DEBUG:approx]
x=(1,2)
*)
  let rec approx_var seen ((a,fv,d) as p) t xs =
(*    assert (Types.subtype t a); 
      assert (IdSet.subset xs fv); *)
    if (IdSet.is_empty xs) || (Types.is_empty t) then xs
    else match d with
      | Cup ((a1,_,_) as p1,p2) ->
473
	  approx_var seen p2 (Types.diff t a1)
474 475 476 477 478 479 480 481 482 483 484 485 486 487 488 489 490 491 492 493 494 495 496
	    (approx_var seen p1 (Types.cap t a1) xs) 
      | Cap ((_,fv1,_) as p1,((_,fv2,_) as p2)) ->
	  IdSet.cup
	    (approx_var seen p1 t (IdSet.cap fv1 xs))
	    (approx_var seen p2 t (IdSet.cap fv2 xs))
      | Capture _ ->
	  xs
      | Constant (_,c) -> 
	  if (Types.subtype t (Types.constant c)) then xs else IdSet.empty
      | Times (q1,q2) ->
	  let xs = IdSet.cap xs (IdSet.cap q1.fv q2.fv) in
	  IdSet.cap
	    (approx_var_node seen q1 (pi1 ~kind:`Normal t) xs)
	    (approx_var_node seen q2 (pi2 ~kind:`Normal t) xs)
      | Xml (q1,q2) ->
	  let xs = IdSet.cap xs (IdSet.cap q1.fv q2.fv) in
	  IdSet.cap
	    (approx_var_node seen q1 (pi1 ~kind:`XML t) xs)
	    (approx_var_node seen q2 (pi2 ~kind:`XML t) xs)
      | Record _ -> IdSet.empty
      | _ -> assert false
	  
  and approx_var_node seen q t xs =
497
    if (NodeTypeSet.mem (q,t) seen) 
498
    then xs
499
    else approx_var (NodeTypeSet.add (q,t) seen) q.descr t xs
500
      
501 502

(* Obviously not complete ! *)      
503
  let rec approx_nil seen ((a,fv,d) as p) t xs =
504 505
    assert (Types.subtype t a); 
    assert (IdSet.subset xs fv);
506 507 508
    if (IdSet.is_empty xs) || (Types.is_empty t) then xs
    else match d with
      | Cup ((a1,_,_) as p1,p2) ->
509
	  approx_nil seen p2 (Types.diff t a1)
510 511 512 513 514 515 516 517 518 519 520 521
	    (approx_nil seen p1 (Types.cap t a1) xs) 
      | Cap ((_,fv1,_) as p1,((_,fv2,_) as p2)) ->
	  IdSet.cup
	    (approx_nil seen p1 t (IdSet.cap fv1 xs))
	    (approx_nil seen p2 t (IdSet.cap fv2 xs))
      | Constant (_,c) when Types.Const.equal c Sequence.nil_cst -> xs
      | Times (q1,q2) ->
	  let xs = IdSet.cap q2.fv (IdSet.diff xs q1.fv) in
	  approx_nil_node seen q2 (pi2 ~kind:`Normal t) xs
      | _ -> IdSet.empty
	  
  and approx_nil_node seen q t xs =
522
    if (NodeTypeSet.mem (q,t) seen) 
523
    then xs
524
    else approx_nil (NodeTypeSet.add (q,t) seen) q.descr t xs
525 526 527 528 529 530 531 532 533 534 535 536 537 538

  let cst ((a,_,_) as p) t xs =
    if IdSet.is_empty xs then IdMap.empty
    else
      let rec aux accu (x,t) =
	if (IdSet.mem xs x) then
	  match Sample.single_opt (Types.descr t) with
	    | Some c -> (x,c)::accu
	    | None -> accu
	else accu in
      let t = Types.cap t a in
      IdMap.from_list_disj (List.fold_left aux [] (filter_descr t p))
	
  let var ((a,_,_) as p) t = 
539
    approx_var NodeTypeSet.empty p (Types.cap t a)
540 541

  let nil ((a,_,_) as p) t = 
542
    approx_nil NodeTypeSet.empty p (Types.cap t a)
543 544 545 546 547
end




548
(* Normal forms for patterns and compilation *)
549

550 551
let min (a:int) (b:int) = if a < b then a else b

552 553
let any_basic = Types.Record.or_absent Types.non_constructed

554 555 556 557 558 559 560 561 562
let rec first_label (acc,fv,d) =
  if Types.is_empty acc 
  then LabelPool.dummy_max
  else match d with
    | Constr t -> Types.Record.first_label t
    | Cap (p,q) -> min (first_label p) (first_label q)
    | Cup ((acc1,_,_) as p,q) -> min (first_label p) (first_label q)
    | Record (l,p) -> l
    | _ -> LabelPool.dummy_max
563

564
module Normal = struct
565

566
  type source = 
567 568
    | SCatch | SConst of Types.const 
    | SLeft | SRight | SRecompose 
569
  type result = source id_map
570

571 572 573 574 575 576 577
  let compare_source s1 s2 =
    if s1 == s2 then 0 
    else match (s1,s2) with
      | SCatch, _ -> -1 | _, SCatch -> 1
      | SLeft, _ -> -1 | _, SLeft -> 1
      | SRight, _ -> -1 | _, SRight -> 1
      | SRecompose, _ -> -1 | _, SRecompose -> 1
578
      | SConst c1, SConst c2 -> Types.Const.compare c1 c2
579 580 581 582 583 584

  let hash_source = function
    | SCatch -> 1
    | SLeft -> 2
    | SRight -> 3
    | SRecompose -> 4
585
    | SConst c -> Types.Const.hash c
586 587 588 589 590 591 592 593
    
  let compare_result r1 r2 =
    IdMap.compare compare_source r1 r2

  let hash_result r =
    IdMap.hash hash_source r


594 595 596 597 598
  let print_result ppf r = Format.fprintf ppf "<result>"
  let print_result_option ppf = function
    | Some x -> Format.fprintf ppf "Some(%a)" print_result x
    | None -> Format.fprintf ppf "None"

599
  module NodeSet = SortedList.Make(Node)
600

601
  module Nnf = struct
602 603
    include Custom.Dummy

604 605 606 607 608 609 610 611 612 613 614 615 616 617
    type t = NodeSet.t * Types.t * IdSet.t (* pl,t;   t <= \accept{pl} *)
	
    let check (pl,t,xs) =
      List.iter (fun p -> assert(Types.subtype t (Types.descr p.accept)))
	(NodeSet.get pl)
    let print ppf (pl,t,xs) =
      Format.fprintf ppf "@[(pl=%a;t=%a)@]" NodeSet.dump pl Types.Print.print t
    let compare (l1,t1,xs1) (l2,t2,xs2) =
      let c = NodeSet.compare l1 l2 in if c <> 0 then c
      else let c = Types.compare t1 t2 in if c <> 0 then c
      else IdSet.compare xs1 xs2
    let hash (l,t,xs) = 
      (NodeSet.hash l) + 17 * (Types.hash t) + 257 * (IdSet.hash xs)
    let equal x y = compare x y == 0
618 619 620 621 622 623 624


    let first_label (pl,t,xs) = 
      List.fold_left
	(fun l p -> min l (first_label (descr p)))
	(Types.Record.first_label t)
	pl
625
  end
626

627 628 629 630 631 632 633 634 635 636
  module NBasic = struct
    include Custom.Dummy
    let serialize s _ = failwith "Patterns.NLineBasic.serialize"
    type t = result * Types.t
    let compare (r1,t1) (r2,t2) =
      let c = compare_result r1 r2 in if c <> 0 then c
      else Types.compare t1 t2
    let equal x y = compare x y == 0
    let hash (r,t) = hash_result r + 17 * Types.hash t
  end
637 638


639 640
  module NProd = struct
    type t = result * Nnf.t * Nnf.t
641

642 643 644 645 646 647
    let serialize s _ = failwith "Patterns.NLineProd.serialize"
    let deserialize s = failwith "Patterns.NLineProd.deserialize"
    let check x = ()
    let dump ppf (r,x,y) =
      Format.fprintf ppf "@[(result=%a;x=%a;y=%a)@]" 
	print_result r Nnf.print x Nnf.print y
648

649 650 651 652 653 654 655
    let compare (r1,x1,y1) (r2,x2,y2) =
      let c = compare_result r1 r2 in if c <> 0 then c
      else let c = Nnf.compare x1 x2 in if c <> 0 then c
      else Nnf.compare y1 y2
    let equal x y = compare x y == 0
    let hash (r,x,y) = hash_result r + 17 * (Nnf.hash x) + 267 * (Nnf.hash y)
  end
656

657 658
  module NLineBasic = SortedList.Make(NBasic)
  module NLineProd = SortedList.Make(NProd)
659

660
  type record =
661
    | RecNolabel of result option * result option
662
    | RecLabel of label * NLineProd.t
663
  type t = {
664
    nfv    : fv;
665 666 667 668
    na     : Types.t;
    nbasic : NLineBasic.t;
    nprod  : NLineProd.t;
    nxml   : NLineProd.t;
669
    nrecord: record
670
  }
671

672 673 674 675 676 677 678 679 680 681
  let print_record ppf = function
    | RecLabel (lab,l) ->
	Format.fprintf ppf "RecLabel(@[%a@],@ @[%a@])"
	  Label.print (LabelPool.value lab)
	  NLineProd.dump l
    | RecNolabel (a,b) -> 
	Format.fprintf ppf "RecNolabel(@[%a@],@[%a@])" 
	  print_result_option a
	  print_result_option b
  let print ppf nf =
682
    Format.fprintf ppf "@[NF{na=%a;@ @[nprod=@ @[%a@]@]};@ @[nrecord=@ @[%a@]@]}@]" 
683
      Types.Print.print nf.na
684
      NLineProd.dump nf.nprod
685 686 687
      print_record nf.nrecord
      

688 689 690 691 692 693 694 695 696 697 698 699 700 701 702 703 704
  include Custom.Dummy
  let compare_record t1 t2 = match t1,t2 with
    | RecNolabel (s1,n1), RecNolabel (s2,n2) ->
	(match (s1,s2,n1,n2) with
	   | Some r1, Some r2, _, _ -> compare_result r1 r2
	   | None, Some _, _, _ -> -1
	   | Some _, None, _, _ -> 1
	   | None,None,Some r1, Some r2 -> compare_result r1 r2
	   | None,None,None, Some _ -> -1
	   | None,None, Some _, None -> 1
	   | None,None, None, None -> 0)
    | RecNolabel (_,_), _ -> -1
    | _, RecNolabel (_,_) -> 1
    | RecLabel (l1,p1), RecLabel (l2,p2) ->
	let c = LabelPool.compare l1 l2 in if c <> 0 then c
	else NLineProd.compare p1 p2
  let compare t1 t2 =
705 706 707 708
    if t1 == t2 then 0
    else
      (* TODO: reorder; remove comparison of nfv ? *)
      let c = IdSet.compare t1.nfv t2.nfv in if c <> 0 then c 
709
      else let c = Types.compare t1.na t2.na in if c <> 0 then c
710 711 712
      else let c = NLineBasic.compare t1.nbasic t2.nbasic in if c <> 0 then c
      else let c = NLineProd.compare t1.nprod t2.nprod in if c <> 0 then c
      else let c = NLineProd.compare t1.nxml t2.nxml in if c <> 0 then c
713
      else compare_record t1.nrecord t2.nrecord
714

715
  let fus = IdMap.union_disj
716

717
  let nempty lab = 
718
    { nfv = IdSet.empty; 
719
      na = Types.empty;
720 721 722
      nbasic = NLineBasic.empty; 
      nprod = NLineProd.empty; 
      nxml = NLineProd.empty;
723
      nrecord = (match lab with 
724
		   | Some l -> RecLabel (l,NLineProd.empty)
725
		   | None -> RecNolabel (None,None))
726
    }
727
  let dummy = nempty None
728 729 730 731 732 733 734


  let ncup nf1 nf2 = 
    (* assert (Types.is_empty (Types.cap nf1.na nf2.na)); *)
    (* assert (nf1.nfv = nf2.nfv); *)
    { nfv = nf1.nfv;
      na      = Types.cup nf1.na nf2.na;
735 736 737
      nbasic  = NLineBasic.cup nf1.nbasic nf2.nbasic;
      nprod   = NLineProd.cup nf1.nprod nf2.nprod;
      nxml    = NLineProd.cup nf1.nxml nf2.nxml;
738
      nrecord = (match (nf1.nrecord,nf2.nrecord) with
739
		   | RecLabel (l1,r1), RecLabel (l2,r2) -> 
740 741
		       (* assert (l1 = l2); *) 
		       RecLabel (l1, NLineProd.cup r1 r2)
742
		   | RecNolabel (x1,y1), RecNolabel (x2,y2) -> 
743 744
		       RecNolabel((if x1 == None then x2 else x1),
				(if y1 == None then y2 else y1))
745
		   | _ -> assert false)
746 747 748
    }

  let double_fold f l1 l2 =
749 750 751 752 753 754
    List.fold_left 
      (fun accu x1 -> List.fold_left (fun accu x2 -> f accu x1 x2) accu l2)
      [] l1

  let double_fold_prod f l1 l2 =
    double_fold f (NLineProd.get l1) (NLineProd.get l2)
755 756
	 
  let ncap nf1 nf2 =
757
    let prod accu (res1,(pl1,t1,xs1),(ql1,s1,ys1)) (res2,(pl2,t2,xs2),(ql2,s2,ys2)) =
758 759 760 761
      let t = Types.cap t1 t2 in
      if Types.is_empty t then accu else
	let s = Types.cap s1 s2  in
	if Types.is_empty s then accu else
762 763 764
	  (fus res1 res2, 
	   (NodeSet.cup pl1 pl2, t, IdSet.cup xs1 xs2),
	   (NodeSet.cup ql1 ql2, s, IdSet.cup ys1 ys2)) 
765
	  :: accu
766 767 768 769 770 771
    in
    let basic accu (res1,t1) (res2,t2) =
      let t = Types.cap t1 t2 in
      if Types.is_empty t then accu else
	(fus res1 res2, t) :: accu
    in
772
    let record r1 r2 = match r1,r2 with
773
      | RecLabel (l1,r1), RecLabel (l2,r2) ->
774
	  (* assert (l1 = l2); *)
775
	  RecLabel(l1, NLineProd.from_list (double_fold_prod prod r1 r2))
776
      | RecNolabel (x1,y1), RecNolabel (x2,y2) ->
777 778 779 780 781 782
	  let x = match x1,x2 with 
	    | Some res1, Some res2 -> Some (fus res1 res2) 
	    | _ -> None
	  and y = match y1,y2 with
	    | Some res1, Some res2 -> Some (fus res1 res2)
	    | _ -> None in
783
	  RecNolabel (x,y)
784
      | _ -> assert false
785
    in
786
    { nfv = IdSet.cup nf1.nfv nf2.nfv;
787
      na = Types.cap nf1.na nf2.na;
788 789 790 791 792 793
      nbasic = NLineBasic.from_list (double_fold basic 
				       (NLineBasic.get nf1.nbasic) 
				       (NLineBasic.get nf2.nbasic));
      nprod = NLineProd.from_list (double_fold_prod prod nf1.nprod nf2.nprod);
      nxml = NLineProd.from_list (double_fold_prod prod nf1.nxml nf2.nxml);
      nrecord = record nf1.nrecord nf2.nrecord;
794 795
    }

796 797
  let nnode p xs = NodeSet.singleton p, Types.descr p.accept, xs
  let nc t = NodeSet.empty, t, IdSet.empty
798
  let ncany = nc Types.any
799
  let ncany_abs = nc Types.Record.any_or_absent
800

801
  let empty_res = IdMap.empty
802

803 804 805 806 807 808 809
  let single_basic src t = NLineBasic.singleton (src, t)
  let single_prod src p q = NLineProd.singleton (src, p,q)

  let ntimes lab acc p q xs = 
    let xsp = IdSet.cap xs p.fv and xsq = IdSet.cap xs q.fv in
    let src_p = IdMap.constant SLeft xsp
    and src_q = IdMap.constant SRight xsq in
810
    let src = IdMap.merge_elem SRecompose src_p src_q in 
811
    { (nempty lab) with 
812
	nfv = xs;
813
	na = acc;
814
	nprod = single_prod src (nnode p xsp) (nnode q xsq)
815 816
    }

817 818 819 820
  let nxml lab acc p q xs = 
    let xsp = IdSet.cap xs p.fv and xsq = IdSet.cap xs q.fv in
    let src_p = IdMap.constant SLeft xsp
    and src_q = IdMap.constant SRight xsq in
821
    let src = IdMap.merge_elem SRecompose src_p src_q in 
822
    { (nempty lab) with 
823
	nfv = xs;
824
	na = acc;
825
	nxml =  single_prod src (nnode p xsp) (nnode q xsq)
826 827
    }
    
828
  let nrecord lab acc l p xs =
829 830 831 832
    match lab with
      | None -> assert false
      | Some label ->
	  assert (label <= l);
833 834 835 836 837 838
	  let src,lft,rgt =
	    if l == label
	    then SLeft, nnode p xs, ncany
	    else SRight, ncany_abs, nnode (cons p.fv (record l p)) xs
	  in
	  let src = IdMap.constant src xs in
839
	  { (nempty lab) with
840 841 842
	      nfv = xs;
	      na = acc;
	      nrecord = RecLabel(label, single_prod src lft rgt) }
843 844

  let nconstr lab t =
845 846
    let aux l = NLineProd.from_list
		(List.map (fun (t1,t2) -> empty_res, nc t1,nc t2) l) in
847 848 849 850
    let record = match lab with
      | None ->
	  let (x,y) = Types.Record.empty_cases t in
	  RecNolabel ((if x then Some empty_res else None), 
851
		      (if y then Some empty_res else None))
852
      | Some l ->
853
	  RecLabel (l,aux (Types.Record.split_normal t l)) in
854
    { (nempty lab) with
855
	na = t;
856
	nbasic = single_basic empty_res (Types.cap t any_basic);
857 858 859
	nprod = aux (Types.Product.normal t);
	nxml  = aux (Types.Product.normal ~kind:`XML t);
	nrecord = record
860 861
    }

862 863
  let nany lab res =
    { nfv = IdMap.domain res;
864
      na = Types.any;
865 866 867
      nbasic = single_basic res any_basic;
      nprod  = single_prod res ncany ncany;
      nxml   = single_prod res ncany ncany;
868
      nrecord = match lab with
869 870
	| None -> RecNolabel (Some res, Some res)
	| Some lab -> RecLabel (lab, single_prod res ncany_abs ncany)
871 872
    }

873 874 875 876 877
  let nconstant lab x c = nany lab (IdMap.singleton x (SConst c))
  let ncapture lab x = nany lab (IdMap.singleton x SCatch)

  let rec nnormal lab ((acc,fv,d) as p) xs =
    let xs = IdSet.cap xs fv in
878
(*
879 880 881 882
    if not (IdSet.equal xs fv) then
      (Format.fprintf Format.std_formatter
	 "ERR: p=%a  xs=%a  fv=%a@." Print.print p Print.print_xs xs Print.print_xs fv;
       exit 1);
883
*)
884 885
    if Types.is_empty acc then nempty lab
    else if IdSet.is_empty xs then nconstr lab acc
886
    else match d with
887 888
      | Constr t -> assert false
      | Cap (p,q) -> ncap (nnormal lab p xs) (nnormal lab q xs)
889
      | Cup ((acc1,_,_) as p,q) -> 
890 891 892 893 894
	  ncup 
	    (nnormal lab p xs) 
	    (ncap (nnormal lab q xs) (nconstr lab (Types.neg acc1)))
      | Times (p,q) -> ntimes lab acc p q xs
      | Xml (p,q) -> nxml lab acc p q xs
895 896
      | Capture x -> ncapture lab x
      | Constant (x,c) -> nconstant lab x c
897
      | Record (l,p) -> nrecord lab acc l p xs
898
      | Dummy -> assert false
899 900 901 902 903

(*TODO: when an operand of Cap has its first_label > lab,
  directly shift it*)