package why3

  1. Overview
  2. Docs
package why3
Legend:
Library
Module
Module type
Parameter
Class
Class type
exception InvalidConstantLiteral of int * string
type integer_literal = private
  1. | IConstRaw of BigInt.t
  2. | IConstDec of string
  3. | IConstHex of string
  4. | IConstOct of string
  5. | IConstBin of string
type integer_constant = {
  1. ic_negative : bool;
  2. ic_abs : integer_literal;
}
type real_literal = private
  1. | RConstDec of string * string * string option
  2. | RConstHex of string * string * string option
type real_constant = {
  1. rc_negative : bool;
  2. rc_abs : real_literal;
}
type constant =
  1. | ConstInt of integer_constant
  2. | ConstReal of real_constant
val is_negative : constant -> bool
val int_literal_dec : string -> integer_literal
val int_literal_hex : string -> integer_literal
val int_literal_oct : string -> integer_literal
val int_literal_bin : string -> integer_literal
val int_literal_raw : BigInt.t -> integer_literal
val int_const_of_int : int -> integer_constant
val int_const_of_big_int : BigInt.t -> integer_constant
val const_of_int : int -> constant
val const_of_big_int : BigInt.t -> constant
val real_const_dec : string -> string -> string option -> real_literal
val real_const_hex : string -> string -> string option -> real_literal
val print_constant : Format.formatter -> constant -> unit
type integer_format = (string -> unit, Format.formatter, unit) format
type real_format = (string -> string -> string -> unit, Format.formatter, unit) format
type part_real_format = (string -> string -> unit, Format.formatter, unit) format
type dec_real_format =
  1. | PrintDecReal of part_real_format * real_format
type frac_real_format =
  1. | PrintFracReal of integer_format * part_real_format * part_real_format
type !'a number_support_kind =
  1. | Number_unsupported
  2. | Number_default
  3. | Number_custom of 'a
type integer_support_kind = integer_format number_support_kind
type !'a negative_format = ((Format.formatter -> 'a -> unit) -> 'a -> unit, Format.formatter, unit) format
type number_support = {
  1. long_int_support : bool;
  2. extra_leading_zeros_support : bool;
  3. negative_int_support : integer_literal negative_format number_support_kind;
  4. dec_int_support : integer_support_kind;
  5. hex_int_support : integer_support_kind;
  6. oct_int_support : integer_support_kind;
  7. bin_int_support : integer_support_kind;
  8. def_int_support : integer_support_kind;
  9. negative_real_support : real_literal negative_format number_support_kind;
  10. dec_real_support : dec_real_format number_support_kind;
  11. hex_real_support : real_format number_support_kind;
  12. frac_real_support : frac_real_format number_support_kind;
  13. def_real_support : integer_support_kind;
}
val print : number_support -> Format.formatter -> constant -> unit
val print_in_base : int -> int option -> Format.formatter -> BigInt.t -> unit
val to_small_integer : integer_literal -> int
val compute_int_literal : integer_literal -> BigInt.t
val compute_int_constant : integer_constant -> BigInt.t
type int_range = {
  1. ir_lower : BigInt.t;
  2. ir_upper : BigInt.t;
}
val create_range : BigInt.t -> BigInt.t -> int_range
exception OutOfRange of integer_constant
val check_range : integer_constant -> int_range -> unit
type float_format = {
  1. fp_exponent_digits : int;
  2. fp_significand_digits : int;
}
exception NonRepresentableFloat of real_literal
val compute_float : real_literal -> float_format -> BigInt.t * BigInt.t
val check_float : real_literal -> float_format -> unit
OCaml

Innovation. Community. Security.

GitHub Discord Twitter Peertube RSS
About
Changelog Releases Industrial Users Academic Users Why OCaml
Ecosystem
Packages Community Events OCaml Planet Jobs
Resources
Install OCaml Get Started Platform Tools Language Manual Standard Library API Books Exercises Papers OCaml Playground Logo
Policies
Carbon Footprint Governance Privacy Code of Conduct