on master help sign in
Add eta-expansion.
commit7dec6997b2e84d873cbefbde7434a593189012ad authorMatus Tejiscak <ziman@functor.sk> dateFri 24 Jan 2014, 22:47 (13 years ago) parenta92914b
1 file changed+43−15
src/Idris/Erasure.hs+43−15
src/Idris/Erasure.hs+43−15
@@ -105,8 +105,9 @@ buildDepMap ctx ns = addPostulates $ dfs S.empty M.empty ns
105105 , (name "prim__strCons", Arg 1)
106106 , (name "prim__strHead", Arg 0)
107107 , (name "prim__strTail", Arg 0)
108+ , (name "prim__concat", Arg 0)
109+ , (name "prim__concat", Arg 1)
108110 , (name "mkForeignPrim", Arg 2)
109−-- , (name "MkIO", Arg 1)
110111 ]
111112 ]
112113
@@ -142,28 +143,40 @@ buildDepMap ctx ns = addPostulates $ dfs S.empty M.empty ns
142143 getDepsDef fn (TyDecl ty t) = M.empty
143144 getDepsDef fn (Operator ty n' f) = M.empty
144145 getDepsDef fn (CaseOp ci ty tys def tot cdefs)
145− = getDepsSC fn varMap sc
146+ = getDepsSC fn etaVars (etaMap `M.union` varMap) sc
146147 where
148+ -- we must eta-expand the definition with fresh variables
149+ -- to capture these dependencies as well
150+ etaIdx = [length vars .. length tys - 1]
151+ etaVars = [eta i | i <- etaIdx]
152+ etaMap = M.fromList [(eta i, S.singleton (fn, Arg i)) | i <- etaIdx]
153+ eta i = MN i (pack "eta")
154+
147155 -- the variables that arose as function arguments only depend on (n, i)
148156 varMap = M.fromList [(v, S.singleton (fn, Arg i)) | (v,i) <- zip vars [0..]]
149157 (vars, sc) = cases_compiletime cdefs -- TODO: or cases_runtime?
150158
151− getDepsSC :: Name -> Vars -> SC -> Deps
152− getDepsSC fn vs ImpossibleCase = M.empty
153− getDepsSC fn vs (UnmatchedCase msg) = M.empty
154− getDepsSC fn vs (ProjCase t alt) = error "ProjCase not supported"
155− getDepsSC fn vs (STerm t) = getDepsTerm vs [] (S.singleton (fn, Result)) t
156− getDepsSC fn vs (Case n alts) = unionMap (getDepsAlt fn vs var) alts
159+ etaExpand :: [Name] -> Term -> Term
160+ etaExpand [] t = t
161+ etaExpand (n : ns) t = App (etaExpand ns t) (P Bound n Erased)
162+
163+ getDepsSC :: Name -> [Name] -> Vars -> SC -> Deps
164+ getDepsSC fn es vs ImpossibleCase = M.empty
165+ getDepsSC fn es vs (UnmatchedCase msg) = M.empty
166+ getDepsSC fn es vs (ProjCase t alt) = error "ProjCase not supported"
167+ getDepsSC fn [] vs (STerm t) = getDepsTerm vs [] (S.singleton (fn, Result)) t
168+ getDepsSC fn es vs (STerm t) | ("EXPAND",es,t,"==>",etaExpand es t) `traceShow` True = getDepsTerm vs [] (S.singleton (fn, Result)) (etaExpand es t)
169+ getDepsSC fn es vs (Case n alts) = unionMap (getDepsAlt fn es vs var) alts
157170 where
158171 var = fromMaybe (error $ "nonpatvar in case: " ++ show n) (M.lookup n vs)
159172
160− getDepsAlt :: Name -> Vars -> Var -> CaseAlt -> Deps
161− getDepsAlt fn vs var (FnCase n ns sc) = error "an FnCase encountered" -- TODO: what's this?
162− getDepsAlt fn vs var (ConstCase c sc) = getDepsSC fn vs sc
163− getDepsAlt fn vs var (SucCase n sc) = getDepsSC fn vs sc -- deps for S can be hardcoded if needed
164− getDepsAlt fn vs var (DefaultCase sc) = getDepsSC fn vs sc
165− getDepsAlt fn vs var (ConCase n cnt ns sc)
166− = getDepsSC fn (vs' `M.union` vs) sc -- left-biased union
173+ getDepsAlt :: Name -> [Name] -> Vars -> Var -> CaseAlt -> Deps
174+ getDepsAlt fn es vs var (FnCase n ns sc) = error "an FnCase encountered" -- TODO: what's this?
175+ getDepsAlt fn es vs var (ConstCase c sc) = getDepsSC fn es vs sc
176+ getDepsAlt fn es vs var (SucCase n sc) = getDepsSC fn es vs sc -- deps for S can be hardcoded if needed
177+ getDepsAlt fn es vs var (DefaultCase sc) = getDepsSC fn es vs sc
178+ getDepsAlt fn es vs var (ConCase n cnt ns sc)
179+ = getDepsSC fn es (vs' `M.union` vs) sc -- left-biased union
167180 where
168181 -- Here we insert dependencies that arose from pattern matching on a constructor.
169182 -- n = ctor name, j = ctor arg#, i = fun arg# of the cased var, cs = ctors of the cased var
@@ -206,6 +219,13 @@ buildDepMap ctx ns = addPostulates $ dfs S.empty M.empty ns
206219 -- a bound variable might draw in additional dependencies,
207220 -- think: f x = x 0 <-- here, `x' _is_ used
208221 P Bound n _ -> var n `ins` unionMap (getDepsTerm vs bs cd) args
222+
223+ -- we interpret applied lambdas as lets in order to reuse code here
224+ Bind n (Lam ty) t ->
225+ ("REFORM", app, "==>", lamToLet [] app) `traceShow`
226+ getDepsTerm vs bs cd (lamToLet [] app)
227+
228+ _ -> error $ "cannot analyse application of: " ++ show fun
209229 where
210230 ins = M.insertWith S.union cd
211231 var n = fromMaybe (error $ "non-existent bound variable: " ++ show n) (M.lookup n vs)
@@ -218,6 +238,14 @@ buildDepMap ctx ns = addPostulates $ dfs S.empty M.empty ns
218238 getDepsTerm vs bs cd Erased = M.empty
219239 getDepsTerm vs bs cd Impossible = M.empty
220240
241+ -- convert applications of lambdas to lets
242+ -- Note that this transformation preserves de bruijn numbering
243+ lamToLet :: [Term] -> Term -> Term
244+ lamToLet xs (App f x) = lamToLet (x:xs) f
245+ lamToLet (x:xs) (Bind n (Lam ty) t) = Bind n (Let ty x) (lamToLet xs t)
246+ lamToLet (x:xs) t = App (lamToLet xs t) x
247+ lamToLet [] t = t
248+
221249 unions :: [Deps] -> Deps
222250 unions = M.unionsWith S.union
223251