From 32ce95f0cb18145f1e5e307b665a3cd1c1750253 Mon Sep 17 00:00:00 2001 From: Masaya Tojo Date: Tue, 5 Jan 2021 07:55:52 +0900 Subject: wip63 --- vikalpa.scm | 132 ++++++++++++++++++++++++---------------------------- vikalpa/prelude.scm | 53 ++++++++++----------- 2 files changed, 88 insertions(+), 97 deletions(-) diff --git a/vikalpa.scm b/vikalpa.scm index d1da85b..78b751a 100644 --- a/vikalpa.scm +++ b/vikalpa.scm @@ -121,9 +121,9 @@ (define-method (write (d ) port) (write-definition 'total-function d port)) -(define-method (lookup (name ) (s )) +(define-method (lookup name (s )) (find (lambda (x) - (eq? name (get-name x))) + (equal? name (get-name x))) (get-definitions s))) (define-method (update-measure-predicate (s ) (sys )) @@ -185,7 +185,7 @@ (define-method (validate (d )) (let* ((vars (get-variables d)) (name (get-name d))) - (validate-vars (symbol->string name) vars))) + (validate-vars (format #f "~a" name) vars))) (define-method (validate (d )) (let* ((vars (get-variables d)) @@ -683,7 +683,7 @@ `(,name ,@args) (lambda args (cons* 'error 'rewrite name args)) - (rewriter '() `(,name)))))))) + `(rewrite () ,name))))))) ((if-form? expr) (let ((test (eval (if-form-test expr)))) (if (error? test) @@ -696,20 +696,14 @@ (else `(error eval invalid-expression ,expr))))) -;; (rewriter path? command?) -> rewriter? -(define (rewriter p c) - (cons p c)) - -(define (rewriter-path r) - (car r)) - -(define (rewriter-command r) - (cdr r)) - (define (rewriter? x) - (and (pair? x) - (path? (car x)) - (command? (cdr x)))) + (match x + (('rewrite path command-name command-ops ...) + (and (path? path) + (command-name? command-name) + (every command-option? command-ops))) + (('eval path) (path? path)) + (else #f))) ;; (sequence? x) -> boolean? (define (sequence? x) @@ -723,15 +717,7 @@ (every natural? x))) ;; (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))) +(define (command-name? x) #t) ;; (command-option? x) -> boolean? (define (command-option? x) @@ -820,14 +806,14 @@ (else (fail 'invalid-option (car ops))))))) -(define (rewrite/theorem cmd b thm preconds expr fail) +(define (rewrite/theorem cmd-name cmd-ops b thm preconds expr fail) (receive (env) - (parse-options/theorem (command-options cmd) fail) + (parse-options/theorem cmd-ops fail) (cond ((any (cut apply-rule preconds <> expr env) (theorem-rules thm)) => identity) (else - (fail 'apply-theorem cmd expr))))) + (fail 'apply-theorem cmd-name expr))))) (define (rewrite/induction sys fname vars expr fail) (cond @@ -846,36 +832,37 @@ (fail 'apply-core-function (get-name f) expr))) (define (rewrite1 sys expr fail r) - (let* ((cmd (rewriter-command r)) - (cmd/name (command-name cmd))) - (debug "~%~%cmd: ~a~%" cmd) - (receive (extracted-expr preconds builder) - (extract (rewriter-path r) expr fail) - (builder - (cond - ((equal? '(eval) cmd/name) - (let ((result (rewrite/eval extracted-expr sys))) - (if (error? result) - (fail 'eval (cddr result) extracted-expr) - result))) - ((and (symbol? cmd/name) - (lookup cmd/name sys)) - => (lambda (x) - (cond - ((is-a? x ) - (rewrite/core-function sys x extracted-expr fail)) - ((is-a? x ) - (rewrite/theorem cmd sys x preconds extracted-expr fail)) - ((is-a? x ) - (cond - ((any (cut apply-rule '() <> extracted-expr '()) - (function->rules x)) - => identity) - (else - (fail 'apply-function cmd extracted-expr)))) - (else - (fail 'invalid-command cmd extracted-expr))))) - (else (fail 'command-not-found cmd extracted-expr))))))) + (match r + (('eval path) + (receive (extracted-expr preconds builder) + (extract path expr fail) + (builder + (let ((result (rewrite/eval extracted-expr sys))) + (if (error? result) + (fail 'eval (cddr result) extracted-expr) + result))))) + (('rewrite path command-name command-ops ...) + (receive (extracted-expr preconds builder) + (extract path expr fail) + (builder + (cond + ((lookup command-name sys) + => (lambda (x) + (cond + ((is-a? x ) + (rewrite/core-function sys x extracted-expr fail)) + ((is-a? x ) + (rewrite/theorem command-name command-ops sys x preconds extracted-expr fail)) + ((is-a? x ) + (cond + ((any (cut apply-rule '() <> extracted-expr '()) + (function->rules x)) + => identity) + (else + (fail 'apply-function command-name extracted-expr)))) + (else + (fail 'invalid-command command-name extracted-expr))))) + (else (fail 'command-not-found command-name extracted-expr)))))))) (define (rewrite sys expr seq) (let loop ((expr expr) @@ -1276,15 +1263,18 @@ (define (validate-sequence sys d seq) (for-each (lambda (r) - (for-each (lambda (x) - (match x - (('set var expr) - (validate-expression sys - `(define-proof ,(get-name d)) - (get-variables d) - expr)) - (else #f))) - (rewriter-command r))) + (match r + (('rewrite _ _ . command-ops) + (for-each (lambda (x) + (match x + (('set var expr) + (validate-expression sys + `(define-proof ,(get-name d)) + (get-variables d) + expr)) + (else #f))) + command-ops)) + (else #f))) seq)) (define (add-proof/function sys f seed seq) @@ -1309,8 +1299,8 @@ (update-claim (fold implies/if (and/if (make-totality-claim* sys seed f) - (make-guard-claim (get-expression f) - sys)) + (make-guard-claim (get-expression f) + sys)) (get-guards f)))) (raise-exception (make-exception @@ -1543,7 +1533,7 @@ (define (system? x) (is-a? x )) -(define/guard (system-lookup (sys system?) (name symbol?)) +(define/guard (system-lookup (sys system?) (name (const #t))) (cond ((lookup name sys) => show) (else #f))) diff --git a/vikalpa/prelude.scm b/vikalpa/prelude.scm index 176983c..201e93d 100644 --- a/vikalpa/prelude.scm +++ b/vikalpa/prelude.scm @@ -163,34 +163,35 @@ (define-system prelude (prelude/measure/natural) (define-proof inexact? - (((2) if-nest) - (() if-same))) + ((rewrite (2) if-nest) + (rewrite () if-same))) (define-proof inexact-predicate - (((1) inexact?) - (() if-not) - ((3 1) inexact?) - ((3 1 1) equal-if-false) - ((3) (eval)) - (() if-same))) + ((rewrite (1) inexact?) + (rewrite () if-not) + (rewrite (3 1) inexact?) + (rewrite (3 1 1) equal-if-false) + (eval (3)) + (rewrite () if-same))) (define-proof positive? - (((2 1 1) (eval)) - ((2 1) if-true) - ((2) if-nest) - (() if-same))) + ((eval (2 1 1)) + (rewrite (2 1) if-true) + (rewrite (2) if-nest) + (rewrite () if-same))) (define-proof positive-predicate - (((1) positive?) - ((2 1) positive?) - ((2 1) less-than-predicate) - ((2) (eval)) - (() if-same))) + ((rewrite (1) positive?) + (rewrite (2 1) positive?) + (rewrite (2 1) less-than-predicate) + (eval (2)) + (rewrite () if-same))) (define-proof negative? - (((2 1) if-nest) - ((2 1) (eval)) - ((2) if-true) - (() if-same))) + ((rewrite (2 1) if-nest) + (eval (2 1)) + (rewrite (2) if-true) + (rewrite () if-same))) (define-proof negative-predicate - (((1) negative?) - ((2 1) negative?) - ((2 1) less-than-predicate) - ((2) (eval)) - (() if-same)))) + ((rewrite (1) negative?) + (rewrite (2 1) negative?) + (rewrite (2 1) less-than-predicate) + (eval (2)) + (rewrite () if-same)))) + -- cgit v1.2.3