From 8afc9346bc88ec885e9c2c88d9ab6c49dd017daa Mon Sep 17 00:00:00 2001 From: Asumu Takikawa Date: Thu, 22 Aug 2013 18:38:09 -0400 Subject: [PATCH] Remove certifiers for Opaque and Refinement types Syntax certifiers are now deprecated. This change should have no effect on the types. original commit: 0e02b7e368a674582c81f5df163ce32b79ade015 --- .../typed-racket-lib/typed-racket/base-env/prims.rkt | 2 +- .../typed-racket-lib/typed-racket/env/init-envs.rkt | 7 +++---- .../typed-racket-lib/typed-racket/infer/infer-unit.rkt | 2 +- .../typed-racket-lib/typed-racket/private/parse-type.rkt | 4 ++-- .../typed-racket/private/type-contract.rkt | 8 ++++---- .../typed-racket-lib/typed-racket/rep/type-rep.rkt | 8 +++----- .../typed-racket/typecheck/tc-toplevel.rkt | 2 +- .../typed-racket-lib/typed-racket/types/printer.rkt | 4 ++-- .../typed-racket/types/remove-intersect.rkt | 8 ++++---- .../typed-racket-lib/typed-racket/types/subtype.rkt | 2 +- 10 files changed, 22 insertions(+), 25 deletions(-) diff --git a/pkgs/typed-racket-pkgs/typed-racket-lib/typed-racket/base-env/prims.rkt b/pkgs/typed-racket-pkgs/typed-racket-lib/typed-racket/base-env/prims.rkt index 8b211934..ee080177 100644 --- a/pkgs/typed-racket-pkgs/typed-racket-lib/typed-racket/base-env/prims.rkt +++ b/pkgs/typed-racket-pkgs/typed-racket-lib/typed-racket/base-env/prims.rkt @@ -322,7 +322,7 @@ This file defines two sorts of primitives. All of them are provided into any mod (pattern #:name-exists)) (syntax-parse stx [(_ ty:id pred:id lib (~optional ne:name-exists-kw) ...) - (register-type-name #'ty (make-Opaque #'pred (syntax-local-certifier))) + (register-type-name #'ty (make-Opaque #'pred)) (with-syntax ([hidden (generate-temporary #'pred)]) (quasisyntax/loc stx (begin diff --git a/pkgs/typed-racket-pkgs/typed-racket-lib/typed-racket/env/init-envs.rkt b/pkgs/typed-racket-pkgs/typed-racket-lib/typed-racket/env/init-envs.rkt index 2156cefa..ef3bdb7c 100644 --- a/pkgs/typed-racket-pkgs/typed-racket-lib/typed-racket/env/init-envs.rkt +++ b/pkgs/typed-racket-pkgs/typed-racket-lib/typed-racket/env/init-envs.rkt @@ -57,10 +57,9 @@ ,(sub flds) ,(sub proc) ,(sub poly?) (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) - (quote-syntax ,pred) - (syntax-local-certifier))] + [(Opaque: pred) `(make-Opaque (quote-syntax ,pred))] + [(Refinement: parent pred) `(make-Refinement ,(sub parent) + (quote-syntax ,pred))] [(Mu-name: n b) `(make-Mu ,(sub n) ,(sub b))] [(Poly-names: ns b) `(make-Poly (list ,@(map sub ns)) ,(sub b))] [(PolyDots-names: ns b) `(make-PolyDots (list ,@(map sub ns)) ,(sub b))] diff --git a/pkgs/typed-racket-pkgs/typed-racket-lib/typed-racket/infer/infer-unit.rkt b/pkgs/typed-racket-pkgs/typed-racket-lib/typed-racket/infer/infer-unit.rkt index d0ac7280..726ea1d6 100644 --- a/pkgs/typed-racket-pkgs/typed-racket-lib/typed-racket/infer/infer-unit.rkt +++ b/pkgs/typed-racket-pkgs/typed-racket-lib/typed-racket/infer/infer-unit.rkt @@ -415,7 +415,7 @@ (nevermind))] ;; refinements are erased to their bound - [((Refinement: S _ _) T) + [((Refinement: S _) T) (cg S T)] ;; variables that are in X and should be constrained diff --git a/pkgs/typed-racket-pkgs/typed-racket-lib/typed-racket/private/parse-type.rkt b/pkgs/typed-racket-pkgs/typed-racket-lib/typed-racket/private/parse-type.rkt index 31dbc535..14516414 100644 --- a/pkgs/typed-racket-pkgs/typed-racket-lib/typed-racket/private/parse-type.rkt +++ b/pkgs/typed-racket-pkgs/typed-racket-lib/typed-racket/private/parse-type.rkt @@ -182,7 +182,7 @@ (add-disappeared-use #'kw) (match (lookup-type/lexical #'p?) [(and t (Function: (list (arr: (list dom) _ #f #f '())))) - (make-Refinement dom #'p? (syntax-local-certifier))] + (make-Refinement dom #'p?)] [t (tc-error "cannot declare refinement for non-predicate ~a" t)])] [((~and kw t:Struct) t) (add-disappeared-use #'kw) @@ -264,7 +264,7 @@ (parse-all-type stx)] [((~and kw t:Opaque) p?) (add-disappeared-use #'kw) - (make-Opaque #'p? (syntax-local-certifier))] + (make-Opaque #'p?)] [((~and kw t:Parameter) t) (let ([ty (parse-type #'t)]) (add-disappeared-use #'kw) diff --git a/pkgs/typed-racket-pkgs/typed-racket-lib/typed-racket/private/type-contract.rkt b/pkgs/typed-racket-pkgs/typed-racket-lib/typed-racket/private/type-contract.rkt index fcbd9811..dea2baae 100644 --- a/pkgs/typed-racket-pkgs/typed-racket-lib/typed-racket/private/type-contract.rkt +++ b/pkgs/typed-racket-pkgs/typed-racket-lib/typed-racket/private/type-contract.rkt @@ -338,8 +338,8 @@ [(== t:-Number type-equal?) #'(flat-named-contract 'Number number?)] [(Base: sym cnt _ _ _) #`(flat-named-contract '#,sym (flat-contract-predicate #,cnt))] - [(Refinement: par p? cert) - #`(and/c #,(t->c par) (flat-contract #,(cert p?)))] + [(Refinement: par p?) + #`(and/c #,(t->c par) (flat-contract #,p?))] [(Union: elems) (let-values ([(vars notvars) (partition F? elems)]) (unless (>= 1 (length vars)) (exit (fail))) @@ -364,8 +364,8 @@ [(Promise: t) (set-chaperone!) #`(promise/c #,(t->c t))] - [(Opaque: p? cert) - #`(flat-named-contract (quote #,(syntax-e p?)) #,(cert p?))] + [(Opaque: p?) + #`(flat-named-contract (quote #,(syntax-e p?)) #,p?)] [(Continuation-Mark-Keyof: t) (set-chaperone!) #`(continuation-mark-key/c #,(t->c/both t))] diff --git a/pkgs/typed-racket-pkgs/typed-racket-lib/typed-racket/rep/type-rep.rkt b/pkgs/typed-racket-pkgs/typed-racket-lib/typed-racket/rep/type-rep.rkt index 83fce5f5..3a8fdd9a 100644 --- a/pkgs/typed-racket-pkgs/typed-racket-lib/typed-racket/rep/type-rep.rkt +++ b/pkgs/typed-racket-pkgs/typed-racket-lib/typed-racket/rep/type-rep.rkt @@ -237,8 +237,7 @@ (*PolyDots n (add-scopes n (type-rec-id body*))))]) ;; pred : identifier -;; cert : syntax certifier -(def-type Opaque ([pred identifier?] [cert procedure?]) +(def-type Opaque ([pred identifier?]) [#:intern (hash-id pred)] [#:frees #f] [#:fold-rhs #:base] [#:key pred]) ;; kw : keyword? @@ -336,7 +335,6 @@ ;; poly? : is this type polymorphicly variant ;; If not, then the predicate is enough for higher order checks ;; pred-id : identifier for the predicate of the struct -;; cert : syntax certifier for pred-id ;; acc-ids : names of the accessors ;; maker-id : name of the constructor (def-type Struct ([name identifier?] @@ -418,10 +416,10 @@ (def-type Hashtable ([key Type/c] [value Type/c]) [#:key 'hash] [#:frees (λ (f) (combine-frees (list (make-invariant (f key)) (make-invariant (f value)))))]) -(def-type Refinement ([parent Type/c] [pred identifier?] [cert procedure?]) +(def-type Refinement ([parent Type/c] [pred identifier?]) [#:key (Type-key parent)] [#:intern (list (Rep-seq parent) (hash-id pred))] - [#:fold-rhs (*Refinement (type-rec-id parent) pred cert)] + [#:fold-rhs (*Refinement (type-rec-id parent) pred)] [#:frees (λ (f) (f parent))]) diff --git a/pkgs/typed-racket-pkgs/typed-racket-lib/typed-racket/typecheck/tc-toplevel.rkt b/pkgs/typed-racket-pkgs/typed-racket-lib/typed-racket/typecheck/tc-toplevel.rkt index a89bec62..a00271d0 100644 --- a/pkgs/typed-racket-pkgs/typed-racket-lib/typed-racket/typecheck/tc-toplevel.rkt +++ b/pkgs/typed-racket-pkgs/typed-racket-lib/typed-racket/typecheck/tc-toplevel.rkt @@ -118,7 +118,7 @@ [(and t (Function: (list (arr: (list dom) (Values: (list (Result: rng _ _))) #f #f '())))) (let ([new-t (make-pred-ty (list dom) rng - (make-Refinement dom #'pred (syntax-local-certifier)))]) + (make-Refinement dom #'pred))]) (register-type #'pred new-t)) (list)] [t (tc-error "cannot declare refinement for non-predicate ~a" t)])] diff --git a/pkgs/typed-racket-pkgs/typed-racket-lib/typed-racket/types/printer.rkt b/pkgs/typed-racket-pkgs/typed-racket-lib/typed-racket/types/printer.rkt index 15fdbe5a..81ad216e 100644 --- a/pkgs/typed-racket-pkgs/typed-racket-lib/typed-racket/types/printer.rkt +++ b/pkgs/typed-racket-pkgs/typed-racket-lib/typed-racket/types/printer.rkt @@ -299,7 +299,7 @@ [(? tuple? t) (fp "~a" (cons 'List (tuple-elems t)))] [(Base: n cnt _ _ _) (fp "~s" n)] - [(Opaque: pred _) (fp "(Opaque ~a)" (syntax->datum pred))] + [(Opaque: pred) (fp "(Opaque ~a)" (syntax->datum pred))] [(Struct: nm par (list (fld: t _ _) ...) proc _ _) (fp "#(struct:~a ~a" nm t) (when proc @@ -381,7 +381,7 @@ [(Result: t fs (Empty:)) (fp "(~a : ~a)" t fs)] [(Result: t fs lo) (fp "(~a : ~a : ~a)" t fs lo)] [(MPair: s t) (fp "(MPairof ~a ~a)" s t)] - [(Refinement: parent p? _) + [(Refinement: parent p?) (fp "(Refinement ~a ~a)" parent (syntax-e p?))] [(Sequence: ts) (fp "(Sequenceof") diff --git a/pkgs/typed-racket-pkgs/typed-racket-lib/typed-racket/types/remove-intersect.rkt b/pkgs/typed-racket-pkgs/typed-racket-lib/typed-racket/types/remove-intersect.rkt index db1ef216..76d23e33 100644 --- a/pkgs/typed-racket-pkgs/typed-racket-lib/typed-racket/types/remove-intersect.rkt +++ b/pkgs/typed-racket-pkgs/typed-racket-lib/typed-racket/types/remove-intersect.rkt @@ -33,8 +33,8 @@ [(list _ (Univ:)) #t] [(list (F: _) _) #t] [(list _ (F: _)) #t] - [(list (Opaque: _ _) _) #t] - [(list _ (Opaque: _ _)) #t] + [(list (Opaque: _) _) #t] + [(list _ (Opaque: _)) #t] [(list (Name: n) (Name: n*)) (or (free-identifier=? n n*) (overlap (resolve-once t1) (resolve-once t2)))] @@ -45,8 +45,8 @@ [(list (? Mu?) _) (overlap (unfold t1) t2)] [(list _ (? Mu?)) (overlap t1 (unfold t2))] - [(list (Refinement: t _ _) t2) (overlap t t2)] - [(list t1 (Refinement: t _ _)) (overlap t1 t)] + [(list (Refinement: t _) t2) (overlap t t2)] + [(list t1 (Refinement: t _)) (overlap t1 t)] [(list (Union: e) t) (ormap (lambda (t*) (overlap t* t)) e)] diff --git a/pkgs/typed-racket-pkgs/typed-racket-lib/typed-racket/types/subtype.rkt b/pkgs/typed-racket-pkgs/typed-racket-lib/typed-racket/types/subtype.rkt index 365248f0..7029f9f9 100644 --- a/pkgs/typed-racket-pkgs/typed-racket-lib/typed-racket/types/subtype.rkt +++ b/pkgs/typed-racket-pkgs/typed-racket-lib/typed-racket/types/subtype.rkt @@ -392,7 +392,7 @@ (hash-set (make-simple-substitution ns (map make-F (take ms (length ns)))) n-dotted (i-subst (map make-F (drop ms (length ns)))))) (subtype* A0 (subst-all subst b1) b2)] - [((Refinement: par _ _) t) + [((Refinement: par _) t) (subtype* A0 par t)] ;; use unification to see if we can use the polytype here [((Poly: vs b) s)