wip13

1 files changed, 152 insertions, 83 deletions

diff --git a/vikalpa.scm b/vikalpa.scm
index e610b80..b8d1bee 100644
--- a/vikalpa.scm
+++ b/vikalpa.scm
@@ -25,6 +25,11 @@
   #:use-module (srfi srfi-8)
   #:use-module (srfi srfi-26))
 
+(define (debug f . args)
+  (if #f
+      (apply format #t f args)
+      (if #f #f)))
+
 (define (option p?)
   (lambda (x)
     (or (p? x) (not x))))
@@ -123,66 +128,79 @@
               (environment (cdr x))))
         (else #f)))
 
-;; (apply-rule preconds rule? expression?) -> (or (cons rhs environment) #f)
 (define (apply-rule preconds rl expr)
+  (call/cc (lambda (k) (apply-rule* preconds rl expr k))))
+
+;; (apply-rule preconds rule? expression?) -> (or (cons rhs environment) #f)
+(define (apply-rule* preconds rl expr fail)
   (define (var? v)
     (and (member v (rule-vars rl))
          #t))
-  (call/cc
-   (lambda (k)
-     (define (mat-map lhss exprs env)
-       (cond ((and (pair? lhss)
-                   (pair? exprs))
-              (mat-map (cdr lhss)
-                       (cdr exprs)
-                       (mat (car lhss)
-                            (car exprs)
-                            env)))
-             ((and (null? lhss)
-                   (null? exprs))
-              env)
-             (else (k #f))))
-     (define (mat lhs expr env)
-       (cond ((expr-quoted? lhs)
-              (if (expr-quoted? expr)
-                  (and (equal? lhs expr)
-                       env)
-                  (k #f)))
-             ((pair? lhs)
-              (if (and (pair? expr)
-                       (symbol? (car lhs))
-                       (eqv? (car lhs) (car expr)))
-                  (mat-map (cdr lhs) (cdr expr) env)
-                  (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))))
-             (else (k #f))))
-     (define (mat-preconds rlps env)
-       (if (null? rlps)
-           env
-           (mat-preconds (cdr rlps)
-                         (any (lambda (p) (mat (car rlps) p env))
-                              preconds))))
-     (define (substitute env expr)
-       (cond ((expr-quoted? expr) expr)
-             ((pair? expr)
-              (cons (substitute env (car expr))
-                    (substitute env (cdr expr))))
-             ((and (variable? expr) (assoc expr env)) => cdr)
-             (else expr)))
-     (substitute (mat (rule-lhs rl)
-                      expr
-                      (mat-preconds (rule-preconds rl) '()))
-                 (rule-rhs rl)))))
+  (define (mat-map lhss exprs env k)
+    (cond ((and (pair? lhss)
+                (pair? exprs))
+           (mat-map (cdr lhss)
+                    (cdr exprs)
+                    (mat (car lhss)
+                         (car exprs)
+                         env
+                         k)
+                    k))
+          ((and (null? lhss)
+                (null? exprs))
+           env)
+          (else (k #f))))
+  (define (mat lhs expr env k)
+    (debug "lhs ~a, expr ~a, env ~a~%" lhs expr env)
+    (cond ((expr-quoted? lhs)
+           (if (expr-quoted? expr)
+               (and (equal? lhs expr)
+                    env)
+               (k #f)))
+          ((pair? lhs)
+           (if (and (pair? expr)
+                    (symbol? (car lhs))
+                    (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))))
+          (else (k #f))))
+  (define (mat-preconds rlps env)
+    (if (null? rlps)
+        env
+        (mat-preconds (cdr rlps)
+                      (any (lambda (p)
+                             (call/cc (lambda (k)
+                                        (mat (car rlps) p env
+                                             (lambda (x) (k #f))))))
+                           preconds))))
+  (define (substitute env expr)
+    (cond ((expr-quoted? expr) expr)
+          ((pair? expr)
+           (cons (substitute env (car expr))
+                 (substitute env (cdr expr))))
+          ((var? expr)
+           (cond ((assoc expr env) => cdr)
+                 (else (fail #f))))
+          (else expr)))
+  (debug "rule: ~a~%" rl)
+  (debug "preconds: ~a~%" preconds)
+  (debug "expr: ~a~%" expr)
+  (substitute (mat (rule-lhs rl)
+                   expr
+                   (mat-preconds (rule-preconds rl) '())
+                   fail)
+              (rule-rhs rl)))
 
 ;; (book? x) -> boolean?
 ;; book is alist
@@ -505,6 +523,7 @@
 ;; (rewrite book? rewriter? expression? procedure?) -> expr
 (define (rewrite1 b expr fail r)
   (let ((cmd (rewriter-command r)))
+    (debug "~%~%cmd: ~a~%" cmd)
     (receive (extracted-expr preconds builder)
         (extract (rewriter-path r) expr fail)
       (builder
@@ -547,6 +566,7 @@
 (define/guard (rewrite (b book?) (expr expression?) (seq sequence?))
   (let loop ((expr expr)
              (seq seq))
+    (debug "~y~%" expr)
     (if (null? seq)
         expr
         (loop (rewrite1 b
@@ -662,41 +682,64 @@
            (error "define-book: error"))
          (current-book))))))
 
+(define (atom? x)
+  (not (pair? x)))
+
 (define-book prelude ()
   (define-axiom equal-same (x)
     (equal? (equal? x x) '#t))
+
   (define-axiom equal-swap (x y)
     (equal? (equal? x y) (equal? y x)))
+
   (define-axiom equal-if (x y)
     (if (equal? x y) (equal? x y) '#t))
-  (define-axiom pair/cons (x y)
-    (equal? (pair? (cons x y)) '#t))
+
+  (define-axiom atom/cons (x y)
+    (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 y)
-    (equal? (if (pair? x)
-                (equal? (cons (car x) (cdr y)) x)
-                '#t)
-            y))
-  (define-axiom cons/car+cdr (x y)
-    (equal? (if (pair? x)
-                (equal? (cons (car x) (cdr y)) x)
-                '#t)
-            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-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-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 (pair? x)
-        (equal? (< (size x) (size (car x)))
-                '#t)
-        '#t))
+    (if (atom? x)
+        '#t
+        (equal? (< (size (car x)) (size x))
+                '#t)))
+
   (define-axiom size/cdr (x)
-    (if (pair? x)
-        (equal? (< (size x) (size (cdr x)))
-                '#t)
-        '#t))
+    (if (atom? x)
+        '#t
+        (equal? (< (size (cdr x)) (size x))
+                '#t)))
   (define-macro list ()
     ((list) '())
     ((list x . y) (cons x (list . y))))
@@ -715,8 +758,6 @@
     ((or) '#f)
     ((or x) x)
     ((or x . xs) (if x x (or . xs))))
-  (define-macro atom? ()
-    ((atom? x) (not (pair? x))))
   (define-axiom if-not (x y z)
     (equal? (if (not x)
                 y
@@ -725,7 +766,7 @@
                 z
                 y))))
 
-(define-book app (prelude)
+(define-book app/book (prelude)
   (define-function app (x y)
     (if (atom? x)
         y
@@ -733,7 +774,38 @@
 
   (define-theorem associate-app (x y z)
     (equal? (app (app x y) z)
-            (app x (app y z)))))
+            (app x (app y z))))
+
+  #;
+  (rewrite (app/book)
+           '(if (atom? a)
+                (equal? (app (app a b) c)
+                        (app a (app b c)))
+                (if (equal? (app (app (cdr a) b) c)
+                            (app (cdr a) (app b c)))
+                    (equal? (app (app a b) c)
+                            (app a (app b c)))
+                    '#t))
+           '(((2 2) app)
+             ((2 2) if-nest-t)
+             ((2 1 1) app)
+             ((2 1 1) if-nest-t)
+             ((2) equal-same)
+             ((3 2 1 1) app)
+             ((3 2 1 1) if-nest-f)
+             ((3 2 2) app)
+             ((3 2 2) if-nest-f)
+             ((3 2 2 2) equal-if)
+             ((3 2 1) app)
+             ((3 2 1 3 1) car/cons)
+             ((3 2 1 3 2 1) cdr/cons)
+             ((3 2 1 1) atom/cons)
+             ((3 2 1) if-false)
+             ((3 2) equal-same)
+             ((3) if-same)
+             (() if-same)))
+
+  )
 
 (define (size x)
   (if (pair? x)
@@ -742,9 +814,6 @@
          (size (cdr x)))
       0))
 
-(define (atom? x)
-  (not (pair? x)))
-
 (define (app x y)
     (if (atom? x)
         y