From 18b165bedeb749b04800866234849c1099c79615 Mon Sep 17 00:00:00 2001
From: Jacob Walters <prog@jacobwalte.rs>
Date: Fri, 15 Mar 2024 22:41:29 +0000
Subject: [PATCH 1/2] [ elab ] Let elab scripts access visibility modifiers

---
 CHANGELOG_NEXT.md                                | 3 +++
 CONTRIBUTORS                                     | 1 +
 libs/base/Language/Reflection.idr                | 7 +++++++
 src/TTImp/Elab/RunElab.idr                       | 5 +++++
 tests/idris2/reflection/reflection028/GetVis.idr | 7 +++++++
 tests/idris2/reflection/reflection028/expected   | 5 +++++
 tests/idris2/reflection/reflection028/input      | 5 +++++
 tests/idris2/reflection/reflection028/run        | 3 +++
 tests/idris2/reflection/reflection028/test.ipkg  | 1 +
 9 files changed, 37 insertions(+)
 create mode 100644 tests/idris2/reflection/reflection028/GetVis.idr
 create mode 100644 tests/idris2/reflection/reflection028/expected
 create mode 100644 tests/idris2/reflection/reflection028/input
 create mode 100755 tests/idris2/reflection/reflection028/run
 create mode 100644 tests/idris2/reflection/reflection028/test.ipkg

diff --git a/CHANGELOG_NEXT.md b/CHANGELOG_NEXT.md
index 800eb9fd0..3c3c45b62 100644
--- a/CHANGELOG_NEXT.md
+++ b/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
diff --git a/CONTRIBUTORS b/CONTRIBUTORS
index 50b728214..677ff6c62 100644
--- a/CONTRIBUTORS
+++ b/CONTRIBUTORS
@@ -31,6 +31,7 @@ Giuseppe Lomurno
 Guillaume Allais
 Hiroki Hattori
 Ilya Rezvov
+Jacob Walters
 Jan de Muijnck-Hughes
 Jeetu
 Jens Petersen
diff --git a/libs/base/Language/Reflection.idr b/libs/base/Language/Reflection.idr
index 2dd00fd8b..f68bc0859 100644
--- a/libs/base/Language/Reflection.idr
+++ b/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
diff --git a/src/TTImp/Elab/RunElab.idr b/src/TTImp/Elab/RunElab.idr
index 979d7a0b6..457a9b962 100644
--- a/src/TTImp/Elab/RunElab.idr
+++ b/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'
diff --git a/tests/idris2/reflection/reflection028/GetVis.idr b/tests/idris2/reflection/reflection028/GetVis.idr
new file mode 100644
index 000000000..812df355b
--- /dev/null
+++ b/tests/idris2/reflection/reflection028/GetVis.idr
@@ -0,0 +1,7 @@
+module GetVis
+
+import Language.Reflection
+
+private fooPriv : Int
+export fooExp : Int
+public export fooPubExp : Int
diff --git a/tests/idris2/reflection/reflection028/expected b/tests/idris2/reflection/reflection028/expected
new file mode 100644
index 000000000..47e727a7d
--- /dev/null
+++ b/tests/idris2/reflection/reflection028/expected
@@ -0,0 +1,5 @@
+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> Bye for now!
diff --git a/tests/idris2/reflection/reflection028/input b/tests/idris2/reflection/reflection028/input
new file mode 100644
index 000000000..00a5a3dde
--- /dev/null
+++ b/tests/idris2/reflection/reflection028/input
@@ -0,0 +1,5 @@
+:let %language ElabReflection
+%runElab getVis `{fooPriv}
+%runElab getVis `{fooExp}
+%runElab getVis `{fooPubExp}
+:q
diff --git a/tests/idris2/reflection/reflection028/run b/tests/idris2/reflection/reflection028/run
new file mode 100755
index 000000000..96c3530d1
--- /dev/null
+++ b/tests/idris2/reflection/reflection028/run
@@ -0,0 +1,3 @@
+. ../../../testutils.sh
+
+idris2 GetVis.idr < input
diff --git a/tests/idris2/reflection/reflection028/test.ipkg b/tests/idris2/reflection/reflection028/test.ipkg
new file mode 100644
index 000000000..2c5b5ab52
--- /dev/null
+++ b/tests/idris2/reflection/reflection028/test.ipkg
@@ -0,0 +1 @@
+package a-test

From da6b21a5706fcc1e1a1d34206070c0672aa702e3 Mon Sep 17 00:00:00 2001
From: Jacob Walters <prog@jacobwalte.rs>
Date: Fri, 15 Mar 2024 22:51:49 +0000
Subject: [PATCH 2/2] [ test ] More comprehensive test for getVis

---
 tests/idris2/reflection/reflection028/GetVis.idr | 9 +++++++++
 tests/idris2/reflection/reflection028/expected   | 1 +
 tests/idris2/reflection/reflection028/input      | 1 +
 3 files changed, 11 insertions(+)

diff --git a/tests/idris2/reflection/reflection028/GetVis.idr b/tests/idris2/reflection/reflection028/GetVis.idr
index 812df355b..cd3921278 100644
--- a/tests/idris2/reflection/reflection028/GetVis.idr
+++ b/tests/idris2/reflection/reflection028/GetVis.idr
@@ -5,3 +5,12 @@ 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
diff --git a/tests/idris2/reflection/reflection028/expected b/tests/idris2/reflection/reflection028/expected
index 47e727a7d..f8cf9ac86 100644
--- a/tests/idris2/reflection/reflection028/expected
+++ b/tests/idris2/reflection/reflection028/expected
@@ -2,4 +2,5 @@
 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!
diff --git a/tests/idris2/reflection/reflection028/input b/tests/idris2/reflection/reflection028/input
index 00a5a3dde..9a05fb5bb 100644
--- a/tests/idris2/reflection/reflection028/input
+++ b/tests/idris2/reflection/reflection028/input
@@ -2,4 +2,5 @@
 %runElab getVis `{fooPriv}
 %runElab getVis `{fooExp}
 %runElab getVis `{fooPubExp}
+%runElab getVis `{foo}
 :q