From f48dbc458eb53b19b7cafff3ef89bf9a23c7885d Mon Sep 17 00:00:00 2001 From: Simon Cruanes Date: Wed, 10 May 2017 17:14:54 +0200 Subject: [PATCH] add rich testsuite to `CCIntMap`, based on @jmid's work --- src/data/CCIntMap.ml | 167 +++++++++++++++++++++++++++++++++++++++++++ 1 file changed, 167 insertions(+) diff --git a/src/data/CCIntMap.ml b/src/data/CCIntMap.ml index 2fde434e..3ea70206 100644 --- a/src/data/CCIntMap.ml +++ b/src/data/CCIntMap.ml @@ -541,3 +541,170 @@ let print pp_x out m = Format.pp_print_cut out () ) m; Format.fprintf out "}@]" + +(* Some thorough tests from Jan Midtgaar + https://github.com/jmid/qc-ptrees + *) + +(*$inject + let test_count = 2_500 + + open QCheck + + type instr_tree = + | Empty + | Singleton of int * int + | Add of int * int * instr_tree + | Remove of int * instr_tree + | Union of instr_tree * instr_tree + | Inter of instr_tree * instr_tree + + let rec to_string (a:instr_tree): string = + let int_to_string = string_of_int in + match a with + | Empty -> "Empty" + | Singleton (k,v) -> Printf.sprintf "Singleton(%d,%d)" k v + | Add (k,v,t) -> Printf.sprintf "Add(%d,%d," k v ^ (to_string t) ^ ")" + | Remove (n,t) -> "Remove (" ^ (int_to_string n) ^ ", " ^ (to_string t) ^ ")" + | Union (t,t') -> "Union (" ^ (to_string t) ^ ", " ^ (to_string t') ^ ")" + | Inter (t,t') -> "Inter (" ^ (to_string t) ^ ", " ^ (to_string t') ^ ")" + + let merge_f _ x y = min x y + + let rec interpret t : _ t = match t with + | Empty -> empty + | Singleton (k,v) -> singleton k v + | Add (k,v,t) -> add k v (interpret t) + | Remove (n,t) -> remove n (interpret t) + | Union (t,t') -> + let s = interpret t in + let s' = interpret t' in + union merge_f s s' + | Inter (t,t') -> + let s = interpret t in + let s' = interpret t' in + inter merge_f s s' + + let tree_gen int_gen : instr_tree Q.Gen.t = + let open Gen in + sized + (fix (fun recgen n -> match n with + | 0 -> oneof [return Empty; + Gen.map2 (fun i j -> Singleton (i,j)) int_gen int_gen] + | _ -> + frequency + [ (1, return Empty); + (1, map2 (fun k v -> Singleton (k,v)) int_gen int_gen); + (2, map3 (fun i j t -> Add (i,j,t)) int_gen int_gen (recgen (n-1))); + (2, map2 (fun i t -> Remove (i,t)) int_gen (recgen (n-1))); + (2, map2 (fun l r -> Union (l,r)) (recgen (n/2)) (recgen (n/2))); + (2, map2 (fun l r -> Inter (l,r)) (recgen (n/2)) (recgen (n/2))); + ])) + + let (<+>) = Q.Iter.(<+>) + + let rec tshrink t : instr_tree Q.Iter.t = match t with + | Empty -> Iter.empty + | Singleton (k,v) -> + (Iter.return Empty) + <+> (Iter.map (fun k' -> Singleton (k',v)) (Shrink.int k)) + <+> (Iter.map (fun v' -> Singleton (k,v')) (Shrink.int v)) + | Add (k,v,t) -> + (Iter.of_list [Empty; t; Singleton (k,v)]) + <+> (Iter.map (fun t' -> Add (k,v,t')) (tshrink t)) + <+> (Iter.map (fun k' -> Add (k',v,t)) (Shrink.int k)) + <+> (Iter.map (fun v' -> Add (k,v',t)) (Shrink.int v)) + | Remove (i,t) -> + (Iter.of_list [Empty; t]) + <+> (Iter.map (fun t' -> Remove (i,t')) (tshrink t)) + <+> (Iter.map (fun i' -> Remove (i',t)) (Shrink.int i)) + | Union (t0,t1) -> + (Iter.of_list [Empty;t0;t1]) + <+> (Iter.map (fun t0' -> Union (t0',t1)) (tshrink t0)) + <+> (Iter.map (fun t1' -> Union (t0,t1')) (tshrink t1)) + | Inter (t0,t1) -> + (Iter.of_list [Empty;t0;t1]) + <+> (Iter.map (fun t0' -> Inter (t0',t1)) (tshrink t0)) + <+> (Iter.map (fun t1' -> Inter (t0,t1')) (tshrink t1)) + + let arb_int = + frequency + [(5,small_signed_int); + (3,int); + (1, oneofl [min_int;max_int])] + + let arb_tree = + make ~print:to_string ~shrink:tshrink + (tree_gen arb_int.gen) + + let empty_m = [] + let singleton_m k v = [k,v] + let mem_m i s = List.mem_assoc i s + let rec remove_m i s = match s with + | [] -> [] + | (j,v)::s' -> if i=j then s' else (j,v)::(remove_m i s') + let add_m k v s = List.sort Pervasives.compare ((k,v)::remove_m k s) + let rec union_m s s' = match s,s' with + | [], _ -> s' + | _, [] -> s + | (k1,v1)::is,(k2,v2)::js -> + if k1k2 then (k2,v2)::(union_m s js) else + (k1,min v1 v2)::(union_m is js) + let rec inter_m s s' = match s with + | [] -> [] + | (k,v)::s -> + if List.mem_assoc k s' + then (k,min v (List.assoc k s'))::(inter_m s s') + else inter_m s s' + + let abstract s = List.sort Pervasives.compare (fold (fun k v acc -> (k,v)::acc) s []) +*) + +(* A bunch of agreement properties *) + +(*$= + empty_m (let s = empty in abstract s) +*) + +(*$QR & ~count:test_count + (Q.pair arb_int arb_int) (fun (k,v) -> + abstract (singleton k v) = singleton_m k v) +*) + +(*$QR & ~count:test_count + Q.(pair arb_tree arb_int) + (fun (t,n) -> + let s = interpret t in + mem n s = mem_m n (abstract s)) +*) + +(*$QR & ~count:test_count + (triple arb_tree arb_int arb_int) + (fun (t,k,v) -> + let s = interpret t in + abstract (add k v s) = add_m k v (abstract s)) + *) + +(*$QR & ~count:test_count + (pair arb_tree arb_int) + (fun (t,n) -> + let s = interpret t in + abstract (remove n s) = remove_m n (abstract s)) + *) + +(*$QR & ~count:test_count + (pair arb_tree arb_tree) + (fun (t,t') -> + let s = interpret t in + let s' = interpret t' in + abstract (union merge_f s s') = union_m (abstract s) (abstract s')) + *) + +(*$QR & ~count:test_count + Q.(pair arb_tree arb_tree) + (fun (t,t') -> + let s = interpret t in + let s' = interpret t' in + abstract (inter merge_f s s') = inter_m (abstract s) (abstract s')) +*)