Make static contracts catch simple parametric contract errors.

This commit is contained in:
Eric Dobson 2014-01-07 21:21:20 -08:00
parent 6deb1e3193
commit 497a7faa83
5 changed files with 57 additions and 17 deletions

View File

@ -250,7 +250,7 @@
(let ((temporaries (generate-temporaries vs-nm)))
(define rv (for/fold ((rv recursive-values)) ((temp temporaries)
(v-nm vs-nm))
(hash-set rv v-nm (same (impersonator/sc temp)))))
(hash-set rv v-nm (same (parametric-var/sc temp)))))
(parametric->/sc temporaries
(t->sc b #:recursive-values rv)))))]
[(Mu: n b)

View File

@ -2,17 +2,23 @@
;; Static contract for parametric->/c.
(require "../structures.rkt" "../constraints.rkt"
racket/list racket/match
unstable/contract
(except-in racket/contract recursive-contract)
(for-template racket/base racket/contract/parametric)
(for-syntax racket/base syntax/parse))
(require
"../structures.rkt"
"../constraints.rkt"
"../terminal.rkt"
racket/list racket/match
unstable/contract
(except-in racket/contract recursive-contract)
(for-template racket/base racket/contract/parametric)
(for-syntax racket/base syntax/parse))
(provide
(contract-out
[parametric->/sc ((listof identifier?) static-contract? . -> . static-contract?)])
parametric->/sc:)
[parametric->/sc ((listof identifier?) static-contract? . -> . static-contract?)]
[parametric-var/sc (identifier? . -> . static-contract?)])
parametric->/sc:
(rename-out
[parametric-var/sc parametric-var/sc:]))
(struct parametric-combinator combinator (vars)
@ -44,3 +50,6 @@
(syntax-parser
[(_ vars body)
#'(parametric-combinator (list body) vars)]))
(define-terminal-sc parametric-var/sc (id) #:impersonator
id)

View File

@ -9,6 +9,7 @@
racket/sequence
(for-template racket/base (prefix-in c: racket/contract))
"kinds.rkt"
"parametric-check.rkt"
"structures.rkt"
"constraints.rkt"
"equations.rkt")
@ -29,11 +30,13 @@
;; kind is the greatest kind of contract that is supported, if a greater kind would be produced the
;; fail procedure is called.
(define (instantiate sc fail [kind 'impersonator])
(with-handlers [(exn:fail:constraint-failure?
(lambda (exn) (fail #:reason (exn:fail:constraint-failure-reason exn))))]
(instantiate/inner sc
(compute-recursive-kinds
(contract-restrict-recursive-values (compute-constraints sc kind))))))
(if (parametric-check sc)
(fail #:reason "multiple parametric contracts are not supported")
(with-handlers [(exn:fail:constraint-failure?
(lambda (exn) (fail #:reason (exn:fail:constraint-failure-reason exn))))]
(instantiate/inner sc
(compute-recursive-kinds
(contract-restrict-recursive-values (compute-constraints sc kind)))))))
(define (compute-constraints sc max-kind)
(define (recur sc)

View File

@ -0,0 +1,26 @@
#lang racket/base
(require
racket/match
racket/contract
(except-in "structures.rkt" recursive-contract)
"combinators/parametric.rkt"
"combinators/structural.rkt")
(provide
(contract-out
[parametric-check (static-contract? . -> . boolean?)]))
(define (parametric-check sc)
(let/ec exit
(define (recur sc variance)
(match sc
[(or/sc: elems ...) (=> continue)
(match elems
[(list-no-order (parametric-var/sc: _) (parametric-var/sc: _) others ...)
(exit #t)]
[else (continue)])]
[else
(sc-traverse sc recur)]))
(recur sc 'covariant)
#f))

View File

@ -41,10 +41,8 @@
;; Polydotted functions should work
(t/fail (-polydots (a) (->... (list) (a a) -Symbol))
"not supported for this type")
"not supported for this type")))
;; These should fail
(t (-> (-poly (a b) (-> (Un a b) (Un a b))) Univ))))
@ -73,6 +71,10 @@
(t/fail ((-poly (a) (-vec a)) . -> . -Symbol)
"cannot generate contract for non-function polymorphic type")
(t/fail (-> (-poly (a b) (-> (Un a b) (Un a b))) Univ)
"multiple parametric contracts are not supported")
(t/fail
(make-Function
(list (make-arr* (list) -Boolean #:kws (list (make-Keyword '#:key Univ #f)))