From 66beb641672385909e542720a59bab167f0349a4 Mon Sep 17 00:00:00 2001 From: Masaya Tojo Date: Tue, 17 Nov 2020 13:12:19 +0900 Subject: wip19 --- vikalpa.scm | 169 +++++++++++++++++++++++++++++++++++++++++++++++++++--------- 1 file changed, 144 insertions(+), 25 deletions(-) diff --git a/vikalpa.scm b/vikalpa.scm index bd55e69..335c653 100644 --- a/vikalpa.scm +++ b/vikalpa.scm @@ -342,9 +342,31 @@ => (cut substitute <> (rule-rhs rl))) (else #f))) -;; (system? x) -> boolean? -;; system is alist + (define (system? x) + (and (list? x) + (= 3 (length x)) + (eq? 'system (list-ref x 0)) + (system-definitions? (system-definitions x)) + (system-proofs? (system-proofs x)))) + +(define (system defs prfs) + (list 'system defs prfs)) + +(define (system-definitions sys) + (list-ref sys 1)) + +(define (system-proofs sys) + (list-ref sys 2)) + +(define (lookup x sys) + (assoc x (system-definitions sys))) + +(define (find-proof x sys) + (assoc x (system-proofs sys))) + +;; (system-definitions? x) -> boolean? +(define (system-definitions? x) (cond ((null? x) #t) ((pair? x) (and (pair? (car x)) @@ -352,7 +374,16 @@ (primitive-function? (car x)) (macro? (car x)) (function? (car x))) - (system? (cdr x)))) + (system-definitions? (cdr x)))) + (else #f))) + +;; (system-proofs? x) -> boolean? +(define (system-proofs? x) + (cond ((null? x) #t) + ((pair? x) + (and (pair? (car x)) + (proof? (car x)) + (system-proofs? (cdr x)))) (else #f))) (define (primitive-function? x) @@ -751,10 +782,7 @@ (else (fail "can't apply-primitive-function (~a)" cmd)))) ((macro? x) - (cond - ((apply-macro x extracted-expr) => identity) - (else - (fail "macro fail")))) + (fail "macro fail")) (else (fail "rewrite error"))))) (else (fail "no cmd (~a)" cmd))))))) @@ -815,47 +843,62 @@ '() (proposition-expression def))) -(define current-system (make-parameter '())) +(define current-system (make-parameter (system '() '()))) -(define (add-system x) - (let ((b (current-system))) +(define (add-definition x) + (let ((sys (current-system))) (current-system - (cond ((assoc (proposition-name x) b) + (cond ((lookup (proposition-name x) sys) => (lambda (prop) (if (equal? x prop) - b - (error "add-system: error")))) - (else (cons x b)))))) + sys + (error "add-definition: error")))) + (else (system (cons x (system-definitions sys)) + (system-proofs sys))))) + x)) + +(define (add-proof x) + (let ((sys (current-system))) + (current-system + (cond ((find-proof (proof-name x) sys) + => (lambda (prf) + (if (equal? x prf) + sys + (error "add-proof: error")))) + (else (system (system-definitions sys) + (cons x (system-proofs sys)))))) + x)) (define-syntax define-axiom (syntax-rules () ((_ name (var ...) expr) - (add-system (axiom 'name '(var ...) 'expr))))) + (add-definition (axiom 'name '(var ...) 'expr))))) (define-syntax define-theorem (syntax-rules () ((_ name (var ...) expr) - (add-system (theorem 'name '(var ...) 'expr))))) + (add-definition (theorem 'name '(var ...) 'expr))))) (define-syntax define-function (syntax-rules () ((_ name (var ...) expr) (let ((f (function 'name '(var ...) 'expr))) - (add-system f) + (add-definition f) f)))) (define-syntax define-macro (syntax-rules () ((_ name () ((lhs1 . lhs2) rhs) ...) - (add-system (macro 'name - (list (mrule '(lhs1 . lhs2) 'rhs) - ...)))))) + (add-definition (macro 'name + (list (mrule '(lhs1 . lhs2) 'rhs) + ...)))))) (define-syntax define-system (syntax-rules () ((_ name (systems ...) expr ...) - (define* (name #:optional (parent '())) - (parameterize ([current-system ((compose systems ... identity) parent)]) + (define* (name #:optional (parent (system '() '()))) + (parameterize ([current-system + ((compose systems ... identity) parent)]) expr ... (unless (system? (current-system)) @@ -1081,14 +1124,57 @@ (implies/if (if (null? app-forms) ''#t (fold implies/if c (map prop app-forms))) - (if/if (if-form-test expr) - (build (if-form-then expr)) - (build (if-form-else expr)))))) + (if/if (if-form-test expr) + (build (if-form-then expr)) + (build (if-form-else expr)))))) (else (let ((app-forms (find-app-forms expr))) (fold implies/if c (map prop app-forms)))))))) (else (error "make-induction-claim: fail<3>"))))) +(define (proof? x) + (and (list? x) + (= 4 (length x)) + (symbol? (proof-name x)) + (eq? 'proof (list-ref x 1)) + (seed? (proof-seed x)) + (sequence? (proof-sequence x)))) + +(define (proof name seed sequence) + (list name 'proof seed sequence)) + +(define (proof-name x) + (list-ref x 0)) + +(define (proof-seed x) + (list-ref x 2)) + +(define (proof-sequence x) + (list-ref x 3)) + +(define seed? (const #t)) + +(define-syntax define-proof + (syntax-rules (total natural? induction) + ((_ name + (total natural? (measure var ...)) + (((n ...) cmd ...) ...)) + (add-proof (proof 'name + '(total natural? (measure var ...)) + '(((n ...) cmd ...) ...)))) + ((_ name + (induction (f var ...)) + (((n ...) cmd ...) ...)) + (add-proof (proof 'name + '(induction (f var ...)) + '(((n ...) cmd ...) ...)))) + ((_ name + () + (((n ...) cmd ...) ...)) + (add-proof (proof 'name + '() + '(((n ...) cmd ...) ...)))))) + (define-system app/system (prelude) (define-function app (x y) (if (atom? x) @@ -1099,6 +1185,39 @@ (equal? (app (app x y) z) (app x (app y z)))) + (define-proof app + (total natural? (size x)) + (((2 3 2 1) app) + ((2 3 2 1) if-nest) + ((2 3 1 1) cdr/cons (set x (car a))) + ((2 3) if-same (set x (atom? (cons (car a) (app (cdr a) b))))) + ((2 3 3) size/cdr) + ((2 3 1) atom/cons) + ((2 3) if-false) + ((2) if-same) + (() if-same))) + + (define-proof associate-app + (induction (list-induction x)) + (((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))) + #; (rewrite (app/system) '(if (natural? (size (app a b))) -- cgit v1.2.3