c01becb · Idris-dev · git.iko.soy

git.iko.soy/Idris-dev

on master help sign in

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

c01becbEdwin Brady15 years ago

src/Idris/AbsSyntax.hs+1

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

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

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

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

890+dumpDecl _ = "..."

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

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

891

892

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

893-- 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

536 pimp (MN 0 "P") Placeholder,

537 pexp l, pexp r])

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

539+ = do ctxt <- get_context

540+ let sc = case lookupCtxt n ctxt of

541+ Nothing -> True

542+ _ -> False

543+ if sc

539− = erun fc $

544+ then erun fc $

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

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

541− (patvar n)

546+ (patvar n)

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

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

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

543 Nothing -> False

549 Nothing -> False

544 _ -> True

550 _ -> True