[ fix #2138] Add an %unhide pragma (#2181)

* add %unhide pragma

* add a test case

* clean up

* more consistent English usage (+fix some typos)

* add a warning for unhiding not-already-hidden names

* move `unhide` (and `hide`) to the bottom of the source file to avoid having to forward-declare `recordWarning`

src/Core/Context.idr

@@ -220,14 +220,16 @@ lookupContextEntry n ctxt
                   | Nothing => pure Nothing
          lookupContextEntry (Resolved idx) ctxt
 
-||| Check if the name has been hidden by the `%hide` directive.
+||| Check if the given name has been hidden by the `%hide` directive.
 export
 isHidden : Name -> Context -> Bool
 isHidden fulln ctxt = isJust $ lookup fulln (hidden ctxt)
 
+||| Look up a possibly hidden name in the context. The first (boolean) argument
+||| controls whether names hidden by `%hide` are returned too (True=yes, False=no).
 export
-lookupCtxtName : Name -> Context -> Core (List (Name, Int, GlobalDef))
-lookupCtxtName n ctxt
+lookupCtxtName' : Bool -> Name -> Context -> Core (List (Name, Int, GlobalDef))
+lookupCtxtName' allowHidden n ctxt
     = case userNameRoot n of
            Nothing => do Just (i, res) <- lookupCtxtExactI n ctxt
                               | Nothing => pure []
@@ -241,12 +243,17 @@ lookupCtxtName n ctxt
     resn : (Name, Int, GlobalDef) -> Int
     resn (_, i, _) = i
 
+    hlookup : Name -> NameMap () -> Maybe ()
+    hlookup fulln hiddens = if allowHidden
+      then Nothing
+      else lookup fulln hiddens
+
     lookupPossibles : List (Name, Int, GlobalDef) -> -- accumulator
                       List PossibleName ->
                       Core (List (Name, Int, GlobalDef))
     lookupPossibles acc [] = pure (reverse acc)
     lookupPossibles acc (Direct fulln i :: ps)
-       = case lookup fulln (hidden ctxt) of
+       = case (hlookup fulln (hidden ctxt)) of
               Nothing =>
                 do Just res <- lookupCtxtExact (Resolved i) ctxt
                         | Nothing => lookupPossibles acc ps
@@ -255,7 +262,7 @@ lookupCtxtName n ctxt
                       else lookupPossibles acc ps
               _ => lookupPossibles acc ps
     lookupPossibles acc (Alias asn fulln i :: ps)
-       = case lookup fulln (hidden ctxt) of
+       = case (hlookup fulln (hidden ctxt)) of
               Nothing =>
                 do Just res <- lookupCtxtExact (Resolved i) ctxt
                         | Nothing => lookupPossibles acc ps
@@ -264,9 +271,22 @@ lookupCtxtName n ctxt
                       else lookupPossibles acc ps
               _ => lookupPossibles acc ps
 
+||| Look up a name in the context, ignoring names hidden by `%hide`.
+export
+lookupCtxtName : Name -> Context -> Core (List (Name, Int, GlobalDef))
+lookupCtxtName = lookupCtxtName' False
+
+||| Look up a (possible hidden) name in the context.
+export
+lookupHiddenCtxtName : Name -> Context -> Core (List (Name, Int, GlobalDef))
+lookupHiddenCtxtName = lookupCtxtName' True
+
 hideName : Name -> Context -> Context
 hideName n ctxt = record { hidden $= insert n () } ctxt
 
+unhideName : Name -> Context -> Context
+unhideName n ctxt = record { hidden $= delete n } ctxt
+
 branchCtxt : Context -> Core Context
 branchCtxt ctxt = pure (record { branchDepth $= S } ctxt)
 
@@ -1404,17 +1424,6 @@ setVisibility fc n vis
               | Nothing => undefinedName fc n
          ignore $ addDef n (record { visibility = vis } def)
 
--- Set a name as Private that was previously visible (and, if 'everywhere' is
--- set, hide in any modules imported by this one)
-export
-hide : {auto c : Ref Ctxt Defs} ->
-       FC -> Name -> Core ()
-hide fc n
-    = do defs <- get Ctxt
-         [(nsn, _)] <- lookupCtxtName n (gamma defs)
-              | res => ambiguousName fc n (map fst res)
-         put Ctxt (record { gamma $= hideName nsn } defs)
-
 public export
 record SearchData where
   constructor MkSearchData
@@ -2381,3 +2390,28 @@ setIncData : {auto c : Ref Ctxt Defs} ->
 setIncData cg res
     = do defs <- get Ctxt
          put Ctxt (record { incData $= ((cg, res) :: )} defs)
+
+-- Set a name as Private that was previously visible (and, if 'everywhere' is
+-- set, hide in any modules imported by this one)
+export
+hide : {auto c : Ref Ctxt Defs} ->
+       FC -> Name -> Core ()
+hide fc n
+    = do defs <- get Ctxt
+         [(nsn, _)] <- lookupCtxtName n (gamma defs)
+              | res => ambiguousName fc n (map fst res)
+         put Ctxt (record { gamma $= hideName nsn } defs)
+
+-- Set a name as Public that was previously hidden
+-- Note: this is here at the bottom only becuase `recordWarning` is defined just above.
+export
+unhide : {auto c : Ref Ctxt Defs} ->
+       FC -> Name -> Core ()
+unhide fc n
+    = do defs <- get Ctxt
+         [(nsn, _)] <- lookupHiddenCtxtName n (gamma defs)
+              | res => ambiguousName fc n (map fst res)
+         put Ctxt (record { gamma $= unhideName nsn } defs)
+         unless (isHidden nsn (gamma defs)) $ do
+           recordWarning $ GenericWarn $
+             "Trying to %unhide `" ++ show nsn ++ "`, which was not hidden in the first place"

src/Idris/Desugar.idr

@@ -1043,6 +1043,7 @@ mutual
   desugarDecl ps (PDirective fc d)
       = case d of
              Hide n => pure [IPragma [] (\nest, env => hide fc n)]
+             Unhide n => pure [IPragma [] (\nest, env => unhide fc n)]
              Logging i => pure [ILog ((\ i => (topics i, verbosity i)) <$> i)]
              LazyOn a => pure [IPragma [] (\nest, env => lazyActive a)]
              UnboundImplicits a => do

src/Idris/Parser.idr

@@ -1224,6 +1224,10 @@ directive fname indents
          n <- name
          atEnd indents
          pure (Hide n)
+  <|> do decorate fname Keyword $ pragma "unhide"
+         n <- name
+         atEnd indents
+         pure (Unhide n)
 --   <|> do pragma "hide_export"
 --          n <- name
 --          atEnd indents

src/Idris/Syntax.idr

@@ -296,6 +296,7 @@ mutual
   public export
   data Directive : Type where
        Hide : Name -> Directive
+       Unhide : Name -> Directive
        Logging : Maybe LogLevel -> Directive
        LazyOn : Bool -> Directive
        UnboundImplicits : Bool -> Directive
@@ -319,7 +320,7 @@ mutual
 
   directiveList : List Directive
   directiveList =
-      [ (Hide ph), (Logging Nothing), (LazyOn False)
+      [ (Hide ph), (Unhide ph), (Logging Nothing), (LazyOn False)
       , (UnboundImplicits False), (AmbigDepth 0)
       , (PairNames ph ph ph), (RewriteName ph ph)
       , (PrimInteger ph), (PrimString ph), (PrimChar ph)
@@ -346,6 +347,7 @@ mutual
     where
       showDirective : Directive -> String
       showDirective (Hide _)             = "%hide name"
+      showDirective (Unhide _)           = "%unhide name"
       showDirective (Logging _)          = "%logging [topic] lvl"
       showDirective (LazyOn _)           = "%auto_lazy on|off"
       showDirective (UnboundImplicits _) = "%unbound_implicits"

tests/Main.idr

@@ -42,7 +42,7 @@ idrisTestsBasic = MkTestPool "Fundamental language features" [] Nothing
        "basic051", "basic052", "basic053", "basic054", "basic055",
        "basic056", "basic057", "basic058", "basic059", "basic060",
        "basic061", "basic062", "basic063", "basic064", "basic065",
-       "basic066", "basic067",
+       "basic066", "basic067", "basic068",
        "interpolation001", "interpolation002", "interpolation003",
        "interpolation004"]
 

tests/idris2/basic068/Issue2138.idr

@@ -0,0 +1,41 @@
+
+namespace Foo
+
+  public export
+  data T
+    = A Int
+    | B T
+
+  export
+  Show T where
+    show (A n) = "[A " ++ show n ++ "]"
+    show (B t) = "[B " ++ show t ++ "]"
+
+namespace Bar
+
+  %hide Foo.T
+
+  public export
+  data T
+    = A Int
+    | B T
+    | C Bool
+
+  export
+  Show T where
+    show (A n) = "{A " ++ show n ++ "}"
+    show (B t) = "{B " ++ show t ++ "}"
+    show (C b) = "{C " ++ show b ++ "}"
+
+  %unhide Foo.T
+
+foo : Foo.T
+foo = B (A 5)
+
+bar : Bar.T
+bar = B (A 6)
+
+main : IO ()
+main = do
+  printLn foo
+  printLn bar

tests/idris2/basic068/expected

@@ -0,0 +1,2 @@
+[B [A 5]]
+{B {A 6}}

tests/idris2/basic068/run

@@ -0,0 +1,3 @@
+rm -rf build
+
+$1 --no-color --console-width 0 --no-banner --exec main Issue2138.idr