ilyakooo0/Idris-dev
1
0
Fork 0
mirror of https://github.com/ilyakooo0/Idris-dev.git synced 2024-09-22 06:29:37 +03:00
Code Issues Projects Releases Wiki Activity

Only rewrite _ under @!

Browse Source 
Also generate actual fresh names.
This commit is contained in:
David Raymond Christiansen 2015-01-10 17:40:43 -08:00
parent 0b23ef2a19
commit 8a03679d24
1 changed files with 8 additions and 2 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

10
src/Idris/Elab/AsPat.hs
View File

@ -33,10 +33,16 @@ collectAs x = return x
-- | Replace _-patterns under @-patterns with fresh names that can be
-- used on the RHS
replaceUnderscore :: PTerm -> PTerm
replaceUnderscore tm = evalState (transformM replaceUnderscore' tm) 0
replaceUnderscore tm = evalState (transformM (underAs replaceUnderscore') tm) 0
where
underAs :: (PTerm -> State Int PTerm) -> PTerm -> State Int PTerm
underAs f (PAs fc n tm) = PAs fc n <$> transformM f tm
underAs f x = return x
fresh :: State Int Name
fresh = flip sMN "underscorePatVar" <$> get
fresh = modify (+1) >> flip sMN "underscorePatVar" <$> get
replaceUnderscore' :: PTerm -> State Int PTerm
replaceUnderscore' Placeholder = PRef emptyFC <$> fresh
replaceUnderscore' tm = return tm