a6f56ce · Idris-dev · git.iko.soy

git.iko.soy/Idris-dev

Fix #3275

Check fixity of type and data constructors that are operators.

commita6f56ce4fab6d674d8177bfb6cdba45158df8021 authorBjörn Aili <bjorn.aili@gmail.com> dateFri 29 Jul 2016, 20:01 (10 years ago) parentce81257

3 files changed+31−16

compare with master

unifiedsplit

src/Idris/Parser.hs+7−15 src/Idris/Parser/Data.hs+12−1 src/Idris/Parser/Ops.hs+12

src/Idris/Parser.hs+7−15

@@ -598,7 +598,7 @@ fnDecl syn = try (do notEndBlock

598598@

599599-}

600600fnDecl' :: SyntaxInfo -> IdrisParser PDecl

601−fnDecl' syn = checkFixity $

601+fnDecl' syn = checkFixity' $

602602 do (doc, argDocs, fc, opts', n, nfc, acc) <- try (do

603603 pushIndent

604604 (doc, argDocs) <- docstring syn

@@ -618,22 +618,14 @@ fnDecl' syn = checkFixity $

618618 <|> caf syn

619619 <|> pattern syn

620620 <?> "function declaration"

621− where checkFixity :: IdrisParser PDecl -> IdrisParser PDecl

622− checkFixity p = do decl <- p

623− case getName decl of

624− Nothing -> return decl

625− Just n -> do fOk <- fixityOK n

626− unless fOk . fail $

627− "Missing fixity declaration for " ++ show n

628− return decl

621+ where checkFixity' :: IdrisParser PDecl -> IdrisParser PDecl

622+ checkFixity' p = do decl <- p

623+ case getName decl of

624+ Nothing -> return decl

625+ Just n -> do checkFixity n

626+ return decl

629627 getName (PTy _ _ _ _ _ n _ _) = Just n

630628 getName _ = Nothing

631− fixityOK (NS n _) = fixityOK n

632− fixityOK (UN n) | all (flip elem opChars) (str n) =

633− do fixities <- fmap idris_infixes get

634− return . elem (str n) . map (\ (Fix _ op) -> op) $ fixities

635− | otherwise = return True

636− fixityOK _ = return True

637629

638630{-| Parses a series of function and accessbility options

639631

src/Idris/Parser/Data.hs+12−1

@@ -198,7 +198,8 @@ SimpleConstructorList ::=

198198 ;

199199-}

200200data_ :: SyntaxInfo -> IdrisParser PDecl

201−data_ syn = do (doc, argDocs, acc, dataOpts) <- try (do

201+data_ syn = checkFixity' $

202+ do (doc, argDocs, acc, dataOpts) <- try (do

202203 (doc, argDocs) <- option noDocs docComment

203204 pushIndent

204205 acc <- accessibility

@@ -250,6 +251,14 @@ data_ syn = do (doc, argDocs, acc, dataOpts) <- try (do

250251 return d)

251252 <?> "data type declaration"

252253 where

254+ checkFixity' :: IdrisParser PDecl -> IdrisParser PDecl

255+ checkFixity' p = do decl <- p

256+ case getName decl of

257+ Nothing -> return decl

258+ Just n -> do checkFixity n

259+ return decl

260+ getName (PData _ _ _ _ _ (PDatadecl tyn _ _ _)) = Just tyn

261+ getName _ = Nothing

253262 mkPApp :: FC -> PTerm -> [PTerm] -> PTerm

254263 mkPApp fc t [] = t

255264 mkPApp fc t xs = PApp fc t (map pexp xs)

@@ -277,6 +286,7 @@ constructor syn

277286 let doc' = annotCode (tryFullExpr syn ist) doc

278287 argDocs' = [ (n, annotCode (tryFullExpr syn ist) d)

279288 | (n, d) <- argDocs ]

289+ checkFixity cn

280290 return (doc', argDocs', cn, nfc, ty, fc, fs)

281291 <?> "constructor"

282292

@@ -293,6 +303,7 @@ simpleConstructor syn

293303 fc <- getFC

294304 args <- many (do notEndApp

295305 simpleExpr syn)

306+ checkFixity cn

296307 return (doc', [], cn, nfc, args, fc, [])

297308 <?> "constructor"

298309

src/Idris/Parser/Ops.hs+12

@@ -161,6 +161,18 @@ fixity = do pushIndent

161161 extractName :: FixDecl -> String

162162 extractName (Fix _ n) = n

163163

164+{- | Checks that an operator name also has a fixity declaration -}

165+checkFixity :: Name -> IdrisParser ()

166+checkFixity n = do fOk <- fixityOk n

167+ unless fOk . fail $

168+ "Missing fixity declaration for " ++ show n

169+ where fixityOk (NS n _) = fixityOk n

170+ fixityOk (UN n) | all (flip elem opChars) (str n) =

171+ do fixities <- fmap idris_infixes get

172+ return . elem (str n) . map (\ (Fix _ op) -> op) $ fixities

173+ | otherwise = return True

174+ fixityOk _ = return True

175+

164176{- | Parses a fixity declaration type (i.e. infix or prefix, associtavity)

165177@

166178 FixityType ::=