contract.scm 12 KB

123456789101112131415161718192021222324252627282930313233343536373839404142434445464748495051525354555657585960616263646566676869707172737475767778798081828384858687888990919293949596979899100101102103104105106107108109110111112113114115116117118119120121122123124125126127128129130131132133134135136137138139140141142143144145146147148149150151152153154155156157158159160161162163164165166167168169170171172173174175176177178179180181182183184185186187188189190191192193194195196197198199200201202203204205206207208209210211212213214215216217218219220221222223224225226227228229230231232233234235236237238239240241242243244245246247248249250251252253254255256257258259260261262263264265266267268269270271272273274275276277278279280281282283284285286287288289290291292293294295296297298299300301302303304305306307308309310311312313314315316317318319320321322323324325326327328329330331332333334335336337338339340341342343344345346
  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. ;; We make a proper module, so that the bindings in this
  15. ;; module can be imported in other modules. It also allows
  16. ;; for things like (import (prefix (contract) contract:)),
  17. ;; which prefixes all things from this module.
  18. (library (contract)
  19. (export require
  20. ensure
  21. define-with-contract
  22. define*-with-contract
  23. lambda-with-contract
  24. lambda*-with-contract
  25. λ-with-contract
  26. λ*-with-contract
  27. <?>)
  28. (import
  29. (except (rnrs base) let-values)
  30. (only (guile)
  31. lambda* λ
  32. syntax-error)
  33. ;; standard library stuff
  34. (ice-9 exceptions)
  35. ;; SRFIs
  36. (srfi srfi-9 gnu)
  37. (srfi srfi-1)
  38. ;; CK style macro stuff
  39. (ck-base)
  40. (ck-extra)
  41. ;; custom exceptions
  42. (exceptions))
  43. ;; Define `require` and `ensure`, so that they are
  44. ;; available as identifiers. This will cause syntax-rules
  45. ;; to be aware of them as identifiers. When the
  46. ;; `define-with-contract` macro is used and one writes an
  47. ;; expression like (require ...), the identifier `require`
  48. ;; is used, instead of it being pure syntax. The advantage
  49. ;; is, that the identifier can be renamed, when imported
  50. ;; in another module. This enables users to change how
  51. ;; macro call looks. They might want to change `ensure` to
  52. ;; `make-sure` or `post-condition`, or any other
  53. ;; renaming. For example like the following import:
  54. ;; (import
  55. ;; (rename (contract)
  56. ;; (require req)
  57. ;; (ensure ens)))
  58. ;; Note, that even though `syntax-rules` specifies
  59. ;; "literals", specifying <?> still works and still allows
  60. ;; for renaming in another module. Very useful!
  61. (define require 'require)
  62. (define ensure 'ensure)
  63. ;; Using vectors here, because eq? does not return #t for
  64. ;; (eq? v1 v2). This means only comparing to the same
  65. ;; object will return #t.
  66. (define unknown-origin (vector "unknown origin"))
  67. (define-syntax define-with-contract
  68. (syntax-rules (require ensure)
  69. [(_ function-name
  70. (require reqs* ...)
  71. (ensure ensu-expr* ...)
  72. (lambda (args* ...)
  73. lambda-body-expr* ...))
  74. (define function-name
  75. (lambda-with-contract
  76. function-name
  77. (require reqs* ...)
  78. (ensure ensu-expr* ...)
  79. (args* ...)
  80. lambda-body-expr* ...))]
  81. [(_ (function-name args* ...)
  82. (require reqs* ...)
  83. (ensure ensu-expr* ...)
  84. lambda-body-expr* ...)
  85. (define function-name
  86. (lambda-with-contract
  87. function-name
  88. (require reqs* ...)
  89. (ensure ensu-expr* ...)
  90. (args* ...)
  91. lambda-body-expr* ...))]
  92. ;; Catch all other cases, including the ones with rest
  93. ;; arguments.
  94. [(_ args* ...)
  95. (define*-with-contract args* ...)]))
  96. (define-syntax define*-with-contract
  97. (syntax-rules (require ensure)
  98. ;; definitions without rest args
  99. ;; short definition
  100. [(_ (function-name args* ...)
  101. (require reqs* ...)
  102. (ensure ensu-expr* ...)
  103. lambda-body-expr* ...)
  104. (define function-name
  105. (lambda*-with-contract
  106. function-name
  107. (require reqs* ...)
  108. (ensure ensu-expr* ...)
  109. (args* ...)
  110. lambda-body-expr* ...))]
  111. ;; long definition
  112. [(_ function-name
  113. (require reqs* ...)
  114. (ensure ensu-expr* ...)
  115. (args* ...)
  116. lambda-body-expr* ...)
  117. (define function-name
  118. (lambda*-with-contract
  119. function-name
  120. (require reqs* ...)
  121. (ensure ensu-expr* ...)
  122. (args* ...)
  123. lambda-body-expr* ...))]
  124. ;; definitions with rest args
  125. ;; shortened definition
  126. [(_ (function-name args* ... . rest-args)
  127. (require reqs* ...)
  128. (ensure ensu-expr* ...)
  129. lambda-body-expr* ...)
  130. (define function-name
  131. (lambda*-with-contract
  132. function-name
  133. (require reqs* ...)
  134. (ensure ensu-expr* ...)
  135. (args* ... . rest-args)
  136. lambda-body-expr* ...))]
  137. ;; long definition
  138. [(_ function-name
  139. (require reqs* ...)
  140. (ensure ensu-expr* ...)
  141. (args* ... . rest-args)
  142. lambda-body-expr* ...)
  143. (define function-name
  144. (lambda*-with-contract
  145. function-name
  146. (require reqs* ...)
  147. (ensure ensu-expr* ...)
  148. (args* ... . rest-args)
  149. lambda-body-expr* ...))]))
  150. ;; `lambda-with-contract` is implemented in terms of
  151. ;; `lambda*-with-contract`.
  152. (define-syntax lambda-with-contract
  153. (syntax-rules (require ensure)
  154. ;; CASE 1: A case for when `lambda-with-contract` is
  155. ;; called without a function name. This should be the
  156. ;; case, when `lambda-with-contract` is used directly,
  157. ;; without the indirection through a
  158. ;; `define-with-contract` call.
  159. [(_ (require reqs* ...)
  160. (ensure ensu-expr* ...)
  161. (args* ...)
  162. lambda-body-expr* ...)
  163. ;; Redirect to version with origin, but giving the origin
  164. ;; `unknown-origin`, since it is unknown.
  165. (lambda-with-contract unknown-origin
  166. (require reqs* ...)
  167. (ensure ensu-expr* ...)
  168. (args* ...)
  169. lambda-body-expr* ...)]
  170. ;; CASE 2: A case for a call with an additional
  171. ;; function name. In case `lambda-with-contract` is
  172. ;; called from define-with-contract, it should be
  173. ;; called with a function name.
  174. [(_ function-name
  175. (require reqs* ...)
  176. (ensure ensu-expr* ...)
  177. (args* ...)
  178. lambda-body-expr* ...)
  179. ;; Redirect to most general case.
  180. (lambda*-with-contract function-name
  181. (require reqs* ...)
  182. (ensure ensu-expr* ...)
  183. (args* ...)
  184. lambda-body-expr* ...)]
  185. ;; Catch all other cases, including the ones with rest
  186. ;; arguments.
  187. [(_ args* ...)
  188. (lambda*-with-contract args* ...)]))
  189. ;; Example usage:
  190. ;; ((lambda-with-contract
  191. ;; (require (> a 0))
  192. ;; (ensure (> ((λ (res) (+ res 1)) <>) 0))
  193. ;; (a b)
  194. ;; (+ a b)) 1 -1)
  195. ;; `lambda*-with-contract` is the macro, which is the
  196. ;; entrypoint to calling CK macros. It is also used for
  197. ;; implementing `lambda-with-contract`,
  198. ;; `define-with-contract` and `define*-with-contract`.
  199. (define-syntax lambda*-with-contract
  200. (syntax-rules (require ensure unknown-origin)
  201. ;; CASE 1: A case for when `lambda-with-contract` is
  202. ;; called without a function name. This should be the
  203. ;; case, when `lambda-with-contract` is used directly,
  204. ;; without the indirection through a
  205. ;; `define-with-contract` call. In this case an
  206. ;; artificial function name is used, which is defined
  207. ;; above.
  208. [(_ (require reqs* ...)
  209. (ensure ensu-expr* ...)
  210. (args* ...)
  211. lambda-body-expr* ...)
  212. ;; If no function-name has been given, call with
  213. ;; unknown-origin as function name.
  214. (lambda*-with-contract unknown-origin
  215. (require reqs* ...)
  216. (ensure ensu-expr* ...)
  217. (args* ...)
  218. lambda-body-expr* ...)]
  219. ;; CASE 2: A case for a call with an additional
  220. ;; function name. `lambda-with-contract` should be
  221. ;; called with function name from a
  222. ;; define-with-contract call, but not with function
  223. ;; name, when used directly.
  224. [(_ function-name
  225. (require reqs* ...)
  226. (ensure ensu-expr* ...)
  227. (args* ...)
  228. lambda-body-expr* ...)
  229. (lambda* (args* ...)
  230. ;; Check, whether the function name is known.
  231. (let* ([pre-condition-check-result
  232. ;; Check the requirements (pre-conditions).
  233. (if (eq? function-name unknown-origin)
  234. (ck () (c-and-raise
  235. (quote "unknown origin")
  236. (c-map '(c-replace-placeholder 'result)
  237. '(list reqs* ...))))
  238. (ck () (c-and-raise
  239. (quote function-name)
  240. (c-map '(c-replace-placeholder 'result)
  241. '(list reqs* ...)))))])
  242. ;; Temporarily store result of the function.
  243. (let ([result
  244. ;; Run the actual code of the contracted
  245. ;; procedure.
  246. (begin
  247. lambda-body-expr* ...)])
  248. (let ([post-condition-check-result
  249. ;; Check ensured conditions (post-conditions).
  250. (if (eq? function-name unknown-origin)
  251. (ck () (c-and-raise
  252. (quote "unknown origin")
  253. (c-map '(c-replace-placeholder 'result)
  254. '(list ensu-expr* ...))))
  255. (ck () (c-and-raise
  256. (quote function-name)
  257. (c-map '(c-replace-placeholder 'result)
  258. '(list ensu-expr* ...)))))])
  259. post-condition-check-result)
  260. ;; Return result, if post-conditions are true.
  261. result)))]
  262. ;; Cases for rest arguments.
  263. [(_ (require reqs* ...)
  264. (ensure ensu-expr* ...)
  265. (args* ... . rest-args)
  266. lambda-body-expr* ...)
  267. (lambda*-with-contract unknown-origin
  268. (require reqs* ...)
  269. (ensure ensu-expr* ...)
  270. (args* ... . rest-args)
  271. lambda-body-expr* ...)]
  272. [(_ function-name
  273. (require reqs* ...)
  274. (ensure ensu-expr* ...)
  275. (args* ... . rest-args)
  276. lambda-body-expr* ...)
  277. (lambda* (args* ... . rest-args)
  278. (let* ([pre-condition-check-result
  279. (if (eq? function-name unknown-origin)
  280. (ck () (c-and-raise
  281. (quote "unknown origin")
  282. (c-map '(c-replace-placeholder 'result)
  283. '(list reqs* ...))))
  284. (ck () (c-and-raise
  285. (quote function-name)
  286. (c-map '(c-replace-placeholder 'result)
  287. '(list reqs* ...)))))])
  288. (let ([result (begin lambda-body-expr* ...)])
  289. (let ([post-condition-check-result
  290. (if (eq? function-name unknown-origin)
  291. (ck () (c-and-raise
  292. (quote "unknown origin")
  293. (c-map '(c-replace-placeholder 'result)
  294. '(list ensu-expr* ...))))
  295. (ck () (c-and-raise
  296. (quote function-name)
  297. (c-map '(c-replace-placeholder 'result)
  298. '(list ensu-expr* ...)))))])
  299. post-condition-check-result)
  300. result)))]))
  301. ;; Make λ and λ* aliases for lambda-with-contract and
  302. ;; lambda*-with-contract.
  303. (define-syntax λ*-with-contract
  304. ;; TODO: Are the literaly really needed here?
  305. (syntax-rules (require ensure unknown-origin)
  306. [(_ args* ...)
  307. (lambda*-with-contract args* ...)]))
  308. (define-syntax λ-with-contract
  309. ;; TODO: Are the literaly really needed here?
  310. (syntax-rules (require ensure unknown-origin)
  311. [(_ args* ...)
  312. (lambda-with-contract args* ...)])))