git.iko.soy/Idris-dev
on master help sign in
Recognise instance constructors in Compiler.hs.
cee5985Matus Tejiscak
src/IRTS/Compiler.hs+14−4
compare with master
unifiedsplit
@@ -315,7 +315,6 @@ irTerm vs env (Constant c) = return $ LConst c
315irTerm vs env (TType _) = return $ LNothing
315irTerm vs env (TType _) = return $ LNothing
316irTerm vs env Erased = return $ LNothing
316irTerm vs env Erased = return $ LNothing
317irTerm vs env Impossible = return $ LNothing
317irTerm vs env Impossible = return $ LNothing
318−-- ir' env _ = return $ LError "Impossible"
319
318
320irCon :: Vars -> [Name] -> Int -> Name -> [Term] -> Idris LExp
319irCon :: Vars -> [Name] -> Int -> Name -> [Term] -> Idris LExp
321irCon vs env arity n args
320irCon vs env arity n args
@@ -472,9 +471,20 @@ irAlt :: Vars -> LExp -> CaseAlt -> Idris LAlt
472
471
473-- this leaves out all unused arguments of the constructor
472-- this leaves out all unused arguments of the constructor
474irAlt vs _ (ConCase n t args sc) = do
473irAlt vs _ (ConCase n t args sc) = do
475− sc' <- irSC vs sc
474+ used <- getUsed . lookup n <$> getIState
475+ let usedArgs = [a | (i,a) <- zip [0..] args, i `elem` used]
476+ LConCase (-1) n usedArgs <$> irSC (methodVars `M.union` vs) sc
477+ where
478+ lookup n = lookupCtxtExact n . idris_callgraph
476− used <- maybe [] (map fst . usedpos) . lookupCtxtExact n . idris_callgraph <$> getIState
479+ getUsed = maybe [] (map fst . usedpos)
477− return $ LConCase (-1) n [a | (i,a) <- zip [0..] args, i `elem` used] sc'
480+
481+ methodVars = case n of
482+ SN (InstanceCtorN className)
483+ -> M.fromList [(v, VI
484+ { viMethod = Just $ mkFieldName n i
485+ }) | (v,i) <- zip args [0..]]
486+ _
487+ -> M.empty -- not an instance constructor
478
488
479irAlt vs _ (ConstCase x rhs)
489irAlt vs _ (ConstCase x rhs)
480 | matchable x = LConstCase x <$> irSC vs rhs
490 | matchable x = LConstCase x <$> irSC vs rhs
src/Idris/Erasure.hs+6−6
@@ -1,6 +1,6 @@
1{-# LANGUAGE PatternGuards #-}
1{-# LANGUAGE PatternGuards #-}
2
2
3−module Idris.Erasure (performUsageAnalysis) where
3+module Idris.Erasure (performUsageAnalysis, mkFieldName) where
4
4
5import Idris.AbsSyntax
5import Idris.AbsSyntax
6import Idris.Core.CaseTree
6import Idris.Core.CaseTree
@@ -306,7 +306,7 @@ buildDepMap ci ctx mainName = addPostulates $ dfs S.empty M.empty [mainName]
306
306
307 -- generate metamethod names, "n" is the instance ctor
307 -- generate metamethod names, "n" is the instance ctor
308 meth :: Int -> Maybe Name
308 meth :: Int -> Maybe Name
309− meth | SN (InstanceCtorN className) <- n = \j -> Just (mkField n j)
309+ meth | SN (InstanceCtorN className) <- n = \j -> Just (mkFieldName n j)
310 | otherwise = \j -> Nothing
310 | otherwise = \j -> Nothing
311
311
312 -- Named variables -> DeBruijn variables -> Conds/guards -> Term -> Deps
312 -- Named variables -> DeBruijn variables -> Conds/guards -> Term -> Deps
@@ -423,7 +423,7 @@ buildDepMap ci ctx mainName = addPostulates $ dfs S.empty M.empty [mainName]
423 deps i = M.singleton (metameth, Arg i) S.empty
423 deps i = M.singleton (metameth, Arg i) S.empty
424 bruijns = reverse [\cd -> M.singleton cd (deps i) | i <- [0 .. length args - 1]]
424 bruijns = reverse [\cd -> M.singleton cd (deps i) | i <- [0 .. length args - 1]]
425 cond = S.singleton (metameth, Result)
425 cond = S.singleton (metameth, Result)
426− metameth = mkField ctorName methNo
426+ metameth = mkFieldName ctorName methNo
427 (args, body) = unfoldLams t
427 (args, body) = unfoldLams t
428
428
429 -- projections
429 -- projections
@@ -471,9 +471,6 @@ buildDepMap ci ctx mainName = addPostulates $ dfs S.empty M.empty [mainName]
471 unfoldLams (Bind n (Lam ty) t) = let (ns,t') = unfoldLams t in (n:ns, t')
471 unfoldLams (Bind n (Lam ty) t) = let (ns,t') = unfoldLams t in (n:ns, t')
472 unfoldLams t = ([], t)
472 unfoldLams t = ([], t)
473
473
474− mkField :: Name -> Int -> Name
475− mkField ctorName fieldNo = SN (WhereN fieldNo ctorName $ sMN fieldNo "field")
476−
477 union :: Deps -> Deps -> Deps
474 union :: Deps -> Deps -> Deps
478 union = M.unionWith (M.unionWith S.union)
475 union = M.unionWith (M.unionWith S.union)
479
476
@@ -482,3 +479,6 @@ buildDepMap ci ctx mainName = addPostulates $ dfs S.empty M.empty [mainName]
482
479
483 unionMap :: (a -> Deps) -> [a] -> Deps
480 unionMap :: (a -> Deps) -> [a] -> Deps
484 unionMap f = M.unionsWith (M.unionWith S.union) . map f
481 unionMap f = M.unionsWith (M.unionWith S.union) . map f
482+
483+mkFieldName :: Name -> Int -> Name
484+mkFieldName ctorName fieldNo = SN (WhereN fieldNo ctorName $ sMN fieldNo "field")