Skip to content

HTTPS clone URL

Subversion checkout URL

You can clone with
or
.
Download ZIP

Loading…

Fix type->contract on structures. Now uses struct/c. #139

Closed
wants to merge 5 commits into from

3 participants

@endobson

This is still not complete. It fails on one test case, fail/pr11686.rkt.

The issue is that the constraint on what kind of contract we need to produce can come from multiple places.
For a immutable struct contract we need that each field is a chaperone contract. Any type which contains an Univ type on the typed side will produce a impersonator contract due to any-wrap. The issue is when we need to make a recursive contract for a Mu type. We need to make it a impersonator contract if it contains an Univ, and we need to make it a chaperone contract if a struct type uses its recursive id in a chaperone only context.

My current solution is to just assume that structs won't use the contract recursively, which is why it fails the test case. The correct solution is to see if it is used in any place where it needs to be a chaperone and then make it a chaperone, otherwise make it an impersonator.

On a side note, I don't see what any-wrap/c protects against. Why cannot it be any/c?

@samth
Collaborator
@endobson
@samth
Collaborator

Right, the problem is due to a weak type in that case. But TR can't just let there be a dynamic error in the typed part of the program, even if a weak type is used.

@endobson

This is still failing some test cases, but I am pretty sure it is because of pr 13090.

I added a parameter which is the current kind of contract, this is for bottom up restrictions (i.e. -> contracts must be chaperones) versus the argument which is a top down restriction (i.e. key contracts must be a chaperone-contract). This seemed cleaner than adding an extra return value.

This is still broken in a couple cases, but they are smaller than before. And it is just that the error is caught when constructing the contract instead of when constructing the syntax of the contract. The issue is that free variables are not checked to make sure they are used in a valid context. Thus if they are used in a context that requires them to be chaperone contracts, but are bound to a value that requires them to be impersonator contracts the error happens at runtime. Should I fix that in this pull request?

;; tmp.rkt
#lang typed/racket/base

(define-type T (Rec r (-> (U (All (a) (a -> Symbol)) (HashTable r Symbol)))))
(: a T)
(: b T)
(define (b) (plambda: (a) ((x : a)) 'y))
(define (a) (make-hash (list (cons b 'sym))))
(: f (T -> Void))
(define (f x) (void))

(provide a f)

;; tmp2.rkt
#lang racket

(require "tmp.rkt")

(f (hash a 'sym))

@samth
Collaborator

Ok, I'm back on this, trying to figure out what's going on in PR 13090.

@samth
Collaborator

And 13090 is now fixed, so I'll get to merging this.

@samth
Collaborator

This currently has two genuine errors:

--------------------
Typed Racket Tests > Integration tests > succeed > pr10939.rkt > #f
Unnamed test 
FAILURE
message:    "Exception raised"
ssage: "a:empty?: undefined;\n cannot reference an identifier before its definition\n  in module: \"/home/samth/sw/plt/collects/tests/typed-racket/succeed/pr10939.rkt\""
exception:  #(struct:exn:fail:contract "a:empty?: undefined;\n cannot reference an identifier before its definition\n  in module: \"/home/samth/sw/plt/collects/tests/typed-racket/succeed/pr10939.rkt\"" #<continuation-mark-set>)
name:       check-not-exn
location:   main.rkt:81:31
expression: (check-not-exn thnk)
params:     #<procedure:...-racket/main.rkt:73:10>

Check failure
--------------------
--------------------
Typed Racket Tests > Integration tests > succeed > pr11504.rkt > #f
Unnamed test 
FAILURE
message:    "Exception raised"
ssage: "cat?: undefined;\n cannot reference an identifier before its definition\n  in module: \"/home/samth/sw/plt/collects/tests/typed-racket/succeed/pr11504.rkt\""
exception:  #(struct:exn:fail:contract "cat?: undefined;\n cannot reference an identifier before its definition\n  in module: \"/home/samth/sw/plt/collects/tests/typed-racket/succeed/pr11504.rkt\"" #<continuation-mark-set>)
name:       check-not-exn
location:   main.rkt:81:31
expression: (check-not-exn thnk)
params:     #<procedure:...-racket/main.rkt:73:10>

Check failure
--------------------

I'm looking into it.

@samth
Collaborator

This was merged as part of #143.

@elibarzilay elibarzilay closed this
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
This page is out of date. Refresh to see the latest.
Showing with 188 additions and 134 deletions.
  1. +23 −0 collects/tests/typed-racket/succeed/contract-struct-equality.rkt
  2. +9 −1 collects/tests/typed-racket/unit-tests/contract-tests.rkt
  3. +7 −8 collects/tests/typed-racket/unit-tests/subtype-tests.rkt
  4. +2 −3 collects/tests/typed-racket/unit-tests/type-equal-tests.rkt
  5. +1 −1  collects/typed-racket/base-env/prims.rkt
  6. +2 −3 collects/typed-racket/env/init-envs.rkt
  7. +2 −2 collects/typed-racket/infer/infer-unit.rkt
  8. +1 −1  collects/typed-racket/private/parse-type.rkt
  9. +95 −63 collects/typed-racket/private/type-contract.rkt
  10. +3 −8 collects/typed-racket/rep/type-rep.rkt
  11. +1 −1  collects/typed-racket/typecheck/signatures.rkt
  12. +2 −1  collects/typed-racket/typecheck/tc-app/signatures.rkt
  13. +2 −2 collects/typed-racket/typecheck/tc-app/tc-app-hetero.rkt
  14. +4 −4 collects/typed-racket/typecheck/tc-envops.rkt
  15. +1 −1  collects/typed-racket/typecheck/tc-funapp.rkt
  16. +6 −8 collects/typed-racket/typecheck/tc-structs.rkt
  17. +2 −2 collects/typed-racket/types/abbrev.rkt
  18. +2 −2 collects/typed-racket/types/printer.rkt
  19. +12 −12 collects/typed-racket/types/remove-intersect.rkt
  20. +11 −11 collects/typed-racket/types/subtype.rkt
View
23 collects/tests/typed-racket/succeed/contract-struct-equality.rkt
@@ -0,0 +1,23 @@
+#lang racket/load
+
+(module typed typed/racket
+ (provide g)
+ (struct: (A) foo ((v : A)))
+ (: f (foo Byte))
+ (define f (foo 2))
+ (: g (-> (foo Byte)))
+ (define (g) f))
+
+(module typed-client typed/racket
+ (require 'typed)
+ (unless (equal? (g) (g))
+ (error 'typed2 "Failed")))
+
+
+(module untyped-client racket
+ (require 'typed)
+ (unless (equal? (g) (g))
+ (error 'typed2 "Failed")))
+
+(require 'typed-client)
+(require 'untyped-client)
View
10 collects/tests/typed-racket/unit-tests/contract-tests.rkt
@@ -10,10 +10,18 @@
(define-syntax-rule (t e)
(test-not-exn (format "~a" e) (lambda () (type->contract e (lambda _ (error "type could not be converted to contract"))))))
+(define-syntax-rule (t/fail e)
+ (test-not-exn (format "~a" e) (lambda ()
+ (let/ec exit
+ (type->contract e (lambda _ (exit #t)))
+ (error "type could be converted to contract")))))
+
(define (contract-tests)
(test-suite "Contract Tests"
(t (-Number . -> . -Number))
- (t (-Promise -Number))))
+ (t (-Promise -Number))
+ (t/fail (-set Univ))
+ ))
(define-go contract-tests)
(provide contract-tests)
View
15 collects/tests/typed-racket/unit-tests/subtype-tests.rkt
@@ -118,13 +118,12 @@
[(-poly (b) ((Un (make-Base 'foo #'dummy values #'values #f)
(-struct #'bar #f
- (list (make-fld -Number #'values #f) (make-fld b #'values #f))
- #'values))
+ (list (make-fld -Number #'values #f) (make-fld b #'values #f))))
. -> . (-lst b)))
- ((Un (make-Base 'foo #'dummy values #'values #f) (-struct #'bar #f (list (make-fld -Number #'values #f) (make-fld (-pair -Number (-v a)) #'values #f)) #'values))
+ ((Un (make-Base 'foo #'dummy values #'values #f) (-struct #'bar #f (list (make-fld -Number #'values #f) (make-fld (-pair -Number (-v a)) #'values #f))))
. -> . (-lst (-pair -Number (-v a))))]
- [(-poly (b) ((-struct #'bar #f (list (make-fld -Number #'values #f) (make-fld b #'values #f)) #'values) . -> . (-lst b)))
- ((-struct #'bar #f (list (make-fld -Number #'values #f) (make-fld (-pair -Number (-v a)) #'values #f)) #'values) . -> . (-lst (-pair -Number (-v a))))]
+ [(-poly (b) ((-struct #'bar #f (list (make-fld -Number #'values #f) (make-fld b #'values #f))) . -> . (-lst b)))
+ ((-struct #'bar #f (list (make-fld -Number #'values #f) (make-fld (-pair -Number (-v a)) #'values #f))) . -> . (-lst (-pair -Number (-v a))))]
[(-poly (a) (a . -> . (make-Listof a))) ((-v b) . -> . (make-Listof (-v b)))]
[(-poly (a) (a . -> . (make-Listof a))) ((-pair -Number (-v b)) . -> . (make-Listof (-pair -Number (-v b))))]
@@ -136,9 +135,9 @@
(FAIL (-> Univ) (null Univ . ->* . Univ))
[(cl->* (-Number . -> . -String) (-Boolean . -> . -String)) ((Un -Boolean -Number) . -> . -String)]
- [(-struct #'a #f null #'values) (-struct #'a #f null #'values)]
- [(-struct #'a #f (list (make-fld -String #'values #f)) #'values) (-struct #'a #f (list (make-fld -String #'values #f)) #'values)]
- [(-struct #'a #f (list (make-fld -String #'values #f)) #'values) (-struct #'a #f (list (make-fld Univ #'values #f)) #'values)]
+ [(-struct #'a #f null) (-struct #'a #f null)]
+ [(-struct #'a #f (list (make-fld -String #'values #f))) (-struct #'a #f (list (make-fld -String #'values #f)))]
+ [(-struct #'a #f (list (make-fld -String #'values #f))) (-struct #'a #f (list (make-fld Univ #'values #f)))]
))
(define-go
View
5 collects/tests/typed-racket/unit-tests/type-equal-tests.rkt
@@ -40,12 +40,11 @@
;; found bug
[FAIL (Un (-mu heap-node
(-struct #'heap-node #f
- (map fld* (list (-base 'comparator) -Number (-v a) (Un heap-node (-base 'heap-empty))))
- #'values))
+ (map fld* (list (-base 'comparator) -Number (-v a) (Un heap-node (-base 'heap-empty))))))
(-base 'heap-empty))
(Un (-mu heap-node
(-struct #'heap-node #f
- (map fld* (list (-base 'comparator) -Number (-pair -Number -Number) (Un heap-node (-base 'heap-empty)))) #'values))
+ (map fld* (list (-base 'comparator) -Number (-pair -Number -Number) (Un heap-node (-base 'heap-empty))))))
(-base 'heap-empty))]))
(define-go
View
2  collects/typed-racket/base-env/prims.rkt
@@ -223,7 +223,7 @@ This file defines two sorts of primitives. All of them are provided into any mod
(type->contract
typ
;; must be a flat contract
- #:flat #t
+ #:kind 'flat
;; the value is not from the typed side
#:typed-side #f
(lambda () (tc-error/stx #'ty "Type ~a could not be converted to a predicate." typ)))
View
5 collects/typed-racket/env/init-envs.rkt
@@ -28,11 +28,10 @@
[(Base: n cnt pred marshaled _) marshaled]
[(Name: stx) `(make-Name (quote-syntax ,stx))]
[(fld: t acc mut) `(make-fld ,(sub t) (quote-syntax ,acc) ,mut)]
- [(Struct: name parent flds proc poly? pred-id cert maker-id)
+ [(Struct: name parent flds proc poly? pred-id)
`(make-Struct (quote-syntax ,name) ,(sub parent)
,(sub flds) ,(sub proc) ,(sub poly?)
- (quote-syntax ,pred-id) (syntax-local-certifier)
- (quote-syntax ,maker-id))]
+ (quote-syntax ,pred-id))]
[(App: rator rands stx) `(make-App ,(sub rator) ,(sub rands) (quote-syntax ,stx))]
[(Opaque: pred cert) `(make-Opaque (quote-syntax ,pred) (syntax-local-certifier))]
[(Refinement: parent pred cert) `(make-Refinement ,(sub parent)
View
4 collects/typed-racket/infer/infer-unit.rkt
@@ -423,7 +423,7 @@
;; two structs with the same name
;; just check pairwise on the fields
- [((Struct: nm _ flds proc _ _ _ _) (Struct: nm* _ flds* proc* _ _ _ _)) (=> nevermind)
+ [((Struct: nm _ flds proc _ _) (Struct: nm* _ flds* proc* _ _)) (=> nevermind)
(unless (free-identifier=? nm nm*) (nevermind))
(let ([proc-c
(cond [(and proc proc*)
@@ -520,7 +520,7 @@
;; If the struct names don't match, try the parent of S
;; Needs to be done after App and Mu in case T is actually the current struct
;; but not currently visible
- [((Struct: nm (? Type? parent) _ _ _ _ _ _) other)
+ [((Struct: nm (? Type? parent) _ _ _ _) other)
(cg parent other)]
;; vectors are invariant - generate constraints *both* ways
View
2  collects/typed-racket/private/parse-type.rkt
@@ -166,7 +166,7 @@
(add-disappeared-use #'kw)
(let ([v (parse-type #'t)])
(match (resolve v)
- [(and s (Struct: _ _ _ _ _ _ _ _)) (make-StructTop s)]
+ [(and s Struct?) (make-StructTop s)]
[_ (tc-error/delayed "Argument to Struct must be a structure type, got ~a" v)
(make-Instance (Un))]))]
[((~and kw t:Instance) t)
View
158 collects/typed-racket/private/type-contract.rkt
@@ -57,9 +57,9 @@
typ
;; this is for a `require/typed', so the value is not from the typed side
#:typed-side #f
- #:flat flat?
+ #:kind (if flat? 'flat 'impersonator)
(lambda () (tc-error/stx prop "Type ~a could not be converted to a contract." typ)))])
- (quasisyntax/loc stx (define-values (n) (recursive-contract cnt #,(if flat? #'#:flat #'#:impersonator))))))]
+ (quasisyntax/loc stx (define-values (n) cnt))))]
[_ (int-err "should never happen - not a define-values: ~a" (syntax->datum stx))]))
(define (change-contract-fixups forms)
@@ -72,20 +72,54 @@
(define (no-duplicates l)
(= (length l) (length (remove-duplicates l))))
+;; To avoid misspellings
+(define impersonator-sym 'impersonator)
+(define chaperone-sym 'chaperone)
+(define flat-sym 'flat)
-(define (type->contract ty fail #:out [out? #f] #:typed-side [from-typed? #t] #:flat [flat? #f])
+(define (contract-kind-max . args)
+ (define (contract-kind-max2 x y)
+ (cond
+ ((equal? flat-sym x) y)
+ ((equal? flat-sym y) x)
+ ((equal? chaperone-sym x) y)
+ ((equal? chaperone-sym y) x)
+ (else impersonator-sym)))
+ (for/fold ((acc flat-sym)) ((v args))
+ (contract-kind-max2 v acc)))
+
+
+(define (contract-kind-min . args)
+ (define (contract-kind-min2 x y)
+ (cond
+ ((equal? flat-sym x) x)
+ ((equal? flat-sym y) y)
+ ((equal? chaperone-sym x) x)
+ ((equal? chaperone-sym y) y)
+ (else impersonator-sym)))
+ (for/fold ((acc flat-sym)) ((v args))
+ (contract-kind-min2 v acc)))
+
+
+(define (contract-kind->keyword sym)
+ (string->keyword (symbol->string sym)))
+
+(define (type->contract ty fail #:out [out? #f] #:typed-side [from-typed? #t] #:kind [kind 'impersonator])
(define vars (make-parameter '()))
+ (define current-contract-kind (make-parameter flat-sym))
+ (define (increase-current-contract-kind! kind)
+ (current-contract-kind (contract-kind-max (current-contract-kind) kind)))
(let/ec exit
- (let loop ([ty ty] [pos? #t] [from-typed? from-typed?] [structs-seen null] [flat? flat?])
- (define (t->c t #:seen [structs-seen structs-seen] #:flat [flat? flat?])
- (loop t pos? from-typed? structs-seen flat?))
- (define (t->c/neg t #:seen [structs-seen structs-seen] #:flat [flat? flat?])
- (loop t (not pos?) (not from-typed?) structs-seen flat?))
+ (let loop ([ty ty] [pos? #t] [from-typed? from-typed?] [structs-seen null] [kind kind])
+ (define (t->c t #:seen [structs-seen structs-seen] #:kind [kind kind])
+ (loop t pos? from-typed? structs-seen kind))
+ (define (t->c/neg t #:seen [structs-seen structs-seen] #:flat [kind kind])
+ (loop t (not pos?) (not from-typed?) structs-seen kind))
(define (t->c/fun f #:method [method? #f])
(match f
[(Function: (list (top-arr:))) #'procedure?]
[(Function: arrs)
- (when flat? (exit (fail)))
+ (set-chaperone!)
(let ()
(define ((f [case-> #f]) a)
(define-values (dom* opt-dom* rngs* rst)
@@ -133,10 +167,25 @@
[(list e) e]
[l #`(case-> #,@l)]))]
[_ (int-err "not a function" f)]))
+
+ ;; Helpers for contract requirements
+ (define (set-impersonator!)
+ (when (not (equal? kind impersonator-sym)) (exit (fail)))
+ (increase-current-contract-kind! impersonator-sym))
+ (define (set-chaperone!)
+ (when (equal? kind flat-sym) (exit (fail)))
+ (increase-current-contract-kind! chaperone-sym))
+
+
(match ty
[(or (App: _ _ _) (Name: _)) (t->c (resolve-once ty))]
;; any/c doesn't provide protection in positive position
- [(Univ:) (if from-typed? #'any-wrap/c #'any/c)]
+ [(Univ:)
+ (if from-typed?
+ (begin
+ (set-impersonator!)
+ #'any-wrap/c)
+ #'any/c)]
;; we special-case lists:
[(Mu: var (Union: (list (Value: '()) (Pair: elem-ty (F: var)))))
(if (and (not from-typed?) (type-equal? elem-ty t:Univ))
@@ -205,24 +254,26 @@
([cnts (append (map t->c vars) (map t->c notvars))])
#'(or/c . cnts)))]
[(and t (Function: _)) (t->c/fun t)]
- [(Set: t) #`(set/c #,(t->c t))]
+ [(Set: t)
+ #`(set/c #,(t->c t #:kind (contract-kind-min kind chaperone-sym)))]
[(Sequence: ts) #`(sequence/c #,@(map t->c ts))]
[(Vector: t)
- (when flat? (exit (fail)))
+ (set-chaperone!)
#`(vectorof #,(t->c t))]
[(HeterogenousVector: ts)
- (when flat? (exit (fail)))
+ (set-chaperone!)
#`(vector/c #,@(map t->c ts))]
[(Box: t)
- (when flat? (exit (fail)))
+ (set-chaperone!)
#`(box/c #,(t->c t))]
[(Pair: t1 t2)
#`(cons/c #,(t->c t1) #,(t->c t2))]
[(Promise: t)
- (when flat? (exit (fail)))
+ (set-chaperone!)
#`(promise/c #,(t->c t))]
[(Opaque: p? cert)
#`(flat-named-contract (quote #,(syntax-e p?)) #,(cert p?))]
+ ;; TODO
[(F: v) (cond [(assoc v (vars)) => second]
[else (int-err "unknown var: ~a" v)])]
[(Poly: vs b)
@@ -233,85 +284,66 @@
;; in negative position, use `parameteric/c'
(match-let ([(Poly-names: vs-nm _) ty])
(with-syntax ([(v ...) (generate-temporaries vs-nm)])
+ (set-impersonator!)
(parameterize ([vars (append (map list vs (syntax->list #'(v ...)))
(vars))])
#`(parametric->/c (v ...) #,(t->c b))))))]
[(Mu: n b)
(match-let ([(Mu-name: n-nm _) ty])
(with-syntax ([(n*) (generate-temporaries (list n-nm))])
- (parameterize ([vars (cons (list n #'n* #'n*) (vars))])
- #`(letrec ([n* (recursive-contract #,(t->c b) #,(if flat? #'#:flat #'#:impersonator))])
+ (parameterize ([vars (cons (list n #'n*) (vars))]
+ [current-contract-kind flat-sym])
+ (define ctc (t->c b))
+ #`(letrec ([n* (recursive-contract
+ #,ctc
+ #,(contract-kind->keyword (current-contract-kind)))])
n*))))]
[(Value: #f) #'false/c]
[(Instance: (Class: _ _ (list (list name fcn) ...)))
- (when flat? (exit (fail)))
+ (set-impersonator!)
(with-syntax ([(fcn-cnts ...) (for/list ([f fcn]) (t->c/fun f #:method #t))]
[(names ...) name])
#'(object/c (names fcn-cnts) ...))]
;; init args not currently handled by class/c
[(Class: _ (list (list by-name-init by-name-init-ty _) ...) (list (list name fcn) ...))
- (when flat? (exit (fail)))
+ (set-impersonator!)
(with-syntax ([(fcn-cnt ...) (for/list ([f fcn]) (t->c/fun f #:method #t))]
[(name ...) name]
[(by-name-cnt ...) (for/list ([t by-name-init-ty]) (t->c/neg t))]
[(by-name-init ...) by-name-init])
#'(class/c (name fcn-cnt) ... (init [by-name-init by-name-cnt] ...)))]
[(Value: '()) #'null?]
- [(Struct: nm par (list (fld: flds acc-ids mut?) ...) proc poly? pred? cert maker-id)
+ [(Struct: nm par (list (fld: flds acc-ids mut?) ...) proc poly? pred?)
(cond
[(assf (λ (t) (type-equal? t ty)) structs-seen)
=>
cdr]
[proc (exit (fail))]
- [(and flat? (ormap values mut?))
+ [(and (equal? kind flat-sym) (ormap values mut?))
(exit (fail))]
[poly?
- (with-syntax* ([(rec blame val) (generate-temporaries '(rec blame val))]
- [maker maker-id]
- [cnt-name nm])
- ;If it should be a flat contract, we make flat contracts for the type of each field,
- ;extract the predicates, and apply the predicates to the corresponding field value
- (if flat?
- #`(letrec ([rec
- (make-flat-contract
- #:name 'cnt-name
- #:first-order
- (lambda (val)
- (and
- (#,pred? val)
- #,@(for/list ([fty flds] [f-acc acc-ids])
- #`((flat-contract-predicate
- #,(t->c fty #:seen (cons (cons ty #'(recursive-contract rec #:flat)) structs-seen)))
- (#,f-acc val))))))])
- rec)
- ;Should make this case a chaperone/impersonator contract
- (with-syntax ([(fld-cnts ...)
- (for/list ([fty flds]
- [f-acc acc-ids]
- [m? mut?])
- #`(((contract-projection
- #,(t->c fty #:seen (cons (cons ty #'(recursive-contract rec)) structs-seen)))
- blame)
- (#,f-acc val)))])
- #`(letrec ([rec
- (make-contract
- #:name 'cnt-name
- #:first-order #,pred?
- #:projection
- (lambda (blame)
- (lambda (val)
- (unless (#,pred? val)
- (raise-blame-error blame val "expected ~a value, got ~v" 'cnt-name val))
- (maker fld-cnts ...))))])
- rec))))]
- [else #`(flat-named-contract '#,(syntax-e pred?) #,(cert pred?))])]
+ (with-syntax* ([struct-ctc (generate-temporary 'struct-ctc)])
+ (define field-contracts
+ (for/list ([fty flds] [mut? mut?])
+ (with-syntax* ([rec (generate-temporary 'rec)])
+ (define required-recursive-kind
+ (contract-kind-min kind (if mut? impersonator-sym chaperone-sym)))
+ (parameterize ((current-contract-kind flat-sym))
+ (let ((fld-ctc (t->c fty #:seen (cons (cons ty #'rec) structs-seen)
+ #:kind required-recursive-kind)))
+ #`(let ((rec (recursive-contract struct-ctc #,(contract-kind->keyword (current-contract-kind)))))
+ #,fld-ctc))))))
+ #`(letrec ((struct-ctc (struct/c #,nm #,@field-contracts))) struct-ctc))]
+ [else #`(flat-named-contract '#,(syntax-e pred?) #,pred?)])]
[(Syntax: (Base: 'Symbol _ _ _ _)) #'identifier?]
- [(Syntax: t) #`(syntax/c #,(t->c t))]
+ [(Syntax: t)
+ #`(syntax/c #,(t->c t #:kind flat-sym))]
[(Value: v) #`(flat-named-contract #,(format "~a" v) (lambda (x) (equal? x '#,v)))]
+ ;; TODO Is this sound?
[(Param: in out) #`(parameter/c #,(t->c out))]
[(Hashtable: k v)
- (when flat? (exit (fail)))
- #`(hash/c #,(t->c k) #,(t->c v) #:immutable 'dont-care)]
+ (when (equal? kind flat-sym) (exit (fail)))
+ #`(hash/c #,(t->c k #:kind chaperone-sym) #,(t->c v) #:immutable 'dont-care)]
[else
(exit (fail))]))))
View
11 collects/typed-racket/rep/type-rep.rkt
@@ -307,16 +307,13 @@
;; acc-ids : names of the accessors
;; maker-id : name of the constructor
(def-type Struct ([name identifier?]
- [parent (or/c #f Struct? Name?)]
+ [parent (or/c #f Struct?)]
[flds (listof fld?)]
[proc (or/c #f Function?)]
[poly? (or/c #f (listof symbol?))]
- [pred-id identifier?]
- [cert procedure?]
- [maker-id identifier?])
+ [pred-id identifier?])
[#:intern (list (hash-id name)
(hash-id pred-id)
- (hash-id maker-id)
(and parent (Rep-seq parent))
(map Rep-seq flds)
(and proc (Rep-seq proc)))]
@@ -328,9 +325,7 @@
(map type-rec-id flds)
(and proc (type-rec-id proc))
poly?
- pred-id
- cert
- maker-id)]
+ pred-id)]
[#:key 'struct])
;; A structure type descriptor
View
2  collects/typed-racket/typecheck/signatures.rkt
@@ -30,7 +30,7 @@
(define-signature tc-app^
([cond-contracted tc/app (syntax? . -> . tc-results?)]
[cond-contracted tc/app/check (syntax? tc-results? . -> . tc-results?)]
- [cond-contracted tc/app-regular (syntax? . -> . tc-results?)]))
+ [cond-contracted tc/app-regular (syntax? (or/c tc-results? #f) . -> . tc-results?)]))
(define-signature tc-apply^
([cond-contracted tc/apply (syntax? syntax? . -> . tc-results?)]))
View
3  collects/typed-racket/typecheck/tc-app/signatures.rkt
@@ -1,11 +1,12 @@
#lang racket/base
(require racket/unit
"../../utils/utils.rkt" "../../utils/unit-utils.rkt"
+ syntax/parse/experimental/reflect
racket/contract
(types utils))
(provide (except-out (all-defined-out) checker/c))
-(define checker/c (syntax? (or/c #f tc-results?). -> . (or/c #f tc-results?)))
+(define checker/c reified-syntax-class?)
(define-signature tc-app-hetero^
([cond-contracted tc/app-hetero checker/c]))
View
4 collects/typed-racket/typecheck/tc-app/tc-app-hetero.rkt
@@ -85,7 +85,7 @@
vector-immutable vector)
(pattern (~and form ((~or unsafe-struct-ref unsafe-struct*-ref) struct:expr index:expr))
(match (single-value #'struct)
- [(tc-result1: (and struct-t (app resolve (Struct: _ _ (list (fld: flds _ _) ...) _ _ _ _ _))))
+ [(tc-result1: (and struct-t (app resolve (Struct: _ _ (list (fld: flds _ _) ...) _ _ _))))
(tc/hetero-ref #'index flds struct-t expected "struct")]
[s-ty (tc/app-regular #'form expected)]))
;; vector-ref on het vectors
@@ -97,7 +97,7 @@
;; unsafe struct-set!
(pattern (~and form ((~or unsafe-struct-set! unsafe-struct*-set!) s:expr index:expr val:expr))
(match (single-value #'s)
- [(tc-result1: (and struct-t (app resolve (Struct: _ _ (list (fld: flds _ _) ...) _ _ _ _ _))))
+ [(tc-result1: (and struct-t (app resolve (Struct: _ _ (list (fld: flds _ _) ...) _ _ _))))
(tc/hetero-set! #'index flds #'val struct-t expected "struct")]
[s-ty (tc/app-regular #'form expected)]))
;; vector-set! on het vectors
View
8 collects/typed-racket/typecheck/tc-envops.rkt
@@ -39,7 +39,7 @@
(make-Syntax (update t (-not-filter u x rst)))]
;; struct ops
- [((Struct: nm par flds proc poly pred cert maker-id)
+ [((Struct: nm par flds proc poly pred)
(TypeFilter: u (list rst ... (StructPE: (? (lambda (s) (subtype t s)) s) idx)) x))
(make-Struct nm par
(list-update flds idx
@@ -48,8 +48,8 @@
(update e (-filter u x rst))
acc-id #f)]
[_ (int-err "update on mutable struct field")]))
- proc poly pred cert maker-id)]
- [((Struct: nm par flds proc poly pred cert maker-id)
+ proc poly pred)]
+ [((Struct: nm par flds proc poly pred)
(NotTypeFilter: u (list rst ... (StructPE: (? (lambda (s) (subtype t s)) s) idx)) x))
(make-Struct nm par (list-update flds idx
(match-lambda [(fld: e acc-id #f)
@@ -57,7 +57,7 @@
(update e (-not-filter u x rst))
acc-id #f)]
[_ (int-err "update on mutable struct field")]))
- proc poly pred cert maker-id)]
+ proc poly pred)]
;; otherwise
[(t (TypeFilter: u (list) _))
View
2  collects/typed-racket/typecheck/tc-funapp.rkt
@@ -127,7 +127,7 @@
(and expected (tc-results->values expected))))
t argtys expected)]
;; procedural structs
- [((tc-result1: (and sty (Struct: _ _ _ (? Function? proc-ty) _ _ _ _))) _)
+ [((tc-result1: (and sty (Struct: _ _ _ (? Function? proc-ty) _ _))) _)
(tc/funapp f-stx #`(#,(syntax/loc f-stx dummy) . #,args-stx) (ret proc-ty)
(cons ftype0 argtys) expected)]
;; parameters are functions too
View
14 collects/typed-racket/typecheck/tc-structs.rkt
@@ -83,7 +83,7 @@
;; Option[Struct-Ty] -> Listof[Type]
(define (get-parent-flds p)
(match p
- [(Struct: _ _ flds _ _ _ _ _) flds]
+ [(Struct: _ _ flds _ _ _) flds]
[(Name: n) (get-parent-flds (lookup-type-name n))]
[#f null]))
@@ -122,10 +122,7 @@
[g (in-list getters)])
(make-fld t g setters?))]
[flds (append parent-fields this-flds)]
- [sty (make-Struct nm parent flds proc-ty poly? pred
- ;; this check is so that the tests work
- (if (syntax-transforming?) (syntax-local-certifier) values)
- (or maker* maker))]
+ [sty (make-Struct nm parent flds proc-ty poly? pred)]
[external-fld-types/no-parent types]
[external-fld-types (map fld-t flds)])
(if type-only
@@ -280,7 +277,7 @@
;; create the actual structure type, and the types of the fields
;; that the outside world will see
- (mk/register-sty nm flds parent-name (get-parent-flds parent) types
+ (mk/register-sty nm flds parent (get-parent-flds parent) types
;; procedure
#:proc-ty proc-ty-parsed
#:maker maker
@@ -298,10 +295,11 @@
(c-> identifier? (or/c #f identifier?) (listof identifier?)
(listof Type/c) (or/c #f identifier?)
any/c)
- (define parent-name (if parent (make-Name parent) #f))
+ (define parent-name (and parent (make-Name parent)))
+ (define parent-type (and parent (lookup-type-name parent)))
(define parent-flds (if parent (get-parent-flds parent-name) null))
(define parent-tys (map fld-t parent-flds))
- (define defs (mk/register-sty nm flds parent-name parent-flds tys #:mutable #t))
+ (define defs (mk/register-sty nm flds parent-type parent-flds tys #:mutable #t))
(when kernel-maker
(register-type kernel-maker (λ () (->* (append parent-tys tys) (lookup-type-name nm))))))
View
4 collects/typed-racket/types/abbrev.rkt
@@ -418,8 +418,8 @@
(define (make-arr-dots dom rng dty dbound)
(make-arr* dom rng #:drest (cons dty dbound)))
-(define (-struct name parent flds constructor [proc #f] [poly #f] [pred #'dummy] [cert values])
- (make-Struct name parent flds proc poly pred cert constructor))
+(define (-struct name parent flds [proc #f] [poly #f] [pred #'dummy])
+ (make-Struct name parent flds proc poly pred))
(define/cond-contract (-filter t i [p null])
(c:->* (Type/c name-ref/c) ((listof PathElem?)) Filter/c)
View
4 collects/typed-racket/types/printer.rkt
@@ -213,7 +213,7 @@
[(Name: stx) (fp "~a" (syntax-e stx))]
[(app has-name? (? values name))
(fp "~a" name)]
- [(StructTop: (Struct: nm _ _ _ _ _ _ _)) (fp "(Struct ~a)" (syntax-e nm))]
+ [(StructTop: (Struct: nm _ _ _ _ _)) (fp "(Struct ~a)" (syntax-e nm))]
[(BoxTop:) (fp "Box")]
[(ChannelTop:) (fp "Channel")]
[(ThreadCellTop:) (fp "ThreadCell")]
@@ -237,7 +237,7 @@
(fp "~a" (cons 'List (tuple-elems t)))]
[(Base: n cnt _ _ _) (fp "~s" n)]
[(Opaque: pred _) (fp "(Opaque ~a)" (syntax->datum pred))]
- [(Struct: nm par (list (fld: t _ _) ...) proc _ _ _ _)
+ [(Struct: nm par (list (fld: t _ _) ...) proc _ _)
(fp "#(struct:~a ~a" nm t)
(when proc
(fp " ~a" proc))
View
24 collects/typed-racket/types/remove-intersect.rkt
@@ -67,29 +67,29 @@
(list _ (Pair: _ _)))
#f]
[(or (list (Value: (? (λ (e) (or (null? e) (symbol? e) (number? e) (boolean? e) (pair? e) (keyword? e)))))
- (Struct: n _ flds _ _ _ _ _))
- (list (Struct: n _ flds _ _ _ _ _)
+ (Struct: n _ flds _ _ _))
+ (list (Struct: n _ flds _ _ _)
(Value: (? (λ (e) (or (null? e) (symbol? e) (number? e) (boolean? e) (pair? e) (keyword? e)))))))
#f]
- [(list (Struct: n _ flds _ _ _ _ _)
- (Struct: n* _ flds* _ _ _ _ _)) (=> nevermind)
+ [(list (Struct: n _ flds _ _ _)
+ (Struct: n* _ flds* _ _ _)) (=> nevermind)
(unless (free-identifier=? n n*) (nevermind))
(for/and ([f flds] [f* flds*])
(match* (f f*)
[((fld: t _ _) (fld: t* _ _)) (overlap t t*)]))]
- [(list (Struct: n #f _ _ _ _ _ _)
- (StructTop: (Struct: n* #f _ _ _ _ _ _))) (=> nevermind)
+ [(list (Struct: n #f _ _ _ _)
+ (StructTop: (Struct: n* #f _ _ _ _))) (=> nevermind)
(unless (free-identifier=? n n*) (nevermind))
#t]
;; n and n* must be different, so there's no overlap
- [(list (Struct: n #f flds _ _ _ _ _)
- (Struct: n* #f flds* _ _ _ _ _))
+ [(list (Struct: n #f flds _ _ _)
+ (Struct: n* #f flds* _ _ _))
#f]
- [(list (Struct: n #f flds _ _ _ _ _)
- (StructTop: (Struct: n* #f flds* _ _ _ _ _)))
+ [(list (Struct: n #f flds _ _ _)
+ (StructTop: (Struct: n* #f flds* _ _ _)))
#f]
- [(list (and t1 (Struct: _ _ _ _ _ _ _ _))
- (and t2 (Struct: _ _ _ _ _ _ _ _)))
+ [(list (and t1 (Struct: _ _ _ _ _ _))
+ (and t2 (Struct: _ _ _ _ _ _)))
(or (subtype t1 t2) (subtype t2 t1))]
[(list (== (-val eof))
(Function: _))
View
22 collects/typed-racket/types/subtype.rkt
@@ -220,19 +220,19 @@
(define (in-hierarchy? s par)
(define s-name
(match s
- [(Poly: _ (Struct: s-name _ _ _ _ _ _ _)) s-name]
- [(Struct: s-name _ _ _ _ _ _ _) s-name]))
+ [(Poly: _ (Struct: s-name _ _ _ _ _)) s-name]
+ [(Struct: s-name _ _ _ _ _) s-name]))
(define p-name
(match par
- [(Poly: _ (Struct: p-name _ _ _ _ _ _ _)) p-name]
- [(Struct: p-name _ _ _ _ _ _ _) p-name]))
+ [(Poly: _ (Struct: p-name _ _ _ _ _)) p-name]
+ [(Struct: p-name _ _ _ _ _) p-name]))
(or (free-identifier=? s-name p-name)
(match s
[(Poly: _ (? Struct? s*)) (in-hierarchy? s* par)]
- [(Struct: _ (and (Name: _) p) _ _ _ _ _ _) (in-hierarchy? (resolve-once p) par)]
- [(Struct: _ (? Struct? p) _ _ _ _ _ _) (in-hierarchy? p par)]
- [(Struct: _ (Poly: _ p) _ _ _ _ _ _) (in-hierarchy? p par)]
- [(Struct: _ #f _ _ _ _ _ _) #f]
+ [(Struct: _ (and (Name: _) p) _ _ _ _) (in-hierarchy? (resolve-once p) par)]
+ [(Struct: _ (? Struct? p) _ _ _ _) (in-hierarchy? p par)]
+ [(Struct: _ (Poly: _ p) _ _ _ _) (in-hierarchy? p par)]
+ [(Struct: _ #f _ _ _ _) #f]
[_ (int-err "wtf is this? ~a" s)])))
(not (or (in-hierarchy? s1 s2) (in-hierarchy? s2 s1))))
@@ -405,13 +405,13 @@
A0
(fail! s t))]
;; subtyping on immutable structs is covariant
- [((Struct: nm _ flds proc _ _ _ _) (Struct: nm* _ flds* proc* _ _ _ _)) (=> nevermind)
+ [((Struct: nm _ flds proc _ _) (Struct: nm* _ flds* proc* _ _)) (=> nevermind)
(unless (free-identifier=? nm nm*) (nevermind))
(let ([A (cond [(and proc proc*) (subtype* proc proc*)]
[proc* (fail! proc proc*)]
[else A0])])
(subtype/flds* A flds flds*))]
- [((Struct: nm _ _ _ _ _ _ _) (StructTop: (Struct: nm* _ _ _ _ _ _ _))) (=> nevermind)
+ [((Struct: nm _ _ _ _ _) (StructTop: (Struct: nm* _ _ _ _ _))) (=> nevermind)
(unless (free-identifier=? nm nm*) (nevermind))
A0]
;; Promises are covariant
@@ -433,7 +433,7 @@
[((MPair: _ _) (MPairTop:)) A0]
[((Hashtable: _ _) (HashtableTop:)) A0]
;; subtyping on structs follows the declared hierarchy
- [((Struct: nm (? Type? parent) _ _ _ _ _ _) other)
+ [((Struct: nm (? Type? parent) _ _ _ _) other)
;(dprintf "subtype - hierarchy : ~a ~a ~a\n" nm parent other)
(subtype* A0 parent other)]
;; subtyping on values is pointwise
Something went wrong with that request. Please try again.