From 543a7f93e6143d0658123d1caa35c2edec4de101 Mon Sep 17 00:00:00 2001
From: "William J. Bowman" <wjb@williamjbowman.com>
Date: Fri, 25 Mar 2016 17:00:25 -0400
Subject: [PATCH] [Perf. Bug] Split subtyping/reduce in conversion
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8
Content-Transfer-Encoding: 8bit

Previous, conversion was doing both reduction and subtyping.
Now, conversion first reduces, then appeal to the subtyping judgment.
The subtyping judgment may recur on conversion for certain subtyping
rules.
This fixes the hack in reduction that reduced Π types.

Unfortunately, after a little bisecting, this seems to introduce a major
performance bug, doubling running time.
---
 cur-lib/cur/curnel/redex-core.rkt | 32 ++++++++++++++++++-------------
 1 file changed, 19 insertions(+), 13 deletions(-)

diff --git a/cur-lib/cur/curnel/redex-core.rkt b/cur-lib/cur/curnel/redex-core.rkt
index 0e05255..10f31f1 100644
--- a/cur-lib/cur/curnel/redex-core.rkt
+++ b/cur-lib/cur/curnel/redex-core.rkt
@@ -312,10 +312,7 @@
   ;; call-by-value
   (E  ::= hole (E e) (v E)
       (elim D e (e ...) (v ... E e ...) e)
-      (elim D e (e ...) (v ...) E)
-      ;; reduce under Π (helps with typing checking)
-      ;; TODO: Should be done in conversion judgment
-      (Π (x : v) E) (Π (x : E) e)))
+      (elim D e (e ...) (v ...) E)))
 
 (define-metafunction tt-ctxtL
   is-inductive-argument : Δ_0 D_0 t -> #t or #f
@@ -392,20 +389,29 @@
   (Γ   ::= ∅ (Γ x : t)))
 
 (define-judgment-form tt-typingL
-  #:mode (convert I I I I)
-  #:contract (convert Δ Γ t t)
+  #:mode (sub I I I I)
+  #:contract (sub Δ Γ t t)
+
+  [-------------
+   (sub Δ Γ t t)]
 
   [(side-condition ,(<= (term i_0) (term i_1)))
    ----------------- "≼-Unv"
-   (convert Δ Γ (Unv i_0) (Unv i_1))]
+   (sub Δ Γ (Unv i_0) (Unv i_1))]
 
-  [(where (t t) ((reduce Δ t_0) (reduce Δ t_1)))
-   ----------------- "≼-αβ"
-   (convert Δ Γ t_0 t_1)]
-
-  [(convert Δ (Γ x : t_0) t_1 t_2)
+  [(convert Δ Γ t_0 t_1)
+   (convert Δ (Γ x_0 : t_0) e_0 (subst e_1 x_1 x_0))
    ----------------- "≼-Π"
-   (convert Δ Γ (Π (x : t_0) t_1) (Π (x : t_0) t_2))])
+   (sub Δ Γ (Π (x_0 : t_0) e_0) (Π (x_1 : t_1) e_1))])
+
+(define-judgment-form tt-typingL
+  #:mode (convert I I I I)
+  #:contract (convert Δ Γ t t)
+
+  [(where (t_2 t_3) ((reduce Δ t_0) (reduce Δ t_1)))
+   (sub Δ Γ t_2 t_3)
+   ----------------- "≼-αβ"
+   (convert Δ Γ t_0 t_1)])
 
 (define-metafunction tt-typingL
   Γ-in-dom : Γ x -> #t or #f