diff options
| -rw-r--r-- | vikalpa.scm | 152 |
1 files changed, 72 insertions, 80 deletions
diff --git a/vikalpa.scm b/vikalpa.scm index e220641..6a2af81 100644 --- a/vikalpa.scm +++ b/vikalpa.scm @@ -202,14 +202,14 @@ (let* ((vars (get-variables d)) (name (get-name d)) (expr (get-expression d))) - (validate-expression (current-system) name vars expr) + (validate-expression name vars expr) (next-method))) (define-method (validate (d <theorem*>)) (let* ((vars (get-variables d)) (name (get-name d)) (expr (get-expression d))) - (validate-expression (current-system) name vars expr) + (validate-expression name vars expr) (next-method))) (define-syntax-rule (define/guard (name (var p?) ...) b b* ...) @@ -649,11 +649,10 @@ (and (list? x) (every variable? x))) -(define (theorem-rules x sys) +(define (theorem-rules x) (expression->rules (get-variables x) '() - (get-expression x) - sys)) + (get-expression x))) (define (result? x) (or (result/error? x) @@ -678,7 +677,7 @@ (define/guard (result/expr-expr (x result/expr?)) (cadr x)) -(define (rewrite/eval expr sys) +(define (rewrite/eval expr) (let eval ((result (result/expr expr))) (cond ((result/error? result) result) @@ -692,7 +691,7 @@ (name (app-form-name expr))) (cond ((find error? args/result) => identity) - ((lookup name sys) + ((lookup name (current-system)) => (lambda (f) (let ((args (map result/expr-expr args/result)) (gs (get-guards f)) @@ -707,8 +706,7 @@ result (expr-unquote (result/expr-expr result))))) (if (every (lambda (g) (guard-ok? vars form g)) gs) - (eval (rewrite1 sys - `(,name ,@args) + (eval (rewrite1 `(,name ,@args) `(rewrite () ,name))) (result/error 'guard-error `(,name ,@args) `(and ,@gs)))))) (else (result/error 'function-not-found name))))) @@ -765,9 +763,8 @@ (cdr x)) (define/guard (system-eval (sys system?) (expr (const #t))) - (rewrite/eval (parameterize ((current-system sys)) - (convert-to-expression expr)) - sys)) + (parameterize ((current-system sys)) + (rewrite/eval (convert-to-expression expr)))) (define (extract path expr fail) (if (null? path) @@ -834,7 +831,7 @@ (else (fail 'invalid-option (car ops))))))) -(define (rewrite/theorem cmd-name cmd-ops b thm preconds expr sys) +(define (rewrite/theorem cmd-name cmd-ops thm preconds expr) (call/cc (lambda (k) (define (fail . args) @@ -843,11 +840,11 @@ (parse-options/theorem cmd-ops fail) (cond ((any (cut apply-rule preconds <> expr env) - (theorem-rules thm sys)) => result/expr) + (theorem-rules thm)) => result/expr) (else (result/error 'apply-theorem cmd-name expr))))))) -(define (rewrite/core-function sys f expr) +(define (rewrite/core-function f expr) (if (and (app-form? expr) (eq? (get-name f) (app-form-name expr)) (= (length (get-variables f)) (length (app-form-args expr))) @@ -857,7 +854,7 @@ (map expr-unquote (app-form-args expr))))) (result/error 'apply-core-function (get-name f) expr))) -(define (rewrite/function sys fname f expr) +(define (rewrite/function fname f expr) (cond ((any (cut apply-rule '() <> expr '()) (function->rules f)) @@ -865,7 +862,7 @@ (else (result/error 'apply-function fname expr)))) -(define (rewrite1 sys expr r) +(define (rewrite1 expr r) (call/cc (lambda (k) (define (fail . args) @@ -881,7 +878,7 @@ (extract path expr fail) (result/expr (builder - (result->expr (rewrite/eval extracted-expr sys)))))) + (result->expr (rewrite/eval extracted-expr)))))) #; (('induction path (fname vars ...)) (receive (extracted-expr preconds builder) @@ -897,20 +894,20 @@ (builder (result->expr (cond - ((lookup cmd-name sys) + ((lookup cmd-name (current-system)) => (lambda (x) (cond ((is-a? x <core-function>) - (rewrite/core-function sys x extracted-expr)) + (rewrite/core-function x extracted-expr)) ((is-a? x <theorem*>) - (rewrite/theorem cmd-name cmd-ops sys x preconds extracted-expr sys)) + (rewrite/theorem cmd-name cmd-ops x preconds extracted-expr)) ((is-a? x <expandable-function>) - (rewrite/function sys cmd-name x extracted-expr)) + (rewrite/function cmd-name x extracted-expr)) (else (result/error 'invalid-command cmd-name extracted-expr))))) (else (result/error 'command-not-found cmd-name extracted-expr)))))))))))) -(define (rewrite sys expr seq) +(define (rewrite expr seq) (let loop ((result (result/expr expr)) (seq seq)) (cond @@ -918,8 +915,7 @@ ((result/expr? result) (if (null? seq) result - (loop (rewrite1 sys - (result/expr-expr result) + (loop (rewrite1 (result/expr-expr result) (car seq)) (cdr seq)))) (else (result/error 'invalid-result result))))) @@ -933,10 +929,10 @@ (('not expr) expr) (expr (expr-not expr)))) -(define (expr-equal? x sys) +(define (expr-equal? x) (and (list? x) (= 3 (length x)) - (eq? (get-equal-symbol sys) (list-ref x 0)) + (eq? (get-equal-symbol (current-system)) (list-ref x 0)) (expression? (list-ref x 1)) (expression? (list-ref x 2)))) @@ -946,25 +942,22 @@ (define (expr-equal-rhs x) (list-ref x 2)) -(define (expression->rules vars preconds expr sys) +(define (expression->rules vars preconds expr) (if (if-form? expr) (append (expression->rules vars (cons (prop-not (prop-not (if-form-test expr))) preconds) - (if-form-then expr) - sys) + (if-form-then expr)) (expression->rules vars (cons (prop-not (if-form-test expr)) preconds) - (if-form-else expr) - sys) + (if-form-else expr)) (expression->rules vars preconds - (if-form-test expr) - sys)) - (if (expr-equal? expr sys) + (if-form-test expr))) + (if (expr-equal? expr) (list (rule vars preconds (expr-equal-lhs expr) @@ -1009,9 +1002,9 @@ (validate t) t)))))) -(define (add-guard-theorem name sys) +(define (add-guard-theorem name) (cond - ((lookup name sys) + ((lookup name (current-system)) => (lambda (f) (if (is-a? f <expandable-function>) (add-definition (make <conjecture> @@ -1019,10 +1012,9 @@ #:variables (get-variables f) #:expression (fold smart-implies (make-guard-claim - (get-expression f) - sys) + (get-expression f)) (get-guards f))) - sys) + (current-system)) (raise-exception (make-exception (make-exception-with-origin 'define-guard-theorem) @@ -1038,7 +1030,7 @@ (define-syntax define-guard-theorem (syntax-rules () ((_ name) - (current-system (add-guard-theorem 'name (current-system)))))) + (current-system (add-guard-theorem 'name))))) (define-syntax define-core-function/guard (syntax-rules (and) @@ -1247,7 +1239,7 @@ (else (smart-if x y ''#t)))) -(define (make-totality-claim* sys m-expr f) +(define (make-totality-claim* m-expr f) (let* ((name (get-name f))) (define (convert app-form) (cond @@ -1263,7 +1255,7 @@ (get-name f) m-expr app-form)))) - (smart-if `(,(get-measure-predicate sys) ,m-expr) + (smart-if `(,(get-measure-predicate (current-system)) ,m-expr) (let loop ((expr (get-expression f))) (cond ((expr-quoted? expr) ''#t) @@ -1284,7 +1276,7 @@ (else (smart-and (loop (car args)) (f (cdr args)))))))) (if (eq? name (app-form-name expr)) - (smart-and `(,(get-measure-less-than sys) + (smart-and `(,(get-measure-less-than (current-system)) ,(convert expr) ,m-expr) rest) @@ -1294,12 +1286,12 @@ m-expr)))) ''#f))) -(define (make-guard-claim expr sys) +(define (make-guard-claim expr) (define (find-preconds expr) (cond ((app-form? expr) (let ((rest (append-map find-preconds (cdr expr)))) - (append (cond ((lookup (car expr) sys) => + (append (cond ((lookup (car expr) (current-system)) => (lambda (f) (let ((preconds (get-guards f))) (map (lambda (precond) @@ -1389,14 +1381,14 @@ (else (error "make-induction-claim: invalid" f vars c)))) -(define (validate-sequence sys d seq) +(define (validate-sequence d seq) (for-each (lambda (r) (match r (('rewrite _ _ . command-ops) (for-each (lambda (x) (match x (('= var expr) - (validate-expression sys + (validate-expression `(define-proof ,(get-name d)) (get-variables d) expr)) @@ -1405,7 +1397,7 @@ (else #f))) seq)) -(define (add-proof/function sys f seed seq) +(define (add-proof/function f seed seq) (define (update-claim claim) (update-definition (make <total-function> #:name (get-name f) @@ -1415,17 +1407,16 @@ #:code (get-code f) #:claim claim #:proof seq) - sys)) - (validate-sequence sys f seq) + (current-system))) + (validate-sequence f seq) (if seed (begin - (validate-expression sys - `(defien-proof ,(get-name f)) + (validate-expression `(defien-proof ,(get-name f)) (get-variables f) seed) (update-claim (fold smart-implies - (make-totality-claim* sys seed f) + (make-totality-claim* seed f) (get-guards f)))) (raise-exception (make-exception @@ -1433,20 +1424,20 @@ (make-exception-with-message "need measure expression") (make-exception-with-irritants (get-expression f)))))) -(define (add-proof/theorem sys t seed seq) +(define (add-proof/theorem t seed seq) (define (seed-error m) (raise-exception (make-exception (make-exception-with-origin 'define-proof) (make-exception-with-message (string-append "invalid seed: " m)) (make-exception-with-irritants (list (get-name t) seed))))) - (validate-sequence sys t seq) + (validate-sequence t seq) (let ((claim (if seed (match seed ((fname vars ...) (cond - ((lookup fname sys) + ((lookup fname (current-system)) => (cut make-induction-claim <> vars (get-expression t))) (else (seed-error "function not found")))) (else (seed-error "format error"))) @@ -1457,9 +1448,9 @@ #:expression (get-expression t) #:claim claim #:proof seq) - sys))) + (current-system)))) -(define (add-proof sys name seed seq) +(define (add-proof name seed seq) (cond ((not (sequence? seq)) (raise-exception @@ -1467,16 +1458,16 @@ (make-exception-with-origin 'define-proof) (make-exception-with-message "not sequence") (make-exception-with-irritants seq)))) - ((lookup name sys) + ((lookup name (current-system)) => (lambda (def) (current-system (if (and (is-a? def <provable>) (not (is-a? def <proved>))) (cond ((is-a? def <function>) - (add-proof/function sys def seed seq)) + (add-proof/function def seed seq)) ((is-a? def <conjecture>) - (add-proof/theorem sys def seed seq)) + (add-proof/theorem def seed seq)) (else (raise-exception (make-exception @@ -1500,24 +1491,23 @@ ((_ name seed seq) - (add-proof (current-system) - 'name + (add-proof 'name 'seed 'seq)) ((_ name seq) (define-proof name #f seq)))) -(define (validate-expression/error sys name vars expr) +(define (validate-expression/error name vars expr) (with-exception-handler (lambda (e) (if (eq? 'validate-expression/error (exception-origin e)) `(error ,name ,vars ,expr)) (raise-exception e)) (lambda () - (validate-expression sys 'validate-expression/error vars expr) + (validate-expression 'validate-expression/error vars expr) #f))) -(define (validate-expression sys name vars expr) +(define (validate-expression name vars expr) (let* ((expr-fnames (expression-functions expr)) (expr-vars (expression-vars expr)) (expr-app-forms (expression-app-forms expr))) @@ -1533,7 +1523,7 @@ vars) (for-each (lambda (fname) (unless (cond - ((lookup fname sys) => + ((lookup fname (current-system)) => (lambda (f) (for-each (lambda (app-form) @@ -1612,21 +1602,22 @@ #f))) (get-definitions sys))) -(define (system-check/guard sys) +(define (system-check/guard) (filter-map (lambda (f) - (if (lookup `(guard ,(get-name f)) sys) + (if (lookup `(guard ,(get-name f)) (current-system)) #f - (if (equal? (make-guard-claim (get-expression f) sys) + (if (equal? (make-guard-claim (get-expression f)) ''#t) #f `((guard ,(get-name f)) (add (define-guard-theorem ,(get-name f))))))) (filter (cut is-a? <> <expandable-function>) - (get-definitions sys)))) + (get-definitions (current-system))))) (define (system-check sys) (append - (system-check/guard sys) + (parameterize ((current-system sys)) + (system-check/guard)) (let loop ((sys sys) (fails '())) (if (system-empty? sys) @@ -1642,12 +1633,12 @@ ((is-a? d <proved>) (let ((result (if (is-a? d <theorem>) - (rewrite sys-without-first - (get-claim d) - (get-proof d)) - (rewrite sys - (get-claim d) - (get-proof d))))) + (parameterize ((current-system sys-without-first)) + (rewrite (get-claim d) + (get-proof d))) + (parameterize ((current-system sys)) + (rewrite (get-claim d) + (get-proof d)))))) (cond ((equal? result (result/expr ''#t)) (next)) @@ -1666,4 +1657,5 @@ (else #f))) (define/guard (system-rewrite (sys system?) (expr (const #t)) (seq sequence?)) - (rewrite sys (convert-to-expression expr) seq)) + (parameterize ((current-system sys)) + (rewrite (convert-to-expression expr) seq))) |