contract.scm 3.9 KB

123456789101112131415161718192021222324252627282930313233343536373839404142434445464748495051525354555657585960616263646566676869707172737475767778798081828384858687888990919293949596979899100101102103104105106107108109110111112113114115116117118119120
  1. ;; Suppose we wanted to check assumptions about arguments to
  2. ;; our function. What kind of form could we write to express
  3. ;; this?
  4. ;; (define-with-contract account-withdraw
  5. ;; (requires (< amount account-balance))
  6. ;; (ensures (>= account-balance 0))
  7. ;; (lambda (amount account-balance)
  8. ;; ...))
  9. ;; Or abstractly:
  10. ;; (define-with-contract func
  11. ;; (requires req-pred* ...)
  12. ;; (ensures ensure-pred* ...)
  13. ;; lambda-expr)
  14. (import
  15. (except (rnrs base) let-values)
  16. (only (guile)
  17. lambda* λ)
  18. (ice-9 exceptions)
  19. (srfi srfi-1))
  20. ;; and-raise needs to be a macro, because its arguments must
  21. ;; not be immediately evaluated, otherwise we cannot raise
  22. ;; an exception containing the failing check.
  23. (define-syntax and-raise
  24. (syntax-rules ()
  25. [(_ (op args* ...) check-expr* ...)
  26. (cond
  27. [(not (op args* ...))
  28. (raise-exception
  29. (make-exception
  30. (make-assertion-failure)
  31. (make-exception-with-message "assertion failed")
  32. (make-exception-with-irritants (quote (op args* ...)))))]
  33. [else
  34. (and-raise check-expr* ...)])]
  35. [(_ #|nothing|#)
  36. #t]))
  37. ;; `ensure` builds up an `and` expression, which contains
  38. ;; all the conditions.
  39. (define-syntax ensure-with-result
  40. (syntax-rules (ensure)
  41. [(_ identifier expr* ... (op args* ...))
  42. (and-raise
  43. ;; insert identifier on the left
  44. (op identifier args* ...)
  45. (ensure-with-result identifier expr* ...))]
  46. ;; If there is only one more ensure clause, transform
  47. ;; it, and do not place another macro call.
  48. [(_ identifier (op args* ...))
  49. ;; insert identifier on the left
  50. (op identifier args* ...)]
  51. ;; If there are no more ensure clauses, transform to
  52. ;; `#t`, the neutral element of `and`.
  53. [(_ identifier)
  54. #t]))
  55. (define-syntax define-with-contract
  56. (syntax-rules (require ensure <?>)
  57. ;; first process ensure (post-conditions)
  58. [(_ function-name
  59. (require reqs* ...)
  60. (ensure ensu-expr* ...)
  61. (lambda (args* ...)
  62. lambda-body-expr* ...))
  63. (define function-name
  64. (lambda (args* ...)
  65. ;; temporarily store result of the function
  66. (let ([result
  67. (cond
  68. ;; check pre-conditions (requirements)
  69. [(not (and-raise reqs* ...))
  70. (raise-exception
  71. (make-exception
  72. (make-assertion-failure)
  73. (make-exception-with-message "assertion failed")
  74. (make-exception-with-irritants (list args* ...))
  75. (make-exception-with-origin (syntax->datum function-name))))]
  76. ;; otherwise run the body
  77. [else
  78. lambda-body-expr* ...])])
  79. (cond
  80. ;; check post-conditions (ensures)
  81. [(not (ensure-with-result result ensu-expr* ...))
  82. ;; Problem: Cannot know which post-condition
  83. ;; failed. Could be improved.
  84. (raise-exception
  85. (make-exception
  86. (make-assertion-failure)
  87. (make-exception-with-message "assertion failed")
  88. (make-exception-with-irritants (list args* ...))
  89. (make-exception-with-origin (syntax->datum function-name))))]
  90. ;; return result if post conditions are true
  91. [else result]))))]))
  92. ;; Lets make an example definition: Withdrawing an amount of
  93. ;; money from an account, returning the new account balance
  94. ;; (although not really mutating the account or anything,
  95. ;; really just a toy example).
  96. (define-with-contract account-withdraw
  97. (require (< amount account-balance)
  98. (>= amount 0))
  99. (ensure (>= 0)) ; depends on what the function returns
  100. (lambda (amount account-balance)
  101. (- account-balance amount)))
  102. ;; Using the defined function just like any other function.
  103. (display (account-withdraw 10 20)) (newline)
  104. (display (account-withdraw 30 20)) (newline)