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

git.iko.soy/Idris-dev

Fix case split/unification bug

If too many underscores to infer, which might have been equal, sometimes unification would solve x for y and y for x simultaneously. In this case, drop one of the solutions.

commit310f04611d1288168b9d2d2b75b2f7a53800f361 authorEdwin Brady <ecb10@st-andrews.ac.uk> dateFri 5 Feb 2016, 14:36 (11 years ago) parent9ecacca

2 files changed+13−3

compare with master

unifiedsplit

src/Idris/CaseSplit.hs+3−2 src/Idris/Core/ProofState.hs+10−1

src/Idris/CaseSplit.hs+3−2

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

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

7878 (map showTmImpls splits))

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

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

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

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

8282 (map (showTmImpls) newPats_in))

8383 newPats_in <- mapM elabNewPat newPats_in

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

227227 i <- getIState

228228 return (True, delab i tm))

229229 (\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

231232 return (False, t))

232233

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

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

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

206206 merge acc ns

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

208208

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+

209217unify' :: Context -> Env ->

210218 (TT Name, Maybe Provenance) ->

211219 (TT Name, Maybe Provenance) ->

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

242250 -- problem for each.

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

244252 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

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

247256 traceWhen (unifylog ps)

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