diff options
Diffstat (limited to 'vikalpa.scm')
| -rw-r--r-- | vikalpa.scm | 213 |
1 files changed, 124 insertions, 89 deletions
diff --git a/vikalpa.scm b/vikalpa.scm index e7126f8..771c623 100644 --- a/vikalpa.scm +++ b/vikalpa.scm @@ -19,6 +19,7 @@ (define-module (vikalpa) #:export (rewrite describe + system? system-check system-apropos system-code @@ -36,12 +37,10 @@ #:use-module (ice-9 exceptions) #:use-module (ice-9 regex) #:use-module ((srfi srfi-1) - #:select (every any member lset-union fold append-map - find)) + #:select (every any lset-union fold append-map find)) #:use-module (srfi srfi-8) #:use-module (srfi srfi-11) #:use-module (srfi srfi-26) - #:use-module (ice-9 pretty-print) #:use-module (oop goops)) (define-class <system> () @@ -85,8 +84,6 @@ (define-class <total-function> (<expandable-function> <proved>)) (define-class <trivial-total-function> (<expandable-function>)) -(define-generic macro-mrules) -(define-generic macro-literals) (define-class <macro> (<definition>) (mrules #:getter macro-mrules #:init-keyword #:mrules) (literals #:getter macro-literals #:init-keyword #:literals)) @@ -123,25 +120,21 @@ (define-method (write (d <total-function>) port) (write-definition 'total-function d port)) -(define-generic lookup) (define-method (lookup (name <symbol>) (s <system>)) (find (lambda (x) (eq? name (get-name x))) (get-definitions s))) -(define-generic update-measure-predicate) (define-method (update-measure-predicate (s <symbol>) (sys <system>)) (let ((new (shallow-clone sys))) (slot-set! new 'measure-predicate s) new)) -(define-generic update-measure-less-than) (define-method (update-measure-less-than (s <symbol>) (sys <system>)) (let ((new (shallow-clone sys))) (slot-set! new 'measure-less-than s) new)) -(define-generic update-definition) (define-method (update-definition (d <definition>) (sys <system>)) (define (update d defs) (if (null? defs) @@ -157,21 +150,19 @@ (slot-set! new 'definitions (update d (get-definitions sys))) new)) -(define-generic remove-first-definition) + (define-method (remove-first-definition (sys <system>)) (let ((new (shallow-clone sys))) (slot-set! new 'definitions (cdr (get-definitions sys))) new)) -(define-generic first-definition) + (define-method (first-definition (sys <system>)) (car (get-definitions sys))) -(define-generic system-empty?) (define-method (system-empty? (sys <system>)) (null? (get-definitions sys))) -(define-generic add-definition) (define-method (add-definition (d <definition>) (s <system>)) (if (lookup (get-name d) s) (raise-exception @@ -179,12 +170,17 @@ (make-exception-with-origin 'add-definition) (make-exception-with-message "duplicated definition") (make-exception-with-irritants (get-name d)))) - (let ((new (shallow-clone s))) - (slot-set! new 'definitions - (cons d (get-definitions s))) - new))) + (if (reserved? (get-name d)) + (raise-exception + (make-exception + (make-exception-with-origin 'add-definition) + (make-exception-with-message "reserved name") + (make-exception-with-irritants (get-name d)))) + (let ((new (shallow-clone s))) + (slot-set! new 'definitions + (cons d (get-definitions s))) + new)))) -(define-generic validate) (define-method (validate (d <definition>)) (let* ((vars (get-variables d)) (name (get-name d))) @@ -510,15 +506,12 @@ => (cut substitute <> (rule-rhs rl))) (else #f))) -(define-type code - code - (0 code?) - (1 (const #t) - expr - code-expr)) +(define (code x) + (list 'code x)) + +(define (code-expr x) + (cadr x)) -(define-generic mrule-lhs) -(define-generic mrule-rhs) (define-class <mrule> () (lhs #:getter mrule-lhs #:init-keyword #:lhs) (rhs #:getter mrule-rhs #:init-keyword #:rhs)) @@ -835,10 +828,11 @@ (receive (env) (parse-options/theorem (cdr ops) fail) (case (caar ops) - ((set) (let ((op (car ops))) - (cons (cons (list-ref op 1) - (list-ref op 2)) - env))) + ((set) + (let ((op (car ops))) + (cons (cons (list-ref op 1) + (list-ref op 2)) + env))) (else (fail 'invalid-option (car ops))))))) @@ -992,37 +986,27 @@ (define-syntax define-function (syntax-rules () - ((_ name (var ...) precond ... expr) - (let ((f (make <function> - #:name 'name - #:variables '(var ...) - #:conditions '(precond ...) - #:expression (convert-to-expression 'expr) - #:code (code 'expr)))) - (current-system (add-definition f (current-system))) - (validate f) - f)))) - -(define-syntax define-function/no-code - (syntax-rules () - ((_ name (var ...) precond ... expr) - (let ((f (make <function> - #:name 'name - #:variables '(var ...) - #:conditions '(precond ...) - #:expression (convert-to-expression 'expr) - #:code (code 'expr)))) + ((_ name (var ...) expr) + (let ((f (let ((expression (convert-to-expression 'expr))) + (make (if (member 'name (expression-functions expression)) + <function> + <trivial-total-function>) + #:name 'name + #:variables '(var ...) + #:conditions '() + #:expression expression + #:code (code 'expr))))) (current-system (add-definition f (current-system))) (validate f) f)))) (define-syntax define-trivial-total-function (syntax-rules () - ((_ name (var ...) precond ... expr) + ((_ name (var ...) expr) (let ((f (make <trivial-total-function> #:name 'name #:variables '(var ...) - #:conditions '(precond ...) + #:conditions '() #:expression (convert-to-expression 'expr) #:code (code 'expr)))) (current-system (add-definition f (current-system))) @@ -1039,10 +1023,16 @@ (current-system (add-definition m (current-system))) m)))) +(define* (core-system #:optional (parent (make <system>))) + (parameterize ((current-system parent)) + (define-core-function not (x) not) + (define-core-function equal? (x y) equal?) + (current-system))) + (define-syntax define-system (syntax-rules () ((_ name (systems ...) expr ...) - (define* (name #:optional (parent (make <system>))) + (define* (name #:optional (parent (core-system))) (parameterize ((current-system ((compose systems ... identity) parent))) expr @@ -1113,6 +1103,16 @@ (if/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 @@ -1159,7 +1159,7 @@ m-expr)))) ''#f))) -(define (make-guard-claim expr sys) +(define (make-condition-claim expr sys) (define (find-preconds expr) (cond ((app-form? expr) @@ -1173,7 +1173,7 @@ (cdr expr)) precond)) preconds)))) - (else (error "make-guard-claim: error"))) + (else (error "make-condition-claim: error"))) rest))) ((if-form? expr) (find-preconds (if-form-test expr))) @@ -1247,17 +1247,36 @@ (else (error "make-induction-claim: invalid" f vars c)))) +(define (validate-sequence sys d seq) + (for-each (lambda (r) + (for-each (lambda (x) + (match x + (('set var expr) + (validate-expression sys + `(define-proof ,(get-name d)) + (get-variables d) + expr)) + (else #f))) + (rewriter-command r))) + seq)) + (define (add-proof/function sys f seed seq) + (validate-sequence sys f seq) (if seed - (update-definition (make <total-function> - #:name (get-name f) - #:variables (get-variables f) - #:conditions (get-conditions f) - #:expression (get-expression f) - #:code (get-code f) - #:claim (make-totality-claim* sys seed f) - #:proof seq) - sys) + (begin + (validate-expression sys + `(defien-proof ,(get-name f)) + (get-variables f) + seed) + (update-definition (make <total-function> + #:name (get-name f) + #:variables (get-variables f) + #:conditions (get-conditions f) + #:expression (get-expression f) + #:code (get-code f) + #:claim (make-totality-claim* sys seed f) + #:proof seq) + sys)) (raise-exception (make-exception (make-exception-with-origin 'define-proof) @@ -1265,13 +1284,32 @@ (make-exception-with-irritants (get-expression f)))))) (define (add-proof/theorem sys t seed seq) + (validate-sequence sys t seq) (let ((claim - (match seed - ((fname . vars) - (cond ((lookup fname sys) - => (cut make-induction-claim <> vars (get-expression t))) - (else (get-expression t)))) - (else (get-expression t))))) + (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) @@ -1328,6 +1366,16 @@ ((_ name seq) (define-proof name #f seq)))) +(define (validate-expression/error sys 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) + #f))) + (define (validate-expression sys name vars expr) (let* ((expr-fnames (expression-functions expr)) (expr-vars (expression-vars expr)) @@ -1384,12 +1432,6 @@ (when (dup? vars) (err))) -(define (recur? f) - (member (get-name f) - (expression-functions (get-expression f)))) - -(define (trivial-total? f sys) - (and (not (recur? f)))) (define/guard (system-apropos (sys system?) (str string?)) (filter (lambda (name) @@ -1399,7 +1441,7 @@ (symbol->string name))) (map get-name (get-definitions sys)))) -(define (system-code sys) +(define/guard (system-code (sys system?)) `(begin ,@(map (lambda (f) `(define (,(get-name f) ,@(get-variables f)) @@ -1409,7 +1451,7 @@ (get-code x))) (get-definitions sys)))))) -(define (check sys) +(define (system-check sys) (let loop ((sys sys) (fails '())) (if (system-empty? sys) @@ -1469,15 +1511,7 @@ (define/guard (system-load (sys system?)) (primitive-eval (system-code sys))) -;; (define/guard (system-environment (sys system?)) -;; (map (lambda (def) -;; (list (get-name def) -;; (show sys name))) -;; (get-definitions sys))) - (define-system prelude () - (define-core-function not (x) not) - (define-core-function equal? (x y) equal?) (define-core-function natural? (x) (lambda (x) (and (integer? x) (< 0 x)))) @@ -1586,6 +1620,9 @@ (define-theorem caar-cons2 (x y z) (equal? (car (car (cons (cons x y) z))) x)) + + (define-function double (x) + (+ x x)) (define-function app (x y) (if (not (pair? x)) @@ -1611,6 +1648,4 @@ (define-proof assoc-app (list-induction x) - ()) - ) - + ())) |