Clean up some assert_total instances (#1644)

libs/base/Data/IOArray.idr

@@ -53,7 +53,7 @@ newArrayCopy newsize arr
              then pure ()
              else do el <- primIO $ prim__arrayGet old pos
                      primIO $ prim__arraySet new pos el
-                     assert_total (copyFrom old new (pos - 1))
+                     copyFrom old new $ assert_smaller pos (pos - 1)
 
 export
 toList : HasIO io => IOArray elem -> io (List (Maybe elem))
@@ -75,8 +75,7 @@ fromList ns
   where
     addToArray : Int -> List (Maybe elem) -> IOArray elem -> io ()
     addToArray loc [] arr = pure ()
-    addToArray loc (Nothing :: ns) arr
-        = assert_total (addToArray (loc + 1) ns arr)
+    addToArray loc (Nothing :: ns) arr = addToArray (loc + 1) ns arr
     addToArray loc (Just el :: ns) arr
         = do primIO $ prim__arraySet (content arr) loc (Just el)
-             assert_total (addToArray (loc + 1) ns arr)
+             addToArray (loc + 1) ns arr

libs/prelude/Prelude/Types.idr

@@ -588,7 +588,7 @@ unpack str = unpack' (prim__cast_IntegerInt (natToInteger (length str)) - 1) str
     unpack' pos str acc
         = if pos < 0
              then acc
-             else assert_total $ unpack' (pos - 1) str (assert_total (prim__strIndex str pos)::acc)
+             else unpack' (assert_smaller pos (pos - 1)) str $ (assert_total $ prim__strIndex str pos) :: acc
 
 -- This function runs fast when compiled but won't compute at compile time.
 -- If you need to unpack strings at compile time, use Prelude.unpack.

src/Core/CaseTree.idr

@@ -236,6 +236,7 @@ export
 Weaken CaseTree where
   weakenNs ns t = insertCaseNames zero ns t
 
+total
 getNames : (forall vs . NameMap Bool -> Term vs -> NameMap Bool) ->
            NameMap Bool -> CaseTree vars -> NameMap Bool
 getNames add ns sc = getSet ns sc
@@ -249,8 +250,7 @@ getNames add ns sc = getSet ns sc
 
       getAltSets : NameMap Bool -> List (CaseAlt vs) -> NameMap Bool
       getAltSets ns [] = ns
-      getAltSets ns (a :: as)
-          = assert_total $ getAltSets (getAltSet ns a) as
+      getAltSets ns (a :: as) = getAltSets (getAltSet ns a) as
 
       getSet : NameMap Bool -> CaseTree vs -> NameMap Bool
       getSet ns (Case _ x ty xs) = getAltSets ns xs

src/Core/TT.idr

@@ -850,11 +850,12 @@ Eq a => Eq (Binder a) where
   (==) = eqBinderBy (==)
 
 export
+total
 Eq (Term vars) where
   (==) (Local _ _ idx _) (Local _ _ idx' _) = idx == idx'
   (==) (Ref _ _ n) (Ref _ _ n') = n == n'
   (==) (Meta _ _ i args) (Meta _ _ i' args')
-      = assert_total (i == i' && args == args')
+      = i == i' && assert_total (args == args')
   (==) (Bind _ _ b sc) (Bind _ _ b' sc')
       = assert_total (b == b' && sc == believe_me sc')
   (==) (App _ f a) (App _ f' a') = f == f' && a == a'
@@ -869,11 +870,12 @@ Eq (Term vars) where
 
 -- Check equality, ignoring variable naming
 export
+total
 eqTerm : Term vs -> Term vs' -> Bool
 eqTerm (Local _ _ idx _) (Local _ _ idx' _) = idx == idx'
 eqTerm (Ref _ _ n) (Ref _ _ n') = n == n'
 eqTerm (Meta _ _ i args) (Meta _ _ i' args')
-    = assert_total (i == i' && all (uncurry eqTerm) (zip args args'))
+    = i == i' && assert_total (all (uncurry eqTerm) (zip args args'))
 eqTerm (Bind _ _ b sc) (Bind _ _ b' sc')
     = assert_total (eqBinderBy eqTerm b b') && eqTerm sc sc'
 eqTerm (App _ f a) (App _ f' a') = eqTerm f f' && eqTerm a a'

src/Libraries/Text/Distance/Levenshtein.idr

@@ -25,7 +25,7 @@ spec a b = loop (fastUnpack a) (fastUnpack b) where
 ||| Dynamic programming
 export
 compute : HasIO io => String -> String -> io Nat
-compute a b = assert_total $ do
+compute a b = do
   let w = strLength a
   let h = strLength b
   -- In mat[i][j], we store the distance between
@@ -43,7 +43,8 @@ compute a b = assert_total $ do
 
   -- We introduce a specialised `read` for ease of use
   let get = \i, j => case !(read {io} mat i j) of
-        Nothing => idris_crash "INTERNAL ERROR: Badly initialised matrix"
+        Nothing => assert_total $
+          idris_crash "INTERNAL ERROR: Badly initialised matrix"
         Just n => pure n
 
   -- We fill the matrix from the bottom up, using the same formula we used
@@ -53,8 +54,8 @@ compute a b = assert_total $ do
       -- here we change Levenshtein slightly so that we may only substitute
       -- alpha / numerical characters for similar ones. This avoids suggesting
       -- "#" as a replacement for an out of scope "n".
-      let cost = let c = strIndex a (i-1)
-                     d = strIndex b (j-1)
+      let cost = let c = assert_total $ strIndex a (i-1)
+                     d = assert_total $ strIndex b (j-1)
                  in if c == d then 0 else
                     if isAlpha c && isAlpha d then 1 else
                     if isDigit c && isDigit d then 1 else 2

src/Libraries/Utils/String.idr

@@ -19,7 +19,7 @@ stripQuotes = stripSurrounds 1 1
 export
 lowerFirst : String -> Bool
 lowerFirst "" = False
-lowerFirst str = assert_total (isLower (prim__strHead str))
+lowerFirst str = isLower $ assert_total $ prim__strHead str
 
 escapeGeneric : Char -> List Char -> String -> String
 escapeGeneric esc toEscape = pack . foldr escape [] . unpack