ata.ml

   1 (* Todo refactor and remove this alias *)
   2 INCLUDE "debug.ml"
   3 module Tree = Tree.Binary
   4
   5 let gen_id =
   6   let id = ref (-1) in
   7     fun () -> incr id;!id
   8
   9
  10 module State = struct
  11
  12   type t = int
  13   let mk = gen_id
  14
  15 end
  16 let mk_state = State.mk
  17
  18 type state = State.t
  19
  20 type predicate = [ `Left of (Tree.t -> bool) | `Right of (Tree.t -> bool) |
  21                        `True
  22                  ]
  23
  24 let eval_pred t =
  25   function `True -> true
  26     | `Left f | `Right f -> f t
  27
  28 type formula_expr =
  29   | False | True
  30   | Or of formula * formula
  31   | And of formula * formula
  32   | Atom of ([ `Left | `Right ]*bool*state)
  33 and formula = { fid: int;
  34                 pos : formula_expr;
  35                 neg : formula;
  36                 st : Ptset.t*Ptset.t;
  37                 size: int;
  38               }
  39
  40
  41 module FormNode =
  42 struct
  43   type t = formula
  44   let hash = function
  45     | False -> 0
  46     | True -> 1
  47     | And(f1,f2) -> 2+17*f1.fid + 37*f2.fid
  48     | Or(f1,f2) -> 3+101*f1.fid + 253*f2.fid
  49     | Atom(d,b,s) -> 5+(if d=`Left then 11 else 19)*(if b then 23 else 31)*s
  50
  51   let hash t = (hash t.pos) land max_int
  52
  53   let equal f1 f2 =
  54     match f1.pos,f2.pos with
  55       | False,False | True,True -> true
  56       | Atom(d1,b1,s1), Atom(d2,b2,s2) when (d1 = d2) && (b1=b2) &&(s1=s2) -> true
  57       | Or(g1,g2),Or(h1,h2)
  58       | And(g1,g2),And(h1,h2)  -> g1.fid == h1.fid && g2.fid == h2.fid
  59       | _ -> false
  60 end
  61 module WH = Weak.Make(FormNode)
  62
  63 let f_pool = WH.create 107
  64
  65 let true_,false_ =
  66   let rec t = { fid = 1; pos = True; neg = f ; st = Ptset.empty,Ptset.empty; size =1; }
  67   and f = { fid = 0; pos = False; neg = t; st = Ptset.empty,Ptset.empty; size = 1; }
  68   in
  69     WH.add f_pool f;
  70     WH.add f_pool t;
  71     t,f
  72
  73 let is_true f = f.fid == 1
  74 let is_false f = f.fid == 0
  75
  76
  77 let cons pos neg s1 s2 size1 size2 =
  78   let rec pnode =
  79     { fid = gen_id ();
  80       pos = pos;
  81       neg = nnode;
  82       st = s1;
  83       size = size1;}
  84   and nnode = {
  85     fid = gen_id ();
  86     pos = neg;
  87     neg = pnode;
  88     st = s2;
  89     size = size2;
  90   }
  91   in
  92     (WH.merge f_pool pnode),(WH.merge f_pool nnode)
  93
  94 let atom_  d p s =
  95   let si = Ptset.singleton s in
  96   let ss = match d with
  97     | `Left -> si,Ptset.empty
  98     | `Right -> Ptset.empty,si
  99   in fst (cons (Atom(d,p,s)) (Atom(d,not p,s)) ss ss 1 1)
 100
 101 let merge_states f1 f2 =
 102   let sp =
 103     Ptset.union (fst f1.st) (fst f2.st),
 104     Ptset.union (snd f1.st) (snd f2.st)
 105   and sn =
 106     Ptset.union (fst f1.neg.st) (fst f2.neg.st),
 107     Ptset.union (snd f1.neg.st) (snd f2.neg.st)
 108   in
 109     sp,sn
 110
 111 let full_or_ f1 f2 =
 112   let f1,f2 = if f1.fid < f2.fid then f2,f1 else f1,f2 in
 113   let sp,sn = merge_states f1 f2 in
 114   let psize = f1.size + f2.size in
 115   let nsize = f1.neg.size + f2.neg.size in
 116     fst (cons (Or(f1,f2)) (And(f1.neg,f2.neg)) sp sn psize nsize )
 117
 118 let or_ f1 f2 =
 119   let f1,f2 = if f1.fid < f2.fid then f2,f1 else f1,f2 in
 120   if is_true f1 || is_true f2 then true_
 121   else if is_false f1 && is_false f2 then false_
 122   else if is_false f1 then f2
 123   else if is_false f2 then f1
 124   else
 125     let psize = f1.size + f2.size in
 126     let nsize = f1.neg.size + f2.neg.size in
 127     let sp,sn = merge_states f1 f2 in
 128       fst (cons (Or(f1,f2)) (And(f1.neg,f2.neg)) sp sn psize nsize)
 129
 130
 131
 132 let and_ f1 f2 =
 133   let f1,f2 = if f1.fid < f2.fid then f2,f1 else f1,f2 in
 134   if is_true f1 && is_true f2 then true_
 135   else if is_false f1 || is_false f2 then false_
 136   else if is_true f1 then f2
 137   else if is_true f2 then f1
 138   else
 139     let psize = f1.size + f2.size in
 140     let nsize = f1.neg.size + f2.neg.size in
 141     let sp,sn = merge_states f1 f2 in
 142       fst (cons (And(f1,f2)) (Or(f1.neg,f2.neg)) sp sn psize nsize)
 143
 144
 145 let not_ f = f.neg
 146
 147
 148 module HTagSetKey =
 149 struct
 150   type t = Ptset.t*Tag.t
 151   let int_hash key = key lsl 31 lor (key lsl 8)
 152   let equal (s1,s2) (t1,t2) = Tag.equal s2 t2 &&  Ptset.equal s1 t1
 153   let hash (s,t) = int_hash (Ptset.hash s) lxor ( int_hash (Tag.hash t))
 154 end
 155 module HTagSet = Hashtbl.Make(HTagSetKey)
 156
 157 type t = {
 158     id : int;
 159     mutable states : Ptset.t;
 160     init : Ptset.t;
 161     mutable final : Ptset.t;
 162     universal : Ptset.t;
 163     (* Transitions of the Alternating automaton *)
 164     phi : (state,(TagSet.t*(bool*formula*predicate)) list) Hashtbl.t;
 165     delta : (state*Tag.t, (bool*formula*predicate)) Hashtbl.t;
 166 (*    delta : (state,(bool*formula*predicate) TagMap.t) Hashtbl.t; *)
 167     sigma : (bool*formula*(predicate list*predicate list)*bool) HTagSet.t;
 168   }
 169
 170   module Pair (X : Set.OrderedType) (Y : Set.OrderedType) =
 171   struct
 172     type t = X.t*Y.t
 173     let compare (x1,y1) (x2,y2) =
 174       let r = X.compare x1 x2 in
 175         if r == 0 then Y.compare y1 y2
 176         else r
 177   end
 178
 179   module PL = Set.Make (Pair (Ptset) (Ptset))
 180
 181
 182       let pr_st ppf l = Format.fprintf ppf "{";
 183     begin
 184       match l with
 185         |       [] -> ()
 186         | [s] -> Format.fprintf ppf " %i" s
 187         | p::r -> Format.fprintf ppf " %i" p;
 188             List.iter (fun i -> Format.fprintf ppf "; %i" i) r
 189     end;
 190     Format.fprintf ppf " }"
 191   let rec pr_frm ppf f = match f.pos with
 192     | True -> Format.fprintf ppf "⊤"
 193     | False -> Format.fprintf ppf "⊥"
 194     | And(f1,f2) ->
 195         Format.fprintf ppf "(";
 196         (pr_frm ppf f1);
 197         Format.fprintf ppf ") ∧ (";
 198         (pr_frm ppf f2);
 199         Format.fprintf ppf ")"
 200     | Or(f1,f2) ->
 201         (pr_frm ppf f1);
 202         Format.fprintf ppf " ∨ ";
 203         (pr_frm ppf f2);
 204     | Atom(dir,b,s) -> Format.fprintf ppf "%s%s[%i]"
 205         (if b then "" else "¬")
 206         (if dir = `Left then "↓₁" else "↓₂") s
 207
 208   let dnf_hash = Hashtbl.create 17
 209
 210   let rec dnf_aux f = match f.pos with
 211     | False -> PL.empty
 212     | True -> PL.singleton (Ptset.empty,Ptset.empty)
 213     | Atom(`Left,_,s) -> PL.singleton (Ptset.singleton s,Ptset.empty)
 214     | Atom(`Right,_,s) -> PL.singleton (Ptset.empty,Ptset.singleton s)
 215     | Or(f1,f2) -> PL.union (dnf f1) (dnf f2)
 216     | And(f1,f2) ->
 217           let pl1 = dnf f1
 218           and pl2 = dnf f2
 219           in
 220             PL.fold (fun (s1,s2) acc ->
 221                        PL.fold ( fun (s1', s2') acc' ->
 222                                    (PL.add
 223                                       ((Ptset.union s1 s1'),
 224                                        (Ptset.union s2 s2')) acc') )
 225                           pl2 acc )
 226               pl1 PL.empty
 227
 228
 229   and dnf f =
 230     try
 231       Hashtbl.find dnf_hash f.fid
 232     with
 233         Not_found ->
 234           let d = dnf_aux f in
 235             Hashtbl.add dnf_hash f.fid d;d
 236
 237
 238   let can_top_down f =
 239     let nf = dnf f in
 240       if (PL.cardinal nf > 3)then None
 241       else match PL.elements nf with
 242         | [(s1,s2); (t1,t2); (u1,u2)] when
 243             Ptset.is_empty s1 && Ptset.is_empty s2 && Ptset.is_empty t1 && Ptset.is_empty u2
 244               -> Some(true,t2,u1)
 245         | [(t1,t2); (u1,u2)] when Ptset.is_empty t1 && Ptset.is_empty u2
 246             -> Some(false,t2,u1)
 247         | _ -> None
 248
 249
 250   let equal_form f1 f2 =
 251     (f1.fid == f2.fid) || (FormNode.equal f1 f2) || (PL.equal (dnf f1) (dnf f2))
 252
 253   let dump ppf a =
 254     Format.fprintf ppf "Automaton (%i) :\n" a.id;
 255     Format.fprintf ppf "States : "; pr_st ppf (Ptset.elements a.states);
 256     Format.fprintf ppf "\nInitial states : "; pr_st ppf (Ptset.elements a.init);
 257     Format.fprintf ppf "\nFinal states : "; pr_st ppf (Ptset.elements a.final);
 258     Format.fprintf ppf "\nUniversal states : "; pr_st ppf (Ptset.elements a.universal);
 259     Format.fprintf ppf "\nAlternating transitions :\n------------------------------\n";
 260     let l = Hashtbl.fold (fun k t acc ->
 261                             (List.map (fun (t,(m,f,p)) -> (t,k),(m,f,p)) t)@ acc) a.phi [] in
 262     let l = List.sort (fun ((tsx,x),_) ((tsy,y),_) -> if x-y == 0 then TagSet.compare tsx tsy else x-y) l in
 263     List.iter (fun ((ts,q),(b,f,_)) ->
 264
 265                     let s =
 266                       if TagSet.is_finite ts
 267                       then "{" ^ (TagSet.fold (fun t a -> a ^ " " ^ (Tag.to_string t)) ts "") ^"}"
 268                       else let cts = TagSet.neg ts in
 269                         if TagSet.is_empty cts then "*" else
 270                           (TagSet.fold (fun t a -> a ^ " " ^ (Tag.to_string t)) cts "*\\{"
 271                           )^ "}"
 272                     in
 273                       Format.fprintf ppf "(%s,%i) %s " s q (if b then "=>" else "->");
 274                       pr_frm ppf f;
 275                       Format.fprintf ppf "\n")l;
 276
 277     Format.fprintf ppf "NFA transitions :\n------------------------------\n";
 278     HTagSet.iter (fun (qs,t) (b,f,_,_) ->
 279                     pr_st ppf (Ptset.elements qs);
 280                     Format.fprintf ppf ",%s  %s " (Tag.to_string t) (if b then "=>" else "->");
 281                     pr_frm ppf f;
 282                     Format.fprintf ppf "(fid=%i) left=" f.fid;
 283                     let l,r = f.st in pr_st ppf (Ptset.elements l);
 284                       Format.fprintf ppf ", right=";
 285                       pr_st ppf (Ptset.elements r);
 286                       Format.fprintf ppf "\n";
 287                  ) a.sigma;
 288     Format.fprintf ppf "=======================================\n"
 289
 290   module Transitions = struct
 291     type t = state*TagSet.t*bool*formula*predicate
 292     let ( ?< ) x = x
 293     let ( >< ) state (l,b) = state,(l,b,`True)
 294     let ( ><@ ) state (l,b,p) = state,(l,b,p)
 295     let ( >=> ) (state,(label,mark,pred)) form = (state,label,mark,form,pred)
 296     let ( +| ) f1 f2 = or_ f1 f2
 297     let ( *& ) f1 f2 = and_ f1 f2
 298     let ( ** ) d s = atom_ d true s
 299
 300
 301   end
 302   type transition = Transitions.t
 303
 304   let equal_trans (q1,t1,m1,f1,_) (q2,t2,m2,f2,_) =
 305     (q1 == q2) && (TagSet.equal t1 t2) && (m1 == m2) && (equal_form f1 f2)
 306
 307   module TS =
 308   struct
 309     type node = Nil | Cons of Tree.t * node | Concat of node*node
 310     and t = { node : node; size : int }
 311     let node n s = { node=n; size = s }
 312
 313     let empty = node Nil 0
 314
 315     let cons e t = node (Cons(e,t.node)) (t.size+1)
 316     let concat t1 t2 = node (Concat (t1.node,t2.node)) (t1.size+t2.size)
 317     let append e t = concat t (cons e empty)
 318
 319     let to_list_rev t =
 320       let rec aux acc l rest =
 321         match l with
 322           | Nil -> begin
 323               match rest with
 324                 | Nil -> acc
 325                 | Cons(e,t) -> aux (e::acc) t Nil
 326                 | Concat(t1,t2) -> aux acc t1 t2
 327             end
 328           | Cons(e,r) -> aux (e::acc) r rest
 329           | Concat(t1,t2) -> aux acc t1 (Concat(t2,rest))
 330       in
 331     aux [] t.node Nil
 332     let length = function { size = s } -> s
 333
 334     let iter f { node = n } =
 335       let rec loop = function
 336         | Nil -> ()
 337         | Cons(e,n) -> let _ = f e in loop n
 338         | Concat(n1,n2) -> let _ = loop n1 in loop n2
 339       in loop n
 340
 341   end
 342
 343
 344   module BottomUpNew = struct
 345
 346 IFDEF DEBUG
 347 THEN
 348     type trace =
 349       | TNil of Ptset.t*Ptset.t
 350       | TNode of Ptset.t*Ptset.t*bool* (int*bool*formula) list
 351
 352     let traces = Hashtbl.create 17
 353     let dump_trace t =
 354       let out = open_out "debug_trace.dot"
 355       in
 356       let outf = Format.formatter_of_out_channel out in
 357
 358       let rec aux t num =
 359         if Tree.is_node t
 360         then
 361           match (try Hashtbl.find traces (Tree.id t) with Not_found -> TNil(Ptset.empty,Ptset.empty)) with
 362             | TNode(r,s,mark,trs) ->
 363                 let numl = aux (Tree.left t) num in
 364                 let numr = aux (Tree.right t) (numl+1) in
 365                 let mynum = numr + 1 in
 366                   Format.fprintf outf "n%i [ label=\"<%s>\\nr=" mynum (Tag.to_string (Tree.tag t));
 367                   pr_st outf (Ptset.elements r);
 368                   Format.fprintf outf "\\ns=";
 369                   pr_st outf (Ptset.elements s);
 370                   List.iter (fun (q,m,f) ->
 371                                Format.fprintf outf "\\n%i %s" q (if m then "⇨" else "→");
 372                                pr_frm outf f ) trs;
 373                   Format.fprintf outf "\", %s shape=box ];\n"
 374                     (if mark then "color=cyan1, style=filled," else "");
 375                   let _ = Format.fprintf outf "n%i -> n%i;\n" mynum numl in
 376                   let _ = Format.fprintf outf "n%i -> n%i;\n" mynum numr in
 377                   mynum
 378             | TNil(r,s) -> Format.fprintf outf "n%i [ shape=box, label=\"Nil\\nr=" num;
 379                 pr_st outf (Ptset.elements r);
 380                 Format.fprintf outf "\\ns=";
 381                 pr_st outf (Ptset.elements s);
 382                 Format.fprintf outf "\"];\n";num
 383         else
 384           match Hashtbl.find traces (-10) with
 385             | TNil(r,s) ->
 386                 Format.fprintf outf "n%i [ shape=box, label=\"Nil\\nr=" num;
 387                 pr_st outf (Ptset.elements r);
 388                 Format.fprintf outf "\\ns=";
 389                 pr_st outf (Ptset.elements s);
 390                 Format.fprintf outf "\"];\n";
 391                 num
 392             | _ -> assert false
 393
 394       in
 395         Format.fprintf outf "digraph G {\n";
 396         ignore(aux t 0);
 397         Format.fprintf outf "}\n%!";
 398         close_out out;
 399         ignore(Sys.command "dot -Tsvg debug_trace.dot > debug_trace.svg")
 400 END
 401
 402
 403
 404     module HFEval = Hashtbl.Make(
 405       struct
 406         type t = int*Ptset.t*Ptset.t
 407         let equal (a,b,c) (d,e,f) =
 408           a==d && (Ptset.equal b e) && (Ptset.equal c f)
 409         let hash (a,b,c) =
 410           a+17*(Ptset.hash b) + 31*(Ptset.hash c)
 411       end)
 412
 413     let hfeval = HFEval.create 4097
 414
 415
 416     let eval_form_bool f s1 s2 =
 417       let rec eval f = match f.pos with
 418         | Atom(`Left,b,q) -> if b == (Ptset.mem q s1) then (true,true,false) else false,false,false
 419         | Atom(`Right,b,q) -> if b == (Ptset.mem q s2) then (true,false,true) else false,false,false
 420             (* test some inlining *)
 421         | True -> true,true,true
 422         | False -> false,false,false
 423         | _ ->
 424             try
 425               HFEval.find hfeval (f.fid,s1,s2)
 426             with
 427               | Not_found -> let r =
 428                   match f.pos with
 429                     | Or(f1,f2) ->
 430                         let b1,rl1,rr1 = eval f1
 431                         in
 432                           if b1 && rl1 && rr1 then (true,true,true)
 433                           else
 434                             let b2,rl2,rr2 = eval f2
 435                             in
 436                             let rl1,rr1 = if b1 then rl1,rr1 else false,false
 437                             and rl2,rr2 = if b2 then rl2,rr2 else false,false
 438                             in (b1 || b2, rl1||rl2,rr1||rr2)
 439                     | And(f1,f2) ->
 440                         let b1,rl1,rr1 = eval f1 in
 441                           if b1 && rl1 && rr1 then (true,true,true)
 442                           else if b1
 443                           then let b2,rl2,rr2 = eval f2 in
 444                             if b2 then (true,rl1||rl2,rr1||rr2)
 445                             else (false,false,false)
 446                           else (false,false,false)
 447                     | _ -> assert false
 448                 in
 449                   HFEval.add hfeval (f.fid,s1,s2) r;
 450                   r
 451       in eval f
 452
 453
 454     module HFEvalDir = Hashtbl.Make(
 455       struct
 456         type t = int*Ptset.t*[`Left | `Right ]
 457         let equal (a,b,c) (d,e,f) =
 458           a==d && (Ptset.equal b e) && (c = f)
 459         let hash_dir = function `Left -> 7919
 460           | `Right -> 3517
 461
 462         let hash (a,b,c) =
 463           a+17*(Ptset.hash b) + 31*(hash_dir c)
 464       end)
 465
 466     let hfeval_dir = HFEvalDir.create 4097
 467
 468
 469     let eval_dir dir f s =
 470       let rec eval f = match f.pos with
 471         | Atom(d,b,q) when d = dir -> if b == (Ptset.mem q s) then true_ else false_
 472         | Atom(_,b,q) -> f
 473             (* test some inlining *)
 474         | True -> true_
 475         | False -> false_
 476         | _ ->
 477             try
 478               HFEvalDir.find hfeval_dir (f.fid,s,dir)
 479             with
 480               | Not_found ->
 481                   let r =
 482                     match f.pos with
 483                       | Or(f1,f2) ->
 484                           let f1 = eval f1
 485                           in
 486                             if is_true f1 then true_
 487                             else if is_false f1 then eval f2
 488                             else or_ f1 f2
 489                       | And(f1,f2) ->
 490                           let f1 = eval f1 in
 491                             if is_false f1 then false_
 492                             else if is_true f1 then eval f2
 493                             else and_ f1 f2
 494                       | _ -> assert false
 495                   in
 496                     HFEvalDir.add hfeval_dir (f.fid,s,dir) r;
 497                     r
 498
 499       in eval f
 500
 501
 502
 503     let fstate_pool = Hashtbl.create 11
 504
 505     let merge_pred a b = match a,b with
 506       | Some(f1), Some(f2) -> Some(fun x -> f1 x || f2 x)
 507       | None,None -> None
 508       | None,Some(_) -> b
 509       | Some(_),None -> a
 510
 511     let acc_pred p l1 l2 = match p with
 512       | `Left _ -> p::l1,l2
 513       | `Right _ -> l1,p::l2
 514       | _ -> l1,l2
 515
 516
 517     let merge_trans t a tag q acc =
 518       List.fold_left (fun (accf,accm,acchtrue) (ts,(m,f,pred)) ->
 519                         if TagSet.mem tag ts
 520                         then
 521                           let tmpf,hastrue =
 522                             if is_true f then
 523                               let newfinal =
 524                                 try Hashtbl.find fstate_pool f.fid with
 525                                   | Not_found -> let s = mk_state() in
 526                                       a.states <- Ptset.add s a.states;
 527                                       a.final <- Ptset.add s a.final;
 528                                       Hashtbl.add fstate_pool f.fid s;s
 529                               in
 530                                 (atom_ `Left true newfinal),true
 531                             else f,false in
 532                             (or_ tmpf accf,accm||m,acchtrue||hastrue)
 533                         else (accf,accm,acchtrue)
 534                      ) acc (Hashtbl.find a.phi q)
 535
 536     let miss = ref 0
 537     let call = ref 0
 538     let get_trans t a tag r =
 539       try
 540         let mark,f,predl,has_true =
 541           HTagSet.find a.sigma (r,tag)
 542         in f.st,f,mark,has_true,r,predl
 543       with
 544           Not_found ->
 545             let f,mark,has_true,accq =
 546               Ptset.fold (fun q (accf,accm,acchtrue,accq) ->
 547                             let naccf,naccm,nacctrue =
 548                               merge_trans t a tag q (accf,accm,acchtrue )
 549                             in
 550                               if is_false naccf then (naccf,naccm,nacctrue,accq)
 551                               else (naccf,naccm,nacctrue,Ptset.add q accq)
 552                          )
 553                 r (false_,false,false,Ptset.empty)
 554             in
 555               HTagSet.add a.sigma (accq,tag) (mark,f,([],[]),has_true);
 556               f.st,f,mark,has_true,accq,([],[])
 557
 558
 559     let check_pred l t = true (*l = [] ||
 560       List.exists (function p ->
 561                      match p with
 562                          `Left f | `Right f -> f t
 563                        | _ -> assert false) l
 564                               *)
 565
 566
 567     let rec accepting_among2 a t r acc =
 568       let orig = r in
 569       let rest = Ptset.inter r a.final in
 570       let r = Ptset.diff r rest in
 571         if Ptset.is_empty r then rest,acc else
 572           if (not (Tree.is_node t))
 573           then
 574               orig,acc
 575           else
 576             let tag = Tree.tag t in
 577             let t1 = Tree.first_child t
 578             and t2 = Tree.next_sibling t in
 579             let (r1,r2),formula,mark,has_true,r,_ = get_trans t a tag r
 580             in
 581             let s1,res1 = accepting_among2 a t1 r1 acc
 582             in
 583             let formula = eval_dir `Left formula s1 in
 584               if is_false formula then rest,acc
 585               else
 586                 if is_true formula then (* tail call equivalent to a top down *)
 587                   accepting_among2 a t2 orig (if mark then TS.append t res1 else res1)
 588                 else
 589                   let s2,res2 = accepting_among2 a t2 r2 res1
 590                   in
 591                   let formula = eval_dir `Right formula s2
 592                   in
 593                     if is_false formula then rest,res1
 594                     else
 595                       orig,(if mark then TS.append t (res2)
 596                             else res2)
 597
 598
 599     let run a t =
 600       let st,res = accepting_among2 a t a.init TS.empty in
 601       let b = Ptset.is_empty (st) in
 602         if b then TS.empty
 603         else
 604           res
 605   end