WIP on fixing free-variance.
This commit is contained in:
parent
e3743b446c
commit
40809e768d
|
@ -581,8 +581,8 @@
|
||||||
;; R : Type? - result type into which we will be substituting
|
;; R : Type? - result type into which we will be substituting
|
||||||
(define/cond-contract (subst-gen C Y R)
|
(define/cond-contract (subst-gen C Y R)
|
||||||
(cset? (listof symbol?) Type? . -> . (or/c #f substitution/c))
|
(cset? (listof symbol?) Type? . -> . (or/c #f substitution/c))
|
||||||
(define var-hash (free-vars* R))
|
(define var-hash (free-vars-hash (free-vars* R)))
|
||||||
(define idx-hash (free-idxs* R))
|
(define idx-hash (free-vars-hash (free-idxs* R)))
|
||||||
;; v : Symbol - variable for which to check variance
|
;; v : Symbol - variable for which to check variance
|
||||||
;; h : (Hash Symbol Variance) - hash to check variance in (either var or idx hash)
|
;; h : (Hash Symbol Variance) - hash to check variance in (either var or idx hash)
|
||||||
;; variable: Symbol - variable to use instead, if v was a temp var for idx extension
|
;; variable: Symbol - variable to use instead, if v was a temp var for idx extension
|
||||||
|
|
|
@ -21,14 +21,12 @@
|
||||||
|
|
||||||
(def-filter TypeFilter ([t Type?] [p (listof PathElem?)] [v name-ref/c])
|
(def-filter TypeFilter ([t Type?] [p (listof PathElem?)] [v name-ref/c])
|
||||||
[#:intern (list (Rep-seq t) (map Rep-seq p) (hash-name v))]
|
[#:intern (list (Rep-seq t) (map Rep-seq p) (hash-name v))]
|
||||||
[#:frees (combine-frees (map free-vars* (cons t p)))
|
[#:frees (λ (f) (combine-frees (map f (cons t p))))]
|
||||||
(combine-frees (map free-idxs* (cons t p)))]
|
|
||||||
[#:fold-rhs (*TypeFilter (type-rec-id t) (map pathelem-rec-id p) v)])
|
[#:fold-rhs (*TypeFilter (type-rec-id t) (map pathelem-rec-id p) v)])
|
||||||
|
|
||||||
(def-filter NotTypeFilter ([t Type?] [p (listof PathElem?)] [v name-ref/c])
|
(def-filter NotTypeFilter ([t Type?] [p (listof PathElem?)] [v name-ref/c])
|
||||||
[#:intern (list (Rep-seq t) (map Rep-seq p) (hash-name v))]
|
[#:intern (list (Rep-seq t) (map Rep-seq p) (hash-name v))]
|
||||||
[#:frees (combine-frees (map free-vars* (cons t p)))
|
[#:frees (λ (f) (combine-frees (map f (cons t p))))]
|
||||||
(combine-frees (map free-idxs* (cons t p)))]
|
|
||||||
[#:fold-rhs (*NotTypeFilter (type-rec-id t) (map pathelem-rec-id p) v)])
|
[#:fold-rhs (*NotTypeFilter (type-rec-id t) (map pathelem-rec-id p) v)])
|
||||||
|
|
||||||
;; implication
|
;; implication
|
||||||
|
@ -36,13 +34,11 @@
|
||||||
|
|
||||||
(def-filter AndFilter ([fs (non-empty-listof Filter/c)])
|
(def-filter AndFilter ([fs (non-empty-listof Filter/c)])
|
||||||
[#:fold-rhs (*AndFilter (map filter-rec-id fs))]
|
[#:fold-rhs (*AndFilter (map filter-rec-id fs))]
|
||||||
[#:frees (combine-frees (map free-vars* fs))
|
[#:frees (λ (f) (combine-frees (map f fs)))])
|
||||||
(combine-frees (map free-idxs* fs))])
|
|
||||||
|
|
||||||
(def-filter OrFilter ([fs (non-empty-listof Filter/c)])
|
(def-filter OrFilter ([fs (non-empty-listof Filter/c)])
|
||||||
[#:fold-rhs (*OrFilter (map filter-rec-id fs))]
|
[#:fold-rhs (*OrFilter (map filter-rec-id fs))]
|
||||||
[#:frees (combine-frees (map free-vars* fs))
|
[#:frees (λ (f) (combine-frees (map f fs)))])
|
||||||
(combine-frees (map free-idxs* fs))])
|
|
||||||
|
|
||||||
(def-filter FilterSet (thn els)
|
(def-filter FilterSet (thn els)
|
||||||
[#:contract (->i ([t any/c]
|
[#:contract (->i ([t any/c]
|
||||||
|
|
|
@ -2,7 +2,7 @@
|
||||||
(require "../utils/utils.rkt" (for-syntax racket/base) (contract-req))
|
(require "../utils/utils.rkt" (for-syntax racket/base) (contract-req))
|
||||||
|
|
||||||
(provide Covariant Contravariant Invariant Constant Dotted
|
(provide Covariant Contravariant Invariant Constant Dotted
|
||||||
combine-frees flip-variances without-below unless-in-table
|
combine-frees flip-variances without-below
|
||||||
fix-bound make-invariant make-constant variance?)
|
fix-bound make-invariant make-constant variance?)
|
||||||
|
|
||||||
;; this file contains support for calculating the free variables/indexes of types
|
;; this file contains support for calculating the free variables/indexes of types
|
||||||
|
@ -22,6 +22,9 @@
|
||||||
(define (variance? e)
|
(define (variance? e)
|
||||||
(memq e (list Covariant Contravariant Invariant Constant Dotted)))
|
(memq e (list Covariant Contravariant Invariant Constant Dotted)))
|
||||||
|
|
||||||
|
(struct frees ())
|
||||||
|
(struct (ht-frees frees) (table))
|
||||||
|
|
||||||
;; frees = HT[Idx,Variance] where Idx is either Symbol or Number
|
;; frees = HT[Idx,Variance] where Idx is either Symbol or Number
|
||||||
;; (listof frees) -> frees
|
;; (listof frees) -> frees
|
||||||
(define (combine-frees freess)
|
(define (combine-frees freess)
|
||||||
|
@ -33,10 +36,11 @@
|
||||||
[(eq? v Constant) w]
|
[(eq? v Constant) w]
|
||||||
[(eq? w Constant) v]
|
[(eq? w Constant) v]
|
||||||
[else Invariant]))
|
[else Invariant]))
|
||||||
(for*/fold ([ht #hasheq()])
|
(ht-frees
|
||||||
([old-ht (in-list freess)]
|
(for*/fold ([ht #hasheq()])
|
||||||
[(sym var) (in-hash old-ht)])
|
([old-free (in-list freess)]
|
||||||
(hash-update ht sym (combine-var var) var)))
|
[(sym var) (in-hash (ht-frees-table old-ht))])
|
||||||
|
(hash-update ht sym (combine-var var) var))))
|
||||||
|
|
||||||
;; given a set of free variables, change bound to ...
|
;; given a set of free variables, change bound to ...
|
||||||
;; (if bound wasn't free, this will add it as Dotted
|
;; (if bound wasn't free, this will add it as Dotted
|
||||||
|
@ -44,31 +48,47 @@
|
||||||
;; it as "free" will -- fixes the case where the
|
;; it as "free" will -- fixes the case where the
|
||||||
;; dotted pre-type base doesn't use the bound).
|
;; dotted pre-type base doesn't use the bound).
|
||||||
(define (fix-bound vs bound)
|
(define (fix-bound vs bound)
|
||||||
(hash-set vs bound Dotted))
|
(match vs
|
||||||
|
((ht-frees ht)
|
||||||
|
(ht-frees (hash-set ht bound Dotted)))))
|
||||||
|
|
||||||
;; frees -> frees
|
;; frees -> frees
|
||||||
(define (flip-variances vs)
|
(define (flip-variances vs)
|
||||||
(for/hasheq ([(k v) (in-hash vs)])
|
(ht-frees
|
||||||
(values k
|
(for/hasheq ([(k v) (in-hash (ht-frees-table vs))])
|
||||||
(cond [(eq? v Covariant) Contravariant]
|
(values k
|
||||||
[(eq? v Contravariant) Covariant]
|
(cond [(eq? v Covariant) Contravariant]
|
||||||
[else v]))))
|
[(eq? v Contravariant) Covariant]
|
||||||
|
[else v])))))
|
||||||
|
|
||||||
(define (make-invariant vs)
|
(define (make-invariant vs)
|
||||||
(for/hasheq ([(k v) (in-hash vs)])
|
(ht-frees
|
||||||
(values k Invariant)))
|
(for/hasheq ([(k v) (in-hash (ht-frees-table vs))])
|
||||||
|
(values k Invariant))))
|
||||||
|
|
||||||
(define (make-constant vs)
|
(define (make-constant vs)
|
||||||
(for/hasheq ([(k v) (in-hash vs)])
|
(ht-frees
|
||||||
(values k Constant)))
|
(for/hasheq ([(k v) (in-hash (ht-frees-table vs))])
|
||||||
|
(values k Constant))))
|
||||||
|
|
||||||
(define (without-below n frees)
|
(define (without-below n frees)
|
||||||
(for/hasheq ([(k v) (in-hash frees)]
|
(ht-frees
|
||||||
#:when (>= k n))
|
(for/hasheq ([(k v) (in-hash (ht-frees-table frees))]
|
||||||
(values k v)))
|
#:when (>= k n))
|
||||||
|
(values k v))))
|
||||||
|
|
||||||
|
(define (single-free-var name (variance Covariant))
|
||||||
|
(ht-frees (hasheq name variance)))
|
||||||
|
|
||||||
|
(define empty-free-vars
|
||||||
|
(ht-frees (hasheq)))
|
||||||
|
|
||||||
|
(define (free-vars-remove vars name)
|
||||||
|
(ht-frees
|
||||||
|
(hash-remove (ht-frees-table vars) name)))
|
||||||
|
|
||||||
|
;; Only valid after full type resolution
|
||||||
|
(define (free-vars-hash vars)
|
||||||
|
(ht-frees-table vars))
|
||||||
|
|
||||||
|
|
||||||
(define-syntax (unless-in-table stx)
|
|
||||||
(syntax-case stx ()
|
|
||||||
[(_ table val . body)
|
|
||||||
(quasisyntax/loc stx
|
|
||||||
(hash-ref table val #,(syntax/loc #'body (lambda () . body))))]))
|
|
||||||
|
|
|
@ -8,14 +8,14 @@
|
||||||
(def-pathelem SyntaxPE () [#:fold-rhs #:base])
|
(def-pathelem SyntaxPE () [#:fold-rhs #:base])
|
||||||
;; t is always a Name (can't put that into the contract b/c of circularity)
|
;; t is always a Name (can't put that into the contract b/c of circularity)
|
||||||
(def-pathelem StructPE ([t Type?] [idx natural-number/c])
|
(def-pathelem StructPE ([t Type?] [idx natural-number/c])
|
||||||
[#:frees (free-vars* t) (free-idxs* t)]
|
[#:frees (λ (f) (f t))]
|
||||||
[#:fold-rhs (*StructPE (type-rec-id t) idx)])
|
[#:fold-rhs (*StructPE (type-rec-id t) idx)])
|
||||||
|
|
||||||
(def-object Empty () [#:fold-rhs #:base])
|
(def-object Empty () [#:fold-rhs #:base])
|
||||||
|
|
||||||
(def-object Path ([p (listof PathElem?)] [v name-ref/c])
|
(def-object Path ([p (listof PathElem?)] [v name-ref/c])
|
||||||
[#:intern (list (map Rep-seq p) (hash-name v))]
|
[#:intern (list (map Rep-seq p) (hash-name v))]
|
||||||
[#:frees (combine-frees (map free-vars* p)) (combine-frees (map free-idxs* p))]
|
[#:frees (λ (f) (combine-frees (map f p)))]
|
||||||
[#:fold-rhs (*Path (map pathelem-rec-id p) v)])
|
[#:fold-rhs (*Path (map pathelem-rec-id p) v)])
|
||||||
|
|
||||||
;; represents no info about the object of this expression
|
;; represents no info about the object of this expression
|
||||||
|
@ -28,6 +28,6 @@
|
||||||
(dlo LEmpty () [#:fold-rhs #:base])
|
(dlo LEmpty () [#:fold-rhs #:base])
|
||||||
|
|
||||||
(dlo LPath ([p (listof PathElem?)] [idx index/c])
|
(dlo LPath ([p (listof PathElem?)] [idx index/c])
|
||||||
[#:frees (combine-frees (map free-vars* p)) (combine-frees (map free-idxs* p))]
|
[#:frees (λ (f) (combine-frees (map f p)))]
|
||||||
[#:fold-rhs (*LPath (map pathelem-rec-id p) idx)])
|
[#:fold-rhs (*LPath (map pathelem-rec-id p) idx)])
|
||||||
|#
|
|#
|
||||||
|
|
|
@ -58,7 +58,7 @@
|
||||||
;; (construction prevents duplicates)
|
;; (construction prevents duplicates)
|
||||||
(define (combiner f flds)
|
(define (combiner f flds)
|
||||||
(syntax-parse flds
|
(syntax-parse flds
|
||||||
[() #'#hasheq()]
|
[() #'empty-free-vars]
|
||||||
[(e) #`(#,f e)]
|
[(e) #`(#,f e)]
|
||||||
[(e ...) #`(combine-frees (list (#,f e) ...))]))
|
[(e ...) #`(combine-frees (list (#,f e) ...))]))
|
||||||
|
|
||||||
|
@ -68,8 +68,8 @@
|
||||||
(pattern (~seq f1:expr f2:expr))
|
(pattern (~seq f1:expr f2:expr))
|
||||||
;; [#:frees #f] pattern in e.g. def-type means no free vars or idxs.
|
;; [#:frees #f] pattern in e.g. def-type means no free vars or idxs.
|
||||||
(pattern #f
|
(pattern #f
|
||||||
#:with f1 #'#hasheq()
|
#:with f1 #'empty-free-vars
|
||||||
#:with f2 #'#hasheq())
|
#:with f2 #'empty-free-vars)
|
||||||
;; [#:frees (λ (f) ...)] should combine free variables or idxs accordingly
|
;; [#:frees (λ (f) ...)] should combine free variables or idxs accordingly
|
||||||
;; (given the respective accessor functions)
|
;; (given the respective accessor functions)
|
||||||
(pattern e:expr
|
(pattern e:expr
|
||||||
|
|
|
@ -52,7 +52,7 @@
|
||||||
|
|
||||||
;; free type variables
|
;; free type variables
|
||||||
;; n is a Name
|
;; n is a Name
|
||||||
(def-type F ([n symbol?]) [#:frees (make-immutable-hasheq (list (cons n Covariant))) #hasheq()] [#:fold-rhs #:base])
|
(def-type F ([n symbol?]) [#:frees (single-free-var n) empty-free-vars] [#:fold-rhs #:base])
|
||||||
|
|
||||||
;; id is an Identifier
|
;; id is an Identifier
|
||||||
(def-type Name ([id identifier?]) [#:intern (hash-id id)] [#:frees #f] [#:fold-rhs #:base])
|
(def-type Name ([id identifier?]) [#:intern (hash-id id)] [#:frees #f] [#:fold-rhs #:base])
|
||||||
|
@ -62,47 +62,22 @@
|
||||||
;; stx is the syntax of the pair of parens
|
;; stx is the syntax of the pair of parens
|
||||||
(def-type App ([rator Type/c] [rands (listof Type/c)] [stx (or/c #f syntax?)])
|
(def-type App ([rator Type/c] [rands (listof Type/c)] [stx (or/c #f syntax?)])
|
||||||
[#:intern (cons (Rep-seq rator) (map Rep-seq rands))]
|
[#:intern (cons (Rep-seq rator) (map Rep-seq rands))]
|
||||||
|
;;TODO THIS
|
||||||
[#:frees (λ (f) (combine-frees (map f (cons rator rands))))]
|
[#:frees (λ (f) (combine-frees (map f (cons rator rands))))]
|
||||||
[#:fold-rhs (*App (type-rec-id rator)
|
[#:fold-rhs (*App (type-rec-id rator)
|
||||||
(map type-rec-id rands)
|
(map type-rec-id rands)
|
||||||
stx)])
|
stx)])
|
||||||
|
|
||||||
(define (get-variances t num-rands)
|
|
||||||
(match t
|
|
||||||
[(Name: v) (error 'fail)]
|
|
||||||
[(Poly: n scope)
|
|
||||||
(let ([t (free-idxs* scope)])
|
|
||||||
(for/list ([i (in-range n)])
|
|
||||||
(hash-ref t i)))]
|
|
||||||
[(PolyDots: n scope)
|
|
||||||
(let ([t (free-idxs* scope)]
|
|
||||||
[base-count (sub1 n)]
|
|
||||||
[extras (max 0 (- n num-rands))])
|
|
||||||
(append
|
|
||||||
;; variances of the fixed arguments
|
|
||||||
(for/list ([i (in-range base-count)])
|
|
||||||
(hash-ref t i))
|
|
||||||
;; variance of the dotted arguments
|
|
||||||
(for/list ([i (in-range extras)])
|
|
||||||
(hash-ref t n))))]))
|
|
||||||
|
|
||||||
(define (apply-variance v tbl)
|
|
||||||
(match v
|
|
||||||
[(== Constant) (make-constant tbl)]
|
|
||||||
[(== Covariant) tbl]
|
|
||||||
[(== Invariant) (make-invariant tbl)]
|
|
||||||
[(== Contravariant) (flip-variances tbl)]))
|
|
||||||
|
|
||||||
;; left and right are Types
|
;; left and right are Types
|
||||||
(def-type Pair ([left Type/c] [right Type/c]) [#:key 'pair])
|
(def-type Pair ([left Type/c] [right Type/c]) [#:key 'pair])
|
||||||
|
|
||||||
;; dotted list -- after expansion, becomes normal Pair-based list type
|
;; dotted list -- after expansion, becomes normal Pair-based list type
|
||||||
(def-type ListDots ([dty Type/c] [dbound (or/c symbol? natural-number/c)])
|
(def-type ListDots ([dty Type/c] [dbound (or/c symbol? natural-number/c)])
|
||||||
[#:frees (if (symbol? dbound)
|
[#:frees (if (symbol? dbound)
|
||||||
(hash-remove (free-vars* dty) dbound)
|
(free-vars-remove (free-vars* dty) dbound)
|
||||||
(free-vars* dty))
|
(free-vars* dty))
|
||||||
(if (symbol? dbound)
|
(if (symbol? dbound)
|
||||||
(combine-frees (list (make-immutable-hasheq (list (cons dbound Covariant))) (free-idxs* dty)))
|
(combine-frees (list (single-free-var dbound) (free-idxs* dty)))
|
||||||
(free-idxs* dty))]
|
(free-idxs* dty))]
|
||||||
[#:fold-rhs (*ListDots (type-rec-id dty) dbound)])
|
[#:fold-rhs (*ListDots (type-rec-id dty) dbound)])
|
||||||
|
|
||||||
|
@ -232,10 +207,10 @@
|
||||||
|
|
||||||
(def-type ValuesDots ([rs (listof Result?)] [dty Type/c] [dbound (or/c symbol? natural-number/c)])
|
(def-type ValuesDots ([rs (listof Result?)] [dty Type/c] [dbound (or/c symbol? natural-number/c)])
|
||||||
[#:frees (if (symbol? dbound)
|
[#:frees (if (symbol? dbound)
|
||||||
(hash-remove (combine-frees (map free-vars* (cons dty rs))) dbound)
|
(free-vars-remove (combine-frees (map free-vars* (cons dty rs))) dbound)
|
||||||
(combine-frees (map free-vars* (cons dty rs))))
|
(combine-frees (map free-vars* (cons dty rs))))
|
||||||
(if (symbol? dbound)
|
(if (symbol? dbound)
|
||||||
(combine-frees (cons (make-immutable-hasheq (list (cons dbound Covariant)))
|
(combine-frees (cons (single-free-var dbound)
|
||||||
(map free-idxs* (cons dty rs))))
|
(map free-idxs* (cons dty rs))))
|
||||||
(combine-frees (map free-idxs* (cons dty rs))))]
|
(combine-frees (map free-idxs* (cons dty rs))))]
|
||||||
[#:fold-rhs (*ValuesDots (map type-rec-id rs) (type-rec-id dty) dbound)])
|
[#:fold-rhs (*ValuesDots (map type-rec-id rs) (type-rec-id dty) dbound)])
|
||||||
|
@ -256,7 +231,7 @@
|
||||||
dom))
|
dom))
|
||||||
(match drest
|
(match drest
|
||||||
[(cons t (? symbol? bnd))
|
[(cons t (? symbol? bnd))
|
||||||
(list (hash-remove (flip-variances (free-vars* t)) bnd))]
|
(list (free-vars-remove (flip-variances (free-vars* t)) bnd))]
|
||||||
[(cons t _)
|
[(cons t _)
|
||||||
(list (flip-variances (free-vars* t)))]
|
(list (flip-variances (free-vars* t)))]
|
||||||
[_ null])
|
[_ null])
|
||||||
|
@ -268,7 +243,7 @@
|
||||||
dom))
|
dom))
|
||||||
(match drest
|
(match drest
|
||||||
[(cons t (? symbol? bnd))
|
[(cons t (? symbol? bnd))
|
||||||
(list (make-immutable-hasheq (list (cons bnd Contravariant)))
|
(list (single-free-var bnd Contravariant)
|
||||||
(flip-variances (free-idxs* t)))]
|
(flip-variances (free-idxs* t)))]
|
||||||
[(cons t _)
|
[(cons t _)
|
||||||
(list (flip-variances (free-idxs* t)))]
|
(list (flip-variances (free-idxs* t)))]
|
||||||
|
|
|
@ -290,9 +290,12 @@
|
||||||
provide?
|
provide?
|
||||||
define/fixup-contract?))
|
define/fixup-contract?))
|
||||||
(do-time "Form splitting done")
|
(do-time "Form splitting done")
|
||||||
|
(printf "before parsing type aliases~n")
|
||||||
(for-each (compose register-type-alias parse-type-alias) type-aliases)
|
(for-each (compose register-type-alias parse-type-alias) type-aliases)
|
||||||
;; Add the struct names to the type table, but not with a type
|
;; Add the struct names to the type table, but not with a type
|
||||||
|
(printf "before adding type names~n")
|
||||||
(for-each (compose add-type-name! names-of-struct) struct-defs)
|
(for-each (compose add-type-name! names-of-struct) struct-defs)
|
||||||
|
(printf "after adding type names~n")
|
||||||
;; resolve all the type aliases, and error if there are cycles
|
;; resolve all the type aliases, and error if there are cycles
|
||||||
(resolve-type-aliases parse-type)
|
(resolve-type-aliases parse-type)
|
||||||
;; Parse and register the structure types
|
;; Parse and register the structure types
|
||||||
|
@ -304,19 +307,20 @@
|
||||||
|
|
||||||
;; register the bindings of the structs
|
;; register the bindings of the structs
|
||||||
(for-each register-parsed-struct-bindings! parsed-structs)
|
(for-each register-parsed-struct-bindings! parsed-structs)
|
||||||
(do-time "Starting pass1")
|
(printf "after resolving type aliases~n")
|
||||||
|
(displayln "Starting pass1")
|
||||||
;; do pass 1, and collect the defintions
|
;; do pass 1, and collect the defintions
|
||||||
(define defs (apply append (filter list? (map tc-toplevel/pass1 forms))))
|
(define defs (apply append (filter list? (map tc-toplevel/pass1 forms))))
|
||||||
(do-time "Finished pass1")
|
(displayln "Finished pass1")
|
||||||
;; separate the definitions into structures we'll handle for provides
|
;; separate the definitions into structures we'll handle for provides
|
||||||
(define def-tbl
|
(define def-tbl
|
||||||
(for/fold ([h (make-immutable-free-id-table)])
|
(for/fold ([h (make-immutable-free-id-table)])
|
||||||
([def (in-list defs)])
|
([def (in-list defs)])
|
||||||
(dict-set h (binding-name def) def)))
|
(dict-set h (binding-name def) def)))
|
||||||
;; typecheck the expressions and the rhss of defintions
|
;; typecheck the expressions and the rhss of defintions
|
||||||
(do-time "Starting pass2")
|
(displayln "Starting pass2")
|
||||||
(for-each tc-toplevel/pass2 forms)
|
(for-each tc-toplevel/pass2 forms)
|
||||||
(do-time "Finished pass2")
|
(displayln "Finished pass2")
|
||||||
;; check that declarations correspond to definitions
|
;; check that declarations correspond to definitions
|
||||||
(check-all-registered-types)
|
(check-all-registered-types)
|
||||||
;; report delayed errors
|
;; report delayed errors
|
||||||
|
|
Loading…
Reference in New Issue
Block a user