diff options
Diffstat (limited to 'vikalpa.scm')
-rw-r--r-- | vikalpa.scm | 146 |
1 files changed, 117 insertions, 29 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)) |