Fixed reduction of (elim ==)

Fixed eliminator reduction, at least for the == type. Code currently
does the minimum required to make #23 work, but may have introduced bugs
in the process.

curnel/redex-core.rkt

@@ -313,7 +313,7 @@
          (Σ (in-hole E (in-hole Θ_r (in-hole Θ_i e_mi))))
          #|
           | The elim form must appear applied like so:
-          | (elim x_D U e_P m_0 ... m_i m_j ... m_n p ... (c_i p ... a ...))
+          | (elim x_D U e_P m_0 ... m_i m_j ... m_n p ... (c_i a ...))
           |
           | Where:
           |   x_D       is the inductive being eliminated
@@ -330,11 +330,8 @@
                 Θ)
          ;; Check that Θ_p actually matches the parameters of x_D, to ensure it doesn't capture other
          ;; arguments.
-         (where Ξ (parameters-of Σ x_D))
-         (judgment-holds (telescope-types Σ ∅ Θ_p Ξ))
-         ;; Ensure the constructor x_ci is applied to Θ_p first, then some arguments Θ_a
-         (where (in-hole Θ_a Θ_p)
-                Θ_i)
+         (judgment-holds (_parameters-of Σ x_D Ξ))
+         (judgment-holds (type-infer Σ ∅ (in-hole (Θ_p (in-hole Θ_i x_ci)) e_P) t))
          ;; Ensure x_ci is actually a constructor for x_D
          (where ((x_c* : t_c*) ...)
                 (constructors-for Σ x_D))
@@ -346,7 +343,7 @@
          ;; Find the method for constructor x_ci, relying on the order of the arguments.
          (where e_mi (method-lookup Σ x_D x_ci Θ_m))
          ;; Generate the inductive recursion
-         (where Θ_r (elim-recur x_D U e_P Θ_m Θ_m Θ_i (x_c* ...)))
+         (where Θ_r (elim-recur x_D U e_P (in-hole Θ_p Θ_m) Θ_m Θ_i (x_c* ...)))
          -->elim)))
 
 (define-metafunction cic-redL
@@ -564,33 +561,33 @@
 ;; defined type x_D, whose parameters/indices are Ξ_pi and whose
 ;; constructors are ((x_ci : t_ci) ...), with motive t_P.
 (define-metafunction cic-redL
-  methods-for : x Ξ t ((x : t) ...) -> Ξ
-  [(methods-for x_D Ξ_pi t_P ()) hole]
-  [(methods-for x_D Ξ_pi t_P ((x_ci : (in-hole Ξ_pi (in-hole Φ (in-hole Θ x_D))))
+  methods-for : x t ((x : t) ...) -> Ξ
+  [(methods-for x_D t_P ()) hole]
+  [(methods-for x_D t_P ((x_ci : (in-hole Φ (in-hole Θ x_D)))
                                     (x_c : t) ...))
-   (Π (x_mi : (in-hole Ξ_pi (in-hole Φ (in-hole Φ_h
-                                                ;; NB: Manually reducing types because no conversion
-                                                ;; NB: rule
-                                                ;; TODO: Thread through Σ for reduce
-                                                ;; TODO: Might be able to remove this now that I have
-                                                ;; TODO: equivalence in type-check
-                                                (reduce ∅ ((in-hole Θ t_P) (apply-telescopes x_ci (Ξ_pi Φ))))))))
-      (methods-for x_D Ξ_pi t_P ((x_c : t) ...)))
+   (Π (x_mi : (in-hole Φ (in-hole Φ_h
+                                  ;; NB: Manually reducing types because no conversion
+                                  ;; NB: rule
+                                  ;; TODO: Thread through Σ for reduce
+                                  ;; TODO: Might be able to remove this now that I have
+                                  ;; TODO: equivalence in type-check
+                                  (reduce ∅ ((in-hole Θ t_P) (apply-telescope x_ci Φ))))))
+      (methods-for x_D t_P ((x_c : t) ...)))
    (where Φ_h (hypotheses-for x_D t_P (inductive-args x_D Φ)))
    ;; NB: Lol hygiene
    (where x_mi ,(string->symbol (format "~a-~a" 'm (term x_ci))))])
 (module+ test
   (check-equal?
-    (term (methods-for nat hole P ((zero : nat) (s : (Π (x : nat) nat)))))
+    (term (methods-for nat P ((zero : nat) (s : (Π (x : nat) nat)))))
     (term (Π (m-zero : (P zero))
              (Π (m-s : (Π (x : nat) (Π (ih-x : (P x)) (P (s x)))))
                 hole))))
   (check-equal?
-    (term (methods-for nat hole (λ (x : nat) nat) ((zero : nat) (s : (Π (x : nat) nat)))))
+    (term (methods-for nat (λ (x : nat) nat) ((zero : nat) (s : (Π (x : nat) nat)))))
     (term (Π (m-zero : nat) (Π (m-s : (Π (x : nat) (Π (ih-x : nat) nat)))
                                    hole))))
   (check-equal?
-    (term (methods-for and (Π (A : Type) (Π (B : Type) hole))
+    (term (methods-for and
                        (λ (A : Type) (λ (B : Type) (λ (x : ((and A) B)) true)))
                        ((conj : (Π (A : Type) (Π (B : Type) (Π (a : A) (Π (b : B)
                                                                              ((and A) B)))))))))
@@ -601,7 +598,7 @@
   (check-true (t? (term (λ (y : false) (Π (x : Type) x)))))
   (check-true (redex-match? cicL ((x : t) ...) (term ())))
   (check-equal?
-    (term (methods-for false hole (λ (y : false) (Π (x : Type) x))
+    (term (methods-for false (λ (y : false) (Π (x : Type) x))
                        ()))
     (term hole)))
 
@@ -621,14 +618,39 @@
     (term (constructor-of ,Σ s))
     (term nat)))
 
-;; TODO: inlined at least in type-infer
 ;; TODO: Define generic traversals of Σ and Γ ?
+;; Figure out what the parameters of an inductive type are, based on the constructor.
+(define-judgment-form cic-typingL
+  #:mode (_parameters-of I I O)
+  #:contract (_parameters-of Σ x Ξ)
+
+  [(side-condition ,(map (curry equal? (term Ξ)) (term (Ξ_* ...))))
+   (side-condition ,(map (curry equal? (term x_D)) (term (x_D* ...))))
+   ;; Not enough conditions to be right, but enough to mostly work
+   -----------------
+   (_parameters-of (Σ (x_D : (in-hole Ξ t_D)
+                          ((x : (in-hole Ξ_* (in-hole Φ (in-hole Θ_* x_D*)))) ...)))
+                  x_D
+                  Ξ)]
+
+  [(_parameters-of Σ x_D Ξ)
+   (side-condition ,(not (equal? (term x_1) (term x_D))))
+   ---------------------
+   (_parameters-of (Σ (x_1 : t_1 ((x : t) ...))) x_D Ξ)]
+  )
+
+
 (define-metafunction cic-redL
   parameters-of : Σ x -> Ξ
-  [(parameters-of (Σ (x_D : (in-hole Ξ U) ((x : t) ...))) x_D)
-   Ξ]
-  [(parameters-of (Σ (x_1 : t_1 ((x : t) ...))) x_D)
-   (parameters-of Σ x_D)])
+  [(parameters-of Σ x_D)
+   ,(car (judgment-holds (_parameters-of Σ x_D Ξ) Ξ))])
+(module+ test
+  (check-equal?
+    (term (parameters-of ,Σ nat))
+    (term hole))
+  (check-equal?
+    (judgment-holds (_parameters-of ,Σ4 and Ξ) Ξ)
+    (term (Π (A : Type) (Π (B : Type) hole)))))
 
 ;; Returns the constructors for the inductively defined type x_D in
 ;; the signature Σ
@@ -669,7 +691,7 @@
                   (term ((hole zero) (λ (x : nat) x)))))
   (check-holds
     (telescope-types ,Σ ∅ (hole zero)
-                     (methods-for nat hole
+                     (methods-for nat
                                   (λ (x : nat) nat)
                                   ((zero : nat)))))
   (check-holds
@@ -679,20 +701,20 @@
     (telescope-types ,Σ ∅
                      ((hole zero)
                       (λ (x : nat) (λ (ih-x : nat) x)))
-                     (methods-for nat hole
+                     (methods-for nat
                                   (λ (x : nat) nat)
                                   (constructors-for ,Σ nat))))
   (check-holds
     (telescope-types (,Σ4 (true : (Unv 0) ((tt : true))))
                      ∅ (hole (λ (A : (Unv 0)) (λ (B : (Unv 0))
                                                     (λ (a : A) (λ (b : B) tt)))))
-                     (methods-for and (Π (A : Type) (Π (B : Type) hole))
+                     (methods-for and
                                   (λ (A : Type) (λ (B : Type) (λ (x : ((and A) B)) true)))
                                   (constructors-for ,Σ4 and))))
   (check-holds
     (telescope-types ,sigma (∅ x : false)
                      hole
-                     (methods-for false hole (λ (y : false) (Π (x : Type) x))
+                     (methods-for false (λ (y : false) (Π (x : Type) x))
                                   ()))))
 
 ;; TODO: Bi-directional and inference?
@@ -733,7 +755,8 @@
    ----------------- "DTR-Abstraction"
    (type-infer Σ Γ (λ (x : t_0) e) (Π (x : t_0) t_1))]
 
-  [(type-infer Σ Γ x_D (in-hole Ξ U_D))
+  [(type-infer Σ Γ x_D (in-hole Ξ t_D))
+   (_parameters-of Σ x_D Ξ)
    ;; A fresh name to bind the discriminant
    (where x (fresh-x Σ Γ x_D Ξ))
    ;; The telescope (∀ a -> ... -> (D a ...) hole), i.e.,
@@ -743,7 +766,7 @@
    ;; A fresh name for the motive
    (where x_P (fresh-x Σ Γ x_D Ξ Ξ_P*D x))
    ;; The types of the methods for this inductive.
-   (where Ξ_m (methods-for x_D Ξ x_P (constructors-for Σ x_D)))
+   (where Ξ_m (methods-for x_D x_P (constructors-for Σ x_D)))
    ----------------- "DTR-Elim_D"
    (type-infer Σ Γ ((elim x_D) U)
      ;; The type of ((elim x_D) U) is something like:
@@ -807,10 +830,10 @@
   (check-holds (type-infer ,Σtruth ∅ (λ (x : truth) (Unv 1))
                            (in-hole Ξ (Π (x : (in-hole Θ truth)) U))))
   (check-equal?
-    (term (methods-for truth hole (λ (x : truth) (Unv 1)) ((T : truth))))
+    (term (methods-for truth (λ (x : truth) (Unv 1)) ((T : truth))))
     (term (Π (m-T : (Unv 1)) hole)))
   (check-holds (telescope-types ,Σtruth ∅ (hole (Unv 0))
-                                (methods-for truth hole
+                                (methods-for truth
                                              (λ (x : truth) (Unv 1))
                                              ((T : truth)))))
   (check-holds (type-infer ,Σtruth ∅ ((elim truth) Type) t))
@@ -1076,4 +1099,35 @@
     (term false))
   (check-equal?
     (term (reduce ,Σ ((,nat-equal? (s zero)) zero)))
-    (term false)))
+    (term false))
+
+  ;; == tests
+  (define Σ= (term (,Σ (== : (Π (A : (Unv 0)) (Π (a : A) (Π (b : A) (Unv 0))))
+                             ((refl : (Π (A : (Unv 0)) (Π (a : A) (((== A) a) a)))))))))
+  (check-true (Σ? Σ=))
+
+  (define refl-elim
+    (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?
+      cic-redL
+      (Σ (in-hole E (in-hole Θ (((elim x_D) U) e_P))))
+      (term (,Σ= ,refl-elim))))
+  (check-true
+    (redex-match?
+      cic-redL
+      (in-hole (Θ_p (in-hole Θ_i x_ci)) Θ_m)
+      (term (((((hole
+              (λ (A1 : (Unv 0)) (λ (x1 : A1) zero))) bool) true) true) ((refl bool) true)))))
+  (check-holds
+    (_parameters-of ,Σ= == (Π (A : Type) (Π (x : A) hole))))
+  (check-equal?
+    (term (reduce ,Σ= ,refl-elim))
+    (term zero)))

stdlib/prop.rkt

@@ -84,3 +84,14 @@
 
 (data == : (forall* (A : Type) (x : A) (-> A Type))
   (refl : (forall* (A : Type) (x : A) (== A x x))))
+
+(module+ test
+  (require rackunit "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))