git.iko.soy/Idris-dev
on master help sign in
Only apply unique implicit conversions (and add test)
commit98599b57b96591d79a75cb6f432a60f6981ab82e authorEdwin Brady <ecb10@st-andrews.ac.uk> dateMon 25 Feb 2013, 10:39 (14 years ago) parentd13941c
7 files changed+65−7
compare with master
unifiedsplit
src/Core/Elaborate.hs+6−5 src/Idris/ElabTerm.hs+2−2 test/README+2 test/test020/expected+6 test/test020/run+5 test/test020/test020.idr+25 test/test020/test020a.idr+19
src/Core/Elaborate.hs+6−5
@@ -45,10 +45,9 @@ proof (ES (p, _) _ _) = p
4545proofFail :: Elab' aux a -> Elab' aux a
4646proofFail e = do s <- get
4747 case runStateT e s of
48− OK (a, s') -> trace ("OK ACTUALLY") $
49− do put s'
50− return a
51− Error err -> trace "BAD" $ lift $ Error (ProofSearchFail err)
48+ OK (a, s') -> do put s'
49+ return a
50+ Error err -> lift $ Error (ProofSearchFail err)
5251
5352saveState :: Elab' aux ()
5453saveState = do e@(ES p s _) <- get
@@ -65,6 +64,8 @@ erun f elab = do s <- get
6564 case runStateT elab s of
6665 OK (a, s') -> do put s'
6766 return a
67+ Error (ProofSearchFail (At f e))
68+ -> lift $ Error (ProofSearchFail (At f e))
6869 Error (At f e) -> lift $ Error (At f e)
6970 Error e -> lift $ Error (At f e)
7071
@@ -528,7 +529,7 @@ try' t1 t2 proofSearch
528529 where recoverableErr err@(CantUnify r _ _ _ _ _)
529530 = -- traceWhen r (show err) $
530531 r || proofSearch
531− recoverableErr (ProofSearchFail _) = trace "FAILED" $ False
532+ recoverableErr (ProofSearchFail _) = False
532533 recoverableErr _ = True
533534
534535tryWhen :: 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
453453 let t' = case (t, cs) of
454454 (PCoerced tm, _) -> tm
455455 (_, []) -> t
456− (_, cs) -> PAlternative False
457− (t : map (mkCoerce t) cs)
456+ (_, cs) -> PAlternative False [t ,
457+ PAlternative True (map (mkCoerce t) cs)]
458458 return t'
459459 where
460460 mkCoerce t n = let fc = FC "Coercion" 0 in -- line never appears!
test/README+2
@@ -18,5 +18,7 @@ Tests:
1818016: codata
1919017: mutually recursive totality checking
2020018: Message passing concurrency (raw form)
21+019: magic with
22+020: implicit conversions
2123
2224regxxx: 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+