[cleanup] Remove Libraries.Data.Bool.Extra

idris2api.ipkg

@@ -115,7 +115,6 @@ modules =
     Libraries.Control.Delayed,
 
     Libraries.Data.ANameMap,
-    Libraries.Data.Bool.Extra,
     Libraries.Data.DList,
     Libraries.Data.IMaybe,
     Libraries.Data.IntMap,

src/Compiler/Scheme/Common.idr

@@ -8,7 +8,6 @@ import Core.Context
 import Core.Name
 import Core.TT
 
-import Libraries.Data.Bool.Extra
 import Data.List
 import Data.Vect
 
@@ -294,17 +293,17 @@ mutual
   used n (NmRef _ _) = False
   used n (NmLam _ _ sc) = used n sc
   used n (NmLet _ _ v sc) = used n v || used n sc
-  used n (NmApp _ f args) = used n f || anyTrue (map (used n) args)
-  used n (NmCon _ _ _ _ args) = anyTrue (map (used n) args)
-  used n (NmOp _ _ args) = anyTrue (toList (map (used n) args))
-  used n (NmExtPrim _ _ args) = anyTrue (map (used n) args)
+  used n (NmApp _ f args) = used n f || any (used n) args
+  used n (NmCon _ _ _ _ args) = any (used n) args
+  used n (NmOp _ _ args) = any (used n) (toList args)
+  used n (NmExtPrim _ _ args) = any (used n) args
   used n (NmForce _ _ t) = used n t
   used n (NmDelay _ _ t) = used n t
   used n (NmConCase _ sc alts def)
-      = used n sc || anyTrue (map (usedCon n) alts)
+      = used n sc || any (usedCon n) alts
             || maybe False (used n) def
   used n (NmConstCase _ sc alts def)
-      = used n sc || anyTrue (map (usedConst n) alts)
+      = used n sc || any (usedConst n) alts
             || maybe False (used n) def
   used n _ = False
 

src/Core/AutoSearch.idr

@@ -9,7 +9,6 @@ import Core.TT
 import Core.Unify
 import Core.Value
 
-import Libraries.Data.Bool.Extra
 import Data.Either
 import Data.List
 import Data.Maybe
@@ -222,12 +221,12 @@ usableLocal loc defaults env (NDCon _ n _ _ args)
     = do defs <- get Ctxt
          us <- traverse (usableLocal loc defaults env)
                         !(traverse (evalClosure defs) $ map snd args)
-         pure (allTrue us)
+         pure (all id us)
 usableLocal loc defaults env (NApp _ (NLocal _ _ _) args)
     = do defs <- get Ctxt
          us <- traverse (usableLocal loc defaults env)
                         !(traverse (evalClosure defs) $ map snd args)
-         pure (allTrue us)
+         pure (all id us)
 usableLocal loc defaults env (NBind fc x (Pi _ _ _ _) sc)
     = do defs <- get Ctxt
          usableLocal loc defaults env

src/Core/CaseTree.idr

@@ -2,10 +2,10 @@ module Core.CaseTree
 
 import Core.TT
 
-import Libraries.Data.Bool.Extra
+import Data.Bool
 import Data.List
-import Libraries.Data.NameMap
 
+import Libraries.Data.NameMap
 import Libraries.Text.PrettyPrint.Prettyprinter
 
 %default covering
@@ -159,7 +159,7 @@ mutual
   eqTree (Case i _ _ alts) (Case i' _ _ alts')
       = i == i'
        && length alts == length alts'
-       && allTrue (zipWith eqAlt alts alts')
+       && all (uncurry eqAlt) (zip alts alts')
   eqTree (STerm _ t) (STerm _ t') = eqTerm t t'
   eqTree (Unmatched _) (Unmatched _) = True
   eqTree Impossible Impossible = True

src/Core/Coverage.idr

@@ -8,10 +8,10 @@ import Core.Normalise
 import Core.TT
 import Core.Value
 
-import Libraries.Data.Bool.Extra
 import Data.List
 import Data.Maybe
 import Data.Strings
+
 import Libraries.Data.NameMap
 import Libraries.Text.PrettyPrint.Prettyprinter
 import Libraries.Data.String.Extra
@@ -48,7 +48,7 @@ conflictMatch ((x, tm) :: ms) = conflictArgs x tm ms || conflictMatch ms
     findN i tm
         = let (Ref _ (DataCon _ _) _, args) = getFnArgs tm
                    | _ => False in
-              anyTrue (map (findN i) args)
+              any (findN i) args
 
     -- Assuming in normal form. Look for: mismatched constructors, or
     -- a name appearing strong rigid in the other term
@@ -56,15 +56,15 @@ conflictMatch ((x, tm) :: ms) = conflictArgs x tm ms || conflictMatch ms
     conflictTm (Local _ _ i _) tm
         = let (Ref _ (DataCon _ _) _, args) = getFnArgs tm
                    | _ => False in
-              anyTrue (map (findN i) args)
+              any (findN i) args
     conflictTm tm (Local _ _ i _)
         = let (Ref _ (DataCon _ _) _, args) = getFnArgs tm
                    | _ => False in
-              anyTrue (map (findN i) args)
+              any (findN i) args
     conflictTm tm tm'
         = let (f, args) = getFnArgs tm
               (f', args') = getFnArgs tm' in
-          clash f f' || anyTrue (zipWith conflictTm args args')
+          clash f f' || any (uncurry conflictTm) (zip args args')
 
     conflictArgs : Name -> Term vars -> List (Name, Term vars) -> Bool
     conflictArgs n tm [] = False

src/Core/LinearCheck.idr

@@ -11,7 +11,6 @@ import Core.UnifyState
 import Core.Value
 import Core.TT
 
-import Libraries.Data.Bool.Extra
 import Data.List
 
 %default covering
@@ -108,7 +107,7 @@ mutual
            let vars = mapMaybe (findLocal (getArgs lhs)) argpos
            hs <- traverse (\vsel => updateHoleUsage useInHole vsel [] rhs)
                           vars
-           pure (anyTrue hs)
+           pure (any id hs)
     where
       findArg : Nat -> List (Term vars) -> List Nat
       findArg i [] = []

src/Core/TT.idr

@@ -3,12 +3,12 @@ module Core.TT
 import public Core.FC
 import public Core.Name
 
-import Libraries.Data.Bool.Extra
 import Data.List
 import Data.Nat
-import Libraries.Data.NameMap
 import Data.Vect
 import Decidable.Equality
+
+import Libraries.Data.NameMap
 import Libraries.Text.PrettyPrint.Prettyprinter
 import Libraries.Text.PrettyPrint.Prettyprinter.Util
 
@@ -873,7 +873,7 @@ 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' && allTrue (zipWith eqTerm args args'))
+    = assert_total (i == i' && 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/Core/Unify.idr

@@ -12,10 +12,10 @@ import Core.TT
 import public Core.UnifyState
 import Core.Value
 
-import Libraries.Data.Bool.Extra
-import Libraries.Data.IntMap
 import Data.List
 import Data.List.Views
+
+import Libraries.Data.IntMap
 import Libraries.Data.NameMap
 
 %default covering
@@ -1500,7 +1500,7 @@ solveConstraints : {auto c : Ref Ctxt Defs} ->
 solveConstraints umode smode
     = do ust <- get UST
          progress <- traverse (retryGuess umode smode) (toList (guesses ust))
-         when (anyTrue progress) $
+         when (any id progress) $
                solveConstraints umode Normal
 
 export
@@ -1511,7 +1511,7 @@ solveConstraintsAfter start umode smode
     = do ust <- get UST
          progress <- traverse (retryGuess umode smode)
                               (filter afterStart (toList (guesses ust)))
-         when (anyTrue progress) $
+         when (any id progress) $
                solveConstraintsAfter start umode Normal
   where
     afterStart : (Int, a) -> Bool

src/Libraries/Data/Bool/Extra.idr

@@ -1,48 +0,0 @@
-module Libraries.Data.Bool.Extra
-
-%default total
-
-public export
-andSameNeutral : (x : Bool) -> x && x = x
-andSameNeutral False = Refl
-andSameNeutral True = Refl
-
-public export
-andFalseFalse : (x : Bool) -> x && False = False
-andFalseFalse False = Refl
-andFalseFalse True = Refl
-
-public export
-andTrueNeutral : (x : Bool) -> x && True = x
-andTrueNeutral False = Refl
-andTrueNeutral True = Refl
-
-public export
-orSameNeutral : (x : Bool) -> x || x = x
-orSameNeutral False = Refl
-orSameNeutral True = Refl
-
-public export
-orFalseNeutral : (x : Bool) -> x || False = x
-orFalseNeutral False = Refl
-orFalseNeutral True = Refl
-
-public export
-orTrueTrue : (x : Bool) -> x || True = True
-orTrueTrue False = Refl
-orTrueTrue True = Refl
-
-public export
-orSameAndRightNeutral : (x, right : Bool) -> x || (x && right) = x
-orSameAndRightNeutral False _ = Refl
-orSameAndRightNeutral True _ = Refl
-
-export
-anyTrue : List Bool -> Bool
-anyTrue [] = False
-anyTrue (x :: xs) = x || anyTrue xs
-
-export
-allTrue : List Bool -> Bool
-allTrue [] = True
-allTrue (x :: xs) = x && allTrue xs

src/Libraries/Text/Lexer.idr

@@ -1,6 +1,6 @@
 module Libraries.Text.Lexer
 
-import Libraries.Data.Bool.Extra
+import Data.Bool
 import Data.List
 import Data.Nat
 

src/Libraries/Text/Lexer/Core.idr

@@ -1,11 +1,11 @@
 module Libraries.Text.Lexer.Core
 
-import public Libraries.Control.Delayed
-import Libraries.Data.Bool.Extra
 import Data.List
 import Data.Maybe
 import Data.Nat
 import Data.Strings
+
+import public Libraries.Control.Delayed
 import public Libraries.Text.Bounded
 
 %default total

src/Libraries/Text/Lexer/Tokenizer.idr

@@ -1,17 +1,18 @@
 module Libraries.Text.Lexer.Tokenizer
 
-import public Libraries.Control.Delayed
-import public Libraries.Text.Bounded
-import Libraries.Data.Bool.Extra
+import Data.List
+import Data.Either
+import Data.Nat
+import Data.Strings
+
 import Libraries.Data.String.Extra
 import Libraries.Text.Lexer.Core
 import Libraries.Text.Lexer
 import Libraries.Text.PrettyPrint.Prettyprinter
 import Libraries.Text.PrettyPrint.Prettyprinter.Util
-import Data.List
-import Data.Either
-import Data.Nat
-import Data.Strings
+
+import public Libraries.Control.Delayed
+import public Libraries.Text.Bounded
 
 %default total
 

src/Libraries/Text/Parser.idr

@@ -1,6 +1,6 @@
 module Libraries.Text.Parser
 
-import Libraries.Data.Bool.Extra
+import Data.Bool
 import Data.List
 import Data.List1
 import Data.Nat

src/Libraries/Text/Parser/Core.idr

@@ -1,7 +1,8 @@
 module Libraries.Text.Parser.Core
 
-import Libraries.Data.Bool.Extra
+import Data.Bool
 import Data.List
+
 import public Libraries.Control.Delayed
 import public Libraries.Text.Bounded
 

src/TTImp/Elab/Ambiguity.idr

@@ -15,9 +15,9 @@ import TTImp.Elab.Check
 import TTImp.Elab.Delayed
 import TTImp.TTImp
 
-import Libraries.Data.Bool.Extra
 import Data.List
 import Data.Strings
+
 import Libraries.Data.StringMap
 
 %default covering
@@ -299,7 +299,7 @@ pruneByType env target alts
          let matches = mapMaybe id matches_in
          logNF "elab.prune" 10 "Prune by" env target
          log "elab.prune" 10 (show matches)
-         res <- if anyTrue (map fst matches)
+         res <- if any Builtin.fst matches
                 -- if there's any concrete matches, drop the non-concrete
                 -- matches marked as '%allow_overloads' from the possible set
                    then do keep <- filterCore (notOverloadable defs) matches

src/TTImp/Interactive/ExprSearch.idr

@@ -28,7 +28,6 @@ import TTImp.TTImp
 import TTImp.Unelab
 import TTImp.Utils
 
-import Libraries.Data.Bool.Extra
 import Data.Either
 import Data.List
 
@@ -431,13 +430,13 @@ tryRecursive fc rig opts env ty topty rdata
       appsDiff : Term vs -> Term vs' -> List (Term vs) -> List (Term vs') ->
                  Bool
       appsDiff (Ref _ (DataCon _ _) f) (Ref _ (DataCon _ _) f') args args'
-         = f /= f' || anyTrue (zipWith argDiff args args')
+         = f /= f' || any (uncurry argDiff) (zip args args')
       appsDiff (Ref _ (TyCon _ _) f) (Ref _ (TyCon _ _) f') args args'
-         = f /= f' || anyTrue (zipWith argDiff args args')
+         = f /= f' || any (uncurry argDiff) (zip args args')
       appsDiff (Ref _ _ f) (Ref _ _ f') args args'
          = f == f'
            && length args == length args'
-           && anyTrue (zipWith argDiff args args')
+           && any (uncurry argDiff) (zip args args')
       appsDiff (Ref _ (DataCon _ _) f) (Local _ _ _ _) _ _ = True
       appsDiff (Local _ _ _ _) (Ref _ (DataCon _ _) f) _ _ = True
       appsDiff f f' [] [] = argDiff f f'

src/TTImp/ProcessBuiltin.idr

@@ -2,11 +2,11 @@
 -- If we get more builtins it might be wise to move each builtin to it's own file.
 module TTImp.ProcessBuiltin
 
-import Libraries.Data.Bool.Extra
 import Data.Fin
-import Libraries.Data.NameMap
 import Data.List
 
+import Libraries.Data.NameMap
+
 import Core.CaseTree
 import Core.Core
 import Core.Context
@@ -112,7 +112,7 @@ termConMatch : Term vs -> Term vs' -> Bool
 termConMatch (Local _ _ x _) (Local _ _ y _) = x == y
 termConMatch (Ref _ _ n) (Ref _ _ m) = n == m
 termConMatch (Meta _ _ i args0) (Meta _ _ j args1)
-    = i == j && allTrue (zipWith termConMatch args0 args1)
+    = i == j && all (uncurry termConMatch) (zip args0 args1)
     -- I don't understand how they're equal if args are different lengths
     -- but this is what's in Core.TT.
 termConMatch (Bind _ _ b s) (Bind _ _ c t) = eqBinderBy termConMatch b c && termConMatch s t