git.iko.soy/Idris-dev
on bf4e535 help sign in
Idris-dev/src/Idris/ParseData.hs
258 lines 11 kB history raw
1{-# LANGUAGE GeneralizedNewtypeDeriving, ConstraintKinds, PatternGuards #-}
2module Idris.ParseData 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.ParseHelpers
16import Idris.ParseOps
17import Idris.ParseExpr
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, argDocs, acc, opts) <- try (do
46 (doc, argDocs) <- option noDocs docComment
47 ist <- get
48 let doc' = annotCode (tryFullExpr syn ist) doc
49 argDocs' = [ (n, annotCode (tryFullExpr syn ist) d)
50 | (n, d) <- argDocs ]
51 acc <- optional accessibility
52 opts <- dataOpts []
53 reserved "record"
54 return (doc', argDocs', acc, opts))
55 fc <- getFC
56 tyn_in <- fnName
57 lchar ':'
58 ty <- typeExpr (allowImp syn)
59 let tyn = expandNS syn tyn_in
60 reserved "where"
61 (cdoc, cargDocs, cn, cty, _, _) <- indentedBlockS (constructor syn)
62 accData acc tyn [cn]
63 let rsyn = syn { syn_namespace = show (nsroot tyn) :
64 syn_namespace syn }
65 let fns = getRecNames rsyn cty
66 mapM_ (\n -> addAcc n acc) fns
67 return $ PRecord doc rsyn fc tyn ty opts cdoc cn cty
68 <?> "record type declaration"
69 where
70 getRecNames :: SyntaxInfo -> PTerm -> [Name]
71 getRecNames syn (PPi _ n _ sc) = [expandNS syn n, expandNS syn (mkType n)]
72 ++ getRecNames syn sc
73 getRecNames _ _ = []
75 toFreeze :: Maybe Accessibility -> Maybe Accessibility
76 toFreeze (Just Frozen) = Just Hidden
77 toFreeze x = x
79{- | Parses data declaration type (normal or codata)
80DataI ::= 'data' | 'codata';
81-}
82dataI :: IdrisParser DataOpts
83dataI = do reserved "data"; return []
84 <|> do reserved "codata"; return [Codata]
86{- | Parses if a data should not have a default eliminator
87DefaultEliminator ::= 'noelim'?
88 -}
89dataOpts :: DataOpts -> IdrisParser DataOpts
90dataOpts opts
91 = do reserved "%elim"; dataOpts (DefaultEliminator : DefaultCaseFun : opts)
92 <|> do reserved "%case"; dataOpts (DefaultCaseFun : opts)
93 <|> do reserved "%error_reverse"; dataOpts (DataErrRev : opts)
94 <|> return opts
95 <?> "data options"
97{- | Parses a data type declaration
98Data ::= DocComment? Accessibility? DataI DefaultEliminator FnName TypeSig ExplicitTypeDataRest?
99 | DocComment? Accessibility? DataI DefaultEliminator FnName Name* DataRest?
100 ;
101Constructor' ::= Constructor KeepTerminator;
102ExplicitTypeDataRest ::= 'where' OpenBlock Constructor'* CloseBlock;
104DataRest ::= '=' SimpleConstructorList Terminator
105  | 'where'!
106 ;
107SimpleConstructorList ::=
108 SimpleConstructor
109 | SimpleConstructor '|' SimpleConstructorList
110 ;
111-}
112data_ :: SyntaxInfo -> IdrisParser PDecl
113data_ syn = do (doc, argDocs, acc, dataOpts) <- try (do
114 (doc, argDocs) <- option noDocs docComment
115 pushIndent
116 acc <- optional accessibility
117 elim <- dataOpts []
118 co <- dataI
119 ist <- get
120 let dataOpts = combineDataOpts (elim ++ co)
121 doc' = annotCode (tryFullExpr syn ist) doc
122 argDocs' = [ (n, annotCode (tryFullExpr syn ist) d)
123 | (n, d) <- argDocs ]
124 return (doc', argDocs', acc, dataOpts))
125 fc <- getFC
126 tyn_in <- fnName
127 (do try (lchar ':')
128 popIndent
129 ty <- typeExpr (allowImp syn)
130 let tyn = expandNS syn tyn_in
131 option (PData doc argDocs syn fc dataOpts (PLaterdecl tyn ty)) (do
132 reserved "where"
133 cons <- indentedBlock (constructor syn)
134 accData acc tyn (map (\ (_, _, n, _, _, _) -> n) cons)
135 return $ PData doc argDocs syn fc dataOpts (PDatadecl tyn ty cons))) <|> (do
136 args <- many name
137 let ty = bindArgs (map (const PType) args) PType
138 let tyn = expandNS syn tyn_in
139 option (PData doc argDocs syn fc dataOpts (PLaterdecl tyn ty)) (do
140 try (lchar '=') <|> do reserved "where"
141 let kw = (if DefaultEliminator `elem` dataOpts then "%elim" else "") ++ (if Codata `elem` dataOpts then "co" else "") ++ "data "
142 let n = show tyn_in ++ " "
143 let s = kw ++ n
144 let as = concat (intersperse " " $ map show args) ++ " "
145 let ns = concat (intersperse " -> " $ map ((\x -> "(" ++ x ++ " : Type)") . show) args)
146 let ss = concat (intersperse " -> " $ map (const "Type") args)
147 let fix1 = s ++ as ++ " = ..."
148 let fix2 = s ++ ": " ++ ns ++ " -> Type where\n ..."
149 let fix3 = s ++ ": " ++ ss ++ " -> Type where\n ..."
150 fail $ fixErrorMsg "unexpected \"where\"" [fix1, fix2, fix3]
151 cons <- sepBy1 (simpleConstructor syn) (reservedOp "|")
152 terminator
153 let conty = mkPApp fc (PRef fc tyn) (map (PRef fc) args)
154 cons' <- mapM (\ (doc, argDocs, x, cargs, cfc, fs) ->
155 do let cty = bindArgs cargs conty
156 return (doc, argDocs, x, cty, cfc, fs)) cons
157 accData acc tyn (map (\ (_, _, n, _, _, _) -> n) cons')
158 return $ PData doc argDocs syn fc dataOpts (PDatadecl tyn ty cons')))
159 <?> "data type declaration"
160 where
161 mkPApp :: FC -> PTerm -> [PTerm] -> PTerm
162 mkPApp fc t [] = t
163 mkPApp fc t xs = PApp fc t (map pexp xs)
164 bindArgs :: [PTerm] -> PTerm -> PTerm
165 bindArgs xs t = foldr (PPi expl (sMN 0 "_t")) t xs
166 combineDataOpts :: DataOpts -> DataOpts
167 combineDataOpts opts = if Codata `elem` opts
168 then delete DefaultEliminator opts
169 else opts
172{- | Parses a type constructor declaration
173 Constructor ::= DocComment? FnName TypeSig;
174-}
175constructor :: SyntaxInfo -> IdrisParser (Docstring (Either Err PTerm), [(Name, Docstring (Either Err PTerm))], Name, PTerm, FC, [Name])
176constructor syn
177 = do (doc, argDocs) <- option noDocs docComment
178 cn_in <- fnName; fc <- getFC
179 let cn = expandNS syn cn_in
180 lchar ':'
181 fs <- option [] (do lchar '%'; reserved "erase"
182 sepBy1 name (lchar ','))
183 ty <- typeExpr (allowImp syn)
184 ist <- get
185 let doc' = annotCode (tryFullExpr syn ist) doc
186 argDocs' = [ (n, annotCode (tryFullExpr syn ist) d)
187 | (n, d) <- argDocs ]
188 return (doc', argDocs', cn, ty, fc, fs)
189 <?> "constructor"
191{- | Parses a constructor for simple discriminated union data types
192 SimpleConstructor ::= FnName SimpleExpr* DocComment?
193-}
194simpleConstructor :: SyntaxInfo -> IdrisParser (Docstring (Either Err PTerm), [(Name, Docstring (Either Err PTerm))], Name, [PTerm], FC, [Name])
195simpleConstructor syn
196 = do (doc, _) <- option noDocs (try docComment)
197 ist <- get
198 let doc' = annotCode (tryFullExpr syn ist) doc
199 cn_in <- fnName
200 let cn = expandNS syn cn_in
201 fc <- getFC
202 args <- many (do notEndApp
203 simpleExpr syn)
204 return (doc', [], cn, args, fc, [])
205 <?> "constructor"
207{- | Parses a dsl block declaration
208DSL ::= 'dsl' FnName OpenBlock Overload'+ CloseBlock;
209 -}
210dsl :: SyntaxInfo -> IdrisParser PDecl
211dsl syn = do reserved "dsl"
212 n <- fnName
213 bs <- indentedBlock (overload syn)
214 let dsl = mkDSL bs (dsl_info syn)
215 checkDSL dsl
216 i <- get
217 put (i { idris_dsls = addDef n dsl (idris_dsls i) })
218 return (PDSL n dsl)
219 <?> "dsl block declaration"
220 where mkDSL :: [(String, PTerm)] -> DSL -> DSL
221 mkDSL bs dsl = let var = lookup "variable" bs
222 first = lookup "index_first" bs
223 next = lookup "index_next" bs
224 leto = lookup "let" bs
225 lambda = lookup "lambda" bs
226 pi = lookup "pi" bs in
227 initDSL { dsl_var = var,
228 index_first = first,
229 index_next = next,
230 dsl_lambda = lambda,
231 dsl_let = leto,
232 dsl_pi = pi }
234{- | Checks DSL for errors -}
235-- FIXME: currently does nothing, check if DSL is really sane
236--
237-- Issue #1595 on the Issue Tracker
238--
239-- https://github.com/idris-lang/Idris-dev/issues/1595
240--
241checkDSL :: DSL -> IdrisParser ()
242checkDSL dsl = return ()
244{- | Parses a DSL overload declaration
245OverloadIdentifier ::= 'let' | Identifier;
246Overload ::= OverloadIdentifier '=' Expr;
247-}
248overload :: SyntaxInfo -> IdrisParser (String, PTerm)
249overload syn = do o <- identifier <|> do reserved "let"
250 return "let"
251 if o `notElem` overloadable
252 then fail $ show o ++ " is not an overloading"
253 else do
254 lchar '='
255 t <- expr syn
256 return (o, t)
257 <?> "dsl overload declaratioN"
258 where overloadable = ["let","lambda","pi","index_first","index_next","variable"]