From 58da83a6f6bee9c614ee67c6823c20ac228be7f6 Mon Sep 17 00:00:00 2001 From: Masaya Tojo Date: Sun, 8 Nov 2020 03:43:42 +0900 Subject: wip4 --- rabbit-prover.scm | 194 ++++++++++++++++++++++++++++++++++++------------------ 1 file changed, 131 insertions(+), 63 deletions(-) (limited to 'rabbit-prover.scm') diff --git a/rabbit-prover.scm b/rabbit-prover.scm index 8c594a8..f84287a 100644 --- a/rabbit-prover.scm +++ b/rabbit-prover.scm @@ -18,8 +18,10 @@ (define-module (rabbit-prover) #:export (rewrite) + #:use-module (rabbit-prover syntax) + #:use-module (rabbit-prover primitive) #:use-module (ice-9 match) - #:use-module ((srfi srfi-1) #:select (every any append-map member)) + #:use-module ((srfi srfi-1) #:select (every any member)) #:use-module (srfi srfi-8) #:use-module (srfi srfi-26)) @@ -27,17 +29,6 @@ (lambda (x) (or (p? x) (not x)))) -(define-syntax-rule (define/assert (name (var pred?) ...) b b* ...) - (define (name var ...) - (unless (pred? var) - (error (format #f - "~a:~% expected: ~a~% given: " - 'name - 'pred?) - var)) - ... - b b* ...)) - ;; (expression? x) -> boolean? (define (expression? expr) (cond ((expr-quoted? expr) @@ -66,11 +57,6 @@ (define (expr-quote expr) (list 'quote expr)) -;; (natural? x) -> boolean? -(define (natural? x) - (and (integer? x) - (not (negative? x)))) - ;; (variable? x) -> boolean? (define (variable? x) (symbol? x)) @@ -131,8 +117,19 @@ #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) - (format #t "lhs: ~s, expr: ~s, env: ~s~%" lhs expr env) (cond ((expr-quoted? lhs) (if (expr-quoted? expr) (and (equal? lhs expr) @@ -142,52 +139,38 @@ (if (and (pair? expr) (symbol? (car lhs)) (eqv? (car lhs) (car expr))) - (let loop ((lhss (cdr lhs)) - (exprs (cdr expr)) - (env env)) - (cond ((and (pair? lhss) - (pair? exprs)) - (loop (cdr lhss) - (cdr exprs) - (mat (car lhss) - (car exprs) - env))) - ((and (null? lhss) - (null? exprs)) - env) - (else (k #f)))) + (mat-map (cdr lhs) (cdr expr) env) (k #f))) ((var? lhs) (cond ((assoc lhs env) - => (lambda (p) - (if (equal? (cdr p) expr) - env - (k #f)))) + => (match-lambda + ((env-var . env-expr) + (if (equal? env-expr expr) + env + (k #f))))) (else (cons (cons lhs expr) env)))) (else (k #f)))) - (define (apply-preconds rlps env) + (define (mat-preconds rlps env) (if (null? rlps) env - (apply-preconds (cdr rlps) - (any (lambda (p) (mat (car rlps) p env)) - preconds)))) + (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 - (apply-preconds (rule-preconds rl) '())) + (mat-preconds (rule-preconds rl) '())) (rule-rhs rl))))) -;; (substitute environment expression?) -> expression? -(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))) - ;; (book? x) -> boolean? ;; book is alist (define (book? x) @@ -248,7 +231,7 @@ ((option proof?) (list-ref x 4)))) ;; (function variable? vars? expression? (option proof?)) -> function? -(define/assert (function (name variable?) (vars vars?) (expr expression?) (proof (option proof))) +(define/guard (function (name variable?) (vars vars?) (expr expression?) (proof (option proof))) (list name 'function vars expr proof)) (define (function-name f) @@ -263,30 +246,99 @@ (define (function-proof f) (list-ref f 4)) +(define (mrule? x) + (and (list? x) + (= 4 (length x)) + (eq? 'mrule (list-ref x 0)) + (vars? (mrule-vars x)) + ((const #t) (mrule-lhs x)) + ((const #t) (mrule-rhs x)))) + +(define (mrule vars lhs rhs) + (list 'mrule vars lhs rhs)) + +(define (mrule-vars mrl) + (list-ref mrl 1)) + +(define (mrule-lhs mrl) + (list-ref mrl 2)) + +(define (mrule-rhs mrl) + (list-ref mrl 3)) + (define (macro? x) (and (list? x) (= 3 (length x)) - (variable? (list-ref x 0)) (eq? 'macro (list-ref x 1)) - (let ((rs (list-ref x 2))) - (and (list? rs) - (every rule? rs))))) + (variable? (macro-name x)) + (let ((mrls (macro-mrules x))) + (and (list? mrls) + (every mrule? mrls))))) (define (macro-name m) (list-ref m 0)) -(define (macro-rules m) +(define (macro-mrules m) (list-ref m 2)) (define (macro name rules) - (list 'macro name rules)) + (list name 'macro rules)) + +(define (apply-mrule rl expr) + (define (var? v) + (and (member v (mrule-vars rl)) + #t)) + (call/cc + (lambda (k) + (define (mat-map lhs-tree expr-tree env) + (cond ((and (pair? lhs-tree) + (pair? expr-tree)) + (mat-map (car lhs-tree) + (car expr-tree) + (mat-map (cdr lhs-tree) + (cdr expr-tree) + env))) + (else (mat lhs-tree expr-tree env)))) + (define (mat lhs expr env) + (cond ((expr-quoted? lhs) + (if (expr-quoted? expr) + (and (equal? lhs expr) + env) + (k #f))) + ((and (pair? lhs) + (pair? expr)) + (mat-map lhs expr env)) + ((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)))) + ((eqv? lhs expr) env) + (else (k #f)))) + (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 (mrule-lhs rl) + expr + '()) + (mrule-rhs rl))))) (define (apply-macro m expr) (cond ((and (pair? expr) (eq? (macro-name m) (car expr))) (let loop ((rs (macro-rules m))) (cond ((null? rs) expr) - ((apply-rule '() (car rs) expr) => + ((apply-mrule (car rs) expr) => (cut apply-macro m <>)) (else (loop (cdr rs)))))) (else expr))) @@ -311,7 +363,7 @@ ;; (axiom variable? vars? expression?) -> axiom? ;; axiom? is proposition -(define/assert (axiom (name variable?) (vars vars?) (expr expression?)) +(define/guard (axiom (name variable?) (vars vars?) (expr expression?)) (list name 'axiom vars expr)) (define (vars? x) @@ -328,7 +380,7 @@ (expression? (list-ref x 3)))) ;; (theorem name vars? expression? proof?) -> theorem? -(define/assert (theorem (name variable?) (vars vars?) (expr expression?) (p (option proof?))) +(define/guard (theorem (name variable?) (vars vars?) (expr expression?) (p (option proof?))) (list name 'theorem vars expr p)) ;; (theorem? x) -> boolean? @@ -355,7 +407,6 @@ (define (proposition? x) (or (axiom? x) (theorem? x) - (conjecture? x) (function? x))) (define (proposition-vars x) @@ -468,7 +519,7 @@ (fail "rewrite error"))))) (else (fail "no cmd (~a)" cmd))))))) -(define/assert (rewrite (b book?) (expr expression?) (seq sequence?)) +(define/guard (rewrite (b book?) (expr expression?) (seq sequence?)) (let loop ((expr expr) (seq seq)) (if (null? seq) @@ -564,4 +615,21 @@ '#t) y)) (define-axiom if-same (x y) - (equal? (if x y y) y)))) + (equal? (if x y y) y)) + (define-axiom size/car (x) + (if (pair? x) + (equal? (< (size x) (size (car x))) + '#t) + '#t)) + (define-axiom size/cdr (x) + (if (pair? x) + (equal? (< (size x) (size (cdr x))) + '#t) + '#t)))) + +(define (size x) + (if (pair? x) + (+ 1 + (size (car x)) + (size (cdr x))) + 0)) -- cgit v1.2.3