62705e4 · Idris-dev · git.iko.soy

git.iko.soy/Idris-dev

Tweak mergeNotunified

No need to add a problem if already equal

commit62705e4b2c6dbb5253d3e6705b186f57666ce856 authorEdwin Brady <ecb10@st-andrews.ac.uk> dateFri 25 Apr 2014, 12:27 (13 years ago) parent70e9dc9

3 files changed+5−2

unifiedsplit

src/Idris/Core/Elaborate.hs+1

@@ -646,6 +646,7 @@ no_errors tac err

646646 Error _ -> lift $ Error e

647647 OK (a, s') -> do put s'

648648 return a

649+ unifyProblems

649650 ps' <- get_probs

650651 if (length ps' > length ps) then

651652 case reverse ps' of

src/Idris/Core/ProofState.hs+3−2

@@ -817,8 +817,9 @@ mergeNotunified :: Env -> [(Name, Term)] -> ([(Name, Term)], Fails)

817817mergeNotunified env ns = mnu ns [] [] where

818818 mnu [] ns_acc ps_acc = (reverse ns_acc, reverse ps_acc)

819819 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)

820+ | Just t' <- lookup n ns, t /= t'

821+ = mnu ns ((n,t') : ns_acc)

822+ ((t,t',env,Msg "", [],Unify) : ps_acc)

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

823824

824825updateNotunified [] nu = nu

src/Idris/Prover.hs+1

@@ -85,6 +85,7 @@ prove opt ctxt lit n ty

8585 [([], P Ref n ty, ptm)]

8686 [([], P Ref n ty, ptm')] ty)

8787 solveDeferred n

88+

8889elabStep :: ElabState [PDecl] -> ElabD a -> Idris (a, ElabState [PDecl])

8990elabStep st e = case runStateT eCheck st of

9091 OK (a, st') -> return (a, st')