wip68

2 files changed, 80 insertions, 45 deletions

diff --git a/vikalpa.scm b/vikalpa.scm
index 8713e25..3e45883 100644
--- a/vikalpa.scm
+++ b/vikalpa.scm
@@ -718,12 +718,12 @@
                          (result/error 'guard-error `(,name ,@args) `(and ,@gs))))))
              (else (result/error 'function-not-found name)))))
          ((if-form? expr)
-          (let ((test/result (eval (if-form-test expr))))
-            (if (error? test/result)
+          (let ((test/result (eval (result/expr (if-form-test expr)))))
+            (if (result/error? test/result)
                 test/result
                 (if (expr-unquote (result/expr-expr test/result))
-                    (eval (if-form-then expr))
-                    (eval (if-form-else expr))))))
+                    (eval (result/expr (if-form-then expr)))
+                    (eval (result/expr (if-form-else expr)))))))
          ((variable? expr)
           (result/error 'eval 'variable-found expr))
          (else
diff --git a/vikalpa/prelude.scm b/vikalpa/prelude.scm
index 2da6e8e..e24d32d 100644
--- a/vikalpa/prelude.scm
+++ b/vikalpa/prelude.scm
@@ -61,8 +61,10 @@
     ((implies x y) (if x y #t))
     ((implies x y z . rest)
      (if x (implies y z . rest) #t)))
-  (define-syntax-rules is-a ()
-    ((is-a x y) (implies x (equal? y #t)))))
+  (define-syntax-rules predicate ()
+    ((predicate x) (implies x (equal? x #t))))
+  (define-syntax-rules is ()
+    ((is x y) (implies x (equal? y #t)))))
 
 (define-system prelude/axiom/equal (prelude/macro)
   (define-axiom equal-same (x)
@@ -91,71 +93,61 @@
 
 (define-system prelude/number (prelude/axiom/if)
   (define-core-function number? (x) number?)
-  (define-axiom number-predicate (x)
-    (is-a (number? x) (number? x)))
+  (define-axiom (predicate number?) (x) (predicate (number? x)))
 
   (define-core-function real? (x) real?)
-  (define-axiom real-predicate (x)
-    (implies (real? x) (equal? (real? x) #t)))
-  (define-axiom real-is-a-numbers (x)
-    (implies (real? x) (equal? (number? x) #t)))
+  (define-axiom (predicate real?) (x) (predicate (real? x)))
+  (define-axiom (is real? number?) (x) (is (real? x) (number? x)))
 
   (define-core-function integer? (x) integer?)
-  (define-axiom integer-predicate (x)
-    (implies (integer? x) (equal? (integer? x) #t)))
-  (define-axiom integer-is-a-real (x)
-    (implies (integer? x) (equal? (number? x) #t)))
+  (define-axiom (predicate integer?) (x) (predicate (integer? x)))
+  (define-axiom (is integer? real?) (x) (is (integer? x) (real? x)))
 
   (define-core-function/guard exact? (x) (number? x) exact?)
-  (define-axiom exact-predicate (x)
-    (implies (exact? x) (equal? (exact? x) #t)))
+  (define-axiom (predicate exact?) (x) (predicate (exact? x)))
 
   (define-function/guard inexact? (x)
     (number? x)
     (not (exact? x)))
-  (define-theorem inexact-predicate (x)
-    (implies (inexact? x) (equal? (inexact? x) #t)))
+  (define-theorem (predicate inexact?) (x) (predicate (inexact? x)))
 
   (define-core-function exact-integer? (x) exact-integer?)
-  (define-axiom exact-integer-predicate (x)
-    (implies (exact-integer? x) (equal? (exact-integer? x) #t)))
-  (define-axiom exact-integer-is-a-integer (x)
-    (implies (exact-integer? x) (equal? (integer? x) #t)))
-  (define-axiom exact-integer-is-a-exact (x)
-    (implies (exact-integer? x) (equal? (exact? x) #t)))
-
+  (define-axiom (predicate exact-integer?) (x) (predicate (exact-integer? x)))
+  (define-axiom (is exact-integer? integer?) (x)
+    (is (exact-integer? x)
+        (integer? x)))
+  (define-axiom (is exact-integer? exact?) (x) (is (exact-integer? x)
+                                                   (exact? x)))
+  (define-theorem (is exact-integer? real?) (x)
+    (is (exact-integer? x) (real? x)))
   (define-core-function/guard < (x y) (and (real? x) (real? y)) <)
-  (define-axiom less-than-predicate (x y)
-    (implies (< x y) (equal? (< x y) #t)))
+  (define-axiom (predicate <) (x y) (predicate (< x y)))
 
   (define-function/guard positive? (x)
     (real? x)
     (< 0 x))
-  (define-theorem positive-predicate (x)
-    (implies (positive? x) (equal? (positive? x) #t)))
+  (define-theorem (predicate positive?) (x) (predicate (positive? x)))
   (define-function/guard negative? (x)
     (real? x)
     (< x 0))
-  (define-theorem negative-predicate (x)
-    (implies (negative? x) (equal? (negative? x) #t)))
+  (define-theorem (predicate negative?) (x) (predicate (negative? x)))
 
   (define-function exact-positive-integer? (x)
     (and (exact-integer? x)
          (positive? x)))
-  (define-theorem exact-positive-integer-predicate (x)
-    (implies (exact-positive-integer? x)
-             (equal? (exact-positive-integer? x) #t)))
+  (define-theorem (predicate exact-positive-integer?) (x)
+    (predicate (exact-positive-integer? x)))
 
   (define-function exact-zero? (x) (equal? x 0))
-  (define-theorem exact-zero-predicate (x)
-    (implies (exact-zero? x) (equal? (exact-zero? x) #t)))
+  (define-theorem (predicate exact-zero?) (x)
+    (predicate (exact-zero? x)))
 
   (define-function natural? (x)
     (if (exact-zero? x)
         #t
         (exact-positive-integer? x)))
   (define-theorem (predicate natural?) (x)
-    (implies (natural? x) (equal? (natural? x) #t))))
+    (predicate (natural? x))))
 
 (define-system prelude/measure/natural (prelude/number)
   (set-measure-predicate natural?)
@@ -171,7 +163,7 @@
   (define-proof inexact?
     ((rewrite (2) if-nest)
      (rewrite () if-same)))
-  (define-proof inexact-predicate
+  (define-proof (predicate inexact?)
     ((rewrite (1) inexact?)
      (rewrite () if-not)
      (rewrite (3 1) inexact?)
@@ -183,10 +175,10 @@
      (rewrite (2 1) if-true)
      (rewrite (2) if-nest)
      (rewrite () if-same)))
-  (define-proof positive-predicate
+  (define-proof (predicate positive?)
     ((rewrite (1) positive?)
      (rewrite (2 1) positive?)
-     (rewrite (2 1) less-than-predicate)
+     (rewrite (2 1) (predicate <))
      (eval (2))
      (rewrite () if-same)))
   (define-proof negative?
@@ -194,10 +186,53 @@
      (eval (2 1))
      (rewrite (2) if-true)
      (rewrite () if-same)))
-  (define-proof negative-predicate
+  (define-proof (predicate negative?)
     ((rewrite (1) negative?)
      (rewrite (2 1) negative?)
-     (rewrite (2 1) less-than-predicate)
+     (rewrite (2 1) (predicate <))
+     (eval (2))
+     (rewrite () if-same)))
+  (define-proof (is exact-integer? real?)
+    ((rewrite (2) if-same (set x (integer? x)))
+     (rewrite (2 2 1) (is integer? real?))
+     (eval (2 2))
+     (rewrite (2 1) (is exact-integer? integer?))
+     (rewrite (2) if-true)
+     (rewrite () if-same)))
+  (define-proof exact-positive-integer?
+    ((rewrite (1 2) (is exact-integer? real?))
+     (rewrite (1) if-same)
+     (eval ())))
+  (define-proof (predicate exact-positive-integer?)
+    ((rewrite (1) exact-positive-integer?)
+     (rewrite () if-same (set x (exact-integer? x)))
+     (rewrite (3 1) if-nest)
+     (rewrite (3) if-false)
+     (rewrite (2 1) if-nest)
+     (rewrite (2 2 1) exact-positive-integer?)
+     (rewrite (2 2 1 1) (predicate exact-integer?))
+     (rewrite (2 2 1 2) (predicate positive?))
+     (eval (2 2))
+     (rewrite (2) if-same)
+     (rewrite () if-same)))
+  (define-proof (predicate exact-zero?)
+    ((rewrite (1) exact-zero?)
+     (rewrite (2 1 1) equal-if)
      (eval (2))
+     (rewrite () if-same)))
+  (define-proof (predicate natural?)
+    ((rewrite (1) natural?)
+     (rewrite () if-same (set x (exact-zero? x)))
+     (rewrite (2 1) if-nest)
+     (rewrite (2) if-true)
+     (rewrite (3 1) if-nest)
+     (rewrite (1) exact-zero?)
+     (rewrite (2 1 1) equal-if)
+     (eval (2))
+     (rewrite (1) exact-zero?)
+     (rewrite (3 2 1) natural?)
+     (rewrite (3 2 1) if-nest)
+     (rewrite (3 2 1) (predicate exact-positive-integer?))
+     (eval (3 2))
+     (rewrite (3) if-same)
      (rewrite () if-same))))
-