type keys now work, mostly
svn: r13580
This commit is contained in:
Sam Tobin-Hochstadt
parent
b5ccbb45bd
commit
e198478055
4
collects/typed-scheme/env/init-envs.ss
vendored
4
collects/typed-scheme/env/init-envs.ss
vendored
|
|
@ -32,9 +32,9 @@
|
|||
[(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))]
|
||||
[(? Type? (app (lambda (v) (vector->list (struct->vector v))) (list-rest tag seq vals)))
|
||||
[(? Type? (app (lambda (v) (vector->list (struct->vector v))) (list-rest tag key seq vals)))
|
||||
`(,(gen-constructor tag) ,@(map sub vals))]
|
||||
[(? Effect? (app (lambda (v) (vector->list (struct->vector v))) (list-rest tag seq vals)))
|
||||
[(? Effect? (app (lambda (v) (vector->list (struct->vector v))) (list-rest tag key seq vals)))
|
||||
`(,(gen-constructor tag) ,@(map sub vals))]
|
||||
[_ (basic v)]))
|
||||
|
||||
|
|
|
|||
|
|
@ -1,7 +1,7 @@
|
|||
#lang scheme/base
|
||||
(require "../utils/utils.ss")
|
||||
|
||||
(require (except-in (rep type-rep effect-rep) sub-eff)
|
||||
(require (except-in (rep type-rep effect-rep rep-utils) sub-eff)
|
||||
(utils tc-utils)
|
||||
"type-utils.ss"
|
||||
"type-comparison.ss"
|
||||
|
|
@ -156,139 +156,139 @@
|
|||
(define (subtype* A s t)
|
||||
(parameterize ([match-equality-test type-equal?]
|
||||
[current-seen A])
|
||||
(if (seen? s t)
|
||||
A
|
||||
(let* ([A0 (remember s t A)])
|
||||
(parameterize ([current-seen A0])
|
||||
#;(match t
|
||||
[(Name: n) (when (eq? 'heap (syntax-e n))
|
||||
(trace subtype*))]
|
||||
[_ #f])
|
||||
(let ([ks (Type-key s)] [kt (Type-key t)])
|
||||
(cond
|
||||
[(or (seen? s t) (type-equal? s t)) A]
|
||||
[(and (symbol? ks) (symbol? kt) (not (eq? ks kt))) (fail! s t)]
|
||||
[(and (symbol? ks) (pair? kt) (not (memq ks kt))) (fail! s t)]
|
||||
[(and (pair? ks) (pair? kt)
|
||||
(for/and ([i (in-list ks)]) (not (memq i kt))))
|
||||
(fail! s t)]
|
||||
[else
|
||||
(let* ([A0 (remember s t A)])
|
||||
(parameterize ([current-seen A0])
|
||||
(match (list s t)
|
||||
;; subtyping is reflexive
|
||||
[(list t t) A0]
|
||||
;; univ is top
|
||||
[(list _ (Univ:)) A0]
|
||||
;; error is top and bot
|
||||
[(list _ (Error:)) A0]
|
||||
[(list (Error:) _) A0]
|
||||
;; (Un) is bot
|
||||
[(list _ (Union: (list))) (fail! s t)]
|
||||
[(list (Union: (list)) _) A0]
|
||||
;; value types
|
||||
[(list (Value: v1) (Value: v2)) (=> unmatch) (if (equal? v1 v2) A0 (unmatch))]
|
||||
;; integers are numbers too
|
||||
[(list (Base: 'Integer _) (Base: 'Number _)) A0]
|
||||
;; values are subtypes of their "type"
|
||||
[(list (Value: (? integer? n)) (Base: 'Integer _)) A0]
|
||||
[(list (Value: (? number? n)) (Base: 'Number _)) A0]
|
||||
[(list (Value: (? boolean? n)) (Base: 'Boolean _)) A0]
|
||||
[(list (Value: (? symbol? n)) (Base: 'Symbol _)) A0]
|
||||
[(list (Value: (? string? n)) (Base: 'String _)) A0]
|
||||
;; tvars are equal if they are the same variable
|
||||
[(list (F: t) (F: t*)) (if (eq? t t*) A0 (fail! s t))]
|
||||
;; case-lambda
|
||||
[(list (Function: arr1) (Function: arr2))
|
||||
(when (null? arr1) (fail! s t))
|
||||
(let loop-arities ([A* A0]
|
||||
[arr2 arr2])
|
||||
(cond
|
||||
[(null? arr2) A*]
|
||||
[(supertype-of-one/arr A* (car arr2) arr1) => (lambda (A) (loop-arities A (cdr arr2)))]
|
||||
[else (fail! s t)]))]
|
||||
;; recur structurally on pairs
|
||||
[(list (Pair: a d) (Pair: a* d*))
|
||||
(let ([A1 (subtype* A0 a a*)])
|
||||
(and A1 (subtype* A1 d d*)))]
|
||||
;; quantification over two types preserves subtyping
|
||||
[(list (Poly: ns b1) (Poly: ms b2))
|
||||
(=> unmatch)
|
||||
(unless (= (length ns) (length ms))
|
||||
(unmatch))
|
||||
;(printf "Poly: ~n~a ~n~a~n" b1 (subst-all (map list ms (map make-F ns)) b2))
|
||||
(subtype* A0 b1 (subst-all (map list ms (map make-F ns)) b2))]
|
||||
;; use unification to see if we can use the polytype here
|
||||
[(list (Poly: vs b) s)
|
||||
(=> unmatch)
|
||||
(if (unify vs (list b) (list s)) A0 (unmatch))]
|
||||
[(list s (Poly: vs b))
|
||||
(=> unmatch)
|
||||
(if (null? (fv b)) (subtype* A0 s b) (unmatch))]
|
||||
;; names are compared for equality:
|
||||
[(list (Name: n) (Name: n*))
|
||||
(=> unmatch)
|
||||
(if (free-identifier=? n n*)
|
||||
A0
|
||||
(unmatch))]
|
||||
;; just unfold the recursive types
|
||||
[(list _ (? Mu?)) (subtype* A0 s (unfold t))]
|
||||
[(list (? Mu?) _) (subtype* A0 (unfold s) t)]
|
||||
;; for unions, we check the cross-product
|
||||
[(list (Union: es) t) (and (andmap (lambda (elem) (subtype* A0 elem t)) es) A0)]
|
||||
[(list s (Union: es)) (and (ormap (lambda (elem) (subtype*/no-fail A0 s elem)) es) A0)]
|
||||
;; subtyping on immutable structs is covariant
|
||||
[(list (Struct: nm _ flds #f _ _ _) (Struct: nm _ flds* #f _ _ _))
|
||||
(subtypes* A0 flds flds*)]
|
||||
[(list (Struct: nm _ flds proc _ _ _) (Struct: nm _ flds* proc* _ _ _))
|
||||
(subtypes* A0 (cons proc flds) (cons proc* flds*))]
|
||||
;; subtyping on structs follows the declared hierarchy
|
||||
[(list (Struct: nm (? Type? parent) flds proc _ _ _) other)
|
||||
;(printf "subtype - hierarchy : ~a ~a ~a~n" nm parent other)
|
||||
(subtype* A0 parent other)]
|
||||
;; applications and names are structs too
|
||||
[(list (App: (Name: n) args stx) other)
|
||||
(let ([t (lookup-type-name n)])
|
||||
(unless (Type? t)
|
||||
(fail! s t))
|
||||
#;(printf "subtype: app-name: name: ~a type: ~a other: ~a ~ninst: ~a~n" (syntax-e n) t other
|
||||
(instantiate-poly t args))
|
||||
(unless (Poly? t)
|
||||
(tc-error/stx stx "cannot apply non-polymorphic type ~a" t))
|
||||
(match t [(Poly-unsafe: n _)
|
||||
(unless (= n (length args))
|
||||
(tc-error/stx stx "wrong number of arguments to polymorphic type: expected ~a and got ~a"
|
||||
n (length args)))])
|
||||
(let ([v (subtype* A0 (instantiate-poly t args) other)])
|
||||
#;(printf "val: ~a~n" v)
|
||||
v))]
|
||||
[(list other (App: (Name: n) args stx))
|
||||
(let ([t (lookup-type-name n)])
|
||||
(unless (Type? t)
|
||||
(fail! s t))
|
||||
#;(printf "subtype: 2 app-name: name: ~a type: ~a other: ~a ~ninst: ~a~n" (syntax-e n) t other
|
||||
(instantiate-poly t args))
|
||||
(unless (Poly? t)
|
||||
(tc-error/stx stx "cannot apply non-polymorphic type ~a" t))
|
||||
(match t [(Poly-unsafe: n _)
|
||||
(unless (= n (length args))
|
||||
(tc-error/stx stx "wrong number of arguments to polymorphic type: expected ~a and got ~a"
|
||||
n (length args)))])
|
||||
;(printf "about to call subtype with: ~a ~a ~n" other (instantiate-poly t args))
|
||||
(let ([v (subtype* A0 other (instantiate-poly t args))])
|
||||
#;(printf "2 val: ~a~n" v)
|
||||
v))]
|
||||
[(list (Name: n) other)
|
||||
(let ([t (lookup-type-name n)])
|
||||
;(printf "subtype: name: ~a ~a ~a~n" (syntax-e n) t other)
|
||||
(if (Type? t)
|
||||
(subtype* A0 t other)
|
||||
(fail! s t)))]
|
||||
;; Promises are covariant
|
||||
[(list (Struct: 'Promise _ (list t) _ _ _ _) (Struct: 'Promise _ (list t*) _ _ _ _)) (subtype* A0 t t*)]
|
||||
;; subtyping on values is pointwise
|
||||
[(list (Values: vals1) (Values: vals2)) (subtypes* A0 vals1 vals2)]
|
||||
;; single values shouldn't actually happen, but they're just like the type
|
||||
[(list t (Values: (list t*))) (int-err "BUG - singleton values type~a" (make-Values (list t*)))]
|
||||
[(list (Values: (list t)) t*) (int-err "BUG - singleton values type~a" (make-Values (list t)))]
|
||||
;; subtyping on other stuff
|
||||
[(list (Syntax: t) (Syntax: t*))
|
||||
(subtype* A0 t t*)]
|
||||
[(list (Instance: t) (Instance: t*))
|
||||
(subtype* A0 t t*)]
|
||||
;; otherwise, not a subtype
|
||||
[_ (fail! s t) #;(printf "failed")]))))))
|
||||
[(list _ (Univ:)) A0]
|
||||
;; error is top and bot
|
||||
[(list _ (Error:)) A0]
|
||||
[(list (Error:) _) A0]
|
||||
;; (Un) is bot
|
||||
[(list _ (Union: (list))) (fail! s t)]
|
||||
[(list (Union: (list)) _) A0]
|
||||
;; value types
|
||||
[(list (Value: v1) (Value: v2)) (=> unmatch) (if (equal? v1 v2) A0 (unmatch))]
|
||||
;; integers are numbers too
|
||||
[(list (Base: 'Integer _) (Base: 'Number _)) A0]
|
||||
;; values are subtypes of their "type"
|
||||
[(list (Value: (? integer? n)) (Base: 'Integer _)) A0]
|
||||
[(list (Value: (? number? n)) (Base: 'Number _)) A0]
|
||||
[(list (Value: (? boolean? n)) (Base: 'Boolean _)) A0]
|
||||
[(list (Value: (? symbol? n)) (Base: 'Symbol _)) A0]
|
||||
[(list (Value: (? string? n)) (Base: 'String _)) A0]
|
||||
;; tvars are equal if they are the same variable
|
||||
[(list (F: t) (F: t*)) (if (eq? t t*) A0 (fail! s t))]
|
||||
;; case-lambda
|
||||
[(list (Function: arr1) (Function: arr2))
|
||||
(when (null? arr1) (fail! s t))
|
||||
(let loop-arities ([A* A0]
|
||||
[arr2 arr2])
|
||||
(cond
|
||||
[(null? arr2) A*]
|
||||
[(supertype-of-one/arr A* (car arr2) arr1) => (lambda (A) (loop-arities A (cdr arr2)))]
|
||||
[else (fail! s t)]))]
|
||||
;; recur structurally on pairs
|
||||
[(list (Pair: a d) (Pair: a* d*))
|
||||
(let ([A1 (subtype* A0 a a*)])
|
||||
(and A1 (subtype* A1 d d*)))]
|
||||
;; quantification over two types preserves subtyping
|
||||
[(list (Poly: ns b1) (Poly: ms b2))
|
||||
(=> unmatch)
|
||||
(unless (= (length ns) (length ms))
|
||||
(unmatch))
|
||||
;(printf "Poly: ~n~a ~n~a~n" b1 (subst-all (map list ms (map make-F ns)) b2))
|
||||
(subtype* A0 b1 (subst-all (map list ms (map make-F ns)) b2))]
|
||||
;; use unification to see if we can use the polytype here
|
||||
[(list (Poly: vs b) s)
|
||||
(=> unmatch)
|
||||
(if (unify vs (list b) (list s)) A0 (unmatch))]
|
||||
[(list s (Poly: vs b))
|
||||
(=> unmatch)
|
||||
(if (null? (fv b)) (subtype* A0 s b) (unmatch))]
|
||||
;; names are compared for equality:
|
||||
[(list (Name: n) (Name: n*))
|
||||
(=> unmatch)
|
||||
(if (free-identifier=? n n*)
|
||||
A0
|
||||
(unmatch))]
|
||||
;; just unfold the recursive types
|
||||
[(list _ (? Mu?)) (subtype* A0 s (unfold t))]
|
||||
[(list (? Mu?) _) (subtype* A0 (unfold s) t)]
|
||||
;; for unions, we check the cross-product
|
||||
[(list (Union: es) t) (and (andmap (lambda (elem) (subtype* A0 elem t)) es) A0)]
|
||||
[(list s (Union: es)) (and (ormap (lambda (elem) (subtype*/no-fail A0 s elem)) es) A0)]
|
||||
;; subtyping on immutable structs is covariant
|
||||
[(list (Struct: nm _ flds #f _ _ _) (Struct: nm _ flds* #f _ _ _))
|
||||
(subtypes* A0 flds flds*)]
|
||||
[(list (Struct: nm _ flds proc _ _ _) (Struct: nm _ flds* proc* _ _ _))
|
||||
(subtypes* A0 (cons proc flds) (cons proc* flds*))]
|
||||
;; subtyping on structs follows the declared hierarchy
|
||||
[(list (Struct: nm (? Type? parent) flds proc _ _ _) other)
|
||||
;(printf "subtype - hierarchy : ~a ~a ~a~n" nm parent other)
|
||||
(subtype* A0 parent other)]
|
||||
;; applications and names are structs too
|
||||
[(list (App: (Name: n) args stx) other)
|
||||
(let ([t (lookup-type-name n)])
|
||||
(unless (Type? t)
|
||||
(fail! s t))
|
||||
#;(printf "subtype: app-name: name: ~a type: ~a other: ~a ~ninst: ~a~n" (syntax-e n) t other
|
||||
(instantiate-poly t args))
|
||||
(unless (Poly? t)
|
||||
(tc-error/stx stx "cannot apply non-polymorphic type ~a" t))
|
||||
(match t [(Poly-unsafe: n _)
|
||||
(unless (= n (length args))
|
||||
(tc-error/stx stx "wrong number of arguments to polymorphic type: expected ~a and got ~a"
|
||||
n (length args)))])
|
||||
(let ([v (subtype* A0 (instantiate-poly t args) other)])
|
||||
#;(printf "val: ~a~n" v)
|
||||
v))]
|
||||
[(list other (App: (Name: n) args stx))
|
||||
(let ([t (lookup-type-name n)])
|
||||
(unless (Type? t)
|
||||
(fail! s t))
|
||||
#;(printf "subtype: 2 app-name: name: ~a type: ~a other: ~a ~ninst: ~a~n" (syntax-e n) t other
|
||||
(instantiate-poly t args))
|
||||
(unless (Poly? t)
|
||||
(tc-error/stx stx "cannot apply non-polymorphic type ~a" t))
|
||||
(match t [(Poly-unsafe: n _)
|
||||
(unless (= n (length args))
|
||||
(tc-error/stx stx "wrong number of arguments to polymorphic type: expected ~a and got ~a"
|
||||
n (length args)))])
|
||||
;(printf "about to call subtype with: ~a ~a ~n" other (instantiate-poly t args))
|
||||
(let ([v (subtype* A0 other (instantiate-poly t args))])
|
||||
#;(printf "2 val: ~a~n" v)
|
||||
v))]
|
||||
[(list (Name: n) other)
|
||||
(let ([t (lookup-type-name n)])
|
||||
;(printf "subtype: name: ~a ~a ~a~n" (syntax-e n) t other)
|
||||
(if (Type? t)
|
||||
(subtype* A0 t other)
|
||||
(fail! s t)))]
|
||||
;; Promises are covariant
|
||||
[(list (Struct: 'Promise _ (list t) _ _ _ _) (Struct: 'Promise _ (list t*) _ _ _ _)) (subtype* A0 t t*)]
|
||||
;; subtyping on values is pointwise
|
||||
[(list (Values: vals1) (Values: vals2)) (subtypes* A0 vals1 vals2)]
|
||||
;; single values shouldn't actually happen, but they're just like the type
|
||||
[(list t (Values: (list t*))) (int-err "BUG - singleton values type~a" (make-Values (list t*)))]
|
||||
[(list (Values: (list t)) t*) (int-err "BUG - singleton values type~a" (make-Values (list t)))]
|
||||
;; subtyping on other stuff
|
||||
[(list (Syntax: t) (Syntax: t*))
|
||||
(subtype* A0 t t*)]
|
||||
[(list (Instance: t) (Instance: t*))
|
||||
(subtype* A0 t t*)]
|
||||
;; otherwise, not a subtype
|
||||
[_ (fail! s t) #;(printf "failed")])))]))))
|
||||
|
||||
(define (type-compare? a b)
|
||||
(define (type-compare? a b)
|
||||
(and (subtype a b) (subtype b a)))
|
||||
|
||||
(provide subtype type-compare? subtypes/varargs subtypes)
|
||||
|
|
|
|||
|
|
@ -9,7 +9,7 @@
|
|||
;; FIXME - currently broken
|
||||
(define print-poly-types? #f)
|
||||
;; do we use simple type aliases in printing
|
||||
(define print-aliases #t)
|
||||
(define print-aliases #f)
|
||||
|
||||
;; does t have a type name associated with it currently?
|
||||
;; has-name : Type -> Maybe[Symbol]
|
||||
|
|
|
|||
|
|
@ -37,7 +37,7 @@
|
|||
(define (sb t) (substitute image name t))
|
||||
(if (hash-ref (free-vars* target) name #f)
|
||||
(type-case sb target
|
||||
[#:Union tys (Un (map sb tys))]
|
||||
;[#:Union tys (Un (map sb tys))]
|
||||
[#:F name* (if (eq? name* name) image target)]
|
||||
[#:arr dom rng rest drest kws thn-eff els-eff
|
||||
(begin
|
||||
|
|
|
|||
|
|
@ -53,7 +53,7 @@
|
|||
(if (andmap Values? types)
|
||||
(make-Values (apply map Un (map Values-types types)))
|
||||
(int-err "Un: should not take the union of multiple values with some other type: ~a" types))]
|
||||
[else (make-union* #;(remove-subtypes types) (foldr union2 (list (car types)) (remove-subtypes (cdr types))))]))]))
|
||||
[else (make-union* #;(remove-subtypes types) (foldr union2 (list) (remove-subtypes types)))]))]))
|
||||
|
||||
#;(defintern (Un-intern args) (lambda (_ args) (apply Un args)) args)
|
||||
|
||||
|
|
|
|||
|
|
@ -13,7 +13,7 @@
|
|||
syntax/stx
|
||||
(utils utils)))
|
||||
|
||||
(provide == dt de print-type* print-effect* Type Type? Effect Effect? defintern hash-id Type-seq Effect-seq)
|
||||
(provide == dt de print-type* print-effect* Type Type? Effect Effect? defintern hash-id Type-seq Effect-seq Type-key)
|
||||
|
||||
|
||||
|
||||
|
|
@ -25,9 +25,9 @@
|
|||
|
||||
|
||||
;; all types are Type?
|
||||
(define-struct/printer Type (seq) (lambda (a b c) ((unbox print-type*) a b c)))
|
||||
(define-struct/printer Type (seq key) (lambda (a b c) ((unbox print-type*) a b c)))
|
||||
|
||||
(define-struct/printer Effect (seq) (lambda (a b c) ((unbox print-effect*) a b c)))
|
||||
(define-struct/printer Effect (seq key) (lambda (a b c) ((unbox print-effect*) a b c)))
|
||||
|
||||
|
||||
|
||||
|
|
@ -44,31 +44,34 @@
|
|||
(define-syntaxes (dt de)
|
||||
(let ()
|
||||
(define (parse-opts opts stx)
|
||||
(let loop ([provide? #t] [intern? #f] [frees #t] [fold-rhs #f] [opts opts])
|
||||
(let loop ([provide? #t] [intern? #f] [frees #t] [fold-rhs #f] [key '(#f)] [opts opts])
|
||||
(cond
|
||||
[(null? opts) (values provide? intern? frees fold-rhs)]
|
||||
[(null? opts) (values provide? intern? frees fold-rhs key)]
|
||||
[(eq? '#:no-provide (syntax-e (stx-car opts)))
|
||||
(loop #f intern? frees fold-rhs (cdr opts))]
|
||||
(loop #f intern? frees fold-rhs key (cdr opts))]
|
||||
[(eq? '#:no-frees (syntax-e (stx-car opts)))
|
||||
(loop #f intern? #f fold-rhs (cdr opts))]
|
||||
(loop #f intern? #f fold-rhs key (cdr opts))]
|
||||
[(not (and (stx-pair? opts) (stx-pair? (stx-car opts))))
|
||||
(raise-syntax-error #f "bad options" stx)]
|
||||
[(eq? '#:intern (syntax-e (stx-car (car opts))))
|
||||
(loop provide? (stx-car (stx-cdr (car opts))) frees fold-rhs (cdr opts))]
|
||||
(loop provide? (stx-car (stx-cdr (car opts))) frees fold-rhs key (cdr opts))]
|
||||
[(eq? '#:frees (syntax-e (stx-car (car opts))))
|
||||
(loop provide? intern? (stx-cdr (car opts)) fold-rhs (cdr opts))]
|
||||
(loop provide? intern? (stx-cdr (car opts)) fold-rhs key (cdr opts))]
|
||||
[(eq? '#:fold-rhs (syntax-e (stx-car (car opts))))
|
||||
(loop provide? intern? frees (stx-cdr (car opts)) (cdr opts))]
|
||||
(loop provide? intern? frees (stx-cdr (car opts)) key (cdr opts))]
|
||||
[(eq? '#:key (syntax-e (stx-car (car opts))))
|
||||
(loop provide? intern? frees fold-rhs (stx-cdr (car opts)) (cdr opts))]
|
||||
[else (raise-syntax-error #f "bad options" stx)])))
|
||||
(define (mk par ht-stx)
|
||||
(lambda (stx)
|
||||
(syntax-case stx ()
|
||||
[(dform nm flds . opts)
|
||||
(let*-values ([(provide? intern? frees fold-rhs) (parse-opts (syntax->list #'opts) #'opts)]
|
||||
(let*-values ([(provide? intern? frees fold-rhs key-expr) (parse-opts (syntax->list #'opts) #'opts)]
|
||||
[(kw) (string->keyword (symbol->string (syntax-e #'nm)))])
|
||||
(with-syntax*
|
||||
([ex (id #'nm #'nm ":")]
|
||||
[kw-stx kw]
|
||||
[(key-expr) key-expr]
|
||||
[parent par]
|
||||
[(s:ty maker pred acc ...) (build-struct-names #'nm (syntax->list #'flds) #f #t #'nm)]
|
||||
[(flds* ...) #'flds]
|
||||
|
|
@ -82,7 +85,12 @@
|
|||
#'(lambda (tr er)
|
||||
#'fr))]
|
||||
[fold-rhs (raise-syntax-error fold-rhs "something went wrong")]
|
||||
[else #'(lambda (type-rec-id effect-rec-id) #`(*maker (#,type-rec-id flds*) ...))])]
|
||||
[else #'(lambda (type-rec-id effect-rec-id)
|
||||
#;
|
||||
(printf "about to call ~a with ~a args~n"
|
||||
'*maker
|
||||
(length '(flds* ...)))
|
||||
#`(*maker (#,type-rec-id flds*) ...))])]
|
||||
[provides (if provide?
|
||||
#`(begin
|
||||
(provide ex pred acc ...)
|
||||
|
|
@ -90,19 +98,18 @@
|
|||
#'(begin))]
|
||||
[intern (cond
|
||||
[(syntax? intern?)
|
||||
#`(defintern (**maker . flds) maker #,intern?)]
|
||||
#`(defintern (**maker key . flds) maker #,intern?)]
|
||||
[(null? (syntax-e #'flds))
|
||||
#'(defintern (**maker . flds) maker #f)]
|
||||
[(stx-null? (stx-cdr #'flds)) #'(defintern (**maker . flds) maker . flds)]
|
||||
[else #'(defintern (**maker . flds) maker (list . flds))])]
|
||||
#'(defintern (**maker key . flds) maker #f)]
|
||||
[(stx-null? (stx-cdr #'flds)) #'(defintern (**maker key . flds) maker . flds)]
|
||||
[else #'(defintern (**maker key . flds) maker (list . flds))])]
|
||||
[frees (cond
|
||||
[(not frees) #'(begin)]
|
||||
;; we know that this has no free vars
|
||||
[(and (pair? frees) (syntax? (car frees)) (not (syntax-e (car frees))))
|
||||
(syntax/loc stx
|
||||
(define (*maker . flds)
|
||||
(define v (**maker . flds))
|
||||
#;(printf "~a entered in #f case~n" '*maker)
|
||||
(define v (**maker key-expr . flds))
|
||||
(unless-in-table
|
||||
var-table v
|
||||
(hash-set! var-table v empty-hash-table)
|
||||
|
|
@ -113,16 +120,14 @@
|
|||
[(and (pair? frees) (pair? (cdr frees)))
|
||||
(quasisyntax/loc
|
||||
stx
|
||||
(define (*maker . flds)
|
||||
(define v (**maker . flds))
|
||||
#;(printf "~a entered in expr case ~n~a~n~a ~n" '*maker '#,(car frees) '#,(cadr frees))
|
||||
(define (*maker . flds)
|
||||
(define v (**maker key-expr . flds))
|
||||
#,
|
||||
(quasisyntax/loc (car frees)
|
||||
(unless-in-table
|
||||
var-table v
|
||||
(hash-set! var-table v #,(car frees))
|
||||
(hash-set! index-table v #,(cadr frees))))
|
||||
#;(printf "~a exited in expr case~n" '*maker)
|
||||
v))]
|
||||
[else
|
||||
(let
|
||||
|
|
@ -134,8 +139,7 @@
|
|||
[(e ...) #`(combine-frees (list (#,f e) ...))]))])
|
||||
(quasisyntax/loc stx
|
||||
(define (*maker . flds)
|
||||
(define v (**maker . flds))
|
||||
#;(printf "~a entered in default case~n" '*maker)
|
||||
(define v (**maker key-expr . flds))
|
||||
(unless-in-table
|
||||
var-table v
|
||||
(define fvs #,(combiner #'free-vars* #'flds))
|
||||
|
|
@ -150,7 +154,7 @@
|
|||
(...
|
||||
(syntax-case s ()
|
||||
[(__ . fs)
|
||||
(with-syntax ([flds** (syntax/loc s (_ . fs))])
|
||||
(with-syntax ([flds** (syntax/loc s (_ _ . fs))])
|
||||
(quasisyntax/loc s (struct nm flds**)))]))))
|
||||
(begin-for-syntax
|
||||
(hash-set! ht-stx 'kw-stx (list #'ex #'flds bfs-fold-rhs #'#,stx)))
|
||||
|
|
|
|||
|
|
@ -13,7 +13,7 @@
|
|||
;; Type is defined in rep-utils.ss
|
||||
|
||||
;; t must be a Type
|
||||
(dt Scope (t))
|
||||
(dt Scope (t) [#:key (Type-key t)])
|
||||
|
||||
;; this is ONLY used when a type error ocurrs
|
||||
(dt Error () [#:frees #f] [#:fold-rhs #:base])
|
||||
|
|
@ -41,39 +41,52 @@
|
|||
stx)])
|
||||
|
||||
;; left and right are Types
|
||||
(dt Pair (left right))
|
||||
(dt Pair (left right) [#:key 'pair])
|
||||
|
||||
;; elem is a Type
|
||||
(dt Vector (elem) [#:frees (make-invariant (free-vars* elem)) (make-invariant (free-idxs* elem))])
|
||||
(dt Vector (elem)
|
||||
[#:frees (make-invariant (free-vars* elem)) (make-invariant (free-idxs* elem))]
|
||||
[#:key 'vector])
|
||||
|
||||
;; elem is a Type
|
||||
(dt Box (elem) [#:frees (make-invariant (free-vars* elem)) (make-invariant (free-idxs* elem))])
|
||||
(dt Box (elem) [#:frees (make-invariant (free-vars* elem)) (make-invariant (free-idxs* elem))]
|
||||
[#:key 'box])
|
||||
|
||||
;; name is a Symbol (not a Name)
|
||||
(dt Base (name contract) [#:frees #f] [#:fold-rhs #:base] [#:intern name])
|
||||
(dt Base (name contract) [#:frees #f] [#:fold-rhs #:base] [#:intern name]
|
||||
[#:key (case name
|
||||
[(Number Integer) 'number]
|
||||
[(Boolean) 'boolean]
|
||||
[(String) 'string]
|
||||
[(Symbol) 'symbol]
|
||||
[(Keyword) 'keyword]
|
||||
[else #f])])
|
||||
|
||||
;; body is a Scope
|
||||
(dt Mu (body) #:no-provide [#:frees (free-vars* body) (without-below 1 (free-idxs* body))]
|
||||
[#:fold-rhs (*Mu (*Scope (type-rec-id (Scope-t body))))])
|
||||
[#:fold-rhs (*Mu (*Scope (type-rec-id (Scope-t body))))]
|
||||
[#:key (Type-key body)])
|
||||
|
||||
;; n is how many variables are bound here
|
||||
;; body is a Scope
|
||||
(dt Poly (n body) #:no-provide
|
||||
[#:frees (free-vars* body) (without-below n (free-idxs* body))]
|
||||
[#:fold-rhs (let ([body* (remove-scopes n body)])
|
||||
(*Poly n (add-scopes n (type-rec-id body*))))])
|
||||
(*Poly n (add-scopes n (type-rec-id body*))))]
|
||||
[#:key (Type-key body)])
|
||||
|
||||
;; n is how many variables are bound here
|
||||
;; there are n-1 'normal' vars and 1 ... var
|
||||
;; body is a Scope
|
||||
(dt PolyDots (n body) #:no-provide
|
||||
[#:key (Type-key body)]
|
||||
[#:frees (free-vars* body) (without-below n (free-idxs* body))]
|
||||
[#:fold-rhs (let ([body* (remove-scopes n body)])
|
||||
(*PolyDots n (add-scopes n (type-rec-id body*))))])
|
||||
|
||||
;; pred : identifier
|
||||
;; cert : syntax certifier
|
||||
(dt Opaque (pred cert) [#:intern (hash-id pred)] [#:frees #f] [#:fold-rhs #:base])
|
||||
(dt Opaque (pred cert) [#:intern (hash-id pred)] [#:frees #f] [#:fold-rhs #:base] [#:key pred])
|
||||
|
||||
;; name : symbol
|
||||
;; parent : Struct
|
||||
|
|
@ -92,7 +105,8 @@
|
|||
(and proc (type-rec-id proc))
|
||||
poly?
|
||||
pred-id
|
||||
cert)])
|
||||
cert)]
|
||||
[#:key (gensym)])
|
||||
|
||||
;; kw : keyword?
|
||||
;; ty : Type
|
||||
|
|
@ -100,7 +114,8 @@
|
|||
(dt Keyword (kw ty required?)
|
||||
[#:frees (free-vars* ty)
|
||||
(free-idxs* ty)]
|
||||
[#:fold-rhs (*Keyword kw (type-rec-id ty) required?)])
|
||||
[#:fold-rhs (*Keyword kw (type-rec-id ty) required?)]
|
||||
[#:key 'keyword])
|
||||
|
||||
;; dom : Listof[Type]
|
||||
;; rng : Type
|
||||
|
|
@ -112,6 +127,7 @@
|
|||
;; els-eff : Effect
|
||||
;; arr is NOT a Type
|
||||
(dt arr (dom rng rest drest kws thn-eff els-eff)
|
||||
[#:key 'procedure]
|
||||
[#:frees (combine-frees (append (map flip-variances (map free-vars* (append (if rest (list rest) null)
|
||||
(map Keyword-ty kws)
|
||||
dom)))
|
||||
|
|
@ -153,13 +169,22 @@
|
|||
[#:fold-rhs (*Function (map type-rec-id arities))])
|
||||
|
||||
;; v : Scheme Value
|
||||
(dt Value (v) [#:frees #f] [#:fold-rhs #:base])
|
||||
(dt Value (v) [#:frees #f] [#:fold-rhs #:base] [#:key (cond [(number? v) 'number]
|
||||
[(boolean? v) 'boolean]
|
||||
[(null? v) 'null]
|
||||
[else #f])])
|
||||
|
||||
;; elems : Listof[Type]
|
||||
(dt Union (elems) [#:frees (combine-frees (map free-vars* elems))
|
||||
(combine-frees (map free-idxs* elems))]
|
||||
[#:fold-rhs ((get-union-maker) (map type-rec-id elems))])
|
||||
|
||||
[#:fold-rhs ((get-union-maker) (map type-rec-id elems))]
|
||||
[#:key (let loop ([res null] [ts elems])
|
||||
(if (null? ts) res
|
||||
(let ([k (Type-key (car ts))])
|
||||
(cond [(pair? k) (loop (append k res) (cdr ts))]
|
||||
[k (loop (cons k res) (cdr ts))]
|
||||
[else #f]))))])
|
||||
|
||||
(dt Univ () [#:frees #f] [#:fold-rhs #:base])
|
||||
|
||||
;; types : Listof[Type]
|
||||
|
|
@ -167,23 +192,25 @@
|
|||
#:no-provide
|
||||
[#:frees (combine-frees (map free-vars* types))
|
||||
(combine-frees (map free-idxs* types))]
|
||||
[#:fold-rhs (*Values (map type-rec-id types))])
|
||||
[#:fold-rhs (*Values (map type-rec-id types))]
|
||||
[#:key 'values])
|
||||
|
||||
(dt ValuesDots (types dty dbound)
|
||||
[#:frees (combine-frees (map free-vars* (cons dty types)))
|
||||
(combine-frees (map free-idxs* (cons dty types)))]
|
||||
[#:fold-rhs (*ValuesDots (map type-rec-id types) (type-rec-id dty) dbound)])
|
||||
[#:fold-rhs (*ValuesDots (map type-rec-id types) (type-rec-id dty) dbound)]
|
||||
[#:key 'values])
|
||||
|
||||
;; in : Type
|
||||
;; out : Type
|
||||
(dt Param (in out))
|
||||
(dt Param (in out) [#:key 'parameter])
|
||||
|
||||
;; key : Type
|
||||
;; value : Type
|
||||
(dt Hashtable (key value))
|
||||
(dt Hashtable (key value) [#:key 'hash])
|
||||
|
||||
;; t : Type
|
||||
(dt Syntax (t))
|
||||
(dt Syntax (t) [#:key 'syntax])
|
||||
|
||||
;; pos-flds : (Listof Type)
|
||||
;; name-flds : (Listof (Tuple Symbol Type Boolean))
|
||||
|
|
@ -197,7 +224,7 @@
|
|||
(map free-idxs* (append pos-flds
|
||||
(map cadr name-flds)
|
||||
(map cadr methods))))]
|
||||
|
||||
[#:key 'class]
|
||||
[#:fold-rhs (match (list pos-flds name-flds methods)
|
||||
[(list
|
||||
pos-tys
|
||||
|
|
@ -211,7 +238,7 @@
|
|||
(map list mname (map type-rec-id mty)))])])
|
||||
|
||||
;; cls : Class
|
||||
(dt Instance (cls))
|
||||
(dt Instance (cls) [#:key 'instance])
|
||||
|
||||
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
|
||||
|
||||
|
|
|
|||
|
|
@ -166,16 +166,27 @@
|
|||
[(_ val)
|
||||
#'(? (lambda (x) (equal? val x)))])))
|
||||
|
||||
(define-for-syntax printing? #t)
|
||||
(define-for-syntax printing? #f)
|
||||
|
||||
(define print-type* (box (lambda _ (error "print-type* not yet defined"))))
|
||||
(define print-effect* (box (lambda _ (error "print-effect* not yet defined"))))
|
||||
|
||||
(require scheme/pretty mzlib/pconvert)
|
||||
|
||||
(define-syntax (define-struct/printer stx)
|
||||
(syntax-case stx ()
|
||||
[(form name (flds ...) printer)
|
||||
#`(define-struct/properties name (flds ...)
|
||||
#,(if printing? #'([prop:custom-write printer]) #'())
|
||||
#,(if printing?
|
||||
#'([prop:custom-write printer])
|
||||
#'([prop:custom-write (lambda (s port mode)
|
||||
(parameterize ([current-output-port port]
|
||||
[show-sharing #f]
|
||||
[booleans-as-true/false #f]
|
||||
[constructor-style-printing #t])
|
||||
(newline)
|
||||
(pretty-print (print-convert s))
|
||||
(newline)))]))
|
||||
#f)]))
|
||||
|
||||
(define (id kw . args)
|
||||
|
|
|
|||
Loading…
Reference in New Issue
Block a user