wip5

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)