From 4fedf4213557ec5fbc14988ba1923c48d1da958a Mon Sep 17 00:00:00 2001
From: Masaya Tojo <masaya@tojo.tokyo>
Date: Wed, 18 Nov 2020 23:25:54 +0900
Subject: wip24

---
 vikalpa.scm | 25 ++++++++++++-------------
 1 file 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
-- 
cgit v1.2.3