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

git.iko.soy/Idris-dev

on master help sign in

Precise highlighting of instances

56b6850David Raymond Christiansen11 years ago

src/Idris/AbsSyntax.hs+5−4

compare with master

unifiedsplit

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

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

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

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

1105 = PClass doc info f

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

1107− n

1107+ n nfc

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

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

1109 pDocs

1110 fds

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

1112 cn

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

1115 = PInstance doc argDocs info f

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

1117 n

1118+ nfc

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

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

1119 (expandParams dec ps ns [] ty)

1120 (expandParams dec ps ns [] ty)

1120 cn

1121 cn

src/Idris/AbsSyntaxTree.hs+14−12

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

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

615 [(Name, t)] -- constraints

616 Name -- class name

617+ FC -- accurate location of class name

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

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

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

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

619− [Name] -- determining parameters

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

620 [PDecl' t] -- declarations

621 [PDecl' t] -- declarations

621− (Maybe Name) -- instance constructor name

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

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

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

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

624 -- ^ 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

625 | PInstance

626 | PInstance

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

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

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

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

628 SyntaxInfo

629 SyntaxInfo

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

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

630 Name -- class

631 Name -- class

632+ FC -- precise location of class

631 [t] -- parameters

633 [t] -- parameters

632 t -- full instance type

634 t -- full instance type

633 (Maybe Name) -- explicit name

635 (Maybe Name) -- explicit name

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

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

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

743declared (PNamespace _ ds) = concatMap declared ds

745declared (PNamespace _ ds) = concatMap declared ds

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

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

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

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

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

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

747declared (PDSL n _) = [n]

749declared (PDSL n _) = [n]

748declared (PSyntax _ _) = []

750declared (PSyntax _ _) = []

749declared (PMutual _ ds) = concatMap declared ds

751declared (PMutual _ ds) = concatMap declared ds

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

762tldeclared (PParams _ _ ds) = []

764tldeclared (PParams _ _ ds) = []

763tldeclared (PMutual _ ds) = concatMap tldeclared ds

765tldeclared (PMutual _ ds) = concatMap tldeclared ds

764tldeclared (PNamespace _ ds) = concatMap tldeclared ds

766tldeclared (PNamespace _ ds) = concatMap tldeclared ds

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

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

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

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

767tldeclared _ = []

769tldeclared _ = []

768

770

769defined :: PDecl -> [Name]

771defined :: PDecl -> [Name]

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

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

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

779defined (PNamespace _ ds) = concatMap defined ds

781defined (PNamespace _ ds) = concatMap defined ds

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

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

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

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

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

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

783defined (PDSL n _) = [n]

785defined (PDSL n _) = [n]

784defined (PSyntax _ _) = []

786defined (PSyntax _ _) = []

785defined (PMutual _ ds) = concatMap defined ds

787defined (PMutual _ ds) = concatMap defined ds

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

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

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

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

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

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

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

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

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

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

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

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

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

1798showDeclImp _ _ = text "..."

1800showDeclImp _ _ = text "..."

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

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

src/Idris/DeepSeq.hs+8−4

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

158 rnf x8 `seq`

159 rnf x9 `seq`

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

162 = rnf x1 `seq`

163 rnf x2 `seq`

164 rnf x3 `seq`

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

167 rnf x6 `seq`

168 rnf x7 `seq`

169 rnf x8 `seq`

170+ rnf x9 `seq`

171+ rnf x10 `seq`

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

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

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

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

172 = rnf x1 `seq`

174 = rnf x1 `seq`

173 rnf x2 `seq`

175 rnf x2 `seq`

174 rnf x3 `seq`

176 rnf x3 `seq`

175 rnf x4 `seq`

177 rnf x4 `seq`

176 rnf x5 `seq`

178 rnf x5 `seq`

177 rnf x6 `seq`

179 rnf x6 `seq`

180+ rnf x7 `seq`

181+ rnf x8 `seq`

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

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

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

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

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

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

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

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

src/Idris/Docs.hs+2−2

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

271 namedInst n@(UN _) = Just n

272 namedInst _ = Nothing

273

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

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

275− getDInst _ = Nothing

275+ getDInst _ = Nothing

276

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

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

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

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

15import Idris.Inliner

16import Idris.PartialEval

17import Idris.DeepSeq

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

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

19import IRTS.Lang

21import Idris.Elab.Type

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

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

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

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

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

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

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

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

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

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

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

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

61 Idris ()

62 Idris ()

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

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

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

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

64− let tty = pibind ps (PType fc)

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

65 let constraint = PApp fc (PRef fc tn)

66 let constraint = PApp fc (PRef fc tn)

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

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

69+ let syn =

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

70+ syn_in { using = addToUsing (using syn_in)

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

72+ }

70 -- build data declaration

74 -- build data declaration

71 let mdecls = filter tydecl ds -- method declarations

75 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

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

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

78 (filter clause ds)

82 (filter clause ds)

79 let (methods, imethods)

83 let (methods, imethods)

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

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

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

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

82 -- build instance constructor type

86 -- build instance constructor type

83− let cty = impbind ps $ conbind constraints

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

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

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

85 constraint

89 constraint

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

91 -- Elaborate the data declaration

95 -- Elaborate the data declaration

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

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

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

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

94− dets <- findDets cn fds

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

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

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

100

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

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

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

102 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

108 -- add the default definitions

112 -- add the default definitions

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

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

110 addIBC (IBCClass tn)

114 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+

111 where

122 where

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

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

124+

113 pibind [] x = x

125 pibind [] x = x

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

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

115

127

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

127

139

128 -- TODO: probably should normalise

140 -- TODO: probably should normalise

129 checkDefaultSuperclassInstance :: PDecl -> Idris ()

141 checkDefaultSuperclassInstance :: PDecl -> Idris ()

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

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

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

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

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

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

133 i <- getIState

145 i <- getIState

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

147

159

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

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

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

161 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

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

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

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

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

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

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

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

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

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

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

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

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

157

169

158 -- Create default definitions

170 -- Create default definitions

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

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

160 case lookup n mtys of

172 case lookup n mtys of

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

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

174+ do let ty' = insertConstraint c ty

162− let ds = map (decorateid defaultdec)

175+ let ds = map (decorateid defaultdec)

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

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

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

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

165− iLOG (show ds)

178+ iLOG (show ds)

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

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

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

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

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

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

169

182

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

172

185

173 tydecl (PTy _ _ _ _ _ _ _ _) = True

186 tydecl (PTy _ _ _ _ _ _ _ _) = True

174 tydecl _ = False

187 tydecl _ = False

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

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

176 instdecl _ = False

189 instdecl _ = False

177 clause (PClauses _ _ _ _) = True

190 clause (PClauses _ _ _ _) = True

178 clause _ = False

191 clause _ = False

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

204

217

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

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

206 -- dictionary (this is inlinable, always)

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

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

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

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

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

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

223 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

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

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

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

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

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

230 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',

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

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

220

233

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

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

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

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

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

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

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

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

268memberDocs (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)

257memberDocs _ = Nothing

270memberDocs _ = Nothing

258

271

259

272

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

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

56 ElabWhat -> -- phase

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

58 Name -> -- the class

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

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

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

60 PTerm -> -- full instance type

61 PTerm -> -- full instance type

61 Maybe Name -> -- explicit name

62 Maybe Name -> -- explicit name

62 [PDecl] -> Idris ()

63 [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

64 i <- getIState

65 i <- getIState

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

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

66 [c] -> return c

67 [c] -> return c

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

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

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

157 Just nm -> nm

158 Just nm -> nm

158

159

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

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

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

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

161

162

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

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

163 = case lookupCtxtName n (idris_classes i) of

164 = case lookupCtxtName n (idris_classes i) of

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

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

165 case lookupTy iname (tt_ctxt i) of

166 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

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

122elabType :: ElabInfo -> SyntaxInfo

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

124+ -> FC -> FnOpts

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

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

125 -> PTerm -> Idris Type

126 -> PTerm -> Idris Type

126elabType = elabType' False

127elabType = elabType' False

127

128

src/Idris/ElabDecls.hs+4−4

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

232 ninfo = case namespace info of

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

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

236 | what /= EDefns

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

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

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 ps t expn ds)

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

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

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

243 | what /= ETypes

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

src/Idris/IBC.hs+8−4

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

1188 put x10

1189 put x11

1190 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

1192 -> do putWord8 7

1193 put x1

1194 put x2

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

1201 put x9

1202 put x10

1203 put x11

1204+ put x12

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

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

1205 do putWord8 8

1206 do putWord8 8

1206 put x1

1207 put x1

1207 put x2

1208 put x2

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

1213 put x8

1214 put x8

1214 put x9

1215 put x9

1215 put x10

1216 put x10

1217+ put x11

1216 PDSL x1 x2 -> do putWord8 9

1218 PDSL x1 x2 -> do putWord8 9

1217 put x1

1219 put x1

1218 put x2

1220 put x2

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

1307 x9 <- get

1309 x9 <- get

1308 x10 <- get

1310 x10 <- get

1309 x11 <- get

1311 x11 <- get

1312+ x12 <- get

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

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

1311 8 -> do x1 <- get

1314 8 -> do x1 <- get

1312 x2 <- get

1315 x2 <- get

1313 x3 <- get

1316 x3 <- get

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

1318 x8 <- get

1321 x8 <- get

1319 x9 <- get

1322 x9 <- get

1320 x10 <- get

1323 x10 <- get

1324+ x11 <- get

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

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

1322 9 -> do x1 <- get

1326 9 -> do x1 <- get

1323 x2 <- get

1327 x2 <- get

1324 return (PDSL x1 x2)

1328 return (PDSL x1 x2)

src/Idris/ParseExpr.hs+8−7

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

372@

373 -}

374bracketed :: SyntaxInfo -> IdrisParser PTerm

375+bracketed syn = do fc <- getFC

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

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

376− bracketed' syn

377+ bracketed' fc syn

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

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

378@

379@

379Bracketed' ::=

380Bracketed' ::=

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

387 ;

388 ;

388@

389@

389-}

390-}

390−bracketed' :: SyntaxInfo -> IdrisParser PTerm

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

391−bracketed' syn =

392+bracketed' open syn =

392− do lchar ')'

393− fc <- getFC

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

394+ lchar ')'

394− return $ PTrue fc TypeOrTerm

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

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

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

396 lty <- expr syn

397 lty <- expr syn

397 reservedOp "**"

398 reservedOp "**"

src/Idris/ParseHelpers.hs+4−4

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

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

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

635collect (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')

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

637− = PClass doc f s cs n ps pdocs fds (collect ds) cn cd : collect 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 ps t en ds : ds')

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

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

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

640collect (d : ds) = d : collect ds

641collect [] = []

src/Idris/Parser.hs+16−16

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

630 ;

631@

632-}

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

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

634classBlock syn = do reserved "where"

635 openBlock

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

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

646 <?> "class block"

647

648 where

649− constructor :: IdrisParser Name

649+ constructor :: IdrisParser (Name, FC)

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

650+ constructor = reserved "constructor" *> fnName

651

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

653 annotate syn ist = annotCode $ tryFullExpr syn ist

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

676 fc <- getFC

677 cons <- constraintList syn

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

679− n_in <- fst <$> fnName

679+ (n_in, nfc) <- fnName

680 let n = expandNS syn n_in

681 cs <- many carg

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

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

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

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

686 <?> "type-class declaration"

687 where

688− fundeps :: IdrisParser [Name]

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

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

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

690

691− carg :: IdrisParser (Name, PTerm)

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

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

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

693− return (i, ty)

693+ return (i, ifc, ty)

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

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

695 fc <- getFC

696− return (i, PType fc)

696+ return (i, ifc, PType fc)

697

698{- | Parses a type class instance declaration

699

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

714 en <- optional instanceName

715 cs <- constraintList syn

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

717− cn <- fst <$> fnName

717+ (cn, cnfc) <- fnName

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

720 let t = bindList (PPi constraint) cs sc

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

723 <?> "instance declaration"

724 where instanceName :: IdrisParser Name

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

src/Idris/REPL.hs+3−3

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

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

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

793 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

795 getName _ = Nothing

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

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

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

839 fixClauses :: PDecl' t -> PDecl' t

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

841 PClauses fc opts (getClauseName clause) css

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

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

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

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

844 fixClauses decl = decl

845

846process fn (Undefine names) = undefine names