@@ -105,8 +105,9 @@ buildDepMap ctx ns = addPostulates $ dfs S.empty M.empty ns
105 , (name "prim__strCons", Arg 1)
105 , (name "prim__strCons", Arg 1)
106 , (name "prim__strHead", Arg 0)
106 , (name "prim__strHead", Arg 0)
107 , (name "prim__strTail", Arg 0)
107 , (name "prim__strTail", Arg 0)
108+ , (name "prim__concat", Arg 0)
109+ , (name "prim__concat", Arg 1)
108 , (name "mkForeignPrim", Arg 2)
110 , (name "mkForeignPrim", Arg 2)
109−-- , (name "MkIO", Arg 1)
@@ -142,28 +143,40 @@ buildDepMap ctx ns = addPostulates $ dfs S.empty M.empty ns
142 getDepsDef fn (TyDecl ty t) = M.empty
143 getDepsDef fn (TyDecl ty t) = M.empty
143 getDepsDef fn (Operator ty n' f) = M.empty
144 getDepsDef fn (Operator ty n' f) = M.empty
144 getDepsDef fn (CaseOp ci ty tys def tot cdefs)
145 getDepsDef fn (CaseOp ci ty tys def tot cdefs)
145− = getDepsSC fn varMap sc
146+ = getDepsSC fn etaVars (etaMap `M.union` varMap) sc
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")
147 -- the variables that arose as function arguments only depend on (n, i)
155 -- the variables that arose as function arguments only depend on (n, i)
148 varMap = M.fromList [(v, S.singleton (fn, Arg i)) | (v,i) <- zip vars [0..]]
156 varMap = M.fromList [(v, S.singleton (fn, Arg i)) | (v,i) <- zip vars [0..]]
149 (vars, sc) = cases_compiletime cdefs -- TODO: or cases_runtime?
157 (vars, sc) = cases_compiletime cdefs -- TODO: or cases_runtime?
159+ etaExpand :: [Name] -> Term -> Term
161+ etaExpand (n : ns) t = App (etaExpand ns t) (P Bound n Erased)
151− getDepsSC :: Name -> Vars -> SC -> Deps
163+ getDepsSC :: Name -> [Name] -> Vars -> SC -> Deps
152− getDepsSC fn vs ImpossibleCase = M.empty
164+ getDepsSC fn es vs ImpossibleCase = M.empty
153− getDepsSC fn vs (UnmatchedCase msg) = M.empty
165+ getDepsSC fn es vs (UnmatchedCase msg) = M.empty
154− getDepsSC fn vs (ProjCase t alt) = error "ProjCase not supported"
166+ getDepsSC fn es vs (ProjCase t alt) = error "ProjCase not supported"
155− getDepsSC fn vs (STerm t) = getDepsTerm vs [] (S.singleton (fn, Result)) t
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)
156− getDepsSC fn vs (Case n alts) = unionMap (getDepsAlt fn vs var) alts
169+ getDepsSC fn es vs (Case n alts) = unionMap (getDepsAlt fn es vs var) alts
158 var = fromMaybe (error $ "nonpatvar in case: " ++ show n) (M.lookup n vs)
171 var = fromMaybe (error $ "nonpatvar in case: " ++ show n) (M.lookup n vs)
160− getDepsAlt :: Name -> Vars -> Var -> CaseAlt -> Deps
173+ getDepsAlt :: Name -> [Name] -> Vars -> Var -> CaseAlt -> Deps
161− getDepsAlt fn vs var (FnCase n ns sc) = error "an FnCase encountered" -- TODO: what's this?
174+ getDepsAlt fn es 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
175+ getDepsAlt fn es vs var (ConstCase c sc) = getDepsSC fn es vs sc
163− getDepsAlt fn vs var (SucCase n sc) = getDepsSC fn vs sc -- deps for S can be hardcoded if needed
176+ getDepsAlt fn es vs var (SucCase n sc) = getDepsSC fn es vs sc -- deps for S can be hardcoded if needed
164− getDepsAlt fn vs var (DefaultCase sc) = getDepsSC fn vs sc
177+ getDepsAlt fn es vs var (DefaultCase sc) = getDepsSC fn es vs sc
165− getDepsAlt fn vs var (ConCase n cnt ns sc)
178+ getDepsAlt fn es vs var (ConCase n cnt ns sc)
166− = getDepsSC fn (vs' `M.union` vs) sc -- left-biased union
179+ = getDepsSC fn es (vs' `M.union` vs) sc -- left-biased union
168 -- Here we insert dependencies that arose from pattern matching on a constructor.
181 -- Here we insert dependencies that arose from pattern matching on a constructor.
169 -- n = ctor name, j = ctor arg#, i = fun arg# of the cased var, cs = ctors of the cased var
182 -- 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
206 -- a bound variable might draw in additional dependencies,
219 -- a bound variable might draw in additional dependencies,
207 -- think: f x = x 0 <-- here, `x' _is_ used
220 -- think: f x = x 0 <-- here, `x' _is_ used
208 P Bound n _ -> var n `ins` unionMap (getDepsTerm vs bs cd) args
221 P Bound n _ -> var n `ins` unionMap (getDepsTerm vs bs cd) args
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)
228+ _ -> error $ "cannot analyse application of: " ++ show fun
210 ins = M.insertWith S.union cd
230 ins = M.insertWith S.union cd
211 var n = fromMaybe (error $ "non-existent bound variable: " ++ show n) (M.lookup n vs)
231 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
218 getDepsTerm vs bs cd Erased = M.empty
238 getDepsTerm vs bs cd Erased = M.empty
219 getDepsTerm vs bs cd Impossible = M.empty
239 getDepsTerm vs bs cd Impossible = M.empty
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
221 unions :: [Deps] -> Deps
249 unions :: [Deps] -> Deps
222 unions = M.unionsWith S.union
250 unions = M.unionsWith S.union