wip70

2 files changed, 73 insertions, 106 deletions

diff --git a/vikalpa.scm b/vikalpa.scm
index 3e45883..79f6fb1 100644
--- a/vikalpa.scm
+++ b/vikalpa.scm
@@ -95,7 +95,7 @@
   (format port "#<~a: ~s>"
           sym (cons (get-name d) (get-variables d))))
 
-(define-method (write (s <system>) port)
+(define-method (display (s <system>) port)
   (format port "#<system: function: ~a theorem: ~a macro: ~a>"
           (length (filter (cut is-a? <> <function*>)
                           (get-definitions s)))
@@ -104,22 +104,14 @@
           (length (filter (cut is-a? <> <macro>)
                           (get-definitions s)))))
 
-(define-method (write (d <macro>) port)
-  (write-definition 'macro d port))
-(define-method (write (d <conjecture>) port)
-  (write-definition 'conjecture d port))
-(define-method (write (d <theorem>) port)
-  (write-definition 'theorem d port))
-(define-method (write (d <axiom>) port)
-  (write-definition 'axiom d port))
-(define-method (write (d <axiom>) port)
-  (write-definition 'axiom d port))
-(define-method (write (d <function>) port)
-  (write-definition 'function d port))
-(define-method (write (d <core-function>) port)
-  (write-definition 'core-function d port))
-(define-method (write (d <total-function>) port)
-  (write-definition 'total-function d port))
+(define-method (write (s <system>) port)
+  (format port "#<system: function: ~a theorem: ~a macro: ~a>"
+          (length (filter (cut is-a? <> <function*>)
+                          (get-definitions s)))
+          (length (filter (cut is-a? <> <theorem*>)
+                          (get-definitions s)))
+          (length (filter (cut is-a? <> <macro>)
+                          (get-definitions s)))))
 
 (define-method (lookup name (s <system>))
   (find (lambda (x)
@@ -201,11 +193,6 @@
     (validate-expression (current-system) name vars expr)
     (next-method)))
 
-(define (debug f . args)
-  (if #f
-      (apply format #t f args)
-      #t))
-
 (define-syntax-rule (define/guard (name (var p?) ...) b b* ...)
   (define (name var ...)
     (unless (p? var)
@@ -367,7 +354,6 @@
   ((list-of binding?) x))
 
 (define/guard (substitute (env env?) (expr (const #t)))
-  (debug "substitute: ~s ~s~%" env expr)
   (cond ((expr-quoted? expr) expr)
         ((pair? expr)
          (cons (substitute env (car expr))
@@ -404,7 +390,6 @@
   (define (mat-begin lhs expr env)
     (reset (mat lhs expr env)))
   (define (mat lhs expr env)
-    (debug "lhs ~a, expr ~a, env ~a~%" lhs expr env)
     (cond ((expr-quoted? lhs)
            (if (expr-quoted? expr)
                (if (equal? lhs expr)
@@ -454,9 +439,6 @@
            (cond ((assoc expr env) => (const #t))
                  (else #f)))
           (else #t)))
-  (debug "rule: lhs: ~a rhs: ~a~%" (rule-lhs rl) (rule-rhs rl))
-  (debug "preconds: ~a~%" preconds)
-  (debug "expr: ~a~%" expr)
   (reset
    (shift k0
           (match (mat-preconds (rule-preconds rl) (cons k0 env))
@@ -852,7 +834,7 @@
               (theorem-rules thm)) => result/expr)
         (else
          (result/error 'apply-theorem cmd-name expr)))))))
-    
+
 (define (rewrite/induction sys fname vars expr fail)
   (cond
    ((lookup fname sys)
@@ -1139,31 +1121,31 @@
   (and (pair? x)
        (null? (cdr x))))
 
-(define (if/if x y z)
+(define (smart-if x y z)
   (cond
    ((equal? y z) y)
    ((equal? x ''#t) y)
    ((equal? x ''#f) z)
    (else `(if ,x ,y ,z))))
 
-(define (and/if . args)
+(define (smart-and . args)
   (cond
    ((null? args) ''#t)
-   ((equal? ''#t (car args)) (apply and/if (cdr args)))
+   ((equal? ''#t (car args)) (apply smart-and (cdr args)))
    (else
-    (let ((rest (apply and/if (cdr args))))
+    (let ((rest (apply smart-and (cdr args))))
       (if (equal? ''#t rest)
           (car args)
-          (if/if (car args)
-                 rest
-                 ''#f))))))
+          (smart-if (car args)
+                    rest
+                    ''#f))))))
 
-(define (implies/if x y)
+(define (smart-implies x y)
   (cond
    ((equal? ''#f x) ''#t)
    ((equal? ''#t y) ''#t)
    (else
-    (if/if x y ''#t))))
+    (smart-if x y ''#t))))
 
 (define (make-totality-claim* sys m-expr f)
   (unless (get-measure-predicate sys)
@@ -1191,36 +1173,36 @@
                     (get-name f)
                     m-expr
                     app-form))))
-    (if/if `(,(get-measure-predicate sys) ,m-expr)
-           (let loop ((expr (get-expression f)))
-             (cond
-              ((expr-quoted? expr) ''#t)
-              ((variable? expr) ''#t)
-              ((if-form? expr)
-               (let ((test/result (loop (if-form-test expr)))
-                     (then/result (loop (if-form-then expr)))
-                     (else/result (loop (if-form-else expr))))
-                 (and/if test/result
-                         (if/if (if-form-test expr)
-                                then/result
-                                else/result))))
-              ((app-form? expr)
-               (let ((rest
-                      (let f ((args (app-form-args expr)))
-                        (cond ((null? args) ''#t)
-                              ((single? args) (loop (car args)))
-                                  (else (and/if (loop (car args))
-                                                (f (cdr args))))))))
-                 (if (eq? name (app-form-name expr))
-                     (and/if `(,(get-measure-less-than sys)
-                               ,(convert expr)
-                                   ,m-expr)
-                                 rest)
-                     rest)))
-              (else (error "(vikalpa) make-totality-claim: error"
-                           (get-name f)
-                           m-expr))))
-           ''#f)))
+    (smart-if `(,(get-measure-predicate sys) ,m-expr)
+              (let loop ((expr (get-expression f)))
+                (cond
+                 ((expr-quoted? expr) ''#t)
+                 ((variable? expr) ''#t)
+                 ((if-form? expr)
+                  (let ((test/result (loop (if-form-test expr)))
+                        (then/result (loop (if-form-then expr)))
+                        (else/result (loop (if-form-else expr))))
+                    (smart-and test/result
+                               (smart-if (if-form-test expr)
+                                         then/result
+                                         else/result))))
+                 ((app-form? expr)
+                  (let ((rest
+                         (let f ((args (app-form-args expr)))
+                           (cond ((null? args) ''#t)
+                                 ((single? args) (loop (car args)))
+                                 (else (smart-and (loop (car args))
+                                                  (f (cdr args))))))))
+                    (if (eq? name (app-form-name expr))
+                        (smart-and `(,(get-measure-less-than sys)
+                                     ,(convert expr)
+                                     ,m-expr)
+                                   rest)
+                        rest)))
+                 (else (error "(vikalpa) make-totality-claim: error"
+                              (get-name f)
+                              m-expr))))
+              ''#f)))
 
 (define (make-guard-claim expr sys)
   (define (find-preconds expr)
@@ -1244,28 +1226,28 @@
   (define (build/find-if expr)
     (cond
      ((if-form? expr)
-      (if/if (build/find-if (if-form-test expr))
-             (build (if-form-then expr))
-             (build (if-form-else expr))))
+      (smart-if (build/find-if (if-form-test expr))
+                (build (if-form-then expr))
+                (build (if-form-else expr))))
      ((app-form? expr)
-      (apply and/if (map build/find-if (app-form-args expr))))
+      (apply smart-and (map build/find-if (app-form-args expr))))
      (else ''#t)))
   (define (build expr)
     (cond
      ((if-form? expr)
-      (apply and/if
+      (apply smart-and
              (append (find-preconds (if-form-test expr))
-                     (list (if/if (if-form-test expr)
-                                  (build (if-form-then expr))
-                                  (build (if-form-else expr)))))))
+                     (list (smart-if (if-form-test expr)
+                                     (build (if-form-then expr))
+                                     (build (if-form-else expr)))))))
      ((app-form? expr)
-      (apply and/if
+      (apply smart-and
              (append (find-preconds expr)
                      (list (build/find-if expr)))))
      (else ''#t)))
-  (if/if (build expr)
-         ''#t
-         ''#f))
+  (smart-if (build expr)
+            ''#t
+            ''#f))
 
 (define (make-induction-claim f vars c)
   (define (find-app-forms expr)
@@ -1298,15 +1280,15 @@
            (cond
             ((if-form? expr)
              (let ((app-forms (find-app-forms (if-form-test expr))))
-               (implies/if (if (null? app-forms)
-                               ''#t
-                               (fold implies/if c (map prop app-forms)))
-                           (if/if (if-form-test expr)
-                                  (build (if-form-then expr))
-                                  (build (if-form-else expr))))))
+               (smart-implies (if (null? app-forms)
+                                  ''#t
+                                  (fold smart-implies c (map prop app-forms)))
+                              (smart-if (if-form-test expr)
+                                        (build (if-form-then expr))
+                                        (build (if-form-else expr))))))
             (else
              (let ((app-forms (find-app-forms expr)))
-               (fold implies/if c (map prop app-forms))))))))
+               (fold smart-implies c (map prop app-forms))))))))
    (else (error "make-induction-claim: invalid"
                 f vars c))))
 
@@ -1346,10 +1328,10 @@
                                  (get-variables f)
                                  seed)
             (update-claim
-             (fold implies/if
-                   (and/if (make-totality-claim* sys seed f)
-                           (make-guard-claim (get-expression f)
-                                             sys))
+             (fold smart-implies
+                   (smart-and (make-totality-claim* sys seed f)
+                              (make-guard-claim (get-expression f)
+                                                sys))
                    (get-guards f))))
           (raise-exception
            (make-exception
@@ -1357,7 +1339,7 @@
             (make-exception-with-message "need measure expression")
             (make-exception-with-irritants (get-expression f)))))
       (update-claim
-       (fold implies/if
+       (fold smart-implies
              (make-guard-claim (get-expression f) sys)
              (get-guards f)))))
 
diff --git a/vikalpa/prelude.scm b/vikalpa/prelude.scm
index 74cbe98..d2e54ce 100644
--- a/vikalpa/prelude.scm
+++ b/vikalpa/prelude.scm
@@ -28,21 +28,6 @@
   (and (exact-integer? x)
        (negative? x)))
 
-(define (succ x)
-  (if (number? x)
-      (+ x 1)
-      1))
-
-(define (pred x)
-  (if (number? x)
-      (- x 1)
-      -1))
-
-(define (negate x)
-  (if (exact-integer? x)
-      (- x)
-      0))
-
 (define-syntax-rule (define-axiom/is p1 p2)
   (define-axiom (is p1 p2) (x) (is (p1 x) (p2 x))))