6e74bd7 · Idris-dev · git.iko.soy

git.iko.soy/Idris-dev

on master help sign in

Merge pull request #945 from david-christiansen/new-docs

6e74bd7Edwin Brady13 years ago

CHANGELOG+6

compare with master

unifiedsplit

@@ -10,6 +10,12 @@ New in 0.9.12:

10* New commands :eval (:e) and :type (:t) in the prover, which either normalise

11 or show the type of expressions

12* Allow type providers to return postulates in addition to terms

13+* New syntax for inline documentation. Documentation starts with |||, and

14+ arguments are documented by preceding their name with @. Example:

15+||| Add two natural numbers

16+||| @ n the first number (examined by the function)

17+||| @ m the second number (not examined)

18+plus (n, m : Nat) -> Nat

14New in 0.9.11:

20New in 0.9.11:

15--------------

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

libs/base/Data/ZZ.idr+2−2

@@ -7,8 +7,8 @@ import Data.Sign

7%access public

10−-- | An integer is either a positive nat or the negated successor of a nat.

10+||| An integer is either a positive nat or the negated successor of a nat.

11−-- Zero is chosen to be positive.

11+||| Zero is arbitrarily chosen to be positive.

12data ZZ = Pos Nat | NegS Nat

14instance Signed ZZ where

libs/base/Debug/Trace.idr+4−1

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

1module Debug.Trace

3+||| Print a message for debugging purposes as a side effect

4+||| @ msg what to print

5+||| @ result the final result

3−trace : String -> a -> a

6+trace : (msg : String) -> (result : a) -> a

4trace x val = unsafePerformIO (do putStrLn x; return val)

7trace x val = unsafePerformIO (do putStrLn x; return val)

libs/base/Decidable/Order.idr+1−1

@@ -21,7 +21,7 @@ class (Preorder t po) => Poset t (po : t -> t -> Type) where

21 total antisymmetric : (a : t) -> (b : t) -> po a b -> po b a -> a = b

23class (Poset t to) => Ordered t (to : t -> t -> Type) where

24− total order : (a : t) -> (b : t) -> Either (to a b) (to b a)

24+ total order : (a : t) -> (b : t) -> Either (to a b) (to b a)

26minimum : (Ordered t to) => t -> t -> t

27minimum x y with (order x y)

libs/base/Language/Reflection.idr+6−6

@@ -22,7 +22,7 @@ data TTUExp = UVar Int

22 -- ^ explicit universe variable

23%name TTUExp uexp

25−-- | Primitive constants

25+||| Primitive constants

26data Const = I Int | BI Integer | Fl Float | Ch Char | Str String

28 | B8 Bits8 | B16 Bits16 | B32 Bits32 | B64 Bits64

@@ -66,7 +66,7 @@ reflectConstant: (ReflConst a) => a -> Const

66reflectConstant = toConst

69−-- | Types of named references

69+||| Types of named references

70data NameType = Bound

71 -- ^ reference which is just bound, e.g. by intro

72 | Ref

@@ -77,8 +77,8 @@ data NameType = Bound

77 -- ^ type constructor with tag and number

78%name NameType nt, nt'

80−-- | Types annotations for bound variables in different

80+||| Types annotations for bound variables in different

81−-- binding contexts

81+||| binding contexts

82data Binder a = Lam a

83 | Pi a

84 | Let a a

@@ -124,7 +124,7 @@ instance Traversable Binder where

124 traverse f (PVTy x) = [| PVTy (f x) |]

125

126

127−-- | Reflection of the well typed core language

127+||| Reflection of the well typed core language

128data TT = P NameType TTName TT

129 -- ^ named binders

130 | V Int

@@ -146,7 +146,7 @@ data TT = P NameType TTName TT

146

147%name TT tm, tm'

148

149−-- | Raw terms without types

149+||| Raw terms without types

150data Raw = Var TTName

151 | RBind TTName (Binder Raw) Raw

152 | RApp Raw Raw

libs/base/Language/Reflection/Errors.idr+1−1

@@ -42,7 +42,7 @@ data Err = Msg String

43%name Err err, e

45−-- | Error reports are a list of report parts

45+||| Error reports are a list of report parts

46data ErrorReportPart = TextPart String

47 | NamePart TTName

48 | TermPart TT

libs/base/Providers.idr+12−1

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

1module Providers

3+||| Type providers must build one of these in an IO computation.

3public

4public

4−data Provider a = Provide a | Error String | Postulate

5+data Provider : (a : Type) -> Type where

6+ ||| Return a term to be spliced in

7+ ||| @ x the term to be spliced (i.e. the proof)

8+ Provide : (x : a) -> Provider a

10+ ||| Report an error to the user and stop compilation

11+ ||| @ msg the error message

12+ Error : (msg : String) -> Provider a

13+

14+ ||| Postulate the goal type

15+ Postulate : Provider a

6-- instances

17-- instances

7instance Functor Provider where

18instance Functor Provider where

libs/base/System.idr+9−6

@@ -5,6 +5,7 @@ import Prelude

5%default partial

6%access public

8+||| Get the command-line arguments that the program was called with.

8getArgs : IO (List String)

9getArgs : IO (List String)

9getArgs = do n <- numArgs

10getArgs = do n <- numArgs

10 ga' [] 0 n

11 ga' [] 0 n

@@ -20,8 +21,8 @@ getArgs = do n <- numArgs

20 do arg <- getArg i

21 do arg <- getArg i

21 ga' (arg :: acc) (i+1) n

22 ga' (arg :: acc) (i+1) n

23−-- Retrieves an value from the environment, if the given key is present,

24+||| Retrieves an value from the environment, if the given key is present,

24−-- otherwise it returns Nothing.

25+||| otherwise it returns Nothing.

25getEnv : String -> IO (Maybe String)

26getEnv : String -> IO (Maybe String)

26getEnv key = do

27getEnv key = do

27 str_ptr <- getEnv'

28 str_ptr <- getEnv'

@@ -33,15 +34,15 @@ getEnv key = do

33 getEnv' : IO String

34 getEnv' : IO String

34 getEnv' = mkForeign (FFun "getenv" [FString] FString) key

35 getEnv' = mkForeign (FFun "getenv" [FString] FString) key

36−-- Sets an environment variable with a given value.

37+||| Sets an environment variable with a given value.

37−-- Returns true if the operation was successful.

38+||| Returns true if the operation was successful.

38setEnv : String -> String -> IO Bool

39setEnv : String -> String -> IO Bool

39setEnv key value = do

40setEnv key value = do

40 ok <- mkForeign (FFun "setenv" [FString, FString, FInt] FInt) key value 1

41 ok <- mkForeign (FFun "setenv" [FString, FString, FInt] FInt) key value 1

41 return (ok == 0)

42 return (ok == 0)

43−-- Unsets an environment variable.

44+||| Unsets an environment variable.

44−-- Returns true if the variable was able to be unset.

45+||| Returns true if the variable was able to be unset.

45unsetEnv : String -> IO Bool

46unsetEnv : String -> IO Bool

46unsetEnv key = do

47unsetEnv key = do

47 ok <- mkForeign (FFun "unsetenv" [FString] FInt) key

48 ok <- mkForeign (FFun "unsetenv" [FString] FInt) key

@@ -68,9 +69,11 @@ getEnvironment = getAllPairs 0 []

68 then return $ reverse $ map splitEq acc

69 then return $ reverse $ map splitEq acc

69 else getAllPairs (n + 1) (envPair :: acc)

70 else getAllPairs (n + 1) (envPair :: acc)

72+||| Quit with a particular exit code

71exit : Int -> IO ()

73exit : Int -> IO ()

72exit code = mkForeign (FFun "exit" [FInt] FUnit) code

74exit code = mkForeign (FFun "exit" [FInt] FUnit) code

76+||| Get the Unix time

74time : IO Int

77time : IO Int

75time = mkForeign (FFun "idris_time" [] FInt)

78time = mkForeign (FFun "idris_time" [] FInt)

libs/prelude/Builtins.idr+22−8

@@ -3,27 +3,35 @@

3%access public

4%default total

6+||| Dependent pairs, in their internal representation

7+||| @ a the type of the witness

8+||| @ P the type of the proof

6data Exists : (a : Type) -> (P : a -> Type) -> Type where

9data Exists : (a : Type) -> (P : a -> Type) -> Type where

7 Ex_intro : {P : a -> Type} -> (x : a) -> P x -> Exists a P

10 Ex_intro : {P : a -> Type} -> (x : a) -> P x -> Exists a P

12+||| The first projection from a dependent pair

9getWitness : {P : a -> Type} -> Exists a P -> a

13getWitness : {P : a -> Type} -> Exists a P -> a

10getWitness (a ** v) = a

14getWitness (a ** v) = a

16+||| The second projection from a dependent pair

12getProof : {P : a -> Type} -> (s : Exists a P) -> P (getWitness s)

17getProof : {P : a -> Type} -> (s : Exists a P) -> P (getWitness s)

13getProof (a ** v) = v

18getProof (a ** v) = v

15FalseElim : _|_ -> a

20FalseElim : _|_ -> a

17−-- For 'symbol syntax. 'foo becomes Symbol_ "foo"

22+||| For 'symbol syntax. 'foo becomes Symbol_ "foo"

18data Symbol_ : String -> Type where

23data Symbol_ : String -> Type where

20-- ------------------------------------------------------ [ For rewrite tactic ]

25-- ------------------------------------------------------ [ For rewrite tactic ]

26+||| Perform substitution in a term. This is used by the `rewrite` tactic and term.

21replace : {a:_} -> {x:_} -> {y:_} -> {P : a -> Type} -> x = y -> P x -> P y

27replace : {a:_} -> {x:_} -> {y:_} -> {P : a -> Type} -> x = y -> P x -> P y

22replace refl prf = prf

28replace refl prf = prf

30+||| Symmetry of propositional equality

24sym : {l:a} -> {r:a} -> l = r -> r = l

31sym : {l:a} -> {r:a} -> l = r -> r = l

25sym refl = refl

32sym refl = refl

34+||| Transitivity of propositional equality

27trans : {a:x} -> {b:x} -> {c:x} -> a = b -> b = c -> a = c

35trans : {a:x} -> {b:x} -> {c:x} -> a = b -> b = c -> a = c

28trans refl refl = refl

36trans refl refl = refl

@@ -48,21 +56,27 @@ malloc size x = x -- compiled specially

48trace_malloc : a -> a

56trace_malloc : a -> a

49trace_malloc x = x -- compiled specially

57trace_malloc x = x -- compiled specially

51−-- Assert to the totality checker than y is always structureally smaller than

59+||| Assert to the totality checker than y is always structurally smaller than

52−-- x (which is typically a pattern argument)

60+||| x (which is typically a pattern argument)

61+||| @ x the larger value (typically a pattern argument)

62+||| @ y the smaller value (typically an argument to a recursive call)

53−assert_smaller : a -> a -> a

63+assert_smaller : (x, y : a) -> a

54assert_smaller x y = y

64assert_smaller x y = y

56−-- Assert to the totality checker than the given expression will always

66+||| Assert to the totality checker than the given expression will always

57−-- terminate.

67+||| terminate.

58assert_total : a -> a

68assert_total : a -> a

59assert_total x = x

69assert_total x = x

71+||| Subvert the type checker. This function is abstract, so it will not reduce in

72+||| the type checker. Use it with care - it can result in segfaults or worse!

61abstract %assert_total -- need to pretend

73abstract %assert_total -- need to pretend

62−believe_me : a -> b -- compiled specially as id, use with care!

74+believe_me : a -> b

63believe_me x = prim__believe_me _ _ x

75believe_me x = prim__believe_me _ _ x

65−public %assert_total -- reduces at compile time, use with extreme care!

77+||| Subvert the type checker. This function *will* reduce in the type checker.

78+||| Use it with extreme care - it can result in segfaults or worse!

79+public %assert_total

66really_believe_me : a -> b

80really_believe_me : a -> b

67really_believe_me x = prim__believe_me _ _ x

81really_believe_me x = prim__believe_me _ _ x

libs/prelude/Prelude/Applicative.idr+3

@@ -19,12 +19,15 @@ infixl 2 $>

19($>) : Applicative f => f a -> f b -> f b

20a $> b = map (const id) a <$> b

22+||| Lift a function to an applicative

22liftA : Applicative f => (a -> b) -> f a -> f b

23liftA : Applicative f => (a -> b) -> f a -> f b

23liftA f a = pure f <$> a

24liftA f a = pure f <$> a

26+||| Lift a two-argument function to an applicative

25liftA2 : Applicative f => (a -> b -> c) -> f a -> f b -> f c

27liftA2 : Applicative f => (a -> b -> c) -> f a -> f b -> f c

26liftA2 f a b = (map f a) <$> b

28liftA2 f a b = (map f a) <$> b

30+||| Lift a three-argument function to an applicative

28liftA3 : Applicative f => (a -> b -> c -> d) -> f a -> f b -> f c -> f d

31liftA3 : Applicative f => (a -> b -> c -> d) -> f a -> f b -> f c -> f d

29liftA3 f a b c = (map f a) <$> b <$> c

32liftA3 f a b c = (map f a) <$> b <$> c

libs/prelude/Prelude/Basics.idr+23−12

@@ -3,44 +3,55 @@ module Prelude.Basics

3Not : Type -> Type

4Not a = a -> _|_

6−-- | Identity function.

6+||| Identity function.

7id : a -> a

8id x = x

10−-- | Manually assign a type to an expression.

10+||| Manually assign a type to an expression.

11+||| @ a the type to assign

12+||| @ x the element to get the type

11−the : (a : Type) -> a -> a

13+the : (a : Type) -> (x : a) -> a

12the _ = id

14the _ = id

14−-- | Constant function.

16+||| Constant function. Ignores its second argument.

15const : a -> b -> a

17const : a -> b -> a

16const x = \v => x

18const x = \v => x

18−-- | Return the first element of a pair.

20+||| Return the first element of a pair.

19fst : (s, t) -> s

21fst : (s, t) -> s

20fst (x, y) = x

22fst (x, y) = x

22−-- | Return the second element of a pair.

24+||| Return the second element of a pair.

23snd : (a, b) -> b

25snd : (a, b) -> b

24snd (x, y) = y

26snd (x, y) = y

26infixl 9 .

28infixl 9 .

28−-- | Function composition

30+||| Function composition

29(.) : (b -> c) -> (a -> b) -> a -> c

31(.) : (b -> c) -> (a -> b) -> a -> c

30(.) f g x = f (g x)

32(.) f g x = f (g x)

32−-- | Takes in the first two arguments in reverse order.

34+||| Takes in the first two arguments in reverse order.

35+||| @ f the function to flip

33−flip : (a -> b -> c) -> b -> a -> c

36+flip : (f : a -> b -> c) -> b -> a -> c

34flip f x y = f y x

37flip f x y = f y x

36−-- | Function application.

39+||| Function application.

37apply : (a -> b) -> a -> b

40apply : (a -> b) -> a -> b

38apply f a = f a

41apply f a = f a

43+||| Equality is a congruence.

40cong : {f : t -> u} -> (a = b) -> f a = f b

44cong : {f : t -> u} -> (a = b) -> f a = f b

41cong refl = refl

45cong refl = refl

47+||| Decidability. A decidable property either holds or is a contradiction.

43data Dec : Type -> Type where

48data Dec : Type -> Type where

49+

50+ ||| The case where the property holds

51+ ||| @ prf the proof

44− Yes : {A : Type} -> A -> Dec A

52+ Yes : {A : Type} -> (prf : A) -> Dec A

53+

54+ ||| The case where the property holding would be a contradiction

55+ ||| @ contra a demonstration that A would be a contradiction

45− No : {A : Type} -> (A -> _|_) -> Dec A

56+ No : {A : Type} -> (contra : A -> _|_) -> Dec A

libs/prelude/Prelude/Bool.idr+10−7

@@ -1,14 +1,17 @@

1module Prelude.Bool

3−-- | Boolean Data Type

3+||| Boolean Data Type

4data Bool = False | True

6−-- | Boolean elimination

6+||| The underlying implementation of the if ... then ... else ... syntax

7+||| @ b the condition on the if

8+||| @ t the value if b is true

9+||| @ e the falue if b is false

7−boolElim : Bool -> (t : Lazy a) -> (e : Lazy a) -> a

10+boolElim : (b : Bool) -> (t : Lazy a) -> (e : Lazy a) -> a

8boolElim True t e = t

11boolElim True t e = t

9boolElim False t e = e

12boolElim False t e = e

11−-- | Defines a predicate on Bool which guarantees that the value is true.

14+||| Defines a predicate on Bool which guarantees that the value is true.

12data so : Bool -> Type where oh : so True

15data so : Bool -> Type where oh : so True

14-- Syntaxtic sugar for boolean elimination.

17-- Syntaxtic sugar for boolean elimination.

@@ -17,17 +20,17 @@ syntax if [test] then [t] else [e] = boolElim test (Delay t) (Delay e)

17-- Boolean Operator Precedence

20-- Boolean Operator Precedence

18infixl 4 &&, ||

21infixl 4 &&, ||

20−-- | Boolean OR

23+||| Boolean OR

21(||) : Bool -> Bool -> Bool

24(||) : Bool -> Bool -> Bool

22(||) False x = x

25(||) False x = x

23(||) True _ = True

26(||) True _ = True

25−-- | Boolean AND

28+||| Boolean AND

26(&&) : Bool -> Bool -> Bool

29(&&) : Bool -> Bool -> Bool

27(&&) True x = x

30(&&) True x = x

28(&&) False _ = False

31(&&) False _ = False

30−-- | Boolean NOT

33+||| Boolean NOT

31not : Bool -> Bool

34not : Bool -> Bool

32not True = False

35not True = False

33not False = True

36not False = True

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

@@ -3,67 +3,67 @@ module Prelude.Char

4import Builtins

6−-- | Return the ASCII representation of the character.

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

7chr : Int -> Char

8chr x = prim__intToChar x

10−-- | Convert the number to its ASCII equivalent.

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

11ord : Char -> Int

12ord x = prim__charToInt x

14−-- | Returns true if the character is in the range [A-Z].

14+||| Returns true if the character is in the range [A-Z].

15isUpper : Char -> Bool

16isUpper x = x >= 'A' && x <= 'Z'

18−-- | Returns true if the character is in the range [a-z]

18+||| Returns true if the character is in the range [a-z]

19isLower : Char -> Bool

20isLower x = x >= 'a' && x <= 'z'

22−-- | Returns true if the character is in the ranges [A-Z][a-z].

22+||| Returns true if the character is in the ranges [A-Z][a-z].

23isAlpha : Char -> Bool

24isAlpha x = isUpper x || isLower x

26−-- | Returns true if the character is in the range [0-9]

26+||| Returns true if the character is in the range [0-9]

27isDigit : Char -> Bool

28isDigit x = (x >= '0' && x <= '9')

30−-- | Returns true if the character is in the ranges [A-Z][a-z][0-9]

30+||| Returns true if the character is in the ranges [A-Z][a-z][0-9]

31isAlphaNum : Char -> Bool

32isAlphaNum x = isDigit x || isAlpha x

34−-- | Returns true if the character is a whitespace character.

34+||| Returns true if the character is a whitespace character.

35isSpace : Char -> Bool

36isSpace x = x == ' ' || x == '\t' || x == '\r' ||

37 x == '\n' || x == '\f' || x == '\v' ||

38 x == '\xa0'

40−-- | Returns true if the character represents a new line.

40+||| Returns true if the character represents a new line.

41isNL : Char -> Bool

42isNL x = x == '\r' || x == '\n'

44−-- | Convert a letter to the corresponding upper-case letter, if any.

44+||| Convert a letter to the corresponding upper-case letter, if any.

45−-- Non-letters are ignored.

45+||| Non-letters are ignored.

46toUpper : Char -> Char

47toUpper x = if (isLower x)

48 then (prim__intToChar (prim__charToInt x - 32))

49 else x

51−-- | Convert a letter to the corresponding lower-case letter, if any.

51+||| Convert a letter to the corresponding lower-case letter, if any.

52−-- Non-letters are ignored.

52+||| Non-letters are ignored.

53toLower : Char -> Char

54toLower x = if (isUpper x)

55 then (prim__intToChar (prim__charToInt x + 32))

56 else x

58−-- | Returns true if the character is a hexadecimal digit i.e. in the range [0-9][a-f][A-F]

58+||| Returns true if the character is a hexadecimal digit i.e. in the range [0-9][a-f][A-F]

59isHexDigit : Char -> Bool

60isHexDigit x = elem (toUpper x) hexChars where

61 hexChars : List Char

62 hexChars = ['0', '1', '2', '3', '4', '5', '6', '7', '8', '9',

63 'A', 'B', 'C', 'D', 'E', 'F']

65−-- | Returns true if the character is an octal digit.

65+||| Returns true if the character is an octal digit.

66isOctDigit : Char -> Bool

67isOctDigit x = (x >= '0' && x <= '7')

69−-- --------------------------------------------------------------------- [ EOF ]

69+

libs/prelude/Prelude/Classes.idr+8−8

@@ -20,7 +20,7 @@ boolOp : (a -> a -> Int) -> a -> a -> Bool

20boolOp op x y = intToBool (op x y)

22-- ---------------------------------------------------------- [ Equality Class ]

23−-- | The Eq class defines inequality and equality.

23+||| The Eq class defines inequality and equality.

24class Eq a where

25 (==) : a -> a -> Bool

26 (/=) : a -> a -> Bool

@@ -65,7 +65,7 @@ instance Eq Ordering where

65 GT == GT = True

66 _ == _ = False

68−-- | The Ord class defines comparison operations on ordered data types.

68+||| The Ord class defines comparison operations on ordered data types.

69class Eq a => Ord a where

70 compare : a -> a -> Ordering

@@ -131,14 +131,14 @@ instance (Ord a, Ord b) => Ord (a, b) where

131 else compare xr yr

132

133-- --------------------------------------------------------- [ Numerical Class ]

134−-- | The Num class defines basic numerical arithmetic.

134+||| The Num class defines basic numerical arithmetic.

135class Num a where

136 (+) : a -> a -> a

137 (-) : a -> a -> a

138 (*) : a -> a -> a

139− -- | Absolute value

139+ ||| Absolute value

140 abs : a -> a

141− -- | Conversion from Integer.

141+ ||| Conversion from Integer.

142 fromInteger : Integer -> a

143

144instance Num Integer where

@@ -245,11 +245,11 @@ instance Ord Bits64 where

245-- ------------------------------------------------------------- [ Bounded ]

246

247class MinBound b where

248− -- | The lower bound for the type

248+ ||| The lower bound for the type

249 minBound : b

250

251class MaxBound b where

252− -- | The upper bound for the type

252+ ||| The upper bound for the type

253 maxBound : b

254

255instance MinBound Bits16 where

@@ -273,7 +273,7 @@ instance MaxBound Bits64 where

273

274-- ------------------------------------------------------------- [ Fractionals ]

275

276−-- | Fractional division of two Floats.

276+||| Fractional division of two Floats.

277(/) : Float -> Float -> Float

278(/) = prim__divFloat

279

libs/prelude/Prelude/Either.idr+13−5

@@ -1,13 +1,16 @@

1−module Prelude.Either

1+ module Prelude.Either

3import Builtins

5import Prelude.Maybe

6import Prelude.List

8+||| A sum type

8−data Either a b

9+data Either a b =

10+ ||| One possibility of the sum, conventionally used to represent errors

9− = Left a

11+ Left a |

12+ ||| The other possibility, conventionally used to represent success

10− | Right b

13+ Right b

12--------------------------------------------------------------------------------

15--------------------------------------------------------------------------------

13-- Syntactic tests

16-- Syntactic tests

@@ -25,11 +28,16 @@ isRight (Right r) = True

25-- Misc.

28-- Misc.

26--------------------------------------------------------------------------------

29--------------------------------------------------------------------------------

31+||| Perform a case analysis on a Boolean, providing clients with a `so` proof

28choose : (b : Bool) -> Either (so b) (so (not b))

32choose : (b : Bool) -> Either (so b) (so (not b))

29choose True = Left oh

33choose True = Left oh

30choose False = Right oh

34choose False = Right oh

36+||| Simply-typed eliminator for Either

37+||| @ f the action to take on Left

38+||| @ g the action to take on Right

39+||| @ e the sum to analyze

32−either : (a -> c) -> (b -> c) -> Either a b -> c

40+either : (f : a -> c) -> (g : b -> c) -> (e : Either a b) -> c

33either l r (Left x) = l x

41either l r (Left x) = l x

34either l r (Right x) = r x

42either l r (Right x) = r x

libs/prelude/Prelude/Fin.idr+11−1

@@ -5,7 +5,9 @@ import Prelude.Either

6%default total

8+||| Numbers strictly less than some bound. The name comes from "finite sets"

9+||| @ n the upper bound

8−data Fin : Nat -> Type where

10+data Fin : (n : Nat) -> Type where

9 fZ : Fin (S k)

11 fZ : Fin (S k)

10 fS : Fin k -> Fin (S k)

12 fS : Fin k -> Fin (S k)

@@ -44,14 +46,18 @@ finToInteger (fS k) = 1 + finToInteger k

44instance Cast (Fin n) Integer where

46instance Cast (Fin n) Integer where

45 cast x = finToInteger x

47 cast x = finToInteger x

49+||| Weaken the bound on a Fin by 1

47weaken : Fin n -> Fin (S n)

50weaken : Fin n -> Fin (S n)

48weaken fZ = fZ

51weaken fZ = fZ

49weaken (fS k) = fS (weaken k)

52weaken (fS k) = fS (weaken k)

54+||| Weaken the bound on a Fin by some amount

51weakenN : (n : Nat) -> Fin m -> Fin (m + n)

55weakenN : (n : Nat) -> Fin m -> Fin (m + n)

52weakenN n fZ = fZ

56weakenN n fZ = fZ

53weakenN n (fS f) = fS (weakenN n f)

57weakenN n (fS f) = fS (weakenN n f)

59+||| Attempt to tighten the bound on a Fin.

60+||| Return `Left` if the bound could not be tightened, or `Right` if it could.

55strengthen : Fin (S n) -> Either (Fin (S n)) (Fin n)

61strengthen : Fin (S n) -> Either (Fin (S n)) (Fin n)

56strengthen {n = S k} fZ = Right fZ

62strengthen {n = S k} fZ = Right fZ

57strengthen {n = S k} (fS i) with (strengthen i)

63strengthen {n = S k} (fS i) with (strengthen i)

@@ -59,10 +65,14 @@ strengthen {n = S k} (fS i) with (strengthen i)

59 strengthen (fS k) | Right x = Right (fS x)

65 strengthen (fS k) | Right x = Right (fS x)

60strengthen f = Left f

66strengthen f = Left f

68+||| Add some natural number to a Fin, extending the bound accordingly

69+||| @ n the previous bound

70+||| @ m the number to increase the Fin by

62shift : (m : Nat) -> Fin n -> Fin (m + n)

71shift : (m : Nat) -> Fin n -> Fin (m + n)

63shift Z f = f

72shift Z f = f

64shift {n=n} (S m) f = fS {k = (m + n)} (shift m f)

73shift {n=n} (S m) f = fS {k = (m + n)} (shift m f)

75+||| The largest element of some Fin type

66last : Fin (S n)

76last : Fin (S n)

67last {n=Z} = fZ

77last {n=Z} = fZ

68last {n=S _} = fS last

78last {n=S _} = fS last

libs/prelude/Prelude/Functor.idr+6−1

@@ -1,4 +1,9 @@

1module Prelude.Functor

3+||| Functors

4+||| @ f the action of the functor on objects

3class Functor (f : Type -> Type) where

5class Functor (f : Type -> Type) where

6+ ||| The action of the functor on morphisms

7+ ||| @ f the functor

8+ ||| @ m the morphism

4− map : (a -> b) -> f a -> f b

9+ map : (m : a -> b) -> f a -> f b

libs/prelude/Prelude/List.idr+11−11

@@ -269,17 +269,17 @@ intersperse sep (x::xs) = x :: intersperse' sep xs

269intercalate : List a -> List (List a) -> List a

270intercalate sep l = concat $ intersperse sep l

271

272−-- | Transposes rows and columns of a list of lists.

272+||| Transposes rows and columns of a list of lists.

273−--

273+|||

274−-- > transpose [[1, 2], [3, 4]] = [[1, 3], [2, 4]]

274+||| > transpose [[1, 2], [3, 4]] = [[1, 3], [2, 4]]

275−--

275+|||

276−-- This also works for non square scenarios, thus

276+||| This also works for non square scenarios, thus

277−-- involution does not always hold:

277+||| involution does not always hold:

278−--

278+|||

279−-- > transpose [[], [1, 2]] = [[1], [2]]

279+||| > transpose [[], [1, 2]] = [[1], [2]]

280−-- > transpose (transpose [[], [1, 2]]) = [[1, 2]]

280+||| > transpose (transpose [[], [1, 2]]) = [[1, 2]]

281−--

281+|||

282−-- TODO: Solution which satisfies the totality checker?

282+||| TODO: Solution which satisfies the totality checker?

283%assert_total

284transpose : List (List a) -> List (List a)

285transpose [] = []

libs/prelude/Prelude/Nat.idr+38−5

@@ -10,9 +10,12 @@ import Prelude.Classes

10%access public

11%default total

13+||| Unary natural numbers

13−%elim data Nat

14+%elim data Nat =

15+ ||| Zero

14− = Z

16+ Z |

17+ ||| Successor

15− | S Nat

18+ S Nat

17-- name hints for interactive editing

20-- name hints for interactive editing

18%name Nat k,j,i,n,m

21%name Nat k,j,i,n,m

@@ -33,14 +36,19 @@ isSucc (S n) = True

33-- Basic arithmetic functions

36-- Basic arithmetic functions

34--------------------------------------------------------------------------------

37--------------------------------------------------------------------------------

39+||| Add two natural numbers.

40+||| @ n the number to case-split on

41+||| @ m the other number

36−total plus : Nat -> Nat -> Nat

42+total plus : (n, m : Nat) -> Nat

37plus Z right = right

43plus Z right = right

38plus (S left) right = S (plus left right)

44plus (S left) right = S (plus left right)

46+||| Multiply natural numbers

40total mult : Nat -> Nat -> Nat

47total mult : Nat -> Nat -> Nat

41mult Z right = Z

48mult Z right = Z

42mult (S left) right = plus right $ mult left right

49mult (S left) right = plus right $ mult left right

51+||| Convert an Integer to a Nat, mapping negative numbers to 0

44fromIntegerNat : Integer -> Nat

52fromIntegerNat : Integer -> Nat

45fromIntegerNat 0 = Z

53fromIntegerNat 0 = Z

46fromIntegerNat n =

54fromIntegerNat n =

@@ -49,15 +57,18 @@ fromIntegerNat n =

49 else

57 else

50 Z

58 Z

60+||| Convert a Nat to an Integer

52toIntegerNat : Nat -> Integer

61toIntegerNat : Nat -> Integer

53toIntegerNat Z = 0

62toIntegerNat Z = 0

54toIntegerNat (S k) = 1 + toIntegerNat k

63toIntegerNat (S k) = 1 + toIntegerNat k

65+||| Subtract natural numbers. If the second number is larger than the first, return 0.

56total minus : Nat -> Nat -> Nat

66total minus : Nat -> Nat -> Nat

57minus Z right = Z

67minus Z right = Z

58minus left Z = left

68minus left Z = left

59minus (S left) (S right) = minus left right

69minus (S left) (S right) = minus left right

71+||| Exponentiation of natural numbers

61total power : Nat -> Nat -> Nat

72total power : Nat -> Nat -> Nat

62power base Z = S Z

73power base Z = S Z

63power base (S exp) = mult base $ power base exp

74power base (S exp) = mult base $ power base exp

@@ -74,33 +85,46 @@ hyper (S pn) a (S pb) = hyper pn a (hyper (S pn) a pb)

74-- Comparisons

85-- Comparisons

75--------------------------------------------------------------------------------

86--------------------------------------------------------------------------------

88+||| Proofs that `n` is less than or equal to `m`

89+||| @ n the smaller number

90+||| @ m the larger number

77−data LTE : Nat -> Nat -> Type where

91+data LTE : (n, m : Nat) -> Type where

92+ ||| Zero is the smallest Nat

78 lteZero : LTE Z right

93 lteZero : LTE Z right

94+ ||| If n <= m, then n + 1 <= m + 1

79 lteSucc : LTE left right -> LTE (S left) (S right)

95 lteSucc : LTE left right -> LTE (S left) (S right)

97+||| Greater than or equal to

81total GTE : Nat -> Nat -> Type

98total GTE : Nat -> Nat -> Type

82GTE left right = LTE right left

99GTE left right = LTE right left

100

101+||| Strict less than

84total LT : Nat -> Nat -> Type

102total LT : Nat -> Nat -> Type

85LT left right = LTE (S left) right

103LT left right = LTE (S left) right

104

105+||| Strict greater than

87total GT : Nat -> Nat -> Type

106total GT : Nat -> Nat -> Type

88GT left right = LT right left

107GT left right = LT right left

108

109+||| Boolean test than one Nat is less than or equal to another

90total lte : Nat -> Nat -> Bool

110total lte : Nat -> Nat -> Bool

91lte Z right = True

111lte Z right = True

92lte left Z = False

112lte left Z = False

93lte (S left) (S right) = lte left right

113lte (S left) (S right) = lte left right

114

115+||| Boolean test than one Nat is greater than or equal to another

95total gte : Nat -> Nat -> Bool

116total gte : Nat -> Nat -> Bool

96gte left right = lte right left

117gte left right = lte right left

118

119+||| Boolean test than one Nat is strictly less than another

98total lt : Nat -> Nat -> Bool

120total lt : Nat -> Nat -> Bool

99lt left right = lte (S left) right

121lt left right = lte (S left) right

100

122

123+||| Boolean test than one Nat is strictly greater than another

101total gt : Nat -> Nat -> Bool

124total gt : Nat -> Nat -> Bool

102gt left right = lt right left

125gt left right = lt right left

103

126

127+||| Find the least of two natural numbers

104total minimum : Nat -> Nat -> Nat

128total minimum : Nat -> Nat -> Nat

105minimum left right =

129minimum left right =

106 if lte left right then

130 if lte left right then

@@ -108,6 +132,7 @@ minimum left right =

108 else

132 else

109 right

133 right

110

134

135+||| Find the greatest of two natural numbers

111total maximum : Nat -> Nat -> Nat

136total maximum : Nat -> Nat -> Nat

112maximum left right =

137maximum left right =

113 if lte left right then

138 if lte left right then

@@ -148,9 +173,11 @@ instance MinBound Nat where

148instance Cast Integer Nat where

173instance Cast Integer Nat where

149 cast = fromInteger

174 cast = fromInteger

150

175

176+||| A wrapper for Nat that specifies the semigroup and monad instances that use (+)

151record Multiplicative : Type where

177record Multiplicative : Type where

152 getMultiplicative : Nat -> Multiplicative

178 getMultiplicative : Nat -> Multiplicative

153

179

180+||| A wrapper for Nat that specifies the semigroup and monad instances that use (*)

154record Additive : Type where

181record Additive : Type where

155 getAdditive : Nat -> Additive

182 getAdditive : Nat -> Additive

156

183

@@ -210,6 +237,7 @@ instance Cast Nat Int where

210-- Auxilliary notions

237-- Auxilliary notions

211--------------------------------------------------------------------------------

238--------------------------------------------------------------------------------

212

239

240+||| The predecessor of a natural number. `pred Z` is `Z`.

213total pred : Nat -> Nat

241total pred : Nat -> Nat

214pred Z = Z

242pred Z = Z

215pred (S n) = n

243pred (S n) = n

@@ -218,11 +246,13 @@ pred (S n) = n

218-- Fibonacci and factorial

246-- Fibonacci and factorial

219--------------------------------------------------------------------------------

247--------------------------------------------------------------------------------

220

248

249+||| Fibonacci numbers

221total fib : Nat -> Nat

250total fib : Nat -> Nat

222fib Z = Z

251fib Z = Z

223fib (S Z) = S Z

252fib (S Z) = S Z

224fib (S (S n)) = fib (S n) + fib n

253fib (S (S n)) = fib (S n) + fib n

225

254

255+||| Factorial function

226total fact : Nat -> Nat

256total fact : Nat -> Nat

227fact Z = S Z

257fact Z = S Z

228fact (S n) = (S n) * fact n

258fact (S n) = (S n) * fact n

@@ -283,10 +313,13 @@ lcm x y = divNat (x * y) (gcd x y)

283--------------------------------------------------------------------------------

313--------------------------------------------------------------------------------

284

314

285-- Succ

315-- Succ

316+

317+||| S preserves equality

286total eqSucc : (left : Nat) -> (right : Nat) -> (p : left = right) ->

318total eqSucc : (left : Nat) -> (right : Nat) -> (p : left = right) ->

287 S left = S right

319 S left = S right

288eqSucc left _ refl = refl

320eqSucc left _ refl = refl

289

321

322+||| S is injective

290total succInjective : (left : Nat) -> (right : Nat) -> (p : S left = S right) ->

323total succInjective : (left : Nat) -> (right : Nat) -> (p : S left = S right) ->

291 left = right

324 left = right

292succInjective left _ refl = refl

325succInjective left _ refl = refl

libs/prelude/Prelude/Stream.idr+19−4

@@ -6,46 +6,61 @@ import Prelude.Vect

6%access public

7%default total

9+||| An infinite stream

9codata Stream : Type -> Type where

10codata Stream : Type -> Type where

10 (::) : a -> Stream a -> Stream a

11 (::) : a -> Stream a -> Stream a

12instance Functor Stream where

13instance Functor Stream where

13 map f (x::xs) = f x :: map f xs

14 map f (x::xs) = f x :: map f xs

16+||| The first element of an infinite stream

15head : Stream a -> a

17head : Stream a -> a

16head (x::xs) = x

18head (x::xs) = x

20+||| All but the first element

18tail : Stream a -> Stream a

21tail : Stream a -> Stream a

19tail (x::xs) = xs

22tail (x::xs) = xs

24+||| Take precisely n elements from the stream

25+||| @ n how many elements to take

26+||| @ xs the stream

21−take : (n : Nat) -> Stream a -> Vect n a

27+take : (n : Nat) -> (xs : Stream a) -> Vect n a

22take Z _ = []

28take Z _ = []

23take (S n) (x :: xs) = x :: (take n xs)

29take (S n) (x :: xs) = x :: (take n xs)

25%assert_total

31%assert_total

26drop : Nat -> Stream a -> Stream a

32drop : Nat -> Stream a -> Stream a

27−drop Z xs = xs

33+drop Z xs = xs

28drop (S k) (x::xs) = drop k xs

34drop (S k) (x::xs) = drop k xs

36+||| An infinite stream of repetitions of the same thing

30repeat : a -> Stream a

37repeat : a -> Stream a

31repeat x = x :: repeat x

38repeat x = x :: repeat x

40+||| Generate an infinite stream by repeatedly applying a function

41+||| @ f the function to iterate

42+||| @ x the initial value that will be the head of the stream

33−iterate : (a -> a) -> a -> Stream a

43+iterate : (f : a -> a) -> (x : a) -> Stream a

34iterate f x = x :: iterate f (f x)

44iterate f x = x :: iterate f (f x)

46+||| Get the nth element of a stream

36index : Nat -> Stream a -> a

47index : Nat -> Stream a -> a

37−index Z (x::xs) = x

48+index Z (x::xs) = x

38index (S k) (x::xs) = index k xs

49index (S k) (x::xs) = index k xs

51+||| Combine two streams element-wise using a function

40zipWith : (a -> b -> c) -> Stream a -> Stream b -> Stream c

52zipWith : (a -> b -> c) -> Stream a -> Stream b -> Stream c

41zipWith f (x::xs) (y::ys) = f x y :: zipWith f xs ys

53zipWith f (x::xs) (y::ys) = f x y :: zipWith f xs ys

55+||| Create a stream of pairs from two streams

43zip : Stream a -> Stream b -> Stream (a, b)

56zip : Stream a -> Stream b -> Stream (a, b)

44zip = zipWith (\x,y => (x,y))

57zip = zipWith (\x,y => (x,y))

59+||| Create a pair of streams from a stream of pairs

46unzip : Stream (a, b) -> (Stream a, Stream b)

60unzip : Stream (a, b) -> (Stream a, Stream b)

47unzip xs = (map fst xs, map snd xs)

61unzip xs = (map fst xs, map snd xs)

63+||| Return the diagonal elements of a stream of streams

49diag : Stream (Stream a) -> Stream a

64diag : Stream (Stream a) -> Stream a

50diag ((x::xs)::xss) = x :: diag (map tail xss)

65diag ((x::xs)::xss) = x :: diag (map tail xss)

libs/prelude/Prelude/Strings.idr+6−6

@@ -7,30 +7,30 @@ import Prelude.Cast

7import Prelude.Either

8import Prelude.Foldable

10−-- | Appends two strings together.

10+||| Appends two strings together.

11(++) : String -> String -> String

12(++) = prim__concat

14−-- | Returns the first character in the specified string.

14+||| Returns the first character in the specified string.

15partial

16strHead : String -> Char

17strHead = prim__strHead

19−-- | Returns the characters specified after the head of the string.

19+||| Returns the characters specified after the head of the string.

20partial

21strTail : String -> String

22strTail = prim__strTail

24−-- | Adds a character to the from of the specified string.

24+||| Adds a character to the from of the specified string.

25strCons : Char -> String -> String

26strCons = prim__strCons

28−-- | Returns the nth character (starting from 0) of the specified string.

28+||| Returns the nth character (starting from 0) of the specified string.

29partial

30strIndex : String -> Int -> Char

31strIndex = prim__strIndex

33−-- | Reverses the elements within a String.

33+||| Reverses the elements within a String.

34reverse : String -> String

35reverse = prim__strRev

libs/prelude/Prelude/Uninhabited.idr+9−3

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

1module Prelude.Uninhabited

3+||| A canonical proof that some type is empty

3class Uninhabited t where

4class Uninhabited t where

5+ ||| If I have a t, I've had a contradiction

6+ ||| @ t the uninhabited type

4 total uninhabited : t -> _|_

7 total uninhabited : t -> _|_

6instance Uninhabited (Fin Z) where

9instance Uninhabited (Fin Z) where

@@ -10,6 +13,9 @@ instance Uninhabited (Fin Z) where

10instance Uninhabited (Z = S n) where

13instance Uninhabited (Z = S n) where

11 uninhabited refl impossible

14 uninhabited refl impossible

13−-- | Use an absurd assumption to discharge a proof obligation

16+||| Use an absurd assumption to discharge a proof obligation

17+||| @ t some empty type

18+||| @ a the goal type

19+||| @ h the contradictory hypothesis

14−absurd : Uninhabited t => t -> a

20+absurd : Uninhabited t => (h : t) -> a

15−absurd t = FalseElim (uninhabited t)

21+absurd h = FalseElim (uninhabited h)

samples/reflection.idr+25−25

@@ -2,93 +2,93 @@ module ReflectionExamples

3import Language.Reflection

5−-- | The reflected term for (\ x => reverse "bba")

5+||| The reflected term for (\ x => reverse "bba")

6reflectVal : TT

7reflectVal = ?valPrf

9−-- | intEq for the integers 3 and 3

9+||| intEq for the integers 3 and 3

10applyTac1 : Int

11applyTac1 = ?tacPrf1

13−-- | intEq for the integers 3 and 42

13+||| intEq for the integers 3 and 42

14applyTac0 : Int

15applyTac0 = ?tacPrf0

17−-- | intEq for the two arguments

17+||| intEq for the two arguments

18applyTacDyn : Int -> Int -> Int

19applyTacDyn x y = ?tacPrfDyn

21−-- | Restored version for RConstant (I 42)

21+||| Restored version for RConstant (I 42)

22fill : Int

23fill = ?fillPrf

25−-- | The type (TTName, TT) computed from its reflected raw rep.

25+||| The type (TTName, TT) computed from its reflected raw rep.

26envTuple : Type

27envTuple = ?envTuplePrf

29−-- | The type List (TTName, TT) computed from its reflected raw rep.

29+||| The type List (TTName, TT) computed from its reflected raw rep.

30envList : List (TTName, TT)

31envList = ?envListPrf

33−-- | Reflected raw rep. for the type (TTName, TT)

33+||| Reflected raw rep. for the type (TTName, TT)

34tupleType : Raw

35tupleType = RApp (RApp (Var (MN 0 "__Pair"))

36 (Var (NS (UN "TTName") ["Reflection", "Language"])))

37 (Var (NS (UN "TT") ["Reflection", "Language"]))

39−-- | Reflected raw rep for the type List (TTName, TT)

39+||| Reflected raw rep for the type List (TTName, TT)

40mkTuple : Raw

41mkTuple = RApp (RApp (Var (MN 0 "__MkPair"))

42 (Var (NS (UN "TTName") ["Reflection", "Language"])))

43 (Var (NS (UN "TT") ["Reflection", "Language"]))

45−-- | Reflected raw rep for Prelude.List.Nil

45+||| Reflected raw rep for Prelude.List.Nil

46nil : Raw

47nil = (Var (NS (UN "Nil") ["List", "Prelude"]))

49−-- | Reflected raw rep for Prelude.List.::

49+||| Reflected raw rep for Prelude.List.::

50cons : Raw

51cons = (Var (NS (UN "::") ["List", "Prelude"]))

53−-- | 1 if the two arguments are equal, 0 otherwise

53+||| 1 if the two arguments are equal, 0 otherwise

54−-- This function is chosen as simple as possible for

54+||| This function is chosen as simple as possible for

55−-- demo purposes.

55+||| demo purposes.

56intEq : Int -> Int -> Int

57intEq x y = case x == y of

58 True => 1

59 False => 0

61−-- | A tactic script to run intEq on two let-bound or introduced

61+||| A tactic script to run intEq on two let-bound or introduced

62−-- arguments of the current (otherwise empty) proof context

62+||| arguments of the current (otherwise empty) proof context

63firstEq : List (TTName, Binder TT) -> TT -> Tactic

64firstEq ((_, (Let _ y))::(_, (Let _ x))::(_, Let _ f)::Nil) _ = Exact (App (App f x) y)

65firstEq ((y, Lam yt)::(x, Lam xt)::(_, Let _ f)::Nil) _ = Exact (App (App f (P (Bound) x xt)) (P Bound y yt))

66firstEq xs _ = Exact (TConst (I 0))

68−-- | Skip 1 argument of the proof context and return the second one which

68+||| Skip 1 argument of the proof context and return the second one which

69−-- has to be introduced. Used for the tactical dispatch example, which

69+||| has to be introduced. Used for the tactical dispatch example, which

70−-- will push dispatch, as first env agrument.

70+||| will push dispatch, as first env agrument.

71innerTac : List (TTName, Binder TT) -> TT -> Tactic

72innerTac (_::(x, Lam xt)::_) _ = Exact (P Bound x xt)

74−-- | Returns the reflected representation of innerTac

74+||| Returns the reflected representation of innerTac

75innerTacTT : TT

76innerTacTT = ?innerTacTTPrf

78−-- | Dispatch to the reflected rep. of innerTac

78+||| Dispatch to the reflected rep. of innerTac

79dispatch : List (TTName, Binder TT) -> TT -> Tactic

80dispatch xs _ = ApplyTactic (innerTacTT)

82−-- | Call dispatch which will then dispatch to innerTac.

82+||| Call dispatch which will then dispatch to innerTac.

83tacticalDispatch : Int -> Int

84tacticalDispatch = ?tacticalDispatchPrf

86−-- | A tactic to get the representation of its goal

86+||| A tactic to get the representation of its goal

87studyGoalTac : List (TTName, Binder TT) -> TT -> Tactic

88studyGoalTac _ goal = Reflect goal

90−-- | Returns the representation of its goal, TT

90+||| Returns the representation of its goal, TT

91−-- (so this is reflect on the type TT)

91+||| (so this is reflect on the type TT)

92studyGoal : TT

93studyGoal = ?studyGoalPrf

src/Idris/AbsSyntax.hs+53−52

@@ -262,10 +262,10 @@ addCoercion :: Name -> Idris ()

262addCoercion n = do i <- getIState

263 putIState $ i { idris_coercions = nub $ n : idris_coercions i }

264

265−addDocStr :: Name -> String -> Idris ()

265+addDocStr :: Name -> String -> [(Name, String)] -> Idris ()

266−addDocStr n doc

266+addDocStr n doc args

267 = do i <- getIState

268− putIState $ i { idris_docstrings = addDef n doc (idris_docstrings i) }

268+ putIState $ i { idris_docstrings = addDef n (doc, args) (idris_docstrings i) }

269

270addNameHint :: Name -> Name -> Idris ()

271addNameHint ty n

@@ -999,12 +999,12 @@ expandParams dec ps ns infs tm = en tm

999expandParamsD :: Bool -> -- True = RHS only

1000 IState ->

1001 (Name -> Name) -> [(Name, PTerm)] -> [Name] -> PDecl -> PDecl

1002−expandParamsD rhsonly ist dec ps ns (PTy doc syn fc o n ty)

1002+expandParamsD rhsonly ist dec ps ns (PTy doc argdocs syn fc o n ty)

1003 = if n `elem` ns && (not rhsonly)

1004 then -- trace (show (n, expandParams dec ps ns ty)) $

1005− PTy doc syn fc o (dec n) (piBindp expl_param ps (expandParams dec ps ns [] ty))

1005+ PTy doc argdocs syn fc o (dec n) (piBindp expl_param ps (expandParams dec ps ns [] ty))

1006 else --trace (show (n, expandParams dec ps ns ty)) $

1007− PTy doc syn fc o n (expandParams dec ps ns [] ty)

1007+ PTy doc argdocs syn fc o n (expandParams dec ps ns [] ty)

1008expandParamsD rhsonly ist dec ps ns (PPostulate doc syn fc o n ty)

1009 = if n `elem` ns && (not rhsonly)

1010 then -- trace (show (n, expandParams dec ps ns ty)) $

@@ -1050,8 +1050,8 @@ expandParamsD rhsonly ist dec ps ns (PClauses fc opts n cs)

1050 bnames (PDPair _ _ l Placeholder r) = bnames l ++ bnames r

1051 bnames _ = []

1052

1053−expandParamsD rhs ist dec ps ns (PData doc syn fc co pd)

1053+expandParamsD rhs ist dec ps ns (PData doc argDocs syn fc co pd)

1054− = PData doc syn fc co (expandPData pd)

1054+ = PData doc argDocs syn fc co (expandPData pd)

1055 where

1056 -- just do the type decl, leave constructors alone (parameters will be

1057 -- added implicitly)

@@ -1060,10 +1060,10 @@ expandParamsD rhs ist dec ps ns (PData doc syn fc co pd)

1060 then PDatadecl (dec n) (piBind ps (expandParams dec ps ns [] ty))

1061 (map econ cons)

1062 else PDatadecl n (expandParams dec ps ns [] ty) (map econ cons)

1063− econ (doc, n, t, fc, fs)

1063+ econ (doc, argDocs, n, t, fc, fs)

1064− = (doc, dec n, piBindp impl ps (expandParams dec ps ns [] t), fc, fs)

1064+ = (doc, argDocs, dec n, piBindp impl ps (expandParams dec ps ns [] t), fc, fs)

1065−expandParamsD rhs ist dec ps ns (PRecord doc syn fc tn tty cdoc cn cty)

1065+expandParamsD rhs ist dec ps ns (PRecord doc syn fc tn tty cdoc cn cty)

1066− = if tn `elem` ns

1066+ = if tn `elem` ns

1067 then PRecord doc syn fc (dec tn) (piBind ps (expandParams dec ps ns [] tty))

1068 cdoc (dec cn) conty

1069 else PRecord doc syn fc (dec tn) (expandParams dec ps ns [] tty)

@@ -1125,6 +1125,7 @@ getPriority i tm = 1 -- pri tm

1125 pri Placeholder = 1

1126 pri _ = 3

1127

1128+

1128addStatics :: Name -> Term -> PTerm -> Idris ()

1129addStatics :: Name -> Term -> PTerm -> Idris ()

1129addStatics n tm ptm =

1130addStatics n tm ptm =

1130 do let (statics, dynamics) = initStatics tm ptm

1131 do let (statics, dynamics) = initStatics tm ptm

@@ -1158,8 +1159,8 @@ addStatics n tm ptm =

1158 -- if a name appears in a type class or tactic implicit index, it doesn't

1159 -- if a name appears in a type class or tactic implicit index, it doesn't

1159 -- affect its 'uniquely inferrable' from a static status since these are

1160 -- affect its 'uniquely inferrable' from a static status since these are

1160 -- resolved by searching.

1161 -- resolved by searching.

1161− searchArg (Constraint _ _ _) = True

1162+ searchArg (Constraint _ _) = True

1162− searchArg (TacImp _ _ _ _) = True

1163+ searchArg (TacImp _ _ _) = True

1163 searchArg _ = False

1164 searchArg _ = False

1164

1165

1165 staticList sts (Bind n (Pi _) sc) = (n `elem` sts) : staticList sts sc

1166 staticList sts (Bind n (Pi _) sc) = (n `elem` sts) : staticList sts sc

@@ -1186,14 +1187,14 @@ addUsingConstraints syn fc t

1186 -- if all of args in ns, then add it

1187 -- if all of args in ns, then add it

1187 doAdd (UConstraint c args : cs) ns t

1188 doAdd (UConstraint c args : cs) ns t

1188 | all (\n -> elem n ns) args

1189 | all (\n -> elem n ns) args

1189− = PPi (Constraint [] Dynamic "") (sMN 0 "cu")

1190+ = PPi (Constraint [] Dynamic) (sMN 0 "cu")

1190 (mkConst c args) (doAdd cs ns t)

1191 (mkConst c args) (doAdd cs ns t)

1191 | otherwise = doAdd cs ns t

1192 | otherwise = doAdd cs ns t

1192

1193

1193 mkConst c args = PApp fc (PRef fc c)

1194 mkConst c args = PApp fc (PRef fc c)

1194− (map (\n -> PExp 0 [] (PRef fc n) "") args)

1195+ (map (\n -> PExp 0 [] (PRef fc n)) args)

1195

1196

1196− getConstraints (PPi (Constraint _ _ _) _ c sc)

1197+ getConstraints (PPi (Constraint _ _) _ c sc)

1197 = getcapp c ++ getConstraints sc

1198 = getcapp c ++ getConstraints sc

1198 getConstraints (PPi _ _ c sc) = getConstraints sc

1199 getConstraints (PPi _ _ c sc) = getConstraints sc

1199 getConstraints _ = []

1200 getConstraints _ = []

@@ -1203,7 +1204,7 @@ addUsingConstraints syn fc t

1203 return (UConstraint c ns)

1204 return (UConstraint c ns)

1204 getcapp _ = []

1205 getcapp _ = []

1205

1206

1206− getName (PExp _ _ (PRef _ n) _) = return n

1207+ getName (PExp _ _ (PRef _ n)) = return n

1207 getName _ = []

1208 getName _ = []

1208

1209

1209-- Add implicit Pi bindings for any names in the term which appear in an

1210-- Add implicit Pi bindings for any names in the term which appear in an

@@ -1253,34 +1254,34 @@ implicitise syn ignore ist tm = -- trace ("INCOMING " ++ showImp True tm) $

1253 = do (decls, ns) <- get

1254 = do (decls, ns) <- get

1254 let isn = concatMap (namesIn uvars ist) (map getTm as)

1255 let isn = concatMap (namesIn uvars ist) (map getTm as)

1255 put (decls, nub (ns ++ (isn `dropAll` (env ++ map fst (getImps decls)))))

1256 put (decls, nub (ns ++ (isn `dropAll` (env ++ map fst (getImps decls)))))

1256− imps top env (PPi (Imp l _ doc _) n ty sc)

1257+ imps top env (PPi (Imp l _ _) n ty sc)

1257 = do let isn = nub (namesIn uvars ist ty) `dropAll` [n]

1258 = do let isn = nub (namesIn uvars ist ty) `dropAll` [n]

1258 (decls , ns) <- get

1259 (decls , ns) <- get

1259− put (PImp (getPriority ist ty) True l n Placeholder doc : decls,

1260+ put (PImp (getPriority ist ty) True l n Placeholder : decls,

1260 nub (ns ++ (isn `dropAll` (env ++ map fst (getImps decls)))))

1261 nub (ns ++ (isn `dropAll` (env ++ map fst (getImps decls)))))

1261 imps True (n:env) sc

1262 imps True (n:env) sc

1262− imps top env (PPi (Exp l _ doc _) n ty sc)

1263+ imps top env (PPi (Exp l _ _) n ty sc)

1263 = do let isn = nub (namesIn uvars ist ty ++ case sc of

1264 = do let isn = nub (namesIn uvars ist ty ++ case sc of

1264 (PRef _ x) -> namesIn uvars ist sc `dropAll` [n]

1265 (PRef _ x) -> namesIn uvars ist sc `dropAll` [n]

1265 _ -> [])

1266 _ -> [])

1266 (decls, ns) <- get -- ignore decls in HO types

1267 (decls, ns) <- get -- ignore decls in HO types

1267− put (PExp (getPriority ist ty) l Placeholder doc : decls,

1268+ put (PExp (getPriority ist ty) l Placeholder : decls,

1268 nub (ns ++ (isn `dropAll` (env ++ map fst (getImps decls)))))

1269 nub (ns ++ (isn `dropAll` (env ++ map fst (getImps decls)))))

1269 imps True (n:env) sc

1270 imps True (n:env) sc

1270− imps top env (PPi (Constraint l _ doc) n ty sc)

1271+ imps top env (PPi (Constraint l _) n ty sc)

1271 = do let isn = nub (namesIn uvars ist ty ++ case sc of

1272 = do let isn = nub (namesIn uvars ist ty ++ case sc of

1272 (PRef _ x) -> namesIn uvars ist sc `dropAll` [n]

1273 (PRef _ x) -> namesIn uvars ist sc `dropAll` [n]

1273 _ -> [])

1274 _ -> [])

1274 (decls, ns) <- get -- ignore decls in HO types

1275 (decls, ns) <- get -- ignore decls in HO types

1275− put (PConstraint 10 l Placeholder doc : decls,

1276+ put (PConstraint 10 l Placeholder : decls,

1276 nub (ns ++ (isn `dropAll` (env ++ map fst (getImps decls)))))

1277 nub (ns ++ (isn `dropAll` (env ++ map fst (getImps decls)))))

1277 imps True (n:env) sc

1278 imps True (n:env) sc

1278− imps top env (PPi (TacImp l _ scr doc) n ty sc)

1279+ imps top env (PPi (TacImp l _ scr) n ty sc)

1279 = do let isn = nub (namesIn uvars ist ty ++ case sc of

1280 = do let isn = nub (namesIn uvars ist ty ++ case sc of

1280 (PRef _ x) -> namesIn uvars ist sc `dropAll` [n]

1281 (PRef _ x) -> namesIn uvars ist sc `dropAll` [n]

1281 _ -> [])

1282 _ -> [])

1282 (decls, ns) <- get -- ignore decls in HO types

1283 (decls, ns) <- get -- ignore decls in HO types

1283− put (PTacImplicit 10 l n scr Placeholder doc : decls,

1284+ put (PTacImplicit 10 l n scr Placeholder : decls,

1284 nub (ns ++ (isn `dropAll` (env ++ map fst (getImps decls)))))

1285 nub (ns ++ (isn `dropAll` (env ++ map fst (getImps decls)))))

1285 imps True (n:env) sc

1286 imps True (n:env) sc

1286 imps top env (PEq _ l r)

1287 imps top env (PEq _ l r)

@@ -1321,8 +1322,8 @@ implicitise syn ignore ist tm = -- trace ("INCOMING " ++ showImp True tm) $

1321 pibind using [] sc = sc

1322 pibind using [] sc = sc

1322 pibind using (n:ns) sc

1323 pibind using (n:ns) sc

1323 = case lookup n using of

1324 = case lookup n using of

1324− Just ty -> PPi (Imp [] Dynamic "" False) n ty (pibind using ns sc)

1325+ Just ty -> PPi (Imp [] Dynamic False) n ty (pibind using ns sc)

1325− Nothing -> PPi (Imp [] Dynamic "" False) n Placeholder

1326+ Nothing -> PPi (Imp [] Dynamic False) n Placeholder

1326 (pibind using ns sc)

1327 (pibind using ns sc)

1327

1328

1328-- Add implicit arguments in function calls

1329-- Add implicit arguments in function calls

@@ -1438,7 +1439,7 @@ aiFn inpat True ist fc f ds []

1438-- any constructor alts || any allImp ialts))

1439-- any constructor alts || any allImp ialts))

1439 then aiFn inpat False ist fc f ds [] -- use it as a constructor

1440 then aiFn inpat False ist fc f ds [] -- use it as a constructor

1440 else Right $ PPatvar fc f

1441 else Right $ PPatvar fc f

1441− where imp (PExp _ _ _ _) = False

1442+ where imp (PExp _ _ _) = False

1442 imp _ = True

1443 imp _ = True

1443-- allImp [] = False

1444-- allImp [] = False

1444 allImp xs = all imp xs

1445 allImp xs = all imp xs

@@ -1487,30 +1488,30 @@ aiFn inpat expat ist fc f ds as

1487

1488

1489

1489 insertImpl :: [PArg] -> [PArg] -> [PArg]

1490 insertImpl :: [PArg] -> [PArg] -> [PArg]

1490− insertImpl (PExp p l ty _ : ps) (PExp _ _ tm d : given) =

1491+ insertImpl (PExp p l ty : ps) (PExp _ _ tm : given) =

1491− PExp p l tm d : insertImpl ps given

1492+ PExp p l tm : insertImpl ps given

1492− insertImpl (PConstraint p l ty _ : ps) (PConstraint _ _ tm d : given) =

1493+ insertImpl (PConstraint p l ty : ps) (PConstraint _ _ tm : given) =

1493− PConstraint p l tm d : insertImpl ps given

1494+ PConstraint p l tm : insertImpl ps given

1494− insertImpl (PConstraint p l ty d : ps) given =

1495+ insertImpl (PConstraint p l ty : ps) given =

1495− PConstraint p l (PResolveTC fc) d : insertImpl ps given

1496+ PConstraint p l (PResolveTC fc) : insertImpl ps given

1496− insertImpl (PImp p _ l n ty d : ps) given =

1497+ insertImpl (PImp p _ l n ty : ps) given =

1497 case find n given [] of

1498 case find n given [] of

1498− Just (tm, given') -> PImp p False l n tm "" : insertImpl ps given'

1499+ Just (tm, given') -> PImp p False l n tm : insertImpl ps given'

1499− Nothing -> PImp p True l n Placeholder "" : insertImpl ps given

1500+ Nothing -> PImp p True l n Placeholder : insertImpl ps given

1500− insertImpl (PTacImplicit p l n sc' ty d : ps) given =

1501+ insertImpl (PTacImplicit p l n sc' ty : ps) given =

1501 let sc = addImpl ist sc' in

1502 let sc = addImpl ist sc' in

1502 case find n given [] of

1503 case find n given [] of

1503− Just (tm, given') -> PTacImplicit p l n sc tm "" : insertImpl ps given'

1504+ Just (tm, given') -> PTacImplicit p l n sc tm : insertImpl ps given'

1504 Nothing -> if inpat

1505 Nothing -> if inpat

1505− then PTacImplicit p l n sc Placeholder "" : insertImpl ps given

1506+ then PTacImplicit p l n sc Placeholder : insertImpl ps given

1506− else PTacImplicit p l n sc sc "" : insertImpl ps given

1507+ else PTacImplicit p l n sc sc : insertImpl ps given

1507 insertImpl expected [] = []

1508 insertImpl expected [] = []

1508 insertImpl _ given = given

1509 insertImpl _ given = given

1509

1510

1510 find n [] acc = Nothing

1511 find n [] acc = Nothing

1511− find n (PImp _ _ _ n' t _ : gs) acc

1512+ find n (PImp _ _ _ n' t : gs) acc

1512 | n == n' = Just (t, reverse acc ++ gs)

1513 | n == n' = Just (t, reverse acc ++ gs)

1513− find n (PTacImplicit _ _ n' _ t _ : gs) acc

1514+ find n (PTacImplicit _ _ n' _ t : gs) acc

1514 | n == n' = Just (t, reverse acc ++ gs)

1515 | n == n' = Just (t, reverse acc ++ gs)

1515 find n (g : gs) acc = find n gs (g : acc)

1516 find n (g : gs) acc = find n gs (g : acc)

1516

1517

@@ -1540,16 +1541,16 @@ stripLinear i tm = evalState (sl tm) [] where

1540 sl (PApp fc fn args) = do fn' <- sl fn

1541 sl (PApp fc fn args) = do fn' <- sl fn

1541 args' <- mapM slA args

1542 args' <- mapM slA args

1542 return $ PApp fc fn' args'

1543 return $ PApp fc fn' args'

1543− where slA (PImp p m l n t d) = do t' <- sl t

1544+ where slA (PImp p m l n t) = do t' <- sl t

1544− return $ PImp p m l n t' d

1545+ return $ PImp p m l n t'

1545− slA (PExp p l t d) = do t' <- sl t

1546+ slA (PExp p l t) = do t' <- sl t

1546− return $ PExp p l t' d

1547+ return $ PExp p l t'

1547− slA (PConstraint p l t d)

1548+ slA (PConstraint p l t)

1548 = do t' <- sl t

1549 = do t' <- sl t

1549− return $ PConstraint p l t' d

1550+ return $ PConstraint p l t'

1550− slA (PTacImplicit p l n sc t d)

1551+ slA (PTacImplicit p l n sc t)

1551 = do t' <- sl t

1552 = do t' <- sl t

1552− return $ PTacImplicit p l n sc t' d

1553+ return $ PTacImplicit p l n sc t'

1553 sl x = return x

1554 sl x = return x

1554

1555

1555-- Remove functions which aren't applied to anything, which must then

1556-- Remove functions which aren't applied to anything, which must then

src/Idris/AbsSyntaxTree.hs+66−74

@@ -111,7 +111,7 @@ data IState = IState {

111 idris_flags :: Ctxt [FnOpt],

112 idris_callgraph :: Ctxt CGInfo, -- name, args used in each pos

113 idris_calledgraph :: Ctxt [Name],

114− idris_docstrings :: Ctxt String,

114+ idris_docstrings :: Ctxt (String, [(Name, String)]),

115 idris_tyinfodata :: Ctxt TIData,

116 idris_totcheck :: [(FC, Name)], -- names to check totality on

117 idris_defertotcheck :: [(FC, Name)], -- names to check at the end

@@ -381,19 +381,15 @@ deriving instance NFData Static

381-- Mark bindings with their explicitness, and laziness

382data Plicity = Imp { pargopts :: [ArgOpt],

383 pstatic :: Static,

384− pdocstr :: String,

385 pparam :: Bool }

384 pparam :: Bool }

386 | Exp { pargopts :: [ArgOpt],

385 | Exp { pargopts :: [ArgOpt],

387 pstatic :: Static,

386 pstatic :: Static,

388− pdocstr :: String,

389 pparam :: Bool }

387 pparam :: Bool }

390 | Constraint { pargopts :: [ArgOpt],

388 | Constraint { pargopts :: [ArgOpt],

391− pstatic :: Static,

389+ pstatic :: Static }

392− pdocstr :: String }

393 | TacImp { pargopts :: [ArgOpt],

390 | TacImp { pargopts :: [ArgOpt],

394 pstatic :: Static,

391 pstatic :: Static,

395− pscript :: PTerm,

392+ pscript :: PTerm }

396− pdocstr :: String }

397 deriving (Show, Eq)

393 deriving (Show, Eq)

398

394

399plazy :: Plicity -> Bool

395plazy :: Plicity -> Bool

@@ -404,11 +400,11 @@ deriving instance Binary Plicity

404deriving instance NFData Plicity

400deriving instance NFData Plicity

405!-}

401!-}

406

402

407−impl = Imp [Lazy] Dynamic "" False

403+impl = Imp [Lazy] Dynamic False

408−expl = Exp [] Dynamic "" False

404+expl = Exp [] Dynamic False

409−expl_param = Exp [] Dynamic "" True

405+expl_param = Exp [] Dynamic True

410−constraint = Constraint [] Dynamic ""

406+constraint = Constraint [] Dynamic

411−tacimpl t = TacImp [] Dynamic t ""

407+tacimpl t = TacImp [] Dynamic t

412

408

413data FnOpt = Inlinable -- always evaluate when simplifying

409data FnOpt = Inlinable -- always evaluate when simplifying

414 | TotalFn | PartialFn

410 | TotalFn | PartialFn

@@ -454,11 +450,11 @@ data ProvideWhat = ProvTerm -- ^ only allow providing terms

454-- datatypes and typeclasses.

450-- datatypes and typeclasses.

455data PDecl' t

451data PDecl' t

456 = PFix FC Fixity [String] -- ^ Fixity declaration

452 = PFix FC Fixity [String] -- ^ Fixity declaration

457− | PTy String SyntaxInfo FC FnOpts Name t -- ^ Type declaration

453+ | PTy String [(Name, String)] SyntaxInfo FC FnOpts Name t -- ^ Type declaration

458 | PPostulate String SyntaxInfo FC FnOpts Name t -- ^ Postulate

454 | PPostulate String SyntaxInfo FC FnOpts Name t -- ^ Postulate

459 | PClauses FC FnOpts Name [PClause' t] -- ^ Pattern clause

455 | PClauses FC FnOpts Name [PClause' t] -- ^ Pattern clause

460 | PCAF FC Name t -- ^ Top level constant

456 | PCAF FC Name t -- ^ Top level constant

461− | PData String SyntaxInfo FC DataOpts (PData' t) -- ^ Data declaration.

457+ | PData String [(Name, String)] SyntaxInfo FC DataOpts (PData' t) -- ^ Data declaration.

462 | PParams FC [(Name, t)] [PDecl' t] -- ^ Params block

458 | PParams FC [(Name, t)] [PDecl' t] -- ^ Params block

463 | PNamespace String [PDecl' t] -- ^ New namespace

459 | PNamespace String [PDecl' t] -- ^ New namespace

464 | PRecord String SyntaxInfo FC Name t String Name t -- ^ Record declaration

460 | PRecord String SyntaxInfo FC Name t String Name t -- ^ Record declaration

@@ -516,7 +512,7 @@ deriving instance NFData PClause'

516-- | Data declaration

512-- | Data declaration

517data PData' t = PDatadecl { d_name :: Name, -- ^ The name of the datatype

513data PData' t = PDatadecl { d_name :: Name, -- ^ The name of the datatype

518 d_tcon :: t, -- ^ Type constructor

514 d_tcon :: t, -- ^ Type constructor

519− d_cons :: [(String, Name, t, FC, [Name])] -- ^ Constructors

515+ d_cons :: [(String, [(Name, String)], Name, t, FC, [Name])] -- ^ Constructors

520 }

516 }

521 -- ^ Data declaration

517 -- ^ Data declaration

522 | PLaterdecl { d_name :: Name, d_tcon :: t }

518 | PLaterdecl { d_name :: Name, d_tcon :: t }

@@ -538,13 +534,13 @@ type PClause = PClause' PTerm

538

534

539declared :: PDecl -> [Name]

535declared :: PDecl -> [Name]

540declared (PFix _ _ _) = []

536declared (PFix _ _ _) = []

541−declared (PTy _ _ _ _ n t) = [n]

537+declared (PTy _ _ _ _ _ n t) = [n]

542declared (PPostulate _ _ _ _ n t) = [n]

538declared (PPostulate _ _ _ _ n t) = [n]

543declared (PClauses _ _ n _) = [] -- not a declaration

539declared (PClauses _ _ n _) = [] -- not a declaration

544declared (PCAF _ n _) = [n]

540declared (PCAF _ n _) = [n]

545−declared (PData _ _ _ _ (PDatadecl n _ ts)) = n : map fstt ts

541+declared (PData _ _ _ _ _ (PDatadecl n _ ts)) = n : map fstt ts

546− where fstt (_, a, _, _, _) = a

542+ where fstt (_, _, a, _, _, _) = a

547−declared (PData _ _ _ _ (PLaterdecl n _)) = [n]

543+declared (PData _ _ _ _ _ (PLaterdecl n _)) = [n]

548declared (PParams _ _ ds) = concatMap declared ds

544declared (PParams _ _ ds) = concatMap declared ds

549declared (PNamespace _ ds) = concatMap declared ds

545declared (PNamespace _ ds) = concatMap declared ds

550declared (PRecord _ _ _ n _ _ c _) = [n, c]

546declared (PRecord _ _ _ n _ _ c _) = [n, c]

@@ -558,12 +554,12 @@ declared (PDirective _) = []

558-- get the names declared, not counting nested parameter blocks

554-- get the names declared, not counting nested parameter blocks

559tldeclared :: PDecl -> [Name]

555tldeclared :: PDecl -> [Name]

560tldeclared (PFix _ _ _) = []

556tldeclared (PFix _ _ _) = []

561−tldeclared (PTy _ _ _ _ n t) = [n]

557+tldeclared (PTy _ _ _ _ _ n t) = [n]

562tldeclared (PPostulate _ _ _ _ n t) = [n]

558tldeclared (PPostulate _ _ _ _ n t) = [n]

563tldeclared (PClauses _ _ n _) = [] -- not a declaration

559tldeclared (PClauses _ _ n _) = [] -- not a declaration

564tldeclared (PRecord _ _ _ n _ _ c _) = [n, c]

560tldeclared (PRecord _ _ _ n _ _ c _) = [n, c]

565−tldeclared (PData _ _ _ _ (PDatadecl n _ ts)) = n : map fstt ts

561+tldeclared (PData _ _ _ _ _ (PDatadecl n _ ts)) = n : map fstt ts

566− where fstt (_, a, _, _, _) = a

562+ where fstt (_, _, a, _, _, _) = a

567tldeclared (PParams _ _ ds) = []

563tldeclared (PParams _ _ ds) = []

568tldeclared (PMutual _ ds) = concatMap tldeclared ds

564tldeclared (PMutual _ ds) = concatMap tldeclared ds

569tldeclared (PNamespace _ ds) = concatMap tldeclared ds

565tldeclared (PNamespace _ ds) = concatMap tldeclared ds

@@ -573,13 +569,13 @@ tldeclared _ = []

573

569

574defined :: PDecl -> [Name]

570defined :: PDecl -> [Name]

575defined (PFix _ _ _) = []

571defined (PFix _ _ _) = []

576−defined (PTy _ _ _ _ n t) = []

572+defined (PTy _ _ _ _ _ n t) = []

577defined (PPostulate _ _ _ _ n t) = []

573defined (PPostulate _ _ _ _ n t) = []

578defined (PClauses _ _ n _) = [n] -- not a declaration

574defined (PClauses _ _ n _) = [n] -- not a declaration

579defined (PCAF _ n _) = [n]

575defined (PCAF _ n _) = [n]

580−defined (PData _ _ _ _ (PDatadecl n _ ts)) = n : map fstt ts

576+defined (PData _ _ _ _ _ (PDatadecl n _ ts)) = n : map fstt ts

581− where fstt (_, a, _, _, _) = a

577+ where fstt (_, _, a, _, _, _) = a

582−defined (PData _ _ _ _ (PLaterdecl n _)) = []

578+defined (PData _ _ _ _ _ (PLaterdecl n _)) = []

583defined (PParams _ _ ds) = concatMap defined ds

579defined (PParams _ _ ds) = concatMap defined ds

584defined (PNamespace _ ds) = concatMap defined ds

580defined (PNamespace _ ds) = concatMap defined ds

585defined (PRecord _ _ _ n _ _ c _) = [n, c]

581defined (PRecord _ _ _ n _ _ c _) = [n, c]

@@ -766,22 +762,18 @@ type PDo = PDo' PTerm

766data PArg' t = PImp { priority :: Int,

762data PArg' t = PImp { priority :: Int,

767 machine_inf :: Bool, -- true if the machine inferred it

763 machine_inf :: Bool, -- true if the machine inferred it

768 argopts :: [ArgOpt],

764 argopts :: [ArgOpt],

769− pname :: Name, getTm :: t,

765+ pname :: Name, getTm :: t }

770− pargdoc :: String }

771 | PExp { priority :: Int,

766 | PExp { priority :: Int,

772 argopts :: [ArgOpt],

767 argopts :: [ArgOpt],

773− getTm :: t,

768+ getTm :: t }

774− pargdoc :: String }

775 | PConstraint { priority :: Int,

769 | PConstraint { priority :: Int,

776 argopts :: [ArgOpt],

770 argopts :: [ArgOpt],

777− getTm :: t,

771+ getTm :: t }

778− pargdoc :: String }

779 | PTacImplicit { priority :: Int,

772 | PTacImplicit { priority :: Int,

780 argopts :: [ArgOpt],

773 argopts :: [ArgOpt],

781 pname :: Name,

774 pname :: Name,

782 getScript :: t,

775 getScript :: t,

783− getTm :: t,

776+ getTm :: t }

784− pargdoc :: String }

785 deriving (Show, Eq, Functor)

777 deriving (Show, Eq, Functor)

786

778

787data ArgOpt = Lazy | HideDisplay

779data ArgOpt = Lazy | HideDisplay

@@ -791,20 +783,20 @@ lazyarg :: PArg' t -> Bool

791lazyarg tm = Lazy `elem` argopts tm

783lazyarg tm = Lazy `elem` argopts tm

792

784

793instance Sized a => Sized (PArg' a) where

785instance Sized a => Sized (PArg' a) where

794− size (PImp p _ l nm trm _) = 1 + size nm + size trm

786+ size (PImp p _ l nm trm) = 1 + size nm + size trm

795− size (PExp p l trm _) = 1 + size trm

787+ size (PExp p l trm) = 1 + size trm

796− size (PConstraint p l trm _) = 1 + size trm

788+ size (PConstraint p l trm) = 1 + size trm

797− size (PTacImplicit p l nm scr trm _) = 1 + size nm + size scr + size trm

789+ size (PTacImplicit p l nm scr trm) = 1 + size nm + size scr + size trm

798

790

799{-!

791{-!

800deriving instance Binary PArg'

792deriving instance Binary PArg'

801deriving instance NFData PArg'

793deriving instance NFData PArg'

802!-}

794!-}

803

795

804−pimp n t mach = PImp 1 mach [Lazy] n t ""

796+pimp n t mach = PImp 1 mach [Lazy] n t

805−pexp t = PExp 1 [] t ""

797+pexp t = PExp 1 [] t

806−pconst t = PConstraint 1 [] t ""

798+pconst t = PConstraint 1 [] t

807−ptacimp n s t = PTacImplicit 2 [Lazy] n s t ""

799+ptacimp n s t = PTacImplicit 2 [Lazy] n s t

808

800

809type PArg = PArg' PTerm

801type PArg = PArg' PTerm

810

802

@@ -956,9 +948,9 @@ inferTy = sMN 0 "__Infer"

956inferCon = sMN 0 "__infer"

948inferCon = sMN 0 "__infer"

957inferDecl = PDatadecl inferTy

949inferDecl = PDatadecl inferTy

958 PType

950 PType

959− [("", inferCon, PPi impl (sMN 0 "iType") PType (

951+ [("", [], inferCon, PPi impl (sMN 0 "iType") PType (

960− PPi expl (sMN 0 "ival") (PRef bi (sMN 0 "iType"))

952+ PPi expl (sMN 0 "ival") (PRef bi (sMN 0 "iType"))

961− (PRef bi inferTy)), bi, [])]

953+ (PRef bi inferTy)), bi, [])]

962inferOpts = []

954inferOpts = []

963

955

964infTerm t = PApp bi (PRef bi inferCon) [pimp (sMN 0 "iType") Placeholder True, pexp t]

956infTerm t = PApp bi (PRef bi inferCon) [pimp (sMN 0 "iType") Placeholder True, pexp t]

@@ -986,7 +978,7 @@ primNames = [unitTy, unitCon,

986unitTy = sMN 0 "__Unit"

978unitTy = sMN 0 "__Unit"

987unitCon = sMN 0 "__II"

979unitCon = sMN 0 "__II"

988unitDecl = PDatadecl unitTy PType

980unitDecl = PDatadecl unitTy PType

989− [("", unitCon, PRef bi unitTy, bi, [])]

981+ [("", [], unitCon, PRef bi unitTy, bi, [])]

990unitOpts = [DefaultEliminator]

982unitOpts = [DefaultEliminator]

991

983

992falseTy = sMN 0 "__False"

984falseTy = sMN 0 "__False"

@@ -996,12 +988,12 @@ falseOpts = []

996pairTy = sMN 0 "__Pair"

988pairTy = sMN 0 "__Pair"

997pairCon = sMN 0 "__MkPair"

989pairCon = sMN 0 "__MkPair"

998pairDecl = PDatadecl pairTy (piBind [(n "A", PType), (n "B", PType)] PType)

990pairDecl = PDatadecl pairTy (piBind [(n "A", PType), (n "B", PType)] PType)

999− [("", pairCon, PPi impl (n "A") PType (

991+ [("", [], pairCon, PPi impl (n "A") PType (

1000− PPi impl (n "B") PType (

992+ PPi impl (n "B") PType (

1001− PPi expl (n "a") (PRef bi (n "A")) (

993+ PPi expl (n "a") (PRef bi (n "A")) (

1002− PPi expl (n "b") (PRef bi (n "B"))

994+ PPi expl (n "b") (PRef bi (n "B"))

1003− (PApp bi (PRef bi pairTy) [pexp (PRef bi (n "A")),

995+ (PApp bi (PRef bi pairTy) [pexp (PRef bi (n "A")),

1004− pexp (PRef bi (n "B"))])))), bi, [])]

996+ pexp (PRef bi (n "B"))])))), bi, [])]

1005 where n a = sMN 0 a

997 where n a = sMN 0 a

1006pairOpts = []

998pairOpts = []

1007

999

@@ -1010,12 +1002,12 @@ eqCon = sUN "refl"

1010eqDecl = PDatadecl eqTy (piBind [(n "A", PType), (n "B", PType),

1002eqDecl = PDatadecl eqTy (piBind [(n "A", PType), (n "B", PType),

1011 (n "x", PRef bi (n "A")), (n "y", PRef bi (n "B"))]

1003 (n "x", PRef bi (n "A")), (n "y", PRef bi (n "B"))]

1012 PType)

1004 PType)

1013− [("", eqCon, PPi impl (n "A") PType (

1005+ [("", [], eqCon, PPi impl (n "A") PType (

1014− PPi impl (n "x") (PRef bi (n "A"))

1006+ PPi impl (n "x") (PRef bi (n "A"))

1015− (PApp bi (PRef bi eqTy) [pimp (n "A") Placeholder False,

1007+ (PApp bi (PRef bi eqTy) [pimp (n "A") Placeholder False,

1016− pimp (n "B") Placeholder False,

1008+ pimp (n "B") Placeholder False,

1017− pexp (PRef bi (n "x")),

1009+ pexp (PRef bi (n "x")),

1018− pexp (PRef bi (n "x"))])), bi, [])]

1010+ pexp (PRef bi (n "x"))])), bi, [])]

1019 where n a = sMN 0 a

1011 where n a = sMN 0 a

1020eqOpts = []

1012eqOpts = []

1021

1013

@@ -1023,8 +1015,8 @@ elimName = sUN "__Elim"

1023elimMethElimTy = sUN "__elimTy"

1015elimMethElimTy = sUN "__elimTy"

1024elimMethElim = sUN "elim"

1016elimMethElim = sUN "elim"

1025elimDecl = PClass "Type class for eliminators" defaultSyntax bi [] elimName [(sUN "scrutineeType", PType)]

1017elimDecl = PClass "Type class for eliminators" defaultSyntax bi [] elimName [(sUN "scrutineeType", PType)]

1026− [PTy "" defaultSyntax bi [TotalFn] elimMethElimTy PType,

1018+ [PTy "" [] defaultSyntax bi [TotalFn] elimMethElimTy PType,

1027− PTy "" defaultSyntax bi [TotalFn] elimMethElim (PRef bi elimMethElimTy)]

1019+ PTy "" [] defaultSyntax bi [TotalFn] elimMethElim (PRef bi elimMethElimTy)]

1028

1020

1029-- Defined in builtins.idr

1021-- Defined in builtins.idr

1030sigmaTy = sUN "Exists"

1022sigmaTy = sUN "Exists"

@@ -1108,7 +1100,7 @@ pprintPTerm impl bnd = prettySe 10 bnd

1108 text "let" <+> bindingOf n False <+> text "=" </>

1100 text "let" <+> bindingOf n False <+> text "=" </>

1109 prettySe 10 bnd v <+> text "in" </>

1101 prettySe 10 bnd v <+> text "in" </>

1110 prettySe 10 ((n, False):bnd) sc

1102 prettySe 10 ((n, False):bnd) sc

1111− prettySe p bnd (PPi (Exp l s _ _) n ty sc)

1103+ prettySe p bnd (PPi (Exp l s _) n ty sc)

1112 | n `elem` allNamesIn sc || impl =

1104 | n `elem` allNamesIn sc || impl =

1113 let open = if Lazy `elem` l then text "|" <> lparen else lparen in

1105 let open = if Lazy `elem` l then text "|" <> lparen else lparen in

1114 bracket p 2 . group $

1106 bracket p 2 . group $

@@ -1122,7 +1114,7 @@ pprintPTerm impl bnd = prettySe 10 bnd

1122 case s of

1114 case s of

1123 Static -> text "[static]" <> space

1115 Static -> text "[static]" <> space

1124 _ -> empty

1116 _ -> empty

1125− prettySe p bnd (PPi (Imp l s _ _) n ty sc)

1117+ prettySe p bnd (PPi (Imp l s _) n ty sc)

1126 | impl =

1118 | impl =

1127 let open = if Lazy `elem` l then text "|" <> lbrace else lbrace in

1119 let open = if Lazy `elem` l then text "|" <> lbrace else lbrace in

1128 bracket p 2 $

1120 bracket p 2 $

@@ -1134,10 +1126,10 @@ pprintPTerm impl bnd = prettySe 10 bnd

1134 case s of

1126 case s of

1135 Static -> text "[static]" <> space

1127 Static -> text "[static]" <> space

1136 _ -> empty

1128 _ -> empty

1137− prettySe p bnd (PPi (Constraint _ _ _) n ty sc) =

1129+ prettySe p bnd (PPi (Constraint _ _) n ty sc) =

1138 bracket p 2 $

1130 bracket p 2 $

1139 prettySe 10 bnd ty <+> text "=>" </> prettySe 10 ((n, True):bnd) sc

1131 prettySe 10 bnd ty <+> text "=>" </> prettySe 10 ((n, True):bnd) sc

1140− prettySe p bnd (PPi (TacImp _ _ s _) n ty sc) =

1132+ prettySe p bnd (PPi (TacImp _ _ s) n ty sc) =

1141 bracket p 2 $

1133 bracket p 2 $

1142 lbrace <> text "tacimp" <+> pretty n <+> colon <+> prettySe 10 bnd ty <>

1134 lbrace <> text "tacimp" <+> pretty n <+> colon <+> prettySe 10 bnd ty <>

1143 rbrace <+> text "->" </> prettySe 10 ((n, True):bnd) sc

1135 rbrace <+> text "->" </> prettySe 10 ((n, True):bnd) sc

@@ -1254,10 +1246,10 @@ pprintPTerm impl bnd = prettySe 10 bnd

1254

1246

1255 prettySe p bnd _ = text "test"

1247 prettySe p bnd _ = text "test"

1256

1248

1257− prettyArgS bnd (PImp _ _ _ n tm _) = prettyArgSi bnd (n, tm)

1249+ prettyArgS bnd (PImp _ _ _ n tm) = prettyArgSi bnd (n, tm)

1258− prettyArgS bnd (PExp _ _ tm _) = prettyArgSe bnd tm

1250+ prettyArgS bnd (PExp _ _ tm) = prettyArgSe bnd tm

1259− prettyArgS bnd (PConstraint _ _ tm _) = prettyArgSc bnd tm

1251+ prettyArgS bnd (PConstraint _ _ tm) = prettyArgSc bnd tm

1260− prettyArgS bnd (PTacImplicit _ _ n _ tm _) = prettyArgSti bnd (n, tm)

1252+ prettyArgS bnd (PTacImplicit _ _ n _ tm) = prettyArgSti bnd (n, tm)

1261

1253

1262 prettyArgSe bnd arg = prettySe 0 bnd arg

1254 prettyArgSe bnd arg = prettySe 0 bnd arg

1263 prettyArgSi bnd (n, val) = lbrace <> pretty n <+> text "=" <+> prettySe 10 bnd val <> rbrace

1255 prettyArgSi bnd (n, val) = lbrace <> pretty n <+> text "=" <+> prettySe 10 bnd val <> rbrace

@@ -1353,16 +1345,16 @@ showCImp impl (PWith _ n l ws r w)

1353showDImp :: Bool -> PData -> Doc OutputAnnotation

1345showDImp :: Bool -> PData -> Doc OutputAnnotation

1354showDImp impl (PDatadecl n ty cons)

1346showDImp impl (PDatadecl n ty cons)

1355 = text "data" <+> text (show n) <+> colon <+> prettyImp impl ty <+> text "where" <$>

1347 = text "data" <+> text (show n) <+> colon <+> prettyImp impl ty <+> text "where" <$>

1356− (indent 2 $ vsep (map (\ (_, n, t, _, _) -> pipe <+> prettyName False [] n <+> colon <+> prettyImp impl t) cons))

1348+ (indent 2 $ vsep (map (\ (_, _, n, t, _, _) -> pipe <+> prettyName False [] n <+> colon <+> prettyImp impl t) cons))

1357

1349

1358showDecls :: Bool -> [PDecl] -> Doc OutputAnnotation

1350showDecls :: Bool -> [PDecl] -> Doc OutputAnnotation

1359showDecls i ds = vsep (map (showDeclImp i) ds)

1351showDecls i ds = vsep (map (showDeclImp i) ds)

1360

1352

1361showDeclImp _ (PFix _ f ops) = text (show f) <+> cat (punctuate (text ",") (map text ops))

1353showDeclImp _ (PFix _ f ops) = text (show f) <+> cat (punctuate (text ",") (map text ops))

1362−showDeclImp i (PTy _ _ _ _ n t) = text "tydecl" <+> text (showCG n) <+> colon <+> prettyImp i t

1354+showDeclImp i (PTy _ _ _ _ _ n t) = text "tydecl" <+> text (showCG n) <+> colon <+> prettyImp i t

1363showDeclImp i (PClauses _ _ n cs) = text "pat" <+> text (showCG n) <+> text "\t" <+>

1355showDeclImp i (PClauses _ _ n cs) = text "pat" <+> text (showCG n) <+> text "\t" <+>

1364 indent 2 (vsep (map (showCImp i) cs))

1356 indent 2 (vsep (map (showCImp i) cs))

1365−showDeclImp _ (PData _ _ _ _ d) = showDImp True d

1357+showDeclImp _ (PData _ _ _ _ _ d) = showDImp True d

1366showDeclImp i (PParams _ ns ps) = text "params" <+> braces (text (show ns) <> line <> showDecls i ps <> line)

1358showDeclImp i (PParams _ ns ps) = text "params" <+> braces (text (show ns) <> line <> showDecls i ps <> line)

1367showDeclImp i (PNamespace n ps) = text "namespace" <+> text n <> braces (line <> showDecls i ps <> line)

1359showDeclImp i (PNamespace n ps) = text "namespace" <+> text n <> braces (line <> showDecls i ps <> line)

1368showDeclImp _ (PSyntax _ syn) = text "syntax" <+> text (show syn)

1360showDeclImp _ (PSyntax _ syn) = text "syntax" <+> text (show syn)

@@ -1378,17 +1370,17 @@ instance Show (Doc OutputAnnotation) where

1378

1370

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

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

1380getImps [] = []

1372getImps [] = []

1381−getImps (PImp _ _ _ n tm _ : xs) = (n, tm) : getImps xs

1373+getImps (PImp _ _ _ n tm : xs) = (n, tm) : getImps xs

1382getImps (_ : xs) = getImps xs

1374getImps (_ : xs) = getImps xs

1383

1375

1384getExps :: [PArg] -> [PTerm]

1376getExps :: [PArg] -> [PTerm]

1385getExps [] = []

1377getExps [] = []

1386−getExps (PExp _ _ tm _ : xs) = tm : getExps xs

1378+getExps (PExp _ _ tm : xs) = tm : getExps xs

1387getExps (_ : xs) = getExps xs

1379getExps (_ : xs) = getExps xs

1388

1380

1389getConsts :: [PArg] -> [PTerm]

1381getConsts :: [PArg] -> [PTerm]

1390getConsts [] = []

1382getConsts [] = []

1391−getConsts (PConstraint _ _ tm _ : xs) = tm : getConsts xs

1383+getConsts (PConstraint _ _ tm : xs) = tm : getConsts xs

1392getConsts (_ : xs) = getConsts xs

1384getConsts (_ : xs) = getConsts xs

1393

1385

1394getAll :: [PArg] -> [PTerm]

1386getAll :: [PArg] -> [PTerm]

src/Idris/CaseSplit.hs+4−4

@@ -150,7 +150,7 @@ mergePat ist (PApp _ _ args) (PApp fc f args') t

150 where mergeArg x (y, t)

151 = do tm' <- mergePat ist (getTm x) (getTm y) t

152 case x of

153− (PImp _ _ _ _ _ _) ->

153+ (PImp _ _ _ _ _) ->

154 return (y { machine_inf = machine_inf x,

155 getTm = tm' })

156 _ -> return (y { getTm = tm' })

@@ -318,14 +318,14 @@ getClause l fn fp = do ty <- getInternalApp fp l

318 let ap = mkApp ist ty []

319 return (show fn ++ " " ++ ap ++

320 "= ?" ++ show fn ++ "_rhs")

321− where mkApp i (PPi (Exp _ _ _ False) (MN _ _) ty sc) used

321+ where mkApp i (PPi (Exp _ _ False) (MN _ _) ty sc) used

322 = let n = getNameFrom i used ty in

323 show n ++ " " ++ mkApp i sc (n : used)

324− mkApp i (PPi (Exp _ _ _ False) (UN n) ty sc) used

324+ mkApp i (PPi (Exp _ _ False) (UN n) ty sc) used

325 | thead n == '_'

326 = let n = getNameFrom i used ty in

327 show n ++ " " ++ mkApp i sc (n : used)

328− mkApp i (PPi (Exp _ _ _ False) n _ sc) used

328+ mkApp i (PPi (Exp _ _ False) n _ sc) used

329 = show n ++ " " ++ mkApp i sc (n : used)

330 mkApp i (PPi _ _ _ sc) used = mkApp i sc used

331 mkApp i _ _ = ""

src/Idris/Coverage.hs+2−2

@@ -56,7 +56,7 @@ genClauses fc n xs given

56 -- there may be more case splitting that the idris_implicits record

57 -- suggests)

58 let parg = case lookupCtxt n (idris_implicits i) of

59− (p : _) -> p ++ repeat (PExp 0 [] Placeholder "")

59+ (p : _) -> p ++ repeat (PExp 0 [] Placeholder)

60 _ -> repeat (pexp Placeholder)

61 let tryclauses = mkClauses parg all_args

62 logLvl 2 $ show (length tryclauses) ++ " initially to check"

@@ -187,7 +187,7 @@ genAll i args

187 _ -> [p]

188 ops fc n arg o = return Placeholder

189

190− getExpTm (PImp _ True _ _ _ _) = Placeholder -- machine inferred, no point!

190+ getExpTm (PImp _ True _ _ _) = Placeholder -- machine inferred, no point!

191 getExpTm t = getTm t

192

193 -- put it back to its original form

src/Idris/DeepSeq.hs+21−20

@@ -57,14 +57,14 @@ instance NFData ArgOpt where

57 rnf _ = ()

59instance NFData Plicity where

60− rnf (Imp x1 x2 x3 x4)

60+ rnf (Imp x1 x2 x3)

61− = rnf x1 `seq` rnf x2 `seq` rnf x3 `seq` rnf x4 `seq` ()

61+ = rnf x1 `seq` rnf x2 `seq` rnf x3 `seq` ()

62− rnf (Exp x1 x2 x3 x4)

62+ rnf (Exp x1 x2 x3)

63− = rnf x1 `seq` rnf x2 `seq` rnf x3 `seq` rnf x4 `seq` ()

63+ = rnf x1 `seq` rnf x2 `seq` rnf x3 `seq` ()

64− rnf (Constraint x1 x2 x3)

64+ rnf (Constraint x1 x2)

65+ = rnf x1 `seq` rnf x2 `seq` ()

66+ rnf (TacImp x1 x2 x3)

65 = rnf x1 `seq` rnf x2 `seq` rnf x3 `seq` ()

67 = rnf x1 `seq` rnf x2 `seq` rnf x3 `seq` ()

66− rnf (TacImp x1 x2 x3 x4)

67− = rnf x1 `seq` rnf x2 `seq` rnf x3 `seq` rnf x4 `seq` ()

69instance NFData FnOpt where

70 rnf Inlinable = ()

@@ -84,18 +84,20 @@ instance NFData DataOpt where

85instance (NFData t) => NFData (PDecl' t) where

86 rnf (PFix x1 x2 x3) = rnf x1 `seq` rnf x2 `seq` rnf x3 `seq` ()

87− rnf (PTy x1 x2 x3 x4 x5 x6)

87+ rnf (PTy x1 x2 x3 x4 x5 x6 x7)

88 = rnf x1 `seq`

89+ rnf x2 `seq`

89− rnf x2 `seq` rnf x3 `seq` rnf x4 `seq` rnf x5 `seq` rnf x6 `seq` ()

90+ rnf x3 `seq` rnf x4 `seq` rnf x5 `seq` rnf x6 `seq` rnf x7 `seq` ()

90 rnf (PPostulate x1 x2 x3 x4 x5 x6)

91 rnf (PPostulate x1 x2 x3 x4 x5 x6)

91 = rnf x1 `seq`

92 = rnf x1 `seq`

92 rnf x2 `seq` rnf x3 `seq` rnf x4 `seq` rnf x5 `seq` rnf x6 `seq` ()

93 rnf x2 `seq` rnf x3 `seq` rnf x4 `seq` rnf x5 `seq` rnf x6 `seq` ()

93 rnf (PClauses x1 x2 x3 x4)

94 rnf (PClauses x1 x2 x3 x4)

94 = rnf x1 `seq` rnf x2 `seq` rnf x3 `seq` rnf x4 `seq` ()

95 = rnf x1 `seq` rnf x2 `seq` rnf x3 `seq` rnf x4 `seq` ()

95 rnf (PCAF x1 x2 x3) = rnf x1 `seq` rnf x2 `seq` rnf x3 `seq` ()

96 rnf (PCAF x1 x2 x3) = rnf x1 `seq` rnf x2 `seq` rnf x3 `seq` ()

96− rnf (PData x1 x2 x3 x4 x5)

97+ rnf (PData x1 x2 x3 x4 x5 x6)

97 = rnf x1 `seq`

98 = rnf x1 `seq`

99+ rnf x2 `seq`

98− rnf x2 `seq` rnf x3 `seq` rnf x4 `seq` rnf x5 `seq` ()

100+ rnf x3 `seq` rnf x4 `seq` rnf x5 `seq` rnf x6 `seq` ()

99 rnf (PParams x1 x2 x3) = rnf x1 `seq` rnf x2 `seq` rnf x3 `seq` ()

101 rnf (PParams x1 x2 x3) = rnf x1 `seq` rnf x2 `seq` rnf x3 `seq` ()

100 rnf (PNamespace x1 x2) = rnf x1 `seq` rnf x2 `seq` ()

102 rnf (PNamespace x1 x2) = rnf x1 `seq` rnf x2 `seq` ()

101 rnf (PRecord x1 x2 x3 x4 x5 x6 x7 x8)

103 rnf (PRecord x1 x2 x3 x4 x5 x6 x7 x8)

@@ -230,16 +232,15 @@ instance (NFData t) => NFData (PDo' t) where

230 rnf (DoLetP x1 x2 x3) = rnf x1 `seq` rnf x2 `seq` rnf x3 `seq` ()

232 rnf (DoLetP x1 x2 x3) = rnf x1 `seq` rnf x2 `seq` rnf x3 `seq` ()

231

233

232instance (NFData t) => NFData (PArg' t) where

234instance (NFData t) => NFData (PArg' t) where

233− rnf (PImp x1 x2 x3 x4 x5 x6)

235+ rnf (PImp x1 x2 x3 x4 x5)

234− = rnf x1 `seq`

235− rnf x2 `seq` rnf x3 `seq` rnf x4 `seq` rnf x5 `seq` rnf x6 `seq` ()

236+ = rnf x1 `seq` rnf x2 `seq` rnf x3 `seq` rnf x4 `seq` rnf x5 `seq` ()

236− rnf (PExp x1 x2 x3 x4)

237+ rnf (PExp x1 x2 x3)

237− = rnf x1 `seq` rnf x2 `seq` rnf x3 `seq` rnf x4 `seq` ()

238+ = rnf x1 `seq` rnf x2 `seq` rnf x3 `seq` ()

238− rnf (PConstraint x1 x2 x3 x4)

239+ rnf (PConstraint x1 x2 x3)

239− = rnf x1 `seq` rnf x2 `seq` rnf x3 `seq` rnf x4 `seq` ()

240+ = rnf x1 `seq` rnf x2 `seq` rnf x3 `seq` ()

240− rnf (PTacImplicit x1 x2 x3 x4 x5 x6)

241+ rnf (PTacImplicit x1 x2 x3 x4 x5)

241 = rnf x1 `seq`

242 = rnf x1 `seq`

242− rnf x2 `seq` rnf x3 `seq` rnf x4 `seq` rnf x5 `seq` rnf x6 `seq` ()

243+ rnf x2 `seq` rnf x3 `seq` rnf x4 `seq` rnf x5 `seq` ()

243

244

244instance NFData ClassInfo where

245instance NFData ClassInfo where

245 rnf (CI x1 x2 x3 x4 x5 x6)

246 rnf (CI x1 x2 x3 x4 x5 x6)

src/Idris/Delaborate.hs+15−10

@@ -56,19 +56,24 @@ delabTy' ist imps tm fullname mvs = de [] imps tm

56 _ -> PRef un n

57 de env _ (Bind n (Lam ty) sc)

58 = PLam n (de env [] ty) (de ((n,n):env) [] sc)

59− de env (PImp _ _ _ _ _ _:is) (Bind n (Pi ty) sc)

59+ de env ((PImp { argopts = opts }):is) (Bind n (Pi ty) sc)

60− = PPi impl n (de env [] ty) (de ((n,n):env) is sc)

60+ = PPi (Imp opts Dynamic False) n (de env [] ty) (de ((n,n):env) is sc)

61− de env (PConstraint _ _ _ _:is) (Bind n (Pi ty) sc)

61+ de env (PConstraint _ _ _:is) (Bind n (Pi ty) sc)

62 = PPi constraint n (de env [] ty) (de ((n,n):env) is sc)

63− de env (PTacImplicit _ _ _ tac _ _:is) (Bind n (Pi ty) sc)

63+ de env (PTacImplicit _ _ _ tac _:is) (Bind n (Pi ty) sc)

64 = PPi (tacimpl tac) n (de env [] ty) (de ((n,n):env) is sc)

65+ de env (plic:is) (Bind n (Pi ty) sc)

66+ = PPi (Exp (argopts plic) Dynamic False)

67+ n

68+ (de env [] ty)

69+ (de ((n,n):env) is sc)

65− de env _ (Bind n (Pi ty) sc)

70+ de env [] (Bind n (Pi ty) sc)

66 = PPi expl n (de env [] ty) (de ((n,n):env) [] sc)

71 = PPi expl n (de env [] ty) (de ((n,n):env) [] sc)

67 de env _ (Bind n (Let ty val) sc)

72 de env _ (Bind n (Let ty val) sc)

68 = PLet n (de env [] ty) (de env [] val) (de ((n,n):env) [] sc)

73 = PLet n (de env [] ty) (de env [] val) (de ((n,n):env) [] sc)

69 de env _ (Bind n (Hole ty) sc) = de ((n, sUN "[__]"):env) [] sc

74 de env _ (Bind n (Hole ty) sc) = de ((n, sUN "[__]"):env) [] sc

70 de env _ (Bind n (Guess ty val) sc) = de ((n, sUN "[__]"):env) [] sc

75 de env _ (Bind n (Guess ty val) sc) = de ((n, sUN "[__]"):env) [] sc

71− de env _ (Bind n _ sc) = de ((n,n):env) [] sc

76+ de env plic (Bind n bb sc) = de ((n,n):env) [] sc

72 de env _ (Constant i) = PConstant i

77 de env _ (Constant i) = PConstant i

73 de env _ Erased = Placeholder

78 de env _ Erased = Placeholder

74 de env _ Impossible = Placeholder

79 de env _ Impossible = Placeholder

@@ -112,10 +117,10 @@ delabTy' ist imps tm fullname mvs = de [] imps tm

112 = PApp un (PRef un n) (zipWith imp (imps ++ repeat (pexp undefined)) args)

117 = PApp un (PRef un n) (zipWith imp (imps ++ repeat (pexp undefined)) args)

113 | otherwise = PApp un (PRef un n) (map pexp args)

118 | otherwise = PApp un (PRef un n) (map pexp args)

114

119

115− imp (PImp p m l n _ d) arg = PImp p m l n arg d

120+ imp (PImp p m l n _) arg = PImp p m l n arg

116− imp (PExp p l _ d) arg = PExp p l arg d

121+ imp (PExp p l _) arg = PExp p l arg

117− imp (PConstraint p l _ d) arg = PConstraint p l arg d

122+ imp (PConstraint p l _) arg = PConstraint p l arg

118− imp (PTacImplicit p l n sc _ d) arg = PTacImplicit p l n sc arg d

123+ imp (PTacImplicit p l n sc _) arg = PTacImplicit p l n sc arg

119

124

120-- | How far to indent sub-errors

125-- | How far to indent sub-errors

121errorIndent :: Int

126errorIndent :: Int

src/Idris/Docs.hs+33−21

@@ -14,15 +14,17 @@ import Data.List

14-- TODO: Only include names with public/abstract accessibility

16data FunDoc = FD Name String

17− [(Name, PTerm, Plicity)] -- args: name, ty, plicity

17+ [(Name, PTerm, Plicity, Maybe String)] -- args: name, ty, implicit, docs

18 PTerm -- function type

19 (Maybe Fixity)

20+ deriving Show

21data Docs = FunDoc FunDoc

22data Docs = FunDoc FunDoc

22 | DataDoc FunDoc -- type constructor docs

23 | DataDoc FunDoc -- type constructor docs

23 [FunDoc] -- data constructor docs

24 [FunDoc] -- data constructor docs

24 | ClassDoc Name String -- class docs

25 | ClassDoc Name String -- class docs

25 [FunDoc] -- method docs

26 [FunDoc] -- method docs

27+ deriving Show

27showDoc "" = empty

29showDoc "" = empty

28showDoc x = text " -- " <> text x

30showDoc x = text " -- " <> text x

@@ -31,23 +33,32 @@ pprintFD :: Bool -> FunDoc -> Doc OutputAnnotation

31pprintFD imp (FD n doc args ty f)

33pprintFD imp (FD n doc args ty f)

32 = nest 4 (prettyName imp [] n <+> colon <+> prettyImp imp ty <$> showDoc doc <$>

34 = nest 4 (prettyName imp [] n <+> colon <+> prettyImp imp ty <$> showDoc doc <$>

33 maybe empty (\f -> text (show f) <> line) f <>

35 maybe empty (\f -> text (show f) <> line) f <>

34− let argshow = mapMaybe showArg args in

36+ let argshow = showArgs args [] in

35 if not (null argshow)

37 if not (null argshow)

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

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

37 else empty)

39 else empty)

39− where showArg (n, ty, arg@(Exp {}))

41+ where showArgs ((n, ty, Exp {}, d):args) bnd

40− = Just $ bindingOf n False <+> colon <+> prettyImp imp ty <>

42+ = bindingOf n False <+> colon <+>

43+ pprintPTerm imp bnd ty <>

41− showDoc (pdocstr arg) <> line

44+ showDoc (maybe "" id d) <> line

45+ :

46+ showArgs args ((n, False):bnd)

42− showArg (n, ty, arg@(Constraint {}))

47+ showArgs ((n, ty, Constraint {}, d):args) bnd

43− = Just $ text "Class constraint" <+>

48+ = text "Class constraint" <+>

44− prettyImp imp ty <> showDoc (pdocstr arg) <> line

49+ pprintPTerm imp bnd ty <> showDoc (maybe "" id d) <> line

45− showArg (n, ty, arg@(Imp {}))

50+ :

51+ showArgs args ((n, True):bnd)

52+ showArgs ((n, ty, Imp {}, d):args) bnd

46 | not (null doc)

53 | not (null doc)

47− = Just $ text "(implicit)" <+>

54+ = text "(implicit)" <+>

48− bindingOf n True <+> colon <+> prettyImp imp ty

55+ bindingOf n True <+> colon <+>

56+ pprintPTerm imp bnd ty <>

49− <> showDoc (pdocstr arg) <> line

57+ showDoc (maybe "" id d) <> line

50− showArg (n, _, _) = Nothing

58+ :

59+ showArgs args ((n, True):bnd)

60+ showArgs ((n, _, _, _):args) bnd = showArgs args ((n, True):bnd)

61+ showArgs [] _ = []

@@ -81,7 +92,7 @@ docClass :: Name -> ClassInfo -> Idris Docs

81docClass n ci

92docClass n ci

82 = do i <- getIState

93 = do i <- getIState

83 let docstr = case lookupCtxt n (idris_docstrings i) of

94 let docstr = case lookupCtxt n (idris_docstrings i) of

84− [str] -> str

95+ [str] -> fst str

85 _ -> ""

96 _ -> ""

86 mdocs <- mapM docFun (map fst (class_methods ci))

97 mdocs <- mapM docFun (map fst (class_methods ci))

87 return (ClassDoc n docstr mdocs)

98 return (ClassDoc n docstr mdocs)

@@ -89,11 +100,11 @@ docClass n ci

89docFun :: Name -> Idris FunDoc

100docFun :: Name -> Idris FunDoc

90docFun n

101docFun n

91 = do i <- getIState

102 = do i <- getIState

92− let docstr = case lookupCtxt n (idris_docstrings i) of

103+ let (docstr, argDocs) = case lookupCtxt n (idris_docstrings i) of

93− [str] -> str

104+ [d] -> d

94− _ -> ""

105+ _ -> ("", [])

95 let ty = delabTy i n

106 let ty = delabTy i n

96− let args = getPArgNames ty

107+ let args = getPArgNames ty argDocs

97 let infixes = idris_infixes i

108 let infixes = idris_infixes i

98 let fixdecls = filter (\(Fix _ x) -> x == funName n) infixes

109 let fixdecls = filter (\(Fix _ x) -> x == funName n) infixes

99 let f = case fixdecls of

110 let f = case fixdecls of

@@ -105,6 +116,7 @@ docFun n

105 funName (UN n) = str n

116 funName (UN n) = str n

106 funName (NS n _) = funName n

117 funName (NS n _) = funName n

107

118

108−getPArgNames :: PTerm -> [(Name, PTerm, Plicity)]

119+getPArgNames :: PTerm -> [(Name, String)] -> [(Name, PTerm, Plicity, Maybe String)]

109−getPArgNames (PPi plicity name ty body) = ((name, ty, plicity) : getPArgNames body)

120+getPArgNames (PPi plicity name ty body) ds =

121+ (name, ty, plicity, lookup name ds) : getPArgNames body ds

110−getPArgNames _ = []

122+getPArgNames _ _ = []

src/Idris/ElabDecls.hs+86−71

@@ -63,15 +63,15 @@ checkAddDef add toplvl fc ((n, (i, top, t)) : ns)

63-- return (n, (i, top, t'))) ns

65-- | Elaborate a top-level type declaration - for example, "foo : Int -> Int".

66−elabType :: ElabInfo -> SyntaxInfo -> String ->

66+elabType :: ElabInfo -> SyntaxInfo -> String -> [(Name, String)] ->

67 FC -> FnOpts -> Name -> PTerm -> Idris Type

68elabType = elabType' False

70elabType' :: Bool -> -- normalise it

71− ElabInfo -> SyntaxInfo -> String ->

71+ ElabInfo -> SyntaxInfo -> String -> [(Name, String)] ->

72 FC -> FnOpts -> Name -> PTerm -> Idris Type

73−elabType' norm info syn doc fc opts n ty' = {- let ty' = piBind (params info) ty_in

73+elabType' norm info syn doc argDocs fc opts n ty' = {- let ty' = piBind (params info) ty_in

74− n = liftname info n_in in -}

74+ n = liftname info n_in in -}

75 do checkUndefined fc n

76 ctxt <- getContext

77 i <- getIState

@@ -122,7 +122,8 @@ elabType' norm info syn doc fc opts n ty' = {- let ty' = piBind (params info) ty

122 let ds' = map (\(n, (i, top, t)) -> (n, (i, top, t, True))) ds

123 addDeferred ds'

124 setFlags n opts'

125+ checkDocs fc argDocs ty

125− addDocStr n doc

126+ addDocStr n doc argDocs

126 addIBC (IBCDoc n)

127 addIBC (IBCDoc n)

127 addIBC (IBCFlags n opts')

128 addIBC (IBCFlags n opts')

128 when (Implicit `elem` opts) $ do addCoercion n

129 when (Implicit `elem` opts) $ do addCoercion n

@@ -167,13 +168,13 @@ elabType' norm info syn doc fc opts n ty' = {- let ty' = piBind (params info) ty

167 , ns2 == map txt ["Maybe", "Prelude"]

168 , ns2 == map txt ["Maybe", "Prelude"]

168 , ns3 == map txt ["List", "Prelude"]

169 , ns3 == map txt ["List", "Prelude"]

169 , ns4 == map txt ["Errors","Reflection","Language"] = True

170 , ns4 == map txt ["Errors","Reflection","Language"] = True

170− tyIsHandler _ = False

171+ tyIsHandler _ = False

171

172

173

173elabPostulate :: ElabInfo -> SyntaxInfo -> String ->

174elabPostulate :: ElabInfo -> SyntaxInfo -> String ->

174 FC -> FnOpts -> Name -> PTerm -> Idris ()

175 FC -> FnOpts -> Name -> PTerm -> Idris ()

175elabPostulate info syn doc fc opts n ty

176elabPostulate info syn doc fc opts n ty

176− = do elabType info syn doc fc opts n ty

177+ = do elabType info syn doc [] fc opts n ty

177 -- make sure it's collapsible, so it is never needed at run time

178 -- make sure it's collapsible, so it is never needed at run time

178 -- start by getting the elaborated type

179 -- start by getting the elaborated type

179 ctxt <- getContext

180 ctxt <- getContext

@@ -194,8 +195,8 @@ elabPostulate info syn doc fc opts n ty

194 -- remove it from the deferred definitions list

195 -- remove it from the deferred definitions list

195 solveDeferred n

196 solveDeferred n

196

197

197−elabData :: ElabInfo -> SyntaxInfo -> String -> FC -> DataOpts -> PData -> Idris ()

198+elabData :: ElabInfo -> SyntaxInfo -> String -> [(Name, String)] -> FC -> DataOpts -> PData -> Idris ()

198−elabData info syn doc fc opts (PLaterdecl n t_in)

199+elabData info syn doc argDocs fc opts (PLaterdecl n t_in)

199 = do let codata = Codata `elem` opts

200 = do let codata = Codata `elem` opts

200 iLOG (show (fc, doc))

201 iLOG (show (fc, doc))

201 checkUndefined fc n

202 checkUndefined fc n

@@ -213,7 +214,7 @@ elabData info syn doc fc opts (PLaterdecl n t_in)

213 logLvl 2 $ "---> " ++ show cty

214 logLvl 2 $ "---> " ++ show cty

214 updateContext (addTyDecl n (TCon 0 0) cty) -- temporary, to check cons

215 updateContext (addTyDecl n (TCon 0 0) cty) -- temporary, to check cons

215

216

216−elabData info syn doc fc opts (PDatadecl n t_in dcons)

217+elabData info syn doc argDocs fc opts (PDatadecl n t_in dcons)

217 = do let codata = Codata `elem` opts

218 = do let codata = Codata `elem` opts

218 iLOG (show fc)

219 iLOG (show fc)

219 undef <- isUndefined fc n

220 undef <- isUndefined fc n

@@ -241,12 +242,13 @@ elabData info syn doc fc opts (PDatadecl n t_in dcons)

241 let as = map (const Nothing) (getArgTys cty)

242 let as = map (const Nothing) (getArgTys cty)

242 let params = findParams (map snd cons)

243 let params = findParams (map snd cons)

243 logLvl 2 $ "Parameters : " ++ show params

244 logLvl 2 $ "Parameters : " ++ show params

244− putIState (i { idris_datatypes =

245+ putIState (i { idris_datatypes =

245 addDef n (TI (map fst cons) codata opts params)

246 addDef n (TI (map fst cons) codata opts params)

246 (idris_datatypes i) })

247 (idris_datatypes i) })

247 addIBC (IBCDef n)

248 addIBC (IBCDef n)

248 addIBC (IBCData n)

249 addIBC (IBCData n)

250+ checkDocs fc argDocs t_in

249− addDocStr n doc

251+ addDocStr n doc argDocs

250 addIBC (IBCDoc n)

252 addIBC (IBCDoc n)

251 let metainf = DataMI params

253 let metainf = DataMI params

252 addIBC (IBCMetaInformation n metainf)

254 addIBC (IBCMetaInformation n metainf)

@@ -258,10 +260,10 @@ elabData info syn doc fc opts (PDatadecl n t_in dcons)

258 if DefaultEliminator `elem` opts then evalStateT (elabEliminator params n t dcons info) Map.empty

260 if DefaultEliminator `elem` opts then evalStateT (elabEliminator params n t dcons info) Map.empty

259 else return ()

261 else return ()

260 where

262 where

261− checkDefinedAs fc n t ctxt

263+ checkDefinedAs fc n t ctxt

262 = case lookupDef n ctxt of

264 = case lookupDef n ctxt of

263 [] -> return ()

265 [] -> return ()

264− [TyDecl _ ty] ->

266+ [TyDecl _ ty] ->

265 case converts ctxt [] t ty of

267 case converts ctxt [] t ty of

266 OK () -> return ()

268 OK () -> return ()

267 _ -> tclift $ tfail (At fc (AlreadyDefined n))

269 _ -> tclift $ tfail (At fc (AlreadyDefined n))

@@ -319,7 +321,8 @@ elabData info syn doc fc opts (PDatadecl n t_in dcons)

319type EliminatorState = StateT (Map.Map String Int) Idris

321type EliminatorState = StateT (Map.Map String Int) Idris

320

322

321-- TODO: Use uniqueName for generating names, rewrite everything to use idris_implicits instead of manual splitting, generally just rewrite

323-- TODO: Use uniqueName for generating names, rewrite everything to use idris_implicits instead of manual splitting, generally just rewrite

322−elabEliminator :: [Int] -> Name -> PTerm -> [(String, Name, PTerm, FC, [Name])] ->

324+elabEliminator :: [Int] -> Name -> PTerm ->

325+ [(String, [(Name, String)], Name, PTerm, FC, [Name])] ->

323 ElabInfo -> EliminatorState ()

326 ElabInfo -> EliminatorState ()

324elabEliminator paramPos n ty cons info = do

327elabEliminator paramPos n ty cons info = do

325 elimLog $ "Elaborating eliminator"

328 elimLog $ "Elaborating eliminator"

@@ -328,15 +331,15 @@ elabEliminator paramPos n ty cons info = do

328 generalParams <- namePis False pms

331 generalParams <- namePis False pms

329 motiveIdxs <- namePis False idxs

332 motiveIdxs <- namePis False idxs

330 let motive = mkMotive n paramPos generalParams motiveIdxs

333 let motive = mkMotive n paramPos generalParams motiveIdxs

331− consTerms <- mapM (\(c@(_,cnm,_,_,_)) -> do

334+ consTerms <- mapM (\(c@(_, _, cnm, _, _, _)) -> do

332− name <- freshName $ "elim_" ++ simpleName cnm

335+ name <- freshName $ "elim_" ++ simpleName cnm

333− consTerm <- extractConsTerm c generalParams

336+ consTerm <- extractConsTerm c generalParams

334− return (name, expl, consTerm)) cons

337+ return (name, expl, consTerm)) cons

335 scrutineeIdxs <- namePis False idxs

338 scrutineeIdxs <- namePis False idxs

336 let motiveConstr = [(motiveName, expl, motive)]

339 let motiveConstr = [(motiveName, expl, motive)]

337 let scrutinee = (scrutineeName, expl, applyCons n (interlievePos paramPos generalParams scrutineeIdxs 0))

340 let scrutinee = (scrutineeName, expl, applyCons n (interlievePos paramPos generalParams scrutineeIdxs 0))

338 let eliminatorTy = piConstr (generalParams ++ motiveConstr ++ consTerms ++ scrutineeIdxs ++ [scrutinee]) (applyMotive (map (\(n,_,_) -> PRef elimFC n) scrutineeIdxs) (PRef elimFC scrutineeName))

341 let eliminatorTy = piConstr (generalParams ++ motiveConstr ++ consTerms ++ scrutineeIdxs ++ [scrutinee]) (applyMotive (map (\(n,_,_) -> PRef elimFC n) scrutineeIdxs) (PRef elimFC scrutineeName))

339− let eliminatorTyDecl = PTy (show n) defaultSyntax elimFC [TotalFn] elimDeclName eliminatorTy

342+ let eliminatorTyDecl = PTy (show n) [] defaultSyntax elimFC [TotalFn] elimDeclName eliminatorTy

340 let clauseConsElimArgs = map getPiName consTerms

343 let clauseConsElimArgs = map getPiName consTerms

341 let clauseGeneralArgs' = map getPiName generalParams ++ [motiveName] ++ clauseConsElimArgs

344 let clauseGeneralArgs' = map getPiName generalParams ++ [motiveName] ++ clauseConsElimArgs

342 let clauseGeneralArgs = map (\arg -> pexp (PRef elimFC arg)) clauseGeneralArgs'

345 let clauseGeneralArgs = map (\arg -> pexp (PRef elimFC arg)) clauseGeneralArgs'

@@ -500,8 +503,8 @@ elabEliminator paramPos n ty cons info = do

500 in return $ filter (\(n,_,_) -> not (n `elem` oldParams))implargs

503 in return $ filter (\(n,_,_) -> not (n `elem` oldParams))implargs

501 _ -> return implargs

504 _ -> return implargs

502

505

503− extractConsTerm :: (String, Name, PTerm, FC, [Name]) -> [(Name, Plicity, PTerm)] -> EliminatorState PTerm

506+ extractConsTerm :: (String, [(Name, String)], Name, PTerm, FC, [Name]) -> [(Name, Plicity, PTerm)] -> EliminatorState PTerm

504− extractConsTerm (doc, cnm, ty, fc, fs) generalParameters = do

507+ extractConsTerm (doc, argDocs, cnm, ty, fc, fs) generalParameters = do

505 let cons' = replaceParams paramPos generalParameters ty

508 let cons' = replaceParams paramPos generalParameters ty

506 let (args, resTy) = splitPi cons'

509 let (args, resTy) = splitPi cons'

507 implidxs <- implicitIndexes (doc, cnm, ty, fc, fs)

510 implidxs <- implicitIndexes (doc, cnm, ty, fc, fs)

@@ -536,8 +539,8 @@ elabEliminator paramPos n ty cons info = do

536 convertImplPi (PImp {getTm = t, pname = n}) = Just (n, expl, t)

539 convertImplPi (PImp {getTm = t, pname = n}) = Just (n, expl, t)

537 convertImplPi _ = Nothing

540 convertImplPi _ = Nothing

538

541

539− generateEliminatorClauses :: (String, Name, PTerm, FC, [Name]) -> Name -> [PArg] -> [(Name, Plicity, PTerm)] -> EliminatorState PClause

542+ generateEliminatorClauses :: (String, [(Name, String)], Name, PTerm, FC, [Name]) -> Name -> [PArg] -> [(Name, Plicity, PTerm)] -> EliminatorState PClause

540− generateEliminatorClauses (doc, cnm, ty, fc, fs) cnsElim generalArgs generalParameters = do

543+ generateEliminatorClauses (doc, _, cnm, ty, fc, fs) cnsElim generalArgs generalParameters = do

541 let cons' = replaceParams paramPos generalParameters ty

544 let cons' = replaceParams paramPos generalParameters ty

542 let (args, resTy) = splitPi cons'

545 let (args, resTy) = splitPi cons'

543 i <- State.lift getIState

546 i <- State.lift getIState

@@ -558,7 +561,7 @@ elabEliminator paramPos n ty cons info = do

558

561

559elabPrims :: Idris ()

562elabPrims :: Idris ()

560elabPrims = do mapM_ (elabDecl EAll toplevel)

563elabPrims = do mapM_ (elabDecl EAll toplevel)

561− (map (\(opt, decl) -> PData "" defaultSyntax (fileFC "builtin") opt decl)

564+ (map (\(opt, decl) -> PData "" [] defaultSyntax (fileFC "builtin") opt decl)

562 (zip

565 (zip

563 [inferOpts, unitOpts, falseOpts, pairOpts, eqOpts]

566 [inferOpts, unitOpts, falseOpts, pairOpts, eqOpts]

564 [inferDecl, unitDecl, falseDecl, pairDecl, eqDecl]))

567 [inferDecl, unitDecl, falseDecl, pairDecl, eqDecl]))

@@ -662,7 +665,7 @@ elabProvider info syn fc what n ty tm

662 Provide tm

665 Provide tm

663 | what `elem` [ProvTerm, ProvAny] ->

666 | what `elem` [ProvTerm, ProvAny] ->

664 do -- Finally add a top-level definition of the provided term

667 do -- Finally add a top-level definition of the provided term

665− elabType info syn "" fc [] n ty

668+ elabType info syn "" [] fc [] n ty

666 elabClauses info fc [] n [PClause fc n (PApp fc (PRef fc n) []) [] (delab i tm) []]

669 elabClauses info fc [] n [PClause fc n (PApp fc (PRef fc n) []) [] (delab i tm) []]

667 logLvl 1 $ "Elaborated provider " ++ show n ++ " as: " ++ show tm

670 logLvl 1 $ "Elaborated provider " ++ show n ++ " as: " ++ show tm

668 | otherwise ->

671 | otherwise ->

@@ -724,7 +727,7 @@ elabTransform info fc safe lhs_in rhs_in

724elabRecord :: ElabInfo -> SyntaxInfo -> String -> FC -> Name ->

727elabRecord :: ElabInfo -> SyntaxInfo -> String -> FC -> Name ->

725 PTerm -> String -> Name -> PTerm -> Idris ()

728 PTerm -> String -> Name -> PTerm -> Idris ()

726elabRecord info syn doc fc tyn ty cdoc cn cty

729elabRecord info syn doc fc tyn ty cdoc cn cty

727− = do elabData info syn doc fc [] (PDatadecl tyn ty [(cdoc, cn, cty, fc, [])])

730+ = do elabData info syn doc [] fc [] (PDatadecl tyn ty [(cdoc, [], cn, cty, fc, [])])

728 cty' <- implicit syn cn cty

731 cty' <- implicit syn cn cty

729 i <- getIState

732 i <- getIState

730 cty <- case lookupTy cn (tt_ctxt i) of

733 cty <- case lookupTy cn (tt_ctxt i) of

@@ -747,7 +750,7 @@ elabRecord info syn doc fc tyn ty cdoc cn cty

747 where

750 where

748-- syn = syn_in { syn_namespace = show (nsroot tyn) : syn_namespace syn_in }

751-- syn = syn_in { syn_namespace = show (nsroot tyn) : syn_namespace syn_in }

749

752

750− isNonImp (PExp _ _ _ _, a) = Just a

753+ isNonImp (PExp _ _ _, a) = Just a

751 isNonImp _ = Nothing

754 isNonImp _ = Nothing

752

755

753 tryElabDecl info (fn, ty, val)

756 tryElabDecl info (fn, ty, val)

@@ -759,15 +762,15 @@ elabRecord info syn doc fc tyn ty cdoc cn cty

759 show fn ++ " (" ++ show ty ++ ")"

762 show fn ++ " (" ++ show ty ++ ")"

760 putIState i)

763 putIState i)

761

764

762− getImplB k (PPi (Imp l s _ _) n Placeholder sc)

765+ getImplB k (PPi (Imp l s _) n Placeholder sc)

763 = getImplB k sc

766 = getImplB k sc

764− getImplB k (PPi (Imp l s d p) n ty sc)

767+ getImplB k (PPi (Imp l s p) n ty sc)

765− = getImplB (\x -> k (PPi (Imp l s d p) n ty x)) sc

768+ = getImplB (\x -> k (PPi (Imp l s p) n ty x)) sc

766 getImplB k (PPi _ n ty sc)

769 getImplB k (PPi _ n ty sc)

767 = getImplB k sc

770 = getImplB k sc

768 getImplB k _ = k

771 getImplB k _ = k

769

772

770− renameBs (PImp _ _ _ _ _ _ : ps) (PPi p n ty s)

773+ renameBs (PImp _ _ _ _ _ : ps) (PPi p n ty s)

771 = PPi p (mkImp n) ty (renameBs ps (substMatch n (PRef fc (mkImp n)) s))

774 = PPi p (mkImp n) ty (renameBs ps (substMatch n (PRef fc (mkImp n)) s))

772 renameBs (_:ps) (PPi p n ty s) = PPi p n ty (renameBs ps s)

775 renameBs (_:ps) (PPi p n ty s) = PPi p n ty (renameBs ps s)

773 renameBs _ t = t

776 renameBs _ t = t

@@ -794,7 +797,7 @@ elabRecord info syn doc fc tyn ty cdoc cn cty

794

797

795 mkProj recty substs cimp ((pn_in, pty), pos)

798 mkProj recty substs cimp ((pn_in, pty), pos)

796 = do let pn = expandNS syn pn_in

799 = do let pn = expandNS syn pn_in

797− let pfnTy = PTy "" defaultSyntax fc [] pn

800+ let pfnTy = PTy "" [] defaultSyntax fc [] pn

798 (PPi expl rec recty

801 (PPi expl rec recty

799 (substMatches substs pty))

802 (substMatches substs pty))

800 let pls = repeat Placeholder

803 let pls = repeat Placeholder

@@ -815,7 +818,7 @@ elabRecord info syn doc fc tyn ty cdoc cn cty

815 let valname = sMN 0 "updateval"

818 let valname = sMN 0 "updateval"

816 let pt = k (PPi expl pn pty

819 let pt = k (PPi expl pn pty

817 (PPi expl rec recty recty))

820 (PPi expl rec recty recty))

818− let pfnTy = PTy "" defaultSyntax fc [] setname pt

821+ let pfnTy = PTy "" [] defaultSyntax fc [] setname pt

819 let pls = map (\x -> PRef fc (sMN x "field")) [0..num-1]

822 let pls = map (\x -> PRef fc (sMN x "field")) [0..num-1]

820 let lhsArgs = pls

823 let lhsArgs = pls

821 let rhsArgs = take pos pls ++ (PRef fc valname) :

824 let rhsArgs = take pos pls ++ (PRef fc valname) :

@@ -831,8 +834,8 @@ elabRecord info syn doc fc tyn ty cdoc cn cty

831 return (pn, pfnTy, PClauses fc [] setname [pclause])

834 return (pn, pfnTy, PClauses fc [] setname [pclause])

832

835

833elabCon :: ElabInfo -> SyntaxInfo -> Name -> Bool ->

836elabCon :: ElabInfo -> SyntaxInfo -> Name -> Bool ->

834− (String, Name, PTerm, FC, [Name]) -> Idris (Name, Type)

837+ (String, [(Name, String)], Name, PTerm, FC, [Name]) -> Idris (Name, Type)

835−elabCon info syn tn codata (doc, n, t_in, fc, forcenames)

838+elabCon info syn tn codata (doc, argDocs, n, t_in, fc, forcenames)

836 = do checkUndefined fc n

839 = do checkUndefined fc n

837 ctxt <- getContext

840 ctxt <- getContext

838 i <- getIState

841 i <- getIState

@@ -853,7 +856,8 @@ elabCon info syn tn codata (doc, n, t_in, fc, forcenames)

853 tyIs cty'

856 tyIs cty'

854 logLvl 2 $ "---> " ++ show n ++ " : " ++ show cty'

857 logLvl 2 $ "---> " ++ show n ++ " : " ++ show cty'

855 addIBC (IBCDef n)

858 addIBC (IBCDef n)

859+ checkDocs fc argDocs t_in

856− addDocStr n doc

860+ addDocStr n doc argDocs

857 addIBC (IBCDoc n)

861 addIBC (IBCDoc n)

858 let fs = map (getNamePos 0 t) forcenames

862 let fs = map (getNamePos 0 t) forcenames

859 -- FIXME: 'forcenames' is an almighty hack! Need a better way of

863 -- FIXME: 'forcenames' is an almighty hack! Need a better way of

@@ -1158,7 +1162,7 @@ elabPE info fc caller r =

1158 (map (\ (lhs, rhs) ->

1162 (map (\ (lhs, rhs) ->

1159 (showTmImpls lhs ++ " = " ++

1163 (showTmImpls lhs ++ " = " ++

1160 showTmImpls rhs)) pats)

1164 showTmImpls rhs)) pats)

1161− elabType info defaultSyntax "" fc opts newnm specTy

1165+ elabType info defaultSyntax "" [] fc opts newnm specTy

1162 let def = map (\ (lhs, rhs) -> PClause fc newnm lhs [] rhs []) pats

1166 let def = map (\ (lhs, rhs) -> PClause fc newnm lhs [] rhs []) pats

1163 elabClauses info fc opts newnm def

1167 elabClauses info fc opts newnm def

1164 logLvl 1 $ "Specialised " ++ show newnm)

1168 logLvl 1 $ "Specialised " ++ show newnm)

@@ -1276,7 +1280,7 @@ checkPossible info fc tcgen fname lhs_in

1276 ((P _ x _, _), (P _ y _, _)) -> x == y

1280 ((P _ x _, _), (P _ y _, _)) -> x == y

1277 _ -> False

1281 _ -> False

1278

1282

1279−getFixedInType i env (PExp _ _ _ _ : is) (Bind n (Pi t) sc)

1283+getFixedInType i env (PExp _ _ _ : is) (Bind n (Pi t) sc)

1280 = getFixedInType i (n : env) is (instantiate (P Bound n t) sc)

1284 = getFixedInType i (n : env) is (instantiate (P Bound n t) sc)

1281getFixedInType i env (_ : is) (Bind n (Pi t) sc)

1285getFixedInType i env (_ : is) (Bind n (Pi t) sc)

1282 = getFixedInType i (n : env) is (instantiate (P Bound n t) sc)

1286 = getFixedInType i (n : env) is (instantiate (P Bound n t) sc)

@@ -1500,7 +1504,7 @@ elabClause info opts (cnum, PClause fc fname lhs_in withs rhs_in whereblock)

1500-- = NS (UN ('#':show x)) [show cnum, show fname]

1504-- = NS (UN ('#':show x)) [show cnum, show fname]

1501

1505

1502 sepBlocks bs = sepBlocks' [] bs where

1506 sepBlocks bs = sepBlocks' [] bs where

1503− sepBlocks' ns (d@(PTy _ _ _ _ n t) : bs)

1507+ sepBlocks' ns (d@(PTy _ _ _ _ _ n t) : bs)

1504 = let (bf, af) = sepBlocks' (n : ns) bs in

1508 = let (bf, af) = sepBlocks' (n : ns) bs in

1505 (d : bf, af)

1509 (d : bf, af)

1506 sepBlocks' ns (d@(PClauses _ _ n _) : bs)

1510 sepBlocks' ns (d@(PClauses _ _ n _) : bs)

@@ -1744,10 +1748,10 @@ elabClass info syn doc fc constraints tn ps ds

1744 let cty = impbind ps $ conbind constraints

1748 let cty = impbind ps $ conbind constraints

1745 $ pibind (map (\ (n, ty) -> (nsroot n, ty)) methods)

1749 $ pibind (map (\ (n, ty) -> (nsroot n, ty)) methods)

1746 constraint

1750 constraint

1747− let cons = [("", cn, cty, fc, [])]

1751+ let cons = [("", [], cn, cty, fc, [])]

1748 let ddecl = PDatadecl tn tty cons

1752 let ddecl = PDatadecl tn tty cons

1749 logLvl 5 $ "Class data " ++ show (showDImp True ddecl)

1753 logLvl 5 $ "Class data " ++ show (showDImp True ddecl)

1750− elabData info (syn { no_imp = no_imp syn ++ mnames }) doc fc [] ddecl

1754+ elabData info (syn { no_imp = no_imp syn ++ mnames }) doc [] fc [] ddecl

1751 -- for each constraint, build a top level function to chase it

1755 -- for each constraint, build a top level function to chase it

1752 logLvl 5 $ "Building functions"

1756 logLvl 5 $ "Building functions"

1753 let usyn = syn { using = map (\ (x,y) -> UImplicit x y) ps

1757 let usyn = syn { using = map (\ (x,y) -> UImplicit x y) ps

@@ -1785,8 +1789,8 @@ elabClass info syn doc fc constraints tn ps ds

1785 conbind (ty : ns) x = PPi constraint (sMN 0 "class") ty (conbind ns x)

1789 conbind (ty : ns) x = PPi constraint (sMN 0 "class") ty (conbind ns x)

1786 conbind [] x = x

1790 conbind [] x = x

1787

1791

1788− getMName (PTy _ _ _ _ n _) = nsroot n

1792+ getMName (PTy _ _ _ _ _ n _) = nsroot n

1789− tdecl allmeths (PTy doc syn _ o n t)

1793+ tdecl allmeths (PTy doc _ syn _ o n t)

1790 = do t' <- implicit' syn allmeths n t

1794 = do t' <- implicit' syn allmeths n t

1791 logLvl 5 $ "Method " ++ show n ++ " : " ++ showTmImpls t'

1795 logLvl 5 $ "Method " ++ show n ++ " : " ++ showTmImpls t'

1792 return ( (n, (toExp (map fst ps) Exp t')),

1796 return ( (n, (toExp (map fst ps) Exp t')),

@@ -1799,7 +1803,7 @@ elabClass info syn doc fc constraints tn ps ds

1799 case lookup n mtys of

1803 case lookup n mtys of

1800 Just (syn, o, ty) -> do let ty' = insertConstraint c ty

1804 Just (syn, o, ty) -> do let ty' = insertConstraint c ty

1801 let ds = map (decorateid defaultdec)

1805 let ds = map (decorateid defaultdec)

1802− [PTy "" syn fc [] n ty',

1806+ [PTy "" [] syn fc [] n ty',

1803 PClauses fc (o ++ opts) n cs]

1807 PClauses fc (o ++ opts) n cs]

1804 iLOG (show ds)

1808 iLOG (show ds)

1805 return (n, ((defaultdec n, ds!!1), ds))

1809 return (n, ((defaultdec n, ds!!1), ds))

@@ -1809,7 +1813,7 @@ elabClass info syn doc fc constraints tn ps ds

1809 defaultdec (UN n) = sUN ("default#" ++ str n)

1813 defaultdec (UN n) = sUN ("default#" ++ str n)

1810 defaultdec (NS n ns) = NS (defaultdec n) ns

1814 defaultdec (NS n ns) = NS (defaultdec n) ns

1811

1815

1812− tydecl (PTy _ _ _ _ _ _) = True

1816+ tydecl (PTy _ _ _ _ _ _ _) = True

1813 tydecl _ = False

1817 tydecl _ = False

1814 instdecl (PInstance _ _ _ _ _ _ _ _) = True

1818 instdecl (PInstance _ _ _ _ _ _ _ _) = True

1815 instdecl _ = False

1819 instdecl _ = False

@@ -1837,7 +1841,7 @@ elabClass info syn doc fc constraints tn ps ds

1837 addInstance False conn' cfn

1841 addInstance False conn' cfn

1838 addIBC (IBCInstance False conn' cfn)

1842 addIBC (IBCInstance False conn' cfn)

1839-- iputStrLn ("Added " ++ show (conn, cfn, ty))

1843-- iputStrLn ("Added " ++ show (conn, cfn, ty))

1840− return [PTy "" syn fc [] cfn ty,

1844+ return [PTy "" [] syn fc [] cfn ty,

1841 PClauses fc [Dictionary] cfn [PClause fc cfn lhs [] rhs []]]

1845 PClauses fc [Dictionary] cfn [PClause fc cfn lhs [] rhs []]]

1842

1846

1843 -- Generate a top level function which looks up a method in a given

1847 -- Generate a top level function which looks up a method in a given

@@ -1853,12 +1857,12 @@ elabClass info syn doc fc constraints tn ps ds

1853 iLOG (showTmImpls ty)

1857 iLOG (showTmImpls ty)

1854 iLOG (show (m, ty', capp, margs))

1858 iLOG (show (m, ty', capp, margs))

1855 iLOG (showTmImpls lhs ++ " = " ++ showTmImpls rhs)

1859 iLOG (showTmImpls lhs ++ " = " ++ showTmImpls rhs)

1856− return [PTy doc syn fc o m ty',

1860+ return [PTy doc [] syn fc o m ty',

1857 PClauses fc [Inlinable] m [PClause fc m lhs [] rhs []]]

1861 PClauses fc [Inlinable] m [PClause fc m lhs [] rhs []]]

1858

1862

1859− getMArgs (PPi (Imp _ _ _ _) n ty sc) = IA : getMArgs sc

1863+ getMArgs (PPi (Imp _ _ _) n ty sc) = IA : getMArgs sc

1860− getMArgs (PPi (Exp _ _ _ _) n ty sc) = EA : getMArgs sc

1864+ getMArgs (PPi (Exp _ _ _) n ty sc) = EA : getMArgs sc

1861− getMArgs (PPi (Constraint _ _ _) n ty sc) = CA : getMArgs sc

1865+ getMArgs (PPi (Constraint _ _) n ty sc) = CA : getMArgs sc

1862 getMArgs _ = []

1866 getMArgs _ = []

1863

1867

1864 getMeth (m:ms) (a:as) x | x == a = PRef fc m

1868 getMeth (m:ms) (a:as) x | x == a = PRef fc m

@@ -1874,14 +1878,14 @@ elabClass info syn doc fc constraints tn ps ds

1874 rhsArgs (CA : xs) ns = pconst (PResolveTC fc) : rhsArgs xs ns

1878 rhsArgs (CA : xs) ns = pconst (PResolveTC fc) : rhsArgs xs ns

1875 rhsArgs [] _ = []

1879 rhsArgs [] _ = []

1876

1880

1877− insertConstraint c (PPi p@(Imp _ _ _ _) n ty sc)

1881+ insertConstraint c (PPi p@(Imp _ _ _) n ty sc)

1878 = PPi p n ty (insertConstraint c sc)

1882 = PPi p n ty (insertConstraint c sc)

1879 insertConstraint c sc = PPi constraint (sMN 0 "class") c sc

1883 insertConstraint c sc = PPi constraint (sMN 0 "class") c sc

1880

1884

1881 -- make arguments explicit and don't bind class parameters

1885 -- make arguments explicit and don't bind class parameters

1882− toExp ns e (PPi (Imp l s _ p) n ty sc)

1886+ toExp ns e (PPi (Imp l s p) n ty sc)

1883 | n `elem` ns = toExp ns e sc

1887 | n `elem` ns = toExp ns e sc

1884− | otherwise = PPi (e l s "" p) n ty (toExp ns e sc)

1888+ | otherwise = PPi (e l s p) n ty (toExp ns e sc)

1885 toExp ns e (PPi p n ty sc) = PPi p n ty (toExp ns e sc)

1889 toExp ns e (PPi p n ty sc) = PPi p n ty (toExp ns e sc)

1886 toExp ns e sc = sc

1890 toExp ns e sc = sc

1887

1891

@@ -1901,7 +1905,7 @@ elabInstance info syn what fc cs n ps t expn ds = do

1901 let constraint = PApp fc (PRef fc n) (map pexp ps)

1905 let constraint = PApp fc (PRef fc n) (map pexp ps)

1902 let iname = mkiname n ps expn

1906 let iname = mkiname n ps expn

1903 when (what /= EDefns) $ do

1907 when (what /= EDefns) $ do

1904− nty <- elabType' True info syn "" fc [] iname t

1908+ nty <- elabType' True info syn "" [] fc [] iname t

1905 -- if the instance type matches any of the instances we have already,

1909 -- if the instance type matches any of the instances we have already,

1906 -- and it's not a named instance, then it's overlapping, so report an error

1910 -- and it's not a named instance, then it's overlapping, so report an error

1907 case expn of

1911 case expn of

@@ -2009,17 +2013,17 @@ elabInstance info syn what fc cs n ps t expn ds = do

2009

2013

2010 mkMethApp (n, _, _, ty)

2014 mkMethApp (n, _, _, ty)

2011 = lamBind 0 ty (papp fc (PRef fc n) (methArgs 0 ty))

2015 = lamBind 0 ty (papp fc (PRef fc n) (methArgs 0 ty))

2012− lamBind i (PPi (Constraint _ _ _) _ _ sc) sc'

2016+ lamBind i (PPi (Constraint _ _) _ _ sc) sc'

2013 = PLam (sMN i "meth") Placeholder (lamBind (i+1) sc sc')

2017 = PLam (sMN i "meth") Placeholder (lamBind (i+1) sc sc')

2014 lamBind i (PPi _ n ty sc) sc'

2018 lamBind i (PPi _ n ty sc) sc'

2015 = PLam (sMN i "meth") Placeholder (lamBind (i+1) sc sc')

2019 = PLam (sMN i "meth") Placeholder (lamBind (i+1) sc sc')

2016 lamBind i _ sc = sc

2020 lamBind i _ sc = sc

2017− methArgs i (PPi (Imp _ _ _ _) n ty sc)

2021+ methArgs i (PPi (Imp _ _ _) n ty sc)

2018− = PImp 0 True [] n (PRef fc (sMN i "meth")) "" : methArgs (i+1) sc

2022+ = PImp 0 True [] n (PRef fc (sMN i "meth")) : methArgs (i+1) sc

2019− methArgs i (PPi (Exp _ _ _ _) n ty sc)

2023+ methArgs i (PPi (Exp _ _ _) n ty sc)

2020− = PExp 0 [] (PRef fc (sMN i "meth")) "" : methArgs (i+1) sc

2024+ = PExp 0 [] (PRef fc (sMN i "meth")) : methArgs (i+1) sc

2021− methArgs i (PPi (Constraint _ _ _) n ty sc)

2025+ methArgs i (PPi (Constraint _ _) n ty sc)

2022− = PConstraint 0 [] (PResolveTC fc) "" : methArgs (i+1) sc

2026+ = PConstraint 0 [] (PResolveTC fc) : methArgs (i+1) sc

2023 methArgs i _ = []

2027 methArgs i _ = []

2024

2028

2025 papp fc f [] = f

2029 papp fc f [] = f

@@ -2038,12 +2042,12 @@ elabInstance info syn what fc cs n ps t expn ds = do

2038 decorate ns iname (UN n) = NS (SN (MethodN (UN n))) ns

2042 decorate ns iname (UN n) = NS (SN (MethodN (UN n))) ns

2039 decorate ns iname (NS (UN n) s) = NS (SN (MethodN (UN n))) ns

2043 decorate ns iname (NS (UN n) s) = NS (SN (MethodN (UN n))) ns

2040

2044

2041− mkTyDecl (n, op, t, _) = PTy "" syn fc op n t

2045+ mkTyDecl (n, op, t, _) = PTy "" [] syn fc op n t

2042

2046

2043 conbind (ty : ns) x = PPi constraint (sMN 0 "class") ty (conbind ns x)

2047 conbind (ty : ns) x = PPi constraint (sMN 0 "class") ty (conbind ns x)

2044 conbind [] x = x

2048 conbind [] x = x

2045

2049

2046− coninsert cs (PPi p@(Imp _ _ _ _) n t sc) = PPi p n t (coninsert cs sc)

2050+ coninsert cs (PPi p@(Imp _ _ _) n t sc) = PPi p n t (coninsert cs sc)

2047 coninsert cs sc = conbind cs sc

2051 coninsert cs sc = conbind cs sc

2048

2052

2049 insertDefaults :: IState -> Name ->

2053 insertDefaults :: IState -> Name ->

@@ -2101,7 +2105,7 @@ elabInstance info syn what fc cs n ps t expn ds = do

2101 PClauses fc [Dictionary] cfn [PClause fc cfn lhs [] rhs []]]

2105 PClauses fc [Dictionary] cfn [PClause fc cfn lhs [] rhs []]]

2102-}

2106-}

2103

2107

2104−decorateid decorate (PTy doc s f o n t) = PTy doc s f o (decorate n) t

2108+decorateid decorate (PTy doc argdocs s f o n t) = PTy doc argdocs s f o (decorate n) t

2105decorateid decorate (PClauses f o n cs)

2109decorateid decorate (PClauses f o n cs)

2106 = PClauses f o (decorate n) (map dc cs)

2110 = PClauses f o (decorate n) (map dc cs)

2107 where dc (PClause fc n t as w ds) = PClause fc (decorate n) (dappname t) as w ds

2111 where dc (PClause fc n t as w ds) = PClause fc (decorate n) (dappname t) as w ds

@@ -2155,22 +2159,22 @@ elabDecl' _ info (PFix _ _ _)

2155 = return () -- nothing to elaborate

2159 = return () -- nothing to elaborate

2156elabDecl' _ info (PSyntax _ p)

2160elabDecl' _ info (PSyntax _ p)

2157 = return () -- nothing to elaborate

2161 = return () -- nothing to elaborate

2158−elabDecl' what info (PTy doc s f o n ty)

2162+elabDecl' what info (PTy doc argdocs s f o n ty)

2159 | what /= EDefns

2163 | what /= EDefns

2160 = do iLOG $ "Elaborating type decl " ++ show n ++ show o

2164 = do iLOG $ "Elaborating type decl " ++ show n ++ show o

2161− elabType info s doc f o n ty

2165+ elabType info s doc argdocs f o n ty

2162 return ()

2166 return ()

2163elabDecl' what info (PPostulate doc s f o n ty)

2167elabDecl' what info (PPostulate doc s f o n ty)

2164 | what /= EDefns

2168 | what /= EDefns

2165 = do iLOG $ "Elaborating postulate " ++ show n ++ show o

2169 = do iLOG $ "Elaborating postulate " ++ show n ++ show o

2166 elabPostulate info s doc f o n ty

2170 elabPostulate info s doc f o n ty

2167−elabDecl' what info (PData doc s f co d)

2171+elabDecl' what info (PData doc argDocs s f co d)

2168 | what /= ETypes

2172 | what /= ETypes

2169 = do iLOG $ "Elaborating " ++ show (d_name d)

2173 = do iLOG $ "Elaborating " ++ show (d_name d)

2170− elabData info s doc f co d

2174+ elabData info s doc argDocs f co d

2171 | otherwise

2175 | otherwise

2172 = do iLOG $ "Elaborating [type of] " ++ show (d_name d)

2176 = do iLOG $ "Elaborating [type of] " ++ show (d_name d)

2173− elabData info s doc f co (PLaterdecl (d_name d) (d_tcon d))

2177+ elabData info s doc argDocs f co (PLaterdecl (d_name d) (d_tcon d))

2174elabDecl' what info d@(PClauses f o n ps)

2178elabDecl' what info d@(PClauses f o n ps)

2175 | what /= ETypes

2179 | what /= ETypes

2176 = do iLOG $ "Elaborating clause " ++ show n

2180 = do iLOG $ "Elaborating clause " ++ show n

@@ -2227,7 +2231,7 @@ elabDecl' what info (PRecord doc s f tyn ty cdoc cn cty)

2227 elabRecord info s doc f tyn ty cdoc cn cty

2231 elabRecord info s doc f tyn ty cdoc cn cty

2228 | otherwise

2232 | otherwise

2229 = do iLOG $ "Elaborating [type of] " ++ show tyn

2233 = do iLOG $ "Elaborating [type of] " ++ show tyn

2230− elabData info s doc f [] (PLaterdecl tyn ty)

2234+ elabData info s doc [] f [] (PLaterdecl tyn ty)

2231elabDecl' _ info (PDSL n dsl)

2235elabDecl' _ info (PDSL n dsl)

2232 = do i <- getIState

2236 = do i <- getIState

2233 putIState (i { idris_dsls = addDef n dsl (idris_dsls i) })

2237 putIState (i { idris_dsls = addDef n dsl (idris_dsls i) })

@@ -2282,3 +2286,14 @@ inferredDiff fc inf user =

2282 Right vs -> return False

2286 Right vs -> return False

2283 Left (x, y) -> return True

2287 Left (x, y) -> return True

2284

2288

2289+-- | Check a PTerm against documentation and ensure that every documented

2290+-- argument actually exists. This must be run _after_ implicits have been

2291+-- found, or it will give spurious errors.

2292+checkDocs :: FC -> [(Name, String)] -> PTerm -> Idris ()

2293+checkDocs fc args tm = cd (Map.fromList args) tm

2294+ where cd as (PPi _ n _ sc) = cd (Map.delete n as) sc

2295+ cd as _ | Map.null as = return ()

2296+ | otherwise = ierror . At fc . Msg $

2297+ "There is documentation for argument(s) "

2298+ ++ (concat . intersperse ", " . map show . Map.keys) as

2299+ ++ " but they were not found."

src/Idris/ElabTerm.hs+2−2

@@ -926,7 +926,7 @@ resTC' tcs depth topg fn ist

926 ulog <- getUnifyLog

927 solve

928 traceWhen ulog ("Got " ++ show n) $ return ()

929− where isImp (PImp p _ _ _ _ _) = (True, p)

929+ where isImp (PImp p _ _ _ _) = (True, p)

930 isImp arg = (False, priority arg)

931

932collectDeferred :: Maybe Name ->

@@ -1001,7 +1001,7 @@ runTac autoSolve ist fn tac

1001 show fn')) fnimps

1002 tryAll tacs

1003 when autoSolve solveAll

1004− where isImp (PImp _ _ _ _ _ _) = True

1004+ where isImp (PImp _ _ _ _ _) = True

1005 isImp _ = False

1006 envArgs n = do e <- get_env

1007 case lookup n e of

src/Idris/IBC.hs+28−40

@@ -52,7 +52,7 @@ data IBCFile = IBCFile { ver :: Word8,

52 ibc_flags :: [(Name, [FnOpt])],

53 ibc_cg :: [(Name, CGInfo)],

54 ibc_defs :: [(Name, Def)],

55− ibc_docstrings :: [(Name, String)],

55+ ibc_docstrings :: [(Name, (String, [(Name, String)]))],

56 ibc_transforms :: [(Term, Term)],

57 ibc_errRev :: [(Term, Term)],

58 ibc_coercions :: [Name],

@@ -393,7 +393,7 @@ pDefs syms ds

393 updateOrig (Left t) = Left (update t)

394 updateOrig (Right (l, r)) = Right (update l, update r)

395

396− updateCD (CaseDefs (ts, t) (cs, c) (is, i) (rs, r))

396+ updateCD (CaseDefs (ts, t) (cs, c) (is, i) (rs, r))

397 = CaseDefs (ts, fmap update t)

398 (cs, fmap update c)

399 (is, fmap update i)

@@ -405,8 +405,8 @@ pDefs syms ds

405 update (Proj t i) = Proj (update t) i

406 update t = t

407

408−pDocs :: [(Name, String)] -> Idris ()

408+pDocs :: [(Name, (String, [(Name, String)]))] -> Idris ()

409−pDocs ds = mapM_ (\ (n, a) -> addDocStr n a) ds

409+pDocs ds = mapM_ (\ (n, a) -> addDocStr n (fst a) (snd a)) ds

410

411pAccess :: [(Name, Accessibility)] -> Idris ()

412pAccess ds = mapM_ (\ (n, a) ->

@@ -1234,51 +1234,43 @@ instance Binary Static where

1234instance Binary Plicity where

1235 put x

1236 = case x of

1237− Imp x1 x2 x3 x4 ->

1237+ Imp x1 x2 x3 ->

1238 do putWord8 0

1239 put x1

1240 put x2

1241 put x3

1242− put x4

1243− Exp x1 x2 x3 x4 ->

1242+ Exp x1 x2 x3 ->

1244 do putWord8 1

1243 do putWord8 1

1245 put x1

1244 put x1

1246 put x2

1245 put x2

1247 put x3

1246 put x3

1248− put x4

1249− Constraint x1 x2 x3 ->

1247+ Constraint x1 x2 ->

1250 do putWord8 2

1248 do putWord8 2

1251 put x1

1249 put x1

1252 put x2

1250 put x2

1253− put x3

1254− TacImp x1 x2 x3 x4 ->

1251+ TacImp x1 x2 x3 ->

1255 do putWord8 3

1252 do putWord8 3

1256 put x1

1253 put x1

1257 put x2

1254 put x2

1258 put x3

1255 put x3

1259− put x4

1260 get

1256 get

1261 = do i <- getWord8

1257 = do i <- getWord8

1262 case i of

1258 case i of

1263 0 -> do x1 <- get

1259 0 -> do x1 <- get

1264 x2 <- get

1260 x2 <- get

1265 x3 <- get

1261 x3 <- get

1266− x4 <- get

1267− return (Imp x1 x2 x3 x4)

1262+ return (Imp x1 x2 x3)

1268 1 -> do x1 <- get

1263 1 -> do x1 <- get

1269 x2 <- get

1264 x2 <- get

1270 x3 <- get

1265 x3 <- get

1271− x4 <- get

1272− return (Exp x1 x2 x3 x4)

1266+ return (Exp x1 x2 x3)

1273 2 -> do x1 <- get

1267 2 -> do x1 <- get

1274 x2 <- get

1268 x2 <- get

1275− x3 <- get

1276− return (Constraint x1 x2 x3)

1269+ return (Constraint x1 x2)

1277 3 -> do x1 <- get

1270 3 -> do x1 <- get

1278 x2 <- get

1271 x2 <- get

1279 x3 <- get

1272 x3 <- get

1280− x4 <- get

1281− return (TacImp x1 x2 x3 x4)

1273+ return (TacImp x1 x2 x3)

1282 _ -> error "Corrupted binary data for Plicity"

1274 _ -> error "Corrupted binary data for Plicity"

1283

1275

1284

1276

@@ -1289,7 +1281,7 @@ instance (Binary t) => Binary (PDecl' t) where

1289 put x1

1281 put x1

1290 put x2

1282 put x2

1291 put x3

1283 put x3

1292− PTy x1 x2 x3 x4 x5 x6

1284+ PTy x1 x2 x3 x4 x5 x6 x7

1293 -> do putWord8 1

1285 -> do putWord8 1

1294 put x1

1286 put x1

1295 put x2

1287 put x2

@@ -1297,18 +1289,20 @@ instance (Binary t) => Binary (PDecl' t) where

1297 put x4

1289 put x4

1298 put x5

1290 put x5

1299 put x6

1291 put x6

1292+ put x7

1300 PClauses x1 x2 x3 x4 -> do putWord8 2

1293 PClauses x1 x2 x3 x4 -> do putWord8 2

1301 put x1

1294 put x1

1302 put x2

1295 put x2

1303 put x3

1296 put x3

1304 put x4

1297 put x4

1305− PData x1 x2 x3 x4 x5 ->

1298+ PData x1 x2 x3 x4 x5 x6 ->

1306 do putWord8 3

1299 do putWord8 3

1307 put x1

1300 put x1

1308 put x2

1301 put x2

1309 put x3

1302 put x3

1310 put x4

1303 put x4

1311 put x5

1304 put x5

1305+ put x6

1312 PParams x1 x2 x3 -> do putWord8 4

1306 PParams x1 x2 x3 -> do putWord8 4

1313 put x1

1307 put x1

1314 put x2

1308 put x2

@@ -1375,7 +1369,8 @@ instance (Binary t) => Binary (PDecl' t) where

1375 x4 <- get

1369 x4 <- get

1376 x5 <- get

1370 x5 <- get

1377 x6 <- get

1371 x6 <- get

1372+ x7 <- get

1378− return (PTy x1 x2 x3 x4 x5 x6)

1373+ return (PTy x1 x2 x3 x4 x5 x6 x7)

1379 2 -> do x1 <- get

1374 2 -> do x1 <- get

1380 x2 <- get

1375 x2 <- get

1381 x3 <- get

1376 x3 <- get

@@ -1386,7 +1381,8 @@ instance (Binary t) => Binary (PDecl' t) where

1386 x3 <- get

1381 x3 <- get

1387 x4 <- get

1382 x4 <- get

1388 x5 <- get

1383 x5 <- get

1384+ x6 <- get

1389− return (PData x1 x2 x3 x4 x5)

1385+ return (PData x1 x2 x3 x4 x5 x6)

1390 4 -> do x1 <- get

1386 4 -> do x1 <- get

1391 x2 <- get

1387 x2 <- get

1392 x3 <- get

1388 x3 <- get

@@ -1924,34 +1920,30 @@ instance (Binary t) => Binary (PDo' t) where

1924instance (Binary t) => Binary (PArg' t) where

1920instance (Binary t) => Binary (PArg' t) where

1925 put x

1921 put x

1926 = case x of

1922 = case x of

1927− PImp x1 x2 x3 x4 x5 x6 ->

1923+ PImp x1 x2 x3 x4 x5 ->

1928 do putWord8 0

1924 do putWord8 0

1929 put x1

1925 put x1

1930 put x2

1926 put x2

1931 put x3

1927 put x3

1932 put x4

1928 put x4

1933 put x5

1929 put x5

1934− put x6

1935− PExp x1 x2 x3 x4 ->

1930+ PExp x1 x2 x3 ->

1936 do putWord8 1

1931 do putWord8 1

1937 put x1

1932 put x1

1938 put x2

1933 put x2

1939 put x3

1934 put x3

1940− put x4

1941− PConstraint x1 x2 x3 x4 ->

1935+ PConstraint x1 x2 x3 ->

1942 do putWord8 2

1936 do putWord8 2

1943 put x1

1937 put x1

1944 put x2

1938 put x2

1945 put x3

1939 put x3

1946− put x4

1947− PTacImplicit x1 x2 x3 x4 x5 x6 ->

1940+ PTacImplicit x1 x2 x3 x4 x5 ->

1948 do putWord8 3

1941 do putWord8 3

1949 put x1

1942 put x1

1950 put x2

1943 put x2

1951 put x3

1944 put x3

1952 put x4

1945 put x4

1953 put x5

1946 put x5

1954− put x6

1955 get

1947 get

1956 = do i <- getWord8

1948 = do i <- getWord8

1957 case i of

1949 case i of

@@ -1960,25 +1952,21 @@ instance (Binary t) => Binary (PArg' t) where

1960 x3 <- get

1952 x3 <- get

1961 x4 <- get

1953 x4 <- get

1962 x5 <- get

1954 x5 <- get

1963− x6 <- get

1964− return (PImp x1 x2 x3 x4 x5 x6)

1955+ return (PImp x1 x2 x3 x4 x5)

1965 1 -> do x1 <- get

1956 1 -> do x1 <- get

1966 x2 <- get

1957 x2 <- get

1967 x3 <- get

1958 x3 <- get

1968− x4 <- get

1969− return (PExp x1 x2 x3 x4)

1959+ return (PExp x1 x2 x3)

1970 2 -> do x1 <- get

1960 2 -> do x1 <- get

1971 x2 <- get

1961 x2 <- get

1972 x3 <- get

1962 x3 <- get

1973− x4 <- get

1974− return (PConstraint x1 x2 x3 x4)

1963+ return (PConstraint x1 x2 x3)

1975 3 -> do x1 <- get

1964 3 -> do x1 <- get

1976 x2 <- get

1965 x2 <- get

1977 x3 <- get

1966 x3 <- get

1978 x4 <- get

1967 x4 <- get

1979 x5 <- get

1968 x5 <- get

1980− x6 <- get

1981− return (PTacImplicit x1 x2 x3 x4 x5 x6)

1969+ return (PTacImplicit x1 x2 x3 x4 x5)

1982 _ -> error "Corrupted binary data for PArg'"

1970 _ -> error "Corrupted binary data for PArg'"

1983

1971

1984

1972

src/Idris/ParseData.hs+26−24

@@ -33,13 +33,15 @@ import qualified Data.HashSet as HS

33import qualified Data.Text as T

34import qualified Data.ByteString.UTF8 as UTF8

36+import Debug.Trace

37+

36{- |Parses a record type declaration

38{- |Parses a record type declaration

37Record ::=

39Record ::=

38 DocComment Accessibility? 'record' FnName TypeSig 'where' OpenBlock Constructor KeepTerminator CloseBlock;

40 DocComment Accessibility? 'record' FnName TypeSig 'where' OpenBlock Constructor KeepTerminator CloseBlock;

39-}

41-}

40record :: SyntaxInfo -> IdrisParser PDecl

42record :: SyntaxInfo -> IdrisParser PDecl

41record syn = do (doc, acc) <- try (do

43record syn = do (doc, acc) <- try (do

42− doc <- option "" (docComment '|')

44+ doc <- option ("", []) docComment

43 acc <- optional accessibility

45 acc <- optional accessibility

44 reserved "record"

46 reserved "record"

45 return (doc, acc))

47 return (doc, acc))

@@ -49,13 +51,13 @@ record syn = do (doc, acc) <- try (do

49 ty <- typeExpr (allowImp syn)

51 ty <- typeExpr (allowImp syn)

50 let tyn = expandNS syn tyn_in

52 let tyn = expandNS syn tyn_in

51 reserved "where"

53 reserved "where"

52− (cdoc, cn, cty, _, _) <- indentedBlockS (constructor syn)

54+ (cdoc, argDocs, cn, cty, _, _) <- indentedBlockS (constructor syn)

53 accData acc tyn [cn]

55 accData acc tyn [cn]

54 let rsyn = syn { syn_namespace = show (nsroot tyn) :

56 let rsyn = syn { syn_namespace = show (nsroot tyn) :

55 syn_namespace syn }

57 syn_namespace syn }

56 let fns = getRecNames rsyn cty

58 let fns = getRecNames rsyn cty

57 mapM_ (\n -> addAcc n acc) fns

59 mapM_ (\n -> addAcc n acc) fns

58− return $ PRecord doc rsyn fc tyn ty cdoc cn cty

60+ return $ PRecord (fst doc) rsyn fc tyn ty cdoc cn cty

59 <?> "record type declaration"

61 <?> "record type declaration"

60 where

62 where

61 getRecNames :: SyntaxInfo -> PTerm -> [Name]

63 getRecNames :: SyntaxInfo -> PTerm -> [Name]

@@ -100,29 +102,29 @@ SimpleConstructorList ::=

100 ;

102 ;

101-}

103-}

102data_ :: SyntaxInfo -> IdrisParser PDecl

104data_ :: SyntaxInfo -> IdrisParser PDecl

103−data_ syn = do (doc, acc, dataOpts) <- try (do

105+data_ syn = do (doc, argDocs, acc, dataOpts) <- try (do

104− doc <- option "" (docComment '|')

106+ (doc, argDocs) <- option ("", []) docComment

105 pushIndent

107 pushIndent

106 acc <- optional accessibility

108 acc <- optional accessibility

107 elim <- dataOpts []

109 elim <- dataOpts []

108 co <- dataI

110 co <- dataI

109 let dataOpts = combineDataOpts(elim ++ co)

111 let dataOpts = combineDataOpts(elim ++ co)

110− return (doc, acc, dataOpts))

112+ return (doc, argDocs, acc, dataOpts))

111 fc <- getFC

113 fc <- getFC

112 tyn_in <- fnName

114 tyn_in <- fnName

113 (do try (lchar ':')

115 (do try (lchar ':')

114 popIndent

116 popIndent

115 ty <- typeExpr (allowImp syn)

117 ty <- typeExpr (allowImp syn)

116 let tyn = expandNS syn tyn_in

118 let tyn = expandNS syn tyn_in

117− option (PData doc syn fc dataOpts (PLaterdecl tyn ty)) (do

119+ option (PData doc argDocs syn fc dataOpts (PLaterdecl tyn ty)) (do

118 reserved "where"

120 reserved "where"

119 cons <- indentedBlock (constructor syn)

121 cons <- indentedBlock (constructor syn)

120− accData acc tyn (map (\ (_, n, _, _, _) -> n) cons)

122+ accData acc tyn (map (\ (_, _, n, _, _, _) -> n) cons)

121− return $ PData doc syn fc dataOpts (PDatadecl tyn ty cons))) <|> (do

123+ return $ PData doc argDocs syn fc dataOpts (PDatadecl tyn ty cons))) <|> (do

122 args <- many name

124 args <- many name

123 let ty = bindArgs (map (const PType) args) PType

125 let ty = bindArgs (map (const PType) args) PType

124 let tyn = expandNS syn tyn_in

126 let tyn = expandNS syn tyn_in

125− option (PData doc syn fc dataOpts (PLaterdecl tyn ty)) (do

127+ option (PData doc argDocs syn fc dataOpts (PLaterdecl tyn ty)) (do

126 try (lchar '=') <|> do reserved "where"

128 try (lchar '=') <|> do reserved "where"

127 let kw = (if DefaultEliminator `elem` dataOpts then "" else "%noelim ") ++ (if Codata `elem` dataOpts then "co" else "") ++ "data "

129 let kw = (if DefaultEliminator `elem` dataOpts then "" else "%noelim ") ++ (if Codata `elem` dataOpts then "co" else "") ++ "data "

128 let n = show tyn_in ++ " "

130 let n = show tyn_in ++ " "

@@ -134,14 +136,14 @@ data_ syn = do (doc, acc, dataOpts) <- try (do

134 let fix2 = s ++ ": " ++ ns ++ " -> Type where\n ..."

136 let fix2 = s ++ ": " ++ ns ++ " -> Type where\n ..."

135 let fix3 = s ++ ": " ++ ss ++ " -> Type where\n ..."

137 let fix3 = s ++ ": " ++ ss ++ " -> Type where\n ..."

136 fail $ fixErrorMsg "unexpected \"where\"" [fix1, fix2, fix3]

138 fail $ fixErrorMsg "unexpected \"where\"" [fix1, fix2, fix3]

137− cons <- sepBy1 (simpleConstructor syn) (lchar '|')

139+ cons <- sepBy1 (simpleConstructor syn) (reservedOp "|")

138 terminator

140 terminator

139 let conty = mkPApp fc (PRef fc tyn) (map (PRef fc) args)

141 let conty = mkPApp fc (PRef fc tyn) (map (PRef fc) args)

140− cons' <- mapM (\ (doc, x, cargs, cfc, fs) ->

142+ cons' <- mapM (\ (doc, argDocs, x, cargs, cfc, fs) ->

141 do let cty = bindArgs cargs conty

143 do let cty = bindArgs cargs conty

142− return (doc, x, cty, cfc, fs)) cons

144+ return (doc, argDocs, x, cty, cfc, fs)) cons

143− accData acc tyn (map (\ (_, n, _, _, _) -> n) cons')

145+ accData acc tyn (map (\ (_, _, n, _, _, _) -> n) cons')

144− return $ PData doc syn fc dataOpts (PDatadecl tyn ty cons')))

146+ return $ PData doc argDocs syn fc dataOpts (PDatadecl tyn ty cons')))

145 <?> "data type declaration"

147 <?> "data type declaration"

146 where

148 where

147 mkPApp :: FC -> PTerm -> [PTerm] -> PTerm

149 mkPApp :: FC -> PTerm -> [PTerm] -> PTerm

@@ -150,17 +152,17 @@ data_ syn = do (doc, acc, dataOpts) <- try (do

150 bindArgs :: [PTerm] -> PTerm -> PTerm

152 bindArgs :: [PTerm] -> PTerm -> PTerm

151 bindArgs xs t = foldr (PPi expl (sMN 0 "_t")) t xs

153 bindArgs xs t = foldr (PPi expl (sMN 0 "_t")) t xs

152 combineDataOpts :: DataOpts -> DataOpts

154 combineDataOpts :: DataOpts -> DataOpts

153− combineDataOpts opts = if Codata `elem` opts

155+ combineDataOpts opts = if Codata `elem` opts

154− then delete DefaultEliminator opts

156+ then delete DefaultEliminator opts

155 else opts

157 else opts

156

158

157

159

158{- | Parses a type constructor declaration

160{- | Parses a type constructor declaration

159 Constructor ::= DocComment? FnName TypeSig;

161 Constructor ::= DocComment? FnName TypeSig;

160-}

162-}

161−constructor :: SyntaxInfo -> IdrisParser (String, Name, PTerm, FC, [Name])

163+constructor :: SyntaxInfo -> IdrisParser (String, [(Name, String)], Name, PTerm, FC, [Name])

162constructor syn

164constructor syn

163− = do doc <- option "" (docComment '|')

165+ = do (doc, argDocs) <- option ("", []) docComment

164 cn_in <- fnName; fc <- getFC

166 cn_in <- fnName; fc <- getFC

165 let cn = expandNS syn cn_in

167 let cn = expandNS syn cn_in

166 lchar ':'

168 lchar ':'

@@ -169,21 +171,21 @@ constructor syn

169 fs <- option [] (do lchar '%'; reserved "erase"

171 fs <- option [] (do lchar '%'; reserved "erase"

170 sepBy1 name (lchar ','))

172 sepBy1 name (lchar ','))

171 ty <- typeExpr (allowImp syn)

173 ty <- typeExpr (allowImp syn)

172− return (doc, cn, ty, fc, fs)

174+ return (doc, argDocs, cn, ty, fc, fs)

173 <?> "constructor"

175 <?> "constructor"

174

176

175{- | Parses a constructor for simple discriminative union data types

177{- | Parses a constructor for simple discriminative union data types

176 SimpleConstructor ::= FnName SimpleExpr* DocComment?

178 SimpleConstructor ::= FnName SimpleExpr* DocComment?

177-}

179-}

178−simpleConstructor :: SyntaxInfo -> IdrisParser (String, Name, [PTerm], FC, [Name])

180+simpleConstructor :: SyntaxInfo -> IdrisParser (String, [(Name, String)], Name, [PTerm], FC, [Name])

179simpleConstructor syn

181simpleConstructor syn

182+ = do doc <- option ("", []) (try docComment)

180− = do cn_in <- fnName

183+ cn_in <- fnName

181 let cn = expandNS syn cn_in

184 let cn = expandNS syn cn_in

182 fc <- getFC

185 fc <- getFC

183 args <- many (do notEndApp

186 args <- many (do notEndApp

184 simpleExpr syn)

187 simpleExpr syn)

185− doc <- option "" (try $ docComment '^')

186− return (doc, cn, args, fc, [])

188+ return (fst doc, [], cn, args, fc, [])

187 <?> "constructor"

189 <?> "constructor"

188

190

189{- | Parses a dsl block declaration

191{- | Parses a dsl block declaration

src/Idris/ParseExpr.hs+4−5

@@ -786,10 +786,9 @@ pi syn =

786 return []

787 st <- static

788 (do try (lchar '('); xt <- typeDeclList syn; lchar ')'

789− doc <- option "" (docComment '^')

790 symbol "->"

789 symbol "->"

791 sc <- expr syn

790 sc <- expr syn

792− return (bindList (PPi (Exp opts st doc False)) xt sc)) <|> (do

791+ return (bindList (PPi (Exp opts st False)) xt sc)) <|> (do

793 lchar '{'

792 lchar '{'

794 (do reserved "auto"

793 (do reserved "auto"

795 when (Lazy `elem` opts || (st == Static)) $ fail "auto type constraints can not be lazy or static"

794 when (Lazy `elem` opts || (st == Static)) $ fail "auto type constraints can not be lazy or static"

@@ -798,7 +797,7 @@ pi syn =

798 symbol "->"

797 symbol "->"

799 sc <- expr syn

798 sc <- expr syn

800 return (bindList (PPi

799 return (bindList (PPi

801− (TacImp [] Dynamic (PTactics [Trivial]) "")) xt sc))

800+ (TacImp [] Dynamic (PTactics [Trivial]))) xt sc))

802 <|> (do

801 <|> (do

803 reserved "default"

802 reserved "default"

804 when (Lazy `elem` opts || (st == Static)) $ fail "default tactic constraints can not be lazy or static"

803 when (Lazy `elem` opts || (st == Static)) $ fail "default tactic constraints can not be lazy or static"

@@ -807,13 +806,13 @@ pi syn =

807 lchar '}'

806 lchar '}'

808 symbol "->"

807 symbol "->"

809 sc <- expr syn

808 sc <- expr syn

810− return (bindList (PPi (TacImp [] Dynamic script "")) xt sc))

809+ return (bindList (PPi (TacImp [] Dynamic script)) xt sc))

811 <|> (if implicitAllowed syn then do

810 <|> (if implicitAllowed syn then do

812 xt <- typeDeclList syn

811 xt <- typeDeclList syn

813 lchar '}'

812 lchar '}'

814 symbol "->"

813 symbol "->"

815 sc <- expr syn

814 sc <- expr syn

816− return (bindList (PPi (Imp opts st "" False)) xt sc)

815+ return (bindList (PPi (Imp opts st False)) xt sc)

817 else do fail "no implicit arguments allowed here"))

816 else do fail "no implicit arguments allowed here"))

818 <?> "dependent type signature"

817 <?> "dependent type signature"

819

818

src/Idris/ParseHelpers.hs+33−32

@@ -17,6 +17,8 @@ import Idris.Core.TT

17import Idris.Core.Evaluate

18import Idris.Delaborate (pprintErr)

20+import qualified Util.Pretty as Pretty (text)

21+

20import Control.Applicative

22import Control.Applicative

21import Control.Monad

23import Control.Monad

22import Control.Monad.State.Strict

24import Control.Monad.State.Strict

@@ -33,6 +35,8 @@ import qualified Data.ByteString.UTF8 as UTF8

34import System.FilePath

36import System.FilePath

38+import Debug.Trace

39+

36-- | Idris parser with state used during parsing

40-- | Idris parser with state used during parsing

37type IdrisParser = StateT IState IdrisInnerParser

41type IdrisParser = StateT IState IdrisInnerParser

@@ -51,10 +55,10 @@ runparser p i inputname =

51 parseString (runInnerParser (evalStateT p i))

55 parseString (runInnerParser (evalStateT p i))

52 (Directed (UTF8.fromString inputname) 0 0 0 0)

56 (Directed (UTF8.fromString inputname) 0 0 0 0)

54−noDocCommentHere :: Char -> String -> IdrisParser ()

58+noDocCommentHere :: String -> IdrisParser ()

55−noDocCommentHere c msg =

59+noDocCommentHere msg =

56 optional (do fc <- getFC

60 optional (do fc <- getFC

57− docComment c

61+ docComment

58 ist <- get

62 ist <- get

59 put ist { parserWarnings = (fc, Msg msg) : parserWarnings ist}) *>

63 put ist { parserWarnings = (fc, Msg msg) : parserWarnings ist}) *>

60 pure ()

64 pure ()

@@ -86,12 +90,6 @@ isEol _ = False

86eol :: MonadicParsing m => m ()

90eol :: MonadicParsing m => m ()

87eol = (satisfy isEol *> pure ()) <|> lookAhead eof <?> "end of line"

91eol = (satisfy isEol *> pure ()) <|> lookAhead eof <?> "end of line"

89−-- | Checks if a character is a documentation comment marker

90−isDocCommentMarker :: Char -> Bool

91−isDocCommentMarker '|' = True

92−isDocCommentMarker '^' = True

93−isDocCommentMarker _ = False

94−

95{- | Consumes a single-line comment

93{- | Consumes a single-line comment

97@

95@

@@ -103,7 +101,6 @@ isDocCommentMarker _ = False

103singleLineComment :: MonadicParsing m => m ()

101singleLineComment :: MonadicParsing m => m ()

104singleLineComment = try (string "--" *> eol *> pure ())

102singleLineComment = try (string "--" *> eol *> pure ())

105 <|> try (string "--" *> many simpleWhiteSpace *>

103 <|> try (string "--" *> many simpleWhiteSpace *>

106− satisfy (not . isDocCommentMarker) *>

107 many (satisfy (not . isEol)) *>

104 many (satisfy (not . isEol)) *>

108 eol *> pure ())

105 eol *> pure ())

109 <?> ""

106 <?> ""

@@ -127,13 +124,12 @@ singleLineComment = try (string "--" *> eol *> pure ())

127-}

124-}

128multiLineComment :: MonadicParsing m => m ()

125multiLineComment :: MonadicParsing m => m ()

129multiLineComment = try (string "{-" *> (string "-}") *> pure ())

126multiLineComment = try (string "{-" *> (string "-}") *> pure ())

130− <|> string "{-" *> satisfy (not . isDocCommentMarker) *> inCommentChars

127+ <|> string "{-" *> inCommentChars

131 <?> ""

128 <?> ""

132 where inCommentChars :: MonadicParsing m => m ()

129 where inCommentChars :: MonadicParsing m => m ()

133 inCommentChars = string "-}" *> pure ()

130 inCommentChars = string "-}" *> pure ()

134 <|> try (multiLineComment) *> inCommentChars

131 <|> try (multiLineComment) *> inCommentChars

135− <|> try (docComment '|') *> inCommentChars

136− <|> try (docComment '^') *> inCommentChars

132+ <|> string "|||" *> many (satisfy (not . isEol)) *> eol *> inCommentChars

137 <|> skipSome (noneOf startEnd) *> inCommentChars

133 <|> skipSome (noneOf startEnd) *> inCommentChars

138 <|> oneOf startEnd *> inCommentChars

134 <|> oneOf startEnd *> inCommentChars

139 <?> "end of comment"

135 <?> "end of comment"

@@ -148,27 +144,32 @@ multiLineComment = try (string "{-" *> (string "-}") *> pure ())

148 ;

144 ;

149@

145@

150 -}

146 -}

151−docComment :: MonadicParsing m => Char -> m String

147+docComment :: IdrisParser (String, [(Name, String)])

152−docComment marker | isDocCommentMarker marker = do dc <- docComment' marker

148+docComment = do dc <- pushIndent *> docCommentLine

149+ rest <- many (indented docCommentLine)

150+ args <- many (indented argDocCommentLine)

151+ popIndent

153− return (T.unpack $ T.strip $ T.pack dc)

152+ return (T.unpack $ T.strip $ T.pack (dc ++ concat rest), args)

154− | otherwise = fail "internal error: tried to parse a documentation comment with invalid marker"

153+

155− where docComment' :: MonadicParsing m => Char -> m String

154+ where docCommentLine :: MonadicParsing m => m String

156− docComment' marker = (do string "--"

155+ docCommentLine = try (do string "|||"

157 many (satisfy isSpace)

156 many (satisfy isSpace)

158− char marker

157+ first <- satisfy (\c -> not (isEol c || c == '@'))

159 res <- many (satisfy (not . isEol))

158 res <- many (satisfy (not . isEol))

160− eol

159+ eol ; someSpace

161− rest <- many (do string "--"

160+ return (first:res))-- ++ concat rest))

161+ <?> ""

162+ argDocCommentLine = do string "|||"

163+ many (satisfy isSpace)

164+ char '@'

165+ many (satisfy isSpace)

166+ n <- name

167+ many (satisfy isSpace)

162− stuff <- many (satisfy (not . isEol))

168+ docs <- many (satisfy (not . isEol))

163− eol

164− return stuff)

165− someSpace

169+ eol ; someSpace

166− return (res ++ concat rest))-- ++ concat rest))

170+ return (n, docs)

167− <|> (do string "{-"

171+

168− many (satisfy isSpace)

172+

169− char marker

170− (manyTill anyChar (try (string "-}")) <?> "end of comment"))

171− <?> ""

172

173

173-- | Parses some white space

174-- | Parses some white space

174whiteSpace :: MonadicParsing m => m ()

175whiteSpace :: MonadicParsing m => m ()

src/Idris/ParseOps.hs+1−1

@@ -59,7 +59,7 @@ binary name f = Infix (do fc <- getFC

59 indentPropHolds gtProp

60 reservedOp name

61 indentPropHolds gtProp

62− doc <- option "" (docComment '^')

62+ doc <- option ("", []) docComment

63 return (f fc))

65-- | Prefix operator

src/Idris/Parser.hs+8−8

@@ -87,7 +87,7 @@ import System.IO

87@

88-}

89moduleHeader :: IdrisParser [String]

90−moduleHeader = try (do noDocCommentHere '|' "Modules cannot have documentation comments"

90+moduleHeader = try (do noDocCommentHere "Modules cannot have documentation comments"

91 reserved "module"

92 i <- identifier

93 option ';' (lchar ';')

@@ -315,7 +315,7 @@ fnDecl' syn = checkFixity $

315 do (doc, fc, opts', n, acc) <- try (do

316 pushIndent

317 ist <- get

318− doc <- option "" (docComment '|')

318+ doc <- option ("", []) docComment

319 ist <- get

320 let initOpts = if default_total ist

321 then [TotalFn]

@@ -331,7 +331,7 @@ fnDecl' syn = checkFixity $

331 ty <- typeExpr (allowImp syn)

332 terminator

333 addAcc n acc

334− return (PTy doc syn fc opts' n ty)

334+ return (PTy (fst doc) (snd doc) syn fc opts' n ty)

335 <|> postulate syn

336 <|> caf syn

337 <|> pattern syn

@@ -344,7 +344,7 @@ fnDecl' syn = checkFixity $

344 unless fOk . fail $

345 "Missing fixity declaration for " ++ show n

346 return decl

347− getName (PTy _ _ _ _ n _) = Just n

347+ getName (PTy _ _ _ _ _ n _) = Just n

348 getName _ = Nothing

349 fixityOK (NS n _) = fixityOK n

350 fixityOK (UN n) | all (flip elem opChars) (str n) =

@@ -413,7 +413,7 @@ Postulate ::=

413@

414-}

415postulate :: SyntaxInfo -> IdrisParser PDecl

416−postulate syn = do doc <- try $ do doc <- option "" (docComment '|')

416+postulate syn = do doc <- try $ do doc <- option ("", []) docComment

417 pushIndent

418 reserved "postulate"

419 return doc

@@ -431,7 +431,7 @@ postulate syn = do doc <- try $ do doc <- option "" (docComment '|')

431 fc <- getFC

432 terminator

433 addAcc n acc

434− return (PPostulate doc syn fc opts' n ty)

434+ return (PPostulate (fst doc) syn fc opts' n ty)

435 <?> "postulate"

436

437{- | Parses a using declaration

@@ -561,7 +561,7 @@ Class ::=

561-}

562class_ :: SyntaxInfo -> IdrisParser [PDecl]

563class_ syn = do (doc, acc) <- try (do

564− doc <- option "" (docComment '|')

564+ doc <- option ("", []) docComment

565 acc <- optional accessibility

566 return (doc, acc))

567 reserved "class"; fc <- getFC; cons <- constraintList syn; n_in <- fnName

@@ -569,7 +569,7 @@ class_ syn = do (doc, acc) <- try (do

569 cs <- many carg

570 ds <- option [] (classBlock syn)

571 accData acc n (concatMap declared ds)

572− return [PClass doc syn fc cons n cs ds]

572+ return [PClass (fst doc) syn fc cons n cs ds]

573 <?> "type-class declaration"

574 where

575 carg :: IdrisParser (Name, PTerm)

src/Idris/PartialEval.hs+2−2

@@ -103,7 +103,7 @@ mkPE_TermDecl ist newname sname ns

103 deImp (PApp fc t as) = PApp fc t (map deImpArg as)

104 deImp t = t

105

106− deImpArg a@(PImp _ _ _ _ _ _) = a { getTm = Placeholder }

106+ deImpArg a@(PImp _ _ _ _ _) = a { getTm = Placeholder }

107 deImpArg a = a

108

109data PEArgType = ImplicitS | ImplicitD

@@ -124,7 +124,7 @@ getSpecApps ist env tm = ga env (explicitNames tm) where

124 | imparg imp = (ImplicitD, tm)

125 | otherwise = (ExplicitD, (P Ref (sUN (show n ++ "arg")) Erased))

126

127− imparg (PExp _ _ _ _) = False

127+ imparg (PExp _ _ _) = False

128 imparg _ = True

129

130 buildApp env [] [] _ _ = []

src/Idris/ProofSearch.hs+1−1

@@ -109,6 +109,6 @@ proofSearch elab fn nroot hints ist

109 (filter (\ (x, y) -> not x) (zip (map fst imps) args))

110 solve

111

112− isImp (PImp p _ _ _ _ _) = (True, p)

112+ isImp (PImp p _ _ _ _) = (True, p)

113 isImp arg = (False, priority arg)

114

src/Idris/Providers.hs+1−1

@@ -11,7 +11,7 @@ import Debug.Trace

12-- | Wrap a type provider in the type of type providers

13providerTy :: FC -> PTerm -> PTerm

14−providerTy fc tm = PApp fc (PRef fc $ sUN "Provider") [PExp 0 [] tm ""]

14+providerTy fc tm = PApp fc (PRef fc $ sUN "Provider") [PExp 0 [] tm]

16ioret = sUN "prim_io_return"

17ermod = sNS (sUN "Error") ["Providers"]