{-# 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

-- Agda.Builtin.Float.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"
-- Agda.Builtin.Float.primFloatInequality
d_primFloatInequality_8 :: Double -> Double -> Bool
d_primFloatInequality_8 = Double -> Double -> Bool
MAlonzo.RTE.Float.doubleLe
-- Agda.Builtin.Float.primFloatEquality
d_primFloatEquality_10 :: Double -> Double -> Bool
d_primFloatEquality_10 = Double -> Double -> Bool
MAlonzo.RTE.Float.doubleEq
-- Agda.Builtin.Float.primFloatLess
d_primFloatLess_12 :: Double -> Double -> Bool
d_primFloatLess_12 = Double -> Double -> Bool
MAlonzo.RTE.Float.doubleLt
-- Agda.Builtin.Float.primFloatIsInfinite
d_primFloatIsInfinite_14 :: Double -> Bool
d_primFloatIsInfinite_14 = (Double -> Bool
forall a. RealFloat a => a -> Bool
isInfinite :: Double -> Bool)
-- Agda.Builtin.Float.primFloatIsNaN
d_primFloatIsNaN_16 :: Double -> Bool
d_primFloatIsNaN_16 = (Double -> Bool
forall a. RealFloat a => a -> Bool
isNaN :: Double -> Bool)
-- Agda.Builtin.Float.primFloatIsNegativeZero
d_primFloatIsNegativeZero_18 :: Double -> Bool
d_primFloatIsNegativeZero_18 = (Double -> Bool
forall a. RealFloat a => a -> Bool
isNegativeZero :: Double -> Bool)
-- Agda.Builtin.Float.primFloatIsSafeInteger
d_primFloatIsSafeInteger_20 :: Double -> Bool
d_primFloatIsSafeInteger_20 = Double -> Bool
MAlonzo.RTE.Float.isSafeInteger
-- Agda.Builtin.Float.primFloatToWord64
d_primFloatToWord64_22 :: Double -> Maybe Word64
d_primFloatToWord64_22 = Double -> Maybe Word64
MAlonzo.RTE.Float.doubleToWord64
-- Agda.Builtin.Float.primNatToFloat
d_primNatToFloat_24 :: Integer -> Double
d_primNatToFloat_24
  = (Integer -> Double
forall a. Integral a => a -> Double
MAlonzo.RTE.Float.intToDouble :: Integer -> Double)
-- Agda.Builtin.Float.primIntToFloat
d_primIntToFloat_26 :: Integer -> Double
d_primIntToFloat_26
  = (Integer -> Double
forall a. Integral a => a -> Double
MAlonzo.RTE.Float.intToDouble :: Integer -> Double)
-- Agda.Builtin.Float.primFloatRound
d_primFloatRound_28 :: Double -> Maybe Integer
d_primFloatRound_28 = Double -> Maybe Integer
MAlonzo.RTE.Float.doubleRound
-- Agda.Builtin.Float.primFloatFloor
d_primFloatFloor_30 :: Double -> Maybe Integer
d_primFloatFloor_30 = Double -> Maybe Integer
MAlonzo.RTE.Float.doubleFloor
-- Agda.Builtin.Float.primFloatCeiling
d_primFloatCeiling_32 :: Double -> Maybe Integer
d_primFloatCeiling_32 = Double -> Maybe Integer
MAlonzo.RTE.Float.doubleCeiling
-- Agda.Builtin.Float.primFloatToRatio
d_primFloatToRatio_36 :: Double -> (Integer, Integer)
d_primFloatToRatio_36 = Double -> (Integer, Integer)
MAlonzo.RTE.Float.doubleToRatio
-- Agda.Builtin.Float.primRatioToFloat
d_primRatioToFloat_38 :: Integer -> Integer -> Double
d_primRatioToFloat_38 = Integer -> Integer -> Double
MAlonzo.RTE.Float.ratioToDouble
-- Agda.Builtin.Float.primFloatDecode
d_primFloatDecode_42 :: Double -> Maybe (Integer, Integer)
d_primFloatDecode_42 = Double -> Maybe (Integer, Integer)
MAlonzo.RTE.Float.doubleDecode
-- Agda.Builtin.Float.primFloatEncode
d_primFloatEncode_44 :: Integer -> Integer -> Maybe Double
d_primFloatEncode_44 = Integer -> Integer -> Maybe Double
MAlonzo.RTE.Float.doubleEncode
-- Agda.Builtin.Float.primShowFloat
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)
-- Agda.Builtin.Float.primFloatPlus
d_primFloatPlus_48 :: Double -> Double -> Double
d_primFloatPlus_48 = Double -> Double -> Double
MAlonzo.RTE.Float.doublePlus
-- Agda.Builtin.Float.primFloatMinus
d_primFloatMinus_50 :: Double -> Double -> Double
d_primFloatMinus_50 = Double -> Double -> Double
MAlonzo.RTE.Float.doubleMinus
-- Agda.Builtin.Float.primFloatTimes
d_primFloatTimes_52 :: Double -> Double -> Double
d_primFloatTimes_52 = Double -> Double -> Double
MAlonzo.RTE.Float.doubleTimes
-- Agda.Builtin.Float.primFloatDiv
d_primFloatDiv_54 :: Double -> Double -> Double
d_primFloatDiv_54 = Double -> Double -> Double
MAlonzo.RTE.Float.doubleDiv
-- Agda.Builtin.Float.primFloatPow
d_primFloatPow_56 :: Double -> Double -> Double
d_primFloatPow_56 = Double -> Double -> Double
MAlonzo.RTE.Float.doublePow
-- Agda.Builtin.Float.primFloatNegate
d_primFloatNegate_58 :: Double -> Double
d_primFloatNegate_58 = Double -> Double
MAlonzo.RTE.Float.doubleNegate
-- Agda.Builtin.Float.primFloatSqrt
d_primFloatSqrt_60 :: Double -> Double
d_primFloatSqrt_60 = Double -> Double
MAlonzo.RTE.Float.doubleSqrt
-- Agda.Builtin.Float.primFloatExp
d_primFloatExp_62 :: Double -> Double
d_primFloatExp_62 = Double -> Double
MAlonzo.RTE.Float.doubleExp
-- Agda.Builtin.Float.primFloatLog
d_primFloatLog_64 :: Double -> Double
d_primFloatLog_64 = Double -> Double
MAlonzo.RTE.Float.doubleLog
-- Agda.Builtin.Float.primFloatSin
d_primFloatSin_66 :: Double -> Double
d_primFloatSin_66 = Double -> Double
MAlonzo.RTE.Float.doubleSin
-- Agda.Builtin.Float.primFloatCos
d_primFloatCos_68 :: Double -> Double
d_primFloatCos_68 = Double -> Double
MAlonzo.RTE.Float.doubleCos
-- Agda.Builtin.Float.primFloatTan
d_primFloatTan_70 :: Double -> Double
d_primFloatTan_70 = Double -> Double
MAlonzo.RTE.Float.doubleTan
-- Agda.Builtin.Float.primFloatASin
d_primFloatASin_72 :: Double -> Double
d_primFloatASin_72 = Double -> Double
MAlonzo.RTE.Float.doubleASin
-- Agda.Builtin.Float.primFloatACos
d_primFloatACos_74 :: Double -> Double
d_primFloatACos_74 = Double -> Double
MAlonzo.RTE.Float.doubleACos
-- Agda.Builtin.Float.primFloatATan
d_primFloatATan_76 :: Double -> Double
d_primFloatATan_76 = Double -> Double
MAlonzo.RTE.Float.doubleATan
-- Agda.Builtin.Float.primFloatATan2
d_primFloatATan2_78 :: Double -> Double -> Double
d_primFloatATan2_78 = Double -> Double -> Double
MAlonzo.RTE.Float.doubleATan2
-- Agda.Builtin.Float.primFloatSinh
d_primFloatSinh_80 :: Double -> Double
d_primFloatSinh_80 = Double -> Double
MAlonzo.RTE.Float.doubleSinh
-- Agda.Builtin.Float.primFloatCosh
d_primFloatCosh_82 :: Double -> Double
d_primFloatCosh_82 = Double -> Double
MAlonzo.RTE.Float.doubleCosh
-- Agda.Builtin.Float.primFloatTanh
d_primFloatTanh_84 :: Double -> Double
d_primFloatTanh_84 = Double -> Double
MAlonzo.RTE.Float.doubleTanh
-- Agda.Builtin.Float.primFloatASinh
d_primFloatASinh_86 :: Double -> Double
d_primFloatASinh_86 = Double -> Double
MAlonzo.RTE.Float.doubleASinh
-- Agda.Builtin.Float.primFloatACosh
d_primFloatACosh_88 :: Double -> Double
d_primFloatACosh_88 = Double -> Double
MAlonzo.RTE.Float.doubleACosh
-- Agda.Builtin.Float.primFloatATanh
d_primFloatATanh_90 :: Double -> Double
d_primFloatATanh_90 = Double -> Double
MAlonzo.RTE.Float.doubleATanh
-- Agda.Builtin.Float.primFloatNumericalEquality
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
-- Agda.Builtin.Float.primFloatNumericalLess
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
-- Agda.Builtin.Float.primRound
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
-- Agda.Builtin.Float.primFloor
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
-- Agda.Builtin.Float.primCeiling
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
-- Agda.Builtin.Float.primExp
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
-- Agda.Builtin.Float.primLog
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
-- Agda.Builtin.Float.primSin
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
-- Agda.Builtin.Float.primCos
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
-- Agda.Builtin.Float.primTan
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
-- Agda.Builtin.Float.primASin
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
-- Agda.Builtin.Float.primACos
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
-- Agda.Builtin.Float.primATan
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
-- Agda.Builtin.Float.primATan2
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