git.iko.soy/Idris-dev
on master help sign in
Idris-dev/src/Idris/Elab/Interface.hs
449 lines 21 kB history raw
1{-|
2Module : Idris.Elab.Interface
3Description : Code to elaborate interfaces.
5License : BSD3
6Maintainer : The Idris Community.
7-}
8{-# LANGUAGE PatternGuards #-}
9{-# OPTIONS_GHC -fwarn-missing-signatures #-}
10module Idris.Elab.Interface(elabInterface) where
12import Idris.AbsSyntax
13import Idris.Core.Evaluate
14import Idris.Core.TT
15import Idris.Delaborate
16import Idris.Docstrings
17import Idris.Elab.Data
18import Idris.Elab.Utils
19import Idris.Error
20import Idris.Output (sendHighlighting)
22import Prelude hiding (id, (.))
24import Control.Category
25import Control.Monad
26import Data.Generics.Uniplate.Data (transform)
27import Data.List
28import Data.Maybe
29import qualified Data.Set as S
31data MArgTy = IA Name | EA Name | CA deriving Show
33elabInterface :: ElabInfo
34 -> SyntaxInfo
35 -> Docstring (Either Err PTerm)
36 -> ElabWhat
37 -> FC
38 -> [(Name, PTerm)] -- ^ Superclass constraints
39 -> Name
40 -> FC
41 -> [(Name, FC, PTerm)] -- ^ Parameters
42 -> [(Name, Docstring (Either Err PTerm))]
43 -> [(Name, FC)] -- ^ determining params
44 -> [PDecl] -- ^ interface body
45 -> Maybe (Name, FC) -- ^ implementation ctor name and location
46 -> Docstring (Either Err PTerm) -- ^ implementation ctor docs
47 -> Idris ()
48elabInterface info_in syn_in doc what fc constraints tn tnfc ps pDocs fds ds mcn cd
49 = do let cn = fromMaybe (SN (ImplementationCtorN tn)) (fst <$> mcn)
50 let constraint = PApp fc (PRef fc [] tn)
51 (map (pexp . PRef fc []) (map (\(n, _, _) -> n) ps))
53 let syn =
54 syn_in { using = addToUsing (using syn_in)
55 [(pn, pt) | (pn, _, pt) <- ps]
56 }
58 -- Calculate implicit parameters
59 ist <- getIState
60 let impps_ns = nub $ map (\n -> (n, emptyFC, Placeholder)) $
61 concatMap (implicitNamesIn [] ist)
62 (map (\ (_,_,x) -> x) ps)
63 let impps = filter (\ (n, _, _) ->
64 n `notElem` (map (\ (n, _, _) -> n) ps)) impps_ns
66 let tty = impbind (map (\(n, _, ty) -> (n, ty)) impps) $
67 pibind (map (\(n, _, ty) -> (n, ty)) ps) (PType fc)
69 logElab 5 $ "Implicit parameters are " ++ show impps
70 logElab 5 $ "Interface type is " ++ showTmImpls tty
72 -- build data declaration
73 let mdecls = filter tydecl ds -- method declarations
74 let idecls = filter impldecl ds -- default super interface implementation declarations
75 mapM_ checkDefaultSuperInterfaceImplementation idecls
76 let mnames = map getMName mdecls
77 let fullmnames = map getFullMName mdecls
78 ist <- getIState
79 let constraintNames = nub $
80 concatMap (namesIn [] ist) (map snd constraints)
82 mapM_ (checkConstraintName (map (\(x, _, _) -> x) ps)) constraintNames
84 let pre_ddecl = PLaterdecl tn NoFC tty
85 -- Elaborate the interface header, as long as we haven't done it
86 -- in an earlier pass
87 when (what /= EDefns) $
88 elabData info (syn { no_imp = no_imp syn ++ mnames,
89 imp_methods = mnames }) doc pDocs fc [] pre_ddecl
90 -- Continue only if we're not in the first pass of a mutual block
91 when (what /= ETypes) $ do
92 dets <- findDets tn (map fst fds)
94 logElab 3 $ "Building methods " ++ show fullmnames
95 ims <- mapM (tdecl impps mnames) mdecls
96 defs <- mapM (defdecl (map (\ (x,y,z) -> z) ims) constraint)
97 (filter clause ds)
98 let imethods = map (\ (x, y, z) -> y) ims
99 let defaults = map (\ (x, (y, z)) -> (x,y)) defs
101 addInterface tn (CI cn (map nodoc imethods) defaults idecls
102 (map (\(n, _, _) -> n) impps)
103 (map (\(n, _, _) -> n) ps)
104 (map snd constraints)
105 [] dets)
107 -- for each constraint, build a top level function to chase it
108 -- elaborate types now, bodies later (after we've done the constructor
109 -- of the interface)
110 cfns <- mapM (cfun cn constraint syn (map fst imethods)) constraints
111 let (cfnTyDecls, cfnDefs) = unzip cfns
112 mapM_ (rec_elabDecl info EAll info) cfnTyDecls
114 -- for each method, build a top level function
115 -- 'tfun' builds appropriate implicits for the constructor
116 -- declaration
117 fns <- mapM (tfun cn constraint (syn { imp_methods = mnames }) -- mnames })
118 (map fst imethods)) imethods
119 let (fnTyDecls, fnDefs) = unzip fns
120 mapM_ (rec_elabDecl info EAll info) fnTyDecls
122 elabMethTys <- mapM getElabMethTy fullmnames
124 logElab 3 $ "Method types:\n" ++ showSep "\n" (map showTmImpls elabMethTys)
126 let cpos = map (\ (n, ty) -> (n, findConstraint ty))
127 (zip fullmnames elabMethTys)
128 logElab 5 $ "Constraint pos: " ++ show cpos
130 -- Method types to store in the IState, taken from the elaborated
131 -- types with the parameter removed
132 let storemeths = map (mkMethTy True cpos) (zip fullmnames elabMethTys)
133 updateIMethods tn storemeths
135 -- build implementation constructor type
136 let cty = impbind [(pn, pt) | (pn, _, pt) <- impps ++ ps] $
137 conbind constraints $
138 pibind (map (mkMethTy False cpos) (zip fullmnames elabMethTys))
139 constraint
140 logElab 3 $ "Constraint constructor type: " ++ showTmImpls cty
142 let cons = [(cd, pDocs ++ mapMaybe memberDocs ds, cn, NoFC, cty, fc, [])]
143 let ddecl = PDatadecl tn NoFC tty cons
145 logElab 10 $ "Interface " ++ show (showDImp verbosePPOption ddecl)
148 -- Elaborate the data declaration
149 elabData info (syn { no_imp = no_imp syn ++ mnames,
150 imp_methods = [] }) doc pDocs fc [] ddecl
153 logElab 5 $ "Function types " ++ show fnTyDecls
154 logElab 5 $ "Method types now: " ++ show imethods
156 -- Elaborate the the top level constraint chasers
157 -- (Types elaborated earlier)
158 mapM_ (rec_elabDecl info EAll info) cfnDefs
159 -- Elaborate the the top level method bodies
160 mapM_ (rec_elabDecl info EAll info) fnDefs
162 -- Flag all the top level data declarations as injective
163 mapM_ (\n -> do setInjectivity n True
164 addIBC (IBCInjective n True))
165 (map fst (filter (\(_, (inj, _, _, _, _)) -> inj) imethods))
167 -- add the default definitions
168 mapM_ (rec_elabDecl info EAll info) (concatMap (snd.snd) defs)
169 addIBC (IBCInterface tn)
171 sendHighlighting $ S.fromList $
172 [(FC' tnfc, AnnName tn Nothing Nothing Nothing)] ++
173 [(FC' pnfc, AnnBoundName pn False) | (pn, pnfc, _) <- ps] ++
174 [(FC' fdfc, AnnBoundName fc False) | (fc, fdfc) <- fds] ++
175 maybe [] (\(conN, conNFC) -> [(FC' conNFC, AnnName conN Nothing Nothing Nothing)]) mcn
177 where
178 info = info_in { noCaseLift = tn : noCaseLift info_in }
180 getElabMethTy :: Name -> Idris PTerm
181 getElabMethTy n = do ist <- getIState
182 let impls = case lookupCtxtExact n (idris_implicits ist) of
183 Just i -> i
184 Nothing -> []
185 case lookupTyExact n (tt_ctxt ist) of
186 Just ty -> return (delabTy' ist impls [] ty False False False)
187 Nothing -> tclift $ tfail (At fc (InternalMsg "Can't happen, elabMethTy"))
189 -- Find the argument position of the current interface in a method type
190 -- (we'll use this to update the elaborated top level method types before
191 -- building a data declaration
192 findConstraint :: PTerm -> Int
193 findConstraint = findPos 0
194 where
195 findPos i (PPi _ _ _ (PRef _ _ n) sc)
196 | n == tn = i
197 findPos i (PPi _ _ _ (PApp _ (PRef _ _ n) _) sc)
198 | n == tn = i
199 findPos i (PPi _ _ _ ty sc) = findPos (i + 1) sc
200 findPos i _ = -1 -- Can't happen!
202 -- Make the method component of the constructor type by taking the
203 -- elaborated top level method and removing the implicits/constraint
204 mkMethTy :: Bool -> [(Name, Int)] -> (Name, PTerm) -> (Name, PTerm)
205 mkMethTy keepns cpos (n, tm)
206 = (if keepns then n else nsroot n, dropPis num (mapPT dropImp tm))
207 where
208 num = case lookup n cpos of
209 Just i -> i + 1
210 Nothing -> 0
212 dropPis n (PPi _ _ _ _ sc) | n > 0 = dropPis (n - 1) sc
213 dropPis _ tm = tm
215 dropImp (PApp fc (PRef fcr fcs n) args)
216 | Just pos <- lookup n cpos
217 = PApp fc (PRef fcr fcs (nsroot n))
218 (filter notConstr (drop (pos + 1) args))
219 dropImp (PApp fc f args)
220 = PApp fc f (filter notConstr args)
221 dropImp tm = tm
223 notConstr (PConstraint {}) = False
224 notConstr _ = True
226 nodoc (n, (inj, _, _, o, t)) = (n, (inj, o, t))
228 pibind [] x = x
229 pibind ((n, ty): ns) x = PPi expl n NoFC ty (pibind ns (chkUniq ty x))
231 -- To make sure the type constructor of the interface is in the appropriate
232 -- uniqueness hierarchy
233 chkUniq u@(PUniverse _ _) (PType _) = u
234 chkUniq (PUniverse _ l) (PUniverse _ r) = PUniverse NoFC (min l r)
235 chkUniq (PPi _ _ _ _ sc) t = chkUniq sc t
236 chkUniq _ t = t
238 -- TODO: probably should normalise
239 checkDefaultSuperInterfaceImplementation :: PDecl -> Idris ()
240 checkDefaultSuperInterfaceImplementation (PImplementation _ _ _ fc cs _ _ _ n _ ps _ _ _ _)
241 = do when (not $ null cs) . tclift
242 $ tfail (At fc (Msg "Default super interface implementations can't have constraints."))
243 i <- getIState
244 let isConstrained = any (checkConstrained i n (map pexp ps)) (map snd constraints)
245 when (not isConstrained) . tclift
246 $ tfail (At fc (Msg "Default implementations must be for a super interface constraint on the containing interface."))
247 return ()
248 where
249 -- First, Check that interface "constraint" has same name & args as default implementation name & args (not checking FC)
250 -- If not the case, recursively lookup in context for parent interface & recheck the same with parent constraints
251 checkConstrained i n args constraint =
252 if (n == cn && args == cargs)
253 then True
254 else any (id) (map (checkConstrained i n args) parentConstraints)
255 where
256 PApp _ (PRef _ _ cn) cargs = constraint
257 parentConstraints = concatMap interface_constraints (lookupCtxt cn (idris_interfaces i))
259 checkConstraintName :: [Name] -> Name -> Idris ()
260 checkConstraintName bound cname
261 | cname `notElem` bound
262 = tclift $ tfail (At fc (Msg $ "Name " ++ show cname ++
263 " is not bound in interface " ++ show tn
264 ++ " " ++ showSep " " (map show bound)))
265 | otherwise = return ()
267 impbind :: [(Name, PTerm)] -> PTerm -> PTerm
268 impbind [] x = x
269 impbind ((n, ty): ns) x = PPi impl n NoFC ty (impbind ns x)
271 conbind :: [(Name, PTerm)] -> PTerm -> PTerm
272 conbind ((c, ty) : ns) x = PPi constraint c NoFC ty (conbind ns x)
273 conbind [] x = x
275 getMName (PTy _ _ _ _ _ n nfc _) = nsroot n
276 getMName (PData _ _ _ _ _ (PLaterdecl n nfc _)) = nsroot n
278 getFullMName (PTy _ _ _ _ _ n nfc _) = n
279 getFullMName (PData _ _ _ _ _ (PLaterdecl n nfc _)) = n
281 tdecl impps allmeths (PTy doc _ syn _ o n nfc t)
282 = do t' <- implicit' info syn (map (\(n, _, _) -> n) (impps ++ ps) ++ allmeths) n t
283 logElab 1 $ "Method " ++ show n ++ " : " ++ showTmImpls t'
284 return ( (n, (toExp (map (\(pn, _, _) -> pn) ps) Exp t')),
285 (n, (False, nfc, doc, o, (toExp (map (\(pn, _, _) -> pn) ps)
286 (\ l s p r -> Imp l s p Nothing True r) t'))),
287 (n, (nfc, syn, o, t) ) )
288 tdecl impps allmeths (PData doc _ syn _ _ (PLaterdecl n nfc t))
289 = do let o = []
290 t' <- implicit' info syn (map (\(n, _, _) -> n) ps ++ allmeths) n t
291 logElab 2 $ "Data method " ++ show n ++ " : " ++ showTmImpls t'
292 return ( (n, (toExp (map (\(pn, _, _) -> pn) ps) Exp t')),
293 (n, (True, nfc, doc, o, (toExp (map (\(pn, _, _) -> pn) ps)
294 (\ l s p r -> Imp l s p Nothing True r) t'))),
295 (n, (nfc, syn, o, t) ) )
296 tdecl impps allmeths (PData doc _ syn _ _ _)
297 = ierror $ At fc (Msg "Data definitions not allowed in an interface declaration")
298 tdecl _ _ _ = ierror $ At fc (Msg "Not allowed in an interface declaration")
300 -- Create default definitions
301 defdecl mtys c d@(PClauses fc opts n cs) =
302 case lookup n mtys of
303 Just (nfc, syn, o, ty) ->
304 do let ty' = insertConstraint c (map fst mtys) ty
305 let ds = map (decorateid defaultdec)
306 [PTy emptyDocstring [] syn fc [] n nfc ty',
307 PClauses fc (o ++ opts) n cs]
308 logElab 1 (show ds)
309 return (n, ((defaultdec n, ds!!1), ds))
310 _ -> ierror $ At fc (Msg (show n ++ " is not a method"))
311 defdecl _ _ _ = ifail "Can't happen (defdecl)"
313 defaultdec (UN n) = sUN ("default#" ++ str n)
314 defaultdec (NS n ns) = NS (defaultdec n) ns
316 tydecl (PTy{}) = True
317 tydecl (PData _ _ _ _ _ _) = True
318 tydecl _ = False
319 impldecl (PImplementation{}) = True
320 impldecl _ = False
321 clause (PClauses{}) = True
322 clause _ = False
324 -- Generate a function for chasing a dictionary constraint
325 cfun :: Name -> PTerm -> SyntaxInfo -> [a] -> (Name, PTerm) -> Idris (PDecl, PDecl)
326 cfun cn c syn all (cnm, con)
327 = do let cfn = SN (ParentN cn (txt (show con)))
328 let mnames = take (length all) $ map (\x -> sMN x "meth") [0..]
329 let capp = PApp fc (PRef fc [] cn) (map (pexp . PRef fc []) mnames)
330 let lhs = PApp fc (PRef fc [] cfn) [pconst capp]
331 let rhs = PResolveTC (fileFC "HACK")
332 let ty = PPi constraint cnm NoFC c con
333 logElab 2 ("Dictionary constraint: " ++ showTmImpls ty)
334 logElab 2 (showTmImpls lhs ++ " = " ++ showTmImpls rhs)
335 i <- getIState
336 let conn = case con of
337 PRef _ _ n -> n
338 PApp _ (PRef _ _ n) _ -> n
339 let conn' = case lookupCtxtName conn (idris_interfaces i) of
340 [(n, _)] -> n
341 _ -> conn
342 addImplementation False True conn' cfn
343 addIBC (IBCImplementation False True conn' cfn)
344-- iputStrLn ("Added " ++ show (conn, cfn, ty))
345 return (PTy emptyDocstring [] syn fc [] cfn NoFC ty,
346 PClauses fc [Inlinable, Dictionary] cfn [PClause fc cfn lhs [] rhs []])
348 -- | Generate a top level function which looks up a method in a given
349 -- dictionary (this is inlinable, always)
350 tfun :: Name -- ^ The name of the interface
351 -> PTerm -- ^ A constraint for the interface, to be inserted under the implicit bindings
352 -> SyntaxInfo -> [Name] -- ^ All the method names
353 -> (Name, (Bool, FC, Docstring (Either Err PTerm), FnOpts, PTerm))
354 -- ^ The present declaration
355 -> Idris (PDecl, PDecl)
356 tfun cn c syn all (m, (isdata, mfc, doc, o, ty))
357 = do let ty' = expandMethNS syn (insertConstraint c all ty)
358 let mnames = take (length all) $ map (\x -> sMN x "meth") [0..]
359 let capp = PApp fc (PRef fc [] cn) (map (pexp . PRef fc []) mnames)
360 let margs = getMArgs ty
361 let anames = map (\x -> sMN x "arg") [0..]
362 let lhs = PApp fc (PRef fc [] m) (pconst capp : lhsArgs margs anames)
363 let rhs = PApp fc (getMeth mnames all m) (rhsArgs margs anames)
364 logElab 2 ("Top level type: " ++ showTmImpls ty')
365 logElab 1 (show (m, ty', capp, margs))
366 logElab 2 ("Definition: " ++ showTmImpls lhs ++ " = " ++ showTmImpls rhs)
367 return (PTy doc [] syn fc o m mfc ty',
368 PClauses fc [Inlinable] m [PClause fc m lhs [] rhs []])
370 getMArgs (PPi (Imp _ _ _ _ _ _) n _ ty sc) = IA n : getMArgs sc
371 getMArgs (PPi (Exp _ _ _ _) n _ ty sc) = EA n : getMArgs sc
372 getMArgs (PPi (Constraint _ _ _) n _ ty sc) = CA : getMArgs sc
373 getMArgs _ = []
375 getMeth :: [Name] -> [Name] -> Name -> PTerm
376 getMeth (m:ms) (a:as) x | x == a = PRef fc [] m
377 | otherwise = getMeth ms as x
379 lhsArgs (EA _ : xs) (n : ns) = [] -- pexp (PRef fc n) : lhsArgs xs ns
380 lhsArgs (IA n : xs) ns = pimp n (PRef fc [] n) False : lhsArgs xs ns
381 lhsArgs (CA : xs) ns = lhsArgs xs ns
382 lhsArgs [] _ = []
384 rhsArgs (EA _ : xs) (n : ns) = [] -- pexp (PRef fc n) : rhsArgs xs ns
385 rhsArgs (IA n : xs) ns = pexp (PRef fc [] n) : rhsArgs xs ns
386 rhsArgs (CA : xs) ns = pconst (PResolveTC fc) : rhsArgs xs ns
387 rhsArgs [] _ = []
389 -- Add the top level constraint. Put it first - elaboration will resolve
390 -- the order of the implicits if there are dependencies.
391 -- Also ensure the dictionary is used for lookup of any methods that
392 -- are used in the type
393 insertConstraint :: PTerm -> [Name] -> PTerm -> PTerm
394 insertConstraint c all sc
395 = let dictN = sMN 0 "__interface" in
396 PPi (constraint { pstatic = Static })
397 dictN NoFC c
398 (constrainMeths (map basename all)
399 dictN sc)
400 where
401 -- After we insert the constraint into the lookup, we need to
402 -- ensure that the same dictionary is used to resolve lookups
403 -- to the other methods in the interface
404 constrainMeths :: [Name] -> Name -> PTerm -> PTerm
405 constrainMeths allM dictN tm = transform (addC allM dictN) tm
407 addC allM dictN m@(PRef fc hls n)
408 | n `elem` allM = PApp NoFC m [pconst (PRef NoFC hls dictN)]
409 | otherwise = m
410 addC _ _ tm = tm
412 -- make arguments explicit and don't bind interface parameters
413 toExp ns e (PPi (Imp l s p _ _ r) n fc ty sc)
414 | n `elem` ns = toExp ns e sc
415 | otherwise = PPi (e l s p r) n fc ty (toExp ns e sc)
416 toExp ns e (PPi p n fc ty sc) = PPi p n fc ty (toExp ns e sc)
417 toExp ns e sc = sc
419-- | Get the docstring corresponding to a member, if one exists
420memberDocs :: PDecl -> Maybe (Name, Docstring (Either Err PTerm))
421memberDocs (PTy d _ _ _ _ n _ _) = Just (basename n, d)
422memberDocs (PPostulate _ d _ _ _ _ n _) = Just (basename n, d)
423memberDocs (PData d _ _ _ _ pdata) = Just (basename $ d_name pdata, d)
424memberDocs (PRecord d _ _ _ n _ _ _ _ _ _ _ ) = Just (basename n, d)
425memberDocs (PInterface d _ _ _ n _ _ _ _ _ _ _) = Just (basename n, d)
426memberDocs _ = Nothing
429-- | In a top level type for a method, expand all the method names' namespaces
430-- so that we don't have to disambiguate later
431expandMethNS :: SyntaxInfo
432 -> PTerm -> PTerm
433expandMethNS syn = mapPT expand
434 where
435 expand (PRef fc hls n) | n `elem` imp_methods syn = PRef fc hls $ expandNS syn n
436 expand t = t
438-- | Find the determining parameter locations
439findDets :: Name -> [Name] -> Idris [Int]
440findDets n ns =
441 do i <- getIState
442 return $ case lookupTyExact n (tt_ctxt i) of
443 Just ty -> getDetPos 0 ns ty
444 Nothing -> []
445 where
446 getDetPos i ns (Bind n (Pi _ _ _ _) sc)
447 | n `elem` ns = i : getDetPos (i + 1) ns sc
448 | otherwise = getDetPos (i + 1) ns sc
449 getDetPos _ _ _ = []