c01becb · Idris-dev · git.iko.soy

git.iko.soy/Idris-dev

Don't bind pattern variables if they're in scope

commitc01becb372d7afc2ea9bf9cc7f41516cd68ba847 authorEdwin Brady <eb@cs.st-andrews.ac.uk> dateTue 15 Nov 2011, 16:00 (15 years ago) parent2e02cf6

2 files changed+10−3

unifiedsplit

src/Idris/AbsSyntax.hs+1

@@ -887,6 +887,7 @@ dumpDecl (PClass _ _ cs n ps ds)

887887 = "class " ++ show cs ++ " " ++ show n ++ " " ++ show ps ++ "\n" ++ dumpDecls ds

888888dumpDecl (PInstance _ _ cs n _ t ds)

889889 = "instance " ++ show cs ++ " " ++ show n ++ " " ++ show t ++ "\n" ++ dumpDecls ds

890+dumpDecl _ = "..."

890891-- dumpDecl (PImport i) = "import " ++ i

891892

892893-- syntactic match of a against b, returning pair of variables in a

src/Idris/ElabDecls.hs+9−3

@@ -536,9 +536,15 @@ elab ist info pattern tm

536536 pimp (MN 0 "P") Placeholder,

537537 pexp l, pexp r])

538538 elab' (PRef fc n) | pattern && not (inparamBlock n)

539− = erun fc $

540− try (do apply (Var n) []; solve)

541− (patvar n)

539+ = do ctxt <- get_context

540+ let sc = case lookupCtxt n ctxt of

541+ Nothing -> True

542+ _ -> False

543+ if sc

544+ then erun fc $

545+ try (do apply (Var n) []; solve)

546+ (patvar n)

547+ else do apply (Var n) []; solve

542548 where inparamBlock n = case lookupCtxt n (inblock info) of

543549 Nothing -> False

544550 _ -> True