git.iko.soy/Idris-dev
on master help sign in
Merge remote-tracking branch 'upstream/master' into wip/tactical

Conflicts: CHANGELOG

commitce403f6c60447bc7724262cee2c410bd168c0029 authorDavid Raymond Christiansen <david@davidchristiansen.dk> dateWed 23 Sep 2015, 13:24 (11 years ago) parentf4c91c6d03c71c
28 files changed+221−112
compare with master
unifiedsplit
CHANGELOG+5−1 config.mk+4 docs/tutorial/starting.rst+2 idris.cabal+4−1 libs/base/Data/Fin.idr+2−20 libs/contrib/Classes/Verified.idr+13−16 libs/contrib/Control/Algebra.idr+1−1 libs/effects/Effects.idr+6−11 libs/prelude/Prelude/Chars.idr+2−2 src/Idris/AbsSyntaxTree.hs+57−24 src/Idris/Core/Elaborate.hs+2−1 src/Idris/Core/ProofState.hs+2−1 src/Idris/Elab/Term.hs+4−6 test/basic009/expected+11−2 test/basic015/basic015.idr+73 test/basic015/expected+3 test/basic015/run+4 test/classes001/ClassName.idr+1−1 test/dsl003/DSLPi.idr+1−1 test/error003/expected+1−1 test/primitives001/substring.idr+5−5 test/proof003/test015.idr+1−1 test/proofsearch001/proofsearch001.idr+1−1 test/quasiquote006/quasiquote006.idr+2−2 test/reg001/reg001.idr+1−1 test/reg041/ott.idr+1−1 test/reg047/reg047.idr+5−5 test/reg047/reg047a.idr+7−7
CHANGELOG+5−1
@@ -12,7 +12,10 @@ Language updates
1212* The previous syntax for tactic proofs and the previous interactive prover
1313 are now deprecated in favour of reflected elaboration. They will be removed
1414 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.
1619
1720Library updates
1821---------------
@@ -22,6 +25,7 @@ Library updates
2225* A special version of (-) on 'Nat' requires that the second argument is
2326 smaller than or equal to the first. 'minus' retains the old behaviour,
2427 returning Z if there is an underflow.
28+* The (+), (-), and (*) operations on Fin have been removed.
2529* New Logging Effects have been added to facilitate logging of effectful
2630 programmes.
2731* Elaborator reflection is now a part of the prelude. It is no longer
config.mk+4
@@ -26,11 +26,15 @@ ifneq (, $(findstring cygwin, $(MACHINE)))
2626else
2727ifneq (, $(findstring mingw, $(MACHINE)))
2828 OS :=windows
29+else
30+ifneq (, $(findstring windows, $(MACHINE)))
31+ OS :=windows
2932else
3033 OS :=unix
3134endif
3235endif
3336endif
37+endif
3438
3539ifeq ($(OS),darwin)
3640 SHLIB_SUFFIX :=.dylib
docs/tutorial/starting.rst+2
@@ -66,6 +66,8 @@ Some useful options to the Idris command are:
6666
6767- ``--check`` type check the file and its dependencies without starting the interactive environment.
6868
69+- ``--package pkg`` add package as dependency, e.g. ``--package contrib`` to make use of the contrib package.
70+
6971- ``--help`` display usage summary and command line options.
7072
7173The Interactive Environment
idris.cabal+4−1
@@ -1,5 +1,5 @@
11Name: idris
2−Version: 0.9.19
2+Version: 0.9.19.1
33License: BSD3
44License-file: LICENSE
55Author: Edwin Brady
@@ -346,6 +346,9 @@ Extra-source-files:
346346 test/basic014/run
347347 test/basic014/*.idr
348348 test/basic014/expected
349+ test/basic015/run
350+ test/basic015/*.idr
351+ test/basic015/expected
349352
350353 test/bignum001/run
351354 test/bignum001/*.idr
libs/base/Data/Fin.idr+2−20
@@ -42,7 +42,7 @@ finToNatInjective FZ FZ Refl = Refl
4242finToNatInjective (FS m) FZ Refl impossible
4343finToNatInjective FZ (FS n) Refl impossible
4444finToNatInjective (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))
4646
4747instance Cast (Fin n) Nat where
4848 cast x = finToNat x
@@ -94,7 +94,7 @@ instance Ord (Fin n) where
9494 compare FZ (FS _) = LT
9595 compare (FS _) FZ = GT
9696 compare (FS x) (FS y) = compare x y
97−
97+
9898instance MinBound (Fin (S n)) where
9999 minBound = FZ
100100
@@ -102,24 +102,6 @@ instance MaxBound (Fin (S n)) where
102102 maxBound = last
103103
104104
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−
123105-- Construct a Fin from an integer literal which must fit in the given Fin
124106
125107natToFin : 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
1717 (g1 : a -> b) -> (g2 : b -> c) ->
1818 map (g2 . g1) x = (map g2 . map g1) x
1919
20−
21−
2220class (Applicative f, VerifiedFunctor f) => VerifiedApplicative (f : Type -> Type) where
2321 applicativeMap : (x : f a) -> (g : a -> b) ->
2422 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
2624 applicativeComposition : (x : f a) -> (g1 : f (a -> b)) -> (g2 : f (b -> c)) ->
2725 ((pure (.) <*> g2) <*> g1) <*> x = g2 <*> (g1 <*> x)
2826 applicativeHomomorphism : (x : a) -> (g : a -> b) ->
@@ -30,14 +28,13 @@ class (Applicative f, VerifiedFunctor f) => VerifiedApplicative (f : Type -> Typ
3028 applicativeInterchange : (x : a) -> (g : f (a -> b)) ->
3129 g <*> pure x = pure (\g' : a -> b => g' x) <*> g
3230
33−
3431class (Monad m, VerifiedApplicative m) => VerifiedMonad (m : Type -> Type) where
3532 monadApplicative : (mf : m (a -> b)) -> (mx : m a) ->
3633 mf <*> mx = mf >>= \f =>
3734 mx >>= \x =>
3835 pure (f x)
3936 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
4138 monadAssociativity : (mx : m a) -> (f : a -> m b) -> (g : b -> m c) ->
4239 (mx >>= f) >>= g = mx >>= (\x => f x >>= g)
4340
@@ -53,8 +50,8 @@ instance VerifiedSemigroup (List a) where
5350
5451
5552class (VerifiedSemigroup a, Monoid a) => VerifiedMonoid a where
56− total monoidNeutralIsNeutralL : (l : a) -> l <+> neutral = l
57− total monoidNeutralIsNeutralR : (r : a) -> neutral <+> r = r
53+ total monoidNeutralIsNeutralL : (l : a) -> l <+> Algebra.neutral = l
54+ total monoidNeutralIsNeutralR : (r : a) -> Algebra.neutral <+> r = r
5855
5956-- instance VerifiedMonoid Nat where
6057-- monoidNeutralIsNeutralL = plusZeroRightNeutral
@@ -65,8 +62,8 @@ instance VerifiedMonoid (List a) where
6562 monoidNeutralIsNeutralR xs = Refl
6663
6764class (VerifiedMonoid a, Group a) => VerifiedGroup a where
68− total groupInverseIsInverseL : (l : a) -> l <+> inverse l = neutral
69− total groupInverseIsInverseR : (r : a) -> inverse r <+> r = neutral
65+ total groupInverseIsInverseL : (l : a) -> l <+> inverse l = Algebra.neutral
66+ total groupInverseIsInverseR : (r : a) -> inverse r <+> r = Algebra.neutral
7067
7168class (VerifiedGroup a, AbelianGroup a) => VerifiedAbelianGroup a where
7269 total abelianGroupOpIsCommutative : (l, r : a) -> l <+> r = r <+> l
@@ -77,12 +74,12 @@ class (VerifiedAbelianGroup a, Ring a) => VerifiedRing a where
7774 total ringOpIsDistributiveR : (l, c, r : a) -> (l <+> c) <.> r = (l <.> r) <+> (c <.> r)
7875
7976class (VerifiedRing a, RingWithUnity a) => VerifiedRingWithUnity a where
80− total ringWithUnityIsUnityL : (l : a) -> l <.> unity = l
81− total ringWithUnityIsUnityR : (r : a) -> unity <.> r = r
77+ total ringWithUnityIsUnityL : (l : a) -> l <.> Algebra.unity = l
78+ total ringWithUnityIsUnityR : (r : a) -> Algebra.unity <.> r = r
8279
8380--class (VerifiedRingWithUnity a, Field a) => VerifiedField a where
84−-- total fieldInverseIsInverseL : (l : a) -> (notId : Not (l = neutral)) -> l <.> (inverseM l notId) = unity
85−-- total fieldInverseIsInverseR : (r : a) -> (notId : Not (r = neutral)) -> (inverseM r notId) <.> r = unity
81+-- total fieldInverseIsInverseL : (l : a) -> (notId : Not (l = neutral)) -> l <.> (inverseM l notId) = Algebra.unity
82+-- total fieldInverseIsInverseR : (r : a) -> (notId : Not (r = neutral)) -> (inverseM r notId) <.> r = Algebra.unity
8683
8784
8885class JoinSemilattice a => VerifiedJoinSemilattice a where
@@ -96,10 +93,10 @@ class MeetSemilattice a => VerifiedMeetSemilattice a where
9693 total meetSemilatticeMeetIsIdempotent : (e : a) -> meet e e = e
9794
9895class (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
10097
10198class (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
103100
104101class (VerifiedJoinSemilattice a, VerifiedMeetSemilattice a) => VerifiedLattice a where
105102 total latticeMeetAbsorbsJoin : (l, r : a) -> meet l (join l r) = l
@@ -110,7 +107,7 @@ class (VerifiedBoundedJoinSemilattice a, VerifiedBoundedMeetSemilattice a, Verif
110107
111108--class (VerifiedRingWithUnity a, VerifiedAbelianGroup b, Module a b) => VerifiedModule a b where
112109-- 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
114111-- total moduleScalarMultDistributiveWRTVectorAddition : (s : a) -> (v, w : b) -> s <#> (v <+> w) = (s <#> v) <+> (s <#> w)
115112-- total moduleScalarMultDistributiveWRTModuleAddition : (s, t : a) -> (v : b) -> (s <+> t) <#> v = (s <#> v) <+> (t <#> v)
116113
libs/contrib/Control/Algebra.idr+1−1
@@ -113,7 +113,7 @@ class Ring a => RingWithUnity a where
113113||| forall a b c, a <.> (b <+> c) == (a <.> b) <+> (a <.> c)
114114||| forall a b c, (a <+> b) <.> c == (a <.> c) <+> (b <.> c)
115115class RingWithUnity a => Field a where
116− inverseM : (x : a) -> Not (x = neutral) -> a
116+ inverseM : (x : a) -> Not (x = Algebra.neutral) -> a
117117
118118sum' : (Foldable t, Monoid a) => t a -> a
119119sum' = concat
libs/effects/Effects.idr+6−11
@@ -254,9 +254,8 @@ execEff : Env m xs -> (p : EffElem e res xs) ->
254254 ((v : a) -> Env m (updateResTy v xs p eff) -> m t) -> m t
255255execEff (val :: env) Here eff' k
256256 = 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
259− = execEff {e} {a} {res} {resk} env p eff (\v, env' => k v (val :: env'))
257+execEff (val :: env) (There p) eff k
258+ = execEff env p eff (\v, env' => k v (val :: env'))
260259
261260-- Q: Instead of m b, implement as StateT (Env m xs') m b, so that state
262261-- updates can be propagated even through failing computations?
@@ -271,11 +270,7 @@ eff env (liftP prf effP) k
271270 eff env' effP (\p', envk => k p' (rebuildEnv envk prf env))
272271eff env (new (MkEff resTy newEff) res {prf=Refl} effP) k
273272 = 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
279274 = let env' = unlabel env in
280275 eff env' prog (\p', envk => k p' (relabel l envk))
281276
@@ -325,8 +320,8 @@ run prog {env} = eff env prog (\r, env => pure r)
325320|||
326321||| @prog The effectful program to run.
327322%no_implicit
328−runPure : (prog : EffM id a xs xs') ->
329− {default MkDefaultEnv env : Env id xs} -> a
323+runPure : (prog : EffM Basics.id a xs xs') ->
324+ {default MkDefaultEnv env : Env Basics.id xs} -> a
330325runPure prog {env} = eff env prog (\r, env => r)
331326
332327||| 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)
346341||| @env The environment to use.
347342||| @prog The effectful program to run.
348343%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
350345runPureInit env prog = eff env prog (\r, env => r)
351346
352347%no_implicit
libs/prelude/Prelude/Chars.idr+2−2
@@ -7,7 +7,7 @@ import Prelude.List
77import Prelude.Cast
88import Builtins
99
10−||| Return the ASCII representation of the character.
10+||| Convert the number to its ASCII equivalent.
1111chr : Int -> Char
1212chr x = if (x >= 0 && x < 0x110000)
1313 then assert_total (prim__intToChar x)
@@ -16,7 +16,7 @@ chr x = if (x >= 0 && x < 0x110000)
1616instance Cast Int Char where
1717 cast = chr
1818
19−||| Convert the number to its ASCII equivalent.
19+||| Return the ASCII representation of the character.
2020ord : Char -> Int
2121ord x = prim__charToInt x
2222
src/Idris/AbsSyntaxTree.hs+57−24
@@ -2249,41 +2249,74 @@ boundNamesIn tm = S.toList (ni 0 S.empty tm)
22492249
22502250-- Return names which are valid implicits in the given term (type).
22512251implicitNamesIn :: [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
22532255 where
2254− ni 0 env (PRef _ _ n)
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+
2274+ ni 0 env (PRef _ _ n@(NS _ _))
22552275 | not (n `elem` env)
2256− = case lookupTy n (tt_ctxt ist) of
2257− [] -> [n]
2258− _ -> if n `elem` uvars then [n] else []
2276+ -- Never implicitly bind if there's a namespace
2277+ = addFn n
2278+ ni 0 env (PRef _ _ n)
2279+ | not (n `elem` env) && implicitable n || n `elem` uvars = addImp n
22592280 ni 0 env (PApp _ f@(PRef _ _ n) as)
2260− | n `elem` uvars = ni 0 env f ++ concatMap (ni 0 env) (map getTm as)
2261− | otherwise = concatMap (ni 0 env) (map getTm as)
2262− ni 0 env (PApp _ f as) = ni 0 env f ++ concatMap (ni 0 env) (map getTm as)
2263− ni 0 env (PAppBind _ f as) = ni 0 env f ++ concatMap (ni 0 env) (map getTm as)
2264− ni 0 env (PCase _ c os) = ni 0 env c ++
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
2286+ mapM_ (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)
2289+ ni 0 env (PAppBind _ f as) = do ni 0 env f
2290+ mapM_ (ni 0 env) (map getTm as)
2291+ ni 0 env (PCase _ c os) = do ni 0 env c
22652292 -- names in 'os', not counting the names bound in the cases
2266− (nub (concatMap (ni 0 env) (map snd os))
2267− \\ nub (concatMap (ni 0 env) (map fst os)))
2268− ni 0 env (PIfThenElse _ c t f) = concatMap (ni 0 env) [c, t, f]
2269− ni 0 env (PLam fc n _ ty sc) = 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
2271− ni 0 env (PRewrite _ l r _) = ni 0 env l ++ ni 0 env r
2272− ni 0 env (PTyped l r) = ni 0 env l ++ ni 0 env r
2273− ni 0 env (PPair _ _ _ l r) = 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
2275− ni 0 env (PDPair _ _ _ l t r) = ni 0 env l ++ ni 0 env t ++ ni 0 env r
2276− ni 0 env (PAlternative ns a as) = concatMap (ni 0 env) as
2293+ mapM_ (ni 0 env) (map snd os)
2294+ (imps, fns) <- get
2295+ put ([] ,[])
2296+ mapM_ (ni 0 env) (map fst os)
2297+ (impsfst, _) <- get
2298+ put (nub imps \\ nub impsfst, fns)
2299+ ni 0 env (PIfThenElse _ c t f) = mapM_ (ni 0 env) [c, t, f]
2300+ ni 0 env (PLam fc n _ ty sc) = do 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
2302+ ni 0 env (PRewrite _ l r _) = do ni 0 env l; ni 0 env r
2303+ ni 0 env (PTyped l r) = do ni 0 env l; ni 0 env r
2304+ ni 0 env (PPair _ _ _ l r) = do ni 0 env l; ni 0 env r
2305+ ni 0 env (PDPair _ _ _ (PRef _ _ n) t r) = do ni 0 env t; ni 0 (n: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
2309+ ni 0 env (PAlternative ns a as) = mapM_ (ni 0 env) as
22772310 ni 0 env (PHidden tm) = ni 0 env tm
22782311 ni 0 env (PUnifyLog tm) = ni 0 env tm
22792312 ni 0 env (PDisamb _ tm) = ni 0 env tm
22802313 ni 0 env (PNoImplicits tm) = ni 0 env tm
22812314
2282− ni i env (PQuasiquote tm ty) = ni (i + 1) env tm ++
2283− maybe [] (ni i env) ty
2315+ ni i env (PQuasiquote tm ty) = do ni (i + 1) env tm
2316+ maybe (return ()) (ni i env) ty
22842317 ni i env (PUnquote tm) = ni (i - 1) env tm
22852318
2286− ni i env tm = concatMap (ni i env) (children tm)
2319+ ni i env tm = mapM_ (ni i env) (children tm)
22872320
22882321-- Return names which are free in the given term.
22892322namesIn :: [(Name, PTerm)] -> IState -> PTerm -> [Name]
src/Idris/Core/Elaborate.hs+2−1
@@ -502,9 +502,10 @@ matchProblems all = processTactic' (MatchProblems all)
502502unifyProblems :: Elab' aux ()
503503unifyProblems = processTactic' UnifyProblems
504504
505−defer :: [Name] -> Name -> Elab' aux ()
505+defer :: [Name] -> Name -> Elab' aux Name
506506defer ds n = do n' <- unique_hole n
507507 processTactic' (Defer ds n')
508+ return n'
508509
509510deferType :: Name -> Raw -> [Name] -> Elab' aux ()
510511deferType n ty ns = processTactic' (DeferType n ty ns)
src/Idris/Core/ProofState.hs+2−1
@@ -429,7 +429,8 @@ defer :: [Name] -> Name -> RunTactic
429429defer dropped n ctxt env (Bind x (Hole t) (P nt x' ty)) | x == x' =
430430 do let env' = filter (\(n, t) -> n `notElem` dropped) env
431431 action (\ps -> let hs = holes ps in
432− ps { holes = hs \\ [x] })
432+ ps { usedns = n : usedns ps,
433+ holes = hs \\ [x] })
433434 ps <- get
434435 return (Bind n (GHole (length env') (psnames ps) (mkTy (reverse env') t))
435436 (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
611611 [] -> False
612612 _ -> True
613613 bindable (NS _ _) = False
614− bindable (UN xs) = True
615614 bindable n = implicitable n
616615 elab' ina _ f@(PInferRef fc hls n) = elab' ina (Just fc) (PApp NoFC f [])
617616 elab' ina fc' tm@(PRef fc hls n)
@@ -981,7 +980,7 @@ elab ist info emode opts fn tm
981980 let n' = metavarName (namespace info) n
982981 attack
983982 psns <- getPSnames
984− defer unique_used n'
983+ n' <- defer unique_used n'
985984 solve
986985 highlightSource nfc (AnnName n' (Just MetavarOutput) Nothing Nothing)
987986 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
10571056
10581057 let args' = filter (\(n, _) -> n `notElem` argsDropped) args
10591058
1060− cname <- unique_hole' True (mkCaseName fn)
1061− let cname' = mkN cname
1062−-- elab' ina fc (PMetavar cname')
1063− attack; defer argsDropped cname'; solve
1059+ attack
1060+ cname' <- defer argsDropped (mkN (mkCaseName fn))
1061+ solve
10641062
10651063 -- if the scrutinee is one of the 'args' in env, we should
10661064 -- inspect it directly, rather than adding it as a new argument
test/basic009/expected+11−2
@@ -1,4 +1,13 @@
11MAIN-PASS
2−Faulty.idr:6:7:When checking type of Faulty.fault:
3−Can't disambiguate name: A.num, B.C.num
2+Faulty.idr:7:7:When checking right hand side of fault:
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
413Multiple.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")
2121test1 : twiceAString 2 = "22"
2222test1 = Refl
2323
24−test2 : twiceAString @{badShow} 2 = "hejhej"
24+test2 : twiceAString @{ClassName.badShow} 2 = "hejhej"
2525test2 = Refl
2626
2727
test/dsl003/DSLPi.idr+1−1
@@ -43,5 +43,5 @@ test2 = specs ((x, y : INT) -> x === y)
4343test3 : Spec []
4444test3 = ForAll INT . ForAll INT . ItHolds $ Var (FS FZ) === Var FZ
4545
46−test4 : test2 = test3
46+test4 : DSLPi.test2 = DSLPi.test3
4747test4 = Refl
test/error003/expected+1−1
@@ -1,2 +1,2 @@
11ErrorReflection.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"
1313firstSentence : String
1414firstSentence = "Idris 是一个通用的依赖类型纯函数式编程语言，其类型系统与 Agda 以及 Epigram 相似。"
1515
16−emptyTest : prim__strSubstr 100000 14 firstSentence = ""
16+emptyTest : prim__strSubstr 100000 14 Main.firstSentence = ""
1717emptyTest = Refl
1818
19−multiTest : prim__strSubstr 10 5 firstSentence = "用的依赖类"
19+multiTest : prim__strSubstr 10 5 Main.firstSentence = "用的依赖类"
2020multiTest = Refl
2121
22−negative : prim__strSubstr (-10) 5 firstSentence = "Idris"
22+negative : prim__strSubstr (-10) 5 Main.firstSentence = "Idris"
2323negative = Refl
2424
25−negativeEnd : prim__strSubstr 0 (-1) firstSentence = ""
25+negativeEnd : prim__strSubstr 0 (-1) Main.firstSentence = ""
2626negativeEnd = Refl
2727
28−negativeLength : prim__strSubstr 4 (-4) firstSentence = ""
28+negativeLength : prim__strSubstr 4 (-4) Main.firstSentence = ""
2929negativeLength = Refl
3030
3131main : IO ()
test/proof003/test015.idr+1−1
@@ -106,7 +106,7 @@ Main.ntbEven = proof {
106106-- There is almost certainly an easier proof. I don't care, for now :)
107107
108108Main.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
110110 rewrite sym (plusZeroRightNeutral x);
111111 rewrite sym (plusZeroRightNeutral v1);
112112 rewrite sym (plusZeroRightNeutral (plus (plus x v) v1));
test/proofsearch001/proofsearch001.idr+1−1
@@ -1,7 +1,7 @@
11%default total
22
33class C a (f : Bool -> Bool) | a where {}
4−instance C Int not where {}
4+instance C Int Bool.not where {}
55
66foo : C Int g => {auto pf : g True = False} -> Unit
77foo = ()
test/quasiquote006/quasiquote006.idr+2−2
@@ -2,7 +2,7 @@
22a : TTName
33a = `{Nat}
44
5−aOK : a = NS (UN "Nat") ["Nat", "Prelude"]
5+aOK : Main.a = NS (UN "Nat") ["Nat", "Prelude"]
66aOK = Refl
77
88b : TTName
@@ -17,5 +17,5 @@ d = `{(::)}
1717d : TTName
1818d = `{List.(::)}
1919
20−dOK : d = NS (UN "::") ["List", "Prelude"]
20+dOK : Main.d = NS (UN "::") ["List", "Prelude"]
2121dOK = Refl
test/reg001/reg001.idr+1−1
@@ -7,7 +7,7 @@ import Data.Fin
77import Control.Isomorphism
88
99class 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
1111
1212data Imp : Type where
1313 MkImp : {any : Type} -> any -> Imp
test/reg041/ott.idr+1−1
@@ -37,6 +37,6 @@ EQ two False two False = one
3737EQ (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)
3838EQ _ _ _ _ = zero
3939
40−example : <| (id == id in (two ~> two)) |>
40+example : <| (Basics.id == Basics.id in (OTT.two ~> OTT.two)) |>
4141example = ?prf
4242
test/reg047/reg047.idr+5−5
@@ -3,7 +3,7 @@ module test
33data TTSigma : (A : Type) -> (B : A -> Type) -> Type where
44 sigma : (A : Type) -> (B : A -> Type) -> (a : A) -> B a -> TTSigma A B
55
6−data Nat = zero | succ Nat
6+data Nat = Zero | Succ Nat
77
88Id : (A : Type) -> A -> A -> Type
99Id A = (=) {A = A} {B = A}
@@ -11,8 +11,8 @@ Id A = (=) {A = A} {B = A}
1111IdRefl : (A : Type) -> (a : A) -> Id A a a
1212IdRefl A a = Refl {x = a}
1313
14−zzz : Id Nat zero zero
15−zzz = IdRefl Nat zero
14+zzz : Id Nat Zero Zero
15+zzz = IdRefl Nat Zero
1616
17−eep : TTSigma Nat (\ a => Id Nat a zero)
18−eep = sigma Nat (\ a => Id Nat a zero) zero zzz
17+eep : TTSigma Nat (\ a => Id Nat a Zero)
18+eep = sigma Nat (\ a => Id Nat a Zero) Zero zzz
test/reg047/reg047a.idr+7−7
@@ -3,7 +3,7 @@ module test
33data TTSigma : (A : Type) -> (B : A -> Type) -> Type where
44 sigma : (A : Type) -> (B : A -> Type) -> (a : A) -> B a -> TTSigma A B
55
6−data MNat = zero | succ MNat
6+data MNat = Zero | Succ MNat
77
88Id : (A : Type) -> A -> A -> Type
99Id = \A,x,y => x = y -- {a = A} {b = A}
@@ -11,14 +11,14 @@ Id = \A,x,y => x = y -- {a = A} {b = A}
1111IdRefl : (A : Type) -> (a : A) -> Id A a a
1212IdRefl A a = Refl {x = a}
1313
14−zzzz : Id MNat zero zero
15−zzzz = IdRefl MNat zero
14+zzzz : Id MNat Zero Zero
15+zzzz = IdRefl MNat Zero
1616
17−eep : TTSigma MNat (\ c => Id MNat c zero)
18−eep = (sigma MNat (\b => Id MNat b zero) zero zzzz)
17+eep : TTSigma MNat (\ c => Id MNat c Zero)
18+eep = (sigma MNat (\b => Id MNat b Zero) Zero zzzz)
1919
20−eep2 : TTSigma MNat (\ c => Id MNat c zero)
21−eep2 = (sigma MNat (\b => Id MNat b zero) zero (IdRefl MNat zero))
20+eep2 : TTSigma MNat (\ c => Id MNat c Zero)
21+eep2 = (sigma MNat (\b => Id MNat b Zero) Zero (IdRefl MNat Zero))
2222
2323
2424