From 7a238e7df0c9c7c684b7f761f495b21aa088bd68 Mon Sep 17 00:00:00 2001 From: Masaya Tojo Date: Mon, 9 Nov 2020 02:56:59 +0900 Subject: wip10 --- vikalpa/ord.scm | 79 +++++++++++++++++++++++++++++++++++++++++++++++++++ vikalpa/primitive.scm | 25 ++++++++++++++++ vikalpa/syntax.scm | 31 ++++++++++++++++++++ 3 files changed, 135 insertions(+) create mode 100644 vikalpa/ord.scm create mode 100644 vikalpa/primitive.scm create mode 100644 vikalpa/syntax.scm (limited to 'vikalpa') 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 +;;; +;;; 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 new file mode 100644 index 0000000..bcbced5 --- /dev/null +++ b/vikalpa/primitive.scm @@ -0,0 +1,25 @@ +;;; 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 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 +;;; +;;; 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