12345678910111213141516171819202122232425262728293031323334353637383940414243444546474849505152535455565758596061626364656667686970717273747576777879808182838485868788899091929394959697(* 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}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==0then{length=n;bits=Bytes.makeq(Char.chrinitv)}elsebeginlets=Bytes.make(q+1)(Char.chrinitv)inbytes_unsafe_setsq(initvlandlow_mask.(r));{length=n;bits=s}endletunsafe_getvn=leti=nlsr3inbytes_unsafe_getv.bitsiland(1lsl(nland7))>0letgetvn=ifn<0||n>=v.lengththeninvalid_arg"Miou_unix.Bitv.get";unsafe_getvnletunsafe_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_setvnbletntz=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.lengththenSomenelseNoneexternalmiou_bitv_clz:bytes->(int[@untagged])="miou_bitv_clz_bytecode""miou_bitv_clz_native"[@@noalloc]letmaxv=miou_bitv_clzv.bits