suzanne.soy/typed-racket
1
0
Fork 0
Code Issues Pull Requests Actions Packages Projects Releases Wiki Activity

fix parsing of refinements and type aliases

Browse Source
This commit is contained in:
Andrew Kent 2017-11-05 15:32:21 -05:00 committed by GitHub
parent 160e926da8
commit 1a042f8520
No known key found for this signature in database
GPG Key ID: 4AEE18F83AFDEB23
3 changed files with 47 additions and 15 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

14
typed-racket-lib/typed-racket/env/type-alias-helper.rkt vendored
View File

@ -111,15 +111,15 @@
;; recursive type aliases should be initialized.
(define-values (type-alias-dependency-map type-alias-class-map)
(for/lists (_1 _2)
([entry (in-list type-alias-map)])
(match-define (cons name alias-info) entry)
([(name alias-info) (in-assoc type-alias-map)])
(define links-box (box null))
(define class-box (box null))
(define type
(parameterize ([current-type-alias-name name]
[current-referenced-aliases links-box]
[current-referenced-class-parents class-box])
(parse-type (car alias-info))))
;; parse types for effect
(parameterize ([current-type-alias-name name]
[current-referenced-aliases links-box]
[current-referenced-class-parents class-box]
[check-type-invariants-while-parsing? #f])
(parse-type (car alias-info)))
(define pre-dependencies
(remove-duplicates (unbox links-box) free-identifier=?))
(define (filter-by-type-alias-names names)

32
typed-racket-lib/typed-racket/private/parse-type.rkt
View File

@ -45,7 +45,8 @@
(provide star ddd/bound
current-referenced-aliases
current-referenced-class-parents
current-type-alias-name)
current-type-alias-name
check-type-invariants-while-parsing?)
;; current-term-names : Parameter<(Listof Id)>
;; names currently "bound" by a type we are parsing
@ -96,6 +97,14 @@
(parameterize ([current-arities (cons arity (current-arities))])
e ...))
;; code in type-alias-helper.rkt calls `parse-type` for effect to build up
;; info about how types depend on eachother -- during this parsing, we can't
;; check certain invariant successfully (i.e. when a user writes `(car p)`
;; `p` is <: (Pair Any Any), etc), so we use this flag to disable/enable
;; invariant checking while parsing
(define check-type-invariants-while-parsing? (make-parameter #t))
(define-literal-syntax-class #:for-label car)
(define-literal-syntax-class #:for-label cdr)
(define-literal-syntax-class #:for-label vector-length)
@ -379,7 +388,8 @@
(pattern o:symbolic-object
#:do [(define obj (attribute o.val))
(define obj-ty (lookup-obj-type/lexical obj))]
#:fail-unless (subtype obj-ty -Int)
#:fail-when (and (check-type-invariants-while-parsing?)
(not (subtype obj-ty -Int)))
(format "terms in linear constraints must be integers, got ~a for ~a"
obj-ty obj)
#:attr val (attribute o.val)))
@ -398,7 +408,8 @@
(pattern (:*^ ~! n:exact-integer o:symbolic-object-w/o-lexp)
#:do [(define obj (attribute o.val))
(define obj-ty (lookup-obj-type/lexical obj))]
#:fail-unless (subtype obj-ty -Int)
#:fail-when (and (check-type-invariants-while-parsing?)
(not (subtype obj-ty -Int)))
(format "terms in linear constraints must be integers, got ~a for ~a"
obj-ty obj)
#:attr val (-lexp (list (syntax->datum #'n) (attribute o.val))))
@ -424,21 +435,24 @@
(pattern (:car^ ~! o:symbolic-object-w/o-lexp)
#:do [(define obj (attribute o.val))
(define obj-ty (lookup-obj-type/lexical obj))]
#:fail-unless (subtype obj-ty (-pair Univ Univ))
#:fail-when (and (check-type-invariants-while-parsing?)
(not (subtype obj-ty (-pair Univ Univ))))
(format "car expects a pair, but got ~a for ~a"
obj-ty obj)
#:attr val (-car-of (attribute o.val)))
(pattern (:cdr^ ~! o:symbolic-object-w/o-lexp)
#:do [(define obj (attribute o.val))
(define obj-ty (lookup-obj-type/lexical obj))]
#:fail-unless (subtype obj-ty (-pair Univ Univ))
#:fail-when (and (check-type-invariants-while-parsing?)
(not (subtype obj-ty (-pair Univ Univ))))
(format "cdr expects a pair, but got ~a for ~a"
obj-ty obj)
#:attr val (-cdr-of (attribute o.val)))
(pattern (:vector-length^ ~! o:symbolic-object-w/o-lexp)
#:do [(define obj (attribute o.val))
(define obj-ty (lookup-obj-type/lexical obj))]
#:fail-unless (subtype obj-ty -VectorTop)
#:fail-when (and (check-type-invariants-while-parsing?)
(not (subtype obj-ty -VectorTop)))
(format "vector-length expects a vector, but got ~a for ~a"
obj-ty obj)
#:attr val (-vec-len-of (attribute o.val))))
@ -461,7 +475,8 @@
(pattern (:*^ ~! coeff:exact-integer o:symbolic-object-w/o-lexp)
#:do [(define obj (attribute o.val))
(define obj-ty (lookup-obj-type/lexical obj))]
#:fail-unless (subtype obj-ty -Int)
#:fail-when (and (check-type-invariants-while-parsing?)
(not (subtype obj-ty -Int)))
(format "terms in linear expressions must be integers, got ~a for ~a"
obj-ty obj)
#:attr val (-lexp (list (syntax->datum #'coeff) (attribute o.val))))
@ -470,7 +485,8 @@
(pattern o:symbolic-object-w/o-lexp
#:do [(define obj (attribute o.val))
(define obj-ty (lookup-obj-type/lexical obj))]
#:fail-unless (subtype obj-ty -Int)
#:fail-when (and (check-type-invariants-while-parsing?)
(not (subtype obj-ty -Int)))
(format "terms in linear expressions must be integers, got ~a for ~a"
obj-ty obj)
#:attr val (attribute o.val))

16
typed-racket-test/succeed/refinements-and-aliases.rkt Normal file
View File

@ -0,0 +1,16 @@
#lang typed/racket/base #:with-refinements
(define-type Pear (Pair Integer Integer))
(define-type SomeVectorsInAPair (Pair (Vectorof String)
(Vectorof String)))
(define-type Pear1
(Refine [p : Pear] (= (car p) 5)))
(define-type Pear2
(Refine [p : Pear] (= (cdr p) 5)))
(define-type Vec
(Refine [p : SomeVectorsInAPair]
(= (vector-length (car p))
(vector-length (cdr p)))))