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

refactor type-constraints a bit

Browse Source
This commit is contained in:
AlexKnauth 2016-06-24 12:25:07 -04:00
parent 103086a62c
commit da3ecfa780
4 changed files with 23 additions and 10 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

2
macrotypes/examples/infer.rkt
View File

@ -47,7 +47,7 @@
(define (solve Xs args expected-τs)
(let-values
([(cs e+τs)
(for/fold ([cs #'()] [e+τs #'()])
(for/fold ([cs '()] [e+τs #'()])
([e_arg (syntax->list args)]
[τ_inX (syntax->list expected-τs)])
(define τ_in (inst-type/cs Xs cs τ_inX))

2
macrotypes/examples/mlish.rkt
View File

@ -90,7 +90,7 @@
(define initial-cs
(if (and (syntax-e #'expected-ty) (stx-null? #'Vs))
(add-constraints Xs '() (list (list #'expected-ty #'τ_outX)))
#'()))
'()))
(syntax-parse stx
[(_ e_fn . args)
(define-values (as- cs)

27
macrotypes/type-constraints.rkt
View File

@ -43,17 +43,13 @@
#'rst)
orig-cs)]
[else
(define entry (list #'a #'b))
(add-constraints
Xs*
;; Add the mapping #'a -> #'b to the substitution,
(cons (list #'a #'b)
(for/list ([subst (in-list (stx->list substs))])
(list (stx-car subst)
(inst-type (list #'b) (list #'a) (stx-cadr subst)))))
(add-substitution-entry entry substs)
;; and substitute that in each of the constraints.
(for/list ([c (in-list (syntax->list #'rst))])
(list (inst-type (list #'b) (list #'a) (stx-car c))
(inst-type (list #'b) (list #'a) (stx-cadr c))))
(cs-substitute-entry entry #'rst)
orig-cs)])]
[([a b:var] . rst)
(add-constraints Xs*
@ -104,6 +100,23 @@
(string-join (map type->str (stx-map stx-cadr orig-cs)) ", "))
#'a #'b)])])]))
;; add-substitution-entry : (List Id Type) (Listof (List Id Type)) -> (Listof (List Id Type))
;; Adds the mapping a -> b to the substitution and substitutes for it in the other entries
(define (add-substitution-entry entry substs)
(match-define (list a b) entry)
(cons entry
(for/list ([subst (in-list substs)])
(list (first subst)
(inst-type (list b) (list a) (second subst))))))
;; cs-substitute-entry : (List Id Type) (Stx-Listof (Stx-List Stx Stx)) -> (Listof (List Stx Stx))
;; substitute a -> b in each of the constraints
(define (cs-substitute-entry entry cs)
(match-define (list a b) entry)
(for/list ([c (in-list (stx->list cs))])
(list (inst-type (list b) (list a) (stx-car c))
(inst-type (list b) (list a) (stx-cadr c)))))
(define (lookup x substs)
(syntax-parse substs
[((y:id τ) . rst)

2
turnstile/examples/mlish.rkt
View File

@ -90,7 +90,7 @@
(define initial-cs
(if (and (syntax-e #'expected-ty) (stx-null? #'Vs))
(add-constraints Xs '() (list (list #'expected-ty #'τ_outX)))
#'()))
'()))
(syntax-parse stx
[(_ e_fn . args)
(define-values (as- cs)