Zulip Chat Archive

Stream: lean4

Topic: Casting Float to some integral type


view this post on Zulip Reed Mullanix (Jan 13 2021 at 07:15):

For the life of me I can't figure out how to turn a Float into an integral type (IE: Int, UInt32, etc). For the record, I've tried some nasty C FFI hacks as well, but I don't think I've figured out exactly how to get that to generate the requisite code.

view this post on Zulip Reid Barton (Jan 13 2021 at 12:31):

how about

def Float.toInt (f : Float) : Int :=
(f.toString.takeWhile (fun c => c == '-' || c.isDigit)).toInt!

:upside_down:

view this post on Zulip Sebastian Ullrich (Jan 13 2021 at 12:41):

Something like

@[extern c inline "(uint32)#1"]  constant Float.toUInt32 : Float  UInt32

should work, though you won't be able to use it in the interpreter without compiling it into a native library first. Implementing Int/Nat should be a bit more interesting if it's supposed to work on values > 2^64...

view this post on Zulip Reed Mullanix (Jan 13 2021 at 17:07):

That inline cast was my first attempt, but I couldn't figure out how to compile as a native library. The solution I settled on was

partial def UInt8.ofFloat (x : Float) : UInt8 :=
  if x >= 255 then 255
  else if x < 0 then 0
  else go 0 255

  where
    go (lo : Nat) (hi : Nat) : UInt8 :=
      let mid := (lo + hi)/2
      if hi <= lo then (UInt8.ofNat $ lo - 1)
      else if x < (Float.ofNat mid) then go lo mid else go (mid + 1) hi

Also, while floats are up for discussion, I think there is a missing instance for Neg Float


Last updated: May 07 2021 at 12:15 UTC