e0b0516 · Idris-dev · git.iko.soy

CHANGELOG+3

compare with master

unifiedsplit

@@ -28,6 +28,9 @@ New in 0.9.18:

28 choice, keeping the first success as Alternative does. The version that

29 collects successes is now a named instance.

30* :exec REPL command now takes an optional expression to compile and run/show

31+* The return types of `Vect.findIndex`, `Vect.elemIndex` and

32+ `Vect.elemIndexBy` were changed from `Maybe Nat` to `Maybe (Fin n)`

33+* A new :browse command shows the contents of a namespace

31

34

32New in 0.9.17:

35New in 0.9.17:

33--------------

36--------------

idris.cabal+3−1

@@ -746,6 +746,8 @@ Library

746 , Idris.Elab.Value

747 , Idris.Elab.Term

748

749+ , Idris.REPL.Browse

750+

749 , Idris.AbsSyntax

751 , Idris.AbsSyntax

750 , Idris.AbsSyntaxTree

752 , Idris.AbsSyntaxTree

751 , Idris.Apropos

753 , Idris.Apropos

@@ -827,7 +829,7 @@ Library

827 , Tools_idris

829 , Tools_idris

828

830

829 Build-depends: base >=4 && <5

831 Build-depends: base >=4 && <5

830− , annotated-wl-pprint >= 0.5.3 && < 0.6

832+ , annotated-wl-pprint >= 0.5.3 && < 0.7

831 , ansi-terminal < 0.7

833 , ansi-terminal < 0.7

832 , ansi-wl-pprint < 0.7

834 , ansi-wl-pprint < 0.7

833 , base64-bytestring < 1.1

835 , base64-bytestring < 1.1

libs/base/Control/Monad/State.idr+13−1

@@ -1,6 +1,6 @@

1module Control.Monad.State

2

3−import Control.Monad.Identity

3+import public Control.Monad.Identity

4import Control.Monad.Trans

5

6%access public

@@ -55,3 +55,15 @@ gets f = do s <- get

55||| The State monad. See the MonadState class

56State : Type -> Type -> Type

57State s a = StateT s Identity a

58+

59+||| Unwrap a State monad computation.

60+runState : State s a -> s -> (a,s)

61+runState m = runIdentity . runStateT m

62+

63+||| Unwrap a State monad computation, but discard the final state.

64+evalState : State s a -> s -> a

65+evalState m = fst . runState m

66+

67+||| Unwrap a State monad computation, but discard the resulting value.

68+execState : State s a -> s -> s

69+execState m = snd . runState m

libs/base/Data/VectType.idr+7−10

@@ -372,14 +372,11 @@ find p (x::xs) with (p x)

372 | False = find p xs

373

374||| Find the index of the first element of the vector that satisfies some test

375−findIndex : (a -> Bool) -> Vect n a -> Maybe Nat

375+findIndex : (a -> Bool) -> Vect n a -> Maybe (Fin n)

376−findIndex = findIndex' 0

377− where

378− findIndex' : Nat -> (a -> Bool) -> Vect n a -> Maybe Nat

379− findIndex' cnt p [] = Nothing

376+findIndex p [] = Nothing

380− findIndex' cnt p (x::xs) with (p x)

377+findIndex p (x :: xs) with (p x)

381− | True = Just cnt

378+ | True = Just 0

382− | False = findIndex' (S cnt) p xs

379+ | False = map FS (findIndex p xs)

383

380

384||| Find the indices of all elements that satisfy some test

381||| Find the indices of all elements that satisfy some test

385total findIndices : (a -> Bool) -> Vect m a -> (p ** Vect p Nat)

382total findIndices : (a -> Bool) -> Vect m a -> (p ** Vect p Nat)

@@ -394,10 +391,10 @@ findIndices = findIndices' 0

394 else

391 else

395 (_ ** tail)

392 (_ ** tail)

396

393

397−elemIndexBy : (a -> a -> Bool) -> a -> Vect m a -> Maybe Nat

394+elemIndexBy : (a -> a -> Bool) -> a -> Vect m a -> Maybe (Fin m)

398elemIndexBy p e = findIndex $ p e

395elemIndexBy p e = findIndex $ p e

399

396

400−elemIndex : Eq a => a -> Vect m a -> Maybe Nat

397+elemIndex : Eq a => a -> Vect m a -> Maybe (Fin m)

401elemIndex = elemIndexBy (==)

398elemIndex = elemIndexBy (==)

402

399

403total elemIndicesBy : (a -> a -> Bool) -> a -> Vect m a -> (p ** Vect p Nat)

400total elemIndicesBy : (a -> a -> Bool) -> a -> Vect m a -> (p ** Vect p Nat)

libs/contrib/Data/String.idr+2−2

@@ -12,7 +12,7 @@ infixr 5 <+

12||| strSnoc "" 'A'

13||| ```

14strSnoc : String -> Char -> String

15−strSnoc s c = s ++ (singleton 'c')

15+strSnoc s c = s ++ (singleton c)

16

17||| Alias of `strSnoc`

18|||

@@ -28,4 +28,4 @@ strSnoc s c = s ++ (singleton 'c')

28||| 'A' <+ "AB"

29||| ```

30(<+) : Char -> String -> String

31−(<+) = strCons

31+(<+) = strCons

samples/ConsoleIO.idr → samples/effects/ConsoleIO.idrrenamed

The content is the same.

samples/Exception.idr → samples/effects/Exception.idrrenamed

The content is the same.

samples/Makefile → samples/effects/Makefilerenamed

The content is the same.

samples/Random.idr → samples/effects/Random.idrrenamed

The content is the same.

samples/ReadInt.idr → samples/effects/ReadInt.idrrenamed

The content is the same.

samples/Select.idr → samples/effects/Select.idrrenamed

The content is the same.

samples/TreeTag-noeff.idr → samples/effects/TreeTag-noeff.idrrenamed

The content is the same.

samples/TreeTag.idr → samples/effects/TreeTag.idrrenamed

The content is the same.

samples/TreeTagCount.idr → samples/effects/TreeTagCount.idrrenamed

The content is the same.

samples/hworld.idr → samples/effects/hworld.idrrenamed

The content is the same.

samples/vadd.idr → samples/effects/vadd.idrrenamed

The content is the same.

samples/misc/Makefilenew file+8

@@ -0,0 +1,8 @@

1+check:

2+ rm -f *.ibc

3+ for x in *.idr ; do \

4+ echo "Checking $$x"; \

5+ idris --check $$x; \

6+ done

7+

8+.PHONY: check

samples/binary.idr → samples/misc/binary.idrrenamed

The content is the same.

samples/interp-alt.idr → samples/misc/interp-alt.idrrenamed

The content is the same.

samples/interp.idr → samples/misc/interp.idrrenamed

The content is the same.

samples/javaffi.idr → samples/misc/javaffi.idrrenamed

The content is the same.

samples/named_instance.lidr → samples/misc/named_instance.lidrrenamed

The content is the same.

samples/reflection.idr → samples/misc/reflection.idrrenamed

The content is the same.

samples/tutorial/Makefilenew file+11

@@ -0,0 +1,11 @@

1+check: .PHONY

2+ rm -f *.ibc

3+ for x in *.idr ; do \

4+ echo "Checking $$x"; \

5+ idris --check $$x; \

6+ done

7+

8+clean:

9+ rm -f *.ibc

10+

11+.PHONY:

samples/tutorial/binary.idrnew file+61

@@ -0,0 +1,61 @@

1+module Main

2+

3+data Binary : Nat -> Type where

4+ bEnd : Binary Z

5+ bO : Binary n -> Binary (n + n)

6+ bI : Binary n -> Binary (S (n + n))

7+

8+instance Show (Binary n) where

9+ show (bO x) = show x ++ "0"

10+ show (bI x) = show x ++ "1"

11+ show bEnd = ""

12+

13+data Parity : Nat -> Type where

14+ Even : Parity (n + n)

15+ Odd : Parity (S (n + n))

16+

17+parity : (n:Nat) -> Parity n

18+parity Z = Even {n=Z}

19+parity (S Z) = Odd {n=Z}

20+parity (S (S k)) with (parity k)

21+ parity (S (S (j + j))) | Even ?= Even {n=S j}

22+ parity (S (S (S (j + j)))) | Odd ?= Odd {n=S j}

23+

24+natToBin : (n:Nat) -> Binary n

25+natToBin Z = bEnd

26+natToBin (S k) with (parity k)

27+ natToBin (S (j + j)) | Even = bI (natToBin j)

28+ natToBin (S (S (j + j))) | Odd ?= bO (natToBin (S j))

29+

30+intToNat : Int -> Nat

31+intToNat 0 = Z

32+intToNat x = if (x>0) then (S (intToNat (x-1))) else Z

33+

34+main : IO ()

35+main = do putStr "Enter a number: "

36+ x <- getLine

37+ print (natToBin (fromInteger (cast x)))

38+

39+---------- Proofs ----------

40+

41+Main.natToBin_lemma_1 = proof

42+ intros

43+ rewrite plusSuccRightSucc j j

44+ rewrite sym (plusSuccRightSucc j j)

45+ trivial

46+

47+

48+parity_lemma_1 = proof

49+ intros

50+ rewrite sym (plusSuccRightSucc j j)

51+ trivial

52+

53+

54+parity_lemma_2 = proof {

55+ intro;

56+ intro;

57+ rewrite sym (plusSuccRightSucc j j);

58+ trivial;

59+}

60+

61+

samples/tutorial/bmain.idrnew file+8

@@ -0,0 +1,8 @@

1+module Main

2+

3+import btree

4+

5+main : IO ()

6+main = do let t = toTree [1,8,2,7,9,3]

7+ print (btree.toList t)

8+

samples/tutorial/btree.idrnew file+18

@@ -0,0 +1,18 @@

1+module btree

2+

3+data BTree a = Leaf

4+ | Node (BTree a) a (BTree a)

5+

6+insert : Ord a => a -> BTree a -> BTree a

7+insert x Leaf = Node Leaf x Leaf

8+insert x (Node l v r) = if (x < v) then (Node (insert x l) v r)

9+ else (Node l v (insert x r))

10+

11+toList : BTree a -> List a

12+toList Leaf = []

13+toList (Node l v r) = btree.toList l ++ (v :: btree.toList r)

14+

15+toTree : Ord a => List a -> BTree a

16+toTree [] = Leaf

17+toTree (x :: xs) = insert x (toTree xs)

18+

samples/tutorial/btreemod.idrnew file+20

@@ -0,0 +1,20 @@

1+module btree

2+

3+abstract data BTree a = Leaf

4+ | Node (BTree a) a (BTree a)

5+

6+abstract

7+insert : Ord a => a -> BTree a -> BTree a

8+insert x Leaf = Node Leaf x Leaf

9+insert x (Node l v r) = if (x < v) then (Node (insert x l) v r)

10+ else (Node l v (insert x r))

11+

12+abstract

13+toList : BTree a -> List a

14+toList Leaf = []

15+toList (Node l v r) = btree.toList l ++ (v :: btree.toList r)

16+

17+abstract

18+toTree : Ord a => List a -> BTree a

19+toTree [] = Leaf

20+toTree (x :: xs) = insert x (toTree xs)

samples/tutorial/classes.idrnew file+10

@@ -0,0 +1,10 @@

1+m_add : Maybe Int -> Maybe Int -> Maybe Int

2+m_add x y = do x' <- x -- Extract value from x

3+ y' <- y -- Extract value from y

4+ return (x' + y') -- Add them

5+

6+m_add' : Maybe Int -> Maybe Int -> Maybe Int

7+m_add' x y = [ x' + y' | x' <- x, y' <- y ]

8+

9+sortAndShow : (Ord a, Show a) => List a -> String

10+sortAndShow xs = show (sort xs)

samples/tutorial/foo.idrnew file+10

@@ -0,0 +1,10 @@

1+module foo

2+

3+namespace x

4+ test : Int -> Int

5+ test x = x * 2

6+

7+namespace y

8+ test : String -> String

9+ test x = x ++ x

10+

samples/tutorial/hello.idrnew file+5

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

1+module Main

2+

3+main : IO ()

4+main = putStrLn "Hello world"

5+

samples/tutorial/idiom.idrnew file+38

@@ -0,0 +1,38 @@

1+module idiom

2+

3+data Expr = Var String

4+ | Val Int

5+ | Add Expr Expr

6+

7+data Eval : Type -> Type where

8+ MkEval : (List (String, Int) -> Maybe a) -> Eval a

9+

10+fetch : String -> Eval Int

11+fetch x = MkEval fetchVal where

12+ fetchVal : List (String, Int) -> Maybe Int

13+ fetchVal [] = Nothing

14+ fetchVal ((v, val) :: xs) = if (x == v) then (Just val) else (fetchVal xs)

15+

16+instance Functor Eval where

17+ map f (MkEval g) = MkEval (\e => map f (g e))

18+

19+instance Applicative Eval where

20+ pure x = MkEval (\e => Just x)

21+

22+ (<*>) (MkEval f) (MkEval g) = MkEval (\x => app (f x) (g x)) where

23+ app : Maybe (a -> b) -> Maybe a -> Maybe b

24+ app (Just fx) (Just gx) = Just (fx gx)

25+ app _ _ = Nothing

26+

27+eval : Expr -> Eval Int

28+eval (Var x) = fetch x

29+eval (Val x) = [| x |]

30+eval (Add x y) = [| eval x + eval y |]

31+

32+runEval : List (String, Int) -> Expr -> Maybe Int

33+runEval env e = case eval e of

34+ MkEval envFn => envFn env

35+

36+m_add' : Maybe Int -> Maybe Int -> Maybe Int

37+m_add' x y = [| x + y |]

38+

samples/tutorial/interp.idrnew file+68

@@ -0,0 +1,68 @@

1+module Main

2+

3+data Ty = TyInt | TyBool| TyFun Ty Ty

4+

5+interpTy : Ty -> Type

6+interpTy TyInt = Int

7+interpTy TyBool = Bool

8+interpTy (TyFun s t) = interpTy s -> interpTy t

9+

10+using (G : Vect n Ty)

11+

12+ data Env : Vect n Ty -> Type where

13+ Nil : Env Nil

14+ (::) : interpTy a -> Env G -> Env (a :: G)

15+

16+ data HasType : (i : Fin n) -> Vect n Ty -> Ty -> Type where

17+ Stop : HasType FZ (t :: G) t

18+ Pop : HasType k G t -> HasType (FS k) (u :: G) t

19+

20+ lookup : HasType i G t -> Env G -> interpTy t

21+ lookup Stop (x :: xs) = x

22+ lookup (Pop k) (x :: xs) = lookup k xs

23+

24+ data Expr : Vect n Ty -> Ty -> Type where

25+ Var : HasType i G t -> Expr G t

26+ Val : (x : Int) -> Expr G TyInt

27+ Lam : Expr (a :: G) t -> Expr G (TyFun a t)

28+ App : Expr G (TyFun a t) -> Expr G a -> Expr G t

29+ Op : (interpTy a -> interpTy b -> interpTy c) -> Expr G a -> Expr G b ->

30+ Expr G c

31+ If : Expr G TyBool -> Lazy (Expr G a) -> Lazy (Expr G a) -> Expr G a

32+

33+ interp : Env G -> [static] (e : Expr G t) -> interpTy t

34+ interp env (Var i) = lookup i env

35+ interp env (Val x) = x

36+ interp env (Lam sc) = \x => interp (x :: env) sc

37+ interp env (App f s) = interp env f (interp env s)

38+ interp env (Op op x y) = op (interp env x) (interp env y)

39+ interp env (If x t e) = if interp env x then interp env t

40+ else interp env e

41+

42+ eId : Expr G (TyFun TyInt TyInt)

43+ eId = Lam (Var Stop)

44+

45+ eAdd : Expr G (TyFun TyInt (TyFun TyInt TyInt))

46+ eAdd = Lam (Lam (Op (+) (Var Stop) (Var (Pop Stop))))

47+

48+ eEq : Expr G (TyFun TyInt (TyFun TyInt TyBool))

49+ eEq = Lam (Lam (Op (==) (Var Stop) (Var (Pop Stop))))

50+

51+ eDouble : Expr G (TyFun TyInt TyInt)

52+ eDouble = Lam (App (App eAdd (Var Stop)) (Var Stop))

53+

54+ fact : Expr G (TyFun TyInt TyInt)

55+ fact = Lam (If (Op (==) (Var Stop) (Val 0))

56+ (Val 1) (Op (*) (App fact (Op (-) (Var Stop) (Val 1))) (Var Stop)))

57+

58+testFac : Int

59+testFac = interp [] fact 4

60+

61+-- unitTestFac : so (interp [] fact 4 == 24)

62+-- unitTestFac = oh

63+

64+main : IO ()

65+main = do putStr "Enter a number: "

66+ x <- getLine

67+ print (interp [] fact (cast x))

68+

samples/tutorial/letbind.idrnew file+16

@@ -0,0 +1,16 @@

1+module letbind

2+

3+mirror : List a -> List a

4+mirror xs = let xs' = reverse xs in

5+ xs ++ xs'

6+

7+data Person = MkPerson String Int

8+

9+showPerson : Person -> String

10+showPerson p = let MkPerson name age = p in

11+ name ++ " is " ++ show age ++ " years old"

12+

13+splitAt : Char -> String -> (String, String)

14+splitAt c x = case break (== c) x of

15+ (x, y) => (x, strTail y)

16+

samples/tutorial/prims.idrnew file+14

@@ -0,0 +1,14 @@

1+module prims

2+

3+x : Int

4+x = 42

5+

6+foo : String

7+foo = "Sausage machine"

8+

9+bar : Char

10+bar = 'Z'

11+

12+quux : Bool

13+quux = False

14+

samples/tutorial/theorems.idrnew file+57

@@ -0,0 +1,57 @@

1+

2+fiveIsFive : 5 = 5

3+fiveIsFive = Refl

4+

5+twoPlusTwo : 2 + 2 = 4

6+twoPlusTwo = Refl

7+

8+total disjoint : (n : Nat) -> Z = S n -> Void

9+disjoint n p = replace {P = disjointTy} p ()

10+ where

11+ disjointTy : Nat -> Type

12+ disjointTy Z = ()

13+ disjointTy (S k) = Void

14+

15+total acyclic : (n : Nat) -> n = S n -> Void

16+acyclic Z p = disjoint _ p

17+acyclic (S k) p = acyclic k (succInjective _ _ p)

18+

19+empty1 : Void

20+empty1 = hd [] where

21+ hd : List a -> a

22+ hd (x :: xs) = x

23+

24+empty2 : Void

25+empty2 = empty2

26+

27+plusReduces : (n:Nat) -> plus Z n = n

28+plusReduces n = Refl

29+

30+plusReducesZ : (n:Nat) -> n = plus n Z

31+plusReducesZ Z = Refl

32+plusReducesZ (S k) = cong (plusReducesZ k)

33+

34+plusReducesS : (n:Nat) -> (m:Nat) -> S (plus n m) = plus n (S m)

35+plusReducesS Z m = Refl

36+plusReducesS (S k) m = cong (plusReducesS k m)

37+

38+plusReducesZ' : (n:Nat) -> n = plus n Z

39+plusReducesZ' Z = ?plusredZ_Z

40+plusReducesZ' (S k) = let ih = plusReducesZ' k in

41+ ?plusredZ_S

42+

43+

44+---------- Proofs ----------

45+

46+plusredZ_S = proof {

47+ intro;

48+ intro;

49+ rewrite ih;

50+ trivial;

51+}

52+

53+plusredZ_Z = proof {

54+ compute;

55+ trivial;

56+}

57+

samples/tutorial/universe.idrnew file+7

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

1+myid : (a : Type) -> a -> a

2+myid _ x = x

3+

4+idid : (a : Type) -> a -> a

5+idid = myid _ myid

6+

7+

samples/tutorial/usefultypes.idrnew file+20

@@ -0,0 +1,20 @@

1+

2+intVec : Vect 5 Int

3+intVec = [1, 2, 3, 4, 5]

4+

5+double : Int -> Int

6+double x = x * 2

7+

8+vec : (n ** Vect n Int)

9+vec = (_ ** [3, 4])

10+

11+list_lookup : Nat -> List a -> Maybe a

12+list_lookup _ Nil = Nothing

13+list_lookup Z (x :: xs) = Just x

14+list_lookup (S k) (x :: xs) = list_lookup k xs

15+

16+lookup_default : Nat -> List a -> a -> a

17+lookup_default i xs def = case list_lookup i xs of

18+ Nothing => def

19+ Just x => x

20+

samples/tutorial/vbroken.idrnew file+10

@@ -0,0 +1,10 @@

1+module Vect

2+

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

4+ Nil : Vect Z a

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

6+

7+(++) : Vect n a -> Vect m a -> Vect (n + m) a

8+(++) Nil ys = ys

9+(++) (x :: xs) ys = x :: xs ++ xs -- BROKEN

10+

samples/tutorial/views.idrnew file+37

@@ -0,0 +1,37 @@

1+module views

2+

3+data Parity : Nat -> Type where

4+ Even : Parity (n + n)

5+ Odd : Parity (S (n + n))

6+

7+parity : (n:Nat) -> Parity n

8+parity Z = Even {n=Z}

9+parity (S Z) = Odd {n=Z}

10+parity (S (S k)) with (parity k)

11+ parity (S (S (j + j))) | Even ?= Even {n=S j}

12+ parity (S (S (S (j + j)))) | Odd ?= Odd {n=S j}

13+

14+natToBin : Nat -> List Bool

15+natToBin Z = Nil

16+natToBin k with (parity k)

17+ natToBin (j + j) | Even = False :: natToBin j

18+ natToBin (S (j + j)) | Odd = True :: natToBin j

19+

20+

21+---------- Proofs ----------

22+

23+views.parity_lemma_2 = proof {

24+ intro;

25+ intro;

26+ rewrite sym (plusSuccRightSucc j j);

27+ trivial;

28+}

29+

30+views.parity_lemma_1 = proof {

31+ intro;

32+ intro;

33+ rewrite sym (plusSuccRightSucc j j);

34+ trivial;

35+}

36+

37+

samples/tutorial/viewsbroken.idrnew file+12

@@ -0,0 +1,12 @@

1+

2+data Parity : Nat -> Type where

3+ Even : Parity (n + n)

4+ Odd : Parity (S (n + n))

5+

6+parity : (n:Nat) -> Parity n

7+parity Z = Even {n=Z}

8+parity (S Z) = Odd {n=Z}

9+parity (S (S k)) with (parity k)

10+ parity (S (S (j + j))) | Even = Even {n=S j}

11+ parity (S (S (S (j + j)))) | Odd = Odd {n=S j}

12+

samples/tutorial/wheres.idrnew file+14

@@ -0,0 +1,14 @@

1+module wheres

2+

3+even : Nat -> Bool

4+even Z = True

5+even (S k) = odd k where

6+ odd Z = False

7+ odd (S k) = even k

8+

9+test : List Nat

10+test = [c (S 1), c Z, d (S Z)]

11+ where c x = 42 + x

12+ d y = c (y + 1 + z y)

13+ where z w = y + w

14+

src/Idris/AbsSyntaxTree.hs+1−3

@@ -408,6 +408,7 @@ data Command = Quit

408 | Apropos [String] String

409 | WhoCalls Name

410 | CallsWho Name

411+ | Browse [String]

411 | MakeDoc String -- IdrisDoc

412 | MakeDoc String -- IdrisDoc

412 | Warranty

413 | Warranty

413 | PrintDef Name

414 | PrintDef Name

@@ -1751,9 +1752,6 @@ showDeclImp o (PInstance _ _ _ _ cs n _ t _ ds)

1751showDeclImp _ _ = text "..."

1752showDeclImp _ _ = text "..."

1752-- showDeclImp (PImport o) = "import " ++ o

1753-- showDeclImp (PImport o) = "import " ++ o

1753

1754

1754−instance Show (Doc OutputAnnotation) where

1755− show = flip (displayS . renderCompact) ""

1756−

1757getImps :: [PArg] -> [(Name, PTerm)]

1755getImps :: [PArg] -> [(Name, PTerm)]

1758getImps [] = []

1756getImps [] = []

1759getImps (PImp _ _ _ n tm : xs) = (n, tm) : getImps xs

1757getImps (PImp _ _ _ n tm : xs) = (n, tm) : getImps xs

src/Idris/IdeMode.hs+2

@@ -222,6 +222,7 @@ data IdeModeCommand = REPLCompletions String

222 | Metavariables Int -- ^^ the Int is the column count for pretty-printing

223 | WhoCalls String

224 | CallsWho String

225+ | BrowseNS String

225 | TermNormalise [(Name, Bool)] Term

226 | TermNormalise [(Name, Bool)] Term

226 | TermShowImplicits [(Name, Bool)] Term

227 | TermShowImplicits [(Name, Bool)] Term

227 | TermNoImplicits [(Name, Bool)] Term

228 | TermNoImplicits [(Name, Bool)] Term

@@ -269,6 +270,7 @@ sexpToCommand (SexpList [SymbolAtom "set-option", SymbolAtom s, BoolAtom b])

269sexpToCommand (SexpList [SymbolAtom "metavariables", IntegerAtom cols]) = Just (Metavariables (fromIntegral cols))

270sexpToCommand (SexpList [SymbolAtom "metavariables", IntegerAtom cols]) = Just (Metavariables (fromIntegral cols))

270sexpToCommand (SexpList [SymbolAtom "who-calls", StringAtom name]) = Just (WhoCalls name)

271sexpToCommand (SexpList [SymbolAtom "who-calls", StringAtom name]) = Just (WhoCalls name)

271sexpToCommand (SexpList [SymbolAtom "calls-who", StringAtom name]) = Just (CallsWho name)

272sexpToCommand (SexpList [SymbolAtom "calls-who", StringAtom name]) = Just (CallsWho name)

273+sexpToCommand (SexpList [SymbolAtom "browse-namespace", StringAtom ns]) = Just (BrowseNS ns)

272sexpToCommand (SexpList [SymbolAtom "normalise-term", StringAtom encoded]) = let (bnd, tm) = decodeTerm encoded in

274sexpToCommand (SexpList [SymbolAtom "normalise-term", StringAtom encoded]) = let (bnd, tm) = decodeTerm encoded in

273 Just (TermNormalise bnd tm)

275 Just (TermNormalise bnd tm)

274sexpToCommand (SexpList [SymbolAtom "show-term-implicits", StringAtom encoded]) = let (bnd, tm) = decodeTerm encoded in

276sexpToCommand (SexpList [SymbolAtom "show-term-implicits", StringAtom encoded]) = let (bnd, tm) = decodeTerm encoded in

src/Idris/REPL.hs+32

@@ -34,6 +34,8 @@ import Idris.WhoCalls

34import Idris.TypeSearch (searchByType)

35import Idris.IBC (loadPkgIndex, writePkgIndex)

36

37+import Idris.REPL.Browse (namesInNS, namespacesInNS)

38+

37import Idris.Elab.Type

39import Idris.Elab.Type

38import Idris.Elab.Clause

40import Idris.Elab.Clause

39import Idris.Elab.Data

41import Idris.Elab.Data

@@ -463,6 +465,7 @@ runIdeModeCommand h id orig fn mods (IdeMode.WhoCalls n) =

463 renderPretty 0.9 1000 .

465 renderPretty 0.9 1000 .

464 fmap (fancifyAnnots ist) .

466 fmap (fancifyAnnots ist) .

465 prettyName True True []

467 prettyName True True []

468+

466runIdeModeCommand h id orig fn mods (IdeMode.CallsWho n) =

469runIdeModeCommand h id orig fn mods (IdeMode.CallsWho n) =

467 case splitName n of

470 case splitName n of

468 Left err -> iPrintError err

471 Left err -> iPrintError err

@@ -476,6 +479,20 @@ runIdeModeCommand h id orig fn mods (IdeMode.CallsWho n) =

476 fmap (fancifyAnnots ist) .

479 fmap (fancifyAnnots ist) .

477 prettyName True True []

480 prettyName True True []

478

481

482+runIdeModeCommand h id orig fn modes (IdeMode.BrowseNS ns) =

483+ case splitOn "." ns of

484+ [] -> iPrintError "No namespace provided"

485+ ns -> do underNSs <- fmap (map $ concat . intersperse ".") $ namespacesInNS ns

486+ names <- namesInNS ns

487+ if null underNSs && null names

488+ then iPrintError "Invalid or empty namespace"

489+ else do ist <- getIState

490+ let msg = (IdeMode.SymbolAtom "ok", (underNSs, map (pn ist) names))

491+ runIO . hPutStrLn h $ IdeMode.convSExp "return" msg id

492+ where pn ist = displaySpans .

493+ renderPretty 0.9 1000 .

494+ fmap (fancifyAnnots ist) .

495+ prettyName True True []

479runIdeModeCommand h id orig fn modes (IdeMode.TermNormalise bnd tm) =

496runIdeModeCommand h id orig fn modes (IdeMode.TermNormalise bnd tm) =

480 do ctxt <- getContext

497 do ctxt <- getContext

481 ist <- getIState

498 ist <- getIState

@@ -1257,6 +1274,21 @@ process fn (CallsWho n) =

1257 prettyName True True [] n <+> text "calls:" <$>

1274 prettyName True True [] n <+> text "calls:" <$>

1258 indent 1 (vsep (map ((text "*" <+>) . align . prettyName True True []) ns)))

1275 indent 1 (vsep (map ((text "*" <+>) . align . prettyName True True []) ns)))

1259 calls

1276 calls

1277+

1278+process fn (Browse ns) =

1279+ do underNSs <- namespacesInNS ns

1280+ names <- namesInNS ns

1281+ if null underNSs && null names

1282+ then iPrintError "Invalid or empty namespace"

1283+ else do ist <- getIState

1284+ iRenderResult $

1285+ text "Namespaces:" <$>

1286+ indent 2 (vsep (map (text . showSep ".") underNSs)) <$>

1287+ text "Names:" <$>

1288+ indent 2 (vsep (map (\n -> prettyName True False [] n <+> colon <+>

1289+ (group . align $ pprintDelabTy ist n))

1290+ names))

1291+

1260-- IdrisDoc

1292-- IdrisDoc

1261process fn (MakeDoc s) =

1293process fn (MakeDoc s) =

1262 do istate <- getIState

1294 do istate <- getIState

src/Idris/REPL/Browse.hsnew file+37

@@ -0,0 +1,37 @@

1+{-# OPTIONS_GHC -fwarn-incomplete-patterns -fwarn-unused-imports #-}

2+

3+module Idris.REPL.Browse (namespacesInNS, namesInNS) where

4+

5+import Data.List (isSuffixOf, nub)

6+import Data.Maybe (mapMaybe)

7+import qualified Data.Text as T (unpack)

8+

9+import Idris.Core.Evaluate (ctxtAlist)

10+import Idris.Core.TT (Name(..))

11+

12+import Idris.AbsSyntaxTree (Idris)

13+import Idris.AbsSyntax (getContext)

14+

15+-- | Find the sub-namespaces of a given namespace. The components

16+-- should be in display order rather than the order that they are in

17+-- inside of NS constructors.

18+namespacesInNS :: [String] -> Idris [[String]]

19+namespacesInNS ns = do let revNS = reverse ns

20+ allNames <- fmap ctxtAlist getContext

21+ return . nub $

22+ [ reverse space | space <- mapMaybe (getNS . fst) allNames

23+ , revNS `isSuffixOf` space

24+ , revNS /= space ]

25+ where getNS (NS _ namespace) = Just (map T.unpack namespace)

26+ getNS _ = Nothing

27+

28+-- | Find the user-accessible names that occur directly within a given

29+-- namespace. The components should be in display order rather than

30+-- the order that they are in inside of NS constructors.

31+namesInNS :: [String] -> Idris [Name]

32+namesInNS ns = do let revNS = reverse ns

33+ allNames <- fmap ctxtAlist getContext

34+ return [ n | (n, space) <- mapMaybe (getNS . fst) allNames

35+ , revNS == space ]

36+ where getNS n@(NS (UN n') namespace) = Just (n, (map T.unpack namespace))

37+ getNS _ = Nothing

src/Idris/REPLParser.hs+14−6

@@ -52,6 +52,7 @@ parserCommandsForHelp =

52 , " Search for values by type", cmd_search)

53 , nameArgCmd ["wc", "whocalls"] WhoCalls "List the callers of some name"

54 , nameArgCmd ["cw", "callswho"] CallsWho "List the callees of some name"

55+ , namespaceArgCmd ["browse"] Browse "List the contents of some namespace"

55 , nameArgCmd ["total"] TotCheck "Check the totality of a name"

56 , nameArgCmd ["total"] TotCheck "Check the totality of a name"

56 , noArgCmd ["r", "reload"] Reload "Reload current file"

57 , noArgCmd ["r", "reload"] Reload "Reload current file"

57 , (["l", "load"], FileArg, "Load a new file"

58 , (["l", "load"], FileArg, "Load a new file"

@@ -136,17 +137,19 @@ parserCommands =

136 )

137 )

137 ]

138 ]

138

139

139−noArgCmd names command doc =

140+noArgCmd names command doc =

140 (names, NoArg, doc, noArgs command)

141 (names, NoArg, doc, noArgs command)

141−nameArgCmd names command doc =

142+nameArgCmd names command doc =

142 (names, NameArg, doc, fnNameArg command)

143 (names, NameArg, doc, fnNameArg command)

144+namespaceArgCmd names command doc =

145+ (names, NamespaceArg, doc, namespaceArg command)

143−exprArgCmd names command doc =

146+exprArgCmd names command doc =

144 (names, ExprArg, doc, exprArg command)

147 (names, ExprArg, doc, exprArg command)

145−metavarArgCmd names command doc =

148+metavarArgCmd names command doc =

146 (names, MetaVarArg, doc, fnNameArg command)

149 (names, MetaVarArg, doc, fnNameArg command)

147−optArgCmd names command doc =

150+optArgCmd names command doc =

148 (names, OptionArg, doc, optArg command)

151 (names, OptionArg, doc, optArg command)

149−proofArgCmd names command doc =

152+proofArgCmd names command doc =

150 (names, NoArg, doc, proofArg command)

153 (names, NoArg, doc, proofArg command)

151

154

152pCmd :: P.IdrisParser (Either String Command)

155pCmd :: P.IdrisParser (Either String Command)

@@ -220,6 +223,11 @@ moduleArg = genArg "module" (fmap toPath P.identifier)

220 where

223 where

221 toPath n = foldl1' (</>) $ splitOn "." n

224 toPath n = foldl1' (</>) $ splitOn "." n

222

225

226+namespaceArg :: ([String] -> Command) -> String -> P.IdrisParser (Either String Command)

227+namespaceArg = genArg "namespace" (fmap toNS P.identifier)

228+ where

229+ toNS = splitOn "."

230+

223optArg :: (Opt -> Command) -> String -> P.IdrisParser (Either String Command)

231optArg :: (Opt -> Command) -> String -> P.IdrisParser (Either String Command)

224optArg cmd name = do

232optArg cmd name = do

225 let emptyArgs = do

233 let emptyArgs = do