fafe598 · Idris-dev · git.iko.soy

git.iko.soy/Idris-dev

Fix bug in scoping rules for pattern matches

If a name appears in argument position which is also a constructor name, it should be pattern-bound unless there is a constructor which has zero explicit arguments.

commitfafe598a22abd3c705f964fce1100e5fba89660c authorEdwin Brady <ecb10@st-andrews.ac.uk> dateSun 20 Oct 2013, 15:12 (13 years ago) parente4343cb

1 file changed+6−3

compare with master

unifiedsplit

src/Idris/AbsSyntax.hs+6−3

src/Idris/AbsSyntax.hs+6−3

@@ -1130,19 +1130,22 @@ aiFn :: Bool -> Bool -> IState -> FC -> Name -> [PArg] -> Either Err PTerm

11301130aiFn inpat True ist fc f []

11311131 = case lookupDef f (tt_ctxt ist) of

11321132 [] -> Right $ PPatvar fc f

1133− alts -> let ialts = lookupCtxt f (idris_implicits ist) in

1133+ alts -> let ialts = lookupCtxtName f (idris_implicits ist) in

11341134 -- trace (show f ++ " " ++ show (fc, any (all imp) ialts, ialts, any constructor alts)) $

11351135 if (not (vname f) || tcname f

1136− || any constructor alts || any allImp ialts)

1136+ || any (conCaf (tt_ctxt ist)) ialts)

1137+-- any constructor alts || any allImp ialts))

11371138 then aiFn inpat False ist fc f [] -- use it as a constructor

11381139 else Right $ PPatvar fc f

11391140 where imp (PExp _ _ _ _) = False

11401141 imp _ = True

1141− allImp [] = False

1142+-- allImp [] = False

11421143 allImp xs = all imp xs

11431144 constructor (TyDecl (DCon _ _) _) = True

11441145 constructor _ = False

11451146

1147+ conCaf ctxt (n, cia) = isDConName n ctxt && allImp cia

1148+

11461149 vname (UN n) = True -- non qualified

11471150 vname _ = False

11481151