f5aecf7 · Idris-dev · git.iko.soy

git.iko.soy/Idris-dev

Deferred autos

These should be solved after type class resolution - they are intended as 'side conditions' that can be proved independently, so they aren't supposed to influence resolution. Fixes #2549.

commitf5aecf7bb7db4b29b0d827a8460ee098e01f1a2b authorEdwin Brady <ecb10@st-andrews.ac.uk> dateWed 26 Aug 2015, 11:50 (11 years ago) parent81e1962

2 files changed+11−2

compare with master

unifiedsplit

src/Idris/Elab/Term.hs+3−2 src/Idris/ProofSearch.hs+8

src/Idris/Elab/Term.hs+3−2

@@ -71,8 +71,6 @@ build ist info emode opts fn tm

7171 [TIPartial] -> True

7272 _ -> False

7373

74− when (not pattern) $ solveAutos ist fn True

75−

7674 hs <- get_holes

7775 ivs <- get_instances

7876 ptm <- get_term

@@ -92,6 +90,9 @@ build ist info emode opts fn tm

9290 g <- goal

9391 ptm <- get_term

9492 resolveTC' True True 10 g fn ist) ivs

93+

94+ when (not pattern) $ solveAutos ist fn True

95+

9596 tm <- get_term

9697 ctxt <- get_context

9798 probs <- get_probs

src/Idris/ProofSearch.hs+8

@@ -198,12 +198,20 @@ proofSearch rec fromProver ambigok deferonfail maxDepth elab fn nroot psnames hi

198198 return $ and (map (notHole hs) (zip as cs))

199199 Nothing -> fail "Can't happen"

200200

201+ -- if n is a metavariable, and c is a constructor form, we're not ready

202+ -- to run yet

201203 notHole hs (P _ n _, c)

202204 | (P _ cn _, _) <- unApply c,

203205 n `elem` hs && isConName cn (tt_ctxt ist) = False

204206 | Constant _ <- c = not (n `elem` hs)

207+ -- if fa is a metavariable applied to anything, we're not ready to run yet.

208+ notHole hs (fa, c)

209+ | (P _ fn _, args) <- unApply fa = fn `notElem` hs

205210 notHole _ _ = True

206211

212+ inHS hs (P _ n _) = n `elem` hs

213+ isHS _ _ = False

214+

207215 toUN t@(P nt (MN i n) ty)

208216 | ('_':xs) <- str n = t

209217 | otherwise = P nt (UN n) ty