From 4307e82a22ad9b48f760252dc805b263e1170da4 Mon Sep 17 00:00:00 2001 From: Masaya Tojo Date: Thu, 19 Nov 2020 04:17:40 +0900 Subject: wip26 --- vikalpa.scm | 230 +++++++++++++++++++++++++++++++++++++----------------------- 1 file 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 . (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 '())) -- cgit v1.2.3