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

git.iko.soy/Idris-dev

More name mangling

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

2 files changed+19−16

compare with master

unifiedsplit

lib/prelude.idr+2−2 src/Idris/AbsSyntax.hs+17−14

lib/prelude.idr+2−2

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

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

3939 show' Nil = "";

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

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

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

4242 }

4343}

4444

@@ -47,7 +47,7 @@ instance Show a => Show (Vect a n) where {

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

4848 show' VNil = "";

4949 show' (x :: VNil) = show x;

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

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

5151 }

5252}

5353

src/Idris/AbsSyntax.hs+17−14

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

610610 PClauses fc n' (map expandParamsC cs)

611611 where

612612 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..])

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

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

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

617− (expandParams dec ps' ns rhs)

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

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

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

618+ (expandParams dec ps'' ns rhs)

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

619620 expandParamsC (PWith n lhs ws wval ds)

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

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

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

623− (expandParams dec ps ns wval)

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

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

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

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

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

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

626+ (expandParams dec ps'' ns wval)

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

628+ updateps yn nm [] = []

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

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

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

629632

630633expandParamsD ist dec ps ns d = d

631634