d120141 · Idris-dev · git.iko.soy

src/Core/Elaborate.hs+3

compare with master

unifiedsplit

@@ -329,6 +329,9 @@ movelast n = processTactic' (MoveLast n)

329matchProblems :: Elab' aux ()

330matchProblems = processTactic' MatchProblems

331

332+unifyProblems :: Elab' aux ()

333+unifyProblems = processTactic' UnifyProblems

334+

332defer :: Name -> Elab' aux ()

335defer :: Name -> Elab' aux ()

333defer n = do n' <- unique_hole n

336defer n = do n' <- unique_hole n

334 processTactic' (Defer n')

337 processTactic' (Defer n')

src/Core/ProofState.hs+10

@@ -79,6 +79,7 @@ data Tactic = Attack

79 | SetInjective Name

80 | MoveLast Name

81 | MatchProblems

82+ | UnifyProblems

82 | ProofState

83 | ProofState

83 | Undo

84 | Undo

84 | QED

85 | QED

@@ -754,6 +755,15 @@ processTactic (Reorder n) ps

754 return (ps' { previous = Just ps, plog = "" }, plog ps')

755 return (ps' { previous = Just ps, plog = "" }, plog ps')

755processTactic (ComputeLet n) ps

756processTactic (ComputeLet n) ps

756 = return (ps { pterm = computeLet (context ps) n (pterm ps) }, "")

757 = return (ps { pterm = computeLet (context ps) n (pterm ps) }, "")

758+processTactic UnifyProblems ps

759+ = let (ns', probs') = updateProblems (context ps) []

760+ (problems ps)

761+ (injective ps)

762+ (holes ps)

763+ pterm' = updateSolved ns' (pterm ps) in

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

765+ previous = Just ps, plog = "",

766+ holes = holes ps \\ (map fst ns') }, plog ps)

757processTactic MatchProblems ps

767processTactic MatchProblems ps

758 = let (ns', probs') = matchProblems (context ps)

768 = let (ns', probs') = matchProblems (context ps)

759 (problems ps)

769 (problems ps)

src/Idris/ElabTerm.hs+1−1

@@ -58,7 +58,7 @@ build ist info pattern fn tm

58 resolveTC 7 fn ist) ivs

59 tm <- get_term

60 ctxt <- get_context

61− when (not pattern) matchProblems

61+ when (not pattern) $ do matchProblems; unifyProblems

62 probs <- get_probs

63 case probs of

64 [] -> return ()