59d07f7 · Idris-dev · git.iko.soy

CHANGELOG+3−1

compare with master

unifiedsplit

@@ -8,13 +8,15 @@ User visible changes:

8* Added ':set' command, with options 'errorcontext' for displaying local

9 variables in scope when a unification error occurs, and 'showimplicits'

10 for displaying elaborated terms in full

11−* Added '--errorcontext' command line swithc

11+* Added '--errorcontext' command line switch

12* Various minor REPL improvements and fixes

13

14Internal changes:

15

16* Normalise before forcing to catch more forceable arguments

17* Types no longer exported in normal form

18+* Try to resolve overloading by inspecting types, rather than full type

19+ checking

18

20

19New in 0.9.2:

21New in 0.9.2:

20-------------

22-------------

idris.cabal+1−1

@@ -78,5 +78,5 @@ Executable idris

78

79 Extensions: MultiParamTypeClasses, FunctionalDependencies,

80 FlexibleInstances, TemplateHaskell

81− ghc-prof-options: -auto-all

81+ ghc-prof-options: -auto-all -caf-all

82 ghc-options: -rtsopts

src/Core/Elaborate.hs+1−2

@@ -439,8 +439,7 @@ tryAll :: [(Elab' aux a, String)] -> Elab' aux a

439tryAll xs = tryAll' [] (cantResolve, 0) (map fst xs)

440 where

441 cantResolve :: Elab' aux a

442− cantResolve = fail $ "Couldn't resolve alternative: "

442+ cantResolve = lift $ tfail $ CantResolveAlts (map snd xs)

443− ++ showSep ", " (map snd xs)

444

443

445 tryAll' :: [Elab' aux a] -> -- successes

444 tryAll' :: [Elab' aux a] -> -- successes

446 (Elab' aux a, Int) -> -- smallest failure

445 (Elab' aux a, Int) -> -- smallest failure

src/Core/TT.hs+2

@@ -48,6 +48,7 @@ data Err = Msg String

48 | NoSuchVariable Name

49 | NotInjective Term Term Term

50 | CantResolve Term

51+ | CantResolveAlts [String]

51 | IncompleteTerm Term

52 | IncompleteTerm Term

52 | UniverseError

53 | UniverseError

53 | ProgramLineComment

54 | ProgramLineComment

@@ -62,6 +63,7 @@ instance Sized Err where

62 size (NoSuchVariable name) = size name

63 size (NoSuchVariable name) = size name

63 size (NotInjective l c r) = size l + size c + size r

64 size (NotInjective l c r) = size l + size c + size r

64 size (CantResolve trm) = size trm

65 size (CantResolve trm) = size trm

66+ size (CantResolveAlts _) = 1

65 size (IncompleteTerm trm) = size trm

67 size (IncompleteTerm trm) = size trm

66 size UniverseError = 1

68 size UniverseError = 1

67 size ProgramLineComment = 1

69 size ProgramLineComment = 1

src/Idris/Delaborate.hs+1

@@ -93,6 +93,7 @@ pshow i (NotInjective p x y) = "Can't verify injectivity of " ++ show (delab i p

93 " when unifying " ++ show (delab i x) ++ " and " ++

94 show (delab i y)

95pshow i (CantResolve c) = "Can't resolve type class " ++ show (delab i c)

96+pshow i (CantResolveAlts as) = "Can't disambiguate name: " ++ showSep ", " as

96pshow i (NoSuchVariable n) = "No such variable " ++ show n

97pshow i (NoSuchVariable n) = "No such variable " ++ show n

97pshow i (IncompleteTerm t) = "Incomplete term " ++ show (delab i t)

98pshow i (IncompleteTerm t) = "Incomplete term " ++ show (delab i t)

98pshow i UniverseError = "Universe inconsistency"

99pshow i UniverseError = "Universe inconsistency"

src/Idris/ElabDecls.hs+2

@@ -389,6 +389,7 @@ elabClause info tcgen (PClause fc fname lhs_in withs rhs_in whereblock)

389 (expandParams decorate newargs decls rhs_in)

390 logLvl 2 (showImp True rhs)

391 ctxt <- getContext -- new context with where block added

392+ logLvl 5 "STARTING CHECK"

392 ((rhs', defer, is), _) <-

393 ((rhs', defer, is), _) <-

393 tclift $ elaborate ctxt (MN 0 "patRHS") clhsty []

394 tclift $ elaborate ctxt (MN 0 "patRHS") clhsty []

394 (do pbinds lhs_tm

395 (do pbinds lhs_tm

@@ -397,6 +398,7 @@ elabClause info tcgen (PClause fc fname lhs_in withs rhs_in whereblock)

397 tt <- get_term

398 tt <- get_term

398 let (tm, ds) = runState (collectDeferred tt) []

399 let (tm, ds) = runState (collectDeferred tt) []

399 return (tm, ds, is))

400 return (tm, ds, is))

401+ logLvl 5 "DONE CHECK"

400 logLvl 2 $ "---> " ++ show rhs'

402 logLvl 2 $ "---> " ++ show rhs'

401 when (not (null defer)) $ iLOG $ "DEFERRED " ++ show defer

403 when (not (null defer)) $ iLOG $ "DEFERRED " ++ show defer

402 def' <- checkDef fc defer

404 def' <- checkDef fc defer

src/Idris/ElabTerm.hs+30−3

@@ -140,9 +140,13 @@ elab ist info pattern tcgen fn tm

140 pimp (MN 0 "P") Placeholder,

141 pexp l, pexp r])

142 elab' ina (PAlternative True as)

143+ = do ty <- goal

144+ ctxt <- get_context

145+ let (tc, _) = unApply ty

146+ let as' = pruneByType tc ctxt as

143− = let as' = pruneAlt as in

147+ let as'' = as' -- pruneAlt as'

144− try (tryAll (zip (map (elab' ina) as') (map showHd as')))

148+ try (tryAll (zip (map (elab' ina) as'') (map showHd as'')))

145− (tryAll (zip (map (elab' ina) as) (map showHd as)))

149+ (tryAll (zip (map (elab' ina) as') (map showHd as')))

146 where showHd (PApp _ h _) = show h

150 where showHd (PApp _ h _) = show h

147 showHd x = show x

151 showHd x = show x

148 elab' ina (PAlternative False as)

152 elab' ina (PAlternative False as)

@@ -356,6 +360,29 @@ pruneAlt xs = map prune xs

356 headIs f (PApp _ f' _) = headIs f f'

360 headIs f (PApp _ f' _) = headIs f f'

357 headIs f _ = True -- keep if it's not an application

361 headIs f _ = True -- keep if it's not an application

358

362

363+-- Rule out alternatives that don't return the same type as the head of the goal

364+-- (If there are none left as a result, do nothing)

365+

366+pruneByType :: Term -> Context -> [PTerm] -> [PTerm]

367+pruneByType (P _ n _) c as

368+ = let as' = filter (headIs n) as in

369+ case as' of

370+ [] -> as

371+ _ -> as'

372+ where

373+ headIs f (PApp _ (PRef _ f') _) = typeHead f f'

374+ headIs f (PApp _ f' _) = headIs f f'

375+ headIs f (PPi _ _ _ sc) = headIs f sc

376+ headIs _ _ = True -- keep if it's not an application

377+

378+ typeHead f f' = case lookupTy Nothing f' c of

379+ [ty] -> case unApply (getRetTy ty) of

380+ (P _ ftyn _, _) -> ftyn == f

381+ _ -> False

382+ _ -> False

383+

384+pruneByType t _ as = as

385+

359trivial :: IState -> ElabD ()

386trivial :: IState -> ElabD ()

360trivial ist = try (do elab ist toplevel False False (MN 0 "tac") (PRefl (FC "prf" 0))

387trivial ist = try (do elab ist toplevel False False (MN 0 "tac") (PRefl (FC "prf" 0))

361 return ())

388 return ())