diff options
author | Péter Diviánszky <divipp@gmail.com> | 2016-05-14 02:20:30 +0200 |
---|---|---|
committer | Péter Diviánszky <divipp@gmail.com> | 2016-05-14 02:20:30 +0200 |
commit | c1079ecb25633a9c47d61bed034b50551cadd326 (patch) | |
tree | 04397a17b6366dabaeb8d477b0ce340358bd6c62 | |
parent | ed2b64667428a737ef67c1632d408633d2717509 (diff) |
refactoring
-rw-r--r-- | src/LambdaCube/Compiler/Core.hs | 22 | ||||
-rw-r--r-- | 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 | |||
328 | where | 328 | where |
329 | f i (Neut n) = substNeut n | 329 | f i (Neut n) = substNeut n |
330 | where | 330 | where |
331 | substNeut e | dbGE i e = Neut e | ||
332 | substNeut e = case e of | 331 | substNeut e = case e of |
333 | Var_ k -> case compare k i of GT -> Var $ k - 1; LT -> Var k; EQ -> up (i - i0) x | 332 | Var_ k -> case compare k i of GT -> Var $ k - 1; LT -> Var k; EQ -> up (i - i0) x |
334 | CaseFun__ fs s as n -> evalCaseFun (adjustDB i fs) s (f i <$> as) (substNeut n) | 333 | CaseFun__ fs s as n -> if dbGE_ i fs then Neut e else evalCaseFun (adjustDB i fs) s (f i <$> as) (substNeut n) |
335 | TyCaseFun__ fs s as n -> evalTyCaseFun_ (adjustDB i fs) s (f i <$> as) (substNeut n) | 334 | TyCaseFun__ fs s as n -> if dbGE_ i fs then Neut e else evalTyCaseFun_ (adjustDB i fs) s (f i <$> as) (substNeut n) |
336 | App__ fs a b -> app__ (adjustDB i fs) (substNeut a) (f i b) | 335 | App__ fs a b -> if dbGE_ i fs then Neut e else app__ (adjustDB i fs) (substNeut a) (f i b) |
337 | Fun_ md fn xs v -> mkFun_ (adjustDB i md) fn (f i <$> xs) $ f i v | 336 | Fun_ md fn xs v -> if dbGE_ i md then Neut e else mkFun_ (adjustDB i md) fn (f i <$> xs) $ f i v |
338 | f i e | dbGE i e = e | ||
339 | f i e = case e of | 337 | f i e = case e of |
340 | Lam_ md b -> Lam_ (adjustDB i md) (f (i+1) b) | 338 | Lam_ md b -> if dbGE_ i md then e else Lam_ (adjustDB i md) (f (i+1) b) |
341 | Con_ md s n as -> Con_ (adjustDB i md) s n $ f i <$> as | 339 | Con_ md s n as -> if dbGE_ i md then e else Con_ (adjustDB i md) s n $ f i <$> as |
342 | Pi_ md h a b -> Pi_ (adjustDB i md) h (f i a) (f (i+1) b) | 340 | Pi_ md h a b -> if dbGE_ i md then e else Pi_ (adjustDB i md) h (f i a) (f (i+1) b) |
343 | TyCon_ md s as -> TyCon_ (adjustDB i md) s $ f i <$> as | 341 | TyCon_ md s as -> if dbGE_ i md then e else TyCon_ (adjustDB i md) s $ f i <$> as |
344 | Let_ md a b -> Let_ (adjustDB i md) (subst_ i dx x a) (f (i+1) b) | 342 | Let_ md a b -> if dbGE_ i md then e else Let_ (adjustDB i md) (subst_ i dx x a) (f (i+1) b) |
345 | RHS a -> RHS $ hnf $ f i a | 343 | RHS a -> if dbGE i a then e else RHS $ hnf $ f i a |
346 | x -> x | 344 | x -> x |
347 | 345 | ||
348 | adjustDB i md = if usedVar i md then delVar i md <> shiftFreeVars (i-i0) dx else delVar i md | 346 | 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 | |||
105 | 105 | ||
106 | 106 | ||
107 | -- TODO: rename | 107 | -- TODO: rename |
108 | dbGE i (getFreeVars -> FreeVars x) = (1 `shiftL` i) > x | 108 | dbGE i x = dbGE_ i $ getFreeVars x |
109 | |||
110 | dbGE_ i (FreeVars x) = (1 `shiftL` i) > x | ||
109 | 111 | ||
110 | -------------------------------------------------------------------------------- type class for getting free variables | 112 | -------------------------------------------------------------------------------- type class for getting free variables |
111 | 113 | ||