diff options
Diffstat (limited to 'rabbit-prover.scm')
-rw-r--r-- | rabbit-prover.scm | 79 |
1 files changed, 50 insertions, 29 deletions
diff --git a/rabbit-prover.scm b/rabbit-prover.scm index f84287a..2a12698 100644 --- a/rabbit-prover.scm +++ b/rabbit-prover.scm @@ -29,6 +29,11 @@ (lambda (x) (or (p? x) (not x)))) +(define (list-of p?) + (lambda (x) + (and (list? x) + (every p? x)))) + ;; (expression? x) -> boolean? (define (expression? expr) (cond ((expr-quoted? expr) @@ -338,19 +343,21 @@ (eq? (macro-name m) (car expr))) (let loop ((rs (macro-rules m))) (cond ((null? rs) expr) - ((apply-mrule (car rs) expr) => - (cut apply-macro m <>)) + ((apply-mrule (car rs) expr) => identity) (else (loop (cdr rs)))))) - (else expr))) + (else #f))) -(define (expand ms expr) +(define/guard (expand (ms (list-of macro?)) (expr (const #t))) (let loop ((ms ms) (expr expr)) (cond ((null? ms) expr) - (else (expand (cdr ms) (apply-macro (car ms) expr)))))) + (else (expand (cdr ms) + (cond + ((apply-macro (car ms) expr) => identity) + (else expr))))))) -(define (expand* ms expr) +(define/guard (expand* (ms (list-of macro?)) (expr (const #t))) (let loop ((ms ms) (expr expr)) (let ((new-expr (expand ms expr))) @@ -438,7 +445,8 @@ (list-ref r 1)) (define (rewriter? x) - (and (path? (car x)) + (and (pair? x) + (path? (car x)) (pair? (cdr x)) (command? (car (cdr x))) (null? (cdr (cdr x))))) @@ -456,7 +464,8 @@ ;; (command? x) -> booelan? (define (command? x) - (symbol? x)) + (or (symbol? x) + ((list-of symbol?) x))) ;; (extract path? expression? preconds? procedure?) -> (values expression? procedure?) (define (extract path expr fail) @@ -497,26 +506,34 @@ (extract (rewriter-path r) expr fail) (builder (cond - ((assoc cmd b) => - (lambda (x) - (cond - ((proposition? x) - (let ((rls (proposition-rules x))) - (cond - ((any (cut apply-rule preconds <> extracted-expr) - rls) => identity) - (else - (fail (format #f "no match-rule (~a)" cmd)))))) - ((primitive-function? x) - (cond - ((match-primitive-function x extracted-expr) - (apply-primitive-function x extracted-expr)) - (else - (fail "can't apply-primitive-function (~a)" cmd)))) - ((macro? x) - (fail "macro は だめ")) - (else - (fail "rewrite error"))))) + ((equal? cmd '(expand)) + (expand (filter macro? b) extracted-expr)) + ((equal? cmd '(expand*)) + (expand* (filter macro? b) extracted-expr)) + ((and (symbol? cmd) + (assoc cmd b)) + => (lambda (x) + (cond + ((proposition? x) + (let ((rls (proposition-rules x))) + (cond + ((any (cut apply-rule preconds <> extracted-expr) + rls) => identity) + (else + (fail (format #f "no match-rule (~a)" cmd)))))) + ((primitive-function? x) + (cond + ((match-primitive-function x extracted-expr) + (apply-primitive-function x extracted-expr)) + (else + (fail "can't apply-primitive-function (~a)" cmd)))) + ((macro? x) + (cond + ((apply-macro x extracted-expr) => identity) + (else + (fail "macro fail")))) + (else + (fail "rewrite error"))))) (else (fail "no cmd (~a)" cmd))))))) (define/guard (rewrite (b book?) (expr expression?) (seq sequence?)) @@ -625,7 +642,11 @@ (if (pair? x) (equal? (< (size x) (size (cdr x))) '#t) - '#t)))) + '#t)) + (macro 'list + (list (mrule '() '(list) ''()) + (mrule '(x y) '(list x . y) + '(cons x (list . y))))))) (define (size x) (if (pair? x) |