git.iko.soy/Idris-dev
on master help sign in
Idris-dev/src/Idris/Elab/Data.hs
313 lines 13 kB history raw
1{-|
2Module : Idris.Elab.Data
3Description : Code to elaborate data structures.
5License : BSD3
6Maintainer : The Idris Community.
7-}
8{-# LANGUAGE CPP, PatternGuards #-}
9module Idris.Elab.Data(elabData) where
11import Idris.AbsSyntax
12import Idris.ASTUtils
13import Idris.Core.Evaluate
14import Idris.Core.TT
15import Idris.Core.Typecheck
16import Idris.Delaborate
17import Idris.Docstrings
18import Idris.Elab.Rewrite
19import Idris.Elab.Type
20import Idris.Elab.Utils
21import Idris.Elab.Value
22import Idris.Error
23import Idris.Output (iWarn, sendHighlighting)
25import Util.Pretty
27#if (MIN_VERSION_base(4,11,0))
28import Prelude hiding (id, (.), (<>))
29#else
30import Prelude hiding (id, (.))
31#endif
33import Control.Category
34import Control.Monad
35import Control.Monad.State.Strict as State
36import Data.Char (isLetter, toLower)
37import Data.List
38import qualified Data.Map as Map
39import Data.Maybe
40import qualified Data.Set as S
41import qualified Data.Text as T
43warnLC :: FC -> Name -> Idris ()
44warnLC fc n
45 = iWarn fc $ annName n <+> text "has a name which may be implicitly bound."
46 <> line <> text "This is likely to lead to problems!"
48elabData :: ElabInfo -> SyntaxInfo -> Docstring (Either Err PTerm)-> [(Name, Docstring (Either Err PTerm))] -> FC -> DataOpts -> PData -> Idris ()
49elabData info syn doc argDocs fc opts (PLaterdecl n nfc t_in)
50 = do logElab 1 (show (fc, doc))
51 checkUndefined fc n
52 when (implicitable (nsroot n)) $ warnLC fc n
53 (cty, _, t, inacc) <- buildType info syn fc [] n t_in
55 addIBC (IBCDef n)
56 updateContext (addTyDecl n (TCon 0 0) cty) -- temporary, to check cons
57 sendHighlighting $ S.fromList [(FC' nfc, AnnName n Nothing Nothing Nothing)]
59elabData info syn doc argDocs fc opts (PDatadecl n nfc t_in dcons)
60 = do let codata = Codata `elem` opts
61 logElab 1 (show fc)
62 undef <- isUndefined fc n
63 when (implicitable (nsroot n)) $ warnLC fc n
64 (cty, ckind, t, inacc) <- buildType info syn fc [] n t_in
65 -- if n is defined already, make sure it is just a type declaration
66 -- with the same type we've just elaborated, and no constructors
67 -- yet
68 i <- getIState
69 checkDefinedAs fc n cty i
70 -- temporary, to check cons
71 when undef $ updateContext (addTyDecl n (TCon 0 0) cty)
72 let cnameinfo = cinfo info (map cname dcons)
73 unique <- case getRetTy (normalise (tt_ctxt i) [] cty) of
74 UType UniqueType -> return True
75 UType _ -> return False
76 TType _ -> return False
77 rt -> tclift $ tfail (At fc (Elaborating "type constructor " n Nothing (Msg "Not a valid type constructor")))
78 cons <- mapM (elabCon cnameinfo syn n codata (getRetTy cty) ckind) dcons
79 ttag <- getName
81 ctxt <- getContext
82 let params = findParams n (normalise ctxt [] cty) (map snd cons)
84 logElab 2 $ "Parameters : " ++ show params
85 addParamConstraints fc params cty cons
87 i <- getIState
88 -- TI contains information about mutually declared types - this will
89 -- be updated when the mutual block is complete
90 putIState (i { idris_datatypes =
91 addDef n (TI (map fst cons) codata opts params [n]
92 (any linearArg (map snd cons)))
93 (idris_datatypes i) })
94 addIBC (IBCDef n)
95 addIBC (IBCData n)
96 checkDocs fc argDocs t
97 doc' <- elabDocTerms info doc
98 argDocs' <- mapM (\(n, d) -> do d' <- elabDocTerms info d
99 return (n, d')) argDocs
100 addDocStr n doc' argDocs'
101 addIBC (IBCDoc n)
102 let metainf = DataMI params
103 addIBC (IBCMetaInformation n metainf)
104 -- TMP HACK! Make this a data option
105 updateContext (addDatatype (Data n ttag cty unique cons))
106 updateContext (setMetaInformation n metainf)
108 mapM_ totcheck (zip (repeat fc) (map fst cons))
109-- mapM_ (checkPositive n) cons
111 -- if there's exactly one constructor,
112 -- mark both the type and the constructor as detaggable
113 case cons of
114 [(cn,ct)] -> setDetaggable cn >> setDetaggable n
115 >> addIBC (IBCOpt cn) >> addIBC (IBCOpt n)
116 _ -> return ()
118 -- create a rewriting lemma
119 when (n /= sUN "=") $
120 elabRewriteLemma info n cty
121 -- Emit highlighting info
122 sendHighlighting $ S.fromList $ [(FC' nfc, AnnName n Nothing Nothing Nothing)] ++
123 map (\(_, _, n, nfc, _, _, _) ->
124 (FC' nfc, AnnName n Nothing Nothing Nothing))
125 dcons
126 where
127 checkDefinedAs fc n t i
128 = let defined = tclift $ tfail (At fc (AlreadyDefined n))
129 ctxt = tt_ctxt i in
130 case lookupDef n ctxt of
131 [] -> return ()
132 [TyDecl _ ty] ->
133 case converts ctxt [] t ty of
134 OK () -> case lookupCtxtExact n (idris_datatypes i) of
135 Nothing -> return ()
136 _ -> defined
137 _ -> defined
138 _ -> defined
141 cname (_, _, n, _, _, _, _) = n
143 -- Abuse of ElabInfo.
144 -- TODO Contemplate whether the ElabInfo type needs modification.
145 cinfo :: ElabInfo -> [Name] -> ElabInfo
146 cinfo info ds
147 = let newps = params info
148 dsParams = map (\n -> (n, [])) ds
149 newb = addAlist dsParams (inblock info) in
150 info { params = newps,
151 inblock = newb,
152 liftname = id -- Is this appropriate?
153 }
155elabCon :: ElabInfo -> SyntaxInfo -> Name -> Bool ->
156 Type -> -- for unique kind checking
157 Type -> -- data type's kind
158 (Docstring (Either Err PTerm), [(Name, Docstring (Either Err PTerm))], Name, FC, PTerm, FC, [Name]) ->
159 Idris (Name, Type)
160elabCon info syn tn codata expkind dkind (doc, argDocs, n, nfc, t_in, fc, forcenames)
161 = do checkUndefined fc n
162 when (implicitable (nsroot n)) $ warnLC fc n
163 logElab 2 $ show fc ++ ":Constructor " ++ show n ++ " : " ++ show t_in
164 (cty, ckind, t, inacc) <- buildType info syn fc [Constructor] n (if codata then mkLazy t_in else t_in)
165 ctxt <- getContext
166 let cty' = normalise ctxt [] cty
167 checkUniqueKind ckind expkind
169 -- Check that the constructor type is, in fact, a part of the family being defined
170 tyIs n cty'
171 -- Need to calculate forceability from the non-normalised type,
172 -- because we might not be able to export the definitions which
173 -- we're normalising which changes the forceability status!
174 let force = if tn == sUN "Delayed"
175 then [] -- TMP HACK! Totality checker needs this info
176 else forceArgs ctxt tn cty
178 logElab 5 $ show fc ++ ":Constructor " ++ show n ++ " elaborated : " ++ show t
179 logElab 5 $ "Inaccessible args: " ++ show inacc
180 logElab 5 $ "Forceable args: " ++ show force
181 logElab 2 $ "---> " ++ show n ++ " : " ++ show cty
183 -- Add to the context (this is temporary, so that later constructors
184 -- can be indexed by it)
185 updateContext (addTyDecl n (DCon 0 0 False) cty)
187 addIBC (IBCDef n)
188 checkDocs fc argDocs t
189 doc' <- elabDocTerms info doc
190 argDocs' <- mapM (\(n, d) -> do d' <- elabDocTerms info d
191 return (n, d')) argDocs
192 addDocStr n doc' argDocs'
193 addIBC (IBCDoc n)
194 fputState (opt_inaccessible . ist_optimisation n) inacc
195 fputState (opt_forceable . ist_optimisation n) force
196 addIBC (IBCOpt n)
197 return (n, cty)
198 where
199 tyIs con (Bind n b sc) = tyIs con (substV (P Bound n Erased) sc)
200 tyIs con t | (P Bound n' _, _) <- unApply t
201 = if n' /= tn then
202 tclift $ tfail (At fc (Elaborating "constructor " con Nothing
203 (Msg ("Type level variable " ++ show n' ++ " is not " ++ show tn))))
204 else return ()
205 tyIs con t | (P _ n' _, _) <- unApply t
206 = if n' /= tn then tclift $ tfail (At fc (Elaborating "constructor " con Nothing (Msg (show n' ++ " is not " ++ show tn))))
207 else return ()
208 tyIs con t = tclift $ tfail (At fc (Elaborating "constructor " con Nothing (Msg (show t ++ " is not " ++ show tn))))
210 mkLazy (PPi pl n nfc ty sc)
211 = let ty' = if getTyName ty
212 then PApp fc (PRef fc [] (sUN "Delayed"))
213 [pexp (PRef fc [] (sUN "Infinite")),
214 pexp ty]
215 else ty in
216 PPi pl n nfc ty' (mkLazy sc)
217 mkLazy t = t
219 getTyName (PApp _ (PRef _ _ n) _) = n == nsroot tn
220 getTyName (PRef _ _ n) = n == nsroot tn
221 getTyName _ = False
223 -- if the constructor is a UniqueType, the datatype must be too
224 -- (AnyType is fine, since that is checked for uniqueness too)
225 -- if hte contructor is AnyType, the datatype must be at least AnyType
226 checkUniqueKind (UType NullType) (UType NullType) = return ()
227 checkUniqueKind (UType NullType) _
228 = tclift $ tfail (At fc (UniqueKindError NullType n))
229 checkUniqueKind (UType UniqueType) (UType UniqueType) = return ()
230 checkUniqueKind (UType UniqueType) (UType AllTypes) = return ()
231 checkUniqueKind (UType UniqueType) _
232 = tclift $ tfail (At fc (UniqueKindError UniqueType n))
233 checkUniqueKind (UType AllTypes) (UType AllTypes) = return ()
234 checkUniqueKind (UType AllTypes) (UType UniqueType) = return ()
235 checkUniqueKind (UType AllTypes) _
236 = tclift $ tfail (At fc (UniqueKindError AllTypes n))
237 checkUniqueKind _ _ = return ()
239forceArgs :: Context -> Name -> Type -> [Int]
240forceArgs ctxt tn ty = forceFrom 0 ty
241 where
242 -- for each argument, substitute in MN pos "FF"
243 -- then when we look at the return type, if we see MN pos name
244 -- constructor guarded, then 'pos' is a forceable position
245 forceFrom :: Int -> Type -> [Int]
246 forceFrom i (Bind n (Pi _ _ _ _) sc)
247 = forceFrom (i + 1) (substV (P Ref (sMN i "FF") Erased) sc)
248 forceFrom i sc
249 -- Go under the top level type application
250 -- We risk affecting erasure of more complex indices, so we'll only
251 -- mark something forced if *everything* which appears in an index
252 -- is forceable
253 -- (FIXME: Actually the real risk is if we erase something a programmer
254 -- definitely wants, which is particularly the case with 'views'.
255 -- So perhaps we need a way of marking that in the source?)
256 | (P _ ty _, args) <- unApply sc,
257 ty == tn -- Must be the right top level type!
258 = if null (concatMap (findNonForcePos True) args)
259 then nub (concatMap findForcePos args)
260 else []
261 forceFrom i sc = []
263 findForcePos (P _ (MN i ff) _)
264 | ff == txt "FF" = [i]
265 -- Only look under constructors in applications
266 findForcePos ap@(App _ f a)
267 | (P _ con _, args) <- unApply ap,
268 isDConName con ctxt
269 = nub $ concatMap findForcePos args
270 findForcePos _ = []
272 findNonForcePos fok (P _ (MN i ff) _)
273 | ff == txt "FF" = if fok then [] else [i]
274 -- Look under non-constructors in applications for things which can't
275 -- be forced
276 findNonForcePos fok ap@(App _ f a)
277 | (P _ con _, args) <- unApply ap
278 = nub $ concatMap (findNonForcePos (fok && isConName con ctxt)) args
279 findNonForcePos _ _ = []
281addParamConstraints :: FC -> [Int] -> Type -> [(Name, Type)] -> Idris ()
282addParamConstraints fc ps cty cons
283 = case getRetTy cty of
284 TType cvar -> mapM_ (addConConstraint ps cvar)
285 (map getParamNames cons)
286 _ -> return ()
287 where
288 getParamNames (n, ty) = (ty, getPs ty)
290 getPs (Bind n (Pi _ _ _ _) sc)
291 = getPs (substV (P Ref n Erased) sc)
292 getPs t | (f, args) <- unApply t
293 = paramArgs 0 args
295 paramArgs i (P _ n _ : args) | i `elem` ps = n : paramArgs (i + 1) args
296 paramArgs i (_ : args) = paramArgs (i + 1) args
297 paramArgs i [] = []
299 addConConstraint ps cvar (ty, pnames) = constraintTy ty
300 where
301 constraintTy (Bind n (Pi _ _ ty _) sc)
302 = case getRetTy ty of
303 TType avar -> do tit <- typeInType
304 when (not tit) $ do
305 ctxt <- getContext
306 let tv = next_tvar ctxt
307 let con = if n `elem` pnames
308 then ULE avar cvar
309 else ULT avar cvar
310 addConstraints fc (tv, [con])
311 addIBC (IBCConstraint fc con)
312 _ -> return ()
313 constraintTy t = return ()