rosette2.rkt (28002B)
1 #lang turnstile 2 (extends "../stlc.rkt" 3 #:except #%module-begin #%app →) 4 (reuse #%datum define-type-alias define-named-type-alias 5 #:from "../stlc+union.rkt") 6 (reuse list #:from "../stlc+cons.rkt") 7 8 (provide (rename-out [ro:#%module-begin #%module-begin]) 9 Any Nothing 10 CU U 11 C→ → (for-syntax ~C→ C→?) 12 Ccase-> ; TODO: symbolic case-> not supported yet 13 CListof CVectorof CMVectorof CIVectorof 14 CParamof ; TODO: symbolic Param not supported yet 15 CUnit Unit 16 CNegInt NegInt 17 CZero Zero 18 CPosInt PosInt 19 CNat Nat 20 CInt Int 21 CFloat Float 22 CNum Num 23 CFalse CTrue CBool Bool 24 CString String 25 CStx ; symblic Stx not supported 26 ;; BV types 27 CBV BV 28 CBVPred BVPred 29 CSolution CPict) 30 31 (require 32 (prefix-in ro: rosette) 33 (only-in "../stlc+union.rkt" define-named-type-alias prune+sort current-sub?) 34 (prefix-in C 35 (combine-in 36 (only-in "../stlc+union+case.rkt" 37 PosInt Zero NegInt Float True False String [U U*] U*? 38 [case-> case->*] → →?) 39 (only-in "../stlc+cons.rkt" Unit [List Listof]))) 40 (only-in "../stlc+union+case.rkt" [~U* ~CU*] [~case-> ~Ccase->] [~→ ~C→]) 41 (only-in "../stlc+cons.rkt" [~List ~CListof]) 42 (only-in "../stlc+reco+var.rkt" [define stlc:define]) 43 (rename-in "rosette-util.rkt" [bitvector? lifted-bitvector?])) 44 45 ;; copied from rosette.rkt 46 (provide rosette-typed-out) 47 (define-for-syntax (mk-ro:-id id) (format-id id "ro:~a" id)) 48 49 (define-syntax rosette-typed-out 50 (make-provide-pre-transformer 51 (lambda (stx modes) 52 (syntax-parse stx #:datum-literals (:) 53 ;; cannot write ty:type bc provides might precede type def 54 [(_ (~and (~or (~and [out-x:id (~optional :) ty] (~parse x #'out-x)) 55 [[x:id (~optional :) ty] out-x:id])) ...) 56 #:with (ro-x ...) (stx-map mk-ro:-id #'(x ...)) 57 (pre-expand-export (syntax/loc stx (typed-out [[ro-x ty] out-x] ...)) 58 modes)])))) 59 60 ;; providing version of define-typed-syntax 61 (define-syntax (define-typed-syntax stx) 62 (syntax-parse stx 63 [(_ name:id #:export-as out-name:id . rst) 64 #'(begin- 65 (provide- (rename-out [name out-name])) 66 (define-typerule name . rst))] ; define-typerule doesnt provide 67 [(_ name:id . rst) 68 #'(define-typed-syntax name #:export-as name . rst)] 69 [(_ (name:id . pat) . rst) 70 #'(define-typed-syntax name #:export-as name [(_ . pat) . rst])])) 71 72 ;; --------------------------------- 73 ;; Concrete and Symbolic union types 74 75 (begin-for-syntax 76 (define (concrete? t) 77 (not (or (Any? t) (U*? t))))) 78 79 (define-base-types Any CBV CStx CSymbol) 80 ;; CVectorof includes all vectors 81 ;; CIVectorof includes only immutable vectors 82 ;; CMVectorof includes only mutable vectors 83 (define-type-constructor CIVectorof #:arity = 1) 84 (define-type-constructor CMVectorof #:arity = 1) 85 (define-named-type-alias (CVectorof X) (CU (CIVectorof X) (CMVectorof X))) 86 87 (define-syntax (CU stx) 88 (syntax-parse stx 89 [(_ . tys) 90 #:with tys+ (stx-map (current-type-eval) #'tys) 91 #:fail-unless (stx-andmap concrete? #'tys+) 92 "CU requires concrete types" 93 #'(CU* . tys+)])) 94 95 (define-named-type-alias Nothing (CU)) 96 97 ;; internal symbolic union constructor 98 (define-type-constructor U* #:arity >= 0) 99 100 ;; user-facing symbolic U constructor: flattens and prunes 101 (define-syntax (U stx) 102 (syntax-parse stx 103 [(_ . tys) 104 ;; canonicalize by expanding to U*, with only (sorted and pruned) leaf tys 105 #:with ((~or (~U* ty1- ...) (~CU* ty2- ...) ty3-) ...) (stx-map (current-type-eval) #'tys) 106 #:with tys- (prune+sort #'(ty1- ... ... ty2- ... ... ty3- ...)) 107 #'(U* . tys-)])) 108 109 ;; --------------------------------- 110 ;; case-> and Ccase-> 111 112 ;; Ccase-> must check that its subparts are concrete → types 113 (define-syntax (Ccase-> stx) 114 (syntax-parse stx 115 [(_ . tys) 116 #:with tys+ (stx-map (current-type-eval) #'tys) 117 #:fail-unless (stx-andmap C→? #'tys+) 118 "CU require concrete arguments" 119 #'(Ccase->* . tys+)])) 120 121 ;; TODO: What should case-> do when given symbolic function 122 ;; types? Should it transform (case-> (U (C→ τ ...)) ...) 123 ;; into (U (Ccase-> (C→ τ ...) ...)) ? What makes sense here? 124 125 ;; --------------------------------- 126 ;; Symbolic versions of types 127 128 (begin-for-syntax 129 (define (add-pred stx pred) 130 (set-stx-prop/preserved stx 'pred pred)) 131 (define (get-pred stx) 132 (syntax-property stx 'pred))) 133 134 (define-syntax-parser add-predm 135 [(_ stx pred) (add-pred #'stx #'pred)]) 136 137 (define-named-type-alias NegInt (add-predm (U CNegInt) negative-integer?)) 138 (define-named-type-alias Zero (add-predm (U CZero) zero-integer?)) 139 (define-named-type-alias PosInt (add-predm (U CPosInt) positive-integer?)) 140 (define-named-type-alias Float (U CFloat)) 141 (define-named-type-alias String (U CString)) 142 (define-named-type-alias Unit (add-predm (U CUnit) ro:void?)) 143 (define-named-type-alias (CParamof X) (Ccase-> (C→ X) 144 (C→ X CUnit))) 145 146 (define-syntax → 147 (syntax-parser 148 [(_ ty ...+) 149 (add-orig #'(U (C→ ty ...)) this-syntax)])) 150 151 (define-syntax define-symbolic-named-type-alias 152 (syntax-parser 153 [(_ Name:id Cτ:expr #:pred p?) 154 #:with Cτ+ ((current-type-eval) #'Cτ) 155 #:fail-when (and (not (concrete? #'Cτ+)) #'Cτ+) 156 "should be a concrete type" 157 #:with CName (format-id #'Name "C~a" #'Name #:source #'Name) 158 #'(begin- 159 (define-named-type-alias CName Cτ) 160 (define-named-type-alias Name (add-predm (U CName) p?)))])) 161 162 (define-symbolic-named-type-alias Bool (CU CFalse CTrue) #:pred ro:boolean?) 163 (define-symbolic-named-type-alias Nat (CU CZero CPosInt) #:pred nonnegative-integer?) 164 (define-symbolic-named-type-alias Int (CU CNegInt CNat) #:pred ro:integer?) 165 (define-symbolic-named-type-alias Num (CU CFloat CInt) #:pred ro:real?) 166 167 ;; --------------------------------- 168 ;; define-symbolic 169 170 (define-typed-syntax define-symbolic 171 [(_ x:id ...+ pred : ty:type) ≫ 172 ;; TODO: still unsound 173 [⊢ [pred ≫ pred- ⇐ : (C→ ty.norm Bool)]] 174 #:with (y ...) (generate-temporaries #'(x ...)) 175 -------- 176 [_ ≻ (begin- 177 (define-syntax- x (make-rename-transformer (⊢ y : ty.norm))) ... 178 (ro:define-symbolic y ... pred-))]]) 179 180 (define-typed-syntax define-symbolic* 181 [(_ x:id ...+ pred : ty:type) ≫ 182 ;; TODO: still unsound 183 [⊢ [pred ≫ pred- ⇐ : (C→ ty.norm Bool)]] 184 #:with (y ...) (generate-temporaries #'(x ...)) 185 -------- 186 [_ ≻ (begin- 187 (define-syntax- x (make-rename-transformer (⊢ y : ty.norm))) ... 188 (ro:define-symbolic* y ... pred-))]]) 189 190 ;; TODO: support internal definition contexts 191 (define-typed-syntax let-symbolic 192 [(_ ([(x:id ...+) pred : ty:type]) e ...) ≫ 193 [⊢ [pred ≫ pred- ⇐ : (C→ ty.norm Bool)]] 194 [([x ≫ x- : ty.norm] ...) ⊢ [(begin e ...) ≫ e- ⇒ τ_out]] 195 -------- 196 [⊢ [_ ≫ (ro:let-values 197 ([(x- ...) (ro:let () 198 (ro:define-symbolic x ... pred-) 199 (ro:values x ...))]) 200 e-) ⇒ : τ_out]]]) 201 (define-typed-syntax let-symbolic* 202 [(_ ([(x:id ...+) pred : ty:type]) e ...) ≫ 203 [⊢ [pred ≫ pred- ⇐ : (C→ ty.norm Bool)]] 204 [([x ≫ x- : ty.norm] ...) ⊢ [(begin e ...) ≫ e- ⇒ τ_out]] 205 -------- 206 [⊢ [_ ≫ (ro:let-values 207 ([(x- ...) (ro:let () 208 (ro:define-symbolic* x ... pred-) 209 (ro:values x ...))]) 210 e-) ⇒ : τ_out]]]) 211 212 ;; --------------------------------- 213 ;; assert, assert-type 214 215 (define-typed-syntax assert 216 [(_ e) ≫ 217 [⊢ [e ≫ e- ⇒ : _]] 218 -------- 219 [⊢ [_ ≫ (ro:assert e-) ⇒ : CUnit]]] 220 [(_ e m) ≫ 221 [⊢ [e ≫ e- ⇒ : _]] 222 [⊢ [m ≫ m- ⇐ : (CU CString (C→ Nothing))]] 223 -------- 224 [⊢ [_ ≫ (ro:assert e- m-) ⇒ : CUnit]]]) 225 226 (define-typed-syntax assert-type #:datum-literals (:) 227 [(_ e : ty:type) ≫ 228 [⊢ [e ≫ e- ⇒ : _]] 229 #:with pred (get-pred #'ty.norm) 230 -------- 231 [⊢ [_ ≫ (ro:#%app assert-pred e- pred) ⇒ : ty.norm]]]) 232 233 234 ;; --------------------------------- 235 ;; Racket forms 236 237 ;; TODO: many of these implementations are copied code, with just the macro 238 ;; output changed to use the ro: version. 239 ;; Is there a way to abstract this? macro mixin? 240 241 (define-typed-syntax define #:datum-literals (: -> →) 242 [(_ x:id e) ≫ 243 -------- 244 [_ ≻ (stlc:define x e)]] 245 [(_ (f [x : ty] ... (~or → ->) ty_out) e ...+) ≫ 246 ; [⊢ [e ≫ e- ⇒ : ty_e]] 247 #:with f- (generate-temporary #'f) 248 -------- 249 [_ ≻ (begin- 250 (define-syntax- f 251 (make-rename-transformer (⊢ f- : (C→ ty ... ty_out)))) 252 (ro:define f- 253 (stlc:λ ([x : ty] ...) (ann (begin e ...) : ty_out))))]]) 254 255 ;; --------------------------------- 256 ;; quote 257 258 (define-typed-syntax quote 259 [(_ x:id) ≫ 260 -------- 261 [⊢ [_ ≫ (quote- x) ⇒ : CSymbol]]] 262 [(_ (x:id ...)) ≫ 263 -------- 264 [⊢ [_ ≫ (quote- (x ...)) ⇒ : (CListof CSymbol)]]]) 265 266 ;; --------------------------------- 267 ;; Function Application 268 269 ;; copied from rosette.rkt 270 (define-typed-syntax app #:export-as #%app 271 [(_ e_fn e_arg ...) ≫ 272 [⊢ [e_fn ≫ e_fn- ⇒ : (~C→ ~! τ_in ... τ_out)]] 273 #:with e_fn/progsrc- (replace-stx-loc #'e_fn- #'e_fn) 274 #:fail-unless (stx-length=? #'[τ_in ...] #'[e_arg ...]) 275 (num-args-fail-msg #'e_fn #'[τ_in ...] #'[e_arg ...]) 276 [⊢ [e_arg ≫ e_arg- ⇐ : τ_in] ...] 277 -------- 278 ;; TODO: use e_fn/progsrc- (currently causing "cannot use id tainted in macro trans" err) 279 [⊢ [_ ≫ (ro:#%app e_fn/progsrc- e_arg- ...) ⇒ : τ_out]]] 280 [(_ e_fn e_arg ...) ≫ 281 [⊢ [e_fn ≫ e_fn- ⇒ : (~Ccase-> ~! . (~and ty_fns ((~C→ . _) ...)))]] 282 #:with e_fn/progsrc- (replace-stx-loc #'e_fn- #'e_fn) 283 [⊢ [e_arg ≫ e_arg- ⇒ : τ_arg] ...] 284 #:with τ_out 285 (for/first ([ty_f (stx->list #'ty_fns)] 286 #:when (syntax-parse ty_f 287 [(~C→ τ_in ... τ_out) 288 (and (stx-length=? #'(τ_in ...) #'(e_arg ...)) 289 (typechecks? #'(τ_arg ...) #'(τ_in ...)))])) 290 (syntax-parse ty_f [(~C→ _ ... t_out) #'t_out])) 291 #:fail-unless (syntax-e #'τ_out) 292 ; use (failing) typechecks? to get err msg 293 (syntax-parse #'ty_fns 294 [((~C→ τ_in ... _) ...) 295 (let* ([τs_expecteds #'((τ_in ...) ...)] 296 [τs_given #'(τ_arg ...)] 297 [expressions #'(e_arg ...)]) 298 (format (string-append "type mismatch\n" 299 " expected one of:\n" 300 " ~a\n" 301 " given: ~a\n" 302 " expressions: ~a") 303 (string-join 304 (stx-map 305 (lambda (τs_expected) 306 (string-join (stx-map type->str τs_expected) ", ")) 307 τs_expecteds) 308 "\n ") 309 (string-join (stx-map type->str τs_given) ", ") 310 (string-join (map ~s (stx-map syntax->datum expressions)) ", ")))]) 311 -------- 312 [⊢ [_ ≫ (ro:#%app e_fn/progsrc- e_arg- ...) ⇒ : τ_out]]] 313 [(_ e_fn e_arg ...) ≫ 314 [⊢ [e_fn ≫ e_fn- ⇒ : (~CU* τ_f ...)]] 315 #:with e_fn/progsrc- (replace-stx-loc #'e_fn- #'e_fn) 316 [⊢ [e_arg ≫ e_arg- ⇒ : τ_arg] ...] 317 #:with (f a ...) (generate-temporaries #'(e_fn e_arg ...)) 318 [([f ≫ _ : τ_f] [a ≫ _ : τ_arg] ...) 319 ⊢ [(app f a ...) ≫ _ ⇒ : τ_out]] 320 ... 321 -------- 322 [⊢ [_ ≫ (ro:#%app e_fn/progsrc- e_arg- ...) ⇒ : (CU τ_out ...)]]] 323 [(_ e_fn e_arg ...) ≫ 324 [⊢ [e_fn ≫ e_fn- ⇒ : (~U* τ_f ...)]] 325 #:with e_fn/progsrc- (replace-stx-loc #'e_fn- #'e_fn) 326 [⊢ [e_arg ≫ e_arg- ⇒ : τ_arg] ...] 327 #:with (f a ...) (generate-temporaries #'(e_fn e_arg ...)) 328 [([f ≫ _ : τ_f] [a ≫ _ : τ_arg] ...) 329 ⊢ [(app f a ...) ≫ _ ⇒ : τ_out]] 330 ... 331 -------- 332 [⊢ [_ ≫ (ro:#%app e_fn/progsrc- e_arg- ...) ⇒ : (U τ_out ...)]]]) 333 334 ;; --------------------------------- 335 ;; if 336 337 (define-typed-syntax if 338 [(_ e_tst e1 e2) ≫ 339 [⊢ [e_tst ≫ e_tst- ⇒ : ty_tst]] 340 #:when (concrete? #'ty_tst) 341 [⊢ [e1 ≫ e1- ⇒ : ty1]] 342 [⊢ [e2 ≫ e2- ⇒ : ty2]] 343 #:when (and (concrete? #'ty1) (concrete? #'ty2)) 344 -------- 345 [⊢ [_ ≫ (ro:if e_tst- e1- e2-) ⇒ : (CU ty1 ty2)]]] 346 [(_ e_tst e1 e2) ≫ 347 [⊢ [e_tst ≫ e_tst- ⇒ : _]] 348 [⊢ [e1 ≫ e1- ⇒ : ty1]] 349 [⊢ [e2 ≫ e2- ⇒ : ty2]] 350 -------- 351 [⊢ [_ ≫ (ro:if e_tst- e1- e2-) ⇒ : (U ty1 ty2)]]]) 352 353 ;; --------------------------------- 354 ;; let, etc (copied from ext-stlc.rkt) 355 356 (define-typed-syntax let 357 [(let ([x e] ...) e_body ...) ⇐ : τ_expected ≫ 358 [⊢ [e ≫ e- ⇒ : τ_x] ...] 359 [() ([x ≫ x- : τ_x] ...) ⊢ [(begin e_body ...) ≫ e_body- ⇐ : τ_expected]] 360 -------- 361 [⊢ [_ ≫ (ro:let ([x- e-] ...) e_body-) ⇐ : _]]] 362 [(let ([x e] ...) e_body ...) ≫ 363 [⊢ [e ≫ e- ⇒ : τ_x] ...] 364 [() ([x ≫ x- : τ_x] ...) ⊢ [(begin e_body ...) ≫ e_body- ⇒ : τ_body]] 365 -------- 366 [⊢ [_ ≫ (ro:let ([x- e-] ...) e_body-) ⇒ : τ_body]]]) 367 368 ; dont need to manually transfer expected type 369 ; result template automatically propagates properties 370 ; - only need to transfer expected type when local expanding an expression 371 ; - see let/tc 372 (define-typed-syntax let* 373 [(let* () e_body ...) ≫ 374 -------- 375 [_ ≻ (begin e_body ...)]] 376 [(let* ([x e] [x_rst e_rst] ...) e_body ...) ≫ 377 -------- 378 [_ ≻ (let ([x e]) (let* ([x_rst e_rst] ...) e_body ...))]]) 379 380 ;; -------------------- 381 ;; begin 382 383 (define-typed-syntax begin 384 [(begin e_unit ... e) ⇐ : τ_expected ≫ 385 [⊢ [e_unit ≫ e_unit- ⇒ : _] ...] 386 [⊢ [e ≫ e- ⇐ : τ_expected]] 387 -------- 388 [⊢ [_ ≫ (ro:begin e_unit- ... e-) ⇐ : _]]] 389 [(begin e_unit ... e) ≫ 390 [⊢ [e_unit ≫ e_unit- ⇒ : _] ...] 391 [⊢ [e ≫ e- ⇒ : τ_e]] 392 -------- 393 [⊢ [_ ≫ (ro:begin e_unit- ... e-) ⇒ : τ_e]]]) 394 395 ;; --------------------------------- 396 ;; set! 397 398 (define-typed-syntax set! 399 [(set! x:id e) ≫ 400 [⊢ [x ≫ x- ⇒ : ty_x]] 401 [⊢ [e ≫ e- ⇐ : ty_x]] 402 -------- 403 [⊢ [_ ≫ (ro:set! x- e-) ⇒ : CUnit]]]) 404 405 ;; --------------------------------- 406 ;; vector 407 408 (define-typed-syntax vector 409 [(_ e ...) ≫ 410 [⊢ [e ≫ e- ⇒ : τ] ...] 411 -------- 412 [⊢ [_ ≫ (ro:vector e- ...) ⇒ : #,(if (stx-andmap concrete? #'(τ ...)) 413 #'(CMVectorof (CU τ ...)) 414 #'(CMVectorof (U τ ...)))]]]) 415 (define-typed-syntax vector-immutable 416 [(_ e ...) ≫ 417 [⊢ [e ≫ e- ⇒ : τ] ...] 418 -------- 419 [⊢ [_ ≫ (ro:vector-immutable e- ...) ⇒ : (if (stx-andmap concrete? #'(τ ...)) 420 #'(CIVectorof (CU τ ...)) 421 #'(CIVectorof (U τ ...)))]]]) 422 ;; --------------------------------- 423 ;; IO and other built-in ops 424 425 (provide (rosette-typed-out [printf : (Ccase-> (C→ CString CUnit) 426 (C→ CString Any CUnit) 427 (C→ CString Any Any CUnit))] 428 [error : (C→ (CU CString CSymbol) Nothing)] 429 [void : (C→ CUnit)] 430 431 [equal? : (C→ Any Any Bool)] 432 [eq? : (C→ Any Any Bool)] 433 434 [pi : CNum] 435 436 [add1 : (Ccase-> (C→ CNegInt (CU CNegInt CZero)) 437 (C→ NegInt (U NegInt Zero)) 438 (C→ CZero CPosInt) 439 (C→ Zero PosInt) 440 (C→ CPosInt CPosInt) 441 (C→ PosInt PosInt) 442 (C→ CNat CPosInt) 443 (C→ Nat PosInt) 444 (C→ CInt CInt) 445 (C→ Int Int))] 446 [sub1 : (Ccase-> (C→ CNegInt CNegInt) 447 (C→ NegInt NegInt) 448 (C→ CZero CNegInt) 449 (C→ Zero NegInt) 450 (C→ CPosInt CNat) 451 (C→ PosInt Nat) 452 (C→ CNat CInt) 453 (C→ Nat Int) 454 (C→ CInt CInt) 455 (C→ Int Int))] 456 [+ : (Ccase-> (C→ CNat CNat CNat) 457 (C→ CNat CNat CNat CNat) 458 (C→ CNat CNat CNat CNat CNat) 459 (C→ Nat Nat Nat) 460 (C→ Nat Nat Nat Nat) 461 (C→ Nat Nat Nat Nat Nat) 462 (C→ CInt CInt CInt) 463 (C→ CInt CInt CInt CInt) 464 (C→ CInt CInt CInt CInt CInt) 465 (C→ Int Int Int) 466 (C→ Int Int Int Int) 467 (C→ Int Int Int Int Int) 468 (C→ CNum CNum CNum) 469 (C→ CNum CNum CNum CNum) 470 (C→ CNum CNum CNum CNum CNum) 471 (C→ Num Num Num) 472 (C→ Num Num Num Num) 473 (C→ Num Num Num Num Num))] 474 [* : (Ccase-> (C→ CNat CNat CNat) 475 (C→ CNat CNat CNat CNat) 476 (C→ CNat CNat CNat CNat CNat) 477 (C→ Nat Nat Nat) 478 (C→ Nat Nat Nat Nat) 479 (C→ Nat Nat Nat Nat Nat) 480 (C→ CInt CInt CInt) 481 (C→ CInt CInt CInt CInt) 482 (C→ CInt CInt CInt CInt CInt) 483 (C→ Int Int Int) 484 (C→ Int Int Int Int) 485 (C→ Int Int Int Int Int) 486 (C→ CNum CNum CNum) 487 (C→ CNum CNum CNum CNum) 488 (C→ CNum CNum CNum CNum CNum) 489 (C→ Num Num Num) 490 (C→ Num Num Num Num) 491 (C→ Num Num Num Num Num))] 492 [= : (Ccase-> (C→ CNum CNum CBool) 493 (C→ Num Num Bool))] 494 [< : (Ccase-> (C→ CNum CNum CBool) 495 (C→ Num Num Bool))] 496 [> : (Ccase-> (C→ CNum CNum CBool) 497 (C→ Num Num Bool))] 498 [<= : (Ccase-> (C→ CNum CNum CBool) 499 (C→ Num Num Bool))] 500 [>= : (Ccase-> (C→ CNum CNum CBool) 501 (C→ Num Num Bool))] 502 503 [abs : (Ccase-> (C→ CPosInt CPosInt) 504 (C→ PosInt PosInt) 505 (C→ CZero CZero) 506 (C→ Zero Zero) 507 (C→ CNegInt CPosInt) 508 (C→ NegInt PosInt) 509 (C→ CInt CInt) 510 (C→ Int Int) 511 (C→ CNum CNum) 512 (C→ Num Num))] 513 514 [not : (C→ Any Bool)] 515 [false? : (C→ Any Bool)] 516 517 ;; TODO: fix types of these predicates 518 [boolean? : (C→ Any Bool)] 519 [integer? : (C→ Any Bool)] 520 [real? : (C→ Any Bool)] 521 [positive? : (Ccase-> (C→ CNum CBool) 522 (C→ Num Bool))] 523 524 ;; rosette-specific 525 [asserts : (C→ (CListof Bool))] 526 [clear-asserts! : (C→ CUnit)])) 527 528 ;; --------------------------------- 529 ;; BV Types and Operations 530 531 ;; this must be a macro in order to support Racket's overloaded set/get 532 ;; parameter patterns 533 (define-typed-syntax current-bitwidth 534 [_:id ≫ 535 -------- 536 [⊢ [_ ≫ ro:current-bitwidth ⇒ : (CParamof (CU CFalse CPosInt))]]] 537 [(_) ≫ 538 -------- 539 [⊢ [_ ≫ (ro:current-bitwidth) ⇒ : (CU CFalse CPosInt)]]] 540 [(_ e) ≫ 541 [⊢ [e ≫ e- ⇐ : (CU CFalse CPosInt)]] 542 -------- 543 [⊢ [_ ≫ (ro:current-bitwidth e-) ⇒ : CUnit]]]) 544 545 (define-named-type-alias BV (add-predm (U CBV) ro:bv?)) 546 (define-symbolic-named-type-alias BVPred (C→ BV Bool) #:pred lifted-bitvector?) 547 548 (provide (rosette-typed-out [bv : (Ccase-> (C→ CInt CBVPred CBV) 549 (C→ CInt CPosInt CBV))] 550 [bv? : (C→ Any Bool)] 551 [bitvector : (C→ CPosInt CBVPred)] 552 [bitvector? : (C→ Any Bool)] 553 554 [bveq : (C→ BV BV Bool)] 555 [bvslt : (C→ BV BV Bool)] 556 [bvult : (C→ BV BV Bool)] 557 [bvsle : (C→ BV BV Bool)] 558 [bvule : (C→ BV BV Bool)] 559 [bvsgt : (C→ BV BV Bool)] 560 [bvugt : (C→ BV BV Bool)] 561 [bvsge : (C→ BV BV Bool)] 562 [bvuge : (C→ BV BV Bool)] 563 564 [bvnot : (C→ BV BV)] 565 566 [bvand : (C→ BV BV BV)] 567 [bvor : (C→ BV BV BV)] 568 [bvxor : (C→ BV BV BV)] 569 570 [bvshl : (C→ BV BV BV)] 571 [bvlshr : (C→ BV BV BV)] 572 [bvashr : (C→ BV BV BV)] 573 [bvneg : (C→ BV BV)] 574 575 [bvadd : (C→ BV BV BV)] 576 [bvsub : (C→ BV BV BV)] 577 [bvmul : (C→ BV BV BV)] 578 579 [bvsdiv : (C→ BV BV BV)] 580 [bvudiv : (C→ BV BV BV)] 581 [bvsrem : (C→ BV BV BV)] 582 [bvurem : (C→ BV BV BV)] 583 [bvsmod : (C→ BV BV BV)] 584 585 [concat : (C→ BV BV BV)] 586 [extract : (C→ Int Int BV BV)] 587 [sign-extend : (C→ BV CBVPred BV)] 588 [zero-extend : (C→ BV BVPred BV)] 589 590 [bitvector->integer : (C→ BV Int)] 591 [bitvector->natural : (C→ BV Nat)] 592 [integer->bitvector : (C→ Int BVPred BV)] 593 594 [bitvector-size : (C→ CBVPred CPosInt)] 595 596 597 ;; --------------------------------- 598 ;; Logic operators 599 600 [! : (C→ Bool Bool)] 601 [<=> : (C→ Bool Bool Bool)])) 602 603 (define-typed-syntax && 604 [(_ e ...) ≫ 605 [⊢ [e ≫ e- ⇐ : Bool] ...] 606 -------- 607 [⊢ [_ ≫ (ro:&& e- ...) ⇒ : Bool]]]) 608 (define-typed-syntax || 609 [(_ e ...) ≫ 610 [⊢ [e ≫ e- ⇐ : Bool] ...] 611 -------- 612 [⊢ [_ ≫ (ro:|| e- ...) ⇒ : Bool]]]) 613 614 ;; --------------------------------- 615 ;; solver forms 616 617 (define-base-types CSolution CPict) 618 619 (provide (rosette-typed-out [core : (C→ Any Any)] 620 [sat? : (C→ Any Bool)] 621 [unsat? : (C→ Any Bool)] 622 [unsat : (Ccase-> (C→ CSolution) 623 (C→ (CListof Bool) CSolution))] 624 [forall : (C→ (CListof Any) Bool Bool)] 625 [exists : (C→ (CListof Any) Bool Bool)])) 626 627 (define-typed-syntax verify 628 [(_ e) ≫ 629 [⊢ [e ≫ e- ⇒ : _]] 630 -------- 631 [⊢ [_ ≫ (ro:verify e-) ⇒ : CSolution]]] 632 [(_ #:assume ae #:guarantee ge) ≫ 633 [⊢ [ae ≫ ae- ⇒ : _]] 634 [⊢ [ge ≫ ge- ⇒ : _]] 635 -------- 636 [⊢ [_ ≫ (ro:verify #:assume ae- #:guarantee ge-) ⇒ : CSolution]]]) 637 638 (define-typed-syntax evaluate 639 [(_ v s) ≫ 640 [⊢ [v ≫ v- ⇒ : ty]] 641 [⊢ [s ≫ s- ⇐ : CSolution]] 642 -------- 643 [⊢ [_ ≫ (ro:evaluate v- s-) ⇒ : ty]]]) 644 645 646 (define-typed-syntax synthesize 647 [(_ #:forall ie #:guarantee ge) ≫ 648 [⊢ [ie ≫ ie- ⇐ : (CListof Any)]] 649 [⊢ [ge ≫ ge- ⇒ : _]] 650 -------- 651 [⊢ [_ ≫ (ro:synthesize #:forall ie- #:guarantee ge-) ⇒ : CSolution]]] 652 [(_ #:forall ie #:assume ae #:guarantee ge) ≫ 653 [⊢ [ie ≫ ie- ⇐ : (CListof Any)]] 654 [⊢ [ae ≫ ae- ⇒ : _]] 655 [⊢ [ge ≫ ge- ⇒ : _]] 656 -------- 657 [⊢ [_ ≫ (ro:synthesize #:forall ie- #:assume ae- #:guarantee ge-) ⇒ : CSolution]]]) 658 659 (define-typed-syntax solve 660 [(_ e) ≫ 661 [⊢ [e ≫ e- ⇒ : _]] 662 -------- 663 [⊢ [_ ≫ (ro:solve e-) ⇒ : CSolution]]]) 664 665 ;; --------------------------------- 666 ;; Subtyping 667 668 (begin-for-syntax 669 (define (sub? t1 t2) 670 ; need this because recursive calls made with unexpanded types 671 ;; (define τ1 ((current-type-eval) t1)) 672 ;; (define τ2 ((current-type-eval) t2)) 673 ;; (printf "t1 = ~a\n" (syntax->datum t1)) 674 ;; (printf "t2 = ~a\n" (syntax->datum t2)) 675 (or 676 (Any? t2) 677 ((current-type=?) t1 t2) 678 (syntax-parse (list t1 t2) 679 [((~CListof ty1) (~CListof ty2)) 680 ((current-sub?) #'ty1 #'ty2)] 681 ;; vectors, only immutable vectors are invariant 682 [((~CIVectorof . tys1) (~CIVectorof . tys2)) 683 (stx-andmap (current-sub?) #'tys1 #'tys2)] 684 ; 2 U types, subtype = subset 685 [((~CU* . ts1) _) 686 (for/and ([t (stx->list #'ts1)]) 687 ((current-sub?) t t2))] 688 [((~U* . ts1) _) 689 (and 690 (not (concrete? t2)) 691 (for/and ([t (stx->list #'ts1)]) 692 ((current-sub?) t t2)))] 693 ; 1 U type, 1 non-U type. subtype = member 694 [(_ (~CU* . ts2)) 695 #:when (not (or (U*? t1) (CU*? t1))) 696 (for/or ([t (stx->list #'ts2)]) 697 ((current-sub?) t1 t))] 698 [(_ (~U* . ts2)) 699 #:when (not (or (U*? t1) (CU*? t1))) 700 (for/or ([t (stx->list #'ts2)]) 701 ((current-sub?) t1 t))] 702 ; 2 case-> types, subtype = subset 703 [(_ (~Ccase-> . ts2)) 704 (for/and ([t (stx->list #'ts2)]) 705 ((current-sub?) t1 t))] 706 ; 1 case-> , 1 non-case-> 707 [((~Ccase-> . ts1) _) 708 (for/or ([t (stx->list #'ts1)]) 709 ((current-sub?) t t2))] 710 [((~C→ s1 ... s2) (~C→ t1 ... t2)) 711 (and (subs? #'(t1 ...) #'(s1 ...)) 712 ((current-sub?) #'s2 #'t2))] 713 [_ #f]))) 714 (current-sub? sub?) 715 (current-typecheck-relation sub?) 716 (define (subs? τs1 τs2) 717 (and (stx-length=? τs1 τs2) 718 (stx-andmap (current-sub?) τs1 τs2))))