2a17e4f · Idris-dev · git.iko.soy

git.iko.soy/Idris-dev

Fix scoping rules on lhs of with clause

commit2a17e4fd6cd8f24f0dc5a55e311d09e2eff13864 authorEdwin Brady <ecb10@st-andrews.ac.uk> dateThu 18 Apr 2013, 15:04 (14 years ago) parent437526a

3 files changed+7−5

compare with master

unifiedsplit

src/Idris/AbsSyntax.hs+2 src/Idris/AbsSyntaxTree.hs+1−1 src/Idris/ElabDecls.hs+4−4

src/Idris/AbsSyntax.hs+2

@@ -1074,6 +1074,8 @@ matchClause' names i x y = checkRpts $ match (fullApp x) (fullApp y) where

10741074-- match (PRef _ n) (PRef _ n') | n == n' = return []

10751075-- | otherwise = Nothing

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

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

10781080 match (PRef _ n) tm@(PRef _ n')

10791081 | n == n' && not names &&

src/Idris/AbsSyntaxTree.hs+1−1

@@ -979,7 +979,7 @@ prettyImp impl = prettySe 10

979979showImp :: Bool -> PTerm -> String

980980showImp impl tm = se 10 tm where

981981 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

983983 se p (PInferRef fc n) = "!" ++ show n -- ++ "[" ++ show fc ++ "]"

984984 se p (PRef fc n) = if impl then show n -- ++ "[" ++ show fc ++ "]"

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

733733 -- Build the LHS as an "Infer", and pull out its type and

734734 -- pattern bindings

735735 i <- getIState

736− let lhs = addImpl i lhs_in

736+ let lhs = addImplPat i lhs_in

737737 logLvl 5 ("LHS: " ++ showImp True lhs)

738738 ((lhs', dlhs, []), _) <-

739739 tclift $ elaborate ctxt (MN 0 "patLHS") infP []

@@ -831,18 +831,18 @@ elabClause info tcgen (_, PWith fc fname lhs_in withs wval_in withblock)

831831

832832 mkAux wname toplhs ns ns' (PClause fc n tm_in (w:ws) rhs wheres)

833833 = do i <- getIState

834− let tm = addImpl i tm_in

834+ let tm = addImplPat i tm_in

835835 logLvl 2 ("Matching " ++ showImp True tm ++ " against " ++

836836 showImp True toplhs)

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

839839 Right mvars ->

840840 do logLvl 3 ("Match vars : " ++ show mvars)

841841 lhs <- updateLHS n wname mvars ns ns' (fullApp tm) w

842842 return $ PClause fc wname lhs ws rhs wheres

843843 mkAux wname toplhs ns ns' (PWith fc n tm_in (w:ws) wval withs)

844844 = do i <- getIState

845− let tm = addImpl i tm_in

845+ let tm = addImplPat i tm_in

846846 logLvl 2 ("Matching " ++ showImp True tm ++ " against " ++

847847 showImp True toplhs)

848848 withs' <- mapM (mkAuxC wname toplhs ns ns') withs