Merge branch 'main' into suppress_arglist_wrapper

CHANGELOG_NEXT.md

@@ -30,6 +30,9 @@ This CHANGELOG describes the merged but unreleased changes. Please see [CHANGELO
   customise the syntax of operator to look more like a binder.
   See [#3113](https://github.com/idris-lang/Idris2/issues/3113).
 
+* Fixity declarations without an export modifier now emit a warning in peparation
+  for a future version where they will become private by default.
+
 * Elaborator scripts were made to be able to access the visibility modifier of a
   definition, via `getVis`.
 

libs/base/Data/Bits.idr

@@ -5,10 +5,10 @@ import Data.Vect
 
 %default total
 
-infixl 8 `shiftL`, `shiftR`
-infixl 7 .&.
-infixl 6 `xor`
-infixl 5 .|.
+export infixl 8 `shiftL`, `shiftR`
+export infixl 7 .&.
+export infixl 6 `xor`
+export infixl 5 .|.
 
 --------------------------------------------------------------------------------
 --          Interface Bits

libs/base/Data/Contravariant.idr

@@ -2,7 +2,7 @@ module Data.Contravariant
 
 %default total
 
-infixl 4 >$, >$<, >&<, $<
+export infixl 4 >$, >$<, >&<, $<
 
 ||| Contravariant functors
 public export

libs/base/Data/Fin.idr

@@ -304,7 +304,7 @@ namespace Equality
     FZ : Pointwise FZ FZ
     FS : Pointwise k l -> Pointwise (FS k) (FS l)
 
-  infix 6 ~~~
+  export infix 6 ~~~
   ||| Convenient infix notation for the notion of pointwise equality of Fins
   public export
   (~~~) : Fin m -> Fin n -> Type

libs/base/Data/List.idr

@@ -270,7 +270,7 @@ public export
 deleteFirstsBy : (p : a -> b -> Bool) -> (source : List b) -> (undesirables : List a) -> List b
 deleteFirstsBy p = foldl (flip (deleteBy p))
 
-infix 7 \\
+export infix 7 \\
 
 ||| The non-associative list-difference.
 ||| A specialized form of @deleteFirstsBy@ where the predicate is equality under the @Eq@

libs/base/Data/List1.idr

@@ -5,7 +5,7 @@ import public Control.Function
 
 %default total
 
-infixr 7 :::
+export infixr 7 :::
 
 ||| Non-empty lists.
 public export

libs/base/Data/Morphisms.idr

@@ -9,7 +9,7 @@ record Morphism a b where
   constructor Mor
   applyMor : a -> b
 
-infixr 1 ~>
+export infixr 1 ~>
 
 public export
 (~>) : Type -> Type -> Type

libs/base/Data/Zippable.idr

@@ -21,7 +21,7 @@ interface Zippable z where
   zip : z a -> z b -> z (a, b)
   zip = zipWith (,)
 
-  infixr 6 `zip`
+  export infixr 6 `zip`
 
   ||| Combine three parameterised types by applying a function.
   ||| @ z the parameterised type

libs/base/Syntax/PreorderReasoning.idr

@@ -2,9 +2,7 @@
 ||| poor-man's equational reasoning
 module Syntax.PreorderReasoning
 
-infixl 0  ~~,~=
-prefix 1  |~
-infix  1  ...,..<,..>,.=.,.=<,.=>
+import public Syntax.PreorderReasoning.Ops
 
 |||Slightly nicer syntax for justifying equations:
 |||```

libs/base/Syntax/PreorderReasoning/Generic.idr

@@ -2,10 +2,7 @@ module Syntax.PreorderReasoning.Generic
 
 import Control.Relation
 import Control.Order
-infixl 0  ~~, ~=
-infixl 0  <~
-prefix 1  |~
-infix  1  ...,..<,..>,.=.,.=<,.=>
+import public Syntax.PreorderReasoning.Ops
 
 public export
 data Step : (leq : a -> a -> Type) -> a -> a -> Type where

libs/base/Syntax/PreorderReasoning/Ops.idr

@@ -0,0 +1,6 @@
+module Syntax.PreorderReasoning.Ops
+
+export infixl 0  ~~, ~=
+export infixl 0  <~
+export prefix 1  |~
+export infix  1  ...,..<,..>,.=.,.=<,.=>

libs/base/base.ipkg

@@ -108,6 +108,7 @@ modules = Control.App,
           Language.Reflection.TTImp,
 
           Syntax.PreorderReasoning,
+          Syntax.PreorderReasoning.Ops,
           Syntax.PreorderReasoning.Generic,
 
           System,

libs/contrib/Control/Algebra.idr

@@ -1,7 +1,7 @@
 module Control.Algebra
 
-infixl 6 <->
-infixl 7 <.>
+export infixl 6 <->
+export infixl 7 <.>
 
 public export
 interface Semigroup ty => SemigroupV ty where

libs/contrib/Control/Arrow.idr

@@ -5,11 +5,11 @@ import Data.Either
 import Data.Morphisms
 
 
-infixr 5 <++>
-infixr 3 ***
-infixr 3 &&&
-infixr 2 +++
-infixr 2 \|/
+export infixr 5 <++>
+export infixr 3 ***
+export infixr 3 &&&
+export infixr 2 +++
+export infixr 2 \|/
 
 public export
 interface Category arr => Arrow (0 arr : Type -> Type -> Type) where

libs/contrib/Control/Category.idr

@@ -20,7 +20,7 @@ Monad m => Category (Kleislimorphism m) where
   id                        = Kleisli (pure . id)
   (Kleisli f) . (Kleisli g) = Kleisli $ \a => g a >>= f
 
-infixr 1 >>>
+export infixr 1 >>>
 
 public export
 (>>>) : Category cat => cat a b -> cat b c -> cat a c

libs/contrib/Control/Validation.idr

@@ -96,7 +96,7 @@ export
 fail : Applicative m => String -> ValidatorT m a b
 fail s = MkValidator $ \_ => left s
 
-infixl 2 >>>
+export infixl 2 >>>
 
 ||| Compose two validators so that the second validates the output of the first.
 export

libs/contrib/Data/List/Alternating.idr

@@ -3,8 +3,8 @@ module Data.List.Alternating
 import Data.Bifoldable
 import Data.List
 
-infixl 5 +>
-infixr 5 <+
+export infixl 5 +>
+export infixr 5 <+
 
 %default total
 

libs/contrib/Data/Monoid/Exponentiation.idr

@@ -23,7 +23,7 @@ public export
 modular : Monoid a => a -> Nat -> a
 modular v n = modularRec v (halfRec n)
 
-infixr 10 ^
+export infixr 10 ^
 public export
 (^) : Num a => a -> Nat -> a
 (^) = modular @{Multiplicative}

libs/contrib/Data/Seq/Internal.idr

@@ -342,7 +342,7 @@ viewRTree (Deep s pr m (Four w x y z)) =
 
 
 -- Construction
-infixr 5 `consTree`
+export infixr 5 `consTree`
 export
 consTree : Sized e => (r : e) -> FingerTree e -> FingerTree e
 a `consTree` Empty                       = Single a
@@ -352,7 +352,7 @@ a `consTree` Deep s (Two b c) st d2      = Deep (size a + s) (Three a b c) st d2
 a `consTree` Deep s (Three b c d) st d2  = Deep (size a + s) (Four a b c d) st d2
 a `consTree` Deep s (Four b c d f) st d2 = Deep (size a + s) (Two a b) (node3 c d f `consTree` st) d2
 
-infixl 5 `snocTree`
+export infixl 5 `snocTree`
 export
 snocTree : Sized e => FingerTree e -> (r : e) -> FingerTree e
 Empty `snocTree` a                       = Single a

libs/contrib/Data/Seq/Sized.idr

@@ -48,13 +48,13 @@ export
 reverse : Seq n a -> Seq n a
 reverse (MkSeq tr) = MkSeq (reverseTree id tr)
 
-infixr 5 `cons`
+export infixr 5 `cons`
 ||| O(1). Add an element to the left end of a sequence.
 export
 cons : e -> Seq n e -> Seq (S n) e
 a `cons` MkSeq tr = MkSeq (MkElem a `consTree` tr)
 
-infixl 5 `snoc`
+export infixl 5 `snoc`
 ||| O(1). Add an element to the right end of a sequence.
 export
 snoc : Seq n e -> e -> Seq (S n) e

libs/contrib/Data/Seq/Unsized.idr

@@ -40,13 +40,13 @@ export
 reverse : Seq a -> Seq a
 reverse (MkSeq tr) = MkSeq (reverseTree id tr)
 
-infixr 5 `cons`
+export infixr 5 `cons`
 ||| O(1). Add an element to the left end of a sequence.
 export
 cons : e -> Seq e -> Seq e
 a `cons` MkSeq tr = MkSeq (MkElem a `consTree` tr)
 
-infixl 5 `snoc`
+export infixl 5 `snoc`
 ||| O(1). Add an element to the right end of a sequence.
 export
 snoc : Seq e -> e -> Seq e

libs/contrib/Data/String/Extra.idr

@@ -5,8 +5,8 @@ import Data.String
 
 %default total
 
-infixl 5 +>
-infixr 5 <+
+export infixl 5 +>
+export infixr 5 <+
 
 ||| Adds a character to the end of the specified string.
 |||

libs/contrib/Data/String/Parser.idr

@@ -106,7 +106,7 @@ export
                                 Fail i _ => Fail i msg)
                             (p.runParser s)
 
-infixl 0 <?>
+export infixl 0 <?>
 
 ||| Discards the result of a parser
 export

libs/contrib/Data/Telescope/Segment.idr

@@ -59,7 +59,7 @@ toTelescope seg = untabulate seg ()
 
 %name Segment delta,delta',delta1,delta2
 
-infixl 3 |++, :++
+export infixl 3 |++, :++
 
 ||| This lemma comes up all the time when mixing induction on Nat with
 ||| indexing modulo addition.  An alternative is to use something like
@@ -141,7 +141,7 @@ projection {n = S n} {delta = ty :: delta} env
                     $ rewrite succLemma n k in env
     in env'
 
-infixl 4 .=
+export infixl 4 .=
 
 public export
 data Environment : (env : Left.Environment gamma)

libs/contrib/Data/Telescope/Telescope.idr

@@ -30,8 +30,8 @@ plusAccZeroRightNeutral m =
   Refl
 
 
-infixl 4 -.
-infixr 4 .-
+export infixl 4 -.
+export infixr 4 .-
 
 namespace Left
 
@@ -158,7 +158,7 @@ namespace Right
 
 namespace Tree
 
-  infixl 4 ><
+  export infixl 4 ><
 
   mutual
     ||| A tree of dependent types
@@ -189,14 +189,14 @@ namespace Tree
          (transpL env1 ** snd (concat (delta (transpL env1))) env2)
     )
 
-infix 5 <++>
+export infix 5 <++>
 
 public export
 (<++>) : (gamma : Left.Telescope m) -> (Environment gamma -> Right.Telescope n) -> Right.Telescope (plusAcc m n)
 [] <++> delta = delta ()
 (gamma -. sigma ) <++> delta = gamma <++> (\ env => sigma env .- \ v => delta (env ** v))
 
-infix 5 >++<
+export infix 5 >++<
 
 (>++<) : {m, n : Nat} -> (gamma : Right.Telescope m) -> (Environment gamma -> Left.Telescope n) ->
          Left.Telescope (plusAcc m n)

libs/contrib/Syntax/WithProof.idr

@@ -1,6 +1,6 @@
 module Syntax.WithProof
 
-prefix 10 @@
+export prefix 10 @@
 
 ||| Until Idris2 supports the 'with (...) proof p' construct, here's a
 ||| poor-man's replacement.

libs/contrib/System/Path.idr

@@ -13,8 +13,8 @@ import Text.Quantity
 
 import System.Info
 
-infixl 5 </>, />
-infixr 7 <.>
+export infixl 5 </>, />
+export infixr 7 <.>
 
 
 ||| The character that separates directories in the path.

libs/contrib/Text/Parser/Core.idr

@@ -128,7 +128,7 @@ export %inline
         Grammar state tok (c1 && c2) ty
 (<|>) = Alt
 
-infixr 2 <||>
+export infixr 2 <||>
 ||| Take the tagged disjunction of two grammars. If both consume, the
 ||| combination is guaranteed to consume.
 export

libs/contrib/Text/PrettyPrint/Prettyprinter/Doc.idr

@@ -122,7 +122,7 @@ export
 fill : Int -> Doc ann -> Doc ann
 fill n doc = width doc (\w => spaces $ n - w)
 
-infixr 6 <++>
+export infixr 6 <++>
 ||| Concatenates two documents with a space in between.
 export
 (<++>) : Doc ann -> Doc ann -> Doc ann

libs/linear/Data/Linear/Copies.idr

@@ -6,7 +6,7 @@ import Data.Nat
 
 %default total
 
-infix 1 `Copies`
+export infix 1 `Copies`
 
 ||| Carries multiple linear copies of the same value. Usage: m `Copies` x
 ||| reads as "m copies of value x". This data structure is necessary to implement

libs/linear/Data/Linear/Interface.idr

@@ -35,7 +35,7 @@ Consumable Int where
 
 -- But crucially we don't have `Consumable World` or `Consumable Handle`.
 
-infixr 5 `seq`
+export infixr 5 `seq`
 ||| We can sequentially compose a computation returning a value that is
 ||| consumable with another computation. This is done by first consuming
 ||| the result of the first computation and then returning the second one.

libs/linear/Data/Linear/Notation.idr

@@ -2,7 +2,7 @@ module Data.Linear.Notation
 
 %default total
 
-infixr 0 -@
+export infixr 0 -@
 ||| Infix notation for linear implication
 public export
 (-@) : Type -> Type -> Type
@@ -18,7 +18,7 @@ public export
 (.) : (b -@ c) -@ (a -@ b) -@ (a -@ c)
 (.) f g v = f (g v)
 
-prefix 5 !*
+export prefix 5 !*
 ||| Prefix notation for the linear unrestricted modality
 public export
 record (!*) (a : Type) where

libs/papers/Data/Description/Regular.idr

@@ -88,7 +88,7 @@ Memo (Const s prop) x b = (v : s) -> b v
 Memo (d1 * d2) x b = Memo d1 x $ \ v1 => Memo d2 x $ \ v2 => b (v1, v2)
 Memo (d1 + d2) x b = (Memo d1 x (b . Left), Memo d2 x (b . Right))
 
-infixr 0 ~>
+export infixr 0 ~>
 
 ||| A memo trie is a coinductive structure
 export