0140e67 · Idris-dev · git.iko.soy

git.iko.soy/Idris-dev

Tweak to hole lifting

Where the hole has a function type, it should display the whole function type!

commit0140e67bc9b639e7ae88ebd2e835295961750f0b authorEdwin Brady <ecb10@st-andrews.ac.uk> dateMon 17 Aug 2015, 19:10 (11 years ago) parentba3fab0

2 files changed+23−12

compare with master

unifiedsplit

src/Idris/Core/Elaborate.hs+1−1 src/Idris/Interactive.hs+22−11

src/Idris/Core/Elaborate.hs+1−1

@@ -722,7 +722,7 @@ simple_app infer fun arg str =

722722 s <- getNameFrom (sMN 0 "s")

723723 claim a RType

724724 claim b RType

725− claim f (RBind (sMN 0 "aX") (Pi Nothing (Var a) RType) (Var b))

725+ claim f (RBind (sMN 0 "_aX") (Pi Nothing (Var a) RType) (Var b))

726726 tm <- get_term

727727 start_unify s

728728 -- if 'infer' is set, we're assuming it's a simply typed application

src/Idris/Interactive.hs+22−11

@@ -292,12 +292,12 @@ makeLemma fn updatefile l n

292292 let isProv = checkProv tyline (show n)

293293

294294 ctxt <- getContext

295− mty <- case lookupTyName n ctxt of

296− [(_,t)] -> return t

297− [] -> ierror (NoSuchVariable n)

298− ns -> ierror (CantResolveAlts (map fst ns))

295+ (fname, mty) <- case lookupTyName n ctxt of

296+ [t] -> return t

297+ [] -> ierror (NoSuchVariable n)

298+ ns -> ierror (CantResolveAlts (map fst ns))

299299 i <- getIState

300− margs <- case lookup n (idris_metavars i) of

300+ margs <- case lookup fname (idris_metavars i) of

301301 Just (_, arity, _, _) -> return arity

302302 _ -> return (-1)

303303

@@ -308,7 +308,7 @@ makeLemma fn updatefile l n

308308 let lem = show n ++ " : " ++

309309 constraints i classes mty ++

310310 showTmOpts (defaultPPOption { ppopt_pinames = True })

311− (stripMNBind skip (delab i mty))

311+ (stripMNBind skip margs (delab i mty))

312312 let lem_app = show n ++ appArgs skip margs mty

313313

314314 if updatefile then

@@ -351,12 +351,13 @@ makeLemma fn updatefile l n

351351 appArgs skip i (Bind _ (Pi _ _ _) sc) = appArgs skip (i - 1) sc

352352 appArgs skip i _ = ""

353353

354− stripMNBind skip (PPi b n@(UN c) _ ty sc)

355− | (thead c /= '_' && n `notElem` skip) ||

354+ stripMNBind _ args t | args <= 0 = t

355+ stripMNBind skip args (PPi b n@(UN c) _ ty sc)

356+ | n `notElem` skip ||

356357 take 4 (str c) == "__pi" -- keep in type, but not in app

357− = PPi b n NoFC ty (stripMNBind skip sc)

358− stripMNBind skip (PPi b _ _ ty sc) = stripMNBind skip sc

359− stripMNBind skip t = t

358+ = PPi b n NoFC ty (stripMNBind skip (args - 1) sc)

359+ stripMNBind skip args (PPi b _ _ ty sc) = stripMNBind skip (args - 1) sc

360+ stripMNBind skip args t = t

360361

361362 constraints :: IState -> [Name] -> Type -> String

362363 constraints i [] ty = ""

@@ -374,13 +375,23 @@ makeLemma fn updatefile l n

374375 -- or at the top level themselves.

375376 -- Also, make type class instances implicit

376377 guessImps :: IState -> Context -> Term -> [Name]

378+ -- machine names aren't lifted

379+ guessImps ist ctxt (Bind n@(MN _ _) (Pi _ ty _) sc)

380+ = n : guessImps ist ctxt sc

377381 guessImps ist ctxt (Bind n (Pi _ ty _) sc)

378382 | guarded ctxt n (substV (P Bound n Erased) sc)

379383 = n : guessImps ist ctxt sc

380384 | isClass ist ty

381385 = n : guessImps ist ctxt sc

386+ | TType _ <- ty = n : guessImps ist ctxt sc

387+ | ignoreName n = n : guessImps ist ctxt sc

382388 | otherwise = guessImps ist ctxt sc

383389 guessImps ist ctxt _ = []

390+

391+ -- TMP HACK unusable name so don't lift

392+ ignoreName n = case show n of

393+ "_aX" -> True

394+ _ -> False

384395

385396 guessClasses :: IState -> Context -> Term -> [Name]

386397 guessClasses ist ctxt (Bind n (Pi _ ty _) sc)