@@ -27,6 +27,7 @@ import System.IO
27import Data.Char
27import Data.Char
28import Data.Maybe (fromMaybe)
28import Data.Maybe (fromMaybe)
31caseSplitAt :: Handle -> FilePath -> Bool -> Int -> Name -> Idris ()
32caseSplitAt :: Handle -> FilePath -> Bool -> Int -> Name -> Idris ()
32caseSplitAt h fn updatefile l n
33caseSplitAt h fn updatefile l n
@@ -248,12 +249,15 @@ makeLemma h fn updatefile l n
248 [] -> ierror (NoSuchVariable n)
249 [] -> ierror (NoSuchVariable n)
249 ns -> ierror (CantResolveAlts (map fst ns))
250 ns -> ierror (CantResolveAlts (map fst ns))
250 i <- getIState
251 i <- getIState
252+ margs <- case lookup n (idris_metavars i) of
253+ Just (_, arity, _) -> return arity
252 if (not isProv) then do
256 if (not isProv) then do
253 let skip = guessImps (tt_ctxt i) mty
257 let skip = guessImps (tt_ctxt i) mty
255 let lem = show n ++ " : " ++ show (stripMNBind skip (delab i mty))
259 let lem = show n ++ " : " ++ show (stripMNBind skip (delab i mty))
256− let lem_app = show n ++ appArgs skip mty
260+ let lem_app = show n ++ appArgs skip margs mty
258 if updatefile then
262 if updatefile then
259 do let fb = fn ++ "~"
263 do let fb = fn ++ "~"
@@ -271,7 +275,7 @@ makeLemma h fn updatefile l n
271 in runIO . hPutStrLn h $ convSExp "return" good n
275 in runIO . hPutStrLn h $ convSExp "return" good n
273 else do -- provisional definition
277 else do -- provisional definition
274− let lem_app = show n ++ appArgs [] mty ++
278+ let lem_app = show n ++ appArgs [] (-1) mty ++
275 " = ?" ++ show n ++ "_rhs"
279 " = ?" ++ show n ++ "_rhs"
276 if updatefile then
280 if updatefile then
277 do let fb = fn ++ "~"
281 do let fb = fn ++ "~"
@@ -288,15 +292,17 @@ makeLemma h fn updatefile l n
289 where getIndent s = length (takeWhile isSpace s)
293 where getIndent s = length (takeWhile isSpace s)
291− appArgs skip (Bind n@(UN c) (Pi _) sc)
295+ appArgs skip 0 _ = ""
296+ appArgs skip i (Bind n@(UN c) (Pi _) sc)
292− | thead c /= '_' && n `notElem` skip
297+ | (thead c /= '_' && n `notElem` skip)
293− = " " ++ show n ++ appArgs skip sc
298+ = " " ++ show n ++ appArgs skip (i - 1) sc
294− appArgs skip (Bind _ (Pi _) sc) = appArgs skip sc
299+ appArgs skip i (Bind _ (Pi _) sc) = appArgs skip (i - 1) sc
295− appArgs skip _ = ""
300+ appArgs skip i _ = ""
297 stripMNBind skip (PPi b n@(UN c) ty sc)
302 stripMNBind skip (PPi b n@(UN c) ty sc)
298− | thead c /= '_' &&
303+ | (thead c /= '_' && n `notElem` skip) ||
304+ take 4 (str c) == "__pi" -- keep in type, but not in app
299− n `notElem` skip = PPi b n ty (stripMNBind skip sc)
305+ = PPi b n ty (stripMNBind skip sc)
300 stripMNBind skip (PPi b _ ty sc) = stripMNBind skip sc
306 stripMNBind skip (PPi b _ ty sc) = stripMNBind skip sc
301 stripMNBind skip t = t
307 stripMNBind skip t = t