Merge pull request #3235 from jacobjwalters/main

[ elab ] Let elab scripts access visibility modifiers

CHANGELOG_NEXT.md

@@ -30,6 +30,9 @@ This CHANGELOG describes the merged but unreleased changes. Please see [CHANGELO
   customise the syntax of operator to look more like a binder.
   See [#3113](https://github.com/idris-lang/Idris2/issues/3113).
 
+* Elaborator scripts were made to be able to access the visibility modifier of a
+  definition, via `getVis`.
+
 ### Backend changes
 
 #### RefC

CONTRIBUTORS

@@ -31,6 +31,7 @@ Giuseppe Lomurno
 Guillaume Allais
 Hiroki Hattori
 Ilya Rezvov
+Jacob Walters
 Jan de Muijnck-Hughes
 Jeetu
 Jens Petersen

libs/base/Language/Reflection.idr

@@ -85,6 +85,8 @@ data Elab : Type -> Type where
      GetType : Name -> Elab (List (Name, TTImp))
      -- Get the metadata associated with a name
      GetInfo : Name -> Elab (List (Name, NameInfo))
+     -- Get the visibility associated with a name
+     GetVis : Name -> Elab (List (Name, Visibility))
      -- Get the type of a local variable
      GetLocalType : Name -> Elab TTImp
      -- Get the constructors of a data type. The name must be fully resolved.
@@ -181,6 +183,9 @@ interface Monad m => Elaboration m where
   ||| Get the metadata associated with a name. Returns all matching names and their types
   getInfo : Name -> m (List (Name, NameInfo))
 
+  ||| Get the visibility associated with a name. Returns all matching names and their visibilities
+  getVis : Name -> m (List (Name, Visibility))
+
   ||| Get the type of a local variable
   getLocalType : Name -> m TTImp
 
@@ -237,6 +242,7 @@ Elaboration Elab where
   inCurrentNS    = InCurrentNS
   getType        = GetType
   getInfo        = GetInfo
+  getVis         = GetVis
   getLocalType   = GetLocalType
   getCons        = GetCons
   getReferredFns = GetReferredFns
@@ -263,6 +269,7 @@ Elaboration m => MonadTrans t => Monad (t m) => Elaboration (t m) where
   inCurrentNS         = lift . inCurrentNS
   getType             = lift . getType
   getInfo             = lift . getInfo
+  getVis              = lift . getVis
   getLocalType        = lift . getLocalType
   getCons             = lift . getCons
   getReferredFns      = lift . getReferredFns

src/TTImp/Elab/RunElab.idr

@@ -18,6 +18,7 @@ import Idris.REPL.Opts
 import Idris.Syntax
 
 import Libraries.Data.NameMap
+import Libraries.Data.WithDefault
 import Libraries.Utils.Path
 
 import TTImp.Elab.Check
@@ -291,6 +292,10 @@ elabScript rig fc nest env script@(NDCon nfc nm t ar args) exp
         = do n' <- evalClosure defs n
              res <- lookupNameInfo !(reify defs n') (gamma defs)
              scriptRet res
+    elabCon defs "GetVis" [n]
+        = do dn <- reify defs !(evalClosure defs n)
+             ds <- lookupCtxtName dn (gamma defs)
+             scriptRet $ map (\(n,_,d) => (n, collapseDefault $ visibility d)) ds
     elabCon defs "GetLocalType" [n]
         = do n' <- evalClosure defs n
              n <- reify defs n'

tests/idris2/reflection/reflection028/GetVis.idr

@@ -0,0 +1,16 @@
+module GetVis
+
+import Language.Reflection
+
+private fooPriv : Int
+export fooExp : Int
+public export fooPubExp : Int
+
+namespace A
+  private foo : Int
+
+namespace B
+  export foo : Int
+
+namespace C
+  public export foo : Int

tests/idris2/reflection/reflection028/expected

@@ -0,0 +1,6 @@
+1/1: Building GetVis (GetVis.idr)
+GetVis> GetVis> [(NS (MkNS ["GetVis"]) (UN (Basic "fooPriv")), Private)]
+GetVis> [(NS (MkNS ["GetVis"]) (UN (Basic "fooExp")), Export)]
+GetVis> [(NS (MkNS ["GetVis"]) (UN (Basic "fooPubExp")), Public)]
+GetVis> [(NS (MkNS ["A", "GetVis"]) (UN (Basic "foo")), Private), (NS (MkNS ["B", "GetVis"]) (UN (Basic "foo")), Export), (NS (MkNS ["C", "GetVis"]) (UN (Basic "foo")), Public)]
+GetVis> Bye for now!

tests/idris2/reflection/reflection028/input

@@ -0,0 +1,6 @@
+:let %language ElabReflection
+%runElab getVis `{fooPriv}
+%runElab getVis `{fooExp}
+%runElab getVis `{fooPubExp}
+%runElab getVis `{foo}
+:q

tests/idris2/reflection/reflection028/run

@@ -0,0 +1,3 @@
+. ../../../testutils.sh
+
+idris2 GetVis.idr < input

tests/idris2/reflection/reflection028/test.ipkg

@@ -0,0 +1 @@
+package a-test