From eb2a217497a7c0910ddcff94078019987a221449 Mon Sep 17 00:00:00 2001 From: Masaya Tojo Date: Wed, 18 Nov 2020 23:47:35 +0900 Subject: wip25 --- vikalpa.scm | 25 ++++++++++++++++--------- 1 file 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 -- cgit v1.2.3