From bc388110c1a00c2450778e433788f8f2997e4359 Mon Sep 17 00:00:00 2001 From: Masaya Tojo Date: Sun, 10 Jan 2021 05:21:58 +0900 Subject: wip70 --- vikalpa.scm | 164 +++++++++++++++++++++++----------------------------- vikalpa/prelude.scm | 15 ----- 2 files changed, 73 insertions(+), 106 deletions(-) diff --git a/vikalpa.scm b/vikalpa.scm index 3e45883..79f6fb1 100644 --- a/vikalpa.scm +++ b/vikalpa.scm @@ -95,7 +95,7 @@ (format port "#<~a: ~s>" sym (cons (get-name d) (get-variables d)))) -(define-method (write (s ) port) +(define-method (display (s ) port) (format port "#" (length (filter (cut is-a? <> ) (get-definitions s))) @@ -104,22 +104,14 @@ (length (filter (cut is-a? <> ) (get-definitions s))))) -(define-method (write (d ) port) - (write-definition 'macro d port)) -(define-method (write (d ) port) - (write-definition 'conjecture d port)) -(define-method (write (d ) port) - (write-definition 'theorem d port)) -(define-method (write (d ) port) - (write-definition 'axiom d port)) -(define-method (write (d ) port) - (write-definition 'axiom d port)) -(define-method (write (d ) port) - (write-definition 'function d port)) -(define-method (write (d ) port) - (write-definition 'core-function d port)) -(define-method (write (d ) port) - (write-definition 'total-function d port)) +(define-method (write (s ) port) + (format port "#" + (length (filter (cut is-a? <> ) + (get-definitions s))) + (length (filter (cut is-a? <> ) + (get-definitions s))) + (length (filter (cut is-a? <> ) + (get-definitions s))))) (define-method (lookup name (s )) (find (lambda (x) @@ -201,11 +193,6 @@ (validate-expression (current-system) name vars expr) (next-method))) -(define (debug f . args) - (if #f - (apply format #t f args) - #t)) - (define-syntax-rule (define/guard (name (var p?) ...) b b* ...) (define (name var ...) (unless (p? var) @@ -367,7 +354,6 @@ ((list-of binding?) x)) (define/guard (substitute (env env?) (expr (const #t))) - (debug "substitute: ~s ~s~%" env expr) (cond ((expr-quoted? expr) expr) ((pair? expr) (cons (substitute env (car expr)) @@ -404,7 +390,6 @@ (define (mat-begin lhs expr env) (reset (mat lhs expr env))) (define (mat lhs expr env) - (debug "lhs ~a, expr ~a, env ~a~%" lhs expr env) (cond ((expr-quoted? lhs) (if (expr-quoted? expr) (if (equal? lhs expr) @@ -454,9 +439,6 @@ (cond ((assoc expr env) => (const #t)) (else #f))) (else #t))) - (debug "rule: lhs: ~a rhs: ~a~%" (rule-lhs rl) (rule-rhs rl)) - (debug "preconds: ~a~%" preconds) - (debug "expr: ~a~%" expr) (reset (shift k0 (match (mat-preconds (rule-preconds rl) (cons k0 env)) @@ -852,7 +834,7 @@ (theorem-rules thm)) => result/expr) (else (result/error 'apply-theorem cmd-name expr))))))) - + (define (rewrite/induction sys fname vars expr fail) (cond ((lookup fname sys) @@ -1139,31 +1121,31 @@ (and (pair? x) (null? (cdr x)))) -(define (if/if x y z) +(define (smart-if x y z) (cond ((equal? y z) y) ((equal? x ''#t) y) ((equal? x ''#f) z) (else `(if ,x ,y ,z)))) -(define (and/if . args) +(define (smart-and . args) (cond ((null? args) ''#t) - ((equal? ''#t (car args)) (apply and/if (cdr args))) + ((equal? ''#t (car args)) (apply smart-and (cdr args))) (else - (let ((rest (apply and/if (cdr args)))) + (let ((rest (apply smart-and (cdr args)))) (if (equal? ''#t rest) (car args) - (if/if (car args) - rest - ''#f)))))) + (smart-if (car args) + rest + ''#f)))))) -(define (implies/if x y) +(define (smart-implies x y) (cond ((equal? ''#f x) ''#t) ((equal? ''#t y) ''#t) (else - (if/if x y ''#t)))) + (smart-if x y ''#t)))) (define (make-totality-claim* sys m-expr f) (unless (get-measure-predicate sys) @@ -1191,36 +1173,36 @@ (get-name f) m-expr app-form)))) - (if/if `(,(get-measure-predicate sys) ,m-expr) - (let loop ((expr (get-expression f))) - (cond - ((expr-quoted? expr) ''#t) - ((variable? expr) ''#t) - ((if-form? expr) - (let ((test/result (loop (if-form-test expr))) - (then/result (loop (if-form-then expr))) - (else/result (loop (if-form-else expr)))) - (and/if test/result - (if/if (if-form-test expr) - then/result - else/result)))) - ((app-form? expr) - (let ((rest - (let f ((args (app-form-args expr))) - (cond ((null? args) ''#t) - ((single? args) (loop (car args))) - (else (and/if (loop (car args)) - (f (cdr args)))))))) - (if (eq? name (app-form-name expr)) - (and/if `(,(get-measure-less-than sys) - ,(convert expr) - ,m-expr) - rest) - rest))) - (else (error "(vikalpa) make-totality-claim: error" - (get-name f) - m-expr)))) - ''#f))) + (smart-if `(,(get-measure-predicate sys) ,m-expr) + (let loop ((expr (get-expression f))) + (cond + ((expr-quoted? expr) ''#t) + ((variable? expr) ''#t) + ((if-form? expr) + (let ((test/result (loop (if-form-test expr))) + (then/result (loop (if-form-then expr))) + (else/result (loop (if-form-else expr)))) + (smart-and test/result + (smart-if (if-form-test expr) + then/result + else/result)))) + ((app-form? expr) + (let ((rest + (let f ((args (app-form-args expr))) + (cond ((null? args) ''#t) + ((single? args) (loop (car args))) + (else (smart-and (loop (car args)) + (f (cdr args)))))))) + (if (eq? name (app-form-name expr)) + (smart-and `(,(get-measure-less-than sys) + ,(convert expr) + ,m-expr) + rest) + rest))) + (else (error "(vikalpa) make-totality-claim: error" + (get-name f) + m-expr)))) + ''#f))) (define (make-guard-claim expr sys) (define (find-preconds expr) @@ -1244,28 +1226,28 @@ (define (build/find-if expr) (cond ((if-form? expr) - (if/if (build/find-if (if-form-test expr)) - (build (if-form-then expr)) - (build (if-form-else expr)))) + (smart-if (build/find-if (if-form-test expr)) + (build (if-form-then expr)) + (build (if-form-else expr)))) ((app-form? expr) - (apply and/if (map build/find-if (app-form-args expr)))) + (apply smart-and (map build/find-if (app-form-args expr)))) (else ''#t))) (define (build expr) (cond ((if-form? expr) - (apply and/if + (apply smart-and (append (find-preconds (if-form-test expr)) - (list (if/if (if-form-test expr) - (build (if-form-then expr)) - (build (if-form-else expr))))))) + (list (smart-if (if-form-test expr) + (build (if-form-then expr)) + (build (if-form-else expr))))))) ((app-form? expr) - (apply and/if + (apply smart-and (append (find-preconds expr) (list (build/find-if expr))))) (else ''#t))) - (if/if (build expr) - ''#t - ''#f)) + (smart-if (build expr) + ''#t + ''#f)) (define (make-induction-claim f vars c) (define (find-app-forms expr) @@ -1298,15 +1280,15 @@ (cond ((if-form? expr) (let ((app-forms (find-app-forms (if-form-test expr)))) - (implies/if (if (null? app-forms) - ''#t - (fold implies/if c (map prop app-forms))) - (if/if (if-form-test expr) - (build (if-form-then expr)) - (build (if-form-else expr)))))) + (smart-implies (if (null? app-forms) + ''#t + (fold smart-implies c (map prop app-forms))) + (smart-if (if-form-test expr) + (build (if-form-then expr)) + (build (if-form-else expr)))))) (else (let ((app-forms (find-app-forms expr))) - (fold implies/if c (map prop app-forms)))))))) + (fold smart-implies c (map prop app-forms)))))))) (else (error "make-induction-claim: invalid" f vars c)))) @@ -1346,10 +1328,10 @@ (get-variables f) seed) (update-claim - (fold implies/if - (and/if (make-totality-claim* sys seed f) - (make-guard-claim (get-expression f) - sys)) + (fold smart-implies + (smart-and (make-totality-claim* sys seed f) + (make-guard-claim (get-expression f) + sys)) (get-guards f)))) (raise-exception (make-exception @@ -1357,7 +1339,7 @@ (make-exception-with-message "need measure expression") (make-exception-with-irritants (get-expression f))))) (update-claim - (fold implies/if + (fold smart-implies (make-guard-claim (get-expression f) sys) (get-guards f))))) diff --git a/vikalpa/prelude.scm b/vikalpa/prelude.scm index 74cbe98..d2e54ce 100644 --- a/vikalpa/prelude.scm +++ b/vikalpa/prelude.scm @@ -28,21 +28,6 @@ (and (exact-integer? x) (negative? x))) -(define (succ x) - (if (number? x) - (+ x 1) - 1)) - -(define (pred x) - (if (number? x) - (- x 1) - -1)) - -(define (negate x) - (if (exact-integer? x) - (- x) - 0)) - (define-syntax-rule (define-axiom/is p1 p2) (define-axiom (is p1 p2) (x) (is (p1 x) (p2 x)))) -- cgit v1.2.3