@@ -530,6 +530,7 @@ solve ctxt env (Bind x (Guess ty val) sc)
530 action (\ps -> ps { holes = traceWhen (unifylog ps) ("Dropping hole " ++ show x) $
530 action (\ps -> ps { holes = traceWhen (unifylog ps) ("Dropping hole " ++ show x) $
531 holes ps \\ [x],
531 holes ps \\ [x],
532 solved = Just (x, val),
532 solved = Just (x, val),
533+ dontunify = filter (/= x) (dontunify ps),
533 notunified = updateNotunified [(x,val)]
534 notunified = updateNotunified [(x,val)]
534 (notunified ps),
535 (notunified ps),
535 recents = x : recents ps,
536 recents = x : recents ps,
@@ -602,6 +603,7 @@ patvar n ctxt env (Bind x (Hole t) sc) =
602 do action (\ps -> ps { holes = traceWhen (unifylog ps) ("Dropping pattern hole " ++ show x) $
603 do action (\ps -> ps { holes = traceWhen (unifylog ps) ("Dropping pattern hole " ++ show x) $
603 holes ps \\ [x],
604 holes ps \\ [x],
604 solved = Just (x, P Bound n t),
605 solved = Just (x, P Bound n t),
606+ dontunify = filter (/=x) (dontunify ps),
605 notunified = updateNotunified [(x,P Bound n t)]
607 notunified = updateNotunified [(x,P Bound n t)]
606 (notunified ps),
608 (notunified ps),
607 injective = addInj n x (injective ps)
609 injective = addInj n x (injective ps)
@@ -911,7 +913,7 @@ processTactic EndUnify ps
911 ns' = map (\ (n, t) -> (n, updateSolvedTerm ns t)) ns
913 ns' = map (\ (n, t) -> (n, updateSolvedTerm ns t)) ns
912 (ns'', probs') = updateProblems ps ns' (problems ps)
914 (ns'', probs') = updateProblems ps ns' (problems ps)
913 tm' = updateSolved ns'' (pterm ps) in
915 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'')) $
915 return (ps { pterm = tm',
917 return (ps { pterm = tm',
916 unified = (h, []),
918 unified = (h, []),
917 problems = probs',
919 problems = probs',
@@ -934,7 +936,7 @@ processTactic (ComputeLet n) ps
934processTactic UnifyProblems ps
936processTactic UnifyProblems ps
935 = do let (ns', probs') = updateProblems ps [] (problems ps)
937 = do let (ns', probs') = updateProblems ps [] (problems ps)
936 pterm' = updateSolved ns' (pterm ps)
938 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')) $
938 return (ps { pterm = pterm', solved = Nothing, problems = probs',
940 return (ps { pterm = pterm', solved = Nothing, problems = probs',
939 previous = Just ps, plog = "",
941 previous = Just ps, plog = "",
940 notunified = updateNotunified ns' (notunified ps),
942 notunified = updateNotunified ns' (notunified ps),
@@ -944,7 +946,7 @@ processTactic (MatchProblems all) ps
944 = do let (ns', probs') = matchProblems all ps [] (problems ps)
946 = do let (ns', probs') = matchProblems all ps [] (problems ps)
945 (ns'', probs'') = matchProblems all ps ns' probs'
947 (ns'', probs'') = matchProblems all ps ns' probs'
946 pterm' = updateSolved ns'' (pterm ps)
948 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'')) $
948 return (ps { pterm = pterm', solved = Nothing, problems = probs'',
950 return (ps { pterm = pterm', solved = Nothing, problems = probs'',
949 previous = Just ps, plog = "",
951 previous = Just ps, plog = "",
950 notunified = updateNotunified ns'' (notunified ps),
952 notunified = updateNotunified ns'' (notunified ps),
@@ -954,16 +956,17 @@ processTactic t ps
954 = case holes ps of
956 = case holes ps of
955 [] -> fail "Nothing to fill in."
957 [] -> fail "Nothing to fill in."
956 (h:_) -> do ps' <- execStateT (process t h) ps
958 (h:_) -> do ps' <- execStateT (process t h) ps
957− let (ns', probs')
959+ let (ns_in, probs')
958 = case solved ps' of
960 = case solved ps' of
959− Just s -> traceWhen (unifylog ps')
961+ Just s -> traceWhen (unifylog ps)
960− ("SOLVED " ++ show s) $
962+ ("SOLVED " ++ show s ++ " " ++ show (dontunify ps')) $
961− updateProblems ps [s] (problems ps')
963+ updateProblems ps' [s] (problems ps')
962 _ -> ([], problems ps')
964 _ -> ([], problems ps')
963 -- rechecking problems may find more solutions, so
965 -- rechecking problems may find more solutions, so
964 -- apply them here
966 -- apply them here
967+ let ns' = dropGiven (dontunify ps') ns_in (holes ps')
965 let pterm'' = updateSolved ns' (pterm ps')
968 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')) $
967 return (ps' { pterm = pterm'',
970 return (ps' { pterm = pterm'',
968 solved = Nothing,
971 solved = Nothing,
969 problems = probs',
972 problems = probs',