Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

examples/contract: Simple function contracts #67

Merged
merged 2 commits into from
May 5, 2020
Merged
Show file tree
Hide file tree
Changes from all commits
Commits
File filter

Filter by extension

Filter by extension

Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
5 changes: 5 additions & 0 deletions examples/contract.golden
Original file line number Diff line number Diff line change
@@ -0,0 +1,5 @@
#<closure> : (Syntax → Syntax)
#<closure> : (Syntax → (Syntax → (Syntax → (Macro Syntax))))
#<closure> : (Syntax → (Syntax → (Syntax → (Macro Syntax))))
#<closure> : ∀α. (α → α)
(true) : Bool
78 changes: 78 additions & 0 deletions examples/contract.kl
Original file line number Diff line number Diff line change
@@ -0,0 +1,78 @@
#lang "n-ary-app.kl"
[import "defun.kl"]
[import "bool.kl"]
[import [shift "n-ary-app.kl" 1]]
[import [shift "defun.kl"1]]

(meta
(defun contract-violation (contract)
(list-syntax ('error (quote '"Contract violation!")) contract)))

(meta -- type annotation
langston-barrett marked this conversation as resolved.
Show resolved Hide resolved
(example (the (-> Syntax Syntax)
contract-violation)))

(meta
(defun enforce-single (arg contract body)
(pure
(list-syntax
('if
(list-syntax (contract arg) contract)
body
(contract-violation contract))
contract))))

(meta -- type annotation
(example (the (-> Syntax (-> Syntax (-> Syntax (Macro Syntax))))
enforce-single)))

(meta
(defun enforce-many (args contracts body)
(syntax-case args
[(cons arg more-args)
(syntax-case contracts
[(cons contract more-contracts)
(>>= (enforce-single arg contract body)
(lambda (new-body)
(enforce-many
more-args
more-contracts
new-body)))]
[_ (syntax-error '"Wrong number of contracts" contracts)])]
[()
(syntax-case contracts
[(list (ret-contract))
(pure
(list-syntax
-- TODO: This is inefficient, use a let-binding
('if
(list-syntax (ret-contract body) ret-contract)
body
(contract-violation ret-contract))
ret-contract))]
[_ (syntax-error '"Wrong number of contracts" contracts)])])))

(meta -- type annotation
(example (the (-> Syntax (-> Syntax (-> Syntax (Macro Syntax))))
enforce-many)))

(define-macros
([defun/contract
[lambda (stx)
(syntax-case stx
[[list [_ f args contracts body]]
(>>= (enforce-many args contracts body)
(lambda (new-body)
(pure
(list-syntax
('defun f args new-body)
stx))))]
[_ (syntax-error '"bad syntax" stx)])]]))

(defun const (x y) x)
(define any (const (true)))
(defun true? (b) (if b (true) (false)))
langston-barrett marked this conversation as resolved.
Show resolved Hide resolved
(defun/contract id (x) (any any) x)
(defun/contract id-bool (x) (true? true?) x)
(example (id id))
(example (id-bool (true)))
1 change: 1 addition & 0 deletions examples/n-ary-app.kl
Original file line number Diff line number Diff line change
Expand Up @@ -114,6 +114,7 @@

(export #%module #%app
const lambda define example define-macros quote meta
the -> Syntax Macro
if true false
error
let flet
Expand Down