on master help sign in
Take more care when expanding names in nested parameter blocks
e4da568Edwin Brady
src/Idris/AbsSyntaxTree.hs+13
@@ -358,6 +358,19 @@ declared (PData _ _ _ _ (PDatadecl n _ ts)) = n : map fstt ts
358declared (PParams _ _ ds) = concatMap declared ds
358declared (PParams _ _ ds) = concatMap declared ds
359declared (PMutual _ ds) = concatMap declared ds
359declared (PMutual _ ds) = concatMap declared ds
360declared (PNamespace _ ds) = concatMap declared ds
360declared (PNamespace _ ds) = concatMap declared ds
361+
362+-- get the names declared, not counting nested parameter blocks
363+tldeclared :: PDecl -> [Name]
364+tldeclared (PFix _ _ _) = []
365+tldeclared (PTy _ _ _ _ n t) = [n]
366+tldeclared (PPostulate _ _ _ _ n t) = [n]
367+tldeclared (PClauses _ _ n _) = [] -- not a declaration
368+tldeclared (PRecord _ _ _ n _ _ c _) = [n, c]
369+tldeclared (PData _ _ _ _ (PDatadecl n _ ts)) = n : map fstt ts
370+ where fstt (_, a, _, _) = a
371+tldeclared (PParams _ _ ds) = []
372+tldeclared (PMutual _ ds) = concatMap tldeclared ds
373+tldeclared (PNamespace _ ds) = concatMap tldeclared ds
361-- declared (PImport _) = []
374-- declared (PImport _) = []
362
375
363defined :: PDecl -> [Name]
376defined :: PDecl -> [Name]
src/Idris/ElabDecls.hs+3−3
@@ -1079,18 +1079,18 @@ elabDecl' what info (PMutual f ps)
1079elabDecl' what info (PParams f ns ps)
1079elabDecl' what info (PParams f ns ps)
1080 = do i <- get
1080 = do i <- get
1081 iLOG $ "Expanding params block with " ++ show ns ++ " decls " ++
1081 iLOG $ "Expanding params block with " ++ show ns ++ " decls " ++
1082− show (concatMap declared ps)
1082+ show (concatMap tldeclared ps)
1083 let nblock = pblock i
1083 let nblock = pblock i
1084 mapM_ (elabDecl' what info) nblock
1084 mapM_ (elabDecl' what info) nblock
1085 where
1085 where
1086− pinfo = let ds = concatMap declared ps
1086+ pinfo = let ds = concatMap tldeclared ps
1087 newps = params info ++ ns
1087 newps = params info ++ ns
1088 dsParams = map (\n -> (n, map fst newps)) ds
1088 dsParams = map (\n -> (n, map fst newps)) ds
1089 newb = addAlist dsParams (inblock info) in
1089 newb = addAlist dsParams (inblock info) in
1090 info { params = newps,
1090 info { params = newps,
1091 inblock = newb }
1091 inblock = newb }
1092 pblock i = map (expandParamsD False i id ns
1092 pblock i = map (expandParamsD False i id ns
1093− (concatMap declared ps)) ps
1093+ (concatMap tldeclared ps)) ps
1094
1094
1095elabDecl' what info (PNamespace n ps) = mapM_ (elabDecl' what ninfo) ps
1095elabDecl' what info (PNamespace n ps) = mapM_ (elabDecl' what ninfo) ps
1096 where
1096 where