package why3

  1. Overview
  2. Docs
package why3
Legend:
Library
Module
Module type
Parameter
Class
Class type
exception InvalidConstantLiteral of int * string
type int_value = BigInt.t
type int_literal_kind =
  1. | ILitUnk
  2. | ILitDec
  3. | ILitHex
  4. | ILitOct
  5. | ILitBin
type int_constant = {
  1. il_kind : int_literal_kind;
  2. il_int : int_value;
}
type real_value = private {
  1. rv_sig : BigInt.t;
  2. rv_pow2 : BigInt.t;
  3. rv_pow5 : BigInt.t;
}
type real_literal_kind =
  1. | RLitUnk
  2. | RLitDec of int
  3. | RLitHex of int
type real_constant = {
  1. rl_kind : real_literal_kind;
  2. rl_real : real_value;
}
val neg_int : int_constant -> int_constant
val abs_int : int_constant -> int_constant
val neg_real : real_constant -> real_constant
val abs_real : real_constant -> real_constant
val compare_real : real_value -> real_value -> int
val int_literal : int_literal_kind -> neg:bool -> string -> int_constant
val real_literal : radix:int -> neg:bool -> int:string -> frac:string -> exp:string option -> real_constant
val real_value : ?pow2:BigInt.t -> ?pow5:BigInt.t -> BigInt.t -> real_value
type default_format = Format.formatter -> string -> unit
type integer_format = Format.formatter -> BigInt.t -> unit
type real_format = Format.formatter -> string -> string -> string option -> unit
type two_strings_format = Format.formatter -> string -> string -> unit
type frac_real_format = (Format.formatter -> string -> unit) * two_strings_format * two_strings_format
type delayed_format = Format.formatter -> (Format.formatter -> unit) -> unit
type number_support = {
  1. long_int_support : [ `Custom of default_format | `Default ];
  2. negative_int_support : [ `Custom of delayed_format | `Default ];
  3. dec_int_support : [ `Custom of integer_format | `Default | `Unsupported of default_format ];
  4. hex_int_support : [ `Custom of integer_format | `Default | `Unsupported ];
  5. oct_int_support : [ `Custom of integer_format | `Default | `Unsupported ];
  6. bin_int_support : [ `Custom of integer_format | `Default | `Unsupported ];
  7. negative_real_support : [ `Custom of delayed_format | `Default ];
  8. dec_real_support : [ `Custom of real_format | `Default | `Unsupported ];
  9. hex_real_support : [ `Custom of real_format | `Default | `Unsupported ];
  10. frac_real_support : [ `Custom of frac_real_format | `Unsupported of default_format ];
}
val full_support : number_support
val print_int_constant : number_support -> Format.formatter -> int_constant -> unit
val print_real_constant : number_support -> Format.formatter -> real_constant -> unit
val print_in_base : int -> int option -> Format.formatter -> BigInt.t -> unit
val to_small_integer : int_constant -> int
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 int_constant
val check_range : int_constant -> int_range -> unit
type float_format = {
  1. fp_exponent_digits : int;
  2. fp_significand_digits : int;
}
exception NonRepresentableFloat of real_constant
val compute_float : real_constant -> float_format -> BigInt.t * BigInt.t
val check_float : real_constant -> 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