mlish+adhoc.rkt (77283B)
1 #lang turnstile 2 (require (postfix-in - racket/fixnum) (postfix-in - racket/flonum)) 3 4 (extends 5 "ext-stlc.rkt" 6 #:except → #%app λ define begin #%datum 7 + - * void = zero? sub1 add1 not let let* and 8 #:rename [~→ ~ext-stlc:→]) 9 (require (rename-in (only-in "sysf.rkt" inst) [inst sysf:inst])) 10 (require (only-in "ext-stlc.rkt" →?)) 11 (require (only-in "sysf.rkt" ~∀ ∀ ∀? Λ)) 12 (reuse × tup proj define-type-alias #:from "stlc+rec-iso.rkt") 13 (require (only-in "stlc+rec-iso.rkt" ~× ×?)) ; using current-type=? from here 14 (provide (rename-out [ext-stlc:and and] [ext-stlc:#%datum #%datum])) 15 (reuse member length reverse list-ref cons nil isnil head tail list #:from "stlc+cons.rkt") 16 (require (prefix-in stlc+cons: (only-in "stlc+cons.rkt" list cons nil))) 17 (require (only-in "stlc+cons.rkt" ~List List? List)) 18 (reuse ref deref := Ref #:from "stlc+box.rkt") 19 (require (rename-in (only-in "stlc+reco+var.rkt" tup proj ×) 20 [tup rec] [proj get] [× ××])) 21 (provide rec get ××) 22 ;; for pattern matching 23 (require (prefix-in stlc+cons: (only-in "stlc+cons.rkt" list))) 24 (require (prefix-in stlc+tup: (only-in "stlc+tup.rkt" tup))) 25 26 ;; ML-like language + ad-hoc polymorphism 27 ;; - top level recursive functions 28 ;; - user-definable algebraic datatypes 29 ;; - pattern matching 30 ;; - (local) type inference 31 ;; 32 ;; - type classes 33 34 (provide → →/test => =>/test 35 List Channel Thread Vector Sequence Hash String-Port Input-Port Regexp 36 define-type define-typeclass define-instance 37 match2) 38 39 (define-type-constructor => #:arity > 0) 40 41 ;; providing version of define-typed-syntax 42 (define-syntax (define-typed-syntax stx) 43 (syntax-parse stx 44 [(_ name:id #:export-as out-name:id . rst) 45 #'(begin- 46 (provide- (rename-out [name out-name])) 47 (define-typerule name . rst))] ; define-typerule doesnt provide 48 [(_ name:id . rst) 49 #'(define-typed-syntax name #:export-as name . rst)] 50 [(_ (name:id . pat) . rst) 51 #'(define-typed-syntax name #:export-as name [(_ . pat) . rst])])) 52 53 ;; type class helper fns 54 (begin-for-syntax 55 (define (mk-app-err-msg stx #:expected [expected-τs #'()] 56 #:given [given-τs #'()] 57 #:note [note ""] 58 #:name [name #f] 59 #:action [other #f]) 60 (syntax-parse stx 61 #;[(app . rst) 62 #:when (not (equal? '#%app (syntax->datum #'app))) 63 (mk-app-err-msg (syntax/loc stx (#%app app . rst)) 64 #:expected expected-τs 65 #:given given-τs 66 #:note note 67 #:name name)] 68 [(app e_fn e_arg ...) 69 (define fn-name 70 (if name name 71 (format "function ~a" 72 (syntax->datum (or (get-orig #'e_fn) #'e_fn))))) 73 (define action (if other other "applying")) 74 (string-append 75 (format "~a (~a:~a):\nType error " 76 (syntax-source stx) (syntax-line stx) (syntax-column stx)) 77 action " " 78 fn-name ". " note "\n" 79 (format " Expected: ~a argument(s) with type(s): " (stx-length expected-τs)) 80 (types->str expected-τs) "\n" 81 " Given:\n" 82 (string-join 83 (map (λ (e t) (format " ~a : ~a" e t)) ; indent each line 84 (syntax->datum #'(e_arg ...)) 85 (if (stx-length=? #'(e_arg ...) given-τs) 86 (stx-map type->str given-τs) 87 (stx-map (lambda (e) "?") #'(e_arg ...)))) 88 "\n") 89 "\n")])) 90 (define (type-hash-code tys) ; tys should be fully expanded 91 (equal-hash-code (syntax->datum (if (syntax? tys) tys #`#,tys)))) 92 (define (mangle o tys) 93 (format-id o "~a~a" o (type-hash-code tys))) 94 ;; pattern expander for type class 95 (define-syntax ~TC 96 (pattern-expander 97 (syntax-parser 98 [(_ [generic-op ty-concrete-op] (~and ooo (~literal ...))) 99 #'(_ (_ (_ generic-op) ty-concrete-op) ooo)] 100 [(_ . ops+tys) 101 #:with expanded (generate-temporary) 102 #'(~and expanded 103 (~parse (_ (_ (_ gen-op) ty-op) (... ...)) 104 #'expanded) 105 (~parse ops+tys #'((gen-op ty-op) (... ...))))]))) 106 (define-syntax ~TC-base 107 (pattern-expander 108 (syntax-parser 109 [(_ . pat) 110 #:with expanded (generate-temporary) 111 #'(~and expanded 112 (~parse ((~TC . pat) . _) (flatten-TC #'expanded)))]))) 113 (define-syntax ~TCs 114 (pattern-expander 115 (syntax-parser 116 ;; pat should be of shape ([op ty] ...) 117 [(_ pat (~and ooo (~literal ...))) 118 #:with expanded (generate-temporary) 119 ;; (stx-map (compose remove-dups flatten-TC) #'expanded) 120 ;; produces [List [List [List op+ty]]] 121 ;; - inner [List op+ty] is from the def of a TC 122 ;; - second List is from the flattened subclass TCs 123 ;; - outer List is bc this pattern matces multiple TCs 124 ;; This pattern expander collapses the inner two Lists 125 #'(~and expanded 126 (~parse (((~TC [op ty] (... ...)) (... ...)) ooo) 127 (stx-map (compose remove-dups flatten-TC) #'expanded)) 128 (~parse (pat ooo) #'(([op ty] (... ...) (... ...)) ooo)))]))) 129 (define (flatten-TC TC) 130 (syntax-parse TC 131 [(~=> sub-TC ... base-TC) 132 (cons #'base-TC (stx-appendmap flatten-TC #'(sub-TC ...)))])) 133 (define (remove-dups TCs) 134 (syntax-parse TCs 135 [() #'()] 136 [(TC . rst) 137 (cons #'TC (stx-filter (lambda (s) (not (typecheck? s #'TC))) (remove-dups #'rst)))]))) 138 ;; type inference constraint solving 139 (begin-for-syntax 140 ;; matching possibly polymorphic types 141 (define-syntax ~?∀ 142 (pattern-expander 143 (lambda (stx) 144 (syntax-case stx () 145 [(?∀ vars-pat body-pat) 146 #'(~or (~∀ vars-pat body-pat) 147 (~and (~not (~∀ _ _)) 148 (~parse vars-pat #'()) 149 body-pat))])))) 150 151 ;; type inference constraint solving 152 (define (compute-constraint τ1-τ2) 153 (syntax-parse τ1-τ2 154 [(X:id τ) #'((X τ))] 155 [((~Any tycons1 τ1 ...) (~Any tycons2 τ2 ...)) 156 #:when (typecheck? #'tycons1 #'tycons2) 157 (compute-constraints #'((τ1 τ2) ...))] 158 ; should only be monomorphic? 159 [((~∀ () (~ext-stlc:→ τ1 ...)) (~∀ () (~ext-stlc:→ τ2 ...))) 160 (compute-constraints #'((τ1 τ2) ...))] 161 [_ #'()])) 162 (define (compute-constraints τs) 163 (stx-appendmap compute-constraint τs)) 164 165 (define (solve-constraint x-τ) 166 (syntax-parse x-τ 167 [(X:id τ) #'((X τ))] 168 [_ #'()])) 169 (define (solve-constraints cs) 170 (stx-appendmap compute-constraint cs)) 171 172 (define (lookup x substs) 173 (syntax-parse substs 174 [((y:id τ) . rst) 175 #:when (free-identifier=? #'y x) 176 #'τ] 177 [(_ . rst) (lookup x #'rst)] 178 [() #f])) 179 180 ;; find-unsolved-Xs : (Stx-Listof Id) Constraints -> (Listof Id) 181 ;; finds the free Xs that aren't constrained by cs 182 (define (find-unsolved-Xs Xs cs) 183 (for/list ([X (in-list (stx->list Xs))] 184 #:when (not (lookup X cs))) 185 X)) 186 187 ;; lookup-Xs/keep-unsolved : (Stx-Listof Id) Constraints -> (Listof Type-Stx) 188 ;; looks up each X in the constraints, returning the X if it's unconstrained 189 (define (lookup-Xs/keep-unsolved Xs cs) 190 (for/list ([X (in-list (stx->list Xs))]) 191 (or (lookup X cs) X))) 192 193 ;; solve for Xs by unifying quantified fn type with the concrete types of stx's args 194 ;; stx = the application stx = (#%app e_fn e_arg ...) 195 ;; tyXs = input and output types from fn type 196 ;; ie (typeof e_fn) = (-> . tyXs) 197 ;; It infers the types of arguments from left-to-right, 198 ;; and it short circuits if it's done early. 199 ;; It returns list of 3 values if successful, else throws a type error 200 ;; - a list of the arguments that it expanded 201 ;; - a list of the the un-constrained type variables 202 ;; - the constraints for substituting the types 203 (define (solve Xs tyXs stx) 204 (syntax-parse tyXs 205 [(τ_inX ... τ_outX) 206 ;; generate initial constraints with expected type and τ_outX 207 #:with expected-ty (get-expected-type stx) 208 (define initial-cs 209 (if (syntax-e #'expected-ty) 210 (compute-constraint (list #'τ_outX ((current-type-eval) #'expected-ty))) 211 #'())) 212 (syntax-parse stx 213 [(_ e_fn . args) 214 (define-values (as- cs) 215 (for/fold ([as- null] [cs initial-cs]) 216 ([a (in-list (syntax->list #'args))] 217 [tyXin (in-list (syntax->list #'(τ_inX ...)))] 218 #:break (empty? (find-unsolved-Xs Xs cs))) 219 (define/with-syntax [a- ty_a] (infer+erase a)) 220 (values 221 (cons #'a- as-) 222 (stx-append cs (compute-constraint (list tyXin #'ty_a)))))) 223 224 (list (reverse as-) (find-unsolved-Xs Xs cs) cs)])])) 225 226 (define (raise-app-poly-infer-error stx expected-tys given-tys e_fn) 227 (type-error #:src stx 228 #:msg (mk-app-err-msg stx #:expected expected-tys #:given given-tys 229 #:note (format "Could not infer instantiation of polymorphic function ~a." 230 (syntax->datum (get-orig e_fn)))))) 231 232 ;; instantiate polymorphic types 233 ;; inst-type : (Listof Type) (Listof Id) Type -> Type 234 ;; Instantiates ty with the tys-solved substituted for the Xs, where the ith 235 ;; identifier in Xs is associated with the ith type in tys-solved 236 (define (inst-type tys-solved Xs ty) 237 (substs tys-solved Xs ty)) 238 239 ;; inst-type/cs : (Stx-Listof Id) Constraints Type-Stx -> Type-Stx 240 ;; Instantiates ty, substituting each identifier in Xs with its mapping in cs. 241 (define (inst-type/cs Xs cs ty) 242 (define tys-solved (lookup-Xs/keep-unsolved Xs cs)) 243 (inst-type tys-solved Xs ty)) 244 ;; inst-types/cs : (Stx-Listof Id) Constraints (Stx-Listof Type-Stx) -> (Listof Type-Stx) 245 ;; the plural version of inst-type/cs 246 (define (inst-types/cs Xs cs tys) 247 (stx-map (lambda (t) (inst-type/cs Xs cs t)) tys)) 248 249 ;; compute unbound tyvars in one unexpanded type ty 250 (define (compute-tyvar1 ty) 251 (syntax-parse ty 252 [X:id #'(X)] 253 [() #'()] 254 [(C t ...) (stx-appendmap compute-tyvar1 #'(t ...))])) 255 ;; computes unbound ids in (unexpanded) tys, to be used as tyvars 256 (define (compute-tyvars tys) 257 (define Xs (stx-appendmap compute-tyvar1 tys)) 258 (filter 259 (lambda (X) 260 (with-handlers 261 ([exn:fail:syntax:unbound? (lambda (e) #t)] 262 [exn:fail:type:infer? (lambda (e) #t)]) 263 (let ([X+ ((current-type-eval) X)]) 264 (not (or (tyvar? X+) (type? X+)))))) 265 (stx-remove-dups Xs)))) 266 267 ;; define -------------------------------------------------- 268 ;; for function defs, define infers type variables 269 ;; - since the order of the inferred type variables depends on expansion order, 270 ;; which is not known to programmers, to make the result slightly more 271 ;; intuitive, we arbitrarily sort the inferred tyvars lexicographically 272 (define-typed-syntax define/tc #:export-as define 273 [(_ x:id e) ≫ 274 [⊢ e ≫ e- ⇒ τ] 275 #:with y (generate-temporary) 276 -------- 277 [≻ (begin- 278 (define-syntax- x (make-rename-transformer (⊢ y : τ))) 279 (define- y e-))]] 280 ; explicit "forall" 281 [(_ Ys (f:id [x:id (~datum :) τ] ... (~or (~datum ->) (~datum →)) τ_out) 282 e_body ... e) ≫ 283 #:when (brace? #'Ys) 284 ;; TODO; remove this code duplication 285 #:with g (add-orig (generate-temporary #'f) #'f) 286 #:with e_ann (syntax/loc #'e (add-expected e τ_out)) 287 #:with (τ+orig ...) (stx-map (λ (t) (add-orig t t)) #'(τ ... τ_out)) 288 ;; TODO: check that specified return type is correct 289 ;; - currently cannot do it here; to do the check here, need all types of 290 ;; top-lvl fns, since they can call each other 291 #:with (~and ty_fn_expected (~∀ _ (~ext-stlc:→ _ ... out_expected))) 292 ((current-type-eval) #'(∀ Ys (ext-stlc:→ τ+orig ...))) 293 -------- 294 [≻ (begin- 295 (define-syntax- f (make-rename-transformer (⊢ g : ty_fn_expected))) 296 (define- g 297 (Λ Ys (ext-stlc:λ ([x : τ] ...) (ext-stlc:begin e_body ... e_ann)))))]] 298 ;; alternate type sig syntax, after parameter names 299 [(_ (f:id x:id ...) (~datum :) ty ... (~or (~datum ->) (~datum →)) ty_out . b) ≫ 300 -------- 301 [≻ (define/tc (f [x : ty] ... -> ty_out) . b)]] 302 [(_ (f:id [x:id (~datum :) τ] ... ; no TC 303 (~or (~datum ->) (~datum →)) τ_out) 304 e_body ... e) ≫ 305 #:with (~and Ys (Y ...)) (compute-tyvars #'(τ ... τ_out)) 306 #:with g (add-orig (generate-temporary #'f) #'f) 307 #:with e_ann (syntax/loc #'e (add-expected e τ_out)) ; must be macro bc t_out may have unbound tvs 308 #:with (τ+orig ...) (stx-map (λ (t) (add-orig t t)) #'(τ ... τ_out)) 309 ;; TODO: check that specified return type is correct 310 ;; - currently cannot do it here; to do the check here, need all types of 311 ;; top-lvl fns, since they can call each other 312 #:with ty_fn_expected 313 (set-stx-prop/preserved 314 ((current-type-eval) #'(∀ Ys (ext-stlc:→ τ+orig ...))) 315 'orig 316 (list #'(→ τ+orig ...))) 317 -------- 318 [≻ (begin- 319 (define-syntax- f (make-rename-transformer (⊢ g : ty_fn_expected))) 320 (define- g 321 (Λ Ys (ext-stlc:λ ([x : τ] ...) (ext-stlc:begin e_body ... e_ann)))))]] 322 [(_ (f:id [x:id (~datum :) τ] ... 323 (~seq #:where TC ...) 324 (~or (~datum ->) (~datum →)) τ_out) 325 e_body ... e) ≫ 326 #:with (~and Ys (Y ...)) (compute-tyvars #'(τ ... τ_out)) 327 #:with g (add-orig (generate-temporary #'f) #'f) 328 #:with e_ann (syntax/loc #'e (add-expected e τ_out)) ; must be macro bc t_out may have unbound tvs 329 #:with (τ+orig ...) (stx-map (λ (t) (add-orig t t)) #'(τ ... τ_out)) 330 ;; TODO: check that specified return type is correct 331 ;; - currently cannot do it here; to do the check here, need all types of 332 ;; top-lvl fns, since they can call each other 333 #:with (~and ty_fn_expected (~∀ _ (~=> _ ... (~ext-stlc:→ _ ... out_expected)))) 334 (syntax-property 335 ((current-type-eval) #'(∀ Ys (=> TC ... (ext-stlc:→ τ+orig ...)))) 336 'orig 337 (list #'(→ τ+orig ...))) 338 -------- 339 [≻ (begin- 340 (define-syntax- f (make-rename-transformer (⊢ g : ty_fn_expected))) 341 #,(quasisyntax/loc this-syntax 342 (define- g 343 ;(Λ Ys (ext-stlc:λ ([x : τ] ...) (ext-stlc:begin e_body ... e_ann)))))]) 344 (liftedλ {Y ...} ([x : τ] ... #:where TC ...) 345 #,(syntax/loc #'e_ann (ext-stlc:begin e_body ... e_ann))))))]]) 346 347 ;; define-type ----------------------------------------------- 348 ;; TODO: should validate τ as part of define-type definition (before it's used) 349 ;; - not completely possible, since some constructors may not be defined yet, 350 ;; ie, mutually recursive datatypes 351 ;; for now, validate types but punt if encountering unbound ids 352 (define-syntax (define-type stx) 353 (syntax-parse stx 354 [(_ Name:id . rst) 355 #:with NewName (generate-temporary #'Name) 356 #:with Name2 (add-orig #'(NewName) #'Name) 357 #`(begin- 358 (define-type Name2 . #,(subst #'Name2 #'Name #'rst)) 359 (stlc+rec-iso:define-type-alias Name Name2))] 360 [(_ (Name:id X:id ...) 361 ;; constructors must have the form (Cons τ ...) 362 ;; but the first ~or clause accepts 0-arg constructors as ids; 363 ;; the ~and is a workaround to bind the duplicate Cons ids (see Ryan's email) 364 (~and (~or (~and IdCons:id 365 (~parse (Cons [fld (~datum :) τ] ...) #'(IdCons))) 366 (Cons [fld (~datum :) τ] ...) 367 (~and (Cons τ ...) 368 (~parse (fld ...) (generate-temporaries #'(τ ...)))))) ...) 369 ;; validate tys 370 #:with (ty_flat ...) (stx-flatten #'((τ ...) ...)) 371 #:with (_ _ (_ _ (_ _ (_ _ ty+ ...)))) 372 (with-handlers 373 ([exn:fail:syntax:unbound? 374 (λ (e) 375 (define X (stx-car (exn:fail:syntax-exprs e))) 376 #`(lambda () (let-syntax () (let-syntax () (#%app void unbound)))))]) 377 (expand/df 378 #`(lambda (X ...) 379 (let-syntax 380 ([Name 381 (syntax-parser 382 [(_ X ...) (mk-type #'void)] 383 [stx 384 (type-error 385 #:src #'stx 386 #:msg 387 (format "Improper use of constructor ~a; expected ~a args, got ~a" 388 (syntax->datum #'Name) (stx-length #'(X ...)) 389 (stx-length (stx-cdr #'stx))))])] 390 [X (make-rename-transformer (mk-type #'X))] ...) 391 (void ty_flat ...))))) 392 #:when (or (equal? '(unbound) (syntax->datum #'(ty+ ...))) 393 (stx-map 394 (lambda (t+ t) (unless (type? t+) 395 (type-error #:src t 396 #:msg "~a is not a valid type" t))) 397 #'(ty+ ...) #'(ty_flat ...))) 398 #:with NameExpander (format-id #'Name "~~~a" #'Name) 399 #:with NameExtraInfo (format-id #'Name "~a-extra-info" #'Name) 400 #:with (StructName ...) (generate-temporaries #'(Cons ...)) 401 #:with ((e_arg ...) ...) (stx-map generate-temporaries #'((τ ...) ...)) 402 #:with ((e_arg- ...) ...) (stx-map generate-temporaries #'((τ ...) ...)) 403 #:with ((τ_arg ...) ...) (stx-map generate-temporaries #'((τ ...) ...)) 404 #:with ((exposed-acc ...) ...) 405 (stx-map 406 (λ (C fs) (stx-map (λ (f) (format-id C "~a-~a" C f)) fs)) 407 #'(Cons ...) #'((fld ...) ...)) 408 #:with ((acc ...) ...) (stx-map (λ (S fs) (stx-map (λ (f) (format-id S "~a-~a" S f)) fs)) 409 #'(StructName ...) #'((fld ...) ...)) 410 #:with (Cons? ...) (stx-map mk-? #'(StructName ...)) 411 #:with (exposed-Cons? ...) (stx-map mk-? #'(Cons ...)) 412 #`(begin- 413 (define-syntax- (NameExtraInfo stx) 414 (syntax-parse stx 415 [(_ X ...) #'(('Cons 'StructName Cons? [acc τ] ...) ...)])) 416 (define-type-constructor Name 417 #:arity = #,(stx-length #'(X ...)) 418 #:extra-info 'NameExtraInfo) 419 (struct- StructName (fld ...) #:reflection-name 'Cons #:transparent) ... 420 (define-syntax- (exposed-acc stx) ; accessor for records 421 (syntax-parse stx 422 [_:id (⊢ acc (∀ (X ...) (ext-stlc:→ (Name X ...) τ)))] 423 [(o . rst) ; handle if used in fn position 424 #:with app (datum->syntax #'o '#%app) 425 #`(app 426 #,(assign-type #'acc #'(∀ (X ...) (ext-stlc:→ (Name X ...) τ))) 427 . rst)])) ... ... 428 (define-syntax- (exposed-Cons? stx) ; predicates for each variant 429 (syntax-parse stx 430 [_:id (⊢ Cons? (∀ (X ...) (ext-stlc:→ (Name X ...) Bool)))] 431 [(o . rst) ; handle if used in fn position 432 #:with app (datum->syntax #'o '#%app) 433 #`(app 434 #,(assign-type #'Cons? #'(∀ (X ...) (ext-stlc:→ (Name X ...) Bool))) 435 . rst)])) ... 436 (define-typerule Cons 437 ; no args and not polymorphic 438 [C:id ≫ 439 #:when (and (stx-null? #'(X ...)) (stx-null? #'(τ ...))) 440 -------- 441 [≻ (C)]] 442 ; no args but polymorphic, check inferred type 443 [C:id ⇐ : (NameExpander τ-expected-arg (... ...)) ≫ 444 #:when (stx-null? #'(τ ...)) 445 -------- 446 [⊢ (StructName)]] 447 [_:id ≫ 448 #:when (not (stx-null? #'(τ ...))) 449 -------- 450 [⊢ StructName ⇒ (∀ (X ...) (ext-stlc:→ τ ... (Name X ...)))]] ; HO fn 451 [(C τs e_arg ...) ≫ 452 #:when (brace? #'τs) ; commit to this clause 453 #:with {~! τ_X:type (... ...)} #'τs 454 #:with (τ_in:type (... ...)) ; instantiated types 455 (stx-map 456 (λ (t) (substs #'(τ_X.norm (... ...)) #'(X ...) t)) 457 #'(τ ...)) 458 ;; e_arg* is only used to get the ellipses to align 459 #:with (τ_arg ...) #'(τ_in.norm (... ...)) 460 ; #:with (e_arg* (... ...)) #'(e_arg ...) 461 [⊢ e_arg ≫ e_arg- ⇐ τ_arg] ... 462 ; #:with (e_arg- ...) #'(e_arg*- (... ...)) 463 -------- 464 [⊢ (StructName e_arg- ...) ⇒ (Name τ_X.norm (... ...))]] 465 [(C . args) ≫ ; no type annotations, must infer instantiation 466 #:with StructName/ty 467 (set-stx-prop/preserved 468 (⊢ StructName : (∀ (X ...) (ext-stlc:→ τ ... (Name X ...)))) 469 'orig 470 (list #'C)) 471 -------- 472 [≻ (mlish:#%app StructName/ty . args)]]) 473 ...)])) 474 475 ;; match -------------------------------------------------- 476 (begin-for-syntax 477 (define (get-ctx pat ty) 478 (unify-pat+ty (list pat ty))) 479 (define (unify-pat+ty pat+ty) 480 (syntax-parse pat+ty 481 [(pat ty) #:when (brace? #'pat) ; handle root pattern specially (to avoid some parens) 482 (syntax-parse #'pat 483 [{(~datum _)} #'()] 484 [{(~literal stlc+cons:nil)} #'()] 485 [{A:id} ; disambiguate 0-arity constructors (that don't need parens) 486 #:when (get-extra-info #'ty) 487 #'()] 488 ;; comma tup syntax always has parens 489 [{(~and ps (p1 (unq p) ...))} 490 #:when (not (stx-null? #'(p ...))) 491 #:when (andmap (lambda (u) (equal? u 'unquote)) (syntax->datum #'(unq ...))) 492 (unify-pat+ty #'(ps ty))] 493 [{p ...} 494 (unify-pat+ty #'((p ...) ty))])] ; pair 495 [((~datum _) ty) #'()] 496 [((~or (~literal stlc+cons:nil)) ty) #'()] 497 [(A:id ty) ; disambiguate 0-arity constructors (that don't need parens) 498 #:with (_ (_ (_ C) . _) ...) (get-extra-info #'ty) 499 #:when (member (syntax->datum #'A) (syntax->datum #'(C ...))) 500 #'()] 501 [(x:id ty) #'((x ty))] 502 [((p1 (unq p) ...) ty) ; comma tup stx 503 #:when (not (stx-null? #'(p ...))) 504 #:when (andmap (lambda (u) (equal? u 'unquote)) (syntax->datum #'(unq ...))) 505 #:with (~× t ...) #'ty 506 #:with (pp ...) #'(p1 p ...) 507 (unifys #'([pp t] ...))] 508 [(((~literal stlc+tup:tup) p ...) ty) ; tup 509 #:with (~× t ...) #'ty 510 (unifys #'([p t] ...))] 511 [(((~literal stlc+cons:list) p ...) ty) ; known length list 512 #:with (~List t) #'ty 513 (unifys #'([p t] ...))] 514 [(((~seq p (~datum ::)) ... rst) ty) ; nicer cons stx 515 #:with (~List t) #'ty 516 (unifys #'([p t] ... [rst ty]))] 517 [(((~literal stlc+cons:cons) p ps) ty) ; arb length list 518 #:with (~List t) #'ty 519 (unifys #'([p t] [ps ty]))] 520 [((Name p ...) ty) 521 #:with (_ (_ Cons) _ _ [_ _ τ] ...) 522 (stx-findf 523 (syntax-parser 524 [(_ 'C . rst) 525 (equal? (syntax->datum #'Name) (syntax->datum #'C))]) 526 (stx-cdr (get-extra-info #'ty))) 527 (unifys #'([p τ] ...))] 528 [p+t #:fail-when #t (format "could not unify ~a" (syntax->datum #'p+t)) 529 #'()])) 530 (define (unifys p+tys) (stx-appendmap unify-pat+ty p+tys)) 531 532 (define (compile-pat p ty) 533 (syntax-parse p 534 [pat #:when (brace? #'pat) ; handle root pattern specially (to avoid some parens) 535 (syntax-parse #'pat 536 [{(~datum _)} #'_] 537 [{(~literal stlc+cons:nil)} (syntax/loc p (list))] 538 [{A:id} ; disambiguate 0-arity constructors (that don't need parens) 539 #:when (get-extra-info ty) 540 (compile-pat #'(A) ty)] 541 ;; comma tup stx always has parens 542 [{(~and ps (p1 (unq p) ...))} 543 #:when (not (stx-null? #'(p ...))) 544 #:when (andmap (lambda (u) (equal? u 'unquote)) (syntax->datum #'(unq ...))) 545 (compile-pat #'ps ty)] 546 [{pat ...} (compile-pat (syntax/loc p (pat ...)) ty)])] 547 [(~datum _) #'_] 548 [(~literal stlc+cons:nil) ; nil 549 #'(list)] 550 [A:id ; disambiguate 0-arity constructors (that don't need parens) 551 #:with (_ (_ (_ C) . _) ...) (get-extra-info ty) 552 #:when (member (syntax->datum #'A) (syntax->datum #'(C ...))) 553 (compile-pat #'(A) ty)] 554 [x:id p] 555 [(p1 (unq p) ...) ; comma tup stx 556 #:when (not (stx-null? #'(p ...))) 557 #:when (andmap (lambda (u) (equal? u 'unquote)) (syntax->datum #'(unq ...))) 558 #:with (~× t ...) ty 559 #:with (p- ...) (stx-map (lambda (p t) (compile-pat p t)) #'(p1 p ...) #'(t ...)) 560 #'(list p- ...)] 561 [((~literal stlc+tup:tup) . pats) 562 #:with (~× . tys) ty 563 #:with (p- ...) (stx-map (lambda (p t) (compile-pat p t)) #'pats #'tys) 564 (syntax/loc p (list p- ...))] 565 [((~literal stlc+cons:list) . ps) 566 #:with (~List t) ty 567 #:with (p- ...) (stx-map (lambda (p) (compile-pat p #'t)) #'ps) 568 (syntax/loc p (list p- ...))] 569 [((~seq pat (~datum ::)) ... last) ; nicer cons stx 570 #:with (~List t) ty 571 #:with (p- ...) (stx-map (lambda (pp) (compile-pat pp #'t)) #'(pat ...)) 572 #:with last- (compile-pat #'last ty) 573 (syntax/loc p (list-rest p- ... last-))] 574 [((~literal stlc+cons:cons) p ps) 575 #:with (~List t) ty 576 #:with p- (compile-pat #'p #'t) 577 #:with ps- (compile-pat #'ps ty) 578 #'(cons p- ps-)] 579 [(Name . pats) 580 #:with (_ (_ Cons) (_ StructName) _ [_ _ τ] ...) 581 (stx-findf 582 (syntax-parser 583 [(_ 'C . rst) 584 (equal? (syntax->datum #'Name) (syntax->datum #'C))]) 585 (stx-cdr (get-extra-info ty))) 586 #:with (p- ...) (stx-map compile-pat #'pats #'(τ ...)) 587 (syntax/loc p (StructName p- ...))])) 588 589 ;; pats = compiled pats = racket pats 590 (define (check-exhaust pats ty) 591 (define (else-pat? p) 592 (syntax-parse p [(~literal _) #t] [_ #f])) 593 (define (nil-pat? p) 594 (syntax-parse p 595 [((~literal list)) #t] 596 [_ #f])) 597 (define (non-nil-pat? p) 598 (syntax-parse p 599 [((~literal list-rest) . rst) #t] 600 [((~literal cons) . rst) #t] 601 [_ #f])) 602 (define (tup-pat? p) 603 (syntax-parse p 604 [((~literal list) . _) #t] [_ #f])) 605 (cond 606 [(or (stx-ormap else-pat? pats) (stx-ormap identifier? pats)) #t] 607 [(List? ty) ; lists 608 (unless (stx-ormap nil-pat? pats) 609 (error 'match2 (let ([last (car (stx-rev pats))]) 610 (format "(~a:~a) missing nil clause for list expression" 611 (syntax-line last) (syntax-column last))))) 612 (unless (stx-ormap non-nil-pat? pats) 613 (error 'match2 (let ([last (car (stx-rev pats))]) 614 (format "(~a:~a) missing clause for non-empty, arbitrary length list" 615 (syntax-line last) (syntax-column last))))) 616 #t] 617 [(×? ty) ; tuples 618 (unless (stx-ormap tup-pat? pats) 619 (error 'match2 (let ([last (car (stx-rev pats))]) 620 (format "(~a:~a) missing pattern for tuple expression" 621 (syntax-line last) (syntax-column last))))) 622 (syntax-parse pats 623 [((_ p ...) ...) 624 (syntax-parse ty 625 [(~× t ...) 626 (apply stx-andmap 627 (lambda (t . ps) (check-exhaust ps t)) 628 #'(t ...) 629 (syntax->list #'((p ...) ...)))])])] 630 [else ; algebraic datatypes 631 (syntax-parse (get-extra-info ty) 632 [(_ (_ (_ C) (_ Cstruct) . rst) ...) 633 (syntax-parse pats 634 [((Cpat _ ...) ...) 635 (define Cs (syntax->datum #'(C ...))) 636 (define Cstructs (syntax->datum #'(Cstruct ...))) 637 (define Cpats (syntax->datum #'(Cpat ...))) 638 (unless (set=? Cstructs Cpats) 639 (error 'match2 640 (let ([last (car (stx-rev pats))]) 641 (format "(~a:~a) clauses not exhaustive; missing: ~a" 642 (syntax-line last) (syntax-column last) 643 (string-join 644 (for/list ([C Cs][Cstr Cstructs] #:unless (member Cstr Cpats)) 645 (symbol->string C)) 646 ", "))))) 647 #t])] 648 [_ #t])])) 649 650 ;; TODO: do get-ctx and compile-pat in one pass 651 (define (compile-pats pats ty) 652 (stx-map (lambda (p) (list (get-ctx p ty) (compile-pat p ty))) pats)) 653 ) 654 655 (define-typed-syntax match2 656 [(_ e (~datum with) . clauses) ≫ 657 #:fail-unless (not (null? (syntax->list #'clauses))) "no clauses" 658 [⊢ e ≫ e- ⇒ τ_e] 659 #:with ([(~seq p ...) (~datum ->) e_body] ...) #'clauses 660 #:with (pat ...) (stx-map ; use brace to indicate root pattern 661 (lambda (ps) (syntax-parse ps [(pp ...) (syntax/loc this-syntax {pp ...})])) 662 #'((p ...) ...)) 663 #:with ([(~and ctx ([x ty] ...)) pat-] ...) (compile-pats #'(pat ...) #'τ_e) 664 #:with ty-expected (get-expected-type this-syntax) 665 [[x ≫ x- : ty] ... ⊢ [(add-expected e_body ty-expected) ≫ e_body- ⇒ ty_body]] ... 666 #:when (check-exhaust #'(pat- ...) #'τ_e) 667 ---- 668 [⊢ (match- e- [pat- (let- ([x- x] ...) e_body-)] ...) ⇒ (⊔ ty_body ...)]]) 669 670 (define-typed-syntax match #:datum-literals (with) 671 [(_ e with . clauses) ≫ 672 #:fail-when (null? (syntax->list #'clauses)) "no clauses" 673 [⊢ e ≫ e- ⇒ τ_e] 674 #:with t_expect (syntax-property this-syntax 'expected-type) ; propagate inferred type 675 #:with out 676 (cond 677 [(×? #'τ_e) ;; e is tuple 678 (syntax-parse/typecheck #'clauses 679 [([x ... (~datum ->) e_body]) ≫ 680 #:with (~× ty ...) #'τ_e 681 #:fail-unless (stx-length=? #'(ty ...) #'(x ...)) 682 "match clause pattern not compatible with given tuple" 683 [[x ≫ x- : ty] ... ⊢ (add-expected e_body t_expect) ≫ e_body- ⇒ ty_body] 684 #:with (acc ...) (for/list ([(a i) (in-indexed (syntax->list #'(x ...)))]) 685 #`(lambda (s) (list-ref s #,(datum->syntax #'here i)))) 686 #:with z (generate-temporary) 687 -------- 688 [⊢ (let- ([z e-]) 689 (let- ([x- (acc z)] ...) e_body-)) 690 ⇒ ty_body]])] 691 [(List? #'τ_e) ;; e is List 692 (syntax-parse/typecheck #'clauses 693 [([(~or (~and (~and xs [x ...]) (~parse rst (generate-temporary))) 694 (~and (~seq (~seq x (~datum ::)) ... rst:id) (~parse xs #'()))) 695 (~datum ->) e_body] ...+) ≫ 696 #:fail-unless (stx-ormap 697 (lambda (xx) (and (brack? xx) (zero? (stx-length xx)))) 698 #'(xs ...)) 699 "match: missing empty list case" 700 #:fail-when (and (stx-andmap brack? #'(xs ...)) 701 (= 1 (stx-length #'(xs ...)))) 702 "match: missing non-empty list case" 703 #:with (~List ty) #'τ_e 704 [[x ≫ x- : ty] ... [rst ≫ rst- : (List ty)] 705 ⊢ (add-expected e_body t_expect) ≫ e_body- ⇒ ty_body] ... 706 #:with (len ...) (stx-map (lambda (p) #`#,(stx-length p)) #'((x ...) ...)) 707 #:with (lenop ...) (stx-map (lambda (p) (if (brack? p) #'=- #'>=-)) #'(xs ...)) 708 #:with (pred? ...) (stx-map 709 (lambda (l lo) #`(λ- (lst) (#,lo (length- lst) #,l))) 710 #'(len ...) #'(lenop ...)) 711 #:with ((acc1 ...) ...) (stx-map 712 (lambda (xs) 713 (for/list ([(x i) (in-indexed (syntax->list xs))]) 714 #`(lambda (lst) (list-ref lst #,(datum->syntax #'here i))))) 715 #'((x ...) ...)) 716 #:with (acc2 ...) (stx-map (lambda (l) #`(lambda (lst) (list-tail lst #,l))) #'(len ...)) 717 -------- 718 [⊢ (let- ([z e-]) 719 (cond- 720 [(pred? z) 721 (let- ([x- (acc1 z)] ... [rst- (acc2 z)]) e_body-)] ...)) 722 ⇒ (⊔ ty_body ...)]])] 723 [else ;; e is variant 724 (syntax-parse/typecheck #'clauses 725 [([Clause:id x:id ... 726 (~optional (~seq #:when e_guard) #:defaults ([e_guard #'(ext-stlc:#%datum . #t)])) 727 (~datum ->) e_c_un] ...+) ≫ ; un = unannotated with expected ty 728 ;; length #'clauses may be > length #'info, due to guards 729 #:with info-body (get-extra-info #'τ_e) 730 #:with (_ (_ (_ ConsAll) . _) ...) #'info-body 731 #:fail-unless (set=? (syntax->datum #'(Clause ...)) 732 (syntax->datum #'(ConsAll ...))) 733 (type-error #:src this-syntax 734 #:msg (string-append 735 "match: clauses not exhaustive; missing: " 736 (string-join 737 (map symbol->string 738 (set-subtract 739 (syntax->datum #'(ConsAll ...)) 740 (syntax->datum #'(Clause ...)))) 741 ", "))) 742 #:with ((_ _ _ Cons? [_ acc τ] ...) ...) 743 (map ; ok to compare symbols since clause names can't be rebound 744 (lambda (Cl) 745 (stx-findf 746 (syntax-parser 747 [(_ 'C . rst) (equal? Cl (syntax->datum #'C))]) 748 (stx-cdr #'info-body))) ; drop leading #%app 749 (syntax->datum #'(Clause ...))) 750 ;; this commented block experiments with expanding to unsafe ops 751 ;; #:with ((acc ...) ...) (stx-map 752 ;; (lambda (accs) 753 ;; (for/list ([(a i) (in-indexed (syntax->list accs))]) 754 ;; #`(lambda (s) (unsafe-struct*-ref s #,(datum->syntax #'here i))))) 755 ;; #'((acc-fn ...) ...)) 756 #:with (e_c ...+) (stx-map (lambda (ec) (add-expected-ty ec #'t_expect)) #'(e_c_un ...)) 757 [[x ≫ x- : τ] ... ⊢ [e_guard ≫ e_guard- ⇐ Bool] 758 [e_c ≫ e_c- ⇒ τ_ec]] ... 759 #:with z (generate-temporary) ; dont duplicate eval of test expr 760 -------- 761 [⊢ (let- ([z e-]) 762 (cond- 763 [(and- (Cons? z) 764 (let- ([x- (acc z)] ...) e_guard-)) 765 (let- ([x- (acc z)] ...) e_c-)] ...)) 766 ⇒ (⊔ τ_ec ...)]])]) 767 -------- 768 [≻ out]]) 769 770 (define-syntax → ; wrapping → 771 (syntax-parser 772 [(_ ty ... #:TC TC ...) 773 #'(∀ () (=> TC ... (ext-stlc:→ ty ...)))] 774 [(_ Xs . rst) 775 #:when (brace? #'Xs) 776 #:with (X ...) #'Xs 777 (syntax-property 778 #'(∀ (X ...) (ext-stlc:→ . rst)) 779 'orig (list #'(→ . rst)))] 780 [(_ . rst) (set-stx-prop/preserved #'(∀ () (ext-stlc:→ . rst)) 'orig (list #'(→ . rst)))])) 781 ; special arrow that computes free vars; for use with tests 782 ; (because we can't write explicit forall 783 (define-syntax →/test 784 (syntax-parser 785 [(_ (~and Xs (X:id ...)) . rst) 786 #:when (brace? #'Xs) 787 #'(∀ (X ...) (ext-stlc:→ . rst))] 788 [(_ . rst) 789 #:with Xs (compute-tyvars #'rst) 790 #'(∀ Xs (ext-stlc:→ . rst))])) 791 792 (define-syntax =>/test 793 (syntax-parser 794 [(_ . (~and rst (TC ... (_arr . tys_arr)))) 795 #:with Xs (compute-tyvars #'rst) 796 #'(∀ Xs (=> TC ... (ext-stlc:→ . tys_arr)))])) 797 798 ; redefine these to use lifted → 799 (provide (typed-out [+ : (→ Int Int Int)] 800 [- : (→ Int Int Int)] 801 [* : (→ Int Int Int)] 802 [max : (→ Int Int Int)] 803 [min : (→ Int Int Int)] 804 [void : (→ Unit)] 805 [= : (→ Int Int Bool)] 806 [<= : (→ Int Int Bool)] 807 [>= : (→ Int Int Bool)] 808 [< : (→ Int Int Bool)] 809 [> : (→ Int Int Bool)] 810 [modulo : (→ Int Int Int)] 811 [zero? : (→ Int Bool)] 812 [sub1 : (→ Int Int)] 813 [add1 : (→ Int Int)] 814 [not : (→ Bool Bool)] 815 [abs : (→ Int Int)] 816 [even? : (→ Int Bool)] 817 [odd? : (→ Int Bool)])) 818 819 ;; λ -------------------------------------------------------------------------- 820 821 ; all λs have type (∀ (X ...) (→ τ_in ... τ_out)), even monomorphic fns 822 (define-typed-syntax liftedλ #:export-as λ 823 [(_ ([x:id (~datum :) ty] ... #:where TC ...) body) ≫ 824 #:with (X ...) (compute-tyvars #'(ty ...)) 825 -------- 826 [≻ (liftedλ {X ...} ([x : ty] ... #:where TC ...) body)]] 827 ;; TODO: I dont think this works for nested lambdas 828 ;; ie, this will will re-infer tyvars X that should be bound by outer lam 829 ;; - tyvars need to be bound in 2nd expand/df 830 ;; - This is fixed in master by Alex 831 [(_ (~and Xs (X ...)) ([x:id (~datum :) ty] ... #:where TC ...) body) ≫ 832 #:when (brace? #'Xs) 833 #:with (_ Xs+ 834 (_ () (_ () (_ () (_ () ; 2 let-stx = 4 let-values 835 (_ (_ _ TC+ ...) 836 (_ _ ty+ ...) 837 (_ op-tmps+ 838 (_ () (_ () 839 ((~literal #%expression) 840 (_ xs+ 841 (_ () (_ () body+))))))))))))) 842 (expand/df 843 #'(lambda (X ...) 844 (let-syntax 845 ([X (make-rename-transformer (mk-type #'X))] ...) 846 (let-syntax 847 ;; must have this inner macro bc body of lambda may require 848 ;; ops defined by TC to be bound 849 ([a (syntax-parser [(_) 850 (syntax-parse (expand/df #'(void TC ...)) ; must expand in ctx of Xs 851 [(_ _ . 852 (~and (TC+ (... ...)) 853 (~TCs ([op-sym ty-op] (... ...)) (... ...)))) 854 ;; here, * suffix = flattened list 855 ;; op* ... = op-sym ... with proper ctx, and then flattened 856 #:with (op* (... ...)) 857 (stx-appendmap 858 (lambda (os tc) 859 (stx-map (lambda (o) (format-id tc "~a" o)) os)) 860 #'((op-sym (... ...)) (... ...)) #'(TC ...)) 861 #:with (op-tmp* (... ...)) (generate-temporaries #'(op* (... ...))) 862 #:with (ty-op* (... ...)) (stx-flatten #'((ty-op (... ...)) (... ...))) 863 #:with ty-in-tagsss 864 (stx-map 865 (syntax-parser 866 [(~∀ _ fa-body) 867 (get-type-tags 868 (syntax-parse #'fa-body 869 [(~ext-stlc:→ in (... ...) _) #'(in (... ...))] 870 [(~=> _ (... ...) (~ext-stlc:→ in (... ...) _)) #'(in (... ...))]))]) 871 #'(ty-op* (... ...))) 872 #:with (mangled-op (... ...)) (stx-map mangle #'(op* (... ...)) #'ty-in-tagsss) 873 #:with (y (... ...)) #'(x ...) 874 #:with (_ _ ty+ (... ...)) (expand/df #'(void ty ...)) 875 #:with res 876 (expand/df 877 #'(lambda (op-tmp* (... ...)) 878 (let-syntax 879 ([mangled-op 880 (make-rename-transformer (assign-type #'op-tmp* #'ty-op*))] (... ...)) 881 (lambda (y (... ...)) 882 (let-syntax 883 ([y (make-rename-transformer (assign-type #'y #'ty+))] (... ...)) 884 body))))) 885 #'((void TC+ (... ...)) (void ty+ (... ...)) res)])])]) 886 (a))))) 887 #:with ty-out (typeof #'body+) 888 #:with ty-out-expected (get-expected-type #'body+) 889 #:fail-unless (or (not (syntax-e #'ty-out-expected)) 890 (typecheck? #'ty-out #'ty-out-expected)) 891 (type-error #:src #'body 892 #:msg "Body has type ~a, expected/given: ~a" 893 #'ty-out #'ty-out-expected) 894 -------- 895 [⊢ (λ- op-tmps+ (λ- xs+ body+)) 896 ⇒ (∀ Xs+ (=> TC+ ... (ext-stlc:→ ty+ ... ty-out)))]] 897 [(_ ([x:id (~datum :) ty] ...) body) ≫ ; no TC 898 #:with (X ...) (compute-tyvars #'(ty ...)) 899 #:with (~∀ () (~ext-stlc:→ _ ... body-ty)) (get-expected-type this-syntax) 900 -------- 901 [≻ (Λ (X ...) (ext-stlc:λ ([x : ty] ...) (add-expected body body-ty)))]] 902 [(_ ([x:id (~datum :) ty] ...) body) ≫ ; no TC, ignoring expected-type 903 #:with (X ...) (compute-tyvars #'(ty ...)) 904 -------- 905 [≻ (Λ (X ...) (ext-stlc:λ ([x : ty] ...) body))]] 906 [(_ (x:id ...+) body) ≫ 907 #:with (~?∀ Xs expected) (get-expected-type this-syntax) 908 #:do [(unless (→? #'expected) 909 (type-error #:src this-syntax #:msg "λ parameters must have type annotations"))] 910 #:with (~ext-stlc:→ arg-ty ... body-ty) #'expected 911 #:do [(unless (stx-length=? #'[x ...] #'[arg-ty ...]) 912 (type-error #:src this-syntax #:msg 913 (format "expected a function of ~a arguments, got one with ~a arguments" 914 (stx-length #'[arg-ty ...] #'[x ...]))))] 915 -------- 916 [≻ (Λ Xs (ext-stlc:λ ([x : arg-ty] ...) #,(add-expected-ty #'body #'body-ty)))]] 917 #;[(_ args body) 918 #:with (~∀ () (~ext-stlc:→ arg-ty ... body-ty)) (get-expected-type stx) 919 #`(Λ () (ext-stlc:λ args #,(add-expected-ty #'body #'body-ty)))] 920 #;[(_ (~and x+tys ([_ (~datum :) ty] ...)) . body) 921 #:with Xs (compute-tyvars #'(ty ...)) 922 ;; TODO is there a way to have λs that refer to ids defined after them? 923 #'(Λ Xs (ext-stlc:λ x+tys . body))]) 924 925 ;; #%app -------------------------------------------------- 926 (define-typed-syntax mlish:#%app #:export-as #%app 927 [(~and this-app (_ e_fn . e_args)) ≫ 928 ; #:when (printf "app: ~a\n" (syntax->datum #'(e_fn . e_args))) 929 ;; ) compute fn type (ie ∀ and →) 930 [⊢ e_fn ≫ e_fn- ⇒ (~and ty_fn (~∀ Xs ty_fnX))] 931 -------- 932 [≻ 933 #,(cond 934 [(stx-null? #'Xs) 935 (define/with-syntax tyX_args 936 (syntax-parse #'ty_fnX 937 [(~ext-stlc:→ . tyX_args) #'tyX_args])) 938 (syntax-parse #'(e_args tyX_args) 939 [((e_arg ...) (τ_inX ... _)) 940 #:fail-unless (stx-length=? #'(e_arg ...) #'(τ_inX ...)) 941 (mk-app-err-msg #'this-app #:expected #'(τ_inX ...) 942 #:note "Wrong number of arguments.") 943 #:with e_fn/ty (⊢ e_fn- : (ext-stlc:→ . tyX_args)) 944 #'(ext-stlc:#%app e_fn/ty (add-expected e_arg τ_inX) ...)])] 945 [else 946 (syntax-parse #'ty_fnX 947 ;; TODO: combine these two clauses 948 ;; no typeclasses, duplicate code for now -------------------------------- 949 [(~ext-stlc:→ . tyX_args) 950 ;; ) solve for type variables Xs 951 (define/with-syntax ((e_arg1- ...) (unsolved-X ...) cs) (solve #'Xs #'tyX_args #'this-app)) 952 ;; ) instantiate polymorphic function type 953 (syntax-parse (inst-types/cs #'Xs #'cs #'tyX_args) 954 [(τ_in ... τ_out) ; concrete types 955 ;; ) arity check 956 #:fail-unless (stx-length=? #'(τ_in ...) #'e_args) 957 (mk-app-err-msg #'this-app #:expected #'(τ_in ...) 958 #:note "Wrong number of arguments.") 959 ;; ) compute argument types; re-use args expanded during solve 960 #:with ([e_arg2- τ_arg2] ...) (let ([n (stx-length #'(e_arg1- ...))]) 961 (infers+erase 962 (stx-map add-expected-ty 963 (stx-drop #'e_args n) (stx-drop #'(τ_in ...) n)))) 964 #:with (τ_arg1 ...) (stx-map typeof #'(e_arg1- ...)) 965 #:with (τ_arg ...) #'(τ_arg1 ... τ_arg2 ...) 966 #:with (e_arg- ...) #'(e_arg1- ... e_arg2- ...) 967 ;; ) typecheck args 968 #:fail-unless (typechecks? #'(τ_arg ...) #'(τ_in ...)) 969 (mk-app-err-msg #'this-app 970 #:given #'(τ_arg ...) 971 #:expected 972 (stx-map 973 (lambda (tyin) 974 (define old-orig (get-orig tyin)) 975 (define new-orig 976 (and old-orig 977 (substs 978 (stx-map get-orig (lookup-Xs/keep-unsolved #'Xs #'cs)) #'Xs old-orig 979 (lambda (x y) 980 (equal? (syntax->datum x) (syntax->datum y)))))) 981 (syntax-property tyin 'orig (list new-orig))) 982 #'(τ_in ...))) 983 #:with τ_out* (if (stx-null? #'(unsolved-X ...)) 984 #'τ_out 985 (syntax-parse #'τ_out 986 [(~?∀ (Y ...) τ_out) 987 (unless (→? #'τ_out) 988 (raise-app-poly-infer-error #'this-app #'(τ_in ...) #'(τ_arg ...) #'e_fn)) 989 #'(∀ (unsolved-X ... Y ...) τ_out)])) 990 (⊢ (#%app- e_fn- e_arg- ...) : τ_out*)])] 991 ;; handle type class constraints ---------------------------------------- 992 [(~=> TCX ... (~ext-stlc:→ . tyX_args)) 993 ;; ) solve for type variables Xs 994 (define/with-syntax ((e_arg1- ...) (unsolved-X ...) cs) (solve #'Xs #'tyX_args #'this-app)) 995 ;; ) instantiate polymorphic function type 996 (syntax-parse (inst-types/cs #'Xs #'cs #'((TCX ...) tyX_args)) 997 [((TC ...) (τ_in ... τ_out)) ; concrete types 998 #:with (~TCs ([generic-op ty-concrete-op] ...) ...) #'(TC ...) 999 #:with (op ...) 1000 (stx-appendmap 1001 (lambda (gen-ops conc-op-tys TC) 1002 (map 1003 (lambda (o tys) 1004 (with-handlers 1005 ([exn:fail:syntax:unbound? 1006 (lambda (e) 1007 (type-error #:src #'this-app 1008 #:msg 1009 (format 1010 (string-append 1011 "~a instance undefined. " 1012 "Cannot instantiate function with constraints " 1013 "~a with:\n ~a") 1014 (type->str 1015 (let* 1016 ([old-orig (get-orig TC)] 1017 [new-orig 1018 (and 1019 old-orig 1020 (substs (stx-map get-orig (lookup-Xs/keep-unsolved #'Xs #'cs)) #'Xs old-orig 1021 (lambda (x y) 1022 (equal? (syntax->datum x) 1023 (syntax->datum y)))))]) 1024 (syntax-property TC 'orig (list new-orig)))) 1025 (types->str #'(TCX ...)) 1026 (string-join 1027 (stx-map 1028 (lambda (X ty-solved) 1029 (string-append (type->str X) " : " (type->str ty-solved))) 1030 #'Xs (lookup-Xs/keep-unsolved #'Xs #'cs)) ", "))))] 1031 [(lambda _ #t) 1032 (lambda (e) (displayln "other exn")(displayln e) 1033 (error 'lookup))]) 1034 (lookup-op o tys))) 1035 (stx-map (lambda (o) (format-id #'this-app "~a" o #:source #'this-app)) gen-ops) 1036 (stx-map 1037 (syntax-parser 1038 [(~∀ _ (~ext-stlc:→ ty_in ... _)) #'(ty_in ...)]) 1039 conc-op-tys))) 1040 #'((generic-op ...) ...) #'((ty-concrete-op ...) ...) #'(TC ...)) 1041 ;; ) arity check 1042 #:fail-unless (stx-length=? #'(τ_in ...) #'e_args) 1043 (mk-app-err-msg #'this-app #:expected #'(τ_in ...) 1044 #:note "Wrong number of arguments.") 1045 ;; ) compute argument types; re-use args expanded during solve 1046 #:with ([e_arg2- τ_arg2] ...) (let ([n (stx-length #'(e_arg1- ...))]) 1047 (infers+erase 1048 (stx-map add-expected-ty 1049 (stx-drop #'e_args n) (stx-drop #'(τ_in ...) n)))) 1050 #:with (τ_arg1 ...) (stx-map typeof #'(e_arg1- ...)) 1051 #:with (τ_arg ...) #'(τ_arg1 ... τ_arg2 ...) 1052 #:with (e_arg- ...) #'(e_arg1- ... e_arg2- ...) 1053 ;; ) typecheck args 1054 #:fail-unless (typechecks? #'(τ_arg ...) #'(τ_in ...)) 1055 (mk-app-err-msg #'this-app 1056 #:given #'(τ_arg ...) 1057 #:expected 1058 (stx-map 1059 (lambda (tyin) 1060 (define old-orig (get-orig tyin)) 1061 (define new-orig 1062 (and old-orig 1063 (substs 1064 (stx-map get-orig (lookup-Xs/keep-unsolved #'Xs #'cs)) #'Xs old-orig 1065 (lambda (x y) 1066 (equal? (syntax->datum x) (syntax->datum y)))))) 1067 (syntax-property tyin 'orig (list new-orig))) 1068 #'(τ_in ...))) 1069 #:with τ_out* (if (stx-null? #'(unsolved-X ...)) 1070 #'τ_out 1071 (syntax-parse #'τ_out 1072 [(~?∀ (Y ...) τ_out) 1073 (unless (→? #'τ_out) 1074 (raise-app-poly-infer-error #'this-app #'(τ_in ...) #'(τ_arg ...) #'e_fn)) 1075 #'(∀ (unsolved-X ... Y ...) τ_out)])) 1076 (⊢ ((#%app- e_fn- op ...) e_arg- ...) : τ_out*)])])])]] 1077 [(_ e_fn . e_args) ≫ ; err case; e_fn is not a function 1078 [⊢ e_fn ≫ e_fn- ⇒ τ_fn] 1079 -------- 1080 [#:error 1081 (type-error #:src #'this-app 1082 #:msg (format "Expected expression ~a to have → type, got: ~a" 1083 (syntax->datum #'e_fn) (type->str #'τ_fn)))]]) 1084 1085 1086 ;; cond and other conditionals 1087 (define-typed-syntax cond 1088 [(_ [(~or (~and (~datum else) (~parse test #'(ext-stlc:#%datum . #t))) 1089 test) 1090 b ... body] ...+) ⇐ τ_expected ≫ 1091 [⊢ test ≫ test- ⇐ Bool] ... 1092 [⊢ (begin b ... body) ≫ body- ⇐ τ_expected] ... 1093 -------- 1094 [⊢ (cond- [test- body-] ...)]] 1095 [(cond [(~or (~and (~datum else) (~parse test #'(ext-stlc:#%datum . #t))) 1096 test) 1097 b ... body] ...+) ≫ 1098 [⊢ test ≫ test- ⇐ Bool] ... 1099 [⊢ (begin b ... body) ≫ body- ⇒ τ_body] ... 1100 -------- 1101 [⊢ (cond- [test- body-] ...) ⇒ (⊔ τ_body ...)]]) 1102 (define-typed-syntax when 1103 [(_ test body ...) ≫ 1104 [⊢ test ≫ test- ⇒ _] ; non-false true 1105 [⊢ body ≫ body- ⇒ _] ... 1106 -------- 1107 [⊢ (when- test- body- ... (void-)) ⇒ Unit]]) 1108 (define-typed-syntax unless 1109 [(_ test body ...) ≫ 1110 [⊢ test ≫ test- ⇒ _] 1111 [⊢ body ≫ body- ⇒ _] ... 1112 -------- 1113 [⊢ (unless- test- body- ... (void-)) ⇒ Unit]]) 1114 1115 ;; sync channels and threads 1116 (define-type-constructor Channel) 1117 1118 (define-typed-syntax make-channel 1119 [(_ (~and tys {ty})) ≫ 1120 #:when (brace? #'tys) 1121 -------- 1122 [⊢ (make-channel-) ⇒ (Channel ty)]]) 1123 (define-typed-syntax channel-get 1124 [(_ c) ⇐ ty ≫ 1125 [⊢ c ≫ c- ⇐ (Channel ty)] 1126 -------- 1127 [⊢ (channel-get- c-)]] 1128 [(_ c) ≫ 1129 [⊢ c ≫ c- ⇒ (~Channel ty)] 1130 -------- 1131 [⊢ (channel-get- c-) ⇒ ty]]) 1132 (define-typed-syntax channel-put 1133 [(_ c v) ≫ 1134 [⊢ c ≫ c- ⇒ (~Channel ty)] 1135 [⊢ v ≫ v- ⇐ ty] 1136 -------- 1137 [⊢ (channel-put- c- v-) ⇒ Unit]]) 1138 1139 (define-base-type Thread) 1140 1141 ;; threads 1142 (define-typed-syntax (thread th) ≫ 1143 [⊢ th ≫ th- ⇒ (~∀ () (~ext-stlc:→ τ_out))] 1144 -------- 1145 [⊢ (thread- th-) ⇒ Thread]) 1146 1147 (provide (typed-out [random : (→ Int Int)] 1148 [integer->char : (→ Int Char)] 1149 [string->list : (→ String (List Char))] 1150 [string->number : (→ String Int)])) 1151 (define-typed-syntax number->string 1152 [_:id ≫ 1153 -------- 1154 [⊢ number->string- ⇒ (→ Int String)]] 1155 [(_ n) ≫ 1156 -------- 1157 [≻ (number->string n (ext-stlc:#%datum . 10))]] 1158 [(_ n rad) ≫ 1159 [⊢ n ≫ n- ⇐ Int] 1160 [⊢ rad ≫ rad- ⇐ Int] 1161 -------- 1162 [⊢ (number->string- n rad) ⇒ String]]) 1163 1164 (provide (typed-out [string : (→ Char String)] 1165 [sleep : (→ Int Unit)] 1166 [string=? : (→ String String Bool)] 1167 [string<? : (→ String String Bool)] 1168 [string<=? : (→ String String Bool)] 1169 [string>? : (→ String String Bool)] 1170 [string>=? : (→ String String Bool)] 1171 [char=? : (→ Char Char Bool)] 1172 [char<? : (→ Char Char Bool)] 1173 [char<=? : (→ Char Char Bool)] 1174 [char>? : (→ Char Char Bool)] 1175 [char>=? : (→ Char Char Bool)])) 1176 1177 (define-typed-syntax string-append 1178 [(_ str ...) ≫ 1179 [⊢ str ≫ str- ⇐ String] ... 1180 -------- 1181 [⊢ (string-append- str- ...) ⇒ String]]) 1182 1183 ;; vectors 1184 (define-type-constructor Vector) 1185 1186 (define-typed-syntax vector 1187 [(_ (~and tys {ty})) ≫ 1188 #:when (brace? #'tys) 1189 -------- 1190 [⊢ (vector-) ⇒ (Vector ty)]] 1191 [(_ v ...) ⇐ (Vector ty) ≫ 1192 [⊢ v ≫ v- ⇐ ty] ... 1193 -------- 1194 [⊢ (vector- v- ...)]] 1195 [(_ v ...) ≫ 1196 [⊢ v ≫ v- ⇒ ty] ... 1197 #:when (same-types? #'(ty ...)) 1198 #:with one-ty (stx-car #'(ty ...)) 1199 -------- 1200 [⊢ (vector- v- ...) ⇒ (Vector one-ty)]]) 1201 (define-typed-syntax make-vector 1202 [(_ n) ≫ 1203 -------- 1204 [≻ (make-vector n (ext-stlc:#%datum . 0))]] 1205 [(_ n e) ≫ 1206 [⊢ n ≫ n- ⇐ Int] 1207 [⊢ e ≫ e- ⇒ ty] 1208 -------- 1209 [⊢ (make-vector- n- e-) ⇒ (Vector ty)]]) 1210 (define-typed-syntax (vector-length e) ≫ 1211 [⊢ e ≫ e- ⇒ (~Vector _)] 1212 -------- 1213 [⊢ (vector-length- e-) ⇒ Int]) 1214 (define-typed-syntax vector-ref 1215 [(_ e n) ⇐ ty ≫ 1216 [⊢ e ≫ e- ⇐ (Vector ty)] 1217 [⊢ n ≫ n- ⇐ Int] 1218 -------- 1219 [⊢ (vector-ref- e- n-)]] 1220 [(_ e n) ≫ 1221 [⊢ e ≫ e- ⇒ (~Vector ty)] 1222 [⊢ n ≫ n- ⇐ Int] 1223 -------- 1224 [⊢ (vector-ref- e- n-) ⇒ ty]]) 1225 (define-typed-syntax (vector-set! e n v) ≫ 1226 [⊢ e ≫ e- ⇒ (~Vector ty)] 1227 [⊢ n ≫ n- ⇐ Int] 1228 [⊢ v ≫ v- ⇐ ty] 1229 -------- 1230 [⊢ (vector-set!- e- n- v-) ⇒ Unit]) 1231 (define-typed-syntax (vector-copy! dest start src) ≫ 1232 [⊢ dest ≫ dest- ⇒ (~Vector ty)] 1233 [⊢ start ≫ start- ⇐ Int] 1234 [⊢ src ≫ src- ⇐ (Vector ty)] 1235 -------- 1236 [⊢ (vector-copy!- dest- start- src-) ⇒ Unit]) 1237 1238 ;; sequences and for loops 1239 1240 (define-type-constructor Sequence) 1241 1242 (define-typed-syntax in-range 1243 [(_ end) ≫ 1244 -------- 1245 [≻ (in-range (ext-stlc:#%datum . 0) end (ext-stlc:#%datum . 1))]] 1246 [(_ start end) ≫ 1247 -------- 1248 [≻ (in-range start end (ext-stlc:#%datum . 1))]] 1249 [(_ start end step) ≫ 1250 [⊢ start ≫ start- ⇐ Int] 1251 [⊢ end ≫ end- ⇐ Int] 1252 [⊢ step ≫ step- ⇐ Int] 1253 -------- 1254 [⊢ (in-range- start- end- step-) ⇒ (Sequence Int)]]) 1255 1256 (define-typed-syntax in-naturals 1257 [(_) ≫ 1258 -------- 1259 [≻ (in-naturals (ext-stlc:#%datum . 0))]] 1260 [(_ start) ≫ 1261 [⊢ start ≫ start- ⇐ Int] 1262 -------- 1263 [⊢ (in-naturals- start-) ⇒ (Sequence Int)]]) 1264 1265 1266 (define-typed-syntax (in-vector e) ≫ 1267 [⊢ e ≫ e- ⇒ (~Vector ty)] 1268 -------- 1269 [⊢ (in-vector- e-) ⇒ (Sequence ty)]) 1270 1271 (define-typed-syntax (in-list e) ≫ 1272 [⊢ e ≫ e- ⇒ (~List ty)] 1273 -------- 1274 [⊢ (in-list- e-) ⇒ (Sequence ty)]) 1275 1276 (define-typed-syntax (in-lines e) ≫ 1277 [⊢ e ≫ e- ⇐ String] 1278 -------- 1279 [⊢ (in-lines- (open-input-string- e-)) ⇒ (Sequence String)]) 1280 1281 (define-typed-syntax (for ([x:id e]...) b ...+) ≫ 1282 [⊢ e ≫ e- ⇒ (~Sequence ty)] ... 1283 [[x ≫ x- : ty] ... ⊢ [b ≫ b- ⇒ _] ...] 1284 -------- 1285 [⊢ (for- ([x- e-] ...) b- ...) ⇒ Unit]) 1286 (define-typed-syntax (for* ([x:id e]...) b ...+) ≫ 1287 [⊢ e ≫ e- ⇒ (~Sequence ty)] ... 1288 [[x ≫ x- : ty] ... ⊢ [b ≫ b- ⇒ _] ...] 1289 -------- 1290 [⊢ (for*- ([x- e-] ...) b- ...) ⇒ Unit]) 1291 1292 (define-typed-syntax (for/list ([x:id e]...) body) ≫ 1293 [⊢ e ≫ e- ⇒ (~Sequence ty)] ... 1294 [[x ≫ x- : ty] ... ⊢ [body ≫ body- ⇒ ty_body]] 1295 -------- 1296 [⊢ (for/list- ([x- e-] ...) body-) ⇒ (List ty_body)]) 1297 (define-typed-syntax (for/vector ([x:id e]...) body) ≫ 1298 [⊢ e ≫ e- ⇒ (~Sequence ty)] ... 1299 [[x ≫ x- : ty] ... ⊢ [body ≫ body- ⇒ ty_body]] 1300 -------- 1301 [⊢ (for/vector- ([x- e-] ...) body-) ⇒ (Vector ty_body)]) 1302 (define-typed-syntax (for*/vector ([x:id e]...) body) ≫ 1303 [⊢ e ≫ e- ⇒ (~Sequence ty)] ... 1304 [[x ≫ x- : ty] ... ⊢ [body ≫ body- ⇒ ty_body]] 1305 -------- 1306 [⊢ (for*/vector- ([x- e-] ...) body-) ⇒ (Vector ty_body)]) 1307 (define-typed-syntax (for*/list ([x:id e]...) body) ≫ 1308 [⊢ e ≫ e- ⇒ (~Sequence ty)] ... 1309 [[x ≫ x- : ty] ... ⊢ [body ≫ body- ⇒ ty_body]] 1310 -------- 1311 [⊢ (for*/list- ([x- e-] ...) body-) ⇒ (List ty_body)]) 1312 (define-typed-syntax for/fold 1313 [(_ ([acc init]) ([x:id e] ...) body) ⇐ τ_expected ≫ 1314 [⊢ init ≫ init- ⇐ τ_expected] 1315 [⊢ e ≫ e- ⇒ (~Sequence ty)] ... 1316 [[acc ≫ acc- : τ_expected] [x ≫ x- : ty] ... ⊢ body ≫ body- ⇐ τ_expected] 1317 -------- 1318 [⊢ (for/fold- ([acc- init-]) ([x- e-] ...) body-)]] 1319 [(_ ([acc init]) ([x:id e] ...) body) ≫ 1320 [⊢ init ≫ init- ⇒ : τ_init] 1321 [⊢ e ≫ e- ⇒ (~Sequence ty)] ... 1322 [[acc ≫ acc- : τ_init] [x ≫ x- : ty] ... ⊢ body ≫ body- ⇐ τ_init] 1323 -------- 1324 [⊢ (for/fold- ([acc- init-]) ([x- e-] ...) body-) ⇒ τ_init]]) 1325 1326 (define-typed-syntax (for/hash ([x:id e]...) body) ≫ 1327 [⊢ e ≫ e- ⇒ (~Sequence ty)] ... 1328 [[x ≫ x- : ty] ... ⊢ body ≫ body- ⇒ (~× ty_k ty_v)] 1329 -------- 1330 [⊢ (for/hash- ([x- e-] ...) 1331 (let- ([t body-]) 1332 (values- (car- t) (cadr- t)))) ⇒ (Hash ty_k ty_v)]) 1333 1334 (define-typed-syntax 1335 (for/sum 1336 ([x:id e]... 1337 (~optional (~seq #:when guard) #:defaults ([guard #'#t]))) 1338 body) ≫ 1339 [⊢ e ≫ e- ⇒ (~Sequence ty)] ... 1340 [[x ≫ x- : ty] ... ⊢ [guard ≫ guard- ⇒ _] [body ≫ body- ⇐ Int]] 1341 -------- 1342 [⊢ (for/sum- ([x- e-] ... #:when guard-) body-) ⇒ Int]) 1343 1344 ; printing and displaying 1345 (define-typed-syntax (printf str e ...) ≫ 1346 [⊢ str ≫ s- ⇐ String] 1347 [⊢ e ≫ e- ⇒ ty] ... 1348 -------- 1349 [⊢ (printf- s- e- ...) ⇒ Unit]) 1350 (define-typed-syntax (format str e ...) ≫ 1351 [⊢ str ≫ s- ⇐ String] 1352 [⊢ e ≫ e- ⇒ ty] ... 1353 -------- 1354 [⊢ (format- s- e- ...) ⇒ String]) 1355 (define-typed-syntax (display e) ≫ 1356 [⊢ e ≫ e- ⇒ _] 1357 -------- 1358 [⊢ (display- e-) ⇒ Unit]) 1359 (define-typed-syntax (displayln e) ≫ 1360 [⊢ e ≫ e- ⇒ _] 1361 -------- 1362 [⊢ (displayln- e-) ⇒ Unit]) 1363 (provide (typed-out [newline : (→ Unit)])) 1364 1365 (define-typed-syntax list->vector 1366 [(_ e) ⇐ (~Vector ty) ≫ 1367 [⊢ e ≫ e- ⇐ (List ty)] 1368 -------- 1369 [⊢ (list->vector- e-)]] 1370 [(_ e) ≫ 1371 [⊢ e ≫ e- ⇒ (~List ty)] 1372 -------- 1373 [⊢ (list->vector- e-) ⇒ (Vector ty)]]) 1374 1375 (define-typed-syntax let 1376 [(_ name:id (~datum :) ty:type ~! ([x:id e] ...) b ... body) ≫ 1377 [⊢ e ≫ e- ⇒ ty_e] ... 1378 [[name ≫ name- : (→ ty_e ... ty.norm)] [x ≫ x- : ty_e] ... 1379 ⊢ [b ≫ b- ⇒ _] ... [body ≫ body- ⇐ ty.norm]] 1380 -------- 1381 [⊢ (letrec- ([name- (λ- (x- ...) b- ... body-)]) 1382 (name- e- ...)) 1383 ⇒ ty.norm]] 1384 [(_ ([x:id e] ...) body ...) ≫ 1385 -------- 1386 [≻ (ext-stlc:let ([x e] ...) (begin body ...))]]) 1387 (define-typed-syntax (let* ([x:id e] ...) body ...) ≫ 1388 -------- 1389 [≻ (ext-stlc:let* ([x e] ...) (begin body ...))]) 1390 1391 (define-typed-syntax begin 1392 [(_ body ... b) ⇐ τ_expected ≫ 1393 [⊢ body ≫ body- ⇒ _] ... 1394 [⊢ b ≫ b- ⇐ τ_expected] 1395 -------- 1396 [⊢ (begin- body- ... b-)]] 1397 [(_ body ... b) ≫ 1398 [⊢ body ≫ body- ⇒ _] ... 1399 [⊢ b ≫ b- ⇒ τ] 1400 -------- 1401 [⊢ (begin- body- ... b-) ⇒ τ]]) 1402 1403 ;; hash 1404 (define-type-constructor Hash #:arity = 2) 1405 1406 (define-typed-syntax (in-hash e) ≫ 1407 [⊢ e ≫ e- ⇒ (~Hash ty_k ty_v)] 1408 -------- 1409 [⊢ (hash-map- e- list-) ⇒ (Sequence (stlc+rec-iso:× ty_k ty_v))]) 1410 1411 ; mutable hashes 1412 (define-typed-syntax hash 1413 [(_ (~and tys {ty_key ty_val})) ≫ 1414 #:when (brace? #'tys) 1415 -------- 1416 [⊢ (make-hash-) ⇒ (Hash ty_key ty_val)]] 1417 [(_ (~seq k v) ...) ≫ 1418 [⊢ k ≫ k- ⇒ ty_k] ... 1419 [⊢ v ≫ v- ⇒ ty_v] ... 1420 #:when (same-types? #'(ty_k ...)) 1421 #:when (same-types? #'(ty_v ...)) 1422 #:with ty_key (stx-car #'(ty_k ...)) 1423 #:with ty_val (stx-car #'(ty_v ...)) 1424 -------- 1425 [⊢ (make-hash- (list- (cons- k- v-) ...)) ⇒ (Hash ty_key ty_val)]]) 1426 (define-typed-syntax (hash-set! h k v) ≫ 1427 [⊢ h ≫ h- ⇒ (~Hash ty_k ty_v)] 1428 [⊢ k ≫ k- ⇐ ty_k] 1429 [⊢ v ≫ v- ⇐ ty_v] 1430 -------- 1431 [⊢ (hash-set!- h- k- v-) ⇒ Unit]) 1432 (define-typed-syntax hash-ref 1433 [(_ h k) ≫ 1434 [⊢ h ≫ h- ⇒ (~Hash ty_k ty_v)] 1435 [⊢ k ≫ k- ⇐ ty_k] 1436 -------- 1437 [⊢ (hash-ref- h- k-) ⇒ ty_v]] 1438 [(_ h k fail) ≫ 1439 [⊢ h ≫ h- ⇒ (~Hash ty_k ty_v)] 1440 [⊢ k ≫ k- ⇐ ty_k] 1441 [⊢ fail ≫ fail- ⇐ (→ ty_v)] 1442 -------- 1443 [⊢ (hash-ref- h- k- fail-) ⇒ ty_val]]) 1444 (define-typed-syntax (hash-has-key? h k) ≫ 1445 [⊢ h ≫ h- ⇒ (~Hash ty_k _)] 1446 [⊢ k ≫ k- ⇐ ty_k] 1447 -------- 1448 [⊢ (hash-has-key?- h- k-) ⇒ Bool]) 1449 1450 (define-typed-syntax (hash-count h) ≫ 1451 [⊢ h ≫ h- ⇒ (~Hash _ _)] 1452 -------- 1453 [⊢ (hash-count- h-) ⇒ Int]) 1454 1455 (define-base-type String-Port) 1456 (define-base-type Input-Port) 1457 (provide (typed-out [open-output-string : (→ String-Port)] 1458 [get-output-string : (→ String-Port String)] 1459 [string-upcase : (→ String String)])) 1460 1461 (define-typed-syntax write-string 1462 [(_ str out) ≫ 1463 -------- 1464 [≻ (write-string str out (ext-stlc:#%datum . 0) (string-length str))]] 1465 [(_ str out start end) ≫ 1466 [⊢ str ≫ str- ⇐ String] 1467 [⊢ out ≫ out- ⇐ String-Port] 1468 [⊢ start ≫ start- ⇐ Int] 1469 [⊢ end ≫ end- ⇐ Int] 1470 -------- 1471 [⊢ (begin- (write-string- str- out- start- end-) (void-)) ⇒ Unit]]) 1472 1473 (define-typed-syntax (string-length str) ≫ 1474 [⊢ str ≫ str- ⇐ String] 1475 -------- 1476 [⊢ (string-length- str-) ⇒ Int]) 1477 (provide (typed-out [make-string : (→ Int String)] 1478 [string-set! : (→ String Int Char Unit)] 1479 [string-ref : (→ String Int Char)])) 1480 (define-typed-syntax string-copy! 1481 [(_ dest dest-start src) ≫ 1482 -------- 1483 [≻ (string-copy! 1484 dest dest-start src (ext-stlc:#%datum . 0) (string-length src))]] 1485 [(_ dest dest-start src src-start src-end) ≫ 1486 [⊢ dest ≫ dest- ⇐ String] 1487 [⊢ src ≫ src- ⇐ String] 1488 [⊢ dest-start ≫ dest-start- ⇐ Int] 1489 [⊢ src-start ≫ src-start- ⇐ Int] 1490 [⊢ src-end ≫ src-end- ⇐ Int] 1491 -------- 1492 [⊢ (string-copy!- dest- dest-start- src- src-start- src-end-) ⇒ Unit]]) 1493 1494 (provide (typed-out [fl+ : (→ Float Float Float)] 1495 [fl- : (→ Float Float Float)] 1496 [fl* : (→ Float Float Float)] 1497 [fl/ : (→ Float Float Float)] 1498 [fl= : (→ Float Float Bool)] 1499 [flsqrt : (→ Float Float)] 1500 [flceiling : (→ Float Float)] 1501 [inexact->exact : (→ Float Int)] 1502 [exact->inexact : (→ Int Float)] 1503 [char->integer : (→ Char Int)] 1504 [real->decimal-string : (→ Float Int String)] 1505 [fx->fl : (→ Int Float)])) 1506 (define-typed-syntax (quotient+remainder x y) ≫ 1507 [⊢ x ≫ x- ⇐ Int] 1508 [⊢ y ≫ y- ⇐ Int] 1509 -------- 1510 [⊢ (let-values- ([[a b] (quotient/remainder- x- y-)]) 1511 (list- a b)) 1512 ⇒ (stlc+rec-iso:× Int Int)]) 1513 (provide (typed-out [quotient : (→ Int Int Int)])) 1514 1515 (define-typed-syntax (set! x:id e) ≫ 1516 [⊢ x ≫ x- ⇒ ty_x] 1517 [⊢ e ≫ e- ⇐ ty_x] 1518 -------- 1519 [⊢ (set!- x e-) ⇒ Unit]) 1520 1521 (define-typed-syntax (provide-type ty ...) ≫ 1522 -------- 1523 [≻ (provide- ty ...)]) 1524 1525 (define-typed-syntax mlish-provide #:export-as provide 1526 [(_ x:id ...) ≫ 1527 [⊢ x ≫ x- ⇒ ty_x] ... 1528 ; TODO: use hash-code to generate this tmp 1529 #:with (x-ty ...) (stx-map (lambda (y) (format-id y "~a-ty" y)) #'(x ...)) 1530 -------- 1531 [≻ (begin- 1532 (provide- x ...) 1533 (stlc+rec-iso:define-type-alias x-ty ty_x) ... 1534 (provide- x-ty ...))]]) 1535 (define-typed-syntax (require-typed x:id ... #:from mod) ≫ 1536 #:with (x-ty ...) (stx-map (lambda (y) (format-id y "~a-ty" y)) #'(x ...)) 1537 #:with (y ...) (generate-temporaries #'(x ...)) 1538 -------- 1539 [≻ (begin- 1540 (require- (rename-in (only-in mod x ... x-ty ...) [x y] ...)) 1541 (define-syntax x (make-rename-transformer (assign-type #'y #'x-ty))) ...)]) 1542 1543 (define-base-type Regexp) 1544 (provide (typed-out [regexp-match : (→ Regexp String (List String))] 1545 [regexp : (→ String Regexp)])) 1546 1547 (define-typed-syntax (equal? e1 e2) ≫ 1548 [⊢ e1 ≫ e1- ⇒ ty1] 1549 [⊢ e2 ≫ e2- ⇐ ty1] 1550 -------- 1551 [⊢ (equal?- e1- e2-) ⇒ Bool]) 1552 1553 (define-typed-syntax (read-int) ≫ 1554 -------- 1555 [⊢ (let- ([x (read-)]) 1556 (cond- [(exact-integer?- x) x] 1557 [else (error- 'read-int "expected an int, given: ~v" x)])) 1558 ⇒ Int]) 1559 1560 (define-typed-syntax (inst e ty ...) ≫ 1561 [⊢ (sysf:inst e ty ...) ≫ e- ⇒ ty_e] 1562 -------- 1563 [⊢ e- ⇒ #,(cond 1564 [(→? #'ty_e) #'(∀ () ty_e)] 1565 [(=>? #'ty_e) #'(∀ () ty_e)] 1566 [else #'ty_e])]) 1567 1568 (begin-for-syntax 1569 ;; - this function should be wrapped with err handlers, 1570 ;; for when an op with the specified generic op and input types does not exist, 1571 ;; otherwise, will get "unbound id" err with internal mangled id 1572 ;; - gen-op must be identifier, eg should already have proper context 1573 ;; and mangled-op is selected based on input types, 1574 ;; ie, dispatch to different concrete fns based on input tpyes 1575 ;; TODO: currently using input types only, but sometimes may need output type 1576 ;; eg, Read typeclass, this is currently unsupported 1577 ;; - need to use expected-type? 1578 (define (lookup-op gen-op tys) 1579 (define (transfer-gen-op-ctx o) (format-id gen-op "~a" o)) 1580 (define (transfer-gen-op-ctxs os) (stx-map transfer-gen-op-ctx os)) 1581 (syntax-parse tys 1582 ;; TODO: for now, only handle uniform tys, ie tys must be all 1583 ;; tycons or all base types or all tyvars 1584 ;; tycon -------------------------------------------------- 1585 ;; - recur on ty-args 1586 [(((~literal #%plain-app) tycon 1587 ((~literal #%plain-lambda) _ _ ty-arg ...)) ...) 1588 ;; 1) look up concrete op corresponding to generic op and input tys 1589 #:with mangled (mangle gen-op #'(tycon ...)) 1590 #:with [conc-op ty-conc-op] (infer+erase #'mangled) 1591 ;; compute sub-ops based on TC constraints (will include gen-op --- for smaller type) 1592 #:with (~∀ Xs (~=> TC ... (~ext-stlc:→ . ty-args))) #'ty-conc-op 1593 #:with (~TCs ([op _] ...) ...) #'(TC ...) ; order matters, must match order of arg types 1594 #:with ((sub-op ...) ...) (stx-map transfer-gen-op-ctxs #'((op ...) ...)) 1595 ;; drop the TCs in result type, the proper subops are already applied 1596 #:with ty-conc-op-noTC #'(∀ Xs (ext-stlc:→ . ty-args)) 1597 ;; recursively call lookup-op for each subop and input ty-args 1598 (⊢ (conc-op 1599 #,@(apply stx-appendmap (lambda (ops . tys) (stx-map (lambda (o) (lookup-op o tys)) ops)) 1600 #'((sub-op ...) ...) 1601 (syntax->list #'((ty-arg ...) ...)))) 1602 : ty-conc-op-noTC)] 1603 ;; base type -------------------------------------------------- 1604 [(((~literal #%plain-app) tag) ...) (expand/df (mangle gen-op #'(tag ...)))] 1605 ;; tyvars -------------------------------------------------- 1606 [_ (expand/df (mangle gen-op tys))])) 1607 (define (get-fn-ty-in-tags ty-fn) 1608 (syntax-parse ty-fn 1609 [(~∀ _ (~ext-stlc:→ ty_in ... _)) 1610 (get-type-tags #'(ty_in ...))])) 1611 (define (TC-exists? TC #:ctx [ctx TC]) ; throws exn if fail 1612 (syntax-parse TC 1613 [(~TC-base [gen-op ty-op] . _) ; only need 1st op 1614 (with-handlers 1615 ([exn:fail:syntax:unbound? 1616 (lambda (e) 1617 (type-error #:src ctx 1618 #:msg "No instance defined for ~a" TC))]) 1619 (expand/df 1620 (mangle (format-id ctx "~a" #'gen-op) 1621 (get-fn-ty-in-tags #'ty-op))))])) 1622 (define (TCs-exist? TCs #:ctx [ctx TCs]) 1623 (stx-map (lambda (tc) (TC-exists? tc #:ctx ctx)) TCs))) 1624 1625 ;; adhoc polymorphism 1626 ;; TODO: make this a formal type? 1627 ;; - or at least define a pattern expander - DONE 2016-05-01 1628 ;; A TC is a #'(=> subclassTC ... ([generic-op gen-op-ty] ...)) 1629 (define-syntax (define-typeclass stx) 1630 (syntax-parse stx 1631 [(~or (_ TC ... (~datum =>) (Name X ...) [op (~datum :) ty] ...) 1632 (~and (_ (Name X ...) [op (~datum :) ty] ...) ; no subclass 1633 (~parse (TC ...) #'()))) 1634 #'(begin- 1635 (define-syntax- (op stx) 1636 (syntax-parse stx 1637 [(o . es) 1638 #:with ([e- ty_e] (... ...)) (infers+erase #'es) 1639 #:with out-op 1640 (with-handlers 1641 ([exn:fail:syntax:unbound? 1642 (lambda (e) 1643 (type-error #:src #'o 1644 #:msg (format 1645 "~a operation undefined for input types: ~a" 1646 (syntax->datum #'o) 1647 (types->str #'(ty_e (... ...))))))]) 1648 (lookup-op #'o #'(ty_e (... ...)))) 1649 #:with app (datum->syntax #'o '#%app) 1650 (datum->syntax stx (cons #'app (cons #'out-op #'(e- (... ...)))))])) ... 1651 (define-syntax- (Name stx) 1652 (syntax-parse stx 1653 [(_ X ...) 1654 (add-orig 1655 #`(=> TC ... #,(mk-type #'(('op ty) ...))) 1656 #'(Name X ...))])))])) 1657 1658 (define-typed-syntax define-instance 1659 ;; base type, possibly with subclasses ------------------------------------ 1660 [(_ (Name ty ...) [generic-op concrete-op] ...) ≫ 1661 [⊢ (Name ty ...) ≫ 1662 (~=> TC ... (~TC [generic-op-expected ty-concrete-op-expected] ...)) ⇒ _] 1663 #:when (TCs-exist? #'(TC ...) #:ctx this-syntax) 1664 #:fail-unless (set=? (syntax->datum #'(generic-op ...)) 1665 (syntax->datum #'(generic-op-expected ...))) 1666 (type-error #:src this-syntax 1667 #:msg (format "Type class instance ~a incomplete, missing: ~a" 1668 (syntax->datum #'(Name ty ...)) 1669 (string-join 1670 (map symbol->string 1671 (set-subtract 1672 (syntax->datum #'(generic-op-expected ...)) 1673 (syntax->datum #'(generic-op ...)))) 1674 ", "))) 1675 ;; sort, using order from define-typeclass 1676 #:with ([generic-op-sorted concrete-op-sorted] ...) 1677 (stx-map 1678 (lambda (expected-op) 1679 (stx-findf 1680 (lambda (gen+conc) 1681 (equal? (syntax->datum (stx-car gen+conc)) 1682 (syntax->datum expected-op))) 1683 #'([generic-op concrete-op] ...))) 1684 #'(generic-op-expected ...)) 1685 ;; typecheck type of given concrete-op with expected type from define-typeclass 1686 [⊢ concrete-op-sorted ≫ concrete-op+ ⇐ ty-concrete-op-expected] ... 1687 ;; generate mangled name from tags in input types 1688 #:with (ty_in-tags ...) 1689 (stx-map 1690 (syntax-parser 1691 [(~∀ _ (~ext-stlc:→ ty_in ... _)) 1692 (get-type-tags #'(ty_in ...))]) 1693 #'(ty-concrete-op-expected ...)) 1694 ;; use input types 1695 #:with (mangled-op ...) (stx-map mangle #'(generic-op ...) #'(ty_in-tags ...)) 1696 -------- 1697 [≻ (begin- 1698 (define-syntax- (mangled-op stx) 1699 (syntax-parse stx 1700 [_:id (assign-type #'concrete-op+ #'ty-concrete-op-expected)])) 1701 ...)]] 1702 ;; tycon, possibly with subclasses ----------------------------------------- 1703 [(_ TC ... (~datum =>) (Name ty ...) [generic-op concrete-op] ...) ≫ 1704 #:with (X ...) (compute-tyvars #'(ty ...)) 1705 ;; ok to drop TCsub ...? I think yes 1706 ;; - the same TCsubs will be part of TC+, 1707 ;; so proper op will be looked up, depending on input args, 1708 ;; using inherited ops in TC+ 1709 ;; This is assuming Name and TC ... are the same typeclass 1710 ;; Won't work for, eg (TC1 (List X)) that depends on some other (TC2 X) 1711 #:with (Xs+ 1712 (TC+ ... 1713 (~=> TCsub ... 1714 (~TC [generic-op-expected ty-concrete-op-expected] ...))) 1715 _) 1716 (infers/tyctx+erase #'(X ...) #'(TC ... (Name ty ...))) 1717 ;; this produces #%app bad stx err, so manually call infer for now 1718 ;; [([X ≫ X- :: #%type] ...) () ⊢ (TC ... (Name ty ...)) ≫ 1719 ;; (TC+ ... 1720 ;; (~=> TCsub ... 1721 ;; (~TC [generic-op-expected ty-concrete-op-expected] ...))) 1722 ;; ⇒ _] 1723 ;; #:with Xs+ #'(X- ...) 1724 #:when (TCs-exist? #'(TCsub ...) #:ctx this-syntax) 1725 ;; simulate as if the declared concrete-op* has TC ... predicates 1726 ;; TODO: fix this manual deconstruction and assembly 1727 #:with ((app fa (lam _ ei ty_fn)) ...) #'(ty-concrete-op-expected ...) 1728 #:with (ty-concrete-op-expected-withTC ...) 1729 (stx-map (current-type-eval) #'((app fa (lam Xs+ ei (=> TC+ ... ty_fn))) ...)) 1730 #:fail-unless (set=? (syntax->datum #'(generic-op ...)) 1731 (syntax->datum #'(generic-op-expected ...))) 1732 (type-error #:src this-syntax 1733 #:msg (format "Type class instance ~a incomplete, missing: ~a" 1734 (syntax->datum #'(Name ty ...)) 1735 (string-join 1736 (map symbol->string 1737 (set-subtract 1738 (syntax->datum #'(generic-op-expected ...)) 1739 (syntax->datum #'(generic-op ...)))) 1740 ", "))) 1741 ;; - sort, using order from define-typeclass 1742 ;; - insert TC ... if lambda 1743 #:with ([generic-op-sorted concrete-op-sorted] ...) 1744 (stx-map 1745 (lambda (expected-op) 1746 (syntax-parse 1747 (stx-findf 1748 (lambda (gen+conc) 1749 (equal? (syntax->datum (stx-car gen+conc)) 1750 (syntax->datum expected-op))) 1751 #'([generic-op concrete-op] ...)) 1752 [(g c) 1753 (syntax-parse #'c 1754 ;; add TCs to (unexpanded) lambda 1755 [((~and lam (~literal liftedλ)) (args ...) . body) 1756 #'(g (lam (args ... #:where TC ...) . body))] 1757 [_ #'(g c)])])) 1758 #'(generic-op-expected ...)) 1759 ;; ;; for now, dont expand (and typecheck) concrete-op 1760 ;; #:with ([concrete-op+ ty-concrete-op] ...) (infers+erase #'(concrete-op ...)) 1761 ;; #:when (typechecks? #'(ty-concrete-op ...) #'(ty-concrete-op-expected ...)) 1762 ;; TODO: right now, dont recur to get nested tags 1763 ;; but may need to do so, ie if an instance needs to define more than one concrete op, 1764 ;; eg (define-instance (Eq (List Int)) ...) 1765 #:with (ty_in-tags ...) 1766 (stx-map 1767 (syntax-parser 1768 [(~∀ _ (~ext-stlc:→ ty_in ... _)) 1769 (get-type-tags #'(ty_in ...))] 1770 #;[(~∀ _ (~=> _ ... (~ext-stlc:→ ty_in ... _))) 1771 (get-type-tags #'(ty_in ...))]) 1772 #'(ty-concrete-op-expected ...)) 1773 #:with (mangled-op ...) (stx-map mangle #'(generic-op ...) #'(ty_in-tags ...)) 1774 ;; need a name for concrete-op because concrete-op and generic-op may be 1775 ;; mutually recursive, eg (Eq (List X)) 1776 #:with (f ...) (generate-temporaries #'(concrete-op-sorted ...)) 1777 -------- 1778 [≻ (begin- 1779 (define- f concrete-op-sorted) ... 1780 (define-syntax- (mangled-op stx) 1781 (syntax-parse stx 1782 [_:id (assign-type #'f #'ty-concrete-op-expected-withTC)])) 1783 ...)]]) 1784