diff --git a/CHANGELOG_NEXT.md b/CHANGELOG_NEXT.md index 997f2b100..992ab72d8 100644 --- a/CHANGELOG_NEXT.md +++ b/CHANGELOG_NEXT.md @@ -26,6 +26,10 @@ This CHANGELOG describes the merged but unreleased changes. Please see [CHANGELO ### Language changes +* Autobind and Typebind modifier on operators allow the user to + customise the syntax of operator to look more like a binder. + See [#3113](https://github.com/idris-lang/Idris2/issues/3113). + ### Backend changes #### RefC diff --git a/docs/source/reference/builtins.rst b/docs/source/reference/builtins.rst index 013317685..6274ab9f3 100644 --- a/docs/source/reference/builtins.rst +++ b/docs/source/reference/builtins.rst @@ -47,7 +47,7 @@ To ensure that a type is optimized to an ``Integer``, use ``%builtin Natural`` i data MyNat = Succ MyNat | Zero - + %builtin Natural MyNat Casting between natural numbers and integer @@ -106,7 +106,7 @@ that a function is correct. It is your responsibility to make sure this is corre data ComplexNat = Zero | Succ ComplexNat - + integerToMaybeNat : Integer -> Maybe ComplexNat integerToMaybeNat _ = ... diff --git a/docs/source/reference/index.rst b/docs/source/reference/index.rst index d1217d09c..6c615141d 100644 --- a/docs/source/reference/index.rst +++ b/docs/source/reference/index.rst @@ -22,6 +22,7 @@ This is a placeholder, to get set up with readthedocs. records literate overloadedlit + operators strings pragmas builtins diff --git a/docs/source/reference/operators.rst b/docs/source/reference/operators.rst new file mode 100644 index 000000000..fd9484793 --- /dev/null +++ b/docs/source/reference/operators.rst @@ -0,0 +1,341 @@ +.. _operators: + +********* +Operators +********* + +Idris2 does not have syntax blocs (like in Idris1) or mixfix operators (like in Agda). +Instead, it expands on the abilities of infix operators to enable library designers +to write Domain Specific Languages (DSLs) while keeping error messages under control. + +Because operators are not linked to function definitions, they are also part of the +file namespacing and follow the same rules as other defintions. + +.. warning:: + Operators can and will make some code less legible. Use with taste and caution. + This document is meant to be mainly used by library authors and advanced users. + If you are on the fence about using operators, err on the side of caution and + avoid them. + +Basics +====== + +Before we jump into the fancy features, let us explain how operators work +for most users. + +When you see an expression + + +.. code-block:: idris + + 1 + n + +It means that there is a function ``(+)`` and a *fixity* declaration +in scope. A fixity for this operator looks like this + +.. code-block:: idris + + infixl 8 + + +It starts with a fixity keyword, you have the choice to use either ``infixl``, +``infixr``, ``infix`` or ``prefix``. + +``infixl`` means the operator is left-associative, so that successive applications +of the operator will bracket to the left: ``n + m + 3 + x = (((n + m) + 3) + x)```. +Similarly, ``infixr`` is right-associative, and ``infix`` is non-associative, so the +brackets are mandatory. Here, we chose for ``+`` to be left-associative, hence ``infixl``. + +The number after the fixity indicate the *precedence level* of the operator, that is, if it should +be bracketed before, or after, other operators used in the same expression. For example, +we want ``*`` to *take precedence* over ``+`` we write: + +.. code-block:: idris + + infixl 9 * + +This way, the expression ``n + m * x`` is correctly interpreted as ``n + (m * x)``. + +Fixity declarations are optional and change how a file is parsed, but you can +use any function defined with operator symbols with parenthesis around it: + +.. code-block:: idris + + -- those two are the same + n + 3 + (+) n 3 + +Because fixities are separated from the function definitions, a single operator +can have 0 or multiple fixity definitions. In the next section, we explain how to +deal with multiple fixity definitions. + +Fixity & Precedence Namespacing +=============================== +Sometimes it could be that you need to import two libraries that export +conflicting fixities. If that is the case, the compiler will emit a warning +and pick one of the fixities to parse the file. If that happens, you should +hide the fixity definitions that you do not wish to use. For this, use the +``%hide`` directive, just like you would to hide a function definition, but +use the fixity and the operator to hide at the end. Let's work through an +example: + +.. code-block:: idris + + module A + export infixl 8 - + +.. code-block:: idris + + module B + export infixr 5 - + +.. code-block:: idris + + module C + + import A + import B + + test : Int + test = 1 - 3 - 10 + +This program will raise a warning on the last line of module ``C`` because +there are two conflicting fixities in scope. Should we parse the expression +as ``(1 - 3) - 10`` or as ``1 - (3 - 10)``? In those cases, you can hide +the extra fixity you do not wish to use by using ``%hide``: + +.. code-block:: idris + + module C + + import A + import B + + %hide A.infixl.(-) + + test : Int + test = 1 - 3 - 10 -- all good, no error + +In which case the program will be parsed as ``1 - (3 - 10)`` and not emit +any errors. + +Export modifiers on fixities +---------------------------- + +Just like other top-level declarations in the language, fixities can be exported +with the ``export`` access modifier, or kept private with ``private``. + +A ``private`` fixity will remain in scope for the rest of the file but will not be +visible to users that import the module. Because fixities and operators are +separate, this does not mean you cannot use the functions that have this operator +name, it merely means that you cannot use it in infix position. But you can use +it as a regular function application using brackets. Let us see what this +looks like + +.. code-block:: idris + + module A + + private infixl &&& 8 + + -- a binary function making use of our fixity definition + export + (&&&) : ... + +.. code-block:: idris + + module B + + import A + + main : IO () + main = do print (a &&& b) -- won't work + print ((&&&) a b) -- ok + +In what follows, we have two examples of programs that benefit from +declaring a fixity ``private`` rather than ``export``. + +Private record fixity pattern +----------------------------- + +Private fixity declarations are useful in conjuction with records. When +you declare a record with operators as fields, it is helpful to write +them in infix position. However, the compiler will also synthesize a +projection function for the field that takes as first argument the +a value of the record to project from. This makes using the operator +as a binary infix operator impossible, since it now has 3 arguments. + +.. code-block:: idris + + + infixl 7 <@> + + record SomeRelation (a : Type) where + (<@>) : a -> a -> Type + -- we use the field here in infix position + compose : {x, y, z : a} -> x <@> y -> y <@> z -> x <@> z + + lteRel : SomeRelation Nat + lteRel = ... + + -- we want to use <@> in infix position here as well but we cannot + natRel : Nat -> Nat -> Type + natRel x y = (<@>) lteRel x y + +What we really want to write is ``natRel x y = (<@>) x y`` but +``(<@>)`` now has type ``SomeRelation a -> a -> a -> Type``. + +The solution is to define a private field with a private fixity +and a public one which relies on proof search to find the appropriate +argument: + +.. code-block:: idris + + private infixl 7 + export infixl 7 <@> + + record SomeRelation (a : Type) where + () : a -> a -> Type + compose : {x, y, z : a} -> x y -> y z -> x z + + export + (<@>) : (rel : SomeRelation a) => a -> a -> Type + x <@> y = () rel x y + + %hint + lteRel : SomeRelation Nat + lteRel = ... + + natRel : Nat -> Nat -> Type + natRel x y = x <@> y + +We define ``(<@>)`` as a projection function with an implicit parameter +allowing it to be used as a binary operator once again. + +Private Local definition +------------------------ + +Private fixity definitions are useful when redefining an operator fixity +in a module. This happens when multiple DSLs are imported as the same time +and you do not want to expose conflicting fixity declarations: + +.. code-block:: idris + + module Coproduct + + import Product + + -- mark this as private since we don't want to clash + -- with the Prelude + when importing the module + private infixr 5 + + + data (+) : a -> a -> Type where + ... + + distrib1 : {x, y, z : a} -> x + y + z -> (x + y) + z + +Here ``distrib1`` makes explicit use of the operator being defined as +right-associative. + +Typebind Operators +================== + +In dependently-typed programming, we have the ability define constructors which +first argument is a type and the second is a type indexed over the first argument. +A typical example of this is the dependent linear arrow: + + .. code-block:: idris + + infixr 0 =@ + 0 (=@) : (x : Type) -> (x -> Type) -> Type + (=@) x f = (1 v : x) -> f v + + +However, when trying to use it in infix position, we have to use a lambda to populate the +second argument: + +.. code-block:: idris + + linearSingleton : Nat =@ (\x => Singleton x) + linearSingleton = ... + +What we really want to write, is something like the dependent arrow ``->`` but +for linear types: + +.. code-block:: idris + + linearSingleton : (x : Nat) =@ Singleton x + linearSingleton = ... + +The above syntax is allowed if the operator is declared as ``typebind``. For +this, simply add the ``typebind`` keyword in front of the fixity declaration. + +.. code-block:: idris + + typebind infixr 0 =@ + +``typebind`` is a modifier like ``export`` and both can be used at the same time. + + +An operator defined as ``typebind`` cannot be used in regular position anymore, +writing ``Nat =@ (\x => Singleton x)`` will raise an error. + +This new syntax is purely syntax sugar and converts any instance of +``(name : type) op expr`` into ``type op (\name : type => expr)`` + +Because of its left-to-right binding structure, typebind operators can +only ever be ``infixr`` with precedence 0. + + +Autobind Operators +================== + +Typebind operators allow to bind a *type* on the left side of an operator, so that is can +be used as the index of the second argument. But sometimes, there is no dependency +between the first and second argument, yet we still want to use binding syntax. For those +cases, we use ``autobind``. + +An example of this is a DSL for a dependently-typed programming language +where the constructor for ``Pi`` takes terms on the left and lambdas on the right: + +.. code-block:: idris + + VPi : Value -> (Value -> Value) -> Value + + sig : Value + sig = VPi VStar (\fstTy -> VPi + (VPi fstTy (const VStar)) (\sndTy -> VPi + fstTy (\val1 -> VPi + (sndTy `vapp` val1) (\val2 -> + VSigma fstTy sndTy))))) + +We would like to use a custom operator to build values using ``VPi``, but its +signature does not follow the pattern that ``typebind`` uses. Instead, we use +``autobind`` to tell the compiler that the type of the lambda must be inferred. +For this we use ``:=`` instead of ``:``: + +.. code-block:: idris + + autobind infixr 0 =>> + (=>>) : Value -> (Value -> Value) -> Value + (=>>) = VPi + + + sig : Value + sig = + (fstTy := VStar) =>> + (sndTy := (_ := fstTy) =>> VStar) =>> + (val1 := fstTy) =>> + (val2 := sndTy `vapp` val1) =>> + VSigma fstTy sndTy + +This new syntax is much closer to what the code is meant to look like for users +accustomed to dependently-typed programming languages. + +More technically, any ``autobind`` operator is called with the syntax +``(name := expr) op body`` and is desugared into ``expr op (\name : ? => body)``. +If you want, or need, to give the type explicitly, you can still do so by using +the full syntax: ``(name : type := expr) op body`` which is desugared into +``expr op (\name : type => body)``. + +Like ``typebind``, ``autobind`` operators cannot be used as regular operators anymore +, additionally an ``autobind`` operator cannot use the ``typebind`` syntax either. diff --git a/src/Core/Binary.idr b/src/Core/Binary.idr index bd9a4e4ce..813dd9a96 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 = 2023_09_08_00 +ttcVersion = 2024_01_23_00 export checkTTCVersion : String -> Int -> Int -> Core () diff --git a/src/Core/Context.idr b/src/Core/Context.idr index 04ae3e8b9..4c388606d 100644 --- a/src/Core/Context.idr +++ b/src/Core/Context.idr @@ -796,6 +796,7 @@ HasNames Error where full gam (BadRunElab fc rho s desc) = BadRunElab fc <$> full gam rho <*> full gam s <*> pure desc full gam (RunElabFail e) = RunElabFail <$> full gam e full gam (GenericMsg fc x) = pure (GenericMsg fc x) + full gam (GenericMsgSol fc x y) = pure (GenericMsgSol fc x y) full gam (TTCError x) = pure (TTCError x) full gam (FileErr x y) = pure (FileErr x y) full gam (CantFindPackage x) = pure (CantFindPackage x) @@ -820,6 +821,9 @@ 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) + = OperatorBindingMismatch {print} fc expected actual + <$> full gam opName <*> pure rhs <*> pure candidates resolved gam (Fatal err) = Fatal <$> resolved gam err resolved _ (CantConvert fc gam rho s t) @@ -887,6 +891,7 @@ HasNames Error where resolved gam (BadRunElab fc rho s desc) = BadRunElab fc <$> resolved gam rho <*> resolved gam s <*> pure desc resolved gam (RunElabFail e) = RunElabFail <$> resolved gam e resolved gam (GenericMsg fc x) = pure (GenericMsg fc x) + resolved gam (GenericMsgSol fc x y) = pure (GenericMsgSol fc x y) resolved gam (TTCError x) = pure (TTCError x) resolved gam (FileErr x y) = pure (FileErr x y) resolved gam (CantFindPackage x) = pure (CantFindPackage x) @@ -911,6 +916,9 @@ 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) + = OperatorBindingMismatch {print} fc expected actual + <$> resolved gam opName <*> pure rhs <*> pure candidates export HasNames Totality where @@ -1123,7 +1131,10 @@ getFieldNames ctxt recNS -- Find similar looking names in the context export getSimilarNames : {auto c : Ref Ctxt Defs} -> - Name -> Core (Maybe (String, List (Name, Visibility, Nat))) + -- Predicate run to customise the behavior of looking for similar names + -- Sometime we might want to hide names that we know make no sense. + {default Nothing keepPredicate : Maybe ((Name, GlobalDef) -> Core Bool)} -> + Name -> Core (Maybe (String, List (Name, Visibility, Nat))) getSimilarNames nm = case show <$> userNameRoot nm of Nothing => pure Nothing Just str => if length str <= 1 then pure (Just (str, [])) else @@ -1137,6 +1148,9 @@ getSimilarNames nm = case show <$> userNameRoot nm of | False => pure Nothing Just def <- lookupCtxtExact nm (gamma defs) | Nothing => pure Nothing -- should be impossible + let predicate = fromMaybe (\_ => pure True) keepPredicate + True <- predicate (nm, def) + | False => pure Nothing pure (Just (collapseDefault $ visibility def, dist)) kept <- NameMap.mapMaybeM @{CORE} test (resolvedAs (gamma defs)) pure $ Just (str, toList kept) diff --git a/src/Core/Core.idr b/src/Core/Core.idr index 3fe662fab..8eaa16b60 100644 --- a/src/Core/Core.idr +++ b/src/Core/Core.idr @@ -10,6 +10,7 @@ import Data.Vect import Libraries.Data.IMaybe import Libraries.Text.PrettyPrint.Prettyprinter import Libraries.Text.PrettyPrint.Prettyprinter.Util +import Libraries.Text.PrettyPrint.Prettyprinter.Doc import Libraries.Data.Tap import public Data.IORef @@ -162,6 +163,10 @@ data Error : Type where FC -> Env Term vars -> Term vars -> (description : String) -> Error RunElabFail : Error -> Error 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 TTCError : TTCErrorMsg -> Error FileErr : String -> FileError -> Error CantFindPackage : String -> Error @@ -350,6 +355,7 @@ Show Error where show (BadRunElab fc env script desc) = show fc ++ ":Bad elaborator script " ++ show script ++ " (" ++ desc ++ ")" show (RunElabFail e) = "Error during reflection: " ++ show e show (GenericMsg fc str) = show fc ++ ":" ++ str + show (GenericMsgSol fc msg sols) = show fc ++ ":" ++ msg ++ " Solutions: " ++ show sols show (TTCError msg) = "Error in TTC file: " ++ show msg show (FileErr fname err) = "File error (" ++ fname ++ "): " ++ show err show (CantFindPackage fname) = "Can't find package " ++ fname @@ -390,10 +396,16 @@ Show Error where show err show (MaybeMisspelling err ns) - = show err ++ "\nDid you mean" ++ case ns of - (n ::: []) => ": " ++ n ++ "?" - _ => " any of: " ++ showSep ", " (map show (forget ns)) ++ "?" + = show err ++ "\nDid you mean" ++ case ns of + (n ::: []) => ": " ++ n ++ "?" + _ => " any of: " ++ showSep ", " (map show (forget ns)) ++ "?" show (WarningAsError w) = show w + 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 fc ++ ": Operator " ++ show opName ++ " has no declared fixity" + ++ " but used as a " ++ show actual ++ " operator" export getWarningLoc : Warning -> FC @@ -459,6 +471,7 @@ getErrorLoc (BadImplicit loc _) = Just loc getErrorLoc (BadRunElab loc _ _ _) = Just loc getErrorLoc (RunElabFail e) = getErrorLoc e getErrorLoc (GenericMsg loc _) = Just loc +getErrorLoc (GenericMsgSol loc _ _) = Just loc getErrorLoc (TTCError _) = Nothing getErrorLoc (FileErr _ _) = Nothing getErrorLoc (CantFindPackage _) = Nothing @@ -483,6 +496,7 @@ getErrorLoc (InLHS _ _ err) = getErrorLoc err getErrorLoc (InRHS _ _ err) = getErrorLoc err getErrorLoc (MaybeMisspelling err _) = getErrorLoc err getErrorLoc (WarningAsError warn) = Just (getWarningLoc warn) +getErrorLoc (OperatorBindingMismatch fc _ _ _ _ _) = Just fc export killWarningLoc : Warning -> Warning @@ -547,6 +561,7 @@ killErrorLoc (BadImplicit fc x) = BadImplicit emptyFC x killErrorLoc (BadRunElab fc x y description) = BadRunElab emptyFC x y description killErrorLoc (RunElabFail e) = RunElabFail $ killErrorLoc e killErrorLoc (GenericMsg fc x) = GenericMsg emptyFC x +killErrorLoc (GenericMsgSol fc x y) = GenericMsgSol emptyFC x y killErrorLoc (TTCError x) = TTCError x killErrorLoc (FileErr x y) = FileErr x y killErrorLoc (CantFindPackage x) = CantFindPackage x @@ -571,6 +586,9 @@ killErrorLoc (InLHS fc x err) = InLHS emptyFC x (killErrorLoc err) killErrorLoc (InRHS fc x err) = InRHS emptyFC x (killErrorLoc err) killErrorLoc (MaybeMisspelling err xs) = MaybeMisspelling (killErrorLoc err) xs killErrorLoc (WarningAsError wrn) = WarningAsError (killWarningLoc wrn) +killErrorLoc (OperatorBindingMismatch {print} fc expected actual opName rhs candidates) + = OperatorBindingMismatch {print} emptyFC expected actual opName rhs candidates + -- Core is a wrapper around IO that is specialised for efficiency. export diff --git a/src/Core/TT.idr b/src/Core/TT.idr index 427ee4638..cab8c5323 100644 --- a/src/Core/TT.idr +++ b/src/Core/TT.idr @@ -15,6 +15,7 @@ import Decidable.Equality import Libraries.Data.NameMap import Libraries.Text.PrettyPrint.Prettyprinter import Libraries.Text.PrettyPrint.Prettyprinter.Util +import Libraries.Text.Bounded import Libraries.Data.String.Extra import Libraries.Data.SnocList.SizeOf @@ -101,6 +102,136 @@ Ord Visibility where compare Public Private = GT compare Public Export = GT +public export +data Fixity = InfixL | InfixR | Infix | Prefix + +export +Show Fixity where + show InfixL = "infixl" + show InfixR = "infixr" + show Infix = "infix" + show Prefix = "prefix" + +export +Interpolation Fixity where + interpolate = show + +export +Eq Fixity where + InfixL == InfixL = True + InfixR == InfixR = True + Infix == Infix = True + Prefix == Prefix = True + _ == _ = False + + +public export +data BindingModifier = NotBinding | Autobind | Typebind + +export +Eq BindingModifier where + NotBinding == NotBinding = True + Autobind == Autobind = True + Typebind == Typebind = True + _ == _ = False + +export +Show BindingModifier where + show NotBinding = "regular" + show Typebind = "typebind" + show Autobind = "autobind" + +export +Interpolation BindingModifier where + interpolate = show + +-- A record to hold all the information about a fixity +public export +record FixityInfo where + constructor MkFixityInfo + fc : FC + vis : Visibility + bindingInfo : BindingModifier + fix : Fixity + precedence : Nat + +export +Show FixityInfo where + show fx = "fc: \{show fx.fc}, visibility: \{show fx.vis}, binding: \{show fx.bindingInfo}, fixity: \{show fx.fix}, precedence: \{show fx.precedence}" + + +export +Eq FixityInfo where + x == y = x.fc == y.fc + && x.vis == y.vis + && x.bindingInfo == y.bindingInfo + && x.fix == y.fix + && x.precedence == y.precedence + +||| 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`. +||| 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 + +-- Left-hand-side information for operators, carries autobind information +-- an operator can either be +-- - not autobind, a regular operator +-- - binding types, such that `(nm : ty) =@ fn nm` desugars into `(=@) ty (\(nm : ty) => fn nm)` +-- - binding expressing with an inferred type such that +-- `(nm := exp) =@ fn nm` desugars into `(=@) exp (\(nm : ?) => fn nm)` +-- - binding both types and expression such that +-- `(nm : ty := exp) =@ fn nm` desugars into `(=@) exp (\(nm : ty) => fn nm)` +public export +data OperatorLHSInfo : tm -> Type where + -- Traditional operator wihtout binding, carries the lhs + NoBinder : (lhs : tm) -> OperatorLHSInfo tm + -- (nm : ty) =@ fn x + BindType : (name : tm) -> (ty : tm) -> OperatorLHSInfo tm + -- (nm := exp) =@ fn nm + BindExpr : (name : tm) -> (expr : tm) -> OperatorLHSInfo tm + -- (nm : ty := exp) =@ fn nm + BindExplicitType : (name : tm) -> (type, expr : tm) -> OperatorLHSInfo tm + +export +Show (OperatorLHSInfo tm) where + show (NoBinder lhs) = "regular" + show (BindType name ty) = "type-binding (typebind)" + show (BindExpr name expr) = "automatically-binding (autobind)" + show (BindExplicitType name type expr) = "automatically-binding (autobind)" + +%name OperatorLHSInfo opInfo + +export +Functor OperatorLHSInfo where + map f (NoBinder lhs) = NoBinder $ f lhs + map f (BindType nm lhs) = BindType (f nm) (f lhs) + map f (BindExpr nm lhs) = BindExpr (f nm) (f lhs) + map f (BindExplicitType nm ty lhs) = BindExplicitType (f nm) (f ty) (f lhs) + +export +(.getLhs) : OperatorLHSInfo tm -> tm +(.getLhs) (NoBinder lhs) = lhs +(.getLhs) (BindExpr _ lhs) = lhs +(.getLhs) (BindType _ lhs) = lhs +(.getLhs) (BindExplicitType _ _ lhs) = lhs + +export +(.getBoundPat) : OperatorLHSInfo tm -> Maybe tm +(.getBoundPat) (NoBinder lhs) = Nothing +(.getBoundPat) (BindType name ty) = Just name +(.getBoundPat) (BindExpr name expr) = Just name +(.getBoundPat) (BindExplicitType name type expr) = Just name + +export +(.getBinder) : OperatorLHSInfo tm -> BindingModifier +(.getBinder) (NoBinder lhs) = NotBinding +(.getBinder) (BindType name ty) = Typebind +(.getBinder) (BindExpr name expr) = Autobind +(.getBinder) (BindExplicitType name type expr) = Autobind + public export data TotalReq = Total | CoveringOnly | PartialOK %name TotalReq treq diff --git a/src/Idris/Desugar.idr b/src/Idris/Desugar.idr index f9196dd34..a61fd910e 100644 --- a/src/Idris/Desugar.idr +++ b/src/Idris/Desugar.idr @@ -105,6 +105,14 @@ mkPrec InfixR = AssocR 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 + +[showWithLoc] Show ((Name, BacktickOrOperatorFixity), b) where + show ((x, DeclaredFixity y), _) = show x ++ " at " ++ show y.fc + show ((x, Backticked), _) = 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 -- modules as long as the fixities are consistent. If they aren't, the fixity @@ -113,39 +121,43 @@ mkPrec Prefix = Prefix checkConflictingFixities : {auto s : Ref Syn SyntaxInfo} -> {auto c : Ref Ctxt Defs} -> (isPrefix : Bool) -> - FC -> Name -> Core OpPrec + FC -> Name -> Core (OpPrec, BacktickOrOperatorFixity) checkConflictingFixities isPrefix exprFC opn - = do syn <- get Syn - let op = nameRoot opn - let foundFixities : List (Name, FixityInfo) = lookupName (UN (Basic op)) (fixities syn) + = do let op = nameRoot opn + 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) -- Backticks are non associative by default + else pure (NonAssoc 1, Backticked) -- 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) unless (isCompatible fx extraFixities) $ warnConflict fxName extraFixities - pure (mkPrec fx.fix fx.precedence) - -- Could not find any prefix operator fixities, there may be infix ones + pure (mkPrec fx.fix fx.precedence, DeclaredFixity fx) + -- Could not find any prefix operator fixities, there may still be conflicts with + -- the infix ones. (True, [] , _) => throw (GenericMsg exprFC $ "'\{op}' is not a prefix operator") (False, _, ((fxName, fx) :: _)) => do -- In the infix case, remove conflicts with prefix (-) let extraFixities = (filter (\(nm, _) => not $ nm == UN (Basic "-")) pre) ++ inf unless (isCompatible fx extraFixities) $ warnConflict fxName extraFixities - pure (mkPrec fx.fix fx.precedence) + pure (mkPrec fx.fix fx.precedence, DeclaredFixity fx) -- Could not find any infix operator fixities, there may be prefix ones (False, _, []) => throw (GenericMsg exprFC $ "'\{op}' is not an infix operator") where - -- Fixities are compatible with all others of the same name that share the same fixity and precedence + -- Fixities are compatible with all others of the same name that share the same + -- fixity, precedence, and binding information isCompatible : FixityInfo -> (fixities : List (Name, FixityInfo)) -> Bool isCompatible fx - = all (\fx' => fx.fix == fx'.fix && fx.precedence == fx'.precedence) . map snd + = all (\fx' => fx.fix == fx'.fix + && fx.precedence == fx'.precedence + && fx.bindingInfo == fx'.bindingInfo) . map snd -- Emits a warning using the fixity that we picked and the list of all conflicting fixities warnConflict : (picked : Name) -> (conflicts : List (Name, FixityInfo)) -> Core () @@ -157,18 +169,77 @@ checkConflictingFixities isPrefix exprFC opn For example: %hide \{show fxName} """ -toTokList : {auto s : Ref Syn SyntaxInfo} -> - {auto c : Ref Ctxt Defs} -> - PTerm -> Core (List (Tok OpStr PTerm)) -toTokList (POp fc opFC opn l r) - = do precInfo <- checkConflictingFixities False fc opn - rtoks <- toTokList r - pure (Expr l :: Op fc opFC opn precInfo :: rtoks) -toTokList (PPrefixOp fc opFC opn arg) - = do precInfo <- checkConflictingFixities True fc opn - rtoks <- toTokList arg - pure (Op fc opFC opn precInfo :: rtoks) -toTokList t = pure [Expr t] +checkConflictingBinding : Ref Ctxt Defs => + Ref Syn SyntaxInfo => + FC -> Name -> (foundFixity : BacktickOrOperatorFixity) -> + (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 + where + isCompatible : BacktickOrOperatorFixity -> OperatorLHSInfo PTerm -> Bool + isCompatible Backticked (NoBinder lhs) = True + isCompatible Backticked _ = 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 + isCompatible (DeclaredFixity fixInfo) (BindExplicitType name type expr) + = fixInfo.bindingInfo == Autobind + + keepCompatibleBinding : BindingModifier -> (Name, GlobalDef) -> Core Bool + keepCompatibleBinding compatibleBinder (name, def) = do + fixities <- getFixityInfo (nameRoot name) + let compatible = any (\(_, fx) => fx.bindingInfo == use_site.getBinder) fixities + pure compatible + + candidates : Core (List String) + 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 + | Nothing => pure [] + ns <- currentNS <$> get Ctxt + pure (showSimilarNames ns opName nm cs) + +checkValidFixity : BindingModifier -> Fixity -> Nat -> Bool + +-- If the fixity declaration is not binding, there are no restrictions +checkValidFixity NotBinding _ _ = True + +-- If the fixity declaration is not binding, either typebind or autobind +-- the fixity can only be `infixr` with precedence `0`. We might want +-- to revisit that in the future, but as of right now we want to be +-- conservative and avoid abuse. +-- having multiple precedence levels would mean that if +-- =@ has higher precedence than -@ +-- the expression (x : a) =@ b -@ (y : List a) =@ List b +-- would be bracketed as ((x : a) =@ b) -@ (y : List a) =@ List b +-- instead of (x : a) =@ (b -@ ((y : List a) =@ List b)) +checkValidFixity _ InfixR 0 = True + +-- If it's binding but not infixr precedence 0, raise an error +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)) + 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 + -- This is because we do not parse binders on the lhs + -- and so, if we check, we will find uses of regular + -- operator when binding is expected. + (checkConflictingBinding opFC opn fixInfo l r) + rtoks <- toTokList r + pure (Expr l.getLhs :: Op fc opFC ((opn, fixInfo), Just l) precInfo :: rtoks) + toTokList (PPrefixOp fc opFC opn arg) + = do (precInfo, fixInfo) <- checkConflictingFixities True fc opn + rtoks <- toTokList arg + pure (Op fc opFC ((opn, fixInfo), Nothing) precInfo :: rtoks) + toTokList t = pure [Expr t] record BangData where constructor MkBangData @@ -308,12 +379,16 @@ mutual [apply (IVar fc (UN $ Basic "===")) [l', r'], apply (IVar fc (UN $ Basic "~=~")) [l', r']] desugarB side ps (PBracketed fc e) = desugarB side ps e - desugarB side ps (POp fc opFC op l r) - = do ts <- toTokList (POp fc opFC op l r) - desugarTree side ps !(parseOps ts) + desugarB side ps (POp fc opFC l op r) + = do ts <- toTokList side (POp fc opFC l op r) + tree <- parseOps @{interpName} @{showWithLoc} ts + unop <- desugarTree side ps (mapFst (\((x, _), y) => (x, y)) tree) + desugarB side ps unop desugarB side ps (PPrefixOp fc opFC op arg) - = do ts <- toTokList (PPrefixOp fc opFC op arg) - desugarTree side ps !(parseOps ts) + = do ts <- toTokList side (PPrefixOp fc opFC op arg) + tree <- parseOps @{interpName} @{showWithLoc} ts + unop <- desugarTree side ps (mapFst (\((x, _), y) => (x, y)) tree) + desugarB side ps unop desugarB side ps (PSectionL fc opFC op arg) = do syn <- get Syn -- It might actually be a prefix argument rather than a section @@ -322,12 +397,12 @@ mutual [] => desugarB side ps (PLam fc top Explicit (PRef fc (MN "arg" 0)) (PImplicit fc) - (POp fc opFC op (PRef fc (MN "arg" 0)) arg)) + (POp fc opFC (NoBinder (PRef fc (MN "arg" 0))) op arg)) (prec :: _) => desugarB side ps (PPrefixOp fc opFC op arg) desugarB side ps (PSectionR fc opFC arg op) = desugarB side ps (PLam fc top Explicit (PRef fc (MN "arg" 0)) (PImplicit fc) - (POp fc opFC op arg (PRef fc (MN "arg" 0)))) + (POp fc opFC (NoBinder arg) op (PRef fc (MN "arg" 0)))) desugarB side ps (PSearch fc depth) = pure $ ISearch fc depth desugarB side ps (PPrimVal fc (BI x)) = case !fromIntegerName of @@ -714,27 +789,48 @@ mutual rule' <- desugarDo side ps ns rule pure $ IRewrite fc rule' rest' + -- Replace all operator by function application desugarTree : {auto s : Ref Syn SyntaxInfo} -> {auto b : Ref Bang BangData} -> {auto c : Ref Ctxt Defs} -> {auto u : Ref UST UState} -> {auto m : Ref MD Metadata} -> {auto o : Ref ROpts REPLOpts} -> - Side -> List Name -> Tree OpStr PTerm -> Core RawImp - desugarTree side ps (Infix loc eqFC (UN $ Basic "=") l r) -- special case since '=' is special syntax + 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 + = 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 = do l' <- desugarTree side ps l r' <- desugarTree side ps r - pure (IAlternative loc FirstSuccess - [apply (IVar eqFC eqName) [l', r'], - apply (IVar eqFC heqName) [l', r']]) - desugarTree side ps (Infix loc _ (UN $ Basic "$") l r) -- special case since '$' is special syntax + pure (PApp loc l' r') + -- normal operators + desugarTree side ps (Infix loc opFC (op, Just (NoBinder lhs)) l r) = do l' <- desugarTree side ps l r' <- desugarTree side ps r - pure (IApp loc l' r') - desugarTree side ps (Infix loc opFC op l r) + pure (PApp loc (PApp loc (PRef opFC op) 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 - r' <- desugarTree side ps r - pure (IApp loc (IApp loc (IVar opFC op) l') r') + body <- desugarTree side ps r + pure $ PApp loc (PApp loc (PRef opFC op) 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') + (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') + (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" -- negation is a special case, since we can't have an operator with -- two meanings otherwise @@ -742,7 +838,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 (UN $ Basic "-", _) $ Leaf $ PPrimVal fc c) = let newFC = fromMaybe EmptyFC (mergeFC loc fc) continue = desugarTree side ps . Leaf . PPrimVal newFC in case c of @@ -756,16 +852,16 @@ mutual -- not a signed integer literal. proceed by desugaring -- and applying to `negate`. _ => do arg' <- desugarTree side ps (Leaf $ PPrimVal fc c) - pure (IApp loc (IVar opFC (UN $ Basic "negate")) arg') + pure (PApp loc (PRef opFC (UN $ Basic "negate")) arg') - desugarTree side ps (Pre loc opFC (UN $ Basic "-") arg) + desugarTree side ps (Pre loc opFC (UN $ Basic "-", _) arg) = do arg' <- desugarTree side ps arg - pure (IApp loc (IVar opFC (UN $ Basic "negate")) arg') + pure (PApp loc (PRef opFC (UN $ Basic "negate")) arg') - desugarTree side ps (Pre loc opFC op arg) + desugarTree side ps (Pre loc opFC (op, _) arg) = do arg' <- desugarTree side ps arg - pure (IApp loc (IVar opFC op) arg') - desugarTree side ps (Leaf t) = desugarB side ps t + pure (PApp loc (PRef opFC op) arg') + desugarTree side ps (Leaf t) = pure t desugarType : {auto s : Ref Syn SyntaxInfo} -> {auto c : Ref Ctxt Defs} -> @@ -1109,8 +1205,14 @@ mutual NS ns (DN str (MN ("__mk" ++ str) 0)) mkConName n = DN (show n) (MN ("__mk" ++ show n) 0) - desugarDecl ps (PFixity fc vis fix prec opName) - = do ctx <- get Ctxt + desugarDecl ps (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}`" + ]) + 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 @@ -1118,7 +1220,7 @@ mutual let updatedNS = NS (mkNestedNamespace (Just ctx.currentNS) (show fix)) (UN $ Basic $ nameRoot opName) - update Syn { fixities $= addName updatedNS (MkFixityInfo fc vis fix prec) } + update Syn { fixities $= addName updatedNS (MkFixityInfo fc 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 @@ -1230,4 +1332,5 @@ mutual {auto u : Ref UST UState} -> {auto o : Ref ROpts REPLOpts} -> Side -> List Name -> PTerm -> Core RawImp + desugar s ps tm = desugarDo s ps Nothing tm diff --git a/src/Idris/Desugar/Mutual.idr b/src/Idris/Desugar/Mutual.idr index b05449cee..c13ca8c41 100644 --- a/src/Idris/Desugar/Mutual.idr +++ b/src/Idris/Desugar/Mutual.idr @@ -29,7 +29,7 @@ getDecl AsType (PRecord fc doc vis mbtot (MkPRecord n ps _ _ _)) mkRecType : List (Name, RigCount, PiInfo PTerm, PTerm) -> PTerm mkRecType [] = PType fc mkRecType ((n, c, p, t) :: ts) = PPi fc c p (Just n) t (mkRecType ts) -getDecl AsType d@(PFixity _ _ _ _ _) = Just d +getDecl AsType d@(PFixity _ _ _ _ _ _) = Just d getDecl AsType d@(PDirective _ _) = Just d getDecl AsType d = Nothing @@ -37,7 +37,7 @@ getDecl AsDef (PClaim _ _ _ _ _) = Nothing getDecl AsDef d@(PData _ _ _ _ (MkPLater _ _ _)) = Just d getDecl AsDef (PInterface _ _ _ _ _ _ _ _ _) = Nothing getDecl AsDef d@(PRecord _ _ _ _ (MkPRecordLater _ _)) = Just d -getDecl AsDef (PFixity _ _ _ _ _) = Nothing +getDecl AsDef (PFixity _ _ _ _ _ _) = Nothing getDecl AsDef (PDirective _ _) = Nothing getDecl AsDef d = Just d diff --git a/src/Idris/Doc/Keywords.idr b/src/Idris/Doc/Keywords.idr index 65084e008..1ef73ff55 100644 --- a/src/Idris/Doc/Keywords.idr +++ b/src/Idris/Doc/Keywords.idr @@ -458,6 +458,55 @@ namespaceblock = vcat $ You can use `export` or `public export` to control whether a function declared in a namespace is available outside of it. """] +autobindDoc : Doc IdrisDocAnn +autobindDoc = """ + Autobind + + `autobind` is a modifier for operator precedence and fixity declaration. + It tells the parser that this operator behaves like a binding operator, + allowing you to give a name to the left-hand-side of the operator and + use it on the right-hand-side. + + `autobind` differs from `typebind` in the syntax it allows and the way + it desugars. Delcaring an operator as `autobind infixr 0 =|>` allows + you to use it with the syntax `(x := e) =|> f x`, `(x : t := e) =|> f x`. + + + You will need to use `autobind` instead of `typebind` whenever the + type of the lambda of the function called by the operator has a type + that is not equal to the argument given on the left side of the operator. + + `autobind` only applies to `infixr` operators and cannot be used as + operator sections. + + `autobind` operators are desugared as a lambda: + `(x := expr) =|> fn x` -> `(expr =|> (\x : ? => fn x))` + `(x : ty := expr) =|> fn x` -> `(expr =|> (\x : ty => fn x))` + """ +typebindDoc : Doc IdrisDocAnn +typebindDoc = """ + Typebind + + `typebind` is a modifier for operator precedence and fixity declaration. + It tells the parser that this operator behaves like a binding operator, + allowing you to give a name to the left-hand-side of the operator and + use it on the right-hand-side. + + A typical example of a typebind operator is `(**)` the type constructor + for dependent pairs. It is used like this: `(x : Nat) ** Vect x String` + + If you declare a new operator to be typebind you can use it the same + way. + + Start by defining `typebind infixr 0 =@`, and then you can use it + like so: `(n : Nat) =@ f n` + + `typebind` only applies to `infixr` operators and cannot be used as + operator sections. + + `typebind` operators are desugared as a lambda: + `(x : ty) =@ fn x` -> `ty =@ (\x : ty =@ fn x)` + """ rewriteeq : Doc IdrisDocAnn rewriteeq = vcat $ @@ -487,8 +536,7 @@ withabstraction = vcat $ If we additionally need to remember that the link between the patterns and the intermediate computation we can use the `proof` keyword to retain an equality proof. - """, "", - """ + In the following example we want to implement a `filter` function that not only returns values that satisfy the input predicate but also proofs that they do. The `with (p x)` construct introduces a value of type `Bool` @@ -564,6 +612,8 @@ keywordsDoc = :: "else" ::= ifthenelse :: "forall" ::= forallquantifier :: "rewrite" ::= rewriteeq + :: "typebind" ::= autobindDoc + :: "autobind" ::= autobindDoc :: "using" ::= "" :: "interface" ::= interfacemechanism :: "implementation" ::= interfacemechanism diff --git a/src/Idris/Error.idr b/src/Idris/Error.idr index 5289d466d..f26c6dc49 100644 --- a/src/Idris/Error.idr +++ b/src/Idris/Error.idr @@ -110,6 +110,7 @@ Eq Error where BadRunElab fc1 rho1 s1 d1 == BadRunElab fc2 rho2 s2 d2 = fc1 == fc2 && d1 == d2 RunElabFail e1 == RunElabFail e2 = e1 == e2 GenericMsg fc1 x1 == GenericMsg fc2 x2 = fc1 == fc2 && x1 == x2 + GenericMsgSol fc1 x1 y1 == GenericMsgSol fc2 x2 y2 = fc1 == fc2 && x1 == x2 && y1 == y2 TTCError x1 == TTCError x2 = x1 == x2 FileErr x1 y1 == FileErr x2 y2 = x1 == x2 && y1 == y2 CantFindPackage x1 == CantFindPackage x2 = x1 == x2 @@ -619,6 +620,89 @@ perrorRaw (BadRunElab fc env script desc) perrorRaw (RunElabFail e) = pure $ reflow "Error during reflection" <+> colon <++> !(perrorRaw e) perrorRaw (GenericMsg fc str) = pure $ pretty0 str <+> line <+> !(ploc fc) +perrorRaw (GenericMsgSol fc header solutions) + = pure $ pretty0 header <+> line <+> !(ploc fc) + <+> line + <+> "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 + <++> "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 + <++> "expr'." + <+> line <+> line + <+> "Possible solutions:" <+> line + <+> indent 1 (vsep (map ("-" <++>) + (expressionDiagnositc ++ [fixityDiagnostic, moduleDiagnostic] ++ spellingCandidates))) + where + spellingCandidates : List (Doc IdrisAnn) + spellingCandidates = case candidates of + [] => [] + [x] => ["Did you mean" <++> enclose "'" "'" (pretty0 x) <++> "?"] + xs => ["Did you mean either of:" <++> hcat (punctuate ", " + (map (enclose "'" "'" . pretty0) xs)) <++> "?"] + + + 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." + infixOpName : Doc IdrisAnn + infixOpName = case expected of + Backticked => enclose "`" "`" (byShow opName) + _ => byShow opName + + displayFixityInfo : FixityInfo -> BindingModifier -> Doc IdrisAnn + displayFixityInfo (MkFixityInfo fc1 vis _ fix precedence) NotBinding + = byShow vis <++> byShow fix <++> byShow precedence <++> pretty0 opName + displayFixityInfo (MkFixityInfo _ vis _ fix precedence) usedBinder + = byShow vis <++> byShow usedBinder <++> byShow fix <++> byShow precedence <++> pretty0 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 + + + fixityDiagnostic : Doc IdrisAnn + fixityDiagnostic = case expected of + Backticked => "Define a new fixity:" <++> "infixr 0" <++> infixOpName + (DeclaredFixity fix) => + "Change the fixity defined at" <++> pretty0 fix.fc <++> "to" + <++> enclose "'" "'" (displayFixityInfo fix actual.getBinder) + <+> dot + + printBindingModifier : BindingModifier -> Doc IdrisAnn + printBindingModifier NotBinding = "a regular" + printBindingModifier Typebind = "a type-binding (typebind)" + printBindingModifier Autobind = "an automatically-binding (autobind)" + + printBindingInfo : BacktickOrOperatorFixity -> Doc IdrisAnn + printBindingInfo Backticked = "a regular" + printBindingInfo (DeclaredFixity x) = printBindingModifier x.bindingInfo + + perrorRaw (TTCError msg) = pure $ errorDesc (reflow "Error in TTC file" <+> colon <++> byShow msg) <++> parens "the most likely case is that the ./build directory in your current project contains files from a previous build of idris2 or the idris2 executable is from a different build than the installed .ttc files" diff --git a/src/Idris/Parser.idr b/src/Idris/Parser.idr index 545da2e70..e8910f52f 100644 --- a/src/Idris/Parser.idr +++ b/src/Idris/Parser.idr @@ -105,14 +105,14 @@ pnoeq = { eqOK := False } export pdef : ParseOpts -pdef = MkParseOpts True True +pdef = MkParseOpts {eqOK = True, withOK = True} pnowith : ParseOpts -pnowith = MkParseOpts True False +pnowith = MkParseOpts {eqOK = True, withOK = False} export plhs : ParseOpts -plhs = MkParseOpts False False +plhs = MkParseOpts {eqOK = False, withOK = False} %hide Prelude.(>>) %hide Prelude.(>>=) @@ -325,15 +325,51 @@ mutual decoratedSymbol fname "]" pure (map (\ n => (boundToFC fname n, n.val)) $ forget ns) - opExpr : ParseOpts -> OriginDesc -> IndentInfo -> Rule PTerm - opExpr q fname indents + -- The different kinds of operator bindings `x : ty` for typebind + -- x := e and x : ty := e for autobind + opBinderTypes : OriginDesc -> IndentInfo -> WithBounds PTerm -> Rule (OperatorLHSInfo PTerm) + opBinderTypes fname indents boundName = + do decoratedSymbol fname ":" + ty <- typeExpr pdef fname indents + decoratedSymbol fname ":=" + exp <- expr pdef fname indents + pure (BindExplicitType boundName.val ty exp) + <|> do decoratedSymbol fname ":=" + exp <- expr pdef fname indents + pure (BindExpr boundName.val exp) + <|> do decoratedSymbol fname ":" + ty <- typeExpr pdef fname indents + pure (BindType boundName.val ty) + + opBinder : OriginDesc -> IndentInfo -> Rule (OperatorLHSInfo PTerm) + opBinder fname indents + = do boundName <- bounds (expr plhs fname indents) + opBinderTypes fname indents boundName + + autobindOp : ParseOpts -> OriginDesc -> IndentInfo -> Rule PTerm + autobindOp q fname indents + = do binder <- bounds $ parens fname (opBinder fname indents) + continue indents + op <- bounds iOperator + commit + e <- bounds (expr q fname indents) + pure (POp (boundToFC fname $ mergeBounds binder e) + (boundToFC fname op) + binder.val + op.val + e.val) + + opExprBase : ParseOpts -> OriginDesc -> IndentInfo -> Rule PTerm + opExprBase q fname indents = do l <- bounds (appExpr q fname indents) (if eqOK q - then do r <- bounds (continue indents *> decoratedSymbol fname "=" *> opExpr q fname indents) + then do r <- bounds (continue indents + *> decoratedSymbol fname "=" + *> opExprBase q fname indents) pure $ let fc = boundToFC fname (mergeBounds l r) opFC = virtualiseFC fc -- already been highlighted: we don't care - in POp fc opFC (UN $ Basic "=") l.val r.val + in POp fc opFC (NoBinder l.val) (UN $ Basic "=") r.val else fail "= not allowed") <|> (do b <- bounds $ do @@ -346,9 +382,13 @@ mutual (op, r) <- pure b.val let fc = boundToFC fname (mergeBounds l b) let opFC = boundToFC fname op - pure (POp fc opFC op.val l.val r)) + pure (POp fc opFC (NoBinder l.val) op.val r)) <|> pure l.val + opExpr : ParseOpts -> OriginDesc -> IndentInfo -> Rule PTerm + opExpr q fname indents = autobindOp q fname indents + <|> opExprBase q fname indents + dpairType : OriginDesc -> WithBounds t -> IndentInfo -> Rule PTerm dpairType fname start indents = do loc <- bounds (do x <- UN . Basic <$> decoratedSimpleBinderName fname @@ -654,8 +694,11 @@ mutual binderName = Basic <$> unqualifiedName <|> symbol "_" $> Underscore + PiBindList : Type + PiBindList = List (RigCount, WithBounds (Maybe Name), PTerm) + pibindList : OriginDesc -> IndentInfo -> - Rule (List (RigCount, WithBounds (Maybe Name), PTerm)) + Rule PiBindList pibindList fname indents = do params <- pibindListName fname indents pure $ map (\(rig, n, ty) => (rig, map Just n, ty)) params @@ -981,6 +1024,7 @@ mutual <|> defaultImplicitPi fname indents <|> forall_ fname indents <|> implicitPi fname indents + <|> autobindOp pdef fname indents <|> explicitPi fname indents <|> lam fname indents @@ -1825,16 +1869,23 @@ definition fname indents = do nd <- bounds (clause 0 Nothing fname indents) pure (PDef (boundToFC fname nd) [nd.val]) +operatorBindingKeyword : OriginDesc -> EmptyRule BindingModifier +operatorBindingKeyword fname + = (decoratedKeyword fname "autobind" >> pure Autobind) + <|> (decoratedKeyword fname "typebind" >> pure Typebind) + <|> pure NotBinding + fixDecl : OriginDesc -> IndentInfo -> Rule (List PDecl) fixDecl fname indents = do vis <- exportVisibility fname + binding <- operatorBindingKeyword fname b <- bounds (do fixity <- decorate fname Keyword $ fix commit prec <- decorate fname Keyword $ intLit ops <- sepBy1 (decoratedSymbol fname ",") iOperator pure (fixity, prec, ops)) (fixity, prec, ops) <- pure b.val - pure (map (PFixity (boundToFC fname b) vis fixity (fromInteger prec)) (forget ops)) + pure (map (PFixity (boundToFC fname b) vis binding fixity (fromInteger prec)) (forget ops)) directiveDecl : OriginDesc -> IndentInfo -> Rule PDecl directiveDecl fname indents diff --git a/src/Idris/Pretty.idr b/src/Idris/Pretty.idr index 6c4cffa8f..34f0eb421 100644 --- a/src/Idris/Pretty.idr +++ b/src/Idris/Pretty.idr @@ -332,7 +332,19 @@ mutual prettyPrec d (PDotted _ p) = dot <+> prettyPrec d p prettyPrec d (PImplicit _) = "_" prettyPrec d (PInfer _) = annotate Hole $ "?" - prettyPrec d (POp _ _ op x y) = + prettyPrec d (POp _ _ (BindType nm left) op right) = + group $ parens (prettyPrec d nm <++> ":" <++> pretty left) + <++> prettyOp op + <++> pretty right + prettyPrec d (POp _ _ (BindExpr nm left) op right) = + group $ parens (prettyPrec d nm <++> ":=" <++> pretty left) + <++> prettyOp op + <++> pretty right + prettyPrec d (POp _ _ (BindExplicitType nm ty left) op right) = + group $ parens (prettyPrec d nm <++> ":" <++> pretty ty <++> ":=" <++> pretty left) + <++> prettyOp op + <++> pretty right + prettyPrec d (POp _ _ (NoBinder x) op y) = parenthesise (d >= App) $ group $ pretty x <++> prettyOp op diff --git a/src/Idris/Resugar.idr b/src/Idris/Resugar.idr index 47b02b54b..2f0607ba0 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 kn (unbracketApp x) (unbracketApp y) + let asOp = POp fc opFC (NoBinder (unbracketApp x)) kn (unbracketApp y) if not (null (lookupName rootName (infixes syn))) then pure asOp else case dropNS raw of @@ -590,8 +590,8 @@ cleanPTerm ptm cleanNode : IPTerm -> Core IPTerm cleanNode (PRef fc nm) = PRef fc <$> cleanKindedName nm - cleanNode (POp fc opFC op x y) = - (\ op => POp fc opFC op x y) <$> cleanKindedName op + cleanNode (POp fc opFC abi op y) = + (\ op => POp fc opFC abi op y) <$> cleanKindedName op cleanNode (PPrefixOp fc opFC op x) = (\ op => PPrefixOp fc opFC op x) <$> cleanKindedName op cleanNode (PSectionL fc opFC op x) = diff --git a/src/Idris/Syntax.idr b/src/Idris/Syntax.idr index ed365477c..56bd1b7c4 100644 --- a/src/Idris/Syntax.idr +++ b/src/Idris/Syntax.idr @@ -29,44 +29,6 @@ import Parser.Lexer.Source %default covering -public export -data Fixity = InfixL | InfixR | Infix | Prefix - -export -Show Fixity where - show InfixL = "infixl" - show InfixR = "infixr" - show Infix = "infix" - show Prefix = "prefix" - -export -Eq Fixity where - InfixL == InfixL = True - InfixR == InfixR = True - Infix == Infix = True - Prefix == Prefix = True - _ == _ = False - --- A record to hold all the information about a fixity -public export -record FixityInfo where - constructor MkFixityInfo - fc : FC - vis : Visibility - fix : Fixity - precedence : Nat - -export -Show FixityInfo where - show fx = "fc: \{show fx.fc}, visibility: \{show fx.vis}, fixity: \{show fx.fix}, precedence: \{show fx.precedence}" - -export -Eq FixityInfo where - x == y = x.fc == y.fc - && x.vis == y.vis - && x.fix == y.fix - && x.precedence == y.precedence - public export OpStr' : Type -> Type OpStr' nm = nm @@ -136,7 +98,9 @@ mutual -- Operators - POp : (full, opFC : FC) -> OpStr' nm -> PTerm' nm -> PTerm' nm -> PTerm' nm + POp : (full, opFC : FC) -> + (lhsInfo : OperatorLHSInfo (PTerm' nm)) -> + OpStr' nm -> (rhs : PTerm' nm) -> PTerm' nm PPrefixOp : (full, opFC : FC) -> OpStr' nm -> PTerm' nm -> PTerm' nm PSectionL : (full, opFC : FC) -> OpStr' nm -> PTerm' nm -> PTerm' nm PSectionR : (full, opFC : FC) -> PTerm' nm -> OpStr' nm -> PTerm' nm @@ -470,7 +434,7 @@ mutual PFail : FC -> Maybe String -> List (PDecl' nm) -> PDecl' nm PMutual : FC -> List (PDecl' nm) -> PDecl' nm - PFixity : FC -> Visibility -> Fixity -> Nat -> OpStr -> PDecl' nm + PFixity : FC -> Visibility -> 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 @@ -489,7 +453,7 @@ mutual getPDeclLoc (PRecord fc _ _ _ _) = fc getPDeclLoc (PMutual fc _) = fc getPDeclLoc (PFail fc _ _) = fc - getPDeclLoc (PFixity fc _ _ _ _) = fc + getPDeclLoc (PFixity fc _ _ _ _ _) = fc getPDeclLoc (PNamespace fc _ _) = fc getPDeclLoc (PTransform fc _ _ _) = fc getPDeclLoc (PRunElabDecl fc _) = fc @@ -806,7 +770,14 @@ parameters {0 nm : Type} (toName : nm -> Name) showPTermPrec d (PDotted _ p) = "." ++ showPTermPrec d p showPTermPrec _ (PImplicit _) = "_" showPTermPrec _ (PInfer _) = "?" - showPTermPrec d (POp _ _ op x y) = showPTermPrec d x ++ " " ++ showOpPrec d op ++ " " ++ showPTermPrec d y + showPTermPrec d (POp _ _ (NoBinder left) op right) + = showPTermPrec d left ++ " " ++ showOpPrec d op ++ " " ++ showPTermPrec d right + showPTermPrec d (POp _ _ (BindType nm left) op right) + = "(" ++ showPTermPrec d nm ++ " : " ++ showPTermPrec d left ++ " " ++ showOpPrec d op ++ " " ++ showPTermPrec d right ++ ")" + showPTermPrec d (POp _ _ (BindExpr nm left) op right) + = "(" ++ showPTermPrec d nm ++ " := " ++ showPTermPrec d left ++ " " ++ showOpPrec d op ++ " " ++ showPTermPrec d right ++ ")" + showPTermPrec d (POp _ _ (BindExplicitType nm ty left) op right) + = "(" ++ showPTermPrec d nm ++ " : " ++ showPTermPrec d ty ++ ":=" ++ showPTermPrec d left ++ " " ++ showOpPrec d op ++ " " ++ showPTermPrec d right ++ ")" showPTermPrec d (PPrefixOp _ _ op x) = showOpPrec d op ++ showPTermPrec d x showPTermPrec d (PSectionL _ _ op x) = "(" ++ showOpPrec d op ++ " " ++ showPTermPrec d x ++ ")" showPTermPrec d (PSectionR _ _ x op) = "(" ++ showPTermPrec d x ++ " " ++ showOpPrec d op ++ ")" @@ -999,9 +970,9 @@ initSyntax initFixities : ANameMap FixityInfo initFixities = fromList - [ (UN $ Basic "-", MkFixityInfo EmptyFC Export Prefix 10) - , (UN $ Basic "negate", MkFixityInfo EmptyFC Export Prefix 10) -- for documentation purposes - , (UN $ Basic "=", MkFixityInfo EmptyFC Export Infix 0) + [ (UN $ Basic "-", MkFixityInfo EmptyFC Export NotBinding Prefix 10) + , (UN $ Basic "negate", MkFixityInfo EmptyFC Export NotBinding Prefix 10) -- for documentation purposes + , (UN $ Basic "=", MkFixityInfo EmptyFC Export NotBinding Infix 0) ] initDocStrings : ANameMap String @@ -1034,6 +1005,13 @@ removeFixity : {auto s : Ref Syn SyntaxInfo} -> Fixity -> Name -> Core () removeFixity _ key = update Syn ({fixities $= removeExact key }) +||| Return all fixity declarations for an operator name +export +getFixityInfo : {auto s : Ref Syn SyntaxInfo} -> String -> Core (List (Name, FixityInfo)) +getFixityInfo nm = do + syn <- get Syn + pure $ lookupName (UN $ Basic nm) (fixities syn) + export covering Show PTypeDecl where diff --git a/src/Idris/Syntax/TTC.idr b/src/Idris/Syntax/TTC.idr index 0ae8a2af3..a8b144d27 100644 --- a/src/Idris/Syntax/TTC.idr +++ b/src/Idris/Syntax/TTC.idr @@ -81,19 +81,33 @@ TTC Import where nameAs <- fromBuf b pure (MkImport loc reexport path nameAs) +export +TTC BindingModifier where + toBuf b NotBinding = tag 0 + toBuf b Typebind = tag 1 + toBuf b Autobind = tag 2 + fromBuf b + = case !getTag of + 0 => pure NotBinding + 1 => pure Typebind + 2 => pure Autobind + _ => corrupt "binding" + export TTC FixityInfo where toBuf b fx = do toBuf b fx.fc toBuf b fx.vis + toBuf b fx.bindingInfo toBuf b fx.fix toBuf b fx.precedence fromBuf b = do fc <- fromBuf b vis <- fromBuf b + binding <- fromBuf b fix <- fromBuf b prec <- fromBuf b - pure $ MkFixityInfo fc vis fix prec + pure $ MkFixityInfo fc vis binding fix prec export diff --git a/src/Idris/Syntax/Traversals.idr b/src/Idris/Syntax/Traversals.idr index 9db5d8fa2..f44230973 100644 --- a/src/Idris/Syntax/Traversals.idr +++ b/src/Idris/Syntax/Traversals.idr @@ -99,9 +99,29 @@ mapPTermM f = goPTerm where >>= f goPTerm t@(PImplicit _) = f t goPTerm t@(PInfer _) = f t - goPTerm (POp fc opFC x y z) = - POp fc opFC x <$> goPTerm y - <*> goPTerm z + goPTerm (POp fc opFC (NoBinder left) op right) = + POp fc opFC + <$> (NoBinder <$> goPTerm left) + <*> pure op + <*> goPTerm right + >>= f + goPTerm (POp fc opFC (BindType nm left) op right) = + POp fc opFC + <$> (BindType <$> goPTerm nm <*> goPTerm left) + <*> pure op + <*> goPTerm right + >>= f + goPTerm (POp fc opFC (BindExpr nm left) op right) = + POp fc opFC + <$> (BindExpr nm <$> goPTerm left) + <*> pure op + <*> goPTerm right + >>= f + goPTerm (POp fc opFC (BindExplicitType nm ty left) op right) = + POp fc opFC + <$> (BindExplicitType <$> goPTerm nm <*> goPTerm ty <*> goPTerm left) + <*> pure op + <*> goPTerm right >>= f goPTerm (PPrefixOp fc opFC x y) = PPrefixOp fc opFC x <$> goPTerm y @@ -265,7 +285,7 @@ mapPTermM f = goPTerm where pure $ PRecord fc doc v tot (MkPRecordLater n !(go4TupledPTerms nts)) goPDecl (PFail fc msg ps) = PFail fc msg <$> goPDecls ps goPDecl (PMutual fc ps) = PMutual fc <$> goPDecls ps - goPDecl p@(PFixity _ _ _ _ _) = pure p + goPDecl p@(PFixity _ _ _ _ _ _) = pure p goPDecl (PNamespace fc strs ps) = PNamespace fc strs <$> goPDecls ps goPDecl (PTransform fc n a b) = PTransform fc n <$> goPTerm a <*> goPTerm b goPDecl (PRunElabDecl fc a) = PRunElabDecl fc <$> goPTerm a @@ -434,8 +454,8 @@ mapPTerm f = goPTerm where = f $ PDotted fc $ goPTerm x goPTerm t@(PImplicit _) = f t goPTerm t@(PInfer _) = f t - goPTerm (POp fc opFC x y z) - = f $ POp fc opFC x (goPTerm y) (goPTerm z) + goPTerm (POp fc opFC autoBindInfo opName z) + = f $ POp fc opFC (map f autoBindInfo) opName (goPTerm z) goPTerm (PPrefixOp fc opFC x y) = f $ PPrefixOp fc opFC x $ goPTerm y goPTerm (PSectionL fc opFC x y) @@ -533,7 +553,7 @@ mapPTerm f = goPTerm where = PRecord fc doc v tot (MkPRecordLater n (go4TupledPTerms nts)) goPDecl (PFail fc msg ps) = PFail fc msg $ goPDecl <$> ps goPDecl (PMutual fc ps) = PMutual fc $ goPDecl <$> ps - goPDecl p@(PFixity _ _ _ _ _) = p + goPDecl p@(PFixity _ _ _ _ _ _) = p goPDecl (PNamespace fc strs ps) = PNamespace fc strs $ goPDecl <$> ps goPDecl (PTransform fc n a b) = PTransform fc n (goPTerm a) (goPTerm b) goPDecl (PRunElabDecl fc a) = PRunElabDecl fc $ goPTerm a @@ -618,7 +638,7 @@ substFC fc = mapPTerm $ \case PDotted _ x => PDotted fc x PImplicit _ => PImplicit fc PInfer _ => PInfer fc - POp _ _ x y z => POp fc fc x y z + POp _ _ ab nm r => POp fc fc ab nm r PPrefixOp _ _ x y => PPrefixOp fc fc x y PSectionL _ _ x y => PSectionL fc fc x y PSectionR _ _ x y => PSectionR fc fc x y diff --git a/src/Idris/Syntax/Views.idr b/src/Idris/Syntax/Views.idr index d9984aeaf..34e9de748 100644 --- a/src/Idris/Syntax/Views.idr +++ b/src/Idris/Syntax/Views.idr @@ -26,7 +26,8 @@ getFnArgs embed fts = go fts [] where go (PAutoApp fc f t) = go f . (Auto fc t ::) go (PNamedApp fc f n t) = go f . (Named fc n t ::) go (PBracketed fc f) = go f - go (POp fc opFC op l r) = (PRef opFC op,) . (Explicit fc l ::) . (Explicit fc r ::) + -- 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 (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/Utils/Shunting.idr b/src/Libraries/Utils/Shunting.idr index 424893cc1..9413daecf 100644 --- a/src/Libraries/Utils/Shunting.idr +++ b/src/Libraries/Utils/Shunting.idr @@ -22,10 +22,9 @@ data OpPrec -- Tokens are either operators or already parsed expressions in some -- higher level language public export -data Tok op a - = ||| The second FC is for the operator alone - Op FC FC op OpPrec - | Expr a +data Tok : (op, a : Type) -> Type where + Op : (expressionLoc : FC) -> (operatorLoc : FC) -> (operatorInfo : op) -> OpPrec -> Tok op a + Expr : a -> Tok op a -- The result of shunting is a parse tree with the precedences made explicit -- in the tree. @@ -41,6 +40,12 @@ data Tree op a = Infix FC FC op (Tree op a) (Tree op a) | Pre FC FC op (Tree op a) | Leaf a +public export +Bifunctor Tree where + bimap f g (Infix fc fc1 x y z) = Infix fc fc1 (f x) (bimap f g y) (bimap f g z) + bimap f g (Pre fc fc1 x y) = Pre fc fc1 (f x) (bimap f g y) + bimap f g (Leaf x) = Leaf (g x) + export (Show op, Show a) => Show (Tree op a) where show (Infix _ _ op l r) = "(" ++ show op ++ " " ++ show l ++ " " ++ show r ++ ")" @@ -85,25 +90,27 @@ isLAssoc : OpPrec -> Bool isLAssoc (AssocL _) = True isLAssoc _ = False --- Return whether the first operator should be applied before the second, --- assuming -higher : Show op => FC -> op -> OpPrec -> op -> OpPrec -> Core Bool +-- Return whether the first operator should be applied before the second. +-- Interpolation to show the operator naked, show to print the operator with its location +higher : Interpolation op => (showLoc : Show op) => FC -> op -> OpPrec -> op -> OpPrec -> Core Bool higher loc opx op opy (Prefix p) = pure False higher loc opx (NonAssoc x) opy oy = if x == getPrec oy - then throw (GenericMsg loc ("Operator '" ++ show opx ++ - "' is non-associative")) + then throw (GenericMsgSol loc ( "Operator \{opx} is non-associative") + [ "Add brackets around every use of \{opx}" + , "Change the fixity of \{show opx} to `infixl` or `infixr`"]) else pure (x > getPrec oy) higher loc opx ox opy (NonAssoc y) = if getPrec ox == y - then throw (GenericMsg loc ("Operator '" ++ show opy ++ - "' is non-associative")) + then throw (GenericMsgSol loc ( "Operator \{opy} is non-associative") + [ "Add brackets around every use of \{opy}" + , "Change the fixity of \{show opy} to `infixl` or `infixr`"]) else pure (getPrec ox > y) higher loc opl l opr r = pure $ (getPrec l > getPrec r) || ((getPrec l == getPrec r) && isLAssoc l) -processStack : Show op => {auto o : Ref Out (List (Tree op a))} -> +processStack : Interpolation op => (showLoc : Show op) => {auto o : Ref Out (List (Tree op a))} -> List (FC, FC, op, OpPrec) -> op -> OpPrec -> Core (List (FC, FC, op, OpPrec)) processStack [] op prec = pure [] @@ -113,7 +120,7 @@ processStack (x@(loc, opFC, opx, sprec) :: xs) opy prec processStack xs opy prec else pure (x :: xs) -shunt : Show op => {auto o : Ref Out (List (Tree op a))} -> +shunt : Interpolation op => (showLoc : Show op) => {auto o : Ref Out (List (Tree op a))} -> (opstk : List (FC, FC, op, OpPrec)) -> List (Tok op a) -> Core (Tree op a) shunt stk (Expr x :: rest) @@ -132,7 +139,7 @@ shunt stk [] mkOp (loc, opFC, op, prec) = Op loc opFC op prec export -parseOps : Show op => List (Tok op a) -> Core (Tree op a) +parseOps : Interpolation op => (showLoc : Show op) => List (Tok op a) -> Core (Tree op a) parseOps toks = do o <- newRef {t = List (Tree op a)} Out [] shunt [] toks diff --git a/src/Parser/Lexer/Source.idr b/src/Parser/Lexer/Source.idr index bc4c3d60c..b3acb22f0 100644 --- a/src/Parser/Lexer/Source.idr +++ b/src/Parser/Lexer/Source.idr @@ -245,7 +245,7 @@ keywords : List String keywords = ["data", "module", "where", "let", "in", "do", "record", "auto", "default", "implicit", "failing", "mutual", "namespace", "parameters", "with", "proof", "impossible", "case", "of", - "if", "then", "else", "forall", "rewrite", + "if", "then", "else", "forall", "rewrite", "typebind", "autobind", "using", "interface", "implementation", "open", "import", "public", "export", "private"] ++ fixityKeywords ++ diff --git a/tests/Main.idr b/tests/Main.idr index 0ee17265e..52016ca93 100644 --- a/tests/Main.idr +++ b/tests/Main.idr @@ -112,6 +112,9 @@ idrisTestsReflection = testsInDir "idris2/reflection" "Quotation and Reflection" idrisTestsWith : IO TestPool idrisTestsWith = testsInDir "idris2/with" "With abstraction" +idrisTestsOperators : IO TestPool +idrisTestsOperators = testsInDir "idris2/operators" "Operator and fixities" + idrisTestsIPKG : IO TestPool idrisTestsIPKG = testsInDir "idris2/pkg" "Package and .ipkg files" @@ -216,6 +219,7 @@ main = runner $ , !idrisTestsSchemeEval , !idrisTestsReflection , !idrisTestsWith + , !idrisTestsOperators , !idrisTestsDebug , !idrisTestsIPKG , testPaths "idris2/misc" idrisTests diff --git a/tests/idris2/interactive/interactive028/expected b/tests/idris2/interactive/interactive028/expected index 529623d7f..6b78dac3e 100644 --- a/tests/idris2/interactive/interactive028/expected +++ b/tests/idris2/interactive/interactive028/expected @@ -4,7 +4,7 @@ Main> Couldn't parse any alternatives: (Interactive):1:4--1:5 1 | :t (3 : Nat) ^ -... (54 others) +... (56 others) Main> Expected string begin. (Interactive):1:5--1:7 diff --git a/tests/idris2/operators/operators001/Test.idr b/tests/idris2/operators/operators001/Test.idr new file mode 100644 index 000000000..c33218298 --- /dev/null +++ b/tests/idris2/operators/operators001/Test.idr @@ -0,0 +1,80 @@ + +module Test + +import Data.Vect + +typebind infixr 0 =@ +infixr 0 -@ + +-- typebind infixr 1 =@@ + +0 (=@) : (a : Type) -> (a -> Type) -> Type +(=@) a f = (1 x : a) -> f x + +0 (=@@) : (a : Type) -> (a -> Type) -> Type +(=@@) a f = (1 x : a) -> f x + +(-@) : (a, b : Type) -> Type +(-@) a b = (1 _ : a) -> b + +data S : {ty : Type} -> (x : ty) -> Type where + MkS : (x : ty) =@ S x + Mk2 : (x : ty) =@ (y : ty) =@ S (x, y) + Mk3 : (x : ty) =@ ty -@ S x + Mk4 : ty -@ (x : ty) =@ S x + +-- map : (x : a) =@@ b -@ (y : List a) =@ List b + +map2 : ((x : a) =@ b) -@ (y : List a) =@ List b + +map3 : (x : a) =@ b -@ (y : List a) =@ List b + +map4 : (x : a) =@ (b -@ (y : List a) =@ List b) + +-- this could be possible if we allowed binding operators +-- with higher precedences +-- test : Test.map === Test.map2 +-- failing +-- test2 : Test.map === Test.map3 + +test3 : Test.map3 === Test.map4 + +typebind infixr 0 *> + +-- (*>) : (ty : Type) -> (ty -> Type) -> Type +-- (*>) = DPair +-- +-- testCompose : (x : Nat) *> (y : Nat) *> Vect (n + m) String +-- testCompose = (1 ** 2 ** ["hello", "world", "!"]) + +autobind infixr 0 `MyLet` + +MyLet : (val) -> (val -> rest) -> rest +MyLet arg fn = fn arg + +program : Nat +program = (n := 3) `MyLet` 2 + n + +program2 : Nat +program2 = (n : Nat := 3) `MyLet` 2 + n + +typebind infixr 0 |> + +record Container where + constructor (|>) + shape : Type + position : shape -> Type + +typebind infixr 0 @@ + +record (@@) (x : Type) (y : x -> Type) where + constructor PairUp + fst : x + snd : y fst + +compose : Container -> Container -> Container +compose (a |> a') (b |> b') = + (x : (y : a) @@ (a' y -> b)) |> + (y : a' x.fst) @@ + b' (x.snd y) + diff --git a/tests/idris2/operators/operators001/expected b/tests/idris2/operators/operators001/expected new file mode 100644 index 000000000..31e5db7f3 --- /dev/null +++ b/tests/idris2/operators/operators001/expected @@ -0,0 +1 @@ +1/1: Building Test (Test.idr) diff --git a/tests/idris2/operators/operators001/run b/tests/idris2/operators/operators001/run new file mode 100755 index 000000000..d35387bb3 --- /dev/null +++ b/tests/idris2/operators/operators001/run @@ -0,0 +1,3 @@ +. ../../../testutils.sh + +check Test.idr diff --git a/tests/idris2/operators/operators002/Error2.idr b/tests/idris2/operators/operators002/Error2.idr new file mode 100644 index 000000000..e3b6a420d --- /dev/null +++ b/tests/idris2/operators/operators002/Error2.idr @@ -0,0 +1,12 @@ + +typebind infixr 0 =@ + +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 + +wrongId : {0 a : Type} -> a =@ a +wrongId x = x diff --git a/tests/idris2/operators/operators002/Errors.idr b/tests/idris2/operators/operators002/Errors.idr new file mode 100644 index 000000000..4ee059bf5 --- /dev/null +++ b/tests/idris2/operators/operators002/Errors.idr @@ -0,0 +1,9 @@ + +typebind infixr 0 =@ + +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/Errors2.idr b/tests/idris2/operators/operators002/Errors2.idr new file mode 100644 index 000000000..f7b6e7b22 --- /dev/null +++ b/tests/idris2/operators/operators002/Errors2.idr @@ -0,0 +1,8 @@ + +autobind infixr 0 =@ + +0 (=@) : (a : Type) -> (a -> Type) -> Type +(=@) a f = (1 x : a) -> f x + +wrongId : {0 a : Type} -> a =@ a +wrongId x = x diff --git a/tests/idris2/operators/operators002/Errors3.idr b/tests/idris2/operators/operators002/Errors3.idr new file mode 100644 index 000000000..0e8994ec5 --- /dev/null +++ b/tests/idris2/operators/operators002/Errors3.idr @@ -0,0 +1,8 @@ + +typebind infixr 0 =@ + +0 (=@) : (a : Type) -> (a -> Type) -> Type +(=@) a f = (1 x : a) -> f x + +wrongId : {0 a : Type} -> a =@ a +wrongId x = x diff --git a/tests/idris2/operators/operators002/Errors4.idr b/tests/idris2/operators/operators002/Errors4.idr new file mode 100644 index 000000000..d6a52f928 --- /dev/null +++ b/tests/idris2/operators/operators002/Errors4.idr @@ -0,0 +1,9 @@ + +infixr 0 =@ + +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/Errors5.idr b/tests/idris2/operators/operators002/Errors5.idr new file mode 100644 index 000000000..fd7225832 --- /dev/null +++ b/tests/idris2/operators/operators002/Errors5.idr @@ -0,0 +1,10 @@ + + +infixr 0 =@ + +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 new file mode 100644 index 000000000..b50c78f4c --- /dev/null +++ b/tests/idris2/operators/operators002/Test.idr @@ -0,0 +1,38 @@ + + +import Data.Vect + +typebind infixr 0 =@ +infixr 0 -@ + +0 (=@) : (a : Type) -> (a -> Type) -> Type +(=@) a f = (1 x : a) -> f x + +(-@) : (a, b : Type) -> Type +(-@) a b = (1 _ : a) -> b + +data S : {ty : Type} -> (x : ty) -> Type where + MkS : (x : ty) =@ S x + Mk2 : (x : ty) =@ (y : ty) =@ S (x, y) + Mk3 : (x : ty) =@ ty -@ S x + Mk4 : ty -@ (x : ty) =@ S x + Chain : (x : ty =@ y : ty =@ S (x, y)) + +typebind infixr 0 *> + +-- (*>) : (ty : Type) -> (ty -> Type) -> Type +-- (*>) = DPair +-- +-- testCompose : (x : Nat) *> (y : Nat) *> Vect (n + m) String +-- testCompose = (1 ** 2 ** ["hello", "world", "!"]) + +autobind infixr 7 `MyLet` + +MyLet : (val) -> (val -> rest) -> rest +MyLet arg fn = fn arg + +program : Nat +program = (n := 3) `MyLet` 2 + n + +program2 : Nat +program2 = (n : Nat := 3) `MyLet` 2 + n diff --git a/tests/idris2/operators/operators002/expected b/tests/idris2/operators/operators002/expected new file mode 100644 index 000000000..8451e1d0b --- /dev/null +++ b/tests/idris2/operators/operators002/expected @@ -0,0 +1,80 @@ +1/1: Building Errors (Errors.idr) +Error: Operator =@ is a type-binding (typebind) operator, but is used as an automatically-binding (autobind) operator. + +Errors: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 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. +1/1: Building Errors2 (Errors2.idr) +Error: Operator =@ is an automatically-binding (autobind) operator, but is used as a regular operator. + +Errors2:7:29--7:31 + 3 | + 4 | 0 (=@) : (a : Type) -> (a -> Type) -> Type + 5 | (=@) a f = (1 x : a) -> f x + 6 | + 7 | wrongId : {0 a : Type} -> a =@ a + ^^ +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 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. +1/1: Building Errors3 (Errors3.idr) +Error: Operator =@ is a type-binding (typebind) operator, but is used as a regular operator. + +Errors3:7:29--7:31 + 3 | + 4 | 0 (=@) : (a : Type) -> (a -> Type) -> Type + 5 | (=@) a f = (1 x : a) -> f x + 6 | + 7 | wrongId : {0 a : Type} -> a =@ a + ^^ +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: '(_ : 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. +1/1: Building Errors4 (Errors4.idr) +Error: Operator =@ is a regular operator, but is used as a type-binding (typebind) operator. + +Errors4:9:18--9:20 + 5 | (=@) a f = (1 x : a) -> f x + 6 | + 7 | + 8 | data S : {ty : Type} -> (x : ty) -> Type where + 9 | 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 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. +1/1: Building Errors5 (Errors5.idr) +Error: Operator =@ is a regular operator, but is used as an automatically-binding (autobind) operator. + +Errors5:10:19--10:21 + 06 | (=@) a f = (1 x : a) -> f x + 07 | + 08 | + 09 | data S : {ty : Type} -> (x : ty) -> Type where + 10 | 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 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. diff --git a/tests/idris2/operators/operators002/run b/tests/idris2/operators/operators002/run new file mode 100755 index 000000000..13baec981 --- /dev/null +++ b/tests/idris2/operators/operators002/run @@ -0,0 +1,8 @@ +. ../../../testutils.sh + +check Errors.idr +check Errors2.idr +check Errors3.idr +check Errors4.idr +check Errors5.idr + diff --git a/tests/idris2/operators/operators003/Error1.idr b/tests/idris2/operators/operators003/Error1.idr new file mode 100644 index 000000000..8860d8899 --- /dev/null +++ b/tests/idris2/operators/operators003/Error1.idr @@ -0,0 +1,3 @@ +module Error1 + +typebind infixl 0 =@ diff --git a/tests/idris2/operators/operators003/Error2.idr b/tests/idris2/operators/operators003/Error2.idr new file mode 100644 index 000000000..de22cfe71 --- /dev/null +++ b/tests/idris2/operators/operators003/Error2.idr @@ -0,0 +1,3 @@ +module Error2 + +typebind infixr 3 =@ diff --git a/tests/idris2/operators/operators003/Error3.idr b/tests/idris2/operators/operators003/Error3.idr new file mode 100644 index 000000000..f91d022ab --- /dev/null +++ b/tests/idris2/operators/operators003/Error3.idr @@ -0,0 +1,3 @@ +module Error3 + +typebind infixl 3 =@ diff --git a/tests/idris2/operators/operators003/expected b/tests/idris2/operators/operators003/expected new file mode 100644 index 000000000..1b262ce82 --- /dev/null +++ b/tests/idris2/operators/operators003/expected @@ -0,0 +1,36 @@ +1/1: Building Error1 (Error1.idr) +Error: Invalid fixity, typebind operator must be infixr 0. + +Error1:3:10--3:21 + 1 | module Error1 + 2 | + 3 | typebind infixl 0 =@ + ^^^^^^^^^^^ + +Possible solutions: + - Make it `infixr 0`: `typebind infixr 0 =@` + - Remove the binding keyword: `infixl 0 =@` +1/1: Building Error2 (Error2.idr) +Error: Invalid fixity, typebind operator must be infixr 0. + +Error2:3:10--3:21 + 1 | module Error2 + 2 | + 3 | typebind infixr 3 =@ + ^^^^^^^^^^^ + +Possible solutions: + - Make it `infixr 0`: `typebind infixr 0 =@` + - Remove the binding keyword: `infixr 3 =@` +1/1: Building Error3 (Error3.idr) +Error: Invalid fixity, typebind operator must be infixr 0. + +Error3:3:10--3:21 + 1 | module Error3 + 2 | + 3 | typebind infixl 3 =@ + ^^^^^^^^^^^ + +Possible solutions: + - Make it `infixr 0`: `typebind infixr 0 =@` + - Remove the binding keyword: `infixl 3 =@` diff --git a/tests/idris2/operators/operators003/run b/tests/idris2/operators/operators003/run new file mode 100755 index 000000000..e87f60f6f --- /dev/null +++ b/tests/idris2/operators/operators003/run @@ -0,0 +1,5 @@ +. ../../../testutils.sh + +check Error1.idr +check Error2.idr +check Error3.idr diff --git a/tests/idris2/operators/operators004/Test.idr b/tests/idris2/operators/operators004/Test.idr new file mode 100644 index 000000000..25093fc0e --- /dev/null +++ b/tests/idris2/operators/operators004/Test.idr @@ -0,0 +1,16 @@ + +infix 5 -:- + +infix 5 :-: + +(-:-) : a -> List a -> List a +(-:-) = (::) + +(:-:) : a -> List a -> List a +(:-:) = (::) + +test : List Nat +test = 4 -:- 3 :-: [] + +test2 : List Nat +test2 = 4 :-: 3 -:- [] diff --git a/tests/idris2/operators/operators004/expected b/tests/idris2/operators/operators004/expected new file mode 100644 index 000000000..f976037ea --- /dev/null +++ b/tests/idris2/operators/operators004/expected @@ -0,0 +1,27 @@ +1/1: Building Test (Test.idr) +Error: Operator -:- is non-associative + +Test:13:8--13:22 + 09 | (:-:) : a -> List a -> List a + 10 | (:-:) = (::) + 11 | + 12 | test : List Nat + 13 | test = 4 -:- 3 :-: [] + ^^^^^^^^^^^^^^ + +Possible solutions: + - Add brackets around every use of -:- + - Change the fixity of -:- at Test:2:1--2:12 to `infixl` or `infixr` +Error: Operator :-: is non-associative + +Test:16:9--16:23 + 12 | test : List Nat + 13 | test = 4 -:- 3 :-: [] + 14 | + 15 | test2 : List Nat + 16 | test2 = 4 :-: 3 -:- [] + ^^^^^^^^^^^^^^ + +Possible solutions: + - Add brackets around every use of :-: + - Change the fixity of :-: at Test:4:1--4:12 to `infixl` or `infixr` diff --git a/tests/idris2/operators/operators004/run b/tests/idris2/operators/operators004/run new file mode 100755 index 000000000..d35387bb3 --- /dev/null +++ b/tests/idris2/operators/operators004/run @@ -0,0 +1,3 @@ +. ../../../testutils.sh + +check Test.idr diff --git a/tests/idris2/operators/operators005/Test.idr b/tests/idris2/operators/operators005/Test.idr new file mode 100644 index 000000000..a96b27435 --- /dev/null +++ b/tests/idris2/operators/operators005/Test.idr @@ -0,0 +1,19 @@ + +import Data.String + +typebind infixr 0 :- +autobind infixr 0 `for` + +record Container where + constructor (:-) + a1 : Type + a2 : a1 -> Type + +const : Type -> Type -> Container +const a b = (_ : a) :- b + +test : Maybe (List Double) +test = (_ := ["1", "two", "3"]) `for` Just 3 + +test2 : Maybe (List Double) +test2 = (_ : String := ["1", "two", "3"]) `for` Just 3 diff --git a/tests/idris2/operators/operators005/expected b/tests/idris2/operators/operators005/expected new file mode 100644 index 000000000..31e5db7f3 --- /dev/null +++ b/tests/idris2/operators/operators005/expected @@ -0,0 +1 @@ +1/1: Building Test (Test.idr) diff --git a/tests/idris2/operators/operators005/run b/tests/idris2/operators/operators005/run new file mode 100755 index 000000000..d35387bb3 --- /dev/null +++ b/tests/idris2/operators/operators005/run @@ -0,0 +1,3 @@ +. ../../../testutils.sh + +check Test.idr diff --git a/tests/idris2/operators/operators006/Test.idr b/tests/idris2/operators/operators006/Test.idr new file mode 100644 index 000000000..b9aa1639c --- /dev/null +++ b/tests/idris2/operators/operators006/Test.idr @@ -0,0 +1,10 @@ + +import Data.Fin + +autobind infixr 0 `bind` + +bind : Monad m => m a -> (a -> m b) -> m b +bind = (>>=) + +both : Maybe (Nat, Nat) -> Maybe Nat +both m = (MkPair x y := m) `bind` Just (x + y) diff --git a/tests/idris2/operators/operators006/expected b/tests/idris2/operators/operators006/expected new file mode 100644 index 000000000..31e5db7f3 --- /dev/null +++ b/tests/idris2/operators/operators006/expected @@ -0,0 +1 @@ +1/1: Building Test (Test.idr) diff --git a/tests/idris2/operators/operators006/run b/tests/idris2/operators/operators006/run new file mode 100755 index 000000000..d35387bb3 --- /dev/null +++ b/tests/idris2/operators/operators006/run @@ -0,0 +1,3 @@ +. ../../../testutils.sh + +check Test.idr diff --git a/tests/idris2/operators/operators007/Test.idr b/tests/idris2/operators/operators007/Test.idr new file mode 100644 index 000000000..b15090ce2 --- /dev/null +++ b/tests/idris2/operators/operators007/Test.idr @@ -0,0 +1,10 @@ + +import Data.Fin + +autobind infixr 0 >> + +(>>) : Monad m => m a -> (a -> m b) -> m b +(>>) = (>>=) + +both : Maybe (Nat, Nat) -> Maybe Nat +both m = (MkPair x y := m) >>= Just (x + y) diff --git a/tests/idris2/operators/operators007/Test2.idr b/tests/idris2/operators/operators007/Test2.idr new file mode 100644 index 000000000..021923a00 --- /dev/null +++ b/tests/idris2/operators/operators007/Test2.idr @@ -0,0 +1,14 @@ + +import Data.Fin + +autobind infixr 0 >> +autobind infixr 0 >= + +(>>) : Monad m => m a -> (a -> m b) -> m b +(>>) = (>>=) + +(>=) : Monad m => m a -> (a -> m b) -> m b +(>=) = (>>=) + +both : Maybe (Nat, Nat) -> Maybe Nat +both m = (MkPair x y := m) >>= Just (x + y) diff --git a/tests/idris2/operators/operators007/expected b/tests/idris2/operators/operators007/expected new file mode 100644 index 000000000..8644014d4 --- /dev/null +++ b/tests/idris2/operators/operators007/expected @@ -0,0 +1,34 @@ +1/1: Building Test (Test.idr) +Error: Operator >>= is a regular operator, but is used as an automatically-binding (autobind) operator. + +Test:10:28--10:31 + 06 | (>>) : Monad m => m a -> (a -> m b) -> m b + 07 | (>>) = (>>=) + 08 | + 09 | both : Maybe (Nat, Nat) -> Maybe Nat + 10 | both m = (MkPair x y := m) >>= Just (x + y) + ^^^ +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 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. + - Did you mean '>>' ? +1/1: Building Test2 (Test2.idr) +Error: Operator >>= is a regular operator, but is used as an automatically-binding (autobind) operator. + +Test2:14:28--14:31 + 10 | (>=) : Monad m => m a -> (a -> m b) -> m b + 11 | (>=) = (>>=) + 12 | + 13 | both : Maybe (Nat, Nat) -> Maybe Nat + 14 | both m = (MkPair x y := m) >>= Just (x + y) + ^^^ +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 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. + - Did you mean either of: '>=', '>>' ? diff --git a/tests/idris2/operators/operators007/run b/tests/idris2/operators/operators007/run new file mode 100755 index 000000000..09019ff63 --- /dev/null +++ b/tests/idris2/operators/operators007/run @@ -0,0 +1,5 @@ +. ../../../testutils.sh + +check Test.idr + +check Test2.idr diff --git a/tests/idris2/operators/operators008/Test.idr b/tests/idris2/operators/operators008/Test.idr new file mode 100644 index 000000000..328dfb3c2 --- /dev/null +++ b/tests/idris2/operators/operators008/Test.idr @@ -0,0 +1,13 @@ +module Test + +import Test2 + +%hide Test2.infixr.(@>) + +infixl 9 @> + +(@>) : a -> b -> (a, b) +(@>) = MkPair + +test : 3 @> 2 @> 1 === (3 @> 2) @> 1 +test = Refl diff --git a/tests/idris2/operators/operators008/Test2.idr b/tests/idris2/operators/operators008/Test2.idr new file mode 100644 index 000000000..d85ce2bcf --- /dev/null +++ b/tests/idris2/operators/operators008/Test2.idr @@ -0,0 +1,4 @@ +module Test2 + +export autobind infixr 0 @> + diff --git a/tests/idris2/operators/operators008/expected b/tests/idris2/operators/operators008/expected new file mode 100644 index 000000000..84943dbde --- /dev/null +++ b/tests/idris2/operators/operators008/expected @@ -0,0 +1,2 @@ +1/2: Building Test2 (Test2.idr) +2/2: Building Test (Test.idr) diff --git a/tests/idris2/operators/operators008/run b/tests/idris2/operators/operators008/run new file mode 100755 index 000000000..d35387bb3 --- /dev/null +++ b/tests/idris2/operators/operators008/run @@ -0,0 +1,3 @@ +. ../../../testutils.sh + +check Test.idr