fabul.rkt (8200B)
1 #lang turnstile 2 (require (for-syntax "fabul-utils.rkt" 3 turnstile/mode)) 4 5 (provide begin let let* letrec λ lambda #%app if tup cons nil 6 drop match-list 7 proj isnil head tail list-ref member 8 define 9 %L %U 10 #%module-begin #%top-interaction require 11 (typed-out [= : (→ Int Int Int)] 12 [< : (→ Int Int Bool)] 13 [sub1 : (→ Int Int)] 14 [add1 : (→ Int Int)] 15 [zero? : (→ Int Bool)])) 16 17 ; import other languages 18 (require (prefix-in U: "../ext-stlc.rkt") 19 (prefix-in U: (except-in "../stlc+cons.rkt" tup proj)) 20 (prefix-in U: (only-in "../stlc+tup.rkt" tup proj)) 21 (prefix-in L: "lin.rkt") 22 (prefix-in L: "lin+cons.rkt") 23 (only-in "../ext-stlc.rkt" → ~→) 24 (only-in "../stlc+tup.rkt" × ~×) 25 (only-in "../stlc+cons.rkt" List ~List) 26 (only-in "lin+cons.rkt" ⊗ ~⊗ MList ~MList) 27 (only-in "lin+tup.rkt" in-cad*rs) 28 "lin.rkt" #| this includes base types like Int, Unit, etc. |#) 29 30 ; reuse types 31 (reuse Unit Bool Int Float String → #:from "../ext-stlc.rkt") 32 (reuse × #:from "../stlc+tup.rkt") 33 (reuse List #:from "../stlc+cons.rkt") 34 (reuse -o ⊗ MList #:from "lin+cons.rkt") 35 36 ; reuse forms 37 (reuse #%datum ann and or define-type-alias #:from "../ext-stlc.rkt") 38 39 40 41 ; begin in unrestricted mode 42 (begin-for-syntax 43 (current-mode (make-empty-unrestricted-mode))) 44 45 46 ; dispatch some forms to L: or U: variant, based on [current-language] 47 (define-syntax language-dispatch 48 (syntax-parser 49 [(_ [lang ...] form) 50 #:with (form/lang ...) (stx-map (λ (X) (format-id X "~a:~a" X #'form)) #'[lang ...]) 51 #'(define-syntax form 52 (syntax-parser 53 [(_ . args) 54 #:when (eq? (current-language) 'lang) 55 (syntax/loc this-syntax 56 (form/lang . args))] ... 57 [_ 58 (raise-syntax-error 'form 59 (format "form not allowed inside ~a language" 60 (language-name)))]))] 61 62 [(_ [lang ...] form ...+) 63 #'(begin- 64 (language-dispatch [lang ...] form) ...)])) 65 66 (language-dispatch [L U] begin let let* letrec λ lambda #%app if tup cons nil) 67 (language-dispatch [L] drop match-list) 68 (language-dispatch [U] proj isnil head tail list-ref member) 69 70 71 (begin-for-syntax 72 (define (fully-unrestricted? type) 73 (and (unrestricted-type? type) 74 (syntax-parse type 75 [(~Any _ τ ...) (for/and ([t (in-syntax #'[τ ...])]) 76 (fully-unrestricted? t))] 77 [_ #t]))) 78 79 (define (fail/type-convert src lang ty) 80 (raise-syntax-error #f (format "cannot convert type ~a into ~a language" 81 (type->str ty) 82 (language-name lang)) 83 src)) 84 85 ; convert-type : Symbol Type -> Type 86 ; converts a type into a more appropriate variant for the given language 87 (define (convert-type lang type 88 #:src [fail-src #f] 89 #:fail [fail (λ (_) (fail/type-convert fail-src lang type))]) 90 (define converter 91 (case lang 92 [(L) 93 (type-converter ([σ #:when (linear-type? #'σ) #'σ]) 94 ([List => MList] 95 [× => ⊗] 96 [→ => →] 97 [-o => -o]) 98 fail)] 99 100 [(U) 101 (type-converter ([τ #:when (fully-unrestricted? #'τ) #'τ]) 102 ([MList => List] 103 [⊗ => ×] 104 [→ => →]) 105 fail)] 106 107 [else (error "invalid language" lang)])) 108 109 ((current-type-eval) (converter type))) 110 111 ; convert-syntax : Type Type Syntax -> Syntax 112 ; creates an expression that wraps the given syntax such that 113 ; it converts objects from the first type into the second type. 114 ; the resulting syntax will never evaluate the original syntax twice. 115 ; e.g. 116 ; (convert-stx #'(List Int) #'(MList Int) #'x) 117 ; -> 118 ; #'(foldr mcons '() x) 119 (define (convert-syntax . args) 120 (syntax-parse args 121 [[τ σ src] #:when (type=? #'τ #'σ) #'src] 122 123 ; convert tuples 124 [[(~or (~⊗ τ ...) (~× τ ...)) (~or (~⊗ σ ...) (~× σ ...)) src] 125 #:with [out ...] (for/list ([cad*r (in-cad*rs #'tmp)] 126 [T (in-syntax #'[τ ...])] 127 [S (in-syntax #'[σ ...])]) 128 (convert-syntax T S cad*r)) 129 #'(let- ([tmp src]) (#%app- list- out ...))] 130 131 ; convert lists 132 [[(~List τ) (~MList σ) src] 133 #:with x+ (convert-syntax #'τ #'σ #'x) 134 #'(#%app- foldr- (λ- (x l) (#%app- mcons- x+ l)) '() src)] 135 136 [[(~MList τ) (~List σ) src] 137 #:with x+ (convert-syntax #'τ #'σ #'x) 138 #'(for/list- ([x (in-mlist src)]) x+)] 139 140 ; convert functions 141 [[(~or (~→ τ ... τ_out) (~-o τ ... τ_out)) 142 (~or (~→ σ ... σ_out) (~-o σ ... σ_out)) 143 src] 144 #:with (x ...) (stx-map generate-temporary #'[τ ...]) 145 #:with (x+ ...) (stx-map convert-syntax #'[σ ...] #'[τ ...] #'[x ...]) 146 #:with out (convert-syntax #'τ_out #'σ_out #'(#%app- f x+ ...)) 147 #'(let- ([f src]) (λ- (x ...) out))])) 148 149 ) 150 151 152 ; generate barrier crossing macros 153 (define-syntax define-barrier 154 (syntax-parser 155 [(_ form LANG A->B) 156 #'(define-typed-syntax form 157 [(_ e) ≫ 158 #:when (eq? (syntax-local-context) 'expression) 159 #:fail-when (eq? (current-language) 'LANG) 160 (format "already in ~a language" 161 (language-name 'LANG)) 162 [⊢ [e ≫ e- ⇒ τ] #:submode A->B] 163 #:with σ (convert-type (current-language) #'τ #:src this-syntax) 164 #:with e-- (convert-syntax #'τ #'σ #'e-) 165 -------- 166 [⊢ e-- ⇒ σ]] 167 168 ; expand toplevels using different syntax, bleh 169 [(_ e ...+) ≫ 170 #:submode (if (eq? (current-language) 'LANG) 171 values 172 A->B) 173 (#:with e- (local-expand #'(begin- e (... ...)) 174 'top-level 175 '())) 176 -------- 177 [≻ e-]])])) 178 179 (define-barrier %L L U->L) 180 (define-barrier %U U L->U) 181 182 183 ; variable syntax 184 (define-typed-variable-syntax 185 #:datum-literals (:) 186 [(_ x- : τ) ≫ 187 #:when (eq? (current-language) 'U) 188 #:fail-unless (fully-unrestricted? #'τ) 189 (raise-syntax-error #f "cannot use linear variable from unrestricted language" #'x-) 190 -------- 191 [⊢ x- ⇒ τ]] 192 193 [(_ x- : σ) ≫ 194 #:when (eq? (current-language) 'L) 195 -------- 196 [≻ (#%lin-var x- : σ)]]) 197 198 ; define syntax 199 (define-typed-syntax define 200 #:datum-literals (:) 201 [(define (f [x:id : ty] ...) ret 202 e ...+) ≫ 203 -------- 204 [≻ (define f : (→ ty ... ret) 205 (letrec ([{f : (→ ty ... ret)} 206 (λ (x ...) 207 (begin e ...))]) 208 f))]] 209 210 [(_ x:id : τ:type e:expr) ≫ 211 #:fail-when (linear-type? #'τ.norm) 212 "cannot define linear type globally" 213 #:with y (generate-temporary #'x) 214 -------- 215 [≻ (begin- 216 (define-syntax x (make-rename-transformer (⊢ y : τ.norm))) 217 (define- y (ann e : τ.norm)))]]) 218 219 220 ; REPL prints expression types 221 ; enter :lang=L or :lang=U to switch language in REPL 222 (define-typed-syntax #%top-interaction 223 [(_ . d) ≫ 224 #:when (regexp-match? #px":lang=L" (~a (syntax-e #'d))) 225 #:do [(when (unrestricted-mode? (current-mode)) 226 (current-mode (U->L (current-mode))))] 227 -------- 228 [≻ (#%app- void-)]] 229 230 [(_ . d) ≫ 231 #:when (regexp-match? #px":lang=U" (~a (syntax-e #'d))) 232 #:do [(when (linear-mode? (current-mode)) 233 (current-mode (L->U (current-mode))))] 234 -------- 235 [≻ (#%app- void-)]] 236 237 [(_ . e) ≫ 238 #:do [(printf "; language: ~a\n" (language-name))] 239 [⊢ e ≫ e- ⇒ τ] 240 -------- 241 [≻ (#%app- printf- '"~v : ~a\n" e- '#,(type->str #'τ))]])