From 93e872a9926f775822270d99257aa3a0542e4693 Mon Sep 17 00:00:00 2001
From: Masaya Tojo <masaya@tojo.tokyo>
Date: Fri, 11 Dec 2020 04:02:58 +0900
Subject: wip44

---
 vikalpa.scm | 1057 +++++++++++++++++++++++++++++++++--------------------------
 1 file changed, 590 insertions(+), 467 deletions(-)

diff --git a/vikalpa.scm b/vikalpa.scm
index 1b3c158..bff63f0 100644
--- a/vikalpa.scm
+++ b/vikalpa.scm
@@ -52,69 +52,159 @@
   #:use-module (oop goops))
 
 (define-class <system> ()
-  (definitions #:getter system-definitions #:init-keyword #:definitions)
-  (total-cliam-method #:getter system-total-claim-method
-                      #:init-keyword #:total-cliam-method))
+  (definitions
+    #:getter get-definitions
+    #:init-keyword #:definitions
+    #:init-value '())
+  (natural-predicate #:getter get-natural-predicate
+                     #:init-value #f)
+  (natural-less-than #:getter get-natural-less-than
+                     #:init-value #f)
+  (ordinal-predicate #:getter get-ordinal-predicate
+                     #:init-value #f)
+  (ordinal-less-than #:getter get-ordinal-less-than
+                     #:init-value #f))
 
 (define-class <definition> ()
-  (name #:getter definition-name #:init-keyword #:name))
+  (name #:getter get-name
+        #:init-keyword #:name)
+  (variables #:getter get-variables
+             #:init-keyword #:variables
+             #:init-value '()))
 
-(define-class <condition> ()
-  (expressions #:getter condition-expressions #:init-keyword #:expressions))
-
-(define-class <function> (<definition>)
-  (variables #:getter function-variables #:init-keyword #:variables)
-  (condition #:getter function-condition #:init-keyword #:condition))
-
-(define-class <total-function> ())
-
-(define-class <core-function> (<function>)
-  (procedure #:getter core-function-procedure #:init-keyword #:procedure))
-
-(define-class <defined-function> (<function>)
-  (expression #:getter defined-function-expression #:init-keyword #:expression)
-  (code #:getter defined-function-code #:init-keyword #:code))
+(define-class <provable> ())
 
-(define-class <total-function> (<defined-function>)
-  (proof #:getter theorem-proof #:init-keyword #:proof))
+(define-class <proved> (<provable>)
+  (claim #:getter get-claim #:init-keyword #:claim)
+  (proof #:getter get-proof #:init-keyword #:proof))
 
-(define-class <primitive-function> (<defined-function>))
+(define-class <theorem*> (<definition>)
+  (expression #:getter get-expression #:init-keyword #:expression))
 
-(define-generic total-function?)
-(define-method (total-function? x)
-  (or (is-a? x <core-function>)
-      (is-a? x <primitive-function>)
-      (is-a? x <total-function>)))
+(define-class <conjecture> (<theorem*> <provable>))
+(define-class <theorem> (<theorem*> <proved>))
+(define-class <axiom> (<theorem*>))
 
-(define-class <proposition> (<definition>)
-  (variables #:getter proposition-variables #:init-keyword #:variables)
-  (expression #:getter proposition-expression #:init-keyword #:expression))
-
-(define-class <conjecture> (<proposition>))
-(define-class <theorem> (<proposition>)
-  (proof #:getter theorem-proof #:init-keyword #:proof))
-(define-class <axiom> (<theorem>))
-
-(define (theorem? x)
-  (or (is-a? x <theorem>)
-      (is-a? x <axiom>)))
+(define-class <condition> ()
+  (expressions #:getter get-expressions #:init-keyword #:expressions))
+
+(define-class <function*> (<definition>)
+  (condition #:getter get-condition #:init-keyword #:condition))
+(define-class <core-function> (<function*>)
+  (procedure #:getter get-procedure #:init-keyword #:procedure))
+(define-class <expandable-function> (<function*>)
+  (expression #:getter get-expression #:init-keyword #:expression)
+  (code #:getter get-code #:init-keyword #:expressions))
+(define-class <function> (<expandable-function> <provable>))
+(define-class <total-function> (<expandable-function> <proved>))
+(define-class <trivial-total-function> (<expandable-function>))
+
+(define (write-definition sym d port)
+  (format port "#<~a: ~s>"
+          sym (cons (get-name d) (get-variables d))))
+
+(define-method (display (d <definition>) port)
+  (write d port))
+
+(define-method (write (s <system>) port)
+  (format port "#<system: function: ~a theorem: ~a macro: ~a>"
+          (length (filter (cut is-a? <> <function*>)
+                          (get-definitions s)))
+          (length (filter (cut is-a? <> <theorem*>)
+                          (get-definitions s)))
+          (length (filter (cut is-a? <> <macro>)
+                          (get-definitions s)))))
+
+(define-method (write (d <conjecture>) port)
+  (write-definition 'conjecture d port))
+(define-method (write (d <theorem>) port)
+  (write-definition 'theorem d port))
+(define-method (write (d <axiom>) port)
+  (write-definition 'axiom d port))
+(define-method (write (d <axiom>) port)
+  (write-definition 'axiom d port))
+(define-method (write (d <function>) port)
+  (write-definition 'function d port))
+(define-method (write (d <core-function>) port)
+  (write-definition 'function d port))
+(define-method (write (d <trivial-total-function>) port)
+  (write-definition 'trivial-total-function d port))
+(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 (definition-name x)))
-        (system-definitions s)))
+  (find (lambda (x)
+          (eq? name (get-name x)))
+        (get-definitions s)))
+
+(define-generic update-natural-predicate)
+(define-method (update-natural-predicate (s <symbol>) (sys <system>))
+  (let ((new (shallow-clone sys)))
+    (slot-set! new 'natural-predicate s)
+    new))
+
+(define-generic update-natural-less-than)
+(define-method (update-natural-less-than (s <symbol>) (sys <system>))
+  (let ((new (shallow-clone sys)))
+    (slot-set! new 'natural-less-than s)
+    new))
+
+(define-generic update-ordinal-predicate)
+(define-method (update-ordinal-predicate (s <symbol>) (sys <system>))
+  (let ((new (shallow-clone sys)))
+    (slot-set! new 'ordinal-predicate s)
+    new))
+
+(define-generic update-ordinal-less-than)
+(define-method (update-ordinal-less-than (s <symbol>) (sys <system>))
+  (let ((new (shallow-clone sys)))
+    (slot-set! new 'ordinal-less-than-function s)
+    new))
+
+(define-generic update-definition)
+(define-method (update-definition (d <definition>) (sys <system>))
+  (let ((new (shallow-clone sys)))
+    (slot-set! new 'definitions
+               (cons d (get-definitions sys)))
+    new))
+
+(define-generic update-definition)
+(define-method (update-definition (d <definition>) (sys <system>))
+  (let ((new (shallow-clone sys)))
+    (slot-set! new 'definitions
+               (cons d (get-definitions sys)))
+    new))
 
 (define-generic add-definition)
 (define-method (add-definition (d <definition>) (s <system>))
-  (if (lookup (definition-name d) s)
+  (if (lookup (get-name d) s)
       (raise-exception
        (make-exception
         (make-exception-with-message
          "(vikalpa) add-definition: duplicated definition")
-        (make-exception-with-irritants (definition-name s))))
-      (make <system>
-        #:definitions (cons d (system-definitions s))
-        #:total-cliam-method (system-total-claim-method s))))
+        (make-exception-with-irritants (get-name d))))
+      (update-definition d s)))
+
+(define-generic validate)
+(define-method (validate (d <definition>))
+  (let* ((vars (get-variables d))
+         (name (get-name d)))
+    (validate-vars (symbol->string name) vars)))
+
+(define-method (validate (d <expandable-function>))
+  (let* ((vars (get-variables d))
+         (name (get-name d))
+         (expr (get-expression d)))
+    (validate-expression (current-system) name vars expr)
+    (next-method)))
+
+(define-method (validate (d <theorem*>))
+  (let* ((vars (get-variables d))
+         (name (get-name d))
+         (expr (get-expression d)))
+    (validate-expression (current-system) name vars expr)
+    (next-method)))
 
 (define (debug f . args)
   (if #f
@@ -217,6 +307,19 @@
 (define (if-form-else expr)
   (list-ref expr 3))
 
+(define (expression-app-forms expr)
+  (cond
+   ((if-form? expr)
+    (append-map expression-app-forms
+                (list (if-form-test expr)
+                      (if-form-then expr)
+                      (if-form-else expr))))
+   ((app-form? expr)
+    (cons expr
+          (append-map expression-app-forms
+                      (app-form-args expr))))
+   (else '())))
+
 (define (expression-functions expr)
   (cond
    ((if-form? expr)
@@ -433,18 +536,18 @@
           (else '())))
   (all-vars (mrule-lhs mrl)))
 
-(define-type macro
-  macro
-  (1 macro?)
-  (0 variable? name macro-name)
-  (2 (lambda (mrls)
-       (and (list? mrls)
-            (every mrule? mrls)))
-     mruls
-     macro-mrules)
-  (3 (list-of symbol?)
-     literals
-     macro-literals))
+(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))
+
+(define (macro name mrules literals)
+  (make <macro>
+    #:name name
+    #:variables '()
+    #:mrules mrules
+    #:literals literals))
 
 (define (apply-mrule rl ls expr)
   (define (literal? x)
@@ -504,7 +607,7 @@
 
 (define (apply-macro m expr)
   (cond ((and (pair? expr)
-              (eq? (macro-name m) (car expr)))
+              (eq? (get-name m) (car expr)))
          (let loop ((rs (macro-mrules m)))
            (cond ((null? rs)
                   (error "(vikalpa) macro fail" m expr))
@@ -585,7 +688,8 @@
 
 (define (convert-to-expression x)
   (quote-all
-   (expand* (filter macro? (system-definitions (current-system)))
+   (expand* (filter (cut is-a? <> <macro>)
+                    (get-definitions (current-system)))
             (expand-let x))))
 
 (define (vars? x)
@@ -593,9 +697,9 @@
        (every variable? x)))
 
 (define (theorem-rules x)
-  (expression->rules (theorem-variables x)
+  (expression->rules (get-variables x)
                      '()
-                     (theorem-expression x)))
+                     (get-expression x)))
 
 (define (rewrite/eval expr sys)
   (let eval ((expr expr))
@@ -608,7 +712,7 @@
             (eval (rewrite1 sys
                             `(,name ,@args)
                             (lambda args
-                              (cons* 'error rewrite name args))
+                              (cons* 'error 'rewrite name args))
                             (rewriter '() `(,name)))))))
      ((if-form? expr)
       (let ((test (eval (if-form-test expr))))
@@ -673,10 +777,10 @@
 (define (command-options x)
   (cdr x))
 
-;; (define/guard (system-eval (expr (const #t)) (sys system?))
-;;   (rewrite/eval (parameterize ((current-system sys))
-;;                   (convert-to-expression expr))
-;;                 sys))
+(define/guard (system-eval (expr (const #t)) (sys (cut is-a? <> <system>)))
+  (rewrite/eval (parameterize ((current-system sys))
+                  (convert-to-expression expr))
+                sys))
 
 ;; (extract path? expression? preconds? procedure?) -> (values expression? procedure?)
 (define (extract path expr fail)
@@ -712,22 +816,22 @@
           (fail 'invalid-path path))))))
 
 (define (function->rules x)
-  (list (rule (function-variables x)
-              (condition-expressions (function-condition x))
-              (function-app-form x)
-              (defined-function-expression x))
-        (rule (function-variables x)
-              (condition-expressions (function-condition x))
-              (defined-function-expression x)
-              (function-app-form x))))
+  (list (rule (get-variables x)
+              (get-expressions (get-condition x))
+              (defined-function-app-form x)
+              (get-expression x))
+        (rule (get-variables x)
+              (get-expressions (get-condition x))
+              (get-expression x)
+              (defined-function-app-form x))))
 
 (define (apply-function f args)
   (apply-rule '()
-              (rule (function-variables f)
+              (rule (get-variables f)
                     '()
                     (defined-function-app-form f)
-                    (defined-function-expression f))
-              (app-form (definition-name f) args)
+                    (get-expression f))
+              (app-form (get-name f) args)
               '()))
 
 (define (parse-options/theorem ops fail)
@@ -779,10 +883,9 @@
               (lookup cmd/name sys))
          => (lambda (x)
               (cond
-               ((is-a? x <proposition>)
+               ((is-a? x <theorem*>)
                 (rewrite/theorem cmd sys x preconds extracted-expr fail))
-               ((and (total-function? x)
-                     (is-a? x <defined-function>))
+               ((is-a? x <expandable-function>)
                 (cond
                  ((any (cut apply-rule '() <> extracted-expr '())
                        (function->rules x)) => identity)
@@ -792,8 +895,7 @@
                 (fail 'invalid-command cmd extracted-expr)))))
         (else (fail 'command-not-found cmd extracted-expr)))))))
 
-#;
-(define/guard (rewrite (sys system?) (expr (const #t)) (seq sequence?))
+(define/guard (rewrite (sys (cut is-a? <> <system>)) (expr (const #t)) (seq sequence?))
   (let ((expr (convert-to-expression expr)))
     (let loop ((expr expr)
                (seq seq))
@@ -856,226 +958,145 @@
           '())))
 
 (define (theorem->rules def)
-  (expression->rules (theorem-variables def)
+  (expression->rules (get-variables def)
                      '()
-                     (theorem-expression def)))
-
-;; (define current-system (make-parameter (make-system '() '() '())))
-
-
-;; (define (add-definition x)
-;;   (let ((sys (current-system)))
-;;     (current-system
-;;      (cond ((lookup (definition-name x) sys)
-;;             => (lambda (d)
-;;                  (if (equal? x d)
-;;                      sys
-;;                      (error "(vikalpa) add-definition: duplicated"
-;;                             (definition-name d)))))
-;;            (else (make-system (cons x (system-definitions sys))
-;;                               (system-proofs sys)
-;;                               (system-totality-claim-list sys)))))
-;;     x))
-
-;; (define (add-proof x)
-;;   (let ((sys (current-system)))
-;;     (current-system
-;;      (cond ((find-proof (proof-name x) sys)
-;;             => (lambda (prf)
-;;                  (if (equal? x prf)
-;;                      sys
-;;                      (error "add-proof: duplicated"))))
-;;            (else (make-system (system-definitions sys)
-;;                               (cons x (system-proofs sys))
-;;                               (system-totality-claim-list sys)))))
-;;     x))
-
-;; (define reserved-symbols '(quote let if error))
-;; (define (reserved? x)
-;;   (member x reserved-symbols))
-
-;; (define-syntax define-axiom
-;;   (syntax-rules ()
-;;     ((_ name (var ...) expr)
-;;      (let ((t (axiom 'name '(var ...)
-;;                      (convert-to-expression 'expr))))
-;;        (add-definition t)
-;;        (validate-definition t)
-;;        t))))
-
-;; (define-syntax define-theorem
-;;   (syntax-rules ()
-;;     ((_ name (var ...) expr)
-;;      (let ((t (theorem 'name '(var ...)
-;;                        (convert-to-expression 'expr))))
-;;        (add-definition t)
-;;        (validate-definition t)
-;;        t))))
-
-;; (define-syntax define-function
-;;   (syntax-rules ()
-;;     ((_ name (var ...) precond ... expr)
-;;      (let ((f (function 'name '(var ...)
-;;                         (convert-to-expression 'expr)
-;;                         '(precond ...)
-;;                         (code 'expr))))
-;;        (add-definition f)
-;;        (validate-definition f)
-;;        f))))
-
-;; (define-syntax define-primitive-function
-;;   (syntax-rules ()
-;;     ((_ name (var ...) precond ... expr)
-;;      (let ((f (primitive-function 'name '(var ...)
-;;                                   (convert-to-expression 'expr)
-;;                                   '(precond ...)
-;;                                   (code 'expr))))
-;;        (add-definition f)
-;;        (validate-definition f)
-;;        f))))
-
-;; (define-syntax define-core-function
-;;   (syntax-rules ()
-;;     ((_ name (var ...) precond ...)
-;;      (let ((f (primitive-function 'name '(var ...) #f '(precond ...) #f)))
-;;        (add-definition f)
-;;        f))))
+                     (get-expression def)))
 
-;; (define-syntax define-syntax-rules
-;;   (syntax-rules ()
-;;     ((_ name (l ...) ((lhs1 . lhs2) rhs) ...)
-;;      (let ((m (macro 'name
-;;                 (list (mrule '(lhs1 . lhs2) 'rhs)
-;;                       ...)
-;;                 '(l ...))))
-;;        (add-definition m)
-;;        m))))
-
-;; (define (find-totality-claim name sys)
-;;   (assoc name (system-totality-claim-list sys)))
-
-;; (define (add-totality-claim tc)
-;;   (let ((sys (current-system)))
-;;     (cond ((find-totality-claim (totality-claim-id tc) sys)
-;;            => (lambda (tc2)
-;;                 (unless (equal? tc tc2)
-;;                   (error "(vikalpa) define-totality-claim: duplicated"
-;;                          tc)))))
-;;     (unless (and (symbol? (totality-claim-id tc))
-;;                  (cond ((lookup (totality-claim-natural tc) sys)
-;;                         => function*?)
-;;                        (else #f))
-;;                  (cond ((lookup (totality-claim-less-than tc) sys)
-;;                         => function*?)
-;;                        (else #f)))
-;;       (error "(vikalpa) define-totality-claim: invalid totality-claim"
-;;              tc))
-;;     (current-system
-;;      (make-system (system-definitions sys)
-;;                   (system-proofs sys)
-;;                   (cons tc (system-totality-claim-list sys))))))
-
-;; (define-syntax-rule (define-totality-claim name nat? <)
-;;   (add-totality-claim (totality-claim 'name 'nat? '<)))
-
-;; (define core-function-names
-;;   '(not equal? pair? cons car cdr integer? < binary-+ unary--))
-
-;; (define (core-function-name? x)
-;;   (member x core-function-names))
-
-;; (define (rewrite/core name extracted-expr fail)
-;;   (case name
-;;     ((not)
-;;      (match extracted-expr
-;;        (('not `(quote ,x))
-;;         (expr-quote (not x)))
-;;        (else
-;;         (fail 'not extracted-expr))))
-;;     ((equal?)
-;;      (match extracted-expr
-;;        (('equal? `(quote ,x) `(quote ,y))
-;;         (expr-quote (equal? x y)))
-;;        (else
-;;         (fail 'equal? extracted-expr))))
-;;     ((pair?)
-;;      (match extracted-expr
-;;        (('pair? `(quote ,x))
-;;         (expr-quote (pair? x)))
-;;        (else
-;;         (fail 'pair? extracted-expr))))
-;;     ((cons)
-;;      (match extracted-expr
-;;        (('cons `(quote ,x) `(quote ,y))
-;;         (expr-quote (cons x y)))
-;;        (else
-;;         (fail 'cons extracted-expr))))
-;;     ((car)
-;;      (match extracted-expr
-;;        (('car `(quote ,x))
-;;         (if (pair? x)
-;;             (expr-quote (car x))
-;;             ''()))
-;;        (else
-;;         (fail 'car extracted-expr))))
-;;     ((cdr)
-;;      (match extracted-expr
-;;        (('cdr `(quote ,x))
-;;         (if (pair? x)
-;;             (expr-quote (cdr x))
-;;             ''()))
-;;        (else
-;;         (fail 'cdr extracted-expr))))
-;;     ((integer?)
-;;      (match extracted-expr
-;;        (('integer? `(quote ,x))
-;;         (expr-quote (integer? x)))
-;;        (else
-;;         (fail 'integer? extracted-expr))))
-;;     ((<)
-;;      (match extracted-expr
-;;        (('< `(quote ,x) `(quote ,y))
-;;         (let ((x (if (integer? x) x 0))
-;;               (y (if (integer? y) y 0)))
-;;           (expr-quote (< x y))))
-;;        (else
-;;         (fail '< extracted-expr))))
-;;     ((succ)
-;;      (match extracted-expr
-;;        (('binary-+ `(quote ,x) `(quote ,y))
-;;         (if (integer? x)
-;;             (if (integer? y)
-;;                 (expr-quote (+ x y))
-;;                 (expr-quote x))
-;;             (if (integer? y)
-;;                 (expr-quote y)
-;;                 (expr-quote 0))))
-;;        (else
-;;         (fail 'binary-+ extracted-expr))))
-;;     ((unary--)
-;;      (match extracted-expr
-;;        (('unary-- `(quote ,x))
-;;         (if (integer? x)
-;;             (expr-quote (- x))
-;;             (expr-quote 0)))
-;;        (else
-;;         (fail 'unary-- extracted-expr))))
-;;     (else (fail 'rewrite/core 'invalid))))
+(define current-system (make-parameter (make <system>)))
+(define reserved-symbols '(quote let if error))
+(define (reserved? x)
+  (member x reserved-symbols))
 
-;; (define-syntax define-system
-;;   (syntax-rules ()
-;;     ((_ name (systems ...) expr ...)
-;;      (define* (name #:optional (parent (make-system '() '() '())))
-;;        (parameterize ((current-system
-;;                        ((compose systems ... core-system) parent)))
-;;          expr
-;;          ...
-;;          (unless (system? (current-system))
-;;            (error "define-system: invalid system"))
-;;          (current-system))))))
+(define-syntax define-axiom
+  (syntax-rules ()
+    ((_ name (var ...) expr)
+     (let ((t (make <axiom>
+                #:name 'name
+                #:variables '(var ...)
+                #:expression (convert-to-expression 'expr))))
+       (current-system (add-definition t (current-system)))
+       (validate t)
+       t))))
+
+(define-syntax define-theorem
+  (syntax-rules ()
+    ((_ name (var ...) expr)
+     (let ((t (make <conjecture>
+                #:name 'name
+                #:variables '(var ...)
+                #:expression (convert-to-expression 'expr))))
+       (current-system (add-definition t (current-system)))
+       (validate t)
+       t))))
+
+(define-syntax define-core-function
+  (syntax-rules ()
+    ((_ name (var ...) precond ... proc)
+     (let ((f (make <core-function>
+                #:name 'name
+                #:variables '(var ...)
+                #:condition '(precond ...)
+                #:procedure proc)))
+       (current-system (add-definition f (current-system)))
+       (validate f)
+       f))))
+
+(define-syntax define-function
+  (syntax-rules ()
+    ((_ name (var ...) precond ... expr)
+     (let ((f (make <function>
+                #:name 'name
+                #:variables '(var ...)
+                #:condition '(precond ...)
+                #:expression (convert-to-expression 'expr)
+                #:precond '(precond ...)
+                #:code 'expr)))
+       (current-system (add-definition f (current-system)))
+       (validate f)
+       f))))
+
+(define-syntax define-trivial-total-function
+  (syntax-rules ()
+    ((_ name (var ...) precond ... expr)
+     (let ((f (make <trivial-total-function>
+                #:name 'name
+                #:variables '(var ...)
+                #:condition '(precond ...)
+                #:expression (convert-to-expression 'expr)
+                #:precond '(precond ...)
+                #:code 'expr)))
+       (current-system (add-definition f (current-system)))
+       (validate f)
+       f))))
+
+(define-syntax define-syntax-rules
+  (syntax-rules ()
+    ((_ name (l ...) ((lhs1 . lhs2) rhs) ...)
+     (let ((m (macro 'name
+                (list (mrule '(lhs1 . lhs2) 'rhs)
+                      ...)
+                '(l ...))))
+       (current-system (add-definition m (current-system)))
+       m))))
+
+(define-syntax define-system
+  (syntax-rules ()
+    ((_ name (systems ...) expr ...)
+     (define* (name #:optional (parent (make <system>)))
+       (parameterize ((current-system
+                       ((compose systems ... identity) parent)))
+         expr
+         ...
+         (current-system))))))
+
+(define (validate-function-name desc name)
+  (define (err)
+    (raise-exception
+     (make-exception
+      (make-exception-with-message
+       (string-append "(vikalpa) " desc ": unbound function"))
+      (make-exception-with-irritants name))))
+  (cond
+   ((lookup name (current-system))
+    => (lambda (f)
+         (if (is-a? f <function*>)
+             name
+             (err))))
+   (else (err))))
+
+(define-syntax set-natural-predicate
+  (syntax-rules ()
+    ((_ name)
+     (begin
+       (validate-function-name "set-natural-predicate" 'name)
+       (current-system (update-natural-predicate 'name (current-system)))))))
+
+(define-syntax set-natural-less-than
+  (syntax-rules ()
+    ((_ name)
+     (begin
+       (validate-function-name "set-natural-less-than" 'name)
+       (current-system
+        (update-natural-less-than 'name (current-system)))))))
+
+(define-syntax set-ordinal-predicate
+  (syntax-rules ()
+    ((_ name)
+     (begin
+       (validate-function-name "set-ordinal-predicate" 'name)
+       (current-system
+        (update-ordinal-predicate 'name (current-system)))))))
+
+(define-syntax set-ordinal-less-than
+  (syntax-rules ()
+    ((_ name)
+     (begin
+       (validate-function-name "set-ordinal-less-than" 'name)
+       (current-system
+        (update-natural-less-than 'name (current-system)))))))
 
 (define (defined-function-app-form f)
-  (cons (definition-name f) (function-variables f)))
+  (app-form (get-name f) (get-variables f)))
 
 (define (single? x)
   (and (pair? x)
@@ -1107,104 +1128,109 @@
    (else
     (if/if x y ''#t))))
 
-;; (define (make-totality-claim tc m-expr f)
-;;   (let* ((name (function-name f)))
-;;     (define (convert app-form)
-;;       (cond
-;;        ((apply-rule '()
-;;                     (rule (function-vars f)
-;;                           '()
-;;                           (function-app-form f)
-;;                           m-expr)
-;;                     app-form
-;;                     '())
-;;         => identity)
-;;        (else (error "make-totality-claim: convert error"
-;;                     (function-name f)
-;;                     m-expr
-;;                     app-form))))
-;;     (if/if `(,(totality-claim-natural tc) ,m-expr)
-;;            (let loop ((expr (function-expression f)))
-;;              (cond
-;;               ((expr-quoted? expr) ''#t)
-;;               ((variable? expr) ''#t)
-;;               ((if-form? expr)
-;;                (let ((test/result (loop (if-form-test expr)))
-;;                      (then/result (loop (if-form-then expr)))
-;;                      (else/result (loop (if-form-else expr))))
-;;                  (and/if test/result
-;;                          (if/if (if-form-test expr)
-;;                                 then/result
-;;                                 else/result))))
-;;               ((app-form? expr)
-;;                (let ((rest
-;;                       (let f ((args (app-form-args expr)))
-;;                         (cond ((null? args) ''#t)
-;;                               ((single? args) (loop (car args)))
-;;                               (else (and/if (loop (car args))
-;;                                             (f (cdr args))))))))
-;;                  (if (eq? name (app-form-name expr))
-;;                      (and/if `(,(totality-claim-less-than tc)
-;;                                ,(convert expr)
-;;                                ,m-expr)
-;;                              rest)
-;;                      rest)))
-;;               (else (error "(vikalpa) make-totality-claim: error"
-;;                            (function-name f)
-;;                            m-expr))))
-;;            ''#f)))
-
-;; (define (make-guard-claim expr sys)
-;;   (define (find-preconds expr)
-;;     (cond
-;;      ((app-form? expr)
-;;       (let ((rest (append-map find-preconds (cdr expr))))
-;;         (append (cond ((lookup (car expr) sys) =>
-;;                        (lambda (f)
-;;                          (let ((preconds (function-guard f)))
-;;                            (map (lambda (precond)
-;;                                   (substitute (map cons
-;;                                                    (function-vars f)
-;;                                                    (cdr expr))
-;;                                               precond))
-;;                                 preconds))))
-;;                       (else (error "make-guard-claim: error")))
-;;                 rest)))
-;;      ((if-form? expr)
-;;       (find-preconds (if-form-test expr)))
-;;      (else '())))
-;;   (define (build/find-if expr)
-;;     (cond
-;;      ((if-form? expr)
-;;       (if/if (build/find-if (if-form-test expr))
-;;              (build (if-form-then expr))
-;;              (build (if-form-else expr))))
-;;      ((app-form? expr)
-;;       (apply and/if (map build/find-if (app-form-args expr))))
-;;      (else ''#t)))
-;;   (define (build expr)
-;;     (cond
-;;      ((if-form? expr)
-;;       (apply and/if
-;;              (append (find-preconds (if-form-test expr))
-;;                      (list (if/if (if-form-test expr)
-;;                                   (build (if-form-then expr))
-;;                                   (build (if-form-else expr)))))))
-;;      ((app-form? expr)
-;;       (apply and/if
-;;              (append (find-preconds expr)
-;;                      (list (build/find-if expr)))))
-;;      (else ''#t)))
-;;   (if/if (build expr)
-;;          ''#t
-;;          ''#f))
+(define-class <totality-claim-method> ()
+  (id #:getter totality-claim-id #:init-keyword #:id)
+  (natural #:getter totality-claim-natural #:init-keyword #:natural)
+  (less-than #:getter totality-claim-less-than #:init-keyword #:less-than))
+
+(define (make-totality-claim tc m-expr f)
+  (let* ((name (get-name f)))
+    (define (convert app-form)
+      (cond
+       ((apply-rule '()
+                    (rule (get-variables f)
+                          '()
+                          (defined-function-app-form f)
+                          m-expr)
+                    app-form
+                    '())
+        => identity)
+       (else (error "make-totality-claim: convert error"
+                    (get-name f)
+                    m-expr
+                    app-form))))
+    (if/if `(,(totality-claim-natural tc) ,m-expr)
+           (let loop ((expr (get-expression f)))
+             (cond
+              ((expr-quoted? expr) ''#t)
+              ((variable? expr) ''#t)
+              ((if-form? expr)
+               (let ((test/result (loop (if-form-test expr)))
+                     (then/result (loop (if-form-then expr)))
+                     (else/result (loop (if-form-else expr))))
+                 (and/if test/result
+                         (if/if (if-form-test expr)
+                                then/result
+                                else/result))))
+              ((app-form? expr)
+               (let ((rest
+                      (let f ((args (app-form-args expr)))
+                        (cond ((null? args) ''#t)
+                              ((single? args) (loop (car args)))
+                              (else (and/if (loop (car args))
+                                            (f (cdr args))))))))
+                 (if (eq? name (app-form-name expr))
+                     (and/if `(,(totality-claim-less-than tc)
+                               ,(convert expr)
+                               ,m-expr)
+                             rest)
+                     rest)))
+              (else (error "(vikalpa) make-totality-claim: error"
+                           (get-name f)
+                           m-expr))))
+           ''#f)))
+
+(define (make-guard-claim expr sys)
+  (define (find-preconds expr)
+    (cond
+     ((app-form? expr)
+      (let ((rest (append-map find-preconds (cdr expr))))
+        (append (cond ((lookup (car expr) sys) =>
+                       (lambda (f)
+                         (let ((preconds (get-condition f)))
+                           (map (lambda (precond)
+                                  (substitute (map cons
+                                                   (get-variables f)
+                                                   (cdr expr))
+                                              precond))
+                                preconds))))
+                      (else (error "make-guard-claim: error")))
+                rest)))
+     ((if-form? expr)
+      (find-preconds (if-form-test expr)))
+     (else '())))
+  (define (build/find-if expr)
+    (cond
+     ((if-form? expr)
+      (if/if (build/find-if (if-form-test expr))
+             (build (if-form-then expr))
+             (build (if-form-else expr))))
+     ((app-form? expr)
+      (apply and/if (map build/find-if (app-form-args expr))))
+     (else ''#t)))
+  (define (build expr)
+    (cond
+     ((if-form? expr)
+      (apply and/if
+             (append (find-preconds (if-form-test expr))
+                     (list (if/if (if-form-test expr)
+                                  (build (if-form-then expr))
+                                  (build (if-form-else expr)))))))
+     ((app-form? expr)
+      (apply and/if
+             (append (find-preconds expr)
+                     (list (build/find-if expr)))))
+     (else ''#t)))
+  (if/if (build expr)
+         ''#t
+         ''#f))
 
 (define (make-induction-claim f vars c)
   (define (find-app-forms expr)
     (cond
      ((app-form? expr)
       (let ((rest (append-map find-app-forms (cdr expr))))
-        (if (eq? (definition-name f) (app-form-name expr))
+        (if (eq? (get-name f) (app-form-name expr))
             (cons expr rest)
             rest)))
      ((if-form? expr)
@@ -1216,7 +1242,7 @@
      ((apply-rule '()
                   (rule vars
                         '()
-                        (app-form (definition-name f) vars)
+                        (app-form (get-name f) vars)
                         c)
                   app-form
                   '())
@@ -1242,27 +1268,7 @@
    (else (error "make-induction-claim: invalid"
                 f vars c))))
 
-;; (define (proof? x)
-;;   (and (list? x)
-;;        (= 4 (length x))
-;;        (symbol? (proof-name x))
-;;        (eq? 'proof (list-ref x 1))
-;;        (seed? (proof-seed x))
-;;        (sequence? (proof-sequence x))))
-
-;; (define (proof name seed sequence)
-;;   (list name 'proof seed sequence))
-
-;; (define (proof-name x)
-;;   (list-ref x 0))
-
-;; (define (proof-seed x)
-;;   (list-ref x 2))
-
-;; (define (proof-sequence x)
-;;   (list-ref x 3))
-
-;; (define seed? (const #t))
+(define seed? (const #t))
 
 ;; (define-syntax define-proof
 ;;   (syntax-rules ()
@@ -1278,48 +1284,69 @@
 ;;                        '(seed ...)
 ;;                        '(((n ...) cmd ...) ...))))))
 
-;; (define (function*? x)
-;;   (or (function? x)
-;;       (primitive-function? x)))
-
-;; (define (validate-expression sys name vars expr)
-;;   (let* ((expr-fnames (expression-functions expr))
-;;          (expr-vars (expression-vars expr)))
-;;     (when (reserved? name)
-;;       (error (format #f "(vikalpa) ~a: reserved name" name)))
-;;     (for-each (lambda (x)
-;;                 (when (member x expr-fnames)
-;;                   (error (format #f "(vikalpa) ~a: invalid variable name" name)
-;;                          x)))
-;;               vars)
-;;     (for-each (lambda (x)
-;;                 (unless (cond ((lookup x sys) => function*?)
-;;                               (else #f))
-;;                   (error (format #f "(vikalpa) ~a: undefined function" name)
-;;                          x)))
-;;               expr-fnames)
-;;     (for-each (lambda (x)
-;;                 (unless (member x vars)
-;;                   (error (format #f "(vikalpa) ~a: undefined variable" name)
-;;                          x)))
-;;               expr-vars)))
-
-;; (define (validate-definition d)
-;;   (let* ((vars (definition-vars d))
-;;          (name (definition-name d))
-;;          (expr (definition-expression d)))
-;;     (validate-expression (current-system) name vars expr)))
-
-;; (define (recur? f)
-;;   (member (function-name f)
-;;           (expression-functions (function-expression f))))
-
-;; (define (p x)
-;;   (format #t "p:~%~y" x)
-;;   x)
-
-;; (define (trivial-total? f sys)
-;;   (and (not (recur? f))))
+
+(define (validate-expression sys name vars expr)
+  (let* ((expr-fnames (expression-functions expr))
+         (expr-vars (expression-vars expr))
+         (expr-app-forms (expression-app-forms expr)))
+    (define (err msg x)
+      (raise-exception
+       (make-exception
+        (make-exception-with-message
+         (format #f "(vikalpa) ~a: ~a" name msg))
+        (make-exception-with-irritants x))))
+    (for-each (lambda (x)
+                (when (member x expr-fnames)
+                  (err "invalid variable" x)))
+              vars)
+    (for-each (lambda (fname)
+                (unless (cond
+                         ((lookup fname sys) =>
+                          (lambda (f)
+                            (for-each
+                             (lambda (app-form)
+                               (when (equal? fname (app-form-name app-form))
+                                 (unless (= (length (get-variables f))
+                                            (length (app-form-args app-form)))
+                                   (err (format
+                                         #f
+                                         "~a :wrong number of arguments ~s"
+                                         (get-name f)
+                                         (get-variables f))
+                                        (app-form-args app-form)))))
+                             expr-app-forms)
+                            #t))
+                         (else #f))
+                  (err "undefined function" fname)))
+              expr-fnames)
+    (for-each (lambda (x)
+                (unless (member x vars)
+                  (err "undefined variable" x)))
+              expr-vars)))
+
+(define (dup? xs)
+  (if (null? xs)
+      #f
+      (if (member (car xs) (cdr xs))
+          #t
+          (dup? (cdr xs)))))
+
+(define (validate-vars desc vars)
+  (define (err)
+    (raise-exception
+     (make-exception
+      (make-exception-with-message
+       (string-append "(vikalpa) " desc ": duplicated variable"))
+      (make-exception-with-irritants vars))))
+  (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 (prove sys def pf)
 ;;   (cond
@@ -1332,7 +1359,7 @@
 ;; (define (prove/theorem sys t pf)
 ;;   (let ((sys-without-self
 ;;          (make-system (filter (lambda (d) (not (equal? t d)))
-;;                               (system-definitions sys))
+;;                               (get-definitions sys))
 ;;                       (system-proofs sys)
 ;;                       (system-totality-claim-list sys))))
 ;;     (rewrite sys-without-self
@@ -1371,12 +1398,12 @@
 ;;             (reverse (filter (lambda (x)
 ;;                                (and (function*? x)
 ;;                                     (function-code x)))
-;;                              (system-definitions sys))))))
+;;                              (get-definitions sys))))))
 
 ;; (define/guard (check (sys system?))
 ;;   (let loop ((sys sys)
 ;;              (fails '()))
-;;     (let ((defs (system-definitions sys)))
+;;     (let ((defs (get-definitions sys)))
 ;;       (define* (next #:optional fail)
 ;;         (loop (make-system (cdr defs)
 ;;                            (system-proofs sys)
@@ -1394,17 +1421,17 @@
 ;;           (next))
 ;;          (else
 ;;           (cond
-;;            ((find-proof (definition-name (car defs)) sys)
+;;            ((find-proof (get-name (car defs)) sys)
 ;;             => (lambda (pf)
 ;;                  (let ((result (prove sys (car defs) pf)))
 ;;                    (cond
 ;;                     ((equal? result ''#t)
 ;;                      (next))
 ;;                     (else
-;;                      (next (list (definition-name (car defs))
+;;                      (next (list (get-name (car defs))
 ;;                                  result)))))))
 ;;            (else
-;;             (next (list (definition-name (car defs)))))))))
+;;             (next (list (get-name (car defs)))))))))
 ;;        (else
 ;;         (next))))))
 
@@ -1426,7 +1453,7 @@
 ;;            `(define-primitive-function
 ;;               ,(function-name def)
 ;;               ,(function-vars def)))
-;;           ((macro? def)
+;;           (((cut is-a? <> <macro>) def)
 ;;            `(define-syntax-rules ,(macro-name def)))
 ;;           (else
 ;;            `(error 'fatal-error ,name)))))
@@ -1440,27 +1467,123 @@
 ;;   (append reserved-symbols
 ;;           (map function-name
 ;;                (filter primitive-function?
-;;                        (system-definitions sys)))))
+;;                        (get-definitions sys)))))
 
 ;; (define/guard (system-functions (sys system?))
 ;;   (map function-name
 ;;        (filter function?
-;;                (system-definitions sys))))
+;;                (get-definitions sys))))
 
 ;; (define/guard (system-theorems (sys system?))
 ;;   (map theorem-name
 ;;        (filter theorem?
-;;                (system-definitions sys))))
+;;                (get-definitions sys))))
 
 ;; (define/guard (system-axioms (sys system?))
 ;;   (map theorem-name
 ;;        (filter axiom?
-;;                (system-definitions sys))))
+;;                (get-definitions sys))))
 
 ;; (define/guard (system-macros (sys system?))
 ;;   (map macro-name
-;;        (filter macro?
-;;                (system-definitions sys))))
+;;        (filter (cut is-a? <> <macro>)
+;;                (get-definitions sys))))
 
 ;; (define/guard (system-totality-claims (sys system?))
 ;;   (system-totality-claim-list 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))))
+  (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) +)
+  (set-natural-predicate natural?)
+  (set-natural-less-than <)
+  (define-trivial-total-function size (x)
+    (if (not (pair? x))
+        0
+        (+ 1
+           (+ (size (car x))
+              (size (cdr x))))))
+
+  (define-syntax-rules and ()
+    ((and) '#t)
+    ((and x) x)
+    ((and x . xs) (if x (and . xs) #f)))
+
+  (define-syntax-rules or ()
+    ((or) '#f)
+    ((or x) x)
+    ((or x . xs) (if x x (or . xs))))
+
+  (define-syntax-rules cond (else)
+    ((cond (else e)) e)
+    ((cond (test then) . rest)
+     (if test then (cond . rest))))
+
+  (define-syntax-rules implies ()
+    ((implies x y) (if x y #t))
+    ((implies x y z . rest)
+     (if x (implies y z . rest) #t)))
+  
+  (define-axiom if-nest (x y z)
+    (if x
+        (equal? (if x y z) y)
+        (equal? (if x y z) z)))
+
+  (define-axiom if-true (x y)
+    (equal? (if '#t x y) x))
+
+  (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 if-not (x y z)
+    (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))
+
+  (define-axiom cons/car+cdr (x)
+    (implies (pair? x)
+             (equal? (cons (car x) (cdr x)) x)))
+
+  (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 equal-car (x1 y1 x2 y2)
+    (implies (equal? (cons x1 y1) (cons x2 y2))
+             (equal? x1 x2)))
+  (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))))
-- 
cgit v1.2.3