56b6850 · Idris-dev · git.iko.soy

git.iko.soy/Idris-dev

Precise highlighting of instances

commit56b6850542e703076d81923596f491debe312926 authorDavid Raymond Christiansen <david@davidchristiansen.dk> dateMon 11 May 2015, 15:36 (11 years ago) parentcc83850

13 files changed+122−95

compare with master

unifiedsplit

src/Idris/AbsSyntax.hs+5−4 src/Idris/AbsSyntaxTree.hs+14−12 src/Idris/DeepSeq.hs+8−4 src/Idris/Docs.hs+2−2 src/Idris/Elab/Class.hs+43−30 src/Idris/Elab/Instance.hs+5−4 src/Idris/Elab/Type.hs+2−1 src/Idris/ElabDecls.hs+4−4 src/Idris/IBC.hs+8−4 src/Idris/ParseExpr.hs+8−7 src/Idris/ParseHelpers.hs+4−4 src/Idris/Parser.hs+16−16 src/Idris/REPL.hs+3−3

src/Idris/AbsSyntax.hs+5−4

@@ -1101,20 +1101,21 @@ expandParamsD rhs ist dec ps ns (PParams f params pds)

11011101-- (map (expandParamsD ist dec ps ns) pds)

11021102expandParamsD rhs ist dec ps ns (PMutual f pds)

11031103 = PMutual f (map (expandParamsD rhs ist dec ps ns) pds)

1104−expandParamsD rhs ist dec ps ns (PClass doc info f cs n params pDocs fds decls cn cd)

1104+expandParamsD rhs ist dec ps ns (PClass doc info f cs n nfc params pDocs fds decls cn cd)

11051105 = PClass doc info f

11061106 (map (\ (n, t) -> (n, expandParams dec ps ns [] t)) cs)

1107− n

1108− (map (mapsnd (expandParams dec ps ns [])) params)

1107+ n nfc

1108+ (map (\(n, fc, t) -> (n, fc, expandParams dec ps ns [] t)) params)

11091109 pDocs

11101110 fds

11111111 (map (expandParamsD rhs ist dec ps ns) decls)

11121112 cn

11131113 cd

1114−expandParamsD rhs ist dec ps ns (PInstance doc argDocs info f cs n params ty cn decls)

1114+expandParamsD rhs ist dec ps ns (PInstance doc argDocs info f cs n nfc params ty cn decls)

11151115 = PInstance doc argDocs info f

11161116 (map (\ (n, t) -> (n, expandParams dec ps ns [] t)) cs)

11171117 n

1118+ nfc

11181119 (map (expandParams dec ps ns []) params)

11191120 (expandParams dec ps ns [] ty)

11201121 cn

src/Idris/AbsSyntaxTree.hs+14−12

@@ -614,20 +614,22 @@ data PDecl' t

614614 | PClass (Docstring (Either Err PTerm)) SyntaxInfo FC

615615 [(Name, t)] -- constraints

616616 Name -- class name

617− [(Name, t)] -- parameters

617+ FC -- accurate location of class name

618+ [(Name, FC, t)] -- parameters and precise locations

618619 [(Name, Docstring (Either Err PTerm))] -- parameter docstrings

619− [Name] -- determining parameters

620+ [(Name, FC)] -- determining parameters and precise locations

620621 [PDecl' t] -- declarations

621− (Maybe Name) -- instance constructor name

622+ (Maybe (Name, FC)) -- instance constructor name and location

622623 (Docstring (Either Err PTerm)) -- instance constructor docs

623624 -- ^ Type class: arguments are documentation, syntax info, source location, constraints,

624− -- class name, parameters, method declarations, optional constructor name

625+ -- class name, class name location, parameters, method declarations, optional constructor name

625626 | PInstance

626627 (Docstring (Either Err PTerm)) -- Instance docs

627628 [(Name, Docstring (Either Err PTerm))] -- Parameter docs

628629 SyntaxInfo

629630 FC [(Name, t)] -- constraints

630631 Name -- class

632+ FC -- precise location of class

631633 [t] -- parameters

632634 t -- full instance type

633635 (Maybe Name) -- explicit name

@@ -742,8 +744,8 @@ declared (PData _ _ _ _ _ (PLaterdecl n _ _)) = [n]

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

743745declared (PNamespace _ ds) = concatMap declared ds

744746declared (PRecord _ _ _ _ n _ _ _ _ cn _ _) = n : map fst (maybeToList cn)

745−declared (PClass _ _ _ _ n _ _ _ ms cn cd) = n : (maybeToList cn ++ concatMap declared ms)

746−declared (PInstance _ _ _ _ _ _ _ _ _ _) = []

747+declared (PClass _ _ _ _ n _ _ _ _ ms cn cd) = n : (map fst (maybeToList cn) ++ concatMap declared ms)

748+declared (PInstance _ _ _ _ _ _ _ _ _ _ _) = []

747749declared (PDSL n _) = [n]

748750declared (PSyntax _ _) = []

749751declared (PMutual _ ds) = concatMap declared ds

@@ -762,8 +764,8 @@ tldeclared (PData _ _ _ _ _ (PDatadecl n _ _ ts)) = n : map fstt ts

762764tldeclared (PParams _ _ ds) = []

763765tldeclared (PMutual _ ds) = concatMap tldeclared ds

764766tldeclared (PNamespace _ ds) = concatMap tldeclared ds

765−tldeclared (PClass _ _ _ _ n _ _ _ ms cn _) = n : (maybeToList cn ++ concatMap tldeclared ms)

766−tldeclared (PInstance _ _ _ _ _ _ _ _ _ _) = []

767+tldeclared (PClass _ _ _ _ n _ _ _ _ ms cn _) = n : (map fst (maybeToList cn) ++ concatMap tldeclared ms)

768+tldeclared (PInstance _ _ _ _ _ _ _ _ _ _ _) = []

767769tldeclared _ = []

768770

769771defined :: PDecl -> [Name]

@@ -778,8 +780,8 @@ defined (PData _ _ _ _ _ (PLaterdecl n _ _)) = []

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

779781defined (PNamespace _ ds) = concatMap defined ds

780782defined (PRecord _ _ _ _ n _ _ _ _ cn _ _) = n : map fst (maybeToList cn)

781−defined (PClass _ _ _ _ n _ _ _ ms cn _) = n : (maybeToList cn ++ concatMap defined ms)

782−defined (PInstance _ _ _ _ _ _ _ _ _ _) = []

783+defined (PClass _ _ _ _ n _ _ _ _ ms cn _) = n : (map fst (maybeToList cn) ++ concatMap defined ms)

784+defined (PInstance _ _ _ _ _ _ _ _ _ _ _) = []

783785defined (PDSL n _) = [n]

784786defined (PSyntax _ _) = []

785787defined (PMutual _ ds) = concatMap defined ds

@@ -1791,9 +1793,9 @@ showDeclImp o (PData _ _ _ _ _ d) = showDImp o { ppopt_impl = True } d

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

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

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

1794−showDeclImp o (PClass _ _ _ cs n ps _ _ ds _ _)

1796+showDeclImp o (PClass _ _ _ cs n _ ps _ _ ds _ _)

17951797 = text "class" <+> text (show cs) <+> text (show n) <+> text (show ps) <> line <> showDecls o ds

1796−showDeclImp o (PInstance _ _ _ _ cs n _ t _ ds)

1798+showDeclImp o (PInstance _ _ _ _ cs n _ _ t _ ds)

17971799 = text "instance" <+> text (show cs) <+> text (show n) <+> prettyImp o t <> line <> showDecls o ds

17981800showDeclImp _ _ = text "..."

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

src/Idris/DeepSeq.hs+8−4

@@ -158,7 +158,7 @@ instance (NFData t) => NFData (PDecl' t) where

158158 rnf x8 `seq`

159159 rnf x9 `seq`

160160 rnf x10 `seq` rnf x11 `seq` rnf x12 `seq` ()

161− rnf (PClass x1 x2 x3 x4 x5 x6 x8 x7 x9 x10 x11)

161+ rnf (PClass x1 x2 x3 x4 x5 x6 x8 x7 x9 x10 x11 x12)

162162 = rnf x1 `seq`

163163 rnf x2 `seq`

164164 rnf x3 `seq`

@@ -167,15 +167,19 @@ instance (NFData t) => NFData (PDecl' t) where

167167 rnf x6 `seq`

168168 rnf x7 `seq`

169169 rnf x8 `seq`

170− rnf x9 `seq` rnf x10 `seq` rnf x11 `seq` ()

171− rnf (PInstance x1 x2 x3 x4 x5 x6 x7 x8 x9 x10)

170+ rnf x9 `seq`

171+ rnf x10 `seq`

172+ rnf x11 `seq` rnf x12 `seq` ()

173+ rnf (PInstance x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11)

172174 = rnf x1 `seq`

173175 rnf x2 `seq`

174176 rnf x3 `seq`

175177 rnf x4 `seq`

176178 rnf x5 `seq`

177179 rnf x6 `seq`

178− rnf x7 `seq` rnf x8 `seq` rnf x9 `seq` rnf x10 `seq` ()

180+ rnf x7 `seq`

181+ rnf x8 `seq`

182+ rnf x9 `seq` rnf x10 `seq` rnf x11 `seq` ()

179183 rnf (PDSL x1 x2) = rnf x1 `seq` rnf x2 `seq` ()

180184 rnf (PSyntax x1 x2) = rnf x1 `seq` rnf x2 `seq` ()

181185 rnf (PMutual x1 x2) = rnf x1 `seq` rnf x2 `seq` ()

src/Idris/Docs.hs+2−2

@@ -271,8 +271,8 @@ docClass n ci

271271 namedInst n@(UN _) = Just n

272272 namedInst _ = Nothing

273273

274− getDInst (PInstance _ _ _ _ _ _ _ t _ _) = Just t

275− getDInst _ = Nothing

274+ getDInst (PInstance _ _ _ _ _ _ _ _ t _ _) = Just t

275+ getDInst _ = Nothing

276276

277277 isSubclass (PPi (Constraint _ _) _ _ (PApp _ _ args) (PApp _ (PRef _ nm) args'))

278278 = nm == n && map getTm args == map getTm args'

src/Idris/Elab/Class.hs+43−30

@@ -15,7 +15,7 @@ import Idris.Primitives

1515import Idris.Inliner

1616import Idris.PartialEval

1717import Idris.DeepSeq

18−import Idris.Output (iputStrLn, pshow, iWarn)

18+import Idris.Output (iputStrLn, pshow, iWarn, sendHighlighting)

1919import IRTS.Lang

2020

2121import Idris.Elab.Type

@@ -54,18 +54,22 @@ data MArgTy = IA Name | EA Name | CA deriving Show

5454

5555elabClass :: ElabInfo -> SyntaxInfo -> Docstring (Either Err PTerm) ->

5656 FC -> [(Name, PTerm)] ->

57− Name -> [(Name, PTerm)] -> [(Name, Docstring (Either Err PTerm))] ->

58− [Name] -> [PDecl] ->

59− Maybe Name {- ^ instance ctor name -} ->

57+ Name -> FC -> [(Name, FC, PTerm)] -> [(Name, Docstring (Either Err PTerm))] ->

58+ [(Name, FC)] {- ^ determining params -} ->

59+ [PDecl] {- ^ class body -} ->

60+ Maybe (Name, FC) {- ^ instance ctor name and location -} ->

6061 Docstring (Either Err PTerm) {- ^ instance ctor docs -} ->

6162 Idris ()

62−elabClass info syn_in doc fc constraints tn ps pDocs fds ds mcn cd

63− = do let cn = fromMaybe (SN (InstanceCtorN tn)) mcn

64− let tty = pibind ps (PType fc)

63+elabClass info syn_in doc fc constraints tn tnfc ps pDocs fds ds mcn cd

64+ = do let cn = fromMaybe (SN (InstanceCtorN tn)) (fst <$> mcn)

65+ let tty = pibind (map (\(n, _, ty) -> (n, ty)) ps) (PType fc)

6566 let constraint = PApp fc (PRef fc tn)

66− (map (pexp . PRef fc) (map fst ps))

67+ (map (pexp . PRef fc) (map (\(n, _, _) -> n) ps))

6768

68− let syn = syn_in { using = addToUsing (using syn_in) ps }

69+ let syn =

70+ syn_in { using = addToUsing (using syn_in)

71+ [(pn, pt) | (pn, _, pt) <- ps]

72+ }

6973

7074 -- build data declaration

7175 let mdecls = filter tydecl ds -- method declarations

@@ -77,10 +81,10 @@ elabClass info syn_in doc fc constraints tn ps pDocs fds ds mcn cd

7781 defs <- mapM (defdecl (map (\ (x,y,z) -> z) ims) constraint)

7882 (filter clause ds)

7983 let (methods, imethods)

80− = unzip (map (\ ( x,y,z) -> (x, y)) ims)

84+ = unzip (map (\ (x, y, z) -> (x, y)) ims)

8185 let defaults = map (\ (x, (y, z)) -> (x,y)) defs

8286 -- build instance constructor type

83− let cty = impbind ps $ conbind constraints

87+ let cty = impbind [(pn, pt) | (pn, _, pt) <- ps] $ conbind constraints

8488 $ pibind (map (\ (n, ty) -> (nsroot n, ty)) methods)

8589 constraint

8690

@@ -91,8 +95,8 @@ elabClass info syn_in doc fc constraints tn ps pDocs fds ds mcn cd

9195 -- Elaborate the data declaration

9296 elabData info (syn { no_imp = no_imp syn ++ mnames,

9397 imp_methods = mnames }) doc pDocs fc [] ddecl

94− dets <- findDets cn fds

95− addClass tn (CI cn (map nodoc imethods) defaults idecls (map fst ps) [] dets)

98+ dets <- findDets cn (map fst fds)

99+ addClass tn (CI cn (map nodoc imethods) defaults idecls (map (\(n, _, _) -> n) ps) [] dets)

96100

97101 -- for each constraint, build a top level function to chase it

98102 cfns <- mapM (cfun cn constraint syn (map fst imethods)) constraints

@@ -108,8 +112,16 @@ elabClass info syn_in doc fc constraints tn ps pDocs fds ds mcn cd

108112 -- add the default definitions

109113 mapM_ (rec_elabDecl info EAll info) (concat (map (snd.snd) defs))

110114 addIBC (IBCClass tn)

115+

116+ sendHighlighting $

117+ [(tnfc, AnnName tn Nothing Nothing Nothing)] ++

118+ [(pnfc, AnnBoundName pn False) | (pn, pnfc, _) <- ps] ++

119+ [(fdfc, AnnBoundName fc False) | (fc, fdfc) <- fds] ++

120+ maybe [] (\(conN, conNFC) -> [(conNFC, AnnName conN Nothing Nothing Nothing)]) mcn

121+

111122 where

112− nodoc (n, (_, o, t)) = (n, (o, t))

123+ nodoc (n, (_, _, o, t)) = (n, (o, t))

124+

113125 pibind [] x = x

114126 pibind ((n, ty): ns) x = PPi expl n NoFC ty (pibind ns (chkUniq ty x))

115127

@@ -127,7 +139,7 @@ elabClass info syn_in doc fc constraints tn ps pDocs fds ds mcn cd

127139

128140 -- TODO: probably should normalise

129141 checkDefaultSuperclassInstance :: PDecl -> Idris ()

130− checkDefaultSuperclassInstance (PInstance _ _ _ fc cs n ps _ _ _)

142+ checkDefaultSuperclassInstance (PInstance _ _ _ fc cs n _ ps _ _ _)

131143 = do when (not $ null cs) . tclift

132144 $ tfail (At fc (Msg $ "Default superclass instances can't have constraints."))

133145 i <- getIState

@@ -147,23 +159,24 @@ elabClass info syn_in doc fc constraints tn ps pDocs fds ds mcn cd

147159

148160 getMName (PTy _ _ _ _ _ n nfc _) = nsroot n

149161 tdecl allmeths (PTy doc _ syn _ o n nfc t)

150− = do t' <- implicit' info syn (map fst ps ++ allmeths) n t

162+ = do t' <- implicit' info syn (map (\(n, _, _) -> n) ps ++ allmeths) n t

151163 logLvl 2 $ "Method " ++ show n ++ " : " ++ showTmImpls t'

152− return ( (n, (toExp (map fst ps) Exp t')),

153− (n, (doc, o, (toExp (map fst ps)

154− (\ l s p -> Imp l s p Nothing) t'))),

155− (n, (syn, o, t) ) )

164+ return ( (n, (toExp (map (\(pn, _, _) -> pn) ps) Exp t')),

165+ (n, (nfc, doc, o, (toExp (map (\(pn, _, _) -> pn) ps)

166+ (\ l s p -> Imp l s p Nothing) t'))),

167+ (n, (nfc, syn, o, t) ) )

156168 tdecl _ _ = ifail "Not allowed in a class declaration"

157169

158170 -- Create default definitions

159171 defdecl mtys c d@(PClauses fc opts n cs) =

160172 case lookup n mtys of

161− Just (syn, o, ty) -> do let ty' = insertConstraint c ty

162− let ds = map (decorateid defaultdec)

163− [PTy emptyDocstring [] syn fc [] n NoFC ty',

164− PClauses fc (o ++ opts) n cs]

165− iLOG (show ds)

166− return (n, ((defaultdec n, ds!!1), ds))

173+ Just (nfc, syn, o, ty) ->

174+ do let ty' = insertConstraint c ty

175+ let ds = map (decorateid defaultdec)

176+ [PTy emptyDocstring [] syn fc [] n nfc ty',

177+ PClauses fc (o ++ opts) n cs]

178+ iLOG (show ds)

179+ return (n, ((defaultdec n, ds!!1), ds))

167180 _ -> ifail $ show n ++ " is not a method"

168181 defdecl _ _ _ = ifail "Can't happen (defdecl)"

169182

@@ -172,7 +185,7 @@ elabClass info syn_in doc fc constraints tn ps pDocs fds ds mcn cd

172185

173186 tydecl (PTy _ _ _ _ _ _ _ _) = True

174187 tydecl _ = False

175− instdecl (PInstance _ _ _ _ _ _ _ _ _ _) = True

188+ instdecl (PInstance _ _ _ _ _ _ _ _ _ _ _) = True

176189 instdecl _ = False

177190 clause (PClauses _ _ _ _) = True

178191 clause _ = False

@@ -204,7 +217,7 @@ elabClass info syn_in doc fc constraints tn ps pDocs fds ds mcn cd

204217

205218 -- Generate a top level function which looks up a method in a given

206219 -- dictionary (this is inlinable, always)

207− tfun cn c syn all (m, (doc, o, ty))

220+ tfun cn c syn all (m, (mfc, doc, o, ty))

208221 = do let ty' = expandMethNS syn (insertConstraint c ty)

209222 let mnames = take (length all) $ map (\x -> sMN x "meth") [0..]

210223 let capp = PApp fc (PRef fc cn) (map (pexp . PRef fc) mnames)

@@ -215,7 +228,7 @@ elabClass info syn_in doc fc constraints tn ps pDocs fds ds mcn cd

215228 logLvl 2 ("Top level type: " ++ showTmImpls ty')

216229 iLOG (show (m, ty', capp, margs))

217230 logLvl 2 ("Definition: " ++ showTmImpls lhs ++ " = " ++ showTmImpls rhs)

218− return [PTy doc [] syn fc o m NoFC ty',

231+ return [PTy doc [] syn fc o m mfc ty',

219232 PClauses fc [Inlinable] m [PClause fc m lhs [] rhs []]]

220233

221234 getMArgs (PPi (Imp _ _ _ _) n _ ty sc) = IA n : getMArgs sc

@@ -253,7 +266,7 @@ memberDocs (PTy d _ _ _ _ n _ _) = Just (basename n, d)

253266memberDocs (PPostulate _ d _ _ _ n _) = Just (basename n, d)

254267memberDocs (PData d _ _ _ _ pdata) = Just (basename $ d_name pdata, d)

255268memberDocs (PRecord d _ _ _ n _ _ _ _ _ _ _ ) = Just (basename n, d)

256−memberDocs (PClass d _ _ _ n _ _ _ _ _ _) = Just (basename n, d)

269+memberDocs (PClass d _ _ _ n _ _ _ _ _ _ _) = Just (basename n, d)

257270memberDocs _ = Nothing

258271

259272

src/Idris/Elab/Instance.hs+5−4

@@ -56,11 +56,12 @@ elabInstance :: ElabInfo -> SyntaxInfo ->

5656 ElabWhat -> -- phase

5757 FC -> [(Name, PTerm)] -> -- constraints

5858 Name -> -- the class

59+ FC -> -- precise location of class name

5960 [PTerm] -> -- class parameters (i.e. instance)

6061 PTerm -> -- full instance type

6162 Maybe Name -> -- explicit name

6263 [PDecl] -> Idris ()

63−elabInstance info syn doc argDocs what fc cs n ps t expn ds = do

64+elabInstance info syn doc argDocs what fc cs n nfc ps t expn ds = do

6465 i <- getIState

6566 (n, ci) <- case lookupCtxtName n (idris_classes i) of

6667 [c] -> return c

@@ -156,10 +157,10 @@ elabInstance info syn doc argDocs what fc cs n ps t expn ds = do

156157 Just m -> sNS (SN (sInstanceN n' (map show ps'))) m

157158 Just nm -> nm

158159

159− substInstance ips pnames (PInstance doc argDocs syn _ cs n ps t expn ds)

160− = PInstance doc argDocs syn fc cs n (map (substMatchesShadow ips pnames) ps) (substMatchesShadow ips pnames t) expn ds

160+ substInstance ips pnames (PInstance doc argDocs syn _ cs n nfc ps t expn ds)

161+ = PInstance doc argDocs syn fc cs n nfc (map (substMatchesShadow ips pnames) ps) (substMatchesShadow ips pnames t) expn ds

161162

162− isOverlapping i (PInstance doc argDocs syn _ _ n ps t expn _)

163+ isOverlapping i (PInstance doc argDocs syn _ _ n nfc ps t expn _)

163164 = case lookupCtxtName n (idris_classes i) of

164165 [(n, ci)] -> let iname = (mkiname n (namespace info) ps expn) in

165166 case lookupTy iname (tt_ctxt i) of

src/Idris/Elab/Type.hs+2−1

@@ -121,7 +121,8 @@ buildType info syn fc opts n ty' = do

121121-- | Elaborate a top-level type declaration - for example, "foo : Int -> Int".

122122elabType :: ElabInfo -> SyntaxInfo

123123 -> Docstring (Either Err PTerm) -> [(Name, Docstring (Either Err PTerm))]

124− -> FC -> FnOpts -> Name -> FC -- ^ The precise location of the name

124+ -> FC -> FnOpts

125+ -> Name -> FC -- ^ The precise location of the name

125126 -> PTerm -> Idris Type

126127elabType = elabType' False

127128

src/Idris/ElabDecls.hs+4−4

@@ -232,13 +232,13 @@ elabDecl' what info (PNamespace n ps) = mapM_ (elabDecl' what ninfo) ps

232232 ninfo = case namespace info of

233233 Nothing -> info { namespace = Just [n] }

234234 Just ns -> info { namespace = Just (n:ns) }

235−elabDecl' what info (PClass doc s f cs n ps pdocs fds ds cn cd)

235+elabDecl' what info (PClass doc s f cs n nfc ps pdocs fds ds cn cd)

236236 | what /= EDefns

237237 = do iLOG $ "Elaborating class " ++ show n

238− elabClass info (s { syn_params = [] }) doc f cs n ps pdocs fds ds cn cd

239−elabDecl' what info (PInstance doc argDocs s f cs n ps t expn ds)

238+ elabClass info (s { syn_params = [] }) doc f cs n nfc ps pdocs fds ds cn cd

239+elabDecl' what info (PInstance doc argDocs s f cs n nfc ps t expn ds)

240240 = do iLOG $ "Elaborating instance " ++ show n

241− elabInstance info s doc argDocs what f cs n ps t expn ds

241+ elabInstance info s doc argDocs what f cs n nfc ps t expn ds

242242elabDecl' what info (PRecord doc rsyn fc opts name nfc ps pdocs fs cname cdoc csyn)

243243 | what /= ETypes

244244 = do iLOG $ "Elaborating record " ++ show name

src/Idris/IBC.hs+8−4

@@ -1188,7 +1188,7 @@ instance (Binary t) => Binary (PDecl' t) where

11881188 put x10

11891189 put x11

11901190 put x12

1191− PClass x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11

1191+ PClass x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12

11921192 -> do putWord8 7

11931193 put x1

11941194 put x2

@@ -1201,7 +1201,8 @@ instance (Binary t) => Binary (PDecl' t) where

12011201 put x9

12021202 put x10

12031203 put x11

1204− PInstance x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 ->

1204+ put x12

1205+ PInstance x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 ->

12051206 do putWord8 8

12061207 put x1

12071208 put x2

@@ -1213,6 +1214,7 @@ instance (Binary t) => Binary (PDecl' t) where

12131214 put x8

12141215 put x9

12151216 put x10

1217+ put x11

12161218 PDSL x1 x2 -> do putWord8 9

12171219 put x1

12181220 put x2

@@ -1307,7 +1309,8 @@ instance (Binary t) => Binary (PDecl' t) where

13071309 x9 <- get

13081310 x10 <- get

13091311 x11 <- get

1310− return (PClass x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11)

1312+ x12 <- get

1313+ return (PClass x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12)

13111314 8 -> do x1 <- get

13121315 x2 <- get

13131316 x3 <- get

@@ -1318,7 +1321,8 @@ instance (Binary t) => Binary (PDecl' t) where

13181321 x8 <- get

13191322 x9 <- get

13201323 x10 <- get

1321− return (PInstance x1 x2 x3 x4 x5 x6 x7 x8 x9 x10)

1324+ x11 <- get

1325+ return (PInstance x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11)

13221326 9 -> do x1 <- get

13231327 x2 <- get

13241328 return (PDSL x1 x2)

src/Idris/ParseExpr.hs+8−7

@@ -372,8 +372,9 @@ Bracketed ::= '(' Bracketed'

372372@

373373 -}

374374bracketed :: SyntaxInfo -> IdrisParser PTerm

375−bracketed syn = do lchar '(' <?> "parenthesized expression"

376− bracketed' syn

375+bracketed syn = do fc <- getFC

376+ lchar '(' <?> "parenthesized expression"

377+ bracketed' fc syn

377378{- |Parses the rest of an expression in braces

378379@

379380Bracketed' ::=

@@ -387,11 +388,11 @@ Bracketed' ::=

387388 ;

388389@

389390-}

390−bracketed' :: SyntaxInfo -> IdrisParser PTerm

391−bracketed' syn =

392− do lchar ')'

393− fc <- getFC

394− return $ PTrue fc TypeOrTerm

391+bracketed' :: FC -> SyntaxInfo -> IdrisParser PTerm

392+bracketed' open syn =

393+ do (FC f start (l, c)) <- getFC

394+ lchar ')'

395+ return $ PTrue (spanFC open (FC f start (l, c+1))) TypeOrTerm

395396 <|> try (do ln <- fst <$> name; lchar ':';

396397 lty <- expr syn

397398 reservedOp "**"

src/Idris/ParseHelpers.hs+4−4

@@ -633,9 +633,9 @@ collect (c@(PClauses _ o _ _) : ds)

633633collect (PParams f ns ps : ds) = PParams f ns (collect ps) : collect ds

634634collect (PMutual f ms : ds) = PMutual f (collect ms) : collect ds

635635collect (PNamespace ns ps : ds) = PNamespace ns (collect ps) : collect ds

636−collect (PClass doc f s cs n ps pdocs fds ds cn cd : ds')

637− = PClass doc f s cs n ps pdocs fds (collect ds) cn cd : collect ds'

638−collect (PInstance doc argDocs f s cs n ps t en ds : ds')

639− = PInstance doc argDocs f s cs n ps t en (collect ds) : collect ds'

636+collect (PClass doc f s cs n nfc ps pdocs fds ds cn cd : ds')

637+ = PClass doc f s cs n nfc ps pdocs fds (collect ds) cn cd : collect ds'

638+collect (PInstance doc argDocs f s cs n nfc ps t en ds : ds')

639+ = PInstance doc argDocs f s cs n nfc ps t en (collect ds) : collect ds'

640640collect (d : ds) = d : collect ds

641641collect [] = []

src/Idris/Parser.hs+16−16

@@ -630,7 +630,7 @@ ClassBlock ::=

630630 ;

631631@

632632-}

633−classBlock :: SyntaxInfo -> IdrisParser (Maybe Name, Docstring (Either Err PTerm), [PDecl])

633+classBlock :: SyntaxInfo -> IdrisParser (Maybe (Name, FC), Docstring (Either Err PTerm), [PDecl])

634634classBlock syn = do reserved "where"

635635 openBlock

636636 (cn, cd) <- option (Nothing, emptyDocstring) $

@@ -646,8 +646,8 @@ classBlock syn = do reserved "where"

646646 <?> "class block"

647647

648648 where

649− constructor :: IdrisParser Name

650− constructor = reserved "constructor" *> (fst <$> fnName)

649+ constructor :: IdrisParser (Name, FC)

650+ constructor = reserved "constructor" *> fnName

651651

652652 annotate :: SyntaxInfo -> IState -> Docstring () -> Docstring (Either Err PTerm)

653653 annotate syn ist = annotCode $ tryFullExpr syn ist

@@ -676,24 +676,24 @@ class_ syn = do (doc, argDocs, acc)

676676 fc <- getFC

677677 cons <- constraintList syn

678678 let cons' = [(c, ty) | (c, _, ty) <- cons]

679− n_in <- fst <$> fnName

679+ (n_in, nfc) <- fnName

680680 let n = expandNS syn n_in

681681 cs <- many carg

682− fds <- option (map fst cs) fundeps

682+ fds <- option [(cn, NoFC) | (cn, _, _) <- cs] fundeps

683683 (cn, cd, ds) <- option (Nothing, fst noDocs, []) (classBlock syn)

684684 accData acc n (concatMap declared ds)

685− return [PClass doc syn fc cons' n cs argDocs fds ds cn cd]

685+ return [PClass doc syn fc cons' n nfc cs argDocs fds ds cn cd]

686686 <?> "type-class declaration"

687687 where

688− fundeps :: IdrisParser [Name]

689− fundeps = do lchar '|'; sepBy (fst <$> name) (lchar ',')

688+ fundeps :: IdrisParser [(Name, FC)]

689+ fundeps = do lchar '|'; sepBy name (lchar ',')

690690

691− carg :: IdrisParser (Name, PTerm)

692− carg = do lchar '('; i <- (fst <$> name); lchar ':'; ty <- expr syn; lchar ')'

693− return (i, ty)

694− <|> do i <- fst <$> name

691+ carg :: IdrisParser (Name, FC, PTerm)

692+ carg = do lchar '('; (i, ifc) <- name; lchar ':'; ty <- expr syn; lchar ')'

693+ return (i, ifc, ty)

694+ <|> do (i, ifc) <- name

695695 fc <- getFC

696− return (i, PType fc)

696+ return (i, ifc, PType fc)

697697

698698{- | Parses a type class instance declaration

699699

@@ -714,12 +714,12 @@ instance_ syn = do (doc, argDocs)

714714 en <- optional instanceName

715715 cs <- constraintList syn

716716 let cs' = [(c, ty) | (c, _, ty) <- cs]

717− cn <- fst <$> fnName

717+ (cn, cnfc) <- fnName

718718 args <- many (simpleExpr syn)

719− let sc = PApp fc (PRef fc cn) (map pexp args)

719+ let sc = PApp fc (PRef cnfc cn) (map pexp args)

720720 let t = bindList (PPi constraint) cs sc

721721 ds <- option [] (instanceBlock syn)

722− return [PInstance doc argDocs syn fc cs' cn args t en ds]

722+ return [PInstance doc argDocs syn fc cs' cn cnfc args t en ds]

723723 <?> "instance declaration"

724724 where instanceName :: IdrisParser Name

725725 instanceName = do lchar '['; n_in <- fst <$> fnName; lchar ']'

src/Idris/REPL.hs+3−3

@@ -791,7 +791,7 @@ process fn (NewDefn decls) = do

791791 getName (PTy docs argdocs syn fc opts name _ ty) = Just name

792792 getName (PClauses fc opts name (clause:clauses)) = Just (getClauseName clause)

793793 getName (PData doc argdocs syn fc opts dataDecl) = Just (d_name dataDecl)

794− getName (PClass doc syn fc constraints name parms parmdocs fds decls _ _) = Just name

794+ getName (PClass doc syn fc constraints name nfc parms parmdocs fds decls _ _) = Just name

795795 getName _ = Nothing

796796 -- getClauseName is partial and I am not sure it's used safely! -- trillioneyes

797797 getClauseName (PClause fc name whole with rhs whereBlock) = name

@@ -839,8 +839,8 @@ process fn (NewDefn decls) = do

839839 fixClauses :: PDecl' t -> PDecl' t

840840 fixClauses (PClauses fc opts _ css@(clause:cs)) =

841841 PClauses fc opts (getClauseName clause) css

842− fixClauses (PInstance doc argDocs syn fc constraints cls parms ty instName decls) =

843− PInstance doc argDocs syn fc constraints cls parms ty instName (map fixClauses decls)

842+ fixClauses (PInstance doc argDocs syn fc constraints cls nfc parms ty instName decls) =

843+ PInstance doc argDocs syn fc constraints cls nfc parms ty instName (map fixClauses decls)

844844 fixClauses decl = decl

845845

846846process fn (Undefine names) = undefine names