-- GENERATED by C->Haskell Compiler, version 0.25.2 Snowboundest, 31 Oct 2014 (Haskell)
-- Edit the ORIGNAL .chs file instead!


{-# LINE 1 "src/Language/Lean/Module.chs" #-}
{-|
Module      : Language.Lean.Module
Copyright   : (c) Galois Inc, 2015
License     : Apache-2
Maintainer  : jhendrix@galois.com, lcasburn@galois.com

Declarations for importing and exporting modules and accessing Lean paths
-}
{-# LANGUAGE ForeignFunctionInterface #-}
{-# LANGUAGE Trustworthy #-}
module Language.Lean.Module
  ( envImport
  , envExport
  , stdPath
  , hottPath
  ) where

import Foreign
import Foreign.C

import Language.Lean.List

import Language.Lean.Internal.Decl
{-# LINE 23 "src/Language/Lean/Module.chs" #-}

import Language.Lean.Internal.Exception
{-# LINE 24 "src/Language/Lean/Module.chs" #-}

import Language.Lean.Internal.Exception.Unsafe
import Language.Lean.Internal.Name
{-# LINE 26 "src/Language/Lean/Module.chs" #-}

import Language.Lean.Internal.IOS
{-# LINE 27 "src/Language/Lean/Module.chs" #-}

import Language.Lean.Internal.String
{-# LINE 28 "src/Language/Lean/Module.chs" #-}













-- | Import the given module names into the lean environment
envImport :: IOState tp -> Env -> List Name -> IO Env
envImport s e names = tryAllocLeanValue $ lean_env_import e (someIOS s) names

lean_env_import :: (Env) -> (SomeIOState) -> (ListName) -> (OutEnvPtr) -> (OutExceptionPtr) -> IO ((Bool))
lean_env_import a1 a2 a3 a4 a5 =
  (withEnv) a1 $ \a1' -> 
  (withSomeIOState) a2 $ \a2' -> 
  (withListName) a3 $ \a3' -> 
  let {a4' = id a4} in 
  let {a5' = id a5} in 
  lean_env_import'_ a1' a2' a3' a4' a5' >>= \res ->
  let {res' = toBool res} in
  return (res')

{-# LINE 51 "src/Language/Lean/Module.chs" #-}


-- | Export the lean environment to a path.
envExport :: Env -> FilePath -> IO ()
envExport e path = runLeanPartialAction $ lean_env_export e path

lean_env_export :: (Env) -> (String) -> (OutExceptionPtr) -> IO ((Bool))
lean_env_export a1 a2 a3 =
  (withEnv) a1 $ \a1' -> 
  withLeanStringPtr a2 $ \a2' -> 
  let {a3' = id a3} in 
  lean_env_export'_ a1' a2' a3' >>= \res ->
  let {res' = toBool res} in
  return (res')

{-# LINE 61 "src/Language/Lean/Module.chs" #-}


-- | Path to lean standard library (extracted from LEAN_PATH)
stdPath :: String
stdPath = tryGetLeanValue $ lean_get_std_path

lean_get_std_path :: (Ptr CString) -> (OutExceptionPtr) -> IO ((Bool))
lean_get_std_path a1 a2 =
  let {a1' = id a1} in 
  let {a2' = id a2} in 
  lean_get_std_path'_ a1' a2' >>= \res ->
  let {res' = toBool res} in
  return (res')

{-# LINE 68 "src/Language/Lean/Module.chs" #-}


-- | Path to lean hott library (extrcted from HLEAN_PATH)
hottPath :: String
hottPath = tryGetLeanValue $ lean_get_hott_path

lean_get_hott_path :: (Ptr CString) -> (OutExceptionPtr) -> IO ((Bool))
lean_get_hott_path a1 a2 =
  let {a1' = id a1} in 
  let {a2' = id a2} in 
  lean_get_hott_path'_ a1' a2' >>= \res ->
  let {res' = toBool res} in
  return (res')

{-# LINE 75 "src/Language/Lean/Module.chs" #-}


foreign import ccall safe "Language/Lean/Module.chs.h lean_env_import"
  lean_env_import'_ :: ((EnvPtr) -> ((Ptr (SomeIOState)) -> ((ListNamePtr) -> ((OutEnvPtr) -> ((OutExceptionPtr) -> (IO CInt))))))

foreign import ccall safe "Language/Lean/Module.chs.h lean_env_export"
  lean_env_export'_ :: ((EnvPtr) -> ((Ptr CChar) -> ((OutExceptionPtr) -> (IO CInt))))

foreign import ccall unsafe "Language/Lean/Module.chs.h lean_get_std_path"
  lean_get_std_path'_ :: ((Ptr (Ptr CChar)) -> ((OutExceptionPtr) -> (IO CInt)))

foreign import ccall unsafe "Language/Lean/Module.chs.h lean_get_hott_path"
  lean_get_hott_path'_ :: ((Ptr (Ptr CChar)) -> ((OutExceptionPtr) -> (IO CInt)))