a0a345d · Idris-dev · git.iko.soy

idris.cabal+3

compare with master

unifiedsplit

@@ -304,6 +304,9 @@ Extra-source-files:

304 test/reg061/run

305 test/reg061/*.idr

306 test/reg061/expected

307+ test/reg062/run

308+ test/reg062/*.idr

309+ test/reg062/expected

307

310

308 test/basic001/run

311 test/basic001/run

309 test/basic001/*.idr

312 test/basic001/*.idr

libs/base/Control/Arrow.idr+2−7

@@ -16,9 +16,7 @@ class Category arr => Arrow (arr : Type -> Type -> Type) where

16 first : arr a b -> arr (a, c) (b, c)

17

18 second : arr a b -> arr (c, a) (c, b)

19− second f = arrow swap >>> first f >>> arrow swap where

19+ second f = arrow swap >>> first f >>> arrow swap

20− swap : (x,y) -> (y,x)

21− swap (x,y) = (y,x)

22

20

23 (***) : arr a b -> arr a' b' -> arr (a, a') (b, b')

21 (***) : arr a b -> arr a' b' -> arr (a, a') (b, b')

24 f *** g = first f >>> second g

22 f *** g = first f >>> second g

@@ -61,10 +59,7 @@ class Arrow arr => ArrowChoice (arr : Type -> Type -> Type) where

61 left : arr a b -> arr (Either a c) (Either b c)

59 left : arr a b -> arr (Either a c) (Either b c)

62

60

63 right : arr a b -> arr (Either c a) (Either c b)

61 right : arr a b -> arr (Either c a) (Either c b)

64− right f = arrow swap >>> left f >>> arrow swap where

62+ right f = arrow mirror >>> left f >>> arrow mirror

65− swap : Either a b -> Either b a

66− swap (Left x) = Right x

67− swap (Right x) = Left x

68

63

69 (+++) : arr a b -> arr c d -> arr (Either a c) (Either b d)

64 (+++) : arr a b -> arr c d -> arr (Either a c) (Either b d)

70 f +++ g = left f >>> right g

65 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

39

40||| Disjunction is commutative

41eitherComm : Iso (Either a b) (Either b a)

42−eitherComm = MkIso swap swap swapSwap swapSwap

42+eitherComm = MkIso mirror mirror mirrorMirror mirrorMirror

43− where swap : Either a' b' -> Either b' a' -- a & b are parameters, so fixed!

43+ where mirrorMirror : (e : Either a' b') -> mirror (mirror e) = e

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

44+ mirrorMirror (Left x) = Refl

48− swapSwap (Right x) = Refl

45+ mirrorMirror (Right x) = Refl

49

46

50||| Disjunction is associative

47||| Disjunction is associative

51eitherAssoc : Iso (Either (Either a b) c) (Either a (Either b c))

48eitherAssoc : Iso (Either (Either a b) c) (Either a (Either b c))

@@ -116,10 +113,7 @@ eitherCongRight i = eitherCong isoRefl i

116||| Conjunction is commutative

113||| Conjunction is commutative

117pairComm : Iso (a, b) (b, a)

114pairComm : Iso (a, b) (b, a)

118pairComm = MkIso swap swap swapSwap swapSwap

115pairComm = 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

123 swapSwap (x, y) = Refl

117 swapSwap (x, y) = Refl

124

118

125||| Conjunction is associative

119||| Conjunction is associative

libs/prelude/Prelude/Either.idr+5

@@ -66,6 +66,11 @@ fromEither : Either a a -> a

66fromEither (Left l) = l

67fromEither (Right r) = r

68

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+

69--------------------------------------------------------------------------------

74--------------------------------------------------------------------------------

70-- Conversions

75-- Conversions

71--------------------------------------------------------------------------------

76--------------------------------------------------------------------------------

libs/prelude/Prelude/Pairs.idr+3

@@ -5,6 +5,9 @@ import Builtins

5%access public

6%default total

7

8+swap : (a, b) -> (b, a)

9+swap (x, y) = (y, x)

10+

8using (a : Type, P : a -> Type)

11using (a : Type, P : a -> Type)

9

12

10 ||| Dependent pair where the first field is erased.

13 ||| Dependent pair where the first field is erased.

src/Idris/Elab/Utils.hs+12−10

@@ -186,27 +186,29 @@ getFixedInType i _ _ _ = []

186getFlexInType i env ps (Bind n (Pi _ t _) sc)

187 = nub $ (if (not (n `elem` ps)) then getFlexInType i env ps t else []) ++

188 getFlexInType i (n : env) ps (instantiate (P Bound n t) sc)

189+

189getFlexInType i env ps tm@(App _ f a)

190getFlexInType i env ps tm@(App _ f a)

190− | (P _ tn _, args) <- unApply tm

191+ | (P nt tn _, args) <- unApply tm, nt /= Bound

191 = case lookupCtxt tn (idris_datatypes i) of

192 = case lookupCtxt tn (idris_datatypes i) of

192 [t] -> nub $ paramNames args env [x | x <- [0..length args],

193 [t] -> nub $ paramNames args env [x | x <- [0..length args],

193 not (x `elem` param_pos t)]

194 not (x `elem` param_pos t)]

194 ++ getFlexInType i env ps f ++

195 ++ getFlexInType i env ps f ++

195 getFlexInType i env ps a

196 getFlexInType i env ps a

196− [] -> let ppos = case lookupCtxt tn (idris_fninfo i) of

197+ [] -> let ppos = case lookupCtxtName tn (idris_fninfo i) of

197− [fi] -> fn_params fi

198+ [fi] -> fn_params (snd fi)

198− [] -> [] in

199+ [] -> []

200+ xs -> error ("Too much function info: " ++ show xs)

199− nub $ paramNames args env [x | x <- [0..length args],

201+ in nub $ paramNames args env [x | x <- [0..length args],

200− not (x `elem` ppos)]

202+ not (x `elem` ppos)]

201− ++ getFlexInType i env ps f ++

203+ ++ getFlexInType i env ps f ++

202− getFlexInType i env ps a

204+ getFlexInType i env ps a

203 | otherwise = nub $ getFlexInType i env ps f ++

205 | otherwise = nub $ getFlexInType i env ps f ++

204 getFlexInType i env ps a

206 getFlexInType i env ps a

205getFlexInType i _ _ _ = []

207getFlexInType i _ _ _ = []

206

208

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

208-- types, and never in a non-parameter position in a (non-param) argument type.

210-- types, and never in a non-parameter position in a (non-param) argument type.

209−

211+getParamsInType :: IState -> [Name] -> [PArg] -> Type -> [Name]

210getParamsInType i env ps t = let fix = getFixedInType i env ps t

212getParamsInType i env ps t = let fix = getFixedInType i env ps t

211 flex = getFlexInType i env fix t in

213 flex = getFlexInType i env fix t in

212 [x | x <- fix, not (x `elem` flex)]

214 [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