From 0719cc51cf761536153ffd2a0ac441305d994178 Mon Sep 17 00:00:00 2001 From: Masaya Tojo Date: Tue, 5 Jan 2021 08:58:20 +0900 Subject: wip65 --- vikalpa.scm | 228 ++++++++++++++++++++++++++++++++++-------------------------- 1 file 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 ) - (rewrite/core-function sys x extracted-expr fail)) - ((is-a? x ) - (rewrite/theorem command-name command-ops sys x preconds extracted-expr fail)) - ((is-a? x ) - (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 ) + (rewrite/core-function sys x extracted-expr)) + ((is-a? x ) + (rewrite/theorem command-name command-ops sys x preconds extracted-expr)) + ((is-a? x ) + (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)) -- cgit v1.2.3