summaryrefslogtreecommitdiff
path: root/vikalpa.scm
diff options
context:
space:
mode:
Diffstat (limited to 'vikalpa.scm')
-rw-r--r--vikalpa.scm398
1 files changed, 167 insertions, 231 deletions
diff --git a/vikalpa.scm b/vikalpa.scm
index 74dbe6c..cc88c06 100644
--- a/vikalpa.scm
+++ b/vikalpa.scm
@@ -33,6 +33,7 @@
define-primitive-function
define-function
define-proof
+ define-totality-claim
define-syntax-rules
total/natural?
induction
@@ -214,77 +215,6 @@
(environment (cdr x))))
(else #f)))
-(define* (rebuild expr preconds
- #:key
- (quoted-proc (lambda (expr preconds) expr))
- (variable-proc (lambda (expr preconds) expr))
- (if-proc (lambda (expr preconds next) (next)))
- (app-form-proc (lambda (expr preconds next) (next))))
- (let rec ((expr expr)
- (preconds preconds))
- (cond
- ((expr-quoted? expr)
- (quoted-proc expr preconds))
- ((variable? expr)
- (variable-proc expr preconds))
- ((if-form? expr)
- (letrec ((next
- (lambda* (#:optional (expr expr))
- (let* ((expr/test (rec (if-form-test expr) preconds))
- (expr/then (rec (if-form-then expr) (cons (if-form-test expr) preconds)))
- (expr/else (rec (if-form-else expr) (cons (expr-not (if-form-test expr)) preconds))))
- (if-form expr/test expr/then expr/else)))))
- (if-proc expr preconds next)))
- ((app-form? expr)
- (letrec ((next
- (lambda* (#:optional (expr expr))
- (let f ((expr-args (app-form-args expr)))
- (cond ((null? expr-args) '())
- (else
- (cons (rec (car expr-args) preconds)
- (f (cdr expr-args)))))))))
- (app-form-proc expr preconds next)))
- (else
- (error "(vikalpa) rebuild: error")))))
-
-(define* (expr-fold expr acc preconds
- #:key
- (quoted-proc (lambda (expr acc preconds) acc))
- (variable-proc (lambda (expr acc preconds) acc))
- (if-proc (lambda (expr acc preconds next) (next)))
- (app-form-proc (lambda (expr acc preconds next) (next))))
- (let rec ((expr expr)
- (acc acc)
- (preconds preconds))
- (cond
- ((expr-quoted? expr)
- (quoted-proc expr acc preconds))
- ((variable? expr)
- (variable-proc expr acc preconds))
- ((if-form? expr)
- (letrec ((next
- (lambda* (#:optional (expr expr) (acc acc) (preconds preconds))
- (let* ((acc/test
- (rec (if-form-test expr) acc preconds))
- (acc/then
- (rec (if-form-then expr) acc/test (cons (if-form-test expr) preconds))))
- (rec (if-form-else expr) acc/then (cons (expr-not (if-form-test expr)) preconds))))))
- (if-proc expr acc preconds next)))
- ((app-form? expr)
- (letrec ((next
- (lambda* (#:optional (expr expr) (acc acc) (preconds preconds))
- (let fold ((expr-args (app-form-args expr))
- (acc acc))
- (cond ((null? expr-args) acc)
- (else
- (fold (cdr expr-args)
- (rec (car expr-args)
- acc
- preconds))))))))
- (app-form-proc expr acc preconds next)))
- (else
- (error "(vikalpa) expr-fold: error")))))
-
(define (substitute env expr)
(cond ((expr-quoted? expr) expr)
((pair? expr)
@@ -390,13 +320,14 @@
(define (system? x)
(and (list? x)
- (= 3 (length x))
+ (= 4 (length x))
(eq? 'system (list-ref x 0))
(system-definitions? (system-definitions x))
- (system-proofs? (system-proofs x))))
+ (system-proofs? (system-proofs x))
+ ((const #t) (system-totality-claims x))))
-(define (make-system defs prfs)
- (list 'system defs prfs))
+(define (make-system defs prfs totality-claims)
+ (list 'system defs prfs totality-claims))
(define (system-definitions sys)
(list-ref sys 1))
@@ -404,6 +335,21 @@
(define (system-proofs sys)
(list-ref sys 2))
+(define (system-totality-claims sys)
+ (list-ref sys 3))
+
+(define (totality-claim id nat? less-than)
+ (list id nat? less-than))
+
+(define (totality-claim-id x)
+ (list-ref x 0))
+
+(define (totality-claim-natural x)
+ (list-ref x 1))
+
+(define (totality-claim-less-than x)
+ (list-ref x 2))
+
(define (lookup x sys)
(assoc x (system-definitions sys)))
@@ -462,7 +408,7 @@
(define/guard (function (name variable?)
(vars vars?)
(expr expression?)
- (code any?)
+ (code (const #t))
(primitive boolean?))
(list name 'function vars expr code primitive))
@@ -599,7 +545,7 @@
(eq? (macro-name m) (car expr)))
(let loop ((rs (macro-mrules m)))
(cond ((null? rs)
- (error "macro fail" m expr))
+ (error "(vikalpa) macro fail" m expr))
((apply-mrule (car rs) (macro-literals m) expr) => identity)
(else (loop (cdr rs))))))
(else #f)))
@@ -827,9 +773,10 @@
(values extracted-expr
(case i
((1) '())
- ((2) (cons precond extracted-preconds))
- ((3) (cons (expr-not precond) extracted-preconds))
- (else (fail "(if) invaild path" path)))
+ ((2) (cons (prop-not (prop-not precond))
+ extracted-preconds))
+ ((3) (cons (prop-not precond) extracted-preconds))
+ (else (fail 'if-invaild-path path)))
(lambda (x)
(append (list-head expr i)
(list (builder x))
@@ -844,7 +791,7 @@
(list (builder x))
(list-tail expr (+ i 1)))))))
(else
- (fail "invalid path" path))))))
+ (fail 'invalid-path path))))))
(define (function->rules x)
(list (rule (function-vars x)
@@ -865,27 +812,27 @@
(cons (function-name f) args)
'()))
-(define (parse-options/theorem ops)
+(define (parse-options/theorem ops fail)
(if (null? ops)
(values '())
(receive (env)
- (parse-options/theorem (cdr ops))
+ (parse-options/theorem (cdr ops) fail)
(case (caar ops)
((set) (let ((op (car ops)))
(cons (cons (list-ref op 1)
(list-ref op 2))
env)))
(else
- (error "invalid option:" (car ops)))))))
+ (fail 'invalid-option (car ops)))))))
(define (rewrite/theorem cmd b thm preconds expr fail)
(receive (env)
- (parse-options/theorem (command-options cmd))
+ (parse-options/theorem (command-options cmd) fail)
(cond
((any (cut apply-rule preconds <> expr env)
(theorem*-rules thm)) => identity)
(else
- (fail (format #f "no match theorem ~a: ~s" cmd expr))))))
+ (fail 'apply-theorem cmd expr)))))
;; (rewrite system? rewriter? expression? procedure?) -> expr
(define (rewrite1 sys expr fail r)
@@ -901,7 +848,8 @@
(('equal? `(quote ,x) `(quote ,y))
(expr-quote (equal? x y)))
(else
- (fail "error: equal? ~a" extracted-expr))))
+ (fail 'equal? 'extracted-expr))))
+ ((eq? 'error cmd/name) (fail extracted-expr))
((and (symbol? cmd/name)
(lookup cmd/name sys))
=> (lambda (x)
@@ -913,10 +861,10 @@
((any (cut apply-rule '() <> extracted-expr '())
(function->rules x)) => identity)
(else
- (fail (format #f "no match-function (~a)" cmd)))))
+ (fail 'apply-function cmd extracted-expr))))
(else
- (fail "rewrite error" cmd)))))
- (else (fail "no cmd" cmd extracted-expr)))))))
+ (fail 'invalid-command cmd extracted-expr)))))
+ (else (fail 'command-not-found cmd extracted-expr)))))))
(define/guard (rewrite (sys system?) (expr expression?) (seq sequence?))
(debug "rewrite ~y~%" expr)
@@ -924,20 +872,25 @@
(seq seq))
(debug "~y~%" expr)
#;(format #t "~y~%" expr)
- (if (null? seq)
- expr
- (loop (rewrite1 sys
- expr
- (lambda (x . args)
- (apply error
- (format #f "rewrite: ~a" x)
- args))
- (car seq))
- (cdr seq)))))
+ (reset
+ (if (null? seq)
+ expr
+ (loop (rewrite1 sys
+ expr
+ (lambda args
+ (shift k (cons 'error args)))
+ (car seq))
+ (cdr seq))))))
(define (expr-not x)
(list 'not x))
+(define (prop-not x)
+ (match x
+ (('not ('not expr)) (prop-not expr))
+ (('not expr) expr)
+ (expr (expr-not expr))))
+
(define (expr-equal? x)
(and (list? x)
(= 3 (length x))
@@ -954,10 +907,14 @@
(define (expression->rules vars preconds expr)
(if (if-form? expr)
(append (expression->rules vars
- (cons (if-form-test expr) preconds)
+ (cons (prop-not
+ (prop-not
+ (if-form-test expr)))
+ preconds)
(if-form-then expr))
(expression->rules vars
- (cons (expr-not (if-form-test expr)) preconds)
+ (cons (prop-not (if-form-test expr))
+ preconds)
(if-form-else expr)))
(if (expr-equal? expr)
(list (rule vars
@@ -975,18 +932,20 @@
'()
(theorem*-expression def)))
-(define current-system (make-parameter (make-system '() '())))
+(define current-system (make-parameter (make-system '() '() '())))
(define (add-definition x)
(let ((sys (current-system)))
(current-system
- (cond ((lookup (theorem*-name x) sys)
- => (lambda (thm)
- (if (equal? x thm)
- sys
- (error "add-definition: error"))))
+ (cond ((lookup (definition-name x) sys)
+ => (lambda (d)
+ (if (equal? x d)
+ x
+ (error "(vikalpa) add-definition: duplicated"
+ (definition-name d)))))
(else (make-system (cons x (system-definitions sys))
- (system-proofs sys)))))
+ (system-proofs sys)
+ (system-totality-claims sys)))))
x))
(define (add-proof x)
@@ -996,12 +955,13 @@
=> (lambda (prf)
(if (equal? x prf)
sys
- (error "add-proof: error"))))
+ (error "add-proof: duplicated"))))
(else (make-system (system-definitions sys)
- (cons x (system-proofs sys))))))
+ (cons x (system-proofs sys))
+ (system-totality-claims sys)))))
x))
-(define reserved-symbols '(quote let if))
+(define reserved-symbols '(quote let if error))
(define (reserved? x)
(member x reserved-symbols))
@@ -1059,63 +1019,52 @@
(add-definition m)
m))))
-(define (size x)
- (if (pair? x)
- (+ 1
- (size (car x))
- (size (cdr x)))
- 0))
-(define (add1 n) (1+ n))
-(define (sub1 n) (1- n))
-
-(define (core-primitive-function)
- (list (primitive-function 'not '(x))
- (primitive-function 'equal? '(x y))
- (primitive-function 'pair? '(x))
- (primitive-function 'cons '(x y))
- (primitive-function 'car '(x))
- (primitive-function 'cdr '(x))
- (primitive-function 'size '(x))
- (primitive-function 'natural? '(x))
- (primitive-function 'add1 '(x))
- (primitive-function 'sub1 '(x))
- (primitive-function '< '(x y))))
-
-(define* (empty-system #:optional (parent (make-system '() '())))
+(define (find-totality-claim name sys)
+ (assoc name (system-totality-claims sys)))
+
+(define (add-totality-claim tc)
+ (let ((sys (current-system)))
+ (cond ((find-totality-claim (totality-claim-id tc) sys)
+ => (lambda (tc2)
+ (unless (equal? tc tc2)
+ (error "(vikalpa) define-totality-claim: duplicated"
+ tc)))))
+ (unless (and (symbol? (totality-claim-id tc))
+ (cond ((lookup (totality-claim-natural tc) sys)
+ => function*?)
+ (else #f))
+ (cond ((lookup (totality-claim-less-than tc) sys)
+ => function*?)
+ (else #f)))
+ (error "(vikalpa) define-totality-claim: invalid totality-claim"
+ tc))
+ (current-system
+ (make-system (system-definitions sys)
+ (system-proofs sys)
+ (cons tc (system-totality-claims sys))))
+ tc))
+
+(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])
(define-primitive-function not (x))
(define-primitive-function equal? (x y))
- (define-primitive-function pair? (x))
- (define-primitive-function cons (x y))
- (define-primitive-function car (x))
- (define-primitive-function cdr (x))
- (define-primitive-function size (x))
- (define-primitive-function natural? (x))
- (define-primitive-function add1 (x))
- (define-primitive-function sub1 (x))
- (define-primitive-function < (x y))
- (unless (system? (current-system))
- (error "define-system: error"))
(current-system)))
(define-syntax define-system
(syntax-rules ()
((_ name (systems ...) expr ...)
- (define* (name #:optional (parent (make-system '() '())))
+ (define* (name #:optional (parent (make-system '() '() '())))
(parameterize ([current-system
- ((compose systems ... empty-system) parent)])
+ ((compose systems ... core-system) parent)])
expr
...
(unless (system? (current-system))
- (error "define-system: error"))
+ (error "define-system: invalid system"))
(current-system))))))
-
-(define (atom? x)
- (not (pair? x)))
-
-(define (any? x) #t)
-
(define (measure? x)
(and (pair? x)
(variable? (car x))
@@ -1131,9 +1080,6 @@
(define (function-app-form f)
(cons (function-name f) (function-vars f)))
-(define (expand-all b expr)
- (expand* (filter macro? b) expr))
-
(define (single? x)
(and (pair? x)
(null? (cdr x))))
@@ -1164,7 +1110,7 @@
(else
(if/if x y ''#t))))
-(define (make-total-claim/natural m-expr f)
+(define (make-totality-claim tc m-expr f)
(let* ((name (function-name f)))
(define (convert app-form)
(cond
@@ -1176,9 +1122,11 @@
app-form
'())
=> identity)
- (else (error "make-total-claim/natural: convert error"
+ (else (error "make-totality-claim: convert error"
+ (function-name f)
+ m-expr
app-form))))
- (if/if `(natural? ,m-expr)
+ (if/if `(,(totality-claim-natural tc) ,m-expr)
(let loop ((expr (function-expression f)))
(cond
((expr-quoted? expr) ''#t)
@@ -1199,10 +1147,14 @@
(else (and/if (loop (car args))
(f (cdr args))))))))
(if (eq? name (app-form-name expr))
- (and/if `(< ,(convert expr) ,m-expr)
+ (and/if `(,(totality-claim-less-than tc)
+ ,(convert expr)
+ ,m-expr)
rest)
rest)))
- (else (error "(vikalpa) make-total-claim: error"))))
+ (else (error "(vikalpa) make-totality-claim: error"
+ (function-name f)
+ m-expr))))
''#t)))
(define/guard (make-induction-claim (f function*?)
@@ -1216,13 +1168,14 @@
(cons expr rest)
rest)))
((if-form? expr)
- (error "make-induction-claim: FAILED m(- -)m"))
+ (error "make-induction-claim(find-app-forms): not supported"
+ expr))
(else '())))
(let ((c (theorem*-expression t)))
(define (prop app-form)
(cond
((apply-rule '()
- (rule (function-vars f)
+ (rule vars
'()
(cons (function-name f) vars)
c)
@@ -1230,7 +1183,7 @@
'())
=> identity)
(else
- (error "make-induction-claim: fail"))))
+ (error "make-induction-claim: fail" app-form))))
(cond
((apply-function f vars)
=> (lambda (expr)
@@ -1273,24 +1226,12 @@
(define seed? (const #t))
(define-syntax define-proof
- (syntax-rules (total natural? induction)
- ((_ name
- (total/natural? m-expr)
- (((n ...) cmd ...) ...))
- (add-proof (proof 'name
- '(total/natural? m-expr)
- '(((n ...) cmd ...) ...))))
- ((_ name
- (induction (f var ...))
- (((n ...) cmd ...) ...))
- (add-proof (proof 'name
- '(induction (f var ...))
- '(((n ...) cmd ...) ...))))
+ (syntax-rules ()
((_ name
- ()
+ (seed ...)
(((n ...) cmd ...) ...))
(add-proof (proof 'name
- '()
+ '(seed ...)
'(((n ...) cmd ...) ...))))))
(define (function*? x)
@@ -1337,12 +1278,18 @@
(define (prove/theorem sys t pf)
(match (proof-seed pf)
- (('induction (f . vars))
- (rewrite sys
- (make-induction-claim (lookup f sys)
- vars
- t)
- (proof-sequence pf)))
+ ((f . vars)
+ (cond
+ ((lookup f sys)
+ => (lambda (seed)
+ (rewrite sys
+ (make-induction-claim seed
+ vars
+ t)
+ (proof-sequence pf))))
+ (else (error "(vikalpa) define-proof: induction function is not found."
+ (proof-name pf)
+ (cons f vars)))))
(()
(rewrite sys
(theorem*-expression t)
@@ -1352,12 +1299,20 @@
(define (prove/function sys f pf)
(match (proof-seed pf)
- (('total/natural? m-expr)
- (rewrite sys
- (make-total-claim/natural m-expr f)
- (proof-sequence pf)))
+ ((id m-expr)
+ (cond
+ ((find-totality-claim id sys)
+ => (lambda (tc)
+ (rewrite sys
+ (make-totality-claim tc m-expr f)
+ (proof-sequence pf))))
+ (else
+ (error "(vikalpa) define-proof: totality-claim is not found:"
+ (proof-name pf)
+ (proof-seed pf)))))
(else
- (error "prove/function: fail"))))
+ (error "define-proof: fail"
+ (proof-name pf) (proof-seed pf)))))
(define (system->scheme sys)
`(begin
@@ -1375,7 +1330,8 @@
(let ((defs (system-definitions sys)))
(define* (next #:optional fail)
(loop (make-system (cdr defs)
- (system-proofs sys))
+ (system-proofs sys)
+ (system-totality-claims sys))
(if fail
(cons fail fails)
fails)))
@@ -1383,12 +1339,9 @@
((null? defs) fails)
((or (theorem? (car defs))
(function? (car defs)))
- (cond
+ (cond
((and (function? (car defs))
(trivial-total? (car defs)))
- #;
- (format #t "`~a` is trivial total function.~%"
- (definition-name (car defs)))
(next))
(else
(cond
@@ -1397,61 +1350,44 @@
(let ((result (prove sys (car defs) pf)))
(cond
((equal? result ''#t)
- #;
- (format #t "`~a` is ~a.~%"
- (definition-name (car defs))
- (if (function? (car defs))
- "total function"
- "true"))
(next))
(else
- #;
- (format #t "`~a`'s proof is failed:~%~y"
- (definition-name (car defs))
- result)
(next (list (definition-name (car defs))
result)))))))
(else
- #;
- (format #t "`~a`'s proof is not found.~%"
- (definition-name (car defs)))
(next (list (definition-name (car defs)))))))))
(else
(next))))))
+(define (pp x)
+ (pretty-print x
+ #:width 79
+ #:max-expr-width 50))
+
(define/guard (show (sys system?) (name symbol?))
- (define (pp x)
- (pretty-print x
- #:width 79
- #:max-expr-width 50))
(cond
((lookup name sys)
=> (lambda (def)
(cond
((function? def)
- (pp
- `(define-function ,(function-name def) ,(function-vars def)
- ,(function-expression def))))
+ `(define-function ,(function-name def) ,(function-vars def)
+ ,(function-expression def)))
((theorem? def)
- (pp
- `(define-theorem ,(theorem*-name def) ,(theorem*-vars def)
- ,(theorem*-expression def))))
+ `(define-theorem ,(theorem*-name def) ,(theorem*-vars def)
+ ,(theorem*-expression def)))
((axiom? def)
- (pp
- `(define-axiom ,(theorem*-name def) ,(theorem*-vars def)
- ,(theorem*-expression def))))
+ `(define-axiom ,(theorem*-name def) ,(theorem*-vars def)
+ ,(theorem*-expression def)))
((primitive-function? def)
- (pp
- `(define-primitive-function
- ,(primitive-function-name def)
- ,(primitive-function-vars def))))
+ `(define-primitive-function
+ ,(primitive-function-name def)
+ ,(primitive-function-vars def)))
((macro? def)
- (pp
- `(define-syntax-rules ,(macro-name def))))
+ `(define-syntax-rules ,(macro-name def)))
(else
- (error "show: error")))))
+ `(error 'fatal-error ,name)))))
(else
- (format #t "~a: not found~%" name))))
+ `(error 'not-found ,name))))
(define/guard (load-system (sys system?))
(primitive-eval (system->scheme sys)))
generated by cgit v1.2.3 (git 2.44.0) at 2024-05-18 20:33:59 +0000