Rqe/rqe_lib.ml

   1 (* ---------------------------------------------------------------------- *)
   2 (*  Refs                                                                  *)
   3 (* ---------------------------------------------------------------------- *)
   4
   5 let (+=) a b = a := !a + b;;
   6 let (+.=) a b = a := !a +. b;;
   7
   8 (* ---------------------------------------------------------------------- *)
   9 (*  Timing                                                                *)
  10 (* ---------------------------------------------------------------------- *)
  11
  12 let ptime f x =
  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
  17       (result,total_time)
  18   with e ->
  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) ^": "));
  23       raise e);;
  24
  25 (* ---------------------------------------------------------------------- *)
  26 (*  Lists                                                                 *)
  27 (* ---------------------------------------------------------------------- *)
  28
  29 let mappair f g l =
  30   let a,b = unzip l in
  31   let la = map f a in
  32   let lb = map g b in
  33     zip la lb;;
  34
  35 let rec insertat i x l =
  36   if i = 0 then x::l else
  37   match l with
  38     [] -> failwith "insertat: list too short for position to exist"
  39   | h::t -> h::(insertat (i-1) x t);;
  40
  41 let rec allcombs f l =
  42   match l with
  43       [] -> []
  44     | h::t ->
  45         map (f h) t @ allcombs f t;;
  46
  47 let rec assoc_list keys assl =
  48   match keys with
  49       [] -> []
  50     | h::t -> assoc h assl::assoc_list t assl;;
  51
  52
  53 let add_to_list l1 l2 =
  54   l1 := !l1 @ l2;;
  55
  56 let list x = [x];;
  57
  58 let rec ith i l =
  59   if i = 0 then hd l else ith (i-1) (tl l);;
  60
  61 let rev_ith i l = ith (length l - i - 1) l;;
  62
  63 let get_index p l =
  64   let rec get_index p l n =
  65     match l with
  66         [] -> failwith "get_index"
  67       | h::t -> if p h then n else get_index p t (n + 1) in
  68     get_index p l 0;;
  69 (*
  70   get_index (fun x -> x > 5) [1;2;3;7;9]
  71 *)
  72
  73
  74 let bindex p l =
  75   let rec bindex p l i =
  76     match l with
  77         [] -> failwith "bindex: not found"
  78       | h::t -> if p h then i else bindex p t (i + 1) in
  79     bindex p l 0;;
  80
  81 let cons x y = x :: y;;
  82
  83 let rec swap_lists l store =
  84   match l with
  85       [] -> store
  86     | h::t ->
  87         let store' = map2 cons h store in
  88           swap_lists t store';;
  89
  90
  91 (*
  92 swap_lists [[1;2;3];[4;5;6];[7;8;9];[10;11;12]]
  93 -->
  94 [[1; 4; 7; 10]; [2; 5; 8; 11]; [3; 6; 9; 12]]
  95 *)
  96
  97 let swap_lists l =
  98   let n = length (hd l) in
  99   let l' = swap_lists l (replicate [] n) in
 100     map rev l';;
 101
 102
 103
 104
 105 (*
 106 bindex (fun x -> x = 5) [1;2;5];;
 107 *)
 108
 109 let fst3 (a,_,_) = a;;
 110 let snd3 (_,a,_) = a;;
 111 let thd3 (_,_,a) = a;;
 112
 113 let odd n = (n mod 2 = 1);;
 114 let even n = (n mod 2 = 0);;
 115
 116 (* ---------------------------------------------------------------------- *)
 117 (*  Terms                                                                 *)
 118 (* ---------------------------------------------------------------------- *)
 119
 120 let dest_var_or_const t =
 121   match t with
 122       Var(s,ty) -> s,ty
 123     | Const(s,ty) -> s,ty
 124     | _ -> failwith "not a var or const";;
 125
 126 let can_match t1 t2 =
 127   try
 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;;
 132
 133 let dest_quant tm =
 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";;
 137
 138 let get_binop tm =
 139   try let f,r = dest_comb tm in
 140       let xop,l = dest_comb f in
 141         xop,l,r
 142   with Failure _ -> failwith "get_binop";;
 143