cb005bc · Idris-dev · git.iko.soy

git.iko.soy/Idris-dev

Fix overenthusiastic unification

Fixes #1896 When a goal is solved explicitly, make sure it doesn't lead to anything in the 'dontunify' set being explicitly unified, or we might accidentally fix errors in the source program!

commitcb005bc030b751d5155f35fd954a8cbb5701d7b7 authorEdwin Brady <ecb10@st-andrews.ac.uk> dateSat 7 Feb 2015, 14:59 (12 years ago) parent5fce446

1 file changed+11−8

compare with master

unifiedsplit

src/Idris/Core/ProofState.hs+11−8

src/Idris/Core/ProofState.hs+11−8

@@ -530,6 +530,7 @@ solve ctxt env (Bind x (Guess ty val) sc)

530530 action (\ps -> ps { holes = traceWhen (unifylog ps) ("Dropping hole " ++ show x) $

531531 holes ps \\ [x],

532532 solved = Just (x, val),

533+ dontunify = filter (/= x) (dontunify ps),

533534 notunified = updateNotunified [(x,val)]

534535 (notunified ps),

535536 recents = x : recents ps,

@@ -602,6 +603,7 @@ patvar n ctxt env (Bind x (Hole t) sc) =

602603 do action (\ps -> ps { holes = traceWhen (unifylog ps) ("Dropping pattern hole " ++ show x) $

603604 holes ps \\ [x],

604605 solved = Just (x, P Bound n t),

606+ dontunify = filter (/=x) (dontunify ps),

605607 notunified = updateNotunified [(x,P Bound n t)]

606608 (notunified ps),

607609 injective = addInj n x (injective ps)

@@ -911,7 +913,7 @@ processTactic EndUnify ps

911913 ns' = map (\ (n, t) -> (n, updateSolvedTerm ns t)) ns

912914 (ns'', probs') = updateProblems ps ns' (problems ps)

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

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

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

915917 return (ps { pterm = tm',

916918 unified = (h, []),

917919 problems = probs',

@@ -934,7 +936,7 @@ processTactic (ComputeLet n) ps

934936processTactic UnifyProblems ps

935937 = do let (ns', probs') = updateProblems ps [] (problems ps)

936938 pterm' = updateSolved ns' (pterm ps)

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

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

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

939941 previous = Just ps, plog = "",

940942 notunified = updateNotunified ns' (notunified ps),

@@ -944,7 +946,7 @@ processTactic (MatchProblems all) ps

944946 = do let (ns', probs') = matchProblems all ps [] (problems ps)

945947 (ns'', probs'') = matchProblems all ps ns' probs'

946948 pterm' = updateSolved ns'' (pterm ps)

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

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

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

949951 previous = Just ps, plog = "",

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

@@ -954,16 +956,17 @@ processTactic t ps

954956 = case holes ps of

955957 [] -> fail "Nothing to fill in."

956958 (h:_) -> do ps' <- execStateT (process t h) ps

957− let (ns', probs')

959+ let (ns_in, probs')

958960 = case solved ps' of

959− Just s -> traceWhen (unifylog ps')

960− ("SOLVED " ++ show s) $

961− updateProblems ps [s] (problems ps')

961+ Just s -> traceWhen (unifylog ps)

962+ ("SOLVED " ++ show s ++ " " ++ show (dontunify ps')) $

963+ updateProblems ps' [s] (problems ps')

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

963965 -- rechecking problems may find more solutions, so

964966 -- apply them here

967+ let ns' = dropGiven (dontunify ps') ns_in (holes ps')

965968 let pterm'' = updateSolved ns' (pterm ps')

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

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

967970 return (ps' { pterm = pterm'',

968971 solved = Nothing,

969972 problems = probs',