www

commit add4a2d7d5b09688350b195a095c5a6243277634
parent b30a1a9425c936cb38fa06e9ffe4471018ee9b21
Author: AlexKnauth <alexander@knauth.org>
Date:   Wed, 24 Aug 2016 19:42:03 -0400

more work on rosette2

Diffstat:
M
turnstile/examples/rosette/rosette2.rkt
 | 
56
++++++++++++++++++++++++++++++++++++++++++++++++++++++--
M
turnstile/examples/tests/rosette/rosette2-tests.rkt
 | 
57
+++++++++++++++++++++++++++++++++++++++++++++++++++++++++

2 files changed, 111 insertions(+), 2 deletions(-)
diff --git a/turnstile/examples/rosette/rosette2.rkt b/turnstile/examples/rosette/rosette2.rkt
@@ -1,9 +1,25 @@
 #lang turnstile
 (extends "../stlc.rkt")
+(reuse #%datum #:from "../stlc+union.rkt")
+(reuse define-type-alias #:from "../stlc+reco+var.rkt")
+(reuse define-named-type-alias #:from "../stlc+union.rkt")
+
+(provide CU U
+         CNegInt NegInt
+         CZero Zero
+         CPosInt PosInt
+         CNat Nat
+         CInt Int
+         CFloat Float
+         CNum Num
+         CBool Bool
+         CString ; symbolic string are not supported
+         )
 
 (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.rkt" define-named-type-alias prune+sort current-sub?)
+ (prefix-in C (only-in "../stlc+union+case.rkt"
+                       PosInt Zero NegInt Float Bool String [U U*] U*? case-> →))
  (only-in "../stlc+union+case.rkt" [~U* ~CU*] [~case-> ~Ccase->] [~→ ~C→]))
 
 (define-syntax (CU stx)
@@ -28,6 +44,32 @@
   (define (concrete? t)
     (not (U*? t))))
 
+;; ---------------------------------
+;; Symbolic versions of types
+
+(define-named-type-alias NegInt (U CNegInt))
+(define-named-type-alias Zero (U CZero))
+(define-named-type-alias PosInt (U CPosInt))
+(define-named-type-alias Float (U CFloat))
+(define-named-type-alias Bool (U CBool))
+
+(define-syntax define-symbolic-named-type-alias
+  (syntax-parser
+    [(_ Name:id Cτ:expr)
+     #:with Cτ+ ((current-type-eval) #'Cτ)
+     #:fail-when (and (not (concrete? #'Cτ+)) #'Cτ+)
+                 "should be a concrete type"
+     #:with CName (format-id #'Name "C~a" #'Name #:source #'Name)
+     #'(begin-
+         (define-named-type-alias CName Cτ)
+         (define-named-type-alias Name (U CName)))]))
+
+(define-symbolic-named-type-alias Nat (CU CZero CPosInt))
+(define-symbolic-named-type-alias Int (CU CNegInt CNat))
+(define-symbolic-named-type-alias Num (CU CFloat CInt))
+
+;; ---------------------------------
+
 (begin-for-syntax
   (define (sub? t1 t2)
     ; need this because recursive calls made with unexpanded types
@@ -42,8 +84,18 @@
        [((~CU* . ts1) _)
         (for/and ([t (stx->list #'ts1)])
           ((current-sub?) t t2))]
+       [((~U* . ts1) _)
+        (and
+         (not (concrete? t2))
+         (for/and ([t (stx->list #'ts1)])
+           ((current-sub?) t t2)))]
        ; 1 U type, 1 non-U type. subtype = member
        [(_ (~CU* . ts2))
+        #:when (not (or (U*? t1) (CU*? t1)))
+        (for/or ([t (stx->list #'ts2)])
+          ((current-sub?) t1 t))]
+       [(_ (~U* . ts2))
+        #:when (not (or (U*? t1) (CU*? t1)))
         (for/or ([t (stx->list #'ts2)])
           ((current-sub?) t1 t))]
        ; 2 case-> types, subtype = subset
diff --git a/turnstile/examples/tests/rosette/rosette2-tests.rkt b/turnstile/examples/tests/rosette/rosette2-tests.rkt
@@ -1,6 +1,63 @@
 #lang s-exp "../../rosette/rosette2.rkt"
 (require "../rackunit-typechecking.rkt")
 
+;; subtyping among concrete
+(check-type     ((λ ([x : CPosInt]) x) ((λ ([x : CPosInt]) x) 1)) : CPosInt -> 1)
+(check-type     ((λ ([x : CZero]) x) ((λ ([x : CZero]) x) 0)) : CZero -> 0)
+(check-type     ((λ ([x : CNegInt]) x) ((λ ([x : CNegInt]) x) -1)) : CNegInt -> -1)
+(check-type     ((λ ([x : PosInt]) x) ((λ ([x : PosInt]) x) 1)) : PosInt -> 1)
+(check-type     ((λ ([x : Zero]) x) ((λ ([x : Zero]) x) 0)) : Zero -> 0)
+(check-type     ((λ ([x : NegInt]) x) ((λ ([x : NegInt]) x) -1)) : NegInt -> -1)
+
+(check-type     ((λ ([x : CNat]) x) ((λ ([x : CZero]) x) 0)) : CNat -> 0)
+(check-type     ((λ ([x : CNat]) x) ((λ ([x : CPosInt]) x) 1)) : CNat -> 1)
+(check-type     ((λ ([x : CNat]) x) ((λ ([x : CNat]) x) 1)) : CNat -> 1)
+(typecheck-fail ((λ ([x : CPosInt]) x) ((λ ([x : CNat]) x) 1)))
+(check-type     ((λ ([x : Nat]) x) ((λ ([x : Zero]) x) 0)) : Nat -> 0)
+(check-type     ((λ ([x : Nat]) x) ((λ ([x : PosInt]) x) 1)) : Nat -> 1)
+(check-type     ((λ ([x : Nat]) x) ((λ ([x : Nat]) x) 1)) : Nat -> 1)
+(typecheck-fail ((λ ([x : PosInt]) x) ((λ ([x : Nat]) x) 1)))
+
+(check-type     ((λ ([x : CInt]) x) ((λ ([x : CNegInt]) x) -1)) : CInt -> -1)
+(check-type     ((λ ([x : CInt]) x) ((λ ([x : CZero]) x) 0)) : CInt -> 0)
+(check-type     ((λ ([x : CInt]) x) ((λ ([x : CPosInt]) x) 1)) : CInt -> 1)
+(check-type     ((λ ([x : CInt]) x) ((λ ([x : CNat]) x) 1)) : CInt -> 1)
+(check-type     ((λ ([x : CInt]) x) ((λ ([x : CInt]) x) 1)) : CInt -> 1)
+(typecheck-fail ((λ ([x : CPosInt]) x) ((λ ([x : CInt]) x) 1)))
+(typecheck-fail ((λ ([x : CNat]) x) ((λ ([x : CInt]) x) 1)))
+(check-type     ((λ ([x : Int]) x) ((λ ([x : NegInt]) x) -1)) : Int -> -1)
+(check-type     ((λ ([x : Int]) x) ((λ ([x : Zero]) x) 0)) : Int -> 0)
+(check-type     ((λ ([x : Int]) x) ((λ ([x : PosInt]) x) 1)) : Int -> 1)
+(check-type     ((λ ([x : Int]) x) ((λ ([x : Nat]) x) 1)) : Int -> 1)
+(check-type     ((λ ([x : Int]) x) ((λ ([x : Int]) x) 1)) : Int -> 1)
+(typecheck-fail ((λ ([x : PosInt]) x) ((λ ([x : Int]) x) 1)))
+(typecheck-fail ((λ ([x : Nat]) x) ((λ ([x : Int]) x) 1)))
+
+;; illustrates flattening
+(define-type-alias A Int)
+(define-type-alias B CString)
+(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-type     ((λ ([x : A-BC]) x) ((λ ([x : AC]) x) #t)) : A-BC -> #t)
+(check-type     ((λ ([x : B-AC]) x) ((λ ([x : A-BC]) x) "1")) : A-BC -> "1")
+(check-type     ((λ ([x : B-AC]) x) ((λ ([x : BC]) x) "1")) : A-BC -> "1")
+(typecheck-fail ((λ ([x : BC]) x) ((λ ([x : B-AC]) x) "1")))
+(typecheck-fail ((λ ([x : AC]) x) ((λ ([x : B-AC]) x) "1")))
+
+;; subtyping between concrete and symbolic types
+(check-type     ((λ ([x : Int]) x) ((λ ([x : CInt]) x) 1)) : Int -> 1)
+(typecheck-fail ((λ ([x : CInt]) x) ((λ ([x : Int]) x) 1)))
+(check-type     ((λ ([x : Bool]) x) ((λ ([x : CBool]) x) #t)) : Bool -> #t)
+(typecheck-fail ((λ ([x : CBool]) x) ((λ ([x : Bool]) x) #t)))
+(check-type     ((λ ([x : (U CInt CBool)]) x) ((λ ([x : (CU CInt CBool)]) x) 1)) : (U CInt CBool))
+(typecheck-fail ((λ ([x : (CU CInt CBool)]) x) ((λ ([x : (U CInt CBool)]) x) 1)))
+(check-type     ((λ ([x : (U Int Bool)]) x) ((λ ([x : (U CInt CBool)]) x) 1)) : (U CInt CBool))
+(check-type     ((λ ([x : (U CInt CBool)]) x) ((λ ([x : (U Int Bool)]) x) 1)) : (U CInt CBool))
+
 ;; (check-type (sub1 10) : Nat -> 9)
 ;; (check-type (sub1 0) : NegInt -> -1)
 ;; (check-type (sub1 -1) : NegInt -> -2)