From aa1b446c3905f3b84b4bc71febfd75da72659399 Mon Sep 17 00:00:00 2001
From: Sergei Winitzki <winitzki@gmail.com>
Date: Sun, 20 Oct 2024 10:52:47 +0200
Subject: [PATCH] first working draft version of sqrt

---
 tutorial/Float/Type.dhall     |  3 +++
 tutorial/Float/numerics.dhall | 17 +++++++++++++++++
 tutorial/Float/sqrt.dhall     | 31 ++++++++++++++++++++++---------
 3 files changed, 42 insertions(+), 9 deletions(-)

diff --git a/tutorial/Float/Type.dhall b/tutorial/Float/Type.dhall
index 0e09053a..d5a564a4 100644
--- a/tutorial/Float/Type.dhall
+++ b/tutorial/Float/Type.dhall
@@ -40,6 +40,8 @@ let Float/leadDigit = λ(a : Float) → a.leadDigit
 
 let Float/mantissa = λ(a : Float) → a.mantissa
 
+let Float/topPower = λ(a : Float) → a.topPower
+
 let Float/exponent = λ(a : Float) → a.exponent
 
 let N = ./numerics.dhall
@@ -324,4 +326,5 @@ in  { Base
     , Float/leadDigit
     , Float/mantissa
     , Float/exponent
+    , Float/topPower
     }
diff --git a/tutorial/Float/numerics.dhall b/tutorial/Float/numerics.dhall
index ff94f5e5..b7b06567 100644
--- a/tutorial/Float/numerics.dhall
+++ b/tutorial/Float/numerics.dhall
@@ -7,6 +7,14 @@ let Natural/lessThan =
       https://prelude.dhall-lang.org/Natural/lessThan
         sha256:3381b66749290769badf8855d8a3f4af62e8de52d1364d838a9d1e20c94fa70c
 
+let Integer/abs =
+      https://prelude.dhall-lang.org/Integer/abs
+        sha256:35212fcbe1e60cb95b033a4a9c6e45befca4a298aa9919915999d09e69ddced1
+
+let Integer/positive =
+      https://prelude.dhall-lang.org/Integer/positive
+        sha256:7bdbf50fcdb83d01f74c7e2a92bf5c9104eff5d8c5b4587e9337f0caefcfdbe3
+
 let power =
       λ(x : Natural) →
       λ(y : Natural) →
@@ -92,10 +100,19 @@ let egyptian_div_mod
 
         in  List/fold Natural powers2 Result update { div = 0, rem = a }
 
+let Integer/mapSign
+    : (Natural → Natural) → Integer → Integer
+    = λ(f : Natural → Natural) →
+      λ(x : Integer) →
+        if    Integer/positive x
+        then  Natural/toInteger (f (Integer/clamp x))
+        else  Integer/negate (Natural/toInteger (f (Integer/abs x)))
+
 in  { log
     , power
     , Result
     , divmod = unsafeDivMod
     , divrem = egyptian_div_mod
     , powersOf2Until
+    , Integer/mapSign
     }
diff --git a/tutorial/Float/sqrt.dhall b/tutorial/Float/sqrt.dhall
index ab60ab41..a1e06a1f 100644
--- a/tutorial/Float/sqrt.dhall
+++ b/tutorial/Float/sqrt.dhall
@@ -42,6 +42,11 @@ let Float/divide = ./divide.dhall
 
 let Float/multiply = ./multiply.dhall
 
+let Integer/divide =
+      λ(i : Integer) →
+      λ(n : Natural) →
+        N.Integer/mapSign (λ(p : Natural) → (T.divmod p n).div) i
+
 let compute_init_sqrt
                       -- if a < 17 then (15.0 + 3 * a) / 15.0   else  (45.0 + a) / 14.0
                       =
@@ -50,16 +55,22 @@ let compute_init_sqrt
 
         let p
             : { new_exponent : Integer, lead_digits : Natural }
-            = if    Natural/isEven (Integer/abs exp)
+            = if    Natural/even (Integer/abs exp)
               then  { new_exponent =
-                        N.Integer/divide
-                          (Integer/subtract (T.Float/topPower x) exp)
+                        Integer/divide
+                          ( Integer/subtract
+                              (Natural/toInteger (T.Float/topPower x))
+                              exp
+                          )
                           2
                     , lead_digits = T.Float/leadDigit x
                     }
               else  { new_exponent =
-                        N.Integer/divide
-                          (Integer/subtract (1 + T.Float/topPower x) exp)
+                        Integer/divide
+                          ( Integer/subtract
+                              (Natural/toInteger (1 + T.Float/topPower x))
+                              exp
+                          )
                           2
                     , lead_digits = 10 * T.Float/leadDigit x
                     }
@@ -67,7 +78,7 @@ let compute_init_sqrt
         let init_approximation =
               if    Natural/lessThan p.lead_digits 17
               then  (T.divmod (3 * p.lead_digits + 15) 15).div
-              else  T.divmod ((p.lead_gitis + 45) 14).div
+              else  (T.divmod (p.lead_digits + 45) 14).div
 
         in  T.Float/create (Natural/toInteger init_approximation) p.new_exponent
 
@@ -81,7 +92,7 @@ let Float/sqrt
 
         in  let init
                 : Accum
-                = { x = compute_init_sqrt x, prec = 1 }
+                = { x = compute_init_sqrt p, prec = 1 }
 
             let update
                 : Accum → Accum
@@ -96,8 +107,10 @@ let Float/sqrt
 
                     in  { x, prec }
 
-            in  (Natural/fold iterations update init).x
+            in  (./rounding.dhall).Float/round
+                  (Natural/fold iterations Accum update init).x
+                  prec
 
-let _ = assert : Float/sqrt (T.Float/create +2 +0) 5 ≡ Float/create +14142 -4
+let _ = assert : Float/sqrt (T.Float/create +2 +0) 5 ≡ T.Float/create +14142 -4
 
 in  Float/sqrt