wip65

1 files changed, 130 insertions, 98 deletions

diff --git a/vikalpa.scm b/vikalpa.scm
index dab81b2..a8217e5 100644
--- a/vikalpa.scm
+++ b/vikalpa.scm
@@ -660,53 +660,75 @@
                      '()
                      (get-expression x)))
 
-(define (error? x)
+(define (result? x)
+  (or (result/error? x)
+      (result/expr? x)))
+
+(define (result/error? x)
   (and (pair? x)
-       (eq? 'error (car x))))
+       (eq? 'result/error (car x))))
+
+(define (result/error . args)
+  (cons* 'result/error args))
+
+(define (result/expr? x)
+  (and (list? x)
+       (= 2 (length x))
+       (eq? 'result/expr (car x))
+       (expression? (cadr x))))
 
+(define (result/expr x)
+  (list 'result/expr x))
+
+(define/guard (result/expr-expr (x result/expr?))
+  (cadr x))
 
 (define (rewrite/eval expr sys)
-  (let eval ((expr expr))
+  (let eval ((result (result/expr expr)))
     (cond
-     ((error? expr) expr)
-     ((expr-quoted? expr) expr)
-     ((app-form? expr)
-      (let ((args (map eval (app-form-args expr)))
-            (name (app-form-name expr)))
-        (define (guard-ok? vars form g)
-          (let ((result (eval (apply-rule '()
-                                          (rule vars '() form g)
-                                          `(,name ,@args)
-                                          '()))))
-            (if (error? result)
-                result
-                (expr-unquote result))))
+     ((result/error? result) result)
+     ((result/expr? result)
+      (let ((expr (result/expr-expr result)))
         (cond
-         ((find error? args) => identity)
-         ((lookup name sys)
-          => (lambda (f)
-               (let ((gs (get-guards f))
-                     (vars (get-variables f))
-                     (form (defined-function-app-form f)))
-                 (if (every (lambda (g) (guard-ok? vars form g)) gs)
-                     (eval (rewrite1 sys
-                                     `(,name ,@args)
-                                     (lambda args
-                                       (cons* 'error 'rewrite name args))
-                                     `(rewrite () ,name)))
-                     `(error guard-error (,name ,@args) (and ,@gs))))))
-         (else `(error function not-found)))))
-     ((if-form? expr)
-      (let ((test (eval (if-form-test expr))))
-        (if (error? test)
-            test
-            (if (expr-unquote test)
-                (eval (if-form-then expr))
-                (eval (if-form-else expr))))))
-     ((variable? expr)
-      `(error eval variable-found ,expr))
-     (else
-      `(error eval invalid-expression ,expr)))))
+         ((expr-quoted? expr) (result/expr expr))
+         ((app-form? expr)
+          (let ((args/result (map (compose eval result/expr)
+                                  (app-form-args expr)))
+                (name (app-form-name expr)))
+            (cond
+             ((find error? args/result) => identity)
+             ((lookup name sys)
+              => (lambda (f)
+                   (let ((args (map result/expr-expr args/result))
+                         (gs (get-guards f))
+                         (vars (get-variables f))
+                         (form (defined-function-app-form f)))
+                     (define (guard-ok? vars form g)
+                       (let ((result (eval (apply-rule '()
+                                                       (rule vars '() form g)
+                                                       `(,name ,@args)
+                                                       '()))))
+                         (if (result/error? result)
+                             result
+                             (expr-unquote (result/expr-expr result)))))
+                     (if (every (lambda (g) (guard-ok? vars form g)) gs)
+                         (eval (rewrite1 sys
+                                         `(,name ,@args)
+                                         `(rewrite () ,name)))
+                         (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)
+                test/result
+                (if (expr-unquote (result/expr-expr test/result))
+                    (eval (if-form-then expr))
+                    (eval (if-form-else expr))))))
+         ((variable? expr)
+          (result/error 'eval 'variable-found expr))
+         (else
+          (result/error 'eval 'invalid-expression expr)))))
+     (else (result/error 'eval 'invalid-result result)))))
 
 (define (rewriter? x)
   (match x
@@ -818,76 +840,86 @@
           (else
            (fail 'invalid-option (car ops)))))))
 
-(define (rewrite/theorem cmd-name cmd-ops b thm preconds expr fail)
-  (receive (env)
-      (parse-options/theorem cmd-ops fail)
-    (cond
-     ((any (cut apply-rule preconds <> expr env)
-           (theorem-rules thm)) => identity)
-     (else
-      (fail 'apply-theorem cmd-name expr)))))
-
+(define (rewrite/theorem cmd-name cmd-ops b thm preconds expr)
+  (call/cc
+   (lambda (k)
+     (define (fail . args)
+       (k (apply result/error args)))
+     (receive (env)
+         (parse-options/theorem cmd-ops fail)
+       (cond
+        ((any (cut apply-rule preconds <> expr env)
+              (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)
     => (cut make-induction-claim <> vars expr))
    (else (fail 'induction 'not-found fname))))
 
-(define (rewrite/core-function sys f expr fail)
+(define (rewrite/core-function sys f expr)
   (if (and (app-form? expr)
            (eq? (get-name f) (app-form-name expr))
            (= (length (get-variables f)) (length (app-form-args expr)))
            (every expr-quoted? (app-form-args expr)))
-      (let ((result (apply (get-procedure f)
-                           (map expr-unquote (app-form-args expr)))))
-        (expr-quote result))
-      (fail 'apply-core-function (get-name f) expr)))
-
-(define (rewrite1 sys expr fail r)
-  (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))))))))
+      (result/expr
+       (expr-quote (apply (get-procedure f)
+                          (map expr-unquote (app-form-args expr)))))
+      (result/error 'apply-core-function (get-name f) expr)))
+
+(define (rewrite1 sys expr r)
+  (call/cc
+   (lambda (k)
+     (define (fail . args)
+       (k (apply result/error args)))
+     (match r
+       (('eval path)
+        (receive (extracted-expr preconds builder)
+            (extract path expr fail)
+          (builder
+           (let ((result (rewrite/eval extracted-expr sys)))
+             (if (result/error? result)
+                 (result/error 'eval 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))
+                   ((is-a? x <theorem*>)
+                    (rewrite/theorem command-name command-ops sys x preconds extracted-expr))
+                   ((is-a? x <expandable-function>)
+                    (cond
+                     ((any (cut apply-rule '() <> extracted-expr '())
+                           (function->rules x))
+                      => result/expr)
+                     (else
+                      (result/error 'apply-function command-name extracted-expr))))
+                   
+                   (else
+                    (result/error 'invalid-command command-name extracted-expr)))))
+            (else (result/error 'command-not-found command-name extracted-expr))))))))))
 
 (define (rewrite sys expr seq)
-  (let loop ((expr expr)
+  (let loop ((result (result/expr expr))
              (seq seq))
-    (reset
-     (if (null? seq)
-         expr
-         (loop (rewrite1 sys
-                         expr
-                         (lambda args
-                           (shift k (cons 'error args)))
-                         (car seq))
-               (cdr seq))))))
+    (cond
+     ((result/error? result) result)
+     ((result/expr? result)
+      (if (null? seq)
+          expr
+          (loop (rewrite1 sys
+                          (result/expr-expr result)
+                          (car seq))
+                (cdr seq))))
+     (else (result/error 'invalid-result result)))))
 
 (define (expr-not x)
   (list 'not x))