diff options
author | Péter Diviánszky <divipp@gmail.com> | 2016-02-03 23:53:32 +0100 |
---|---|---|
committer | Péter Diviánszky <divipp@gmail.com> | 2016-02-03 23:53:32 +0100 |
commit | 70a5a26212d99e90625c8d8ed29cb20218168520 (patch) | |
tree | 06cbd187a485b756b5f08578982c61df74f486a5 | |
parent | cd509ac8dead8465a036824eb6188ecdc58c9a25 (diff) |
eliminate downS
-rw-r--r-- | src/LambdaCube/Compiler/Infer.hs | 2 | ||||
-rw-r--r-- | src/LambdaCube/Compiler/Parser.hs | 22 | ||||
-rw-r--r-- | testdata/typeclass.lc | 6 | ||||
-rw-r--r-- | testdata/typeclass.out | 24 |
4 files changed, 18 insertions, 36 deletions
diff --git a/src/LambdaCube/Compiler/Infer.hs b/src/LambdaCube/Compiler/Infer.hs index 9397245b..fe17cfa4 100644 --- a/src/LambdaCube/Compiler/Infer.hs +++ b/src/LambdaCube/Compiler/Infer.hs | |||
@@ -1153,7 +1153,7 @@ handleStmt defs = \case | |||
1153 | Let n mf mt ar t_ -> do | 1153 | Let n mf mt ar t_ -> do |
1154 | af <- addF | 1154 | af <- addF |
1155 | let t__ = maybe id (flip SAnn . af) mt t_ | 1155 | let t__ = maybe id (flip SAnn . af) mt t_ |
1156 | (x, t) <- inferTerm (snd n) tr id $ trSExp' $ fromMaybe (SBuiltin "primFix" `SAppV` SLamV t__) $ downS 0 t__ | 1156 | (x, t) <- inferTerm (snd n) tr id $ trSExp' $ if usedS n t__ then SBuiltin "primFix" `SAppV` SLamV (substSG0 n t__) else t__ |
1157 | tellStmtType (fst n) t | 1157 | tellStmtType (fst n) t |
1158 | addToEnv n (mkELet (True, n, SData mf, ar) x t, t) | 1158 | addToEnv n (mkELet (True, n, SData mf, ar) x t, t) |
1159 | PrecDef{} -> return () | 1159 | PrecDef{} -> return () |
diff --git a/src/LambdaCube/Compiler/Parser.hs b/src/LambdaCube/Compiler/Parser.hs index 0ec5e83e..67dbe5fc 100644 --- a/src/LambdaCube/Compiler/Parser.hs +++ b/src/LambdaCube/Compiler/Parser.hs | |||
@@ -248,6 +248,8 @@ foldS h g f = fs | |||
248 | 248 | ||
249 | freeS = nub . foldS (\_ _ _ -> error "freeS") (\sn _ -> [sn]) mempty 0 | 249 | freeS = nub . foldS (\_ _ _ -> error "freeS") (\sn _ -> [sn]) mempty 0 |
250 | 250 | ||
251 | usedS n = getAny . foldS (\_ _ _ -> error "usedS") (\sn _ -> Any $ n == sn) mempty 0 | ||
252 | |||
251 | mapS' = mapS__ (\_ _ _ -> error "mapS'") (const . SGlobal) | 253 | mapS' = mapS__ (\_ _ _ -> error "mapS'") (const . SGlobal) |
252 | mapS__ hh gg f2 h = g where | 254 | mapS__ hh gg f2 h = g where |
253 | g i = \case | 255 | g i = \case |
@@ -261,7 +263,7 @@ mapS__ hh gg f2 h = g where | |||
261 | 263 | ||
262 | rearrangeS :: (Int -> Int) -> SExp -> SExp | 264 | rearrangeS :: (Int -> Int) -> SExp -> SExp |
263 | rearrangeS f = mapS' (\sn j i -> SVar sn $ if j < i then j else i + f (j - i)) (+1) 0 | 265 | rearrangeS f = mapS' (\sn j i -> SVar sn $ if j < i then j else i + f (j - i)) (+1) 0 |
264 | 266 | {- | |
265 | substS'' :: Int -> Int -> SExp' a -> SExp' a | 267 | substS'' :: Int -> Int -> SExp' a -> SExp' a |
266 | substS'' j' x = mapS' f2 (+1) j' | 268 | substS'' j' x = mapS' f2 (+1) j' |
267 | where | 269 | where |
@@ -269,12 +271,12 @@ substS'' j' x = mapS' f2 (+1) j' | |||
269 | | j < i = SVar sn j | 271 | | j < i = SVar sn j |
270 | | j == i = SVar sn $ x + (j - j') | 272 | | j == i = SVar sn $ x + (j - j') |
271 | | j > i = SVar sn $ j - 1 | 273 | | j > i = SVar sn $ j - 1 |
272 | 274 | -} | |
273 | substSG j = mapS__ (\_ _ _ -> error "substSG") (\sn x -> if sn == j then SVar sn x else SGlobal sn) (\sn j -> const $ SVar sn j) (+1) | 275 | substSG j = mapS__ (\_ _ _ -> error "substSG") (\sn x -> if sn == j then SVar sn x else SGlobal sn) (\sn j -> const $ SVar sn j) (+1) |
274 | substSG0 n = substSG n 0 . up1 | 276 | substSG0 n = substSG n 0 . up1 |
275 | 277 | ||
276 | downS t x | used t x = Nothing | 278 | downS n x | usedS n x = Nothing |
277 | | otherwise = Just $ substS'' t (error "impossible") x | 279 | | otherwise = Just x -- $ substS'' t (error "impossible") x |
278 | 280 | ||
279 | instance Up Void where | 281 | instance Up Void where |
280 | up_ n i = error "up_ @Void" | 282 | up_ n i = error "up_ @Void" |
@@ -744,7 +746,7 @@ data Stmt | |||
744 | | Class SIName [SExp]{-parameters-} [(SIName, SExp)]{-method names and types-} | 746 | | Class SIName [SExp]{-parameters-} [(SIName, SExp)]{-method names and types-} |
745 | | Instance SIName [Pat]{-parameter patterns-} [SExp]{-constraints-} [Stmt]{-method definitions-} | 747 | | Instance SIName [Pat]{-parameter patterns-} [SExp]{-constraints-} [Stmt]{-method definitions-} |
746 | | TypeAnn SIName SExp -- intermediate | 748 | | TypeAnn SIName SExp -- intermediate |
747 | | FunAlt SIName [((Visibility, SExp), Pat)] (Either [(SExp, SExp)] SExp) | 749 | | FunAlt SIName [((Visibility, SExp), Pat)] (Either [(SExp, SExp)]{-guards-} SExp{-no guards-}) |
748 | deriving (Show) | 750 | deriving (Show) |
749 | 751 | ||
750 | pattern Primitive n mf t <- Let n mf (Just t) _ (SBuiltin "undefined") where Primitive n mf t = Let n mf (Just t) (map fst $ fst $ getParamsS t) $ SBuiltin "undefined" | 752 | pattern Primitive n mf t <- Let n mf (Just t) _ (SBuiltin "undefined") where Primitive n mf t = Let n mf (Just t) (map fst $ fst $ getParamsS t) $ SBuiltin "undefined" |
@@ -814,7 +816,7 @@ parseDef = | |||
814 | where | 816 | where |
815 | mkProj (cn, (Just fs, _)) | 817 | mkProj (cn, (Just fs, _)) |
816 | = [ Let fn Nothing Nothing [Visible] | 818 | = [ Let fn Nothing Nothing [Visible] |
817 | $ up1{-non-rec-} $ patLam SLabelEnd ge (PCon cn $ replicate (length fs) $ ParPat [PVar (fst cn, "generated_name1")]) $ SVar (fst cn, ".proj") i | 819 | $ patLam SLabelEnd ge (PCon cn $ replicate (length fs) $ ParPat [PVar (fst cn, "generated_name1")]) $ SVar (fst cn, ".proj") i |
818 | | (i, fn) <- zip [0..] fs] | 820 | | (i, fn) <- zip [0..] fs] |
819 | mkProj _ = [] | 821 | mkProj _ = [] |
820 | 822 | ||
@@ -844,7 +846,7 @@ funAltDef parseName = do -- todo: use ns to determine parseName | |||
844 | n <- parseSIName parseName | 846 | n <- parseSIName parseName |
845 | localIndentation Gt $ (,) n <$> telescopePat <* lookAhead (reservedOp "=" <|> reservedOp "|") | 847 | localIndentation Gt $ (,) n <$> telescopePat <* lookAhead (reservedOp "=" <|> reservedOp "|") |
846 | checkPattern fee | 848 | checkPattern fee |
847 | FunAlt n (map (second $ upP 0 1{-todo: replace n with Var 0-}) tss) <$> parseRHS (dbf' $ fee ++ [n]) "=" | 849 | FunAlt n tss <$> parseRHS (dbf' fee) "=" |
848 | 850 | ||
849 | valueDef :: P Stmt | 851 | valueDef :: P Stmt |
850 | valueDef = do | 852 | valueDef = do |
@@ -867,9 +869,9 @@ parseSomeGuards f = do | |||
867 | 869 | ||
868 | mkLets :: Bool -> DesugarInfo -> [Stmt]{-where block-} -> SExp{-main expression-} -> SExp{-big let with lambdas; replaces global names with de bruijn indices-} | 870 | mkLets :: Bool -> DesugarInfo -> [Stmt]{-where block-} -> SExp{-main expression-} -> SExp{-big let with lambdas; replaces global names with de bruijn indices-} |
869 | mkLets _ _ [] e = e | 871 | mkLets _ _ [] e = e |
870 | mkLets False ge (Let n _ mt ar (downS 0 -> Just x): ds) e | 872 | mkLets False ge (Let n _ mt ar x: ds) e | not $ usedS n x |
871 | = SLet (False, n, SData Nothing, ar) (maybe id (flip SAnn . addForalls {-todo-}[] []) mt x) (substSG0 n $ mkLets False ge ds e) | 873 | = SLet (False, n, SData Nothing, ar) (maybe id (flip SAnn . addForalls {-todo-}[] []) mt x) (substSG0 n $ mkLets False ge ds e) |
872 | mkLets True ge (Let n _ mt ar (downS 0 -> Just x): ds) e | 874 | mkLets True ge (Let n _ mt ar x: ds) e | not $ usedS n x |
873 | = SLet (False, n, SData Nothing, ar) (maybe id (flip SAnn . addForalls {-todo-}[] []) mt x) (substSG0 n $ mkLets True ge ds e) | 875 | = SLet (False, n, SData Nothing, ar) (maybe id (flip SAnn . addForalls {-todo-}[] []) mt x) (substSG0 n $ mkLets True ge ds e) |
874 | mkLets le ge (ValueDef p x: ds) e = patLam id ge p (dbff (getPVars p) $ mkLets le ge ds e) `SAppV` x -- (p = e; f) --> (\p -> f) e | 876 | mkLets le ge (ValueDef p x: ds) e = patLam id ge p (dbff (getPVars p) $ mkLets le ge ds e) `SAppV` x -- (p = e; f) --> (\p -> f) e |
875 | mkLets _ _ (x: ds) e = error $ "mkLets: " ++ show x | 877 | mkLets _ _ (x: ds) e = error $ "mkLets: " ++ show x |
@@ -906,7 +908,7 @@ compileFunAlts par ulend lend ds xs = dsInfo >>= \ge -> case xs of | |||
906 | ++ [ FunAlt n (replicate (length ps) (noTA $ PVar (debugSI "compileFunAlts1", "generated_name0"))) $ Right $ SBuiltin "'Empty" `SAppV` sLit (LString $ "no instance of " ++ snd n ++ " on ???")] | 908 | ++ [ FunAlt n (replicate (length ps) (noTA $ PVar (debugSI "compileFunAlts1", "generated_name0"))) $ Right $ SBuiltin "'Empty" `SAppV` sLit (LString $ "no instance of " ++ snd n ++ " on ???")] |
907 | ++ concat | 909 | ++ concat |
908 | [ TypeAnn m (addParamsS (map ((,) Hidden) ps) $ SPi Hidden (foldl SAppV (SGlobal n) $ downToS 0 $ length ps) $ up1 t) | 910 | [ TypeAnn m (addParamsS (map ((,) Hidden) ps) $ SPi Hidden (foldl SAppV (SGlobal n) $ downToS 0 $ length ps) $ up1 t) |
909 | : [ FunAlt m p $ Right $ {- SLam Hidden (Wildcard SType) $ up1 $ -} substS'' 0 ic $ up1_ (ic+1) e | 911 | : [ FunAlt m p $ Right {- $ SLam Hidden (Wildcard SType) $ up1 -} e |
910 | | Instance n' i cstrs alts <- ds, n' == n | 912 | | Instance n' i cstrs alts <- ds, n' == n |
911 | , Let m' ~Nothing ~Nothing ar e <- alts, m' == m | 913 | , Let m' ~Nothing ~Nothing ar e <- alts, m' == m |
912 | , let p = zip ((,) Hidden <$> ps) i -- ++ ((Hidden, Wildcard SType), PVar): [] | 914 | , let p = zip ((,) Hidden <$> ps) i -- ++ ((Hidden, Wildcard SType), PVar): [] |
diff --git a/testdata/typeclass.lc b/testdata/typeclass.lc index a0ba8068..1ec4ba73 100644 --- a/testdata/typeclass.lc +++ b/testdata/typeclass.lc | |||
@@ -24,12 +24,12 @@ a /= b = not (a == b) | |||
24 | instance Eq Bool where | 24 | instance Eq Bool where |
25 | True == a = a | 25 | True == a = a |
26 | False == a = not a | 26 | False == a = not a |
27 | 27 | {- todo | |
28 | instance Eq t => Eq [t] where | 28 | instance Eq t => Eq [t] where |
29 | [] == [] = True | 29 | [] == [] = True |
30 | (==) (a:as) (b:bs) = a == b -- && as == bs | 30 | a:as == b:bs = a == b && as == bs |
31 | -- TODO a:as == b:bs = a == b && as == bs | ||
32 | _ == _ = False | 31 | _ == _ = False |
32 | -} | ||
33 | {- | 33 | {- |
34 | Ord = \a -> Eq a & Ord' a -- so this is an alias, always subst. | 34 | Ord = \a -> Eq a & Ord' a -- so this is an alias, always subst. |
35 | 35 | ||
diff --git a/testdata/typeclass.out b/testdata/typeclass.out index 43360117..3b1d788d 100644 --- a/testdata/typeclass.out +++ b/testdata/typeclass.out | |||
@@ -29,7 +29,6 @@ testdata/typeclass.lc 16:14-17:17 Bool->Bool | |||
29 | testdata/typeclass.lc 17:13-17:17 Bool | 29 | testdata/typeclass.lc 17:13-17:17 Bool |
30 | testdata/typeclass.lc 19:7-19:9 Type->Type | 30 | testdata/typeclass.lc 19:7-19:9 Type->Type |
31 | testdata/typeclass.lc 19:7-20:27 Type | 31 | testdata/typeclass.lc 19:7-20:27 Type |
32 | testdata/typeclass.lc 19:7-32:25 V0->V1 | {a} -> {b : Eq a} -> a -> a->Bool | ||
33 | testdata/typeclass.lc 20:5-20:9 {a} -> {b : Eq a} -> a -> a->Bool | 32 | testdata/typeclass.lc 20:5-20:9 {a} -> {b : Eq a} -> a -> a->Bool |
34 | testdata/typeclass.lc 20:13-20:14 Type | 33 | testdata/typeclass.lc 20:13-20:14 Type |
35 | testdata/typeclass.lc 20:13-20:27 Type | 34 | testdata/typeclass.lc 20:13-20:27 Type |
@@ -44,10 +43,8 @@ testdata/typeclass.lc 22:15-22:16 V5 | |||
44 | testdata/typeclass.lc 22:15-22:19 V4->Bool | 43 | testdata/typeclass.lc 22:15-22:19 V4->Bool |
45 | testdata/typeclass.lc 22:17-22:19 {a} -> {b : Eq a} -> a -> a->Bool | 44 | testdata/typeclass.lc 22:17-22:19 {a} -> {b : Eq a} -> a -> a->Bool |
46 | testdata/typeclass.lc 22:20-22:21 V2 | 45 | testdata/typeclass.lc 22:20-22:21 V2 |
47 | testdata/typeclass.lc 24:13-24:17 Type | 46 | testdata/typeclass.lc 24:13-24:17 Type | Type->Type |
48 | testdata/typeclass.lc 24:13-26:23 ({a : Eq V0} -> V1 -> V2->Bool) -> {e : Eq V1} -> V2 -> V3->Bool | 47 | testdata/typeclass.lc 24:13-26:23 ({a : Eq V0} -> V1 -> V2->Bool) -> {e : Eq V1} -> V2 -> V3->Bool | {a} -> {b : Eq a} -> a -> a->Bool |
49 | testdata/typeclass.lc 24:13-28:23 Type | Type->Type | V0->V1 | ||
50 | testdata/typeclass.lc 24:13-32:25 {a : Eq V0} -> V1 -> V2->Bool | {a} -> {b : Eq a} -> a -> a->Bool | ||
51 | testdata/typeclass.lc 25:5-25:9 Bool | 48 | testdata/typeclass.lc 25:5-25:9 Bool |
52 | testdata/typeclass.lc 25:5-26:23 Bool | Bool -> Bool->Bool | Bool->Bool | 49 | testdata/typeclass.lc 25:5-26:23 Bool | Bool -> Bool->Bool | Bool->Bool |
53 | testdata/typeclass.lc 25:17-25:18 Bool | 50 | testdata/typeclass.lc 25:17-25:18 Bool |
@@ -55,20 +52,3 @@ testdata/typeclass.lc 25:17-26:23 Bool->Bool | |||
55 | testdata/typeclass.lc 26:18-26:21 Bool->Bool | 52 | testdata/typeclass.lc 26:18-26:21 Bool->Bool |
56 | testdata/typeclass.lc 26:18-26:23 Bool | 53 | testdata/typeclass.lc 26:18-26:23 Bool |
57 | testdata/typeclass.lc 26:22-26:23 Bool | 54 | testdata/typeclass.lc 26:22-26:23 Bool |
58 | testdata/typeclass.lc 28:10-28:12 Type->Type | ||
59 | testdata/typeclass.lc 28:10-28:14 Type | Type->Type | ||
60 | testdata/typeclass.lc 28:10-28:23 Type->Type | ||
61 | testdata/typeclass.lc 28:13-28:14 Type | ||
62 | testdata/typeclass.lc 28:22-28:23 Type | ||
63 | testdata/typeclass.lc 28:22-32:25 ({a : Eq V0} -> V1 -> V2->Bool) -> {e : Eq V1} -> V2 -> V3->Bool | ||
64 | testdata/typeclass.lc 29:20-29:24 Bool | ||
65 | testdata/typeclass.lc 29:20-32:25 Bool | List V0 -> Bool | List V1 -> List V2 -> Bool | List V2 -> Bool | a:Type -> {b : Eq a} -> List a -> List a -> Bool | ||
66 | testdata/typeclass.lc 30:18-30:22 List V7 | ||
67 | testdata/typeclass.lc 30:18-32:25 Bool | List V1 -> Bool | V0 -> List V1 -> Bool | ||
68 | testdata/typeclass.lc 30:26-30:27 V7 | ||
69 | testdata/typeclass.lc 30:26-30:30 V6->Bool | ||
70 | testdata/typeclass.lc 30:26-30:32 Bool | List V1 -> Bool | V0 -> List V1 -> Bool | ||
71 | testdata/typeclass.lc 30:26-32:25 List V3 -> Bool | ||
72 | testdata/typeclass.lc 30:28-30:30 {a} -> {b : Eq a} -> a -> a->Bool | ||
73 | testdata/typeclass.lc 30:31-30:32 V3 | ||
74 | testdata/typeclass.lc 32:20-32:25 Bool | List V1 -> Bool | V0 -> List V1 -> Bool | ||