summaryrefslogtreecommitdiff
diff options
context:
space:
mode:
authorMasaya Tojo <masaya@tojo.tokyo>2021-01-05 08:19:47 +0900
committerMasaya Tojo <masaya@tojo.tokyo>2021-01-05 08:19:47 +0900
commit54431be7b5461dde802d93f28b7b65f1139a8106 (patch)
treef28f1f6074db5ad8f3b1887476fb84e61d438d05
parent32ce95f0cb18145f1e5e307b665a3cd1c1750253 (diff)
wip64
-rw-r--r--vikalpa.scm34
-rw-r--r--vikalpa/prelude.scm8
2 files changed, 30 insertions, 12 deletions
diff --git a/vikalpa.scm b/vikalpa.scm
index 78b751a..dab81b2 100644
--- a/vikalpa.scm
+++ b/vikalpa.scm
@@ -233,11 +233,7 @@
;; (expression? x) -> boolean?
(define (expression? expr)
- (cond ((expr-quoted? expr)
- (or (exact-integer? (expr-unquote expr))
- (boolean? (expr-unquote expr))
- (symbol? (expr-unquote expr))
- (null? (expr-unquote expr))))
+ (cond ((expr-quoted? expr) #t)
((if-form? expr)
(and (expression? (if-form-test expr))
(expression? (if-form-then expr))
@@ -668,6 +664,7 @@
(and (pair? x)
(eq? 'error (car x))))
+
(define (rewrite/eval expr sys)
(let eval ((expr expr))
(cond
@@ -676,14 +673,29 @@
((app-form? expr)
(let ((args (map eval (app-form-args expr)))
(name (app-form-name expr)))
+ (define (guard-ok? vars form g)
+ (let ((result (eval (apply-rule '()
+ (rule vars '() form g)
+ `(,name ,@args)
+ '()))))
+ (if (error? result)
+ result
+ (expr-unquote result))))
(cond
((find error? args) => identity)
- (else
- (eval (rewrite1 sys
- `(,name ,@args)
- (lambda args
- (cons* 'error 'rewrite name args))
- `(rewrite () ,name)))))))
+ ((lookup name sys)
+ => (lambda (f)
+ (let ((gs (get-guards f))
+ (vars (get-variables f))
+ (form (defined-function-app-form f)))
+ (if (every (lambda (g) (guard-ok? vars form g)) gs)
+ (eval (rewrite1 sys
+ `(,name ,@args)
+ (lambda args
+ (cons* 'error 'rewrite name args))
+ `(rewrite () ,name)))
+ `(error guard-error (,name ,@args) (and ,@gs))))))
+ (else `(error function not-found)))))
((if-form? expr)
(let ((test (eval (if-form-test expr))))
(if (error? test)
diff --git a/vikalpa/prelude.scm b/vikalpa/prelude.scm
index 201e93d..2da6e8e 100644
--- a/vikalpa/prelude.scm
+++ b/vikalpa/prelude.scm
@@ -161,7 +161,13 @@
(set-measure-predicate natural?)
(set-measure-predicate <))
-(define-system prelude (prelude/measure/natural)
+(define-system prelude/pair (prelude/measure/natural)
+ (define-core-function pair? (x) pair?)
+ (define-core-function cons (x y) cons)
+ (define-core-function/guard car (x) (pair? x) car)
+ (define-core-function/guard cdr (x) (pair? x) cdr))
+
+(define-system prelude (prelude/pair)
(define-proof inexact?
((rewrite (2) if-nest)
(rewrite () if-same)))