text_formalization/general/lib.hl

   1 (* ========================================================================= *)
   2 (* Convenient library functions.                                             *)
   3 (*                                                                           *)
   4 (*       John Harrison, University of Cambridge Computer Laboratory          *)
   5 (*                                                                           *)
   6 (*            (c) Copyright, University of Cambridge 1998                    *)
   7 (*              (c) Copyright, John Harrison 1998-2007                       *)
   8 (* ========================================================================= *)
   9
  10 module Lib = struct
  11
  12 let fail() = failwith "";;
  13
  14 (* ------------------------------------------------------------------------- *)
  15 (* Combinators.                                                              *)
  16 (* ------------------------------------------------------------------------- *)
  17
  18 let curry f x y = f(x,y);;
  19
  20 let uncurry f(x,y) = f x y;;
  21
  22 let I x = x;;
  23
  24 let K x y = x;;
  25
  26 let C f x y = f y x;;
  27
  28 let W f x = f x x;;
  29
  30 let (o) = fun f g x -> f(g x);;
  31
  32 let (F_F) = fun f g (x,y) -> (f x,g y);;
  33
  34 (* ------------------------------------------------------------------------- *)
  35 (* List basics.                                                              *)
  36 (* ------------------------------------------------------------------------- *)
  37
  38 let hd l =
  39   match l with
  40    h::t -> h
  41   | _ -> failwith "hd";;
  42
  43 let tl l =
  44   match l with
  45    h::t -> t
  46   | _ -> failwith "tl";;
  47
  48 let map f =
  49   let rec mapf l =
  50     match l with
  51       [] -> []
  52     | (x::t) -> let y = f x in y::(mapf t) in
  53   mapf;;
  54
  55 let rec last l =
  56   match l with
  57     [x] -> x
  58   | (h::t) -> last t
  59   | [] -> failwith "last";;
  60
  61 let rec butlast l =
  62   match l with
  63     [_] -> []
  64   | (h::t) -> h::(butlast t)
  65   | [] -> failwith "butlast";;
  66
  67 let rec el n l =
  68   if n = 0 then hd l else el (n - 1) (tl l);;
  69
  70 let rev =
  71   let rec rev_append acc l =
  72     match l with
  73       [] -> acc
  74     | h::t -> rev_append (h::acc) t in
  75   fun l -> rev_append [] l;;
  76
  77 let rec map2 f l1 l2 =
  78   match (l1,l2) with
  79     [],[] -> []
  80   | (h1::t1),(h2::t2) -> let h = f h1 h2 in h::(map2 f t1 t2)
  81   | _ -> failwith "map2: length mismatch";;
  82
  83 (* ------------------------------------------------------------------------- *)
  84 (* Attempting function or predicate applications.                            *)
  85 (* ------------------------------------------------------------------------- *)
  86
  87 let can f x = try (f x; true) with Failure _ -> false;;
  88
  89 let check p x = if p x then x else failwith "check";;
  90
  91 (* ------------------------------------------------------------------------- *)
  92 (* Repetition of a function.                                                 *)
  93 (* ------------------------------------------------------------------------- *)
  94
  95 let rec funpow n f x =
  96   if n < 1 then x else funpow (n-1) f (f x);;
  97
  98 let rec repeat f x =
  99   try let y = f x in repeat f y with Failure _ -> x;;
 100
 101 (* ------------------------------------------------------------------------- *)
 102 (* To avoid consing in various situations, we propagate this exception.      *)
 103 (* I should probably eliminate this and use pointer EQ tests instead.        *)
 104 (* ------------------------------------------------------------------------- *)
 105
 106 exception Unchanged;;
 107
 108 (* ------------------------------------------------------------------------- *)
 109 (* Various versions of list iteration.                                       *)
 110 (* ------------------------------------------------------------------------- *)
 111
 112 let rec itlist f l b =
 113   match l with
 114     [] -> b
 115   | (h::t) -> f h (itlist f t b);;
 116
 117 let rec rev_itlist f l b =
 118   match l with
 119     [] -> b
 120   | (h::t) -> rev_itlist f t (f h b);;
 121
 122 let rec end_itlist f l =
 123   match l with
 124         []     -> failwith "end_itlist"
 125       | [x]    -> x
 126       | (h::t) -> f h (end_itlist f t);;
 127
 128 let rec itlist2 f l1 l2 b =
 129   match (l1,l2) with
 130     ([],[]) -> b
 131   | (h1::t1,h2::t2) -> f h1 h2 (itlist2 f t1 t2 b)
 132   | _ -> failwith "itlist2";;
 133
 134 let rec rev_itlist2 f l1 l2 b =
 135    match (l1,l2) with
 136      ([],[]) -> b
 137    | (h1::t1,h2::t2) -> rev_itlist2 f t1 t2 (f h1 h2 b)
 138       | _ -> failwith "rev_itlist2";;
 139
 140 (* ------------------------------------------------------------------------- *)
 141 (* Iterative splitting (list) and stripping (tree) via destructor.           *)
 142 (* ------------------------------------------------------------------------- *)
 143
 144 let rec splitlist dest x =
 145   try let l,r = dest x in
 146       let ls,res = splitlist dest r in
 147       (l::ls,res)
 148   with Failure _ -> ([],x);;
 149
 150 let rev_splitlist dest =
 151   let rec rsplist ls x =
 152     try let l,r = dest x in
 153         rsplist (r::ls) l
 154     with Failure _ -> (x,ls) in
 155   fun x -> rsplist [] x;;
 156
 157 let striplist dest =
 158   let rec strip x acc =
 159     try let l,r = dest x in
 160         strip l (strip r acc)
 161     with Failure _ -> x::acc in
 162   fun x -> strip x [];;
 163
 164 (* ------------------------------------------------------------------------- *)
 165 (* Apply a destructor as many times as elements in list.                     *)
 166 (* ------------------------------------------------------------------------- *)
 167
 168 let rec nsplit dest clist x =
 169   if clist = [] then [],x else
 170   let l,r = dest x in
 171   let ll,y = nsplit dest (tl clist) r in
 172   l::ll,y;;
 173
 174 (* ------------------------------------------------------------------------- *)
 175 (* Replication and sequences.                                                *)
 176 (* ------------------------------------------------------------------------- *)
 177
 178 let rec replicate x n =
 179     if n < 1 then []
 180     else x::(replicate x (n - 1));;
 181
 182 let rec (--) = fun m n -> if m > n then [] else m::((m + 1) -- n);;
 183
 184 (* ------------------------------------------------------------------------- *)
 185 (* Various useful list operations.                                           *)
 186 (* ------------------------------------------------------------------------- *)
 187
 188 let rec forall p l =
 189   match l with
 190     [] -> true
 191   | h::t -> p(h) & forall p t;;
 192
 193 let rec forall2 p l1 l2 =
 194   match (l1,l2) with
 195     [],[] -> true
 196   | (h1::t1,h2::t2) -> p h1 h2 & forall2 p t1 t2
 197   | _ -> false;;
 198
 199 let rec exists p l =
 200   match l with
 201     [] -> false
 202   | h::t -> p(h) or exists p t;;
 203
 204 let length =
 205   let rec len k l =
 206     if l = [] then k else len (k + 1) (tl l) in
 207   fun l -> len 0 l;;
 208
 209 let rec filter p l =
 210   match l with
 211     [] -> l
 212   | h::t -> let t' = filter p t in
 213             if p(h) then if t'==t then l else h::t'
 214             else t';;
 215
 216 let rec partition p l =
 217   match l with
 218     [] -> [],l
 219   | h::t -> let yes,no = partition p t in
 220             if p(h) then (if yes == t then l,[] else h::yes,no)
 221             else (if no == t then [],l else yes,h::no);;
 222
 223 let rec mapfilter f l =
 224   match l with
 225     [] -> []
 226   | (h::t) -> let rest = mapfilter f t in
 227               try (f h)::rest with Failure _ -> rest;;
 228
 229 let rec find p l =
 230   match l with
 231       [] -> failwith "find"
 232     | (h::t) -> if p(h) then h else find p t;;
 233
 234 let rec tryfind f l =
 235   match l with
 236       [] -> failwith "tryfind"
 237     | (h::t) -> try f h with Failure _ -> tryfind f t;;
 238
 239 let flat l = itlist (@) l [];;
 240
 241 let rec remove p l =
 242   match l with
 243     [] -> failwith "remove"
 244   | (h::t) -> if p(h) then h,t else
 245               let y,n = remove p t in y,h::n;;
 246
 247 let rec chop_list n l =
 248   if n = 0 then [],l else
 249   try let m,l' = chop_list (n-1) (tl l) in (hd l)::m,l'
 250   with Failure _ -> failwith "chop_list";;
 251
 252 let index x =
 253   let rec ind n l =
 254     match l with
 255       [] -> failwith "index"
 256     | (h::t) -> if Pervasives.compare x h = 0 then n else ind (n + 1) t in
 257   ind 0;;
 258
 259 (* ------------------------------------------------------------------------- *)
 260 (* "Set" operations on lists.                                                *)
 261 (* ------------------------------------------------------------------------- *)
 262
 263 let rec mem x lis =
 264   match lis with
 265     [] -> false
 266   | (h::t) -> Pervasives.compare x h = 0 or mem x t;;
 267
 268 let insert x l =
 269   if mem x l then l else x::l;;
 270
 271 let union l1 l2 = itlist insert l1 l2;;
 272
 273 let unions l = itlist union l [];;
 274
 275 let intersect l1 l2 = filter (fun x -> mem x l2) l1;;
 276
 277 let subtract l1 l2 = filter (fun x -> not (mem x l2)) l1;;
 278
 279 let subset l1 l2 = forall (fun t -> mem t l2) l1;;
 280
 281 let set_eq l1 l2 = subset l1 l2 & subset l2 l1;;
 282
 283 (* ------------------------------------------------------------------------- *)
 284 (* Association lists.                                                        *)
 285 (* ------------------------------------------------------------------------- *)
 286
 287 let rec assoc a l =
 288   match l with
 289     (x,y)::t -> if Pervasives.compare x a = 0 then y else assoc a t
 290   | [] -> failwith "find";;
 291
 292 let rec rev_assoc a l =
 293   match l with
 294     (x,y)::t -> if Pervasives.compare y a = 0 then x else rev_assoc a t
 295   | [] -> failwith "find";;
 296
 297 (* ------------------------------------------------------------------------- *)
 298 (* Zipping, unzipping etc.                                                   *)
 299 (* ------------------------------------------------------------------------- *)
 300
 301 let rec zip l1 l2 =
 302   match (l1,l2) with
 303         ([],[]) -> []
 304       | (h1::t1,h2::t2) -> (h1,h2)::(zip t1 t2)
 305       | _ -> failwith "zip";;
 306
 307 let rec unzip =
 308   function [] -> [],[]
 309          | ((a,b)::rest) -> let alist,blist = unzip rest in
 310                             (a::alist,b::blist);;
 311
 312 (* ------------------------------------------------------------------------- *)
 313 (* Sharing out a list according to pattern in list-of-lists.                 *)
 314 (* ------------------------------------------------------------------------- *)
 315
 316 let rec shareout pat all =
 317   if pat = [] then [] else
 318   let l,r = chop_list (length (hd pat)) all in
 319   l::(shareout (tl pat) r);;
 320
 321 (* ------------------------------------------------------------------------- *)
 322 (* Iterating functions over lists.                                           *)
 323 (* ------------------------------------------------------------------------- *)
 324
 325 let rec do_list f l =
 326   match l with
 327     [] -> ()
 328   | (h::t) -> (f h; do_list f t);;
 329
 330 (* ------------------------------------------------------------------------- *)
 331 (* Sorting.                                                                  *)
 332 (* ------------------------------------------------------------------------- *)
 333
 334 let rec sort cmp lis =
 335   match lis with
 336     [] -> []
 337   | piv::rest ->
 338       let r,l = partition (cmp piv) rest in
 339       (sort cmp l) @ (piv::(sort cmp r));;
 340
 341 (* ------------------------------------------------------------------------- *)
 342 (* Removing adjacent (NB!) equal elements from list.                         *)
 343 (* ------------------------------------------------------------------------- *)
 344
 345 let rec uniq l =
 346   match l with
 347     x::(y::_ as t) -> let t' = uniq t in
 348                       if Pervasives.compare x y = 0 then t' else
 349                       if t'==t then l else x::t'
 350  | _ -> l;;
 351
 352 (* ------------------------------------------------------------------------- *)
 353 (* Convert list into set by eliminating duplicates.                          *)
 354 (* ------------------------------------------------------------------------- *)
 355
 356 let setify s = uniq (sort (fun x y -> Pervasives.compare x y <= 0) s);;
 357
 358 (* ------------------------------------------------------------------------- *)
 359 (* String operations (surely there is a better way...)                       *)
 360 (* ------------------------------------------------------------------------- *)
 361
 362 let implode l = itlist (^) l "";;
 363
 364 let explode s =
 365   let rec exap n l =
 366       if n < 0 then l else
 367       exap (n - 1) ((String.sub s n 1)::l) in
 368   exap (String.length s - 1) [];;
 369
 370 (* ------------------------------------------------------------------------- *)
 371 (* Greatest common divisor.                                                  *)
 372 (* ------------------------------------------------------------------------- *)
 373
 374 let gcd =
 375   let rec gxd x y =
 376     if y = 0 then x else gxd y (x mod y) in
 377   fun x y -> let x' = abs x and y' = abs y in
 378               if x' < y' then gxd y' x' else gxd x' y';;
 379
 380 (* ------------------------------------------------------------------------- *)
 381 (* Some useful functions on "num" type.                                      *)
 382 (* ------------------------------------------------------------------------- *)
 383
 384 let num_0 = Int 0
 385 and num_1 = Int 1
 386 and num_2 = Int 2
 387 and num_10 = Int 10;;
 388
 389 let pow2 n = power_num num_2 (Int n);;
 390 let pow10 n = power_num num_10 (Int n);;
 391
 392 let numdom r =
 393   let r' = Ratio.normalize_ratio (ratio_of_num r) in
 394   num_of_big_int(Ratio.numerator_ratio r'),
 395   num_of_big_int(Ratio.denominator_ratio r');;
 396
 397 let numerator = fst o numdom
 398 and denominator = snd o numdom;;
 399
 400 let gcd_num n1 n2 =
 401   num_of_big_int(Big_int.gcd_big_int (big_int_of_num n1) (big_int_of_num n2));;
 402
 403 let lcm_num x y =
 404   if x =/ num_0 & y =/ num_0 then num_0
 405   else abs_num((x */ y) // gcd_num x y);;
 406
 407 (* ------------------------------------------------------------------------- *)
 408 (* All pairs arising from applying a function over two lists.                *)
 409 (* ------------------------------------------------------------------------- *)
 410
 411 let rec allpairs f l1 l2 =
 412   match l1 with
 413    h1::t1 ->  itlist (fun x a -> f h1 x :: a) l2 (allpairs f t1 l2)
 414   | [] -> [];;
 415
 416 (* ------------------------------------------------------------------------- *)
 417 (* Issue a report with a newline.                                            *)
 418 (* ------------------------------------------------------------------------- *)
 419
 420 let report s =
 421   Format.print_string s; Format.print_newline();;
 422
 423 (* ------------------------------------------------------------------------- *)
 424 (* Convenient function for issuing a warning.                                *)
 425 (* ------------------------------------------------------------------------- *)
 426
 427 let warn cond s =
 428   if cond then report ("Warning: "^s) else ();;
 429
 430 (* ------------------------------------------------------------------------- *)
 431 (* Flags to switch on verbose mode.                                          *)
 432 (* ------------------------------------------------------------------------- *)
 433
 434 let verbose = ref true;;
 435 let report_timing = ref true;;
 436
 437 (* ------------------------------------------------------------------------- *)
 438 (* Switchable version of "report".                                           *)
 439 (* ------------------------------------------------------------------------- *)
 440
 441 let remark s =
 442   if !verbose then report s else ();;
 443
 444 (* ------------------------------------------------------------------------- *)
 445 (* Time a function.                                                          *)
 446 (* ------------------------------------------------------------------------- *)
 447
 448 let time f x =
 449   if not (!report_timing) then f x else
 450   let start_time = Sys.time() in
 451   try let result = f x in
 452       let finish_time = Sys.time() in
 453       report("CPU time (user): "^(string_of_float(finish_time -. start_time)));
 454       result
 455   with e ->
 456       let finish_time = Sys.time() in
 457       Format.print_string("Failed after (user) CPU time of "^
 458                           (string_of_float(finish_time -. start_time))^": ");
 459       raise e;;
 460
 461 (* ------------------------------------------------------------------------- *)
 462 (* Versions of assoc and rev_assoc with default rather than failure.         *)
 463 (* ------------------------------------------------------------------------- *)
 464
 465 let rec assocd a l d =
 466   match l with
 467     [] -> d
 468   | (x,y)::t -> if Pervasives.compare x a = 0 then y else assocd a t d;;
 469
 470 let rec rev_assocd a l d =
 471   match l with
 472     [] -> d
 473   | (x,y)::t -> if Pervasives.compare y a = 0 then x else rev_assocd a t d;;
 474
 475 (* ------------------------------------------------------------------------- *)
 476 (* Version of map that avoids rebuilding unchanged subterms.                 *)
 477 (* ------------------------------------------------------------------------- *)
 478
 479 let rec qmap f l =
 480   match l with
 481     h::t -> let h' = f h and t' = qmap f t in
 482             if h' == h & t' == t then l else h'::t'
 483   | _ -> l;;
 484
 485 (* ------------------------------------------------------------------------- *)
 486 (* Merging and bottom-up mergesort.                                          *)
 487 (* ------------------------------------------------------------------------- *)
 488
 489 let rec merge ord l1 l2 =
 490   match l1 with
 491     [] -> l2
 492   | h1::t1 -> match l2 with
 493                 [] -> l1
 494               | h2::t2 -> if ord h1 h2 then h1::(merge ord t1 l2)
 495                           else h2::(merge ord l1 t2);;
 496
 497 let mergesort ord =
 498   let rec mergepairs l1 l2 =
 499     match (l1,l2) with
 500         ([s],[]) -> s
 501       | (l,[]) -> mergepairs [] l
 502       | (l,[s1]) -> mergepairs (s1::l) []
 503       | (l,(s1::s2::ss)) -> mergepairs ((merge ord s1 s2)::l) ss in
 504   fun l -> if l = [] then [] else mergepairs [] (map (fun x -> [x]) l);;
 505
 506 (* ------------------------------------------------------------------------- *)
 507 (* Common measure predicates to use with "sort".                             *)
 508 (* ------------------------------------------------------------------------- *)
 509
 510 let increasing f x y = Pervasives.compare (f x) (f y) < 0;;
 511
 512 let decreasing f x y = Pervasives.compare (f x) (f y) > 0;;
 513
 514 (* ------------------------------------------------------------------------- *)
 515 (* Polymorphic finite partial functions via Patricia trees.                  *)
 516 (*                                                                           *)
 517 (* The point of this strange representation is that it is canonical (equal   *)
 518 (* functions have the same encoding) yet reasonably efficient on average.    *)
 519 (*                                                                           *)
 520 (* Idea due to Diego Olivier Fernandez Pons (OCaml list, 2003/11/10).        *)
 521 (* ------------------------------------------------------------------------- *)
 522
 523 type ('a,'b)func =
 524    Empty
 525  | Leaf of int * ('a*'b)list
 526  | Branch of int * int * ('a,'b)func * ('a,'b)func;;
 527
 528 (* ------------------------------------------------------------------------- *)
 529 (* Undefined function.                                                       *)
 530 (* ------------------------------------------------------------------------- *)
 531
 532 let undefined = Empty;;
 533
 534 (* ------------------------------------------------------------------------- *)
 535 (* In case of equality comparison worries, better use this.                  *)
 536 (* ------------------------------------------------------------------------- *)
 537
 538 let is_undefined f =
 539   match f with
 540     Empty -> true
 541   | _ -> false;;
 542
 543 (* ------------------------------------------------------------------------- *)
 544 (* Operation analagous to "map" for lists.                                   *)
 545 (* ------------------------------------------------------------------------- *)
 546
 547 let mapf =
 548   let rec map_list f l =
 549     match l with
 550       [] -> []
 551     | (x,y)::t -> (x,f(y))::(map_list f t) in
 552   let rec mapf f t =
 553     match t with
 554       Empty -> Empty
 555     | Leaf(h,l) -> Leaf(h,map_list f l)
 556     | Branch(p,b,l,r) -> Branch(p,b,mapf f l,mapf f r) in
 557   mapf;;
 558
 559 (* ------------------------------------------------------------------------- *)
 560 (* Operations analogous to "fold" for lists.                                 *)
 561 (* ------------------------------------------------------------------------- *)
 562
 563 let foldl =
 564   let rec foldl_list f a l =
 565     match l with
 566       [] -> a
 567     | (x,y)::t -> foldl_list f (f a x y) t in
 568   let rec foldl f a t =
 569     match t with
 570       Empty -> a
 571     | Leaf(h,l) -> foldl_list f a l
 572     | Branch(p,b,l,r) -> foldl f (foldl f a l) r in
 573   foldl;;
 574
 575 let foldr =
 576   let rec foldr_list f l a =
 577     match l with
 578       [] -> a
 579     | (x,y)::t -> f x y (foldr_list f t a) in
 580   let rec foldr f t a =
 581     match t with
 582       Empty -> a
 583     | Leaf(h,l) -> foldr_list f l a
 584     | Branch(p,b,l,r) -> foldr f l (foldr f r a) in
 585   foldr;;
 586
 587 (* ------------------------------------------------------------------------- *)
 588 (* Mapping to sorted-list representation of the graph, domain and range.     *)
 589 (* ------------------------------------------------------------------------- *)
 590
 591 let graph f = setify (foldl (fun a x y -> (x,y)::a) [] f);;
 592
 593 let dom f = setify(foldl (fun a x y -> x::a) [] f);;
 594
 595 let ran f = setify(foldl (fun a x y -> y::a) [] f);;
 596
 597 (* ------------------------------------------------------------------------- *)
 598 (* Application.                                                              *)
 599 (* ------------------------------------------------------------------------- *)
 600
 601 let applyd =
 602   let rec apply_listd l d x =
 603     match l with
 604       (a,b)::t -> let c = Pervasives.compare x a in
 605                   if c = 0 then b else if c > 0 then apply_listd t d x else d x
 606     | [] -> d x in
 607   fun f d x ->
 608     let k = Hashtbl.hash x in
 609     let rec look t =
 610       match t with
 611         Leaf(h,l) when h = k -> apply_listd l d x
 612       | Branch(p,b,l,r) when (k lxor p) land (b - 1) = 0
 613                 -> look (if k land b = 0 then l else r)
 614       | _ -> d x in
 615     look f;;
 616
 617 let apply f = applyd f (fun x -> failwith "apply");;
 618
 619 let tryapplyd f a d = applyd f (fun x -> d) a;;
 620
 621 let defined f x = try apply f x; true with Failure _ -> false;;
 622
 623 (* ------------------------------------------------------------------------- *)
 624 (* Undefinition.                                                             *)
 625 (* ------------------------------------------------------------------------- *)
 626
 627 let undefine =
 628   let rec undefine_list x l =
 629     match l with
 630       (a,b as ab)::t ->
 631           let c = Pervasives.compare x a in
 632           if c = 0 then t
 633           else if c < 0 then l else
 634           let t' = undefine_list x t in
 635           if t' == t then l else ab::t'
 636     | [] -> [] in
 637   fun x ->
 638     let k = Hashtbl.hash x in
 639     let rec und t =
 640       match t with
 641         Leaf(h,l) when h = k ->
 642           let l' = undefine_list x l in
 643           if l' == l then t
 644           else if l' = [] then Empty
 645           else Leaf(h,l')
 646       | Branch(p,b,l,r) when k land (b - 1) = p ->
 647           if k land b = 0 then
 648             let l' = und l in
 649             if l' == l then t
 650             else (match l' with Empty -> r | _ -> Branch(p,b,l',r))
 651           else
 652             let r' = und r in
 653             if r' == r then t
 654             else (match r' with Empty -> l | _ -> Branch(p,b,l,r'))
 655       | _ -> t in
 656     und;;
 657
 658 (* ------------------------------------------------------------------------- *)
 659 (* Redefinition and combination.                                             *)
 660 (* ------------------------------------------------------------------------- *)
 661
 662 let (|->),combine =
 663   let newbranch p1 t1 p2 t2 =
 664     let zp = p1 lxor p2 in
 665     let b = zp land (-zp) in
 666     let p = p1 land (b - 1) in
 667     if p1 land b = 0 then Branch(p,b,t1,t2)
 668     else Branch(p,b,t2,t1) in
 669   let rec define_list (x,y as xy) l =
 670     match l with
 671       (a,b as ab)::t ->
 672           let c = Pervasives.compare x a in
 673           if c = 0 then xy::t
 674           else if c < 0 then xy::l
 675           else ab::(define_list xy t)
 676     | [] -> [xy]
 677   and combine_list op z l1 l2 =
 678     match (l1,l2) with
 679       [],_ -> l2
 680     | _,[] -> l1
 681     | ((x1,y1 as xy1)::t1,(x2,y2 as xy2)::t2) ->
 682           let c = Pervasives.compare x1 x2 in
 683           if c < 0 then xy1::(combine_list op z t1 l2)
 684           else if c > 0 then xy2::(combine_list op z l1 t2) else
 685           let y = op y1 y2 and l = combine_list op z t1 t2 in
 686           if z(y) then l else (x1,y)::l in
 687   let (|->) x y =
 688     let k = Hashtbl.hash x in
 689     let rec upd t =
 690       match t with
 691         Empty -> Leaf (k,[x,y])
 692       | Leaf(h,l) ->
 693            if h = k then Leaf(h,define_list (x,y) l)
 694            else newbranch h t k (Leaf(k,[x,y]))
 695       | Branch(p,b,l,r) ->
 696           if k land (b - 1) <> p then newbranch p t k (Leaf(k,[x,y]))
 697           else if k land b = 0 then Branch(p,b,upd l,r)
 698           else Branch(p,b,l,upd r) in
 699     upd in
 700   let rec combine op z t1 t2 =
 701     match (t1,t2) with
 702       Empty,_ -> t2
 703     | _,Empty -> t1
 704     | Leaf(h1,l1),Leaf(h2,l2) ->
 705           if h1 = h2 then
 706             let l = combine_list op z l1 l2 in
 707             if l = [] then Empty else Leaf(h1,l)
 708           else newbranch h1 t1 h2 t2
 709     | (Leaf(k,lis) as lf),(Branch(p,b,l,r) as br) ->
 710           if k land (b - 1) = p then
 711             if k land b = 0 then
 712               (match combine op z lf l with
 713                  Empty -> r | l' -> Branch(p,b,l',r))
 714             else
 715               (match combine op z lf r with
 716                  Empty -> l | r' -> Branch(p,b,l,r'))
 717           else
 718             newbranch k lf p br
 719     | (Branch(p,b,l,r) as br),(Leaf(k,lis) as lf) ->
 720           if k land (b - 1) = p then
 721             if k land b = 0 then
 722               (match combine op z l lf with
 723                 Empty -> r | l' -> Branch(p,b,l',r))
 724             else
 725               (match combine op z r lf with
 726                  Empty -> l | r' -> Branch(p,b,l,r'))
 727           else
 728             newbranch p br k lf
 729     | Branch(p1,b1,l1,r1),Branch(p2,b2,l2,r2) ->
 730           if b1 < b2 then
 731             if p2 land (b1 - 1) <> p1 then newbranch p1 t1 p2 t2
 732             else if p2 land b1 = 0 then
 733               (match combine op z l1 t2 with
 734                  Empty -> r1 | l -> Branch(p1,b1,l,r1))
 735             else
 736               (match combine op z r1 t2 with
 737                  Empty -> l1 | r -> Branch(p1,b1,l1,r))
 738           else if b2 < b1 then
 739             if p1 land (b2 - 1) <> p2 then newbranch p1 t1 p2 t2
 740             else if p1 land b2 = 0 then
 741               (match combine op z t1 l2 with
 742                  Empty -> r2 | l -> Branch(p2,b2,l,r2))
 743             else
 744               (match combine op z t1 r2 with
 745                  Empty -> l2 | r -> Branch(p2,b2,l2,r))
 746           else if p1 = p2 then
 747            (match (combine op z l1 l2,combine op z r1 r2) with
 748               (Empty,r) -> r | (l,Empty) -> l | (l,r) -> Branch(p1,b1,l,r))
 749           else
 750             newbranch p1 t1 p2 t2 in
 751   (|->),combine;;
 752
 753 (* ------------------------------------------------------------------------- *)
 754 (* Special case of point function.                                           *)
 755 (* ------------------------------------------------------------------------- *)
 756
 757 let (|=>) = fun x y -> (x |-> y) undefined;;
 758
 759 (* ------------------------------------------------------------------------- *)
 760 (* Grab an arbitrary element.                                                *)
 761 (* ------------------------------------------------------------------------- *)
 762
 763 let rec choose t =
 764   match t with
 765     Empty -> failwith "choose: completely undefined function"
 766   | Leaf(h,l) -> hd l
 767   | Branch(b,p,t1,t2) -> choose t1;;
 768
 769 (* ------------------------------------------------------------------------- *)
 770 (* Install a trivial printer for the general polymorphic case.               *)
 771 (* ------------------------------------------------------------------------- *)
 772
 773 (* let print_fpf (f:('a,'b)func) = Format.print_string "<func>";;
 774
 775 #install_printer print_fpf;;
 776 *)
 777
 778 (* ------------------------------------------------------------------------- *)
 779 (* Set operations parametrized by equality (from Steven Obua).               *)
 780 (* ------------------------------------------------------------------------- *)
 781
 782 let rec mem' eq =
 783   let rec mem x lis =
 784     match lis with
 785       [] -> false
 786     | (h::t) -> eq x h or mem x t
 787   in mem;;
 788
 789 let insert' eq x l =
 790   if mem' eq x l then l else x::l;;
 791
 792 let union' eq l1 l2 = itlist (insert' eq) l1 l2;;
 793
 794 let unions' eq l = itlist (union' eq) l [];;
 795
 796 let subtract' eq l1 l2 = filter (fun x -> not (mem' eq x l2)) l1;;
 797
 798 (* ------------------------------------------------------------------------- *)
 799 (* Accepts decimal, hex or binary numeral, using C notation 0x... for hex    *)
 800 (* and analogous 0b... for binary.                                           *)
 801 (* ------------------------------------------------------------------------- *)
 802
 803 let num_of_string =
 804   let values =
 805    ["0",0; "1",1; "2",2; "3",3; "4",4;
 806     "5",5; "6",6; "7",7; "8",8; "9",9;
 807     "a",10; "A",10; "b",11; "B",11;
 808     "c",12; "C",12; "d",13; "D",13;
 809     "e",14; "E",14; "f",15; "F",15] in
 810   let valof b s =
 811     let v = Int(assoc s values) in
 812     if v </ b then v else failwith "num_of_string: invalid digit for base"
 813   and two = num_2 and ten = num_10 and sixteen = Int 16 in
 814   let rec num_of_stringlist b l =
 815     match l with
 816       [] -> failwith "num_of_string: no digits after base indicator"
 817     | [h] -> valof b h
 818     | h::t -> valof b h +/ b */ num_of_stringlist b t in
 819   fun s ->
 820     match explode(s) with
 821         [] -> failwith "num_of_string: no digits"
 822       | "0"::"x"::hexdigits -> num_of_stringlist sixteen (rev hexdigits)
 823       | "0"::"b"::bindigits -> num_of_stringlist two (rev bindigits)
 824       | decdigits -> num_of_stringlist ten (rev decdigits);;
 825
 826 (* ------------------------------------------------------------------------- *)
 827 (* Convenient conversion between files and (lists of) strings.               *)
 828 (* ------------------------------------------------------------------------- *)
 829
 830 let strings_of_file filename =
 831   let fd = try Pervasives.open_in filename
 832            with Sys_error _ ->
 833              failwith("strings_of_file: can't open "^filename) in
 834   let rec suck_lines acc =
 835     try let l = Pervasives.input_line fd in
 836         suck_lines (l::acc)
 837     with End_of_file -> rev acc in
 838   let data = suck_lines [] in
 839   (Pervasives.close_in fd; data);;
 840
 841 let string_of_file filename =
 842   end_itlist (fun s t -> s^"\n"^t) (strings_of_file filename);;
 843
 844 let file_of_string filename s =
 845   let fd = Pervasives.open_out filename in
 846   output_string fd s; close_out fd;;
 847
 848 end;;