git.iko.soy/Idris-dev
on master help sign in
Idris-dev/src/Idris/Elab/Type.hs
257 lines 10 kB history raw
1{-|
2Module : Idris.Elab.Type
3Description : Code to elaborate types.
5License : BSD3
6Maintainer : The Idris Community.
7-}
8{-# LANGUAGE PatternGuards #-}
9module Idris.Elab.Type (
10 buildType, elabType, elabType'
11 , elabPostulate, elabExtern
12 ) where
14import Idris.AbsSyntax
15import Idris.ASTUtils
16import Idris.Core.Elaborate hiding (Tactic(..))
17import Idris.Core.Evaluate
18import Idris.Core.TT
19import Idris.Docstrings (Docstring)
20import Idris.Elab.Term
21import Idris.Elab.Utils
22import Idris.Elab.Value
23import Idris.Error
24import Idris.Options
25import Idris.Output (sendHighlighting)
27import Prelude hiding (id, (.))
29import Control.Category
30import Control.Monad
31import qualified Data.Set as S
33buildType :: ElabInfo
34 -> SyntaxInfo
35 -> FC
36 -> FnOpts
37 -> Name
38 -> PTerm
39 -> Idris (Type, Type, PTerm, [(Int, Name)])
40buildType info syn fc opts n ty' = do
41 ctxt <- getContext
42 i <- getIState
44 logElab 2 $ show n ++ " pre-type " ++ showTmImpls ty' ++ show (no_imp syn)
45 ty' <- addUsingConstraints syn fc ty'
46 ty' <- addUsingImpls syn n fc ty'
47 let ty = addImpl (imp_methods syn) i ty'
49 logElab 5 $ show n ++ " type pre-addimpl " ++ showTmImpls ty'
50 logElab 5 $ "with methods " ++ show (imp_methods syn)
51 logElab 2 $ show n ++ " type " ++ show (using syn) ++ "\n" ++ showTmImpls ty
53 ((ElabResult tyT' defer is ctxt' newDecls highlights newGName, est), log) <-
54 tclift $ elaborate (constraintNS info) ctxt (idris_datatypes i) (idris_name i) n (TType (UVal 0)) initEState
55 (errAt "type of " n Nothing
56 (erunAux fc (build i info ETyDecl [] n ty)))
58 displayWarnings est
59 setContext ctxt'
60 processTacticDecls info newDecls
61 sendHighlighting highlights
62 updateIState $ \i -> i { idris_name = newGName }
64 let tyT = patToImp tyT'
66 logElab 3 $ show ty ++ "\nElaborated: " ++ show tyT'
68 ds <- checkAddDef True False info fc iderr True defer
69 -- if the type is not complete, note that we'll need to infer
70 -- things later (for solving metavariables)
71 when (length ds > length is) -- more deferred than case blocks
72 $ addTyInferred n
74 mapM_ (elabCaseBlock info opts) is
75 ctxt <- getContext
76 logElab 5 "Rechecking"
77 logElab 6 (show tyT)
78 logElab 10 $ "Elaborated to " ++ showEnvDbg [] tyT
79 (cty, ckind) <- recheckC (constraintNS info) fc id [] tyT
81 -- record the implicit and inaccessible arguments
82 i <- getIState
83 let (inaccData, impls) = unzip $ getUnboundImplicits i cty ty
84 let inacc = inaccessibleImps 0 cty inaccData
85 logElab 3 $ show n ++ ": inaccessible arguments: " ++ show inacc ++
86 " from " ++ show cty ++ "\n" ++ showTmImpls ty
88 putIState $ i { idris_implicits = addDef n impls (idris_implicits i) }
89 logElab 3 ("Implicit " ++ show n ++ " " ++ show impls)
90 addIBC (IBCImp n)
92 -- Add the names referenced to the call graph, and check we're not
93 -- referring to anything less visible
94 -- In particular, a public/export type can not refer to anything
95 -- private, but can refer to any public/export
96 let refs = freeNames cty
97 nvis <- getFromHideList n
98 case nvis of
99 Nothing -> return ()
100 Just acc -> mapM_ (checkVisibility fc n (max Frozen acc) acc) refs
101 addCalls n refs
102 addIBC (IBCCG n)
104 when (Constructor `notElem` opts) $ do
105 let pnames = getParamsInType i [] impls cty
106 let fninfo = FnInfo (param_pos 0 pnames cty)
107 setFnInfo n fninfo
108 addIBC (IBCFnInfo n fninfo)
110 return (cty, ckind, ty, inacc)
111 where
112 patToImp (Bind n (PVar rig t) sc) = Bind n (Pi rig Nothing t (TType (UVar [] 0))) (patToImp sc)
113 patToImp (Bind n b sc) = Bind n b (patToImp sc)
114 patToImp t = t
116 param_pos i ns (Bind n (Pi _ _ t _) sc)
117 | n `elem` ns = i : param_pos (i + 1) ns sc
118 | otherwise = param_pos (i + 1) ns sc
119 param_pos i ns t = []
121-- | Elaborate a top-level type declaration - for example, "foo : Int -> Int".
122elabType :: ElabInfo
123 -> SyntaxInfo
124 -> Docstring (Either Err PTerm)
125 -> [(Name, Docstring (Either Err PTerm))]
126 -> FC
127 -> FnOpts
128 -> Name
129 -> FC -- ^ The precise location of the name
130 -> PTerm
131 -> Idris Type
132elabType = elabType' False
134elabType' :: Bool -- normalise it
135 -> ElabInfo
136 -> SyntaxInfo
137 -> Docstring (Either Err PTerm)
138 -> [(Name, Docstring (Either Err PTerm))]
139 -> FC
140 -> FnOpts
141 -> Name
142 -> FC
143 -> PTerm
144 -> Idris Type
145elabType' norm info syn doc argDocs fc opts n nfc ty' = {- let ty' = piBind (params info) ty_in
146 n = liftname info n_in in -}
147 do checkUndefined fc n
148 (cty, _, ty, inacc) <- buildType info syn fc opts n ty'
150 addStatics n cty ty
151 let nty = cty -- normalise ctxt [] cty
152 -- if the return type is something coinductive, freeze the definition
153 ctxt <- getContext
154 logElab 2 $ "Rechecked to " ++ show nty
155 let nty' = normalise ctxt [] nty
156 logElab 2 $ "Rechecked to " ++ show nty'
158 -- Add function name to internals (used for making :addclause know
159 -- the name unambiguously)
160 i <- getIState
161 rep <- useREPL
162 when rep $ do
163 addInternalApp (fc_fname fc) (fst . fc_start $ fc) (PTyped (PRef fc [] n) ty') -- (mergeTy ty' (delab i nty')) -- TODO: Should use span instead of line and filename?
164 addIBC (IBCLineApp (fc_fname fc) (fst . fc_start $ fc) (PTyped (PRef fc [] n) ty')) -- (mergeTy ty' (delab i nty')))
166 let (fam, _) = unApply (getRetTy nty')
167 -- Productivity checking now via checking for guarded 'Delay'
168 let opts' = opts -- if corec then (Coinductive : opts) else opts
169 let usety = if norm then nty' else nty
170 ds <- checkDef info fc iderr True [(n, (-1, Nothing, usety, []))]
171 addIBC (IBCDef n)
172 addDefinedName n
173 let ds' = map (\(n, (i, top, fam, ns)) -> (n, (i, top, fam, ns, True, True))) ds
174 addDeferred ds'
175 setFlags n opts'
176 checkDocs fc argDocs ty
177 doc' <- elabDocTerms info doc
178 argDocs' <- mapM (\(n, d) -> do d' <- elabDocTerms info d
179 return (n, d')) argDocs
180 addDocStr n doc' argDocs'
181 addIBC (IBCDoc n)
182 addIBC (IBCFlags n)
183 fputState (opt_inaccessible . ist_optimisation n) inacc
184 addIBC (IBCOpt n)
185 when (Implicit `elem` opts') $ do addCoercion n
186 addIBC (IBCCoercion n)
187 when (AutoHint `elem` opts') $
188 case fam of
189 P _ tyn _ -> do addAutoHint tyn n
190 addIBC (IBCAutoHint tyn n)
191 t -> ifail "Hints must return a data or record type"
193 -- If the function is declared as an error handler and the language
194 -- extension is enabled, then add it to the list of error handlers.
195 errorReflection <- fmap (elem ErrorReflection . idris_language_extensions) getIState
196 when (ErrorHandler `elem` opts) $ do
197 if errorReflection
198 then
199 -- Check that the declared type is the correct type for an error handler:
200 -- handler : List (TTName, TT) -> Err -> ErrorReport - for now no ctxt
201 if tyIsHandler nty'
202 then do i <- getIState
203 putIState $ i { idris_errorhandlers = idris_errorhandlers i ++ [n] }
204 addIBC (IBCErrorHandler n)
205 else ifail $ "The type " ++ show nty' ++ " is invalid for an error handler"
206 else ifail "Error handlers can only be defined when the ErrorReflection language extension is enabled."
207 -- Send highlighting information about the name being declared
208 sendHighlighting $ S.fromList [(FC' nfc, AnnName n Nothing Nothing Nothing)]
209 -- if it's an export list type, make a note of it
210 case (unApply usety) of
211 (P _ ut _, _)
212 | ut == ffiexport -> do addIBC (IBCExport n)
213 addExport n
214 _ -> return ()
215 return usety
216 where
217 ffiexport = sNS (sUN "FFI_Export") ["FFI_Export"]
219 err = txt "Err"
220 maybe = txt "Maybe"
221 lst = txt "List"
222 errrep = txt "ErrorReportPart"
224 tyIsHandler (Bind _ (Pi _ _ (P _ (NS (UN e) ns1) _) _)
225 (App _ (P _ (NS (UN m) ns2) _)
226 (App _ (P _ (NS (UN l) ns3) _)
227 (P _ (NS (UN r) ns4) _))))
228 | e == err && m == maybe && l == lst && r == errrep
229 , ns1 == map txt ["Errors","Reflection","Language"]
230 , ns2 == map txt ["Maybe", "Prelude"]
231 , ns3 == map txt ["List", "Prelude"]
232 , ns4 == map txt ["Reflection","Language"] = True
233 tyIsHandler _ = False
235elabPostulate :: ElabInfo -> SyntaxInfo -> Docstring (Either Err PTerm) ->
236 FC -> FC -> FnOpts -> Name -> PTerm -> Idris ()
237elabPostulate info syn doc fc nfc opts n ty = do
238 elabType info syn doc [] fc opts n NoFC ty
239 putIState . (\ist -> ist{ idris_postulates = S.insert n (idris_postulates ist) }) =<< getIState
240 addIBC (IBCPostulate n)
241 sendHighlighting $ S.fromList [(FC' nfc, AnnName n (Just PostulateOutput) Nothing Nothing)]
243 -- remove it from the deferred definitions list
244 solveDeferred fc n
246elabExtern :: ElabInfo -> SyntaxInfo -> Docstring (Either Err PTerm) ->
247 FC -> FC -> FnOpts -> Name -> PTerm -> Idris ()
248elabExtern info syn doc fc nfc opts n ty = do
249 cty <- elabType info syn doc [] fc opts n NoFC ty
250 ist <- getIState
251 let arity = length (getArgTys (normalise (tt_ctxt ist) [] cty))
253 putIState . (\ist -> ist{ idris_externs = S.insert (n, arity) (idris_externs ist) }) =<< getIState
254 addIBC (IBCExtern (n, arity))
256 -- remove it from the deferred definitions list
257 solveDeferred fc n