f2bf55d · Idris-dev · git.iko.soy

git.iko.soy/Idris-dev

on master help sign in

Merge 'not unified' variables

f2bf55dEdwin Brady13 years ago

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

compare with master

unifiedsplit

@@ -212,10 +212,11 @@ unify' ctxt env topx topy =

212 (fails ++ problems ps)

213 (injective ps)

214 (holes ps)

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

215− put (ps { problems = probs',

216+ put (ps { problems = probs' ++ probs_notu,

216 unified = (h, ns'),

217 unified = (h, ns'),

217 injective = updateInj u (injective ps),

218 injective = updateInj u (injective ps),

218− notunified = notu ++ notunified ps })

219+ notunified = notu' })

219 return u

220 return u

220 where updateInj ((n, a) : us) inj

221 where updateInj ((n, a) : us) inj

221 | (P _ n' _, _) <- unApply a,

222 | (P _ n' _, _) <- unApply a,

@@ -812,6 +813,14 @@ solveInProblems x val ((l, r, env, err) : ps)

812 = ((psubst x val l, psubst x val r,

813 = ((psubst x val l, psubst x val r,

813 updateEnv [(x, val)] env, err) : solveInProblems x val ps)

814 updateEnv [(x, val)] env, err) : solveInProblems x val ps)

814

815

816+mergeNotunified :: Env -> [(Name, Term)] -> ([(Name, Term)], Fails)

817+mergeNotunified env ns = mnu ns [] [] where

818+ mnu [] ns_acc ps_acc = (reverse ns_acc, reverse ps_acc)

819+ mnu ((n, t):ns) ns_acc ps_acc

820+ | Just t' <- lookup n ns = mnu ns ((n,t) : ns_acc)

821+ ((t,t',env,Msg "", [],Match) : ps_acc)

822+ | otherwise = mnu ns ((n,t) : ns_acc) ps_acc

823+

815updateNotunified [] nu = nu

824updateNotunified [] nu = nu

816updateNotunified ns nu = up nu where

825updateNotunified ns nu = up nu where

817 up [] = []

826 up [] = []

@@ -877,8 +886,7 @@ processTactic EndUnify ps

877 notunified = updateNotunified ns'' (notunified ps),

886 notunified = updateNotunified ns'' (notunified ps),

878 holes = holes ps \\ map fst ns'' }, "")

887 holes = holes ps \\ map fst ns'' }, "")

879processTactic UnifyAll ps

888processTactic UnifyAll ps

880− = trace (show (notunified ps)) $

881− let tm' = updateSolved (notunified ps) (pterm ps) in

889+ = let tm' = updateSolved (notunified ps) (pterm ps) in

882 return (ps { pterm = tm',

890 return (ps { pterm = tm',

883 notunified = [],

891 notunified = [],

884 holes = holes ps \\ map fst (notunified ps) }, "")

892 holes = holes ps \\ map fst (notunified ps) }, "")

src/Idris/ElabTerm.hs+2−1

@@ -69,7 +69,7 @@ build ist info pattern opts fn tm

70 when (not pattern) $

71 traceWhen u ("Remaining problems:\n" ++ show probs) $

72− do matchProblems True; unifyProblems

72+ do unify_all; matchProblems True; unifyProblems

73 probs <- get_probs

74 case probs of

75 [] -> return ()

@@ -123,6 +123,7 @@ elab ist info pattern opts fn tm

123 end_unify

124 when pattern -- convert remaining holes to pattern vars

125 (do update_term orderPats

126+ unify_all

126 matchProblems False -- only the ones we matched earlier

127 matchProblems False -- only the ones we matched earlier

127 unifyProblems

128 unifyProblems

128 mkPat)

129 mkPat)