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

CHANGELOG+6

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

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

1111 or show the type of expressions

1212* 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

1319

1420New in 0.9.11:

1521--------------

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

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

77%access public

88

99

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

11−-- Zero is chosen to be positive.

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

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

1212data ZZ = Pos Nat | NegS Nat

1313

1414instance Signed ZZ where

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

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

11module Debug.Trace

22

3−trace : String -> a -> a

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

4+||| @ msg what to print

5+||| @ result the final result

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

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

58

69

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

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

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

2222

2323class (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)

2525

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

2727minimum x y with (order x y)

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

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

2222 -- ^ explicit universe variable

2323%name TTUExp uexp

2424

25−-- | Primitive constants

25+||| Primitive constants

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

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

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

6666reflectConstant = toConst

6767

6868

69−-- | Types of named references

69+||| Types of named references

7070data NameType = Bound

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

7272 | Ref

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

7777 -- ^ type constructor with tag and number

7878%name NameType nt, nt'

7979

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

81−-- binding contexts

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

81+||| binding contexts

8282data Binder a = Lam a

8383 | Pi a

8484 | Let a a

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

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

125125

126126

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

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

128128data TT = P NameType TTName TT

129129 -- ^ named binders

130130 | V Int

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

146146

147147%name TT tm, tm'

148148

149−-- | Raw terms without types

149+||| Raw terms without types

150150data Raw = Var TTName

151151 | RBind TTName (Binder Raw) Raw

152152 | RApp Raw Raw

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

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

4242

4343%name Err err, e

4444

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

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

4646data ErrorReportPart = TextPart String

4747 | NamePart TTName

4848 | TermPart TT

libs/base/Providers.idr+12−1

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

11module Providers

22

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

34public

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

9+

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

516

617-- instances

718instance Functor Provider where

libs/base/System.idr+9−6

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

55%default partial

66%access public

77

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

89getArgs : IO (List String)

910getArgs = do n <- numArgs

1011 ga' [] 0 n

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

2021 do arg <- getArg i

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

2223

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

24−-- otherwise it returns Nothing.

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

25+||| otherwise it returns Nothing.

2526getEnv : String -> IO (Maybe String)

2627getEnv key = do

2728 str_ptr <- getEnv'

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

3334 getEnv' : IO String

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

3536

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

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

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

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

3839setEnv : String -> String -> IO Bool

3940setEnv key value = do

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

4142 return (ok == 0)

4243

43−-- Unsets an environment variable.

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

44+||| Unsets an environment variable.

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

4546unsetEnv : String -> IO Bool

4647unsetEnv key = do

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

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

6869 then return $ reverse $ map splitEq acc

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

7071

72+||| Quit with a particular exit code

7173exit : Int -> IO ()

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

7375

76+||| Get the Unix time

7477time : IO Int

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

7679

libs/prelude/Builtins.idr+22−8

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

33%access public

44%default total

55

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

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

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

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

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

811

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

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

1014getWitness (a ** v) = a

1115

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

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

1318getProof (a ** v) = v

1419

1520FalseElim : _|_ -> a

1621

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

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

1823data Symbol_ : String -> Type where

1924

2025-- ------------------------------------------------------ [ For rewrite tactic ]

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

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

2228replace refl prf = prf

2329

30+||| Symmetry of propositional equality

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

2532sym refl = refl

2633

34+||| Transitivity of propositional equality

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

2836trans refl refl = refl

2937

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

4856trace_malloc : a -> a

4957trace_malloc x = x -- compiled specially

5058

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

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

53−assert_smaller : a -> a -> a

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

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)

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

5464assert_smaller x y = y

5565

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

57−-- terminate.

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

67+||| terminate.

5868assert_total : a -> a

5969assert_total x = x

6070

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!

6173abstract %assert_total -- need to pretend

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

74+believe_me : a -> b

6375believe_me x = prim__believe_me _ _ x

6476

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

6680really_believe_me : a -> b

6781really_believe_me x = prim__believe_me _ _ x

6882

libs/prelude/Prelude/Applicative.idr+3

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

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

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

2121

22+||| Lift a function to an applicative

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

2324liftA f a = pure f <$> a

2425

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

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

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

2729

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

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

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

3033

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

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

33Not : Type -> Type

44Not a = a -> _|_

55

6−-- | Identity function.

6+||| Identity function.

77id : a -> a

88id x = x

99

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

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

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

11+||| @ a the type to assign

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

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

1214the _ = id

1315

14−-- | Constant function.

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

1517const : a -> b -> a

1618const x = \v => x

1719

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

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

1921fst : (s, t) -> s

2022fst (x, y) = x

2123

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

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

2325snd : (a, b) -> b

2426snd (x, y) = y

2527

2628infixl 9 .

2729

28−-- | Function composition

30+||| Function composition

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

3032(.) f g x = f (g x)

3133

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

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

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

35+||| @ f the function to flip

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

3437flip f x y = f y x

3538

36−-- | Function application.

39+||| Function application.

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

3841apply f a = f a

3942

43+||| Equality is a congruence.

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

4145cong refl = refl

4246

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

4348data Dec : Type -> Type where

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

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

49+

50+ ||| The case where the property holds

51+ ||| @ prf the proof

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

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

4657

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

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

11module Prelude.Bool

22

3−-- | Boolean Data Type

3+||| Boolean Data Type

44data Bool = False | True

55

6−-- | Boolean elimination

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

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

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

811boolElim True t e = t

912boolElim False t e = e

1013

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.

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

1316

1417-- Syntaxtic sugar for boolean elimination.

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

1720-- Boolean Operator Precedence

1821infixl 4 &&, ||

1922

20−-- | Boolean OR

23+||| Boolean OR

2124(||) : Bool -> Bool -> Bool

2225(||) False x = x

2326(||) True _ = True

2427

25−-- | Boolean AND

28+||| Boolean AND

2629(&&) : Bool -> Bool -> Bool

2730(&&) True x = x

2831(&&) False _ = False

2932

30−-- | Boolean NOT

33+||| Boolean NOT

3134not : Bool -> Bool

3235not True = False

3336not False = True

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

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

33

44import Builtins

55

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

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

77chr : Int -> Char

88chr x = prim__intToChar x

99

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

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

1111ord : Char -> Int

1212ord x = prim__charToInt x

1313

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

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

1515isUpper : Char -> Bool

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

1717

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

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

1919isLower : Char -> Bool

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

2121

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].

2323isAlpha : Char -> Bool

2424isAlpha x = isUpper x || isLower x

2525

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

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

2727isDigit : Char -> Bool

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

2929

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]

3131isAlphaNum : Char -> Bool

3232isAlphaNum x = isDigit x || isAlpha x

3333

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

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

3535isSpace : Char -> Bool

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

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

3838 x == '\xa0'

3939

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

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

4141isNL : Char -> Bool

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

4343

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

45−-- Non-letters are ignored.

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

45+||| Non-letters are ignored.

4646toUpper : Char -> Char

4747toUpper x = if (isLower x)

4848 then (prim__intToChar (prim__charToInt x - 32))

4949 else x

5050

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

52−-- Non-letters are ignored.

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

52+||| Non-letters are ignored.

5353toLower : Char -> Char

5454toLower x = if (isUpper x)

5555 then (prim__intToChar (prim__charToInt x + 32))

5656 else x

5757

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]

5959isHexDigit : Char -> Bool

6060isHexDigit x = elem (toUpper x) hexChars where

6161 hexChars : List Char

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

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

6464

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

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

6666isOctDigit : Char -> Bool

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

6868

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

69+

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

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

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

2121

2222-- ---------------------------------------------------------- [ Equality Class ]

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

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

2424class Eq a where

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

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

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

6565 GT == GT = True

6666 _ == _ = False

6767

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

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

6969class Eq a => Ord a where

7070 compare : a -> a -> Ordering

7171

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

131131 else compare xr yr

132132

133133-- --------------------------------------------------------- [ Numerical Class ]

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

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

135135class Num a where

136136 (+) : a -> a -> a

137137 (-) : a -> a -> a

138138 (*) : a -> a -> a

139− -- | Absolute value

139+ ||| Absolute value

140140 abs : a -> a

141− -- | Conversion from Integer.

141+ ||| Conversion from Integer.

142142 fromInteger : Integer -> a

143143

144144instance Num Integer where

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

245245-- ------------------------------------------------------------- [ Bounded ]

246246

247247class MinBound b where

248− -- | The lower bound for the type

248+ ||| The lower bound for the type

249249 minBound : b

250250

251251class MaxBound b where

252− -- | The upper bound for the type

252+ ||| The upper bound for the type

253253 maxBound : b

254254

255255instance MinBound Bits16 where

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

273273

274274-- ------------------------------------------------------------- [ Fractionals ]

275275

276−-- | Fractional division of two Floats.

276+||| Fractional division of two Floats.

277277(/) : Float -> Float -> Float

278278(/) = prim__divFloat

279279

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

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

1−module Prelude.Either

1+ module Prelude.Either

22

33import Builtins

44

55import Prelude.Maybe

66import Prelude.List

77

8−data Either a b

9− = Left a

10− | Right b

8+||| A sum type

9+data Either a b =

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

11+ Left a |

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

13+ Right b

1114

1215--------------------------------------------------------------------------------

1316-- Syntactic tests

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

2528-- Misc.

2629--------------------------------------------------------------------------------

2730

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

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

2933choose True = Left oh

3034choose False = Right oh

3135

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

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

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

3341either l r (Left x) = l x

3442either l r (Right x) = r x

3543

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

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

55

66%default total

77

8−data Fin : Nat -> Type where

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

9+||| @ n the upper bound

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

911 fZ : Fin (S k)

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

1113

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

4446instance Cast (Fin n) Integer where

4547 cast x = finToInteger x

4648

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

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

4851weaken fZ = fZ

4952weaken (fS k) = fS (weaken k)

5053

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

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

5256weakenN n fZ = fZ

5357weakenN n (fS f) = fS (weakenN n f)

5458

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

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

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

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

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

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

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

6066strengthen f = Left f

6167

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

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

6372shift Z f = f

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

6574

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

6676last : Fin (S n)

6777last {n=Z} = fZ

6878last {n=S _} = fS last

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

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

11module Prelude.Functor

22

3+||| Functors

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

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

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

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

7+ ||| @ f the functor

8+ ||| @ m the morphism

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

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

270270intercalate sep l = concat $ intersperse sep l

271271

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

273−--

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

275−--

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

277−-- involution does not always hold:

278−--

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

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

281−--

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

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

273+|||

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

275+|||

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

277+||| involution does not always hold:

278+|||

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

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

281+|||

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

283283%assert_total

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

285285transpose [] = []

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

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

1010%access public

1111%default total

1212

13−%elim data Nat

14− = Z

15− | S Nat

13+||| Unary natural numbers

14+%elim data Nat =

15+ ||| Zero

16+ Z |

17+ ||| Successor

18+ S Nat

1619

1720-- name hints for interactive editing

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

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

3336-- Basic arithmetic functions

3437--------------------------------------------------------------------------------

3538

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

39+||| Add two natural numbers.

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

41+||| @ m the other number

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

3743plus Z right = right

3844plus (S left) right = S (plus left right)

3945

46+||| Multiply natural numbers

4047total mult : Nat -> Nat -> Nat

4148mult Z right = Z

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

4350

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

4452fromIntegerNat : Integer -> Nat

4553fromIntegerNat 0 = Z

4654fromIntegerNat n =

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

4957 else

5058 Z

5159

60+||| Convert a Nat to an Integer

5261toIntegerNat : Nat -> Integer

5362toIntegerNat Z = 0

5463toIntegerNat (S k) = 1 + toIntegerNat k

5564

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

5666total minus : Nat -> Nat -> Nat

5767minus Z right = Z

5868minus left Z = left

5969minus (S left) (S right) = minus left right

6070

71+||| Exponentiation of natural numbers

6172total power : Nat -> Nat -> Nat

6273power base Z = S Z

6374power 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)

7485-- Comparisons

7586--------------------------------------------------------------------------------

7687

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

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

89+||| @ n the smaller number

90+||| @ m the larger number

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

92+ ||| Zero is the smallest Nat

7893 lteZero : LTE Z right

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

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

8096

97+||| Greater than or equal to

8198total GTE : Nat -> Nat -> Type

8299GTE left right = LTE right left

83100

101+||| Strict less than

84102total LT : Nat -> Nat -> Type

85103LT left right = LTE (S left) right

86104

105+||| Strict greater than

87106total GT : Nat -> Nat -> Type

88107GT left right = LT right left

89108

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

90110total lte : Nat -> Nat -> Bool

91111lte Z right = True

92112lte left Z = False

93113lte (S left) (S right) = lte left right

94114

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

95116total gte : Nat -> Nat -> Bool

96117gte left right = lte right left

97118

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

98120total lt : Nat -> Nat -> Bool

99121lt left right = lte (S left) right

100122

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

101124total gt : Nat -> Nat -> Bool

102125gt left right = lt right left

103126

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

104128total minimum : Nat -> Nat -> Nat

105129minimum left right =

106130 if lte left right then

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

108132 else

109133 right

110134

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

111136total maximum : Nat -> Nat -> Nat

112137maximum left right =

113138 if lte left right then

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

148173instance Cast Integer Nat where

149174 cast = fromInteger

150175

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

151177record Multiplicative : Type where

152178 getMultiplicative : Nat -> Multiplicative

153179

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

154181record Additive : Type where

155182 getAdditive : Nat -> Additive

156183

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

210237-- Auxilliary notions

211238--------------------------------------------------------------------------------

212239

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

213241total pred : Nat -> Nat

214242pred Z = Z

215243pred (S n) = n

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

218246-- Fibonacci and factorial

219247--------------------------------------------------------------------------------

220248

249+||| Fibonacci numbers

221250total fib : Nat -> Nat

222251fib Z = Z

223252fib (S Z) = S Z

224253fib (S (S n)) = fib (S n) + fib n

225254

255+||| Factorial function

226256total fact : Nat -> Nat

227257fact Z = S Z

228258fact (S n) = (S n) * fact n

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

283313--------------------------------------------------------------------------------

284314

285315-- Succ

316+

317+||| S preserves equality

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

287319 S left = S right

288320eqSucc left _ refl = refl

289321

322+||| S is injective

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

291324 left = right

292325succInjective left _ refl = refl

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

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

66%access public

77%default total

88

9+||| An infinite stream

910codata Stream : Type -> Type where

1011 (::) : a -> Stream a -> Stream a

1112

1213instance Functor Stream where

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

1415

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

1517head : Stream a -> a

1618head (x::xs) = x

1719

20+||| All but the first element

1821tail : Stream a -> Stream a

1922tail (x::xs) = xs

2023

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

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

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

26+||| @ xs the stream

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

2228take Z _ = []

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

2430

2531%assert_total

2632drop : Nat -> Stream a -> Stream a

27−drop Z xs = xs

33+drop Z xs = xs

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

2935

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

3037repeat : a -> Stream a

3138repeat x = x :: repeat x

3239

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

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

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

3444iterate f x = x :: iterate f (f x)

3545

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

3647index : Nat -> Stream a -> a

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

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

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

3950

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

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

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

4254

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

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

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

4558

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

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

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

4862

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

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

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

5166

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

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

77import Prelude.Either

88import Prelude.Foldable

99

10−-- | Appends two strings together.

10+||| Appends two strings together.

1111(++) : String -> String -> String

1212(++) = prim__concat

1313

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

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

1515partial

1616strHead : String -> Char

1717strHead = prim__strHead

1818

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

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

2020partial

2121strTail : String -> String

2222strTail = prim__strTail

2323

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

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

2525strCons : Char -> String -> String

2626strCons = prim__strCons

2727

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

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

2929partial

3030strIndex : String -> Int -> Char

3131strIndex = prim__strIndex

3232

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

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

3434reverse : String -> String

3535reverse = prim__strRev

3636

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

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

11module Prelude.Uninhabited

22

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

34class Uninhabited t where

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

6+ ||| @ t the uninhabited type

47 total uninhabited : t -> _|_

58

69instance Uninhabited (Fin Z) where

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

1013instance Uninhabited (Z = S n) where

1114 uninhabited refl impossible

1215

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

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

15−absurd t = FalseElim (uninhabited t)

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

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

21+absurd h = FalseElim (uninhabited h)

samples/reflection.idr+25−25

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

22

33import Language.Reflection

44

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

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

66reflectVal : TT

77reflectVal = ?valPrf

88

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

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

1010applyTac1 : Int

1111applyTac1 = ?tacPrf1

1212

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

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

1414applyTac0 : Int

1515applyTac0 = ?tacPrf0

1616

17−-- | intEq for the two arguments

17+||| intEq for the two arguments

1818applyTacDyn : Int -> Int -> Int

1919applyTacDyn x y = ?tacPrfDyn

2020

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

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

2222fill : Int

2323fill = ?fillPrf

2424

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

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

2626envTuple : Type

2727envTuple = ?envTuplePrf

2828

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

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

3030envList : List (TTName, TT)

3131envList = ?envListPrf

3232

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

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

3434tupleType : Raw

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

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

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

3838

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

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

4040mkTuple : Raw

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

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

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

4444

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

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

4646nil : Raw

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

4848

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

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

5050cons : Raw

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

5252

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

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

55−-- demo purposes.

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

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

55+||| demo purposes.

5656intEq : Int -> Int -> Int

5757intEq x y = case x == y of

5858 True => 1

5959 False => 0

6060

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

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

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

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

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

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

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

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

6767

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

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

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

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

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

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

7373

74−-- | Returns the reflected representation of innerTac

74+||| Returns the reflected representation of innerTac

7575innerTacTT : TT

7676innerTacTT = ?innerTacTTPrf

7777

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

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

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

8080dispatch xs _ = ApplyTactic (innerTacTT)

8181

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

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

8383tacticalDispatch : Int -> Int

8484tacticalDispatch = ?tacticalDispatchPrf

8585

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

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

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

8888studyGoalTac _ goal = Reflect goal

8989

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

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

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

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

9292studyGoal : TT

9393studyGoal = ?studyGoalPrf

9494

src/Idris/AbsSyntax.hs+53−52

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

262262addCoercion n = do i <- getIState

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

264264

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

266−addDocStr n doc

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

266+addDocStr n doc args

267267 = 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) }

269269

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

271271addNameHint ty n

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

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

10001000 IState ->

10011001 (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)

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

10041004 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))

10061006 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)

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

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

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

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

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

10511051 bnames _ = []

10521052

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

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

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

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

10551055 where

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

10571057 -- added implicitly)

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

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

10611061 (map econ cons)

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

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

1064− = (doc, 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)

1066− = if tn `elem` ns

1063+ econ (doc, argDocs, n, 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)

1066+ = if tn `elem` ns

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

10681068 cdoc (dec cn) conty

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

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

11251125 pri Placeholder = 1

11261126 pri _ = 3

11271127

1128+

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

11291130addStatics n tm ptm =

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

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

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

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

11601161 -- resolved by searching.

1161− searchArg (Constraint _ _ _) = True

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

1162+ searchArg (Constraint _ _) = True

1163+ searchArg (TacImp _ _ _) = True

11631164 searchArg _ = False

11641165

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

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

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

11871188 doAdd (UConstraint c args : cs) ns t

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

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

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

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

11911192 | otherwise = doAdd cs ns t

11921193

11931194 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)

11951196

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

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

11971198 = getcapp c ++ getConstraints sc

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

11991200 getConstraints _ = []

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

12031204 return (UConstraint c ns)

12041205 getcapp _ = []

12051206

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

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

12071208 getName _ = []

12081209

12091210-- 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) $

12531254 = do (decls, ns) <- get

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

12551256 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)

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

12581259 (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,

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

12611262 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)

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

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

12651266 _ -> [])

12661267 (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,

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

12691270 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)

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

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

12731274 _ -> [])

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

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

1276+ put (PConstraint 10 l Placeholder : decls,

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

12771278 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)

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

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

12811282 _ -> [])

12821283 (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,

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

12851286 imps True (n:env) sc

12861287 imps top env (PEq _ l r)

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

13211322 pibind using [] sc = sc

13221323 pibind using (n:ns) sc

13231324 = case lookup n using of

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

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

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

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

13261327 (pibind using ns sc)

13271328

13281329-- Add implicit arguments in function calls

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

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

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

14401441 else Right $ PPatvar fc f

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

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

14421443 imp _ = True

14431444-- allImp [] = False

14441445 allImp xs = all imp xs

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

14871488

14881489

14891490 insertImpl :: [PArg] -> [PArg] -> [PArg]

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

1491− PExp p l tm d : insertImpl ps given

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

1493− PConstraint p l tm d : insertImpl ps given

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

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

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

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

1492+ PExp p l tm : insertImpl ps given

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

1494+ PConstraint p l tm : insertImpl ps given

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

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

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

14971498 case find n given [] of

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

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

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

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

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

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

15011502 let sc = addImpl ist sc' in

15021503 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'

15041505 Nothing -> if inpat

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

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

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

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

15071508 insertImpl expected [] = []

15081509 insertImpl _ given = given

15091510

15101511 find n [] acc = Nothing

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

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

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

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

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

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

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

15161517

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

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

15411542 args' <- mapM slA args

15421543 return $ PApp fc fn' args'

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

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

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

1546− return $ PExp p l t' d

1547− slA (PConstraint p l t d)

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

1545+ return $ PImp p m l n t'

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

1547+ return $ PExp p l t'

1548+ slA (PConstraint p l t)

15481549 = do t' <- sl t

1549− return $ PConstraint p l t' d

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

1550+ return $ PConstraint p l t'

1551+ slA (PTacImplicit p l n sc t)

15511552 = do t' <- sl t

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

1553+ return $ PTacImplicit p l n sc t'

15531554 sl x = return x

15541555

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

src/Idris/AbsSyntaxTree.hs+66−74

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

111111 idris_flags :: Ctxt [FnOpt],

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

113113 idris_calledgraph :: Ctxt [Name],

114− idris_docstrings :: Ctxt String,

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

115115 idris_tyinfodata :: Ctxt TIData,

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

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

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

381381-- Mark bindings with their explicitness, and laziness

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

383383 pstatic :: Static,

384− pdocstr :: String,

385384 pparam :: Bool }

386385 | Exp { pargopts :: [ArgOpt],

387386 pstatic :: Static,

388− pdocstr :: String,

389387 pparam :: Bool }

390388 | Constraint { pargopts :: [ArgOpt],

391− pstatic :: Static,

392− pdocstr :: String }

389+ pstatic :: Static }

393390 | TacImp { pargopts :: [ArgOpt],

394391 pstatic :: Static,

395− pscript :: PTerm,

396− pdocstr :: String }

392+ pscript :: PTerm }

397393 deriving (Show, Eq)

398394

399395plazy :: Plicity -> Bool

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

404400deriving instance NFData Plicity

405401!-}

406402

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

408−expl = Exp [] Dynamic "" False

409−expl_param = Exp [] Dynamic "" True

410−constraint = Constraint [] Dynamic ""

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

403+impl = Imp [Lazy] Dynamic False

404+expl = Exp [] Dynamic False

405+expl_param = Exp [] Dynamic True

406+constraint = Constraint [] Dynamic

407+tacimpl t = TacImp [] Dynamic t

412408

413409data FnOpt = Inlinable -- always evaluate when simplifying

414410 | TotalFn | PartialFn

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

454450-- datatypes and typeclasses.

455451data PDecl' t

456452 = 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

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

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

460456 | 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.

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

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

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

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

516512-- | Data declaration

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

518514 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

520516 }

521517 -- ^ Data declaration

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

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

538534

539535declared :: PDecl -> [Name]

540536declared (PFix _ _ _) = []

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

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

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

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

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

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

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

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

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

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

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

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

549545declared (PNamespace _ ds) = concatMap declared ds

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

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

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

559555tldeclared :: PDecl -> [Name]

560556tldeclared (PFix _ _ _) = []

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

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

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

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

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

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

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

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

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

567563tldeclared (PParams _ _ ds) = []

568564tldeclared (PMutual _ ds) = concatMap tldeclared ds

569565tldeclared (PNamespace _ ds) = concatMap tldeclared ds

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

573569

574570defined :: PDecl -> [Name]

575571defined (PFix _ _ _) = []

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

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

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

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

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

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

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

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

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

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

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

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

584580defined (PNamespace _ ds) = concatMap defined ds

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

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

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

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

768764 argopts :: [ArgOpt],

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

770− pargdoc :: String }

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

771766 | PExp { priority :: Int,

772767 argopts :: [ArgOpt],

773− getTm :: t,

774− pargdoc :: String }

768+ getTm :: t }

775769 | PConstraint { priority :: Int,

776770 argopts :: [ArgOpt],

777− getTm :: t,

778− pargdoc :: String }

771+ getTm :: t }

779772 | PTacImplicit { priority :: Int,

780773 argopts :: [ArgOpt],

781774 pname :: Name,

782775 getScript :: t,

783− getTm :: t,

784− pargdoc :: String }

776+ getTm :: t }

785777 deriving (Show, Eq, Functor)

786778

787779data ArgOpt = Lazy | HideDisplay

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

791783lazyarg tm = Lazy `elem` argopts tm

792784

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

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

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

796− size (PConstraint p l trm _) = 1 + size trm

797− size (PTacImplicit p l nm scr trm _) = 1 + size nm + size scr + size trm

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

787+ size (PExp p l trm) = 1 + size trm

788+ size (PConstraint p l trm) = 1 + size trm

789+ size (PTacImplicit p l nm scr trm) = 1 + size nm + size scr + size trm

798790

799791{-!

800792deriving instance Binary PArg'

801793deriving instance NFData PArg'

802794!-}

803795

804−pimp n t mach = PImp 1 mach [Lazy] n t ""

805−pexp t = PExp 1 [] t ""

806−pconst t = PConstraint 1 [] t ""

807−ptacimp n s t = PTacImplicit 2 [Lazy] n s t ""

796+pimp n t mach = PImp 1 mach [Lazy] n t

797+pexp t = PExp 1 [] t

798+pconst t = PConstraint 1 [] t

799+ptacimp n s t = PTacImplicit 2 [Lazy] n s t

808800

809801type PArg = PArg' PTerm

810802

@@ -956,9 +948,9 @@ inferTy = sMN 0 "__Infer"

956948inferCon = sMN 0 "__infer"

957949inferDecl = PDatadecl inferTy

958950 PType

959− [("", inferCon, PPi impl (sMN 0 "iType") PType (

960− PPi expl (sMN 0 "ival") (PRef bi (sMN 0 "iType"))

961− (PRef bi inferTy)), bi, [])]

951+ [("", [], inferCon, PPi impl (sMN 0 "iType") PType (

952+ PPi expl (sMN 0 "ival") (PRef bi (sMN 0 "iType"))

953+ (PRef bi inferTy)), bi, [])]

962954inferOpts = []

963955

964956infTerm t = PApp bi (PRef bi inferCon) [pimp (sMN 0 "iType") Placeholder True, pexp t]

@@ -986,7 +978,7 @@ primNames = [unitTy, unitCon,

986978unitTy = sMN 0 "__Unit"

987979unitCon = sMN 0 "__II"

988980unitDecl = PDatadecl unitTy PType

989− [("", unitCon, PRef bi unitTy, bi, [])]

981+ [("", [], unitCon, PRef bi unitTy, bi, [])]

990982unitOpts = [DefaultEliminator]

991983

992984falseTy = sMN 0 "__False"

@@ -996,12 +988,12 @@ falseOpts = []

996988pairTy = sMN 0 "__Pair"

997989pairCon = sMN 0 "__MkPair"

998990pairDecl = PDatadecl pairTy (piBind [(n "A", PType), (n "B", PType)] PType)

999− [("", pairCon, PPi impl (n "A") PType (

1000− PPi impl (n "B") PType (

1001− PPi expl (n "a") (PRef bi (n "A")) (

1002− PPi expl (n "b") (PRef bi (n "B"))

1003− (PApp bi (PRef bi pairTy) [pexp (PRef bi (n "A")),

1004− pexp (PRef bi (n "B"))])))), bi, [])]

991+ [("", [], pairCon, PPi impl (n "A") PType (

992+ PPi impl (n "B") PType (

993+ PPi expl (n "a") (PRef bi (n "A")) (

994+ PPi expl (n "b") (PRef bi (n "B"))

995+ (PApp bi (PRef bi pairTy) [pexp (PRef bi (n "A")),

996+ pexp (PRef bi (n "B"))])))), bi, [])]

1005997 where n a = sMN 0 a

1006998pairOpts = []

1007999

@@ -1010,12 +1002,12 @@ eqCon = sUN "refl"

10101002eqDecl = PDatadecl eqTy (piBind [(n "A", PType), (n "B", PType),

10111003 (n "x", PRef bi (n "A")), (n "y", PRef bi (n "B"))]

10121004 PType)

1013− [("", eqCon, PPi impl (n "A") PType (

1014− PPi impl (n "x") (PRef bi (n "A"))

1015− (PApp bi (PRef bi eqTy) [pimp (n "A") Placeholder False,

1016− pimp (n "B") Placeholder False,

1017− pexp (PRef bi (n "x")),

1018− pexp (PRef bi (n "x"))])), bi, [])]

1005+ [("", [], eqCon, PPi impl (n "A") PType (

1006+ PPi impl (n "x") (PRef bi (n "A"))

1007+ (PApp bi (PRef bi eqTy) [pimp (n "A") Placeholder False,

1008+ pimp (n "B") Placeholder False,

1009+ pexp (PRef bi (n "x")),

1010+ pexp (PRef bi (n "x"))])), bi, [])]

10191011 where n a = sMN 0 a

10201012eqOpts = []

10211013

@@ -1023,8 +1015,8 @@ elimName = sUN "__Elim"

10231015elimMethElimTy = sUN "__elimTy"

10241016elimMethElim = sUN "elim"

10251017elimDecl = PClass "Type class for eliminators" defaultSyntax bi [] elimName [(sUN "scrutineeType", PType)]

1026− [PTy "" defaultSyntax bi [TotalFn] elimMethElimTy PType,

1027− PTy "" defaultSyntax bi [TotalFn] elimMethElim (PRef bi elimMethElimTy)]

1018+ [PTy "" [] defaultSyntax bi [TotalFn] elimMethElimTy PType,

1019+ PTy "" [] defaultSyntax bi [TotalFn] elimMethElim (PRef bi elimMethElimTy)]

10281020

10291021-- Defined in builtins.idr

10301022sigmaTy = sUN "Exists"

@@ -1108,7 +1100,7 @@ pprintPTerm impl bnd = prettySe 10 bnd

11081100 text "let" <+> bindingOf n False <+> text "=" </>

11091101 prettySe 10 bnd v <+> text "in" </>

11101102 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)

11121104 | n `elem` allNamesIn sc || impl =

11131105 let open = if Lazy `elem` l then text "|" <> lparen else lparen in

11141106 bracket p 2 . group $

@@ -1122,7 +1114,7 @@ pprintPTerm impl bnd = prettySe 10 bnd

11221114 case s of

11231115 Static -> text "[static]" <> space

11241116 _ -> empty

1125− prettySe p bnd (PPi (Imp l s _ _) n ty sc)

1117+ prettySe p bnd (PPi (Imp l s _) n ty sc)

11261118 | impl =

11271119 let open = if Lazy `elem` l then text "|" <> lbrace else lbrace in

11281120 bracket p 2 $

@@ -1134,10 +1126,10 @@ pprintPTerm impl bnd = prettySe 10 bnd

11341126 case s of

11351127 Static -> text "[static]" <> space

11361128 _ -> empty

1137− prettySe p bnd (PPi (Constraint _ _ _) n ty sc) =

1129+ prettySe p bnd (PPi (Constraint _ _) n ty sc) =

11381130 bracket p 2 $

11391131 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) =

11411133 bracket p 2 $

11421134 lbrace <> text "tacimp" <+> pretty n <+> colon <+> prettySe 10 bnd ty <>

11431135 rbrace <+> text "->" </> prettySe 10 ((n, True):bnd) sc

@@ -1254,10 +1246,10 @@ pprintPTerm impl bnd = prettySe 10 bnd

12541246

12551247 prettySe p bnd _ = text "test"

12561248

1257− prettyArgS bnd (PImp _ _ _ n tm _) = prettyArgSi bnd (n, tm)

1258− prettyArgS bnd (PExp _ _ tm _) = prettyArgSe bnd tm

1259− prettyArgS bnd (PConstraint _ _ tm _) = prettyArgSc bnd tm

1260− prettyArgS bnd (PTacImplicit _ _ n _ tm _) = prettyArgSti bnd (n, tm)

1249+ prettyArgS bnd (PImp _ _ _ n tm) = prettyArgSi bnd (n, tm)

1250+ prettyArgS bnd (PExp _ _ tm) = prettyArgSe bnd tm

1251+ prettyArgS bnd (PConstraint _ _ tm) = prettyArgSc bnd tm

1252+ prettyArgS bnd (PTacImplicit _ _ n _ tm) = prettyArgSti bnd (n, tm)

12611253

12621254 prettyArgSe bnd arg = prettySe 0 bnd arg

12631255 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)

13531345showDImp :: Bool -> PData -> Doc OutputAnnotation

13541346showDImp impl (PDatadecl n ty cons)

13551347 = 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))

13571349

13581350showDecls :: Bool -> [PDecl] -> Doc OutputAnnotation

13591351showDecls i ds = vsep (map (showDeclImp i) ds)

13601352

13611353showDeclImp _ (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

13631355showDeclImp i (PClauses _ _ n cs) = text "pat" <+> text (showCG n) <+> text "\t" <+>

13641356 indent 2 (vsep (map (showCImp i) cs))

1365−showDeclImp _ (PData _ _ _ _ d) = showDImp True d

1357+showDeclImp _ (PData _ _ _ _ _ d) = showDImp True d

13661358showDeclImp i (PParams _ ns ps) = text "params" <+> braces (text (show ns) <> line <> showDecls i ps <> line)

13671359showDeclImp i (PNamespace n ps) = text "namespace" <+> text n <> braces (line <> showDecls i ps <> line)

13681360showDeclImp _ (PSyntax _ syn) = text "syntax" <+> text (show syn)

@@ -1378,17 +1370,17 @@ instance Show (Doc OutputAnnotation) where

13781370

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

13801372getImps [] = []

1381−getImps (PImp _ _ _ n tm _ : xs) = (n, tm) : getImps xs

1373+getImps (PImp _ _ _ n tm : xs) = (n, tm) : getImps xs

13821374getImps (_ : xs) = getImps xs

13831375

13841376getExps :: [PArg] -> [PTerm]

13851377getExps [] = []

1386−getExps (PExp _ _ tm _ : xs) = tm : getExps xs

1378+getExps (PExp _ _ tm : xs) = tm : getExps xs

13871379getExps (_ : xs) = getExps xs

13881380

13891381getConsts :: [PArg] -> [PTerm]

13901382getConsts [] = []

1391−getConsts (PConstraint _ _ tm _ : xs) = tm : getConsts xs

1383+getConsts (PConstraint _ _ tm : xs) = tm : getConsts xs

13921384getConsts (_ : xs) = getConsts xs

13931385

13941386getAll :: [PArg] -> [PTerm]

src/Idris/CaseSplit.hs+4−4

@@ -150,7 +150,7 @@ mergePat ist (PApp _ _ args) (PApp fc f args') t

150150 where mergeArg x (y, t)

151151 = do tm' <- mergePat ist (getTm x) (getTm y) t

152152 case x of

153− (PImp _ _ _ _ _ _) ->

153+ (PImp _ _ _ _ _) ->

154154 return (y { machine_inf = machine_inf x,

155155 getTm = tm' })

156156 _ -> return (y { getTm = tm' })

@@ -318,14 +318,14 @@ getClause l fn fp = do ty <- getInternalApp fp l

318318 let ap = mkApp ist ty []

319319 return (show fn ++ " " ++ ap ++

320320 "= ?" ++ 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

322322 = let n = getNameFrom i used ty in

323323 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

325325 | thead n == '_'

326326 = let n = getNameFrom i used ty in

327327 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

329329 = show n ++ " " ++ mkApp i sc (n : used)

330330 mkApp i (PPi _ _ _ sc) used = mkApp i sc used

331331 mkApp i _ _ = ""

src/Idris/Coverage.hs+2−2

@@ -56,7 +56,7 @@ genClauses fc n xs given

5656 -- there may be more case splitting that the idris_implicits record

5757 -- suggests)

5858 let parg = case lookupCtxt n (idris_implicits i) of

59− (p : _) -> p ++ repeat (PExp 0 [] Placeholder "")

59+ (p : _) -> p ++ repeat (PExp 0 [] Placeholder)

6060 _ -> repeat (pexp Placeholder)

6161 let tryclauses = mkClauses parg all_args

6262 logLvl 2 $ show (length tryclauses) ++ " initially to check"

@@ -187,7 +187,7 @@ genAll i args

187187 _ -> [p]

188188 ops fc n arg o = return Placeholder

189189

190− getExpTm (PImp _ True _ _ _ _) = Placeholder -- machine inferred, no point!

190+ getExpTm (PImp _ True _ _ _) = Placeholder -- machine inferred, no point!

191191 getExpTm t = getTm t

192192

193193 -- put it back to its original form

src/Idris/DeepSeq.hs+21−20

@@ -57,14 +57,14 @@ instance NFData ArgOpt where

5757 rnf _ = ()

5858

5959instance NFData Plicity where

60− rnf (Imp x1 x2 x3 x4)

61− = rnf x1 `seq` rnf x2 `seq` rnf x3 `seq` rnf x4 `seq` ()

62− rnf (Exp x1 x2 x3 x4)

63− = rnf x1 `seq` rnf x2 `seq` rnf x3 `seq` rnf x4 `seq` ()

64− rnf (Constraint x1 x2 x3)

60+ rnf (Imp x1 x2 x3)

61+ = rnf x1 `seq` rnf x2 `seq` rnf x3 `seq` ()

62+ rnf (Exp x1 x2 x3)

63+ = rnf x1 `seq` rnf x2 `seq` rnf x3 `seq` ()

64+ rnf (Constraint x1 x2)

65+ = rnf x1 `seq` rnf x2 `seq` ()

66+ rnf (TacImp x1 x2 x3)

6567 = 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` ()

6868

6969instance NFData FnOpt where

7070 rnf Inlinable = ()

@@ -84,18 +84,20 @@ instance NFData DataOpt where

8484

8585instance (NFData t) => NFData (PDecl' t) where

8686 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)

8888 = rnf x1 `seq`

89− rnf x2 `seq` rnf x3 `seq` rnf x4 `seq` rnf x5 `seq` rnf x6 `seq` ()

89+ rnf x2 `seq`

90+ rnf x3 `seq` rnf x4 `seq` rnf x5 `seq` rnf x6 `seq` rnf x7 `seq` ()

9091 rnf (PPostulate x1 x2 x3 x4 x5 x6)

9192 = rnf x1 `seq`

9293 rnf x2 `seq` rnf x3 `seq` rnf x4 `seq` rnf x5 `seq` rnf x6 `seq` ()

9394 rnf (PClauses x1 x2 x3 x4)

9495 = rnf x1 `seq` rnf x2 `seq` rnf x3 `seq` rnf x4 `seq` ()

9596 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)

9798 = rnf x1 `seq`

98− rnf x2 `seq` rnf x3 `seq` rnf x4 `seq` rnf x5 `seq` ()

99+ rnf x2 `seq`

100+ rnf x3 `seq` rnf x4 `seq` rnf x5 `seq` rnf x6 `seq` ()

99101 rnf (PParams x1 x2 x3) = rnf x1 `seq` rnf x2 `seq` rnf x3 `seq` ()

100102 rnf (PNamespace x1 x2) = rnf x1 `seq` rnf x2 `seq` ()

101103 rnf (PRecord x1 x2 x3 x4 x5 x6 x7 x8)

@@ -230,16 +232,15 @@ instance (NFData t) => NFData (PDo' t) where

230232 rnf (DoLetP x1 x2 x3) = rnf x1 `seq` rnf x2 `seq` rnf x3 `seq` ()

231233

232234instance (NFData t) => NFData (PArg' t) where

233− rnf (PImp x1 x2 x3 x4 x5 x6)

234− = rnf x1 `seq`

235− rnf x2 `seq` rnf x3 `seq` rnf x4 `seq` rnf x5 `seq` rnf x6 `seq` ()

236− rnf (PExp x1 x2 x3 x4)

237− = rnf x1 `seq` rnf x2 `seq` rnf x3 `seq` rnf x4 `seq` ()

238− rnf (PConstraint x1 x2 x3 x4)

239− = rnf x1 `seq` rnf x2 `seq` rnf x3 `seq` rnf x4 `seq` ()

240− rnf (PTacImplicit x1 x2 x3 x4 x5 x6)

235+ rnf (PImp x1 x2 x3 x4 x5)

236+ = rnf x1 `seq` rnf x2 `seq` rnf x3 `seq` rnf x4 `seq` rnf x5 `seq` ()

237+ rnf (PExp x1 x2 x3)

238+ = rnf x1 `seq` rnf x2 `seq` rnf x3 `seq` ()

239+ rnf (PConstraint x1 x2 x3)

240+ = rnf x1 `seq` rnf x2 `seq` rnf x3 `seq` ()

241+ rnf (PTacImplicit x1 x2 x3 x4 x5)

241242 = 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` ()

243244

244245instance NFData ClassInfo where

245246 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

5656 _ -> PRef un n

5757 de env _ (Bind n (Lam ty) sc)

5858 = PLam n (de env [] ty) (de ((n,n):env) [] sc)

59− de env (PImp _ _ _ _ _ _:is) (Bind n (Pi ty) sc)

60− = PPi impl n (de env [] ty) (de ((n,n):env) is sc)

61− de env (PConstraint _ _ _ _:is) (Bind n (Pi ty) sc)

59+ de env ((PImp { argopts = opts }):is) (Bind n (Pi ty) 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)

6262 = 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)

6464 = PPi (tacimpl tac) n (de env [] ty) (de ((n,n):env) is sc)

65− de env _ (Bind n (Pi ty) 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)

70+ de env [] (Bind n (Pi ty) sc)

6671 = PPi expl n (de env [] ty) (de ((n,n):env) [] sc)

6772 de env _ (Bind n (Let ty val) sc)

6873 = PLet n (de env [] ty) (de env [] val) (de ((n,n):env) [] sc)

6974 de env _ (Bind n (Hole ty) sc) = de ((n, sUN "[__]"):env) [] sc

7075 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

7277 de env _ (Constant i) = PConstant i

7378 de env _ Erased = Placeholder

7479 de env _ Impossible = Placeholder

@@ -112,10 +117,10 @@ delabTy' ist imps tm fullname mvs = de [] imps tm

112117 = PApp un (PRef un n) (zipWith imp (imps ++ repeat (pexp undefined)) args)

113118 | otherwise = PApp un (PRef un n) (map pexp args)

114119

115− imp (PImp p m l n _ d) arg = PImp p m l n arg d

116− imp (PExp p l _ d) arg = PExp p l arg d

117− imp (PConstraint p l _ d) arg = PConstraint p l arg d

118− imp (PTacImplicit p l n sc _ d) arg = PTacImplicit p l n sc arg d

120+ imp (PImp p m l n _) arg = PImp p m l n arg

121+ imp (PExp p l _) arg = PExp p l arg

122+ imp (PConstraint p l _) arg = PConstraint p l arg

123+ imp (PTacImplicit p l n sc _) arg = PTacImplicit p l n sc arg

119124

120125-- | How far to indent sub-errors

121126errorIndent :: Int

src/Idris/Docs.hs+33−21

@@ -14,15 +14,17 @@ import Data.List

1414-- TODO: Only include names with public/abstract accessibility

1515

1616data FunDoc = FD Name String

17− [(Name, PTerm, Plicity)] -- args: name, ty, plicity

17+ [(Name, PTerm, Plicity, Maybe String)] -- args: name, ty, implicit, docs

1818 PTerm -- function type

1919 (Maybe Fixity)

20+ deriving Show

2021

2122data Docs = FunDoc FunDoc

2223 | DataDoc FunDoc -- type constructor docs

2324 [FunDoc] -- data constructor docs

2425 | ClassDoc Name String -- class docs

2526 [FunDoc] -- method docs

27+ deriving Show

2628

2729showDoc "" = empty

2830showDoc x = text " -- " <> text x

@@ -31,23 +33,32 @@ pprintFD :: Bool -> FunDoc -> Doc OutputAnnotation

3133pprintFD imp (FD n doc args ty f)

3234 = nest 4 (prettyName imp [] n <+> colon <+> prettyImp imp ty <$> showDoc doc <$>

3335 maybe empty (\f -> text (show f) <> line) f <>

34− let argshow = mapMaybe showArg args in

36+ let argshow = showArgs args [] in

3537 if not (null argshow)

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

3739 else empty)

3840

39− where showArg (n, ty, arg@(Exp {}))

40− = Just $ bindingOf n False <+> colon <+> prettyImp imp ty <>

41− showDoc (pdocstr arg) <> line

42− showArg (n, ty, arg@(Constraint {}))

43− = Just $ text "Class constraint" <+>

44− prettyImp imp ty <> showDoc (pdocstr arg) <> line

45− showArg (n, ty, arg@(Imp {}))

41+ where showArgs ((n, ty, Exp {}, d):args) bnd

42+ = bindingOf n False <+> colon <+>

43+ pprintPTerm imp bnd ty <>

44+ showDoc (maybe "" id d) <> line

45+ :

46+ showArgs args ((n, False):bnd)

47+ showArgs ((n, ty, Constraint {}, d):args) bnd

48+ = text "Class constraint" <+>

49+ pprintPTerm imp bnd ty <> showDoc (maybe "" id d) <> line

50+ :

51+ showArgs args ((n, True):bnd)

52+ showArgs ((n, ty, Imp {}, d):args) bnd

4653 | not (null doc)

47− = Just $ text "(implicit)" <+>

48− bindingOf n True <+> colon <+> prettyImp imp ty

49− <> showDoc (pdocstr arg) <> line

50− showArg (n, _, _) = Nothing

54+ = text "(implicit)" <+>

55+ bindingOf n True <+> colon <+>

56+ pprintPTerm imp bnd ty <>

57+ showDoc (maybe "" id d) <> line

58+ :

59+ showArgs args ((n, True):bnd)

60+ showArgs ((n, _, _, _):args) bnd = showArgs args ((n, True):bnd)

61+ showArgs [] _ = []

5162

5263

5364

@@ -81,7 +92,7 @@ docClass :: Name -> ClassInfo -> Idris Docs

8192docClass n ci

8293 = do i <- getIState

8394 let docstr = case lookupCtxt n (idris_docstrings i) of

84− [str] -> str

95+ [str] -> fst str

8596 _ -> ""

8697 mdocs <- mapM docFun (map fst (class_methods ci))

8798 return (ClassDoc n docstr mdocs)

@@ -89,11 +100,11 @@ docClass n ci

89100docFun :: Name -> Idris FunDoc

90101docFun n

91102 = do i <- getIState

92− let docstr = case lookupCtxt n (idris_docstrings i) of

93− [str] -> str

94− _ -> ""

103+ let (docstr, argDocs) = case lookupCtxt n (idris_docstrings i) of

104+ [d] -> d

105+ _ -> ("", [])

95106 let ty = delabTy i n

96− let args = getPArgNames ty

107+ let args = getPArgNames ty argDocs

97108 let infixes = idris_infixes i

98109 let fixdecls = filter (\(Fix _ x) -> x == funName n) infixes

99110 let f = case fixdecls of

@@ -105,6 +116,7 @@ docFun n

105116 funName (UN n) = str n

106117 funName (NS n _) = funName n

107118

108−getPArgNames :: PTerm -> [(Name, PTerm, Plicity)]

109−getPArgNames (PPi plicity name ty body) = ((name, ty, plicity) : getPArgNames body)

110−getPArgNames _ = []

119+getPArgNames :: PTerm -> [(Name, String)] -> [(Name, PTerm, Plicity, Maybe String)]

120+getPArgNames (PPi plicity name ty body) ds =

121+ (name, ty, plicity, lookup name ds) : getPArgNames body ds

122+getPArgNames _ _ = []

src/Idris/ElabDecls.hs+86−71

@@ -63,15 +63,15 @@ checkAddDef add toplvl fc ((n, (i, top, t)) : ns)

6363-- return (n, (i, top, t'))) ns

6464

6565-- | Elaborate a top-level type declaration - for example, "foo : Int -> Int".

66−elabType :: ElabInfo -> SyntaxInfo -> String ->

66+elabType :: ElabInfo -> SyntaxInfo -> String -> [(Name, String)] ->

6767 FC -> FnOpts -> Name -> PTerm -> Idris Type

6868elabType = elabType' False

6969

7070elabType' :: Bool -> -- normalise it

71− ElabInfo -> SyntaxInfo -> String ->

71+ ElabInfo -> SyntaxInfo -> String -> [(Name, String)] ->

7272 FC -> FnOpts -> Name -> PTerm -> Idris Type

73−elabType' norm info syn doc fc opts n ty' = {- let ty' = piBind (params info) ty_in

74− n = liftname info n_in 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 -}

7575 do checkUndefined fc n

7676 ctxt <- getContext

7777 i <- getIState

@@ -122,7 +122,8 @@ elabType' norm info syn doc fc opts n ty' = {- let ty' = piBind (params info) ty

122122 let ds' = map (\(n, (i, top, t)) -> (n, (i, top, t, True))) ds

123123 addDeferred ds'

124124 setFlags n opts'

125− addDocStr n doc

125+ checkDocs fc argDocs ty

126+ addDocStr n doc argDocs

126127 addIBC (IBCDoc n)

127128 addIBC (IBCFlags n opts')

128129 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

167168 , ns2 == map txt ["Maybe", "Prelude"]

168169 , ns3 == map txt ["List", "Prelude"]

169170 , ns4 == map txt ["Errors","Reflection","Language"] = True

170− tyIsHandler _ = False

171+ tyIsHandler _ = False

171172

172173

173174elabPostulate :: ElabInfo -> SyntaxInfo -> String ->

174175 FC -> FnOpts -> Name -> PTerm -> Idris ()

175176elabPostulate 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

177178 -- make sure it's collapsible, so it is never needed at run time

178179 -- start by getting the elaborated type

179180 ctxt <- getContext

@@ -194,8 +195,8 @@ elabPostulate info syn doc fc opts n ty

194195 -- remove it from the deferred definitions list

195196 solveDeferred n

196197

197−elabData :: ElabInfo -> SyntaxInfo -> String -> FC -> DataOpts -> PData -> Idris ()

198−elabData info syn doc fc opts (PLaterdecl n t_in)

198+elabData :: ElabInfo -> SyntaxInfo -> String -> [(Name, String)] -> FC -> DataOpts -> PData -> Idris ()

199+elabData info syn doc argDocs fc opts (PLaterdecl n t_in)

199200 = do let codata = Codata `elem` opts

200201 iLOG (show (fc, doc))

201202 checkUndefined fc n

@@ -213,7 +214,7 @@ elabData info syn doc fc opts (PLaterdecl n t_in)

213214 logLvl 2 $ "---> " ++ show cty

214215 updateContext (addTyDecl n (TCon 0 0) cty) -- temporary, to check cons

215216

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)

217218 = do let codata = Codata `elem` opts

218219 iLOG (show fc)

219220 undef <- isUndefined fc n

@@ -241,12 +242,13 @@ elabData info syn doc fc opts (PDatadecl n t_in dcons)

241242 let as = map (const Nothing) (getArgTys cty)

242243 let params = findParams (map snd cons)

243244 logLvl 2 $ "Parameters : " ++ show params

244− putIState (i { idris_datatypes =

245+ putIState (i { idris_datatypes =

245246 addDef n (TI (map fst cons) codata opts params)

246247 (idris_datatypes i) })

247248 addIBC (IBCDef n)

248249 addIBC (IBCData n)

249− addDocStr n doc

250+ checkDocs fc argDocs t_in

251+ addDocStr n doc argDocs

250252 addIBC (IBCDoc n)

251253 let metainf = DataMI params

252254 addIBC (IBCMetaInformation n metainf)

@@ -258,10 +260,10 @@ elabData info syn doc fc opts (PDatadecl n t_in dcons)

258260 if DefaultEliminator `elem` opts then evalStateT (elabEliminator params n t dcons info) Map.empty

259261 else return ()

260262 where

261− checkDefinedAs fc n t ctxt

263+ checkDefinedAs fc n t ctxt

262264 = case lookupDef n ctxt of

263265 [] -> return ()

264− [TyDecl _ ty] ->

266+ [TyDecl _ ty] ->

265267 case converts ctxt [] t ty of

266268 OK () -> return ()

267269 _ -> tclift $ tfail (At fc (AlreadyDefined n))

@@ -319,7 +321,8 @@ elabData info syn doc fc opts (PDatadecl n t_in dcons)

319321type EliminatorState = StateT (Map.Map String Int) Idris

320322

321323-- 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])] ->

323326 ElabInfo -> EliminatorState ()

324327elabEliminator paramPos n ty cons info = do

325328 elimLog $ "Elaborating eliminator"

@@ -328,15 +331,15 @@ elabEliminator paramPos n ty cons info = do

328331 generalParams <- namePis False pms

329332 motiveIdxs <- namePis False idxs

330333 let motive = mkMotive n paramPos generalParams motiveIdxs

331− consTerms <- mapM (\(c@(_,cnm,_,_,_)) -> do

332− name <- freshName $ "elim_" ++ simpleName cnm

333− consTerm <- extractConsTerm c generalParams

334− return (name, expl, consTerm)) cons

334+ consTerms <- mapM (\(c@(_, _, cnm, _, _, _)) -> do

335+ name <- freshName $ "elim_" ++ simpleName cnm

336+ consTerm <- extractConsTerm c generalParams

337+ return (name, expl, consTerm)) cons

335338 scrutineeIdxs <- namePis False idxs

336339 let motiveConstr = [(motiveName, expl, motive)]

337340 let scrutinee = (scrutineeName, expl, applyCons n (interlievePos paramPos generalParams scrutineeIdxs 0))

338341 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

340343 let clauseConsElimArgs = map getPiName consTerms

341344 let clauseGeneralArgs' = map getPiName generalParams ++ [motiveName] ++ clauseConsElimArgs

342345 let clauseGeneralArgs = map (\arg -> pexp (PRef elimFC arg)) clauseGeneralArgs'

@@ -500,8 +503,8 @@ elabEliminator paramPos n ty cons info = do

500503 in return $ filter (\(n,_,_) -> not (n `elem` oldParams))implargs

501504 _ -> return implargs

502505

503− extractConsTerm :: (String, Name, PTerm, FC, [Name]) -> [(Name, Plicity, PTerm)] -> EliminatorState PTerm

504− extractConsTerm (doc, cnm, ty, fc, fs) generalParameters = do

506+ extractConsTerm :: (String, [(Name, String)], Name, PTerm, FC, [Name]) -> [(Name, Plicity, PTerm)] -> EliminatorState PTerm

507+ extractConsTerm (doc, argDocs, cnm, ty, fc, fs) generalParameters = do

505508 let cons' = replaceParams paramPos generalParameters ty

506509 let (args, resTy) = splitPi cons'

507510 implidxs <- implicitIndexes (doc, cnm, ty, fc, fs)

@@ -536,8 +539,8 @@ elabEliminator paramPos n ty cons info = do

536539 convertImplPi (PImp {getTm = t, pname = n}) = Just (n, expl, t)

537540 convertImplPi _ = Nothing

538541

539− generateEliminatorClauses :: (String, Name, PTerm, FC, [Name]) -> Name -> [PArg] -> [(Name, Plicity, PTerm)] -> EliminatorState PClause

540− generateEliminatorClauses (doc, cnm, ty, fc, fs) cnsElim generalArgs generalParameters = do

542+ generateEliminatorClauses :: (String, [(Name, String)], Name, PTerm, FC, [Name]) -> Name -> [PArg] -> [(Name, Plicity, PTerm)] -> EliminatorState PClause

543+ generateEliminatorClauses (doc, _, cnm, ty, fc, fs) cnsElim generalArgs generalParameters = do

541544 let cons' = replaceParams paramPos generalParameters ty

542545 let (args, resTy) = splitPi cons'

543546 i <- State.lift getIState

@@ -558,7 +561,7 @@ elabEliminator paramPos n ty cons info = do

558561

559562elabPrims :: Idris ()

560563elabPrims = 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)

562565 (zip

563566 [inferOpts, unitOpts, falseOpts, pairOpts, eqOpts]

564567 [inferDecl, unitDecl, falseDecl, pairDecl, eqDecl]))

@@ -662,7 +665,7 @@ elabProvider info syn fc what n ty tm

662665 Provide tm

663666 | what `elem` [ProvTerm, ProvAny] ->

664667 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

666669 elabClauses info fc [] n [PClause fc n (PApp fc (PRef fc n) []) [] (delab i tm) []]

667670 logLvl 1 $ "Elaborated provider " ++ show n ++ " as: " ++ show tm

668671 | otherwise ->

@@ -724,7 +727,7 @@ elabTransform info fc safe lhs_in rhs_in

724727elabRecord :: ElabInfo -> SyntaxInfo -> String -> FC -> Name ->

725728 PTerm -> String -> Name -> PTerm -> Idris ()

726729elabRecord 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, [])])

728731 cty' <- implicit syn cn cty

729732 i <- getIState

730733 cty <- case lookupTy cn (tt_ctxt i) of

@@ -747,7 +750,7 @@ elabRecord info syn doc fc tyn ty cdoc cn cty

747750 where

748751-- syn = syn_in { syn_namespace = show (nsroot tyn) : syn_namespace syn_in }

749752

750− isNonImp (PExp _ _ _ _, a) = Just a

753+ isNonImp (PExp _ _ _, a) = Just a

751754 isNonImp _ = Nothing

752755

753756 tryElabDecl info (fn, ty, val)

@@ -759,15 +762,15 @@ elabRecord info syn doc fc tyn ty cdoc cn cty

759762 show fn ++ " (" ++ show ty ++ ")"

760763 putIState i)

761764

762− getImplB k (PPi (Imp l s _ _) n Placeholder sc)

765+ getImplB k (PPi (Imp l s _) n Placeholder sc)

763766 = getImplB k sc

764− getImplB k (PPi (Imp l s d p) n ty sc)

765− = getImplB (\x -> k (PPi (Imp l s d p) n ty x)) sc

767+ getImplB k (PPi (Imp l s p) n ty sc)

768+ = getImplB (\x -> k (PPi (Imp l s p) n ty x)) sc

766769 getImplB k (PPi _ n ty sc)

767770 = getImplB k sc

768771 getImplB k _ = k

769772

770− renameBs (PImp _ _ _ _ _ _ : ps) (PPi p n ty s)

773+ renameBs (PImp _ _ _ _ _ : ps) (PPi p n ty s)

771774 = PPi p (mkImp n) ty (renameBs ps (substMatch n (PRef fc (mkImp n)) s))

772775 renameBs (_:ps) (PPi p n ty s) = PPi p n ty (renameBs ps s)

773776 renameBs _ t = t

@@ -794,7 +797,7 @@ elabRecord info syn doc fc tyn ty cdoc cn cty

794797

795798 mkProj recty substs cimp ((pn_in, pty), pos)

796799 = do let pn = expandNS syn pn_in

797− let pfnTy = PTy "" defaultSyntax fc [] pn

800+ let pfnTy = PTy "" [] defaultSyntax fc [] pn

798801 (PPi expl rec recty

799802 (substMatches substs pty))

800803 let pls = repeat Placeholder

@@ -815,7 +818,7 @@ elabRecord info syn doc fc tyn ty cdoc cn cty

815818 let valname = sMN 0 "updateval"

816819 let pt = k (PPi expl pn pty

817820 (PPi expl rec recty recty))

818− let pfnTy = PTy "" defaultSyntax fc [] setname pt

821+ let pfnTy = PTy "" [] defaultSyntax fc [] setname pt

819822 let pls = map (\x -> PRef fc (sMN x "field")) [0..num-1]

820823 let lhsArgs = pls

821824 let rhsArgs = take pos pls ++ (PRef fc valname) :

@@ -831,8 +834,8 @@ elabRecord info syn doc fc tyn ty cdoc cn cty

831834 return (pn, pfnTy, PClauses fc [] setname [pclause])

832835

833836elabCon :: ElabInfo -> SyntaxInfo -> Name -> Bool ->

834− (String, Name, PTerm, FC, [Name]) -> Idris (Name, Type)

835−elabCon info syn tn codata (doc, n, t_in, fc, forcenames)

837+ (String, [(Name, String)], Name, PTerm, FC, [Name]) -> Idris (Name, Type)

838+elabCon info syn tn codata (doc, argDocs, n, t_in, fc, forcenames)

836839 = do checkUndefined fc n

837840 ctxt <- getContext

838841 i <- getIState

@@ -853,7 +856,8 @@ elabCon info syn tn codata (doc, n, t_in, fc, forcenames)

853856 tyIs cty'

854857 logLvl 2 $ "---> " ++ show n ++ " : " ++ show cty'

855858 addIBC (IBCDef n)

856− addDocStr n doc

859+ checkDocs fc argDocs t_in

860+ addDocStr n doc argDocs

857861 addIBC (IBCDoc n)

858862 let fs = map (getNamePos 0 t) forcenames

859863 -- FIXME: 'forcenames' is an almighty hack! Need a better way of

@@ -1158,7 +1162,7 @@ elabPE info fc caller r =

11581162 (map (\ (lhs, rhs) ->

11591163 (showTmImpls lhs ++ " = " ++

11601164 showTmImpls rhs)) pats)

1161− elabType info defaultSyntax "" fc opts newnm specTy

1165+ elabType info defaultSyntax "" [] fc opts newnm specTy

11621166 let def = map (\ (lhs, rhs) -> PClause fc newnm lhs [] rhs []) pats

11631167 elabClauses info fc opts newnm def

11641168 logLvl 1 $ "Specialised " ++ show newnm)

@@ -1276,7 +1280,7 @@ checkPossible info fc tcgen fname lhs_in

12761280 ((P _ x _, _), (P _ y _, _)) -> x == y

12771281 _ -> False

12781282

1279−getFixedInType i env (PExp _ _ _ _ : is) (Bind n (Pi t) sc)

1283+getFixedInType i env (PExp _ _ _ : is) (Bind n (Pi t) sc)

12801284 = getFixedInType i (n : env) is (instantiate (P Bound n t) sc)

12811285getFixedInType i env (_ : is) (Bind n (Pi t) sc)

12821286 = 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)

15001504-- = NS (UN ('#':show x)) [show cnum, show fname]

15011505

15021506 sepBlocks bs = sepBlocks' [] bs where

1503− sepBlocks' ns (d@(PTy _ _ _ _ n t) : bs)

1507+ sepBlocks' ns (d@(PTy _ _ _ _ _ n t) : bs)

15041508 = let (bf, af) = sepBlocks' (n : ns) bs in

15051509 (d : bf, af)

15061510 sepBlocks' ns (d@(PClauses _ _ n _) : bs)

@@ -1744,10 +1748,10 @@ elabClass info syn doc fc constraints tn ps ds

17441748 let cty = impbind ps $ conbind constraints

17451749 $ pibind (map (\ (n, ty) -> (nsroot n, ty)) methods)

17461750 constraint

1747− let cons = [("", cn, cty, fc, [])]

1751+ let cons = [("", [], cn, cty, fc, [])]

17481752 let ddecl = PDatadecl tn tty cons

17491753 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

17511755 -- for each constraint, build a top level function to chase it

17521756 logLvl 5 $ "Building functions"

17531757 let usyn = syn { using = map (\ (x,y) -> UImplicit x y) ps

@@ -1785,8 +1789,8 @@ elabClass info syn doc fc constraints tn ps ds

17851789 conbind (ty : ns) x = PPi constraint (sMN 0 "class") ty (conbind ns x)

17861790 conbind [] x = x

17871791

1788− getMName (PTy _ _ _ _ n _) = nsroot n

1789− tdecl allmeths (PTy doc syn _ o n t)

1792+ getMName (PTy _ _ _ _ _ n _) = nsroot n

1793+ tdecl allmeths (PTy doc _ syn _ o n t)

17901794 = do t' <- implicit' syn allmeths n t

17911795 logLvl 5 $ "Method " ++ show n ++ " : " ++ showTmImpls t'

17921796 return ( (n, (toExp (map fst ps) Exp t')),

@@ -1799,7 +1803,7 @@ elabClass info syn doc fc constraints tn ps ds

17991803 case lookup n mtys of

18001804 Just (syn, o, ty) -> do let ty' = insertConstraint c ty

18011805 let ds = map (decorateid defaultdec)

1802− [PTy "" syn fc [] n ty',

1806+ [PTy "" [] syn fc [] n ty',

18031807 PClauses fc (o ++ opts) n cs]

18041808 iLOG (show ds)

18051809 return (n, ((defaultdec n, ds!!1), ds))

@@ -1809,7 +1813,7 @@ elabClass info syn doc fc constraints tn ps ds

18091813 defaultdec (UN n) = sUN ("default#" ++ str n)

18101814 defaultdec (NS n ns) = NS (defaultdec n) ns

18111815

1812− tydecl (PTy _ _ _ _ _ _) = True

1816+ tydecl (PTy _ _ _ _ _ _ _) = True

18131817 tydecl _ = False

18141818 instdecl (PInstance _ _ _ _ _ _ _ _) = True

18151819 instdecl _ = False

@@ -1837,7 +1841,7 @@ elabClass info syn doc fc constraints tn ps ds

18371841 addInstance False conn' cfn

18381842 addIBC (IBCInstance False conn' cfn)

18391843-- iputStrLn ("Added " ++ show (conn, cfn, ty))

1840− return [PTy "" syn fc [] cfn ty,

1844+ return [PTy "" [] syn fc [] cfn ty,

18411845 PClauses fc [Dictionary] cfn [PClause fc cfn lhs [] rhs []]]

18421846

18431847 -- 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

18531857 iLOG (showTmImpls ty)

18541858 iLOG (show (m, ty', capp, margs))

18551859 iLOG (showTmImpls lhs ++ " = " ++ showTmImpls rhs)

1856− return [PTy doc syn fc o m ty',

1860+ return [PTy doc [] syn fc o m ty',

18571861 PClauses fc [Inlinable] m [PClause fc m lhs [] rhs []]]

18581862

1859− getMArgs (PPi (Imp _ _ _ _) n ty sc) = IA : getMArgs sc

1860− getMArgs (PPi (Exp _ _ _ _) n ty sc) = EA : getMArgs sc

1861− getMArgs (PPi (Constraint _ _ _) n ty sc) = CA : getMArgs sc

1863+ getMArgs (PPi (Imp _ _ _) n ty sc) = IA : getMArgs sc

1864+ getMArgs (PPi (Exp _ _ _) n ty sc) = EA : getMArgs sc

1865+ getMArgs (PPi (Constraint _ _) n ty sc) = CA : getMArgs sc

18621866 getMArgs _ = []

18631867

18641868 getMeth (m:ms) (a:as) x | x == a = PRef fc m

@@ -1874,14 +1878,14 @@ elabClass info syn doc fc constraints tn ps ds

18741878 rhsArgs (CA : xs) ns = pconst (PResolveTC fc) : rhsArgs xs ns

18751879 rhsArgs [] _ = []

18761880

1877− insertConstraint c (PPi p@(Imp _ _ _ _) n ty sc)

1881+ insertConstraint c (PPi p@(Imp _ _ _) n ty sc)

18781882 = PPi p n ty (insertConstraint c sc)

18791883 insertConstraint c sc = PPi constraint (sMN 0 "class") c sc

18801884

18811885 -- 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)

18831887 | 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)

18851889 toExp ns e (PPi p n ty sc) = PPi p n ty (toExp ns e sc)

18861890 toExp ns e sc = sc

18871891

@@ -1901,7 +1905,7 @@ elabInstance info syn what fc cs n ps t expn ds = do

19011905 let constraint = PApp fc (PRef fc n) (map pexp ps)

19021906 let iname = mkiname n ps expn

19031907 when (what /= EDefns) $ do

1904− nty <- elabType' True info syn "" fc [] iname t

1908+ nty <- elabType' True info syn "" [] fc [] iname t

19051909 -- if the instance type matches any of the instances we have already,

19061910 -- and it's not a named instance, then it's overlapping, so report an error

19071911 case expn of

@@ -2009,17 +2013,17 @@ elabInstance info syn what fc cs n ps t expn ds = do

20092013

20102014 mkMethApp (n, _, _, ty)

20112015 = 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'

20132017 = PLam (sMN i "meth") Placeholder (lamBind (i+1) sc sc')

20142018 lamBind i (PPi _ n ty sc) sc'

20152019 = PLam (sMN i "meth") Placeholder (lamBind (i+1) sc sc')

20162020 lamBind i _ sc = sc

2017− methArgs i (PPi (Imp _ _ _ _) n ty sc)

2018− = PImp 0 True [] n (PRef fc (sMN i "meth")) "" : methArgs (i+1) sc

2019− methArgs i (PPi (Exp _ _ _ _) n ty sc)

2020− = PExp 0 [] (PRef fc (sMN i "meth")) "" : methArgs (i+1) sc

2021− methArgs i (PPi (Constraint _ _ _) n ty sc)

2022− = PConstraint 0 [] (PResolveTC fc) "" : methArgs (i+1) sc

2021+ methArgs i (PPi (Imp _ _ _) n ty sc)

2022+ = PImp 0 True [] n (PRef fc (sMN i "meth")) : methArgs (i+1) sc

2023+ methArgs i (PPi (Exp _ _ _) n ty sc)

2024+ = PExp 0 [] (PRef fc (sMN i "meth")) : methArgs (i+1) sc

2025+ methArgs i (PPi (Constraint _ _) n ty sc)

2026+ = PConstraint 0 [] (PResolveTC fc) : methArgs (i+1) sc

20232027 methArgs i _ = []

20242028

20252029 papp fc f [] = f

@@ -2038,12 +2042,12 @@ elabInstance info syn what fc cs n ps t expn ds = do

20382042 decorate ns iname (UN n) = NS (SN (MethodN (UN n))) ns

20392043 decorate ns iname (NS (UN n) s) = NS (SN (MethodN (UN n))) ns

20402044

2041− mkTyDecl (n, op, t, _) = PTy "" syn fc op n t

2045+ mkTyDecl (n, op, t, _) = PTy "" [] syn fc op n t

20422046

20432047 conbind (ty : ns) x = PPi constraint (sMN 0 "class") ty (conbind ns x)

20442048 conbind [] x = x

20452049

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)

20472051 coninsert cs sc = conbind cs sc

20482052

20492053 insertDefaults :: IState -> Name ->

@@ -2101,7 +2105,7 @@ elabInstance info syn what fc cs n ps t expn ds = do

21012105 PClauses fc [Dictionary] cfn [PClause fc cfn lhs [] rhs []]]

21022106-}

21032107

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

21052109decorateid decorate (PClauses f o n cs)

21062110 = PClauses f o (decorate n) (map dc cs)

21072111 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 _ _ _)

21552159 = return () -- nothing to elaborate

21562160elabDecl' _ info (PSyntax _ p)

21572161 = 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)

21592163 | what /= EDefns

21602164 = 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

21622166 return ()

21632167elabDecl' what info (PPostulate doc s f o n ty)

21642168 | what /= EDefns

21652169 = do iLOG $ "Elaborating postulate " ++ show n ++ show o

21662170 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)

21682172 | what /= ETypes

21692173 = do iLOG $ "Elaborating " ++ show (d_name d)

2170− elabData info s doc f co d

2174+ elabData info s doc argDocs f co d

21712175 | otherwise

21722176 = 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))

21742178elabDecl' what info d@(PClauses f o n ps)

21752179 | what /= ETypes

21762180 = do iLOG $ "Elaborating clause " ++ show n

@@ -2227,7 +2231,7 @@ elabDecl' what info (PRecord doc s f tyn ty cdoc cn cty)

22272231 elabRecord info s doc f tyn ty cdoc cn cty

22282232 | otherwise

22292233 = 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)

22312235elabDecl' _ info (PDSL n dsl)

22322236 = do i <- getIState

22332237 putIState (i { idris_dsls = addDef n dsl (idris_dsls i) })

@@ -2282,3 +2286,14 @@ inferredDiff fc inf user =

22822286 Right vs -> return False

22832287 Left (x, y) -> return True

22842288

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

926926 ulog <- getUnifyLog

927927 solve

928928 traceWhen ulog ("Got " ++ show n) $ return ()

929− where isImp (PImp p _ _ _ _ _) = (True, p)

929+ where isImp (PImp p _ _ _ _) = (True, p)

930930 isImp arg = (False, priority arg)

931931

932932collectDeferred :: Maybe Name ->

@@ -1001,7 +1001,7 @@ runTac autoSolve ist fn tac

10011001 show fn')) fnimps

10021002 tryAll tacs

10031003 when autoSolve solveAll

1004− where isImp (PImp _ _ _ _ _ _) = True

1004+ where isImp (PImp _ _ _ _ _) = True

10051005 isImp _ = False

10061006 envArgs n = do e <- get_env

10071007 case lookup n e of

src/Idris/IBC.hs+28−40

@@ -52,7 +52,7 @@ data IBCFile = IBCFile { ver :: Word8,

5252 ibc_flags :: [(Name, [FnOpt])],

5353 ibc_cg :: [(Name, CGInfo)],

5454 ibc_defs :: [(Name, Def)],

55− ibc_docstrings :: [(Name, String)],

55+ ibc_docstrings :: [(Name, (String, [(Name, String)]))],

5656 ibc_transforms :: [(Term, Term)],

5757 ibc_errRev :: [(Term, Term)],

5858 ibc_coercions :: [Name],

@@ -393,7 +393,7 @@ pDefs syms ds

393393 updateOrig (Left t) = Left (update t)

394394 updateOrig (Right (l, r)) = Right (update l, update r)

395395

396− updateCD (CaseDefs (ts, t) (cs, c) (is, i) (rs, r))

396+ updateCD (CaseDefs (ts, t) (cs, c) (is, i) (rs, r))

397397 = CaseDefs (ts, fmap update t)

398398 (cs, fmap update c)

399399 (is, fmap update i)

@@ -405,8 +405,8 @@ pDefs syms ds

405405 update (Proj t i) = Proj (update t) i

406406 update t = t

407407

408−pDocs :: [(Name, String)] -> Idris ()

409−pDocs ds = mapM_ (\ (n, a) -> addDocStr n a) ds

408+pDocs :: [(Name, (String, [(Name, String)]))] -> Idris ()

409+pDocs ds = mapM_ (\ (n, a) -> addDocStr n (fst a) (snd a)) ds

410410

411411pAccess :: [(Name, Accessibility)] -> Idris ()

412412pAccess ds = mapM_ (\ (n, a) ->

@@ -1234,51 +1234,43 @@ instance Binary Static where

12341234instance Binary Plicity where

12351235 put x

12361236 = case x of

1237− Imp x1 x2 x3 x4 ->

1237+ Imp x1 x2 x3 ->

12381238 do putWord8 0

12391239 put x1

12401240 put x2

12411241 put x3

1242− put x4

1243− Exp x1 x2 x3 x4 ->

1242+ Exp x1 x2 x3 ->

12441243 do putWord8 1

12451244 put x1

12461245 put x2

12471246 put x3

1248− put x4

1249− Constraint x1 x2 x3 ->

1247+ Constraint x1 x2 ->

12501248 do putWord8 2

12511249 put x1

12521250 put x2

1253− put x3

1254− TacImp x1 x2 x3 x4 ->

1251+ TacImp x1 x2 x3 ->

12551252 do putWord8 3

12561253 put x1

12571254 put x2

12581255 put x3

1259− put x4

12601256 get

12611257 = do i <- getWord8

12621258 case i of

12631259 0 -> do x1 <- get

12641260 x2 <- get

12651261 x3 <- get

1266− x4 <- get

1267− return (Imp x1 x2 x3 x4)

1262+ return (Imp x1 x2 x3)

12681263 1 -> do x1 <- get

12691264 x2 <- get

12701265 x3 <- get

1271− x4 <- get

1272− return (Exp x1 x2 x3 x4)

1266+ return (Exp x1 x2 x3)

12731267 2 -> do x1 <- get

12741268 x2 <- get

1275− x3 <- get

1276− return (Constraint x1 x2 x3)

1269+ return (Constraint x1 x2)

12771270 3 -> do x1 <- get

12781271 x2 <- get

12791272 x3 <- get

1280− x4 <- get

1281− return (TacImp x1 x2 x3 x4)

1273+ return (TacImp x1 x2 x3)

12821274 _ -> error "Corrupted binary data for Plicity"

12831275

12841276

@@ -1289,7 +1281,7 @@ instance (Binary t) => Binary (PDecl' t) where

12891281 put x1

12901282 put x2

12911283 put x3

1292− PTy x1 x2 x3 x4 x5 x6

1284+ PTy x1 x2 x3 x4 x5 x6 x7

12931285 -> do putWord8 1

12941286 put x1

12951287 put x2

@@ -1297,18 +1289,20 @@ instance (Binary t) => Binary (PDecl' t) where

12971289 put x4

12981290 put x5

12991291 put x6

1292+ put x7

13001293 PClauses x1 x2 x3 x4 -> do putWord8 2

13011294 put x1

13021295 put x2

13031296 put x3

13041297 put x4

1305− PData x1 x2 x3 x4 x5 ->

1298+ PData x1 x2 x3 x4 x5 x6 ->

13061299 do putWord8 3

13071300 put x1

13081301 put x2

13091302 put x3

13101303 put x4

13111304 put x5

1305+ put x6

13121306 PParams x1 x2 x3 -> do putWord8 4

13131307 put x1

13141308 put x2

@@ -1375,7 +1369,8 @@ instance (Binary t) => Binary (PDecl' t) where

13751369 x4 <- get

13761370 x5 <- get

13771371 x6 <- get

1378− return (PTy x1 x2 x3 x4 x5 x6)

1372+ x7 <- get

1373+ return (PTy x1 x2 x3 x4 x5 x6 x7)

13791374 2 -> do x1 <- get

13801375 x2 <- get

13811376 x3 <- get

@@ -1386,7 +1381,8 @@ instance (Binary t) => Binary (PDecl' t) where

13861381 x3 <- get

13871382 x4 <- get

13881383 x5 <- get

1389− return (PData x1 x2 x3 x4 x5)

1384+ x6 <- get

1385+ return (PData x1 x2 x3 x4 x5 x6)

13901386 4 -> do x1 <- get

13911387 x2 <- get

13921388 x3 <- get

@@ -1924,34 +1920,30 @@ instance (Binary t) => Binary (PDo' t) where

19241920instance (Binary t) => Binary (PArg' t) where

19251921 put x

19261922 = case x of

1927− PImp x1 x2 x3 x4 x5 x6 ->

1923+ PImp x1 x2 x3 x4 x5 ->

19281924 do putWord8 0

19291925 put x1

19301926 put x2

19311927 put x3

19321928 put x4

19331929 put x5

1934− put x6

1935− PExp x1 x2 x3 x4 ->

1930+ PExp x1 x2 x3 ->

19361931 do putWord8 1

19371932 put x1

19381933 put x2

19391934 put x3

1940− put x4

1941− PConstraint x1 x2 x3 x4 ->

1935+ PConstraint x1 x2 x3 ->

19421936 do putWord8 2

19431937 put x1

19441938 put x2

19451939 put x3

1946− put x4

1947− PTacImplicit x1 x2 x3 x4 x5 x6 ->

1940+ PTacImplicit x1 x2 x3 x4 x5 ->

19481941 do putWord8 3

19491942 put x1

19501943 put x2

19511944 put x3

19521945 put x4

19531946 put x5

1954− put x6

19551947 get

19561948 = do i <- getWord8

19571949 case i of

@@ -1960,25 +1952,21 @@ instance (Binary t) => Binary (PArg' t) where

19601952 x3 <- get

19611953 x4 <- get

19621954 x5 <- get

1963− x6 <- get

1964− return (PImp x1 x2 x3 x4 x5 x6)

1955+ return (PImp x1 x2 x3 x4 x5)

19651956 1 -> do x1 <- get

19661957 x2 <- get

19671958 x3 <- get

1968− x4 <- get

1969− return (PExp x1 x2 x3 x4)

1959+ return (PExp x1 x2 x3)

19701960 2 -> do x1 <- get

19711961 x2 <- get

19721962 x3 <- get

1973− x4 <- get

1974− return (PConstraint x1 x2 x3 x4)

1963+ return (PConstraint x1 x2 x3)

19751964 3 -> do x1 <- get

19761965 x2 <- get

19771966 x3 <- get

19781967 x4 <- get

19791968 x5 <- get

1980− x6 <- get

1981− return (PTacImplicit x1 x2 x3 x4 x5 x6)

1969+ return (PTacImplicit x1 x2 x3 x4 x5)

19821970 _ -> error "Corrupted binary data for PArg'"

19831971

19841972

src/Idris/ParseData.hs+26−24

@@ -33,13 +33,15 @@ import qualified Data.HashSet as HS

3333import qualified Data.Text as T

3434import qualified Data.ByteString.UTF8 as UTF8

3535

36+import Debug.Trace

37+

3638{- |Parses a record type declaration

3739Record ::=

3840 DocComment Accessibility? 'record' FnName TypeSig 'where' OpenBlock Constructor KeepTerminator CloseBlock;

3941-}

4042record :: SyntaxInfo -> IdrisParser PDecl

4143record syn = do (doc, acc) <- try (do

42− doc <- option "" (docComment '|')

44+ doc <- option ("", []) docComment

4345 acc <- optional accessibility

4446 reserved "record"

4547 return (doc, acc))

@@ -49,13 +51,13 @@ record syn = do (doc, acc) <- try (do

4951 ty <- typeExpr (allowImp syn)

5052 let tyn = expandNS syn tyn_in

5153 reserved "where"

52− (cdoc, cn, cty, _, _) <- indentedBlockS (constructor syn)

54+ (cdoc, argDocs, cn, cty, _, _) <- indentedBlockS (constructor syn)

5355 accData acc tyn [cn]

5456 let rsyn = syn { syn_namespace = show (nsroot tyn) :

5557 syn_namespace syn }

5658 let fns = getRecNames rsyn cty

5759 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

5961 <?> "record type declaration"

6062 where

6163 getRecNames :: SyntaxInfo -> PTerm -> [Name]

@@ -100,29 +102,29 @@ SimpleConstructorList ::=

100102 ;

101103-}

102104data_ :: SyntaxInfo -> IdrisParser PDecl

103−data_ syn = do (doc, acc, dataOpts) <- try (do

104− doc <- option "" (docComment '|')

105+data_ syn = do (doc, argDocs, acc, dataOpts) <- try (do

106+ (doc, argDocs) <- option ("", []) docComment

105107 pushIndent

106108 acc <- optional accessibility

107109 elim <- dataOpts []

108110 co <- dataI

109111 let dataOpts = combineDataOpts(elim ++ co)

110− return (doc, acc, dataOpts))

112+ return (doc, argDocs, acc, dataOpts))

111113 fc <- getFC

112114 tyn_in <- fnName

113115 (do try (lchar ':')

114116 popIndent

115117 ty <- typeExpr (allowImp syn)

116118 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

118120 reserved "where"

119121 cons <- indentedBlock (constructor syn)

120− accData acc tyn (map (\ (_, n, _, _, _) -> n) cons)

121− return $ PData doc syn fc dataOpts (PDatadecl tyn ty cons))) <|> (do

122+ accData acc tyn (map (\ (_, _, n, _, _, _) -> n) cons)

123+ return $ PData doc argDocs syn fc dataOpts (PDatadecl tyn ty cons))) <|> (do

122124 args <- many name

123125 let ty = bindArgs (map (const PType) args) PType

124126 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

126128 try (lchar '=') <|> do reserved "where"

127129 let kw = (if DefaultEliminator `elem` dataOpts then "" else "%noelim ") ++ (if Codata `elem` dataOpts then "co" else "") ++ "data "

128130 let n = show tyn_in ++ " "

@@ -134,14 +136,14 @@ data_ syn = do (doc, acc, dataOpts) <- try (do

134136 let fix2 = s ++ ": " ++ ns ++ " -> Type where\n ..."

135137 let fix3 = s ++ ": " ++ ss ++ " -> Type where\n ..."

136138 fail $ fixErrorMsg "unexpected \"where\"" [fix1, fix2, fix3]

137− cons <- sepBy1 (simpleConstructor syn) (lchar '|')

139+ cons <- sepBy1 (simpleConstructor syn) (reservedOp "|")

138140 terminator

139141 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) ->

141143 do let cty = bindArgs cargs conty

142− return (doc, x, cty, cfc, fs)) cons

143− accData acc tyn (map (\ (_, n, _, _, _) -> n) cons')

144− return $ PData doc syn fc dataOpts (PDatadecl tyn ty cons')))

144+ return (doc, argDocs, x, cty, cfc, fs)) cons

145+ accData acc tyn (map (\ (_, _, n, _, _, _) -> n) cons')

146+ return $ PData doc argDocs syn fc dataOpts (PDatadecl tyn ty cons')))

145147 <?> "data type declaration"

146148 where

147149 mkPApp :: FC -> PTerm -> [PTerm] -> PTerm

@@ -150,17 +152,17 @@ data_ syn = do (doc, acc, dataOpts) <- try (do

150152 bindArgs :: [PTerm] -> PTerm -> PTerm

151153 bindArgs xs t = foldr (PPi expl (sMN 0 "_t")) t xs

152154 combineDataOpts :: DataOpts -> DataOpts

153− combineDataOpts opts = if Codata `elem` opts

154− then delete DefaultEliminator opts

155+ combineDataOpts opts = if Codata `elem` opts

156+ then delete DefaultEliminator opts

155157 else opts

156158

157159

158160{- | Parses a type constructor declaration

159161 Constructor ::= DocComment? FnName TypeSig;

160162-}

161−constructor :: SyntaxInfo -> IdrisParser (String, Name, PTerm, FC, [Name])

163+constructor :: SyntaxInfo -> IdrisParser (String, [(Name, String)], Name, PTerm, FC, [Name])

162164constructor syn

163− = do doc <- option "" (docComment '|')

165+ = do (doc, argDocs) <- option ("", []) docComment

164166 cn_in <- fnName; fc <- getFC

165167 let cn = expandNS syn cn_in

166168 lchar ':'

@@ -169,21 +171,21 @@ constructor syn

169171 fs <- option [] (do lchar '%'; reserved "erase"

170172 sepBy1 name (lchar ','))

171173 ty <- typeExpr (allowImp syn)

172− return (doc, cn, ty, fc, fs)

174+ return (doc, argDocs, cn, ty, fc, fs)

173175 <?> "constructor"

174176

175177{- | Parses a constructor for simple discriminative union data types

176178 SimpleConstructor ::= FnName SimpleExpr* DocComment?

177179-}

178−simpleConstructor :: SyntaxInfo -> IdrisParser (String, Name, [PTerm], FC, [Name])

180+simpleConstructor :: SyntaxInfo -> IdrisParser (String, [(Name, String)], Name, [PTerm], FC, [Name])

179181simpleConstructor syn

180− = do cn_in <- fnName

182+ = do doc <- option ("", []) (try docComment)

183+ cn_in <- fnName

181184 let cn = expandNS syn cn_in

182185 fc <- getFC

183186 args <- many (do notEndApp

184187 simpleExpr syn)

185− doc <- option "" (try $ docComment '^')

186− return (doc, cn, args, fc, [])

188+ return (fst doc, [], cn, args, fc, [])

187189 <?> "constructor"

188190

189191{- | Parses a dsl block declaration

src/Idris/ParseExpr.hs+4−5

@@ -786,10 +786,9 @@ pi syn =

786786 return []

787787 st <- static

788788 (do try (lchar '('); xt <- typeDeclList syn; lchar ')'

789− doc <- option "" (docComment '^')

790789 symbol "->"

791790 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

793792 lchar '{'

794793 (do reserved "auto"

795794 when (Lazy `elem` opts || (st == Static)) $ fail "auto type constraints can not be lazy or static"

@@ -798,7 +797,7 @@ pi syn =

798797 symbol "->"

799798 sc <- expr syn

800799 return (bindList (PPi

801− (TacImp [] Dynamic (PTactics [Trivial]) "")) xt sc))

800+ (TacImp [] Dynamic (PTactics [Trivial]))) xt sc))

802801 <|> (do

803802 reserved "default"

804803 when (Lazy `elem` opts || (st == Static)) $ fail "default tactic constraints can not be lazy or static"

@@ -807,13 +806,13 @@ pi syn =

807806 lchar '}'

808807 symbol "->"

809808 sc <- expr syn

810− return (bindList (PPi (TacImp [] Dynamic script "")) xt sc))

809+ return (bindList (PPi (TacImp [] Dynamic script)) xt sc))

811810 <|> (if implicitAllowed syn then do

812811 xt <- typeDeclList syn

813812 lchar '}'

814813 symbol "->"

815814 sc <- expr syn

816− return (bindList (PPi (Imp opts st "" False)) xt sc)

815+ return (bindList (PPi (Imp opts st False)) xt sc)

817816 else do fail "no implicit arguments allowed here"))

818817 <?> "dependent type signature"

819818

src/Idris/ParseHelpers.hs+33−32

@@ -17,6 +17,8 @@ import Idris.Core.TT

1717import Idris.Core.Evaluate

1818import Idris.Delaborate (pprintErr)

1919

20+import qualified Util.Pretty as Pretty (text)

21+

2022import Control.Applicative

2123import Control.Monad

2224import Control.Monad.State.Strict

@@ -33,6 +35,8 @@ import qualified Data.ByteString.UTF8 as UTF8

3335

3436import System.FilePath

3537

38+import Debug.Trace

39+

3640-- | Idris parser with state used during parsing

3741type IdrisParser = StateT IState IdrisInnerParser

3842

@@ -51,10 +55,10 @@ runparser p i inputname =

5155 parseString (runInnerParser (evalStateT p i))

5256 (Directed (UTF8.fromString inputname) 0 0 0 0)

5357

54−noDocCommentHere :: Char -> String -> IdrisParser ()

55−noDocCommentHere c msg =

58+noDocCommentHere :: String -> IdrisParser ()

59+noDocCommentHere msg =

5660 optional (do fc <- getFC

57− docComment c

61+ docComment

5862 ist <- get

5963 put ist { parserWarnings = (fc, Msg msg) : parserWarnings ist}) *>

6064 pure ()

@@ -86,12 +90,6 @@ isEol _ = False

8690eol :: MonadicParsing m => m ()

8791eol = (satisfy isEol *> pure ()) <|> lookAhead eof <?> "end of line"

8892

89−-- | Checks if a character is a documentation comment marker

90−isDocCommentMarker :: Char -> Bool

91−isDocCommentMarker '|' = True

92−isDocCommentMarker '^' = True

93−isDocCommentMarker _ = False

94−

9593{- | Consumes a single-line comment

9694

9795@

@@ -103,7 +101,6 @@ isDocCommentMarker _ = False

103101singleLineComment :: MonadicParsing m => m ()

104102singleLineComment = try (string "--" *> eol *> pure ())

105103 <|> try (string "--" *> many simpleWhiteSpace *>

106− satisfy (not . isDocCommentMarker) *>

107104 many (satisfy (not . isEol)) *>

108105 eol *> pure ())

109106 <?> ""

@@ -127,13 +124,12 @@ singleLineComment = try (string "--" *> eol *> pure ())

127124-}

128125multiLineComment :: MonadicParsing m => m ()

129126multiLineComment = try (string "{-" *> (string "-}") *> pure ())

130− <|> string "{-" *> satisfy (not . isDocCommentMarker) *> inCommentChars

127+ <|> string "{-" *> inCommentChars

131128 <?> ""

132129 where inCommentChars :: MonadicParsing m => m ()

133130 inCommentChars = string "-}" *> pure ()

134131 <|> try (multiLineComment) *> inCommentChars

135− <|> try (docComment '|') *> inCommentChars

136− <|> try (docComment '^') *> inCommentChars

132+ <|> string "|||" *> many (satisfy (not . isEol)) *> eol *> inCommentChars

137133 <|> skipSome (noneOf startEnd) *> inCommentChars

138134 <|> oneOf startEnd *> inCommentChars

139135 <?> "end of comment"

@@ -148,27 +144,32 @@ multiLineComment = try (string "{-" *> (string "-}") *> pure ())

148144 ;

149145@

150146 -}

151−docComment :: MonadicParsing m => Char -> m String

152−docComment marker | isDocCommentMarker marker = do dc <- docComment' marker

153− return (T.unpack $ T.strip $ T.pack dc)

154− | otherwise = fail "internal error: tried to parse a documentation comment with invalid marker"

155− where docComment' :: MonadicParsing m => Char -> m String

156− docComment' marker = (do string "--"

147+docComment :: IdrisParser (String, [(Name, String)])

148+docComment = do dc <- pushIndent *> docCommentLine

149+ rest <- many (indented docCommentLine)

150+ args <- many (indented argDocCommentLine)

151+ popIndent

152+ return (T.unpack $ T.strip $ T.pack (dc ++ concat rest), args)

153+

154+ where docCommentLine :: MonadicParsing m => m String

155+ docCommentLine = try (do string "|||"

157156 many (satisfy isSpace)

158− char marker

157+ first <- satisfy (\c -> not (isEol c || c == '@'))

159158 res <- many (satisfy (not . isEol))

160− eol

161− rest <- many (do string "--"

162− stuff <- many (satisfy (not . isEol))

163− eol

164− return stuff)

165− someSpace

166− return (res ++ concat rest))-- ++ concat rest))

167− <|> (do string "{-"

168− many (satisfy isSpace)

169− char marker

170− (manyTill anyChar (try (string "-}")) <?> "end of comment"))

171− <?> ""

159+ eol ; someSpace

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)

168+ docs <- many (satisfy (not . isEol))

169+ eol ; someSpace

170+ return (n, docs)

171+

172+

172173

173174-- | Parses some white space

174175whiteSpace :: MonadicParsing m => m ()

src/Idris/ParseOps.hs+1−1

@@ -59,7 +59,7 @@ binary name f = Infix (do fc <- getFC

5959 indentPropHolds gtProp

6060 reservedOp name

6161 indentPropHolds gtProp

62− doc <- option "" (docComment '^')

62+ doc <- option ("", []) docComment

6363 return (f fc))

6464

6565-- | Prefix operator

src/Idris/Parser.hs+8−8

@@ -87,7 +87,7 @@ import System.IO

8787@

8888-}

8989moduleHeader :: IdrisParser [String]

90−moduleHeader = try (do noDocCommentHere '|' "Modules cannot have documentation comments"

90+moduleHeader = try (do noDocCommentHere "Modules cannot have documentation comments"

9191 reserved "module"

9292 i <- identifier

9393 option ';' (lchar ';')

@@ -315,7 +315,7 @@ fnDecl' syn = checkFixity $

315315 do (doc, fc, opts', n, acc) <- try (do

316316 pushIndent

317317 ist <- get

318− doc <- option "" (docComment '|')

318+ doc <- option ("", []) docComment

319319 ist <- get

320320 let initOpts = if default_total ist

321321 then [TotalFn]

@@ -331,7 +331,7 @@ fnDecl' syn = checkFixity $

331331 ty <- typeExpr (allowImp syn)

332332 terminator

333333 addAcc n acc

334− return (PTy doc syn fc opts' n ty)

334+ return (PTy (fst doc) (snd doc) syn fc opts' n ty)

335335 <|> postulate syn

336336 <|> caf syn

337337 <|> pattern syn

@@ -344,7 +344,7 @@ fnDecl' syn = checkFixity $

344344 unless fOk . fail $

345345 "Missing fixity declaration for " ++ show n

346346 return decl

347− getName (PTy _ _ _ _ n _) = Just n

347+ getName (PTy _ _ _ _ _ n _) = Just n

348348 getName _ = Nothing

349349 fixityOK (NS n _) = fixityOK n

350350 fixityOK (UN n) | all (flip elem opChars) (str n) =

@@ -413,7 +413,7 @@ Postulate ::=

413413@

414414-}

415415postulate :: SyntaxInfo -> IdrisParser PDecl

416−postulate syn = do doc <- try $ do doc <- option "" (docComment '|')

416+postulate syn = do doc <- try $ do doc <- option ("", []) docComment

417417 pushIndent

418418 reserved "postulate"

419419 return doc

@@ -431,7 +431,7 @@ postulate syn = do doc <- try $ do doc <- option "" (docComment '|')

431431 fc <- getFC

432432 terminator

433433 addAcc n acc

434− return (PPostulate doc syn fc opts' n ty)

434+ return (PPostulate (fst doc) syn fc opts' n ty)

435435 <?> "postulate"

436436

437437{- | Parses a using declaration

@@ -561,7 +561,7 @@ Class ::=

561561-}

562562class_ :: SyntaxInfo -> IdrisParser [PDecl]

563563class_ syn = do (doc, acc) <- try (do

564− doc <- option "" (docComment '|')

564+ doc <- option ("", []) docComment

565565 acc <- optional accessibility

566566 return (doc, acc))

567567 reserved "class"; fc <- getFC; cons <- constraintList syn; n_in <- fnName

@@ -569,7 +569,7 @@ class_ syn = do (doc, acc) <- try (do

569569 cs <- many carg

570570 ds <- option [] (classBlock syn)

571571 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]

573573 <?> "type-class declaration"

574574 where

575575 carg :: IdrisParser (Name, PTerm)

src/Idris/PartialEval.hs+2−2

@@ -103,7 +103,7 @@ mkPE_TermDecl ist newname sname ns

103103 deImp (PApp fc t as) = PApp fc t (map deImpArg as)

104104 deImp t = t

105105

106− deImpArg a@(PImp _ _ _ _ _ _) = a { getTm = Placeholder }

106+ deImpArg a@(PImp _ _ _ _ _) = a { getTm = Placeholder }

107107 deImpArg a = a

108108

109109data PEArgType = ImplicitS | ImplicitD

@@ -124,7 +124,7 @@ getSpecApps ist env tm = ga env (explicitNames tm) where

124124 | imparg imp = (ImplicitD, tm)

125125 | otherwise = (ExplicitD, (P Ref (sUN (show n ++ "arg")) Erased))

126126

127− imparg (PExp _ _ _ _) = False

127+ imparg (PExp _ _ _) = False

128128 imparg _ = True

129129

130130 buildApp env [] [] _ _ = []

src/Idris/ProofSearch.hs+1−1

@@ -109,6 +109,6 @@ proofSearch elab fn nroot hints ist

109109 (filter (\ (x, y) -> not x) (zip (map fst imps) args))

110110 solve

111111

112− isImp (PImp p _ _ _ _ _) = (True, p)

112+ isImp (PImp p _ _ _ _) = (True, p)

113113 isImp arg = (False, priority arg)

114114

src/Idris/Providers.hs+1−1

@@ -11,7 +11,7 @@ import Debug.Trace

1111

1212-- | Wrap a type provider in the type of type providers

1313providerTy :: 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]

1515

1616ioret = sUN "prim_io_return"

1717ermod = sNS (sUN "Error") ["Providers"]