diff --git a/src/Core/TT.idr b/src/Core/TT.idr index 621d9067f44..e368b80b1f6 100644 --- a/src/Core/TT.idr +++ b/src/Core/TT.idr @@ -201,18 +201,18 @@ data FixityDeclarationInfo = UndeclaredFixity | DeclaredFixity FixityInfo -- - 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)` +-- `(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)` +-- `(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 + -- (nm <- exp) =@ fn nm BindExpr : (name : tm) -> (expr : tm) -> OperatorLHSInfo tm - -- (nm : ty := exp) =@ fn nm + -- (nm : ty <- exp) =@ fn nm BindExplicitType : (name : tm) -> (type, expr : tm) -> OperatorLHSInfo tm export diff --git a/src/Idris/Desugar.idr b/src/Idris/Desugar.idr index 367901015da..a6405ff8a0a 100644 --- a/src/Idris/Desugar.idr +++ b/src/Idris/Desugar.idr @@ -116,6 +116,35 @@ mkPrec Prefix = Prefix show ((x, DeclaredFixity y), _) = show x ++ " at " ++ show y.fc show ((x, UndeclaredFixity), _) = show x +checkConflictingBinding : Ref Ctxt Defs => + Ref Syn SyntaxInfo => + WithFC OpStr -> (foundFixity : FixityInfo) -> + (usage : OperatorLHSInfo PTerm) -> (rhs : PTerm) -> Core () +checkConflictingBinding opName foundFixity use_site rhs + = if isCompatible foundFixity use_site + then pure () + else throw $ OperatorBindingMismatch + {print = byShow} opName.fc (DeclaredFixity foundFixity) use_site (opNameToEither opName.val) rhs !candidates + where + + isCompatible : FixityInfo -> OperatorLHSInfo PTerm -> Bool + isCompatible fixInfo (NoBinder lhs) = fixInfo.bindingInfo == NotBinding + isCompatible fixInfo (BindType name ty) = fixInfo.bindingInfo == Typebind + isCompatible fixInfo (BindExpr name expr) = fixInfo.bindingInfo == Autobind + isCompatible 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 Just (nm, cs) <- getSimilarNames {keepPredicate = Just (keepCompatibleBinding foundFixity.bindingInfo)} opName.val.toName + | Nothing => pure [] + ns <- currentNS <$> get Ctxt + pure (showSimilarNames ns opName.val.toName nm cs) + -- 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 @@ -123,36 +152,40 @@ mkPrec Prefix = Prefix -- Once conflicts are handled we return the operator precedence we found. checkConflictingFixities : {auto s : Ref Syn SyntaxInfo} -> {auto c : Ref Ctxt Defs} -> - (isPrefix : Bool) -> + (side : Side) -> + (usageType : Maybe (OperatorLHSInfo PTerm, PTerm)) -> -- `Nothing` for prefix WithFC (OpStr' Name) -> Core (OpPrec, FixityDeclarationInfo) -checkConflictingFixities isPrefix opn +checkConflictingFixities side usageType opn = do let op = nameRoot opn.val.toName - foundFixities <- getFixityInfo op - let (pre, inf) = partition ((== Prefix) . fix . snd) foundFixities - case (isPrefix, pre, inf) of - -- 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.val of - OpSymbols _ => throw (GenericMsg opn.fc "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) - unless (isCompatible fx extraFixities) $ warnConflict fxName extraFixities - 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 opn.fc $ "'\{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, DeclaredFixity fx) - -- Could not find any infix operator fixities, there may be prefix ones - (False, _, []) => throw (GenericMsg opn.fc $ "'\{op}' is not an infix operator") + foundFixities@(_::_) <- getFixityInfo op + | [] => do + -- 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.val of + OpSymbols _ => throw (GenericMsg opn.fc "Unknown operator '\{op}'") + Backticked _ => pure (NonAssoc 1, UndeclaredFixity) -- Backticks are non associative by default + + let (opType, f) : (String, _) = case usageType of + Nothing => ("a prefix", (== Prefix) . fix) + Just (b, _) => do + let b = b.getBinder + ("a \{show b} infix", \op => op.fix /= Prefix && (op.bindingInfo == b || side == LHS)) + let ops = filter (f . snd) foundFixities + + case ops of + [] => do + 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. + whenJust usageType $ \(l, r) => do + whenJust (head' $ filter ((/= Prefix) . fix . snd) foundFixities) $ \(_, fx) => + checkConflictingBinding opn fx l r + throw (GenericMsg opn.fc $ "'\{op}' is not \{opType} operator") + (fxName, fx) :: _ => do + unless (isCompatible fx ops) $ warnConflict fxName ops + pure (mkPrec fx.fix fx.precedence, DeclaredFixity fx) where -- Fixities are compatible with all others of the same name that share the same -- fixity, precedence, and binding information @@ -172,41 +205,6 @@ checkConflictingFixities isPrefix opn For example: %hide \{show fxName} """ -checkConflictingBinding : Ref Ctxt Defs => - Ref Syn SyntaxInfo => - WithFC OpStr -> (foundFixity : FixityDeclarationInfo) -> - (usage : OperatorLHSInfo PTerm) -> (rhs : PTerm) -> Core () -checkConflictingBinding opName foundFixity use_site rhs - = if isCompatible foundFixity use_site - then pure () - else throw $ OperatorBindingMismatch - {print = byShow} opName.fc foundFixity use_site (opNameToEither opName.val) rhs !candidates - where - - 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 - 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.val.toName - | Nothing => pure [] - ns <- currentNS <$> get Ctxt - pure (showSimilarNames ns opName.val.toName nm cs) - checkValidFixity : BindingModifier -> Fixity -> Nat -> Bool -- If the fixity declaration is not binding, there are no restrictions @@ -231,16 +229,11 @@ parameters (side : Side) {auto c : Ref Ctxt Defs} -> PTerm -> Core (List (Tok ((OpStr, FixityDeclarationInfo), Maybe (OperatorLHSInfo PTerm)) PTerm)) toTokList (POp fc (MkWithData _ l) opn r) - = do (precInfo, fixInfo) <- checkConflictingFixities False 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 opn fixInfo l r) + = do (precInfo, fixInfo) <- checkConflictingFixities side (Just (l, r)) opn rtoks <- toTokList r pure (Expr l.getLhs :: Op fc opn.fc ((opn.val, fixInfo), Just l) precInfo :: rtoks) toTokList (PPrefixOp fc opn arg) - = do (precInfo, fixInfo) <- checkConflictingFixities True opn + = do (precInfo, fixInfo) <- checkConflictingFixities side Nothing opn rtoks <- toTokList arg pure (Op fc opn.fc ((opn.val, fixInfo), Nothing) precInfo :: rtoks) toTokList t = pure [Expr t] diff --git a/tests/idris2/misc/namespace005/expected b/tests/idris2/misc/namespace005/expected index f9c9f68e859..7d44441b32c 100644 --- a/tests/idris2/misc/namespace005/expected +++ b/tests/idris2/misc/namespace005/expected @@ -34,21 +34,6 @@ MainFail:7:27--7:30 ^^^ 2/2: Building Main3 (Main3.idr) -Warning: operator fixity is ambiguous, we are picking Main3.prefix.(%%%) out of : - - Main3.prefix.(%%%), precedence level 4 - - Lib1.infixr.(%%%), precedence level 5 - -To remove this warning, use `%hide` with the fixity to remove -For example: %hide Main3.prefix.(%%%) - -Main3:12:29--12:32 - 08 | (%%%) : Nat -> Nat - 09 | (%%%) = S - 10 | - 11 | main : IO () - 12 | main = do printLn (the Nat (%%% 4)) - ^^^ - Warning: operator fixity is ambiguous, we are picking Prelude.Ops.infixl.(-) out of : - Prelude.Ops.infixl.(-), precedence level 8 - Main3.infixr.(-), precedence level 8 diff --git a/tests/idris2/operators/operators013/Neg.idr b/tests/idris2/operators/operators013/Neg.idr new file mode 100644 index 00000000000..3c85e1d167a --- /dev/null +++ b/tests/idris2/operators/operators013/Neg.idr @@ -0,0 +1,10 @@ +private prefix 0 *&*&*&*&*&*&*&*&* + +badRegular : Nat +badRegular = 5 *&*&*&*&*&*&*&*&* 6 + +badTypebind : Nat +badTypebind = (x : Nat) *&*&*&*&*&*&*&*&* 6 + +badAutobind : Nat +badAutobind = (x <- 5) *&*&*&*&*&*&*&*&* 6 diff --git a/tests/idris2/operators/operators013/Pos0.idr b/tests/idris2/operators/operators013/Pos0.idr new file mode 100644 index 00000000000..0f6ec28ed83 --- /dev/null +++ b/tests/idris2/operators/operators013/Pos0.idr @@ -0,0 +1,9 @@ +import Data.Vect + +export typebind infixr 0 * + +(*) : (a : Type) -> (a -> Type) -> Type +(*) = DPair + +aPair : (n : Nat) * Vect n Nat +aPair = (_ ** [1, 2, 3, 4, 5]) diff --git a/tests/idris2/operators/operators013/Pos1.idr b/tests/idris2/operators/operators013/Pos1.idr new file mode 100644 index 00000000000..65a609dcfcb --- /dev/null +++ b/tests/idris2/operators/operators013/Pos1.idr @@ -0,0 +1,19 @@ +import Data.Vect + +export typebind infixr 0 *** +export infix 1 *** + +namespace DPairType + + public export + (***) : (a : Type) -> (a -> Type) -> Type + (***) = DPair + +namespace DPairVal + + public export + (***) : {0 f : _} -> (x : a) -> f x -> (x : a) *** f x + (***) = MkDPair + +anotherPair : (a : Type) *** (n : Nat) *** Vect n a +anotherPair = Nat *** (5 *** [1, 2, 3, 4, 5]) diff --git a/tests/idris2/operators/operators013/Pos2.idr b/tests/idris2/operators/operators013/Pos2.idr new file mode 100644 index 00000000000..8a698fdca53 --- /dev/null +++ b/tests/idris2/operators/operators013/Pos2.idr @@ -0,0 +1,20 @@ +import Data.Vect + +namespace DPairType + + export typebind infixr 0 *** + + public export + (***) : (a : Type) -> (a -> Type) -> Type + (***) = DPair + +namespace DPairVal + + export infixr 0 *** + + public export + (***) : {0 f : _} -> (x : a) -> f x -> (x : a) *** f x + (***) = MkDPair + +anotherPair : (a : Type) *** (n : Nat) *** Vect n a +anotherPair = Nat *** 5 *** [1, 2, 3, 4, 5] diff --git a/tests/idris2/operators/operators013/expected b/tests/idris2/operators/operators013/expected new file mode 100644 index 00000000000..77d0ca880da --- /dev/null +++ b/tests/idris2/operators/operators013/expected @@ -0,0 +1,33 @@ +1/1: Building Pos0 (Pos0.idr) +1/1: Building Pos1 (Pos1.idr) +1/1: Building Pos2 (Pos2.idr) +1/1: Building Neg (Neg.idr) +Error: '*&*&*&*&*&*&*&*&*' is not a regular infix operator + +Neg:4:16--4:33 + 1 | private prefix 0 *&*&*&*&*&*&*&*&* + 2 | + 3 | badRegular : Nat + 4 | badRegular = 5 *&*&*&*&*&*&*&*&* 6 + ^^^^^^^^^^^^^^^^^ + +Error: '*&*&*&*&*&*&*&*&*' is not a typebind infix operator + +Neg:7:25--7:42 + 3 | badRegular : Nat + 4 | badRegular = 5 *&*&*&*&*&*&*&*&* 6 + 5 | + 6 | badTypebind : Nat + 7 | badTypebind = (x : Nat) *&*&*&*&*&*&*&*&* 6 + ^^^^^^^^^^^^^^^^^ + +Error: '*&*&*&*&*&*&*&*&*' is not a autobind infix operator + +Neg:10:24--10:41 + 06 | badTypebind : Nat + 07 | badTypebind = (x : Nat) *&*&*&*&*&*&*&*&* 6 + 08 | + 09 | badAutobind : Nat + 10 | badAutobind = (x <- 5) *&*&*&*&*&*&*&*&* 6 + ^^^^^^^^^^^^^^^^^ + diff --git a/tests/idris2/operators/operators013/run b/tests/idris2/operators/operators013/run new file mode 100755 index 00000000000..c9dd280eb20 --- /dev/null +++ b/tests/idris2/operators/operators013/run @@ -0,0 +1,6 @@ +. ../../../testutils.sh + +check Pos0.idr +check Pos1.idr +check Pos2.idr +check Neg.idr