git.iko.soy/Idris-dev
on bc8da8d help sign in
Idris-dev/src/Idris/Parser/Data.hs
325 lines 14 kB history raw
1{-|
2Module : Idris.Parser.Data
3Description : Parse Data declarations.
5License : BSD3
6Maintainer : The Idris Community.
7-}
8{-# LANGUAGE ConstraintKinds, GeneralizedNewtypeDeriving, PatternGuards #-}
9module Idris.Parser.Data where
11import Idris.AbsSyntax
12import Idris.Core.TT
13import Idris.Docstrings
14import Idris.Options
15import Idris.Parser.Expr
16import Idris.Parser.Helpers
17import Idris.Parser.Ops
19import Prelude hiding (pi)
21import Control.Applicative
22import Control.Monad.State.Strict
23import Data.List
24import Data.Maybe
25import Text.Megaparsec ((<?>))
26import qualified Text.Megaparsec as P
28{- | Parses a record type declaration
29Record ::=
30 DocComment Accessibility? 'record' FnName TypeSig 'where' OpenBlock Constructor KeepTerminator CloseBlock;
31-}
32record :: SyntaxInfo -> IdrisParser PDecl
33record syn = do (doc, paramDocs, acc, opts) <- P.try (do
34 (doc, paramDocs) <- P.option noDocs docComment
35 ist <- get
36 let doc' = annotCode (tryFullExpr syn ist) doc
37 paramDocs' = [ (n, annotCode (tryFullExpr syn ist) d)
38 | (n, d) <- paramDocs ]
39 acc <- accessibility
40 opts <- dataOpts []
41 co <- recordI
42 return (doc', paramDocs', acc, opts ++ co))
43 fc <- getFC
44 (tyn_in, nfc) <- fnName
45 let tyn = expandNS syn tyn_in
46 let rsyn = syn { syn_namespace = show (nsroot tyn) :
47 syn_namespace syn }
48 params <- P.manyTill (recordParameter rsyn) (reservedHL "where")
49 (fields, cname, cdoc) <- indentedBlockS $ recordBody rsyn tyn
50 let fnames = map (expandNS rsyn) (mapMaybe getName fields)
51 case cname of
52 Just cn' -> accData acc tyn (fst cn' : fnames)
53 Nothing -> return ()
54 return $ PRecord doc rsyn fc opts tyn nfc params paramDocs fields cname cdoc syn
55 <?> "record type declaration"
56 where
57 getName (Just (n, _), _, _, _) = Just n
58 getName _ = Nothing
60 recordBody :: SyntaxInfo -> Name -> IdrisParser ([((Maybe (Name, FC)), Plicity, PTerm, Maybe (Docstring (Either Err PTerm)))], Maybe (Name, FC), Docstring (Either Err PTerm))
61 recordBody syn tyn = do
62 ist <- get
63 fc <- getFC
65 (constructorName, constructorDoc) <- P.option (Nothing, emptyDocstring)
66 (do (doc, _) <- P.option noDocs docComment
67 n <- 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) <- 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 :: IdrisParser (Name, FC)
95 constructor = (reservedHL "constructor") *> fnName
98 endPlicity :: Maybe Char -> IdrisParser Plicity
99 endPlicity (Just _) = do lchar '}'
100 return impl
101 endPlicity Nothing = return expl
103 annotate :: SyntaxInfo -> IState -> Docstring () -> Docstring (Either Err PTerm)
104 annotate syn ist = annotCode $ tryFullExpr syn ist
106recordParameter :: SyntaxInfo -> IdrisParser (Name, FC, Plicity, PTerm)
107recordParameter syn =
108 (do lchar '('
109 (n, nfc, pt) <- (namedTy syn <|> onlyName syn)
110 lchar ')'
111 return (n, nfc, expl, pt))
112 <|>
113 (do (n, nfc, pt) <- onlyName syn
114 return (n, nfc, expl, pt))
115 where
116 namedTy :: SyntaxInfo -> IdrisParser (Name, FC, PTerm)
117 namedTy syn =
118 do (n, nfc) <- fnName
119 lchar ':'
120 ty <- typeExpr (allowImp syn)
121 return (expandNS syn n, nfc, ty)
122 onlyName :: SyntaxInfo -> IdrisParser (Name, FC, PTerm)
123 onlyName syn =
124 do (n, nfc) <- fnName
125 fc <- getFC
126 return (expandNS syn n, nfc, PType fc)
128{- | Parses data declaration type (normal or codata)
129DataI ::= 'data' | 'codata';
130-}
131dataI :: IdrisParser DataOpts
132dataI = do reservedHL "data"; return []
133 <|> do reservedHL "codata"; return [Codata]
135recordI :: IdrisParser DataOpts
136recordI = do reservedHL "record"; return []
137 <|> do reservedHL "corecord"; return [Codata]
139{- | Parses if a data should not have a default eliminator
140DefaultEliminator ::= 'noelim'?
141 -}
142dataOpts :: DataOpts -> IdrisParser DataOpts
143dataOpts opts
144 = do fc <- reservedFC "%elim"
145 warnElim fc
146 dataOpts (DefaultEliminator : DefaultCaseFun : opts)
147 <|> do fc <- reservedFC "%case"
148 warnElim fc
149 dataOpts (DefaultCaseFun : opts)
150 <|> do reserved "%error_reverse"; dataOpts (DataErrRev : opts)
151 <|> return opts
152 <?> "data options"
153 where warnElim fc =
154 parserWarning fc (Just NoElimDeprecationWarnings) (Msg "The 'class' keyword is deprecated. Use 'interface' instead.")
156{- | Parses a data type declaration
157Data ::= DocComment? Accessibility? DataI DefaultEliminator FnName TypeSig ExplicitTypeDataRest?
158 | DocComment? Accessibility? DataI DefaultEliminator FnName Name* DataRest?
159 ;
160Constructor' ::= Constructor KeepTerminator;
161ExplicitTypeDataRest ::= 'where' OpenBlock Constructor'* CloseBlock;
163DataRest ::= '=' SimpleConstructorList Terminator
164  | 'where'!
165 ;
166SimpleConstructorList ::=
167 SimpleConstructor
168 | SimpleConstructor '|' SimpleConstructorList
169 ;
170-}
171data_ :: SyntaxInfo -> IdrisParser PDecl
172data_ syn = (checkDeclFixity $
173 do (doc, argDocs, acc, dataOpts) <- P.try (do
174 (doc, argDocs) <- P.option noDocs docComment
175 pushIndent
176 acc <- accessibility
177 elim <- dataOpts []
178 co <- dataI
179 ist <- get
180 let dataOpts = combineDataOpts (elim ++ co)
181 doc' = annotCode (tryFullExpr syn ist) doc
182 argDocs' = [ (n, annotCode (tryFullExpr syn ist) d)
183 | (n, d) <- argDocs ]
184 return (doc', argDocs', acc, dataOpts))
185 fc <- getFC
186 (tyn_in, nfc) <- 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 fc dataOpts (PLaterdecl tyn nfc ty)) (do
191 reservedHL "where"
192 cons <- indentedBlock (constructor syn)
193 accData acc tyn (map (\ (_, _, n, _, _, _, _) -> n) cons)
194 return $ PData doc argDocs syn fc dataOpts (PDatadecl tyn nfc ty cons))
195 terminator
196 return d) <|> (do
197 args <- many (do notEndApp
198 x <- fst <$> name
199 return x)
200 let ty = bindArgs (map (const (PType fc)) args) (PType fc)
201 let tyn = expandNS syn tyn_in
202 d <- P.option (PData doc argDocs syn fc dataOpts (PLaterdecl tyn nfc ty)) (do
203 P.try (lchar '=') <|> do reservedHL "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 fc (PRef fc [] tyn) (map (PRef fc []) 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 fc 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) <- fnName; fc <- getFC
243 let cn = expandNS syn cn_in
244 lchar ':'
245 fs <- P.option [] (do lchar '%'; reserved "erase"
246 P.sepBy1 (fst <$> name) (lchar ','))
247 ty <- 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 = do (doc, _) <- P.option noDocs (P.try docComment)
262 ist <- get
263 let doc' = annotCode (tryFullExpr syn ist) doc
264 (cn_in, nfc) <- fnName
265 let cn = expandNS syn cn_in
266 fc <- getFC
267 args <- many (do notEndApp
268 simpleExpr syn)
269 checkNameFixity cn
270 return (doc', [], cn, nfc, args, fc, [])
271 <?> "constructor"
273{- | Parses a dsl block declaration
274DSL ::= 'dsl' FnName OpenBlock Overload'+ CloseBlock;
275 -}
276dsl :: SyntaxInfo -> IdrisParser PDecl
277dsl syn = do reservedHL "dsl"
278 n <- fst <$> fnName
279 bs <- indentedBlock (overload syn)
280 let dsl = mkDSL bs (dsl_info syn)
281 checkDSL dsl
282 i <- get
283 put (i { idris_dsls = addDef n dsl (idris_dsls i) })
284 return (PDSL n dsl)
285 <?> "dsl block declaration"
286 where mkDSL :: [(String, PTerm)] -> DSL -> DSL
287 mkDSL bs dsl = let var = lookup "variable" bs
288 first = lookup "index_first" bs
289 next = lookup "index_next" bs
290 leto = lookup "let" bs
291 lambda = lookup "lambda" bs
292 pi = lookup "pi" bs in
293 initDSL { dsl_var = var,
294 index_first = first,
295 index_next = next,
296 dsl_lambda = lambda,
297 dsl_let = leto,
298 dsl_pi = pi }
300{- | Checks DSL for errors -}
301-- FIXME: currently does nothing, check if DSL is really sane
302--
303-- Issue #1595 on the Issue Tracker
304--
305-- https://github.com/idris-lang/Idris-dev/issues/1595
306--
307checkDSL :: DSL -> IdrisParser ()
308checkDSL dsl = return ()
310{- | Parses a DSL overload declaration
311OverloadIdentifier ::= 'let' | Identifier;
312Overload ::= OverloadIdentifier '=' Expr;
313-}
314overload :: SyntaxInfo -> IdrisParser (String, PTerm)
315overload syn = do (o, fc) <- identifier <|> do fc <- reservedFC "let"
316 return ("let", fc)
317 if o `notElem` overloadable
318 then fail $ show o ++ " is not an overloading"
319 else do
320 highlightP fc AnnKeyword
321 lchar '='
322 t <- expr syn
323 return (o, t)
324 <?> "dsl overload declaratioN"
325 where overloadable = ["let","lambda","pi","index_first","index_next","variable"]