move subtype.ss
svn: r13815
This commit is contained in:
parent
af3449cf56
commit
ea86a63e80
|
@ -1,16 +1,17 @@
|
||||||
#lang scheme/base
|
#lang scheme/base
|
||||||
(require "../utils/utils.ss")
|
(require "../utils/utils.ss")
|
||||||
|
|
||||||
(require (except-in (rep type-rep effect-rep rep-utils) sub-eff)
|
(require (rep type-rep filter-rep object-rep rep-utils)
|
||||||
(utils tc-utils)
|
(utils tc-utils)
|
||||||
"type-utils.ss"
|
"type-utils.ss"
|
||||||
"type-comparison.ss"
|
"comparison.ss"
|
||||||
"resolve-type.ss"
|
"resolve.ss"
|
||||||
"type-abbrev.ss"
|
"type-abbrev.ss"
|
||||||
(env type-name-env)
|
(env type-name-env)
|
||||||
(only-in (infer infer-dummy) unify)
|
(only-in (infer infer-dummy) unify)
|
||||||
scheme/match
|
scheme/match
|
||||||
mzlib/trace)
|
mzlib/trace
|
||||||
|
(for-syntax scheme/base stxclass))
|
||||||
|
|
||||||
|
|
||||||
|
|
||||||
|
@ -18,18 +19,11 @@
|
||||||
;; s,t both types
|
;; s,t both types
|
||||||
|
|
||||||
(define-struct (exn:subtype exn:fail) (s t))
|
(define-struct (exn:subtype exn:fail) (s t))
|
||||||
#;
|
|
||||||
(define-values (fail-sym exn:subtype?)
|
|
||||||
(let ([sym (gensym)])
|
|
||||||
(values sym (lambda (s) (eq? s sym)))))
|
|
||||||
|
|
||||||
;; inference failure - masked before it gets to the user program
|
;; inference failure - masked before it gets to the user program
|
||||||
(define-syntax fail!
|
(define-syntax fail!
|
||||||
(syntax-rules ()
|
(syntax-rules ()
|
||||||
[(_ s t) #;(raise fail-sym)
|
[(_ s t) (raise (make-exn:subtype "subtyping failed" (current-continuation-marks) s t))]))
|
||||||
(raise (make-exn:subtype "subtyping failed" (current-continuation-marks) s t))
|
|
||||||
#;(error "inference failed" s t)]))
|
|
||||||
|
|
||||||
|
|
||||||
;; data structures for remembering things on recursive calls
|
;; data structures for remembering things on recursive calls
|
||||||
(define (empty-set) '())
|
(define (empty-set) '())
|
||||||
|
@ -94,19 +88,20 @@
|
||||||
(define (supertype-of-one/arr A s ts)
|
(define (supertype-of-one/arr A s ts)
|
||||||
(ormap (lambda (e) (arr-subtype*/no-fail A e s)) ts))
|
(ormap (lambda (e) (arr-subtype*/no-fail A e s)) ts))
|
||||||
|
|
||||||
(define (sub-eff e1 e2)
|
(define-syntax (subtype-seq stx)
|
||||||
(match* (e1 e2)
|
(define-syntax-class sub*
|
||||||
[(e e) #t]
|
(pattern e:expr))
|
||||||
[((Latent-Restrict-Effect: t) (Latent-Restrict-Effect: t*))
|
(syntax-parse stx
|
||||||
(and (subtype t t*)
|
[(_ init (s1:sub* . args1) (s:sub* . args) ...)
|
||||||
(subtype t* t))]
|
(with-syntax ([(A* ... A-last) (generate-temporaries #'(s1 s ...))])
|
||||||
[((Latent-Remove-Effect: t) (Latent-Remove-Effect: t*))
|
(with-syntax ([(clauses ...)
|
||||||
(and (subtype t t*)
|
(for/list ([s (syntax->list #'(s1 s ...))]
|
||||||
(subtype t* t))]
|
[args (syntax->list #'(args1 args ...))]
|
||||||
[(_ _) #f]))
|
[A (syntax->list #'(init A* ...))]
|
||||||
|
[A-next (syntax->list #'(A* ... A-last))])
|
||||||
;(trace sub-eff)
|
#`[A-next (#,s #,A . #,args)])])
|
||||||
|
#'(let* (clauses ...)
|
||||||
|
A-last)))]))
|
||||||
|
|
||||||
;; simple co/contra-variance for ->
|
;; simple co/contra-variance for ->
|
||||||
(define (arr-subtype*/no-fail A0 s t)
|
(define (arr-subtype*/no-fail A0 s t)
|
||||||
|
@ -115,11 +110,16 @@
|
||||||
(match (list s t)
|
(match (list s t)
|
||||||
;; top for functions is above everything
|
;; top for functions is above everything
|
||||||
[(list _ (top-arr:)) A0]
|
[(list _ (top-arr:)) A0]
|
||||||
[(list (arr: s1 s2 #f #f (list (cons kw s-kw-ty) ...) thn-eff els-eff)
|
[(list (arr: s1 s2 #f #f s-kws)
|
||||||
(arr: t1 t2 #f #f (list (cons kw t-kw-ty) ...) thn-eff els-eff))
|
(arr: t1 t2 #f #f t-kws))
|
||||||
(let* ([A1 (subtypes* A0 t1 s1)]
|
;; optional keywords are subtypes of required keywords
|
||||||
[A2 (subtypes* A1 t-kw-ty s-kw-ty)])
|
(unless (for/and ([s-r s-req] [t-r t-req])
|
||||||
(subtype* A1 s2 t2))]
|
(or (eq? s-r t-r) (not s-r)))
|
||||||
|
(fail! s t))
|
||||||
|
(subtype-seq A0
|
||||||
|
(subtypes* t1 s1)
|
||||||
|
(kw-subtypes* t-kws s-kws)
|
||||||
|
(subtype* s2 t2))]
|
||||||
[(list (arr: s1 s2 s3 #f (list (cons kw s-kw-ty) ...) thn-eff els-eff)
|
[(list (arr: s1 s2 s3 #f (list (cons kw s-kw-ty) ...) thn-eff els-eff)
|
||||||
(arr: t1 t2 t3 #f (list (cons kw t-kw-ty) ...) thn-eff* els-eff*))
|
(arr: t1 t2 t3 #f (list (cons kw t-kw-ty) ...) thn-eff* els-eff*))
|
||||||
(unless
|
(unless
|
Loading…
Reference in New Issue
Block a user