From d9e4ce77062f21659f82513bc4b4d281e6c6fb4b Mon Sep 17 00:00:00 2001
From: Masaya Tojo <masaya@tojo.tokyo>
Date: Sat, 7 Nov 2020 15:29:34 +0900
Subject: wip2

---
 rabbit-prover.scm | 105 +++++++++++++++++++++++++++---------------------------
 1 file changed, 52 insertions(+), 53 deletions(-)

(limited to 'rabbit-prover.scm')

diff --git a/rabbit-prover.scm b/rabbit-prover.scm
index 702ba07..b448eaf 100644
--- a/rabbit-prover.scm
+++ b/rabbit-prover.scm
@@ -19,7 +19,7 @@
 (define-module (rabbit-prover)
   #:export (rewrite)
   #:use-module (ice-9 match)
-  #:use-module ((srfi srfi-1) #:select (every any append-map))
+  #:use-module ((srfi srfi-1) #:select (every any append-map member))
   #:use-module (srfi srfi-8)
   #:use-module (srfi srfi-26))
 
@@ -129,49 +129,48 @@
   (define (var? v)
     (and (member v (rule-vars rl))
          #t))
-  (and (every (cut member <> preconds)
-              (rule-preconds rl))
-       (call/cc
-        (lambda (k)
-          (substitute (let mat ((lhs (rule-lhs rl))
-                                (expr 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)))
-                                   (let loop ((lhss (cdr lhs))
-                                              (exprs (cdr expr))
-                                              (env env))
-                                     (cond ((and (pair? lhss)
-                                                 (pair? exprs))
-                                            (loop (cdr lhss)
-                                                  (cdr exprs)
-                                                  (mat (car lhss)
-                                                       (car exprs)
-                                                       env)))
-                                           ((and (null? lhss)
-                                                 (null? exprs))
-                                            env)
-                                           (else (k #f))))
-                                   (k #f)))
-                              ((var? lhs)
-                               (cond
-                                ((assoc lhs env)
-                                 => (lambda (p)
-                                      (if (equal? (cdr p) expr)
-                                          env
-                                          (k #f))))
-                                (else
-                                 (cons (cons lhs expr)
-                                       env))))
-                              (else (k #f))))
-                      (rule-rhs rl))))))
+  (call/cc
+   (lambda (k)
+     (substitute (let mat ((lhs `(and ,@(rule-preconds rl) ,(rule-lhs rl)))
+                           (expr `(and ,@preconds ,expr))
+                           (env '()))
+                   (format #t "lhs: ~s, expr: ~s, env: ~s~%" 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)))
+                              (let loop ((lhss (cdr lhs))
+                                         (exprs (cdr expr))
+                                         (env env))
+                                (cond ((and (pair? lhss)
+                                            (pair? exprs))
+                                       (loop (cdr lhss)
+                                             (cdr exprs)
+                                             (mat (car lhss)
+                                                  (car exprs)
+                                                  env)))
+                                      ((and (null? lhss)
+                                            (null? exprs))
+                                       env)
+                                      (else (k #f))))
+                              (k #f)))
+                         ((var? lhs)
+                          (cond
+                           ((assoc lhs env)
+                            => (lambda (p)
+                                 (if (equal? (cdr p) expr)
+                                     env
+                                     (k #f))))
+                           (else
+                            (cons (cons lhs expr)
+                                  env))))
+                         (else (k #f))))
+                 (rule-rhs rl)))))
 
 ;; (substitute environment expression?) -> expression?
 (define (substitute env expr)
@@ -407,15 +406,6 @@
       (values expr '() identity)
       (let ((i (car path)))
         (cond
-         ((< i (length expr))
-          (receive (extracted-expr preconds builder)
-              (extract (cdr path) (list-ref expr i) fail)
-            (values extracted-expr
-                    preconds
-                    (lambda (x)
-                      (append (list-head expr i)
-                              (list (builder x))
-                              (list-tail expr (+ i 1)))))))
          ((expr-if? expr)
           (let ((precond (expr-if-cond expr)))
             (receive (extracted-expr extracted-preconds builder)
@@ -430,6 +420,15 @@
                         (append (list-head expr i)
                                 (list (builder x))
                                 (list-tail expr (+ i 1))))))))
+         ((< i (length expr))
+          (receive (extracted-expr preconds builder)
+              (extract (cdr path) (list-ref expr i) fail)
+            (values extracted-expr
+                    preconds
+                    (lambda (x)
+                      (append (list-head expr i)
+                              (list (builder x))
+                              (list-tail expr (+ i 1)))))))
          (else
           (fail "invalid path" path))))))
 
-- 
cgit v1.2.3