0dec4a1 · Idris-dev · git.iko.soy

git.iko.soy/Idris-dev

on master help sign in

Fix name substitution in with functions

0dec4a1Edwin Brady11 years ago

CHANGELOG.md+1

@@ -31,6 +31,7 @@

31* `Control.WellFounded` module removed, and added to the Prelude as

32 `Prelude.WellFounded`.

33* Added `Data.List.Views` with views on `List` and their covering functions.

34+* Added `Data.Nat.Views` with views on `Nat` and their covering functions.

35## Miscellaneous updates

36## Miscellaneous updates

src/Idris/AbsSyntax.hs+9−6

@@ -2218,17 +2218,20 @@ matchClause' names i x y = checkRpts $ match (fullApp x) (fullApp y) where

2218substMatches :: [(Name, PTerm)] -> PTerm -> PTerm

2219substMatches ms = substMatchesShadow ms []

2220

2221−substMatchesShadow :: [(Name, PTerm)] -> [Name] -> PTerm -> PTerm

2221+-- substMatchesShadow :: [(Name, PTerm)] -> [Name] -> PTerm -> PTerm

2222−substMatchesShadow [] shs t = t

2222+-- substMatchesShadow [] shs t = t

2223−substMatchesShadow ((n,tm):ns) shs t

2223+-- substMatchesShadow ((n,tm):ns) shs t

2224− = substMatchShadow n shs tm (substMatchesShadow ns shs t)

2224+-- = substMatchShadow n shs tm (substMatchesShadow ns shs t)

2225

2226substMatch :: Name -> PTerm -> PTerm -> PTerm

2227substMatch n = substMatchShadow n []

2228

2229substMatchShadow :: Name -> [Name] -> PTerm -> PTerm -> PTerm

2230−substMatchShadow n shs tm t = sm shs t where

2230+substMatchShadow n shs tm t = substMatchesShadow [(n, tm)] shs t

2231+

2232+substMatchesShadow :: [(Name, PTerm)] -> [Name] -> PTerm -> PTerm

2233+substMatchesShadow nmap shs t = sm shs t where

2231− sm xs (PRef _ _ n') | n == n' = tm

2234+ sm xs (PRef _ _ n) | Just tm <- lookup n nmap = tm

2232 sm xs (PLam fc x xfc t sc) = PLam fc x xfc (sm xs t) (sm xs sc)

2235 sm xs (PLam fc x xfc t sc) = PLam fc x xfc (sm xs t) (sm xs sc)

2233 sm xs (PPi p x fc t sc)

2236 sm xs (PPi p x fc t sc)

2234 | x `elem` xs

2237 | x `elem` xs