Proof search fix
commitb651aaf1fdc189d6b5d59dbdccb0030980b6b623
authorEdwin Brady <ecb10@st-andrews.ac.uk>
dateThu 20 Feb 2014, 23:30 (13 years ago)
parent4227b95
idris.cabal+4
@@ -301,6 +301,10 @@ Extra-source-files:
301301 test/interactive002/input
302302 test/interactive002/*.idr
303303 test/interactive002/expected
304+ test/interactive003/run
305+ test/interactive003/input
306+ test/interactive003/*.idr
307+ test/interactive003/expected
304308
305309 test/io001/run
306310 test/io001/*.idr
src/Idris/ErrReverse.hs+1−1
@@ -13,7 +13,7 @@ import Debug.Trace
1313-- errors will be more readable
1414
1515errReverse :: IState -> Term -> Term
16−errReverse ist t = rewrite 5 t -- (elideLambdas t)
16+errReverse ist t = rewrite 5 (elideLambdas t)
1717 where
1818
1919 rewrite 0 t = t
src/Idris/ProofSearch.hs+2−1
@@ -100,7 +100,8 @@ proofSearch elab fn nroot hints ist
100100 [args] -> map isImp (snd args)
101101 _ -> fail "Ambiguous name"
102102 ps <- get_probs
103− args <- map snd <$> apply (Var n) imps
103+ args <- map snd <$> try' (apply (Var n) imps)
104+ (match_apply (Var n) imps) True
104105 ps' <- get_probs
105106 when (length ps < length ps') $ fail "Can't apply constructor"
106107 mapM_ (\ (_, h) -> do focus h
test/interactive003/expectednew file+5
@@ -0,0 +1,5 @@
1+Type checking ./interactive003.idr
2+ys
3+x :: (app xs ys)
4+[]
5+f x y :: (vzipWith f xs ys)
test/interactive003/inputnew file+4
@@ -0,0 +1,4 @@
1+:ps 2 app_rhs_1
2+:ps 3 app_rhs_2
3+:ps 6 vzipWith_rhs_3
4+:ps 7 vzipWith_rhs_1
test/interactive003/interactive003.idrnew file+8
@@ -0,0 +1,8 @@
1+app : Vect n a -> Vect m a -> Vect (n + m) a
2+app [] ys = ?app_rhs_1
3+app (x :: xs) ys = ?app_rhs_2
4+
5+vzipWith : (a -> b -> c) -> Vect n a -> Vect n b -> Vect n c
6+vzipWith f [] [] = ?vzipWith_rhs_3
7+vzipWith f (x :: xs) (y :: ys) = ?vzipWith_rhs_1
8+
test/interactive003/runnew file+3
@@ -0,0 +1,3 @@
1+#!/usr/bin/env bash
2+idris --quiet interactive003.idr < input
3+rm -f *.ibc