92bf28e · Idris-dev · git.iko.soy

git.iko.soy/Idris-dev

on master help sign in

More name mangling

92bf28eEdwin Brady15 years ago

lib/prelude.idr+2−2

compare with master

unifiedsplit

@@ -38,7 +38,7 @@ instance Show a => Show (List a) where {

38 show' : Show a => List a -> String;

39 show' Nil = "";

40 show' (Cons x Nil) = show x;

41− show' (Cons x xs') = show x ++ ", " ++ show' xs';

41+ show' (Cons x xs) = show x ++ ", " ++ show' xs;

42 }

43}

@@ -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−14

@@ -610,22 +610,25 @@ expandParamsD ist dec ps ns (PClauses fc n cs)

610 PClauses fc n' (map expandParamsC cs)

611 where

612 expandParamsC (PClause n lhs ws rhs ds)

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

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

614+ ps'' = updateps False (namesIn ist lhs) (zip ps' [0..])

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

615 n' = if n `elem` ns then dec n else n in

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

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

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

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

617− (expandParams dec ps' ns rhs)

618+ (expandParams dec ps'' ns rhs)

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

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

619 expandParamsC (PWith n lhs ws wval ds)

620 expandParamsC (PWith n lhs ws wval ds)

621+ = let ps' = updateps True (namesIn ist wval) (zip ps [0..])

622+ ps'' = updateps False (namesIn ist lhs) (zip ps' [0..])

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

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

621− PWith n' (expandParams dec ps ns lhs)

624+ PWith n' (expandParams dec ps'' ns lhs)

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

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

623− (expandParams dec ps ns wval)

626+ (expandParams dec ps'' ns wval)

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

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

625− updateps nm [] = []

628+ updateps yn nm [] = []

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

629+ updateps yn nm (((a, t), i):as)

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

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

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

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

629

632

630expandParamsD ist dec ps ns d = d

633expandParamsD ist dec ps ns d = d

631

634