git.iko.soy/Idris-dev
on 385dcbf help sign in
Idris-dev/src/Idris/Elab/Implementation.hs
515 lines 21 kB history raw
1{-|
2Module : Idris.Elab.Implementation
3Description : Code to elaborate instances.
4Copyright :
5License : BSD3
6Maintainer : The Idris Community.
7-}
8{-# LANGUAGE PatternGuards #-}
9module Idris.Elab.Implementation(elabImplementation) where
11import Idris.AbsSyntax
12import Idris.ASTUtils
13import Idris.Core.CaseTree
14import Idris.Core.Elaborate hiding (Tactic(..))
15import Idris.Core.Evaluate
16import Idris.Core.Execute
17import Idris.Core.TT
18import Idris.Core.Typecheck
19import Idris.Coverage
20import Idris.DataOpts
21import Idris.DeepSeq
22import Idris.Delaborate
23import Idris.Docstrings
24import Idris.DSL
25import Idris.Elab.Data
26import Idris.Elab.Term
27import Idris.Elab.Type
28import Idris.Elab.Utils
29import Idris.Error
30import Idris.Imports
31import Idris.Inliner
32import Idris.Output (iWarn, iputStrLn, pshow, sendHighlighting)
33import Idris.PartialEval
34import Idris.Primitives
35import Idris.Providers
36import IRTS.Lang
38import Util.Pretty (pretty, text)
40import Prelude hiding (id, (.))
42import Control.Applicative hiding (Const)
43import Control.Category
44import Control.DeepSeq
45import Control.Monad
46import Control.Monad.State.Strict as State
47import Data.Char (isLetter, toLower)
48import Data.List
49import Data.List.Split (splitOn)
50import qualified Data.Map as Map
51import Data.Maybe
52import qualified Data.Set as S
53import qualified Data.Text as T
54import Debug.Trace
57elabImplementation :: ElabInfo
58 -> SyntaxInfo
59 -> Docstring (Either Err PTerm)
60 -> [(Name, Docstring (Either Err PTerm))]
61 -> ElabWhat -- ^ phase
62 -> FC
63 -> [(Name, PTerm)] -- ^ constraints
64 -> [Name] -- ^ parent dictionary names (optionally)
65 -> Accessibility
66 -> FnOpts
67 -> Name -- ^ the interface
68 -> FC -- ^ precise location of interface name
69 -> [PTerm] -- ^ interface parameters (i.e. implementation)
70 -> [(Name, PTerm)] -- ^ Extra arguments in scope (e.g. implementation in where block)
71 -> PTerm -- ^ full implementation type
72 -> Maybe Name -- ^ explicit name
73 -> [PDecl]
74 -> Idris ()
75elabImplementation info syn doc argDocs what fc cs parents acc opts n nfc ps pextra t expn ds = do
76 ist <- getIState
77 (n, ci) <- case lookupCtxtName n (idris_interfaces ist) of
78 [c] -> return c
79 [] -> ifail $ show fc ++ ":" ++ show n ++ " is not an interface"
80 cs -> tclift $ tfail $ At fc
81 (CantResolveAlts (map fst cs))
82 let constraint = PApp fc (PRef fc [] n) (map pexp ps)
83 let iname = mkiname n (namespace info) ps expn
84 putIState (ist { hide_list = addDef iname acc (hide_list ist) })
85 ist <- getIState
87 let totopts = Dictionary : Inlinable : opts
89 let emptyinterface = null (interface_methods ci)
90 when (what /= EDefns) $ do
91 nty <- elabType' True info syn doc argDocs fc totopts iname NoFC
92 (piBindp expl_param pextra t)
93 -- if the implementation type matches any of the implementations we have already,
94 -- and it's not a named implementation, then it's overlapping, so report an error
95 case expn of
96 Nothing
97 | OverlappingDictionary `notElem` opts ->
98 do mapM_ (maybe (return ()) overlapping . findOverlapping ist (interface_determiners ci) (delab ist nty))
99 (map fst $ interface_implementations ci)
100 addImplementation intImpl True n iname
101 _ -> addImplementation intImpl False n iname
103 ist <- getIState
104 checkInjectiveArgs fc n (interface_determiners ci) (lookupTyExact iname (tt_ctxt ist))
106 when (what /= ETypes && (not (null ds && not emptyinterface))) $ do
107 -- Add the parent implementation names to the privileged set
108 oldOpen <- addOpenImpl parents
110 let ips = zip (interface_params ci) ps
111 let ns = case n of
112 NS n ns' -> ns'
113 _ -> []
114 -- get the implicit parameters that need passing through to the
115 -- where block
116 wparams <- mapM (\p -> case p of
117 PApp _ _ args -> getWParams (map getTm args)
118 a@(PRef fc _ f) -> getWParams [a]
119 _ -> return []) ps
120 ist <- getIState
121 let pnames = nub $ map pname (concat (nub wparams)) ++
122 concatMap (namesIn [] ist) ps
124 let superInterfaceImplementations = map (substImplementation ips pnames) (interface_default_super_interfaces ci)
125 undefinedSuperInterfaceImplementations <- filterM (fmap not . isOverlapping ist) superInterfaceImplementations
126 mapM_ (rec_elabDecl info EAll info) undefinedSuperInterfaceImplementations
128 ist <- getIState
129 -- Bring variables in implementation head into scope when building the
130 -- dictionary
131 let headVars = nub $ concatMap getHeadVars ps
132 let (headVarTypes, ty)
133 = case lookupTyExact iname (tt_ctxt ist) of
134 Just ty -> (map (\n -> (n, getTypeIn ist n ty)) headVars, ty)
135 _ -> (zip headVars (repeat Placeholder), Erased)
137 let impps = getImpParams ist (interface_impparams ci)
138 (snd (unApply (substRetTy ty)))
139 let iimpps = zip (interface_impparams ci) impps
141 logElab 5 $ "ImpPS: " ++ show impps ++ " --- " ++ show iimpps
142 logElab 5 $ "Head var types " ++ show headVarTypes ++ " from " ++ show ty
144 let all_meths = map (nsroot . fst) (interface_methods ci)
145 let mtys = map (\ (n, (inj, op, t)) ->
146 let t_in = substMatchesShadow (iimpps ++ ips) pnames t
147 mnamemap =
148 map (\n -> (n, PApp fc (PRef fc [] (decorate ns iname n))
149 (map (toImp fc) headVars)))
150 all_meths
151 t' = substMatchesShadow mnamemap pnames t_in in
152 (decorate ns iname n,
153 op, coninsert cs pextra t', t'))
154 (interface_methods ci)
156 logElab 5 (show (mtys, (iimpps ++ ips)))
157 logElab 5 ("Before defaults: " ++ show ds ++ "\n" ++ show (map fst (interface_methods ci)))
158 let ds_defs = insertDefaults ist iname (interface_defaults ci) ns ds
159 logElab 3 ("After defaults: " ++ show ds_defs ++ "\n")
161 let ds' = reorderDefs (map fst (interface_methods ci)) ds_defs
162 logElab 1 ("Reordered: " ++ show ds' ++ "\n")
164 mapM_ (warnMissing ds' ns iname) (map fst (interface_methods ci))
165 mapM_ (checkInInterface (map fst (interface_methods ci))) (concatMap defined ds')
166 let wbTys = map mkTyDecl mtys
167 let wbVals_orig = map (decorateid (decorate ns iname)) ds'
168 ist <- getIState
169 let wbVals = map (expandParamsD False ist id pextra (map methName mtys)) wbVals_orig
170 let wb = wbTys ++ wbVals
172 logElab 3 $ "Method types " ++ showSep "\n" (map (show . showDeclImp verbosePPOption . mkTyDecl) mtys)
173 logElab 3 $ "Implementation is " ++ show ps ++ " implicits " ++ show (concat (nub wparams))
175 let lhsImps = map (\n -> pimp n (PRef fc [] n) True) headVars
177 let lhs = PApp fc (PRef fc [] iname) (lhsImps ++ map (toExp .fst) pextra)
178 let rhs = PApp fc (PRef fc [] (implementationCtorName ci))
179 (map (pexp . (mkMethApp lhsImps)) mtys)
181 logElab 5 $ "Implementation LHS " ++ show totopts ++ "\n" ++ showTmImpls lhs ++ " " ++ show headVars
182 logElab 5 $ "Implementation RHS " ++ show rhs
184 push_estack iname True
185 logElab 3 ("Method types: " ++ show wbTys)
186 logElab 3 ("Method bodies (before params): " ++ show wbVals_orig)
187 logElab 3 ("Method bodies: " ++ show wbVals)
189 let idecls = [PClauses fc totopts iname
190 [PClause fc iname lhs [] rhs []]]
192 mapM_ (rec_elabDecl info EAll info) (map (impBind headVarTypes) wbTys)
193 mapM_ (rec_elabDecl info EAll info) idecls
195 ctxt <- getContext
196 let ifn_ty = case lookupTyExact iname ctxt of
197 Just t -> t
198 Nothing -> error "Can't happen (interface constructor)"
199 let ifn_is = case lookupCtxtExact iname (idris_implicits ist) of
200 Just t -> t
201 Nothing -> []
202 let prop_params = getParamsInType ist [] ifn_is ifn_ty
204 logElab 3 $ "Propagating parameters to methods: "
205 ++ show (iname, prop_params)
207 let wbVals' = map (addParams prop_params) wbVals
209 logElab 5 ("Elaborating method bodies: " ++ show wbVals')
210 mapM_ (rec_elabDecl info EAll info) wbVals'
212 mapM_ (checkInjectiveDef fc (interface_methods ci)) (zip ds' wbVals')
214 pop_estack
216 setOpenImpl oldOpen
217-- totalityCheckBlock
219 addIBC (IBCImplementation intImpl (isNothing expn) n iname)
221 where
222 getImpParams ist = zipWith (\n tm -> delab ist tm)
224 intImpl = case ps of
225 [PConstant NoFC (AType (ATInt ITNative))] -> True
226 _ -> False
228 mkiname n' ns ps' expn' =
229 case expn' of
230 Nothing -> case ns of
231 [] -> SN (sImplementationN n' (map show ps'))
232 m -> sNS (SN (sImplementationN n' (map show ps'))) m
233 Just nm -> nm
235 substImplementation ips pnames (PImplementation doc argDocs syn _ cs parents acc opts n nfc ps pextra t expn ds)
236 = PImplementation doc argDocs syn fc cs parents acc opts n nfc
237 (map (substMatchesShadow ips pnames) ps)
238 pextra
239 (substMatchesShadow ips pnames t) expn ds
241 isOverlapping i (PImplementation doc argDocs syn _ _ _ _ _ n nfc ps pextra t expn _)
242 = case lookupCtxtName n (idris_interfaces i) of
243 [(n, ci)] -> let iname = (mkiname n (namespace info) ps expn) in
244 case lookupTy iname (tt_ctxt i) of
245 [] -> elabFindOverlapping i ci iname syn t
246 (_:_) -> return True
247 _ -> return False -- couldn't find interface, just let elabImplementation fail later
249 elabFindOverlapping i ci iname syn t
250 = do ty' <- addUsingConstraints syn fc t
251 -- TODO think: something more in info?
252 ty' <- implicit info syn iname ty'
253 let ty = addImpl [] i ty'
254 ctxt <- getContext
255 (ElabResult tyT _ _ ctxt' newDecls highlights newGName, _) <-
256 tclift $ elaborate (constraintNS info) ctxt (idris_datatypes i) (idris_name i) iname (TType (UVal 0)) initEState
257 (errAt "type of " iname Nothing (erun fc (build i info ERHS [] iname ty)))
258 setContext ctxt'
259 processTacticDecls info newDecls
260 sendHighlighting highlights
261 updateIState $ \i -> i { idris_name = newGName }
263 ctxt <- getContext
264 (cty, _) <- recheckC (constraintNS info) fc id [] tyT
265 let nty = normalise ctxt [] cty
266 return $ any (isJust . findOverlapping i (interface_determiners ci) (delab i nty)) (map fst $ interface_implementations ci)
268 findOverlapping i dets t n
269 | SN (ParentN _ _) <- n = Nothing
270 | Just opts <- lookupCtxtExact n (idris_flags i),
271 OverlappingDictionary `elem` opts = Nothing
272 | otherwise
273 = case lookupTy n (tt_ctxt i) of
274 [t'] -> let tret = getRetType t
275 tret' = getRetType (delab i t') in
276 case matchArgs i dets tret' tret of
277 Right _ -> Just tret'
278 Left _ -> case matchArgs i dets tret tret' of
279 Right _ -> Just tret'
280 Left _ -> Nothing
281 _ -> Nothing
282 overlapping t' = tclift $ tfail (At fc (Msg $
283 "Overlapping implementation: " ++ show t' ++ " already defined"))
284 getRetType (PPi _ _ _ _ sc) = getRetType sc
285 getRetType t = t
287 matchArgs i dets x y =
288 let x' = keepDets dets x
289 y' = keepDets dets y in
290 matchClause i x' y'
292 keepDets dets (PApp fc f args)
293 = PApp fc f $ let a' = zip [0..] args in
294 map snd (filter (\(i, _) -> i `elem` dets) a')
295 keepDets dets t = t
297 methName (n, _, _, _) = n
298 toExp n = pexp (PRef fc [] n)
300 mkMethApp ps (n, _, _, ty)
301 = lamBind 0 ty (papp fc (PRef fc [] n)
302 (ps ++ map (toExp . fst) pextra ++ methArgs 0 ty))
303 where
304 needed is p = pname p `elem` map pname is
306 lamBind i (PPi (Constraint _ _ _) _ _ _ sc) sc'
307 = PLam fc (sMN i "meth") NoFC Placeholder (lamBind (i+1) sc sc')
308 lamBind i (PPi _ n _ ty sc) sc'
309 = PLam fc (sMN i "meth") NoFC Placeholder (lamBind (i+1) sc sc')
310 lamBind i _ sc = sc
311 methArgs i (PPi (Imp _ _ _ _ _ _) n _ ty sc)
312 = PImp 0 True [] n (PRef fc [] (sMN i "meth")) : methArgs (i+1) sc
313 methArgs i (PPi (Exp _ _ _ _) n _ ty sc)
314 = PExp 0 [] (sMN 0 "marg") (PRef fc [] (sMN i "meth")) : methArgs (i+1) sc
315 methArgs i (PPi (Constraint _ _ _) n _ ty sc)
316 = PConstraint 0 [] (sMN 0 "marg") (PResolveTC fc) : methArgs (i+1) sc
317 methArgs i _ = []
319 papp fc f [] = f
320 papp fc f as = PApp fc f as
322 getWParams [] = return []
323 getWParams (p : ps)
324 | PRef _ _ n <- p
325 = do ps' <- getWParams ps
326 ctxt <- getContext
327 case lookupP n ctxt of
328 [] -> return (pimp n (PRef fc [] n) True : ps')
329 _ -> return ps'
330 getWParams (_ : ps) = getWParams ps
332 decorate ns iname (NS (UN nm) s)
333 = NS (SN (WhereN 0 iname (SN (MethodN (UN nm))))) ns
334 decorate ns iname nm
335 = NS (SN (WhereN 0 iname (SN (MethodN nm)))) ns
337 mkTyDecl (n, op, t, _)
338 = PTy emptyDocstring [] syn fc op n NoFC
339 (mkUniqueNames [] [] t)
341 conbind :: [(Name, PTerm)] -> PTerm -> PTerm
342 conbind ((c,ty) : ns) x = PPi constraint c NoFC ty (conbind ns x)
343 conbind [] x = x
345 extrabind :: [(Name, PTerm)] -> PTerm -> PTerm
346 extrabind ((c,ty) : ns) x = PPi expl c NoFC ty (extrabind ns x)
347 extrabind [] x = x
349 coninsert :: [(Name, PTerm)] -> [(Name, PTerm)] -> PTerm -> PTerm
350 coninsert cs ex (PPi p@(Imp _ _ _ _ _ _) n fc t sc) = PPi p n fc t (coninsert cs ex sc)
351 coninsert cs ex sc = conbind cs (extrabind ex sc)
353 -- Reorder declarations to be in the same order as defined in the
354 -- interface declaration (important so that we insert default definitions
355 -- in the right place, and so that dependencies between methods are
356 -- respected)
357 reorderDefs :: [Name] -> [PDecl] -> [PDecl]
358 reorderDefs ns [] = []
359 reorderDefs [] ds = ds
360 reorderDefs (n : ns) ds = case pick n [] ds of
361 Just (def, ds') -> def : reorderDefs ns ds'
362 Nothing -> reorderDefs ns ds
364 pick n acc [] = Nothing
365 pick n acc (def@(PClauses _ _ cn cs) : ds)
366 | nsroot n == nsroot cn = Just (def, acc ++ ds)
367 pick n acc (d : ds) = pick n (acc ++ [d]) ds
369 insertDefaults :: IState -> Name ->
370 [(Name, (Name, PDecl))] -> [T.Text] ->
371 [PDecl] -> [PDecl]
372 insertDefaults i iname [] ns ds = ds
373 insertDefaults i iname ((n,(dn, clauses)) : defs) ns ds
374 = insertDefaults i iname defs ns (insertDef i n dn clauses ns iname ds)
376 insertDef i meth def clauses ns iname decls
377 | not $ any (clauseFor meth iname ns) decls
378 = let newd = expandParamsD False i (\n -> meth) [] [def] clauses in
379 -- trace (show newd) $
380 decls ++ [newd]
381 | otherwise = decls
383 warnMissing decls ns iname meth
384 | not $ any (clauseFor meth iname ns) decls
385 = iWarn fc . text $ "method " ++ show meth ++ " not defined"
386 | otherwise = return ()
388 checkInInterface ns meth
389 | any (eqRoot meth) ns = return ()
390 | otherwise = tclift $ tfail (At fc (Msg $
391 show meth ++ " not a method of interface " ++ show n))
393 eqRoot x y = nsroot x == nsroot y
395 clauseFor m iname ns (PClauses _ _ m' _)
396 = decorate ns iname m == decorate ns iname m'
397 clauseFor m iname ns _ = False
399getHeadVars :: PTerm -> [Name]
400getHeadVars (PRef _ _ n) | implicitable n = [n]
401getHeadVars (PApp _ _ args) = concatMap getHeadVars (map getTm args)
402getHeadVars (PPair _ _ _ l r) = getHeadVars l ++ getHeadVars r
403getHeadVars (PDPair _ _ _ l t r) = getHeadVars l ++ getHeadVars t ++ getHeadVars t
404getHeadVars _ = []
406-- | Implicitly bind variables from the implementation head in method types
407impBind :: [(Name, PTerm)] -> PDecl -> PDecl
408impBind vs (PTy d ds syn fc opts n fc' t)
409 = PTy d ds syn fc opts n fc'
410 (doImpBind (filter (\(n, ty) -> n `notElem` boundIn t) vs) t)
411 where
412 doImpBind [] ty = ty
413 doImpBind ((n, argty) : ns) ty
414 = PPi impl n NoFC argty (doImpBind ns ty)
416 boundIn (PPi _ n _ _ sc) = n : boundIn sc
417 boundIn _ = []
419getTypeIn :: IState -> Name -> Type -> PTerm
420getTypeIn ist n (Bind x b sc)
421 | n == x = delab ist (binderTy b)
422 | otherwise = getTypeIn ist n (substV (P Ref x Erased) sc)
423getTypeIn ist n tm = Placeholder
425toImp fc n = pimp n (PRef fc [] n) True
427-- | Propagate interface parameters to method bodies, if they're not
428-- already there, and they are needed (i.e. appear in method's type)
429addParams :: [Name] -> PDecl -> PDecl
430addParams ps (PClauses fc opts n cs) = PClauses fc opts n (map addCParams cs)
431 where
432 addCParams (PClause fc n lhs ws rhs wb)
433 = PClause fc n (addTmParams (dropPs (allNamesIn lhs) ps) lhs) ws rhs wb
434 addCParams (PWith fc n lhs ws sc pn ds)
435 = PWith fc n (addTmParams (dropPs (allNamesIn lhs) ps) lhs) ws sc pn
436 (map (addParams ps) ds)
437 addCParams c = c
439 addTmParams ps (PRef fc hls n)
440 = PApp fc (PRef fc hls n) (map (toImp fc) ps)
441 addTmParams ps (PApp fc ap@(PRef fc' hls n) args)
442 = PApp fc ap (mergePs (map (toImp fc) ps) args)
443 addTmParams ps tm = tm
445 mergePs [] args = args
446 mergePs (p : ps) args
447 | isImplicit p,
448 pname p `notElem` map pname args
449 = p : mergePs ps args
450 where
451 isImplicit (PExp{}) = False
452 isImplicit _ = True
453 mergePs (p : ps) args
454 = mergePs ps args
456 -- Don't propagate a parameter if the name is rebound explicitly
457 dropPs :: [Name] -> [Name] -> [Name]
458 dropPs ns = filter (\x -> x `notElem` ns)
460addParams ps d = d
462-- | Check a given method definition is injective, if the interface info
463-- says it needs to be. Takes originally written decl and the one
464-- with name decoration, so we know which name to look up.
465checkInjectiveDef :: FC -> [(Name, (Bool, FnOpts, PTerm))] ->
466 (PDecl, PDecl) -> Idris ()
467checkInjectiveDef fc ns (PClauses _ _ n cs, PClauses _ _ elabn _)
468 | Just (True, _, _) <- clookup n ns
469 = do ist <- getIState
470 case lookupDefExact elabn (tt_ctxt ist) of
471 Just (CaseOp _ _ _ _ _ cdefs) ->
472 checkInjectiveCase ist (snd (cases_compiletime cdefs))
473 where
474 checkInjectiveCase ist (STerm tm)
475 = checkInjectiveApp ist (fst (unApply tm))
476 checkInjectiveCase _ _ = notifail
478 checkInjectiveApp ist (P (TCon _ _) n _) = return ()
479 checkInjectiveApp ist (P (DCon _ _ _) n _) = return ()
480 checkInjectiveApp ist (P Ref n _)
481 | Just True <- lookupInjectiveExact n (tt_ctxt ist) = return ()
482 checkInjectiveApp ist (P Ref n _) = notifail
483 checkInjectiveApp _ _ = notifail
485 notifail = ierror $ At fc (Msg (show n ++ " must be defined by a type or data constructor"))
487 clookup n [] = Nothing
488 clookup n ((n', d) : ds) | nsroot n == nsroot n' = Just d
489 | otherwise = Nothing
490checkInjectiveDef fc ns _ = return ()
492checkInjectiveArgs :: FC -> Name -> [Int] -> Maybe Type -> Idris ()
493checkInjectiveArgs fc n ds Nothing = return ()
494checkInjectiveArgs fc n ds (Just ty)
495 = do ist <- getIState
496 let (_, args) = unApply (instantiateRetTy ty)
497 ci 0 ist args
498 where
499 ci i ist (a : as) | i `elem` ds
500 = if isInj ist a then ci (i + 1) ist as
501 else tclift $ tfail (At fc (InvalidTCArg n a))
502 ci i ist (a : as) = ci (i + 1) ist as
503 ci i ist [] = return ()
505 isInj i (P Bound n _) = True
506 isInj i (P _ n _) = isConName n (tt_ctxt i)
507 isInj i (App _ f a) = isInj i f && isInj i a
508 isInj i (V _) = True
509 isInj i (Bind n b@(Pi{}) sc) = isInj i (binderTy b) && isInj i sc
510 isInj i (Bind n b sc) = False
511 isInj _ _ = True
513 instantiateRetTy (Bind n (Pi _ _ _ _) sc)
514 = substV (P Bound n Erased) (instantiateRetTy sc)
515 instantiateRetTy t = t