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