Bisect report

000001| open QCheck

000002|

000003| (* split : int -> 'a list -> 'a list * 'a list *)

000004| let rec split i ls = match i,ls with

000005| | 0, ls -> (*[113081514]*)[],ls

000006| | n, [] -> (*[0]*)failwith "splitting beyond list length"

000007| | n,l::ls -> (*[161207296]*)let ls,rs = split (n-1) ls in (*[161207296]*)l::ls,rs

000008|

000009|

000010| (** Generic lattice tests *)

000011|

000012| module type LATTICE_TOPLESS =

000013| sig

000014| val name : string

000015| type elem

000016| val leq : elem -> elem -> bool

000017| val join : elem -> elem -> elem

000018| val meet : elem -> elem -> elem

000019| val bot : elem

000020| (* val top : elem *)

000021| val eq : elem -> elem -> bool

000022| val to_string : elem -> string

000023| val pprint : elem -> unit

000024| val arb_elem : elem Arbitrary.t

000025| val equiv_pair : (elem * elem) Arbitrary.t

000026| val arb_elem_le : elem -> elem Arbitrary.t

000027| end

000028|

000029| module type LATTICE =

000030| sig

000031| include LATTICE_TOPLESS

000032| val top : elem

000033| end

000034|

000035| module GenericTests (L : LATTICE_TOPLESS) =

000036| struct

000037| (* Helpers for generating pairs and triples *)

000038| let arb_pair = (*[15]*)Arbitrary.pair L.arb_elem L.arb_elem

000039| let arb_triple = (*[15]*)Arbitrary.triple L.arb_elem L.arb_elem L.arb_elem

000040|

000041| let ord_pair = (*[15]*)Arbitrary.(L.arb_elem >>= fun e -> (*[105000]*)pair (L.arb_elem_le e) (return e))

000042| let ord_triple = (*[15]*)Arbitrary.(L.arb_elem >>= fun e ->

000043| (*[15000]*)L.arb_elem_le e >>= fun e' ->

000044| (*[15000]*)L.arb_elem_le e' >>= fun e'' -> (*[15000]*)return (e'',e',e))

000045|

000046| (* Helpers for pretty printing pairs and triples *)

000047| let pp_pair = (*[15]*)PP.pair L.to_string L.to_string

000048| let pp_triple = (*[15]*)PP.triple L.to_string L.to_string L.to_string

000049|

000050| let size a = (*[0]*)String.length (L.to_string a)

000051| let size_pair p = (*[0]*)String.length (pp_pair p)

000052| let size_triple t = (*[0]*)String.length (pp_triple t)

000053|

000054| (* Generic lattice property tests *)

000055| let leq_refl = (* forall a. a <= a *)

000056| (*[15]*)mk_test ~n:1000 ~pp:L.to_string ~limit:1 ~name:("leq reflexive in " ^ L.name) ~size:size

000057| L.arb_elem

000058| (fun a -> (*[15000]*)L.leq a a)

000059|

000060| let leq_trans = (* forall a,b,c. a <= b /\ b <= c => a <= c *)

000061| (*[15]*)mk_test ~n:1000 ~pp:pp_triple ~limit:1 ~name:("leq transitive in " ^ L.name) ~size:size_triple

000062| ord_triple (* arb_triple *)

000063| (fun (a,b,c) -> (*[15000]*)Prop.assume (L.leq a b);

000064| (*[15000]*)Prop.assume (L.leq b c);

000065| (*[15000]*)L.leq a c)

000066|

000067| let leq_antisym = (* forall a,b. a <= b /\ b <= a => a = b *)

000068| (*[15]*)mk_test ~n:1000 ~pp:pp_pair ~limit:1 ~name:("leq anti symmetric in " ^ L.name) ~size:size_pair

000069| L.equiv_pair (* Alternatively: Arbitrary.(choose [L.equiv_pair; ord_pair; ord_pair >>= fun (a,b) -> return (b,a)]) *)

000070| (fun (a,b) -> (*[15000]*)Prop.assume (L.leq a b);

000071| (*[15000]*)Prop.assume (L.leq b a);

000072| (*[15000]*)L.eq a b)

000073|

000074| (*let top_is_upperbound = (* forall a. a <= top *)

000075| mk_test ~n:1000 ~pp:L.to_string ~limit:1 ~name:("top is upper bound in " ^ L.name)

000076| ~size:(fun a -> String.length (pp_pair a))

000077| L.arb_elem

000078| (fun a -> L.(leq a top)) *)

000079|

000080| let bot_is_lowerbound = (* forall a. bot <= a *)

000081| (*[15]*)mk_test ~n:1000 ~pp:L.to_string ~limit:1 ~name:("bot is lower bound in " ^ L.name) ~size:size

000082| L.arb_elem

000083| (fun a -> (*[15000]*)L.(leq bot a))

000084|

000085| let join_comm = (* forall a,b. a \/ b = b \/ a *)

000086| (*[15]*)mk_test ~n:1000 ~pp:pp_pair ~limit:1 ~name:("join commutative in " ^ L.name) ~size:size_pair

000087| arb_pair

000088| (fun (a,b) -> (*[15000]*)L.(eq (join a b) (join b a)))

000089|

000090| let join_assoc = (* forall a,b,c. (a \/ b) \/ c = a \/ (b \/ c) *)

000091| (*[15]*)mk_test ~n:1000 ~pp:pp_triple ~limit:1 ~name:("join associative in " ^ L.name) ~size:size_triple

000092| arb_triple

000093| (fun (a,b,c) -> (*[15000]*)L.(eq (join (join a b) c) (join a (join b c)) ))

000094|

000095| let join_idempotent = (* forall a. a \/ a = a *)

000096| (*[15]*)mk_test ~n:1000 ~pp:L.to_string ~limit:1 ~name:("join idempotent in " ^ L.name) ~size:size

000097| L.arb_elem

000098| (fun a -> (*[15000]*)L.(eq (join a a) a))

000099|

000100| let meet_comm = (* forall a,b. a /\ b = b /\ a *)

000101| (*[15]*)mk_test ~n:1000 ~pp:pp_pair ~limit:1 ~name:("meet commutative in " ^ L.name) ~size:size_pair

000102| arb_pair

000103| (fun (a,b) -> (*[15000]*)L.(eq (meet a b) (meet b a)))

000104|

000105| let meet_assoc = (* forall a,b,c. (a /\ b) /\ c = a /\ (b /\ c) *)

000106| (*[15]*)mk_test ~n:1000 ~pp:pp_triple ~limit:1 ~name:("meet associative in " ^ L.name) ~size:size_triple

000107| arb_triple

000108| (fun (a,b,c) -> (*[15000]*)L.(eq (meet (meet a b) c) (meet a (meet b c)) ))

000109|

000110| let meet_idempotent = (* forall a. a /\ a = a *)

000111| (*[15]*)mk_test ~n:1000 ~pp:L.to_string ~limit:1 ~name:("meet idempotent in " ^ L.name) ~size:size

000112| L.arb_elem

000113| (fun a -> (*[15000]*)L.(eq (meet a a) a))

000114|

000115| let join_meet_absorption = (* forall a,b. a \/ (a /\ b) = a *)

000116| (*[15]*)mk_test ~n:1000 ~pp:pp_pair ~limit:1 ~name:("join meet absorbtion in " ^ L.name) ~size:size_pair

000117| arb_pair

000118| (fun (a,b) -> (*[15000]*)L.(eq (join a (meet a b)) a))

000119|

000120| let meet_join_absorption = (* forall a,b. a /\ (a \/ b) = a *)

000121| (*[15]*)mk_test ~n:1000 ~pp:pp_pair ~limit:1 ~name:("meet join absorbtion in " ^ L.name) ~size:size_pair

000122| arb_pair

000123| (fun (a,b) -> (*[15000]*)L.(eq (meet a (join a b)) a))

000124|

000125| let leq_compat_join = (* forall a,b. a < b ==> a \/ b = b *)

000126| (*[15]*)mk_test ~n:1000 ~pp:pp_pair ~limit:1 ~name:("leq compatible join in " ^ L.name) ~size:size_pair

000127| ord_pair (*arb_pair*)

000128| (fun (a,b) -> (*[15000]*)Prop.assume (L.leq a b);

000129| (*[15000]*)L.(eq (join a b) b))

000130|

000131| let join_compat_leq = (* forall a,b. a \/ b = b ==> a < b *)

000132| (*[15]*)mk_test ~n:1000 ~pp:pp_pair ~limit:1 ~name:("join compatible leq in " ^ L.name) ~size:size_pair

000133| ord_pair (*arb_pair*)

000134| (fun (a,b) -> (*[15000]*)Prop.assume L.(eq (join a b) b);

000135| ((*[15000]*)L.leq a b))

000136|

000137| let join_compat_meet = (* forall a,b. a \/ b = b ==> a /\ b = a *)

000138| (*[15]*)mk_test ~n:1000 ~pp:pp_pair ~limit:1 ~name:("join compatible meet in " ^ L.name) ~size:size_pair

000139| ord_pair (*arb_pair*)

000140| (fun (a,b) -> (*[15000]*)Prop.assume L.(eq (join a b) b);

000141| (*[15000]*)L.(eq (meet a b) a))

000142|

000143| let meet_compat_join = (* forall a,b. a /\ b = a ==> a \/ b = b *)

000144| (*[15]*)mk_test ~n:1000 ~pp:pp_pair ~limit:1 ~name:("meet compatible join in " ^ L.name) ~size:size_pair

000145| ord_pair (*arb_pair*)

000146| (fun (a,b) -> (*[15000]*)Prop.assume L.(eq (meet a b) a);

000147| (*[15000]*)L.(eq (join a b) b))

000148|

000149| let meet_compat_leq = (* forall a,b. a /\ b = a ==> a <= b *)

000150| (*[15]*)mk_test ~n:1000 ~pp:pp_pair ~limit:1 ~name:("meet compatible leq in " ^ L.name) ~size:size_pair

000151| ord_pair (*arb_pair*)

000152| (fun (a,b) -> (*[15000]*)Prop.assume (L.(eq (meet a b) a));

000153| (*[15000]*)L.leq a b)

000154|

000155| let leq_compat_meet = (* forall a,b. a <= b ==> a /\ b = a *)

000156| (*[15]*)mk_test ~n:1000 ~pp:pp_pair ~limit:1 ~name:("leq compatible meet in " ^ L.name) ~size:size_pair

000157| ord_pair (*arb_pair*)

000158| (fun (a,b) -> (*[15000]*)Prop.assume (L.leq a b);

000159| (*[15000]*)L.(eq (meet a b) a))

000160|

000161| (* Consistency check: generated ordered pairs are in fact ordered *)

000162| let check_ordering =

000163| (*[15]*)mk_test ~n:1000 ~pp:pp_pair ~limit:1 ~name:("generated ordered pairs consistent in " ^ L.name) ~size:size_pair

000164| ord_pair (fun (a,b) -> (*[15000]*)L.leq a b)

000165|

000166| let pp_pair = (*[15]*)PP.pair L.to_string L.to_string

000167| let ord_pair = (*[15]*)Arbitrary.(L.arb_elem >>= fun v -> (*[2000]*)pair (L.arb_elem_le v) (return v))

000168|

000169| let suite =

000170| [ (*[15]*)leq_refl; leq_trans; leq_antisym;

000171| (*top_is_upperbound;*)

000172| bot_is_lowerbound;

000173| join_comm; join_assoc; join_idempotent;

000174| meet_comm; meet_assoc; meet_idempotent;

000175| join_meet_absorption; meet_join_absorption;

000176| (* compatibility *)

000177| leq_compat_join; join_compat_leq;

000178| join_compat_meet; meet_compat_join;

000179| meet_compat_leq; leq_compat_meet;

000180| check_ordering; ]

000181| end

000182|

000183| module GenericTopTests (L : LATTICE) =

000184| struct

000185| let top_is_upperbound = (* forall a. a <= top *)

000186| (*[5]*)mk_test ~n:1000 ~pp:L.to_string ~limit:1 ~name:("top is upper bound in " ^ L.name)

000187| ~size:(fun a -> (*[0]*)String.length (L.to_string a))

000188| L.arb_elem

000189| (fun a -> (*[5000]*)L.(leq a top))

000190|

000191| let suite = [ (*[5]*)top_is_upperbound ]

000192| end

000193|

000194|

000195| (** EDSL for lattice operation tests *)

000196|

000197| let ord_pair (*[1]*)(type a) (module L : LATTICE_TOPLESS with type elem = a) =

000198| (*[0]*)Arbitrary.(L.arb_elem >>= fun e -> (*[0]*)pair (L.arb_elem_le e) (return e))

000199|

000200| module type ARB_ARG =

000201| sig

000202| (* val name : string *)

000203| type elem

000204| val arb_elem : elem Arbitrary.t

000205| val to_string : elem -> string

000206| end

000207|

000208| module MkArbListArg (A : ARB_ARG) =

000209| struct

000210| type elem = A.elem list

000211| let arb_elem = (*[2]*)Arbitrary.(list ~len:(int 20) A.arb_elem)

000212| let to_string = (*[2]*)PP.list A.to_string

000213| end

000214|

000215| let op_monotone (*[1]*)(type a) (type b) (module PL : LATTICE_TOPLESS with type elem = a)

000216| (module RL : LATTICE_TOPLESS with type elem = b) k =

000217| (*[198]*)let ord_pair = Arbitrary.(PL.arb_elem >>= fun e -> (*[198000]*)pair (PL.arb_elem_le e) (return e)) in

000218| (*[198]*)k (PP.pair PL.to_string PL.to_string,

000219| ord_pair,

000220| (fun op (v,v') -> (*[198000]*)Prop.assume (PL.leq v v'); (*[198000]*)RL.leq (op v) (op v')),

000221| "monotone",

000222| 1)

000223|

000224| let op_invariant (*[1]*)(type a) (type b) (module PL : LATTICE_TOPLESS with type elem = a)

000225| (module RL : LATTICE_TOPLESS with type elem = b) k =

000226| (*[205]*)k (PP.pair PL.to_string PL.to_string,

000227| PL.equiv_pair,

000228| (fun op (v,v') -> (*[205000]*)Prop.assume (PL.eq v v'); (*[205000]*)RL.eq (op v) (op v')),

000229| "invariant",

000230| 1)

000231|

000232| let op_strict (*[1]*)(type a) (type b) (module PL : LATTICE_TOPLESS with type elem = a)

000233| (module RL : LATTICE_TOPLESS with type elem = b) k =

000234| (*[170]*)k (PL.to_string,

000235| Arbitrary.return PL.bot,

000236| (fun op bot -> (*[170000]*)Prop.assume (PL.eq bot PL.bot); (*[170000]*)RL.eq (op bot) RL.bot),

000237| "strict",

000238| 1)

000239|

000240| let op_distributive (*[1]*)(type a) (type b) (module PL : LATTICE_TOPLESS with type elem = a)

000241| (module RL : LATTICE_TOPLESS with type elem = b) k =

000242| (*[0]*)let arb_pair = Arbitrary.pair PL.arb_elem PL.arb_elem in

000243| (*[0]*)k (PP.pair PL.to_string PL.to_string,

000244| arb_pair,

000245| (fun op (v,v') -> (*[0]*)RL.eq (op (PL.join v v')) (RL.join (op v) (op v'))),

000246| "distributive",

000247| 1)

000248|

000249| let pw_left (*[1]*)(type a) (module PL : ARB_ARG with type elem = a) op_prop m1 m2 k =

000250| (*[300]*)op_prop m1 m2 (fun (subpp,subgen,prop,pname,leftargs) -> (*[300]*)k (PP.pair PL.to_string subpp,

000251| Arbitrary.pair PL.arb_elem subgen,

000252| (fun op (a,b) -> (*[300000]*)prop (op a) b),

000253| pname,

000254| leftargs+1))

000255|

000256| let pw_right (*[1]*)(type a) (module PL : ARB_ARG with type elem = a) op_prop m1 m2 k =

000257| (*[353]*)op_prop m1 m2 (fun (subpp,subgen,prop,pname,leftargs) -> (*[353]*)k (PP.pair subpp PL.to_string,

000258| Arbitrary.pair subgen PL.arb_elem,

000259| (fun op (p,st) -> (*[353000]*)prop (fun v -> (*[608000]*)op v st) p),

000260| pname,

000261| leftargs))

000262|

000263| let ( ---> ) (*[1]*)(type e) (type e') = fun a -> fun (b : (module LATTICE_TOPLESS with type elem = e)) ->

000264| fun k -> (*[456]*)a (fun (l,optranl,r,optranr,prop) ->

000265| (*[456]*)let module R = (val r : LATTICE_TOPLESS with type elem = e') in (* manual "upcast" *)

000266| let r = (module R : ARB_ARG with type elem = e') in (* the module type *)

000267| (*[456]*)k (l,(fun prop -> (*[222]*)optranl (pw_left r prop)),

000268| b,(fun prop -> (*[234]*)optranr (pw_right r prop)),

000269| prop))

000270| let ( -<-> ) (*[1]*)(type e) = fun a -> fun (b : (module LATTICE_TOPLESS with type elem = e)) ->

000271| fun k -> (*[163]*)a (fun (l,optranl,r,_,_) -> (*[163]*)k (r,(fun prop -> (*[0]*)prop),b,optranl,op_monotone))

000272| let ( -$-> ) (*[1]*)(type e) = fun a -> fun (b : (module LATTICE_TOPLESS with type elem = e)) ->

000273| fun k -> (*[143]*)a (fun (l,optranl,r,_,_) -> (*[143]*)k (r,(fun prop -> (*[0]*)prop),b,optranl,op_strict))

000274| let ( -~-> ) (*[1]*)(type e) = fun a -> fun (b : (module LATTICE_TOPLESS with type elem = e)) ->

000275| fun k -> (*[169]*)a (fun (l,optranl,r,_,_) -> (*[169]*)k (r,(fun prop -> (*[0]*)prop),b,optranl,op_invariant))

000276| let ( -%-> ) (*[1]*)(type e) = fun a -> fun (b : (module LATTICE_TOPLESS with type elem = e)) ->

000277| fun k -> (*[0]*)a (fun (l,optranl,r,_,_) -> (*[0]*)k (r,(fun prop -> (*[0]*)prop),b,optranl,op_distributive))

000278|

000279| let testsig (*[1]*)(type e) (i : (module LATTICE_TOPLESS with type elem = e)) k =

000280| (*[475]*)k (i,(fun prop -> (*[475]*)prop),i,(fun prop -> (*[0]*)prop),(fun _ -> (*[0]*)assert false))

000281|

000282| let finalize opsig (opname,op) =

000283| (*[573]*)opsig (fun (pp,gen,prop,pname,leftargs) ->

000284| (*[573]*)mk_test ~n:1000 ~pp:pp ~limit:1 ~size:(fun a -> (*[0]*)String.length (pp a))

000285| ~name:(Printf.sprintf "'%s %s in argument %i'" opname pname leftargs)

000286| gen (prop op))

000287|

000288| let ( =:: ) a (b,c) = (*[98]*)finalize a (b,c)

000289|

000290| let for_op = (fun (l,_,r,optrans,prop) (opname,op) ->

000291| (*[475]*)finalize (optrans prop l r) (opname,op))

000292| let ( =: ) a (b,c) = (*[475]*)a for_op (b,c)

000293|

000294|

000295| (** A number of reusable lattices *)

000296|

000297| (* Note: the following module represents the Boolean lattice: *)

000298| (* {true,false} under reverse implication ordering, *)

000299| (* bot = true <== true <== false <== false = top *)

000300| module Bool =

000301| struct

000302| let name = (*[1]*)"Boolean lattice"

000303| type elem = bool

000304| let leq a b = (*[22000]*)if a then (*[10616]*)true else ((*[11384]*)not b)

000305| let join = (*[1]*)(&&)

000306| let meet = (*[1]*)(||)

000307| let bot = (*[1]*)true

000308| let top = (*[1]*)false

000309| let eq = (*[1]*)(=)

000310| let to_string = (*[1]*)string_of_bool

000311| let pprint = (*[1]*)Format.printf "%b"

000312| (* The below ones are generic *)

000313| let arb_elem = (*[1]*)Arbitrary.among [bot; top]

000314| let equiv_pair = (*[1]*)Arbitrary.(lift (fun a -> ((*[1000]*)a,a)) arb_elem)

000315| let arb_elem_le e = (*[9000]*)if e = top then (*[4258]*)arb_elem else (*[4742]*)Arbitrary.return bot

000316| end

000317|

000318| (* Note: the following module represents the dual Boolean lattice: *)

000319| (* {true,false} under implication ordering, *)

000320| (* bot = false <== false <== true <== true = top *)

000321| module DBool =

000322| struct

000323| let name = (*[1]*)"Dual Boolean lattice"

000324| type elem = bool

000325| let leq a b = (*[20000]*)if a then (*[7924]*)b else (*[12076]*)true

000326| let join = (*[1]*)(||)

000327| let meet = (*[1]*)(&&)

000328| let bot = (*[1]*)false

000329| let top = (*[1]*)true

000330| let eq = (*[1]*)(=)

000331| let to_string = (*[1]*)string_of_bool

000332| let pprint = (*[1]*)Format.printf "%b"

000333| (* The below ones are generic *)

000334| let arb_elem = (*[1]*)Arbitrary.among [bot; top]

000335| let equiv_pair = (*[1]*)Arbitrary.(lift (fun a -> ((*[1000]*)a,a)) arb_elem)

000336| let arb_elem_le e = (*[9000]*)if e = top then (*[4330]*)arb_elem else (*[4670]*)Arbitrary.return bot

000337| end

000338|

000339| module GenBoolTests = GenericTests(Bool)

000340| module GenBoolTopTests = GenericTopTests(Bool)

000341| module GenDBoolTests = GenericTests(DBool)

000342| module GenDBoolTopTests = GenericTopTests(DBool)

000343|

000344| module MkPairLattice (A : LATTICE_TOPLESS) (B : LATTICE_TOPLESS)

000345| = struct

000346| let name = (*[3]*)"(" ^ A.name ^ " * " ^ B.name ^ ") pair lattice"

000347| type elem = A.elem * B.elem

000348| let leq p p' = (*[91920]*)A.leq (fst p) (fst p') && (*[91920]*)B.leq (snd p) (snd p')

000349| let join p p' = ((*[39000]*)A.join (fst p) (fst p'), B.join (snd p) (snd p'))

000350| let meet p p' = ((*[39000]*)A.meet (fst p) (fst p'), B.meet (snd p) (snd p'))

000351| let bot = ((*[3]*)A.bot, B.bot)

000352| let eq p p' = (*[167000]*)A.eq (fst p) (fst p') && (*[167000]*)B.eq (snd p) (snd p')

000353| let to_string = (*[3]*)PP.pair A.to_string B.to_string

000354| let pprint p = (*[0]*)Format.printf "%s" (to_string p)

000355| let arb_elem = (*[3]*)Arbitrary.pair A.arb_elem B.arb_elem

000356| let equiv_pair = (*[3]*)Arbitrary.(A.equiv_pair >>= fun (a,a') ->

000357| (*[3000]*)B.equiv_pair >>= fun (b,b') -> (*[3000]*)return ((a,b),(a',b')))

000358| let arb_elem_le p = (*[27000]*)Arbitrary.pair (A.arb_elem_le (fst p)) (B.arb_elem_le (snd p))

000359| end

000360|

000361| module MkListLattice (A : LATTICE_TOPLESS) =

000362| struct

000363| let name = (*[1]*)"(" ^ A.name ^ ") list lattice"

000364| type elem = A.elem list

000365| let rec leq vs us = match vs,us with

000366| | [],_ -> (*[99000]*)true

000367| | _,[] -> (*[0]*)false

000368| | v::vs,u::us -> (*[149680]*)A.leq v u && (*[149680]*)leq vs us

000369| let rec join vs us = match vs,us with

000370| | [],_ -> (*[18792]*)us

000371| | _,[] -> (*[7208]*)vs

000372| | v::vs,u::us -> (*[75595]*)(A.join v u) :: (join vs us)

000373| let rec meet vs us = match vs,us with

000374| | [],_ -> (*[19643]*)[]

000375| | _,[] -> (*[6357]*)[]

000376| | v::vs,u::us -> (*[72065]*)(A.meet v u) :: (meet vs us)

000377| let bot = (*[1]*)[]

000378| let rec eq vs us = match vs,us with

000379| | [],[]-> (*[201000]*)true

000380| | v::vs,u::us -> (*[321613]*)A.eq v u && (*[321613]*)eq vs us

000381| | _,_ -> (*[0]*)false

000382| let to_string = (*[1]*)PP.list A.to_string

000383| let pprint vs = (*[0]*)Format.printf "%s" (to_string vs)

000384| let arb_elem = (*[1]*)Arbitrary.list A.arb_elem

000385| let equiv_pair = (*[1]*)Arbitrary.(lift (fun v -> ((*[32000]*)v,v)) arb_elem)

000386| let arb_elem_le vs = (*[41000]*)Arbitrary.(int (1 + List.length vs) >>= fun i ->

000387| (*[41000]*)let smaller_vs,_ = split i vs in

000388| (*[41000]*)List.fold_right

000389| (fun v acc_gen -> (*[90290]*)lift2 (fun v a -> (*[90290]*)v::a) (A.arb_elem_le v) acc_gen)

000390| smaller_vs (Arbitrary.return []))

000391| end