From 8e54a6de230cf79702f493531ea32f8bddb4d93c Mon Sep 17 00:00:00 2001
From: Masaya Tojo <masaya@tojo.tokyo>
Date: Sun, 13 Dec 2020 13:09:05 +0900
Subject: wip55

---
 vikalpa.scm | 623 +++++++++++++++++++++++++++++++-----------------------------
 1 file changed, 325 insertions(+), 298 deletions(-)

diff --git a/vikalpa.scm b/vikalpa.scm
index bff63f0..e7126f8 100644
--- a/vikalpa.scm
+++ b/vikalpa.scm
@@ -17,31 +17,24 @@
 ;;; along with Vikalpa.  If not, see <http://www.gnu.org/licenses/>.
 
 (define-module (vikalpa)
-  #:export () ;; (rewrite
-           ;;  show
-           ;;  check
-           ;;  system->scheme
-           ;;  load-system
-           ;;  system-primitives
-           ;;  system-functions
-           ;;  system-macros
-           ;;  system-theorems
-           ;;  system-axioms
-           ;;  system-totality-claims
-           ;;  define-system
-           ;;  define-axiom
-           ;;  define-theorem
-           ;;  define-primitive-function
-           ;;  define-function
-           ;;  define-scheme-function
-           ;;  define-proof
-           ;;  define-totality-claim
-           ;;  define-syntax-rules
-           ;;  system-eval)
+  #:export (rewrite
+            describe
+            system-check
+            system-apropos
+            system-code
+            system-load
+            set-measure-predicate
+            set-measure-less-than
+            define-system
+            define-proof
+            define-core-function
+            define-function
+            define-theorem)
   #:use-module (ice-9 match)
   #:use-module (ice-9 format)
   #:use-module (ice-9 control)
   #: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))
@@ -56,13 +49,9 @@
     #:getter get-definitions
     #:init-keyword #:definitions
     #:init-value '())
-  (natural-predicate #:getter get-natural-predicate
+  (measure-predicate #:getter get-measure-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
+  (measure-less-than #:getter get-measure-less-than
                      #:init-value #f))
 
 (define-class <definition> ()
@@ -85,27 +74,27 @@
 (define-class <theorem> (<theorem*> <proved>))
 (define-class <axiom> (<theorem*>))
 
-(define-class <condition> ()
-  (expressions #:getter get-expressions #:init-keyword #:expressions))
-
 (define-class <function*> (<definition>)
-  (condition #:getter get-condition #:init-keyword #:condition))
+  (conditions #:getter get-conditions #:init-keyword #:conditions))
 (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))
+  (code #:getter get-code #:init-keyword #:code))
 (define-class <function> (<expandable-function> <provable>))
 (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))
+
 (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*>)
@@ -115,6 +104,8 @@
           (length (filter (cut is-a? <> <macro>)
                           (get-definitions s)))))
 
+(define-method (write (d <macro>) port)
+  (write-definition 'macro d port))
 (define-method (write (d <conjecture>) port)
   (write-definition 'conjecture d port))
 (define-method (write (d <theorem>) port)
@@ -126,7 +117,7 @@
 (define-method (write (d <function>) port)
   (write-definition 'function d port))
 (define-method (write (d <core-function>) port)
-  (write-definition 'function d port))
+  (write-definition 'core-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)
@@ -138,53 +129,60 @@
           (eq? name (get-name x)))
         (get-definitions s)))
 
-(define-generic update-natural-predicate)
-(define-method (update-natural-predicate (s <symbol>) (sys <system>))
+(define-generic update-measure-predicate)
+(define-method (update-measure-predicate (s <symbol>) (sys <system>))
   (let ((new (shallow-clone sys)))
-    (slot-set! new 'natural-predicate s)
+    (slot-set! new 'measure-predicate s)
     new))
 
-(define-generic update-natural-less-than)
-(define-method (update-natural-less-than (s <symbol>) (sys <system>))
+(define-generic update-measure-less-than)
+(define-method (update-measure-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)
+    (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)
+        (raise-exception
+         (make-exception
+          (make-exception-with-origin 'update-definition)
+          (make-exception-with-message "not found")
+          (make-exception-with-irritants (list d defs))))
+        (if (equal? (get-name d) (get-name (car defs)))
+            (cons d (cdr defs))
+            (cons (car defs) (update d (cdr defs))))))
   (let ((new (shallow-clone sys)))
     (slot-set! new 'definitions
-               (cons d (get-definitions sys)))
+               (update d (get-definitions sys)))
     new))
-
-(define-generic update-definition)
-(define-method (update-definition (d <definition>) (sys <system>))
+(define-generic remove-first-definition)
+(define-method (remove-first-definition (sys <system>))
   (let ((new (shallow-clone sys)))
     (slot-set! new 'definitions
-               (cons d (get-definitions sys)))
+               (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
        (make-exception
-        (make-exception-with-message
-         "(vikalpa) add-definition: duplicated definition")
+        (make-exception-with-origin 'add-definition)
+        (make-exception-with-message "duplicated definition")
         (make-exception-with-irritants (get-name d))))
-      (update-definition d s)))
+      (let ((new (shallow-clone s)))
+        (slot-set! new 'definitions
+                   (cons d (get-definitions s)))
+        new)))
 
 (define-generic validate)
 (define-method (validate (d <definition>))
@@ -229,16 +227,15 @@
         (m p?)
         (n t? getter-var getter) ...)
      (begin
-       (define len (+ 1 (length (list n ...))))
        (define (constractor getter-var ...)
-         (let ((data (make-list len)))
+         (let ((data (make-list (+ 1 (length (list t? ...))))))
            (list-set! data m 'name)
            (list-set! data n getter-var)
            ...
            data))
        (define (p? x)
          (and (list? x)
-              (= len (length x))
+              (= (+ 1 (length (list t? ...))) (length x))
               (eq? 'name (list-ref x m))
               (t? (list-ref x n)) ...))
        (define (getter x)
@@ -520,11 +517,14 @@
      expr
      code-expr))
 
-(define-type mrule
-  mrule
-  (0 mrule?)
-  (1 (const #t) lhs mrule-lhs)
-  (2 (const #t) rhs mrule-rhs))
+(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))
+
+(define (mrule lhs rhs)
+  (make <mrule> #:lhs lhs #:rhs rhs))
 
 (define (mrule-vars mrl)
   (define (all-vars x)
@@ -536,12 +536,6 @@
           (else '())))
   (all-vars (mrule-lhs mrl)))
 
-(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
@@ -620,10 +614,11 @@
              (expr expr))
     (cond
      ((null? ms) expr)
-     (else (expand (cdr ms)
-                   (cond
-                    ((apply-macro (car ms) expr) => identity)
-                    (else expr)))))))
+     (else
+      (expand (cdr ms)
+              (cond
+               ((apply-macro (car ms) expr) => identity)
+               (else expr)))))))
 
 (define (expand* ms expr)
   (let loop ((ms ms)
@@ -817,11 +812,11 @@
 
 (define (function->rules x)
   (list (rule (get-variables x)
-              (get-expressions (get-condition x))
+              (get-conditions x)
               (defined-function-app-form x)
               (get-expression x))
         (rule (get-variables x)
-              (get-expressions (get-condition x))
+              (get-conditions x)
               (get-expression x)
               (defined-function-app-form x))))
 
@@ -859,7 +854,7 @@
 (define (rewrite/induction sys fname vars expr fail)
   (cond
    ((lookup fname sys)
-    (cut make-induction-claim <> vars expr))
+    => (cut make-induction-claim <> vars expr))
    (else (fail 'induction 'not-found fname))))
 
 (define (rewrite1 sys expr fail r)
@@ -872,13 +867,6 @@
        (cond
         ((equal? '(eval) cmd/name)
          (rewrite/eval extracted-expr sys))
-        ((match cmd/name
-           (`(induction ,(f . vars))
-            (rewrite/induction sys f vars extracted-expr fail))
-           (`(induction . ,x)
-            (fail 'induction x))
-           (else #f)) => identity)
-        ((eq? 'error cmd/name) (fail extracted-expr))
         ((and (symbol? cmd/name)
               (lookup cmd/name sys))
          => (lambda (x)
@@ -888,14 +876,15 @@
                ((is-a? x <expandable-function>)
                 (cond
                  ((any (cut apply-rule '() <> extracted-expr '())
-                       (function->rules x)) => identity)
+                       (function->rules x))
+                  => identity)
                  (else
                   (fail 'apply-function cmd extracted-expr))))
                (else
                 (fail 'invalid-command cmd extracted-expr)))))
         (else (fail 'command-not-found cmd extracted-expr)))))))
 
-(define/guard (rewrite (sys (cut is-a? <> <system>)) (expr (const #t)) (seq sequence?))
+(define/guard (rewrite (sys (cut is-a? <> <system>)) (expr (const #t)) (seq (const #t)))
   (let ((expr (convert-to-expression expr)))
     (let loop ((expr expr)
                (seq seq))
@@ -995,7 +984,7 @@
      (let ((f (make <core-function>
                 #:name 'name
                 #:variables '(var ...)
-                #:condition '(precond ...)
+                #:conditions '(precond ...)
                 #:procedure proc)))
        (current-system (add-definition f (current-system)))
        (validate f)
@@ -1007,10 +996,22 @@
      (let ((f (make <function>
                 #:name 'name
                 #:variables '(var ...)
-                #:condition '(precond ...)
+                #:conditions '(precond ...)
                 #:expression (convert-to-expression 'expr)
-                #:precond '(precond ...)
-                #:code '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))))
        (current-system (add-definition f (current-system)))
        (validate f)
        f))))
@@ -1021,10 +1022,9 @@
      (let ((f (make <trivial-total-function>
                 #:name 'name
                 #:variables '(var ...)
-                #:condition '(precond ...)
+                #:conditions '(precond ...)
                 #:expression (convert-to-expression 'expr)
-                #:precond '(precond ...)
-                #:code 'expr)))
+                #:code (code 'expr))))
        (current-system (add-definition f (current-system)))
        (validate f)
        f))))
@@ -1053,8 +1053,8 @@
   (define (err)
     (raise-exception
      (make-exception
-      (make-exception-with-message
-       (string-append "(vikalpa) " desc ": unbound function"))
+      (make-exception-with-origin 'desc)
+      (make-exception-with-message "unbound function")
       (make-exception-with-irritants name))))
   (cond
    ((lookup name (current-system))
@@ -1064,36 +1064,20 @@
              (err))))
    (else (err))))
 
-(define-syntax set-natural-predicate
+(define-syntax set-measure-predicate
   (syntax-rules ()
     ((_ name)
      (begin
-       (validate-function-name "set-natural-predicate" 'name)
-       (current-system (update-natural-predicate 'name (current-system)))))))
+       (validate-function-name 'set-measure-predicate 'name)
+       (current-system (update-measure-predicate 'name (current-system)))))))
 
-(define-syntax set-natural-less-than
+(define-syntax set-measure-less-than
   (syntax-rules ()
     ((_ name)
      (begin
-       (validate-function-name "set-natural-less-than" 'name)
+       (validate-function-name 'set-measure-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)))))))
+        (update-measure-less-than 'name (current-system)))))))
 
 (define (defined-function-app-form f)
   (app-form (get-name f) (get-variables f)))
@@ -1128,12 +1112,7 @@
    (else
     (if/if x y ''#t))))
 
-(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)
+(define (make-totality-claim* sys m-expr f)
   (let* ((name (get-name f)))
     (define (convert app-form)
       (cond
@@ -1149,7 +1128,7 @@
                     (get-name f)
                     m-expr
                     app-form))))
-    (if/if `(,(totality-claim-natural tc) ,m-expr)
+    (if/if `(,(get-measure-predicate sys) ,m-expr)
            (let loop ((expr (get-expression f)))
              (cond
               ((expr-quoted? expr) ''#t)
@@ -1170,7 +1149,7 @@
                               (else (and/if (loop (car args))
                                             (f (cdr args))))))))
                  (if (eq? name (app-form-name expr))
-                     (and/if `(,(totality-claim-less-than tc)
+                     (and/if `(,(get-measure-less-than sys)
                                ,(convert expr)
                                ,m-expr)
                              rest)
@@ -1187,7 +1166,7 @@
       (let ((rest (append-map find-preconds (cdr expr))))
         (append (cond ((lookup (car expr) sys) =>
                        (lambda (f)
-                         (let ((preconds (get-condition f)))
+                         (let ((preconds (get-conditions f)))
                            (map (lambda (precond)
                                   (substitute (map cons
                                                    (get-variables f)
@@ -1237,14 +1216,14 @@
       (error "make-induction-claim(find-app-forms): not supported"
              expr))
      (else '())))
-  (define (prop app-form)
+  (define (prop form)
     (cond
      ((apply-rule '()
                   (rule vars
                         '()
                         (app-form (get-name f) vars)
                         c)
-                  app-form
+                  form
                   '())
       => identity)
      (else
@@ -1268,22 +1247,86 @@
    (else (error "make-induction-claim: invalid"
                 f vars c))))
 
-(define seed? (const #t))
-
-;; (define-syntax define-proof
-;;   (syntax-rules ()
-;;     ((_ name
-;;         (((n ...) cmd ...) ...))
-;;      (add-proof (proof 'name
-;;                        '()
-;;                        '(((n ...) cmd ...) ...))))
-;;     ((_ name
-;;         (seed ...)
-;;         (((n ...) cmd ...) ...))
-;;      (add-proof (proof 'name
-;;                        '(seed ...)
-;;                        '(((n ...) cmd ...) ...))))))
+(define (add-proof/function sys f seed 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)
+      (raise-exception
+       (make-exception
+        (make-exception-with-origin 'define-proof)
+        (make-exception-with-message "need seed")
+        (make-exception-with-irritants (get-expression f))))))
+
+(define (add-proof/theorem sys t seed 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)))))
+    (update-definition (make <theorem>
+                         #:name (get-name t)
+                         #:variables (get-variables t)
+                         #:expression (get-expression t)
+                         #:claim claim
+                         #:proof seq)
+                       sys)))
+
+(define (add-proof sys name seed seq)
+  (cond
+   ((not (sequence? seq))
+    (raise-exception
+     (make-exception
+      (make-exception-with-origin 'define-proof)
+      (make-exception-with-message "not sequence")
+      (make-exception-with-irritants seq))))
+   ((lookup name sys)
+    => (lambda (def)
+         (current-system
+          (if (and (is-a? def <provable>)
+                   (not (is-a? def <proved>)))
+              (cond
+               ((is-a? def <function>)
+                (add-proof/function sys def seed seq))
+               ((is-a? def <conjecture>)
+                (add-proof/theorem sys def seed seq))
+               (else
+                (raise-exception
+                 (make-exception
+                  (make-exception-with-origin 'define-proof)
+                  (make-exception-with-message "error")
+                  (make-exception-with-irritants def)))))
+              (raise-exception
+               (make-exception
+                (make-exception-with-origin 'define-proof)
+                (make-exception-with-message "not provable definition")
+                (make-exception-with-irritants def)))))))
+   (else
+    (raise-exception
+     (make-exception
+      (make-exception-with-origin 'define-proof)
+      (make-exception-with-message "definition is not found")
+      (make-exception-with-irritants name))))))
 
+(define-syntax define-proof
+  (syntax-rules ()
+    ((_ name
+        seed
+        seq)
+     (add-proof (current-system)
+                'name
+                'seed
+                'seq))
+    ((_ name seq)
+     (define-proof name #f seq))))
 
 (define (validate-expression sys name vars expr)
   (let* ((expr-fnames (expression-functions expr))
@@ -1292,8 +1335,8 @@
     (define (err msg x)
       (raise-exception
        (make-exception
-        (make-exception-with-message
-         (format #f "(vikalpa) ~a: ~a" name msg))
+        (make-exception-with-origin name)
+        (make-exception-with-message msg)
         (make-exception-with-irritants x))))
     (for-each (lambda (x)
                 (when (member x expr-fnames)
@@ -1348,149 +1391,89 @@
 (define (trivial-total? f sys)
   (and (not (recur? f))))
 
-;; (define (prove sys def pf)
-;;   (cond
-;;    ((theorem? def)
-;;     (prove/theorem sys def pf))
-;;    ((function? def)
-;;     (prove/function sys def pf))
-;;    (else (error "prove" def pf))))
-
-;; (define (prove/theorem sys t pf)
-;;   (let ((sys-without-self
-;;          (make-system (filter (lambda (d) (not (equal? t d)))
-;;                               (get-definitions sys))
-;;                       (system-proofs sys)
-;;                       (system-totality-claim-list sys))))
-;;     (rewrite sys-without-self
-;;              (theorem-expression t)
-;;              (proof-sequence pf))))
-
-;; (define (prove/function sys f pf)
-;;   (match (proof-seed pf)
-;;     (()
-;;      (error "prove/function error"))
-;;     ((id m-expr)
-;;      (cond
-;;       ((find-totality-claim id sys)
-;;        => (lambda (tc)
-;;             (let ((claim (make-totality-claim tc m-expr f)))
-;;               (validate-expression sys
-;;                                    `(claim-of ,(function-name f))
-;;                                    (function-vars f)
-;;                                    claim)
-;;               (rewrite sys
-;;                        claim
-;;                        (proof-sequence pf)))))
-;;       (else
-;;        (error "(vikalpa) define-proof: totality-claim is not found:"
-;;               (proof-name pf)
-;;               (proof-seed pf)))))
-;;     (else
-;;      (error "define-proof: fail"
-;;             (proof-name pf) (proof-seed pf)))))
-
-;; (define (system->scheme sys)
-;;   `(begin
-;;      ,@(map (lambda (f)
-;;               `(define (,(function-name f) ,@(function-vars f))
-;;                  ,(code-expr (function-code f))))
-;;             (reverse (filter (lambda (x)
-;;                                (and (function*? x)
-;;                                     (function-code x)))
-;;                              (get-definitions sys))))))
-
-;; (define/guard (check (sys system?))
-;;   (let loop ((sys sys)
-;;              (fails '()))
-;;     (let ((defs (get-definitions sys)))
-;;       (define* (next #:optional fail)
-;;         (loop (make-system (cdr defs)
-;;                            (system-proofs sys)
-;;                            (system-totality-claim-list 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) sys))
-;;           (next))
-;;          (else
-;;           (cond
-;;            ((find-proof (get-name (car defs)) sys)
-;;             => (lambda (pf)
-;;                  (let ((result (prove sys (car defs) pf)))
-;;                    (cond
-;;                     ((equal? result ''#t)
-;;                      (next))
-;;                     (else
-;;                      (next (list (get-name (car defs))
-;;                                  result)))))))
-;;            (else
-;;             (next (list (get-name (car defs)))))))))
-;;        (else
-;;         (next))))))
-
-;; (define/guard (show (sys system?) (name symbol?))
-;;   (cond
-;;    ((lookup name sys)
-;;     => (lambda (def)
-;;          (cond
-;;           ((function? def)
-;;            `(define-function ,(function-name def) ,(function-vars def)
-;;               ,(function-expression def)))
-;;           ((theorem? def)
-;;            `(define-theorem ,(theorem-name def) ,(theorem-vars def)
-;;               ,(theorem-expression def)))
-;;           ((axiom? def)
-;;            `(define-axiom ,(theorem-name def) ,(theorem-vars def)
-;;               ,(theorem-expression def)))
-;;           ((primitive-function? def)
-;;            `(define-primitive-function
-;;               ,(function-name def)
-;;               ,(function-vars def)))
-;;           (((cut is-a? <> <macro>) def)
-;;            `(define-syntax-rules ,(macro-name def)))
-;;           (else
-;;            `(error 'fatal-error ,name)))))
-;;    (else
-;;     `(error 'not-found ,name))))
-
-;; (define/guard (load-system (sys system?))
-;;   (primitive-eval (system->scheme sys)))
-
-;; (define/guard (system-primitives (sys system?))
-;;   (append reserved-symbols
-;;           (map function-name
-;;                (filter primitive-function?
-;;                        (get-definitions sys)))))
-
-;; (define/guard (system-functions (sys system?))
-;;   (map function-name
-;;        (filter function?
-;;                (get-definitions sys))))
-
-;; (define/guard (system-theorems (sys system?))
-;;   (map theorem-name
-;;        (filter theorem?
-;;                (get-definitions sys))))
-
-;; (define/guard (system-axioms (sys system?))
-;;   (map theorem-name
-;;        (filter axiom?
-;;                (get-definitions sys))))
-
-;; (define/guard (system-macros (sys system?))
-;;   (map macro-name
-;;        (filter (cut is-a? <> <macro>)
-;;                (get-definitions sys))))
-
-;; (define/guard (system-totality-claims (sys system?))
-;;   (system-totality-claim-list sys))
+(define/guard (system-apropos (sys system?) (str string?))
+  (filter (lambda (name)
+            (string-match (string-append ".*"
+                                         (regexp-quote str)
+                                         ".*")
+                          (symbol->string name)))
+          (map get-name (get-definitions sys))))
+
+(define (system-code sys)
+  `(begin
+     ,@(map (lambda (f)
+              `(define (,(get-name f) ,@(get-variables f))
+                 ,(code-expr (get-code f))))
+            (reverse (filter (lambda (x)
+                               (and (is-a? x <expandable-function>)
+                                    (get-code x)))
+                             (get-definitions sys))))))
+
+(define (check sys)
+  (let loop ((sys sys)
+             (fails '()))
+    (if (system-empty? sys)
+        fails
+        (let ((d (first-definition sys))
+              (sys-without-first (remove-first-definition sys)))
+          (define* (next #:optional fail)
+            (loop sys-without-first
+                  (if fail
+                      (cons fail fails)
+                      fails)))
+          (cond
+           ((is-a? d <proved>)
+            (let ((result
+                   (if (is-a? d <theorem>)
+                       (rewrite sys-without-first
+                                (get-claim d)
+                                (get-proof d))
+                       (rewrite sys
+                                (get-claim d)
+                                (get-proof d)))))
+              (cond
+               ((equal? result ''#t)
+                (next))
+               (else
+                (next (list (get-name d) result))))))
+           ((is-a? d <provable>)
+            (next (list (get-name d))))
+           (else (next)))))))
+
+(define (system? x)
+  (is-a? x <system>))
+
+(define/guard (describe (sys system?) (name symbol?))
+  (cond
+   ((lookup name sys)
+    => (lambda (def)
+         (cond
+          ((is-a? def <core-function>)
+           `(define-core-function ,(get-name def) ,(get-variables def)))
+          ((is-a? def <expandable-function>)
+           `(define-function ,(get-name def) ,(get-variables def)
+              ,(get-expression def)))
+          ((is-a? def <axiom>)
+           `(define-axiom ,(get-name def) ,(get-variables def)
+              ,(get-expression def)))
+          ((is-a? def <theorem*>)
+           `(define-theorem ,(get-name def) ,(get-variables def)
+              ,(get-expression def)))
+          (((cut is-a? <> <macro>) def)
+           `(define-syntax-rules ,(get-name def)))
+          (else
+           `(error 'fatal-error ,name)))))
+   (else
+    `(error 'not-found ,name))))
+
+(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)
@@ -1505,9 +1488,22 @@
     (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-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
@@ -1575,9 +1571,22 @@
   (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-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
@@ -1586,4 +1595,22 @@
   
   (define-theorem assoc-app (x y z)
     (equal? (app x (app y z))
-            (app (app x 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)
+    ())
+  )
+
-- 
cgit v1.2.3