2Module : Idris.Elab.Interface
3Description : Code to elaborate interfaces.
6Maintainer : The Idris Community.
8{-# LANGUAGE PatternGuards #-}
9{-# OPTIONS_GHC -fwarn-missing-signatures #-}
10module Idris.Elab.Interface(elabInterface) where
14import Idris.Core.CaseTree
15import Idris.Core.Elaborate hiding (Tactic(..))
16import Idris.Core.Evaluate
17import Idris.Core.Execute
19import Idris.Core.Typecheck
23import Idris.Delaborate
24import Idris.Docstrings
29import Idris.Elab.Utils
33import Idris.Output (iWarn, iputStrLn, pshow, sendHighlighting)
34import Idris.PartialEval
35import Idris.Primitives
39import Util.Pretty (pretty, text)
41import Prelude hiding (id, (.))
43import Control.Applicative hiding (Const)
44import Control.Category
47import Control.Monad.State.Strict as State
48import Data.Char (isLetter, toLower)
49import Data.Generics.Uniplate.Data (transform)
51import Data.List.Split (splitOn)
52import qualified Data.Map as Map
54import qualified Data.Set as S
55import qualified Data.Text as T
59data MArgTy = IA Name | EA Name | CA deriving Show
61elabInterface :: ElabInfo
63 -> Docstring (Either Err PTerm)
66 -> [(Name, PTerm)] -- ^ Superclass constraints
69 -> [(Name, FC, PTerm)] -- ^ Parameters
70 -> [(Name, Docstring (Either Err PTerm))]
71 -> [(Name, FC)] -- ^ determining params
72 -> [PDecl] -- ^ interface body
73 -> Maybe (Name, FC) -- ^ implementation ctor name and location
74 -> Docstring (Either Err PTerm) -- ^ implementation ctor docs
76elabInterface info_in syn_in doc what fc constraints tn tnfc ps pDocs fds ds mcn cd
77 = do let cn = fromMaybe (SN (ImplementationCtorN tn)) (fst <$> mcn)
78 let constraint = PApp fc (PRef fc [] tn)
79 (map (pexp . PRef fc []) (map (\(n, _, _) -> n) ps))
82 syn_in { using = addToUsing (using syn_in)
83 [(pn, pt) | (pn, _, pt) <- ps]
86 -- Calculate implicit parameters
88 let impps_ns = nub $ map (\n -> (n, emptyFC, Placeholder)) $
89 concatMap (implicitNamesIn [] ist)
90 (map (\ (_,_,x) -> x) ps)
91 let impps = filter (\ (n, _, _) ->
92 n `notElem` (map (\ (n, _, _) -> n) ps)) impps_ns
94 let tty = impbind (map (\(n, _, ty) -> (n, ty)) impps) $
95 pibind (map (\(n, _, ty) -> (n, ty)) ps) (PType fc)
97 logElab 5 $ "Implicit parameters are " ++ show impps
98 logElab 5 $ "Interface type is " ++ showTmImpls tty
100 -- build data declaration
101 let mdecls = filter tydecl ds -- method declarations
102 let idecls = filter impldecl ds -- default super interface implementation declarations
103 mapM_ checkDefaultSuperInterfaceImplementation idecls
104 let mnames = map getMName mdecls
105 let fullmnames = map getFullMName mdecls
107 let constraintNames = nub $
108 concatMap (namesIn [] ist) (map snd constraints)
110 mapM_ (checkConstraintName (map (\(x, _, _) -> x) ps)) constraintNames
112 let pre_ddecl = PLaterdecl tn NoFC tty
113 -- Elaborate the interface header, as long as we haven't done it
114 -- in an earlier pass
115 when (what /= EDefns) $
116 elabData info (syn { no_imp = no_imp syn ++ mnames,
117 imp_methods = mnames }) doc pDocs fc [] pre_ddecl
118 -- Continue only if we're not in the first pass of a mutual block
119 when (what /= ETypes) $ do
120 dets <- findDets tn (map fst fds)
122 logElab 3 $ "Building methods " ++ show fullmnames
123 ims <- mapM (tdecl impps mnames) mdecls
124 defs <- mapM (defdecl (map (\ (x,y,z) -> z) ims) constraint)
126 let (methods, imethods)
127 = unzip (map (\ (x, y, z) -> (x, y)) ims)
128 let defaults = map (\ (x, (y, z)) -> (x,y)) defs
130 addInterface tn (CI cn (map nodoc imethods) defaults idecls
131 (map (\(n, _, _) -> n) impps)
132 (map (\(n, _, _) -> n) ps)
133 (map snd constraints)
136 -- for each constraint, build a top level function to chase it
137 -- elaborate types now, bodies later (after we've done the constructor
139 cfns <- mapM (cfun cn constraint syn (map fst imethods)) constraints
140 let (cfnTyDecls, cfnDefs) = unzip cfns
141 mapM_ (rec_elabDecl info EAll info) cfnTyDecls
143 -- for each method, build a top level function
144 -- 'tfun' builds appropriate implicits for the constructor
146 fns <- mapM (tfun cn constraint (syn { imp_methods = mnames }) -- mnames })
147 (map fst imethods)) imethods
148 let (fnTyDecls, fnDefs) = unzip fns
149 mapM_ (rec_elabDecl info EAll info) fnTyDecls
151 elabMethTys <- mapM getElabMethTy fullmnames
153 logElab 3 $ "Method types:\n" ++ showSep "\n" (map showTmImpls elabMethTys)
155 let cpos = map (\ (n, ty) -> (n, findConstraint ty))
156 (zip fullmnames elabMethTys)
157 logElab 5 $ "Constraint pos: " ++ show cpos
159 -- Method types to store in the IState, taken from the elaborated
160 -- types with the parameter removed
161 let storemeths = map (mkMethTy True cpos) (zip fullmnames elabMethTys)
162 updateIMethods tn storemeths
164 -- build implementation constructor type
165 let cty = impbind [(pn, pt) | (pn, _, pt) <- impps ++ ps] $
166 conbind constraints $
167 pibind (map (mkMethTy False cpos) (zip fullmnames elabMethTys))
169 logElab 3 $ "Constraint constructor type: " ++ showTmImpls cty
171 let cons = [(cd, pDocs ++ mapMaybe memberDocs ds, cn, NoFC, cty, fc, [])]
172 let ddecl = PDatadecl tn NoFC tty cons
174 logElab 10 $ "Interface " ++ show (showDImp verbosePPOption ddecl)
177 -- Elaborate the data declaration
178 elabData info (syn { no_imp = no_imp syn ++ mnames,
179 imp_methods = [] }) doc pDocs fc [] ddecl
182 logElab 5 $ "Function types " ++ show fnTyDecls
183 logElab 5 $ "Method types now: " ++ show imethods
185 -- Elaborate the the top level constraint chasers
186 -- (Types elaborated earlier)
187 mapM_ (rec_elabDecl info EAll info) cfnDefs
188 -- Elaborate the the top level method bodies
189 mapM_ (rec_elabDecl info EAll info) fnDefs
191 -- Flag all the top level data declarations as injective
192 mapM_ (\n -> do setInjectivity n True
193 addIBC (IBCInjective n True))
194 (map fst (filter (\(_, (inj, _, _, _, _)) -> inj) imethods))
196 -- add the default definitions
197 mapM_ (rec_elabDecl info EAll info) (concatMap (snd.snd) defs)
198 addIBC (IBCInterface tn)
201 [(tnfc, AnnName tn Nothing Nothing Nothing)] ++
202 [(pnfc, AnnBoundName pn False) | (pn, pnfc, _) <- ps] ++
203 [(fdfc, AnnBoundName fc False) | (fc, fdfc) <- fds] ++
204 maybe [] (\(conN, conNFC) -> [(conNFC, AnnName conN Nothing Nothing Nothing)]) mcn
207 info = info_in { noCaseLift = tn : noCaseLift info_in }
209 getElabMethTy :: Name -> Idris PTerm
210 getElabMethTy n = do ist <- getIState
211 let impls = case lookupCtxtExact n (idris_implicits ist) of
214 case lookupTyExact n (tt_ctxt ist) of
215 Just ty -> return (delabTy' ist impls [] ty False False False)
216 Nothing -> tclift $ tfail (At fc (InternalMsg "Can't happen, elabMethTy"))
218 -- Find the argument position of the current interface in a method type
219 -- (we'll use this to update the elaborated top level method types before
220 -- building a data declaration
221 findConstraint :: PTerm -> Int
222 findConstraint = findPos 0
224 findPos i (PPi _ _ _ (PRef _ _ n) sc)
226 findPos i (PPi _ _ _ (PApp _ (PRef _ _ n) _) sc)
228 findPos i (PPi _ _ _ ty sc) = findPos (i + 1) sc
229 findPos i _ = -1 -- Can't happen!
231 -- Make the method component of the constructor type by taking the
232 -- elaborated top level method and removing the implicits/constraint
233 mkMethTy :: Bool -> [(Name, Int)] -> (Name, PTerm) -> (Name, PTerm)
234 mkMethTy keepns cpos (n, tm)
235 = (if keepns then n else nsroot n, dropPis num (mapPT dropImp tm))
237 num = case lookup n cpos of
241 dropPis n (PPi _ _ _ _ sc) | n > 0 = dropPis (n - 1) sc
244 dropImp (PApp fc (PRef fcr fcs n) args)
245 | Just pos <- lookup n cpos
246 = PApp fc (PRef fcr fcs (nsroot n))
247 (filter notConstr (drop (pos + 1) args))
248 dropImp (PApp fc f args)
249 = PApp fc f (filter notConstr args)
252 notConstr (PConstraint {}) = False
255 nodoc (n, (inj, _, _, o, t)) = (n, (inj, o, t))
258 pibind ((n, ty): ns) x = PPi expl n NoFC ty (pibind ns (chkUniq ty x))
260 -- To make sure the type constructor of the interface is in the appropriate
261 -- uniqueness hierarchy
262 chkUniq u@(PUniverse _ _) (PType _) = u
263 chkUniq (PUniverse _ l) (PUniverse _ r) = PUniverse NoFC (min l r)
264 chkUniq (PPi _ _ _ _ sc) t = chkUniq sc t
267 -- TODO: probably should normalise
268 checkDefaultSuperInterfaceImplementation :: PDecl -> Idris ()
269 checkDefaultSuperInterfaceImplementation (PImplementation _ _ _ fc cs _ _ _ n _ ps _ _ _ _)
270 = do when (not $ null cs) . tclift
271 $ tfail (At fc (Msg "Default super interface implementations can't have constraints."))
273 let t = PApp fc (PRef fc [] n) (map pexp ps)
274 let isConstrained = any (== t) (map snd constraints)
275 when (not isConstrained) . tclift
276 $ tfail (At fc (Msg "Default implementations must be for a super interface constraint on the containing interface."))
279 checkConstraintName :: [Name] -> Name -> Idris ()
280 checkConstraintName bound cname
281 | cname `notElem` bound
282 = tclift $ tfail (At fc (Msg $ "Name " ++ show cname ++
283 " is not bound in interface " ++ show tn
284 ++ " " ++ showSep " " (map show bound)))
285 | otherwise = return ()
287 impbind :: [(Name, PTerm)] -> PTerm -> PTerm
289 impbind ((n, ty): ns) x = PPi impl n NoFC ty (impbind ns x)
291 conbind :: [(Name, PTerm)] -> PTerm -> PTerm
292 conbind ((c, ty) : ns) x = PPi constraint c NoFC ty (conbind ns x)
295 getMName (PTy _ _ _ _ _ n nfc _) = nsroot n
296 getMName (PData _ _ _ _ _ (PLaterdecl n nfc _)) = nsroot n
298 getFullMName (PTy _ _ _ _ _ n nfc _) = n
299 getFullMName (PData _ _ _ _ _ (PLaterdecl n nfc _)) = n
301 tdecl impps allmeths (PTy doc _ syn _ o n nfc t)
302 = do t' <- implicit' info syn (map (\(n, _, _) -> n) (impps ++ ps) ++ allmeths) n t
303 logElab 1 $ "Method " ++ show n ++ " : " ++ showTmImpls t'
304 return ( (n, (toExp (map (\(pn, _, _) -> pn) ps) Exp t')),
305 (n, (False, nfc, doc, o, (toExp (map (\(pn, _, _) -> pn) ps)
306 (\ l s p r -> Imp l s p Nothing True r) t'))),
307 (n, (nfc, syn, o, t) ) )
308 tdecl impps allmeths (PData doc _ syn _ _ (PLaterdecl n nfc t))
310 t' <- implicit' info syn (map (\(n, _, _) -> n) ps ++ allmeths) n t
311 logElab 2 $ "Data method " ++ show n ++ " : " ++ showTmImpls t'
312 return ( (n, (toExp (map (\(pn, _, _) -> pn) ps) Exp t')),
313 (n, (True, nfc, doc, o, (toExp (map (\(pn, _, _) -> pn) ps)
314 (\ l s p r -> Imp l s p Nothing True r) t'))),
315 (n, (nfc, syn, o, t) ) )
316 tdecl impps allmeths (PData doc _ syn _ _ _)
317 = ierror $ At fc (Msg "Data definitions not allowed in an interface declaration")
318 tdecl _ _ _ = ierror $ At fc (Msg "Not allowed in an interface declaration")
320 -- Create default definitions
321 defdecl mtys c d@(PClauses fc opts n cs) =
322 case lookup n mtys of
323 Just (nfc, syn, o, ty) ->
324 do let ty' = insertConstraint c (map fst mtys) ty
325 let ds = map (decorateid defaultdec)
326 [PTy emptyDocstring [] syn fc [] n nfc ty',
327 PClauses fc (o ++ opts) n cs]
329 return (n, ((defaultdec n, ds!!1), ds))
330 _ -> ierror $ At fc (Msg (show n ++ " is not a method"))
331 defdecl _ _ _ = ifail "Can't happen (defdecl)"
333 defaultdec (UN n) = sUN ("default#" ++ str n)
334 defaultdec (NS n ns) = NS (defaultdec n) ns
336 tydecl (PTy{}) = True
337 tydecl (PData _ _ _ _ _ _) = True
339 impldecl (PImplementation{}) = True
341 clause (PClauses{}) = True
344 -- Generate a function for chasing a dictionary constraint
345 cfun :: Name -> PTerm -> SyntaxInfo -> [a] -> (Name, PTerm) -> Idris (PDecl, PDecl)
346 cfun cn c syn all (cnm, con)
347 = do let cfn = SN (ParentN cn (txt (show con)))
348 let mnames = take (length all) $ map (\x -> sMN x "meth") [0..]
349 let capp = PApp fc (PRef fc [] cn) (map (pexp . PRef fc []) mnames)
350 let lhs = PApp fc (PRef fc [] cfn) [pconst capp]
351 let rhs = PResolveTC (fileFC "HACK")
352 let ty = PPi constraint cnm NoFC c con
353 logElab 2 ("Dictionary constraint: " ++ showTmImpls ty)
354 logElab 2 (showTmImpls lhs ++ " = " ++ showTmImpls rhs)
356 let conn = case con of
358 PApp _ (PRef _ _ n) _ -> n
359 let conn' = case lookupCtxtName conn (idris_interfaces i) of
362 addImplementation False True conn' cfn
363 addIBC (IBCImplementation False True conn' cfn)
364-- iputStrLn ("Added " ++ show (conn, cfn, ty))
365 return (PTy emptyDocstring [] syn fc [] cfn NoFC ty,
366 PClauses fc [Inlinable, Dictionary] cfn [PClause fc cfn lhs [] rhs []])
368 -- | Generate a top level function which looks up a method in a given
369 -- dictionary (this is inlinable, always)
370 tfun :: Name -- ^ The name of the interface
371 -> PTerm -- ^ A constraint for the interface, to be inserted under the implicit bindings
372 -> SyntaxInfo -> [Name] -- ^ All the method names
373 -> (Name, (Bool, FC, Docstring (Either Err PTerm), FnOpts, PTerm))
374 -- ^ The present declaration
375 -> Idris (PDecl, PDecl)
376 tfun cn c syn all (m, (isdata, mfc, doc, o, ty))
377 = do let ty' = expandMethNS syn (insertConstraint c all ty)
378 let mnames = take (length all) $ map (\x -> sMN x "meth") [0..]
379 let capp = PApp fc (PRef fc [] cn) (map (pexp . PRef fc []) mnames)
380 let margs = getMArgs ty
381 let anames = map (\x -> sMN x "arg") [0..]
382 let lhs = PApp fc (PRef fc [] m) (pconst capp : lhsArgs margs anames)
383 let rhs = PApp fc (getMeth mnames all m) (rhsArgs margs anames)
384 logElab 2 ("Top level type: " ++ showTmImpls ty')
385 logElab 1 (show (m, ty', capp, margs))
386 logElab 2 ("Definition: " ++ showTmImpls lhs ++ " = " ++ showTmImpls rhs)
387 return (PTy doc [] syn fc o m mfc ty',
388 PClauses fc [Inlinable] m [PClause fc m lhs [] rhs []])
390 updateIMethod :: [(Name, PTerm)] ->
391 (Name, (a, b, c, d, PTerm)) ->
392 (Name, (a, b, c, d, PTerm))
393 updateIMethod ns tm@(n, (isf, mfc, doc, o, ty))
394 | Just ty' <- lookup (nsroot n) ns = (n, (isf, mfc, doc, o, ty'))
397 getMArgs (PPi (Imp _ _ _ _ _ _) n _ ty sc) = IA n : getMArgs sc
398 getMArgs (PPi (Exp _ _ _ _) n _ ty sc) = EA n : getMArgs sc
399 getMArgs (PPi (Constraint _ _ _) n _ ty sc) = CA : getMArgs sc
402 getMeth :: [Name] -> [Name] -> Name -> PTerm
403 getMeth (m:ms) (a:as) x | x == a = PRef fc [] m
404 | otherwise = getMeth ms as x
406 lhsArgs (EA _ : xs) (n : ns) = [] -- pexp (PRef fc n) : lhsArgs xs ns
407 lhsArgs (IA n : xs) ns = pimp n (PRef fc [] n) False : lhsArgs xs ns
408 lhsArgs (CA : xs) ns = lhsArgs xs ns
411 rhsArgs (EA _ : xs) (n : ns) = [] -- pexp (PRef fc n) : rhsArgs xs ns
412 rhsArgs (IA n : xs) ns = pexp (PRef fc [] n) : rhsArgs xs ns
413 rhsArgs (CA : xs) ns = pconst (PResolveTC fc) : rhsArgs xs ns
416 -- Add the top level constraint. Put it first - elaboration will resolve
417 -- the order of the implicits if there are dependencies.
418 -- Also ensure the dictionary is used for lookup of any methods that
419 -- are used in the type
420 insertConstraint :: PTerm -> [Name] -> PTerm -> PTerm
421 insertConstraint c all sc
422 = let dictN = sMN 0 "__interface" in
423 PPi (constraint { pstatic = Static })
425 (constrainMeths (map basename all)
428 -- After we insert the constraint into the lookup, we need to
429 -- ensure that the same dictionary is used to resolve lookups
430 -- to the other methods in the interface
431 constrainMeths :: [Name] -> Name -> PTerm -> PTerm
432 constrainMeths allM dictN tm = transform (addC allM dictN) tm
434 addC allM dictN m@(PRef fc hls n)
435 | n `elem` allM = PApp NoFC m [pconst (PRef NoFC hls dictN)]
439 -- make arguments explicit and don't bind interface parameters
440 toExp ns e (PPi (Imp l s p _ _ r) n fc ty sc)
441 | n `elem` ns = toExp ns e sc
442 | otherwise = PPi (e l s p r) n fc ty (toExp ns e sc)
443 toExp ns e (PPi p n fc ty sc) = PPi p n fc ty (toExp ns e sc)
446-- | Get the method declaration name corresponding to a user-provided name
448mdec (UN n) = SN (MethodN (UN n))
449mdec (NS x n) = NS (mdec x) n
452-- | Get the docstring corresponding to a member, if one exists
453memberDocs :: PDecl -> Maybe (Name, Docstring (Either Err PTerm))
454memberDocs (PTy d _ _ _ _ n _ _) = Just (basename n, d)
455memberDocs (PPostulate _ d _ _ _ _ n _) = Just (basename n, d)
456memberDocs (PData d _ _ _ _ pdata) = Just (basename $ d_name pdata, d)
457memberDocs (PRecord d _ _ _ n _ _ _ _ _ _ _ ) = Just (basename n, d)
458memberDocs (PInterface d _ _ _ n _ _ _ _ _ _ _) = Just (basename n, d)
459memberDocs _ = Nothing
462-- | In a top level type for a method, expand all the method names' namespaces
463-- so that we don't have to disambiguate later
464expandMethNS :: SyntaxInfo
466expandMethNS syn = mapPT expand
468 expand (PRef fc hls n) | n `elem` imp_methods syn = PRef fc hls $ expandNS syn n
471-- | Find the determining parameter locations
472findDets :: Name -> [Name] -> Idris [Int]
475 return $ case lookupTyExact n (tt_ctxt i) of
476 Just ty -> getDetPos 0 ns ty
479 getDetPos i ns (Bind n (Pi _ _ _ _) sc)
480 | n `elem` ns = i : getDetPos (i + 1) ns sc
481 | otherwise = getDetPos (i + 1) ns sc
keysesc to close
- j k
- move down, up
- enter
- open
- esc
- back, or up a level
- 1 2 3 4
- readme, files, commits, refs
- /
- filter
- y
- copy the clone command
- c
- compare the chosen commit with another (or shift-click both)
- ?
- show or hide this list