From 8b58736101fbea42f2da68e56de70d239863acc2 Mon Sep 17 00:00:00 2001
From: "William J. Bowman" <wjb@williamjbowman.com>
Date: Fri, 25 Mar 2016 03:00:46 -0400
Subject: [PATCH] Split wf and validity checking
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8
Content-Transfer-Encoding: 8bit

Previously, wf was serving double-duty checking that Γ was well-formed
w.r.t. Δ, and then checking that Δ was valid (i.e. satisfied
positivity conditions and such).

Now these are different judgments.
---
 cur-lib/cur/curnel/redex-core.rkt | 37 +++++++++++++++++++------------
 1 file changed, 23 insertions(+), 14 deletions(-)

diff --git a/cur-lib/cur/curnel/redex-core.rkt b/cur-lib/cur/curnel/redex-core.rkt
index 9892ffe..a54338d 100644
--- a/cur-lib/cur/curnel/redex-core.rkt
+++ b/cur-lib/cur/curnel/redex-core.rkt
@@ -454,30 +454,39 @@
    ,(and (term (positive D (in-hole Ξ (Unv 0)))) (term (positive* D (t_rest ...))))
    (where (in-hole Ξ (in-hole Θ D)) t_c)])
 
-;; Holds when the signature Δ and typing context Γ are well-formed.
+;; Holds when the signature Δ is valid
 (define-judgment-form tt-typingL
-  #:mode (wf I I)
-  #:contract (wf Δ Γ)
+  #:mode (valid I)
+  #:contract (valid Δ)
 
-  [----------------- "WF-Empty"
-   (wf ∅ ∅)]
+  [-------- "Valid-Empty"
+   (valid ∅)]
 
-  [(type-infer Δ Γ t t_0)
-   (wf Δ Γ)
-   ----------------- "WF-Var"
-   (wf Δ (Γ x : t))]
-
-  [(wf Δ ∅)
+  [(valid Δ)
    (type-infer Δ ∅ t_D U_D)
    (type-infer Δ (∅ D : t_D) t_c U_c) ...
    ;; NB: Ugh this should be possible with pattern matching alone ....
    (side-condition ,(andmap (curry equal? (term D)) (term (D_0 ...))))
    (side-condition (positive* D (t_c ...)))
-   ----------------- "WF-Inductive"
-   (wf (Δ (D : t_D
+   ----------------- "Valid-Inductive"
+   (valid (Δ (D : t_D
                ;; Checks that a constructor for x actually produces an x, i.e., that
                ;; the constructor is well-formed.
-               ((c : (name t_c (in-hole Ξ (in-hole Θ D_0)))) ...))) ∅)])
+               ((c : (name t_c (in-hole Ξ (in-hole Θ D_0)))) ...))))])
+
+;; Holds when the signature Δ and typing context Γ are well-formed.
+(define-judgment-form tt-typingL
+  #:mode (wf I I)
+  #:contract (wf Δ Γ)
+
+  [(valid Δ)
+   ----------------- "WF-Empty"
+   (wf Δ ∅)]
+
+  [(type-infer Δ Γ t t_0)
+   (wf Δ Γ)
+   ----------------- "WF-Var"
+   (wf Δ (Γ x : t))])
 
 ;; TODO: Bi-directional and inference?
 ;; TODO: http://www.cs.ox.ac.uk/ralf.hinze/WG2.8/31/slides/stephanie.pdf