git.iko.soy/Idris-dev
on d773edd help sign in
Idris-dev/src/Idris/Parser/Data.hs
322 lines 14 kB history raw
1{-|
2Module : Idris.Parser.Data
3Description : Parse Data declarations.
5License : BSD3
6Maintainer : The Idris Community.
7-}
8{-# LANGUAGE ConstraintKinds, FlexibleContexts, GeneralizedNewtypeDeriving,
9 MultiParamTypeClasses, PatternGuards #-}
10module Idris.Parser.Data where
12import Idris.AbsSyntax
13import Idris.Core.TT
14import Idris.Docstrings
15import Idris.Options
16import Idris.Parser.Expr
17import Idris.Parser.Helpers
18import Idris.Parser.Ops
20import Prelude hiding (pi)
22import Control.Applicative
23import Control.Monad.State.Strict
24import Data.List
25import Data.Maybe
26import Text.Megaparsec ((<?>))
27import qualified Text.Megaparsec as P
29{- | Parses a record type declaration
30Record ::=
31 DocComment Accessibility? 'record' FnName TypeSig 'where' OpenBlock Constructor KeepTerminator CloseBlock;
32-}
33record :: SyntaxInfo -> IdrisParser PDecl
34record syn = (appExtent $ do
35 (doc, paramDocs, acc, opts) <- P.try (do
36 (doc, paramDocs) <- P.option noDocs docComment
37 ist <- get
38 let doc' = annotCode (tryFullExpr syn ist) doc
39 paramDocs' = [ (n, annotCode (tryFullExpr syn ist) d)
40 | (n, d) <- paramDocs ]
41 acc <- accessibility
42 opts <- dataOpts []
43 co <- recordI
44 return (doc', paramDocs', acc, opts ++ co))
45 (tyn_in, nfc) <- withExtent fnName
46 let tyn = expandNS syn tyn_in
47 let rsyn = syn { syn_namespace = show (nsroot tyn) :
48 syn_namespace syn }
49 params <- P.manyTill (recordParameter rsyn) (keyword "where")
50 (fields, cname, cdoc) <- indentedBlockS $ recordBody rsyn tyn
51 let fnames = map (expandNS rsyn) (mapMaybe getName fields)
52 case cname of
53 Just cn' -> accData acc tyn (fst cn' : fnames)
54 Nothing -> return ()
55 return $ \fc -> PRecord doc rsyn fc opts tyn nfc params paramDocs fields cname cdoc syn)
56 <?> "record type declaration"
57 where
58 getName (Just (n, _), _, _, _) = Just n
59 getName _ = Nothing
61 recordBody :: SyntaxInfo -> Name -> IdrisParser ([((Maybe (Name, FC)), Plicity, PTerm, Maybe (Docstring (Either Err PTerm)))], Maybe (Name, FC), Docstring (Either Err PTerm))
62 recordBody syn tyn = do
63 ist <- get
65 (constructorName, constructorDoc) <- P.option (Nothing, emptyDocstring)
66 (do (doc, _) <- P.option noDocs docComment
67 n <- withExtent constructor
68 return (Just n, doc))
70 let constructorDoc' = annotate syn ist constructorDoc
72 fields <- many . indented $ fieldLine syn
74 return (concat fields, constructorName, constructorDoc')
75 where
76 fieldLine :: SyntaxInfo -> IdrisParser [(Maybe (Name, FC), Plicity, PTerm, Maybe (Docstring (Either Err PTerm)))]
77 fieldLine syn = do
78 doc <- optional docComment
79 c <- optional $ lchar '{'
80 let oneName = (do (n, nfc) <- withExtent fnName
81 return $ Just (expandNS syn n, nfc))
82 <|> (symbol "_" >> return Nothing)
83 ns <- commaSeparated oneName
84 lchar ':'
85 -- Implicits are scoped in fields (fields aren't top level)
86 t <- typeExpr (scopedImp syn)
87 p <- endPlicity c
88 ist <- get
89 let doc' = case doc of -- Temp: Throws away any possible arg docs
90 Just (d,_) -> Just $ annotate syn ist d
91 Nothing -> Nothing
92 return $ map (\n -> (n, p, t, doc')) ns
94 constructor :: (Parsing m, MonadState IState m) => m Name
95 constructor = keyword "constructor" *> fnName
97 endPlicity :: Maybe Char -> IdrisParser Plicity
98 endPlicity (Just _) = do lchar '}'
99 return impl
100 endPlicity Nothing = return expl
102 annotate :: SyntaxInfo -> IState -> Docstring () -> Docstring (Either Err PTerm)
103 annotate syn ist = annotCode $ tryFullExpr syn ist
105recordParameter :: SyntaxInfo -> IdrisParser (Name, FC, Plicity, PTerm)
106recordParameter syn =
107 (do lchar '('
108 (n, nfc, pt) <- (namedTy syn <|> onlyName syn)
109 lchar ')'
110 return (n, nfc, expl, pt))
111 <|>
112 (do (n, nfc, pt) <- onlyName syn
113 return (n, nfc, expl, pt))
114 where
115 namedTy :: SyntaxInfo -> IdrisParser (Name, FC, PTerm)
116 namedTy syn =
117 do (n, nfc) <- withExtent fnName
118 lchar ':'
119 ty <- typeExpr (allowImp syn)
120 return (expandNS syn n, nfc, ty)
121 onlyName :: SyntaxInfo -> IdrisParser (Name, FC, PTerm)
122 onlyName syn =
123 do (n, nfc) <- withExtent fnName
124 return (expandNS syn n, nfc, PType nfc)
126{- | Parses data declaration type (normal or codata)
127DataI ::= 'data' | 'codata';
128-}
129dataI :: IdrisParser DataOpts
130dataI = do keyword "data"; return []
131 <|> do keyword "codata"; return [Codata]
133recordI :: IdrisParser DataOpts
134recordI = do keyword "record"; return []
135 <|> do keyword "corecord"; return [Codata]
137{- | Parses if a data should not have a default eliminator
138DefaultEliminator ::= 'noelim'?
139 -}
140dataOpts :: DataOpts -> IdrisParser DataOpts
141dataOpts opts
142 = do let kw = "%elim"
143 fc <- extent $ reserved kw
144 warnElim fc kw
145 dataOpts (DefaultEliminator : DefaultCaseFun : opts)
146 <|> do let kw = "%case"
147 fc <- extent $ reserved kw
148 warnElim fc kw
149 dataOpts (DefaultCaseFun : opts)
150 <|> do reserved "%error_reverse"; dataOpts (DataErrRev : opts)
151 <|> return opts
152 <?> "data options"
153 where warnElim fc kw =
154 parserWarning fc (Just NoElimDeprecationWarnings)
155 (Msg ("The '" ++ kw ++ "' directive is deprecated."))
157{- | Parses a data type declaration
158Data ::= DocComment? Accessibility? DataI DefaultEliminator FnName TypeSig ExplicitTypeDataRest?
159 | DocComment? Accessibility? DataI DefaultEliminator FnName Name* DataRest?
160 ;
161Constructor' ::= Constructor KeepTerminator;
162ExplicitTypeDataRest ::= 'where' OpenBlock Constructor'* CloseBlock;
164DataRest ::= '=' SimpleConstructorList Terminator
165  | 'where'!
166 ;
167SimpleConstructorList ::=
168 SimpleConstructor
169 | SimpleConstructor '|' SimpleConstructorList
170 ;
171-}
172data_ :: SyntaxInfo -> IdrisParser PDecl
173data_ syn = (checkDeclFixity $
174 do (doc, argDocs, acc, dataOpts) <- P.try (do
175 (doc, argDocs) <- P.option noDocs docComment
176 pushIndent
177 acc <- accessibility
178 elim <- dataOpts []
179 co <- dataI
180 ist <- get
181 let dataOpts = combineDataOpts (elim ++ co)
182 doc' = annotCode (tryFullExpr syn ist) doc
183 argDocs' = [ (n, annotCode (tryFullExpr syn ist) d)
184 | (n, d) <- argDocs ]
185 return (doc', argDocs', acc, dataOpts))
186 (tyn_in, nfc) <- withExtent fnName
187 (do P.try (lchar ':')
188 ty <- typeExpr (allowImp syn)
189 let tyn = expandNS syn tyn_in
190 d <- P.option (PData doc argDocs syn nfc dataOpts (PLaterdecl tyn nfc ty)) (do
191 keyword "where"
192 cons <- indentedBlock (constructor syn)
193 accData acc tyn (map (\ (_, _, n, _, _, _, _) -> n) cons)
194 return $ PData doc argDocs syn nfc dataOpts (PDatadecl tyn nfc ty cons))
195 terminator
196 return d) <|> (do
197 args <- many (do notEndApp
198 x <- name
199 return x)
200 let ty = bindArgs (map (const (PType nfc)) args) (PType nfc)
201 let tyn = expandNS syn tyn_in
202 d <- P.option (PData doc argDocs syn nfc dataOpts (PLaterdecl tyn nfc ty)) (do
203 P.try (lchar '=') <|> do keyword "where"
204 let kw = (if DefaultEliminator `elem` dataOpts then "%elim" else "") ++ (if Codata `elem` dataOpts then "co" else "") ++ "data "
205 let n = show tyn_in ++ " "
206 let s = kw ++ n
207 let as = unwords (map show args) ++ " "
208 let ns = concat (intersperse " -> " $ map ((\x -> "(" ++ x ++ " : Type)") . show) args)
209 let ss = concat (intersperse " -> " $ map (const "Type") args)
210 let fix1 = s ++ as ++ " = ..."
211 let fix2 = s ++ ": " ++ ns ++ " -> Type where\n ..."
212 let fix3 = s ++ ": " ++ ss ++ " -> Type where\n ..."
213 fail $ fixErrorMsg "unexpected \"where\"" [fix1, fix2, fix3]
214 cons <- P.sepBy1 (simpleConstructor (syn { withAppAllowed = False })) (reservedOp "|")
215 let conty = mkPApp nfc (PRef nfc [] tyn) (map (PRef nfc []) args)
216 cons' <- mapM (\ (doc, argDocs, x, xfc, cargs, cfc, fs) ->
217 do let cty = bindArgs cargs conty
218 return (doc, argDocs, x, xfc, cty, cfc, fs)) cons
219 accData acc tyn (map (\ (_, _, n, _, _, _, _) -> n) cons')
220 return $ PData doc argDocs syn nfc dataOpts (PDatadecl tyn nfc ty cons'))
221 terminator
222 return d))
223 <?> "data type declaration"
224 where
225 mkPApp :: FC -> PTerm -> [PTerm] -> PTerm
226 mkPApp fc t [] = t
227 mkPApp fc t xs = PApp fc t (map pexp xs)
228 bindArgs :: [PTerm] -> PTerm -> PTerm
229 bindArgs xs t = foldr (PPi expl (sMN 0 "_t") NoFC) t xs
230 combineDataOpts :: DataOpts -> DataOpts
231 combineDataOpts opts = if Codata `elem` opts
232 then delete DefaultEliminator opts
233 else opts
236{- | Parses a type constructor declaration
237 Constructor ::= DocComment? FnName TypeSig;
238-}
239constructor :: SyntaxInfo -> IdrisParser (Docstring (Either Err PTerm), [(Name, Docstring (Either Err PTerm))], Name, FC, PTerm, FC, [Name])
240constructor syn
241 = do (doc, argDocs) <- P.option noDocs docComment
242 (cn_in, nfc) <- withExtent fnName
243 let cn = expandNS syn cn_in
244 lchar ':'
245 fs <- P.option [] (do lchar '%'; reserved "erase"
246 P.sepBy1 name (lchar ','))
247 (ty, fc) <- withExtent $ typeExpr (allowImp syn)
248 ist <- get
249 let doc' = annotCode (tryFullExpr syn ist) doc
250 argDocs' = [ (n, annotCode (tryFullExpr syn ist) d)
251 | (n, d) <- argDocs ]
252 checkNameFixity cn
253 return (doc', argDocs', cn, nfc, ty, fc, fs)
254 <?> "constructor"
256{- | Parses a constructor for simple discriminated union data types
257 SimpleConstructor ::= FnName SimpleExpr* DocComment?
258-}
259simpleConstructor :: SyntaxInfo -> IdrisParser (Docstring (Either Err PTerm), [(Name, Docstring (Either Err PTerm))], Name, FC, [PTerm], FC, [Name])
260simpleConstructor syn
261 = (appExtent $ do
262 (doc, _) <- P.option noDocs (P.try docComment)
263 ist <- get
264 let doc' = annotCode (tryFullExpr syn ist) doc
265 (cn_in, nfc) <- withExtent fnName
266 let cn = expandNS syn cn_in
267 args <- many (do notEndApp
268 simpleExpr syn)
269 checkNameFixity cn
270 return $ \fc -> (doc', [], cn, nfc, args, fc, []))
271 <?> "constructor"
272{- | Parses a dsl block declaration
273DSL ::= 'dsl' FnName OpenBlock Overload'+ CloseBlock;
274 -}
275dsl :: SyntaxInfo -> IdrisParser PDecl
276dsl syn = do keyword "dsl"
277 n <- fnName
278 bs <- indentedBlock (overload syn)
279 let dsl = mkDSL bs (dsl_info syn)
280 checkDSL dsl
281 i <- get
282 put (i { idris_dsls = addDef n dsl (idris_dsls i) })
283 return (PDSL n dsl)
284 <?> "dsl block declaration"
285 where mkDSL :: [(String, PTerm)] -> DSL -> DSL
286 mkDSL bs dsl = let var = lookup "variable" bs
287 first = lookup "index_first" bs
288 next = lookup "index_next" bs
289 leto = lookup "let" bs
290 lambda = lookup "lambda" bs
291 pi = lookup "pi" bs in
292 initDSL { dsl_var = var,
293 index_first = first,
294 index_next = next,
295 dsl_lambda = lambda,
296 dsl_let = leto,
297 dsl_pi = pi }
299{- | Checks DSL for errors -}
300-- FIXME: currently does nothing, check if DSL is really sane
301--
302-- Issue #1595 on the Issue Tracker
303--
304-- https://github.com/idris-lang/Idris-dev/issues/1595
305--
306checkDSL :: DSL -> IdrisParser ()
307checkDSL dsl = return ()
309{- | Parses a DSL overload declaration
310OverloadIdentifier ::= 'let' | Identifier;
311Overload ::= OverloadIdentifier '=' Expr;
312-}
313overload :: SyntaxInfo -> IdrisParser (String, PTerm)
314overload syn = do o <- highlight AnnKeyword $ identifier <|> "let" <$ reserved "let"
315 if o `notElem` overloadable
316 then fail $ show o ++ " is not an overloading"
317 else do
318 lchar '='
319 t <- expr syn
320 return (o, t)
321 <?> "dsl overload declaratioN"
322 where overloadable = ["let","lambda","pi","index_first","index_next","variable"]