Skip to content

Commit

Permalink
Emit warning for fixities with no export modifiers
Browse files Browse the repository at this point in the history 
This is to help update all the existing code to program with explicit
fixity export directives in preparation for the behavioral change where
they will become private by default.
  • Loading branch information
@andrevidela
andrevidela committed Mar 15, 2024
1 parent c3239cb commit 16bea7b
Show file tree
Hide file tree
Showing 59 changed files with 242 additions and 180 deletions.
14 changes: 10 additions & 4 deletions src/Core/Context.idr
View file
Original file line number Diff line number Diff line change
Expand Up @@ -821,9 +821,12 @@ HasNames Error where
full gam (InRHS fc n err) = InRHS fc <$> full gam n <*> full gam err
full gam (MaybeMisspelling err xs) = MaybeMisspelling <$> full gam err <*> pure xs
full gam (WarningAsError wrn) = WarningAsError <$> full gam wrn
full gam (OperatorBindingMismatch {print} fc expected actual opName rhs candidates)
full gam (OperatorBindingMismatch {print} fc expected actual (Left opName) rhs candidates)
= OperatorBindingMismatch {print} fc expected actual
<$> full gam opName <*> pure rhs <*> pure candidates
<$> (Left <$> full gam opName) <*> pure rhs <*> pure candidates
full gam (OperatorBindingMismatch {print} fc expected actual (Right opName) rhs candidates)
= OperatorBindingMismatch {print} fc expected actual
<$> (Right <$> full gam opName) <*> pure rhs <*> pure candidates

resolved gam (Fatal err) = Fatal <$> resolved gam err
resolved _ (CantConvert fc gam rho s t)
Expand Down Expand Up @@ -916,9 +919,12 @@ HasNames Error where
resolved gam (InRHS fc n err) = InRHS fc <$> resolved gam n <*> resolved gam err
resolved gam (MaybeMisspelling err xs) = MaybeMisspelling <$> resolved gam err <*> pure xs
resolved gam (WarningAsError wrn) = WarningAsError <$> resolved gam wrn
resolved gam (OperatorBindingMismatch {print} fc expected actual opName rhs candidates)
resolved gam (OperatorBindingMismatch {print} fc expected actual (Left opName) rhs candidates)
= OperatorBindingMismatch {print} fc expected actual
<$> (Left <$> resolved gam opName) <*> pure rhs <*> pure candidates
resolved gam (OperatorBindingMismatch {print} fc expected actual (Right opName) rhs candidates)
= OperatorBindingMismatch {print} fc expected actual
<$> resolved gam opName <*> pure rhs <*> pure candidates
<$> (Right <$> resolved gam opName) <*> pure rhs <*> pure candidates

export
HasNames Totality where
Expand Down
7 changes: 4 additions & 3 deletions src/Core/Core.idr
View file
Original file line number Diff line number Diff line change
Expand Up @@ -165,8 +165,9 @@ data Error : Type where
GenericMsg : FC -> String -> Error
GenericMsgSol : FC -> (message : String) -> (solutions : List String) -> Error
OperatorBindingMismatch : {a : Type} -> {print : a -> Doc ()} ->
FC -> (expectedFixity : BacktickOrOperatorFixity) -> (use_site : OperatorLHSInfo a) ->
(opName : Name) -> (rhs : a) -> (candidates : List String) -> Error
FC -> (expectedFixity : FixityDeclarationInfo) -> (use_site : OperatorLHSInfo a) ->
-- left: backticked, right: op symbolds
(opName : Either Name Name) -> (rhs : a) -> (candidates : List String) -> Error
TTCError : TTCErrorMsg -> Error
FileErr : String -> FileError -> Error
CantFindPackage : String -> Error
Expand Down Expand Up @@ -403,7 +404,7 @@ Show Error where
show (OperatorBindingMismatch fc (DeclaredFixity expected) actual opName rhs _)
= show fc ++ ": Operator " ++ show opName ++ " is " ++ show expected
++ " but used as a " ++ show actual ++ " operator"
show (OperatorBindingMismatch fc Backticked actual opName rhs _)
show (OperatorBindingMismatch fc UndeclaredFixity actual opName rhs _)
= show fc ++ ": Operator " ++ show opName ++ " has no declared fixity"
++ " but used as a " ++ show actual ++ " operator"

Expand Down
4 changes: 2 additions & 2 deletions src/Core/TT.idr
View file
Original file line number Diff line number Diff line change
Expand Up @@ -170,11 +170,11 @@ Eq FixityInfo where

||| Whenever we read an operator from the parser, we don't know if it's a backticked expression with no fixity
||| declaration, or if it has a fixity declaration. If it does not have a declaration, we represent this state
||| with `Backticked`.
||| with `UndeclaredFixity`.
||| Note that a backticked expression can have a fixity declaration, in which case it is represented with
||| `DeclaredFixity`.
public export
data BacktickOrOperatorFixity = Backticked | DeclaredFixity FixityInfo
data FixityDeclarationInfo = UndeclaredFixity | DeclaredFixity FixityInfo

-- Left-hand-side information for operators, carries autobind information
-- an operator can either be
Expand Down
86 changes: 53 additions & 33 deletions src/Idris/Desugar.idr
View file
Original file line number Diff line number Diff line change
Expand Up @@ -35,6 +35,7 @@ import TTImp.TTImp
import TTImp.Utils

import Libraries.Data.IMaybe
import Libraries.Data.WithDefault
import Libraries.Utils.Shunting
import Libraries.Text.PrettyPrint.Prettyprinter

Expand Down Expand Up @@ -106,12 +107,12 @@ mkPrec Infix = NonAssoc
mkPrec Prefix = Prefix

-- This is used to print the error message for fixities
[interpName] Interpolation ((Name, BacktickOrOperatorFixity), b) where
interpolate ((x, _), _) = show x
[interpName] Interpolation ((OpStr' Name, FixityDeclarationInfo), b) where
interpolate ((x, _), _) = show x.toName

[showWithLoc] Show ((Name, BacktickOrOperatorFixity), b) where
[showWithLoc] Show ((OpStr' Name, FixityDeclarationInfo), b) where
show ((x, DeclaredFixity y), _) = show x ++ " at " ++ show y.fc
show ((x, Backticked), _) = show x
show ((x, UndeclaredFixity), _) = show x

-- Check that an operator does not have any conflicting fixities in scope.
-- Each operator can have its fixity defined multiple times across multiple
Expand All @@ -121,19 +122,19 @@ mkPrec Prefix = Prefix
checkConflictingFixities : {auto s : Ref Syn SyntaxInfo} ->
{auto c : Ref Ctxt Defs} ->
(isPrefix : Bool) ->
FC -> Name -> Core (OpPrec, BacktickOrOperatorFixity)
FC -> OpStr' Name -> Core (OpPrec, FixityDeclarationInfo)
checkConflictingFixities isPrefix exprFC opn
= do let op = nameRoot opn
= do let op = nameRoot opn.toName
foundFixities <- getFixityInfo op
let (pre, inf) = partition ((== Prefix) . fix . snd) foundFixities
case (isPrefix, pre, inf) of
-- If we do not find any fixity for this operator we check that it uses operator
-- characters, if not, it must be a backticked expression.
(_, [], []) => if any isOpChar (fastUnpack op)
then throw (GenericMsg exprFC "Unknown operator '\{op}'")
else pure (NonAssoc 1, Backticked) -- Backticks are non associative by default
-- If we do not find any fixity, and it is a backticked operator, then we
-- return the default fixity and associativity for backticked operators
-- Otherwise, it's an unknown operator.
(_, [], []) => case opn of
OpSymbols _ => throw (GenericMsg exprFC "Unknown operator '\{op}'")
Backticked _ => pure (NonAssoc 1, UndeclaredFixity) -- Backticks are non associative by default

--
(True, ((fxName, fx) :: _), _) => do
-- in the prefix case, remove conflicts with infix (-)
let extraFixities = pre ++ (filter (\(nm, _) => not $ nameRoot nm == "-") inf)
Expand Down Expand Up @@ -171,17 +172,18 @@ checkConflictingFixities isPrefix exprFC opn

checkConflictingBinding : Ref Ctxt Defs =>
Ref Syn SyntaxInfo =>
FC -> Name -> (foundFixity : BacktickOrOperatorFixity) ->
FC -> OpStr -> (foundFixity : FixityDeclarationInfo) ->
(usage : OperatorLHSInfo PTerm) -> (rhs : PTerm) -> Core ()
checkConflictingBinding fc opName foundFixity use_site rhs
= if isCompatible foundFixity use_site
then pure ()
else throw $ OperatorBindingMismatch
{print = byShow} fc foundFixity use_site opName rhs !candidates
{print = byShow} fc foundFixity use_site (opNameToEither opName) rhs !candidates
where
isCompatible : BacktickOrOperatorFixity -> OperatorLHSInfo PTerm -> Bool
isCompatible Backticked (NoBinder lhs) = True
isCompatible Backticked _ = False

isCompatible : FixityDeclarationInfo -> OperatorLHSInfo PTerm -> Bool
isCompatible UndeclaredFixity (NoBinder lhs) = True
isCompatible UndeclaredFixity _ = False
isCompatible (DeclaredFixity fixInfo) (NoBinder lhs) = fixInfo.bindingInfo == NotBinding
isCompatible (DeclaredFixity fixInfo) (BindType name ty) = fixInfo.bindingInfo == Typebind
isCompatible (DeclaredFixity fixInfo) (BindExpr name expr) = fixInfo.bindingInfo == Autobind
Expand All @@ -198,10 +200,10 @@ checkConflictingBinding fc opName foundFixity use_site rhs
candidates = do let DeclaredFixity fxInfo = foundFixity
| _ => pure [] -- if there is no declared fixity we can't know what's
-- supposed to go there.
Just (nm, cs) <- getSimilarNames {keepPredicate = Just (keepCompatibleBinding fxInfo.bindingInfo)} opName
Just (nm, cs) <- getSimilarNames {keepPredicate = Just (keepCompatibleBinding fxInfo.bindingInfo)} opName.toName
| Nothing => pure []
ns <- currentNS <$> get Ctxt
pure (showSimilarNames ns opName nm cs)
pure (showSimilarNames ns opName.toName nm cs)

checkValidFixity : BindingModifier -> Fixity -> Nat -> Bool

Expand All @@ -225,7 +227,7 @@ checkValidFixity _ _ _ = False
parameters (side : Side)
toTokList : {auto s : Ref Syn SyntaxInfo} ->
{auto c : Ref Ctxt Defs} ->
PTerm -> Core (List (Tok ((OpStr, BacktickOrOperatorFixity), Maybe (OperatorLHSInfo PTerm)) PTerm))
PTerm -> Core (List (Tok ((OpStr, FixityDeclarationInfo), Maybe (OperatorLHSInfo PTerm)) PTerm))
toTokList (POp fc opFC l opn r)
= do (precInfo, fixInfo) <- checkConflictingFixities False fc opn
unless (side == LHS) -- do not check for conflicting fixity on the LHS
Expand Down Expand Up @@ -393,7 +395,7 @@ mutual
= do syn <- get Syn
-- It might actually be a prefix argument rather than a section
-- so check that first, otherwise desugar as a lambda
case lookupName op (prefixes syn) of
case lookupName op.toName (prefixes syn) of
[] =>
desugarB side ps
(PLam fc top Explicit (PRef fc (MN "arg" 0)) (PImplicit fc)
Expand Down Expand Up @@ -798,36 +800,36 @@ mutual
{auto o : Ref ROpts REPLOpts} ->
Side -> List Name -> Tree (OpStr, Maybe $ OperatorLHSInfo PTerm) PTerm ->
Core PTerm
desugarTree side ps (Infix loc eqFC (UN $ Basic "=", _) l r) -- special case since '=' is special syntax
desugarTree side ps (Infix loc eqFC (OpSymbols $ UN $ Basic "=", _) l r) -- special case since '=' is special syntax
= pure $ PEq eqFC !(desugarTree side ps l) !(desugarTree side ps r)

desugarTree side ps (Infix loc _ (UN $ Basic "$", _) l r) -- special case since '$' is special syntax
desugarTree side ps (Infix loc _ (OpSymbols $ UN $ Basic "$", _) l r) -- special case since '$' is special syntax
= do l' <- desugarTree side ps l
r' <- desugarTree side ps r
pure (PApp loc l' r')
-- 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 (PApp loc (PApp loc (PRef opFC op) l') r')
pure (PApp loc (PApp loc (PRef opFC op.toName) l') r')
-- (x : ty) =@ f x ==>> (=@) ty (\x : ty => f x)
desugarTree side ps (Infix loc opFC (op, Just (BindType pat lhs)) l r)
= do l' <- desugarTree side ps l
body <- desugarTree side ps r
pure $ PApp loc (PApp loc (PRef opFC op) l')
pure $ PApp loc (PApp loc (PRef opFC op.toName) l')
(PLam loc top Explicit pat l' body)
-- (x := exp) =@ f x ==>> (=@) exp (\x : ? => f x)
desugarTree side ps (Infix loc opFC (op, Just (BindExpr pat lhs)) l r)
= do l' <- desugarTree side ps l
body <- desugarTree side ps r
pure $ PApp loc (PApp loc (PRef opFC op) l')
pure $ PApp loc (PApp loc (PRef opFC op.toName) l')
(PLam loc top Explicit pat (PInfer opFC) body)

-- (x : ty := exp) =@ f x ==>> (=@) exp (\x : ty => f x)
desugarTree side ps (Infix loc opFC (op, Just (BindExplicitType pat ty expr)) l r)
= do l' <- desugarTree side ps l
body <- desugarTree side ps r
pure $ PApp loc (PApp loc (PRef opFC op) l')
pure $ PApp loc (PApp loc (PRef opFC op.toName) l')
(PLam loc top Explicit pat ty body)
desugarTree side ps (Infix loc opFC (op, Nothing) _ r)
= throw $ InternalError "illegal fixity: Parsed as infix but no binding information"
Expand All @@ -838,7 +840,7 @@ mutual
-- Note: In case of negated signed integer literals, we apply the
-- negation directly. Otherwise, the literal might be
-- truncated to 0 before being passed on to `negate`.
desugarTree side ps (Pre loc opFC (UN $ Basic "-", _) $ Leaf $ PPrimVal fc c)
desugarTree side ps (Pre loc opFC (OpSymbols $ UN $ Basic "-", _) $ Leaf $ PPrimVal fc c)
= let newFC = fromMaybe EmptyFC (mergeFC loc fc)
continue = desugarTree side ps . Leaf . PPrimVal newFC
in case c of
Expand All @@ -854,13 +856,13 @@ mutual
_ => do arg' <- desugarTree side ps (Leaf $ PPrimVal fc c)
pure (PApp loc (PRef opFC (UN $ Basic "negate")) arg')

desugarTree side ps (Pre loc opFC (UN $ Basic "-", _) arg)
desugarTree side ps (Pre loc opFC (OpSymbols $ UN $ Basic "-", _) arg)
= do arg' <- desugarTree side ps arg
pure (PApp loc (PRef opFC (UN $ Basic "negate")) arg')

desugarTree side ps (Pre loc opFC (op, _) arg)
= do arg' <- desugarTree side ps arg
pure (PApp loc (PRef opFC op) arg')
pure (PApp loc (PRef opFC op.toName) arg')
desugarTree side ps (Leaf t) = pure t

desugarType : {auto s : Ref Syn SyntaxInfo} ->
Expand Down Expand Up @@ -1016,6 +1018,11 @@ mutual
List Name -> PiInfo PTerm -> Core (PiInfo RawImp)
mapDesugarPiInfo ps = PiInfo.traverse (desugar AnyExpr ps)

displayFixity : Maybe Visibility -> BindingModifier -> Fixity -> Nat -> OpStr -> String
displayFixity Nothing NotBinding fix prec op = "\{show fix} \{show prec} \{show op}"
displayFixity Nothing bind fix prec op = "\{show bind} \{show fix} \{show prec} \{show op}"
displayFixity (Just vis) bind fix prec op = "\{show vis} \{show bind} \{show fix} \{show prec} \{show op}"

-- Given a high level declaration, return a list of TTImp declarations
-- which process it, and update any necessary state on the way.
export
Expand Down Expand Up @@ -1205,22 +1212,35 @@ mutual
NS ns (DN str (MN ("__mk" ++ str) 0))
mkConName n = DN (show n) (MN ("__mk" ++ show n) 0)

desugarDecl ps (PFixity fc vis binding fix prec opName)
desugarDecl ps fx@(PFixity fc vis binding fix prec opName)
= do unless (checkValidFixity binding fix prec)
(throw $ GenericMsgSol fc
"Invalid fixity, \{binding} operator must be infixr 0."
[ "Make it `infixr 0`: `\{binding} infixr 0 \{show opName}`"
, "Remove the binding keyword: `\{fix} \{show prec} \{show opName}`"
])
when (isDefaulted vis) $
let adjustedExport = displayFixity (Just Export) binding fix prec opName
adjustedPrivate = displayFixity (Just Private) binding fix prec opName
originalFixity = displayFixity Nothing binding fix prec opName
in recordWarning $ GenericWarn fc """
Fixity declaration '\{originalFixity}' does not have an export modifier, and
will become private by default in a future version.
To expose it outside of its module, write '\{adjustedExport}'. If you
intend to keep it private, write '\{adjustedPrivate}'.
"""
ctx <- get Ctxt
-- We update the context of fixities by adding a namespaced fixity
-- given by the current namespace and its fixity name.
-- This allows fixities to be stored along with the namespace at their
-- declaration site and detect and handle ambiguous fixities
let updatedNS = NS (mkNestedNamespace (Just ctx.currentNS) (show fix))
(UN $ Basic $ nameRoot opName)
(UN $ Basic $ nameRoot opName.toName)

update Syn { fixities $= addName updatedNS (MkFixityInfo fc vis binding fix prec) }
update Syn
{ fixities $=
addName updatedNS
(MkFixityInfo fc (collapseDefault vis) binding fix prec) }
pure []
desugarDecl ps d@(PFail fc mmsg ds)
= do -- save the state: the content of a failing block should be discarded
Expand Down
Loading

0 comments on commit 16bea7b

Please sign in to comment.