be54e85 · Idris-dev · git.iko.soy

git.iko.soy/Idris-dev

Reorder instance methods

They need to be in the same order as in the class declaration, to preserve dependencies and make sure dependencies which need to reduce are defined. Fixes #1993

commitbe54e85a03ecd039d6d22cc8ae85abfaed5cd9b7 authorEdwin Brady <ecb10@st-andrews.ac.uk> dateFri 20 Mar 2015, 12:59 (12 years ago) parent159a0c4

2 files changed+22−3

compare with master

unifiedsplit

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

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

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

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

7070 mapM_ checkDefaultSuperclassInstance idecls

7171 let mnames = map getMName mdecls

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

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

7373 ims <- mapM (tdecl mnames) mdecls

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

7575 (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

103103 op, coninsert cs t', t'))

104104 (class_methods ci)

105105 logLvl 3 (show (mtys, ips))

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

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

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

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

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

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

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

110113 let wbTys = map mkTyDecl mtys

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

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

250253 coninsert cs sc = conbind cs sc

251254

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+

252271 insertDefaults :: IState -> Name ->

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

254273 [PDecl] -> [PDecl]