git.iko.soy/Idris-dev
on 199c45d help sign in
Idris-dev/src/Idris/Elab/Implementation.hs
521 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' = map (addUnfold iname (map fst (interface_methods ci))) $
158 reorderDefs (map fst (interface_methods ci)) ds_defs
159 logElab 1 ("Reordered: " ++ show ds' ++ "\n")
161 mapM_ (warnMissing ds' ns iname) (map fst (interface_methods ci))
162 mapM_ (checkInInterface (map fst (interface_methods ci))) (concatMap defined ds')
163 let wbTys = map mkTyDecl mtys
164 let wbVals_orig = map (decorateid (decorate ns iname)) ds'
165 ist <- getIState
166 let wbVals = map (expandParamsD False ist id pextra (map methName mtys)) wbVals_orig
167 let wb = wbTys ++ wbVals
169 logElab 3 $ "Method types " ++ showSep "\n" (map (show . showDeclImp verbosePPOption . mkTyDecl) mtys)
170 logElab 3 $ "Implementation is " ++ show ps ++ " implicits " ++ show (concat (nub wparams))
172 let lhsImps = map (\n -> pimp n (PRef fc [] n) True) headVars
174 let lhs = PApp fc (PRef fc [] iname) (lhsImps ++ map (toExp .fst) pextra)
175 let rhs = PApp fc (PRef fc [] (implementationCtorName ci))
176 (map (pexp . (mkMethApp lhsImps)) mtys)
178 logElab 5 $ "Implementation LHS " ++ show totopts ++ "\n" ++ showTmImpls lhs ++ " " ++ show headVars
179 logElab 5 $ "Implementation RHS " ++ show rhs
181 push_estack iname True
182 logElab 3 ("Method types: " ++ show wbTys)
183 logElab 3 ("Method bodies (before params): " ++ show wbVals_orig)
184 logElab 3 ("Method bodies: " ++ show wbVals)
186 let idecls = [PClauses fc totopts iname
187 [PClause fc iname lhs [] rhs []]]
189 mapM_ (rec_elabDecl info EAll info) (map (impBind headVarTypes) wbTys)
190 mapM_ (rec_elabDecl info EAll info) idecls
192 ctxt <- getContext
193 let ifn_ty = case lookupTyExact iname ctxt of
194 Just t -> t
195 Nothing -> error "Can't happen (interface constructor)"
196 let ifn_is = case lookupCtxtExact iname (idris_implicits ist) of
197 Just t -> t
198 Nothing -> []
199 let prop_params = getParamsInType ist [] ifn_is ifn_ty
201 logElab 3 $ "Propagating parameters to methods: "
202 ++ show (iname, prop_params)
204 let wbVals' = map (addParams prop_params) wbVals
206 logElab 5 ("Elaborating method bodies: " ++ show wbVals')
207 mapM_ (rec_elabDecl info EAll info) wbVals'
209 mapM_ (checkInjectiveDef fc (interface_methods ci)) (zip ds' wbVals')
211 pop_estack
213 setOpenImpl oldOpen
214-- totalityCheckBlock
216 checkInjectiveArgs fc n (interface_determiners ci) (lookupTyExact iname (tt_ctxt ist))
217 addIBC (IBCImplementation intImpl (isNothing expn) n iname)
219 where
220 getImpParams ist = zipWith (\n tm -> delab ist tm)
222 intImpl = case ps of
223 [PConstant NoFC (AType (ATInt ITNative))] -> True
224 _ -> False
226 addUnfold iname ms (PTy doc docs syn fc opts n fc' tm)
227 = PTy doc docs syn fc (UnfoldIface iname ms : opts) n fc' tm
228 addUnfold iname ms (PClauses fc opts n cs)
229 = PClauses fc (UnfoldIface iname ms : opts) n cs
230 addUnfold iname ms dec = dec
232 mkiname n' ns ps' expn' =
233 case expn' of
234 Nothing -> case ns of
235 [] -> SN (sImplementationN n' (map show ps'))
236 m -> sNS (SN (sImplementationN n' (map show ps'))) m
237 Just nm -> nm
239 substImplementation ips pnames (PImplementation doc argDocs syn _ cs parents acc opts n nfc ps pextra t expn ds)
240 = PImplementation doc argDocs syn fc cs parents acc opts n nfc
241 (map (substMatchesShadow ips pnames) ps)
242 pextra
243 (substMatchesShadow ips pnames t) expn ds
245 isOverlapping i (PImplementation doc argDocs syn _ _ _ _ _ n nfc ps pextra t expn _)
246 = case lookupCtxtName n (idris_interfaces i) of
247 [(n, ci)] -> let iname = (mkiname n (namespace info) ps expn) in
248 case lookupTy iname (tt_ctxt i) of
249 [] -> elabFindOverlapping i ci iname syn t
250 (_:_) -> return True
251 _ -> return False -- couldn't find interface, just let elabImplementation fail later
253 -- TODO: largely based upon elabType' - should try to abstract
254 -- Issue #1614 in the issue tracker:
255 -- https://github.com/idris-lang/Idris-dev/issues/1614
256 elabFindOverlapping i ci iname syn t
257 = do ty' <- addUsingConstraints syn fc t
258 -- TODO think: something more in info?
259 ty' <- implicit info syn iname ty'
260 let ty = addImpl [] i ty'
261 ctxt <- getContext
262 (ElabResult tyT _ _ ctxt' newDecls highlights newGName, _) <-
263 tclift $ elaborate (constraintNS info) ctxt (idris_datatypes i) (idris_name i) iname (TType (UVal 0)) initEState
264 (errAt "type of " iname Nothing (erun fc (build i info ERHS [] iname ty)))
265 setContext ctxt'
266 processTacticDecls info newDecls
267 sendHighlighting highlights
268 updateIState $ \i -> i { idris_name = newGName }
270 ctxt <- getContext
271 (cty, _) <- recheckC (constraintNS info) fc id [] tyT
272 let nty = normalise ctxt [] cty
273 return $ any (isJust . findOverlapping i (interface_determiners ci) (delab i nty)) (map fst $ interface_implementations ci)
275 findOverlapping i dets t n
276 | SN (ParentN _ _) <- n = Nothing
277 | Just opts <- lookupCtxtExact n (idris_flags i),
278 OverlappingDictionary `elem` opts = Nothing
279 | otherwise
280 = case lookupTy n (tt_ctxt i) of
281 [t'] -> let tret = getRetType t
282 tret' = getRetType (delab i t') in
283 case matchArgs i dets tret' tret of
284 Right _ -> Just tret'
285 Left _ -> case matchArgs i dets tret tret' of
286 Right _ -> Just tret'
287 Left _ -> Nothing
288 _ -> Nothing
289 overlapping t' = tclift $ tfail (At fc (Msg $
290 "Overlapping implementation: " ++ show t' ++ " already defined"))
291 getRetType (PPi _ _ _ _ sc) = getRetType sc
292 getRetType t = t
294 matchArgs i dets x y =
295 let x' = keepDets dets x
296 y' = keepDets dets y in
297 matchClause i x' y'
299 keepDets dets (PApp fc f args)
300 = PApp fc f $ let a' = zip [0..] args in
301 map snd (filter (\(i, _) -> i `elem` dets) a')
302 keepDets dets t = t
304 methName (n, _, _, _) = n
305 toExp n = pexp (PRef fc [] n)
307 mkMethApp ps (n, _, _, ty)
308 = lamBind 0 ty (papp fc (PRef fc [] n)
309 (ps ++ map (toExp . fst) pextra ++ methArgs 0 ty))
310 where
311 needed is p = pname p `elem` map pname is
313 lamBind i (PPi (Constraint _ _ _) _ _ _ sc) sc'
314 = PLam fc (sMN i "meth") NoFC Placeholder (lamBind (i+1) sc sc')
315 lamBind i (PPi _ n _ ty sc) sc'
316 = PLam fc (sMN i "meth") NoFC Placeholder (lamBind (i+1) sc sc')
317 lamBind i _ sc = sc
318 methArgs i (PPi (Imp _ _ _ _ _ _) n _ ty sc)
319 = PImp 0 True [] n (PRef fc [] (sMN i "meth")) : methArgs (i+1) sc
320 methArgs i (PPi (Exp _ _ _ _) n _ ty sc)
321 = PExp 0 [] (sMN 0 "marg") (PRef fc [] (sMN i "meth")) : methArgs (i+1) sc
322 methArgs i (PPi (Constraint _ _ _) n _ ty sc)
323 = PConstraint 0 [] (sMN 0 "marg") (PResolveTC fc) : methArgs (i+1) sc
324 methArgs i _ = []
326 papp fc f [] = f
327 papp fc f as = PApp fc f as
329 getWParams [] = return []
330 getWParams (p : ps)
331 | PRef _ _ n <- p
332 = do ps' <- getWParams ps
333 ctxt <- getContext
334 case lookupP n ctxt of
335 [] -> return (pimp n (PRef fc [] n) True : ps')
336 _ -> return ps'
337 getWParams (_ : ps) = getWParams ps
339 decorate ns iname (NS (UN nm) s)
340 = NS (SN (WhereN 0 iname (SN (MethodN (UN nm))))) ns
341 decorate ns iname nm
342 = NS (SN (WhereN 0 iname (SN (MethodN nm)))) ns
344 mkTyDecl (n, op, t, _)
345 = PTy emptyDocstring [] syn fc op n NoFC
346 (mkUniqueNames [] [] t)
348 conbind :: [(Name, PTerm)] -> PTerm -> PTerm
349 conbind ((c,ty) : ns) x = PPi constraint c NoFC ty (conbind ns x)
350 conbind [] x = x
352 extrabind :: [(Name, PTerm)] -> PTerm -> PTerm
353 extrabind ((c,ty) : ns) x = PPi expl c NoFC ty (extrabind ns x)
354 extrabind [] x = x
356 coninsert :: [(Name, PTerm)] -> [(Name, PTerm)] -> PTerm -> PTerm
357 coninsert cs ex (PPi p@(Imp _ _ _ _ _ _) n fc t sc) = PPi p n fc t (coninsert cs ex sc)
358 coninsert cs ex sc = conbind cs (extrabind ex sc)
360 -- Reorder declarations to be in the same order as defined in the
361 -- interface declaration (important so that we insert default definitions
362 -- in the right place, and so that dependencies between methods are
363 -- respected)
364 reorderDefs :: [Name] -> [PDecl] -> [PDecl]
365 reorderDefs ns [] = []
366 reorderDefs [] ds = ds
367 reorderDefs (n : ns) ds = case pick n [] ds of
368 Just (def, ds') -> def : reorderDefs ns ds'
369 Nothing -> reorderDefs ns ds
371 pick n acc [] = Nothing
372 pick n acc (def@(PClauses _ _ cn cs) : ds)
373 | nsroot n == nsroot cn = Just (def, acc ++ ds)
374 pick n acc (d : ds) = pick n (acc ++ [d]) ds
376 insertDefaults :: IState -> Name ->
377 [(Name, (Name, PDecl))] -> [T.Text] ->
378 [PDecl] -> [PDecl]
379 insertDefaults i iname [] ns ds = ds
380 insertDefaults i iname ((n,(dn, clauses)) : defs) ns ds
381 = insertDefaults i iname defs ns (insertDef i n dn clauses ns iname ds)
383 insertDef i meth def clauses ns iname decls
384 | not $ any (clauseFor meth iname ns) decls
385 = let newd = expandParamsD False i (\n -> meth) [] [def] clauses in
386 -- trace (show newd) $
387 decls ++ [newd]
388 | otherwise = decls
390 warnMissing decls ns iname meth
391 | not $ any (clauseFor meth iname ns) decls
392 = iWarn fc . text $ "method " ++ show meth ++ " not defined"
393 | otherwise = return ()
395 checkInInterface ns meth
396 | any (eqRoot meth) ns = return ()
397 | otherwise = tclift $ tfail (At fc (Msg $
398 show meth ++ " not a method of interface " ++ show n))
400 eqRoot x y = nsroot x == nsroot y
402 clauseFor m iname ns (PClauses _ _ m' _)
403 = decorate ns iname m == decorate ns iname m'
404 clauseFor m iname ns _ = False
406getHeadVars :: PTerm -> [Name]
407getHeadVars (PRef _ _ n) | implicitable n = [n]
408getHeadVars (PApp _ _ args) = concatMap getHeadVars (map getTm args)
409getHeadVars (PPair _ _ _ l r) = getHeadVars l ++ getHeadVars r
410getHeadVars (PDPair _ _ _ l t r) = getHeadVars l ++ getHeadVars t ++ getHeadVars t
411getHeadVars _ = []
413-- | Implicitly bind variables from the implementation head in method types
414impBind :: [(Name, PTerm)] -> PDecl -> PDecl
415impBind vs (PTy d ds syn fc opts n fc' t)
416 = PTy d ds syn fc opts n fc'
417 (doImpBind (filter (\(n, ty) -> n `notElem` boundIn t) vs) t)
418 where
419 doImpBind [] ty = ty
420 doImpBind ((n, argty) : ns) ty
421 = PPi impl n NoFC argty (doImpBind ns ty)
423 boundIn (PPi _ n _ _ sc) = n : boundIn sc
424 boundIn _ = []
426getTypeIn :: IState -> Name -> Type -> PTerm
427getTypeIn ist n (Bind x b sc)
428 | n == x = delab ist (binderTy b)
429 | otherwise = getTypeIn ist n (substV (P Ref x Erased) sc)
430getTypeIn ist n tm = Placeholder
432toImp fc n = pimp n (PRef fc [] n) True
434-- | Propagate interface parameters to method bodies, if they're not
435-- already there, and they are needed (i.e. appear in method's type)
436addParams :: [Name] -> PDecl -> PDecl
437addParams ps (PClauses fc opts n cs) = PClauses fc opts n (map addCParams cs)
438 where
439 addCParams (PClause fc n lhs ws rhs wb)
440 = PClause fc n (addTmParams (dropPs (allNamesIn lhs) ps) lhs) ws rhs wb
441 addCParams (PWith fc n lhs ws sc pn ds)
442 = PWith fc n (addTmParams (dropPs (allNamesIn lhs) ps) lhs) ws sc pn
443 (map (addParams ps) ds)
444 addCParams c = c
446 addTmParams ps (PRef fc hls n)
447 = PApp fc (PRef fc hls n) (map (toImp fc) ps)
448 addTmParams ps (PApp fc ap@(PRef fc' hls n) args)
449 = PApp fc ap (mergePs (map (toImp fc) ps) args)
450 addTmParams ps tm = tm
452 mergePs [] args = args
453 mergePs (p : ps) args
454 | isImplicit p,
455 pname p `notElem` map pname args
456 = p : mergePs ps args
457 where
458 isImplicit (PExp{}) = False
459 isImplicit _ = True
460 mergePs (p : ps) args
461 = mergePs ps args
463 -- Don't propagate a parameter if the name is rebound explicitly
464 dropPs :: [Name] -> [Name] -> [Name]
465 dropPs ns = filter (\x -> x `notElem` ns)
467addParams ps d = d
469-- | Check a given method definition is injective, if the interface info
470-- says it needs to be. Takes originally written decl and the one
471-- with name decoration, so we know which name to look up.
472checkInjectiveDef :: FC -> [(Name, (Bool, FnOpts, PTerm))] ->
473 (PDecl, PDecl) -> Idris ()
474checkInjectiveDef fc ns (PClauses _ _ n cs, PClauses _ _ elabn _)
475 | Just (True, _, _) <- clookup n ns
476 = do ist <- getIState
477 case lookupDefExact elabn (tt_ctxt ist) of
478 Just (CaseOp _ _ _ _ _ cdefs) ->
479 checkInjectiveCase ist (snd (cases_compiletime cdefs))
480 where
481 checkInjectiveCase ist (STerm tm)
482 = checkInjectiveApp ist (fst (unApply tm))
483 checkInjectiveCase _ _ = notifail
485 checkInjectiveApp ist (P (TCon _ _) n _) = return ()
486 checkInjectiveApp ist (P (DCon _ _ _) n _) = return ()
487 checkInjectiveApp ist (P Ref n _)
488 | Just True <- lookupInjectiveExact n (tt_ctxt ist) = return ()
489 checkInjectiveApp ist (P Ref n _) = notifail
490 checkInjectiveApp _ _ = notifail
492 notifail = ierror $ At fc (Msg (show n ++ " must be defined by a type or data constructor"))
494 clookup n [] = Nothing
495 clookup n ((n', d) : ds) | nsroot n == nsroot n' = Just d
496 | otherwise = Nothing
497checkInjectiveDef fc ns _ = return ()
499checkInjectiveArgs :: FC -> Name -> [Int] -> Maybe Type -> Idris ()
500checkInjectiveArgs fc n ds Nothing = return ()
501checkInjectiveArgs fc n ds (Just ty)
502 = do ist <- getIState
503 let (_, args) = unApply (instantiateRetTy ty)
504 ci 0 ist args
505 where
506 ci i ist (a : as) | i `elem` ds
507 = if isInj ist a then ci (i + 1) ist as
508 else tclift $ tfail (At fc (InvalidTCArg n a))
509 ci i ist (a : as) = ci (i + 1) ist as
510 ci i ist [] = return ()
512 isInj i (P Bound n _) = True
513 isInj i (P _ n _) = isConName n (tt_ctxt i)
514 isInj i (App _ f a) = isInj i f && isInj i a
515 isInj i (V _) = True
516 isInj i (Bind n b sc) = isInj i sc
517 isInj _ _ = True
519 instantiateRetTy (Bind n (Pi _ _ _ _) sc)
520 = substV (P Bound n Erased) (instantiateRetTy sc)
521 instantiateRetTy t = t