@@ -78,6 +78,7 @@ data Tactic = Attack
7878 | Instance Name
7979 | SetInjective Name
8080 | MoveLast Name
81+ | MatchProblems
8182 | ProofState
8283 | Undo
8384 | QED
@@ -711,6 +712,20 @@ updateProblems ctxt ns ps inj holes = up ns ps where
711712 _ -> let (ns', ps') = up ns ps in
712713 (ns', (x',y',env',err') : ps')
713714
715+-- attempt to solve remaining problems with match_unify
716+matchProblems ctxt ps inj holes = up [] ps where
717+ up ns [] = (ns, [])
718+ up ns ((x, y, env, err) : ps) =
719+ let x' = updateSolved ns x
720+ y' = updateSolved ns y
721+ err' = updateError ns err
722+ env' = updateEnv ns env in
723+ case match_unify ctxt env' x' y' inj holes of
724+ OK v -> -- trace ("Added " ++ show v ++ " from " ++ show (x', y')) $
725+ up (ns ++ v) ps
726+ _ -> let (ns', ps') = up ns ps in
727+ (ns', (x',y',env',err') : ps')
728+
714729processTactic :: Tactic -> ProofState -> TC (ProofState, String)
715730processTactic QED ps = case holes ps of
716731 [] -> do let tm = {- normalise (context ps) [] -} (pterm ps)
@@ -739,6 +754,15 @@ processTactic (Reorder n) ps
739754 return (ps' { previous = Just ps, plog = "" }, plog ps')
740755processTactic (ComputeLet n) ps
741756 = return (ps { pterm = computeLet (context ps) n (pterm ps) }, "")
757+processTactic MatchProblems ps
758+ = let (ns', probs') = matchProblems (context ps)
759+ (problems ps)
760+ (injective ps)
761+ (holes ps)
762+ pterm' = updateSolved ns' (pterm ps) in
763+ return (ps { pterm = pterm', solved = Nothing, problems = probs',
764+ previous = Just ps, plog = "",
765+ holes = holes ps \\ (map fst ns') }, plog ps)
742766processTactic t ps
743767 = case holes ps of
744768 [] -> fail "Nothing to fill in."
@@ -795,4 +819,3 @@ process t h = tactic (Just h) (mktac t)
795819 mktac (Instance n) = instanceArg n
796820 mktac (SetInjective n) = setinj n
797821 mktac (MoveLast n) = movelast n
798−