@@ -25,11 +25,13 @@ import Data.Maybe
2525import Debug.Trace
2626
2727-- | Data type representing binding-time annotations for partial evaluation of arguments
28−data PEArgType = ImplicitS -- ^ Implicit static argument
29− | ImplicitD -- ^ Implicit dynamic argument
30− | ExplicitS -- ^ Explicit static argument
31− | ExplicitD -- ^ Explicit dynamic argument
32− | UnifiedD -- ^ Erasable dynamic argument (found under unification)
28+data PEArgType = ImplicitS Name -- ^ Implicit static argument
29+ | ImplicitD Name -- ^ Implicit dynamic argument
30+ | ConstraintS -- ^ Implementation constraint
31+ | ConstraintD -- ^ Implementation constraint
32+ | ExplicitS -- ^ Explicit static argument
33+ | ExplicitD -- ^ Explicit dynamic argument
34+ | UnifiedD -- ^ Erasable dynamic argument (found under unification)
3335 deriving (Eq, Show)
3436
3537-- | A partially evaluated function. pe_app captures the lhs of the
@@ -97,7 +99,9 @@ specType args ty = let (t, args') = runState (unifyEq args ty) [] in
9799 -- of expecting it as a function argument
98100 st ((ExplicitS, v) : xs) (Bind n (Pi _ t _) sc)
99101 = Bind n (Let t v) (st xs sc)
100− st ((ImplicitS, v) : xs) (Bind n (Pi _ t _) sc)
102+ st ((ImplicitS _, v) : xs) (Bind n (Pi _ t _) sc)
103+ = Bind n (Let t v) (st xs sc)
104+ st ((ConstraintS, v) : xs) (Bind n (Pi _ t _) sc)
101105 = Bind n (Let t v) (st xs sc)
102106 -- Erase argument from function type
103107 st ((UnifiedD, _) : xs) (Bind n (Pi _ t _) sc)
@@ -109,7 +113,7 @@ specType args ty = let (t, args') = runState (unifyEq args ty) [] in
109113
110114 -- Erase implicit dynamic argument if existing argument shares it value,
111115 -- by substituting the value of previous argument
112− unifyEq (imp@(ImplicitD, v) : xs) (Bind n (Pi i t k) sc)
116+ unifyEq (imp@(ImplicitD _, v) : xs) (Bind n (Pi i t k) sc)
113117 = do amap <- get
114118 case lookup imp amap of
115119 Just n' ->
@@ -139,11 +143,12 @@ mkPE_TyDecl ist args ty = mkty args ty
139143 where
140144 mkty ((ExplicitD, v) : xs) (Bind n (Pi _ t k) sc)
141145 = PPi expl n NoFC (delab ist (generaliseIn t)) (mkty xs sc)
142− mkty ((ImplicitD, v) : xs) (Bind n (Pi _ t k) sc)
146+ mkty ((ConstraintD, v) : xs) (Bind n (Pi _ t k) sc)
143147 | concreteInterface ist t = mkty xs sc
144148 | interfaceConstraint ist t
145149 = PPi constraint n NoFC (delab ist (generaliseIn t)) (mkty xs sc)
146− | otherwise = PPi impl n NoFC (delab ist (generaliseIn t)) (mkty xs sc)
150+ mkty ((ImplicitD _, v) : xs) (Bind n (Pi _ t k) sc)
151+ = PPi impl n NoFC (delab ist (generaliseIn t)) (mkty xs sc)
147152
148153 mkty (_ : xs) t
149154 = mkty xs t
@@ -200,7 +205,8 @@ mkNewPats ist d ns newname sname lhs rhs | all dynVar (map fst d)
200205 (_, args) -> dynArgs ns args
201206 dynArgs _ [] = True -- can definitely reduce from here
202207 -- if Static, doesn't matter what the argument is
203− dynArgs ((ImplicitS, _) : ns) (a : as) = dynArgs ns as
208+ dynArgs ((ImplicitS _, _) : ns) (a : as) = dynArgs ns as
209+ dynArgs ((ConstraintS, _) : ns) (a : as) = dynArgs ns as
204210 dynArgs ((ExplicitS, _) : ns) (a : as) = dynArgs ns as
205211 -- if Dynamic, it had better be a variable or we'll need to
206212 -- do some more work
@@ -209,7 +215,7 @@ mkNewPats ist d ns newname sname lhs rhs | all dynVar (map fst d)
209215 dynArgs _ _ = False -- and now we'll get stuck
210216
211217mkNewPats ist d ns newname sname lhs rhs =
212− PEDecl lhs rhs (map mkClause d) False
218+ PEDecl lhs rhs (map mkClause d) False
213219 where
214220 mkClause :: (Term, Term) -> (PTerm, PTerm)
215221 mkClause (oldlhs, oldrhs)
@@ -221,25 +227,37 @@ mkNewPats ist d ns newname sname lhs rhs =
221227 (lhs, rhs)
222228
223229 mkLHSargs _ [] _ = []
224− -- dynamics don't appear if they're implicit
230+ -- dynamics don't appear on the LHS if they're implicit
225231 mkLHSargs sub ((ExplicitD, t) : ns) (a : as)
226232 = pexp (delab ist (substNames sub a)) : mkLHSargs sub ns as
227− mkLHSargs sub ((ImplicitD, _) : ns) (a : as)
228− = mkLHSargs sub ns as
233+ mkLHSargs sub ((ImplicitD n, t) : ns) (a : as)
234+ = pimp n (delab ist (substNames sub a)) True : mkLHSargs sub ns as
235+ mkLHSargs sub ((ConstraintD, t) : ns) (a : as)
236+ = pconst (delab ist (substNames sub a)) : mkLHSargs sub ns as
229237 mkLHSargs sub ((UnifiedD, _) : ns) (a : as)
230238 = mkLHSargs sub ns as
231239 -- statics get dropped in any case
232− mkLHSargs sub ((ImplicitS, t) : ns) (a : as)
240+ mkLHSargs sub ((ImplicitS _, t) : ns) (a : as)
233241 = mkLHSargs (extend a t sub) ns as
234242 mkLHSargs sub ((ExplicitS, t) : ns) (a : as)
235243 = mkLHSargs (extend a t sub) ns as
244+ mkLHSargs sub ((ConstraintS, t) : ns) (a : as)
245+ = mkLHSargs (extend a t sub) ns as
236246 mkLHSargs sub _ [] = [] -- no more LHS
237247
238248 extend (P _ n _) t sub = (n, t) : sub
239249 extend _ _ sub = sub
240250
251+ --- 'as' are the LHS arguments
241252 mkRHSargs ((ExplicitS, t) : ns) as = pexp (delab ist t) : mkRHSargs ns as
242253 mkRHSargs ((ExplicitD, t) : ns) (a : as) = a : mkRHSargs ns as
254+ -- Keep the implicits on the RHS, in case they got matched on
255+ mkRHSargs ((ImplicitD n, t) : ns) (a : as) = a : mkRHSargs ns as
256+ mkRHSargs ((ImplicitS n, t) : ns) as -- Dropped from LHS
257+ = pimp n (delab ist t) True : mkRHSargs ns as
258+ mkRHSargs ((ConstraintD, t) : ns) (a : as) = a : mkRHSargs ns as
259+ mkRHSargs ((ConstraintS, t) : ns) as -- Dropped from LHS
260+ = pconst (delab ist t) : mkRHSargs ns as
243261 mkRHSargs (_ : ns) as = mkRHSargs ns as
244262 mkRHSargs _ _ = []
245263
@@ -254,12 +272,26 @@ mkNewPats ist d ns newname sname lhs rhs =
254272mkPE_TermDecl :: IState
255273 -> Name
256274 -> Name
275+ -> PTerm -- ^ Type of specialised function
257276 -> [(PEArgType, Term)]
258277 -> PEDecl
259−mkPE_TermDecl ist newname sname ns
260− = let lhs = PApp emptyFC (PRef emptyFC [] newname) (map pexp (mkp ns))
261− rhs = eraseImps $ delab ist (mkApp (P Ref sname Erased) (map snd ns))
262− patdef = lookupCtxtExact sname (idris_patdefs ist)
278+mkPE_TermDecl ist newname sname specty ns
279+ {- We need to erase the *dynamic* arguments
280+ where their *name* appears in the *type* of a later argument
281+ in specty.
282+ i.e. if a later dynamic argument depends on an earlier dynamic
283+ argument, we should infer the earlier one.
284+ Then we need to erase names from the LHS which no longer appear
285+ on the RHS.
286+ -}
287+ = let deps = getDepNames (eraseRet specty)
288+ lhs = eraseDeps deps $
289+ PApp emptyFC (PRef emptyFC [] newname) (mkp ns)
290+ rhs = eraseDeps deps $
291+ delab ist (mkApp (P Ref sname Erased) (map snd ns))
292+ patdef = -- trace (showTmImpls specty ++ "\n" ++ showTmImpls lhs ++ "\n"
293+ -- ++ showTmImpls rhs) $
294+ lookupCtxtExact sname (idris_patdefs ist)
263295 newpats = case patdef of
264296 Nothing -> PEDecl lhs rhs [(lhs, rhs)] True
265297 Just d -> mkNewPats ist (getPats d) ns
@@ -268,17 +300,28 @@ mkPE_TermDecl ist newname sname ns
268300
269301 getPats (ps, _) = map (\(_, lhs, rhs) -> (lhs, rhs)) ps
270302
303+ eraseRet (PPi p n fc ty sc) = PPi p n fc ty (eraseRet sc)
304+ eraseRet _ = Placeholder
305+
306+ -- Get names used in later arguments; assume we've called eraseRet so there's
307+ -- no names going to appear in return type
308+ getDepNames (PPi _ n _ _ sc)
309+ | n `elem` allNamesIn sc = n : getDepNames sc
310+ | otherwise = getDepNames sc
311+ getDepNames tm = []
312+
271313 mkp [] = []
272− mkp ((ExplicitD, tm) : tms) = delab ist tm : mkp tms
314+ mkp ((ExplicitD, tm) : tms) = pexp (delab ist tm) : mkp tms
315+ mkp ((ImplicitD n, tm) : tms) = pimp n (delab ist tm) True : mkp tms
273316 mkp (_ : tms) = mkp tms
274317
275− eraseImps tm = mapPT deImp tm
318+ eraseDeps ns tm = mapPT (deImp ns) tm
276319
277− deImp (PApp fc t as) = PApp fc t (map deImpArg as)
278− deImp t = t
320+ deImp ns (PApp fc t as) = PApp fc t (map (deImpArg ns) as)
321+ deImp ns t = t
279322
280− deImpArg a@(PImp _ _ _ _ _) = a { getTm = Placeholder }
281− deImpArg a = a
323+ deImpArg ns a | pname a `elem` ns = a { getTm = Placeholder }
324+ | otherwise = a
282325
283326-- | Get specialised applications for a given function
284327getSpecApps :: IState
@@ -290,14 +333,22 @@ getSpecApps ist env tm = ga env (explicitNames tm) where
290333-- staticArg env True _ tm@(P _ n _) _ | n `elem` env = Just (True, tm)
291334-- staticArg env True _ tm@(App f a) _ | (P _ n _, args) <- unApply tm,
292335-- n `elem` env = Just (True, tm)
293− staticArg env x imp tm n
294− | x && imparg imp = (ImplicitS, tm)
295− | x = (ExplicitS, tm)
296− | imparg imp = (ImplicitD, tm)
336+ staticArg env True imp tm n
337+ | Just n <- imparg imp = (ImplicitS n, tm)
338+ | constrarg imp = (ConstraintS, tm)
339+ | otherwise = (ExplicitS, tm)
340+
341+ staticArg env False imp tm n
342+ | Just nm <- imparg imp = (ImplicitD nm, (P Ref (sUN (show n ++ "arg")) Erased))
343+ | constrarg imp = (ConstraintD, tm)
297344 | otherwise = (ExplicitD, (P Ref (sUN (show n ++ "arg")) Erased))
298345
299− imparg (PExp _ _ _ _) = False
300− imparg _ = True
346+ imparg (PExp _ _ _ _) = Nothing
347+ imparg (PConstraint _ _ _ _) = Nothing
348+ imparg arg = Just (pname arg)
349+
350+ constrarg (PConstraint _ _ _ _) = True
351+ constrarg arg = False
301352
302353 buildApp env [] [] _ _ = []
303354 buildApp env (s:ss) (i:is) (a:as) (n:ns)