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

git.iko.soy/Idris-dev

on master help sign in

Fix bug in lifting of with clauses

4ddbc65Edwin Brady14 years ago

src/Idris/AbsSyntax.hs+5−1

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

958-- | otherwise = Nothing

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

960 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 []

962 match (PRef _ n) tm

966 match (PRef _ n) tm

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

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

964 = return [(n, tm)]

968 = 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)

625 return $ PWith fc wname lhs ws wval withs'

626

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

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

628− = return $ substMatches mvars $

629+ return $ substMatches mvars $

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

630+ PApp fc (PRef fc' wname)

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

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

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

631

633

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

635+ | otherwise = Placeholder

636+

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

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

633 fullApp x = x

638 fullApp x = x

634

639