commit 0eefdab628b809448dbc77890ff8099724b14bdc
parent cddfdc03495561c10a3f68dcd935ceab15180eee
Author: AlexKnauth <alexander@knauth.org>
Date: Wed, 24 Aug 2016 15:27:04 -0400
add case-> to rosette
Diffstat:
4 files changed, 111 insertions(+), 36 deletions(-)
diff --git a/turnstile/examples/rosette/rosette.rkt b/turnstile/examples/rosette/rosette.rkt
@@ -10,7 +10,7 @@
zero? void sub1 or and not add1 = - * + boolean? integer? list)
(for-syntax (except-in "../../../turnstile/turnstile.rkt")))
(provide (rename-out [ro:#%module-begin #%module-begin]))
-(extends "../stlc+union.rkt" #:except if #%app #%module-begin)
+(extends "../stlc+union+case.rkt" #:except if #%app #%module-begin add1 sub1 +)
(reuse List list #:from "../stlc+cons.rkt")
(require (only-in "../stlc+reco+var.rkt" [define stlc:define]))
;(require (only-in "../stlc+reco+var.rkt" define-type-alias))
@@ -49,11 +49,43 @@
(define-typed-syntax app #:export-as #%app
[(_ e_fn e_arg ...) ≫
- [⊢ [e_fn ≫ e_fn- ⇒ : (~→ τ_in ... τ_out)]]
+ [⊢ [e_fn ≫ e_fn- ⇒ : (~→ ~! τ_in ... τ_out)]]
#:fail-unless (stx-length=? #'[τ_in ...] #'[e_arg ...])
(num-args-fail-msg #'e_fn #'[τ_in ...] #'[e_arg ...])
[⊢ [e_arg ≫ e_arg- ⇐ : τ_in] ...]
--------
+ [⊢ [_ ≫ (ro:#%app e_fn- e_arg- ...) ⇒ : τ_out]]]
+ [(_ e_fn e_arg ...) ≫
+ [⊢ [e_fn ≫ e_fn- ⇒ : (~case-> ~! . (~and ty_fns ((~→ . _) ...)))]]
+ [⊢ [e_arg ≫ e_arg- ⇒ : τ_arg] ...]
+ #:with τ_out
+ (for/first ([ty_f (stx->list #'ty_fns)]
+ #:when (syntax-parse ty_f
+ [(~→ τ_in ... τ_out)
+ (and (stx-length=? #'(τ_in ...) #'(e_arg ...))
+ (typechecks? #'(τ_arg ...) #'(τ_in ...)))]))
+ (syntax-parse ty_f [(~→ _ ... t_out) #'t_out]))
+ #:fail-unless (syntax-e #'τ_out)
+ ; use (failing) typechecks? to get err msg
+ (syntax-parse #'ty_fns
+ [((~→ τ_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- e_arg- ...) ⇒ : τ_out]]])
;; ----------------------------------------------------------------------------
@@ -76,6 +108,20 @@
(define-rosette-primop string? : (→ String Bool))
(define-rosette-primop pregexp : (→ String Regexp))
+(define-rosette-primop add1 : (case-> (→ NegInt (U NegInt Zero))
+ (→ Zero PosInt)
+ (→ PosInt PosInt)
+ (→ Nat PosInt)
+ (→ Int Int)))
+(define-rosette-primop sub1 : (case-> (→ NegInt NegInt)
+ (→ Zero NegInt)
+ (→ PosInt Nat)
+ (→ Nat Int)
+ (→ Int Int)))
+(define-rosette-primop + : (case-> (→ Int Int Int)
+ (→ Nat Nat Nat)
+ (→ Num Num Num)))
+
(define-typed-syntax equal?
[(equal? e1 e2) ≫
[⊢ [e1 ≫ e1- ⇒ : ty1]]
@@ -130,35 +176,19 @@
(define-base-type BV) ; represents actual bitvectors
; a predicate recognizing bv's of a certain size
-(define-syntax BVPred
- (make-variable-like-transformer
- (add-orig #'(→ BV Bool) #'BVPred)))
-;(define-type-alias BVPred (→ BV Bool))
+(define-named-type-alias BVPred (→ BV Bool))
-;; TODO: fix me --- need subtyping?
-;(define-syntax Nat (make-rename-transformer #'Int))
-;(define-type-alias Nat Int)
-
-;; TODO: support higher order case --- need intersect types?
-(define-typed-syntax bv
- [(_ e_val e_size) ≫
- [⊢ [e_val ≫ e_val- ⇐ : Int]]
- [⊢ [e_size ≫ e_size- ⇐ : BVPred]]
- --------
- [⊢ [_ ≫ (ro:bv e_val- e_size-) ⇒ : BV]]]
- [(_ e_val e_size) ≫
- [⊢ [e_val ≫ e_val- ⇐ : Int]]
- [⊢ [e_size ≫ e_size- ⇐ : PosInt]]
- --------
- [⊢ [_ ≫ (ro:bv e_val- e_size-) ⇒ : BV]]])
+;; support higher order case with case-> types
+(define-rosette-primop bv : (case-> (→ Int BVPred BV)
+ (→ Int PosInt BV)))
(define-rosette-primop bv? : (→ BV Bool))
-(define-rosette-primop bitvector : (→ Nat BVPred))
+(define-rosette-primop bitvector : (→ PosInt BVPred))
(define-rosette-primop bitvector? : (→ BVPred Bool))
-(define-rosette-primop* bitvector bvpred : (→ Nat BVPred))
+(define-rosette-primop* bitvector bvpred : (→ PosInt BVPred))
(define-rosette-primop* bitvector? bvpred? : (→ BVPred Bool))
-(define-rosette-primop bitvector-size : (→ BVPred Nat))
-(define-rosette-primop* bitvector-size bvpred-size : (→ BVPred Nat))
+(define-rosette-primop bitvector-size : (→ BVPred PosInt))
+(define-rosette-primop* bitvector-size bvpred-size : (→ BVPred PosInt))
(define-rosette-primop bveq : (→ BV BV Bool))
(define-rosette-primop bvslt : (→ BV BV Bool))
diff --git a/turnstile/examples/stlc+union+case.rkt b/turnstile/examples/stlc+union+case.rkt
@@ -33,7 +33,7 @@
--------
[⊢ [_ ≫ (#%app- e_fn- e_arg- ...) ⇒ : τ_out]]]
[(_ e_fn e_arg ...) ≫
- [⊢ [e_fn ≫ e_fn- ⇒ : (~case-> . (~and ty_fns ((~→ . _) ...)))]]
+ [⊢ [e_fn ≫ e_fn- ⇒ : (~case-> ~! . (~and ty_fns ((~→ . _) ...)))]]
[⊢ [e_arg ≫ e_arg- ⇒ : τ_arg] ...]
#:with τ_out
(for/first ([ty_f (stx->list #'ty_fns)]
@@ -42,6 +42,26 @@
(and (stx-length=? #'(τ_in ...) #'(e_arg ...))
(typechecks? #'(τ_arg ...) #'(τ_in ...)))]))
(syntax-parse ty_f [(~→ _ ... t_out) #'t_out]))
+ #:fail-unless (syntax-e #'τ_out)
+ ; use (failing) typechecks? to get err msg
+ (syntax-parse #'ty_fns
+ [((~→ τ_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)) ", ")))])
--------
[⊢ [_ ≫ (#%app- e_fn- e_arg- ...) ⇒ : τ_out]]])
@@ -56,7 +76,7 @@
((current-type=?) t1 t2)
(syntax-parse (list t1 t2)
; 2 U types, subtype = subset
- [((~U* . tys1) (~U* . tys2))
+ [((~U* . tys1) _)
(for/and ([t (stx->list #'tys1)])
((current-sub?) t t2))]
; 1 U type, 1 non-U type. subtype = member
@@ -64,7 +84,7 @@
(for/or ([t (stx->list #'tys)])
((current-sub?) #'ty t))]
; 2 case-> types, subtype = subset
- [((~case-> . tys1) (~case-> . tys2))
+ [(_ (~case-> . tys2))
(for/and ([t (stx->list #'tys2)])
((current-sub?) t1 t))]
; 1 case-> , 1 non-case->
diff --git a/turnstile/examples/stlc+union.rkt b/turnstile/examples/stlc+union.rkt
@@ -3,6 +3,7 @@
#:except #%app #%datum + add1 sub1 * Int Int? ~Int Float Float? ~Float)
(reuse define-type-alias #:from "stlc+reco+var.rkt")
(provide Int Num Nat U
+ define-named-type-alias
(for-syntax current-sub?))
;; Simply-Typed Lambda Calculus, plus union types
@@ -21,6 +22,12 @@
;; - also *
;; Other: sub? current-sub?
+(define-syntax define-named-type-alias
+ (syntax-parser
+ [(define-named-type-alias Name:id τ:type)
+ #'(define-syntax Name
+ (make-variable-like-transformer (add-orig #'τ #'Name)))]))
+
(define-base-types Zero NegInt PosInt Float)
(define-type-constructor U* #:arity > 0)
diff --git a/turnstile/examples/tests/rosette/rosette-tests.rkt b/turnstile/examples/tests/rosette/rosette-tests.rkt
@@ -1,28 +1,30 @@
#lang s-exp "../../rosette/rosette.rkt"
(require "../rackunit-typechecking.rkt")
-(check-type (sub1 10) : Int -> 9) ; TODO: Nat
-(check-type (sub1 0) : Int -> -1) ; TODO: NegInt
-(check-type (sub1 -1) : Int -> -2) ; TODO: NegInt
+(check-type (sub1 10) : Nat -> 9)
+(check-type (sub1 0) : NegInt -> -1)
+(check-type (sub1 -1) : NegInt -> -2)
-;(check-type bv : (→ Int BVPred BV))
+(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 : (→ Nat BVPred))
+(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 : (→ Nat 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 Nat, given NegInt")
+(typecheck-fail (bvpred -1) #:with-msg "expected PosInt, given NegInt")
;(check-runtime-exn (bvpred -1))
(typecheck-fail (bitvector? "2"))
@@ -107,3 +109,19 @@
(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\\)\\)"))
+
