f2368e9 · Idris-dev · git.iko.soy

lib/prelude.idr+9

compare with master

unifiedsplit

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

42 }

43}

44

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+

45---- Monad and instances

54---- Monad and instances

46

55

47infixl 5 >>= ;

56infixl 5 >>= ;

src/Core/Elaborate.hs+1−1

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

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

120unique_hole :: Name -> Elab Name

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

122− let bs = bound_in (pterm p)

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

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

124 where

125 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)

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

140 let decls = concatMap declared whereblock

141 let newargs = pvars ist lhs_tm

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

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

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

143 logLvl 5 $ show wb

144 logLvl 5 $ show wb

144 mapM_ (elabDecl' info) wb

145 mapM_ (elabDecl' info) wb

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

146 -- 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)

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

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

165 return (clhs, crhs)

166 return (clhs, crhs)

166 where

167 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+

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

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

168 pinfo ns ps i

174 pinfo ns ps i

169 = let ds = concatMap declared ps

175 = let ds = concatMap declared ps