-- 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/Env.chs" #-}
{-|
Module      : Language.Lean.Env
Copyright   : (c) Galois Inc, 2015
License     : Apache-2
Maintainer  : jhendrix@galois.com, lcasburn@galois.com

Operations for working with Lean environments.
-}
{-# LANGUAGE DoAndIfThenElse #-}
{-# LANGUAGE ForeignFunctionInterface #-}
{-# LANGUAGE GeneralizedNewtypeDeriving #-}
{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE Trustworthy #-}
module Language.Lean.Env
  ( Env
  , TrustLevel
  , trustHigh
    -- * Constructing and manipulating environments.
  , standardEnv
  , hottEnv
  , envAddUniv
  , envAddDecl
  , envReplaceAxiom
    -- * Projections
  , envTrustLevel
  , envContainsProofIrrelProp
  , envIsImpredicative
  , envContainsDecl
  , envLookupDecl
  , envContainsUniv
  , envIsDescendant
    -- * Operations
  , envForget
  , envDecls
  , forEnvDecl_
  , envUnivs
  , forEnvUniv_
  ) where

import Control.Exception (bracket)
import Control.Lens
import Control.Monad
import Data.IORef
import Foreign
import Foreign.C
import System.IO.Unsafe

import Language.Lean.Internal.Decl
{-# LINE 48 "src/Language/Lean/Env.chs" #-}

import Language.Lean.Internal.Exception
{-# LINE 49 "src/Language/Lean/Env.chs" #-}

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












-- | Function prototype to wrap a Lean function that visits arguments.
type WrapLeanVisitFn p = (p -> IO ()) -> IO (FunPtr (p -> IO ()))

-- | Prototype for function that
type LeanFoldFn s p = s -> FunPtr (p -> IO ()) -> OutExceptionPtr -> IO Bool

runLeanFold :: IsLeanValue a p
            => WrapLeanVisitFn p
            -> LeanFoldFn s p
            -> Fold s a
runLeanFold wrapFn foldFn h e = unsafePerformIO $ do
  -- Create reference for storing result, the initial value is pure.
  ref <- newIORef $! (coerce $! pure ())

  let g d_ptr = do
        d <- mkLeanValue d_ptr
        cur_val <- readIORef ref
        let hd = h d
        let chd = coerce hd
        seq hd $ seq chd $ do
        writeIORef ref $! cur_val *> chd

  -- Create function pointer for callback.
  bracket (wrapFn g) freeHaskellFunPtr $ \g_ptr -> do
    alloca $ \ex_ptr -> do
      success <- foldFn e g_ptr ex_ptr
      if success then
        readIORef ref
      else
        throwLeanException =<< peek ex_ptr
{-# INLINABLE runLeanFold #-}

safeRunLeanFold :: IsLeanValue a p
                => WrapLeanVisitFn p
                -> LeanFoldFn s p
                -> (a -> IO ())
                -> (s -> IO ())
safeRunLeanFold wrapFn foldFn f s = do
  let g = mkLeanValue >=> f

  -- Create function pointer for callback.
  bracket (wrapFn g) freeHaskellFunPtr $ \g_ptr -> do
    alloca $ \ex_ptr -> do
      success <- foldFn s g_ptr ex_ptr
      unless success $ do
        throwLeanException =<< peek ex_ptr
{-# INLINABLE safeRunLeanFold #-}

------------------------------------------------------------------------
-- Trust level

-- | The level of trust associated with an environment.
newtype TrustLevel = TrustLevel { _trustValue :: Word32 }
  deriving (Eq, Ord, Num, Show)

-- | Create a trust level from a unsigned C integer.
trustFromUInt :: CUInt -> TrustLevel
trustFromUInt = TrustLevel . fromIntegral

-- | Get the trust level as a unsigned C integer.
trustUInt :: TrustLevel -> CUInt
trustUInt (TrustLevel u) = fromIntegral u

-- | Trust level for all macros implemented in Lean.
trustHigh :: TrustLevel
trustHigh = TrustLevel 100000
{-# LINE 128 "src/Language/Lean/Env.chs" #-}


------------------------------------------------------------------------
-- Env constructors

-- | Create an empty standard environment with the given trust level.
standardEnv :: TrustLevel -> Env
standardEnv lvl = tryGetLeanValue $ lean_env_mk_std lvl

lean_env_mk_std :: (TrustLevel) -> (OutEnvPtr) -> (OutExceptionPtr) -> IO ((Bool))
lean_env_mk_std a1 a2 a3 =
  let {a1' = trustUInt a1} in 
  let {a2' = id a2} in 
  let {a3' = id a3} in 
  lean_env_mk_std'_ a1' a2' a3' >>= \res ->
  let {res' = toBool res} in
  return (res')

{-# LINE 141 "src/Language/Lean/Env.chs" #-}


-- | Create an empty hott environment with the given trust level.
hottEnv :: TrustLevel -> Env
hottEnv lvl = tryGetLeanValue $ lean_env_mk_hott lvl

lean_env_mk_hott :: (TrustLevel) -> (OutEnvPtr) -> (OutExceptionPtr) -> IO ((Bool))
lean_env_mk_hott a1 a2 a3 =
  let {a1' = trustUInt a1} in 
  let {a2' = id a2} in 
  let {a3' = id a3} in 
  lean_env_mk_hott'_ a1' a2' a3' >>= \res ->
  let {res' = toBool res} in
  return (res')

{-# LINE 151 "src/Language/Lean/Env.chs" #-}


-- | Add a new global universe with the given name.
envAddUniv :: Name -> Env -> Env
envAddUniv u e = tryGetLeanValue $ lean_env_add_univ e u

lean_env_add_univ :: (Env) -> (Name) -> (OutEnvPtr) -> (OutExceptionPtr) -> IO ((Bool))
lean_env_add_univ a1 a2 a3 a4 =
  (withEnv) a1 $ \a1' -> 
  (withName) a2 $ \a2' -> 
  let {a3' = id a3} in 
  let {a4' = id a4} in 
  lean_env_add_univ'_ a1' a2' a3' a4' >>= \res ->
  let {res' = toBool res} in
  return (res')

{-# LINE 162 "src/Language/Lean/Env.chs" #-}


-- | Adding the given certified declaration to the environment.
envAddDecl :: CertDecl -> Env -> Env
envAddDecl d e = tryGetLeanValue $ lean_env_add e d

lean_env_add :: (Env) -> (CertDecl) -> (OutEnvPtr) -> (OutExceptionPtr) -> IO ((Bool))
lean_env_add a1 a2 a3 a4 =
  (withEnv) a1 $ \a1' -> 
  (withCertDecl) a2 $ \a2' -> 
  let {a3' = id a3} in 
  let {a4' = id a4} in 
  lean_env_add'_ a1' a2' a3' a4' >>= \res ->
  let {res' = toBool res} in
  return (res')

{-# LINE 173 "src/Language/Lean/Env.chs" #-}


-- |  Replace the axiom that has the name of the given certified declaration with the
-- certified declaration.
--
-- This procedure throws an exception if
--
--  * The theorem was certified in an environment which is not an ancestor of the environment.
--  * The environment does not contain an axiom with the given name.
envReplaceAxiom :: CertDecl -> Env -> Env
envReplaceAxiom d e = tryGetLeanValue $ lean_env_replace e d

lean_env_replace :: (Env) -> (CertDecl) -> (OutEnvPtr) -> (OutExceptionPtr) -> IO ((Bool))
lean_env_replace a1 a2 a3 a4 =
  (withEnv) a1 $ \a1' -> 
  (withCertDecl) a2 $ \a2' -> 
  let {a3' = id a3} in 
  let {a4' = id a4} in 
  lean_env_replace'_ a1' a2' a3' a4' >>= \res ->
  let {res' = toBool res} in
  return (res')

{-# LINE 190 "src/Language/Lean/Env.chs" #-}


------------------------------------------------------------------------
-- Env Projections

-- | The trust level of the given environment.
envTrustLevel :: Env -> TrustLevel
envTrustLevel = lean_env_trust_level

lean_env_trust_level :: (Env) -> (TrustLevel)
lean_env_trust_level a1 =
  unsafePerformIO $
  (withEnv) a1 $ \a1' -> 
  let {res = lean_env_trust_level'_ a1'} in
  let {res' = trustFromUInt res} in
  return (res')

{-# LINE 200 "src/Language/Lean/Env.chs" #-}


-- | Return @true@ if the given environment has a proof irrelevant Prop such as
-- @Type.{0}@.
envContainsProofIrrelProp :: (Env) -> (Bool)
envContainsProofIrrelProp a1 =
  unsafePerformIO $
  (withEnv) a1 $ \a1' -> 
  let {res = envContainsProofIrrelProp'_ a1'} in
  let {res' = toBool res} in
  return (res')

{-# LINE 205 "src/Language/Lean/Env.chs" #-}


-- | Return @true@ iff in the given environment @Prop@ is impredicative.
envIsImpredicative :: (Env) -> (Bool)
envIsImpredicative a1 =
  unsafePerformIO $
  (withEnv) a1 $ \a1' -> 
  let {res = envIsImpredicative'_ a1'} in
  let {res' = toBool res} in
  return (res')

{-# LINE 209 "src/Language/Lean/Env.chs" #-}


-- |  Return @true@ iff the environment contains a global universe with the name.
envContainsUniv :: (Env) -> (Name) -> (Bool)
envContainsUniv a1 a2 =
  unsafePerformIO $
  (withEnv) a1 $ \a1' -> 
  (withName) a2 $ \a2' -> 
  let {res = envContainsUniv'_ a1' a2'} in
  let {res' = toBool res} in
  return (res')

{-# LINE 213 "src/Language/Lean/Env.chs" #-}


-- |  Return @true@ iff the environment contains a declaration with the name.
envContainsDecl :: (Env) -> (Name) -> (Bool)
envContainsDecl a1 a2 =
  unsafePerformIO $
  (withEnv) a1 $ \a1' -> 
  (withName) a2 $ \a2' -> 
  let {res = envContainsDecl'_ a1' a2'} in
  let {res' = toBool res} in
  return (res')

{-# LINE 217 "src/Language/Lean/Env.chs" #-}


-- |  Lookup the declaration with the given name in the environment.
envLookupDecl :: Name -> Env -> Maybe Decl
envLookupDecl nm e =
  if envContainsDecl e nm then
    Just (tryGetLeanValue $ lean_env_get_decl e nm)
  else
    Nothing

-- |  Return the declaration with the given name in the environment if any.
lean_env_get_decl :: (Env) -> (Name) -> (OutDeclPtr) -> (OutExceptionPtr) -> IO ((Bool))
lean_env_get_decl a1 a2 a3 a4 =
  (withEnv) a1 $ \a1' -> 
  (withName) a2 $ \a2' -> 
  let {a3' = id a3} in 
  let {a4' = id a4} in 
  lean_env_get_decl'_ a1' a2' a3' a4' >>= \res ->
  let {res' = toBool res} in
  return (res')

{-# LINE 229 "src/Language/Lean/Env.chs" #-}


-- | @x `'envIsDescendant'` y@ return true @x@ is a descendant of @y@, that is, @x@
-- was created by adding declarations to @y@.
envIsDescendant :: Env -> Env -> Bool
envIsDescendant = lean_env_is_descendant

lean_env_is_descendant :: (Env) -> (Env) -> (Bool)
lean_env_is_descendant a1 a2 =
  unsafePerformIO $
  (withEnv) a1 $ \a1' -> 
  (withEnv) a2 $ \a2' -> 
  let {res = lean_env_is_descendant'_ a1' a2'} in
  let {res' = toBool res} in
  return (res')

{-# LINE 237 "src/Language/Lean/Env.chs" #-}


------------------------------------------------------------------------
-- envForget

-- | Return a new environment, where its "history" has been truncated/forgotten.
-- That is, @envForget x `envIsDescendant` y@ will return false for any environment
-- @y@ that is not pointer equal to the result @envForget x@.
envForget :: Env -> Env
envForget x = tryGetLeanValue $ lean_env_forget x

-- |  Return the declaration with the given name in the environment if any.
lean_env_forget :: (Env) -> (OutEnvPtr) -> (OutExceptionPtr) -> IO ((Bool))
lean_env_forget a1 a2 a3 =
  (withEnv) a1 $ \a1' -> 
  let {a2' = id a2} in 
  let {a3' = id a3} in 
  lean_env_forget'_ a1' a2' a3' >>= \res ->
  let {res' = toBool res} in
  return (res')

{-# LINE 250 "src/Language/Lean/Env.chs" #-}


------------------------------------------------------------------------
-- foldEnvDecls

-- | A fold over the declaration in the environment.
envDecls :: Fold Env Decl
envDecls = runLeanFold wrapDeclVisitFn lean_env_for_each_decl

-- | Run an IO action on each declaration in the environment.
forEnvDecl_ :: Env -> (Decl -> IO ()) -> IO ()
forEnvDecl_ e f = safeRunLeanFold wrapDeclVisitFn lean_env_for_each_decl f e

foreign import ccall "wrapper" wrapDeclVisitFn :: WrapLeanVisitFn DeclPtr

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

{-# LINE 269 "src/Language/Lean/Env.chs" #-}


------------------------------------------------------------------------
-- foldEnvUnivs

-- | Fold over the global universes in the environment.
envUnivs :: Fold Env Name
envUnivs = runLeanFold wrapNameVisitFn lean_env_for_each_univ

-- | Run an IO action on each universe in the environment.
forEnvUniv_ :: Env -> (Name -> IO ()) -> IO ()
forEnvUniv_ e f = safeRunLeanFold wrapNameVisitFn lean_env_for_each_univ f e


foreign import ccall "wrapper" wrapNameVisitFn :: WrapLeanVisitFn NamePtr

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

{-# LINE 289 "src/Language/Lean/Env.chs" #-}


foreign import ccall unsafe "Language/Lean/Env.chs.h lean_env_mk_std"
  lean_env_mk_std'_ :: (CUInt -> ((OutEnvPtr) -> ((OutExceptionPtr) -> (IO CInt))))

foreign import ccall unsafe "Language/Lean/Env.chs.h lean_env_mk_hott"
  lean_env_mk_hott'_ :: (CUInt -> ((OutEnvPtr) -> ((OutExceptionPtr) -> (IO CInt))))

foreign import ccall unsafe "Language/Lean/Env.chs.h lean_env_add_univ"
  lean_env_add_univ'_ :: ((EnvPtr) -> ((NamePtr) -> ((OutEnvPtr) -> ((OutExceptionPtr) -> (IO CInt)))))

foreign import ccall unsafe "Language/Lean/Env.chs.h lean_env_add"
  lean_env_add'_ :: ((EnvPtr) -> ((CertDeclPtr) -> ((OutEnvPtr) -> ((OutExceptionPtr) -> (IO CInt)))))

foreign import ccall unsafe "Language/Lean/Env.chs.h lean_env_replace"
  lean_env_replace'_ :: ((EnvPtr) -> ((CertDeclPtr) -> ((OutEnvPtr) -> ((OutExceptionPtr) -> (IO CInt)))))

foreign import ccall unsafe "Language/Lean/Env.chs.h lean_env_trust_level"
  lean_env_trust_level'_ :: ((EnvPtr) -> CUInt)

foreign import ccall unsafe "Language/Lean/Env.chs.h lean_env_proof_irrel"
  envContainsProofIrrelProp'_ :: ((EnvPtr) -> CInt)

foreign import ccall unsafe "Language/Lean/Env.chs.h lean_env_impredicative"
  envIsImpredicative'_ :: ((EnvPtr) -> CInt)

foreign import ccall unsafe "Language/Lean/Env.chs.h lean_env_contains_univ"
  envContainsUniv'_ :: ((EnvPtr) -> ((NamePtr) -> CInt))

foreign import ccall unsafe "Language/Lean/Env.chs.h lean_env_contains_decl"
  envContainsDecl'_ :: ((EnvPtr) -> ((NamePtr) -> CInt))

foreign import ccall unsafe "Language/Lean/Env.chs.h lean_env_get_decl"
  lean_env_get_decl'_ :: ((EnvPtr) -> ((NamePtr) -> ((OutDeclPtr) -> ((OutExceptionPtr) -> (IO CInt)))))

foreign import ccall unsafe "Language/Lean/Env.chs.h lean_env_is_descendant"
  lean_env_is_descendant'_ :: ((EnvPtr) -> ((EnvPtr) -> CInt))

foreign import ccall unsafe "Language/Lean/Env.chs.h lean_env_forget"
  lean_env_forget'_ :: ((EnvPtr) -> ((OutEnvPtr) -> ((OutExceptionPtr) -> (IO CInt))))

foreign import ccall safe "Language/Lean/Env.chs.h lean_env_for_each_decl"
  lean_env_for_each_decl'_ :: ((EnvPtr) -> ((FunPtr ((DeclPtr) -> (IO ()))) -> ((OutExceptionPtr) -> (IO CInt))))

foreign import ccall safe "Language/Lean/Env.chs.h lean_env_for_each_univ"
  lean_env_for_each_univ'_ :: ((EnvPtr) -> ((FunPtr ((NamePtr) -> (IO ()))) -> ((OutExceptionPtr) -> (IO CInt))))