f1e61da · Idris-dev · git.iko.soy

CHANGELOG+2

compare with master

unifiedsplit

@@ -9,10 +9,12 @@ User visible changes:

9* Tab completion in REPL

10* Dynamic loading of C libraries in the interpreter

11* Testing IO actions at the REPL with :x command

12+* Fixed some INTERNAL ERROR messages

12

13

13Internal changes:

14Internal changes:

14

15

15* Improved name disambiguation

16* Improved name disambiguation

17+* More flexible unification and elaboration of lambdas

16* Various unification and totality checking bug fixes

18* Various unification and totality checking bug fixes

17

19

18New in 0.9.7:

20New in 0.9.7:

src/Core/Elaborate.hs+17

@@ -469,6 +469,23 @@ apply_elab n args =

469 mkMN n@(UN x) = MN 1000 x

470 mkMN (NS n ns) = NS (mkMN n) ns

471

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

473+checkPiGoal :: Elab' aux ()

474+checkPiGoal = do g <- goal

475+ case g of

476+ Bind _ (Pi _) _ -> return ()

477+ _ -> do a <- unique_hole (MN 0 "argTy")

478+ b <- unique_hole (MN 0 "retTy")

479+ f <- unique_hole (MN 0 "f")

480+ claim a RType

481+ claim b RType

482+ claim f (RBind (MN 0 "aX") (Pi (Var a)) (Var b))

483+ movelast a

484+ movelast b

485+ fill (Var f)

486+ solve

487+ focus f

488+

472simple_app :: Elab' aux () -> Elab' aux () -> Elab' aux ()

489simple_app :: Elab' aux () -> Elab' aux () -> Elab' aux ()

473simple_app fun arg =

490simple_app fun arg =

474 do a <- unique_hole (MN 0 "argTy")

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

src/Idris/ElabTerm.hs+2

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

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

231 ptm <- get_term

232 g <- goal

233+ checkPiGoal

233 attack; intro (Just n);

234 attack; intro (Just n);

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

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

235 elabE (True, a) sc; solve

236 elabE (True, a) sc; solve

@@ -239,6 +240,7 @@ elab ist info pattern tcgen fn tm

239 = do hsin <- get_holes

240 = do hsin <- get_holes

240 ptmin <- get_term

241 ptmin <- get_term

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

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

243+ checkPiGoal

242 claim tyn RType

244 claim tyn RType

243 attack

245 attack

244 ptm <- get_term

246 ptm <- get_term