wip

1 files changed, 535 insertions, 1 deletions

diff --git a/rabbit-prover.scm b/rabbit-prover.scm
index e661db2..702ba07 100644
--- a/rabbit-prover.scm
+++ b/rabbit-prover.scm
@@ -17,4 +17,538 @@
 ;;; along with Rabbit Prover.  If not, see <http://www.gnu.org/licenses/>.
 
 (define-module (rabbit-prover)
-  #:export ())
+  #:export (rewrite)
+  #:use-module (ice-9 match)
+  #:use-module ((srfi srfi-1) #:select (every any append-map))
+  #:use-module (srfi srfi-8)
+  #:use-module (srfi srfi-26))
+
+(define (option p?)
+  (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)
+         (or (integer? (expr-unquote expr))
+             (boolean? (expr-unquote expr))
+             (symbol? (expr-unquote expr))))
+        ((pair? expr)
+         (and (expression? (car expr))
+              (list? (cdr expr))
+              (every expression? (cdr expr))))
+        ((variable? expr) #t)
+        (else #f)))
+
+;; (expr-quoted? x) -> boolean?
+(define (expr-quoted? expr)
+  (and (pair? expr)
+       (eq? 'quote (car expr))
+       (pair? (cdr expr))
+       ((const #t) (car (cdr expr)))
+       (null? (cdr (cdr expr)))))
+
+(define (expr-unquote expr)
+  (car (cdr expr)))
+
+;; (expr-quoted? x) -> boolean?
+(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))
+
+;; (variable=? variable? variable?) -> boolean?
+(define (variable=? v1 v2)
+  (eq? v1 v2))
+
+;; (rule? x) -> boolean?
+(define (rule? x)
+  (and (list? x)
+       (= 5 (length x))
+       (eq? (car x) 'rule)
+       (let ((vars (list-ref x 1)))
+         (and (list? vars)
+              (every variable? vars)))
+       (let ((preconds (list-ref x 2)))
+         (and (list? preconds)
+              (every expression? preconds)))
+       (expression? (list-ref x 3))
+       (expression? (list-ref x 4))))
+
+;; (rule (list-of variable?) expression? expression?) -> rule?
+(define (rule vars preconds lhs rhs)
+  (list 'rule vars preconds lhs rhs))
+
+;; (rule-vars rule?) -> (list-of variable?)
+(define (rule-vars r)
+  (list-ref r 1))
+
+;; (rule-preconds rule?) -> expression?
+(define (rule-preconds r)
+  (list-ref r 2))
+
+;; (rule-lhs rule?) -> expression?
+(define (rule-lhs r)
+  (list-ref r 3))
+
+;; (rule-rhs rule?) -> expression?
+(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)))
+
+;; (apply-rule preconds rule? expression?) -> (or (cons rhs environment) #f)
+(define (apply-rule preconds rl expr)
+  (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))))))
+
+;; (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)
+  (cond ((null? x) #t)
+        ((pair? x)
+         (and (pair? (car x))
+              (or (proposition? (car x))
+                  (primitive-function? (car x))
+                  (macro? (car x)))
+              (book? (cdr x))))
+        (else #f)))
+
+(define (primitive-function? x)
+  (and (list? x)
+       (= 4 (length x))
+       (variable? (list-ref x 0))
+       (eq? 'primitive-function (list-ref x 1))
+       (let ((ps (list-ref x 2)))
+         (and (list? ps)
+              (every procedure? ps)))
+       (procedure? (list-ref x 3))))
+
+;; (primitive-function variable? (list-of procedure?) procedure?) -> primitive-function?
+(define (primitive-function name ps proc)
+  (list name 'primitive-function ps proc))
+
+(define (primitive-function-name pf)
+  (list-ref pf 0))
+
+(define (primitive-function-preds pf)
+  (list-ref pf 2))
+
+(define (primitive-function-proc pf)
+  (list-ref pf 3))
+
+(define (match-primitive-function pf expression)
+  (and (pair? expression)
+       (eq? (primitive-function-name pf) (car expression))
+       (list? (cdr expression))
+       (every identity (map (lambda (pred expr)
+                              (and (expr-quoted? expr)
+                                   (pred (expr-unquote expr))))
+                            (primitive-function-preds pf)
+                            (cdr expression)))))
+
+(define (apply-primitive-function pf expression)
+  (if (match-primitive-function pf expression)
+      (apply (primitive-function-proc pf) (cdr expression))
+      expression))
+
+(define (function? x)
+  (and (list? x)
+       (= 5 (length x))
+       (variable? (list-ref x 0))
+       (eq? 'function (list-ref x 1))
+       (vars? (list-ref x 2))
+       (expression? (list-ref x 3))
+       ((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)))
+  (list name 'function vars expr proof))
+
+(define (function-name f)
+  (list-ref f 0))
+
+(define (function-vars f)
+  (list-ref f 2))
+
+(define (function-expression f)
+  (list-ref f 3))
+
+(define (function-proof f)
+  (list-ref f 4))
+
+(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)))))
+
+(define (macro-name m)
+  (list-ref m 0))
+
+(define (macro-rules m)
+  (list-ref m 2))
+
+(define (macro name rules)
+  (list 'macro name rules))
+
+(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) =>
+                  (cut apply-macro m <>))
+                 (else (loop (cdr rs))))))
+        (else expr)))
+
+(define (expand ms expr)
+  (let loop ((ms ms)
+             (expr expr))
+    (cond
+     ((null? ms) expr)
+     (else (expand (cdr ms) (apply-macro (car ms) expr))))))
+
+(define (expand* ms expr)
+  (let loop ((ms ms)
+             (expr expr))
+    (let ((new-expr (expand ms expr)))
+      (if (equal? expr new-expr)
+          (if (pair? new-expr)
+              (cons (expand* ms (car new-expr))
+                    (expand* ms (cdr new-expr)))
+              new-expr)
+          (expand* ms new-expr)))))
+
+;; (axiom variable? vars? expression?) -> axiom?
+;; axiom? is proposition
+(define/assert (axiom (name variable?) (vars vars?) (expr expression?))
+  (list name 'axiom vars expr))
+
+(define (vars? x)
+  (and (list? x)
+       (every variable? x)))
+
+;; (axiom? x) -> boolean?
+(define (axiom? x)
+  (and (list? x)
+       (= 4 (length x))
+       (variable?  (list-ref x 0))
+       (eq? 'axiom (list-ref x 1))
+       (vars? (list-ref x 2))
+       (expression? (list-ref x 3))))
+
+;; (theorem name vars? expression? proof?) -> theorem?
+(define/assert (theorem (name variable?) (vars vars?) (expr expression?) (p (option proof?)))
+  (list name 'theorem vars expr p))
+
+;; (theorem? x) -> boolean?
+;; theorem? is proposition
+(define (theorem? x)
+  (and (list? x)
+       (= 5 (length x))
+       (variable? (list-ref x 0))
+       (eq? 'theorem (list-ref x 1))
+       (vars? (list-ref x 2))
+       (expression? (list-ref x 3))
+       ((option proof?) (list-ref x 4))))
+
+(define (theorem-name x)
+  (list-ref x 0))
+
+(define (theorem-proof x)
+  (list-ref x 4))
+
+(define (proof seq)
+  (list 'proof seq))
+
+;; (proposition? x) -> boolean?
+(define (proposition? x)
+  (or (axiom? x)
+      (theorem? x)
+      (conjecture? x)
+      (function? x)))
+
+(define (proposition-vars x)
+  (list-ref x 2))
+
+(define (proposition-expression x)
+  (list-ref x 3))
+
+(define (proposition-rules x)
+  (expression->rules (proposition-vars x)
+                     '()
+                     (proposition-expression x)))
+
+;; (proof? x) -> boolean?
+(define (proof? x)
+  (and (list? x)
+       (= 2 (length x))
+       (eq? 'proof (list-ref x 0))
+       (sequence? (list-ref x 1))))
+
+;; (rewriter path? command?) -> rewriter?
+(define (rewriter p c)
+  (list p c))
+
+(define (rewriter-path r)
+  (list-ref r 0))
+
+(define (rewriter-command r)
+  (list-ref r 1))
+
+(define (rewriter? x)
+  (and (path? (car x))
+       (pair? (cdr x))
+       (command? (car (cdr x)))
+       (null? (cdr (cdr x)))))
+
+;; (sequence? x) -> boolean?
+(define (sequence? x)
+  (and (list? x)
+       (every rewriter? x)))
+
+;; (path? x) -> boolean?
+;; path is list
+(define (path? x)
+  (and (list? x)
+       (every natural? x)))
+
+;; (command? x) -> booelan?
+(define (command? x)
+  (symbol? x))
+
+;; (extract path? expression? preconds? procedure?) -> (values expression? procedure?)
+(define (extract path expr fail)
+  (if (null? path)
+      (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)
+                (extract (cdr path) (list-ref expr i) fail)
+              (values extracted-expr
+                      (case i
+                        ((1) '())
+                        ((2) (cons precond extracted-preconds))
+                        ((3) (cons (expr-not precond) extracted-preconds))
+                        (else (fail "(if) invaild path" path)))
+                      (lambda (x)
+                        (append (list-head expr i)
+                                (list (builder x))
+                                (list-tail expr (+ i 1))))))))
+         (else
+          (fail "invalid path" path))))))
+
+;; (rewrite book? rewriter? expression? procedure?) -> expr
+(define (rewrite1 b expr fail r)
+  (let ((cmd (rewriter-command r)))
+    (receive (extracted-expr preconds builder)
+        (extract (rewriter-path r) expr fail)
+      (builder
+       (cond
+        ((assoc cmd b) =>
+         (lambda (x)
+           (cond
+            ((proposition? x)
+             (let ((rls (proposition-rules x)))
+               (cond
+                ((any (cut apply-rule preconds <> extracted-expr)
+                      rls) => identity)
+                (else
+                 (fail (format #f "no match-rule (~a)" cmd))))))
+            ((primitive-function? x)
+             (cond
+              ((match-primitive-function x extracted-expr)
+               (apply-primitive-function x extracted-expr))
+              (else
+               (fail "can't apply-primitive-function (~a)" cmd))))
+            ((macro? x)
+             (fail "macro は だめ"))
+            (else
+             (fail "rewrite error")))))
+        (else (fail "no cmd (~a)" cmd)))))))
+
+(define/assert (rewrite (b book?) (expr expression?) (seq sequence?))
+  (let loop ((expr expr)
+             (seq seq))
+    (if (null? seq)
+        expr
+        (loop (rewrite1 b
+                        expr
+                        (lambda (x . args)
+                          (apply error
+                                 (format #f "rewrite: ~a" x)
+                                 args))
+                        (car seq))
+              (cdr seq)))))
+
+(define (expr-not x)
+  (list 'not x))
+
+(define (expr-equal? x)
+  (and (list? x)
+       (= 3 (length x))
+       (eq? 'equal? (list-ref x 0))
+       (expression? (list-ref x 1))
+       (expression? (list-ref x 2))))
+
+(define (expr-equal-lhs x)
+  (list-ref x 1))
+
+(define (expr-equal-rhs x)
+  (list-ref x 2))
+
+(define (expr-if? x)
+  (and (list? x)
+       (= 4 (length x))
+       (eq? 'if (list-ref x 0))
+       (expression? (list-ref x 1))
+       (expression? (list-ref x 2))
+       (expression? (list-ref x 3))))
+
+(define (expr-if-cond x)
+  (list-ref x 1))
+
+(define (expr-if-then x)
+  (list-ref x 2))
+
+(define (expr-if-else x)
+  (list-ref x 3))
+
+(define (expression->rules vars preconds expr)
+  (if (expr-if? expr)
+      (append (expression->rules vars
+                                 (cons (expr-if-cond expr) preconds)
+                                 (expr-if-then expr))
+              (expression->rules vars
+                                 (cons (expr-not (expr-if-cond expr)) preconds)
+                                 (expr-if-else expr)))
+      (if (expr-equal? expr)
+          (list (rule vars
+                      preconds
+                      (expr-equal-lhs expr)
+                      (expr-equal-rhs expr)))
+          '())))
+
+(define (proposition->rules def)
+  (expression->rules (proposition-vars def)
+                     '()
+                     (proposition-expression def)))
+
+(define-syntax define-axiom
+  (syntax-rules ()
+    ((_ name (var ...) expr)
+     (axiom 'name '(var ...) 'expr))))
+
+(define prelude
+  (list (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 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))))