From a1668838d8e620186ee1a463f1d779fdea788b7d Mon Sep 17 00:00:00 2001
From: Masaya Tojo <masaya@tojo.tokyo>
Date: Sat, 14 Nov 2020 11:31:10 +0900
Subject: wip15

---
 vikalpa.scm | 343 +++++++++++++++++++++++++++++++++++++++++++++---------------
 1 file changed, 261 insertions(+), 82 deletions(-)

diff --git a/vikalpa.scm b/vikalpa.scm
index 6dadcd2..2b68c41 100644
--- a/vikalpa.scm
+++ b/vikalpa.scm
@@ -22,12 +22,14 @@
   #:use-module (vikalpa primitive)
   #:use-module (ice-9 match)
   #:use-module (ice-9 format)
-  #:use-module ((srfi srfi-1) #:select (every any member))
+  #:use-module (ice-9 control)
+  #:use-module ((srfi srfi-1) #:select (every any member lset-union fold))
   #:use-module (srfi srfi-8)
+  #:use-module (srfi srfi-11)
   #:use-module (srfi srfi-26))
 
 (define (debug f . args)
-  (if #t
+  (if #f
       (apply format #t f args)
       #t))
 
@@ -46,20 +48,62 @@
          (or (integer? (expr-unquote expr))
              (boolean? (expr-unquote expr))
              (symbol? (expr-unquote expr))))
-        ((pair? expr)
+        ((form? expr)
          (and (expression? (car expr))
               (list? (cdr expr))
               (every expression? (cdr expr))))
         ((variable? expr) #t)
         (else #f)))
 
-(define (all-vars x)
-  (cond ((expr-quoted? x) '())
-        ((pair? x)
-         (append (all-vars (car x))
-                 (all-vars (cdr x))))
-        ((variable? x) (list x))
-        (else '())))
+(define (form? expr)
+  (and (pair? expr)
+       (not (eq? (car expr) 'quote))))
+
+(define (form-name expr)
+  (car expr))
+
+(define (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 (expression-functions expr)
+  (cond
+   ((form? expr)
+    (cons (form-name expr)
+          (apply lset-union
+                 eq?
+                 (map expression-functions (form-args expr)))))
+   (else '())))
+
+(define (expression-vars expr)
+  (cond
+   ((form? expr)
+    (apply lset-union eq?
+           (map expression-vars (form-args expr))))
+   ((variable? expr) (list expr))
+   (else '())))
 
 ;; (expr-quoted? x) -> boolean?
 (define (expr-quoted? expr)
@@ -129,62 +173,128 @@
               (environment (cdr x))))
         (else #f)))
 
-(define (apply-rule preconds rl expr env)
-  (call/cc (lambda (k) (apply-rule* preconds rl expr env k))))
+
+(define (match-expr f context acc preconds expr1 expr2 fail)
+  (cond
+   ((and (expr-quoted? expr1)
+         (expr-quoted? expr2)
+         (equal? expr1 expr2))
+    (f (cons '(quoted) context) acc preconds expr1 expr2 fail))
+   ((and (expr-if? expr1)
+         (expr-if? expr2))
+    (let*-values (((acc/test expr/test)
+                   (match-expr f '(if 1)
+                               acc
+                               preconds
+                               (expr-if-test expr1)
+                               (expr-if-test expr2)
+                               fail))
+                  ((expr/then acc/then)
+                   (match-expr f
+                               (cons '(if 2) context)
+                               acc/test
+                               (cons (expr-if-test expr2) preconds)
+                               (expr-if-then expr1)
+                               (expr-if-then expr2)
+                               fail))
+                  ((acc/else expr/else)
+                   (match-expr f
+                               (cons '(if 3) context)
+                               acc/then
+                               (cons (expr-not (expr-if-test expr2))
+                                     preconds)
+                               (expr-if-else expr1)
+                               (expr-if-else expr2)
+                               fail)))
+      (values acc/else (expr-if expr/test expr/then expr/else))))
+   ((and (form? expr1)
+         (form? expr2)
+         (eq? (form-name expr1)
+              (form-name expr2)))
+    (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-acc first-expr)
+                 (match-expr f
+                             (cons `(,(form-name expr1) ,i) context)
+                             acc
+                             preconds
+                             (car expr1-args)
+                             (car expr2-args)
+                             fail)
+               (receive (rest-acc rest-expr)
+                   (fold2 (cdr expr1-args)
+                          (cdr expr2-args)
+                          first-acc
+                          (+ i 1))
+                 (values (cons first-expr rest-expr)
+                         rest-acc))))
+            (else
+             (fail context acc)))))
+   (else
+    (fail context acc))))
 
 ;; (apply-rule preconds rule? expression?) -> (or (cons rhs environment) #f)
-(define (apply-rule* preconds rl expr env fail)
+(define (apply-rule preconds rl expr env)
+  (define (fail)
+    (shift k #f))
   (define (var? v)
     (and (member v (rule-vars rl))
          #t))
-  (define (add-env var expr env k)
+  (define (add-env var expr env)
     (cond
      ((assoc var env)
       => (match-lambda
            ((env-var . env-expr)
             (if (equal? env-expr expr)
                 env
-                (k #f)))))
+                (fail)))))
      (else
       (cons (cons var expr)
             env))))
-  (define (mat-map lhss exprs env k)
+  (define (mat-map lhss exprs env)
     (cond ((and (pair? lhss)
                 (pair? exprs))
            (mat-map (cdr lhss)
                     (cdr exprs)
                     (mat (car lhss)
                          (car exprs)
-                         env
-                         k)
-                    k))
+                         env)))
           ((and (null? lhss)
                 (null? exprs))
            env)
-          (else (k #f))))
-  (define (mat lhs expr env k)
+          (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)
-               (k #f)))
-          ((pair? lhs)
-           (if (and (pair? expr)
-                    (symbol? (car lhs))
-                    (eqv? (car lhs) (car expr)))
-               (mat-map (cdr lhs) (cdr expr) env k)
-               (k #f)))
-          ((var? lhs) (add-env lhs expr env k))
-          (else (k #f))))
-  (define (mat-preconds rlps 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)
+               (fail)))
+          ((var? lhs) (add-env lhs expr env))
+          (else (fail))))
+  (define (mat-preconds rlps k+env)
     (if (null? rlps)
-        env
+        k+env
         (mat-preconds (cdr rlps)
                       (any (lambda (p)
-                             (call/cc (lambda (k)
-                                        (mat (car rlps) p env
-                                             (lambda (x) (k #f))))))
+                             (shift k
+                                    (cond
+                                     ((reset (mat (car rlps) p (cdr k+env)))
+                                      => (lambda (env) (k (cons k env))))
+                                     (else (k #f)))))
                            preconds))))
   (define (substitute env expr)
     (cond ((expr-quoted? expr) expr)
@@ -193,20 +303,27 @@
                  (substitute env (cdr expr))))
           ((var? expr)
            (cond ((assoc expr env) => cdr)
-                 (else (fail #f))))
+                 (else (fail))))
           (else expr)))
   (debug "rule: ~a~%" rl)
   (debug "preconds: ~a~%" preconds)
   (debug "expr: ~a~%" expr)
-  (substitute (mat (rule-lhs rl)
-                   expr
-                   (mat-preconds (rule-preconds rl) env)
-                   fail)
-              (rule-rhs rl)))
-
-;; (book? x) -> boolean?
-;; book is alist
-(define (book? x)
+  (reset
+   (shift k
+          (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))))
+            (else #f)))))
+
+;; (system? x) -> boolean?
+;; system is alist
+(define (system? x)
   (cond ((null? x) #t)
         ((pair? x)
          (and (pair? (car x))
@@ -214,7 +331,7 @@
                   (primitive-function? (car x))
                   (macro? (car x))
                   (function? (car x)))
-              (book? (cdr x))))
+              (system? (cdr x))))
         (else #f)))
 
 (define (primitive-function? x)
@@ -276,23 +393,29 @@
 
 (define (mrule? x)
   (and (list? x)
-       (= 4 (length x))
+       (= 3 (length x))
        (eq? 'mrule (list-ref x 0))
-       (vars? (mrule-vars x))
        ((const #t) (mrule-lhs x))
        ((const #t) (mrule-rhs x))))
 
-(define (mrule vars lhs rhs)
-  (list 'mrule vars lhs rhs))
+(define (mrule lhs rhs)
+  (list 'mrule lhs rhs))
 
 (define (mrule-vars mrl)
-  (list-ref mrl 1))
+  (define (all-vars x)
+    (cond ((expr-quoted? x) '())
+          ((pair? x)
+           (append (all-vars (car x))
+                   (all-vars (cdr x))))
+          ((variable? x) (list x))
+          (else '())))
+  (all-vars (mrule-lhs mrl)))
 
 (define (mrule-lhs mrl)
-  (list-ref mrl 2))
+  (list-ref mrl 1))
 
 (define (mrule-rhs mrl)
-  (list-ref mrl 3))
+  (list-ref mrl 2))
 
 (define (macro? x)
   (and (list? x)
@@ -505,7 +628,7 @@
       (let ((i (car path)))
         (cond
          ((expr-if? expr)
-          (let ((precond (expr-if-cond expr)))
+          (let ((precond (expr-if-test expr)))
             (receive (extracted-expr extracted-preconds builder)
                 (extract (cdr path) (list-ref expr i) fail)
               (values extracted-expr
@@ -564,7 +687,7 @@
      (else
       (fail (format #f "no match-rule (~a)" cmd))))))
 
-;; (rewrite book? rewriter? expression? procedure?) -> expr
+;; (rewrite system? rewriter? expression? procedure?) -> expr
 (define (rewrite1 b expr fail r)
   (let* ((cmd (rewriter-command r))
          (cmd/name (command-name cmd)))
@@ -607,7 +730,7 @@
                 (fail "rewrite error")))))
         (else (fail "no cmd (~a)" cmd)))))))
 
-(define/guard (rewrite (b book?) (expr expression?) (seq sequence?))
+(define/guard (rewrite (b system?) (expr expression?) (seq sequence?))
   (let loop ((expr expr)
              (seq seq))
     (debug "~y~%" expr)
@@ -643,11 +766,14 @@
   (and (list? x)
        (= 4 (length x))
        (eq? 'if (list-ref x 0))
-       (expression? (list-ref x 1))
-       (expression? (list-ref x 2))
-       (expression? (list-ref x 3))))
+       (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-cond x)
+(define (expr-if-test x)
   (list-ref x 1))
 
 (define (expr-if-then x)
@@ -659,10 +785,10 @@
 (define (expression->rules vars preconds expr)
   (if (expr-if? expr)
       (append (expression->rules vars
-                                 (cons (expr-if-cond expr) preconds)
+                                 (cons (expr-if-test expr) preconds)
                                  (expr-if-then expr))
               (expression->rules vars
-                                 (cons (expr-not (expr-if-cond expr)) preconds)
+                                 (cons (expr-not (expr-if-test expr)) preconds)
                                  (expr-if-else expr)))
       (if (expr-equal? expr)
           (list (rule vars
@@ -680,57 +806,57 @@
                      '()
                      (proposition-expression def)))
 
-(define current-book (make-parameter '()))
+(define current-system (make-parameter '()))
 
-(define (add-book x)
-  (let ((b (current-book)))
-    (current-book
+(define (add-system x)
+  (let ((b (current-system)))
+    (current-system
      (cond ((assoc (proposition-name x) b)
             => (lambda (prop)
                  (if (equal? x prop)
                      b
-                     (error "add-book: error"))))
+                     (error "add-system: error"))))
            (else (cons x b))))))
 
 (define-syntax define-axiom
   (syntax-rules ()
     ((_ name (var ...) expr)
-     (add-book (axiom 'name '(var ...) 'expr)))))
+     (add-system (axiom 'name '(var ...) 'expr)))))
 
 (define-syntax define-theorem
   (syntax-rules ()
     ((_ name (var ...) expr)
-     (add-book (theorem 'name '(var ...) 'expr)))))
+     (add-system (theorem 'name '(var ...) 'expr)))))
 
 (define-syntax define-function
   (syntax-rules ()
     ((_ name (var ...) expr)
      (let ((f (function 'name '(var ...) 'expr)))
-       (add-book f)
+       (add-system f)
        f))))
 
 (define-syntax define-macro
   (syntax-rules ()
     ((_ name () ((lhs1 . lhs2) rhs) ...)
-     (add-book (macro 'name
-                 (list (mrule (all-vars 'lhs2) '(lhs1 . lhs2) 'rhs)
+     (add-system (macro 'name
+                 (list (mrule '(lhs1 . lhs2) 'rhs)
                        ...))))))
 
-(define-syntax define-book
+(define-syntax define-system
   (syntax-rules ()
-    ((_ name (books ...) expr ...)
+    ((_ name (systems ...) expr ...)
      (define* (name #:optional (parent '()))
-       (parameterize ([current-book ((compose books ... identity) parent)])
+       (parameterize ([current-system ((compose systems ... identity) parent)])
          expr
          ...
-         (unless (book? (current-book))
-           (error "define-book: error"))
-         (current-book))))))
+         (unless (system? (current-system))
+           (error "define-system: error"))
+         (current-system))))))
 
 (define (atom? x)
   (not (pair? x)))
 
-(define-book prelude ()
+(define-system prelude ()
   (define-axiom equal-same (x)
     (equal? (equal? x x) '#t))
 
@@ -742,6 +868,7 @@
 
   (define-axiom atom/cons (x y)
     (equal? (atom? (cons x y)) '#f))
+
   (define-axiom car/cons (x y)
     (equal? (car (cons x y)) x))
 
@@ -770,7 +897,7 @@
 
   (define-axiom if-false (x y)
     (equal? (if '#f x y) y))
-    
+
   (define-axiom if-same (x y)
     (equal? (if x y y) y))
 
@@ -793,21 +920,26 @@
   (define-macro list ()
     ((list) '())
     ((list x . y) (cons x (list . y))))
+
   (define-macro + ()
     ((+) '0)
     ((+ x) x)
     ((+ x . xs) (b+ x (+ . xs))))
+
   (define-macro - ()
     ((- x) (u- x))
     ((- x . xs) (+ x . (u- (+ . xs)))))
+
   (define-macro and ()
     ((and) '#t)
     ((and x) x)
     ((and x . xs) (if x (and . xs) #f)))
+
   (define-macro or ()
     ((or) '#f)
     ((or x) x)
     ((or x . xs) (if x x (or . xs))))
+
   (define-axiom if-not (x y z)
     (equal? (if (not x)
                 y
@@ -816,7 +948,37 @@
                 z
                 y))))
 
-(define-book app/book (prelude)
+(define (measure? x)
+  (and (pair? x)
+       (variable? (car x))
+       (list? (cdr x))
+       (<= 1 (length (cdr x)))))
+
+(define (measure-function-name m)
+  (car m))
+
+(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)
+  (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-system app/system (prelude)
   (define-function app (x y)
     (if (atom? x)
         y
@@ -827,7 +989,24 @@
             (app x (app y z))))
 
   #;
-  (rewrite (app/book)
+  (rewrite (app/system)
+           '(if (natural? (size (app a b)))
+                (if (atom? a)
+                    '#t
+                    (< (size (app (cdr a) b))
+                       (size (app a b))))
+                '#t)
+           '(((2 3 2 1) app)
+             ((2 3 2 1) if-nest)
+             ((2 3 1 1) cdr/cons (set x (car a)))
+             ((2 3) if-same (set x (atom? (cons (car a) (app (cdr a) b)))))
+             ((2 3 3) size/cdr)
+             ((2 3 1) atom/cons)
+             ((2 3) if-false)
+             ((2) if-same)
+             (() if-same)))
+  #;
+  (rewrite (app/system)
            '(if (atom? a)
                 (equal? (app (app a b) c)
                         (app a (app b c)))
-- 
cgit v1.2.3