(************************************************************************) (* * 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 valsub : 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
(* 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 elseif 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
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.
