wip14

1 files changed, 95 insertions, 46 deletions

diff --git a/vikalpa.scm b/vikalpa.scm
index b8d1bee..6dadcd2 100644
--- a/vikalpa.scm
+++ b/vikalpa.scm
@@ -21,14 +21,15 @@
   #:use-module (vikalpa syntax)
   #:use-module (vikalpa primitive)
   #:use-module (ice-9 match)
+  #:use-module (ice-9 format)
   #:use-module ((srfi srfi-1) #:select (every any member))
   #:use-module (srfi srfi-8)
   #:use-module (srfi srfi-26))
 
 (define (debug f . args)
-  (if #f
+  (if #t
       (apply format #t f args)
-      (if #f #f)))
+      #t))
 
 (define (option p?)
   (lambda (x)
@@ -128,14 +129,25 @@
               (environment (cdr x))))
         (else #f)))
 
-(define (apply-rule preconds rl expr)
-  (call/cc (lambda (k) (apply-rule* preconds rl expr k))))
+(define (apply-rule preconds rl expr env)
+  (call/cc (lambda (k) (apply-rule* preconds rl expr env k))))
 
 ;; (apply-rule preconds rule? expression?) -> (or (cons rhs environment) #f)
-(define (apply-rule* preconds rl expr fail)
+(define (apply-rule* preconds rl expr env fail)
   (define (var? v)
     (and (member v (rule-vars rl))
          #t))
+  (define (add-env var expr env k)
+    (cond
+     ((assoc var env)
+      => (match-lambda
+           ((env-var . env-expr)
+            (if (equal? env-expr expr)
+                env
+                (k #f)))))
+     (else
+      (cons (cons var expr)
+            env))))
   (define (mat-map lhss exprs env k)
     (cond ((and (pair? lhss)
                 (pair? exprs))
@@ -163,17 +175,7 @@
                     (eqv? (car lhs) (car expr)))
                (mat-map (cdr lhs) (cdr expr) env k)
                (k #f)))
-          ((var? lhs)
-           (cond
-            ((assoc lhs env)
-             => (match-lambda
-                  ((env-var . env-expr)
-                   (if (equal? env-expr expr)
-                       env
-                       (k #f)))))
-            (else
-             (cons (cons lhs expr)
-                   env))))
+          ((var? lhs) (add-env lhs expr env k))
           (else (k #f))))
   (define (mat-preconds rlps env)
     (if (null? rlps)
@@ -198,7 +200,7 @@
   (debug "expr: ~a~%" expr)
   (substitute (mat (rule-lhs rl)
                    expr
-                   (mat-preconds (rule-preconds rl) '())
+                   (mat-preconds (rule-preconds rl) env)
                    fail)
               (rule-rhs rl)))
 
@@ -445,20 +447,18 @@
 
 ;; (rewriter path? command?) -> rewriter?
 (define (rewriter p c)
-  (list p c))
+  (cons p c))
 
 (define (rewriter-path r)
-  (list-ref r 0))
+  (car r))
 
 (define (rewriter-command r)
-  (list-ref r 1))
+  (cdr r))
 
 (define (rewriter? x)
   (and (pair? x)
        (path? (car x))
-       (pair? (cdr x))
-       (command? (car (cdr x)))
-       (null? (cdr (cdr x)))))
+       (command? (cdr x))))
 
 ;; (sequence? x) -> boolean?
 (define (sequence? x)
@@ -471,11 +471,33 @@
   (and (list? x)
        (every natural? x)))
 
-;; (command? x) -> booelan?
+;; (command-name? x) -> booelan?
 (define (command? x)
+  (and (pair? x)
+       (command-name? (car x))
+       ((list-of command-option?) (cdr x))))
+
+;; (command-name? x) -> booelan?
+(define (command-name? x)
   (or (symbol? x)
       ((list-of symbol?) x)))
 
+;; (command-option? x) -> boolean?
+(define (command-option? x)
+  (and (pair? x)
+       (case (car x)
+         ((set) (and (list? x)
+                     (= 3 (length x))
+                     (variable? (list-ref x 1))
+                     (expression? (list-ref x 2))))
+         (else #f))))
+
+(define (command-name x)
+  (car x))
+
+(define (command-options x)
+  (cdr x))
+
 ;; (extract path? expression? preconds? procedure?) -> (values expression? procedure?)
 (define (extract path expr fail)
   (if (null? path)
@@ -520,34 +542,56 @@
               (cons (function-name x)
                     (function-vars x)))))
 
+(define (parse-options/prop ops)
+  (if (null? ops)
+      (values '())
+      (receive (env)
+          (parse-options/prop (cdr ops))
+        (case (caar ops)
+          ((set) (let ((op (car ops)))
+                   (cons (cons (list-ref op 1)
+                               (list-ref op 2))
+                         env)))
+          (else
+           (error "invalid option:" (car ops)))))))
+
+(define (rewrite/prop cmd b prop preconds expr fail)
+  (receive (env)
+      (parse-options/prop (command-options cmd))
+    (cond
+     ((any (cut apply-rule preconds <> expr env)
+           (proposition-rules prop)) => identity)
+     (else
+      (fail (format #f "no match-rule (~a)" cmd))))))
+
 ;; (rewrite book? rewriter? expression? procedure?) -> expr
 (define (rewrite1 b expr fail r)
-  (let ((cmd (rewriter-command r)))
+  (let* ((cmd (rewriter-command r))
+         (cmd/name (command-name cmd)))
     (debug "~%~%cmd: ~a~%" cmd)
+    #;(format #t "~%~%cmd: ~a~%" cmd)
     (receive (extracted-expr preconds builder)
         (extract (rewriter-path r) expr fail)
       (builder
        (cond
-        ((equal? cmd '(expand))
+        ((equal? cmd/name '(look))
+         (format #t "~y" extracted-expr)
+         (error "look"))
+        ((equal? cmd/name '(expand))
          (expand (filter macro? b) extracted-expr))
-        ((equal? cmd '(expand*))
+        ((equal? cmd/name '(expand*))
          (expand* (filter macro? b) extracted-expr))
-        ((and (symbol? cmd)
-              (assoc cmd b))
+        ((and (symbol? cmd/name)
+              (assoc cmd/name b))
          => (lambda (x)
               (cond
-               ((proposition? x)
-                (cond
-                 ((any (cut apply-rule preconds <> extracted-expr)
-                       (proposition-rules x)) => identity)
-                 (else
-                  (fail (format #f "no match-rule (~a)" cmd)))))
+               ((proposition? x) (rewrite/prop cmd b x preconds extracted-expr fail))
                ((function? x)
                 (cond
-                 ((any (cut apply-rule '() <> extracted-expr)
+                 ((any (cut apply-rule '() <> extracted-expr '())
                        (function->rules x)) => identity)
                  (else
-                  (fail (format #f "no match-rule (~a)" cmd)))))
+                  (fail (format #f "no match-function (~a)" cmd)))))
                ((primitive-function? x)
                 (cond
                  ((match-primitive-function x extracted-expr)
@@ -567,6 +611,7 @@
   (let loop ((expr expr)
              (seq seq))
     (debug "~y~%" expr)
+    #;(format #t "~y~%" expr)
     (if (null? seq)
         expr
         (loop (rewrite1 b
@@ -699,36 +744,40 @@
     (equal? (atom? (cons x y)) '#f))
   (define-axiom car/cons (x y)
     (equal? (car (cons x y)) x))
+
   (define-axiom cdr/cons (x y)
     (equal? (cdr (cons x y)) y))
+
   (define-axiom cons/car+cdr (x)
     (if (atom? x)
         '#t
         (equal? (cons (car x) (cdr x)) x)))
 
-  ;; バグる
-  ;; (define-axiom if-nest (x y z)
-  ;;   (if x
-  ;;       (equal? (if x y z) y)
-  ;;       (equal? (if x y z) z)))
+  (define-axiom if-nest (x y z)
+    (if x
+        (equal? (if x y z) y)
+        (equal? (if x y z) z)))
 
-  (define-axiom if-false (x y)
-    (equal? (if '#f x y) y))
-    
   (define-axiom if-nest-t (x y z)
     (if x
         (equal? (if x y z) y)
         '#t))
+
   (define-axiom if-nest-f (x y z)
     (if x
         '#t
         (equal? (if x y z) z)))
+
+  (define-axiom if-false (x y)
+    (equal? (if '#f x y) y))
+    
   (define-axiom if-same (x y)
     (equal? (if x y y) y))
 
   (define-axiom natural/size (x)
     (equal? (natural? (size x))
             '#t))
+
   (define-axiom size/car (x)
     (if (atom? x)
         '#t
@@ -740,6 +789,7 @@
         '#t
         (equal? (< (size (cdr x)) (size x))
                 '#t)))
+
   (define-macro list ()
     ((list) '())
     ((list x . y) (cons x (list . y))))
@@ -804,7 +854,6 @@
              ((3 2) equal-same)
              ((3) if-same)
              (() if-same)))
-
   )
 
 (define (size x)