@@ -1002,6 +1002,18 @@ updateProblems ps updates probs = rec 10 updates probs
10021002 (x', y', newx || newy,
10031003 updateEnv ns env, updateError ns err, fc, fa)
10041004
1005+orderUpdateSolved :: [(Name, Term)] -> ProofTerm -> (ProofTerm, [Name])
1006+orderUpdateSolved ns tm = update [] ns tm
1007+ where
1008+ update done [] t = (t, done)
1009+ update done ((n, P _ n' _) : ns) t | n == n' = update done ns t
1010+ update done (n : ns) t = update (fst n : done)
1011+ (map (updateMatch n) ns)
1012+ (updateSolved [n] t)
1013+
1014+ -- Update the later solutions too
1015+ updateMatch n (x, tm) = (x, updateSolvedTerm [n] tm)
1016+
10051017-- attempt to solve remaining problems with match_unify
10061018matchProblems :: Bool -> ProofState -> [(Name, TT Name)] -> Fails
10071019 -> ([(Name, TT Name)], Fails)
@@ -1065,30 +1077,25 @@ processTactic (ComputeLet n) ps
10651077 (getProofTerm (pterm ps)) }, "")
10661078processTactic UnifyProblems ps
10671079 = do let (ns', probs') = updateProblems ps [] (map setReady (problems ps))
1068− pterm' = orderUpdateSolved ns' (pterm ps)
1069− traceWhen (unifylog ps) ("(UnifyProblems) Dropping holes: " ++ show (map fst ns')) $
1080+ (pterm', dropped) = orderUpdateSolved ns' (pterm ps)
1081+ traceWhen (unifylog ps) ("(UnifyProblems) Dropping holes: " ++ show dropped) $
10701082 return (ps { pterm = pterm', solved = Nothing, problems = probs',
10711083 previous = Just ps, plog = "",
10721084 notunified = updateNotunified ns' (notunified ps),
1073− recents = recents ps ++ map fst ns',
1085+ recents = recents ps ++ dropped,
10741086 dotted = filter (notIn ns') (dotted ps),
1075− holes = holes ps \\ (map fst ns') }, plog ps)
1087+ holes = holes ps \\ dropped }, plog ps)
10761088 where notIn ns (h, _) = h `notElem` map fst ns
1077− orderUpdateSolved [] t = t
1078− orderUpdateSolved (n : ns) t = orderUpdateSolved ns (updateSolved [n] t)
10791089processTactic (MatchProblems all) ps
10801090 = do let (ns', probs') = matchProblems all ps [] (map setReady (problems ps))
10811091 (ns'', probs'') = matchProblems all ps ns' probs'
1082− pterm' = orderUpdateSolved ns'' (resetProofTerm (pterm ps))
1083− traceWhen (unifylog ps) ("(MatchProblems) Dropping holes: " ++ show ns'') $
1092+ (pterm', dropped) = orderUpdateSolved ns'' (resetProofTerm (pterm ps))
1093+ traceWhen (unifylog ps) ("(MatchProblems) Dropping holes: " ++ show dropped) $
10841094 return (ps { pterm = pterm', solved = Nothing, problems = probs'',
10851095 previous = Just ps, plog = "",
10861096 notunified = updateNotunified ns'' (notunified ps),
1087− recents = recents ps ++ map fst ns'',
1088− holes = holes ps \\ (map fst ns'') }, plog ps)
1089− where
1090− orderUpdateSolved [] t = t
1091− orderUpdateSolved (n : ns) t = orderUpdateSolved ns (updateSolved [n] t)
1097+ recents = recents ps ++ dropped,
1098+ holes = holes ps \\ dropped }, plog ps)
10921099processTactic t ps
10931100 = case holes ps of
10941101 [] -> case t of