rosette.rkt (10940B)
1 #lang turnstile 2 (extends "../stlc+union+case.rkt" 3 #:except define if #%app #%module-begin add1 sub1 +) 4 (reuse List list #:from "../stlc+cons.rkt") 5 (require (prefix-in ro: rosette)) 6 (require (prefix-in ro: rosette/lib/synthax)) 7 (provide (rename-out [ro:#%module-begin #%module-begin]) 8 Symbol Regexp Param Stx BV BVPred) 9 10 ;; providing version of define-typed-syntax 11 (define-syntax (define-typed-syntax stx) 12 (syntax-parse stx 13 [(_ name:id #:export-as out-name:id . rst) 14 #'(begin- 15 (provide- (rename-out [name out-name])) 16 (define-typerule name . rst))] ; define-typerule doesnt provide 17 [(_ name:id . rst) 18 #'(define-typed-syntax name #:export-as name . rst)] 19 [(_ (name:id . pat) . rst) 20 #'(define-typed-syntax name #:export-as name [(_ . pat) . rst])])) 21 22 (define-for-syntax (mk-ro:-id id) (format-id id "ro:~a" id)) 23 24 (define-syntax rosette-typed-out 25 (make-provide-pre-transformer 26 (lambda (stx modes) 27 (syntax-parse stx #:datum-literals (:) 28 ;; cannot write ty:type bc provides might precede type def 29 [(_ (~and (~or (~and [out-x:id (~optional :) ty] (~parse x #'out-x)) 30 [[x:id (~optional :) ty] out-x:id])) ...) 31 #:with (ro-x ...) (stx-map mk-ro:-id #'(x ...)) 32 (pre-expand-export (syntax/loc stx (typed-out [[ro-x ty] out-x] ...)) 33 modes)])))) 34 35 ;; ---------------------------------------------------------------------------- 36 ;; Rosette stuff 37 38 (define-typed-syntax define-symbolic 39 [(_ x:id ...+ pred : ty:type) ≫ 40 [⊢ [pred ≫ pred- ⇐ : (→ ty.norm Bool)]] 41 #:with (y ...) (generate-temporaries #'(x ...)) 42 -------- 43 [_ ≻ (begin- 44 (define-syntax- x (make-rename-transformer (⊢ y : ty.norm))) ... 45 (ro:define-symbolic y ... pred-))]]) 46 47 (define-typed-syntax choose 48 [(ch e ...+) ≫ 49 [⊢ [e ≫ e- ⇒ : ty]] ... 50 -------- 51 ;; the #'choose identifier itself must have the location of its use 52 ;; see define-synthax implementation, specifically syntax/source in utils 53 [⊢ [_ ≫ (#,(syntax/loc #'ch ro:choose) e- ...) ⇒ : (⊔ ty ...)]]]) 54 55 (define-typed-syntax app #:export-as #%app 56 [(_ e_fn e_arg ...) ≫ 57 [⊢ [e_fn ≫ e_fn- ⇒ : (~→ ~! τ_in ... τ_out)]] 58 #:fail-unless (stx-length=? #'[τ_in ...] #'[e_arg ...]) 59 (num-args-fail-msg #'e_fn #'[τ_in ...] #'[e_arg ...]) 60 [⊢ [e_arg ≫ e_arg- ⇐ : τ_in] ...] 61 -------- 62 [⊢ [_ ≫ (ro:#%app e_fn- e_arg- ...) ⇒ : τ_out]]] 63 [(_ e_fn e_arg ...) ≫ 64 [⊢ [e_fn ≫ e_fn- ⇒ : (~case-> ~! . (~and ty_fns ((~→ . _) ...)))]] 65 [⊢ [e_arg ≫ e_arg- ⇒ : τ_arg] ...] 66 #:with τ_out 67 (for/first ([ty_f (stx->list #'ty_fns)] 68 #:when (syntax-parse ty_f 69 [(~→ τ_in ... τ_out) 70 (and (stx-length=? #'(τ_in ...) #'(e_arg ...)) 71 (typechecks? #'(τ_arg ...) #'(τ_in ...)))])) 72 (syntax-parse ty_f [(~→ _ ... t_out) #'t_out])) 73 #:fail-unless (syntax-e #'τ_out) 74 ; use (failing) typechecks? to get err msg 75 (syntax-parse #'ty_fns 76 [((~→ τ_in ... _) ...) 77 (let* ([τs_expecteds #'((τ_in ...) ...)] 78 [τs_given #'(τ_arg ...)] 79 [expressions #'(e_arg ...)]) 80 (format (string-append "type mismatch\n" 81 " expected one of:\n" 82 " ~a\n" 83 " given: ~a\n" 84 " expressions: ~a") 85 (string-join 86 (stx-map 87 (lambda (τs_expected) 88 (string-join (stx-map type->str τs_expected) ", ")) 89 τs_expecteds) 90 "\n ") 91 (string-join (stx-map type->str τs_given) ", ") 92 (string-join (map ~s (stx-map syntax->datum expressions)) ", ")))]) 93 -------- 94 [⊢ [_ ≫ (ro:#%app e_fn- e_arg- ...) ⇒ : τ_out]]]) 95 96 ;; ---------------------------------------------------------------------------- 97 ;; Racket stuff 98 99 (define-base-types Symbol Regexp) 100 101 (define-typed-syntax quote 102 [(_ x:id) ≫ 103 -------- 104 [⊢ [_ ≫ (quote- x) ⇒ : Symbol]]] 105 [(_ (x:id ...)) ≫ 106 -------- 107 [⊢ [_ ≫ (quote- (x ...)) ⇒ : (stlc+cons:List Symbol)]]]) 108 109 (define-type-constructor Param #:arity = 1) 110 111 (provide (rosette-typed-out [boolean? : (→ Bool Bool)] 112 [integer? : (→ Int Bool)] 113 [string? : (→ String Bool)] 114 [pregexp : (→ String Regexp)] 115 116 [add1 : (case-> (→ NegInt (U NegInt Zero)) 117 (→ Zero PosInt) 118 (→ PosInt PosInt) 119 (→ Nat PosInt) 120 (→ Int Int))] 121 [sub1 : (case-> (→ NegInt NegInt) 122 (→ Zero NegInt) 123 (→ PosInt Nat) 124 (→ Nat Int) 125 (→ Int Int))] 126 [+ : (case-> (→ Nat Nat Nat) 127 (→ Int Int Int) 128 (→ Num Num Num))])) 129 130 (define-typed-syntax equal? 131 [(equal? e1 e2) ≫ 132 [⊢ [e1 ≫ e1- ⇒ : ty1]] 133 [⊢ [e2 ≫ e2- ⇐ : ty1]] 134 -------- 135 [⊢ [_ ≫ (ro:equal? e1- e2-) ⇒ : Bool]]]) 136 137 (define-typed-syntax if 138 [(if e_tst e1 e2) ⇐ : τ-expected ≫ 139 [⊢ [e_tst ≫ e_tst- ⇒ : _]] ; Any non-false value is truthy. 140 [⊢ [e1 ≫ e1- ⇐ : τ-expected]] 141 [⊢ [e2 ≫ e2- ⇐ : τ-expected]] 142 -------- 143 [⊢ [_ ≫ (ro:if e_tst- e1- e2-) ⇐ : _]]] 144 [(if e_tst e1 e2) ≫ 145 [⊢ [e_tst ≫ e_tst- ⇒ : _]] ; Any non-false value is truthy. 146 [⊢ [e1 ≫ e1- ⇒ : τ1]] 147 [⊢ [e2 ≫ e2- ⇒ : τ2]] 148 -------- 149 [⊢ [_ ≫ (ro:if e_tst- e1- e2-) ⇒ : (⊔ τ1 τ2)]]]) 150 151 ;; TODO: fix this to support Racket parameter usage patterns? 152 ;; eg, this wont work if applied since it's not a function type 153 (define-typed-syntax make-parameter 154 #;[(_ e) ⇐ : (~Param τ_expected) ≫ 155 [⊢ [e ≫ e- ⇐ : τ_expected]] 156 -------- 157 [⊢ [_ ≫ (ro:make-parameter e-)]]] 158 [(_ e) ≫ 159 [⊢ [e ≫ e- ⇒ : τ]] 160 -------- 161 [⊢ [_ ≫ (ro:make-parameter e-) ⇒ : (Param τ)]]]) 162 163 (define-typed-syntax define #:datum-literals (: -> →) 164 [(_ x:id e) ≫ 165 -------- 166 [_ ≻ (stlc+union+case:define x e)]] 167 [(_ (f [x : ty] ... (~or → ->) ty_out) e) ≫ 168 ; [⊢ [e ≫ e- ⇒ : ty_e]] 169 #:with f- (generate-temporary #'f) 170 -------- 171 [_ ≻ (begin- 172 (define-syntax- f 173 (make-rename-transformer (⊢ f- : (→ ty ... ty_out)))) 174 (stlc+union+case:define f- 175 (stlc+union+case:λ ([x : ty] ...) e)))]]) 176 177 (define-base-type Stx) 178 179 ;; ---------------------------------------------------------------------------- 180 ;; BV stuff 181 182 ;; TODO: make BV parametric in a dependent n? 183 (define-base-type BV) ; represents actual bitvectors 184 185 ; a predicate recognizing bv's of a certain size 186 (define-named-type-alias BVPred (→ BV Bool)) 187 188 ;; support higher order case with case-> types 189 (provide (rosette-typed-out [bv : (case-> (→ Int BVPred BV) 190 (→ Int PosInt BV))] 191 [bv? : (→ BV Bool)] 192 [bitvector : (→ PosInt BVPred)] 193 [bitvector? : (→ BVPred Bool)] 194 [[bitvector : (→ PosInt BVPred)] bvpred] 195 [[bitvector? : (→ BVPred Bool)] bvpred?] 196 [bitvector-size : (→ BVPred PosInt)] 197 [[bitvector-size : (→ BVPred PosInt)] bvpred-size] 198 [bveq : (→ BV BV Bool)] 199 [bvslt : (→ BV BV Bool)] 200 [bvult : (→ BV BV Bool)] 201 [bvsle : (→ BV BV Bool)] 202 [bvule : (→ BV BV Bool)] 203 [bvsgt : (→ BV BV Bool)] 204 [bvugt : (→ BV BV Bool)] 205 [bvsge : (→ BV BV Bool)] 206 [bvuge : (→ BV BV Bool)] 207 [bvnot : (→ BV BV)])) 208 209 (define-typed-syntax bvand 210 [f:id ≫ ; TODO: implement variable arity types 211 -------- 212 [⊢ [_ ≫ ro:bvand ⇒ : (→ BV BV BV)]]] 213 [(_ e ...+) ≫ 214 [⊢ [e ≫ e- ⇐ : BV] ...] 215 -------- 216 [⊢ [_ ≫ (ro:bvand e- ...) ⇒ : BV]]]) 217 (define-typed-syntax bvor 218 [f:id ≫ ; TODO: implement variable arity types 219 -------- 220 [⊢ [_ ≫ ro:bvor ⇒ : (→ BV BV BV)]]] 221 [(_ e ...+) ≫ 222 [⊢ [e ≫ e- ⇐ : BV] ...] 223 -------- 224 [⊢ [_ ≫ (ro:bvor e- ...) ⇒ : BV]]]) 225 (define-typed-syntax bvxor 226 [f:id ≫ ; TODO: implement variable arity types 227 -------- 228 [⊢ [_ ≫ ro:bvxor ⇒ : (→ BV BV BV)]]] 229 [(_ e ...+) ≫ 230 [⊢ [e ≫ e- ⇐ : BV] ...] 231 -------- 232 [⊢ [_ ≫ (ro:bvxor e- ...) ⇒ : BV]]]) 233 234 (provide (rosette-typed-out [bvshl : (→ BV BV BV)] 235 [bvlshr : (→ BV BV BV)] 236 [bvashr : (→ BV BV BV)] 237 [bvneg : (→ BV BV)])) 238 239 (define-typed-syntax bvadd 240 [f:id ≫ ; TODO: implement variable arity types 241 -------- 242 [⊢ [_ ≫ ro:bvadd ⇒ : (→ BV BV BV)]]] 243 [(_ e ...+) ≫ 244 [⊢ [e ≫ e- ⇐ : BV] ...] 245 -------- 246 [⊢ [_ ≫ (ro:bvadd e- ...) ⇒ : BV]]]) 247 (define-typed-syntax bvsub 248 [f:id ≫ ; TODO: implement variable arity types 249 -------- 250 [⊢ [_ ≫ ro:bvsub ⇒ : (→ BV BV BV)]]] 251 [(_ e ...+) ≫ 252 [⊢ [e ≫ e- ⇐ : BV] ...] 253 -------- 254 [⊢ [_ ≫ (ro:bvsub e- ...) ⇒ : BV]]]) 255 (define-typed-syntax bvmul 256 [f:id ≫ ; TODO: implement variable arity types 257 -------- 258 [⊢ [_ ≫ ro:bvmul ⇒ : (→ BV BV BV)]]] 259 [(_ e ...+) ≫ 260 [⊢ [e ≫ e- ⇐ : BV] ...] 261 -------- 262 [⊢ [_ ≫ (ro:bvmul e- ...) ⇒ : BV]]]) 263 264 (provide (rosette-typed-out [bvsdiv : (→ BV BV BV)] 265 [bvudiv : (→ BV BV BV)] 266 [bvsrem : (→ BV BV BV)] 267 [bvurem : (→ BV BV BV)] 268 [bvsmod : (→ BV BV BV)])) 269 270 (define-typed-syntax concat 271 [(_ e ...+) ≫ 272 [⊢ [e ≫ e- ⇐ : BV] ...] 273 -------- 274 [⊢ [_ ≫ (ro:concat e- ...) ⇒ : BV]]]) 275 276 (provide (rosette-typed-out [extract : (→ Int Int BV BV)] 277 ;; TODO: support union in 2nd arg 278 [sign-extend : (→ BV BVPred BV)] 279 [zero-extend : (→ BV BVPred BV)] 280 [bitvector->integer : (→ BV Int)] 281 [bitvector->natural : (→ BV Int)] 282 [integer->bitvector : (→ Int BVPred BV)]))