From c1079ecb25633a9c47d61bed034b50551cadd326 Mon Sep 17 00:00:00 2001
From: Péter Diviánszky <divipp@gmail.com>
Date: Sat, 14 May 2016 02:20:30 +0200
Subject: refactoring

---
 src/LambdaCube/Compiler/Core.hs     | 22 ++++++++++------------
 src/LambdaCube/Compiler/DeBruijn.hs |  4 +++-
 2 files changed, 13 insertions(+), 13 deletions(-)

diff --git a/src/LambdaCube/Compiler/Core.hs b/src/LambdaCube/Compiler/Core.hs
index e86e205a..5c13e54a 100644
--- a/src/LambdaCube/Compiler/Core.hs
+++ b/src/LambdaCube/Compiler/Core.hs
@@ -328,21 +328,19 @@ instance Subst Exp Exp where
       where
         f i (Neut n) = substNeut n
           where
-            substNeut e | dbGE i e = Neut e
             substNeut e = case e of
                 Var_ k              -> case compare k i of GT -> Var $ k - 1; LT -> Var k; EQ -> up (i - i0) x
-                CaseFun__ fs s as n -> evalCaseFun (adjustDB i fs) s (f i <$> as) (substNeut n)
-                TyCaseFun__ fs s as n -> evalTyCaseFun_ (adjustDB i fs) s (f i <$> as) (substNeut n)
-                App__ fs a b        -> app__ (adjustDB i fs) (substNeut a) (f i b)
-                Fun_ md fn xs v     -> mkFun_ (adjustDB i md) fn (f i <$> xs) $ f i v
-        f i e | dbGE i e = e
+                CaseFun__ fs s as n -> if dbGE_ i fs then Neut e else evalCaseFun (adjustDB i fs) s (f i <$> as) (substNeut n)
+                TyCaseFun__ fs s as n -> if dbGE_ i fs then Neut e else evalTyCaseFun_ (adjustDB i fs) s (f i <$> as) (substNeut n)
+                App__ fs a b        -> if dbGE_ i fs then Neut e else app__ (adjustDB i fs) (substNeut a) (f i b)
+                Fun_ md fn xs v     -> if dbGE_ i md then Neut e else mkFun_ (adjustDB i md) fn (f i <$> xs) $ f i v
         f i e = case e of
-            Lam_ md b       -> Lam_ (adjustDB i md) (f (i+1) b)
-            Con_ md s n as  -> Con_ (adjustDB i md) s n $ f i <$> as
-            Pi_ md h a b    -> Pi_ (adjustDB i md) h (f i a) (f (i+1) b)
-            TyCon_ md s as  -> TyCon_ (adjustDB i md) s $ f i <$> as
-            Let_ md a b     -> Let_ (adjustDB i md) (subst_ i dx x a) (f (i+1) b)
-            RHS a           -> RHS $ hnf $ f i a
+            Lam_ md b       -> if dbGE_ i md then e else Lam_ (adjustDB i md) (f (i+1) b)
+            Con_ md s n as  -> if dbGE_ i md then e else Con_ (adjustDB i md) s n $ f i <$> as
+            Pi_ md h a b    -> if dbGE_ i md then e else Pi_ (adjustDB i md) h (f i a) (f (i+1) b)
+            TyCon_ md s as  -> if dbGE_ i md then e else TyCon_ (adjustDB i md) s $ f i <$> as
+            Let_ md a b     -> if dbGE_ i md then e else Let_ (adjustDB i md) (subst_ i dx x a) (f (i+1) b)
+            RHS a           -> if dbGE i a then e else RHS $ hnf $ f i a
             x               -> x
 
         adjustDB i md = if usedVar i md then delVar i md <> shiftFreeVars (i-i0) dx else delVar i md
diff --git a/src/LambdaCube/Compiler/DeBruijn.hs b/src/LambdaCube/Compiler/DeBruijn.hs
index f49654c4..a1af40db 100644
--- a/src/LambdaCube/Compiler/DeBruijn.hs
+++ b/src/LambdaCube/Compiler/DeBruijn.hs
@@ -105,7 +105,9 @@ rearrangeFreeVars g l (FreeVars i) = FreeVars $ case g of
 
 
 -- TODO: rename
-dbGE i (getFreeVars -> FreeVars x) = (1 `shiftL` i) > x
+dbGE i x = dbGE_ i $ getFreeVars x
+
+dbGE_ i (FreeVars x) = (1 `shiftL` i) > x
 
 -------------------------------------------------------------------------------- type class for getting free variables
 
-- 
cgit v1.2.3