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

git.iko.soy/Idris-dev

Merge pull request #3294 from beark/FixityFix

Fix #3275

commit6eadbe82e71609e4a1160456ae9643cac476aa4a authorDavid Christiansen <david@davidchristiansen.dk> dateTue 9 Aug 2016, 17:24 (10 years ago) parent1aba372 ea0f628

8 files changed+54−18

compare with master

unifiedsplit

CONTRIBUTORS+1 src/Idris/Parser.hs+1−17 src/Idris/Parser/Data.hs+4−1 src/Idris/Parser/Ops.hs+23 test/regression002/expected+14 test/regression002/reg076.idr+7 test/regression002/reg077.idr+2 test/regression002/run+2

CONTRIBUTORS+1

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

5151Daniel Waterworth

5252Eric Weinstein

5353Jonas Westerlund

54+Björn Aili

src/Idris/Parser.hs+1−17

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

598598@

599599-}

600600fnDecl' :: SyntaxInfo -> IdrisParser PDecl

601−fnDecl' syn = checkFixity $

601+fnDecl' syn = checkDeclFixity $

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

603603 pushIndent

604604 (doc, argDocs) <- docstring syn

@@ -618,22 +618,6 @@ 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

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

637621

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

639623

src/Idris/Parser/Data.hs+4−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 = checkDeclFixity $

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

202203 (doc, argDocs) <- option noDocs docComment

203204 pushIndent

204205 acc <- accessibility

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

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

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

279280 | (n, d) <- argDocs ]

281+ checkNameFixity cn

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

281283 <?> "constructor"

282284

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

293295 fc <- getFC

294296 args <- many (do notEndApp

295297 simpleExpr syn)

298+ checkNameFixity cn

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

297300 <?> "constructor"

298301

src/Idris/Parser/Ops.hs+23

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

161161 extractName :: FixDecl -> String

162162 extractName (Fix _ n) = n

163163

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+

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

165188@

166189 FixityType ::=

test/regression002/expected+14

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

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

118118reg070.idr:7:1:

119119Test_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+^

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

121135 Void

122136

test/regression002/reg076.idrnew file+7

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

2+data Qux : a -> Type where

3+ Tux : String -> Qux a

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

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

test/regression002/run+2

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

2929:load reg068.idr

3030:load reg069.idr

3131:load reg070.idr

32+:load reg076.idr

33+:load reg077.idr

3234:load DoubleEquality.idr

3335!

3436