Merge pull request #3762 from bio-aeon/add-getfc-elab

[ elab ] Add `getFC` for call-site source location

Author: dunhamsteve

CHANGELOG_NEXT.md

@@ -73,6 +73,8 @@ should target this file (`CHANGELOG_NEXT`).
 * Better messages for errors inside string interpolation.
 * Added execution time logging for elaboration scripts.
 * Optimised the passing of local variables during compile-time normalisation.
+* Added `getFC` to elaborator reflection, exposing the macro call-site source
+  location.
 
 ### Building/Packaging changes
 

CONTRIBUTORS

@@ -8,6 +8,7 @@ Aleksei Volkov
 Alex Asafov
 Alex Gryzlov
 Alex Silva
+Alexandr Chigrinets
 Alissa Tung
 Andor Penzes
 Andre Kuhlenschmidt

libs/base/Language/Reflection.idr

@@ -97,6 +97,8 @@ data Elab : Type -> Type where
      GetReferredFns : Name -> Elab (List Name)
      -- Get the name of the current and outer functions, if it is applicable
      GetCurrentFn : Elab (SnocList Name)
+     -- Get the source location of the macro call site
+     GetFC : Elab FC
      -- Check a group of top level declarations
      Declare : List Decl -> Elab ()
 
@@ -203,6 +205,9 @@ interface Monad m => Elaboration m where
   ||| Get the name of the current and outer functions, if we are in a function
   getCurrentFn : m (SnocList Name)
 
+  ||| Get the source location of the macro call site.
+  getFC : m FC
+
   ||| Make some top level declarations
   declare : List Decl -> m ()
 
@@ -253,6 +258,7 @@ Elaboration Elab where
   getCons        = GetCons
   getReferredFns = GetReferredFns
   getCurrentFn   = GetCurrentFn
+  getFC          = GetFC
   declare        = Declare
   readFile       = ReadFile
   writeFile      = WriteFile
@@ -281,6 +287,7 @@ Elaboration m => MonadTrans t => Monad (t m) => Elaboration (t m) where
   getCons             = lift . getCons
   getReferredFns      = lift . getReferredFns
   getCurrentFn        = lift getCurrentFn
+  getFC               = lift getFC
   declare             = lift . declare
   readFile            = lift .: readFile
   writeFile d         = lift .: writeFile d

src/TTImp/Elab/RunElab.idr

@@ -317,6 +317,8 @@ elabScript rig fc nest env script@(NDCon nfc nm t ar args) exp
     elabCon defs "GetCurrentFn" []
         = do defs <- get Ctxt
              scriptRet defs.defsStack
+    elabCon defs "GetFC" []
+        = scriptRet fc
     elabCon defs "Declare" [d]
         = do d' <- evalClosure defs d
              decls <- reify defs d'

tests/idris2/reflection/reflection036/GetFC.idr

@@ -0,0 +1,13 @@
+import Language.Reflection
+
+%language ElabReflection
+
+%macro
+here : Elab String
+here = do
+  MkFC (PhysicalIdrSrc _) (l, c) _ <- getFC
+    | _ => fail "expected a physical source location"
+  pure $ "line " ++ show l ++ ", col " ++ show c
+
+main : IO ()
+main = putStrLn here

tests/idris2/reflection/reflection036/expected

@@ -0,0 +1 @@
+line 12, col 16

tests/idris2/reflection/reflection036/run

@@ -0,0 +1,3 @@
+. ../../../testutils.sh
+
+run GetFC.idr