diff options
Diffstat (limited to 'vikalpa.scm')
| -rw-r--r-- | vikalpa.scm | 208 |
1 files changed, 123 insertions, 85 deletions
diff --git a/vikalpa.scm b/vikalpa.scm index 79f6fb1..3d5e3e5 100644 --- a/vikalpa.scm +++ b/vikalpa.scm @@ -30,10 +30,14 @@ define-core-function define-core-function/guard define-function + define-function define-function/guard + define-axiom-function + define-axiom-function/guard define-syntax-rules define-axiom - define-theorem) + define-theorem + admit) #:use-module (ice-9 match) #:use-module (ice-9 format) #:use-module (ice-9 control) @@ -69,6 +73,7 @@ (define-class <proved> (<provable>) (claim #:getter get-claim #:init-keyword #:claim) (proof #:getter get-proof #:init-keyword #:proof)) +(define-class <admitted> ()) (define-class <theorem*> (<definition>) (expression #:getter get-expression #:init-keyword #:expression)) @@ -86,6 +91,7 @@ (code #:getter get-code #:init-keyword #:code)) (define-class <function> (<expandable-function> <provable>)) (define-class <total-function> (<expandable-function> <proved>)) +(define-class <admitted-function> (<expandable-function> <proved> <admitted>)) (define-class <macro> (<definition>) (mrules #:getter macro-mrules #:init-keyword #:mrules) @@ -719,6 +725,10 @@ (command-name? command-name) (every command-option? command-ops))) (('eval path) (path? path)) + (('induction path (fname vars ...)) + (and (path? path) + (symbol? fname) + (every variable? vars))) (else #f))) ;; (sequence? x) -> boolean? @@ -835,12 +845,6 @@ (else (result/error 'apply-theorem cmd-name expr))))))) -(define (rewrite/induction sys fname vars expr fail) - (cond - ((lookup fname sys) - => (cut make-induction-claim <> vars expr)) - (else (fail 'induction 'not-found fname)))) - (define (rewrite/core-function sys f expr) (if (and (app-form? expr) (eq? (get-name f) (app-form-name expr)) @@ -851,6 +855,30 @@ (map expr-unquote (app-form-args expr))))) (result/error 'apply-core-function (get-name f) expr))) +(define (rewrite/function sys fname f expr) + (cond + ((any (cut apply-rule '() <> expr '()) + (function->rules f)) + => result/expr) + (else + (result/error 'apply-function fname expr)))) + +(define (rewrite/induction sys fname vars ps expr) + (cond + ((lookup fname sys) + => (lambda (f) + (cond + ((not (is-a? f <expandable-function>)) + (result/error 'induction 'not-expandable-function fname expr)) + ((apply-rule ps + (make-induction-rule f vars expr) + expr + '()) + => result/expr) + (else + (result/error 'induction 'error fname expr))))) + (else (result/error 'induction 'not-found fname expr)))) + (define (rewrite1 sys expr r) (call/cc (lambda (k) @@ -868,6 +896,13 @@ (result/expr (builder (result->expr (rewrite/eval extracted-expr sys)))))) + (('induction path (fname vars ...)) + (receive (extracted-expr preconds builder) + (extract path expr fail) + (result/expr + (builder + (result->expr + (rewrite/induction sys fname vars preconds extracted-expr)))))) (('rewrite path cmd-name cmd-ops ...) (receive (extracted-expr preconds builder) (extract path expr fail) @@ -883,13 +918,7 @@ ((is-a? x <theorem*>) (rewrite/theorem cmd-name cmd-ops sys x preconds extracted-expr)) ((is-a? x <expandable-function>) - (cond - ((any (cut apply-rule '() <> extracted-expr '()) - (function->rules x)) - => result/expr) - (else - (result/error 'apply-function cmd-name extracted-expr)))) - + (rewrite/function sys cmd-name x extracted-expr)) (else (result/error 'invalid-command cmd-name extracted-expr))))) (else (result/error 'command-not-found cmd-name extracted-expr)))))))))))) @@ -1058,6 +1087,35 @@ (current-system (add-definition m (current-system))) m)))) +(define-syntax admit + (syntax-rules (and) + ((_ name) + (cond + ((lookup 'name (current-system)) + => (lambda (f) + (unless (is-a? f <function>) + (raise-exception + (make-exception + (make-exception-with-origin 'name) + (make-exception-with-message "not provable definition") + (make-exception-with-irritants 'name)))) + (let ((g (make <admitted-function> + #:name (get-name f) + #:variables (get-variables f) + #:guards (get-guards f) + #:expression (get-expression f) + #:code (get-code f) + #:claim ''#t + #:proof '()))) + (validate g) + (current-system (update-definition g (current-system)))))) + (else + (raise-exception + (make-exception + (make-exception-with-origin 'name) + (make-exception-with-message "not found") + (make-exception-with-irritants 'name)))))))) + (define* (core-system #:optional (parent (make <system>))) (parameterize ((current-system parent)) (define-syntax-rules and () @@ -1148,16 +1206,6 @@ (smart-if x y ''#t)))) (define (make-totality-claim* sys m-expr f) - (unless (get-measure-predicate sys) - (raise-exception - (make-exception - (make-exception-with-origin `(define-proof ,(get-name f))) - (make-exception-with-message "measure-predicate is not found")))) - (unless (get-measure-less-than sys) - (raise-exception - (make-exception - (make-exception-with-origin `(define-proof ,(get-name f))) - (make-exception-with-message "measure-less-than is not found")))) (let* ((name (get-name f))) (define (convert app-form) (cond @@ -1249,7 +1297,14 @@ ''#t ''#f)) -(define (make-induction-claim f vars c) +(define (make-induction-rule f vars c) + (unless (is-a? f <proved>) + (raise-exception + (make-exception + (make-exception-with-origin 'define-proof) + (make-exception-with-message + "measure function must be proved function") + (make-exception-with-irritants (get-name f))))) (define (find-app-forms expr) (cond ((app-form? expr) @@ -1273,24 +1328,28 @@ => identity) (else (error "make-induction-claim: fail" app-form)))) - (cond - ((apply-function f vars) - => (lambda (expr) - (let build ((expr expr)) - (cond - ((if-form? expr) - (let ((app-forms (find-app-forms (if-form-test 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 smart-implies c (map prop app-forms)))))))) - (else (error "make-induction-claim: invalid" - f vars c)))) + (define rhs + (cond + ((apply-function f vars) + => (lambda (expr) + (let build ((expr expr)) + (cond + ((if-form? expr) + (let ((app-forms (find-app-forms (if-form-test 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 smart-implies c (map prop app-forms)))))))) + (else (error "make-induction-claim: invalid" + f vars c)))) + (rule vars (get-guards f) c rhs)) (define (validate-sequence sys d seq) (for-each (lambda (r) @@ -1345,38 +1404,13 @@ (define (add-proof/theorem sys t seed seq) (validate-sequence sys t seq) - (let ((claim - (if seed - (begin - (validate-expression sys - `(define-proof ,(get-name t)) - (get-variables t) - seed) - (match seed - ((fname . vars) - (cond - ((lookup fname sys) - => (cut make-induction-claim <> vars (get-expression t))) - (else - (raise-exception - (make-exception - (make-exception-with-origin 'add-proof/theorem) - (make-exception-with-message "error") - (make-exception-with-irritants seed)))))) - (else - (raise-exception - (make-exception - (make-exception-with-origin `(define-proof ,(get-name t))) - (make-exception-with-message "invalid induction form") - (make-exception-with-irritants seed)))))) - (get-expression t)))) - (update-definition (make <theorem> - #:name (get-name t) - #:variables (get-variables t) - #:expression (get-expression t) - #:claim claim - #:proof seq) - sys))) + (update-definition (make <theorem> + #:name (get-name t) + #:variables (get-variables t) + #:expression (get-expression t) + #:claim (get-expression t) + #:proof seq) + sys)) (define (add-proof sys name seed seq) (cond @@ -1498,6 +1532,7 @@ (define-method (get-type (s <core-function>)) 'core-function) (define-method (get-type (s <function>)) 'function) (define-method (get-type (s <total-function>)) 'total-function) +(define-method (get-type (s <admitted-function>)) 'admitted-function) (define-method (get-type (s <macro>)) 'macro) (define-method (show (d <macro>)) @@ -1513,21 +1548,24 @@ (list (get-type d) (get-variables d) (get-expression d))) +(define-method (show (d <admitted-function>)) + (list (get-type d) + (get-variables d) + (get-expression d))) (define* (system-apropos sys str #:key all?) (filter-map (lambda (d) - (if (and (or all? - (not (string-match "^%" - (symbol->string - (get-name d))))) - (string-match (string-append ".*" - (regexp-quote str) - ".*") - (symbol->string (get-name d)))) - (list (get-name d) (show d)) - #f)) + (let ((name (format #f "~a" (get-name d)))) + (if (and (or all? + (not (string-match "^%" name))) + (string-match (string-append ".*" + (regexp-quote str) + ".*") + name)) + (list (get-name d) (show d)) + #f))) (get-definitions sys))) (define (system-check sys) |