d120141 · Idris-dev · git.iko.soy

git.iko.soy/Idris-dev

Add a final unification step

Since solving matched implicits may help solve remaining problems.

commitd1201412c5cb7defc46c16f85f69374bd28ff02a authorEdwin Brady <ecb10@st-andrews.ac.uk> dateTue 22 Oct 2013, 14:51 (13 years ago) parent38ddde3

3 files changed+14−1

compare with master

unifiedsplit

src/Core/Elaborate.hs+3 src/Core/ProofState.hs+10 src/Idris/ElabTerm.hs+1−1

src/Core/Elaborate.hs+3

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

329329matchProblems :: Elab' aux ()

330330matchProblems = processTactic' MatchProblems

331331

332+unifyProblems :: Elab' aux ()

333+unifyProblems = processTactic' UnifyProblems

334+

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

333336defer n = do n' <- unique_hole n

334337 processTactic' (Defer n')

src/Core/ProofState.hs+10

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

7979 | SetInjective Name

8080 | MoveLast Name

8181 | MatchProblems

82+ | UnifyProblems

8283 | ProofState

8384 | Undo

8485 | QED

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

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

755756processTactic (ComputeLet n) ps

756757 = 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)

757767processTactic MatchProblems ps

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

759769 (problems ps)

src/Idris/ElabTerm.hs+1−1

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

5858 resolveTC 7 fn ist) ivs

5959 tm <- get_term

6060 ctxt <- get_context

61− when (not pattern) matchProblems

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

6262 probs <- get_probs

6363 case probs of

6464 [] -> return ()