From 50c60185a74ea51cb69739c1d27a2f0119212313 Mon Sep 17 00:00:00 2001 From: Ruslan Feizerahmanov Date: Tue, 9 Mar 2021 17:13:29 +0300 Subject: [PATCH] [ auto ] Ignore hidden names in Core.Context.getSearchData (#1143) Co-authored-by: Guillaume ALLAIS --- src/Core/Context.idr | 28 +++++++++++++++---- tests/Main.idr | 3 +- tests/idris2/interface025/AutoSearchHide1.idr | 15 ++++++++++ tests/idris2/interface025/AutoSearchHide2.idr | 22 +++++++++++++++ tests/idris2/interface025/expected | 3 ++ tests/idris2/interface025/input | 1 + tests/idris2/interface025/run | 3 ++ 7 files changed, 68 insertions(+), 7 deletions(-) create mode 100644 tests/idris2/interface025/AutoSearchHide1.idr create mode 100644 tests/idris2/interface025/AutoSearchHide2.idr create mode 100644 tests/idris2/interface025/expected create mode 100644 tests/idris2/interface025/input create mode 100644 tests/idris2/interface025/run diff --git a/src/Core/Context.idr b/src/Core/Context.idr index 2cb186876..8b59a5014 100644 --- a/src/Core/Context.idr +++ b/src/Core/Context.idr @@ -15,6 +15,7 @@ import Libraries.Utils.Binary import Libraries.Data.IntMap import Data.IOArray import Data.List +import Data.Maybe import Libraries.Data.NameMap import Libraries.Data.StringMap @@ -531,6 +532,11 @@ lookupContextEntry n ctxt | Nothing => pure Nothing lookupContextEntry (Resolved idx) ctxt +||| Check if the name has been hidden by the `%hide` directive. +export +isHidden : Name -> Context -> Bool +isHidden fulln ctxt = isJust $ lookup fulln (hidden ctxt) + export lookupCtxtName : Name -> Context -> Core (List (Name, Int, GlobalDef)) lookupCtxtName n ctxt @@ -1583,15 +1589,18 @@ getSearchData fc defaults target = do defs <- get Ctxt Just (TCon _ _ _ dets u _ _ _) <- lookupDefExact target (gamma defs) | _ => throw (UndefinedName fc target) - let hs = case lookup !(toFullNames target) (typeHints defs) of - Just hs => hs - Nothing => [] + hs <- case lookup !(toFullNames target) (typeHints defs) of + Just hs => filterM (\x => notHidden x (gamma defs)) hs + Nothing => pure [] if defaults - then let defns = map fst (filter isDefault + then let defns = map fst !(filterM (\x => pure $ isDefault x + && !(notHidden x (gamma defs))) (toList (autoHints defs))) in pure (MkSearchData [] [(False, defns)]) - else let opens = map fst (toList (openHints defs)) - autos = map fst (filter (not . isDefault) + else let opens = map fst !(filterM (\x => notHidden x (gamma defs)) + (toList (openHints defs))) + autos = map fst !(filterM (\x => pure $ not (isDefault x) + && !(notHidden x (gamma defs))) (toList (autoHints defs))) tyhs = map fst (filter direct hs) chasers = map fst (filter (not . direct) hs) in @@ -1601,6 +1610,13 @@ getSearchData fc defaults target (not (uniqueAuto u), tyhs), (True, chasers)])) where + ||| We don't want hidden (by `%hide`) names to appear in the search. + ||| Lookup has to be done by a full qualified name, not a resolved ID. + notHidden : forall a. (Name, a) -> Context -> Core Bool + notHidden (n, _) ctxt = do + fulln <- toFullNames n + pure $ not (isHidden fulln ctxt) + isDefault : (Name, Bool) -> Bool isDefault = snd diff --git a/tests/Main.idr b/tests/Main.idr index 0268fe993..6d76f1ac1 100644 --- a/tests/Main.idr +++ b/tests/Main.idr @@ -90,7 +90,8 @@ idrisTestsInterface = MkTestPool [] "interface009", "interface010", "interface011", "interface012", "interface013", "interface014", "interface015", "interface016", "interface017", "interface018", "interface019", "interface020", - "interface021", "interface022", "interface023", "interface024"] + "interface021", "interface022", "interface023", "interface024", + "interface025"] idrisTestsLinear : TestPool idrisTestsLinear = MkTestPool [] diff --git a/tests/idris2/interface025/AutoSearchHide1.idr b/tests/idris2/interface025/AutoSearchHide1.idr new file mode 100644 index 000000000..06c5d7f3d --- /dev/null +++ b/tests/idris2/interface025/AutoSearchHide1.idr @@ -0,0 +1,15 @@ +module AutoSearchHide1 + +public export +interface A where + Value : Nat + +public export +[ZeroA] A where + Value = 0 + +public export +%hint +HintZeroA : A +HintZeroA = ZeroA + diff --git a/tests/idris2/interface025/AutoSearchHide2.idr b/tests/idris2/interface025/AutoSearchHide2.idr new file mode 100644 index 000000000..81deea53d --- /dev/null +++ b/tests/idris2/interface025/AutoSearchHide2.idr @@ -0,0 +1,22 @@ +module AutoSearchHide2 + +import AutoSearchHide1 + +myZero : Value === 0 +myZero = Refl + +[OneA] A where + Value = 1 + +%hint +HintOneA : A +HintOneA = OneA + +-- Want to use the OneA (via HintOneA) instance here. + +-- `%hide` should block the auto-search from +-- including the `HintZeroA` hint into the list of solutions. +-- Thus, we don't get into the `multiple solutions` situation. +%hide HintZeroA +myOne : Value === 1 +myOne = Refl diff --git a/tests/idris2/interface025/expected b/tests/idris2/interface025/expected new file mode 100644 index 000000000..6a399667b --- /dev/null +++ b/tests/idris2/interface025/expected @@ -0,0 +1,3 @@ +1/2: Building AutoSearchHide1 (AutoSearchHide1.idr) +2/2: Building AutoSearchHide2 (AutoSearchHide2.idr) +AutoSearchHide2> Bye for now! diff --git a/tests/idris2/interface025/input b/tests/idris2/interface025/input new file mode 100644 index 000000000..d325550eb --- /dev/null +++ b/tests/idris2/interface025/input @@ -0,0 +1 @@ +:q diff --git a/tests/idris2/interface025/run b/tests/idris2/interface025/run new file mode 100644 index 000000000..67279ad61 --- /dev/null +++ b/tests/idris2/interface025/run @@ -0,0 +1,3 @@ +$1 --no-banner --no-color --console-width 0 AutoSearchHide2.idr < input + +rm -rf build