www

commit f3014ef2e7b56fdd9a92470ec51c8f04a5a51e47
parent cc27c76ab8968d4fbd1118725c15ee207001fa08
Author: AlexKnauth <alexander@knauth.org>
Date:   Thu, 25 Aug 2016 11:09:58 -0400

rosette2: add sub1 and +

Diffstat:
M
turnstile/examples/rosette/rosette.rkt
 | 
4
++--
M
turnstile/examples/rosette/rosette2.rkt
 | 
18
++++++++++++++++++
M
turnstile/examples/tests/rosette/rosette2-tests.rkt
 | 
15
++++++++++++---

3 files changed, 32 insertions(+), 5 deletions(-)
diff --git a/turnstile/examples/rosette/rosette.rkt b/turnstile/examples/rosette/rosette.rkt
@@ -118,8 +118,8 @@
                                       (→ PosInt Nat)
                                       (→ Nat Int)
                                       (→ Int Int)))
-(define-rosette-primop + : (case-> (→ Int Int Int)
-                                   (→ Nat Nat Nat)
+(define-rosette-primop + : (case-> (→ Nat Nat Nat)
+                                   (→ Int Int Int)
                                    (→ Num Num Num)))
 
 (define-typed-syntax equal?
diff --git a/turnstile/examples/rosette/rosette2.rkt b/turnstile/examples/rosette/rosette2.rkt
@@ -166,6 +166,24 @@
                                        (C→ Nat PosInt)
                                        (C→ CInt CInt)
                                        (C→ Int Int)))
+(define-rosette-primop sub1 : (Ccase-> (C→ CNegInt CNegInt)
+                                       (C→ NegInt NegInt)
+                                       (C→ CZero CNegInt)
+                                       (C→ Zero NegInt)
+                                       (C→ CPosInt CNat)
+                                       (C→ PosInt Nat)
+                                       (C→ CNat CInt)
+                                       (C→ Nat Int)
+                                       (C→ CInt CInt)
+                                       (C→ Int Int)))
+(define-rosette-primop + : (Ccase-> (C→ CNat CNat CNat)
+                                    (C→ Nat Nat Nat)
+                                    (C→ CInt CInt CInt)
+                                    (C→ Int Int Int)
+                                    (C→ CNum CNum CNum)
+                                    (C→ Num Num Num)))
+
+
 
 ;; ---------------------------------
 ;; Subtyping
diff --git a/turnstile/examples/tests/rosette/rosette2-tests.rkt b/turnstile/examples/tests/rosette/rosette2-tests.rkt
@@ -72,9 +72,18 @@
 (check-type (add1 (ann -9 : NegInt)) : (U NegInt Zero) -> -8)
 (check-type (add1 (ann 9 : Int)) : Int -> 10)
 
-;; (check-type (sub1 10) : Nat -> 9)
-;; (check-type (sub1 0) : NegInt -> -1)
-;; (check-type (sub1 -1) : NegInt -> -2)
+;; sub1 has a similar case-> type
+(check-type (sub1 10) : CNat -> 9)
+(check-type (sub1 0) : CNegInt -> -1)
+(check-type (sub1 -1) : CNegInt -> -2)
+(check-type (sub1 (ann 10 : PosInt)) : Nat -> 9)
+(check-type (sub1 (ann 0 : Zero)) : NegInt -> -1)
+(check-type (sub1 (ann -1 : NegInt)) : NegInt -> -2)
+
+(check-type (+ 1 10) : CNat -> 11)
+(check-type (+ -10 10) : CInt -> 0)
+(check-type (+ (ann 1 : PosInt) (ann 10 : PosInt)) : Nat -> 11)
+(check-type (+ (ann -10 : NegInt) (ann 10 : PosInt)) : Int -> 0)
 
 ;; (check-type bv : (case-> (→ Int BVPred BV)
 ;;                          (→ Int PosInt BV)))