From f67b303ccabe20933c91fc8ffe7d2f214e78daab Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Andr=C3=A9=20Videla?= Date: Sun, 16 Jun 2024 15:59:19 +0100 Subject: [PATCH 1/2] Emit error when unbound fixity is hidden --- src/Core/Context.idr | 4 +- src/Core/Core.idr | 9 ++-- src/Core/Name.idr | 26 ++++++++++++ src/Idris/Desugar.idr | 4 +- src/Idris/Error.idr | 6 +-- src/Idris/Syntax.idr | 22 ++++++++-- src/Libraries/Utils/Shunting.idr | 4 +- .../idris2/operators/operators011/Module.idr | 3 ++ tests/idris2/operators/operators011/Test.idr | 2 + tests/idris2/operators/operators011/Test1.idr | 3 ++ tests/idris2/operators/operators011/Test2.idr | 3 ++ tests/idris2/operators/operators011/Test3.idr | 3 ++ tests/idris2/operators/operators011/expected | 42 +++++++++++++++++++ tests/idris2/operators/operators011/run | 6 +++ 14 files changed, 121 insertions(+), 16 deletions(-) create mode 100644 tests/idris2/operators/operators011/Module.idr create mode 100644 tests/idris2/operators/operators011/Test.idr create mode 100644 tests/idris2/operators/operators011/Test1.idr create mode 100644 tests/idris2/operators/operators011/Test2.idr create mode 100644 tests/idris2/operators/operators011/Test3.idr create mode 100644 tests/idris2/operators/operators011/expected create mode 100755 tests/idris2/operators/operators011/run diff --git a/src/Core/Context.idr b/src/Core/Context.idr index aa1231c889..ce7256c79e 100644 --- a/src/Core/Context.idr +++ b/src/Core/Context.idr @@ -796,7 +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 (GenericMsgSol fc x y z) = pure (GenericMsgSol fc x y z) full gam (TTCError x) = pure (TTCError x) full gam (FileErr x y) = pure (FileErr x y) full gam (CantFindPackage x) = pure (CantFindPackage x) @@ -894,7 +894,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 (GenericMsgSol fc x y z) = pure (GenericMsgSol fc x y z) resolved gam (TTCError x) = pure (TTCError x) resolved gam (FileErr x y) = pure (FileErr x y) resolved gam (CantFindPackage x) = pure (CantFindPackage x) diff --git a/src/Core/Core.idr b/src/Core/Core.idr index 29a2827415..878201c01d 100644 --- a/src/Core/Core.idr +++ b/src/Core/Core.idr @@ -163,7 +163,8 @@ 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 + GenericMsgSol : FC -> (message : String) -> + (solutionHeader : String) -> (solutions : List String) -> Error OperatorBindingMismatch : {a : Type} -> {print : a -> Doc ()} -> FC -> (expectedFixity : FixityDeclarationInfo) -> (use_site : OperatorLHSInfo a) -> -- left: backticked, right: op symbolds @@ -356,7 +357,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 (GenericMsgSol fc msg solutionHeader sols) = show fc ++ ":" ++ msg ++ " \{solutionHeader}: " ++ 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 @@ -472,7 +473,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 (GenericMsgSol loc _ _ _) = Just loc getErrorLoc (TTCError _) = Nothing getErrorLoc (FileErr _ _) = Nothing getErrorLoc (CantFindPackage _) = Nothing @@ -562,7 +563,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 (GenericMsgSol fc x y z) = GenericMsgSol emptyFC x y z killErrorLoc (TTCError x) = TTCError x killErrorLoc (FileErr x y) = FileErr x y killErrorLoc (CantFindPackage x) = CantFindPackage x diff --git a/src/Core/Name.idr b/src/Core/Name.idr index d3d09a9924..ee466b056d 100644 --- a/src/Core/Name.idr +++ b/src/Core/Name.idr @@ -8,6 +8,8 @@ import Libraries.Text.PrettyPrint.Prettyprinter import Libraries.Text.PrettyPrint.Prettyprinter.Util import Libraries.Utils.String +import Libraries.Text.Distance.Levenshtein as Distance + import public Core.Name.Namespace %default total @@ -464,3 +466,27 @@ next (MN n i) = MN n (i + 1) next (UN n) = MN (show n) 0 next (NS ns n) = NS ns (next n) next n = MN (show n) 0 + +||| levenstein distance that needs to be reached in order for a +||| namespace path to closely match another one. +closeNamespaceDistance : Nat +closeNamespaceDistance = 3 + +||| Check if two strings are close enough to be similar, using the namespace +||| distance criteria. +closeDistance : String -> String -> IO Bool +closeDistance s1 s2 = pure (!(Distance.compute s1 s2) < closeNamespaceDistance) + +||| Check if the test closely match the reference. +||| We only check for namespaces and user-defined names. +export +closeMatch : (test, reference : Name) -> IO Bool +closeMatch (NS pathTest nameTest) (NS pathRef nameRef) + = let extractNameString = toList . (map snd . isUN >=> isBasic) + unfoldedTest = unsafeUnfoldNamespace pathTest ++ extractNameString nameTest + unfoldedRef = unsafeUnfoldNamespace pathRef ++ extractNameString nameRef + tests : IO (List Nat) = traverse (uncurry Distance.compute) (zip unfoldedTest unfoldedRef) + in map ((<= closeNamespaceDistance) . sum) tests +closeMatch (UN (Basic test)) (UN (Basic ref)) = closeDistance test ref +closeMatch _ _ = pure False + diff --git a/src/Idris/Desugar.idr b/src/Idris/Desugar.idr index 291e10958e..8985d4d7e2 100644 --- a/src/Idris/Desugar.idr +++ b/src/Idris/Desugar.idr @@ -1219,7 +1219,7 @@ mutual 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." + "Invalid fixity, \{binding} operator must be infixr 0." "Possible solutions" [ "Make it `infixr 0`: `\{binding} infixr 0 \{show opName}`" , "Remove the binding keyword: `\{fix} \{show prec} \{show opName}`" ]) @@ -1306,7 +1306,7 @@ mutual desugarDecl ps (PDirective fc d) = case d of Hide (HideName n) => pure [IPragma fc [] (\nest, env => hide fc n)] - Hide (HideFixity fx n) => pure [IPragma fc [] (\_, _ => removeFixity fx n)] + Hide (HideFixity fx n) => pure [IPragma fc [] (\_, _ => removeFixity fc fx n)] Unhide n => pure [IPragma fc [] (\nest, env => unhide fc n)] Logging i => pure [ILog ((\ i => (topics i, verbosity i)) <$> i)] LazyOn a => pure [IPragma fc [] (\nest, env => lazyActive a)] diff --git a/src/Idris/Error.idr b/src/Idris/Error.idr index a8fd7e1ccb..ca30b4546e 100644 --- a/src/Idris/Error.idr +++ b/src/Idris/Error.idr @@ -111,7 +111,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 + GenericMsgSol fc1 x1 y1 z1 == GenericMsgSol fc2 x2 y2 z2 = fc1 == fc2 && x1 == x2 && y1 == y2 && z1 == z2 TTCError x1 == TTCError x2 = x1 == x2 FileErr x1 y1 == FileErr x2 y2 = x1 == x2 && y1 == y2 CantFindPackage x1 == CantFindPackage x2 = x1 == x2 @@ -621,10 +621,10 @@ 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) +perrorRaw (GenericMsgSol fc header solutionHeader solutions) = pure $ pretty0 header <+> line <+> !(ploc fc) <+> line - <+> "Possible solutions:" <+> line + <+> fromString "\{solutionHeader}:" <+> line <+> indent 1 (vsep (map (\s => "-" <++> pretty0 s) solutions)) perrorRaw (OperatorBindingMismatch fc {print=p} expected actual opName rhs candidates) = pure $ "Operator" <++> pretty0 !(getFullName (fromEither opName)) <++> "is" diff --git a/src/Idris/Syntax.idr b/src/Idris/Syntax.idr index 0c3b31b3fb..ee650dcc61 100644 --- a/src/Idris/Syntax.idr +++ b/src/Idris/Syntax.idr @@ -1035,11 +1035,27 @@ addModDocInfo mi doc reexpts , modDocexports $= insert mi reexpts , modDocstrings $= insert mi doc } --- remove a fixity from the context +||| Remove a fixity from the context export removeFixity : - {auto s : Ref Syn SyntaxInfo} -> Fixity -> Name -> Core () -removeFixity _ key = update Syn ({fixities $= removeExact key }) + {auto s : Ref Syn SyntaxInfo} -> FC -> Fixity -> Name -> Core () +removeFixity loc _ key = do + fixityInfo <- fixities <$> get Syn + if isJust $ lookupExact key fixityInfo + then -- When the fixity is found, simply remove it + update Syn ({ fixities $= removeExact key }) + else -- When the fixity is not found, find close matches + let fixityNames : List Name = map fst (toList fixityInfo) + closeNames = !(filterM (coreLift . closeMatch key) fixityNames) + in if null closeNames + then + throw $ GenericMsg loc "Fixity \{show key} not found" + else + throw $ GenericMsgSol loc "Fixity \{show key} not found" "Did you mean" + (map printFixityHide closeNames) + where + printFixityHide : Name -> String + printFixityHide nm = "%hide \{show nm}" ||| Return all fixity declarations for an operator name export diff --git a/src/Libraries/Utils/Shunting.idr b/src/Libraries/Utils/Shunting.idr index 9413daecfb..6ef7dd9a7b 100644 --- a/src/Libraries/Utils/Shunting.idr +++ b/src/Libraries/Utils/Shunting.idr @@ -96,13 +96,13 @@ higher : Interpolation op => (showLoc : Show op) => FC -> op -> OpPrec -> op -> higher loc opx op opy (Prefix p) = pure False higher loc opx (NonAssoc x) opy oy = if x == getPrec oy - then throw (GenericMsgSol loc ( "Operator \{opx} is non-associative") + then throw (GenericMsgSol loc "Operator \{opx} is non-associative" "Possible solutions" [ "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 (GenericMsgSol loc ( "Operator \{opy} is non-associative") + then throw (GenericMsgSol loc "Operator \{opy} is non-associative" "Possible solutions" [ "Add brackets around every use of \{opy}" , "Change the fixity of \{show opy} to `infixl` or `infixr`"]) else pure (getPrec ox > y) diff --git a/tests/idris2/operators/operators011/Module.idr b/tests/idris2/operators/operators011/Module.idr new file mode 100644 index 0000000000..4d54872e0b --- /dev/null +++ b/tests/idris2/operators/operators011/Module.idr @@ -0,0 +1,3 @@ +module Module + +export infixl 7 &&++ diff --git a/tests/idris2/operators/operators011/Test.idr b/tests/idris2/operators/operators011/Test.idr new file mode 100644 index 0000000000..ec0e3f8d88 --- /dev/null +++ b/tests/idris2/operators/operators011/Test.idr @@ -0,0 +1,2 @@ + +%hide DoesNotExist.infixl.(+) diff --git a/tests/idris2/operators/operators011/Test1.idr b/tests/idris2/operators/operators011/Test1.idr new file mode 100644 index 0000000000..0baec87125 --- /dev/null +++ b/tests/idris2/operators/operators011/Test1.idr @@ -0,0 +1,3 @@ +import Module + +%hide Modul.infixl.(&&++) diff --git a/tests/idris2/operators/operators011/Test2.idr b/tests/idris2/operators/operators011/Test2.idr new file mode 100644 index 0000000000..3a2d0c6d18 --- /dev/null +++ b/tests/idris2/operators/operators011/Test2.idr @@ -0,0 +1,3 @@ +import Module + +%hide Module.infixr.(&&++) diff --git a/tests/idris2/operators/operators011/Test3.idr b/tests/idris2/operators/operators011/Test3.idr new file mode 100644 index 0000000000..a217b2f9ed --- /dev/null +++ b/tests/idris2/operators/operators011/Test3.idr @@ -0,0 +1,3 @@ +import Module + +%hide Module.infixl.(&&+*) diff --git a/tests/idris2/operators/operators011/expected b/tests/idris2/operators/operators011/expected new file mode 100644 index 0000000000..f9c2445fe3 --- /dev/null +++ b/tests/idris2/operators/operators011/expected @@ -0,0 +1,42 @@ +1/1: Building Test (Test.idr) +Error: Fixity DoesNotExist.infixl.(+) not found + +Test:2:1--2:30 + 1 | + 2 | %hide DoesNotExist.infixl.(+) + ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^ + +1/2: Building Module (Module.idr) +2/2: Building Test1 (Test1.idr) +Error: Fixity Modul.infixl.(&&++) not found + +Test1:3:1--3:26 + 1 | import Module + 2 | + 3 | %hide Modul.infixl.(&&++) + ^^^^^^^^^^^^^^^^^^^^^^^^^ + +Did you mean: + - %hide Module.infixl.(&&++) +2/2: Building Test2 (Test2.idr) +Error: Fixity Module.infixr.(&&++) not found + +Test2:3:1--3:27 + 1 | import Module + 2 | + 3 | %hide Module.infixr.(&&++) + ^^^^^^^^^^^^^^^^^^^^^^^^^^ + +Did you mean: + - %hide Module.infixl.(&&++) +2/2: Building Test3 (Test3.idr) +Error: Fixity Module.infixl.(&&+*) not found + +Test3:3:1--3:27 + 1 | import Module + 2 | + 3 | %hide Module.infixl.(&&+*) + ^^^^^^^^^^^^^^^^^^^^^^^^^^ + +Did you mean: + - %hide Module.infixl.(&&++) diff --git a/tests/idris2/operators/operators011/run b/tests/idris2/operators/operators011/run new file mode 100755 index 0000000000..5483007315 --- /dev/null +++ b/tests/idris2/operators/operators011/run @@ -0,0 +1,6 @@ +. ../../../testutils.sh + +check Test.idr +check Test1.idr +check Test2.idr +check Test3.idr From 0e09b8d575ca6c56c9d3fc23c7639b4f9e4c34f7 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Andr=C3=A9=20Videla?= Date: Mon, 17 Jun 2024 12:39:37 +0100 Subject: [PATCH 2/2] Show unrelated namespace with matching operator name --- src/Idris/Syntax.idr | 8 +++++--- tests/idris2/operators/operators011/Test.idr | 2 +- tests/idris2/operators/operators011/Test4.idr | 4 ++++ tests/idris2/operators/operators011/expected | 20 +++++++++++++++---- tests/idris2/operators/operators011/run | 1 + 5 files changed, 27 insertions(+), 8 deletions(-) create mode 100644 tests/idris2/operators/operators011/Test4.idr diff --git a/src/Idris/Syntax.idr b/src/Idris/Syntax.idr index ee650dcc61..7c712d5e39 100644 --- a/src/Idris/Syntax.idr +++ b/src/Idris/Syntax.idr @@ -1047,12 +1047,14 @@ removeFixity loc _ key = do else -- When the fixity is not found, find close matches let fixityNames : List Name = map fst (toList fixityInfo) closeNames = !(filterM (coreLift . closeMatch key) fixityNames) - in if null closeNames + sameName : List Name = fst <$> lookupName (dropAllNS key) fixityInfo + similarNamespaces = nub (closeNames ++ sameName) + in if null similarNamespaces then throw $ GenericMsg loc "Fixity \{show key} not found" else - throw $ GenericMsgSol loc "Fixity \{show key} not found" "Did you mean" - (map printFixityHide closeNames) + throw $ GenericMsgSol loc "Fixity \{show key} not found" "Did you mean" + $ map printFixityHide similarNamespaces where printFixityHide : Name -> String printFixityHide nm = "%hide \{show nm}" diff --git a/tests/idris2/operators/operators011/Test.idr b/tests/idris2/operators/operators011/Test.idr index ec0e3f8d88..fcf137e65a 100644 --- a/tests/idris2/operators/operators011/Test.idr +++ b/tests/idris2/operators/operators011/Test.idr @@ -1,2 +1,2 @@ -%hide DoesNotExist.infixl.(+) +%hide DoesNotExist.infixl.(+-+) diff --git a/tests/idris2/operators/operators011/Test4.idr b/tests/idris2/operators/operators011/Test4.idr new file mode 100644 index 0000000000..8a26c96fe7 --- /dev/null +++ b/tests/idris2/operators/operators011/Test4.idr @@ -0,0 +1,4 @@ + +import Module + +%hide DoesNotExist.infixl.(&&++) diff --git a/tests/idris2/operators/operators011/expected b/tests/idris2/operators/operators011/expected index f9c2445fe3..e923effa62 100644 --- a/tests/idris2/operators/operators011/expected +++ b/tests/idris2/operators/operators011/expected @@ -1,10 +1,10 @@ 1/1: Building Test (Test.idr) -Error: Fixity DoesNotExist.infixl.(+) not found +Error: Fixity DoesNotExist.infixl.(+-+) not found -Test:2:1--2:30 +Test:2:1--2:32 1 | - 2 | %hide DoesNotExist.infixl.(+) - ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^ + 2 | %hide DoesNotExist.infixl.(+-+) + ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^ 1/2: Building Module (Module.idr) 2/2: Building Test1 (Test1.idr) @@ -40,3 +40,15 @@ Test3:3:1--3:27 Did you mean: - %hide Module.infixl.(&&++) +2/2: Building Test4 (Test4.idr) +Error: Fixity DoesNotExist.infixl.(&&++) not found + +Test4:4:1--4:33 + 1 | + 2 | import Module + 3 | + 4 | %hide DoesNotExist.infixl.(&&++) + ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^ + +Did you mean: + - %hide Module.infixl.(&&++) diff --git a/tests/idris2/operators/operators011/run b/tests/idris2/operators/operators011/run index 5483007315..151c8ed7a1 100755 --- a/tests/idris2/operators/operators011/run +++ b/tests/idris2/operators/operators011/run @@ -4,3 +4,4 @@ check Test.idr check Test1.idr check Test2.idr check Test3.idr +check Test4.idr