From 297e5df6ae1e76d060b9be70118ad248714ea2ca Mon Sep 17 00:00:00 2001 From: Stephen Chang Date: Mon, 31 Oct 2016 13:56:24 -0400 Subject: [PATCH] start host lang param experiment --- macrotypes/typecheck.rkt | 5 +- turnstile/examples/rosette/bv3.rkt | 97 + turnstile/examples/rosette/lib/angelic3.rkt | 14 + turnstile/examples/rosette/lib/lift3.rkt | 23 + turnstile/examples/rosette/lib/render3.rkt | 17 + turnstile/examples/rosette/lib/synthax3.rkt | 80 + turnstile/examples/rosette/query/debug3.rkt | 39 + turnstile/examples/rosette/rosette3.rkt | 1789 +++++++++++++++++ .../tests/rosette/rosette3/bv-ref-tests.rkt | 404 ++++ .../tests/rosette/rosette3/bv-tests.rkt | 30 + .../rosette/rosette3/check-type+asserts.rkt | 17 + .../tests/rosette/rosette3/fsm-test.rkt | 43 + .../tests/rosette/rosette3/ifc-tests.rkt | 92 + .../rosette3/rosette-guide-sec2-tests.rkt | 251 +++ .../rosette3/rosette-guide-sec3-tests.rkt | 120 ++ .../rosette3/rosette-guide-sec4-tests.rkt | 259 +++ .../rosette3/rosette-guide-sec43-tests.rkt | 190 ++ .../rosette3/rosette-guide-sec44-tests.rkt | 114 ++ .../rosette3/rosette-guide-sec45-tests.rkt | 21 + .../rosette3/rosette-guide-sec46-tests.rkt | 95 + .../rosette3/rosette-guide-sec49-tests.rkt | 32 + .../rosette3/rosette-guide-sec5-tests.rkt | 59 + .../rosette3/rosette-guide-sec6-tests.rkt | 52 + .../rosette3/rosette-guide-sec7-tests.rkt | 230 +++ .../tests/rosette/rosette3/rosette3-tests.rkt | 345 ++++ .../rosette3/run-all-rosette-tests-script.rkt | 23 + 26 files changed, 4440 insertions(+), 1 deletion(-) create mode 100644 turnstile/examples/rosette/bv3.rkt create mode 100644 turnstile/examples/rosette/lib/angelic3.rkt create mode 100644 turnstile/examples/rosette/lib/lift3.rkt create mode 100644 turnstile/examples/rosette/lib/render3.rkt create mode 100644 turnstile/examples/rosette/lib/synthax3.rkt create mode 100644 turnstile/examples/rosette/query/debug3.rkt create mode 100644 turnstile/examples/rosette/rosette3.rkt create mode 100644 turnstile/examples/tests/rosette/rosette3/bv-ref-tests.rkt create mode 100644 turnstile/examples/tests/rosette/rosette3/bv-tests.rkt create mode 100644 turnstile/examples/tests/rosette/rosette3/check-type+asserts.rkt create mode 100644 turnstile/examples/tests/rosette/rosette3/fsm-test.rkt create mode 100644 turnstile/examples/tests/rosette/rosette3/ifc-tests.rkt create mode 100644 turnstile/examples/tests/rosette/rosette3/rosette-guide-sec2-tests.rkt create mode 100644 turnstile/examples/tests/rosette/rosette3/rosette-guide-sec3-tests.rkt create mode 100644 turnstile/examples/tests/rosette/rosette3/rosette-guide-sec4-tests.rkt create mode 100644 turnstile/examples/tests/rosette/rosette3/rosette-guide-sec43-tests.rkt create mode 100644 turnstile/examples/tests/rosette/rosette3/rosette-guide-sec44-tests.rkt create mode 100644 turnstile/examples/tests/rosette/rosette3/rosette-guide-sec45-tests.rkt create mode 100644 turnstile/examples/tests/rosette/rosette3/rosette-guide-sec46-tests.rkt create mode 100644 turnstile/examples/tests/rosette/rosette3/rosette-guide-sec49-tests.rkt create mode 100644 turnstile/examples/tests/rosette/rosette3/rosette-guide-sec5-tests.rkt create mode 100644 turnstile/examples/tests/rosette/rosette3/rosette-guide-sec6-tests.rkt create mode 100644 turnstile/examples/tests/rosette/rosette3/rosette-guide-sec7-tests.rkt create mode 100644 turnstile/examples/tests/rosette/rosette3/rosette3-tests.rkt create mode 100644 turnstile/examples/tests/rosette/rosette3/run-all-rosette-tests-script.rkt diff --git a/macrotypes/typecheck.rkt b/macrotypes/typecheck.rkt index 4ec3da2..a01ec03 100644 --- a/macrotypes/typecheck.rkt +++ b/macrotypes/typecheck.rkt @@ -76,7 +76,10 @@ ;; extract-filename : PathString -> String (define (extract-filename f) (path->string (path-replace-suffix (file-name-from-path f) ""))) - (define-syntax-parameter stx (syntax-rules ()))) + (define-syntax-parameter stx (syntax-rules ())) + + ;; parameter is an identifier transformer + (define current-host-lang (make-parameter mk--))) ;; non-Turnstile define-typed-syntax ;; TODO: potentially confusing? get rid of this? diff --git a/turnstile/examples/rosette/bv3.rkt b/turnstile/examples/rosette/bv3.rkt new file mode 100644 index 0000000..5d2c3de --- /dev/null +++ b/turnstile/examples/rosette/bv3.rkt @@ -0,0 +1,97 @@ +#lang turnstile +(extends "rosette3.rkt" ; extends typed rosette + #:except bv bveq bvslt bvult bvsle bvule bvsgt bvugt bvsge bvuge) +(require (prefix-in ro: rosette)) ; untyped +(require (only-in sdsl/bv/lang/bvops bvredand bvredor bv bv*) + (prefix-in bv: (only-in sdsl/bv/lang/bvops BV))) +(require sdsl/bv/lang/core (prefix-in bv: sdsl/bv/lang/form)) + +(provide Prog Lib + (typed-out [bv : (Ccase-> (C→ CInt CBV) + (C→ CInt CBVPred CBV) + (C→ CInt CPosInt CBV))] + [bv* : (Ccase-> (C→ BV) + (C→ CBVPred BV))] + [bvredor : (C→ BV BV)] + [bvredand : (C→ BV BV)]) + current-bvpred define-fragment bvlib thunk) + +;; this must be a macro in order to support Racket's overloaded set/get +;; parameter patterns +(define-typed-syntax current-bvpred + [c-bvpred:id ≫ + -------- + [⊢ [_ ≫ bv:BV ⇒ : (CParamof CBVPred)]]] + [(_) ≫ + -------- + [⊢ [_ ≫ (bv:BV) ⇒ : CBVPred]]] + [(_ e) ≫ + [⊢ [e ≫ e- ⇐ : CBVPred]] + -------- + [⊢ [_ ≫ (bv:BV e-) ⇒ : CUnit]]]) + +(define-syntax-rule (bv:bool->bv b) + (ro:if b + (bv (rosette3:#%datum . 1)) + (bv (rosette3:#%datum . 0)))) + +(define-simple-macro (define-comparators id ...) + #:with (op ...) (stx-map (lambda (o) (format-id o "ro:~a" o)) #'(id ...)) + #:with (id/tc ...) (generate-temporaries #'(id ...)) + (begin- + (define- (id x y) (bv:bool->bv (ro:#%app op x y))) ... + (provide (rename-out [id/tc id] ...)) + (define-primop id/tc id (C→ BV BV BV)) ...)) + +(define-comparators bveq bvslt bvult bvsle bvule bvsgt bvugt bvsge bvuge) + +(define-base-types Prog Lib) + +(define-typed-syntax define-fragment + [(_ (id param ...) #:implements spec #:library lib-expr) ≫ + -------- + [_ ≻ (define-fragment (id param ...) + #:implements spec #:library lib-expr #:minbv (rosette3:#%datum . 4))]] + [(_ (id param ...) #:implements spec #:library lib-expr #:minbv minbv) ≫ + [⊢ [spec ≫ spec- ⇒ : ty_spec]] + #:fail-unless (C→? #'ty_spec) "spec must be a function" + [⊢ [lib-expr ≫ lib-expr- ⇐ : Lib]] + [⊢ [minbv ≫ minbv- ⇐ : Int]] + #:with id-stx (format-id #'id "~a-stx" #'id #:source #'id) + -------- + [_ ≻ (begin- + (define-values- (id-internal id-stx-internal) + (bv:synthesize-fragment (id param ...) + #:implements spec- + #:library lib-expr- + #:minbv minbv-)) + (define-syntax id + (make-rename-transformer (⊢ id-internal : ty_spec))) + (define-syntax id-stx + (make-rename-transformer (⊢ id-stx-internal : CStx))) + )]]) + +(define-typed-syntax bvlib + [(_ [(~and ids (id ...)) n] ...) ≫ + #:fail-unless (stx-andmap brace? #'(ids ...)) + "given ops must be enclosed with braces" + [⊢ [n ≫ n- ⇐ : Int] ...] + [⊢ [id ≫ id- ⇒ : ty_id] ... ...] + #:fail-unless (stx-andmap (lambda (t) (or (C→? t) (Ccase->? t))) #'(ty_id ... ...)) + "given op must be a function" + ;; outer ~and wrapper is a syntax-parse workaround + #:with ((~and (~or (~C→ ty ...) + (~and (~Ccase-> (~C→ ty* ...) ...) + (~parse (ty ...) #'(ty* ... ...))))) ...) + #'(ty_id ... ...) + #:fail-unless (stx-andmap τ⊑BV? #'(ty ... ...)) + "given op must have BV inputs and output" + -------- + [⊢ [_ ≫ (bv:bvlib [{id- ...} n-] ...) ⇒ : Lib]]]) + +(begin-for-syntax + (define BV* ((current-type-eval) #'BV)) + (define (τ⊑BV? τ) + (typecheck? τ BV*))) + +(define-syntax-rule (thunk e) (rosette3:λ () e)) diff --git a/turnstile/examples/rosette/lib/angelic3.rkt b/turnstile/examples/rosette/lib/angelic3.rkt new file mode 100644 index 0000000..b552b69 --- /dev/null +++ b/turnstile/examples/rosette/lib/angelic3.rkt @@ -0,0 +1,14 @@ +#lang turnstile +(require + (prefix-in t/ro: (only-in "../rosette3.rkt" U)) + (prefix-in ro: rosette/lib/angelic)) +(provide choose*) + +(define-typed-syntax choose* + [(ch e ...+) ≫ + [⊢ [e ≫ e- ⇒ : ty]] ... + #:with (e/disarmed ...) (stx-map replace-stx-loc #'(e- ...) #'(e ...)) + -------- + ;; the #'choose* identifier itself must have the location of its use + ;; see define-synthax implementation, specifically syntax/source in utils + [⊢ [_ ≫ (#,(syntax/loc #'ch ro:choose*) e/disarmed ...) ⇒ : (t/ro:U ty ...)]]]) diff --git a/turnstile/examples/rosette/lib/lift3.rkt b/turnstile/examples/rosette/lib/lift3.rkt new file mode 100644 index 0000000..c2529b7 --- /dev/null +++ b/turnstile/examples/rosette/lib/lift3.rkt @@ -0,0 +1,23 @@ +#lang turnstile +(require + (prefix-in t/ro: (only-in "../rosette3.rkt" U ~C→ C→)) + (prefix-in ro: rosette/lib/lift)) +(provide define-lift) + +(define-typed-syntax define-lift + [(_ x:id [(pred? ...) racket-fn:id]) ≫ + [⊢ [pred? ≫ pred?- ⇒ : (t/ro:~C→ _ ...)]] ... + [⊢ [racket-fn ≫ racket-fn- ⇒ : (t/ro:~C→ ty1 ty2)]] + #:with y (generate-temporary #'x) + -------- + [_ ≻ (begin- + (define-syntax- x (make-rename-transformer (⊢ y : (t/ro:C→ (t/ro:U ty1) (t/ro:U ty2))))) + (ro:define-lift y [(pred?- ...) racket-fn-]))]] + [(_ x:id [pred? racket-fn:id]) ≫ + [⊢ [pred? ≫ pred?- ⇒ : (t/ro:~C→ _ ...)]] + [⊢ [racket-fn ≫ racket-fn- ⇒ : (t/ro:~C→ ty1 ty2)]] + #:with y (generate-temporary #'x) + -------- + [_ ≻ (begin- + (define-syntax- x (make-rename-transformer (⊢ y : (t/ro:C→ (t/ro:U ty1) (t/ro:U ty2))))) + (ro:define-lift y [pred?- racket-fn-]))]]) diff --git a/turnstile/examples/rosette/lib/render3.rkt b/turnstile/examples/rosette/lib/render3.rkt new file mode 100644 index 0000000..e0955f8 --- /dev/null +++ b/turnstile/examples/rosette/lib/render3.rkt @@ -0,0 +1,17 @@ +#lang turnstile +(require + (prefix-in t/ro: (only-in "../rosette3.rkt" CNat CSolution CPict)) + (prefix-in ro: rosette/lib/render)) +(provide render) + +(define-typed-syntax render + [(_ s) ≫ + [⊢ [s ≫ s- ⇐ : t/ro:CSolution]] + -------- + [⊢ [_ ≫ (ro:render s-) ⇒ : t/ro:CPict]]] + [(_ s sz) ≫ + [⊢ [s ≫ s- ⇐ : t/ro:CSolution]] + [⊢ [sz ≫ sz- ⇐ : t/ro:CNat]] + -------- + [⊢ [_ ≫ (ro:render s- sz-) ⇒ : t/ro:CPict]]]) + diff --git a/turnstile/examples/rosette/lib/synthax3.rkt b/turnstile/examples/rosette/lib/synthax3.rkt new file mode 100644 index 0000000..93c2d53 --- /dev/null +++ b/turnstile/examples/rosette/lib/synthax3.rkt @@ -0,0 +1,80 @@ +#lang turnstile +(require + (only-in "../rosette3.rkt" rosette-typed-out) + (prefix-in + t/ro: + (only-in "../rosette3.rkt" U Int Bool C→ CSolution Unit CSyntax CListof)) + (prefix-in ro: rosette/lib/synthax)) + +(provide (rosette-typed-out [print-forms : (t/ro:C→ t/ro:CSolution t/ro:Unit)]) + ??) + +(provide generate-forms choose) + +(define-typed-syntax ?? + [(qq) ≫ + #:with ??/progsrc (datum->syntax #'here 'ro:?? #'qq) + -------- + [⊢ [_ ≫ (??/progsrc) ⇒ : t/ro:Int]]] + [(qq pred?) ≫ + #:with ??/progsrc (datum->syntax #'here 'ro:?? #'qq) + [⊢ [pred? ≫ pred?- (⇒ : _) (⇒ typefor ty) (⇒ solvable? s?) (⇒ function? f?)]] + #:fail-unless (syntax-e #'s?) + (format "Expected a Rosette-solvable type, given ~a." + (syntax->datum #'pred?)) + #:fail-when (syntax-e #'f?) + (format "Expected a non-function Rosette type, given ~a." + (syntax->datum #'pred?)) + -------- + [⊢ [_ ≫ (??/progsrc pred?-) ⇒ : ty]]]) + +(define-syntax print-forms + (make-variable-like-transformer + (assign-type #'ro:print-forms #'(t/ro:C→ t/ro:CSolution t/ro:Unit)))) + +(define-syntax generate-forms + (make-variable-like-transformer + (assign-type #'ro:generate-forms #'(t/ro:C→ t/ro:CSolution (t/ro:CListof t/ro:CSyntax))))) + +(define-typed-syntax choose + [(ch e ...+) ≫ + [⊢ [e ≫ e- ⇒ : ty]] ... + #:with (e/disarmed ...) (stx-map replace-stx-loc #'(e- ...) #'(e ...)) + -------- + ;; the #'choose identifier itself must have the location of its use + ;; see define-synthax implementation, specifically syntax/source in utils + [⊢ [_ ≫ (#,(syntax/loc #'ch ro:choose) e/disarmed ...) ⇒ : (t/ro:U ty ...)]]]) + +;; TODO: not sure how to handle define-synthax +;; it defines a macro, but may refer to itself in #:base and #:else +;; - so must expand "be" and "ee", but what to do about self reference? +;; - the current letrec-like implementation results in an #%app of the the f macro +;; which isnt quite right +#;(define-typed-syntax define-synthax #:datum-literals (: -> →) + #;[(_ x:id ([pat e] ...+)) ≫ + [⊢ [e ≫ e- ⇒ : τ]] ... + #:with y (generate-temporary #'x) + -------- + [_ ≻ (begin- + (define-syntax- x (make-rename-transformer (⊢ y : t/ro:Int))) + (ro:define-synthax y ([pat e-] ...)))]] + [(_ (f [x:id : ty] ... [k:id : tyk] -> ty_out) #:base be #:else ee) ≫ + #:with (e ...) #'(be ee) + [() ([x ≫ x- : ty] ... [k ≫ k- : tyk] [f ≫ f- : (t/ro:C→ ty ... tyk ty_out)]) ⊢ + [e ≫ e- ⇒ : ty_e] ...] + #:with (be- ee-) #'(e- ...) + #:with f* (generate-temporary) + #:with app-f (format-id #'f "apply-~a" #'f) + -------- + [_ ≻ (begin- + (ro:define-synthax (f- x- ... k-) #:base be- #:else ee-) + (define-syntax- app-f + (syntax-parser + [(_ . es) + ;; TODO: typecheck es + #:with es- (stx-map expand/df #'es) +; #:with es/fixsrc (stx-map replace-stx-loc #'es- #'es) + (assign-type #'(f- . es) #'ty_out)])))]]) +; (⊢ f- : (t/ro:C→ ty ... tyk ty_out)) +; #;(ro:define-synthax (f- x- ... k-) +; #:base be- #:else ee-))]]) diff --git a/turnstile/examples/rosette/query/debug3.rkt b/turnstile/examples/rosette/query/debug3.rkt new file mode 100644 index 0000000..e6c86fc --- /dev/null +++ b/turnstile/examples/rosette/query/debug3.rkt @@ -0,0 +1,39 @@ +#lang turnstile +(require + (prefix-in t/ro: (only-in "../rosette3.rkt" + λ ann begin C→ Nothing Bool CSolution)) + (prefix-in ro: rosette/query/debug)) + +(provide define/debug debug) + +(define-typed-syntax define/debug #:datum-literals (: -> →) + [(_ x:id e) ≫ + [⊢ [e ≫ e- ⇒ : τ]] + #:with y (generate-temporary #'x) + -------- + [_ ≻ (begin- + (define-syntax- x (make-rename-transformer (⊢ y : τ))) + (ro:define/debug y e-))]] + [(_ (f [x : ty] ... (~or → ->) ty_out) e ...+) ≫ +; [⊢ [e ≫ e- ⇒ : ty_e]] + #:with f- (generate-temporary #'f) + -------- + [_ ≻ (begin- + (define-syntax- f (make-rename-transformer (⊢ f- : (t/ro:C→ ty ... ty_out)))) + (ro:define/debug f- + (t/ro:λ ([x : ty] ...) + (t/ro:ann (t/ro:begin e ...) : ty_out))))]]) + +(define-typed-syntax debug + [(_ (pred? ...+) e) ≫ + [⊢ [pred? ≫ pred?- (⇒ : _) (⇒ typefor ty) (⇒ solvable? s?) (⇒ function? f?)]] ... + #:fail-unless (stx-andmap syntax-e #'(s? ...)) + (format "Expected a Rosette-solvable type, given ~a." + (syntax->datum #'(pred? ...))) + #:fail-when (stx-ormap syntax-e #'(f? ...)) + (format "Expected a non-function Rosette type, given ~a." + (syntax->datum #'(pred? ...))) + [⊢ [e ≫ e- ⇒ : τ]] + -------- + [⊢ [_ ≫ (ro:debug (pred?- ...) e-) ⇒ : t/ro:CSolution]]]) + diff --git a/turnstile/examples/rosette/rosette3.rkt b/turnstile/examples/rosette/rosette3.rkt new file mode 100644 index 0000000..f7ae136 --- /dev/null +++ b/turnstile/examples/rosette/rosette3.rkt @@ -0,0 +1,1789 @@ +#lang turnstile +(extends "../stlc.rkt" #:except #%module-begin #%app →) +(reuse #%datum define-type-alias define-named-type-alias + #:from "../stlc+union.rkt") + +(provide (rename-out [ro:#%module-begin #%module-begin] + [stlc:λ lambda]) + Any Nothing + CU U + Constant + C→ → (for-syntax ~C→ C→?) + Ccase-> (for-syntax ~Ccase-> Ccase->?) ; TODO: symbolic case-> not supported yet + CListof Listof CList CPair Pair + CVectorof MVectorof IVectorof Vectorof CMVectorof CIVectorof + CParamof ; TODO: symbolic Param not supported yet + CBoxof MBoxof IBoxof CMBoxof CIBoxof CHashTable + CUnit Unit + CNegInt NegInt + CZero Zero + CPosInt PosInt + CNat Nat + CInt Int + CFloat Float + CNum Num + CFalse CTrue CBool Bool + CString String + CStx ; symblic Stx not supported + CAsserts + ;; BV types + CBV BV + CBVPred BVPred + CSolution CSolver CPict CSyntax) + +(require + (prefix-in ro: rosette) + (only-in "../stlc+union.rkt" define-named-type-alias prune+sort current-sub?) + (prefix-in C + (combine-in + (only-in "../stlc+union+case.rkt" + PosInt Zero NegInt Float True False String [U U*] U*? + [case-> case->*] case->? → →?) + (only-in "../stlc+cons.rkt" Unit [List Listof]))) + (only-in "../stlc+union+case.rkt" [~U* ~CU*] [~case-> ~Ccase->] [~→ ~C→]) + (only-in "../stlc+cons.rkt" [~List ~CListof]) + (only-in "../ext-stlc.rkt" [define stlc:define]) + (rename-in "rosette-util.rkt" [bitvector? lifted-bitvector?])) + +;; copied from rosette.rkt +(provide rosette-typed-out) +(define-for-syntax (mk-ro:-id id) (format-id id "ro:~a" id)) + +(define-syntax rosette-typed-out + (make-provide-pre-transformer + (lambda (stx modes) + (syntax-parse stx #:datum-literals (:) + ;; cannot write ty:type bc provides might precede type def + [(_ (~and (~or (~and [out-x:id (~optional :) ty] (~parse x #'out-x)) + [[x:id (~optional :) ty] out-x:id])) ...) + #:with (ro-x ...) (stx-map mk-ro:-id #'(x ...)) + (pre-expand-export (syntax/loc stx (typed-out [[ro-x ty] out-x] ...)) + modes)])))) + +;; a legacy auto-providing version of define-typed-syntax +;; TODO: convert everything to new define-typed-syntax +(define-syntax (define-typed-syntax stx) + (syntax-parse stx + [(_ name:id #:export-as out-name:id . rst) + #'(begin- + (provide- (rename-out [name out-name])) + (define-typerule name . rst))] ; define-typerule doesnt provide + [(_ name:id . rst) + #'(define-typed-syntax name #:export-as name . rst)] + [(_ (name:id . pat) . rst) + #'(define-typed-syntax name #:export-as name [(_ . pat) . rst])])) + +;; --------------------------------- +;; Concrete and Symbolic union types + +(begin-for-syntax + (define (concrete? t) + (not (or (Any? t) (U*? t) (Constant*? t))))) + +(define-base-types Any CBV CStx CSymbol) +;; CVectorof includes all vectors +;; CIVectorof includes only immutable vectors +;; CMVectorof includes only mutable vectors +(define-type-constructor CIVectorof #:arity = 1) +(define-type-constructor CMVectorof #:arity = 1) +(define-type-constructor CMBoxof #:arity = 1) +(define-type-constructor CIBoxof #:arity = 1) +;; TODO: Hash subtyping? +;; - invariant for now, like TR, though Rosette only uses immutable hashes? +(define-type-constructor CHashTable #:arity = 2) +(define-named-type-alias (CVectorof X) (CU (CIVectorof X) (CMVectorof X))) +(define-named-type-alias (CBoxof X) (CU (CIBoxof X) (CMBoxof X))) +(define-type-constructor CList #:arity >= 0) +(define-type-constructor CPair #:arity = 2) + +;; TODO: update orig to use reduced type +(define-syntax (CU stx) + (syntax-parse stx + [(_ . tys) + #:with tys+ (stx-map (current-type-eval) #'tys) + #:fail-unless (stx-andmap concrete? #'tys+) + "CU requires concrete types" + #'(CU* . tys+)])) + +(define-named-type-alias Nothing (CU)) + +;; internal symbolic union constructor +(define-type-constructor U* #:arity >= 0) + +;; user-facing symbolic U constructor: flattens and prunes +(define-syntax (U stx) + (syntax-parse stx + [(_ . tys) + ;; canonicalize by expanding to U*, with only (sorted and pruned) leaf tys + #:with ((~or (~U* ty1- ...) (~CU* ty2- ...) ty3-) ...) (stx-map (current-type-eval) #'tys) + #:with tys- (prune+sort #'(ty1- ... ... ty2- ... ... ty3- ...)) + #'(U* . tys-)])) + +;; internal symbolic constant constructor +(define-type-constructor Constant* #:arity = 1) + +(define-for-syntax (remove-Constant ty) + (syntax-parse ty + [(~Constant* t) #'t] + [(~U* . tys) ; redo U reductions + ((current-type-eval) #`(U . #,(stx-map remove-Constant #'tys)))] + [(tycon . tys) + (transfer-stx-props #`(tycon . #,(stx-map remove-Constant #'tys)) ty)] + [any ty])) + +;; user-facing symbolic constant constructor: enforce non-concrete type +(define-syntax Constant + (syntax-parser + [(_ τ) + #:with τ+ ((current-type-eval) #'τ) + #:fail-when (and (concrete? #'τ+) #'τ) + "Constant requires a symbolic type" + #'(Constant* τ+)])) + +;; --------------------------------- +;; case-> and Ccase-> + +;; Ccase-> must check that its subparts are concrete → types +(define-syntax (Ccase-> stx) + (syntax-parse stx + [(_ . tys) + #:with tys+ (stx-map (current-type-eval) #'tys) + #:fail-unless (stx-andmap C→? #'tys+) + "CU require concrete arguments" + #'(Ccase->* . tys+)])) + +;; TODO: What should case-> do when given symbolic function +;; types? Should it transform (case-> (U (C→ τ ...)) ...) +;; into (U (Ccase-> (C→ τ ...) ...)) ? What makes sense here? + +;; --------------------------------- +;; Symbolic versions of types + +(begin-for-syntax + (define (add-pred stx pred) + (set-stx-prop/preserved stx 'pred pred)) + (define (get-pred stx) + (syntax-property stx 'pred)) + (define (add-typefor stx t) + (set-stx-prop/preserved stx 'typefor t)) + (define (get-typefor stx) + (syntax-property stx 'typefor)) + (define (mark-solvable stx) + (set-stx-prop/preserved stx 'solvable? #t)) + (define (set-solvable stx v) + (set-stx-prop/preserved stx 'solvable? v)) + (define (solvable? stx) + (syntax-property stx 'solvable?)) + (define (mark-function stx) + (set-stx-prop/preserved stx 'function? #t)) + (define (set-function stx v) + (set-stx-prop/preserved stx 'function? v)) + (define (function? stx) + (syntax-property stx 'function?))) + +(define-syntax-parser add-predm + [(_ stx pred) (add-pred #'stx #'pred)]) +(define-syntax-parser add-typeform + [(_ stx t) (add-typefor #'stx #'t)]) +(define-syntax-parser mark-solvablem + [(_ stx) (mark-solvable #'stx)]) +(define-syntax-parser mark-functionm + [(_ stx) (mark-function #'stx)]) + +(define-named-type-alias NegInt (add-predm (U CNegInt) negative-integer?)) +(define-named-type-alias Zero (add-predm (U CZero) zero-integer?)) +(define-named-type-alias PosInt (add-predm (U CPosInt) positive-integer?)) +(define-named-type-alias Float (U CFloat)) +(define-named-type-alias String (U CString)) +(define-named-type-alias Unit (add-predm (U CUnit) ro:void?)) +(define-named-type-alias (CParamof X) (Ccase-> (C→ X) + (C→ X CUnit))) +(define-named-type-alias (Listof X) (U (CListof X))) +(define-named-type-alias (Vectorof X) (U (CVectorof X))) +(define-named-type-alias (MVectorof X) (U (CMVectorof X))) +(define-named-type-alias (IVectorof X) (U (CIVectorof X))) +(define-named-type-alias (MBoxof X) (U (CMBoxof X))) +(define-named-type-alias (IBoxof X) (U (CIBoxof X))) +(define-named-type-alias (Pair X Y) (U (CPair X Y))) + +(define-syntax → + (syntax-parser + [(_ ty ...+) + (add-pred + (add-orig + #'(U (C→ ty ...)) + this-syntax) + #'ro:fv?)])) + +(define-syntax define-symbolic-named-type-alias + (syntax-parser + [(_ Name:id Cτ:expr #:pred p?) + #:with Cτ+ ((current-type-eval) #'Cτ) + #:fail-when (and (not (concrete? #'Cτ+)) #'Cτ+) + "should be a concrete type" + #:with CName (format-id #'Name "C~a" #'Name #:source #'Name) + #'(begin- + (define-named-type-alias CName Cτ) + (define-named-type-alias Name (add-predm (U CName) p?)))])) + +(define-symbolic-named-type-alias Bool (CU CFalse CTrue) #:pred ro:boolean?) +(define-symbolic-named-type-alias Nat (CU CZero CPosInt) #:pred nonnegative-integer?) +(define-symbolic-named-type-alias Int (CU CNegInt CNat) #:pred ro:integer?) +(define-symbolic-named-type-alias Num (CU CFloat CInt) #:pred ro:real?) + +(define-named-type-alias CPred (C→ Any Bool)) + +;; --------------------------------- +;; define-symbolic + +(define-typed-syntax define-symbolic + [(_ x:id ...+ pred?) ≫ + [⊢ [pred? ≫ pred?- (⇒ : _) (⇒ typefor ty) (⇒ solvable? s?)]] + #:fail-unless (syntax-e #'s?) + (format "Expected a Rosette-solvable type, given ~a." + (syntax->datum #'pred?)) + #:with (y ...) (generate-temporaries #'(x ...)) + -------- + [_ ≻ (begin- + (define-syntax- x (make-rename-transformer (⊢ y : (Constant ty)))) ... + (ro:define-symbolic y ... pred?-))]]) + +(define-typed-syntax define-symbolic* + [(_ x:id ...+ pred?) ≫ + [⊢ [pred? ≫ pred?- (⇒ : _) (⇒ typefor ty) (⇒ solvable? s?)]] + #:fail-unless (syntax-e #'s?) + (format "Expected a Rosette-solvable type, given ~a." + (syntax->datum #'pred?)) + #:with (y ...) (generate-temporaries #'(x ...)) + -------- + [_ ≻ (begin- + (define-syntax- x (make-rename-transformer (⊢ y : (Constant ty)))) ... + (ro:define-symbolic* y ... pred?-))]]) + +;; TODO: support internal definition contexts +(define-typed-syntax let-symbolic + [(_ (x:id ...+ pred?) e ...) ≫ + [⊢ [pred? ≫ pred?- (⇒ : _) (⇒ typefor ty) (⇒ solvable? s?)]] + #:fail-unless (syntax-e #'s?) + (format "Expected a Rosette-solvable type, given ~a." + (syntax->datum #'pred?)) + [([x ≫ x- : (Constant ty)] ...) ⊢ [(begin e ...) ≫ e- ⇒ τ_out]] + -------- + [⊢ [_ ≫ (ro:let-values + ([(x- ...) (ro:let () + (ro:define-symbolic x ... pred?-) + (ro:values x ...))]) + e-) ⇒ : τ_out]]]) +(define-typed-syntax let-symbolic* + [(_ (x:id ...+ pred?) e ...) ≫ + [⊢ [pred? ≫ pred?- (⇒ : _) (⇒ typefor ty) (⇒ solvable? s?)]] + #:fail-unless (syntax-e #'s?) + (format "Expected a Rosette-solvable type, given ~a." + (syntax->datum #'pred?)) + [([x ≫ x- : (Constant ty)] ...) ⊢ [(begin e ...) ≫ e- ⇒ τ_out]] + -------- + [⊢ [_ ≫ (ro:let-values + ([(x- ...) (ro:let () + (ro:define-symbolic* x ... pred?-) + (ro:values x ...))]) + e-) ⇒ : τ_out]]]) + +;; --------------------------------- +;; assert, assert-type + +(define-typed-syntax assert + [(_ e) ≫ + [⊢ [e ≫ e- ⇒ : _]] + -------- + [⊢ [_ ≫ (ro:assert e-) ⇒ : CUnit]]] + [(_ e m) ≫ + [⊢ [e ≫ e- ⇒ : _]] + [⊢ [m ≫ m- ⇐ : (CU CString (C→ Nothing))]] + -------- + [⊢ [_ ≫ (ro:assert e- m-) ⇒ : CUnit]]]) + +;; TODO: assert-type wont work with unlifted types +;; but sometimes it should, eg in with for/all lifted functions +;; - but this means we need to lift a pred (eg string?) and associate it with the newly lifted type +(define-typed-syntax assert-type #:datum-literals (:) + [(_ e : ty:type) ≫ + [⊢ [e ≫ e- ⇒ : _]] + #:with pred (get-pred #'ty.norm) + -------- + [⊢ [_ ≫ (ro:#%app assert-pred e- pred) ⇒ : ty.norm]]]) + + +;; --------------------------------- +;; Racket forms + +;; TODO: many of these implementations are copied code, with just the macro +;; output changed to use the ro: version. +;; Is there a way to abstract this? macro mixin? + +(define-typed-syntax define #:datum-literals (: -> →) + [(_ x:id e) ≫ + -------- + [_ ≻ (stlc:define x e)]] + [(_ (f [x : ty] ... (~or → ->) ty_out) e ...+) ≫ +; [⊢ [e ≫ e- ⇒ : ty_e]] + #:with f- (generate-temporary #'f) + -------- + [_ ≻ (begin- + (define-syntax- f + (make-rename-transformer (⊢ f- : (C→ ty ... ty_out)))) + (ro:define f- + (stlc:λ ([x : ty] ...) (ann (begin e ...) : ty_out))))]]) + +;; TODO: get subtyping to work for struct-generated types? +;; TODO: handle mutable structs properly +(define-typed-syntax struct #:datum-literals (:) + [(_ name:id (x:id ...) ~! . rst) ≫ + #:fail-when #t "Missing type annotations for fields" + -------- + [_ ≻ (ro:struct name (x ...) . rst)]] + [(_ name:id ([x:id : ty:type] ...) . kws) ≫ + #:fail-unless (id-lower-case? #'name) + (format "Expected lowercase struct name, given ~a" #'name) + #:with name* (generate-temporary #'name) + #:with Name (id-upcase #'name) + #:with CName (format-id #'name "C~a" #'Name) + #:with TyOut #'(Name ty ...) + #:with CTyOut #'(CName ty ...) + #:with (name-x ...) (stx-map (lambda (f) (format-id #'name "~a-~a" #'name f)) #'(x ...)) + #:with (name-x* ...) (stx-map (lambda (f) (format-id #'name* "~a-~a" #'name* f)) #'(x ...)) + #:with name? (format-id #'name "~a?" #'name) + #:with name?* (format-id #'name* "~a?" #'name*) + -------- + [_ ≻ (ro:begin + (ro:struct name* (x ...) . kws) + (define-type-constructor CName #:arity = #,(stx-length #'(x ...))) + (define-named-type-alias (Name x ...) (U (CName x ...))) + (define-syntax name ; constructor + (make-variable-like-transformer + (assign-type #'name* #'(C→ ty ... CTyOut)))) + (define-syntax name? ; predicate + (make-variable-like-transformer + (assign-type #'name?* #'(C→ Any Bool)))) + (define-syntax name-x ; accessors + (make-variable-like-transformer + (assign-type #'name-x* #'(C→ TyOut ty)))) ...)]]) + +;; TODO: add type rules for generics +(define-typed-syntax define-generics #:datum-literals (: ->) + [(_ name:id (f:id x:id ... -> ty-out)) ≫ + #:with app-f (format-id #'f "apply-~a" #'f) + -------- + [_ ≻ (ro:begin + (ro:define-generics name (f x ...)) + (define-syntax app-f ; tmp workaround: each gen fn has its own apply + (syntax-parser + [(_ . es) + #:with es+ (stx-map expand/df #'es) + (assign-type #'(ro:#%app f . es+) #'ty-out)])))]]) + +;; --------------------------------- +;; quote + +;; TODO: don't duplicate #%datum code here +(define-typed-syntax quote + [(_ x:id) ≫ + -------- + [⊢ [_ ≫ (quote- x) ⇒ : CSymbol]]] + [(_ (x:integer ...)) ≫ + #:with ty_out (let ([xs (syntax->datum #'(x ...))]) + (cond [(andmap zero? xs) #'CZero] + [(andmap positive? xs) #'CPosInt] + [else #'CNegInt])) + -------- + [⊢ [_ ≫ (quote- (x ...)) ⇒ : (CListof ty_out)]]] + [(_ (x:id ...)) ≫ + -------- + [⊢ [_ ≫ (quote- (x ...)) ⇒ : (CListof CSymbol)]]] + [(_ (x . y)) ≫ + [⊢ [x ≫ x- ⇒ : τx]] + [⊢ [y ≫ y- ⇒ : τy]] + -------- + [⊢ [_ ≫ (quote- (x . y)) ⇒ : (CPair τx τy)]]]) + +;; --------------------------------- +;; Function Application + +;; copied from rosette.rkt +(define-typed-syntax app #:export-as #%app + ;; concrete functions + [(_ e_fn e_arg ...) ≫ + [⊢ [e_fn ≫ e_fn- ⇒ : (~C→ ~! τ_in ... τ_out)]] + #:with e_fn/progsrc- (replace-stx-loc #'e_fn- #'e_fn) + #:fail-unless (stx-length=? #'[τ_in ...] #'[e_arg ...]) + (num-args-fail-msg #'e_fn #'[τ_in ...] #'[e_arg ...]) + [⊢ [e_arg ≫ e_arg- ⇐ : τ_in] ...] + -------- + ;; TODO: use e_fn/progsrc- (currently causing "cannot use id tainted in macro trans" err) + [⊢ [_ ≫ (ro:#%app e_fn/progsrc- e_arg- ...) ⇒ : τ_out]]] + ;; concrete case-> + [(_ e_fn e_arg ...) ≫ + [⊢ [e_fn ≫ e_fn- ⇒ : (~Ccase-> ~! . (~and ty_fns ((~C→ . _) ...)))]] + #:with e_fn/progsrc- (replace-stx-loc #'e_fn- #'e_fn) + [⊢ [e_arg ≫ e_arg- ⇒ : τ_arg] ...] + #:with τ_out + (for/first ([ty_f (stx->list #'ty_fns)] + #:when (syntax-parse ty_f + [(~C→ τ_in ... τ_out) + (and (stx-length=? #'(τ_in ...) #'(e_arg ...)) + (typechecks? #'(τ_arg ...) #'(τ_in ...)))])) + (syntax-parse ty_f [(~C→ _ ... t_out) #'t_out])) + #:fail-unless (syntax-e #'τ_out) + ; use (failing) typechecks? to get err msg + (syntax-parse #'ty_fns + [((~C→ τ_in ... _) ...) + (let* ([τs_expecteds #'((τ_in ...) ...)] + [τs_given #'(τ_arg ...)] + [expressions #'(e_arg ...)]) + (format (string-append "type mismatch\n" + " expected one of:\n" + " ~a\n" + " given: ~a\n" + " expressions: ~a") + (string-join + (stx-map + (lambda (τs_expected) + (string-join (stx-map type->str τs_expected) ", ")) + τs_expecteds) + "\n ") + (string-join (stx-map type->str τs_given) ", ") + (string-join (map ~s (stx-map syntax->datum expressions)) ", ")))]) + -------- + [⊢ [_ ≫ (ro:#%app e_fn/progsrc- e_arg- ...) ⇒ : τ_out]]] + ;; concrete union functions + [(_ e_fn e_arg ...) ≫ + [⊢ [e_fn ≫ e_fn- ⇒ : (~CU* τ_f ...)]] + #:with e_fn/progsrc- (replace-stx-loc #'e_fn- #'e_fn) + [⊢ [e_arg ≫ e_arg- ⇒ : τ_arg] ...] + #:with (f a ...) (generate-temporaries #'(e_fn e_arg ...)) + [([f ≫ _ : τ_f] [a ≫ _ : τ_arg] ...) + ⊢ [(app f a ...) ≫ _ ⇒ : τ_out]] + ... + -------- + [⊢ [_ ≫ (ro:#%app e_fn/progsrc- e_arg- ...) ⇒ : (CU τ_out ...)]]] + ;; symbolic functions + [(_ e_fn e_arg ...) ≫ + [⊢ [e_fn ≫ e_fn- ⇒ : (~U* τ_f ...)]] + #:with e_fn/progsrc- (replace-stx-loc #'e_fn- #'e_fn) + [⊢ [e_arg ≫ e_arg- ⇒ : τ_arg] ...] + #:with (f a ...) (generate-temporaries #'(e_fn e_arg ...)) + [([f ≫ _ : τ_f] [a ≫ _ : τ_arg] ...) + ⊢ [(app f a ...) ≫ _ ⇒ : τ_out]] + ... + -------- + [⊢ [_ ≫ (ro:#%app e_fn/progsrc- e_arg- ...) ⇒ : (U τ_out ...)]]] + ;; constant symbolic fns + [(_ e_fn e_arg ...) ≫ + [⊢ [e_fn ≫ e_fn- ⇒ : (~Constant* (~U* τ_f ...))]] + #:with e_fn/progsrc- (replace-stx-loc #'e_fn- #'e_fn) + [⊢ [e_arg ≫ e_arg- ⇒ : τ_arg] ...] + #:with (f a ...) (generate-temporaries #'(e_fn e_arg ...)) + [([f ≫ _ : τ_f] [a ≫ _ : τ_arg] ...) + ⊢ [(app f a ...) ≫ _ ⇒ : τ_out]] + ... + -------- + [⊢ [_ ≫ (ro:#%app e_fn/progsrc- e_arg- ...) ⇒ : (U τ_out ...)]]]) + +;; --------------------------------- +;; if + +;; TODO: this is not precise enough +;; specifically, a symbolic non-bool should produce a concrete val +(define-typed-syntax if + [(_ e_tst e1 e2) ≫ + [⊢ [e_tst ≫ e_tst- ⇒ : ty_tst]] + #:when (or (concrete? #'ty_tst) ; either concrete + ; or non-bool symbolic + (not (typecheck? #'ty_tst ((current-type-eval) #'Bool)))) + [⊢ [e1 ≫ e1- ⇒ : ty1]] + [⊢ [e2 ≫ e2- ⇒ : ty2]] + #:when (and (concrete? #'ty1) (concrete? #'ty2)) + -------- + [⊢ [_ ≫ (ro:if e_tst- e1- e2-) ⇒ : (CU ty1 ty2)]]] + [(_ e_tst e1 e2) ≫ + [⊢ [e_tst ≫ e_tst- ⇒ : _]] + [⊢ [e1 ≫ e1- ⇒ : ty1]] + [⊢ [e2 ≫ e2- ⇒ : ty2]] + -------- + [⊢ [_ ≫ (ro:if e_tst- e1- e2-) ⇒ : (U ty1 ty2)]]]) + +;; --------------------------------- +;; let, etc (copied from ext-stlc.rkt) + +(define-typed-syntax let + [(let ([x e] ...) e_body ...) ⇐ : τ_expected ≫ + [⊢ [e ≫ e- ⇒ : τ_x] ...] + [() ([x ≫ x- : τ_x] ...) ⊢ [(begin e_body ...) ≫ e_body- ⇐ : τ_expected]] + -------- + [⊢ [_ ≫ (ro:let ([x- e-] ...) e_body-) ⇐ : _]]] + [(let ([x e] ...) e_body ...) ≫ + [⊢ [e ≫ e- ⇒ : τ_x] ...] + [() ([x ≫ x- : τ_x] ...) ⊢ [(begin e_body ...) ≫ e_body- ⇒ : τ_body]] + -------- + [⊢ [_ ≫ (ro:let ([x- e-] ...) e_body-) ⇒ : τ_body]]]) + +; dont need to manually transfer expected type +; result template automatically propagates properties +; - only need to transfer expected type when local expanding an expression +; - see let/tc +(define-typed-syntax let* + [(let* () e_body ...) ≫ + -------- + [_ ≻ (begin e_body ...)]] + [(let* ([x e] [x_rst e_rst] ...) e_body ...) ≫ + -------- + [_ ≻ (let ([x e]) (let* ([x_rst e_rst] ...) e_body ...))]]) + +(define-typed-syntax letrec + [(letrec ([b:type-bind e] ...) e_body ...) ⇐ : τ_expected ≫ + [() ([b.x ≫ x- : b.type] ...) + ⊢ [e ≫ e- ⇐ : b.type] ... [(begin e_body ...) ≫ e_body- ⇐ : τ_expected]] + -------- + [⊢ [_ ≫ (ro:letrec ([x- e-] ...) e_body-) ⇐ : _]]] + [(letrec ([b:type-bind e] ...) e_body ...) ≫ + [() ([b.x ≫ x- : b.type] ...) + ⊢ [e ≫ e- ⇐ : b.type] ... [(begin e_body ...) ≫ e_body- ⇒ : τ_body]] + -------- + [⊢ [_ ≫ (ro:letrec ([x- e-] ...) e_body-) ⇒ : τ_body]]]) + +;; -------------------- +;; begin + +(define-typed-syntax begin + [(begin e_unit ... e) ⇐ : τ_expected ≫ + [⊢ [e_unit ≫ e_unit- ⇒ : _] ...] + [⊢ [e ≫ e- ⇐ : τ_expected]] + -------- + [⊢ [_ ≫ (ro:begin e_unit- ... e-) ⇐ : _]]] + [(begin e_unit ... e) ≫ + [⊢ [e_unit ≫ e_unit- ⇒ : _] ...] + [⊢ [e ≫ e- ⇒ : τ_e]] + -------- + [⊢ [_ ≫ (ro:begin e_unit- ... e-) ⇒ : τ_e]]]) + +;; --------------------------------- +;; set! + +;; TODO: use x instead of x-? +(define-typed-syntax set! + [(set! x:id e) ≫ + [⊢ [x ≫ x- ⇒ : ty_x]] + [⊢ [e ≫ e- ⇐ : ty_x]] + -------- + [⊢ [_ ≫ (ro:set! x- e-) ⇒ : CUnit]]]) + +;; --------------------------------- +;; vector + +;; mutable constructor +(define-typed-syntax vector + [(_ e ...) ≫ + [⊢ [e ≫ e- ⇒ : τ] ...] + -------- + [⊢ [_ ≫ (ro:vector e- ...) ⇒ : #,(if (stx-andmap concrete? #'(τ ...)) + #'(CMVectorof (CU τ ...)) + #'(CMVectorof (U τ ...)))]]]) + +(provide (rosette-typed-out [vector? : CPred])) + +;; immutable constructor +(define-typed-syntax vector-immutable + [(_ e ...) ≫ + [⊢ [e ≫ e- ⇒ : τ] ...] + -------- + [⊢ [_ ≫ (ro:vector-immutable e- ...) ⇒ : #,(if (stx-andmap concrete? #'(τ ...)) + #'(CIVectorof (CU τ ...)) + #'(CIVectorof (U τ ...)))]]]) + +;; TODO: add CList case? +;; returne mutable vector +(define-typed-syntax list->vector + [_:id ≫ ;; TODO: use polymorphism + -------- + [⊢ [_ ≫ ro:list->vector ⇒ : (Ccase-> (C→ (CListof Any) (CMVectorof Any)) + (C→ (Listof Any) (MVectorof Any)))]]] + [(_ e) ≫ + [⊢ [e ≫ e- ⇒ : (~CListof τ)]] + -------- + [⊢ [_ ≫ (ro:list->vector e-) ⇒ : (CMVectorof τ)]]] + [(_ e) ≫ + [⊢ [e ≫ e- ⇒ : (~U* (~CListof τ) ...)]] + -------- + [⊢ [_ ≫ (ro:list->vector e-) ⇒ : (U (CMVectorof τ) ...)]]] + [(_ e) ≫ + [⊢ [e ≫ e- ⇒ : (~CList τ ...)]] + -------- + [⊢ [_ ≫ (ro:list->vector e-) ⇒ : (CMVectorof (U τ ...))]]] + [(_ e) ≫ + [⊢ [e ≫ e- ⇒ : (~U* (~CList τ ...) ...)]] + -------- + [⊢ [_ ≫ (ro:list->vector e-) ⇒ : (U (CMVector (U τ ...)) ...)]]]) + +(define-typed-syntax vector-ref + [(_ e n) ≫ + [⊢ [e ≫ e- ⇒ : (~or (~CMVectorof τ) (~CIVectorof τ))]] + [⊢ [n ≫ n- ⇐ : Int]] + -------- + [⊢ [_ ≫ (ro:vector-ref e- n-) ⇒ : τ]]] + [(_ e n) ≫ + [⊢ [e ≫ e- ⇒ : (~U* (~and (~or (~CMVectorof τ) (~CIVectorof τ))) ...)]] + [⊢ [n ≫ n- ⇐ : Int]] + -------- + [⊢ [_ ≫ (ro:vector-ref e- n-) ⇒ : (U τ ...)]]]) + +;; --------------------------------- +;; hash tables + +(define-typed-syntax hash-keys + [(_ e) ≫ + [⊢ [e ≫ e- ⇒ : (~CHashTable τ _)]] + -------- + [⊢ [_ ≫ (ro:hash-keys e-) ⇒ : (CListof τ)]]]) + +(define-typed-syntax hash-values + [(_ e) ≫ + [⊢ [e ≫ e- ⇒ : (~CHashTable _ τ)]] + -------- + [⊢ [_ ≫ (ro:hash-values e-) ⇒ : (CListof τ)]]]) + +;; --------------------------------- +;; lists + +(provide (rosette-typed-out [null? : (Ccase-> (C→ (CListof Any) CBool) + (C→ (Listof Any) Bool))] + [empty? : (Ccase-> (C→ (CListof Any) CBool) + (C→ (Listof Any) Bool))] + [list? : CPred])) + +(define-typed-syntax list + [(_ e ...) ≫ + [⊢ [e ≫ e- ⇒ : τ] ...] + -------- + [⊢ [_ ≫ (ro:list e- ...) ⇒ : (CList τ ...)]]]) + +(define-typed-syntax cons + [_:id ≫ ;; TODO: use polymorphism + -------- + [⊢ [_ ≫ ro:cons ⇒ : (Ccase-> + (C→ Any Any (CPair Any Any)) + (C→ Any (CListof Any) (CListof Any)) + (C→ Any (Listof Any) (Listof Any)))]]] + [(_ e1 e2) ≫ + [⊢ [e2 ≫ e2- ⇒ : (~CListof τ1)]] + [⊢ [e1 ≫ e1- ⇒ : τ2]] + -------- + [⊢ [_ ≫ (ro:cons e1- e2-) + ⇒ : #,(if (and (concrete? #'τ1) (concrete? #'τ2)) + #'(CListof (CU τ1 τ2)) + #'(CListof (U τ1 τ2)))]]] + [(_ e1 e2) ≫ + [⊢ [e2 ≫ e2- ⇒ : (~U* (~CListof τ) ...)]] + [⊢ [e1 ≫ e1- ⇒ : τ1]] + -------- + [⊢ [_ ≫ (ro:cons e1- e2-) ⇒ : (U (CListof (U τ1 τ)) ...)]]] + [(_ e1 e2) ≫ + [⊢ [e1 ≫ e1- ⇒ : τ1]] + [⊢ [e2 ≫ e2- ⇒ : (~CList τ ...)]] + -------- + [⊢ [_ ≫ (ro:cons e1- e2-) ⇒ : (CList τ1 τ ...)]]] + [(_ e1 e2) ≫ + [⊢ [e1 ≫ e1- ⇒ : τ1]] + [⊢ [e2 ≫ e2- ⇒ : (~U* (~CList τ ...) ...)]] + -------- + [⊢ [_ ≫ (ro:cons e1- e2-) ⇒ : (U (CList τ1 τ ...) ...)]]] + [(_ e1 e2) ≫ + [⊢ [e1 ≫ e1- ⇒ : τ1]] + [⊢ [e2 ≫ e2- ⇒ : τ2]] + -------- + [⊢ [_ ≫ (ro:cons e1- e2-) ⇒ : (CPair τ1 τ2)]]]) + +;; car and cdr additionally support pairs +(define-typed-syntax car + [_:id ≫ ;; TODO: use polymorphism + -------- + [⊢ [_ ≫ ro:car ⇒ : (Ccase-> (C→ (Pair Any Any) Any) + (C→ (Listof Any) Any))]]] + [(_ e) ≫ + [⊢ [e ≫ e- ⇒ : (~CListof τ)]] + -------- + [⊢ [_ ≫ (ro:car e-) ⇒ : τ]]] + [(_ e) ≫ + [⊢ [e ≫ e- ⇒ : (~U* (~CListof τ) ...)]] + -------- + [⊢ [_ ≫ (ro:car e-) ⇒ : (U τ ...)]]] + [(_ e) ≫ + [⊢ [e ≫ e- ⇒ : (~CList τ1 τ ...)]] + -------- + [⊢ [_ ≫ (ro:car e-) ⇒ : τ1]]] + [(_ e) ≫ + [⊢ [e ≫ e- ⇒ : (~U* (~CList τ1 τ ...) ...)]] + -------- + [⊢ [_ ≫ (ro:car e-) ⇒ : (U τ1 ...)]]] + [(_ e) ≫ + [⊢ [e ≫ e- ⇒ : (~CPair τ _)]] + -------- + [⊢ [_ ≫ (ro:car e-) ⇒ : τ]]] + [(_ e) ≫ + [⊢ [e ≫ e- ⇒ : (~U* (~CPair τ _) ...)]] + -------- + [⊢ [_ ≫ (ro:car e-) ⇒ : (U τ ...)]]]) + +(define-typed-syntax cdr + [_:id ≫ ;; TODO: use polymorphism + -------- + [⊢ [_ ≫ ro:cdr ⇒ : (Ccase-> (C→ (CListof Any) (CListof Any)) + (C→ (Listof Any) (Listof Any)))]]] + [(_ e) ≫ + [⊢ [e ≫ e- ⇒ : (~CListof τ)]] + -------- + [⊢ [_ ≫ (ro:cdr e-) ⇒ : (CListof τ)]]] + [(_ e) ≫ + [⊢ [e ≫ e- ⇒ : (~U* (~CListof τ) ...)]] + -------- + [⊢ [_ ≫ (ro:cdr e-) ⇒ : (U (CListof τ) ...)]]] + [(_ e) ≫ + [⊢ [e ≫ e- ⇒ : (~CList τ1 τ ...)]] + -------- + [⊢ [_ ≫ (ro:cdr e-) ⇒ : (CList τ ...)]]] + [(_ e) ≫ + [⊢ [e ≫ e- ⇒ : (~U* (~CList τ1 τ ...) ...)]] + -------- + [⊢ [_ ≫ (ro:cdr e-) ⇒ : (U (CList τ ...) ...)]]] + [(_ e) ≫ + [⊢ [e ≫ e- ⇒ : (~CPair _ τ)]] + -------- + [⊢ [_ ≫ (ro:cdr e-) ⇒ : τ]]] + [(_ e) ≫ + [⊢ [e ≫ e- ⇒ : (~U* (~CPair _ τ) ...)]] + -------- + [⊢ [_ ≫ (ro:cdr e-) ⇒ : (U τ ...)]]]) + + +(define-typed-syntax first + [_:id ≫ ;; TODO: use polymorphism + -------- + [⊢ [_ ≫ ro:first ⇒ : (C→ (Listof Any) Any)]]] + [(_ e) ≫ + [⊢ [e ≫ e- ⇒ : (~CListof τ)]] + -------- + [⊢ [_ ≫ (ro:first e-) ⇒ : τ]]] + [(_ e) ≫ + [⊢ [e ≫ e- ⇒ : (~U* (~CListof τ) ...)]] + -------- + [⊢ [_ ≫ (ro:first e-) ⇒ : (U τ ...)]]] + [(_ e) ≫ + [⊢ [e ≫ e- ⇒ : (~CList τ1 τ ...)]] + -------- + [⊢ [_ ≫ (ro:first e-) ⇒ : τ1]]] + [(_ e) ≫ + [⊢ [e ≫ e- ⇒ : (~U* (~CList τ1 τ ...) ...)]] + -------- + [⊢ [_ ≫ (ro:first e-) ⇒ : (U τ1 ...)]]]) + +(define-typed-syntax rest + [_:id ≫ ;; TODO: use polymorphism + -------- + [⊢ [_ ≫ ro:rest ⇒ : (Ccase-> (C→ (CListof Any) (CListof Any)) + (C→ (Listof Any) (Listof Any)))]]] + [(_ e) ≫ + [⊢ [e ≫ e- ⇒ : (~CListof τ)]] + -------- + [⊢ [_ ≫ (ro:rest e-) ⇒ : (CListof τ)]]] + [(_ e) ≫ + [⊢ [e ≫ e- ⇒ : (~U* (~CListof τ) ...)]] + -------- + [⊢ [_ ≫ (ro:rest e-) ⇒ : (U (CListof τ) ...)]]] + [(_ e) ≫ + [⊢ [e ≫ e- ⇒ : (~CList τ1 τ ...)]] + -------- + [⊢ [_ ≫ (ro:rest e-) ⇒ : (CList τ ...)]]] + [(_ e) ≫ + [⊢ [e ≫ e- ⇒ : (~U* (~CList τ1 τ ...) ...)]] + -------- + [⊢ [_ ≫ (ro:rest e-) ⇒ : (U (CList τ ...) ...)]]]) + +(define-typed-syntax second + [_:id ≫ ;; TODO: use polymorphism + -------- + [⊢ [_ ≫ ro:second ⇒ : (C→ (Listof Any) Any)]]] + [(_ e) ≫ + [⊢ [e ≫ e- ⇒ : (~CListof τ)]] + -------- + [⊢ [_ ≫ (ro:second e-) ⇒ : τ]]] + [(_ e) ≫ + [⊢ [e ≫ e- ⇒ : (~U* (~CListof τ) ...)]] + -------- + [⊢ [_ ≫ (ro:second e-) ⇒ : (U τ ...)]]] + [(_ e) ≫ + [⊢ [e ≫ e- ⇒ : (~CList τ1 τ2 τ ...)]] + -------- + [⊢ [_ ≫ (ro:second e-) ⇒ : τ2]]] + [(_ e) ≫ + [⊢ [e ≫ e- ⇒ : (~U* (~CList τ1 τ2 τ ...) ...)]] + -------- + [⊢ [_ ≫ (ro:second e-) ⇒ : (U τ2 ...)]]]) + +;; n must be Int bc Rosette does not have symbolic Nats +(define-typed-syntax take + [_:id ≫ ;; TODO: use polymorphism + -------- + [⊢ [_ ≫ ro:take ⇒ : (Ccase-> (C→ (CListof Any) CInt (CListof Any)) + (C→ (Listof Any) Int (Listof Any)))]]] + [(_ e n) ≫ + [⊢ [e ≫ e- ⇒ : (~CListof τ)]] + [⊢ [n ≫ n- ⇐ : Int]] + -------- + [⊢ [_ ≫ (ro:take e- n-) ⇒ : (CListof τ)]]] + [(_ e n) ≫ + [⊢ [e ≫ e- ⇒ : (~U* (~CListof τ) ...)]] + [⊢ [n ≫ n- ⇐ : Int]] + -------- + [⊢ [_ ≫ (ro:take e- n-) ⇒ : (U (CListof τ) ...)]]] + [(_ e n) ≫ + [⊢ [e ≫ e- ⇒ : (~CList τ ...)]] + [⊢ [n ≫ n- ⇐ : Int]] + -------- + [⊢ [_ ≫ (ro:take e- n-) ⇒ : (CListof (U τ ...))]]] + [(_ e n) ≫ + [⊢ [e ≫ e- ⇒ : (~U* (~CList τ ...) ...)]] + [⊢ [n ≫ n- ⇐ : Int]] + -------- + [⊢ [_ ≫ (ro:take e- n-) ⇒ : (U (CList (U τ ...)) ...)]]]) + +(define-typed-syntax length + [_:id ≫ ;; TODO: use polymorphism + -------- + [⊢ [_ ≫ ro:length ⇒ : (Ccase-> (C→ (CListof Any) CNat) + (C→ (Listof Any) Nat))]]] + [(_ e) ≫ + [⊢ [e ≫ e- ⇐ : (CListof Any)]] + -------- + [⊢ [_ ≫ (ro:length e-) ⇒ : CNat]]] + [(_ e) ≫ + [⊢ [e ≫ e- ⇒ : (~U* (~CListof _) ...)]] + -------- + [⊢ [_ ≫ (ro:length e-) ⇒ : Nat]]] + [(_ e) ≫ + [⊢ [e ≫ e- ⇒ : (~CList _ ...)]] + -------- + [⊢ [_ ≫ (ro:length e-) ⇒ : CNat]]] + [(_ e) ≫ + [⊢ [e ≫ e- ⇒ : (~U* (~CList _ ...) ...)]] + -------- + [⊢ [_ ≫ (ro:length e-) ⇒ : Nat]]]) + +(define-typed-syntax reverse + [_:id ≫ ;; TODO: use polymorphism + -------- + [⊢ [_ ≫ ro:reverse ⇒ : (Ccase-> (C→ (CListof Any) (CListof Any)) + (C→ (Listof Any) (Listof Any)))]]] + [(_ e) ≫ + [⊢ [e ≫ e- ⇒ : (~CListof τ)]] + -------- + [⊢ [_ ≫ (ro:reverse e-) ⇒ : (CListof τ)]]] + [(_ e) ≫ + [⊢ [e ≫ e- ⇒ : (~U* (~CListof τ) ...)]] + -------- + [⊢ [_ ≫ (ro:reverse e-) ⇒ : (U (CListof τ) ...)]]] + [(_ e) ≫ + [⊢ [e ≫ e- ⇒ : (~CList . τs)]] + #:with τs/rev (stx-rev #'τs) + -------- + [⊢ [_ ≫ (ro:reverse e-) ⇒ : (CList . τs/rev)]]] + [(_ e) ≫ + [⊢ [e ≫ e- ⇒ : (~U* (~CList . τs) ...)]] + #:with (τs/rev ...) (stx-map stx-rev #'(τs ...)) + -------- + [⊢ [_ ≫ (ro:reverse e-) ⇒ : (U (CList . τs/rev) ...)]]]) + +(define-typed-syntax build-list + [_:id ≫ ;; TODO: use polymorphism + -------- + [⊢ [_ ≫ ro:build-list ⇒ : (C→ CNat (C→ CNat Any) (CListof Any))]]] + [(_ n f) ≫ + [⊢ [n ≫ n- ⇐ : CNat]] + [⊢ [f ≫ f- ⇒ : (~C→ ty1 ty2)]] + #:fail-unless (typecheck? #'ty1 ((current-type-eval) #'CNat)) + "expected function that consumes concrete Nat" + -------- + [⊢ [_ ≫ (ro:build-list n- f-) ⇒ : (CListof ty2)]]]) +(define-typed-syntax map + #;[_:id ≫ ;; TODO: use polymorphism + -------- + [⊢ [_ ≫ ro:map ⇒ : (C→ (C→ Any Any) (CListof Any) (CListof Any))]]] + [(_ f lst) ≫ + [⊢ [f ≫ f- ⇒ : (~C→ ~! ty1 ty2)]] + [⊢ [lst ≫ lst- ⇐ : (CListof ty1)]] + -------- + [⊢ [_ ≫ (ro:map f- lst-) ⇒ : (CListof ty2)]]] + [(_ f lst) ≫ + [⊢ [lst ≫ lst- ⇒ : (~CListof ty1)]] + [⊢ [f ≫ f- ⇒ : (~Ccase-> ~! ty-fns ...)]] ; find first match + #:with (~C→ _ ty2) + (for/first ([ty-fn (stx->list #'(ty-fns ...))] + #:when (syntax-parse ty-fn + [(~C→ t1 _) #:when (typecheck? #'ty1 #'t1) #t] + [_ #f])) + (displayln (syntax->datum ty-fn)) + ty-fn) + -------- + [⊢ [_ ≫ (ro:map f- lst-) ⇒ : (CListof ty2)]]] + [(_ f lst) ≫ + [⊢ [lst ≫ lst- ⇒ : (~U* (~CListof ty1))]] + [⊢ [f ≫ f- ⇒ : (~Ccase-> ~! ty-fns ...)]] ; find first match + #:with (~C→ _ ty2) + (for/first ([ty-fn (stx->list #'(ty-fns ...))] + #:when (syntax-parse ty-fn + [(~C→ t1 _) #:when (typecheck? #'ty1 #'t1) #t] + [_ #f])) + ty-fn) + -------- + [⊢ [_ ≫ (ro:map f- lst-) ⇒ : (CListof ty2)]]]) + +;; TODO: finish andmap +(define-typed-syntax andmap + #;[_:id ≫ ;; TODO: use polymorphism + -------- + [⊢ [_ ≫ ro:andmap ⇒ : (C→ (C→ Any Bool) (CListof Any) Bool)]]] + [(_ f lst) ≫ + [⊢ [f ≫ f- ⇒ : (~C→ ~! ty ty-bool)]] + [⊢ [lst ≫ lst- ⇒ : (~CListof _)]] + -------- + [⊢ [_ ≫ (ro:andmap f- lst-) ⇒ : Bool]]] + #;[(_ f lst) ≫ + [⊢ [lst ≫ lst- ⇒ : (~CListof ty)]] + [⊢ [f ≫ f- ⇒ : (~Ccase-> ~! ty-fns ...)]] ; find first match + #:with (~C→ _ ty2) + (for/first ([ty-fn (stx->list #'(ty-fns ...))] + #:when (syntax-parse ty-fn + [(~C→ t1 _) #:when (typecheck? #'ty1 #'t1) #t] + [_ #f])) + (displayln (syntax->datum ty-fn)) + ty-fn) + -------- + [⊢ [_ ≫ (ro:map f- lst-) ⇒ : (CListof ty2)]]] + #;[(_ f lst) ≫ + [⊢ [lst ≫ lst- ⇒ : (~U* (~CListof ty1))]] + [⊢ [f ≫ f- ⇒ : (~Ccase-> ~! ty-fns ...)]] ; find first match + #:with (~C→ _ ty2) + (for/first ([ty-fn (stx->list #'(ty-fns ...))] + #:when (syntax-parse ty-fn + [(~C→ t1 _) #:when (typecheck? #'ty1 #'t1) #t] + [_ #f])) + ty-fn) + -------- + [⊢ [_ ≫ (ro:map f- lst-) ⇒ : (CListof ty2)]]]) + +(define-typed-syntax sort + [_:id ≫ ;; TODO: use polymorphism + -------- + [⊢ [_ ≫ ro:sort ⇒ : (Ccase-> (C→ (CListof Any) (C→ Any Any Bool) (CListof Any)) + (C→ (Listof Any) (C→ Any Any Bool) (Listof Any)))]]] + [(_ e cmp) ≫ + [⊢ [e ≫ e- ⇒ : (~CListof τ)]] + [⊢ [cmp ≫ cmp- ⇐ : (C→ τ τ Bool)]] + -------- + [⊢ [_ ≫ (ro:sort e- cmp-) ⇒ : (CListof τ)]]] + [(_ e cmp) ≫ + [⊢ [e ≫ e- ⇒ : (~U* (~CListof τ) ...)]] + [⊢ [cmp ≫ cmp- ⇐ : (C→ (U τ ...) (U τ ...) Bool)]] + -------- + [⊢ [_ ≫ (ro:sort e- cmp-) ⇒ : (U (CListof τ) ...)]]] + [(_ e cmp) ≫ + [⊢ [e ≫ e- ⇒ : (~CList . τs)]] + [⊢ [cmp ≫ cmp- ⇐ : (C→ (U . τs) (U . τs) Bool)]] + -------- + [⊢ [_ ≫ (ro:sort e- cmp-) ⇒ : (CListof (U . τs))]]] + [(_ e cmp) ≫ + [⊢ [e ≫ e- ⇒ : (~U* (~CList τ ...) ...)]] + [⊢ [cmp ≫ cmp- ⇐ : (C→ (U τ ... ...) (U τ ... ...) Bool)]] + -------- + [⊢ [_ ≫ (ro:sort e- cmp-) ⇒ : (U (CList (U τ ...)) ...)]]]) + +;; --------------------------------- +;; IO and other built-in ops + +(define-named-type-alias CAsserts (CListof Bool)) + +(provide (rosette-typed-out [printf : (Ccase-> (C→ CString CUnit) + (C→ CString Any CUnit) + (C→ CString Any Any CUnit))] + [displayln : (C→ Any CUnit)] + [pretty-print : (C→ Any CUnit)] + [error : (Ccase-> (C→ (CU CString CSymbol) Nothing) + (C→ CSymbol CString Nothing))] + [void : (C→ CUnit)] + + [string-length : (C→ CString CNat)] + + [equal? : (C→ Any Any Bool)] + [eq? : (C→ Any Any Bool)] + [distinct? : (Ccase-> (C→ Bool) + (C→ Any Bool) + (C→ Any Any Bool) + (C→ Any Any Any Bool) + (C→ Any Any Any Any Bool) + (C→ Any Any Any Any Any Bool) + (C→ Any Any Any Any Any Any Bool))] + + [pi : CNum] + + [add1 : (Ccase-> (C→ CNegInt (CU CNegInt CZero)) + (C→ NegInt (U NegInt Zero)) + (C→ CZero CPosInt) + (C→ Zero PosInt) + (C→ CPosInt CPosInt) + (C→ PosInt PosInt) + (C→ CNat CPosInt) + (C→ Nat PosInt) + (C→ CInt CInt) + (C→ Int Int))] + [sub1 : (Ccase-> (C→ CNegInt CNegInt) + (C→ NegInt NegInt) + (C→ CZero CNegInt) + (C→ Zero NegInt) + (C→ CPosInt CNat) + (C→ PosInt Nat) + (C→ CNat CInt) + (C→ Nat Int) + (C→ CInt CInt) + (C→ Int Int))] + [+ : (Ccase-> (C→ CZero) + (C→ CNat CNat CNat) + (C→ CNat CNat CNat CNat) + (C→ CNat CNat CNat CNat CNat) + (C→ Nat Nat Nat) + (C→ Nat Nat Nat Nat) + (C→ Nat Nat Nat Nat Nat) + (C→ CInt CInt CInt) + (C→ CInt CInt CInt CInt) + (C→ CInt CInt CInt CInt CInt) + (C→ Int Int Int) + (C→ Int Int Int Int) + (C→ Int Int Int Int Int) + (C→ CNum CNum CNum) + (C→ CNum CNum CNum CNum) + (C→ CNum CNum CNum CNum CNum) + (C→ Num Num Num) + (C→ Num Num Num Num) + (C→ Num Num Num Num Num))] + [- : (Ccase-> (C→ CInt CInt) + (C→ CInt CInt CInt) + (C→ CInt CInt CInt CInt) + (C→ CInt CInt CInt CInt CInt) + (C→ Int Int Int) + (C→ Int Int Int Int) + (C→ Int Int Int Int Int) + (C→ CNum CNum CNum) + (C→ CNum CNum CNum CNum) + (C→ CNum CNum CNum CNum CNum) + (C→ Num Num Num) + (C→ Num Num Num Num) + (C→ Num Num Num Num Num))] + [* : (Ccase-> (C→ CNat CNat CNat) + (C→ CNat CNat CNat CNat) + (C→ CNat CNat CNat CNat CNat) + (C→ Nat Nat Nat) + (C→ Nat Nat Nat Nat) + (C→ Nat Nat Nat Nat Nat) + (C→ CInt CInt CInt) + (C→ CInt CInt CInt CInt) + (C→ CInt CInt CInt CInt CInt) + (C→ Int Int Int) + (C→ Int Int Int Int) + (C→ Int Int Int Int Int) + (C→ CNum CNum CNum) + (C→ CNum CNum CNum CNum) + (C→ CNum CNum CNum CNum CNum) + (C→ Num Num Num) + (C→ Num Num Num Num) + (C→ Num Num Num Num Num))] + [/ : (Ccase-> (C→ CNum CNum) + (C→ CNum CNum CNum) + (C→ CNum CNum CNum CNum) + (C→ Num Num) + (C→ Num Num Num) + (C→ Num Num Num Num))] + [= : (Ccase-> (C→ CNum CNum CBool) + (C→ CNum CNum CNum CBool) + (C→ Num Num Bool) + (C→ Num Num Num Bool))] + [< : (Ccase-> (C→ CNum CNum CBool) + (C→ CNum CNum CNum CBool) + (C→ Num Num Bool) + (C→ Num Num Num Bool))] + [> : (Ccase-> (C→ CNum CNum CBool) + (C→ CNum CNum CNum CBool) + (C→ Num Num Bool) + (C→ Num Num Num Bool))] + [<= : (Ccase-> (C→ CNum CNum CBool) + (C→ CNum CNum CNum CBool) + (C→ Num Num Bool) + (C→ Num Num Num Bool))] + [>= : (Ccase-> (C→ CNum CNum CBool) + (C→ CNum CNum CNum CBool) + (C→ Num Num Bool) + (C→ Num Num Num Bool))] + + [abs : (Ccase-> (C→ CPosInt CPosInt) + (C→ PosInt PosInt) + (C→ CZero CZero) + (C→ Zero Zero) + (C→ CNegInt CPosInt) + (C→ NegInt PosInt) + (C→ CInt CInt) + (C→ Int Int) + (C→ CNum CNum) + (C→ Num Num))] + + [max : (Ccase-> (C→ CInt CInt CInt) + (C→ CInt CInt CInt CInt) + (C→ CNum CNum CNum) + (C→ CNum CNum CNum CNum) + (C→ Int Int Int) + (C→ Int Int Int Int) + (C→ Num Num Num) + (C→ Num Num Num Num))] + [min : (Ccase-> (C→ CInt CInt CInt) + (C→ CInt CInt CInt CInt) + (C→ CNum CNum CNum) + (C→ CNum CNum CNum CNum) + (C→ Int Int Int) + (C→ Int Int Int Int) + (C→ Num Num Num) + (C→ Num Num Num Num))] + ;; out type for these fns must be CNum, because of +inf.0 and +nan.0 + [floor : (Ccase-> (C→ CNum CNum) + (C→ Num Num))] + [ceiling : (Ccase-> (C→ CNum CNum) + (C→ Num Num))] + [truncate : (Ccase-> (C→ CNum CNum) + (C→ Num Num))] + [sgn : (Ccase-> (C→ CZero CZero) + (C→ Zero Zero) + (C→ CInt CInt) + (C→ Int Int) + (C→ CNum CNum) + (C→ Num Num))] + + [expt : (Ccase-> (C→ CNum CZero CPosInt) + (C→ Num Zero PosInt) + (C→ CInt CInt CInt) + (C→ Int Int Int) + (C→ CNum CNum CNum) + (C→ Num Num Num))] + + [not : (C→ Any Bool)] + [xor : (C→ Any Any Any)] + [false? : (C→ Any Bool)] + + [true : CTrue] + [false : CFalse] + [real->integer : (C→ Num Int)] + [string? : (C→ Any Bool)] + [number? : (C→ Any Bool)] + [positive? : (Ccase-> (C→ CNum CBool) + (C→ Num Bool))] + [negative? : (Ccase-> (C→ CNum CBool) + (C→ Num Bool))] + [zero? : (Ccase-> (C→ CNum CBool) + (C→ Num Bool))] + [even? : (Ccase-> (C→ CInt CBool) + (C→ Int Bool))] + [odd? : (Ccase-> (C→ CInt CBool) + (C→ Int Bool))] + [inexact->exact : (Ccase-> (C→ CNum CNum) + (C→ Num Num))] + [exact->inexact : (Ccase-> (C→ CNum CNum) + (C→ Num Num))] + [quotient : (Ccase-> (C→ CInt CInt CInt) + (C→ Int Int Int))] + [remainder : (Ccase-> (C→ CInt CInt CInt) + (C→ Int Int Int))] + [modulo : (Ccase-> (C→ CInt CInt CInt) + (C→ Int Int Int))] + + ;; rosette-specific + [pc : (C→ Bool)] + [asserts : (C→ CAsserts)] + [clear-asserts! : (C→ CUnit)])) + +;; --------------------------------- +;; more built-in ops + +;(define-rosette-primop boolean? : (C→ Any Bool)) +(define-typed-syntax boolean? + [_:id ≫ + -------- + [⊢ [_ ≫ (mark-solvablem + (add-typeform + ro:boolean? + Bool)) + ⇒ : (C→ Any Bool)]]] + [(_ e) ≫ + [⊢ [e ≫ e- ⇒ : ty]] + -------- + [⊢ [_ ≫ (ro:boolean? e-) ⇒ : #,(if (concrete? #'ty) #'CBool #'Bool)]]]) + +;(define-rosette-primop integer? : (C→ Any Bool)) +(define-typed-syntax integer? + [_:id ≫ + -------- + [⊢ [_ ≫ (mark-solvablem + (add-typeform + ro:integer? + Int)) + ⇒ : (C→ Any Bool)]]] + [(_ e) ≫ + [⊢ [e ≫ e- ⇒ : ty]] + -------- + [⊢ [_ ≫ (ro:integer? e-) ⇒ : #,(if (concrete? #'ty) #'CBool #'Bool)]]]) + +;(define-rosette-primop real? : (C→ Any Bool)) +(define-typed-syntax real? + [_:id ≫ + -------- + [⊢ [_ ≫ (mark-solvablem + (add-typeform + ro:real? + Num)) ⇒ : (C→ Any Bool)]]] + [(_ e) ≫ + [⊢ [e ≫ e- ⇒ : ty]] + -------- + [⊢ [_ ≫ (ro:real? e-) ⇒ : #,(if (concrete? #'ty) #'CBool #'Bool)]]]) + +(define-typed-syntax time + [(_ e) ≫ + [⊢ [e ≫ e- ⇒ : ty]] + -------- + [⊢ [_ ≫ (ro:time e-) ⇒ : ty]]]) + +;; --------------------------------- +;; mutable boxes + +(define-typed-syntax box + [(_ e) ≫ + [⊢ [e ≫ e- ⇒ : τ]] + -------- + [⊢ [_ ≫ (ro:box e-) ⇒ : (CMBoxof τ)]]]) + +(define-typed-syntax box-immutable + [(_ e) ≫ + [⊢ [e ≫ e- ⇒ : τ]] + -------- + [⊢ [_ ≫ (ro:box-immutable e-) ⇒ : (CIBoxof τ)]]]) + +(define-typed-syntax unbox + [(_ e) ≫ + [⊢ [e ≫ e- ⇒ : (~or (~CMBoxof τ) (~CIBoxof τ))]] + -------- + [⊢ [_ ≫ (ro:unbox e-) ⇒ : τ]]] + [(_ e) ≫ + [⊢ [e ≫ e- ⇒ : (~U* (~and (~or (~CMBoxof τ) (~CIBoxof τ))) ...)]] + -------- + [⊢ [_ ≫ (ro:unbox e-) ⇒ : (U τ ...)]]]) + +;; TODO: implement multiple values +;; result type should be (Valuesof ty CAsserts) +(define-typed-syntax with-asserts + [(_ e) ≫ + [⊢ [e ≫ e- ⇒ : ty]] + -------- + [⊢ [_ ≫ (ro:with-asserts e-) ⇒ : ty]]]) + +(provide (rosette-typed-out + [term-cache + : (Ccase-> (C→ (CHashTable Any Any)) + (C→ (CHashTable Any Any) CUnit))] + [clear-terms! + : (Ccase-> (C→ CUnit) + (C→ CFalse CUnit) + (C→ (CListof Any) CUnit))])) ; list of terms + +;; --------------------------------- +;; BV Types and Operations + +;; this must be a macro in order to support Racket's overloaded set/get +;; parameter patterns +(define-typed-syntax current-bitwidth + [_:id ≫ + -------- + [⊢ [_ ≫ ro:current-bitwidth ⇒ : (CParamof (CU CFalse CPosInt))]]] + [(_) ≫ + -------- + [⊢ [_ ≫ (ro:current-bitwidth) ⇒ : (CU CFalse CPosInt)]]] + [(_ e) ≫ + [⊢ [e ≫ e- ⇐ : (CU CFalse CPosInt)]] + -------- + [⊢ [_ ≫ (ro:current-bitwidth e-) ⇒ : CUnit]]]) + +(define-named-type-alias BV (add-predm (U CBV) ro:bv?)) +(define-symbolic-named-type-alias BVPred (C→ Any Bool) #:pred lifted-bitvector?) +(define-named-type-alias BVMultiArgOp (Ccase-> (C→ BV BV BV) + (C→ BV BV BV BV))) + +(provide (rosette-typed-out [bv : (Ccase-> (C→ CInt CBVPred CBV) + (C→ CInt CPosInt CBV))] + [bv? : (C→ Any Bool)] + + [bveq : (C→ BV BV Bool)] + [bvslt : (C→ BV BV Bool)] + [bvult : (C→ BV BV Bool)] + [bvsle : (C→ BV BV Bool)] + [bvule : (C→ BV BV Bool)] + [bvsgt : (C→ BV BV Bool)] + [bvugt : (C→ BV BV Bool)] + [bvsge : (C→ BV BV Bool)] + [bvuge : (C→ BV BV Bool)] + + [bvnot : (C→ BV BV)] + + [bvand : (C→ BV BV BV)] + [bvor : (C→ BV BV BV)] + [bvxor : (C→ BV BV BV)] + + [bvshl : (C→ BV BV BV)] + [bvlshr : (C→ BV BV BV)] + [bvashr : (C→ BV BV BV)] + [bvneg : (C→ BV BV)] + + [bvadd : BVMultiArgOp] + [bvsub : BVMultiArgOp] + [bvmul : BVMultiArgOp] + + [bvsdiv : (C→ BV BV BV)] + [bvudiv : (C→ BV BV BV)] + [bvsrem : (C→ BV BV BV)] + [bvurem : (C→ BV BV BV)] + [bvsmod : (C→ BV BV BV)] + + [concat : BVMultiArgOp] + [extract : (C→ Int Int BV BV)] + [sign-extend : (C→ BV CBVPred BV)] + [zero-extend : (C→ BV BVPred BV)] + + [bitvector->integer : (C→ BV Int)] + [bitvector->natural : (C→ BV Nat)] + [integer->bitvector : (C→ Int BVPred BV)] + + [bitvector-size : (C→ CBVPred CPosInt)])) + +;(define-rosette-primop bitvector : (C→ CPosInt CBVPred)) +(define-typed-syntax bitvector + [_:id ≫ + -------- + [⊢ [_ ≫ ro:bitvector ⇒ : (C→ CPosInt CBVPred)]]] + [(_ n) ≫ + [⊢ [n ≫ n- ⇐ : CPosInt]] + -------- + [⊢ [_ ≫ (mark-solvablem + (add-typeform + (ro:bitvector n-) + BV)) ⇒ : CBVPred]]]) + +;; bitvector? can produce type CFalse if input does not have type (C→ Any Bool) +;; result is always CBool, since anything symbolic returns false +;(define-rosette-primop bitvector? : (C→ Any Bool)) +(define-typed-syntax bitvector? + [_:id ≫ + -------- + [⊢ [_ ≫ ro:bitvector? ⇒ : (C→ Any CBool)]]] + [(_ e) ≫ + [⊢ [e ≫ e- ⇐ : (C→ Any Bool)]] + -------- + [⊢ [_ ≫ (ro:bitvector? e-) ⇒ : CBool]]] + [(_ e) ≫ + [⊢ [e ≫ e- ⇒ : _]] + -------- + [⊢ [_ ≫ (ro:bitvector? e-) ⇒ : CFalse]]]) + +;; --------------------------------- +;; Uninterpreted functions + +(define-typed-syntax ~> + [(_ pred? ...+ out) ≫ + [⊢ [pred? ≫ pred?- (⇒ : _) (⇒ typefor ty) (⇒ solvable? s?) (⇒ function? f?)]] ... + [⊢ [out ≫ out- (⇒ : _) (⇒ typefor ty-out) (⇒ solvable? out-s?) (⇒ function? out-f?)]] + #:fail-unless (stx-andmap syntax-e #'(s? ... out-s?)) + (format "Expected a Rosette-solvable type, given ~a." + (syntax->datum #'(pred? ... out))) + #:fail-when (stx-ormap syntax-e #'(f? ... out-f?)) + (format "Expected a non-function Rosette type, given ~a." + (syntax->datum #'(pred? ... out))) + -------- + [⊢ [_ ≫ (mark-solvablem + (mark-functionm + (add-typeform + (ro:~> pred?- ... out-) + (→ ty ... ty-out)))) + ⇒ : (C→ Any Bool)]]]) + +(provide (rosette-typed-out [fv? : (C→ Any Bool)])) + +;; function? can produce type CFalse if input does not have type (C→ Any Bool) +;; result is always CBool, since anything symbolic returns false +;(define-rosette-primop function? : (C→ Any Bool)) +(define-typed-syntax function? + [_:id ≫ + -------- + [⊢ [_ ≫ ro:function? ⇒ : (C→ Any CBool)]]] + [(_ e) ≫ + [⊢ [e ≫ e- ⇐ : (C→ Any Bool)]] + -------- + [⊢ [_ ≫ (ro:function? e-) ⇒ : CBool]]] + [(_ e) ≫ + [⊢ [e ≫ e- ⇒ : _]] + -------- + [⊢ [_ ≫ (ro:function? e-) ⇒ : CFalse]]]) + +;; --------------------------------- +;; Logic operators +(provide (rosette-typed-out [! : (C→ Bool Bool)] + [<=> : (C→ Bool Bool Bool)] + [=> : (C→ Bool Bool Bool)])) + +(define-typed-syntax && + [_:id ≫ + -------- + [⊢ [_ ≫ ro:&& ⇒ : + (Ccase-> (C→ Bool) + (C→ Bool Bool) + (C→ Bool Bool Bool))]]] + [(_ e ...) ≫ + [⊢ [e ≫ e- ⇐ : Bool] ...] + -------- + [⊢ [_ ≫ (ro:&& e- ...) ⇒ : Bool]]]) +(define-typed-syntax || + [_:id ≫ + -------- + [⊢ [_ ≫ ro:|| ⇒ : + (Ccase-> (C→ Bool) + (C→ Bool Bool) + (C→ Bool Bool Bool))]]] + [(_ e ...) ≫ + [⊢ [e ≫ e- ⇐ : Bool] ...] + -------- + [⊢ [_ ≫ (ro:|| e- ...) ⇒ : Bool]]]) + +(define-typed-syntax and + [(_) ≫ + -------- + [⊢ [_ ≫ (ro:and) ⇒ : CTrue]]] + [(_ e ...) ≫ + [⊢ [e ≫ e- ⇐ : Bool] ...] + -------- + [⊢ [_ ≫ (ro:and e- ...) ⇒ : Bool]]] + [(_ e ... elast) ≫ + [⊢ [e ≫ e- ⇒ : ty] ...] + [⊢ [elast ≫ elast- ⇒ : ty-last]] + -------- + [⊢ [_ ≫ (ro:and e- ... elast-) ⇒ : (U CFalse ty-last)]]]) +(define-typed-syntax or + [(_) ≫ + -------- + [⊢ [_ ≫ (ro:or) ⇒ : CFalse]]] + [(_ e ...) ≫ + [⊢ [e ≫ e- ⇐ : Bool] ...] + -------- + [⊢ [_ ≫ (ro:or e- ...) ⇒ : Bool]]] + [(_ e ...) ≫ + [⊢ [e ≫ e- ⇒ : ty] ...] + -------- + [⊢ [_ ≫ (ro:or efirst- e- ...) ⇒ : (U ty ...)]]]) +(define-typed-syntax nand + [(_) ≫ + -------- + [⊢ [_ ≫ (ro:nand) ⇒ : CFalse]]] + [(_ e ...) ≫ + [⊢ [e ≫ e- ⇒ : _] ...] + -------- + [⊢ [_ ≫ (ro:nand e- ...) ⇒ : Bool]]]) +(define-typed-syntax nor + [(_) ≫ + -------- + [⊢ [_ ≫ (ro:nor) ⇒ : CTrue]]] + [(_ e ...) ≫ + [⊢ [e ≫ e- ⇒ : _] ...] + -------- + [⊢ [_ ≫ (ro:nor e- ...) ⇒ : Bool]]]) +(define-typed-syntax implies + [(_ e1 e2) ≫ + -------- + [_ ≻ (if e1 e2 (stlc+union:#%datum . #t))]]) + +;; --------------------------------- +;; solver forms + +(define-base-types CSolution CSolver CPict CSyntax) + +(provide (rosette-typed-out [sat? : (C→ Any Bool)] + [unsat? : (C→ Any Bool)] + [solution? : CPred] + [unknown? : CPred] + [sat : (Ccase-> (C→ CSolution) + (C→ (CHashTable Any Any) CSolution))] + [unsat : (Ccase-> (C→ CSolution) + (C→ (CListof Bool) CSolution))] + [unknown : (C→ CSolution)] + [model : (C→ CSolution (CHashTable Any Any))] + [core : (C→ CSolution (U (Listof Any) CFalse))])) + +;(define-rosette-primop forall : (C→ (CListof Any) Bool Bool)) +;(define-rosette-primop exists : (C→ (CListof Any) Bool Bool)) +(define-typed-syntax forall + [(_ vs body) ≫ + ;; TODO: allow U of Constants? + [⊢ [vs ≫ vs- ⇒ : (~CListof ~! ty)]] + #:fail-unless (Constant*? #'ty) + (format "Expected list of symbolic constants, given list of ~a" + (type->str #'ty)) + [⊢ [body ≫ body- ⇐ : Bool]] + -------- + [⊢ [_ ≫ (ro:forall vs- body-) ⇒ : Bool]]] + [(_ vs body) ≫ + [⊢ [vs ≫ vs- ⇒ : (~CList ~! ty ...)]] + #:fail-unless (stx-andmap Constant*? #'(ty ...)) + (format "Expected list of symbolic constants, given list containing: ~a" + (string-join (stx-map type->str #'(ty ...)) ", ")) + [⊢ [body ≫ body- ⇐ : Bool]] + -------- + [⊢ [_ ≫ (ro:forall vs- body-) ⇒ : Bool]]]) +(define-typed-syntax exists + [(_ vs body) ≫ + [⊢ [vs ≫ vs- ⇒ : (~CListof ~! ty)]] + ;; TODO: allow U of Constants? + #:fail-unless (Constant*? #'ty) + (format "Expected list of symbolic constants, given list of ~a" + (type->str #'ty)) + [⊢ [body ≫ body- ⇐ : Bool]] + -------- + [⊢ [_ ≫ (ro:exists vs- body-) ⇒ : Bool]]] + [(_ vs body) ≫ + [⊢ [vs ≫ vs- ⇒ : (~CList ~! ty ...)]] + #:fail-unless (stx-andmap Constant*? #'(ty ...)) + (format "Expected list of symbolic constants, given list containing: ~a" + (string-join (stx-map type->str #'(ty ...)) ", ")) + [⊢ [body ≫ body- ⇐ : Bool]] + -------- + [⊢ [_ ≫ (ro:exists vs- body-) ⇒ : Bool]]]) + +(define-typed-syntax verify + [(_ e) ≫ + [⊢ [e ≫ e- ⇒ : _]] + -------- + [⊢ [_ ≫ (ro:verify e-) ⇒ : CSolution]]] + [(_ #:assume ae #:guarantee ge) ≫ + [⊢ [ae ≫ ae- ⇒ : _]] + [⊢ [ge ≫ ge- ⇒ : _]] + -------- + [⊢ [_ ≫ (ro:verify #:assume ae- #:guarantee ge-) ⇒ : CSolution]]]) + +(define-typed-syntax evaluate + [(_ v s) ≫ + [⊢ [v ≫ v- ⇒ : (~Constant* ty)]] + [⊢ [s ≫ s- ⇐ : CSolution]] + -------- + [⊢ [_ ≫ (ro:evaluate v- s-) ⇒ : ty]]] + [(_ v s) ≫ + [⊢ [v ≫ v- ⇒ : ty]] + [⊢ [s ≫ s- ⇐ : CSolution]] + -------- + [⊢ [_ ≫ (ro:evaluate v- s-) ⇒ : #,(remove-Constant #'ty)]]]) + +;; TODO: enforce list of constants? +(define-typed-syntax synthesize + [(_ #:forall ie #:guarantee ge) ≫ + [⊢ [ie ≫ ie- ⇐ : (CListof Any)]] + [⊢ [ge ≫ ge- ⇒ : _]] + -------- + [⊢ [_ ≫ (ro:synthesize #:forall ie- #:guarantee ge-) ⇒ : CSolution]]] + [(_ #:forall ie #:assume ae #:guarantee ge) ≫ + [⊢ [ie ≫ ie- ⇐ : (CListof Any)]] + [⊢ [ae ≫ ae- ⇒ : _]] + [⊢ [ge ≫ ge- ⇒ : _]] + -------- + [⊢ [_ ≫ (ro:synthesize #:forall ie- #:assume ae- #:guarantee ge-) ⇒ : CSolution]]]) + +(define-typed-syntax solve + [(_ e) ≫ + [⊢ [e ≫ e- ⇒ : _]] + -------- + [⊢ [_ ≫ (ro:solve e-) ⇒ : CSolution]]]) + +(define-typed-syntax optimize + [(_ #:guarantee ge) ≫ + [⊢ [ge ≫ ge- ⇒ : _]] + -------- + [⊢ [_ ≫ (ro:optimize #:guarantee ge-) ⇒ : CSolution]]] + [(_ #:minimize mine #:guarantee ge) ≫ + [⊢ [ge ≫ ge- ⇒ : _]] + [⊢ [mine ≫ mine- ⇐ : (CListof (U Num BV))]] + -------- + [⊢ [_ ≫ (ro:optimize #:minimize mine- #:guarantee ge-) ⇒ : CSolution]]] + [(_ #:maximize maxe #:guarantee ge) ≫ + [⊢ [ge ≫ ge- ⇒ : _]] + [⊢ [maxe ≫ maxe- ⇐ : (CListof (U Num BV))]] + -------- + [⊢ [_ ≫ (ro:optimize #:maximize maxe- #:guarantee ge-) ⇒ : CSolution]]] + [(_ #:minimize mine #:maximize maxe #:guarantee ge) ≫ + [⊢ [ge ≫ ge- ⇒ : _]] + [⊢ [maxe ≫ maxe- ⇐ : (CListof (U Num BV))]] + [⊢ [mine ≫ mine- ⇐ : (CListof (U Num BV))]] + -------- + [⊢ [_ ≫ (ro:optimize #:minimize mine- #:maximize maxe- #:guarantee ge-) ⇒ : CSolution]]] + [(_ #:maximize maxe #:minimize mine #:guarantee ge) ≫ + [⊢ [ge ≫ ge- ⇒ : _]] + [⊢ [maxe ≫ maxe- ⇐ : (CListof (U Num BV))]] + [⊢ [mine ≫ mine- ⇐ : (CListof (U Num BV))]] + -------- + [⊢ [_ ≫ (ro:optimize #:maximize maxe- #:minimize mine- #:guarantee ge-) ⇒ : CSolution]]]) + +;; this must be a macro in order to support Racket's overloaded set/get +;; parameter patterns +(define-typed-syntax current-solver + [_:id ≫ + -------- + [⊢ [_ ≫ ro:current-solver ⇒ : (CParamof CSolver)]]] + [(_) ≫ + -------- + [⊢ [_ ≫ (ro:current-solver) ⇒ : CSolver]]] + [(_ e) ≫ + [⊢ [e ≫ e- ⇐ : CSolver]] + -------- + [⊢ [_ ≫ (ro:current-solver e-) ⇒ : CUnit]]]) + +;(define-rosette-primop gen:solver : CSolver) +(provide (rosette-typed-out + [solver? : CPred] + [solver-assert : (C→ CSolver (CListof Bool) CUnit)] + [solver-clear : (C→ CSolver CUnit)] + [solver-minimize : (C→ CSolver (CListof (U Int Num BV)) CUnit)] + [solver-maximize : (C→ CSolver (CListof (U Int Num BV)) CUnit)] + [solver-check : (C→ CSolver CSolution)] + [solver-debug : (C→ CSolver CSolution)] + [solver-shutdown : (C→ CSolver CUnit)])) +;; this is in rosette/solver/smt/z3 (is not in #lang rosette) +;; make this part of base typed/rosette or separate lib? +;(define-rosette-primop z3 : (C→ CSolver)) + +;; --------------------------------- +;; Reflecting on symbolic values + +(provide (rosette-typed-out + [term? : CPred] + [expression? : CPred] + [constant? : CPred] + [type? : CPred] + [solvable? : CPred] + [union? : CPred])) + +(define-typed-syntax union-contents + [(_ u) ≫ + ;; TODO: can U sometimes be converted to CU? + [⊢ [u ≫ u- ⇒ : (~and τ (~U* _ ...))]] ; input must be symbolic, and not constant + -------- + [⊢ [_ ≫ (ro:union-contents u-) ⇒ : (CListof (CPair Bool τ))]]]) + +;; TODO: add match and match expanders + +;; TODO: should a type-of expression have a solvable stx prop? +(provide (rosette-typed-out [type-of : (Ccase-> (C→ Any CPred) + (C→ Any Any CPred))] + [any/c : (C→ Any CTrue)])) + +(define-typed-syntax for/all + ;; symbolic e + [(_ ([x:id e]) e_body) ≫ + [⊢ [e ≫ e- ⇒ : (~U* τ_x)]] + [() ([x ≫ x- : τ_x]) ⊢ [e_body ≫ e_body- ⇒ : τ_body]] + -------- + [⊢ [_ ≫ (ro:for/all ([x- e-]) e_body-) ⇒ : (U τ_body)]]] + [(_ ([x:id e]) e_body) ≫ + [⊢ [e ≫ e- ⇒ : τ_x]] + [() ([x ≫ x- : τ_x]) ⊢ [e_body ≫ e_body- ⇒ : τ_body]] + -------- + [⊢ [_ ≫ (ro:for/all ([x- e-]) e_body-) ⇒ : (U τ_body)]]]) + +(define-typed-syntax for*/all + [(_ () e_body) ≫ + -------- + [_ ≻ e_body]] + [(_ ([x e] [x_rst e_rst] ...) e_body) ≫ + -------- + [_ ≻ (for/all ([x e]) (for*/all ([x_rst e_rst] ...) e_body))]]) + + +;; --------------------------------- +;; Subtyping + +(begin-for-syntax + (define (sub? t1 t2) + ; need this because recursive calls made with unexpanded types + ;; (define τ1 ((current-type-eval) t1)) + ;; (define τ2 ((current-type-eval) t2)) + ;; (printf "t1 = ~a\n" (syntax->datum t1)) + ;; (printf "t2 = ~a\n" (syntax->datum t2)) + (or + (Any? t2) + ((current-type=?) t1 t2) + (syntax-parse (list t1 t2) + ;; Constant clause must appear before U, ow (Const Int) <: Int wont hold + [((~Constant* ty1) (~Constant* ty2)) + (typecheck? #'ty1 #'ty2)] + [((~Constant* ty) _) + (typecheck? #'ty t2)] + [((~CListof ty1) (~CListof ty2)) + (typecheck? #'ty1 #'ty2)] + [((~CList . tys1) (~CList . tys2)) + (and (stx-length=? #'tys1 #'tys2) + (typechecks? #'tys1 #'tys2))] + [((~CList . tys) (~CListof ty)) + (for/and ([t (stx->list #'tys)]) + (typecheck? t #'ty))] + ;; vectors, only immutable vectors are invariant + [((~CIVectorof ty1) (~CIVectorof ty2)) + (typecheck? #'ty1 #'ty2)] + [((~CIBoxof ty1) (~CIBoxof ty2)) + (typecheck? #'ty1 #'ty2)] + [((~CPair ty1a ty1b) (~CPair ty2a ty2b)) + (and (typecheck? #'ty1a #'ty2a) + (typecheck? #'ty1b #'ty2b))] + ; 2 U types, subtype = subset + [((~CU* . ts1) _) + (for/and ([t (stx->list #'ts1)]) + (typecheck? t t2))] + [((~U* . ts1) _) + (and + (not (concrete? t2)) + (for/and ([t (stx->list #'ts1)]) + (typecheck? t t2)))] + ; 1 U type, 1 non-U type. subtype = member + [(_ (~CU* . ts2)) + #:when (not (or (U*? t1) (CU*? t1))) + (for/or ([t (stx->list #'ts2)]) + (typecheck? t1 t))] + [(_ (~U* . ts2)) + #:when (not (or (U*? t1) (CU*? t1))) + (for/or ([t (stx->list #'ts2)]) + (typecheck? t1 t))] + ; 2 case-> types, subtype = subset + [(_ (~Ccase-> . ts2)) + (for/and ([t (stx->list #'ts2)]) + (typecheck? t1 t))] + ; 1 case-> , 1 non-case-> + [((~Ccase-> . ts1) _) + (for/or ([t (stx->list #'ts1)]) + (typecheck? t t2))] + [((~C→ s1 ... s2) (~C→ t1 ... t2)) + (and (typechecks? #'(t1 ...) #'(s1 ...)) + (typecheck? #'s2 #'t2))] + [_ #f]))) + (current-sub? sub?) + (current-typecheck-relation sub?) + (define (subs? τs1 τs2) + (and (stx-length=? τs1 τs2) + (stx-andmap (current-sub?) τs1 τs2)))) diff --git a/turnstile/examples/tests/rosette/rosette3/bv-ref-tests.rkt b/turnstile/examples/tests/rosette/rosette3/bv-ref-tests.rkt new file mode 100644 index 0000000..172410a --- /dev/null +++ b/turnstile/examples/tests/rosette/rosette3/bv-ref-tests.rkt @@ -0,0 +1,404 @@ +#lang s-exp "../../../rosette/bv3.rkt" +(require syntax/parse/define + (only-in racket/base for-syntax) (for-syntax racket/base)) +(require "../../rackunit-typechecking.rkt") + +; The 25 Hacker's Delight benchmarks from the following paper: +; Sumit Gulwani, Susmit Jha, Ashish Tiwari, and Ramarathnam Venkatesan. +; 2011. Synthesis of loop-free programs. In Proceedings of the 32nd ACM +; SIGPLAN Conference on Programming Language Design and Implementation (PLDI '11). +; +; The first 20 benchmarks are also used in the SyGuS competition: http://www.sygus.org + +(current-bvpred (bitvector 32)) + +(check-type (thunk (bv 1)) : (C→ BV)) + +; Constants. +(define bv1 (thunk (bv 1))) +(define bv2 (thunk (bv 2))) +(define bvsz (thunk (bv (sub1 (bitvector-size (current-bvpred)))))) + +(check-type bv1 : (C→ BV)) +(check-type (bv1) : BV -> (bv 1)) +(check-type ((bitvector 4) (bv1)) : Bool -> #f) +(check-type ((bitvector 32) (bv1)) : Bool -> #t) +(check-type bv2 : (C→ BV)) +(check-type bvsz : (C→ BV)) + +(check-type (bvsub (bv 1) (bv1)) : BV -> (bv 0)) +(check-type ((bitvector 32) (bvsub (bv 1) (bv1))) : Bool -> #t) + +; Mask off the rightmost 1-bit. +(define (p1 [x : BV] -> BV) + (let* ([o1 (bvsub x (bv 1))] + [o2 (bvand x o1)]) + o2)) + +(check-type (p1 (bv 1)) : BV -> (bv 0)) +(check-type ((bitvector 32) (p1 (bv 1))) : Bool -> #t) + +; Test whether an unsigned integer is of the form 2^n-1. +(define (p2 [x : BV] -> BV) + (let* ([o1 (bvadd x (bv 1))] + [o2 (bvand x o1)]) + o2)) + +; Isolate the right most 1-bit. +(define (p3 [x : BV] -> BV) + (let* ([o1 (bvneg x)] + [o2 (bvand x o1)]) + o2)) + +; Form a mask that identifies the rightmost 1-bit and trailing 0s. +(define (p4 [x : BV] -> BV) + (let* ([o1 (bvsub x (bv 1))] + [o2 (bvxor x o1)]) + o2)) + +; Right propagate rightmost 1-bit. +(define (p5 [x : BV] -> BV) + (let* ([o1 (bvsub x (bv 1))] + [o2 (bvor x o1)]) + o2)) + +; Turn on the right-most 0-bit in a word. +(define (p6 [x : BV] -> BV) + (let* ([o1 (bvadd x (bv 1))] + [o2 (bvor x o1)]) + o2)) + +; Isolate the right most 0 bit of a given bitvector. +(define (p7 [x : BV] -> BV) + (let* ([o1 (bvnot x)] + [o2 (bvadd x (bv 1))] + [o3 (bvand o1 o2)]) + o3)) + +; Form a mask that identifies the trailing 0s. +(define (p8 [x : BV] -> BV) + (let* ([o1 (bvsub x (bv 1))] + [o2 (bvnot x)] + [o3 (bvand o1 o2)]) + o3)) + +; Absolute value function. +(define (p9 [x : BV] -> BV) + (let* ([o1 (bvashr x (bv 31))] + [o2 (bvxor x o1)] + [o3 (bvsub o2 o1)]) + o3)) + +; Test if nlz(x) == nlz(y) where nlz is number of leading zeroes. +(define (p10 [x : BV] [y : BV] -> BV) + (let* ([o1 (bvand x y)] + [o2 (bvxor x y)] + [o3 (bvule o2 o1)]) + o3)) + +; Test if nlz(x) < nlz(y) where nlz is number of leading zeroes. +(define (p11 [x : BV] [y : BV] -> BV) + (let* ([o1 (bvnot y)] + [o2 (bvand x o1)] + [o3 (bvugt o2 y)]) + o3)) + +; Test if nlz(x) <= nlz(y) where nlz is number of leading zeroes. +(define (p12 [x : BV] [y : BV] -> BV) + (let* ([o1 (bvnot x)] + [o2 (bvand y o1)] + [o3 (bvule o2 x)]) + o3)) + +; Sign function. +(define (p13 [x : BV] -> BV) + (let* ([o1 (bvneg x)] + [o2 (bvlshr o1 (bv 31))] + [o3 (bvashr x (bv 31))] + [o4 (bvor o2 o3)]) + o4)) + +; Floor of average of two integers without over-flowing. +(define (p14 [x : BV] [y : BV] -> BV) + (let* ([o1 (bvand x y)] + [o2 (bvxor x y)] + [o3 (bvlshr o2 (bv 1))] + [o4 (bvadd o1 o3)]) + o4)) + +; Ceil of average of two integers without over-flowing. +(define (p15 [x : BV] [y : BV] -> BV) + (let* ([o1 (bvor x y)] + [o2 (bvxor x y)] + [o3 (bvlshr o2 (bv 1))] + [o4 (bvsub o1 o3)]) + o4)) + +; The max function. +(define (p16 [x : BV] [y : BV] -> BV) + (if (equal? (bv 1) (bvsge x y)) x y)) + +; Turn-off the rightmost contiguous string of 1 bits. +(define (p17 [x : BV] -> BV) + (let* ([o1 (bvsub x (bv 1))] + [o2 (bvor x o1)] + [o3 (bvadd o2 (bv 1))] + [o4 (bvand o3 x)]) + o4)) + +; Test whether an unsigned integer is of the form 2^n. +(define (p18 [x : BV] -> BV) + (let* ([o1 (bvsub x (bv 1))] + [o2 (bvand o1 x)] + [o3 (bvredor x)] + [o4 (bvredor o2)] + [o5 (bvnot o4)] + [o6 (bvand o5 o3)]) + o6)) + +; Exchanging 2 fields A and B of the same register +; x where m is mask which identifies field B and k +; is number of bits from end of A to start of B. +(define (p19 [x : BV] [m : BV] [k : BV] -> BV) + (let* ([o1 (bvlshr x k)] + [o2 (bvxor x o1)] + [o3 (bvand o2 m)] + [o4 (bvshl o3 k)] + [o5 (bvxor o4 o3)] + [o6 (bvxor o5 x)]) + o6)) + +; Next higher unsigned number with the same number of 1 bits. +(define (p20 [x : BV] -> BV) + (let* ([o1 (bvneg x)] + [o2 (bvand x o1)] + [o3 (bvadd x o2)] + [o4 (bvxor x o2)] + [o5 (bvlshr o4 (bv 2))] + [o6 (bvudiv o5 o2)] + [o7 (bvor o6 o3)]) + o7)) + +; Cycling through 3 values a, b, c. +(define (p21 [x : BV] [a : BV] [b : BV] [c : BV] -> BV) + (let* ([o1 (bveq x c)] + [o2 (bvneg o1)] + [o3 (bvxor a c)] + [o4 (bveq x a)] + [o5 (bvneg o4)] + [o6 (bvxor b c)] + [o7 (bvand o2 o3)] + [o8 (bvand o5 o6)] + [o9 (bvxor o7 o8)] + [o10 (bvxor o9 c)]) + o10)) + +; Compute parity. +(define (p22 [x : BV] -> BV) + (let* ([o1 (bvlshr x (bv 1))] + [o2 (bvxor o1 x)] + [o3 (bvlshr o2 (bv 2))] + [o4 (bvxor o2 o3)] + [o5 (bvand o4 (bv #x11111111))] + [o6 (bvmul o5 (bv #x11111111))] + [o7 (bvlshr o6 (bv 28))] + [o8 (bvand o7 (bv 1))]) + o8)) + +; Counting number of bits. +(define (p23 [x : BV] -> BV) + (let* ([o1 (bvlshr x (bv 1))] + [o2 (bvand o1 (bv #x55555555))] + [o3 (bvsub x o2)] + [o4 (bvand o3 (bv #x33333333))] + [o5 (bvlshr o3 (bv 2))] + [o6 (bvand o5 (bv #x33333333))] + [o7 (bvadd o4 o6)] + [o8 (bvlshr o7 (bv 4))] + [o9 (bvadd o8 o7)] + [o10 (bvand o9 (bv #x0f0f0f0f))]) + o10)) + +; Round up to the next higher power of 2. +(define (p24 [x : BV] -> BV) + (let* ([o1 (bvsub x (bv 1))] + [o2 (bvlshr o1 (bv 1))] + [o3 (bvor o1 o2)] + [o4 (bvlshr o3 (bv 2))] + [o5 (bvor o3 o4)] + [o6 (bvlshr o5 (bv 4))] + [o7 (bvor o5 o6)] + [o8 (bvlshr o7 (bv 8))] + [o9 (bvor o7 o8)] + [o10 (bvlshr o9 (bv 16))] + [o11 (bvor o9 o10)] + [o12 (bvadd o11 (bv 1))]) + o12)) + +; Compute higher order half of product of x and y. +(define (p25 [x : BV] [y : BV] -> BV) + (let* ([o1 (bvand x (bv #xffff))] + [o2 (bvlshr x (bv 16))] + [o3 (bvand y (bv #xffff))] + [o4 (bvlshr y (bv 16))] + [o5 (bvmul o1 o3)] + [o6 (bvmul o2 o3)] + [o7 (bvmul o1 o4)] + [o8 (bvmul o2 o4)] + [o9 (bvlshr o5 (bv 16))] + [o10 (bvadd o6 o9)] + [o11 (bvand o10 (bv #xffff))] + [o12 (bvlshr o10 (bv 16))] + [o13 (bvadd o7 o11)] + [o14 (bvlshr o13 (bv 16))] + [o15 (bvadd o14 o12)] + [o16 (bvadd o15 o8)]) + o16)) + + (define-simple-macro (check-equal/rand/bv f) + #:with out (syntax/loc this-syntax + (check-equal/rand f #:process (λ ([x : CInt]) (bv x)))) + out) + +;; Mask off the rightmost 1-bit. < 1 sec. +(define-fragment (p1* x) + #:implements p1 + #:library (bvlib [{bv1 bvand bvsub} 1])) + +(check-equal/rand/bv p1) + +; Test whether an unsigned integer is of the form 2^n-1. < 1 sec. +(define-fragment (p2* x) + #:implements p2 + #:library (bvlib [{bv1 bvand bvadd} 1])) + +(check-equal/rand/bv p2) + +; Isolate the right most 1-bit. < 1 sec. +(define-fragment (p3* x) + #:implements p3 + #:library (bvlib [{bvand bvneg} 1])) + +(check-equal/rand/bv p3) + +;; Form a mask that identifies the rightmost 1-bit and trailing 0s. < 1 sec. +(define-fragment (p4* x) + #:implements p4 + #:library (bvlib [{bv1 bvsub bvxor} 1])) + +(check-equal/rand/bv p4) + +; Right propagate rightmost 1-bit. < 1 sec. +(define-fragment (p5* x) + #:implements p5 + #:library (bvlib [{bv1 bvsub bvor} 1])) + +(check-equal/rand/bv p5) + +; Turn on the right-most 0-bit in a word. < 1 sec. +(define-fragment (p6* x) + #:implements p6 + #:library (bvlib [{bv1 bvor bvadd} 1])) + +(check-equal/rand/bv p6) + +; Isolate the right most 0 bit of a given bitvector. < 1 sec. +(define-fragment (p7* x) + #:implements p7 + #:library (bvlib [{bvand bvadd bvnot bv1} 1])) + +(check-equal/rand/bv p7) + +; Form a mask that identifies the trailing 0s. < 1 sec. +(define-fragment (p8* x) + #:implements p8 + #:library (bvlib [{bv1 bvsub bvand bvnot} 1])) + +(check-equal/rand/bv p8) + +; Absolute value function. ~ 1 sec. +(define-fragment (p9* x) + #:implements p9 + #:library (bvlib [{bvsz bvsub bvxor bvashr} 1])) + +(check-equal/rand/bv p9) + +; Test if nlz(x) == nlz(y) where nlz is number of leading zeroes. < 1 sec. +(define-fragment (p10* x y) + #:implements p10 + #:library (bvlib [{bvand bvxor bvule} 1])) + +(check-equal/rand/bv p10) + +; Test if nlz(x) < nlz(y) where nlz is number of leading zeroes. < 1 sec. +(define-fragment (p11* x y) + #:implements p11 + #:library (bvlib [{bvnot bvand bvugt} 1])) + +(check-equal/rand/bv p11) + +; Test if nlz(x) <= nlz(y) where nlz is number of leading zeroes. < 1 sec. +(define-fragment (p12* x y) + #:implements p12 + #:library (bvlib [{bvand bvnot bvule} 1])) + +(check-equal/rand/bv p12) + +; Sign function. ~ 1.4 sec. +(define-fragment (p13* x) + #:implements p13 + #:library (bvlib [{bvsz bvneg bvlshr bvashr bvor} 1]) + #:minbv 32) + +(check-equal/rand/bv p13) + +; Floor of average of two integers without over-flowing. ~ 2.5 sec. +(define-fragment (p14* x y) + #:implements p14 + #:library (bvlib [{bv1 bvand bvlshr bvxor bvadd} 1])) + +(check-equal/rand/bv p14) + +; Ceil of average of two integers without over-flowing. ~ 1 sec. +(define-fragment (p15* x y) + #:implements p15 + #:library (bvlib [{bv1 bvor bvlshr bvxor bvsub} 1])) + +(check-equal/rand/bv p15) + +; Compute max of two integers. Bug in the PLDI'11 paper: bvuge should be bvge. +; ~ 1.3 sec. +(define-fragment (p16* x y) + #:implements p16 + #:library (bvlib [{bvneg bvsge bvand} 1] [{bvxor} 2])) + +(check-equal/rand/bv p16) + +; Turn-off the rightmost contiguous string of 1 bits. ~ 1.8 sec. +(define-fragment (p17* x) + #:implements p17 + #:library (bvlib [{bv1 bvand bvor bvadd bvsub} 1])) + +(check-equal/rand/bv p17) + +; Test whether an unsigned integer is of the form 2^n. ~ 1.6 sec. +(define-fragment (p18* x) + #:implements p18 + #:library (bvlib [{bvand bvredor} 2] [{bvsub bvnot bv1} 1])) + +(check-equal/rand/bv p18) + +; x where m is mask which identifies field B and k +; is number of bits from end of A to start of B. ~ 3.5 sec. +(define-fragment (p19* x m k) + #:implements p19 + #:library (bvlib [{bvlshr bvshl bvand} 1] [{bvxor} 3])) + +(check-equal/rand/bv p19) + +; Next higher unsigned number with the same number of 1 bits. ~ 600 sec. +(define-fragment (p20* x) + #:implements p20 + #:library (bvlib [{bv2 bvneg bvand bvadd bvxor bvlshr bvudiv bvor} 1])) + +(check-equal/rand/bv p20) diff --git a/turnstile/examples/tests/rosette/rosette3/bv-tests.rkt b/turnstile/examples/tests/rosette/rosette3/bv-tests.rkt new file mode 100644 index 0000000..df27815 --- /dev/null +++ b/turnstile/examples/tests/rosette/rosette3/bv-tests.rkt @@ -0,0 +1,30 @@ +#lang s-exp "../../../rosette/bv3.rkt" +(require "../../rackunit-typechecking.rkt") + +(check-type current-bvpred : (CParamof CBVPred)) +(check-type (current-bvpred) : BVPred -> (bitvector 4)) +(check-type (current-bvpred (bitvector 5)) : CUnit -> (void)) +(check-type (current-bvpred) : BVPred -> (bitvector 5)) +(check-type (current-bvpred (bitvector 4)) : CUnit -> (void)) + +(check-type (bv 1) : BV) +(check-type ((bitvector 4) (bv 1)) : Bool -> #t) +(check-type ((bitvector 1) (bv 1)) : Bool -> #f) +(check-type (bv 2 (bitvector 3)) : BV) +(check-type ((bitvector 3) (bv 2 (bitvector 3))) : Bool -> #t) + +(check-type (bv*) : BV) + +(check-type (if 1 (bv 1) (bv 0)) : BV -> (bv 1)) +(check-type (if #f (bv 1) (bv 0)) : BV -> (bv 0)) +(define-symbolic i integer?) +(define-symbolic b boolean?) +(check-type (if i (bv 1) (bv 0)) : BV -> (bv 1)) +(check-type (if b (bv 1) (bv 0)) : BV -> (if b (bv 1) (bv 0))) + +(check-type (bvredor (bv 1)) : BV) +(check-type (bvredand (bv 1)) : BV) + +(check-type bveq : (→ BV BV BV)) +(check-type (bveq (bv 1) (bv 1)) : BV -> (bv 1)) +(check-type (bveq (bv 1) (bv 0)) : BV -> (bv 0)) diff --git a/turnstile/examples/tests/rosette/rosette3/check-type+asserts.rkt b/turnstile/examples/tests/rosette/rosette3/check-type+asserts.rkt new file mode 100644 index 0000000..a92411e --- /dev/null +++ b/turnstile/examples/tests/rosette/rosette3/check-type+asserts.rkt @@ -0,0 +1,17 @@ +#lang racket/base + +(provide check-type+asserts) + +(require turnstile/turnstile + "../check-asserts.rkt" + (only-in "../../../rosette/rosette3.rkt" CListof Bool CUnit)) + +(define-typed-syntax check-type+asserts #:datum-literals (: ->) + [(_ e : τ-expected -> v asserts) ≫ + [⊢ [e ≫ e- ⇐ : τ-expected]] + -------- + [⊢ [_ ≫ (check-equal?/asserts e- + (add-expected v τ-expected) + (add-expected asserts (CListof Bool))) + ⇒ : CUnit]]]) + diff --git a/turnstile/examples/tests/rosette/rosette3/fsm-test.rkt b/turnstile/examples/tests/rosette/rosette3/fsm-test.rkt new file mode 100644 index 0000000..6a9c944 --- /dev/null +++ b/turnstile/examples/tests/rosette/rosette3/fsm-test.rkt @@ -0,0 +1,43 @@ +#lang s-exp "../../rosette/fsm3.rkt" +(require "../../rackunit-typechecking.rkt") + +(define m + (automaton init + [init : (c → more)] + [more : (a → more) + (d → more) + (r → end)] + [end : ])) + +(define rx #px"^c[ad]+r$") + +(typecheck-fail (automaton init) + #:with-msg "initial state init is not declared state") +(typecheck-fail (automaton init [init : (c → more)]) + #:with-msg "unbound identifier") +(typecheck-fail (automaton init [init : (c → "more")]) + #:with-msg "expected State, given String") + +(define M + (automaton init + [init : (c → (? s1 s2))] + [s1 : (a → (? s1 s2 end reject)) + (d → (? s1 s2 end reject)) + (r → (? s1 s2 end reject))] + [s2 : (a → (? s1 s2 end reject)) + (d → (? s1 s2 end reject)) + (r → (? s1 s2 end reject))] + [end : ])) + + +(check-type (M '(c a r)) : Bool) ; symbolic result +(check-type (if (M '(c a r)) 1 2) : Int) + +;; example commands +(check-type (m '(c a r)) : Bool -> #t) +(check-type (m '(c d r)) : Bool -> #t) +(check-type (m '(c a d a r)) : Bool -> #t) +(check-type (m '(c a d a)) : Bool -> #f) +(check-type (verify-automaton m #px"^c[ad]+r$") : (List Symbol) -> '(c r)) +(check-type (debug-automaton m #px"^c[ad]+r$" '(c r)) : Pict) +(check-type (synthesize-automaton M #px"^c[ad]+r$") : Unit) diff --git a/turnstile/examples/tests/rosette/rosette3/ifc-tests.rkt b/turnstile/examples/tests/rosette/rosette3/ifc-tests.rkt new file mode 100644 index 0000000..98188b8 --- /dev/null +++ b/turnstile/examples/tests/rosette/rosette3/ifc-tests.rkt @@ -0,0 +1,92 @@ +#lang s-exp "../../rosette/ifc3.rkt" +(require "../../rackunit-typechecking.rkt") + +#;(define (cex-case name ended? prog [k #f]) + (test-case name (check-pred EENI-witness? (verify-EENI* init ended? mem≈ prog k)))) +(define p0 (program 3 (list Halt Noop Push Pop Add* Load* Store*AB))) +(check-type p0 : Prog) + +;; expected: +;; m0 initial: +;; (machine [pc = 0@⊥] +;; [stack = ()] +;; [mem = (0@⊥ 0@⊥)] +;; [insts = ((Push -16@⊥) (Push 1@⊤) (Store*AB))] +;; m0 final: +;; (machine [pc = 3@⊥] +;; [stack = ()] +;; [mem = (0@⊥ -16@⊥)] +;; [insts = ((Push -16@⊥) (Push 1@⊤) (Store*AB))] +;; m1 initial: +;; (machine [pc = 0@⊥] +;; [stack = ()] +;; [mem = (0@⊥ 0@⊥)] +;; [insts = ((Push -16@⊥) (Push 0@⊤) (Store*AB))] +;; m1 final: +;; (machine [pc = 3@⊥] +;; [stack = ()] +;; [mem = (-16@⊥ 0@⊥)] +;; [insts = ((Push -16@⊥) (Push 0@⊤) (Store*AB))] +(define w0 (verify-EENI* init halted? mem≈ p0 #f)) +(check-type w0 : Witness) +(check-type (EENI-witness? w0) : Bool -> #t) + +;; (define (valid-case name ended? prog [k #f]) +;; (test-case name (check-true (verify-EENI* init ended? mem≈ prog k)))) + +;; (define-syntax-rule (define-tests id desc expr ...) +;; (define id +;; (test-suite+ +;; desc +;; (begin expr ...)))) + +;; ; Checks for counterexamples for bugs in basic semantics. +;; (define-tests basic-bugs "IFC: counterexamples for bugs in basic semantics" +;; (cex-case "Fig. 1" halted? (program 3 (list Halt Noop Push Pop Add* Load* Store*AB))) +;; (cex-case "Fig. 2" halted? (program 3 (list Halt Noop Push Pop Add* Load* Store*B))) +;; (cex-case "Fig. 3" halted? (program 5 (list Halt Noop Push Pop Add* Load* Store))) +;; (cex-case "Fig. 4" halted? (program 7 (list Halt Noop Push Pop Add Load* Store)))) + +;; (define-tests basic-correct "IFC: no bounded counterexamples for correct basic semantics" +;; (valid-case "*" halted? (program 7 (list Halt Noop Push Pop Add Load Store))) +;; (valid-case "+" halted? (program 8 (list Halt Noop Push Pop Add Load Store)))) + +;; (define-tests jump-bugs "IFC: counterexamples for bugs in jump+basic semantics" +;; (cex-case "11" halted? (program 6 (list Halt Noop Push Pop Add Load Store Jump*AB))) +;; (cex-case "12" halted? (program 4 (list Halt Noop Push Pop Add Load Store Jump*B)))) + +;; (define-tests jump-correct "IFC: no bounded counterexamples for correct jump+basic semantics" +;; (valid-case "**" halted? (program 7 (list Halt Noop Push Pop Add Load Store Jump))) +;; (valid-case "++" halted? (program 8 (list Halt Noop Push Pop Add Load Store Jump)))) + +;; (define-tests call-return-bugs "IFC: counterexamples for buggy call+return+basic semantics" +;; (cex-case "Fig. 13" halted∩low? (program 7 (list Halt Noop Push Pop Add Load Store Call*B Return*AB))) +;; (cex-case "Fig. 15" halted∩low? (program 8 (list Halt Noop Push Pop Add Load StoreCR Call*B Return*AB))) +;; (cex-case "Fig. 16" halted∩low? (program 8 (list Halt Noop Push Pop Add Load StoreCR Call*B Return*B))) +;; (cex-case "Fig. 17" halted∩low? (program 10 (list Halt Noop Push Pop Add Load StoreCR Call Return)))) + +;; (define-tests reproduce-bugs "IFC: counterexamples that are structurally similar to those in prior work" +;; (cex-case "Fig. 13*" halted∩low? (program (list Push Call*B Halt Push Push Store Return*AB))) +;; (cex-case "Fig. 15*" halted∩low? (program (list Push Push Call*B Push StoreCR Halt Push Return*AB))) +;; (cex-case "Fig. 16*" halted∩low? (program (list Push Push Call*B Push StoreCR Halt Return*B Push Return*B))) +;; (cex-case "Fig. 17*" +;; halted∩low? +;; (program (list Push Call Push StoreCR Halt Push Push Call Pop Push Return)) +;; 13)) + +;; (define (fast-tests) +;; (time (run-tests basic-bugs)) ; ~10 sec +;; (time (run-tests basic-correct)) ; ~20 sec +;; (time (run-tests jump-bugs))) ; ~7 sec + +;; (define (slow-tests) +;; (time (run-tests jump-correct)) ; ~52 sec +;; (time (run-tests call-return-bugs)) ; ~440 sec +;; (time (run-tests reproduce-bugs))) ; ~256 sec + +;; (module+ fast +;; (fast-tests)) + +;; (module+ test +;; (fast-tests) +;; (slow-tests)) diff --git a/turnstile/examples/tests/rosette/rosette3/rosette-guide-sec2-tests.rkt b/turnstile/examples/tests/rosette/rosette3/rosette-guide-sec2-tests.rkt new file mode 100644 index 0000000..04c6ae6 --- /dev/null +++ b/turnstile/examples/tests/rosette/rosette3/rosette-guide-sec2-tests.rkt @@ -0,0 +1,251 @@ +#lang s-exp "../../../rosette/rosette3.rkt" +(require "../../rackunit-typechecking.rkt" + "check-type+asserts.rkt") + +;; all examples from the Rosette Guide, Sec 2 + +(define-symbolic b boolean?) +(check-type b : Bool) +(check-type (boolean? b) : Bool -> #t) +(check-type (integer? b) : Bool -> #f) + +;; TODO: fix these tests? +(check-type (vector b 1) : (CMVectorof (U (Constant Bool) CPosInt)) -> (vector b 1)) +;; mut vectors are invariant +(check-not-type (vector b 1) : (CMVectorof (U Bool CPosInt))) +(check-not-type (vector b 1) : (CIVectorof (U Bool CPosInt))) +(check-not-type (vector b 1) : (CMVectorof (CU CBool CPosInt))) +(check-type (vector b 1) : (CMVectorof (U (Constant Bool) CPosInt))) +;; mutable vectors are invariant +(check-not-type (vector b 1) : (CMVectorof (U CBool CPosInt))) +(check-not-type (vector b 1) : (CMVectorof (U Bool CInt))) + +(check-type (vector b 1) : (CVectorof (U (Constant Bool) PosInt))) +;; vectors are also invariant, because it includes mvectors +(check-not-type (vector b 1) : (CVectorof (U Bool PosInt))) +(check-not-type (vector b 1) : (CVectorof (U Bool CInt))) +(check-not-type (vector b 1) : (CVectorof (U Bool Int))) + +(check-type (not b) : Bool -> (! b)) +(check-type (boolean? (not b)) : Bool -> #t) + +(define-symbolic* n integer?) + +;; TODO: support internal definition contexts +(define (static -> Bool) + (let-symbolic (x boolean?) x)) +#;(define (static -> Bool) + (define-symbolic x boolean? : Bool) ; creates the same constant when evaluated + x) + +(define (dynamic -> Int) + (let-symbolic* (y integer?) y)) +#;(define (dynamic -> Int) + (define-symbolic* y integer? : Int) ; creates a different constant when evaluated + y) + +(check-type static : (C→ Bool)) +(check-not-type static : (C→ CBool)) +(check-type dynamic : (C→ Int)) +(check-type dynamic : (C→ Num)) +(check-not-type dynamic : (C→ CInt)) +(check-type (eq? (static) (static)) : Bool -> #t) + +(define sym*1 (dynamic)) +(define sym*2 (dynamic)) +(check-type (eq? sym*1 sym*2) : Bool -> (= sym*1 sym*2)) + +(define (yet-another-x -> Bool) + (let-symbolic (x boolean?) x)) + +(check-type (eq? (static) (yet-another-x)) + : Bool -> (<=> (static) (yet-another-x))) + +(check-type+asserts (assert #t) : Unit -> (void) (list)) +(check-runtime-exn (assert #f)) + +(check-type+asserts (assert (not b)) : Unit -> (void) (list (! b) #f)) + +(check-type (clear-asserts!) : Unit -> (void)) +(check-type (asserts) : (CListof Bool) -> (list)) + +;; sec 2.3 +(define (poly [x : Int] -> Int) + (+ (* x x x x) (* 6 x x x) (* 11 x x) (* 6 x))) + +(define (factored [x : Int] -> Int) + (* x (+ x 1) (+ x 2) (+ x 2))) + +(define (same [p : (C→ Int Int)] [f : (C→ Int Int)] [x : Int] -> Unit) + (assert (= (p x) (f x)))) + +; check zeros; all seems well ... +(check-type+asserts (same poly factored 0) : Unit -> (void) (list)) +(check-type+asserts (same poly factored -1) : Unit -> (void) (list)) +(check-type+asserts (same poly factored -2) : Unit -> (void) (list)) + +;; 2.3.1 Verification + +(define-symbolic i integer?) +(define cex (verify (same poly factored i))) +(check-type cex : CSolution) +(check-type (sat? cex) : Bool -> #t) +(check-type (unsat? cex) : Bool -> #f) +(check-type (evaluate i cex) : Int -> 12) +(check-runtime-exn (same poly factored 12)) +(clear-asserts!) + +;; 2.3.2 Debugging + +(require "../../../rosette/query/debug3.rkt" + "../../../rosette/lib/render3.rkt") +(define/debug (factored/d [x : Int] -> Int) + (* x (+ x 1) (+ x 2) (+ x 2))) + +(define ucore (debug [integer?] (same poly factored/d 12))) +(typecheck-fail (debug [positive?] (same poly factored/d 12)) + #:with-msg "Expected a Rosette-solvable type, given.*positive?") +(typecheck-fail (debug [(~> integer? integer?)] (same poly factored/d 12)) + #:with-msg "Expected a non-function Rosette type, given.*~> integer\\? integer\\?") +(check-type ucore : CSolution) +;; TESTING TODO: requires visual inspection (in DrRacket) +(check-type (render ucore) : CPict) + +;; 2.3.3 Synthesis + +(require "../../../rosette/lib/synthax3.rkt") +(check-type (??) : Int) +(check-type (?? boolean?) : Bool) +(typecheck-fail (?? positive?) + #:with-msg "Expected a Rosette-solvable type, given.*positive?") +(typecheck-fail (?? (~> integer? integer?)) + #:with-msg "Expected a non-function Rosette type, given.*integer\\? integer\\?") + + +(define (factored/?? [x : Int] -> Int) + (* (+ x (??)) (+ x 1) (+ x (??)) (+ x (??)))) + + +(define binding + (synthesize #:forall (list i) + #:guarantee (same poly factored/?? i))) +(check-type binding : CSolution) +(check-type (sat? binding) : Bool -> #t) +(check-type (unsat? binding) : Bool -> #f) +;; TESTING TODO: requires visual inspection of stdout +(check-type (print-forms binding) : Unit -> (void)) +;; typed/rosette should print: +;; '(define (factored/?? (x : Int) -> Int) (* (+ x 3) (+ x 1) (+ x 2) (+ x 0))) +;; (untyped) rosette should print: +;; '(define (factored x) (* (+ x 3) (+ x 1) (+ x 2) (+ x 0))) + +;; 2.3.4 Angelic Execution + +(define-symbolic x y integer?) +(define sol + (solve (begin (assert (not (= x y))) + (assert (< (abs x) 10)) + (assert (< (abs y) 10)) + (assert (not (= (poly x) 0))) + (assert (= (poly x) (poly y)))))) +(check-type sol : CSolution) +(check-type (sat? sol) : Bool -> #t) +(check-type (unsat? sol) : Bool -> #f) +(check-type (evaluate x sol) : Int -> -5) +(check-type (evaluate y sol) : Int -> 2) +(check-type (evaluate (poly x) sol) : Int -> 120) +(check-type (evaluate (poly y) sol) : Int -> 120) + +;; 2.4 Symbolic Reasoning + +(define-symbolic x1 y1 real?) +(check-type (current-bitwidth) : (CU CPosInt CFalse) -> 5) +(check-type (current-bitwidth #f) : CUnit -> (void)) +(check-type (current-bitwidth) : (CU CPosInt CFalse) -> #f) +(check-not-type (current-bitwidth) : CFalse) +(typecheck-fail (current-bitwidth #t) #:with-msg "expected \\(CU CFalse CPosInt\\), given True") +(typecheck-fail (current-bitwidth 0) #:with-msg "expected \\(CU CFalse CPosInt\\), given Zero") +(typecheck-fail (current-bitwidth -1) #:with-msg "expected \\(CU CFalse CPosInt\\), given NegInt") +(check-type (current-bitwidth 5) : CUnit -> (void)) + +; there is no solution under 5-bit signed integer semantics +(check-type (solve (assert (= x1 3.5))) : CSolution -> (unsat)) +(check-type (solve (assert (= x1 64))) : CSolution -> (unsat)) + +; and quantifiers are not supported +(check-runtime-exn (solve (assert (forall (list x1) (= x1 (+ x1 y1)))))) +;; expected err: +;; finitize: cannot use (current-bitwidth 5) with a quantified formula +;; (forall (x1) (= x1 (+ x1 y1))); use (current-bitwidth #f) instead + +;; infinite precision semantics +(current-bitwidth #f) + +(define sol1 (solve (assert (= x1 3.5)))) +;; sol1 = (model [x1 7/2]) +(check-type sol1 : CSolution) +(check-type (sat? sol1) : Bool -> #t) +(check-type (evaluate x1 sol1) : Num -> 7/2) + +(define sol2 (solve (assert (= x1 64)))) +;; sol2 = (model [x1 64.0]) +(check-type sol2 : CSolution) +(check-type (sat? sol2) : Bool -> #t) +(check-type (evaluate x1 sol2) : Num -> 64.0) + +;; and quantifiers work +(define sol3 (solve (assert (forall (list x1) (= x1 (+ x1 y1)))))) +;; sol3 = (model [y1 0.0]) +(check-type sol3 : CSolution) +(check-type (sat? sol3) : Bool -> #t) +(check-type (evaluate y1 sol3) : Num -> 0.0) + +;; these examples uses symbolic lists +(check-type + (letrec ([[ones : (C→ Int (Listof Int))] + (lambda ([n : Int]) + (if (<= n 0) + (list) + (cons 1 (ones (- n 1)))))]) + (printf "~a" (ones 3)) + (printf "~a" (ones x))) + : Unit) + +(check-type + (letrec ([[ones : (C→ Int (Listof Int))] + (lambda ([n : Int]) + (if (<= n 0) + (list) + (cons 1 (ones (- n 1)))))]) + (ones 3)) + : (Listof Int) -> (list 1 1 1)) + +;; inf loop +(check-type + (letrec ([[ones : (C→ Int (Listof Int))] + (lambda ([n : Int]) + (if (<= n 0) + (list) + (cons 1 (ones (- n 1)))))]) + (ones x)) + : (Listof Int)) + +;; drop lambda annotation +(check-type + (letrec ([[ones : (C→ Int (Listof Int))] + (lambda (n) + (if (<= n 0) + (list) + (cons 1 (ones (- n 1)))))]) + (printf "~a" (ones 3)) + (printf "~a" (ones x))) + : Unit) + +(check-type + (letrec ([[adder : (C→ (CListof Int) Int (CListof Int))] + (lambda (vs n) + (if (null? vs) + (list) + (cons (+ (car vs) n) (adder (cdr vs) n))))]) + (adder '(1 2 3) x)) + : (CListof Int) -> (list (+ 1 x) (+ 2 x) (+ 3 x))) diff --git a/turnstile/examples/tests/rosette/rosette3/rosette-guide-sec3-tests.rkt b/turnstile/examples/tests/rosette/rosette3/rosette-guide-sec3-tests.rkt new file mode 100644 index 0000000..9eed2db --- /dev/null +++ b/turnstile/examples/tests/rosette/rosette3/rosette-guide-sec3-tests.rkt @@ -0,0 +1,120 @@ +#lang s-exp "../../../rosette/rosette3.rkt" +(require "../../rackunit-typechecking.rkt" + "check-type+asserts.rkt") + +;; Examples from the Rosette Guide, Section 3 + +;; Symbolic effects +(define y1 (ann 0 : Nat)) +(check-type (if #t (void) (set! y1 3)) : CUnit -> (void)) +;; y1 unchanged: 0 +(check-type y1 : Nat -> 0) +(check-type (if #f (set! y1 3) (void)) : CUnit -> (void)) +;; y1 unchanged: 0 +(check-type y1 : Nat -> 0) +;; symbolic effect! +(define-symbolic x1 boolean?) +(typecheck-fail (define-symbolic x1 boolean? : Bool)) +(check-type (if x1 (void) (set! y1 3)) : Unit -> (void)) +;; y1 symbolic: (ite x1 0 3) +(check-type y1 : Nat -> (if x1 0 3)) + + +(define res + (let ([y (ann 0 : Nat)]) + (if #t (void) (set! y 3)) + (printf "y unchanged: ~a\n" y) + (if #f (set! y 3) (void)) + (printf "y unchanged: ~a\n" y) + (let-symbolic (x boolean?) + (if x (void) (set! y 3)) + (printf "y symbolic: ~a\n" y) + (list x y)))) + +(check-type res : (CList Bool Nat)) + +(check-type (second res) : Nat -> (if (first res) 0 3)) +;; use car and cdr instead +(check-type (car (cdr res)) : Nat -> (if (car res) 0 3)) + +;; 3.2 Solver-Aided Forms + +;; 3.2.1 Symbolic Constants + +(define (always-same -> Int) + (let-symbolic (x integer?) + x)) +(check-type (always-same) : Int) +(check-type (eq? (always-same) (always-same)) : Bool -> #t) + +(define (always-different -> Int) + (let-symbolic* (x integer?) + x)) +(check-type (always-different) : Int) +(define diff-sym*1 (always-different)) +(define diff-sym*2 (always-different)) +(check-type (eq? diff-sym*1 diff-sym*2) : Bool -> (= diff-sym*1 diff-sym*2)) + +;; 3.2.2 Assertions + +(check-type+asserts (assert #t) : Unit -> (void) (list)) +(check-type+asserts (assert 1) : Unit -> (void) (list)) +(define-symbolic x123 boolean?) +(check-type+asserts (assert x123) : Unit -> (void) (list x123)) +(check-runtime-exn (assert #f "bad value")) + +(check-type (asserts) : (CListof Bool) -> (list #f)) +(check-type (clear-asserts!) : Unit -> (void)) +(check-type (asserts) : (CListof Bool) -> (list)) + +;; 3.2.3 Angelic Execution +(define-symbolic x y boolean?) +(check-type (assert x) : Unit -> (void)) +(check-type (asserts) : (CListof Bool) -> (list x)) +(define solve-sol (solve (assert y))) +(check-type solve-sol : CSolution) +(check-type (sat? solve-sol) : Bool -> #t) +(check-type (evaluate x solve-sol) : Bool -> #t) ; x must be true +(check-type (evaluate y solve-sol) : Bool -> #t) ; y must be true +(check-type (solve (assert (not x))) : CSolution -> (unsat)) +(clear-asserts!) + +;; 3.2.4 Verification +(check-type (assert x) : Unit -> (void)) +(check-type (asserts) : (CListof Bool) -> (list x)) +(define verif-sol (verify (assert y))) +(check-type (asserts) : (CListof Bool) -> (list x)) +(check-type (evaluate x verif-sol) : Bool -> #t) ; x must be true +(check-type (evaluate y verif-sol) : Bool -> #f) ; y must be false +(check-type (verify #:assume (assert y) #:guarantee (assert (and x y))) + : CSolution -> (unsat)) +(clear-asserts!) + +;; 3.2.5 Synthesis +(define-symbolic synth-x synth-c integer?) +(check-type (assert (even? synth-x)) : Unit -> (void)) +(check-type (asserts) : (CListof Bool) -> (list (= 0 (remainder synth-x 2)))) +(define synth-sol + (synthesize #:forall (list synth-x) + #:guarantee (assert (odd? (+ synth-x synth-c))))) +(check-type (asserts) : (CListof Bool) -> (list (= 0 (remainder synth-x 2)))) +(check-type (evaluate synth-x synth-sol) : Int -> synth-x) ; x is unbound +(check-type (evaluate synth-c synth-sol) : Int -> 1) ; c must an odd integer +(clear-asserts!) + +;; 3.2.6 Optimization +(current-bitwidth #f) ; use infinite-precision arithmetic +(define-symbolic opt-x opt-y integer?) +(check-type (assert (< opt-x 2)) : Unit -> (void)) +(check-type (asserts) : (CListof Bool) -> (list (< opt-x 2))) +(define opt-sol + (optimize #:maximize (list (+ opt-x opt-y)) + #:guarantee (assert (< (- opt-y opt-x) 1)))) +; assertion store same as before +(check-type (asserts) : (CListof Bool) -> (list (< opt-x 2))) +; x + y is maximal at x = 1 and y = 1 +(check-type (evaluate opt-x opt-sol) : Int -> 1) +(check-type (evaluate opt-y opt-sol) : Int -> 1) + +;; 3.2.8 Reasoning Precision +;; see rosette-guide-sec2-tests.rkt, Sec 2.4 Symbolic Reasoning diff --git a/turnstile/examples/tests/rosette/rosette3/rosette-guide-sec4-tests.rkt b/turnstile/examples/tests/rosette/rosette3/rosette-guide-sec4-tests.rkt new file mode 100644 index 0000000..a20d78c --- /dev/null +++ b/turnstile/examples/tests/rosette/rosette3/rosette-guide-sec4-tests.rkt @@ -0,0 +1,259 @@ +#lang s-exp "../../../rosette/rosette3.rkt" +(require "../../rackunit-typechecking.rkt") + +;; Examples from the Rosette Guide, Section 4.1 - 4.2 + +;; 4.1 Equality + +;; should equal? produce CBool? +;; (check-type (equal? 1 #t) : CBool -> #f) +;; (check-type (equal? 1 1.0) : CBool -> #t) +;; (check-type (equal? (list 1) (list 1.0)) : CBool -> #t) +;; (check-type (equal? (box 1) (box 1)) : CBool -> #t) +;; (check-type (equal? (box 1) (box 1.0)) : CBool -> #t) +;; (check-type (equal? (list (box 1)) (list (box 1))) : CBool -> #t) +;; (check-type (equal? (list (box 1)) (list (box 1.0))) : CBool -> #t) +(check-type (equal? 1 #t) : Bool -> #f) +(check-type (equal? 1 1.0) : Bool -> #t) +(check-type (equal? (list 1) (list 1.0)) : Bool -> #t) +(check-type (equal? (box 1) (box 1)) : Bool -> #t) +(check-type (equal? (box 1) (box 1.0)) : Bool -> #t) +(check-type (equal? (list (box 1)) (list (box 1))) : Bool -> #t) +(check-type (equal? (list (box 1)) (list (box 1.0))) : Bool -> #t) + +(define-symbolic n integer?) +(check-type (equal? n 1) : Bool -> (= 1 n)) +(check-type (equal? (box n) (box 1)) : Bool -> (= 1 n)) +(check-not-type (equal? n 1) : CBool) +(check-not-type (equal? (box n) (box 1)) : CBool) +(typecheck-fail (~> positive? positive?) + #:with-msg "Expected a Rosette\\-solvable type, given.*positive?") +(typecheck-fail (~> (~> integer? integer?) integer?) + #:with-msg "Expected a non\\-function Rosette type, given.*~> integer?") +(define-symbolic f g (~> integer? integer?)) +(check-type f : (→ Int Int)) +(check-type g : (→ Int Int)) +(check-type (equal? f g) : Bool -> #f) +(check-type (f 1) : Int -> (f 1)) + +(check-type (eq? 1 #t) : Bool -> #f) +(check-type (eq? 1 1.0) : Bool -> #t) ; equal? transparent solvable values +(check-type (eq? (list 1) (list 1.0)) : Bool -> #t) ; transparent immutable values with eq? contents +(check-type (eq? (box 1) (box 1)) : Bool -> #f); but boxes are mutable, so eq? follows Racket +(check-type (eq? (list (box 1)) (list (box 1))) : Bool -> #f) +(check-type (eq? n 1) : Bool -> (= 1 n)) +(check-type (eq? (box n) (box 1)) : Bool -> #f) +(check-type (eq? f g) : Bool -> #f) ; and procedures are opaque, so eq? follows Racket +(check-type (eq? f f) : Bool -> #t) + +(check-type (distinct?) : Bool -> #t) +(check-type (distinct? 1) : Bool -> #t) +(check-type (distinct? (list 1 2) (list 3) (list 1 2)) : Bool -> #f) +(define-symbolic x y z integer?) +(check-type (distinct? 3 z x y 2) : Bool -> (distinct? 2 3 x y z)) +(define-symbolic b boolean?) +(check-type (distinct? 3 (bv 3 4) (list 1) (list x) y 2) + : Bool -> (&& (! (= 3 y)) (&& (! (= 1 x)) (! (= 2 y))))) +(clear-asserts!) + +;; 4.2 Booleans, Integers, and Reals + +;(define-symbolic b boolean?) +(check-type (boolean? b) : Bool -> #t) +(check-type (boolean? #t) : Bool -> #t) +(check-type (boolean? #f) : Bool -> #t) +(check-type (boolean? true) : Bool -> #t) +(check-type (boolean? false) : Bool -> #t) +(check-type (boolean? 1) : Bool -> #f) +(check-type (not b) : Bool -> (! b)) + +(check-type (nand) : CFalse -> #f) +(check-type (nand #t #t) : Bool -> #f) +(check-type (nand 1 2) : Bool -> #f) +(check-type (nor) : CTrue -> #t) +(check-type (nor #f #f) : Bool -> #t) +(check-type (nor 1 2) : Bool -> #f) + +(check-type (nand #f #t) : Bool -> #t) +(check-type (nand #f (error 'ack "we don't get here")) : Bool -> #t) +(check-type (nor #f #t) : Bool -> #f) +(check-type (nor #t (error 'ack "we don't get here")) : Bool -> #f) +(check-type (implies #f #t) : Bool -> #t) +(check-type (implies #f #f) : Bool -> #t) +(check-type (implies #t #f) : Bool -> #f) +(check-type (implies #f (error 'ack "we don't get here")) : Bool -> #t) +;; (check-type (xor 11 #f) : Any -> 11) +;; (check-type (xor #f 22) : Any -> 22) +;; (check-type (xor 11 22) : Any -> #f) +;; (check-type (xor #f #f) : Any -> #f) + +(check-type +inf.0 : CFloat) +(check-type -inf.0 : CFloat) +(check-type +nan.0 : CFloat) +(check-type -nan.0 : CFloat) + +(check-type (number? 1) : Bool -> #t) +(typecheck-fail (number? 2+3i) #:with-msg "Unsupported literal") +(check-type (number? "hello") : Bool -> #f) +(check-type (real? 1) : Bool -> #t) +(check-type (real? +inf.0) : Bool -> #t) +(typecheck-fail (real? 2+3i) #:with-msg "Unsupported literal") +(typecheck-fail (real? 2.0+0.0i) #:with-msg "Unsupported literal") +(check-type (real? "hello") : Bool -> #f) +(check-type (integer? 1) : Bool -> #t) +(check-type (integer? 2.3) : Bool -> #f) +(check-type (integer? 4.0) : Bool -> #t) +(check-type (integer? +inf.0) : Bool -> #f) +(typecheck-fail (integer? 2+3i) #:with-msg "Unsupported literal") +(check-type (integer? "hello") : Bool -> #f) +(check-type (zero? 0) : CBool -> #t) +(check-type (zero? -0.0) : CBool -> #t) +(check-type (positive? 10) : CBool -> #t) +(check-type (positive? -10) : CBool -> #f) +(check-type (positive? 0.0) : CBool -> #f) +(check-type (negative? 10) : CBool -> #f) +(check-type (negative? -10) : CBool -> #t) +(check-type (negative? -0.0) : CBool -> #f) +(check-type (even? 10.0) : CBool -> #t) +(check-type (even? 11) : CBool -> #f) +(check-type +inf.0 : CNum) +(typecheck-fail (even? +inf.0) #:with-msg "expected.*Int") +(check-type (odd? 10.0) : Bool -> #f) +(check-type (odd? 11) : Bool -> #t) +(typecheck-fail (odd? +inf.0) #:with-msg "expected.*Int") +(check-type (inexact->exact 1) : CNum -> 1) +(check-type (inexact->exact 1.0) : CNum -> 1) +(check-type (exact->inexact 1) : CNum -> 1.0) +(check-type (exact->inexact 1.0) : CNum -> 1.0) + +(check-type (+ 1 2) : CInt -> 3) +(typecheck-fail (+ 1.0 2+3i 5) #:with-msg "Unsupported literal") +(check-type (+) : CInt -> 0) +(check-type (- 5 3.0) : CInt -> 2.0) +(check-type (- 1) : CInt -> -1) +(typecheck-fail (- 2+7i 1 3) #:with-msg "Unsupported literal") +(check-type (* 2 3) : CInt -> 6) +(check-type (* 8.0 9) : CInt -> 72.0) +(typecheck-fail (* 1+2i 3+4i) #:with-msg "Unsupported literal") +(check-type (/ 3 4) : CNum -> 3/4) +(check-type (/ 81 3 3) : CNum -> 9) +(check-type (/ 10.0) : CNum -> 0.1) +(typecheck-fail (/ 1+2i 3+4i) #:with-msg "Unsupported literal") +(check-type (quotient 10 3) : CInt -> 3) +(check-type (quotient -10.0 3) : CInt -> -3.0) +(typecheck-fail (quotient +inf.0 3) #:with-msg "expected.*Int") +(check-type (remainder 10 3) : CInt -> 1) +(check-type (remainder -10.0 3) : CInt -> -1.0) +(check-type (remainder 10.0 -3) : CInt -> 1.0) +(check-type (remainder -10 -3) : CInt -> -1) +(typecheck-fail (remainder +inf.0 3) #:with-msg "expected.*Int") +(check-type (modulo 10 3) : CInt -> 1) +(check-type (modulo -10.0 3) : CInt -> 2.0) +(check-type (modulo 10.0 -3) : CInt -> -2.0) +(check-type (modulo -10 -3) : CInt -> -1) +(typecheck-fail (modulo +inf.0 3) #:with-msg "expected.*Int") +(check-type (abs 1.0) : CInt -> 1.0) +(check-type (abs -1) : CInt -> 1) +(check-type (max 1 3 2) : CInt -> 3) +(check-type (max 1 3 2.0) : CInt -> 3) ; Racket coerces to inexact, but Rosette does not? +(check-type (min 1 3 2) : CInt -> 1) +(check-type (min 1 3 2.0) : CInt -> 1) ; Racket coerces to inexact, but Rosette does not? +(check-type (floor 17/4) : CNum -> 4) +(check-type (floor -17/4) : CNum -> -5) +(check-type (floor 2.5) : CNum -> 2.0) +(check-type (floor -2.5) : CNum -> -3.0) +(check-type (floor +inf.0) : CNum -> +inf.0) +(check-type (ceiling 17/4) : CNum -> 5) +(check-type (ceiling -17/4) : CNum -> -4) +(check-type (ceiling 2.5) : CNum -> 3.0) +(check-type (ceiling -2.5) : CNum -> -2.0) +(check-type (ceiling +inf.0) : CNum -> +inf.0) +(check-type (truncate 17/4) : CNum -> 4) +(check-type (truncate -17/4) : CNum -> -4) +(check-type (truncate 2.5) : CNum -> 2.0) +(check-type (truncate -2.5) : CNum -> -2.0) +(check-type (truncate +inf.0) : CNum -> +inf.0) +(check-type (= 1 1.0) : CBool -> #t) +(check-type (= 1 2) : CBool -> #f) +(typecheck-fail (= 2+3i 2+3i 2+3i) #:with-msg "Unsupported literal") +(check-type (< 1 1) : CBool -> #f) +(check-type (< 1 2 3) : CBool -> #t) +(check-type (< 1 +inf.0) : CBool -> #t) +(check-type (< 1 +nan.0) : CBool -> #f) +(check-type (<= 1 1) : CBool -> #t) +(check-type (<= 1 2 1) : CBool -> #f) +(check-type (> 1 1) : CBool -> #f) +(check-type (> 3 2 1) : CBool -> #t) +(check-type (> +inf.0 1) : CBool -> #t) +(check-type (> +nan.0 1) : CBool -> #f) +(check-type (>= 1 1) : CBool -> #t) +(check-type (>= 1 2 1) : CBool -> #f) +(check-type (expt 2 3) : CInt -> 8) +(check-type (expt 4 0.5) : CNum -> 2.0) +(check-type (expt +inf.0 0) : CInt -> 1) +(check-type pi : CNum -> 3.141592653589793) +(check-type (sgn 10) : CInt -> 1) +(check-type (sgn -10.0) : CInt -> -1.0) +(check-type (sgn 0) : CInt -> 0) +(check-type (sgn +nan.0) : CNum -> +nan.0) + +(clear-asserts!) + +;; 4.2.1 Additional Logic Operators +(check-type (! #f) : Bool -> #t) +(check-type (! #t) : Bool -> #f) +; this typechecks only when b is true +(check-type (! (assert-type (if b #f 3) : Bool)) : Bool -> #t) +; so Rosette emits a corresponding assertion +(check-type (asserts) : (CListof Bool) -> (list b)) +(clear-asserts!) +(check-type (&&) : Bool -> #t) +(check-type (||) : Bool -> #f) +; no shortcircuiting +(check-type (&& #f (begin (displayln "hello") #t)) : Bool -> #f) +(define-symbolic a boolean?) + ; this typechecks only when b is true +(check-type (&& a (assert-type (if b #t 1) : Bool)) : Bool -> a) +; so Rosette emits a corresponding assertion +(check-type (asserts) : (CListof Bool) -> (list b)) +(clear-asserts!) +; no shortcircuiting +(check-type (=> #f (begin (displayln "hello") #f)) : Bool -> #t) +; this typechecks only when b is true +(check-type (<=> a (assert-type (if b #t 1) : Bool)) : Bool -> a) +; so Rosette emits a corresponding assertion +(check-type (asserts) : (CListof Bool) -> (list b)) +(clear-asserts!) + +(current-bitwidth #f) + +(define-symbolic a1 b1 integer?) +(check-type (forall (list) (= a1 b1)) : Bool -> (= a1 b1)) +(define f1 (forall (list a1) (exists (list b1) (= a1 (+ a1 b1))))) ; no free constants +(check-type (list 1) : (CListof PosInt)) +(check-type (list 1) : (CList PosInt)) +(typecheck-fail (exists (list 1) (= a1 b1)) + #:with-msg "Expected list of symbolic constants, given list containing: PosInt") +(typecheck-fail (exists (list (+ a1 b1)) (= a1 b1)) + #:with-msg "Expected list of symbolic constants, given list containing: Int") +(check-type (cons a1 (cons b (list))) : (CList (Constant Int) (Constant Bool))) +(typecheck-fail (forall (list 1) (= a1 b1)) + #:with-msg "Expected list of symbolic constants, given list containing: PosInt") +(typecheck-fail (forall (list (+ a1 b1)) (= a1 b1)) + #:with-msg "Expected list of symbolic constants, given list containing: Int") +; so the model has no bindings +(define sol1 (solve (assert f1))) +(check-type sol1 : CSolution) +(check-type (model sol1) : (CHashTable Any Any)) +(check-type (hash-keys (model sol1)) : (CListof Any) -> (list)) ; empty solution +(check-type (sat? sol1) : Bool -> #t) +(define g1 (forall (list a1) (= a1 (+ a1 b1)))) ; b1 is free in g1 +; so the model has a binding for b +(define sol2 (solve (assert g1))) +(check-type sol2 : CSolution) +(check-type (sat? sol2) : Bool -> #t) +(check-type (evaluate b1 sol2) : Int -> 0) +; body refers to the innermost a1 +(define h (exists (list a1) (forall (list a1) (= a1 (+ a1 a1))))) +; so h is unsatisfiable. +(check-type (solve (assert h)) : CSolution -> (unsat)) diff --git a/turnstile/examples/tests/rosette/rosette3/rosette-guide-sec43-tests.rkt b/turnstile/examples/tests/rosette/rosette3/rosette-guide-sec43-tests.rkt new file mode 100644 index 0000000..a4cc752 --- /dev/null +++ b/turnstile/examples/tests/rosette/rosette3/rosette-guide-sec43-tests.rkt @@ -0,0 +1,190 @@ +#lang s-exp "../../../rosette/rosette3.rkt" +(require "../../rackunit-typechecking.rkt") + +;; Examples from the Rosette Guide, Section 4.3 + +;; 4.3 Bitvectors + +; a bitvector literal of size 7 +(check-type (bv 4 (bitvector 7)) : BV -> (bv 4 7)) +(check-type (bv 4 7) : BV -> (bv 4 7)) +(define-symbolic x y (bitvector 7)) ; symbolic bitvector constants +(check-type x : BV) +(check-type y : BV) +(check-type (bvslt (bv 4 7) (bv -1 7)) : Bool -> #f) +; unsigned 7-bit < comparison of 4 and -1 +(check-type (bvult (bv 4 7) (bv -1 7)) : Bool -> #t) +(define-symbolic b boolean?) +; this typechecks only when b is true +(check-type (bvadd x (if b y (bv 3 4))) : BV -> (bvadd x y)) +(check-type (asserts) : (CListof Bool) -> (list b)) ; Rosette emits an appropriate assertion +(clear-asserts!) + +;; bitvector +(define bv6? (bitvector 6)) +(check-type (bv6? 1) : Bool -> #f) +(check-type (bv6? (bv 3 6)) : Bool -> #t) +(check-type (bv6? (bv 3 5)) : Bool -> #f) +;(define-symbolic b boolean?) +(check-type (bv6? (if b (bv 3 6) #t)) : Bool -> b) +(check-not-type (bv6? (if b (bv 3 6) #t)) : CBool) + +;; bitvector? +;(define bv6? (bitvector 6)) +(define bv7? (bitvector 7)) +;(define-symbolic b boolean?) +(check-type (bitvector? bv6?) : Bool -> #t) ; a concrete bitvector type +(check-type (bitvector? (if b bv6? bv7?)) : Bool -> #f) ; not a concrete type +(check-type (bitvector? integer?) : Bool -> #f) ; not a bitvector type +(check-type (bitvector? 3) : Bool -> #f) ; not a type +;; result is always CBool +(check-type (bitvector? bv6?) : CBool -> #t) ; a concrete bitvector type +(check-type (bitvector? (if b bv6? bv7?)) : CBool -> #f) ; not a concrete type +(check-type (bitvector? integer?) : CBool -> #f) ; not a bitvector type +(check-type (bitvector? 3) : CBool -> #f) ; not a type +;; check CFalse when possible +(check-not-type (bitvector? bv6?) : CFalse) ; a concrete bitvector type +(check-type (bitvector? (if b bv6? bv7?)) : CFalse -> #f) ; not a concrete type +(check-not-type (bitvector? integer?) : CFalse) ; not a bitvector type +(check-type (bitvector? 3) : CFalse -> #f) ; not a type + +;; bv? +(check-type (bv? 1) : Bool -> #f) +(check-type (bv? (bv 1 1)) : Bool -> #t) +(check-type (bv? (bv 2 2)) : Bool -> #t) +;define-symbolic b boolean?) +(check-type (bv? (if b (bv 3 6) #t)) : Bool -> b) + +;; 4.3.1 Comparison Ops +(define-symbolic u v (bitvector 7)) ; symbolic bitvector constants +(check-type (bvslt (bv 4 7) (bv -1 7)) : Bool -> #f) ; signed 7-bit < of 4 and -1 +(check-type (bvult (bv 4 7) (bv -1 7)) : Bool -> #t) ; unsigned 7-bit < of 4 and -1 +;(define-symbolic b boolean?) +(check-type (bvsge u (if b v (bv 3 4))) : Bool -> (bvsle v u)) ; b must be true, else err +(check-type (asserts) : (CListof Bool) -> (list b)) ; so Rosette emits assertion +(clear-asserts!) + +;; 4.3.2 Bitwise Ops +(check-type (bvnot (bv -1 4)) : BV -> (bv 0 4)) +(check-type (bvnot (bv 0 4)) : BV -> (bv -1 4)) +;(define-symbolic b boolean?) +;; typed Rosette rejects this program +(typecheck-fail (bvnot (if b 0 (bv 0 4))) + #:with-msg "expected BV, given \\(U Zero CBV\\)") +;; need assert-type annotation +(check-type (bvnot (assert-type (if b 0 (bv 0 4)) : BV)) : BV -> (bv -1 4)) +(check-type (asserts) : (CListof Bool) -> (list (! b))) +(clear-asserts!) + +(check-type (bvand (bv -1 4) (bv 2 4)) : BV -> (bv 2 4)) +(check-type (bvor (bv 0 3) (bv 1 3)) : BV -> (bv 1 3)) +(check-type (bvxor (bv -1 5) (bv 1 5)) : BV -> (bv -2 5)) +;(define-symbolic b boolean?) +;; typed Rosette rejects this program +(typecheck-fail (bvand (bv -1 4) (if b 0 (bv 2 4))) + #:with-msg "expected BV, given \\(U Zero CBV\\)") +;; need assert-type annotation +(check-type (bvand (bv -1 4) (assert-type (if b 0 (bv 2 4)) : BV)) : BV -> (bv 2 4)) +(check-type (asserts) : (CListof Bool) -> (list (! b))) +(clear-asserts!) + +(check-type (bvshl (bv 1 4) (bv 2 4)) : BV -> (bv 4 4)) +(check-type (bvlshr (bv -1 3) (bv 1 3)) : BV -> (bv 3 3)) +(check-type (bvashr (bv -1 5) (bv 1 5)) : BV -> (bv -1 5)) +;(define-symbolic b boolean?) +;; typed Rosette rejects this program +(typecheck-fail (bvshl (bv -1 4) (if b 0 (bv 2 4))) + #:with-msg "expected BV, given \\(U Zero CBV\\)") +;; need assert-type annotation +(check-type (bvshl (bv -1 4) (assert-type (if b 0 (bv 2 4)) : BV)) : BV -> (bv -4 4)) +(check-type (asserts) : CAsserts -> (list (! b))) +(clear-asserts!) + +;; 4.3.3 Arithmetic Ops +(check-type (bvneg (bv -1 4)) : BV -> (bv 1 4)) +(check-type (bvneg (bv 0 4)) : BV -> (bv 0 4)) +(define-symbolic z (bitvector 3)) +(check-type (bvneg z) : BV -> (bvneg z)) + +(check-type (bvadd (bv -1 4) (bv 2 4)) : BV -> (bv 1 4)) +(check-type (bvsub (bv 0 3) (bv 1 3)) : BV -> (bv -1 3)) +(check-type (bvmul (bv -1 5) (bv 1 5)) : BV -> (bv -1 5)) +;> (define-symbolic b boolean?) +;; typed Rosette rejects this program +(typecheck-fail (bvadd (bv -1 4) (bv 2 4) (if b (bv 1 4) "bad")) + #:with-msg "expected.*BV.*given.*\\(U CBV String\\)") +;; need assert-type annotation +(check-type (bvadd (bv -1 4) (bv 2 4) (assert-type (if b (bv 1 4) "bad") : BV)) + : BV -> (bv 2 4)) +(check-type (asserts) : CAsserts -> (list b)) +(clear-asserts!) + +(check-type (bvsdiv (bv -3 4) (bv 2 4)) : BV -> (bv -1 4)) +(check-type (bvudiv (bv -3 3) (bv 2 3)) : BV -> (bv 2 3)) +(check-type (bvsmod (bv 1 5) (bv 0 5)) : BV -> (bv 1 5)) +;> (define-symbolic b boolean?) +;; typed Rosette rejects this program +(typecheck-fail (bvsrem (bv -3 4) (if b (bv 2 4) "bad")) + #:with-msg "expected.*BV.*given.*\\(U CBV String\\)") +;; need assert-type annotation +(check-type (bvsrem (bv -3 4) (assert-type (if b (bv 2 4) "bad") : BV)) + : BV -> (bv -1 4)) +(check-type (asserts) : CAsserts -> (list b)) +(clear-asserts!) + +;; 4.3.4 Conversion Ops +(check-type (concat (bv -1 4) (bv 0 1) (bv -1 3)) : BV -> (bv -9 8)) +;> (define-symbolic b boolean?) +(check-type (concat (bv -1 4) (if b (bv 0 1) (bv 0 2)) (bv -1 3)) + : BV); -> {[b (bv -9 8)] [(! b) (bv -25 9)]}) + +(check-type (extract 2 1 (bv -1 4)) : BV -> (bv -1 2)) +(check-type (extract 3 3 (bv 1 4)) : BV -> (bv 0 1)) +(define-symbolic i j integer?) +(check-type (extract i j (bv 1 2)) : BV -> (extract i j (bv 1 2))) + ; -> {[(&& (= 0 j) (= 1 i)) (bv 1 2)] ...} +(check-type (asserts) : CAsserts -> (list (< i 2) (<= 0 j) (<= j i))) +(clear-asserts!) + +(check-type (sign-extend (bv -3 4) (bitvector 6)) : BV -> (bv -3 6)) +(check-type (zero-extend (bv -3 4) (bitvector 6)) : BV -> (bv 13 6)) +(define-symbolic c boolean?) +(check-type (zero-extend (bv -3 4) (if b (bitvector 5) (bitvector 6))) + : BV -> (zero-extend (bv -3 4) (if b (bitvector 5) (bitvector 6)))) +; {[b (bv 13 5)] [(! b) (bv 13 6)]}) +;; typed Rosette rejects this program +(typecheck-fail (zero-extend (bv -3 4) (if b (bitvector 5) "bad")) + #:with-msg "expected.*BVPred.*given.*\\(U CBVPred String\\)") +;; need assert-type annotation +(check-type (zero-extend (bv -3 4) (assert-type (if b (bitvector 5) "bad") : BVPred)) + : BV -> (bv 13 5)) +(check-type (asserts) : CAsserts -> (list b)) +(check-type (zero-extend (bv -3 4) (if c (bitvector 5) (bitvector 1))) : BV -> (bv 13 5)) +(check-type (asserts) : CAsserts -> (list c b)) +(clear-asserts!) + +(check-type (bitvector->integer (bv -1 4)) : Int -> -1) +(check-type (bitvector->natural (bv -1 4)) : Nat -> 15) +;> (define-symbolic b boolean?) +(check-type (bitvector->integer (if b (bv -1 3) (bv -3 4))) : Int -> (if b -1 -3)) +;; typed Rosette rejects this program +(typecheck-fail (bitvector->integer (if b (bv -1 3) "bad")) + #:with-msg "expected.*BV.*given.*\\(U CBV String\\)") +;; need assert-type annotation +(check-type (bitvector->integer (assert-type (if b (bv -1 3) "bad") : BV)) : Int -> -1) +(check-type (asserts) : CAsserts -> (list b)) +(clear-asserts!) + +(check-type (integer->bitvector 4 (bitvector 2)) : BV -> (bv 0 2)) +(check-type (integer->bitvector 15 (bitvector 4)) : BV -> (bv -1 4)) +;> (define-symbolic b c boolean?) +;; typed Rosette rejects this program +(typecheck-fail (integer->bitvector (if b pi 3) (if c (bitvector 5) (bitvector 6))) + #:with-msg "expected Int, given.*Num") +(check-type (if b pi 3) : Num) +(check-not-type (if b pi 3) : Int) +;; need assert-type annotation +(define res (integer->bitvector (assert-type (if b pi 3) : Int) + (if c (bitvector 5) (bitvector 6)))) +(check-type res : BV) ;{[c (bv 3 5)] [(! c) (bv 3 6)]}) +(check-type (asserts) : CAsserts -> (list (! b))) diff --git a/turnstile/examples/tests/rosette/rosette3/rosette-guide-sec44-tests.rkt b/turnstile/examples/tests/rosette/rosette3/rosette-guide-sec44-tests.rkt new file mode 100644 index 0000000..73fbbba --- /dev/null +++ b/turnstile/examples/tests/rosette/rosette3/rosette-guide-sec44-tests.rkt @@ -0,0 +1,114 @@ +#lang s-exp "../../../rosette/rosette3.rkt" +(require "../../rackunit-typechecking.rkt") + +;; Examples from the Rosette Guide, Section 4.4 + +;; 4.4 Uninterpreted Functions + +;; example demonstrating unsoundness of Constant +;; (define-symbolic f (~> integer? boolean?)) +;; (define-symbolic x integer?) +;; (define sol (solve (assert (not (equal? (f x) (f 1)))))) +;; (define res (evaluate x sol)) +;; (check-type res : (Constant Int)) +;; (constant? res) + +; an uninterpreted function from integers to booleans: +(define-symbolic f (~> integer? boolean?)) +; no built-in interpretation for 1 +(check-type (f 1) : Bool -> (f 1)) +(check-not-type (f 1) : CBool) +(define-symbolic x real?) +; typed Rosette rejects tis program +(typecheck-fail (f x) #:with-msg "expected Int, given.*Num") +;; must use assert-type to cast to Int +(check-type (f (assert-type x : Int)) + : Bool -> (f (assert-type x : Int))) ;(app f (real->integer x))) +(check-type (asserts) : CAsserts -> (list (integer? x))) +(clear-asserts!) +;(clear-terms!) ; must not clear terms + +;; typed Rosette rejects this program +(typecheck-fail (solve (assert (not (equal? (f x) (f 1))))) + #:with-msg "expected Int, given.*Num") +;; must use assert-type to cast x toInt +(define sol (solve (assert (not (equal? (f (assert-type x : Int)) (f 1)))))) +(check-type sol : CSolution) +(define g (evaluate f sol)) ; an interpretation of f +(check-type g : (→ Int Bool)) ; -> (fv (((1) . #f) ((0) . #t)) #f integer?~>boolean?) +; f is a function value +(check-type (fv? f) : Bool -> #t) +; and so is g +(check-type (fv? g) : Bool -> #t) + +;; The tests below depend on a specific term-cache (should be commented out above) +;; at the time solve was called +;; should this be Num or Int? +;(check-type (evaluate x sol) : Int -> 0) +(check-type (evaluate x sol) : Num -> 0) +;; check soundness of Constant +(check-not-type (evaluate x sol) : (Constant Num)) +; we can apply g to concrete values +(check-type (g 2) : Bool -> #f) +; and to symbolic values +(check-type (g (assert-type x : Int)) : Bool -> (= 0 (real->integer x))) + +;; this test does not depend on the term cache +(check-type (equal? (g 1) (g (assert-type (evaluate x sol) : Int))) : Bool -> #f) +(clear-asserts!) + +;; ~> +(define t (~> integer? real? boolean? (bitvector 4))) +(check-type t : (C→ Any Bool) -> (~> integer? real? boolean? (bitvector 4))) ;integer?~>real?~>boolean?~>(bitvector? 4) +(typecheck-fail (~> t integer?) + #:with-msg "Expected a non-function Rosette type, given.*t") +(define-symbolic b boolean?) +(typecheck-fail (~> integer? (if b boolean? real?)) + #:with-msg "Expected a Rosette-solvable type, given") +(typecheck-fail (~> real?) #:with-msg "expected more terms") + +;; function? +(define t0? (~> integer? real? boolean? (bitvector 4))) +(define t1? (~> integer? real?)) +(check-type (function? t0?) : Bool -> #t) +(check-type (function? t1?) : Bool -> #t) +;> (define-symbolic b boolean?) +(check-type (function? (if b t0? t1?)) : Bool -> #f) ; not a concrete type +(check-type (function? integer?) : Bool -> #f) ; not a function type +(check-type (function? 3) : Bool -> #f) ; not a type + +;; should always be CBool, and sometimes CFalse +(check-type (function? t0?) : CBool -> #t) +(check-type (function? t1?) : CBool -> #t) +(check-type (function? (if b t0? t1?)) : CBool -> #f) ; not a concrete type +(check-type (function? integer?) : CBool -> #f) ; not a function type +(check-type (function? 3) : CBool -> #f) ; not a type + +(check-type (function? t0?) : CBool -> #t) +(check-type (function? t1?) : CBool -> #t) +(check-type (function? (if b t0? t1?)) : CFalse -> #f) ; not a concrete type +(check-type (function? integer?) : CBool -> #f) ; not a function type +(check-type (function? 3) : CFalse -> #f) ; not a type + +;; fv? +(define-symbolic f2 (~> boolean? boolean?)) +(check-type (fv? f2) : Bool -> #t) +(check-not-type (fv? f2) : CBool) +(check-type (fv? (lambda ([x : Int]) x)) : Bool -> #f) +;> (define-symbolic b boolean?) +(check-type (fv? (if b f2 1)) : Bool -> b) +(define sol2 + (solve + (begin + (assert (not (f2 #t))) + (assert (f2 #f))))) +(check-type sol2 : CSolution) +(check-type (sat? sol2) : Bool -> #t) +(define g2 (evaluate f2 sol2)) +(check-type g2 : (→ Bool Bool)) ; g2 implements logical negation +;(fv (((#f) . #t) ((#t) . #f)) #t boolean?~>boolean?) +(check-type (fv? g2) : Bool -> #t) +; verify that g implements logical negation: +(check-type (verify (assert (equal? (g2 b) (not b)))) : CSolution -> (unsat)) +(check-type (g2 #t) : Bool -> #f) +(check-type (g2 #f) : Bool -> #t) diff --git a/turnstile/examples/tests/rosette/rosette3/rosette-guide-sec45-tests.rkt b/turnstile/examples/tests/rosette/rosette3/rosette-guide-sec45-tests.rkt new file mode 100644 index 0000000..fbeae1e --- /dev/null +++ b/turnstile/examples/tests/rosette/rosette3/rosette-guide-sec45-tests.rkt @@ -0,0 +1,21 @@ +#lang s-exp "../../../rosette/rosette3.rkt" +(require "../../rackunit-typechecking.rkt") + +;; Examples from the Rosette Guide, Section 4.5 + +;; 4.5 Procedures +(define-symbolic b boolean?) +(define-symbolic x integer?) +(define p (if b * -)) ; p is a symbolic procedure +(check-type p : (→ Num Num Num)) +(check-not-type p : (C→ Num Num Num)) ; should not have concrete type +(check-type p : (→ Int Int Int)) +(define sol (synthesize #:forall (list x) + #:guarantee (assert (= x (p x 1))))) +(check-type (evaluate p sol) : (→ Int Int Int) -> *) +;; this doesnt hold bc type of result is from p +;(check-type (evaluate p sol) : (→ PosInt PosInt PosInt) -> *) +(define sol2 (synthesize #:forall (list x) + #:guarantee (assert (= x (p x 0))))) +(check-type (evaluate p sol2) : (→ Int Int Int) -> -) +(check-not-type (evaluate p sol2) : (→ PosInt PosInt PosInt)) diff --git a/turnstile/examples/tests/rosette/rosette3/rosette-guide-sec46-tests.rkt b/turnstile/examples/tests/rosette/rosette3/rosette-guide-sec46-tests.rkt new file mode 100644 index 0000000..3ffb077 --- /dev/null +++ b/turnstile/examples/tests/rosette/rosette3/rosette-guide-sec46-tests.rkt @@ -0,0 +1,95 @@ +#lang s-exp "../../../rosette/rosette3.rkt" +(require "../../rackunit-typechecking.rkt") + +;; Examples from the Rosette Guide, Section 4.6-4.8 + +;; 4.6 Pairs and Lists +(define-symbolic x y z n integer?) +(define xs (take (list x y z) n)) ; (1) xs is a symbolic list +(check-type xs : (Listof Int)) +(define sol1 (solve (assert (null? xs)))) +(check-type sol1 : CSolution) +(check-type (sat? sol1) : Bool -> #t) +(check-type (evaluate xs sol1) : (Listof Int) -> '()) +(define sol2 + (solve (begin + (assert (= (length xs) 2)) + (assert (not (equal? xs (reverse xs)))) + (assert (equal? xs (sort xs <)))))) +(check-type (evaluate xs sol2) : (Listof Int) -> '(1 4)) +(define-symbolic b boolean?) +(define p (if b (cons 1 2) (cons 4 #f))) ; (2) p is a symbolic pair +(check-type p : (Pair Nat (U Nat Bool))) +(check-type p : (Pair Any Any)) +(check-not-type p : (CPair Any Any)) ; check not concrete +(check-type p : (Pair CNat (CU CNat CBool))) ; contents are concrete +(define sol3 (solve (assert (boolean? (cdr p))))) +(check-type (evaluate p sol3) : (Pair Nat (U Nat Bool)) -> '(4 . #f)) +(define sol4 (solve (assert (odd? (car p))))) +(check-type (evaluate p sol4) : (Pair Nat (U Nat Bool)) -> '(1 . 2)) + +;; 4.7 Vectors +(define v1 (vector 1 2 #f)) +(define v2 (vector 1 2 #f)) +;; mutable vectors are invariant +(check-type v1 : (CMVectorof (CU CPosInt CFalse))) +(check-type v1 : (CVectorof (CU CPosInt CFalse))) +(check-not-type v1 : (CMVectorof (U Nat Bool))) +(check-not-type v1 : (CVectorof (U Nat Bool))) +(check-type v2 : (CMVectorof (CU CPosInt CFalse))) +(check-type (eq? v1 v2) : Bool -> #f) +(check-type (equal? v1 v2) : Bool -> #t) + +(define v3 (vector-immutable 1 2 #f)) +(define v4 (vector-immutable 1 2 #f)) +;; immutable vectors have supertypes +(check-type v3 : (CIVectorof (CU CPosInt CFalse))) +(check-type v3 : (CVectorof (U Nat Bool))) +(check-type v4 : (CIVectorof (CU CPosInt CFalse))) +(check-type (eq? v3 v4) : Bool -> #t) +(check-type (equal? v1 v3) : Bool -> #t) +;(define-symbolic x y z n integer?) +;(define xs (take (list x y z) n)) ; xs is a symbolic list +(define vs (list->vector xs)) ; vs is a symbolic vector +(check-type vs : (CVectorof (U (Constant Int)))) +(check-type vs : (CMVectorof (U (Constant Int)))) +(define sol5 (solve (assert (= 4 (vector-ref vs (sub1 n)))))) +(check-type (= 4 (vector-ref (evaluate vs sol5) (sub1 (evaluate n sol5)))) + : Bool -> #t) +;; TODO: Constant unsound +(check-type (evaluate vs sol5) : (CVectorof Int) -> (vector 0 4)) +(check-type (evaluate xs sol5) : (Listof Int) -> '(0 4)) + +;; 4.8 Boxes +(define b1 (box 1)) +(define b2 (box 1)) +(check-type b1 : (CMBoxof CPosInt)) +(check-type b1 : (CBoxof CPosInt)) +(check-not-type b1 : (CMBoxof Nat)) ; invariant +(check-type b2 : (CMBoxof CPosInt)) + +(check-type (eq? b1 b2) : Bool -> #f) +(check-type (equal? b1 b2) : Bool -> #t) + +(define b3 (box-immutable 1)) +(define b4 (box-immutable 1)) +(check-type b3 : (CIBoxof CPosInt)) +(check-type b3 : (CBoxof CPosInt)) +(check-type b3 : (CBoxof Nat)) ; subtype ok +(check-type b4 : (CBoxof Nat)) + +(check-type (eq? b3 b4) : Bool -> #t) +(check-type (equal? b1 b3) : Bool -> #t) +;> (define-symbolic x integer?) +;> (define-symbolic b boolean?) + +(define sb1 (box x)) ; sb1 is a box with symbolic contents +(check-type sb1 : (CMBoxof (Constant Int))) +(define sb2 (if b sb1 (box 3))) ; sb2 is a symbolic box +(check-type sb2 : (U (CMBoxof (Constant Int)) (CMBoxof CPosInt))) +(define sol6 (solve (assert (= 4 (unbox sb2))))) +(check-type (evaluate sb1 sol6) : (CMBoxof Int) -> (box 4)) +(check-type (evaluate sb2 sol6) : (U (CMBoxof Int) (CMBoxof CPosInt)) -> (box 4)) +(check-not-type (evaluate sb2 sol6) : (MBoxof Int)) +(check-type (= 4 (unbox (evaluate sb2 sol6))) : Bool -> #t) +(check-type (evaluate (eq? sb1 sb2) sol6) : Bool -> #t) diff --git a/turnstile/examples/tests/rosette/rosette3/rosette-guide-sec49-tests.rkt b/turnstile/examples/tests/rosette/rosette3/rosette-guide-sec49-tests.rkt new file mode 100644 index 0000000..c55519e --- /dev/null +++ b/turnstile/examples/tests/rosette/rosette3/rosette-guide-sec49-tests.rkt @@ -0,0 +1,32 @@ +#lang s-exp "../../../rosette/rosette3.rkt" +(require "../../rackunit-typechecking.rkt") + +;; Examples from the Rosette Guide, Section 4.9 Solvers and Solutions + +;; 4.9.1 The Solver Interface + +(check-type (current-solver) : CSolver -> (current-solver)) +;; TODO +;(check-type gen:solver : CSolver) + +;; 4.9.2 Solutions +(define-symbolic a b boolean?) +(define-symbolic x y integer?) +(define sol + (solve (begin (assert a) + (assert (= x 1)) + (assert (= y 2))))) +(check-type sol : CSolution) +(check-type (sat? sol) : Bool -> #t) +(check-type (evaluate (list 4 5 x) sol) : (Listof Int) -> '(4 5 1)) +(check-type (evaluate (list 4 5 x) sol) : (CListof Int)) ; concrete list ok +(check-not-type (evaluate (list 4 5 x) sol) : (Listof Nat)) +(define vec (vector a)) +(check-type (evaluate vec sol) : (CMVectorof Bool)) +;'#(#t) +; evaluation produces a new vector +(check-type (eq? vec (evaluate vec sol)) : Bool -> #f) +(check-type (evaluate (+ x y) sol) : Int -> 3) +(check-not-type (evaluate (+ x y) sol) : CInt) ; not concrete +(check-type (evaluate (and a b) sol) : Bool -> b) +(check-not-type (evaluate (and a b) sol) : CBool) ; not concrete diff --git a/turnstile/examples/tests/rosette/rosette3/rosette-guide-sec5-tests.rkt b/turnstile/examples/tests/rosette/rosette3/rosette-guide-sec5-tests.rkt new file mode 100644 index 0000000..1eb6a20 --- /dev/null +++ b/turnstile/examples/tests/rosette/rosette3/rosette-guide-sec5-tests.rkt @@ -0,0 +1,59 @@ +#lang s-exp "../../../rosette/rosette3.rkt" +(require "../../rackunit-typechecking.rkt") + +;; Examples from the Rosette Guide, Section 5 Structures + +; immutable transparent type +(struct point ([x : Int] [y : Int]) #:transparent) +(check-type point : (C→ Int Int (CPoint Int Int))) +(check-type point-x : (C→ (CPoint Int Int) Int)) +(check-type point-y : (C→ (CPoint Int Int) Int)) +(check-type point? : (C→ Any Bool)) + +; opaque immutable type +(struct pt ([x : Int] [y : Int])) +; mutable transparent type +(struct pnt ([x : Int] [y : Int]) #:mutable #:transparent) + +(check-type (point 1 2) : (CPoint Int Int) -> (point 1 2)) +(typecheck-fail (point #f 2) #:with-msg "expected Int, given False") +(check-type (pt 1 2) : (CPt Int Int)) ; opaque, incomparable +(check-type (pnt 1 2) : (CPnt Int Int) -> (pnt 1 2)) + +(check-type (eq? (point 1 2) (point 1 2)) : Bool -> #t) ; point structures are values +(check-type (eq? (pt 1 2) (pt 1 2)) : Bool -> #f) ; pt structures are references + +(check-type (eq? (pnt 1 2) (pnt 1 2)) : Bool -> #f) ; pnt structures are references + +(define-symbolic b boolean?) +(define p (if b (point 1 2) (point 3 4))) ; p holds a symbolic structure +(check-type p : (Point Int Int)) +(check-not-type p : (CPoint Int Int)) +(check-type (point-x p) : Int -> (if b 1 3)) ;(ite b 1 3) +(check-type (point-y p) : Int -> (if b 2 4)) ;(ite b 2 4) +(define sol (solve (assert (= (point-x p) 3)))) +(check-type (evaluate p sol) : (Point Int Int) -> (point 3 4)) ;#(struct:point 3 4) +(check-type (= (point-x (evaluate p sol)) 3) : Bool -> #t) + +;; Generics +(define-generics viewable (view viewable -> Nat)) +(typecheck-fail + (struct square (side) + #:methods gen:viewable + [(define (view self) (square-side self))]) + #:with-msg "Missing type annotations for fields") +(struct square ([side : Nat]) + #:methods gen:viewable + [(define (view [self : (Square Nat)] -> Nat) (square-side self))]) +(struct circle ([radius : Nat]) + #:transparent + #:methods gen:viewable + [(define (view [self : (Circle Nat)] -> Nat) (circle-radius self))]) +;(define-symbolic b boolean?) +(define p2 (if b (square 2) (circle 3))) ; p holds a symbolic structure +(check-type p2 : (U (CSquare Nat) (CCircle Nat))) +(check-type p2 : (U (Square Nat) (Circle Nat))) +(check-type (apply-view p2) : Nat -> (if b 2 3)) ;(ite b 2 3) +(define sol2 (solve (assert (= (apply-view p2) 3)))) +(check-type (evaluate p2 sol2) : (U (Square Nat) (Circle Nat)) -> (circle 3)) +(check-type (= (apply-view (evaluate p2 sol2)) 3) : Bool -> #t) diff --git a/turnstile/examples/tests/rosette/rosette3/rosette-guide-sec6-tests.rkt b/turnstile/examples/tests/rosette/rosette3/rosette-guide-sec6-tests.rkt new file mode 100644 index 0000000..911bfcd --- /dev/null +++ b/turnstile/examples/tests/rosette/rosette3/rosette-guide-sec6-tests.rkt @@ -0,0 +1,52 @@ +#lang s-exp "../../../rosette/rosette3.rkt" +(require "../../rackunit-typechecking.rkt") + +;; Examples from the Rosette Guide, Section 6 Libraries + +;; 6.2.1 Synthesis library +(require "../../../rosette/lib/synthax3.rkt") + +;; choose +(define (div2 [x : BV] -> BV) + ([choose bvshl bvashr bvlshr bvadd bvsub bvmul] x (?? (bitvector 8)))) +(define-symbolic i (bitvector 8)) +(print-forms + (synthesize #:forall (list i) + #:guarantee (assert (equal? (div2 i) (bvudiv i (bv 2 8)))))) +(printf "expected output:\n~a\n" + "'(define (div2 [x : BV] -> BV) (bvlshr x (bv 1 8)))") + +;; TODO: define-synthax +; Defines a grammar for boolean expressions +; in negation normal form (NNF). +#;(define-synthax (nnf [x : Bool] [y : Bool] [depth : Int] -> Bool) + #:base (choose x (! x) y (! y)) + #:else (choose + x (! x) y (! y) + ((choose && ||) (nnf x y (- depth 1)) + (nnf x y (- depth 1))))) + +; The body of nnf=> is a hole to be filled with an +; expression of depth (up to) 1 from the NNF grammar. +#;(define (nnf=> [x : Bool] [y : Bool] -> Bool) + (apply-nnf x y 1)) + +;; (define-symbolic a b boolean?) +;; (print-forms +;; (synthesize +;; #:forall (list a b) +;; #:guarantee (assert (equal? (=> a b) (nnf=> a b))))) +;; (printf "expected output:\n~a\n" +;; "'(define (nnf=> [x : Bool] [y : Bool] -> Bool) (|| (! x) y))") + +;; 6.2.2 Angelic Execution Library +(require "../../../rosette/lib/angelic3.rkt") + +(define (static -> Int) (choose 1 2 3)) +(define (dynamic -> Int) (choose* 1 2 3)) +(check-type (equal? (static) (static)) : Bool -> #t) +(define dyn1 (dynamic)) +(define dyn2 (dynamic)) +(check-type (equal? dyn1 dyn2) : Bool -> (equal? dyn1 dyn2)) +;(= (ite xi?$4 1 (ite xi?$5 2 3)) (ite xi?$6 1 (ite xi?$7 2 3))) + diff --git a/turnstile/examples/tests/rosette/rosette3/rosette-guide-sec7-tests.rkt b/turnstile/examples/tests/rosette/rosette3/rosette-guide-sec7-tests.rkt new file mode 100644 index 0000000..8f9dc72 --- /dev/null +++ b/turnstile/examples/tests/rosette/rosette3/rosette-guide-sec7-tests.rkt @@ -0,0 +1,230 @@ +#lang s-exp "../../../rosette/rosette3.rkt" +(require "../../rackunit-typechecking.rkt") + +;; Examples from the Rosette Guide, Section 7 Reflecting on Symbolic Values + +;; 7.1.1 Symbolic Terms +(define-symbolic x integer?) ; constant +(define e (+ x 1)) ; expression +(check-type (list (term? x) (term? e)) : (CListof Bool) -> (list #t #t)) +(check-type (list (constant? x) (constant? e)) : (CListof Bool) -> (list #t #f)) +(check-type (list (expression? x) (expression? e)) : (CListof Bool) -> (list #f #t)) +(check-type (term? 1) : Bool -> #f) + +;; TODO: match and match expanders +;; > (define-symbolic x integer?) ; constant +;; > (define e (+ x 1)) ; expression +;; > (match x +;; [(constant identifier type) (list identifier type)]) +;; '(# integer?) +;; > (match x +;; [(term content type) (list content type)]) +;; '(# integer?) +;; > (match e +;; [(expression op child ...) (cons op child)]) +;; '(+ 1 x) +;; > (match e +;; [(term content type) (list content type)]) +;; '((+ 1 x) integer?) + +;(define-symbolic x integer?) +(check-type (type-of x) : (C→ Any Bool) -> integer?) +(check-type (type-of (+ x 1)) : (C→ Any Bool) -> integer?) +(check-type (type-of x 3.14) : (C→ Any Bool) -> real?) +(check-type (type-of #t) : (C→ Any Bool) -> boolean?) +(check-type (type-of #t 1) : (C→ Any Bool) -> any/c) + +(check-type (type? integer?) : Bool -> #t) +(check-type (type? boolean?) : Bool -> #t) +(check-type (type? list?) : Bool -> #t) +(struct circle ([radius : Nat])) +(check-type (type? circle?) : Bool -> #t) +(check-type (type? any/c) : Bool -> #t) +(check-type (type? 1) : Bool -> #f) + +(check-type (solvable? boolean?) : Bool -> #t) +(check-type (solvable? integer?) : Bool -> #t) +(check-type (solvable? real?) : Bool -> #t) +(check-type (solvable? (~> (bitvector 3) (bitvector 4))) : Bool -> #t) +(check-type (solvable? list?) : Bool -> #f) +;(struct circle (radius)) +(check-type (solvable? circle?) : Bool -> #f) +(check-type (solvable? any/c) : Bool -> #f) + +;; 7.1.2 Symbolic Unions +(define-symbolic b boolean?) +(define v (vector 1)) +(check-type v : (CVectorof CPosInt)) +(define w (vector 2 3)) +(check-type v : (CVectorof CPosInt)) +(define s (if b v w)) +(check-type s : (Vectorof CPosInt)) ;{[b #(1)] [(! b) #(2 3)]} +(check-not-type s : (CVectorof CPosInt)) ; check union doesnt have concrete type +(check-type (type-of s) : (C→ Any Bool) -> vector?) +(check-type (eq? s v) : Bool -> b) +(check-type (eq? s w) : Bool -> (! b)) + +; (define-symbolic b boolean?) +(define-symbolic c boolean?) +(define v2 (if c "c" 0)) +(check-type v2 : (U String Int)) +(check-type v2 : (U CString CInt)) +(check-not-type v2 : (CU CString CInt)) ; check not concrete +(check-type v2 : (U CString CInt)) +(check-type v2 : (U CString CZero)) +(define u (if b (vector v2) 4)) +(check-type u : (U (CVectorof (U CString CZero)) Int)) ;{[b #({[c "c"] [(! c) 0]})] [(! b) 4]} +(check-type (type-of u) : (C→ Any Bool) -> any/c) + +(check-type '(1 2) : (CListof CPosInt)) +;> (define-symbolic b boolean?) +(define u2 (if b '(1 2) 3)) +(check-type u2 : (U (CListof CPosInt) CPosInt)) +(check-type (union? u2) : Bool -> #t) +(check-type (union? b) : Bool -> #f) +(define v3 (if b '(1 2) 3)) +(check-type (union-contents v3) + : (CListof (CPair Bool (U (CListof CPosInt) CPosInt))) + -> (list (cons b '(1 2)) (cons (! b) 3))) + +;; 7.1.3 Symbolic Lifting +(require (only-in "../../../rosette/rosette3.rkt" [string-length racket/string-length])) + +(define (string-length [value : String] -> Nat) + (for/all ([str value]) + (racket/string-length str))) + + +(check-type (string-length "abababa") : Nat -> 7) +(check-type (racket/string-length "abababa") : CNat -> 7) +(check-not-type (string-length "abababa") : CNat) + +(typecheck-fail (string-length 3) #:with-msg "expected String") +;> (define-symbolic b boolean?) +(check-type (string-length (if b "a" "abababa")) : Nat -> (if b 1 7)) ;(ite b 1 7) +(check-not-type (string-length (if b "a" "abababa")) : CNat) + +;; Typed Rosette rejects this program +(typecheck-fail (string-length (if b "a" 3)) #:with-msg "expected String") +;; need assert-type +;; TODO: this doesnt work yet because String has no pred +;; - and we cant use string? bc it's unlifted --- will always be assert fail +;(check-type (string-length (assert-type (if b "a" 3) : String)) : Nat -> 1) +;;(check-type (asserts) : CAsserts -> (list b)) +(typecheck-fail (string-length (if b 3 #f)) #:with-msg "expected String") +;; not runtime exn: for/all: all paths infeasible + +;; Making symbolic evaluation more efficient. +;; (require (only-in racket build-list)) + +(define limit 1000) + +(define (slow [xs : (Listof CInt)] -> (U CFalse Int)) + (and (= (length xs) limit) (car (map add1 xs)))) + +(define (fast [xs : (Listof CInt)] -> (U CFalse Int)) + (for/all ([xs xs]) (slow xs))) + +(define ys (build-list limit (lambda ([x : CNat]) x))) +(check-type ys : (CListof CInt)) + +(define-symbolic a boolean?) + +(define xs (if a ys (cdr ys))) +(check-type xs : (Listof CInt)) +(check-not-type xs : (CListof CInt)) + +(check-type (time (slow xs)) : (U CFalse Int) -> (if a 1 #f)) +;; cpu time: 1 real time: 2 gc time: 0 +;; {[a 1] [(! a) #f]} +(check-type (time (fast xs)) : (U CFalse Int) -> (if a 1 #f)) +;; cpu time: 0 real time: 0 gc time: 0 +;; {[a 1] [(! a) #f]} +(printf "First printed time should be slightly slower than second time\n") + +;; define-lift +(require "../../../rosette/lib/lift3.rkt") +(define-lift lifted-string-length [(string?) racket/string-length]) + +(check-type (lifted-string-length "abababa") : Nat -> 7) +(check-not-type (lifted-string-length "abababa") : CNat) +;> (define-symbolic b boolean?) +(check-type (lifted-string-length (if b "a" "abababa")) + : Nat -> (if b 1 7)) ;(ite b 1 7) +;; typed rosette rejects this progrm +(typecheck-fail (lifted-string-length (if b "a" 3)) #:with-msg "expected.*String") +;; TODO: need type-assert +;; (check-type (lifted-string-length (assert-type (if b "a" 3) : String)) : Nat -> 1) +;; (check-type (asserts) : CAsserts -> (list b)) + +;; 7.2 Reflecting on Symbolic State +;> (define-symbolic a b boolean?) +(check-type (if a + (if b + #f + (pc)) + #f) : Bool -> (&& a (! b))) + +(check-type (assert a) : CUnit -> (void)) +(check-type (asserts) : CAsserts -> (list a)) +(check-type (assert b) : CUnit -> (void)) +(check-type (asserts) : CAsserts -> (list b a)) +(check-type (clear-asserts!) : CUnit -> (void)) +(check-type (asserts) : CAsserts -> (list)) + +(printf "expected output: 4 and (list b a)\n") +(with-asserts + (begin (assert a) + (assert b) + 4)) +(check-type (asserts) : CAsserts -> (list)) + +;; term-cache +(clear-terms!) +(check-type (term-cache) : (CHashTable Any Any) -> (term-cache)) +(check-type (hash-keys (term-cache)) : (CListof Any) -> (list)) + +(define-symbolic a1 b1 c1 d1 integer?) + +(define (p? [x : Int] -> Bool) + (or (eq? x a1) (eq? x b1) (eq? x c1) (eq? x d1))) + +(check-type (hash-values (term-cache)) : (CListof Any)); -> (list d1 c1 b1 a1)) +;; make test more deterministic +(check-type (andmap p? (hash-values (term-cache))) : Bool -> #t) +;; (hash +;; # +;; d +;; # +;; c +;; # +;; b +;; # +;; a) +(check-type (* d1 (- (+ a1 b1) c1)) : Int -> (* d1 (- (+ a1 b1) c1))) +;(check-type (hash-keys (term-cache)) : CUnit -> (list (list * d (+ (+ a b) (- c))) d c b a)) +(printf "expected output: hash with a-d and large arith op with all subexprs\n") +(pretty-print (term-cache)) +;; (hash +;; (list * d (+ (+ a b) (- c))) +;; (* d (+ (+ a b) (- c))) +;; # +;; d +;; # +;; c +;; # +;; b +;; # +;; a +;; (list - c) +;; (- c) +;; (list + a b) +;; (+ a b) +;; (list + (+ a b) (- c)) +;; (+ (+ a b) (- c))) +(check-type (clear-terms! (list c1 d1)) : CUnit -> (void)) +(printf "expected output: hash with c and d missing\n") +(pretty-print (term-cache)) +(check-type (clear-terms!) : CUnit -> (void)) +(check-type (hash-keys (term-cache)) : (CListof Any) -> (list)) + diff --git a/turnstile/examples/tests/rosette/rosette3/rosette3-tests.rkt b/turnstile/examples/tests/rosette/rosette3/rosette3-tests.rkt new file mode 100644 index 0000000..a53aa4d --- /dev/null +++ b/turnstile/examples/tests/rosette/rosette3/rosette3-tests.rkt @@ -0,0 +1,345 @@ +#lang s-exp "../../../rosette/rosette3.rkt" +(require "../../rackunit-typechecking.rkt" + "check-type+asserts.rkt") + +;; subtyping among concrete +(check-type ((λ ([x : CPosInt]) x) ((λ ([x : CPosInt]) x) 1)) : CPosInt -> 1) +(check-type ((λ ([x : CZero]) x) ((λ ([x : CZero]) x) 0)) : CZero -> 0) +(check-type ((λ ([x : CNegInt]) x) ((λ ([x : CNegInt]) x) -1)) : CNegInt -> -1) +(check-type ((λ ([x : PosInt]) x) ((λ ([x : PosInt]) x) 1)) : PosInt -> 1) +(check-type ((λ ([x : Zero]) x) ((λ ([x : Zero]) x) 0)) : Zero -> 0) +(check-type ((λ ([x : NegInt]) x) ((λ ([x : NegInt]) x) -1)) : NegInt -> -1) + +(check-type ((λ ([x : CNat]) x) ((λ ([x : CZero]) x) 0)) : CNat -> 0) +(check-type ((λ ([x : CNat]) x) ((λ ([x : CPosInt]) x) 1)) : CNat -> 1) +(check-type ((λ ([x : CNat]) x) ((λ ([x : CNat]) x) 1)) : CNat -> 1) +(typecheck-fail ((λ ([x : CPosInt]) x) ((λ ([x : CNat]) x) 1))) +(check-type ((λ ([x : Nat]) x) ((λ ([x : Zero]) x) 0)) : Nat -> 0) +(check-type ((λ ([x : Nat]) x) ((λ ([x : PosInt]) x) 1)) : Nat -> 1) +(check-type ((λ ([x : Nat]) x) ((λ ([x : Nat]) x) 1)) : Nat -> 1) +(typecheck-fail ((λ ([x : PosInt]) x) ((λ ([x : Nat]) x) 1))) + +(check-type ((λ ([x : CInt]) x) ((λ ([x : CNegInt]) x) -1)) : CInt -> -1) +(check-type ((λ ([x : CInt]) x) ((λ ([x : CZero]) x) 0)) : CInt -> 0) +(check-type ((λ ([x : CInt]) x) ((λ ([x : CPosInt]) x) 1)) : CInt -> 1) +(check-type ((λ ([x : CInt]) x) ((λ ([x : CNat]) x) 1)) : CInt -> 1) +(check-type ((λ ([x : CInt]) x) ((λ ([x : CInt]) x) 1)) : CInt -> 1) +(typecheck-fail ((λ ([x : CPosInt]) x) ((λ ([x : CInt]) x) 1))) +(typecheck-fail ((λ ([x : CNat]) x) ((λ ([x : CInt]) x) 1))) +(check-type ((λ ([x : Int]) x) ((λ ([x : NegInt]) x) -1)) : Int -> -1) +(check-type ((λ ([x : Int]) x) ((λ ([x : Zero]) x) 0)) : Int -> 0) +(check-type ((λ ([x : Int]) x) ((λ ([x : PosInt]) x) 1)) : Int -> 1) +(check-type ((λ ([x : Int]) x) ((λ ([x : Nat]) x) 1)) : Int -> 1) +(check-type ((λ ([x : Int]) x) ((λ ([x : Int]) x) 1)) : Int -> 1) +(typecheck-fail ((λ ([x : PosInt]) x) ((λ ([x : Int]) x) 1))) +(typecheck-fail ((λ ([x : Nat]) x) ((λ ([x : Int]) x) 1))) + +;; illustrates flattening +(define-type-alias A Int) +(define-type-alias B CString) +(define-type-alias C Bool) +(define-type-alias AC (U A C)) +(define-type-alias BC (U B C)) +(define-type-alias A-BC (U A BC)) +(define-type-alias B-AC (U B AC)) +(check-type ((λ ([x : A-BC]) x) ((λ ([x : B-AC]) x) "1")) : A-BC -> "1") +(check-type ((λ ([x : A-BC]) x) ((λ ([x : AC]) x) #t)) : A-BC -> #t) +(check-type ((λ ([x : B-AC]) x) ((λ ([x : A-BC]) x) "1")) : A-BC -> "1") +(check-type ((λ ([x : B-AC]) x) ((λ ([x : BC]) x) "1")) : A-BC -> "1") +(typecheck-fail ((λ ([x : BC]) x) ((λ ([x : B-AC]) x) "1"))) +(typecheck-fail ((λ ([x : AC]) x) ((λ ([x : B-AC]) x) "1"))) + +;; subtyping between concrete and symbolic types +(check-type ((λ ([x : Int]) x) ((λ ([x : CInt]) x) 1)) : Int -> 1) +(typecheck-fail ((λ ([x : CInt]) x) ((λ ([x : Int]) x) 1))) +(check-type ((λ ([x : Bool]) x) ((λ ([x : CBool]) x) #t)) : Bool -> #t) +(typecheck-fail ((λ ([x : CBool]) x) ((λ ([x : Bool]) x) #t))) +(check-type ((λ ([x : (U CInt CBool)]) x) ((λ ([x : (CU CInt CBool)]) x) 1)) : (U CInt CBool)) +(typecheck-fail ((λ ([x : (CU CInt CBool)]) x) ((λ ([x : (U CInt CBool)]) x) 1))) +(check-type ((λ ([x : (U Int Bool)]) x) ((λ ([x : (U CInt CBool)]) x) 1)) : (U CInt CBool)) +(check-type ((λ ([x : (U CInt CBool)]) x) ((λ ([x : (U Int Bool)]) x) 1)) : (U CInt CBool)) + +;; add1 has a case-> type with cases for different subtypes of Int +;; to preserve some of the type information through the operation +(check-type (add1 9) : CPosInt -> 10) +(check-type (add1 0) : CPosInt -> 1) +(check-type (add1 -1) : (CU CNegInt CZero) -> 0) +(check-type (add1 -9) : (CU CNegInt CZero) -> -8) +(check-type (add1 (ann 9 : PosInt)) : PosInt -> 10) +(check-type (add1 (ann 0 : Zero)) : PosInt -> 1) +(check-type (add1 (ann 9 : Nat)) : PosInt -> 10) +(check-type (add1 (ann 0 : Nat)) : PosInt -> 1) +(check-type (add1 (ann -1 : NegInt)) : (U NegInt Zero) -> 0) +(check-type (add1 (ann -9 : NegInt)) : (U NegInt Zero) -> -8) +(check-type (add1 (ann 9 : Int)) : Int -> 10) + +;; sub1 has a similar case-> type +(check-type (sub1 10) : CNat -> 9) +(check-type (sub1 0) : CNegInt -> -1) +(check-type (sub1 -1) : CNegInt -> -2) +(check-type (sub1 (ann 10 : PosInt)) : Nat -> 9) +(check-type (sub1 (ann 0 : Zero)) : NegInt -> -1) +(check-type (sub1 (ann -1 : NegInt)) : NegInt -> -2) + +(check-type (+ 1 10) : CNat -> 11) +(check-type (+ -10 10) : CInt -> 0) +(check-type (+ (ann 1 : PosInt) (ann 10 : PosInt)) : Nat -> 11) +(check-type (+ (ann -10 : NegInt) (ann 10 : PosInt)) : Int -> 0) + +;; if tests +;; if expr has concrete type only if test and both branches are concrete +(check-type (if #t 1 #f) : (CU CBool CInt)) +(check-type (if #t 1 #f) : (U CBool CInt)) +(check-type (if #t 1 #f) : (U Bool CInt)) +(check-type (if #t 1 #f) : (U Bool Int)) +(check-type (if #t 1 2) : CInt) +(check-type (if #t 1 2) : Int) +(check-type (if #t 1 2) : (CU CInt CBool)) +(check-type (if #t 1 2) : (U Int Bool)) +;; non-bool test +(check-type (if 1 2 3) : CInt) +;; else, if expr produces symbolic type +(define-symbolic b0 boolean?) +(define-symbolic i0 integer?) +(typecheck-fail (define-symbolic posint1 positive?) + #:with-msg "Expected a Rosette-solvable type, given positive?") +(typecheck-fail (lambda ([x : (Constant CInt)]) x) + #:with-msg "Constant requires a symbolic type") +(check-type b0 : Bool -> b0) +(check-type b0 : (Constant Bool) -> b0) +(check-not-type b0 : CBool) +(check-type i0 : Int -> i0) +(check-type i0 : (Constant Int) -> i0) +(check-type (if b0 1 2) : Int) +(check-not-type (if b0 1 2) : CInt) +(check-type (if #t i0 2) : Int) +(check-not-type (if #t i0 2) : CInt) +(check-type (if #t 2 i0) : Int) +(check-not-type (if #t 2 i0) : CInt) +(check-type (if b0 i0 2) : Int) +(check-type (if b0 1 #f) : (U CInt CBool)) +(check-type (if b0 1 #f) : (U Int Bool)) +;; slightly unintuitive case: (U Int Bool) <: (U CInt Bool), ok for now (see notes) +(check-type (if #f i0 #f) : (U CInt CBool)) +(check-type (if #f i0 #f) : (U CInt Bool)) +(check-type (if #f i0 #f) : (U Int Bool)) +(check-type (if #f (+ i0 1) #f) : (U Int Bool)) + +;; BVs + +(check-type bv : (Ccase-> (C→ CInt CBVPred CBV) + (C→ CInt CPosInt CBV))) +(typecheck-fail (bv "1" 2) #:with-msg "expected.*Int.*given.*String") +(check-type (bv 1 2) : CBV -> (bv 1 (bitvector 2))) +(check-type (bv 1 (bitvector 2)) : CBV -> (bv 1 (bitvector 2))) +(typecheck-fail (bv (ann 1 : Int) 2) #:with-msg "expected.*CInt") +(typecheck-fail (bv (ann 1 : Int) (bitvector 2)) #:with-msg "expected.*CInt") + +(typecheck-fail (bv 0 0) #:with-msg "expected.*PosInt.*given.*Zero") +(check-type bitvector : (C→ CPosInt CBVPred)) +(check-type (bitvector 3) : CBVPred) +(check-type ((bitvector 4) 1) : Bool -> #f) +(check-type ((bitvector 4) (bv 10 (bitvector 4))) : Bool) + +(check-type (bitvector? "2") : Bool -> #f) +(check-type (bitvector? (bitvector 10)) : Bool -> #t) + +;; bvops +(check-type (bveq (bv 1 3) (bv 1 3)) : Bool -> #t) +(typecheck-fail (bveq (bv 1 3) 1)) +(check-type (bveq (bv 1 2) (bv 1 3)) : Bool) ; -> runtime exn +(check-runtime-exn (bveq (bv 1 2) (bv 1 3))) +(clear-asserts!) + +(check-type (bvand (bv -1 4) (bv 2 4)) : BV + -> (bv 2 4)) +(check-type (bvor (bv 0 3) (bv 1 3)) : BV + -> (bv 1 3)) +(check-type (bvxor (bv -1 5) (bv 1 5)) : BV + -> (bv -2 5)) + +;; examples from rosette guide +(check-type (bvand (bv -1 4) (bv 2 4)) : BV -> (bv 2 4)) +(check-type (bvor (bv 0 3) (bv 1 3)) : BV -> (bv 1 3)) +(check-type (bvxor (bv -1 5) (bv 1 5)) : BV -> (bv -2 5)) + +(define-symbolic b boolean?) +(check-type (bvand (bv -1 4) (if b (bv 3 4) (bv 2 4))) : BV + -> (if b (bv 3 4) (bv 2 4))) + +(check-type (bvshl (bv 1 4) (bv 2 4)) : BV -> (bv 4 4)) +(check-type (bvlshr (bv -1 3) (bv 1 3)) : BV -> (bv 3 3)) +(check-type (bvashr (bv -1 5) (bv 1 5)) : BV -> (bv -1 5)) +;; TODO: see rosette issue #23 --- issue closed, won't fix +(check-type (bvshl (bv -1 4) (if b (bv 3 4) (bv 2 4))) : BV) + +(check-type (bvneg (bv -1 4)) : BV -> (bv 1 4)) +(check-type (bvneg (bv 0 4)) : BV -> (bv 0 4)) +(define-symbolic z (bitvector 3)) +(check-type (bvneg z) : BV) +(check-type (bvadd (bv -1 4) (bv 2 4)) : BV -> (bv 1 4)) +(check-type (bvsub (bv 0 3) (bv 1 3)) : BV -> (bv -1 3)) +(check-type (bvmul (bv -1 5) (bv 1 5)) : BV -> (bv -1 5)) +;; TODO: see rosette issue #23 --- issue closed, won't fix +(check-type (bvadd (bvadd (bv -1 4) (bv 2 4)) (if b (bv 1 4) (bv 3 4))) : BV) +(check-type (bvsdiv (bv -3 4) (bv 2 4)) : BV -> (bv -1 4)) +(check-type (bvudiv (bv -3 3) (bv 2 3)) : BV -> (bv 2 3)) +(check-type (bvsmod (bv 1 5) (bv 0 5)) : BV -> (bv 1 5)) +(check-type (bvsrem (bv -3 4) (if b (bv 2 4) (bv 3 4))) : BV + -> (if b (bv -1 4) (bv 0 4))) +(check-type (concat (concat (bv -1 4) (bv 0 1)) (bv -1 3)) : BV -> (bv -9 8)) +(check-type (concat (concat (bv -1 4) (if b (bv 0 1) (bv 0 2))) (bv -1 3)) : BV + -> (if b (bv -9 8) (bv -25 9))) + +(check-type (extract 2 1 (bv -1 4)) : BV -> (bv -1 2)) +(check-type (extract 3 3 (bv 1 4)) : BV -> (bv 0 1)) +(define-symbolic i j integer?) +(check-type (extract i j (bv 1 2)) : BV) +; -> {[(&& (= 0 j) (= 1 i)) (bv 1 2)] ...}) + +(check-type (sign-extend (bv -3 4) (bitvector 6)) : BV -> (bv -3 6)) +(check-type (zero-extend (bv -3 4) (bitvector 6)) : BV -> (bv 13 6)) +(define-symbolic c boolean?) +(check-type (zero-extend (bv -3 4) (if b (bitvector 5) (bitvector 6))) + : BV -> (if b (bv 13 5) (bv 13 6))) +(check-type+asserts + (zero-extend (bv -3 4) (assert-type (if b (bitvector 5) "bad") : BVPred)) + : BV -> (bv 13 5) (list b)) +(check-type+asserts (zero-extend (bv -3 4) (if c (bitvector 5) (bitvector 1))) + : BV -> (bv 13 5) (list c)) + +(check-type (bitvector->integer (bv -1 4)) : Int -> -1) +(check-type (bitvector->natural (bv -1 4)) : Int -> 15) +(check-type (bitvector->integer (if b (bv -1 3) (bv -3 4))) + : Int -> (if b -1 -3)) +(check-type+asserts + (bitvector->integer (assert-type (if b (bv -1 3) "bad") : BV)) + : Int -> -1 (list b)) +(check-type (integer->bitvector 4 (bitvector 2)) : BV -> (bv 0 2)) +(check-type (integer->bitvector 15 (bitvector 4)) : BV -> (bv -1 4)) +(check-type+asserts (integer->bitvector (assert-type (if b pi 3) : Int) + (if c (bitvector 5) (bitvector 6))) + : BV -> (integer->bitvector 3 (if c (bitvector 5) (bitvector 6))) + (list (not b))) +;; TODO: check that CInt also has the right pred (do we want this?) +#;(check-type+asserts (integer->bitvector (assert-type (if b pi 3) : CInt) + (if c (bitvector 5) (bitvector 6))) + : BV -> (integer->bitvector 3 (if c (bitvector 5) (bitvector 6))) + (list (not b))) +(check-type (integer->bitvector 3 + (if c (bitvector 5) (bitvector 6))) + : BV -> (if c (bv 3 5) (bv 3 6))) + +;; case-> subtyping +(check-type ((λ ([f : (C→ Int Int)]) (f 10)) add1) : Int -> 11) +(check-type ((λ ([f : (Ccase-> (C→ Int Int))]) (f 10)) add1) : Int -> 11) +(check-type ((λ ([f : (Ccase-> (C→ Nat Nat) + (C→ Int Int))]) (f 10)) add1) : Int -> 11) +(check-not-type ((λ ([f : (Ccase-> (C→ Int Int))]) (f 10)) add1) : Nat) +(check-type ((λ ([f : (Ccase-> (C→ Nat Nat) + (C→ Int Int))]) (f 10)) add1) : Nat -> 11) +(typecheck-fail ((λ ([f : (Ccase-> (C→ Zero Zero) + (C→ Int Int))]) (f 10)) add1) + #:with-msg + (string-append "expected \\(Ccase-> \\(C→ Zero Zero\\) \\(C→ Int Int\\)\\), " + "given \\(Ccase-> .*\\(C→ NegInt \\(U NegInt Zero\\)\\) .*\\(C→ Zero PosInt\\) " + ".*\\(C→ PosInt PosInt\\) .*\\(C→ Nat PosInt\\) .*\\(C→ Int Int\\)\\)")) + +;; applying symbolic function types +(check-type ((λ ([f : (U (C→ CInt CInt))]) (f 10)) add1) : Int -> 11) +;; it's either (→ CInt CInt) or (→ CInt CBool), but not both, so +;; add1 can have this type even though it never returns a boolean +(check-type ((λ ([f : (U (C→ CInt CInt) (C→ CInt CBool))]) (f 10)) add1) : (U Int Bool) -> 11) +(check-type ((λ ([f : (U (C→ CInt CInt) (C→ CInt Bool))]) (f 10)) + (if #t add1 positive?)) + : (U CInt Bool) -> 11) +(check-type ((λ ([f : (U (C→ CInt CInt) (C→ CInt Bool))]) (f 10)) + (if #t add1 positive?)) + : (U Int Bool) -> 11) +;; concrete union of functions +(check-type ((λ ([f : (CU (C→ CInt CInt) (C→ CInt CBool))]) (f 10)) add1) : (CU CInt CBool) -> 11) +(check-type ((λ ([f : (CU (C→ CInt CInt) (C→ CInt CBool))]) (f 10)) + (if #t add1 positive?)) + : (CU CInt CBool) -> 11) + +;; check BVPred as type annotation +;; CBV input annotation on arg is too restrictive to work as BVPred +(typecheck-fail ((λ ([bvp : BVPred]) bvp) (λ ([bv : CBV]) #t)) + #:with-msg "expected BVPred.*given.*CBV") +(typecheck-fail ((λ ([bvp : BVPred]) bvp) (λ ([bv : BV]) #t)) + #:with-msg "expected BVPred.*given.*BV") +;; BVpred arg must have Any input type +(check-type ((λ ([bvp : BVPred]) bvp) (λ ([bv : Any]) ((bitvector 2) bv))) : BVPred) + +;; assert-type tests +(check-type+asserts (assert-type (sub1 10) : PosInt) : PosInt -> 9 (list)) +(check-runtime-exn (assert-type (sub1 1) : PosInt)) +(define-symbolic b1 b2 boolean?) + +(check-type (clear-asserts!) : CUnit -> (void)) +;; asserts directly on a symbolic union +(check-type+asserts (assert-type (if b1 1 #f) : Int) : Int -> 1 (list b1)) +(check-type+asserts (assert-type (if b2 1 #f) : Bool) : Bool -> #f (list (not b2))) +;; asserts on the (pc) +(check-type+asserts (if b1 (assert-type 1 : Int) (assert-type #f : Int)) : Int + -> 1 (list b1)) +(check-type+asserts (if b2 (assert-type 1 : Bool) (assert-type #f : Bool)) : Bool + -> #f (list (not b2))) +;; asserts on a define-symbolic value +(define-symbolic i1 integer?) +(check-type+asserts (assert-type i1 : PosInt) : PosInt -> i1 (list (< 0 i1))) +(check-type+asserts (assert-type i1 : Zero) : Zero -> i1 (list (= 0 i1))) +(check-type+asserts (assert-type i1 : NegInt) : NegInt -> i1 (list (< i1 0))) +;; TODO: should this assertion be equivalent to (<= 0 i1) ? +(check-type+asserts (assert-type i1 : Nat) : Nat -> i1 (list (not (< i1 0)))) +;; asserts on other terms involving define-symbolic values +(check-type+asserts (assert-type (+ i1 1) : PosInt) : PosInt -> (+ 1 i1) (list (< 0 (+ 1 i1)))) +(check-type+asserts (assert-type (+ i1 1) : Zero) : Zero -> (+ 1 i1) (list (= 0 (+ 1 i1)))) +(check-type+asserts (assert-type (+ i1 1) : NegInt) : NegInt -> (+ 1 i1) (list (< (+ 1 i1) 0))) + +(check-type+asserts (assert-type (if b1 i1 b2) : Int) : Int -> i1 (list b1)) +(check-type+asserts (assert-type (if b1 i1 b2) : Bool) : Bool -> b2 (list (not b1))) +;; asserts on the (pc) +(check-type+asserts (if b1 (assert-type i1 : Int) (assert-type b2 : Int)) : Int + -> i1 (list b1)) +(check-type+asserts (if b1 (assert-type i1 : Bool) (assert-type b2 : Bool)) : Bool + -> b2 (list (not b1))) +;; TODO: should assert-type cause some predicates to return true or return false? +(check-type+asserts (integer? (assert-type (if b1 i1 b2) : Int)) : Bool -> #t (list b1)) +(check-type+asserts (integer? (assert-type (if b1 i1 b2) : Bool)) : Bool -> #f (list (not b1))) +(check-type+asserts (boolean? (assert-type (if b1 i1 b2) : Int)) : Bool -> #f (list b1)) +(check-type+asserts (boolean? (assert-type (if b1 i1 b2) : Bool)) : Bool -> #t (list (not b1))) + +(check-type (asserts) : (CListof Bool) -> (list)) + +;; tests for Constant +(define-symbolic ci1 integer?) +(define-symbolic bi1 bi2 boolean?) + +(check-type ci1 : (Constant Int)) +(check-type ci1 : Int) +(check-type ci1 : (Constant Num)) +(check-type ci1 : Num) + +;; homogeneous list of constants +(check-type (list bi1 bi2) : (CList (Constant Bool) (Constant Bool))) +(check-type (list bi1 bi2) : (CListof (Constant Bool))) + +;; heterogeneous list of constants +(check-type (list ci1 bi1) : (CList (Constant Int) (Constant Bool))) +(check-type (cons ci1 (cons bi1 (list))) : (CList (Constant Int) (Constant Bool))) + +(check-type + (lambda ([x : CInt] [lst : (CListof CBool)]) (cons x lst)) + : (C→ CInt (CListof CBool) (CListof (CU CInt CBool)))) +(check-not-type + (lambda ([x : Int] [lst : (CListof Bool)]) (cons x lst)) + : (C→ Int (CListof Bool) (CListof (CU CInt CBool)))) +(check-type + (lambda ([x : Int] [lst : (CListof Bool)]) (cons x lst)) + : (C→ Int (CListof Bool) (CListof (U Int Bool)))) + +;; TODO: should these tests hold? +;(check-type ci1 : (U (Constant Int) (Constant Bool))) +;(check-type (list ci1 bi1) : (CListof (U (Constant Int) (Constant Bool)))) +;(check-type (cons ci1 (cons bi1 (list))) : (CListof (U (Constant Int) (Constant Bool)))) diff --git a/turnstile/examples/tests/rosette/rosette3/run-all-rosette-tests-script.rkt b/turnstile/examples/tests/rosette/rosette3/run-all-rosette-tests-script.rkt new file mode 100644 index 0000000..c4c1fc2 --- /dev/null +++ b/turnstile/examples/tests/rosette/rosette3/run-all-rosette-tests-script.rkt @@ -0,0 +1,23 @@ +#lang racket/base + +(require macrotypes/examples/tests/do-tests) + +(do-tests + "rosette3-tests.rkt" "General" + "rosette-guide-sec2-tests.rkt" "Rosette Guide, Section 2" + "rosette-guide-sec3-tests.rkt" "Rosette Guide, Section 3" + "rosette-guide-sec4-tests.rkt" "Rosette Guide, Section 4.1-4.2" + "rosette-guide-sec43-tests.rkt" "Rosette Guide, Section 4.3 BVs" + "rosette-guide-sec44-tests.rkt" "Rosette Guide, Section 4.4 Uninterp Fns" + "rosette-guide-sec45-tests.rkt" "Rosette Guide, Section 4.5 Procedures" + "rosette-guide-sec46-tests.rkt" "Rosette Guide, Section 4.6-4.8") + +(do-tests + "rosette-guide-sec49-tests.rkt" "Rosette Guide, Section 4.9" + "rosette-guide-sec5-tests.rkt" "Rosette Guide, Section 5 Structures" + "rosette-guide-sec6-tests.rkt" "Rosette Guide, Section 6 Libraries" + "rosette-guide-sec7-tests.rkt" "Guide Sec. 7 Reflecting on Symbolic Values") + +(do-tests "bv-tests.rkt" "BV SDSL - General" + "bv-ref-tests.rkt" "BV SDSL - Hacker's Delight synthesis") +