git.iko.soy/Idris-dev
on master help sign in
Instance docs: factor away unnecessary try:s
df1a933Adam Sandberg Eriksson
src/Idris/Parser.hs+33−30
compare with master
unifiedsplit
@@ -45,7 +45,7 @@ import Paths_idris
45import Util.DynamicLinker
45import Util.DynamicLinker
46import qualified Util.Pretty as P
46import qualified Util.Pretty as P
47
47
48−import Idris.Core.TT
48+import Idris.Core.TT as TT
49import Idris.Core.Evaluate
49import Idris.Core.Evaluate
50
50
51import Control.Applicative hiding (Const)
51import Control.Applicative hiding (Const)
@@ -87,7 +87,7 @@ import System.IO
87{- | Parses module definition
87{- | Parses module definition
88
88
89@
89@
90− ModuleHeader ::= 'module' Identifier_t ';'?;
90+ ModuleHeader ::= DocComment_t? 'module' Identifier_t ';'?;
91@
91@
92-}
92-}
93moduleHeader :: IdrisParser (Maybe (Docstring ()), [String])
93moduleHeader :: IdrisParser (Maybe (Docstring ()), [String])
@@ -178,7 +178,8 @@ decl syn = do fc <- getFC
178 <|> params syn
178 <|> params syn
179 <|> mutual syn
179 <|> mutual syn
180 <|> namespace syn
180 <|> namespace syn
181+ <|> class_ syn
181− <|> (try (class_ syn) <|> instance_ syn)
182+ <|> instance_ syn
182 <|> do d <- dsl syn; return [d]
183 <|> do d <- dsl syn; return [d]
183 <|> directive syn
184 <|> directive syn
184 <|> provider syn
185 <|> provider syn
@@ -347,13 +348,9 @@ fnDecl' :: SyntaxInfo -> IdrisParser PDecl
347fnDecl' syn = checkFixity $
348fnDecl' syn = checkFixity $
348 do (doc, argDocs, fc, opts', n, acc) <- try (do
349 do (doc, argDocs, fc, opts', n, acc) <- try (do
349 pushIndent
350 pushIndent
350− (doc, argDocs) <- option noDocs docComment
351+ (doc, argDocs) <- docstring syn
351 ist <- get
352 ist <- get
352− let doc' = annotCode (tryFullExpr syn ist) doc
353− argDocs' = [ (n, annotCode (tryFullExpr syn ist) d)
354− | (n, d) <- argDocs ]
355−
356− initOpts = if default_total ist
353+ let initOpts = if default_total ist
357 then [TotalFn]
354 then [TotalFn]
358 else []
355 else []
359 opts <- fnOpts initOpts
356 opts <- fnOpts initOpts
@@ -363,7 +360,7 @@ fnDecl' syn = checkFixity $
363 let n = expandNS syn n_in
360 let n = expandNS syn n_in
364 fc <- getFC
361 fc <- getFC
365 lchar ':'
362 lchar ':'
366− return (doc', argDocs', fc, opts', n, acc))
363+ return (doc, argDocs, fc, opts', n, acc))
367 ty <- typeExpr (allowImp syn)
364 ty <- typeExpr (allowImp syn)
368 terminator
365 terminator
369 addAcc n acc
366 addAcc n acc
@@ -458,12 +455,10 @@ Postulate ::=
458@
455@
459-}
456-}
460postulate :: SyntaxInfo -> IdrisParser PDecl
457postulate :: SyntaxInfo -> IdrisParser PDecl
461−postulate syn = do doc <- try $ do (doc, _) <- option noDocs docComment
458+postulate syn = do doc <- try $ do (doc, _) <- docstring syn
462− ist <- get
463− let doc' = annotCode (tryFullExpr syn ist) doc
464 pushIndent
459 pushIndent
465 reserved "postulate"
460 reserved "postulate"
466− return doc'
461+ return doc
467 ist <- get
462 ist <- get
468 let initOpts = if default_total ist
463 let initOpts = if default_total ist
469 then [TotalFn]
464 then [TotalFn]
@@ -586,7 +581,7 @@ ClassBlock ::=
586classBlock :: SyntaxInfo -> IdrisParser [PDecl]
581classBlock :: SyntaxInfo -> IdrisParser [PDecl]
587classBlock syn = do reserved "where"
582classBlock syn = do reserved "where"
588 openBlock
583 openBlock
589− ds <- many (try (notEndBlock >> instance_ syn) <|> fnDecl syn)
584+ ds <- many (notEndBlock >> instance_ syn <|> fnDecl syn)
590 closeBlock
585 closeBlock
591 return (concat ds)
586 return (concat ds)
592 <?> "class block"
587 <?> "class block"
@@ -607,15 +602,14 @@ Class ::=
607@
602@
608-}
603-}
609class_ :: SyntaxInfo -> IdrisParser [PDecl]
604class_ :: SyntaxInfo -> IdrisParser [PDecl]
610−class_ syn = do (doc, argDocs, acc) <- try (do
605+class_ syn = do (doc, argDocs, acc)
611− (doc, argDocs) <- option noDocs docComment
606+ <- try (do (doc, argDocs) <- docstring syn
612− ist <- get
613− let doc' = annotCode (tryFullExpr syn ist) doc
614− argDocs' = [ (n, annotCode (tryFullExpr syn ist) d)
615− | (n, d) <- argDocs ]
616− acc <- optional accessibility
607+ acc <- optional accessibility
617− return (doc', argDocs', acc))
608+ reserved "class"
609+ return (doc, argDocs, acc))
610+ fc <- getFC
618− reserved "class"; fc <- getFC; cons <- constraintList syn; n_in <- fnName
611+ cons <- constraintList syn
612+ n_in <- fnName
619 let n = expandNS syn n_in
613 let n = expandNS syn n_in
620 cs <- many carg
614 cs <- many carg
621 ds <- option [] (classBlock syn)
615 ds <- option [] (classBlock syn)
@@ -642,12 +636,9 @@ InstanceName ::= '[' Name ']';
642@
636@
643-}
637-}
644instance_ :: SyntaxInfo -> IdrisParser [PDecl]
638instance_ :: SyntaxInfo -> IdrisParser [PDecl]
645−instance_ syn = do doc <- try (do
639+instance_ syn = do (doc, _)
646− (doc, _) <- option noDocs docComment
647− ist <- get
648− let doc' = annotCode (tryFullExpr syn ist) doc
649− return doc')
650− reserved "instance"; fc <- getFC
640+ <- try (docstring syn <* reserved "instance")
641+ fc <- getFC
651 en <- optional instanceName
642 en <- optional instanceName
652 cs <- constraintList syn
643 cs <- constraintList syn
653 cn <- fnName
644 cn <- fnName
@@ -664,6 +655,18 @@ instance_ syn = do doc <- try (do
664 <?> "instance name"
655 <?> "instance name"
665
656
666
657
658+-- | Parse a docstring
659+docstring :: SyntaxInfo
660+ -> IdrisParser (Docstring (Either TT.Err PTerm),
661+ [(Name,Docstring (Either TT.Err PTerm))])
662+docstring syn = do (doc, argDocs) <- option noDocs docComment
663+ ist <- get
664+ let doc' = annotCode (tryFullExpr syn ist) doc
665+ argDocs' = [ (n, annotCode (tryFullExpr syn ist) d)
666+ | (n, d) <- argDocs ]
667+ return (doc', argDocs')
668+
669+
667{- | Parses a using declaration list
670{- | Parses a using declaration list
668
671
669@
672@