27f5a9c · Idris-dev · git.iko.soy

git.iko.soy/Idris-dev

on master help sign in

Fix previous fix ;)

27f5a9cEdwin Brady15 years ago

lib/prelude.idr+1−1

compare with master

unifiedsplit

@@ -47,7 +47,7 @@ instance Show a => Show (Vect a n) 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;

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

51 }

52}

src/Idris/AbsSyntax.hs+17−10

@@ -599,28 +599,35 @@ expandParams dec ps ns tm = en tm

599 en (PApp fc f as) = PApp fc (en f) (map (fmap en) as)

600 en t = t

601

602+expandParamsD :: IState ->

602−expandParamsD :: (Name -> Name) -> [(Name, PTerm)] -> [Name] -> PDecl -> PDecl

603+ (Name -> Name) -> [(Name, PTerm)] -> [Name] -> PDecl -> PDecl

603−expandParamsD dec ps ns (PTy syn fc n ty)

604+expandParamsD ist dec ps ns (PTy syn fc n ty)

604 = if n `elem` ns

605 = if n `elem` ns

605 then PTy syn fc (dec n) (piBind ps (expandParams dec ps ns ty))

606 then PTy syn fc (dec n) (piBind ps (expandParams dec ps ns ty))

606 else PTy syn fc n (expandParams dec ps ns ty)

607 else PTy syn fc n (expandParams dec ps ns ty)

607−expandParamsD dec ps ns (PClauses fc n cs)

608+expandParamsD ist dec ps ns (PClauses fc n cs)

608 = let n' = if n `elem` ns then dec n else n in

609 = let n' = if n `elem` ns then dec n else n in

609 PClauses fc n' (map expandParamsC cs)

610 PClauses fc n' (map expandParamsC cs)

610 where

611 where

611 expandParamsC (PClause n lhs ws rhs ds)

612 expandParamsC (PClause n lhs ws rhs ds)

613+ = let ps' = updateps (namesIn ist rhs) (zip ps [0..])

612− = let n' = if n `elem` ns then dec n else n in

614+ n' = if n `elem` ns then dec n else n in

613− PClause n' (expandParams dec ps ns lhs)

615+ PClause n' (expandParams dec ps' ns lhs)

614− (map (expandParams dec ps ns) ws)

616+ (map (expandParams dec ps' ns) ws)

615− (expandParams dec ps ns rhs)

617+ (expandParams dec ps' ns rhs)

616− (map (expandParamsD dec ps ns) ds)

618+ (map (expandParamsD ist dec ps' ns) ds)

617 expandParamsC (PWith n lhs ws wval ds)

619 expandParamsC (PWith n lhs ws wval ds)

618 = let n' = if n `elem` ns then dec n else n in

620 = let n' = if n `elem` ns then dec n else n in

619 PWith n' (expandParams dec ps ns lhs)

621 PWith n' (expandParams dec ps ns lhs)

620 (map (expandParams dec ps ns) ws)

622 (map (expandParams dec ps ns) ws)

621 (expandParams dec ps ns wval)

623 (expandParams dec ps ns wval)

622− (map (expandParamsD dec ps ns) ds)

624+ (map (expandParamsD ist dec ps ns) ds)

625+ updateps nm [] = []

626+ updateps nm (((a, t), i):as)

627+ | a `elem` nm = (a, t) : updateps nm as

628+ | otherwise = (MN i (show n ++ "_u"), t) : updateps nm as

629+

623−expandParamsD dec ps ns d = d

630+expandParamsD ist dec ps ns d = d

624

631

625-- Calculate a priority for a type, for deciding elaboration order

632-- Calculate a priority for a type, for deciding elaboration order

626-- * if it's just a type variable or concrete type, do it early (0)

633-- * if it's just a type variable or concrete type, do it early (0)

src/Idris/ElabDecls.hs+1−7

@@ -139,8 +139,7 @@ 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..])

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

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

144 logLvl 5 $ show wb

143 logLvl 5 $ show wb

145 mapM_ (elabDecl' info) wb

144 mapM_ (elabDecl' info) wb

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

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

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

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

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

166 return (clhs, crhs)

165 return (clhs, crhs)

167 where

166 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−

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

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

174 pinfo ns ps i

168 pinfo ns ps i

175 = let ds = concatMap declared ps

169 = let ds = concatMap declared ps