[ libs ] Strengthen some totality checks (#2304)

libs/base/Data/Fuel.idr

@@ -14,7 +14,7 @@ limit (S n) = More (limit n)
 
 ||| Provide fuel indefinitely.
 ||| This function is fundamentally partial.
-partial
 export
+covering
 forever : Fuel
 forever = More forever

libs/base/Data/Nat.idr

@@ -348,7 +348,8 @@ export partial
 divNat : Nat -> Nat -> Nat
 divNat left (S right) = divNatNZ left (S right) SIsNonZero
 
-export partial
+export
+covering
 divCeilNZ : Nat -> (y: Nat) -> (0 _ : NonZero y) -> Nat
 divCeilNZ x y p = case (modNatNZ x y p) of
   Z   => divNatNZ x y p
@@ -379,7 +380,8 @@ Integral Nat where
   div = divNat
   mod = modNat
 
-export partial
+export
+covering
 gcd : (a: Nat) -> (b: Nat) -> {auto ok: NotBothZero a b} -> Nat
 gcd a Z     = a
 gcd Z b     = b

libs/base/Data/String.idr

@@ -241,11 +241,11 @@ public export partial
 strIndex : String -> Int -> Char
 strIndex = prim__strIndex
 
-public export partial
+public export covering
 strLength : String -> Int
 strLength = prim__strLength
 
-public export partial
+public export covering
 strSubstr : Int -> Int -> String -> String
 strSubstr = prim__strSubstr
 

libs/base/System/File/ReadWrite.idr

@@ -203,7 +203,7 @@ readFilePage offset fuel fname
 |||
 ||| @ fname the name of the file to read
 export
-partial
+covering
 readFile : HasIO io => (fname : String) -> io (Either FileError String)
 readFile = (map $ map (fastConcat . snd)) . readFilePage 0 forever
 

libs/contrib/Data/List/TailRec.idr

@@ -22,21 +22,21 @@ import Syntax.WithProof
 import Data.List
 import Data.List1
 
-total
+%default total
+
 lengthAcc : List a -> Nat -> Nat
 lengthAcc [] acc = acc
 lengthAcc (_::xs) acc = lengthAcc xs $ S acc
 
-export total
+export
 length : List a -> Nat
 length xs = lengthAcc xs Z
 
-total
 lengthAccSucc : (xs : List a) -> (n : Nat) -> lengthAcc xs (S n) = S (lengthAcc xs n)
 lengthAccSucc [] _ = Refl
 lengthAccSucc (_::xs) n = rewrite lengthAccSucc xs (S n) in cong S Refl
 
-export total
+export
 length_ext : (xs : List a) -> List.length xs = Data.List.TailRec.length xs
 length_ext [] = Refl
 length_ext (_::xs) = rewrite length_ext xs in sym $ lengthAccSucc xs Z
@@ -121,7 +121,7 @@ splitOnto : List (List a) -> (a -> Bool) -> List a -> List1 (List a)
 splitOnto acc p xs =
   case Data.List.break p xs of
     (chunk, []       ) => reverseOnto (chunk ::: []) acc
-    (chunk, (c::rest)) => splitOnto (chunk::acc) p rest
+    (chunk, (c::rest)) => splitOnto (chunk::acc) p $ assert_smaller xs rest
 
 export
 split : (a -> Bool) -> List a -> List1 (List a)
@@ -136,7 +136,7 @@ splitOnto_ext  acc p xs with (@@(Data.List.break p xs))
    Refl
  splitOnto_ext acc p xs | ((chunk, c::rest)**pf) =
    rewrite pf in
-   rewrite splitOnto_ext (chunk::acc) p rest in
+   rewrite splitOnto_ext (chunk::acc) p $ assert_smaller xs rest in
    Refl
 
 export
@@ -272,6 +272,7 @@ sorted  (x :: xs@(y :: ys)) = case (x <= y) of
                                 True  => Data.List.TailRec.sorted xs
 
 export
+covering
 sorted_ext : Ord a => (xs : List a) ->
   Data.List.sorted xs = Data.List.TailRec.sorted xs
 sorted_ext []  = Refl
@@ -289,6 +290,7 @@ mergeByOnto acc order left@(x::xs) right@(y::ys) =
     LT => mergeByOnto (x :: acc) order (assert_smaller left xs)   right
     _  => mergeByOnto (y :: acc) order left                       (assert_smaller right ys)
 
+covering
 mergeByOnto_ext : (acc : List a)
                -> (order : a -> a -> Ordering)
                -> (left, right : List a)
@@ -313,6 +315,7 @@ mergeBy : (a -> a -> Ordering) -> List a -> List a -> List a
 mergeBy order left right = mergeByOnto [] order left right
 
 export
+covering
 mergeBy_ext : (order : a -> a -> Ordering) -> (left, right : List a) ->
   Data.List.mergeBy order left right =
   Data.List.TailRec.mergeBy order left right
@@ -323,6 +326,7 @@ merge : Ord a => List a -> List a -> List a
 merge = Data.List.TailRec.mergeBy compare
 
 export
+covering
 merge_ext : Ord a => (left, right : List a) ->
   Data.List.merge left right = Data.List.TailRec.merge left right
 merge_ext left right = mergeBy_ext compare left right

libs/contrib/Data/List/Views/Extra.idr

@@ -146,7 +146,7 @@ data LazyFilterRec : List a -> Type where
 
 ||| Covering function for the LazyFilterRec view.
 ||| Constructs the view lazily in linear time.
-total export
+export
 lazyFilterRec : (pred : (a -> Bool)) -> (xs : List a) -> LazyFilterRec xs
 lazyFilterRec pred [] = Exhausted []
 lazyFilterRec pred (x :: xs) with (pred x)

libs/contrib/Data/Vect/Sort.idr

@@ -3,6 +3,8 @@ module Data.Vect.Sort
 import Data.Vect
 import Data.Nat.Views
 
+%default total
+
 mutual
   sortBySplit : (n : Nat) -> (a -> a -> Ordering) -> Vect n a -> Vect n a
   sortBySplit Z cmp [] = []
@@ -19,10 +21,10 @@ mutual
         (sortBySplit m cmp (assert_smaller xs right))
 
 ||| Merge sort implementation for Vect n a
-export total
+export
 sortBy : {n : Nat} -> (cmp : a -> a -> Ordering) -> (xs : Vect n a) -> Vect n a
 sortBy cmp xs = sortBySplit n cmp xs
 
-export total
+export
 sort : Ord a => {n : Nat} -> Vect n a -> Vect n a
 sort = sortBy compare

libs/contrib/Data/Vect/Views/Extra.idr

@@ -5,6 +5,7 @@ import Control.WellFounded
 import Data.Vect
 import Data.Nat
 
+%default total
 
 ||| View for splitting a vector in half, non-recursively
 public export
@@ -16,7 +17,6 @@ data Split : Vect n a -> Type where
                 (x : a) -> (xs : Vect n a) -> (y : a) -> (ys : Vect m a) ->
                 Split (x :: xs ++ y :: ys)
 
-total
 splitHelp : {n : Nat} -> (head : a) -> (zs : Vect n a) ->
             Nat -> Split (head :: zs)
 splitHelp head [] _ = SplitOne
@@ -29,7 +29,7 @@ splitHelp head (z :: zs) (S (S k))
 
 ||| Covering function for the `Split` view
 ||| Constructs the view in linear time
-export total
+export
 split : {n : Nat} -> (xs : Vect n a) -> Split xs
 split [] = SplitNil
 split {n = S k} (x :: xs) = splitHelp x xs k

libs/network/Network/Socket.idr

@@ -174,7 +174,7 @@ export
 recvAll : HasIO io => (sock : Socket) -> io (Either SocketError String)
 recvAll sock = recvRec sock [] 64
   where
-    partial
+    covering
     recvRec : Socket -> List String -> ByteLength -> io (Either SocketError String)
     recvRec sock acc n = do res <- recv sock n
                             case res of

nix/test.nix

@@ -5,6 +5,7 @@
 , stdenv
 , runCommand
 , lib
+, which
 }:
 let
   withTests = tests: drv: