From 75032a7164ce1a55026264761673ea76c2f51173 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Andr=C3=A9=20Videla?= Date: Wed, 3 Apr 2024 15:41:57 +0100 Subject: [PATCH] Emit warning for fixities with no export modifiers (#3234) * Emit warning for fixities with no export modifiers This is to help update all the existing code to program with explicit fixity export directives in preparation for the behavioral change where they will become private by default. --- CHANGELOG_NEXT.md | 3 + libs/base/Data/Bits.idr | 8 +- libs/base/Data/Contravariant.idr | 2 +- libs/base/Data/Fin.idr | 2 +- libs/base/Data/List.idr | 2 +- libs/base/Data/List1.idr | 2 +- libs/base/Data/Morphisms.idr | 2 +- libs/base/Data/Zippable.idr | 2 +- libs/base/Syntax/PreorderReasoning.idr | 4 +- .../base/Syntax/PreorderReasoning/Generic.idr | 5 +- libs/base/Syntax/PreorderReasoning/Ops.idr | 6 ++ libs/base/base.ipkg | 1 + libs/contrib/Control/Algebra.idr | 4 +- libs/contrib/Control/Arrow.idr | 10 +-- libs/contrib/Control/Category.idr | 2 +- libs/contrib/Control/Validation.idr | 2 +- libs/contrib/Data/List/Alternating.idr | 4 +- libs/contrib/Data/Monoid/Exponentiation.idr | 2 +- libs/contrib/Data/Seq/Internal.idr | 4 +- libs/contrib/Data/Seq/Sized.idr | 4 +- libs/contrib/Data/Seq/Unsized.idr | 4 +- libs/contrib/Data/String/Extra.idr | 4 +- libs/contrib/Data/String/Parser.idr | 2 +- libs/contrib/Data/Telescope/Segment.idr | 4 +- libs/contrib/Data/Telescope/Telescope.idr | 10 +-- libs/contrib/Syntax/WithProof.idr | 2 +- libs/contrib/System/Path.idr | 4 +- libs/contrib/Text/Parser/Core.idr | 2 +- .../Text/PrettyPrint/Prettyprinter/Doc.idr | 2 +- libs/linear/Data/Linear/Copies.idr | 2 +- libs/linear/Data/Linear/Interface.idr | 2 +- libs/linear/Data/Linear/Notation.idr | 4 +- libs/papers/Data/Description/Regular.idr | 2 +- libs/papers/Data/W.idr | 6 +- .../Language/IntrinsicScoping/TypeTheory.idr | 4 +- libs/papers/Language/Tagless.idr | 2 +- libs/papers/Language/TypeTheory.idr | 11 +-- libs/papers/Search/HDecidable.idr | 2 +- libs/papers/Search/Tychonoff/PartI.idr | 2 +- libs/prelude/Builtin.idr | 4 +- libs/prelude/Prelude/Basics.idr | 2 +- libs/prelude/Prelude/Ops.idr | 32 +++---- libs/prelude/Prelude/Types.idr | 4 +- src/Algebra/Semiring.idr | 4 +- src/Core/Binary.idr | 2 +- src/Core/Context.idr | 14 ++- src/Core/Core.idr | 7 +- src/Core/Hash.idr | 2 +- src/Core/TT.idr | 4 +- src/Idris/Desugar.idr | 86 ++++++++++++------- src/Idris/Doc/Keywords.idr | 3 +- src/Idris/Error.idr | 62 ++++++------- src/Idris/Parser.idr | 15 ++-- src/Idris/Pretty.idr | 14 +-- src/Idris/Resugar.idr | 16 ++-- src/Idris/Syntax.idr | 44 ++++++++-- src/Idris/Syntax/Views.idr | 2 +- src/Libraries/Data/Ordering/Extra.idr | 2 +- src/Libraries/Data/PosMap.idr | 4 +- src/Libraries/Data/String/Extra.idr | 4 +- src/Libraries/Text/Parser/Core.idr | 2 +- .../Text/PrettyPrint/Prettyprinter/Doc.idr | 2 +- src/Libraries/Utils/Path.idr | 6 +- tests/base/sortedmap_001/SortedMapTest.idr | 2 +- tests/ideMode/ideMode005/LetBinders.idr | 2 +- tests/ideMode/ideMode005/expectedG | 5 +- tests/idris2/basic/basic002/Do.idr | 2 +- tests/idris2/basic/basic003/Ambig2.idr | 2 +- tests/idris2/basic/basic004/Stuff.idr | 2 +- tests/idris2/basic/basic006/Stuff.idr | 2 +- tests/idris2/basic/basic007/Stuff.idr | 2 +- tests/idris2/basic/basic009/Stuff.idr | 4 +- tests/idris2/basic/basic028/Do.idr | 2 +- tests/idris2/basic/basic058/DataTypeOp.idr | 8 +- tests/idris2/interface/interface001/IFace.idr | 2 +- .../idris2/interface/interface001/IFace1.idr | 2 +- tests/idris2/interface/interface001/Stuff.idr | 6 +- tests/idris2/interface/interface002/Stuff.idr | 2 +- tests/idris2/interface/interface006/Apply.idr | 2 +- .../interface/interface006/Biapplicative.idr | 2 +- .../idris2/interface/interface006/Bimonad.idr | 2 +- tests/idris2/interface/interface024/EH.idr | 4 +- tests/idris2/linear/linear001/Stuff.idr | 2 +- tests/idris2/linear/linear002/Stuff.idr | 2 +- tests/idris2/linear/linear012/linholes.idr | 2 +- tests/idris2/misc/docs004/List.idr | 4 +- tests/idris2/misc/import009/Test.idr | 1 + tests/idris2/misc/lazy001/Lazy.idr | 2 +- tests/idris2/misc/namespace005/Lib1.idr | 2 +- tests/idris2/misc/namespace005/Lib2.idr | 2 +- tests/idris2/misc/namespace005/LibPre1.idr | 2 +- tests/idris2/misc/namespace005/LibPre2.idr | 2 +- tests/idris2/misc/namespace005/Main3.idr | 4 +- .../idris2/misc/namespace005/NonConflict1.idr | 2 +- .../idris2/misc/namespace005/NonConflict2.idr | 2 +- tests/idris2/misc/pretty001/Issue1328A.idr | 4 +- tests/idris2/operators/operators001/Test.idr | 12 +-- .../idris2/operators/operators002/Error2.idr | 2 +- .../idris2/operators/operators002/Errors.idr | 2 +- .../idris2/operators/operators002/Errors2.idr | 2 +- .../idris2/operators/operators002/Errors3.idr | 2 +- .../idris2/operators/operators002/Errors4.idr | 2 +- .../idris2/operators/operators002/Errors5.idr | 2 +- tests/idris2/operators/operators002/Lin.idr | 4 + .../operators/operators002/LinImport.idr | 9 ++ tests/idris2/operators/operators002/Test.idr | 8 +- tests/idris2/operators/operators002/expected | 37 +++++--- tests/idris2/operators/operators002/run | 1 + tests/idris2/operators/operators004/Test.idr | 4 +- tests/idris2/operators/operators004/expected | 4 +- tests/idris2/operators/operators005/Test.idr | 4 +- tests/idris2/operators/operators006/Test.idr | 2 +- tests/idris2/operators/operators007/Test.idr | 2 +- tests/idris2/operators/operators007/Test2.idr | 4 +- tests/idris2/operators/operators007/expected | 8 +- tests/idris2/operators/operators008/Test.idr | 2 +- tests/idris2/operators/operators009/Test.idr | 4 + tests/idris2/operators/operators009/expected | 11 +++ tests/idris2/operators/operators009/run | 3 + tests/idris2/reflection/reflection016/Eta.idr | 2 +- tests/idris2/reg/reg023/boom.idr | 2 +- tests/idris2/reg/reg034/void.idr | 6 +- tests/idris2/warning/warning004/Lib1.idr | 2 +- tests/idris2/warning/warning004/Lib2.idr | 2 +- tests/typedd-book/chapter06/DataStore.idr | 2 +- .../typedd-book/chapter06/DataStoreHoles.idr | 2 +- tests/typedd-book/chapter10/DataStore.idr | 2 +- tests/typedd-book/chapter12/DataStore.idr | 2 +- 128 files changed, 417 insertions(+), 303 deletions(-) create mode 100644 libs/base/Syntax/PreorderReasoning/Ops.idr create mode 100644 tests/idris2/operators/operators002/Lin.idr create mode 100644 tests/idris2/operators/operators002/LinImport.idr create mode 100644 tests/idris2/operators/operators009/Test.idr create mode 100644 tests/idris2/operators/operators009/expected create mode 100755 tests/idris2/operators/operators009/run diff --git a/CHANGELOG_NEXT.md b/CHANGELOG_NEXT.md index 1c237367f..ee8ca0727 100644 --- a/CHANGELOG_NEXT.md +++ b/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`. diff --git a/libs/base/Data/Bits.idr b/libs/base/Data/Bits.idr index 68bc156cb..0d3ce45e1 100644 --- a/libs/base/Data/Bits.idr +++ b/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 diff --git a/libs/base/Data/Contravariant.idr b/libs/base/Data/Contravariant.idr index b0d441b6e..098d66a42 100644 --- a/libs/base/Data/Contravariant.idr +++ b/libs/base/Data/Contravariant.idr @@ -2,7 +2,7 @@ module Data.Contravariant %default total -infixl 4 >$, >$<, >&<, $< +export infixl 4 >$, >$<, >&<, $< ||| Contravariant functors public export diff --git a/libs/base/Data/Fin.idr b/libs/base/Data/Fin.idr index 009fa32ca..997b5c65b 100644 --- a/libs/base/Data/Fin.idr +++ b/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 diff --git a/libs/base/Data/List.idr b/libs/base/Data/List.idr index edc1d16da..e879de24e 100644 --- a/libs/base/Data/List.idr +++ b/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@ diff --git a/libs/base/Data/List1.idr b/libs/base/Data/List1.idr index 1b02fb5cb..072ad9268 100644 --- a/libs/base/Data/List1.idr +++ b/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 diff --git a/libs/base/Data/Morphisms.idr b/libs/base/Data/Morphisms.idr index d25c2c010..9b0cb356b 100644 --- a/libs/base/Data/Morphisms.idr +++ b/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 diff --git a/libs/base/Data/Zippable.idr b/libs/base/Data/Zippable.idr index c4ee8f47e..75c72114a 100644 --- a/libs/base/Data/Zippable.idr +++ b/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 diff --git a/libs/base/Syntax/PreorderReasoning.idr b/libs/base/Syntax/PreorderReasoning.idr index e5ab95998..82e429fda 100644 --- a/libs/base/Syntax/PreorderReasoning.idr +++ b/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: |||``` diff --git a/libs/base/Syntax/PreorderReasoning/Generic.idr b/libs/base/Syntax/PreorderReasoning/Generic.idr index b52f71ba4..2f7732269 100644 --- a/libs/base/Syntax/PreorderReasoning/Generic.idr +++ b/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 diff --git a/libs/base/Syntax/PreorderReasoning/Ops.idr b/libs/base/Syntax/PreorderReasoning/Ops.idr new file mode 100644 index 000000000..ae3cc8ea9 --- /dev/null +++ b/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 ...,..<,..>,.=.,.=<,.=> diff --git a/libs/base/base.ipkg b/libs/base/base.ipkg index 0250fe775..0b4a920a4 100644 --- a/libs/base/base.ipkg +++ b/libs/base/base.ipkg @@ -108,6 +108,7 @@ modules = Control.App, Language.Reflection.TTImp, Syntax.PreorderReasoning, + Syntax.PreorderReasoning.Ops, Syntax.PreorderReasoning.Generic, System, diff --git a/libs/contrib/Control/Algebra.idr b/libs/contrib/Control/Algebra.idr index f8d877ffa..6fa1fc9eb 100644 --- a/libs/contrib/Control/Algebra.idr +++ b/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 diff --git a/libs/contrib/Control/Arrow.idr b/libs/contrib/Control/Arrow.idr index 13922d3b6..26fe8f12c 100644 --- a/libs/contrib/Control/Arrow.idr +++ b/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 diff --git a/libs/contrib/Control/Category.idr b/libs/contrib/Control/Category.idr index 1c0e72bb8..bf59a96d0 100644 --- a/libs/contrib/Control/Category.idr +++ b/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 diff --git a/libs/contrib/Control/Validation.idr b/libs/contrib/Control/Validation.idr index 00317c787..3357f9aff 100644 --- a/libs/contrib/Control/Validation.idr +++ b/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 diff --git a/libs/contrib/Data/List/Alternating.idr b/libs/contrib/Data/List/Alternating.idr index b80d19aaa..eb62d1ed2 100644 --- a/libs/contrib/Data/List/Alternating.idr +++ b/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 diff --git a/libs/contrib/Data/Monoid/Exponentiation.idr b/libs/contrib/Data/Monoid/Exponentiation.idr index d2e44bbb3..f7ddbe386 100644 --- a/libs/contrib/Data/Monoid/Exponentiation.idr +++ b/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} diff --git a/libs/contrib/Data/Seq/Internal.idr b/libs/contrib/Data/Seq/Internal.idr index b9cf10664..a54f39c4a 100644 --- a/libs/contrib/Data/Seq/Internal.idr +++ b/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 diff --git a/libs/contrib/Data/Seq/Sized.idr b/libs/contrib/Data/Seq/Sized.idr index 43578cbd7..79ca527cc 100644 --- a/libs/contrib/Data/Seq/Sized.idr +++ b/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 diff --git a/libs/contrib/Data/Seq/Unsized.idr b/libs/contrib/Data/Seq/Unsized.idr index cb0eb28f5..ce011cc97 100644 --- a/libs/contrib/Data/Seq/Unsized.idr +++ b/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 diff --git a/libs/contrib/Data/String/Extra.idr b/libs/contrib/Data/String/Extra.idr index 40f45b84a..418bd4746 100644 --- a/libs/contrib/Data/String/Extra.idr +++ b/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. ||| diff --git a/libs/contrib/Data/String/Parser.idr b/libs/contrib/Data/String/Parser.idr index 4de6f12f4..bf5b46121 100644 --- a/libs/contrib/Data/String/Parser.idr +++ b/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 diff --git a/libs/contrib/Data/Telescope/Segment.idr b/libs/contrib/Data/Telescope/Segment.idr index 88c077320..1d97e6a95 100644 --- a/libs/contrib/Data/Telescope/Segment.idr +++ b/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) diff --git a/libs/contrib/Data/Telescope/Telescope.idr b/libs/contrib/Data/Telescope/Telescope.idr index d46f308e7..d4dbdc419 100644 --- a/libs/contrib/Data/Telescope/Telescope.idr +++ b/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) diff --git a/libs/contrib/Syntax/WithProof.idr b/libs/contrib/Syntax/WithProof.idr index 0c57d4ad8..1231ff535 100644 --- a/libs/contrib/Syntax/WithProof.idr +++ b/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. diff --git a/libs/contrib/System/Path.idr b/libs/contrib/System/Path.idr index 1b43bd56e..603f6f9bb 100644 --- a/libs/contrib/System/Path.idr +++ b/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. diff --git a/libs/contrib/Text/Parser/Core.idr b/libs/contrib/Text/Parser/Core.idr index 93db72bb9..2dc7c9812 100644 --- a/libs/contrib/Text/Parser/Core.idr +++ b/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 diff --git a/libs/contrib/Text/PrettyPrint/Prettyprinter/Doc.idr b/libs/contrib/Text/PrettyPrint/Prettyprinter/Doc.idr index 97fb9f7d3..c2ec32d49 100644 --- a/libs/contrib/Text/PrettyPrint/Prettyprinter/Doc.idr +++ b/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 diff --git a/libs/linear/Data/Linear/Copies.idr b/libs/linear/Data/Linear/Copies.idr index 1fca2dd1f..99a7353b2 100644 --- a/libs/linear/Data/Linear/Copies.idr +++ b/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 diff --git a/libs/linear/Data/Linear/Interface.idr b/libs/linear/Data/Linear/Interface.idr index ec7d857ae..6a8f5fcfe 100644 --- a/libs/linear/Data/Linear/Interface.idr +++ b/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. diff --git a/libs/linear/Data/Linear/Notation.idr b/libs/linear/Data/Linear/Notation.idr index 11989ec35..be379a7c6 100644 --- a/libs/linear/Data/Linear/Notation.idr +++ b/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 diff --git a/libs/papers/Data/Description/Regular.idr b/libs/papers/Data/Description/Regular.idr index c4a0251f6..0b904c35b 100644 --- a/libs/papers/Data/Description/Regular.idr +++ b/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 diff --git a/libs/papers/Data/W.idr b/libs/papers/Data/W.idr index b8dcd4f7a..e92e46ab5 100644 --- a/libs/papers/Data/W.idr +++ b/libs/papers/Data/W.idr @@ -66,12 +66,12 @@ namespace Finitary Arr (AUnit nm) r = One nm r Arr (d || e) r = (Arr d r, Arr e r) - infixr 0 ~> + export infixr 0 ~> record (~>) (d : Fin) (r : Type) where constructor MkArr runArr : Arr d r - infix 5 .= + export infix 5 .= (.=) : (nm : String) -> s -> One nm s nm .= v = MkOne v @@ -98,7 +98,7 @@ namespace Finitary appArr (d || e) f (Left x) = appArr d (fst f) x appArr (d || e) f (Right x) = appArr e (snd f) x - infixl 0 $$ + export infixl 0 $$ ($$) : {d : Fin} -> (d ~> r) -> (Elem d -> r) MkArr f $$ x = appArr d f x diff --git a/libs/papers/Language/IntrinsicScoping/TypeTheory.idr b/libs/papers/Language/IntrinsicScoping/TypeTheory.idr index c64aa33f5..9539e6c74 100644 --- a/libs/papers/Language/IntrinsicScoping/TypeTheory.idr +++ b/libs/papers/Language/IntrinsicScoping/TypeTheory.idr @@ -76,7 +76,7 @@ data Infer : Scoped where ||| The application of a function to its argument App : Infer f g -> Check f g -> Infer f g -infixl 3 `App` +export infixl 3 `App` %name Infer e @@ -229,7 +229,7 @@ namespace Value vfree : Level nm f -> Value f vfree x = VEmb (NVar x) -infixl 5 `vapp` +export infixl 5 `vapp` ||| We can easily apply a value standing for a function ||| to a value standing for its argument by either deploying diff --git a/libs/papers/Language/Tagless.idr b/libs/papers/Language/Tagless.idr index 1e90bd629..1378cbf34 100644 --- a/libs/papers/Language/Tagless.idr +++ b/libs/papers/Language/Tagless.idr @@ -9,7 +9,7 @@ import Data.List.Quantifiers %default total -infixr 0 -# +export infixr 0 -# public export (-#) : Type -> Type -> Type a -# b = (0 _ : a) -> b diff --git a/libs/papers/Language/TypeTheory.idr b/libs/papers/Language/TypeTheory.idr index 2065a9066..6845ca4d3 100644 --- a/libs/papers/Language/TypeTheory.idr +++ b/libs/papers/Language/TypeTheory.idr @@ -15,6 +15,8 @@ import Data.List %default covering +private infixl 3 `App` + ||| We use this wrapper to mark places where binding occurs. ||| This is a major footgun and we hope the type constructor ||| forces users to think carefully about what they are doing @@ -55,7 +57,7 @@ namespace Section2 Quote m == Quote n = m == n _ == _ = False - infixr 0 ~> + private infixr 0 ~> total data Ty : Type where ||| A family of base types @@ -91,8 +93,6 @@ namespace Section2 ||| The application of a function to its argument App : Infer -> Check -> Infer - infixl 3 `App` - %name Infer e, f total @@ -359,7 +359,6 @@ namespace Section3 ||| The application of a function to its argument App : Infer -> Check -> Infer - infixl 3 `App` %name Infer e, f @@ -600,8 +599,6 @@ namespace Section4 ||| The application of a function to its argument App : Infer -> Check -> Infer - infixl 3 `App` - %name Infer e, f total @@ -695,7 +692,7 @@ namespace Section4 vfree : Name -> Value vfree x = VEmb (NVar x) - infixl 5 `vapp` + private infixl 5 `vapp` ||| We can easily apply a value standing for a function ||| to a value standing for its argument by either deploying diff --git a/libs/papers/Search/HDecidable.idr b/libs/papers/Search/HDecidable.idr index 32c2298cb..608916527 100644 --- a/libs/papers/Search/HDecidable.idr +++ b/libs/papers/Search/HDecidable.idr @@ -114,7 +114,7 @@ not : (AnHDec l, Negates na a) => l na -> HDec (Not a) not p = [| toNegation (toHDec p) |] -infixr 3 ==> +export infixr 3 ==> ||| Half deciders are closed under implication public export diff --git a/libs/papers/Search/Tychonoff/PartI.idr b/libs/papers/Search/Tychonoff/PartI.idr index 1926bcbb5..50c7f5023 100644 --- a/libs/papers/Search/Tychonoff/PartI.idr +++ b/libs/papers/Search/Tychonoff/PartI.idr @@ -40,7 +40,7 @@ HilbertEpsilon p = (v : x ** (v0 : x) -> p v0 -> p v) 0 IsSearchable : Type -> Type IsSearchable x = (0 p : Pred x) -> Decidable p -> HilbertEpsilon p -infix 0 <-> +private infix 0 <-> record (<->) (a, b : Type) where constructor MkIso forwards : a -> b diff --git a/libs/prelude/Builtin.idr b/libs/prelude/Builtin.idr index 1a839238d..85e778142 100644 --- a/libs/prelude/Builtin.idr +++ b/libs/prelude/Builtin.idr @@ -74,7 +74,7 @@ swap (x, y) = (y, x) -- This directive tells auto implicit search what to use to look inside pairs %pair Pair fst snd -infixr 5 # +export infixr 5 # ||| A pair type where each component is linear public export @@ -126,7 +126,7 @@ data Equal : forall a, b . a -> b -> Type where %name Equal prf -infix 6 ===, ~=~ +export infix 6 ===, ~=~ -- An equality type for when you want to assert that each side of the -- equality has the same type, but there's not other evidence available diff --git a/libs/prelude/Prelude/Basics.idr b/libs/prelude/Prelude/Basics.idr index d275c2c0b..e5b9884d5 100644 --- a/libs/prelude/Prelude/Basics.idr +++ b/libs/prelude/Prelude/Basics.idr @@ -69,7 +69,7 @@ public export %tcinline on : (b -> b -> c) -> (a -> b) -> a -> a -> c on f g = \x, y => g x `f` g y -infixl 0 `on` +export infixl 0 `on` ||| Takes in the first two arguments in reverse order. ||| @ f the function to flip diff --git a/libs/prelude/Prelude/Ops.idr b/libs/prelude/Prelude/Ops.idr index 062b42670..dc987a1b8 100644 --- a/libs/prelude/Prelude/Ops.idr +++ b/libs/prelude/Prelude/Ops.idr @@ -1,30 +1,30 @@ module Prelude.Ops -- Numerical operators -infix 6 ==, /=, <, <=, >, >= -infixl 8 +, - -infixl 9 *, / +export infix 6 ==, /=, <, <=, >, >= +export infixl 8 +, - +export infixl 9 *, / -- Boolean operators -infixr 5 && -infixr 4 || +export infixr 5 && +export infixr 4 || -- List and String operators -infixr 7 ::, ++ -infixl 7 :< +export infixr 7 ::, ++ +export infixl 7 :< -- Equivalence -infix 0 <=> +export infix 0 <=> -- Functor/Applicative/Monad/Algebra operators -infixl 1 >>=, =<<, >>, >=>, <=<, <&> -infixr 2 <|> -infixl 3 <*>, *>, <* -infixr 4 <$>, $>, <$ -infixl 8 <+> +export infixl 1 >>=, =<<, >>, >=>, <=<, <&> +export infixr 2 <|> +export infixl 3 <*>, *>, <* +export infixr 4 <$>, $>, <$ +export infixl 8 <+> -- Utility operators -infixr 9 ., .: -infixr 0 $ +export infixr 9 ., .: +export infixr 0 $ -infixl 9 `div`, `mod` +export infixl 9 `div`, `mod` diff --git a/libs/prelude/Prelude/Types.idr b/libs/prelude/Prelude/Types.idr index 7482c10e9..95bc08c2c 100644 --- a/libs/prelude/Prelude/Types.idr +++ b/libs/prelude/Prelude/Types.idr @@ -406,8 +406,8 @@ Ord a => Ord (List a) where namespace SnocList - infixl 7 <>< - infixr 6 <>> + export infixl 7 <>< + export infixr 6 <>> ||| 'fish': Action of lists on snoc-lists public export diff --git a/src/Algebra/Semiring.idr b/src/Algebra/Semiring.idr index cbe0b9f0c..f1fcdca94 100644 --- a/src/Algebra/Semiring.idr +++ b/src/Algebra/Semiring.idr @@ -2,8 +2,8 @@ module Algebra.Semiring %default total -infixl 8 |+| -infixl 9 |*| +export infixl 8 |+| +export infixl 9 |*| ||| A Semiring has two binary operations and an identity for each public export diff --git a/src/Core/Binary.idr b/src/Core/Binary.idr index 813dd9a96..c967f1f04 100644 --- a/src/Core/Binary.idr +++ b/src/Core/Binary.idr @@ -29,7 +29,7 @@ import public Libraries.Utils.Binary ||| version number if you're changing the version more than once in the same day. export ttcVersion : Int -ttcVersion = 2024_01_23_00 +ttcVersion = 2024_03_29_00 export checkTTCVersion : String -> Int -> Int -> Core () diff --git a/src/Core/Context.idr b/src/Core/Context.idr index 52700615d..c12e21cd2 100644 --- a/src/Core/Context.idr +++ b/src/Core/Context.idr @@ -821,9 +821,12 @@ HasNames Error where full gam (InRHS fc n err) = InRHS fc <$> full gam n <*> full gam err full gam (MaybeMisspelling err xs) = MaybeMisspelling <$> full gam err <*> pure xs full gam (WarningAsError wrn) = WarningAsError <$> full gam wrn - full gam (OperatorBindingMismatch {print} fc expected actual opName rhs candidates) + full gam (OperatorBindingMismatch {print} fc expected actual (Left opName) rhs candidates) = OperatorBindingMismatch {print} fc expected actual - <$> full gam opName <*> pure rhs <*> pure candidates + <$> (Left <$> full gam opName) <*> pure rhs <*> pure candidates + full gam (OperatorBindingMismatch {print} fc expected actual (Right opName) rhs candidates) + = OperatorBindingMismatch {print} fc expected actual + <$> (Right <$> full gam opName) <*> pure rhs <*> pure candidates resolved gam (Fatal err) = Fatal <$> resolved gam err resolved _ (CantConvert fc gam rho s t) @@ -916,9 +919,12 @@ HasNames Error where resolved gam (InRHS fc n err) = InRHS fc <$> resolved gam n <*> resolved gam err resolved gam (MaybeMisspelling err xs) = MaybeMisspelling <$> resolved gam err <*> pure xs resolved gam (WarningAsError wrn) = WarningAsError <$> resolved gam wrn - resolved gam (OperatorBindingMismatch {print} fc expected actual opName rhs candidates) + resolved gam (OperatorBindingMismatch {print} fc expected actual (Left opName) rhs candidates) = OperatorBindingMismatch {print} fc expected actual - <$> resolved gam opName <*> pure rhs <*> pure candidates + <$> (Left <$> resolved gam opName) <*> pure rhs <*> pure candidates + resolved gam (OperatorBindingMismatch {print} fc expected actual (Right opName) rhs candidates) + = OperatorBindingMismatch {print} fc expected actual + <$> (Right <$> resolved gam opName) <*> pure rhs <*> pure candidates export HasNames Totality where diff --git a/src/Core/Core.idr b/src/Core/Core.idr index 8eaa16b60..29a282741 100644 --- a/src/Core/Core.idr +++ b/src/Core/Core.idr @@ -165,8 +165,9 @@ data Error : Type where GenericMsg : FC -> String -> Error GenericMsgSol : FC -> (message : String) -> (solutions : List String) -> Error OperatorBindingMismatch : {a : Type} -> {print : a -> Doc ()} -> - FC -> (expectedFixity : BacktickOrOperatorFixity) -> (use_site : OperatorLHSInfo a) -> - (opName : Name) -> (rhs : a) -> (candidates : List String) -> Error + FC -> (expectedFixity : FixityDeclarationInfo) -> (use_site : OperatorLHSInfo a) -> + -- left: backticked, right: op symbolds + (opName : Either Name Name) -> (rhs : a) -> (candidates : List String) -> Error TTCError : TTCErrorMsg -> Error FileErr : String -> FileError -> Error CantFindPackage : String -> Error @@ -403,7 +404,7 @@ Show Error where show (OperatorBindingMismatch fc (DeclaredFixity expected) actual opName rhs _) = show fc ++ ": Operator " ++ show opName ++ " is " ++ show expected ++ " but used as a " ++ show actual ++ " operator" - show (OperatorBindingMismatch fc Backticked actual opName rhs _) + show (OperatorBindingMismatch fc UndeclaredFixity actual opName rhs _) = show fc ++ ": Operator " ++ show opName ++ " has no declared fixity" ++ " but used as a " ++ show actual ++ " operator" diff --git a/src/Core/Hash.idr b/src/Core/Hash.idr index 20d62bba1..fedb7dbef 100644 --- a/src/Core/Hash.idr +++ b/src/Core/Hash.idr @@ -23,7 +23,7 @@ interface Hashable a where hash = hashWithSalt 5381 hashWithSalt h i = h * 33 + hash i -infixl 5 `hashWithSalt` +export infixl 5 `hashWithSalt` export Hashable Int where diff --git a/src/Core/TT.idr b/src/Core/TT.idr index cab8c5323..efa8521ac 100644 --- a/src/Core/TT.idr +++ b/src/Core/TT.idr @@ -170,11 +170,11 @@ Eq FixityInfo where ||| Whenever we read an operator from the parser, we don't know if it's a backticked expression with no fixity ||| declaration, or if it has a fixity declaration. If it does not have a declaration, we represent this state -||| with `Backticked`. +||| with `UndeclaredFixity`. ||| Note that a backticked expression can have a fixity declaration, in which case it is represented with ||| `DeclaredFixity`. public export -data BacktickOrOperatorFixity = Backticked | DeclaredFixity FixityInfo +data FixityDeclarationInfo = UndeclaredFixity | DeclaredFixity FixityInfo -- Left-hand-side information for operators, carries autobind information -- an operator can either be diff --git a/src/Idris/Desugar.idr b/src/Idris/Desugar.idr index a61fd910e..fe32b9540 100644 --- a/src/Idris/Desugar.idr +++ b/src/Idris/Desugar.idr @@ -35,6 +35,7 @@ import TTImp.TTImp import TTImp.Utils import Libraries.Data.IMaybe +import Libraries.Data.WithDefault import Libraries.Utils.Shunting import Libraries.Text.PrettyPrint.Prettyprinter @@ -106,12 +107,12 @@ mkPrec Infix = NonAssoc mkPrec Prefix = Prefix -- This is used to print the error message for fixities -[interpName] Interpolation ((Name, BacktickOrOperatorFixity), b) where - interpolate ((x, _), _) = show x +[interpName] Interpolation ((OpStr' Name, FixityDeclarationInfo), b) where + interpolate ((x, _), _) = show x.toName -[showWithLoc] Show ((Name, BacktickOrOperatorFixity), b) where +[showWithLoc] Show ((OpStr' Name, FixityDeclarationInfo), b) where show ((x, DeclaredFixity y), _) = show x ++ " at " ++ show y.fc - show ((x, Backticked), _) = show x + show ((x, UndeclaredFixity), _) = show x -- Check that an operator does not have any conflicting fixities in scope. -- Each operator can have its fixity defined multiple times across multiple @@ -121,19 +122,19 @@ mkPrec Prefix = Prefix checkConflictingFixities : {auto s : Ref Syn SyntaxInfo} -> {auto c : Ref Ctxt Defs} -> (isPrefix : Bool) -> - FC -> Name -> Core (OpPrec, BacktickOrOperatorFixity) + FC -> OpStr' Name -> Core (OpPrec, FixityDeclarationInfo) checkConflictingFixities isPrefix exprFC opn - = do let op = nameRoot opn + = do let op = nameRoot opn.toName foundFixities <- getFixityInfo op let (pre, inf) = partition ((== Prefix) . fix . snd) foundFixities case (isPrefix, pre, inf) of - -- If we do not find any fixity for this operator we check that it uses operator - -- characters, if not, it must be a backticked expression. - (_, [], []) => if any isOpChar (fastUnpack op) - then throw (GenericMsg exprFC "Unknown operator '\{op}'") - else pure (NonAssoc 1, Backticked) -- Backticks are non associative by default + -- If we do not find any fixity, and it is a backticked operator, then we + -- return the default fixity and associativity for backticked operators + -- Otherwise, it's an unknown operator. + (_, [], []) => case opn of + OpSymbols _ => throw (GenericMsg exprFC "Unknown operator '\{op}'") + Backticked _ => pure (NonAssoc 1, UndeclaredFixity) -- Backticks are non associative by default - -- (True, ((fxName, fx) :: _), _) => do -- in the prefix case, remove conflicts with infix (-) let extraFixities = pre ++ (filter (\(nm, _) => not $ nameRoot nm == "-") inf) @@ -171,17 +172,18 @@ checkConflictingFixities isPrefix exprFC opn checkConflictingBinding : Ref Ctxt Defs => Ref Syn SyntaxInfo => - FC -> Name -> (foundFixity : BacktickOrOperatorFixity) -> + FC -> OpStr -> (foundFixity : FixityDeclarationInfo) -> (usage : OperatorLHSInfo PTerm) -> (rhs : PTerm) -> Core () checkConflictingBinding fc opName foundFixity use_site rhs = if isCompatible foundFixity use_site then pure () else throw $ OperatorBindingMismatch - {print = byShow} fc foundFixity use_site opName rhs !candidates + {print = byShow} fc foundFixity use_site (opNameToEither opName) rhs !candidates where - isCompatible : BacktickOrOperatorFixity -> OperatorLHSInfo PTerm -> Bool - isCompatible Backticked (NoBinder lhs) = True - isCompatible Backticked _ = False + + isCompatible : FixityDeclarationInfo -> OperatorLHSInfo PTerm -> Bool + isCompatible UndeclaredFixity (NoBinder lhs) = True + isCompatible UndeclaredFixity _ = False isCompatible (DeclaredFixity fixInfo) (NoBinder lhs) = fixInfo.bindingInfo == NotBinding isCompatible (DeclaredFixity fixInfo) (BindType name ty) = fixInfo.bindingInfo == Typebind isCompatible (DeclaredFixity fixInfo) (BindExpr name expr) = fixInfo.bindingInfo == Autobind @@ -198,10 +200,10 @@ checkConflictingBinding fc opName foundFixity use_site rhs candidates = do let DeclaredFixity fxInfo = foundFixity | _ => pure [] -- if there is no declared fixity we can't know what's -- supposed to go there. - Just (nm, cs) <- getSimilarNames {keepPredicate = Just (keepCompatibleBinding fxInfo.bindingInfo)} opName + Just (nm, cs) <- getSimilarNames {keepPredicate = Just (keepCompatibleBinding fxInfo.bindingInfo)} opName.toName | Nothing => pure [] ns <- currentNS <$> get Ctxt - pure (showSimilarNames ns opName nm cs) + pure (showSimilarNames ns opName.toName nm cs) checkValidFixity : BindingModifier -> Fixity -> Nat -> Bool @@ -225,7 +227,7 @@ checkValidFixity _ _ _ = False parameters (side : Side) toTokList : {auto s : Ref Syn SyntaxInfo} -> {auto c : Ref Ctxt Defs} -> - PTerm -> Core (List (Tok ((OpStr, BacktickOrOperatorFixity), Maybe (OperatorLHSInfo PTerm)) PTerm)) + PTerm -> Core (List (Tok ((OpStr, FixityDeclarationInfo), Maybe (OperatorLHSInfo PTerm)) PTerm)) toTokList (POp fc opFC l opn r) = do (precInfo, fixInfo) <- checkConflictingFixities False fc opn unless (side == LHS) -- do not check for conflicting fixity on the LHS @@ -393,7 +395,7 @@ mutual = do syn <- get Syn -- It might actually be a prefix argument rather than a section -- so check that first, otherwise desugar as a lambda - case lookupName op (prefixes syn) of + case lookupName op.toName (prefixes syn) of [] => desugarB side ps (PLam fc top Explicit (PRef fc (MN "arg" 0)) (PImplicit fc) @@ -798,10 +800,10 @@ mutual {auto o : Ref ROpts REPLOpts} -> Side -> List Name -> Tree (OpStr, Maybe $ OperatorLHSInfo PTerm) PTerm -> Core PTerm - desugarTree side ps (Infix loc eqFC (UN $ Basic "=", _) l r) -- special case since '=' is special syntax + desugarTree side ps (Infix loc eqFC (OpSymbols $ UN $ Basic "=", _) l r) -- special case since '=' is special syntax = pure $ PEq eqFC !(desugarTree side ps l) !(desugarTree side ps r) - desugarTree side ps (Infix loc _ (UN $ Basic "$", _) l r) -- special case since '$' is special syntax + desugarTree side ps (Infix loc _ (OpSymbols $ UN $ Basic "$", _) l r) -- special case since '$' is special syntax = do l' <- desugarTree side ps l r' <- desugarTree side ps r pure (PApp loc l' r') @@ -809,25 +811,25 @@ mutual desugarTree side ps (Infix loc opFC (op, Just (NoBinder lhs)) l r) = do l' <- desugarTree side ps l r' <- desugarTree side ps r - pure (PApp loc (PApp loc (PRef opFC op) l') r') + pure (PApp loc (PApp loc (PRef opFC op.toName) l') r') -- (x : ty) =@ f x ==>> (=@) ty (\x : ty => f x) desugarTree side ps (Infix loc opFC (op, Just (BindType pat lhs)) l r) = do l' <- desugarTree side ps l body <- desugarTree side ps r - pure $ PApp loc (PApp loc (PRef opFC op) l') + pure $ PApp loc (PApp loc (PRef opFC op.toName) l') (PLam loc top Explicit pat l' body) -- (x := exp) =@ f x ==>> (=@) exp (\x : ? => f x) desugarTree side ps (Infix loc opFC (op, Just (BindExpr pat lhs)) l r) = do l' <- desugarTree side ps l body <- desugarTree side ps r - pure $ PApp loc (PApp loc (PRef opFC op) l') + pure $ PApp loc (PApp loc (PRef opFC op.toName) l') (PLam loc top Explicit pat (PInfer opFC) body) -- (x : ty := exp) =@ f x ==>> (=@) exp (\x : ty => f x) desugarTree side ps (Infix loc opFC (op, Just (BindExplicitType pat ty expr)) l r) = do l' <- desugarTree side ps l body <- desugarTree side ps r - pure $ PApp loc (PApp loc (PRef opFC op) l') + pure $ PApp loc (PApp loc (PRef opFC op.toName) l') (PLam loc top Explicit pat ty body) desugarTree side ps (Infix loc opFC (op, Nothing) _ r) = throw $ InternalError "illegal fixity: Parsed as infix but no binding information" @@ -838,7 +840,7 @@ mutual -- Note: In case of negated signed integer literals, we apply the -- negation directly. Otherwise, the literal might be -- truncated to 0 before being passed on to `negate`. - desugarTree side ps (Pre loc opFC (UN $ Basic "-", _) $ Leaf $ PPrimVal fc c) + desugarTree side ps (Pre loc opFC (OpSymbols $ UN $ Basic "-", _) $ Leaf $ PPrimVal fc c) = let newFC = fromMaybe EmptyFC (mergeFC loc fc) continue = desugarTree side ps . Leaf . PPrimVal newFC in case c of @@ -854,13 +856,13 @@ mutual _ => do arg' <- desugarTree side ps (Leaf $ PPrimVal fc c) pure (PApp loc (PRef opFC (UN $ Basic "negate")) arg') - desugarTree side ps (Pre loc opFC (UN $ Basic "-", _) arg) + desugarTree side ps (Pre loc opFC (OpSymbols $ UN $ Basic "-", _) arg) = do arg' <- desugarTree side ps arg pure (PApp loc (PRef opFC (UN $ Basic "negate")) arg') desugarTree side ps (Pre loc opFC (op, _) arg) = do arg' <- desugarTree side ps arg - pure (PApp loc (PRef opFC op) arg') + pure (PApp loc (PRef opFC op.toName) arg') desugarTree side ps (Leaf t) = pure t desugarType : {auto s : Ref Syn SyntaxInfo} -> @@ -1016,6 +1018,11 @@ mutual List Name -> PiInfo PTerm -> Core (PiInfo RawImp) mapDesugarPiInfo ps = PiInfo.traverse (desugar AnyExpr ps) + displayFixity : Maybe Visibility -> BindingModifier -> Fixity -> Nat -> OpStr -> String + displayFixity Nothing NotBinding fix prec op = "\{show fix} \{show prec} \{show op}" + displayFixity Nothing bind fix prec op = "\{show bind} \{show fix} \{show prec} \{show op}" + displayFixity (Just vis) bind fix prec op = "\{show vis} \{show bind} \{show fix} \{show prec} \{show op}" + -- Given a high level declaration, return a list of TTImp declarations -- which process it, and update any necessary state on the way. export @@ -1205,22 +1212,35 @@ mutual NS ns (DN str (MN ("__mk" ++ str) 0)) mkConName n = DN (show n) (MN ("__mk" ++ show n) 0) - desugarDecl ps (PFixity fc vis binding fix prec opName) + desugarDecl ps fx@(PFixity fc vis binding fix prec opName) = do unless (checkValidFixity binding fix prec) (throw $ GenericMsgSol fc "Invalid fixity, \{binding} operator must be infixr 0." [ "Make it `infixr 0`: `\{binding} infixr 0 \{show opName}`" , "Remove the binding keyword: `\{fix} \{show prec} \{show opName}`" ]) + when (isDefaulted vis) $ + let adjustedExport = displayFixity (Just Export) binding fix prec opName + adjustedPrivate = displayFixity (Just Private) binding fix prec opName + originalFixity = displayFixity Nothing binding fix prec opName + in recordWarning $ GenericWarn fc """ + Fixity declaration '\{originalFixity}' does not have an export modifier, and + will become private by default in a future version. + To expose it outside of its module, write '\{adjustedExport}'. If you + intend to keep it private, write '\{adjustedPrivate}'. + """ ctx <- get Ctxt -- We update the context of fixities by adding a namespaced fixity -- given by the current namespace and its fixity name. -- This allows fixities to be stored along with the namespace at their -- declaration site and detect and handle ambiguous fixities let updatedNS = NS (mkNestedNamespace (Just ctx.currentNS) (show fix)) - (UN $ Basic $ nameRoot opName) + (UN $ Basic $ nameRoot opName.toName) - update Syn { fixities $= addName updatedNS (MkFixityInfo fc vis binding fix prec) } + update Syn + { fixities $= + addName updatedNS + (MkFixityInfo fc (collapseDefault vis) binding fix prec) } pure [] desugarDecl ps d@(PFail fc mmsg ds) = do -- save the state: the content of a failing block should be discarded diff --git a/src/Idris/Doc/Keywords.idr b/src/Idris/Doc/Keywords.idr index 1ef73ff55..1f081303f 100644 --- a/src/Idris/Doc/Keywords.idr +++ b/src/Idris/Doc/Keywords.idr @@ -12,7 +12,8 @@ import Libraries.Data.List.Quantifiers.Extra import Libraries.Data.String.Extra -infix 10 ::= +private infix 10 ::= + data DocFor : String -> Type where (::=) : (0 str : String) -> (doc : Doc IdrisDocAnn) -> DocFor str diff --git a/src/Idris/Error.idr b/src/Idris/Error.idr index f26c6dc49..a8fd7e1cc 100644 --- a/src/Idris/Error.idr +++ b/src/Idris/Error.idr @@ -14,6 +14,7 @@ import Idris.Pretty import Parser.Source import Data.List +import Data.Either import Data.List1 import Data.String @@ -626,14 +627,14 @@ perrorRaw (GenericMsgSol fc header solutions) <+> "Possible solutions:" <+> line <+> indent 1 (vsep (map (\s => "-" <++> pretty0 s) solutions)) perrorRaw (OperatorBindingMismatch fc {print=p} expected actual opName rhs candidates) - = pure $ "Operator" <++> pretty0 !(getFullName opName) <++> "is" - <++> printBindingInfo expected + = pure $ "Operator" <++> pretty0 !(getFullName (fromEither opName)) <++> "is" + <++> printBindingInfo expected-- .bindingInfo <++> "operator, but is used as" <++> printBindingModifier actual.getBinder <++> "operator." <+> line <+> !(ploc fc) <+> "Explanation: regular, typebind and autobind operators all use a slightly different" - <++> "syntax, typebind looks like this: '(name : type)" <++> pretty0 opName - <++> "expr', autobind looks like this: '(name := expr)" <++> pretty0 opName + <++> "syntax, typebind looks like this: '(name : type)" <++> infixOpName + <++> "expr', autobind looks like this: '(name := expr)" <++> infixOpName <++> "expr'." <+> line <+> line <+> "Possible solutions:" <+> line @@ -650,45 +651,46 @@ perrorRaw (OperatorBindingMismatch fc {print=p} expected actual opName rhs candi moduleDiagnostic : Doc IdrisAnn moduleDiagnostic = case expected of - Backticked => "Import a module that exports a suitable fixity." - (DeclaredFixity a) => "Hide or remove the fixity at" <++> byShow a.fc - <++> "and import a module that exports a compatible fixity." + UndeclaredFixity => "Import a module that exports a suitable fixity." + (DeclaredFixity e) => "Hide or remove the fixity at" <++> byShow e.fc + <++> "and import a module that exports a compatible fixity." + infixOpName : Doc IdrisAnn - infixOpName = case expected of - Backticked => enclose "`" "`" (byShow opName) - _ => byShow opName + infixOpName = case opName of + Left backtickedOp => enclose "`" "`" (byShow backtickedOp) + Right symbolOp => byShow symbolOp displayFixityInfo : FixityInfo -> BindingModifier -> Doc IdrisAnn displayFixityInfo (MkFixityInfo fc1 vis _ fix precedence) NotBinding - = byShow vis <++> byShow fix <++> byShow precedence <++> pretty0 opName + = byShow vis <++> byShow fix <++> byShow precedence <++> pretty0 (fromEither opName) displayFixityInfo (MkFixityInfo _ vis _ fix precedence) usedBinder - = byShow vis <++> byShow usedBinder <++> byShow fix <++> byShow precedence <++> pretty0 opName + = byShow vis <++> byShow usedBinder <++> byShow fix <++> byShow precedence <++> pretty0 (fromEither opName) printE : ? -> Doc IdrisAnn printE x = reAnnotate (const Code) (p x) expressionDiagnositc : List (Doc IdrisAnn) expressionDiagnositc = case expected of - Backticked => [] - (DeclaredFixity e) => let sentence = "Write the expression using" <++> byShow e.bindingInfo <++> "syntax:" - in pure $ sentence <++> enclose "'" "'" (case e.bindingInfo of - NotBinding => - printE actual.getLhs <++> infixOpName <++> printE rhs - Autobind => - parens (maybe "_" printE actual.getBoundPat <++> ":=" - <++> printE actual.getLhs) - <++> infixOpName <++> printE rhs - Typebind => - parens (maybe "_" printE actual.getBoundPat <++> ":" - <++> printE actual.getLhs) - <++> infixOpName <++> printE rhs - ) <+> dot + UndeclaredFixity => [] + DeclaredFixity e => let sentence = "Write the expression using" <++> byShow e.bindingInfo <++> "syntax:" + in pure $ sentence <++> enclose "'" "'" (case e.bindingInfo of + NotBinding => + printE actual.getLhs <++> infixOpName <++> printE rhs + Autobind => + parens (maybe "_" printE actual.getBoundPat <++> ":=" + <++> printE actual.getLhs) + <++> infixOpName <++> printE rhs + Typebind => + parens (maybe "_" printE actual.getBoundPat <++> ":" + <++> printE actual.getLhs) + <++> infixOpName <++> printE rhs + ) <+> dot fixityDiagnostic : Doc IdrisAnn fixityDiagnostic = case expected of - Backticked => "Define a new fixity:" <++> "infixr 0" <++> infixOpName - (DeclaredFixity fix) => + UndeclaredFixity => "Define a new fixity:" <++> "infixr 0" <++> infixOpName + (DeclaredFixity fix) => "Change the fixity defined at" <++> pretty0 fix.fc <++> "to" <++> enclose "'" "'" (displayFixityInfo fix actual.getBinder) <+> dot @@ -698,8 +700,8 @@ perrorRaw (OperatorBindingMismatch fc {print=p} expected actual opName rhs candi printBindingModifier Typebind = "a type-binding (typebind)" printBindingModifier Autobind = "an automatically-binding (autobind)" - printBindingInfo : BacktickOrOperatorFixity -> Doc IdrisAnn - printBindingInfo Backticked = "a regular" + printBindingInfo : FixityDeclarationInfo -> Doc IdrisAnn + printBindingInfo UndeclaredFixity = "a regular" printBindingInfo (DeclaredFixity x) = printBindingModifier x.bindingInfo diff --git a/src/Idris/Parser.idr b/src/Idris/Parser.idr index e8910f52f..0be4fc526 100644 --- a/src/Idris/Parser.idr +++ b/src/Idris/Parser.idr @@ -176,9 +176,10 @@ continueWith : IndentInfo -> String -> Rule () continueWith indents req = mustContinue indents (Just req) *> symbol req -iOperator : Rule Name +iOperator : Rule OpStr iOperator - = operator <|> (symbol "`" *> name <* symbol "`") + = OpSymbols <$> operator + <|> Backticked <$> (symbol "`" *> name <* symbol "`") data ArgType = UnnamedExpArg PTerm @@ -369,14 +370,14 @@ mutual pure $ let fc = boundToFC fname (mergeBounds l r) opFC = virtualiseFC fc -- already been highlighted: we don't care - in POp fc opFC (NoBinder l.val) (UN $ Basic "=") r.val + in POp fc opFC (NoBinder l.val) (OpSymbols $ UN $ Basic "=") r.val else fail "= not allowed") <|> (do b <- bounds $ do continue indents op <- bounds iOperator e <- case op.val of - UN (Basic "$") => typeExpr q fname indents + OpSymbols (UN (Basic "$")) => typeExpr q fname indents _ => expr q fname indents pure (op, e) (op, r) <- pure b.val @@ -1175,10 +1176,10 @@ visibility fname = (specified <$> visOption fname) <|> pure defaulted -exportVisibility : OriginDesc -> EmptyRule Visibility +exportVisibility : OriginDesc -> EmptyRule (WithDefault Visibility Export) exportVisibility fname - = visOption fname - <|> pure Export + = (specified <$> visOption fname) + <|> pure defaulted tyDecls : Rule Name -> String -> OriginDesc -> IndentInfo -> Rule (List1 PTypeDecl) tyDecls declName predoc fname indents diff --git a/src/Idris/Pretty.idr b/src/Idris/Pretty.idr index 34f0eb421..ee44d85cd 100644 --- a/src/Idris/Pretty.idr +++ b/src/Idris/Pretty.idr @@ -334,24 +334,24 @@ mutual prettyPrec d (PInfer _) = annotate Hole $ "?" prettyPrec d (POp _ _ (BindType nm left) op right) = group $ parens (prettyPrec d nm <++> ":" <++> pretty left) - <++> prettyOp op + <++> prettyOp op.toName <++> pretty right prettyPrec d (POp _ _ (BindExpr nm left) op right) = group $ parens (prettyPrec d nm <++> ":=" <++> pretty left) - <++> prettyOp op + <++> prettyOp op.toName <++> pretty right prettyPrec d (POp _ _ (BindExplicitType nm ty left) op right) = group $ parens (prettyPrec d nm <++> ":" <++> pretty ty <++> ":=" <++> pretty left) - <++> prettyOp op + <++> prettyOp op.toName <++> pretty right prettyPrec d (POp _ _ (NoBinder x) op y) = parenthesise (d >= App) $ group $ pretty x - <++> prettyOp op + <++> prettyOp op.toName <++> pretty y - prettyPrec d (PPrefixOp _ _ op x) = parenthesise (d > startPrec) $ prettyOp op <+> pretty x - prettyPrec d (PSectionL _ _ op x) = parens (prettyOp op <++> pretty x) - prettyPrec d (PSectionR _ _ x op) = parens (pretty x <++> prettyOp op) + prettyPrec d (PPrefixOp _ _ op x) = parenthesise (d > startPrec) $ prettyOp op.toName <+> pretty x + prettyPrec d (PSectionL _ _ op x) = parens (prettyOp op.toName <++> pretty x) + prettyPrec d (PSectionR _ _ x op) = parens (pretty x <++> prettyOp op.toName) prettyPrec d (PEq fc l r) = parenthesise (d > startPrec) $ prettyPrec Equal l <++> equals <++> prettyPrec Equal r prettyPrec d (PBracketed _ tm) = parens (pretty tm) prettyPrec d (PString _ _ xs) = parenthesise (d > startPrec) $ hsep $ punctuate "++" (prettyPStr <$> xs) diff --git a/src/Idris/Resugar.idr b/src/Idris/Resugar.idr index 2f0607ba0..cc39c7f4f 100644 --- a/src/Idris/Resugar.idr +++ b/src/Idris/Resugar.idr @@ -46,7 +46,7 @@ mkOp tm@(PApp fc (PApp _ (PRef opFC kn) x) y) -- to know if the name is an operator or not, it's enough to check -- that the fixity context contains the name `(++)` let rootName = UN (Basic (nameRoot raw)) - let asOp = POp fc opFC (NoBinder (unbracketApp x)) kn (unbracketApp y) + let asOp = POp fc opFC (NoBinder (unbracketApp x)) (OpSymbols kn) (unbracketApp y) if not (null (lookupName rootName (infixes syn))) then pure asOp else case dropNS raw of @@ -55,7 +55,7 @@ mkOp tm@(PApp fc (PApp _ (PRef opFC kn) x) y) mkOp tm@(PApp fc (PRef opFC kn) x) = do syn <- get Syn let n = rawName kn - let asOp = PSectionR fc opFC (unbracketApp x) kn + let asOp = PSectionR fc opFC (unbracketApp x) (OpSymbols kn) if not (null $ lookupName (UN $ Basic (nameRoot n)) (infixes syn)) then pure asOp else case dropNS n of @@ -73,7 +73,7 @@ mkSectionL tm@(PLam fc rig info (PRef _ bd) ty | _ => pure tm syn <- get Syn let n = rawName kn - let asOp = PSectionL fc opFC kn (unbracketApp x) + let asOp = PSectionL fc opFC (OpSymbols kn) (unbracketApp x) if not (null $ lookupName (UN $ Basic (nameRoot n)) (fixities syn)) then pure asOp else case dropNS n of @@ -591,15 +591,15 @@ cleanPTerm ptm cleanNode (PRef fc nm) = PRef fc <$> cleanKindedName nm cleanNode (POp fc opFC abi op y) = - (\ op => POp fc opFC abi op y) <$> cleanKindedName op + (\ op => POp fc opFC abi op y) <$> traverseOp @{Functor.CORE} cleanKindedName op cleanNode (PPrefixOp fc opFC op x) = - (\ op => PPrefixOp fc opFC op x) <$> cleanKindedName op + (\ op => PPrefixOp fc opFC op x) <$> traverseOp @{Functor.CORE} cleanKindedName op cleanNode (PSectionL fc opFC op x) = - (\ op => PSectionL fc opFC op x) <$> cleanKindedName op + (\ op => PSectionL fc opFC op x) <$> traverseOp @{Functor.CORE} cleanKindedName op cleanNode (PSectionR fc opFC x op) = - PSectionR fc opFC x <$> cleanKindedName op + PSectionR fc opFC x <$> traverseOp @{Functor.CORE} cleanKindedName op cleanNode (PPi fc rig vis (Just n) arg ret) = - (\ n => PPi fc rig vis n arg ret) <$> cleanBinderName vis n + (\ n => PPi fc rig vis n arg ret) <$> (cleanBinderName vis n) cleanNode tm = pure tm toCleanPTerm : {auto c : Ref Ctxt Defs} -> diff --git a/src/Idris/Syntax.idr b/src/Idris/Syntax.idr index 56bd1b7c4..b09b3e5fd 100644 --- a/src/Idris/Syntax.idr +++ b/src/Idris/Syntax.idr @@ -30,8 +30,39 @@ import Parser.Lexer.Source %default covering public export -OpStr' : Type -> Type -OpStr' nm = nm +data OpStr' nm = OpSymbols nm | Backticked nm + +-- Left: backticked, Right: operator symbols +export +opNameToEither : OpStr' nm -> Either nm nm +opNameToEither (Backticked nm) = Left nm +opNameToEither (OpSymbols nm) = Right nm + +export +Functor OpStr' where + map f (OpSymbols x) = OpSymbols (f x) + map f (Backticked x) = Backticked (f x) + +export +Foldable OpStr' where + foldr f i (OpSymbols x) = f x i + foldr f i (Backticked x) = f x i + +export +traverseOp : (fn : Functor f) => (a -> f b) -> OpStr' a -> f (OpStr' b) +traverseOp f (OpSymbols x) = map OpSymbols (f x) +traverseOp f (Backticked x) = map Backticked (f x) + + +public export +Show nm => Show (OpStr' nm) where + show (OpSymbols nm) = show nm + show (Backticked nm) = "`\{show nm}`" + +public export +(.toName) : OpStr' nm -> nm +(.toName) (OpSymbols nm) = nm +(.toName) (Backticked nm) = nm public export OpStr : Type @@ -434,7 +465,7 @@ mutual PFail : FC -> Maybe String -> List (PDecl' nm) -> PDecl' nm PMutual : FC -> List (PDecl' nm) -> PDecl' nm - PFixity : FC -> Visibility -> BindingModifier -> Fixity -> Nat -> OpStr -> PDecl' nm + PFixity : FC -> WithDefault Visibility Export -> BindingModifier -> Fixity -> Nat -> OpStr -> PDecl' nm PNamespace : FC -> Namespace -> List (PDecl' nm) -> PDecl' nm PTransform : FC -> String -> PTerm' nm -> PTerm' nm -> PDecl' nm PRunElabDecl : FC -> PTerm' nm -> PDecl' nm @@ -832,10 +863,8 @@ parameters {0 nm : Type} (toName : nm -> Name) showPTermPrec d (PWithUnambigNames fc ns rhs) = "with " ++ show ns ++ " " ++ showPTermPrec d rhs - showOpPrec d op = let op = toName op in - if isOpName op - then showPrec d op - else "`" ++ showPrec d op ++ "`" + showOpPrec d (OpSymbols op) = showPrec d (toName op) + showOpPrec d (Backticked op) = "`\{showPrec d (toName op)}`" export covering @@ -1045,3 +1074,4 @@ Show PDecl where show (PRunElabDecl{}) = "PRunElabDecl" show (PDirective{}) = "PDirective" show (PBuiltin{}) = "PBuiltin" + diff --git a/src/Idris/Syntax/Views.idr b/src/Idris/Syntax/Views.idr index 34e9de748..c10612e46 100644 --- a/src/Idris/Syntax/Views.idr +++ b/src/Idris/Syntax/Views.idr @@ -27,7 +27,7 @@ getFnArgs embed fts = go fts [] where go (PNamedApp fc f n t) = go f . (Named fc n t ::) go (PBracketed fc f) = go f -- we don't care about the binder info here - go (POp fc opFC leftSide op r) = (PRef opFC op,) . (Explicit fc leftSide.getLhs ::) . (Explicit fc r ::) + go (POp fc opFC leftSide op r) = (PRef opFC op.toName,) . (Explicit fc leftSide.getLhs ::) . (Explicit fc r ::) go (PEq fc l r) = (PRef fc $ embed eqName,) . (Explicit fc l ::) . (Explicit fc r ::) -- ambiguous, picking the type constructor here go (PPair fc l r) = (PRef fc $ embed pairname,) . (Explicit fc l ::) . (Explicit fc r ::) diff --git a/src/Libraries/Data/Ordering/Extra.idr b/src/Libraries/Data/Ordering/Extra.idr index 1e00a524a..f9691042c 100644 --- a/src/Libraries/Data/Ordering/Extra.idr +++ b/src/Libraries/Data/Ordering/Extra.idr @@ -2,7 +2,7 @@ module Libraries.Data.Ordering.Extra %default total -infixl 5 `thenCmp` +export infixl 5 `thenCmp` export thenCmp : Ordering -> Lazy Ordering -> Ordering diff --git a/src/Libraries/Data/PosMap.idr b/src/Libraries/Data/PosMap.idr index 00dbdf686..d38b46dd4 100644 --- a/src/Libraries/Data/PosMap.idr +++ b/src/Libraries/Data/PosMap.idr @@ -12,8 +12,8 @@ import Data.List %default total -infixr 5 <|, <: -infixl 5 |>, :> +export infixr 5 <|, <: +export infixl 5 |>, :> public export FileRange : Type diff --git a/src/Libraries/Data/String/Extra.idr b/src/Libraries/Data/String/Extra.idr index ece2ad214..6a6dea930 100644 --- a/src/Libraries/Data/String/Extra.idr +++ b/src/Libraries/Data/String/Extra.idr @@ -7,8 +7,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. ||| diff --git a/src/Libraries/Text/Parser/Core.idr b/src/Libraries/Text/Parser/Core.idr index a3e9ef7ca..adb808024 100644 --- a/src/Libraries/Text/Parser/Core.idr +++ b/src/Libraries/Text/Parser/Core.idr @@ -132,7 +132,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 diff --git a/src/Libraries/Text/PrettyPrint/Prettyprinter/Doc.idr b/src/Libraries/Text/PrettyPrint/Prettyprinter/Doc.idr index d74599e3f..61e39077b 100644 --- a/src/Libraries/Text/PrettyPrint/Prettyprinter/Doc.idr +++ b/src/Libraries/Text/PrettyPrint/Prettyprinter/Doc.idr @@ -134,7 +134,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 diff --git a/src/Libraries/Utils/Path.idr b/src/Libraries/Utils/Path.idr index 896643738..7a148dc4e 100644 --- a/src/Libraries/Utils/Path.idr +++ b/src/Libraries/Utils/Path.idr @@ -19,9 +19,9 @@ import System.File %default total -infixl 5 , /> -infixr 7 <.> -infixr 7 <..> +export infixl 5 , /> +export infixr 7 <.> +export infixr 7 <..> ||| The character that separates directories in the path. diff --git a/tests/base/sortedmap_001/SortedMapTest.idr b/tests/base/sortedmap_001/SortedMapTest.idr index c6222f5b8..cc107e867 100644 --- a/tests/base/sortedmap_001/SortedMapTest.idr +++ b/tests/base/sortedmap_001/SortedMapTest.idr @@ -3,7 +3,7 @@ import Data.SortedMap (&~) : a -> (a -> b) -> b (&~) x f = f x -infixl 2 &~ +private infixl 2 &~ testLookupBetween : List (Maybe (Maybe (Int,Int),Maybe (Int,Int))) testLookupBetween = diff --git a/tests/ideMode/ideMode005/LetBinders.idr b/tests/ideMode/ideMode005/LetBinders.idr index ac8a898bf..40ed1e683 100644 --- a/tests/ideMode/ideMode005/LetBinders.idr +++ b/tests/ideMode/ideMode005/LetBinders.idr @@ -1,6 +1,6 @@ module LetBinders -infix 1 ::: +private infix 1 ::: record List1 (a : Type) where constructor (:::) head : a diff --git a/tests/ideMode/ideMode005/expectedG b/tests/ideMode/ideMode005/expectedG index 4b8df8d28..f7bbd2dde 100644 --- a/tests/ideMode/ideMode005/expectedG +++ b/tests/ideMode/ideMode005/expectedG @@ -2,8 +2,9 @@ 00003e(:write-string "1/1: Building LetBinders (LetBinders.idr)" 1) 000075(:output (:ok (:highlight-source ((((:filename "LetBinders.idr") (:start 0 0) (:end 0 6)) ((:decor :keyword)))))) 1) 000075(:output (:ok (:highlight-source ((((:filename "LetBinders.idr") (:start 0 7) (:end 0 17)) ((:decor :module)))))) 1) -000075(:output (:ok (:highlight-source ((((:filename "LetBinders.idr") (:start 2 0) (:end 2 5)) ((:decor :keyword)))))) 1) -000075(:output (:ok (:highlight-source ((((:filename "LetBinders.idr") (:start 2 6) (:end 2 7)) ((:decor :keyword)))))) 1) +000075(:output (:ok (:highlight-source ((((:filename "LetBinders.idr") (:start 2 0) (:end 2 7)) ((:decor :keyword)))))) 1) +000076(:output (:ok (:highlight-source ((((:filename "LetBinders.idr") (:start 2 8) (:end 2 13)) ((:decor :keyword)))))) 1) +000077(:output (:ok (:highlight-source ((((:filename "LetBinders.idr") (:start 2 14) (:end 2 15)) ((:decor :keyword)))))) 1) 000075(:output (:ok (:highlight-source ((((:filename "LetBinders.idr") (:start 3 0) (:end 3 6)) ((:decor :keyword)))))) 1) 000073(:output (:ok (:highlight-source ((((:filename "LetBinders.idr") (:start 3 7) (:end 3 12)) ((:decor :type)))))) 1) 000077(:output (:ok (:highlight-source ((((:filename "LetBinders.idr") (:start 3 13) (:end 3 14)) ((:decor :keyword)))))) 1) diff --git a/tests/idris2/basic/basic002/Do.idr b/tests/idris2/basic/basic002/Do.idr index 9da45c9f0..e3262f636 100644 --- a/tests/idris2/basic/basic002/Do.idr +++ b/tests/idris2/basic/basic002/Do.idr @@ -1,7 +1,7 @@ data Maybe a = Nothing | Just a -infixl 1 >>= +private infixl 1 >>= (>>=) : Maybe a -> (a -> Maybe b) -> Maybe b (>>=) Nothing k = Nothing diff --git a/tests/idris2/basic/basic003/Ambig2.idr b/tests/idris2/basic/basic003/Ambig2.idr index 306805c23..b59ac7b5e 100644 --- a/tests/idris2/basic/basic003/Ambig2.idr +++ b/tests/idris2/basic/basic003/Ambig2.idr @@ -1,4 +1,4 @@ -infixr 5 :: +private infixr 5 :: export data List a = Nil | (::) a (List a) diff --git a/tests/idris2/basic/basic004/Stuff.idr b/tests/idris2/basic/basic004/Stuff.idr index 73c10a4f1..87a3798c6 100644 --- a/tests/idris2/basic/basic004/Stuff.idr +++ b/tests/idris2/basic/basic004/Stuff.idr @@ -36,7 +36,7 @@ plus : Nat -> Nat -> Nat plus Z y = y plus (S k) y = S (plus k y) -infixr 5 :: +export infixr 5 :: public export data List a = Nil | (::) a (List a) diff --git a/tests/idris2/basic/basic006/Stuff.idr b/tests/idris2/basic/basic006/Stuff.idr index c129ba5d2..c4d208de8 100644 --- a/tests/idris2/basic/basic006/Stuff.idr +++ b/tests/idris2/basic/basic006/Stuff.idr @@ -36,7 +36,7 @@ plus : Nat -> Nat -> Nat plus Z y = y plus (S k) y = S (plus k y) -infixr 5 :: +export infixr 5 :: public export data List a = Nil | (::) a (List a) diff --git a/tests/idris2/basic/basic007/Stuff.idr b/tests/idris2/basic/basic007/Stuff.idr index c129ba5d2..c4d208de8 100644 --- a/tests/idris2/basic/basic007/Stuff.idr +++ b/tests/idris2/basic/basic007/Stuff.idr @@ -36,7 +36,7 @@ plus : Nat -> Nat -> Nat plus Z y = y plus (S k) y = S (plus k y) -infixr 5 :: +export infixr 5 :: public export data List a = Nil | (::) a (List a) diff --git a/tests/idris2/basic/basic009/Stuff.idr b/tests/idris2/basic/basic009/Stuff.idr index 361f0a553..4421123bc 100644 --- a/tests/idris2/basic/basic009/Stuff.idr +++ b/tests/idris2/basic/basic009/Stuff.idr @@ -13,7 +13,7 @@ not False = True public export data Maybe a = Nothing | Just a -infixl 4 && +export infixl 4 && public export (&&) : Bool -> Lazy Bool -> Bool @@ -43,7 +43,7 @@ plus : Nat -> Nat -> Nat plus Z y = y plus (S k) y = S (plus k y) -infixr 5 :: +export infixr 5 :: public export data List a = Nil | (::) a (List a) diff --git a/tests/idris2/basic/basic028/Do.idr b/tests/idris2/basic/basic028/Do.idr index 9da45c9f0..e3262f636 100644 --- a/tests/idris2/basic/basic028/Do.idr +++ b/tests/idris2/basic/basic028/Do.idr @@ -1,7 +1,7 @@ data Maybe a = Nothing | Just a -infixl 1 >>= +private infixl 1 >>= (>>=) : Maybe a -> (a -> Maybe b) -> Maybe b (>>=) Nothing k = Nothing diff --git a/tests/idris2/basic/basic058/DataTypeOp.idr b/tests/idris2/basic/basic058/DataTypeOp.idr index 36ac4e26f..1df6a2947 100644 --- a/tests/idris2/basic/basic058/DataTypeOp.idr +++ b/tests/idris2/basic/basic058/DataTypeOp.idr @@ -1,19 +1,19 @@ --- Data declarations --- -infix 0 =%= +private infix 0 =%= public export data (=%=) : (a -> b) -> (a -> b) -> Type where ExtEq : {0 f, g : a -> b} -> ((x : a) -> f x = g x) -> f =%= g -infix 0 %% +private infix 0 %% public export data (%%) a b = Equs (a = b) (b = a) --- Records --- -infix 0 =%%= +private infix 0 =%%= public export record (=%%=) {a : Type} {b : Type} (f : a -> b) (g : a -> b) where @@ -22,7 +22,7 @@ record (=%%=) {a : Type} {b : Type} (f : a -> b) (g : a -> b) where --- Interfaces --- -infix 0 =%%%= +private infix 0 =%%%= public export interface (=%%%=) (x : a) (y : a) (b : Type) (i : Type) where diff --git a/tests/idris2/interface/interface001/IFace.idr b/tests/idris2/interface/interface001/IFace.idr index 41e8f56ef..33d769c09 100644 --- a/tests/idris2/interface/interface001/IFace.idr +++ b/tests/idris2/interface/interface001/IFace.idr @@ -4,7 +4,7 @@ import Stuff %default partial -infixl 5 ==, /= +private infixl 5 ==, /= interface Eq b where (==) : b -> b -> Bool diff --git a/tests/idris2/interface/interface001/IFace1.idr b/tests/idris2/interface/interface001/IFace1.idr index 0a9d9ba30..1f9801fed 100644 --- a/tests/idris2/interface/interface001/IFace1.idr +++ b/tests/idris2/interface/interface001/IFace1.idr @@ -4,7 +4,7 @@ import Stuff %default partial -infixl 5 ==, /= +private infixl 5 ==, /= interface Eq b where (==) : b -> b -> Bool diff --git a/tests/idris2/interface/interface001/Stuff.idr b/tests/idris2/interface/interface001/Stuff.idr index 8e163324c..f63f76301 100644 --- a/tests/idris2/interface/interface001/Stuff.idr +++ b/tests/idris2/interface/interface001/Stuff.idr @@ -13,7 +13,7 @@ not False = True public export data Maybe a = Nothing | Just a -infixl 4 && +export infixl 4 && public export (&&) : Bool -> Bool -> Bool @@ -43,7 +43,7 @@ plus : Nat -> Nat -> Nat plus Z y = y plus (S k) y = S (plus k y) -infixr 5 :: +export infixr 5 :: public export data List a = Nil | (::) a (List a) @@ -52,7 +52,7 @@ public export data Equal : a -> b -> Type where Refl : {0 x : a} -> Equal x x -infix 9 ===, ~=~ +export infix 9 ===, ~=~ public export (===) : (x : a) -> (y : a) -> Type diff --git a/tests/idris2/interface/interface002/Stuff.idr b/tests/idris2/interface/interface002/Stuff.idr index 8bcc33117..e88a1aae5 100644 --- a/tests/idris2/interface/interface002/Stuff.idr +++ b/tests/idris2/interface/interface002/Stuff.idr @@ -36,7 +36,7 @@ plus : Nat -> Nat -> Nat plus Z y = y plus (S k) y = S (plus k y) -infixr 5 :: +export infixr 5 :: public export data List a = Nil | (::) a (List a) diff --git a/tests/idris2/interface/interface006/Apply.idr b/tests/idris2/interface/interface006/Apply.idr index 92407dfc2..8eca32865 100644 --- a/tests/idris2/interface/interface006/Apply.idr +++ b/tests/idris2/interface/interface006/Apply.idr @@ -2,7 +2,7 @@ module Apply -- These are not Biapplicatives. Those are in Data.Biapplicative -infixl 4 <<$>>, <<&>>, <<.>>, <<., .>>, <<..>> +export infixl 4 <<$>>, <<&>>, <<.>>, <<., .>>, <<..>> ||| Primarily used to make the definitions of bilift2 and bilift3 pretty ||| diff --git a/tests/idris2/interface/interface006/Biapplicative.idr b/tests/idris2/interface/interface006/Biapplicative.idr index 00c564309..22b14bde2 100644 --- a/tests/idris2/interface/interface006/Biapplicative.idr +++ b/tests/idris2/interface/interface006/Biapplicative.idr @@ -2,7 +2,7 @@ module Biapplicative import Apply -infixl 4 <<*>>, <<*, *>>, <<**>> +export infixl 4 <<*>>, <<*, *>>, <<**>> ||| Biapplicatives ||| @p the action of the Biapplicative on pairs of objects diff --git a/tests/idris2/interface/interface006/Bimonad.idr b/tests/idris2/interface/interface006/Bimonad.idr index d0eef33fc..b62f46888 100644 --- a/tests/idris2/interface/interface006/Bimonad.idr +++ b/tests/idris2/interface/interface006/Bimonad.idr @@ -2,7 +2,7 @@ module Bimonad import Biapplicative -infixl 4 >>== +export infixl 4 >>== ||| Bimonads ||| @p the action of the first Bifunctor component on pairs of objects diff --git a/tests/idris2/interface/interface024/EH.idr b/tests/idris2/interface/interface024/EH.idr index a03b2f94c..364f5e31e 100644 --- a/tests/idris2/interface/interface024/EH.idr +++ b/tests/idris2/interface/interface024/EH.idr @@ -1,8 +1,8 @@ import Syntax.PreorderReasoning -------- some notation ---------- -infixr 6 .+.,:+: -infixr 7 .*.,:*: +private infixr 6 .+.,:+: +private infixr 7 .*.,:*: interface Additive a where constructor MkAdditive diff --git a/tests/idris2/linear/linear001/Stuff.idr b/tests/idris2/linear/linear001/Stuff.idr index d0081e435..ffc56c203 100644 --- a/tests/idris2/linear/linear001/Stuff.idr +++ b/tests/idris2/linear/linear001/Stuff.idr @@ -43,7 +43,7 @@ plus : Nat -> Nat -> Nat plus Z y = y plus (S k) y = S (plus k y) -infixr 5 :: +export infixr 5 :: public export data List a = Nil | (::) a (List a) diff --git a/tests/idris2/linear/linear002/Stuff.idr b/tests/idris2/linear/linear002/Stuff.idr index d0081e435..ffc56c203 100644 --- a/tests/idris2/linear/linear002/Stuff.idr +++ b/tests/idris2/linear/linear002/Stuff.idr @@ -43,7 +43,7 @@ plus : Nat -> Nat -> Nat plus Z y = y plus (S k) y = S (plus k y) -infixr 5 :: +export infixr 5 :: public export data List a = Nil | (::) a (List a) diff --git a/tests/idris2/linear/linear012/linholes.idr b/tests/idris2/linear/linear012/linholes.idr index f5bfdff78..0f5d6c979 100644 --- a/tests/idris2/linear/linear012/linholes.idr +++ b/tests/idris2/linear/linear012/linholes.idr @@ -1,4 +1,4 @@ -infixr 6 -* +private infixr 6 -* (-*) : Type -> Type -> Type (-*) a b = (1 _ : a) -> b diff --git a/tests/idris2/misc/docs004/List.idr b/tests/idris2/misc/docs004/List.idr index aaac9b8bf..402f3b8c1 100644 --- a/tests/idris2/misc/docs004/List.idr +++ b/tests/idris2/misc/docs004/List.idr @@ -2,8 +2,8 @@ module List data List a = Nil | (::) a (List a) -infixr 5 :: -infixr 5 ++ +export infixr 5 :: +export infixr 5 ++ interface Monoid ty where ||| Users can hand-craft their own monoid implementations diff --git a/tests/idris2/misc/import009/Test.idr b/tests/idris2/misc/import009/Test.idr index 78aae7420..184d7600e 100644 --- a/tests/idris2/misc/import009/Test.idr +++ b/tests/idris2/misc/import009/Test.idr @@ -5,6 +5,7 @@ infixr 5 ~:> public export infixr 5 ~> +export infixl 5 |> public export diff --git a/tests/idris2/misc/lazy001/Lazy.idr b/tests/idris2/misc/lazy001/Lazy.idr index 69bd065a6..7c34448a2 100644 --- a/tests/idris2/misc/lazy001/Lazy.idr +++ b/tests/idris2/misc/lazy001/Lazy.idr @@ -1,4 +1,4 @@ -infixr 5 :: +private infixr 5 :: namespace List public export diff --git a/tests/idris2/misc/namespace005/Lib1.idr b/tests/idris2/misc/namespace005/Lib1.idr index f358c8153..b7ee29179 100644 --- a/tests/idris2/misc/namespace005/Lib1.idr +++ b/tests/idris2/misc/namespace005/Lib1.idr @@ -1,6 +1,6 @@ module Lib1 -infixr 5 %%% +export infixr 5 %%% export (%%%) : Nat -> Nat -> Nat diff --git a/tests/idris2/misc/namespace005/Lib2.idr b/tests/idris2/misc/namespace005/Lib2.idr index 8c8c8825e..0a0efa9d0 100644 --- a/tests/idris2/misc/namespace005/Lib2.idr +++ b/tests/idris2/misc/namespace005/Lib2.idr @@ -1,3 +1,3 @@ module Lib2 -infixl 5 %%% +export infixl 5 %%% diff --git a/tests/idris2/misc/namespace005/LibPre1.idr b/tests/idris2/misc/namespace005/LibPre1.idr index 9b8963c87..cdfedf0dc 100644 --- a/tests/idris2/misc/namespace005/LibPre1.idr +++ b/tests/idris2/misc/namespace005/LibPre1.idr @@ -1,6 +1,6 @@ module LibPre1 -prefix 6 *! +export prefix 6 *! export (*!) : Nat -> Nat diff --git a/tests/idris2/misc/namespace005/LibPre2.idr b/tests/idris2/misc/namespace005/LibPre2.idr index 7fff7c0fc..f045e6e12 100644 --- a/tests/idris2/misc/namespace005/LibPre2.idr +++ b/tests/idris2/misc/namespace005/LibPre2.idr @@ -1,3 +1,3 @@ module LibPre2 -prefix 2 *! +export prefix 2 *! diff --git a/tests/idris2/misc/namespace005/Main3.idr b/tests/idris2/misc/namespace005/Main3.idr index eae81a68b..a419e90cd 100644 --- a/tests/idris2/misc/namespace005/Main3.idr +++ b/tests/idris2/misc/namespace005/Main3.idr @@ -2,8 +2,8 @@ module Main3 import Lib1 -prefix 4 %%% -infixr 8 - +private prefix 4 %%% +private infixr 8 - (%%%) : Nat -> Nat (%%%) = S diff --git a/tests/idris2/misc/namespace005/NonConflict1.idr b/tests/idris2/misc/namespace005/NonConflict1.idr index d3c212bf3..6d5a64c8d 100644 --- a/tests/idris2/misc/namespace005/NonConflict1.idr +++ b/tests/idris2/misc/namespace005/NonConflict1.idr @@ -1,6 +1,6 @@ module NonConflict1 -infixr 5 &&& +export infixr 5 &&& export (&&&) : Nat -> Nat -> Nat diff --git a/tests/idris2/misc/namespace005/NonConflict2.idr b/tests/idris2/misc/namespace005/NonConflict2.idr index 4b767df4b..f73597be8 100644 --- a/tests/idris2/misc/namespace005/NonConflict2.idr +++ b/tests/idris2/misc/namespace005/NonConflict2.idr @@ -1,3 +1,3 @@ module NonConflict2 -infixr 5 &&& +export infixr 5 &&& diff --git a/tests/idris2/misc/pretty001/Issue1328A.idr b/tests/idris2/misc/pretty001/Issue1328A.idr index bb9a7cc96..9c15ca95b 100644 --- a/tests/idris2/misc/pretty001/Issue1328A.idr +++ b/tests/idris2/misc/pretty001/Issue1328A.idr @@ -1,7 +1,7 @@ module Issue1328A %default total -infix 4 `InCtx` +private infix 4 `InCtx` data InCtx : (a, b : Type) -> Type where prop0 : a `InCtx` b @@ -22,7 +22,7 @@ def1 m n = (`div` n) m def2 : (m, n : Integer) -> Integer def2 m n = (m `div`) n -infix 4 |- +private infix 4 |- data (|-) : (a, b : Type) -> Type where inProp0 : a |- b diff --git a/tests/idris2/operators/operators001/Test.idr b/tests/idris2/operators/operators001/Test.idr index c33218298..78f95861d 100644 --- a/tests/idris2/operators/operators001/Test.idr +++ b/tests/idris2/operators/operators001/Test.idr @@ -3,8 +3,8 @@ module Test import Data.Vect -typebind infixr 0 =@ -infixr 0 -@ +private typebind infixr 0 =@ +private infixr 0 -@ -- typebind infixr 1 =@@ @@ -39,7 +39,7 @@ map4 : (x : a) =@ (b -@ (y : List a) =@ List b) test3 : Test.map3 === Test.map4 -typebind infixr 0 *> +private typebind infixr 0 *> -- (*>) : (ty : Type) -> (ty -> Type) -> Type -- (*>) = DPair @@ -47,7 +47,7 @@ typebind infixr 0 *> -- testCompose : (x : Nat) *> (y : Nat) *> Vect (n + m) String -- testCompose = (1 ** 2 ** ["hello", "world", "!"]) -autobind infixr 0 `MyLet` +private autobind infixr 0 `MyLet` MyLet : (val) -> (val -> rest) -> rest MyLet arg fn = fn arg @@ -58,14 +58,14 @@ program = (n := 3) `MyLet` 2 + n program2 : Nat program2 = (n : Nat := 3) `MyLet` 2 + n -typebind infixr 0 |> +private typebind infixr 0 |> record Container where constructor (|>) shape : Type position : shape -> Type -typebind infixr 0 @@ +private typebind infixr 0 @@ record (@@) (x : Type) (y : x -> Type) where constructor PairUp diff --git a/tests/idris2/operators/operators002/Error2.idr b/tests/idris2/operators/operators002/Error2.idr index e3b6a420d..5d5e97893 100644 --- a/tests/idris2/operators/operators002/Error2.idr +++ b/tests/idris2/operators/operators002/Error2.idr @@ -1,5 +1,5 @@ -typebind infixr 0 =@ +private typebind infixr 0 =@ 0 (=@) : (a : Type) -> (a -> Type) -> Type (=@) a f = (1 x : a) -> f x diff --git a/tests/idris2/operators/operators002/Errors.idr b/tests/idris2/operators/operators002/Errors.idr index 4ee059bf5..89c69f796 100644 --- a/tests/idris2/operators/operators002/Errors.idr +++ b/tests/idris2/operators/operators002/Errors.idr @@ -1,5 +1,5 @@ -typebind infixr 0 =@ +private typebind infixr 0 =@ 0 (=@) : (a : Type) -> (a -> Type) -> Type (=@) a f = (1 x : a) -> f x diff --git a/tests/idris2/operators/operators002/Errors2.idr b/tests/idris2/operators/operators002/Errors2.idr index f7b6e7b22..f36ace64d 100644 --- a/tests/idris2/operators/operators002/Errors2.idr +++ b/tests/idris2/operators/operators002/Errors2.idr @@ -1,5 +1,5 @@ -autobind infixr 0 =@ +private autobind infixr 0 =@ 0 (=@) : (a : Type) -> (a -> Type) -> Type (=@) a f = (1 x : a) -> f x diff --git a/tests/idris2/operators/operators002/Errors3.idr b/tests/idris2/operators/operators002/Errors3.idr index 0e8994ec5..b9a7ec0cc 100644 --- a/tests/idris2/operators/operators002/Errors3.idr +++ b/tests/idris2/operators/operators002/Errors3.idr @@ -1,5 +1,5 @@ -typebind infixr 0 =@ +private typebind infixr 0 =@ 0 (=@) : (a : Type) -> (a -> Type) -> Type (=@) a f = (1 x : a) -> f x diff --git a/tests/idris2/operators/operators002/Errors4.idr b/tests/idris2/operators/operators002/Errors4.idr index d6a52f928..56e1786a8 100644 --- a/tests/idris2/operators/operators002/Errors4.idr +++ b/tests/idris2/operators/operators002/Errors4.idr @@ -1,5 +1,5 @@ -infixr 0 =@ +private infixr 0 =@ 0 (=@) : (a : Type) -> (a -> Type) -> Type (=@) a f = (1 x : a) -> f x diff --git a/tests/idris2/operators/operators002/Errors5.idr b/tests/idris2/operators/operators002/Errors5.idr index fd7225832..4e84a1e12 100644 --- a/tests/idris2/operators/operators002/Errors5.idr +++ b/tests/idris2/operators/operators002/Errors5.idr @@ -1,6 +1,6 @@ -infixr 0 =@ +private infixr 0 =@ 0 (=@) : (a : Type) -> (a -> Type) -> Type (=@) a f = (1 x : a) -> f x diff --git a/tests/idris2/operators/operators002/Lin.idr b/tests/idris2/operators/operators002/Lin.idr new file mode 100644 index 000000000..830e53fd7 --- /dev/null +++ b/tests/idris2/operators/operators002/Lin.idr @@ -0,0 +1,4 @@ +module Lin + +export typebind infixr 0 =@ + diff --git a/tests/idris2/operators/operators002/LinImport.idr b/tests/idris2/operators/operators002/LinImport.idr new file mode 100644 index 000000000..c31930b5f --- /dev/null +++ b/tests/idris2/operators/operators002/LinImport.idr @@ -0,0 +1,9 @@ + +import Lin + +0 (=@) : (a : Type) -> (a -> Type) -> Type +(=@) a f = (1 x : a) -> f x + +data S : {ty : Type} -> (x : ty) -> Type where + MkS : (x := ty) =@ S x + diff --git a/tests/idris2/operators/operators002/Test.idr b/tests/idris2/operators/operators002/Test.idr index b50c78f4c..901e7dda8 100644 --- a/tests/idris2/operators/operators002/Test.idr +++ b/tests/idris2/operators/operators002/Test.idr @@ -2,8 +2,8 @@ import Data.Vect -typebind infixr 0 =@ -infixr 0 -@ +private typebind infixr 0 =@ +private infixr 0 -@ 0 (=@) : (a : Type) -> (a -> Type) -> Type (=@) a f = (1 x : a) -> f x @@ -18,7 +18,7 @@ data S : {ty : Type} -> (x : ty) -> Type where Mk4 : ty -@ (x : ty) =@ S x Chain : (x : ty =@ y : ty =@ S (x, y)) -typebind infixr 0 *> +private typebind infixr 0 *> -- (*>) : (ty : Type) -> (ty -> Type) -> Type -- (*>) = DPair @@ -26,7 +26,7 @@ typebind infixr 0 *> -- testCompose : (x : Nat) *> (y : Nat) *> Vect (n + m) String -- testCompose = (1 ** 2 ** ["hello", "world", "!"]) -autobind infixr 7 `MyLet` +private autobind infixr 7 `MyLet` MyLet : (val) -> (val -> rest) -> rest MyLet arg fn = fn arg diff --git a/tests/idris2/operators/operators002/expected b/tests/idris2/operators/operators002/expected index 8451e1d0b..6da168498 100644 --- a/tests/idris2/operators/operators002/expected +++ b/tests/idris2/operators/operators002/expected @@ -12,8 +12,8 @@ Explanation: regular, typebind and autobind operators all use a slightly differe Possible solutions: - Write the expression using typebind syntax: '(x : ty) =@ S x'. - - Change the fixity defined at Errors:2:10--2:21 to 'export autobind infixr 0 =@'. - - Hide or remove the fixity at Errors:2:10--2:21 and import a module that exports a compatible fixity. + - Change the fixity defined at Errors:2:18--2:29 to 'private autobind infixr 0 =@'. + - Hide or remove the fixity at Errors:2:18--2:29 and import a module that exports a compatible fixity. 1/1: Building Errors2 (Errors2.idr) Error: Operator =@ is an automatically-binding (autobind) operator, but is used as a regular operator. @@ -28,8 +28,8 @@ Explanation: regular, typebind and autobind operators all use a slightly differe Possible solutions: - Write the expression using autobind syntax: '(_ := a) =@ a'. - - Change the fixity defined at Errors2:2:10--2:21 to 'export infixr 0 =@'. - - Hide or remove the fixity at Errors2:2:10--2:21 and import a module that exports a compatible fixity. + - Change the fixity defined at Errors2:2:18--2:29 to 'private infixr 0 =@'. + - Hide or remove the fixity at Errors2:2:18--2:29 and import a module that exports a compatible fixity. 1/1: Building Errors3 (Errors3.idr) Error: Operator =@ is a type-binding (typebind) operator, but is used as a regular operator. @@ -44,8 +44,8 @@ Explanation: regular, typebind and autobind operators all use a slightly differe Possible solutions: - Write the expression using typebind syntax: '(_ : a) =@ a'. - - Change the fixity defined at Errors3:2:10--2:21 to 'export infixr 0 =@'. - - Hide or remove the fixity at Errors3:2:10--2:21 and import a module that exports a compatible fixity. + - Change the fixity defined at Errors3:2:18--2:29 to 'private infixr 0 =@'. + - Hide or remove the fixity at Errors3:2:18--2:29 and import a module that exports a compatible fixity. 1/1: Building Errors4 (Errors4.idr) Error: Operator =@ is a regular operator, but is used as a type-binding (typebind) operator. @@ -60,8 +60,8 @@ Explanation: regular, typebind and autobind operators all use a slightly differe Possible solutions: - Write the expression using regular syntax: 'ty =@ S x'. - - Change the fixity defined at Errors4:2:1--2:12 to 'export typebind infixr 0 =@'. - - Hide or remove the fixity at Errors4:2:1--2:12 and import a module that exports a compatible fixity. + - Change the fixity defined at Errors4:2:9--2:20 to 'private typebind infixr 0 =@'. + - Hide or remove the fixity at Errors4:2:9--2:20 and import a module that exports a compatible fixity. 1/1: Building Errors5 (Errors5.idr) Error: Operator =@ is a regular operator, but is used as an automatically-binding (autobind) operator. @@ -76,5 +76,22 @@ Explanation: regular, typebind and autobind operators all use a slightly differe Possible solutions: - Write the expression using regular syntax: 'ty =@ S x'. - - Change the fixity defined at Errors5:3:1--3:12 to 'export autobind infixr 0 =@'. - - Hide or remove the fixity at Errors5:3:1--3:12 and import a module that exports a compatible fixity. + - Change the fixity defined at Errors5:3:9--3:20 to 'private autobind infixr 0 =@'. + - Hide or remove the fixity at Errors5:3:9--3:20 and import a module that exports a compatible fixity. +1/2: Building Lin (Lin.idr) +2/2: Building LinImport (LinImport.idr) +Error: Operator =@ is a type-binding (typebind) operator, but is used as an automatically-binding (autobind) operator. + +LinImport:8:19--8:21 + 4 | 0 (=@) : (a : Type) -> (a -> Type) -> Type + 5 | (=@) a f = (1 x : a) -> f x + 6 | + 7 | data S : {ty : Type} -> (x : ty) -> Type where + 8 | MkS : (x := ty) =@ S x + ^^ +Explanation: regular, typebind and autobind operators all use a slightly different syntax, typebind looks like this: '(name : type) =@ expr', autobind looks like this: '(name := expr) =@ expr'. + +Possible solutions: + - Write the expression using typebind syntax: '(x : ty) =@ S x'. + - Change the fixity defined at Lin:3:17--3:28 to 'export autobind infixr 0 =@'. + - Hide or remove the fixity at Lin:3:17--3:28 and import a module that exports a compatible fixity. diff --git a/tests/idris2/operators/operators002/run b/tests/idris2/operators/operators002/run index 13baec981..0edd4d47f 100755 --- a/tests/idris2/operators/operators002/run +++ b/tests/idris2/operators/operators002/run @@ -5,4 +5,5 @@ check Errors2.idr check Errors3.idr check Errors4.idr check Errors5.idr +check LinImport.idr diff --git a/tests/idris2/operators/operators004/Test.idr b/tests/idris2/operators/operators004/Test.idr index 25093fc0e..bea8e1fb6 100644 --- a/tests/idris2/operators/operators004/Test.idr +++ b/tests/idris2/operators/operators004/Test.idr @@ -1,7 +1,7 @@ -infix 5 -:- +private infix 5 -:- -infix 5 :-: +private infix 5 :-: (-:-) : a -> List a -> List a (-:-) = (::) diff --git a/tests/idris2/operators/operators004/expected b/tests/idris2/operators/operators004/expected index f976037ea..9a060b5ce 100644 --- a/tests/idris2/operators/operators004/expected +++ b/tests/idris2/operators/operators004/expected @@ -11,7 +11,7 @@ Test:13:8--13:22 Possible solutions: - Add brackets around every use of -:- - - Change the fixity of -:- at Test:2:1--2:12 to `infixl` or `infixr` + - Change the fixity of -:- at Test:2:9--2:20 to `infixl` or `infixr` Error: Operator :-: is non-associative Test:16:9--16:23 @@ -24,4 +24,4 @@ Test:16:9--16:23 Possible solutions: - Add brackets around every use of :-: - - Change the fixity of :-: at Test:4:1--4:12 to `infixl` or `infixr` + - Change the fixity of :-: at Test:4:9--4:20 to `infixl` or `infixr` diff --git a/tests/idris2/operators/operators005/Test.idr b/tests/idris2/operators/operators005/Test.idr index a96b27435..9e5a6a81a 100644 --- a/tests/idris2/operators/operators005/Test.idr +++ b/tests/idris2/operators/operators005/Test.idr @@ -1,8 +1,8 @@ import Data.String -typebind infixr 0 :- -autobind infixr 0 `for` +private typebind infixr 0 :- +private autobind infixr 0 `for` record Container where constructor (:-) diff --git a/tests/idris2/operators/operators006/Test.idr b/tests/idris2/operators/operators006/Test.idr index b9aa1639c..d83d122e5 100644 --- a/tests/idris2/operators/operators006/Test.idr +++ b/tests/idris2/operators/operators006/Test.idr @@ -1,7 +1,7 @@ import Data.Fin -autobind infixr 0 `bind` +private autobind infixr 0 `bind` bind : Monad m => m a -> (a -> m b) -> m b bind = (>>=) diff --git a/tests/idris2/operators/operators007/Test.idr b/tests/idris2/operators/operators007/Test.idr index b15090ce2..cc28d7cfa 100644 --- a/tests/idris2/operators/operators007/Test.idr +++ b/tests/idris2/operators/operators007/Test.idr @@ -1,7 +1,7 @@ import Data.Fin -autobind infixr 0 >> +private autobind infixr 0 >> (>>) : Monad m => m a -> (a -> m b) -> m b (>>) = (>>=) diff --git a/tests/idris2/operators/operators007/Test2.idr b/tests/idris2/operators/operators007/Test2.idr index 021923a00..d16a843bd 100644 --- a/tests/idris2/operators/operators007/Test2.idr +++ b/tests/idris2/operators/operators007/Test2.idr @@ -1,8 +1,8 @@ import Data.Fin -autobind infixr 0 >> -autobind infixr 0 >= +private autobind infixr 0 >> +private autobind infixr 0 >= (>>) : Monad m => m a -> (a -> m b) -> m b (>>) = (>>=) diff --git a/tests/idris2/operators/operators007/expected b/tests/idris2/operators/operators007/expected index 8644014d4..d93d1084e 100644 --- a/tests/idris2/operators/operators007/expected +++ b/tests/idris2/operators/operators007/expected @@ -12,8 +12,8 @@ Explanation: regular, typebind and autobind operators all use a slightly differe Possible solutions: - Write the expression using regular syntax: 'm >>= Just (x + y)'. - - Change the fixity defined at Prelude.Ops:20:1--20:37 to 'export autobind infixl 1 >>='. - - Hide or remove the fixity at Prelude.Ops:20:1--20:37 and import a module that exports a compatible fixity. + - Change the fixity defined at Prelude.Ops:20:8--20:44 to 'export autobind infixl 1 >>='. + - Hide or remove the fixity at Prelude.Ops:20:8--20:44 and import a module that exports a compatible fixity. - Did you mean '>>' ? 1/1: Building Test2 (Test2.idr) Error: Operator >>= is a regular operator, but is used as an automatically-binding (autobind) operator. @@ -29,6 +29,6 @@ Explanation: regular, typebind and autobind operators all use a slightly differe Possible solutions: - Write the expression using regular syntax: 'm >>= Just (x + y)'. - - Change the fixity defined at Prelude.Ops:20:1--20:37 to 'export autobind infixl 1 >>='. - - Hide or remove the fixity at Prelude.Ops:20:1--20:37 and import a module that exports a compatible fixity. + - Change the fixity defined at Prelude.Ops:20:8--20:44 to 'export autobind infixl 1 >>='. + - Hide or remove the fixity at Prelude.Ops:20:8--20:44 and import a module that exports a compatible fixity. - Did you mean either of: '>=', '>>' ? diff --git a/tests/idris2/operators/operators008/Test.idr b/tests/idris2/operators/operators008/Test.idr index 328dfb3c2..8b7e1561c 100644 --- a/tests/idris2/operators/operators008/Test.idr +++ b/tests/idris2/operators/operators008/Test.idr @@ -4,7 +4,7 @@ import Test2 %hide Test2.infixr.(@>) -infixl 9 @> +private infixl 9 @> (@>) : a -> b -> (a, b) (@>) = MkPair diff --git a/tests/idris2/operators/operators009/Test.idr b/tests/idris2/operators/operators009/Test.idr new file mode 100644 index 000000000..f4a1a92dc --- /dev/null +++ b/tests/idris2/operators/operators009/Test.idr @@ -0,0 +1,4 @@ + +infixr 0 =@ +export infixl 9 -:- + diff --git a/tests/idris2/operators/operators009/expected b/tests/idris2/operators/operators009/expected new file mode 100644 index 000000000..a584bda3c --- /dev/null +++ b/tests/idris2/operators/operators009/expected @@ -0,0 +1,11 @@ +1/1: Building Test (Test.idr) +Warning: Fixity declaration 'infixr 0 =@' does not have an export modifier, and +will become private by default in a future version. +To expose it outside of its module, write 'export regular infixr 0 =@'. If you +intend to keep it private, write 'private regular infixr 0 =@'. + +Test:2:1--2:12 + 1 | + 2 | infixr 0 =@ + ^^^^^^^^^^^ + diff --git a/tests/idris2/operators/operators009/run b/tests/idris2/operators/operators009/run new file mode 100755 index 000000000..d35387bb3 --- /dev/null +++ b/tests/idris2/operators/operators009/run @@ -0,0 +1,3 @@ +. ../../../testutils.sh + +check Test.idr diff --git a/tests/idris2/reflection/reflection016/Eta.idr b/tests/idris2/reflection/reflection016/Eta.idr index ee191ceaf..21af530da 100644 --- a/tests/idris2/reflection/reflection016/Eta.idr +++ b/tests/idris2/reflection/reflection016/Eta.idr @@ -7,7 +7,7 @@ import Language.Reflection x : List String x = ["a", "b"] -infixl 1 >==> +private infixl 1 >==> -- From prelude: --(>=>) : Monad m => (a -> m b) -> (b -> m c) -> (a -> m c) diff --git a/tests/idris2/reg/reg023/boom.idr b/tests/idris2/reg/reg023/boom.idr index f740e38a0..c00ea99ab 100644 --- a/tests/idris2/reg/reg023/boom.idr +++ b/tests/idris2/reg/reg023/boom.idr @@ -2,7 +2,7 @@ import Data.Vect %default total -infix 3 .<=. +private infix 3 .<=. (.<=.) : Int -> Int -> Bool (.<=.) p q = case (p, q) of (0, _) => True diff --git a/tests/idris2/reg/reg034/void.idr b/tests/idris2/reg/reg034/void.idr index 11ee407d3..ba2a22e44 100644 --- a/tests/idris2/reg/reg034/void.idr +++ b/tests/idris2/reg/reg034/void.idr @@ -1,6 +1,6 @@ -infixl 0 ~~ -prefix 1 |~ -infix 1 ... +private infixl 0 ~~ +private prefix 1 |~ +private infix 1 ... public export (...) : (x : a) -> (y ~=~ x) -> (z : a ** y ~=~ z) diff --git a/tests/idris2/warning/warning004/Lib1.idr b/tests/idris2/warning/warning004/Lib1.idr index f358c8153..b7ee29179 100644 --- a/tests/idris2/warning/warning004/Lib1.idr +++ b/tests/idris2/warning/warning004/Lib1.idr @@ -1,6 +1,6 @@ module Lib1 -infixr 5 %%% +export infixr 5 %%% export (%%%) : Nat -> Nat -> Nat diff --git a/tests/idris2/warning/warning004/Lib2.idr b/tests/idris2/warning/warning004/Lib2.idr index 8c8c8825e..0a0efa9d0 100644 --- a/tests/idris2/warning/warning004/Lib2.idr +++ b/tests/idris2/warning/warning004/Lib2.idr @@ -1,3 +1,3 @@ module Lib2 -infixl 5 %%% +export infixl 5 %%% diff --git a/tests/typedd-book/chapter06/DataStore.idr b/tests/typedd-book/chapter06/DataStore.idr index 73406d2e6..b16fc3fbc 100644 --- a/tests/typedd-book/chapter06/DataStore.idr +++ b/tests/typedd-book/chapter06/DataStore.idr @@ -5,7 +5,7 @@ import Data.String import Data.Vect import System.REPL -infixr 5 .+. +private infixr 5 .+. data Schema = SString | SInt | (.+.) Schema Schema diff --git a/tests/typedd-book/chapter06/DataStoreHoles.idr b/tests/typedd-book/chapter06/DataStoreHoles.idr index 620760e9a..ed4cc0295 100644 --- a/tests/typedd-book/chapter06/DataStoreHoles.idr +++ b/tests/typedd-book/chapter06/DataStoreHoles.idr @@ -4,7 +4,7 @@ import Data.String import Data.Vect import System.REPL -infixr 5 .+. +private infixr 5 .+. data Schema = SString | SInt | (.+.) Schema Schema diff --git a/tests/typedd-book/chapter10/DataStore.idr b/tests/typedd-book/chapter10/DataStore.idr index ea10754ec..3ac4afda6 100644 --- a/tests/typedd-book/chapter10/DataStore.idr +++ b/tests/typedd-book/chapter10/DataStore.idr @@ -2,7 +2,7 @@ module DataStore import Data.Vect -infixr 5 .+. +export infixr 5 .+. public export data Schema = SString | SInt | (.+.) Schema Schema diff --git a/tests/typedd-book/chapter12/DataStore.idr b/tests/typedd-book/chapter12/DataStore.idr index a284db2df..e816c515f 100644 --- a/tests/typedd-book/chapter12/DataStore.idr +++ b/tests/typedd-book/chapter12/DataStore.idr @@ -2,7 +2,7 @@ module Main import Data.Vect -infixr 5 .+. +private infixr 5 .+. data Schema = SString | SInt | (.+.) Schema Schema