From 5e86af3f7845f2c0b10b1f7b788b8c38255d42fd Mon Sep 17 00:00:00 2001
From: Masaya Tojo <masaya@tojo.tokyo>
Date: Sat, 7 Nov 2020 16:00:36 +0900
Subject: wip3

---
 rabbit-prover.scm | 94 ++++++++++++++++++++++++++++++++-----------------------
 1 file changed, 54 insertions(+), 40 deletions(-)

(limited to 'rabbit-prover.scm')

diff --git a/rabbit-prover.scm b/rabbit-prover.scm
index b448eaf..8c594a8 100644
--- a/rabbit-prover.scm
+++ b/rabbit-prover.scm
@@ -131,45 +131,52 @@
          #t))
   (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))))
+     (define (mat lhs 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))))
+     (define (apply-preconds rlps env)
+       (if (null? rlps)
+           env
+           (apply-preconds (cdr rlps)
+                           (any (lambda (p) (mat (car rlps) p env))
+                                preconds))))
+     (substitute (mat (rule-lhs rl)
+                      expr
+                      (apply-preconds (rule-preconds rl) '()))
                  (rule-rhs rl)))))
 
 ;; (substitute environment expression?) -> expression?
@@ -550,4 +557,11 @@
           (equal? (if (pair? x)
                       (equal? (cons (car x) (cdr y)) x)
                       '#t)
-                  y))))
+                  y))
+        (define-axiom cons/car+cdr (x y)
+          (equal? (if (pair? x)
+                      (equal? (cons (car x) (cdr y)) x)
+                      '#t)
+                  y))
+        (define-axiom if-same (x y)
+          (equal? (if x y y) y))))
-- 
cgit v1.2.3