From 97366f022df7ceaab832b1aa8371a2f17334c745 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Fabi=C3=A1n=20Heredia=20Montiel?= Date: Mon, 25 May 2020 10:05:12 -0500 Subject: [PATCH] Add missing totality annotations --- src/Algebra.idr | 2 ++ src/Algebra/Preorder.idr | 2 ++ src/Algebra/ZeroOneOmega.idr | 2 ++ src/Compiler/Common.idr | 2 ++ src/Control/Delayed.idr | 2 ++ src/Core/Directory.idr | 8 +++++++- src/Core/Env.idr | 2 ++ src/Core/FC.idr | 2 ++ src/Core/Metadata.idr | 4 ++-- src/Core/Options.idr | 2 ++ src/Core/Transform.idr | 9 ++++++++- src/Core/Value.idr | 2 ++ src/Data/ANameMap.idr | 2 ++ src/Data/Bool/Extra.idr | 2 ++ src/Data/IntMap.idr | 2 +- src/Data/LengthMatch.idr | 2 ++ src/Data/List/Extra.idr | 2 +- src/Data/NameMap.idr | 2 +- src/Data/StringMap.idr | 2 +- src/Idris/Elab/Interface.idr | 2 ++ src/Idris/IDEMode/Commands.idr | 4 ++-- src/Idris/IDEMode/Holes.idr | 8 +++++--- src/Idris/IDEMode/MakeClause.idr | 2 ++ src/Idris/IDEMode/Parser.idr | 4 ++++ src/Idris/IDEMode/REPL.idr | 2 ++ src/Idris/IDEMode/SyntaxHighlight.idr | 2 ++ src/Idris/IDEMode/TokenLine.idr | 2 ++ src/Idris/ProcessIdr.idr | 2 ++ src/Idris/REPLCommon.idr | 2 ++ src/Idris/REPLOpts.idr | 2 ++ src/Idris/SetOptions.idr | 2 ++ src/Idris/Version.idr | 2 ++ src/Parser/Package.idr | 3 +++ src/TTImp/Elab.idr | 2 ++ src/TTImp/Elab/Check.idr | 2 ++ src/TTImp/Elab/Utils.idr | 2 ++ src/TTImp/Impossible.idr | 2 ++ src/TTImp/Parser.idr | 2 ++ src/TTImp/ProcessDecls.idr | 2 ++ src/TTImp/ProcessDef.idr | 2 ++ src/TTImp/ProcessRecord.idr | 2 ++ src/TTImp/ProcessTransform.idr | 2 ++ src/TTImp/WithClause.idr | 2 ++ src/Utils/Either.idr | 2 ++ src/Utils/Hex.idr | 5 ++++- src/Utils/Octal.idr | 5 ++++- src/Yaffle/Main.idr | 2 ++ 47 files changed, 111 insertions(+), 15 deletions(-) diff --git a/src/Algebra.idr b/src/Algebra.idr index 3e3b30f11..9b850a74f 100644 --- a/src/Algebra.idr +++ b/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 diff --git a/src/Algebra/Preorder.idr b/src/Algebra/Preorder.idr index ab59133f4..385c5861a 100644 --- a/src/Algebra/Preorder.idr +++ b/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 diff --git a/src/Algebra/ZeroOneOmega.idr b/src/Algebra/ZeroOneOmega.idr index 6ea13f1f6..8ea753b98 100644 --- a/src/Algebra/ZeroOneOmega.idr +++ b/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 diff --git a/src/Compiler/Common.idr b/src/Compiler/Common.idr index b80abb19b..cd98887e0 100644 --- a/src/Compiler/Common.idr +++ b/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 diff --git a/src/Control/Delayed.idr b/src/Control/Delayed.idr index 4be93fa71..0219a82cc 100644 --- a/src/Control/Delayed.idr +++ b/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 diff --git a/src/Core/Directory.idr b/src/Core/Directory.idr index 0d6ef6fe8..c6547d271 100644 --- a/src/Core/Directory.idr +++ b/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 diff --git a/src/Core/Env.idr b/src/Core/Env.idr index 19b9a6c3a..9399aaf24 100644 --- a/src/Core/Env.idr +++ b/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 diff --git a/src/Core/FC.idr b/src/Core/FC.idr index 2b586b7ce..2d39a66d8 100644 --- a/src/Core/FC.idr +++ b/src/Core/FC.idr @@ -1,5 +1,7 @@ module Core.FC +%default total + public export FilePos : Type FilePos = (Int, Int) diff --git a/src/Core/Metadata.idr b/src/Core/Metadata.idr index 8192c7875..5eee88bba 100644 --- a/src/Core/Metadata.idr +++ b/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 diff --git a/src/Core/Options.idr b/src/Core/Options.idr index fa4a976d1..d9b7d3416 100644 --- a/src/Core/Options.idr +++ b/src/Core/Options.idr @@ -11,6 +11,8 @@ import Data.Strings import System.Info +%default total + public export record Dirs where constructor MkDirs diff --git a/src/Core/Transform.idr b/src/Core/Transform.idr index 7ce171be0..f6f5bb238 100644 --- a/src/Core/Transform.idr +++ b/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 diff --git a/src/Core/Value.idr b/src/Core/Value.idr index 2a051c777..66506de32 100644 --- a/src/Core/Value.idr +++ b/src/Core/Value.idr @@ -7,6 +7,8 @@ import Core.TT import Data.IntMap +%default covering + public export record EvalOpts where constructor MkEvalOpts diff --git a/src/Data/ANameMap.idr b/src/Data/ANameMap.idr index 3a0f650e8..861fed8ee 100644 --- a/src/Data/ANameMap.idr +++ b/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 diff --git a/src/Data/Bool/Extra.idr b/src/Data/Bool/Extra.idr index 95f31a97e..31aac57ad 100644 --- a/src/Data/Bool/Extra.idr +++ b/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 diff --git a/src/Data/IntMap.idr b/src/Data/IntMap.idr index 312b97c59..1adf74868 100644 --- a/src/Data/IntMap.idr +++ b/src/Data/IntMap.idr @@ -2,7 +2,7 @@ module Data.IntMap -- Hand specialised map, for efficiency... -%default covering +%default total Key : Type Key = Int diff --git a/src/Data/LengthMatch.idr b/src/Data/LengthMatch.idr index bac69bacb..bebde240c 100644 --- a/src/Data/LengthMatch.idr +++ b/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 [] [] diff --git a/src/Data/List/Extra.idr b/src/Data/List/Extra.idr index ca19f6f8e..83a02f568 100644 --- a/src/Data/List/Extra.idr +++ b/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. diff --git a/src/Data/NameMap.idr b/src/Data/NameMap.idr index 88a208195..73bfe623e 100644 --- a/src/Data/NameMap.idr +++ b/src/Data/NameMap.idr @@ -4,7 +4,7 @@ import Core.Name -- Hand specialised map, for efficiency... -%default covering +%default total Key : Type Key = Name diff --git a/src/Data/StringMap.idr b/src/Data/StringMap.idr index 3aef4ebc7..1fc820e81 100644 --- a/src/Data/StringMap.idr +++ b/src/Data/StringMap.idr @@ -2,7 +2,7 @@ module Data.StringMap -- Hand specialised map, for efficiency... -%default covering +%default total Key : Type Key = String diff --git a/src/Idris/Elab/Interface.idr b/src/Idris/Elab/Interface.idr index 6121a44ae..7c6efee71 100644 --- a/src/Idris/Elab/Interface.idr +++ b/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 diff --git a/src/Idris/IDEMode/Commands.idr b/src/Idris/IDEMode/Commands.idr index 5676079c8..cf29cbd30 100644 --- a/src/Idris/IDEMode/Commands.idr +++ b/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 diff --git a/src/Idris/IDEMode/Holes.idr b/src/Idris/IDEMode/Holes.idr index fbf97d029..deb86a362 100644 --- a/src/Idris/IDEMode/Holes.idr +++ b/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 diff --git a/src/Idris/IDEMode/MakeClause.idr b/src/Idris/IDEMode/MakeClause.idr index 6250be0c4..0610e2856 100644 --- a/src/Idris/IDEMode/MakeClause.idr +++ b/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 diff --git a/src/Idris/IDEMode/Parser.idr b/src/Idris/IDEMode/Parser.idr index d6054d4a2..0c87b03ca 100644 --- a/src/Idris/IDEMode/Parser.idr +++ b/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) diff --git a/src/Idris/IDEMode/REPL.idr b/src/Idris/IDEMode/REPL.idr index f48cfb910..73e3d79fe 100644 --- a/src/Idris/IDEMode/REPL.idr +++ b/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 diff --git a/src/Idris/IDEMode/SyntaxHighlight.idr b/src/Idris/IDEMode/SyntaxHighlight.idr index 2c29585a7..aab7aa7cf 100644 --- a/src/Idris/IDEMode/SyntaxHighlight.idr +++ b/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 diff --git a/src/Idris/IDEMode/TokenLine.idr b/src/Idris/IDEMode/TokenLine.idr index db5b986aa..4f871528e 100644 --- a/src/Idris/IDEMode/TokenLine.idr +++ b/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 diff --git a/src/Idris/ProcessIdr.idr b/src/Idris/ProcessIdr.idr index 6305282bd..96b38bddc 100644 --- a/src/Idris/ProcessIdr.idr +++ b/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} -> diff --git a/src/Idris/REPLCommon.idr b/src/Idris/REPLCommon.idr index 4e3954c09..5bd8f8f69 100644 --- a/src/Idris/REPLCommon.idr +++ b/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} -> diff --git a/src/Idris/REPLOpts.idr b/src/Idris/REPLOpts.idr index 91b8f5f67..1f42959a4 100644 --- a/src/Idris/REPLOpts.idr +++ b/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 diff --git a/src/Idris/SetOptions.idr b/src/Idris/SetOptions.idr index 62e62ff8c..4ca64ba94 100644 --- a/src/Idris/SetOptions.idr +++ b/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} -> diff --git a/src/Idris/Version.idr b/src/Idris/Version.idr index 8447cdb82..7e08d1e16 100644 --- a/src/Idris/Version.idr +++ b/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 diff --git a/src/Parser/Package.idr b/src/Parser/Package.idr index 6b1089595..a902d0a92 100644 --- a/src/Parser/Package.idr +++ b/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 diff --git a/src/TTImp/Elab.idr b/src/TTImp/Elab.idr index fbbc663a2..d22e86b6a 100644 --- a/src/TTImp/Elab.idr +++ b/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) diff --git a/src/TTImp/Elab/Check.idr b/src/TTImp/Elab/Check.idr index 4eb063455..0d63b46f7 100644 --- a/src/TTImp/Elab/Check.idr +++ b/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 diff --git a/src/TTImp/Elab/Utils.idr b/src/TTImp/Elab/Utils.idr index 2ca7080b0..1323f9c82 100644 --- a/src/TTImp/Elab/Utils.idr +++ b/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) diff --git a/src/TTImp/Impossible.idr b/src/TTImp/Impossible.idr index 2e8fbb90a..63bc91bda 100644 --- a/src/TTImp/Impossible.idr +++ b/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 diff --git a/src/TTImp/Parser.idr b/src/TTImp/Parser.idr index 9784ab98f..351f9e422 100644 --- a/src/TTImp/Parser.idr +++ b/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 diff --git a/src/TTImp/ProcessDecls.idr b/src/TTImp/ProcessDecls.idr index 09ec491ad..171b10fae 100644 --- a/src/TTImp/ProcessDecls.idr +++ b/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} -> diff --git a/src/TTImp/ProcessDef.idr b/src/TTImp/ProcessDef.idr index d447c7814..0c6fdb6e7 100644 --- a/src/TTImp/ProcessDef.idr +++ b/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 diff --git a/src/TTImp/ProcessRecord.idr b/src/TTImp/ProcessRecord.idr index b717a3f2c..c0ba0c65e 100644 --- a/src/TTImp/ProcessRecord.idr +++ b/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) diff --git a/src/TTImp/ProcessTransform.idr b/src/TTImp/ProcessTransform.idr index 5a6ff1556..014954e63 100644 --- a/src/TTImp/ProcessTransform.idr +++ b/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} -> diff --git a/src/TTImp/WithClause.idr b/src/TTImp/WithClause.idr index 4e8bac40b..ae3bdc8ef 100644 --- a/src/TTImp/WithClause.idr +++ b/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") diff --git a/src/Utils/Either.idr b/src/Utils/Either.idr index 28eb4ea4f..fd22b0e7e 100644 --- a/src/Utils/Either.idr +++ b/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 diff --git a/src/Utils/Hex.idr b/src/Utils/Hex.idr index 7f066ef8a..7ff4fb031 100644 --- a/src/Utils/Hex.idr +++ b/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 diff --git a/src/Utils/Octal.idr b/src/Utils/Octal.idr index 919403e87..f6a0f434c 100644 --- a/src/Utils/Octal.idr +++ b/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 diff --git a/src/Yaffle/Main.idr b/src/Yaffle/Main.idr index 2ddbc988c..36f2b6d00 100644 --- a/src/Yaffle/Main.idr +++ b/src/Yaffle/Main.idr @@ -25,6 +25,8 @@ import Data.So import Data.Strings import System +%default covering + usage : String usage = "Usage: yaffle [--timing]"