4efeda8 · Idris-dev · git.iko.soy

CHANGELOG.md+1

compare with master

unifiedsplit

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

9+ Modules no longer require building if imports have changed but all

10 interfaces (i.e. types for names declared `export` and definitions of names

11 declared `public export`) are unchanged.

12++ The result of calling `:doc` now details the accessbility of items as well as their totality.

12

13

13## Miscellaneous updates

14## Miscellaneous updates

14+ Compiler flag `--optimise-nat-like-types` enables compilation

15+ Compiler flag `--optimise-nat-like-types` enables compilation

src/Idris/Core/Evaluate.hs+7

@@ -24,6 +24,7 @@ module Idris.Core.Evaluate(normalise, normaliseTrace, normaliseC,

24 lookupNames, lookupTyName, lookupTyNameExact, lookupTy, lookupTyExact,

25 lookupP, lookupP_all, lookupDef, lookupNameDef, lookupDefExact, lookupDefAcc, lookupDefAccExact, lookupVal,

26 mapDefCtxt, tcReducible,

27+ lookupTotalAccessibility,

27 lookupTotal, lookupTotalExact, lookupInjectiveExact,

28 lookupTotal, lookupTotalExact, lookupInjectiveExact,

28 lookupRigCount, lookupRigCountExact,

29 lookupRigCount, lookupRigCountExact,

29 lookupNameTotal, lookupMetaInformation, lookupTyEnv, isTCDict,

30 lookupNameTotal, lookupMetaInformation, lookupTyEnv, isTCDict,

@@ -1167,6 +1168,12 @@ lookupDefAcc n mkpublic ctxt

1167 where mkp (d, _, inj, a, _, _) = if mkpublic && (not (n == sUN "io_bind" || n == sUN "io_pure"))

1168 where mkp (d, _, inj, a, _, _) = if mkpublic && (not (n == sUN "io_bind" || n == sUN "io_pure"))

1168 then (d, Public) else (d, a)

1169 then (d, Public) else (d, a)

1169

1170

1171+lookupTotalAccessibility :: Name -> Context -> [(Totality,Accessibility)]

1172+lookupTotalAccessibility n ctxt = fmap unpack $ lookupCtxt n (definitions ctxt)

1173+

1174+ where

1175+ unpack ((_,_,_,a,t,_)) = (t,a)

1176+

1170lookupDefAccExact :: Name -> Bool -> Context ->

1177lookupDefAccExact :: Name -> Bool -> Context ->

1171 Maybe (Def, Accessibility)

1178 Maybe (Def, Accessibility)

1172lookupDefAccExact n mkpublic ctxt

1179lookupDefAccExact n mkpublic ctxt

src/Idris/Docs.hs+11−6

@@ -94,11 +94,9 @@ pprintFD ist totalityFlag nsFlag (FD n doc args ty f) =

94 (if not (null argshow)

95 then nest 4 $ text "Arguments:" <$> vsep argshow

96 else empty)

97− -- show totality status

97+ -- show totality and visibility status

98− <> let totality = getTotality in

98+ <> showTotalVisibility

99− (if totalityFlag && not (null totality)

99+ )

100− then line <> (vsep . map (\t -> text "The function is" <+> t) $ totality)

101− else empty))

102

100

103 where

101 where

104 ppo = ppOptionIst ist

102 ppo = ppOptionIst ist

@@ -135,7 +133,14 @@ pprintFD ist totalityFlag nsFlag (FD n doc args ty f) =

135 showArgs args ((n, True):bnd)

133 showArgs args ((n, True):bnd)

136 showArgs [] _ = [] -- end of arguments

134 showArgs [] _ = [] -- end of arguments

137

135

138− getTotality = map (text . show) $ lookupTotal n (tt_ctxt ist)

136+ showTotalVisibility =

137+ case lookupTotalAccessibility n (tt_ctxt ist) of

138+ [] -> empty

139+ xs -> line <> vsep (map (doShowTotalVisibility) xs)

140+

141+ doShowTotalVisibility (t,v) = if totalityFlag

142+ then text "The function is:" <+> ((text . show) t) <+> (text "&") <+> ((text . show) v)

143+ else text "The function is:" <+> ((text . show) v)

139

144

140pprintFDWithTotality :: IState -> Bool -> FunDoc -> Doc OutputAnnotation

145pprintFDWithTotality :: IState -> Bool -> FunDoc -> Doc OutputAnnotation

141pprintFDWithTotality ist = pprintFD ist True

146pprintFDWithTotality ist = pprintFD ist True

test/docs001/expected+1−1

@@ -8,7 +8,7 @@ Methods:

8 m : C t => t

9 member of interface

10

11− The function is Total

11+ The function is: Total & public export

12Implementations:

13 C A

14 implementation of interface

test/docs002/expected+3−3

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

1T1 : Type

2 Some documentation

3

4− The function is Total

4+ The function is: Total & public export

5T2 : Type

6 Some other documentation

7

8− The function is Total

8+ The function is: Total & public export

9T3 : Int

10 Some provided postulate

11

12− The function is not yet checked for totality

12+ The function is: not yet checked for totality & public export

test/docs003/expected+3−1

@@ -8,7 +8,7 @@ Methods:

8 map : Functor f => (func : a -> b) -> f a -> f b

9 Apply a function across everything of type 'a' in a parameterised type

10

11− The function is Total

11+ The function is: Total & public export

12Implementations:

13 Functor (Pair a)

14 Functor List

@@ -33,7 +33,9 @@ Named implementation:

33 docs003.mine : Functor List

34

35

36+ The function is: public export

36Named implementation:

37Named implementation:

37 docs003.another : Functor List

38 docs003.another : Functor List

38 More functors!

39 More functors!

39

40

41+ The function is: public export

test/docs004/expected+3−3

@@ -7,12 +7,12 @@ Main.MkFoo : (bar : Nat) -> (baz : Bool) -> Foo a

7

8 baz : Bool -- A field baz

9

10− The function is Total

10+ The function is: Total & public export

11Main.Foo.bar : (rec : Foo a) -> Nat

12 A field bar

13

14− The function is Total

14+ The function is: Total & public export

15Main.Foo.baz : (rec : Foo a) -> Bool

16 A field baz

17

18− The function is Total

18+ The function is: Total & public export

test/docs005/expected+3−1

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

1Data type docs005.Foobar : Type

2 A foobar with an auto implicit

3

4+ The function is: public export

4Constructors:

5Constructors:

5 NewFoo : (xs : List String) ->

6 NewFoo : (xs : List String) ->

6 (ys : List Nat) -> {auto prf : NonEmpty ys} -> Foobar

7 (ys : List Nat) -> {auto prf : NonEmpty ys} -> Foobar

@@ -14,6 +15,7 @@ Constructors:

14

15

15 (auto implicit) prf : NonEmpty ys -- The prf

16 (auto implicit) prf : NonEmpty ys -- The prf

16

17

18+ The function is: public export

17docs005.NewFoo : (xs : List String) ->

19docs005.NewFoo : (xs : List String) ->

18 (ys : List Nat) -> {auto prf : NonEmpty ys} -> Foobar

20 (ys : List Nat) -> {auto prf : NonEmpty ys} -> Foobar

19 New Foo

21 New Foo

@@ -26,4 +28,4 @@ docs005.NewFoo : (xs : List String) ->

26

28

27 (auto implicit) prf : NonEmpty ys -- The prf

29 (auto implicit) prf : NonEmpty ys -- The prf

28

30

29− The function is Total

31+ The function is: Total & public export

test/docs006/expected+1−1

@@ -11,6 +11,6 @@ Methods:

11 m : Foo t => t

12 member of interface

13

14− The function is Total

14+ The function is: Total & public export

15Implementations:

16 <no implementations>

test/idrisdoc009/expected+2

@@ -1,10 +1,12 @@

1Data type Test.Test : Type

2 Docs for datatype Test.

3

4+ The function is: public export

4Constructors:

5Constructors:

5 MkTest : Test

6 MkTest : Test

6

7

8

9+ The function is: public export

8Module Test:

10Module Test:

9 Docs for module Test.

11 Docs for module Test.

10

12

test/interactive005/expected+3−3

@@ -3,7 +3,7 @@ Hello, World

3Main.main : IO ()

4 This is a docstring

5

6− The function is Total

6+ The function is: Total & public export

7Main.main is Total

8Hello, World

9id : a -> a

@@ -27,10 +27,10 @@ Main.main : IO ()

27 is a

28 docstring

29

30− The function is Total

30+ The function is: Total & public export

31Main.main : IO ()

32 This is a docstring

33

34− The function is Total

34+ The function is: Total & public export

35Nat2 : Type

36Invalid filename for compiler output "Test.idr"

test/interfaces001/expected+3−2

@@ -8,7 +8,7 @@ Methods:

8 myShow : MyShow a => (x : a) -> String

9 The shower

10

11− The function is Total

11+ The function is: Total & public export

12Implementation constructor:

13 MkMyShow : (myShow : a -> String) -> MyShow a

14 Build a MyShow

@@ -17,6 +17,7 @@ Implementation constructor:

17

18 myShow : a -> String -- The shower

19

20+ The function is: public export

20Implementations:

21Implementations:

21 MyShow Integer

22 MyShow Integer

22MkMyShow : (myShow : a -> String) -> MyShow a

23MkMyShow : (myShow : a -> String) -> MyShow a

@@ -26,4 +27,4 @@ MkMyShow : (myShow : a -> String) -> MyShow a

26

27

27 myShow : a -> String -- The shower

28 myShow : a -> String -- The shower

28

29

29− The function is Total

30+ The function is: Total & public export