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