blob: 97159797657fdfab0e0608972069f31c5f30e07f (
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
|
;;; Vikalpa --- Prove S-expression
;;; 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 ord)
#:export (ord?
ord-fin?
ord-inf?
ord-first-expt
ord-first-coeff
ord-rest
ord<)
#:use-module (vikalpa syntax)
#:use-module (vikalpa 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)))))
|
