diff options
Diffstat (limited to 'src')
-rw-r--r-- | src/LambdaCube/Compiler.hs | 2 | ||||
-rw-r--r-- | src/LambdaCube/Compiler/Core.hs | 30 | ||||
-rw-r--r-- | src/LambdaCube/Compiler/DesugaredSource.hs | 12 | ||||
-rw-r--r-- | src/LambdaCube/Compiler/Infer.hs | 18 | ||||
-rw-r--r-- | src/LambdaCube/Compiler/Parser.hs | 4 | ||||
-rw-r--r-- | src/LambdaCube/Compiler/Statements.hs | 12 |
6 files changed, 52 insertions, 26 deletions
diff --git a/src/LambdaCube/Compiler.hs b/src/LambdaCube/Compiler.hs index 60412e25..46288639 100644 --- a/src/LambdaCube/Compiler.hs +++ b/src/LambdaCube/Compiler.hs | |||
@@ -52,7 +52,7 @@ import LambdaCube.Compiler.CoreToIR | |||
52 | 52 | ||
53 | import LambdaCube.Compiler.Utils | 53 | import LambdaCube.Compiler.Utils |
54 | import LambdaCube.Compiler.DesugaredSource as Exported (FileInfo(..), Range(..), SPos(..), SIName(..), pattern SIName, sName, SI(..)) | 54 | import LambdaCube.Compiler.DesugaredSource as Exported (FileInfo(..), Range(..), SPos(..), SIName(..), pattern SIName, sName, SI(..)) |
55 | import LambdaCube.Compiler.Core as Exported (mkDoc, Exp, ExpType(..), outputType, boolType, trueExp, hnf) | 55 | import LambdaCube.Compiler.Core as Exported (mkDoc, Exp, ExpType(..), pattern ET, outputType, boolType, trueExp, hnf) |
56 | import LambdaCube.Compiler.InferMonad as Exported (errorRange, listAllInfos, listAllInfos', listTypeInfos, listTraceInfos, Infos, Info(..)) | 56 | import LambdaCube.Compiler.InferMonad as Exported (errorRange, listAllInfos, listAllInfos', listTypeInfos, listTraceInfos, Infos, Info(..)) |
57 | --import LambdaCube.Compiler.Infer as Exported () | 57 | --import LambdaCube.Compiler.Infer as Exported () |
58 | 58 | ||
diff --git a/src/LambdaCube/Compiler/Core.hs b/src/LambdaCube/Compiler/Core.hs index 273791a7..0a221d2c 100644 --- a/src/LambdaCube/Compiler/Core.hs +++ b/src/LambdaCube/Compiler/Core.hs | |||
@@ -148,6 +148,7 @@ data Exp | |||
148 | | Pi_ !MaxDB Visibility Exp Exp | 148 | | Pi_ !MaxDB Visibility Exp Exp |
149 | | Neut Neutral | 149 | | Neut Neutral |
150 | | RHS Exp{-always in hnf-} | 150 | | RHS Exp{-always in hnf-} |
151 | | Let_ !MaxDB ExpType Exp | ||
151 | 152 | ||
152 | data Neutral | 153 | data Neutral |
153 | = Var_ !Int{-De Bruijn index-} | 154 | = Var_ !Int{-De Bruijn index-} |
@@ -155,7 +156,6 @@ data Neutral | |||
155 | | CaseFun__ !MaxDB CaseFunName [Exp] Neutral | 156 | | CaseFun__ !MaxDB CaseFunName [Exp] Neutral |
156 | | TyCaseFun__ !MaxDB TyCaseFunName [Exp] Neutral | 157 | | TyCaseFun__ !MaxDB TyCaseFunName [Exp] Neutral |
157 | | Fun_ !MaxDB FunName [Exp]{-given parameters, reversed-} Exp{-unfolded expression, in hnf-} | 158 | | Fun_ !MaxDB FunName [Exp]{-given parameters, reversed-} Exp{-unfolded expression, in hnf-} |
158 | -- | Let_ !MaxDB | ||
159 | 159 | ||
160 | -------------------------------------------------------------------------------- auxiliary functions and patterns | 160 | -------------------------------------------------------------------------------- auxiliary functions and patterns |
161 | 161 | ||
@@ -163,7 +163,10 @@ type Type = Exp | |||
163 | 163 | ||
164 | data ExpType = ET {expr :: Exp, ty :: Type} | 164 | data ExpType = ET {expr :: Exp, ty :: Type} |
165 | deriving (Eq) | 165 | deriving (Eq) |
166 | 166 | {- | |
167 | pattern ET a b <- ET_ a b | ||
168 | where ET a b = ET_ a (hnf b) | ||
169 | -} | ||
167 | instance Rearrange ExpType where | 170 | instance Rearrange ExpType where |
168 | rearrange l f (ET e t) = ET (rearrange l f e) (rearrange l f t) | 171 | rearrange l f (ET e t) = ET (rearrange l f e) (rearrange l f t) |
169 | 172 | ||
@@ -201,6 +204,13 @@ pattern Lam y <- Lam_ _ y | |||
201 | where Lam y = Lam_ (lowerDB (maxDB_ y)) y | 204 | where Lam y = Lam_ (lowerDB (maxDB_ y)) y |
202 | pattern Pi v x y <- Pi_ _ v x y | 205 | pattern Pi v x y <- Pi_ _ v x y |
203 | where Pi v x y = Pi_ (maxDB_ x <> lowerDB (maxDB_ y)) v x y | 206 | where Pi v x y = Pi_ (maxDB_ x <> lowerDB (maxDB_ y)) v x y |
207 | pattern Let x y <- Let_ _ x y | ||
208 | where Let x y = Let_ (maxDB_ x <> lowerDB (maxDB_ y)) x y | ||
209 | |||
210 | pattern SubstLet x <- (substLet -> Just x) | ||
211 | |||
212 | substLet (Let x y) = Just $ subst 0 (expr x) y | ||
213 | substLet _ = Nothing | ||
204 | 214 | ||
205 | pattern CaseFun a b c = Neut (CaseFun_ a b c) | 215 | pattern CaseFun a b c = Neut (CaseFun_ a b c) |
206 | pattern TyCaseFun a b c = Neut (TyCaseFun_ a b c) | 216 | pattern TyCaseFun a b c = Neut (TyCaseFun_ a b c) |
@@ -306,9 +316,14 @@ mkFun :: FunName -> [Exp] -> Exp -> Exp | |||
306 | mkFun f xs e = mkFun_ (foldMap maxDB_ xs) f xs e | 316 | mkFun f xs e = mkFun_ (foldMap maxDB_ xs) f xs e |
307 | 317 | ||
308 | pattern ReducedN y <- Fun f _ (RHS y) | 318 | pattern ReducedN y <- Fun f _ (RHS y) |
309 | pattern Reduced y <- Neut (ReducedN y) | 319 | pattern Reduced y <- (reduce -> Just y) |
320 | |||
321 | -- TODO: too much hnf call | ||
322 | reduce (Neut (ReducedN y)) = Just $ hnf y | ||
323 | reduce (SubstLet x) = Just $ hnf x | ||
324 | reduce _ = Nothing | ||
310 | 325 | ||
311 | hnf (Reduced y) = y | 326 | hnf (reduce -> Just y) = y |
312 | hnf a = a | 327 | hnf a = a |
313 | 328 | ||
314 | outputType = tTyCon0 FOutput $ error "cs 9" | 329 | outputType = tTyCon0 FOutput $ error "cs 9" |
@@ -385,6 +400,7 @@ instance Subst Exp Exp where | |||
385 | Con_ md s n as -> Con_ (md <> upDB i dx) s n $ f i <$> as | 400 | Con_ md s n as -> Con_ (md <> upDB i dx) s n $ f i <$> as |
386 | Pi_ md h a b -> Pi_ (md <> upDB i dx) h (f i a) (f (i+1) b) | 401 | Pi_ md h a b -> Pi_ (md <> upDB i dx) h (f i a) (f (i+1) b) |
387 | TyCon_ md s as -> TyCon_ (md <> upDB i dx) s $ f i <$> as | 402 | TyCon_ md s as -> TyCon_ (md <> upDB i dx) s $ f i <$> as |
403 | Let_ md a b -> Let_ (md <> upDB i dx) (subst_ i dx x a) (f (i+1) b) | ||
388 | RHS a -> RHS $ hnf $ f i a | 404 | RHS a -> RHS $ hnf $ f i a |
389 | 405 | ||
390 | instance Rearrange Exp where | 406 | instance Rearrange Exp where |
@@ -396,6 +412,7 @@ instance Rearrange Exp where | |||
396 | Con_ md s pn as -> Con_ (upDB_ g i md) s pn $ map (f i) as | 412 | Con_ md s pn as -> Con_ (upDB_ g i md) s pn $ map (f i) as |
397 | TyCon_ md s as -> TyCon_ (upDB_ g i md) s $ map (f i) as | 413 | TyCon_ md s as -> TyCon_ (upDB_ g i md) s $ map (f i) as |
398 | Neut x -> Neut $ rearrange i g x | 414 | Neut x -> Neut $ rearrange i g x |
415 | Let x y -> Let (rearrange i g x) (rearrange (i+1) g y) | ||
399 | RHS x -> RHS $ rearrange i g x | 416 | RHS x -> RHS $ rearrange i g x |
400 | 417 | ||
401 | instance Rearrange Neutral where | 418 | instance Rearrange Neutral where |
@@ -421,6 +438,7 @@ instance Up Exp where | |||
421 | TType_ _ -> mempty | 438 | TType_ _ -> mempty |
422 | ELit{} -> mempty | 439 | ELit{} -> mempty |
423 | Neut x -> foldVar f i x | 440 | Neut x -> foldVar f i x |
441 | Let x y -> foldVar f i x <> foldVar f (i+1) y | ||
424 | RHS x -> foldVar f i x | 442 | RHS x -> foldVar f i x |
425 | 443 | ||
426 | instance Up Neutral where | 444 | instance Up Neutral where |
@@ -445,6 +463,7 @@ instance HasMaxDB Exp where | |||
445 | Pi_ c _ _ _ -> c | 463 | Pi_ c _ _ _ -> c |
446 | Con_ c _ _ _ -> c | 464 | Con_ c _ _ _ -> c |
447 | TyCon_ c _ _ -> c | 465 | TyCon_ c _ _ -> c |
466 | Let_ c _ _ -> c | ||
448 | 467 | ||
449 | TType_ _ -> mempty | 468 | TType_ _ -> mempty |
450 | ELit{} -> mempty | 469 | ELit{} -> mempty |
@@ -481,6 +500,7 @@ instance ClosedExp Exp where | |||
481 | e@TType_{} -> e | 500 | e@TType_{} -> e |
482 | e@ELit{} -> e | 501 | e@ELit{} -> e |
483 | Neut a -> Neut $ closedExp a | 502 | Neut a -> Neut $ closedExp a |
503 | Let a b -> Let_ mempty a b | ||
484 | RHS a -> RHS (closedExp a) | 504 | RHS a -> RHS (closedExp a) |
485 | 505 | ||
486 | instance ClosedExp Neutral where | 506 | instance ClosedExp Neutral where |
@@ -519,6 +539,7 @@ instance MkDoc Exp where | |||
519 | TType -> text "Type" | 539 | TType -> text "Type" |
520 | ELit l -> pShow l | 540 | ELit l -> pShow l |
521 | Neut x -> mkDoc pr x | 541 | Neut x -> mkDoc pr x |
542 | Let a b -> shLet_ (pShow a) (pShow b) | ||
522 | RHS x -> text "_rhs" `DApp` mkDoc pr x | 543 | RHS x -> text "_rhs" `DApp` mkDoc pr x |
523 | 544 | ||
524 | showNth n = show n ++ f (n `div` 10 `mod` 10) (n `mod` 10) | 545 | showNth n = show n ++ f (n `div` 10 `mod` 10) (n `mod` 10) |
@@ -719,6 +740,7 @@ app_ :: Exp -> Exp -> Exp | |||
719 | app_ (Lam x) a = subst 0 a x | 740 | app_ (Lam x) a = subst 0 a x |
720 | app_ (Con s n xs) a = if n < conParams s then Con s (n+1) xs else Con s n (xs ++ [a]) | 741 | app_ (Con s n xs) a = if n < conParams s then Con s (n+1) xs else Con s n (xs ++ [a]) |
721 | app_ (TyCon s xs) a = TyCon s (xs ++ [a]) | 742 | app_ (TyCon s xs) a = TyCon s (xs ++ [a]) |
743 | app_ (SubstLet f) a = app_ f a | ||
722 | app_ (Neut f) a = neutApp f a | 744 | app_ (Neut f) a = neutApp f a |
723 | where | 745 | where |
724 | neutApp (ReducedN x) a = app_ x a -- ??? | 746 | neutApp (ReducedN x) a = app_ x a -- ??? |
diff --git a/src/LambdaCube/Compiler/DesugaredSource.hs b/src/LambdaCube/Compiler/DesugaredSource.hs index d47726d0..325338bf 100644 --- a/src/LambdaCube/Compiler/DesugaredSource.hs +++ b/src/LambdaCube/Compiler/DesugaredSource.hs | |||
@@ -533,22 +533,22 @@ shLet_ a b = DFreshName True $ showLet (DLet "=" (shVar 0) $ DUp 0 a) b | |||
533 | -------------------------------------------------------------------------------- statement | 533 | -------------------------------------------------------------------------------- statement |
534 | 534 | ||
535 | data Stmt | 535 | data Stmt |
536 | = Let SIName (Maybe SExp) SExp | 536 | = StLet SIName (Maybe SExp) SExp |
537 | | Data SIName [(Visibility, SExp)]{-parameters-} SExp{-type-} [(SIName, SExp)]{-constructor names and types-} | 537 | | Data SIName [(Visibility, SExp)]{-parameters-} SExp{-type-} [(SIName, SExp)]{-constructor names and types-} |
538 | | PrecDef SIName Fixity | 538 | | PrecDef SIName Fixity |
539 | 539 | ||
540 | pattern Primitive n t = Let n (Just t) (SBuiltin "undefined") | 540 | pattern Primitive n t = StLet n (Just t) (SBuiltin "undefined") |
541 | 541 | ||
542 | instance PShow Stmt where | 542 | instance PShow Stmt where |
543 | pShow stmt = vcat . map DResetFreshNames $ case stmt of | 543 | pShow stmt = vcat . map DResetFreshNames $ case stmt of |
544 | Primitive n t -> pure $ shAnn (pShow n) (pShow t) | 544 | Primitive n t -> pure $ shAnn (pShow n) (pShow t) |
545 | Let n ty e -> [shAnn (pShow n) (pShow t) | Just t <- [ty]] ++ [DLet "=" (pShow n) (pShow e)] | 545 | StLet n ty e -> [shAnn (pShow n) (pShow t) | Just t <- [ty]] ++ [DLet "=" (pShow n) (pShow e)] |
546 | Data n ps ty cs -> pure $ nest 2 $ "data" <+> nest 2 (shAnn (foldl DApp (DTypeNamespace True $ pShow n) [shAnn (text "_") (pShow t) | (v, t) <- ps]) (pShow ty)) </> "where" <> nest 2 (hardline <> vcat [shAnn (pShow n) $ pShow $ UncurryS (first (const Hidden) <$> ps) t | (n, t) <- cs]) | 546 | Data n ps ty cs -> pure $ nest 2 $ "data" <+> nest 2 (shAnn (foldl DApp (DTypeNamespace True $ pShow n) [shAnn (text "_") (pShow t) | (v, t) <- ps]) (pShow ty)) </> "where" <> nest 2 (hardline <> vcat [shAnn (pShow n) $ pShow $ UncurryS (first (const Hidden) <$> ps) t | (n, t) <- cs]) |
547 | PrecDef n i -> pure $ pShow i <+> text (sName n) --DOp0 (sName n) i | 547 | PrecDef n i -> pure $ pShow i <+> text (sName n) --DOp0 (sName n) i |
548 | 548 | ||
549 | instance DeBruijnify SIName Stmt where | 549 | instance DeBruijnify SIName Stmt where |
550 | deBruijnify_ k v = \case | 550 | deBruijnify_ k v = \case |
551 | Let sn mt e -> Let sn (deBruijnify_ k v <$> mt) (deBruijnify_ k v e) | 551 | StLet sn mt e -> StLet sn (deBruijnify_ k v <$> mt) (deBruijnify_ k v e) |
552 | x -> error $ "deBruijnify @ " ++ ppShow x | 552 | x -> error $ "deBruijnify @ " ++ ppShow x |
553 | 553 | ||
554 | -------------------------------------------------------------------------------- statement with dependencies | 554 | -------------------------------------------------------------------------------- statement with dependencies |
@@ -570,7 +570,7 @@ sortDefs xs = map snValue <$> scc snId snChildren snRevChildren nodes | |||
570 | where | 570 | where |
571 | need = Set.toList $ case s of | 571 | need = Set.toList $ case s of |
572 | PrecDef{} -> mempty | 572 | PrecDef{} -> mempty |
573 | Let _ mt e -> foldMap names mt <> names e | 573 | StLet _ mt e -> foldMap names mt <> names e |
574 | Data _ ps t cs -> foldMap (names . snd) ps <> names t <> foldMap (names . snd) cs | 574 | Data _ ps t cs -> foldMap (names . snd) ps <> names t <> foldMap (names . snd) cs |
575 | 575 | ||
576 | names = foldName Set.singleton | 576 | names = foldName Set.singleton |
@@ -581,7 +581,7 @@ sortDefs xs = map snValue <$> scc snId snChildren snRevChildren nodes | |||
581 | where | 581 | where |
582 | def = \case | 582 | def = \case |
583 | PrecDef{} -> mempty | 583 | PrecDef{} -> mempty |
584 | Let n _ _ -> [n] | 584 | StLet n _ _ -> [n] |
585 | Data n _ _ cs -> n: map fst cs | 585 | Data n _ _ cs -> n: map fst cs |
586 | 586 | ||
587 | -------------------------------------------------------------------------------- module | 587 | -------------------------------------------------------------------------------- module |
diff --git a/src/LambdaCube/Compiler/Infer.hs b/src/LambdaCube/Compiler/Infer.hs index 3b8bdd5a..38269b0e 100644 --- a/src/LambdaCube/Compiler/Infer.hs +++ b/src/LambdaCube/Compiler/Infer.hs | |||
@@ -227,6 +227,9 @@ inferN e s = do | |||
227 | 227 | ||
228 | substTo i x = subst i x . up1_ (i+1) | 228 | substTo i x = subst i x . up1_ (i+1) |
229 | 229 | ||
230 | mkLet x xt y = subst 0 x y | ||
231 | --mkLet x xt (ET y yt) = ET (Let (ET x xt) y) yt | ||
232 | |||
230 | inferN_ :: forall m . Monad m => (forall a . String -> String -> IM m a -> IM m a) -> Env -> SExp2 -> IM m ExpType' | 233 | inferN_ :: forall m . Monad m => (forall a . String -> String -> IM m a -> IM m a) -> Env -> SExp2 -> IM m ExpType' |
231 | inferN_ tellTrace = infer where | 234 | inferN_ tellTrace = infer where |
232 | 235 | ||
@@ -243,7 +246,7 @@ inferN_ tellTrace = infer where | |||
243 | SApp_ si h a b -> infer (EApp1 (si `validate` [sourceInfo a, sourceInfo b]) h te b) a | 246 | SApp_ si h a b -> infer (EApp1 (si `validate` [sourceInfo a, sourceInfo b]) h te b) a |
244 | SBind_ si h _ a b -> infer ((if h /= BMeta then CheckType_ (sourceInfo exp) TType else id) $ EBind1 si h te $ (if isPi h then TyType else id) b) a | 247 | SBind_ si h _ a b -> infer ((if h /= BMeta then CheckType_ (sourceInfo exp) TType else id) $ EBind1 si h te $ (if isPi h then TyType else id) b) a |
245 | 248 | ||
246 | checkN :: Env -> SExp2 -> Type -> IM m ExpType' | 249 | checkN :: Env -> SExp2 -> Type{-hnf-} -> IM m ExpType' |
247 | checkN te x t = tellTrace "check" (showEnvSExpType te x t) $ checkN_ te x t | 250 | checkN te x t = tellTrace "check" (showEnvSExpType te x t) $ checkN_ te x t |
248 | 251 | ||
249 | checkN_ te (Parens e) t = checkN_ te e t | 252 | checkN_ te (Parens e) t = checkN_ te e t |
@@ -269,10 +272,10 @@ inferN_ tellTrace = infer where | |||
269 | | SLam h a b <- e, Pi h' x y <- t, h == h' = do | 272 | | SLam h a b <- e, Pi h' x y <- t, h == h' = do |
270 | -- tellType e t | 273 | -- tellType e t |
271 | let same = checkSame te a x | 274 | let same = checkSame te a x |
272 | if same then checkN (EBind2 (BLam h) x te) b y else error $ "checkSame:\n" ++ ppShow a ++ "\nwith\n" ++ showEnvExp te (ET x TType) | 275 | if same then checkN (EBind2 (BLam h) x te) b $ hnf y else error $ "checkSame:\n" ++ ppShow a ++ "\nwith\n" ++ showEnvExp te (ET x TType) |
273 | | Pi Hidden a b <- t = do | 276 | | Pi Hidden a b <- t = do |
274 | bb <- notHiddenLam e | 277 | bb <- notHiddenLam e |
275 | if bb then checkN (EBind2 (BLam Hidden) a te) (up1 e) b | 278 | if bb then checkN (EBind2 (BLam Hidden) a te) (up1 e) $ hnf b |
276 | else infer (CheckType_ (sourceInfo e) t te) e | 279 | else infer (CheckType_ (sourceInfo e) t te) e |
277 | | otherwise = infer (CheckType_ (sourceInfo e) t te) e | 280 | | otherwise = infer (CheckType_ (sourceInfo e) t te) e |
278 | where | 281 | where |
@@ -313,15 +316,15 @@ inferN_ tellTrace = infer where | |||
313 | _ -> focus_ (EBind2_ (sourceInfo b) BMeta (cstr_ TType t y) $ EApp1 si h te b) $ up 1 eet | 316 | _ -> focus_ (EBind2_ (sourceInfo b) BMeta (cstr_ TType t y) $ EApp1 si h te b) $ up 1 eet |
314 | | otherwise -> focus_ (EApp1 si h (CheckType_ (sourceInfo b) t te) b) eet | 317 | | otherwise -> focus_ (EApp1 si h (CheckType_ (sourceInfo b) t te) b) eet |
315 | EApp1 si h te b | 318 | EApp1 si h te b |
316 | | Pi h' x y <- et, h == h' -> checkN (EApp2 si h eet te) b x | 319 | | Pi h' x y <- et, h == h' -> checkN (EApp2 si h eet te) b $ hnf x |
317 | | Pi Hidden x y <- et, h == Visible -> focus_ (EApp1 mempty Hidden env $ Wildcard $ Wildcard SType) eet -- e b --> e _ b | 320 | | Pi Hidden x y <- et, h == Visible -> focus_ (EApp1 mempty Hidden env $ Wildcard $ Wildcard SType) eet -- e b --> e _ b |
318 | -- | CheckType (Pi Hidden _ _) te' <- te -> error "ok" | 321 | -- | CheckType (Pi Hidden _ _) te' <- te -> error "ok" |
319 | -- | CheckAppType Hidden _ te' _ <- te -> error "ok" | 322 | -- | CheckAppType Hidden _ te' _ <- te -> error "ok" |
320 | | otherwise -> infer (CheckType_ (sourceInfo b) (Var 2) $ cstr' h (up 2 et) (Pi Visible (Var 1) (Var 1)) (up 2 e) $ EBind2_ (sourceInfo b) BMeta TType $ EBind2_ (sourceInfo b) BMeta TType te) (up 3 b) | 323 | | otherwise -> infer (CheckType_ (sourceInfo b) (Var 2) $ cstr' h (up 2 et) (Pi Visible (Var 1) (Var 1)) (up 2 e) $ EBind2_ (sourceInfo b) BMeta TType $ EBind2_ (sourceInfo b) BMeta TType te) (up 3 b) |
321 | where | 324 | where |
322 | cstr' h x y e = EApp2 mempty h (ET (evalCoe (up 1 x) (up 1 y) (Var 0) (up 1 e)) (up 1 y)) . EBind2_ (sourceInfo b) BMeta (cstr_ TType x y) | 325 | cstr' h x y e = EApp2 mempty h (ET (evalCoe (up 1 x) (up 1 y) (Var 0) (up 1 e)) (up 1 y)) . EBind2_ (sourceInfo b) BMeta (cstr_ TType x y) |
323 | ELet2 ln (ET x{-let-} xt) te -> focus_ te $ subst 0 (mkELet ln x xt te){-let-} eet{-in-} | 326 | ELet2 ln (ET x{-let-} xt) te -> focus_ te $ mkLet (mkELet ln x xt te){-let-} xt eet{-in-} |
324 | CheckIType x te -> checkN te x e | 327 | CheckIType x te -> checkN te x $ hnf e |
325 | CheckType_ si t te | 328 | CheckType_ si t te |
326 | | hArgs et > hArgs t | 329 | | hArgs et > hArgs t |
327 | -> focus_ (EApp1 mempty Hidden (CheckType_ si t te) $ Wildcard $ Wildcard SType) eet | 330 | -> focus_ (EApp1 mempty Hidden (CheckType_ si t te) $ Wildcard $ Wildcard SType) eet |
@@ -461,6 +464,7 @@ recheck' sn e (ET x xt) = ET (recheck_ "main" (checkEnv e) (ET x xt)) xt | |||
461 | ET (CaseFun s@(CaseFunName _ t pars) as n) zt -> checkApps (ppShow s) [] zt (\xs -> evalCaseFun s (init $ drop pars xs) (last xs)) te (nType s) (makeCaseFunPars te n ++ as ++ [Neut n]) | 464 | ET (CaseFun s@(CaseFunName _ t pars) as n) zt -> checkApps (ppShow s) [] zt (\xs -> evalCaseFun s (init $ drop pars xs) (last xs)) te (nType s) (makeCaseFunPars te n ++ as ++ [Neut n]) |
462 | ET (TyCaseFun s [m, t, f] n) zt -> checkApps (ppShow s) [] zt (\[m, t, n, f] -> evalTyCaseFun s [m, t, f] n) te (nType s) [m, t, Neut n, f] | 465 | ET (TyCaseFun s [m, t, f] n) zt -> checkApps (ppShow s) [] zt (\[m, t, n, f] -> evalTyCaseFun s [m, t, f] n) te (nType s) [m, t, Neut n, f] |
463 | ET (Neut (Fun_ md f a x)) zt -> checkApps ("lab-" ++ show f ++ ppShow a ++ "\n" ++ ppShow (nType f)) [] zt (\xs -> Neut $ Fun_ md f (reverse xs) x) te (nType f) $ reverse a -- TODO: recheck x | 466 | ET (Neut (Fun_ md f a x)) zt -> checkApps ("lab-" ++ show f ++ ppShow a ++ "\n" ++ ppShow (nType f)) [] zt (\xs -> Neut $ Fun_ md f (reverse xs) x) te (nType f) $ reverse a -- TODO: recheck x |
467 | ET (Let (ET x xt) y) zt -> Let (recheck'' "let" te $ ET x xt) $ recheck_ "let_in" te $ ET y (Pi Visible xt $ up1 zt) -- TODO | ||
464 | ET (RHS x) zt -> RHS $ recheck_ msg te (ET x zt) | 468 | ET (RHS x) zt -> RHS $ recheck_ msg te (ET x zt) |
465 | where | 469 | where |
466 | checkApps s acc zt f _ t [] | 470 | checkApps s acc zt f _ t [] |
@@ -485,7 +489,7 @@ handleStmt = \case | |||
485 | t <- inferType n $ trSExp' t_ | 489 | t <- inferType n $ trSExp' t_ |
486 | tellType (sourceInfo n) t | 490 | tellType (sourceInfo n) t |
487 | addToEnv n $ flip ET t $ lamify t $ DFun (mkFName n) t | 491 | addToEnv n $ flip ET t $ lamify t $ DFun (mkFName n) t |
488 | Let n mt t_ -> do | 492 | StLet n mt t_ -> do |
489 | let t__ = maybe id (flip SAnn) mt t_ | 493 | let t__ = maybe id (flip SAnn) mt t_ |
490 | ET x t <- inferTerm n $ trSExp' $ addFix n t__ | 494 | ET x t <- inferTerm n $ trSExp' $ addFix n t__ |
491 | tellType (sourceInfo n) t | 495 | tellType (sourceInfo n) t |
diff --git a/src/LambdaCube/Compiler/Parser.hs b/src/LambdaCube/Compiler/Parser.hs index f4ea8489..1d5139b8 100644 --- a/src/LambdaCube/Compiler/Parser.hs +++ b/src/LambdaCube/Compiler/Parser.hs | |||
@@ -131,7 +131,7 @@ mkDesugarInfo ss = DesugarInfo | |||
131 | , consMap = Map.fromList $ | 131 | , consMap = Map.fromList $ |
132 | [(sName cn, Left ((CaseName $ sName t, pars ty), second pars <$> cs)) | Data t ps ty cs <- ss, (cn, ct) <- cs] | 132 | [(sName cn, Left ((CaseName $ sName t, pars ty), second pars <$> cs)) | Data t ps ty cs <- ss, (cn, ct) <- cs] |
133 | ++ [(sName t, Right $ pars $ UncurryS ps ty) | Data t ps ty _ <- ss] | 133 | ++ [(sName t, Right $ pars $ UncurryS ps ty) | Data t ps ty _ <- ss] |
134 | -- ++ [(t, Right $ length xs) | Let (_, t) _ (Just ty) xs _ <- ss] | 134 | -- ++ [(t, Right $ length xs) | StLet (_, t) _ (Just ty) xs _ <- ss] |
135 | ++ [("'Type", Right 0)] | 135 | ++ [("'Type", Right 0)] |
136 | , definedSet = Set.singleton "'Type" <> foldMap defined ss | 136 | , definedSet = Set.singleton "'Type" <> foldMap defined ss |
137 | } | 137 | } |
@@ -139,7 +139,7 @@ mkDesugarInfo ss = DesugarInfo | |||
139 | pars (UncurryS l _) = length $ filter ((== Visible) . fst) l -- todo | 139 | pars (UncurryS l _) = length $ filter ((== Visible) . fst) l -- todo |
140 | 140 | ||
141 | defined = \case | 141 | defined = \case |
142 | Let sn _ _ -> Set.singleton $ sName sn | 142 | StLet sn _ _ -> Set.singleton $ sName sn |
143 | Data sn _ _ cs -> Set.fromList $ sName sn: map (sName . fst) cs | 143 | Data sn _ _ cs -> Set.fromList $ sName sn: map (sName . fst) cs |
144 | PrecDef{} -> mempty | 144 | PrecDef{} -> mempty |
145 | 145 | ||
diff --git a/src/LambdaCube/Compiler/Statements.hs b/src/LambdaCube/Compiler/Statements.hs index 42f02b07..1ce2beb6 100644 --- a/src/LambdaCube/Compiler/Statements.hs +++ b/src/LambdaCube/Compiler/Statements.hs | |||
@@ -49,7 +49,7 @@ mkLets_ mkLet = mkLets' mkLet . concatMap desugarMutual . sortDefs | |||
49 | 49 | ||
50 | mkLets' mkLet = f where | 50 | mkLets' mkLet = f where |
51 | f [] e = e | 51 | f [] e = e |
52 | f (Let n mt x: ds) e = mkLet n (maybe id (flip SAnn) mt (addFix n x)) (deBruijnify [n] $ f ds e) | 52 | f (StLet n mt x: ds) e = mkLet n (maybe id (flip SAnn) mt (addFix n x)) (deBruijnify [n] $ f ds e) |
53 | f (PrecDef{}: ds) e = f ds e | 53 | f (PrecDef{}: ds) e = f ds e |
54 | f (x: ds) e = error $ "mkLets: " ++ ppShow x | 54 | f (x: ds) e = error $ "mkLets: " ++ ppShow x |
55 | 55 | ||
@@ -57,7 +57,7 @@ addFix n x | |||
57 | | usedS n x = SBuiltin "primFix" `SAppV` SLamV (deBruijnify [n] x) | 57 | | usedS n x = SBuiltin "primFix" `SAppV` SLamV (deBruijnify [n] x) |
58 | | otherwise = x | 58 | | otherwise = x |
59 | 59 | ||
60 | addFix' (Let n nt nd) = Let n nt $ addFix n nd | 60 | addFix' (StLet n nt nd) = StLet n nt $ addFix n nd |
61 | addFix' x = x | 61 | addFix' x = x |
62 | 62 | ||
63 | type DefinedSet = Set.Set SName | 63 | type DefinedSet = Set.Set SName |
@@ -97,7 +97,7 @@ compileStmt compilegt ds = \case | |||
97 | -- , let ts = fst $ getParamsS $ up1 t | 97 | -- , let ts = fst $ getParamsS $ up1 t |
98 | , let as = [ funAlt m p $ noGuards {- -$ SLam Hidden (Wildcard SType) $ up1 -} $ SLet m' e $ sVar "cst" 0 | 98 | , let as = [ funAlt m p $ noGuards {- -$ SLam Hidden (Wildcard SType) $ up1 -} $ SLet m' e $ sVar "cst" 0 |
99 | | Instance n' i cstrs alts <- ds, n' == n | 99 | | Instance n' i cstrs alts <- ds, n' == n |
100 | , Let m' ~Nothing e <- alts, m' == m | 100 | , StLet m' ~Nothing e <- alts, m' == m |
101 | , let p = zip ((,) Hidden <$> ps) i ++ [((Hidden, Wildcard SType), PVarSimp $ dummyName "cst2")] | 101 | , let p = zip ((,) Hidden <$> ps) i ++ [((Hidden, Wildcard SType), PVarSimp $ dummyName "cst2")] |
102 | -- , let ic = patVars i | 102 | -- , let ic = patVars i |
103 | ] | 103 | ] |
@@ -113,7 +113,7 @@ compileStmt compilegt ds = \case | |||
113 | | n `elem` [n' | TypeFamily n' _ <- ds] -> return [] | 113 | | n `elem` [n' | TypeFamily n' _ <- ds] -> return [] |
114 | | otherwise -> do | 114 | | otherwise -> do |
115 | cf <- compilegt (SIName_ (mconcat [sourceInfo n | FunAlt n _ _ <- fs]) (nameFixity n) $ sName n) vs [gt | FunAlt _ _ gt <- fs] | 115 | cf <- compilegt (SIName_ (mconcat [sourceInfo n | FunAlt n _ _ <- fs]) (nameFixity n) $ sName n) vs [gt | FunAlt _ _ gt <- fs] |
116 | return [Let n (listToMaybe [t | TypeAnn n' t <- ds, n' == n]) cf] | 116 | return [StLet n (listToMaybe [t | TypeAnn n' t <- ds, n' == n]) cf] |
117 | fs -> fail $ "different number of arguments of " ++ sName n ++ ":\n" ++ show (vcat $ pShow . sourceInfo . snd . head <$> fs) | 117 | fs -> fail $ "different number of arguments of " ++ sName n ++ ":\n" ++ show (vcat $ pShow . sourceInfo . snd . head <$> fs) |
118 | [Stmt x] -> return [x] | 118 | [Stmt x] -> return [x] |
119 | where | 119 | where |
@@ -134,7 +134,7 @@ desugarValueDef p e = sequence | |||
134 | dns = reverse $ getPVars p | 134 | dns = reverse $ getPVars p |
135 | n = mangleNames dns | 135 | n = mangleNames dns |
136 | 136 | ||
137 | getLet (Let x Nothing (SRHS dx)) = Just (x, dx) | 137 | getLet (StLet x Nothing (SRHS dx)) = Just (x, dx) |
138 | getLet _ = Nothing | 138 | getLet _ = Nothing |
139 | 139 | ||
140 | fst' (x, _) = x -- TODO | 140 | fst' (x, _) = x -- TODO |
@@ -144,7 +144,7 @@ desugarMutual [x] = [x] | |||
144 | desugarMutual (traverse getLet -> Just (unzip -> (ns, ds))) = fst' $ runWriter $ do | 144 | desugarMutual (traverse getLet -> Just (unzip -> (ns, ds))) = fst' $ runWriter $ do |
145 | ss <- compileStmt' =<< desugarValueDef (foldr cHCons cHNil $ PVarSimp <$> ns) (SGlobal xy) | 145 | ss <- compileStmt' =<< desugarValueDef (foldr cHCons cHNil $ PVarSimp <$> ns) (SGlobal xy) |
146 | return $ | 146 | return $ |
147 | Let xy Nothing (addFix xy $ SRHS $ mkLets' SLet ss $ foldr HCons HNil ds) : ss | 147 | StLet xy Nothing (addFix xy $ SRHS $ mkLets' SLet ss $ foldr HCons HNil ds) : ss |
148 | where | 148 | where |
149 | xy = mangleNames ns | 149 | xy = mangleNames ns |
150 | desugarMutual xs = error "desugarMutual" | 150 | desugarMutual xs = error "desugarMutual" |