4ddbc65 · Idris-dev · git.iko.soy

git.iko.soy/Idris-dev

Fix bug in lifting of with clauses

Need to make sure _ remains _ on lifting - stray variables were creeping in after 'match'.

commit4ddbc65bddc56be67e993f09c37901660f3d9d81 authorEdwin Brady <ecb10@st-andrews.ac.uk> dateWed 21 Nov 2012, 15:42 (14 years ago) parent11d1aa3

2 files changed+12−3

unifiedsplit

src/Idris/AbsSyntax.hs+5−1

@@ -958,7 +958,11 @@ matchClause' names i x y = checkRpts $ match (fullApp x) (fullApp y) where

958958-- | otherwise = Nothing

959959 match (PRef f n) (PApp _ x []) = match (PRef f n) x

960960 match (PApp _ x []) (PRef f n) = match x (PRef f n)

961− match (PRef _ n) (PRef _ n') | n == n' = return []

961+ match (PRef _ n) tm@(PRef _ n')

962+ | n == n' && not names &&

963+ (not (isConName Nothing n (tt_ctxt i)) || tm == Placeholder)

964+ = return [(n, tm)]

965+ | n == n' = return []

962966 match (PRef _ n) tm

963967 | not names && (not (isConName Nothing n (tt_ctxt i)) || tm == Placeholder)

964968 = return [(n, tm)]

src/Idris/ElabDecls.hs+7−2

@@ -625,10 +625,15 @@ elabClause info tcgen (_, PWith fc fname lhs_in withs wval_in withblock)

625625 return $ PWith fc wname lhs ws wval withs'

626626

627627 updateLHS n wname mvars ns (PApp fc (PRef fc' n') args) w

628− = return $ substMatches mvars $

629− PApp fc (PRef fc' wname) (map (pexp . (PRef fc')) ns ++ [pexp w])

628+ = let ns' = map (keepMvar (map fst mvars) fc') ns in

629+ return $ substMatches mvars $

630+ PApp fc (PRef fc' wname)

631+ (map pexp ns' ++ [pexp w])

630632 updateLHS n wname mvars ns tm w = fail $ "Not implemented match " ++ show tm

631633

634+ keepMvar mvs fc v | v `elem` mvs = PRef fc v

635+ | otherwise = Placeholder

636+

632637 fullApp (PApp _ (PApp fc f args) xs) = fullApp (PApp fc f (args ++ xs))

633638 fullApp x = x

634639