This is an archived version pinned as of the submission of my master's thesis. An up-to-date version may be found online.

Floats

module primitives.floats where

open import elementary-number-theory.natural-numbers

open import foundation.booleans
open import foundation.maybe
open import foundation.universe-levels

open import primitives.machine-integers
open import primitives.strings

Idea

The Float type represents IEEE754 floats. Agda provides primitive functions to manipulate them. Floats can be written as usual, using dots as separators, e.g. 3.14.

Definitions

postulate
  Float : UU lzero

{-# BUILTIN FLOAT Float #-}

primitive
  -- Relations
  primFloatInequality : Float → Float → bool
  primFloatEquality : Float → Float → bool
  primFloatLess : Float → Float → bool
  primFloatIsInfinite : Float → bool
  primFloatIsNaN : Float → bool
  primFloatIsNegativeZero : Float → bool
  primFloatIsSafeInteger : Float → bool
  -- Conversions
  primFloatToWord64 : Float → Maybe' Word64
  primNatToFloat : ℕ → 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
  -- Operations
  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