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