123456789101112131415161718192021222324252627282930313233343536373839404142434445464748495051525354555657585960616263646566676869707172737475767778798081828384858687888990919293949596979899100101102103104105106107108109110111112113114115116117118119120121122123124125126127128129130131132133134135136137138139140141142143144145146147148149150151152153154155156157158159160161162163164165166167168169170171172173174175176177178179180181182183184185186187188189190191192193194195196197198199200201202203204205206207208209210211212213214215216217218219220221222223224225226227228229230231232233234235236237238239240241242243244245246247248249250251252253254255256257258259260261262263264265266267268269270271272273274275276277278279280281282283284285286287288289290291292293294295296297298299300301302303304305306307308309310311312313314315316317318319320321322323324325326327328329330331332333334335336337338339340341342343344345346 |
- ;; Suppose we wanted to check assumptions about arguments to
- ;; our function. What kind of form could we write to express
- ;; this?
- ;; (define-with-contract account-withdraw
- ;; (requires (< amount account-balance))
- ;; (ensures (>= account-balance 0))
- ;; (lambda (amount account-balance)
- ;; ...))
- ;; Or abstractly:
- ;; (define-with-contract func
- ;; (requires req-pred* ...)
- ;; (ensures ensure-pred* ...)
- ;; lambda-expr)
- ;; We make a proper module, so that the bindings in this
- ;; module can be imported in other modules. It also allows
- ;; for things like (import (prefix (contract) contract:)),
- ;; which prefixes all things from this module.
- (library (contract)
- (export require
- ensure
- define-with-contract
- define*-with-contract
- lambda-with-contract
- lambda*-with-contract
- λ-with-contract
- λ*-with-contract
- <?>)
- (import
- (except (rnrs base) let-values)
- (only (guile)
- lambda* λ
- syntax-error)
- ;; standard library stuff
- (ice-9 exceptions)
- ;; SRFIs
- (srfi srfi-9 gnu)
- (srfi srfi-1)
- ;; CK style macro stuff
- (ck-base)
- (ck-extra)
- ;; custom exceptions
- (exceptions))
- ;; Define `require` and `ensure`, so that they are
- ;; available as identifiers. This will cause syntax-rules
- ;; to be aware of them as identifiers. When the
- ;; `define-with-contract` macro is used and one writes an
- ;; expression like (require ...), the identifier `require`
- ;; is used, instead of it being pure syntax. The advantage
- ;; is, that the identifier can be renamed, when imported
- ;; in another module. This enables users to change how
- ;; macro call looks. They might want to change `ensure` to
- ;; `make-sure` or `post-condition`, or any other
- ;; renaming. For example like the following import:
- ;; (import
- ;; (rename (contract)
- ;; (require req)
- ;; (ensure ens)))
- ;; Note, that even though `syntax-rules` specifies
- ;; "literals", specifying <?> still works and still allows
- ;; for renaming in another module. Very useful!
- (define require 'require)
- (define ensure 'ensure)
- ;; Using vectors here, because eq? does not return #t for
- ;; (eq? v1 v2). This means only comparing to the same
- ;; object will return #t.
- (define unknown-origin (vector "unknown origin"))
- (define-syntax define-with-contract
- (syntax-rules (require ensure)
- [(_ function-name
- (require reqs* ...)
- (ensure ensu-expr* ...)
- (lambda (args* ...)
- lambda-body-expr* ...))
- (define function-name
- (lambda-with-contract
- function-name
- (require reqs* ...)
- (ensure ensu-expr* ...)
- (args* ...)
- lambda-body-expr* ...))]
- [(_ (function-name args* ...)
- (require reqs* ...)
- (ensure ensu-expr* ...)
- lambda-body-expr* ...)
- (define function-name
- (lambda-with-contract
- function-name
- (require reqs* ...)
- (ensure ensu-expr* ...)
- (args* ...)
- lambda-body-expr* ...))]
- ;; Catch all other cases, including the ones with rest
- ;; arguments.
- [(_ args* ...)
- (define*-with-contract args* ...)]))
- (define-syntax define*-with-contract
- (syntax-rules (require ensure)
- ;; definitions without rest args
- ;; short definition
- [(_ (function-name args* ...)
- (require reqs* ...)
- (ensure ensu-expr* ...)
- lambda-body-expr* ...)
- (define function-name
- (lambda*-with-contract
- function-name
- (require reqs* ...)
- (ensure ensu-expr* ...)
- (args* ...)
- lambda-body-expr* ...))]
- ;; long definition
- [(_ function-name
- (require reqs* ...)
- (ensure ensu-expr* ...)
- (args* ...)
- lambda-body-expr* ...)
- (define function-name
- (lambda*-with-contract
- function-name
- (require reqs* ...)
- (ensure ensu-expr* ...)
- (args* ...)
- lambda-body-expr* ...))]
- ;; definitions with rest args
- ;; shortened definition
- [(_ (function-name args* ... . rest-args)
- (require reqs* ...)
- (ensure ensu-expr* ...)
- lambda-body-expr* ...)
- (define function-name
- (lambda*-with-contract
- function-name
- (require reqs* ...)
- (ensure ensu-expr* ...)
- (args* ... . rest-args)
- lambda-body-expr* ...))]
- ;; long definition
- [(_ function-name
- (require reqs* ...)
- (ensure ensu-expr* ...)
- (args* ... . rest-args)
- lambda-body-expr* ...)
- (define function-name
- (lambda*-with-contract
- function-name
- (require reqs* ...)
- (ensure ensu-expr* ...)
- (args* ... . rest-args)
- lambda-body-expr* ...))]))
- ;; `lambda-with-contract` is implemented in terms of
- ;; `lambda*-with-contract`.
- (define-syntax lambda-with-contract
- (syntax-rules (require ensure)
- ;; CASE 1: A case for when `lambda-with-contract` is
- ;; called without a function name. This should be the
- ;; case, when `lambda-with-contract` is used directly,
- ;; without the indirection through a
- ;; `define-with-contract` call.
- [(_ (require reqs* ...)
- (ensure ensu-expr* ...)
- (args* ...)
- lambda-body-expr* ...)
- ;; Redirect to version with origin, but giving the origin
- ;; `unknown-origin`, since it is unknown.
- (lambda-with-contract unknown-origin
- (require reqs* ...)
- (ensure ensu-expr* ...)
- (args* ...)
- lambda-body-expr* ...)]
- ;; CASE 2: A case for a call with an additional
- ;; function name. In case `lambda-with-contract` is
- ;; called from define-with-contract, it should be
- ;; called with a function name.
- [(_ function-name
- (require reqs* ...)
- (ensure ensu-expr* ...)
- (args* ...)
- lambda-body-expr* ...)
- ;; Redirect to most general case.
- (lambda*-with-contract function-name
- (require reqs* ...)
- (ensure ensu-expr* ...)
- (args* ...)
- lambda-body-expr* ...)]
- ;; Catch all other cases, including the ones with rest
- ;; arguments.
- [(_ args* ...)
- (lambda*-with-contract args* ...)]))
- ;; Example usage:
- ;; ((lambda-with-contract
- ;; (require (> a 0))
- ;; (ensure (> ((λ (res) (+ res 1)) <>) 0))
- ;; (a b)
- ;; (+ a b)) 1 -1)
- ;; `lambda*-with-contract` is the macro, which is the
- ;; entrypoint to calling CK macros. It is also used for
- ;; implementing `lambda-with-contract`,
- ;; `define-with-contract` and `define*-with-contract`.
- (define-syntax lambda*-with-contract
- (syntax-rules (require ensure unknown-origin)
- ;; CASE 1: A case for when `lambda-with-contract` is
- ;; called without a function name. This should be the
- ;; case, when `lambda-with-contract` is used directly,
- ;; without the indirection through a
- ;; `define-with-contract` call. In this case an
- ;; artificial function name is used, which is defined
- ;; above.
- [(_ (require reqs* ...)
- (ensure ensu-expr* ...)
- (args* ...)
- lambda-body-expr* ...)
- ;; If no function-name has been given, call with
- ;; unknown-origin as function name.
- (lambda*-with-contract unknown-origin
- (require reqs* ...)
- (ensure ensu-expr* ...)
- (args* ...)
- lambda-body-expr* ...)]
- ;; CASE 2: A case for a call with an additional
- ;; function name. `lambda-with-contract` should be
- ;; called with function name from a
- ;; define-with-contract call, but not with function
- ;; name, when used directly.
- [(_ function-name
- (require reqs* ...)
- (ensure ensu-expr* ...)
- (args* ...)
- lambda-body-expr* ...)
- (lambda* (args* ...)
- ;; Check, whether the function name is known.
- (let* ([pre-condition-check-result
- ;; Check the requirements (pre-conditions).
- (if (eq? function-name unknown-origin)
- (ck () (c-and-raise
- (quote "unknown origin")
- (c-map '(c-replace-placeholder 'result)
- '(list reqs* ...))))
- (ck () (c-and-raise
- (quote function-name)
- (c-map '(c-replace-placeholder 'result)
- '(list reqs* ...)))))])
- ;; Temporarily store result of the function.
- (let ([result
- ;; Run the actual code of the contracted
- ;; procedure.
- (begin
- lambda-body-expr* ...)])
- (let ([post-condition-check-result
- ;; Check ensured conditions (post-conditions).
- (if (eq? function-name unknown-origin)
- (ck () (c-and-raise
- (quote "unknown origin")
- (c-map '(c-replace-placeholder 'result)
- '(list ensu-expr* ...))))
- (ck () (c-and-raise
- (quote function-name)
- (c-map '(c-replace-placeholder 'result)
- '(list ensu-expr* ...)))))])
- post-condition-check-result)
- ;; Return result, if post-conditions are true.
- result)))]
- ;; Cases for rest arguments.
- [(_ (require reqs* ...)
- (ensure ensu-expr* ...)
- (args* ... . rest-args)
- lambda-body-expr* ...)
- (lambda*-with-contract unknown-origin
- (require reqs* ...)
- (ensure ensu-expr* ...)
- (args* ... . rest-args)
- lambda-body-expr* ...)]
- [(_ function-name
- (require reqs* ...)
- (ensure ensu-expr* ...)
- (args* ... . rest-args)
- lambda-body-expr* ...)
- (lambda* (args* ... . rest-args)
- (let* ([pre-condition-check-result
- (if (eq? function-name unknown-origin)
- (ck () (c-and-raise
- (quote "unknown origin")
- (c-map '(c-replace-placeholder 'result)
- '(list reqs* ...))))
- (ck () (c-and-raise
- (quote function-name)
- (c-map '(c-replace-placeholder 'result)
- '(list reqs* ...)))))])
- (let ([result (begin lambda-body-expr* ...)])
- (let ([post-condition-check-result
- (if (eq? function-name unknown-origin)
- (ck () (c-and-raise
- (quote "unknown origin")
- (c-map '(c-replace-placeholder 'result)
- '(list ensu-expr* ...))))
- (ck () (c-and-raise
- (quote function-name)
- (c-map '(c-replace-placeholder 'result)
- '(list ensu-expr* ...)))))])
- post-condition-check-result)
- result)))]))
- ;; Make λ and λ* aliases for lambda-with-contract and
- ;; lambda*-with-contract.
- (define-syntax λ*-with-contract
- ;; TODO: Are the literaly really needed here?
- (syntax-rules (require ensure unknown-origin)
- [(_ args* ...)
- (lambda*-with-contract args* ...)]))
- (define-syntax λ-with-contract
- ;; TODO: Are the literaly really needed here?
- (syntax-rules (require ensure unknown-origin)
- [(_ args* ...)
- (lambda-with-contract args* ...)])))
|