1 (* ========================================================================= *)
2 (* Convenient library functions. *)
4 (* John Harrison, University of Cambridge Computer Laboratory *)
6 (* (c) Copyright, University of Cambridge 1998 *)
7 (* (c) Copyright, John Harrison 1998-2007 *)
8 (* ========================================================================= *)
10 let fail() = failwith "";;
12 (* ------------------------------------------------------------------------- *)
14 (* ------------------------------------------------------------------------- *)
16 let curry f x y = f(x,y);;
18 let uncurry f(x,y) = f x y;;
28 let (o) = fun f g x -> f(g x);;
30 let (F_F) = fun f g (x,y) -> (f x,g y);;
32 (* ------------------------------------------------------------------------- *)
34 (* ------------------------------------------------------------------------- *)
39 | _ -> failwith "hd";;
44 | _ -> failwith "tl";;
50 | (x::t) -> let y = f x in y::(mapf t) in
57 | [] -> failwith "last";;
62 | (h::t) -> h::(butlast t)
63 | [] -> failwith "butlast";;
66 if n = 0 then hd l else el (n - 1) (tl l);;
69 let rec rev_append acc l =
72 | h::t -> rev_append (h::acc) t in
73 fun l -> rev_append [] l;;
75 let rec map2 f l1 l2 =
78 | (h1::t1),(h2::t2) -> let h = f h1 h2 in h::(map2 f t1 t2)
79 | _ -> failwith "map2: length mismatch";;
81 (* ------------------------------------------------------------------------- *)
82 (* Attempting function or predicate applications. *)
83 (* ------------------------------------------------------------------------- *)
85 let can f x = try (f x; true) with Failure _ -> false;;
87 let check p x = if p x then x else failwith "check";;
89 (* ------------------------------------------------------------------------- *)
90 (* Repetition of a function. *)
91 (* ------------------------------------------------------------------------- *)
93 let rec funpow n f x =
94 if n < 1 then x else funpow (n-1) f (f x);;
97 try let y = f x in repeat f y with Failure _ -> x;;
99 (* ------------------------------------------------------------------------- *)
100 (* To avoid consing in various situations, we propagate this exception. *)
101 (* I should probably eliminate this and use pointer EQ tests instead. *)
102 (* ------------------------------------------------------------------------- *)
104 exception Unchanged;;
106 (* ------------------------------------------------------------------------- *)
107 (* Various versions of list iteration. *)
108 (* ------------------------------------------------------------------------- *)
110 let rec itlist f l b =
113 | (h::t) -> f h (itlist f t b);;
115 let rec rev_itlist f l b =
118 | (h::t) -> rev_itlist f t (f h b);;
120 let rec end_itlist f l =
122 [] -> failwith "end_itlist"
124 | (h::t) -> f h (end_itlist f t);;
126 let rec itlist2 f l1 l2 b =
129 | (h1::t1,h2::t2) -> f h1 h2 (itlist2 f t1 t2 b)
130 | _ -> failwith "itlist2";;
132 let rec rev_itlist2 f l1 l2 b =
135 | (h1::t1,h2::t2) -> rev_itlist2 f t1 t2 (f h1 h2 b)
136 | _ -> failwith "rev_itlist2";;
138 (* ------------------------------------------------------------------------- *)
139 (* Iterative splitting (list) and stripping (tree) via destructor. *)
140 (* ------------------------------------------------------------------------- *)
142 let rec splitlist dest x =
143 try let l,r = dest x in
144 let ls,res = splitlist dest r in
146 with Failure _ -> ([],x);;
148 let rev_splitlist dest =
149 let rec rsplist ls x =
150 try let l,r = dest x in
152 with Failure _ -> (x,ls) in
153 fun x -> rsplist [] x;;
156 let rec strip x acc =
157 try let l,r = dest x in
158 strip l (strip r acc)
159 with Failure _ -> x::acc in
160 fun x -> strip x [];;
162 (* ------------------------------------------------------------------------- *)
163 (* Apply a destructor as many times as elements in list. *)
164 (* ------------------------------------------------------------------------- *)
166 let rec nsplit dest clist x =
167 if clist = [] then [],x else
169 let ll,y = nsplit dest (tl clist) r in
172 (* ------------------------------------------------------------------------- *)
173 (* Replication and sequences. *)
174 (* ------------------------------------------------------------------------- *)
176 let rec replicate x n =
178 else x::(replicate x (n - 1));;
180 let rec (--) = fun m n -> if m > n then [] else m::((m + 1) -- n);;
182 (* ------------------------------------------------------------------------- *)
183 (* Various useful list operations. *)
184 (* ------------------------------------------------------------------------- *)
189 | h::t -> p(h) & forall p t;;
191 let rec forall2 p l1 l2 =
194 | (h1::t1,h2::t2) -> p h1 h2 & forall2 p t1 t2
200 | h::t -> p(h) or exists p t;;
204 if l = [] then k else len (k + 1) (tl l) in
210 | h::t -> let t' = filter p t in
211 if p(h) then if t'==t then l else h::t'
214 let rec partition p l =
217 | h::t -> let yes,no = partition p t in
218 if p(h) then (if yes == t then l,[] else h::yes,no)
219 else (if no == t then [],l else yes,h::no);;
221 let rec mapfilter f l =
224 | (h::t) -> let rest = mapfilter f t in
225 try (f h)::rest with Failure _ -> rest;;
229 [] -> failwith "find"
230 | (h::t) -> if p(h) then h else find p t;;
232 let rec tryfind f l =
234 [] -> failwith "tryfind"
235 | (h::t) -> try f h with Failure _ -> tryfind f t;;
237 let flat l = itlist (@) l [];;
241 [] -> failwith "remove"
242 | (h::t) -> if p(h) then h,t else
243 let y,n = remove p t in y,h::n;;
245 let rec chop_list n l =
246 if n = 0 then [],l else
247 try let m,l' = chop_list (n-1) (tl l) in (hd l)::m,l'
248 with Failure _ -> failwith "chop_list";;
253 [] -> failwith "index"
254 | (h::t) -> if Pervasives.compare x h = 0 then n else ind (n + 1) t in
257 (* ------------------------------------------------------------------------- *)
258 (* "Set" operations on lists. *)
259 (* ------------------------------------------------------------------------- *)
264 | (h::t) -> Pervasives.compare x h = 0 or mem x t;;
267 if mem x l then l else x::l;;
269 let union l1 l2 = itlist insert l1 l2;;
271 let unions l = itlist union l [];;
273 let intersect l1 l2 = filter (fun x -> mem x l2) l1;;
275 let subtract l1 l2 = filter (fun x -> not (mem x l2)) l1;;
277 let subset l1 l2 = forall (fun t -> mem t l2) l1;;
279 let set_eq l1 l2 = subset l1 l2 & subset l2 l1;;
281 (* ------------------------------------------------------------------------- *)
282 (* Association lists. *)
283 (* ------------------------------------------------------------------------- *)
287 (x,y)::t -> if Pervasives.compare x a = 0 then y else assoc a t
288 | [] -> failwith "find";;
290 let rec rev_assoc a l =
292 (x,y)::t -> if Pervasives.compare y a = 0 then x else rev_assoc a t
293 | [] -> failwith "find";;
295 (* ------------------------------------------------------------------------- *)
296 (* Zipping, unzipping etc. *)
297 (* ------------------------------------------------------------------------- *)
302 | (h1::t1,h2::t2) -> (h1,h2)::(zip t1 t2)
303 | _ -> failwith "zip";;
307 | ((a,b)::rest) -> let alist,blist = unzip rest in
308 (a::alist,b::blist);;
310 (* ------------------------------------------------------------------------- *)
311 (* Sharing out a list according to pattern in list-of-lists. *)
312 (* ------------------------------------------------------------------------- *)
314 let rec shareout pat all =
315 if pat = [] then [] else
316 let l,r = chop_list (length (hd pat)) all in
317 l::(shareout (tl pat) r);;
319 (* ------------------------------------------------------------------------- *)
320 (* Iterating functions over lists. *)
321 (* ------------------------------------------------------------------------- *)
323 let rec do_list f l =
326 | (h::t) -> (f h; do_list f t);;
328 (* ------------------------------------------------------------------------- *)
330 (* ------------------------------------------------------------------------- *)
332 let rec sort cmp lis =
336 let r,l = partition (cmp piv) rest in
337 (sort cmp l) @ (piv::(sort cmp r));;
339 (* ------------------------------------------------------------------------- *)
340 (* Removing adjacent (NB!) equal elements from list. *)
341 (* ------------------------------------------------------------------------- *)
345 x::(y::_ as t) -> let t' = uniq t in
346 if Pervasives.compare x y = 0 then t' else
347 if t'==t then l else x::t'
350 (* ------------------------------------------------------------------------- *)
351 (* Convert list into set by eliminating duplicates. *)
352 (* ------------------------------------------------------------------------- *)
354 let setify s = uniq (sort (fun x y -> Pervasives.compare x y <= 0) s);;
356 (* ------------------------------------------------------------------------- *)
357 (* String operations (surely there is a better way...) *)
358 (* ------------------------------------------------------------------------- *)
360 let implode l = itlist (^) l "";;
365 exap (n - 1) ((String.sub s n 1)::l) in
366 exap (String.length s - 1) [];;
368 (* ------------------------------------------------------------------------- *)
369 (* Greatest common divisor. *)
370 (* ------------------------------------------------------------------------- *)
374 if y = 0 then x else gxd y (x mod y) in
375 fun x y -> let x' = abs x and y' = abs y in
376 if x' < y' then gxd y' x' else gxd x' y';;
378 (* ------------------------------------------------------------------------- *)
379 (* Some useful functions on "num" type. *)
380 (* ------------------------------------------------------------------------- *)
385 and num_10 = Int 10;;
387 let pow2 n = power_num num_2 (Int n);;
388 let pow10 n = power_num num_10 (Int n);;
391 let r' = Ratio.normalize_ratio (ratio_of_num r) in
392 num_of_big_int(Ratio.numerator_ratio r'),
393 num_of_big_int(Ratio.denominator_ratio r');;
395 let numerator = fst o numdom
396 and denominator = snd o numdom;;
399 num_of_big_int(Big_int.gcd_big_int (big_int_of_num n1) (big_int_of_num n2));;
402 if x =/ num_0 & y =/ num_0 then num_0
403 else abs_num((x */ y) // gcd_num x y);;
405 (* ------------------------------------------------------------------------- *)
406 (* All pairs arising from applying a function over two lists. *)
407 (* ------------------------------------------------------------------------- *)
409 let rec allpairs f l1 l2 =
411 h1::t1 -> itlist (fun x a -> f h1 x :: a) l2 (allpairs f t1 l2)
414 (* ------------------------------------------------------------------------- *)
415 (* Issue a report with a newline. *)
416 (* ------------------------------------------------------------------------- *)
419 Format.print_string s; Format.print_newline();;
421 (* ------------------------------------------------------------------------- *)
422 (* Convenient function for issuing a warning. *)
423 (* ------------------------------------------------------------------------- *)
426 if cond then report ("Warning: "^s) else ();;
428 (* ------------------------------------------------------------------------- *)
429 (* Flags to switch on verbose mode. *)
430 (* ------------------------------------------------------------------------- *)
432 let verbose = ref true;;
433 let report_timing = ref true;;
435 (* ------------------------------------------------------------------------- *)
436 (* Switchable version of "report". *)
437 (* ------------------------------------------------------------------------- *)
440 if !verbose then report s else ();;
442 (* ------------------------------------------------------------------------- *)
443 (* Time a function. *)
444 (* ------------------------------------------------------------------------- *)
447 if not (!report_timing) then f x else
448 let start_time = Sys.time() in
449 try let result = f x in
450 let finish_time = Sys.time() in
451 report("CPU time (user): "^(string_of_float(finish_time -. start_time)));
454 let finish_time = Sys.time() in
455 Format.print_string("Failed after (user) CPU time of "^
456 (string_of_float(finish_time -. start_time))^": ");
459 (* ------------------------------------------------------------------------- *)
460 (* Versions of assoc and rev_assoc with default rather than failure. *)
461 (* ------------------------------------------------------------------------- *)
463 let rec assocd a l d =
466 | (x,y)::t -> if Pervasives.compare x a = 0 then y else assocd a t d;;
468 let rec rev_assocd a l d =
471 | (x,y)::t -> if Pervasives.compare y a = 0 then x else rev_assocd a t d;;
473 (* ------------------------------------------------------------------------- *)
474 (* Version of map that avoids rebuilding unchanged subterms. *)
475 (* ------------------------------------------------------------------------- *)
479 h::t -> let h' = f h and t' = qmap f t in
480 if h' == h & t' == t then l else h'::t'
483 (* ------------------------------------------------------------------------- *)
484 (* Merging and bottom-up mergesort. *)
485 (* ------------------------------------------------------------------------- *)
487 let rec merge ord l1 l2 =
490 | h1::t1 -> match l2 with
492 | h2::t2 -> if ord h1 h2 then h1::(merge ord t1 l2)
493 else h2::(merge ord l1 t2);;
496 let rec mergepairs l1 l2 =
499 | (l,[]) -> mergepairs [] l
500 | (l,[s1]) -> mergepairs (s1::l) []
501 | (l,(s1::s2::ss)) -> mergepairs ((merge ord s1 s2)::l) ss in
502 fun l -> if l = [] then [] else mergepairs [] (map (fun x -> [x]) l);;
504 (* ------------------------------------------------------------------------- *)
505 (* Common measure predicates to use with "sort". *)
506 (* ------------------------------------------------------------------------- *)
508 let increasing f x y = Pervasives.compare (f x) (f y) < 0;;
510 let decreasing f x y = Pervasives.compare (f x) (f y) > 0;;
512 (* ------------------------------------------------------------------------- *)
513 (* Polymorphic finite partial functions via Patricia trees. *)
515 (* The point of this strange representation is that it is canonical (equal *)
516 (* functions have the same encoding) yet reasonably efficient on average. *)
518 (* Idea due to Diego Olivier Fernandez Pons (OCaml list, 2003/11/10). *)
519 (* ------------------------------------------------------------------------- *)
523 | Leaf of int * ('a*'b)list
524 | Branch of int * int * ('a,'b)func * ('a,'b)func;;
526 (* ------------------------------------------------------------------------- *)
527 (* Undefined function. *)
528 (* ------------------------------------------------------------------------- *)
530 let undefined = Empty;;
532 (* ------------------------------------------------------------------------- *)
533 (* In case of equality comparison worries, better use this. *)
534 (* ------------------------------------------------------------------------- *)
541 (* ------------------------------------------------------------------------- *)
542 (* Operation analagous to "map" for lists. *)
543 (* ------------------------------------------------------------------------- *)
546 let rec map_list f l =
549 | (x,y)::t -> (x,f(y))::(map_list f t) in
553 | Leaf(h,l) -> Leaf(h,map_list f l)
554 | Branch(p,b,l,r) -> Branch(p,b,mapf f l,mapf f r) in
557 (* ------------------------------------------------------------------------- *)
558 (* Operations analogous to "fold" for lists. *)
559 (* ------------------------------------------------------------------------- *)
562 let rec foldl_list f a l =
565 | (x,y)::t -> foldl_list f (f a x y) t in
566 let rec foldl f a t =
569 | Leaf(h,l) -> foldl_list f a l
570 | Branch(p,b,l,r) -> foldl f (foldl f a l) r in
574 let rec foldr_list f l a =
577 | (x,y)::t -> f x y (foldr_list f t a) in
578 let rec foldr f t a =
581 | Leaf(h,l) -> foldr_list f l a
582 | Branch(p,b,l,r) -> foldr f l (foldr f r a) in
585 (* ------------------------------------------------------------------------- *)
586 (* Mapping to sorted-list representation of the graph, domain and range. *)
587 (* ------------------------------------------------------------------------- *)
589 let graph f = setify (foldl (fun a x y -> (x,y)::a) [] f);;
591 let dom f = setify(foldl (fun a x y -> x::a) [] f);;
593 let ran f = setify(foldl (fun a x y -> y::a) [] f);;
595 (* ------------------------------------------------------------------------- *)
597 (* ------------------------------------------------------------------------- *)
600 let rec apply_listd l d x =
602 (a,b)::t -> let c = Pervasives.compare x a in
603 if c = 0 then b else if c > 0 then apply_listd t d x else d x
606 let k = Hashtbl.hash x in
609 Leaf(h,l) when h = k -> apply_listd l d x
610 | Branch(p,b,l,r) when (k lxor p) land (b - 1) = 0
611 -> look (if k land b = 0 then l else r)
615 let apply f = applyd f (fun x -> failwith "apply");;
617 let tryapplyd f a d = applyd f (fun x -> d) a;;
619 let defined f x = try apply f x; true with Failure _ -> false;;
621 (* ------------------------------------------------------------------------- *)
623 (* ------------------------------------------------------------------------- *)
626 let rec undefine_list x l =
629 let c = Pervasives.compare x a in
631 else if c < 0 then l else
632 let t' = undefine_list x t in
633 if t' == t then l else ab::t'
636 let k = Hashtbl.hash x in
639 Leaf(h,l) when h = k ->
640 let l' = undefine_list x l in
642 else if l' = [] then Empty
644 | Branch(p,b,l,r) when k land (b - 1) = p ->
648 else (match l' with Empty -> r | _ -> Branch(p,b,l',r))
652 else (match r' with Empty -> l | _ -> Branch(p,b,l,r'))
656 (* ------------------------------------------------------------------------- *)
657 (* Redefinition and combination. *)
658 (* ------------------------------------------------------------------------- *)
661 let newbranch p1 t1 p2 t2 =
662 let zp = p1 lxor p2 in
663 let b = zp land (-zp) in
664 let p = p1 land (b - 1) in
665 if p1 land b = 0 then Branch(p,b,t1,t2)
666 else Branch(p,b,t2,t1) in
667 let rec define_list (x,y as xy) l =
670 let c = Pervasives.compare x a in
672 else if c < 0 then xy::l
673 else ab::(define_list xy t)
675 and combine_list op z l1 l2 =
679 | ((x1,y1 as xy1)::t1,(x2,y2 as xy2)::t2) ->
680 let c = Pervasives.compare x1 x2 in
681 if c < 0 then xy1::(combine_list op z t1 l2)
682 else if c > 0 then xy2::(combine_list op z l1 t2) else
683 let y = op y1 y2 and l = combine_list op z t1 t2 in
684 if z(y) then l else (x1,y)::l in
686 let k = Hashtbl.hash x in
689 Empty -> Leaf (k,[x,y])
691 if h = k then Leaf(h,define_list (x,y) l)
692 else newbranch h t k (Leaf(k,[x,y]))
694 if k land (b - 1) <> p then newbranch p t k (Leaf(k,[x,y]))
695 else if k land b = 0 then Branch(p,b,upd l,r)
696 else Branch(p,b,l,upd r) in
698 let rec combine op z t1 t2 =
702 | Leaf(h1,l1),Leaf(h2,l2) ->
704 let l = combine_list op z l1 l2 in
705 if l = [] then Empty else Leaf(h1,l)
706 else newbranch h1 t1 h2 t2
707 | (Leaf(k,lis) as lf),(Branch(p,b,l,r) as br) ->
708 if k land (b - 1) = p then
710 (match combine op z lf l with
711 Empty -> r | l' -> Branch(p,b,l',r))
713 (match combine op z lf r with
714 Empty -> l | r' -> Branch(p,b,l,r'))
717 | (Branch(p,b,l,r) as br),(Leaf(k,lis) as lf) ->
718 if k land (b - 1) = p then
720 (match combine op z l lf with
721 Empty -> r | l' -> Branch(p,b,l',r))
723 (match combine op z r lf with
724 Empty -> l | r' -> Branch(p,b,l,r'))
727 | Branch(p1,b1,l1,r1),Branch(p2,b2,l2,r2) ->
729 if p2 land (b1 - 1) <> p1 then newbranch p1 t1 p2 t2
730 else if p2 land b1 = 0 then
731 (match combine op z l1 t2 with
732 Empty -> r1 | l -> Branch(p1,b1,l,r1))
734 (match combine op z r1 t2 with
735 Empty -> l1 | r -> Branch(p1,b1,l1,r))
737 if p1 land (b2 - 1) <> p2 then newbranch p1 t1 p2 t2
738 else if p1 land b2 = 0 then
739 (match combine op z t1 l2 with
740 Empty -> r2 | l -> Branch(p2,b2,l,r2))
742 (match combine op z t1 r2 with
743 Empty -> l2 | r -> Branch(p2,b2,l2,r))
745 (match (combine op z l1 l2,combine op z r1 r2) with
746 (Empty,r) -> r | (l,Empty) -> l | (l,r) -> Branch(p1,b1,l,r))
748 newbranch p1 t1 p2 t2 in
751 (* ------------------------------------------------------------------------- *)
752 (* Special case of point function. *)
753 (* ------------------------------------------------------------------------- *)
755 let (|=>) = fun x y -> (x |-> y) undefined;;
757 (* ------------------------------------------------------------------------- *)
758 (* Grab an arbitrary element. *)
759 (* ------------------------------------------------------------------------- *)
763 Empty -> failwith "choose: completely undefined function"
765 | Branch(b,p,t1,t2) -> choose t1;;
767 (* ------------------------------------------------------------------------- *)
768 (* Install a trivial printer for the general polymorphic case. *)
769 (* ------------------------------------------------------------------------- *)
771 let print_fpf (f:('a,'b)func) = Format.print_string "<func>";;
773 #install_printer print_fpf;;
775 (* ------------------------------------------------------------------------- *)
776 (* Set operations parametrized by equality (from Steven Obua). *)
777 (* ------------------------------------------------------------------------- *)
783 | (h::t) -> eq x h or mem x t
787 if mem' eq x l then l else x::l;;
789 let union' eq l1 l2 = itlist (insert' eq) l1 l2;;
791 let unions' eq l = itlist (union' eq) l [];;
793 let subtract' eq l1 l2 = filter (fun x -> not (mem' eq x l2)) l1;;
795 (* ------------------------------------------------------------------------- *)
796 (* Accepts decimal, hex or binary numeral, using C notation 0x... for hex *)
797 (* and analogous 0b... for binary. *)
798 (* ------------------------------------------------------------------------- *)
802 ["0",0; "1",1; "2",2; "3",3; "4",4;
803 "5",5; "6",6; "7",7; "8",8; "9",9;
804 "a",10; "A",10; "b",11; "B",11;
805 "c",12; "C",12; "d",13; "D",13;
806 "e",14; "E",14; "f",15; "F",15] in
808 let v = Int(assoc s values) in
809 if v </ b then v else failwith "num_of_string: invalid digit for base"
810 and two = num_2 and ten = num_10 and sixteen = Int 16 in
811 let rec num_of_stringlist b l =
813 [] -> failwith "num_of_string: no digits after base indicator"
815 | h::t -> valof b h +/ b */ num_of_stringlist b t in
817 match explode(s) with
818 [] -> failwith "num_of_string: no digits"
819 | "0"::"x"::hexdigits -> num_of_stringlist sixteen (rev hexdigits)
820 | "0"::"b"::bindigits -> num_of_stringlist two (rev bindigits)
821 | decdigits -> num_of_stringlist ten (rev decdigits);;
823 (* ------------------------------------------------------------------------- *)
824 (* Convenient conversion between files and (lists of) strings. *)
825 (* ------------------------------------------------------------------------- *)
827 let strings_of_file filename =
828 let fd = try Pervasives.open_in filename
830 failwith("strings_of_file: can't open "^filename) in
831 let rec suck_lines acc =
832 try let l = Pervasives.input_line fd in
834 with End_of_file -> rev acc in
835 let data = suck_lines [] in
836 (Pervasives.close_in fd; data);;
838 let string_of_file filename =
839 end_itlist (fun s t -> s^"\n"^t) (strings_of_file filename);;
841 let file_of_string filename s =
842 let fd = Pervasives.open_out filename in
843 output_string fd s; close_out fd;;