[ refactor ] Typed environment variables

Author: spcfox

micropack/micropack.rkt

@@ -7,6 +7,7 @@ import Idris.Package.Types
 import Pack.CmdLn
 import Pack.Config.TOML
 import Pack.Config.Types
+import public Pack.Config.Environment.Variable
 import Pack.Core
 import Pack.Database
 import System
@@ -267,43 +268,27 @@ bootstrapCmd = if useRacket then "bootstrap-racket" else "bootstrap"
 --          Environment Variables
 --------------------------------------------------------------------------------
 
-%inline
-mkEnvVar : Interpolation a => String -> a -> String
-mkEnvVar var val = "\{var}=\{val}"
-
-export %inline
-mkPrefixVar :  Path Abs -> String
-mkPrefixVar = mkEnvVar "PREFIX"
-
-export %inline
-mkIdrisBootVar : File Abs -> String
-mkIdrisBootVar = mkEnvVar "IDRIS2_BOOT"
-
-export %inline
-mkIdrisDataVar : Path Abs -> String
-mkIdrisDataVar = mkEnvVar "IDRIS2_DATA"
 
 ||| `$PREFIX` variable during Idris2 installation, unquoted
 export
-prefixVar : PackDirs => DB => String
-prefixVar = mkPrefixVar idrisPrefixDir
+prefixVar : PackDirs => DB => EnvVar
+prefixVar = PrefixVar idrisPrefixDir
 
 ||| `$IDRIS2_BOOT` variable during Idris2 installation, unquoted
 export
-idrisBootVar : PackDirs => DB => String
-idrisBootVar = mkIdrisBootVar idrisExec
+idrisBootVar : PackDirs => DB => EnvVar
+idrisBootVar = IdrisBootVar idrisExec
 
 ||| `$SCHEME` variable during Idris2 installation, unquoted
 export
-schemeVar : (c : Config) => String
-schemeVar = if useRacket then mkEnvVar "IDRIS2_CG" "racket" else mkEnvVar "SCHEME" c.scheme
+schemeVar : (c : Config) => EnvVar
+schemeVar = if useRacket then IdrisCGVar Racket else SchemeVar c.scheme
 
 ||| `IDRIS2_PREFIX` to be used with Idris when installing a library
 ||| to a custom location.
 export
-libInstallPrefix : PackDirs => DB => ResolvedLib t -> List (String,String)
-libInstallPrefix rl =
-  [("IDRIS2_PREFIX", "\{pkgPrefixDir rl.name rl.hash rl.pkg}")]
+libInstallPrefix : PackDirs => DB => ResolvedLib t -> List EnvVar
+libInstallPrefix rl = [IdrisPrefixVar $ pkgPrefixDir rl.name rl.hash rl.pkg]
 
 ||| Idris executable with extra arguments, if they are present in the config.
 export

micropack/micropack.ss

@@ -0,0 +1,35 @@
+module Pack.Config.Environment.Variable
+
+import public Data.FilePath.File
+import Pack.Config.Types
+
+public export
+data EnvVar : Type where
+  PrefixVar : Path Abs -> EnvVar
+  IdrisPrefixVar : Path Abs -> EnvVar
+  IdrisBootVar : File Abs -> EnvVar
+  IdrisDataVar : List (Path Abs) -> EnvVar
+  IdrisCGVar : Codegen -> EnvVar
+  IdrisPackagePathVar : List (Path Abs) -> EnvVar
+  IdrisLibsVar : List (Path Abs) -> EnvVar
+  SchemeVar : FilePath -> EnvVar
+
+%inline
+interpolateEnvVar : Interpolation a => String -> a -> String
+interpolateEnvVar var val = "\{var}=\{val}"
+
+export %inline
+Interpolation (List (Path Abs)) where
+  interpolate = fastConcat . intersperse ":" . map interpolate
+
+export %inline
+Interpolation EnvVar where
+  interpolate (PrefixVar p) = interpolateEnvVar "PREFIX" p
+  interpolate (IdrisPrefixVar p) = interpolateEnvVar "IDRIS2_PREFIX" p
+  interpolate (IdrisBootVar p) = interpolateEnvVar "IDRIS2_BOOT" p
+  interpolate (IdrisDataVar p) = interpolateEnvVar "IDRIS2_DATA" p
+  interpolate (IdrisCGVar p) = interpolateEnvVar "IDRIS2_CG" p
+  interpolate (IdrisPackagePathVar p) = interpolateEnvVar "IDRIS2_PACKAGE_PATH" p
+  interpolate (IdrisLibsVar p) = interpolateEnvVar "IDRIS2_LIBS" p
+  interpolate (SchemeVar p) = interpolateEnvVar "SCHEME" p
+

src/Pack/Config/Environment.idr

@@ -1,6 +1,7 @@
 module Pack.Core.IO
 
 import public Control.Monad.Either
+import Pack.Config.Environment.Variable
 import Pack.Config.Types
 import Pack.Core.Logging
 import Pack.Core.Types
@@ -67,8 +68,8 @@ run (MkEitherT io) = io >>= either fatal pure
 ||| Display a list of variable-value pairs in the format
 ||| `VAR1="val1" VAR2="val2"`.
 export
-dispEnv : List (String,String) -> String
-dispEnv = unwords . map (\(e,v) => "\{e}=\{quote v}")
+dispEnv : List EnvVar -> String
+dispEnv = unwords . map interpolate
 
 ||| Tries to run a system command.
 export
@@ -104,7 +105,7 @@ sysAndLog lvl cmd = do
     | n => throwE (Sys cmd n)
   pure ()
 
-cmdWithEnv : CmdArgList -> List (String,String) -> String
+cmdWithEnv : CmdArgList -> List EnvVar -> String
 cmdWithEnv cmd []  = escapeCmd cmd
 cmdWithEnv cmd env = "\{dispEnv env} \{escapeCmd cmd}"
 
@@ -120,7 +121,7 @@ export
 sysWithEnv :
      {auto _ : HasIO io}
   -> (cmd : CmdArgList)
-  -> (env : List (String,String))
+  -> (env : List EnvVar)
   -> EitherT PackErr io ()
 sysWithEnv cmd env = do
   0 <- system (cmdWithEnv cmd env) | n => throwE (Sys cmd n)
@@ -132,7 +133,7 @@ sysWithEnvAndLog :
   -> {auto _ : Env}
   -> (lvl : LogLevel)
   -> (cmd : CmdArgList)
-  -> (env : List (String,String))
+  -> (env : List EnvVar)
   -> EitherT PackErr io ()
 sysWithEnvAndLog lvl cmd env = do
   0 <- runProcessingOutput
@@ -160,7 +161,7 @@ export covering
 sysRunWithEnv :
      {auto _ : HasIO io}
   -> (cmd : CmdArgList)
-  -> (env : List (String,String))
+  -> (env : List EnvVar)
   -> EitherT PackErr io String
 sysRunWithEnv cmd env = do
   (res,0) <- System.run (cmdWithEnv cmd env) | (_,n) => throwE (Sys cmd n)

src/Pack/Config/Environment/Variable.idr

@@ -173,9 +173,9 @@ runCmd = do
       (RemoveApp ** [ps])       => idrisEnv mc fetch >>= \e => removeApps ps
       (Update ** [])            => idrisEnv mc fetch >>= update
       (Fetch ** [])             => idrisEnv mc fetch >>= \e => install []
-      (PackagePath ** [])       => env mc fetch >>= packagePathDirs >>= putStrLn
-      (LibsPath ** [])          => env mc fetch >>= packageLibDirs  >>= putStrLn
-      (DataPath ** [])          => env mc fetch >>= packageDataDirs >>= putStrLn
+      (PackagePath ** [])       => env mc fetch >>= packagePathDirs >>= putStrLn . interpolate
+      (LibsPath ** [])          => env mc fetch >>= packageLibDirs  >>= putStrLn . interpolate
+      (DataPath ** [])          => env mc fetch >>= packageDataDirs >>= putStrLn . interpolate
       (AppPath ** [n])          => env mc fetch >>= appPath n
       (Info ** [])              => env mc fetch >>= printInfo
       (New ** [pty,p])          => idrisEnv mc fetch >>= new cd pty p

src/Pack/Core/IO.idr

@@ -21,63 +21,58 @@ pathDirs :
      {auto _ : HasIO io}
   -> {auto _ : PackDirs}
   -> {auto e : Env}
-  -> (pre : String)
+  -> (pre : Path Abs)
   -> (pth : PkgName -> Hash -> Package -> Path Abs)
-  -> EitherT PackErr io String
+  -> EitherT PackErr io (List (Path Abs))
 pathDirs pre pth = do
   rs <- traverse resolveLib (keys e.all)
   ps <- filterM (\r => exists $ pth r.name r.hash r.pkg) rs
   let ps' := filter (not . isCorePkg . value . name) ps
-  pure $
-      fastConcat
-    . intersperse ":"
-    . (pre ::)
-    $ map (\r => "\{pth r.name r.hash r.pkg}") ps'
+  pure $ (pre ::) $ map (\r => pth r.name r.hash r.pkg) ps'
 
 ||| Directories to be listed in the `IDRIS2_PACKAGE_PATH` variable, so
 ||| that Idris finds all libraries installed by pack in custom locations.
 export
-packagePathDirs : HasIO io => Env -> EitherT PackErr io String
-packagePathDirs _ = pathDirs "\{idrisInstallDir}" pkgPathDir
+packagePathDirs : HasIO io => Env -> EitherT PackErr io (List (Path Abs))
+packagePathDirs _ = pathDirs idrisInstallDir pkgPathDir
 
 ||| Directories to be listed in the `IDRIS2_LIBS` variable, so
 ||| that Idris finds all `.so` files installed by pack in custom locations.
 export
-packageLibDirs : HasIO io => Env -> EitherT PackErr io String
-packageLibDirs _ = pathDirs "\{idrisLibDir}" pkgLibDir
+packageLibDirs : HasIO io => Env -> EitherT PackErr io (List (Path Abs))
+packageLibDirs _ = pathDirs idrisLibDir pkgLibDir
 
 ||| Directories to be listed in the `IDRIS2_DATA` variable, so
 ||| that Idris finds all support files installed by pack in custom locations.
 export
-packageDataDirs : HasIO io => Env -> EitherT PackErr io String
-packageDataDirs _ = pathDirs "\{idrisDataDir}" pkgDataDir
+packageDataDirs : HasIO io => Env -> EitherT PackErr io (List (Path Abs))
+packageDataDirs _ = pathDirs idrisDataDir pkgDataDir
 
 ||| `IDRIS2_PACKAGE_PATH` variable to be used with Idris, so
 ||| that it finds all libraries installed by pack in custom locations.
 export
-packagePath : HasIO io => Env => EitherT PackErr io (String, String)
-packagePath =
-  ("IDRIS2_PACKAGE_PATH",) <$>  packagePathDirs %search
+packagePath : HasIO io => Env => EitherT PackErr io EnvVar
+packagePath = IdrisPackagePathVar <$> packagePathDirs %search
 
 ||| `IDRIS2_LIBS` variable to be used with Idris, so
 ||| that it finds all `.so` files installed by pack in custom locations.
 export
-libPath : HasIO io => Env => EitherT PackErr io (String, String)
-libPath = ("IDRIS2_LIBS",) <$> packageLibDirs %search
+libPath : HasIO io => Env => EitherT PackErr io EnvVar
+libPath = IdrisLibsVar <$> packageLibDirs %search
 
 ||| `IDRIS2_DATA` variable to be used with Idris, so
 ||| that it finds all support files installed by pack in custom locations.
 export
-dataPath : HasIO io => Env => EitherT PackErr io (String, String)
-dataPath = ("IDRIS2_DATA",) <$> packageDataDirs %search
+dataPath : HasIO io => Env => EitherT PackErr io EnvVar
+dataPath = IdrisDataVar <$> packageDataDirs %search
 
 ||| This unifies `packagePath`, `libPath` and `dataPath`,
 ||| to generate an environment necessary to build packages with Idris
 ||| the dependencies of which are handled by pack.
 export
-buildEnv : HasIO io => Env => EitherT PackErr io (List (String,String))
+buildEnv : HasIO io => Env => EitherT PackErr io (List EnvVar)
 buildEnv =
-  let pre := if useRacket then [("IDRIS2_CG", "racket")] else []
+  let pre := if useRacket then [IdrisCGVar Racket] else []
    in (pre ++ ) <$> sequence [packagePath, libPath, dataPath]
 
 ||| Idris executable loading the given package plus the
@@ -87,7 +82,7 @@ idrisWithPkg :
      {auto _ : HasIO io}
   -> {auto _ : IdrisEnv}
   -> ResolvedLib t
-  -> EitherT PackErr io (CmdArgList, List (String,String))
+  -> EitherT PackErr io (CmdArgList, List EnvVar)
 idrisWithPkg rl =
   (idrisWithCG ++ ["-p", name rl],) <$> buildEnv
 
@@ -98,7 +93,7 @@ idrisWithPkgs :
      {auto _ : HasIO io}
   -> {auto _ : IdrisEnv}
   -> List (ResolvedLib t)
-  -> EitherT PackErr io (CmdArgList, List (String,String))
+  -> EitherT PackErr io (CmdArgList, List EnvVar)
 idrisWithPkgs [] = pure (idrisWithCG, [])
 idrisWithPkgs pkgs =
   let ps = concatMap (\p => ["-p", name p]) pkgs
@@ -221,7 +216,7 @@ export covering
 libPkg :
      {auto _     : HasIO io}
   -> {auto e     : IdrisEnv}
-  -> (env        : List (String,String))
+  -> (env        : List EnvVar)
   -> (logLevel   : LogLevel)
   -> (cleanBuild : Bool)
   -> (cmd        : CmdArgList)
@@ -276,15 +271,15 @@ idrisCleanup =
 
 idrisBootstrapWithStage3 : HasIO io => (e : Env) => Path Abs -> EitherT PackErr io ()
 idrisBootstrapWithStage3 dir = do
-  let bootstrappedPrefixVar = mkPrefixVar dir
+  let bootstrappedPrefixVar = PrefixVar dir
   sysAndLog Build ["make", bootstrapCmd, bootstrappedPrefixVar, schemeVar]
   debug "Install bootstrapped Idris..."
   sysAndLog Build ["make", "bootstrap-install", bootstrappedPrefixVar, schemeVar]
   idrisCleanup
 
   debug "Stage 3: Rebuilding Idris..."
-  let idrisBootVar = mkIdrisBootVar $ dir /> "bin" /> "idris2"
-  let idrisDataVar = mkIdrisDataVar $ dir /> idrisDir /> "support"
+  let idrisBootVar = IdrisBootVar $ dir /> "bin" /> "idris2"
+  let idrisDataVar = IdrisDataVar [dir /> idrisDir /> "support"]
   sysAndLog Build ["make", "idris2-exec", prefixVar, idrisBootVar, idrisDataVar, schemeVar]
 
   ignoreError $ sysAndLog Build ["rm", "-rf", dir]
@@ -461,7 +456,7 @@ installDocs rl = case rl.status of
     let docsDir : Path Abs
         docsDir = buildPath rl.desc /> "docs"
 
-        pre : List (String,String)
+        pre : List EnvVar
         pre = libInstallPrefix rl
 
         htmlDir : Path Abs