fix inf loop in current-sub?

- add more guide tests
This commit is contained in:
Stephen Chang 2016-08-29 16:57:50 -04:00
parent 513f6dcfd4
commit 54c0ee1cb6
3 changed files with 46 additions and 6 deletions

View File

@ -1,3 +1,9 @@
2016-08-29 --------------------
Interesting parts of Typed Rosette
- only need a single U symbolic constructor
- assert-type, using cast-type and assertion store
2016-08-25 --------------------
TODOs:
@ -13,6 +19,7 @@ TODOs:
- add Any type?
- STARTED 2016-08-26
- support internal definition contexts
- fix type of Vector and List to differentiate homogeneous/hetero
2016-08-25 --------------------

View File

@ -486,6 +486,7 @@
;; Logic operators
(define-rosette-primop ! : (C→ Bool Bool))
(define-rosette-primop <=> : (C→ Bool Bool Bool))
(define-typed-syntax &&
[(_ e ...)
@ -513,9 +514,10 @@
((current-type=?) t1 t2)
(syntax-parse (list t1 t2)
[((~CList ty1) (~CList ty2))
((current-sub?) t1 t2)]
((current-sub?) #'ty1 #'ty2)]
;; vectors are mutable and thus invariant
[((~CVector . tys1) (~CVector . tys2))
(stx-andmap (current-sub?) #'tys1 #'tys2)]
(stx-andmap (current-type=?) #'tys1 #'tys2)]
; 2 U types, subtype = subset
[((~CU* . ts1) _)
(for/and ([t (stx->list #'ts1)])

View File

@ -11,17 +11,19 @@
(check-type (boolean? b) : Bool -> #t)
(check-type (integer? b) : Bool -> #f)
;; TODO: fix these tests
(check-type (vector b 1) : (CVector Bool CPosInt) -> (vector b 1))
(check-not-type (vector b 1) : (CVector CBool CPosInt))
(check-type (vector b 1) : (CVector Bool PosInt))
(check-type (vector b 1) : (CVector Bool CInt))
(check-type (vector b 1) : (CVector Bool Int))
;; (check-not-type (vector b 1) : (CVector CBool CPosInt))
;; (check-type (vector b 1) : (CVector Bool PosInt))
;; (check-type (vector b 1) : (CVector Bool CInt))
;; (check-type (vector b 1) : (CVector Bool Int))
(check-type (not b) : Bool -> (! b))
(check-type (boolean? (not b)) : Bool -> #t)
(define-symbolic* n integer? : Int)
;; TODO: support internal definition contexts
(define (static -> Bool)
(let-symbolic ([(x) boolean? : Bool]) x))
#;(define (static -> Bool)
@ -44,3 +46,32 @@
(define y0 (dynamic))
(define y1 (dynamic))
(check-type (eq? y0 y1) : Bool -> (= y0 y1))
(define (yet-another-x -> Bool)
(let-symbolic ([(x) boolean? : Bool]) 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) : (CList 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 f x)
;; (assert (= (p x) (f x))))
;; ; check zeros; all seems well ...
;; > (same poly factored 0)
;; > (same poly factored -1)
;; > (same poly factored -2)