diff options
-rw-r--r-- | TODO | 2 | ||||
-rw-r--r-- | src/LambdaCube/Compiler.hs | 2 | ||||
-rw-r--r-- | src/LambdaCube/Compiler/Infer.hs | 214 | ||||
-rw-r--r-- | src/LambdaCube/Compiler/Parser.hs | 13 |
4 files changed, 133 insertions, 98 deletions
@@ -76,6 +76,7 @@ done: | |||
76 | - backend: support Texture2DSlot (purescript) | 76 | - backend: support Texture2DSlot (purescript) |
77 | - editor: user texture support (no crossdomain support) | 77 | - editor: user texture support (no crossdomain support) |
78 | - normalized variable names in the generated pipeline (so that the same structures have to be equal) | 78 | - normalized variable names in the generated pipeline (so that the same structures have to be equal) |
79 | - move to megaparsec | ||
79 | 80 | ||
80 | next: | 81 | next: |
81 | 82 | ||
@@ -160,7 +161,6 @@ extra (improvement): | |||
160 | 161 | ||
161 | extra (refactoring): | 162 | extra (refactoring): |
162 | - compiler: refactor pretty printing | 163 | - compiler: refactor pretty printing |
163 | - move to megaparsec | ||
164 | 164 | ||
165 | ------------------------------------------------------------------- weeks Feb 22, Feb 29 | 165 | ------------------------------------------------------------------- weeks Feb 22, Feb 29 |
166 | 166 | ||
diff --git a/src/LambdaCube/Compiler.hs b/src/LambdaCube/Compiler.hs index e5496062..f6e2ccd3 100644 --- a/src/LambdaCube/Compiler.hs +++ b/src/LambdaCube/Compiler.hs | |||
@@ -145,7 +145,7 @@ loadModule imp mname = do | |||
145 | ms <- mapM loadModuleImports $ moduleImports e | 145 | ms <- mapM loadModuleImports $ moduleImports e |
146 | x' <- {-trace ("loading " ++ fname) $-} do | 146 | x' <- {-trace ("loading " ++ fname) $-} do |
147 | env <- joinPolyEnvs False ms | 147 | env <- joinPolyEnvs False ms |
148 | x <- MMT $ lift $ mapExceptT (lift . mapWriterT (return . runIdentity)) $ inference_ env e | 148 | x <- MMT $ lift $ mapExceptT (lift . mapWriterT (return . runIdentity)) $ inference_ env e src |
149 | case moduleExports e of | 149 | case moduleExports e of |
150 | Nothing -> return x | 150 | Nothing -> return x |
151 | Just es -> joinPolyEnvs False $ flip map es $ \exp -> case exp of | 151 | Just es -> joinPolyEnvs False $ flip map es $ \exp -> case exp of |
diff --git a/src/LambdaCube/Compiler/Infer.hs b/src/LambdaCube/Compiler/Infer.hs index 3bbe1a3c..181a686b 100644 --- a/src/LambdaCube/Compiler/Infer.hs +++ b/src/LambdaCube/Compiler/Infer.hs | |||
@@ -51,7 +51,7 @@ import LambdaCube.Compiler.Parser | |||
51 | data Exp | 51 | data Exp |
52 | = TType | 52 | = TType |
53 | | ELit Lit | 53 | | ELit Lit |
54 | | Con_ MaxDB ConName !Int [Exp] | 54 | | Con_ MaxDB ConName !Int{-number of ereased arguments applied-} [Exp] |
55 | | TyCon_ MaxDB TyConName [Exp] | 55 | | TyCon_ MaxDB TyConName [Exp] |
56 | | Pi_ MaxDB Visibility Exp Exp | 56 | | Pi_ MaxDB Visibility Exp Exp |
57 | | Lam_ MaxDB Exp | 57 | | Lam_ MaxDB Exp |
@@ -61,16 +61,14 @@ data Exp | |||
61 | 61 | ||
62 | pattern FixLabel f xs e <- FixLabel_ f xs e _ where FixLabel f xs e = {-trace_ ("fixl: " ++ ppShow e ++ " " ++ ppShow xs) $ -} let x = FixLabel_ f [] e (subst 0 x e) in foldl app_ x xs | 62 | pattern FixLabel f xs e <- FixLabel_ f xs e _ where FixLabel f xs e = {-trace_ ("fixl: " ++ ppShow e ++ " " ++ ppShow xs) $ -} let x = FixLabel_ f [] e (subst 0 x e) in foldl app_ x xs |
63 | 63 | ||
64 | --app_ (FixLabel_ f xs e u) a = FixLabel_ f (xs ++ [a]) e (app_ u a) | ||
65 | |||
66 | data Neutral | 64 | data Neutral |
67 | = Fun_ MaxDB FunName !Int{-number of missing parameters-} [Exp]{-given parameters-} Neutral{-unfolded expression-} | 65 | = Fun_ MaxDB FunName !Int{-number of missing parameters-} [Exp]{-given parameters-} Neutral{-unfolded expression-}{-not neut?-} |
68 | | CaseFun__ MaxDB CaseFunName [Exp] Neutral | 66 | | CaseFun__ MaxDB CaseFunName [Exp] Neutral |
69 | | TyCaseFun__ MaxDB TyCaseFunName [Exp] Neutral | 67 | | TyCaseFun__ MaxDB TyCaseFunName [Exp] Neutral |
70 | | App__ MaxDB Neutral Exp | 68 | | App__ MaxDB Neutral Exp |
71 | | Var_ !Int -- De Bruijn variable | 69 | | Var_ !Int -- De Bruijn variable |
72 | | LabelEnd_ Exp | 70 | | LabelEnd_ Exp -- not neut? |
73 | | Delta (SData ([Exp] -> Exp)) | 71 | | Delta (SData ([Exp] -> Exp)) -- not neut? |
74 | deriving (Show) | 72 | deriving (Show) |
75 | 73 | ||
76 | data ConName = ConName SName Int{-ordinal number, e.g. Zero:0, Succ:1-} Type | 74 | data ConName = ConName SName Int{-ordinal number, e.g. Zero:0, Succ:1-} Type |
@@ -250,11 +248,13 @@ trueExp = EBool True | |||
250 | pattern LabelEnd x = Neut (LabelEnd_ x) | 248 | pattern LabelEnd x = Neut (LabelEnd_ x) |
251 | 249 | ||
252 | pmLabel' :: FunName -> Int -> [Exp] -> Exp -> Exp | 250 | pmLabel' :: FunName -> Int -> [Exp] -> Exp -> Exp |
253 | pmLabel' _ 0 _ (unfixlabel -> LabelEnd y) = y | ||
254 | pmLabel' (FunName_ _ _) 0 as (Neut (Delta (SData f))) = f as | 251 | pmLabel' (FunName_ _ _) 0 as (Neut (Delta (SData f))) = f as |
252 | pmLabel' f 0 xs (unfixlabel -> LabelEnd y) = y--FL f xs y | ||
255 | pmLabel' f i xs (unfixlabel -> Neut y) = Neut $ Fun f i xs y | 253 | pmLabel' f i xs (unfixlabel -> Neut y) = Neut $ Fun f i xs y |
256 | pmLabel' f i xs y = error $ "pmLabel: " ++ show (f, i, length xs, y) | 254 | pmLabel' f i xs y = error $ "pmLabel: " ++ show (f, i, length xs, y) |
257 | 255 | ||
256 | addFixLabel x y z = FixLabel x y z | ||
257 | |||
258 | pmLabel :: FunName -> Int -> [Exp] -> Exp -> Exp | 258 | pmLabel :: FunName -> Int -> [Exp] -> Exp -> Exp |
259 | pmLabel f i xs e = pmLabel' f (i + numLams e) xs (Neut $ dropLams e) | 259 | pmLabel f i xs e = pmLabel' f (i + numLams e) xs (Neut $ dropLams e) |
260 | 260 | ||
@@ -264,6 +264,9 @@ dropLams (unfixlabel -> Neut x) = x | |||
264 | numLams (unfixlabel -> Lam x) = 1 + numLams x | 264 | numLams (unfixlabel -> Lam x) = 1 + numLams x |
265 | numLams x = 0 | 265 | numLams x = 0 |
266 | 266 | ||
267 | pattern FL f xs y = Neut (Fun f 0 xs ({-unfixlabel -> -} LabelEnd_ y)) | ||
268 | |||
269 | unfixlabel (FL _ _ y) = y | ||
267 | unfixlabel (FixLabel_ _ _ _ a) = unfixlabel a | 270 | unfixlabel (FixLabel_ _ _ _ a) = unfixlabel a |
268 | unfixlabel a = a | 271 | unfixlabel a = a |
269 | 272 | ||
@@ -281,6 +284,9 @@ down t x | used t x = Nothing | |||
281 | | otherwise = Just $ subst t (error "impossible: down" :: Exp) x | 284 | | otherwise = Just $ subst t (error "impossible: down" :: Exp) x |
282 | 285 | ||
283 | instance Eq Exp where | 286 | instance Eq Exp where |
287 | FL f xs _ == FL f' xs' _ = (f, xs) == (f', xs') | ||
288 | FL _ _ a == a' = a == a' | ||
289 | a == FL _ _ a' = a == a' | ||
284 | FixLabel_ _ a f _ == FixLabel_ _ a' f' _ = (f, a) == (f', a') | 290 | FixLabel_ _ a f _ == FixLabel_ _ a' f' _ = (f, a) == (f', a') |
285 | FixLabel_ _ _ _ a == a' = a == a' | 291 | FixLabel_ _ _ _ a == a' = a == a' |
286 | a == FixLabel_ _ _ _ a' = a == a' | 292 | a == FixLabel_ _ _ _ a' = a == a' |
@@ -442,11 +448,13 @@ evalCaseFun a ps (Con n@(ConName _ i _) _ vs) | |||
442 | xs !!! i = xs !! i | 448 | xs !!! i = xs !! i |
443 | 449 | ||
444 | evalCaseFun a b (Neut c) = CaseFun a b c | 450 | evalCaseFun a b (Neut c) = CaseFun a b c |
451 | evalCaseFun a b (FL _ _ c) = evalCaseFun a b c | ||
445 | evalCaseFun a b (FixLabel_ _ _ _ c) = evalCaseFun a b c | 452 | evalCaseFun a b (FixLabel_ _ _ _ c) = evalCaseFun a b c |
446 | evalCaseFun a b x = error $ "evalCaseFun: " ++ show (a, x) | 453 | evalCaseFun a b x = error $ "evalCaseFun: " ++ show (a, x) |
447 | 454 | ||
448 | evalTyCaseFun a b (Neut c) = TyCaseFun a b c | 455 | evalTyCaseFun a b (Neut c) = TyCaseFun a b c |
449 | evalTyCaseFun a b (FixLabel_ _ _ _ c) = evalTyCaseFun a b c | 456 | evalTyCaseFun a b (FixLabel_ _ _ _ c) = evalTyCaseFun a b c |
457 | evalTyCaseFun a b (FL _ _ c) = evalTyCaseFun a b c | ||
450 | evalTyCaseFun (TyCaseFunName "match'Type" ty) [_, t, f] TType = t | 458 | evalTyCaseFun (TyCaseFunName "match'Type" ty) [_, t, f] TType = t |
451 | evalTyCaseFun (TyCaseFunName n ty) [_, t, f] (TyCon (TyConName n' _ _ _ _) vs) | n == n' = foldl app_ t vs | 459 | evalTyCaseFun (TyCaseFunName n ty) [_, t, f] (TyCon (TyConName n' _ _ _ _) vs) | n == n' = foldl app_ t vs |
452 | --evalTyCaseFun (TyCaseFunName n ty) [_, t, f] (DFun (FunName n' _) vs) | n == n' = foldl app_ t vs -- hack | 460 | --evalTyCaseFun (TyCaseFunName n ty) [_, t, f] (DFun (FunName n' _) vs) | n == n' = foldl app_ t vs -- hack |
@@ -525,6 +533,8 @@ cstr = f [] | |||
525 | f ns typ a (LabelEnd a') = f ns typ a a' | 533 | f ns typ a (LabelEnd a') = f ns typ a a' |
526 | f ns typ (FixLabel_ _ _ _ a) a' = f ns typ a a' | 534 | f ns typ (FixLabel_ _ _ _ a) a' = f ns typ a a' |
527 | f ns typ a (FixLabel_ _ _ _ a') = f ns typ a a' | 535 | f ns typ a (FixLabel_ _ _ _ a') = f ns typ a a' |
536 | f ns typ (FL _ _ a) a' = f ns typ a a' | ||
537 | f ns typ a (FL _ _ a') = f ns typ a a' | ||
528 | f ns typ (Con a n xs) (Con a' n' xs') | a == a' && n == n' && length xs == length xs' = | 538 | f ns typ (Con a n xs) (Con a' n' xs') | a == a' && n == n' && length xs == length xs' = |
529 | if null xs then Unit else ff ns (foldl appTy (conType typ a) $ mkConPars n typ) $ zip xs xs' | 539 | if null xs then Unit else ff ns (foldl appTy (conType typ a) $ mkConPars n typ) $ zip xs xs' |
530 | f ns typ (TyCon a xs) (TyCon a' xs') | a == a' && length xs == length xs' = | 540 | f ns typ (TyCon a xs) (TyCon a' xs') | a == a' && length xs == length xs' = |
@@ -675,7 +685,7 @@ data Env | |||
675 | | EApp2 SI Visibility ExpType Env | 685 | | EApp2 SI Visibility ExpType Env |
676 | | ELet1 LI Env SExp2 | 686 | | ELet1 LI Env SExp2 |
677 | | ELet2 LI ExpType Env | 687 | | ELet2 LI ExpType Env |
678 | | EGlobal String{-full source of current module-} GlobalEnv [Stmt] | 688 | | EGlobal |
679 | | ELabelEnd Env | 689 | | ELabelEnd Env |
680 | 690 | ||
681 | | EAssign Int ExpType Env | 691 | | EAssign Int ExpType Env |
@@ -701,7 +711,7 @@ parent = \case | |||
701 | -- CheckSame _ x -> Right x | 711 | -- CheckSame _ x -> Right x |
702 | CheckAppType _ _ _ x _ -> Right x | 712 | CheckAppType _ _ _ x _ -> Right x |
703 | ELabelEnd x -> Right x | 713 | ELabelEnd x -> Right x |
704 | EGlobal s x _ -> Left (s, x) | 714 | EGlobal -> Left () |
705 | 715 | ||
706 | -------------------------------------------------------------------------------- simple typing | 716 | -------------------------------------------------------------------------------- simple typing |
707 | 717 | ||
@@ -742,9 +752,8 @@ appTy t x = error $ "appTy: " ++ show t | |||
742 | 752 | ||
743 | -------------------------------------------------------------------------------- inference | 753 | -------------------------------------------------------------------------------- inference |
744 | 754 | ||
745 | type TCM m = ExceptT String (WriterT Infos m) | 755 | -- inference monad |
746 | 756 | type IM m = ExceptT String (ReaderT (Extensions, String{-full source-}, GlobalEnv) (WriterT Infos m)) | |
747 | --runTCM = either error id . runExcept | ||
748 | 757 | ||
749 | expAndType s (e, t, si) = (e, t) | 758 | expAndType s (e, t, si) = (e, t) |
750 | 759 | ||
@@ -754,21 +763,24 @@ lookupName s m = expAndType s <$> Map.lookup s m | |||
754 | --elemIndex' s@('\'':s') m = elemIndex s m `mplus` elemIndex s' m | 763 | --elemIndex' s@('\'':s') m = elemIndex s m `mplus` elemIndex s' m |
755 | --elemIndex' s m = elemIndex s m | 764 | --elemIndex' s m = elemIndex s m |
756 | 765 | ||
757 | getDef te si s = maybe (throwError $ "can't find: " ++ s ++ " in " ++ showSI te si {- ++ "\nitems:\n" ++ intercalate ", " (take' "..." 10 $ Map.keys $ snd $ extractEnv te)-}) return (lookupName s $ snd $ extractEnv te) | 766 | getSource = asks $ \(_, s, _) -> s |
767 | |||
768 | getDef te si s = do | ||
769 | src <- getSource | ||
770 | nv <- asks $ \(_, _, s) -> s | ||
771 | maybe (throwError $ "can't find: " ++ s ++ " in " ++ showSI_ src si {- ++ "\nitems:\n" ++ intercalate ", " (take' "..." 10 $ Map.keys $ snd $ extractEnv te)-}) return (lookupName s nv) | ||
758 | {- | 772 | {- |
759 | take' e n xs = case splitAt n xs of | 773 | take' e n xs = case splitAt n xs of |
760 | (as, []) -> as | 774 | (as, []) -> as |
761 | (as, _) -> as ++ [e] | 775 | (as, _) -> as ++ [e] |
762 | -} | 776 | -} |
763 | showSI :: Env -> SI -> String | ||
764 | showSI e = showSI_ (fst $ extractEnv e) | ||
765 | 777 | ||
766 | type ExpType' = CEnv ExpType | 778 | type ExpType' = CEnv ExpType |
767 | 779 | ||
768 | inferN :: forall m . Monad m => TraceLevel -> Env -> SExp2 -> TCM m ExpType' | 780 | inferN :: forall m . Monad m => TraceLevel -> Env -> SExp2 -> IM m ExpType' |
769 | inferN tracelevel = infer where | 781 | inferN tracelevel = infer where |
770 | 782 | ||
771 | infer :: Env -> SExp2 -> TCM m ExpType' | 783 | infer :: Env -> SExp2 -> IM m ExpType' |
772 | infer te exp = (if tracelevel >= 1 then trace_ ("infer: " ++ showEnvSExp te exp) else id) $ (if debug then fmap (fmap{-todo-} $ recheck' "infer" te) else id) $ case exp of | 784 | infer te exp = (if tracelevel >= 1 then trace_ ("infer: " ++ showEnvSExp te exp) else id) $ (if debug then fmap (fmap{-todo-} $ recheck' "infer" te) else id) $ case exp of |
773 | SAnn x t -> checkN (CheckIType x te) t TType | 785 | SAnn x t -> checkN (CheckIType x te) t TType |
774 | SLabelEnd x -> infer (ELabelEnd te) x | 786 | SLabelEnd x -> infer (ELabelEnd te) x |
@@ -780,7 +792,7 @@ inferN tracelevel = infer where | |||
780 | SLet le a b -> infer (ELet1 le te b{-in-}) a{-let-} -- infer te SLamV b `SAppV` a) | 792 | SLet le a b -> infer (ELet1 le te b{-in-}) a{-let-} -- infer te SLamV b `SAppV` a) |
781 | 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 | 793 | 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 |
782 | 794 | ||
783 | checkN :: Env -> SExp2 -> Type -> TCM m ExpType' | 795 | checkN :: Env -> SExp2 -> Type -> IM m ExpType' |
784 | checkN te x t = (if tracelevel >= 1 then trace_ $ "check: " ++ showEnvSExpType te x t else id) $ checkN_ te x t | 796 | checkN te x t = (if tracelevel >= 1 then trace_ $ "check: " ++ showEnvSExpType te x t else id) $ checkN_ te x t |
785 | 797 | ||
786 | checkN_ te e t | 798 | checkN_ te e t |
@@ -800,18 +812,24 @@ inferN tracelevel = infer where | |||
800 | | SLabelEnd x <- e = checkN (ELabelEnd te) x t | 812 | | SLabelEnd x <- e = checkN (ELabelEnd te) x t |
801 | | SApp si h a b <- e = infer (CheckAppType si h t te b) a | 813 | | SApp si h a b <- e = infer (CheckAppType si h t te b) a |
802 | | SLam h a b <- e, Pi h' x y <- t, h == h' = do | 814 | | SLam h a b <- e, Pi h' x y <- t, h == h' = do |
803 | tellType te e t | 815 | tellType e t |
804 | let same = checkSame te a x | 816 | let same = checkSame te a x |
805 | if same then checkN (EBind2 (BLam h) x te) b y else error $ "checkSame:\n" ++ show a ++ "\nwith\n" ++ showEnvExp te (x, TType) | 817 | if same then checkN (EBind2 (BLam h) x te) b y else error $ "checkSame:\n" ++ show a ++ "\nwith\n" ++ showEnvExp te (x, TType) |
806 | | Pi Hidden a b <- t, notHiddenLam e = checkN (EBind2 (BLam Hidden) a te) (up1 e) b | 818 | | Pi Hidden a b <- t = do |
819 | bb <- notHiddenLam e | ||
820 | if bb then checkN (EBind2 (BLam Hidden) a te) (up1 e) b | ||
821 | else infer (CheckType_ (sourceInfo e) t te) e | ||
807 | | otherwise = infer (CheckType_ (sourceInfo e) t te) e | 822 | | otherwise = infer (CheckType_ (sourceInfo e) t te) e |
808 | where | 823 | where |
809 | -- todo | 824 | -- todo |
810 | notHiddenLam = \case | 825 | notHiddenLam = \case |
811 | SLam Visible _ _ -> True | 826 | SLam Visible _ _ -> return True |
812 | SGlobal (si,s) | (Lam _, Pi Hidden _ _) <- fromMaybe (error $ "infer: can't find: " ++ s) $ lookupName s $ snd $ extractEnv te -> False | 827 | SGlobal (si,s) -> do |
813 | | otherwise -> True | 828 | nv <- asks $ \(_,_,s) -> s |
814 | _ -> False | 829 | case fromMaybe (error $ "infer: can't find: " ++ s) $ lookupName s nv of |
830 | (Lam _, Pi Hidden _ _) -> return False | ||
831 | _ -> return True | ||
832 | _ -> return False | ||
815 | {- | 833 | {- |
816 | -- todo | 834 | -- todo |
817 | checkSame te (Wildcard _) a = return (te, True) | 835 | checkSame te (Wildcard _) a = return (te, True) |
@@ -828,9 +846,9 @@ inferN tracelevel = infer where | |||
828 | hArgs (Pi Hidden _ b) = 1 + hArgs b | 846 | hArgs (Pi Hidden _ b) = 1 + hArgs b |
829 | hArgs _ = 0 | 847 | hArgs _ = 0 |
830 | 848 | ||
831 | focus_' env si eet = tellType env si (snd eet) >> focus_ env eet | 849 | focus_' env si eet = tellType si (snd eet) >> focus_ env eet |
832 | 850 | ||
833 | focus_ :: Env -> ExpType -> TCM m ExpType' | 851 | focus_ :: Env -> ExpType -> IM m ExpType' |
834 | focus_ env eet@(e, et) = (if tracelevel >= 1 then trace_ $ "focus: " ++ showEnvExp env eet else id) $ (if debug then fmap (fmap{-todo-} $ recheck' "focus" env) else id) $ case env of | 852 | focus_ env eet@(e, et) = (if tracelevel >= 1 then trace_ $ "focus: " ++ showEnvExp env eet else id) $ (if debug then fmap (fmap{-todo-} $ recheck' "focus" env) else id) $ case env of |
835 | ELabelEnd te -> focus_ te (LabelEnd e, et) | 853 | ELabelEnd te -> focus_ te (LabelEnd e, et) |
836 | -- CheckSame x te -> focus_ (EBind2_ (debugSI "focus_ CheckSame") BMeta (cstr x e) te) $ up 1 eet | 854 | -- CheckSame x te -> focus_ (EBind2_ (debugSI "focus_ CheckSame") BMeta (cstr x e) te) $ up 1 eet |
@@ -861,12 +879,12 @@ inferN tracelevel = infer where | |||
861 | EBind2_ si (BPi h) a te -> focus_' te si (Pi h a e, TType) | 879 | EBind2_ si (BPi h) a te -> focus_' te si (Pi h a e, TType) |
862 | _ -> focus2 env $ MEnd eet | 880 | _ -> focus2 env $ MEnd eet |
863 | 881 | ||
864 | focus2 :: Env -> CEnv ExpType -> TCM m ExpType' | 882 | focus2 :: Env -> CEnv ExpType -> IM m ExpType' |
865 | focus2 env eet = case env of | 883 | focus2 env eet = case env of |
866 | ELet1 le te b{-in-} -> infer (ELet2 le (replaceMetas' eet{-let-}) te) b{-in-} | 884 | ELet1 le te b{-in-} -> infer (ELet2 le (replaceMetas' eet{-let-}) te) b{-in-} |
867 | EBind2_ si BMeta tt te | 885 | EBind2_ si BMeta tt te |
868 | | Unit <- tt -> refocus te $ subst 0 TT eet | 886 | | Unit <- tt -> refocus te $ subst 0 TT eet |
869 | | Empty msg <- tt -> throwError $ "type error: " ++ msg ++ "\nin " ++ showSI te si ++ "\n"-- todo: better error msg | 887 | | Empty msg <- tt -> getSource >>= \src -> throwError $ "type error: " ++ msg ++ "\nin " ++ showSI_ src si ++ "\n"-- todo: better error msg |
870 | | T2 x y <- tt, let te' = EBind2_ si BMeta (up 1 y) $ EBind2_ si BMeta x te | 888 | | T2 x y <- tt, let te' = EBind2_ si BMeta (up 1 y) $ EBind2_ si BMeta x te |
871 | -> refocus te' $ subst 2 (t2C (Var 1) (Var 0)) $ up 2 eet | 889 | -> refocus te' $ subst 2 (t2C (Var 1) (Var 0)) $ up 2 eet |
872 | | CstrT t a b <- tt, Just r <- cst (a, t) b -> r | 890 | | CstrT t a b <- tt, Just r <- cst (a, t) b -> r |
@@ -889,7 +907,7 @@ inferN tracelevel = infer where | |||
889 | | otherwise -> focus2 te $ Meta tt eet | 907 | | otherwise -> focus2 te $ Meta tt eet |
890 | where | 908 | where |
891 | refocus = refocus_ focus2 | 909 | refocus = refocus_ focus2 |
892 | cst :: ExpType -> Exp -> Maybe (TCM m ExpType') | 910 | cst :: ExpType -> Exp -> Maybe (IM m ExpType') |
893 | cst x = \case | 911 | cst x = \case |
894 | Var i | fst (varType "X" i te) == BMeta | 912 | Var i | fst (varType "X" i te) == BMeta |
895 | , Just y <- down i x | 913 | , Just y <- down i x |
@@ -926,7 +944,7 @@ inferN tracelevel = infer where | |||
926 | MEnd x -> throwError_ $ "focus todo: " ++ ppShow x | 944 | MEnd x -> throwError_ $ "focus todo: " ++ ppShow x |
927 | _ -> throwError_ $ "focus checkMetas: " ++ ppShow env ++ "\n" ++ ppShow (fst <$> eet) | 945 | _ -> throwError_ $ "focus checkMetas: " ++ ppShow env ++ "\n" ++ ppShow (fst <$> eet) |
928 | where | 946 | where |
929 | refocus_ :: (Env -> CEnv ExpType -> TCM m ExpType') -> Env -> CEnv ExpType -> TCM m ExpType' | 947 | refocus_ :: (Env -> CEnv ExpType -> IM m ExpType') -> Env -> CEnv ExpType -> IM m ExpType' |
930 | refocus_ _ e (MEnd at) = focus_ e at | 948 | refocus_ _ e (MEnd at) = focus_ e at |
931 | refocus_ f e (Meta x at) = f (EBind2 BMeta x e) at | 949 | refocus_ f e (Meta x at) = f (EBind2 BMeta x e) at |
932 | refocus_ _ e (Assign i x at) = focus2 (EAssign i x e) at | 950 | refocus_ _ e (Assign i x at) = focus2 (EAssign i x e) at |
@@ -1053,12 +1071,6 @@ dependentVars ie = cycle mempty | |||
1053 | 1071 | ||
1054 | type GlobalEnv = Map.Map SName (Exp, Type, (SI, MFixity)) | 1072 | type GlobalEnv = Map.Map SName (Exp, Type, (SI, MFixity)) |
1055 | 1073 | ||
1056 | -- monad used during elaborating statments -- TODO: use zippers instead | ||
1057 | type ElabStmtM m = ReaderT (Extensions, String{-full source-}) (StateT GlobalEnv (ExceptT String (WriterT Infos m))) | ||
1058 | |||
1059 | extractEnv :: Env -> (String, GlobalEnv) | ||
1060 | extractEnv = either id extractEnv . parent | ||
1061 | |||
1062 | initEnv :: GlobalEnv | 1074 | initEnv :: GlobalEnv |
1063 | initEnv = Map.fromList | 1075 | initEnv = Map.fromList |
1064 | [ (,) "'Type" (TType, TType, (debugSI "source-of-Type", Nothing)) | 1076 | [ (,) "'Type" (TType, TType, (debugSI "source-of-Type", Nothing)) |
@@ -1096,7 +1108,7 @@ listInfos (Infos m) = [(r, Set.toList i) | (r, i) <- Map.toList m] | |||
1096 | 1108 | ||
1097 | -------------------------------------------------------------------------------- inference for statements | 1109 | -------------------------------------------------------------------------------- inference for statements |
1098 | 1110 | ||
1099 | handleStmt :: MonadFix m => [Stmt] -> Stmt -> ElabStmtM m () | 1111 | handleStmt :: MonadFix m => [Stmt] -> Stmt -> IM m GlobalEnv |
1100 | handleStmt defs = \case | 1112 | handleStmt defs = \case |
1101 | Primitive n mf (trSExp' -> t_) -> do | 1113 | Primitive n mf (trSExp' -> t_) -> do |
1102 | t <- inferType tr =<< ($ t_) <$> addF | 1114 | t <- inferType tr =<< ($ t_) <$> addF |
@@ -1105,7 +1117,7 @@ handleStmt defs = \case | |||
1105 | Let n mf mt t_ -> do | 1117 | Let n mf mt t_ -> do |
1106 | af <- addF | 1118 | af <- addF |
1107 | let t__ = maybe id (flip SAnn . af) mt t_ | 1119 | let t__ = maybe id (flip SAnn . af) mt t_ |
1108 | (x, t) <- inferTerm (snd n) tr id $ trSExp' $ if usedS n t__ then SBuiltin "primFix" `SAppV` SLamV (substSG0 n t__) else t__ | 1120 | (x, t) <- inferTerm (snd n) tr $ trSExp' $ if usedS n t__ then SBuiltin "primFix" `SAppV` SLamV (substSG0 n t__) else t__ |
1109 | tellStmtType (fst n) t | 1121 | tellStmtType (fst n) t |
1110 | addToEnv n mf (mkELet (True, n) x t, t) | 1122 | addToEnv n mf (mkELet (True, n) x t, t) |
1111 | {- -- hack | 1123 | {- -- hack |
@@ -1118,10 +1130,9 @@ handleStmt defs = \case | |||
1118 | :~> Var 3 `app_` Var 1 | 1130 | :~> Var 3 `app_` Var 1 |
1119 | addToEnv (fst n, MatchName (snd n)) (lamify t'' $ \[m, tr, n', f] -> evalTyCaseFun (TyCaseFunName (snd n) t) [m, tr, f] n', t'') | 1131 | addToEnv (fst n, MatchName (snd n)) (lamify t'' $ \[m, tr, n', f] -> evalTyCaseFun (TyCaseFunName (snd n) t) [m, tr, f] n', t'') |
1120 | -} | 1132 | -} |
1121 | PrecDef{} -> return () | 1133 | PrecDef{} -> return mempty |
1122 | Data s (map (second trSExp') -> ps) (trSExp' -> t_) addfa (map (second trSExp') -> cs) -> do | 1134 | Data s (map (second trSExp') -> ps) (trSExp' -> t_) addfa (map (second trSExp') -> cs) -> do |
1123 | exs <- asks fst | 1135 | af <- if addfa then asks $ \(exs, _, ge) -> addForalls exs . (snd s:) . defined' $ ge else return id |
1124 | af <- if addfa then gets $ addForalls exs . (snd s:) . defined' else return id | ||
1125 | vty <- inferType tr $ addParamsS ps t_ | 1136 | vty <- inferType tr $ addParamsS ps t_ |
1126 | tellStmtType (fst s) vty | 1137 | tellStmtType (fst s) vty |
1127 | let | 1138 | let |
@@ -1129,7 +1140,7 @@ handleStmt defs = \case | |||
1129 | inum = arity vty - length ps | 1140 | inum = arity vty - length ps |
1130 | 1141 | ||
1131 | mkConstr j (cn, af -> ct) | 1142 | mkConstr j (cn, af -> ct) |
1132 | | c == SGlobal s && take pnum' xs == downToS (length . fst . getParamsS $ ct) pnum' | 1143 | | c == SGlobal s && take pnum' xs == downToS "a3" (length . fst . getParamsS $ ct) pnum' |
1133 | = do | 1144 | = do |
1134 | cty <- removeHiddenUnit <$> inferType tr (addParamsS [(Hidden, x) | (Visible, x) <- ps] ct) | 1145 | cty <- removeHiddenUnit <$> inferType tr (addParamsS [(Hidden, x) | (Visible, x) <- ps] ct) |
1135 | tellStmtType (fst cn) cty | 1146 | tellStmtType (fst cn) cty |
@@ -1137,47 +1148,52 @@ handleStmt defs = \case | |||
1137 | act = length . fst . getParams $ cty | 1148 | act = length . fst . getParams $ cty |
1138 | acts = map fst . fst . getParams $ cty | 1149 | acts = map fst . fst . getParams $ cty |
1139 | conn = ConName (snd cn) j cty | 1150 | conn = ConName (snd cn) j cty |
1140 | addToEnv cn (listToMaybe [f | PrecDef n f <- defs, n == cn]) (Con conn 0 [], cty) | 1151 | e <- addToEnv cn (listToMaybe [f | PrecDef n f <- defs, n == cn]) (Con conn 0 [], cty) |
1141 | return ( (conn, cty) | 1152 | return (e, ((conn, cty) |
1142 | , addParamsS pars | 1153 | , addParamsS pars |
1143 | $ foldl SAppV (SVar (debugSI "22", ".cs") $ j + length pars) $ drop pnum' xs ++ [apps' (SGlobal cn) (zip acts $ downToS (j+1+length pars) (length ps) ++ downToS 0 (act- length ps))] | 1154 | $ foldl SAppV (SVar (debugSI "22", ".cs") $ j + length pars) $ drop pnum' xs ++ [apps' (SGlobal cn) (zip acts $ downToS ("a4 " ++ snd cn ++ " " ++ show (length ps)) (j+1+length pars) (length ps) ++ downToS "a5" 0 (act- length ps))] |
1144 | ) | 1155 | )) |
1145 | | otherwise = throwError "illegal data definition (parameters are not uniform)" -- ++ show (c, cn, take pnum' xs, act) | 1156 | | otherwise = throwError "illegal data definition (parameters are not uniform)" -- ++ show (c, cn, take pnum' xs, act) |
1146 | where | 1157 | where |
1147 | (c, map snd -> xs) = getApps $ snd $ getParamsS ct | 1158 | (c, map snd -> xs) = getApps $ snd $ getParamsS ct |
1148 | 1159 | ||
1149 | motive = addParamsS (replicate inum (Visible, Wildcard SType)) $ | 1160 | motive = addParamsS (replicate inum (Visible, Wildcard SType)) $ |
1150 | SPi Visible (apps' (SGlobal s) $ zip (map fst ps) (downToS inum $ length ps) ++ zip (map fst $ fst $ getParamsS t_) (downToS 0 inum)) SType | 1161 | SPi Visible (apps' (SGlobal s) $ zip (map fst ps) (downToS "a6" inum $ length ps) ++ zip (map fst $ fst $ getParamsS t_) (downToS "a7" 0 inum)) SType |
1151 | 1162 | ||
1152 | mdo | 1163 | (e1, es, tcn, cfn@(CaseFunName _ ct _), _, _) <- mfix $ \ ~(_, _, _, _, ct', cons') -> do |
1153 | let tcn = TyConName (snd s) inum vty (map fst cons) cfn | 1164 | let cfn = CaseFunName (snd s) ct' $ length ps |
1154 | let cfn = CaseFunName (snd s) ct $ length ps | 1165 | let tcn = TyConName (snd s) inum vty (map fst cons') cfn |
1155 | addToEnv s (listToMaybe [f | PrecDef n f <- defs, n == s]) (TyCon tcn [], vty) | 1166 | e1 <- addToEnv s (listToMaybe [f | PrecDef n f <- defs, n == s]) (TyCon tcn [], vty) |
1156 | cons <- zipWithM mkConstr [0..] cs | 1167 | (unzip -> (mconcat -> es, cons)) <- withEnv e1 $ zipWithM mkConstr [0..] cs |
1157 | ct <- inferType tr | 1168 | ct <- withEnv (e1 <> es) $ inferType tr |
1158 | ( (\x -> traceD ("type of case-elim before elaboration: " ++ ppShow x) x) $ addParamsS | 1169 | ( (\x -> traceD ("type of case-elim before elaboration: " ++ ppShow x) x) $ addParamsS |
1159 | ( [(Hidden, x) | (_, x) <- ps] | 1170 | ( [(Hidden, x) | (_, x) <- ps] |
1160 | ++ (Visible, motive) | 1171 | ++ (Visible, motive) |
1161 | : map ((,) Visible . snd) cons | 1172 | : map ((,) Visible . snd) cons |
1162 | ++ replicate inum (Hidden, Wildcard SType) | 1173 | ++ replicate inum (Hidden, Wildcard SType) |
1163 | ++ [(Visible, apps' (SGlobal s) $ zip (map fst ps) (downToS (inum + length cs + 1) $ length ps) ++ zip (map fst $ fst $ getParamsS t_) (downToS 0 inum))] | 1174 | ++ [(Visible, apps' (SGlobal s) $ zip (map fst ps) (downToS "a8" (inum + length cs + 1) $ length ps) ++ zip (map fst $ fst $ getParamsS t_) (downToS "a9" 0 inum))] |
1164 | ) | 1175 | ) |
1165 | $ foldl SAppV (SVar (debugSI "23", ".ct") $ length cs + inum + 1) $ downToS 1 inum ++ [SVar (debugSI "24", ".24") 0] | 1176 | $ foldl SAppV (SVar (debugSI "23", ".ct") $ length cs + inum + 1) $ downToS "a10" 1 inum ++ [SVar (debugSI "24", ".24") 0] |
1166 | ) | 1177 | ) |
1167 | addToEnv (fst s, caseName (snd s)) Nothing (lamify ct $ \xs -> evalCaseFun cfn (init $ drop (length ps) xs) (last xs), ct) | 1178 | return (e1, es, tcn, cfn, ct, cons) |
1168 | let ps' = fst $ getParams vty | 1179 | |
1169 | t = (TType :~> TType) | 1180 | e2 <- addToEnv (fst s, caseName (snd s)) Nothing (lamify ct $ \xs -> evalCaseFun cfn (init $ drop (length ps) xs) (last xs), ct) |
1170 | :~> addParams ps' (Var (length ps') `app_` TyCon tcn (downTo 0 $ length ps')) | 1181 | let ps' = fst $ getParams vty |
1171 | :~> TType | 1182 | t = (TType :~> TType) |
1172 | :~> Var 2 `app_` Var 0 | 1183 | :~> addParams ps' (Var (length ps') `app_` TyCon tcn (downTo 0 $ length ps')) |
1173 | :~> Var 3 `app_` Var 1 | 1184 | :~> TType |
1174 | addToEnv (fst s, MatchName (snd s)) Nothing (lamify t $ \[m, tr, n, f] -> evalTyCaseFun (TyCaseFunName (snd s) t) [m, tr, f] n, t) | 1185 | :~> Var 2 `app_` Var 0 |
1186 | :~> Var 3 `app_` Var 1 | ||
1187 | e3 <- addToEnv (fst s, MatchName (snd s)) Nothing (lamify t $ \[m, tr, n, f] -> evalTyCaseFun (TyCaseFunName (snd s) t) [m, tr, f] n, t) | ||
1188 | return (e1 <> e2 <> e3 <> es) | ||
1175 | 1189 | ||
1176 | stmt -> error $ "handleStmt: " ++ show stmt | 1190 | stmt -> error $ "handleStmt: " ++ show stmt |
1177 | 1191 | ||
1192 | withEnv e = local (\(a,b,c) -> (a,b,c <> e)) | ||
1193 | |||
1178 | mkELet (False, n) x xt = x | 1194 | mkELet (False, n) x xt = x |
1179 | mkELet (True, n) x t{-type of x-} | 1195 | mkELet (True, n) x t{-type of x-} |
1180 | | Just (t, f, i) <- getFix x 0 = fix $ \term -> pmLabel fn i [] $ Lam f `app_` FixLabel (nType fn) (downTo 0 i) term | 1196 | | Just (t, f, i) <- getFix x 0 = fix $ \term -> pmLabel fn i [] $ Lam f `app_` addFixLabel (nType fn) (downTo 0 i) term |
1181 | | otherwise = pmLabel fn 0 [] x | 1197 | | otherwise = pmLabel fn 0 [] x |
1182 | where | 1198 | where |
1183 | fn = FunName (snd n) t | 1199 | fn = FunName (snd n) t |
@@ -1212,33 +1228,36 @@ getParams x = ([], x) | |||
1212 | getLams (Lam b) = getLams b | 1228 | getLams (Lam b) = getLams b |
1213 | getLams x = x | 1229 | getLams x = x |
1214 | 1230 | ||
1215 | getGEnv f = do | 1231 | inferTerm :: Monad m => String -> Bool -> SExp2 -> IM m ExpType |
1216 | (exs, src) <- ask | 1232 | inferTerm msg tr t = ask >>= \(exs, _, _) -> smartTrace exs $ \tr -> |
1217 | gets (\ge -> EGlobal src ge mempty) >>= f | 1233 | fmap ((closedExp *** closedExp) . recheck msg EGlobal . replaceMetas (lamPi Hidden)) $ inferN (if tr then traceLevel exs else 0) EGlobal t |
1218 | inferTerm msg tr f t = asks fst >>= \exs -> getGEnv $ \env -> let env' = f env in smartTrace exs $ \tr -> | 1234 | inferType :: Monad m => Bool -> SExp2 -> IM m Type |
1219 | fmap ((closedExp *** closedExp) . recheck msg env' . replaceMetas (lamPi Hidden)) $ lift (lift $ inferN (if tr then traceLevel exs else 0) env' t) | 1235 | inferType tr t = ask >>= \(exs, _, _) -> fmap (closedExp . fst . recheck "inferType" EGlobal . flip (,) TType . replaceMetas (Pi Hidden) . fmap fst) $ inferN (if tr then traceLevel exs else 0) (CheckType_ (debugSI "inferType CheckType_") TType EGlobal) t |
1220 | inferType tr t = asks fst >>= \exs -> getGEnv $ \env -> fmap (closedExp . fst . recheck "inferType" env . flip (,) TType . replaceMetas (Pi Hidden) . fmap fst) $ lift (lift $ inferN (if tr then traceLevel exs else 0) (CheckType_ (debugSI "inferType CheckType_") TType env) t) | ||
1221 | 1236 | ||
1222 | addToEnv :: Monad m => SIName -> MFixity -> (Exp, Exp) -> ElabStmtM m () | 1237 | addToEnv :: Monad m => SIName -> MFixity -> ExpType -> IM m GlobalEnv |
1223 | addToEnv (si, s) mf (x, t) = do | 1238 | addToEnv (si, s) mf (x, t) = do |
1224 | -- maybe (pure ()) throwError_ $ ambiguityCheck s t -- TODO | 1239 | -- maybe (pure ()) throwError_ $ ambiguityCheck s t -- TODO |
1225 | exs <- asks fst | 1240 | exs <- asks $ \(exs, _, _) -> exs |
1226 | when (trLight exs) $ mtrace (s ++ " :: " ++ ppShow t) | 1241 | when (trLight exs) $ mtrace (s ++ " :: " ++ ppShow t) |
1227 | v <- gets $ Map.lookup s | 1242 | v <- asks $ \(_, _, ge) -> Map.lookup s ge |
1228 | case v of | 1243 | case v of |
1229 | Nothing -> modify $ Map.insert s (closedExp x, closedExp t, (si, mf)) | 1244 | Nothing -> return $ Map.singleton s (closedExp x, closedExp t, (si, mf)) |
1230 | Just (_, _, (si', _)) | 1245 | Just (_, _, (si', _)) |
1231 | | sameSource si si' -> getGEnv $ \ge -> throwError $ "already defined " ++ s ++ " at " ++ showSI ge si ++ "\n and at " ++ showSI ge si' | 1246 | | sameSource si si' -> getSource >>= \ge -> throwError $ "already defined " ++ s ++ " at " ++ showSI_ ge si ++ "\n and at " ++ showSI_ ge si' |
1232 | | otherwise -> getGEnv $ \ge -> throwError $ "already defined " ++ s ++ " at " ++ showSI ge si ++ "\n and at " ++ showSourcePosSI si' | 1247 | | otherwise -> getSource >>= \ge -> throwError $ "already defined " ++ s ++ " at " ++ showSI_ ge si ++ "\n and at " ++ showSourcePosSI si' |
1248 | {- | ||
1249 | joinEnv :: Monad m => GlobalEnv -> GlobalEnv -> IM m GlobalEnv | ||
1250 | joinEnv e1 e2 = do | ||
1251 | -} | ||
1233 | 1252 | ||
1234 | downTo n m = map Var [n+m-1, n+m-2..n] | 1253 | downTo n m = map Var [n+m-1, n+m-2..n] |
1235 | 1254 | ||
1236 | defined' = Map.keys | 1255 | defined' = Map.keys |
1237 | 1256 | ||
1238 | addF = asks fst >>= \exs -> gets $ addForalls exs . defined' | 1257 | addF = asks $ \(exs, _, ge) -> addForalls exs $ defined' ge |
1239 | 1258 | ||
1240 | tellType te si t = tell $ mkInfoItem (sourceInfo si) $ removeEscs $ showDoc $ mkDoc True (t, TType) | 1259 | tellType si t = tell $ mkInfoItem (sourceInfo si) $ removeEscs $ showDoc $ mkDoc True (t, TType) |
1241 | tellStmtType si t = getGEnv $ \te -> tellType te si t | 1260 | tellStmtType si t = tellType si t |
1242 | 1261 | ||
1243 | 1262 | ||
1244 | -------------------------------------------------------------------------------- inference output | 1263 | -------------------------------------------------------------------------------- inference output |
@@ -1398,17 +1417,34 @@ traceLevel exs = if TraceTypeCheck `elem` exs then 1 else 0 :: TraceLevel -- 0: | |||
1398 | tr = False --traceLevel >= 2 | 1417 | tr = False --traceLevel >= 2 |
1399 | trLight exs = traceLevel exs >= 1 | 1418 | trLight exs = traceLevel exs >= 1 |
1400 | 1419 | ||
1401 | inference_ :: PolyEnv -> Module -> ErrorT (WriterT Infos Identity) PolyEnv | 1420 | mfix' f = ExceptT (mfix (runExceptT . f . either bomb id)) |
1402 | inference_ (PolyEnv pe is) m = ff $ runWriter $ runExceptT $ mdo | 1421 | where bomb e = error $ "mfix (ExceptT): inner computation returned Left value:\n" ++ show e |
1403 | let (x, dns) = definitions m ds | 1422 | |
1404 | ds = mkDesugarInfo defs `joinDesugarInfo` extractDesugarInfo pe | 1423 | inference_ :: PolyEnv -> Module -> String -> ErrorT (WriterT Infos Identity) PolyEnv |
1405 | defs <- either (throwError . ErrorMsg) return x | 1424 | inference_ (PolyEnv pe is) m src = do |
1425 | |||
1426 | ((defs, dns), ds) <- mfix $ \ff -> do | ||
1427 | let ds = snd ff | ||
1428 | (x, dns) = definitions m ds | ||
1429 | defs <- either (throwError . ErrorMsg) return x | ||
1430 | let ds' = mkDesugarInfo defs `joinDesugarInfo` extractDesugarInfo pe | ||
1431 | return ((defs, dns), ds') | ||
1432 | |||
1406 | mapM_ (maybe (return ()) (throwErrorTCM . text)) dns | 1433 | mapM_ (maybe (return ()) (throwErrorTCM . text)) dns |
1407 | mapExceptT (fmap $ ErrorMsg +++ snd) . flip runStateT (initEnv <> pe) . flip runReaderT (extensions m, sourceCode m) . mapM_ (handleStmt defs) $ sortDefs ds defs | 1434 | mapExceptT (ff . runWriter . flip runReaderT (extensions m, src, mempty)) $ gg (handleStmt defs) (initEnv <> pe) $ sortDefs ds defs |
1435 | |||
1408 | where | 1436 | where |
1409 | ff (Left e, is) = throwError e | 1437 | ff (Left e, is) = do |
1410 | ff (Right ge, is) = do | ||
1411 | tell is | 1438 | tell is |
1412 | return $ PolyEnv ge is | 1439 | return $ Left $ ErrorMsg e |
1440 | ff (Right ge, is) = do | ||
1441 | return $ Right $ PolyEnv ge is | ||
1442 | |||
1443 | gg _ acc [] = return acc | ||
1444 | gg m acc (x:xs) = do | ||
1445 | y <- withEnv acc $ m x | ||
1446 | gg m (acc <> y) xs | ||
1447 | |||
1448 | |||
1413 | 1449 | ||
1414 | 1450 | ||
diff --git a/src/LambdaCube/Compiler/Parser.hs b/src/LambdaCube/Compiler/Parser.hs index 5c0c64b8..d643b746 100644 --- a/src/LambdaCube/Compiler/Parser.hs +++ b/src/LambdaCube/Compiler/Parser.hs | |||
@@ -162,7 +162,8 @@ getApps = second reverse . run where | |||
162 | run (SApp _ h a b) = second ((h, b):) $ run a | 162 | run (SApp _ h a b) = second ((h, b):) $ run a |
163 | run x = (x, []) | 163 | run x = (x, []) |
164 | 164 | ||
165 | downToS n m = map (SVar (debugSI "20", ".ds")) [n+m-1, n+m-2..n] | 165 | -- todo: remove |
166 | downToS err n m = [SVar (debugSI $ err ++ " " ++ show i, ".ds") (n + i) | i <- [m-1, m-2..0]] | ||
166 | 167 | ||
167 | instance SourceInfo (SExp' a) where | 168 | instance SourceInfo (SExp' a) where |
168 | sourceInfo = \case | 169 | sourceInfo = \case |
@@ -226,7 +227,7 @@ class Up a where | |||
226 | instance (Up a, Up b) => Up (a, b) where | 227 | instance (Up a, Up b) => Up (a, b) where |
227 | up_ n i (a, b) = (up_ n i a, up_ n i b) | 228 | up_ n i (a, b) = (up_ n i a, up_ n i b) |
228 | used i (a, b) = used i a || used i b | 229 | used i (a, b) = used i a || used i b |
229 | fold _ _ _ = error "fold @(_,_)" | 230 | fold f i (a, b) = fold f i a <> fold f i b |
230 | maxDB_ (a, b) = maxDB_ a <> maxDB_ b | 231 | maxDB_ (a, b) = maxDB_ a <> maxDB_ b |
231 | closedExp (a, b) = (closedExp a, closedExp b) | 232 | closedExp (a, b) = (closedExp a, closedExp b) |
232 | 233 | ||
@@ -287,7 +288,7 @@ instance Up Void where | |||
287 | 288 | ||
288 | instance Up a => Up (SExp' a) where | 289 | instance Up a => Up (SExp' a) where |
289 | up_ n = mapS' (\sn j i -> SVar sn $ if j < i then j else j+n) (+1) | 290 | up_ n = mapS' (\sn j i -> SVar sn $ if j < i then j else j+n) (+1) |
290 | fold f = foldS (\_ _ _ -> error "fold @SExp") mempty $ \sn j i -> f j i | 291 | fold f = foldS (\i si x -> fold f i x) mempty $ \sn j i -> f j i |
291 | maxDB_ _ = error "maxDB @SExp" | 292 | maxDB_ _ = error "maxDB @SExp" |
292 | 293 | ||
293 | dbf' = dbf_ 0 | 294 | dbf' = dbf_ 0 |
@@ -756,7 +757,7 @@ parseDef = | |||
756 | t <- dbf' npsd <$> parseType (Just SType) | 757 | t <- dbf' npsd <$> parseType (Just SType) |
757 | let mkConTy mk (nps', ts') = | 758 | let mkConTy mk (nps', ts') = |
758 | ( if mk then Just nps' else Nothing | 759 | ( if mk then Just nps' else Nothing |
759 | , foldr (uncurry SPi) (foldl SAppV (SGlobal x) $ downToS (length ts') $ length ts) ts') | 760 | , foldr (uncurry SPi) (foldl SAppV (SGlobal x) $ downToS "a1" (length ts') $ length ts) ts') |
760 | (af, cs) <- option (True, []) $ | 761 | (af, cs) <- option (True, []) $ |
761 | do fmap ((,) True) $ (reserved "where" >>) $ indentMS True $ second ((,) Nothing . dbf' npsd) <$> typedIds Nothing | 762 | do fmap ((,) True) $ (reserved "where" >>) $ indentMS True $ second ((,) Nothing . dbf' npsd) <$> typedIds Nothing |
762 | <|> (,) False <$ reservedOp "=" <*> | 763 | <|> (,) False <$ reservedOp "=" <*> |
@@ -949,7 +950,7 @@ compileFunAlts par ulend lend ds xs = dsInfo >>= \ge -> case xs of | |||
949 | ++ [ FunAlt n (replicate (length ps) (noTA $ PVar (debugSI "compileFunAlts1", "generated_name0"))) $ Right $ SBuiltin "'Empty" `SAppV` sLit (LString $ "no instance of " ++ snd n ++ " on ???")] | 950 | ++ [ FunAlt n (replicate (length ps) (noTA $ PVar (debugSI "compileFunAlts1", "generated_name0"))) $ Right $ SBuiltin "'Empty" `SAppV` sLit (LString $ "no instance of " ++ snd n ++ " on ???")] |
950 | cds <- sequence | 951 | cds <- sequence |
951 | [ compileFunAlts' SLabelEnd | 952 | [ compileFunAlts' SLabelEnd |
952 | $ TypeAnn m (addParamsS (map ((,) Hidden) ps) $ SPi Hidden (foldl SAppV (SGlobal n) $ downToS 0 $ length ps) $ up1 t) | 953 | $ TypeAnn m (addParamsS (map ((,) Hidden) ps) $ SPi Hidden (foldl SAppV (SGlobal n) $ downToS "a2" 0 $ length ps) $ up1 t) |
953 | : as | 954 | : as |
954 | | (m, t) <- ms | 955 | | (m, t) <- ms |
955 | -- , let ts = fst $ getParamsS $ up1 t | 956 | -- , let ts = fst $ getParamsS $ up1 t |
@@ -1054,7 +1055,6 @@ data Module | |||
1054 | , moduleImports :: [(SName, ImportItems)] | 1055 | , moduleImports :: [(SName, ImportItems)] |
1055 | , moduleExports :: Maybe [Export] | 1056 | , moduleExports :: Maybe [Export] |
1056 | , definitions :: DesugarInfo -> (Either String [Stmt], [PostponedCheck]) | 1057 | , definitions :: DesugarInfo -> (Either String [Stmt], [PostponedCheck]) |
1057 | , sourceCode :: String | ||
1058 | } | 1058 | } |
1059 | 1059 | ||
1060 | parseModule :: FilePath -> String -> P Module | 1060 | parseModule :: FilePath -> String -> P Module |
@@ -1085,7 +1085,6 @@ parseModule f str = do | |||
1085 | , moduleImports = [("Prelude", ImportAllBut []) | NoImplicitPrelude `notElem` exts] ++ idefs | 1085 | , moduleImports = [("Prelude", ImportAllBut []) | NoImplicitPrelude `notElem` exts] ++ idefs |
1086 | , moduleExports = join $ snd <$> header | 1086 | , moduleExports = join $ snd <$> header |
1087 | , definitions = \ge -> first ((show +++ id) . snd) $ runP' (ge, ns) f (parseDefs SLabelEnd <* eof) st | 1087 | , definitions = \ge -> first ((show +++ id) . snd) $ runP' (ge, ns) f (parseDefs SLabelEnd <* eof) st |
1088 | , sourceCode = str | ||
1089 | } | 1088 | } |
1090 | 1089 | ||
1091 | parseLC :: MonadError ErrorMsg m => FilePath -> String -> m Module | 1090 | parseLC :: MonadError ErrorMsg m => FilePath -> String -> m Module |