diff --git a/CHANGELOG.md b/CHANGELOG.md
index 66b5ee0c77..a4941be8b6 100644
--- a/CHANGELOG.md
+++ b/CHANGELOG.md
@@ -20,6 +20,8 @@
 * New `fromTTImp`, `fromName`, and `fromDecls` names for custom `TTImp`,
   `Name`, and `Decls` literals.
 * Call to `%macro`-functions do not require the `ElabReflection` extension.
+* Elaborator scripts were made to be able to access project files,
+  allowing the support for type providers and similar stuff.
 
 ### REPL changes
 
diff --git a/libs/base/Language/Reflection.idr b/libs/base/Language/Reflection.idr
index 512c576053..97ab3b361d 100644
--- a/libs/base/Language/Reflection.idr
+++ b/libs/base/Language/Reflection.idr
@@ -11,6 +11,23 @@ import public Control.Monad.Trans
 --- Elaboration data structure ---
 ----------------------------------
 
+public export
+data LookupDir =
+  ||| The dir of the `ipkg`-file, or the current dir if there is no one
+  ProjectDir |
+  ||| The source dir set in the `ipkg`-file, or the current dir if there is no one
+  SourceDir |
+  ||| The dir where the current module is located
+  |||
+  ||| For the module `Language.Reflection` it would be `<source_dir>/Language/`
+  CurrentModuleDir |
+  ||| The dir where submodules of the current module are located
+  |||
+  ||| For the module `Language.Reflection` it would be `<source_dir>/Language/Reflection/`
+  SubmodulesDir |
+  ||| The dir where built files are located, set in the `ipkg`-file and defaulted to `build`
+  BuildDir
+
 ||| Elaboration scripts
 ||| Where types/terms are returned, binders will have unique, if not
 ||| necessarily human readabe, names
@@ -73,6 +90,13 @@ data Elab : Type -> Type where
      -- Check a group of top level declarations
      Declare : List Decl -> Elab ()
 
+     -- Read the contents of a file, if it is present
+     ReadFile : LookupDir -> (path : String) -> Elab $ Maybe String
+     -- Writes to a file, replacing existing contents, if were present
+     WriteFile : LookupDir -> (path : String) -> (contents : String) -> Elab ()
+     -- Returns the specified type of dir related to the current idris project
+     IdrisDir : LookupDir -> Elab String
+
 export
 Functor Elab where
   map f e = Bind e $ Pure . f
@@ -148,7 +172,7 @@ interface Monad m => Elaboration m where
   ||| Given a possibly ambiguous name, get all the matching names and their types
   getType : Name -> m (List (Name, TTImp))
 
-  ||| Get the metadata associated with a name. Returns all matching namea and their types
+  ||| Get the metadata associated with a name. Returns all matching names and their types
   getInfo : Name -> m (List (Name, NameInfo))
 
   ||| Get the type of a local variable
@@ -160,6 +184,15 @@ interface Monad m => Elaboration m where
   ||| Make some top level declarations
   declare : List Decl -> m ()
 
+  ||| Read the contents of a file, if it is present
+  readFile : LookupDir -> (path : String) -> m $ Maybe String
+
+  ||| Writes to a file, replacing existing contents, if were present
+  writeFile : LookupDir -> (path : String) -> (contents : String) -> m ()
+
+  ||| Returns the specified type of dir related to the current idris project
+  idrisDir : LookupDir -> m String
+
 export %inline
 ||| Report an error in elaboration
 fail : Elaboration m => String -> m a
@@ -195,6 +228,9 @@ Elaboration Elab where
   getLocalType   = GetLocalType
   getCons        = GetCons
   declare        = Declare
+  readFile       = ReadFile
+  writeFile      = WriteFile
+  idrisDir       = IdrisDir
 
 public export
 Elaboration m => MonadTrans t => Monad (t m) => Elaboration (t m) where
@@ -216,6 +252,9 @@ Elaboration m => MonadTrans t => Monad (t m) => Elaboration (t m) where
   getLocalType        = lift . getLocalType
   getCons             = lift . getCons
   declare             = lift . declare
+  readFile            = lift .: readFile
+  writeFile d         = lift .: writeFile d
+  idrisDir            = lift . idrisDir
 
 ||| Catch failures and use the `Maybe` monad instead
 export
diff --git a/src/Core/Name/Namespace.idr b/src/Core/Name/Namespace.idr
index 1e8f8f7b21..7e683b5ef0 100644
--- a/src/Core/Name/Namespace.idr
+++ b/src/Core/Name/Namespace.idr
@@ -124,6 +124,11 @@ namespace ModuleIdent
   toPath : ModuleIdent -> String
   toPath = joinPath . reverse . unsafeUnfoldModuleIdent
 
+  export
+  parent : ModuleIdent -> Maybe ModuleIdent
+  parent (MkMI (_::rest)) = Just $ MkMI rest
+  parent _ = Nothing
+
 -------------------------------------------------------------------------------------
 -- HIERARCHICAL STRUCTURE
 -------------------------------------------------------------------------------------
diff --git a/src/TTImp/Elab/RunElab.idr b/src/TTImp/Elab/RunElab.idr
index 05515a3d56..4158990107 100644
--- a/src/TTImp/Elab/RunElab.idr
+++ b/src/TTImp/Elab/RunElab.idr
@@ -3,6 +3,7 @@ module TTImp.Elab.RunElab
 import Core.Context
 import Core.Context.Log
 import Core.Core
+import Core.Directory
 import Core.Env
 import Core.Metadata
 import Core.Normalise
@@ -16,6 +17,8 @@ import Idris.Resugar
 import Idris.REPL.Opts
 import Idris.Syntax
 
+import Libraries.Utils.Path
+
 import TTImp.Elab.Check
 import TTImp.Elab.Delayed
 import TTImp.Reflect
@@ -23,6 +26,8 @@ import TTImp.TTImp
 import TTImp.TTImp.Functor
 import TTImp.Unelab
 
+import System.File.Meta
+
 %default covering
 
 record NameInfo where
@@ -85,6 +90,47 @@ elabScript rig fc nest env script@(NDCon nfc nm t ar args) exp
       EmptyFC => fc
       x       => x
 
+    -- parses and resolves `Language.Reflection.LookupDir`
+    lookupDir : Defs -> NF vars -> Core String
+    lookupDir defs (NDCon _ conName _ _ [])
+        = do defs <- get Ctxt
+             NS ns (UN (Basic n)) <- toFullNames conName
+               | fnm => failWith defs $ "bad lookup dir fullnames " ++ show fnm
+             let True = ns == reflectionNS
+               | False => failWith defs $ "bad lookup dir namespace " ++ show ns
+             let wd = defs.options.dirs.working_dir
+             let sd = maybe wd (\sd => joinPath [wd, sd]) defs.options.dirs.source_dir
+             let modDir : Bool -> Core String := \doParent => do
+                            syn <- get Syn
+                            let parentIfNeeded = if doParent then parent else pure
+                            let moduleSuffix = toList $ (head' syn.saveMod >>= parentIfNeeded) <&> toPath
+                            pure $ joinPath $ sd :: moduleSuffix
+             case n of
+               "ProjectDir"       => pure wd
+               "SourceDir"        => pure sd
+               "CurrentModuleDir" => modDir True
+               "SubmodulesDir"    => modDir False
+               "BuildDir"         => pure $ joinPath [wd, defs.options.dirs.build_dir]
+               _ => failWith defs $ "bad lookup dir value"
+    lookupDir defs lk
+        = do defs <- get Ctxt
+             empty <- clearDefs defs
+             throw (BadRunElab fc env !(quote empty env lk) "lookup dir is not a data value")
+
+    validatePath : Defs -> String -> Core ()
+    validatePath defs path = do
+      let True = isRelative path
+        | False => failWith defs $ "path must be relative"
+      let True = pathDoesNotEscape 0 $ splitPath path
+        | False => failWith defs $ "path must not escape the directory"
+      pure ()
+      where
+        pathDoesNotEscape : (depth : Nat) -> List String -> Bool
+        pathDoesNotEscape _     []           = True
+        pathDoesNotEscape Z     (".."::rest) = False
+        pathDoesNotEscape (S n) (".."::rest) = pathDoesNotEscape n rest
+        pathDoesNotEscape n     (_   ::rest) = pathDoesNotEscape (S n) rest
+
     elabCon : Defs -> String -> List (Closure vars) -> Core (NF vars)
     elabCon defs "Pure" [_,val]
         = do empty <- clearDefs defs
@@ -228,6 +274,26 @@ elabScript rig fc nest env script@(NDCon nfc nm t ar args) exp
              decls <- reify defs d'
              traverse_ (processDecl [] (MkNested []) []) decls
              scriptRet ()
+    elabCon defs "ReadFile" [lk, pth]
+        = do pathPrefix <- lookupDir defs !(evalClosure defs lk)
+             path <- reify defs !(evalClosure defs pth)
+             validatePath defs path
+             let fullPath = joinPath [pathPrefix, path]
+             True <- coreLift $ exists fullPath
+               | False => scriptRet $ Nothing {ty=String}
+             contents <- readFile fullPath
+             scriptRet $ Just contents
+    elabCon defs "WriteFile" [lk, pth, contents]
+        = do pathPrefix <- lookupDir defs !(evalClosure defs lk)
+             path <- reify defs !(evalClosure defs pth)
+             validatePath defs path
+             contents <- reify defs !(evalClosure defs contents)
+             let fullPath = joinPath [pathPrefix, path]
+             whenJust (parent fullPath) ensureDirectoryExists
+             writeFile fullPath contents
+             scriptRet ()
+    elabCon defs "IdrisDir" [lk]
+        = do evalClosure defs lk >>= lookupDir defs >>= scriptRet
     elabCon defs n args = failWith defs $ "unexpected Elab constructor " ++ n ++
                                           ", or incorrect count of arguments: " ++ show (length args)
 elabScript rig fc nest env script exp
diff --git a/tests/idris2/reflection/reflection024/.gitignore b/tests/idris2/reflection/reflection024/.gitignore
new file mode 100644
index 0000000000..ddbaeea8c5
--- /dev/null
+++ b/tests/idris2/reflection/reflection024/.gitignore
@@ -0,0 +1,3 @@
+src/*xistent*
+src/..a-dot-named-file
+src/another-fancy-record.json
diff --git a/tests/idris2/reflection/reflection024/expected b/tests/idris2/reflection/reflection024/expected
new file mode 100644
index 0000000000..8da12f7b0c
--- /dev/null
+++ b/tests/idris2/reflection/reflection024/expected
@@ -0,0 +1,61 @@
+--- Print dirs with ipkg ---
+1/1: Building Inside.PrintDirs (src/Inside/PrintDirs.idr)
+LOG elab:0: project dir: __TEST_DIR__
+LOG elab:0: source dir: __TEST_DIR__/src
+LOG elab:0: current module dir: __TEST_DIR__/src/Inside
+LOG elab:0: submodules dir: __TEST_DIR__/src/Inside/PrintDirs
+LOG elab:0: build dir: __TEST_DIR__/build
+
+--- Print dirs with ipkg (with changed pwd) ---
+1/1: Building Inside.PrintDirs (src/Inside/PrintDirs.idr)
+LOG elab:0: project dir: __TEST_DIR__
+LOG elab:0: source dir: __TEST_DIR__/src
+LOG elab:0: current module dir: __TEST_DIR__/src/Inside
+LOG elab:0: submodules dir: __TEST_DIR__/src/Inside/PrintDirs
+LOG elab:0: build dir: __TEST_DIR__/build
+
+--- Print dirs without ipkg (with changed pwd) ---
+1/1: Building Inside.PrintDirs (Inside/PrintDirs.idr)
+LOG elab:0: project dir: __TEST_DIR__
+LOG elab:0: source dir: __TEST_DIR__
+LOG elab:0: current module dir: __TEST_DIR__/Inside
+LOG elab:0: submodules dir: __TEST_DIR__/Inside/PrintDirs
+LOG elab:0: build dir: __TEST_DIR__/build
+
+--- Simple reads and writes ---
+1/1: Building SimpleRW (src/SimpleRW.idr)
+LOG elab:0: reading existentToRead:
+LOG elab:0:     contents:
+existent to read
+second line
+
+LOG elab:0: reading nonExistentToRead:
+LOG elab:0:     FILE DOES NOT EXIST
+LOG elab:0: written to existentToWrite
+LOG elab:0: written to nonExistentToWrite
+existent to read
+second line
+cat: src/nonExistentToRead: No such file or directory
+WRITTEN CONTENTS
+LA-LA-LA
+WRITTEN CONTENTS
+LA-LA-LA
+
+--- A little but less simple reads and writes ---
+1/1: Building LessSimpleRW (src/LessSimpleRW.idr)
+LOG elab:0: written to nonExistentOriginally/a-generated-file
+LOG elab:0: reading nonExistentOriginally/../nonExistentOriginally/a-generated-file:
+LOG elab:0:     contents:
+WRITTEN CONTENTS
+LA-LA-LA
+
+LOG elab:0: written to ..a-dot-named-file
+WRITTEN CONTENTS
+LA-LA-LA
+WRITTEN CONTENTS
+LA-LA-LA
+
+--- Type providers ---
+1/1: Building TypeProviders (src/TypeProviders.idr)
+Derived:
+{"veryStringField":"String","veryIntegerField":"Integer","varyNatField":"Prelude.Types.Nat"}
diff --git a/tests/idris2/reflection/reflection024/run b/tests/idris2/reflection/reflection024/run
new file mode 100755
index 0000000000..823e58d1f4
--- /dev/null
+++ b/tests/idris2/reflection/reflection024/run
@@ -0,0 +1,77 @@
+. ../../../testutils.sh
+
+echo "--- Print dirs with ipkg ---"
+check --find-ipkg src/Inside/PrintDirs.idr | filter_test_dir
+
+##############################
+
+echo
+. ../../../testutils.sh
+
+(
+cd src
+echo "--- Print dirs with ipkg (with changed pwd) ---"
+check --find-ipkg Inside/PrintDirs.idr | filter_test_dir
+)
+
+##############################
+
+echo
+
+(
+cd src
+. ../../../../testutils.sh # this is here because we will pollute with `build` dir here
+echo "--- Print dirs without ipkg (with changed pwd) ---"
+check Inside/PrintDirs.idr | filter_test_dir
+)
+
+##############################
+
+echo
+. ../../../testutils.sh
+
+echo "--- Simple reads and writes ---"
+
+rm -rf src/nonExistent*
+echo "non-overwritten existent to write" > src/existentToWrite
+
+check --find-ipkg src/SimpleRW.idr
+
+cat src/existentToRead
+cat src/nonExistentToRead 2>&1
+cat src/existentToWrite
+cat src/nonExistentToWrite 2>&1
+
+rm -rf src/nonExistent*
+echo "non-overwritten existent to write" > src/existentToWrite
+
+##############################
+
+echo
+. ../../../testutils.sh
+
+echo "--- A little but less simple reads and writes ---"
+
+rm -rf src/nonExistent*
+rm -f src/..a-dot-named-file
+
+check --find-ipkg src/LessSimpleRW.idr
+
+cat src/nonExistentOriginally/a-generated-file 2>&1
+cat src/..a-dot-named-file 2>&1
+
+rm -rf src/nonExistent*
+rm -f src/..a-dot-named-file
+
+##############################
+
+echo
+. ../../../testutils.sh
+
+echo "--- Type providers ---"
+rm -rf src/another-fancy-record.json
+check --find-ipkg src/TypeProviders.idr
+
+echo "Derived:"
+cat src/another-fancy-record.json
+echo
diff --git a/tests/idris2/reflection/reflection024/src/Inside/PrintDirs.idr b/tests/idris2/reflection/reflection024/src/Inside/PrintDirs.idr
new file mode 100644
index 0000000000..1929045909
--- /dev/null
+++ b/tests/idris2/reflection/reflection024/src/Inside/PrintDirs.idr
@@ -0,0 +1,19 @@
+module Inside.PrintDirs
+
+import Language.Reflection
+
+dirs : List (String, LookupDir)
+dirs =
+  [ ("project dir"       , ProjectDir      )
+  , ("source dir"        , SourceDir       )
+  , ("current module dir", CurrentModuleDir)
+  , ("submodules dir"    , SubmodulesDir   )
+  , ("build dir"         , BuildDir        )
+  ]
+
+logAllDirs : Elab ()
+logAllDirs = for_ dirs $ \(msg, lk) => logMsg "elab" 0 "\{msg}: \{!(idrisDir lk)}"
+
+%language ElabReflection
+
+%runElab logAllDirs
diff --git a/tests/idris2/reflection/reflection024/src/LessSimpleRW.idr b/tests/idris2/reflection/reflection024/src/LessSimpleRW.idr
new file mode 100644
index 0000000000..bb6336deb8
--- /dev/null
+++ b/tests/idris2/reflection/reflection024/src/LessSimpleRW.idr
@@ -0,0 +1,37 @@
+module LessSimpleRW
+
+import Language.Reflection
+
+%default total
+
+readAndLog : (path : String) -> Elab ()
+readAndLog path = do
+  v <- readFile CurrentModuleDir path
+  logMsg "elab" 0 "reading \{path}:"
+  logMsg "elab" 0 $ ("    " ++) $ maybe "FILE DOES NOT EXIST" ("contents:\n" ++) v
+
+writeAndLog : (path : String) -> Elab ()
+writeAndLog path = do
+  writeFile CurrentModuleDir path "WRITTEN CONTENTS\nLA-LA-LA\n"
+  logMsg "elab" 0 "written to \{path}"
+
+%language ElabReflection
+
+-- Check that we can write to a dir that was not previously existent
+%runElab writeAndLog "nonExistentOriginally/a-generated-file"
+
+-- Check that '..' in path are okay unless they escape the lookup dir
+%runElab readAndLog "nonExistentOriginally/../nonExistentOriginally/a-generated-file"
+
+-- Check double dots are allowed inside file names
+%runElab writeAndLog "..a-dot-named-file"
+
+failing "path must not escape the directory"
+
+  -- Check that we cannot escape
+  %runElab readAndLog "../whatever"
+
+failing "path must not escape the directory"
+
+  -- Check a slightly more complicated case of escaping
+  %runElab readAndLog "nonExistentOriginally/../../whatever"
diff --git a/tests/idris2/reflection/reflection024/src/SimpleRW.idr b/tests/idris2/reflection/reflection024/src/SimpleRW.idr
new file mode 100644
index 0000000000..315c071dc5
--- /dev/null
+++ b/tests/idris2/reflection/reflection024/src/SimpleRW.idr
@@ -0,0 +1,33 @@
+module SimpleRW
+
+import Language.Reflection
+
+%default total
+
+existentToRead, nonExistentToRead, existentToWrite, nonExistentToWrite : String
+existentToRead     = "existentToRead"
+nonExistentToRead  = "nonExistentToRead"
+existentToWrite    = "existentToWrite"
+nonExistentToWrite = "nonExistentToWrite"
+
+readAndLog : (path : String) -> Elab ()
+readAndLog path = do
+  v <- readFile CurrentModuleDir path
+  logMsg "elab" 0 "reading \{path}:"
+  logMsg "elab" 0 $ ("    " ++) $ maybe "FILE DOES NOT EXIST" ("contents:\n" ++) v
+
+writeAndLog : (path : String) -> Elab ()
+writeAndLog path = do
+  writeFile CurrentModuleDir path "WRITTEN CONTENTS\nLA-LA-LA\n"
+  logMsg "elab" 0 "written to \{path}"
+
+go : Elab ()
+go = do
+  readAndLog existentToRead
+  readAndLog nonExistentToRead
+  writeAndLog existentToWrite
+  writeAndLog nonExistentToWrite
+
+%language ElabReflection
+
+%runElab go
diff --git a/tests/idris2/reflection/reflection024/src/TypeProviders.idr b/tests/idris2/reflection/reflection024/src/TypeProviders.idr
new file mode 100644
index 0000000000..b5acc75907
--- /dev/null
+++ b/tests/idris2/reflection/reflection024/src/TypeProviders.idr
@@ -0,0 +1,74 @@
+||| This module is purely for illustration purposes of the mechanism a-la original type providers
+module TypeProviders
+
+import Data.List1
+
+import Language.JSON.Data
+
+import Language.Reflection
+
+%default total
+
+%language ElabReflection
+
+||| Mode one: source of truth in an external file, so generate Idris definitions using a file
+
+declareRecordFromSimpleText : LookupDir -> (path : String) -> (tyName, consName : Name) -> Elab ()
+declareRecordFromSimpleText lk textPath dataName consName = do
+  let errDesc : Elab String := do pure "text at \{textPath} in \{!(idrisDir lk)}"
+  Just text <- readFile lk textPath
+    | Nothing => do fail "Did not found \{!errDesc}"
+  let fs = lines text
+  fs <- for fs $ \line => case words line of
+          [name, type] => pure (name, type)
+          _ => fail "Expected two strings in line in \{!errDesc}"
+  let dataDecl : Decl = IRecord EmptyFC Nothing Public Nothing $
+                          MkRecord EmptyFC dataName [] [] consName $
+                            fs <&> \(name, type) => do
+                              let (ns, n) = unsnoc $ split (== '.') type
+                              let type = if null ns then UN $ Basic n
+                                           else NS (MkNS $ reverse ns) (UN $ Basic n)
+                              MkIField EmptyFC MW ExplicitArg (UN $ Basic name) (IVar EmptyFC type)
+  declare [dataDecl]
+
+-- Declare a type from a definitions in a file
+%runElab declareRecordFromSimpleText CurrentModuleDir "fancy-record.txt" `{FancyRecord} `{MkFancyRecord}
+
+-- Use newly created data type
+frVal : FancyRecord
+frVal = MkFancyRecord {natField = S Z, boolField = True}
+
+||| Mode two: source of truth in Idris module, so generate an external file by Idris definition
+
+saveRecordToSimpleJSON : LookupDir -> (path : String) -> (type : Name) -> Elab ()
+saveRecordToSimpleJSON lk jsonPath type = do
+  infos <- getInfo type
+  let [(type, _)] = flip filter infos $ \case
+                      (name, MkNameInfo $ TyCon _ _) => True
+                      _                              => False
+    | [] => fail "Did not found any type matching \{show type}"
+    | (_::_) => fail "Too many types matching \{show type}"
+  [con] <- getCons type
+    | [] => fail "Did not found any constructors of \{show type}"
+    | (_::_) => fail "Too many constructors of \{show type}"
+  [(_, conType)] <- getType con
+    | _ => fail "Error while getting the type of constructor \{show con}"
+  args <- unPi conType
+  let args = args <&> map (JString . show)
+  writeFile lk jsonPath $ show $ JObject args
+
+  where
+
+    unPi : TTImp -> Elab $ List (String, TTImp)
+    unPi $ IPi _ MW ExplicitArg (Just $ UN $ Basic nm) ty rest = ((nm, ty) ::) <$> unPi rest
+    unPi $ IPi fc _ _ _ _ _ = failAt fc "Unsupported parameter (we support only omega explicit simply named ones)"
+    unPi _ = pure []
+
+-- Declare a type which would be a source of truth
+record AnotherFancyRecord where
+  veryStringField : String
+  veryIntegerField : Integer
+  varyNatField : Nat
+
+-- Generate an external description to a data type
+%runElab saveRecordToSimpleJSON CurrentModuleDir "another-fancy-record.json" `{AnotherFancyRecord}
diff --git a/tests/idris2/reflection/reflection024/src/existentToRead b/tests/idris2/reflection/reflection024/src/existentToRead
new file mode 100644
index 0000000000..2f83a54454
--- /dev/null
+++ b/tests/idris2/reflection/reflection024/src/existentToRead
@@ -0,0 +1,2 @@
+existent to read
+second line
diff --git a/tests/idris2/reflection/reflection024/src/existentToWrite b/tests/idris2/reflection/reflection024/src/existentToWrite
new file mode 100644
index 0000000000..a75a770286
--- /dev/null
+++ b/tests/idris2/reflection/reflection024/src/existentToWrite
@@ -0,0 +1 @@
+non-overwritten existent to write
diff --git a/tests/idris2/reflection/reflection024/src/fancy-record.txt b/tests/idris2/reflection/reflection024/src/fancy-record.txt
new file mode 100644
index 0000000000..39fa6add12
--- /dev/null
+++ b/tests/idris2/reflection/reflection024/src/fancy-record.txt
@@ -0,0 +1,2 @@
+natField Prelude.Types.Nat
+boolField Bool
diff --git a/tests/idris2/reflection/reflection024/test.ipkg b/tests/idris2/reflection/reflection024/test.ipkg
new file mode 100644
index 0000000000..86bdfc4b73
--- /dev/null
+++ b/tests/idris2/reflection/reflection024/test.ipkg
@@ -0,0 +1,5 @@
+package a-test
+
+sourcedir = "src"
+
+depends = contrib