Remove sys variables.

1 files changed, 72 insertions, 80 deletions

diff --git a/vikalpa.scm b/vikalpa.scm
index e220641..6a2af81 100644
--- a/vikalpa.scm
+++ b/vikalpa.scm
@@ -202,14 +202,14 @@
   (let* ((vars (get-variables d))
          (name (get-name d))
          (expr (get-expression d)))
-    (validate-expression (current-system) name vars expr)
+    (validate-expression 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)
+    (validate-expression name vars expr)
     (next-method)))
 
 (define-syntax-rule (define/guard (name (var p?) ...) b b* ...)
@@ -649,11 +649,10 @@
   (and (list? x)
        (every variable? x)))
 
-(define (theorem-rules x sys)
+(define (theorem-rules x)
   (expression->rules (get-variables x)
                      '()
-                     (get-expression x)
-                     sys))
+                     (get-expression x)))
 
 (define (result? x)
   (or (result/error? x)
@@ -678,7 +677,7 @@
 (define/guard (result/expr-expr (x result/expr?))
   (cadr x))
 
-(define (rewrite/eval expr sys)
+(define (rewrite/eval expr)
   (let eval ((result (result/expr expr)))
     (cond
      ((result/error? result) result)
@@ -692,7 +691,7 @@
                 (name (app-form-name expr)))
             (cond
              ((find error? args/result) => identity)
-             ((lookup name sys)
+             ((lookup name (current-system))
               => (lambda (f)
                    (let ((args (map result/expr-expr args/result))
                          (gs (get-guards f))
@@ -707,8 +706,7 @@
                              result
                              (expr-unquote (result/expr-expr result)))))
                      (if (every (lambda (g) (guard-ok? vars form g)) gs)
-                         (eval (rewrite1 sys
-                                         `(,name ,@args)
+                         (eval (rewrite1 `(,name ,@args)
                                          `(rewrite () ,name)))
                          (result/error 'guard-error `(,name ,@args) `(and ,@gs))))))
              (else (result/error 'function-not-found name)))))
@@ -765,9 +763,8 @@
   (cdr x))
 
 (define/guard (system-eval (sys system?) (expr (const #t)))
-  (rewrite/eval (parameterize ((current-system sys))
-                  (convert-to-expression expr))
-                sys))
+  (parameterize ((current-system sys))
+    (rewrite/eval (convert-to-expression expr))))
 
 (define (extract path expr fail)
   (if (null? path)
@@ -834,7 +831,7 @@
           (else
            (fail 'invalid-option (car ops)))))))
 
-(define (rewrite/theorem cmd-name cmd-ops b thm preconds expr sys)
+(define (rewrite/theorem cmd-name cmd-ops thm preconds expr)
   (call/cc
    (lambda (k)
      (define (fail . args)
@@ -843,11 +840,11 @@
          (parse-options/theorem cmd-ops fail)
        (cond
         ((any (cut apply-rule preconds <> expr env)
-              (theorem-rules thm sys)) => result/expr)
+              (theorem-rules thm)) => result/expr)
         (else
          (result/error 'apply-theorem cmd-name expr)))))))
 
-(define (rewrite/core-function sys f expr)
+(define (rewrite/core-function f expr)
   (if (and (app-form? expr)
            (eq? (get-name f) (app-form-name expr))
            (= (length (get-variables f)) (length (app-form-args expr)))
@@ -857,7 +854,7 @@
                           (map expr-unquote (app-form-args expr)))))
       (result/error 'apply-core-function (get-name f) expr)))
 
-(define (rewrite/function sys fname f expr)
+(define (rewrite/function fname f expr)
   (cond
    ((any (cut apply-rule '() <> expr '())
          (function->rules f))
@@ -865,7 +862,7 @@
    (else
     (result/error 'apply-function fname expr))))
 
-(define (rewrite1 sys expr r)
+(define (rewrite1 expr r)
   (call/cc
    (lambda (k)
      (define (fail . args)
@@ -881,7 +878,7 @@
             (extract path expr fail)
           (result/expr
            (builder
-            (result->expr (rewrite/eval extracted-expr sys))))))
+            (result->expr (rewrite/eval extracted-expr))))))
        #;
        (('induction path (fname vars ...))
         (receive (extracted-expr preconds builder)
@@ -897,20 +894,20 @@
            (builder
             (result->expr
              (cond
-              ((lookup cmd-name sys)
+              ((lookup cmd-name (current-system))
                => (lambda (x)
                     (cond
                      ((is-a? x <core-function>)
-                      (rewrite/core-function sys x extracted-expr))
+                      (rewrite/core-function x extracted-expr))
                      ((is-a? x <theorem*>)
-                      (rewrite/theorem cmd-name cmd-ops sys x preconds extracted-expr sys))
+                      (rewrite/theorem cmd-name cmd-ops x preconds extracted-expr))
                      ((is-a? x <expandable-function>)
-                      (rewrite/function sys cmd-name x extracted-expr))
+                      (rewrite/function cmd-name x extracted-expr))
                      (else
                       (result/error 'invalid-command cmd-name extracted-expr)))))
               (else (result/error 'command-not-found cmd-name extracted-expr))))))))))))
 
-(define (rewrite sys expr seq)
+(define (rewrite expr seq)
   (let loop ((result (result/expr expr))
              (seq seq))
     (cond
@@ -918,8 +915,7 @@
      ((result/expr? result)
       (if (null? seq)
           result
-          (loop (rewrite1 sys
-                          (result/expr-expr result)
+          (loop (rewrite1 (result/expr-expr result)
                           (car seq))
                 (cdr seq))))
      (else (result/error 'invalid-result result)))))
@@ -933,10 +929,10 @@
     (('not expr) expr)
     (expr (expr-not expr))))
 
-(define (expr-equal? x sys)
+(define (expr-equal? x)
   (and (list? x)
        (= 3 (length x))
-       (eq? (get-equal-symbol sys) (list-ref x 0))
+       (eq? (get-equal-symbol (current-system)) (list-ref x 0))
        (expression? (list-ref x 1))
        (expression? (list-ref x 2))))
 
@@ -946,25 +942,22 @@
 (define (expr-equal-rhs x)
   (list-ref x 2))
 
-(define (expression->rules vars preconds expr sys)
+(define (expression->rules vars preconds expr)
   (if (if-form? expr)
       (append (expression->rules vars
                                  (cons (prop-not
                                         (prop-not
                                          (if-form-test expr)))
                                        preconds)
-                                 (if-form-then expr)
-                                 sys)
+                                 (if-form-then expr))
               (expression->rules vars
                                  (cons (prop-not (if-form-test expr))
                                        preconds)
-                                 (if-form-else expr)
-                                 sys)
+                                 (if-form-else expr))
               (expression->rules vars
                                  preconds
-                                 (if-form-test expr)
-                                 sys))
-      (if (expr-equal? expr sys)
+                                 (if-form-test expr)))
+      (if (expr-equal? expr)
           (list (rule vars
                       preconds
                       (expr-equal-lhs expr)
@@ -1009,9 +1002,9 @@
           (validate t)
           t))))))
 
-(define (add-guard-theorem name sys)
+(define (add-guard-theorem name)
   (cond
-   ((lookup name sys)
+   ((lookup name (current-system))
     => (lambda (f)
          (if (is-a? f <expandable-function>)
              (add-definition (make <conjecture>
@@ -1019,10 +1012,9 @@
                                #:variables (get-variables f)
                                #:expression (fold smart-implies
                                                   (make-guard-claim
-                                                   (get-expression f)
-                                                   sys)
+                                                   (get-expression f))
                                                   (get-guards f)))
-                             sys)
+                             (current-system))
              (raise-exception
               (make-exception
                (make-exception-with-origin 'define-guard-theorem)
@@ -1038,7 +1030,7 @@
 (define-syntax define-guard-theorem
   (syntax-rules ()
     ((_ name)
-     (current-system (add-guard-theorem 'name (current-system))))))
+     (current-system (add-guard-theorem 'name)))))
 
 (define-syntax define-core-function/guard
   (syntax-rules (and)
@@ -1247,7 +1239,7 @@
    (else
     (smart-if x y ''#t))))
 
-(define (make-totality-claim* sys m-expr f)
+(define (make-totality-claim* m-expr f)
   (let* ((name (get-name f)))
     (define (convert app-form)
       (cond
@@ -1263,7 +1255,7 @@
                     (get-name f)
                     m-expr
                     app-form))))
-    (smart-if `(,(get-measure-predicate sys) ,m-expr)
+    (smart-if `(,(get-measure-predicate (current-system)) ,m-expr)
               (let loop ((expr (get-expression f)))
                 (cond
                  ((expr-quoted? expr) ''#t)
@@ -1284,7 +1276,7 @@
                                  (else (smart-and (loop (car args))
                                                   (f (cdr args))))))))
                     (if (eq? name (app-form-name expr))
-                        (smart-and `(,(get-measure-less-than sys)
+                        (smart-and `(,(get-measure-less-than (current-system))
                                      ,(convert expr)
                                      ,m-expr)
                                    rest)
@@ -1294,12 +1286,12 @@
                               m-expr))))
               ''#f)))
 
-(define (make-guard-claim expr sys)
+(define (make-guard-claim expr)
   (define (find-preconds expr)
     (cond
      ((app-form? expr)
       (let ((rest (append-map find-preconds (cdr expr))))
-        (append (cond ((lookup (car expr) sys) =>
+        (append (cond ((lookup (car expr) (current-system)) =>
                        (lambda (f)
                          (let ((preconds (get-guards f)))
                            (map (lambda (precond)
@@ -1389,14 +1381,14 @@
    (else (error "make-induction-claim: invalid"
                 f vars c))))
 
-(define (validate-sequence sys d seq)
+(define (validate-sequence d seq)
   (for-each (lambda (r)
               (match r
                 (('rewrite _ _ . command-ops)
                  (for-each (lambda (x)
                              (match x
                                (('= var expr)
-                                (validate-expression sys
+                                (validate-expression 
                                                      `(define-proof ,(get-name d))
                                                      (get-variables d)
                                                      expr))
@@ -1405,7 +1397,7 @@
                 (else #f)))
             seq))
 
-(define (add-proof/function sys f seed seq)
+(define (add-proof/function f seed seq)
   (define (update-claim claim)
     (update-definition (make <total-function>
                          #:name (get-name f)
@@ -1415,17 +1407,16 @@
                          #:code (get-code f)
                          #:claim claim
                          #:proof seq)
-                       sys))
-  (validate-sequence sys f seq)
+                       (current-system)))
+  (validate-sequence f seq)
   (if seed
       (begin
-        (validate-expression sys
-                             `(defien-proof ,(get-name f))
+        (validate-expression `(defien-proof ,(get-name f))
                              (get-variables f)
                              seed)
         (update-claim
          (fold smart-implies
-               (make-totality-claim* sys seed f)
+               (make-totality-claim* seed f)
                (get-guards f))))
       (raise-exception
        (make-exception
@@ -1433,20 +1424,20 @@
         (make-exception-with-message "need measure expression")
         (make-exception-with-irritants (get-expression f))))))
 
-(define (add-proof/theorem sys t seed seq)
+(define (add-proof/theorem t seed seq)
   (define (seed-error m)
     (raise-exception
      (make-exception
       (make-exception-with-origin 'define-proof)
       (make-exception-with-message (string-append "invalid seed: " m))
       (make-exception-with-irritants (list (get-name t) seed)))))
-  (validate-sequence sys t seq)
+  (validate-sequence t seq)
   (let ((claim
          (if seed
              (match seed
                ((fname vars ...)
                 (cond
-                 ((lookup fname sys)
+                 ((lookup fname (current-system))
                   => (cut make-induction-claim <> vars (get-expression t)))
                  (else (seed-error "function not found"))))
                (else (seed-error "format error")))
@@ -1457,9 +1448,9 @@
                          #:expression (get-expression t)
                          #:claim claim
                          #:proof seq)
-                       sys)))
+                       (current-system))))
 
-(define (add-proof sys name seed seq)
+(define (add-proof name seed seq)
   (cond
    ((not (sequence? seq))
     (raise-exception
@@ -1467,16 +1458,16 @@
       (make-exception-with-origin 'define-proof)
       (make-exception-with-message "not sequence")
       (make-exception-with-irritants seq))))
-   ((lookup name sys)
+   ((lookup name (current-system))
     => (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))
+                (add-proof/function def seed seq))
                ((is-a? def <conjecture>)
-                (add-proof/theorem sys def seed seq))
+                (add-proof/theorem def seed seq))
                (else
                 (raise-exception
                  (make-exception
@@ -1500,24 +1491,23 @@
     ((_ name
         seed
         seq)
-     (add-proof (current-system)
-                'name
+     (add-proof 'name
                 'seed
                 'seq))
     ((_ name seq)
      (define-proof name #f seq))))
 
-(define (validate-expression/error sys name vars expr)
+(define (validate-expression/error name vars expr)
   (with-exception-handler
       (lambda (e)
         (if (eq? 'validate-expression/error (exception-origin e))
             `(error ,name ,vars ,expr))
         (raise-exception e))
     (lambda ()
-      (validate-expression sys 'validate-expression/error vars expr)
+      (validate-expression 'validate-expression/error vars expr)
       #f)))
 
-(define (validate-expression sys name vars expr)
+(define (validate-expression name vars expr)
   (let* ((expr-fnames (expression-functions expr))
          (expr-vars (expression-vars expr))
          (expr-app-forms (expression-app-forms expr)))
@@ -1533,7 +1523,7 @@
               vars)
     (for-each (lambda (fname)
                 (unless (cond
-                         ((lookup fname sys) =>
+                         ((lookup fname (current-system)) =>
                           (lambda (f)
                             (for-each
                              (lambda (app-form)
@@ -1612,21 +1602,22 @@
                       #f)))
               (get-definitions sys)))
 
-(define (system-check/guard sys)
+(define (system-check/guard)
   (filter-map (lambda (f)
-                (if (lookup `(guard ,(get-name f)) sys)
+                (if (lookup `(guard ,(get-name f)) (current-system))
                     #f
-                    (if (equal? (make-guard-claim (get-expression f) sys)
+                    (if (equal? (make-guard-claim (get-expression f))
                                 ''#t)
                         #f
                         `((guard ,(get-name f))
                           (add (define-guard-theorem ,(get-name f)))))))
               (filter (cut is-a? <> <expandable-function>)
-                      (get-definitions sys))))
+                      (get-definitions (current-system)))))
 
 (define (system-check sys)
   (append
-   (system-check/guard sys)
+   (parameterize ((current-system sys))
+     (system-check/guard))
    (let loop ((sys sys)
               (fails '()))
      (if (system-empty? sys)
@@ -1642,12 +1633,12 @@
             ((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)))))
+                        (parameterize ((current-system sys-without-first))
+                          (rewrite (get-claim d)
+                                   (get-proof d)))
+                        (parameterize ((current-system sys))
+                          (rewrite (get-claim d)
+                                   (get-proof d))))))
                (cond
                 ((equal? result (result/expr ''#t))
                  (next))
@@ -1666,4 +1657,5 @@
    (else #f)))
 
 (define/guard (system-rewrite (sys system?) (expr (const #t)) (seq sequence?))
-  (rewrite sys (convert-to-expression expr) seq))
+  (parameterize ((current-system sys))
+    (rewrite (convert-to-expression expr) seq)))