123456789101112131415161718192021222324252627282930313233343536373839404142434445464748495051525354555657585960616263646566676869707172737475767778798081828384858687888990919293949596979899100101(* Copyright (c) Jean-Christophe Filliatre
SPDX-License-Identifier: MIT
Copyright (c) 2025 Romain Calascibetta <romain.calascibetta@gmail.com> *)(* Bit vectors. The interface and part of the code are borrowed from the
[Array] module of the OCaml standard library (but things are simplified
here since we can always initialize a bit vector). This module also
provides bitwise operations. *)(* We represent a bit vector by a string of bytes (field [bits]), and
we keep the information of the size of the bit vector (field
[length]) since it can not be figured out with the size of the
array. *)externalbytes_unsafe_set:bytes->int->int->unit="%bytes_unsafe_set"externalbytes_unsafe_get:bytes->int->int="%bytes_unsafe_get"typet={length:int;bits:bytes;mutablehi:int}letlength{length;_}=lengthlet[@inline]equal(v1:t)(v2:t)=v1=v2letmax_length=ifmax_intlsr3<Sys.max_string_lengththenmax_intelseSys.max_string_length*8let_exceeds_max_lengthn=lets=n/8in(ifnland0b111=0thenselses+1)/Sys.max_string_lengthletlow_mask=Array.init9(funi->(1lsli)-1)letcreatenb=ifn<0||n>max_lengththeninvalid_arg"Miou_unix.Bitv.create";letinitv=ifbthen255else0inletq=nlsr3andr=nland7inifr==0thenletbits=Bytes.makeq(Char.chrinitv)in{length=n;bits;hi=ifbthennelse0}elsebeginlets=Bytes.make(q+1)(Char.chrinitv)inbytes_unsafe_setsq(initvlandlow_mask.(r));{length=n;bits=s;hi=ifbthennelse0}endletunsafe_getvn=leti=nlsr3inbytes_unsafe_getv.bitsiland(1lsl(nland7))>0letgetvn=ifn<0||n>=v.lengththeninvalid_arg"Miou_unix.Bitv.get";unsafe_getvnexternalmiou_bitv_clz:bytes->(int[@untagged])="miou_bitv_clz_bytecode""miou_bitv_clz_native"[@@noalloc]letunsafe_setvnb=leti=nlsr3inletc=bytes_unsafe_getv.bitsiinletmask=1lsl(nland7)inbytes_unsafe_setv.bitsi(ifbthenclormaskelseclandlnotmask)letsetvnb=ifn<0||n>=v.lengththeninvalid_arg"Miou_unix.Bitv.set";unsafe_setvnb;ifbthen(ifn+1>v.hithenv.hi<-n+1)elseifn+1=v.hithenv.hi<-miou_bitv_clzv.bitsletntz=Array.make2560let()=fori=0to7dontz.(1lsli)<-idoneletntz8x=Array.unsafe_getntzxletrec_visit~fnidxx=ifx!=0thenbeginletb=xland-xinfn(idx+ntz8b);_visit~fnidx(x-b)endletiterfnv=fori=0toBytes.lengthv.bits-1doletc=bytes_unsafe_getv.bitsiinletidx=ilsl3in_visit~fnidxcdoneexternalmiou_bitv_next:bytes->(int[@untagged])="miou_bitv_next_bytecode""miou_bitv_next_native"[@@noalloc]letnextv=letn=miou_bitv_nextv.bitsinifn<v.lengththenSomenelseNoneletmaxv=v.hi