git.iko.soy/Idris-dev
on bf4e535 help sign in
Idris-dev/src/Idris/Elab/Type.hs
252 lines 10 kB history raw
1{-# LANGUAGE PatternGuards #-}
2module Idris.Elab.Type (buildType, elabType, elabType',
3 elabPostulate, elabExtern) where
5import Idris.AbsSyntax
6import Idris.ASTUtils
7import Idris.DSL
8import Idris.Error
9import Idris.Delaborate
10import Idris.Imports
11import Idris.ElabTerm
12import Idris.Coverage
13import Idris.DataOpts
14import Idris.Providers
15import Idris.Primitives
16import Idris.Inliner
17import Idris.PartialEval
18import Idris.DeepSeq
19import Idris.Output (iputStrLn, pshow, iWarn)
20import IRTS.Lang
22import Idris.Elab.Utils
23import Idris.Elab.Value
25import Idris.Core.TT
26import Idris.Core.Elaborate hiding (Tactic(..))
27import Idris.Core.Evaluate
28import Idris.Core.Execute
29import Idris.Core.Typecheck
30import Idris.Core.CaseTree
32import Idris.Docstrings (Docstring)
34import Prelude hiding (id, (.))
35import Control.Category
37import Control.Applicative hiding (Const)
38import Control.DeepSeq
39import Control.Monad
40import Control.Monad.State.Strict as State
41import Data.List
42import Data.Maybe
43import Debug.Trace
45import qualified Data.Traversable as Traversable
47import qualified Data.Map as Map
48import qualified Data.Set as S
49import qualified Data.Text as T
50import Data.Char(isLetter, toLower)
51import Data.List.Split (splitOn)
53import Util.Pretty(pretty, text)
55buildType :: ElabInfo -> SyntaxInfo -> FC -> FnOpts -> Name -> PTerm ->
56 Idris (Type, Type, PTerm, [(Int, Name)])
57buildType info syn fc opts n ty' = do
58 ctxt <- getContext
59 i <- getIState
61 logLvl 2 $ show n ++ " pre-type " ++ showTmImpls ty' ++ show (no_imp syn)
62 ty' <- addUsingConstraints syn fc ty'
63 ty' <- addUsingImpls syn n fc ty'
64 let ty = addImpl (imp_methods syn) i ty'
66 logLvl 5 $ show n ++ " type pre-addimpl " ++ showTmImpls ty'
67 logLvl 2 $ show n ++ " type " ++ show (using syn) ++ "\n" ++ showTmImpls ty
69 (ElabResult tyT' defer is ctxt' newDecls, log) <-
70 tclift $ elaborate ctxt n (TType (UVal 0)) initEState
71 (errAt "type of " n (erun fc (build i info ETyDecl [] n ty)))
72 setContext ctxt'
73 processTacticDecls newDecls
75 let tyT = patToImp tyT'
77 logLvl 3 $ show ty ++ "\nElaborated: " ++ show tyT'
79 ds <- checkAddDef True False fc iderr defer
80 -- if the type is not complete, note that we'll need to infer
81 -- things later (for solving metavariables)
82 when (not (null ds)) $ addTyInferred n
84 mapM_ (elabCaseBlock info opts) is
85 ctxt <- getContext
86 logLvl 5 $ "Rechecking"
87 logLvl 6 $ show tyT
88 logLvl 10 $ "Elaborated to " ++ showEnvDbg [] tyT
89 (cty, ckind) <- recheckC fc id [] tyT
91 -- record the implicit and inaccessible arguments
92 i <- getIState
93 let (inaccData, impls) = unzip $ getUnboundImplicits i cty ty
94 let inacc = inaccessibleImps 0 cty inaccData
95 logLvl 3 $ show n ++ ": inaccessible arguments: " ++ show inacc ++
96 " from " ++ show cty ++ "\n" ++ showTmImpls ty
98 putIState $ i { idris_implicits = addDef n impls (idris_implicits i) }
99 logLvl 3 ("Implicit " ++ show n ++ " " ++ show impls)
100 addIBC (IBCImp n)
102 when (Constructor `notElem` opts) $ do
103 let pnames = getParamsInType i [] impls cty
104 let fninfo = FnInfo (param_pos 0 pnames cty)
105 setFnInfo n fninfo
106 addIBC (IBCFnInfo n fninfo)
108 return (cty, ckind, ty, inacc)
109 where
110 patToImp (Bind n (PVar t) sc) = Bind n (Pi Nothing t (TType (UVar 0))) (patToImp sc)
111 patToImp (Bind n b sc) = Bind n b (patToImp sc)
112 patToImp t = t
114 param_pos i ns (Bind n (Pi _ t _) sc)
115 | n `elem` ns = i : param_pos (i + 1) ns sc
116 | otherwise = param_pos (i + 1) ns sc
117 param_pos i ns t = []
119-- | Elaborate a top-level type declaration - for example, "foo : Int -> Int".
120elabType :: ElabInfo -> SyntaxInfo
121 -> Docstring (Either Err PTerm) -> [(Name, Docstring (Either Err PTerm))]
122 -> FC -> FnOpts -> Name -> PTerm -> Idris Type
123elabType = elabType' False
125elabType' :: Bool -> -- normalise it
126 ElabInfo -> SyntaxInfo ->
127 Docstring (Either Err PTerm) -> [(Name, Docstring (Either Err PTerm))] ->
128 FC -> FnOpts -> Name -> PTerm -> Idris Type
129elabType' norm info syn doc argDocs fc opts n ty' = {- let ty' = piBind (params info) ty_in
130 n = liftname info n_in in -}
131 do checkUndefined fc n
132 (cty, _, ty, inacc) <- buildType info syn fc opts n ty'
134 addStatics n cty ty
135 let nty = cty -- normalise ctxt [] cty
136 -- if the return type is something coinductive, freeze the definition
137 ctxt <- getContext
138 logLvl 2 $ "Rechecked to " ++ show nty
139 let nty' = normalise ctxt [] nty
140 logLvl 2 $ "Rechecked to " ++ show nty'
142 -- Add normalised type to internals
143 i <- getIState
144 rep <- useREPL
145 when rep $ do
146 addInternalApp (fc_fname fc) (fst . fc_start $ fc) ty' -- (mergeTy ty' (delab i nty')) -- TODO: Should use span instead of line and filename?
147 addIBC (IBCLineApp (fc_fname fc) (fst . fc_start $ fc) ty') -- (mergeTy ty' (delab i nty')))
149 let (fam, _) = unApply (getRetTy nty')
150 let corec = case fam of
151 P _ rcty _ -> case lookupCtxt rcty (idris_datatypes i) of
152 [TI _ True _ _ _] -> True
153 _ -> False
154 _ -> False
155 -- Productivity checking now via checking for guarded 'Delay'
156 let opts' = opts -- if corec then (Coinductive : opts) else opts
157 let usety = if norm then nty' else nty
158 ds <- checkDef fc iderr [(n, (-1, Nothing, usety))]
159 addIBC (IBCDef n)
160 let ds' = map (\(n, (i, top, fam)) -> (n, (i, top, fam, True))) ds
161 addDeferred ds'
162 setFlags n opts'
163 checkDocs fc argDocs ty
164 doc' <- elabDocTerms info doc
165 argDocs' <- mapM (\(n, d) -> do d' <- elabDocTerms info d
166 return (n, d')) argDocs
167 addDocStr n doc' argDocs'
168 addIBC (IBCDoc n)
169 addIBC (IBCFlags n opts')
170 fputState (opt_inaccessible . ist_optimisation n) inacc
171 addIBC (IBCOpt n)
172 when (Implicit `elem` opts') $ do addCoercion n
173 addIBC (IBCCoercion n)
174 when (AutoHint `elem` opts') $
175 case fam of
176 P _ tyn _ -> do addAutoHint tyn n
177 addIBC (IBCAutoHint tyn n)
178 t -> ifail $ "Hints must return a data or record type"
180 -- If the function is declared as an error handler and the language
181 -- extension is enabled, then add it to the list of error handlers.
182 errorReflection <- fmap (elem ErrorReflection . idris_language_extensions) getIState
183 when (ErrorHandler `elem` opts) $ do
184 if errorReflection
185 then
186 -- Check that the declared type is the correct type for an error handler:
187 -- handler : List (TTName, TT) -> Err -> ErrorReport - for now no ctxt
188 if tyIsHandler nty'
189 then do i <- getIState
190 putIState $ i { idris_errorhandlers = idris_errorhandlers i ++ [n] }
191 addIBC (IBCErrorHandler n)
192 else ifail $ "The type " ++ show nty' ++ " is invalid for an error handler"
193 else ifail "Error handlers can only be defined when the ErrorReflection language extension is enabled."
194 -- if it's an export list type, make a note of it
195 case (unApply usety) of
196 (P _ ut _, _)
197 | ut == ffiexport -> do addIBC (IBCExport n)
198 addExport n
199 _ -> return ()
200 return usety
201 where
202 -- for making an internalapp, we only want the explicit ones, and don't
203 -- want the parameters, so just take the arguments which correspond to the
204 -- user declared explicit ones
205 mergeTy (PPi e n ty sc) (PPi e' n' _ sc')
206 | e == e' = PPi e n ty (mergeTy sc sc')
207 | otherwise = mergeTy sc sc'
208 mergeTy _ sc = sc
210 ffiexport = sNS (sUN "FFI_Export") ["FFI_Export"]
212 err = txt "Err"
213 maybe = txt "Maybe"
214 lst = txt "List"
215 errrep = txt "ErrorReportPart"
217 tyIsHandler (Bind _ (Pi _ (P _ (NS (UN e) ns1) _) _)
218 (App (P _ (NS (UN m) ns2) _)
219 (App (P _ (NS (UN l) ns3) _)
220 (P _ (NS (UN r) ns4) _))))
221 | e == err && m == maybe && l == lst && r == errrep
222 , ns1 == map txt ["Errors","Reflection","Language"]
223 , ns2 == map txt ["Maybe", "Prelude"]
224 , ns3 == map txt ["List", "Prelude"]
225 , ns4 == map txt ["Reflection","Language"] = True
226 tyIsHandler _ = False
228elabPostulate :: ElabInfo -> SyntaxInfo -> Docstring (Either Err PTerm) ->
229 FC -> FnOpts -> Name -> PTerm -> Idris ()
230elabPostulate info syn doc fc opts n ty = do
231 elabType info syn doc [] fc opts n ty
232 putIState . (\ist -> ist{ idris_postulates = S.insert n (idris_postulates ist) }) =<< getIState
233 addIBC (IBCPostulate n)
235 -- remove it from the deferred definitions list
236 solveDeferred n
238elabExtern :: ElabInfo -> SyntaxInfo -> Docstring (Either Err PTerm) ->
239 FC -> FnOpts -> Name -> PTerm -> Idris ()
240elabExtern info syn doc fc opts n ty = do
241 cty <- elabType info syn doc [] fc opts n ty
242 ist <- getIState
243 let arity = length (getArgTys (normalise (tt_ctxt ist) [] cty))
245 putIState . (\ist -> ist{ idris_externs = S.insert (n, arity) (idris_externs ist) }) =<< getIState
246 addIBC (IBCExtern (n, arity))
248 -- remove it from the deferred definitions list
249 solveDeferred n