From 2935ac95403858c8a8b4af696ea6ba5e7aef5e92 Mon Sep 17 00:00:00 2001
From: Masaya Tojo <masaya@tojo.tokyo>
Date: Tue, 5 Jan 2021 09:10:17 +0900
Subject: wip66

---
 vikalpa.scm | 55 ++++++++++++++++++++++++++++++-------------------------
 1 file changed, 30 insertions(+), 25 deletions(-)

diff --git a/vikalpa.scm b/vikalpa.scm
index a8217e5..1061a6e 100644
--- a/vikalpa.scm
+++ b/vikalpa.scm
@@ -874,38 +874,43 @@
    (lambda (k)
      (define (fail . args)
        (k (apply result/error args)))
+     (define (result->expr x)
+       (cond
+        ((result/error? x) (fail (cdr x)))
+        (else
+         (result/expr-expr x))))
      (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)))))
+          (result/expr
+           (builder
+            (result->expr (rewrite/eval extracted-expr sys))))))
        (('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>)
+          (result/expr
+           (builder
+            (result->expr
+             (cond
+              ((lookup command-name sys)
+               => (lambda (x)
                     (cond
-                     ((any (cut apply-rule '() <> extracted-expr '())
-                           (function->rules x))
-                      => result/expr)
+                     ((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 '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))))))))))
+                      (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 ((result (result/expr expr))
@@ -914,7 +919,7 @@
      ((result/error? result) result)
      ((result/expr? result)
       (if (null? seq)
-          expr
+          result
           (loop (rewrite1 sys
                           (result/expr-expr result)
                           (car seq))
@@ -1566,7 +1571,7 @@
                                 (get-claim d)
                                 (get-proof d)))))
               (cond
-               ((equal? result ''#t)
+               ((equal? result (result/expr ''#t))
                 (next))
                (else
                 (next (list (get-name d) result))))))
-- 
cgit v1.2.3