[ elab ] Add an ability to inspect in which function we currently are

CHANGELOG.md

@@ -28,7 +28,9 @@
 * Elaborator scripts were made to be able to access project files,
   allowing the support for type providers and similar stuff.
 * Elaborator scripts were made to be able to inspect which definitions are
-  referred to by another definitions.
+  referred to by another definitions, and in which function currently elaborator is.
+  These features together give an ability to inspect whether particular expressions
+  are recursive (including mutual recursion).
 
 ### REPL changes
 

libs/base/Language/Reflection.idr

@@ -89,6 +89,8 @@ data Elab : Type -> Type where
      GetCons : Name -> Elab (List Name)
      -- Get all function definition names referred in a definition. The name must be fully resolved.
      GetReferredFns : Name -> Elab (List Name)
+     -- Get the name of the current and outer functions, if it is applicable
+     GetCurrentFn : Elab (SnocList Name)
      -- Check a group of top level declarations
      Declare : List Decl -> Elab ()
 
@@ -186,6 +188,9 @@ interface Monad m => Elaboration m where
   ||| Get all the name of function definitions that a given definition refers to (transitively)
   getReferredFns : Name -> m (List Name)
 
+  ||| Get the name of the current and outer functions, if we are in a function
+  getCurrentFn : m (SnocList Name)
+
   ||| Make some top level declarations
   declare : List Decl -> m ()
 
@@ -233,6 +238,7 @@ Elaboration Elab where
   getLocalType   = GetLocalType
   getCons        = GetCons
   getReferredFns = GetReferredFns
+  getCurrentFn   = GetCurrentFn
   declare        = Declare
   readFile       = ReadFile
   writeFile      = WriteFile
@@ -258,6 +264,7 @@ Elaboration m => MonadTrans t => Monad (t m) => Elaboration (t m) where
   getLocalType        = lift . getLocalType
   getCons             = lift . getCons
   getReferredFns      = lift . getReferredFns
+  getCurrentFn        = lift getCurrentFn
   declare             = lift . declare
   readFile            = lift .: readFile
   writeFile d         = lift .: writeFile d

src/Core/Context.idr

@@ -1044,6 +1044,7 @@ record Defs where
   foreignExports : NameMap (List (String, String))
        -- ^ For functions which are callable from a foreign language. This
        -- maps names to a pair of the back end and the exported function name
+  defsStack : SnocList Name -- stack of the definition names being processed
 
 -- Label for context references
 export
@@ -1093,6 +1094,7 @@ initDefs
            , warnings = []
            , schemeEvalLoaded = False
            , foreignExports = empty
+           , defsStack = [<]
            }
 
 -- Reset the context, except for the options
@@ -1669,6 +1671,15 @@ setVisibility fc n vis
               | Nothing => undefinedName fc n
          ignore $ addDef n ({ visibility := specified vis } def)
 
+export
+withDefStacked : {auto c : Ref Ctxt Defs} ->
+                 Name -> Core a -> Core a
+withDefStacked n act
+    = do defs <- get Ctxt
+         let ds = defs.defsStack
+         put Ctxt $ {defsStack $= (:< n)} defs
+         act <* update Ctxt {defsStack := ds}
+
 public export
 record SearchData where
   constructor MkSearchData

src/Core/Reflect.idr

@@ -276,6 +276,26 @@ Reflect a => Reflect (List1 a) where
            appCon fc defs (NS (mkNamespace "Data.List1")
                   (UN $ Basic ":::")) [Erased fc Placeholder, x', xs']
 
+export
+Reify a => Reify (SnocList a) where
+  reify defs val@(NDCon _ n _ _ args)
+      = case (dropAllNS !(full (gamma defs) n), args) of
+             (UN (Basic "Lin"), _) => pure [<]
+             (UN (Basic ":<"), [_, (_, sx), (_, x)])
+                  => do sx' <- reify defs !(evalClosure defs sx)
+                        x' <- reify defs !(evalClosure defs x)
+                        pure (sx' :< x')
+             _ => cantReify val "SnocList"
+  reify defs val = cantReify val "SnocList"
+
+export
+Reflect a => Reflect (SnocList a) where
+  reflect fc defs lhs env [<] = appCon fc defs (basics "Lin") [Erased fc Placeholder]
+  reflect fc defs lhs env (sx :< x)
+      = do sx' <- reflect fc defs lhs env sx
+           x' <- reflect fc defs lhs env x
+           appCon fc defs (basics ":<") [Erased fc Placeholder, sx', x']
+
 export
 Reify a => Reify (Maybe a) where
   reify defs val@(NDCon _ n _ _ args)

src/TTImp/Elab/RunElab.idr

@@ -299,6 +299,9 @@ elabScript rig fc nest env script@(NDCon nfc nm t ar args) exp
                  | Nothing => failWith defs $ show dn ++ " is not a definition"
              ns <- deepRefersTo def
              scriptRet ns
+    elabCon defs "GetCurrentFn" []
+        = do defs <- get Ctxt
+             scriptRet defs.defsStack
     elabCon defs "Declare" [d]
         = do d' <- evalClosure defs d
              decls <- reify defs d'

src/TTImp/ProcessDef.idr

@@ -978,7 +978,8 @@ processDef : {vars : _} ->
              List ElabOpt -> NestedNames vars -> Env Term vars -> FC ->
              Name -> List ImpClause -> Core ()
 processDef opts nest env fc n_in cs_in
-    = do n <- inCurrentNS n_in
+  = do n <- inCurrentNS n_in
+       withDefStacked n $ do
          defs <- get Ctxt
          Just gdef <- lookupOrAddAlias opts nest env fc n cs_in
            | Nothing => noDeclaration fc n

tests/idris2/reflection/reflection025/CurrFn.idr

@@ -0,0 +1,37 @@
+module CurrFn
+
+import Language.Reflection
+
+%default total
+
+%language ElabReflection
+
+logCurrFn : Elab ()
+logCurrFn = logMsg "elab" 0 "current fn: \{show !getCurrentFn}"
+
+%runElab logCurrFn
+
+f : Nat -> Nat
+f x = case %runElab logCurrFn of () => x + 4
+
+f' : Nat -> Nat
+f' x = x + case %runElab logCurrFn of () => 4
+
+f'' : Nat -> Nat
+f'' Z     = 4
+f'' (S x) = f $ case %runElab logCurrFn of () => x
+
+f''' : Nat -> Nat
+f''' x = case x of
+           Z   => 4
+           S x => f $ case %runElab logCurrFn of () => x
+
+n : Nat -> Nat
+n x = x + f x where
+  f : Nat -> Nat
+  f x = case %runElab logCurrFn of () => x + 4
+
+w : Nat -> Nat
+w x with (x + 5)
+  _ | Z   = x + case %runElab logCurrFn of () => 4
+  _ | S n = f $ case %runElab logCurrFn of () => n

tests/idris2/reflection/reflection025/InspectRec.idr

@@ -0,0 +1,61 @@
+module InspectRec
+
+import Control.Monad.Writer
+
+import Language.Reflection
+
+%default total
+
+%language ElabReflection
+
+isFunc : NameInfo -> Bool
+isFunc $ MkNameInfo Func = True
+isFunc _                 = False
+
+inspectRec : Elaboration m => (desc : String) -> a -> m a
+inspectRec desc val = do
+  expr <- quote val
+  fns <- getCurrentFn
+  let _ : Monoid Bool := Any
+  rec <- execWriterT $ flip mapMTTImp expr $ \case
+           e@(IVar fc nm) => do
+             is <- getInfo nm
+             let is = fst <$> filter (isFunc . snd) is
+             refs <- map join $ for is $ \n => (n::) <$> getReferredFns n
+             tell $ any (\fn => any (==fn) refs) fns
+             pure e
+           e => pure e
+  logMsg "elab" 0 "case \{desc}: \{the String $ if rec then "recursive" else "non-recursive"}"
+  pure val
+
+----------------------------------------------
+
+dec : Nat -> Nat
+dec Z     = %runElab inspectRec "zero case" 0
+dec (S n) = %runElab inspectRec "non-zero case" n
+
+----------------------------------------------
+
+simpleRec : Nat -> Nat
+simpleRec Z     = %runElab inspectRec "base case" 10
+simpleRec (S n) = %runElab inspectRec "next cast" $ simpleRec n
+
+----------------------------------------------
+
+mutualRec1 : Nat -> Nat
+mutualRec2 : Nat -> Nat
+
+mutualRec1 Z     = %runElab inspectRec "mutual rec 1, base" 11
+mutualRec1 (S n) = %runElab inspectRec "mutual rec 1, next" $ mutualRec2 n
+
+mutualRec2 Z     = %runElab inspectRec "mutual rec 2, base" 12
+mutualRec2 (S n) = %runElab inspectRec "mutual rec 2, next" $ mutualRec1 n
+
+----------------------------------------------
+
+nestedMutRec1 : Nat -> Nat
+nestedMutRec1 Z     = %runElab inspectRec "nestedMut rec 1, base" 11
+nestedMutRec1 (S n) = %runElab inspectRec "nestedMut rec 1, next" $ nestedMutRec2 n where
+  nestedMutRec2 : Nat -> Nat
+  nestedMutRec2 Z     = %runElab inspectRec "nestedMut rec 2, base" 12
+  nestedMutRec2 (S n) = %runElab inspectRec "nestedMut rec 2, next" $ nestedMutRec1 n

tests/idris2/reflection/reflection025/RefDefs.idr

@@ -22,6 +22,7 @@ mutRec1 (S n) = mutRec2 n
 mutRec2 Z = Z
 mutRec2 (S n) = mutRec1 n
 
+export
 printRefDefs : Name -> Elab ()
 printRefDefs name = do
   [(name, _)] <- getInfo name

tests/idris2/reflection/reflection025/RefDefsDeep.idr

@@ -0,0 +1,51 @@
+module RefDefsDeep
+
+import Language.Reflection
+
+import RefDefs
+
+%default total
+
+%language ElabReflection
+
+logCurrFn : Elab ()
+logCurrFn = do
+  currFn <- getCurrentFn
+  logMsg "elab" 0 "=== current fn: \{show currFn} ==="
+
+%runElab logCurrFn
+
+f : Nat -> Nat
+f x = case %runElab logCurrFn of () => x + 4
+
+f' : Nat -> Nat
+f' x = x + case %runElab logCurrFn of () => 4
+
+f'' : Nat -> Nat
+f'' Z     = 4
+f'' (S x) = f $ case %runElab logCurrFn of () => x
+
+f''' : Nat -> Nat
+f''' x = case x of
+           Z   => 4
+           S x => f $ case %runElab logCurrFn of () => x
+
+n : Nat -> Nat
+n x = x + f x where
+  f : Nat -> Nat
+  f x = case %runElab logCurrFn of () => x + 4
+
+w : Nat -> Nat
+w x with (x + 5)
+  _ | Z   = x + case %runElab logCurrFn of () => 4
+  _ | S n = f $ case %runElab logCurrFn of () => n
+
+%runElab
+  traverse_ printRefDefs
+    [ `{f}
+    , `{f'}
+    , `{f''}
+    , `{f'''}
+    , `{n}
+    , `{w}
+    ]