git.iko.soy/Idris-dev
on master help sign in
New syntax for documentation comments

Implementation entailed removing documentation from the idris_implicits field of IState, which is why so many files are touched.

commitc1ef93887a1f01d02efc7163ba06eddbbd3e63a0 authorDavid Raymond Christiansen <david@davidchristiansen.dk> dateSat 1 Mar 2014, 22:53 (13 years ago) parentc2671c0
29 files changed+476−460
compare with master
unifiedsplit
libs/base/Data/ZZ.idr+2−2 libs/base/Language/Reflection.idr+6−6 libs/base/Language/Reflection/Errors.idr+1−1 libs/prelude/Prelude/Basics.idr+8−8 libs/prelude/Prelude/Bool.idr+6−6 libs/prelude/Prelude/Chars.idr+15−15 libs/prelude/Prelude/Classes.idr+8−8 libs/prelude/Prelude/List.idr+11−11 libs/prelude/Prelude/Strings.idr+6−6 libs/prelude/Prelude/Uninhabited.idr+1−1 samples/reflection.idr+25−25 src/Idris/AbsSyntax.hs+53−52 src/Idris/AbsSyntaxTree.hs+66−74 src/Idris/CaseSplit.hs+4−4 src/Idris/Coverage.hs+2−2 src/Idris/DeepSeq.hs+21−20 src/Idris/Delaborate.hs+15−10 src/Idris/Docs.hs+33−21 src/Idris/ElabDecls.hs+86−71 src/Idris/ElabTerm.hs+2−2 src/Idris/IBC.hs+29−41 src/Idris/ParseData.hs+26−24 src/Idris/ParseExpr.hs+4−5 src/Idris/ParseHelpers.hs+33−32 src/Idris/ParseOps.hs+1−1 src/Idris/Parser.hs+8−8 src/Idris/PartialEval.hs+2−2 src/Idris/ProofSearch.hs+1−1 src/Idris/Providers.hs+1−1
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 chosen to be positive.
1212data ZZ = Pos Nat | NegS Nat
1313
1414instance Signed ZZ where
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
2727 | IType | BIType | FlType | ChType | StrType
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/prelude/Prelude/Basics.idr+8−8
@@ -3,37 +3,37 @@ 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.
10+||| Manually assign a type to an expression.
1111the : (a : Type) -> a -> a
1212the _ = id
1313
14−-- | Constant function.
14+||| Constant function.
1515const : a -> b -> a
1616const x = \v => x
1717
18−-- | Return the first element of a pair.
18+||| Return the first element of a pair.
1919fst : (s, t) -> s
2020fst (x, y) = x
2121
22−-- | Return the second element of a pair.
22+||| Return the second element of a pair.
2323snd : (a, b) -> b
2424snd (x, y) = y
2525
2626infixl 9 .
2727
28−-- | Function composition
28+||| Function composition
2929(.) : (b -> c) -> (a -> b) -> a -> c
3030(.) f g x = f (g x)
3131
32−-- | Takes in the first two arguments in reverse order.
32+||| Takes in the first two arguments in reverse order.
3333flip : (a -> b -> c) -> b -> a -> c
3434flip f x y = f y x
3535
36−-- | Function application.
36+||| Function application.
3737apply : (a -> b) -> a -> b
3838apply f a = f a
3939
libs/prelude/Prelude/Bool.idr+6−6
@@ -1,14 +1,14 @@
11module Prelude.Bool
22
3−-- | Boolean Data Type
3+||| Boolean Data Type
44data Bool = False | True
55
6−-- | Boolean elimination
6+||| Boolean elimination
77boolElim : Bool -> (t : Lazy a) -> (e : Lazy a) -> a
88boolElim True t e = t
99boolElim False t e = e
1010
11−-- | Defines a predicate on Bool which guarantees that the value is true.
11+||| Defines a predicate on Bool which guarantees that the value is true.
1212data so : Bool -> Type where oh : so True
1313
1414-- Syntaxtic sugar for boolean elimination.
@@ -17,17 +17,17 @@ syntax if [test] then [t] else [e] = boolElim test (Delay t) (Delay e)
1717-- Boolean Operator Precedence
1818infixl 4 &&, ||
1919
20−-- | Boolean OR
20+||| Boolean OR
2121(||) : Bool -> Bool -> Bool
2222(||) False x = x
2323(||) True _ = True
2424
25−-- | Boolean AND
25+||| Boolean AND
2626(&&) : Bool -> Bool -> Bool
2727(&&) True x = x
2828(&&) False _ = False
2929
30−-- | Boolean NOT
30+||| Boolean NOT
3131not : Bool -> Bool
3232not True = False
3333not False = True
libs/prelude/Prelude/Chars.idr+15−15
@@ -3,66 +3,66 @@ 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
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/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/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+1−1
@@ -10,6 +10,6 @@ instance Uninhabited (Fin Z) where
1010instance Uninhabited (Z = S n) where
1111 uninhabited refl impossible
1212
13−-- | Use an absurd assumption to discharge a proof obligation
13+||| Use an absurd assumption to discharge a proof obligation
1414absurd : Uninhabited t => t -> a
1515absurd t = FalseElim (uninhabited t)
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+29−41
@@ -25,7 +25,7 @@ import Codec.Compression.Zlib (compress)
2525import Util.Zlib (decompressEither)
2626
2727ibcVersion :: Word8
28−ibcVersion = 61
28+ibcVersion = 62
2929
3030
3131data IBCFile = IBCFile { ver :: Word8,
@@ -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) ->
@@ -1231,51 +1231,43 @@ instance Binary Static where
12311231instance Binary Plicity where
12321232 put x
12331233 = case x of
1234− Imp x1 x2 x3 x4 ->
1234+ Imp x1 x2 x3 ->
12351235 do putWord8 0
12361236 put x1
12371237 put x2
12381238 put x3
1239− put x4
1240− Exp x1 x2 x3 x4 ->
1239+ Exp x1 x2 x3 ->
12411240 do putWord8 1
12421241 put x1
12431242 put x2
12441243 put x3
1245− put x4
1246− Constraint x1 x2 x3 ->
1244+ Constraint x1 x2 ->
12471245 do putWord8 2
12481246 put x1
12491247 put x2
1250− put x3
1251− TacImp x1 x2 x3 x4 ->
1248+ TacImp x1 x2 x3 ->
12521249 do putWord8 3
12531250 put x1
12541251 put x2
12551252 put x3
1256− put x4
12571253 get
12581254 = do i <- getWord8
12591255 case i of
12601256 0 -> do x1 <- get
12611257 x2 <- get
12621258 x3 <- get
1263− x4 <- get
1264− return (Imp x1 x2 x3 x4)
1259+ return (Imp x1 x2 x3)
12651260 1 -> do x1 <- get
12661261 x2 <- get
12671262 x3 <- get
1268− x4 <- get
1269− return (Exp x1 x2 x3 x4)
1263+ return (Exp x1 x2 x3)
12701264 2 -> do x1 <- get
12711265 x2 <- get
1272− x3 <- get
1273− return (Constraint x1 x2 x3)
1266+ return (Constraint x1 x2)
12741267 3 -> do x1 <- get
12751268 x2 <- get
12761269 x3 <- get
1277− x4 <- get
1278− return (TacImp x1 x2 x3 x4)
1270+ return (TacImp x1 x2 x3)
12791271 _ -> error "Corrupted binary data for Plicity"
12801272
12811273
@@ -1286,7 +1278,7 @@ instance (Binary t) => Binary (PDecl' t) where
12861278 put x1
12871279 put x2
12881280 put x3
1289− PTy x1 x2 x3 x4 x5 x6
1281+ PTy x1 x2 x3 x4 x5 x6 x7
12901282 -> do putWord8 1
12911283 put x1
12921284 put x2
@@ -1294,18 +1286,20 @@ instance (Binary t) => Binary (PDecl' t) where
12941286 put x4
12951287 put x5
12961288 put x6
1289+ put x7
12971290 PClauses x1 x2 x3 x4 -> do putWord8 2
12981291 put x1
12991292 put x2
13001293 put x3
13011294 put x4
1302− PData x1 x2 x3 x4 x5 ->
1295+ PData x1 x2 x3 x4 x5 x6 ->
13031296 do putWord8 3
13041297 put x1
13051298 put x2
13061299 put x3
13071300 put x4
13081301 put x5
1302+ put x6
13091303 PParams x1 x2 x3 -> do putWord8 4
13101304 put x1
13111305 put x2
@@ -1372,7 +1366,8 @@ instance (Binary t) => Binary (PDecl' t) where
13721366 x4 <- get
13731367 x5 <- get
13741368 x6 <- get
1375− return (PTy x1 x2 x3 x4 x5 x6)
1369+ x7 <- get
1370+ return (PTy x1 x2 x3 x4 x5 x6 x7)
13761371 2 -> do x1 <- get
13771372 x2 <- get
13781373 x3 <- get
@@ -1383,7 +1378,8 @@ instance (Binary t) => Binary (PDecl' t) where
13831378 x3 <- get
13841379 x4 <- get
13851380 x5 <- get
1386− return (PData x1 x2 x3 x4 x5)
1381+ x6 <- get
1382+ return (PData x1 x2 x3 x4 x5 x6)
13871383 4 -> do x1 <- get
13881384 x2 <- get
13891385 x3 <- get
@@ -1921,34 +1917,30 @@ instance (Binary t) => Binary (PDo' t) where
19211917instance (Binary t) => Binary (PArg' t) where
19221918 put x
19231919 = case x of
1924− PImp x1 x2 x3 x4 x5 x6 ->
1920+ PImp x1 x2 x3 x4 x5 ->
19251921 do putWord8 0
19261922 put x1
19271923 put x2
19281924 put x3
19291925 put x4
19301926 put x5
1931− put x6
1932− PExp x1 x2 x3 x4 ->
1927+ PExp x1 x2 x3 ->
19331928 do putWord8 1
19341929 put x1
19351930 put x2
19361931 put x3
1937− put x4
1938− PConstraint x1 x2 x3 x4 ->
1932+ PConstraint x1 x2 x3 ->
19391933 do putWord8 2
19401934 put x1
19411935 put x2
19421936 put x3
1943− put x4
1944− PTacImplicit x1 x2 x3 x4 x5 x6 ->
1937+ PTacImplicit x1 x2 x3 x4 x5 ->
19451938 do putWord8 3
19461939 put x1
19471940 put x2
19481941 put x3
19491942 put x4
19501943 put x5
1951− put x6
19521944 get
19531945 = do i <- getWord8
19541946 case i of
@@ -1957,25 +1949,21 @@ instance (Binary t) => Binary (PArg' t) where
19571949 x3 <- get
19581950 x4 <- get
19591951 x5 <- get
1960− x6 <- get
1961− return (PImp x1 x2 x3 x4 x5 x6)
1952+ return (PImp x1 x2 x3 x4 x5)
19621953 1 -> do x1 <- get
19631954 x2 <- get
19641955 x3 <- get
1965− x4 <- get
1966− return (PExp x1 x2 x3 x4)
1956+ return (PExp x1 x2 x3)
19671957 2 -> do x1 <- get
19681958 x2 <- get
19691959 x3 <- get
1970− x4 <- get
1971− return (PConstraint x1 x2 x3 x4)
1960+ return (PConstraint x1 x2 x3)
19721961 3 -> do x1 <- get
19731962 x2 <- get
19741963 x3 <- get
19751964 x4 <- get
19761965 x5 <- get
1977− x6 <- get
1978− return (PTacImplicit x1 x2 x3 x4 x5 x6)
1966+ return (PTacImplicit x1 x2 x3 x4 x5)
19791967 _ -> error "Corrupted binary data for PArg'"
19801968
19811969
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"]