diff options
| -rw-r--r-- | vikalpa.scm | 25 |
1 files changed, 12 insertions, 13 deletions
diff --git a/vikalpa.scm b/vikalpa.scm index fb6b500..79c92b8 100644 --- a/vikalpa.scm +++ b/vikalpa.scm @@ -103,6 +103,11 @@ (define (expression-functions expr) (cond + ((if-form? expr) + ;; FIXME + (apply lset-union + eq? + (map expression-functions (cdr expr)))) ((app-form? expr) (cons (app-form-name expr) (apply lset-union @@ -1088,14 +1093,15 @@ (define (convert app-form) (cond ((apply-rule '() - (rule vars + (rule (function-vars f) '() - (cons (function-name f) vars) + (function-app-form f) m-expr) app-form '()) => identity) - (else (error "make-total-claim/natural: convert error")))) + (else (error "make-total-claim/natural: convert error" + app-form)))) (if/if `(natural? ,m-expr) (let loop ((expr (function-expression f))) (cond @@ -1298,16 +1304,8 @@ (define-proof app (total natural? (size x)) - (((2 3 2 1) app) - ((2 3 2 1) if-nest) - ((2 3 1 1) cdr/cons (set x (car x))) - ((2 3) if-same (set x (atom? (cons (car x) (app (cdr x) y))))) - ((2 3 3) size/cdr) - ((2 3 1) atom/cons) - ((2 3) if-false) - ((2) if-same) - (() if-same))) - + ()) + (define-proof associate-app (induction (app x y)) (((2 2) app) @@ -1358,6 +1356,7 @@ (cond ((and (function? (car defs)) (trivial-total? (car defs))) + (format #t "uhehe ~y ~%" (expression-functions (function-expression (car defs)))) (format #t "~a が全域なのは自明で〜す~%" (definition-name (car defs))) (next)) (else |