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