Finished moving tests to cur-test

cur-lib/cur/oll.rkt

@@ -12,7 +12,15 @@
   Var
   avar
   var-equal?
-  generate-coq)
+  generate-coq
+
+  ;; private; exported for testing only
+  (for-syntax
+   coq-defns
+   output-latex-bnf
+   output-coq
+   new-name
+   fresh-name))
 
 (begin-for-syntax
   (define-syntax-class dash
@@ -86,27 +94,6 @@
   (define (fresh-name id)
     (datum->syntax id (gensym (syntax->datum id)))))
 
-(module+ test
-  (begin-for-syntax
-    (require rackunit)
-    (define (check-id-equal? v1 v2)
-      (check-equal?
-        (syntax->datum v1)
-        (syntax->datum v2)))
-    (define (check-id-match? v1 v2)
-       (check-regexp-match
-         v1
-         (symbol->string (syntax->datum v2))))
-    (check-id-match?
-      #px"term\\d+"
-      (fresh-name #'term))
-    (check-id-equal?
-      #'stlc-lambda
-      (new-name #'stlc #'lambda))
-    (check-id-match?
-      #px"stlc-term\\d+"
-      (new-name #'stlc (fresh-name #'term)))))
-
 ;; TODO: Oh, this is a mess. Rewrite it.
 (begin-for-syntax
   (define lang-name (make-parameter #'name))
@@ -196,20 +183,7 @@
     (with-output-to-file file-name
       (thunk (printf (output-latex-bnf vars clauses)))
       #:exists 'append)))
-(module+ test
+
-  (require "stdlib/sugar.rkt")
-  (begin-for-syntax
-    (require rackunit)
-    (check-equal?
-      (format "$$\\begin{array}{lrrl}~n~a~n\\end{array}$$"
-        (format "\\mbox{\\textit{term}} & e & \\bnfdef & (e1 e2) \\bnfalt (lambda (x) e)\\\\~n"))
-      (output-latex-bnf #'(x)
-                    #'((term (e) ::= (e1 e2) (lambda (x) e)))))
-    (check-equal?
-      (format "$$\\begin{array}{lrrl}~n~a~n\\end{array}$$"
-        (format "\\mbox{\\textit{type}} & A,B,C & \\bnfdef & unit \\bnfalt (* A B) \\bnfalt (+ A C)\\\\~n"))
-      (output-latex-bnf #'(x)
-                    #'((type (A B C) ::= unit (* A B) (+ A C)))))))
 ;; TODO: For better error messages, add context, rename some of these patterns. e.g.
 ;;    (type (meta-vars) ::= ?? )
 ;; TODO: Extend define-language with syntax such as ....
@@ -243,14 +217,6 @@
      (match v2
        [(avar (n2 : Nat))
         (nat-equal? n1 n2)])]))
-(module+ test
-  (require rackunit)
-  (check-equal?
-    (var-equal? (avar z) (avar z))
-    true)
-  (check-equal?
-    (var-equal? (avar z) (avar (s z)))
-    false))
 
 ;; See stlc.rkt for examples
 
@@ -346,41 +312,3 @@
                (format "Eval compute in ~a." body))))
        (displayln (format "~a~a" (coq-defns) output))
        #'(begin))]))
-
-(module+ test
-  (begin-for-syntax
-    (check-equal?
-      (parameterize ([coq-defns ""]) (output-coq #'(data nat : Type (z : nat))) (coq-defns))
-      (format "Inductive nat : Type :=~n| z : nat.~n"))
-    (check-regexp-match
-      "(forall .+ : Type, Type)"
-      (output-coq #'(-> Type Type)))
-    (let ([t (parameterize ([coq-defns ""])
-               (output-coq #'(define-relation (meow gamma term type)
-                               [(g : gamma) (e : term) (t : type)
-                                --------------- T-Bla
-                                (meow g e t)]))
-               (coq-defns))])
-      (check-regexp-match
-        "Inductive meow : \\(forall .+ : gamma, \\(forall .+ : term, \\(forall .+ : type, Type\\)\\)\\) :="
-        (first (string-split t "\n")))
-      (check-regexp-match
-        "\\| T-Bla : \\(forall g : gamma, \\(forall e : term, \\(forall t : type, \\(\\(\\(meow g\\) e\\) t\\)\\)\\)\\)\\."
-        (second (string-split t "\n"))))
-    (let ([t (output-coq #'(elim nat Type (lambda (x : nat) nat) z
-                             (lambda* (x : nat) (ih-x : nat) ih-x)
-                             e))])
-      (check-regexp-match
-        "\\(\\(\\(\\(nat_rect \\(fun x : nat => nat\\)\\) z\\) \\(fun x : nat => \\(fun ih_x : nat => ih_x\\)\\)\\) e\\)"
-        t))
-    (check-regexp-match
-      "Definition thm_plus_commutes := \\(forall n : nat, \\(forall m : nat, \\(\\(\\(== nat\\) \\(\\(plus n\\) m\\)\\) \\(\\(plus m\\) n\\)\\)\\)\\).\n"
-      (parameterize ([coq-defns ""])
-        (output-coq #'(define thm:plus-commutes (forall* (n : nat) (m : nat)
-                                              (== nat (plus n m) (plus m n)))))
-        (coq-defns)))
-    (check-regexp-match
-      "Function add1 \\(n : nat\\)  := \\(s n\\).\n"
-      (parameterize ([coq-defns ""])
-        (output-coq #'(define (add1 (n : nat)) (s n)))
-        (coq-defns)))))

cur-lib/cur/stdlib/tactics/sartactics.rkt

@@ -124,11 +124,3 @@
             (loop (apply (lookup-tactic #'tactic)
                     (append (syntax->list #'(arg ...)) (list ps)))
                   (cons cmd cmds)))]))))
-
-(module+ test
-  (require
-    rackunit
-    "../bool.rkt")
-  (define-theorem meow (forall (x : Bool) Bool))
-  #;(proof (interactive))
-  )

cur-lib/cur/stdlib/typeclass.rkt

@@ -71,27 +71,3 @@
                     #'body))
                 #`(define #,(format-id syn "~a-~a" name #'param)
                     #,body))))]))
-
-(module+ test
-  (require rackunit)
-  (typeclass (Eqv (A : Type))
-    (equal? : (forall* (a : A) (b : A) Bool)))
-  (impl (Eqv Bool)
-    (define (equal? (a : Bool) (b : Bool))
-      (if a
-          (if b true false)
-          (if b false true))))
-  (impl (Eqv Nat)
-    (define equal? nat-equal?))
-  (check-equal?
-    (equal? z z)
-    true)
-  (check-equal?
-    (equal? z (s z))
-    false)
-  (check-equal?
-    (equal? true false)
-    false)
-  (check-equal?
-    (equal? true true)
-    true))

cur-test/cur/tests/oll.rkt

@@ -0,0 +1,85 @@
+#lang cur
+
+;; NB TODO: raco test reports incorrect number of total tests due to
+;; beign-for-syntax; but all failing tests correctly raise errors
+
+(require
+ rackunit
+ cur/stdlib/sugar
+ cur/oll)
+
+(begin-for-syntax
+  (require rackunit)
+  (define (check-id-equal? v1 v2)
+    (check-equal?
+     (syntax->datum v1)
+     (syntax->datum v2)))
+  (define (check-id-match? v1 v2)
+    (check-regexp-match
+     v1
+     (symbol->string (syntax->datum v2))))
+  (check-id-match?
+   #px"term\\d+"
+   (fresh-name #'term))
+  (check-id-equal?
+   #'stlc-lambda
+   (new-name #'stlc #'lambda))
+  (check-id-match?
+   #px"stlc-term\\d+"
+   (new-name #'stlc (fresh-name #'term))))
+
+(begin-for-syntax
+  (check-equal?
+   (format "$$\\begin{array}{lrrl}~n~a~n\\end{array}$$"
+           (format "\\mbox{\\textit{term}} & e & \\bnfdef & (e1 e2) \\bnfalt (lambda (x) e)\\\\~n"))
+   (output-latex-bnf #'(x)
+                     #'((term (e) ::= (e1 e2) (lambda (x) e)))))
+  (check-equal?
+   (format "$$\\begin{array}{lrrl}~n~a~n\\end{array}$$"
+           (format "\\mbox{\\textit{type}} & A,B,C & \\bnfdef & unit \\bnfalt (* A B) \\bnfalt (+ A C)\\\\~n"))
+   (output-latex-bnf #'(x)
+                     #'((type (A B C) ::= unit (* A B) (+ A C))))))
+
+(check-equal?
+ (var-equal? (avar z) (avar z))
+ true)
+(check-equal?
+ (var-equal? (avar z) (avar (s z)))
+ false)
+
+(begin-for-syntax
+  (check-equal?
+   (parameterize ([coq-defns ""]) (output-coq #'(data nat : Type (z : nat))) (coq-defns))
+   (format "Inductive nat : Type :=~n| z : nat.~n"))
+  (check-regexp-match
+   "(forall .+ : Type, Type)"
+   (output-coq #'(-> Type Type)))
+  (let ([t (parameterize ([coq-defns ""])
+             (output-coq #'(define-relation (meow gamma term type)
+                             [(g : gamma) (e : term) (t : type)
+                              --------------- T-Bla
+                              (meow g e t)]))
+             (coq-defns))])
+    (check-regexp-match
+     "Inductive meow : \\(forall .+ : gamma, \\(forall .+ : term, \\(forall .+ : type, Type\\)\\)\\) :="
+     (first (string-split t "\n")))
+    (check-regexp-match
+     "\\| T-Bla : \\(forall g : gamma, \\(forall e : term, \\(forall t : type, \\(\\(\\(meow g\\) e\\) t\\)\\)\\)\\)\\."
+     (second (string-split t "\n"))))
+  (let ([t (output-coq #'(elim nat Type (lambda (x : nat) nat) z
+                               (lambda* (x : nat) (ih-x : nat) ih-x)
+                               e))])
+    (check-regexp-match
+     "\\(\\(\\(\\(nat_rect \\(fun x : nat => nat\\)\\) z\\) \\(fun x : nat => \\(fun ih_x : nat => ih_x\\)\\)\\) e\\)"
+     t))
+  (check-regexp-match
+   "Definition thm_plus_commutes := \\(forall n : nat, \\(forall m : nat, \\(\\(\\(== nat\\) \\(\\(plus n\\) m\\)\\) \\(\\(plus m\\) n\\)\\)\\)\\).\n"
+   (parameterize ([coq-defns ""])
+     (output-coq #'(define thm:plus-commutes (forall* (n : nat) (m : nat)
+                                                      (== nat (plus n m) (plus m n)))))
+     (coq-defns)))
+  (check-regexp-match
+   "Function add1 \\(n : nat\\)  := \\(s n\\).\n"
+   (parameterize ([coq-defns ""])
+     (output-coq #'(define (add1 (n : nat)) (s n)))
+     (coq-defns))))

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

@@ -0,0 +1,12 @@
+#lang cur
+
+(require
+ rackunit
+ cur/stdlib/bool
+ cur/stdlib/sugar
+ cur/stdlib/tactics/base
+ cur/stdlib/tactics/sartactics)
+
+;; TODO: To much randomness for easy automated testing
+(define-theorem meow (forall (x : Bool) Bool))
+  #;(proof (interactive))

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

@@ -0,0 +1,30 @@
+#lang cur
+
+(require
+ rackunit
+ cur/stdlib/sugar
+ cur/stdlib/bool
+ cur/stdlib/nat
+ cur/stdlib/typeclass)
+
+(typeclass (Eqv (A : Type))
+           (equal? : (forall* (a : A) (b : A) Bool)))
+(impl (Eqv Bool)
+      (define (equal? (a : Bool) (b : Bool))
+        (if a
+            (if b true false)
+            (if b false true))))
+(impl (Eqv Nat)
+      (define equal? nat-equal?))
+(check-equal?
+ (equal? z z)
+ true)
+(check-equal?
+ (equal? z (s z))
+ false)
+(check-equal?
+ (equal? true false)
+ false)
+(check-equal?
+ (equal? true true)
+ true)