db69077 · Idris-dev · git.iko.soy

libs/contrib/Control/ST.idr+1−1

compare with master

unifiedsplit

@@ -399,7 +399,7 @@ runST env (Write lbl prf val) k = k () (updateEnv prf env val)

399runSTLoop : Fuel -> Env invars -> STransLoop m a invars outfn ->

400 (k : (x : a) -> Env (outfn x) -> m b) ->

401 (onDry : m b) -> m b

402−runSTLoop Empty _ _ _ onDry = onDry

402+runSTLoop Dry _ _ _ onDry = onDry

403runSTLoop (More x) env (Bind prog next) k onDry

404 = runST env prog (\prog', env' => runSTLoop x env' (next prog') k onDry)

405runSTLoop (More x) env (Pure result) k onDry = k result env

libs/prelude/Builtins.idr+1−1

@@ -89,7 +89,7 @@ replace Refl prf = prf

89||| in the other direction, which puts it in a form usable by the `rewrite`

90||| tactic and term.

91rewrite__impl : (P : a -> Type) -> x = y -> P y -> P x

92−rewrite__impl P Refl prf = prf

92+rewrite__impl p Refl prf = prf

93

94||| Symmetry of propositional equality

95sym : {left:a} -> {right:b} -> left = right -> right = left

libs/prelude/Prelude/WellFounded.idr+2−2

@@ -60,8 +60,8 @@ accRec step z (Access f) =

60accInd : {rel : a -> a -> Type} -> {P : a -> Type} ->

61 (step : (x : a) -> ((y : a) -> rel y x -> P y) -> P x) ->

62 (z : a) -> Accessible rel z -> P z

63−accInd {P} step z (Access f) =

63+accInd {P=p} step z (Access f) =

64− step z $ \y, lt => accInd {P} step y (f y lt)

64+ step z $ \y, lt => accInd {P=p} step y (f y lt)

65

66

67||| Use well-foundedness of a relation to write terminating operations.

libs/pruviloj/Pruviloj/Core.idr+9−9

@@ -234,12 +234,12 @@ getTTType r = snd <$> check !getEnv r

234both : Raw -> TTName -> TTName -> Elab ()

235both tm n1 n2 =

236 do -- We don't know that the term is canonical, so let-bind projections applied to it

237− (A, B) <- isPairTy !(getTTType tm)

237+ (a, b) <- isPairTy !(getTTType tm)

238− remember n1 A; apply `(fst {a=~A} {b=~B} ~tm) []; solve

238+ remember n1 a; apply `(fst {a=~a} {b=~b} ~tm) []; solve

239− remember n2 B; apply `(snd {a=~A} {b=~B} ~tm) []; solve

239+ remember n2 b; apply `(snd {a=~a} {b=~b} ~tm) []; solve

240 where

241 isPairTy : TT -> Elab (Raw, Raw)

242− isPairTy `((~A, ~B) : Type) = [| MkPair (forget A) (forget B) |]

242+ isPairTy `((~a, ~b) : Type) = [| MkPair (forget a) (forget b) |]

243 isPairTy tm = fail [TermPart tm, TextPart "is not a pair"]

244

245||| Let-bind all results of completely destructuring nested tuples.

@@ -282,8 +282,8 @@ construct = case headName !goalType of

282reflexivity : Elab ()

283reflexivity =

284 case !goalType of

285− `((=) {A=~A} {B=~_} ~x ~_) =>

285+ `((=) {A=~a} {B=~_} ~x ~_) =>

286− do fill `(Refl {A=~A} {x=~x})

286+ do fill `(Refl {A=~a} {x=~x})

287 solve

288 _ => fail [ TextPart "The goal is not an equality, so"

289 , NamePart `{reflexivity}

@@ -307,9 +307,9 @@ symmetry =

307symmetryAs : (t : Raw) -> (hint : String) -> Elab TTName

308symmetryAs t hint =

309 case !(getTTType t) of

310− `((=) {A=~A} {B=~B} ~l ~r) =>

310+ `((=) {A=~a} {B=~b} ~l ~r) =>

311− do af <- forget A

311+ do af <- forget a

312− bf <- forget B

312+ bf <- forget b

313 lf <- forget l

314 rf <- forget r

315 let ts = the Raw $ `(sym {a=~af} {b=~bf} {left=~lf} {right=~rf} ~t)

libs/pruviloj/Pruviloj/Derive/DecEq.idr+4−4

@@ -82,7 +82,7 @@ partial

82mkRhs : (fn, fam : TTName) -> Nat -> Elab ()

83mkRhs fn fam k =

84 case snd !getGoal of

85− `(Dec ((=) {A=~A} {B=~_} ~x ~y)) =>

85+ `(Dec ((=) {A=~_} {B=~_} ~x ~y)) =>

86 let (c1, args1) = unApply x

87 (c2, args2) = unApply y

88 in if c1 /= c2

@@ -138,17 +138,17 @@ deriveDecEq : (fn : TTName) -> Elab ()

138deriveDecEq fn =

139 do (_, Ref, sig') <- lookupTyExact fn

140 sig <- forget sig'

141− (args, `(Dec ((=) {A=~A} {B=~_} ~(Var x) ~(Var y)))) <- stealBindings sig noRenames

141+ (args, `(Dec ((=) {A=~aTy} {B=~_} ~(Var x) ~(Var y)))) <- stealBindings sig noRenames

142 | other => fail [ TextPart "Return type"

143 , RawPart (snd other)

144 , TextPart "isn't decidable equality"

145 ]

146

147− datatype <- maybe (fail [ RawPart A

147+ datatype <- maybe (fail [ RawPart aTy

148 , TextPart "is not an application of a TC"

149 ])

150 lookupDatatypeExact

151− (headName A)

151+ (headName aTy)

152

153 -- the signature must be like this:

154 -- 1. a collection of variable bindings (will be implicit)

libs/pruviloj/Pruviloj/Disjoint.idr+2−2

@@ -78,7 +78,7 @@ disjoint =

78 do compute

79 g <- snd <$> getGoal

80 case g of

81− `(((=) {A=~A} {B=~B} ~a ~b) -> Void) =>

81+ `(((=) {A=~aTy} {B=~bTy} ~a ~b) -> Void) =>

82 do Just lHead <- headName <$> forget a

83 | Nothing => fail [TermPart a, TextPart "doesn't have a name at the head"]

84 Just rHead <- headName <$> forget b

@@ -101,7 +101,7 @@ discriminate =

101 -- for each thing in the context, until we find one that succeeds

102 flip choiceMap !getEnv $ \(n, b) =>

103 do -- 1) check if it is an equality

104− `(((=) {A=~A} {B=~B} ~a ~b)) <- forget (binderTy b)

104+ `(((=) {A=~aTy} {B=~bTy} ~a ~b)) <- forget (binderTy b)

105 | _ => fail [TextPart "Not equality type"]

106 -- 2) check if both sides of the equality have heads

107 case (headName a, headName b) of

libs/pruviloj/Pruviloj/Injective.idr+1−1

@@ -97,7 +97,7 @@ injective : (tm : Raw) -> (n : TTName) -> Elab ()

97injective tm n =

98 do (_, ty) <- check !getEnv tm

99 case !(forget ty) of

100− `((=) {A=~A} {B=~B} ~x ~y) =>

100+ `((=) {A=~a} {B=~b} ~x ~y) =>

101 case (headName x, headName y) of

102 (Just xHd, Just yHd) =>

103 if xHd /= yHd

src/Idris/AbsSyntax.hs+6−1

@@ -30,6 +30,7 @@ import Control.Applicative

30import Control.Monad.State

31import Prelude hiding (Applicative, Foldable, Traversable, (<$>))

32

33+import Data.Char

33import Data.Either

34import Data.Either

34import Data.List hiding (insert, union)

35import Data.List hiding (insert, union)

35import qualified Data.Map as M

36import qualified Data.Map as M

@@ -1982,7 +1983,11 @@ aiFn topname inpat True qq imp_meths ist fc f ffc ds []

1982 | inpat && implicitable f && unqualified f = Right $ PPatvar ffc f

1983 | inpat && implicitable f && unqualified f = Right $ PPatvar ffc f

1983 | otherwise

1984 | otherwise

1984 = case lookupDef f (tt_ctxt ist) of

1985 = case lookupDef f (tt_ctxt ist) of

1986+ [] -> case f of

1985− [] -> Right $ PPatvar ffc f

1987+ MN _ _ -> Right $ PPatvar ffc f

1988+ UN xs | isDigit (T.head xs) -- for partial evaluation vars

1989+ -> Right $ PPatvar ffc f

1990+ _ -> Left $ Msg $ show f ++ " is not a valid name for a pattern variable"

1986 alts -> let ialts = lookupCtxtName f (idris_implicits ist) in

1991 alts -> let ialts = lookupCtxtName f (idris_implicits ist) in

1987 -- trace (show f ++ " " ++ show (fc, any (all imp) ialts, ialts, any constructor alts)) $

1992 -- trace (show f ++ " " ++ show (fc, any (all imp) ialts, ialts, any constructor alts)) $

1988 if (not (vname f) || tcname f

1993 if (not (vname f) || tcname f

src/Idris/Core/TT.hs+2−1

@@ -581,7 +581,8 @@ tcname _ = False

581

582implicitable (NS n _) = False

583implicitable (UN xs) | T.null xs = False

584− | otherwise = isLower (T.head xs) || T.head xs == '_'

584+ | otherwise = isLower (T.head xs) ||

585+ T.head xs == '_'

585implicitable (MN _ x) = not (tnull x) && thead x /= '_'

586implicitable (MN _ x) = not (tnull x) && thead x /= '_'

586implicitable _ = False

587implicitable _ = False

587

588

test/disambig002/disambig002.idr+2−2

@@ -8,7 +8,7 @@ Dec0 : Type -> Type

8Dec0 = Dec

9

10Dec1 : {A : Type} -> (P : A -> Type) -> Type

11−Dec1 {A} P = (a : A) -> Dec0 (P a)

11+Dec1 {A=aTy} p = (a : aTy) -> Dec0 (p a)

12

13Unique : Type -> Type

14Unique t = (p : t) -> (q : t) -> p = q

@@ -41,7 +41,7 @@ namespace Finite

41

42 ||| Notion of finiteness for types

43 Finite : Type -> Type

44− Finite A = Exists (\ n => Iso A (Fin n))

44+ Finite a = Exists (\ n => Iso a (Fin n))

45

46 ||| Cardinality of finite types

47 card : {A : Type} -> (fA : Finite A) -> Nat

test/dsl002/Resimp.idr+1−1

@@ -91,7 +91,7 @@ using (i: Fin n, gam : Vect n Ty, gam' : Vect n Ty, gam'' : Vect n Ty)

91 Args gam as -> Args gam (interpTy a :: as)

92

93 funTy : List Type -> Ty -> Ty

94− funTy list.Nil t = t

94+ funTy List.Nil t = t

95 funTy (a :: as) t = a :-> funTy as t

96

97 data Res : Vect n Ty -> Vect n Ty -> Ty -> Type where

test/proof002/Reflect.idr+45−45

@@ -6,7 +6,7 @@ import Decidable.Equality

6%default total

7%language FirstClassReflection

8

9−using (xs : List a, ys : List a, G : List (List a))

9+using (xs : List a, ys : List a, gam : List (List a))

10

11 data Elem : a -> List a -> Type where

12 Stop : Elem x (x :: xs)

@@ -16,20 +16,20 @@ using (xs : List a, ys : List a, G : List (List a))

16-- and over a set of list variables.

17

18 data Expr : List (List a) -> List a -> Type where

19− App : Expr G xs -> Expr G ys -> Expr G (xs ++ ys)

19+ App : Expr gam xs -> Expr gam ys -> Expr gam (xs ++ ys)

20− Var : Elem xs G -> Expr G xs

20+ Var : Elem xs gam -> Expr gam xs

21− ENil : Expr G []

21+ ENil : Expr gam []

22

23-- Reflection of list equalities, indexed over the concrete equality.

24

25 data ListEq : List (List a) -> Type -> Type where

26− EqP : Expr G xs -> Expr G ys -> ListEq G (xs = ys)

26+ EqP : Expr gam xs -> Expr gam ys -> ListEq gam (xs = ys)

27

28-- Fully right associative list expressions

29

30 data RExpr : List (List a) -> List a -> Type where

31− RApp : RExpr G xs -> Elem ys G -> RExpr G (xs ++ ys)

31+ RApp : RExpr gam xs -> Elem ys gam -> RExpr gam (xs ++ ys)

32− RNil : RExpr G []

32+ RNil : RExpr gam []

33

34-- Convert an expression to a right associative expression, and return

35-- a proof that the rewriting has an equal interpretation to the original

@@ -38,7 +38,7 @@ using (xs : List a, ys : List a, G : List (List a))

38-- The idea is that we use this proof to build a proof of equality of

39-- list appends

40

41− expr_r : Expr G xs -> (xs' ** (RExpr G xs', xs = xs'))

41+ expr_r : Expr gam xs -> (xs' ** (RExpr gam xs', xs = xs'))

42 expr_r ENil = (_ ** (RNil, Refl))

43 expr_r (Var i) = (_ ** (RApp RNil i, Refl))

44 expr_r (App ex ey) = let (xl ** (xr, xprf)) = expr_r ex in

@@ -46,29 +46,29 @@ using (xs : List a, ys : List a, G : List (List a))

46 appRExpr _ _ xr yr xprf yprf

47 where

48 appRExpr : (xs', ys' : List a) ->

49− {G : List (List a)} -> {xs, ys : List a} ->

49+ {gam : List (List a)} -> {xs, ys : List a} ->

50− RExpr G xs -> RExpr G ys -> (xs' = xs) -> (ys' = ys) ->

50+ RExpr gam xs -> RExpr gam ys -> (xs' = xs) -> (ys' = ys) ->

51− (ws' ** (RExpr G ws', xs' ++ ys' = ws'))

51+ (ws' ** (RExpr gam ws', xs' ++ ys' = ws'))

52 appRExpr x' y' rxs (RApp e i) xprf yprf

53 = let (xs ** (rec, prf)) = appRExpr _ _ rxs e Refl Refl in

54 (_ ** (RApp rec i, ?appRExpr1))

55 appRExpr x' y' rxs RNil xprf yprf = (_ ** (rxs, ?appRExpr2))

56

57− r_expr : RExpr G xs -> Expr G xs

57+ r_expr : RExpr gam xs -> Expr gam xs

58 r_expr RNil = ENil

59 r_expr (RApp xs i) = App (r_expr xs) (Var i)

60

61-- Convert an expression to some other equivalent expression (which

62-- just happens to be normalised to right associative form)

63

64− reduce : Expr G xs -> (xs' ** (Expr G xs', xs = xs'))

64+ reduce : Expr gam xs -> (xs' ** (Expr gam xs', xs = xs'))

65 reduce e = let (x' ** (e', prf)) = expr_r e in

66 (x' ** (r_expr e', prf))

67

68-- Build a proof that two expressions are equal. If they are, we'll know

69-- that the indices are equal.

70

71− eqExpr : (e : Expr G xs) -> (e' : Expr G ys) ->

71+ eqExpr : (e : Expr gam xs) -> (e' : Expr gam ys) ->

72 Maybe (e = e')

73 eqExpr (App x y) (App x' y') with (eqExpr x x', eqExpr y y')

74 eqExpr (App x y) (App x y) | (Just Refl, Just Refl) = Just Refl

@@ -83,20 +83,20 @@ using (xs : List a, ys : List a, G : List (List a))

83-- they are equal

84

85 buildProof : {xs : List a} -> {ys : List a} ->

86− Expr G ln -> Expr G rn ->

86+ Expr gam ln -> Expr gam rn ->

87 (xs = ln) -> (ys = rn) -> Maybe (xs = ys)

88 buildProof e e' lp rp with (eqExpr e e')

89 buildProof e e lp rp | Just Refl = ?bp1

90 buildProof e e' lp rp | Nothing = Nothing

91

92− testEq : Expr G xs -> Expr G ys -> Maybe (xs = ys)

92+ testEq : Expr gam xs -> Expr gam ys -> Maybe (xs = ys)

93 testEq l r = let (ln ** (l', lPrf)) = reduce l in

94 let (rn ** (r', rPrf)) = reduce r in

95 buildProof l' r' lPrf rPrf

96

97-- Given a reflected equality, try to produce a proof that holds

98

99− prove : ListEq G t -> Maybe t

99+ prove : ListEq gam t -> Maybe t

100 prove (EqP xs ys) = testEq xs ys

101

102 getJust : (x : Maybe a) -> IsJust x -> a

@@ -114,15 +114,15 @@ using (xs : List a, ys : List a, G : List (List a))

114 isElem x (x :: ys) | Just Refl = [| Stop |]

115 isElem x (y :: ys) | Nothing = [| Pop (isElem x ys) |]

116

117− weakenElem : (G' : List a) -> Elem x xs -> Elem x (G' ++ xs)

117+ weakenElem : (gam' : List a) -> Elem x xs -> Elem x (gam' ++ xs)

118 weakenElem [] p = p

119− weakenElem (g :: G) p = Pop (weakenElem G p)

119+ weakenElem (g :: gam) p = Pop (weakenElem gam p)

120

121− weaken : (G' : List (List a)) ->

121+ weaken : (gam' : List (List a)) ->

122− Expr G xs -> Expr (G' ++ G) xs

122+ Expr gam xs -> Expr (gam' ++ gam) xs

123− weaken G' (App l r) = App (weaken G' l) (weaken G' r)

123+ weaken gam' (App l r) = App (weaken gam' l) (weaken gam' r)

124− weaken G' (Var x) = Var (weakenElem G' x)

124+ weaken gam' (Var x) = Var (weakenElem gam' x)

125− weaken G' ENil = ENil

125+ weaken gam' ENil = ENil

126

127

128-- Now, some reflection magic.

@@ -133,21 +133,21 @@ using (xs : List a, ys : List a, G : List (List a))

133-- reduction will work the right way.

134

135%reflection

136−reflectList : (G : List (List a)) ->

136+reflectList : (gam : List (List a)) ->

137− (xs : List a) -> (G' ** Expr (G' ++ G) xs)

137+ (xs : List a) -> (gam' ** Expr (gam' ++ gam) xs)

138−reflectList G [] = ([] ** ENil)

138+reflectList gam [] = ([] ** ENil)

139−

139+

140−reflectList G (x :: xs) with (reflectList G xs)

140+reflectList gam (x :: xs) with (reflectList gam xs)

141− | (G' ** xs') with (isElem (List.(::) x []) (G' ++ G))

141+ | (gam' ** xs') with (isElem (List.(::) x []) (gam' ++ gam))

142− | Just p = (G' ** App (Var p) xs')

142+ | Just p = (gam' ** App (Var p) xs')

143− | Nothing = ([x] :: G' ** App (Var Stop) (weaken [[x]] xs'))

143+ | Nothing = ([x] :: gam' ** App (Var Stop) (weaken [[x]] xs'))

144−

144+

145−reflectList G (xs ++ ys) with (reflectList G xs)

145+reflectList gam (xs ++ ys) with (reflectList gam xs)

146− | (G' ** xs') with (reflectList (G' ++ G) ys)

146+ | (gam' ** xs') with (reflectList (gam' ++ gam) ys)

147− | (G'' ** ys') = ((G'' ++ G') **

147+ | (gam'' ** ys') = ((gam'' ++ gam') **

148− rewrite (sym (appendAssociative G'' G' G)) in

148+ rewrite (sym (appendAssociative gam'' gam' gam)) in

149− App (weaken G'' xs') ys')

149+ App (weaken gam'' xs') ys')

150−reflectList G t with (isElem t G)

150+reflectList gam t with (isElem t gam)

151 | Just p = ([] ** Var p)

152 | Nothing = ([t] ** Var Stop)

153

@@ -160,12 +160,12 @@ reflectList G t with (isElem t G)

160-- forms of equality proofs anyway.

161

162%reflection

163−reflectEq : (a : Type) -> (G : List (List a)) -> (P : Type) -> (G' ** ListEq (G' ++ G) P)

163+reflectEq : (a : Type) -> (gam : List (List a)) -> (P : Type) -> (gam' ** ListEq (gam' ++ gam) P)

164−reflectEq a G (the (List a) xs = the (List a) ys) with (reflectList G xs)

164+reflectEq a gam (the (List a) xs = the (List a) ys) with (reflectList gam xs)

165− | (G' ** xs') with (reflectList (G' ++ G) ys)

165+ | (gam' ** xs') with (reflectList (gam' ++ gam) ys)

166− | (G'' ** ys') = ((G'' ++ G') **

166+ | (gam'' ** ys') = ((gam'' ++ gam') **

167− rewrite (sym (appendAssociative G'' G' G)) in

167+ rewrite (sym (appendAssociative gam'' gam' gam)) in

168− EqP (weaken G'' xs') ys')

168+ EqP (weaken gam'' xs') ys')

169

170

171-- Need these before we can test it or the reductions won't normalise fully...

test/regression001/reg001.idr+1−1

@@ -53,7 +53,7 @@ vfoldl P cons nil (x :: xs)

53total soElim : (C : (b : Bool) -> So b -> Type) ->

54 C True Oh ->

55 (b : Bool) -> (s : So b) -> (C b s)

56−soElim C coh True Oh = coh

56+soElim c coh True Oh = coh

57

58soFalseElim : So False -> a

59soFalseElim x = void (soElim C () False x)

test/regression001/reg004.lidr+14−14

@@ -6,9 +6,9 @@

6> (Functor F) => (Functor G) =>

7> (t : {A : Type} -> F A -> G A) ->

8> Type

9−> Natural {F} {G} t = {A, B : Type} ->

9+> Natural {F=fF} {G=gG} t = {A, B : Type} ->

10> (f : A -> B) ->

11−> (x : F A) ->

11+> (x : fF A) ->

12> t (map f x) = map f (t x)

13

14> Monotone : {B, C : Type} -> {F : Type -> Type} -> (Functor F) =>

@@ -16,13 +16,13 @@

16> (LTE_C : C -> C -> Type) ->

17> (measure : F B -> C) ->

18> Type

19−> Monotone {B} {C} {F} LTE_B LTE_C measure =

19+> Monotone {B=bB} {C=cC} {F=fF} lte_B lte_C measure =

20> {A : Type} ->

21−> (f : A -> B) ->

21+> (f : A -> bB) ->

22−> (g : A -> B) ->

22+> (g : A -> bB) ->

23−> (p : (a : A) -> f a `LTE_B` g a) ->

23+> (p : (a : A) -> f a `lte_B` g a) ->

24−> (x : F A) ->

24+> (x : fF A) ->

25−> measure (map f x) `LTE_C` measure (map g x)

25+> measure (map f x) `lte_C` measure (map g x)

26

27> monotoneNaturalLemma: {B, C : Type} -> {F : Type -> Type} -> (Functor F) =>

28> (LTE_B : B -> B -> Type) ->

@@ -32,12 +32,12 @@

32> (t : {A : Type} -> F A -> F A) ->

33> Natural t ->

34> Monotone LTE_B LTE_C (measure . t)

35−> monotoneNaturalLemma {B} {C} {F} LTE_B LTE_C m mm t nt = mmt where

35+> monotoneNaturalLemma {B=bB} {C=cC} {F=fF} lte_B lte_C m mm t nt = mmt where

36> mmt : {A : Type} ->

37−> (f : A -> B) ->

37+> (f : A -> bB) ->

38−> (g : A -> B) ->

38+> (g : A -> bB) ->

39−> (p : (a : A) -> f a `LTE_B` g a) ->

39+> (p : (a : A) -> f a `lte_B` g a) ->

40−> (x : F A) ->

40+> (x : fF A) ->

41−> m (t {A = B} (map f x)) `LTE_C` m (t {A = B} (map g x))

41+> m (t {A = bB} (map f x)) `lte_C` m (t {A = bB} (map g x))

42> mmt = ?kika

43

test/regression001/reg046.idr+4−4

@@ -10,10 +10,10 @@ elimList : (A : Type) ->

10 (f2 : (a : A) -> (as : MyList A) -> m as -> m (MyCons A a as)) ->

11 (e : MyList A) ->

12 m e

13−elimList A m f1 f2 (MyNil A) = f1

13+elimList aA m f1 f2 (MyNil aA) = f1

14−elimList A m f1 f2 (MyCons A a as) = f2 a as (elimList A m f1 f2 as)

14+elimList aA m f1 f2 (MyCons aA a as) = f2 a as (elimList aA m f1 f2 as)

15

16append : (A : Type) -> (b : MyList A) -> (c : MyList A) -> MyList A

17−append A b c = (elimList A (\ d => MyList A) c

17+append aA b c = (elimList aA (\ d => MyList aA) c

18− (\ d => \ e => \ f => MyCons A d f)

18+ (\ d => \ e => \ f => MyCons aA d f)

19 b)

test/regression001/reg047.idr+2−2

@@ -6,10 +6,10 @@ data TTSigma : (A : Type) -> (B : A -> Type) -> Type where

6data Nat = Zero | Succ Nat

7

8Id : (A : Type) -> A -> A -> Type

9−Id A = (=) {A = A} {B = A}

9+Id aTy = (=) {A = aTy} {B = aTy}

10

11IdRefl : (A : Type) -> (a : A) -> Id A a a

12−IdRefl A a = Refl {x = a}

12+IdRefl aTy a = Refl {x = a}

13

14zzz : Id Nat Zero Zero

15zzz = IdRefl Nat Zero

test/regression001/reg047a.idr+1−1

@@ -9,7 +9,7 @@ Id : (A : Type) -> A -> A -> Type

9Id = \A,x,y => x = y -- {a = A} {b = A}

10

11IdRefl : (A : Type) -> (a : A) -> Id A a a

12−IdRefl A a = Refl {x = a}

12+IdRefl aTy a = Refl {x = a}

13

14zzzz : Id MNat Zero Zero

15zzzz = IdRefl MNat Zero

test/regression001/reg062.lidrdeleted−41

@@ -1,41 +0,0 @@

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/regression001/reg064.idr+1−1

@@ -5,4 +5,4 @@ sigmaEq2 : {A : Type} ->

5 fst s1 = fst s2 ->

6 snd s1 = snd s2 ->

7 s1 = s2

8−sigmaEq2 {A} {P} {s1 = (x ** prf)} {s2 = (x ** prf)} Refl Refl = Refl

8+sigmaEq2 {A=a} {P=p} {s1 = (x ** prf)} {s2 = (x ** prf)} Refl Refl = Refl

test/regression001/run+1−1

@@ -13,6 +13,6 @@ ${IDRIS:-idris} $@ --check \

13${IDRIS:-idris} $@ --check --nobuiltins reg047.idr

14

15${IDRIS:-idris} $@ --check --nocolour \

16− reg062.lidr reg073.lidr

16+ reg073.lidr

17

18rm -f *.ibc

test/regression002/expected+8

@@ -5,6 +5,14 @@ reg001.idr:2:1-9:

5When checking left hand side of foo:

6Can't match on foo a a x

7

8+reg002.idr:3:1-19:

9+ |

10+3 | append (X :: XS) ys = X :: append XS ys

11+ | ~~~~~~~~~~~~~~~~~~~

12+When checking left hand side of append:

13+When checking argument x to constructor Prelude.List.:::

14+ X is not a valid name for a pattern variable

15+

8reg003a.idr:4:13-38:

16reg003a.idr:4:13-38:

9 |

17 |

104 | ECons : Nat -> OddList -> EvenList

184 | ECons : Nat -> OddList -> EvenList

test/regression002/reg002.idrnew file+3

@@ -0,0 +1,3 @@

1+append : List a -> List a -> List a

2+append [] ys = ys

3+append (X :: XS) ys = X :: append XS ys

test/regression002/run+1

@@ -2,6 +2,7 @@

2

3${IDRIS:-idris} $@ --nobanner --nocolour --quiet --port none <<!

4:load reg001.idr

5+:load reg002.idr

5:load reg003.idr

6:load reg003.idr

6:load reg003a.idr

7:load reg003a.idr

7:load reg006.idr

8:load reg006.idr

test/sugar005/As.idr+1−1

@@ -8,7 +8,7 @@ isS n@(S _) = Just n

8-- Test @ under a constructor

9hasS : List Nat -> Maybe Nat

10hasS (Z::xs) = hasS xs

11−hasS (n@(S_)::xs) = Just n

11+hasS (n@(S _)::xs) = Just n

12hasS _ = Nothing

13

14-- Test nested @s

test/totality011/totality011.lidr+2−2

@@ -20,10 +20,10 @@

20> t'' `GTE` t

21

22> weCanOnlyGetOlder {t'' = Z} {t = Z} _ _ _ = LTEZero

23−> weCanOnlyGetOlder {t'' = Z} {t = S m} _ _ (Zeqt , _) =

23+> weCanOnlyGetOlder {t'' = Z} {t = S m} _ _ (zeqt , _) =

24> void (uninhabited u) where

25> u : Z = S m

26−> u = trans Zeqt Refl

26+> u = trans zeqt Refl

27

28> weCanOnlyGetOlder {t'' = S _} {t = S _} _ _ _ = ?foo

29