{-# OPTIONS --cubical-compatible --safe --no-sized-types --no-guardedness --level-universe #-}
module Agda.Builtin.Float where
open import Agda.Builtin.Bool
open import Agda.Builtin.Int
open import Agda.Builtin.Maybe
open import Agda.Builtin.Nat
open import Agda.Builtin.Sigma
open import Agda.Builtin.String
open import Agda.Builtin.Word
postulate Float : Set
{-# BUILTIN FLOAT Float #-}
primitive
primFloatInequality : Float → Float → Bool
primFloatEquality : Float → Float → Bool
primFloatLess : Float → Float → Bool
primFloatIsInfinite : Float → Bool
primFloatIsNaN : Float → Bool
primFloatIsNegativeZero : Float → Bool
primFloatIsSafeInteger : Float → Bool
primFloatToWord64 : Float → Maybe Word64
primNatToFloat : Nat → Float
primIntToFloat : Int → Float
primFloatRound : Float → Maybe Int
primFloatFloor : Float → Maybe Int
primFloatCeiling : Float → Maybe Int
primFloatToRatio : Float → (Σ Int λ _ → Int)
primRatioToFloat : Int → Int → Float
primFloatDecode : Float → Maybe (Σ Int λ _ → Int)
primFloatEncode : Int → Int → Maybe Float
primShowFloat : Float → String
primFloatPlus : Float → Float → Float
primFloatMinus : Float → Float → Float
primFloatTimes : Float → Float → Float
primFloatDiv : Float → Float → Float
primFloatPow : Float → Float → Float
primFloatNegate : Float → Float
primFloatSqrt : Float → Float
primFloatExp : Float → Float
primFloatLog : Float → Float
primFloatSin : Float → Float
primFloatCos : Float → Float
primFloatTan : Float → Float
primFloatASin : Float → Float
primFloatACos : Float → Float
primFloatATan : Float → Float
primFloatATan2 : Float → Float → Float
primFloatSinh : Float → Float
primFloatCosh : Float → Float
primFloatTanh : Float → Float
primFloatASinh : Float → Float
primFloatACosh : Float → Float
primFloatATanh : Float → Float
{-# COMPILE JS
primFloatRound = function(x) {
x = agdaRTS._primFloatRound(x);
if (x === null) {
return z_jAgda_Agda_Builtin_Maybe["Maybe"]["nothing"];
}
else {
return z_jAgda_Agda_Builtin_Maybe["Maybe"]["just"](x);
}
};
#-}
{-# COMPILE JS
primFloatFloor = function(x) {
x = agdaRTS._primFloatFloor(x);
if (x === null) {
return z_jAgda_Agda_Builtin_Maybe["Maybe"]["nothing"];
}
else {
return z_jAgda_Agda_Builtin_Maybe["Maybe"]["just"](x);
}
};
#-}
{-# COMPILE JS
primFloatCeiling = function(x) {
x = agdaRTS._primFloatCeiling(x);
if (x === null) {
return z_jAgda_Agda_Builtin_Maybe["Maybe"]["nothing"];
}
else {
return z_jAgda_Agda_Builtin_Maybe["Maybe"]["just"](x);
}
};
#-}
{-# COMPILE JS
primFloatToRatio = function(x) {
x = agdaRTS._primFloatToRatio(x);
return z_jAgda_Agda_Builtin_Sigma["_,_"](x.numerator)(x.denominator);
};
#-}
{-# COMPILE JS
primFloatDecode = function(x) {
x = agdaRTS._primFloatDecode(x);
if (x === null) {
return z_jAgda_Agda_Builtin_Maybe["Maybe"]["nothing"];
}
else {
return z_jAgda_Agda_Builtin_Maybe["Maybe"]["just"](
z_jAgda_Agda_Builtin_Sigma["_,_"](x.mantissa)(x.exponent));
}
};
#-}
{-# COMPILE JS
primFloatEncode = function(x) {
return function (y) {
x = agdaRTS.uprimFloatEncode(x, y);
if (x === null) {
return z_jAgda_Agda_Builtin_Maybe["Maybe"]["nothing"];
}
else {
return z_jAgda_Agda_Builtin_Maybe["Maybe"]["just"](x);
}
}
};
#-}
primFloatNumericalEquality = primFloatEquality
{-# WARNING_ON_USAGE primFloatNumericalEquality
"Warning: primFloatNumericalEquality was deprecated in Agda v2.6.2.
Please use primFloatEquality instead."
#-}
primFloatNumericalLess = primFloatLess
{-# WARNING_ON_USAGE primFloatNumericalLess
"Warning: primFloatNumericalLess was deprecated in Agda v2.6.2.
Please use primFloatLess instead."
#-}
primRound = primFloatRound
{-# WARNING_ON_USAGE primRound
"Warning: primRound was deprecated in Agda v2.6.2.
Please use primFloatRound instead."
#-}
primFloor = primFloatFloor
{-# WARNING_ON_USAGE primFloor
"Warning: primFloor was deprecated in Agda v2.6.2.
Please use primFloatFloor instead."
#-}
primCeiling = primFloatCeiling
{-# WARNING_ON_USAGE primCeiling
"Warning: primCeiling was deprecated in Agda v2.6.2.
Please use primFloatCeiling instead."
#-}
primExp = primFloatExp
{-# WARNING_ON_USAGE primExp
"Warning: primExp was deprecated in Agda v2.6.2.
Please use primFloatExp instead."
#-}
primLog = primFloatLog
{-# WARNING_ON_USAGE primLog
"Warning: primLog was deprecated in Agda v2.6.2.
Please use primFloatLog instead."
#-}
primSin = primFloatSin
{-# WARNING_ON_USAGE primSin
"Warning: primSin was deprecated in Agda v2.6.2.
Please use primFloatSin instead."
#-}
primCos = primFloatCos
{-# WARNING_ON_USAGE primCos
"Warning: primCos was deprecated in Agda v2.6.2.
Please use primFloatCos instead."
#-}
primTan = primFloatTan
{-# WARNING_ON_USAGE primTan
"Warning: primTan was deprecated in Agda v2.6.2.
Please use primFloatTan instead."
#-}
primASin = primFloatASin
{-# WARNING_ON_USAGE primASin
"Warning: primASin was deprecated in Agda v2.6.2.
Please use primFloatASin instead."
#-}
primACos = primFloatACos
{-# WARNING_ON_USAGE primACos
"Warning: primACos was deprecated in Agda v2.6.2.
Please use primFloatACos instead."
#-}
primATan = primFloatATan
{-# WARNING_ON_USAGE primATan
"Warning: primATan was deprecated in Agda v2.6.2.
Please use primFloatATan instead."
#-}
primATan2 = primFloatATan2
{-# WARNING_ON_USAGE primATan2
"Warning: primATan2 was deprecated in Agda v2.6.2.
Please use primFloatATan2 instead."
#-}