wip18

1 files changed, 314 insertions, 214 deletions

diff --git a/vikalpa.scm b/vikalpa.scm
index 2b45012..bd55e69 100644
--- a/vikalpa.scm
+++ b/vikalpa.scm
@@ -23,7 +23,7 @@
   #:use-module (ice-9 match)
   #:use-module (ice-9 format)
   #:use-module (ice-9 control)
-  #:use-module ((srfi srfi-1) #:select (every any member lset-union fold))
+  #:use-module ((srfi srfi-1) #:select (every any member lset-union fold append-map))
   #:use-module (srfi srfi-8)
   #:use-module (srfi srfi-11)
   #:use-module (srfi srfi-26))
@@ -48,60 +48,58 @@
          (or (integer? (expr-unquote expr))
              (boolean? (expr-unquote expr))
              (symbol? (expr-unquote expr))))
-        ((form? expr)
-         (and (expression? (car expr))
+        ((if-form? expr)
+         (and (expression? (if-form-test expr))
+              (expression? (if-form-then expr))
+              (expression? (if-form-else expr))))
+        ((app-form? expr)
+         (and (symbol? (car expr))
               (list? (cdr expr))
               (every expression? (cdr expr))))
         ((variable? expr) #t)
         (else #f)))
 
-(define (form? expr)
+(define (app-form? expr)
   (and (pair? expr)
-       (not (eq? (car expr) 'quote))))
+       (not (eq? (car expr) 'quote))
+       (not (eq? (car expr) 'if))))
 
-(define (form-name expr)
+(define (app-form-name expr)
   (car expr))
 
-(define (form-args expr)
+(define (app-form-args expr)
   (cdr expr))
 
-;; (define (expression-fold2 f fail acc expr1 expr2)
-;;   (cond ((and (form? expr1)
-;;               (form? expr2)
-;;               (eq? (form-name expr1)
-;;                    (form-name expr2)))
-;;          (f (cons (form-name expr1)
-;;                   (fold (lambda (x acc)
-;;                           (expression-fold2 f fail <> <> acc))
-;;                        (form-args expr1)
-;;                        (form-args expr2)))))
-;;         ((or (form? expr1)
-;;              (form? expr2))
-;;          (fail expr1 expr2 acc))
-;;         (else (f expr1 expr2 acc))))
-
-;; (define (expression-fold f acc expr)
-;;   (cond ((form? expr)
-;;          (f (cons (form-name expr)
-;;                   (map (cut expression-fold f acc <>)
-;;                        (form-args expr)))
-;;             acc))
-;;         (else (f expr acc))))
+(define (if-form test then else)
+  (list 'if test then else))
+
+(define (if-form? x)
+  (and (pair? x)
+       (eq? (car x) 'if)))
+
+(define (if-form-test expr)
+  (list-ref expr 1))
+
+(define (if-form-then expr)
+  (list-ref expr 2))
+
+(define (if-form-else expr)
+  (list-ref expr 3))
 
 (define (expression-functions expr)
   (cond
-   ((form? expr)
-    (cons (form-name expr)
+   ((app-form? expr)
+    (cons (app-form-name expr)
           (apply lset-union
                  eq?
-                 (map expression-functions (form-args expr)))))
+                 (map expression-functions (app-form-args expr)))))
    (else '())))
 
 (define (expression-vars expr)
   (cond
-   ((form? expr)
+   ((app-form? expr)
     (apply lset-union eq?
-           (map expression-vars (form-args expr))))
+           (map expression-vars (app-form-args expr))))
    ((variable? expr) (list expr))
    (else '())))
 
@@ -173,103 +171,86 @@
               (environment (cdr x))))
         (else #f)))
 
-(define (traverse f expr acc context preconds fail)
-  (match-expr (lambda (ex1 ex2 a c ps fail)
-                (f ex1 a c ps fail))
-              expr
-              expr
-              acc
-              context
-              preconds
-              fail))
-
-(define (match-expr f g expr1 expr2 acc context preconds fail)
-  (cond
-   ((or (and (expr-quoted? expr1)
-             (expr-quoted? expr2)
-             (equal? expr1 expr2))
-        (variable? expr1))
-    (f expr1 expr2 acc context preconds fail))
-   ((and (expr-if? expr1)
-         (expr-if? expr2))
-    (let*-values (((expr/test acc/test)
-                   (match-expr f g
-                               (expr-if-test expr1)
-                               (expr-if-test expr2)
-                               acc
-                               (cons '(if 1) context)
-                               preconds
-                               fail))
-                  ((expr/then acc/then)
-                   (match-expr f g
-                               (expr-if-then expr1)
-                               (expr-if-then expr2)
-                               acc/test
-                               (cons '(if 2) context)
-                               (cons (expr-if-test expr2) preconds)
-                               fail))
-                  ((expr/else acc/else)
-                   (match-expr f g
-                               (expr-if-else expr1)
-                               (expr-if-else expr2)
-                               acc/then
-                               (cons '(if 3) context)
-                               (cons (expr-not (expr-if-test expr2))
-                                     preconds)
-                               fail)))
-      (g (expr-if expr/test expr/then expr/else)
-         acc/else
-         context
-         preconds
-         fail)))
-   ((and (form? expr1)
-         (form? expr2)
-         (eq? (form-name expr1)
-              (form-name expr2)))
-    (receive (args-expr args-acc)
-        (let fold2 ((expr1-args (form-args expr1))
-                    (expr2-args (form-args expr2))
-                    (acc acc)
-                    (i 1))
-          (cond ((and (null? expr1-args)
-                      (null? expr2-args))
-                 (values '() acc))
-                ((and (pair? expr1-args)
-                      (pair? expr2-args))
-                 (receive (first-expr first-acc)
-                     (match-expr f
-                                 (car expr1-args)
-                                 (car expr2-args)
-                                 acc
-                                 (cons `(,(form-name expr1) ,i) context)
-                                 preconds
-                                 fail)
-                   (receive (rest-expr rest-acc)
-                       (fold2 (cdr expr1-args)
-                              (cdr expr2-args)
-                              first-acc
-                              (+ i 1))
-                     (values (cons first-expr rest-expr)
-                             rest-acc))))
-                (else
-                 (fail expr1
-                       expr2
-                       acc
-                       context))))
-      (g expr1
-         (cons (form-name expr1) args-expr)
-         acc/else
-         context
-         preconds
-         fail)))
-   (else
-    (fail expr1
-          expr2
-          acc
-          context))))
+(define* (rebuild expr preconds
+                  #:key
+                  (quoted-proc (lambda (expr preconds) expr))
+                  (variable-proc (lambda (expr preconds) expr))
+                  (if-proc (lambda (expr preconds next) (next)))
+                  (app-form-proc (lambda (expr preconds next) (next))))
+  (let rec ((expr expr)
+            (preconds preconds))
+    (cond
+     ((expr-quoted? expr)
+      (quoted-proc expr preconds))
+     ((variable? expr)
+      (variable-proc expr preconds))
+     ((if-form? expr)
+      (letrec ((next
+                (lambda* (#:optional (expr expr))
+                  (let* ((expr/test (rec (if-form-test expr) preconds))
+                         (expr/then (rec (if-form-then expr) (cons (if-form-test expr) preconds)))
+                         (expr/else (rec (if-form-else expr) (cons (expr-not (if-form-test expr)) preconds))))
+                    (if-form expr/test expr/then expr/else)))))
+        (if-proc expr preconds next)))
+     ((app-form? expr)
+      (letrec ((next
+                (lambda* (#:optional (expr expr))
+                  (let f ((expr-args (app-form-args expr)))
+                    (cond ((null? expr-args) '())
+                          (else
+                           (cons (rec (car expr-args) preconds)
+                                 (f (cdr expr-args)))))))))
+        (app-form-proc expr preconds next)))
+     (else
+      (error "(vikalpa) rebuild: error")))))
+
+(define* (expr-fold expr acc preconds
+                    #:key
+                    (quoted-proc (lambda (expr acc preconds) acc))
+                    (variable-proc (lambda (expr acc preconds) acc))
+                    (if-proc (lambda (expr acc preconds next) (next)))
+                    (app-form-proc (lambda (expr acc preconds next) (next))))
+  (let rec ((expr expr)
+            (acc acc)
+            (preconds preconds))
+    (cond
+     ((expr-quoted? expr)
+      (quoted-proc expr acc preconds))
+     ((variable? expr)
+      (variable-proc expr acc preconds))
+     ((if-form? expr)
+      (letrec ((next
+                (lambda* (#:optional (expr expr) (acc acc) (preconds preconds))
+                  (let* ((acc/test
+                          (rec (if-form-test expr) acc preconds))
+                         (acc/then
+                          (rec (if-form-then expr) acc/test (cons (if-form-test expr) preconds))))
+                    (rec (if-form-else expr) acc/then (cons (expr-not (if-form-test expr)) preconds))))))
+        (if-proc expr acc preconds next)))
+     ((app-form? expr)
+      (letrec ((next
+                (lambda* (#:optional (expr expr) (acc acc) (preconds preconds))
+                  (let fold ((expr-args (app-form-args expr))
+                             (acc acc))
+                    (cond ((null? expr-args) acc)
+                          (else
+                           (fold (cdr expr-args)
+                                 (rec (car expr-args)
+                                      acc
+                                      preconds))))))))
+        (app-form-proc expr acc preconds next)))
+     (else
+      (error "(vikalpa) expr-fold: error")))))
 
-;; (apply-rule preconds rule? expression?) -> (or (cons rhs environment) #f)
-(define (apply-rule preconds rl expr env)
+(define (substitute env expr)
+  (cond ((expr-quoted? expr) expr)
+        ((pair? expr)
+         (cons (substitute env (car expr))
+               (substitute env (cdr expr))))
+        ((assoc expr env) => cdr)
+        (else expr)))
+
+(define (match-rule preconds rl expr env)
   (define (fail)
     (shift k #f))
   (define (var? v)
@@ -286,30 +267,35 @@
      (else
       (cons (cons var expr)
             env))))
-  (define (mat-map lhss exprs env)
-    (cond ((and (pair? lhss)
-                (pair? exprs))
-           (mat-map (cdr lhss)
-                    (cdr exprs)
-                    (mat (car lhss)
-                         (car exprs)
-                         env)))
-          ((and (null? lhss)
-                (null? exprs))
-           env)
+  (define (mat-fold lhss exprs env)
+    (cond ((and (pair? lhss) (pair? exprs))
+           (mat-fold (cdr lhss)
+                     (cdr exprs)
+                     (mat (car lhss)
+                          (car exprs)
+                          env)))
+          ((and (null? lhss) (null? exprs)) env)
           (else (fail))))
   (define (mat lhs expr env)
     (debug "lhs ~a, expr ~a, env ~a~%" lhs expr env)
     (cond ((expr-quoted? lhs)
            (if (expr-quoted? expr)
-               (and (equal? lhs expr)
-                    env)
+               (and (equal? lhs expr) env)
                (fail)))
-          ((form? lhs)
-           (if (and (form? expr)
-                    (symbol? (form-name lhs))
-                    (eqv? (form-name lhs) (form-name expr)))
-               (mat-map (form-args lhs) (form-args expr) env)
+          ((and (if-form? lhs)
+                (if-form? expr))
+           (mat-fold (list (if-form-test lhs)
+                           (if-form-then lhs)
+                           (if-form-else lhs))
+                     (list (if-form-test expr)
+                           (if-form-then expr)
+                           (if-form-else expr))
+                     env))
+          ((app-form? lhs)
+           (if (and (app-form? expr)
+                    (symbol? (app-form-name lhs))
+                    (eqv? (app-form-name lhs) (app-form-name expr)))
+               (mat-fold (app-form-args lhs) (app-form-args expr) env)
                (fail)))
           ((var? lhs) (add-env lhs expr env))
           (else (fail))))
@@ -324,15 +310,15 @@
                                       => (lambda (env) (k (cons k env))))
                                      (else (k #f)))))
                            preconds))))
-  (define (substitute env expr)
-    (cond ((expr-quoted? expr) expr)
+  (define (valid? env expr)
+    (cond ((expr-quoted? expr) #t)
           ((pair? expr)
-           (cons (substitute env (car expr))
-                 (substitute env (cdr expr))))
+           (and (valid? env (car expr))
+                (valid? env (cdr expr))))
           ((var? expr)
-           (cond ((assoc expr env) => cdr)
-                 (else (fail))))
-          (else expr)))
+           (cond ((assoc expr env) => (const #t))
+                 (else #f)))
+          (else #t)))
   (debug "rule: ~a~%" rl)
   (debug "preconds: ~a~%" preconds)
   (debug "expr: ~a~%" expr)
@@ -341,14 +327,21 @@
           (match (mat-preconds (rule-preconds rl) (cons k env))
             ((k . env)
              (cond
-              ((reset (mat (rule-lhs rl)
-                           expr
-                           env))
-               => (cut substitute <> (rule-rhs rl)))
-              (else
-               (k #f))))
+              ((reset (mat (rule-lhs rl) expr env))
+               => (lambda (env)
+                    (if (valid? env (rule-rhs rl))
+                        env
+                        #f)))
+              (else (k #f))))
             (else #f)))))
 
+;; (apply-rule preconds rule? expression?) -> (or (cons rhs environment) #f)
+(define (apply-rule preconds rl expr env)
+  (cond
+   ((match-rule preconds rl expr env)
+    => (cut substitute <> (rule-rhs rl)))
+   (else #f)))
+
 ;; (system? x) -> boolean?
 ;; system is alist
 (define (system? x)
@@ -500,17 +493,17 @@
                       env))))
              ((eqv? lhs expr) env)
              (else (k #f))))
-     (define (substitute env expr)
+     (define (mrule-substitute env expr)
        (cond ((expr-quoted? expr) expr)
              ((pair? expr)
-              (cons (substitute env (car expr))
-                    (substitute env (cdr expr))))
+              (cons (mrule-substitute env (car expr))
+                    (mrule-substitute env (cdr expr))))
              ((and (variable? expr) (assoc expr env)) => cdr)
              (else expr)))
-     (substitute (mat (mrule-lhs rl)
-                      expr
-                      '())
-                 (mrule-rhs rl)))))
+     (mrule-substitute (mat (mrule-lhs rl)
+                            expr
+                            '())
+                       (mrule-rhs rl)))))
 
 (define (apply-macro m expr)
   (cond ((and (pair? expr)
@@ -655,8 +648,8 @@
       (values expr '() identity)
       (let ((i (car path)))
         (cond
-         ((expr-if? expr)
-          (let ((precond (expr-if-test expr)))
+         ((if-form? expr)
+          (let ((precond (if-form-test expr)))
             (receive (extracted-expr extracted-preconds builder)
                 (extract (cdr path) (list-ref expr i) fail)
               (values extracted-expr
@@ -684,14 +677,21 @@
 (define (function->rules x)
   (list (rule (function-vars x)
               '()
-              (cons (function-name x)
-                    (function-vars x))
+              (function-app-form x)
               (function-expression x))
         (rule (function-vars x)
               '()
               (function-expression x)
-              (cons (function-name x)
-                    (function-vars x)))))
+              (function-app-form x))))
+
+(define (apply-function f args)
+  (apply-rule '()
+              (rule (function-vars f)
+                    '()
+                    (function-app-form f)
+                    (function-expression f))
+              (cons (function-name f) args)
+              '()))
 
 (define (parse-options/prop ops)
   (if (null? ops)
@@ -715,6 +715,7 @@
      (else
       (fail (format #f "no match-rule (~a)" cmd))))))
 
+
 ;; (rewrite system? rewriter? expression? procedure?) -> expr
 (define (rewrite1 b expr fail r)
   (let* ((cmd (rewriter-command r))
@@ -790,34 +791,14 @@
 (define (expr-equal-rhs x)
   (list-ref x 2))
 
-(define (expr-if? x)
-  (and (list? x)
-       (= 4 (length x))
-       (eq? 'if (list-ref x 0))
-       (expression? (expr-if-test x))
-       (expression? (expr-if-then x))
-       (expression? (expr-if-else x))))
-
-(define (expr-if x y z)
-  (list 'if x y z))
-
-(define (expr-if-test x)
-  (list-ref x 1))
-
-(define (expr-if-then x)
-  (list-ref x 2))
-
-(define (expr-if-else x)
-  (list-ref x 3))
-
 (define (expression->rules vars preconds expr)
-  (if (expr-if? expr)
+  (if (if-form? expr)
       (append (expression->rules vars
-                                 (cons (expr-if-test expr) preconds)
-                                 (expr-if-then expr))
+                                 (cons (if-form-test expr) preconds)
+                                 (if-form-then expr))
               (expression->rules vars
-                                 (cons (expr-not (expr-if-test expr)) preconds)
-                                 (expr-if-else expr)))
+                                 (cons (expr-not (if-form-test expr)) preconds)
+                                 (if-form-else expr)))
       (if (expr-equal? expr)
           (list (rule vars
                       preconds
@@ -988,23 +969,125 @@
 (define (measure-function-vars m)
   (cdr m))
 
-(define (subst lhs rhs expr)
-  (apply-rule '()
-              (rule (expression-vars lhs) '() lhs rhs)
-              expr
-              '()))
-
-(define (function-form f)
+(define (function-app-form f)
   (cons (function-name f) (function-vars f)))
 
-;; (define (make-totality-claim m f)
-;;   (let ((vs (function-vars f))
-;;         (fexpr (function-expression f)))
-;;     (expression-fold (lambda (expr)
-;;                        (cond
-;;                         ((form? expr)
-;;                          )))
-;;                      (function-expression f))))
+(define (expand-all b expr)
+  (expand* (filter macro? b) expr))
+
+(define (single? x)
+  (and (pair? x)
+       (null? (cdr x))))
+
+(define (if/if x y z)
+  (cond
+   ((equal? y z) y)
+   ((equal? x ''#t) y)
+   ((equal? x ''#f) z)
+   (else `(if ,x ,y ,z))))
+
+(define (and/if . args)
+  (cond
+   ((null? args) ''#t)
+   ((equal? ''#t (car args)) (apply and/if (cdr args)))
+   (else
+    (let ((rest (apply and/if (cdr args))))
+      (if (equal? ''#t rest)
+          (car args)
+          (if/if (car args)
+                 rest
+                 ''#f))))))
+
+(define (implies/if x y)
+  (cond
+   ((equal? ''#f x) ''#t)
+   ((equal? ''#t y) ''#t)
+   (else
+    (if/if x y ''#t))))
+
+(define (make-totality-claim/natural m vars f)
+  (let ((name (function-name f))
+        (m-expr (cons (function-name m) vars)))
+    (define (convert app-form)
+      (cond
+       ((apply-rule '()
+                    (rule vars
+                          '()
+                          (cons (function-name f) vars)
+                          m-expr)
+                    app-form
+                    '())
+        => identity)
+       (else
+        (error "make-totality-claim/natural: fail<p>"))))
+    (if/if `(natural? ,(cons (function-name m) vars))
+           (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 `(< ,(convert expr) ,m-expr)
+                             rest)
+                     rest)))
+              (else (error "(vikalpa) make-totality-claim: error"))))
+           ''#t)))
+
+(define (make-induction-claim f vars t)
+  (define (find-app-forms expr)
+    (cond
+     ((app-form? expr)
+      (let ((rest (append-map find-app-forms (cdr expr))))
+        (if (eq? (function-name f) (app-form-name expr))
+            (cons expr rest)
+            rest)))
+     ((if-form? expr)
+      (error "make-induction-claim: FAILED m(- -)m"))
+     (else '())))
+  (let ((c (proposition-expression t)))
+    (define (prop app-form)
+      (cond
+       ((apply-rule '()
+                    (rule (function-vars f)
+                          '()
+                          (cons (function-name f) vars)
+                          c)
+                    app-form
+                    '())
+        => identity)
+       (else
+        (error "make-induction-claim: fail"))))
+    (cond
+     ((apply-function f vars)
+      => (lambda (expr)
+           (let build ((expr expr))
+             (cond
+              ((if-form? expr)
+               (let ((app-forms (find-app-forms (if-form-test expr))))
+                 (implies/if (if (null? app-forms)
+                                 ''#t
+                                 (fold implies/if c (map prop app-forms)))
+                         (if/if (if-form-test expr)
+                                (build (if-form-then expr))
+                                (build (if-form-else expr))))))
+              (else
+               (let ((app-forms (find-app-forms expr)))
+                 (fold implies/if c (map prop app-forms))))))))
+     (else (error "make-induction-claim: fail<3>")))))
 
 (define-system app/system (prelude)
   (define-function app (x y)
@@ -1063,6 +1146,23 @@
              (() if-same)))
   )
 
+(define-system test/system (prelude)
+  (define-function id (x)
+    x)
+
+  (define-function even? (n)
+    (if (zero? n)
+        '#t
+        (if (= n '1)
+            '#f
+            (if (even? (- n '2))
+                '#t
+                '#f))))
+    
+  (define-theorem even-n+4 (n)
+    (equal? (even? n) (even? (+ n '4))))
+  )
+
 (define (size x)
   (if (pair? x)
       (+ 1