From 31901d7bc02e464dd194f4b235287b5dce056471 Mon Sep 17 00:00:00 2001
From: Masaya Tojo <masaya@tojo.tokyo>
Date: Wed, 18 Nov 2020 23:07:08 +0900
Subject: wip22

---
 vikalpa.scm | 206 ++++++++++++++++++++++++++++++++++--------------------------
 1 file changed, 116 insertions(+), 90 deletions(-)

diff --git a/vikalpa.scm b/vikalpa.scm
index 4454e52..c66e130 100644
--- a/vikalpa.scm
+++ b/vikalpa.scm
@@ -61,7 +61,8 @@
   (cond ((expr-quoted? expr)
          (or (integer? (expr-unquote expr))
              (boolean? (expr-unquote expr))
-             (symbol? (expr-unquote expr))))
+             (symbol? (expr-unquote expr))
+             (null? (expr-unquote expr))))
         ((if-form? expr)
          (and (expression? (if-form-test expr))
               (expression? (if-form-then expr))
@@ -402,27 +403,21 @@
 
 (define (primitive-function? x)
   (and (list? x)
-       (= 4 (length x))
-       (variable? (list-ref x 0))
+       (= 3 (length x))
+       (variable? (primitive-function-name x))
        (eq? 'primitive-function (list-ref x 1))
-       (let ((ps (list-ref x 2)))
-         (and (list? ps)
-              (every procedure? ps)))
-       (procedure? (list-ref x 3))))
+       (vars? (primitive-function-vars x))))
 
-;; (primitive-function variable? (list-of procedure?) procedure?) -> primitive-function?
-(define (primitive-function name ps proc)
-  (list name 'primitive-function ps proc))
+;; (primitive-function variable? vars?) -> primitive-function?
+(define (primitive-function name vs)
+  (list name 'primitive-function vs))
 
 (define (primitive-function-name pf)
   (list-ref pf 0))
 
-(define (primitive-function-preds pf)
+(define (primitive-function-vars pf)
   (list-ref pf 2))
 
-(define (primitive-function-proc pf)
-  (list-ref pf 3))
-
 (define (match-primitive-function pf expression)
   (and (pair? expression)
        (eq? (primitive-function-name pf) (car expression))
@@ -457,6 +452,9 @@
 (define (function-expression f)
   (list-ref f 3))
 
+(define (definition-name d)
+  (list-ref d 0))
+
 (define (mrule? x)
   (and (list? x)
        (= 3 (length x))
@@ -580,6 +578,24 @@
               new-expr)
           (expand* ms new-expr)))))
 
+(define (quote-all x)
+  (cond
+   ((expr-quoted? x) x)
+   ((if-form? x)
+    (if-form (quote-all (if-form-test x))
+             (quote-all (if-form-then x))
+             (quote-all (if-form-else x))))
+   ((app-form? x)
+    (cons (app-form-name x)
+          (map quote-all (app-form-args x))))
+   ((variable? x) x)
+   (else `',x)))
+
+(define (convert-to-expression x)
+  (quote-all
+   (expand* (filter macro? (system-definitions (current-system)))
+            x)))
+
 ;; (axiom variable? vars? expression?) -> axiom?
 ;; axiom? is theorem*
 (define/guard (axiom (name variable?) (vars vars?) (expr expression?))
@@ -784,11 +800,7 @@
                  (else
                   (fail (format #f "no match-function (~a)" cmd)))))
                ((primitive-function? x)
-                (cond
-                 ((match-primitive-function x extracted-expr)
-                  (apply-primitive-function x extracted-expr))
-                 (else
-                  (fail "can't apply-primitive-function (~a)" cmd))))
+                (fail "primitive-function fail"))
                ((macro? x)
                 (fail "macro fail"))
                (else
@@ -881,7 +893,8 @@
 (define-syntax define-axiom
   (syntax-rules ()
     ((_ name (var ...) expr)
-     (let ((t (axiom 'name '(var ...) 'expr)))
+     (let ((t (axiom 'name '(var ...)
+                     (convert-to-expression 'expr))))
        (validate-theorem t)
        (add-definition t)
        t))))
@@ -889,7 +902,8 @@
 (define-syntax define-theorem
   (syntax-rules ()
     ((_ name (var ...) expr)
-     (let ((t (theorem 'name '(var ...) 'expr)))
+     (let ((t (theorem 'name '(var ...)
+                       (convert-to-expression 'expr))))
        (validate-theorem t)
        (add-definition t)
        t))))
@@ -897,15 +911,16 @@
 (define-syntax define-function
   (syntax-rules ()
     ((_ name (var ...) expr)
-     (let ((f (function 'name '(var ...) 'expr)))
+     (let ((f (function 'name '(var ...)
+                        (convert-to-expression 'expr))))
        (validate-function f)
        (add-definition f)
        f))))
 
-(define-syntax define-primitivge-function
+(define-syntax define-primitive-function
   (syntax-rules ()
-    ((_ name (p? ...) proc)
-     (let ((f (primitive-function 'name (list p? ...) proc)))
+    ((_ name (var ...))
+     (let ((f (primitive-function 'name '(var ...))))
        (add-definition f)
        f))))
 
@@ -936,107 +951,69 @@
 (define (any? x) #t)
 
 (define-system prelude ()
-  (define-primitivge-function natural?
-    (any?)
-    natural?)
-
-  (define-primitivge-function equal?
-    (any? any?)
-    equal?)
-
-  (define-primitivge-function atom?
-    (any?)
-    (lambda (x) (not (pair? x))))
-
-  (define-primitivge-function cons
-    (any? any?)
-    cons)
-
-  (define-primitivge-function car
-    (pair?)
-    car)
-
-  (define-primitivge-function cdr
-    (pair?)
-    cdr)
-
-  (define-primitivge-function size
-    (any?)
-    size)
-  
+  (define-primitive-function natural? (x))
+  (define-primitive-function equal? (x y))
+  (define-primitive-function atom? (x))
+  (define-primitive-function cons (x y))
+  (define-primitive-function car (x))
+  (define-primitive-function cdr (x))
+  (define-primitive-function size (x))
+  (define-primitive-function < (x y))
+  (define-primitive-function not (x))
+
   (define-axiom equal-same (x)
     (equal? (equal? x x) '#t))
-
   (define-axiom equal-swap (x y)
     (equal? (equal? x y) (equal? y x)))
-
   (define-axiom equal-if (x y)
     (if (equal? x y) (equal? x y) '#t))
-
   (define-axiom atom/cons (x y)
     (equal? (atom? (cons x y)) '#f))
-
   (define-axiom car/cons (x y)
     (equal? (car (cons x y)) x))
-
   (define-axiom cdr/cons (x y)
     (equal? (cdr (cons x y)) y))
-
   (define-axiom cons/car+cdr (x)
     (if (atom? x)
         '#t
         (equal? (cons (car x) (cdr x)) x)))
-
   (define-axiom if-nest (x y z)
     (if x
         (equal? (if x y z) y)
         (equal? (if x y z) z)))
-
   (define-axiom if-nest-t (x y z)
     (if x
         (equal? (if x y z) y)
         '#t))
-
   (define-axiom if-nest-f (x y z)
     (if x
         '#t
         (equal? (if x y z) z)))
-
   (define-axiom if-false (x y)
     (equal? (if '#f x y) y))
-
   (define-axiom if-same (x y)
     (equal? (if x y y) y))
-
   (define-axiom natural/size (x)
     (equal? (natural? (size x))
             '#t))
-
   (define-axiom size/car (x)
     (if (atom? x)
         '#t
         (equal? (< (size (car x)) (size x))
                 '#t)))
-
   (define-axiom size/cdr (x)
     (if (atom? x)
         '#t
         (equal? (< (size (cdr x)) (size x))
                 '#t)))
+  (define-axiom if-not (x y z)
+    (equal? (if (not x) y z)
+            (if x z y)))
 
   (define-macro list ()
     ((list) '())
     ((list x . y) (cons x (list . y))))
 
-  (define-macro + ()
-    ((+) '0)
-    ((+ x) x)
-    ((+ x . xs) (b+ x (+ . xs))))
-
-  (define-macro - ()
-    ((- x) (u- x))
-    ((- x . xs) (+ x . (u- (+ . xs)))))
-
   (define-macro and ()
     ((and) '#t)
     ((and x) x)
@@ -1047,13 +1024,16 @@
     ((or x) x)
     ((or x . xs) (if x x (or . xs))))
 
-  (define-axiom if-not (x y z)
-    (equal? (if (not x)
-                y
-                z)
-            (if x
-                z
-                y))))
+  #;
+  (define-macro + ()
+    ((+) '0)
+    ((+ x) x)
+    ((+ x . xs) (b+ x (+ . xs))))
+  #;
+  (define-macro - ()
+    ((- x) (u- x))
+    ((- x . xs) (+ x . (u- (+ . xs)))))
+)
 
 (define (measure? x)
   (and (pair? x)
@@ -1105,8 +1085,18 @@
 
 (define (make-total-claim/natural m vars f)
   (let ((name (function-name f))
-        (m-expr (list (function-name m)
-                      (function-app-form f))))
+        (m-expr (cons (function-name m) vars)))
+    (define (convert app-form)
+      (cond
+       ((apply-rule '()
+                    (rule vars
+                          '()
+                          (cons (function-name f) vars)
+                          m-expr)
+                    app-form
+                    '())
+        => identity)
+       (else (error "make-total-claim/natural: convert error"))))
     (if/if `(natural? ,m-expr)
            (let loop ((expr (function-expression f)))
              (cond
@@ -1128,7 +1118,7 @@
                               (else (and/if (loop (car args))
                                             (f (cdr args))))))))
                  (if (eq? name (app-form-name expr))
-                     (and/if `(< ,(list (function-name m) expr) ,m-expr)
+                     (and/if `(< ,(convert expr) ,m-expr)
                              rest)
                      rest)))
               (else (error "(vikalpa) make-total-claim: error"))))
@@ -1317,8 +1307,7 @@
      ((2 3 1) atom/cons)
      ((2 3) if-false)
      ((2) if-same)
-     (() if-same)
-     ))
+     (() if-same)))
 
   (define-proof associate-app
     (induction (app x y))
@@ -1353,5 +1342,42 @@
       y
       (cons (car x) (app (cdr x) y))))
 
-;; (define (review sys)
-;;   )
+(define (check sys)
+  (let loop ((sys sys)
+             (fails '()))
+    (let ((defs (system-definitions sys)))
+      (define* (next #:optional fail)
+        (loop (make-system (cdr defs)
+                           (system-proofs sys))
+              (if fail
+                  (cons fail fails)
+                  fails)))
+      (cond
+       ((null? defs) fails)
+       ((or (theorem? (car defs))
+            (function? (car defs)))
+        (cond
+         ((and (function? (car defs))
+               (trivial-total? (car defs)))
+          (format #t "~a が全域なのは自明で〜す~%" (definition-name (car defs)))
+          (next))
+         (else
+          (cond
+           ((find-proof (definition-name (car defs)) sys)
+            => (lambda (pf)
+                 (let ((result (prove sys (car defs) pf)))
+                   (cond
+                    ((equal? result ''#t)
+                     (format #t "~a が全域であると証明しました!!~%"
+                             (definition-name (car defs)))
+                     (next))
+                    (else
+                     (format #t "~a の証明に失敗しました(しょぼ〜ん)~%~y"
+                             (definition-name (car defs))
+                             result)
+                     (next (definition-name (car defs))))))))
+           (else
+            (format #t "~a の証明がありません(しょぼ〜ん)~%"
+                    (definition-name (car defs))))))))
+       (else
+        (next))))))
-- 
cgit v1.2.3