@@ -1,4 +1,5 @@
11{-# LANGUAGE PatternGuards #-}
2+{-# OPTIONS_GHC -fwarn-missing-signatures #-}
23module Idris.Elab.Class(elabClass) where
34
45import Idris.AbsSyntax
@@ -47,6 +48,7 @@ import qualified Data.Set as S
4748import qualified Data.Text as T
4849import Data.Char(isLetter, toLower)
4950import Data.List.Split (splitOn)
51+import Data.Generics.Uniplate.Data (transform)
5052
5153import Util.Pretty(pretty, text)
5254
@@ -83,6 +85,7 @@ elabClass info syn_in doc fc constraints tn tnfc ps pDocs fds ds mcn cd
8385 let (methods, imethods)
8486 = unzip (map (\ (x, y, z) -> (x, y)) ims)
8587 let defaults = map (\ (x, (y, z)) -> (x,y)) defs
88+
8689 -- build instance constructor type
8790 let cty = impbind [(pn, pt) | (pn, _, pt) <- ps] $ conbind constraints
8891 $ pibind (map (\ (n, ty) -> (nsroot n, ty)) methods)
@@ -92,6 +95,7 @@ elabClass info syn_in doc fc constraints tn tnfc ps pDocs fds ds mcn cd
9295 let ddecl = PDatadecl tn NoFC tty cons
9396
9497 logLvl 5 $ "Class data " ++ show (showDImp verbosePPOption ddecl)
98+
9599 -- Elaborate the data declaration
96100 elabData info (syn { no_imp = no_imp syn ++ mnames,
97101 imp_methods = mnames }) doc pDocs fc [] ddecl
@@ -118,7 +122,7 @@ elabClass info syn_in doc fc constraints tn tnfc ps pDocs fds ds mcn cd
118122 [(pnfc, AnnBoundName pn False) | (pn, pnfc, _) <- ps] ++
119123 [(fdfc, AnnBoundName fc False) | (fc, fdfc) <- fds] ++
120124 maybe [] (\(conN, conNFC) -> [(conNFC, AnnName conN Nothing Nothing Nothing)]) mcn
121−
125+
122126 where
123127 nodoc (n, (_, _, o, t)) = (n, (o, t))
124128
@@ -132,11 +136,6 @@ elabClass info syn_in doc fc constraints tn tnfc ps pDocs fds ds mcn cd
132136 chkUniq (PPi _ _ _ _ sc) t = chkUniq sc t
133137 chkUniq _ t = t
134138
135− mdec :: Name -> Name
136− mdec (UN n) = SN (MethodN (UN n))
137− mdec (NS x n) = NS (mdec x) n
138− mdec x = x
139−
140139 -- TODO: probably should normalise
141140 checkDefaultSuperclassInstance :: PDecl -> Idris ()
142141 checkDefaultSuperclassInstance (PInstance _ _ _ fc cs n _ ps _ _ _)
@@ -171,7 +170,7 @@ elabClass info syn_in doc fc constraints tn tnfc ps pDocs fds ds mcn cd
171170 defdecl mtys c d@(PClauses fc opts n cs) =
172171 case lookup n mtys of
173172 Just (nfc, syn, o, ty) ->
174− do let ty' = insertConstraint c ty
173+ do let ty' = insertConstraint c (map fst mtys) ty
175174 let ds = map (decorateid defaultdec)
176175 [PTy emptyDocstring [] syn fc [] n nfc ty',
177176 PClauses fc (o ++ opts) n cs]
@@ -215,10 +214,16 @@ elabClass info syn_in doc fc constraints tn tnfc ps pDocs fds ds mcn cd
215214 return [PTy emptyDocstring [] syn fc [] cfn NoFC ty,
216215 PClauses fc [Dictionary] cfn [PClause fc cfn lhs [] rhs []]]
217216
218− -- Generate a top level function which looks up a method in a given
217+ -- | Generate a top level function which looks up a method in a given
219218 -- dictionary (this is inlinable, always)
219+ tfun :: Name -- ^ The name of the class
220+ -> PTerm -- ^ A constraint for the class, to be inserted under the implicit bindings
221+ -> SyntaxInfo -> [Name] -- ^ All the method names
222+ -> (Name, (FC, Docstring (Either Err PTerm), FnOpts, PTerm))
223+ -- ^ The present declaration
224+ -> Idris [PDecl]
220225 tfun cn c syn all (m, (mfc, doc, o, ty))
221− = do let ty' = expandMethNS syn (insertConstraint c ty)
226+ = do let ty' = expandMethNS syn (insertConstraint c all ty)
222227 let mnames = take (length all) $ map (\x -> sMN x "meth") [0..]
223228 let capp = PApp fc (PRef fc cn) (map (pexp . PRef fc) mnames)
224229 let margs = getMArgs ty
@@ -236,6 +241,7 @@ elabClass info syn_in doc fc constraints tn tnfc ps pDocs fds ds mcn cd
236241 getMArgs (PPi (Constraint _ _) n _ ty sc) = CA : getMArgs sc
237242 getMArgs _ = []
238243
244+ getMeth :: [Name] -> [Name] -> Name -> PTerm
239245 getMeth (m:ms) (a:as) x | x == a = PRef fc m
240246 | otherwise = getMeth ms as x
241247
@@ -249,10 +255,24 @@ elabClass info syn_in doc fc constraints tn tnfc ps pDocs fds ds mcn cd
249255 rhsArgs (CA : xs) ns = pconst (PResolveTC fc) : rhsArgs xs ns
250256 rhsArgs [] _ = []
251257
252− insertConstraint c (PPi p@(Imp _ _ _ _) n fc ty sc)
253− = PPi p n fc ty (insertConstraint c sc)
254− insertConstraint c sc = PPi (constraint { pstatic = Static })
255− (sMN 0 "class") NoFC c sc
258+ insertConstraint :: PTerm -> [Name] -> PTerm -> PTerm
259+ insertConstraint c all (PPi p@(Imp _ _ _ _) n fc ty sc)
260+ = PPi p n fc ty (insertConstraint c all sc)
261+ insertConstraint c all sc = let dictN = sMN 0 "class"
262+ in PPi (constraint { pstatic = Static })
263+ dictN NoFC c
264+ (constrainMeths (map basename all)
265+ dictN sc)
266+ where
267+ -- After we insert the constraint into the lookup, we need to
268+ -- ensure that the same dictionary is used to resolve lookups
269+ -- to the other methods in the class
270+ constrainMeths :: [Name] -> Name -> PTerm -> PTerm
271+ constrainMeths allM dictN tm = transform (addC allM dictN) tm
272+ addC allM dictN m@(PRef fc n)
273+ | n `elem` allM = PApp NoFC m [pconst (PRef NoFC dictN)]
274+ | otherwise = m
275+ addC _ _ tm = tm
256276
257277 -- make arguments explicit and don't bind class parameters
258278 toExp ns e (PPi (Imp l s p _) n fc ty sc)
@@ -261,6 +281,13 @@ elabClass info syn_in doc fc constraints tn tnfc ps pDocs fds ds mcn cd
261281 toExp ns e (PPi p n fc ty sc) = PPi p n fc ty (toExp ns e sc)
262282 toExp ns e sc = sc
263283
284+-- | Get the method declaration name corresponding to a user-provided name
285+mdec :: Name -> Name
286+mdec (UN n) = SN (MethodN (UN n))
287+mdec (NS x n) = NS (mdec x) n
288+mdec x = x
289+
290+-- | Get the docstring corresponding to a member, if one exists
264291memberDocs :: PDecl -> Maybe (Name, Docstring (Either Err PTerm))
265292memberDocs (PTy d _ _ _ _ n _ _) = Just (basename n, d)
266293memberDocs (PPostulate _ d _ _ _ n _) = Just (basename n, d)
@@ -270,17 +297,18 @@ memberDocs (PClass d _ _ _ n _ _ _ _ _ _ _) = Just (basename n, d)
270297memberDocs _ = Nothing
271298
272299
273−-- In a top level type for a method, expand all the method names namespaces
300+-- | In a top level type for a method, expand all the method names' namespaces
274301-- so that we don't have to disambiguate later
275−expandMethNS :: SyntaxInfo
302+expandMethNS :: SyntaxInfo
276303 -> PTerm -> PTerm
277304expandMethNS syn = mapPT expand
278305 where
279306 expand (PRef fc n) | n `elem` imp_methods syn = PRef fc $ expandNS syn n
280307 expand t = t
281308
309+-- | Find the determining parameter locations
282310findDets :: Name -> [Name] -> Idris [Int]
283−findDets n ns =
311+findDets n ns =
284312 do i <- getIState
285313 return $ case lookupTyExact n (tt_ctxt i) of
286314 Just ty -> getDetPos 0 ns ty