git.iko.soy/Idris-dev
on 008fb1f help sign in
Idris-dev/src/Idris/Elab/Implementation.hs
514 lines 22 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
102 when (what /= ETypes && (not (null ds && not emptyinterface))) $ do
103 -- Add the parent implementation names to the privileged set
104 oldOpen <- addOpenImpl parents
106 let ips = zip (interface_params ci) ps
107 let ns = case n of
108 NS n ns' -> ns'
109 _ -> []
110 -- get the implicit parameters that need passing through to the
111 -- where block
112 wparams <- mapM (\p -> case p of
113 PApp _ _ args -> getWParams (map getTm args)
114 a@(PRef fc _ f) -> getWParams [a]
115 _ -> return []) ps
116 ist <- getIState
117 let pnames = nub $ map pname (concat (nub wparams)) ++
118 concatMap (namesIn [] ist) ps
120 let superInterfaceImplementations = map (substImplementation ips pnames) (interface_default_super_interfaces ci)
121 undefinedSuperInterfaceImplementations <- filterM (fmap not . isOverlapping ist) superInterfaceImplementations
122 mapM_ (rec_elabDecl info EAll info) undefinedSuperInterfaceImplementations
124 ist <- getIState
125 -- Bring variables in implementation head into scope when building the
126 -- dictionary
127 let headVars = nub $ concatMap getHeadVars ps
128 let (headVarTypes, ty)
129 = case lookupTyExact iname (tt_ctxt ist) of
130 Just ty -> (map (\n -> (n, getTypeIn ist n ty)) headVars, ty)
131 _ -> (zip headVars (repeat Placeholder), Erased)
133 let impps = getImpParams ist (interface_impparams ci)
134 (snd (unApply (substRetTy ty)))
135 let iimpps = zip (interface_impparams ci) impps
137 logElab 5 $ "ImpPS: " ++ show impps ++ " --- " ++ show iimpps
138 logElab 5 $ "Head var types " ++ show headVarTypes ++ " from " ++ show ty
140 let all_meths = map (nsroot . fst) (interface_methods ci)
141 let mtys = map (\ (n, (inj, op, t)) ->
142 let t_in = substMatchesShadow (iimpps ++ ips) pnames t
143 mnamemap =
144 map (\n -> (n, PApp fc (PRef fc [] (decorate ns iname n))
145 (map (toImp fc) headVars)))
146 all_meths
147 t' = substMatchesShadow mnamemap pnames t_in in
148 (decorate ns iname n,
149 op, coninsert cs pextra t', t'))
150 (interface_methods ci)
152 logElab 5 (show (mtys, (iimpps ++ ips)))
153 logElab 5 ("Before defaults: " ++ show ds ++ "\n" ++ show (map fst (interface_methods ci)))
154 let ds_defs = insertDefaults ist iname (interface_defaults ci) ns ds
155 logElab 3 ("After defaults: " ++ show ds_defs ++ "\n")
157 let ds' = reorderDefs (map fst (interface_methods ci)) ds_defs
158 logElab 1 ("Reordered: " ++ show ds' ++ "\n")
160 mapM_ (warnMissing ds' ns iname) (map fst (interface_methods ci))
161 mapM_ (checkInInterface (map fst (interface_methods ci))) (concatMap defined ds')
162 let wbTys = map mkTyDecl mtys
163 let wbVals_orig = map (decorateid (decorate ns iname)) ds'
164 ist <- getIState
165 let wbVals = map (expandParamsD False ist id pextra (map methName mtys)) wbVals_orig
166 let wb = wbTys ++ wbVals
168 logElab 3 $ "Method types " ++ showSep "\n" (map (show . showDeclImp verbosePPOption . mkTyDecl) mtys)
169 logElab 3 $ "Implementation is " ++ show ps ++ " implicits " ++ show (concat (nub wparams))
171 let lhsImps = map (\n -> pimp n (PRef fc [] n) True) headVars
173 let lhs = PApp fc (PRef fc [] iname) (lhsImps ++ map (toExp .fst) pextra)
174 let rhs = PApp fc (PRef fc [] (implementationCtorName ci))
175 (map (pexp . (mkMethApp lhsImps)) mtys)
177 logElab 5 $ "Implementation LHS " ++ show totopts ++ "\n" ++ showTmImpls lhs ++ " " ++ show headVars
178 logElab 5 $ "Implementation RHS " ++ show rhs
180 push_estack iname True
181 logElab 3 ("Method types: " ++ show wbTys)
182 logElab 3 ("Method bodies (before params): " ++ show wbVals_orig)
183 logElab 3 ("Method bodies: " ++ show wbVals)
185 let idecls = [PClauses fc totopts iname
186 [PClause fc iname lhs [] rhs []]]
188 mapM_ (rec_elabDecl info EAll info) (map (impBind headVarTypes) wbTys)
189 mapM_ (rec_elabDecl info EAll info) idecls
191 ctxt <- getContext
192 let ifn_ty = case lookupTyExact iname ctxt of
193 Just t -> t
194 Nothing -> error "Can't happen (interface constructor)"
195 let ifn_is = case lookupCtxtExact iname (idris_implicits ist) of
196 Just t -> t
197 Nothing -> []
198 let prop_params = getParamsInType ist [] ifn_is ifn_ty
200 logElab 3 $ "Propagating parameters to methods: "
201 ++ show (iname, prop_params)
203 let wbVals' = map (addParams prop_params) wbVals
205 logElab 5 ("Elaborating method bodies: " ++ show wbVals')
206 mapM_ (rec_elabDecl info EAll info) wbVals'
208 mapM_ (checkInjectiveDef fc (interface_methods ci)) (zip ds' wbVals')
210 pop_estack
212 setOpenImpl oldOpen
213-- totalityCheckBlock
215 checkInjectiveArgs fc n (interface_determiners ci) (lookupTyExact iname (tt_ctxt ist))
216 addIBC (IBCImplementation intImpl (isNothing expn) n iname)
218 where
219 getImpParams ist = zipWith (\n tm -> delab ist tm)
221 intImpl = case ps of
222 [PConstant NoFC (AType (ATInt ITNative))] -> True
223 _ -> False
225 mkiname n' ns ps' expn' =
226 case expn' of
227 Nothing -> case ns of
228 [] -> SN (sImplementationN n' (map show ps'))
229 m -> sNS (SN (sImplementationN n' (map show ps'))) m
230 Just nm -> nm
232 substImplementation ips pnames (PImplementation doc argDocs syn _ cs parents acc opts n nfc ps pextra t expn ds)
233 = PImplementation doc argDocs syn fc cs parents acc opts n nfc
234 (map (substMatchesShadow ips pnames) ps)
235 pextra
236 (substMatchesShadow ips pnames t) expn ds
238 isOverlapping i (PImplementation doc argDocs syn _ _ _ _ _ n nfc ps pextra t expn _)
239 = case lookupCtxtName n (idris_interfaces i) of
240 [(n, ci)] -> let iname = (mkiname n (namespace info) ps expn) in
241 case lookupTy iname (tt_ctxt i) of
242 [] -> elabFindOverlapping i ci iname syn t
243 (_:_) -> return True
244 _ -> return False -- couldn't find interface, just let elabImplementation fail later
246 -- TODO: largely based upon elabType' - should try to abstract
247 -- Issue #1614 in the issue tracker:
248 -- https://github.com/idris-lang/Idris-dev/issues/1614
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 sc) = isInj i sc
510 isInj _ _ = True
512 instantiateRetTy (Bind n (Pi _ _ _ _) sc)
513 = substV (P Bound n Erased) (instantiateRetTy sc)
514 instantiateRetTy t = t