41f921f · Idris-dev · git.iko.soy

git.iko.soy/Idris-dev

on master help sign in

Unify more things!

41f921fEdwin Brady12 years ago

src/Idris/Core/Elaborate.hs+4−2

compare with master

unifiedsplit

@@ -681,11 +681,13 @@ try' :: Elab' aux a -> Elab' aux a -> Bool -> Elab' aux a

681try' t1 t2 proofSearch

682 = do s <- get

683 ps <- get_probs

684+ ulog <- getUnifyLog

684 case prunStateT 999999 False ps t1 s of

685 case prunStateT 999999 False ps t1 s of

685 OK ((v, _, _), s') -> do put s'

686 OK ((v, _, _), s') -> do put s'

686 return $! v

687 return $! v

688+ Error e1 -> traceWhen ulog ("try failed " ++ show e1) $

687− Error e1 -> if recoverableErr e1 then

689+ if recoverableErr e1 then

688− do case runStateT t2 s of

690+ do case runStateT t2 s of

689 OK (v, s') -> do put s'; return $! v

691 OK (v, s') -> do put s'; return $! v

690 Error e2 -> if score e1 >= score e2

692 Error e2 -> if score e1 >= score e2

691 then lift (tfail e1)

693 then lift (tfail e1)

src/Idris/Core/ProofState.hs+25−7

@@ -180,6 +180,19 @@ match_unify' ctxt env topx topy =

180-- -- ++ show (pterm ps)

181-- ++ "\n----------") $

182

183+mergeSolutions :: Env -> [(Name, TT Name)] -> StateT TState TC [(Name, TT Name)]

184+mergeSolutions env ns = merge [] ns

185+ where

186+ merge acc [] = return (reverse acc)

187+ merge acc ((n, t) : ns)

188+ | Just t' <- lookup n ns

189+ = do ps <- get

190+ let probs = problems ps

191+ put (ps { problems = probs ++ [(t,t',env,Msg "New problem",

192+ [], Unify)] })

193+ merge acc ns

194+ | otherwise = merge ((n, t): acc) ns

195+

183unify' :: Context -> Env -> TT Name -> TT Name ->

196unify' :: Context -> Env -> TT Name -> TT Name ->

184 StateT TState TC [(Name, TT Name)]

197 StateT TState TC [(Name, TT Name)]

185unify' ctxt env topx topy =

198unify' ctxt env topx topy =

@@ -206,17 +219,22 @@ unify' ctxt env topx topy =

206 ++ "\nCurrent problems:\n" ++ qshow (problems ps)

219 ++ "\nCurrent problems:\n" ++ qshow (problems ps)

207-- ++ show (pterm ps)

220-- ++ show (pterm ps)

208 ++ "\n----------") $

221 ++ "\n----------") $

209− do ps <- get

210− let (h, ns) = unified ps

222+ do let (h, ns) = unified ps

223+ -- if a metavar has multiple solutions, make a new unification

224+ -- problem for each.

225+ uns <- mergeSolutions env (u ++ ns)

226+ ps <- get

211− let (ns', probs') = updateProblems (context ps) (u ++ ns)

227+ let (ns', probs') = updateProblems (context ps) uns

212 (fails ++ problems ps)

228 (fails ++ problems ps)

213 (injective ps)

229 (injective ps)

214 (holes ps)

230 (holes ps)

215 let (notu', probs_notu) = mergeNotunified env (notu ++ notunified ps)

231 let (notu', probs_notu) = mergeNotunified env (notu ++ notunified ps)

232+ traceWhen (unifylog ps)

233+ ("Now solved: " ++ show ns') $

216− put (ps { problems = probs' ++ probs_notu,

234+ put (ps { problems = probs' ++ probs_notu,

217− unified = (h, ns'),

235+ unified = (h, ns'),

218− injective = updateInj u (injective ps),

236+ injective = updateInj u (injective ps),

219− notunified = notu' })

237+ notunified = notu' })

220 return u

238 return u

221 where updateInj ((n, a) : us) inj

239 where updateInj ((n, a) : us) inj

222 | (P _ n' _, _) <- unApply a,

240 | (P _ n' _, _) <- unApply a,

src/Idris/ElabTerm.hs+3−1

@@ -66,9 +66,11 @@ build ist info pattern opts fn tm

66 ctxt <- get_context

67 probs <- get_probs

68 u <- getUnifyLog

69+ hs <- get_holes

70 when (not pattern) $

71 when (not pattern) $

72+ traceWhen u ("Remaining holes:\n" ++ show hs ++ "\n" ++

71− traceWhen u ("Remaining problems:\n" ++ show probs) $

73+ "Remaining problems:\n" ++ show probs) $

72 do unify_all; matchProblems True; unifyProblems

74 do unify_all; matchProblems True; unifyProblems

74 probs <- get_probs

76 probs <- get_probs