diff options
-rw-r--r-- | vikalpa.scm | 235 |
1 files changed, 152 insertions, 83 deletions
diff --git a/vikalpa.scm b/vikalpa.scm index e610b80..b8d1bee 100644 --- a/vikalpa.scm +++ b/vikalpa.scm @@ -25,6 +25,11 @@ #:use-module (srfi srfi-8) #:use-module (srfi srfi-26)) +(define (debug f . args) + (if #f + (apply format #t f args) + (if #f #f))) + (define (option p?) (lambda (x) (or (p? x) (not x)))) @@ -123,66 +128,79 @@ (environment (cdr x)))) (else #f))) -;; (apply-rule preconds rule? expression?) -> (or (cons rhs environment) #f) (define (apply-rule preconds rl expr) + (call/cc (lambda (k) (apply-rule* preconds rl expr k)))) + +;; (apply-rule preconds rule? expression?) -> (or (cons rhs environment) #f) +(define (apply-rule* preconds rl expr fail) (define (var? v) (and (member v (rule-vars rl)) #t)) - (call/cc - (lambda (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))) - ((and (null? lhss) - (null? exprs)) - env) - (else (k #f)))) - (define (mat 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 #f))) - ((var? lhs) - (cond - ((assoc lhs env) - => (match-lambda - ((env-var . env-expr) - (if (equal? env-expr expr) - env - (k #f))))) - (else - (cons (cons lhs expr) - env)))) - (else (k #f)))) - (define (mat-preconds rlps env) - (if (null? rlps) - env - (mat-preconds (cdr rlps) - (any (lambda (p) (mat (car rlps) p env)) - preconds)))) - (define (substitute env expr) - (cond ((expr-quoted? expr) expr) - ((pair? expr) - (cons (substitute env (car expr)) - (substitute env (cdr expr)))) - ((and (variable? expr) (assoc expr env)) => cdr) - (else expr))) - (substitute (mat (rule-lhs rl) - expr - (mat-preconds (rule-preconds rl) '())) - (rule-rhs rl))))) + (define (mat-map lhss exprs env k) + (cond ((and (pair? lhss) + (pair? exprs)) + (mat-map (cdr lhss) + (cdr exprs) + (mat (car lhss) + (car exprs) + env + k) + k)) + ((and (null? lhss) + (null? exprs)) + env) + (else (k #f)))) + (define (mat lhs expr env k) + (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) + (cond + ((assoc lhs env) + => (match-lambda + ((env-var . env-expr) + (if (equal? env-expr expr) + env + (k #f))))) + (else + (cons (cons lhs expr) + env)))) + (else (k #f)))) + (define (mat-preconds rlps env) + (if (null? rlps) + env + (mat-preconds (cdr rlps) + (any (lambda (p) + (call/cc (lambda (k) + (mat (car rlps) p env + (lambda (x) (k #f)))))) + preconds)))) + (define (substitute env expr) + (cond ((expr-quoted? expr) expr) + ((pair? expr) + (cons (substitute env (car expr)) + (substitute env (cdr expr)))) + ((var? expr) + (cond ((assoc expr env) => cdr) + (else (fail #f)))) + (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) '()) + fail) + (rule-rhs rl))) ;; (book? x) -> boolean? ;; book is alist @@ -505,6 +523,7 @@ ;; (rewrite book? rewriter? expression? procedure?) -> expr (define (rewrite1 b expr fail r) (let ((cmd (rewriter-command r))) + (debug "~%~%cmd: ~a~%" cmd) (receive (extracted-expr preconds builder) (extract (rewriter-path r) expr fail) (builder @@ -547,6 +566,7 @@ (define/guard (rewrite (b book?) (expr expression?) (seq sequence?)) (let loop ((expr expr) (seq seq)) + (debug "~y~%" expr) (if (null? seq) expr (loop (rewrite1 b @@ -662,41 +682,64 @@ (error "define-book: error")) (current-book)))))) +(define (atom? x) + (not (pair? x))) + (define-book prelude () (define-axiom equal-same (x) (equal? (equal? x x) '#t)) + (define-axiom equal-swap (x y) (equal? (equal? x y) (equal? y x))) + (define-axiom equal-if (x y) (if (equal? x y) (equal? x y) '#t)) - (define-axiom pair/cons (x y) - (equal? (pair? (cons x y)) '#t)) + + (define-axiom atom/cons (x y) + (equal? (atom? (cons x y)) '#f)) (define-axiom car/cons (x y) (equal? (car (cons x y)) x)) (define-axiom cdr/cons (x y) (equal? (cdr (cons x y)) y)) - (define-axiom cons/car+cdr (x y) - (equal? (if (pair? x) - (equal? (cons (car x) (cdr y)) x) - '#t) - y)) - (define-axiom cons/car+cdr (x y) - (equal? (if (pair? x) - (equal? (cons (car x) (cdr y)) x) - '#t) - y)) + (define-axiom cons/car+cdr (x) + (if (atom? x) + '#t + (equal? (cons (car x) (cdr x)) x))) + + ;; バグる + ;; (define-axiom if-nest (x y z) + ;; (if x + ;; (equal? (if x y z) y) + ;; (equal? (if x y z) z))) + + (define-axiom if-false (x y) + (equal? (if '#f x y) y)) + + (define-axiom if-nest-t (x y z) + (if x + (equal? (if x y z) y) + '#t)) + (define-axiom if-nest-f (x y z) + (if x + '#t + (equal? (if x y z) z))) (define-axiom if-same (x y) (equal? (if x y y) y)) + + (define-axiom natural/size (x) + (equal? (natural? (size x)) + '#t)) (define-axiom size/car (x) - (if (pair? x) - (equal? (< (size x) (size (car x))) - '#t) - '#t)) + (if (atom? x) + '#t + (equal? (< (size (car x)) (size x)) + '#t))) + (define-axiom size/cdr (x) - (if (pair? x) - (equal? (< (size x) (size (cdr x))) - '#t) - '#t)) + (if (atom? x) + '#t + (equal? (< (size (cdr x)) (size x)) + '#t))) (define-macro list () ((list) '()) ((list x . y) (cons x (list . y)))) @@ -715,8 +758,6 @@ ((or) '#f) ((or x) x) ((or x . xs) (if x x (or . xs)))) - (define-macro atom? () - ((atom? x) (not (pair? x)))) (define-axiom if-not (x y z) (equal? (if (not x) y @@ -725,7 +766,7 @@ z y)))) -(define-book app (prelude) +(define-book app/book (prelude) (define-function app (x y) (if (atom? x) y @@ -733,7 +774,38 @@ (define-theorem associate-app (x y z) (equal? (app (app x y) z) - (app x (app y z))))) + (app x (app y z)))) + + #; + (rewrite (app/book) + '(if (atom? a) + (equal? (app (app a b) c) + (app a (app b c))) + (if (equal? (app (app (cdr a) b) c) + (app (cdr a) (app b c))) + (equal? (app (app a b) c) + (app a (app b c))) + '#t)) + '(((2 2) app) + ((2 2) if-nest-t) + ((2 1 1) app) + ((2 1 1) if-nest-t) + ((2) equal-same) + ((3 2 1 1) app) + ((3 2 1 1) if-nest-f) + ((3 2 2) app) + ((3 2 2) if-nest-f) + ((3 2 2 2) equal-if) + ((3 2 1) app) + ((3 2 1 3 1) car/cons) + ((3 2 1 3 2 1) cdr/cons) + ((3 2 1 1) atom/cons) + ((3 2 1) if-false) + ((3 2) equal-same) + ((3) if-same) + (() if-same))) + + ) (define (size x) (if (pair? x) @@ -742,9 +814,6 @@ (size (cdr x))) 0)) -(define (atom? x) - (not (pair? x))) - (define (app x y) (if (atom? x) y |