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

git.iko.soy/Idris-dev

Fix previous fix ;)

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

3 files changed+19−18

compare with master

unifiedsplit

lib/prelude.idr+1−1 src/Idris/AbsSyntax.hs+17−10 src/Idris/ElabDecls.hs+1−7

lib/prelude.idr+1−1

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

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

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

600600 en t = t

601601

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

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

602+expandParamsD :: IState ->

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

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

604605 = if n `elem` ns

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

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

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

609610 PClauses fc n' (map expandParamsC cs)

610611 where

611612 expandParamsC (PClause n lhs ws rhs ds)

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

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

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

615− (expandParams dec ps ns rhs)

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

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

614+ 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)

617619 expandParamsC (PWith n lhs ws wval ds)

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

619621 PWith n' (expandParams dec ps ns lhs)

620622 (map (expandParams dec ps ns) ws)

621623 (expandParams dec ps ns wval)

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

623−expandParamsD dec ps ns d = d

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+

630+expandParamsD ist dec ps ns d = d

624631

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

626633-- * 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)

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

144143 logLvl 5 $ show wb

145144 mapM_ (elabDecl' info) wb

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

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

166165 return (clhs, crhs)

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

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

174168 pinfo ns ps i

175169 = let ds = concatMap declared ps