Skip to content

Commit

Permalink
Reorder instance methods
Browse files Browse the repository at this point in the history
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
  • Loading branch information
edwinb committed Mar 20, 2015
1 parent 159a0c4 commit be54e85
Show file tree
Hide file tree
Showing 2 changed files with 22 additions and 3 deletions.
2 changes: 1 addition & 1 deletion src/Idris/Elab/Class.hs
Original file line number Diff line number Diff line change
Expand Up @@ -69,7 +69,7 @@ elabClass info syn_in doc fc constraints tn ps pDocs fds ds
let idecls = filter instdecl ds -- default superclass instance declarations
mapM_ checkDefaultSuperclassInstance idecls
let mnames = map getMName mdecls
logLvl 2 $ "Building methods " ++ show mnames
logLvl 1 $ "Building methods " ++ show mnames
ims <- mapM (tdecl mnames) mdecls
defs <- mapM (defdecl (map (\ (x,y,z) -> z) ims) constraint)
(filter clause ds)
Expand Down
23 changes: 21 additions & 2 deletions src/Idris/Elab/Instance.hs
Original file line number Diff line number Diff line change
Expand Up @@ -103,8 +103,11 @@ elabInstance info syn doc argDocs what fc cs n ps t expn ds = do
op, coninsert cs t', t'))
(class_methods ci)
logLvl 3 (show (mtys, ips))
let ds' = insertDefaults i iname (class_defaults ci) ns ds
iLOG ("Defaults inserted: " ++ show ds' ++ "\n" ++ show ci)
logLvl 5 ("Before defaults: " ++ show ds ++ "\n" ++ show (map fst (class_methods ci)))
let ds_defs = insertDefaults i iname (class_defaults ci) ns ds
logLvl 3 ("After defaults: " ++ show ds_defs ++ "\n")
let ds' = reorderDefs (map fst (class_methods ci)) $ ds_defs
iLOG ("Reordered: " ++ show ds' ++ "\n")
mapM_ (warnMissing ds' ns iname) (map fst (class_methods ci))
mapM_ (checkInClass (map fst (class_methods ci))) (concatMap defined ds')
let wbTys = map mkTyDecl mtys
Expand Down Expand Up @@ -249,6 +252,22 @@ elabInstance info syn doc argDocs what fc cs n ps t expn ds = do
coninsert cs (PPi p@(Imp _ _ _ _) n t sc) = PPi p n t (coninsert cs sc)
coninsert cs sc = conbind cs sc

-- Reorder declarations to be in the same order as defined in the
-- class declaration (important so that we insert default definitions
-- in the right place, and so that dependencies between methods are
-- respected)
reorderDefs :: [Name] -> [PDecl] -> [PDecl]
reorderDefs ns [] = []
reorderDefs [] ds = ds
reorderDefs (n : ns) ds = case pick n [] ds of
Just (def, ds') -> def : reorderDefs ns ds'
Nothing -> reorderDefs ns ds

pick n acc [] = Nothing
pick n acc (def@(PClauses _ _ cn cs) : ds)
| nsroot n == nsroot cn = Just (def, acc ++ ds)
pick n acc (d : ds) = pick n (acc ++ [d]) ds

insertDefaults :: IState -> Name ->
[(Name, (Name, PDecl))] -> [T.Text] ->
[PDecl] -> [PDecl]
Expand Down

0 comments on commit be54e85

Please sign in to comment.