diff options
| -rw-r--r-- | vikalpa.scm | 55 |
1 files 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)))))) |