f2368e9 · Idris-dev · git.iko.soy

git.iko.soy/Idris-dev

More care with naming in where clauses

commitf2368e9cce8af766198706d998b6e8d7d4fc576e authorEdwin Brady <eb@cs.st-andrews.ac.uk> dateTue 8 Nov 2011, 23:18 (15 years ago) parent814ebda

3 files changed+17−2

compare with master

unifiedsplit

lib/prelude.idr+9 src/Core/Elaborate.hs+1−1 src/Idris/ElabDecls.hs+7−1

lib/prelude.idr+9

@@ -42,6 +42,15 @@ instance Show a => Show (List a) where {

4242 }

4343}

4444

45+instance Show a => Show (Vect a n) where {

46+ show xs = "[" ++ show' xs ++ "]" where {

47+ show' : Show a => Vect a n -> String;

48+ show' VNil = "";

49+ show' (x :: VNil) = show x;

50+ show' (x :: xs) = show x ++ ", " ++ show' xs;

51+ }

52+}

53+

4554---- Monad and instances

4655

4756infixl 5 >>= ;

src/Core/Elaborate.hs+1−1

@@ -119,7 +119,7 @@ get_instances = do ES p _ _ <- get

119119-- given a desired hole name, return a unique hole name

120120unique_hole :: Name -> Elab Name

121121unique_hole n = do ES p _ _ <- get

122− let bs = bound_in (pterm p)

122+ let bs = bound_in (pterm p) ++ bound_in (ptype p)

123123 return (uniqueName n (holes p ++ bs))

124124 where

125125 bound_in (Bind n b sc) = n : bi b ++ bound_in sc

src/Idris/ElabDecls.hs+7−1

@@ -139,7 +139,8 @@ elabClause info fc (PClause fname lhs_in withs rhs_in whereblock)

139139 let winfo = pinfo (pvars ist lhs_tm) whereblock windex

140140 let decls = concatMap declared whereblock

141141 let newargs = pvars ist lhs_tm

142− let wb = map (expandParamsD decorate newargs decls) whereblock

142+ let newargs' = updateNewargs (namesIn ist rhs_in) (zip newargs [0..])

143+ let wb = map (expandParamsD decorate newargs' decls) whereblock

143144 logLvl 5 $ show wb

144145 mapM_ (elabDecl' info) wb

145146 -- Now build the RHS, using the type of the LHS as the goal.

@@ -164,6 +165,11 @@ elabClause info fc (PClause fname lhs_in withs rhs_in whereblock)

164165 (crhs, crhsty) <- tclift $ recheck ctxt [] rhs'

165166 return (clhs, crhs)

166167 where

168+ updateNewargs nm [] = []

169+ updateNewargs nm (((a, t), i):as)

170+ | a `elem` nm = (a, t) : updateNewargs nm as

171+ | otherwise = (MN i (show fname ++ "_u"), t) : updateNewargs nm as

172+

167173 decorate x = UN [show fname ++ "#" ++ show x]

168174 pinfo ns ps i

169175 = let ds = concatMap declared ps