on master help sign in
Add retval nodes.
commite8b267f30865c2ddfe9da7108a22955fd0f7f657 authorMatus Tejiscak <ziman@functor.sk> dateFri 24 Jan 2014, 19:07 (13 years ago) parent6fe5f15
1 file changed+35−23
src/Idris/Erasure.hs+35−23
src/Idris/Erasure.hs+35−23
@@ -26,10 +26,17 @@ import Data.Set (Set)
2626import Data.IntSet (IntSet)
2727import Data.Map (Map)
2828import Data.IntMap (IntMap)
29+import Data.Text (pack)
2930
3031-- UseMap maps names to the set of used (reachable) argument positions.
3132type UseMap = Map Name IntSet
3233
34+data Arg = Arg !Int | Result
35+
36+instance Show Arg where
37+ show (Arg i) = show i
38+ show Result = "*"
39+
3340type Node = (Name, Int)
3441type Deps = Map Cond (Set Node)
3542
@@ -44,11 +51,16 @@ type Vars = Map Name Var
4451
4552-- Find the minimal consistent usage by forward chaining.
4653minimalUsage :: Deps -> UseMap
47−minimalUsage = gather . forwardChain
54+minimalUsage = gather . forwardChain . triggerMain
4855 where
4956 gather :: Ord a => Set (a, Int) -> Map a IntSet
5057 gather = foldr (\(n,i) -> M.insertWith IS.union n (IS.singleton i)) M.empty . S.toList
5158
59+ triggerMain :: Deps -> Deps
60+ triggerMain = M.insert S.empty $ S.singleton (main, -1)
61+ where
62+ main = NS (UN $ pack "main") [pack "Main"]
63+
5264forwardChain :: Deps -> Set Node
5365forwardChain deps
5466 | Just trivials <- M.lookup S.empty deps
@@ -91,32 +103,32 @@ buildDepMap ctx ns = dfs S.empty M.empty ns
91103 _ -> error $ "erasure checker: ambiguous name: " ++ show n
92104
93105 getDepsDef :: Name -> Def -> Deps
94− getDepsDef n (Function ty t) = error "a function encountered" -- TODO
95− getDepsDef n (TyDecl ty t) = M.empty
96− getDepsDef n (Operator ty n' f) = M.empty
97− getDepsDef n (CaseOp ci ty tys def tot cdefs)
98− = getDepsSC varMap sc
106+ getDepsDef fn (Function ty t) = error "a function encountered" -- TODO
107+ getDepsDef fn (TyDecl ty t) = M.empty
108+ getDepsDef fn (Operator ty n' f) = M.empty
109+ getDepsDef fn (CaseOp ci ty tys def tot cdefs)
110+ = getDepsSC fn varMap sc
99111 where
100112 -- the variables that arose as function arguments only depend on (n, i)
101− varMap = M.fromList [(v, S.singleton (n,i)) | (v,i) <- zip vars [0..]]
113+ varMap = M.fromList [(v, S.singleton (fn,i)) | (v,i) <- zip vars [0..]]
102114 (vars, sc) = cases_compiletime cdefs -- TODO: or cases_runtime?
103115
104− getDepsSC :: Vars -> SC -> Deps
105− getDepsSC vs ImpossibleCase = M.empty
106− getDepsSC vs (UnmatchedCase msg) = M.empty
107− getDepsSC vs (ProjCase t alt) = error "ProjCase not supported"
108− getDepsSC vs (STerm t) = getDepsTerm vs [] S.empty t
109− getDepsSC vs (Case n alts) = unionMap (getDepsAlt vs var) alts
116+ getDepsSC :: Name -> Vars -> SC -> Deps
117+ getDepsSC fn vs ImpossibleCase = M.empty
118+ getDepsSC fn vs (UnmatchedCase msg) = M.empty
119+ getDepsSC fn vs (ProjCase t alt) = error "ProjCase not supported"
120+ getDepsSC fn vs (STerm t) = getDepsTerm vs [] (S.singleton (fn, -1)) t
121+ getDepsSC fn vs (Case n alts) = unionMap (getDepsAlt fn vs var) alts
110122 where
111123 var = fromMaybe (error $ "nonpatvar in case: " ++ show n) (M.lookup n vs)
112124
113− getDepsAlt :: Vars -> Var -> CaseAlt -> Deps
114− getDepsAlt vs var (FnCase n ns sc) = error "an FnCase encountered" -- TODO: what's this?
115− getDepsAlt vs var (ConstCase c sc) = getDepsSC vs sc
116− getDepsAlt vs var (SucCase n sc) = getDepsSC vs sc -- deps for S can be hardcoded if needed
117− getDepsAlt vs var (DefaultCase sc) = getDepsSC vs sc
118− getDepsAlt vs var (ConCase n cnt ns sc)
119− = getDepsSC (vs' `M.union` vs) sc -- left-biased union
125+ getDepsAlt :: Name -> Vars -> Var -> CaseAlt -> Deps
126+ getDepsAlt fn vs var (FnCase n ns sc) = error "an FnCase encountered" -- TODO: what's this?
127+ getDepsAlt fn vs var (ConstCase c sc) = getDepsSC fn vs sc
128+ getDepsAlt fn vs var (SucCase n sc) = getDepsSC fn vs sc -- deps for S can be hardcoded if needed
129+ getDepsAlt fn vs var (DefaultCase sc) = getDepsSC fn vs sc
130+ getDepsAlt fn vs var (ConCase n cnt ns sc)
131+ = getDepsSC fn (vs' `M.union` vs) sc -- left-biased union
120132 where
121133 -- Here we insert dependencies that arose from pattern matching on a constructor.
122134 -- n = ctor name, j = ctor arg#, i = fun arg# of the cased var, cs = ctors of the cased var
@@ -150,14 +162,14 @@ buildDepMap ctx ns = dfs S.empty M.empty ns
150162 getDepsTerm vs bs cd app@(App _ _)
151163 | (fun, args) <- unApply app = case fun of
152164 -- these depend on whether the referred thing uses the argument
153− P Ref n _ -> called n args
154− P (DCon _ _) n _ -> called n args
165+ P Ref n _ -> unionMap (getDepsArgs n) $ zip [0..] args
166+ P (DCon _ _) n _ -> unionMap (getDepsArgs n) $ zip [0..] args
155167
156168 -- these do not
157169 P (TCon _ _) n _ -> unionMap (getDepsTerm vs bs cd) args
158170 P Bound n _ -> unionMap (getDepsTerm vs bs cd) args
159171 where
160− called n args = unionMap (\(i,t) -> getDepsTerm vs bs (S.insert (n,i) cd) t) (zip [0..] args)
172+ getDepsArgs n (i, t) = getDepsTerm vs bs (S.insert (n,i) . S.insert (n,-1) $ cd) t
161173
162174 -- the easy cases
163175 getDepsTerm vs bs cd (Constant _) = M.empty