1234567891011121314151617181920212223242526272829303132333435363738394041424344454647484950515253545556575859606162636465666768697071727374757677787980818283848586878889909192(************************************************************************)(* * 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('a,'r)u=|Nil|Consof'a*'rtype'anode=('a,'at)uand'at='anodeLazy.tletempty=Lazy.from_valNilletconsxs=Lazy.from_val(Cons(x,s))letthunk=Lazy.from_funletrecmake_nodefs=matchfswith|Nil->Nil|Cons(x,s)->Cons(x,makefs)andmakefs=lazy(make_nodefs)letrecforces=matchLazy.forceswith|Nil->()|Cons(_,s)->forcesletforces=forces;sletis_emptys=matchLazy.forceswith|Nil->true|Cons(_,_)->falseletpeek=Lazy.forceletrecof_list=function|[]->empty|x::l->consx(of_listl)letrecto_lists=matchLazy.forceswith|Nil->[]|Cons(x,s)->x::(to_lists)letreciterfs=matchLazy.forceswith|Nil->()|Cons(x,s)->fx;iterfsletrecmap_nodef=function|Nil->Nil|Cons(x,s)->Cons(fx,mapfs)andmapfs=lazy(map_nodef(Lazy.forces))letrecapp_noden1s2=matchn1with|Nil->Lazy.forces2|Cons(x,s1)->Cons(x,apps1s2)andapps1s2=lazy(app_node(Lazy.forces1)s2)letrecfoldfaccus=matchLazy.forceswith|Nil->accu|Cons(x,s)->foldf(faccux)sletrecmap_filter_nodef=function|Nil->Nil|Cons(x,s)->beginmatchfxwith|None->map_filter_nodef(Lazy.forces)|Somey->Cons(y,map_filterfs)endandmap_filterfs=lazy(map_filter_nodef(Lazy.forces))letrecconcat_node=function|Nil->Nil|Cons(s,sl)->app_node(Lazy.forces)(concatsl)andconcat(s:'att)=lazy(concat_node(Lazy.forces))letrecconcat_map_nodef=function|Nil->Nil|Cons(x,s)->app_node(Lazy.force(fx))(concat_mapfs)andconcat_mapfl=lazy(concat_map_nodef(Lazy.forcel))