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

git.iko.soy/Idris-dev

Give Pi bindings the proper name when elaborating lambdas

Fixes #360

commit6924ceb4459581466438ac34fea42ee6b47d7e05 authorEdwin Brady <ecb10@st-andrews.ac.uk> dateThu 4 Jul 2013, 19:44 (13 years ago) parentdad12e6

2 files changed+9−8

compare with master

unifiedsplit

src/Core/Elaborate.hs+7−6 src/Idris/ElabTerm.hs+2−2

src/Core/Elaborate.hs+7−6

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

484484 mkMN (NS n ns) = NS (mkMN n) ns

485485

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

487−checkPiGoal :: Elab' aux ()

488−checkPiGoal = do g <- goal

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

488+checkPiGoal n

489+ = do g <- goal

489490 case g of

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

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

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

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

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

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

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

494495 claim a RType

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

497498 movelast a

498499 movelast b

499500 fill (Var f)

src/Idris/ElabTerm.hs+2−2

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

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

235235 ptm <- get_term

236236 g <- goal

237− checkPiGoal

237+ checkPiGoal n

238238 attack; intro (Just n);

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

240240 elabE (True, a) sc; solve

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

244244 = do hsin <- get_holes

245245 ptmin <- get_term

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

247− checkPiGoal

247+ checkPiGoal n

248248 claim tyn RType

249249 attack

250250 ptm <- get_term