git.iko.soy/Idris-dev
on ff01a4c help sign in
Idris-dev/src/Idris/Parser/Data.hs
348 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 t <- typeExpr (allowImp syn)
110 p <- endPlicity c
111 ist <- get
112 let doc' = case doc of -- Temp: Throws away any possible arg docs
113 Just (d,_) -> Just $ annotate syn ist d
114 Nothing -> Nothing
115 return $ map (\n -> (n, p, t, doc')) ns
117 constructor :: IdrisParser (Name, FC)
118 constructor = (reservedHL "constructor") *> fnName
121 endPlicity :: Maybe Char -> IdrisParser Plicity
122 endPlicity (Just _) = do lchar '}'
123 return impl
124 endPlicity Nothing = return expl
126 annotate :: SyntaxInfo -> IState -> Docstring () -> Docstring (Either Err PTerm)
127 annotate syn ist = annotCode $ tryFullExpr syn ist
129recordParameter :: SyntaxInfo -> IdrisParser (Name, FC, Plicity, PTerm)
130recordParameter syn =
131 (do lchar '('
132 (n, nfc, pt) <- (namedTy syn <|> onlyName syn)
133 lchar ')'
134 return (n, nfc, expl, pt))
135 <|>
136 (do (n, nfc, pt) <- onlyName syn
137 return (n, nfc, expl, pt))
138 where
139 namedTy :: SyntaxInfo -> IdrisParser (Name, FC, PTerm)
140 namedTy syn =
141 do (n, nfc) <- fnName
142 lchar ':'
143 ty <- typeExpr (allowImp syn)
144 return (expandNS syn n, nfc, ty)
145 onlyName :: SyntaxInfo -> IdrisParser (Name, FC, PTerm)
146 onlyName syn =
147 do (n, nfc) <- fnName
148 fc <- getFC
149 return (expandNS syn n, nfc, PType fc)
151{- | Parses data declaration type (normal or codata)
152DataI ::= 'data' | 'codata';
153-}
154dataI :: IdrisParser DataOpts
155dataI = do reservedHL "data"; return []
156 <|> do reservedHL "codata"; return [Codata]
158recordI :: IdrisParser DataOpts
159recordI = do reservedHL "record"; return []
160 <|> do reservedHL "corecord"; return [Codata]
162{- | Parses if a data should not have a default eliminator
163DefaultEliminator ::= 'noelim'?
164 -}
165dataOpts :: DataOpts -> IdrisParser DataOpts
166dataOpts opts
167 = do fc <- reservedFC "%elim"
168 warnElim fc
169 dataOpts (DefaultEliminator : DefaultCaseFun : opts)
170 <|> do fc <- reservedFC "%case"
171 warnElim fc
172 dataOpts (DefaultCaseFun : opts)
173 <|> do reserved "%error_reverse"; dataOpts (DataErrRev : opts)
174 <|> return opts
175 <?> "data options"
176 where warnElim fc =
177 parserWarning fc (Just NoElimDeprecationWarnings) (Msg "The 'class' keyword is deprecated. Use 'interface' instead.")
179{- | Parses a data type declaration
180Data ::= DocComment? Accessibility? DataI DefaultEliminator FnName TypeSig ExplicitTypeDataRest?
181 | DocComment? Accessibility? DataI DefaultEliminator FnName Name* DataRest?
182 ;
183Constructor' ::= Constructor KeepTerminator;
184ExplicitTypeDataRest ::= 'where' OpenBlock Constructor'* CloseBlock;
186DataRest ::= '=' SimpleConstructorList Terminator
187  | 'where'!
188 ;
189SimpleConstructorList ::=
190 SimpleConstructor
191 | SimpleConstructor '|' SimpleConstructorList
192 ;
193-}
194data_ :: SyntaxInfo -> IdrisParser PDecl
195data_ syn = checkDeclFixity $
196 do (doc, argDocs, acc, dataOpts) <- try (do
197 (doc, argDocs) <- option noDocs docComment
198 pushIndent
199 acc <- accessibility
200 elim <- dataOpts []
201 co <- dataI
202 ist <- get
203 let dataOpts = combineDataOpts (elim ++ co)
204 doc' = annotCode (tryFullExpr syn ist) doc
205 argDocs' = [ (n, annotCode (tryFullExpr syn ist) d)
206 | (n, d) <- argDocs ]
207 return (doc', argDocs', acc, dataOpts))
208 fc <- getFC
209 (tyn_in, nfc) <- fnName
210 (do try (lchar ':')
211 ty <- typeExpr (allowImp syn)
212 let tyn = expandNS syn tyn_in
213 d <- option (PData doc argDocs syn fc dataOpts (PLaterdecl tyn nfc ty)) (do
214 reservedHL "where"
215 cons <- indentedBlock (constructor syn)
216 accData acc tyn (map (\ (_, _, n, _, _, _, _) -> n) cons)
217 return $ PData doc argDocs syn fc dataOpts (PDatadecl tyn nfc ty cons))
218 terminator
219 return d) <|> (do
220 args <- many (do notEndApp
221 x <- fst <$> name
222 return x)
223 let ty = bindArgs (map (const (PType fc)) args) (PType fc)
224 let tyn = expandNS syn tyn_in
225 d <- option (PData doc argDocs syn fc dataOpts (PLaterdecl tyn nfc ty)) (do
226 try (lchar '=') <|> do reservedHL "where"
227 let kw = (if DefaultEliminator `elem` dataOpts then "%elim" else "") ++ (if Codata `elem` dataOpts then "co" else "") ++ "data "
228 let n = show tyn_in ++ " "
229 let s = kw ++ n
230 let as = unwords (map show args) ++ " "
231 let ns = concat (intersperse " -> " $ map ((\x -> "(" ++ x ++ " : Type)") . show) args)
232 let ss = concat (intersperse " -> " $ map (const "Type") args)
233 let fix1 = s ++ as ++ " = ..."
234 let fix2 = s ++ ": " ++ ns ++ " -> Type where\n ..."
235 let fix3 = s ++ ": " ++ ss ++ " -> Type where\n ..."
236 fail $ fixErrorMsg "unexpected \"where\"" [fix1, fix2, fix3]
237 cons <- sepBy1 (simpleConstructor (syn { withAppAllowed = False })) (reservedOp "|")
238 let conty = mkPApp fc (PRef fc [] tyn) (map (PRef fc []) args)
239 cons' <- mapM (\ (doc, argDocs, x, xfc, cargs, cfc, fs) ->
240 do let cty = bindArgs cargs conty
241 return (doc, argDocs, x, xfc, cty, cfc, fs)) cons
242 accData acc tyn (map (\ (_, _, n, _, _, _, _) -> n) cons')
243 return $ PData doc argDocs syn fc dataOpts (PDatadecl tyn nfc ty cons'))
244 terminator
245 return d)
246 <?> "data type declaration"
247 where
248 mkPApp :: FC -> PTerm -> [PTerm] -> PTerm
249 mkPApp fc t [] = t
250 mkPApp fc t xs = PApp fc t (map pexp xs)
251 bindArgs :: [PTerm] -> PTerm -> PTerm
252 bindArgs xs t = foldr (PPi expl (sMN 0 "_t") NoFC) t xs
253 combineDataOpts :: DataOpts -> DataOpts
254 combineDataOpts opts = if Codata `elem` opts
255 then delete DefaultEliminator opts
256 else opts
259{- | Parses a type constructor declaration
260 Constructor ::= DocComment? FnName TypeSig;
261-}
262constructor :: SyntaxInfo -> IdrisParser (Docstring (Either Err PTerm), [(Name, Docstring (Either Err PTerm))], Name, FC, PTerm, FC, [Name])
263constructor syn
264 = do (doc, argDocs) <- option noDocs docComment
265 (cn_in, nfc) <- fnName; fc <- getFC
266 let cn = expandNS syn cn_in
267 lchar ':'
268 fs <- option [] (do lchar '%'; reserved "erase"
269 sepBy1 (fst <$> name) (lchar ','))
270 ty <- typeExpr (allowImp syn)
271 ist <- get
272 let doc' = annotCode (tryFullExpr syn ist) doc
273 argDocs' = [ (n, annotCode (tryFullExpr syn ist) d)
274 | (n, d) <- argDocs ]
275 checkNameFixity cn
276 return (doc', argDocs', cn, nfc, ty, fc, fs)
277 <?> "constructor"
279{- | Parses a constructor for simple discriminated union data types
280 SimpleConstructor ::= FnName SimpleExpr* DocComment?
281-}
282simpleConstructor :: SyntaxInfo -> IdrisParser (Docstring (Either Err PTerm), [(Name, Docstring (Either Err PTerm))], Name, FC, [PTerm], FC, [Name])
283simpleConstructor syn
284 = do (doc, _) <- option noDocs (try docComment)
285 ist <- get
286 let doc' = annotCode (tryFullExpr syn ist) doc
287 (cn_in, nfc) <- fnName
288 let cn = expandNS syn cn_in
289 fc <- getFC
290 args <- many (do notEndApp
291 simpleExpr syn)
292 checkNameFixity cn
293 return (doc', [], cn, nfc, args, fc, [])
294 <?> "constructor"
296{- | Parses a dsl block declaration
297DSL ::= 'dsl' FnName OpenBlock Overload'+ CloseBlock;
298 -}
299dsl :: SyntaxInfo -> IdrisParser PDecl
300dsl syn = do reservedHL "dsl"
301 n <- fst <$> fnName
302 bs <- indentedBlock (overload syn)
303 let dsl = mkDSL bs (dsl_info syn)
304 checkDSL dsl
305 i <- get
306 put (i { idris_dsls = addDef n dsl (idris_dsls i) })
307 return (PDSL n dsl)
308 <?> "dsl block declaration"
309 where mkDSL :: [(String, PTerm)] -> DSL -> DSL
310 mkDSL bs dsl = let var = lookup "variable" bs
311 first = lookup "index_first" bs
312 next = lookup "index_next" bs
313 leto = lookup "let" bs
314 lambda = lookup "lambda" bs
315 pi = lookup "pi" bs in
316 initDSL { dsl_var = var,
317 index_first = first,
318 index_next = next,
319 dsl_lambda = lambda,
320 dsl_let = leto,
321 dsl_pi = pi }
323{- | Checks DSL for errors -}
324-- FIXME: currently does nothing, check if DSL is really sane
325--
326-- Issue #1595 on the Issue Tracker
327--
328-- https://github.com/idris-lang/Idris-dev/issues/1595
329--
330checkDSL :: DSL -> IdrisParser ()
331checkDSL dsl = return ()
333{- | Parses a DSL overload declaration
334OverloadIdentifier ::= 'let' | Identifier;
335Overload ::= OverloadIdentifier '=' Expr;
336-}
337overload :: SyntaxInfo -> IdrisParser (String, PTerm)
338overload syn = do (o, fc) <- identifier <|> do fc <- reservedFC "let"
339 return ("let", fc)
340 if o `notElem` overloadable
341 then fail $ show o ++ " is not an overloading"
342 else do
343 highlightP fc AnnKeyword
344 lchar '='
345 t <- expr syn
346 return (o, t)
347 <?> "dsl overload declaratioN"
348 where overloadable = ["let","lambda","pi","index_first","index_next","variable"]