123456789101112131415161718192021222324252627282930313233343536373839404142434445464748495051525354555657585960616263646566676869707172737475767778798081828384858687888990919293(************************************************************************)(* * The Coq Proof Assistant / The Coq Development Team *)(* v * Copyright INRIA, CNRS and contributors *)(* <O___,, * (see version control and CREDITS file for authors & dates) *)(* \VV/ **************************************************************)(* // * This file is distributed under the terms of the *)(* * GNU Lesser General Public License Version 2.1 *)(* * (see LICENSE file for the text of the license) *)(************************************************************************)type'atree=|Leafof'a|Nodeof'a*'atree*'atreetype'at=Nil|Consofint*'atree*'atletoob()=invalid_arg"index out of bounds"letempty=Nilletconsxl=matchlwith|Cons(h1,t1,Cons(h2,t2,rem))->ifInt.equalh1h2thenCons(1+h1+h2,Node(x,t1,t2),rem)elseCons(1,Leafx,l)|_->Cons(1,Leafx,l)letis_empty=function|Nil->true|_->falseletrectree_gethti=matchtwith|Leafx->ifi=0thenxelseoob()|Node(x,t1,t2)->ifi=0thenxelseleth=h/2inifi<=hthentree_getht1(i-1)elsetree_getht2(i-h-1)letrecgetli=matchlwith|Nil->oob()|Cons(h,t,rem)->ifi<hthentree_gethtielsegetrem(i-h)letlengthl=letreclengthaccu=function|Nil->accu|Cons(h,_,l)->length(h+accu)linlength0lletrectree_mapf=function|Leafx->Leaf(fx)|Node(x,t1,t2)->Node(fx,tree_mapft1,tree_mapft2)letrecmapf=function|Nil->Nil|Cons(h,t,l)->Cons(h,tree_mapft,mapfl)letrectree_fold_leftfaccu=function|Leafx->faccux|Node(x,t1,t2)->tree_fold_leftf(tree_fold_leftf(faccux)t1)t2letrecfold_leftfaccu=function|Nil->accu|Cons(_,t,l)->fold_leftf(tree_fold_leftfaccut)lletrectree_fold_rightftaccu=matchtwith|Leafx->fxaccu|Node(x,t1,t2)->fx(tree_fold_rightft1(tree_fold_rightft2accu))letrecfold_rightflaccu=matchlwith|Nil->accu|Cons(_,t,l)->tree_fold_rightft(fold_rightflaccu)lethd=function|Nil->failwith"hd"|Cons(_,Leafx,_)->x|Cons(_,Node(x,_,_),_)->xlettl=function|Nil->failwith"tl"|Cons(_,Leaf_,l)->l|Cons(h,Node(_,t1,t2),l)->leth=h/2inCons(h,t1,Cons(h,t2,l))letrecskipnnl=ifn=0thenlelseifis_emptylthenfailwith"List.skipn"elseskipn(predn)(tll)