1234567891011121314151617181920212223242526272829303132333435363738394041424344454647484950515253545556575859606162636465666768697071727374757677787980818283848586878889909192939495969798991001011021031041051061071081091101111121131141151161171181191201211221231241251261271281291301311321331341351361371381391401411421431441451461471481491501511521531541551561571581591601611621631641651661671681691701711721731741751761771781791801811821831841851861871881891901911921931941951961971981992002012022032042052062072082092102112122132142152162172182192202212222232242252262272282292302312322332342352362372382392402412422432442452462472482492502512522532542552562572582592602612622632642652662672682692702712722732742752762772782792802812822832842852862872882892902912922932942952962972982993003013023033043053063073083093103113123133143153163173183193203213223233243253263273283293303313323333343353363373383393403413423433443453463473483493503513523533543553563573583593603613623633643653663673683693703713723733743753763773783793803813823833843853863873883893903913923933943953963973983994004014024034044054064074084094104114124134144154164174184194204214224234244254264274284294304314324334344354364374384394404414424434444454464474484494504514524534544554564574584594604614624634644654664674684694704714724734744754764774784794804814824834844854864874884894904914924934944954964974984995005015025035045055065075085095105115125135145155165175185195205215225235245255265275285295305315325335345355365375385395405415425435445455465475485495505515525535545555565575585595605615625635645655665675685695705715725735745755765775785795805815825835845855865875885895905915925935945955965975985996006016026036046056066076086096106116126136146156166176186196206216226236246256266276286296306316326336346356366376386396406416426436446456466476486496506516526536546556566576586596606616626636646656666676686696706716726736746756766776786796806816826836846856866876886896906916926936946956966976986997007017027037047057067077087097107117127137147157167177187197207217227237247257267277287297307317327337347357367377387397407417427437447457467477487497507517527537547557567577587597607617627637647657667677687697707717727737747757767777787797807817827837847857867877887897907917927937947957967977987998008018028038048058068078088098108118128138148158168178188198208218228238248258268278288298308318328338348358368378388398408418428438448458468478488498508518528538548558568578588598608618628638648658668678688698708718728738748758768778788798808818828838848858868878888898908918928938948958968978988999009019029039049059069079089099109119129139149159169179189199209219229239249259269279289299309319329339349359369379389399409419429439449459469479489499509519529539549559569579589599609619629639649659669679689699709719729739749759769779789799809819829839849859869879889899909919929939949959969979989991000100110021003100410051006100710081009101010111012101310141015101610171018101910201021102210231024102510261027102810291030103110321033103410351036103710381039104010411042104310441045104610471048104910501051105210531054105510561057105810591060106110621063106410651066106710681069107010711072107310741075107610771078107910801081108210831084108510861087108810891090109110921093109410951096109710981099110011011102110311041105110611071108110911101111111211131114111511161117111811191120112111221123112411251126112711281129113011311132113311341135113611371138113911401141114211431144114511461147114811491150115111521153115411551156115711581159116011611162116311641165116611671168116911701171117211731174117511761177117811791180118111821183118411851186118711881189119011911192119311941195119611971198119912001201120212031204120512061207120812091210121112121213121412151216121712181219122012211222122312241225122612271228122912301231123212331234123512361237123812391240124112421243124412451246124712481249125012511252125312541255125612571258125912601261126212631264126512661267126812691270127112721273127412751276127712781279128012811282128312841285128612871288128912901291129212931294129512961297129812991300130113021303130413051306130713081309131013111312131313141315131613171318131913201321132213231324132513261327132813291330133113321333133413351336133713381339134013411342134313441345134613471348134913501351135213531354135513561357135813591360136113621363136413651366136713681369137013711372137313741375137613771378137913801381138213831384138513861387138813891390139113921393139413951396139713981399140014011402140314041405140614071408140914101411141214131414141514161417141814191420142114221423142414251426142714281429143014311432143314341435143614371438143914401441144214431444144514461447144814491450145114521453145414551456145714581459146014611462146314641465146614671468146914701471147214731474typeint8=inttypeint16=inttypeint32=Int32.ttypeint24=inttypeint64=Int64.ttypeint40=int64typeint48=int64typeint56=int64typeint128typeuint8=inttypeuint16=inttypeuint24=inttypeuint32typeuint64typeuint40=uint64typeuint48=uint64typeuint56=uint64typeuint128moduletypeInt=sigtypetvalzero:tvalone:tvalmax_int:tvalmin_int:tvalbits:intval(+):t->t->tval(-):t->t->tval(*):t->t->tval(/):t->t->tvaladd:t->t->tvalsub:t->t->tvalmul:t->t->tvaldiv:t->t->tvalrem:t->t->tvalsucc:t->tvalpred:t->tvalabs:t->tvalneg:t->tvallogand:t->t->tvallogor:t->t->tvallogxor:t->t->tvallognot:t->tvalshift_left:t->int->tvalshift_right:t->int->tvalshift_right_logical:t->int->tvalof_int:int->tvalto_int:t->intvalof_float:float->tvalto_float:t->floatvalof_nativeint:nativeint->tvalto_nativeint:t->nativeintvalof_int8:int8->tvalto_int8:t->int8valof_int16:int16->tvalto_int16:t->int16valof_int24:int24->tvalto_int24:t->int24valof_int32:int32->tvalto_int32:t->int32valof_int40:int40->tvalto_int40:t->int40valof_int48:int48->tvalto_int48:t->int48valof_int56:int56->tvalto_int56:t->int56valof_int64:int64->tvalto_int64:t->int64valof_int128:int128->tvalto_int128:t->int128valof_uint8:uint8->tvalto_uint8:t->uint8valof_uint16:uint16->tvalto_uint16:t->uint16valof_uint24:uint24->tvalto_uint24:t->uint24valof_uint32:uint32->tvalto_uint32:t->uint32valof_uint40:uint40->tvalto_uint40:t->uint40valof_uint48:uint48->tvalto_uint48:t->uint48valof_uint56:uint56->tvalto_uint56:t->uint56valof_uint64:uint64->tvalto_uint64:t->uint64valof_uint128:uint128->tvalto_uint128:t->uint128valof_substring:string->pos:int->(t*int)valof_string:string->tvalto_string:t->stringvalto_string_bin:t->stringvalto_string_oct:t->stringvalto_string_hex:t->stringvalprinter:Format.formatter->t->unitvalprinter_bin:Format.formatter->t->unitvalprinter_oct:Format.formatter->t->unitvalprinter_hex:Format.formatter->t->unitvalof_bytes_big_endian:Bytes.t->int->tvalof_bytes_little_endian:Bytes.t->int->tvalto_bytes_big_endian:t->Bytes.t->int->unitvalto_bytes_little_endian:t->Bytes.t->int->unitvalcompare:t->t->intendmoduleInt8=structmoduleBase=structincludeInt_wrapper.Make_signed(structletbits=8end)letfmt="hh"letname="Int8"endincludeBaseexternalof_nativeint:nativeint->int8="int8_of_nativeint"externalof_float:float->int8="int8_of_float"externalof_int8:int8->int8="%identity"externalof_int16:int16->int8="int8_of_int16"externalof_int24:int24->int8="int8_of_int24"externalof_int32:int32->int8="int8_of_int32"externalof_int40:int40->int8="int8_of_int40"externalof_int48:int48->int8="int8_of_int48"externalof_int56:int56->int8="int8_of_int56"externalof_int64:int64->int8="int8_of_int64"externalof_int128:int128->int8="int8_of_int128"externalof_uint8:uint8->int8="int8_of_uint8"externalof_uint16:uint16->int8="int8_of_uint16"externalof_uint24:uint24->int8="int8_of_uint24"externalof_uint32:uint32->int8="int8_of_uint32"externalof_uint40:uint40->int8="int8_of_uint40"externalof_uint48:uint48->int8="int8_of_uint48"externalof_uint56:uint56->int8="int8_of_uint56"externalof_uint64:uint64->int8="int8_of_uint64"externalof_uint128:uint128->int8="int8_of_uint128"externalto_nativeint:int8->nativeint="nativeint_of_int8"externalto_float:int8->float="float_of_int8"externalto_int8:int8->int8="%identity"externalto_int16:int8->int16="int16_of_int8"externalto_int24:int8->int24="int24_of_int8"externalto_int32:int8->int32="int32_of_int8"externalto_int40:int8->int40="int40_of_int8"externalto_int48:int8->int48="int48_of_int8"externalto_int56:int8->int56="int56_of_int8"externalto_int64:int8->int64="int64_of_int8"externalto_int128:int8->int128="int128_of_int8"externalto_uint8:int8->uint8="uint8_of_int8"externalto_uint16:int8->uint16="uint16_of_int8"externalto_uint24:int8->uint24="uint24_of_int8"externalto_uint32:int8->uint32="uint32_of_int8"externalto_uint40:int8->uint40="uint40_of_int8"externalto_uint48:int8->uint48="uint48_of_int8"externalto_uint56:int8->uint56="uint56_of_int8"externalto_uint64:int8->uint64="uint64_of_int8"externalto_uint128:int8->uint128="uint128_of_int8"externalbits_of_float:float->int8="int8_bits_of_float"externalfloat_of_bits:int8->float="int8_float_of_bits"moduleConv=Str_conv.Make(Base)include(Conv:moduletypeofConvwithtypet:=int8)moduleEndian=Bytes_conv.Make(Base)include(Endian:moduletypeofEndianwithtypet:=int8)moduleInf=Infix.Make(Base)include(Inf:moduletypeofInfwithtypet:=int8)endmoduleInt16=structmoduleBase=structincludeInt_wrapper.Make_signed(structletbits=16end)letfmt="h"letname="int16"endincludeBaseexternalof_nativeint:nativeint->int16="int16_of_nativeint"externalof_float:float->int16="int16_of_float"externalof_int8:int8->int16="int16_of_int8"externalof_int16:int16->int16="%identity"externalof_int24:int24->int16="int16_of_int24"externalof_int32:int32->int16="int16_of_int32"externalof_int40:int40->int16="int16_of_int40"externalof_int48:int48->int16="int16_of_int48"externalof_int56:int56->int16="int16_of_int56"externalof_int64:int64->int16="int16_of_int64"externalof_int128:int128->int16="int16_of_int128"externalof_uint8:uint8->int16="int16_of_uint8"externalof_uint16:uint16->int16="int16_of_uint16"externalof_uint24:uint24->int16="int16_of_uint24"externalof_uint32:uint32->int16="int16_of_uint32"externalof_uint40:uint40->int16="int16_of_uint40"externalof_uint48:uint48->int16="int16_of_uint48"externalof_uint56:uint56->int16="int16_of_uint56"externalof_uint64:uint64->int16="int16_of_uint64"externalof_uint128:uint128->int16="int16_of_uint128"externalto_nativeint:int16->nativeint="nativeint_of_int16"externalto_float:int16->float="float_of_int16"externalto_int8:int16->int8="int8_of_int16"externalto_int16:int16->int16="%identity"externalto_int24:int16->int24="int24_of_int16"externalto_int32:int16->int32="int32_of_int16"externalto_int40:int16->int40="int40_of_int16"externalto_int48:int16->int48="int48_of_int16"externalto_int56:int16->int56="int56_of_int16"externalto_int64:int16->int64="int64_of_int16"externalto_int128:int16->int128="int128_of_int16"externalto_uint8:int16->uint8="uint8_of_int16"externalto_uint16:int16->uint16="uint16_of_int16"externalto_uint24:int16->uint24="uint24_of_int16"externalto_uint32:int16->uint32="uint32_of_int16"externalto_uint40:int16->uint40="uint40_of_int16"externalto_uint48:int16->uint48="uint48_of_int16"externalto_uint56:int16->uint56="uint56_of_int16"externalto_uint64:int16->uint64="uint64_of_int16"externalto_uint128:int16->uint128="uint128_of_int16"externalbits_of_float:float->int16="int16_bits_of_float"externalfloat_of_bits:int16->float="int16_float_of_bits"moduleConv=Str_conv.Make(Base)include(Conv:moduletypeofConvwithtypet:=int16)moduleEndian=Bytes_conv.Make(Base)include(Endian:moduletypeofEndianwithtypet:=int16)moduleInf=Infix.Make(Base)include(Inf:moduletypeofInfwithtypet:=int16)endmoduleInt24=structmoduleBase=structincludeInt_wrapper.Make_signed(structletbits=24end)letfmt="l"letname="Int24"endincludeBaseexternalof_nativeint:nativeint->int24="int24_of_nativeint"externalof_float:float->int24="int24_of_float"externalof_int8:int8->int24="int24_of_int8"externalof_int16:int16->int24="int24_of_int16"externalof_int24:int24->int24="%identity"externalof_int32:int32->int24="int24_of_int32"externalof_int40:int40->int24="int24_of_int40"externalof_int48:int48->int24="int24_of_int48"externalof_int56:int56->int24="int24_of_int56"externalof_int64:int64->int24="int24_of_int64"externalof_int128:int128->int24="int24_of_int128"externalof_uint8:uint8->int24="int24_of_uint8"externalof_uint16:uint16->int24="int24_of_uint16"externalof_uint24:uint24->int24="int24_of_uint24"externalof_uint32:uint32->int24="int24_of_uint32"externalof_uint40:uint40->int24="int24_of_uint40"externalof_uint48:uint48->int24="int24_of_uint48"externalof_uint56:uint56->int24="int24_of_uint56"externalof_uint64:uint64->int24="int24_of_uint64"externalof_uint128:uint128->int24="int24_of_uint128"externalto_nativeint:int24->nativeint="nativeint_of_int24"externalto_float:int24->float="float_of_int24"externalto_int8:int24->int8="int8_of_int24"externalto_int16:int24->int16="int16_of_int24"externalto_int24:int24->int24="%identity"externalto_int32:int24->int32="int32_of_int24"externalto_int40:int24->int40="int40_of_int24"externalto_int48:int24->int48="int48_of_int24"externalto_int56:int24->int56="int56_of_int24"externalto_int64:int24->int64="int64_of_int24"externalto_int128:int24->int128="int128_of_int24"externalto_uint8:int24->uint8="uint8_of_int24"externalto_uint16:int24->uint16="uint16_of_int24"externalto_uint24:int24->uint24="uint24_of_int24"externalto_uint32:int24->uint32="uint32_of_int24"externalto_uint40:int24->uint40="uint40_of_int24"externalto_uint48:int24->uint48="uint48_of_int24"externalto_uint56:int24->uint56="uint56_of_int24"externalto_uint64:int24->uint64="uint64_of_int24"externalto_uint128:int24->uint128="uint128_of_int24"moduleConv=Str_conv.Make(Base)include(Conv:moduletypeofConvwithtypet:=int24)moduleEndian=Bytes_conv.Make(Base)include(Endian:moduletypeofEndianwithtypet:=int24)moduleInf=Infix.Make(Base)include(Inf:moduletypeofInfwithtypet:=int24)endmoduleInt32=structmoduleBase=structincludeInt32letbits=32letfmt="l"letname="int32"letdivmod=(funxy->divxy,remxy)endincludeBaseletof_nativeint=Nativeint.to_int32letto_nativeint=Nativeint.of_int32externalof_int8:int8->int32="int32_of_int8"externalof_int16:int16->int32="int32_of_int16"externalof_int24:int24->int32="int32_of_int24"externalof_int32:int32->int32="%identity"externalof_int40:int40->int32="int32_of_int40"externalof_int48:int48->int32="int32_of_int48"externalof_int56:int56->int32="int32_of_int56"externalof_int64:int64->int32="int32_of_int64"externalof_int128:int128->int32="int32_of_int128"externalof_uint8:uint8->int32="int32_of_uint8"externalof_uint16:uint16->int32="int32_of_uint16"externalof_uint24:uint24->int32="int32_of_uint24"externalof_uint32:uint32->int32="int32_of_uint32"externalof_uint40:uint40->int32="int32_of_uint40"externalof_uint48:uint48->int32="int32_of_uint48"externalof_uint56:uint56->int32="int32_of_uint56"externalof_uint64:uint64->int32="int32_of_uint64"externalof_uint128:uint128->int32="int32_of_uint128"externalto_int8:int32->int8="int8_of_int32"externalto_int16:int32->int16="int16_of_int32"externalto_int24:int32->int24="int24_of_int32"externalto_int32:int32->int32="%identity"externalto_int40:int32->int40="int40_of_int32"externalto_int48:int32->int48="int48_of_int32"externalto_int56:int32->int56="int56_of_int32"externalto_int64:int32->int64="int64_of_int32"externalto_int128:int32->int128="int128_of_int32"externalto_uint8:int32->uint8="uint8_of_int32"externalto_uint16:int32->uint16="uint16_of_int32"externalto_uint24:int32->uint24="uint24_of_int32"externalto_uint32:int32->uint32="uint32_of_int32"externalto_uint40:int32->uint40="uint40_of_int32"externalto_uint48:int32->uint48="uint48_of_int32"externalto_uint56:int32->uint56="uint56_of_int32"externalto_uint64:int32->uint64="uint64_of_int32"externalto_uint128:int32->uint128="uint128_of_int32"moduleConv=Str_conv.Make(Base)include(Conv:moduletypeofConvwithtypet:=int32)moduleEndian=Bytes_conv.Make(Base)include(Endian:moduletypeofEndianwithtypet:=int32)moduleInf=Infix.Make(Base)include(Inf:moduletypeofInfwithtypet:=int32)endmoduleInt64=structmoduleBase=structincludeInt64letbits=64letfmt="ll"letname="int64"letdivmod=(funxy->divxy,remxy)endincludeBaseexternalof_int8:int8->int64="int64_of_int8"externalof_int16:int16->int64="int64_of_int16"externalof_int24:int24->int64="int64_of_int24"externalof_int32:int32->int64="int64_of_int32"externalof_int40:int40->int64="int64_of_int40"externalof_int48:int48->int64="int64_of_int48"externalof_int56:int56->int64="int64_of_int56"externalof_int64:int64->int64="%identity"externalof_int128:int128->int64="int64_of_int128"externalof_uint8:uint8->int64="int64_of_uint8"externalof_uint16:uint16->int64="int64_of_uint16"externalof_uint24:uint24->int64="int64_of_uint24"externalof_uint32:uint32->int64="int64_of_uint32"externalof_uint40:uint40->int64="int64_of_uint40"externalof_uint48:uint48->int64="int64_of_uint48"externalof_uint56:uint56->int64="int64_of_uint56"externalof_uint64:uint64->int64="int64_of_uint64"externalof_uint128:uint128->int64="int64_of_uint128"externalto_int8:int64->int8="int8_of_int64"externalto_int16:int64->int16="int16_of_int64"externalto_int24:int64->int24="int24_of_int64"externalto_int32:int64->int32="int32_of_int64"externalto_int40:int64->int40="int40_of_int64"externalto_int48:int64->int48="int48_of_int64"externalto_int56:int64->int56="int56_of_int64"externalto_int64:int64->int64="%identity"externalto_int128:int64->int128="int128_of_int64"externalto_uint8:int64->uint8="uint8_of_int64"externalto_uint16:int64->uint16="uint16_of_int64"externalto_uint24:int64->uint24="uint24_of_int64"externalto_uint32:int64->uint32="uint32_of_int64"externalto_uint40:int64->uint40="uint40_of_int64"externalto_uint48:int64->uint48="uint48_of_int64"externalto_uint56:int64->uint56="uint56_of_int64"externalto_uint64:int64->uint64="uint64_of_int64"externalto_uint128:int64->uint128="uint128_of_int64"moduleConv=Str_conv.Make(Base)include(Conv:moduletypeofConvwithtypet:=int64)moduleEndian=Bytes_conv.Make(Base)include(Endian:moduletypeofEndianwithtypet:=int64)moduleInf=Infix.Make(Base)include(Inf:moduletypeofInfwithtypet:=int64)endmoduleInt40=struct(* int40 is modeled as int64, where only the UPPER 40 bits are used;
this has the advantage that most operations are identical to the int64 ones.
The post-condition of all int40 opertaions is, that the LOWER 24 bit are 0x000000.
Only operations that are not identical or do not preserve the post-condition are implemented.
*)moduleBase=structincludeInt64.Baseletbits=40letfmt="ll"letname="Int40"externalmul:int40->int40->int40="int40_mul"externaldiv:int40->int40->int40="int40_div"externallogxor:int40->int40->int40="uint40_xor"externalshift_right:int40->int->int40="int40_shift_right"externalshift_right_logical:int40->int->int40="uint40_shift_right"externalof_int:int->int40="int40_of_int"externalof_nativeint:nativeint->int40="int40_of_nativeint"externalof_float:float->int40="int40_of_float"externalof_int8:int8->int40="int40_of_int8"externalof_int16:int16->int40="int40_of_int16"externalof_int24:int24->int40="int40_of_int24"externalof_int32:int32->int40="int40_of_int32"externalof_int40:int40->int40="%identity"externalof_int48:int48->int40="int40_of_int48"externalof_int56:int56->int40="int40_of_int56"externalof_int64:int64->int40="int40_of_int64"externalof_int128:int128->int40="int40_of_int128"externalof_uint8:uint8->int40="int40_of_uint8"externalof_uint16:uint16->int40="int40_of_uint16"externalof_uint24:uint24->int40="int40_of_uint24"externalof_uint32:uint32->int40="int40_of_uint32"externalof_uint40:uint40->int40="int40_of_uint40"externalof_uint48:uint48->int40="int40_of_uint48"externalof_uint56:uint56->int40="int40_of_uint56"externalof_uint64:uint64->int40="int40_of_uint64"externalof_uint128:uint128->int40="int40_of_uint128"externalto_int:int40->int="int_of_int40"externalto_nativeint:int40->nativeint="nativeint_of_int40"externalto_float:int40->float="float_of_int40"externalto_int8:int40->int8="int8_of_int40"externalto_int16:int40->int16="int16_of_int40"externalto_int24:int40->int24="int24_of_int40"externalto_int32:int40->int32="int32_of_int40"externalto_int40:int40->int40="%identity"externalto_int48:int40->int48="int48_of_int40"externalto_int56:int40->int56="int56_of_int40"externalto_int64:int40->int64="int64_of_int40"externalto_int128:int40->int128="int128_of_int40"externalto_uint8:int40->uint8="uint8_of_int40"externalto_uint16:int40->uint16="uint16_of_int40"externalto_uint24:int40->uint24="uint24_of_int40"externalto_uint32:int40->uint32="uint32_of_int40"externalto_uint40:int40->uint40="uint40_of_int40"externalto_uint48:int40->uint48="uint48_of_int40"externalto_uint56:int40->uint56="uint56_of_int40"externalto_uint64:int40->uint64="uint64_of_int40"externalto_uint128:int40->uint128="uint128_of_int40"externalmax_int_fun:unit->int40="int40_max_int"externalmin_int_fun:unit->int40="int40_min_int"letone=of_int1letmax_int=max_int_fun()letmin_int=min_int_fun()letlognot=logxormax_intletcompare=Stdint_stdlib_.compareletdivmod=(funxy->divxy,remxy)endincludeBasemoduleConv=Str_conv.Make(Base)include(Conv:moduletypeofConvwithtypet:=int40)moduleEndian=Bytes_conv.Make(Base)include(Endian:moduletypeofEndianwithtypet:=int40)moduleInf=Infix.Make(Base)include(Inf:moduletypeofInfwithtypet:=int40)endmoduleInt48=struct(* int48 is modeled as int64, where only the UPPER 48 bits are used;
this has the advantage that most operations are identical to the int64 ones.
The post-condition of all int48 opertaions is, that the LOWER 16 bit are 0x0000.
Only operations that are not identical or do not preserve the post-condition are implemented.
*)moduleBase=structincludeInt64.Baseletbits=48letfmt="ll"letname="Int48"externalmul:int48->int48->int48="int48_mul"externaldiv:int48->int48->int48="int48_div"externallogxor:int48->int48->int48="uint48_xor"externalshift_right:int48->int->int48="int48_shift_right"externalshift_right_logical:int48->int->int48="uint48_shift_right"externalof_int:int->int48="int48_of_int"externalof_nativeint:nativeint->int48="int48_of_nativeint"externalof_float:float->int48="int48_of_float"externalof_int8:int8->int48="int48_of_int8"externalof_int16:int16->int48="int48_of_int16"externalof_int24:int24->int48="int48_of_int24"externalof_int32:int32->int48="int48_of_int32"externalof_int40:int40->int48="int48_of_int40"externalof_int48:int48->int48="%identity"externalof_int56:int56->int48="int48_of_int56"externalof_int64:int64->int48="int48_of_int64"externalof_int128:int128->int48="int48_of_int128"externalof_uint8:uint8->int48="int48_of_uint8"externalof_uint16:uint16->int48="int48_of_uint16"externalof_uint24:uint24->int48="int48_of_uint24"externalof_uint32:uint32->int48="int48_of_uint32"externalof_uint40:uint40->int48="int48_of_uint40"externalof_uint48:uint48->int48="int48_of_uint48"externalof_uint56:uint56->int48="int48_of_uint56"externalof_uint64:uint64->int48="int48_of_uint64"externalof_uint128:uint128->int48="int48_of_uint128"externalto_int:int48->int="int_of_int48"externalto_nativeint:int48->nativeint="nativeint_of_int48"externalto_float:int48->float="float_of_int48"externalto_int8:int48->int8="int8_of_int48"externalto_int16:int48->int16="int16_of_int48"externalto_int24:int48->int24="int24_of_int48"externalto_int32:int48->int32="int32_of_int48"externalto_int40:int48->int40="int40_of_int48"externalto_int48:int48->int48="%identity"externalto_int56:int48->int56="int56_of_int48"externalto_int64:int48->int64="int64_of_int48"externalto_int128:int48->int128="int128_of_int48"externalto_uint8:int48->uint8="uint8_of_int48"externalto_uint16:int48->uint16="uint16_of_int48"externalto_uint24:int48->uint24="uint24_of_int48"externalto_uint32:int48->uint32="uint32_of_int48"externalto_uint40:int48->uint40="uint40_of_int48"externalto_uint48:int48->uint48="uint48_of_int48"externalto_uint56:int48->uint56="uint56_of_int48"externalto_uint64:int48->uint64="uint64_of_int48"externalto_uint128:int48->uint128="uint128_of_int48"externalmax_int_fun:unit->int48="int48_max_int"externalmin_int_fun:unit->int48="int48_min_int"letone=of_int1letmax_int=max_int_fun()letmin_int=min_int_fun()letlognot=logxormax_intletcompare=Stdint_stdlib_.compareletdivmod=(funxy->divxy,remxy)endincludeBasemoduleConv=Str_conv.Make(Base)include(Conv:moduletypeofConvwithtypet:=int48)moduleEndian=Bytes_conv.Make(Base)include(Endian:moduletypeofEndianwithtypet:=int48)moduleInf=Infix.Make(Base)include(Inf:moduletypeofInfwithtypet:=int48)endmoduleInt56=struct(* int56 is modeled as int64, where only the UPPER 56 bits are used;
this has the advantage that most operations are identical to the int64 ones.
The post-condition of all int56 opertaions is, that the LOWER 8 bit are 0x00.
Only operations that are not identical or do not preserve the post-condition are implemented.
*)moduleBase=structincludeInt64.Baseletbits=56letfmt="ll"letname="Int56"externalmul:int56->int56->int56="int56_mul"externaldiv:int56->int56->int56="int56_div"externallogxor:int56->int56->int56="uint56_xor"externalshift_right:int56->int->int56="int56_shift_right"externalshift_right_logical:int56->int->int56="uint56_shift_right"externalof_int:int->int56="int56_of_int"externalof_nativeint:nativeint->int56="int56_of_nativeint"externalof_float:float->int56="int56_of_float"externalof_int8:int8->int56="int56_of_int8"externalof_int16:int16->int56="int56_of_int16"externalof_int24:int24->int56="int56_of_int24"externalof_int32:int32->int56="int56_of_int32"externalof_int40:int40->int56="int56_of_int40"externalof_int48:int48->int56="int56_of_int48"externalof_int56:int56->int56="%identity"externalof_int64:int64->int56="int56_of_int64"externalof_int128:int128->int56="int56_of_int128"externalof_uint8:uint8->int56="int56_of_uint8"externalof_uint16:uint16->int56="int56_of_uint16"externalof_uint24:uint24->int56="int56_of_uint24"externalof_uint32:uint32->int56="int56_of_uint32"externalof_uint40:uint40->int56="int56_of_uint40"externalof_uint48:uint48->int56="int56_of_uint48"externalof_uint56:uint56->int56="int56_of_uint56"externalof_uint64:uint64->int56="int56_of_uint64"externalof_uint128:uint128->int56="int56_of_uint128"externalto_int:int56->int="int_of_int56"externalto_nativeint:int56->nativeint="nativeint_of_int56"externalto_float:int56->float="float_of_int56"externalto_int8:int56->int8="int8_of_int56"externalto_int16:int56->int16="int16_of_int56"externalto_int24:int56->int24="int24_of_int56"externalto_int32:int56->int32="int32_of_int56"externalto_int40:int56->int40="int40_of_int56"externalto_int48:int56->int48="int48_of_int56"externalto_int56:int56->int56="%identity"externalto_int64:int56->int64="int64_of_int56"externalto_int128:int56->int128="int128_of_int56"externalto_uint8:int56->uint8="uint8_of_int56"externalto_uint16:int56->uint16="uint16_of_int56"externalto_uint24:int56->uint24="uint24_of_int56"externalto_uint32:int56->uint32="uint32_of_int56"externalto_uint40:int56->uint40="uint40_of_int56"externalto_uint48:int56->uint48="uint48_of_int56"externalto_uint56:int56->uint56="uint56_of_int56"externalto_uint64:int56->uint64="uint64_of_int56"externalto_uint128:int56->uint128="uint128_of_int56"externalmax_int_fun:unit->int56="int56_max_int"externalmin_int_fun:unit->int56="int56_min_int"letone=of_int1letmax_int=max_int_fun()letmin_int=min_int_fun()letlognot=logxormax_intletcompare=Stdint_stdlib_.compareletdivmod=(funxy->divxy,remxy)endincludeBasemoduleConv=Str_conv.Make(Base)include(Conv:moduletypeofConvwithtypet:=int56)moduleEndian=Bytes_conv.Make(Base)include(Endian:moduletypeofEndianwithtypet:=int56)moduleInf=Infix.Make(Base)include(Inf:moduletypeofInfwithtypet:=int56)endmoduleInt128=structmoduleBase=structtypet=int128letbits=128letfmt="LL"letname="Int128"externaladd:int128->int128->int128="int128_add"externalsub:int128->int128->int128="int128_sub"externalmul:int128->int128->int128="int128_mul"externaldiv:int128->int128->int128="int128_div"externalrem:int128->int128->int128="int128_mod"externallogand:int128->int128->int128="int128_and"externallogor:int128->int128->int128="int128_or"externallogxor:int128->int128->int128="int128_xor"externalshift_left:int128->int->int128="int128_shift_left"externalshift_right:int128->int->int128="int128_shift_right"externalshift_right_logical:int128->int->int128="int128_shift_right"externalabs:int128->int128="int128_abs"externalneg:int128->int128="int128_neg"externalof_int:int->int128="int128_of_int"externalof_nativeint:nativeint->int128="int128_of_nativeint"externalof_float:float->int128="int128_of_float"externalof_int8:int8->int128="int128_of_int8"externalof_int16:int16->int128="int128_of_int16"externalof_int24:int24->int128="int128_of_int24"externalof_int32:int32->int128="int128_of_int32"externalof_int40:int40->int128="int128_of_int40"externalof_int48:int48->int128="int128_of_int48"externalof_int56:int56->int128="int128_of_int56"externalof_int64:int64->int128="int128_of_int64"externalof_int128:int128->int128="%identity"externalof_uint8:uint8->int128="int128_of_uint8"externalof_uint16:uint16->int128="int128_of_uint16"externalof_uint24:uint24->int128="int128_of_uint24"externalof_uint32:uint32->int128="int128_of_uint32"externalof_uint40:uint40->int128="int128_of_uint40"externalof_uint48:uint48->int128="int128_of_uint48"externalof_uint56:uint56->int128="int128_of_uint56"externalof_uint64:uint64->int128="int128_of_uint64"externalof_uint128:uint128->int128="int128_of_uint128"externalto_int:int128->int="int_of_int128"externalto_nativeint:int128->nativeint="nativeint_of_int128"externalto_float:int128->float="float_of_int128"externalto_int8:int128->int8="int8_of_int128"externalto_int16:int128->int16="int16_of_int128"externalto_int24:int128->int24="int24_of_int128"externalto_int32:int128->int32="int32_of_int128"externalto_int40:int128->int40="int40_of_int128"externalto_int48:int128->int48="int48_of_int128"externalto_int56:int128->int56="int56_of_int128"externalto_int64:int128->int64="int64_of_int128"externalto_int128:int128->int128="%identity"externalto_uint8:int128->uint8="uint8_of_int128"externalto_uint16:int128->uint16="uint16_of_int128"externalto_uint24:int128->uint24="uint24_of_int128"externalto_uint32:int128->uint32="uint32_of_int128"externalto_uint40:int128->uint40="uint40_of_int128"externalto_uint48:int128->uint48="uint48_of_int128"externalto_uint56:int128->uint56="uint56_of_int128"externalto_uint64:int128->uint64="uint64_of_int128"externalto_uint128:int128->uint128="uint128_of_int128"externalmax_int_fun:unit->int128="int128_max_int"externalmin_int_fun:unit->int128="int128_min_int"letzero=of_int0letone=of_int1letsucc=addoneletpredx=subxoneletmax_int=max_int_fun()letmin_int=min_int_fun()letlognot=logxormax_intletcompare=Stdint_stdlib_.compareletdivmod=(funxy->divxy,remxy)externalinit_custom_ops:unit->unit="int128_init_custom_ops"let()=init_custom_ops()endincludeBasemoduleConv=Str_conv.Make(Base)include(Conv:moduletypeofConvwithtypet:=int128)moduleEndian=Bytes_conv.Make(Base)include(Endian:moduletypeofEndianwithtypet:=int128)moduleInf=Infix.Make(Base)include(Inf:moduletypeofInfwithtypet:=int128)endmoduleUint8=structmoduleBase=structincludeInt_wrapper.Make_unsigned(structletbits=8end)letfmt="Uhh"letname="Uint8"endincludeBaseexternalof_nativeint:nativeint->uint8="uint8_of_nativeint"externalof_float:float->uint8="uint8_of_float"externalof_int8:int8->uint8="uint8_of_int8"externalof_int16:int16->uint8="uint8_of_int16"externalof_int24:int24->uint8="uint8_of_int24"externalof_int32:int32->uint8="uint8_of_int32"externalof_int40:int40->uint8="uint8_of_int40"externalof_int48:int48->uint8="uint8_of_int48"externalof_int56:int56->uint8="uint8_of_int56"externalof_int64:int64->uint8="uint8_of_int64"externalof_int128:int128->uint8="uint8_of_int128"externalof_uint8:uint8->uint8="%identity"externalof_uint16:uint16->uint8="uint8_of_uint16"externalof_uint24:uint24->uint8="uint8_of_uint24"externalof_uint32:uint32->uint8="uint8_of_uint32"externalof_uint40:uint40->uint8="uint8_of_uint40"externalof_uint48:uint48->uint8="uint8_of_uint48"externalof_uint56:uint56->uint8="uint8_of_uint56"externalof_uint64:uint64->uint8="uint8_of_uint64"externalof_uint128:uint128->uint8="uint8_of_uint128"externalto_nativeint:uint8->nativeint="nativeint_of_uint8"externalto_float:uint8->float="float_of_uint8"externalto_int8:uint8->int8="int8_of_uint8"externalto_int16:uint8->int16="int16_of_uint8"externalto_int24:uint8->int24="int24_of_uint8"externalto_int32:uint8->int32="int32_of_uint8"externalto_int40:uint8->int40="int40_of_uint8"externalto_int48:uint8->int48="int48_of_uint8"externalto_int56:uint8->int56="int56_of_uint8"externalto_int64:uint8->int64="int64_of_uint8"externalto_int128:uint8->int128="int128_of_uint8"externalto_uint8:uint8->uint8="%identity"externalto_uint16:uint8->uint16="uint16_of_uint8"externalto_uint24:uint8->uint24="uint24_of_uint8"externalto_uint32:uint8->uint32="uint32_of_uint8"externalto_uint40:uint8->uint40="uint40_of_uint8"externalto_uint48:uint8->uint48="uint48_of_uint8"externalto_uint56:uint8->uint56="uint56_of_uint8"externalto_uint64:uint8->uint64="uint64_of_uint8"externalto_uint128:uint8->uint128="uint128_of_uint8"moduleConv=Str_conv.Make(Base)include(Conv:moduletypeofConvwithtypet:=uint8)moduleEndian=Bytes_conv.Make(Base)include(Endian:moduletypeofEndianwithtypet:=uint8)moduleInf=Infix.Make(Base)include(Inf:moduletypeofInfwithtypet:=uint8)endmoduleUint16=structmoduleBase=structincludeInt_wrapper.Make_unsigned(structletbits=16end)letfmt="Uh"letname="Uint16"endincludeBaseexternalof_nativeint:nativeint->uint16="uint16_of_nativeint"externalof_float:float->uint16="uint16_of_float"externalof_int8:int8->uint16="uint16_of_int8"externalof_int16:int16->uint16="uint16_of_int16"externalof_int24:int24->uint16="uint16_of_int24"externalof_int32:int32->uint16="uint16_of_int32"externalof_int40:int40->uint16="uint16_of_int40"externalof_int48:int48->uint16="uint16_of_int48"externalof_int56:int56->uint16="uint16_of_int56"externalof_int64:int64->uint16="uint16_of_int64"externalof_int128:int128->uint16="uint16_of_int128"externalof_uint8:uint8->uint16="uint16_of_uint8"externalof_uint16:uint16->uint16="%identity"externalof_uint24:uint24->uint16="uint16_of_uint24"externalof_uint32:uint32->uint16="uint16_of_uint32"externalof_uint40:uint40->uint16="uint16_of_uint40"externalof_uint48:uint48->uint16="uint16_of_uint48"externalof_uint56:uint56->uint16="uint16_of_uint56"externalof_uint64:uint64->uint16="uint16_of_uint64"externalof_uint128:uint128->uint16="uint16_of_uint128"externalto_nativeint:uint16->nativeint="nativeint_of_uint16"externalto_float:uint16->float="float_of_uint16"externalto_int8:uint16->int8="int8_of_uint16"externalto_int16:uint16->int16="int16_of_uint16"externalto_int24:uint16->int24="int24_of_uint16"externalto_int32:uint16->int32="int32_of_uint16"externalto_int40:uint16->int40="int40_of_uint16"externalto_int48:uint16->int48="int48_of_uint16"externalto_int56:uint16->int56="int56_of_uint16"externalto_int64:uint16->int64="int64_of_uint16"externalto_int128:uint16->int128="int128_of_uint16"externalto_uint8:uint16->uint8="uint8_of_uint16"externalto_uint16:uint16->uint16="%identity"externalto_uint24:uint16->uint24="uint24_of_uint16"externalto_uint32:uint16->uint32="uint32_of_uint16"externalto_uint40:uint16->uint40="uint40_of_uint16"externalto_uint48:uint16->uint48="uint48_of_uint16"externalto_uint56:uint16->uint56="uint56_of_uint16"externalto_uint64:uint16->uint64="uint64_of_uint16"externalto_uint128:uint16->uint128="uint128_of_uint16"moduleConv=Str_conv.Make(Base)include(Conv:moduletypeofConvwithtypet:=uint16)moduleEndian=Bytes_conv.Make(Base)include(Endian:moduletypeofEndianwithtypet:=uint16)moduleInf=Infix.Make(Base)include(Inf:moduletypeofInfwithtypet:=uint16)endmoduleUint24=structmoduleBase=structincludeInt_wrapper.Make_unsigned(structletbits=24end)letfmt="Ul"letname="Uint24"endincludeBaseexternalof_nativeint:nativeint->uint24="uint24_of_nativeint"externalof_float:float->uint24="uint24_of_float"externalof_int8:int8->uint24="uint24_of_int8"externalof_int16:int16->uint24="uint24_of_int16"externalof_int24:int24->uint24="uint24_of_int24"externalof_int32:int32->uint24="uint24_of_int32"externalof_int40:int40->uint24="uint24_of_int40"externalof_int48:int48->uint24="uint24_of_int48"externalof_int56:int56->uint24="uint24_of_int56"externalof_int64:int64->uint24="uint24_of_int64"externalof_int128:int128->uint24="uint24_of_int128"externalof_uint8:uint8->uint24="uint24_of_uint8"externalof_uint16:uint16->uint24="uint24_of_uint16"externalof_uint24:uint24->uint24="%identity"externalof_uint32:uint32->uint24="uint24_of_uint32"externalof_uint40:uint40->uint24="uint24_of_uint40"externalof_uint48:uint48->uint24="uint24_of_uint48"externalof_uint56:uint56->uint24="uint24_of_uint56"externalof_uint64:uint64->uint24="uint24_of_uint64"externalof_uint128:uint128->uint24="uint24_of_uint128"externalto_nativeint:uint24->nativeint="nativeint_of_uint24"externalto_float:uint24->float="float_of_uint24"externalto_int8:uint24->int8="int8_of_uint24"externalto_int16:uint24->int16="int16_of_uint24"externalto_int24:uint24->int24="int24_of_uint24"externalto_int32:uint24->int32="int32_of_uint24"externalto_int40:uint24->int40="int40_of_uint24"externalto_int48:uint24->int48="int48_of_uint24"externalto_int56:uint24->int56="int56_of_uint24"externalto_int64:uint24->int64="int64_of_uint24"externalto_int128:uint24->int128="int128_of_uint24"externalto_uint8:uint24->uint8="uint8_of_uint24"externalto_uint16:uint24->uint16="uint16_of_uint24"externalto_uint24:uint24->uint24="%identity"externalto_uint32:uint24->uint32="uint32_of_uint24"externalto_uint40:uint24->uint40="uint40_of_uint24"externalto_uint48:uint24->uint48="uint48_of_uint24"externalto_uint56:uint24->uint56="uint56_of_uint24"externalto_uint64:uint24->uint64="uint64_of_uint24"externalto_uint128:uint24->uint128="uint128_of_uint24"moduleConv=Str_conv.Make(Base)include(Conv:moduletypeofConvwithtypet:=uint24)moduleEndian=Bytes_conv.Make(Base)include(Endian:moduletypeofEndianwithtypet:=uint24)moduleInf=Infix.Make(Base)include(Inf:moduletypeofInfwithtypet:=uint24)endmoduleUint32=structmoduleBase=structtypet=uint32letbits=32letfmt="Ul"letname="Uint32"externaladd:uint32->uint32->uint32="uint32_add"externalsub:uint32->uint32->uint32="uint32_sub"externalmul:uint32->uint32->uint32="uint32_mul"externaldiv:uint32->uint32->uint32="uint32_div"externalrem:uint32->uint32->uint32="uint32_mod"externallogand:uint32->uint32->uint32="uint32_and"externallogor:uint32->uint32->uint32="uint32_or"externallogxor:uint32->uint32->uint32="uint32_xor"externalshift_left:uint32->int->uint32="uint32_shift_left"externalshift_right:uint32->int->uint32="uint32_shift_right"letshift_right_logical=shift_rightexternalabs:uint32->uint32="%identity"externalneg:uint32->uint32="uint32_neg"externalof_int:int->uint32="uint32_of_int"externalof_nativeint:nativeint->uint32="uint32_of_nativeint"externalof_float:float->uint32="uint32_of_float"externalof_int8:int8->uint32="uint32_of_int8"externalof_int16:int16->uint32="uint32_of_int16"externalof_int24:int24->uint32="uint32_of_int24"externalof_int32:int32->uint32="uint32_of_int32"externalof_int40:int40->uint32="uint32_of_int40"externalof_int48:int48->uint32="uint32_of_int48"externalof_int56:int56->uint32="uint32_of_int56"externalof_int64:int64->uint32="uint32_of_int64"externalof_int128:int128->uint32="uint32_of_int128"externalof_uint8:uint8->uint32="uint32_of_uint8"externalof_uint16:uint16->uint32="uint32_of_uint16"externalof_uint24:uint24->uint32="uint32_of_uint24"externalof_uint32:uint32->uint32="%identity"externalof_uint40:uint40->uint32="uint32_of_uint40"externalof_uint48:uint48->uint32="uint32_of_uint48"externalof_uint56:uint56->uint32="uint32_of_uint56"externalof_uint64:uint64->uint32="uint32_of_uint64"externalof_uint128:uint128->uint32="uint32_of_uint128"externalto_int:uint32->int="int_of_uint32"externalto_nativeint:uint32->nativeint="nativeint_of_uint32"externalto_float:uint32->float="float_of_uint32"externalto_int8:uint32->int8="int8_of_uint32"externalto_int16:uint32->int16="int16_of_uint32"externalto_int24:uint32->int24="int24_of_uint32"externalto_int32:uint32->int32="int32_of_uint32"externalto_int40:uint32->int40="int40_of_uint32"externalto_int48:uint32->int48="int48_of_uint32"externalto_int56:uint32->int56="int56_of_uint32"externalto_int64:uint32->int64="int64_of_uint32"externalto_int128:uint32->int128="int128_of_uint32"externalto_uint8:uint32->uint8="uint8_of_uint32"externalto_uint16:uint32->uint16="uint16_of_uint32"externalto_uint24:uint32->uint24="uint24_of_uint32"externalto_uint32:uint32->uint32="%identity"externalto_uint40:uint32->uint40="uint40_of_uint32"externalto_uint48:uint32->uint48="uint48_of_uint32"externalto_uint56:uint32->uint56="uint56_of_uint32"externalto_uint64:uint32->uint64="uint64_of_uint32"externalto_uint128:uint32->uint128="uint128_of_uint32"externalmax_int_fun:unit->uint32="uint32_max_int"letzero=of_int0letone=of_int1letsucc=addoneletpredx=subxoneletmax_int=max_int_fun()letmin_int=zeroletlognot=logxormax_intletcompare=Stdint_stdlib_.compareletdivmod=(funxy->divxy,remxy)externalinit_custom_ops:unit->unit="uint32_init_custom_ops"let()=init_custom_ops()endincludeBasemoduleConv=Str_conv.Make(Base)include(Conv:moduletypeofConvwithtypet:=uint32)moduleEndian=Bytes_conv.Make(Base)include(Endian:moduletypeofEndianwithtypet:=uint32)moduleInf=Infix.Make(Base)include(Inf:moduletypeofInfwithtypet:=uint32)endmoduleUint64=structmoduleBase=structtypet=uint64letbits=64letname="Uint64"letfmt="UL"externaladd:uint64->uint64->uint64="uint64_add"externalsub:uint64->uint64->uint64="uint64_sub"externalmul:uint64->uint64->uint64="uint64_mul"externaldiv:uint64->uint64->uint64="uint64_div"externalrem:uint64->uint64->uint64="uint64_mod"externallogand:uint64->uint64->uint64="uint64_and"externallogor:uint64->uint64->uint64="uint64_or"externallogxor:uint64->uint64->uint64="uint64_xor"externalshift_left:uint64->int->uint64="uint64_shift_left"externalshift_right:uint64->int->uint64="uint64_shift_right"letshift_right_logical=shift_rightexternalabs:uint64->uint64="%identity"externalneg:uint64->uint64="uint64_neg"externalof_int:int->uint64="uint64_of_int"externalof_nativeint:nativeint->uint64="uint64_of_nativeint"externalof_float:float->uint64="uint64_of_float"externalof_int8:int8->uint64="uint64_of_int8"externalof_int16:int16->uint64="uint64_of_int16"externalof_int24:int24->uint64="uint64_of_int24"externalof_int32:int32->uint64="uint64_of_int32"externalof_int40:int40->uint64="uint64_of_int40"externalof_int48:int48->uint64="uint64_of_int48"externalof_int56:int56->uint64="uint64_of_int56"externalof_int64:int64->uint64="uint64_of_int64"externalof_int128:int128->uint64="uint64_of_int128"externalof_uint8:uint8->uint64="uint64_of_uint8"externalof_uint16:uint16->uint64="uint64_of_uint16"externalof_uint24:uint24->uint64="uint64_of_uint24"externalof_uint32:uint32->uint64="uint64_of_uint32"externalof_uint40:uint40->uint64="uint64_of_uint40"externalof_uint48:uint48->uint64="uint64_of_uint48"externalof_uint56:uint56->uint64="uint64_of_uint56"externalof_uint64:uint64->uint64="%identity"externalof_uint128:uint128->uint64="uint64_of_uint128"externalto_int:uint64->int="int_of_uint64"externalto_nativeint:uint64->nativeint="nativeint_of_uint64"externalto_float:uint64->float="float_of_uint64"externalto_int8:uint64->int8="int8_of_uint64"externalto_int16:uint64->int16="int16_of_uint64"externalto_int24:uint64->int24="int24_of_uint64"externalto_int32:uint64->int32="int32_of_uint64"externalto_int40:uint64->int40="int40_of_uint64"externalto_int48:uint64->int48="int48_of_uint64"externalto_int56:uint64->int56="int56_of_uint64"externalto_int64:uint64->int64="int64_of_uint64"externalto_int128:uint64->int128="int128_of_uint64"externalto_uint8:uint64->uint8="uint8_of_uint64"externalto_uint16:uint64->uint16="uint16_of_uint64"externalto_uint24:uint64->uint24="uint24_of_uint64"externalto_uint32:uint64->uint32="uint32_of_uint64"externalto_uint40:uint64->uint40="uint40_of_uint64"externalto_uint48:uint64->uint48="uint48_of_uint64"externalto_uint56:uint64->uint56="uint56_of_uint64"externalto_uint64:uint64->uint64="%identity"externalto_uint128:uint64->uint128="uint128_of_uint64"externalmax_int_fun:unit->uint64="uint64_max_int"letzero=of_int0letone=of_int1letsucc=addoneletpredx=subxoneletmax_int=max_int_fun()letmin_int=zeroletlognot=logxormax_intletcompare=Stdint_stdlib_.compareletdivmod=(funxy->divxy,remxy)externalinit_custom_ops:unit->unit="uint64_init_custom_ops"let()=init_custom_ops()endincludeBasemoduleConv=Str_conv.Make(Base)include(Conv:moduletypeofConvwithtypet:=uint64)moduleEndian=Bytes_conv.Make(Base)include(Endian:moduletypeofEndianwithtypet:=uint64)moduleInf=Infix.Make(Base)include(Inf:moduletypeofInfwithtypet:=uint64)endmoduleUint40=struct(* uint40 is modeled as uint64, where only the UPPER 40 bits are used;
this has the advantage that most operations are identical to the uint64 ones.
The post-condition of all uint40 opertaions is, that the LOWER 24 bit are 0x000000.
Only operations that are not identical or do not preserve the post-condition are implemented.
*)moduleBase=structincludeUint64.Baseletbits=40letfmt="Ul"letname="Uint40"externalmul:uint40->uint40->uint40="uint40_mul"externaldiv:uint40->uint40->uint40="uint40_div"externallogxor:uint40->uint40->uint40="uint40_xor"externalshift_right:uint40->int->uint40="uint40_shift_right"letshift_right_logical=shift_rightexternalneg:uint40->uint40="uint40_neg"externalof_int:int->uint40="uint40_of_int"externalof_nativeint:nativeint->uint40="uint40_of_nativeint"externalof_float:float->uint40="uint40_of_float"externalof_int8:int8->uint40="uint40_of_int8"externalof_int16:int16->uint40="uint40_of_int16"externalof_int24:int24->uint40="uint40_of_int24"externalof_int32:int32->uint40="uint40_of_int32"externalof_int40:int40->uint40="uint40_of_int40"externalof_int48:int48->uint40="uint40_of_int48"externalof_int56:int56->uint40="uint40_of_int56"externalof_int64:int64->uint40="uint40_of_int64"externalof_int128:int128->uint40="uint40_of_int128"externalof_uint8:uint8->uint40="uint40_of_uint8"externalof_uint16:uint16->uint40="uint40_of_uint16"externalof_uint24:uint24->uint40="uint40_of_uint24"externalof_uint32:uint32->uint40="uint40_of_uint32"externalof_uint40:uint40->uint40="%identity"externalof_uint48:uint48->uint40="uint40_of_uint48"externalof_uint56:uint56->uint40="uint40_of_uint56"externalof_uint64:uint64->uint40="uint40_of_uint64"externalof_uint128:uint128->uint40="uint40_of_uint128"externalto_int:uint40->int="int_of_uint40"externalto_nativeint:uint40->nativeint="nativeint_of_uint40"externalto_float:uint40->float="float_of_uint40"externalto_int8:uint40->int8="int8_of_uint40"externalto_int16:uint40->int16="int16_of_uint40"externalto_int24:uint40->int24="int24_of_uint40"externalto_int32:uint40->int32="int32_of_uint40"externalto_int40:uint40->int40="int40_of_uint40"externalto_int48:uint40->int48="int48_of_uint40"externalto_int56:uint40->int56="int56_of_uint40"externalto_int64:uint40->int64="int64_of_uint40"externalto_int128:uint40->int128="int128_of_uint40"externalto_uint8:uint40->uint8="uint8_of_uint40"externalto_uint16:uint40->uint16="uint16_of_uint40"externalto_uint24:uint40->uint24="uint24_of_uint40"externalto_uint32:uint40->uint32="uint32_of_uint40"externalto_uint40:uint40->uint40="%identity"externalto_uint48:uint40->uint48="uint48_of_uint40"externalto_uint56:uint40->uint56="uint56_of_uint40"externalto_uint64:uint40->uint64="uint64_of_uint40"externalto_uint128:uint40->uint128="uint128_of_uint40"letone=of_int1letmax_int=max_int_fun()letlognot=logxormax_intletcompare=Stdint_stdlib_.compareletdivmod=(funxy->divxy,remxy)endincludeBasemoduleConv=Str_conv.Make(Base)include(Conv:moduletypeofConvwithtypet:=uint40)moduleEndian=Bytes_conv.Make(Base)include(Endian:moduletypeofEndianwithtypet:=uint40)moduleInf=Infix.Make(Base)include(Inf:moduletypeofInfwithtypet:=uint40)endmoduleUint48=struct(* uint48 is modeled as uint64, where only the UPPER 48 bits are used;
this has the advantage that most operations are identical to the uint64 ones.
The post-condition of all uint48 opertaions is, that the LOWER 16 bit are 0x0000.
Only operations that are not identical or do not preserve the post-condition are implemented.
*)moduleBase=structincludeUint64.Baseletbits=48letfmt="Ul"letname="Uint48"externalmul:uint48->uint48->uint48="uint48_mul"externaldiv:uint48->uint48->uint48="uint48_div"externallogxor:uint48->uint48->uint48="uint48_xor"externalshift_right:uint48->int->uint48="uint48_shift_right"letshift_right_logical=shift_rightexternalneg:uint48->uint48="uint48_neg"externalof_int:int->uint48="uint48_of_int"externalof_nativeint:nativeint->uint48="uint48_of_nativeint"externalof_float:float->uint48="uint48_of_float"externalof_int8:int8->uint48="uint48_of_int8"externalof_int16:int16->uint48="uint48_of_int16"externalof_int24:int24->uint48="uint48_of_int24"externalof_int32:int32->uint48="uint48_of_int32"externalof_int40:int40->uint48="uint48_of_int40"externalof_int48:int48->uint48="uint48_of_int48"externalof_int56:int56->uint48="uint48_of_int56"externalof_int64:int64->uint48="uint48_of_int64"externalof_int128:int128->uint48="uint48_of_int128"externalof_uint8:uint8->uint48="uint48_of_uint8"externalof_uint16:uint16->uint48="uint48_of_uint16"externalof_uint24:uint24->uint48="uint48_of_uint24"externalof_uint32:uint32->uint48="uint48_of_uint32"externalof_uint40:uint40->uint48="uint48_of_uint40"externalof_uint48:uint48->uint48="%identity"externalof_uint56:uint56->uint48="uint48_of_uint56"externalof_uint64:uint64->uint48="uint48_of_uint64"externalof_uint128:uint128->uint48="uint48_of_uint128"externalto_int:uint48->int="int_of_uint48"externalto_nativeint:uint48->nativeint="nativeint_of_uint48"externalto_float:uint48->float="float_of_uint48"externalto_int8:uint48->int8="int8_of_uint48"externalto_int16:uint48->int16="int16_of_uint48"externalto_int24:uint48->int24="int24_of_uint48"externalto_int32:uint48->int32="int32_of_uint48"externalto_int40:uint48->int40="int40_of_uint48"externalto_int48:uint48->int48="int48_of_uint48"externalto_int56:uint48->int56="int56_of_uint48"externalto_int64:uint48->int64="int64_of_uint48"externalto_int128:uint48->int128="int128_of_uint48"externalto_uint8:uint48->uint8="uint8_of_uint48"externalto_uint16:uint48->uint16="uint16_of_uint48"externalto_uint24:uint48->uint24="uint24_of_uint48"externalto_uint32:uint48->uint32="uint32_of_uint48"externalto_uint40:uint48->uint40="uint40_of_uint48"externalto_uint48:uint48->uint48="%identity"externalto_uint56:uint48->uint56="uint56_of_uint48"externalto_uint64:uint48->uint64="uint64_of_uint48"externalto_uint128:uint48->uint128="uint128_of_uint48"letone=of_int1letmax_int=max_int_fun()letlognot=logxormax_intletcompare=Stdint_stdlib_.compareletdivmod=(funxy->divxy,remxy)endincludeBasemoduleConv=Str_conv.Make(Base)include(Conv:moduletypeofConvwithtypet:=uint48)moduleEndian=Bytes_conv.Make(Base)include(Endian:moduletypeofEndianwithtypet:=uint48)moduleInf=Infix.Make(Base)include(Inf:moduletypeofInfwithtypet:=uint48)endmoduleUint56=struct(* uint56 is modeled as uint64, where only the UPPER 56 bits are used;
this has the advantage that most operations are identical to the uint64 ones.
The post-condition of all uint56 opertaions is, that the LOWER 8 bit are 0x00.
Only operations that are not identical or do not preserve the post-condition are implemented.
*)moduleBase=structincludeUint64.Baseletbits=56letfmt="Ul"letname="Uint56"externalmul:uint56->uint56->uint56="uint56_mul"externaldiv:uint56->uint56->uint56="uint56_div"externallogxor:uint56->uint56->uint56="uint56_xor"externalshift_right:uint56->int->uint56="uint56_shift_right"letshift_right_logical=shift_rightexternalneg:uint56->uint56="uint56_neg"externalof_int:int->uint56="uint56_of_int"externalof_nativeint:nativeint->uint56="uint56_of_nativeint"externalof_float:float->uint56="uint56_of_float"externalof_int8:int8->uint56="uint56_of_int8"externalof_int16:int16->uint56="uint56_of_int16"externalof_int24:int24->uint56="uint56_of_int24"externalof_int32:int32->uint56="uint56_of_int32"externalof_int40:int40->uint56="uint56_of_int40"externalof_int48:int48->uint56="uint56_of_int48"externalof_int56:int56->uint56="uint56_of_int56"externalof_int64:int64->uint56="uint56_of_int64"externalof_int128:int128->uint56="uint56_of_int128"externalof_uint8:uint8->uint56="uint56_of_uint8"externalof_uint16:uint16->uint56="uint56_of_uint16"externalof_uint24:uint24->uint56="uint56_of_uint24"externalof_uint32:uint32->uint56="uint56_of_uint32"externalof_uint40:uint40->uint56="uint56_of_uint40"externalof_uint48:uint48->uint56="uint56_of_uint48"externalof_uint56:uint56->uint56="%identity"externalof_uint64:uint64->uint56="uint56_of_uint64"externalof_uint128:uint128->uint56="uint56_of_uint128"externalto_int:uint56->int="int_of_uint56"externalto_nativeint:uint56->nativeint="nativeint_of_uint56"externalto_float:uint56->float="float_of_uint56"externalto_int8:uint56->int8="int8_of_uint56"externalto_int16:uint56->int16="int16_of_uint56"externalto_int24:uint56->int24="int24_of_uint56"externalto_int32:uint56->int32="int32_of_uint56"externalto_int40:uint56->int40="int40_of_uint56"externalto_int48:uint56->int48="int48_of_uint56"externalto_int56:uint56->int56="int56_of_uint56"externalto_int64:uint56->int64="int64_of_uint56"externalto_int128:uint56->int128="int128_of_uint56"externalto_uint8:uint56->uint8="uint8_of_uint56"externalto_uint16:uint56->uint16="uint16_of_uint56"externalto_uint24:uint56->uint24="uint24_of_uint56"externalto_uint32:uint56->uint32="uint32_of_uint56"externalto_uint40:uint56->uint40="uint40_of_uint56"externalto_uint48:uint56->uint48="uint48_of_uint56"externalto_uint56:uint56->uint56="%identity"externalto_uint64:uint56->uint64="uint64_of_uint56"externalto_uint128:uint56->uint128="uint128_of_uint56"letone=of_int1letmax_int=max_int_fun()letlognot=logxormax_intletcompare=Stdint_stdlib_.compareletdivmod=(funxy->divxy,remxy)endincludeBasemoduleConv=Str_conv.Make(Base)include(Conv:moduletypeofConvwithtypet:=uint56)moduleEndian=Bytes_conv.Make(Base)include(Endian:moduletypeofEndianwithtypet:=uint56)moduleInf=Infix.Make(Base)include(Inf:moduletypeofInfwithtypet:=uint56)endmoduleUint128=structmoduleBase=structtypet=uint128letbits=128letfmt="ULL"letname="Int1128"externaladd:uint128->uint128->uint128="uint128_add"externalsub:uint128->uint128->uint128="uint128_sub"externalmul:uint128->uint128->uint128="uint128_mul"externaldiv:uint128->uint128->uint128="uint128_div"externalrem:uint128->uint128->uint128="uint128_mod"externallogand:uint128->uint128->uint128="uint128_and"externallogor:uint128->uint128->uint128="uint128_or"externallogxor:uint128->uint128->uint128="uint128_xor"externalshift_left:uint128->int->uint128="uint128_shift_left"externalshift_right:uint128->int->uint128="uint128_shift_right"letshift_right_logical=shift_rightexternalabs:uint128->uint128="%identity"externalof_int:int->uint128="uint128_of_int"externalof_nativeint:nativeint->uint128="uint128_of_nativeint"externalof_float:float->uint128="uint128_of_float"externalof_int8:int8->uint128="uint128_of_int8"externalof_int16:int16->uint128="uint128_of_int16"externalof_int24:int24->uint128="uint128_of_int24"externalof_int32:int32->uint128="uint128_of_int32"externalof_int40:int40->uint128="uint128_of_int40"externalof_int48:int48->uint128="uint128_of_int48"externalof_int56:int56->uint128="uint128_of_int56"externalof_int64:int64->uint128="uint128_of_int64"externalof_int128:int128->uint128="uint128_of_int128"externalof_uint8:uint8->uint128="uint128_of_uint8"externalof_uint16:uint16->uint128="uint128_of_uint16"externalof_uint24:uint24->uint128="uint128_of_uint24"externalof_uint32:uint32->uint128="uint128_of_uint32"externalof_uint40:uint40->uint128="uint128_of_uint40"externalof_uint48:uint48->uint128="uint128_of_uint48"externalof_uint56:uint56->uint128="uint128_of_uint56"externalof_uint64:uint64->uint128="uint128_of_uint64"externalof_uint128:uint128->uint128="%identity"externalto_int:uint128->int="int_of_uint128"externalto_nativeint:uint128->nativeint="nativeint_of_uint128"externalto_float:uint128->float="float_of_uint128"externalto_int8:uint128->int8="int8_of_uint128"externalto_int16:uint128->int16="int16_of_uint128"externalto_int24:uint128->int24="int24_of_uint128"externalto_int32:uint128->int32="int32_of_uint128"externalto_int40:uint128->int40="int40_of_uint128"externalto_int48:uint128->int48="int48_of_uint128"externalto_int56:uint128->int56="int56_of_uint128"externalto_int64:uint128->int64="int64_of_uint128"externalto_int128:uint128->int128="int128_of_uint128"externalto_uint8:uint128->uint8="uint8_of_uint128"externalto_uint16:uint128->uint16="uint16_of_uint128"externalto_uint24:uint128->uint24="uint24_of_uint128"externalto_uint32:uint128->uint32="uint32_of_uint128"externalto_uint40:uint128->uint40="uint40_of_uint128"externalto_uint48:uint128->uint48="uint48_of_uint128"externalto_uint56:uint128->uint56="uint56_of_uint128"externalto_uint64:uint128->uint64="uint64_of_uint128"externalto_uint128:uint128->uint128="%identity"externalmax_int_fun:unit->uint128="uint128_max_int"letzero=of_int0letone=of_int1letsucc=addoneletpredx=subxoneletmax_int=max_int_fun()letmin_int=zeroletlognot=logxormax_intletcompare=Stdint_stdlib_.compareletdivmod=(funxy->divxy,remxy)letnegx=add(submax_intx)oneexternalinit_custom_ops:unit->unit="uint128_init_custom_ops"let()=init_custom_ops()endincludeBasemoduleConv=Str_conv.Make(Base)include(Conv:moduletypeofConvwithtypet:=uint128)moduleEndian=Bytes_conv.Make(Base)include(Endian:moduletypeofEndianwithtypet:=uint128)moduleInf=Infix.Make(Base)include(Inf:moduletypeofInfwithtypet:=uint128)end