From 03361beae477d7bb1ebde3871d2230b9dd75a8a4 Mon Sep 17 00:00:00 2001 From: Masaya Tojo Date: Wed, 18 Nov 2020 23:17:18 +0900 Subject: wip23 --- vikalpa.scm | 30 +++++++++++++++--------------- 1 file changed, 15 insertions(+), 15 deletions(-) diff --git a/vikalpa.scm b/vikalpa.scm index c66e130..fb6b500 100644 --- a/vikalpa.scm +++ b/vikalpa.scm @@ -418,19 +418,6 @@ (define (primitive-function-vars pf) (list-ref pf 2)) -(define (match-primitive-function pf expression) - (and (pair? expression) - (eq? (primitive-function-name pf) (car expression)) - (list? (cdr expression)) - (every identity (map (lambda (pred expr) - (and (expr-quoted? expr) - (pred (expr-unquote expr)))) - (primitive-function-preds pf) - (cdr expression))))) - -(define (apply-primitive-function pf expression) - (apply (primitive-function-proc pf) (cdr expression))) - (define (function? x) (and (list? x) (= 4 (length x)) @@ -945,6 +932,18 @@ (error "define-system: error")) (current-system)))))) +(define-syntax system + (syntax-rules () + ((_ (systems ...) expr ...) + (lambda* (#:optional (parent (make-system '() '()))) + (parameterize ([current-system + ((compose systems ... identity) parent)]) + expr + ... + (unless (system? (current-system)) + (error "define-system: error")) + (current-system)))))) + (define (atom? x) (not (pair? x))) @@ -1271,7 +1270,7 @@ (proof-sequence pf))) (() (rewrite sys - (theorem*-expression pf) + (theorem*-expression t) (proof-sequence pf))) (else (error "prove/theorem: fail")))) @@ -1378,6 +1377,7 @@ (next (definition-name (car defs)))))))) (else (format #t "~a の証明がありません(しょぼ〜ん)~%" - (definition-name (car defs)))))))) + (definition-name (car defs))) + (next (definition-name (car defs)))))))) (else (next)))))) -- cgit v1.2.3