123456789101112131415161718192021222324252627282930313233343536373839404142434445464748495051525354555657585960616263646566676869707172737475767778798081828384(************************************************************************)(* * 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'anode=|Nil|Consof'a*'atand'at='anodeLazy.tletempty=Lazy.from_valNilletconsxs=Lazy.from_val(Cons(x,s))letpeekx:_node=Lazy.forcexletthunkf:_t=Lazy.from_funfletrecforces=matchpeekswith|Nil->()|Cons(_,s)->forcesletforces=forces;sletis_emptys=matchpeekswith|Nil->true|Cons(_,_)->falseletrecof_list=function|[]->empty|x::l->consx(of_listl)letrecto_lists=matchpeekswith|Nil->[]|Cons(x,s)->x::(to_lists)letreciterfs=matchpeekswith|Nil->()|Cons(x,s)->fx;iterfsletrecmap_nodef=function|Nil->Nil|Cons(x,s)->Cons(fx,mapfs)andmapfs=lazy(map_nodef(peeks))letrecapp_noden1s2=matchn1with|Nil->peeks2|Cons(x,s1)->Cons(x,apps1s2)andapps1s2=lazy(app_node(peeks1)s2)letrecfoldfaccus=matchpeekswith|Nil->accu|Cons(x,s)->foldf(faccux)sletrecmap_filter_nodef=function|Nil->Nil|Cons(x,s)->beginmatchfxwith|None->map_filter_nodef(peeks)|Somey->Cons(y,map_filterfs)endandmap_filterfs=lazy(map_filter_nodef(peeks))letrecconcat_node=function|Nil->Nil|Cons(s,sl)->app_node(peeks)(concatsl)andconcat(s:'att)=lazy(concat_node(peeks))letrecconcat_map_nodef=function|Nil->Nil|Cons(x,s)->app_node(peek(fx))(concat_mapfs)andconcat_mapfl=lazy(concat_map_nodef(peekl))