wip63

2 files changed, 88 insertions, 97 deletions

diff --git a/vikalpa.scm b/vikalpa.scm
index d1da85b..78b751a 100644
--- a/vikalpa.scm
+++ b/vikalpa.scm
@@ -121,9 +121,9 @@
 (define-method (write (d <total-function>) port)
   (write-definition 'total-function d port))
 
-(define-method (lookup (name <symbol>) (s <system>))
+(define-method (lookup name (s <system>))
   (find (lambda (x)
-          (eq? name (get-name x)))
+          (equal? name (get-name x)))
         (get-definitions s)))
 
 (define-method (update-measure-predicate (s <symbol>) (sys <system>))
@@ -185,7 +185,7 @@
 (define-method (validate (d <definition>))
   (let* ((vars (get-variables d))
          (name (get-name d)))
-    (validate-vars (symbol->string name) vars)))
+    (validate-vars (format #f "~a" name) vars)))
 
 (define-method (validate (d <expandable-function>))
   (let* ((vars (get-variables d))
@@ -683,7 +683,7 @@
                           `(,name ,@args)
                           (lambda args
                             (cons* 'error 'rewrite name args))
-                          (rewriter '() `(,name))))))))
+                          `(rewrite () ,name)))))))
      ((if-form? expr)
       (let ((test (eval (if-form-test expr))))
         (if (error? test)
@@ -696,20 +696,14 @@
      (else
       `(error eval invalid-expression ,expr)))))
 
-;; (rewriter path? command?) -> rewriter?
-(define (rewriter p c)
-  (cons p c))
-
-(define (rewriter-path r)
-  (car r))
-
-(define (rewriter-command r)
-  (cdr r))
-
 (define (rewriter? x)
-  (and (pair? x)
-       (path? (car x))
-       (command? (cdr x))))
+  (match x
+    (('rewrite path command-name command-ops ...)
+     (and (path? path)
+          (command-name? command-name)
+          (every command-option? command-ops)))
+    (('eval path) (path? path))
+    (else #f)))
 
 ;; (sequence? x) -> boolean?
 (define (sequence? x)
@@ -723,15 +717,7 @@
        (every natural? x)))
 
 ;; (command-name? x) -> booelan?
-(define (command? x)
-  (and (pair? x)
-       (command-name? (car x))
-       ((list-of command-option?) (cdr x))))
-
-;; (command-name? x) -> booelan?
-(define (command-name? x)
-  (or (symbol? x)
-      ((list-of symbol?) x)))
+(define (command-name? x) #t)
 
 ;; (command-option? x) -> boolean?
 (define (command-option? x)
@@ -820,14 +806,14 @@
           (else
            (fail 'invalid-option (car ops)))))))
 
-(define (rewrite/theorem cmd b thm preconds expr fail)
+(define (rewrite/theorem cmd-name cmd-ops b thm preconds expr fail)
   (receive (env)
-      (parse-options/theorem (command-options cmd) fail)
+      (parse-options/theorem cmd-ops fail)
     (cond
      ((any (cut apply-rule preconds <> expr env)
            (theorem-rules thm)) => identity)
      (else
-      (fail 'apply-theorem cmd expr)))))
+      (fail 'apply-theorem cmd-name expr)))))
 
 (define (rewrite/induction sys fname vars expr fail)
   (cond
@@ -846,36 +832,37 @@
       (fail 'apply-core-function (get-name f) expr)))
 
 (define (rewrite1 sys expr fail r)
-  (let* ((cmd (rewriter-command r))
-         (cmd/name (command-name cmd)))
-    (debug "~%~%cmd: ~a~%" cmd)
-    (receive (extracted-expr preconds builder)
-        (extract (rewriter-path r) expr fail)
-      (builder
-       (cond
-        ((equal? '(eval) cmd/name)
-         (let ((result (rewrite/eval extracted-expr sys)))
-           (if (error? result)
-               (fail 'eval (cddr result) extracted-expr)
-               result)))
-        ((and (symbol? cmd/name)
-              (lookup cmd/name sys))
-         => (lambda (x)
-              (cond
-               ((is-a? x <core-function>)
-                (rewrite/core-function sys x extracted-expr fail))
-               ((is-a? x <theorem*>)
-                (rewrite/theorem cmd sys x preconds extracted-expr fail))
-               ((is-a? x <expandable-function>)
-                (cond
-                 ((any (cut apply-rule '() <> extracted-expr '())
-                       (function->rules x))
-                  => identity)
-                 (else
-                  (fail 'apply-function cmd extracted-expr))))
-               (else
-                (fail 'invalid-command cmd extracted-expr)))))
-        (else (fail 'command-not-found cmd extracted-expr)))))))
+  (match r
+    (('eval path)
+     (receive (extracted-expr preconds builder)
+         (extract path expr fail)
+       (builder
+        (let ((result (rewrite/eval extracted-expr sys)))
+          (if (error? result)
+              (fail 'eval (cddr result) extracted-expr)
+              result)))))
+    (('rewrite path command-name command-ops ...)
+     (receive (extracted-expr preconds builder)
+         (extract path expr fail)
+       (builder
+        (cond
+         ((lookup command-name sys)
+          => (lambda (x)
+               (cond
+                ((is-a? x <core-function>)
+                 (rewrite/core-function sys x extracted-expr fail))
+                ((is-a? x <theorem*>)
+                 (rewrite/theorem command-name command-ops sys x preconds extracted-expr fail))
+                ((is-a? x <expandable-function>)
+                 (cond
+                  ((any (cut apply-rule '() <> extracted-expr '())
+                        (function->rules x))
+                   => identity)
+                  (else
+                   (fail 'apply-function command-name extracted-expr))))
+                (else
+                 (fail 'invalid-command command-name extracted-expr)))))
+         (else (fail 'command-not-found command-name extracted-expr))))))))
 
 (define (rewrite sys expr seq)
   (let loop ((expr expr)
@@ -1276,15 +1263,18 @@
 
 (define (validate-sequence sys d seq)
   (for-each (lambda (r)
-              (for-each (lambda (x)
-                          (match x
-                            (('set var expr)
-                             (validate-expression sys
-                                                  `(define-proof ,(get-name d))
-                                                  (get-variables d)
-                                                  expr))
-                            (else #f)))
-                        (rewriter-command r)))
+              (match r
+                (('rewrite _ _ . command-ops)
+                 (for-each (lambda (x)
+                             (match x
+                               (('set var expr)
+                                (validate-expression sys
+                                                     `(define-proof ,(get-name d))
+                                                     (get-variables d)
+                                                     expr))
+                               (else #f)))
+                           command-ops))
+                (else #f)))
             seq))
 
 (define (add-proof/function sys f seed seq)
@@ -1309,8 +1299,8 @@
             (update-claim
              (fold implies/if
                    (and/if (make-totality-claim* sys seed f)
-                            (make-guard-claim (get-expression f)
-                                              sys))
+                           (make-guard-claim (get-expression f)
+                                             sys))
                    (get-guards f))))
           (raise-exception
            (make-exception
@@ -1543,7 +1533,7 @@
 (define (system? x)
   (is-a? x <system>))
 
-(define/guard (system-lookup (sys system?) (name symbol?))
+(define/guard (system-lookup (sys system?) (name (const #t)))
   (cond
    ((lookup name sys) => show)
    (else #f)))
diff --git a/vikalpa/prelude.scm b/vikalpa/prelude.scm
index 176983c..201e93d 100644
--- a/vikalpa/prelude.scm
+++ b/vikalpa/prelude.scm
@@ -163,34 +163,35 @@
 
 (define-system prelude (prelude/measure/natural)
   (define-proof inexact?
-    (((2) if-nest)
-     (() if-same)))
+    ((rewrite (2) if-nest)
+     (rewrite () if-same)))
   (define-proof inexact-predicate
-    (((1) inexact?)
-     (() if-not)
-     ((3 1) inexact?)
-     ((3 1 1) equal-if-false)
-     ((3) (eval))
-     (() if-same)))
+    ((rewrite (1) inexact?)
+     (rewrite () if-not)
+     (rewrite (3 1) inexact?)
+     (rewrite (3 1 1) equal-if-false)
+     (eval (3))
+     (rewrite () if-same)))
   (define-proof positive?
-    (((2 1 1) (eval))
-     ((2 1) if-true)
-     ((2) if-nest)
-     (() if-same)))
+    ((eval (2 1 1))
+     (rewrite (2 1) if-true)
+     (rewrite (2) if-nest)
+     (rewrite () if-same)))
   (define-proof positive-predicate
-    (((1) positive?)
-     ((2 1) positive?)
-     ((2 1) less-than-predicate)
-     ((2) (eval))
-     (() if-same)))
+    ((rewrite (1) positive?)
+     (rewrite (2 1) positive?)
+     (rewrite (2 1) less-than-predicate)
+     (eval (2))
+     (rewrite () if-same)))
   (define-proof negative?
-    (((2 1) if-nest)
-     ((2 1) (eval))
-     ((2) if-true)
-     (() if-same)))
+    ((rewrite (2 1) if-nest)
+     (eval (2 1))
+     (rewrite (2) if-true)
+     (rewrite () if-same)))
   (define-proof negative-predicate
-    (((1) negative?)
-     ((2 1) negative?)
-     ((2 1) less-than-predicate)
-     ((2) (eval))
-     (() if-same))))
+    ((rewrite (1) negative?)
+     (rewrite (2 1) negative?)
+     (rewrite (2 1) less-than-predicate)
+     (eval (2))
+     (rewrite () if-same))))
+