git.iko.soy/Idris-dev
on master help sign in
Make sensible implicit choices in :addlemma
50f63b5Edwin Brady
src/Idris/AbsSyntax.hs+1−1
compare with master
unifiedsplit
@@ -937,7 +937,7 @@ expandParamsD rhsonly ist dec ps ns (PClauses fc opts n cs)
937 updateps yn nm [] = []
937 updateps yn nm [] = []
938 updateps yn nm (((a, t), i):as)
938 updateps yn nm (((a, t), i):as)
939 | (a `elem` nm) == yn = (a, t) : updateps yn nm as
939 | (a `elem` nm) == yn = (a, t) : updateps yn nm as
940− | otherwise = (sMN i (show n ++ "_u"), t) : updateps yn nm as
940+ | otherwise = (sMN i ('_' : show n ++ "_u"), t) : updateps yn nm as
941
941
942 removeBound lhs ns = ns \\ nub (bnames lhs)
942 removeBound lhs ns = ns \\ nub (bnames lhs)
943
943
src/Idris/Interactive.hs+37−11
@@ -1,3 +1,5 @@
1+{-# LANGUAGE PatternGuards #-}
2+
1module Idris.Interactive(caseSplitAt, addClauseFrom, addProofClauseFrom,
3module Idris.Interactive(caseSplitAt, addClauseFrom, addProofClauseFrom,
2 addMissing, makeWith, doProofSearch,
4 addMissing, makeWith, doProofSearch,
3 makeLemma) where
5 makeLemma) where
@@ -228,8 +230,10 @@ makeLemma h fn updatefile l n
228 ns -> ierror (CantResolveAlts (map show ns))
230 ns -> ierror (CantResolveAlts (map show ns))
229
231
230 i <- getIState
232 i <- getIState
233+ let skip = guessImps (tt_ctxt i) mty
234+
231− let lem = show n ++ " : " ++ show (stripMNBind (delab i mty))
235+ let lem = show n ++ " : " ++ show (stripMNBind skip (delab i mty))
232− let lem_app = show n ++ appArgs mty
236+ let lem_app = show n ++ appArgs skip mty
233
237
234 if updatefile then
238 if updatefile then
235 do let fb = fn ++ "~"
239 do let fb = fn ++ "~"
@@ -239,15 +243,37 @@ makeLemma h fn updatefile l n
239
243
240 where getIndent s = length (takeWhile isSpace s)
244 where getIndent s = length (takeWhile isSpace s)
241
245
242− appArgs (Bind n@(UN c) (Pi _) sc)
246+ appArgs skip (Bind n@(UN c) (Pi _) sc)
247+ | thead c /= '_' && n `notElem` skip
243− | thead c /= '_' = " " ++ show n ++ appArgs sc
248+ = " " ++ show n ++ appArgs skip sc
244− appArgs (Bind _ (Pi _) sc) = appArgs sc
249+ appArgs skip (Bind _ (Pi _) sc) = appArgs skip sc
245− appArgs _ = ""
250+ appArgs skip _ = ""
246−
251+
247− stripMNBind (PPi b n@(UN c) ty sc)
252+ stripMNBind skip (PPi b n@(UN c) ty sc)
253+ | thead c /= '_' &&
248− | thead c /= '_' = PPi b n ty (stripMNBind sc)
254+ n `notElem` skip = PPi b n ty (stripMNBind skip sc)
249− stripMNBind (PPi b _ ty sc) = stripMNBind sc
255+ stripMNBind skip (PPi b _ ty sc) = stripMNBind skip sc
250− stripMNBind t = t
256+ stripMNBind skip t = t
257+
258+ -- Guess which binders should be implicits in the generated lemma.
259+ -- Make them implicit if they appear guarded by a top level constructor,
260+ -- or at the top level themselves.
261+ guessImps :: Context -> Term -> [Name]
262+ guessImps ctxt (Bind n (Pi _) sc)
263+ | guarded ctxt n (substV (P Bound n Erased) sc)
264+ = n : guessImps ctxt sc
265+ | otherwise = guessImps ctxt sc
266+ guessImps ctxt _ = []
267+
268+ guarded ctxt n (P _ n' _) | n == n' = True
269+ guarded ctxt n ap@(App _ _)
270+ | (P _ f _, args) <- unApply ap,
271+ isConName f ctxt = any (guarded ctxt n) args
272+-- guarded ctxt n (Bind (UN cn) (Pi t) sc) -- ignore shadows
273+-- | thead cn /= '_' = guarded ctxt n t || guarded ctxt n sc
274+ guarded ctxt n (Bind _ (Pi t) sc)
275+ = guarded ctxt n t || guarded ctxt n sc
276+ guarded ctxt n _ = False
251
277
252 blank = all isSpace
278 blank = all isSpace
253
279