cc83850 · Idris-dev · git.iko.soy

git.iko.soy/Idris-dev

on master help sign in

Accurate highlighting for records

cc83850David Raymond Christiansen11 years ago

src/Idris/AbsSyntax.hs+2−2

compare with master

unifiedsplit

@@ -1093,8 +1093,8 @@ expandParamsD rhs ist dec ps ns (PData doc argDocs syn fc co pd)

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

1094 econ (doc, argDocs, n, nfc, t, fc, fs)

1095 = (doc, argDocs, dec n, nfc, piBindp expl ps (expandParams dec ps ns [] t), fc, fs)

1096−expandParamsD rhs ist dec ps ns d@(PRecord doc rsyn fc opts name prs pdocs fls cn cdoc csyn)

1096+expandParamsD rhs ist dec ps ns d@(PRecord doc rsyn fc opts name nfc prs pdocs fls cn cdoc csyn)

1097− = d

1097+ = d

1098expandParamsD rhs ist dec ps ns (PParams f params pds)

1099 = PParams f (ps ++ map (mapsnd (expandParams dec ps ns [])) params)

1100 (map (expandParamsD True ist dec ps ns) pds)

src/Idris/AbsSyntaxTree.hs+6−5

@@ -603,10 +603,11 @@ data PDecl' t

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

604 | PRecord (Docstring (Either Err PTerm)) SyntaxInfo FC DataOpts

605 Name -- Record name

606+ FC -- Record name precise location

606 [(Name, FC, Plicity, t)] -- Parameters, where FC is precise name span

607 [(Name, FC, Plicity, t)] -- Parameters, where FC is precise name span

607 [(Name, Docstring (Either Err PTerm))] -- Param Docs

608 [(Name, Docstring (Either Err PTerm))] -- Param Docs

608− [((Maybe Name), Plicity, t, Maybe (Docstring (Either Err PTerm)))] -- Fields

609+ [((Maybe (Name, FC)), Plicity, t, Maybe (Docstring (Either Err PTerm)))] -- Fields

609− (Maybe Name) -- Optional constructor name

610+ (Maybe (Name, FC)) -- Optional constructor name and location

610 (Docstring (Either Err PTerm)) -- Constructor doc

611 (Docstring (Either Err PTerm)) -- Constructor doc

611 SyntaxInfo -- Constructor SyntaxInfo

612 SyntaxInfo -- Constructor SyntaxInfo

612 -- ^ Record declaration

613 -- ^ Record declaration

@@ -740,7 +741,7 @@ declared (PData _ _ _ _ _ (PDatadecl n _ _ ts)) = n : map fstt ts

740declared (PData _ _ _ _ _ (PLaterdecl n _ _)) = [n]

741declared (PData _ _ _ _ _ (PLaterdecl n _ _)) = [n]

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

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

742declared (PNamespace _ ds) = concatMap declared ds

743declared (PNamespace _ ds) = concatMap declared ds

743−declared (PRecord _ _ _ _ n _ _ _ cn _ _) = n : maybeToList cn

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

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

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

745declared (PInstance _ _ _ _ _ _ _ _ _ _) = []

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

746declared (PDSL n _) = [n]

747declared (PDSL n _) = [n]

@@ -755,7 +756,7 @@ tldeclared (PFix _ _ _) = []

755tldeclared (PTy _ _ _ _ _ n _ t) = [n]

756tldeclared (PTy _ _ _ _ _ n _ t) = [n]

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

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

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

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

758−tldeclared (PRecord _ _ _ _ n _ _ _ cn _ _) = n : maybeToList cn

759+tldeclared (PRecord _ _ _ _ n _ _ _ _ cn _ _) = n : map fst (maybeToList cn)

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

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

760 where fstt (_, _, a, _, _, _, _) = a

761 where fstt (_, _, a, _, _, _, _) = a

761tldeclared (PParams _ _ ds) = []

762tldeclared (PParams _ _ ds) = []

@@ -776,7 +777,7 @@ defined (PData _ _ _ _ _ (PDatadecl n _ _ ts)) = n : map fstt ts

776defined (PData _ _ _ _ _ (PLaterdecl n _ _)) = []

777defined (PData _ _ _ _ _ (PLaterdecl n _ _)) = []

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

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

778defined (PNamespace _ ds) = concatMap defined ds

779defined (PNamespace _ ds) = concatMap defined ds

779−defined (PRecord _ _ _ _ n _ _ _ cn _ _) = n : maybeToList cn

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

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

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

781defined (PInstance _ _ _ _ _ _ _ _ _ _) = []

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

782defined (PDSL n _) = [n]

783defined (PDSL n _) = [n]

src/Idris/DeepSeq.hs+8−2

@@ -147,11 +147,17 @@ instance (NFData t) => NFData (PDecl' t) where

147 rnf x3 `seq` rnf x4 `seq` rnf x5 `seq` rnf x6 `seq` ()

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

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

150− rnf (PRecord x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11)

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

151 = rnf x1 `seq`

152 rnf x2 `seq`

153 rnf x3 `seq`

154− rnf x4 `seq` rnf x5 `seq` rnf x6 `seq` rnf x7 `seq` rnf x8 `seq` rnf x9 `seq` rnf x10 `seq` rnf x11 `seq` ()

154+ rnf x4 `seq`

155+ rnf x5 `seq`

156+ rnf x6 `seq`

157+ rnf x7 `seq`

158+ rnf x8 `seq`

159+ rnf x9 `seq`

160+ rnf x10 `seq` rnf x11 `seq` rnf x12 `seq` ()

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

156 = rnf x1 `seq`

162 = rnf x1 `seq`

157 rnf x2 `seq`

163 rnf x2 `seq`

src/Idris/Elab/Class.hs+1−1

@@ -252,7 +252,7 @@ memberDocs :: PDecl -> Maybe (Name, Docstring (Either Err PTerm))

252memberDocs (PTy d _ _ _ _ n _ _) = Just (basename n, d)

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

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

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

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

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

257memberDocs _ = Nothing

258

src/Idris/Elab/Record.hs+41−33

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

14import Idris.Inliner

15import Idris.PartialEval

16import Idris.DeepSeq

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

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

18import IRTS.Lang

20import Idris.ParseExpr (tryFullExpr)

@@ -37,21 +37,22 @@ elabRecord :: ElabInfo

37 -> (Docstring (Either Err PTerm)) -- ^ The documentation for the whole declaration

38 -> SyntaxInfo -> FC -> DataOpts

39 -> Name -- ^ The name of the type being defined

40+ -> FC -- ^ The precise source location of the tycon name

40 -> [(Name, FC, Plicity, PTerm)] -- ^ Parameters

41 -> [(Name, FC, Plicity, PTerm)] -- ^ Parameters

41 -> [(Name, Docstring (Either Err PTerm))] -- ^ Parameter Docs

42 -> [(Name, Docstring (Either Err PTerm))] -- ^ Parameter Docs

42− -> [((Maybe Name), Plicity, PTerm, Maybe (Docstring (Either Err PTerm)))] -- ^ Fields

43+ -> [(Maybe (Name, FC), Plicity, PTerm, Maybe (Docstring (Either Err PTerm)))] -- ^ Fields

43− -> Maybe Name -- ^ Constructor Name

44+ -> Maybe (Name, FC) -- ^ Constructor Name

44 -> (Docstring (Either Err PTerm)) -- ^ Constructor Doc

45 -> (Docstring (Either Err PTerm)) -- ^ Constructor Doc

45 -> SyntaxInfo -- ^ Constructor SyntaxInfo

46 -> SyntaxInfo -- ^ Constructor SyntaxInfo

46 -> Idris ()

47 -> Idris ()

47−elabRecord info doc rsyn fc opts tyn params paramDocs fields cname cdoc csyn

48+elabRecord info doc rsyn fc opts tyn nfc params paramDocs fields cname cdoc csyn

48 = do logLvl 1 $ "Building data declaration for " ++ show tyn

49 = do logLvl 1 $ "Building data declaration for " ++ show tyn

49 -- Type constructor

50 -- Type constructor

50 let tycon = generateTyConType params

51 let tycon = generateTyConType params

51 logLvl 1 $ "Type constructor " ++ showTmImpls tycon

52 logLvl 1 $ "Type constructor " ++ showTmImpls tycon

53 -- Data constructor

54 -- Data constructor

54− dconName <- generateDConName cname

55+ dconName <- generateDConName (fmap fst cname)

55 let dconTy = generateDConType params fieldsWithNameAndDoc

56 let dconTy = generateDConType params fieldsWithNameAndDoc

56 logLvl 1 $ "Data constructor: " ++ showTmImpls dconTy

57 logLvl 1 $ "Data constructor: " ++ showTmImpls dconTy

@@ -62,7 +63,13 @@ elabRecord info doc rsyn fc opts tyn params paramDocs fields cname cdoc csyn

63 iLOG $ "fieldsWithName " ++ show fieldsWithName

64 iLOG $ "fieldsWithName " ++ show fieldsWithName

64 iLOG $ "fieldsWIthNameAndDoc " ++ show fieldsWithNameAndDoc

65 iLOG $ "fieldsWIthNameAndDoc " ++ show fieldsWithNameAndDoc

65− elabRecordFunctions info rsyn fc tyn [(n, p, t, d) | (n, _, p, t, d) <- paramsAndDoc] fieldsWithNameAndDoc dconName target

66+ elabRecordFunctions info rsyn fc tyn paramsAndDoc fieldsWithNameAndDoc dconName target

67+

68+ sendHighlighting $

69+ [(nfc, AnnName tyn Nothing Nothing Nothing)] ++

70+ maybe [] (\(_, cnfc) -> [(cnfc, AnnName dconName Nothing Nothing Nothing)]) cname ++

71+ [(ffc, AnnBoundName fn False) | (fn, ffc, _, _, _) <- fieldsWithName]

72+

66 where

73 where

67 -- | Generates a type constructor.

74 -- | Generates a type constructor.

68 generateTyConType :: [(Name, FC, Plicity, PTerm)] -> PTerm

75 generateTyConType :: [(Name, FC, Plicity, PTerm)] -> PTerm

@@ -81,9 +88,9 @@ elabRecord info doc rsyn fc opts tyn params paramDocs fields cname cdoc csyn

81 Nothing -> return n

88 Nothing -> return n

83 -- | Generates the data constructor type.

90 -- | Generates the data constructor type.

84− generateDConType :: [(Name, FC, Plicity, PTerm)] -> [(Name, Plicity, PTerm, a)] -> PTerm

91+ generateDConType :: [(Name, FC, Plicity, PTerm)] -> [(Name, FC, Plicity, PTerm, a)] -> PTerm

85 generateDConType ((n, nfc, _, t) : ps) as = PPi impl (nsroot n) NoFC t (generateDConType ps as)

92 generateDConType ((n, nfc, _, t) : ps) as = PPi impl (nsroot n) NoFC t (generateDConType ps as)

86− generateDConType [] ((n, p, t, _) : as) = PPi p (nsroot n) NoFC t (generateDConType [] as)

93+ generateDConType [] ((n, _, p, t, _) : as) = PPi p (nsroot n) NoFC t (generateDConType [] as)

87 generateDConType [] [] = target

94 generateDConType [] [] = target

89 -- | The target for the constructor and projection functions. Also the source of the update functions.

96 -- | The target for the constructor and projection functions. Also the source of the update functions.

@@ -104,42 +111,43 @@ elabRecord info doc rsyn fc opts tyn params paramDocs fields cname cdoc csyn

104 dconsArgDocs :: [(Name, Docstring (Either Err PTerm))]

111 dconsArgDocs :: [(Name, Docstring (Either Err PTerm))]

105 dconsArgDocs = paramDocs ++ (dcad fieldsWithName)

112 dconsArgDocs = paramDocs ++ (dcad fieldsWithName)

106 where

113 where

107− dcad :: [(Name, Plicity, PTerm, Maybe (Docstring (Either Err PTerm)))] -> [(Name, Docstring (Either Err PTerm))]

114+ dcad :: [(Name, FC, Plicity, PTerm, Maybe (Docstring (Either Err PTerm)))] -> [(Name, Docstring (Either Err PTerm))]

108− dcad ((n, _, _, (Just d)) : rest) = ((nsroot n), d) : (dcad rest)

115+ dcad ((n, _, _, _, (Just d)) : rest) = ((nsroot n), d) : (dcad rest)

109 dcad (_ : rest) = dcad rest

116 dcad (_ : rest) = dcad rest

110 dcad [] = []

117 dcad [] = []

111

118

112− fieldsWithName :: [(Name, Plicity, PTerm, Maybe (Docstring (Either Err PTerm)))]

119+ fieldsWithName :: [(Name, FC, Plicity, PTerm, Maybe (Docstring (Either Err PTerm)))]

113 fieldsWithName = fwn [] fields

120 fieldsWithName = fwn [] fields

114 where

121 where

115− fwn :: [Name] -> [(Maybe Name, Plicity, PTerm, Maybe (Docstring (Either Err PTerm)))] -> [(Name, Plicity, PTerm, Maybe (Docstring (Either Err PTerm)))]

122+ fwn :: [Name] -> [(Maybe (Name, FC), Plicity, PTerm, Maybe (Docstring (Either Err PTerm)))] -> [(Name, FC, Plicity, PTerm, Maybe (Docstring (Either Err PTerm)))]

116 fwn ns ((n, p, t, d) : rest)

123 fwn ns ((n, p, t, d) : rest)

117 = let nn = case n of

124 = let nn = case n of

118 Just n' -> n'

125 Just n' -> n'

119 Nothing -> newName ns baseName

126 Nothing -> newName ns baseName

127+ withNS = expandNS rsyn (fst nn)

120− in (expandNS rsyn $ nn, p, t, d) : (fwn (nn : ns) rest)

128+ in (withNS, snd nn, p, t, d) : (fwn (fst nn : ns) rest)

121 fwn _ _ = []

129 fwn _ _ = []

122

130

123− baseName = sUN "__pi_arg"

131+ baseName = (sUN "__pi_arg", NoFC)

124

132

125− newName :: [Name] -> Name -> Name

133+ newName :: [Name] -> (Name, FC) -> (Name, FC)

126− newName ns n

134+ newName ns (n, nfc)

127− | n `elem` ns = newName ns (nextName n)

135+ | n `elem` ns = newName ns (nextName n, nfc)

128− | otherwise = n

136+ | otherwise = (n, nfc)

129−

137+

130− fieldsWithNameAndDoc :: [(Name, Plicity, PTerm, Docstring (Either Err PTerm))]

138+ fieldsWithNameAndDoc :: [(Name, FC, Plicity, PTerm, Docstring (Either Err PTerm))]

131 fieldsWithNameAndDoc = fwnad fieldsWithName

139 fieldsWithNameAndDoc = fwnad fieldsWithName

132 where

140 where

133− fwnad :: [(Name, Plicity, PTerm, Maybe (Docstring (Either Err PTerm)))] -> [(Name, Plicity, PTerm, Docstring (Either Err PTerm))]

141+ fwnad :: [(Name, FC, Plicity, PTerm, Maybe (Docstring (Either Err PTerm)))] -> [(Name, FC, Plicity, PTerm, Docstring (Either Err PTerm))]

134− fwnad ((n, p, t, d) : rest)

142+ fwnad ((n, nfc, p, t, d) : rest)

135 = let doc = fromMaybe emptyDocstring d

143 = let doc = fromMaybe emptyDocstring d

136− in (n, p, t, doc) : (fwnad rest)

144+ in (n, nfc, p, t, doc) : (fwnad rest)

137 fwnad [] = []

145 fwnad [] = []

138

146

139elabRecordFunctions :: ElabInfo -> SyntaxInfo -> FC

147elabRecordFunctions :: ElabInfo -> SyntaxInfo -> FC

140 -> Name -- ^ Record type name

148 -> Name -- ^ Record type name

141− -> [(Name, Plicity, PTerm, Docstring (Either Err PTerm))] -- ^ Parameters

149+ -> [(Name, FC, Plicity, PTerm, Docstring (Either Err PTerm))] -- ^ Parameters

142− -> [(Name, Plicity, PTerm, Docstring (Either Err PTerm))] -- ^ Fields

150+ -> [(Name, FC, Plicity, PTerm, Docstring (Either Err PTerm))] -- ^ Fields

143 -> Name -- ^ Constructor Name

151 -> Name -- ^ Constructor Name

144 -> PTerm -- ^ Target type

152 -> PTerm -- ^ Target type

145 -> Idris ()

153 -> Idris ()

@@ -164,11 +172,11 @@ elabRecordFunctions info rsyn fc tyn params fields dconName target

164

172

165 -- The parameters for elaboration with their documentation

173 -- The parameters for elaboration with their documentation

166 -- Parameter functions are all prefixed with "param_".

174 -- Parameter functions are all prefixed with "param_".

167− let paramsForElab = [((nsroot n), (paramName n), impl, t, d) | (n, _, t, d) <- params] -- zipParams i params paramDocs]

175+ let paramsForElab = [((nsroot n), (paramName n), impl, t, d) | (n, _, _, t, d) <- params] -- zipParams i params paramDocs]

168−

176+

169 -- The fields (written by the user) with their documentation.

177 -- The fields (written by the user) with their documentation.

170− let userFieldsForElab = [((nsroot n), n, p, t, d) | (n, p, t, d) <- fields]

178+ let userFieldsForElab = [((nsroot n), n, p, t, d) | (n, nfc, p, t, d) <- fields]

171−

179+

172 -- All things we need to elaborate projection functions for, together with a number denoting their position in the constructor.

180 -- All things we need to elaborate projection functions for, together with a number denoting their position in the constructor.

173 let projectors = [(n, n', p, t, d, i) | ((n, n', p, t, d), i) <- zip (freeFieldsForElab ++ paramsForElab ++ userFieldsForElab) [0..]]

181 let projectors = [(n, n', p, t, d, i) | ((n, n', p, t, d), i) <- zip (freeFieldsForElab ++ paramsForElab ++ userFieldsForElab) [0..]]

174 -- Build and elaborate projection functions

182 -- Build and elaborate projection functions

@@ -189,10 +197,10 @@ elabRecordFunctions info rsyn fc tyn params fields dconName target

189

197

190 -- | Root names of all fields in the current record declarations

198 -- | Root names of all fields in the current record declarations

191 fieldNames :: [Name]

199 fieldNames :: [Name]

192− fieldNames = [nsroot n | (n, _, _, _) <- fields]

200+ fieldNames = [nsroot n | (n, _, _, _, _) <- fields]

193

201

194 paramNames :: [Name]

202 paramNames :: [Name]

195− paramNames = [nsroot n | (n, _, _, _) <- params]

203+ paramNames = [nsroot n | (n, _, _, _, _) <- params]

196

204

197 isFieldOrParam :: Name -> Bool

205 isFieldOrParam :: Name -> Bool

198 isFieldOrParam n = n `elem` (fieldNames ++ paramNames)

206 isFieldOrParam n = n `elem` (fieldNames ++ paramNames)

@@ -207,7 +215,7 @@ elabRecordFunctions info rsyn fc tyn params fields dconName target

207 isField' (n, _, _, _, _, _) = isField n

215 isField' (n, _, _, _, _, _) = isField n

208

216

209 fieldTerms :: [PTerm]

217 fieldTerms :: [PTerm]

210− fieldTerms = [t | (_, _, t, _) <- fields]

218+ fieldTerms = [t | (_, _, _, t, _) <- fields]

211

219

212 -- Delabs the TT to PTerm

220 -- Delabs the TT to PTerm

213 -- This is not good.

221 -- This is not good.

@@ -263,7 +271,7 @@ elabRecordFunctions info rsyn fc tyn params fields dconName target

263

271

264 -- | A map from a field name to the other fields it depends on.

272 -- | A map from a field name to the other fields it depends on.

265 fieldDependencies :: [(Name, [Name])]

273 fieldDependencies :: [(Name, [Name])]

266− fieldDependencies = map (uncurry fieldDep) [(n, t) | (n, _, t, _) <- fields ++ params]

274+ fieldDependencies = map (uncurry fieldDep) [(n, t) | (n, _, _, t, _) <- fields ++ params]

267 where

275 where

268 fieldDep :: Name -> PTerm -> (Name, [Name])

276 fieldDep :: Name -> PTerm -> (Name, [Name])

269 fieldDep n t = ((nsroot n), paramNames ++ fieldNames `intersect` allNamesIn t)

277 fieldDep n t = ((nsroot n), paramNames ++ fieldNames `intersect` allNamesIn t)

src/Idris/ElabDecls.hs+2−2

@@ -239,10 +239,10 @@ elabDecl' what info (PClass doc s f cs n ps pdocs fds ds cn cd)

239elabDecl' what info (PInstance doc argDocs s f cs n 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

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

242+elabDecl' 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

245− elabRecord info doc rsyn fc opts name ps pdocs fs cname cdoc csyn

245+ elabRecord info doc rsyn fc opts name nfc ps pdocs fs cname cdoc csyn

246{-

247 | otherwise

248 = do iLOG $ "Elaborating [type of] " ++ show tyn

src/Idris/IBC.hs+4−2

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

1174 PNamespace x1 x2 -> do putWord8 5

1175 put x1

1176 put x2

1177− PRecord x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 ->

1177+ PRecord x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 ->

1178 do putWord8 6

1179 put x1

1180 put x2

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

1187 put x9

1188 put x10

1189 put x11

1190+ put x12

1190 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

1191 -> do putWord8 7

1192 -> do putWord8 7

1192 put x1

1193 put x1

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

1293 x9 <- get

1294 x9 <- get

1294 x10 <- get

1295 x10 <- get

1295 x11 <- get

1296 x11 <- get

1297+ x12 <- get

1296− return (PRecord x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11)

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

1297 7 -> do x1 <- get

1299 7 -> do x1 <- get

1298 x2 <- get

1300 x2 <- get

1299 x3 <- get

1301 x3 <- get

src/Idris/ParseData.hs+11−11

@@ -53,16 +53,16 @@ record syn = do (doc, paramDocs, acc, opts) <- try (do

53 co <- recordI

54 return (doc', paramDocs', acc, opts ++ co))

55 fc <- getFC

56− tyn_in <- fst <$> fnName

56+ (tyn_in, nfc) <- fnName

57 let tyn = expandNS syn tyn_in

58 let rsyn = syn { syn_namespace = show (nsroot tyn) :

59 syn_namespace syn }

60 params <- manyTill (recordParameter rsyn) (reserved "where")

61− (fields, cname, cdoc) <- indentedBlockS $ agdaStyleBody rsyn tyn

61+ (fields, cname, cdoc) <- indentedBlockS $ recordBody rsyn tyn

62 case cname of

63− Just cn' -> accData acc tyn [cn']

63+ Just cn' -> accData acc tyn [fst cn']

64 Nothing -> return ()

65− return $ PRecord doc rsyn fc opts tyn params paramDocs fields cname cdoc syn

65+ return $ PRecord doc rsyn fc opts tyn nfc params paramDocs fields cname cdoc syn

66 <?> "record type declaration"

67 where

68 getRecNames :: SyntaxInfo -> PTerm -> [Name]

@@ -74,8 +74,8 @@ record syn = do (doc, paramDocs, acc, opts) <- try (do

74 toFreeze (Just Frozen) = Just Hidden

75 toFreeze x = x

77− agdaStyleBody :: SyntaxInfo -> Name -> IdrisParser ([((Maybe Name), Plicity, PTerm, Maybe (Docstring (Either Err PTerm)))], Maybe Name, Docstring (Either Err PTerm))

77+ recordBody :: SyntaxInfo -> Name -> IdrisParser ([((Maybe (Name, FC)), Plicity, PTerm, Maybe (Docstring (Either Err PTerm)))], Maybe (Name, FC), Docstring (Either Err PTerm))

78− agdaStyleBody syn tyn = do

78+ recordBody syn tyn = do

79 ist <- get

80 fc <- getFC

@@ -90,11 +90,11 @@ record syn = do (doc, paramDocs, acc, opts) <- try (do

91 return (fields, constructorName, constructorDoc')

92 where

93− field :: SyntaxInfo -> IdrisParser ((Maybe Name), Plicity, PTerm, Maybe (Docstring (Either Err PTerm)))

93+ field :: SyntaxInfo -> IdrisParser ((Maybe (Name, FC)), Plicity, PTerm, Maybe (Docstring (Either Err PTerm)))

94 field syn = do doc <- optional docComment

95 c <- optional $ lchar '{'

96− n <- (do n <- fst <$> fnName

96+ n <- (do (n, nfc) <- fnName

97− return $ Just (expandNS syn n))

97+ return $ Just (expandNS syn n, nfc))

98 <|> (do symbol "_"

99 return Nothing)

100 lchar ':'

@@ -106,8 +106,8 @@ record syn = do (doc, paramDocs, acc, opts) <- try (do

106 Nothing -> Nothing

107 return (n, p, t, doc')

108

109− constructor :: IdrisParser Name

109+ constructor :: IdrisParser (Name, FC)

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

110+ constructor = (reserved "constructor") *> fnName

111

112

113 endPlicity :: Maybe Char -> IdrisParser Plicity