ilyakooo0/Idris-dev
1
0
Fork 0
mirror of https://github.com/ilyakooo0/Idris-dev.git synced 2024-09-21 22:17:19 +03:00
Code Issues Projects Releases Wiki Activity

Unification fix

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

Fixes #1381
This commit is contained in:
Edwin Brady 2014-07-16 19:49:26 +02:00
parent 6cc18fdee6
commit e6e1ad964a
2 changed files with 15 additions and 7 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

14
src/Idris/Core/ProofState.hs
View File

@ -213,7 +213,8 @@ unify' ctxt env topx topy =
"\nHoles: " ++ show (holes ps)
++ "\nInjective: " ++ show (injective ps)
++ "\n") $
lift $ unify ctxt env topx topy inj (holes ps) while
lift $ unify ctxt env topx topy inj (holes ps)
(map fst (notunified ps)) while
let notu = filter (\ (n, t) -> case t of
P _ _ _ -> False
_ -> n `elem` dont) u
@ -233,6 +234,7 @@ unify' ctxt env topx topy =
(fails ++ problems ps)
(injective ps)
(holes ps)
(map fst (notunified ps))
let (notu', probs_notu) = mergeNotunified env (notu ++ notunified ps)
traceWhen (unifylog ps)
("Now solved: " ++ show ns' ++
@ -869,10 +871,11 @@ updateNotunified ns nu = up nu where
up ((n, t) : nus) = let t' = updateSolved ns t in
((n, t') : up nus)
updateProblems :: Context -> [(Name, TT Name)] -> Fails -> [Name] -> [Name]
-- FIXME: Why not just pass the whole proof state?
updateProblems :: Context -> [(Name, TT Name)] -> Fails -> [Name] -> [Name] -> [Name]
-> ([(Name, TT Name)], Fails)
-- updateProblems ctxt [] ps inj holes = ([], ps)
updateProblems ctxt ns ps inj holes = up ns ps where
updateProblems ctxt ns ps inj holes usupp = up ns ps where
up ns [] = (ns, [])
up ns ((x, y, env, err, while, um) : ps) =
let x' = updateSolved ns x
@ -880,7 +883,7 @@ updateProblems ctxt ns ps inj holes = up ns ps where
err' = updateError ns err
env' = updateEnv ns env in
-- trace ("Updating " ++ show (x',y')) $
case unify ctxt env' x' y' inj holes while of
case unify ctxt env' x' y' inj holes usupp while of
OK (v, []) -> -- trace ("Added " ++ show v ++ " from " ++ show (x', y')) $
up (ns ++ v) ps
e -> -- trace ("Failed " ++ show e) $
@ -921,6 +924,7 @@ processTactic EndUnify ps
ns' = map (\ (n, t) -> (n, updateSolved ns t)) ns
(ns'', probs') = updateProblems (context ps) ns' (problems ps)
(injective ps) (holes ps)
(map fst (notunified ps))
tm' = updateSolved ns'' (pterm ps) in
traceWhen (unifylog ps) ("Dropping holes: " ++ show (map fst ns'')) $
return (ps { pterm = tm',
@ -943,6 +947,7 @@ processTactic UnifyProblems ps
(problems ps)
(injective ps)
(holes ps)
(map fst (notunified ps))
pterm' = updateSolved ns' (pterm ps) in
traceWhen (unifylog ps) ("Dropping holes: " ++ show (map fst ns')) $
return (ps { pterm = pterm', solved = Nothing, problems = probs',
@ -976,6 +981,7 @@ processTactic t ps
[s] (problems ps')
(injective ps')
(holes ps')
(map fst (notunified ps))
_ -> ([], problems ps')
-- rechecking problems may find more solutions, so
-- apply them here

8
src/Idris/Core/Unify.hs
View File

@ -242,9 +242,10 @@ hasv (App f a) = hasv f || hasv a
hasv (Bind x b sc) = hasv (binderTy b) || hasv sc
hasv _ = False
unify :: Context -> Env -> TT Name -> TT Name -> [Name] -> [Name] -> [FailContext] ->
unify :: Context -> Env -> TT Name -> TT Name ->
[Name] -> [Name] -> [Name] -> [FailContext] ->
TC ([(Name, TT Name)], Fails)
unify ctxt env topx topy inj holes from =
unify ctxt env topx topy inj holes usersupp from =
-- traceWhen (hasv topx || hasv topy)
-- ("Unifying " ++ show topx ++ "\nAND\n" ++ show topy ++ "\n") $
-- don't bother if topx and topy are different at the head
@ -497,7 +498,8 @@ unify ctxt env topx topy inj holes from =
_ -> False
metavar t = case t of
P _ x _ -> (x `elem` holes || holeIn env x)
P _ x _ -> (x `notElem` usersupp &&
(x `elem` holes || holeIn env x))
|| globmetavar t
_ -> False
pat t = case t of