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