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

Starting to add support for subtyping to mlish

Browse Source
This commit is contained in:
Georges Dupéron 2017-09-20 15:50:15 +02:00
parent 6d496741c6
commit 6e15e6a05b
2 changed files with 30 additions and 3 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

17
macrotypes/type-constraints.rkt
View File

@ -28,7 +28,16 @@
(member X Xs* free-identifier=?))
(add-constraints/var? Xs* X? substs new-cs orig-cs))
(define (add-constraints/var? Xs* var? substs new-cs [orig-cs new-cs])
;; Variance Type Type -> Boolean
(define (typecheck?/variance variance a-expected b-actual)
(cond
[(equal? variance covariant) (typecheck? b-actual a-expected)]
[(equal? variance contravariant) (typecheck? b-actual a-expected)]
;; invariant and irrelevant
[else (and (typecheck? a-expected b-actual)
(typecheck? b-actual a-expected))]))
(define (add-constraints/var? Xs* var? substs new-cs [orig-cs new-cs] [variance covariant]) ;; TODO: variance ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
(define Xs (stx->list Xs*))
(define Ys (stx-map stx-car substs))
(define-syntax-class var
@ -59,7 +68,8 @@
Xs
var?
;; Add the mapping #'a -> #'b to the substitution,
(add-substitution-entry entry substs)
(begin (displayln (list (type->str (car entry)) '-> (type->str (cadr entry)) 'with-substs substs))
(add-substitution-entry entry substs))
;; and substitute that in each of the constraints.
(cs-substitute-entry entry #'rst)
orig-cs)])]
@ -95,7 +105,7 @@
[else
(syntax-parse #'[a b]
[_
#:when (typecheck? #'a #'b)
#:when (typecheck?/variance variance #'a #'b)
(add-constraints/var? Xs
var?
substs
@ -110,6 +120,7 @@
#'((τ1 τ2) ... . rst)
orig-cs)]
[else
(displayln 2)
(type-error #:src (get-orig #'b)
#:msg (format "couldn't unify ~~a and ~~a\n expected: ~a\n given: ~a"
(string-join (map type->str (stx-map stx-car orig-cs)) ", ")

16
turnstile/examples/mlish.rkt
View File

@ -880,6 +880,9 @@
[⊢ e_fn ≫ e_fn- ⇒ (~?∀ Xs (~ext-stlc:→ . tyX_args))]
;; solve for type variables Xs
#:with [[e_arg- ...] Xs* cs] (solve #'Xs #'tyX_args this-syntax)
#:do {(newline)
(displayln "Solved argument types")
(map displayln (syntax->datum #'[[e_arg- ...] Xs* cs]))}
;; instantiate polymorphic function type
#:with [τ_in ... τ_out] (inst-types/cs #'Xs* #'cs #'tyX_args)
#:with (unsolved-X ...) (find-free-Xs #'Xs* #'τ_out)
@ -888,8 +891,20 @@
(num-args-fail-msg #'e_fn #'[τ_in ...] #'[e_arg ...])
;; compute argument types
#:with (τ_arg ...) (stx-map typeof #'(e_arg- ...))
#:do {(newline)
(displayln "Computed argument types")
(for ([a (in-syntax #'(τ_arg ...))]
[in (in-syntax #'(τ_in ...))]
[e (in-syntax #'(e_arg ...))])
(display 'a=) (displayln (type->str a))
(display 'i=) (displayln (type->str in))
(display 'e=) (displayln (syntax->datum e))
(display 'ck) (displayln (check? a in))
(newline))
(displayln "----")}
;; typecheck args
[τ_arg τ⊑ τ_in #:for e_arg] ...
#:do {(displayln "AAA")}
#:with τ_out* (if (stx-null? #'(unsolved-X ...))
#'τ_out
(syntax-parse #'τ_out
@ -903,6 +918,7 @@
(mk-app-poly-infer-error this-syntax #'(τ_in ...) #'(τ_arg ...) #'e_fn)
this-syntax)))
#'(∀ (unsolved-X ... Y ...) τ_out)]))
#:do {(displayln "BBB")}
--------
[⊢ (#%app- e_fn- e_arg- ...) ⇒ τ_out*]])