blob: 874614d3379bc4b10f0f06dd7dda0c7f71e06013 (
plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
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))))
|
