Fixed some bugs introduced by changes to sugar

Yesterday's changes to sugar broke some things:

* case isn't smart enough to infer the right things in all cases yet, so
  added previously existing case* for when it is necessary.
* reexport define-theorem and qed from sugar, since still used in prop.

oll.rkt

@@ -1,7 +1,10 @@
 #lang s-exp "cur.rkt"
 ;; OLL: The OTT-Like Library
 ;; TODO: Automagically create a parser from bnf grammar
-(require "stdlib/sugar.rkt" "stdlib/nat.rkt")
+(require
+  "stdlib/sugar.rkt"
+  "stdlib/nat.rkt"
+  (only-in "curnel/redex-lang.rkt" [#%app real-app]))
 
 (provide
   define-relation
@@ -236,9 +239,9 @@
 (data Var : Type (avar : (-> Nat Var)))
 
 (define (var-equal? (v1 : Var) (v2 : Var))
-  (case* Var v1 (lambda* (v : Var) Bool)
+  (case* Var v1 (lambda (v : Var) Bool)
     [(avar (n1 : Nat)) IH: ()
-     (case* Var v2 (lambda* (v : Var) Bool)
+     (case* Var v2 (lambda (v : Var) Bool)
        [(avar (n2 : Nat)) IH: ()
         (nat-equal? n1 n2)])]))
 (module+ test

scribblings/stdlib/sugar.scrbl

@@ -83,7 +83,7 @@ defining curried functions via @racket[lambda*].
 Like @racket[define], but uses @racket[forall*] instead of @racket[lambda*].
 }
 
-@defform[(case* e [pattern maybe-IH body] ...)
+@defform[(case e [pattern maybe-IH body] ...)
          #:grammar
          [(pattern
             constructor
@@ -104,6 +104,28 @@ defined.
              IH: ((_ : Bool))
              false])]
 }
+
+@defform[(case* type e motive [pattern maybe-IH body] ...)
+         #:grammar
+         [(pattern
+            constructor
+            (code:line)
+            (code:line (constructor (x : t) ...)))
+          (maybe-IH
+            (code:line)
+            (code:line IH: ((x : t) ...)))]]{
+A pattern-matcher-like syntax for inductive elimination that does not try to infer the type or motive.
+Necessary for more advanced types, like @racket[And], because @racket[case] is not very smart.
+
+@examples[#:eval curnel-eval
+          (require cur/stdlib/nat)
+          (case* Nat z (lambda (x : Bool) Nat)
+            [z true]
+            [(s (n : Nat))
+             IH: ((_ : Bool))
+             false])]
+}
+
 @defform[(run syn)]{
 Like @racket[normalize/syn], but is a syntactic form which allows a Cur term to be written by
 computing part of the term from another Cur term.

stdlib/maybe.rkt

@@ -9,8 +9,7 @@
 (module+ test
   (require rackunit "bool.rkt")
   #;(check-equal?
-    (case* Maybe (some Bool true)
-      (lambda (x : (Maybe Bool)) Bool)
+    (case (some Bool true)
       [(none (A : Type)) IH: ()
        false]
       [(some (A : Type) (x : A)) IH: ()

stdlib/sugar.rkt

@@ -6,9 +6,15 @@
   lambda*
   #%app
   define
-  case
   define-type
-  run)
+  case
+  case*
+  run
+
+  ;; don't use these
+  define-theorem
+  qed
+  )
 
 (require
   (only-in "../cur.rkt"
@@ -88,6 +94,11 @@
             [M (type-infer/syn (clause-body #'(clause* ...)))])
        #`(elim #,D e (lambda (x : #,D) #,M) #,@(map rewrite-clause (syntax->list #'(clause* ...)))))]))
 
+(define-syntax (case* syn)
+  (syntax-case syn (=>)
+    [(_ D e M clause* ...)
+     #`(elim D e M #,@(map rewrite-clause (syntax->list #'(clause* ...))))]))
+
 (define-syntax-rule (define-theorem name prop)
   (define name prop))