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

git.iko.soy/Idris-dev

Quicker resolution of overloaded names

By checking the name's type against the goal type rather than fully checking.

commit59d07f7aee34a81e60eb3784ff18720a599ce65c authorEdwin Brady <eb@cs.st-andrews.ac.uk> dateFri 15 Jun 2012, 16:07 (14 years ago) parentfe4997e

7 files changed+40−7

compare with master

unifiedsplit

CHANGELOG+3−1 idris.cabal+1−1 src/Core/Elaborate.hs+1−2 src/Core/TT.hs+2 src/Idris/Delaborate.hs+1 src/Idris/ElabDecls.hs+2 src/Idris/ElabTerm.hs+30−3

CHANGELOG+3−1

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

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

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

1010 for displaying elaborated terms in full

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

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

1212* Various minor REPL improvements and fixes

1313

1414Internal changes:

1515

1616* Normalise before forcing to catch more forceable arguments

1717* Types no longer exported in normal form

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

19+ checking

1820

1921New in 0.9.2:

2022-------------

idris.cabal+1−1

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

7878

7979 Extensions: MultiParamTypeClasses, FunctionalDependencies,

8080 FlexibleInstances, TemplateHaskell

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

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

8282 ghc-options: -rtsopts

src/Core/Elaborate.hs+1−2

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

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

440440 where

441441 cantResolve :: Elab' aux a

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

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

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

444443

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

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

src/Core/TT.hs+2

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

4848 | NoSuchVariable Name

4949 | NotInjective Term Term Term

5050 | CantResolve Term

51+ | CantResolveAlts [String]

5152 | IncompleteTerm Term

5253 | UniverseError

5354 | ProgramLineComment

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

6263 size (NoSuchVariable name) = size name

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

6465 size (CantResolve trm) = size trm

66+ size (CantResolveAlts _) = 1

6567 size (IncompleteTerm trm) = size trm

6668 size UniverseError = 1

6769 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

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

9494 show (delab i y)

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

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

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

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

9899pshow 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)

389389 (expandParams decorate newargs decls rhs_in)

390390 logLvl 2 (showImp True rhs)

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

392+ logLvl 5 "STARTING CHECK"

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

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

394395 (do pbinds lhs_tm

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

397398 tt <- get_term

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

399400 return (tm, ds, is))

401+ logLvl 5 "DONE CHECK"

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

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

402404 def' <- checkDef fc defer

src/Idris/ElabTerm.hs+30−3

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

140140 pimp (MN 0 "P") Placeholder,

141141 pexp l, pexp r])

142142 elab' ina (PAlternative True as)

143− = let as' = pruneAlt as in

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

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

143+ = do ty <- goal

144+ ctxt <- get_context

145+ let (tc, _) = unApply ty

146+ let as' = pruneByType tc ctxt as

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

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

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

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

147151 showHd x = show x

148152 elab' ina (PAlternative False as)

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

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

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

358362

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+

359386trivial :: IState -> ElabD ()

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

361388 return ())