
  0 | module TTImp.ProcessDecls.Totality
  1 | 
  2 | import Core.Context.Log
  3 | import Core.Termination
  4 | 
  5 | import Libraries.Data.NameMap
  6 | 
  7 | %default covering
  8 | 
  9 | export
 10 | checkTotalityOK : {auto c : Ref Ctxt Defs} ->
 11 |                   Name -> Core (Maybe Error)
 12 | checkTotalityOK (NS _ (MN {})) = pure Nothing -- not interested in generated names
 13 | checkTotalityOK (NS _ (CaseBlock {})) = pure Nothing -- case blocks checked elsewhere
 14 | checkTotalityOK n
 15 |     = do defs <- get Ctxt
 16 |          Just gdef <- lookupCtxtExact n (gamma defs)
 17 |               | Nothing => pure Nothing
 18 |          let fc = location gdef
 19 | 
 20 |          let treq = fromMaybe !getDefaultTotalityOption (findSetTotal (flags gdef))
 21 | 
 22 |          -- #524: need to check positivity even if we're not in a total context
 23 |          -- because a definition coming later may need to know it is positive
 24 |          case definition gdef of
 25 |            TCon {} => ignore $ checkPositive fc n
 26 |            _ => pure ()
 27 | 
 28 |          -- Once that is done, we build up errors if necessary
 29 |          let tot = totality gdef
 30 |          log "totality" 3 $ show n ++ " must be: " ++ show treq
 31 |          case treq of
 32 |             PartialOK => pure Nothing
 33 |             CoveringOnly => checkCovering fc (isCovering tot)
 34 |             Total => checkTotality fc
 35 |   where
 36 |     checkCovering : FC -> Covering -> Core (Maybe Error)
 37 |     checkCovering fc IsCovering = pure Nothing
 38 |     checkCovering fc cov
 39 |         = pure (Just (NotCovering fc n cov))
 40 | 
 41 |     checkTotality : FC -> Core (Maybe Error)
 42 |     checkTotality fc
 43 |         = do ignore $ logTime 3 ("Checking Termination " ++ show n) (checkTotal fc n)
 44 |              -- ^ checked lazily, so better calculate here
 45 |              t <- getTotality fc n
 46 |              err <- checkCovering fc (isCovering t)
 47 |              maybe (case isTerminating t of
 48 |                          NotTerminating p => pure (Just (NotTotal fc n p))
 49 |                          _ => pure Nothing)
 50 |                    (pure . Just) err
 51 | 
 52 | -- Check totality of all the names added in the file, and return a list of
 53 | -- totality errors.
 54 | -- Do this at the end of processing a file (or a batch of definitions) since
 55 | -- they might be mutually dependent so we need all the definitions to be able
 56 | -- to check accurately.
 57 | export
 58 | getTotalityErrors : {auto c : Ref Ctxt Defs} ->
 59 |                     Core (List Error)
 60 | getTotalityErrors
 61 |     = do defs <- get Ctxt
 62 |          errs <- traverse checkTotalityOK (keys (toSave defs))
 63 |          pure (mapMaybe id errs)
 64 |