diff options
| -rw-r--r-- | vikalpa.scm | 1645 |
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)) |