0432a70 · Idris-dev · git.iko.soy

git.iko.soy/Idris-dev

on master help sign in

Check that methods are part of a class when defining instances

0432a70Edwin Brady15 years ago

src/Idris/AbsSyntax.hs+10

compare with master

unifiedsplit

@@ -472,6 +472,16 @@ declared (PParams _ _ ds) = concatMap declared ds

472declared (PNamespace _ ds) = concatMap declared ds

473-- declared (PImport _) = []

474

475+defined :: PDecl -> [Name]

476+defined (PFix _ _ _) = []

477+defined (PTy _ _ _ n t) = []

478+defined (PClauses _ _ n _) = [n] -- not a declaration

479+defined (PData _ _ (PDatadecl n _ ts)) = n : map fstt ts

480+ where fstt (a, _, _) = a

481+defined (PParams _ _ ds) = concatMap defined ds

482+defined (PNamespace _ ds) = concatMap defined ds

483+-- declared (PImport _) = []

484+

475updateN :: [(Name, Name)] -> Name -> Name

485updateN :: [(Name, Name)] -> Name -> Name

476updateN ns n | Just n' <- lookup n ns = n'

486updateN ns n | Just n' <- lookup n ns = n'

477updateN _ n = n

487updateN _ n = n

src/Idris/ElabDecls.hs+8

@@ -686,6 +686,7 @@ elabInstance info syn fc cs n ps t ds

686 let ds' = insertDefaults (class_defaults ci) ns ds

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

688 mapM_ (warnMissing ds' ns) (map fst (class_methods ci))

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

689 let wb = map mkTyDecl mtys ++ map (decorateid (decorate ns)) ds'

690 let wb = map mkTyDecl mtys ++ map (decorateid (decorate ns)) ds'

690 logLvl 3 $ "Method types " ++ showSep "\n" (map (showDeclImp True . mkTyDecl) mtys)

691 logLvl 3 $ "Method types " ++ showSep "\n" (map (showDeclImp True . mkTyDecl) mtys)

691 -- get the implicit parameters that need passing through to the where block

692 -- get the implicit parameters that need passing through to the where block

@@ -780,6 +781,13 @@ elabInstance info syn fc cs n ps t ds

780 = iWarn fc $ "method " ++ show meth ++ " not defined"

781 = iWarn fc $ "method " ++ show meth ++ " not defined"

781 | otherwise = return ()

782 | otherwise = return ()

782

783

784+ checkInClass ns meth

785+ | not (null (filter (eqRoot meth) ns)) = return ()

786+ | otherwise = tclift $ tfail (At fc (Msg $

787+ show meth ++ " not a method of class " ++ show n))

788+

789+ eqRoot x y = nsroot x == nsroot y

790+

783 clauseFor m ns (PClauses _ _ m' _) = decorate ns m == decorate ns m'

791 clauseFor m ns (PClauses _ _ m' _) = decorate ns m == decorate ns m'

784 clauseFor m ns _ = False

792 clauseFor m ns _ = False

785

793