From f590c9c29ff60b1e3ab9ebfb8703d390a5b3df1c Mon Sep 17 00:00:00 2001 From: Masaya Tojo Date: Tue, 5 Jan 2021 10:02:22 +0900 Subject: wip68 --- vikalpa.scm | 8 ++-- vikalpa/prelude.scm | 117 ++++++++++++++++++++++++++++++++++------------------ 2 files changed, 80 insertions(+), 45 deletions(-) diff --git a/vikalpa.scm b/vikalpa.scm index 8713e25..3e45883 100644 --- a/vikalpa.scm +++ b/vikalpa.scm @@ -718,12 +718,12 @@ (result/error 'guard-error `(,name ,@args) `(and ,@gs)))))) (else (result/error 'function-not-found name))))) ((if-form? expr) - (let ((test/result (eval (if-form-test expr)))) - (if (error? test/result) + (let ((test/result (eval (result/expr (if-form-test expr))))) + (if (result/error? test/result) test/result (if (expr-unquote (result/expr-expr test/result)) - (eval (if-form-then expr)) - (eval (if-form-else expr)))))) + (eval (result/expr (if-form-then expr))) + (eval (result/expr (if-form-else expr))))))) ((variable? expr) (result/error 'eval 'variable-found expr)) (else diff --git a/vikalpa/prelude.scm b/vikalpa/prelude.scm index 2da6e8e..e24d32d 100644 --- a/vikalpa/prelude.scm +++ b/vikalpa/prelude.scm @@ -61,8 +61,10 @@ ((implies x y) (if x y #t)) ((implies x y z . rest) (if x (implies y z . rest) #t))) - (define-syntax-rules is-a () - ((is-a x y) (implies x (equal? y #t))))) + (define-syntax-rules predicate () + ((predicate x) (implies x (equal? x #t)))) + (define-syntax-rules is () + ((is x y) (implies x (equal? y #t))))) (define-system prelude/axiom/equal (prelude/macro) (define-axiom equal-same (x) @@ -91,71 +93,61 @@ (define-system prelude/number (prelude/axiom/if) (define-core-function number? (x) number?) - (define-axiom number-predicate (x) - (is-a (number? x) (number? x))) + (define-axiom (predicate number?) (x) (predicate (number? x))) (define-core-function real? (x) real?) - (define-axiom real-predicate (x) - (implies (real? x) (equal? (real? x) #t))) - (define-axiom real-is-a-numbers (x) - (implies (real? x) (equal? (number? x) #t))) + (define-axiom (predicate real?) (x) (predicate (real? x))) + (define-axiom (is real? number?) (x) (is (real? x) (number? x))) (define-core-function integer? (x) integer?) - (define-axiom integer-predicate (x) - (implies (integer? x) (equal? (integer? x) #t))) - (define-axiom integer-is-a-real (x) - (implies (integer? x) (equal? (number? x) #t))) + (define-axiom (predicate integer?) (x) (predicate (integer? x))) + (define-axiom (is integer? real?) (x) (is (integer? x) (real? x))) (define-core-function/guard exact? (x) (number? x) exact?) - (define-axiom exact-predicate (x) - (implies (exact? x) (equal? (exact? x) #t))) + (define-axiom (predicate exact?) (x) (predicate (exact? x))) (define-function/guard inexact? (x) (number? x) (not (exact? x))) - (define-theorem inexact-predicate (x) - (implies (inexact? x) (equal? (inexact? x) #t))) + (define-theorem (predicate inexact?) (x) (predicate (inexact? x))) (define-core-function exact-integer? (x) exact-integer?) - (define-axiom exact-integer-predicate (x) - (implies (exact-integer? x) (equal? (exact-integer? x) #t))) - (define-axiom exact-integer-is-a-integer (x) - (implies (exact-integer? x) (equal? (integer? x) #t))) - (define-axiom exact-integer-is-a-exact (x) - (implies (exact-integer? x) (equal? (exact? x) #t))) - + (define-axiom (predicate exact-integer?) (x) (predicate (exact-integer? x))) + (define-axiom (is exact-integer? integer?) (x) + (is (exact-integer? x) + (integer? x))) + (define-axiom (is exact-integer? exact?) (x) (is (exact-integer? x) + (exact? x))) + (define-theorem (is exact-integer? real?) (x) + (is (exact-integer? x) (real? x))) (define-core-function/guard < (x y) (and (real? x) (real? y)) <) - (define-axiom less-than-predicate (x y) - (implies (< x y) (equal? (< x y) #t))) + (define-axiom (predicate <) (x y) (predicate (< x y))) (define-function/guard positive? (x) (real? x) (< 0 x)) - (define-theorem positive-predicate (x) - (implies (positive? x) (equal? (positive? x) #t))) + (define-theorem (predicate positive?) (x) (predicate (positive? x))) (define-function/guard negative? (x) (real? x) (< x 0)) - (define-theorem negative-predicate (x) - (implies (negative? x) (equal? (negative? x) #t))) + (define-theorem (predicate negative?) (x) (predicate (negative? x))) (define-function exact-positive-integer? (x) (and (exact-integer? x) (positive? x))) - (define-theorem exact-positive-integer-predicate (x) - (implies (exact-positive-integer? x) - (equal? (exact-positive-integer? x) #t))) + (define-theorem (predicate exact-positive-integer?) (x) + (predicate (exact-positive-integer? x))) (define-function exact-zero? (x) (equal? x 0)) - (define-theorem exact-zero-predicate (x) - (implies (exact-zero? x) (equal? (exact-zero? x) #t))) + (define-theorem (predicate exact-zero?) (x) + (predicate (exact-zero? x))) (define-function natural? (x) (if (exact-zero? x) #t (exact-positive-integer? x))) (define-theorem (predicate natural?) (x) - (implies (natural? x) (equal? (natural? x) #t)))) + (predicate (natural? x)))) (define-system prelude/measure/natural (prelude/number) (set-measure-predicate natural?) @@ -171,7 +163,7 @@ (define-proof inexact? ((rewrite (2) if-nest) (rewrite () if-same))) - (define-proof inexact-predicate + (define-proof (predicate inexact?) ((rewrite (1) inexact?) (rewrite () if-not) (rewrite (3 1) inexact?) @@ -183,10 +175,10 @@ (rewrite (2 1) if-true) (rewrite (2) if-nest) (rewrite () if-same))) - (define-proof positive-predicate + (define-proof (predicate positive?) ((rewrite (1) positive?) (rewrite (2 1) positive?) - (rewrite (2 1) less-than-predicate) + (rewrite (2 1) (predicate <)) (eval (2)) (rewrite () if-same))) (define-proof negative? @@ -194,10 +186,53 @@ (eval (2 1)) (rewrite (2) if-true) (rewrite () if-same))) - (define-proof negative-predicate + (define-proof (predicate negative?) ((rewrite (1) negative?) (rewrite (2 1) negative?) - (rewrite (2 1) less-than-predicate) + (rewrite (2 1) (predicate <)) + (eval (2)) + (rewrite () if-same))) + (define-proof (is exact-integer? real?) + ((rewrite (2) if-same (set x (integer? x))) + (rewrite (2 2 1) (is integer? real?)) + (eval (2 2)) + (rewrite (2 1) (is exact-integer? integer?)) + (rewrite (2) if-true) + (rewrite () if-same))) + (define-proof exact-positive-integer? + ((rewrite (1 2) (is exact-integer? real?)) + (rewrite (1) if-same) + (eval ()))) + (define-proof (predicate exact-positive-integer?) + ((rewrite (1) exact-positive-integer?) + (rewrite () if-same (set x (exact-integer? x))) + (rewrite (3 1) if-nest) + (rewrite (3) if-false) + (rewrite (2 1) if-nest) + (rewrite (2 2 1) exact-positive-integer?) + (rewrite (2 2 1 1) (predicate exact-integer?)) + (rewrite (2 2 1 2) (predicate positive?)) + (eval (2 2)) + (rewrite (2) if-same) + (rewrite () if-same))) + (define-proof (predicate exact-zero?) + ((rewrite (1) exact-zero?) + (rewrite (2 1 1) equal-if) (eval (2)) + (rewrite () if-same))) + (define-proof (predicate natural?) + ((rewrite (1) natural?) + (rewrite () if-same (set x (exact-zero? x))) + (rewrite (2 1) if-nest) + (rewrite (2) if-true) + (rewrite (3 1) if-nest) + (rewrite (1) exact-zero?) + (rewrite (2 1 1) equal-if) + (eval (2)) + (rewrite (1) exact-zero?) + (rewrite (3 2 1) natural?) + (rewrite (3 2 1) if-nest) + (rewrite (3 2 1) (predicate exact-positive-integer?)) + (eval (3 2)) + (rewrite (3) if-same) (rewrite () if-same)))) - -- cgit v1.2.3