e6e1ad9 · Idris-dev · git.iko.soy

git.iko.soy/Idris-dev

Unification fix

If a variable is already solved with a user's term, don't try to infer a new value for it. Fixes #1381

commite6e1ad964aba1971457af8db963e74bba28d6ea0 authorEdwin Brady <ecb10@st-andrews.ac.uk> dateWed 16 Jul 2014, 19:49 (12 years ago) parent6cc18fd

2 files changed+15−7

compare with master

unifiedsplit

src/Idris/Core/ProofState.hs+10−4 src/Idris/Core/Unify.hs+5−3

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

@@ -213,7 +213,8 @@ unify' ctxt env topx topy =

213213 "\nHoles: " ++ show (holes ps)

214214 ++ "\nInjective: " ++ show (injective ps)

215215 ++ "\n") $

216− lift $ unify ctxt env topx topy inj (holes ps) while

216+ lift $ unify ctxt env topx topy inj (holes ps)

217+ (map fst (notunified ps)) while

217218 let notu = filter (\ (n, t) -> case t of

218219 P _ _ _ -> False

219220 _ -> n `elem` dont) u

@@ -233,6 +234,7 @@ unify' ctxt env topx topy =

233234 (fails ++ problems ps)

234235 (injective ps)

235236 (holes ps)

237+ (map fst (notunified ps))

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

237239 traceWhen (unifylog ps)

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

@@ -869,10 +871,11 @@ updateNotunified ns nu = up nu where

869871 up ((n, t) : nus) = let t' = updateSolved ns t in

870872 ((n, t') : up nus)

871873

872−updateProblems :: Context -> [(Name, TT Name)] -> Fails -> [Name] -> [Name]

874+-- FIXME: Why not just pass the whole proof state?

875+updateProblems :: Context -> [(Name, TT Name)] -> Fails -> [Name] -> [Name] -> [Name]

873876 -> ([(Name, TT Name)], Fails)

874877-- updateProblems ctxt [] ps inj holes = ([], ps)

875−updateProblems ctxt ns ps inj holes = up ns ps where

878+updateProblems ctxt ns ps inj holes usupp = up ns ps where

876879 up ns [] = (ns, [])

877880 up ns ((x, y, env, err, while, um) : ps) =

878881 let x' = updateSolved ns x

@@ -880,7 +883,7 @@ updateProblems ctxt ns ps inj holes = up ns ps where

880883 err' = updateError ns err

881884 env' = updateEnv ns env in

882885-- trace ("Updating " ++ show (x',y')) $

883− case unify ctxt env' x' y' inj holes while of

886+ case unify ctxt env' x' y' inj holes usupp while of

884887 OK (v, []) -> -- trace ("Added " ++ show v ++ " from " ++ show (x', y')) $

885888 up (ns ++ v) ps

886889 e -> -- trace ("Failed " ++ show e) $

@@ -921,6 +924,7 @@ processTactic EndUnify ps

921924 ns' = map (\ (n, t) -> (n, updateSolved ns t)) ns

922925 (ns'', probs') = updateProblems (context ps) ns' (problems ps)

923926 (injective ps) (holes ps)

927+ (map fst (notunified ps))

924928 tm' = updateSolved ns'' (pterm ps) in

925929 traceWhen (unifylog ps) ("Dropping holes: " ++ show (map fst ns'')) $

926930 return (ps { pterm = tm',

@@ -943,6 +947,7 @@ processTactic UnifyProblems ps

943947 (problems ps)

944948 (injective ps)

945949 (holes ps)

950+ (map fst (notunified ps))

946951 pterm' = updateSolved ns' (pterm ps) in

947952 traceWhen (unifylog ps) ("Dropping holes: " ++ show (map fst ns')) $

948953 return (ps { pterm = pterm', solved = Nothing, problems = probs',

@@ -976,6 +981,7 @@ processTactic t ps

976981 [s] (problems ps')

977982 (injective ps')

978983 (holes ps')

984+ (map fst (notunified ps))

979985 _ -> ([], problems ps')

980986 -- rechecking problems may find more solutions, so

981987 -- apply them here

src/Idris/Core/Unify.hs+5−3

@@ -242,9 +242,10 @@ hasv (App f a) = hasv f || hasv a

242242hasv (Bind x b sc) = hasv (binderTy b) || hasv sc

243243hasv _ = False

244244

245−unify :: Context -> Env -> TT Name -> TT Name -> [Name] -> [Name] -> [FailContext] ->

245+unify :: Context -> Env -> TT Name -> TT Name ->

246+ [Name] -> [Name] -> [Name] -> [FailContext] ->

246247 TC ([(Name, TT Name)], Fails)

247−unify ctxt env topx topy inj holes from =

248+unify ctxt env topx topy inj holes usersupp from =

248249-- traceWhen (hasv topx || hasv topy)

249250-- ("Unifying " ++ show topx ++ "\nAND\n" ++ show topy ++ "\n") $

250251 -- don't bother if topx and topy are different at the head

@@ -497,7 +498,8 @@ unify ctxt env topx topy inj holes from =

497498 _ -> False

498499

499500 metavar t = case t of

500− P _ x _ -> (x `elem` holes || holeIn env x)

501+ P _ x _ -> (x `notElem` usersupp &&

502+ (x `elem` holes || holeIn env x))

501503 || globmetavar t

502504 _ -> False

503505 pat t = case t of