diff options
author | Masaya Tojo <masaya@tojo.tokyo> | 2020-11-09 02:56:59 +0900 |
---|---|---|
committer | Masaya Tojo <masaya@tojo.tokyo> | 2020-11-09 02:56:59 +0900 |
commit | 7a238e7df0c9c7c684b7f761f495b21aa088bd68 (patch) | |
tree | 299eb84b8706557655a6ea01d32ab37ec94d2789 /vikalpa | |
parent | 51b6399599676a5c1a9c6cb27be88a1381f7af8a (diff) |
wip10
Diffstat (limited to 'vikalpa')
-rw-r--r-- | vikalpa/ord.scm | 79 | ||||
-rw-r--r-- | vikalpa/primitive.scm | 25 | ||||
-rw-r--r-- | vikalpa/syntax.scm | 31 |
3 files changed, 135 insertions, 0 deletions
diff --git a/vikalpa/ord.scm b/vikalpa/ord.scm new file mode 100644 index 0000000..9715979 --- /dev/null +++ b/vikalpa/ord.scm @@ -0,0 +1,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))))) diff --git a/vikalpa/primitive.scm b/vikalpa/primitive.scm new file mode 100644 index 0000000..bcbced5 --- /dev/null +++ b/vikalpa/primitive.scm @@ -0,0 +1,25 @@ +;;; 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 primitive) + #:export (natural?)) + +;; (natural? x) -> boolean? +(define (natural? x) + (and (integer? x) + (not (negative? x)))) diff --git a/vikalpa/syntax.scm b/vikalpa/syntax.scm new file mode 100644 index 0000000..046c13a --- /dev/null +++ b/vikalpa/syntax.scm @@ -0,0 +1,31 @@ +;;; 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 syntax) + #:export (define/guard)) + +(define-syntax-rule (define/guard (name (var pred?) ...) b b* ...) + (define (name var ...) + (unless (pred? var) + (error (format #f + "~a:~% expected: ~a~% given: " + 'name + 'pred?) + var)) + ... + b b* ...)) |