Skip to content
Browse files

Quicker resolution of overloaded names

By checking the name's type against the goal type rather than fully
checking.
  • Loading branch information...
1 parent fe4997e commit 59d07f7aee34a81e60eb3784ff18720a599ce65c Edwin Brady committed
Showing with 40 additions and 7 deletions.
  1. +3 −1 CHANGELOG
  2. +1 −1 idris.cabal
  3. +1 −2 src/Core/Elaborate.hs
  4. +2 −0 src/Core/TT.hs
  5. +1 −0 src/Idris/Delaborate.hs
  6. +2 −0 src/Idris/ElabDecls.hs
  7. +30 −3 src/Idris/ElabTerm.hs
View
4 CHANGELOG
@@ -8,13 +8,15 @@ User visible changes:
* Added ':set' command, with options 'errorcontext' for displaying local
variables in scope when a unification error occurs, and 'showimplicits'
for displaying elaborated terms in full
-* Added '--errorcontext' command line swithc
+* Added '--errorcontext' command line switch
* Various minor REPL improvements and fixes
Internal changes:
* Normalise before forcing to catch more forceable arguments
* Types no longer exported in normal form
+* Try to resolve overloading by inspecting types, rather than full type
+ checking
New in 0.9.2:
-------------
View
2 idris.cabal
@@ -78,5 +78,5 @@ Executable idris
Extensions: MultiParamTypeClasses, FunctionalDependencies,
FlexibleInstances, TemplateHaskell
- ghc-prof-options: -auto-all
+ ghc-prof-options: -auto-all -caf-all
ghc-options: -rtsopts
View
3 src/Core/Elaborate.hs
@@ -439,8 +439,7 @@ tryAll :: [(Elab' aux a, String)] -> Elab' aux a
tryAll xs = tryAll' [] (cantResolve, 0) (map fst xs)
where
cantResolve :: Elab' aux a
- cantResolve = fail $ "Couldn't resolve alternative: "
- ++ showSep ", " (map snd xs)
+ cantResolve = lift $ tfail $ CantResolveAlts (map snd xs)
tryAll' :: [Elab' aux a] -> -- successes
(Elab' aux a, Int) -> -- smallest failure
View
2 src/Core/TT.hs
@@ -48,6 +48,7 @@ data Err = Msg String
| NoSuchVariable Name
| NotInjective Term Term Term
| CantResolve Term
+ | CantResolveAlts [String]
| IncompleteTerm Term
| UniverseError
| ProgramLineComment
@@ -62,6 +63,7 @@ instance Sized Err where
size (NoSuchVariable name) = size name
size (NotInjective l c r) = size l + size c + size r
size (CantResolve trm) = size trm
+ size (CantResolveAlts _) = 1
size (IncompleteTerm trm) = size trm
size UniverseError = 1
size ProgramLineComment = 1
View
1 src/Idris/Delaborate.hs
@@ -93,6 +93,7 @@ pshow i (NotInjective p x y) = "Can't verify injectivity of " ++ show (delab i p
" when unifying " ++ show (delab i x) ++ " and " ++
show (delab i y)
pshow i (CantResolve c) = "Can't resolve type class " ++ show (delab i c)
+pshow i (CantResolveAlts as) = "Can't disambiguate name: " ++ showSep ", " as
pshow i (NoSuchVariable n) = "No such variable " ++ show n
pshow i (IncompleteTerm t) = "Incomplete term " ++ show (delab i t)
pshow i UniverseError = "Universe inconsistency"
View
2 src/Idris/ElabDecls.hs
@@ -389,6 +389,7 @@ elabClause info tcgen (PClause fc fname lhs_in withs rhs_in whereblock)
(expandParams decorate newargs decls rhs_in)
logLvl 2 (showImp True rhs)
ctxt <- getContext -- new context with where block added
+ logLvl 5 "STARTING CHECK"
((rhs', defer, is), _) <-
tclift $ elaborate ctxt (MN 0 "patRHS") clhsty []
(do pbinds lhs_tm
@@ -397,6 +398,7 @@ elabClause info tcgen (PClause fc fname lhs_in withs rhs_in whereblock)
tt <- get_term
let (tm, ds) = runState (collectDeferred tt) []
return (tm, ds, is))
+ logLvl 5 "DONE CHECK"
logLvl 2 $ "---> " ++ show rhs'
when (not (null defer)) $ iLOG $ "DEFERRED " ++ show defer
def' <- checkDef fc defer
View
33 src/Idris/ElabTerm.hs
@@ -140,9 +140,13 @@ elab ist info pattern tcgen fn tm
pimp (MN 0 "P") Placeholder,
pexp l, pexp r])
elab' ina (PAlternative True as)
- = let as' = pruneAlt as in
- try (tryAll (zip (map (elab' ina) as') (map showHd as')))
- (tryAll (zip (map (elab' ina) as) (map showHd as)))
+ = do ty <- goal
+ ctxt <- get_context
+ let (tc, _) = unApply ty
+ let as' = pruneByType tc ctxt as
+ let as'' = as' -- pruneAlt as'
+ try (tryAll (zip (map (elab' ina) as'') (map showHd as'')))
+ (tryAll (zip (map (elab' ina) as') (map showHd as')))
where showHd (PApp _ h _) = show h
showHd x = show x
elab' ina (PAlternative False as)
@@ -356,6 +360,29 @@ pruneAlt xs = map prune xs
headIs f (PApp _ f' _) = headIs f f'
headIs f _ = True -- keep if it's not an application
+-- Rule out alternatives that don't return the same type as the head of the goal
+-- (If there are none left as a result, do nothing)
+
+pruneByType :: Term -> Context -> [PTerm] -> [PTerm]
+pruneByType (P _ n _) c as
+ = let as' = filter (headIs n) as in
+ case as' of
+ [] -> as
+ _ -> as'
+ where
+ headIs f (PApp _ (PRef _ f') _) = typeHead f f'
+ headIs f (PApp _ f' _) = headIs f f'
+ headIs f (PPi _ _ _ sc) = headIs f sc
+ headIs _ _ = True -- keep if it's not an application
+
+ typeHead f f' = case lookupTy Nothing f' c of
+ [ty] -> case unApply (getRetTy ty) of
+ (P _ ftyn _, _) -> ftyn == f
+ _ -> False
+ _ -> False
+
+pruneByType t _ as = as
+
trivial :: IState -> ElabD ()
trivial ist = try (do elab ist toplevel False False (MN 0 "tac") (PRefl (FC "prf" 0))
return ())

0 comments on commit 59d07f7

Please sign in to comment.
Something went wrong with that request. Please try again.