stlc+cons.rkt (3078B)
1 #lang s-exp macrotypes/typecheck 2 (extends "stlc+reco+var.rkt") 3 4 ;; Simply-Typed Lambda Calculus, plus cons 5 ;; Types: 6 ;; - types from stlc+reco+var.rkt 7 ;; - List constructor 8 ;; Terms: 9 ;; - terms from stlc+reco+var.rkt 10 11 ;; TODO: enable HO use of list primitives 12 13 (provide (type-out List) 14 nil isnil cons list head tail 15 reverse length list-ref member) 16 17 (define-type-constructor List) 18 19 (define-typed-syntax nil 20 [(_ ~! τi:type-ann) 21 (⊢ null- : (List τi.norm))] 22 ; minimal type inference 23 [nil:id 24 #:with expected-τ (get-expected-type #'nil) 25 ; 'expected-type property exists (ie, not false) 26 #:fail-unless (syntax-e #'expected-τ) 27 (raise 28 (exn:fail:type:infer 29 (format 30 "~a (~a:~a): nil: ~a" 31 (syntax-source stx) (syntax-line stx) (syntax-column stx) 32 (no-expected-type-fail-msg)) 33 (current-continuation-marks))) 34 #:fail-unless (List? #'expected-τ) 35 (raise 36 (exn:fail:type:infer 37 (format 38 "~a (~a:~a): Inferred ~a type for nil, which is not a List." 39 (syntax-source stx) (syntax-line stx) (syntax-column stx) 40 (type->str #'ty_lst)) 41 (current-continuation-marks))) 42 (⊢ null- : expected-τ)]) 43 (define-typed-syntax cons 44 [(_ e1 e2) 45 #:with [e1- τ_e1] (infer+erase #'e1) 46 #:with τ_list ((current-type-eval) #'(List τ_e1)) 47 #:with [e2- τ_e2] (infer+erase (add-expected-ty #'e2 #'τ_list)) 48 #:fail-unless (typecheck? #'τ_e2 #'τ_list) 49 (typecheck-fail-msg/1 #'τ_list #'τ_e2 #'e2) 50 ;; propagate up inferred types of variables 51 #:with env (stx-flatten (filter (λ (x) x) (stx-map get-env #'(e1- e2-)))) 52 #:with result-cons (add-env #'(cons- e1- e2-) #'env) 53 (⊢/no-teval result-cons : τ_list)]) 54 (define-typed-syntax isnil 55 [(_ e) 56 #:with [e- (~List _)] (infer+erase #'e) 57 (⊢ (null?- e-) : Bool)]) 58 (define-typed-syntax head 59 [(_ e) 60 #:with [e- (~List τ)] (infer+erase #'e) 61 (⊢/no-teval (car- e-) : τ)]) 62 (define-typed-syntax tail 63 [(_ e) 64 #:with [e- τ_lst] (infer+erase #'e) 65 #:when (List? #'τ_lst) 66 (⊢/no-teval (cdr- e-) : τ_lst)]) 67 (define-typed-syntax list 68 [(_) #'nil] 69 [(_ x . rst) ; has expected type 70 #:with expected-τ (get-expected-type stx) 71 #:when (syntax-e #'expected-τ) 72 #:with (~List τ) (local-expand #'expected-τ 'expression null) 73 #'(cons (add-expected x τ) (list . rst))] 74 [(_ x . rst) ; no expected type 75 #'(cons x (list . rst))]) 76 (define-typed-syntax reverse 77 [(_ e) 78 #:with (e- τ-lst) (infer+erase #'e) 79 #:when (List? #'τ-lst) 80 (⊢/no-teval (reverse- e-) : τ-lst)]) 81 (define-typed-syntax length 82 [(_ e) 83 #:with (e- τ-lst) (infer+erase #'e) 84 #:when (List? #'τ-lst) 85 (⊢ (length- e-) : Int)]) 86 (define-typed-syntax list-ref 87 [(_ e n) 88 #:with (e- (ty)) (⇑ e as List) 89 #:with n- (⇑ n as Int) 90 (⊢/no-teval (list-ref- e- n-) : ty)]) 91 (define-typed-syntax member 92 [(_ v e) 93 #:with (e- (ty)) (⇑ e as List) 94 #:with [v- ty_v] (infer+erase #'(add-expected v ty)) 95 #:when (typecheck? #'ty_v #'ty) 96 (⊢ (member- v- e-) : Bool)])