6924ceb · Idris-dev · git.iko.soy

git.iko.soy/Idris-dev

on master help sign in

Give Pi bindings the proper name when elaborating lambdas

6924cebEdwin Brady13 years ago

src/Core/Elaborate.hs+7−6

compare with master

unifiedsplit

@@ -484,16 +484,17 @@ apply_elab n args =

484 mkMN (NS n ns) = NS (mkMN n) ns

485

486-- If the goal is not a Pi-type, invent some names and make it a pi type

487−checkPiGoal :: Elab' aux ()

487+checkPiGoal :: Name -> Elab' aux ()

488−checkPiGoal = do g <- goal

488+checkPiGoal n

489+ = do g <- goal

489 case g of

490 case g of

490 Bind _ (Pi _) _ -> return ()

491 Bind _ (Pi _) _ -> return ()

491− _ -> do a <- unique_hole (MN 0 "argTy")

492+ _ -> do a <- unique_hole (MN 0 "pargTy")

492− b <- unique_hole (MN 0 "retTy")

493+ b <- unique_hole (MN 0 "pretTy")

493− f <- unique_hole (MN 0 "f")

494+ f <- unique_hole (MN 0 "pf")

494 claim a RType

495 claim a RType

495 claim b RType

496 claim b RType

496− claim f (RBind (MN 0 "aX") (Pi (Var a)) (Var b))

497+ claim f (RBind n (Pi (Var a)) (Var b))

497 movelast a

498 movelast a

498 movelast b

499 movelast b

499 fill (Var f)

500 fill (Var f)

src/Idris/ElabTerm.hs+2−2

@@ -234,7 +234,7 @@ elab ist info pattern tcgen fn tm

234 -- let sc' = mapPT (repN n n') sc

235 ptm <- get_term

236 g <- goal

237− checkPiGoal

237+ checkPiGoal n

238 attack; intro (Just n);

239 -- trace ("------ intro " ++ show n ++ " ---- \n" ++ show ptm)

240 elabE (True, a) sc; solve

@@ -244,7 +244,7 @@ elab ist info pattern tcgen fn tm

244 = do hsin <- get_holes

245 ptmin <- get_term

246 tyn <- unique_hole (MN 0 "lamty")

247− checkPiGoal

247+ checkPiGoal n

248 claim tyn RType

249 attack

250 ptm <- get_term