From c321ba1187d3175b4843b26f94f0b7654296d9d7 Mon Sep 17 00:00:00 2001
From: Masaya Tojo <masaya@tojo.tokyo>
Date: Wed, 16 Dec 2020 23:38:45 +0900
Subject: wip57

---
 vikalpa.scm         | 213 ++++++++++++++++++++++++++++++----------------------
 vikalpa/prelude.scm | 114 +++++++++++++++++++---------
 2 files changed, 203 insertions(+), 124 deletions(-)

diff --git a/vikalpa.scm b/vikalpa.scm
index e7126f8..771c623 100644
--- a/vikalpa.scm
+++ b/vikalpa.scm
@@ -19,6 +19,7 @@
 (define-module (vikalpa)
   #:export (rewrite
             describe
+            system?
             system-check
             system-apropos
             system-code
@@ -36,12 +37,10 @@
   #:use-module (ice-9 exceptions)
   #:use-module (ice-9 regex)
   #:use-module ((srfi srfi-1)
-                #:select (every any member lset-union fold append-map
-                                find))
+                #:select (every any lset-union fold append-map find))
   #:use-module (srfi srfi-8)
   #:use-module (srfi srfi-11)
   #:use-module (srfi srfi-26)
-  #:use-module (ice-9 pretty-print)
   #:use-module (oop goops))
 
 (define-class <system> ()
@@ -85,8 +84,6 @@
 (define-class <total-function> (<expandable-function> <proved>))
 (define-class <trivial-total-function> (<expandable-function>))
 
-(define-generic macro-mrules)
-(define-generic macro-literals)
 (define-class <macro> (<definition>)
   (mrules #:getter macro-mrules #:init-keyword #:mrules)
   (literals #:getter macro-literals #:init-keyword #:literals))
@@ -123,25 +120,21 @@
 (define-method (write (d <total-function>) port)
   (write-definition 'total-function d port))
 
-(define-generic lookup)
 (define-method (lookup (name <symbol>) (s <system>))
   (find (lambda (x)
           (eq? name (get-name x)))
         (get-definitions s)))
 
-(define-generic update-measure-predicate)
 (define-method (update-measure-predicate (s <symbol>) (sys <system>))
   (let ((new (shallow-clone sys)))
     (slot-set! new 'measure-predicate s)
     new))
 
-(define-generic update-measure-less-than)
 (define-method (update-measure-less-than (s <symbol>) (sys <system>))
   (let ((new (shallow-clone sys)))
     (slot-set! new 'measure-less-than s)
     new))
 
-(define-generic update-definition)
 (define-method (update-definition (d <definition>) (sys <system>))
   (define (update d defs)
     (if (null? defs)
@@ -157,21 +150,19 @@
     (slot-set! new 'definitions
                (update d (get-definitions sys)))
     new))
-(define-generic remove-first-definition)
+
 (define-method (remove-first-definition (sys <system>))
   (let ((new (shallow-clone sys)))
     (slot-set! new 'definitions
                (cdr (get-definitions sys)))
     new))
-(define-generic first-definition)
+
 (define-method (first-definition (sys <system>))
   (car (get-definitions sys)))
 
-(define-generic system-empty?)
 (define-method (system-empty? (sys <system>))
   (null? (get-definitions sys)))
 
-(define-generic add-definition)
 (define-method (add-definition (d <definition>) (s <system>))
   (if (lookup (get-name d) s)
       (raise-exception
@@ -179,12 +170,17 @@
         (make-exception-with-origin 'add-definition)
         (make-exception-with-message "duplicated definition")
         (make-exception-with-irritants (get-name d))))
-      (let ((new (shallow-clone s)))
-        (slot-set! new 'definitions
-                   (cons d (get-definitions s)))
-        new)))
+      (if (reserved? (get-name d))
+          (raise-exception
+           (make-exception
+            (make-exception-with-origin 'add-definition)
+            (make-exception-with-message "reserved name")
+            (make-exception-with-irritants (get-name d))))
+          (let ((new (shallow-clone s)))
+            (slot-set! new 'definitions
+                       (cons d (get-definitions s)))
+            new))))
 
-(define-generic validate)
 (define-method (validate (d <definition>))
   (let* ((vars (get-variables d))
          (name (get-name d)))
@@ -510,15 +506,12 @@
     => (cut substitute <> (rule-rhs rl)))
    (else #f)))
 
-(define-type code
-  code
-  (0 code?)
-  (1 (const #t)
-     expr
-     code-expr))
+(define (code x)
+  (list 'code x))
+
+(define (code-expr x)
+  (cadr x))
 
-(define-generic mrule-lhs)
-(define-generic mrule-rhs)
 (define-class <mrule> ()
   (lhs #:getter mrule-lhs #:init-keyword #:lhs)
   (rhs #:getter mrule-rhs #:init-keyword #:rhs))
@@ -835,10 +828,11 @@
       (receive (env)
           (parse-options/theorem (cdr ops) fail)
         (case (caar ops)
-          ((set) (let ((op (car ops)))
-                   (cons (cons (list-ref op 1)
-                               (list-ref op 2))
-                         env)))
+          ((set)
+           (let ((op (car ops)))
+             (cons (cons (list-ref op 1)
+                         (list-ref op 2))
+                   env)))
           (else
            (fail 'invalid-option (car ops)))))))
 
@@ -992,37 +986,27 @@
 
 (define-syntax define-function
   (syntax-rules ()
-    ((_ name (var ...) precond ... expr)
-     (let ((f (make <function>
-                #:name 'name
-                #:variables '(var ...)
-                #:conditions '(precond ...)
-                #:expression (convert-to-expression 'expr)
-                #:code (code 'expr))))
-       (current-system (add-definition f (current-system)))
-       (validate f)
-       f))))
-
-(define-syntax define-function/no-code
-  (syntax-rules ()
-    ((_ name (var ...) precond ... expr)
-     (let ((f (make <function>
-                #:name 'name
-                #:variables '(var ...)
-                #:conditions '(precond ...)
-                #:expression (convert-to-expression 'expr)
-                #:code (code 'expr))))
+    ((_ name (var ...) expr)
+     (let ((f (let ((expression (convert-to-expression 'expr)))
+                (make (if (member 'name (expression-functions expression))
+                          <function>
+                          <trivial-total-function>)
+                  #:name 'name
+                  #:variables '(var ...)
+                  #:conditions '()
+                  #:expression expression
+                  #:code (code 'expr)))))
        (current-system (add-definition f (current-system)))
        (validate f)
        f))))
 
 (define-syntax define-trivial-total-function
   (syntax-rules ()
-    ((_ name (var ...) precond ... expr)
+    ((_ name (var ...) expr)
      (let ((f (make <trivial-total-function>
                 #:name 'name
                 #:variables '(var ...)
-                #:conditions '(precond ...)
+                #:conditions '()
                 #:expression (convert-to-expression 'expr)
                 #:code (code 'expr))))
        (current-system (add-definition f (current-system)))
@@ -1039,10 +1023,16 @@
        (current-system (add-definition m (current-system)))
        m))))
 
+(define* (core-system #:optional (parent (make <system>)))
+  (parameterize ((current-system parent))
+    (define-core-function not (x) not)
+    (define-core-function equal? (x y) equal?)
+    (current-system)))
+
 (define-syntax define-system
   (syntax-rules ()
     ((_ name (systems ...) expr ...)
-     (define* (name #:optional (parent (make <system>)))
+     (define* (name #:optional (parent (core-system)))
        (parameterize ((current-system
                        ((compose systems ... identity) parent)))
          expr
@@ -1113,6 +1103,16 @@
     (if/if x y ''#t))))
 
 (define (make-totality-claim* sys m-expr f)
+  (unless (get-measure-predicate sys)
+    (raise-exception
+     (make-exception
+      (make-exception-with-origin `(define-proof ,(get-name f)))
+      (make-exception-with-message "measure-predicate is not found"))))
+  (unless (get-measure-less-than sys)
+    (raise-exception
+     (make-exception
+      (make-exception-with-origin `(define-proof ,(get-name f)))
+      (make-exception-with-message "measure-less-than is not found"))))
   (let* ((name (get-name f)))
     (define (convert app-form)
       (cond
@@ -1159,7 +1159,7 @@
                            m-expr))))
            ''#f)))
 
-(define (make-guard-claim expr sys)
+(define (make-condition-claim expr sys)
   (define (find-preconds expr)
     (cond
      ((app-form? expr)
@@ -1173,7 +1173,7 @@
                                                    (cdr expr))
                                               precond))
                                 preconds))))
-                      (else (error "make-guard-claim: error")))
+                      (else (error "make-condition-claim: error")))
                 rest)))
      ((if-form? expr)
       (find-preconds (if-form-test expr)))
@@ -1247,17 +1247,36 @@
    (else (error "make-induction-claim: invalid"
                 f vars c))))
 
+(define (validate-sequence sys d seq)
+  (for-each (lambda (r)
+              (for-each (lambda (x)
+                          (match x
+                            (('set var expr)
+                             (validate-expression sys
+                                                  `(define-proof ,(get-name d))
+                                                  (get-variables d)
+                                                  expr))
+                            (else #f)))
+                        (rewriter-command r)))
+            seq))
+
 (define (add-proof/function sys f seed seq)
+  (validate-sequence sys f seq)
   (if seed
-      (update-definition (make <total-function>
-                           #:name (get-name f)
-                           #:variables (get-variables f)
-                           #:conditions (get-conditions f)
-                           #:expression (get-expression f)
-                           #:code (get-code f)
-                           #:claim (make-totality-claim* sys seed f)
-                           #:proof seq)
-                         sys)
+      (begin
+        (validate-expression sys
+                             `(defien-proof ,(get-name f))
+                             (get-variables f)
+                             seed)
+        (update-definition (make <total-function>
+                                  #:name (get-name f)
+                                  #:variables (get-variables f)
+                                  #:conditions (get-conditions f)
+                                  #:expression (get-expression f)
+                                  #:code (get-code f)
+                                  #:claim (make-totality-claim* sys seed f)
+                                  #:proof seq)
+                                sys))
       (raise-exception
        (make-exception
         (make-exception-with-origin 'define-proof)
@@ -1265,13 +1284,32 @@
         (make-exception-with-irritants (get-expression f))))))
 
 (define (add-proof/theorem sys t seed seq)
+  (validate-sequence sys t seq)
   (let ((claim
-         (match seed
-           ((fname . vars)
-            (cond ((lookup fname sys)
-                   => (cut make-induction-claim <> vars (get-expression t)))
-                  (else (get-expression t))))
-           (else (get-expression t)))))
+         (if seed
+             (begin
+               (validate-expression sys
+                                    `(define-proof ,(get-name t))
+                                    (get-variables t)
+                                    seed)
+               (match seed
+                 ((fname . vars)
+                  (cond
+                   ((lookup fname sys)
+                    => (cut make-induction-claim <> vars (get-expression t)))
+                   (else
+                    (raise-exception
+                     (make-exception
+                      (make-exception-with-origin 'add-proof/theorem)
+                      (make-exception-with-message "error")
+                      (make-exception-with-irritants seed))))))
+                 (else
+                  (raise-exception
+                   (make-exception
+                    (make-exception-with-origin `(define-proof ,(get-name t)))
+                    (make-exception-with-message "invalid induction form")
+                    (make-exception-with-irritants seed))))))
+             (get-expression t))))
     (update-definition (make <theorem>
                          #:name (get-name t)
                          #:variables (get-variables t)
@@ -1328,6 +1366,16 @@
     ((_ name seq)
      (define-proof name #f seq))))
 
+(define (validate-expression/error sys name vars expr)
+  (with-exception-handler
+      (lambda (e)
+        (if (eq? 'validate-expression/error (exception-origin e))
+            `(error ,name ,vars ,expr))
+        (raise-exception e))
+    (lambda ()
+      (validate-expression sys 'validate-expression/error vars expr)
+      #f)))
+
 (define (validate-expression sys name vars expr)
   (let* ((expr-fnames (expression-functions expr))
          (expr-vars (expression-vars expr))
@@ -1384,12 +1432,6 @@
   (when (dup? vars)
     (err)))
 
-(define (recur? f)
-  (member (get-name f)
-          (expression-functions (get-expression f))))
-
-(define (trivial-total? f sys)
-  (and (not (recur? f))))
 
 (define/guard (system-apropos (sys system?) (str string?))
   (filter (lambda (name)
@@ -1399,7 +1441,7 @@
                           (symbol->string name)))
           (map get-name (get-definitions sys))))
 
-(define (system-code sys)
+(define/guard (system-code (sys system?))
   `(begin
      ,@(map (lambda (f)
               `(define (,(get-name f) ,@(get-variables f))
@@ -1409,7 +1451,7 @@
                                     (get-code x)))
                              (get-definitions sys))))))
 
-(define (check sys)
+(define (system-check sys)
   (let loop ((sys sys)
              (fails '()))
     (if (system-empty? sys)
@@ -1469,15 +1511,7 @@
 (define/guard (system-load (sys system?))
   (primitive-eval (system-code sys)))
 
-;; (define/guard (system-environment (sys system?))
-;;   (map (lambda (def)
-;;          (list (get-name def)
-;;                (show sys name)))
-;;        (get-definitions sys)))
-
 (define-system prelude ()
-  (define-core-function not (x) not)
-  (define-core-function equal? (x y) equal?)
   (define-core-function natural? (x) (lambda (x)
                                        (and (integer? x)
                                             (< 0 x))))
@@ -1586,6 +1620,9 @@
 
   (define-theorem caar-cons2 (x y z)
     (equal? (car (car (cons (cons x y) z))) x))
+
+  (define-function double (x)
+    (+ x x))
   
   (define-function app (x y)
     (if (not (pair? x))
@@ -1611,6 +1648,4 @@
 
   (define-proof assoc-app
     (list-induction x)
-    ())
-  )
-
+    ()))
diff --git a/vikalpa/prelude.scm b/vikalpa/prelude.scm
index f37bdd0..17d1db8 100644
--- a/vikalpa/prelude.scm
+++ b/vikalpa/prelude.scm
@@ -21,23 +21,38 @@
   #:use-module (vikalpa))
 
 (define-system prelude ()
-  (define-function natural? (x)
-    (if (integer? x)
-        (< 0 x)
-        #f))
-
-  (define-syntax-rules + ()
-    ((+ x . xs) (binary-+ x (+ . xs)))
-    ((+ x) x)
-    ((+) '0))
-
-  (define-syntax-rules - ()
-    ((- x . xs) (binary-+ x (- . xs)))
-    ((- x) (unary-- x)))
-  
-  (define-syntax-rules list ()
-    ((list) '())
-    ((list x . y) (cons x (list . y))))
+  (define-core-function natural? (x) (lambda (x)
+                                       (and (integer? x)
+                                            (< 0 x))))
+  (define-core-function < (x y) (natural? x) (natural? y) <)
+  (define-core-function pair? (x) pair?)
+  (define-core-function cons (x y) cons)
+  (define-core-function car (x) (pair? x)
+    (lambda (x) (if (pair? x) (car x) '())))
+  (define-core-function cdr (x) (pair? x)
+    (lambda (x) (if (pair? x) (cdr x) '())))
+  (define-core-function + (x y)
+    (lambda (x y)
+      (if (number? x)
+          (if (number? y)
+              (+ x y)
+              x)
+          (if (number? y)
+              y
+              0))))
+  (set-measure-predicate natural?)
+  (set-measure-less-than <)
+  (define-trivial-total-function list-induction (x)
+    (if (not (pair? x))
+        x
+        (cons (car x)
+              (list-induction (cdr x)))))
+  (define-trivial-total-function size (x)
+    (if (not (pair? x))
+        0
+        (+ 1
+           (+ (size (car x))
+              (size (cdr x))))))
 
   (define-syntax-rules and ()
     ((and) '#t)
@@ -58,16 +73,7 @@
     ((implies x y) (if x y #t))
     ((implies x y z . rest)
      (if x (implies y z . rest) #t)))
-
-  (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)
-    (implies (equal? x y) (equal? x y)))
-
+  
   (define-axiom if-nest (x y z)
     (if x
         (equal? (if x y z) y)
@@ -86,6 +92,15 @@
     (equal? (if (not x) y z)
             (if x z y)))
 
+  (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)
+    (implies (equal? x y) (equal? x y)))
+  
   (define-axiom pair/cons (x y)
     (equal? (pair? (cons x y)) '#t))
 
@@ -99,16 +114,45 @@
   (define-axiom cdr/cons (x y)
     (equal? (cdr (cons x y)) y))
 
+  (define-axiom natural/size (x)
+    (equal? (natural? (size x)) #t))
+
+  (define-axiom size/car (x)
+    (equal? (< (size (car x)) (size x)) #t))
+
+  (define-axiom size/cdr (x)
+    (equal? (< (size (cdr x)) (size x)) #t))
+
   (define-axiom equal-car (x1 y1 x2 y2)
     (implies (equal? (cons x1 y1) (cons x2 y2))
              (equal? x1 x2)))
 
-  (define-axiom equal-cdr (x1 y1 x2 y2)
-    (implies (equal? (cons x1 y1) (cons x2 y2))
-             (equal? y1 y2)))
-
-  (define-function zero? (x)
-    (equal? 0 x))
+  (define-theorem caar-cons2 (x y z)
+    (equal? (car (car (cons (cons x y) z))) x))
+  
+  (define-function app (x y)
+    (if (not (pair? x))
+        y
+        (cons (car x)
+              (app (cdr x) y))))
+  
+  (define-theorem assoc-app (x y z)
+    (equal? (app x (app y z))
+            (app (app x y) z)))
+
+  (define-proof caar-cons2
+    (((1 1)  car/cons)
+     ((1) car/cons)
+     (() equal-same)))
+
+  (define-proof app
+    (size x)
+    (((2 3) size/cdr)
+     ((2) if-same)
+     ((1) natural/size)
+     (() if-true)))
+
+  (define-proof assoc-app
+    (list-induction x)
+    ()))
 
-  (define-totality-claim natural? natural? <)
-  )
-- 
cgit v1.2.3