e4da568 · Idris-dev · git.iko.soy

git.iko.soy/Idris-dev

Take more care when expanding names in nested parameter blocks

commite4da56825a5e7e16d2af109fb68f2db810e29a1f authorEdwin Brady <ecb10@st-andrews.ac.uk> dateTue 11 Dec 2012, 23:36 (14 years ago) parent9070208

2 files changed+16−3

compare with master

unifiedsplit

src/Idris/AbsSyntaxTree.hs+13 src/Idris/ElabDecls.hs+3−3

src/Idris/AbsSyntaxTree.hs+13

@@ -358,6 +358,19 @@ declared (PData _ _ _ _ (PDatadecl n _ ts)) = n : map fstt ts

358358declared (PParams _ _ ds) = concatMap declared ds

359359declared (PMutual _ ds) = concatMap declared ds

360360declared (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

361374-- declared (PImport _) = []

362375

363376defined :: PDecl -> [Name]

src/Idris/ElabDecls.hs+3−3

@@ -1079,18 +1079,18 @@ elabDecl' what info (PMutual f ps)

10791079elabDecl' what info (PParams f ns ps)

10801080 = do i <- get

10811081 iLOG $ "Expanding params block with " ++ show ns ++ " decls " ++

1082− show (concatMap declared ps)

1082+ show (concatMap tldeclared ps)

10831083 let nblock = pblock i

10841084 mapM_ (elabDecl' what info) nblock

10851085 where

1086− pinfo = let ds = concatMap declared ps

1086+ pinfo = let ds = concatMap tldeclared ps

10871087 newps = params info ++ ns

10881088 dsParams = map (\n -> (n, map fst newps)) ds

10891089 newb = addAlist dsParams (inblock info) in

10901090 info { params = newps,

10911091 inblock = newb }

10921092 pblock i = map (expandParamsD False i id ns

1093− (concatMap declared ps)) ps

1093+ (concatMap tldeclared ps)) ps

10941094

10951095elabDecl' what info (PNamespace n ps) = mapM_ (elabDecl' what ninfo) ps

10961096 where