git.iko.soy/Idris-dev
on master help sign in
Make sensible implicit choices in :addlemma

Specifically, make an argument implicit if it's constructor guarded elsewhere in the type (i.e. can be inferred by unification in the usual way).

commit50f63b51743240aaaf49b0f19ad41c7a424fe02c authorEdwin Brady <ecb10@st-andrews.ac.uk> dateMon 12 May 2014, 11:08 (12 years ago) parentf02f3c0
2 files changed+38−12
compare with master
unifiedsplit
src/Idris/AbsSyntax.hs+1−1 src/Idris/Interactive.hs+37−11
src/Idris/AbsSyntax.hs+1−1
@@ -937,7 +937,7 @@ expandParamsD rhsonly ist dec ps ns (PClauses fc opts n cs)
937937 updateps yn nm [] = []
938938 updateps yn nm (((a, t), i):as)
939939 | (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
941941
942942 removeBound lhs ns = ns \\ nub (bnames lhs)
943943
src/Idris/Interactive.hs+37−11
@@ -1,3 +1,5 @@
1+{-# LANGUAGE PatternGuards #-}
2+
13module Idris.Interactive(caseSplitAt, addClauseFrom, addProofClauseFrom,
24 addMissing, makeWith, doProofSearch,
35 makeLemma) where
@@ -228,8 +230,10 @@ makeLemma h fn updatefile l n
228230 ns -> ierror (CantResolveAlts (map show ns))
229231
230232 i <- getIState
231− let lem = show n ++ " : " ++ show (stripMNBind (delab i mty))
232− let lem_app = show n ++ appArgs mty
233+ let skip = guessImps (tt_ctxt i) mty
234+
235+ let lem = show n ++ " : " ++ show (stripMNBind skip (delab i mty))
236+ let lem_app = show n ++ appArgs skip mty
233237
234238 if updatefile then
235239 do let fb = fn ++ "~"
@@ -239,15 +243,37 @@ makeLemma h fn updatefile l n
239243
240244 where getIndent s = length (takeWhile isSpace s)
241245
242− appArgs (Bind n@(UN c) (Pi _) sc)
243− | thead c /= '_' = " " ++ show n ++ appArgs sc
244− appArgs (Bind _ (Pi _) sc) = appArgs sc
245− appArgs _ = ""
246−
247− stripMNBind (PPi b n@(UN c) ty sc)
248− | thead c /= '_' = PPi b n ty (stripMNBind sc)
249− stripMNBind (PPi b _ ty sc) = stripMNBind sc
250− stripMNBind t = t
246+ appArgs skip (Bind n@(UN c) (Pi _) sc)
247+ | thead c /= '_' && n `notElem` skip
248+ = " " ++ show n ++ appArgs skip sc
249+ appArgs skip (Bind _ (Pi _) sc) = appArgs skip sc
250+ appArgs skip _ = ""
251+
252+ stripMNBind skip (PPi b n@(UN c) ty sc)
253+ | thead c /= '_' &&
254+ n `notElem` skip = PPi b n ty (stripMNBind skip sc)
255+ stripMNBind skip (PPi b _ ty sc) = stripMNBind skip sc
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
251277
252278 blank = all isSpace
253279