Implementation of floating-point numbers (experimental).

def Int.shift2 (a b : ℕ) : ℤ → ℕ × ℕ

Equations

• Int.shift2 a b (Int.ofNat e) = (a <<< e, b)
• Int.shift2 a b (Int.negSucc e) = (a, b <<< e.succ)

inductive FP.RMode : Type

• NE: FP.RMode

instance FP.instInhabitedRMode : Inhabited FP.RMode

Equations

• FP.instInhabitedRMode = { default := FP.RMode.NE }

class FP.FloatCfg : Type

• prec : ℕ
• emax : ℕ
• precPos : 0 < FP.FloatCfg.prec
• precMax : FP.FloatCfg.prec ≤ FP.FloatCfg.emax

def FP.prec [C : FP.FloatCfg] : ℕ

Equations

• FP.prec = FP.FloatCfg.prec

def FP.emax [C : FP.FloatCfg] : ℕ

Equations

• FP.emax = FP.FloatCfg.emax

def FP.emin [C : FP.FloatCfg] : ℤ

Equations

• FP.emin = 1 - ↑FP.FloatCfg.emax

def FP.ValidFinite [C : FP.FloatCfg] (e : ℤ) (m : ℕ) : Prop

Equations

• FP.ValidFinite e m = (FP.emin ≤ e + ↑FP.prec - 1 ∧ e + ↑FP.prec - 1 ≤ ↑FP.emax ∧ e = (e + ↑m.size - ↑FP.prec) ⊔ FP.emin)

instance FP.decValidFinite [C : FP.FloatCfg] (e : ℤ) (m : ℕ) : Decidable (FP.ValidFinite e m)

Equations

• FP.decValidFinite e m = id inferInstance

inductive FP.Float [C : FP.FloatCfg] : Type

• inf: [C : FP.FloatCfg] → Bool → FP.Float
• nan: [C : FP.FloatCfg] → FP.Float
• finite: [C : FP.FloatCfg] → Bool → (e : ℤ) → (m : ℕ) → FP.ValidFinite e m → FP.Float

def FP.Float.isFinite [C : FP.FloatCfg] : FP.Float → Bool

Equations

• (FP.Float.finite a e m a_1).isFinite = true
• x.isFinite = false

def FP.toRat [C : FP.FloatCfg] (f : FP.Float) : f.isFinite = true → ℚ

Equations

• FP.toRat (FP.Float.finite s e m a) x_2 = match Int.shift2 m 1 e with | (n, d) => let r := mkRat (↑n) d; if s = true then -r else r

theorem FP.Float.Zero.valid [C : FP.FloatCfg] : FP.ValidFinite FP.emin 0

def FP.Float.zero [C : FP.FloatCfg] (s : Bool) : FP.Float

Equations

• FP.Float.zero s = FP.Float.finite s FP.emin 0 ⋯

instance FP.instInhabitedFloat [C : FP.FloatCfg] : Inhabited FP.Float

Equations

• FP.instInhabitedFloat = { default := FP.Float.zero true }

def FP.Float.sign' [C : FP.FloatCfg] : FP.Float → Semiquot Bool

Equations

• (FP.Float.inf s).sign' = pure s
• FP.Float.nan.sign' = ⊤
• (FP.Float.finite s e m a).sign' = pure s

def FP.Float.sign [C : FP.FloatCfg] : FP.Float → Bool

Equations

• (FP.Float.inf s).sign = s
• FP.Float.nan.sign = false
• (FP.Float.finite s e m a).sign = s

def FP.Float.isZero [C : FP.FloatCfg] : FP.Float → Bool

Equations

• (FP.Float.finite a e 0 a_1).isZero = true
• x.isZero = false

def FP.Float.neg [C : FP.FloatCfg] : FP.Float → FP.Float

Equations

• (FP.Float.inf s).neg = FP.Float.inf !s
• FP.Float.nan.neg = FP.Float.nan
• (FP.Float.finite s e m a).neg = FP.Float.finite (!s) e m a

def FP.divNatLtTwoPow (n d : ℕ) : ℤ → Bool

Equations

• FP.divNatLtTwoPow n d (Int.ofNat e) = decide (n < d <<< e)
• FP.divNatLtTwoPow n d (Int.negSucc e) = decide (n <<< e.succ < d)

unsafe def FP.ofPosRatDn [C : FP.FloatCfg] (n d : ℕ+) : FP.Float × Bool

unsafe def FP.nextUpPos [C : FP.FloatCfg] (e : ℤ) (m : ℕ) (v : FP.ValidFinite e m) : FP.Float

unsafe def FP.nextDnPos [C : FP.FloatCfg] (e : ℤ) (m : ℕ) (v : FP.ValidFinite e m) : FP.Float

unsafe def FP.nextUp [C : FP.FloatCfg] : FP.Float → FP.Float

unsafe def FP.nextDn [C : FP.FloatCfg] : FP.Float → FP.Float

unsafe def FP.ofRatUp [C : FP.FloatCfg] : ℚ → FP.Float

unsafe def FP.ofRatDn [C : FP.FloatCfg] (r : ℚ) : FP.Float

unsafe def FP.ofRat [C : FP.FloatCfg] : FP.RMode → ℚ → FP.Float

instance FP.Float.instNeg [C : FP.FloatCfg] : Neg FP.Float

Equations

• FP.Float.instNeg = { neg := FP.Float.neg }

unsafe def FP.Float.add [C : FP.FloatCfg] (mode : FP.RMode) : FP.Float → FP.Float → FP.Float

unsafe instance FP.Float.instAdd [C : FP.FloatCfg] : Add FP.Float

unsafe def FP.Float.sub [C : FP.FloatCfg] (mode : FP.RMode) (f1 f2 : FP.Float) : FP.Float

unsafe instance FP.Float.instSub [C : FP.FloatCfg] : Sub FP.Float

unsafe def FP.Float.mul [C : FP.FloatCfg] (mode : FP.RMode) : FP.Float → FP.Float → FP.Float

unsafe def FP.Float.div [C : FP.FloatCfg] (mode : FP.RMode) : FP.Float → FP.Float → FP.Float