wip4

4 files changed, 266 insertions, 63 deletions

diff --git a/rabbit-prover.scm b/rabbit-prover.scm
index 8c594a8..f84287a 100644
--- a/rabbit-prover.scm
+++ b/rabbit-prover.scm
@@ -18,8 +18,10 @@
 
 (define-module (rabbit-prover)
   #:export (rewrite)
+  #:use-module (rabbit-prover syntax)
+  #:use-module (rabbit-prover primitive)
   #:use-module (ice-9 match)
-  #:use-module ((srfi srfi-1) #:select (every any append-map member))
+  #:use-module ((srfi srfi-1) #:select (every any member))
   #:use-module (srfi srfi-8)
   #:use-module (srfi srfi-26))
 
@@ -27,17 +29,6 @@
   (lambda (x)
     (or (p? x) (not x))))
 
-(define-syntax-rule (define/assert (name (var pred?) ...) b b* ...)
-  (define (name var ...)
-    (unless (pred? var)
-      (error (format #f
-                     "~a:~%  expected:  ~a~%  given: "
-                     'name
-                     'pred?)
-             var))
-    ...
-    b b* ...))
-
 ;; (expression? x) -> boolean?
 (define (expression? expr)
   (cond ((expr-quoted? expr)
@@ -66,11 +57,6 @@
 (define (expr-quote expr)
   (list 'quote expr))
 
-;; (natural? x) -> boolean?
-(define (natural? x)
-  (and (integer? x)
-       (not (negative? x))))
-
 ;; (variable? x) -> boolean?
 (define (variable? x)
   (symbol? x))
@@ -131,8 +117,19 @@
          #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)
-       (format #t "lhs: ~s, expr: ~s, env: ~s~%" lhs expr env)
        (cond ((expr-quoted? lhs)
               (if (expr-quoted? expr)
                   (and (equal? lhs expr)
@@ -142,52 +139,38 @@
               (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))))
+                  (mat-map (cdr lhs) (cdr expr) env)
                   (k #f)))
              ((var? lhs)
               (cond
                ((assoc lhs env)
-                => (lambda (p)
-                     (if (equal? (cdr p) expr)
-                         env
-                         (k #f))))
+                => (match-lambda
+                     ((env-var . env-expr)
+                      (if (equal? env-expr expr)
+                          env
+                          (k #f)))))
                (else
                 (cons (cons lhs expr)
                       env))))
              (else (k #f))))
-     (define (apply-preconds rlps env)
+     (define (mat-preconds rlps env)
        (if (null? rlps)
            env
-           (apply-preconds (cdr rlps)
-                           (any (lambda (p) (mat (car rlps) p env))
-                                preconds))))
+           (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
-                      (apply-preconds (rule-preconds rl) '()))
+                      (mat-preconds (rule-preconds rl) '()))
                  (rule-rhs rl)))))
 
-;; (substitute environment expression?) -> expression?
-(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)))
-
 ;; (book? x) -> boolean?
 ;; book is alist
 (define (book? x)
@@ -248,7 +231,7 @@
        ((option proof?) (list-ref x 4))))
 
 ;; (function variable? vars? expression? (option proof?)) -> function?
-(define/assert (function (name variable?) (vars vars?) (expr expression?) (proof (option proof)))
+(define/guard (function (name variable?) (vars vars?) (expr expression?) (proof (option proof)))
   (list name 'function vars expr proof))
 
 (define (function-name f)
@@ -263,30 +246,99 @@
 (define (function-proof f)
   (list-ref f 4))
 
+(define (mrule? x)
+  (and (list? x)
+       (= 4 (length x))
+       (eq? 'mrule (list-ref x 0))
+       (vars? (mrule-vars x))
+       ((const #t) (mrule-lhs x))
+       ((const #t) (mrule-rhs x))))
+
+(define (mrule vars lhs rhs)
+  (list 'mrule vars lhs rhs))
+
+(define (mrule-vars mrl)
+  (list-ref mrl 1))
+
+(define (mrule-lhs mrl)
+  (list-ref mrl 2))
+
+(define (mrule-rhs mrl)
+  (list-ref mrl 3))
+
 (define (macro? x)
   (and (list? x)
        (= 3 (length x))
-       (variable? (list-ref x 0))
        (eq? 'macro (list-ref x 1))
-       (let ((rs (list-ref x 2)))
-         (and (list? rs)
-              (every rule? rs)))))
+       (variable? (macro-name x))
+       (let ((mrls (macro-mrules x)))
+         (and (list? mrls)
+              (every mrule? mrls)))))
 
 (define (macro-name m)
   (list-ref m 0))
 
-(define (macro-rules m)
+(define (macro-mrules m)
   (list-ref m 2))
 
 (define (macro name rules)
-  (list 'macro name rules))
+  (list name 'macro rules))
+
+(define (apply-mrule rl expr)
+  (define (var? v)
+    (and (member v (mrule-vars rl))
+         #t))
+  (call/cc
+   (lambda (k)
+     (define (mat-map lhs-tree expr-tree env)
+       (cond ((and (pair? lhs-tree)
+                   (pair? expr-tree))
+              (mat-map (car lhs-tree)
+                       (car expr-tree)
+                       (mat-map (cdr lhs-tree)
+                                (cdr expr-tree)
+                                env)))
+             (else (mat lhs-tree expr-tree env))))
+     (define (mat lhs expr env)
+       (cond ((expr-quoted? lhs)
+              (if (expr-quoted? expr)
+                  (and (equal? lhs expr)
+                       env)
+                  (k #f)))
+             ((and (pair? lhs)
+                   (pair? expr))
+              (mat-map lhs expr env))
+             ((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))))
+             ((eqv? lhs expr) env)
+             (else (k #f))))
+     (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 (mrule-lhs rl)
+                      expr
+                      '())
+                 (mrule-rhs rl)))))
 
 (define (apply-macro m expr)
   (cond ((and (pair? expr)
               (eq? (macro-name m) (car expr)))
          (let loop ((rs (macro-rules m)))
            (cond ((null? rs) expr)
-                 ((apply-rule '() (car rs) expr) =>
+                 ((apply-mrule (car rs) expr) =>
                   (cut apply-macro m <>))
                  (else (loop (cdr rs))))))
         (else expr)))
@@ -311,7 +363,7 @@
 
 ;; (axiom variable? vars? expression?) -> axiom?
 ;; axiom? is proposition
-(define/assert (axiom (name variable?) (vars vars?) (expr expression?))
+(define/guard (axiom (name variable?) (vars vars?) (expr expression?))
   (list name 'axiom vars expr))
 
 (define (vars? x)
@@ -328,7 +380,7 @@
        (expression? (list-ref x 3))))
 
 ;; (theorem name vars? expression? proof?) -> theorem?
-(define/assert (theorem (name variable?) (vars vars?) (expr expression?) (p (option proof?)))
+(define/guard (theorem (name variable?) (vars vars?) (expr expression?) (p (option proof?)))
   (list name 'theorem vars expr p))
 
 ;; (theorem? x) -> boolean?
@@ -355,7 +407,6 @@
 (define (proposition? x)
   (or (axiom? x)
       (theorem? x)
-      (conjecture? x)
       (function? x)))
 
 (define (proposition-vars x)
@@ -468,7 +519,7 @@
              (fail "rewrite error")))))
         (else (fail "no cmd (~a)" cmd)))))))
 
-(define/assert (rewrite (b book?) (expr expression?) (seq sequence?))
+(define/guard (rewrite (b book?) (expr expression?) (seq sequence?))
   (let loop ((expr expr)
              (seq seq))
     (if (null? seq)
@@ -564,4 +615,21 @@
                       '#t)
                   y))
         (define-axiom if-same (x y)
-          (equal? (if x y y) y))))
+          (equal? (if x y y) y))
+        (define-axiom size/car (x)
+          (if (pair? x)
+              (equal? (< (size x) (size (car x)))
+                      '#t)
+              '#t))
+        (define-axiom size/cdr (x)
+          (if (pair? x)
+              (equal? (< (size x) (size (cdr x)))
+                      '#t)
+              '#t))))
+
+(define (size x)
+  (if (pair? x)
+      (+ 1
+         (size (car x))
+         (size (cdr x)))
+      0))
diff --git a/rabbit-prover/ord.scm b/rabbit-prover/ord.scm
new file mode 100644
index 0000000..c752d36
--- /dev/null
+++ b/rabbit-prover/ord.scm
@@ -0,0 +1,79 @@
+;;; Rabbit Prover --- Prove S-expression
+;;; Copyright © 2020 Masaya Tojo <masaya@tojo.tokyo>
+;;;
+;;; This file is part of Rabbit Prover.
+;;;
+;;; Rabbit Prover is free software; you can redistribute it and/or modify it
+;;; under the terms of the GNU General Public License as published by
+;;; the Free Software Foundation; either version 3 of the License, or
+;;; (at your option) any later version.
+;;;
+;;; Rabbit Prover is distributed in the hope that it will be useful, but
+;;; WITHOUT ANY WARRANTY; without even the implied warranty of
+;;; MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the GNU
+;;; General Public License for more details.
+;;;
+;;; You should have received a copy of the GNU General Public License
+;;; along with Rabbit Prover.  If not, see <http://www.gnu.org/licenses/>.
+
+(define-module (rabbit-prover ord)
+  #:export (ord?
+            ord-fin?
+            ord-inf?
+            ord-first-expt
+            ord-first-coeff
+            ord-rest
+            ord<)
+  #:use-module (rabbit-prover syntax)
+  #:use-module (rabbit-prover primitive))
+
+;;; ACL2's O-p
+;; https://www.cs.utexas.edu/users/moore/acl2/manuals/current/manual/index-seo.php/ACL2____O-P?path=3574/6842/3819/225/243
+(define (ord? x)
+  (if (ord-fin? x)
+      (natural? x)
+      (and (pair? (car x))
+           (ord? (ord-first-expt x))
+           (not (eqv? 0 (ord-first-expt x)))
+           (positive? (ord-first-coeff x))
+           (ord< (ord-first-expt (ord-rest x))
+                 (ord-first-expt x)))))
+
+(define/guard (ord (first-expt ord?) (first-coeff positive?) (rest ord?))
+  (cons (cons first-expt first-coeff) rest))
+
+(define (ord-fin? x)
+  (not (pair? x)))
+
+(define (ord-inf? x)
+  (pair? x))
+
+(define (ord-first-expt x)
+  (if (ord-fin? x)
+      0
+      (caar x)))
+
+(define (ord-first-coeff x)
+  (if (ord-fin? x)
+      x
+      (cdar x)))
+
+(define (ord-rest x)
+  (cdr x))
+
+(define (ord< x y)
+  (cond ((ord-fin? x)
+         (or (ord-inf? y)
+             (< x y)))
+        ((ord-fin? y) #f)
+        ((not (equal? (ord-first-expt x)
+                      (ord-first-expt y)))
+         (ord< (ord-first-expt x)
+               (ord-first-expt y)))
+        ((not (= (ord-first-coeff x)
+                 (ord-first-coeff y)))
+         (< (ord-first-coeff x)
+            (ord-first-coeff y)))
+        (else
+         (ord< (ord-rest x)
+               (ord-rest y)))))
diff --git a/rabbit-prover/primitive.scm b/rabbit-prover/primitive.scm
new file mode 100644
index 0000000..e20406e
--- /dev/null
+++ b/rabbit-prover/primitive.scm
@@ -0,0 +1,25 @@
+;;; Rabbit Prover --- Prove S-expression
+;;; Copyright © 2020 Masaya Tojo <masaya@tojo.tokyo>
+;;;
+;;; This file is part of Rabbit Prover.
+;;;
+;;; Rabbit Prover is free software; you can redistribute it and/or modify it
+;;; under the terms of the GNU General Public License as published by
+;;; the Free Software Foundation; either version 3 of the License, or
+;;; (at your option) any later version.
+;;;
+;;; Rabbit Prover is distributed in the hope that it will be useful, but
+;;; WITHOUT ANY WARRANTY; without even the implied warranty of
+;;; MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the GNU
+;;; General Public License for more details.
+;;;
+;;; You should have received a copy of the GNU General Public License
+;;; along with Rabbit Prover.  If not, see <http://www.gnu.org/licenses/>.
+
+(define-module (rabbit-prover primitive)
+  #:export (natural?))
+
+;; (natural? x) -> boolean?
+(define (natural? x)
+  (and (integer? x)
+       (not (negative? x))))
diff --git a/rabbit-prover/syntax.scm b/rabbit-prover/syntax.scm
new file mode 100644
index 0000000..5087ea2
--- /dev/null
+++ b/rabbit-prover/syntax.scm
@@ -0,0 +1,31 @@
+;;; Rabbit Prover --- Prove S-expression
+;;; Copyright © 2020 Masaya Tojo <masaya@tojo.tokyo>
+;;;
+;;; This file is part of Rabbit Prover.
+;;;
+;;; Rabbit Prover is free software; you can redistribute it and/or modify it
+;;; under the terms of the GNU General Public License as published by
+;;; the Free Software Foundation; either version 3 of the License, or
+;;; (at your option) any later version.
+;;;
+;;; Rabbit Prover is distributed in the hope that it will be useful, but
+;;; WITHOUT ANY WARRANTY; without even the implied warranty of
+;;; MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the GNU
+;;; General Public License for more details.
+;;;
+;;; You should have received a copy of the GNU General Public License
+;;; along with Rabbit Prover.  If not, see <http://www.gnu.org/licenses/>.
+
+(define-module (rabbit-prover syntax)
+  #:export (define/guard))
+
+(define-syntax-rule (define/guard (name (var pred?) ...) b b* ...)
+  (define (name var ...)
+    (unless (pred? var)
+      (error (format #f
+                     "~a:~%  expected:  ~a~%  given: "
+                     'name
+                     'pred?)
+             var))
+    ...
+    b b* ...))