
  0 | module Core.Termination.References
  1 | 
  2 | import Core.Context.Log
  3 | 
  4 | import Libraries.Data.NameMap
  5 | 
  6 | -- Check that the names a function refers to are terminating
  7 | export
  8 | totRefs : {auto c : Ref Ctxt Defs} ->
  9 |           Defs -> List Name -> Core Terminating
 10 | totRefs defs [] = pure IsTerminating
 11 | totRefs defs (n :: ns)
 12 |     = do rest <- totRefs defs ns
 13 |          Just d <- lookupCtxtExact n (gamma defs)
 14 |               | Nothing => pure rest
 15 |          case isTerminating (totality d) of
 16 |               IsTerminating => pure rest
 17 |               Unchecked => do
 18 |                 logC "totality" 20 $ do pure $ "Totality unchecked for " ++ show !(toFullNames n)
 19 |                 pure rest
 20 |               _ => case rest of
 21 |                           NotTerminating (BadCall ns)
 22 |                              => toFullNames $ NotTerminating (BadCall (n :: ns))
 23 |                           _ => toFullNames $ NotTerminating (BadCall [n])
 24 | 
 25 | export
 26 | totRefsIn : {auto c : Ref Ctxt Defs} ->
 27 |             Defs -> Term vars -> Core Terminating
 28 | totRefsIn defs ty = totRefs defs (keys (getRefs (Resolved (-1)) ty))
 29 |