b651aaf · Idris-dev · git.iko.soy

idris.cabal+4

compare with master

unifiedsplit

@@ -301,6 +301,10 @@ Extra-source-files:

301 test/interactive002/input

302 test/interactive002/*.idr

303 test/interactive002/expected

304+ test/interactive003/run

305+ test/interactive003/input

306+ test/interactive003/*.idr

307+ test/interactive003/expected

304

308

305 test/io001/run

309 test/io001/run

306 test/io001/*.idr

310 test/io001/*.idr

src/Idris/ErrReverse.hs+1−1

@@ -13,7 +13,7 @@ import Debug.Trace

13-- errors will be more readable

14

15errReverse :: IState -> Term -> Term

16−errReverse ist t = rewrite 5 t -- (elideLambdas t)

16+errReverse ist t = rewrite 5 (elideLambdas t)

17 where

18

19 rewrite 0 t = t

src/Idris/ProofSearch.hs+2−1

@@ -100,7 +100,8 @@ proofSearch elab fn nroot hints ist

100 [args] -> map isImp (snd args)

101 _ -> fail "Ambiguous name"

102 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

104 ps' <- get_probs

105 ps' <- get_probs

105 when (length ps < length ps') $ fail "Can't apply constructor"

106 when (length ps < length ps') $ fail "Can't apply constructor"

106 mapM_ (\ (_, h) -> do focus h

107 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