diff options
Diffstat (limited to 'vikalpa.scm')
| -rw-r--r-- | vikalpa.scm | 28 |
1 files changed, 15 insertions, 13 deletions
diff --git a/vikalpa.scm b/vikalpa.scm index f4ef953..5be2824 100644 --- a/vikalpa.scm +++ b/vikalpa.scm @@ -324,7 +324,7 @@ (eq? 'system (list-ref x 0)) (system-definitions? (system-definitions x)) (system-proofs? (system-proofs x)) - ((const #t) (system-totality-claims x)))) + ((const #t) (system-totality-claim-list x)))) (define (make-system defs prfs totality-claims) (list 'system defs prfs totality-claims)) @@ -335,7 +335,7 @@ (define (system-proofs sys) (list-ref sys 2)) -(define/guard (system-totality-claims (sys system?)) +(define (system-totality-claim-list sys) (list-ref sys 3)) (define (totality-claim id nat? less-than) @@ -628,7 +628,7 @@ (- x 1)) (define (natural->expr n) - (if (zero? n) + (if (<= n 0) ''0 `(succ ,(natural->expr (pred n))))) @@ -946,12 +946,12 @@ (cond ((lookup (definition-name x) sys) => (lambda (d) (if (equal? x d) - x + sys (error "(vikalpa) add-definition: duplicated" (definition-name d))))) (else (make-system (cons x (system-definitions sys)) (system-proofs sys) - (system-totality-claims sys))))) + (system-totality-claim-list sys))))) x)) (define (add-proof x) @@ -964,7 +964,7 @@ (error "add-proof: duplicated")))) (else (make-system (system-definitions sys) (cons x (system-proofs sys)) - (system-totality-claims sys))))) + (system-totality-claim-list sys))))) x)) (define reserved-symbols '(quote let if error)) @@ -1026,7 +1026,7 @@ m)))) (define (find-totality-claim name sys) - (assoc name (system-totality-claims sys))) + (assoc name (system-totality-claim-list sys))) (define (add-totality-claim tc) (let ((sys (current-system))) @@ -1047,14 +1047,13 @@ (current-system (make-system (system-definitions sys) (system-proofs sys) - (cons tc (system-totality-claims sys)))) - tc)) + (cons tc (system-totality-claim-list sys)))))) (define-syntax-rule (define-totality-claim name nat? <) (add-totality-claim (totality-claim 'name 'nat? '<))) (define* (core-system #:optional (parent (make-system '() '() '()))) - (parameterize ([current-system parent]) + (parameterize ((current-system parent)) (define-primitive-function not (x)) (define-primitive-function equal? (x y)) (define-primitive-function cons (x y)) @@ -1068,8 +1067,8 @@ (syntax-rules () ((_ name (systems ...) expr ...) (define* (name #:optional (parent (make-system '() '() '()))) - (parameterize ([current-system - ((compose systems ... core-system) parent)]) + (parameterize ((current-system + ((compose systems ... core-system) parent))) expr ... (unless (system? (current-system)) @@ -1342,7 +1341,7 @@ (define* (next #:optional fail) (loop (make-system (cdr defs) (system-proofs sys) - (system-totality-claims sys)) + (system-totality-claim-list sys)) (if fail (cons fail fails) fails))) @@ -1428,3 +1427,6 @@ (map macro-name (filter macro? (system-definitions sys)))) + +(define/guard (system-totality-claims (sys system?)) + (system-totality-claim-list sys)) |