Move Float16 Prelude off the Double primitive

.github/workflows/ci-edric-wrapper.yml

@@ -5,21 +5,21 @@ on:
     paths:
       - 'edric'
       - 'scripts/ensure-chez.sh'
-      - 'src/Parser/Source.idr'
-      - 'libs/prelude/Prelude.idr'
-      - 'libs/prelude/Prelude/Float16.idr'
-      - 'libs/prelude/prelude.ipkg'
+      - 'bootstrap/idris2_app/**'
+      - 'src/**'
+      - 'libs/prelude/**'
       - 'tests/idris2/basic/edric007/**'
+      - 'support/chez/**'
       - '.github/workflows/ci-edric-wrapper.yml'
   pull_request:
     paths:
       - 'edric'
       - 'scripts/ensure-chez.sh'
-      - 'src/Parser/Source.idr'
-      - 'libs/prelude/Prelude.idr'
-      - 'libs/prelude/Prelude/Float16.idr'
-      - 'libs/prelude/prelude.ipkg'
+      - 'bootstrap/idris2_app/**'
+      - 'src/**'
+      - 'libs/prelude/**'
       - 'tests/idris2/basic/edric007/**'
+      - 'support/chez/**'
       - '.github/workflows/ci-edric-wrapper.yml'
 
 jobs:
@@ -70,6 +70,19 @@ jobs:
     steps:
       - uses: actions/checkout@v4
 
+      - name: Require Float16 Prelude to avoid the wide primitive
+        shell: bash
+        run: |
+          set -euo pipefail
+          file=libs/prelude/Prelude/Float16.idr
+          ! grep -q 'Double' "$file"
+          ! grep -q 'prim__cast_FloatInteger' "$file"
+          grep -q 'float16Carrier : Float' "$file"
+          grep -q 'prim__add_Float' "$file"
+          grep -q 'prim__div_Float' "$file"
+          grep -q 'FloatType' src/Core/TT/Primitive.idr
+          grep -q 'blodwen-float32' support/chez/support.ss
+
       - name: Install Chez Scheme
         run: |
           sudo apt-get update

libs/base/Language/Reflection/TT.idr

@@ -133,6 +133,7 @@ data PrimType
     | CharType
     | DoubleType
     | WorldType
+    | FloatType
 
 %name PrimType pty
 
@@ -172,6 +173,7 @@ Show PrimType where
   show CharType = "Char"
   show DoubleType = "Double"
   show WorldType = "%World"
+  show FloatType = "Float"
 
 export
 Show Constant where
@@ -436,6 +438,7 @@ Eq PrimType where
   CharType    == CharType    = True
   DoubleType  == DoubleType  = True
   WorldType   == WorldType   = True
+  FloatType   == FloatType   = True
   _ == _ = False
 
 public export

libs/prelude/Builtin.idr

@@ -273,6 +273,11 @@ public export
 FromDouble Double where
   fromDouble s = s
 
+%inline
+public export
+FromDouble Float where
+  fromDouble = prim__cast_DoubleFloat
+
 %defaulthint
 %inline
 public export

libs/prelude/Prelude/EqOrd.idr

@@ -80,6 +80,10 @@ public export
 Eq Double where
   x == y = intToBool (prim__eq_Double x y)
 
+public export
+Eq Float where
+  x == y = intToBool (prim__eq_Float x y)
+
 public export
 Eq Char where
   x == y = intToBool (prim__eq_Char x y)
@@ -246,6 +250,13 @@ Ord Double where
   (>) x y = intToBool (prim__gt_Double x y)
   (>=) x y = intToBool (prim__gte_Double x y)
 
+public export
+Ord Float where
+  (<) x y = intToBool (prim__lt_Float x y)
+  (<=) x y = intToBool (prim__lte_Float x y)
+  (>) x y = intToBool (prim__gt_Float x y)
+  (>=) x y = intToBool (prim__gte_Float x y)
+
 public export
 Ord String where
   (<) x y = intToBool (prim__lt_String x y)

libs/prelude/Prelude/Float16.idr

@@ -9,100 +9,123 @@ import Prelude.Types
 
 %default total
 
-||| Idriç's ordinary floating value. The current compiler carries the value in
-||| a Double internally, but every constructor and arithmetic operation rounds
-||| through the IEEE-754 binary16 boundary. Backends may replace this carrier
-||| with a native/unboxed representation without changing source semantics.
+||| Idriç's ordinary floating value. The Prelude carrier is the compiler's
+||| primitive floating value, not an inherited wider floating primitive.
+||| Every constructor and arithmetic operation rounds through the IEEE-754
+||| binary16 boundary. A later compiler slice can make binary16 itself a core
+||| primitive without changing this source-level contract.
 public export
 record Float16 where
   constructor MkFloat16
-  float16Carrier : Double
+  float16Carrier : Float
 
 private
-roundNearestEven : Double -> Integer
+asFloat : Integer -> Float
+asFloat = prim__cast_IntegerFloat
+
+private
+half : Float
+half = assert_total (prim__div_Float (asFloat 1) (asFloat 2))
+
+||| Find the integer floor of a nonnegative primitive floating value inside a
+||| known integer interval. The recursion depth is supplied explicitly so the
+||| Prelude never needs a floating-to-integer primitive.
+private
+floorBounded : Nat -> Integer -> Integer -> Float -> Integer
+floorBounded Z lower upper value = lower
+floorBounded (S fuel) lower upper value =
+  let width = prim__sub_Integer upper lower in
+    if width <= 1
+       then lower
+       else
+         let midpoint = prim__add_Integer
+                          lower
+                          (assert_total (prim__div_Integer width 2))
+             midpointValue = asFloat midpoint in
+           if midpointValue <= value
+              then floorBounded fuel midpoint upper value
+              else floorBounded fuel lower midpoint value
+
+private
+roundNearestEven : Float -> Integer
 roundNearestEven value =
-  let lower = prim__cast_DoubleInteger value
-      lowerValue = prim__cast_IntegerDouble lower
-      fraction = prim__sub_Double value lowerValue in
-    if fraction < 0.5
+  let lower = floorBounded 12 0 2048 value
+      lowerValue = asFloat lower
+      fraction = prim__sub_Float value lowerValue in
+    if fraction < half
        then lower
-       else if fraction > 0.5
+       else if fraction > half
                then prim__add_Integer lower 1
                else if assert_total (prim__mod_Integer lower 2) == 0
                        then lower
                        else prim__add_Integer lower 1
 
 ||| Return the binary16 unit in the last place for a positive finite value.
-||| The recursive bound is fixed by the binary16 exponent range, so this is a
-||| small deterministic source-semantics operation rather than an unbounded
-||| numeric search.
+||| The recursive bound is fixed by the binary16 exponent range.
 private
-halfStep : Nat -> Double -> Double -> Double
-halfStep Z value threshold = 0.000000059604644775390625 -- 2^-24, subnormal step
+halfStep : Nat -> Float -> Float -> Float
+halfStep Z value threshold =
+  assert_total (prim__div_Float (asFloat 1) (asFloat 16777216)) -- 2^-24
 halfStep (S fuel) value threshold =
   if value >= threshold
-     then assert_total (prim__div_Double threshold 1024.0)
-     else halfStep fuel value (assert_total (prim__div_Double threshold 2.0))
+     then assert_total (prim__div_Float threshold (asFloat 1024))
+     else halfStep fuel value
+                   (assert_total (prim__div_Float threshold (asFloat 2)))
 
 private
-quantizeFloat16Carrier : Double -> Double
+quantizeFloat16Carrier : Float -> Float
 quantizeFloat16Carrier value =
   if value /= value
      then value -- preserve NaN
-     else if value == 0.0
+     else if value == asFloat 0
              then value -- preserve signed zero
              else
-               let negative = value < 0.0
-                   magnitude = if negative then prim__negate_Double value else value in
-                 if magnitude >= 65520.0
-                    then let infinity = assert_total (prim__div_Double 1.0 0.0) in
-                           if negative then prim__negate_Double infinity else infinity
+               let negative = value < asFloat 0
+                   magnitude = if negative then prim__negate_Float value else value in
+                 if magnitude >= asFloat 65520
+                    then let infinity = assert_total
+                                          (prim__div_Float (asFloat 1) (asFloat 0)) in
+                           if negative then prim__negate_Float infinity else infinity
                     else
-                      let step = halfStep 29 magnitude 32768.0
-                          scaled = assert_total (prim__div_Double magnitude step)
+                      let step = halfStep 29 magnitude (asFloat 32768)
+                          scaled = assert_total (prim__div_Float magnitude step)
                           rounded = roundNearestEven scaled
-                          roundedValue = prim__mul_Double
-                                           (prim__cast_IntegerDouble rounded)
-                                           step in
+                          roundedValue = prim__mul_Float (asFloat rounded) step in
                         if negative
-                           then prim__negate_Double roundedValue
+                           then prim__negate_Float roundedValue
                            else roundedValue
 
-||| Explicitly pass a host/compiler floating carrier through the binary16
-||| rounding boundary.
+||| Explicitly pass a primitive floating value through the binary16 rounding
+||| boundary. The `.idric` lexer uses this for decimal literals.
 public export
-idricFloat16 : Double -> Float16
+idricFloat16 : Float -> Float16
 idricFloat16 value = MkFloat16 (quantizeFloat16Carrier value)
 
-public export
-FromDouble Float16 where
-  fromDouble = idricFloat16
-
 public export
 Num Float16 where
   (MkFloat16 left) + (MkFloat16 right) =
-    idricFloat16 (prim__add_Double left right)
+    idricFloat16 (prim__add_Float left right)
   (MkFloat16 left) * (MkFloat16 right) =
-    idricFloat16 (prim__mul_Double left right)
-  fromInteger value = idricFloat16 (prim__cast_IntegerDouble value)
+    idricFloat16 (prim__mul_Float left right)
+  fromInteger value = idricFloat16 (asFloat value)
 
 public export
 Neg Float16 where
-  negate (MkFloat16 value) = idricFloat16 (prim__negate_Double value)
+  negate (MkFloat16 value) = idricFloat16 (prim__negate_Float value)
   (MkFloat16 left) - (MkFloat16 right) =
-    idricFloat16 (prim__sub_Double left right)
+    idricFloat16 (prim__sub_Float left right)
 
 public export
 Abs Float16 where
   abs (MkFloat16 value) =
-    if value < 0.0
-       then idricFloat16 (prim__negate_Double value)
+    if value < asFloat 0
+       then idricFloat16 (prim__negate_Float value)
        else MkFloat16 value
 
 public export
 Fractional Float16 where
   (MkFloat16 left) / (MkFloat16 right) =
-    idricFloat16 (assert_total (prim__div_Double left right))
+    idricFloat16 (assert_total (prim__div_Float left right))
 
 public export
 Eq Float16 where
@@ -115,6 +138,51 @@ Ord Float16 where
   (MkFloat16 left) > (MkFloat16 right) = left > right
   (MkFloat16 left) >= (MkFloat16 right) = left >= right
 
+private
+fractionDigits : Nat -> Float -> String
+fractionDigits Z fraction = ""
+fractionDigits (S fuel) fraction =
+  let scaled = prim__mul_Float fraction (asFloat 10)
+      digit = floorBounded 4 0 10 scaled
+      rest = prim__sub_Float scaled (asFloat digit) in
+    show digit ++ fractionDigits fuel rest
+
+private
+stripLeadingZeros : List Char -> List Char
+stripLeadingZeros ('0' :: rest) = stripLeadingZeros rest
+stripLeadingZeros rest = rest
+
+private
+trimTrailingZeros : String -> String
+trimTrailingZeros digits =
+  let trimmed = reverse (stripLeadingZeros (reverse (unpack digits))) in
+    case trimmed of
+      [] => "0"
+      _ => pack trimmed
+
+||| Format the binary16 value without routing through the inherited wide
+||| floating primitive. Eight fractional decimal digits are enough to
+||| distinguish every finite binary16 value; trailing zeroes are removed.
+private
+showFloat16Carrier : Float -> String
+showFloat16Carrier value =
+  if value /= value
+     then "NaN"
+     else
+       let infinity = assert_total (prim__div_Float (asFloat 1) (asFloat 0)) in
+         if value == infinity
+            then "Infinity"
+            else if value == prim__negate_Float infinity
+                    then "-Infinity"
+                    else
+                      let negative = value < asFloat 0
+                          magnitude = if negative then prim__negate_Float value else value
+                          whole = floorBounded 17 0 65536 magnitude
+                          fraction = prim__sub_Float magnitude (asFloat whole)
+                          sign = if negative then "-" else ""
+                          decimals = trimTrailingZeros (fractionDigits 8 fraction) in
+                        sign ++ show whole ++ "." ++ decimals
+
 export
 Show Float16 where
-  showPrec precedence (MkFloat16 value) = showPrec precedence value
+  showPrec _ (MkFloat16 value) = showFloat16Carrier value

libs/prelude/Prelude/Num.idr

@@ -377,3 +377,25 @@ Abs Double where
 public export
 Fractional Double where
   (/) = prim__div_Double
+
+-- Float
+
+public export
+Num Float where
+  (+) = prim__add_Float
+  (*) = prim__mul_Float
+  fromInteger = prim__cast_IntegerFloat
+
+%inline
+public export
+Neg Float where
+  negate x = prim__negate_Float x
+  (-) = prim__sub_Float
+
+public export
+Abs Float where
+  abs x = if x < 0 then -x else x
+
+public export
+Fractional Float where
+  (/) = prim__div_Float

src/Compiler/RefC/RefC.idr

@@ -137,6 +137,7 @@ cPrimType StringType = "string"
 cPrimType CharType = "Char"
 cPrimType DoubleType = "Double"
 cPrimType WorldType = "void"
+cPrimType FloatType = "Float"
 
 ||| Generate scheme for a primitive function.
 cOp : {0 arity : Nat} -> PrimFn arity -> Vect arity String -> String

src/Compiler/Scheme/Common.idr

@@ -138,6 +138,11 @@ constPrimitives = MkConstantPrimitives {
 
 ||| Generate scheme for a primitive function.
 schOp : {0 arity : Nat} -> PrimFn arity -> Vect arity Builder -> Core Builder
+schOp (Add FloatType) [x, y] = pure $ op "blodwen-float32" [op "+" [x, y]]
+schOp (Sub FloatType) [x, y] = pure $ op "blodwen-float32" [op "-" [x, y]]
+schOp (Mul FloatType) [x, y] = pure $ op "blodwen-float32" [op "*" [x, y]]
+schOp (Div FloatType) [x, y] = pure $ op "blodwen-float32" [op "/" [x, y]]
+schOp (Neg FloatType) [x] = pure $ op "blodwen-float32" [op "-" [x]]
 schOp (Add ty) [x, y] = pure $ add (intKind ty) x y
 schOp (Sub ty) [x, y] = pure $ sub (intKind ty) x y
 schOp (Mul ty) [x, y] = pure $ mul (intKind ty) x y
@@ -187,6 +192,9 @@ schOp DoubleSqrt [x] = pure $ op "flsqrt" [x]
 schOp DoubleFloor [x] = pure $ op "flfloor" [x]
 schOp DoubleCeiling [x] = pure $ op "flceiling" [x]
 
+schOp (Cast IntegerType FloatType) [x] = pure $ op "blodwen-float32" [op "exact->inexact" [x]]
+schOp (Cast DoubleType FloatType)  [x] = pure $ op "blodwen-float32" [x]
+schOp (Cast FloatType DoubleType)  [x] = pure x
 schOp (Cast DoubleType StringType)  [x] = pure $ op "number->string" [x]
 schOp (Cast CharType StringType)    [x] = pure $ op "string" [x]
 schOp (Cast StringType DoubleType)  [x] = pure $ op "cast-string-double" [x]

src/Core/Hash.idr

@@ -291,6 +291,7 @@ Hashable PrimType where
     CharType    => h `hashWithSalt` 12
     DoubleType  => h `hashWithSalt` 13
     WorldType   => h `hashWithSalt` 14
+    FloatType   => h `hashWithSalt` 15
 
 export
 Hashable Constant where