@@ -101,6 +101,7 @@ elabInterface info syn_in doc fc constraints tn tnfc ps pDocs fds ds mcn cd
101 let idecls = filter impldecl ds -- default super interface implementation declarations
101 let idecls = filter impldecl ds -- default super interface implementation declarations
102 mapM_ checkDefaultSuperInterfaceImplementation idecls
102 mapM_ checkDefaultSuperInterfaceImplementation idecls
103 let mnames = map getMName mdecls
103 let mnames = map getMName mdecls
104+ let fullmnames = map getFullMName mdecls
104 ist <- getIState
105 ist <- getIState
105 let constraintNames = nub $
106 let constraintNames = nub $
106 concatMap (namesIn [] ist) (map snd constraints)
107 concatMap (namesIn [] ist) (map snd constraints)
@@ -113,7 +114,7 @@ elabInterface info syn_in doc fc constraints tn tnfc ps pDocs fds ds mcn cd
113 imp_methods = mnames }) doc pDocs fc [] pre_ddecl
114 imp_methods = mnames }) doc pDocs fc [] pre_ddecl
114 dets <- findDets tn (map fst fds)
115 dets <- findDets tn (map fst fds)
116− logElab 2 $ "Building methods " ++ show mnames
117+ logElab 3 $ "Building methods " ++ show fullmnames
117 ims <- mapM (tdecl impps mnames) mdecls
118 ims <- mapM (tdecl impps mnames) mdecls
118 defs <- mapM (defdecl (map (\ (x,y,z) -> z) ims) constraint)
119 defs <- mapM (defdecl (map (\ (x,y,z) -> z) ims) constraint)
119 (filter clause ds)
120 (filter clause ds)
@@ -134,28 +135,43 @@ elabInterface info syn_in doc fc constraints tn tnfc ps pDocs fds ds mcn cd
134 let (cfnTyDecls, cfnDefs) = unzip cfns
135 let (cfnTyDecls, cfnDefs) = unzip cfns
135 mapM_ (rec_elabDecl info EAll info) cfnTyDecls
136 mapM_ (rec_elabDecl info EAll info) cfnTyDecls
138+ -- for each method, build a top level function
139+ -- 'tfun' builds appropriate implicits for the constructor
141+ fns <- mapM (tfun cn constraint (syn { imp_methods = mnames }) -- mnames })
142+ (map fst imethods)) imethods
143+ let (fnTyDecls, fnDefs) = unzip fns
144+ mapM_ (rec_elabDecl info EAll info) fnTyDecls
146+ elabMethTys <- mapM getElabMethTy fullmnames
147+ logElab 3 $ "Method types:\n" ++ showSep "\n" (map showTmImpls elabMethTys)
149+ let cpos = map (\ (n, ty) -> (n, findConstraint ty))
150+ (zip fullmnames elabMethTys)
151+ logElab 5 $ "Constraint pos: " ++ show cpos
137 -- build implementation constructor type
153 -- build implementation constructor type
138− let cty = impbind [(pn, pt) | (pn, _, pt) <- impps ++ ps] $ conbind constraints
154+ let cty = impbind [(pn, pt) | (pn, _, pt) <- impps ++ ps] $
155+ conbind constraints $
156+ pibind (map (mkMethTy cpos) (zip fullmnames elabMethTys))
158+ let ctyOld = impbind [(pn, pt) | (pn, _, pt) <- impps ++ ps] $ conbind constraints
139 $ pibind (map (\ (n, ty) -> (nsroot n, ty)) methods)
159 $ pibind (map (\ (n, ty) -> (nsroot n, ty)) methods)
140 constraint
160 constraint
162+ logElab 3 $ "Constraint constructor type: " ++ showTmImpls cty
142 let cons = [(cd, pDocs ++ mapMaybe memberDocs ds, cn, NoFC, cty, fc, [])]
165 let cons = [(cd, pDocs ++ mapMaybe memberDocs ds, cn, NoFC, cty, fc, [])]
143 let ddecl = PDatadecl tn NoFC tty cons
166 let ddecl = PDatadecl tn NoFC tty cons
145− logElab 5 $ "Interface " ++ show (showDImp verbosePPOption ddecl)
168+ logElab 10 $ "Interface " ++ show (showDImp verbosePPOption ddecl)
147− -- for each method, build a top level function
148− -- 'tfun' builds appropriate implicits for the constructor
150− fns <- mapM (tfun cn constraint (syn { imp_methods = mnames }) -- mnames })
151− (map fst imethods)) imethods
152− let (fnTyDecls, fnDefs) = unzip fns
154 -- Elaborate the data declaration
171 -- Elaborate the data declaration
155 elabData info (syn { no_imp = no_imp syn ++ mnames,
172 elabData info (syn { no_imp = no_imp syn ++ mnames,
156− imp_methods = mnames }) doc pDocs fc [] ddecl
173+ imp_methods = [] }) doc pDocs fc [] ddecl
158− mapM_ (rec_elabDecl info EAll info) fnTyDecls
160 logElab 5 $ "Function types " ++ show fnTyDecls
176 logElab 5 $ "Function types " ++ show fnTyDecls
161 logElab 5 $ "Method types now: " ++ show imethods
177 logElab 5 $ "Method types now: " ++ show imethods
@@ -182,6 +198,48 @@ elabInterface info syn_in doc fc constraints tn tnfc ps pDocs fds ds mcn cd
182 maybe [] (\(conN, conNFC) -> [(conNFC, AnnName conN Nothing Nothing Nothing)]) mcn
198 maybe [] (\(conN, conNFC) -> [(conNFC, AnnName conN Nothing Nothing Nothing)]) mcn
201+ getElabMethTy :: Name -> Idris PTerm
202+ getElabMethTy n = do ist <- getIState
203+ case lookupTyExact n (tt_ctxt ist) of
204+ Just ty -> return (delabDirect ist ty)
205+ Nothing -> tclift $ tfail (At fc (InternalMsg "Can't happen, elabMethTy"))
207+ -- Find the argument position of the current interface in a method type
208+ -- (we'll use this to update the elaborated top level method types before
209+ -- building a data declaration
210+ findConstraint :: PTerm -> Int
211+ findConstraint = findPos 0
213+ findPos i (PPi _ _ _ (PRef _ _ n) sc)
215+ findPos i (PPi _ _ _ (PApp _ (PRef _ _ n) _) sc)
217+ findPos i (PPi _ _ _ ty sc) = findPos (i + 1) sc
218+ findPos i _ = -1 -- Can't happen!
220+ -- Make the method component of the constructor type by taking the
221+ -- elaborated top level method and removing the implicits/constraint
222+ mkMethTy :: [(Name, Int)] -> (Name, PTerm) -> (Name, PTerm)
223+ mkMethTy cpos (n, tm) = (nsroot n, dropPis num (mapPT dropImp tm))
225+ num = case lookup n cpos of
229+ dropPis n (PPi _ _ _ _ sc) | n > 0 = dropPis (n - 1) sc
232+ dropImp (PApp fc (PRef fcr fcs n) args)
233+ | Just pos <- lookup n cpos
234+ = PApp fc (PRef fcr fcs (nsroot n))
235+ (filter notConstr (drop (pos + 1) args))
236+ dropImp (PApp fc f args)
237+ = PApp fc f (filter notConstr args)
240+ notConstr (PConstraint {}) = False
185 nodoc (n, (inj, _, _, o, t)) = (n, (inj, o, t))
243 nodoc (n, (inj, _, _, o, t)) = (n, (inj, o, t))
187 pibind [] x = x
245 pibind [] x = x
@@ -224,6 +282,9 @@ elabInterface info syn_in doc fc constraints tn tnfc ps pDocs fds ds mcn cd
225 getMName (PTy _ _ _ _ _ n nfc _) = nsroot n
283 getMName (PTy _ _ _ _ _ n nfc _) = nsroot n
226 getMName (PData _ _ _ _ _ (PLaterdecl n nfc _)) = nsroot n
284 getMName (PData _ _ _ _ _ (PLaterdecl n nfc _)) = nsroot n
286+ getFullMName (PTy _ _ _ _ _ n nfc _) = n
287+ getFullMName (PData _ _ _ _ _ (PLaterdecl n nfc _)) = n
228 tdecl impps allmeths (PTy doc _ syn _ o n nfc t)
289 tdecl impps allmeths (PTy doc _ syn _ o n nfc t)
229 = do t' <- implicit' info syn (map (\(n, _, _) -> n) (impps ++ ps) ++ allmeths) n t
290 = do t' <- implicit' info syn (map (\(n, _, _) -> n) (impps ++ ps) ++ allmeths) n t