idris-lang/Idris2
1
1
Fork 0
mirror of https://github.com/idris-lang/Idris2.git synced 2024-11-28 11:05:17 +03:00
Code Issues Projects Releases Wiki Activity

Some productivity checker fixes

Browse Source 
Getting there... it still needs to be a bit cleverer at allowing
"obviously productive" functions before we can switch it on though.
This commit is contained in:
Edwin Brady 2020-05-22 15:08:42 +01:00
parent b6a3c51129
commit 088bb52f58
1 changed files with 5 additions and 0 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

5
src/Core/Termination.idr
View File

@ -79,6 +79,8 @@ mutual
-- If we're Guarded and find a Delay, continue with the argument as InDelay
findSC defs env Guarded pats (TDelay _ _ _ tm)
= findSC defs env InDelay pats tm
findSC defs env g pats (TDelay _ _ _ tm)
= findSC defs env g pats tm
findSC defs env g pats tm
= case (g, getFnArgs tm) of
-- If we're InDelay and find a constructor (or a function call which is
@ -91,6 +93,9 @@ mutual
(InDelay, _, args) =>
do scs <- traverse (findSC defs env Unguarded pats) args
pure (concat scs)
(Guarded, Ref fc (DataCon _ _) cn, args) =>
do scs <- traverse (findSC defs env Guarded pats) args
pure (concat scs)
(Toplevel, Ref fc (DataCon _ _) cn, args) =>
do scs <- traverse (findSC defs env Guarded pats) args
pure (concat scs)