wip26

1 files changed, 142 insertions, 88 deletions

diff --git a/vikalpa.scm b/vikalpa.scm
index 42f046a..5151204 100644
--- a/vikalpa.scm
+++ b/vikalpa.scm
@@ -17,11 +17,19 @@
 ;;; along with Vikalpa.  If not, see <http://www.gnu.org/licenses/>.
 
 (define-module (vikalpa)
-  #:export (rewrite)
+  #:export (check
+            system->scheme
+            define-system
+            define-axiom
+            define-theorem
+            define-primitive-function
+            define-function
+            define-macro)
   #: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 append-map))
+  #: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))
@@ -302,7 +310,9 @@
     (debug "lhs ~a, expr ~a, env ~a~%" lhs expr env)
     (cond ((expr-quoted? lhs)
            (if (expr-quoted? expr)
-               (and (equal? lhs expr) env)
+               (if (equal? lhs expr)
+                   env
+                   (fail))
                (fail)))
           ((and (if-form? lhs)
                 (if-form? expr))
@@ -427,15 +437,19 @@
 
 (define (function? x)
   (and (list? x)
-       (= 4 (length x))
+       (= 5 (length x))
        (variable? (function-name x))
        (eq? 'function (list-ref x 1))
        (vars? (function-vars x))
-       (expression? (function-expression x))))
+       (expression? (function-expression x))
+       ((const #t) (function-code x))))
 
 ;; (function variable? vars? expression?) -> function?
-(define/guard (function (name variable?) (vars vars?) (expr expression?))
-  (list name 'function vars expr))
+(define/guard (function (name variable?)
+                        (vars vars?)
+                        (expr expression?)
+                        (code any?))
+  (list name 'function vars expr code))
 
 (define (function-name f)
   (list-ref f 0))
@@ -446,9 +460,18 @@
 (define (function-expression f)
   (list-ref f 3))
 
+(define (function-code f)
+  (list-ref f 4))
+
 (define (definition-name d)
   (list-ref d 0))
 
+(define (definition-vars d)
+  (list-ref d 2))
+
+(define (definition-expression d)
+  (list-ref d 3))
+
 (define (mrule? x)
   (and (list? x)
        (= 3 (length x))
@@ -477,12 +500,13 @@
 
 (define (macro? x)
   (and (list? x)
-       (= 3 (length x))
+       (= 4 (length x))
        (eq? 'macro (list-ref x 1))
        (variable? (macro-name x))
        (let ((mrls (macro-mrules x)))
          (and (list? mrls)
-              (every mrule? mrls)))))
+              (every mrule? mrls)))
+       ((list-of symbol?) (macro-literals x))))
 
 (define (macro-name m)
   (list-ref m 0))
@@ -490,10 +514,15 @@
 (define (macro-mrules m)
   (list-ref m 2))
 
-(define (macro name rules)
-  (list name 'macro rules))
+(define (macro-literals m)
+  (list-ref m 3))
 
-(define (apply-mrule rl expr)
+(define (macro name rules ls)
+  (list name 'macro rules ls))
+
+(define (apply-mrule rl ls expr)
+  (define (literal? x)
+    (member x ls))
   (define (var? v)
     (and (member v (mrule-vars rl))
          #t))
@@ -511,12 +540,16 @@
      (define (mat lhs expr env)
        (cond ((expr-quoted? lhs)
               (if (expr-quoted? expr)
-                  (and (equal? lhs expr)
-                       env)
+                  (if (equal? lhs expr)
+                      env
+                      (k #f))
                   (k #f)))
-             ((and (pair? lhs)
-                   (pair? expr))
+             ((and (pair? lhs) (pair? expr))
               (mat-map lhs expr env))
+             ((literal? lhs)
+              (if (eq? lhs expr)
+                  env
+                  (k #f)))
              ((var? lhs)
               (cond
                ((assoc lhs env)
@@ -535,6 +568,7 @@
              ((pair? expr)
               (cons (mrule-substitute env (car expr))
                     (mrule-substitute env (cdr expr))))
+             ((literal? expr) expr)
              ((and (variable? expr) (assoc expr env)) => cdr)
              (else expr)))
      (mrule-substitute (mat (mrule-lhs rl)
@@ -546,8 +580,9 @@
   (cond ((and (pair? expr)
               (eq? (macro-name m) (car expr)))
          (let loop ((rs (macro-mrules m)))
-           (cond ((null? rs) expr)
-                 ((apply-mrule (car rs) expr) => identity)
+           (cond ((null? rs)
+                  (error "macro fail" m expr))
+                 ((apply-mrule (car rs) (macro-literals m) expr) => identity)
                  (else (loop (cdr rs))))))
         (else #f)))
 
@@ -575,20 +610,55 @@
 (define (quote-all x)
   (cond
    ((expr-quoted? x) x)
-   ((if-form? x)
-    (if-form (quote-all (if-form-test x))
-             (quote-all (if-form-then x))
-             (quote-all (if-form-else x))))
-   ((app-form? x)
-    (cons (app-form-name x)
-          (map quote-all (app-form-args x))))
-   ((variable? x) x)
+   ((pair? x)
+    (cons (expand-let (car x))
+          (expand-let (cdr x))))
+   ((symbol? x) x)
    (else `',x)))
 
+(define (let? x)
+  (and (list? x)
+       (= 3 (length x))
+       (eq? 'let (list-ref x 0))
+       ((list-of (lambda (x)
+                   (and (list? x)
+                        (= 2 (length x))
+                        (symbol? (car x))))) 
+        (list-ref x 1))))
+
+(define (expand-let x)
+  (define (let-substitute env expr)
+    (cond ((expr-quoted? expr) expr)
+          ((let? expr)
+           (let-substitute
+            (append (map (lambda (binding)
+                           (cons (car binding)
+                                 (let-substitute env
+                                                 (cadr binding))))
+                         (list-ref expr 1))
+                    env)
+            (list-ref expr 2)))
+          ((pair? expr)
+           (cons (let-substitute env (car expr))
+                 (let-substitute env (cdr expr))))
+          ((assoc expr env) => cdr)
+          (else expr)))
+  (cond
+   ((expr-quoted? x) x)
+   ((let? x)
+    (expand-let
+     (let-substitute (map (lambda (binding) (cons (car binding)
+                                                  (cadr binding)))
+                          (list-ref x 1))
+                     (list-ref x 2))))
+   ((pair? x)
+    (cons (expand-let (car x))
+          (expand-let (cdr x))))
+   (else x)))
+
 (define (convert-to-expression x)
-  (quote-all
-   (expand* (filter macro? (system-definitions (current-system)))
-            x)))
+  (expand* (filter macro? (system-definitions (current-system)))
+           (quote-all (expand-let x))))
 
 ;; (axiom variable? vars? expression?) -> axiom?
 ;; axiom? is theorem*
@@ -775,7 +845,6 @@
   (let* ((cmd (rewriter-command r))
          (cmd/name (command-name cmd)))
     (debug "~%~%cmd: ~a~%" cmd)
-    #;(format #t "~%~%cmd: ~a~%" cmd)
     (receive (extracted-expr preconds builder)
         (extract (rewriter-path r) expr fail)
       (builder
@@ -787,18 +856,13 @@
                ((theorem*? x)
                 (rewrite/theorem cmd sys x preconds extracted-expr fail))
                ((function? x)
-                (debug "FUNCTION: ~y" x)
                 (cond
                  ((any (cut apply-rule '() <> extracted-expr '())
                        (function->rules x)) => identity)
                  (else
                   (fail (format #f "no match-function (~a)" cmd)))))
-               ((primitive-function? x)
-                (fail "primitive-function fail"))
-               ((macro? x)
-                (fail "macro fail"))
                (else
-                (fail "rewrite error")))))
+                (fail "rewrite error" cmd)))))
         (else (fail "no cmd (~a)" cmd)))))))
 
 (define/guard (rewrite (sys system?) (expr expression?) (seq sequence?))
@@ -889,8 +953,8 @@
     ((_ name (var ...) expr)
      (let ((t (axiom 'name '(var ...)
                      (convert-to-expression 'expr))))
-       (validate-theorem t)
        (add-definition t)
+       (validate-definition t)
        t))))
 
 (define-syntax define-theorem
@@ -898,17 +962,18 @@
     ((_ name (var ...) expr)
      (let ((t (theorem 'name '(var ...)
                        (convert-to-expression 'expr))))
-       (validate-theorem t)
        (add-definition t)
+       (validate-definition t)
        t))))
 
 (define-syntax define-function
   (syntax-rules ()
     ((_ name (var ...) expr)
      (let ((f (function 'name '(var ...)
-                        (convert-to-expression 'expr))))
-       (validate-function f)
+                        (convert-to-expression 'expr)
+                        'expr)))
        (add-definition f)
+       (validate-definition f)
        f))))
 
 (define-syntax define-primitive-function
@@ -920,10 +985,11 @@
 
 (define-syntax define-macro
   (syntax-rules ()
-    ((_ name () ((lhs1 . lhs2) rhs) ...)
+    ((_ name (l ...) ((lhs1 . lhs2) rhs) ...)
      (let ((m (macro 'name
                 (list (mrule '(lhs1 . lhs2) 'rhs)
-                      ...))))
+                      ...)
+                '(l ...))))
        (add-definition m)
        m))))
 
@@ -942,9 +1008,9 @@
 (define-syntax system
   (syntax-rules ()
     ((_ (systems ...) expr ...)
-     (lambda* (#:optional (parent (make-system '() '())))
+     (let ()
        (parameterize ([current-system
-                       ((compose systems ... identity) parent)])
+                       ((compose systems ... identity) (make-system '() '()))])
          expr
          ...
          (unless (system? (current-system))
@@ -1030,16 +1096,10 @@
     ((or x) x)
     ((or x . xs) (if x x (or . xs))))
 
-  #;
-  (define-macro + ()
-    ((+) '0)
-    ((+ x) x)
-    ((+ x . xs) (b+ x (+ . xs))))
-  #;
-  (define-macro - ()
-    ((- x) (u- x))
-    ((- x . xs) (+ x . (u- (+ . xs)))))
-)
+  (define-macro cond (else)
+    ((cond (else e)) e)
+    ((cond (test then) . rest)
+     (if test then (cond . rest)))))
 
 (define (measure? x)
   (and (pair? x)
@@ -1223,38 +1283,29 @@
   (or (function? x)
       (primitive-function? x)))
 
-(define (validate-function f)
-  (let ((fexpr (function-expression f))
-        (fvars (function-vars f))
-        (fname (function-name f)))
+(define (validate-definition d)
+  (let* ((expr (definition-expression d))
+         (vars (definition-vars d))
+         (name (definition-name d))
+         (expr-fnames (expression-functions expr))
+         (expr-vars (expression-vars expr)))
     (for-each (lambda (x)
                 (unless (cond
                          ((lookup x (current-system)) => function*?)
-                         (else (eq? fname x)))
-                  (error (format #f "(vikalpa) ~a: undefined function" fname)
+                         (else #f))
+                  (error (format #f "(vikalpa) ~a: undefined function" name)
                          x)))
-              (expression-functions fexpr))
+              expr-fnames)
     (for-each (lambda (x)
-                (unless (member x fvars)
-                  (error (format #f "(vikalpa) ~a: undefined variable" fname)
+                (unless (member x vars)
+                  (error (format #f "(vikalpa) ~a: undefined variable" name)
+                         x))
+                (when (member x (if (function? d)
+                                    (cons name expr-fnames)
+                                    expr-fnames))
+                  (error (format #f "(vikalpa) ~a: invalid variable name" name)
                          x)))
-              (expression-vars fexpr))))
-
-(define (validate-theorem t)
-  (let ((texpr (function-expression t))
-        (tvars (function-vars t))
-        (tname (function-name t)))
-    (for-each (lambda (x)
-                (unless (cond ((lookup x (current-system)) => function*?)
-                              (else #f))
-                  (error (format #f "~a: undefined function" tname)
-                         x)))
-              (expression-functions texpr))
-    (for-each (lambda (x)
-                (unless (member x tvars)
-                  (error (format #f "~a: undefined variable" tname)
-                         x)))
-              (expression-vars texpr))))
+              expr-vars)))
 
 (define (trivial-total? f)
   (not (member (function-name f)
@@ -1294,11 +1345,19 @@
     (else
      (error "prove/function: fail"))))
 
+(define (system->scheme sys)
+  `(begin
+     ,@(map (lambda (f)
+              `(define (,(function-name f) ,@(function-vars f))
+                 ,(function-code f)))
+            (reverse (filter function? (system-definitions sys))))))
+
 (define-system app/system (prelude)
   (define-function app (x y)
-    (if (atom? x)
-        y
-        (cons (car x) (app (cdr x) y))))
+    (cond
+     ((atom? x) y)
+     (else
+      (cons (car x) (app (cdr x) y)))))
 
   (define-theorem associate-app (x y z)
     (equal? (app (app x y) z)
@@ -1338,11 +1397,6 @@
          (size (cdr x)))
       0))
 
-(define (app x y)
-  (if (atom? x)
-      y
-      (cons (car x) (app (cdr x) y))))
-
 (define (check sys)
   (let loop ((sys sys)
              (fails '()))