ce403f6 · Idris-dev · git.iko.soy

CHANGELOG+5−1

compare with master

unifiedsplit

@@ -12,7 +12,10 @@ Language updates

12* The previous syntax for tactic proofs and the previous interactive prover

13 are now deprecated in favour of reflected elaboration. They will be removed

14 at some point in the future.

15−

15+* Changed scoping rules for unbound implicits: any name which would be a

16+ valid unbound implicit is now *always* an unbound implicit. This is much

17+ more resilient to changes in inputs, but does require that function names

18+ be explicitly qualified when in argument position.

16

19

17Library updates

20Library updates

18---------------

21---------------

@@ -22,6 +25,7 @@ Library updates

22* A special version of (-) on 'Nat' requires that the second argument is

25* A special version of (-) on 'Nat' requires that the second argument is

23 smaller than or equal to the first. 'minus' retains the old behaviour,

26 smaller than or equal to the first. 'minus' retains the old behaviour,

24 returning Z if there is an underflow.

27 returning Z if there is an underflow.

28+* The (+), (-), and (*) operations on Fin have been removed.

25* New Logging Effects have been added to facilitate logging of effectful

29* New Logging Effects have been added to facilitate logging of effectful

26 programmes.

30 programmes.

27* Elaborator reflection is now a part of the prelude. It is no longer

31* Elaborator reflection is now a part of the prelude. It is no longer

config.mk+4

@@ -26,11 +26,15 @@ ifneq (, $(findstring cygwin, $(MACHINE)))

26else

27ifneq (, $(findstring mingw, $(MACHINE)))

28 OS :=windows

29+else

30+ifneq (, $(findstring windows, $(MACHINE)))

31+ OS :=windows

29else

32else

30 OS :=unix

33 OS :=unix

31endif

34endif

32endif

35endif

33endif

36endif

37+endif

34

38

35ifeq ($(OS),darwin)

39ifeq ($(OS),darwin)

36 SHLIB_SUFFIX :=.dylib

40 SHLIB_SUFFIX :=.dylib

docs/tutorial/starting.rst+2

@@ -66,6 +66,8 @@ Some useful options to the Idris command are:

66

67- ``--check`` type check the file and its dependencies without starting the interactive environment.

68

69+- ``--package pkg`` add package as dependency, e.g. ``--package contrib`` to make use of the contrib package.

70+

69- ``--help`` display usage summary and command line options.

71- ``--help`` display usage summary and command line options.

70

72

71The Interactive Environment

73The Interactive Environment

idris.cabal+4−1

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

1Name: idris

2−Version: 0.9.19

2+Version: 0.9.19.1

3License: BSD3

4License-file: LICENSE

5Author: Edwin Brady

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

346 test/basic014/run

347 test/basic014/*.idr

348 test/basic014/expected

349+ test/basic015/run

350+ test/basic015/*.idr

351+ test/basic015/expected

349

352

350 test/bignum001/run

353 test/bignum001/run

351 test/bignum001/*.idr

354 test/bignum001/*.idr

libs/base/Data/Fin.idr+2−20

@@ -42,7 +42,7 @@ finToNatInjective FZ FZ Refl = Refl

42finToNatInjective (FS m) FZ Refl impossible

43finToNatInjective FZ (FS n) Refl impossible

44finToNatInjective (FS m) (FS n) prf =

45− cong (finToNatInjective m n (succInjective (finToNat m) (finToNat n) prf))

45+ cong (finToNatInjective m n (succInjective (finToNat m) (finToNat n) prf))

46

47instance Cast (Fin n) Nat where

48 cast x = finToNat x

@@ -94,7 +94,7 @@ instance Ord (Fin n) where

94 compare FZ (FS _) = LT

95 compare (FS _) FZ = GT

96 compare (FS x) (FS y) = compare x y

97−

97+

98instance MinBound (Fin (S n)) where

99 minBound = FZ

100

@@ -102,24 +102,6 @@ instance MaxBound (Fin (S n)) where

102 maxBound = last

103

104

105−||| Add two Fins, extending the bound

106−(+) : Fin n -> Fin m -> Fin (n + m)

107−(+) {n=S n} {m=m} FZ f' = rewrite plusCommutative n m in weaken (weakenN n f')

108−(+) (FS f) f' = FS (f + f')

109−

110−||| Substract two Fins, keeping the bound of the minuend

111−(-) : Fin n -> Fin m -> Fin n

112−FZ - _ = FZ

113−f - FZ = f

114−(FS f) - (FS f') = weaken $ f - f'

115−

116−||| Multiply two Fins, extending the bound

117−(*) : Fin n -> Fin m -> Fin (n * m)

118−(*) {n=Z} f f' = FinZElim f

119−(*) {m=Z} f f' = FinZElim f'

120−(*) {n=S n} {m=S m} FZ f' = FZ

121−(*) {n=S n} {m=S m} (FS f) f' = f' + (f * f')

122−

123-- Construct a Fin from an integer literal which must fit in the given Fin

105-- Construct a Fin from an integer literal which must fit in the given Fin

124

106

125natToFin : Nat -> (n : Nat) -> Maybe (Fin n)

107natToFin : Nat -> (n : Nat) -> Maybe (Fin n)

libs/contrib/Classes/Verified.idr+13−16

@@ -17,12 +17,10 @@ class Functor f => VerifiedFunctor (f : Type -> Type) where

17 (g1 : a -> b) -> (g2 : b -> c) ->

18 map (g2 . g1) x = (map g2 . map g1) x

19

20−

21−

22class (Applicative f, VerifiedFunctor f) => VerifiedApplicative (f : Type -> Type) where

20class (Applicative f, VerifiedFunctor f) => VerifiedApplicative (f : Type -> Type) where

23 applicativeMap : (x : f a) -> (g : a -> b) ->

21 applicativeMap : (x : f a) -> (g : a -> b) ->

24 map g x = pure g <*> x

22 map g x = pure g <*> x

25− applicativeIdentity : (x : f a) -> pure id <*> x = x

23+ applicativeIdentity : (x : f a) -> pure Basics.id <*> x = x

26 applicativeComposition : (x : f a) -> (g1 : f (a -> b)) -> (g2 : f (b -> c)) ->

24 applicativeComposition : (x : f a) -> (g1 : f (a -> b)) -> (g2 : f (b -> c)) ->

27 ((pure (.) <*> g2) <*> g1) <*> x = g2 <*> (g1 <*> x)

25 ((pure (.) <*> g2) <*> g1) <*> x = g2 <*> (g1 <*> x)

28 applicativeHomomorphism : (x : a) -> (g : a -> b) ->

26 applicativeHomomorphism : (x : a) -> (g : a -> b) ->

@@ -30,14 +28,13 @@ class (Applicative f, VerifiedFunctor f) => VerifiedApplicative (f : Type -> Typ

30 applicativeInterchange : (x : a) -> (g : f (a -> b)) ->

28 applicativeInterchange : (x : a) -> (g : f (a -> b)) ->

31 g <*> pure x = pure (\g' : a -> b => g' x) <*> g

29 g <*> pure x = pure (\g' : a -> b => g' x) <*> g

32

30

33−

34class (Monad m, VerifiedApplicative m) => VerifiedMonad (m : Type -> Type) where

31class (Monad m, VerifiedApplicative m) => VerifiedMonad (m : Type -> Type) where

35 monadApplicative : (mf : m (a -> b)) -> (mx : m a) ->

32 monadApplicative : (mf : m (a -> b)) -> (mx : m a) ->

36 mf <*> mx = mf >>= \f =>

33 mf <*> mx = mf >>= \f =>

37 mx >>= \x =>

34 mx >>= \x =>

38 pure (f x)

35 pure (f x)

39 monadLeftIdentity : (x : a) -> (f : a -> m b) -> return x >>= f = f x

36 monadLeftIdentity : (x : a) -> (f : a -> m b) -> return x >>= f = f x

40− monadRightIdentity : (mx : m a) -> mx >>= return = mx

37+ monadRightIdentity : (mx : m a) -> mx >>= Monad.return = mx

41 monadAssociativity : (mx : m a) -> (f : a -> m b) -> (g : b -> m c) ->

38 monadAssociativity : (mx : m a) -> (f : a -> m b) -> (g : b -> m c) ->

42 (mx >>= f) >>= g = mx >>= (\x => f x >>= g)

39 (mx >>= f) >>= g = mx >>= (\x => f x >>= g)

43

40

@@ -53,8 +50,8 @@ instance VerifiedSemigroup (List a) where

53

50

54

51

55class (VerifiedSemigroup a, Monoid a) => VerifiedMonoid a where

52class (VerifiedSemigroup a, Monoid a) => VerifiedMonoid a where

56− total monoidNeutralIsNeutralL : (l : a) -> l <+> neutral = l

53+ total monoidNeutralIsNeutralL : (l : a) -> l <+> Algebra.neutral = l

57− total monoidNeutralIsNeutralR : (r : a) -> neutral <+> r = r

54+ total monoidNeutralIsNeutralR : (r : a) -> Algebra.neutral <+> r = r

58

55

59-- instance VerifiedMonoid Nat where

56-- instance VerifiedMonoid Nat where

60-- monoidNeutralIsNeutralL = plusZeroRightNeutral

57-- monoidNeutralIsNeutralL = plusZeroRightNeutral

@@ -65,8 +62,8 @@ instance VerifiedMonoid (List a) where

65 monoidNeutralIsNeutralR xs = Refl

62 monoidNeutralIsNeutralR xs = Refl

66

63

67class (VerifiedMonoid a, Group a) => VerifiedGroup a where

64class (VerifiedMonoid a, Group a) => VerifiedGroup a where

68− total groupInverseIsInverseL : (l : a) -> l <+> inverse l = neutral

65+ total groupInverseIsInverseL : (l : a) -> l <+> inverse l = Algebra.neutral

69− total groupInverseIsInverseR : (r : a) -> inverse r <+> r = neutral

66+ total groupInverseIsInverseR : (r : a) -> inverse r <+> r = Algebra.neutral

70

67

71class (VerifiedGroup a, AbelianGroup a) => VerifiedAbelianGroup a where

68class (VerifiedGroup a, AbelianGroup a) => VerifiedAbelianGroup a where

72 total abelianGroupOpIsCommutative : (l, r : a) -> l <+> r = r <+> l

69 total abelianGroupOpIsCommutative : (l, r : a) -> l <+> r = r <+> l

@@ -77,12 +74,12 @@ class (VerifiedAbelianGroup a, Ring a) => VerifiedRing a where

77 total ringOpIsDistributiveR : (l, c, r : a) -> (l <+> c) <.> r = (l <.> r) <+> (c <.> r)

74 total ringOpIsDistributiveR : (l, c, r : a) -> (l <+> c) <.> r = (l <.> r) <+> (c <.> r)

78

75

79class (VerifiedRing a, RingWithUnity a) => VerifiedRingWithUnity a where

76class (VerifiedRing a, RingWithUnity a) => VerifiedRingWithUnity a where

80− total ringWithUnityIsUnityL : (l : a) -> l <.> unity = l

77+ total ringWithUnityIsUnityL : (l : a) -> l <.> Algebra.unity = l

81− total ringWithUnityIsUnityR : (r : a) -> unity <.> r = r

78+ total ringWithUnityIsUnityR : (r : a) -> Algebra.unity <.> r = r

82

79

83--class (VerifiedRingWithUnity a, Field a) => VerifiedField a where

80--class (VerifiedRingWithUnity a, Field a) => VerifiedField a where

84−-- total fieldInverseIsInverseL : (l : a) -> (notId : Not (l = neutral)) -> l <.> (inverseM l notId) = unity

81+-- total fieldInverseIsInverseL : (l : a) -> (notId : Not (l = neutral)) -> l <.> (inverseM l notId) = Algebra.unity

85−-- total fieldInverseIsInverseR : (r : a) -> (notId : Not (r = neutral)) -> (inverseM r notId) <.> r = unity

82+-- total fieldInverseIsInverseR : (r : a) -> (notId : Not (r = neutral)) -> (inverseM r notId) <.> r = Algebra.unity

86

83

87

84

88class JoinSemilattice a => VerifiedJoinSemilattice a where

85class JoinSemilattice a => VerifiedJoinSemilattice a where

@@ -96,10 +93,10 @@ class MeetSemilattice a => VerifiedMeetSemilattice a where

96 total meetSemilatticeMeetIsIdempotent : (e : a) -> meet e e = e

93 total meetSemilatticeMeetIsIdempotent : (e : a) -> meet e e = e

97

94

98class (VerifiedJoinSemilattice a, BoundedJoinSemilattice a) => VerifiedBoundedJoinSemilattice a where

95class (VerifiedJoinSemilattice a, BoundedJoinSemilattice a) => VerifiedBoundedJoinSemilattice a where

99− total boundedJoinSemilatticeBottomIsBottom : (e : a) -> join e bottom = e

96+ total boundedJoinSemilatticeBottomIsBottom : (e : a) -> join e Algebra.bottom = e

100

97

101class (VerifiedMeetSemilattice a, BoundedMeetSemilattice a) => VerifiedBoundedMeetSemilattice a where

98class (VerifiedMeetSemilattice a, BoundedMeetSemilattice a) => VerifiedBoundedMeetSemilattice a where

102− total boundedMeetSemilatticeTopIsTop : (e : a) -> meet e top = e

99+ total boundedMeetSemilatticeTopIsTop : (e : a) -> meet e Algebra.top = e

103

100

104class (VerifiedJoinSemilattice a, VerifiedMeetSemilattice a) => VerifiedLattice a where

101class (VerifiedJoinSemilattice a, VerifiedMeetSemilattice a) => VerifiedLattice a where

105 total latticeMeetAbsorbsJoin : (l, r : a) -> meet l (join l r) = l

102 total latticeMeetAbsorbsJoin : (l, r : a) -> meet l (join l r) = l

@@ -110,7 +107,7 @@ class (VerifiedBoundedJoinSemilattice a, VerifiedBoundedMeetSemilattice a, Verif

110

107

111--class (VerifiedRingWithUnity a, VerifiedAbelianGroup b, Module a b) => VerifiedModule a b where

108--class (VerifiedRingWithUnity a, VerifiedAbelianGroup b, Module a b) => VerifiedModule a b where

112-- total moduleScalarMultiplyComposition : (x,y : a) -> (v : b) -> x <#> (y <#> v) = (x <.> y) <#> v

109-- total moduleScalarMultiplyComposition : (x,y : a) -> (v : b) -> x <#> (y <#> v) = (x <.> y) <#> v

113−-- total moduleScalarUnityIsUnity : (v : b) -> unity {a} <#> v = v

110+-- total moduleScalarUnityIsUnity : (v : b) -> Algebra.unity {a} <#> v = v

114-- total moduleScalarMultDistributiveWRTVectorAddition : (s : a) -> (v, w : b) -> s <#> (v <+> w) = (s <#> v) <+> (s <#> w)

111-- total moduleScalarMultDistributiveWRTVectorAddition : (s : a) -> (v, w : b) -> s <#> (v <+> w) = (s <#> v) <+> (s <#> w)

115-- total moduleScalarMultDistributiveWRTModuleAddition : (s, t : a) -> (v : b) -> (s <+> t) <#> v = (s <#> v) <+> (t <#> v)

112-- total moduleScalarMultDistributiveWRTModuleAddition : (s, t : a) -> (v : b) -> (s <+> t) <#> v = (s <#> v) <+> (t <#> v)

116

113

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

@@ -113,7 +113,7 @@ class Ring a => RingWithUnity a where

113||| forall a b c, a <.> (b <+> c) == (a <.> b) <+> (a <.> c)

114||| forall a b c, (a <+> b) <.> c == (a <.> c) <+> (b <.> c)

115class RingWithUnity a => Field a where

116− inverseM : (x : a) -> Not (x = neutral) -> a

116+ inverseM : (x : a) -> Not (x = Algebra.neutral) -> a

117

118sum' : (Foldable t, Monoid a) => t a -> a

119sum' = concat

libs/effects/Effects.idr+6−11

@@ -254,9 +254,8 @@ execEff : Env m xs -> (p : EffElem e res xs) ->

254 ((v : a) -> Env m (updateResTy v xs p eff) -> m t) -> m t

255execEff (val :: env) Here eff' k

256 = handle val eff' (\v, res => k v (res :: env))

257−-- FIXME: Teach the elaborator to propagate parameters here

258−execEff {e} {a} {res} {resk} (val :: env) (There p) eff k

257+execEff (val :: env) (There p) eff k

259− = execEff {e} {a} {res} {resk} env p eff (\v, env' => k v (val :: env'))

258+ = execEff env p eff (\v, env' => k v (val :: env'))

260

259

261-- Q: Instead of m b, implement as StateT (Env m xs') m b, so that state

260-- Q: Instead of m b, implement as StateT (Env m xs') m b, so that state

262-- updates can be propagated even through failing computations?

261-- updates can be propagated even through failing computations?

@@ -271,11 +270,7 @@ eff env (liftP prf effP) k

271 eff env' effP (\p', envk => k p' (rebuildEnv envk prf env))

270 eff env' effP (\p', envk => k p' (rebuildEnv envk prf env))

272eff env (new (MkEff resTy newEff) res {prf=Refl} effP) k

271eff env (new (MkEff resTy newEff) res {prf=Refl} effP) k

273 = eff (res :: env) effP (\p', (val :: envk) => k p' envk)

272 = eff (res :: env) effP (\p', (val :: envk) => k p' envk)

274−-- FIXME:

275−-- xs is needed explicitly because otherwise the pattern binding for

276−-- 'l' appears too late. Solution seems to be to reorder patterns at the

277−-- end so that everything is in scope when it needs to be.

278−eff {xs = [l ::: x]} env (l :- prog) k

273+eff env (l :- prog) k

279 = let env' = unlabel env in

274 = let env' = unlabel env in

280 eff env' prog (\p', envk => k p' (relabel l envk))

275 eff env' prog (\p', envk => k p' (relabel l envk))

281

276

@@ -325,8 +320,8 @@ run prog {env} = eff env prog (\r, env => pure r)

325|||

320|||

326||| @prog The effectful program to run.

321||| @prog The effectful program to run.

327%no_implicit

322%no_implicit

328−runPure : (prog : EffM id a xs xs') ->

323+runPure : (prog : EffM Basics.id a xs xs') ->

329− {default MkDefaultEnv env : Env id xs} -> a

324+ {default MkDefaultEnv env : Env Basics.id xs} -> a

330runPure prog {env} = eff env prog (\r, env => r)

325runPure prog {env} = eff env prog (\r, env => r)

331

326

332||| Run an effectful program in a given context `m` with a default value for the environment.

327||| Run an effectful program in a given context `m` with a default value for the environment.

@@ -346,7 +341,7 @@ runInit env prog = eff env prog (\r, env => pure r)

346||| @env The environment to use.

341||| @env The environment to use.

347||| @prog The effectful program to run.

342||| @prog The effectful program to run.

348%no_implicit

343%no_implicit

349−runPureInit : (env : Env id xs) -> (prog : EffM id a xs xs') -> a

344+runPureInit : (env : Env Basics.id xs) -> (prog : EffM Basics.id a xs xs') -> a

350runPureInit env prog = eff env prog (\r, env => r)

345runPureInit env prog = eff env prog (\r, env => r)

351

346

352%no_implicit

347%no_implicit

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

@@ -7,7 +7,7 @@ import Prelude.List

7import Prelude.Cast

8import Builtins

9

10−||| Return the ASCII representation of the character.

10+||| Convert the number to its ASCII equivalent.

11chr : Int -> Char

12chr x = if (x >= 0 && x < 0x110000)

13 then assert_total (prim__intToChar x)

@@ -16,7 +16,7 @@ chr x = if (x >= 0 && x < 0x110000)

16instance Cast Int Char where

17 cast = chr

18

19−||| Convert the number to its ASCII equivalent.

19+||| Return the ASCII representation of the character.

20ord : Char -> Int

21ord x = prim__charToInt x

22

src/Idris/AbsSyntaxTree.hs+57−24

@@ -2249,41 +2249,74 @@ boundNamesIn tm = S.toList (ni 0 S.empty tm)

2249

2250-- Return names which are valid implicits in the given term (type).

2251implicitNamesIn :: [Name] -> IState -> PTerm -> [Name]

2252−implicitNamesIn uvars ist tm = nub $ ni 0 [] tm

2252+implicitNamesIn uvars ist tm

2253+ = let (imps, fns) = execState (ni 0 [] tm) ([], []) in

2254+ nub imps \\ nub fns

2253 where

2255 where

2256+ addImp n = do (imps, fns) <- get

2257+ put (n : imps, fns)

2258+ addFn n = do (imps, fns) <- get

2259+ put (imps, n: fns)

2260+

2261+ notCAF [] = False

2262+ notCAF (PExp _ _ _ _ : _) = True

2263+ notCAF (_ : xs) = notCAF xs

2264+

2265+ notHidden (n, _) = case getAccessibility n of

2266+ Hidden -> False

2267+ _ -> True

2268+

2269+ getAccessibility n

2270+ = case lookupDefAccExact n False (tt_ctxt ist) of

2271+ Just (n,t) -> t

2272+ _ -> Public

2273+

2254− ni 0 env (PRef _ _ n)

2274+ ni 0 env (PRef _ _ n@(NS _ _))

2255 | not (n `elem` env)

2275 | not (n `elem` env)

2256− = case lookupTy n (tt_ctxt ist) of

2276+ -- Never implicitly bind if there's a namespace

2257− [] -> [n]

2277+ = addFn n

2258− _ -> if n `elem` uvars then [n] else []

2278+ ni 0 env (PRef _ _ n)

2279+ | not (n `elem` env) && implicitable n || n `elem` uvars = addImp n

2259 ni 0 env (PApp _ f@(PRef _ _ n) as)

2280 ni 0 env (PApp _ f@(PRef _ _ n) as)

2260− | n `elem` uvars = ni 0 env f ++ concatMap (ni 0 env) (map getTm as)

2281+ | n `elem` uvars = do ni 0 env f

2282+ mapM_ (ni 0 env) (map getTm as)

2283+ | otherwise = do case lookupTy n (tt_ctxt ist) of

2284+ [] -> return ()

2285+ _ -> addFn n

2261− | otherwise = concatMap (ni 0 env) (map getTm as)

2286+ mapM_ (ni 0 env) (map getTm as)

2262− ni 0 env (PApp _ f as) = ni 0 env f ++ concatMap (ni 0 env) (map getTm as)

2287+ ni 0 env (PApp _ f as) = do ni 0 env f

2288+ mapM_ (ni 0 env) (map getTm as)

2263− ni 0 env (PAppBind _ f as) = ni 0 env f ++ concatMap (ni 0 env) (map getTm as)

2289+ ni 0 env (PAppBind _ f as) = do ni 0 env f

2290+ mapM_ (ni 0 env) (map getTm as)

2264− ni 0 env (PCase _ c os) = ni 0 env c ++

2291+ ni 0 env (PCase _ c os) = do ni 0 env c

2265 -- names in 'os', not counting the names bound in the cases

2292 -- names in 'os', not counting the names bound in the cases

2266− (nub (concatMap (ni 0 env) (map snd os))

2293+ mapM_ (ni 0 env) (map snd os)

2294+ (imps, fns) <- get

2295+ put ([] ,[])

2267− \\ nub (concatMap (ni 0 env) (map fst os)))

2296+ mapM_ (ni 0 env) (map fst os)

2297+ (impsfst, _) <- get

2298+ put (nub imps \\ nub impsfst, fns)

2268− ni 0 env (PIfThenElse _ c t f) = concatMap (ni 0 env) [c, t, f]

2299+ ni 0 env (PIfThenElse _ c t f) = mapM_ (ni 0 env) [c, t, f]

2269− ni 0 env (PLam fc n _ ty sc) = ni 0 env ty ++ ni 0 (n:env) sc

2300+ ni 0 env (PLam fc n _ ty sc) = do ni 0 env ty; ni 0 (n:env) sc

2270− ni 0 env (PPi p n _ ty sc) = ni 0 env ty ++ ni 0 (n:env) sc

2301+ ni 0 env (PPi p n _ ty sc) = do ni 0 env ty; ni 0 (n:env) sc

2271− ni 0 env (PRewrite _ l r _) = ni 0 env l ++ ni 0 env r

2302+ ni 0 env (PRewrite _ l r _) = do ni 0 env l; ni 0 env r

2272− ni 0 env (PTyped l r) = ni 0 env l ++ ni 0 env r

2303+ ni 0 env (PTyped l r) = do ni 0 env l; ni 0 env r

2273− ni 0 env (PPair _ _ _ l r) = ni 0 env l ++ ni 0 env r

2304+ ni 0 env (PPair _ _ _ l r) = do ni 0 env l; ni 0 env r

2274− ni 0 env (PDPair _ _ _ (PRef _ _ n) t r) = ni 0 env t ++ ni 0 (n:env) r

2305+ ni 0 env (PDPair _ _ _ (PRef _ _ n) t r) = do ni 0 env t; ni 0 (n:env) r

2275− ni 0 env (PDPair _ _ _ l t r) = ni 0 env l ++ ni 0 env t ++ ni 0 env r

2306+ ni 0 env (PDPair _ _ _ l t r) = do ni 0 env l

2307+ ni 0 env t

2308+ ni 0 env r

2276− ni 0 env (PAlternative ns a as) = concatMap (ni 0 env) as

2309+ ni 0 env (PAlternative ns a as) = mapM_ (ni 0 env) as

2277 ni 0 env (PHidden tm) = ni 0 env tm

2310 ni 0 env (PHidden tm) = ni 0 env tm

2278 ni 0 env (PUnifyLog tm) = ni 0 env tm

2311 ni 0 env (PUnifyLog tm) = ni 0 env tm

2279 ni 0 env (PDisamb _ tm) = ni 0 env tm

2312 ni 0 env (PDisamb _ tm) = ni 0 env tm

2280 ni 0 env (PNoImplicits tm) = ni 0 env tm

2313 ni 0 env (PNoImplicits tm) = ni 0 env tm

2281

2314

2282− ni i env (PQuasiquote tm ty) = ni (i + 1) env tm ++

2315+ ni i env (PQuasiquote tm ty) = do ni (i + 1) env tm

2283− maybe [] (ni i env) ty

2316+ maybe (return ()) (ni i env) ty

2284 ni i env (PUnquote tm) = ni (i - 1) env tm

2317 ni i env (PUnquote tm) = ni (i - 1) env tm

2285

2318

2286− ni i env tm = concatMap (ni i env) (children tm)

2319+ ni i env tm = mapM_ (ni i env) (children tm)

2287

2320

2288-- Return names which are free in the given term.

2321-- Return names which are free in the given term.

2289namesIn :: [(Name, PTerm)] -> IState -> PTerm -> [Name]

2322namesIn :: [(Name, PTerm)] -> IState -> PTerm -> [Name]

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

@@ -502,9 +502,10 @@ matchProblems all = processTactic' (MatchProblems all)

502unifyProblems :: Elab' aux ()

503unifyProblems = processTactic' UnifyProblems

504

505−defer :: [Name] -> Name -> Elab' aux ()

505+defer :: [Name] -> Name -> Elab' aux Name

506defer ds n = do n' <- unique_hole n

507 processTactic' (Defer ds n')

508+ return n'

508

509

509deferType :: Name -> Raw -> [Name] -> Elab' aux ()

510deferType :: Name -> Raw -> [Name] -> Elab' aux ()

510deferType n ty ns = processTactic' (DeferType n ty ns)

511deferType n ty ns = processTactic' (DeferType n ty ns)

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

@@ -429,7 +429,8 @@ defer :: [Name] -> Name -> RunTactic

429defer dropped n ctxt env (Bind x (Hole t) (P nt x' ty)) | x == x' =

430 do let env' = filter (\(n, t) -> n `notElem` dropped) env

431 action (\ps -> let hs = holes ps in

432+ ps { usedns = n : usedns ps,

432− ps { holes = hs \\ [x] })

433+ holes = hs \\ [x] })

433 ps <- get

434 ps <- get

434 return (Bind n (GHole (length env') (psnames ps) (mkTy (reverse env') t))

435 return (Bind n (GHole (length env') (psnames ps) (mkTy (reverse env') t))

435 (mkApp (P Ref n ty) (map getP (reverse env'))))

436 (mkApp (P Ref n ty) (map getP (reverse env'))))

src/Idris/Elab/Term.hs+4−6

@@ -611,7 +611,6 @@ elab ist info emode opts fn tm

611 [] -> False

612 _ -> True

613 bindable (NS _ _) = False

614− bindable (UN xs) = True

615 bindable n = implicitable n

614 bindable n = implicitable n

616 elab' ina _ f@(PInferRef fc hls n) = elab' ina (Just fc) (PApp NoFC f [])

615 elab' ina _ f@(PInferRef fc hls n) = elab' ina (Just fc) (PApp NoFC f [])

617 elab' ina fc' tm@(PRef fc hls n)

616 elab' ina fc' tm@(PRef fc hls n)

@@ -981,7 +980,7 @@ elab ist info emode opts fn tm

981 let n' = metavarName (namespace info) n

980 let n' = metavarName (namespace info) n

982 attack

981 attack

983 psns <- getPSnames

982 psns <- getPSnames

984− defer unique_used n'

983+ n' <- defer unique_used n'

985 solve

984 solve

986 highlightSource nfc (AnnName n' (Just MetavarOutput) Nothing Nothing)

985 highlightSource nfc (AnnName n' (Just MetavarOutput) Nothing Nothing)

987 elab' ina fc (PProof ts) = do compute; mapM_ (runTac True ist (elabFC info) fn) ts

986 elab' ina fc (PProof ts) = do compute; mapM_ (runTac True ist (elabFC info) fn) ts

@@ -1057,10 +1056,9 @@ elab ist info emode opts fn tm

1057

1056

1058 let args' = filter (\(n, _) -> n `notElem` argsDropped) args

1057 let args' = filter (\(n, _) -> n `notElem` argsDropped) args

1059

1058

1059+ attack

1060− cname <- unique_hole' True (mkCaseName fn)

1060+ cname' <- defer argsDropped (mkN (mkCaseName fn))

1061− let cname' = mkN cname

1061+ solve

1062−-- elab' ina fc (PMetavar cname')

1063− attack; defer argsDropped cname'; solve

1064

1062

1065 -- if the scrutinee is one of the 'args' in env, we should

1063 -- if the scrutinee is one of the 'args' in env, we should

1066 -- inspect it directly, rather than adding it as a new argument

1064 -- inspect it directly, rather than adding it as a new argument

test/basic009/expected+11−2

@@ -1,4 +1,13 @@

1MAIN-PASS

2−Faulty.idr:6:7:When checking type of Faulty.fault:

2+Faulty.idr:7:7:When checking right hand side of fault:

3−Can't disambiguate name: A.num, B.C.num

3+Type mismatch between

4+ 0 = 0 (Type of Refl)

5+and

6+ num = 0 (Expected type)

7+

8+Specifically:

9+ Type mismatch between

10+ 0

11+ and

12+ num

4Multiple.idr:3:1:import alias not unique: "X"

13Multiple.idr:3:1:import alias not unique: "X"

test/basic015/basic015.idrnew file+73

@@ -0,0 +1,73 @@

1+{-

2+data Nat = Z | S Nat

3+

4+plus : Nat -> Nat -> Nat

5+plus Z y = y

6+plus (S x) y = S (plus x y)

7+-}

8+

9+data Vect : Nat -> Type -> Type where

10+ Nil : Vect Z a

11+ (::) : a -> Vect k a -> Vect (S k) a

12+

13+%name Vect xs, ys, zs

14+

15+append : Vect n a -> Vect m a -> Vect (n + m) a

16+append [] ys = ys

17+append (x :: xs) ys = x :: append xs ys

18+

19+

20+zipWith : (a -> b -> c) -> Vect n a -> Vect n b -> Vect n c

21+zipWith f [] ys = []

22+zipWith f (x :: xs) (y :: ys) = f x y :: zipWith f xs ys

23+

24+create_empties : Vect m (Vect 0 elem)

25+create_empties {m = Z} = []

26+create_empties {m = (S k)} = [] :: create_empties

27+

28+transpose_helper : (row : Vect m elem) -> (rest_trans : Vect m (Vect k elem)) ->

29+ Vect m (Vect (S k) elem)

30+transpose_helper [] [] = []

31+transpose_helper (rowval :: xs) (restrow :: ys) = (rowval :: restrow) :: transpose_helper xs ys

32+

33+transpose_vec : Vect n (Vect m elem) -> Vect m (Vect n elem)

34+transpose_vec [] = create_empties

35+transpose_vec (row :: rest) = let rest_trans = transpose_vec rest in

36+ transpose_helper row rest_trans

37+

38+

39+

40+

41+

42+

43+

44+

45+------- A main program to read dimensions, generate and tranpose a vector

46+

47+instance Functor (Vect m) where

48+ map m [] = []

49+ map m (x :: xs) = m x :: map m xs

50+

51+instance Show a => Show (Vect m a) where

52+ show x = show (toList x)

53+ where

54+ toList : Vect m a -> List a

55+ toList [] = []

56+ toList (y :: xs) = y :: toList xs

57+

58+countTo : (m : Nat) -> Vect m Int

59+countTo Z = []

60+countTo (S k) = 0 :: map (+1) (countTo k)

61+

62+mkVect : (n, m : Nat) -> Vect n (Vect m Int)

63+mkVect Z m = []

64+mkVect (S k) m = countTo m :: map (map (+ cast m)) (mkVect k m)

65+

66+main : IO ()

67+main = do putStr "Rows: "

68+ let r : Nat = 5

69+ putStr "Columns: "

70+ let c : Nat = 6

71+ printLn (mkVect r c)

72+ putStrLn "Transposed:"

73+ printLn (transpose_vec (mkVect r c))

test/basic015/expectednew file+3

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

1+Rows: Columns: [[0, 1, 2, 3, 4, 5], [6, 7, 8, 9, 10, 11], [12, 13, 14, 15, 16, 17], [18, 19, 20, 21, 22, 23], [24, 25, 26, 27, 28, 29]]

2+Transposed:

3+[[0, 6, 12, 18, 24], [1, 7, 13, 19, 25], [2, 8, 14, 20, 26], [3, 9, 15, 21, 27], [4, 10, 16, 22, 28], [5, 11, 17, 23, 29]]

test/basic015/runnew file+4

@@ -0,0 +1,4 @@

1+#!/usr/bin/env bash

2+idris $@ basic015.idr -o basic015

3+./basic015

4+rm -f basic015 *.ibc

test/classes001/ClassName.idr+1−1

@@ -21,7 +21,7 @@ badShow = MkMyShow (const "hej")

21test1 : twiceAString 2 = "22"

22test1 = Refl

23

24−test2 : twiceAString @{badShow} 2 = "hejhej"

24+test2 : twiceAString @{ClassName.badShow} 2 = "hejhej"

25test2 = Refl

26

27

test/dsl003/DSLPi.idr+1−1

@@ -43,5 +43,5 @@ test2 = specs ((x, y : INT) -> x === y)

43test3 : Spec []

44test3 = ForAll INT . ForAll INT . ItHolds $ Var (FS FZ) === Var FZ

45

46−test4 : test2 = test3

46+test4 : DSLPi.test2 = DSLPi.test3

47test4 = Refl

test/error003/expected+1−1

@@ -1,2 +1,2 @@

1ErrorReflection.idr:68:5:When checking right hand side of bad:

2−DSL type error: (t(503) => t'(504)) doesn't match ()

2+DSL type error: (t(504) => t'(503)) doesn't match ()

test/primitives001/substring.idr+5−5

@@ -13,19 +13,19 @@ foo = "Hello! here's the thing"

13firstSentence : String

14firstSentence = "Idris 是一个通用的依赖类型纯函数式编程语言，其类型系统与 Agda 以及 Epigram 相似。"

15

16−emptyTest : prim__strSubstr 100000 14 firstSentence = ""

16+emptyTest : prim__strSubstr 100000 14 Main.firstSentence = ""

17emptyTest = Refl

18

19−multiTest : prim__strSubstr 10 5 firstSentence = "用的依赖类"

19+multiTest : prim__strSubstr 10 5 Main.firstSentence = "用的依赖类"

20multiTest = Refl

21

22−negative : prim__strSubstr (-10) 5 firstSentence = "Idris"

22+negative : prim__strSubstr (-10) 5 Main.firstSentence = "Idris"

23negative = Refl

24

25−negativeEnd : prim__strSubstr 0 (-1) firstSentence = ""

25+negativeEnd : prim__strSubstr 0 (-1) Main.firstSentence = ""

26negativeEnd = Refl

27

28−negativeLength : prim__strSubstr 4 (-4) firstSentence = ""

28+negativeLength : prim__strSubstr 4 (-4) Main.firstSentence = ""

29negativeLength = Refl

30

31main : IO ()

test/proof003/test015.idr+1−1

@@ -106,7 +106,7 @@ Main.ntbEven = proof {

106-- There is almost certainly an easier proof. I don't care, for now :)

107

108Main.adc_lemma_2 = proof {

109− intro w,v,num0,v1,num1,x,bx,x1,bx1,bit0,b0,bit1,b1,c,bc

109+ intro v,w,num0,v1,num1,x,bx,x1,bx1,bit0,b0,bit1,b1,c,bc

110 rewrite sym (plusZeroRightNeutral x);

111 rewrite sym (plusZeroRightNeutral v1);

112 rewrite sym (plusZeroRightNeutral (plus (plus x v) v1));

test/proofsearch001/proofsearch001.idr+1−1

@@ -1,7 +1,7 @@

1%default total

2

3class C a (f : Bool -> Bool) | a where {}

4−instance C Int not where {}

4+instance C Int Bool.not where {}

5

6foo : C Int g => {auto pf : g True = False} -> Unit

7foo = ()

test/quasiquote006/quasiquote006.idr+2−2

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

2a : TTName

3a = `{Nat}

4

5−aOK : a = NS (UN "Nat") ["Nat", "Prelude"]

5+aOK : Main.a = NS (UN "Nat") ["Nat", "Prelude"]

6aOK = Refl

7

8b : TTName

@@ -17,5 +17,5 @@ d = `{(::)}

17d : TTName

18d = `{List.(::)}

19

20−dOK : d = NS (UN "::") ["List", "Prelude"]

20+dOK : Main.d = NS (UN "::") ["List", "Prelude"]

21dOK = Refl

test/reg001/reg001.idr+1−1

@@ -7,7 +7,7 @@ import Data.Fin

7import Control.Isomorphism

8

9class Functor f => VerifiedFunctor (f : Type -> Type) where

10− identity : (fa : f a) -> map id fa = fa

10+ identity : (fa : f a) -> map Basics.id fa = fa

11

12data Imp : Type where

13 MkImp : {any : Type} -> any -> Imp

test/reg041/ott.idr+1−1

@@ -37,6 +37,6 @@ EQ two False two False = one

37EQ (pi s t) f (pi s' t') g = pi s $ \x => pi s' $ \y => EQ s x s' y ~> EQ (t x) (f x) (t' y) (g y)

38EQ _ _ _ _ = zero

39

40−example : <| (id == id in (two ~> two)) |>

40+example : <| (Basics.id == Basics.id in (OTT.two ~> OTT.two)) |>

41example = ?prf

42

test/reg047/reg047.idr+5−5

@@ -3,7 +3,7 @@ module test

3data TTSigma : (A : Type) -> (B : A -> Type) -> Type where

4 sigma : (A : Type) -> (B : A -> Type) -> (a : A) -> B a -> TTSigma A B

5

6−data Nat = zero | succ Nat

6+data Nat = Zero | Succ Nat

7

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

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

@@ -11,8 +11,8 @@ Id A = (=) {A = A} {B = A}

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

12IdRefl A a = Refl {x = a}

13

14−zzz : Id Nat zero zero

14+zzz : Id Nat Zero Zero

15−zzz = IdRefl Nat zero

15+zzz = IdRefl Nat Zero

16

17−eep : TTSigma Nat (\ a => Id Nat a zero)

17+eep : TTSigma Nat (\ a => Id Nat a Zero)

18−eep = sigma Nat (\ a => Id Nat a zero) zero zzz

18+eep = sigma Nat (\ a => Id Nat a Zero) Zero zzz

test/reg047/reg047a.idr+7−7

@@ -3,7 +3,7 @@ module test

3data TTSigma : (A : Type) -> (B : A -> Type) -> Type where

4 sigma : (A : Type) -> (B : A -> Type) -> (a : A) -> B a -> TTSigma A B

5

6−data MNat = zero | succ MNat

6+data MNat = Zero | Succ MNat

7

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

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

@@ -11,14 +11,14 @@ Id = \A,x,y => x = y -- {a = A} {b = A}

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

12IdRefl A a = Refl {x = a}

13

14−zzzz : Id MNat zero zero

14+zzzz : Id MNat Zero Zero

15−zzzz = IdRefl MNat zero

15+zzzz = IdRefl MNat Zero

16

17−eep : TTSigma MNat (\ c => Id MNat c zero)

17+eep : TTSigma MNat (\ c => Id MNat c Zero)

18−eep = (sigma MNat (\b => Id MNat b zero) zero zzzz)

18+eep = (sigma MNat (\b => Id MNat b Zero) Zero zzzz)

19

20−eep2 : TTSigma MNat (\ c => Id MNat c zero)

20+eep2 : TTSigma MNat (\ c => Id MNat c Zero)

21−eep2 = (sigma MNat (\b => Id MNat b zero) zero (IdRefl MNat zero))

21+eep2 = (sigma MNat (\b => Id MNat b Zero) Zero (IdRefl MNat Zero))

22

23

24