98599b5 · Idris-dev · git.iko.soy

src/Core/Elaborate.hs+6−5

compare with master

unifiedsplit

@@ -45,10 +45,9 @@ proof (ES (p, _) _ _) = p

45proofFail :: Elab' aux a -> Elab' aux a

46proofFail e = do s <- get

47 case runStateT e s of

48− OK (a, s') -> trace ("OK ACTUALLY") $

49− do put s'

48+ OK (a, s') -> do put s'

50− return a

49+ return a

51− Error err -> trace "BAD" $ lift $ Error (ProofSearchFail err)

50+ Error err -> lift $ Error (ProofSearchFail err)

52

51

53saveState :: Elab' aux ()

52saveState :: Elab' aux ()

54saveState = do e@(ES p s _) <- get

53saveState = do e@(ES p s _) <- get

@@ -65,6 +64,8 @@ erun f elab = do s <- get

65 case runStateT elab s of

64 case runStateT elab s of

66 OK (a, s') -> do put s'

65 OK (a, s') -> do put s'

67 return a

66 return a

67+ Error (ProofSearchFail (At f e))

68+ -> lift $ Error (ProofSearchFail (At f e))

68 Error (At f e) -> lift $ Error (At f e)

69 Error (At f e) -> lift $ Error (At f e)

69 Error e -> lift $ Error (At f e)

70 Error e -> lift $ Error (At f e)

70

71

@@ -528,7 +529,7 @@ try' t1 t2 proofSearch

528 where recoverableErr err@(CantUnify r _ _ _ _ _)

529 where recoverableErr err@(CantUnify r _ _ _ _ _)

529 = -- traceWhen r (show err) $

530 = -- traceWhen r (show err) $

530 r || proofSearch

531 r || proofSearch

531− recoverableErr (ProofSearchFail _) = trace "FAILED" $ False

532+ recoverableErr (ProofSearchFail _) = False

532 recoverableErr _ = True

533 recoverableErr _ = True

533

534

534tryWhen :: Bool -> Elab' aux a -> Elab' aux a -> Elab' aux a

535tryWhen :: Bool -> Elab' aux a -> Elab' aux a -> Elab' aux a

src/Idris/ElabTerm.hs+2−2

@@ -453,8 +453,8 @@ elab ist info pattern tcgen fn tm

453 let t' = case (t, cs) of

454 (PCoerced tm, _) -> tm

455 (_, []) -> t

456− (_, cs) -> PAlternative False

456+ (_, cs) -> PAlternative False [t ,

457− (t : map (mkCoerce t) cs)

457+ PAlternative True (map (mkCoerce t) cs)]

458 return t'

459 where

460 mkCoerce t n = let fc = FC "Coercion" 0 in -- line never appears!

test/README+2

@@ -18,5 +18,7 @@ Tests:

18016: codata

19017: mutually recursive totality checking

20018: Message passing concurrency (raw form)

21+019: magic with

22+020: implicit conversions

21

23

22regxxx: various regression tests

24regxxx: various regression tests

test/test020/expectednew file+6

@@ -0,0 +1,6 @@

1+test020a.idr:16:Can't unify Vect a n with List a

2+

3+Specifically:

4+ Can't unify Vect a n with List a

5+[3, 2, 1]

6+Number 42

test/test020/runnew file+5

@@ -0,0 +1,5 @@

1+#!/bin/bash

2+idris $@ test020.idr -o test020

3+idris $@ test020a.idr --check

4+./test020

5+rm -f test020 *.ibc

test/test020/test020.idrnew file+25

@@ -0,0 +1,25 @@

1+module Main

2+

3+implicit

4+natInt : Nat -> Int

5+natInt x = cast x

6+

7+implicit

8+forget : Vect a n -> List a

9+forget [] = []

10+forget (x :: xs) = x :: forget xs

11+

12+foo : Vect a n -> List a

13+foo xs = reverse xs

14+

15+implicit intString : Int -> String

16+intString = show

17+

18+test : Int -> String

19+test x = "Number " ++ x

20+

21+main : IO ()

22+main = do print (foo [1,2,3])

23+ print (test 42)

24+

25+

test/test020/test020a.idrnew file+19

@@ -0,0 +1,19 @@

1+module Main

2+

3+implicit

4+forget : Vect a n -> List a

5+forget [] = []

6+forget (x :: xs) = x :: forget xs

7+

8+implicit

9+forget' : Vect a n -> List a

10+forget' [] = []

11+forget' (x :: xs) = forget xs

12+

13+foo : Vect a n -> List a

14+foo xs = reverse xs

15+

16+main : IO ()

17+main = print (foo [1,2,3])

18+

19+