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

git.iko.soy/Idris-dev

on master help sign in

Tweak to hole lifting

0140e67Edwin Brady11 years ago

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

compare with master

unifiedsplit

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

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

723 claim a RType

724 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))

726 tm <- get_term

727 start_unify s

728 -- 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

292 let isProv = checkProv tyline (show n)

293

294 ctxt <- getContext

295− mty <- case lookupTyName n ctxt of

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

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

296+ [t] -> return t

297− [] -> ierror (NoSuchVariable n)

297+ [] -> ierror (NoSuchVariable n)

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

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

299 i <- getIState

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

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

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

302 _ -> return (-1)

303

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

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

309 constraints i classes mty ++

310 showTmOpts (defaultPPOption { ppopt_pinames = True })

311− (stripMNBind skip (delab i mty))

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

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

313

314 if updatefile then

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

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

352 appArgs skip i _ = ""

353

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

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

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

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

356+ | n `notElem` skip ||

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

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

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

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

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

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

359− stripMNBind skip t = t

360+ stripMNBind skip args t = t

360

361

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

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

362 constraints i [] ty = ""

363 constraints i [] ty = ""

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

374 -- or at the top level themselves.

375 -- or at the top level themselves.

375 -- Also, make type class instances implicit

376 -- Also, make type class instances implicit

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

377 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

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

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

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

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

379 = n : guessImps ist ctxt sc

383 = n : guessImps ist ctxt sc

380 | isClass ist ty

384 | isClass ist ty

381 = n : guessImps ist ctxt sc

385 = n : guessImps ist ctxt sc

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

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

382 | otherwise = guessImps ist ctxt sc

388 | otherwise = guessImps ist ctxt sc

383 guessImps ist ctxt _ = []

389 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

384

395

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

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

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

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