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

add sec45 guide tests

Browse Source
This commit is contained in:
Stephen Chang 2016-09-09 10:59:39 -04:00
parent 5862112f57
commit 3995203803
2 changed files with 22 additions and 2 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

3
turnstile/examples/tests/rosette/rosette-guide-sec44-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.4

21
turnstile/examples/tests/rosette/rosette-guide-sec45-tests.rkt Normal file
View File

@ -0,0 +1,21 @@
#lang s-exp "../../rosette/rosette2.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))