e6e1ad9 · Idris-dev · git.iko.soy

git.iko.soy/Idris-dev

on master help sign in

Unification fix

e6e1ad9Edwin Brady12 years ago

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

compare with master

unifiedsplit

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

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

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

215 ++ "\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

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

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

218 P _ _ _ -> False

219 P _ _ _ -> False

219 _ -> n `elem` dont) u

220 _ -> n `elem` dont) u

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

233 (fails ++ problems ps)

234 (fails ++ problems ps)

234 (injective ps)

235 (injective ps)

235 (holes ps)

236 (holes ps)

237+ (map fst (notunified ps))

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

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

237 traceWhen (unifylog ps)

239 traceWhen (unifylog ps)

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

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

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

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

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

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

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

871

873

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

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

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

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

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

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

877-- 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

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

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

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

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

878 let x' = updateSolved ns x

881 let x' = updateSolved ns x

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

880 err' = updateError ns err

883 err' = updateError ns err

881 env' = updateEnv ns env in

884 env' = updateEnv ns env in

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

885-- 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

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

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

885 up (ns ++ v) ps

888 up (ns ++ v) ps

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

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

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

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

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

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

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

923 (injective ps) (holes ps)

926 (injective ps) (holes ps)

927+ (map fst (notunified ps))

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

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

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

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

926 return (ps { pterm = tm',

930 return (ps { pterm = tm',

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

943 (problems ps)

947 (problems ps)

944 (injective ps)

948 (injective ps)

945 (holes ps)

949 (holes ps)

950+ (map fst (notunified ps))

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

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

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

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

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

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

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

976 [s] (problems ps')

981 [s] (problems ps')

977 (injective ps')

982 (injective ps')

978 (holes ps')

983 (holes ps')

984+ (map fst (notunified ps))

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

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

980 -- rechecking problems may find more solutions, so

986 -- rechecking problems may find more solutions, so

981 -- apply them here

987 -- apply them here

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

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

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

243hasv _ = False

244

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

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

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

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

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

247−unify ctxt env topx topy inj holes from =

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

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

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

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

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

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

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

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

497 _ -> False

498 _ -> False

498

499

499 metavar t = case t of

500 metavar t = case t of

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

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

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

501 || globmetavar t

503 || globmetavar t

502 _ -> False

504 _ -> False

503 pat t = case t of

505 pat t = case t of