diff options
Diffstat (limited to 'vikalpa.scm')
| -rw-r--r-- | vikalpa.scm | 242 |
1 files changed, 138 insertions, 104 deletions
diff --git a/vikalpa.scm b/vikalpa.scm index ab87b7d..40b4bf1 100644 --- a/vikalpa.scm +++ b/vikalpa.scm @@ -17,19 +17,23 @@ ;;; along with Vikalpa. If not, see <http://www.gnu.org/licenses/>. (define-module (vikalpa) - #:export (rewrite - describe - system? + #:export (system? + system-rewrite system-check system-apropos system-code system-load + system-eval + system-lookup set-measure-predicate set-measure-less-than define-system define-proof define-core-function define-function + define-trivial-total-function + define-syntax-rules + define-axiom define-theorem) #:use-module (ice-9 match) #:use-module (ice-9 format) @@ -37,7 +41,8 @@ #:use-module (ice-9 exceptions) #:use-module (ice-9 regex) #:use-module ((srfi srfi-1) - #:select (every any lset-union fold append-map find)) + #:select (every any lset-union fold append-map find + filter-map)) #:use-module (srfi srfi-8) #:use-module (srfi srfi-11) #:use-module (srfi srfi-26) @@ -216,28 +221,6 @@ ... b b* ...)) -(define-syntax define-type - (syntax-rules () - ((_ name - constractor - (m p?) - (n t? getter-var getter) ...) - (begin - (define (constractor getter-var ...) - (let ((data (make-list (+ 1 (length (list t? ...)))))) - (list-set! data m 'name) - (list-set! data n getter-var) - ... - data)) - (define (p? x) - (and (list? x) - (= (+ 1 (length (list t? ...))) (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) @@ -367,25 +350,21 @@ (define (variable=? v1 v2) (eq? v1 v2)) -(define-type rule - rule - (0 rule?) - (1 (lambda (vars) - (and (list? vars) - (every variable? vars))) - vars - rule-vars) - (2 (lambda (ps) - (and (list? ps) - (every expression? ps))) - ps - rule-preconds) - (3 expression? - lhs - rule-lhs) - (4 expression? - rhs - rule-rhs)) +(define-class <rule> () + (vars #:getter rule-vars #:init-keyword #:vars) + (preconds #:getter rule-preconds #:init-keyword #:preconds) + (lhs #:getter rule-lhs #:init-keyword #:lhs) + (rhs #:getter rule-rhs #:init-keyword #:rhs)) + +(define (rule var preconds lhs rhs) + (make <rule> + #:vars var + #:preconds preconds + #:lhs lhs + #:rhs rhs)) + +(define (rule? x) + (is-a? x <rule>)) (define (binding? x) (and (pair? x) @@ -689,19 +668,26 @@ '() (get-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))))))) + (cond + ((find error? args) => identity) + (else + (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) @@ -709,6 +695,8 @@ (if (expr-unquote test) (eval (if-form-then expr)) (eval (if-form-else expr)))))) + ((variable? expr) + `(error eval variable-found ,expr)) (else `(error eval invalid-expression ,expr))))) @@ -765,7 +753,7 @@ (define (command-options x) (cdr x)) -(define/guard (system-eval (expr (const #t)) (sys (cut is-a? <> <system>))) +(define/guard (system-eval (sys system?) (expr (const #t))) (rewrite/eval (parameterize ((current-system sys)) (convert-to-expression expr)) sys)) @@ -851,6 +839,16 @@ => (cut make-induction-claim <> vars expr)) (else (fail 'induction 'not-found fname)))) +(define (rewrite/core-function sys f expr fail) + (if (and (app-form? expr) + (eq? (get-name f) (app-form-name expr)) + (= (length (get-variables f)) (length (app-form-args expr))) + (every expr-quoted? (app-form-args expr))) + (let ((result (apply (get-procedure f) + (map expr-unquote (app-form-args expr))))) + (expr-quote result)) + (fail 'apply-core-function (get-name f) expr))) + (define (rewrite1 sys expr fail r) (let* ((cmd (rewriter-command r)) (cmd/name (command-name cmd))) @@ -860,11 +858,16 @@ (builder (cond ((equal? '(eval) cmd/name) - (rewrite/eval extracted-expr sys)) + (let ((result (rewrite/eval extracted-expr sys))) + (if (error? result) + (fail 'eval (cddr result) extracted-expr) + result))) ((and (symbol? cmd/name) (lookup cmd/name sys)) => (lambda (x) (cond + ((is-a? x <core-function>) + (rewrite/core-function sys x extracted-expr fail)) ((is-a? x <theorem*>) (rewrite/theorem cmd sys x preconds extracted-expr fail)) ((is-a? x <expandable-function>) @@ -878,19 +881,18 @@ (fail 'invalid-command cmd extracted-expr))))) (else (fail 'command-not-found cmd extracted-expr))))))) -(define/guard (rewrite (sys (cut is-a? <> <system>)) (expr (const #t)) (seq (const #t))) - (let ((expr (convert-to-expression expr))) - (let loop ((expr expr) - (seq seq)) - (reset - (if (null? seq) - expr - (loop (rewrite1 sys - expr - (lambda args - (shift k (cons 'error args))) - (car seq)) - (cdr seq))))))) +(define (rewrite sys expr seq) + (let loop ((expr expr) + (seq 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)) @@ -974,11 +976,11 @@ (define-syntax define-core-function (syntax-rules () - ((_ name (var ...) precond ... proc) + ((_ name (var ...) proc) (let ((f (make <core-function> #:name 'name #:variables '(var ...) - #:conditions '(precond ...) + #:conditions '() #:procedure proc))) (current-system (add-definition f (current-system))) (validate f) @@ -1033,6 +1035,12 @@ (syntax-rules () ((_ name (systems ...) expr ...) (define* (name #:optional (parent (core-system))) + (when (member 'name (list 'systems ...)) + (raise-exception + (make-exception + (make-exception-with-origin 'name) + (make-exception-with-message "recursive system") + (make-exception-with-irritants '(systems ...))))) (parameterize ((current-system ((compose systems ... identity) parent))) expr @@ -1432,24 +1440,59 @@ (when (dup? vars) (err))) +(define-method (get-type (s <axiom>)) 'axiom) +(define-method (get-type (s <theorem>)) 'theorem) +(define-method (get-type (s <conjecture>)) 'conjecture) +(define-method (get-type (s <core-function>)) 'core-function) +(define-method (get-type (s <function>)) 'function) +(define-method (get-type (s <total-function>)) 'total-function) +(define-method (get-type (s <trivial-total-function>)) 'trivial-total-function) +(define-method (get-type (s <macro>)) 'macro) + +(define-method (show (d <macro>)) + (list (get-type d))) +(define-method (show (d <theorem*>)) + (list (get-type d) + (get-variables d) + (get-expression d))) +(define-method (show (d <core-function>)) + (list (get-type d) + (get-variables d))) +(define-method (show (d <expandable-function>)) + (list (get-type d) + (get-variables d) + (get-expression d))) (define/guard (system-apropos (sys system?) (str string?)) - (filter (lambda (name) - (string-match (string-append ".*" - (regexp-quote str) - ".*") - (symbol->string name))) - (map get-name (get-definitions sys)))) - -(define/guard (system-code (sys system?)) + (filter-map (lambda (d) + (if (string-match (string-append ".*" + (regexp-quote str) + ".*") + (symbol->string (get-name d))) + (list (get-name d) (show d)) + #f)) + (get-definitions sys))) + +(define (system-code/definition d) + (and (is-a? d <expandable-function>) + (get-code d) + `(define (,(get-name d) ,@(get-variables d)) + ,(code-expr (get-code d))))) + +(define/guard (system-code/name (sys system?) (name symbol?)) + (cond + ((lookup name sys) => system-code/definition) + (else #f))) + +(define/guard (system-code/all (sys system?)) `(begin - ,@(map (lambda (f) - `(define (,(get-name f) ,@(get-variables f)) - ,(code-expr (get-code f)))) - (reverse (filter (lambda (x) - (and (is-a? x <expandable-function>) - (get-code x))) - (get-definitions sys)))))) + ,@(filter-map system-code/definition + (reverse (get-definitions sys))))) + +(define* (system-code sys #:optional (name #f)) + (if name + (system-code/name sys name) + (system-code/all sys))) (define (system-check sys) (let loop ((sys sys) @@ -1485,28 +1528,19 @@ (define (system? x) (is-a? x <system>)) -(define/guard (describe (sys system?) (name symbol?)) +(define/guard (system-lookup (sys system?) (name symbol?)) (cond - ((lookup name sys) - => (lambda (def) - (cond - ((is-a? def <core-function>) - `(define-core-function ,(get-name def) ,(get-variables def))) - ((is-a? def <expandable-function>) - `(define-function ,(get-name def) ,(get-variables def) - ,(get-expression def))) - ((is-a? def <axiom>) - `(define-axiom ,(get-name def) ,(get-variables def) - ,(get-expression def))) - ((is-a? def <theorem*>) - `(define-theorem ,(get-name def) ,(get-variables def) - ,(get-expression def))) - (((cut is-a? <> <macro>) def) - `(define-syntax-rules ,(get-name def))) - (else - `(error 'fatal-error ,name))))) - (else - `(error 'not-found ,name)))) + ((lookup name sys) => show) + (else #f))) + +(define/guard (system-load/name (sys system?) (name symbol?)) + (primitive-eval (system-code sys name))) + +(define/guard (system-load/all (sys system?)) + (primitive-eval (system-code sys))) (define/guard (system-load (sys system?)) (primitive-eval (system-code sys))) + +(define/guard (system-rewrite (sys system?) (expr (const #t)) (seq sequence?)) + (rewrite sys (convert-to-expression expr) seq)) |