Attempting to fix conversion rules

Currently, part of conversion is done in reduction, which is stupid

cur-doc/cur/scribblings/curnel.scrbl

@@ -17,7 +17,7 @@ Edwin C. Brady.
 @(define curnel-eval (curnel-sandbox "(require cur/stdlib/nat cur/stdlib/bool cur/stdlib/prop)"))
 
 @defform*[((Type n)
-           Type)]{
+	   Type)]{
 Define the universe of types at level @racket[n], where @racket[n] is any natural number.
 @racket[Type] is a synonym for @racket[(Type 0)]. Cur is impredicative
 in @racket[(Type 0)], although this is likely to change to a more
@@ -91,16 +91,13 @@ For instance, Cur does not currently perform strict positivity checking.
           ((((conj Bool) Bool) true) false)]
 }
 
-@defform[(elim inductive-type motive (index ...) (method ...) disc)]{
-Fold over the term @racket[disc] of the inductively defined type @racket[inductive-type].
-The @racket[motive] is a function that expects the indices of the inductive
-type and a term of the inductive type and produces the type that this
-fold returns.
-The type of @racket[disc] is @racket[(inductive-type index ...)].
-@racket[elim] takes one method for each constructor of @racket[inductive-type].
-Each @racket[method] expects the arguments for its corresponding constructor,
-and the inductive hypotheses generated by recursively eliminating all recursive
-arguments of the constructor.
+@defform[(elim type motive-universe)]{
+Returns the inductive eliminator for @racket[type] where the @racket[motive-universe] is the universe
+of the motive.
+The eliminator expects the next argument to be the motive, the next @racket[N] arguments to be the methods for
+each of the @racket[N] constructors of the inductive type @racket[type], the next @racket[P] arguments
+to be the parameters @racket[p_0 ... p_P] of the inductive @racket[type], and the final argument to be the term to
+eliminate of type @racket[(type p_0 ... p_P)].
 
 The following example runs @racket[(sub1 (s z))].
 
@@ -108,11 +105,11 @@ The following example runs @racket[(sub1 (s z))].
           (data Nat : Type
             (z : Nat)
             (s : (Π (n : Nat) Nat)))
-          (elim Nat (λ (x : Nat) Nat)
-                ()
-                (z
-                 (λ (n : Nat) (λ (IH : Nat) n)))
-                (s z))]
+          (((((elim Nat Type)
+              (λ (x : Nat) Nat))
+             z)
+            (λ (n : Nat) (λ (IH : Nat) n)))
+           (s z))]
 }
 
 @defform[(define id expr)]{
@@ -123,11 +120,9 @@ Binds @racket[id] to the result of @racket[expr].
             (z : Nat)
             (s : (Π (n : Nat) Nat)))
           (define sub1 (λ (n : Nat)
-                         (elim Nat (λ (x : Nat) Nat)
-                               ()
-                               (z
-                                (λ (n : Nat) (λ (IH : Nat) n)))
-                               n)))
+                         (((((elim Nat Type) (λ (x : Nat) Nat))
+                           z)
+                          (λ (n : Nat) (λ (IH : Nat) n))) n)))
           (sub1 (s (s z)))
           (sub1 (s z))
           (sub1 z)]

cur-doc/cur/scribblings/reflection.scrbl

@@ -76,10 +76,10 @@ Runs the Cur term @racket[syn] for one step.
 (eval:alts (cur-step #'((λ (x : Type) x) Bool))
            (eval:result @racket[#'Bool] "" ""))
 (eval:alts (cur-step #'(sub1 (s (s z))))
-           (eval:result @racket[#'(elim Nat (λ (x2 : Nat) Nat)
-                                        ()
-                                        (z (λ (x2 : Nat) (λ (ih-n2 : Nat) x2)))
-                                        (s (s z)))] "" ""))
+           (eval:result @racket[#'(((((elim Nat (Type 0))
+                                      (λ (x2 : Nat) Nat)) z)
+                                    (λ (x2 : Nat) (λ (ih-n2 : Nat) x2)))
+                                   (s (s z)))] "" ""))
 ]
 }
 

cur-doc/cur/scribblings/stdlib/bool.scrbl

@@ -22,7 +22,7 @@ A syntactic form that expands to the inductive eliminator for @racket[Bool]. Thi
 
 @examples[#:eval curnel-eval
           (if true false true)
-	  (elim Bool (λ (x : Bool) Bool) () (false true) true)]
+	  (elim Bool Type (λ (x : Bool) Bool) false true true)]
 }
 
 @defproc[(not [x Bool])

cur-doc/cur/scribblings/stdlib/sugar.scrbl

@@ -82,6 +82,17 @@ a @racket[(: name type)] form appears earlier in the module.
 	  (define (id A a) a)]
 }
 
+@defform[(elim type motive-result-type e ...)]{
+Like the @racket[elim] provided by @racketmodname[cur], but supports
+automatically curries the remaining arguments @racket[e ...].
+
+@examples[#:eval curnel-eval
+          (elim Bool Type (lambda (x : Bool) Bool)
+            false
+            true
+            true)]
+}
+
 @defform*[((define-type name type)
            (define-type (name (a : t) ...) body))]{
 Like @racket[define], but uses @racket[forall] instead of @racket[lambda].

cur-doc/info.rkt

@@ -1,6 +1,6 @@
 #lang info
 (define collection 'multi)
 (define deps '("base" "racket-doc"))
-(define build-deps '("scribble-lib" ("cur-lib" #:version "0.4") "sandbox-lib"))
+(define build-deps '("scribble-lib" ("cur-lib" #:version "0.2") "sandbox-lib"))
 (define pkg-desc "Documentation for \"cur\".")
 (define pkg-authors '(wilbowma))

cur-lib/cur/curnel/redex-core.rkt

@@ -27,10 +27,10 @@
   (i j k  ::= natural)
   (U ::= (Unv i))
   (D x c ::= variable-not-otherwise-mentioned)
+  (t e ::= U (λ (x : t) e) x (Π (x : t) t) (e e) (elim D U))
+  ;; Δ (signature). (inductive-name : type ((constructor : type) ...))
+  ;; NB: Δ is a map from a name x to a pair of it's type and a map of constructor names to their types
   (Δ   ::= ∅ (Δ (D : t ((c : t) ...))))
-  (t e ::= U (λ (x : t) e) x (Π (x : t) t) (e e)
-     ;; (elim inductive-type motive (indices ...) (methods ...) discriminant)
-     (elim D e (e ...) (e ...) e))
   #:binding-forms
   (λ (x : t) e #:refers-to x)
   (Π (x : t_0) t_1 #:refers-to x))
@@ -108,6 +108,27 @@
   [(Δ-union Δ_2 (Δ_1 (x : t any)))
    ((Δ-union Δ_2 Δ_1) (x : t any))])
 
+;; Returns the inductively defined type that x constructs
+;; NB: Depends on clause order
+(define-metafunction ttL
+  Δ-key-by-constructor : Δ x -> x or #f
+  [(Δ-key-by-constructor (Δ (x : t ((x_0 : t_0) ... (x_c : t_c) (x_1 : t_1) ...))) x_c)
+   x]
+  [(Δ-key-by-constructor (Δ (x_1 : t_1 any)) x)
+   (Δ-key-by-constructor Δ x)]
+  [(Δ-key-by-constructor Δ x)
+   #f])
+
+;; Returns the constructor map for the inductively defined type x_D in the signature Δ
+(define-metafunction ttL
+  Δ-ref-constructor-map : Δ x -> ((x : t) ...) or #f
+  ;; NB: Depends on clause order
+  [(Δ-ref-constructor-map ∅ x_D) #f]
+  [(Δ-ref-constructor-map (Δ (x_D : t_D any)) x_D)
+   any]
+  [(Δ-ref-constructor-map (Δ (x_1 : t_1 any)) x_D)
+   (Δ-ref-constructor-map Δ x_D)])
+
 ;; TODO: Should not use Δ-ref-type
 (define-metafunction ttL
   Δ-ref-constructor-type : Δ x x -> t
@@ -127,6 +148,14 @@
 ;; TODO: Mix of pure Redex/escaping to Racket sometimes is getting confusing.
 ;; TODO: Justify, or stop.
 
+;; Return the number of constructors that D has
+(define-metafunction ttL
+  Δ-constructor-count : Δ D -> natural or #f
+  [(Δ-constructor-count Δ D)
+   ,(length (term (x ...)))
+   (where (x ...) (Δ-ref-constructors Δ D))]
+  [(Δ-constructor-count Δ D) #f])
+
 ;; NB: Depends on clause order
 (define-metafunction ttL
   sequence-index-of : any (any ...) -> natural
@@ -171,23 +200,39 @@
   [(Ξ-apply hole t) t]
   [(Ξ-apply (Π (x : t) Ξ) t_0) (Ξ-apply Ξ (t_0 x))])
 
+;; Compose multiple telescopes into a single telescope:
+(define-metafunction tt-ctxtL
+  Ξ-compose : Ξ Ξ ... -> Ξ
+  [(Ξ-compose Ξ) Ξ]
+  [(Ξ-compose Ξ_0 Ξ_1 Ξ_rest ...)
+   (Ξ-compose (in-hole Ξ_0 Ξ_1) Ξ_rest ...)])
+
 ;; Compute the number of arguments in a Ξ
 (define-metafunction tt-ctxtL
   Ξ-length : Ξ -> natural
   [(Ξ-length hole) 0]
   [(Ξ-length (Π (x : t) Ξ)) ,(add1 (term (Ξ-length Ξ)))])
 
+;; Compute the number of applications in a Θ
+(define-metafunction tt-ctxtL
+  Θ-length : Θ -> natural
+  [(Θ-length hole) 0]
+  [(Θ-length (Θ e)) ,(add1 (term (Θ-length Θ)))])
+
+;; Convert an apply context to a sequence of terms
+(define-metafunction tt-ctxtL
+  Θ->list : Θ -> (e ...)
+  [(Θ->list hole) ()]
+  [(Θ->list (Θ e))
+   (e_r ... e)
+   (where (e_r ...) (Θ->list Θ))])
+
 (define-metafunction tt-ctxtL
   list->Θ : (e ...) -> Θ
   [(list->Θ ()) hole]
   [(list->Θ (e e_r ...))
    (in-hole (list->Θ (e_r ...)) (hole e))])
 
-(define-metafunction tt-ctxtL
-  apply : e e ... -> e
-  [(apply e_f e ...)
-   (in-hole (list->Θ (e ...)) e_f)])
-
 ;; Reference an expression in Θ by index; index 0 corresponds to the the expression applied to a hole.
 (define-metafunction tt-ctxtL
   Θ-ref : Θ natural -> e or #f
@@ -209,6 +254,15 @@
   [(Δ-ref-parameter-Ξ Δ x)
    #f])
 
+;; Return the number of parameters of D
+(define-metafunction tt-ctxtL
+  Δ-parameter-count : Δ D -> natural or #f
+  [(Δ-parameter-count Δ D)
+   (Ξ-length Ξ)
+   (where Ξ (Δ-ref-parameter-Ξ Δ D))]
+  [(Δ-parameter-count Δ D)
+   #f])
+
 ;; Returns the telescope of the arguments for the constructor x_ci of the inductively defined type x_D
 (define-metafunction tt-ctxtL
   Δ-constructor-telescope : Δ x x -> Ξ
@@ -226,6 +280,21 @@
    (where (in-hole Ξ (in-hole Θ x_D))
      (Δ-ref-constructor-type Δ x_D x_ci))])
 
+;; Inner loop for Δ-constructor-noninductive-telescope
+(define-metafunction tt-ctxtL
+  noninductive-loop : x Φ -> Φ
+  [(noninductive-loop x_D hole) hole]
+  [(noninductive-loop x_D (Π (x : (in-hole Φ (in-hole Θ x_D))) Φ_1))
+   (noninductive-loop x_D Φ_1)]
+  [(noninductive-loop x_D (Π (x : t) Φ_1))
+   (Π (x : t) (noninductive-loop x_D Φ_1))])
+
+;; Returns the noninductive arguments to the constructor x_ci of the inductively defined type x_D
+(define-metafunction tt-ctxtL
+  Δ-constructor-noninductive-telescope : Δ x x -> Ξ
+  [(Δ-constructor-noninductive-telescope Δ x_D x_ci)
+   (noninductive-loop x_D (Δ-constructor-telescope Δ x_D x_ci))])
+
 ;; Inner loop for Δ-constructor-inductive-telescope
 ;; NB: Depends on clause order
 (define-metafunction tt-ctxtL
@@ -254,6 +323,36 @@
       (hypotheses-loop x_D t_P Φ_1))
    (where x_h ,(variable-not-in (term (x_D t_P any_0)) 'x-ih))])
 
+;; Returns the inductive hypotheses required for the elimination method of constructor x_ci for
+;; inductive type x_D, when eliminating with motive t_P.
+(define-metafunction tt-ctxtL
+  Δ-constructor-inductive-hypotheses : Δ x x t -> Ξ
+  [(Δ-constructor-inductive-hypotheses Δ x_D x_ci t_P)
+   (hypotheses-loop x_D t_P (Δ-constructor-inductive-telescope Δ x_D x_ci))])
+
+(define-metafunction tt-ctxtL
+  Δ-constructor-method-telescope : Δ x x t -> Ξ
+  [(Δ-constructor-method-telescope Δ x_D x_ci t_P)
+   (Π (x_mi : (in-hole Ξ_a (in-hole Ξ_h ((in-hole Θ_p t_P) (Ξ-apply Ξ_a x_ci)))))
+      hole)
+   (where Θ_p (Δ-constructor-parameters Δ x_D x_ci))
+   (where Ξ_a (Δ-constructor-telescope Δ x_D x_ci))
+   (where Ξ_h (Δ-constructor-inductive-hypotheses Δ x_D x_ci t_P))
+   (where x_mi ,(variable-not-in (term (t_P Δ)) 'x-mi))])
+
+;; fold Ξ-compose over map Δ-constructor-method-telescope over the list of constructors
+(define-metafunction tt-ctxtL
+  method-loop : Δ x t (x ...) -> Ξ
+  [(method-loop Δ x_D t_P ()) hole]
+  [(method-loop Δ x_D t_P (x_0 x_rest ...))
+   (Ξ-compose (Δ-constructor-method-telescope Δ x_D x_0 t_P) (method-loop Δ x_D t_P (x_rest ...)))])
+
+;; Returns the telescope of all methods required to eliminate the type x_D with motive t_P
+(define-metafunction tt-ctxtL
+  Δ-methods-telescope : Δ x t -> Ξ
+  [(Δ-methods-telescope Δ x_D t_P)
+   (method-loop Δ x_D t_P (Δ-ref-constructors Δ x_D))])
+
 ;; Computes the type of the eliminator for the inductively defined type x_D with a motive whose result
 ;; is in universe U.
 ;;
@@ -269,40 +368,29 @@
 ;; Ξ_P*D is the telescope of the parameters of x_D and
 ;;       the witness of type x_D (applied to the parameters)
 ;; Ξ_m   is the telescope of the methods for x_D
-
-;; Returns the inductive hypotheses required for the elimination method of constructor c_i for
-;; inductive type D, when eliminating with motive t_P.
 (define-metafunction tt-ctxtL
-  Δ-constructor-inductive-hypotheses : Δ D c t -> Ξ
-  [(Δ-constructor-inductive-hypotheses Δ D c_i t_P)
-   (hypotheses-loop D t_P (Δ-constructor-inductive-telescope Δ D c_i))])
-
-;; Returns the type of the method corresponding to c_i
-(define-metafunction tt-ctxtL
-  Δ-constructor-method-type : Δ D c t -> t
-  [(Δ-constructor-method-type Δ D c_i t_P)
-   (in-hole Ξ_a (in-hole Ξ_h ((in-hole Θ_p t_P) (Ξ-apply Ξ_a c_i))))
-   (where Θ_p (Δ-constructor-parameters Δ D c_i))
-   (where Ξ_a (Δ-constructor-telescope Δ D c_i))
-   (where Ξ_h (Δ-constructor-inductive-hypotheses Δ D c_i t_P))])
-
-(define-metafunction tt-ctxtL
-  Δ-method-types : Δ D e -> (t ...)
-  [(Δ-method-types Δ D e)
-   ,(map (lambda (c) (term (Δ-constructor-method-type Δ D ,c e))) (term (c ...)))
-   (where (c ...) (Δ-ref-constructors Δ D))])
-
-(define-metafunction tt-ctxtL
-  Δ-motive-type : Δ D U -> t
-  [(Δ-motive-type Δ D U)
-   (in-hole Ξ_P*D U)
-   (where Ξ (Δ-ref-parameter-Ξ Δ D))
+  Δ-elim-type : Δ x U -> t
+  [(Δ-elim-type Δ x_D U)
+   (Π (x_P : (in-hole Ξ_P*D U))
+      ;; The methods Ξ_m for each constructor of type x_D
+      (in-hole Ξ_m
+        ;; And finally, the parameters and discriminant
+        (in-hole Ξ_P*D
+          ;; The result is (P a ... (x_D a ...)), i.e., the motive
+          ;; applied to the paramters and discriminant
+          (Ξ-apply Ξ_P*D x_P))))
+   ;; Get the parameters of x_D
+   (where Ξ (Δ-ref-parameter-Ξ Δ x_D))
    ;; A fresh name to bind the discriminant
-   (where x ,(variable-not-in (term (Δ D Ξ)) 'x-D))
+   (where x ,(variable-not-in (term (Δ Γ x_D Ξ)) 'x-D))
    ;; The telescope (∀ a -> ... -> (D a ...) hole), i.e.,
-   ;; of the indices and the inductive type applied to the
-   ;; indices
-   (where Ξ_P*D (in-hole Ξ (Π (x : (Ξ-apply Ξ D)) hole)))])
+   ;; of the parameters and the inductive type applied to the
+   ;; parameters
+   (where Ξ_P*D (in-hole Ξ (Π (x : (Ξ-apply Ξ x_D)) hole)))
+   ;; A fresh name for the motive
+   (where x_P ,(variable-not-in (term (Δ Γ x_D Ξ Ξ_P*D x)) 'x-P))
+   ;; The types of the methods for this inductive.
+   (where Ξ_m (Δ-methods-telescope Δ x_D x_P))])
 
 ;;; ------------------------------------------------------------------------
 ;;; Dynamic semantics
@@ -310,21 +398,16 @@
 ;;; inductively defined type x with a motive whose result is in universe U
 
 (define-extended-language tt-redL tt-ctxtL
-  (v  ::= x U (Π (x : t) t) (λ (x : t) t) (in-hole Θv c))
-  (Θv ::= hole (Θv v))
-  (C-elim  ::= (elim D t_P (e_i ...) (e_m ...) hole))
+  ;; NB: (in-hole Θv (elim x U)) is only a value when it's a partially applied elim. However,
+  ;; determining whether or not it is partially applied cannot be done with the grammar alone.
+  (v   ::= x U (Π (x : t) t) (λ (x : t) t) (elim x U) (in-hole Θv x) (in-hole Θv (elim x U)))
+  (Θv  ::= hole (Θv v))
   ;; call-by-value
-  (E  ::= hole (E e) (v E)
-      (elim D e (e ...) (v ... E e ...) e)
-      (elim D e (e ...) (v ...) E)
-      ;; reduce under Π (helps with typing checking)
-      ;; TODO: Should be done in conversion judgment
-      (Π (x : v) E) (Π (x : E) e)))
+  (E   ::= hole (E e) (v E)))
 
 (define Θv? (redex-match? tt-redL Θv))
 (define E? (redex-match? tt-redL E))
 (define v? (redex-match? tt-redL v))
-
 #|
  | The elim form must appear applied like so:
  | (elim D U v_P m_0 ... m_i m_j ... m_n p ... (c_i a ...))
@@ -340,6 +423,75 @@
  |
  | Using contexts, this appears as (in-hole Θ ((elim D U) v_P))
  |#
+
+
+;;; NB: Next 3 meta-function Assume of Θ n constructors, j parameters, n+j+1-th element is discriminant
+
+;; Given the apply context Θ in which an elimination of D with motive
+;; v of type U appears, extract the parameters p ... from Θ.
+(define-metafunction tt-redL
+  elim-parameters : Δ D Θ -> Θ
+  [(elim-parameters Δ D Θ)
+    ;; Drop the methods, take the parameters
+   (list->Θ
+    ,(take
+      (drop (term (Θ->list Θ)) (term (Δ-constructor-count Δ D)))
+      (term (Δ-parameter-count Δ D))))])
+
+;; Given the apply context Θ in which an elimination of D with motive
+;; v of type U appears, extract the methods m_0 ... m_n from Θ.
+(define-metafunction tt-redL
+  elim-methods : Δ D Θ -> Θ
+  [(elim-methods Δ D Θ)
+   ;; Take the methods, one for each constructor
+   (list->Θ
+    ,(take
+      (term (Θ->list Θ))
+      (term (Δ-constructor-count Δ D))))])
+
+;; Given the apply context Θ in which an elimination of D with motive
+;; v of type U appears, extract the discriminant (c_i a ...) from Θ.
+(define-metafunction tt-redL
+  elim-discriminant : Δ D Θ -> e
+  [(elim-discriminant Δ D Θ)
+   ;; Drop the methods, the parameters, and take the last element
+   ,(car
+     (drop
+      (drop (term (Θ->list Θ)) (term (Δ-constructor-count Δ D)))
+      (term (Δ-parameter-count Δ D))))])
+
+;; Check that Θ is valid and ready to be evaluated as the arguments to an elim.
+;; has length m = n + j + 1 and D has n constructors and j parameters,
+;; and the 1 represents the discriminant.
+;; discharges assumption for previous 3 meta-functions
+(define-metafunction tt-redL
+  Θ-valid : Δ D Θ -> #t or #f
+  [(Θ-valid Δ D Θ)
+   #t
+   (where natural_m (Θ-length Θ))
+   (where natural_n (Δ-constructor-count Δ D))
+   (where natural_j (Δ-parameter-count Δ D))
+   (side-condition (= (+ (term natural_n) (term natural_j) 1) (term natural_m)))
+   ;; As Cur allows reducing (through reflection) open terms, 
+   ;; check that the discriminant is a canonical form so that
+   ;; reduction can proceed; otherwise not valid.
+   (where (in-hole Θ_i c_i) (elim-discriminant Δ D Θ))
+   (where D (Δ-key-by-constructor Δ c_i))]
+  [(Θ-valid Δ D Θ) #f])
+
+(module+ test
+  (require rackunit)
+  (check-equal?
+   (term (Θ-length (((hole (s zero)) (λ (x : nat) (λ (ih-x : nat) (s (s x))))) zero)))
+   3)
+  (check-true
+   (term
+    (Θ-valid
+     ((∅ (nat : (Unv 0) ((zero : nat) (s : (Π (x : nat) nat))))) (bool : (Unv 0) ((true : bool) (false : bool))))
+     nat
+     (((hole (s zero)) (λ (x : nat) (λ (ih-x : nat) (s (s x))))) zero)))))
+
+
 (define-metafunction tt-ctxtL
   is-inductive-argument : Δ D t -> #t or #f
   ;; Think this only works in call-by-value. A better solution would
@@ -353,34 +505,39 @@
 ;; x_ci for x_D, for each inductively smaller term t_i of type (in-hole Θ_p x_D) inside Θ_i,
 ;; generate: (elim x_D U t_P  Θ_m ... Θ_p ... t_i)
 ;; TODO TTEESSSSSTTTTTTTT
-(define-metafunction tt-redL
-  Δ-inductive-elim : Δ D C-elim Θ -> Θ
+(define-metafunction tt-ctxtL
+  Δ-inductive-elim : Δ x U t Θ Θ Θ -> Θ
   ;; NB: If metafunction fails, recursive
   ;; NB: elimination will be wrong. This will introduced extremely sublte bugs,
   ;; NB: inconsistency, failure of type safety, and other bad things.
   ;; NB: It should be tested and audited thoroughly
-  [(Δ-inductive-elim any ... hole)
-   hole]
-  [(Δ-inductive-elim Δ D C-elim (Θ_c t_i))
-   ((Δ-inductive-elim Δ D C-elim Θ_c)
-    (in-hole C-elim t_i))
-   (side-condition (term (is-inductive-argument Δ D t_i)))]
-  [(Δ-inductive-elim any ... (Θ_c t_i))
-   (Δ-inductive-elim any ... Θ_c)])
+  [(Δ-inductive-elim Δ x_D U t_P Θ_p Θ_m (Θ_i t_i))
+   ((Δ-inductive-elim Δ x_D U t_P Θ_p Θ_m Θ_i)
+    (in-hole ((in-hole Θ_p Θ_m) t_i) ((elim x_D U) t_P)))
+   (side-condition (term (is-inductive-argument Δ x_D t_i)))]
+  [(Δ-inductive-elim Δ x_D U t_P Θ_p Θ_m (Θ_i t_i))
+   (Δ-inductive-elim Δ x_D U t_P Θ_p Θ_m Θ_i)]
+  [(Δ-inductive-elim Δ x_D U t_P Θ_p Θ_m hole)
+   hole])
 
 (define tt-->
   (reduction-relation tt-redL
     (--> (Δ (in-hole E ((λ (x : t_0) t_1) t_2)))
          (Δ (in-hole E (subst t_1 x t_2)))
          -->β)
-    (--> (Δ (in-hole E (elim D e_motive (e_i ...) (v_m ...) (in-hole Θv_c c))))
-         (Δ (in-hole E (in-hole Θ_mi v_mi)))
-         ;; Find the method for constructor c_i, relying on the order of the arguments.
-         (where natural (Δ-constructor-index Δ D c))
-         (where v_mi ,(list-ref (term (v_m ...)) (term natural)))
+    (--> (Δ (in-hole E (in-hole Θv ((elim D U) v_P))))
+         (Δ (in-hole E (in-hole Θ_r (in-hole Θv_i v_mi))))
+         ;; Check that Θv is valid to avoid capturing other things
+         (side-condition (term (Θ-valid Δ D Θv)))
+          ;; Split Θv into its components: the paramters Θv_P for x_D, the methods Θv_m for x_D, and
+          ;; the discriminant: the constructor c_i applied to its argument Θv_i
+         (where Θv_p (elim-parameters Δ D Θv))
+         (where Θv_m (elim-methods Δ D Θv))
+         (where (in-hole Θv_i c_i) (elim-discriminant Δ D Θv))
+         ;; Find the method for constructor x_ci, relying on the order of the arguments.
+         (where v_mi (Θ-ref Θv_m (Δ-constructor-index Δ D c_i)))
          ;; Generate the inductive recursion
-         (where Θ_ih (Δ-inductive-elim Δ D (elim D e_motive (e_i ...) (v_m ...) hole) Θv_c))
-         (where Θ_mi (in-hole Θ_ih Θv_c))
+         (where Θ_r (Δ-inductive-elim Δ D U v_P Θv_p Θv_m Θv_i))
          -->elim)))
 
 (define-metafunction tt-redL
@@ -413,15 +570,15 @@
    ----------------- "≼-Unv"
    (convert Δ Γ (Unv i_0) (Unv i_1))]
 
-  [(where t_2 (reduce Δ t_0))
-   (where t_3 (reduce Δ t_1))
-   (side-condition (α-equivalent? t_2 t_3))
+  [(where (t_2 t_2) ((reduce Δ t_0) (reduce Δ t_1)))
    ----------------- "≼-αβ"
    (convert Δ Γ t_0 t_1)]
 
-  [(convert Δ (Γ x : t_0) t_1 t_2)
+  [(where (t_a t_a) ((reduce Δ t_0) (reduce Δ t_1)))
+   (convert Δ (Γ x_0 : t_0) e_0 (subst e_1 x_1 x_0))
    ----------------- "≼-Π"
-   (convert Δ Γ (Π (x : t_0) t_1) (Π (x : t_0) t_2))])
+   (convert Δ Γ (Π (x_0 : t_0) e_0)
+                (Π (x_1 : t_1) e_1))])
 
 (define-metafunction tt-typingL
   Γ-union : Γ Γ -> Γ
@@ -541,16 +698,10 @@
    ----------------- "DTR-Application"
    (type-infer Δ Γ (e_0 e_1) t_3)]
 
-  [(type-check Δ Γ e_c (apply D e_i ...))
-
-   (type-infer Δ Γ e_motive (name t_motive (in-hole Ξ U)))
-   (convert Δ Γ t_motive (Δ-motive-type Δ D U))
-
-   (where (t_m ...) (Δ-method-types Δ D e_motive))
-   (type-check Δ Γ e_m t_m) ...
+  [(where t (Δ-elim-type Δ D U))
+   (type-infer Δ Γ t U_e)
    ----------------- "DTR-Elim_D"
-   (type-infer Δ Γ (elim D e_motive (e_i ...) (e_m ...) e_c)
-               (apply e_motive e_i ... e_c))])
+   (type-infer Δ Γ (elim D U) t)])
 
 (define-judgment-form tt-typingL
   #:mode (type-check I I I I)

cur-lib/cur/curnel/redex-lang.rkt

@@ -2,7 +2,7 @@
 ;; This module just provide module language sugar over the redex model.
 
 (require
-  (except-in "redex-core.rkt" apply)
+  "redex-core.rkt"
   redex/reduction-semantics
   racket/provide-syntax
   (for-syntax
@@ -11,7 +11,7 @@
     racket/syntax
     (except-in racket/provide-transform export)
     racket/require-transform
-    (except-in "redex-core.rkt" apply)
+    "redex-core.rkt"
     redex/reduction-semantics))
 (provide
   ;; Basic syntax
@@ -177,11 +177,10 @@
                     [e (parameterize ([gamma (extend-Γ/term gamma x t)])
                          (cur->datum #'e))])
                (term (,(syntax->datum #'b) (,x : ,t) ,e)))]
-            [(elim D motive (i ...) (m ...) d)
-             (term (elim ,(cur->datum #'D) ,(cur->datum #'motive)
-                         ,(map cur->datum (syntax->list #'(i ...)))
-                         ,(map cur->datum (syntax->list #'(m ...)))
-                         ,(cur->datum #'d)))]
+            [(elim t1 t2)
+             (let* ([t1 (cur->datum #'t1)]
+                    [t2 (cur->datum #'t2)])
+               (term (elim ,t1 ,t2)))]
             [(#%app e1 e2)
              (term (,(cur->datum #'e1) ,(cur->datum #'e2)))]))))
     (unless (or (inner-expand?) (type-infer/term reified-term))
@@ -447,9 +446,9 @@
 
 (define-syntax (dep-elim syn)
   (syntax-parse syn
-    [(_ D:id motive (i ...) (m ...) e)
+    [(_ D:id T)
      (syntax->curnel-syntax
-       (quasisyntax/loc syn (elim D motive (i ...) (m ...) e)))]))
+       (quasisyntax/loc syn (elim D T)))]))
 
 (define-syntax-rule (dep-void) (void))
 

cur-lib/cur/olly.rkt

@@ -95,18 +95,8 @@
                                      (cur->coq #'t))]))))
                "")]
             [(Type i) "Type"]
-            [(real-elim var:id motive (i ...) (m ...) d)
-             (format
-              "(~a_rect ~a~a~a ~a)"
-              (cur->coq #'var)
-              (cur->coq #'motive)
-              (for/fold ([strs ""])
-                        ([m (syntax->list #'(m ...))])
-                (format "~a ~a" strs (cur->coq m)))
-              (for/fold ([strs ""])
-                        ([i (syntax->list #'(i ...))])
-                (format "~a ~a" strs (cur->coq i)))
-              (cur->coq #'d))]
+            [(real-elim var t)
+             (format "~a_rect" (cur->coq #'var))]
             [(real-app e1 e2)
              (format "(~a ~a)" (cur->coq #'e1) (cur->coq #'e2))]
             [e:id (sanitize-id (format "~a" (syntax->datum #'e)))])))

cur-lib/cur/stdlib/prop.rkt

@@ -71,12 +71,11 @@
 (define proof:A-or-A
   (lambda (A : Type) (c : (Or A A))
     ;; TODO: What should the motive be?
-    (elim Or (lambda (A : Type) (B : Type) (c : (Or A B)) A)
-          (A A)
-          ((lambda (A : Type) (B : Type) (a : A) a)
-           ;; TODO: How do we know B is A?
-           (lambda (A : Type) (B : Type) (b : B) b))
-          c)))
+    (elim Or Type (lambda (A : Type) (B : Type) (c : (Or A B)) A)
+      (lambda (A : Type) (B : Type) (a : A) a)
+      ;; TODO: How do we know B is A?
+      (lambda (A : Type) (B : Type) (b : B) b)
+      A A c)))
 
 (qed thm:A-or-A proof:A-or-A)
 |#

cur-lib/cur/stdlib/sugar.rkt

@@ -12,6 +12,7 @@
   #%app
   define
   :
+  elim
   define-type
   match
   recur
@@ -28,6 +29,7 @@
 
 (require
   (only-in "../main.rkt"
+    [elim real-elim]
     [#%app real-app]
     [λ real-lambda]
     [Π real-Π]
@@ -161,67 +163,8 @@
      (quasisyntax/loc syn
        (real-define id body))]))
 
-#|
-(begin-for-syntax
-  (define (type->telescope syn)
-    (syntax-parse (cur-expand syn)
-      #:literals (real-Π)
-      #:datum-literals (:)
-      [(real-Π (x:id : t) body)
-       (cons #'(x : t) (type->telescope #'body))]
-      [_ '()]))
-
-  (define (type->body syn)
-    (syntax-parse syn
-      #:literals (real-Π)
-      #:datum-literals (:)
-      [(real-Π (x:id : t) body)
-       (type->body #'body)]
-      [e #'e]))
-
-  (define (constructor-indices D syn)
-    (let loop ([syn syn]
-               [args '()])
-      (syntax-parse (cur-expand syn)
-        #:literals (real-app)
-        [D:id args]
-        [(real-app e1 e2)
-         (loop #'e1 (cons #'e2 args))])))
-
-  (define (inductive-index-telescope D)
-    (type->telescope (cur-type-infer D)))
-
-  (define (inductive-method-telescope D motive)
-    (for/list ([syn (cur-constructor-map D)])
-      (with-syntax ([(c : t) syn]
-                    [name (gensym (format-symbol "~a-~a" #'c 'method))]
-                    [((arg : arg-type) ...) (type->telescope #'t)]
-                    [((rarg : rarg-type) ...) (constructor-recursive-args D #'((arg : arg-type) ...))]
-                    [((ih : ih-type) ...) (constructor-inductive-hypotheses #'((rarg : rarg-type) ...) motive)]
-                    [(iarg ...) (constructor-indices D (type->body #'t))]
-                    )
-        #`(name : (forall (arg : arg-type) ...
-                          (ih : ih-type) ...
-                          (motive iarg ...)))))))
-
-(define-syntax (elim syn)
-  (syntax-parse syn
-    [(elim D:id U e ...)
-     (with-syntax ([((x : t) ...) (inductive-index-telescope #'D)]
-                   [motive (gensym 'motive)]
-                   [y (gensym 'y)]
-                   [disc (gensym 'disc)]
-                   [((method : method-type) ...) (inductive-method-telescope #'D #'motive)])
-       #`((lambda
-            (motive : (forall (x : t) ... (y : (D x ...)) U))
-            (method : ) ...
-            (x : t) ...
-            (disc : (D x ...)) ...
-            (real-elim D motive (x ...) (method ...) disc))
-          e ...)
-       )
-     ]))
-|#
+(define-syntax-rule (elim t1 t2 e ...)
+  ((real-elim t1 t2) e ...))
 
 ;; Quite fragie to give a syntactic treatment of pattern matching -> eliminator. Replace with "Elimination with a Motive"
 (begin-for-syntax
@@ -423,9 +366,15 @@
      (quasisyntax/loc syn
        (elim
         D.inductive-name
+        #,(or
+           (cur-type-infer (attribute return-type))
+           (raise-syntax-error
+            'match
+            "Could not infer type of motive. Sorry, you'll have to use elim."
+            syn))
         motive
-        #,(attribute D.indices)
-        (c.method ...)
+        c.method ...
+        #,@(attribute D.indices)
         d))]))
 
 (begin-for-syntax

cur-lib/info.rkt

@@ -3,5 +3,5 @@
 (define deps '("base" ("redex-lib" #:version "1.11")))
 (define build-deps '())
 (define pkg-desc "implementation (no documentation, tests) part of \"cur\".")
-(define version "0.4")
+(define version "0.2")
 (define pkg-authors '(wilbowma))

cur-test/cur/tests/olly.rkt

@@ -41,12 +41,11 @@
      "\\| T-Bla : \\(forall g : gamma, \\(forall e : term, \\(forall t : type, \\(\\(\\(meow g\\) e\\) t\\)\\)\\)\\)\\."
      (second (string-split t "\n"))))
   (let ([t (cur->coq
-            #'(elim nat (lambda (x : nat) nat)
-                    ()
-                    (z (lambda (x : nat) (ih-x : nat) ih-x))
+            #'(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\\)"
+     "\\(\\(\\(\\(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"

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

@@ -81,6 +81,23 @@
    (Π (a : S) (Π (b : B) ((and S) B)))
    (subst (Π (a : A) (Π (b : B) ((and A) B))) A S))))
 
+;; Various accessor tests
+;; ------------------------------------------------------------------------
+
+(check-equal?
+ (term (Δ-key-by-constructor ,Δ zero))
+ (term nat))
+(check-equal?
+ (term (Δ-key-by-constructor ,Δ s))
+ (term nat))
+
+(check-equal?
+ (term (Δ-ref-constructor-map ,Δ nat))
+ (term ((zero : nat) (s : (Π (x : nat) nat)))))
+(check-equal?
+ (term (Δ-ref-constructor-map ,sigma false))
+ (term ()))
+
 ;; Telescope tests
 ;; ------------------------------------------------------------------------
 ;; Are these telescopes the same when filled with alpha-equivalent, and equivalently renamed, termed
@@ -98,10 +115,41 @@
  (term (Δ-ref-parameter-Ξ ,Δ4 and))
  (term (Π (A : Type) (Π (B : Type) hole))))
 
+(check-telescope-equiv?
+ (term (Ξ-compose
+        (Π (x : t_0) (Π (y : t_1) hole))
+        (Π (z : t_2) (Π (a : t_3) hole))))
+ (term (Π (x : t_0) (Π (y : t_1) (Π (z : t_2) (Π (a : t_3) hole))))))
+
+(check-telescope-equiv?
+ (term (Δ-methods-telescope ,Δ nat (λ (x : nat) nat)))
+ (term (Π (m-zero : ((λ (x : nat) nat) zero))
+          (Π (m-s : (Π (x : nat) (Π (x-ih : ((λ (x : nat) nat) x)) ((λ (x : nat) nat) (s x))))) hole))))
+(check-telescope-equiv?
+ (term (Δ-methods-telescope ,Δ nat P))
+ (term (Π (m-zero : (P zero))
+          (Π (m-s : (Π (x : nat) (Π (ih-x : (P x)) (P (s x)))))
+             hole))))
+(check-telescope-equiv?
+ (term (Δ-methods-telescope ,Δ  nat (λ (x : nat) nat)))
+ (term (Π (m-zero :  ((λ (x : nat) nat) zero))
+          (Π (m-s : (Π (x : nat) (Π (ih-x : ((λ (x : nat) nat) x)) ((λ (x : nat) nat) (s x)))))
+             hole))))
+(check-telescope-equiv?
+ (term (Δ-methods-telescope ,Δ4 and (λ (A : Type) (λ (B : Type) (λ (x : ((and A) B)) true)))))
+ (term (Π (m-conj : (Π (A : Type) (Π (B : Type) (Π (a : A) (Π (b : B)
+                                                              ((((λ (A : Type) (λ (B : Type) (λ (x : ((and A) B)) true)))
+                                                                 A)
+                                                                B)
+                                                               ((((conj A) B) a) b)))))))
+          hole)))
 (check-true (x? (term false)))
 (check-true (Ξ? (term hole)))
 (check-true (t? (term (λ (y : false) (Π (x : Type) x)))))
 (check-true (redex-match? ttL ((x : t) ...) (term ())))
+(check-telescope-equiv?
+ (term (Δ-methods-telescope ,sigma false (λ (y : false) (Π (x : Type) x))))
+ (term hole))
 
 ;; Tests for inductive elimination
 ;; ------------------------------------------------------------------------
@@ -109,32 +157,21 @@
 (check-true
  (redex-match? tt-ctxtL (in-hole Θ_i (hole (in-hole Θ_r zero))) (term (hole zero))))
 (check-telescope-equiv?
- (term (Δ-inductive-elim ,Δ nat
-                         (elim nat (λ (x : nat) nat) ()
-                               ((s zero) (λ (x : nat) (λ (ih-x : nat) (s (s x)))))
-                               hole)
+ (term (Δ-inductive-elim ,Δ nat Type (λ (x : nat) nat) hole
+                         ((hole (s zero)) (λ (x : nat) (λ (ih-x : nat) (s (s x)))))
                          (hole zero)))
- (term (hole (elim nat (λ (x : nat) nat)
-                   ()
-                   ((s zero)
-                    (λ (x : nat) (λ (ih-x : nat) (s (s x)))))
-                   zero))))
+ (term (hole (((((elim nat Type) (λ (x : nat) nat))
+                (s zero))
+               (λ (x : nat) (λ (ih-x : nat) (s (s x)))))
+              zero))))
 (check-telescope-equiv?
- (term (Δ-inductive-elim ,Δ nat
-                         (elim nat (λ (x : nat) nat) ()
-                               ((s zero) (λ (x : nat) (λ (ih-x : nat) (s (s x)))))
-                               hole)
+ (term (Δ-inductive-elim ,Δ nat Type (λ (x : nat) nat) hole
+                         ((hole (s zero)) (λ (x : nat) (λ (ih-x : nat) (s (s x)))))
                          (hole (s zero))))
- (term (hole (elim nat (λ (x : nat) nat) ()
-                   ((s zero) (λ (x : nat) (λ (ih-x : nat) (s (s x)))))
-                   (s zero)))))
-(check-telescope-equiv?
- (term (Δ-inductive-elim ,Δ nat
-                         (elim nat (λ (x : nat) nat) ()
-                               ((s zero) (λ (x : nat) (λ (ih-x : nat) (s (s x)))))
-                               hole)
-                         hole))
- (term hole))
+ (term (hole (((((elim nat Type) (λ (x : nat) nat))
+                (s zero))
+               (λ (x : nat) (λ (ih-x : nat) (s (s x)))))
+              (s zero)))))
 
 ;; Tests for dynamic semantics
 ;; ------------------------------------------------------------------------
@@ -142,8 +179,6 @@
 (check-true (v? (term (λ (x_0 : (Unv 0)) x_0))))
 (check-true (v? (term (refl Nat))))
 (check-true (v? (term ((refl Nat) z))))
-(check-true (v? (term zero)))
-(check-true (v? (term (s zero))))
 
 ;; TODO: Move equivalence up here, and use in these tests.
 (check-equiv? (term (reduce ∅ (Unv 0))) (term (Unv 0)))
@@ -153,68 +188,60 @@
                   (term (Π (x : t) (Unv 0))))
 (check-not-equiv? (term (reduce ∅ (Π (x : t) ((Π (x_0 : t) (x_0 x)) x))))
                   (term (Π (x : t) (x x))))
-
-(check-equal? (term (Δ-constructor-index ,Δ nat zero)) 0)
-(check-equiv? (term (reduce ,Δ (elim nat (λ (x : nat) nat)
-                                     ()
-                                     ((s zero)
-                                      (λ (x : nat) (λ (ih-x : nat) (s (s x)))))
-                                     zero)))
+(check-equiv? (term (reduce ,Δ (((((elim nat Type) (λ (x : nat) nat))
+                                  (s zero))
+                                 (λ (x : nat) (λ (ih-x : nat)
+                                                (s (s x)))))
+                                zero)))
               (term (s zero)))
-(check-equiv? (term (reduce ,Δ (elim nat (λ (x : nat) nat)
-                                     ()
-                                     ((s zero)
-                                      (λ (x : nat) (λ (ih-x : nat) (s (s x)))))
-                                     (s zero))))
+(check-equiv? (term (reduce ,Δ (((((elim nat Type) (λ (x : nat) nat))
+                                  (s zero))
+                                 (λ (x : nat) (λ (ih-x : nat)
+                                                (s (s x)))))
+                                (s zero))))
               (term (s (s zero))))
-(check-equiv? (term (reduce ,Δ (elim nat (λ (x : nat) nat)
-                                     ()
-                                     ((s zero)
-                                      (λ (x : nat) (λ (ih-x : nat) (s (s x)))))
+(check-equiv? (term (reduce ,Δ (((((elim nat Type) (λ (x : nat) nat))
+                                  (s zero))
+                                 (λ (x : nat) (λ (ih-x : nat) (s (s x)))))
                                 (s (s (s zero))))))
               (term (s (s (s (s zero))))))
 
 (check-equiv?
  (term (reduce ,Δ
-               (elim nat (λ (x : nat) nat)
-                     ()
-                     ((s (s zero))
-                      (λ (x : nat) (λ (ih-x : nat) (s ih-x))))
-                     (s (s zero)))))
+               (((((elim nat Type) (λ (x : nat) nat))
+                  (s (s zero)))
+                 (λ (x : nat) (λ (ih-x : nat) (s ih-x))))
+                (s (s zero)))))
  (term (s (s (s (s zero))))))
 (check-equiv?
  (term (step ,Δ
-             (elim nat (λ (x : nat) nat)
-                     ()
-                     ((s (s zero))
-                      (λ (x : nat) (λ (ih-x : nat) (s ih-x))))
-                     (s (s zero)))))
+             (((((elim nat Type) (λ (x : nat) nat))
+                (s (s zero)))
+               (λ (x : nat) (λ (ih-x : nat) (s ih-x))))
+              (s (s zero)))))
  (term
   (((λ (x : nat) (λ (ih-x : nat) (s ih-x)))
     (s zero))
-   (elim nat (λ (x : nat) nat)
-         ()
-         ((s (s zero))
-          (λ (x : nat) (λ (ih-x : nat) (s ih-x))))
-         (s zero)))))
+   (((((elim nat Type) (λ (x : nat) nat))
+      (s (s zero)))
+     (λ (x : nat) (λ (ih-x : nat) (s ih-x))))
+    (s zero)))))
 (check-equiv?
  (term (step ,Δ (step ,Δ
                       (((λ (x : nat) (λ (ih-x : nat) (s ih-x)))
                         (s zero))
-                       (elim nat (λ (x : nat) nat)
-                             ()
-                             ((s (s zero))
-                              (λ (x : nat) (λ (ih-x : nat) (s ih-x))))
-                             (s zero))))))
+                       (((((elim nat Type) (λ (x : nat) nat))
+                          (s (s zero)))
+                         (λ (x : nat) (λ (ih-x : nat) (s ih-x))))
+                        (s zero))))))
  (term
   ((λ (ih-x1 : nat) (s ih-x1))
    (((λ (x : nat) (λ (ih-x : nat) (s ih-x)))
      zero)
-    (elim nat (λ (x : nat) nat)
-          ()
-          ((s (s zero))
-           (λ (x : nat) (λ (ih-x : nat) (s ih-x))))
-          zero)))))
+    (((((elim nat Type) (λ (x : nat) nat))
+       (s (s zero)))
+      (λ (x : nat) (λ (ih-x : nat) (s ih-x))))
+     zero)))))
 
 (define-syntax-rule (check-equivalent e1 e2)
   (check-holds (convert ∅ ∅ e1 e2)))
@@ -316,42 +343,28 @@
                U))
 ;; ---- Elim
 ;; TODO: Clean up/Reorganize these tests
+(check-true
+ (redex-match? tt-typingL
+               (in-hole Θ_m (((elim x_D U) e_D) e_P))
+               (term ((((elim truth Type) T) (Π (x : truth) (Unv 1))) (Unv 0)))))
 (define Δtruth (term (∅ (truth : (Unv 0) ((T : truth))))))
 (check-holds (type-infer ,Δtruth ∅ truth (in-hole Ξ U)))
 (check-holds (type-infer ,Δtruth ∅ T (in-hole Θ_ai truth)))
 (check-holds (type-infer ,Δtruth ∅ (λ (x : truth) (Unv 1))
                          (in-hole Ξ (Π (x : (in-hole Θ truth)) U))))
 
-(check-equiv?
- (term (Δ-motive-type ,Δtruth truth (Unv 2)))
- (term (Π (x : truth) (Unv 2))))
-
-
-(check-holds (type-check ,Δtruth ∅ (Unv 0) ,(car (term (Δ-method-types ,Δtruth truth (λ (x : truth) (Unv 1)))))))
-
-(check-holds (type-check ,Δtruth ∅ (λ (x : truth) (Unv 1)) (Π (x : truth) (Unv 2))))
-
-(check-equiv?
- (term (apply (λ (x : truth) (Unv 1)) T))
- (term ((λ (x : truth) (Unv 1)) T)))
-
-(check-holds
- (convert ,Δtruth ∅ (apply (λ (x : truth) (Unv 1)) T) (Unv 1)))
-
-(check-holds (type-infer ,Δtruth
+(check-telescope-equiv?
+ (term (Δ-methods-telescope ,Δtruth truth (λ (x : truth) (Unv 1))))
+ (term (Π (m-T : ((λ (x : truth) (Unv 1)) T)) hole)))
+(check-holds (type-infer ,Δtruth ∅ (elim truth Type) t))
+(check-holds (type-check (∅ (truth : (Unv 0) ((T : truth))))
                          ∅
-                         (elim truth (λ (x : truth) (Unv 1))
-                               () ((Unv 0)) T)
-                         t))
-
-(check-holds (type-check ,Δtruth
-                         ∅
-                         (elim truth (λ (x : truth) (Unv 1))
-                               () ((Unv 0)) T)
+                         ((((elim truth (Unv 2)) (λ (x : truth) (Unv 1))) (Unv 0))
+                          T)
                          (Unv 1)))
 (check-not-holds (type-check (∅ (truth : (Unv 0) ((T : truth))))
                              ∅
-                             (elim truth Type () (Type) T)
+                             ((((elim truth (Unv 1)) Type) Type) T)
                              (Unv 1)))
 (check-holds
  (type-infer ∅ ∅ (Π (x2 : (Unv 0)) (Unv 0)) U))
@@ -369,54 +382,47 @@
   (check-holds (type-check ,Δ syn ...)))
 (nat-test ∅ (Π (x : nat) nat) (Unv 0))
 (nat-test ∅ (λ (x : nat) x) (Π (x : nat) nat))
-(nat-test ∅ (elim nat (λ (x : nat) nat) ()
-                  (zero (λ (x : nat) (λ (ih-x : nat) x)))
-                  zero)
+(nat-test ∅ (((((elim nat Type) (λ (x : nat) nat)) zero)
+              (λ (x : nat) (λ (ih-x : nat) x))) zero)
             nat)
 (nat-test ∅ nat (Unv 0))
 (nat-test ∅ zero nat)
 (nat-test ∅ s (Π (x : nat) nat))
 (nat-test ∅ (s zero) nat)
+;; TODO: Meta-function auto-currying and such
 (check-holds
- (type-infer ,Δ ∅ (λ (x : nat)
-                    (elim nat (λ (x : nat) nat)
-                          ()
-                          (zero
-                           (λ (x : nat) (λ (ih-x : nat) x)))
-                          x))
+ (type-infer ,Δ ∅ ((((elim nat (Unv 0)) (λ (x : nat) nat))
+                    zero)
+                   (λ (x : nat) (λ (ih-x : nat) x)))
              t))
-(nat-test ∅ (elim nat (λ (x : nat) nat)
-                  ()
-                  (zero (λ (x : nat) (λ (ih-x : nat) x)))
-                  zero)
+(nat-test ∅ (((((elim nat (Unv 0)) (λ (x : nat) nat))
+               zero)
+              (λ (x : nat) (λ (ih-x : nat) x)))
+             zero)
             nat)
-(nat-test ∅ (elim nat (λ (x : nat) nat)
-                  ()
-                  ((s zero) (λ (x : nat) (λ (ih-x : nat) (s (s x)))))
-                  zero)
+(nat-test ∅ (((((elim nat (Unv 0)) (λ (x : nat) nat))
+               (s zero))
+              (λ (x : nat) (λ (ih-x : nat) (s (s x)))))
+             zero)
             nat)
-(nat-test ∅ (elim nat (λ (x : nat) nat)
-                  ()
-                  ((s zero) (λ (x : nat) (λ (ih-x : nat) (s (s x)))))
-                  zero)
+(nat-test ∅ (((((elim nat Type) (λ (x : nat) nat))
+               (s zero))
+              (λ (x : nat) (λ (ih-x : nat) (s (s x))))) zero)
             nat)
 (nat-test (∅ n : nat)
-          (elim nat (λ (x : nat) nat)
-                ()
-                (zero (λ (x : nat) (λ (ih-x : nat) x)))
-                n)
+          (((((elim nat (Unv 0)) (λ (x : nat) nat)) zero) (λ (x : nat) (λ (ih-x : nat) x))) n)
           nat)
 (check-holds
  (type-check (,Δ (bool : (Unv 0) ((btrue : bool) (bfalse : bool))))
              (∅ n2 : nat)
-             (elim nat (λ (x : nat) bool)
-                   ()
-                   (btrue (λ (x : nat) (λ (ih-x : bool) bfalse)))
-                   n2)
+             (((((elim nat (Unv 0)) (λ (x : nat) bool))
+                btrue)
+               (λ (x : nat) (λ (ih-x : bool) bfalse)))
+              n2)
              bool))
 (check-not-holds
  (type-check ,Δ ∅
-             (elim nat nat () ((s zero)) zero)
+             ((((elim nat (Unv 0)) nat) (s zero)) zero)
              nat))
 (define lam (term (λ (nat : (Unv 0)) nat)))
 (check-equivalent
@@ -475,15 +481,15 @@
              (in-hole Ξ (Π (x : (in-hole Θ_Ξ and)) U_P))))
 (check-holds
  (type-check (,Δ4 (true : (Unv 0) ((tt : true)))) ∅
-             (elim and
-                   (λ (A : Type) (λ (B : Type) (λ (x : ((and A) B))
-                                                 true)))
-                   (true true)
-                   ((λ (A : (Unv 0))
-                      (λ (B : (Unv 0))
-                        (λ (a : A)
-                          (λ (b : B) tt)))))
-                   ((((conj true) true) tt) tt))
+             ((((((elim and (Unv 0))
+                  (λ (A : Type) (λ (B : Type) (λ (x : ((and A) B))
+                                                true))))
+                 (λ (A : (Unv 0))
+                   (λ (B : (Unv 0))
+                     (λ (a : A)
+                       (λ (b : B) tt)))))
+                true) true)
+              ((((conj true) true) tt) tt))
              true))
 (check-true (Γ? (term (((∅ P : (Unv 0)) Q : (Unv 0)) ab : ((and P) Q)))))
 (check-holds
@@ -512,15 +518,14 @@
 (check-holds
  (type-check ,Δ4
              (((∅ P : (Unv 0)) Q : (Unv 0)) ab : ((and P) Q))
-             (elim and
-                   (λ (A : Type) (λ (B : Type) (λ (x : ((and A) B))
-                                                 ((and B) A))))
-                   (P Q)
-                   ((λ (A : (Unv 0))
-                      (λ (B : (Unv 0))
-                        (λ (a : A)
-                          (λ (b : B) ((((conj B) A) b) a))))))
-                   ab)
+             ((((((elim and (Unv 0))
+                  (λ (A : Type) (λ (B : Type) (λ (x : ((and A) B))
+                                                ((and B) A)))))
+                 (λ (A : (Unv 0))
+                   (λ (B : (Unv 0))
+                     (λ (a : A)
+                       (λ (b : B) ((((conj B) A) b) a))))))
+                P) Q) ab)
              ((and Q) P)))
 (check-holds
  (type-check (,Δ4 (true : (Unv 0) ((tt : true)))) ∅
@@ -533,14 +538,14 @@
              t))
 (check-holds
  (type-check (,Δ4 (true : (Unv 0) ((tt : true)))) ∅
-             (elim and
+             ((((((elim and (Unv 0))
                   (λ (A : Type) (λ (B : Type) (λ (x : ((and A) B))
-                                                ((and B) A))))
-                 (true true)
-                 ((λ (A : (Unv 0))
+                                                ((and B) A)))))
+                 (λ (A : (Unv 0))
                    (λ (B : (Unv 0))
                      (λ (a : A)
                        (λ (b : B) ((((conj B) A) b) a))))))
+                true) true)
               ((((conj true) true) tt) tt))
              ((and true) true)))
 (define gamma (term (∅ temp863 : pre)))
@@ -563,18 +568,21 @@
 (check-holds
  (type-infer ,sigma (,gamma x : false) (λ (y : false) (Π (x : Type) x))
              (in-hole Ξ (Π (x : (in-hole Θ false)) U))))
-
+(check-true
+ (redex-match? tt-typingL
+               ((in-hole Θ_m ((elim x_D U) e_P)) e_D)
+               (term (((elim false (Unv 1)) (λ (y : false) (Π (x : Type) x)))
+                      x))))
 (check-holds
  (type-check ,sigma (,gamma x : false)
-             (elim false (λ (y : false) (Π (x : Type) x)) () () x)
+             (((elim false (Unv 0)) (λ (y : false) (Π (x : Type) x))) x)
              (Π (x : (Unv 0)) x)))
 
 ;; nat-equal? tests
 (define zero?
-  (term (λ (n : nat)
-          (elim nat (λ (x : nat) bool) ()
-              (true (λ (x : nat) (λ (x_ih : bool) false)))
-              n))))
+  (term ((((elim nat Type) (λ (x : nat) bool))
+          true)
+         (λ (x : nat) (λ (x_ih : bool) false)))))
 (check-holds
  (type-check ,Δ ∅ ,zero? (Π (x : nat) bool)))
 (check-equal?
@@ -584,12 +592,9 @@
  (term (reduce ,Δ (,zero? (s zero))))
  (term false))
 (define ih-equal?
-  (term (λ (ih : nat)
-          (elim nat (λ (x : nat) bool)
-              ()
-              (false
-               (λ (x : nat) (λ (y : bool) (x_ih x))))
-              ih))))
+  (term ((((elim nat Type) (λ (x : nat) bool))
+          false)
+         (λ (x : nat) (λ (y : bool) (x_ih x))))))
 (check-holds
  (type-check ,Δ (∅ x_ih : (Π (x : nat) bool))
              ,ih-equal?
@@ -601,13 +606,10 @@
 (check-holds
  (type-infer ,Δ ∅ (λ (x : nat) (Π (x : nat) bool)) (Π (x : nat) (Unv 0))))
 (define nat-equal?
-  (term (λ (n : nat)
-          (elim nat (λ (x : nat) (Π (x : nat) bool))
-              ()
-              (,zero?
-              (λ (x : nat) (λ (x_ih : (Π (x : nat) bool))
-                             ,ih-equal?)))
-              n))))
+  (term ((((elim nat Type) (λ (x : nat) (Π (x : nat) bool)))
+          ,zero?)
+         (λ (x : nat) (λ (x_ih : (Π (x : nat) bool))
+                        ,ih-equal?)))))
 (check-holds
  (type-check ,Δ (∅ nat-equal? : (Π (x-D«4158» : nat) ((λ (x«4159» : nat) (Π (x«4160» : nat) bool)) x-D«4158»)))
              ((nat-equal? zero) zero)
@@ -629,12 +631,19 @@
 (check-true (Δ? Δ=))
 
 (define refl-elim
-  (term (elim == (λ (A1 : (Unv 0)) (λ (x1 : A1) (λ (y1 : A1) (λ (p2 : (((== A1) x1) y1)) nat))))
-                  (bool true true)
-                  ((λ (A1 : (Unv 0)) (λ (x1 : A1) zero)))
-                  ((refl bool) true))))
+  (term (((((((elim == (Unv 0)) (λ (A1 : (Unv 0)) (λ (x1 : A1) (λ (y1 : A1) (λ (p2 : (((==
+                                                                                        A1)
+                                                                                       x1)
+                                                                                      y1))
+                                                                              nat)))))
+             (λ (A1 : (Unv 0)) (λ (x1 : A1) zero))) bool) true) true) ((refl bool) true))))
 (check-holds
  (type-check ,Δ= ∅ ,refl-elim nat))
+(check-true
+ (redex-match?
+  tt-redL
+  (Δ (in-hole E (in-hole Θ ((elim x_D U) e_P))))
+  (term (,Δ= ,refl-elim))))
 (check-true
  (redex-match?
   tt-redL

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

@@ -32,11 +32,11 @@
  (:: (lambda (A : Type) (n : Nat) (none A)) (forall (A : Type) (-> Nat (Maybe A)))))
 (check-equal?
  (void)
- (:: (elim List (lambda (A : Type) (ls : (List A)) Nat)
-           (Bool)
-          ((lambda (A : Type) z)
-           (lambda (A : Type) (a : A) (ls : (List A)) (ih : Nat)
-                   z))
+ (:: (elim List Type (lambda (A : Type) (ls : (List A)) Nat)
+          (lambda (A : Type) z)
+          (lambda (A : Type) (a : A) (ls : (List A)) (ih : Nat)
+                   z)
+          Bool
           (nil Bool))
     Nat))
 

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

@@ -11,11 +11,11 @@
 (:: pf:proj1 thm:proj1)
 (:: pf:proj2 thm:proj2)
 (check-equal?
- (elim == (λ (A : Type) (x : A) (y : A) (p : (== A x y)) Nat)
-       (Bool
-        true
-        true)
-       ((λ (A : Type) (x : A) z))
+ (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)
 

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

@@ -11,7 +11,9 @@
            (equal? : (forall (a : A) (b : A) Bool)))
 (impl (Eqv Bool)
       (define (equal? (a : Bool) (b : Bool))
-        (if a b (not b))))
+        (if a
+            (if b true false)
+            (if b false true))))
 (impl (Eqv Nat)
       (define equal? nat-equal?))
 (check-equal?

cur-test/info.rkt

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