310f046 · Idris-dev · git.iko.soy

git.iko.soy/Idris-dev

on master help sign in

Fix case split/unification bug

310f046Edwin Brady11 years ago

src/Idris/CaseSplit.hs+3−2

compare with master

unifiedsplit

@@ -77,7 +77,7 @@ split n t'

77 logElab 1 ("New patterns " ++ showSep ", "

78 (map showTmImpls splits))

79 let newPats_in = zipWith (replaceVar ctxt n) splits (repeat t)

80− logElab 4 ("Working from " ++ show t)

80+ logElab 4 ("Working from " ++ showTmImpls t)

81 logElab 4 ("Trying " ++ showSep "\n"

82 (map (showTmImpls) newPats_in))

83 newPats_in <- mapM elabNewPat newPats_in

@@ -227,7 +227,8 @@ elabNewPat t = idrisCatch (do (tm, ty) <- elabVal recinfo ELHS t

227 i <- getIState

228 return (True, delab i tm))

229 (\e -> do i <- getIState

230− logElab 5 $ "Not a valid split:\n" ++ pshow i e

230+ logElab 5 $ "Not a valid split:\n" ++ showTmImpls t ++ "\n"

231+ ++ pshow i e

231 return (False, t))

232 return (False, t))

232

233

233findPats :: IState -> Type -> [PTerm]

234findPats :: IState -> Type -> [PTerm]

src/Idris/Core/ProofState.hs+10−1

@@ -206,6 +206,14 @@ mergeSolutions env ns = merge [] ns

206 merge acc ns

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

208

209+dropSwaps :: [(Name, TT Name)] -> [(Name, TT Name)]

210+dropSwaps [] = []

211+dropSwaps (p@(x, P _ y _) : xs) | solvedIn y x xs = dropSwaps xs

212+ where solvedIn _ _ [] = False

213+ solvedIn y x ((y', P _ x' _) : xs) | y == y' && x == x' = True

214+ solvedIn y x (_ : xs) = solvedIn y x xs

215+dropSwaps (p : xs) = p : dropSwaps xs

216+

209unify' :: Context -> Env ->

217unify' :: Context -> Env ->

210 (TT Name, Maybe Provenance) ->

218 (TT Name, Maybe Provenance) ->

211 (TT Name, Maybe Provenance) ->

219 (TT Name, Maybe Provenance) ->

@@ -242,7 +250,8 @@ unify' ctxt env (topx, xfrom) (topy, yfrom) =

242 -- problem for each.

250 -- problem for each.

243 uns <- mergeSolutions env (u' ++ ns)

251 uns <- mergeSolutions env (u' ++ ns)

244 ps <- get

252 ps <- get

245− let (ns', probs') = updateProblems ps uns (fails ++ problems ps)

253+ let (ns_p, probs') = updateProblems ps uns (fails ++ problems ps)

254+ let ns' = dropSwaps ns_p

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

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

247 traceWhen (unifylog ps)

256 traceWhen (unifylog ps)

248 ("Now solved: " ++ show ns' ++

257 ("Now solved: " ++ show ns' ++