6eadbe8 · Idris-dev · git.iko.soy

CONTRIBUTORS+1

compare with master

unifiedsplit

@@ -51,3 +51,4 @@ Leif Warner

51Daniel Waterworth

52Eric Weinstein

53Jonas Westerlund

54+Björn Aili

src/Idris/Parser.hs+1−17

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

598@

599-}

600fnDecl' :: SyntaxInfo -> IdrisParser PDecl

601−fnDecl' syn = checkFixity $

601+fnDecl' syn = checkDeclFixity $

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

603 pushIndent

604 (doc, argDocs) <- docstring syn

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

618 <|> caf syn

619 <|> pattern syn

620 <?> "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

629− getName (PTy _ _ _ _ _ n _ _) = Just n

630− 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

637

621

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

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

639

623

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

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

198 ;

199-}

200data_ :: SyntaxInfo -> IdrisParser PDecl

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

201+data_ syn = checkDeclFixity $

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

202 (doc, argDocs) <- option noDocs docComment

203 (doc, argDocs) <- option noDocs docComment

203 pushIndent

204 pushIndent

204 acc <- accessibility

205 acc <- accessibility

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

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

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

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

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

279 | (n, d) <- argDocs ]

280 | (n, d) <- argDocs ]

281+ checkNameFixity cn

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

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

281 <?> "constructor"

283 <?> "constructor"

282

284

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

293 fc <- getFC

295 fc <- getFC

294 args <- many (do notEndApp

296 args <- many (do notEndApp

295 simpleExpr syn)

297 simpleExpr syn)

298+ checkNameFixity cn

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

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

297 <?> "constructor"

300 <?> "constructor"

298

301

src/Idris/Parser/Ops.hs+23

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

161 extractName :: FixDecl -> String

162 extractName (Fix _ n) = n

163

164+-- | Check that a declaration of an operator also has fixity declared

165+checkDeclFixity :: IdrisParser PDecl -> IdrisParser PDecl

166+checkDeclFixity p = do decl <- p

167+ case getDeclName decl of

168+ Nothing -> return decl

169+ Just n -> do checkNameFixity n

170+ return decl

171+ where getDeclName (PTy _ _ _ _ _ n _ _ ) = Just n

172+ getDeclName (PData _ _ _ _ _ (PDatadecl n _ _ _)) = Just n

173+ getDeclName _ = Nothing

174+

175+-- | Checks that an operator name also has a fixity declaration

176+checkNameFixity :: Name -> IdrisParser ()

177+checkNameFixity n = do fOk <- fixityOk n

178+ unless fOk . fail $

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

180+ where fixityOk (NS n' _) = fixityOk n'

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

182+ do fixities <- fmap idris_infixes get

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

184+ | otherwise = return True

185+ fixityOk _ = return True

186+

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

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

165@

188@

166 FixityType ::=

189 FixityType ::=

test/regression002/expected+14

@@ -117,6 +117,20 @@ Type level variable nat is not Main.nat

117Mod.idr:11:1:public export Mod.natexp can't refer to export Mod.natfn

118reg070.idr:7:1:

119Test_show.Te implementation of Prelude.Show.Show is possibly not total due to: Prelude.Show.Test_show.Te implementation of Prelude.Show.Show, method show

120+./reg076.idr:8:1: error: Missing

121+ fixity declaration for

122+ Main.:>, expected: "->", "=>",

123+ ambiguous use of a left-associative operator,

124+ ambiguous use of a non-associative operator,

125+ ambiguous use of a right-associative operator

126+<EOF>

127+^

128+./reg077.idr:3:1: error: Missing

129+ fixity declaration for

130+ Main.:>>, expected: ")", ";",

131+ "in", start of block

132+<EOF>

133+^

120DoubleEquality.idr:4:87:When checking right hand side of oops with expected type

134DoubleEquality.idr:4:87:When checking right hand side of oops with expected type

121 Void

135 Void

122

136

test/regression002/reg076.idrnew file+7

@@ -0,0 +1,7 @@

1+

2+data Qux : a -> Type where

3+ Tux : String -> Qux a

4+

5+data Bar : a -> Type where

6+ Nil : Bar a

7+ (:>) : Qux a -> Bar a -> Bar a

test/regression002/reg077.idrnew file+2

@@ -0,0 +1,2 @@

1+

2+data (:>>) : a -> b -> Type where

test/regression002/run+2

@@ -29,6 +29,8 @@ ${IDRIS:-idris} $@ --nobanner --nocolour --quiet <<!

29:load reg068.idr

30:load reg069.idr

31:load reg070.idr

32+:load reg076.idr

33+:load reg077.idr

32:load DoubleEquality.idr

34:load DoubleEquality.idr

33!

35!

34

36