diff --git a/src/Core/Context.idr b/src/Core/Context.idr index aa1231c88..ce7256c79 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 29a282741..878201c01 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 d3d09a992..ee466b056 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 291e10958..8985d4d7e 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 a8fd7e1cc..ca30b4546 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 0c3b31b3f..ee650dcc6 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 9413daecf..6ef7dd9a7 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 000000000..4d54872e0 --- /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 000000000..ec0e3f8d8 --- /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 000000000..0baec8712 --- /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 000000000..3a2d0c6d1 --- /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 000000000..a217b2f9e --- /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 000000000..f9c2445fe --- /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 000000000..548300731 --- /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