diff options
Diffstat (limited to 'src/LambdaCube/Compiler/Infer.hs')
-rw-r--r-- | src/LambdaCube/Compiler/Infer.hs | 8 |
1 files changed, 5 insertions, 3 deletions
diff --git a/src/LambdaCube/Compiler/Infer.hs b/src/LambdaCube/Compiler/Infer.hs index f2795657..0bff609f 100644 --- a/src/LambdaCube/Compiler/Infer.hs +++ b/src/LambdaCube/Compiler/Infer.hs | |||
@@ -435,7 +435,7 @@ type Infos = [Info] | |||
435 | -------------------------------------------------------------------------------- low-level toolbox | 435 | -------------------------------------------------------------------------------- low-level toolbox |
436 | 436 | ||
437 | label LabelFix x y = FixLabel x y | 437 | label LabelFix x y = FixLabel x y |
438 | label LabelPM x (LabelEnd y) = y | 438 | label LabelPM x (UL (LabelEnd y)) = y |
439 | label LabelPM x y = PMLabel x y | 439 | label LabelPM x y = PMLabel x y |
440 | 440 | ||
441 | pattern UBind a b c = {-UnLabel-} (Bind a b c) -- todo: review | 441 | pattern UBind a b c = {-UnLabel-} (Bind a b c) -- todo: review |
@@ -606,7 +606,7 @@ eval te = \case | |||
606 | ReflCstr a -> reflCstr te a | 606 | ReflCstr a -> reflCstr te a |
607 | Coe a b TT d -> d | 607 | Coe a b TT d -> d |
608 | 608 | ||
609 | CaseFun (CaseFunName _ t pars) (drop (pars + 1) -> ps@(last -> Con (ConName _ _ i _) (drop pars -> vs))) | i /= (-1) -> foldl app_ (ps !! i) vs | 609 | CaseFun (CaseFunName _ t pars) (drop (pars + 1) -> ps@(last -> UL (Con (ConName _ _ i _) (drop pars -> vs)))) | i /= (-1) -> foldl app_ (ps !! i) vs |
610 | TyCaseFun (TyCaseFunName n ty) [_, t, TyCon (TyConName n' _ _ _ _ _) vs, f] | n == n' -> foldl app_ t vs | 610 | TyCaseFun (TyCaseFunName n ty) [_, t, TyCon (TyConName n' _ _ _ _ _) vs, f] | n == n' -> foldl app_ t vs |
611 | TyCaseFun (TyCaseFunName n ty) [_, t, LCon, f] -> f | 611 | TyCaseFun (TyCaseFunName n ty) [_, t, LCon, f] -> f |
612 | T2 a b -> t2 a b | 612 | T2 a b -> t2 a b |
@@ -680,6 +680,8 @@ cstr = cstr__ [] | |||
680 | cstr_ [] a a' | a == a' = Unit | 680 | cstr_ [] a a' | a == a' = Unit |
681 | cstr_ ns (FixLabel _ a) a' = cstr_ ns a a' | 681 | cstr_ ns (FixLabel _ a) a' = cstr_ ns a a' |
682 | cstr_ ns a (FixLabel _ a') = cstr_ ns a a' | 682 | cstr_ ns a (FixLabel _ a') = cstr_ ns a a' |
683 | -- cstr_ ns (PMLabel a _) a' = cstr_ ns a a' | ||
684 | -- cstr_ ns a (PMLabel a' _) = cstr_ ns a a' | ||
683 | cstr_ ns TType TType = Unit | 685 | cstr_ ns TType TType = Unit |
684 | cstr_ ns (Con a []) (Con a' []) | a == a' = Unit | 686 | cstr_ ns (Con a []) (Con a' []) | a == a' = Unit |
685 | cstr_ ns (TyCon a []) (TyCon a' []) | a == a' = Unit | 687 | cstr_ ns (TyCon a []) (TyCon a' []) | a == a' = Unit |
@@ -1208,7 +1210,7 @@ handleStmt exs = \case | |||
1208 | par i (Hidden: ar) (Pi Hidden _ tt) (Lam Hidden k z) = Lam Hidden k $ par (i+1) ar tt z | 1210 | par i (Hidden: ar) (Pi Hidden _ tt) (Lam Hidden k z) = Lam Hidden k $ par (i+1) ar tt z |
1209 | par i ar@(Visible: _) (Pi Hidden _ tt) (Lam Hidden k z) = Lam Hidden k $ par (i+1) ar tt z | 1211 | par i ar@(Visible: _) (Pi Hidden _ tt) (Lam Hidden k z) = Lam Hidden k $ par (i+1) ar tt z |
1210 | par i ar tt (Var i' `App` _ `App` f) | i == i' = x where | 1212 | par i ar tt (Var i' `App` _ `App` f) | i == i' = x where |
1211 | x = label LabelPM (addLams' (FunName n mf t) ar tt $ reverse $ downTo 0 i) $ f `app_` x | 1213 | x = label LabelPM (addLams' (FunName n mf t) ar tt $ reverse $ downTo 0 i) $ label LabelFix (addLams' (FunName n mf t) ar tt $ reverse $ downTo 0 i) $ f `app_` x |
1212 | 1214 | ||
1213 | x' = x `app_` (Lam Hidden TType $ Lam Visible (Pi Visible (Var 0) (Var 1)) $ TFun "f_i_x" fixType [Var 1, Var 0]) | 1215 | x' = x `app_` (Lam Hidden TType $ Lam Visible (Pi Visible (Var 0) (Var 1)) $ TFun "f_i_x" fixType [Var 1, Var 0]) |
1214 | t = expType x' | 1216 | t = expType x' |