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

git.iko.soy/Idris-dev

Check that methods are part of a class when defining instances

commit0432a7095e0e8d83dce0e6cfb9568bceb964a9cf authorEdwin Brady <eb@cs.st-andrews.ac.uk> dateTue 14 Feb 2012, 14:21 (15 years ago) parenta87be32

2 files changed+18

unifiedsplit

src/Idris/AbsSyntax.hs+10

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

472472declared (PNamespace _ ds) = concatMap declared ds

473473-- declared (PImport _) = []

474474

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+

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

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

477487updateN _ n = n

src/Idris/ElabDecls.hs+8

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

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

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

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

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

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

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

691692 -- 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

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

781782 | otherwise = return ()

782783

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+

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

784792 clauseFor m ns _ = False

785793