be54e85 · Idris-dev · git.iko.soy

git.iko.soy/Idris-dev

on master help sign in

Reorder instance methods

be54e85Edwin Brady12 years ago

src/Idris/Elab/Class.hs+1−1

compare with master

unifiedsplit

@@ -69,7 +69,7 @@ elabClass info syn_in doc fc constraints tn ps pDocs fds ds

69 let idecls = filter instdecl ds -- default superclass instance declarations

70 mapM_ checkDefaultSuperclassInstance idecls

71 let mnames = map getMName mdecls

72− logLvl 2 $ "Building methods " ++ show mnames

72+ logLvl 1 $ "Building methods " ++ show mnames

73 ims <- mapM (tdecl mnames) mdecls

74 defs <- mapM (defdecl (map (\ (x,y,z) -> z) ims) constraint)

75 (filter clause ds)

src/Idris/Elab/Instance.hs+21−2

@@ -103,8 +103,11 @@ elabInstance info syn doc argDocs what fc cs n ps t expn ds = do

103 op, coninsert cs t', t'))

104 (class_methods ci)

105 logLvl 3 (show (mtys, ips))

106+ logLvl 5 ("Before defaults: " ++ show ds ++ "\n" ++ show (map fst (class_methods ci)))

106− let ds' = insertDefaults i iname (class_defaults ci) ns ds

107+ let ds_defs = insertDefaults i iname (class_defaults ci) ns ds

108+ logLvl 3 ("After defaults: " ++ show ds_defs ++ "\n")

109+ let ds' = reorderDefs (map fst (class_methods ci)) $ ds_defs

107− iLOG ("Defaults inserted: " ++ show ds' ++ "\n" ++ show ci)

110+ iLOG ("Reordered: " ++ show ds' ++ "\n")

108 mapM_ (warnMissing ds' ns iname) (map fst (class_methods ci))

111 mapM_ (warnMissing ds' ns iname) (map fst (class_methods ci))

109 mapM_ (checkInClass (map fst (class_methods ci))) (concatMap defined ds')

112 mapM_ (checkInClass (map fst (class_methods ci))) (concatMap defined ds')

110 let wbTys = map mkTyDecl mtys

113 let wbTys = map mkTyDecl mtys

@@ -249,6 +252,22 @@ elabInstance info syn doc argDocs what fc cs n ps t expn ds = do

249 coninsert cs (PPi p@(Imp _ _ _ _) n t sc) = PPi p n t (coninsert cs sc)

252 coninsert cs (PPi p@(Imp _ _ _ _) n t sc) = PPi p n t (coninsert cs sc)

250 coninsert cs sc = conbind cs sc

253 coninsert cs sc = conbind cs sc

251

254

255+ -- Reorder declarations to be in the same order as defined in the

256+ -- class declaration (important so that we insert default definitions

257+ -- in the right place, and so that dependencies between methods are

258+ -- respected)

259+ reorderDefs :: [Name] -> [PDecl] -> [PDecl]

260+ reorderDefs ns [] = []

261+ reorderDefs [] ds = ds

262+ reorderDefs (n : ns) ds = case pick n [] ds of

263+ Just (def, ds') -> def : reorderDefs ns ds'

264+ Nothing -> reorderDefs ns ds

265+

266+ pick n acc [] = Nothing

267+ pick n acc (def@(PClauses _ _ cn cs) : ds)

268+ | nsroot n == nsroot cn = Just (def, acc ++ ds)

269+ pick n acc (d : ds) = pick n (acc ++ [d]) ds

270+

252 insertDefaults :: IState -> Name ->

271 insertDefaults :: IState -> Name ->

253 [(Name, (Name, PDecl))] -> [T.Text] ->

272 [(Name, (Name, PDecl))] -> [T.Text] ->

254 [PDecl] -> [PDecl]

273 [PDecl] -> [PDecl]