------------------------------------------------------------------------
-- The Agda standard library
--
-- Miscellanous information about the system environment
------------------------------------------------------------------------

{-# OPTIONS --cubical-compatible --guardedness #-}

module System.Environment where

open import IO using (IO; lift; run; ignore)
open import Data.List.Base using (List)
open import Data.Maybe.Base using (Maybe)
open import Data.Product.Base using (_×_)
open import Data.String.Base using (String)
open import Data.Unit.Polymorphic using (⊤)
open import Foreign.Haskell.Coerce

import System.Environment.Primitive as Prim

getArgs : IO (List String)
getArgs = lift Prim.getArgs

getProgName : IO String
getProgName = lift Prim.getProgName

lookupEnv : String → IO (Maybe String)
lookupEnv var = lift (coerce (Prim.lookupEnv var))

setEnv : String → String → IO ⊤
setEnv var val = ignore (lift (Prim.setEnv var val))

unsetEnv : String → IO ⊤
unsetEnv var = ignore (lift (Prim.unsetEnv var))

withArgs : ∀ {a} {A : Set a} → List String → IO A → IO A
withArgs args io = lift (Prim.withArgs args (run io))

withProgName : ∀ {a} {A : Set a} → String → IO A → IO A
withProgName name io = lift (Prim.withProgName name (run io))

getEnvironment : IO (List (String × String))
getEnvironment = lift (coerce Prim.getEnvironment)