git.iko.soy/Idris-dev
on master help sign in
Merge remote-tracking branch 'refs/remotes/upstream/master' into wip/tactical
commita0a345d967f78b5418497824b1b88e17616a71ee authorDavid Raymond Christiansen <david@davidchristiansen.dk> dateMon 20 Apr 2015, 15:19 (12 years ago) parentb5dd402e88802b
10 files changed+88−28
compare with master
unifiedsplit
idris.cabal+3 libs/base/Control/Arrow.idr+2−7 libs/base/Control/Isomorphism.idr+5−11 libs/prelude/Prelude/Either.idr+5 libs/prelude/Prelude/Pairs.idr+3 src/Idris/Elab/Utils.hs+12−10 test/reg062/expected test/reg062/reg062.idr+13 test/reg062/reg062.lidr+41 test/reg062/run+4
idris.cabal+3
@@ -304,6 +304,9 @@ Extra-source-files:
304304 test/reg061/run
305305 test/reg061/*.idr
306306 test/reg061/expected
307+ test/reg062/run
308+ test/reg062/*.idr
309+ test/reg062/expected
307310
308311 test/basic001/run
309312 test/basic001/*.idr
libs/base/Control/Arrow.idr+2−7
@@ -16,9 +16,7 @@ class Category arr => Arrow (arr : Type -> Type -> Type) where
1616 first : arr a b -> arr (a, c) (b, c)
1717
1818 second : arr a b -> arr (c, a) (c, b)
19− second f = arrow swap >>> first f >>> arrow swap where
20− swap : (x,y) -> (y,x)
21− swap (x,y) = (y,x)
19+ second f = arrow swap >>> first f >>> arrow swap
2220
2321 (***) : arr a b -> arr a' b' -> arr (a, a') (b, b')
2422 f *** g = first f >>> second g
@@ -61,10 +59,7 @@ class Arrow arr => ArrowChoice (arr : Type -> Type -> Type) where
6159 left : arr a b -> arr (Either a c) (Either b c)
6260
6361 right : arr a b -> arr (Either c a) (Either c b)
64− right f = arrow swap >>> left f >>> arrow swap where
65− swap : Either a b -> Either b a
66− swap (Left x) = Right x
67− swap (Right x) = Left x
62+ right f = arrow mirror >>> left f >>> arrow mirror
6863
6964 (+++) : arr a b -> arr c d -> arr (Either a c) (Either b d)
7065 f +++ g = left f >>> right g
libs/base/Control/Isomorphism.idr+5−11
@@ -39,13 +39,10 @@ isoSym (MkIso to from toFrom fromTo) = MkIso from to fromTo toFrom
3939
4040||| Disjunction is commutative
4141eitherComm : Iso (Either a b) (Either b a)
42−eitherComm = MkIso swap swap swapSwap swapSwap
43− where swap : Either a' b' -> Either b' a' -- a & b are parameters, so fixed!
44− swap (Left x) = Right x
45− swap (Right x) = Left x
46− swapSwap : (e : Either a' b') -> swap (swap e) = e
47− swapSwap (Left x) = Refl
48− swapSwap (Right x) = Refl
42+eitherComm = MkIso mirror mirror mirrorMirror mirrorMirror
43+ where mirrorMirror : (e : Either a' b') -> mirror (mirror e) = e
44+ mirrorMirror (Left x) = Refl
45+ mirrorMirror (Right x) = Refl
4946
5047||| Disjunction is associative
5148eitherAssoc : Iso (Either (Either a b) c) (Either a (Either b c))
@@ -116,10 +113,7 @@ eitherCongRight i = eitherCong isoRefl i
116113||| Conjunction is commutative
117114pairComm : Iso (a, b) (b, a)
118115pairComm = MkIso swap swap swapSwap swapSwap
119− where swap : (a', b') -> (b', a')
120− swap (x, y) = (y, x)
121−
122− swapSwap : (x : (a', b')) -> swap (swap x) = x
116+ where swapSwap : (x : (a', b')) -> swap (swap x) = x
123117 swapSwap (x, y) = Refl
124118
125119||| Conjunction is associative
libs/prelude/Prelude/Either.idr+5
@@ -66,6 +66,11 @@ fromEither : Either a a -> a
6666fromEither (Left l) = l
6767fromEither (Right r) = r
6868
69+||| Right becomes left and left becomes right
70+mirror : Either a b -> Either b a
71+mirror (Left x) = Right x
72+mirror (Right x) = Left x
73+
6974--------------------------------------------------------------------------------
7075-- Conversions
7176--------------------------------------------------------------------------------
libs/prelude/Prelude/Pairs.idr+3
@@ -5,6 +5,9 @@ import Builtins
55%access public
66%default total
77
8+swap : (a, b) -> (b, a)
9+swap (x, y) = (y, x)
10+
811using (a : Type, P : a -> Type)
912
1013 ||| Dependent pair where the first field is erased.
src/Idris/Elab/Utils.hs+12−10
@@ -186,27 +186,29 @@ getFixedInType i _ _ _ = []
186186getFlexInType i env ps (Bind n (Pi _ t _) sc)
187187 = nub $ (if (not (n `elem` ps)) then getFlexInType i env ps t else []) ++
188188 getFlexInType i (n : env) ps (instantiate (P Bound n t) sc)
189+
189190getFlexInType i env ps tm@(App _ f a)
190− | (P _ tn _, args) <- unApply tm
191+ | (P nt tn _, args) <- unApply tm, nt /= Bound
191192 = case lookupCtxt tn (idris_datatypes i) of
192193 [t] -> nub $ paramNames args env [x | x <- [0..length args],
193194 not (x `elem` param_pos t)]
194195 ++ getFlexInType i env ps f ++
195196 getFlexInType i env ps a
196− [] -> let ppos = case lookupCtxt tn (idris_fninfo i) of
197− [fi] -> fn_params fi
198− [] -> [] in
199− nub $ paramNames args env [x | x <- [0..length args],
200− not (x `elem` ppos)]
201− ++ getFlexInType i env ps f ++
202− getFlexInType i env ps a
197+ [] -> let ppos = case lookupCtxtName tn (idris_fninfo i) of
198+ [fi] -> fn_params (snd fi)
199+ [] -> []
200+ xs -> error ("Too much function info: " ++ show xs)
201+ in nub $ paramNames args env [x | x <- [0..length args],
202+ not (x `elem` ppos)]
203+ ++ getFlexInType i env ps f ++
204+ getFlexInType i env ps a
203205 | otherwise = nub $ getFlexInType i env ps f ++
204206 getFlexInType i env ps a
205207getFlexInType i _ _ _ = []
206208
207−-- Treat a name as a parameter if it appears in parameter positions in
209+-- | Treat a name as a parameter if it appears in parameter positions in
208210-- types, and never in a non-parameter position in a (non-param) argument type.
209−
211+getParamsInType :: IState -> [Name] -> [PArg] -> Type -> [Name]
210212getParamsInType i env ps t = let fix = getFixedInType i env ps t
211213 flex = getFlexInType i env fix t in
212214 [x | x <- fix, not (x `elem` flex)]
test/reg062/expectednew file

No changes to the content.

test/reg062/reg062.idrnew file+13
@@ -0,0 +1,13 @@
1+module MinCrash
2+
3+-- Test that #2130 stays fixed. It's important that the first argument
4+-- to revInduction be called `pred` here, because the bug was
5+-- triggered by looking up a bound variable in the global context and
6+-- getting an ambiguous result in a context where fully-qualified
7+-- names were expected.
8+
9+revInduction : (P : List a -> Type) -> P [] -> ((xs : List a) -> (x : a) -> P xs -> P (xs ++ [x]))
10+ -> (ys : List a) -> P ys
11+revInduction pred base ind ys with (reverse ys)
12+ revInduction pred base ind _ | revys =
13+ ?revInduction_rhs
test/reg062/reg062.lidrnew file+41
@@ -0,0 +1,41 @@
1+
2+This is a test to make sure that #2130 doesn't re-break.
3+
4+> import Data.Vect
5+> import Data.Fin
6+
7+> %default total
8+
9+> idSuccPreservesLTE : (m : Nat) -> (n : Nat) -> m `LTE` n -> m `LTE` (S n)
10+> idSuccPreservesLTE Z n prf = LTEZero
11+> idSuccPreservesLTE (S m) Z prf = absurd prf
12+> idSuccPreservesLTE (S m) (S n) prf = LTESucc (idSuccPreservesLTE m n (fromLteSucc prf))
13+
14+> ltZS : (m : Nat) -> LT Z (S m)
15+> ltZS Z = LTESucc LTEZero
16+> ltZS (S m) = idSuccPreservesLTE (S Z) (S m) (ltZS m)
17+
18+> record Preorder : {T : Type} -> (T -> T -> Type) -> Type where
19+> MkPreorder : {T : Type} ->
20+> (R : T -> T -> Type) ->
21+> (reflexive : (x : T) -> R x x) ->
22+> (transitive : (x : T) -> (y : T) -> (z : T) -> R x y -> R y z -> R x z) ->
23+> Preorder R
24+
25+> record TotalPreorder : {T : Type} -> (T -> T -> Type) -> Type where
26+> MkTotalPreorder : {T : Type} ->
27+> (R : T -> T -> Type) ->
28+> (reflexive : (x : T) -> R x x) ->
29+> (transitive : (x : T) -> (y : T) -> (z : T) -> R x y -> R y z -> R x z) ->
30+> (either : (x : T) -> (y : T) -> Either (R x y) (R y x)) ->
31+> TotalPreorder R
32+
33+> argmaxMax : {A : Type} -> {R : A -> A -> Type} -> TotalPreorder {T = A} R ->
34+> Vect n A -> LT Z n -> (Fin n, A)
35+> argmaxMax {n = Z} tp Nil p = absurd p
36+> argmaxMax {n = S Z} tp (a :: Nil) _ = (FZ, a)
37+> argmaxMax {A} {R} {n = S (S m)} (MkTotalPreorder R r t e) (a' :: (a'' :: as)) _
38+> with (argmaxMax (MkTotalPreorder {T = A} R r t e) (a'' :: as) (ltZS m))
39+> | (k, max) with (e a' max)
40+> | (Left _) = (FS k, max)
41+> | (Right _) = (FZ, a')
test/reg062/runnew file+4
@@ -0,0 +1,4 @@
1+#!/usr/bin/env bash
2+idris $@ reg062.idr --check --nocolour
3+idris $@ reg062.lidr --check --nocolour
4+rm -f *.ibc