Skip to content

Commit fda76b8

Browse files
edwinbedwinb
committed
Merge github.com:idris-lang/Idris2
2 parents 97ee3d4 + 42d4c36 commit fda76b8

File tree

22 files changed

+68
-113
lines changed

22 files changed

+68
-113
lines changed

‎README.md

Lines changed: 9 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -104,6 +104,15 @@ Things still missing
104104
+ ':search' and ':apropos' at the REPL
105105
+ Metaprogramming (reflection, partial evaluation)
106106

107+
Contributions wanted
108+
-------------------
109+
110+
+ [Good first issues](https://github.com/idris-lang/Idris2/issues?q=is%3Aopen+is%3Aissue+label%3A%22good+first+issue%22)
111+
+ [Contributors wanted](https://github.com/idris-lang/Idris2/wiki/Contributions-wanted)
112+
113+
If you want to learn about Idris more, contributing to the compiler could be one
114+
way to do so. Just select one good first issue and ask about it on the [Discord](https://discord.gg/UX68fDs2jc) channel.
115+
107116
Talks
108117
-----
109118

‎idris2api.ipkg

Lines changed: 0 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -115,7 +115,6 @@ modules =
115115
Libraries.Control.Delayed,
116116

117117
Libraries.Data.ANameMap,
118-
Libraries.Data.Bool.Extra,
119118
Libraries.Data.DList,
120119
Libraries.Data.IMaybe,
121120
Libraries.Data.IntMap,

‎src/Compiler/Scheme/Common.idr

Lines changed: 6 additions & 7 deletions
Original file line numberDiff line numberDiff line change
@@ -8,7 +8,6 @@ import Core.Context
88
import Core.Name
99
import Core.TT
1010

11-
import Libraries.Data.Bool.Extra
1211
import Data.List
1312
import Data.Vect
1413

@@ -294,17 +293,17 @@ mutual
294293
used n (NmRef _ _) = False
295294
used n (NmLam _ _ sc) = used n sc
296295
used n (NmLet _ _ v sc) = used n v || used n sc
297-
used n (NmApp _ f args) = used n f || anyTrue (map (used n) args)
298-
used n (NmCon _ _ _ _ args) = anyTrue (map (used n) args)
299-
used n (NmOp _ _ args) = anyTrue (toList (map (used n) args))
300-
used n (NmExtPrim _ _ args) = anyTrue (map (used n) args)
296+
used n (NmApp _ f args) = used n f || any (used n) args
297+
used n (NmCon _ _ _ _ args) = any (used n) args
298+
used n (NmOp _ _ args) = any (used n) (toList args)
299+
used n (NmExtPrim _ _ args) = any (used n) args
301300
used n (NmForce _ _ t) = used n t
302301
used n (NmDelay _ _ t) = used n t
303302
used n (NmConCase _ sc alts def)
304-
= used n sc || anyTrue (map (usedCon n) alts)
303+
= used n sc || any (usedCon n) alts
305304
|| maybe False (used n) def
306305
used n (NmConstCase _ sc alts def)
307-
= used n sc || anyTrue (map (usedConst n) alts)
306+
= used n sc || any (usedConst n) alts
308307
|| maybe False (used n) def
309308
used n _ = False
310309

‎src/Core/AutoSearch.idr

Lines changed: 2 additions & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -9,7 +9,6 @@ import Core.TT
99
import Core.Unify
1010
import Core.Value
1111

12-
import Libraries.Data.Bool.Extra
1312
import Data.Either
1413
import Data.List
1514
import Data.Maybe
@@ -222,12 +221,12 @@ usableLocal loc defaults env (NDCon _ n _ _ args)
222221
= do defs <- get Ctxt
223222
us <- traverse (usableLocal loc defaults env)
224223
!(traverse (evalClosure defs) $ map snd args)
225-
pure (allTrue us)
224+
pure (all id us)
226225
usableLocal loc defaults env (NApp _ (NLocal _ _ _) args)
227226
= do defs <- get Ctxt
228227
us <- traverse (usableLocal loc defaults env)
229228
!(traverse (evalClosure defs) $ map snd args)
230-
pure (allTrue us)
229+
pure (all id us)
231230
usableLocal loc defaults env (NBind fc x (Pi _ _ _ _) sc)
232231
= do defs <- get Ctxt
233232
usableLocal loc defaults env

‎src/Core/CaseTree.idr

Lines changed: 3 additions & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -2,10 +2,10 @@ module Core.CaseTree
22

33
import Core.TT
44

5-
import Libraries.Data.Bool.Extra
5+
import Data.Bool
66
import Data.List
7-
import Libraries.Data.NameMap
87

8+
import Libraries.Data.NameMap
99
import Libraries.Text.PrettyPrint.Prettyprinter
1010

1111
%default covering
@@ -159,7 +159,7 @@ mutual
159159
eqTree (Case i _ _ alts) (Case i' _ _ alts')
160160
= i == i'
161161
&& length alts == length alts'
162-
&& allTrue (zipWith eqAlt alts alts')
162+
&& all (uncurry eqAlt) (zip alts alts')
163163
eqTree (STerm _ t) (STerm _ t') = eqTerm t t'
164164
eqTree (Unmatched _) (Unmatched _) = True
165165
eqTree Impossible Impossible = True

‎src/Core/Coverage.idr

Lines changed: 5 additions & 5 deletions
Original file line numberDiff line numberDiff line change
@@ -8,10 +8,10 @@ import Core.Normalise
88
import Core.TT
99
import Core.Value
1010

11-
import Libraries.Data.Bool.Extra
1211
import Data.List
1312
import Data.Maybe
1413
import Data.Strings
14+
1515
import Libraries.Data.NameMap
1616
import Libraries.Text.PrettyPrint.Prettyprinter
1717
import Libraries.Data.String.Extra
@@ -48,23 +48,23 @@ conflictMatch ((x, tm) :: ms) = conflictArgs x tm ms || conflictMatch ms
4848
findN i tm
4949
= let (Ref _ (DataCon _ _) _, args) = getFnArgs tm
5050
| _ => False in
51-
anyTrue (map (findN i) args)
51+
any (findN i) args
5252

5353
-- Assuming in normal form. Look for: mismatched constructors, or
5454
-- a name appearing strong rigid in the other term
5555
conflictTm : Term vars -> Term vars -> Bool
5656
conflictTm (Local _ _ i _) tm
5757
= let (Ref _ (DataCon _ _) _, args) = getFnArgs tm
5858
| _ => False in
59-
anyTrue (map (findN i) args)
59+
any (findN i) args
6060
conflictTm tm (Local _ _ i _)
6161
= let (Ref _ (DataCon _ _) _, args) = getFnArgs tm
6262
| _ => False in
63-
anyTrue (map (findN i) args)
63+
any (findN i) args
6464
conflictTm tm tm'
6565
= let (f, args) = getFnArgs tm
6666
(f', args') = getFnArgs tm' in
67-
clash f f' || anyTrue (zipWith conflictTm args args')
67+
clash f f' || any (uncurry conflictTm) (zip args args')
6868

6969
conflictArgs : Name -> Term vars -> List (Name, Term vars) -> Bool
7070
conflictArgs n tm [] = False

‎src/Core/LinearCheck.idr

Lines changed: 1 addition & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -11,7 +11,6 @@ import Core.UnifyState
1111
import Core.Value
1212
import Core.TT
1313

14-
import Libraries.Data.Bool.Extra
1514
import Data.List
1615

1716
%default covering
@@ -108,7 +107,7 @@ mutual
108107
let vars = mapMaybe (findLocal (getArgs lhs)) argpos
109108
hs <- traverse (\vsel => updateHoleUsage useInHole vsel [] rhs)
110109
vars
111-
pure (anyTrue hs)
110+
pure (any id hs)
112111
where
113112
findArg : Nat -> List (Term vars) -> List Nat
114113
findArg i [] = []

‎src/Core/TT.idr

Lines changed: 3 additions & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -3,12 +3,12 @@ module Core.TT
33
import public Core.FC
44
import public Core.Name
55

6-
import Libraries.Data.Bool.Extra
76
import Data.List
87
import Data.Nat
9-
import Libraries.Data.NameMap
108
import Data.Vect
119
import Decidable.Equality
10+
11+
import Libraries.Data.NameMap
1212
import Libraries.Text.PrettyPrint.Prettyprinter
1313
import Libraries.Text.PrettyPrint.Prettyprinter.Util
1414

@@ -873,7 +873,7 @@ eqTerm : Term vs -> Term vs' -> Bool
873873
eqTerm (Local _ _ idx _) (Local _ _ idx' _) = idx == idx'
874874
eqTerm (Ref _ _ n) (Ref _ _ n') = n == n'
875875
eqTerm (Meta _ _ i args) (Meta _ _ i' args')
876-
= assert_total (i == i' && allTrue (zipWith eqTerm args args'))
876+
= assert_total (i == i' && all (uncurry eqTerm) (zip args args'))
877877
eqTerm (Bind _ _ b sc) (Bind _ _ b' sc')
878878
= assert_total (eqBinderBy eqTerm b b') && eqTerm sc sc'
879879
eqTerm (App _ f a) (App _ f' a') = eqTerm f f' && eqTerm a a'

‎src/Core/Unify.idr

Lines changed: 4 additions & 4 deletions
Original file line numberDiff line numberDiff line change
@@ -12,10 +12,10 @@ import Core.TT
1212
import public Core.UnifyState
1313
import Core.Value
1414

15-
import Libraries.Data.Bool.Extra
16-
import Libraries.Data.IntMap
1715
import Data.List
1816
import Data.List.Views
17+
18+
import Libraries.Data.IntMap
1919
import Libraries.Data.NameMap
2020

2121
%default covering
@@ -1507,7 +1507,7 @@ solveConstraints : {auto c : Ref Ctxt Defs} ->
15071507
solveConstraints umode smode
15081508
= do ust <- get UST
15091509
progress <- traverse (retryGuess umode smode) (toList (guesses ust))
1510-
when (anyTrue progress) $
1510+
when (any id progress) $
15111511
solveConstraints umode Normal
15121512

15131513
export
@@ -1518,7 +1518,7 @@ solveConstraintsAfter start umode smode
15181518
= do ust <- get UST
15191519
progress <- traverse (retryGuess umode smode)
15201520
(filter afterStart (toList (guesses ust)))
1521-
when (anyTrue progress) $
1521+
when (any id progress) $
15221522
solveConstraintsAfter start umode Normal
15231523
where
15241524
afterStart : (Int, a) -> Bool

‎src/Idris/Error.idr

Lines changed: 6 additions & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -15,18 +15,21 @@ import Idris.Pretty
1515
import Parser.Source
1616

1717
import Data.List
18-
import Libraries.Data.List1 as Lib
19-
import Libraries.Data.List.Extra
18+
import Data.List1
2019
import Data.Maybe
2120
import Data.Stream
2221
import Data.Strings
22+
23+
import Libraries.Data.List.Extra
24+
import Libraries.Data.List1 as Lib
2325
import Libraries.Data.String.Extra
2426
import Libraries.Text.PrettyPrint.Prettyprinter
2527
import Libraries.Text.PrettyPrint.Prettyprinter.Util
26-
import System.File
2728
import Libraries.Utils.String
2829
import Libraries.Data.String.Extra
2930

31+
import System.File
32+
3033
%hide Data.Strings.lines
3134
%hide Data.Strings.lines'
3235
%hide Data.Strings.unlines

0 commit comments

Comments
 (0)