summaryrefslogtreecommitdiff
path: root/vikalpa.scm
diff options
context:
space:
mode:
Diffstat (limited to 'vikalpa.scm')
-rw-r--r--vikalpa.scm362
1 files changed, 248 insertions, 114 deletions
diff --git a/vikalpa.scm b/vikalpa.scm
index 671082a..dc5b6de 100644
--- a/vikalpa.scm
+++ b/vikalpa.scm
@@ -33,16 +33,20 @@
define-theorem
define-primitive-function
define-function
+ define-scheme-function
define-proof
define-totality-claim
define-syntax-rules
+ system-eval
+ natural?
succ
pred)
#:use-module (ice-9 match)
#:use-module (ice-9 format)
#:use-module (ice-9 control)
#:use-module ((srfi srfi-1)
- #:select (every any member lset-union fold append-map))
+ #:select (every any member lset-union fold append-map
+ find))
#:use-module (srfi srfi-8)
#:use-module (srfi srfi-11)
#:use-module (srfi srfi-26)
@@ -53,17 +57,40 @@
(apply format #t f args)
#t))
-(define-syntax-rule (define/guard (name (var pred?) ...) b b* ...)
+(define-syntax-rule (define/guard (name (var p?) ...) b b* ...)
(define (name var ...)
- (unless (pred? var)
+ (unless (p? var)
(error (format #f
"~a:~% expected: ~a~% given: "
'name
- 'pred?)
+ 'p?)
var))
...
b b* ...))
+(define-syntax define-type
+ (syntax-rules ()
+ ((_ name
+ constractor
+ (m p?)
+ (n t? getter-name getter) ...)
+ (begin
+ (define len (+ 1 (length (list n ...))))
+ (define (constractor getter-name ...)
+ (let ((data (make-list len)))
+ (list-set! data m 'name)
+ (list-set! data n getter-name)
+ ...
+ data))
+ (define (p? x)
+ (and (list? x)
+ (= len (length x))
+ (eq? 'name (list-ref x m))
+ (t? (list-ref x n)) ...))
+ (define (getter x)
+ (list-ref x n))
+ ...))))
+
;; (natural? x) -> boolean?
(define (natural? x)
(and (exact-integer? x)
@@ -141,7 +168,7 @@
(define (expression-vars expr)
(cond
- ((app-form? expr)
+ ((pair? expr)
(apply lset-union eq?
(map expression-vars (app-form-args expr))))
((variable? expr) (list expr))
@@ -323,7 +350,6 @@
=> (cut substitute <> (rule-rhs rl)))
(else #f)))
-
(define (system? x)
(and (list? x)
(= 4 (length x))
@@ -385,14 +411,16 @@
(define (primitive-function? x)
(and (list? x)
- (= 3 (length x))
+ (= 5 (length x))
(variable? (primitive-function-name x))
(eq? 'primitive-function (list-ref x 1))
- (vars? (primitive-function-vars x))))
+ (vars? (primitive-function-vars x))
+ ((option expression?) (primitive-function-expression x))
+ ((option code?) (primitive-function-code x))))
;; (primitive-function variable? vars?) -> primitive-function?
-(define (primitive-function name vs)
- (list name 'primitive-function vs))
+(define (primitive-function name vs expr code)
+ (list name 'primitive-function vs expr code))
(define (primitive-function-name pf)
(list-ref pf 0))
@@ -400,23 +428,39 @@
(define (primitive-function-vars pf)
(list-ref pf 2))
+(define (primitive-function-expression pf)
+ (list-ref pf 3))
+
+(define (primitive-function-code pf)
+ (list-ref pf 4))
+
(define (function? x)
(and (list? x)
- (= 6 (length x))
+ (= 5 (length x))
(variable? (function-name x))
(eq? 'function (list-ref x 1))
(vars? (function-vars x))
(expression? (function-expression x))
- ((const #t) (function-code x))
- (boolean? (function-primitive? x))))
+ ((option code?) (function-code x))))
+
+(define (code? x)
+ (and (list? x)
+ (= 2 (length x))
+ (eq? 'code (list-ref x 0))
+ ((const #t) (code-expr x))))
+
+(define (code x)
+ (list 'code x))
+
+(define (code-expr x)
+ (cadr x))
;; (function variable? vars? expression?) -> function?
(define/guard (function (name variable?)
(vars vars?)
(expr expression?)
- (code (const #t))
- (primitive boolean?))
- (list name 'function vars expr code primitive))
+ (code (option code?)))
+ (list name 'function vars expr code))
(define (function-name f)
(list-ref f 0))
@@ -430,9 +474,6 @@
(define (function-code f)
(list-ref f 4))
-(define (function-primitive? f)
- (list-ref f 5))
-
(define (definition-name d)
(list-ref d 0))
@@ -644,26 +685,10 @@
,(pair->expr (cdr x)))
(expr-quote x)))
-(define (expand-quoted x)
- (cond
- ((expr-quoted? x)
- (let ((val (expr-unquote x)))
- (cond
- ((natural? val)
- (natural->expr val))
- ((pair? val)
- (pair->expr val))
- (else x))))
- ((pair? x)
- (cons (expand-quoted (car x))
- (expand-quoted (cdr x))))
- (else x)))
-
(define (convert-to-expression x)
- (expand-quoted
- (quote-all
- (expand* (filter macro? (system-definitions (current-system)))
- (expand-let x)))))
+ (quote-all
+ (expand* (filter macro? (system-definitions (current-system)))
+ (expand-let x))))
;; (axiom variable? vars? expression?) -> axiom?
;; axiom? is theorem*
@@ -719,6 +744,39 @@
'()
(theorem*-expression x)))
+(define (error? x)
+ (and (pair? x)
+ (eq? 'error (car x))))
+
+(define (rewrite/eval expr sys)
+ (let eval ((expr expr))
+ (cond
+ ((error? expr) expr)
+ ((expr-quoted? expr) expr)
+ ((app-form? expr)
+ (let ((args (map eval (app-form-args expr)))
+ (name (app-form-name expr)))
+ (or (find error? args)
+ (eval (rewrite1 sys
+ `(,name ,@args)
+ (lambda args
+ (cons* 'error rewrite name args))
+ (rewriter '() `(,name)))))))
+ ((if-form? expr)
+ (let ((test (eval (if-form-test expr))))
+ (if (error? test)
+ test
+ (if (expr-unquote test)
+ (eval (if-form-then expr))
+ (eval (if-form-else expr))))))
+ (else
+ `(error eval invalid-expression ,expr)))))
+
+(define/guard (system-eval (expr (const #t)) (sys system?))
+ (rewrite/eval (parameterize ((current-system sys))
+ (convert-to-expression expr))
+ sys))
+
;; (rewriter path? command?) -> rewriter?
(define (rewriter p c)
(cons p c))
@@ -809,10 +867,10 @@
(list (rule (function-vars x)
'()
(function-app-form x)
- (function-expression x))
+ (definition-expression x))
(rule (function-vars x)
'()
- (function-expression x)
+ (definition-expression x)
(function-app-form x))))
(define (apply-function f args)
@@ -854,24 +912,10 @@
(extract (rewriter-path r) expr fail)
(builder
(cond
- ((eq? 'equal? cmd/name)
- (match extracted-expr
- (('equal? `(quote ,x) `(quote ,y))
- (expr-quote (equal? x y)))
- (else
- (fail 'equal? extracted-expr))))
- ((eq? 'pair? cmd/name)
- (match extracted-expr
- (('pair? `(quote ,x))
- (expr-quote (pair? x)))
- (else
- (fail 'pair? extracted-expr))))
- ((eq? 'not cmd/name)
- (match extracted-expr
- (('not `(quote ,x))
- (expr-quote (not x)))
- (else
- (fail 'not extracted-expr))))
+ ((core-function-name? cmd/name)
+ (rewrite/core cmd/name extracted-expr fail))
+ ((equal? '(eval) cmd/name)
+ (rewrite/eval extracted-expr sys))
((eq? 'error cmd/name) (fail extracted-expr))
((and (symbol? cmd/name)
(lookup cmd/name sys))
@@ -879,7 +923,9 @@
(cond
((theorem*? x)
(rewrite/theorem cmd sys x preconds extracted-expr fail))
- ((function? x)
+ ((or (function? x)
+ (and (primitive-function? x)
+ (primitive-function-expression x)))
(cond
((any (cut apply-rule '() <> extracted-expr '())
(function->rules x)) => identity)
@@ -1012,23 +1058,24 @@
((_ name (var ...) expr)
(let ((f (function 'name '(var ...)
(convert-to-expression 'expr)
- 'expr
- #f)))
+ (code 'expr))))
(add-definition f)
(validate-definition f)
f))))
-(define-syntax define-primitive-function
+(define-syntax define-core-function
(syntax-rules ()
((_ name (var ...))
- (let ((f (primitive-function 'name '(var ...))))
+ (let ((f (primitive-function 'name '(var ...) #f #f)))
(add-definition f)
- f))
+ f))))
+
+(define-syntax define-primitive-function
+ (syntax-rules ()
((_ name (var ...) expr)
- (let ((f (function 'name '(var ...)
- (convert-to-expression 'expr)
- 'expr
- '#t)))
+ (let ((f (primitive-function 'name '(var ...)
+ (convert-to-expression 'expr)
+ (code 'expr))))
(add-definition f)
(validate-definition f)
f))))
@@ -1070,16 +1117,90 @@
(define-syntax-rule (define-totality-claim name nat? <)
(add-totality-claim (totality-claim 'name 'nat? '<)))
+(define core-function-names
+ '(not equal? pair? cons car cdr integer? < succ pred))
+
+(define (core-function-name? x)
+ (member x core-function-names))
+
+(define (rewrite/core name extracted-expr fail)
+ (case name
+ ((not)
+ (match extracted-expr
+ (('not `(quote ,x))
+ (expr-quote (not x)))
+ (else
+ (fail 'not extracted-expr))))
+ ((equal?)
+ (match extracted-expr
+ (('equal? `(quote ,x) `(quote ,y))
+ (expr-quote (equal? x y)))
+ (else
+ (fail 'equal? extracted-expr))))
+ ((pair?)
+ (match extracted-expr
+ (('pair? `(quote ,x))
+ (expr-quote (pair? x)))
+ (else
+ (fail 'pair? extracted-expr))))
+ ((cons)
+ (match extracted-expr
+ (('cons `(quote ,x) `(quote ,y))
+ (expr-quote (cons x y)))
+ (else
+ (fail 'cons extracted-expr))))
+ ((car)
+ (match extracted-expr
+ (('car `(quote ,x))
+ (if (pair? x)
+ (expr-quote (car x))
+ ''undefined))
+ (else
+ (fail 'car extracted-expr))))
+ ((cdr)
+ (match extracted-expr
+ (('cdr `(quote ,x))
+ (if (pair? x)
+ (expr-quote (cdr x))
+ ''undefined))
+ (else
+ (fail 'cdr extracted-expr))))
+ ((integer?)
+ (match extracted-expr
+ (('integer? `(quote ,x))
+ (expr-quote (integer? x)))
+ (else
+ (fail 'integer? extracted-expr))))
+ ((succ)
+ (match extracted-expr
+ (('succ `(quote ,x))
+ (if (integer? x)
+ (expr-quote (succ x))
+ ''undefined))
+ (else
+ (fail 'succ extracted-expr))))
+ ((pred)
+ (match extracted-expr
+ (('pred `(quote ,x))
+ (if (integer? x)
+ (expr-quote (pred x))
+ ''undefined))
+ (else
+ (fail 'pred extracted-expr))))
+ (else (fail 'rewrite/core 'invalid))))
+
(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 y))
- (define-primitive-function cons (x y))
- (define-primitive-function car (x))
- (define-primitive-function cdr (x))
- (define-primitive-function succ (x))
- (define-primitive-function pred (x))
+ (define-core-function not (x))
+ (define-core-function equal? (x y))
+ (define-core-function pair? (x y))
+ (define-core-function cons (x y))
+ (define-core-function car (x))
+ (define-core-function cdr (x))
+ (define-core-function integer? (x))
+ (define-core-function < (x y))
+ (define-core-function succ (x))
+ (define-core-function pred (x))
(current-system)))
(define-syntax define-system
@@ -1267,32 +1388,34 @@
(or (function? x)
(primitive-function? x)))
-(define (validate-definition d)
- (let* ((expr (definition-expression d))
- (vars (definition-vars d))
- (name (definition-name d))
- (expr-fnames (expression-functions expr))
+(define (validate-expression sys name vars expr)
+ (let* ((expr-fnames (expression-functions expr))
(expr-vars (expression-vars expr)))
(when (reserved? name)
(error (format #f "(vikalpa) ~a: reserved name" name)))
(for-each (lambda (x)
- (unless (cond
- ((lookup x (current-system)) => function*?)
- (else #f))
+ (when (member x expr-fnames)
+ (error (format #f "(vikalpa) ~a: invalid variable name" name)
+ x)))
+ vars)
+ (for-each (lambda (x)
+ (unless (cond ((lookup x sys) => function*?)
+ (else #f))
(error (format #f "(vikalpa) ~a: undefined function" name)
x)))
expr-fnames)
(for-each (lambda (x)
(unless (member x vars)
(error (format #f "(vikalpa) ~a: undefined variable" name)
- x))
- (when (member x (if (function? d)
- (cons name expr-fnames)
- expr-fnames))
- (error (format #f "(vikalpa) ~a: invalid variable name" name)
x)))
expr-vars)))
+(define (validate-definition d)
+ (let* ((vars (definition-vars d))
+ (name (definition-name d))
+ (expr (definition-expression d)))
+ (validate-expression (current-system) name vars expr)))
+
(define (trivial-total? f)
(not (member (function-name f)
(expression-functions (function-expression f)))))
@@ -1306,25 +1429,31 @@
(else (error "prove" def pf))))
(define (prove/theorem sys t pf)
- (match (proof-seed 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)
- (proof-sequence pf)))
- (else
- (error "prove/theorem: fail"))))
+ (let ((sys-without-self
+ (make-system (filter (lambda (d) (not (equal? t d)))
+ (system-definitions sys))
+ (system-proofs sys)
+ (system-totality-claim-list sys))))
+ (match (proof-seed pf)
+ ((f . vars)
+ (cond
+ ((lookup f sys-without-self)
+ => (lambda (seed)
+ (let ((claim (make-induction-claim seed vars t)))
+ (validate-expression sys
+ `(claim-of ,(proof-name pf))
+ (theorem*-vars t)
+ claim)
+ (rewrite sys-without-self claim (proof-sequence pf)))))
+ (else (error "(vikalpa) define-proof: induction function is not found."
+ (proof-name pf)
+ (cons f vars)))))
+ (()
+ (rewrite sys-without-self
+ (theorem*-expression t)
+ (proof-sequence pf)))
+ (else
+ (error "prove/theorem: fail")))))
(define (prove/function sys f pf)
(match (proof-seed pf)
@@ -1332,9 +1461,14 @@
(cond
((find-totality-claim id sys)
=> (lambda (tc)
- (rewrite sys
- (make-totality-claim tc m-expr f)
- (proof-sequence pf))))
+ (let ((claim (make-totality-claim tc m-expr f)))
+ (validate-expression sys
+ `(claim-of ,(function-name f))
+ (function-vars f)
+ claim)
+ (rewrite sys
+ claim
+ (proof-sequence pf)))))
(else
(error "(vikalpa) define-proof: totality-claim is not found:"
(proof-name pf)
@@ -1347,10 +1481,10 @@
`(begin
,@(map (lambda (f)
`(define (,(function-name f) ,@(function-vars f))
- ,(function-code f)))
+ ,(code-expr (function-code f))))
(reverse (filter (lambda (x)
- (and (function? x)
- (not (function-primitive? x))))
+ (and (function*? x)
+ (function-code x)))
(system-definitions sys))))))
(define/guard (check (sys system?))
generated by cgit v1.2.3 (git 2.44.0) at 2024-05-18 22:22:48 +0000