Add totality annotations to src and libs/{prelude, base}

Author: fabianhjr

libs/base/Control/App.idr

@@ -2,6 +2,8 @@ module Control.App
 
 import Data.IORef
 
+%default covering
+
 ||| `Error` is a type synonym for `Type`, specify for exception handling.
 public export
 Error : Type

libs/base/Control/App/Console.idr

@@ -2,6 +2,8 @@ module Control.App.Console
 
 import public Control.App
 
+%default total
+
 public export
 interface Console e where
   putChar : Char -> App {l} e ()

libs/base/Control/App/FileIO.idr

@@ -6,6 +6,8 @@ import Data.List
 import Data.Strings
 import System.File
 
+%default covering
+
 toFileEx : FileError -> FileEx
 toFileEx (GenericFileError i) = GenericFileEx i
 toFileEx FileReadError = FileReadError

libs/base/Control/Applicative/Const.idr

@@ -3,6 +3,8 @@ module Control.Applicative.Const
 import Data.Contravariant
 import Data.Bits
 
+%default total
+
 public export
 record Const (a : Type) (b : Type) where
   constructor MkConst

libs/base/Control/Monad/Error/Either.idr

@@ -15,6 +15,8 @@ module Control.Monad.Error.Either
 
 import Control.Monad.Trans
 
+%default total
+
 public export
 data EitherT : (e : Type) -> (m : Type -> Type) -> (a : Type) -> Type where
   MkEitherT : m (Either e a) -> EitherT e m a

libs/base/Control/Monad/Error/Interface.idr

@@ -9,6 +9,8 @@ import Control.Monad.State.State
 import Control.Monad.Trans
 import Control.Monad.Writer.CPS
 
+%default total
+
 ||| The strategy of combining computations that can throw exceptions
 ||| by bypassing bound functions
 ||| from the point an exception is thrown to the point that it is handled.

libs/base/Control/Monad/Identity.idr

@@ -2,6 +2,8 @@ module Control.Monad.Identity
 
 import Data.Bits
 
+%default total
+
 public export
 record Identity (a : Type) where
   constructor Id

libs/base/Control/Monad/Maybe.idr

@@ -14,6 +14,8 @@ module Control.Monad.Maybe
 import Control.Monad.Trans
 import Data.Maybe
 
+%default total
+
 public export
 data MaybeT : (m : Type -> Type) -> (a : Type) -> Type where
   MkMaybeT : m (Maybe a) -> MaybeT m a

libs/base/Control/Monad/RWS/CPS.idr

@@ -7,6 +7,8 @@ module Control.Monad.RWS.CPS
 import Control.Monad.Identity
 import Control.Monad.Trans
 
+%default total
+
 ||| A monad transformer adding reading an environment of type `r`,
 ||| collecting an output of type `w` and updating a state of type `s`
 ||| to an inner monad `m`.

libs/base/Control/Monad/RWS/Interface.idr

@@ -5,6 +5,8 @@ import Control.Monad.Reader.Interface
 import Control.Monad.State.Interface
 import Control.Monad.Writer.Interface
 
+%default covering
+
 public export
 interface (MonadReader r m, MonadWriter w m, MonadState s m) =>
   MonadRWS r w s m | m where