Documented new elim form

Previous eliminator for inductive types was too complex. It performs
automagic currying, making it difficult to type check and reduce.

New version must be fully applied, and magic is left to the surface language.

This version is now working and all core tests are passing, but
documentation, etc needs to be changed. Also, there is dead code that
should be removed.

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

@@ -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,12 +200,33 @@
   [(Ξ-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]
@@ -209,6 +259,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 +285,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
@@ -379,6 +453,7 @@
          (where natural (Δ-constructor-index Δ D c))
          (where v_mi ,(list-ref (term (v_m ...)) (term natural)))
          ;; Generate the inductive recursion
+         #;(Δ-inductive-elim Δ D U v_P Θv_p Θv_m Θv_i)
          (where Θ_ih (Δ-inductive-elim Δ D (elim D e_motive (e_i ...) (v_m ...) hole) Θv_c))
          (where Θ_mi (in-hole Θ_ih Θv_c))
          -->elim)))

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,6 +115,12 @@
  (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-true (x? (term false)))
 (check-true (Ξ? (term hole)))
 (check-true (t? (term (λ (y : false) (Π (x : Type) x)))))