1 files changed, 116 insertions, 0 deletions
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))))