Fix interactive prover
safeForget broke things due to missing case. Also added a test to ensure
it doesn't happen again.
commit2d503f1c8ab0f164869576165c24038b2b00f323
authorEdwin Brady <ecb10@st-andrews.ac.uk>
dateMon 23 Mar 2015, 19:51 (12 years ago)
parentcea7870
idris.cabal+13
@@ -516,9 +516,22 @@ Extra-source-files:
516516 test/proof004/run
517517 test/proof004/*.idr
518518 test/proof004/expected
519+ test/proof005/run
520+ test/proof005/*.idr
521+ test/proof005/expected
522+ test/proof006/run
523+ test/proof006/*.idr
524+ test/proof006/expected
525+ test/proof007/run
526+ test/proof007/*.idr
527+ test/proof007/expected
519528 test/proof008/run
520529 test/proof008/*.idr
521530 test/proof008/expected
531+ test/proof009/run
532+ test/proof009/*.idr
533+ test/proof009/expected
534+ test/proof009/input
522535
523536 test/quasiquote001/run
524537 test/quasiquote001/*.idr
src/Idris/Core/TT.hs+2
@@ -1193,6 +1193,8 @@ safeForgetEnv env (Bind n b sc)
11931193 Just $ RBind n' b' sc'
11941194 where safeForgetEnvB env (Let t v) = liftM2 Let (safeForgetEnv env t)
11951195 (safeForgetEnv env v)
1196+ safeForgetEnvB env (Guess t v) = liftM2 Guess (safeForgetEnv env t)
1197+ (safeForgetEnv env v)
11961198 safeForgetEnvB env b = do ty' <- safeForgetEnv env (binderTy b)
11971199 Just $ fmap (\_ -> ty') b
11981200safeForgetEnv env (App f a) = liftM2 RApp (safeForgetEnv env f) (safeForgetEnv env a)
src/Idris/ElabTerm.hs+2−1
@@ -1734,7 +1734,8 @@ runTac autoSolve ist perhapsFC fn tac
17341734 bname _ = Nothing
17351735 runT (Intro xs) = mapM_ (\x -> do attack; intro (Just x)) xs
17361736 runT Intros = do g <- goal
1737− attack; intro (bname g)
1737+ attack;
1738+ intro (bname g)
17381739 try' (runT Intros)
17391740 (return ()) True
17401741 where
test/proof009/expectednew file+26
@@ -0,0 +1,26 @@
1+Type checking ./proof009.idr
2+
3+
4+---------- Goal: ----------
5+{hole0} : Int -> Int -> Int
6+-Main.arhs> ---------- Other goals: ----------
7+{hole0}
8+---------- Assumptions: ----------
9+ x : Int
10+---------- Goal: ----------
11+{hole1} : Int -> Int
12+-Main.arhs> ---------- Other goals: ----------
13+{hole1},{hole0}
14+---------- Assumptions: ----------
15+ x : Int
16+ y : Int
17+---------- Goal: ----------
18+{hole2} : Int
19+-Main.arhs> arhs: No more goals.
20+-Main.arhs> Proof completed!
21+Main.arhs = proof
22+ intro x
23+ intros
24+ trivial
25+
26+
test/proof009/inputnew file+6
@@ -0,0 +1,6 @@
1+:p arhs
2+intro x
3+intros
4+trivial
5+qed
6+:q
test/proof009/proof009.idrnew file+9
@@ -0,0 +1,9 @@
1+afn : Int -> Int -> Int
2+afn x y = ?arhs
3+
4+-- plus_comm_rhs_1 : y = plus y 0
5+--
6+-- plus_comm : (x, y : Nat) -> plus x y = plus y x
7+-- plus_comm Z y = plus_comm_rhs_1
8+-- plus_comm (S k) y = ?plus_comm_rhs_2
9+
test/proof009/runnew file+3
@@ -0,0 +1,3 @@
1+#!/usr/bin/env bash
2+idris $@ --quiet proof009.idr < input
3+rm -f *.ibc