From a11683d118505ad3ca9c27a5734fae9ee122267c Mon Sep 17 00:00:00 2001 From: Masaya Tojo Date: Wed, 18 Nov 2020 12:55:16 +0900 Subject: wip21 --- vikalpa/ord.scm | 79 --------------------------------------------------- vikalpa/primitive.scm | 25 ---------------- vikalpa/syntax.scm | 31 -------------------- 3 files changed, 135 deletions(-) delete mode 100644 vikalpa/ord.scm delete mode 100644 vikalpa/primitive.scm delete mode 100644 vikalpa/syntax.scm (limited to 'vikalpa') diff --git a/vikalpa/ord.scm b/vikalpa/ord.scm deleted file mode 100644 index 9715979..0000000 --- a/vikalpa/ord.scm +++ /dev/null @@ -1,79 +0,0 @@ -;;; Vikalpa --- Prove S-expression -;;; Copyright © 2020 Masaya Tojo -;;; -;;; 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 . - -(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 deleted file mode 100644 index bcbced5..0000000 --- a/vikalpa/primitive.scm +++ /dev/null @@ -1,25 +0,0 @@ -;;; Vikalpa --- Proof Assistant -;;; Copyright © 2020 Masaya Tojo -;;; -;;; 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 . - -(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 deleted file mode 100644 index 046c13a..0000000 --- a/vikalpa/syntax.scm +++ /dev/null @@ -1,31 +0,0 @@ -;;; Vikalpa --- Prove S-expression -;;; Copyright © 2020 Masaya Tojo -;;; -;;; 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 . - -(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* ...)) -- cgit v1.2.3