123456789101112131415161718192021222324252627282930313233343536373839404142434445464748495051525354555657585960616263646566676869707172737475767778798081828384858687888990919293949596979899100101102103104105106107108109110111112113114115116117118119120121122123124125126127128129130131132133134135136137138139140141142143144145146147148149150151152153154155156157158159160161162163164165166167168169170171172173174175176177178179180181182183184185186187188189190191192193194195196197198199200201202203204205206207208209210211212213214215216217218219220221222223224225226227228229230231232233234235236237238239240241242243244245246247248249250251252253254255256257258259260261262263264265266267268269270271272273274275276277278279280281282283284285286287288289290291292293294295296297298299300301302303304305306307308309310311312313314315316317318319320321322323324325326327328329330331332333334335336337338339340341342343344345346347348349350351352353354355356357358359360361362363364365366367368369370371372373374375376377378379380381382383384385386387388389390391392393394395396397398399400401402403404405406407408409410411412413414415416417418419420421422423424425426427428429430431432433434435436437438439440441442443444445446447448449450451452453454455456457458459460461462463464465466467468469470471472473474475476477478479480481482483484485486487488489490491492493494495496497498499500501502503504505506507508509510511512513514515516517518519520521522523524525526527528529530531532533534535536537538539540541542543544545546547548549550551552553554555556557558559560561562563564565566567568569570571572573574575576577578579580581582583584585586587588589590591592593594595596597598599600601602603604605606607608609610611612613614615616617618619620621622623624625626627628629630631632633634635636637638639640641642643644645646647648649650651652653654655656657658659660661662663664665666667668669670671672673674675676677678679680681682683684685686687688689690691692693694695696697698699700701702703704705706707708709710711712713714715716717718719720721722723724725726727728729730731732733734735736737738739740741742743744745746747748749750751752753754755756757758759760761762763764765766767768769770771772773774775776777778779780781782783784785786787788789790791792793794795796797798799800801802803804805806807808809810811812813814815816817818819820821822823824825826827828829830831832833834835836837838839840841842843844845846847848849850851852853854855856857858859860861862863864865866867868869870871872873874875876877878879880881882883884885886887888889890891892893894895896897898899900(* This file is free software, part of containers. See file "license" for more details. *)(** {1 Map specialized for Int keys} *)(* "Fast Mergeable Integer Maps", Okasaki & Gill.
We use big-endian trees. *)(** Masks with exactly one bit active *)moduleBit:sigtypet=privateintvalhighest:int->tvalmin_int:tvalequal:t->t->boolvalis_0:bit:t->int->boolvalis_1:bit:t->int->boolvalmask:mask:t->int->int(* zeroes the bit, puts all lower bits to 1 *)vallt:t->t->boolvalgt:t->t->boolvalequal_int:int->t->boolend=structtypet=intletmin_int=min_intletequal:t->t->bool=Stdlib.(=)letrechighest_bit_naivexm=ifx=mthenmelsehighest_bit_naive(xland(lnotm))(2*m)letmask_20_=1lsl20letmask_40_=1lsl40lethighestx=ifx<0thenmin_intelseifSys.word_size>40&&x>mask_40_then((* remove least significant 40 bits *)letx'=xland(lnot(mask_40_-1))inhighest_bit_naivex'mask_40_)elseifx>mask_20_then((* small shortcut: remove least significant 20 bits *)letx'=xland(lnot(mask_20_-1))inhighest_bit_naivex'mask_20_)else(highest_bit_naivex1)letis_0~bitx=xlandbit=0letis_1~bitx=xlandbit=bitletmask~maskx=(xlor(mask-1))land(lnotmask)(* low endian: let mask_ x ~mask = x land (mask - 1) *)letgtab=(b!=min_int)&&(a=min_int||a>b)letltab=gtbaletequal_int=Stdlib.(=)end(*$inject
let highest2 x : int =
let rec aux i =
if i=0 then i
else if 1 = (x lsr i) then 1 lsl i else aux (i-1)
in
if x<0 then min_int else aux (Sys.word_size-2)
*)(*$QR & ~count:1_000
Q.int (fun x ->
if Bit.equal_int (highest2 x) (Bit.highest x) then true
else QCheck.Test.fail_reportf "x=%d, highest=%d, highest2=%d@." x
(Bit.highest x :> int) (highest2 x))
*)(*$inject
let _list_uniq l = CCList.sort_uniq ~cmp:(fun a b-> Stdlib.compare (fst a)(fst b)) l
*)type+'at=|E(* empty *)|Lofint*'a(* leaf *)|Nofint(* common prefix *)*Bit.t(* bit switch *)*'at*'atletempty=Eletis_empty=function|E->true|_->false(*$Q
Q.(small_list (pair int int)) (fun l -> \
let m = of_list l in \
is_empty m = (cardinal m = 0))
*)letis_prefix_~prefixy~bit=prefix=Bit.masky~mask:bit(*$Q
Q.int (fun i -> \
let b = Bit.highest i in \
((b:>int) land i = (b:>int)) && (i < 0 || ((b:>int) <= i && (i-(b:>int)) < (b:>int))))
Q.int (fun i -> (Bit.highest i = Bit.min_int) = (i < 0))
Q.int (fun i -> ((Bit.highest i:>int) < 0) = (Bit.highest i = Bit.min_int))
Q.int (fun i -> let j = (Bit.highest i :> int) in j land (j-1) = 0)
*)(*$T
(Bit.highest min_int :> int) = min_int
(Bit.highest 2 :> int) = 2
(Bit.highest 17 :> int) = 16
(Bit.highest 300 :> int) = 256
*)(* helper:
let b_of_i i =
let rec f acc i =
if i=0 then acc else let q, r = i/2, abs (i mod 2)
in
f (r::acc) q in f [] i;;
*)(* low endian: let branching_bit_ a _ b _ = lowest_bit_ (a lxor b) *)letbranching_bit_ab=Bit.highest(alxorb)(* TODO use hint in branching_bit_ *)letcheck_invariantst=(* check that keys are prefixed by every node in their path *)letreccheck_keyspatht=matchtwith|E->true|L(k,_)->List.for_all(fun(prefix,switch,side)->is_prefix_~prefixk~bit:switch&&beginmatchsidewith|`Left->Bit.is_0k~bit:switch|`Right->Bit.is_1k~bit:switchend)path|N(prefix,switch,l,r)->check_keys((prefix,switch,`Left)::path)l&&check_keys((prefix,switch,`Right)::path)rincheck_keys[]t(*$Q
Q.(list (pair int bool)) (fun l -> \
check_invariants (of_list l))
*)letrecfind_exnkt=matchtwith|E->raiseNot_found|L(k',v)whenk=k'->v|L_->raiseNot_found|N(prefix,m,l,r)->ifis_prefix_~prefixk~bit:mthen(ifBit.is_0k~bit:mthenfind_exnklelsefind_exnkr)else(raiseNot_found)(* XXX could test with lt_unsigned_? *)(*
if k <= prefix (* search tree *)
then find_exn k l
else find_exn k r
*)letfindkt=trySome(find_exnkt)withNot_found->None(*$Q
Q.(list (pair int int)) (fun l -> \
let l = _list_uniq l in \
let m = of_list l in \
List.for_all (fun (k,v) -> find k m = Some v) l)
*)letmemkt=tryignore(find_exnkt);truewithNot_found->false(*$Q
Q.(list (pair int int)) (fun l -> \
let m = of_list l in \
List.for_all (fun (k,_) -> mem k m) l)
*)letmk_node_prefixswitchlr=matchl,rwith|E,o|o,E->o|_->N(prefix,switch,l,r)(* join trees t1 and t2 with prefix p1 and p2 respectively
(p1 and p2 do not overlap) *)letjoin_t1p1t2p2=letswitch=branching_bit_p1p2inletprefix=Bit.maskp1~mask:switchinifBit.is_0p1~bit:switchthen(assert(Bit.is_1p2~bit:switch);mk_node_prefixswitcht1t2)else(assert(Bit.is_0p2~bit:switch);mk_node_prefixswitcht2t1)letsingletonkv=L(k,v)(* c: conflict function *)letrecinsert_ckvt=matchtwith|E->L(k,v)|L(k',v')->ifk=k'thenL(k,c~old:v'v)elsejoin_tk'(L(k,v))k|N(prefix,switch,l,r)->ifis_prefix_~prefixk~bit:switchthen(ifBit.is_0k~bit:switchthenN(prefix,switch,insert_ckvl,r)elseN(prefix,switch,l,insert_ckvr))else(join_(L(k,v))ktprefix)letaddkvt=insert_(fun~old:_v->v)kvt(*$Q & ~count:20
Q.(list (pair int int)) (fun l -> \
let l = _list_uniq l in let m = of_list l in \
List.for_all (fun (k,v) -> find_exn k m = v) l)
*)letrecremovekt=matchtwith|E->E|L(k',_)->ifk=k'thenEelset|N(prefix,switch,l,r)->ifis_prefix_~prefixk~bit:switchthen(ifBit.is_0k~bit:switchthenmk_node_prefixswitch(removekl)relsemk_node_prefixswitchl(removekr))else(t(* not present *))(*$Q & ~count:20
Q.(list (pair int int)) (fun l -> \
let l = _list_uniq l in let m = of_list l in \
List.for_all (fun (k,_) -> mem k m && not (mem k (remove k m))) l)
*)letupdatekft=tryletv=find_exnktinbeginmatchf(Somev)with|None->removekt|Somev'->addkv'tendwithNot_found->matchfNonewith|None->t|Somev->addkvt(*$= & ~printer:Q.Print.(list (pair int int))
[1,1; 2, 22; 3, 3] \
(of_list [1,1;2,2;3,3] \
|> update 2 (function None -> assert false | Some _ -> Some 22) \
|> to_list |> List.sort Stdlib.compare)
*)letdoubletonk1v1k2v2=addk1v1(singletonk2v2)letrecequal~eqab=Stdlib.(==)ab||beginmatcha,bwith|E,E->true|L(ka,va),L(kb,vb)->ka=kb&&eqvavb|N(pa,sa,la,ra),N(pb,sb,lb,rb)->pa=pb&&Bit.equalsasb&&equal~eqlalb&&equal~eqrarb|E,_|N_,_|L_,_->falseend(*$Q
Q.(list (pair int bool)) ( fun l -> \
equal ~eq:(=) (of_list l) (of_list (List.rev l)))
*)letreciterft=matchtwith|E->()|L(k,v)->fkv|N(_,_,l,r)->iterfl;iterfrletrecfoldftacc=matchtwith|E->acc|L(k,v)->fkvacc|N(_,_,l,r)->letacc=foldflaccinfoldfraccletcardinalt=fold(fun__n->n+1)t0letrecmapift=matchtwith|E->E|L(k,v)->L(k,fkv)|N(p,s,l,r)->N(p,s,mapifl,mapifr)letrecmapft=matchtwith|E->E|L(k,v)->L(k,fv)|N(p,s,l,r)->N(p,s,mapfl,mapfr)letrecchoose_exn=function|E->raiseNot_found|L(k,v)->k,v|N(_,_,l,_)->choose_exnlletchooset=trySome(choose_exnt)withNot_found->None(** {2 Whole-collection operations} *)letrecunionft1t2=matcht1,t2with|E,o|o,E->o|L(k,v),o|o,L(k,v)->(* insert k, v into o *)insert_(fun~oldv->fkoldv)kvo|N(p1,m1,l1,r1),N(p2,m2,l2,r2)->ifp1=p2&&Bit.equalm1m2then(mk_node_p1m1(unionfl1l2)(unionfr1r2))elseifBit.gtm1m2&&is_prefix_~prefix:p1p2~bit:m1then(ifBit.is_0p2~bit:m1thenN(p1,m1,unionfl1t2,r1)elseN(p1,m1,l1,unionfr1t2))elseifBit.ltm1m2&&is_prefix_~prefix:p2p1~bit:m2then(ifBit.is_0p1~bit:m2thenN(p2,m2,unionft1l2,r2)elseN(p2,m2,l2,unionft1r2))else(join_t1p1t2p2)(*$Q & ~small:(fun (a,b) -> List.length a + List.length b)
Q.(pair (list (pair int bool)) (list (pair int bool))) (fun (l1,l2) -> \
check_invariants (union (fun _ _ x -> x) (of_list l1) (of_list l2)))
Q.(pair (list (pair int bool)) (list (pair int bool))) (fun (l1,l2) -> \
check_invariants (inter (fun _ _ x -> x) (of_list l1) (of_list l2)))
*)(* associativity of union *)(*$Q & ~small:(fun (a,b,c) -> List.(length a + length b + length c))
Q.(let p = list (pair int int) in triple p p p) (fun (l1,l2,l3) -> \
let m1 = of_list l1 and m2 = of_list l2 and m3 = of_list l3 in \
let f _ x y = max x y in \
equal ~eq:(=) (union f (union f m1 m2) m3) (union f m1 (union f m2 m3)))
*)(*$R
assert_equal ~cmp:(equal ~eq:(=)) ~printer:(CCFormat.to_string (pp CCString.pp))
(of_list [1, "1"; 2, "2"; 3, "3"; 4, "4"])
(union (fun _ a b -> a)
(of_list [1, "1"; 3, "3"]) (of_list [2, "2"; 4, "4"]));
*)(*$R
assert_equal ~cmp:(equal ~eq:(=)) ~printer:(CCFormat.to_string (pp CCString.pp))
(of_list [1, "1"; 2, "2"; 3, "3"; 4, "4"])
(union (fun _ a b -> a)
(of_list [1, "1"; 2, "2"; 3, "3"]) (of_list [2, "2"; 4, "4"]))
*)(*$Q
Q.(list (pair int bool)) (fun l -> \
equal ~eq:(=) (of_list l) (union (fun _ a _ -> a) (of_list l)(of_list l)))
*)(*$inject
let union_l l1 l2 =
let l2' = List.filter (fun (x,_) -> not @@ List.mem_assoc x l1) l2 in
_list_uniq (l1 @ l2')
let inter_l l1 l2 =
let l2' = List.filter (fun (x,_) -> List.mem_assoc x l1) l2 in
_list_uniq l2'
*)(*$QR
Q.(pair (small_list (pair small_int unit)) (small_list (pair small_int unit)))
(fun (l1,l2) ->
union_l l1 l2 = _list_uniq @@ to_list (union (fun _ _ _ ->())(of_list l1) (of_list l2)))
*)(*$QR
Q.(pair (small_list (pair small_int unit)) (small_list (pair small_int unit)))
(fun (l1,l2) ->
inter_l l1 l2 = _list_uniq @@ to_list (inter (fun _ _ _ ->()) (of_list l1) (of_list l2)))
*)letrecinterfab=matcha,bwith|E,_|_,E->E|L(k,v),o|o,L(k,v)->begintryletv'=find_exnkoinL(k,fkvv')withNot_found->Eend|N(p1,m1,l1,r1),N(p2,m2,l2,r2)->ifp1=p2&&Bit.equalm1m2then(mk_node_p1m1(interfl1l2)(interfr1r2))elseifBit.gtm1m2&&is_prefix_~prefix:p1p2~bit:m1then(ifBit.is_0p2~bit:m1theninterfl1belseinterfr1b)elseifBit.ltm1m2&&is_prefix_~prefix:p2p1~bit:m2then(ifBit.is_0p1~bit:m2theninterfal2elseinterfar2)elseE(*$R
assert_equal ~cmp:(equal ~eq:(=)) ~printer:(CCFormat.to_string (pp CCString.pp))
(singleton 2 "2")
(inter (fun _ a b -> a)
(of_list [1, "1"; 2, "2"; 3, "3"]) (of_list [2, "2"; 4, "4"]))
*)(*$Q
Q.(list (pair int bool)) (fun l -> \
equal ~eq:(=) (of_list l) (inter (fun _ a _ -> a) (of_list l)(of_list l)))
*)(* associativity of inter *)(*$Q & ~small:(fun (a,b,c) -> List.(length a + length b + length c))
Q.(let p = list (pair int int) in triple p p p) (fun (l1,l2,l3) -> \
let m1 = of_list l1 and m2 = of_list l2 and m3 = of_list l3 in \
let f _ x y = max x y in \
equal ~eq:(=) (inter f (inter f m1 m2) m3) (inter f m1 (inter f m2 m3)))
*)letrecdisjoint_union_t1t2:_t=matcht1,t2with|E,o|o,E->o|L(k,v),o|o,L(k,v)->insert_(fun~old:__->assertfalse)kvo|N(p1,m1,l1,r1),N(p2,m2,l2,r2)->ifp1=p2&&Bit.equalm1m2then(mk_node_p1m1(disjoint_union_l1l2)(disjoint_union_r1r2))elseifBit.gtm1m2&&is_prefix_~prefix:p1p2~bit:m1then(ifBit.is_0p2~bit:m1thenmk_node_p1m1(disjoint_union_l1t2)r1elsemk_node_p1m1l1(disjoint_union_r1t2))elseifBit.ltm1m2&&is_prefix_~prefix:p2p1~bit:m2then(ifBit.is_0p1~bit:m2thenmk_node_p2m2(disjoint_union_t1l2)r2elsemk_node_p2m2l2(disjoint_union_t1r2))else(join_t1p1t2p2)letrecfilterfm=matchmwith|E->E|L(k,v)->iffkvthenmelseE|N(_,_,l,r)->disjoint_union_(filterfl)(filterfr)(*$QR
Q.(pair (fun2 Observable.int Observable.int bool) (small_list (pair int int))) (fun (f,l) ->
let QCheck.Fun(_,f) = f in
_list_uniq (List.filter (fun (x,y) -> f x y) l) =
(_list_uniq @@ to_list @@ filter f @@ of_list l)
)
*)letrecfilter_mapfm=matchmwith|E->E|L(k,v)->beginmatchfkvwith|None->E|Somev'->L(k,v')end|N(_,_,l,r)->disjoint_union_(filter_mapfl)(filter_mapfr)(*$QR
Q.(pair (fun2 Observable.int Observable.int @@ option bool) (small_list (pair int int))) (fun (f,l) ->
let QCheck.Fun(_,f) = f in
_list_uniq (CCList.filter_map (fun (x,y) -> CCOpt.map (CCPair.make x) @@ f x y) l) =
(_list_uniq @@ to_list @@ filter_map f @@ of_list l)
)
*)letrecmerge~ft1t2:_t=letmerge1t=filter_map(funkv->fk(`Leftv))tandmerge2t=filter_map(funkv->fk(`Rightv))tandadd_somekoptm=matchoptwith|None->m|Somev->insert_(fun~old:__->assertfalse)kvminmatcht1,t2with|E,o->merge2o|o,E->merge1o|L(k,v),o->letothers=merge2(removeko)inadd_somek(tryfk(`Both(v,find_exnko))withNot_found->fk(`Leftv))others|o,L(k,v)->letothers=merge1(removeko)inadd_somek(tryfk(`Both(find_exnko,v))withNot_found->fk(`Rightv))others|N(p1,m1,l1,r1),N(p2,m2,l2,r2)->ifp1=p2&&Bit.equalm1m2then(mk_node_p1m1(merge~fl1l2)(merge~fr1r2))elseifBit.gtm1m2&&is_prefix_~prefix:p1p2~bit:m1then(ifBit.is_0p2~bit:m1thenmk_node_p1m1(merge~fl1t2)(merge1r1)elsemk_node_p1m1(merge1l1)(merge~fr1t2))elseifBit.ltm1m2&&is_prefix_~prefix:p2p1~bit:m2then(ifBit.is_0p1~bit:m2thenmk_node_p2m2(merge~ft1l2)(merge2r2)elsemk_node_p2m2(merge2l2)(merge~ft1r2))else(join_(merge1t1)p1(merge2t2)p2)(*$inject
let merge_union _x o = match o with
| `Left v | `Right v | `Both (v,_) -> Some v
let merge_inter _x o = match o with
| `Left _ | `Right _ -> None
| `Both (v,_) -> Some v
*)(*$QR
Q.(let p = small_list (pair small_int small_int) in pair p p) (fun (l1,l2) ->
check_invariants
(merge ~f:merge_union (of_list l1) (of_list l2)))
*)(*$QR
Q.(let p = small_list (pair small_int small_int) in pair p p) (fun (l1,l2) ->
check_invariants
(merge ~f:merge_inter (of_list l1) (of_list l2)))
*)(*$QR
Q.(let p = small_list (pair small_int unit) in pair p p) (fun (l1,l2) ->
let l1 = _list_uniq l1 and l2 = _list_uniq l2 in
equal Stdlib.(=)
(union (fun _ v1 _ -> v1) (of_list l1) (of_list l2))
(merge ~f:merge_union (of_list l1) (of_list l2)))
*)(*$QR
Q.(let p = small_list (pair small_int unit) in pair p p) (fun (l1,l2) ->
let l1 = _list_uniq l1 and l2 = _list_uniq l2 in
equal Stdlib.(=)
(inter (fun _ v1 _ -> v1) (of_list l1) (of_list l2))
(merge ~f:merge_inter (of_list l1) (of_list l2)))
*)(** {2 Conversions} *)type'asequence=('a->unit)->unittype'agen=unit->'aoptiontype'aklist=unit->[`Nil|`Consof'a*'aklist]letadd_listtl=List.fold_left(funt(k,v)->addkvt)tlletof_listl=add_listemptylletto_listt=fold(funkvl->(k,v)::l)t[](*$Q
Q.(list (pair int int)) (fun l -> \
let l = List.map (fun (k,v) -> abs k,v) l in \
let rec is_sorted = function [] | [_] -> true \
| x::y::tail -> x <= y && is_sorted (y::tail) in \
of_list l |> to_list |> List.rev_map fst |> is_sorted)
*)(*$Q
Q.(list (pair int int)) (fun l -> \
of_list l |> cardinal = List.length l)
*)letadd_seqtseq=lett=reftinseq(fun(k,v)->t:=addkv!t);!tletof_seqseq=add_seqemptyseqletto_seqtyield=iter(funkv->yield(k,v))tletkeystyield=iter(funk_->yieldk)tletvaluestyield=iter(fun_v->yieldv)tletrecadd_genmg=matchg()with|None->m|Some(k,v)->add_gen(addkvm)gletof_geng=add_genemptygletto_genm=letst=Stack.create()inStack.pushmst;letrecnext()=ifStack.is_emptystthenNoneelseexplore(Stack.popst)andexploren=matchnwith|E->next()(* backtrack *)|L(k,v)->Some(k,v)|N(_,_,l,r)->Stack.pushrst;explorelinnext(*$T
doubleton 1 "a" 2 "b" |> to_gen |> of_gen |> to_list \
|> List.sort Stdlib.compare = [1, "a"; 2, "b"]
*)(*$Q
Q.(list (pair int bool)) (fun l -> \
let m = of_list l in equal ~eq:(=) m (m |> to_gen |> of_gen))
*)(* E < L < N; arbitrary order for switches *)letcompare~cmpab=letreccmp_gencmpab=matcha(),b()with|None,None->0|Some_,None->1|None,Some_->-1|Some(ka,va),Some(kb,vb)->ifka=kbthen(letc=cmpvavbinifc=0thencmp_gencmpabelsec)else(comparekakb)incmp_gencmp(to_gena)(to_genb)(*$Q
Q.(list (pair int bool)) ( fun l -> \
let m1 = of_list l and m2 = of_list (List.rev l) in \
compare ~cmp:Stdlib.compare m1 m2 = 0)
*)(*$QR
Q.(pair (list (pair int bool)) (list (pair int bool))) (fun (l1, l2) ->
let l1 = List.map (fun (k,v) -> abs k,v) l1 in
let l2 = List.map (fun (k,v) -> abs k,v) l2 in
let m1 = of_list l1 and m2 = of_list l2 in
let c = compare ~cmp:Stdlib.compare m1 m2
and c' = compare ~cmp:Stdlib.compare m2 m1 in
(c = 0) = (c' = 0) && (c < 0) = (c' > 0) && (c > 0) = (c' < 0))
*)(*$QR
Q.(pair (list (pair int bool)) (list (pair int bool))) (fun (l1, l2) ->
let l1 = List.map (fun (k,v) -> abs k,v) l1 in
let l2 = List.map (fun (k,v) -> abs k,v) l2 in
let m1 = of_list l1 and m2 = of_list l2 in
(compare ~cmp:Stdlib.compare m1 m2 = 0) = equal ~eq:(=) m1 m2)
*)letrecadd_klistml=matchl()with|`Nil->m|`Cons((k,v),tl)->add_klist(addkvm)tlletof_klistl=add_klistemptylletto_klistm=(* [st]: stack of alternatives *)letrecexplorestm()=matchmwith|E->nextst()|L(k,v)->`Cons((k,v),nextst)|N(_,_,l,r)->explore(r::st)l()andnextst()=matchstwith|[]->`Nil|x::st'->explorest'x()innext[m](*$Q
Q.(list (pair int bool)) (fun l -> \
let m = of_list l in equal ~eq:(=) m (m |> to_klist |> of_klist))
*)type'atree=unit->[`Nil|`Nodeof'a*'atreelist]letrecas_treet()=matchtwith|E->`Nil|L(k,v)->`Node(`Leaf(k,v),[])|N(prefix,switch,l,r)->`Node(`Node(prefix,(switch:>int)),[as_treel;as_treer])(** {2 IO} *)type'aprinter=Format.formatter->'a->unitletpppp_xoutm=Format.fprintfout"@[<hov2>intmap {@,";letfirst=reftrueiniter(funkv->if!firstthenfirst:=falseelseFormat.pp_print_stringout", ";Format.fprintfout"%d -> "k;pp_xoutv;Format.pp_print_cutout())m;Format.fprintfout"}@]"(* 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 Stdlib.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 k1<k2 then (k1,v1)::(union_m is s') else
if k1>k2 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 Stdlib.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'))
*)