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