diff options
| -rw-r--r-- | vikalpa.scm | 52 |
1 files changed, 35 insertions, 17 deletions
diff --git a/vikalpa.scm b/vikalpa.scm index 771d484..3bc3374 100644 --- a/vikalpa.scm +++ b/vikalpa.scm @@ -26,6 +26,7 @@ set-measure-predicate set-measure-less-than core-system + core-system/equal define-system define-proof define-core-function @@ -58,6 +59,8 @@ #:getter get-definitions #:init-keyword #:definitions #:init-value '()) + (equal-symbol #:getter get-equal-symbol + #:init-value 'equal?) (measure-predicate #:getter get-measure-predicate #:init-value #f) (measure-less-than #:getter get-measure-less-than @@ -128,6 +131,11 @@ (equal? name (get-name x))) (get-definitions s))) +(define-method (update-equal-symbol (s <symbol>) (sys <system>)) + (let ((new (shallow-clone sys))) + (slot-set! new 'equal-symbol s) + new)) + (define-method (update-measure-predicate (s <symbol>) (sys <system>)) (let ((new (shallow-clone sys))) (slot-set! new 'measure-predicate s) @@ -640,10 +648,11 @@ (and (list? x) (every variable? x))) -(define (theorem-rules x) +(define (theorem-rules x sys) (expression->rules (get-variables x) '() - (get-expression x))) + (get-expression x) + sys)) (define (result? x) (or (result/error? x) @@ -824,7 +833,7 @@ (else (fail 'invalid-option (car ops))))))) -(define (rewrite/theorem cmd-name cmd-ops b thm preconds expr) +(define (rewrite/theorem cmd-name cmd-ops b thm preconds expr sys) (call/cc (lambda (k) (define (fail . args) @@ -833,7 +842,7 @@ (parse-options/theorem cmd-ops fail) (cond ((any (cut apply-rule preconds <> expr env) - (theorem-rules thm)) => result/expr) + (theorem-rules thm sys)) => result/expr) (else (result/error 'apply-theorem cmd-name expr))))))) @@ -893,7 +902,7 @@ ((is-a? x <core-function>) (rewrite/core-function sys x extracted-expr)) ((is-a? x <theorem*>) - (rewrite/theorem cmd-name cmd-ops sys x preconds extracted-expr)) + (rewrite/theorem cmd-name cmd-ops sys x preconds extracted-expr sys)) ((is-a? x <expandable-function>) (rewrite/function sys cmd-name x extracted-expr)) (else @@ -923,10 +932,10 @@ (('not expr) expr) (expr (expr-not expr)))) -(define (expr-equal? x) +(define (expr-equal? x sys) (and (list? x) (= 3 (length x)) - (eq? 'equal? (list-ref x 0)) + (eq? (get-equal-symbol sys) (list-ref x 0)) (expression? (list-ref x 1)) (expression? (list-ref x 2)))) @@ -936,22 +945,25 @@ (define (expr-equal-rhs x) (list-ref x 2)) -(define (expression->rules vars preconds expr) +(define (expression->rules vars preconds expr sys) (if (if-form? expr) (append (expression->rules vars (cons (prop-not (prop-not (if-form-test expr))) preconds) - (if-form-then expr)) + (if-form-then expr) + sys) (expression->rules vars (cons (prop-not (if-form-test expr)) preconds) - (if-form-else expr)) + (if-form-else expr) + sys) (expression->rules vars preconds - (if-form-test expr))) - (if (expr-equal? expr) + (if-form-test expr) + sys)) + (if (expr-equal? expr sys) (list (rule vars preconds (expr-equal-lhs expr) @@ -962,11 +974,6 @@ (expr-equal-lhs expr))) '()))) -(define (theorem->rules def) - (expression->rules (get-variables def) - '() - (get-expression def))) - (define current-system (make-parameter (make <system>))) (define reserved-symbols '(quote let if error)) (define (reserved? x) @@ -1145,6 +1152,17 @@ (define-core-function equal? (x y) equal?) (current-system))) +(define (core-system/equal) + (parameterize ((current-system (make <system>))) + (current-system (update-equal-symbol 'equal (current-system))) + (define-syntax-rules and () + ((and) '#t) + ((and x) x) + ((and x . xs) (if x (and . xs) #f))) + (define-core-function not (x) not) + (define-core-function equal (x y) equal?) + (current-system))) + (define-syntax define-system (syntax-rules () ((_ name (system) expr ...) |