From 025d51a54e3b1ed50caa48e3799d84270c5adf70 Mon Sep 17 00:00:00 2001
From: Masaya Tojo <masaya@tojo.tokyo>
Date: Tue, 24 Nov 2020 18:12:32 +0900
Subject: wip34

---
 examples/the-little-prover.scm |  5 +---
 vikalpa.scm                    | 55 ++++++++++++++++++++++++------------------
 vikalpa/the-little-prover.scm  |  1 -
 3 files changed, 32 insertions(+), 29 deletions(-)

diff --git a/examples/the-little-prover.scm b/examples/the-little-prover.scm
index 6a919a8..3d0329f 100644
--- a/examples/the-little-prover.scm
+++ b/examples/the-little-prover.scm
@@ -46,10 +46,7 @@
      ((3 2 1) list-length)
      ((3 2 1) if-nest-E)
      ((3) if-same (set x (natural? (succ '0))))
-     ((3 2 2) natural?/+
-      ;; ルール探索アルゴリズムにバグがある
-      (set x (succ '0))
-      (set y (list-length (cdr xs))))
+     ((3 2 2) natural?/+)
      ((3 2) if-same)
      ((3 1) natural?/1)
      ((3) if-true)
diff --git a/vikalpa.scm b/vikalpa.scm
index 5be2824..f45a571 100644
--- a/vikalpa.scm
+++ b/vikalpa.scm
@@ -204,18 +204,16 @@
 (define (rule-rhs r)
   (list-ref r 4))
 
-;; (environment x) -> boolean?
-;; environment is alist
-(define (environment x)
-  (cond ((null? x) #t)
-        ((pair? x)
-         (and (pair? (car x))
-              (variable? (car (car x)))
-              (expression? (cdr (car x)))
-              (environment (cdr x))))
-        (else #f)))
+(define (binding? x)
+  (and (pair? x)
+       (symbol? (car x))
+       (expression? (cdr x))))
+
+(define (env? x)
+  ((list-of binding?) x))
 
-(define (substitute env expr)
+(define/guard (substitute (env env?) (expr (const #t)))
+  (debug "substitute: ~s ~s~%" env expr)
   (cond ((expr-quoted? expr) expr)
         ((pair? expr)
          (cons (substitute env (car expr))
@@ -249,6 +247,8 @@
                           env)))
           ((and (null? lhss) (null? exprs)) env)
           (else (fail))))
+  (define (mat-begin lhs expr env)
+    (reset (mat lhs expr env)))
   (define (mat lhs expr env)
     (debug "lhs ~a, expr ~a, env ~a~%" lhs expr env)
     (cond ((expr-quoted? lhs)
@@ -277,14 +277,21 @@
   (define (mat-preconds rlps k+env)
     (if (null? rlps)
         k+env
-        (mat-preconds (cdr rlps)
-                      (any (lambda (p)
-                             (shift k
-                                    (cond
-                                     ((reset (mat (car rlps) p (cdr k+env)))
-                                      => (lambda (env) (k (cons k env))))
-                                     (else (k #f)))))
-                           preconds))))
+        (mat-preconds
+         (cdr rlps)
+         (let search ((ps preconds))
+           (when (equal? rl '(rule (x y) ((natural? y) (natural? x)) (quote #t) (natural? (+ x y))))
+             (format #t "search~% rl: ~s~% rlps: ~s~% ps: ~s~% env: ~s~%" rl rlps ps (cdr k+env)))
+           (if (null? ps)
+               ((car k+env) #f)
+               (let ((env (mat-begin (car rlps) (car ps) (cdr k+env))))
+                 (cond
+                  ((mat-begin (car rlps) (car ps) (cdr k+env))
+                   => (lambda (env)
+                        (shift k0
+                               (reset (or (shift k (k0 (cons k env)))
+                                          (k0 (search (cdr ps))))))))
+                  (else (search (cdr ps))))))))))
   (define (valid? env expr)
     (cond ((expr-quoted? expr) #t)
           ((pair? expr)
@@ -298,19 +305,19 @@
   (debug "preconds: ~a~%" preconds)
   (debug "expr: ~a~%" expr)
   (reset
-   (shift k
-          (match (mat-preconds (rule-preconds rl) (cons k env))
+   (shift k0
+          (match (mat-preconds (rule-preconds rl) (cons k0 env))
             ((k . env)
              (cond
-              ((reset (mat (rule-lhs rl) expr env))
+              ((mat-begin (rule-lhs rl) expr env)
                => (lambda (env)
                     (if (valid? env (rule-rhs rl))
                         env
-                        #f)))
+                        (k #f))))
               (else (k #f))))
             (else #f)))))
 
-;; (apply-rule preconds rule? expression?) -> (or (cons rhs environment) #f)
+;; (apply-rule preconds rule? expression?) -> (or (cons rhs env?) #f)
 (define (apply-rule preconds rl expr env)
   (cond
    ((match-rule preconds rl expr env)
diff --git a/vikalpa/the-little-prover.scm b/vikalpa/the-little-prover.scm
index fd71082..b892f7f 100644
--- a/vikalpa/the-little-prover.scm
+++ b/vikalpa/the-little-prover.scm
@@ -112,7 +112,6 @@
     (if (natural? x)
         (equal? (natural? (succ x)) #t)
         #t))
-  
 
   ;; Prelude
   (define-function list-induction (x)
-- 
cgit v1.2.3