diff options
Diffstat (limited to 'vikalpa.scm')
| -rw-r--r-- | vikalpa.scm | 91 |
1 files changed, 56 insertions, 35 deletions
diff --git a/vikalpa.scm b/vikalpa.scm index 6a2af81..8c3d10c 100644 --- a/vikalpa.scm +++ b/vikalpa.scm @@ -26,7 +26,7 @@ set-measure-predicate set-measure-less-than core-system - core-system/equal + core-system/equal-t-nil define-system define-proof define-core-function @@ -61,12 +61,22 @@ #:init-keyword #:definitions #:init-value '()) (equal-symbol #:getter get-equal-symbol - #:init-value 'equal?) + #:init-value 'equal? + #:init-keyword #:equal-symbol) + (true-object #:getter get-true-object + #:init-value ''#t + #:init-keyword #:true-object) + (false-object #:getter get-false-object + #:init-value ''#f + #:init-keyword #:false-object) (measure-predicate #:getter get-measure-predicate #:init-value #f) (measure-less-than #:getter get-measure-less-than #:init-value #f)) +(define-syntax-rule (true) (get-true-object (current-system))) +(define-syntax-rule (false) (get-false-object (current-system))) + (define-class <definition> () (name #:getter get-name #:init-keyword #:name) @@ -132,11 +142,6 @@ (equal? name (get-name x))) (get-definitions s))) -(define-method (update-equal-symbol (s <symbol>) (sys <system>)) - (let ((new (shallow-clone sys))) - (slot-set! new 'equal-symbol s) - new)) - (define-method (update-measure-predicate (s <symbol>) (sys <system>)) (let ((new (shallow-clone sys))) (slot-set! new 'measure-predicate s) @@ -1075,7 +1080,7 @@ #:guards (get-guards f) #:expression (get-expression f) #:code (get-code f) - #:claim ''#t + #:claim (true) #:proof '()))) (current-system (update-definition g (current-system))) (validate g))) @@ -1116,7 +1121,7 @@ #:name (get-name d) #:variables (get-variables d) #:expression (get-expression d) - #:claim ''#t + #:claim (true) #:proof '()) (make <admitted-function> #:name (get-name d) @@ -1124,7 +1129,7 @@ #:guards (get-guards d) #:expression (get-expression d) #:code (get-code d) - #:claim ''#t + #:claim (true) #:proof '())))) (validate g) (current-system (update-definition g (current-system)))))) @@ -1145,15 +1150,24 @@ (define-core-function equal? (x y) equal?) (current-system))) -(define (core-system/equal) - (parameterize ((current-system (make <system>))) - (current-system (update-equal-symbol 'equal (current-system))) +(define (core-system/equal-t-nil) + (parameterize ((current-system (make <system> + #:equal-symbol 'equal + #:true-object ''t + #:false-object ''nil))) (define-syntax-rules and () - ((and) '#t) + ((and) 't) ((and x) x) - ((and x . xs) (if x (and . xs) #f))) - (define-core-function not (x) not) - (define-core-function equal (x y) equal?) + ((and x . xs) (if x (and . xs) 'nil))) + (define-core-function equal (x y) (lambda (x y) + (if (equal? x y) + 't + 'nil))) + (define-core-function not (x) + (lambda (x) + (if (eq? x 'nil) + 't + 'nil))) (current-system))) (define-syntax define-system @@ -1216,28 +1230,28 @@ (define (smart-if x y z) (cond ((equal? y z) y) - ((equal? x ''#t) y) - ((equal? x ''#f) z) + ((equal? x (true)) y) + ((equal? x (false)) z) (else `(if ,x ,y ,z)))) (define (smart-and . args) (cond - ((null? args) ''#t) - ((equal? ''#t (car args)) (apply smart-and (cdr args))) + ((null? args) (true)) + ((equal? (true) (car args)) (apply smart-and (cdr args))) (else (let ((rest (apply smart-and (cdr args)))) - (if (equal? ''#t rest) + (if (equal? (true) rest) (car args) (smart-if (car args) rest - ''#f)))))) + (false))))))) (define (smart-implies x y) (cond - ((equal? ''#f x) ''#t) - ((equal? ''#t y) ''#t) + ((equal? (false) x) (true)) + ((equal? (true) y) (true)) (else - (smart-if x y ''#t)))) + (smart-if x y (true))))) (define (make-totality-claim* m-expr f) (let* ((name (get-name f))) @@ -1258,8 +1272,8 @@ (smart-if `(,(get-measure-predicate (current-system)) ,m-expr) (let loop ((expr (get-expression f))) (cond - ((expr-quoted? expr) ''#t) - ((variable? expr) ''#t) + ((expr-quoted? expr) (true)) + ((variable? expr) (true)) ((if-form? expr) (let ((test/result (loop (if-form-test expr))) (then/result (loop (if-form-then expr))) @@ -1271,7 +1285,7 @@ ((app-form? expr) (let ((rest (let f ((args (app-form-args expr))) - (cond ((null? args) ''#t) + (cond ((null? args) (true)) ((single? args) (loop (car args))) (else (smart-and (loop (car args)) (f (cdr args)))))))) @@ -1284,7 +1298,7 @@ (else (error "(vikalpa) make-totality-claim: error" (get-name f) m-expr)))) - ''#f))) + (false)))) (define (make-guard-claim expr) (define (find-preconds expr) @@ -1313,7 +1327,7 @@ (build (if-form-else expr)))) ((app-form? expr) (apply smart-and (map build/find-if (app-form-args expr)))) - (else ''#t))) + (else (true)))) (define (build expr) (cond ((if-form? expr) @@ -1326,7 +1340,7 @@ (apply smart-and (append (find-preconds expr) (list (build/find-if expr))))) - (else ''#t))) + (else (true)))) (build expr)) (define (make-induction-claim f vars c) @@ -1368,7 +1382,7 @@ ((if-form? expr) (let ((app-forms (find-app-forms (if-form-test expr)))) (smart-implies (if (null? app-forms) - ''#t + (true) (fold smart-implies c (map prop app-forms))) @@ -1607,7 +1621,7 @@ (if (lookup `(guard ,(get-name f)) (current-system)) #f (if (equal? (make-guard-claim (get-expression f)) - ''#t) + (true)) #f `((guard ,(get-name f)) (add (define-guard-theorem ,(get-name f))))))) @@ -1639,8 +1653,15 @@ (parameterize ((current-system sys)) (rewrite (get-claim d) (get-proof d)))))) + (display + (list result + (parameterize ((current-system sys)) + (result/expr (true))))) + (newline) (cond - ((equal? result (result/expr ''#t)) + ((equal? result + (parameterize ((current-system sys)) + (result/expr (true)))) (next)) (else (next (list (get-name d) result)))))) |