infer.rkt (8303B)
1 #lang turnstile/lang 2 (extends "ext-stlc.rkt" #:except define #%app λ ann) 3 (reuse inst #:from "sysf.rkt") 4 (require (only-in "sysf.rkt" ∀ ~∀ ∀? Λ)) 5 (reuse cons [head hd] [tail tl] nil [isnil nil?] List list #:from "stlc+cons.rkt") 6 ;(require (only-in "stlc+cons.rkt" ~List)) 7 (reuse tup × proj #:from "stlc+tup.rkt") 8 (reuse define-type-alias #:from "stlc+reco+var.rkt") 9 (require (for-syntax macrotypes/type-constraints)) 10 ;(provide hd tl nil? ∀) 11 12 (provide → ∀ define define/rec λ #%app) 13 14 ;; (Some [X ...] τ_body (Constraints (Constraint τ_1 τ_2) ...)) 15 (define-binding-type Some #:arity = 2) 16 (define-type-constructor Constraint #:arity = 2) 17 (define-type-constructor Constraints #:arity >= 0) 18 (define-syntax Cs 19 (syntax-parser 20 [(_ [a b] ...) 21 (Cs #'([a b] ...))])) 22 (begin-for-syntax 23 (define (?∀ Xs τ) 24 (if (stx-null? Xs) 25 τ 26 #`(∀ #,Xs #,τ))) 27 (define (?Some Xs τ cs) 28 (if (and (stx-null? Xs) (stx-null? cs)) 29 τ 30 #`(Some #,Xs #,τ (Cs #,@cs)))) 31 (define (Cs cs) 32 (syntax-parse cs 33 [([a b] ...) 34 #'(Constraints (Constraint a b) ...)])) 35 (define-syntax-class ?Some-form 36 #:attributes (Xs τ Cs) 37 [pattern (~Some Xs τ Cs)] 38 [pattern (~and τ (~not (~Some _ _ _))) 39 #:with Xs #'[] 40 #:with Cs ((current-type-eval) #'(Cs))]) 41 (define-syntax ~?∀ 42 (pattern-expander 43 (syntax-parser 44 [(?∀ Xs-pat τ-pat) 45 #'(~or (~∀ Xs-pat τ-pat) 46 (~and (~not (~∀ _ _)) 47 (~parse Xs-pat #'()) 48 τ-pat))]))) 49 (define-syntax ~?Some 50 (pattern-expander 51 (syntax-parser 52 [(?Some Xs-pat τ-pat Cs-pat) 53 #:with tmp (generate-temporary 'Some-form) 54 #:with tmp.Xs (format-id #'tmp "~a.Xs" #'tmp) 55 #:with tmp.τ (format-id #'tmp "~a.τ" #'tmp) 56 #:with tmp.Cs (format-id #'tmp "~a.Cs" #'tmp) 57 #'(~and (~var tmp ?Some-form) 58 (~parse Xs-pat #'tmp.Xs) 59 (~parse τ-pat #'tmp.τ) 60 (~parse Cs-pat #'tmp.Cs))]))) 61 (define-syntax ~Cs 62 (pattern-expander 63 (syntax-parser #:literals (...) 64 [(_ [a b] ooo:...) 65 #:with cs (generate-temporary) 66 #'(~and cs 67 (~parse (~Constraints (~Constraint a b) ooo) 68 (if (syntax-e #'cs) 69 #'cs 70 ((current-type-eval) #'(Cs)))))])))) 71 72 (begin-for-syntax 73 ;; find-free-Xs : (Stx-Listof Id) Type -> (Listof Id) 74 ;; finds the free Xs in the type 75 (define (find-free-Xs Xs ty) 76 (for/list ([X (in-list (stx->list Xs))] 77 #:when (stx-contains-id? ty X)) 78 X)) 79 80 ;; constrainable-X? : Id Solved-Constraints (Stx-Listof Id) -> Boolean 81 (define (constrainable-X? X cs Vs) 82 (for/or ([c (in-list (stx->list cs))]) 83 (or (free-identifier=? X (stx-car c)) 84 (and (member (stx-car c) Vs free-identifier=?) 85 (stx-contains-id? (stx-cadr c) X) 86 )))) 87 88 ;; find-constrainable-vars : (Stx-Listof Id) Solved-Constraints (Stx-Listof Id) -> (Listof Id) 89 (define (find-constrainable-vars Xs cs Vs) 90 (for/list ([X (in-list Xs)] #:when (constrainable-X? X cs Vs)) 91 X)) 92 93 ;; set-minus/Xs : (Listof Id) (Listof Id) -> (Listof Id) 94 (define (set-minus/Xs Xs Ys) 95 (for/list ([X (in-list Xs)] 96 #:when (not (member X Ys free-identifier=?))) 97 X)) 98 ;; set-intersect/Xs : (Listof Id) (Listof Id) -> (Listof Id) 99 (define (set-intersect/Xs Xs Ys) 100 (for/list ([X (in-list Xs)] 101 #:when (member X Ys free-identifier=?)) 102 X)) 103 104 ;; some/inst/generalize : (Stx-Listof Id) Type-Stx Constraints -> Type-Stx 105 (define (some/inst/generalize Xs* ty* cs1) 106 (define Xs (stx->list Xs*)) 107 (define cs2 (add-constraints/var? Xs identifier? '() cs1)) 108 (define Vs (set-minus/Xs (stx-map stx-car cs2) Xs)) 109 (define constrainable-vars 110 (find-constrainable-vars Xs cs2 Vs)) 111 (define constrainable-Xs 112 (set-intersect/Xs Xs constrainable-vars)) 113 (define concrete-constrained-vars 114 (for/list ([X (in-list constrainable-vars)] 115 #:when (empty? (find-free-Xs Xs (or (lookup X cs2) X)))) 116 X)) 117 (define unconstrainable-Xs 118 (set-minus/Xs Xs constrainable-Xs)) 119 (define ty (inst-type/cs/orig constrainable-vars cs2 ty* datum=?)) 120 ;; pruning constraints that are useless now 121 (define concrete-constrainable-Xs 122 (for/list ([X (in-list constrainable-Xs)] 123 #:when (empty? (find-free-Xs constrainable-Xs (or (lookup X cs2) X)))) 124 X)) 125 (define cs3 126 (for/list ([c (in-list cs2)] 127 #:when (not (member (stx-car c) concrete-constrainable-Xs free-identifier=?))) 128 c)) 129 (?Some 130 (set-minus/Xs constrainable-Xs concrete-constrainable-Xs) 131 (?∀ (find-free-Xs unconstrainable-Xs ty) ty) 132 cs3)) 133 134 (define (datum=? a b) 135 (equal? (syntax->datum a) (syntax->datum b))) 136 137 (define (tycons id args) 138 (define/syntax-parse [X ...] 139 (for/list ([arg (in-list (stx->list args))]) 140 (add-orig (generate-temporary arg) (get-orig arg)))) 141 (define/syntax-parse [arg ...] args) 142 (define/syntax-parse (~∀ (X- ...) body) 143 ((current-type-eval) #`(∀ (X ...) (#,id X ...)))) 144 (inst-type/cs #'[X- ...] #'([X- arg] ...) #'body)) 145 146 (define old-join (current-join)) 147 148 (define (new-join a b) 149 (syntax-parse (list a b) 150 [[(~?Some [X ...] A (~Cs [τ_1 τ_2] ...)) 151 (~?Some [Y ...] B (~Cs [τ_3 τ_4] ...))] 152 (define AB (old-join #'A #'B)) 153 (?Some #'[X ... Y ...] AB #'([τ_1 τ_2] ... [τ_3 τ_4] ...))])) 154 (current-join new-join) 155 ) 156 157 (define-typed-syntax λ 158 [(λ (x:id ...) body:expr) ≫ 159 #:with [X ...] 160 (for/list ([X (in-list (generate-temporaries #'[x ...]))]) 161 (add-orig X X)) 162 [([X ≫ X- :: #%type] ...) ([x ≫ x- : X] ...) 163 ⊢ [body ≫ body- ⇒ : τ_body*]] 164 #:with (~?Some [V ...] τ_body (~Cs [id_2 τ_2] ...)) (syntax-local-introduce #'τ_body*) 165 #:with τ_fn (some/inst/generalize #'[X- ... V ...] 166 #'(→ X- ... τ_body) 167 #'([id_2 τ_2] ...)) 168 -------- 169 [⊢ [_ ≫ (λ- (x- ...) body-) ⇒ : τ_fn]]]) 170 171 (define-typed-syntax #%app 172 [(_ e_fn e_arg ...) ≫ 173 #:with [A ...] (generate-temporaries #'[e_arg ...]) 174 #:with B (generate-temporary 'result) 175 [⊢ [e_fn ≫ e_fn- ⇒ : τ_fn*]] 176 #:with (~?Some [V1 ...] (~?∀ (V2 ...) τ_fn) (~Cs [τ_3 τ_4] ...)) 177 (syntax-local-introduce #'τ_fn*) 178 #:with τ_fn-expected (tycons #'→ #'[A ... B]) 179 [⊢ [e_arg ≫ e_arg- ⇒ : τ_arg*] ...] 180 #:with [(~?Some [V3 ...] (~?∀ (V4 ...) τ_arg) (~Cs [τ_5 τ_6] ...)) ...] 181 (syntax-local-introduce #'[τ_arg* ...]) 182 #:with τ_out (some/inst/generalize #'[A ... B V1 ... V2 ... V3 ... ... V4 ... ...] 183 #'B 184 #'([τ_fn-expected τ_fn] 185 [τ_3 τ_4] ... 186 [A τ_arg] ... 187 [τ_5 τ_6] ... ...)) 188 -------- 189 [⊢ [_ ≫ (#%app- e_fn- e_arg- ...) ⇒ : τ_out]]]) 190 191 (define-typed-syntax ann #:datum-literals (:) 192 [(ann e:expr : τ:type) ≫ 193 [⊢ [e ≫ e- ⇒ : τ_e]] 194 #:with (~?Some [V1 ...] (~?∀ (V2 ...) τ_fn) (~Cs [τ_1 τ_2] ...)) 195 (syntax-local-introduce #'τ_e) 196 #:with τ_e* (some/inst/generalize #'[V1 ... V2 ...] 197 #'τ.norm 198 #'([τ.norm τ_e] 199 [τ_1 τ_2] 200 ...)) 201 [τ_e* τ⊑ τ.norm #:for e] 202 -------- 203 [⊢ [_ ≫ e- ⇒ : τ.norm]]]) 204 205 (define-typed-syntax define 206 [(define x:id e:expr) ≫ 207 [⊢ [e ≫ e- ⇒ : τ_e]] 208 #:with tmp (generate-temporary #'x) 209 -------- 210 [_ ≻ (begin- 211 (define-syntax- x (make-rename-transformer (⊢ tmp : τ_e))) 212 (define- tmp e-))]]) 213 214 (define-typed-syntax define/rec #:datum-literals (:) 215 [(define/rec x:id : τ_x:type e:expr) ≫ 216 #:with tmp (generate-temporary #'x) 217 -------- 218 [_ ≻ (begin- 219 (define-syntax- x (make-rename-transformer (⊢ tmp : τ_x.norm))) 220 (define- tmp (ann e : τ_x.norm)))]])