git.iko.soy/Idris-dev
on 75feef7 help sign in
Idris-dev/src/Idris/Parser/Data.hs
304 lines 13 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]
137dataOpts :: DataOpts -> IdrisParser DataOpts
138dataOpts opts =
139 do reserved "%error_reverse"; dataOpts (DataErrRev : opts)
140 <|> return opts
141 <?> "data options"
143{- | Parses a data type declaration
144Data ::= DocComment? Accessibility? DataI FnName TypeSig ExplicitTypeDataRest?
145 | DocComment? Accessibility? DataI FnName Name* DataRest?
146 ;
147Constructor' ::= Constructor KeepTerminator;
148ExplicitTypeDataRest ::= 'where' OpenBlock Constructor'* CloseBlock;
150DataRest ::= '=' SimpleConstructorList Terminator
151  | 'where'!
152 ;
153SimpleConstructorList ::=
154 SimpleConstructor
155 | SimpleConstructor '|' SimpleConstructorList
156 ;
157-}
158data_ :: SyntaxInfo -> IdrisParser PDecl
159data_ syn = (checkDeclFixity $
160 do (doc, argDocs, acc, dataOpts) <- P.try (do
161 (doc, argDocs) <- P.option noDocs docComment
162 pushIndent
163 acc <- accessibility
164 errRev <- dataOpts []
165 co <- dataI
166 ist <- get
167 let dataOpts = errRev ++ co
168 doc' = annotCode (tryFullExpr syn ist) doc
169 argDocs' = [ (n, annotCode (tryFullExpr syn ist) d)
170 | (n, d) <- argDocs ]
171 return (doc', argDocs', acc, dataOpts))
172 (tyn_in, nfc) <- withExtent fnName
173 (do P.try (lchar ':')
174 ty <- typeExpr (allowImp syn)
175 let tyn = expandNS syn tyn_in
176 d <- P.option (PData doc argDocs syn nfc dataOpts (PLaterdecl tyn nfc ty)) (do
177 keyword "where"
178 cons <- indentedBlock (constructor syn)
179 accData acc tyn (map (\ (_, _, n, _, _, _, _) -> n) cons)
180 return $ PData doc argDocs syn nfc dataOpts (PDatadecl tyn nfc ty cons))
181 terminator
182 return d) <|> (do
183 args <- many (do notEndApp
184 x <- name
185 return x)
186 let ty = bindArgs (map (const (PType nfc)) args) (PType nfc)
187 let tyn = expandNS syn tyn_in
188 d <- P.option (PData doc argDocs syn nfc dataOpts (PLaterdecl tyn nfc ty)) (do
189 P.try (lchar '=') <|> do keyword "where"
190 let kw = (if Codata `elem` dataOpts then "co" else "") ++ "data "
191 let n = show tyn_in ++ " "
192 let s = kw ++ n
193 let as = unwords (map show args) ++ " "
194 let ns = concat (intersperse " -> " $ map ((\x -> "(" ++ x ++ " : Type)") . show) args)
195 let ss = concat (intersperse " -> " $ map (const "Type") args)
196 let fix1 = s ++ as ++ " = ..."
197 let fix2 = s ++ ": " ++ ns ++ " -> Type where\n ..."
198 let fix3 = s ++ ": " ++ ss ++ " -> Type where\n ..."
199 fail $ fixErrorMsg "unexpected \"where\"" [fix1, fix2, fix3]
200 cons <- P.sepBy1 (simpleConstructor (syn { withAppAllowed = False })) (reservedOp "|")
201 let conty = mkPApp nfc (PRef nfc [] tyn) (map (PRef nfc []) args)
202 cons' <- mapM (\ (doc, argDocs, x, xfc, cargs, cfc, fs) ->
203 do let cty = bindArgs cargs conty
204 return (doc, argDocs, x, xfc, cty, cfc, fs)) cons
205 accData acc tyn (map (\ (_, _, n, _, _, _, _) -> n) cons')
206 return $ PData doc argDocs syn nfc dataOpts (PDatadecl tyn nfc ty cons'))
207 terminator
208 return d))
209 <?> "data type declaration"
210 where
211 mkPApp :: FC -> PTerm -> [PTerm] -> PTerm
212 mkPApp fc t [] = t
213 mkPApp fc t xs = PApp fc t (map pexp xs)
214 bindArgs :: [PTerm] -> PTerm -> PTerm
215 bindArgs xs t = foldr (PPi expl (sMN 0 "_t") NoFC) t xs
218{- | Parses a type constructor declaration
219 Constructor ::= DocComment? FnName TypeSig;
220-}
221constructor :: SyntaxInfo -> IdrisParser (Docstring (Either Err PTerm), [(Name, Docstring (Either Err PTerm))], Name, FC, PTerm, FC, [Name])
222constructor syn
223 = do (doc, argDocs) <- P.option noDocs docComment
224 (cn_in, nfc) <- withExtent fnName
225 let cn = expandNS syn cn_in
226 lchar ':'
227 fs <- P.option [] (do lchar '%'; reserved "erase"
228 P.sepBy1 name (lchar ','))
229 (ty, fc) <- withExtent $ typeExpr (allowImp syn)
230 ist <- get
231 let doc' = annotCode (tryFullExpr syn ist) doc
232 argDocs' = [ (n, annotCode (tryFullExpr syn ist) d)
233 | (n, d) <- argDocs ]
234 checkNameFixity cn
235 return (doc', argDocs', cn, nfc, ty, fc, fs)
236 <?> "constructor"
238{- | Parses a constructor for simple discriminated union data types
239 SimpleConstructor ::= FnName SimpleExpr* DocComment?
240-}
241simpleConstructor :: SyntaxInfo -> IdrisParser (Docstring (Either Err PTerm), [(Name, Docstring (Either Err PTerm))], Name, FC, [PTerm], FC, [Name])
242simpleConstructor syn
243 = (appExtent $ do
244 (doc, _) <- P.option noDocs (P.try docComment)
245 ist <- get
246 let doc' = annotCode (tryFullExpr syn ist) doc
247 (cn_in, nfc) <- withExtent fnName
248 let cn = expandNS syn cn_in
249 args <- many (do notEndApp
250 simpleExpr syn)
251 checkNameFixity cn
252 return $ \fc -> (doc', [], cn, nfc, args, fc, []))
253 <?> "constructor"
254{- | Parses a dsl block declaration
255DSL ::= 'dsl' FnName OpenBlock Overload'+ CloseBlock;
256 -}
257dsl :: SyntaxInfo -> IdrisParser PDecl
258dsl syn = do keyword "dsl"
259 n <- fnName
260 bs <- indentedBlock (overload syn)
261 let dsl = mkDSL bs (dsl_info syn)
262 checkDSL dsl
263 i <- get
264 put (i { idris_dsls = addDef n dsl (idris_dsls i) })
265 return (PDSL n dsl)
266 <?> "dsl block declaration"
267 where mkDSL :: [(String, PTerm)] -> DSL -> DSL
268 mkDSL bs dsl = let var = lookup "variable" bs
269 first = lookup "index_first" bs
270 next = lookup "index_next" bs
271 leto = lookup "let" bs
272 lambda = lookup "lambda" bs
273 pi = lookup "pi" bs in
274 initDSL { dsl_var = var,
275 index_first = first,
276 index_next = next,
277 dsl_lambda = lambda,
278 dsl_let = leto,
279 dsl_pi = pi }
281{- | Checks DSL for errors -}
282-- FIXME: currently does nothing, check if DSL is really sane
283--
284-- Issue #1595 on the Issue Tracker
285--
286-- https://github.com/idris-lang/Idris-dev/issues/1595
287--
288checkDSL :: DSL -> IdrisParser ()
289checkDSL dsl = return ()
291{- | Parses a DSL overload declaration
292OverloadIdentifier ::= 'let' | Identifier;
293Overload ::= OverloadIdentifier '=' Expr;
294-}
295overload :: SyntaxInfo -> IdrisParser (String, PTerm)
296overload syn = do o <- highlight AnnKeyword $ identifier <|> "let" <$ reserved "let"
297 if o `notElem` overloadable
298 then fail $ show o ++ " is not an overloading"
299 else do
300 lchar '='
301 t <- expr syn
302 return (o, t)
303 <?> "dsl overload declaratioN"
304 where overloadable = ["let","lambda","pi","index_first","index_next","variable"]