git.iko.soy/Idris-dev
on aeb032a help sign in
Idris-dev/src/Idris/Elab/Implementation.hs
488 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.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 checkInjectiveArgs fc n (interface_determiners ci) (lookupTyExact iname (tt_ctxt ist))
82 when (what /= ETypes && (not (null ds && not emptyinterface))) $ do
83 -- Add the parent implementation names to the privileged set
84 oldOpen <- addOpenImpl parents
86 let ips = zip (interface_params ci) ps
87 let ns = case n of
88 NS n ns' -> ns'
89 _ -> []
90 -- get the implicit parameters that need passing through to the
91 -- where block
92 wparams <- mapM (\p -> case p of
93 PApp _ _ args -> getWParams (map getTm args)
94 a@(PRef fc _ f) -> getWParams [a]
95 _ -> return []) ps
96 ist <- getIState
97 let pnames = nub $ map pname (concat (nub wparams)) ++
98 concatMap (namesIn [] ist) ps
100 let superInterfaceImplementations = map (substImplementation ips pnames) (interface_default_super_interfaces ci)
101 undefinedSuperInterfaceImplementations <- filterM (fmap not . isOverlapping ist) superInterfaceImplementations
102 mapM_ (rec_elabDecl info EAll info) undefinedSuperInterfaceImplementations
104 ist <- getIState
105 -- Bring variables in implementation head into scope when building the
106 -- dictionary
107 let headVars = nub $ concatMap getHeadVars ps
108 let (headVarTypes, ty)
109 = case lookupTyExact iname (tt_ctxt ist) of
110 Just ty -> (map (\n -> (n, getTypeIn ist n ty)) headVars, ty)
111 _ -> (zip headVars (repeat Placeholder), Erased)
113 let impps = getImpParams ist (interface_impparams ci)
114 (snd (unApply (substRetTy ty)))
115 let iimpps = zip (interface_impparams ci) impps
117 logElab 5 $ "ImpPS: " ++ show impps ++ " --- " ++ show iimpps
118 logElab 5 $ "Head var types " ++ show headVarTypes ++ " from " ++ show ty
120 let all_meths = map (nsroot . fst) (interface_methods ci)
121 let mtys = map (\ (n, (inj, op, t)) ->
122 let t_in = substMatchesShadow (iimpps ++ ips) pnames t
123 mnamemap =
124 map (\n -> (n, PApp fc (PRef fc [] (decorate ns iname n))
125 (map (toImp fc) headVars)))
126 all_meths
127 t' = substMatchesShadow mnamemap pnames t_in in
128 (decorate ns iname n,
129 op, coninsert cs pextra t', t'))
130 (interface_methods ci)
132 logElab 5 (show (mtys, (iimpps ++ ips)))
133 logElab 5 ("Before defaults: " ++ show ds ++ "\n" ++ show (map fst (interface_methods ci)))
134 let ds_defs = insertDefaults ist iname (interface_defaults ci) ns ds
135 logElab 3 ("After defaults: " ++ show ds_defs ++ "\n")
137 let ds' = reorderDefs (map fst (interface_methods ci)) ds_defs
138 logElab 1 ("Reordered: " ++ show ds' ++ "\n")
140 mapM_ (warnMissing ds' ns iname) (map fst (interface_methods ci))
141 mapM_ (checkInInterface (map fst (interface_methods ci))) (concatMap defined ds')
142 let wbTys = map mkTyDecl mtys
143 let wbVals_orig = map (decorateid (decorate ns iname)) ds'
144 ist <- getIState
145 let wbVals = map (expandParamsD False ist id pextra (map methName mtys)) wbVals_orig
147 logElab 3 $ "Method types " ++ showSep "\n" (map (show . showDeclImp verbosePPOption . mkTyDecl) mtys)
148 logElab 3 $ "Implementation is " ++ show ps ++ " implicits " ++ show (concat (nub wparams))
150 let lhsImps = map (\n -> pimp n (PRef fc [] n) True) headVars
152 let lhs = PApp fc (PRef fc [] iname) (lhsImps ++ map (toExp .fst) pextra)
153 let rhs = PApp fc (PRef fc [] (implementationCtorName ci))
154 (map (pexp . (mkMethApp lhsImps)) mtys)
156 logElab 5 $ "Implementation LHS " ++ show totopts ++ "\n" ++ showTmImpls lhs ++ " " ++ show headVars
157 logElab 5 $ "Implementation RHS " ++ show rhs
159 push_estack iname True
160 logElab 3 ("Method types: " ++ show wbTys)
161 logElab 3 ("Method bodies (before params): " ++ show wbVals_orig)
162 logElab 3 ("Method bodies: " ++ show wbVals)
164 let idecls = [PClauses fc totopts iname
165 [PClause fc iname lhs [] rhs []]]
167 mapM_ (rec_elabDecl info EAll info) (map (impBind headVarTypes) wbTys)
168 mapM_ (rec_elabDecl info EAll info) idecls
170 ctxt <- getContext
171 let ifn_ty = case lookupTyExact iname ctxt of
172 Just t -> t
173 Nothing -> error "Can't happen (interface constructor)"
174 let ifn_is = case lookupCtxtExact iname (idris_implicits ist) of
175 Just t -> t
176 Nothing -> []
177 let prop_params = getParamsInType ist [] ifn_is ifn_ty
179 logElab 3 $ "Propagating parameters to methods: "
180 ++ show (iname, prop_params)
182 let wbVals' = map (addParams prop_params) wbVals
184 logElab 5 ("Elaborating method bodies: " ++ show wbVals')
185 mapM_ (rec_elabDecl info EAll info) wbVals'
187 mapM_ (checkInjectiveDef fc (interface_methods ci)) (zip ds' wbVals')
189 pop_estack
191 setOpenImpl oldOpen
192-- totalityCheckBlock
194 addIBC (IBCImplementation intImpl (isNothing expn) n iname)
196 where
197 getImpParams ist = zipWith (\n tm -> delab ist tm)
199 intImpl = case ps of
200 [PConstant NoFC (AType (ATInt ITNative))] -> True
201 _ -> False
203 mkiname n' ns ps' expn' =
204 case expn' of
205 Nothing -> case ns of
206 [] -> SN (sImplementationN n' (map show ps'))
207 m -> sNS (SN (sImplementationN n' (map show ps'))) m
208 Just nm -> nm
210 substImplementation ips pnames (PImplementation doc argDocs syn _ cs parents acc opts n nfc ps pextra t expn ds)
211 = PImplementation doc argDocs syn fc cs parents acc opts n nfc
212 (map (substMatchesShadow ips pnames) ps)
213 pextra
214 (substMatchesShadow ips pnames t) expn ds
216 isOverlapping i (PImplementation doc argDocs syn _ _ _ _ _ n nfc ps pextra t expn _)
217 = case lookupCtxtName n (idris_interfaces i) of
218 [(n, ci)] -> let iname = (mkiname n (namespace info) ps expn) in
219 case lookupTy iname (tt_ctxt i) of
220 [] -> elabFindOverlapping i ci iname syn t
221 (_:_) -> return True
222 _ -> return False -- couldn't find interface, just let elabImplementation fail later
224 elabFindOverlapping i ci iname syn t
225 = do ty' <- addUsingConstraints syn fc t
226 -- TODO think: something more in info?
227 ty' <- implicit info syn iname ty'
228 let ty = addImpl [] i ty'
229 ctxt <- getContext
230 (ElabResult tyT _ _ ctxt' newDecls highlights newGName, _) <-
231 tclift $ elaborate (constraintNS info) ctxt (idris_datatypes i) (idris_name i) iname (TType (UVal 0)) initEState
232 (errAt "type of " iname Nothing (erun fc (build i info ERHS [] iname ty)))
233 setContext ctxt'
234 processTacticDecls info newDecls
235 sendHighlighting highlights
236 updateIState $ \i -> i { idris_name = newGName }
238 ctxt <- getContext
239 (cty, _) <- recheckC (constraintNS info) fc id [] tyT
240 let nty = normalise ctxt [] cty
241 return $ any (isJust . findOverlapping i (interface_determiners ci) (delab i nty)) (map fst $ interface_implementations ci)
243 findOverlapping i dets t n
244 | SN (ParentN _ _) <- n = Nothing
245 | Just opts <- lookupCtxtExact n (idris_flags i),
246 OverlappingDictionary `elem` opts = Nothing
247 | otherwise
248 = case lookupTy n (tt_ctxt i) of
249 [t'] -> let tret = getRetType t
250 tret' = getRetType (delab i t') in
251 case matchArgs i dets tret' tret of
252 Right _ -> Just tret'
253 Left _ -> case matchArgs i dets tret tret' of
254 Right _ -> Just tret'
255 Left _ -> Nothing
256 _ -> Nothing
257 overlapping t' = tclift $ tfail (At fc (Msg $
258 "Overlapping implementation: " ++ show t' ++ " already defined"))
259 getRetType (PPi _ _ _ _ sc) = getRetType sc
260 getRetType t = t
262 matchArgs i dets x y =
263 let x' = keepDets dets x
264 y' = keepDets dets y in
265 matchClause i x' y'
267 keepDets dets (PApp fc f args)
268 = PApp fc f $ let a' = zip [0..] args in
269 map snd (filter (\(i, _) -> i `elem` dets) a')
270 keepDets dets t = t
272 methName (n, _, _, _) = n
273 toExp n = pexp (PRef fc [] n)
275 mkMethApp ps (n, _, _, ty)
276 = lamBind 0 ty (papp fc (PRef fc [] n)
277 (ps ++ map (toExp . fst) pextra ++ methArgs 0 ty))
279 lamBind i (PPi (Constraint _ _ _) _ _ _ sc) sc'
280 = PLam fc (sMN i "meth") NoFC Placeholder (lamBind (i+1) sc sc')
281 lamBind i (PPi _ n _ ty sc) sc'
282 = PLam fc (sMN i "meth") NoFC Placeholder (lamBind (i+1) sc sc')
283 lamBind i _ sc = sc
284 methArgs i (PPi (Imp _ _ _ _ _ _) n _ ty sc)
285 = PImp 0 True [] n (PRef fc [] (sMN i "meth")) : methArgs (i+1) sc
286 methArgs i (PPi (Exp _ _ _ _) n _ ty sc)
287 = PExp 0 [] (sMN 0 "marg") (PRef fc [] (sMN i "meth")) : methArgs (i+1) sc
288 methArgs i (PPi (Constraint _ _ _) n _ ty sc)
289 = PConstraint 0 [] (sMN 0 "marg") (PResolveTC fc) : methArgs (i+1) sc
290 methArgs i _ = []
292 papp fc f [] = f
293 papp fc f as = PApp fc f as
295 getWParams [] = return []
296 getWParams (p : ps)
297 | PRef _ _ n <- p
298 = do ps' <- getWParams ps
299 ctxt <- getContext
300 case lookupP n ctxt of
301 [] -> return (pimp n (PRef fc [] n) True : ps')
302 _ -> return ps'
303 getWParams (_ : ps) = getWParams ps
305 decorate ns iname (NS (UN nm) s)
306 = NS (SN (WhereN 0 iname (SN (MethodN (UN nm))))) ns
307 decorate ns iname nm
308 = NS (SN (WhereN 0 iname (SN (MethodN nm)))) ns
310 mkTyDecl (n, op, t, _)
311 = PTy emptyDocstring [] syn fc op n NoFC
312 (mkUniqueNames [] [] t)
314 conbind :: [(Name, PTerm)] -> PTerm -> PTerm
315 conbind ((c,ty) : ns) x = PPi constraint c NoFC ty (conbind ns x)
316 conbind [] x = x
318 extrabind :: [(Name, PTerm)] -> PTerm -> PTerm
319 extrabind ((c,ty) : ns) x = PPi expl c NoFC ty (extrabind ns x)
320 extrabind [] x = x
322 coninsert :: [(Name, PTerm)] -> [(Name, PTerm)] -> PTerm -> PTerm
323 coninsert cs ex (PPi p@(Imp _ _ _ _ _ _) n fc t sc) = PPi p n fc t (coninsert cs ex sc)
324 coninsert cs ex sc = conbind cs (extrabind ex sc)
326 -- Reorder declarations to be in the same order as defined in the
327 -- interface declaration (important so that we insert default definitions
328 -- in the right place, and so that dependencies between methods are
329 -- respected)
330 reorderDefs :: [Name] -> [PDecl] -> [PDecl]
331 reorderDefs ns [] = []
332 reorderDefs [] ds = ds
333 reorderDefs (n : ns) ds = case pick n [] ds of
334 Just (def, ds') -> def : reorderDefs ns ds'
335 Nothing -> reorderDefs ns ds
337 pick n acc [] = Nothing
338 pick n acc (def@(PClauses _ _ cn cs) : ds)
339 | nsroot n == nsroot cn = Just (def, acc ++ ds)
340 pick n acc (d : ds) = pick n (acc ++ [d]) ds
342 insertDefaults :: IState -> Name ->
343 [(Name, (Name, PDecl))] -> [T.Text] ->
344 [PDecl] -> [PDecl]
345 insertDefaults i iname [] ns ds = ds
346 insertDefaults i iname ((n,(dn, clauses)) : defs) ns ds
347 = insertDefaults i iname defs ns (insertDef i n dn clauses ns iname ds)
349 insertDef i meth def clauses ns iname decls
350 | not $ any (clauseFor meth iname ns) decls
351 = let newd = expandParamsD False i (\n -> meth) [] [def] clauses in
352 -- trace (show newd) $
353 decls ++ [newd]
354 | otherwise = decls
356 warnMissing decls ns iname meth
357 | not $ any (clauseFor meth iname ns) decls
358 = iWarn fc . text $ "method " ++ show meth ++ " not defined"
359 | otherwise = return ()
361 checkInInterface ns meth
362 | any (eqRoot meth) ns = return ()
363 | otherwise = tclift $ tfail (At fc (Msg $
364 show meth ++ " not a method of interface " ++ show n))
366 eqRoot x y = nsroot x == nsroot y
368 clauseFor m iname ns (PClauses _ _ m' _)
369 = decorate ns iname m == decorate ns iname m'
370 clauseFor m iname ns _ = False
372getHeadVars :: PTerm -> [Name]
373getHeadVars (PRef _ _ n) | implicitable n = [n]
374getHeadVars (PApp _ _ args) = concatMap getHeadVars (map getTm args)
375getHeadVars (PPair _ _ _ l r) = getHeadVars l ++ getHeadVars r
376getHeadVars (PDPair _ _ _ l t r) = getHeadVars l ++ getHeadVars t ++ getHeadVars t
377getHeadVars _ = []
379-- | Implicitly bind variables from the implementation head in method types
380impBind :: [(Name, PTerm)] -> PDecl -> PDecl
381impBind vs (PTy d ds syn fc opts n fc' t)
382 = PTy d ds syn fc opts n fc'
383 (doImpBind (filter (\(n, ty) -> n `notElem` boundIn t) vs) t)
384 where
385 doImpBind [] ty = ty
386 doImpBind ((n, argty) : ns) ty
387 = PPi impl n NoFC argty (doImpBind ns ty)
389 boundIn (PPi _ n _ _ sc) = n : boundIn sc
390 boundIn _ = []
392getTypeIn :: IState -> Name -> Type -> PTerm
393getTypeIn ist n (Bind x b sc)
394 | n == x = delab ist (binderTy b)
395 | otherwise = getTypeIn ist n (substV (P Ref x Erased) sc)
396getTypeIn ist n tm = Placeholder
398toImp fc n = pimp n (PRef fc [] n) True
400-- | Propagate interface parameters to method bodies, if they're not
401-- already there, and they are needed (i.e. appear in method's type)
402addParams :: [Name] -> PDecl -> PDecl
403addParams ps (PClauses fc opts n cs) = PClauses fc opts n (map addCParams cs)
404 where
405 addCParams (PClause fc n lhs ws rhs wb)
406 = PClause fc n (addTmParams (dropPs (allNamesIn lhs) ps) lhs) ws rhs wb
407 addCParams (PWith fc n lhs ws sc pn ds)
408 = PWith fc n (addTmParams (dropPs (allNamesIn lhs) ps) lhs) ws sc pn
409 (map (addParams ps) ds)
410 addCParams c = c
412 addTmParams ps (PRef fc hls n)
413 = PApp fc (PRef fc hls n) (map (toImp fc) ps)
414 addTmParams ps (PApp fc ap@(PRef fc' hls n) args)
415 = PApp fc ap (mergePs (map (toImp fc) ps) args)
416 addTmParams ps tm = tm
418 mergePs [] args = args
419 mergePs (p : ps) args
420 | isImplicit p,
421 pname p `notElem` map pname args
422 = p : mergePs ps args
423 where
424 isImplicit (PExp{}) = False
425 isImplicit _ = True
426 mergePs (p : ps) args
427 = mergePs ps args
429 -- Don't propagate a parameter if the name is rebound explicitly
430 dropPs :: [Name] -> [Name] -> [Name]
431 dropPs ns = filter (\x -> x `notElem` ns)
433addParams ps d = d
435-- | Check a given method definition is injective, if the interface info
436-- says it needs to be. Takes originally written decl and the one
437-- with name decoration, so we know which name to look up.
438checkInjectiveDef :: FC -> [(Name, (Bool, FnOpts, PTerm))] ->
439 (PDecl, PDecl) -> Idris ()
440checkInjectiveDef fc ns (PClauses _ _ n cs, PClauses _ _ elabn _)
441 | Just (True, _, _) <- clookup n ns
442 = do ist <- getIState
443 case lookupDefExact elabn (tt_ctxt ist) of
444 Just (CaseOp _ _ _ _ _ cdefs) ->
445 checkInjectiveCase ist (snd (cases_compiletime cdefs))
446 where
447 checkInjectiveCase ist (STerm tm)
448 = checkInjectiveApp ist (fst (unApply tm))
449 checkInjectiveCase _ _ = notifail
451 checkInjectiveApp ist (P (TCon _ _) n _) = return ()
452 checkInjectiveApp ist (P (DCon _ _ _) n _) = return ()
453 checkInjectiveApp ist (P Ref n _)
454 | Just True <- lookupInjectiveExact n (tt_ctxt ist) = return ()
455 checkInjectiveApp ist (P Ref n _) = notifail
456 checkInjectiveApp _ _ = notifail
458 notifail = ierror $ At fc (Msg (show n ++ " must be defined by a type or data constructor"))
460 clookup n [] = Nothing
461 clookup n ((n', d) : ds) | nsroot n == nsroot n' = Just d
462 | otherwise = Nothing
463checkInjectiveDef fc ns _ = return ()
465checkInjectiveArgs :: FC -> Name -> [Int] -> Maybe Type -> Idris ()
466checkInjectiveArgs fc n ds Nothing = return ()
467checkInjectiveArgs fc n ds (Just ty)
468 = do ist <- getIState
469 let (_, args) = unApply (instantiateRetTy ty)
470 ci 0 ist args
471 where
472 ci i ist (a : as) | i `elem` ds
473 = if isInj ist a then ci (i + 1) ist as
474 else tclift $ tfail (At fc (InvalidTCArg n a))
475 ci i ist (a : as) = ci (i + 1) ist as
476 ci i ist [] = return ()
478 isInj i (P Bound n _) = True
479 isInj i (P _ n _) = isConName n (tt_ctxt i)
480 isInj i (App _ f a) = isInj i f && isInj i a
481 isInj i (V _) = True
482 isInj i (Bind n b@(Pi{}) sc) = isInj i (binderTy b) && isInj i sc
483 isInj i (Bind n b sc) = False
484 isInj _ _ = True
486 instantiateRetTy (Bind n (Pi _ _ _ _) sc)
487 = substV (P Bound n Erased) (instantiateRetTy sc)
488 instantiateRetTy t = t