Add missing totality annotations

src/Algebra.idr

@@ -4,6 +4,8 @@ import public Algebra.ZeroOneOmega
 import public Algebra.Semiring
 import public Algebra.Preorder
 
+%default total
+
 public export
 RigCount : Type
 RigCount = ZeroOneOmega

src/Algebra/Preorder.idr

@@ -1,5 +1,7 @@
 module Algebra.Preorder
 
+%default total
+
 ||| Preorder defines a binary relation using the `<=` operator
 public export
 interface Preorder a where

src/Algebra/ZeroOneOmega.idr

@@ -3,6 +3,8 @@ module Algebra.ZeroOneOmega
 import Algebra.Semiring
 import Algebra.Preorder
 
+%default total
+
 export
 data ZeroOneOmega = Rig0 | Rig1 | RigW
 

src/Compiler/Common.idr

@@ -22,6 +22,8 @@ import System.Directory
 import System.Info
 import System.File
 
+%default covering
+
 ||| Generic interface to some code generator
 public export
 record Codegen where

src/Control/Delayed.idr

@@ -1,6 +1,8 @@
 ||| Utilities functions for contitionally delaying values.
 module Control.Delayed
 
+%default total
+
 ||| Type-level function for a conditionally infinite type.
 public export
 inf : Bool -> Type -> Type

src/Core/Directory.idr

@@ -15,7 +15,7 @@ import System.Directory
 import System.File
 import System.Info
 
-%default covering
+%default total
 
 -- Return the name of the first file available in the list
 firstAvailable : List String -> Core (Maybe String)
@@ -27,6 +27,7 @@ firstAvailable (f :: fs)
          pure (Just f)
 
 export
+covering
 readDataFile : {auto c : Ref Ctxt Defs} ->
                String -> Core String
 readDataFile fname
@@ -101,6 +102,7 @@ dirExists dir = do Right d <- openDir dir
 
 -- Create subdirectories, if they don't exist
 export
+covering
 mkdirAll : String -> IO (Either FileError ())
 mkdirAll dir = if parse dir == emptyPath 
                   then pure (Right ())
@@ -115,6 +117,7 @@ mkdirAll dir = if parse dir == emptyPath
 -- Given a namespace (i.e. a module name), make the build directory for the
 -- corresponding ttc file
 export
+covering
 makeBuildDirectory : {auto c : Ref Ctxt Defs} ->
                      List String -> Core ()
 makeBuildDirectory ns
@@ -127,6 +130,7 @@ makeBuildDirectory ns
          pure ()
 
 export
+covering
 makeExecDirectory : {auto c : Ref Ctxt Defs} ->
                     Core ()
 makeExecDirectory
@@ -175,6 +179,7 @@ dirEntries dir
 -- returns the directory, the ipkg file name, and the directories we've
 -- gone up
 export
+covering
 findIpkgFile : IO (Maybe (String, String, String))
 findIpkgFile
     = do Just dir <- currentDir
@@ -182,6 +187,7 @@ findIpkgFile
          res <- findIpkgFile' dir ""
          pure res
   where
+    covering
     findIpkgFile' : String -> String -> IO (Maybe (String, String, String))
     findIpkgFile' dir up 
         = do Right files <- dirEntries dir

src/Core/Env.idr

@@ -3,6 +3,8 @@ module Core.Env
 import Core.TT
 import Data.List
 
+%default total
+
 -- Environment containing types and values of local variables
 public export
 data Env : (tm : List Name -> Type) -> List Name -> Type where

src/Core/FC.idr

@@ -1,5 +1,7 @@
 module Core.FC
 
+%default total
+
 public export
 FilePos : Type
 FilePos = (Int, Int)

src/Core/Metadata.idr

@@ -10,10 +10,10 @@ import Core.TT
 import Core.TTC
 
 import Data.List
-
+import System.File
 import Utils.Binary
 
-import System.File
+%default covering
 
 -- Additional data we keep about the context to support interactive editing
 

src/Core/Options.idr

@@ -11,6 +11,8 @@ import Data.Strings
 
 import System.Info
 
+%default total
+
 public export
 record Dirs where
   constructor MkDirs

src/Core/Transform.idr

@@ -7,6 +7,8 @@ import Core.TT
 
 import Data.NameMap
 
+%default total
+
 unload : List (FC, Term vars) -> Term vars -> Term vars
 unload [] fn = fn
 unload ((fc, arg) :: args) fn = unload args (App fc fn arg)
@@ -35,7 +37,7 @@ addMatch idx p val ms
                            else Nothing
 
 -- LHS of a rule must be a function application, so there's not much work
--- to do here! 
+-- to do here!
 match : MatchVars vars vs ->
         Term vars -> Term vs -> Maybe (MatchVars vars vs)
 match ms (Local _ _ idx p) val
@@ -48,6 +50,7 @@ match ms x y
          then Just ms
          else Nothing
 
+covering
 tryReplace : MatchVars vars vs -> Term vars -> Maybe (Term vs)
 tryReplace ms (Local _ _ idx p) = lookupMatch idx p ms
 tryReplace ms (Ref fc nt n) = pure (Ref fc nt n)
@@ -80,6 +83,7 @@ tryReplace ms (PrimVal fc c) = pure (PrimVal fc c)
 tryReplace ms (Erased fc i) = pure (Erased fc i)
 tryReplace ms (TType fc) = pure (TType fc)
 
+covering
 tryApply : Transform -> Term vs -> Maybe (Term vs)
 tryApply trans@(MkTransform {vars} n _ lhs rhs) tm
    = case match None lhs tm of
@@ -100,6 +104,7 @@ apply (t :: ts) tm
 
 data Upd : Type where
 
+covering
 trans : {auto c : Ref Ctxt Defs} ->
         {auto u : Ref Upd Bool} ->
         Env Term vars -> List (FC, Term vars) -> Term vars ->
@@ -135,6 +140,7 @@ trans env stk (TForce fc r tm)
          pure $ unload stk (TForce fc r tm')
 trans env stk tm = pure $ unload stk tm
 
+covering
 transLoop : {auto c : Ref Ctxt Defs} ->
             Nat -> Env Term vars -> Term vars -> Core (Term vars)
 transLoop Z env tm = pure tm
@@ -148,6 +154,7 @@ transLoop (S k) env tm
             else pure tm'
 
 export
+covering
 applyTransforms : {auto c : Ref Ctxt Defs} ->
                   Env Term vars -> Term vars -> Core (Term vars)
 applyTransforms env tm = transLoop 5 env tm

src/Core/Value.idr

@@ -7,6 +7,8 @@ import Core.TT
 
 import Data.IntMap
 
+%default covering
+
 public export
 record EvalOpts where
   constructor MkEvalOpts

src/Data/ANameMap.idr

@@ -7,6 +7,8 @@ import Data.List
 import Data.NameMap
 import Data.StringMap
 
+%default total
+
 export
 record ANameMap a where
      constructor MkANameMap

src/Data/Bool/Extra.idr

@@ -1,5 +1,7 @@
 module Data.Bool.Extra
 
+%default total
+
 public export
 andSameNeutral : (x : Bool) -> x && x = x
 andSameNeutral False = Refl

src/Data/IntMap.idr

@@ -2,7 +2,7 @@ module Data.IntMap
 
 -- Hand specialised map, for efficiency...
 
-%default covering
+%default total
 
 Key : Type
 Key = Int

src/Data/LengthMatch.idr

@@ -1,5 +1,7 @@
 module Data.LengthMatch
 
+%default total
+
 public export
 data LengthMatch : List a -> List b -> Type where
      NilMatch : LengthMatch [] []

src/Data/List/Extra.idr

@@ -1,6 +1,6 @@
 module Data.List.Extra
 
-%default covering
+%default total
 
 ||| Fetches the element at a given position.
 ||| Returns `Nothing` if the position beyond the list's end.

src/Data/NameMap.idr

@@ -4,7 +4,7 @@ import Core.Name
 
 -- Hand specialised map, for efficiency...
 
-%default covering
+%default total
 
 Key : Type
 Key = Name

src/Data/StringMap.idr

@@ -2,7 +2,7 @@ module Data.StringMap
 
 -- Hand specialised map, for efficiency...
 
-%default covering
+%default total
 
 Key : Type
 Key = String

src/Idris/Elab/Interface.idr

@@ -23,6 +23,8 @@ import Data.ANameMap
 import Data.List
 import Data.Maybe
 
+%default covering
+
 -- TODO: Check all the parts of the body are legal
 -- TODO: Deal with default superclass implementations
 

src/Idris/IDEMode/Commands.idr

@@ -6,7 +6,7 @@ import public Idris.REPLOpts
 
 import System.File
 
-%default covering
+%default total
 
 public export
 data SExp = SExpList (List SExp)
@@ -186,7 +186,7 @@ escape = pack . concatMap escapeChar . unpack
 
 export
 Show SExp where
-  show (SExpList xs) = "(" ++ showSep " " (map show xs) ++ ")"
+  show (SExpList xs) = assert_total $ "(" ++ showSep " " (map show xs) ++ ")"
   show (StringAtom str) = "\"" ++ escape str ++ "\""
   show (BoolAtom b) = ":" ++ show b
   show (IntegerAtom i) = show i

src/Idris/IDEMode/Holes.idr

@@ -7,14 +7,16 @@ import Idris.Syntax
 
 import Idris.IDEMode.Commands
 
+%default covering
+
 public export
 record HolePremise where
   constructor MkHolePremise
   name         : Name
   type         : PTerm
-  multiplicity : RigCount  
+  multiplicity : RigCount
   isImplicit   : Bool
-  
+
 
 public export
 record HoleData where
@@ -25,7 +27,7 @@ record HoleData where
 
 ||| If input is a hole, return number of locals in scope at binding
 ||| point
-export  
+export
 isHole : GlobalDef -> Maybe Nat
 isHole def
     = case definition def of

src/Idris/IDEMode/MakeClause.idr

@@ -8,6 +8,8 @@ import Data.List
 import Data.Nat
 import Data.Strings
 
+%default total
+
 -- Implement make-with and make-case from the IDE mode
 
 showRHSName : Name -> String

src/Idris/IDEMode/Parser.idr

@@ -14,6 +14,8 @@ import Text.Parser
 import Utils.Either
 import Utils.String
 
+%default total
+
 %hide Text.Lexer.symbols
 %hide Parser.Lexer.Source.symbols
 
@@ -42,6 +44,7 @@ idelex str
                           Comment _ => False
                           _ => True
 
+covering
 sexp : Rule SExp
 sexp
     = do symbol ":"; exactIdent "True"
@@ -67,6 +70,7 @@ ideParser str p
 
 
 export
+covering
 parseSExp : String -> Either (ParseError Token) SExp
 parseSExp inp
     = ideParser inp (do c <- sexp; eoi; pure c)

src/Idris/IDEMode/REPL.idr

@@ -45,6 +45,8 @@ import System.File
 import Network.Socket
 import Network.Socket.Data
 
+%default covering
+
 %foreign "C:fdopen,libc 6"
 prim__fdopen : Int -> String -> PrimIO AnyPtr
 

src/Idris/IDEMode/SyntaxHighlight.idr

@@ -10,6 +10,8 @@ import Idris.IDEMode.Commands
 
 import Data.List
 
+%default covering
+
 data Decoration : Type where
   Typ : Decoration
   Function : Decoration

src/Idris/IDEMode/TokenLine.idr

@@ -4,6 +4,8 @@ module Idris.IDEMode.TokenLine
 import Parser.Lexer.Source
 import Text.Lexer
 
+%default total
+
 public export
 RawName : Type
 RawName = String

src/Idris/ProcessIdr.idr

@@ -28,6 +28,8 @@ import Data.NameMap
 
 import System.File
 
+%default covering
+
 processDecl : {auto c : Ref Ctxt Defs} ->
               {auto u : Ref UST UState} ->
               {auto s : Ref Syn SyntaxInfo} ->

src/Idris/REPLCommon.idr

@@ -13,6 +13,8 @@ import Idris.Syntax
 
 import Data.List
 
+%default covering
+
 -- Output informational messages, unless quiet flag is set
 export
 iputStrLn : {auto o : Ref ROpts REPLOpts} ->

src/Idris/REPLOpts.idr

@@ -5,6 +5,8 @@ import Idris.Syntax
 import Data.Strings
 import System.File
 
+%default total
+
 public export
 data OutputMode
   = IDEMode Integer File File

src/Idris/SetOptions.idr

@@ -17,6 +17,8 @@ import IdrisPaths
 import Data.So
 import System
 
+%default covering
+
 -- TODO: Version numbers on dependencies
 export
 addPkgDir : {auto c : Ref Ctxt Defs} ->

src/Idris/Version.idr

@@ -4,6 +4,8 @@ module Idris.Version
 import IdrisPaths
 import Data.List
 
+%default total
+
 ||| Semantic versioning with optional tag
 ||| See [semver](https://semver.org/) for proper definition of semantic versioning
 public export

src/Parser/Package.idr

@@ -9,6 +9,8 @@ import public Parser.Support
 import System.File
 import Utils.Either
 
+%default total
+
 export
 runParser : String -> Rule ty -> Either (ParseError Token) ty
 runParser str p
@@ -17,6 +19,7 @@ runParser str p
          Right (fst parsed)
 
 export
+covering
 parseFile : (fn : String) -> Rule ty -> IO (Either (ParseError Token) ty)
 parseFile fn p
     = do Right str <- readFile fn

src/TTImp/Elab.idr

@@ -19,6 +19,8 @@ import Data.IntMap
 import Data.List
 import Data.NameMap
 
+%default covering
+
 findPLetRenames : {vars : _} ->
                   Term vars -> List (Name, (RigCount, Name))
 findPLetRenames (Bind fc n (PLet c (Local _ _ idx p) ty) sc)

src/TTImp/Elab/Check.idr

@@ -21,6 +21,8 @@ import Data.List
 import Data.NameMap
 import Data.StringMap
 
+%default covering
+
 public export
 data ElabMode = InType | InLHS RigCount | InExpr | InTransform
 

src/TTImp/Elab/Utils.idr

@@ -10,6 +10,8 @@ import Core.Value
 import TTImp.Elab.Check
 import TTImp.TTImp
 
+%default covering
+
 detagSafe : Defs -> NF [] -> Core Bool
 detagSafe defs (NTCon _ n _ _ args)
     = do Just (TCon _ _ _ _ _ _ _ (Just detags)) <- lookupDefExact n (gamma defs)

src/TTImp/Impossible.idr

@@ -10,6 +10,8 @@ import TTImp.TTImp
 
 import Data.List
 
+%default covering
+
 -- This file contains support for building a guess at the term on the LHS of an 
 -- 'impossible' case, in order to help build a tree of covered cases for
 -- coverage checking. Since the LHS by definition won't be well typed, we are

src/TTImp/Parser.idr

@@ -18,6 +18,8 @@ topDecl : FileName -> IndentInfo -> Rule ImpDecl
 export
 collectDefs : List ImpDecl -> List ImpDecl
 
+%default covering
+
 %hide Prelude.(>>=)
 %hide Core.Core.(>>=)
 %hide Prelude.pure

src/TTImp/ProcessDecls.idr

@@ -24,6 +24,8 @@ import Data.List
 import Data.Maybe
 import Data.NameMap
 
+%default covering
+
 -- Implements processDecl, declared in TTImp.Elab.Check
 process : {vars : _} ->
           {auto c : Ref Ctxt Defs} ->

src/TTImp/ProcessDef.idr

@@ -30,6 +30,8 @@ import Data.Either
 import Data.List
 import Data.NameMap
 
+%default covering
+
 mutual
   mismatchNF : {vars : _} ->
                Defs -> NF vars -> NF vars -> Core Bool

src/TTImp/ProcessRecord.idr

@@ -17,6 +17,8 @@ import TTImp.Utils
 
 import Data.List
 
+%default covering
+
 mkDataTy : FC -> List (Name, RigCount, PiInfo RawImp, RawImp) -> RawImp
 mkDataTy fc [] = IType fc
 mkDataTy fc ((n, c, p, ty) :: ps)

src/TTImp/ProcessTransform.idr

@@ -12,6 +12,8 @@ import TTImp.Elab.Check
 import TTImp.ProcessDef -- for checking LHS
 import TTImp.TTImp
 
+%default covering
+
 export
 processTransform : {vars : _} ->
                    {auto c : Ref Ctxt Defs} ->

src/TTImp/WithClause.idr

@@ -7,6 +7,8 @@ import TTImp.TTImp
 
 import Data.List
 
+%default covering
+
 matchFail : FC -> Core a
 matchFail loc = throw (GenericMsg loc "With clause does not match parent")
 

src/Utils/Either.idr

@@ -1,5 +1,7 @@
 module Utils.Either
 
+%default total
+
 export
 mapError : (a -> c) -> Either a b -> Either c b
 mapError f e = either (Left . f) (Right . id) e

src/Utils/Hex.idr

@@ -2,6 +2,8 @@ module Utils.Hex
 
 import Data.Primitives.Views
 
+%default total
+
 hexDigit : Int -> Char
 hexDigit 0 = '0'
 hexDigit 1 = '1'
@@ -29,7 +31,8 @@ asHex n = pack $ asHex' n []
     asHex' : Int -> List Char -> List Char
     asHex' 0 hex = hex
     asHex' n hex with (n `divides` 16)
-      asHex' (16 * div + rem) hex | DivBy div rem _ = asHex' div (hexDigit rem :: hex)
+      asHex' (16 * div + rem) hex | DivBy div rem _ =
+        assert_total $ asHex' div (hexDigit rem :: hex)
 
 export
 fromHexDigit : Char -> Maybe Int

src/Utils/Octal.idr

@@ -2,6 +2,8 @@ module Utils.Octal
 
 import Data.Primitives.Views
 
+%default total
+
 octDigit : Int -> Char
 octDigit 0 = '0'
 octDigit 1 = '1'
@@ -21,7 +23,8 @@ asOct n = pack $ asOct' n []
     asOct' : Int -> List Char -> List Char
     asOct' 0 oct = oct
     asOct' n oct with (n `divides` 8)
-      asOct' (8 * div + rem) oct | DivBy div rem _ = asOct' div (octDigit rem :: oct)
+      asOct' (8 * div + rem) oct | DivBy div rem _ =
+        assert_total $ asOct' div (octDigit rem :: oct)
 
 export
 fromOctDigit : Char -> Maybe Int

src/Yaffle/Main.idr

@@ -25,6 +25,8 @@ import Data.So
 import Data.Strings
 import System
 
+%default covering
+
 usage : String
 usage = "Usage: yaffle <input file> [--timing]"