stlc+overloading.rkt (6081B)
1 #lang s-exp macrotypes/typecheck 2 (reuse List cons nil #:from "stlc+cons.rkt") 3 (extends "stlc+sub.rkt" #:except #%datum) 4 5 ;; Revision of overloading, using identifier macros instead of overriding #%app 6 7 ;; ============================================================================= 8 9 (provide Bot Str #%datum signature resolve instance) 10 11 (define-base-types Bot Str) 12 13 (define-typed-syntax #%datum 14 [(_ . n:str) (⊢ (#%datum- . n) : Str)] 15 [(_ . x) #'(stlc+sub:#%datum . x)]) 16 17 (define-for-syntax xerox syntax->datum) 18 19 ;; ============================================================================= 20 ;; === Resolvers 21 22 (begin-for-syntax 23 (struct ℜ ( 24 name ;; Symbol 25 dom* ;; (Box (Listof (Pairof Type Expr))) 26 cod ;; Type 27 ) #:constructor-name make-ℜ 28 #:transparent 29 #:property prop:procedure 30 (lambda (self τ-or-e #:exact? [exact? #f]) 31 (define r 32 (if (syntax? τ-or-e) ;; Can I ask "type?" 33 (ℜ-resolve-syntax self τ-or-e #:exact? exact?) 34 (ℜ-resolve-value self τ-or-e #:exact? exact?))) 35 (or r 36 (error 'ℜ (format "Resolution for '~a' failed at type ~a" 37 (syntax->datum (ℜ-name self)) 38 τ-or-e)))) 39 ) 40 41 ;; Rad! 42 (define (ℜ-add! ℜ τ e) 43 (define dom* (ℜ-dom* ℜ)) 44 (set-box! dom* (cons (cons τ e) (unbox dom*)))) 45 46 (define (ℜ-init name τ-cod) 47 (make-ℜ name (box '()) τ-cod)) 48 49 (define (ℜ->type ℜ #:subst [τ-dom (assign-type #''α #'#%type)]) 50 ((current-type-eval) #`(→ #,τ-dom #,(ℜ-cod ℜ)))) 51 52 (define (ℜ-find ℜ τ #:=? =?) 53 (define (τ=? τ2) 54 (=? τ τ2)) 55 (assf τ=? (unbox (ℜ-dom* ℜ)))) 56 57 (define (ℜ-resolve-syntax ℜ τ #:exact? [exact? #f]) 58 ;; First try exact matches, then fall back to subtyping (unless 'exact?' is set). 59 ;; When subtyping, the __order instances were declared__ resolves ties. 60 (define result 61 (or (ℜ-find ℜ τ #:=? (current-type=?)) 62 (and (not exact?) 63 (ℜ-find ℜ τ #:=? (current-typecheck-relation))))) 64 (and (pair? result) 65 (cdr result))) 66 67 (define (ℜ-resolve-value ℜ e #:exact? [exact? #f]) 68 (error 'ℜ (format "Runtime resolution not implemented. Anyway your value was ~a" e))) 69 70 (define (ℜ-unbound? ℜ τ) 71 (not (ℜ-resolve-syntax ℜ τ #:exact? #t))) 72 73 (define (syntax->ℜ id) 74 ;; Don't care about the type 75 (define stx+τ (infer+erase id)) 76 ;; Boy, I wish I had a monad 77 (define (fail) 78 (error 'resolve (format "Identifier '~a' is not overloaded" (syntax->datum id)))) 79 (unless (pair? stx+τ) (fail)) 80 (define stx (car stx+τ)) 81 (unless (syntax? stx) (fail)) 82 (define ℜ-stx (syntax->datum (car stx+τ))) 83 (unless (and (list? ℜ-stx) 84 (not (null? ℜ-stx)) 85 (not (null? (cdr ℜ-stx)))) 86 (fail)) 87 (define ℜ (cadr ℜ-stx)) 88 (unless (ℜ? ℜ) (fail)) 89 ℜ) 90 91 (define-syntax-rule (error-template sym id τ reason) 92 (error sym (format "Failure for '~a' at type '~a'. ~a" 93 (syntax->datum id) 94 (syntax->datum τ) 95 reason))) 96 97 (define-syntax-rule (instance-error id τ reason) 98 (error-template 'instance id τ reason)) 99 100 (define-syntax-rule (resolve-error id τ reason) 101 (error-template 'resolve id τ reason)) 102 ) 103 104 ;; ============================================================================= 105 ;; === Overloaded signature environment 106 107 (define-typed-syntax signature 108 [(_ (name:id α:id) τ) 109 #:with ((α+) (~→ τ_α:id τ-cod) _) (infer/tyctx+erase #'([α :: #%type]) #'τ) 110 (define ℜ (ℜ-init #'name #'τ-cod)) 111 (⊢ (define-syntax name 112 (syntax-parser 113 [_:id 114 #'(quote- #,ℜ)] ;; Is there a way to transmit ℜ directly? 115 [(n e) 116 #:with [e+ τ+] (infer+erase #'e) 117 #:with n+ (#,ℜ #'τ+) 118 (⊢ (#%app- n+ e+) 119 : τ-cod)] 120 [(_ e* (... ...)) 121 #'(raise-arity-error- (syntax->datum- name) 1 e* (... ...))])) 122 : Bot)] 123 [(_ e* ...) 124 (error 'signature (format "Expected (signature (NAME VAR) (→ VAR τ)), got ~a" (xerox #'(e* ...))))]) 125 126 (define-typed-syntax resolve 127 [(_ name:id τ) 128 #:with τ+ ((current-type-eval) #'τ) 129 ;; Extract a resolver from the syntax object 130 (define ℜ (syntax->ℜ #'name)) 131 ;; Apply the resolver to the argument type. woo-wee! 132 (⊢ #,(ℜ #'τ+ #:exact? #t) : #,(ℜ->type ℜ #:subst #'τ+))]) 133 134 (define-typed-syntax instance 135 [(_ (name:id τ-stx) e) 136 #:with τ ((current-type-eval) #'τ-stx) 137 #:with [e+ τ+] (infer+erase #'e) 138 (define ℜ (syntax->ℜ #'name)) 139 (unless (ℜ-unbound? ℜ #'τ) (instance-error #'name #'τ "Overlaps with existing instance.")) 140 (define _unify ;; Should be a helper function 141 (syntax-parse #`(τ+ #,(ℜ->type ℜ)) 142 [((~→ τ_dom1 τ_cod1) 143 (~→ _ τ_cod2)) 144 ;; Really, need to unify this type with the template 145 ;; (unless ((current-type=?) τ_dom1 τ_dom2) 146 ;; (instance-error #'name #'τ (format "Domain '~a' must unify with template domain '~a'." 147 ;; (syntax->datum #'τ_dom1) (syntax->datum #'τ_dom2)))) 148 (unless ((current-type=?) ((current-type-eval) #'τ) #'τ_dom1) 149 (instance-error #'name #'τ (format "Domain '~a' must be the instance type, for now (2015-10-20)." (syntax->datum #'τ_dom1)))) 150 (unless ((current-type=?) #'τ_cod1 #'τ_cod2) 151 (instance-error #'name #'τ (format "Codomain '~a' must match template codomain '~a'" 152 (syntax->datum #'τ_cod1) (syntax->datum #'τ_cod2)))) 153 (void)] 154 [(a b) 155 (instance-error #'name #'τ (format "May only overload single-argument functions. (Got ~a and ~a)" 156 (syntax->datum #'a) (syntax->datum #'b)) 157 )])) 158 ;; Should we use syntax instead of e+ ? 159 (ℜ-add! ℜ #'τ #'e+) 160 (⊢ (void-) : Bot)] 161 [_ 162 (error 'instance "Expected (instance (id τ) e).")]) 163 164