Quelle numCompat.ml Sprache: SML

(************************************************************************)
(*         *      The Rocq Prover / The Rocq Development Team           *)
(*  v      *         Copyright INRIA, CNRS and contributors             *)
(* <O___,, * (see version control and CREDITS file for authors & dates) *)
(*   \VV/  **************************************************************)
(*    //   *    This file is distributed under the terms of the         *)
(*         *     GNU Lesser General Public License Version 2.1          *)
(*         *     (see LICENSE file for the text of the license)         *)
(************************************************************************)

module type ZArith = sig
  type t

  val zero : t
  val one : t
  val two : t
  val add : t -> t -> t
  val sub : t -> t -> t
  val mul : t -> t -> t
  val div : t -> t -> t
  val neg : t -> t
  val sign : t -> int
  val equal : t -> t -> bool
  val compare : t -> t -> int
  val power_int : t -> int -> t
  val quomod : t -> t -> t * t
  val ppcm : t -> t -> t
  val gcd : t -> t -> t
  val lcm : t -> t -> t
  val to_string : t -> string
end

module Z = struct
  (* Beware this only works fine in ZArith >= 1.10 due to
     https://github.com/ocaml/Zarith/issues/58 *)
  include Z

  (* Constants *)
  let two = Z.of_int 2
  let ten = Z.of_int 10
  let power_int = Big_int_Z.power_big_int_positive_int
  let quomod = Big_int_Z.quomod_big_int

  (* zarith fails with division by zero if x == 0 && y == 0 *)
  let lcm x y = if Z.equal x zero && Z.equal y zero then zero else Z.lcm x y

  let ppcm x y =
    let g = gcd x y in
    let x' = Z.div x g in
    let y' = Z.div y g in
    Z.mul g (Z.mul x' y')
end

module type QArith = sig
  module Z : ZArith

  type t

  val of_int : int -> t
  val zero : t
  val one : t
  val two : t
  val ten : t
  val minus_one : t

  module Notations : sig
    val ( // ) : t -> t -> t
    val ( +/ ) : t -> t -> t
    val ( -/ ) : t -> t -> t
    val ( */ ) : t -> t -> t
    val ( =/ ) : t -> t -> bool
    val ( <>/ ) : t -> t -> bool
    val ( >/ ) : t -> t -> bool
    val ( >=/ ) : t -> t -> bool
    val ( </ ) : t -> t -> bool
    val ( <=/ ) : t -> t -> bool
  end

  val compare : t -> t -> int
  val make : Z.t -> Z.t -> t
  val den : t -> Z.t
  val num : t -> Z.t
  val of_bigint : Z.t -> t
  val to_bigint : t -> Z.t
  val neg : t -> t

  (* val inv : t -> t *)
  val max : t -> t -> t
  val min : t -> t -> t
  val sign : t -> int
  val abs : t -> t
  val mod_ : t -> t -> t
  val floor : t -> t

  (* val floorZ : t -> Z.t *)
  val ceiling : t -> t
  val round : t -> t
  val pow2 : int -> t
  val pow10 : int -> t
  val power : int -> t -> t
  val to_string : t -> string
  val of_string : string -> t
  val to_float : t -> float
end

module Q : QArith with module Z = Z = struct
  module Z = Z

  let pow_check_exp x y =
    let z_res =
      if y = 0 then Z.one
      else if y > 0 then Z.pow x y
      else (* s < 0 *)
        Z.pow x (abs y)
    in
    let z_res = Q.of_bigint z_res in
    if 0 <= y then z_res else Q.inv z_res

  include Q

  let two = Q.(of_int 2)
  let ten = Q.(of_int 10)

  module Notations = struct
    let ( // ) = Q.div
    let ( +/ ) = Q.add
    let ( -/ ) = Q.sub
    let ( */ ) = Q.mul
    let ( =/ ) = Q.equal
    let ( <>/ ) x y = not (Q.equal x y)
    let ( >/ ) = Q.gt
    let ( >=/ ) = Q.geq
    let ( </ ) = Q.lt
    let ( <=/ ) = Q.leq
  end

  (* XXX: review / improve *)
  let floorZ q : Z.t = Z.fdiv (num q) (den q)
  let floor q : t = floorZ q |> Q.of_bigint
  let ceiling q : t = Z.cdiv (Q.num q) (Q.den q) |> Q.of_bigint
  let half = Q.make Z.one Z.two

  (* We imitate Num's round which is to the nearest *)
  let round q = floor (Q.add half q)

  (* XXX: review / improve *)
  let quo x y =
    let s = sign y in
    let res = floor (x / abs y) in
    if Int.equal s (-1) then neg res else res

  let mod_ x y = x - (y * quo x y)

  (* XXX: review / improve *)
  (* Note that Z.pow doesn't support negative exponents *)

  let pow2 y = pow_check_exp Z.two y
  let pow10 y = pow_check_exp Z.ten y

  let power (x : int) (y : t) : t =
    let y =
      try Q.to_int y
      with Z.Overflow ->
        (* XXX: make doesn't link Pp / CErrors for csdpcert, that could be fixed *)
        raise (Invalid_argument "[micromega] overflow in exponentiation")
      (* CErrors.user_err (Pp.str "[micromega] overflow in exponentiation") *)
    in
    pow_check_exp (Z.of_int x) y
end

quality100%

¤ Dauer der Verarbeitung: 0.13 Sekunden (vorverarbeitet) ¤

Wurzel

Suchen

Beweissystem der NASA

Beweissystem Isabelle

NIST Cobol Testsuite

Cephes Mathematical Library

Wiener Entwicklungsmethode

Haftungshinweis

Die Informationen auf dieser Webseite wurden nach bestem Wissen sorgfältig zusammengestellt. Es wird jedoch weder Vollständigkeit, noch Richtigkeit, noch Qualität der bereit gestellten Informationen zugesichert.

Bemerkung:

Die farbliche Syntaxdarstellung ist noch experimentell.