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

[ cleanup ] remove unused code left by previous change

Browse Source
This commit is contained in:
Steve Dunham 2024-06-18 17:29:08 -07:00 committed by Justus Matthiesen
parent 2994e23fd0
commit 1a3df3fb62
1 changed files with 0 additions and 12 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

12
src/Core/Termination/CallGraph.idr
View File

@ -105,24 +105,12 @@ mutual
do scs <- traverse (findSC defs env Unguarded pats) args do scs <- traverse (findSC defs env Unguarded pats) args
pure (concat scs) pure (concat scs)
(Guarded, Ref fc (DataCon _ _) cn, args) => (Guarded, Ref fc (DataCon _ _) cn, args) =>
do Just ty <- lookupTyExact cn (gamma defs)
| Nothing => do
log "totality" 50 $ "Lookup failed"
findSCcall defs env Guarded pats fc cn args
findSCcall defs env Guarded pats fc cn args findSCcall defs env Guarded pats fc cn args
(Toplevel, Ref fc (DataCon _ _) cn, args) => (Toplevel, Ref fc (DataCon _ _) cn, args) =>
do Just ty <- lookupTyExact cn (gamma defs)
| Nothing => do
log "totality" 50 $ "Lookup failed"
findSCcall defs env Guarded pats fc cn args
findSCcall defs env Guarded pats fc cn args findSCcall defs env Guarded pats fc cn args
(_, Ref fc Func fn, args) => (_, Ref fc Func fn, args) =>
do logC "totality" 50 $ do logC "totality" 50 $
pure $ "Looking up type of " ++ show !(toFullNames fn) pure $ "Looking up type of " ++ show !(toFullNames fn)
Just ty <- lookupTyExact fn (gamma defs)
| Nothing => do
log "totality" 50 $ "Lookup failed"
findSCcall defs env Unguarded pats fc fn args
findSCcall defs env Unguarded pats fc fn args findSCcall defs env Unguarded pats fc fn args
(_, f, args) => (_, f, args) =>
do scs <- traverse (findSC defs env Unguarded pats) args do scs <- traverse (findSC defs env Unguarded pats) args