git.iko.soy/Idris-dev
on master help sign in
Add check after each proof step, not just the end
140d8d2Edwin Brady
src/Idris/Prover.hs+6−1
compare with master
unifiedsplit
@@ -86,9 +86,14 @@ prove opt ctxt lit n ty
86 [([], P Ref n ty, ptm')] ty)
86 [([], P Ref n ty, ptm')] ty)
87 solveDeferred n
87 solveDeferred n
88elabStep :: ElabState [PDecl] -> ElabD a -> Idris (a, ElabState [PDecl])
88elabStep :: 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
90 OK (a, st') -> return (a, st')
90 OK (a, st') -> return (a, st')
91 Error a -> ierror a
91 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
92
97
93dumpState :: IState -> ProofState -> Idris ()
98dumpState :: IState -> ProofState -> Idris ()
94dumpState ist (PS nm [] _ _ tm _ _ _ _ _ _ _ _ _ _ _ _ _ _ _) =
99dumpState ist (PS nm [] _ _ tm _ _ _ _ _ _ _ _ _ _ _ _ _ _ _) =