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 (* ========================================================================= *)
12 let fail() = failwith "";;
14 (* ------------------------------------------------------------------------- *)
16 (* ------------------------------------------------------------------------- *)
18 let curry f x y = f(x,y);;
20 let uncurry f(x,y) = f x y;;
30 let (o) = fun f g x -> f(g x);;
32 let (F_F) = fun f g (x,y) -> (f x,g y);;
34 (* ------------------------------------------------------------------------- *)
36 (* ------------------------------------------------------------------------- *)
41 | _ -> failwith "hd";;
46 | _ -> failwith "tl";;
52 | (x::t) -> let y = f x in y::(mapf t) in
59 | [] -> failwith "last";;
64 | (h::t) -> h::(butlast t)
65 | [] -> failwith "butlast";;
68 if n = 0 then hd l else el (n - 1) (tl l);;
71 let rec rev_append acc l =
74 | h::t -> rev_append (h::acc) t in
75 fun l -> rev_append [] l;;
77 let rec map2 f l1 l2 =
80 | (h1::t1),(h2::t2) -> let h = f h1 h2 in h::(map2 f t1 t2)
81 | _ -> failwith "map2: length mismatch";;
83 (* ------------------------------------------------------------------------- *)
84 (* Attempting function or predicate applications. *)
85 (* ------------------------------------------------------------------------- *)
87 let can f x = try (f x; true) with Failure _ -> false;;
89 let check p x = if p x then x else failwith "check";;
91 (* ------------------------------------------------------------------------- *)
92 (* Repetition of a function. *)
93 (* ------------------------------------------------------------------------- *)
95 let rec funpow n f x =
96 if n < 1 then x else funpow (n-1) f (f x);;
99 try let y = f x in repeat f y with Failure _ -> x;;
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 (* ------------------------------------------------------------------------- *)
106 exception Unchanged;;
108 (* ------------------------------------------------------------------------- *)
109 (* Various versions of list iteration. *)
110 (* ------------------------------------------------------------------------- *)
112 let rec itlist f l b =
115 | (h::t) -> f h (itlist f t b);;
117 let rec rev_itlist f l b =
120 | (h::t) -> rev_itlist f t (f h b);;
122 let rec end_itlist f l =
124 [] -> failwith "end_itlist"
126 | (h::t) -> f h (end_itlist f t);;
128 let rec itlist2 f l1 l2 b =
131 | (h1::t1,h2::t2) -> f h1 h2 (itlist2 f t1 t2 b)
132 | _ -> failwith "itlist2";;
134 let rec rev_itlist2 f l1 l2 b =
137 | (h1::t1,h2::t2) -> rev_itlist2 f t1 t2 (f h1 h2 b)
138 | _ -> failwith "rev_itlist2";;
140 (* ------------------------------------------------------------------------- *)
141 (* Iterative splitting (list) and stripping (tree) via destructor. *)
142 (* ------------------------------------------------------------------------- *)
144 let rec splitlist dest x =
145 try let l,r = dest x in
146 let ls,res = splitlist dest r in
148 with Failure _ -> ([],x);;
150 let rev_splitlist dest =
151 let rec rsplist ls x =
152 try let l,r = dest x in
154 with Failure _ -> (x,ls) in
155 fun x -> rsplist [] x;;
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 [];;
164 (* ------------------------------------------------------------------------- *)
165 (* Apply a destructor as many times as elements in list. *)
166 (* ------------------------------------------------------------------------- *)
168 let rec nsplit dest clist x =
169 if clist = [] then [],x else
171 let ll,y = nsplit dest (tl clist) r in
174 (* ------------------------------------------------------------------------- *)
175 (* Replication and sequences. *)
176 (* ------------------------------------------------------------------------- *)
178 let rec replicate x n =
180 else x::(replicate x (n - 1));;
182 let rec (--) = fun m n -> if m > n then [] else m::((m + 1) -- n);;
184 (* ------------------------------------------------------------------------- *)
185 (* Various useful list operations. *)
186 (* ------------------------------------------------------------------------- *)
191 | h::t -> p(h) & forall p t;;
193 let rec forall2 p l1 l2 =
196 | (h1::t1,h2::t2) -> p h1 h2 & forall2 p t1 t2
202 | h::t -> p(h) or exists p t;;
206 if l = [] then k else len (k + 1) (tl l) in
212 | h::t -> let t' = filter p t in
213 if p(h) then if t'==t then l else h::t'
216 let rec partition p 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);;
223 let rec mapfilter f l =
226 | (h::t) -> let rest = mapfilter f t in
227 try (f h)::rest with Failure _ -> rest;;
231 [] -> failwith "find"
232 | (h::t) -> if p(h) then h else find p t;;
234 let rec tryfind f l =
236 [] -> failwith "tryfind"
237 | (h::t) -> try f h with Failure _ -> tryfind f t;;
239 let flat l = itlist (@) l [];;
243 [] -> failwith "remove"
244 | (h::t) -> if p(h) then h,t else
245 let y,n = remove p t in y,h::n;;
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";;
255 [] -> failwith "index"
256 | (h::t) -> if Pervasives.compare x h = 0 then n else ind (n + 1) t in
259 (* ------------------------------------------------------------------------- *)
260 (* "Set" operations on lists. *)
261 (* ------------------------------------------------------------------------- *)
266 | (h::t) -> Pervasives.compare x h = 0 or mem x t;;
269 if mem x l then l else x::l;;
271 let union l1 l2 = itlist insert l1 l2;;
273 let unions l = itlist union l [];;
275 let intersect l1 l2 = filter (fun x -> mem x l2) l1;;
277 let subtract l1 l2 = filter (fun x -> not (mem x l2)) l1;;
279 let subset l1 l2 = forall (fun t -> mem t l2) l1;;
281 let set_eq l1 l2 = subset l1 l2 & subset l2 l1;;
283 (* ------------------------------------------------------------------------- *)
284 (* Association lists. *)
285 (* ------------------------------------------------------------------------- *)
289 (x,y)::t -> if Pervasives.compare x a = 0 then y else assoc a t
290 | [] -> failwith "find";;
292 let rec rev_assoc a l =
294 (x,y)::t -> if Pervasives.compare y a = 0 then x else rev_assoc a t
295 | [] -> failwith "find";;
297 (* ------------------------------------------------------------------------- *)
298 (* Zipping, unzipping etc. *)
299 (* ------------------------------------------------------------------------- *)
304 | (h1::t1,h2::t2) -> (h1,h2)::(zip t1 t2)
305 | _ -> failwith "zip";;
309 | ((a,b)::rest) -> let alist,blist = unzip rest in
310 (a::alist,b::blist);;
312 (* ------------------------------------------------------------------------- *)
313 (* Sharing out a list according to pattern in list-of-lists. *)
314 (* ------------------------------------------------------------------------- *)
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);;
321 (* ------------------------------------------------------------------------- *)
322 (* Iterating functions over lists. *)
323 (* ------------------------------------------------------------------------- *)
325 let rec do_list f l =
328 | (h::t) -> (f h; do_list f t);;
330 (* ------------------------------------------------------------------------- *)
332 (* ------------------------------------------------------------------------- *)
334 let rec sort cmp lis =
338 let r,l = partition (cmp piv) rest in
339 (sort cmp l) @ (piv::(sort cmp r));;
341 (* ------------------------------------------------------------------------- *)
342 (* Removing adjacent (NB!) equal elements from list. *)
343 (* ------------------------------------------------------------------------- *)
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'
352 (* ------------------------------------------------------------------------- *)
353 (* Convert list into set by eliminating duplicates. *)
354 (* ------------------------------------------------------------------------- *)
356 let setify s = uniq (sort (fun x y -> Pervasives.compare x y <= 0) s);;
358 (* ------------------------------------------------------------------------- *)
359 (* String operations (surely there is a better way...) *)
360 (* ------------------------------------------------------------------------- *)
362 let implode l = itlist (^) l "";;
367 exap (n - 1) ((String.sub s n 1)::l) in
368 exap (String.length s - 1) [];;
370 (* ------------------------------------------------------------------------- *)
371 (* Greatest common divisor. *)
372 (* ------------------------------------------------------------------------- *)
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';;
380 (* ------------------------------------------------------------------------- *)
381 (* Some useful functions on "num" type. *)
382 (* ------------------------------------------------------------------------- *)
387 and num_10 = Int 10;;
389 let pow2 n = power_num num_2 (Int n);;
390 let pow10 n = power_num num_10 (Int n);;
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');;
397 let numerator = fst o numdom
398 and denominator = snd o numdom;;
401 num_of_big_int(Big_int.gcd_big_int (big_int_of_num n1) (big_int_of_num n2));;
404 if x =/ num_0 & y =/ num_0 then num_0
405 else abs_num((x */ y) // gcd_num x y);;
407 (* ------------------------------------------------------------------------- *)
408 (* All pairs arising from applying a function over two lists. *)
409 (* ------------------------------------------------------------------------- *)
411 let rec allpairs f l1 l2 =
413 h1::t1 -> itlist (fun x a -> f h1 x :: a) l2 (allpairs f t1 l2)
416 (* ------------------------------------------------------------------------- *)
417 (* Issue a report with a newline. *)
418 (* ------------------------------------------------------------------------- *)
421 Format.print_string s; Format.print_newline();;
423 (* ------------------------------------------------------------------------- *)
424 (* Convenient function for issuing a warning. *)
425 (* ------------------------------------------------------------------------- *)
428 if cond then report ("Warning: "^s) else ();;
430 (* ------------------------------------------------------------------------- *)
431 (* Flags to switch on verbose mode. *)
432 (* ------------------------------------------------------------------------- *)
434 let verbose = ref true;;
435 let report_timing = ref true;;
437 (* ------------------------------------------------------------------------- *)
438 (* Switchable version of "report". *)
439 (* ------------------------------------------------------------------------- *)
442 if !verbose then report s else ();;
444 (* ------------------------------------------------------------------------- *)
445 (* Time a function. *)
446 (* ------------------------------------------------------------------------- *)
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)));
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))^": ");
461 (* ------------------------------------------------------------------------- *)
462 (* Versions of assoc and rev_assoc with default rather than failure. *)
463 (* ------------------------------------------------------------------------- *)
465 let rec assocd a l d =
468 | (x,y)::t -> if Pervasives.compare x a = 0 then y else assocd a t d;;
470 let rec rev_assocd a l d =
473 | (x,y)::t -> if Pervasives.compare y a = 0 then x else rev_assocd a t d;;
475 (* ------------------------------------------------------------------------- *)
476 (* Version of map that avoids rebuilding unchanged subterms. *)
477 (* ------------------------------------------------------------------------- *)
481 h::t -> let h' = f h and t' = qmap f t in
482 if h' == h & t' == t then l else h'::t'
485 (* ------------------------------------------------------------------------- *)
486 (* Merging and bottom-up mergesort. *)
487 (* ------------------------------------------------------------------------- *)
489 let rec merge ord l1 l2 =
492 | h1::t1 -> match l2 with
494 | h2::t2 -> if ord h1 h2 then h1::(merge ord t1 l2)
495 else h2::(merge ord l1 t2);;
498 let rec mergepairs l1 l2 =
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);;
506 (* ------------------------------------------------------------------------- *)
507 (* Common measure predicates to use with "sort". *)
508 (* ------------------------------------------------------------------------- *)
510 let increasing f x y = Pervasives.compare (f x) (f y) < 0;;
512 let decreasing f x y = Pervasives.compare (f x) (f y) > 0;;
514 (* ------------------------------------------------------------------------- *)
515 (* Polymorphic finite partial functions via Patricia trees. *)
517 (* The point of this strange representation is that it is canonical (equal *)
518 (* functions have the same encoding) yet reasonably efficient on average. *)
520 (* Idea due to Diego Olivier Fernandez Pons (OCaml list, 2003/11/10). *)
521 (* ------------------------------------------------------------------------- *)
525 | Leaf of int * ('a*'b)list
526 | Branch of int * int * ('a,'b)func * ('a,'b)func;;
528 (* ------------------------------------------------------------------------- *)
529 (* Undefined function. *)
530 (* ------------------------------------------------------------------------- *)
532 let undefined = Empty;;
534 (* ------------------------------------------------------------------------- *)
535 (* In case of equality comparison worries, better use this. *)
536 (* ------------------------------------------------------------------------- *)
543 (* ------------------------------------------------------------------------- *)
544 (* Operation analagous to "map" for lists. *)
545 (* ------------------------------------------------------------------------- *)
548 let rec map_list f l =
551 | (x,y)::t -> (x,f(y))::(map_list f t) in
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
559 (* ------------------------------------------------------------------------- *)
560 (* Operations analogous to "fold" for lists. *)
561 (* ------------------------------------------------------------------------- *)
564 let rec foldl_list f a l =
567 | (x,y)::t -> foldl_list f (f a x y) t in
568 let rec foldl f a t =
571 | Leaf(h,l) -> foldl_list f a l
572 | Branch(p,b,l,r) -> foldl f (foldl f a l) r in
576 let rec foldr_list f l a =
579 | (x,y)::t -> f x y (foldr_list f t a) in
580 let rec foldr f t a =
583 | Leaf(h,l) -> foldr_list f l a
584 | Branch(p,b,l,r) -> foldr f l (foldr f r a) in
587 (* ------------------------------------------------------------------------- *)
588 (* Mapping to sorted-list representation of the graph, domain and range. *)
589 (* ------------------------------------------------------------------------- *)
591 let graph f = setify (foldl (fun a x y -> (x,y)::a) [] f);;
593 let dom f = setify(foldl (fun a x y -> x::a) [] f);;
595 let ran f = setify(foldl (fun a x y -> y::a) [] f);;
597 (* ------------------------------------------------------------------------- *)
599 (* ------------------------------------------------------------------------- *)
602 let rec apply_listd l d x =
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
608 let k = Hashtbl.hash x in
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)
617 let apply f = applyd f (fun x -> failwith "apply");;
619 let tryapplyd f a d = applyd f (fun x -> d) a;;
621 let defined f x = try apply f x; true with Failure _ -> false;;
623 (* ------------------------------------------------------------------------- *)
625 (* ------------------------------------------------------------------------- *)
628 let rec undefine_list x l =
631 let c = Pervasives.compare x a in
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'
638 let k = Hashtbl.hash x in
641 Leaf(h,l) when h = k ->
642 let l' = undefine_list x l in
644 else if l' = [] then Empty
646 | Branch(p,b,l,r) when k land (b - 1) = p ->
650 else (match l' with Empty -> r | _ -> Branch(p,b,l',r))
654 else (match r' with Empty -> l | _ -> Branch(p,b,l,r'))
658 (* ------------------------------------------------------------------------- *)
659 (* Redefinition and combination. *)
660 (* ------------------------------------------------------------------------- *)
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 =
672 let c = Pervasives.compare x a in
674 else if c < 0 then xy::l
675 else ab::(define_list xy t)
677 and combine_list op z l1 l2 =
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
688 let k = Hashtbl.hash x in
691 Empty -> Leaf (k,[x,y])
693 if h = k then Leaf(h,define_list (x,y) l)
694 else newbranch h t k (Leaf(k,[x,y]))
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
700 let rec combine op z t1 t2 =
704 | Leaf(h1,l1),Leaf(h2,l2) ->
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
712 (match combine op z lf l with
713 Empty -> r | l' -> Branch(p,b,l',r))
715 (match combine op z lf r with
716 Empty -> l | r' -> Branch(p,b,l,r'))
719 | (Branch(p,b,l,r) as br),(Leaf(k,lis) as lf) ->
720 if k land (b - 1) = p then
722 (match combine op z l lf with
723 Empty -> r | l' -> Branch(p,b,l',r))
725 (match combine op z r lf with
726 Empty -> l | r' -> Branch(p,b,l,r'))
729 | Branch(p1,b1,l1,r1),Branch(p2,b2,l2,r2) ->
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))
736 (match combine op z r1 t2 with
737 Empty -> l1 | r -> Branch(p1,b1,l1,r))
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))
744 (match combine op z t1 r2 with
745 Empty -> l2 | r -> Branch(p2,b2,l2,r))
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))
750 newbranch p1 t1 p2 t2 in
753 (* ------------------------------------------------------------------------- *)
754 (* Special case of point function. *)
755 (* ------------------------------------------------------------------------- *)
757 let (|=>) = fun x y -> (x |-> y) undefined;;
759 (* ------------------------------------------------------------------------- *)
760 (* Grab an arbitrary element. *)
761 (* ------------------------------------------------------------------------- *)
765 Empty -> failwith "choose: completely undefined function"
767 | Branch(b,p,t1,t2) -> choose t1;;
769 (* ------------------------------------------------------------------------- *)
770 (* Install a trivial printer for the general polymorphic case. *)
771 (* ------------------------------------------------------------------------- *)
773 (* let print_fpf (f:('a,'b)func) = Format.print_string "<func>";;
775 #install_printer print_fpf;;
778 (* ------------------------------------------------------------------------- *)
779 (* Set operations parametrized by equality (from Steven Obua). *)
780 (* ------------------------------------------------------------------------- *)
786 | (h::t) -> eq x h or mem x t
790 if mem' eq x l then l else x::l;;
792 let union' eq l1 l2 = itlist (insert' eq) l1 l2;;
794 let unions' eq l = itlist (union' eq) l [];;
796 let subtract' eq l1 l2 = filter (fun x -> not (mem' eq x l2)) l1;;
798 (* ------------------------------------------------------------------------- *)
799 (* Accepts decimal, hex or binary numeral, using C notation 0x... for hex *)
800 (* and analogous 0b... for binary. *)
801 (* ------------------------------------------------------------------------- *)
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
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 =
816 [] -> failwith "num_of_string: no digits after base indicator"
818 | h::t -> valof b h +/ b */ num_of_stringlist b t in
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);;
826 (* ------------------------------------------------------------------------- *)
827 (* Convenient conversion between files and (lists of) strings. *)
828 (* ------------------------------------------------------------------------- *)
830 let strings_of_file filename =
831 let fd = try Pervasives.open_in filename
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
837 with End_of_file -> rev acc in
838 let data = suck_lines [] in
839 (Pervasives.close_in fd; data);;
841 let string_of_file filename =
842 end_itlist (fun s t -> s^"\n"^t) (strings_of_file filename);;
844 let file_of_string filename s =
845 let fd = Pervasives.open_out filename in
846 output_string fd s; close_out fd;;