suzanne.soy/macrotypes
1
0
Fork 0
Code Issues Pull Requests Actions Packages Projects Releases Wiki Activity

start sec4.4 tests; fix ~> arity; transfer stx props in define

Browse Source 
- change solvable, etc stx-prop-related err msg
This commit is contained in:
Stephen Chang 2016-09-08 17:04:14 -04:00
parent e3171e2b47
commit a242442a46
10 changed files with 127 additions and 34 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

4
turnstile/examples/rosette/lib/synthax.rkt
View File

@ -16,10 +16,10 @@
#:with ??/progsrc (datum->syntax #'here 'ro:?? #'qq)
[⊢ [pred? ≫ pred?- (⇒ : _) (⇒ typefor ty) (⇒ solvable? s?) (⇒ function? f?)]]
#:fail-unless (syntax-e #'s?)
(format "Must provide a Rosette-solvable type, given ~a."
(format "Expected a Rosette-solvable type, given ~a."
(syntax->datum #'pred?))
#:fail-when (syntax-e #'f?)
(format "Must provide a non-function Rosette type, given ~a."
(format "Expected a non-function Rosette type, given ~a."
(syntax->datum #'pred?))
--------
[⊢ [_ ≫ (??/progsrc pred?-) ⇒ : ty]]])

4
turnstile/examples/rosette/query/debug.rkt
View File

@ -29,10 +29,10 @@
[(_ (pred? ...+) e) ≫
[⊢ [pred? ≫ pred?- (⇒ : _) (⇒ typefor ty) (⇒ solvable? s?) (⇒ function? f?)]] ...
#:fail-unless (stx-andmap syntax-e #'(s? ...))
(format "Must provide a Rosette-solvable type, given ~a."
(format "Expected a Rosette-solvable type, given ~a."
(syntax->datum #'(pred? ...)))
#:fail-when (stx-ormap syntax-e #'(f? ...))
(format "Must provide a non-function Rosette type, given ~a."
(format "Expected a non-function Rosette type, given ~a."
(syntax->datum #'(pred? ...)))
[⊢ [e ≫ e- ⇒ : τ]]
--------

18
turnstile/examples/rosette/rosette-notes.txt
View File

@ -1,4 +1,17 @@
2016-09-08
2016-09-08 --------------------
** Problem: Constant is unsound:
(define-symbolic f (~> integer? boolean?))
(define-symbolic x integer?)
(define sol (solve (assert (not (equal? (f x) (f 1))))))
(define res (evaluate x sol))
res has type (Constant Int) but (constant? res) is false
** Workaround:
2016-09-08 --------------------
Typed Rosette tricky subtyping examples:
@ -122,6 +135,9 @@ TODOs:
- use variance information in type constructors?
- instead of special-casing individual constructors
- ok to say "Rosette type" in type err msgs?
- 2016-09-08: fix Constant soundness wrt evaluate
- 2016-09-08: transfer "typefor" and "solvable?" props to id in define
- DONE 2016-09-08
2016-08-25 --------------------

47
turnstile/examples/rosette/rosette2.rkt
View File

@ -155,10 +155,14 @@
(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?)))
@ -213,7 +217,7 @@
[(_ x:id ...+ pred?) ≫
[⊢ [pred? ≫ pred?- (⇒ : _) (⇒ typefor ty) (⇒ solvable? s?)]]
#:fail-unless (syntax-e #'s?)
(format "Must provide a Rosette-solvable type, given ~a."
(format "Expected a Rosette-solvable type, given ~a."
(syntax->datum #'pred?))
#:with (y ...) (generate-temporaries #'(x ...))
--------
@ -225,7 +229,7 @@
[(_ x:id ...+ pred?) ≫
[⊢ [pred? ≫ pred?- (⇒ : _) (⇒ typefor ty) (⇒ solvable? s?)]]
#:fail-unless (syntax-e #'s?)
(format "Must provide a Rosette-solvable type, given ~a."
(format "Expected a Rosette-solvable type, given ~a."
(syntax->datum #'pred?))
#:with (y ...) (generate-temporaries #'(x ...))
--------
@ -238,7 +242,7 @@
[(_ (x:id ...+ pred?) e ...) ≫
[⊢ [pred? ≫ pred?- (⇒ : _) (⇒ typefor ty) (⇒ solvable? s?)]]
#:fail-unless (syntax-e #'s?)
(format "Must provide a Rosette-solvable type, given ~a."
(format "Expected a Rosette-solvable type, given ~a."
(syntax->datum #'pred?))
[([x ≫ x- : (Constant ty)] ...) ⊢ [(begin e ...) ≫ e- ⇒ τ_out]]
--------
@ -251,7 +255,7 @@
[(_ (x:id ...+ pred?) e ...) ≫
[⊢ [pred? ≫ pred?- (⇒ : _) (⇒ typefor ty) (⇒ solvable? s?)]]
#:fail-unless (syntax-e #'s?)
(format "Must provide a Rosette-solvable type, given ~a."
(format "Expected a Rosette-solvable type, given ~a."
(syntax->datum #'pred?))
[([x ≫ x- : (Constant ty)] ...) ⊢ [(begin e ...) ≫ e- ⇒ τ_out]]
--------
@ -794,6 +798,7 @@
[true : CTrue]
[false : CFalse]
[real->integer : (C→ Num Int)]
[number? : (C→ Any Bool)]
[positive? : (Ccase-> (C→ CNum CBool)
(C→ Num Bool))]
@ -896,6 +901,7 @@
[⊢ [_ ≫ (ro:current-bitwidth e-) ⇒ : CUnit]]])
(define-named-type-alias BV (add-predm (U CBV) bv?))
(define-named-type-alias CPred (C→ Any Bool))
(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)))
@ -979,22 +985,25 @@
;; Uninterpreted functions
(define-typed-syntax ~>
[(_ pred? ...+) ≫
[(_ pred? ...+ out) ≫
[⊢ [pred? ≫ pred?- (⇒ : _) (⇒ typefor ty) (⇒ solvable? s?) (⇒ function? f?)]] ...
#:fail-unless (stx-andmap syntax-e #'(s? ...))
(format "Must provide a Rosette-solvable type, given ~a."
(syntax->datum #'(pred? ...)))
#:fail-when (stx-ormap syntax-e #'(f? ...))
(format "Must provide a non-function Rosette type, given ~a."
(syntax->datum #'(pred? ...)))
[⊢ [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?- ...)
(→ ty ...))))
(ro:~> pred?- ... out-)
(→ ty ... ty-out))))
⇒ : (C→ Any Bool)]]])
(define-rosette-primop fv? : (C→ Any Bool))
;; ---------------------------------
;; Logic operators
(provide (rosette-typed-out [! : (C→ Bool Bool)]
@ -1123,6 +1132,11 @@
[⊢ [_ ≫ (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]]
@ -1177,6 +1191,13 @@
--------
[⊢ [_ ≫ (ro:optimize #:maximize maxe- #:minimize mine- #:guarantee ge-) ⇒ : CSolution]]])
;; ---------------------------------
;; Symbolic reflection
(define-rosette-primop term? : CPred)
(define-rosette-primop expression? : CPred)
(define-rosette-primop constant? : CPred)
;; ---------------------------------
;; Subtyping

12
turnstile/examples/tests/rosette/rosette-guide-sec2-tests.rkt
View File

@ -104,9 +104,9 @@
(define ucore (debug [integer?] (same poly factored/d 12)))
(typecheck-fail (debug [positive?] (same poly factored/d 12))
#:with-msg "Must provide a Rosette-solvable type, given.*positive?")
(typecheck-fail (debug [(~> integer?)] (same poly factored/d 12))
#:with-msg "Must provide a non-function Rosette type, given.*~> integer?")
#: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)
@ -117,9 +117,9 @@
(check-type (??) : Int)
(check-type (?? boolean?) : Bool)
(typecheck-fail (?? positive?)
#:with-msg "Must provide a Rosette-solvable type, given.*positive?")
(typecheck-fail (?? (~> integer?))
#:with-msg "Must provide a non-function Rosette type, given.*integer?")
#: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)

11
turnstile/examples/tests/rosette/rosette-guide-sec4-tests.rkt
View File

@ -1,6 +1,5 @@
#lang s-exp "../../rosette/rosette2.rkt"
(require "../rackunit-typechecking.rkt"
"check-type+asserts.rkt")
(require "../rackunit-typechecking.rkt")
;; Examples from the Rosette Guide, Section 4.1 - 4.2
@ -27,10 +26,10 @@
(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?)
#:with-msg "Must provide a Rosette\\-solvable type, given.*positive?")
(typecheck-fail (~> (~> integer?))
#:with-msg "Must provide a non\\-function Rosette type, given.*~> integer?")
(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))

3
turnstile/examples/tests/rosette/rosette-guide-sec43-tests.rkt
View File

@ -1,6 +1,5 @@
#lang s-exp "../../rosette/rosette2.rkt"
(require "../rackunit-typechecking.rkt"
"check-type+asserts.rkt")
(require "../rackunit-typechecking.rkt")
;; Examples from the Rosette Guide, Section 4.3

57
turnstile/examples/tests/rosette/rosette-guide-sec44-tests.rkt Normal file
View File

@ -0,0 +1,57 @@
#lang s-exp "../../rosette/rosette2.rkt"
(require "../rackunit-typechecking.rkt"
"check-type+asserts.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")
(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)))
(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?)
;; should this be Num or Int?
;(check-type (evaluate x sol) : Int -> 0)
(check-type (evaluate x sol) : Num -> 0) ; nondeterministic result
;; check soundness of Constant
(check-not-type (evaluate x sol) : (Constant Num))
; f is a function value
(check-type (fv? f) : Bool -> #t)
; and so is g
(check-type (fv? g) : Bool -> #t)
; 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))) ; nondet result
;; this should be the only test that is deterministic
(check-type (equal? (g 1) (g (assert-type (evaluate x sol) : Int))) : Bool -> #f)
;; ~>
(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")

2
turnstile/examples/tests/rosette/rosette2-tests.rkt
View File

@ -102,7 +102,7 @@
(define-symbolic b0 boolean?)
(define-symbolic i0 integer?)
(typecheck-fail (define-symbolic posint1 positive?)
#:with-msg "Must provide a Rosette-solvable type, given 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)

3
turnstile/examples/tests/rosette/run-all-rosette-tests-script.rkt
View File

@ -6,7 +6,8 @@
"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")
"rosette-guide-sec43-tests.rkt" "Rosette Guide, Section 4.3 BVs"
"rosette-guide-sec44-tests.rkt" "Rosette Guide, Section 4.4 Uninterp Fns")
(do-tests "bv-tests.rkt" "BV SDSL - General"
"bv-ref-tests.rkt" "BV SDSL - Hacker's Delight synthesis")