[ elab ] Support limited file operations in elab scripts, e.g. enable type providers

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
 

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

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
 -------------------------------------------------------------------------------------

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,13 +17,17 @@ 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
 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

tests/idris2/reflection/reflection024/.gitignore

@@ -0,0 +1,3 @@
+src/*xistent*
+src/..a-dot-named-file
+src/another-fancy-record.json

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"}

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

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