diff options
Diffstat (limited to 'vikalpa.scm')
-rw-r--r-- | vikalpa.scm | 74 |
1 files changed, 59 insertions, 15 deletions
diff --git a/vikalpa.scm b/vikalpa.scm index 5151204..fcb9005 100644 --- a/vikalpa.scm +++ b/vikalpa.scm @@ -17,14 +17,16 @@ ;;; along with Vikalpa. If not, see <http://www.gnu.org/licenses/>. (define-module (vikalpa) - #:export (check + #:export (rewrite + show + check system->scheme define-system define-axiom define-theorem define-primitive-function define-function - define-macro) + define-syntax-rules) #:use-module (ice-9 match) #:use-module (ice-9 format) #:use-module (ice-9 control) @@ -32,7 +34,8 @@ #:select (every any member lset-union fold append-map)) #:use-module (srfi srfi-8) #:use-module (srfi srfi-11) - #:use-module (srfi srfi-26)) + #:use-module (srfi srfi-26) + #:use-module (ice-9 pretty-print)) (define (debug f . args) (if #f @@ -586,7 +589,7 @@ (else (loop (cdr rs)))))) (else #f))) -(define/guard (expand (ms (list-of macro?)) (expr (const #t))) +(define (expand ms expr) (let loop ((ms ms) (expr expr)) (cond @@ -596,7 +599,7 @@ ((apply-macro (car ms) expr) => identity) (else expr))))))) -(define/guard (expand* (ms (list-of macro?)) (expr (const #t))) +(define (expand* ms expr) (let loop ((ms ms) (expr expr)) (let ((new-expr (expand ms expr))) @@ -609,10 +612,11 @@ (define (quote-all x) (cond + ((null? x) x) ((expr-quoted? x) x) ((pair? x) - (cons (expand-let (car x)) - (expand-let (cdr x)))) + (cons (quote-all (car x)) + (quote-all (cdr x)))) ((symbol? x) x) (else `',x))) @@ -657,8 +661,9 @@ (else x))) (define (convert-to-expression x) - (expand* (filter macro? (system-definitions (current-system))) - (quote-all (expand-let x)))) + (quote-all + (expand* (filter macro? (system-definitions (current-system))) + (expand-let x)))) ;; (axiom variable? vars? expression?) -> axiom? ;; axiom? is theorem* @@ -948,6 +953,9 @@ (cons x (system-proofs sys)))))) x)) +(define (reserved? x) + (member x '(if quote let))) + (define-syntax define-axiom (syntax-rules () ((_ name (var ...) expr) @@ -983,7 +991,7 @@ (add-definition f) f)))) -(define-syntax define-macro +(define-syntax define-syntax-rules (syntax-rules () ((_ name (l ...) ((lhs1 . lhs2) rhs) ...) (let ((m (macro 'name @@ -1082,21 +1090,21 @@ (equal? (if (not x) y z) (if x z y))) - (define-macro list () + (define-syntax-rules list () ((list) '()) ((list x . y) (cons x (list . y)))) - (define-macro and () + (define-syntax-rules and () ((and) '#t) ((and x) x) ((and x . xs) (if x (and . xs) #f))) - (define-macro or () + (define-syntax-rules or () ((or) '#f) ((or x) x) ((or x . xs) (if x x (or . xs)))) - (define-macro cond (else) + (define-syntax-rules cond (else) ((cond (else e)) e) ((cond (test then) . rest) (if test then (cond . rest))))) @@ -1289,6 +1297,8 @@ (name (definition-name d)) (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*?) @@ -1397,7 +1407,7 @@ (size (cdr x))) 0)) -(define (check sys) +(define/guard (check (sys system?)) (let loop ((sys sys) (fails '())) (let ((defs (system-definitions sys))) @@ -1441,3 +1451,37 @@ (next (definition-name (car defs)))))))) (else (next)))))) + +(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)))) + ((theorem? def) + (pp + `(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)))) + ((primitive-function? def) + (pp + `(define-primitive-function + ,(primitive-function-name def) + ,(primitive-function-vars def)))) + ((macro? def) + (pp + `(define-syntax-rules ,(macro-name def)))) + (else + (error "show: error"))))) + (else + (format #t "~a: not found~%" name)))) |