summaryrefslogtreecommitdiff
path: root/vikalpa.scm
diff options
context:
space:
mode:
Diffstat (limited to 'vikalpa.scm')
-rw-r--r--vikalpa.scm195
1 files changed, 95 insertions, 100 deletions
diff --git a/vikalpa.scm b/vikalpa.scm
index 5f7b16d..d1da85b 100644
--- a/vikalpa.scm
+++ b/vikalpa.scm
@@ -1,5 +1,5 @@
;;; Vikalpa --- Proof Assistant
-;;; Copyright © 2020 Masaya Tojo <masaya@tojo.tokyo>
+;;; Copyright © 2020, 2021 Masaya Tojo <masaya@tojo.tokyo>
;;;
;;; This file is part of Vikalpa.
;;;
@@ -28,8 +28,9 @@
define-system
define-proof
define-core-function
+ define-core-function/guard
define-function
- define-trivial-total-function
+ define-function/guard
define-syntax-rules
define-axiom
define-theorem)
@@ -77,7 +78,7 @@
(define-class <axiom> (<theorem*>))
(define-class <function*> (<definition>)
- (conditions #:getter get-conditions #:init-keyword #:conditions))
+ (guards #:getter get-guards #:init-keyword #:guards))
(define-class <core-function> (<function*>)
(procedure #:getter get-procedure #:init-keyword #:procedure))
(define-class <expandable-function> (<function*>)
@@ -85,7 +86,6 @@
(code #:getter get-code #:init-keyword #:code))
(define-class <function> (<expandable-function> <provable>))
(define-class <total-function> (<expandable-function> <proved>))
-(define-class <trivial-total-function> (<expandable-function>))
(define-class <macro> (<definition>)
(mrules #:getter macro-mrules #:init-keyword #:mrules)
@@ -118,8 +118,6 @@
(write-definition 'function d port))
(define-method (write (d <core-function>) port)
(write-definition 'core-function d port))
-(define-method (write (d <trivial-total-function>) port)
- (write-definition 'trivial-total-function d port))
(define-method (write (d <total-function>) port)
(write-definition 'total-function d port))
@@ -791,11 +789,11 @@
(define (function->rules x)
(list (rule (get-variables x)
- (get-conditions x)
+ (list)
(defined-function-app-form x)
(get-expression x))
(rule (get-variables x)
- (get-conditions x)
+ (list)
(get-expression x)
(defined-function-app-form x))))
@@ -972,53 +970,65 @@
(validate t)
t))))
-(define-syntax define-core-function
- (syntax-rules ()
- ((_ name (var ...) proc)
+(define-syntax define-core-function/guard
+ (syntax-rules (and)
+ ((_ name (var ...) (and guard ...) proc)
(let ((f (make <core-function>
#:name 'name
#:variables '(var ...)
- #:conditions '()
+ #:guards (map convert-to-expression (list 'guard ...))
#:procedure proc)))
(current-system (add-definition f (current-system)))
(validate f)
- f))))
+ f))
+ ((_ name (var ...) guard proc)
+ (define-core-function/guard name (var ...) (and guard) proc))))
-(define-syntax define-function
+(define-syntax define-core-function
(syntax-rules ()
- ((_ name (var ...) expr)
- (let ((f (let ((expression (convert-to-expression 'expr)))
- (if (member 'name (expression-functions expression))
- (make <function>
- #:name 'name
- #:variables '(var ...)
- #:conditions '()
- #:expression expression
- #:code (code 'expr))
- (make <total-function>
- #:name 'name
- #:variables '(var ...)
- #:conditions '()
- #:expression expression
- #:code (code 'expr)
- #:claim ''#t
- #:proof '())))))
+ ((_ name (var ...) proc)
+ (define-core-function/guard name (var ...) (and) proc))))
+
+(define (recursive? f)
+ (member (get-name f) (expression-functions (get-expression f))))
+
+(define (has-guard-claim? f sys)
+ (let ((claim (make-guard-claim (get-expression f) sys)))
+ (not (equal? ''#t claim))))
+
+(define-syntax define-function/guard
+ (syntax-rules (and)
+ ((_ name (var ...) (and guard ...) expr)
+ (let* ((expression (convert-to-expression 'expr))
+ (guard-expressions (map convert-to-expression
+ (list 'guard ...)))
+ (f (make <function>
+ #:name 'name
+ #:variables '(var ...)
+ #:guards guard-expressions
+ #:expression expression
+ #:code (code 'expr))))
(current-system (add-definition f (current-system)))
(validate f)
- f))))
+ (when (and (not (recursive? f))
+ (not (has-guard-claim? f (current-system))))
+ (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-trivial-total-function
+(define-syntax define-function
(syntax-rules ()
((_ name (var ...) expr)
- (let ((f (make <trivial-total-function>
- #:name 'name
- #:variables '(var ...)
- #:conditions '()
- #:expression (convert-to-expression 'expr)
- #:code (code 'expr))))
- (current-system (add-definition f (current-system)))
- (validate f)
- f))))
+ (define-function/guard name (var ...) (and) expr))))
(define-syntax define-syntax-rules
(syntax-rules ()
@@ -1032,6 +1042,10 @@
(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)))
@@ -1159,34 +1173,34 @@
(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))))))))
+ (else (and/if (loop (car args))
+ (f (cdr args))))))))
(if (eq? name (app-form-name expr))
(and/if `(,(get-measure-less-than sys)
,(convert expr)
- ,m-expr)
- rest)
+ ,m-expr)
+ rest)
rest)))
(else (error "(vikalpa) make-totality-claim: error"
(get-name f)
m-expr))))
''#f)))
-(define (make-condition-claim expr sys)
+(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-conditions f)))
+ (let ((preconds (get-guards f)))
(map (lambda (precond)
(substitute (map cons
(get-variables f)
(cdr expr))
precond))
preconds))))
- (else (error "make-condition-claim: error")))
+ (else (error "make-guard-claim: error" (car expr))))
rest)))
((if-form? expr)
(find-preconds (if-form-test expr)))
@@ -1274,27 +1288,39 @@
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-definition (make <total-function>
- #:name (get-name f)
- #:variables (get-variables f)
- #:conditions (get-conditions f)
- #:expression (get-expression f)
- #:code (get-code f)
- #:claim (make-totality-claim* sys seed f)
- #:proof seq)
- sys))
- (raise-exception
- (make-exception
- (make-exception-with-origin 'define-proof)
- (make-exception-with-message "need seed")
- (make-exception-with-irritants (get-expression f))))))
+ (if (recursive? f)
+ (if seed
+ (begin
+ (validate-expression sys
+ `(defien-proof ,(get-name f))
+ (get-variables f)
+ seed)
+ (update-claim
+ (fold implies/if
+ (and/if (make-totality-claim* sys seed f)
+ (make-guard-claim (get-expression f)
+ sys))
+ (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)))))
+ (update-claim
+ (fold implies/if
+ (make-guard-claim (get-expression f) sys)
+ (get-guards f)))))
(define (add-proof/theorem sys t seed seq)
(validate-sequence sys t seq)
@@ -1451,7 +1477,6 @@
(define-method (get-type (s <core-function>)) 'core-function)
(define-method (get-type (s <function>)) 'function)
(define-method (get-type (s <total-function>)) 'total-function)
-(define-method (get-type (s <trivial-total-function>)) 'trivial-total-function)
(define-method (get-type (s <macro>)) 'macro)
(define-method (show (d <macro>))
@@ -1484,27 +1509,6 @@
#f))
(get-definitions sys)))
-(define (system-code/definition d)
- (and (is-a? d <expandable-function>)
- (get-code d)
- `(define (,(get-name d) ,@(get-variables d))
- ,(code-expr (get-code d)))))
-
-(define/guard (system-code/name (sys system?) (name symbol?))
- (cond
- ((lookup name sys) => system-code/definition)
- (else #f)))
-
-(define/guard (system-code/all (sys system?))
- `(begin
- ,@(filter-map system-code/definition
- (reverse (get-definitions sys)))))
-
-(define* (system-code sys #:optional (name #f))
- (if name
- (system-code/name sys name)
- (system-code/all sys)))
-
(define (system-check sys)
(let loop ((sys sys)
(fails '()))
@@ -1544,14 +1548,5 @@
((lookup name sys) => show)
(else #f)))
-(define/guard (system-load/name (sys system?) (name symbol?))
- (primitive-eval (system-code sys name)))
-
-(define/guard (system-load/all (sys system?))
- (primitive-eval (system-code sys)))
-
-(define/guard (system-load (sys system?))
- (primitive-eval (system-code sys)))
-
(define/guard (system-rewrite (sys system?) (expr (const #t)) (seq sequence?))
(rewrite sys (convert-to-expression expr) seq))
generated by cgit v1.2.3 (git 2.44.0) at 2024-05-19 01:17:57 +0000