cc83850 · Idris-dev · git.iko.soy

git.iko.soy/Idris-dev

Accurate highlighting for records

commitcc83850d44052d6200c292f61c062950296a61ee authorDavid Raymond Christiansen <david@davidchristiansen.dk> dateMon 11 May 2015, 12:26 (11 years ago) parentc303a38

8 files changed+75−58

compare with master

unifiedsplit

src/Idris/AbsSyntax.hs+2−2 src/Idris/AbsSyntaxTree.hs+6−5 src/Idris/DeepSeq.hs+8−2 src/Idris/Elab/Class.hs+1−1 src/Idris/Elab/Record.hs+41−33 src/Idris/ElabDecls.hs+2−2 src/Idris/IBC.hs+4−2 src/Idris/ParseData.hs+11−11

src/Idris/AbsSyntax.hs+2−2

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

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

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

10951095 = (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)

1097− = d

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

1097+ = d

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

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

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

src/Idris/AbsSyntaxTree.hs+6−5

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

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

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

605605 Name -- Record name

606+ FC -- Record name precise location

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

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

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

609− (Maybe Name) -- Optional constructor name

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

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

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

611612 SyntaxInfo -- Constructor SyntaxInfo

612613 -- ^ Record declaration

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

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

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

742743declared (PNamespace _ ds) = concatMap declared ds

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

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

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

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

746747declared (PDSL n _) = [n]

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

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

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

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

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

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

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

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

761762tldeclared (PParams _ _ ds) = []

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

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

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

778779defined (PNamespace _ ds) = concatMap defined ds

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

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

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

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

782783defined (PDSL n _) = [n]

src/Idris/DeepSeq.hs+8−2

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

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

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

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

151151 = rnf x1 `seq`

152152 rnf x2 `seq`

153153 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` ()

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

156162 = rnf x1 `seq`

157163 rnf x2 `seq`

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

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

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

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

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

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

257257memberDocs _ = Nothing

258258

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

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

1414import Idris.Inliner

1515import Idris.PartialEval

1616import Idris.DeepSeq

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

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

1818import IRTS.Lang

1919

2020import Idris.ParseExpr (tryFullExpr)

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

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

3838 -> SyntaxInfo -> FC -> DataOpts

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

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

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

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

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

43− -> Maybe Name -- ^ Constructor Name

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

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

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

4546 -> SyntaxInfo -- ^ Constructor SyntaxInfo

4647 -> 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

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

4950 -- Type constructor

5051 let tycon = generateTyConType params

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

5253

5354 -- Data constructor

54− dconName <- generateDConName cname

55+ dconName <- generateDConName (fmap fst cname)

5556 let dconTy = generateDConType params fieldsWithNameAndDoc

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

5758

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

6263

6364 iLOG $ "fieldsWithName " ++ show fieldsWithName

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

6673 where

6774 -- | Generates a type constructor.

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

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

8188 Nothing -> return n

8289

8390 -- | 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

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

8794 generateDConType [] [] = target

8895

8996 -- | 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

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

105112 dconsArgDocs = paramDocs ++ (dcad fieldsWithName)

106113 where

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

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

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

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

109116 dcad (_ : rest) = dcad rest

110117 dcad [] = []

111118

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

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

113120 fieldsWithName = fwn [] fields

114121 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)))]

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

117124 = let nn = case n of

118125 Just n' -> n'

119126 Nothing -> newName ns baseName

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

127+ withNS = expandNS rsyn (fst nn)

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

121129 fwn _ _ = []

122130

123− baseName = sUN "__pi_arg"

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

124132

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

126− newName ns n

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

128− | otherwise = n

129−

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

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

134+ newName ns (n, nfc)

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

136+ | otherwise = (n, nfc)

137+

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

131139 fieldsWithNameAndDoc = fwnad fieldsWithName

132140 where

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

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

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

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

135143 = let doc = fromMaybe emptyDocstring d

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

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

137145 fwnad [] = []

138146

139147elabRecordFunctions :: ElabInfo -> SyntaxInfo -> FC

140148 -> Name -- ^ Record type name

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

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

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

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

143151 -> Name -- ^ Constructor Name

144152 -> PTerm -- ^ Target type

145153 -> Idris ()

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

164172

165173 -- The parameters for elaboration with their documentation

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

168−

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

176+

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

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

171−

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

179+

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

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

174182 -- Build and elaborate projection functions

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

189197

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

191199 fieldNames :: [Name]

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

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

193201

194202 paramNames :: [Name]

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

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

196204

197205 isFieldOrParam :: Name -> Bool

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

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

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

208216

209217 fieldTerms :: [PTerm]

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

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

211219

212220 -- Delabs the TT to PTerm

213221 -- This is not good.

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

263271

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

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

267275 where

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

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

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

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

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

243243 | what /= ETypes

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

246246{-

247247 | otherwise

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

src/Idris/IBC.hs+4−2

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

11741174 PNamespace x1 x2 -> do putWord8 5

11751175 put x1

11761176 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 ->

11781178 do putWord8 6

11791179 put x1

11801180 put x2

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

11871187 put x9

11881188 put x10

11891189 put x11

1190+ put x12

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

11911192 -> do putWord8 7

11921193 put x1

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

12931294 x9 <- get

12941295 x10 <- get

12951296 x11 <- get

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

1297+ x12 <- get

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

12971299 7 -> do x1 <- get

12981300 x2 <- get

12991301 x3 <- get

src/Idris/ParseData.hs+11−11

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

5353 co <- recordI

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

5555 fc <- getFC

56− tyn_in <- fst <$> fnName

56+ (tyn_in, nfc) <- fnName

5757 let tyn = expandNS syn tyn_in

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

5959 syn_namespace syn }

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

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

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

6262 case cname of

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

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

6464 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

6666 <?> "record type declaration"

6767 where

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

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

7474 toFreeze (Just Frozen) = Just Hidden

7575 toFreeze x = x

7676

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

78− agdaStyleBody syn tyn = do

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

78+ recordBody syn tyn = do

7979 ist <- get

8080 fc <- getFC

8181

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

9090

9191 return (fields, constructorName, constructorDoc')

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

9494 field syn = do doc <- optional docComment

9595 c <- optional $ lchar '{'

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

97− return $ Just (expandNS syn n))

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

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

9898 <|> (do symbol "_"

9999 return Nothing)

100100 lchar ':'

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

106106 Nothing -> Nothing

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

108108

109− constructor :: IdrisParser Name

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

109+ constructor :: IdrisParser (Name, FC)

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

111111

112112

113113 endPlicity :: Maybe Char -> IdrisParser Plicity