From 024f4e188e41be66004d655fbc84945a156a0778 Mon Sep 17 00:00:00 2001
From: "William J. Bowman" <wjb@williamjbowman.com>
Date: Sat, 26 Sep 2015 00:57:36 -0400
Subject: [PATCH] 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 | 40 +++++++++++++++++++++++++++++++---------
 stdlib/prop.rkt       | 11 +++++++++++
 2 files changed, 42 insertions(+), 9 deletions(-)

diff --git a/curnel/redex-core.rkt b/curnel/redex-core.rkt
index c618183..1d39e81 100644
--- a/curnel/redex-core.rkt
+++ b/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
@@ -331,10 +331,7 @@
          ;; Check that Θ_p actually matches the parameters of x_D, to ensure it doesn't capture other
          ;; arguments.
          (judgment-holds (_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 (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
@@ -1105,7 +1102,32 @@
     (term false))
 
   ;; == tests
-  (define Σ= (term (,Σ (== : (Π (A : Type) (Π (a : A) (Π (b : A) Type)))
-                             ((refl : (Π (A : Type) (a : A) (== A a a))))))))
+  (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)))
diff --git a/stdlib/prop.rkt b/stdlib/prop.rkt
index 5422c53..143c4a9 100644
--- a/stdlib/prop.rkt
+++ b/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))