Float

book/Float/_.kind2

@@ -0,0 +1,10 @@
+/// Defines a floating point number representation
+///
+///
+/// # Fields
+///
+/// * `mantissa` - The significant digits of the float
+/// * `exponent` - The power of 10 by which to multiply the mantissa. It is ALWAYS used as it was negative for floating points.
+
+data Float
+| new (mantissa: U48) (exponent: U48) 

book/Float/add.kind2

@@ -0,0 +1,40 @@
+/// Adds two Float values.
+///
+/// # Inputs
+///
+/// * `a` - The first Float value.
+/// * `b` - The second Float value.
+///
+/// # Output
+///
+/// The sum of `a` and `b` as a new Float.
+
+use Float/{new,normalize}
+use Bool/{true,false}
+use U48/{exp,less_than,equal}
+
+add
+- a: Float
+- b: Float
+: Float
+
+match a {
+  new:
+    match b {
+      new:
+        let exp_diff = (- a.exponent b.exponent)
+        let a_larger = (less_than b.exponent a.exponent)
+        match a_larger {
+          true:
+            let scaled_b = (* b.mantissa (exp 10 (- a.exponent b.exponent)))
+            let sum = (+ scaled_b a.mantissa)
+            (normalize (new sum a.exponent))
+          false:
+            let scaled_a = (* a.mantissa (exp 10 (- b.exponent a.exponent)))
+            let sum = (+ scaled_a b.mantissa)
+            (normalize (new sum b.exponent))
+        }
+
+     }
+}
+

book/Float/div.kind2

@@ -0,0 +1,37 @@
+/// Divides two Float values.
+///
+/// # Inputs
+///
+/// * `a` - The first Float value.
+/// * `b` - The second Float value.
+///
+/// # Output
+///
+/// The division of `a` and `b` as a new Float.
+/// 
+
+use Float/{new,normalize}
+use U48/{exp}
+
+div
+- a: Float
+- b: Float
+: Float
+
+// divide both mantissas and sub both exponents
+match a {
+  new:
+    match b {
+      new:
+        // Shift the numerator left by 1 digit (multiply by 10) -> this should be adjusted for N digits of precision
+        let digits_precision = 4
+        let precision = (exp 10 digits_precision)
+        let shifted_num = (Float/new (* a.mantissa precision) a.exponent)
+        match shifted_num {
+          new:
+            let new_mantissa = (/ shifted_num.mantissa b.mantissa)
+            let new_exponent = (- shifted_num.exponent b.exponent) 
+            (normalize (Float/new new_mantissa (+ new_exponent digits_precision)))
+        }
+    }
+}

book/Float/from_U48.kind2

@@ -0,0 +1,17 @@
+/// Constructs a Float from a U48 
+///
+/// # Input
+///
+/// * `a` - The U48 number.
+///
+/// # Output
+///
+/// The Float representation of that number.
+
+use Float/{new}
+
+from_U48
+- a: U48
+: Float
+
+(Float/new a 0)

book/Float/get_exponent.kind2

@@ -0,0 +1,20 @@
+/// Gets the exponent of a Float number.
+///
+/// # Input
+///
+/// * `a` - The Float number
+///
+/// # Output
+///
+/// The exponent of the float (negative) as a U48
+/// Note that the exponent 2 is interpreted as -2 in calculations.
+
+use Float/{new}
+
+get_exponent
+- a: Float
+: U48
+
+match a {
+  new: a.exponent
+}

book/Float/get_mantissa.kind2

@@ -0,0 +1,19 @@
+/// Gets the mantissa of a Float number.
+///
+/// # Input
+///
+/// * `a` - The Float number
+///
+/// # Output
+///
+/// The mantissa of the float as a U48
+
+use Float/{new}
+
+get_mantissa
+- a: Float
+: U48
+
+match a {
+  new: a.mantissa
+}

book/Float/match.kind2

@@ -0,0 +1,19 @@
+/// Provides a way to pattern match on Float values.
+///
+/// # Inputs
+///
+/// * `P` - The motive of the elimination.
+/// * `n` - The case for the Float constructor.
+/// * `x` - The Float value to match on.
+///
+/// # Output
+///
+/// The result of the elimination.
+
+match
+- P: Float -> *
+- n: ∀(mantissa: U48) ∀(exponent: U48) (P (Float/new mantissa exponent))
+- x: Float
+: (P x)
+
+(~x P n)

book/Float/mul.kind2

@@ -0,0 +1,29 @@
+/// Multiplies two Float values.
+///
+/// # Inputs
+///
+/// * `a` - The first Float value.
+/// * `b` - The second Float value.
+///
+/// # Output
+///
+/// The product of `a` and `b` as a new Float.
+
+use Float/{new,normalize}
+
+mul
+- a: Float
+- b: Float
+: Float
+
+// multiply both mantissas and add both exponents
+match a {
+  new:
+    match b {
+      new:
+        let new_mantissa = (* a.mantissa b.mantissa)
+        let new_exponent = (+ a.exponent b.exponent)
+        (normalize (Float/new new_mantissa new_exponent))
+     }
+}
+

book/Float/new.kind2

@@ -0,0 +1,17 @@
+/// Constructs a new Float instance.
+///
+/// # Inputs
+///
+/// * `mantissa` - The significant digits of the float.
+/// * `exponent` - The power of 10 by which to multiply the mantissa.
+///
+/// # Output
+///
+/// A new Float instance.
+
+new
+- mantissa: U48
+- exponent: U48
+: Float
+
+~λP λnew (new mantissa exponent)

book/Float/normalize.kind2

@@ -0,0 +1,29 @@
+/// Normalizes a Float value.
+///
+/// This function adjusts the mantissa and exponent of a Float so that:
+/// 1. There are no trailing zeros in the mantissa.
+/// 2. The exponent is adjusted accordingly.
+///
+/// Examples:
+/// - Float (40000 3) normalizes to Float (4 0)
+/// - Float (3 1) remains Float (3 1) (representing 0.3)
+/// - Float (150 2) normalizes to Float (15 1)
+///
+/// # Input
+///
+/// * `x` - The Float value to normalize.
+///
+/// # Output
+///
+/// A normalized Float value.
+
+use Float/{new}
+
+normalize
+- x: Float
+: Float
+
+match x {
+  new:
+    (Float/normalize/go x.mantissa x.exponent)
+}

book/Float/normalize/go.kind2

@@ -0,0 +1,36 @@
+/// Helper function for normalizing a Float value.
+///
+/// This function recursively adjusts the mantissa and exponent
+///
+/// # Inputs
+///
+/// * `mantissa` - The current mantissa value.
+/// * `exponent` - The current exponent value.
+///
+/// # Output
+///
+/// A normalized Float value.
+
+use Float/{new}
+
+go
+- mantissa: U48
+- exponent: U48
+: Float
+
+// the num that divides and modulo mantissa here is also the precision
+// Imagine we have 10 -> 1 digit of precision. Then 3/2 would be 15 * 10^-1, but the 1 digit precision
+// Would normalize it to 1 * 10^0 which is wrong (too bad precision).
+let mantissa_mod_10 = (% mantissa 10)
+switch mantissa_mod_10 {
+  0:
+    switch mantissa {
+      0: (new 0 0)
+      _: (go (/ mantissa 10) (- exponent 1))
+    }
+  _:
+    switch mantissa {
+      0: (new 0 0)
+      _: (new mantissa exponent)
+    }
+}

book/Float/sub.kind2

@@ -0,0 +1,40 @@
+/// Subtracts two Float values.
+///
+/// # Inputs
+///
+/// * `a` - The first Float value.
+/// * `b` - The second Float value.
+///
+/// # Output
+///
+/// The subtraction of `a` and `b` as a new Float.
+
+use Float/{new,normalize}
+use Bool/{true,false}
+use U48/{less_than,exp}
+
+sub
+- a: Float
+- b: Float
+: Float
+
+match a {
+  new:
+    match b {
+      new:
+        let exp_diff = (- a.exponent b.exponent)
+        let a_larger = (less_than b.exponent a.exponent)
+        match a_larger {
+          true:
+            let scaled_b = (* b.mantissa (exp 10 (- a.exponent b.exponent)))
+            let subt = (- scaled_b a.mantissa)
+            (normalize (new subt a.exponent))
+          false:
+            let scaled_a = (* a.mantissa (exp 10 (- b.exponent a.exponent)))
+            let subt = (- scaled_a b.mantissa)
+            (normalize (new subt b.exponent))
+        }
+
+     }
+}
+

book/Float/to_U48.kind2

@@ -0,0 +1,24 @@
+/// Constructs a U48 from a Float. It truncates the float to the next integer.
+///
+/// Examples:
+/// - 1.25 (Float/new 125 2) -> 1 : U48
+/// - 1000.0 (Float/new 1 3) -> 1000 : U48
+/// - 0.75 (Float/new 75 2) -> 0 : U48
+///
+/// # Input
+///
+/// * `a` - The Float number.
+///
+/// # Output
+///
+/// The U48 representation of that number, truncated.
+
+use Float/{new}
+
+to_U48
+- a: Float
+: U48
+
+match a {
+  new: (Float/to_U48/go a.mantissa a.exponent)
+}

book/Float/to_U48/go.kind2

@@ -0,0 +1,22 @@
+/// Helper function to convert a Float to U48.
+///
+/// This function recursively adjusts the mantissa based on the exponent.
+///
+/// # Inputs
+///
+/// * `mantissa` - The current mantissa value.
+/// * `exponent` - The current exponent value.
+///
+/// # Output
+///
+/// The U48 representation of the Float, truncated to the next integer.
+
+go
+- mantissa: U48
+- exponent: U48
+: U48
+
+switch exponent {
+  0: mantissa
+  _: (go (/ mantissa 10) (- exponent 1))
+}

book/U48/exp.kind2

@@ -0,0 +1,19 @@
+/// Computes the exponentiation of two U48 numbers.
+///
+/// # Inputs
+///
+/// * `base` - The base number.
+/// * `exp` - The exponent.
+///
+/// # Output
+///
+/// The result of `base` raised to the power of `exp`.
+
+use U48/exp/{go}
+
+exp
+- base: U48
+- exp: U48
+: U48
+
+(go base exp 1)