From ab5026c96d9cf1e5bd95776edafecf1cbd64c42c Mon Sep 17 00:00:00 2001 From: Masaya Tojo Date: Tue, 10 Nov 2020 02:40:55 +0900 Subject: wip14 --- vikalpa.scm | 141 ++++++++++++++++++++++++++++++++++++++++-------------------- 1 file changed, 95 insertions(+), 46 deletions(-) (limited to 'vikalpa.scm') diff --git a/vikalpa.scm b/vikalpa.scm index b8d1bee..6dadcd2 100644 --- a/vikalpa.scm +++ b/vikalpa.scm @@ -21,14 +21,15 @@ #:use-module (vikalpa syntax) #: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 (srfi srfi-8) #:use-module (srfi srfi-26)) (define (debug f . args) - (if #f + (if #t (apply format #t f args) - (if #f #f))) + #t)) (define (option p?) (lambda (x) @@ -128,14 +129,25 @@ (environment (cdr x)))) (else #f))) -(define (apply-rule preconds rl expr) - (call/cc (lambda (k) (apply-rule* preconds rl expr k)))) +(define (apply-rule preconds rl expr env) + (call/cc (lambda (k) (apply-rule* preconds rl expr env k)))) ;; (apply-rule preconds rule? expression?) -> (or (cons rhs environment) #f) -(define (apply-rule* preconds rl expr fail) +(define (apply-rule* preconds rl expr env fail) (define (var? v) (and (member v (rule-vars rl)) #t)) + (define (add-env var expr env k) + (cond + ((assoc var env) + => (match-lambda + ((env-var . env-expr) + (if (equal? env-expr expr) + env + (k #f))))) + (else + (cons (cons var expr) + env)))) (define (mat-map lhss exprs env k) (cond ((and (pair? lhss) (pair? exprs)) @@ -163,17 +175,7 @@ (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)))) + ((var? lhs) (add-env lhs expr env k)) (else (k #f)))) (define (mat-preconds rlps env) (if (null? rlps) @@ -198,7 +200,7 @@ (debug "expr: ~a~%" expr) (substitute (mat (rule-lhs rl) expr - (mat-preconds (rule-preconds rl) '()) + (mat-preconds (rule-preconds rl) env) fail) (rule-rhs rl))) @@ -445,20 +447,18 @@ ;; (rewriter path? command?) -> rewriter? (define (rewriter p c) - (list p c)) + (cons p c)) (define (rewriter-path r) - (list-ref r 0)) + (car r)) (define (rewriter-command r) - (list-ref r 1)) + (cdr r)) (define (rewriter? x) (and (pair? x) (path? (car x)) - (pair? (cdr x)) - (command? (car (cdr x))) - (null? (cdr (cdr x))))) + (command? (cdr x)))) ;; (sequence? x) -> boolean? (define (sequence? x) @@ -471,11 +471,33 @@ (and (list? x) (every natural? x))) -;; (command? x) -> booelan? +;; (command-name? x) -> booelan? (define (command? x) + (and (pair? x) + (command-name? (car x)) + ((list-of command-option?) (cdr x)))) + +;; (command-name? x) -> booelan? +(define (command-name? x) (or (symbol? x) ((list-of symbol?) x))) +;; (command-option? x) -> boolean? +(define (command-option? x) + (and (pair? x) + (case (car x) + ((set) (and (list? x) + (= 3 (length x)) + (variable? (list-ref x 1)) + (expression? (list-ref x 2)))) + (else #f)))) + +(define (command-name x) + (car x)) + +(define (command-options x) + (cdr x)) + ;; (extract path? expression? preconds? procedure?) -> (values expression? procedure?) (define (extract path expr fail) (if (null? path) @@ -520,34 +542,56 @@ (cons (function-name x) (function-vars x))))) +(define (parse-options/prop ops) + (if (null? ops) + (values '()) + (receive (env) + (parse-options/prop (cdr ops)) + (case (caar ops) + ((set) (let ((op (car ops))) + (cons (cons (list-ref op 1) + (list-ref op 2)) + env))) + (else + (error "invalid option:" (car ops))))))) + +(define (rewrite/prop cmd b prop preconds expr fail) + (receive (env) + (parse-options/prop (command-options cmd)) + (cond + ((any (cut apply-rule preconds <> expr env) + (proposition-rules prop)) => identity) + (else + (fail (format #f "no match-rule (~a)" cmd)))))) + ;; (rewrite book? rewriter? expression? procedure?) -> expr (define (rewrite1 b expr fail r) - (let ((cmd (rewriter-command r))) + (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 (cond - ((equal? cmd '(expand)) + ((equal? cmd/name '(look)) + (format #t "~y" extracted-expr) + (error "look")) + ((equal? cmd/name '(expand)) (expand (filter macro? b) extracted-expr)) - ((equal? cmd '(expand*)) + ((equal? cmd/name '(expand*)) (expand* (filter macro? b) extracted-expr)) - ((and (symbol? cmd) - (assoc cmd b)) + ((and (symbol? cmd/name) + (assoc cmd/name b)) => (lambda (x) (cond - ((proposition? x) - (cond - ((any (cut apply-rule preconds <> extracted-expr) - (proposition-rules x)) => identity) - (else - (fail (format #f "no match-rule (~a)" cmd))))) + ((proposition? x) (rewrite/prop cmd b x preconds extracted-expr fail)) ((function? x) (cond - ((any (cut apply-rule '() <> extracted-expr) + ((any (cut apply-rule '() <> extracted-expr '()) (function->rules x)) => identity) (else - (fail (format #f "no match-rule (~a)" cmd))))) + (fail (format #f "no match-function (~a)" cmd))))) ((primitive-function? x) (cond ((match-primitive-function x extracted-expr) @@ -567,6 +611,7 @@ (let loop ((expr expr) (seq seq)) (debug "~y~%" expr) + #;(format #t "~y~%" expr) (if (null? seq) expr (loop (rewrite1 b @@ -699,36 +744,40 @@ (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) (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-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-false (x y) + (equal? (if '#f x y) y)) + (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 (atom? x) '#t @@ -740,6 +789,7 @@ '#t (equal? (< (size (cdr x)) (size x)) '#t))) + (define-macro list () ((list) '()) ((list x . y) (cons x (list . y)))) @@ -804,7 +854,6 @@ ((3 2) equal-same) ((3) if-same) (() if-same))) - ) (define (size x) -- cgit v1.2.3