5eaf1f5 · Idris-dev · git.iko.soy

git.iko.soy/Idris-dev

Cut off fruitless proof search earlier

In particular, trying to unify a function type with a constructor is never going to work, so abandon as an unrecoverable error. This means arity-based unification errors no longer make the elaborator search for ages.

commit5eaf1f5eb82218abffb61668c728e86ced1ff0d3 authorEdwin Brady <ecb10@st-andrews.ac.uk> dateSun 22 Dec 2013, 12:34 (13 years ago) parentc303030

4 files changed+11−3

compare with master

unifiedsplit

src/Core/Elaborate.hs+1−1 src/Core/Unify.hs+6 src/Idris/AbsSyntax.hs+2−2 src/Idris/ElabTerm.hs+2

src/Core/Elaborate.hs+1−1

@@ -601,7 +601,7 @@ try' t1 t2 proofSearch

601601 then lift (tfail e1)

602602 else lift (tfail e2)

603603 else lift (tfail e1)

604− where recoverableErr err@(CantUnify r _ _ _ _ _)

604+ where recoverableErr err@(CantUnify r x y _ _ _)

605605 = -- traceWhen r (show err) $

606606 r || proofSearch

607607 recoverableErr (ProofSearchFail _) = False

src/Core/Unify.hs+6

@@ -508,6 +508,12 @@ recoverable p@(P _ n _) (App f a) = recoverable p f

508508-- recoverable (App f a) p@(P _ _ _) = recoverable f p

509509recoverable (App f a) (App f' a')

510510 = recoverable f f' -- && recoverable a a'

511+recoverable f (Bind _ (Pi _) sc)

512+ | (P (DCon _ _) _ _, _) <- unApply f = False

513+ | (P (TCon _ _) _ _, _) <- unApply f = False

514+recoverable (Bind _ (Pi _) sc) f

515+ | (P (DCon _ _) _ _, _) <- unApply f = False

516+ | (P (TCon _ _) _ _, _) <- unApply f = False

511517recoverable _ _ = True

512518

513519errEnv = map (\(x, b) -> (x, binderTy b))

src/Idris/AbsSyntax.hs+2−2

@@ -135,10 +135,10 @@ getCoercionsTo i ty =

135135 where findCoercions t [] = []

136136 findCoercions t (n : ns) =

137137 let ps = case lookupTy n (tt_ctxt i) of

138− [ty] -> case unApply (getRetTy ty) of

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

139139 (t', _) ->

140140 if t == t' then [n] else []

141− _ -> [] in

141+ _ -> [] in

142142 ps ++ findCoercions t ns

143143

144144addToCG :: Name -> CGInfo -> Idris ()

src/Idris/ElabTerm.hs+2

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

139139-- ++ "\nholes " ++ show hs

140140-- ++ "\nproblems " ++ show ps

141141-- ++ "\n-----------\n") $

142+-- trace ("ELAB " ++ show t') $

142143 elab' ina t'

143144

144145 local f = do e <- get_env

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

208209-- as -> lift $ tfail $ CantResolveAlts (map showHd as)

209210-- trace ("Original " ++ show (length as, as) ++ "\n" ++

210211-- "New " ++ show (length as', as)) $

212+-- traceWhen (length as' > 1) (show as') $

211213 tryAll (zip (map (elab' ina) as') (map showHd as'))

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

213215 showHd x = show x