f5aecf7 · Idris-dev · git.iko.soy

git.iko.soy/Idris-dev

on master help sign in

Deferred autos

f5aecf7Edwin Brady11 years ago

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

compare with master

unifiedsplit

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

71 [TIPartial] -> True

72 _ -> False

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

75−

76 hs <- get_holes

74 hs <- get_holes

77 ivs <- get_instances

75 ivs <- get_instances

78 ptm <- get_term

76 ptm <- get_term

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

92 g <- goal

90 g <- goal

93 ptm <- get_term

91 ptm <- get_term

94 resolveTC' True True 10 g fn ist) ivs

92 resolveTC' True True 10 g fn ist) ivs

93+

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

95+

95 tm <- get_term

96 tm <- get_term

96 ctxt <- get_context

97 ctxt <- get_context

97 probs <- get_probs

98 probs <- get_probs

src/Idris/ProofSearch.hs+8

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

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

199 Nothing -> fail "Can't happen"

200

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

202+ -- to run yet

201 notHole hs (P _ n _, c)

203 notHole hs (P _ n _, c)

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

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

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

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

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

206 | 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

205 notHole _ _ = True

210 notHole _ _ = True

206

211

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

213+ isHS _ _ = False

214+

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

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

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

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

209 | otherwise = P nt (UN n) ty

217 | otherwise = P nt (UN n) ty