diff options
| author | Masaya Tojo <masaya@tojo.tokyo> | 2020-11-18 23:47:35 +0900 |
|---|---|---|
| committer | Masaya Tojo <masaya@tojo.tokyo> | 2020-11-18 23:47:35 +0900 |
| commit | eb2a217497a7c0910ddcff94078019987a221449 (patch) | |
| tree | 84e2af85c546b9253801acd6112d61d9afcb031c | |
| parent | 4fedf4213557ec5fbc14988ba1923c48d1da958a (diff) | |
wip25
| -rw-r--r-- | vikalpa.scm | 25 |
1 files changed, 16 insertions, 9 deletions
diff --git a/vikalpa.scm b/vikalpa.scm index 79c92b8..42f046a 100644 --- a/vikalpa.scm +++ b/vikalpa.scm @@ -104,10 +104,12 @@ (define (expression-functions expr) (cond ((if-form? expr) - ;; FIXME (apply lset-union eq? - (map expression-functions (cdr expr)))) + (map expression-functions + (list (if-form-test expr) + (if-form-then expr) + (if-form-else expr))))) ((app-form? expr) (cons (app-form-name expr) (apply lset-union @@ -1304,7 +1306,9 @@ (define-proof app (total natural? (size x)) - ()) + (((2 3) size/cdr) + ((2) if-same) + (() if-same))) (define-proof associate-app (induction (app x y)) @@ -1356,8 +1360,8 @@ (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))) + (format #t "`~a` is trivial total function.~%" + (definition-name (car defs))) (next)) (else (cond @@ -1366,16 +1370,19 @@ (let ((result (prove sys (car defs) pf))) (cond ((equal? result ''#t) - (format #t "~a が全域であると証明しました!!~%" - (definition-name (car defs))) + (format #t "`~a` is ~a.~%" + (definition-name (car defs)) + (if (function? (car defs)) + "total function" + "true")) (next)) (else - (format #t "~a の証明に失敗しました(しょぼ〜ん)~%~y" + (format #t "`~a`'s proof is failed:~%~y" (definition-name (car defs)) result) (next (definition-name (car defs)))))))) (else - (format #t "~a の証明がありません(しょぼ〜ん)~%" + (format #t "`~a`'s proof is not found.~%" (definition-name (car defs))) (next (definition-name (car defs)))))))) (else |