Commit: 00f0108a7c05a0ab9419bae62b233e2a9a0f9622 - cammy (git)

A categorical programming language

Commit MetaInfo

• Revision: 00f0108a7c05a0ab9419bae62b233e2a9a0f9622 (tree)
• Time: 2023-02-26 16:43:31
• Author: Corbin <cds@corb...>
• Commiter: Corbin

Log Message

Force the principal branch for f-sqrt.

This halves the search space.

Change Summary

• modified: movelist/cammyo.scm
• modified: movelist/fp.scm

Incremental Difference

--- a/movelist/cammyo.scm
+++ b/movelist/cammyo.scm
@@ -253,7 +253,7 @@
                   ((== o #f) (fp-<=° i2 i1)))))
         ((== expr 'f-add) (eval-binary° fp-+° i o))
         ((== expr 'f-mul) (eval-binary° fp-*° i o))
-        ((== expr 'f-sqrt) (fp-pos° i) (== o `(left ,f))
+        ((== expr 'f-sqrt) (fp-pos° i) (== o `(left ,f)) (fp-pos° f)
          (fresh (p) (conso f f p) (eval-binary° fp-*° p i)))
         ((== expr 'f-sqrt) (== o '(right star)) (fp-neg° i)))
       ; (project (expr s t i o) (begin (pp `(eval° ,expr ,s ,t ,i ,o)) succeed))

--- a/movelist/fp.scm
+++ b/movelist/fp.scm
@@ -220,8 +220,10 @@
   ; See p6.
   (define (fp-*° f1 f2 r)
     (fresh (s1 s2 rs)
+           ; (project (f1 f2 r) (begin (pp `(fp-*? ,f1 ,f2 ,r)) succeed))
            (sign-xor° s1 s2 rs)
            (fp-sign° f1 s1) (fp-sign° f2 s2) (fp-sign° r rs)
+           ; (project (f1 f2 r) (begin (pp `(fp-* signs ,f1 ,f2 ,r)) succeed))
            (conde
              ; XXX wrong WRT IEEE 754!
              ((fp-zero° r) (conde ((fp-zero° f1)) ((fp-zero° f2))))
@@ -230,9 +232,13 @@
                      (fp-decomp° f1 s1 e1 m1)
                      (fp-decomp° f2 s2 e2 m2)
                      (*o m1 m2 m1m2)
+                     ; (project (m1 m2 m1m2) (begin (pp `(fp-* mantissas ,m1 ,m2 ,m1m2)) succeed))
                      (drop-leastsig-bit° m1m2 rm lsb)
                      (compute-exp° e1 e2 lsb re)
+                     ; (project (e1 e2 re) (begin (pp `(fp-* exponents ,e1 ,e2 ,re)) succeed))
                      (conde
                        ((fp-inf° r) (fp-overflow° re))
-                       ((fp-decomp° r rs re rm))))))))
+                       ((fp-decomp° r rs re rm))))))
+           ; (project (f1 f2 r) (begin (pp `(fp-*° ,f1 ,f2 ,r)) succeed))
+           ))
 )