1 (* ---------------------------------------------------------------------- *)
3 (* ---------------------------------------------------------------------- *)
5 let (+=) a b = a := !a + b;;
6 let (+.=) a b = a := !a +. b;;
8 (* ---------------------------------------------------------------------- *)
10 (* ---------------------------------------------------------------------- *)
13 let start_time = Sys.time() in
14 try let result = f x in
15 let finish_time = Sys.time() in
16 let total_time = finish_time -. start_time in
19 let finish_time = Sys.time() in
20 let total_time = finish_time -. start_time in
21 (print_string("Failed after (user) CPU time of "^
22 (string_of_float(total_time) ^": "));
25 (* ---------------------------------------------------------------------- *)
27 (* ---------------------------------------------------------------------- *)
35 let rec insertat i x l =
36 if i = 0 then x::l else
38 [] -> failwith "insertat: list too short for position to exist"
39 | h::t -> h::(insertat (i-1) x t);;
41 let rec allcombs f l =
45 map (f h) t @ allcombs f t;;
47 let rec assoc_list keys assl =
50 | h::t -> assoc h assl::assoc_list t assl;;
53 let add_to_list l1 l2 =
59 if i = 0 then hd l else ith (i-1) (tl l);;
61 let rev_ith i l = ith (length l - i - 1) l;;
64 let rec get_index p l n =
66 [] -> failwith "get_index"
67 | h::t -> if p h then n else get_index p t (n + 1) in
70 get_index (fun x -> x > 5) [1;2;3;7;9]
75 let rec bindex p l i =
77 [] -> failwith "bindex: not found"
78 | h::t -> if p h then i else bindex p t (i + 1) in
81 let cons x y = x :: y;;
83 let rec swap_lists l store =
87 let store' = map2 cons h store in
92 swap_lists [[1;2;3];[4;5;6];[7;8;9];[10;11;12]]
94 [[1; 4; 7; 10]; [2; 5; 8; 11]; [3; 6; 9; 12]]
98 let n = length (hd l) in
99 let l' = swap_lists l (replicate [] n) in
106 bindex (fun x -> x = 5) [1;2;5];;
109 let fst3 (a,_,_) = a;;
110 let snd3 (_,a,_) = a;;
111 let thd3 (_,_,a) = a;;
113 let odd n = (n mod 2 = 1);;
114 let even n = (n mod 2 = 0);;
116 (* ---------------------------------------------------------------------- *)
118 (* ---------------------------------------------------------------------- *)
120 let dest_var_or_const t =
123 | Const(s,ty) -> s,ty
124 | _ -> failwith "not a var or const";;
126 let can_match t1 t2 =
128 let n1,_ = dest_var_or_const t1 in
129 let n2,_ = dest_var_or_const t2 in
130 n1 = n2 & can (term_match [] t1) t2
131 with Failure _ -> false;;
134 if is_forall tm then dest_forall tm
135 else if is_exists tm then dest_exists tm
136 else failwith "dest_quant: not a quantified term";;
139 try let f,r = dest_comb tm in
140 let xop,l = dest_comb f in
142 with Failure _ -> failwith "get_binop";;