wip26

2 files changed, 175 insertions, 15 deletions

diff --git a/vikalpa.scm b/vikalpa.scm
index 5151204..fcb9005 100644
--- a/vikalpa.scm
+++ b/vikalpa.scm
@@ -17,14 +17,16 @@
 ;;; along with Vikalpa.  If not, see <http://www.gnu.org/licenses/>.
 
 (define-module (vikalpa)
-  #:export (check
+  #:export (rewrite
+            show
+            check
             system->scheme
             define-system
             define-axiom
             define-theorem
             define-primitive-function
             define-function
-            define-macro)
+            define-syntax-rules)
   #:use-module (ice-9 match)
   #:use-module (ice-9 format)
   #:use-module (ice-9 control)
@@ -32,7 +34,8 @@
                 #:select (every any member lset-union fold append-map))
   #:use-module (srfi srfi-8)
   #:use-module (srfi srfi-11)
-  #:use-module (srfi srfi-26))
+  #:use-module (srfi srfi-26)
+  #:use-module (ice-9 pretty-print))
 
 (define (debug f . args)
   (if #f
@@ -586,7 +589,7 @@
                  (else (loop (cdr rs))))))
         (else #f)))
 
-(define/guard (expand (ms (list-of macro?)) (expr (const #t)))
+(define (expand ms expr)
   (let loop ((ms ms)
              (expr expr))
     (cond
@@ -596,7 +599,7 @@
                     ((apply-macro (car ms) expr) => identity)
                     (else expr)))))))
 
-(define/guard (expand* (ms (list-of macro?)) (expr (const #t)))
+(define (expand* ms expr)
   (let loop ((ms ms)
              (expr expr))
     (let ((new-expr (expand ms expr)))
@@ -609,10 +612,11 @@
 
 (define (quote-all x)
   (cond
+   ((null? x) x)
    ((expr-quoted? x) x)
    ((pair? x)
-    (cons (expand-let (car x))
-          (expand-let (cdr x))))
+    (cons (quote-all (car x))
+          (quote-all (cdr x))))
    ((symbol? x) x)
    (else `',x)))
 
@@ -657,8 +661,9 @@
    (else x)))
 
 (define (convert-to-expression x)
-  (expand* (filter macro? (system-definitions (current-system)))
-           (quote-all (expand-let x))))
+  (quote-all
+   (expand* (filter macro? (system-definitions (current-system)))
+            (expand-let x))))
 
 ;; (axiom variable? vars? expression?) -> axiom?
 ;; axiom? is theorem*
@@ -948,6 +953,9 @@
                               (cons x (system-proofs sys))))))
     x))
 
+(define (reserved? x)
+  (member x '(if quote let)))
+
 (define-syntax define-axiom
   (syntax-rules ()
     ((_ name (var ...) expr)
@@ -983,7 +991,7 @@
        (add-definition f)
        f))))
 
-(define-syntax define-macro
+(define-syntax define-syntax-rules
   (syntax-rules ()
     ((_ name (l ...) ((lhs1 . lhs2) rhs) ...)
      (let ((m (macro 'name
@@ -1082,21 +1090,21 @@
     (equal? (if (not x) y z)
             (if x z y)))
 
-  (define-macro list ()
+  (define-syntax-rules list ()
     ((list) '())
     ((list x . y) (cons x (list . y))))
 
-  (define-macro and ()
+  (define-syntax-rules and ()
     ((and) '#t)
     ((and x) x)
     ((and x . xs) (if x (and . xs) #f)))
 
-  (define-macro or ()
+  (define-syntax-rules or ()
     ((or) '#f)
     ((or x) x)
     ((or x . xs) (if x x (or . xs))))
 
-  (define-macro cond (else)
+  (define-syntax-rules cond (else)
     ((cond (else e)) e)
     ((cond (test then) . rest)
      (if test then (cond . rest)))))
@@ -1289,6 +1297,8 @@
          (name (definition-name d))
          (expr-fnames (expression-functions expr))
          (expr-vars (expression-vars expr)))
+    (when (reserved? name)
+      (error (format #f "(vikalpa) ~a: reserved name" name)))
     (for-each (lambda (x)
                 (unless (cond
                          ((lookup x (current-system)) => function*?)
@@ -1397,7 +1407,7 @@
          (size (cdr x)))
       0))
 
-(define (check sys)
+(define/guard (check (sys system?))
   (let loop ((sys sys)
              (fails '()))
     (let ((defs (system-definitions sys)))
@@ -1441,3 +1451,37 @@
             (next (definition-name (car defs))))))))
        (else
         (next))))))
+
+(define/guard (show (sys system?) (name symbol?))
+  (define (pp x)
+    (pretty-print x
+                  #:width 79
+                  #:max-expr-width 50))
+  (cond
+   ((lookup name sys)
+    => (lambda (def)
+         (cond
+          ((function? def)
+           (pp
+            `(define-function ,(function-name def) ,(function-vars def)
+               ,(function-expression def))))
+          ((theorem? def)
+           (pp
+            `(define-theorem ,(theorem*-name def) ,(theorem*-vars def)
+               ,(theorem*-expression def))))
+          ((axiom? def)
+           (pp
+            `(define-axiom ,(theorem*-name def) ,(theorem*-vars def)
+               ,(theorem*-expression def))))
+          ((primitive-function? def)
+           (pp
+            `(define-primitive-function
+               ,(primitive-function-name def)
+               ,(primitive-function-vars def))))
+          ((macro? def)
+           (pp
+            `(define-syntax-rules ,(macro-name def))))
+          (else
+           (error "show: error")))))
+   (else
+    (format #t "~a: not found~%" name))))
diff --git a/vikalpa/prelude.scm b/vikalpa/prelude.scm
new file mode 100644
index 0000000..874614d
--- /dev/null
+++ b/vikalpa/prelude.scm
@@ -0,0 +1,116 @@
+;;; Vikalpa --- Proof Assistant
+;;; Copyright © 2020 Masaya Tojo <masaya@tojo.tokyo>
+;;;
+;;; This file is part of Vikalpa.
+;;;
+;;; Vikalpa 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.
+;;;
+;;; Vikalpa 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 Vikalpa.  If not, see <http://www.gnu.org/licenses/>.
+
+(define-module (vikalpa prelude)
+  #:export (atom? natural? size implies prelude)
+  #:use-module (vikalpa))
+
+(define (atom? x)
+  (not (pair? x)))
+
+(define (natural? x)
+  (and (integer? x)
+       (not (negative? x))))
+
+(define (size x)
+  (if (pair? x)
+      (+ 1
+         (size (car x))
+         (size (cdr x)))
+      0))
+
+(define-syntax implies
+  (syntax-rules ()
+    ((_ x y) (if x y #t))
+    ((_ x y z rest ...)
+     (if x (implies y z rest ...) #t))))
+
+(define-system prelude ()
+  (define-primitive-function natural? (x))
+  (define-primitive-function equal? (x y))
+  (define-primitive-function atom? (x))
+  (define-primitive-function cons (x y))
+  (define-primitive-function car (x))
+
+  (define-primitive-function cdr (x))
+  (define-primitive-function size (x))
+  (define-primitive-function not (x))
+  (define-primitive-function < (x y))
+
+  (define-syntax-rules list ()
+    ((list) '())
+    ((list x . y) (cons x (list . y))))
+  (define-syntax-rules and ()
+    ((and) '#t)
+    ((and x) x)
+    ((and x . xs) (if x (and . xs) #f)))
+  (define-syntax-rules or ()
+    ((or) '#f)
+    ((or x) x)
+    ((or x . xs) (if x x (or . xs))))
+  (define-syntax-rules cond (else)
+    ((cond (else e)) e)
+    ((cond (test then) . rest)
+     (if test then (cond . rest))))
+  (define-syntax-rules implies ()
+    ((implies x y) (if x y #t))
+    ((implies x y z . rest)
+     (if x (implies y z . rest) #t)))
+  
+  (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)
+    (implies (equal? x y) (equal? x y)))
+  (define-axiom atom/cons (x y)
+    (equal? (atom? (cons x y)) '#f))
+  (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)
+    (if (atom? x)
+        '#t
+        (equal? (cons (car x) (cdr x)) x)))
+  (define-axiom if-nest (x y z)
+    (if x
+        (equal? (if x y z) y)
+        (equal? (if x y z) z)))
+  (define-axiom if-true (x y)
+    (equal? (if '#f x y) y))
+  (define-axiom if-false (x y)
+    (equal? (if '#f x y) y))
+  (define-axiom if-same (x y)
+    (equal? (if x y y) y))
+  (define-axiom natural/size (x)
+    (equal? (natural? (size x))
+            '#t))
+  (define-axiom size/car (x)
+    (if (atom? x)
+        '#t
+        (equal? (< (size (car x)) (size x))
+                '#t)))
+  (define-axiom size/cdr (x)
+    (if (atom? x)
+        '#t
+        (equal? (< (size (cdr x)) (size x))
+                '#t)))
+  (define-axiom if-not (x y z)
+    (equal? (if (not x) y z)
+            (if x z y))))