140d8d2 · Idris-dev · git.iko.soy

git.iko.soy/Idris-dev

Add check after each proof step, not just the end

In elaboration, unification errors aren't always fatal, because some information may turn up later which fixes things. Interactive proofs ought to have immediate feedback instead. Fixes #974 It may also be worth considering automatically filling more things in by unification (refine currently requires each explicit argument to be given explicitly, because that is easier to explain). Possibly this should be a different tactic.

commit140d8d2ee5a194abe18b738c24a6511ad0e88119 authorEdwin Brady <ecb10@st-andrews.ac.uk> dateWed 23 Apr 2014, 19:29 (13 years ago) parenta85feeb

1 file changed+6−1

compare with master

unifiedsplit

src/Idris/Prover.hs+6−1

src/Idris/Prover.hs+6−1

@@ -86,9 +86,14 @@ prove opt ctxt lit n ty

8686 [([], P Ref n ty, ptm')] ty)

8787 solveDeferred n

8888elabStep :: ElabState [PDecl] -> ElabD a -> Idris (a, ElabState [PDecl])

89−elabStep st e = do case runStateT e st of

89+elabStep st e = case runStateT eCheck st of

9090 OK (a, st') -> return (a, st')

9191 Error a -> ierror a

92+ where eCheck = do res <- e

93+ tm <- get_term

94+ ctxt <- get_context

95+ lift $ check ctxt [] (forget tm)

96+ return res

9297

9398dumpState :: IState -> ProofState -> Idris ()

9499dumpState ist (PS nm [] _ _ tm _ _ _ _ _ _ _ _ _ _ _ _ _ _ _) =