add stlc+union+case

turnstile/examples/rosette/rosette.rkt

@@ -10,10 +10,10 @@
            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 "../ext-stlc.rkt" #:except if #%app #%module-begin)
+(extends "../stlc+union.rkt" #:except if #%app #%module-begin)
 (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))
+;(require (only-in "../stlc+reco+var.rkt" define-type-alias))
 (require (prefix-in ro: rosette))
 (require (prefix-in ro: rosette/lib/synthax))
 (provide BVPred)
@@ -119,7 +119,7 @@
    --------
    [_ ≻ (begin-
           (define-syntax- f (make-rename-transformer (⊢ f- : (→ ty ... ty_out))))
-          (stlc:define f- (ext-stlc:λ ([x : ty] ...) e)))]])
+          (stlc:define f- (stlc+union:λ ([x : ty] ...) e)))]])
 
 (define-base-type Stx)
 
@@ -130,17 +130,16 @@
 (define-base-type BV) ; represents actual bitvectors
 
 ; a predicate recognizing bv's of a certain size
-#;(define-syntax BVPred 
+(define-syntax BVPred 
   (make-variable-like-transformer 
-   ((current-type-eval) #'(→ BV Bool))))
-(define-type-alias BVPred (→ BV Bool))
+   (add-orig #'(→ BV Bool) #'BVPred)))
+;(define-type-alias BVPred (→ BV Bool))
 
 ;; TODO: fix me --- need subtyping?
 ;(define-syntax Nat (make-rename-transformer #'Int))
-(define-type-alias Nat Int)
+;(define-type-alias Nat Int)
 
 ;; TODO: support higher order case --- need intersect types?
-;(define-rosette-primop bv : (→ Int BVPred BV)
 (define-typed-syntax bv
   [(_ e_val e_size) ≫
    [⊢ [e_val ≫ e_val- ⇐ : Int]]
@@ -149,7 +148,7 @@
    [⊢ [_ ≫ (ro:bv e_val- e_size-) ⇒ : BV]]]
   [(_ e_val e_size) ≫
    [⊢ [e_val ≫ e_val- ⇐ : Int]]
-   [⊢ [e_size ≫ e_size- ⇐ : Nat]]
+   [⊢ [e_size ≫ e_size- ⇐ : PosInt]]
    --------
    [⊢ [_ ≫ (ro:bv e_val- e_size-) ⇒ : BV]]])
 
@@ -158,8 +157,8 @@
 (define-rosette-primop bitvector? : (→ BVPred Bool))
 (define-rosette-primop* bitvector bvpred : (→ Nat BVPred))
 (define-rosette-primop* bitvector? bvpred? : (→ BVPred Bool))
-(define-rosette-primop bitvector-size : (→ BVPred Int))
-(define-rosette-primop* bitvector-size bvpred-size : (→ BVPred Int))
+(define-rosette-primop bitvector-size : (→ BVPred Nat))
+(define-rosette-primop* bitvector-size bvpred-size : (→ BVPred Nat))
 
 (define-rosette-primop bveq : (→ BV BV Bool))
 (define-rosette-primop bvslt : (→ BV BV Bool))

turnstile/examples/stlc+union+case.rkt

@@ -0,0 +1,85 @@
+#lang turnstile
+(extends "stlc+union.rkt"
+ #:except #%app add1 sub1)
+(provide case→)
+
+;; Simply-Typed Lambda Calculus, plus union types and case-> function types
+;; Types:
+;; - types from and stlc+union.rkt
+;; - case->
+;; Type relations:
+;; - sub?
+;; Terms:
+;; - terms from stlc+union.rkt
+;; Other: updated current-sub?
+
+(define-type-constructor case-> #:arity > 0)
+(define-syntax case→ (make-rename-transformer #'case->))
+
+(define-primop add1 : (case→ (→ Nat Nat)
+                             (→ Int Int)))
+(define-primop sub1 : (case→ (→ Zero NegInt)
+                             (→ PosInt Nat)
+                             (→ NegInt NegInt)
+                             (→ Nat Nat)
+                             (→ Int Int)))
+
+(define-typed-syntax app #:export-as #%app
+  [(_ e_fn e_arg ...) ≫
+   [⊢ [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] ...]
+   --------
+   [⊢ [_ ≫ (#%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]))
+   --------
+   [⊢ [_ ≫ (#%app- e_fn- e_arg- ...) ⇒ : τ_out]]])
+
+(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
+       [((~U* . tys1) (~U* . tys2))
+        (for/and ([t (stx->list #'tys1)])
+          ((current-sub?) t t2))]
+       ; 1 U type, 1 non-U type. subtype = member
+       [(ty (~U* . tys))
+        (for/or ([t (stx->list #'tys)])
+          ((current-sub?) #'ty t))]
+       ; 2 case-> types, subtype = subset
+       [((~case-> . tys1) (~case-> . tys2))
+        (for/and ([t (stx->list #'tys2)])
+          ((current-sub?) t1 t))]
+       ; 1 case-> , 1 non-case->
+       [((~case-> . tys) ty)
+        (for/or ([t (stx->list #'tys)])
+          ((current-sub?) t #'ty))]
+       [((~→ s1 ... s2) (~→ 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)))
+  
+  )
+                   

turnstile/examples/stlc+union.rkt

@@ -1,7 +1,9 @@
 #lang turnstile
-(extends "ext-stlc.rkt" #:except #%datum + add1 * Int Int? ~Int Float Float? ~Float)
+(extends "ext-stlc.rkt" 
+ #:except #%app #%datum + add1 sub1 * Int Int? ~Int Float Float? ~Float)
 (reuse define-type-alias #:from "stlc+reco+var.rkt")
-(provide Int Num U)
+(provide Int Num Nat U
+         (for-syntax current-sub?))
 
 ;; Simply-Typed Lambda Calculus, plus union types
 ;; Types:
@@ -19,45 +21,61 @@
 ;; - also *
 ;; Other: sub? current-sub?
 
-(define-base-types Nat NegInt Float)
+(define-base-types Zero NegInt PosInt Float)
 (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?)))
   
-  
 (define-syntax (U stx)
   (syntax-parse stx
     [(_ . tys)
+     ;; canonicalize by expanding to U*, with only (sorted and pruned) leaf tys
      #:with ((~or (~U* ty1- ...) ty2-) ...) (stx-map (current-type-eval) #'tys)
      #:with tys- (prune+sort #'(ty1- ... ... ty2- ...))
      (if (= 1 (stx-length #'tys-))
          (stx-car #'tys)
          #'(U* . tys-))]))
+(define-syntax Nat
+  (make-variable-like-transformer 
+   (add-orig #'(U Zero PosInt) #'Nat)))
 (define-syntax Int
-  (make-variable-like-transformer (add-orig #'(U Nat NegInt) #'Int)))
+  (make-variable-like-transformer 
+   (add-orig #'(U NegInt Nat) #'Int)))
 (define-syntax Num 
   (make-variable-like-transformer (add-orig #'(U Float Int) #'Num)))
 
 (define-primop + : (→ Num Num Num))
 (define-primop * : (→ Num Num Num))
 (define-primop add1 : (→ Int Int))
+(define-primop sub1 : (→ Int Int))
 
-(define-typed-syntax #%datum
-  [(#%datum . n:nat) ≫
+(define-typed-syntax datum #:export-as #%datum
+  [(_ . n:integer) ≫
+   #:with ty_out (let ([m (syntax-e #'n)])
+                   (cond [(zero? m) #'Zero]
+                         [(> m 0) #'PosInt]
+                         [else #'NegInt]))
    --------
-   [⊢ [_ ≫ (#%datum- . n) ⇒ : Nat]]]
-  [(#%datum . n:integer) ≫
-   --------
-   [⊢ [_ ≫ (#%datum- . n) ⇒ : NegInt]]]
+   [⊢ [_ ≫ (#%datum- . n) ⇒ : ty_out]]]
   [(#%datum . n:number) ≫
    #:when (real? (syntax-e #'n))
    --------
    [⊢ [_ ≫ (#%datum- . n) ⇒ : Float]]]
-  [(#%datum . x) ≫
+  [(_ . x) ≫
    --------
    [_ ≻ (ext-stlc:#%datum . x)]])
 
+(define-typed-syntax app #:export-as #%app
+  [(_ e_fn e_arg ...) ≫
+   [⊢ [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] ...]
+   --------
+   [⊢ [_ ≫ (#%app- e_fn- e_arg- ...) ⇒ : τ_out]]])
+
 (begin-for-syntax
   (define (sub? t1 t2)
     ; need this because recursive calls made with unexpanded types
@@ -68,12 +86,17 @@
     (or 
      ((current-type=?) t1 t2)
      (syntax-parse (list t1 t2)
+       ; 2 U types, subtype = subset
        [((~U* . tys1) (~U* . tys2))
         (for/and ([t (stx->list #'tys1)])
           ((current-sub?) t t2))]
+       ; 1 U type, 1 non-U type. subtype = member
        [(ty (~U* . tys))
         (for/or ([t (stx->list #'tys)])
           ((current-sub?) #'ty t))]
+       [((~→ s1 ... s2) (~→ t1 ... t2))
+        (and (subs? #'(t1 ...) #'(s1 ...))
+             ((current-sub?) #'s2 #'t2))]
        [_ #f])))
   (define current-sub? (make-parameter sub?))
   (current-typecheck-relation sub?)

turnstile/examples/tests/rackunit-typechecking.rkt

@@ -11,7 +11,7 @@
   (define (add-escs str)
     (replace-brackets
         (foldl (lambda (c s) (regexp-replace* c s (add-esc c))) str escs)))
-  (define (expected tys #:given [givens ""] #:note [note ""])
+  #;(define (expected tys #:given [givens ""] #:note [note ""])
     (string-append  
      note ".*Expected.+argument\\(s\\) with type\\(s\\).+" 
      (add-escs tys) ".*Given:.*" 

turnstile/examples/tests/rosette/rosette-tests.rkt

@@ -1,23 +1,29 @@
 #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 bv : (→ Int BVPred BV))
-(typecheck-fail (bv "1" 2) #:with-msg "expected Int, given String")
+(typecheck-fail (bv "1" 2) #:with-msg "expected.*Int.*given.*String")
 (check-type (bv 1 (bvpred 2)) : BV -> (bv 1 (bvpred 2)))
 
-(check-type bitvector : (→ Int BVPred))
+(typecheck-fail (bv 0 0) #:with-msg "expected.*PosInt.*given.*Zero")
+(check-type bitvector : (→ Nat 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 : (→ Int BVPred))
+(check-type bvpred : (→ Nat BVPred))
 (check-type (bvpred 3) : BVPred)
 (typecheck-fail ((bvpred 4) 1))
 (check-type ((bvpred 4) (bv 10 (bvpred 4))) :  Bool)
-;; TODO: add Nat to catch this at compile time?
-(check-type (bvpred -1) : BVPred) ; runtime exn
-(check-runtime-exn (bvpred -1))
+;; typed rosette catches this during typechecking, 
+;; whereas untyped rosette uses a runtime exn
+(typecheck-fail (bvpred -1) #:with-msg "expected Nat, given NegInt")
+;(check-runtime-exn (bvpred -1))
 
 (typecheck-fail (bitvector? "2"))
 (check-type (bitvector? (bitvector 10)) : Bool -> #t)

turnstile/examples/tests/stlc+union+case.rkt

@@ -0,0 +1,94 @@
+#lang s-exp "../stlc+union+case.rkt"
+(require "rackunit-typechecking.rkt")
+
+(check-type 1 : Nat)
+(check-type -1 : NegInt)
+(check-type 1.1 : Float)
+(check-type (+ 1 1.1) : Num -> 2.1)
+(check-type (+ 1.1 1) : Num -> 2.1)
+(typecheck-fail (+ "1" 1) #:with-msg "expected Num, given String")
+
+;; 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 "expected \\(case-> \\(→ Zero Zero\\) \\(→ Int Int\\)\\), given \\(case→ \\(→ Nat Nat\\) \\(→ Int Int\\)")
+
+;; Alex's example
+;; illustrates flattening
+(define-type-alias A Int)
+(define-type-alias B String)
+(define-type-alias C Bool)
+(define-type-alias AC (U A C))
+(define-type-alias BC (U B C))
+(define-type-alias A-BC (U A BC))
+(define-type-alias B-AC (U B AC))
+(check-type ((λ ([x : A-BC]) x) ((λ ([x : B-AC]) x) "1")) : A-BC -> "1")
+
+; check pruning and collapsing
+(define-type-alias NN (U Nat Nat))
+(check-type ((λ ([x : NN]) x) 1) : Nat -> 1)
+(define-type-alias NNN (U (U Nat Nat) (U (U Nat Nat Nat) (U Nat Nat))))
+(check-type ((λ ([x : NNN]) x) 1) : Nat -> 1)
+
+
+;; tests from stlc+sub ---------------------
+(check-type 1 : Num)
+(check-type 1 : Int)
+(check-type -1 : Num)
+(check-type -1 : Int)
+(check-not-type -1 : Nat)
+(check-type ((λ ([x : Num]) x) -1) : Num ⇒ -1)
+(check-type ((λ ([x : Int]) x) -1) : Int ⇒ -1)
+(typecheck-fail ((λ ([x : Nat]) x) -1) #:with-msg "expected Nat, given NegInt")
+(check-type (λ ([x : Int]) x) : (→ Int Int))
+; TODO: no function subtypes for now
+;(check-type (λ ([x : Int]) x) : (→ Int Num)) ; covariant output
+(check-not-type (λ ([x : Int]) x) : (→ Int Nat))
+;(check-type (λ ([x : Int]) x) : (→ Nat Int)) ; contravariant input
+(check-not-type (λ ([x : Int]) x) : (→ Num Int))
+
+(check-type ((λ ([f : (→ Int Int)]) (f -1)) add1) : Int ⇒ 0)
+; (check-type ((λ ([f : (→ Nat Int)]) (f 1)) add1) : Int ⇒ 2)
+(typecheck-fail ((λ ([f : (→ Num Int)]) (f 1.1)) add1))
+;(check-type ((λ ([f : (→ Nat Num)]) (f 1)) add1) : Num ⇒ 2)
+(typecheck-fail ((λ ([f : (→ Num Num)]) (f 1.1)) add1))
+
+(check-type + : (→ Num Num Num))
+;(check-type + : (→ Int Num Num))
+;(check-type + : (→ Int Int Num))
+;(check-not-type + : (→ Top Int Num))
+(check-not-type + : (→ Int Int Int))
+;(check-type + : (→ Nat Int Top))
+
+;; previous tests -------------------------------------------------------------
+;; some change due to more specific types
+(check-not-type 1 : (→ Int Int))
+(check-type "one" : String) 
+(check-type #f : Bool)
+(check-type (λ ([x : Int] [y : Int]) x) : (→ Int Int Int))
+(check-type ((λ ([x : Int] [y : Int]) x) -1 1) : Int -> -1)
+(check-not-type (λ ([x : Int]) x) : Int)
+(check-type (λ ([x : Int]) x) : (→ Int Int))
+(check-type (λ ([f : (→ Int Int)]) 1) : (→ (→ Int Int) PosInt))
+(check-type (λ ([f : (→ Int Int)]) 1) : (→ (→ Int Int) Nat))
+(check-type ((λ ([x : Int]) x) 1) : Int ⇒ 1)
+(typecheck-fail ((λ ([x : Sym]) x) 1)) ; Sym is not valid type
+(typecheck-fail (λ ([x : Sym]) x)) ; Sym is not valid type
+(typecheck-fail (λ ([f : Int]) (f 1 2))) ; applying f with non-fn type
+(check-type (λ ([f : (→ Int Int Int)] [x : Int] [y : Int]) (f x y))
+            : (→ (→ Int Int Int) Int Int Int))
+(check-type ((λ ([f : (→ Num Num Num)] [x : Int] [y : Int]) (f x y)) + 1 2) : Num ⇒ 3)
+(typecheck-fail (+ 1 (λ ([x : Int]) x))) ; adding non-Int
+(typecheck-fail (λ ([x : (→ Int Int)]) (+ x x))) ; x should be Int
+(typecheck-fail ((λ ([x : Int] [y : Int]) y) 1)) ; wrong number of args
+(check-type ((λ ([x : Int]) (+ x x)) 10) : Num ⇒ 20)
+
+(check-not-type (λ ([x : Int] [y : Int]) x) : (→ Int Int))
+(check-not-type (λ ([x : Int]) x) : (→ Int Int Int Int))

turnstile/examples/tests/stlc+union.rkt

@@ -8,6 +8,8 @@
 (check-type (+ 1.1 1) : Num -> 2.1)
 (typecheck-fail (+ "1" 1) #:with-msg "expected Num, given String")
 
+(check-type ((λ ([f : (→ Int Int)]) (f 10)) add1) : Int -> 11)
+
 ;; Alex's example
 ;; illustrates flattening
 (define-type-alias A Int)
@@ -64,6 +66,7 @@
 (check-type ((λ ([x : Int] [y : Int]) x) -1 1) : Int -> -1)
 (check-not-type (λ ([x : Int]) x) : Int)
 (check-type (λ ([x : Int]) x) : (→ Int Int))
+(check-type (λ ([f : (→ Int Int)]) 1) : (→ (→ Int Int) PosInt))
 (check-type (λ ([f : (→ Int Int)]) 1) : (→ (→ Int Int) Nat))
 (check-type ((λ ([x : Int]) x) 1) : Int ⇒ 1)
 (typecheck-fail ((λ ([x : Sym]) x) 1)) ; Sym is not valid type