start rosette2
This commit is contained in:
Stephen Chang
parent
0eefdab628
commit
b30a1a9425
65
turnstile/examples/rosette/rosette2.rkt
Normal file
65
turnstile/examples/rosette/rosette2.rkt
Normal file
|
|
@ -0,0 +1,65 @@
|
|||
#lang turnstile
|
||||
(extends "../stlc.rkt")
|
||||
|
||||
(require
|
||||
(only-in "../stlc+union.rkt" prune+sort current-sub?)
|
||||
(prefix-in C (only-in "../stlc+union+case.rkt" PosInt Zero NegInt Float Bool [U U*] case-> →))
|
||||
(only-in "../stlc+union+case.rkt" [~U* ~CU*] [~case-> ~Ccase->] [~→ ~C→]))
|
||||
|
||||
(define-syntax (CU stx)
|
||||
(syntax-parse stx
|
||||
[(_ . tys)
|
||||
#:with tys+ (stx-map (current-type-eval) #'tys)
|
||||
#:fail-unless (stx-andmap concrete? #'tys+)
|
||||
"CU require concrete arguments"
|
||||
#'(CU* . tys+)]))
|
||||
|
||||
;; internal symbolic union constructor
|
||||
(define-type-constructor U* #:arity >= 0)
|
||||
(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-)]))
|
||||
|
||||
(begin-for-syntax
|
||||
(define (concrete? t)
|
||||
(not (U*? t))))
|
||||
|
||||
(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
|
||||
((current-type=?) t1 t2)
|
||||
(syntax-parse (list t1 t2)
|
||||
; 2 U types, subtype = subset
|
||||
[((~CU* . ts1) _)
|
||||
(for/and ([t (stx->list #'ts1)])
|
||||
((current-sub?) t t2))]
|
||||
; 1 U type, 1 non-U type. subtype = member
|
||||
[(_ (~CU* . ts2))
|
||||
(for/or ([t (stx->list #'ts2)])
|
||||
((current-sub?) t1 t))]
|
||||
; 2 case-> types, subtype = subset
|
||||
[(_ (~Ccase-> . ts2))
|
||||
(for/and ([t (stx->list #'ts2)])
|
||||
((current-sub?) t1 t))]
|
||||
; 1 case-> , 1 non-case->
|
||||
[((~Ccase-> . ts1) _)
|
||||
(for/or ([t (stx->list #'ts1)])
|
||||
((current-sub?) t t2))]
|
||||
[((~C→ s1 ... s2) (~C→ t1 ... t2))
|
||||
(and (subs? #'(t1 ...) #'(s1 ...))
|
||||
((current-sub?) #'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))))
|
||||
|
|
@ -4,7 +4,7 @@
|
|||
(reuse define-type-alias #:from "stlc+reco+var.rkt")
|
||||
(provide Int Num Nat U
|
||||
define-named-type-alias
|
||||
(for-syntax current-sub?))
|
||||
(for-syntax current-sub? prune+sort))
|
||||
|
||||
;; Simply-Typed Lambda Calculus, plus union types
|
||||
;; Types:
|
||||
|
|
@ -32,8 +32,12 @@
|
|||
(define-type-constructor U* #:arity > 0)
|
||||
|
||||
(define-for-syntax (prune+sort tys)
|
||||
(define ts (stx->list tys))
|
||||
(stx-sort (remove-duplicates (stx->list tys) typecheck?)))
|
||||
(stx-sort
|
||||
(remove-duplicates
|
||||
(stx->list tys)
|
||||
;; remove dups keeps first element
|
||||
;; but we want to keep supertype
|
||||
(lambda (x y) (typecheck? y x)))))
|
||||
|
||||
(define-syntax (U stx)
|
||||
(syntax-parse stx
|
||||
|
|
|
|||
127
turnstile/examples/tests/rosette/rosette2-tests.rkt
Normal file
127
turnstile/examples/tests/rosette/rosette2-tests.rkt
Normal file
|
|
@ -0,0 +1,127 @@
|
|||
#lang s-exp "../../rosette/rosette2.rkt"
|
||||
(require "../rackunit-typechecking.rkt")
|
||||
|
||||
;; (check-type (sub1 10) : Nat -> 9)
|
||||
;; (check-type (sub1 0) : NegInt -> -1)
|
||||
;; (check-type (sub1 -1) : NegInt -> -2)
|
||||
|
||||
;; (check-type bv : (case-> (→ Int BVPred BV)
|
||||
;; (→ Int PosInt BV)))
|
||||
;; (typecheck-fail (bv "1" 2) #:with-msg "expected.*Int.*given.*String")
|
||||
;; (check-type (bv 1 2) : BV -> (bv 1 (bvpred 2)))
|
||||
;; (check-type (bv 1 (bvpred 2)) : BV -> (bv 1 (bvpred 2)))
|
||||
|
||||
;; (typecheck-fail (bv 0 0) #:with-msg "expected.*PosInt.*given.*Zero")
|
||||
;; (check-type bitvector : (→ PosInt BVPred))
|
||||
;; (check-type (bitvector 3) : BVPred)
|
||||
;; (typecheck-fail ((bitvector 4) 1))
|
||||
;; (check-type ((bitvector 4) (bv 10 (bvpred 4))) : Bool)
|
||||
|
||||
;; ;; same as above, but with bvpred
|
||||
;; (check-type bvpred : (→ PosInt BVPred))
|
||||
;; (check-type (bvpred 3) : BVPred)
|
||||
;; (typecheck-fail ((bvpred 4) 1))
|
||||
;; (check-type ((bvpred 4) (bv 10 (bvpred 4))) : Bool)
|
||||
;; ;; typed rosette catches this during typechecking,
|
||||
;; ;; whereas untyped rosette uses a runtime exn
|
||||
;; (typecheck-fail (bvpred -1) #:with-msg "expected PosInt, given NegInt")
|
||||
;; ;(check-runtime-exn (bvpred -1))
|
||||
|
||||
;; (typecheck-fail (bitvector? "2"))
|
||||
;; (check-type (bitvector? (bitvector 10)) : Bool -> #t)
|
||||
;; (typecheck-fail (bvpred? "2"))
|
||||
;; (check-type (bvpred? (bvpred 10)) : Bool -> #t)
|
||||
|
||||
;; ;; bvops
|
||||
;; (check-type (bveq (bv 1 (bvpred 3)) (bv 1 (bvpred 3))) : Bool -> #t)
|
||||
;; (typecheck-fail (bveq (bv 1 (bvpred 3)) 1))
|
||||
;; (check-type (bveq (bv 1 (bvpred 2)) (bv 1 (bvpred 3))) : Bool) ; -> runtime exn
|
||||
;; (check-runtime-exn (bveq (bv 1 (bvpred 2)) (bv 1 (bvpred 3))))
|
||||
|
||||
;; ;; non-primop bvops
|
||||
;; (check-type (bvand (bv -1 (bvpred 4)) (bv 2 (bvpred 4))) : BV
|
||||
;; -> (bv 2 (bvpred 4)))
|
||||
;; (check-type (bvor (bv 0 (bvpred 3)) (bv 1 (bvpred 3))) : BV
|
||||
;; -> (bv 1 (bvpred 3)))
|
||||
;; (check-type (bvxor (bv -1 (bvpred 5)) (bv 1 (bvpred 5))) : BV
|
||||
;; -> (bv -2 (bvpred 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? : Bool)
|
||||
;; (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 issue #23
|
||||
;; (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) : BV)
|
||||
;; (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 issue #23
|
||||
;; (check-type (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 (bv -1 4) (bv 0 1) (bv -1 3)) : BV -> (bv -9 8))
|
||||
;; (check-type (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? : Int)
|
||||
;; (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? : Bool)
|
||||
;; (check-type (zero-extend (bv -3 4) (if b (bitvector 5) (bitvector 6)))
|
||||
;; : BV -> (if b (bv 13 5) (bv 13 6)))
|
||||
;; #;(check-type (zero-extend (bv -3 4) (if b (bitvector 5) "bad"))
|
||||
;; : BV -> (bv 13 5))
|
||||
;; (check-type (zero-extend (bv -3 4) (if c (bitvector 5) (bitvector 1)))
|
||||
;; : BV -> (bv 13 5))
|
||||
|
||||
;; (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 (bitvector->integer (if b (bv -1 3) "bad")) : BV -> -1)
|
||||
;; (check-type (integer->bitvector 4 (bitvector 2)) : BV -> (bv 0 2))
|
||||
;; (check-type (integer->bitvector 15 (bitvector 4)) : BV -> (bv -1 4))
|
||||
;; #;(check-type (integer->bitvector (if b pi 3)
|
||||
;; (if c (bitvector 5) (bitvector 6)))
|
||||
;; : BV -> {[c (bv 3 5)] [(! c) (bv 3 6)]})
|
||||
;; (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 : (→ Int Int)]) (f 10)) add1) : Int -> 11)
|
||||
;; (check-type ((λ ([f : (case-> (→ Int Int))]) (f 10)) add1) : Int -> 11)
|
||||
;; (check-type ((λ ([f : (case-> (→ Nat Nat)
|
||||
;; (→ Int Int))]) (f 10)) add1) : Int -> 11)
|
||||
;; (check-not-type ((λ ([f : (case-> (→ Int Int))]) (f 10)) add1) : Nat)
|
||||
;; (check-type ((λ ([f : (case-> (→ Nat Nat)
|
||||
;; (→ Int Int))]) (f 10)) add1) : Nat -> 11)
|
||||
;; (typecheck-fail ((λ ([f : (case-> (→ Zero Zero)
|
||||
;; (→ Int Int))]) (f 10)) add1)
|
||||
;; #:with-msg
|
||||
;; (string-append "expected \\(case-> \\(→ Zero Zero\\) \\(→ Int Int\\)\\), "
|
||||
;; "given \\(case-> \\(→ NegInt \\(U NegInt Zero\\)\\) \\(→ Zero PosInt\\) "
|
||||
;; "\\(→ PosInt PosInt\\) \\(→ Nat PosInt\\) \\(→ Int Int\\)\\)"))
|
||||
|
||||
Loading…
Reference in New Issue
Block a user