diff options
| -rw-r--r-- | vikalpa.scm | 146 | ||||
| -rw-r--r-- | vikalpa/prelude.scm | 65 |
2 files changed, 166 insertions, 45 deletions
diff --git a/vikalpa.scm b/vikalpa.scm index 27d09c8..98a7d97 100644 --- a/vikalpa.scm +++ b/vikalpa.scm @@ -418,25 +418,27 @@ (define (primitive-function? x) (and (list? x) - (= 5 (length x)) + (= 6 (length x)) (variable? (function-name x)) (eq? 'primitive-function (list-ref x 1)) (vars? (function-vars x)) ((option expression?) (function-expression x)) - ((option code?) (function-code x)))) + ((option code?) (function-code x)) + ((list-of expression?) (function-preconds x)))) ;; (primitive-function variable? vars?) -> primitive-function? -(define (primitive-function name vs expr code) - (list name 'primitive-function vs expr code)) +(define (primitive-function name vs expr preconds code) + (list name 'primitive-function vs expr preconds code)) (define (function? x) (and (list? x) - (= 5 (length x)) + (= 6 (length x)) (variable? (function-name x)) (eq? 'function (list-ref x 1)) (vars? (function-vars x)) (expression? (function-expression x)) - ((option code?) (function-code x)))) + ((option code?) (function-code x)) + ((list-of expression?) (function-preconds x)))) (define (code? x) (and (list? x) @@ -454,8 +456,9 @@ (define/guard (function (name variable?) (vars vars?) (expr expression?) + (preconds (list-of expression?)) (code (option code?))) - (list name 'function vars expr code)) + (list name 'function vars expr preconds code)) (define (function-name f) (list-ref f 0)) @@ -466,9 +469,12 @@ (define (function-expression f) (list-ref f 3)) -(define (function-code f) +(define (function-preconds f) (list-ref f 4)) +(define (function-code f) + (list-ref f 5)) + (define (definition-name d) (list-ref d 0)) @@ -630,7 +636,7 @@ ((list-of (lambda (x) (and (list? x) (= 2 (length x)) - (symbol? (car x))))) + (symbol? (car x))))) (list-ref x 1)))) (define (expand-let x) @@ -860,11 +866,11 @@ (define (function->rules x) (list (rule (function-vars x) - '() + (function-preconds x) (function-app-form x) (definition-expression x)) (rule (function-vars x) - '() + (function-preconds x) (definition-expression x) (function-app-form x)))) @@ -1050,31 +1056,33 @@ (define-syntax define-function (syntax-rules () - ((_ name (var ...) expr) + ((_ 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-core-function - (syntax-rules () - ((_ name (var ...)) - (let ((f (primitive-function 'name '(var ...) #f #f))) - (add-definition f) - f)))) - (define-syntax define-primitive-function (syntax-rules () - ((_ name (var ...) expr) + ((_ 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 ...) + (let ((f (primitive-function 'name '(var ...) #f '(precond ...) #f))) + (add-definition f) + f)))) + (define-syntax define-syntax-rules (syntax-rules () ((_ name (l ...) ((lhs1 . lhs2) rhs) ...) @@ -1182,6 +1190,14 @@ ''undefined)) (else (fail 'pred extracted-expr)))) + ((<) + (match extracted-expr + (('< `(quote ,x) `(quote ,y)) + (if (and (integer? x) (integer? y)) + (expr-quote (< x y)) + ''undefined)) + (else + (fail 'pred extracted-expr)))) (else (fail 'rewrite/core 'invalid)))) (define* (core-system #:optional (parent (make-system '() '() '()))) @@ -1190,12 +1206,20 @@ (define-core-function equal? (x y)) (define-core-function pair? (x y)) (define-core-function cons (x y)) - (define-core-function car (x)) - (define-core-function cdr (x)) + (define-core-function car (x) + #;(pair? x) + ) + (define-core-function cdr (x) + #;(pair? x) + ) (define-core-function integer? (x)) - (define-core-function < (x y)) - (define-core-function succ (x)) - (define-core-function pred (x)) + (define-core-function < (x y) + ;;(integer? x) (integer? y) + ) + (define-core-function succ (x) ;;(integer? x) + ) + (define-core-function pred (x) ;;(integer? x) + ) (current-system))) (define-syntax define-system @@ -1300,7 +1324,52 @@ (else (error "(vikalpa) make-totality-claim: error" (function-name f) m-expr)))) - ''#t))) + ''#f))) + +(define (make-totality-claim/preconds 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-preconds f))) + (map (lambda (precond) + (substitute (map cons + (function-vars f) + (cdr expr)) + precond)) + preconds)))) + (else (error "make-totality-claim/preconds: 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/guard (make-induction-claim (f function*?) (vars (list-of variable?)) @@ -1439,7 +1508,9 @@ `(claim-of ,(proof-name pf)) (theorem-vars t) claim) - (rewrite sys-without-self claim (proof-sequence pf))))) + (rewrite sys-without-self + claim + (proof-sequence pf))))) (else (error "(vikalpa) define-proof: induction function is not found." (proof-name pf) (cons f vars))))) @@ -1452,6 +1523,16 @@ (define (prove/function sys f pf) (match (proof-seed pf) + (() + (unless (trivial-total? f) + (error "prove/function")) + (rewrite sys + (fold implies/if + (make-totality-claim/preconds + (function-expression f) + sys) + (function-preconds f)) + (proof-sequence pf))) ((id m-expr) (cond ((find-totality-claim id sys) @@ -1462,7 +1543,13 @@ (function-vars f) claim) (rewrite sys - claim + (fold implies/if + (and/if + (make-totality-claim/preconds + (function-expression f) + sys) + claim) + (function-preconds f)) (proof-sequence pf))))) (else (error "(vikalpa) define-proof: totality-claim is not found:" @@ -1497,7 +1584,8 @@ ((null? defs) fails) ((or (theorem? (car defs)) (function? (car defs))) - (cond + (cond + #; ((and (function? (car defs)) (trivial-total? (car defs))) (next)) diff --git a/vikalpa/prelude.scm b/vikalpa/prelude.scm index 5b70a72..c7ab89e 100644 --- a/vikalpa/prelude.scm +++ b/vikalpa/prelude.scm @@ -51,16 +51,6 @@ ((implies x y z . rest) (if x (implies y z . rest) #t))) - (define-function zero? (x) - (equal? 0 x)) - - (define-function natural? (x) - (and (integer? x) - (or (zero? x) - (< 0 x)))) - - (define-totality-claim natural? natural? <) - (define-axiom equal-same (x) (equal? (equal? x x) '#t)) @@ -109,10 +99,19 @@ (implies (equal? (cons x1 y1) (cons x2 y2)) (equal? y1 y2))) + (define-function zero? (x) + (equal? 0 x)) + + (define-function natural? (x) + (and (integer? x) + (or (zero? x) + (< 0 x)))) + (define-axiom pred/succ (x) (implies (natural? x) (equal? (pred (succ x)) x))) + (define-axiom succ/pred (x) (implies (natural? x) (not (zero? x)) @@ -121,16 +120,51 @@ (define-axiom less/pred (x) (implies (natural? x) (equal? (< (pred x) x) #t))) + + (define-totality-claim natural? natural? <) + (define-function + (x y) - (if (natural? x) - (if (zero? x) - y - (succ (+ (pred x) y))) - 'undeifned<+>)) + (natural? x) + (natural? y) + (if (zero? x) + y + (succ (+ (pred x) y)))) + + (define-proof zero? + () + ()) + (define-proof natural? + () + ()) + (define-proof + + (natural? x) + ()) + + #; + (define-proof natural? + () + (((1 2 3 1) (eval)) + ((1 2 3) if-true) + (() if-same (set x (zero? x))) + ((2 1 2) if-nest) + ((2 1) if-same) + ((2) if-true) + ((3 1 2) if-nest) + ((3) if-same (set x (integer? x))) + ((3 2 1) if-nest) + ((3 2) if-nest) + ((3 3 1) if-nest) + ((3 3) if-true) + ((3) if-same) + (() if-same))) + + #; (define-proof + (natural? x) + () + #; (((2) if-nest) ((2 3) less/pred) ((2) if-same) @@ -142,7 +176,6 @@ ;; ((1 2 1) if-nest) ;; ((1 3 1) if-nest) ;; ((1 3) if-true) - ;; (() equal-same))) ;; (define-proof less-than/pred ;; (natural-induction x) |