From 616391177e0dbdaff8be7fb73d4ce14f9e97eb70 Mon Sep 17 00:00:00 2001 From: Masaya Tojo Date: Fri, 4 Dec 2020 04:12:22 +0900 Subject: wip43 --- vikalpa.scm | 1704 ++++++++++++++++++++++----------------------------- vikalpa/prelude.scm | 243 +------- 2 files changed, 746 insertions(+), 1201 deletions(-) diff --git a/vikalpa.scm b/vikalpa.scm index a2b4dd2..1b3c158 100644 --- a/vikalpa.scm +++ b/vikalpa.scm @@ -17,40 +17,104 @@ ;;; along with Vikalpa. If not, see . (define-module (vikalpa) - #:export (rewrite - show - check - system->scheme - load-system - system-primitives - system-functions - system-macros - system-theorems - system-axioms - system-totality-claims - define-system - define-axiom - define-theorem - define-primitive-function - define-function - define-scheme-function - define-proof - define-totality-claim - define-syntax-rules - system-eval - natural? - succ - pred) + #:export () ;; (rewrite + ;; show + ;; check + ;; system->scheme + ;; load-system + ;; system-primitives + ;; system-functions + ;; system-macros + ;; system-theorems + ;; system-axioms + ;; system-totality-claims + ;; define-system + ;; define-axiom + ;; define-theorem + ;; define-primitive-function + ;; define-function + ;; define-scheme-function + ;; define-proof + ;; define-totality-claim + ;; define-syntax-rules + ;; system-eval) #:use-module (ice-9 match) #:use-module (ice-9 format) #:use-module (ice-9 control) + #:use-module (ice-9 exceptions) #:use-module ((srfi srfi-1) #:select (every any member lset-union fold append-map find)) #:use-module (srfi srfi-8) #:use-module (srfi srfi-11) #:use-module (srfi srfi-26) - #:use-module (ice-9 pretty-print)) + #:use-module (ice-9 pretty-print) + #:use-module (oop goops)) + +(define-class () + (definitions #:getter system-definitions #:init-keyword #:definitions) + (total-cliam-method #:getter system-total-claim-method + #:init-keyword #:total-cliam-method)) + +(define-class () + (name #:getter definition-name #:init-keyword #:name)) + +(define-class () + (expressions #:getter condition-expressions #:init-keyword #:expressions)) + +(define-class () + (variables #:getter function-variables #:init-keyword #:variables) + (condition #:getter function-condition #:init-keyword #:condition)) + +(define-class ()) + +(define-class () + (procedure #:getter core-function-procedure #:init-keyword #:procedure)) + +(define-class () + (expression #:getter defined-function-expression #:init-keyword #:expression) + (code #:getter defined-function-code #:init-keyword #:code)) + +(define-class () + (proof #:getter theorem-proof #:init-keyword #:proof)) + +(define-class ()) + +(define-generic total-function?) +(define-method (total-function? x) + (or (is-a? x ) + (is-a? x ) + (is-a? x ))) + +(define-class () + (variables #:getter proposition-variables #:init-keyword #:variables) + (expression #:getter proposition-expression #:init-keyword #:expression)) + +(define-class ()) +(define-class () + (proof #:getter theorem-proof #:init-keyword #:proof)) +(define-class ()) + +(define (theorem? x) + (or (is-a? x ) + (is-a? x ))) + +(define-generic lookup) +(define-method (lookup (name ) (s )) + (find (lambda (x) (eq? name (definition-name x))) + (system-definitions s))) + +(define-generic add-definition) +(define-method (add-definition (d ) (s )) + (if (lookup (definition-name d) s) + (raise-exception + (make-exception + (make-exception-with-message + "(vikalpa) add-definition: duplicated definition") + (make-exception-with-irritants (definition-name s)))) + (make + #:definitions (cons d (system-definitions s)) + #:total-cliam-method (system-total-claim-method s)))) (define (debug f . args) (if #f @@ -73,13 +137,13 @@ ((_ name constractor (m p?) - (n t? getter-name getter) ...) + (n t? getter-var getter) ...) (begin (define len (+ 1 (length (list n ...)))) - (define (constractor getter-name ...) + (define (constractor getter-var ...) (let ((data (make-list len))) (list-set! data m 'name) - (list-set! data n getter-name) + (list-set! data n getter-var) ... data)) (define (p? x) @@ -128,6 +192,9 @@ (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)) @@ -204,39 +271,25 @@ (define (variable=? v1 v2) (eq? v1 v2)) -;; (rule? x) -> boolean? -(define (rule? x) - (and (list? x) - (= 5 (length x)) - (eq? (car x) 'rule) - (let ((vars (list-ref x 1))) - (and (list? vars) - (every variable? vars))) - (let ((preconds (list-ref x 2))) - (and (list? preconds) - (every expression? preconds))) - (expression? (list-ref x 3)) - (expression? (list-ref x 4)))) - -;; (rule (list-of variable?) expression? expression?) -> rule? -(define (rule vars preconds lhs rhs) - (list 'rule vars preconds lhs rhs)) - -;; (rule-vars rule?) -> (list-of variable?) -(define (rule-vars r) - (list-ref r 1)) - -;; (rule-preconds rule?) -> expression? -(define (rule-preconds r) - (list-ref r 2)) - -;; (rule-lhs rule?) -> expression? -(define (rule-lhs r) - (list-ref r 3)) - -;; (rule-rhs rule?) -> expression? -(define (rule-rhs r) - (list-ref r 4)) +(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 (binding? x) (and (pair? x) @@ -357,142 +410,18 @@ => (cut substitute <> (rule-rhs rl))) (else #f))) -(define (system? x) - (and (list? x) - (= 4 (length x)) - (eq? 'system (list-ref x 0)) - (system-definitions? (system-definitions x)) - (system-proofs? (system-proofs x)) - ((const #t) (system-totality-claim-list x)))) - -(define (make-system defs prfs totality-claims) - (list 'system defs prfs totality-claims)) - -(define (system-definitions sys) - (list-ref sys 1)) - -(define (system-proofs sys) - (list-ref sys 2)) - -(define (system-totality-claim-list sys) - (list-ref sys 3)) - -(define (totality-claim id nat? less-than) - (list id nat? less-than)) - -(define (totality-claim-id x) - (list-ref x 0)) - -(define (totality-claim-natural x) - (list-ref x 1)) - -(define (totality-claim-less-than x) - (list-ref x 2)) - -(define (lookup x sys) - (assoc x (system-definitions sys))) - -(define (find-proof x sys) - (assoc x (system-proofs sys))) - -;; (system-definitions? x) -> boolean? -(define (system-definitions? x) - (cond ((null? x) #t) - ((pair? x) - (and (pair? (car x)) - (or (theorem*? (car x)) - (primitive-function? (car x)) - (macro? (car x)) - (function? (car x))) - (system-definitions? (cdr x)))) - (else #f))) - -;; (system-proofs? x) -> boolean? -(define (system-proofs? x) - (cond ((null? x) #t) - ((pair? x) - (and (pair? (car x)) - (proof? (car x)) - (system-proofs? (cdr x)))) - (else #f))) - -(define (primitive-function? x) - (and (list? x) - (= 6 (length x)) - (variable? (function-name x)) - (eq? 'primitive-function (list-ref x 1)) - (vars? (function-vars x)) - ((option expression?) (function-expression x)) - ((option code?) (function-code x)) - ((list-of expression?) (function-preconds x)))) - -;; (primitive-function variable? vars?) -> primitive-function? -(define (primitive-function name vs expr preconds code) - (list name 'primitive-function vs expr preconds code)) - -(define (function? x) - (and (list? x) - (= 6 (length x)) - (variable? (function-name x)) - (eq? 'function (list-ref x 1)) - (vars? (function-vars x)) - (expression? (function-expression x)) - ((option code?) (function-code x)) - ((list-of expression?) (function-preconds x)))) - -(define (code? x) - (and (list? x) - (= 2 (length x)) - (eq? 'code (list-ref x 0)) - ((const #t) (code-expr x)))) - -(define (code x) - (list 'code x)) - -(define (code-expr x) - (cadr x)) - -;; (function variable? vars? expression?) -> function? -(define/guard (function (name variable?) - (vars vars?) - (expr expression?) - (preconds (list-of expression?)) - (code (option code?))) - (list name 'function vars expr preconds code)) - -(define (function-name f) - (list-ref f 0)) - -(define (function-vars f) - (list-ref f 2)) - -(define (function-expression f) - (list-ref f 3)) - -(define (function-preconds f) - (list-ref f 4)) +(define-type code + code + (0 code?) + (1 (const #t) + expr + code-expr)) -(define (function-code f) - (list-ref f 5)) - -(define (definition-name d) - (list-ref d 0)) - -(define (definition-vars d) - (list-ref d 2)) - -(define (definition-expression d) - (list-ref d 3)) - -(define (mrule? x) - (and (list? x) - (= 3 (length x)) - (eq? 'mrule (list-ref x 0)) - ((const #t) (mrule-lhs x)) - ((const #t) (mrule-rhs x)))) - -(define (mrule lhs rhs) - (list 'mrule lhs rhs)) +(define-type mrule + mrule + (0 mrule?) + (1 (const #t) lhs mrule-lhs) + (2 (const #t) rhs mrule-rhs)) (define (mrule-vars mrl) (define (all-vars x) @@ -504,33 +433,18 @@ (else '()))) (all-vars (mrule-lhs mrl))) -(define (mrule-lhs mrl) - (list-ref mrl 1)) - -(define (mrule-rhs mrl) - (list-ref mrl 2)) - -(define (macro? x) - (and (list? x) - (= 4 (length x)) - (eq? 'macro (list-ref x 1)) - (variable? (macro-name x)) - (let ((mrls (macro-mrules x))) - (and (list? mrls) - (every mrule? mrls))) - ((list-of symbol?) (macro-literals x)))) - -(define (macro-name m) - (list-ref m 0)) - -(define (macro-mrules m) - (list-ref m 2)) - -(define (macro-literals m) - (list-ref m 3)) - -(define (macro name rules ls) - (list name 'macro rules ls)) +(define-type macro + macro + (1 macro?) + (0 variable? name macro-name) + (2 (lambda (mrls) + (and (list? mrls) + (every mrule? mrls))) + mruls + macro-mrules) + (3 (list-of symbol?) + literals + macro-literals)) (define (apply-mrule rl ls expr) (define (literal? x) @@ -669,90 +583,23 @@ (expand-let (cdr x)))) (else x))) -(define (succ x) - (+ x 1)) - -(define (pred x) - (- x 1)) - -(define (natural->expr n) - (if (<= n 0) - ''0 - `(succ ,(natural->expr (pred n))))) - -(define (pair->expr x) - (if (pair? x) - `(cons ,(pair->expr (car x)) - ,(pair->expr (cdr x))) - (expr-quote x))) - (define (convert-to-expression x) (quote-all (expand* (filter macro? (system-definitions (current-system))) (expand-let x)))) -;; (axiom variable? vars? expression?) -> axiom? -;; axiom? is theorem* -(define/guard (axiom (name variable?) (vars vars?) (expr expression?)) - (list name 'axiom vars expr)) - (define (vars? x) (and (list? x) (every variable? x))) -;; (axiom? x) -> boolean? -(define (axiom? x) - (and (list? x) - (= 4 (length x)) - (variable? (list-ref x 0)) - (eq? 'axiom (list-ref x 1)) - (vars? (list-ref x 2)) - (expression? (list-ref x 3)))) - -;; (theorem name vars? expression?) -> theorem? -(define/guard (theorem (name variable?) (vars vars?) (expr expression?)) - (list name 'theorem vars expr)) - -;; (theorem? x) -> boolean? -;; theorem? is theorem* -(define (theorem? x) - (and (list? x) - (= 4 (length x)) - (variable? (list-ref x 0)) - (eq? 'theorem (list-ref x 1)) - (vars? (list-ref x 2)) - (expression? (list-ref x 3)))) - -(define (theorem-name x) - (list-ref x 0)) - -;; (theorem*? x) -> boolean? -(define (theorem*? x) - (or (axiom? x) - (theorem? x))) - -(define (theorem-name x) - (list-ref x 0)) - -(define (theorem-vars x) - (list-ref x 2)) - -(define (theorem-expression x) - (list-ref x 3)) - (define (theorem-rules x) - (expression->rules (theorem-vars x) + (expression->rules (theorem-variables x) '() (theorem-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))) @@ -773,11 +620,6 @@ (else `(error eval invalid-expression ,expr))))) -(define/guard (system-eval (expr (const #t)) (sys system?)) - (rewrite/eval (parameterize ((current-system sys)) - (convert-to-expression expr)) - sys)) - ;; (rewriter path? command?) -> rewriter? (define (rewriter p c) (cons p c)) @@ -831,6 +673,11 @@ (define (command-options x) (cdr x)) +;; (define/guard (system-eval (expr (const #t)) (sys system?)) +;; (rewrite/eval (parameterize ((current-system sys)) +;; (convert-to-expression expr)) +;; sys)) + ;; (extract path? expression? preconds? procedure?) -> (values expression? procedure?) (define (extract path expr fail) (if (null? path) @@ -865,22 +712,22 @@ (fail 'invalid-path path)))))) (define (function->rules x) - (list (rule (function-vars x) - (function-preconds x) + (list (rule (function-variables x) + (condition-expressions (function-condition x)) (function-app-form x) - (definition-expression x)) - (rule (function-vars x) - (function-preconds x) - (definition-expression x) + (defined-function-expression x)) + (rule (function-variables x) + (condition-expressions (function-condition x)) + (defined-function-expression x) (function-app-form x)))) (define (apply-function f args) (apply-rule '() - (rule (function-vars f) + (rule (function-variables f) '() - (function-app-form f) - (function-expression f)) - (cons (function-name f) args) + (defined-function-app-form f) + (defined-function-expression f)) + (app-form (definition-name f) args) '())) (define (parse-options/theorem ops fail) @@ -905,6 +752,12 @@ (else (fail 'apply-theorem cmd expr))))) +(define (rewrite/induction sys fname vars expr fail) + (cond + ((lookup fname sys) + (cut make-induction-claim <> vars expr)) + (else (fail 'induction 'not-found fname)))) + (define (rewrite1 sys expr fail r) (let* ((cmd (rewriter-command r)) (cmd/name (command-name cmd))) @@ -913,20 +766,23 @@ (extract (rewriter-path r) expr fail) (builder (cond - ((core-function-name? cmd/name) - (rewrite/core cmd/name extracted-expr fail)) ((equal? '(eval) cmd/name) (rewrite/eval extracted-expr sys)) + ((match cmd/name + (`(induction ,(f . vars)) + (rewrite/induction sys f vars extracted-expr fail)) + (`(induction . ,x) + (fail 'induction x)) + (else #f)) => identity) ((eq? 'error cmd/name) (fail extracted-expr)) ((and (symbol? cmd/name) (lookup cmd/name sys)) => (lambda (x) (cond - ((theorem*? x) + ((is-a? x ) (rewrite/theorem cmd sys x preconds extracted-expr fail)) - ((or (function? x) - (and (primitive-function? x) - (function-expression x))) + ((and (total-function? x) + (is-a? x )) (cond ((any (cut apply-rule '() <> extracted-expr '()) (function->rules x)) => identity) @@ -936,6 +792,7 @@ (fail 'invalid-command cmd extracted-expr))))) (else (fail 'command-not-found cmd extracted-expr))))))) +#; (define/guard (rewrite (sys system?) (expr (const #t)) (seq sequence?)) (let ((expr (convert-to-expression expr))) (let loop ((expr expr) @@ -999,250 +856,226 @@ '()))) (define (theorem->rules def) - (expression->rules (theorem-vars def) + (expression->rules (theorem-variables def) '() (theorem-expression def))) -(define current-system (make-parameter (make-system '() '() '()))) - -(define (add-definition x) - (let ((sys (current-system))) - (current-system - (cond ((lookup (definition-name x) sys) - => (lambda (d) - (if (equal? x d) - sys - (error "(vikalpa) add-definition: duplicated" - (definition-name d))))) - (else (make-system (cons x (system-definitions sys)) - (system-proofs sys) - (system-totality-claim-list sys))))) - x)) - -(define (add-proof x) - (let ((sys (current-system))) - (current-system - (cond ((find-proof (proof-name x) sys) - => (lambda (prf) - (if (equal? x prf) - sys - (error "add-proof: duplicated")))) - (else (make-system (system-definitions sys) - (cons x (system-proofs sys)) - (system-totality-claim-list sys))))) - x)) - -(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 (axiom 'name '(var ...) - (make-theorem-claim (convert-to-expression 'expr) - (current-system))))) - (add-definition t) - (validate-definition t) - t)))) - -(define-syntax define-theorem - (syntax-rules () - ((_ name (var ...) expr) - (let ((t (theorem 'name '(var ...) - (make-theorem-claim (convert-to-expression 'expr) - (current-system))))) - (add-definition t) - (validate-definition t) - t)))) - -(define-syntax define-function - (syntax-rules () - ((_ name (var ...) precond ... expr) - (let ((f (function 'name '(var ...) - (convert-to-expression 'expr) - '(precond ...) - (code 'expr)))) - (add-definition f) - (validate-definition f) - f)))) - -(define-syntax define-primitive-function - (syntax-rules () - ((_ name (var ...) precond ... expr) - (let ((f (primitive-function 'name '(var ...) - (convert-to-expression 'expr) - '(precond ...) - (code 'expr)))) - (add-definition f) - (validate-definition f) - f)))) - -(define-syntax define-core-function - (syntax-rules () - ((_ name (var ...) precond ...) - (let ((f (primitive-function 'name '(var ...) #f '(precond ...) #f))) - (add-definition f) - f)))) - -(define-syntax define-syntax-rules - (syntax-rules () - ((_ name (l ...) ((lhs1 . lhs2) rhs) ...) - (let ((m (macro 'name - (list (mrule '(lhs1 . lhs2) 'rhs) - ...) - '(l ...)))) - (add-definition m) - m)))) - -(define (find-totality-claim name sys) - (assoc name (system-totality-claim-list sys))) - -(define (add-totality-claim tc) - (let ((sys (current-system))) - (cond ((find-totality-claim (totality-claim-id tc) sys) - => (lambda (tc2) - (unless (equal? tc tc2) - (error "(vikalpa) define-totality-claim: duplicated" - tc))))) - (unless (and (symbol? (totality-claim-id tc)) - (cond ((lookup (totality-claim-natural tc) sys) - => function*?) - (else #f)) - (cond ((lookup (totality-claim-less-than tc) sys) - => function*?) - (else #f))) - (error "(vikalpa) define-totality-claim: invalid totality-claim" - tc)) - (current-system - (make-system (system-definitions sys) - (system-proofs sys) - (cons tc (system-totality-claim-list sys)))))) - -(define-syntax-rule (define-totality-claim name nat? <) - (add-totality-claim (totality-claim 'name 'nat? '<))) - -(define core-function-names - '(not equal? pair? cons car cdr integer? < succ pred)) - -(define (core-function-name? x) - (member x core-function-names)) - -(define (rewrite/core name extracted-expr fail) - (case name - ((not) - (match extracted-expr - (('not `(quote ,x)) - (expr-quote (not x))) - (else - (fail 'not extracted-expr)))) - ((equal?) - (match extracted-expr - (('equal? `(quote ,x) `(quote ,y)) - (expr-quote (equal? x y))) - (else - (fail 'equal? extracted-expr)))) - ((pair?) - (match extracted-expr - (('pair? `(quote ,x)) - (expr-quote (pair? x))) - (else - (fail 'pair? extracted-expr)))) - ((cons) - (match extracted-expr - (('cons `(quote ,x) `(quote ,y)) - (expr-quote (cons x y))) - (else - (fail 'cons extracted-expr)))) - ((car) - (match extracted-expr - (('car `(quote ,x)) - (if (pair? x) - (expr-quote (car x)) - ''undefined)) - (else - (fail 'car extracted-expr)))) - ((cdr) - (match extracted-expr - (('cdr `(quote ,x)) - (if (pair? x) - (expr-quote (cdr x)) - ''undefined)) - (else - (fail 'cdr extracted-expr)))) - ((integer?) - (match extracted-expr - (('natural? `(quote ,x)) - (expr-quote (natural? x))) - (else - (fail 'natural? extracted-expr)))) - ((succ) - (match extracted-expr - (('succ `(quote ,x)) - (if (and (natural? x) - (< 0 x)) - (expr-quote (succ x)) - ''undefined)) - (else - (fail 'succ extracted-expr)))) - ((pred) - (match extracted-expr - (('pred `(quote ,x)) - (if (natural? x) - (expr-quote (pred x)) - ''undefined)) - (else - (fail 'pred extracted-expr)))) - ((<) - (match extracted-expr - (('< `(quote ,x) `(quote ,y)) - (if (and (natural? x) (natural? y)) - (expr-quote (< x y)) - ''undefined)) - (else - (fail 'pred extracted-expr)))) - (else (fail 'rewrite/core 'invalid)))) - -(define* (core-system #:optional (parent (make-system '() '() '()))) - (parameterize ((current-system parent)) - (define-core-function not (x)) - (define-core-function equal? (x y)) - (define-core-function pair? (x y)) - (define-core-function cons (x y)) - (define-core-function car (x) (pair? x)) - (define-core-function cdr (x) (pair? x)) - (define-core-function natural? (x)) - (define-core-function < (x y) (natural? x) (natural? y)) - (define-core-function succ (x) (natural? x)) - (define-core-function pred (x) (natural? x)) - (current-system))) - -(define-syntax define-system - (syntax-rules () - ((_ name (systems ...) expr ...) - (define* (name #:optional (parent (make-system '() '() '()))) - (parameterize ((current-system - ((compose systems ... core-system) parent))) - expr - ... - (unless (system? (current-system)) - (error "define-system: invalid system")) - (current-system)))))) - -(define (measure? x) - (and (pair? x) - (variable? (car x)) - (list? (cdr x)) - (<= 1 (length (cdr x))))) - -(define (measure-function-name m) - (car m)) - -(define (measure-function-vars m) - (cdr m)) - -(define (function-app-form f) - (cons (function-name f) (function-vars f))) +;; (define current-system (make-parameter (make-system '() '() '()))) + + +;; (define (add-definition x) +;; (let ((sys (current-system))) +;; (current-system +;; (cond ((lookup (definition-name x) sys) +;; => (lambda (d) +;; (if (equal? x d) +;; sys +;; (error "(vikalpa) add-definition: duplicated" +;; (definition-name d))))) +;; (else (make-system (cons x (system-definitions sys)) +;; (system-proofs sys) +;; (system-totality-claim-list sys))))) +;; x)) + +;; (define (add-proof x) +;; (let ((sys (current-system))) +;; (current-system +;; (cond ((find-proof (proof-name x) sys) +;; => (lambda (prf) +;; (if (equal? x prf) +;; sys +;; (error "add-proof: duplicated")))) +;; (else (make-system (system-definitions sys) +;; (cons x (system-proofs sys)) +;; (system-totality-claim-list sys))))) +;; x)) + +;; (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 (axiom 'name '(var ...) +;; (convert-to-expression 'expr)))) +;; (add-definition t) +;; (validate-definition t) +;; t)))) + +;; (define-syntax define-theorem +;; (syntax-rules () +;; ((_ name (var ...) expr) +;; (let ((t (theorem 'name '(var ...) +;; (convert-to-expression 'expr)))) +;; (add-definition t) +;; (validate-definition t) +;; t)))) + +;; (define-syntax define-function +;; (syntax-rules () +;; ((_ name (var ...) precond ... expr) +;; (let ((f (function 'name '(var ...) +;; (convert-to-expression 'expr) +;; '(precond ...) +;; (code 'expr)))) +;; (add-definition f) +;; (validate-definition f) +;; f)))) + +;; (define-syntax define-primitive-function +;; (syntax-rules () +;; ((_ name (var ...) precond ... expr) +;; (let ((f (primitive-function 'name '(var ...) +;; (convert-to-expression 'expr) +;; '(precond ...) +;; (code 'expr)))) +;; (add-definition f) +;; (validate-definition f) +;; f)))) + +;; (define-syntax define-core-function +;; (syntax-rules () +;; ((_ name (var ...) precond ...) +;; (let ((f (primitive-function 'name '(var ...) #f '(precond ...) #f))) +;; (add-definition f) +;; f)))) + +;; (define-syntax define-syntax-rules +;; (syntax-rules () +;; ((_ name (l ...) ((lhs1 . lhs2) rhs) ...) +;; (let ((m (macro 'name +;; (list (mrule '(lhs1 . lhs2) 'rhs) +;; ...) +;; '(l ...)))) +;; (add-definition m) +;; m)))) + +;; (define (find-totality-claim name sys) +;; (assoc name (system-totality-claim-list sys))) + +;; (define (add-totality-claim tc) +;; (let ((sys (current-system))) +;; (cond ((find-totality-claim (totality-claim-id tc) sys) +;; => (lambda (tc2) +;; (unless (equal? tc tc2) +;; (error "(vikalpa) define-totality-claim: duplicated" +;; tc))))) +;; (unless (and (symbol? (totality-claim-id tc)) +;; (cond ((lookup (totality-claim-natural tc) sys) +;; => function*?) +;; (else #f)) +;; (cond ((lookup (totality-claim-less-than tc) sys) +;; => function*?) +;; (else #f))) +;; (error "(vikalpa) define-totality-claim: invalid totality-claim" +;; tc)) +;; (current-system +;; (make-system (system-definitions sys) +;; (system-proofs sys) +;; (cons tc (system-totality-claim-list sys)))))) + +;; (define-syntax-rule (define-totality-claim name nat? <) +;; (add-totality-claim (totality-claim 'name 'nat? '<))) + +;; (define core-function-names +;; '(not equal? pair? cons car cdr integer? < binary-+ unary--)) + +;; (define (core-function-name? x) +;; (member x core-function-names)) + +;; (define (rewrite/core name extracted-expr fail) +;; (case name +;; ((not) +;; (match extracted-expr +;; (('not `(quote ,x)) +;; (expr-quote (not x))) +;; (else +;; (fail 'not extracted-expr)))) +;; ((equal?) +;; (match extracted-expr +;; (('equal? `(quote ,x) `(quote ,y)) +;; (expr-quote (equal? x y))) +;; (else +;; (fail 'equal? extracted-expr)))) +;; ((pair?) +;; (match extracted-expr +;; (('pair? `(quote ,x)) +;; (expr-quote (pair? x))) +;; (else +;; (fail 'pair? extracted-expr)))) +;; ((cons) +;; (match extracted-expr +;; (('cons `(quote ,x) `(quote ,y)) +;; (expr-quote (cons x y))) +;; (else +;; (fail 'cons extracted-expr)))) +;; ((car) +;; (match extracted-expr +;; (('car `(quote ,x)) +;; (if (pair? x) +;; (expr-quote (car x)) +;; ''())) +;; (else +;; (fail 'car extracted-expr)))) +;; ((cdr) +;; (match extracted-expr +;; (('cdr `(quote ,x)) +;; (if (pair? x) +;; (expr-quote (cdr x)) +;; ''())) +;; (else +;; (fail 'cdr extracted-expr)))) +;; ((integer?) +;; (match extracted-expr +;; (('integer? `(quote ,x)) +;; (expr-quote (integer? x))) +;; (else +;; (fail 'integer? extracted-expr)))) +;; ((<) +;; (match extracted-expr +;; (('< `(quote ,x) `(quote ,y)) +;; (let ((x (if (integer? x) x 0)) +;; (y (if (integer? y) y 0))) +;; (expr-quote (< x y)))) +;; (else +;; (fail '< extracted-expr)))) +;; ((succ) +;; (match extracted-expr +;; (('binary-+ `(quote ,x) `(quote ,y)) +;; (if (integer? x) +;; (if (integer? y) +;; (expr-quote (+ x y)) +;; (expr-quote x)) +;; (if (integer? y) +;; (expr-quote y) +;; (expr-quote 0)))) +;; (else +;; (fail 'binary-+ extracted-expr)))) +;; ((unary--) +;; (match extracted-expr +;; (('unary-- `(quote ,x)) +;; (if (integer? x) +;; (expr-quote (- x)) +;; (expr-quote 0))) +;; (else +;; (fail 'unary-- extracted-expr)))) +;; (else (fail 'rewrite/core 'invalid)))) + +;; (define-syntax define-system +;; (syntax-rules () +;; ((_ name (systems ...) expr ...) +;; (define* (name #:optional (parent (make-system '() '() '()))) +;; (parameterize ((current-system +;; ((compose systems ... core-system) parent))) +;; expr +;; ... +;; (unless (system? (current-system)) +;; (error "define-system: invalid system")) +;; (current-system)))))) + +(define (defined-function-app-form f) + (cons (definition-name f) (function-variables f))) (define (single? x) (and (pair? x) @@ -1274,435 +1107,360 @@ (else (if/if x y ''#t)))) -(define (make-totality-claim tc m-expr f) - (let* ((name (function-name f))) - (define (convert app-form) - (cond - ((apply-rule '() - (rule (function-vars f) - '() - (function-app-form f) - m-expr) - app-form - '()) - => identity) - (else (error "make-totality-claim: convert error" - (function-name f) - m-expr - app-form)))) - (if/if `(,(totality-claim-natural tc) ,m-expr) - (let loop ((expr (function-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)))) - (and/if test/result - (if/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 (and/if (loop (car args)) - (f (cdr args)))))))) - (if (eq? name (app-form-name expr)) - (and/if `(,(totality-claim-less-than tc) - ,(convert expr) - ,m-expr) - rest) - rest))) - (else (error "(vikalpa) make-totality-claim: error" - (function-name f) - m-expr)))) - ''#f))) - -(define (make-totality-claim/preconds 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 (function-preconds f))) - (map (lambda (precond) - (substitute (map cons - (function-vars f) - (cdr expr)) - precond)) - preconds)))) - (else (error "make-totality-claim/preconds: error"))) - rest))) - ((if-form? expr) - (find-preconds (if-form-test expr))) - (else '()))) - (define (build/find-if expr) - (cond - ((if-form? expr) - (if/if (build/find-if (if-form-test expr)) - (build (if-form-then expr)) - (build (if-form-else expr)))) - ((app-form? expr) - (apply and/if (map build/find-if (app-form-args expr)))) - (else ''#t))) - (define (build expr) - (cond - ((if-form? expr) - (apply and/if - (append (find-preconds (if-form-test expr)) - (list (if/if (if-form-test expr) - (build (if-form-then expr)) - (build (if-form-else expr))))))) - ((app-form? expr) - (apply and/if - (append (find-preconds expr) - (list (build/find-if expr))))) - (else ''#t))) - (if/if (build expr) - '#t - '#f)) - -(define (make-theorem-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 (function-preconds f))) - (map (lambda (precond) - (substitute (map cons - (function-vars f) - (cdr expr)) - precond)) - preconds)))) - (else (error "make-theorem-claim/preconds: error"))) - rest))) - ((if-form? expr) - (find-preconds (if-form-test expr))) - (else '()))) - (define (build/find-if expr) - (cond - ((if-form? expr) - (if/if (build/find-if (if-form-test expr)) - (build (if-form-then expr)) - (build (if-form-else expr)))) - ((app-form? expr) - (fold implies/if - expr - (map build/find-if (app-form-args expr)))) - (else expr))) - (define (build expr) - (cond - ((if-form? expr) - (fold implies/if - (if/if (if-form-test expr) - (build (if-form-then expr)) - (build (if-form-else expr))) - (find-preconds (if-form-test expr)))) - ((app-form? expr) - (fold implies/if - (build/find-if expr) - (find-preconds expr))) - (else expr))) - (build expr)) - -(define/guard (make-induction-claim (f function*?) - (vars (list-of variable?)) - (t theorem?)) +;; (define (make-totality-claim tc m-expr f) +;; (let* ((name (function-name f))) +;; (define (convert app-form) +;; (cond +;; ((apply-rule '() +;; (rule (function-vars f) +;; '() +;; (function-app-form f) +;; m-expr) +;; app-form +;; '()) +;; => identity) +;; (else (error "make-totality-claim: convert error" +;; (function-name f) +;; m-expr +;; app-form)))) +;; (if/if `(,(totality-claim-natural tc) ,m-expr) +;; (let loop ((expr (function-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)))) +;; (and/if test/result +;; (if/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 (and/if (loop (car args)) +;; (f (cdr args)))))))) +;; (if (eq? name (app-form-name expr)) +;; (and/if `(,(totality-claim-less-than tc) +;; ,(convert expr) +;; ,m-expr) +;; rest) +;; rest))) +;; (else (error "(vikalpa) make-totality-claim: error" +;; (function-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 (function-guard f))) +;; (map (lambda (precond) +;; (substitute (map cons +;; (function-vars f) +;; (cdr expr)) +;; precond)) +;; preconds)))) +;; (else (error "make-guard-claim: error"))) +;; rest))) +;; ((if-form? expr) +;; (find-preconds (if-form-test expr))) +;; (else '()))) +;; (define (build/find-if expr) +;; (cond +;; ((if-form? expr) +;; (if/if (build/find-if (if-form-test expr)) +;; (build (if-form-then expr)) +;; (build (if-form-else expr)))) +;; ((app-form? expr) +;; (apply and/if (map build/find-if (app-form-args expr)))) +;; (else ''#t))) +;; (define (build expr) +;; (cond +;; ((if-form? expr) +;; (apply and/if +;; (append (find-preconds (if-form-test expr)) +;; (list (if/if (if-form-test expr) +;; (build (if-form-then expr)) +;; (build (if-form-else expr))))))) +;; ((app-form? expr) +;; (apply and/if +;; (append (find-preconds expr) +;; (list (build/find-if expr))))) +;; (else ''#t))) +;; (if/if (build expr) +;; ''#t +;; ''#f)) + +(define (make-induction-claim f vars c) (define (find-app-forms expr) (cond ((app-form? expr) (let ((rest (append-map find-app-forms (cdr expr)))) - (if (eq? (function-name f) (app-form-name expr)) + (if (eq? (definition-name f) (app-form-name expr)) (cons expr rest) rest))) ((if-form? expr) (error "make-induction-claim(find-app-forms): not supported" expr)) (else '()))) - (let ((c (theorem-expression t))) - (define (prop app-form) - (cond - ((apply-rule '() - (rule vars - '() - (cons (function-name f) vars) - c) - app-form - '()) - => identity) - (else - (error "make-induction-claim: fail" app-form)))) + (define (prop 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)))) - (implies/if (if (null? app-forms) - ''#t - (fold implies/if c (map prop app-forms))) - (if/if (if-form-test expr) - (build (if-form-then expr)) - (build (if-form-else expr)))))) - (else - (let ((app-forms (find-app-forms expr))) - (fold implies/if c (map prop app-forms)))))))) - (else (error "make-induction-claim: invalid" - f vars t))))) - -(define (proof? x) - (and (list? x) - (= 4 (length x)) - (symbol? (proof-name x)) - (eq? 'proof (list-ref x 1)) - (seed? (proof-seed x)) - (sequence? (proof-sequence x)))) - -(define (proof name seed sequence) - (list name 'proof seed sequence)) - -(define (proof-name x) - (list-ref x 0)) - -(define (proof-seed x) - (list-ref x 2)) - -(define (proof-sequence x) - (list-ref x 3)) - -(define seed? (const #t)) - -(define-syntax define-proof - (syntax-rules () - ((_ name - (seed ...) - (((n ...) cmd ...) ...)) - (add-proof (proof 'name - '(seed ...) - '(((n ...) cmd ...) ...)))))) - -(define (function*? x) - (or (function? x) - (primitive-function? x))) - -(define (validate-expression sys name vars expr) - (let* ((expr-fnames (expression-functions expr)) - (expr-vars (expression-vars expr))) - (when (reserved? name) - (error (format #f "(vikalpa) ~a: reserved name" name))) - (for-each (lambda (x) - (when (member x expr-fnames) - (error (format #f "(vikalpa) ~a: invalid variable name" name) - x))) - vars) - (for-each (lambda (x) - (unless (cond ((lookup x sys) => function*?) - (else #f)) - (error (format #f "(vikalpa) ~a: undefined function" name) - x))) - expr-fnames) - (for-each (lambda (x) - (unless (member x vars) - (error (format #f "(vikalpa) ~a: undefined variable" name) - x))) - expr-vars))) - -(define (validate-definition d) - (let* ((vars (definition-vars d)) - (name (definition-name d)) - (expr (definition-expression d))) - (validate-expression (current-system) name vars expr))) - -(define (trivial-total? f) - (not (member (function-name f) - (expression-functions (function-expression f))))) - -(define (prove sys def pf) - (cond - ((theorem? def) - (prove/theorem sys def pf)) - ((function? def) - (prove/function sys def pf)) - (else (error "prove" def pf)))) - -(define (prove/theorem sys t pf) - (let ((sys-without-self - (make-system (filter (lambda (d) (not (equal? t d))) - (system-definitions sys)) - (system-proofs sys) - (system-totality-claim-list sys)))) - (match (proof-seed pf) - ((f . vars) - (cond - ((lookup f sys-without-self) - => (lambda (seed) - (let ((claim (make-induction-claim seed vars t))) - (validate-expression sys - `(claim-of ,(proof-name pf)) - (theorem-vars t) - claim) - (rewrite sys-without-self - claim - (proof-sequence pf))))) - (else (error "(vikalpa) define-proof: induction function is not found." - (proof-name pf) - (cons f vars))))) - (() - (rewrite sys-without-self - (theorem-expression t) - (proof-sequence pf))) - (else - (error "prove/theorem: fail"))))) - -(define (prove/function sys f pf) - (match (proof-seed pf) - (() - (unless (trivial-total? f) - (error "prove/function")) - (rewrite sys - (fold implies/if - (make-totality-claim/preconds - (function-expression f) - sys) - (function-preconds f)) - (proof-sequence pf))) - ((id m-expr) - (cond - ((find-totality-claim id sys) - => (lambda (tc) - (let ((claim (make-totality-claim tc m-expr f))) - (validate-expression sys - `(claim-of ,(function-name f)) - (function-vars f) - claim) - (rewrite sys - (fold implies/if - (and/if - (make-totality-claim/preconds - (function-expression f) - sys) - claim) - (function-preconds f)) - (proof-sequence pf))))) - (else - (error "(vikalpa) define-proof: totality-claim is not found:" - (proof-name pf) - (proof-seed pf))))) - (else - (error "define-proof: fail" - (proof-name pf) (proof-seed pf))))) - -(define (system->scheme sys) - `(begin - ,@(map (lambda (f) - `(define (,(function-name f) ,@(function-vars f)) - ,(code-expr (function-code f)))) - (reverse (filter (lambda (x) - (and (function*? x) - (function-code x))) - (system-definitions sys)))))) - -(define/guard (check (sys system?)) - (let loop ((sys sys) - (fails '())) - (let ((defs (system-definitions sys))) - (define* (next #:optional fail) - (loop (make-system (cdr defs) - (system-proofs sys) - (system-totality-claim-list sys)) - (if fail - (cons fail fails) - fails))) - (cond - ((null? defs) fails) - ((or (theorem? (car defs)) - (function? (car defs))) - (cond - #; - ((and (function? (car defs)) - (trivial-total? (car defs))) - (next)) - (else - (cond - ((find-proof (definition-name (car defs)) sys) - => (lambda (pf) - (let ((result (prove sys (car defs) pf))) - (cond - ((equal? result ''#t) - (next)) - (else - (next (list (definition-name (car defs)) - result))))))) - (else - (next (list (definition-name (car defs))))))))) - (else - (next)))))) - -(define (pp x) - (pretty-print x - #:width 79 - #:max-expr-width 50)) - -(define/guard (show (sys system?) (name symbol?)) + ((apply-rule '() + (rule vars + '() + (app-form (definition-name f) vars) + c) + app-form + '()) + => identity) + (else + (error "make-induction-claim: fail" app-form)))) (cond - ((lookup name sys) - => (lambda (def) - (cond - ((function? def) - `(define-function ,(function-name def) ,(function-vars def) - ,(function-expression def))) - ((theorem? def) - `(define-theorem ,(theorem-name def) ,(theorem-vars def) - ,(theorem-expression def))) - ((axiom? def) - `(define-axiom ,(theorem-name def) ,(theorem-vars def) - ,(theorem-expression def))) - ((primitive-function? def) - `(define-primitive-function - ,(function-name def) - ,(function-vars def))) - ((macro? def) - `(define-syntax-rules ,(macro-name def))) - (else - `(error 'fatal-error ,name))))) - (else - `(error 'not-found ,name)))) - -(define/guard (load-system (sys system?)) - (primitive-eval (system->scheme sys))) - -(define/guard (system-primitives (sys system?)) - (append reserved-symbols - (map function-name - (filter primitive-function? - (system-definitions sys))))) - -(define/guard (system-functions (sys system?)) - (map function-name - (filter function? - (system-definitions sys)))) - -(define/guard (system-theorems (sys system?)) - (map theorem-name - (filter theorem? - (system-definitions sys)))) - -(define/guard (system-axioms (sys system?)) - (map theorem-name - (filter axiom? - (system-definitions sys)))) - -(define/guard (system-macros (sys system?)) - (map macro-name - (filter macro? - (system-definitions sys)))) - -(define/guard (system-totality-claims (sys system?)) - (system-totality-claim-list sys)) + ((apply-function f vars) + => (lambda (expr) + (let build ((expr expr)) + (cond + ((if-form? expr) + (let ((app-forms (find-app-forms (if-form-test expr)))) + (implies/if (if (null? app-forms) + ''#t + (fold implies/if c (map prop app-forms))) + (if/if (if-form-test expr) + (build (if-form-then expr)) + (build (if-form-else expr)))))) + (else + (let ((app-forms (find-app-forms expr))) + (fold implies/if c (map prop app-forms)))))))) + (else (error "make-induction-claim: invalid" + f vars c)))) + +;; (define (proof? x) +;; (and (list? x) +;; (= 4 (length x)) +;; (symbol? (proof-name x)) +;; (eq? 'proof (list-ref x 1)) +;; (seed? (proof-seed x)) +;; (sequence? (proof-sequence x)))) + +;; (define (proof name seed sequence) +;; (list name 'proof seed sequence)) + +;; (define (proof-name x) +;; (list-ref x 0)) + +;; (define (proof-seed x) +;; (list-ref x 2)) + +;; (define (proof-sequence x) +;; (list-ref x 3)) + +;; (define seed? (const #t)) + +;; (define-syntax define-proof +;; (syntax-rules () +;; ((_ name +;; (((n ...) cmd ...) ...)) +;; (add-proof (proof 'name +;; '() +;; '(((n ...) cmd ...) ...)))) +;; ((_ name +;; (seed ...) +;; (((n ...) cmd ...) ...)) +;; (add-proof (proof 'name +;; '(seed ...) +;; '(((n ...) cmd ...) ...)))))) + +;; (define (function*? x) +;; (or (function? x) +;; (primitive-function? x))) + +;; (define (validate-expression sys name vars expr) +;; (let* ((expr-fnames (expression-functions expr)) +;; (expr-vars (expression-vars expr))) +;; (when (reserved? name) +;; (error (format #f "(vikalpa) ~a: reserved name" name))) +;; (for-each (lambda (x) +;; (when (member x expr-fnames) +;; (error (format #f "(vikalpa) ~a: invalid variable name" name) +;; x))) +;; vars) +;; (for-each (lambda (x) +;; (unless (cond ((lookup x sys) => function*?) +;; (else #f)) +;; (error (format #f "(vikalpa) ~a: undefined function" name) +;; x))) +;; expr-fnames) +;; (for-each (lambda (x) +;; (unless (member x vars) +;; (error (format #f "(vikalpa) ~a: undefined variable" name) +;; x))) +;; expr-vars))) + +;; (define (validate-definition d) +;; (let* ((vars (definition-vars d)) +;; (name (definition-name d)) +;; (expr (definition-expression d))) +;; (validate-expression (current-system) name vars expr))) + +;; (define (recur? f) +;; (member (function-name f) +;; (expression-functions (function-expression f)))) + +;; (define (p x) +;; (format #t "p:~%~y" x) +;; x) + +;; (define (trivial-total? f sys) +;; (and (not (recur? f)))) + +;; (define (prove sys def pf) +;; (cond +;; ((theorem? def) +;; (prove/theorem sys def pf)) +;; ((function? def) +;; (prove/function sys def pf)) +;; (else (error "prove" def pf)))) + +;; (define (prove/theorem sys t pf) +;; (let ((sys-without-self +;; (make-system (filter (lambda (d) (not (equal? t d))) +;; (system-definitions sys)) +;; (system-proofs sys) +;; (system-totality-claim-list sys)))) +;; (rewrite sys-without-self +;; (theorem-expression t) +;; (proof-sequence pf)))) + +;; (define (prove/function sys f pf) +;; (match (proof-seed pf) +;; (() +;; (error "prove/function error")) +;; ((id m-expr) +;; (cond +;; ((find-totality-claim id sys) +;; => (lambda (tc) +;; (let ((claim (make-totality-claim tc m-expr f))) +;; (validate-expression sys +;; `(claim-of ,(function-name f)) +;; (function-vars f) +;; claim) +;; (rewrite sys +;; claim +;; (proof-sequence pf))))) +;; (else +;; (error "(vikalpa) define-proof: totality-claim is not found:" +;; (proof-name pf) +;; (proof-seed pf))))) +;; (else +;; (error "define-proof: fail" +;; (proof-name pf) (proof-seed pf))))) + +;; (define (system->scheme sys) +;; `(begin +;; ,@(map (lambda (f) +;; `(define (,(function-name f) ,@(function-vars f)) +;; ,(code-expr (function-code f)))) +;; (reverse (filter (lambda (x) +;; (and (function*? x) +;; (function-code x))) +;; (system-definitions sys)))))) + +;; (define/guard (check (sys system?)) +;; (let loop ((sys sys) +;; (fails '())) +;; (let ((defs (system-definitions sys))) +;; (define* (next #:optional fail) +;; (loop (make-system (cdr defs) +;; (system-proofs sys) +;; (system-totality-claim-list sys)) +;; (if fail +;; (cons fail fails) +;; fails))) +;; (cond +;; ((null? defs) fails) +;; ((or (theorem? (car defs)) +;; (function? (car defs))) +;; (cond +;; ((and (function? (car defs)) +;; (trivial-total? (car defs) sys)) +;; (next)) +;; (else +;; (cond +;; ((find-proof (definition-name (car defs)) sys) +;; => (lambda (pf) +;; (let ((result (prove sys (car defs) pf))) +;; (cond +;; ((equal? result ''#t) +;; (next)) +;; (else +;; (next (list (definition-name (car defs)) +;; result))))))) +;; (else +;; (next (list (definition-name (car defs))))))))) +;; (else +;; (next)))))) + +;; (define/guard (show (sys system?) (name symbol?)) +;; (cond +;; ((lookup name sys) +;; => (lambda (def) +;; (cond +;; ((function? def) +;; `(define-function ,(function-name def) ,(function-vars def) +;; ,(function-expression def))) +;; ((theorem? def) +;; `(define-theorem ,(theorem-name def) ,(theorem-vars def) +;; ,(theorem-expression def))) +;; ((axiom? def) +;; `(define-axiom ,(theorem-name def) ,(theorem-vars def) +;; ,(theorem-expression def))) +;; ((primitive-function? def) +;; `(define-primitive-function +;; ,(function-name def) +;; ,(function-vars def))) +;; ((macro? def) +;; `(define-syntax-rules ,(macro-name def))) +;; (else +;; `(error 'fatal-error ,name))))) +;; (else +;; `(error 'not-found ,name)))) + +;; (define/guard (load-system (sys system?)) +;; (primitive-eval (system->scheme sys))) + +;; (define/guard (system-primitives (sys system?)) +;; (append reserved-symbols +;; (map function-name +;; (filter primitive-function? +;; (system-definitions sys))))) + +;; (define/guard (system-functions (sys system?)) +;; (map function-name +;; (filter function? +;; (system-definitions sys)))) + +;; (define/guard (system-theorems (sys system?)) +;; (map theorem-name +;; (filter theorem? +;; (system-definitions sys)))) + +;; (define/guard (system-axioms (sys system?)) +;; (map theorem-name +;; (filter axiom? +;; (system-definitions sys)))) + +;; (define/guard (system-macros (sys system?)) +;; (map macro-name +;; (filter macro? +;; (system-definitions sys)))) + +;; (define/guard (system-totality-claims (sys system?)) +;; (system-totality-claim-list sys)) diff --git a/vikalpa/prelude.scm b/vikalpa/prelude.scm index c61e459..f37bdd0 100644 --- a/vikalpa/prelude.scm +++ b/vikalpa/prelude.scm @@ -17,16 +17,24 @@ ;;; along with Vikalpa. If not, see . (define-module (vikalpa prelude) - #:export (natural? size implies prelude) + #:export (prelude) #:use-module (vikalpa)) -(define-syntax implies - (syntax-rules () - ((_ x y) (if x y #t)) - ((_ x y z rest ...) - (if x (implies y z rest ...) #t)))) - (define-system prelude () + (define-function natural? (x) + (if (integer? x) + (< 0 x) + #f)) + + (define-syntax-rules + () + ((+ x . xs) (binary-+ x (+ . xs))) + ((+ x) x) + ((+) '0)) + + (define-syntax-rules - () + ((- x . xs) (binary-+ x (- . xs))) + ((- x) (unary-- x))) + (define-syntax-rules list () ((list) '()) ((list x . y) (cons x (list . y)))) @@ -102,226 +110,5 @@ (define-function zero? (x) (equal? 0 x)) - (define-axiom pred/succ (x) - (implies (natural? x) - (equal? (pred (succ x)) x))) - - - (define-axiom succ/pred (x) - (implies (natural? x) - (not (zero? x)) - (equal? (succ (pred x)) x))) - - (define-axiom less/pred (x) - (implies (natural? x) - (equal? (< (pred x) x) #t))) - (define-totality-claim natural? natural? <) - (define-function + (x y) - (natural? x) - (natural? y) - (if (zero? x) - y - (succ (+ (pred x) y)))) - - (define-proof + - (natural? x) - ()) - - #; - (define-proof natural? - () - (((1 2 3 1) (eval)) - ((1 2 3) if-true) - (() if-same (set x (zero? x))) - ((2 1 2) if-nest) - ((2 1) if-same) - ((2) if-true) - ((3 1 2) if-nest) - ((3) if-same (set x (integer? x))) - ((3 2 1) if-nest) - ((3 2) if-nest) - ((3 3 1) if-nest) - ((3 3) if-true) - ((3) if-same) - (() if-same))) - - #; - (define-proof + - (natural? x) - () - #; - (((2) if-nest) - ((2 3) less/pred) - ((2) if-same) - (() if-same))) - - ;; (define-proof if-implies - ;; () - ;; (((1) if-same (set x x)) - ;; ((1 2 1) if-nest) - ;; ((1 3 1) if-nest) - ;; ((1 3) if-true) - - ;; (define-proof less-than/pred - ;; (natural-induction x) - ;; (((2 2) if-nest) - ;; ((2 2) if-not) - ;; ((2 2) if-nest) - ;; ((2 3 2) if-nest) - ;; ((2 3 2) if-nest) - ;; ((2 3) if-implies) - ;; ((2 3 2) if-implies) - - ;; (() error) - ;; (() error))) - - ;; (define-proof less-than/pred-1 - ;; () - ;; (((2 2) if-same (set x (natural? (pred x)))) - ;; ((2 2 2) if-same (set x (not (zero? (pred x))))) - ;; ((2 2 2) if-same (set x (not (zero? (pred x))))) - ;; ;; ((2 2 3 1 1) zero?) - ;; ;; ((2 2 3 1 1) if-nest) - ;; ;; ((2 2 3 1) if-false) - ;; ;; ((2 2 3 1) if-false) - ;; )) - - - - ;; (define-theorem natural/add1 (x) - ;; (implies (natural? x) - ;; (equal? (natural? (add1 x)) #t))) - - #; - (define-axiom natural/sub1 (x) - (if (natural? x) - (if (< '0 x) - (equal? (natural? (sub1 x)) '#t) - '#t) - '#t)) - - #; - (define-theorem less-than/sub1 (x) - (implies (natural? x) - (< '0 x) - (equal? (< (sub1 x) x) '#t))) - - #; - (define-axiom add1/sub1 (x) - (if (natural? x) - (if (equal? '0 x) - '#t - (equal? (add1 (sub1 x)) x)) - '#t)) - - #; - (define-built-in-function + (x y) - (if (natural? x) - (if (equal? '0 x) - y - (add1 (+ (sub1 x) y))) - 'undefined)) - - #; - (define-axiom natural/size (x) - (equal? (natural? (size x)) - '#t)) - - #; - (define-axiom size/car (x) - (if (pair? x) - (equal? (< (size (car x)) (size x)) - '#t) - '#t)) - - #; - (define-axiom size/cdr (x) - (if (pair? x) - (equal? (< (size (cdr x)) (size x)) - '#t) - '#t)) - - #; - (define-proof + - (total/natural? x) - (((2) if-nest) - ((2 3)