[ new ] bindings for System.Environment (#1347)

Author: gallais

CHANGELOG.md

@@ -123,6 +123,8 @@ New modules
   Algebra.Properties.CommutativeSemigroup.Divisibility
   ```
 
+* Added bindings for Haskell's `System.Environment`
+
 Other major changes
 -------------------
 

GenerateEverything.hs

@@ -41,6 +41,8 @@ unsafeModules = map modToFile
   , "IO"
   , "IO.Primitive"
   , "Relation.Binary.PropositionalEquality.TrustMe"
+  , "System.Environment"
+  , "System.Environment.Primitive"
   , "Text.Pretty.Core"
   , "Text.Pretty"
   ]

src/Foreign/Haskell/Coerce.agda

@@ -39,7 +39,7 @@ import IO.Primitive    as STD
 import Data.List.Base  as STD
 import Data.Maybe.Base as STD
 import Data.Product    as STD
-import Data.Sum        as STD
+import Data.Sum.Base   as STD
 
 import Foreign.Haskell.Maybe  as FFI
 import Foreign.Haskell.Pair   as FFI

src/IO.agda

@@ -69,6 +69,9 @@ module _ {a b} {A : Set a} {B : Set b} where
   mapM′ : (A → IO B) → Colist A → IO ⊤
   mapM′ f = sequence′ ∘ map f
 
+ignore : ∀ {a} {A : Set a} → IO A → IO ⊤
+ignore io = ♯ io >> ♯ return _
+
 ------------------------------------------------------------------------
 -- Simple lazy IO
 
@@ -94,33 +97,25 @@ readFiniteFile : String → IO String
 readFiniteFile f = lift (Prim.readFiniteFile f)
 
 writeFile∞ : String → Costring → IO ⊤
-writeFile∞ f s =
-  ♯ lift (Prim.writeFile f s) >>
-  ♯ return _
+writeFile∞ f s = ignore (lift (Prim.writeFile f s))
 
 writeFile : String → String → IO ⊤
 writeFile f s = writeFile∞ f (toCostring s)
 
 appendFile∞ : String → Costring → IO ⊤
-appendFile∞ f s =
-  ♯ lift (Prim.appendFile f s) >>
-  ♯ return _
+appendFile∞ f s = ignore (lift (Prim.appendFile f s))
 
 appendFile : String → String → IO ⊤
 appendFile f s = appendFile∞ f (toCostring s)
 
 putStr∞ : Costring → IO ⊤
-putStr∞ s =
-  ♯ lift (Prim.putStr s) >>
-  ♯ return _
+putStr∞ s = ignore (lift (Prim.putStr s))
 
 putStr : String → IO ⊤
 putStr s = putStr∞ (toCostring s)
 
 putStrLn∞ : Costring → IO ⊤
-putStrLn∞ s =
-  ♯ lift (Prim.putStrLn s) >>
-  ♯ return _
+putStrLn∞ s = ignore (lift (Prim.putStrLn s))
 
 putStrLn : String → IO ⊤
 putStrLn s = putStrLn∞ (toCostring s)

src/System/Environment.agda

@@ -0,0 +1,43 @@
+------------------------------------------------------------------------
+-- The Agda standard library
+--
+-- Miscellanous information about the system environment
+------------------------------------------------------------------------
+
+{-# OPTIONS --without-K #-}
+
+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 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)

src/System/Environment/Primitive.agda

@@ -0,0 +1,47 @@
+------------------------------------------------------------------------
+-- The Agda standard library
+--
+-- Primitive System.Environment: simple bindings to Haskell functions
+--
+-- Note that we currently leave out:
+-- * filepath-related functions (until we have a good representation of
+--   absolute vs. relative & directory vs. file)
+-- * functions that may fail with an exception
+--   e.g. we provide `lookupEnv` but not `getEnv`
+------------------------------------------------------------------------
+
+{-# OPTIONS --without-K #-}
+
+module System.Environment.Primitive where
+
+open import IO.Primitive using (IO)
+open import Data.List.Base using (List)
+open import Data.String.Base using (String)
+open import Data.Unit using (⊤)
+
+open import Foreign.Haskell.Maybe using (Maybe)
+open import Foreign.Haskell.Pair using (Pair)
+
+{-# FOREIGN GHC import qualified System.Environment as SE #-}
+{-# FOREIGN GHC import qualified Data.Text          as T  #-}
+{-# FOREIGN GHC import Data.Bifunctor (bimap)             #-}
+{-# FOREIGN GHC import Data.Function (on)                 #-}
+
+postulate
+  getArgs        : IO (List String)
+  getProgName    : IO String
+  lookupEnv      : String → IO (Maybe String)
+  setEnv         : String → String → IO ⊤
+  unsetEnv       : String → IO ⊤
+  withArgs       : ∀ {a} {A : Set a} → List String → IO A → IO A
+  withProgName   : ∀ {a} {A : Set a} → String → IO A → IO A
+  getEnvironment : IO (List (Pair String String))
+
+{-# COMPILE GHC getArgs        = fmap (fmap T.pack) SE.getArgs #-}
+{-# COMPILE GHC getProgName    = fmap T.pack SE.getProgName #-}
+{-# COMPILE GHC lookupEnv      = fmap (fmap T.pack) . SE.lookupEnv . T.unpack #-}
+{-# COMPILE GHC setEnv         = SE.setEnv `on` T.unpack #-}
+{-# COMPILE GHC unsetEnv       = SE.unsetEnv . T.unpack #-}
+{-# COMPILE GHC withArgs       = \ _ _ -> SE.withArgs . fmap T.unpack #-}
+{-# COMPILE GHC withProgName   = \ _ _ -> SE.withProgName . T.unpack #-}
+{-# COMPILE GHC getEnvironment = fmap (fmap (bimap T.pack T.pack)) SE.getEnvironment #-}