summaryrefslogtreecommitdiff
path: root/vikalpa.scm
diff options
context:
space:
mode:
Diffstat (limited to 'vikalpa.scm')
-rw-r--r--vikalpa.scm1645
1 files changed, 1645 insertions, 0 deletions
diff --git a/vikalpa.scm b/vikalpa.scm
new file mode 100644
index 0000000..eadd2a0
--- /dev/null
+++ b/vikalpa.scm
@@ -0,0 +1,1645 @@
+;;; Vikalpa --- Proof Assistant
+;;; Copyright © 2020, 2021 Masaya Tojo <masaya@tojo.tokyo>
+;;;
+;;; This file is part of Vikalpa.
+;;;
+;;; Vikalpa is free software; you can redistribute it and/or modify it
+;;; under the terms of the GNU General Public License as published by
+;;; the Free Software Foundation; either version 3 of the License, or
+;;; (at your option) any later version.
+;;;
+;;; Vikalpa is distributed in the hope that it will be useful, but
+;;; WITHOUT ANY WARRANTY; without even the implied warranty of
+;;; MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the GNU
+;;; General Public License for more details.
+;;;
+;;; You should have received a copy of the GNU General Public License
+;;; along with Vikalpa. If not, see <http://www.gnu.org/licenses/>.
+
+(define-module (vikalpa)
+ #:export (system?
+ system-rewrite
+ system-check
+ system-apropos
+ system-eval
+ system-lookup
+ set-measure-predicate
+ set-measure-less-than
+ define-system
+ define-proof
+ define-core-function
+ define-core-function/guard
+ define-function
+ define-function
+ define-function/guard
+ define-axiom-function
+ define-axiom-function/guard
+ define-syntax-rules
+ define-axiom
+ define-theorem
+ define-guard-theorem
+ admit)
+ #:use-module (ice-9 match)
+ #:use-module (ice-9 format)
+ #:use-module (ice-9 control)
+ #:use-module (ice-9 exceptions)
+ #:use-module (ice-9 regex)
+ #:use-module ((srfi srfi-1)
+ #: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)
+ #:use-module (oop goops))
+
+(define-class <system> ()
+ (definitions
+ #:getter get-definitions
+ #:init-keyword #:definitions
+ #:init-value '())
+ (measure-predicate #:getter get-measure-predicate
+ #:init-value #f)
+ (measure-less-than #:getter get-measure-less-than
+ #:init-value #f))
+
+(define-class <definition> ()
+ (name #:getter get-name
+ #:init-keyword #:name)
+ (variables #:getter get-variables
+ #:init-keyword #:variables
+ #:init-value '()))
+
+(define-class <provable> ())
+
+(define-class <proved> (<provable>)
+ (claim #:getter get-claim #:init-keyword #:claim)
+ (proof #:getter get-proof #:init-keyword #:proof))
+
+(define-class <admitted> ())
+
+(define-class <theorem*> (<definition>)
+ (expression #:getter get-expression #:init-keyword #:expression))
+
+(define-class <conjecture> (<theorem*> <provable>))
+(define-class <theorem> (<theorem*> <proved>))
+(define-class <axiom> (<theorem*>))
+(define-class <admitted-theorem> (<theorem*> <proved> <admitted>))
+
+(define-class <function*> (<definition>)
+ (guards #:getter get-guards #:init-keyword #:guards))
+(define-class <core-function> (<function*>)
+ (procedure #:getter get-procedure #:init-keyword #:procedure))
+(define-class <expandable-function> (<function*>)
+ (expression #:getter get-expression #:init-keyword #:expression)
+ (code #:getter get-code #:init-keyword #:code))
+(define-class <function> (<expandable-function> <provable>))
+(define-class <total-function> (<expandable-function> <proved>))
+(define-class <admitted-function> (<expandable-function> <proved> <admitted>))
+
+(define-class <macro> (<definition>)
+ (mrules #:getter macro-mrules #:init-keyword #:mrules)
+ (literals #:getter macro-literals #:init-keyword #:literals))
+
+(define (write-definition sym d port)
+ (format port "#<~a: ~s>"
+ sym (cons (get-name d) (get-variables d))))
+
+(define-method (display (s <system>) port)
+ (format port "#<system: function: ~a theorem: ~a macro: ~a>"
+ (length (filter (cut is-a? <> <function*>)
+ (get-definitions s)))
+ (length (filter (cut is-a? <> <theorem*>)
+ (get-definitions s)))
+ (length (filter (cut is-a? <> <macro>)
+ (get-definitions s)))))
+
+(define-method (write (s <system>) port)
+ (format port "#<system: function: ~a theorem: ~a macro: ~a>"
+ (length (filter (cut is-a? <> <function*>)
+ (get-definitions s)))
+ (length (filter (cut is-a? <> <theorem*>)
+ (get-definitions s)))
+ (length (filter (cut is-a? <> <macro>)
+ (get-definitions s)))))
+
+(define-method (lookup name (s <system>))
+ (find (lambda (x)
+ (equal? name (get-name x)))
+ (get-definitions s)))
+
+(define-method (update-measure-predicate (s <symbol>) (sys <system>))
+ (let ((new (shallow-clone sys)))
+ (slot-set! new 'measure-predicate s)
+ new))
+
+(define-method (update-measure-less-than (s <symbol>) (sys <system>))
+ (let ((new (shallow-clone sys)))
+ (slot-set! new 'measure-less-than s)
+ new))
+
+(define-method (update-definition (d <definition>) (sys <system>))
+ (define (update d defs)
+ (if (null? defs)
+ (raise-exception
+ (make-exception
+ (make-exception-with-origin 'update-definition)
+ (make-exception-with-message "not found")
+ (make-exception-with-irritants (list d defs))))
+ (if (equal? (get-name d) (get-name (car defs)))
+ (cons d (cdr defs))
+ (cons (car defs) (update d (cdr defs))))))
+ (let ((new (shallow-clone sys)))
+ (slot-set! new 'definitions
+ (update d (get-definitions sys)))
+ new))
+
+(define-method (remove-first-definition (sys <system>))
+ (let ((new (shallow-clone sys)))
+ (slot-set! new 'definitions
+ (cdr (get-definitions sys)))
+ new))
+
+(define-method (first-definition (sys <system>))
+ (car (get-definitions sys)))
+
+(define-method (system-empty? (sys <system>))
+ (null? (get-definitions sys)))
+
+(define-method (add-definition (d <definition>) (s <system>))
+ (if (lookup (get-name d) s)
+ (raise-exception
+ (make-exception
+ (make-exception-with-origin 'add-definition)
+ (make-exception-with-message "duplicated definition")
+ (make-exception-with-irritants (get-name d))))
+ (if (reserved? (get-name d))
+ (raise-exception
+ (make-exception
+ (make-exception-with-origin 'add-definition)
+ (make-exception-with-message "reserved name")
+ (make-exception-with-irritants (get-name d))))
+ (let ((new (shallow-clone s)))
+ (slot-set! new 'definitions
+ (cons d (get-definitions s)))
+ new))))
+
+(define-method (validate (d <definition>))
+ (let* ((vars (get-variables d))
+ (name (get-name d)))
+ (validate-vars (format #f "~a" name) vars)))
+
+(define-method (validate (d <expandable-function>))
+ (let* ((vars (get-variables d))
+ (name (get-name d))
+ (expr (get-expression d)))
+ (validate-expression (current-system) name vars expr)
+ (next-method)))
+
+(define-method (validate (d <theorem*>))
+ (let* ((vars (get-variables d))
+ (name (get-name d))
+ (expr (get-expression d)))
+ (validate-expression (current-system) name vars expr)
+ (next-method)))
+
+(define-syntax-rule (define/guard (name (var p?) ...) b b* ...)
+ (define (name var ...)
+ (unless (p? var)
+ (error (format #f
+ "~a:~% expected: ~a~% given: "
+ 'name
+ 'p?)
+ var))
+ ...
+ b b* ...))
+
+(define (natural? x)
+ (and (exact-integer? x)
+ (not (negative? x))))
+
+(define (option p?)
+ (lambda (x)
+ (or (p? x) (not x))))
+
+(define (list-of p?)
+ (lambda (x)
+ (and (list? x)
+ (every p? x))))
+
+(define (expression? expr)
+ (cond ((expr-quoted? expr) #t)
+ ((if-form? expr)
+ (and (expression? (if-form-test expr))
+ (expression? (if-form-then expr))
+ (expression? (if-form-else expr))))
+ ((app-form? expr)
+ (and (symbol? (car expr))
+ (list? (cdr expr))
+ (every expression? (cdr expr))))
+ ((variable? expr) #t)
+ (else #f)))
+
+(define (app-form? expr)
+ (and (pair? expr)
+ (not (eq? (car expr) 'quote))
+ (not (eq? (car expr) 'if))))
+
+(define (app-form name args)
+ (cons name args))
+
+(define (app-form-name expr)
+ (car expr))
+
+(define (app-form-args expr)
+ (cdr expr))
+
+(define (if-form test then else)
+ (list 'if test then else))
+
+(define (if-form? x)
+ (and (pair? x)
+ (eq? (car x) 'if)))
+
+(define (if-form-test expr)
+ (list-ref expr 1))
+
+(define (if-form-then expr)
+ (list-ref expr 2))
+
+(define (if-form-else expr)
+ (list-ref expr 3))
+
+(define (expression-app-forms expr)
+ (cond
+ ((if-form? expr)
+ (append-map expression-app-forms
+ (list (if-form-test expr)
+ (if-form-then expr)
+ (if-form-else expr))))
+ ((app-form? expr)
+ (cons expr
+ (append-map expression-app-forms
+ (app-form-args expr))))
+ (else '())))
+
+(define (expression-functions expr)
+ (cond
+ ((if-form? expr)
+ (apply lset-union
+ eq?
+ (map expression-functions
+ (list (if-form-test expr)
+ (if-form-then expr)
+ (if-form-else expr)))))
+ ((app-form? expr)
+ (cons (app-form-name expr)
+ (apply lset-union
+ eq?
+ (map expression-functions (app-form-args expr)))))
+ (else '())))
+
+(define (expression-vars expr)
+ (cond
+ ((expr-quoted? expr) '())
+ ((if-form? expr)
+ (lset-union eq?
+ (expression-vars (if-form-test expr))
+ (expression-vars (if-form-then expr))
+ (expression-vars (if-form-else expr))))
+ ((app-form? expr)
+ (apply lset-union
+ eq?
+ (map expression-vars (app-form-args expr))))
+ ((variable? expr) (list expr))
+ (else '())))
+
+(define (expr-quoted? expr)
+ (and (pair? expr)
+ (eq? 'quote (car expr))
+ (pair? (cdr expr))
+ ((const #t) (car (cdr expr)))
+ (null? (cdr (cdr expr)))))
+
+(define (expr-unquote expr)
+ (car (cdr expr)))
+
+(define (expr-quote expr)
+ (list 'quote expr))
+
+(define (variable? x)
+ (symbol? x))
+
+(define (variable=? v1 v2)
+ (eq? v1 v2))
+
+(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)
+ (symbol? (car x))
+ (expression? (cdr x))))
+
+(define (env? x)
+ ((list-of binding?) x))
+
+(define/guard (substitute (env env?) (expr (const #t)))
+ (cond ((expr-quoted? expr) expr)
+ ((pair? expr)
+ (cons (substitute env (car expr))
+ (substitute env (cdr expr))))
+ ((assoc expr env) => cdr)
+ (else expr)))
+
+(define (match-rule preconds rl expr env)
+ (define (fail)
+ (shift k #f))
+ (define (var? v)
+ (and (member v (rule-vars rl))
+ #t))
+ (define (add-env var expr env)
+ (cond
+ ((assoc var env)
+ => (match-lambda
+ ((env-var . env-expr)
+ (if (equal? env-expr expr)
+ env
+ (fail)))))
+ (else
+ (cons (cons var expr)
+ env))))
+ (define (mat-fold lhss exprs env)
+ (cond ((and (pair? lhss) (pair? exprs))
+ (mat-fold (cdr lhss)
+ (cdr exprs)
+ (mat (car lhss)
+ (car exprs)
+ env)))
+ ((and (null? lhss) (null? exprs)) env)
+ (else (fail))))
+ (define (mat-begin lhs expr env)
+ (reset (mat lhs expr env)))
+ (define (mat lhs expr env)
+ (cond ((expr-quoted? lhs)
+ (if (expr-quoted? expr)
+ (if (equal? lhs expr)
+ env
+ (fail))
+ (fail)))
+ ((and (if-form? lhs)
+ (if-form? expr))
+ (mat-fold (list (if-form-test lhs)
+ (if-form-then lhs)
+ (if-form-else lhs))
+ (list (if-form-test expr)
+ (if-form-then expr)
+ (if-form-else expr))
+ env))
+ ((app-form? lhs)
+ (if (and (app-form? expr)
+ (symbol? (app-form-name lhs))
+ (eqv? (app-form-name lhs) (app-form-name expr)))
+ (mat-fold (app-form-args lhs) (app-form-args expr) env)
+ (fail)))
+ ((var? lhs) (add-env lhs expr env))
+ (else (fail))))
+ (define (mat-preconds rlps k+env)
+ (if (null? rlps)
+ k+env
+ (mat-preconds
+ (cdr rlps)
+ (let search ((ps preconds))
+ (if (null? ps)
+ (shift k ((car k+env) #f))
+ (let ((env (mat-begin (car rlps) (car ps) (cdr k+env))))
+ (cond
+ ((mat-begin (car rlps) (car ps) (cdr k+env))
+ => (lambda (env)
+ (shift k0
+ (reset
+ (or (shift k (k0 (cons k env)))
+ (k0 (search (cdr ps))))))))
+ (else (search (cdr ps))))))))))
+ (define (valid? env expr)
+ (cond ((expr-quoted? expr) #t)
+ ((pair? expr)
+ (and (valid? env (car expr))
+ (valid? env (cdr expr))))
+ ((var? expr)
+ (cond ((assoc expr env) => (const #t))
+ (else #f)))
+ (else #t)))
+ (reset
+ (shift k0
+ (match (mat-preconds (rule-preconds rl) (cons k0 env))
+ ((k . env)
+ (cond
+ ((mat-begin (rule-lhs rl) expr env)
+ => (lambda (env)
+ (if (valid? env (rule-rhs rl))
+ env
+ (k #f))))
+ (else (k #f))))
+ (else #f)))))
+
+(define (apply-rule preconds rl expr env)
+ (cond
+ ((match-rule preconds rl expr env)
+ => (cut substitute <> (rule-rhs rl)))
+ (else #f)))
+
+(define (code x)
+ (list 'code x))
+
+(define (code-expr x)
+ (cadr x))
+
+(define-class <mrule> ()
+ (lhs #:getter mrule-lhs #:init-keyword #:lhs)
+ (rhs #:getter mrule-rhs #:init-keyword #:rhs))
+
+(define (mrule lhs rhs)
+ (make <mrule> #:lhs lhs #:rhs rhs))
+
+(define (mrule-vars mrl)
+ (define (all-vars x)
+ (cond ((expr-quoted? x) '())
+ ((pair? x)
+ (append (all-vars (car x))
+ (all-vars (cdr x))))
+ ((variable? x) (list x))
+ (else '())))
+ (all-vars (mrule-lhs mrl)))
+
+(define (macro name mrules literals)
+ (make <macro>
+ #:name name
+ #:variables '()
+ #:mrules mrules
+ #:literals literals))
+
+(define (apply-mrule rl ls expr)
+ (define (literal? x)
+ (member x ls))
+ (define (var? v)
+ (and (member v (mrule-vars rl))
+ #t))
+ (call/cc
+ (lambda (k)
+ (define (mat-map lhs-tree expr-tree env)
+ (cond ((and (pair? lhs-tree)
+ (pair? expr-tree))
+ (mat-map (car lhs-tree)
+ (car expr-tree)
+ (mat-map (cdr lhs-tree)
+ (cdr expr-tree)
+ env)))
+ (else (mat lhs-tree expr-tree env))))
+ (define (mat lhs expr env)
+ (cond ((expr-quoted? lhs)
+ (if (expr-quoted? expr)
+ (if (equal? lhs expr)
+ env
+ (k #f))
+ (k #f)))
+ ((and (pair? lhs) (pair? expr))
+ (mat-map lhs expr env))
+ ((literal? lhs)
+ (if (eq? lhs expr)
+ env
+ (k #f)))
+ ((var? lhs)
+ (cond
+ ((assoc lhs env)
+ => (match-lambda
+ ((env-var . env-expr)
+ (if (equal? env-expr expr)
+ env
+ (k #f)))))
+ (else
+ (cons (cons lhs expr)
+ env))))
+ ((eqv? lhs expr) env)
+ (else (k #f))))
+ (define (mrule-substitute env expr)
+ (cond ((expr-quoted? expr) expr)
+ ((pair? expr)
+ (cons (mrule-substitute env (car expr))
+ (mrule-substitute env (cdr expr))))
+ ((literal? expr) expr)
+ ((and (variable? expr) (assoc expr env)) => cdr)
+ (else expr)))
+ (mrule-substitute (mat (mrule-lhs rl)
+ expr
+ '())
+ (mrule-rhs rl)))))
+
+(define (apply-macro m expr)
+ (cond ((and (pair? expr)
+ (eq? (get-name m) (car expr)))
+ (let loop ((rs (macro-mrules m)))
+ (cond ((null? rs)
+ (error "(vikalpa) macro fail" m expr))
+ ((apply-mrule (car rs) (macro-literals m) expr) => identity)
+ (else (loop (cdr rs))))))
+ (else #f)))
+
+(define (expand ms expr)
+ (let loop ((ms ms)
+ (expr expr))
+ (cond
+ ((null? ms) expr)
+ (else
+ (expand (cdr ms)
+ (cond
+ ((apply-macro (car ms) expr) => identity)
+ (else expr)))))))
+
+(define (expand* ms expr)
+ (let loop ((ms ms)
+ (expr expr))
+ (let ((new-expr (expand ms expr)))
+ (if (equal? expr new-expr)
+ (if (pair? new-expr)
+ (cons (expand* ms (car new-expr))
+ (expand* ms (cdr new-expr)))
+ new-expr)
+ (expand* ms new-expr)))))
+
+(define (quote-all x)
+ (cond
+ ((null? x) x)
+ ((expr-quoted? x) x)
+ ((pair? x)
+ (cons (quote-all (car x))
+ (quote-all (cdr x))))
+ ((symbol? x) x)
+ (else `',x)))
+
+(define (let? x)
+ (and (list? x)
+ (= 3 (length x))
+ (eq? 'let (list-ref x 0))
+ ((list-of (lambda (x)
+ (and (list? x)
+ (= 2 (length x))
+ (symbol? (car x)))))
+ (list-ref x 1))))
+
+(define (expand-let x)
+ (define (let-substitute env expr)
+ (cond ((expr-quoted? expr) expr)
+ ((let? expr)
+ (let-substitute
+ (append (map (lambda (binding)
+ (cons (car binding)
+ (let-substitute env
+ (cadr binding))))
+ (list-ref expr 1))
+ env)
+ (list-ref expr 2)))
+ ((pair? expr)
+ (cons (let-substitute env (car expr))
+ (let-substitute env (cdr expr))))
+ ((assoc expr env) => cdr)
+ (else expr)))
+ (cond
+ ((expr-quoted? x) x)
+ ((let? x)
+ (expand-let
+ (let-substitute (map (lambda (binding) (cons (car binding)
+ (cadr binding)))
+ (list-ref x 1))
+ (list-ref x 2))))
+ ((pair? x)
+ (cons (expand-let (car x))
+ (expand-let (cdr x))))
+ (else x)))
+
+(define (convert-to-expression x)
+ (quote-all
+ (expand* (filter (cut is-a? <> <macro>)
+ (get-definitions (current-system)))
+ (expand-let x))))
+
+(define (vars? x)
+ (and (list? x)
+ (every variable? x)))
+
+(define (theorem-rules x)
+ (expression->rules (get-variables x)
+ '()
+ (get-expression x)))
+
+(define (result? x)
+ (or (result/error? x)
+ (result/expr? x)))
+
+(define (result/error? x)
+ (and (pair? x)
+ (eq? 'result/error (car x))))
+
+(define (result/error . args)
+ (cons* 'result/error args))
+
+(define (result/expr? x)
+ (and (list? x)
+ (= 2 (length x))
+ (eq? 'result/expr (car x))
+ (expression? (cadr x))))
+
+(define (result/expr x)
+ (list 'result/expr x))
+
+(define/guard (result/expr-expr (x result/expr?))
+ (cadr x))
+
+(define (rewrite/eval expr sys)
+ (let eval ((result (result/expr expr)))
+ (cond
+ ((result/error? result) result)
+ ((result/expr? result)
+ (let ((expr (result/expr-expr result)))
+ (cond
+ ((expr-quoted? expr) (result/expr expr))
+ ((app-form? expr)
+ (let ((args/result (map (compose eval result/expr)
+ (app-form-args expr)))
+ (name (app-form-name expr)))
+ (cond
+ ((find error? args/result) => identity)
+ ((lookup name sys)
+ => (lambda (f)
+ (let ((args (map result/expr-expr args/result))
+ (gs (get-guards f))
+ (vars (get-variables f))
+ (form (defined-function-app-form f)))
+ (define (guard-ok? vars form g)
+ (let ((result (eval (apply-rule '()
+ (rule vars '() form g)
+ `(,name ,@args)
+ '()))))
+ (if (result/error? result)
+ result
+ (expr-unquote (result/expr-expr result)))))
+ (if (every (lambda (g) (guard-ok? vars form g)) gs)
+ (eval (rewrite1 sys
+ `(,name ,@args)
+ `(rewrite () ,name)))
+ (result/error 'guard-error `(,name ,@args) `(and ,@gs))))))
+ (else (result/error 'function-not-found name)))))
+ ((if-form? expr)
+ (let ((test/result (eval (result/expr (if-form-test expr)))))
+ (if (result/error? test/result)
+ test/result
+ (if (expr-unquote (result/expr-expr test/result))
+ (eval (result/expr (if-form-then expr)))
+ (eval (result/expr (if-form-else expr)))))))
+ ((variable? expr)
+ (result/error 'eval 'variable-found expr))
+ (else
+ (result/error 'eval 'invalid-expression expr)))))
+ (else (result/error 'eval 'invalid-result result)))))
+
+(define (rewriter? x)
+ (match x
+ (('rewrite path command-name command-ops ...)
+ (and (path? path)
+ (command-name? command-name)
+ (every command-option? command-ops)))
+ (('eval path) (path? path))
+ #;
+ (('induction path (fname vars ...))
+ (and (path? path)
+ (symbol? fname)
+ (every variable? vars)))
+ (else #f)))
+
+(define (sequence? x)
+ (and (list? x)
+ (every rewriter? x)))
+
+(define (path? x)
+ (and (list? x)
+ (every natural? x)))
+
+(define (command-name? x) #t)
+
+(define (command-option? x)
+ (and (pair? x)
+ (case (car x)
+ ((set) (and (list? x)
+ (= 3 (length x))
+ (variable? (list-ref x 1))
+ (expression? (list-ref x 2))))
+ (else #f))))
+
+(define (command-name x)
+ (car x))
+
+(define (command-options x)
+ (cdr x))
+
+(define/guard (system-eval (sys system?) (expr (const #t)))
+ (rewrite/eval (parameterize ((current-system sys))
+ (convert-to-expression expr))
+ sys))
+
+(define (extract path expr fail)
+ (if (null? path)
+ (values expr '() identity)
+ (let ((i (car path)))
+ (cond
+ ((if-form? expr)
+ (let ((precond (if-form-test expr)))
+ (receive (extracted-expr preconds builder)
+ (extract (cdr path) (list-ref expr i) fail)
+ (values extracted-expr
+ (case i
+ ((1) preconds)
+ ((2) (cons (prop-not (prop-not precond))
+ preconds))
+ ((3) (cons (prop-not precond) preconds))
+ (else (fail 'if-invaild-path path)))
+ (lambda (x)
+ (append (list-head expr i)
+ (list (builder x))
+ (list-tail expr (+ i 1))))))))
+ ((< i (length expr))
+ (receive (extracted-expr preconds builder)
+ (extract (cdr path) (list-ref expr i) fail)
+ (values extracted-expr
+ preconds
+ (lambda (x)
+ (append (list-head expr i)
+ (list (builder x))
+ (list-tail expr (+ i 1)))))))
+ (else
+ (fail 'invalid-path path))))))
+
+(define (function->rules x)
+ (list (rule (get-variables x)
+ (list)
+ (defined-function-app-form x)
+ (get-expression x))
+ (rule (get-variables x)
+ (list)
+ (get-expression x)
+ (defined-function-app-form x))))
+
+(define (apply-function f args)
+ (apply-rule '()
+ (rule (get-variables f)
+ '()
+ (defined-function-app-form f)
+ (get-expression f))
+ (app-form (get-name f) args)
+ '()))
+
+(define (parse-options/theorem ops fail)
+ (if (null? ops)
+ (values '())
+ (receive (env)
+ (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
+ (fail 'invalid-option (car ops)))))))
+
+(define (rewrite/theorem cmd-name cmd-ops b thm preconds expr)
+ (call/cc
+ (lambda (k)
+ (define (fail . args)
+ (k (apply result/error args)))
+ (receive (env)
+ (parse-options/theorem cmd-ops fail)
+ (cond
+ ((any (cut apply-rule preconds <> expr env)
+ (theorem-rules thm)) => result/expr)
+ (else
+ (result/error 'apply-theorem cmd-name expr)))))))
+
+(define (rewrite/core-function sys f expr)
+ (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)))
+ (result/expr
+ (expr-quote (apply (get-procedure f)
+ (map expr-unquote (app-form-args expr)))))
+ (result/error 'apply-core-function (get-name f) expr)))
+
+(define (rewrite/function sys fname f expr)
+ (cond
+ ((any (cut apply-rule '() <> expr '())
+ (function->rules f))
+ => result/expr)
+ (else
+ (result/error 'apply-function fname expr))))
+
+(define (rewrite1 sys expr r)
+ (call/cc
+ (lambda (k)
+ (define (fail . args)
+ (k (apply result/error args)))
+ (define (result->expr x)
+ (cond
+ ((result/error? x) (fail (cdr x)))
+ (else
+ (result/expr-expr x))))
+ (match r
+ (('eval path)
+ (receive (extracted-expr preconds builder)
+ (extract path expr fail)
+ (result/expr
+ (builder
+ (result->expr (rewrite/eval extracted-expr sys))))))
+ #;
+ (('induction path (fname vars ...))
+ (receive (extracted-expr preconds builder)
+ (extract path expr fail)
+ (result/expr
+ (builder
+ (result->expr
+ (rewrite/induction sys fname vars preconds extracted-expr))))))
+ (('rewrite path cmd-name cmd-ops ...)
+ (receive (extracted-expr preconds builder)
+ (extract path expr fail)
+ (result/expr
+ (builder
+ (result->expr
+ (cond
+ ((lookup cmd-name sys)
+ => (lambda (x)
+ (cond
+ ((is-a? x <core-function>)
+ (rewrite/core-function sys x extracted-expr))
+ ((is-a? x <theorem*>)
+ (rewrite/theorem cmd-name cmd-ops sys x preconds extracted-expr))
+ ((is-a? x <expandable-function>)
+ (rewrite/function sys cmd-name x extracted-expr))
+ (else
+ (result/error 'invalid-command cmd-name extracted-expr)))))
+ (else (result/error 'command-not-found cmd-name extracted-expr))))))))))))
+
+(define (rewrite sys expr seq)
+ (let loop ((result (result/expr expr))
+ (seq seq))
+ (cond
+ ((result/error? result) result)
+ ((result/expr? result)
+ (if (null? seq)
+ result
+ (loop (rewrite1 sys
+ (result/expr-expr result)
+ (car seq))
+ (cdr seq))))
+ (else (result/error 'invalid-result result)))))
+
+(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))
+ (eq? 'equal? (list-ref x 0))
+ (expression? (list-ref x 1))
+ (expression? (list-ref x 2))))
+
+(define (expr-equal-lhs x)
+ (list-ref x 1))
+
+(define (expr-equal-rhs x)
+ (list-ref x 2))
+
+(define (expression->rules vars preconds expr)
+ (if (if-form? expr)
+ (append (expression->rules vars
+ (cons (prop-not
+ (prop-not
+ (if-form-test expr)))
+ preconds)
+ (if-form-then expr))
+ (expression->rules vars
+ (cons (prop-not (if-form-test expr))
+ preconds)
+ (if-form-else expr))
+ (expression->rules vars
+ preconds
+ (if-form-test expr)))
+ (if (expr-equal? expr)
+ (list (rule vars
+ preconds
+ (expr-equal-lhs expr)
+ (expr-equal-rhs expr))
+ (rule vars
+ preconds
+ (expr-equal-rhs expr)
+ (expr-equal-lhs expr)))
+ '())))
+
+(define (theorem->rules def)
+ (expression->rules (get-variables def)
+ '()
+ (get-expression def)))
+
+(define current-system (make-parameter (make <system>)))
+(define reserved-symbols '(quote let if error))
+(define (reserved? x)
+ (member x reserved-symbols))
+
+(define-syntax define-axiom
+ (syntax-rules ()
+ ((_ name (var ...) expr)
+ (let ((t (make <axiom>
+ #:name 'name
+ #:variables '(var ...)
+ #:expression (convert-to-expression 'expr))))
+ (current-system (add-definition t (current-system)))
+ (validate t)
+ t))))
+
+(define-syntax define-theorem
+ (syntax-rules ()
+ ((_ name (var ...) expr)
+ (match 'name
+ (`(guard . ,_)
+ (raise-exception (make-exception
+ (make-exception-with-origin "define-theorem")
+ (make-exception-with-message "invalid theorem name (guard _ ...)")
+ (make-exception-with-irritants 'name))))
+ (else
+ (let ((t (make <conjecture>
+ #:name 'name
+ #:variables '(var ...)
+ #:expression (convert-to-expression 'expr))))
+ (current-system (add-definition t (current-system)))
+ (validate t)
+ t))))))
+
+(define (add-guard-theorem name sys)
+ (cond
+ ((lookup name sys)
+ => (lambda (f)
+ (if (is-a? f <expandable-function>)
+ (add-definition (make <conjecture>
+ #:name `(guard ,name)
+ #:variables (get-variables f)
+ #:expression (fold smart-implies
+ (make-guard-claim
+ (get-expression f)
+ sys)
+ (get-guards f)))
+ sys)
+ (raise-exception
+ (make-exception
+ (make-exception-with-origin 'define-guard-theorem)
+ (make-exception-with-message "not expandable function")
+ (make-exception-with-irritants name))))))
+ (else
+ (raise-exception
+ (make-exception
+ (make-exception-with-origin 'define-guard-theorem)
+ (make-exception-with-message "not found")
+ (make-exception-with-irritants name))))))
+
+(define-syntax define-guard-theorem
+ (syntax-rules ()
+ ((_ name)
+ (current-system (add-guard-theorem 'name (current-system))))))
+
+(define-syntax define-core-function/guard
+ (syntax-rules (and)
+ ((_ name (var ...) (and guard ...) proc)
+ (let ((f (make <core-function>
+ #:name 'name
+ #:variables '(var ...)
+ #:guards (map convert-to-expression (list 'guard ...))
+ #:procedure proc)))
+ (current-system (add-definition f (current-system)))
+ (validate f)
+ f))
+ ((_ name (var ...) guard proc)
+ (define-core-function/guard name (var ...) (and guard) proc))))
+
+(define-syntax define-core-function
+ (syntax-rules ()
+ ((_ name (var ...) proc)
+ (define-core-function/guard name (var ...) (and) proc))))
+
+(define (recursive? f)
+ (member (get-name f) (expression-functions (get-expression f))))
+
+(define-syntax define-function/guard
+ (syntax-rules (and)
+ ((_ name (var ...) (and guard-expr ...) expr)
+ (let* ((expression (convert-to-expression 'expr))
+ (guard-expressions (map convert-to-expression
+ (list 'guard-expr ...)))
+ (f (make <function>
+ #:name 'name
+ #:variables '(var ...)
+ #:guards guard-expressions
+ #:expression expression
+ #:code (code 'expr))))
+ (current-system (add-definition f (current-system)))
+ (validate f)
+ (when (not (recursive? f))
+ (let ((g (make <total-function>
+ #:name (get-name f)
+ #:variables (get-variables f)
+ #:guards (get-guards f)
+ #:expression (get-expression f)
+ #:code (get-code f)
+ #:claim ''#t
+ #:proof '())))
+ (current-system (update-definition g (current-system)))
+ (validate g)))
+ ))
+ ((_ name (var ...) guard expr)
+ (define-function/guard name (var ...) (and guard) expr))))
+
+(define-syntax define-function
+ (syntax-rules ()
+ ((_ name (var ...) expr)
+ (define-function/guard name (var ...) (and) expr))))
+
+(define-syntax define-syntax-rules
+ (syntax-rules ()
+ ((_ name (l ...) ((lhs1 . lhs2) rhs) ...)
+ (let ((m (macro 'name
+ (list (mrule '(lhs1 . lhs2) 'rhs)
+ ...)
+ '(l ...))))
+ (current-system (add-definition m (current-system)))
+ m))))
+
+(define-syntax admit
+ (syntax-rules (and)
+ ((_ name)
+ (cond
+ ((lookup 'name (current-system))
+ => (lambda (d)
+ (unless (or (is-a? d <conjecture>)
+ (is-a? d <function>))
+ (raise-exception
+ (make-exception
+ (make-exception-with-origin 'name)
+ (make-exception-with-message "not provable definition")
+ (make-exception-with-irritants 'name))))
+ (let ((g (if (is-a? d <conjecture>)
+ (make <admitted-theorem>
+ #:name (get-name d)
+ #:variables (get-variables d)
+ #:expression (get-expression d)
+ #:claim ''#t
+ #:proof '())
+ (make <admitted-function>
+ #:name (get-name d)
+ #:variables (get-variables d)
+ #:guards (get-guards d)
+ #:expression (get-expression d)
+ #:code (get-code d)
+ #:claim ''#t
+ #:proof '()))))
+ (validate g)
+ (current-system (update-definition g (current-system))))))
+ (else
+ (raise-exception
+ (make-exception
+ (make-exception-with-origin 'name)
+ (make-exception-with-message "not found")
+ (make-exception-with-irritants 'name))))))))
+
+(define* (core-system #:optional (parent (make <system>)))
+ (parameterize ((current-system parent))
+ (define-syntax-rules and ()
+ ((and) '#t)
+ ((and x) x)
+ ((and x . xs) (if x (and . xs) #f)))
+ (define-core-function not (x) not)
+ (define-core-function equal? (x y) equal?)
+ (current-system)))
+
+(define-syntax define-system
+ (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
+ ...
+ (current-system))))))
+
+(define (validate-function-name desc name)
+ (define (err)
+ (raise-exception
+ (make-exception
+ (make-exception-with-origin 'desc)
+ (make-exception-with-message "unbound function")
+ (make-exception-with-irritants name))))
+ (cond
+ ((lookup name (current-system))
+ => (lambda (f)
+ (if (is-a? f <function*>)
+ name
+ (err))))
+ (else (err))))
+
+(define-syntax set-measure-predicate
+ (syntax-rules ()
+ ((_ name)
+ (begin
+ (validate-function-name 'set-measure-predicate 'name)
+ (current-system (update-measure-predicate 'name (current-system)))))))
+
+(define-syntax set-measure-less-than
+ (syntax-rules ()
+ ((_ name)
+ (begin
+ (validate-function-name 'set-measure-less-than 'name)
+ (current-system
+ (update-measure-less-than 'name (current-system)))))))
+
+(define (defined-function-app-form f)
+ (app-form (get-name f) (get-variables f)))
+
+(define (single? x)
+ (and (pair? x)
+ (null? (cdr x))))
+
+(define (smart-if x y z)
+ (cond
+ ((equal? y z) y)
+ ((equal? x ''#t) y)
+ ((equal? x ''#f) z)
+ (else `(if ,x ,y ,z))))
+
+(define (smart-and . args)
+ (cond
+ ((null? args) ''#t)
+ ((equal? ''#t (car args)) (apply smart-and (cdr args)))
+ (else
+ (let ((rest (apply smart-and (cdr args))))
+ (if (equal? ''#t rest)
+ (car args)
+ (smart-if (car args)
+ rest
+ ''#f))))))
+
+(define (smart-implies x y)
+ (cond
+ ((equal? ''#f x) ''#t)
+ ((equal? ''#t y) ''#t)
+ (else
+ (smart-if x y ''#t))))
+
+(define (make-totality-claim* sys m-expr f)
+ (let* ((name (get-name f)))
+ (define (convert app-form)
+ (cond
+ ((apply-rule '()
+ (rule (get-variables f)
+ '()
+ (defined-function-app-form f)
+ m-expr)
+ app-form
+ '())
+ => identity)
+ (else (error "make-totality-claim: convert error"
+ (get-name f)
+ m-expr
+ app-form))))
+ (smart-if `(,(get-measure-predicate sys) ,m-expr)
+ (let loop ((expr (get-expression f)))
+ (cond
+ ((expr-quoted? expr) ''#t)
+ ((variable? expr) ''#t)
+ ((if-form? expr)
+ (let ((test/result (loop (if-form-test expr)))
+ (then/result (loop (if-form-then expr)))
+ (else/result (loop (if-form-else expr))))
+ (smart-and test/result
+ (smart-if (if-form-test expr)
+ then/result
+ else/result))))
+ ((app-form? expr)
+ (let ((rest
+ (let f ((args (app-form-args expr)))
+ (cond ((null? args) ''#t)
+ ((single? args) (loop (car args)))
+ (else (smart-and (loop (car args))
+ (f (cdr args))))))))
+ (if (eq? name (app-form-name expr))
+ (smart-and `(,(get-measure-less-than sys)
+ ,(convert expr)
+ ,m-expr)
+ rest)
+ rest)))
+ (else (error "(vikalpa) make-totality-claim: error"
+ (get-name f)
+ m-expr))))
+ ''#f)))
+
+(define (make-guard-claim expr sys)
+ (define (find-preconds expr)
+ (cond
+ ((app-form? expr)
+ (let ((rest (append-map find-preconds (cdr expr))))
+ (append (cond ((lookup (car expr) sys) =>
+ (lambda (f)
+ (let ((preconds (get-guards f)))
+ (map (lambda (precond)
+ (substitute (map cons
+ (get-variables f)
+ (cdr expr))
+ precond))
+ preconds))))
+ (else (error "make-guard-claim: error" (car expr))))
+ rest)))
+ ((if-form? expr)
+ (find-preconds (if-form-test expr)))
+ (else '())))
+ (define (build/find-if expr)
+ (cond
+ ((if-form? expr)
+ (smart-if (build/find-if (if-form-test expr))
+ (build (if-form-then expr))
+ (build (if-form-else expr))))
+ ((app-form? expr)
+ (apply smart-and (map build/find-if (app-form-args expr))))
+ (else ''#t)))
+ (define (build expr)
+ (cond
+ ((if-form? expr)
+ (apply smart-and
+ (append (find-preconds (if-form-test expr))
+ (list (smart-if (if-form-test expr)
+ (build (if-form-then expr))
+ (build (if-form-else expr)))))))
+ ((app-form? expr)
+ (apply smart-and
+ (append (find-preconds expr)
+ (list (build/find-if expr)))))
+ (else ''#t)))
+ (build expr))
+
+(define (make-induction-claim f vars c)
+ (unless (is-a? f <expandable-function>)
+ (raise-exception
+ (make-exception
+ (make-exception-with-origin 'define-proof)
+ (make-exception-with-message
+ "measure function must be expandable function")
+ (make-exception-with-irritants (get-name f)))))
+ (define (find-app-forms expr)
+ (cond
+ ((app-form? expr)
+ (let ((rest (append-map find-app-forms (cdr expr))))
+ (if (eq? (get-name f) (app-form-name expr))
+ (cons expr rest)
+ rest)))
+ ((if-form? expr)
+ (error "make-induction-claim(find-app-forms): not supported"
+ expr))
+ (else '())))
+ (define (prop form)
+ (cond
+ ((apply-rule '()
+ (rule vars
+ '()
+ (app-form (get-name f) vars)
+ c)
+ form
+ '())
+ => identity)
+ (else
+ (error "make-induction-claim: fail" app-form))))
+ (cond
+ ((apply-function f vars)
+ => (lambda (expr)
+ (let build ((expr expr))
+ (cond
+ ((if-form? expr)
+ (let ((app-forms (find-app-forms (if-form-test expr))))
+ (smart-implies (if (null? app-forms)
+ ''#t
+ (fold smart-implies
+ c
+ (map prop app-forms)))
+ (smart-if (if-form-test expr)
+ (build (if-form-then expr))
+ (build (if-form-else expr))))))
+ (else
+ (let ((app-forms (find-app-forms expr)))
+ (fold smart-implies c (map prop app-forms))))))))
+ (else (error "make-induction-claim: invalid"
+ f vars c))))
+
+(define (validate-sequence sys d seq)
+ (for-each (lambda (r)
+ (match r
+ (('rewrite _ _ . command-ops)
+ (for-each (lambda (x)
+ (match x
+ (('set var expr)
+ (validate-expression sys
+ `(define-proof ,(get-name d))
+ (get-variables d)
+ expr))
+ (else #f)))
+ command-ops))
+ (else #f)))
+ seq))
+
+(define (add-proof/function sys f seed seq)
+ (define (update-claim claim)
+ (update-definition (make <total-function>
+ #:name (get-name f)
+ #:variables (get-variables f)
+ #:guards (get-guards f)
+ #:expression (get-expression f)
+ #:code (get-code f)
+ #:claim claim
+ #:proof seq)
+ sys))
+ (validate-sequence sys f seq)
+ (if seed
+ (begin
+ (validate-expression sys
+ `(defien-proof ,(get-name f))
+ (get-variables f)
+ seed)
+ (update-claim
+ (fold smart-implies
+ (make-totality-claim* sys seed f)
+ (get-guards f))))
+ (raise-exception
+ (make-exception
+ (make-exception-with-origin 'define-proof)
+ (make-exception-with-message "need measure expression")
+ (make-exception-with-irritants (get-expression f))))))
+
+(define (add-proof/theorem sys t seed seq)
+ (define (seed-error m)
+ (raise-exception
+ (make-exception
+ (make-exception-with-origin 'define-proof)
+ (make-exception-with-message (string-append "invalid seed: " m))
+ (make-exception-with-irritants (list (get-name t) seed)))))
+ (validate-sequence sys t seq)
+ (let ((claim
+ (if seed
+ (match seed
+ ((fname vars ...)
+ (cond
+ ((lookup fname sys)
+ => (cut make-induction-claim <> vars (get-expression t)))
+ (else (seed-error "function not found"))))
+ (else (seed-error "format error")))
+ (get-expression t))))
+ (update-definition (make <theorem>
+ #:name (get-name t)
+ #:variables (get-variables t)
+ #:expression (get-expression t)
+ #:claim claim
+ #:proof seq)
+ sys)))
+
+(define (add-proof sys name seed seq)
+ (cond
+ ((not (sequence? seq))
+ (raise-exception
+ (make-exception
+ (make-exception-with-origin 'define-proof)
+ (make-exception-with-message "not sequence")
+ (make-exception-with-irritants seq))))
+ ((lookup name sys)
+ => (lambda (def)
+ (current-system
+ (if (and (is-a? def <provable>)
+ (not (is-a? def <proved>)))
+ (cond
+ ((is-a? def <function>)
+ (add-proof/function sys def seed seq))
+ ((is-a? def <conjecture>)
+ (add-proof/theorem sys def seed seq))
+ (else
+ (raise-exception
+ (make-exception
+ (make-exception-with-origin 'define-proof)
+ (make-exception-with-message "error")
+ (make-exception-with-irritants def)))))
+ (raise-exception
+ (make-exception
+ (make-exception-with-origin 'define-proof)
+ (make-exception-with-message "not provable definition")
+ (make-exception-with-irritants def)))))))
+ (else
+ (raise-exception
+ (make-exception
+ (make-exception-with-origin 'define-proof)
+ (make-exception-with-message "definition is not found")
+ (make-exception-with-irritants name))))))
+
+(define-syntax define-proof
+ (syntax-rules ()
+ ((_ name
+ seed
+ seq)
+ (add-proof (current-system)
+ 'name
+ 'seed
+ 'seq))
+ ((_ name seq)
+ (define-proof name #f seq))))
+
+(define (validate-expression/error sys name vars expr)
+ (with-exception-handler
+ (lambda (e)
+ (if (eq? 'validate-expression/error (exception-origin e))
+ `(error ,name ,vars ,expr))
+ (raise-exception e))
+ (lambda ()
+ (validate-expression sys 'validate-expression/error vars expr)
+ #f)))
+
+(define (validate-expression sys name vars expr)
+ (let* ((expr-fnames (expression-functions expr))
+ (expr-vars (expression-vars expr))
+ (expr-app-forms (expression-app-forms expr)))
+ (define (err msg x)
+ (raise-exception
+ (make-exception
+ (make-exception-with-origin name)
+ (make-exception-with-message msg)
+ (make-exception-with-irritants x))))
+ (for-each (lambda (x)
+ (when (member x expr-fnames)
+ (err "invalid variable" x)))
+ vars)
+ (for-each (lambda (fname)
+ (unless (cond
+ ((lookup fname sys) =>
+ (lambda (f)
+ (for-each
+ (lambda (app-form)
+ (when (equal? fname (app-form-name app-form))
+ (unless (= (length (get-variables f))
+ (length (app-form-args app-form)))
+ (err (format
+ #f
+ "~a :wrong number of arguments ~s"
+ (get-name f)
+ (get-variables f))
+ (app-form-args app-form)))))
+ expr-app-forms)
+ #t))
+ (else #f))
+ (err "undefined function" fname)))
+ expr-fnames)
+ (for-each (lambda (x)
+ (unless (member x vars)
+ (err "undefined variable" x)))
+ expr-vars)))
+
+(define (dup? xs)
+ (if (null? xs)
+ #f
+ (if (member (car xs) (cdr xs))
+ #t
+ (dup? (cdr xs)))))
+
+(define (validate-vars desc vars)
+ (define (err)
+ (raise-exception
+ (make-exception
+ (make-exception-with-message
+ (string-append "(vikalpa) " desc ": duplicated variable"))
+ (make-exception-with-irritants vars))))
+ (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 <admitted-function>)) 'admitted-function)
+(define-method (get-type (s <admitted-theorem>)) 'admitted-theorem)
+(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-method (show (d <admitted-function>))
+ (list (get-type d)
+ (get-variables d)
+ (get-expression d)))
+
+(define* (system-apropos sys str)
+ (filter-map (lambda (d)
+ (let ((name (format #f "~a" (get-name d))))
+ (if (string-match (string-append ".*"
+ (regexp-quote str)
+ ".*")
+ name)
+ (list (get-name d) (show d))
+ #f)))
+ (get-definitions sys)))
+
+(define (system-check/guard sys)
+ (filter-map (lambda (f)
+ (if (lookup `(guard ,(get-name f)) sys)
+ #f
+ (if (equal? (make-guard-claim (get-expression f) sys)
+ ''#t)
+ #f
+ `((guard ,(get-name f))
+ (add (define-guard-theorem ,(get-name f)))))))
+ (filter (cut is-a? <> <expandable-function>)
+ (get-definitions sys))))
+
+(define (system-check sys)
+ (append
+ (system-check/guard sys)
+ (let loop ((sys sys)
+ (fails '()))
+ (if (system-empty? sys)
+ fails
+ (let ((d (first-definition sys))
+ (sys-without-first (remove-first-definition sys)))
+ (define* (next #:optional fail)
+ (loop sys-without-first
+ (if fail
+ (cons fail fails)
+ fails)))
+ (cond
+ ((is-a? d <proved>)
+ (let ((result
+ (if (is-a? d <theorem>)
+ (rewrite sys-without-first
+ (get-claim d)
+ (get-proof d))
+ (rewrite sys
+ (get-claim d)
+ (get-proof d)))))
+ (cond
+ ((equal? result (result/expr ''#t))
+ (next))
+ (else
+ (next (list (get-name d) result))))))
+ ((is-a? d <provable>)
+ (next (list (get-name d))))
+ (else (next))))))))
+
+(define (system? x)
+ (is-a? x <system>))
+
+(define/guard (system-lookup (sys system?) (name (const #t)))
+ (cond
+ ((lookup name sys) => show)
+ (else #f)))
+
+(define/guard (system-rewrite (sys system?) (expr (const #t)) (seq sequence?))
+ (rewrite sys (convert-to-expression expr) seq))