Simplify fast path for typechecking simple function applications.
Also, minorly revise subtyping code.
This commit is contained in:
parent
73526b449b
commit
b3c640870e
|
@ -5,7 +5,7 @@
|
||||||
"utils.rkt"
|
"utils.rkt"
|
||||||
syntax/parse racket/match
|
syntax/parse racket/match
|
||||||
syntax/parse/experimental/reflect
|
syntax/parse/experimental/reflect
|
||||||
(typecheck signatures check-below tc-funapp)
|
(typecheck signatures check-below tc-funapp tc-app-helper)
|
||||||
(types utils abbrev)
|
(types utils abbrev)
|
||||||
(rep type-rep filter-rep object-rep rep-utils)
|
(rep type-rep filter-rep object-rep rep-utils)
|
||||||
(for-template racket/base))
|
(for-template racket/base))
|
||||||
|
@ -58,23 +58,19 @@
|
||||||
|
|
||||||
|
|
||||||
(define (tc/app-regular form expected)
|
(define (tc/app-regular form expected)
|
||||||
(syntax-parse form
|
(syntax-case form ()
|
||||||
[(f . args)
|
[(f . args)
|
||||||
(let* ([f-ty (single-value #'f)])
|
(let* ([f-ty (single-value #'f)]
|
||||||
|
[args* (syntax->list #'args)])
|
||||||
(match f-ty
|
(match f-ty
|
||||||
[(tc-result1:
|
[(tc-result1:
|
||||||
(and t (Function:
|
(and t (Function:
|
||||||
(list (and a (arr: (? (lambda (d)
|
(list (and a (arr: (? (λ (d) (= (length d) (length args*))) dom)
|
||||||
(= (length d)
|
|
||||||
(length (syntax->list #'args))))
|
|
||||||
dom)
|
|
||||||
(Values: (list (Result: v (FilterSet: (Top:) (Top:)) (Empty:))))
|
(Values: (list (Result: v (FilterSet: (Top:) (Top:)) (Empty:))))
|
||||||
#f #f (list (Keyword: _ _ #f) ...)))))))
|
#f #f (list (Keyword: _ _ #f) ...)))))))
|
||||||
;(printf "f dom: ~a ~a\n" (syntax->datum #'f) dom)
|
(for ([a (in-list args*)] [t (in-list dom)])
|
||||||
(let ([arg-tys (map (lambda (a t) (tc-expr/check a (ret t)))
|
(tc-expr/check a (ret t)))
|
||||||
(syntax->list #'args)
|
(ret v)]
|
||||||
dom)])
|
|
||||||
(tc/funapp #'f #'args f-ty arg-tys expected))]
|
|
||||||
[_
|
[_
|
||||||
(let ([arg-tys (map single-value (syntax->list #'args))])
|
(let ([arg-tys (map single-value (syntax->list #'args))])
|
||||||
(tc/funapp #'f #'args f-ty arg-tys expected))]))]))
|
(tc/funapp #'f #'args f-ty arg-tys expected))]))]))
|
||||||
|
|
|
@ -1,5 +1,5 @@
|
||||||
#lang racket/base
|
#lang racket/base
|
||||||
(require (except-in "../utils/utils.rkt" infer)
|
(require (except-in "../utils/utils.rkt" infer) racket/unsafe/ops
|
||||||
(rep type-rep filter-rep object-rep rep-utils)
|
(rep type-rep filter-rep object-rep rep-utils)
|
||||||
(utils tc-utils)
|
(utils tc-utils)
|
||||||
(types utils resolve base-abbrev numeric-tower substitute)
|
(types utils resolve base-abbrev numeric-tower substitute)
|
||||||
|
@ -17,7 +17,6 @@
|
||||||
|
|
||||||
;; exn representing failure of subtyping
|
;; exn representing failure of subtyping
|
||||||
;; s,t both types
|
;; s,t both types
|
||||||
|
|
||||||
(define-struct (exn:subtype exn:fail) (s t))
|
(define-struct (exn:subtype exn:fail) (s t))
|
||||||
|
|
||||||
;; subtyping failure - masked before it gets to the user program
|
;; subtyping failure - masked before it gets to the user program
|
||||||
|
@ -28,7 +27,7 @@
|
||||||
;; data structures for remembering things on recursive calls
|
;; data structures for remembering things on recursive calls
|
||||||
(define (empty-set) '())
|
(define (empty-set) '())
|
||||||
|
|
||||||
(define current-seen (make-parameter (empty-set) #;pair?))
|
(define current-seen (make-parameter (empty-set)))
|
||||||
|
|
||||||
(define (seen-before s t) (cons (Type-seq s) (Type-seq t)))
|
(define (seen-before s t) (cons (Type-seq s) (Type-seq t)))
|
||||||
(define (remember s t A) (cons (seen-before s t) A))
|
(define (remember s t A) (cons (seen-before s t) A))
|
||||||
|
@ -42,38 +41,28 @@
|
||||||
(define (cached? s t)
|
(define (cached? s t)
|
||||||
(hash-ref subtype-cache (cons (Type-seq s) (Type-seq t)) #f))
|
(hash-ref subtype-cache (cons (Type-seq s) (Type-seq t)) #f))
|
||||||
|
|
||||||
|
(define-syntax-rule (handle-failure e)
|
||||||
|
(with-handlers ([exn:subtype? (λ (_) #f)])
|
||||||
|
e))
|
||||||
|
|
||||||
;; is s a subtype of t?
|
;; is s a subtype of t?
|
||||||
;; type type -> boolean
|
;; type type -> boolean
|
||||||
(define/cond-contract (subtype s t)
|
(define/cond-contract (subtype s t)
|
||||||
(c:-> (c:or/c Type/c Values?) (c:or/c Type/c Values?) boolean?)
|
(c:-> (c:or/c Type/c Values?) (c:or/c Type/c Values?) boolean?)
|
||||||
(define k (cons (Type-seq s) (Type-seq t)))
|
(define k (cons (unsafe-struct-ref s 0) (unsafe-struct-ref t 0)))
|
||||||
(define lookup? (hash-ref subtype-cache k 'no))
|
(define (new-val)
|
||||||
(if (eq? 'no lookup?)
|
(define result (handle-failure (and (subtype* (current-seen) s t) #t)))
|
||||||
(let ([result (with-handlers
|
(printf "subtype cache miss ~a ~a\n" s t)
|
||||||
([exn:subtype? (lambda _ #f)])
|
|
||||||
(and (subtype* (current-seen) s t) #t))])
|
|
||||||
(hash-set! subtype-cache k result)
|
|
||||||
result)
|
result)
|
||||||
lookup?))
|
(hash-ref! subtype-cache k new-val))
|
||||||
|
|
||||||
;; are all the s's subtypes of all the t's?
|
;; are all the s's subtypes of all the t's?
|
||||||
;; [type] [type] -> boolean
|
;; [type] [type] -> boolean
|
||||||
(define (subtypes s t)
|
(define (subtypes s t) (handle-failure (subtypes* (current-seen) s t)))
|
||||||
(with-handlers
|
|
||||||
([exn:subtype? (lambda _ #f)])
|
|
||||||
(subtypes* (current-seen) s t)))
|
|
||||||
|
|
||||||
;; subtyping under constraint set, but produces boolean result instead of raising exn
|
;; subtyping under constraint set, but produces boolean result instead of raising exn
|
||||||
;; List[(cons Number Number)] type type -> maybe[List[(cons Number Number)]]
|
;; List[(cons Number Number)] type type -> maybe[List[(cons Number Number)]]
|
||||||
(define (subtype*/no-fail A s t)
|
(define (subtype*/no-fail A s t) (handle-failure (subtype* A s t)))
|
||||||
(with-handlers
|
|
||||||
([exn:subtype? (lambda _ #f)])
|
|
||||||
(subtype* A s t)))
|
|
||||||
|
|
||||||
;; type type -> (does not return)
|
|
||||||
;; subtying fails
|
|
||||||
#;
|
|
||||||
(define (fail! s t) (raise (make-exn:subtype "subtyping failed" (current-continuation-marks) s t)))
|
|
||||||
|
|
||||||
;; check subtyping for two lists of types
|
;; check subtyping for two lists of types
|
||||||
;; List[(cons Number Number)] listof[type] listof[type] -> List[(cons Number Number)]
|
;; List[(cons Number Number)] listof[type] listof[type] -> List[(cons Number Number)]
|
||||||
|
|
Loading…
Reference in New Issue
Block a user