{-# LANGUAGE BangPatterns #-}
{-# LANGUAGE EmptyCase #-}
{-# LANGUAGE EmptyDataDecls #-}
{-# LANGUAGE ExistentialQuantification #-}
{-# LANGUAGE NoMonomorphismRestriction #-}
{-# LANGUAGE OverloadedStrings #-}
{-# LANGUAGE PatternSynonyms #-}
{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# OPTIONS_GHC -Wno-overlapping-patterns #-}
module MAlonzo.Code.Agda.Builtin.Float where
import MAlonzo.RTE (coe, erased, AgdaAny, addInt, subInt, mulInt,
quotInt, remInt, geqInt, ltInt, eqInt, add64, sub64, mul64, quot64,
rem64, lt64, eq64, word64FromNat, word64ToNat)
import qualified MAlonzo.RTE
import qualified Data.Text
import qualified MAlonzo.RTE.Float
type T_Float_6 = Double
d_Float_6 :: a
d_Float_6
= [Char] -> a
forall a. HasCallStack => [Char] -> a
error
[Char]
"MAlonzo Runtime Error: postulate evaluated: Agda.Builtin.Float.Float"
d_primFloatInequality_8 :: Double -> Double -> Bool
d_primFloatInequality_8 = Double -> Double -> Bool
MAlonzo.RTE.Float.doubleLe
d_primFloatEquality_10 :: Double -> Double -> Bool
d_primFloatEquality_10 = Double -> Double -> Bool
MAlonzo.RTE.Float.doubleEq
d_primFloatLess_12 :: Double -> Double -> Bool
d_primFloatLess_12 = Double -> Double -> Bool
MAlonzo.RTE.Float.doubleLt
d_primFloatIsInfinite_14 :: Double -> Bool
d_primFloatIsInfinite_14 = (Double -> Bool
forall a. RealFloat a => a -> Bool
isInfinite :: Double -> Bool)
d_primFloatIsNaN_16 :: Double -> Bool
d_primFloatIsNaN_16 = (Double -> Bool
forall a. RealFloat a => a -> Bool
isNaN :: Double -> Bool)
d_primFloatIsNegativeZero_18 :: Double -> Bool
d_primFloatIsNegativeZero_18 = (Double -> Bool
forall a. RealFloat a => a -> Bool
isNegativeZero :: Double -> Bool)
d_primFloatIsSafeInteger_20 :: Double -> Bool
d_primFloatIsSafeInteger_20 = Double -> Bool
MAlonzo.RTE.Float.isSafeInteger
d_primFloatToWord64_22 :: Double -> Maybe Word64
d_primFloatToWord64_22 = Double -> Maybe Word64
MAlonzo.RTE.Float.doubleToWord64
d_primNatToFloat_24 :: Integer -> Double
d_primNatToFloat_24
= (Integer -> Double
forall a. Integral a => a -> Double
MAlonzo.RTE.Float.intToDouble :: Integer -> Double)
d_primIntToFloat_26 :: Integer -> Double
d_primIntToFloat_26
= (Integer -> Double
forall a. Integral a => a -> Double
MAlonzo.RTE.Float.intToDouble :: Integer -> Double)
d_primFloatRound_28 :: Double -> Maybe Integer
d_primFloatRound_28 = Double -> Maybe Integer
MAlonzo.RTE.Float.doubleRound
d_primFloatFloor_30 :: Double -> Maybe Integer
d_primFloatFloor_30 = Double -> Maybe Integer
MAlonzo.RTE.Float.doubleFloor
d_primFloatCeiling_32 :: Double -> Maybe Integer
d_primFloatCeiling_32 = Double -> Maybe Integer
MAlonzo.RTE.Float.doubleCeiling
d_primFloatToRatio_36 :: Double -> (Integer, Integer)
d_primFloatToRatio_36 = Double -> (Integer, Integer)
MAlonzo.RTE.Float.doubleToRatio
d_primRatioToFloat_38 :: Integer -> Integer -> Double
d_primRatioToFloat_38 = Integer -> Integer -> Double
MAlonzo.RTE.Float.ratioToDouble
d_primFloatDecode_42 :: Double -> Maybe (Integer, Integer)
d_primFloatDecode_42 = Double -> Maybe (Integer, Integer)
MAlonzo.RTE.Float.doubleDecode
d_primFloatEncode_44 :: Integer -> Integer -> Maybe Double
d_primFloatEncode_44 = Integer -> Integer -> Maybe Double
MAlonzo.RTE.Float.doubleEncode
d_primShowFloat_46 :: Double -> Text
d_primShowFloat_46
= ([Char] -> Text
Data.Text.pack ([Char] -> Text) -> (Double -> [Char]) -> Double -> Text
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Double -> [Char]
forall a. Show a => a -> [Char]
show :: Double -> Data.Text.Text)
d_primFloatPlus_48 :: Double -> Double -> Double
d_primFloatPlus_48 = Double -> Double -> Double
MAlonzo.RTE.Float.doublePlus
d_primFloatMinus_50 :: Double -> Double -> Double
d_primFloatMinus_50 = Double -> Double -> Double
MAlonzo.RTE.Float.doubleMinus
d_primFloatTimes_52 :: Double -> Double -> Double
d_primFloatTimes_52 = Double -> Double -> Double
MAlonzo.RTE.Float.doubleTimes
d_primFloatDiv_54 :: Double -> Double -> Double
d_primFloatDiv_54 = Double -> Double -> Double
MAlonzo.RTE.Float.doubleDiv
d_primFloatPow_56 :: Double -> Double -> Double
d_primFloatPow_56 = Double -> Double -> Double
MAlonzo.RTE.Float.doublePow
d_primFloatNegate_58 :: Double -> Double
d_primFloatNegate_58 = Double -> Double
MAlonzo.RTE.Float.doubleNegate
d_primFloatSqrt_60 :: Double -> Double
d_primFloatSqrt_60 = Double -> Double
MAlonzo.RTE.Float.doubleSqrt
d_primFloatExp_62 :: Double -> Double
d_primFloatExp_62 = Double -> Double
MAlonzo.RTE.Float.doubleExp
d_primFloatLog_64 :: Double -> Double
d_primFloatLog_64 = Double -> Double
MAlonzo.RTE.Float.doubleLog
d_primFloatSin_66 :: Double -> Double
d_primFloatSin_66 = Double -> Double
MAlonzo.RTE.Float.doubleSin
d_primFloatCos_68 :: Double -> Double
d_primFloatCos_68 = Double -> Double
MAlonzo.RTE.Float.doubleCos
d_primFloatTan_70 :: Double -> Double
d_primFloatTan_70 = Double -> Double
MAlonzo.RTE.Float.doubleTan
d_primFloatASin_72 :: Double -> Double
d_primFloatASin_72 = Double -> Double
MAlonzo.RTE.Float.doubleASin
d_primFloatACos_74 :: Double -> Double
d_primFloatACos_74 = Double -> Double
MAlonzo.RTE.Float.doubleACos
d_primFloatATan_76 :: Double -> Double
d_primFloatATan_76 = Double -> Double
MAlonzo.RTE.Float.doubleATan
d_primFloatATan2_78 :: Double -> Double -> Double
d_primFloatATan2_78 = Double -> Double -> Double
MAlonzo.RTE.Float.doubleATan2
d_primFloatSinh_80 :: Double -> Double
d_primFloatSinh_80 = Double -> Double
MAlonzo.RTE.Float.doubleSinh
d_primFloatCosh_82 :: Double -> Double
d_primFloatCosh_82 = Double -> Double
MAlonzo.RTE.Float.doubleCosh
d_primFloatTanh_84 :: Double -> Double
d_primFloatTanh_84 = Double -> Double
MAlonzo.RTE.Float.doubleTanh
d_primFloatASinh_86 :: Double -> Double
d_primFloatASinh_86 = Double -> Double
MAlonzo.RTE.Float.doubleASinh
d_primFloatACosh_88 :: Double -> Double
d_primFloatACosh_88 = Double -> Double
MAlonzo.RTE.Float.doubleACosh
d_primFloatATanh_90 :: Double -> Double
d_primFloatATanh_90 = Double -> Double
MAlonzo.RTE.Float.doubleATanh
d_primFloatNumericalEquality_92 :: T_Float_6 -> T_Float_6 -> Bool
d_primFloatNumericalEquality_92 :: Double -> Double -> Bool
d_primFloatNumericalEquality_92 = (Double -> Double -> Bool) -> Double -> Double -> Bool
forall a b. a -> b
coe Double -> Double -> Bool
d_primFloatEquality_10
d_primFloatNumericalLess_94 :: T_Float_6 -> T_Float_6 -> Bool
d_primFloatNumericalLess_94 :: Double -> Double -> Bool
d_primFloatNumericalLess_94 = (Double -> Double -> Bool) -> Double -> Double -> Bool
forall a b. a -> b
coe Double -> Double -> Bool
d_primFloatLess_12
d_primRound_96 :: T_Float_6 -> Maybe Integer
d_primRound_96 :: Double -> Maybe Integer
d_primRound_96 = (Double -> Maybe Integer) -> Double -> Maybe Integer
forall a b. a -> b
coe Double -> Maybe Integer
d_primFloatRound_28
d_primFloor_98 :: T_Float_6 -> Maybe Integer
d_primFloor_98 :: Double -> Maybe Integer
d_primFloor_98 = (Double -> Maybe Integer) -> Double -> Maybe Integer
forall a b. a -> b
coe Double -> Maybe Integer
d_primFloatFloor_30
d_primCeiling_100 :: T_Float_6 -> Maybe Integer
d_primCeiling_100 :: Double -> Maybe Integer
d_primCeiling_100 = (Double -> Maybe Integer) -> Double -> Maybe Integer
forall a b. a -> b
coe Double -> Maybe Integer
d_primFloatCeiling_32
d_primExp_102 :: T_Float_6 -> T_Float_6
d_primExp_102 :: Double -> Double
d_primExp_102 = (Double -> Double) -> Double -> Double
forall a b. a -> b
coe Double -> Double
d_primFloatExp_62
d_primLog_104 :: T_Float_6 -> T_Float_6
d_primLog_104 :: Double -> Double
d_primLog_104 = (Double -> Double) -> Double -> Double
forall a b. a -> b
coe Double -> Double
d_primFloatLog_64
d_primSin_106 :: T_Float_6 -> T_Float_6
d_primSin_106 :: Double -> Double
d_primSin_106 = (Double -> Double) -> Double -> Double
forall a b. a -> b
coe Double -> Double
d_primFloatSin_66
d_primCos_108 :: T_Float_6 -> T_Float_6
d_primCos_108 :: Double -> Double
d_primCos_108 = (Double -> Double) -> Double -> Double
forall a b. a -> b
coe Double -> Double
d_primFloatCos_68
d_primTan_110 :: T_Float_6 -> T_Float_6
d_primTan_110 :: Double -> Double
d_primTan_110 = (Double -> Double) -> Double -> Double
forall a b. a -> b
coe Double -> Double
d_primFloatTan_70
d_primASin_112 :: T_Float_6 -> T_Float_6
d_primASin_112 :: Double -> Double
d_primASin_112 = (Double -> Double) -> Double -> Double
forall a b. a -> b
coe Double -> Double
d_primFloatASin_72
d_primACos_114 :: T_Float_6 -> T_Float_6
d_primACos_114 :: Double -> Double
d_primACos_114 = (Double -> Double) -> Double -> Double
forall a b. a -> b
coe Double -> Double
d_primFloatACos_74
d_primATan_116 :: T_Float_6 -> T_Float_6
d_primATan_116 :: Double -> Double
d_primATan_116 = (Double -> Double) -> Double -> Double
forall a b. a -> b
coe Double -> Double
d_primFloatATan_76
d_primATan2_118 :: T_Float_6 -> T_Float_6 -> T_Float_6
d_primATan2_118 :: Double -> Double -> Double
d_primATan2_118 = (Double -> Double -> Double) -> Double -> Double -> Double
forall a b. a -> b
coe Double -> Double -> Double
d_primFloatATan2_78