README
T
Carry
T
Comparison
T
FloatClass
T
FloatComparison
- ::copyPArray::copy
- ::defaultPArray::default
- ::getPArray::get
- ::lengthPArray::length
- ::makePArray::make
- ::of_arrayPArray::of_array
- ::setPArray::set
- ::to_arrayPArray::to_array
V
f64_abs
V
f64_add
V
f64_classify
V
f64_compare
V
f64_div
V
f64_eqb
V
f64_equal
V
f64_frshiftexp
V
f64_ldexp
V
f64_ldshiftexp
V
f64_leb
V
f64_ltb
V
f64_mul
V
f64_next_down
V
f64_next_up
V
f64_normfr_mantissa
V
f64_of_uint63
V
f64_opp
V
f64_sqrt
V
f64_sub
V
max_length
V
u63_add
V
u63_addc
V
u63_addcarryc
V
u63_addmuldiv
V
u63_asr
V
u63_compare
V
u63_compares
V
u63_div
V
u63_diveucl
V
u63_diveucl_21
V
u63_divs
V
u63_eqb
V
u63_head0
V
u63_land
V
u63_leb
V
u63_lesb
V
u63_lor
V
u63_lsl
V
u63_lsr
V
u63_ltb
V
u63_ltsb
V
u63_lxor
V
u63_mod
V
u63_mods
V
u63_mul
V
u63_mulc
V
u63_of_int
V
u63_of_int64
V
u63_sub
V
u63_subc
V
u63_subcarryc
V
u63_tail0
V
u63_to_int
V
u63_to_int64

rocqrt

Runtime support for MoonBit code extracted from Rocq by rocq2mbt

rocq

coq

extraction

runtime

Download zip

Author

GreckF

Version

0.1.0

License

MIT

Repository

github.com/GreckF/rocq2mbt

Last updated

12 hours ago

Downloads

No dependencies

#GreckF/rocqrt

Runtime support for MoonBit code extracted from Rocq by rocq2mbt: Rocq's native 63-bit integers (Uint63), floats (Float64) and persistent arrays (PArray, as diff-arrays).

Extracted code that uses Rocq's native types depends on this module:

// moon.mod
import { "GreckF/rocqrt@0.1.0" }

// moon.pkg of the extracted package
import { "GreckF/rocqrt" @rocqrt }

See the rocq2mbt repository for the extraction plugin and its documentation.

Carry

source

pub(all) enum Carry[A] {
  C0(A)
  C1(A)
} derive(Eq, @moonbitlang/core/debug.Debug
Debug)

Constructor results of the carry type.

Comparison

source

pub(all) enum Comparison {
  Eq
  Lt
  Gt
} derive(Eq, @moonbitlang/core/debug.Debug
Debug)

Rocq's comparison type.

FloatClass

source

pub(all) enum FloatClass {
  PNormal
  NNormal
  PSubn
  NSubn
  PZero
  NZero
  PInf
  NInf
  NaN
} derive(Eq, @moonbitlang/core/debug.Debug
Debug)

FloatComparison

source

pub(all) enum FloatComparison {
  FEq
  FLt
  FGt
  FNotComparable
} derive(Eq, @moonbitlang/core/debug.Debug
Debug)

PArray

source

pub struct PArray[A] {
  // private fields
}

PArray::copy

source

fn[A] PArray::copy(p : PArray[A]) -> PArray[A]

PArray::default

source

fn[A] PArray::default(p : PArray[A]) -> A

PArray::get

source

fn[A] PArray::get(p : PArray[A], n : UInt64) -> A

PArray::length

source

fn[A] PArray::length(p : PArray[A]) -> UInt64

PArray::make

source

fn[A] PArray::make(n : UInt64, def : A) -> PArray[A]

PArray::of_array

source

fn[A] PArray::of_array(a : Array[A], def : A) -> PArray[A]

Literal arrays produced by extraction.

PArray::set

source

fn[A] PArray::set(p : PArray[A], n : UInt64, e : A) -> PArray[A]

PArray::to_array

source

fn[A] PArray::to_array(p : PArray[A]) -> Array[A]

Snapshot of the contents, for interoperability.

f64_abs

source

fn f64_abs(x : Double) -> Double

f64_add

source

fn f64_add(x : Double, y : Double) -> Double

f64_classify

source

fn f64_classify(x : Double) -> FloatClass

f64_compare

source

fn f64_compare(x : Double, y : Double) -> FloatComparison

f64_div

source

fn f64_div(x : Double, y : Double) -> Double

f64_eqb

source

fn f64_eqb(x : Double, y : Double) -> Bool

f64_equal

source

fn f64_equal(x : Double, y : Double) -> Bool

Leibniz equality: NaNs are equal, +0 and -0 are not.

f64_frshiftexp

source

fn f64_frshiftexp(x : Double) -> (Double, UInt64)

f64_ldexp

source

fn f64_ldexp(x : Double, n : Int) -> Double

x * 2^n, correctly rounded (port of musl's scalbn).

f64_ldshiftexp

source

fn f64_ldshiftexp(x : Double, e : UInt64) -> Double

f64_leb

source

fn f64_leb(x : Double, y : Double) -> Bool

f64_ltb

source

fn f64_ltb(x : Double, y : Double) -> Bool

f64_mul

source

fn f64_mul(x : Double, y : Double) -> Double

f64_next_down

source

fn f64_next_down(x : Double) -> Double

f64_next_up

source

fn f64_next_up(x : Double) -> Double

f64_normfr_mantissa

source

fn f64_normfr_mantissa(x : Double) -> UInt64

f64_of_uint63

source

fn f64_of_uint63(x : UInt64) -> Double

f64_opp

source

fn f64_opp(x : Double) -> Double

f64_sqrt

source

fn f64_sqrt(x : Double) -> Double

f64_sub

source

fn f64_sub(x : Double, y : Double) -> Double

max_length

source

let max_length : UInt64

u63_add

source

fn u63_add(x : UInt64, y : UInt64) -> UInt64

u63_addc

source

fn u63_addc(x : UInt64, y : UInt64) -> Carry[UInt64]

u63_addcarryc

source

fn u63_addcarryc(x : UInt64, y : UInt64) -> Carry[UInt64]

u63_addmuldiv

source

fn u63_addmuldiv(p : UInt64, x : UInt64, y : UInt64) -> UInt64

u63_asr

source

fn u63_asr(x : UInt64, y : UInt64) -> UInt64

u63_compare

source

fn u63_compare(x : UInt64, y : UInt64) -> Comparison

Unsigned comparison.

u63_compares

source

fn u63_compares(x : UInt64, y : UInt64) -> Comparison

Signed comparison.

u63_div

source

fn u63_div(x : UInt64, y : UInt64) -> UInt64

u63_diveucl

source

fn u63_diveucl(x : UInt64, y : UInt64) -> (UInt64, UInt64)

u63_diveucl_21

source

fn u63_diveucl_21(xh : UInt64, xl : UInt64, y : UInt64) -> (UInt64, UInt64)

Division of the 126-bit number xh * 2^63 + xl by y.

u63_divs

source

fn u63_divs(x : UInt64, y : UInt64) -> UInt64

u63_eqb

source

fn u63_eqb(x : UInt64, y : UInt64) -> Bool

u63_head0

source

fn u63_head0(x : UInt64) -> UInt64

u63_land

source

fn u63_land(x : UInt64, y : UInt64) -> UInt64

u63_leb

source

fn u63_leb(x : UInt64, y : UInt64) -> Bool

u63_lesb

source

fn u63_lesb(x : UInt64, y : UInt64) -> Bool

u63_lor

source

fn u63_lor(x : UInt64, y : UInt64) -> UInt64

u63_lsl

source

fn u63_lsl(x : UInt64, y : UInt64) -> UInt64

u63_lsr

source

fn u63_lsr(x : UInt64, y : UInt64) -> UInt64

u63_ltb

source

fn u63_ltb(x : UInt64, y : UInt64) -> Bool

u63_ltsb

source

fn u63_ltsb(x : UInt64, y : UInt64) -> Bool

u63_lxor

source

fn u63_lxor(x : UInt64, y : UInt64) -> UInt64

u63_mod

source

fn u63_mod(x : UInt64, y : UInt64) -> UInt64

u63_mods

source

fn u63_mods(x : UInt64, y : UInt64) -> UInt64

u63_mul

source

fn u63_mul(x : UInt64, y : UInt64) -> UInt64

u63_mulc

source

fn u63_mulc(x : UInt64, y : UInt64) -> (UInt64, UInt64)

Exact product as (high, low) 63-bit words: x * y = high * 2^63 + low.

u63_of_int

source

fn u63_of_int(x : Int) -> UInt64

Conversions for interoperability with MoonBit integers.

u63_of_int64

source

fn u63_of_int64(x : Int64) -> UInt64

u63_sub

source

fn u63_sub(x : UInt64, y : UInt64) -> UInt64

u63_subc

source

fn u63_subc(x : UInt64, y : UInt64) -> Carry[UInt64]

u63_subcarryc

source

fn u63_subcarryc(x : UInt64, y : UInt64) -> Carry[UInt64]

u63_tail0

source

fn u63_tail0(x : UInt64) -> UInt64

u63_to_int

source

fn u63_to_int(x : UInt64) -> Int

u63_to_int64

source

fn u63_to_int64(x : UInt64) -> Int64

Source Files

Install

Download zip

Runtime support for MoonBit code extracted from Rocq by rocq2mbt

rocqcoqextractionruntime

GreckF

MIT

github.com/GreckF/rocq2mbt

Updated 12 hours ago

10 downloads

Site source Report issue Modules Skills CLI Build queue Statistics

rocqrt

#GreckF/rocqrt

#Carry

#Comparison

#FloatClass

#FloatComparison

#PArray

#PArray::copy

#PArray::default

#PArray::get

#PArray::length

#PArray::make

#PArray::of_array

#PArray::set

#PArray::to_array

#f64_abs

#f64_add

#f64_classify

#f64_compare

#f64_div

#f64_eqb

#f64_equal

#f64_frshiftexp

#f64_ldexp

#f64_ldshiftexp

#f64_leb

#f64_ltb

#f64_mul

#f64_next_down

#f64_next_up

#f64_normfr_mantissa

#f64_of_uint63

#f64_opp

#f64_sqrt

#f64_sub

#max_length

#u63_add

#u63_addc

#u63_addcarryc

#u63_addmuldiv

#u63_asr

#u63_compare

#u63_compares

#u63_div

#u63_diveucl

#u63_diveucl_21

#u63_divs

#u63_eqb

#u63_head0

#u63_land

#u63_leb

#u63_lesb

#u63_lor

#u63_lsl

#u63_lsr

#u63_ltb

#u63_ltsb

#u63_lxor

#u63_mod

#u63_mods

#u63_mul

#u63_mulc

#u63_of_int

#u63_of_int64

#u63_sub

#u63_subc

#u63_subcarryc

#u63_tail0

#u63_to_int

#u63_to_int64

Source Files

Carry

Comparison

FloatClass

FloatComparison

PArray

PArray::copy

PArray::default

PArray::get

PArray::length

PArray::make

PArray::of_array

PArray::set

PArray::to_array

f64_abs

f64_add

f64_classify

f64_compare

f64_div

f64_eqb

f64_equal

f64_frshiftexp

f64_ldexp

f64_ldshiftexp

f64_leb

f64_ltb

f64_mul

f64_next_down

f64_next_up

f64_normfr_mantissa

f64_of_uint63

f64_opp

f64_sqrt

f64_sub

max_length

u63_add

u63_addc

u63_addcarryc

u63_addmuldiv

u63_asr

u63_compare

u63_compares

u63_div

u63_diveucl

u63_diveucl_21

u63_divs

u63_eqb

u63_head0

u63_land

u63_leb

u63_lesb

u63_lor

u63_lsl

u63_lsr

u63_ltb

u63_ltsb

u63_lxor

u63_mod

u63_mods

u63_mul

u63_mulc

u63_of_int

u63_of_int64

u63_sub

u63_subc

u63_subcarryc

u63_tail0

u63_to_int

u63_to_int64