diff options
| -rw-r--r-- | vikalpa.scm | 1013 |
1 files changed, 568 insertions, 445 deletions
diff --git a/vikalpa.scm b/vikalpa.scm index 1b3c158..bff63f0 100644 --- a/vikalpa.scm +++ b/vikalpa.scm @@ -52,69 +52,159 @@ #:use-module (oop goops)) (define-class <system> () - (definitions #:getter system-definitions #:init-keyword #:definitions) - (total-cliam-method #:getter system-total-claim-method - #:init-keyword #:total-cliam-method)) + (definitions + #:getter get-definitions + #:init-keyword #:definitions + #:init-value '()) + (natural-predicate #:getter get-natural-predicate + #:init-value #f) + (natural-less-than #:getter get-natural-less-than + #:init-value #f) + (ordinal-predicate #:getter get-ordinal-predicate + #:init-value #f) + (ordinal-less-than #:getter get-ordinal-less-than + #:init-value #f)) (define-class <definition> () - (name #:getter definition-name #:init-keyword #:name)) + (name #:getter get-name + #:init-keyword #:name) + (variables #:getter get-variables + #:init-keyword #:variables + #:init-value '())) -(define-class <condition> () - (expressions #:getter condition-expressions #:init-keyword #:expressions)) - -(define-class <function> (<definition>) - (variables #:getter function-variables #:init-keyword #:variables) - (condition #:getter function-condition #:init-keyword #:condition)) +(define-class <provable> ()) -(define-class <total-function> ()) +(define-class <proved> (<provable>) + (claim #:getter get-claim #:init-keyword #:claim) + (proof #:getter get-proof #:init-keyword #:proof)) -(define-class <core-function> (<function>) - (procedure #:getter core-function-procedure #:init-keyword #:procedure)) +(define-class <theorem*> (<definition>) + (expression #:getter get-expression #:init-keyword #:expression)) -(define-class <defined-function> (<function>) - (expression #:getter defined-function-expression #:init-keyword #:expression) - (code #:getter defined-function-code #:init-keyword #:code)) +(define-class <conjecture> (<theorem*> <provable>)) +(define-class <theorem> (<theorem*> <proved>)) +(define-class <axiom> (<theorem*>)) -(define-class <total-function> (<defined-function>) - (proof #:getter theorem-proof #:init-keyword #:proof)) +(define-class <condition> () + (expressions #:getter get-expressions #:init-keyword #:expressions)) -(define-class <primitive-function> (<defined-function>)) +(define-class <function*> (<definition>) + (condition #:getter get-condition #:init-keyword #:condition)) +(define-class <core-function> (<function*>) + (procedure #:getter get-procedure #:init-keyword #:procedure)) +(define-class <expandable-function> (<function*>) + (expression #:getter get-expression #:init-keyword #:expression) + (code #:getter get-code #:init-keyword #:expressions)) +(define-class <function> (<expandable-function> <provable>)) +(define-class <total-function> (<expandable-function> <proved>)) +(define-class <trivial-total-function> (<expandable-function>)) -(define-generic total-function?) -(define-method (total-function? x) - (or (is-a? x <core-function>) - (is-a? x <primitive-function>) - (is-a? x <total-function>))) +(define (write-definition sym d port) + (format port "#<~a: ~s>" + sym (cons (get-name d) (get-variables d)))) -(define-class <proposition> (<definition>) - (variables #:getter proposition-variables #:init-keyword #:variables) - (expression #:getter proposition-expression #:init-keyword #:expression)) +(define-method (display (d <definition>) port) + (write d port)) -(define-class <conjecture> (<proposition>)) -(define-class <theorem> (<proposition>) - (proof #:getter theorem-proof #:init-keyword #:proof)) -(define-class <axiom> (<theorem>)) +(define-method (write (s <system>) port) + (format port "#<system: function: ~a theorem: ~a macro: ~a>" + (length (filter (cut is-a? <> <function*>) + (get-definitions s))) + (length (filter (cut is-a? <> <theorem*>) + (get-definitions s))) + (length (filter (cut is-a? <> <macro>) + (get-definitions s))))) -(define (theorem? x) - (or (is-a? x <theorem>) - (is-a? x <axiom>))) +(define-method (write (d <conjecture>) port) + (write-definition 'conjecture d port)) +(define-method (write (d <theorem>) port) + (write-definition 'theorem d port)) +(define-method (write (d <axiom>) port) + (write-definition 'axiom d port)) +(define-method (write (d <axiom>) port) + (write-definition 'axiom d port)) +(define-method (write (d <function>) port) + (write-definition 'function d port)) +(define-method (write (d <core-function>) port) + (write-definition 'function d port)) +(define-method (write (d <trivial-total-function>) port) + (write-definition 'trivial-total-function d port)) +(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 (definition-name x))) - (system-definitions s))) + (find (lambda (x) + (eq? name (get-name x))) + (get-definitions s))) + +(define-generic update-natural-predicate) +(define-method (update-natural-predicate (s <symbol>) (sys <system>)) + (let ((new (shallow-clone sys))) + (slot-set! new 'natural-predicate s) + new)) + +(define-generic update-natural-less-than) +(define-method (update-natural-less-than (s <symbol>) (sys <system>)) + (let ((new (shallow-clone sys))) + (slot-set! new 'natural-less-than s) + new)) + +(define-generic update-ordinal-predicate) +(define-method (update-ordinal-predicate (s <symbol>) (sys <system>)) + (let ((new (shallow-clone sys))) + (slot-set! new 'ordinal-predicate s) + new)) + +(define-generic update-ordinal-less-than) +(define-method (update-ordinal-less-than (s <symbol>) (sys <system>)) + (let ((new (shallow-clone sys))) + (slot-set! new 'ordinal-less-than-function s) + new)) + +(define-generic update-definition) +(define-method (update-definition (d <definition>) (sys <system>)) + (let ((new (shallow-clone sys))) + (slot-set! new 'definitions + (cons d (get-definitions sys))) + new)) + +(define-generic update-definition) +(define-method (update-definition (d <definition>) (sys <system>)) + (let ((new (shallow-clone sys))) + (slot-set! new 'definitions + (cons d (get-definitions sys))) + new)) (define-generic add-definition) (define-method (add-definition (d <definition>) (s <system>)) - (if (lookup (definition-name d) s) + (if (lookup (get-name d) s) (raise-exception (make-exception (make-exception-with-message "(vikalpa) add-definition: duplicated definition") - (make-exception-with-irritants (definition-name s)))) - (make <system> - #:definitions (cons d (system-definitions s)) - #:total-cliam-method (system-total-claim-method s)))) + (make-exception-with-irritants (get-name d)))) + (update-definition d s))) + +(define-generic validate) +(define-method (validate (d <definition>)) + (let* ((vars (get-variables d)) + (name (get-name d))) + (validate-vars (symbol->string name) vars))) + +(define-method (validate (d <expandable-function>)) + (let* ((vars (get-variables d)) + (name (get-name d)) + (expr (get-expression d))) + (validate-expression (current-system) 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) + (next-method))) (define (debug f . args) (if #f @@ -217,6 +307,19 @@ (define (if-form-else expr) (list-ref expr 3)) +(define (expression-app-forms expr) + (cond + ((if-form? expr) + (append-map expression-app-forms + (list (if-form-test expr) + (if-form-then expr) + (if-form-else expr)))) + ((app-form? expr) + (cons expr + (append-map expression-app-forms + (app-form-args expr)))) + (else '()))) + (define (expression-functions expr) (cond ((if-form? expr) @@ -433,18 +536,18 @@ (else '()))) (all-vars (mrule-lhs mrl))) -(define-type macro - macro - (1 macro?) - (0 variable? name macro-name) - (2 (lambda (mrls) - (and (list? mrls) - (every mrule? mrls))) - mruls - macro-mrules) - (3 (list-of symbol?) - literals - macro-literals)) +(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)) + +(define (macro name mrules literals) + (make <macro> + #:name name + #:variables '() + #:mrules mrules + #:literals literals)) (define (apply-mrule rl ls expr) (define (literal? x) @@ -504,7 +607,7 @@ (define (apply-macro m expr) (cond ((and (pair? expr) - (eq? (macro-name m) (car expr))) + (eq? (get-name m) (car expr))) (let loop ((rs (macro-mrules m))) (cond ((null? rs) (error "(vikalpa) macro fail" m expr)) @@ -585,7 +688,8 @@ (define (convert-to-expression x) (quote-all - (expand* (filter macro? (system-definitions (current-system))) + (expand* (filter (cut is-a? <> <macro>) + (get-definitions (current-system))) (expand-let x)))) (define (vars? x) @@ -593,9 +697,9 @@ (every variable? x))) (define (theorem-rules x) - (expression->rules (theorem-variables x) + (expression->rules (get-variables x) '() - (theorem-expression x))) + (get-expression x))) (define (rewrite/eval expr sys) (let eval ((expr expr)) @@ -608,7 +712,7 @@ (eval (rewrite1 sys `(,name ,@args) (lambda args - (cons* 'error rewrite name args)) + (cons* 'error 'rewrite name args)) (rewriter '() `(,name))))))) ((if-form? expr) (let ((test (eval (if-form-test expr)))) @@ -673,10 +777,10 @@ (define (command-options x) (cdr x)) -;; (define/guard (system-eval (expr (const #t)) (sys system?)) -;; (rewrite/eval (parameterize ((current-system sys)) -;; (convert-to-expression expr)) -;; sys)) +(define/guard (system-eval (expr (const #t)) (sys (cut is-a? <> <system>))) + (rewrite/eval (parameterize ((current-system sys)) + (convert-to-expression expr)) + sys)) ;; (extract path? expression? preconds? procedure?) -> (values expression? procedure?) (define (extract path expr fail) @@ -712,22 +816,22 @@ (fail 'invalid-path path)))))) (define (function->rules x) - (list (rule (function-variables x) - (condition-expressions (function-condition x)) - (function-app-form x) - (defined-function-expression x)) - (rule (function-variables x) - (condition-expressions (function-condition x)) - (defined-function-expression x) - (function-app-form x)))) + (list (rule (get-variables x) + (get-expressions (get-condition x)) + (defined-function-app-form x) + (get-expression x)) + (rule (get-variables x) + (get-expressions (get-condition x)) + (get-expression x) + (defined-function-app-form x)))) (define (apply-function f args) (apply-rule '() - (rule (function-variables f) + (rule (get-variables f) '() (defined-function-app-form f) - (defined-function-expression f)) - (app-form (definition-name f) args) + (get-expression f)) + (app-form (get-name f) args) '())) (define (parse-options/theorem ops fail) @@ -779,10 +883,9 @@ (lookup cmd/name sys)) => (lambda (x) (cond - ((is-a? x <proposition>) + ((is-a? x <theorem*>) (rewrite/theorem cmd sys x preconds extracted-expr fail)) - ((and (total-function? x) - (is-a? x <defined-function>)) + ((is-a? x <expandable-function>) (cond ((any (cut apply-rule '() <> extracted-expr '()) (function->rules x)) => identity) @@ -792,8 +895,7 @@ (fail 'invalid-command cmd extracted-expr))))) (else (fail 'command-not-found cmd extracted-expr))))))) -#; -(define/guard (rewrite (sys system?) (expr (const #t)) (seq sequence?)) +(define/guard (rewrite (sys (cut is-a? <> <system>)) (expr (const #t)) (seq sequence?)) (let ((expr (convert-to-expression expr))) (let loop ((expr expr) (seq seq)) @@ -856,226 +958,145 @@ '()))) (define (theorem->rules def) - (expression->rules (theorem-variables def) + (expression->rules (get-variables def) '() - (theorem-expression def))) - -;; (define current-system (make-parameter (make-system '() '() '()))) - - -;; (define (add-definition x) -;; (let ((sys (current-system))) -;; (current-system -;; (cond ((lookup (definition-name x) sys) -;; => (lambda (d) -;; (if (equal? x d) -;; sys -;; (error "(vikalpa) add-definition: duplicated" -;; (definition-name d))))) -;; (else (make-system (cons x (system-definitions sys)) -;; (system-proofs sys) -;; (system-totality-claim-list sys))))) -;; x)) - -;; (define (add-proof x) -;; (let ((sys (current-system))) -;; (current-system -;; (cond ((find-proof (proof-name x) sys) -;; => (lambda (prf) -;; (if (equal? x prf) -;; sys -;; (error "add-proof: duplicated")))) -;; (else (make-system (system-definitions sys) -;; (cons x (system-proofs sys)) -;; (system-totality-claim-list sys))))) -;; x)) + (get-expression def))) -;; (define reserved-symbols '(quote let if error)) -;; (define (reserved? x) -;; (member x reserved-symbols)) +(define current-system (make-parameter (make <system>))) +(define reserved-symbols '(quote let if error)) +(define (reserved? x) + (member x reserved-symbols)) -;; (define-syntax define-axiom -;; (syntax-rules () -;; ((_ name (var ...) expr) -;; (let ((t (axiom 'name '(var ...) -;; (convert-to-expression 'expr)))) -;; (add-definition t) -;; (validate-definition t) -;; t)))) - -;; (define-syntax define-theorem -;; (syntax-rules () -;; ((_ name (var ...) expr) -;; (let ((t (theorem 'name '(var ...) -;; (convert-to-expression 'expr)))) -;; (add-definition t) -;; (validate-definition t) -;; t)))) +(define-syntax define-axiom + (syntax-rules () + ((_ name (var ...) expr) + (let ((t (make <axiom> + #:name 'name + #:variables '(var ...) + #:expression (convert-to-expression 'expr)))) + (current-system (add-definition t (current-system))) + (validate t) + t)))) -;; (define-syntax define-function -;; (syntax-rules () -;; ((_ name (var ...) precond ... expr) -;; (let ((f (function 'name '(var ...) -;; (convert-to-expression 'expr) -;; '(precond ...) -;; (code 'expr)))) -;; (add-definition f) -;; (validate-definition f) -;; f)))) +(define-syntax define-theorem + (syntax-rules () + ((_ name (var ...) expr) + (let ((t (make <conjecture> + #:name 'name + #:variables '(var ...) + #:expression (convert-to-expression 'expr)))) + (current-system (add-definition t (current-system))) + (validate t) + t)))) -;; (define-syntax define-primitive-function -;; (syntax-rules () -;; ((_ name (var ...) precond ... expr) -;; (let ((f (primitive-function 'name '(var ...) -;; (convert-to-expression 'expr) -;; '(precond ...) -;; (code 'expr)))) -;; (add-definition f) -;; (validate-definition f) -;; f)))) +(define-syntax define-core-function + (syntax-rules () + ((_ name (var ...) precond ... proc) + (let ((f (make <core-function> + #:name 'name + #:variables '(var ...) + #:condition '(precond ...) + #:procedure proc))) + (current-system (add-definition f (current-system))) + (validate f) + f)))) -;; (define-syntax define-core-function -;; (syntax-rules () -;; ((_ name (var ...) precond ...) -;; (let ((f (primitive-function 'name '(var ...) #f '(precond ...) #f))) -;; (add-definition f) -;; f)))) +(define-syntax define-function + (syntax-rules () + ((_ name (var ...) precond ... expr) + (let ((f (make <function> + #:name 'name + #:variables '(var ...) + #:condition '(precond ...) + #:expression (convert-to-expression 'expr) + #:precond '(precond ...) + #:code 'expr))) + (current-system (add-definition f (current-system))) + (validate f) + f)))) -;; (define-syntax define-syntax-rules -;; (syntax-rules () -;; ((_ name (l ...) ((lhs1 . lhs2) rhs) ...) -;; (let ((m (macro 'name -;; (list (mrule '(lhs1 . lhs2) 'rhs) -;; ...) -;; '(l ...)))) -;; (add-definition m) -;; m)))) +(define-syntax define-trivial-total-function + (syntax-rules () + ((_ name (var ...) precond ... expr) + (let ((f (make <trivial-total-function> + #:name 'name + #:variables '(var ...) + #:condition '(precond ...) + #:expression (convert-to-expression 'expr) + #:precond '(precond ...) + #:code 'expr))) + (current-system (add-definition f (current-system))) + (validate f) + f)))) -;; (define (find-totality-claim name sys) -;; (assoc name (system-totality-claim-list sys))) +(define-syntax define-syntax-rules + (syntax-rules () + ((_ name (l ...) ((lhs1 . lhs2) rhs) ...) + (let ((m (macro 'name + (list (mrule '(lhs1 . lhs2) 'rhs) + ...) + '(l ...)))) + (current-system (add-definition m (current-system))) + m)))) -;; (define (add-totality-claim tc) -;; (let ((sys (current-system))) -;; (cond ((find-totality-claim (totality-claim-id tc) sys) -;; => (lambda (tc2) -;; (unless (equal? tc tc2) -;; (error "(vikalpa) define-totality-claim: duplicated" -;; tc))))) -;; (unless (and (symbol? (totality-claim-id tc)) -;; (cond ((lookup (totality-claim-natural tc) sys) -;; => function*?) -;; (else #f)) -;; (cond ((lookup (totality-claim-less-than tc) sys) -;; => function*?) -;; (else #f))) -;; (error "(vikalpa) define-totality-claim: invalid totality-claim" -;; tc)) -;; (current-system -;; (make-system (system-definitions sys) -;; (system-proofs sys) -;; (cons tc (system-totality-claim-list sys)))))) +(define-syntax define-system + (syntax-rules () + ((_ name (systems ...) expr ...) + (define* (name #:optional (parent (make <system>))) + (parameterize ((current-system + ((compose systems ... identity) parent))) + expr + ... + (current-system)))))) -;; (define-syntax-rule (define-totality-claim name nat? <) -;; (add-totality-claim (totality-claim 'name 'nat? '<))) +(define (validate-function-name desc name) + (define (err) + (raise-exception + (make-exception + (make-exception-with-message + (string-append "(vikalpa) " desc ": unbound function")) + (make-exception-with-irritants name)))) + (cond + ((lookup name (current-system)) + => (lambda (f) + (if (is-a? f <function*>) + name + (err)))) + (else (err)))) -;; (define core-function-names -;; '(not equal? pair? cons car cdr integer? < binary-+ unary--)) +(define-syntax set-natural-predicate + (syntax-rules () + ((_ name) + (begin + (validate-function-name "set-natural-predicate" 'name) + (current-system (update-natural-predicate 'name (current-system))))))) -;; (define (core-function-name? x) -;; (member x core-function-names)) +(define-syntax set-natural-less-than + (syntax-rules () + ((_ name) + (begin + (validate-function-name "set-natural-less-than" 'name) + (current-system + (update-natural-less-than 'name (current-system))))))) -;; (define (rewrite/core name extracted-expr fail) -;; (case name -;; ((not) -;; (match extracted-expr -;; (('not `(quote ,x)) -;; (expr-quote (not x))) -;; (else -;; (fail 'not extracted-expr)))) -;; ((equal?) -;; (match extracted-expr -;; (('equal? `(quote ,x) `(quote ,y)) -;; (expr-quote (equal? x y))) -;; (else -;; (fail 'equal? extracted-expr)))) -;; ((pair?) -;; (match extracted-expr -;; (('pair? `(quote ,x)) -;; (expr-quote (pair? x))) -;; (else -;; (fail 'pair? extracted-expr)))) -;; ((cons) -;; (match extracted-expr -;; (('cons `(quote ,x) `(quote ,y)) -;; (expr-quote (cons x y))) -;; (else -;; (fail 'cons extracted-expr)))) -;; ((car) -;; (match extracted-expr -;; (('car `(quote ,x)) -;; (if (pair? x) -;; (expr-quote (car x)) -;; ''())) -;; (else -;; (fail 'car extracted-expr)))) -;; ((cdr) -;; (match extracted-expr -;; (('cdr `(quote ,x)) -;; (if (pair? x) -;; (expr-quote (cdr x)) -;; ''())) -;; (else -;; (fail 'cdr extracted-expr)))) -;; ((integer?) -;; (match extracted-expr -;; (('integer? `(quote ,x)) -;; (expr-quote (integer? x))) -;; (else -;; (fail 'integer? extracted-expr)))) -;; ((<) -;; (match extracted-expr -;; (('< `(quote ,x) `(quote ,y)) -;; (let ((x (if (integer? x) x 0)) -;; (y (if (integer? y) y 0))) -;; (expr-quote (< x y)))) -;; (else -;; (fail '< extracted-expr)))) -;; ((succ) -;; (match extracted-expr -;; (('binary-+ `(quote ,x) `(quote ,y)) -;; (if (integer? x) -;; (if (integer? y) -;; (expr-quote (+ x y)) -;; (expr-quote x)) -;; (if (integer? y) -;; (expr-quote y) -;; (expr-quote 0)))) -;; (else -;; (fail 'binary-+ extracted-expr)))) -;; ((unary--) -;; (match extracted-expr -;; (('unary-- `(quote ,x)) -;; (if (integer? x) -;; (expr-quote (- x)) -;; (expr-quote 0))) -;; (else -;; (fail 'unary-- extracted-expr)))) -;; (else (fail 'rewrite/core 'invalid)))) +(define-syntax set-ordinal-predicate + (syntax-rules () + ((_ name) + (begin + (validate-function-name "set-ordinal-predicate" 'name) + (current-system + (update-ordinal-predicate 'name (current-system))))))) -;; (define-syntax define-system -;; (syntax-rules () -;; ((_ name (systems ...) expr ...) -;; (define* (name #:optional (parent (make-system '() '() '()))) -;; (parameterize ((current-system -;; ((compose systems ... core-system) parent))) -;; expr -;; ... -;; (unless (system? (current-system)) -;; (error "define-system: invalid system")) -;; (current-system)))))) +(define-syntax set-ordinal-less-than + (syntax-rules () + ((_ name) + (begin + (validate-function-name "set-ordinal-less-than" 'name) + (current-system + (update-natural-less-than 'name (current-system))))))) (define (defined-function-app-form f) - (cons (definition-name f) (function-variables f))) + (app-form (get-name f) (get-variables f))) (define (single? x) (and (pair? x) @@ -1107,104 +1128,109 @@ (else (if/if x y ''#t)))) -;; (define (make-totality-claim tc m-expr f) -;; (let* ((name (function-name f))) -;; (define (convert app-form) -;; (cond -;; ((apply-rule '() -;; (rule (function-vars f) -;; '() -;; (function-app-form f) -;; m-expr) -;; app-form -;; '()) -;; => identity) -;; (else (error "make-totality-claim: convert error" -;; (function-name f) -;; m-expr -;; app-form)))) -;; (if/if `(,(totality-claim-natural tc) ,m-expr) -;; (let loop ((expr (function-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 `(,(totality-claim-less-than tc) -;; ,(convert expr) -;; ,m-expr) -;; rest) -;; rest))) -;; (else (error "(vikalpa) make-totality-claim: error" -;; (function-name f) -;; m-expr)))) -;; ''#f))) +(define-class <totality-claim-method> () + (id #:getter totality-claim-id #:init-keyword #:id) + (natural #:getter totality-claim-natural #:init-keyword #:natural) + (less-than #:getter totality-claim-less-than #:init-keyword #:less-than)) + +(define (make-totality-claim tc m-expr f) + (let* ((name (get-name f))) + (define (convert app-form) + (cond + ((apply-rule '() + (rule (get-variables f) + '() + (defined-function-app-form f) + m-expr) + app-form + '()) + => identity) + (else (error "make-totality-claim: convert error" + (get-name f) + m-expr + app-form)))) + (if/if `(,(totality-claim-natural tc) ,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 `(,(totality-claim-less-than tc) + ,(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) -;; (cond -;; ((app-form? expr) -;; (let ((rest (append-map find-preconds (cdr expr)))) -;; (append (cond ((lookup (car expr) sys) => -;; (lambda (f) -;; (let ((preconds (function-guard f))) -;; (map (lambda (precond) -;; (substitute (map cons -;; (function-vars f) -;; (cdr expr)) -;; precond)) -;; preconds)))) -;; (else (error "make-guard-claim: error"))) -;; rest))) -;; ((if-form? expr) -;; (find-preconds (if-form-test expr))) -;; (else '()))) -;; (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)))) -;; ((app-form? expr) -;; (apply and/if (map build/find-if (app-form-args expr)))) -;; (else ''#t))) -;; (define (build expr) -;; (cond -;; ((if-form? expr) -;; (apply and/if -;; (append (find-preconds (if-form-test expr)) -;; (list (if/if (if-form-test expr) -;; (build (if-form-then expr)) -;; (build (if-form-else expr))))))) -;; ((app-form? expr) -;; (apply and/if -;; (append (find-preconds expr) -;; (list (build/find-if expr))))) -;; (else ''#t))) -;; (if/if (build expr) -;; ''#t -;; ''#f)) +(define (make-guard-claim expr sys) + (define (find-preconds expr) + (cond + ((app-form? expr) + (let ((rest (append-map find-preconds (cdr expr)))) + (append (cond ((lookup (car expr) sys) => + (lambda (f) + (let ((preconds (get-condition f))) + (map (lambda (precond) + (substitute (map cons + (get-variables f) + (cdr expr)) + precond)) + preconds)))) + (else (error "make-guard-claim: error"))) + rest))) + ((if-form? expr) + (find-preconds (if-form-test expr))) + (else '()))) + (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)))) + ((app-form? expr) + (apply and/if (map build/find-if (app-form-args expr)))) + (else ''#t))) + (define (build expr) + (cond + ((if-form? expr) + (apply and/if + (append (find-preconds (if-form-test expr)) + (list (if/if (if-form-test expr) + (build (if-form-then expr)) + (build (if-form-else expr))))))) + ((app-form? expr) + (apply and/if + (append (find-preconds expr) + (list (build/find-if expr))))) + (else ''#t))) + (if/if (build expr) + ''#t + ''#f)) (define (make-induction-claim f vars c) (define (find-app-forms expr) (cond ((app-form? expr) (let ((rest (append-map find-app-forms (cdr expr)))) - (if (eq? (definition-name f) (app-form-name expr)) + (if (eq? (get-name f) (app-form-name expr)) (cons expr rest) rest))) ((if-form? expr) @@ -1216,7 +1242,7 @@ ((apply-rule '() (rule vars '() - (app-form (definition-name f) vars) + (app-form (get-name f) vars) c) app-form '()) @@ -1242,27 +1268,7 @@ (else (error "make-induction-claim: invalid" f vars c)))) -;; (define (proof? x) -;; (and (list? x) -;; (= 4 (length x)) -;; (symbol? (proof-name x)) -;; (eq? 'proof (list-ref x 1)) -;; (seed? (proof-seed x)) -;; (sequence? (proof-sequence x)))) - -;; (define (proof name seed sequence) -;; (list name 'proof seed sequence)) - -;; (define (proof-name x) -;; (list-ref x 0)) - -;; (define (proof-seed x) -;; (list-ref x 2)) - -;; (define (proof-sequence x) -;; (list-ref x 3)) - -;; (define seed? (const #t)) +(define seed? (const #t)) ;; (define-syntax define-proof ;; (syntax-rules () @@ -1278,48 +1284,69 @@ ;; '(seed ...) ;; '(((n ...) cmd ...) ...)))))) -;; (define (function*? x) -;; (or (function? x) -;; (primitive-function? x))) -;; (define (validate-expression sys name vars expr) -;; (let* ((expr-fnames (expression-functions expr)) -;; (expr-vars (expression-vars expr))) -;; (when (reserved? name) -;; (error (format #f "(vikalpa) ~a: reserved name" name))) -;; (for-each (lambda (x) -;; (when (member x expr-fnames) -;; (error (format #f "(vikalpa) ~a: invalid variable name" name) -;; x))) -;; vars) -;; (for-each (lambda (x) -;; (unless (cond ((lookup x sys) => function*?) -;; (else #f)) -;; (error (format #f "(vikalpa) ~a: undefined function" name) -;; x))) -;; expr-fnames) -;; (for-each (lambda (x) -;; (unless (member x vars) -;; (error (format #f "(vikalpa) ~a: undefined variable" name) -;; x))) -;; expr-vars))) +(define (validate-expression sys name vars expr) + (let* ((expr-fnames (expression-functions expr)) + (expr-vars (expression-vars expr)) + (expr-app-forms (expression-app-forms expr))) + (define (err msg x) + (raise-exception + (make-exception + (make-exception-with-message + (format #f "(vikalpa) ~a: ~a" name msg)) + (make-exception-with-irritants x)))) + (for-each (lambda (x) + (when (member x expr-fnames) + (err "invalid variable" x))) + vars) + (for-each (lambda (fname) + (unless (cond + ((lookup fname sys) => + (lambda (f) + (for-each + (lambda (app-form) + (when (equal? fname (app-form-name app-form)) + (unless (= (length (get-variables f)) + (length (app-form-args app-form))) + (err (format + #f + "~a :wrong number of arguments ~s" + (get-name f) + (get-variables f)) + (app-form-args app-form))))) + expr-app-forms) + #t)) + (else #f)) + (err "undefined function" fname))) + expr-fnames) + (for-each (lambda (x) + (unless (member x vars) + (err "undefined variable" x))) + expr-vars))) -;; (define (validate-definition d) -;; (let* ((vars (definition-vars d)) -;; (name (definition-name d)) -;; (expr (definition-expression d))) -;; (validate-expression (current-system) name vars expr))) +(define (dup? xs) + (if (null? xs) + #f + (if (member (car xs) (cdr xs)) + #t + (dup? (cdr xs))))) -;; (define (recur? f) -;; (member (function-name f) -;; (expression-functions (function-expression f)))) +(define (validate-vars desc vars) + (define (err) + (raise-exception + (make-exception + (make-exception-with-message + (string-append "(vikalpa) " desc ": duplicated variable")) + (make-exception-with-irritants vars)))) + (when (dup? vars) + (err))) -;; (define (p x) -;; (format #t "p:~%~y" x) -;; x) +(define (recur? f) + (member (get-name f) + (expression-functions (get-expression f)))) -;; (define (trivial-total? f sys) -;; (and (not (recur? f)))) +(define (trivial-total? f sys) + (and (not (recur? f)))) ;; (define (prove sys def pf) ;; (cond @@ -1332,7 +1359,7 @@ ;; (define (prove/theorem sys t pf) ;; (let ((sys-without-self ;; (make-system (filter (lambda (d) (not (equal? t d))) -;; (system-definitions sys)) +;; (get-definitions sys)) ;; (system-proofs sys) ;; (system-totality-claim-list sys)))) ;; (rewrite sys-without-self @@ -1371,12 +1398,12 @@ ;; (reverse (filter (lambda (x) ;; (and (function*? x) ;; (function-code x))) -;; (system-definitions sys)))))) +;; (get-definitions sys)))))) ;; (define/guard (check (sys system?)) ;; (let loop ((sys sys) ;; (fails '())) -;; (let ((defs (system-definitions sys))) +;; (let ((defs (get-definitions sys))) ;; (define* (next #:optional fail) ;; (loop (make-system (cdr defs) ;; (system-proofs sys) @@ -1394,17 +1421,17 @@ ;; (next)) ;; (else ;; (cond -;; ((find-proof (definition-name (car defs)) sys) +;; ((find-proof (get-name (car defs)) sys) ;; => (lambda (pf) ;; (let ((result (prove sys (car defs) pf))) ;; (cond ;; ((equal? result ''#t) ;; (next)) ;; (else -;; (next (list (definition-name (car defs)) +;; (next (list (get-name (car defs)) ;; result))))))) ;; (else -;; (next (list (definition-name (car defs))))))))) +;; (next (list (get-name (car defs))))))))) ;; (else ;; (next)))))) @@ -1426,7 +1453,7 @@ ;; `(define-primitive-function ;; ,(function-name def) ;; ,(function-vars def))) -;; ((macro? def) +;; (((cut is-a? <> <macro>) def) ;; `(define-syntax-rules ,(macro-name def))) ;; (else ;; `(error 'fatal-error ,name))))) @@ -1440,27 +1467,123 @@ ;; (append reserved-symbols ;; (map function-name ;; (filter primitive-function? -;; (system-definitions sys))))) +;; (get-definitions sys))))) ;; (define/guard (system-functions (sys system?)) ;; (map function-name ;; (filter function? -;; (system-definitions sys)))) +;; (get-definitions sys)))) ;; (define/guard (system-theorems (sys system?)) ;; (map theorem-name ;; (filter theorem? -;; (system-definitions sys)))) +;; (get-definitions sys)))) ;; (define/guard (system-axioms (sys system?)) ;; (map theorem-name ;; (filter axiom? -;; (system-definitions sys)))) +;; (get-definitions sys)))) ;; (define/guard (system-macros (sys system?)) ;; (map macro-name -;; (filter macro? -;; (system-definitions sys)))) +;; (filter (cut is-a? <> <macro>) +;; (get-definitions sys)))) ;; (define/guard (system-totality-claims (sys system?)) ;; (system-totality-claim-list 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)))) + (define-core-function < (x y) (natural? x) (natural? y) <) + (define-core-function pair? (x) pair?) + (define-core-function cons (x y) cons) + (define-core-function car (x) (pair? x) + (lambda (x) (if (pair? x) (car x) '()))) + (define-core-function cdr (x) (pair? x) + (lambda (x) (if (pair? x) (cdr x) '()))) + (define-core-function + (x y) +) + (set-natural-predicate natural?) + (set-natural-less-than <) + (define-trivial-total-function size (x) + (if (not (pair? x)) + 0 + (+ 1 + (+ (size (car x)) + (size (cdr x)))))) + + (define-syntax-rules and () + ((and) '#t) + ((and x) x) + ((and x . xs) (if x (and . xs) #f))) + + (define-syntax-rules or () + ((or) '#f) + ((or x) x) + ((or x . xs) (if x x (or . xs)))) + + (define-syntax-rules cond (else) + ((cond (else e)) e) + ((cond (test then) . rest) + (if test then (cond . rest)))) + + (define-syntax-rules implies () + ((implies x y) (if x y #t)) + ((implies x y z . rest) + (if x (implies y z . rest) #t))) + + (define-axiom if-nest (x y z) + (if x + (equal? (if x y z) y) + (equal? (if x y z) z))) + + (define-axiom if-true (x y) + (equal? (if '#t x y) x)) + + (define-axiom if-false (x y) + (equal? (if '#f x y) y)) + + (define-axiom if-same (x y) + (equal? (if x y y) y)) + + (define-axiom if-not (x y z) + (equal? (if (not x) y z) + (if x z y))) + + (define-axiom equal-same (x) + (equal? (equal? x x) '#t)) + + (define-axiom equal-swap (x y) + (equal? (equal? x y) (equal? y x))) + + (define-axiom equal-if (x y) + (implies (equal? x y) (equal? x y))) + + (define-axiom pair/cons (x y) + (equal? (pair? (cons x y)) '#t)) + + (define-axiom cons/car+cdr (x) + (implies (pair? x) + (equal? (cons (car x) (cdr x)) x))) + + (define-axiom car/cons (x y) + (equal? (car (cons x y)) x)) + + (define-axiom cdr/cons (x y) + (equal? (cdr (cons x y)) y)) + + (define-axiom equal-car (x1 y1 x2 y2) + (implies (equal? (cons x1 y1) (cons x2 y2)) + (equal? x1 x2))) + (define-function app (x y) + (if (not (pair? x)) + y + (cons (car x) + (app (cdr x) y)))) + + (define-theorem assoc-app (x y z) + (equal? (app x (app y z)) + (app (app x y) z)))) |