"/>

Module Once.Sort

type 'a t = 'a sort

A sort of 'a kind.

val bool : bv t

A Boolean sort is a bit-vector sort of size 1.

val bv : int -> bv t

bv size create a bit-vector sort of given size.

parameter size

The size of the bit-vector sort.

returns

A bit-vector sort of given size.

val size : bv t -> int

size sort get the size of a bit-vector sort.

parameter sort

The sort.

returns

The size of the bit-vector sort.

val fp : exponent:int -> int -> fp t

fp exp_size size create a floating-point sort of given size with exp_size exponent bits.

parameter exp_size

The size of the exponent.

parameter size

The total size of the floating-point.

returns

A floating-point sort of given format.

val exponent : fp t -> int

exponent sort get the exponent size of a floating-point sort.

parameter sort

The sort.

returns

The exponent size of the floating-point sort.

val significand : fp t -> int

significand sort get the significand size of a floating-point sort.

parameter sort

The sort.

returns

The significand size of the floating-point sort.

val rm : rm t

A Roundingmode sort.

val ar : 'a t -> 'b t -> ('a, 'b) ar t

ar index element create an array sort.

parameter index

The index sort of the array sort.

parameter element

The element sort of the array sort.

returns

An array sort which maps sort index to sort element.

val index : ('a, 'b) ar t -> 'a t

index sort get the index sort of an array sort.

parameter sort

The sort.

returns

The index sort of the array sort.

val element : ('a, 'b) ar t -> 'b t

element sort get the element sort of an array sort.

parameter sort

The sort.

returns

The element sort of the array sort.

type 'a variadic =
| ([]) : unit variadic
| (::) : [< bv | rm | fp ] as 'a sort * 'b variadic -> ('a -> 'b) variadic

Functions accept only bit-vector, rounding-mode or floating-point as argument

Statically typed list of function argument sorts.

val fn : 'a variadic -> 'b t -> ('a, 'b) fn t

fn domain codomain create a function sort.

parameter domain

The domain sorts (the sorts of the arguments).

parameter codomain

The codomain sort (the sort of the return value).

returns

A function sort of given domain and codomain sorts.

val arity : ('a, 'b) fn t -> int

arity sort get the arity of a function sort.

parameter sort

The sort.

returns

The number of arguments of the function sort.

val domain : ('a, 'b) fn t -> 'a variadic

domain sort get the domain sorts of a function sort.

parameter sort

The sort.

returns

The domain sorts of the function sort as an array of sort.

val codomain : ('a, 'b) fn t -> 'b t

codomain sort get the codomain sort of a function sort.

parameter sort

The sort.

returns

The codomain sort of the function sort.

val hash : 'a t -> int

hash sort compute the hash value for a sort.

parameter sort

The sort.

returns

The hash value of the sort.

val equal : 'a t -> 'a t -> bool

equal sort0 sort1 determine if two sorts are equal.

parameter sort0

The first sort.

parameter sort1

The second sort.

returns

true if the given sorts are equal.

val pp : Stdlib.Format.formatter -> 'a t -> unit

pp formatter sort pretty print sort.

parameter formatter

The outpout formatter

parameter sort

The sort.