From 3e5af7233465c00cd94208c74834cdcbed251da3 Mon Sep 17 00:00:00 2001
From: "William J. Bowman" <wjb@williamjbowman.com>
Date: Thu, 24 Sep 2015 14:41:01 -0400
Subject: [PATCH 1/3] Started converting to Redex + binding

---
 curnel/redex-core.rkt | 73 +++++++++----------------------------------
 1 file changed, 15 insertions(+), 58 deletions(-)

diff --git a/curnel/redex-core.rkt b/curnel/redex-core.rkt
index b19a5b8..6b04cdc 100644
--- a/curnel/redex-core.rkt
+++ b/curnel/redex-core.rkt
@@ -36,7 +36,10 @@
   (U ::= (Unv i))
   (x ::= variable-not-otherwise-mentioned)
   (v ::= (Π (x : t) t) (λ (x : t) t) elim x U)
-  (t e ::= v (t t)))
+  (t e ::= v (t t))
+  #:binding-forms
+  (λ (x : t) e #:refers-to x)
+  (Π (x : t) t #:refers-to x))
 
 (define x? (redex-match? cicL x))
 (define t? (redex-match? cicL t))
@@ -93,67 +96,21 @@
    ----------------
    (unv-kind (Unv i_1) (Unv i_2) (Unv i_3))])
 
-(define-judgment-form cicL
-  #:mode (α-equivalent I I)
-  #:contract (α-equivalent t t)
-
-  [----------------- "α-x"
-                     (α-equivalent x x)]
-
-  [----------------- "α-U"
-                     (α-equivalent U U)]
-
-  [(α-equivalent t_1 (subst t_3 x_1 x_0))
-   (α-equivalent t_0 t_2)
-   ----------------- "α-binder"
-   (α-equivalent (any (x_0 : t_0) t_1)
-                 (any (x_1 : t_2) t_3))]
-
-  [(α-equivalent e_0 e_2)
-   (α-equivalent e_1 e_3)
-   ----------------- "α-app"
-   (α-equivalent (e_0 e_1) (e_2 e_3))])
-(module+ test
-  (check-holds (α-equivalent x x))
-  (check-not-holds (α-equivalent x y))
-  (check-holds (α-equivalent (λ (x : A) x) (λ (y : A) y))))
-
-;; NB: Substitution is hard
-;; NB: Copy and pasted from Redex examples
 (define-metafunction cicL
-  subst-vars : (x any) ... any -> any
-  [(subst-vars (x_1 any_1) x_1) any_1]
-  [(subst-vars (x_1 any_1) (any_2 ...))
-   ((subst-vars (x_1 any_1) any_2) ...)]
-  [(subst-vars (x_1 any_1) any_2) any_2]
-  [(subst-vars (x_1 any_1) (x_2 any_2) ... any_3)
-   (subst-vars (x_1 any_1) (subst-vars (x_2 any_2) ... any_3))]
-  [(subst-vars any) any])
-
+  α-equivalent? : t t -> #t or #f
+  [(α-equivalent? t_0 t_1)
+   ,(alpha-equivalent? cicL (term t_0) (term t_1)) ])
 (define-metafunction cicL
   subst : t x t -> t
-  [(subst U x t) U]
-  [(subst x x t) t]
-  [(subst x_0 x t) x_0]
-  [(subst (any (x : t_0) t_1) x t)
-   (any (x : (subst t_0 x t)) t_1)]
-  [(subst (any (x_0 : t_0) t_1) x t)
-   (any (x_new : (subst (subst-vars (x_0 x_new) t_0) x t))
-        (subst (subst-vars (x_0 x_new) t_1) x t))
-   (where x_new
-          ,(variable-not-in
-             (term (x_0 t_0 x t t_1))
-             (term x_0)))]
-  [(subst (e_0 e_1) x t) ((subst e_0 x t) (subst e_1 x t))]
-  [(subst elim x t) elim])
+  [(subst t_0 x t_1)
+   ,(substitute cicL (term t_0) (term x) (term t_1))])
 (module+ test
   (check-true (t? (term (Π (a : A) (Π (b : B) ((and A) B))))))
-  (check-holds
-    (α-equivalent
-      (Π (a : S) (Π (b : B) ((and S) B)))
-      (subst (Π (a : A) (Π (b : B) ((and A) B))) A S))))
-;; NB:
-;; TODO: Why do I not have tests for substitutions?!?!?!?!?!?!?!!?!?!?!?!?!?!!??!?!
+  (check-true
+    (term
+      (α-equivalent?
+        (Π (a : S) (Π (b : B) ((and S) B)))
+        (subst (Π (a : A) (Π (b : B) ((and A) B))) A S)))))
 
 (define-metafunction cicL
   subst-all : t (x ...) (e ...) -> t
@@ -343,7 +300,7 @@
 
   [(where t_2 (reduce Σ t_0))
    (where t_3 (reduce Σ t_1))
-   (α-equivalent t_2 t_3)
+   (side-condition (α-equivalent? t_2 t_3))
    ----------------- "≡-αβ"
    (equivalent Σ t_0 t_1)])
 

From 008f4451f73acbc2c1a0906556927f5dbd758769 Mon Sep 17 00:00:00 2001
From: "William J. Bowman" <wjb@williamjbowman.com>
Date: Thu, 24 Sep 2015 16:56:22 -0400
Subject: [PATCH 2/3] Tests seem to be passing.

---
 curnel/redex-core.rkt | 52 +++++++++++++++++++++++++------------------
 1 file changed, 30 insertions(+), 22 deletions(-)

diff --git a/curnel/redex-core.rkt b/curnel/redex-core.rkt
index 6b04cdc..98db81a 100644
--- a/curnel/redex-core.rkt
+++ b/curnel/redex-core.rkt
@@ -39,7 +39,7 @@
   (t e ::= v (t t))
   #:binding-forms
   (λ (x : t) e #:refers-to x)
-  (Π (x : t) t #:refers-to x))
+  (Π (x : t_0) t_1 #:refers-to x))
 
 (define x? (redex-match? cicL x))
 (define t? (redex-match? cicL t))
@@ -303,6 +303,14 @@
    (side-condition (α-equivalent? t_2 t_3))
    ----------------- "≡-αβ"
    (equivalent Σ t_0 t_1)])
+(module+ test
+  (define-syntax-rule (check-equivalent e1 e2)
+    (check-holds (equivalent ∅ e1 e2)))
+  (check-equivalent
+    (λ (x : Type) x) (λ (y : Type) y))
+  (check-equivalent
+    (Π (x : Type) x) (Π (y : Type) y))
+  )
 
 (define-extended-language cic-typingL cic-redL
   ;; NB: There may be a bijection between Γ and Ξ. That's
@@ -657,8 +665,8 @@
   (check-holds (unv-kind (Unv 0) (Unv 0) (Unv 0)))
   (check-holds (type-infer ∅ (∅ x_0 : (Unv 0)) (Π (x_2 : x_0) (Unv 0)) t))
 
-  (check-holds (type-infer ∅ ∅ (λ (x : (Unv 0)) x) (Π (x : (Unv 0)) (Unv 0))))
-  (check-holds (type-infer ∅ ∅ (λ (y : (Unv 0)) (λ (x : y) x))
+  (check-holds (type-check ∅ ∅ (λ (x : (Unv 0)) x) (Π (x : (Unv 0)) (Unv 0))))
+  (check-holds (type-check ∅ ∅ (λ (y : (Unv 0)) (λ (x : y) x))
                            (Π (y : (Unv 0)) (Π (x : y) y))))
 
   (check-equal? (list (term (Unv 1)))
@@ -734,25 +742,25 @@
                 ((((elim nat) zero) nat) (s zero))
                 nat))
   (define lam (term (λ (nat : (Unv 0)) nat)))
-  (check-equal?
-    (list (term (Π (nat : (Unv 0)) (Unv 0))))
-    (judgment-holds (type-infer ,Σ0 ∅ ,lam t) t))
-  (check-equal?
-    (list (term (Π (nat : (Unv 0)) (Unv 0))))
-    (judgment-holds (type-infer ,Σ ∅ ,lam t) t))
-  (check-equal?
-    (list (term (Π (x : (Π (y : (Unv 0)) y)) nat)))
-    (judgment-holds (type-infer (∅ (nat : (Unv 0) ())) ∅ (λ (x : (Π (y : (Unv 0)) y)) (x nat))
-                                t) t))
-  (check-equal?
-    (list (term (Π (y : (Unv 0)) (Unv 0))))
-    (judgment-holds (type-infer (∅ (nat : (Unv 0) ())) ∅ (λ (y : (Unv 0)) y) t) t))
-  (check-equal?
-    (list (term (Unv 0)))
-    (judgment-holds (type-infer (∅ (nat : (Unv 0) ())) ∅
-                                ((λ (x : (Π (y : (Unv 0)) (Unv 0))) (x nat))
-                                 (λ (y : (Unv 0)) y))
-                                t) t))
+  (check-equivalent
+    (Π (nat : (Unv 0)) (Unv 0))
+    ,(car (judgment-holds (type-infer ,Σ0 ∅ ,lam t) t)))
+  (check-equivalent
+    (Π (nat : (Unv 0)) (Unv 0))
+    ,(car (judgment-holds (type-infer ,Σ ∅ ,lam t) t)))
+  (check-equivalent
+    (Π (x : (Π (y : (Unv 0)) y)) nat)
+    ,(car (judgment-holds (type-infer (∅ (nat : (Unv 0) ())) ∅ (λ (x : (Π (y : (Unv 0)) y)) (x nat))
+                                  t) t)))
+  (check-equivalent
+    (Π (y : (Unv 0)) (Unv 0))
+    ,(car (judgment-holds (type-infer (∅ (nat : (Unv 0) ())) ∅ (λ (y : (Unv 0)) y) t) t)))
+  (check-equivalent
+    (Unv 0)
+    ,(car (judgment-holds (type-infer (∅ (nat : (Unv 0) ())) ∅
+                                 ((λ (x : (Π (y : (Unv 0)) (Unv 0))) (x nat))
+                                  (λ (y : (Unv 0)) y))
+                                 t) t)))
   (check-equal?
     (list (term (Unv 0)) (term (Unv 1)))
     (judgment-holds

From 6e27c1fc395dfccd4ae4f54434a254cac6a2b8ee Mon Sep 17 00:00:00 2001
From: "William J. Bowman" <wjb@williamjbowman.com>
Date: Thu, 24 Sep 2015 16:58:36 -0400
Subject: [PATCH 3/3] Tweaks dependencies

---
 info.rkt | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/info.rkt b/info.rkt
index 3a32978..1e018fd 100644
--- a/info.rkt
+++ b/info.rkt
@@ -1,6 +1,6 @@
 #lang info
 (define collection "cur")
-(define deps '("base" "rackunit-lib" ("redex-lib" #:version "1.6")))
+(define deps '("base" "rackunit-lib" ("redex-lib" #:version "1.8" #;redex-1-paul-public)))
 (define build-deps '("scribble-lib" "racket-doc" "sandbox-lib"))
 (define scribblings '(("scribblings/cur.scrbl" (multi-page))))
 (define pkg-desc "Dependent types with parenthesis and meta-programming.")