Moved more from cur-lib tests to cur-test

cur-lib/cur/stdlib/bool.rkt

@@ -13,29 +13,12 @@
 
 (define (not (x : Bool)) (if x false true))
 
-(module+ test
-  (require rackunit)
-  (check-equal? (not true) false)
-  (check-equal? (not false) true))
-
 (define (and (x : Bool) (y : Bool))
   (if x
       y
       (not y)))
 
-(module+ test
-  (check-equal? (and true false) false)
-  (check-equal? (and false false) true)
-  (check-equal? (and false true) false)
-  (check-equal? (and true true) true))
-
 (define (or (x : Bool) (y : Bool))
   (if x
       true
       y))
-
-(module+ test
-  (check-equal? (or true false) true)
-  (check-equal? (or false false) false)
-  (check-equal? (or false true) true)
-  (check-equal? (or true true) true))

cur-lib/cur/stdlib/maybe.rkt

@@ -11,19 +11,3 @@
    [(_ a)
     (let ([a-ty (type-infer/syn #'a)])
       #`(some #,a-ty a))]))
-
-(module+ test
-  (require rackunit "bool.rkt")
-  (check-equal?
-   (some/i true)
-   (some Bool true))
-  ;; Disabled until #22 fixed
-  #;(check-equal?
-    (case* Maybe Type (some Bool true) (Bool)
-      (lambda* (A : Type) (x : (Maybe A)) A)
-      [(none (A : Type)) IH: ()
-       false]
-      [(some (A : Type) (x : A)) IH: ()
-       ;; TODO: Don't know how to use dependency yet
-       (if x true false)])
-    true))

cur-lib/cur/stdlib/nat.rkt

@@ -3,55 +3,37 @@
 ;; TODO: override (all-defined-out) to enable exporting all these
 ;; properly.
 (provide Nat z s add1 sub1 plus mult exp square nat-equal? even? odd?)
-(module+ test
-  (require rackunit))
 
 (data Nat : Type
   (z : Nat)
   (s : (-> Nat Nat)))
 
 (define (add1 (n : Nat)) (s n))
-(module+ test
-  (check-equal? (add1 (s z)) (s (s z))))
 
 (define (sub1 (n : Nat))
   (match n
     [z z]
     [(s (x : Nat)) x]))
-(module+ test
-  (check-equal? (sub1 (s z)) z))
 
 (define (plus (n1 : Nat) (n2 : Nat))
   (match n1
     [z n2]
     [(s (x : Nat))
      (s (recur x))]))
-(module+ test
-  (check-equal? (plus z z) z)
-  (check-equal? (plus (s (s z)) (s (s z))) (s (s (s (s z))))))
 
 (define (mult (m : Nat) (n : Nat))
   (match m
     [z z]
     [(s (x : Nat))
      (plus n (recur x))]))
-(module+ test
-  (check-equal? (mult (s (s z)) z) z)
-  (check-equal? (mult (s (s z)) (s z)) (s (s z))))
 
 (define (exp (m : Nat) (e : Nat))
   (match m
     [z (s z)]
     [(s (x : Nat))
      (mult e (recur x))]))
-(module+ test
-  #;(check-equal? (exp z z) (s z))
-  #;(check-equal? (exp (s z) z) z))
 
 (define square (run (exp (s (s z)))))
-;; TODO: This test takes too long t run
-#;(module+ test
-  (check-equal? (square (s (s z))) (s (s (s (s z))))))
 
 ;; Credit to this function goes to Max
 (define nat-equal?
@@ -64,10 +46,6 @@
             false
             (lambda* (x : Nat) (ih-bla : Bool)
                      (ih x))))))
-(module+ test
-  (check-equal? (nat-equal? z z) true)
-  (check-equal? (nat-equal? z (s z)) false)
-  (check-equal? (nat-equal? (s z) (s z)) true))
 
 (define (even? (n : Nat))
   (match n
@@ -77,26 +55,3 @@
 
 (define (odd? (n : Nat))
   (not (even? n)))
-
-(module+ test
-  (check-equal?
-    (even? z)
-    true)
-  (check-equal?
-    (even? (s z))
-    false)
-  (check-equal?
-    (even? (s (s z)))
-    true)
-  (check-equal?
-    (odd? z)
-    false)
-  (check-equal?
-    (odd? (s z))
-    true)
-  (check-equal?
-    (odd? (s (s z)))
-    false)
-  #;(check-equal?
-    (odd? (s (s (s z))))
-    true))

cur-lib/cur/stdlib/prop.rkt

@@ -15,17 +15,11 @@
   thm:proj2 pf:proj2
   == refl)
 
-(module+ test
-  (require rackunit))
-
 (data True : Type (T : True))
 
 (define thm:anything-implies-true (forall (P : Type) True))
 (define pf:anything-implies-true (lambda (P : Type) T))
 
-(module+ test
-  (:: pf:anything-implies-true thm:anything-implies-true))
-
 (data False : Type)
 
 (define-type (Not (A : Type)) (-> A False))
@@ -51,9 +45,6 @@
          (And Q P))
       ((conj (P : Type) (Q : Type) (x : P) (y : Q)) IH: () (conj/i y x)))))
 
-(module+ test
-  (:: pf:and-is-symmetric thm:and-is-symmetric))
-
 (define thm:proj1
   (forall* (A : Type) (B : Type) (c : (And A B)) A))
 
@@ -63,9 +54,6 @@
       (lambda* (A : Type) (B : Type) (c : (And A B)) A)
       ((conj (A : Type) (B : Type) (a : A) (b : B)) IH: () a))))
 
-(module+ test
-  (:: pf:proj1 thm:proj1))
-
 (define thm:proj2
   (forall* (A : Type) (B : Type) (c : (And A B)) B))
 
@@ -75,9 +63,6 @@
       (lambda* (A : Type) (B : Type) (c : (And A B)) B)
       ((conj (A : Type) (B : Type) (a : A) (b : B)) IH: () b))))
 
-(module+ test
-  (:: pf:proj2 thm:proj2))
-
 #| TODO: Disabled until #22 fixed
 (data Or : (forall* (A : Type) (B : Type) Type)
   (left : (forall* (A : Type) (B : Type) (a : A) (Or A B)))
@@ -100,30 +85,3 @@
 
 (data == : (forall* (A : Type) (x : A) (-> A Type))
   (refl : (forall* (A : Type) (x : A) (== A x x))))
-
-(module+ test
-  (require  "bool.rkt" "nat.rkt")
-  (check-equal?
-    (elim == Type (λ* (A : Type) (x : A) (y : A) (p : (== A x y)) Nat)
-         (λ* (A : Type) (x : A) z)
-         Bool
-         true
-         true
-         (refl Bool true))
-    z)
-
-  (check-equal?
-    (conj/i (conj/i T T) T)
-    (conj (And True True) True (conj True True T T) T))
-
-  (define (id (A : Type) (x : A)) x)
-
-  (check-equal?
-    ((id (== True T T))
-     (refl True (run (id True T))))
-    (refl True T))
-
-  (check-equal?
-    ((id (== True T T))
-     (refl True (id True T)))
-    (refl True T)))

cur-lib/cur/stdlib/sugar.rkt

@@ -249,53 +249,3 @@
        (printf "\"~a\" has type \"~a\"~n" (syntax->datum #'term) (syntax->datum (type-infer/syn #'term)))
        ;; Void is undocumented and a hack, but sort of works
        #'(void))]))
-
-(module+ test
-  (require rackunit (submod ".."))
-
-  (check-equal?
-    ((λ* (x : (Type 1)) (y : (∀* (x : (Type 1)) (Type 1))) (y x))
-     Type
-     (λ (x : (Type 1)) x))
-    Type)
-
-  (check-equal?
-    ((λ* (x : (Type 1)) (y : (→* (Type 1) (Type 1))) (y x))
-     Type
-     (λ (x : (Type 1)) x))
-    Type)
-
-  (check-equal?
-    ((λ* (x : (Type 1)) (y : (→ (Type 1) (Type 1))) (y x))
-     Type
-     (λ (x : (Type 1)) x))
-    Type)
-
-  (check-equal?
-    (let ([x Type]
-          [y (λ (x : (Type 1)) x)])
-      (y x))
-    Type)
-
-  (check-equal?
-    (let ([(x : (Type 1)) Type]
-          [y (λ (x : (Type 1)) x)])
-      (y x))
-    Type)
-
-  ;; check that raises decent syntax error
-  ;; Can't use this because (lambda () ...) and thunk are not things in Cur at runtime
-  #;(check-exn
-    exn:fail:syntax?
-    (let ([x : (Type 1) Type]
-          [y (λ (x : (Type 1)) x)])
-      (y x)))
-
-  ;; check that raises type error
-  #;(check-exn
-    exn:fail:syntax?
-    (let ([x uninferrable-expr]
-          [y (λ (x : (Type 1)) x)])
-      (y x)))
-
-  )

cur-test/cur/tests/redex-core.rkt

@@ -1,11 +1,10 @@
 #lang racket/base
-
 (require
  redex/reduction-semantics
  cur/curnel/redex-core
  rackunit
+ racket/function
  (only-in racket/set set=?))
-
 (define-syntax-rule (check-holds (e ...))
   (check-true
    (judgment-holds (e ...))))

cur-test/cur/tests/stdlib/bool.rkt

@@ -0,0 +1,15 @@
+#lang cur
+(require rackunit)
+
+(check-equal? (not true) false)
+(check-equal? (not false) true)
+
+(check-equal? (and true false) false)
+(check-equal? (and false false) true)
+(check-equal? (and false true) false)
+(check-equal? (and true true) true)
+
+(check-equal? (or true false) true)
+(check-equal? (or false false) false)
+(check-equal? (or false true) true)
+(check-equal? (or true true) true)

cur-test/cur/tests/stdlib/maybe.rkt

@@ -0,0 +1,20 @@
+#lang cur
+
+(require
+ rackunit
+ cur/stdlib/bool
+ cur/stdlib/maybe)
+
+(check-equal?
+ (some/i true)
+ (some Bool true))
+;; Disabled until #22 fixed
+#;(check-equal?
+   (case* Maybe Type (some Bool true) (Bool)
+          (lambda* (A : Type) (x : (Maybe A)) A)
+          [(none (A : Type)) IH: ()
+           false]
+          [(some (A : Type) (x : A)) IH: ()
+           ;; TODO: Don't know how to use dependency yet
+           (if x true false)])
+   true)

cur-test/cur/tests/stdlib/nat.rkt

@@ -0,0 +1,32 @@
+#lang cur
+(require
+ cur/stdlib/sugar
+ cur/stdlib/nat
+ cur/stdlib/bool
+ rackunit)
+
+(check-equal? (add1 (s z)) (s (s z)))
+(check-equal? (sub1 (s z)) z)
+
+(check-equal? (plus z z) z)
+(check-equal? (plus (s (s z)) (s (s z))) (s (s (s (s z)))))
+
+(check-equal? (mult (s (s z)) z) z)
+(check-equal? (mult (s (s z)) (s z)) (s (s z)))
+
+;; TODO Disabled due to performance bugs
+#;(check-equal? (exp z z) (s z))
+#;(check-equal? (exp (s z) z) z)
+#;(check-equal? (square (s (s z))) (s (s (s (s z)))))
+
+(check-equal? (nat-equal? z z) true)
+(check-equal? (nat-equal? z (s z)) false)
+(check-equal? (nat-equal? (s z) (s z)) true)
+
+(check-equal? (even? z) true)
+(check-equal? (even? (s z)) false)
+(check-equal? (even? (s (s z))) true)
+(check-equal? (odd? z) false)
+(check-equal? (odd? (s z)) true)
+(check-equal? (odd? (s (s z))) false)
+(check-equal? (odd? (s (s (s z)))) true)

cur-test/cur/tests/stdlib/prop.rkt

@@ -0,0 +1,36 @@
+#lang cur
+(require
+ cur/stdlib/prop
+ cur/stdlib/sugar
+ cur/stdlib/bool
+ cur/stdlib/nat
+ rackunit)
+
+(:: pf:anything-implies-true thm:anything-implies-true)
+(:: pf:and-is-symmetric thm:and-is-symmetric)
+(:: pf:proj1 thm:proj1)
+(:: pf:proj2 thm:proj2)
+(check-equal?
+ (elim == Type (λ* (A : Type) (x : A) (y : A) (p : (== A x y)) Nat)
+       (λ* (A : Type) (x : A) z)
+       Bool
+       true
+       true
+       (refl Bool true))
+ z)
+
+(check-equal?
+ (conj/i (conj/i T T) T)
+ (conj (And True True) True (conj True True T T) T))
+
+(define (id (A : Type) (x : A)) x)
+
+(check-equal?
+ ((id (== True T T))
+  (refl True (run (id True T))))
+ (refl True T))
+
+(check-equal?
+ ((id (== True T T))
+  (refl True (id True T)))
+ (refl True T))

cur-test/cur/tests/stdlib/sugar.rkt

@@ -0,0 +1,51 @@
+#lang cur
+(require
+ rackunit
+ cur/stdlib/sugar)
+
+;; TODO: Missing tests for match, others
+(check-equal?
+ ((λ* (x : (Type 1)) (y : (∀* (x : (Type 1)) (Type 1))) (y x))
+  Type
+  (λ (x : (Type 1)) x))
+ Type)
+
+(check-equal?
+ ((λ* (x : (Type 1)) (y : (→* (Type 1) (Type 1))) (y x))
+  Type
+  (λ (x : (Type 1)) x))
+ Type)
+
+(check-equal?
+ ((λ* (x : (Type 1)) (y : (→ (Type 1) (Type 1))) (y x))
+  Type
+  (λ (x : (Type 1)) x))
+ Type)
+
+(check-equal?
+ (let ([x Type]
+       [y (λ (x : (Type 1)) x)])
+   (y x))
+ Type)
+
+(check-equal?
+ (let ([(x : (Type 1)) Type]
+       [y (λ (x : (Type 1)) x)])
+   (y x))
+ Type)
+
+;; check that raises decent syntax error
+;; Can't use this because (lambda () ...) and thunk are not things in Cur at runtime
+#;(check-exn
+   exn:fail:syntax?
+   (let ([x : (Type 1) Type]
+         [y (λ (x : (Type 1)) x)])
+     (y x)))
+
+;; check that raises type error
+#;(check-exn
+   exn:fail:syntax?
+   (let ([x uninferrable-expr]
+         [y (λ (x : (Type 1)) x)])
+     (y x)))
+

cur-test/info.rkt

@@ -1,6 +1,7 @@
 #lang info
 (define collection 'multi)
-(define deps '("base" "rackunit-lib" ("cur-lib" #:version "0.2")))
-(define build-deps '())
+(define deps '())
+(define build-deps '("base" "rackunit-lib" ("cur-lib" #:version "0.2")))
+(define update-implies '("cur-lib"))
 (define pkg-desc "Tests for \"cur\".")
 (define pkg-authors '(wilbowma))