diff options
Diffstat (limited to 'src')
-rw-r--r-- | src/LambdaCube/Compiler/Infer.hs | 38 |
1 files changed, 19 insertions, 19 deletions
diff --git a/src/LambdaCube/Compiler/Infer.hs b/src/LambdaCube/Compiler/Infer.hs index 74ae6002..08e29630 100644 --- a/src/LambdaCube/Compiler/Infer.hs +++ b/src/LambdaCube/Compiler/Infer.hs | |||
@@ -266,16 +266,16 @@ pattern MatchName cs <- (getMatchName -> Just cs) | |||
266 | 266 | ||
267 | type ExpType = (Exp, Type) | 267 | type ExpType = (Exp, Type) |
268 | 268 | ||
269 | pattern Fun a b <- Neut _ (Fun_ a b) where Fun a b = Neut (foldMap maxDB0 b) (Fun_ a b) | 269 | pattern Fun a b <- Neut _ (Fun_ a b) where Fun a b = Neut (foldMap maxDB_ b) (Fun_ a b) |
270 | pattern CaseFun a b <- Neut _ (CaseFun_ a b) where CaseFun a b = Neut (foldMap maxDB0 b) (CaseFun_ a b) | 270 | pattern CaseFun a b <- Neut _ (CaseFun_ a b) where CaseFun a b = Neut (foldMap maxDB_ b) (CaseFun_ a b) |
271 | pattern TyCaseFun a b <- Neut _ (TyCaseFun_ a b) where TyCaseFun a b = Neut (foldMap maxDB0 b) (TyCaseFun_ a b) | 271 | pattern TyCaseFun a b <- Neut _ (TyCaseFun_ a b) where TyCaseFun a b = Neut (foldMap maxDB_ b) (TyCaseFun_ a b) |
272 | pattern App a b <- Neut _ (App_ a b) where App a b = Neut (maxDB0 a <> maxDB0 b) (App_ a b) | 272 | pattern App a b <- Neut _ (App_ a b) where App a b = Neut (maxDB_ a <> maxDB_ b) (App_ a b) |
273 | pattern Var a <- Neut _ (Var_ a) where Var a = Neut (varDB a) (Var_ a) | 273 | pattern Var a <- Neut _ (Var_ a) where Var a = Neut (varDB a) (Var_ a) |
274 | 274 | ||
275 | pattern Con x y <- Con_ _ x y where Con x y = Con_ (foldMap maxDB0 y) x y | 275 | pattern Con x y <- Con_ _ x y where Con x y = Con_ (foldMap maxDB_ y) x y |
276 | pattern TyCon x y <- TyCon_ _ x y where TyCon x y = TyCon_ (foldMap maxDB0 y) x y | 276 | pattern TyCon x y <- TyCon_ _ x y where TyCon x y = TyCon_ (foldMap maxDB_ y) x y |
277 | pattern Lam v x y <- Lam_ _ v x y where Lam v x y = Lam_ ({-maxDB0 x <> -}{-type erasure-} maxDB_ 1 y) v x y | 277 | pattern Lam v x y <- Lam_ _ v x y where Lam v x y = Lam_ ({-maxDB_ x <> -}{-type erasure-} lowerDB (maxDB_ y)) v x y |
278 | pattern Pi v x y <- Pi_ _ v x y where Pi v x y = Pi_ (maxDB0 x <> maxDB_ 1 y) v x y | 278 | pattern Pi v x y <- Pi_ _ v x y where Pi v x y = Pi_ (maxDB_ x <> lowerDB (maxDB_ y)) v x y |
279 | 279 | ||
280 | pattern FunN a b <- Fun (FunName a _ _) b | 280 | pattern FunN a b <- Fun (FunName a _ _) b |
281 | pattern TFun a t b <- Fun (FunName a _ t) b where TFun a t b = Fun (FunName a Nothing t) b | 281 | pattern TFun a t b <- Fun (FunName a _ t) b where TFun a t b = Fun (FunName a Nothing t) b |
@@ -510,16 +510,16 @@ instance Monoid MaxDB where | |||
510 | 510 | ||
511 | instance Show MaxDB where show _ = "MaxDB" | 511 | instance Show MaxDB where show _ = "MaxDB" |
512 | 512 | ||
513 | varDB i = MaxDB $ max 0 i | 513 | varDB i = MaxDB $ i + 1 |
514 | 514 | ||
515 | -- 0 means that no free variable is used | 515 | -- 0 means that no free variable is used |
516 | -- 1 means that only var 0 is used | 516 | -- 1 means that only var 0 is used |
517 | maxDB :: Int -> Exp -> Int | 517 | maxDB :: Exp -> Int |
518 | maxDB l e = getMaxDB $ maxDB_ l e | 518 | maxDB = max 0 . getMaxDB . maxDB_ |
519 | 519 | ||
520 | maxDB0 = maxDB_ 0 | 520 | lowerDB (MaxDB i) = MaxDB $ i-1 |
521 | 521 | ||
522 | maxDB_ i = \case | 522 | maxDB_ = \case |
523 | 523 | ||
524 | Lam_ c _ _ _ -> c | 524 | Lam_ c _ _ _ -> c |
525 | Pi_ c _ _ _ -> c | 525 | Pi_ c _ _ _ -> c |
@@ -527,13 +527,13 @@ maxDB_ i = \case | |||
527 | TyCon_ c _ _ -> c | 527 | TyCon_ c _ _ -> c |
528 | Neut c _ -> c | 528 | Neut c _ -> c |
529 | 529 | ||
530 | PMLabel x _ -> maxDB_ i x | 530 | PMLabel x _ -> maxDB_ x |
531 | FixLabel _ x -> maxDB_ i x | 531 | FixLabel _ x -> maxDB_ x |
532 | Meta a b -> maxDB_ i a <> maxDB_ (i+1) b | 532 | Meta a b -> maxDB_ a <> lowerDB (maxDB_ b) |
533 | TType -> mempty | 533 | TType -> mempty |
534 | ELit _ -> mempty | 534 | ELit _ -> mempty |
535 | Assign j x a -> handleLet i j $ \i' j' -> maxDB_ i' x <> maxDB_ i' a | 535 | -- Assign j x a -> handleLet i j $ \i' j' -> maxDB_ i' x <> maxDB_ i' a |
536 | LabelEnd x -> maxDB_ i x | 536 | LabelEnd x -> maxDB_ x |
537 | 537 | ||
538 | assign :: (Int -> Exp -> Exp -> a) -> (Int -> Exp -> Exp -> a) -> Int -> Exp -> Exp -> a | 538 | assign :: (Int -> Exp -> Exp -> a) -> (Int -> Exp -> Exp -> a) -> Int -> Exp -> Exp -> a |
539 | assign _ clet i (Var j) b | i > j = clet j (Var (i-1)) $ substE "assign" j (Var (i-1)) $ up1E i b | 539 | assign _ clet i (Var j) b | i > j = clet j (Var (i-1)) $ substE "assign" j (Var (i-1)) $ up1E i b |
@@ -575,7 +575,7 @@ freeE = foldE (\i k -> Set.fromList [k - i | k >= i]) 0 | |||
575 | usedS = (getAny .) . foldS mempty (const $ (Any .) . usedE) | 575 | usedS = (getAny .) . foldS mempty (const $ (Any .) . usedE) |
576 | 576 | ||
577 | usedE i e | 577 | usedE i e |
578 | | i > maxDB 0 e = False | 578 | | i >= maxDB e = False |
579 | | otherwise = ((getAny .) . foldE ((Any .) . (==))) i e | 579 | | otherwise = ((getAny .) . foldE ((Any .) . (==))) i e |
580 | 580 | ||
581 | mapS = mapS_ (\si _ x -> SGlobal (si, x)) | 581 | mapS = mapS_ (\si _ x -> SGlobal (si, x)) |