From c07e93a8704e15b0056c307e7e08a590e2181704 Mon Sep 17 00:00:00 2001
From: "William J. Bowman" <wjb@williamjbowman.com>
Date: Tue, 6 Oct 2015 02:32:09 -0400
Subject: [PATCH] Nuts to this sanity check

---
 curnel/redex-core.rkt | 52 +++++++++++++++++++++++++++++++------------
 stdlib/sugar.rkt      | 11 +++++----
 2 files changed, 45 insertions(+), 18 deletions(-)

diff --git a/curnel/redex-core.rkt b/curnel/redex-core.rkt
index 395f29f..5bb37b8 100644
--- a/curnel/redex-core.rkt
+++ b/curnel/redex-core.rkt
@@ -592,10 +592,6 @@
 ;;; inductively defined type x with a motive whose result is in universe U
 
 ;; Necessary to get the side-condition patterns to work.
-(define current-Σ (make-parameter (term ∅)))
-(define (elim-arity x)
-  (term (Σ-elim-arity ,(current-Σ) ,x)))
-
 (define-extended-language tt-redL tt-ctxtL
   (Θv  ::= hole (Θv v))
   (v   ::= x U (Π (x : t) t) (λ (x : t) t) (elim x U) (in-hole Θv x)
@@ -603,7 +599,7 @@
            (in-hole Θv (elim x U))
            #;(side-condition
              (not (equal? (term (Θ-length Θv_0))
-                          (elim-arity (term x_0))))))
+                          (Σ-elim-arity ?? (term x_0))))))
   ;; call-by-value, plus reduce under Π (helps with typing checking)
   (E   ::= hole (E e) (v E) (Π (x : v) E) (Π (x : E) e)))
 
@@ -616,6 +612,33 @@
   (check-true (v? (term (refl Nat))))
   (check-true (v? (term ((refl Nat) z)))))
 
+(define-metafunction tt-redL
+  elim-Θv-really : Σ Θv -> #t or #f
+  [(elim-Θv-really Σ hole) #t]
+  [(elim-Θv-really Σ (Θv (in-hole Θv_1 (elim x_D U))))
+   ,(and
+      (not (equal? (term (Θ-length Θv_1))
+                   (term (Σ-elim-arity Σ x_D))))
+      (term (elim-Θv-really Σ Θv_1))
+      (term (elim-Θv-really Σ Θv)))]
+  [(elim-Θv-really Σ (Θv v))
+   (elim-Θv-really Σ Θv)])
+
+(module+ test
+  (check-true
+    (term (elim-Θv-really ,Σ (hole (elim nat Type)))))
+  (check-true
+    (term (elim-Θv-really ,Σ (hole ((elim nat Type) (λ (x : nat) nat))))))
+  (check-true
+    (term (elim-Θv-really ,Σ (hole (((elim nat Type) (λ (x : nat) nat)) zero)))))
+  (check-true
+    (term (elim-Θv-really ,Σ (hole ((((elim nat Type) (λ (x : nat) nat)) zero)
+                                              (λ (x : nat) (λ (ih : nat) zero)))))))
+  (check-false
+    (term (elim-Θv-really ,Σ (hole (((((elim nat Type) (λ (x : nat) nat)) zero)
+                                               (λ (x : nat) (λ (ih : nat) zero)))
+                                                                  zero))))))
+
 (define tt-->
   (reduction-relation tt-redL
     (--> (Σ (in-hole E ((any (x : t_0) t_1) t_2)))
@@ -638,8 +661,10 @@
           | Unfortunately, Θ contexts turn all this inside out:
           | TODO: Write better abstractions for this notation
           |#
-          ;; Split Θv into its components: the paramters Θv_P for x_D, the methods Θv_m for x_D, and
-          ;; the discriminant: the constructor x_ci applied to its argument Θv_i
+         ;; Check that Θv only contains partially applied elims.
+         (side-condition (term (elim-Θv-really Σ Θ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 x_ci applied to its argument Θv_i
          (where (in-hole (Θv_p (in-hole Θv_i x_ci)) Θv_m) Θv)
          ;; Check that Θ_p actually matches the parameters of x_D, to ensure it doesn't capture other
          ;; arguments.
@@ -660,19 +685,18 @@
   step : Σ e -> e
   [(step Σ e)
    e_r
-   (where (_ e_r) ,(parameterize ([current-Σ (term Σ)]) (car (apply-reduction-relation tt--> (term (Σ e))))))])
+   (where (_ e_r) ,(car (apply-reduction-relation tt--> (term (Σ e)))))])
 
 (define-metafunction tt-redL
   reduce : Σ e -> e
   [(reduce Σ e)
    e_r
    (where (_ e_r)
-     ,(parameterize ([current-Σ (term Σ)])
-        (let ([r (apply-reduction-relation* tt--> (term (Σ e)) #:cache-all? #t)])
-         ;; Efficient check for (= (length r) 1)
-         (unless (null? (cdr r))
-           (error "Church-Rosser broken" r (term e)))
-         (car r))))])
+     ,(let ([r (apply-reduction-relation* tt--> (term (Σ e)) #:cache-all? #t)])
+        ;; Efficient check for (= (length r) 1)
+        #;(unless (null? (cdr r))
+          (error "Church-Rosser broken" r (term e)))
+        (car r)))])
 
 ;; TODO: Move equivalence up here, and use in these tests.
 (module+ test
diff --git a/stdlib/sugar.rkt b/stdlib/sugar.rkt
index ef76264..1d637e2 100644
--- a/stdlib/sugar.rkt
+++ b/stdlib/sugar.rkt
@@ -69,15 +69,18 @@
             (unless (type-check/syn? #'e2 #'t1)
               (raise-syntax-error
                 '#%app
-                (format "Operand does not have expected type; expected ~a but inferred ~a"
+                (format "Operand '~a' does not have expected type; expected '~a' but inferred '~a'"
+                        (cur->datum #'e2)
                         (cur->datum #'t1)
                         (cur->datum (type-infer/syn #'e2)))
-                f-type (quasisyntax/loc syn (e1 e2))))
+                (quasisyntax/loc syn (e1 e2))))
             #'(real-app e1 e2))]
          [_ (raise-syntax-error
               '#%app
-              (format "Operator does not have function type; inferred type was: ~a" (cur->datum f-type))
-              f-type (quasisyntax/loc syn (e1 e2)))]))]
+              (format "Operator '~a' does not have function type; inferred type was: '~a'"
+                      (cur->datum #'e1)
+                      (cur->datum f-type))
+              (quasisyntax/loc syn (e1 e2)))]))]
     [(_ e1 e2 e3 ...)
      #'(#%app (#%app e1 e2) e3 ...)]))