git.iko.soy/Idris-dev
on master help sign in
Check that proof steps introduce no new problems

In interactive mode only (it is important that proofs can fail temporarily during elaboration since futher information may help refine the goal). Fixes #1243

commit2d22462fd8086afe1cbd1768760125c7c0556094 authorEdwin Brady <ecb10@st-andrews.ac.uk> dateThu 22 May 2014, 12:14 (12 years ago) parent602552e
5 files changed+30−4
compare with master
unifiedsplit
idris.cabal+3 src/Idris/Prover.hs+7−4 test/reg044/expected+11 test/reg044/reg044.idr+6 test/reg044/run+3
idris.cabal+3
@@ -238,6 +238,9 @@ Extra-source-files:
238238 test/reg042/expected
239239 test/reg043/run
240240 test/reg043/expected
241+ test/reg044/run
242+ test/reg044/*.idr
243+ test/reg044/expected
241244
242245 test/basic001/run
243246 test/basic001/*.idr
src/Idris/Prover.hs+7−4
@@ -91,10 +91,13 @@ elabStep st e = case runStateT eCheck st of
9191 OK (a, st') -> return (a, st')
9292 Error a -> ierror a
9393 where eCheck = do res <- e
94− tm <- get_term
95− ctxt <- get_context
96− lift $ check ctxt [] (forget tm)
97− return res
94+ probs' <- get_probs
95+ case probs' of
96+ [] -> do tm <- get_term
97+ ctxt <- get_context
98+ lift $ check ctxt [] (forget tm)
99+ return res
100+ ((_,_,_,e,_,_):_) -> lift $ Error e
98101
99102dumpState :: IState -> ProofState -> Idris ()
100103dumpState ist (PS nm [] _ _ tm _ _ _ _ _ _ _ _ _ _ _ _ _ _ _) =
test/reg044/expectednew file+11
@@ -0,0 +1,11 @@
1+reg044.idr:4:4:When elaborating right hand side of Main.pf:
2+Can't unify
3+ b = b
4+with
5+ a = b
6+
7+Specifically:
8+ Can't unify
9+ b
10+ with
11+ a
test/reg044/reg044.idrnew file+6
@@ -0,0 +1,6 @@
1+exjection : S a = S b -> a = b
2+exjection = ?pf
3+
4+pf = proof
5+ intros
6+ refine refl
test/reg044/runnew file+3
@@ -0,0 +1,3 @@
1+#!/usr/bin/env bash
2+idris reg044.idr --check
3+rm -f *.ibc