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