git.iko.soy/Idris-dev
on master help sign in
Fix scoping rules on lhs of with clause
2a17e4fEdwin Brady
src/Idris/AbsSyntax.hs+2
compare with master
unifiedsplit
@@ -1074,6 +1074,8 @@ matchClause' names i x y = checkRpts $ match (fullApp x) (fullApp y) where
1074-- match (PRef _ n) (PRef _ n') | n == n' = return []
1074-- match (PRef _ n) (PRef _ n') | n == n' = return []
1075-- | otherwise = Nothing
1075-- | otherwise = Nothing
1076 match (PRef f n) (PApp _ x []) = match (PRef f n) x
1076 match (PRef f n) (PApp _ x []) = match (PRef f n) x
1077+ match (PPatvar f n) xr = match (PRef f n) xr
1078+ match xr (PPatvar f n) = match xr (PRef f n)
1077 match (PApp _ x []) (PRef f n) = match x (PRef f n)
1079 match (PApp _ x []) (PRef f n) = match x (PRef f n)
1078 match (PRef _ n) tm@(PRef _ n')
1080 match (PRef _ n) tm@(PRef _ n')
1079 | n == n' && not names &&
1081 | n == n' && not names &&
src/Idris/AbsSyntaxTree.hs+1−1
@@ -979,7 +979,7 @@ prettyImp impl = prettySe 10
979showImp :: Bool -> PTerm -> String
979showImp :: Bool -> PTerm -> String
980showImp impl tm = se 10 tm where
980showImp impl tm = se 10 tm where
981 se p (PQuote r) = "![" ++ show r ++ "]"
981 se p (PQuote r) = "![" ++ show r ++ "]"
982− se p (PPatvar fc n) = show n
982+ se p (PPatvar fc n) = if impl then show n ++ "[p]" else show n
983 se p (PInferRef fc n) = "!" ++ show n -- ++ "[" ++ show fc ++ "]"
983 se p (PInferRef fc n) = "!" ++ show n -- ++ "[" ++ show fc ++ "]"
984 se p (PRef fc n) = if impl then show n -- ++ "[" ++ show fc ++ "]"
984 se p (PRef fc n) = if impl then show n -- ++ "[" ++ show fc ++ "]"
985 else showbasic n
985 else showbasic n
src/Idris/ElabDecls.hs+4−4
@@ -733,7 +733,7 @@ elabClause info tcgen (_, PWith fc fname lhs_in withs wval_in withblock)
733 -- Build the LHS as an "Infer", and pull out its type and
733 -- Build the LHS as an "Infer", and pull out its type and
734 -- pattern bindings
734 -- pattern bindings
735 i <- getIState
735 i <- getIState
736− let lhs = addImpl i lhs_in
736+ let lhs = addImplPat i lhs_in
737 logLvl 5 ("LHS: " ++ showImp True lhs)
737 logLvl 5 ("LHS: " ++ showImp True lhs)
738 ((lhs', dlhs, []), _) <-
738 ((lhs', dlhs, []), _) <-
739 tclift $ elaborate ctxt (MN 0 "patLHS") infP []
739 tclift $ elaborate ctxt (MN 0 "patLHS") infP []
@@ -831,18 +831,18 @@ elabClause info tcgen (_, PWith fc fname lhs_in withs wval_in withblock)
831
831
832 mkAux wname toplhs ns ns' (PClause fc n tm_in (w:ws) rhs wheres)
832 mkAux wname toplhs ns ns' (PClause fc n tm_in (w:ws) rhs wheres)
833 = do i <- getIState
833 = do i <- getIState
834− let tm = addImpl i tm_in
834+ let tm = addImplPat i tm_in
835 logLvl 2 ("Matching " ++ showImp True tm ++ " against " ++
835 logLvl 2 ("Matching " ++ showImp True tm ++ " against " ++
836 showImp True toplhs)
836 showImp True toplhs)
837 case matchClause i toplhs tm of
837 case matchClause i toplhs tm of
838− Left _ -> fail $ show fc ++ "with clause does not match top level"
838+ Left f -> fail $ show fc ++ ":with clause does not match top level"
839 Right mvars ->
839 Right mvars ->
840 do logLvl 3 ("Match vars : " ++ show mvars)
840 do logLvl 3 ("Match vars : " ++ show mvars)
841 lhs <- updateLHS n wname mvars ns ns' (fullApp tm) w
841 lhs <- updateLHS n wname mvars ns ns' (fullApp tm) w
842 return $ PClause fc wname lhs ws rhs wheres
842 return $ PClause fc wname lhs ws rhs wheres
843 mkAux wname toplhs ns ns' (PWith fc n tm_in (w:ws) wval withs)
843 mkAux wname toplhs ns ns' (PWith fc n tm_in (w:ws) wval withs)
844 = do i <- getIState
844 = do i <- getIState
845− let tm = addImpl i tm_in
845+ let tm = addImplPat i tm_in
846 logLvl 2 ("Matching " ++ showImp True tm ++ " against " ++
846 logLvl 2 ("Matching " ++ showImp True tm ++ " against " ++
847 showImp True toplhs)
847 showImp True toplhs)
848 withs' <- mapM (mkAuxC wname toplhs ns ns') withs
848 withs' <- mapM (mkAuxC wname toplhs ns ns') withs