b57da9d · Idris-dev · git.iko.soy

git.iko.soy/Idris-dev

Pattern matching lambda fix

It's only a pattern matching lambda if it binds a constructor name. We don't want to introduce 'case' unnecessarily since it is restricted in the type inference it can do, so only do that if it really is binding a constructor name. Fixes #2150

commitb57da9db3c61c81fcd8a6244734e1d416c75b7d6 authorEdwin Brady <ecb10@st-andrews.ac.uk> dateThu 21 Apr 2016, 13:12 (11 years ago) parent0dec4a1

1 file changed+7−8

compare with master

unifiedsplit

src/Idris/AbsSyntax.hs+7−8

src/Idris/AbsSyntax.hs+7−8

@@ -1772,17 +1772,16 @@ addImpl' inpat env infns imp_meths ist ptm

17721772 (ai inpat qq env ds t)

17731773 (ai inpat qq env ds f)

17741774

1775− -- If the name in a lambda is a constructor name, do this as a 'case'

1776− -- instead (it is harmless to do so, especially since the lambda will

1777− -- be lifted anyway!)

1775+ -- If the name in a lambda is an unapplied data constructor name, do this

1776+ -- as a 'case' instead because we'll expect to match on it

17781777 ai inpat qq env ds (PLam fc n nfc ty sc)

1779− = case lookupDef n (tt_ctxt ist) of

1780− [] -> let ty' = ai inpat qq env ds ty

1781− sc' = ai inpat qq ((n, Just ty):env) ds sc in

1782− PLam fc n nfc ty' sc'

1783− _ -> ai inpat qq env ds (PLam fc (sMN 0 "lamp") NoFC ty

1778+ = if canBeDConName n (tt_ctxt ist)

1779+ then ai inpat qq env ds (PLam fc (sMN 0 "lamp") NoFC ty

17841780 (PCase fc (PRef fc [] (sMN 0 "lamp") )

17851781 [(PRef fc [] n, sc)]))

1782+ else let ty' = ai inpat qq env ds ty

1783+ sc' = ai inpat qq ((n, Just ty):env) ds sc in

1784+ PLam fc n nfc ty' sc'

17861785 ai inpat qq env ds (PLet fc n nfc ty val sc)

17871786 = case lookupDef n (tt_ctxt ist) of

17881787 [] -> let ty' = ai inpat qq env ds ty