140d06a · Idris-dev · git.iko.soy

idris.cabal+4

compare with master

unifiedsplit

@@ -545,6 +545,10 @@ Extra-source-files:

545 test/interactive011/input

546 test/interactive011/run

547 test/interactive011/*.idr

548+ test/interactive012/expected

549+ test/interactive012/input

550+ test/interactive012/run

551+ test/interactive012/*.idr

548

552

549 test/io001/run

553 test/io001/run

550 test/io001/*.idr

554 test/io001/*.idr

src/Idris/Elab/Term.hs+18−31

@@ -1721,38 +1721,25 @@ resolveTC' di mv depth tm n ist

1721

1722collectDeferred :: Maybe Name -> [Name] -> Context ->

1723 Term -> State [(Name, (Int, Maybe Name, Type, [Name]))] Term

1724−collectDeferred top casenames ctxt (Bind n (GHole i psns t) app) =

1724+collectDeferred top casenames ctxt tm = cd [] tm

1725− do ds <- get

1726− t' <- collectDeferred top casenames ctxt t

1727− when (not (n `elem` map fst ds)) $ put (ds ++ [(n, (i, top, tidyArg [] t', psns))])

1728− collectDeferred top casenames ctxt app

1729 where

1725 where

1730− -- Evaluate the top level functions in arguments, if possible, and if it's

1726+ cd env (Bind n (GHole i psns t) app) =

1731− -- not a name we're immediately going to define in a case block, so that

1727+ do ds <- get

1732− -- any immediate specialisation of the function applied to constructors

1728+ t' <- collectDeferred top casenames ctxt t

1733− -- can be done

1729+ when (not (n `elem` map fst ds)) $ put (ds ++ [(n, (i, top, t', psns))])

1730+ cd env app

1734− tidyArg env (Bind n b@(Pi im t k) sc)

1731+ cd env (Bind n b t)

1735− = Bind n (Pi im (tidy ctxt env t) k)

1732+ = do b' <- cdb b

1736− (tidyArg ((n, b) : env) sc)

1733+ t' <- cd ((n, b) : env) t

1737− tidyArg env t = tidy ctxt env t

1738−

1739− tidy ctxt env t = normalise ctxt env t

1740−

1741− getFn (Bind n (Lam _) t) = getFn t

1742− getFn t | (f, a) <- unApply t = f

1743−

1744−collectDeferred top ns ctxt (Bind n b t)

1745− = do b' <- cdb b

1746− t' <- collectDeferred top ns ctxt t

1747− return (Bind n b' t')

1734+ return (Bind n b' t')

1748− where

1735+ where

1749− cdb (Let t v) = liftM2 Let (collectDeferred top ns ctxt t) (collectDeferred top ns ctxt v)

1736+ cdb (Let t v) = liftM2 Let (cd env t) (cd env v)

1750− cdb (Guess t v) = liftM2 Guess (collectDeferred top ns ctxt t) (collectDeferred top ns ctxt v)

1737+ cdb (Guess t v) = liftM2 Guess (cd env t) (cd env v)

1751− cdb b = do ty' <- collectDeferred top ns ctxt (binderTy b)

1738+ cdb b = do ty' <- cd env (binderTy b)

1752− return (b { binderTy = ty' })

1739+ return (b { binderTy = ty' })

1753−collectDeferred top ns ctxt (App s f a) = liftM2 (App s) (collectDeferred top ns ctxt f)

1740+ cd env (App s f a) = liftM2 (App s) (cd env f)

1754− (collectDeferred top ns ctxt a)

1741+ (cd env a)

1755−collectDeferred top ns ctxt t = return t

1742+ cd env t = return t

1756

1743

1757case_ :: Bool -> Bool -> IState -> Name -> PTerm -> ElabD ()

1744case_ :: Bool -> Bool -> IState -> Name -> PTerm -> ElabD ()

1758case_ ind autoSolve ist fn tm = do

1745case_ ind autoSolve ist fn tm = do

src/Idris/REPL.hs+2−1

@@ -943,7 +943,8 @@ process fn (Check (PRef _ _ n))

943 where

944 showMetavarInfo ppo ist n i

945 = case lookupTy n (tt_ctxt ist) of

946+ (ty:_) -> let ty' = normaliseC (tt_ctxt ist) [] ty in

946− (ty:_) -> putTy ppo ist i [] (delab ist (errReverse ist ty))

947+ putTy ppo ist i [] (delab ist (errReverse ist ty'))

947 putTy :: PPOption -> IState -> Int -> [(Name, Bool)] -> PTerm -> Doc OutputAnnotation

948 putTy :: PPOption -> IState -> Int -> [(Name, Bool)] -> PTerm -> Doc OutputAnnotation

948 putTy ppo ist 0 bnd sc = putGoal ppo ist bnd sc

949 putTy ppo ist 0 bnd sc = putGoal ppo ist bnd sc

949 putTy ppo ist i bnd (PPi _ n _ t sc)

950 putTy ppo ist i bnd (PPi _ n _ t sc)

test/basic002/test006.idr+1−1

@@ -23,7 +23,7 @@ main = do printLn (natToBin 42)

23---------- Proofs ----------

24

25Main.parity_lemma_2 = proof {

26− intro;

26+ intro j;

27 intro;

28 rewrite sym (plusSuccRightSucc j j);

29 trivial;

test/interactive012/expectednew file+33

@@ -0,0 +1,33 @@

1+ x : Int

2+--------------------------------------

3+mkString_rhs_1 : String

4+ x : String

5+--------------------------------------

6+mkString_rhs_2 : String

7+--------------------------------------

8+mkThing_rhs_1 : Int

9+--------------------------------------

10+mkThing_rhs_2 : String

11+ str : Bool

12+ x : IntString str

13+--------------------------------------

14+mkString2_rhs : String

15+ x : ?what

16+--------------------------------------

17+mkString3_rhs_1 : String

18+ x : ?what

19+--------------------------------------

20+mkString3_rhs_2 : String

21+ a : Type

22+ m : Nat

23+ ys : Vect m a

24+--------------------------------------

25+append_rhs_1 : Vect m a

26+ a : Type

27+ x : a

28+ k : Nat

29+ xs : Vect k a

30+ m : Nat

31+ ys : Vect m a

32+--------------------------------------

33+append_rhs_2 : Vect (S (plus k m)) a

test/interactive012/inputnew file+9

@@ -0,0 +1,9 @@

1+:t mkString_rhs_1

2+:t mkString_rhs_2

3+:t mkThing_rhs_1

4+:t mkThing_rhs_2

5+:t mkString2_rhs

6+:t mkString3_rhs_1

7+:t mkString3_rhs_2

8+:t append_rhs_1

9+:t append_rhs_2

test/interactive012/interactive012.idrnew file+26

@@ -0,0 +1,26 @@

1+IntString : Bool -> Type

2+IntString False = Int

3+IntString True = String

4+

5+mkString : (str : Bool) -> IntString str -> String

6+mkString False x = ?mkString_rhs_1

7+mkString True x = ?mkString_rhs_2

8+

9+mkThing : (str : Bool) -> IntString str

10+mkThing False = ?mkThing_rhs_1

11+mkThing True = ?mkThing_rhs_2

12+

13+mkString2 : (str : Bool) -> IntString str -> String

14+mkString2 str x = ?mkString2_rhs

15+

16+mkString3 : (str : Bool) -> ?what -> String

17+mkString3 False x = ?mkString3_rhs_1

18+mkString3 True x = ?mkString3_rhs_2

19+

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

21+ Nil : Vect Z a

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

23+

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

25+append [] ys = ?append_rhs_1

26+append (x :: xs) ys = ?append_rhs_2

test/interactive012/runnew file+3

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

1+#!/usr/bin/env bash

2+idris --quiet interactive012.idr < input

3+rm -f *.ibc

test/reg001/reg001.idr+11

@@ -197,3 +197,14 @@ Max p = (Nat , (k : Nat) -> p k -> Nat)

197maxEquiv : Max p -> (n1 : Nat) -> p n1 -> Nat

198maxEquiv a n1 pr1 = snd a n1 pr1

199

200+data Rho = R

201+

202+rho : Rho -> Rho

203+rho r = case r of R => r

204+

205+data Kappa : (r : Rho) -> Type where K : Kappa r

206+

207+kappa : Kappa (rho r) -> Kappa (rho r)

208+kappa {r} k = k' where -- k' : Kappa (rho r)

209+ k' = k

210+