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

Operations for universe levels.
-}
{-# LANGUAGE ForeignFunctionInterface #-}
{-# LANGUAGE Trustworthy #-}
module Language.Lean.Univ
  ( Univ
  , zeroUniv
  , succUniv
  , maxUniv
  , imaxUniv
  , paramUniv
  , globalUniv
  , metaUniv
  , explicitUniv
  , UnivView(..)
  , univView
  , showUniv
  , showUnivUsing
    -- * Operations on universe levels
  , normalizeUniv
  , instantiateUniv
  , instantiateUniv2
  , univGeq
  , univLt
  ) where

import Foreign
import Foreign.C
import System.IO.Unsafe

import Language.Lean.List
import Language.Lean.Internal.Exception
{-# LINE 38 "src/Language/Lean/Univ.chs" #-}

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

import Language.Lean.Internal.Univ
{-# LINE 41 "src/Language/Lean/Univ.chs" #-}









------------------------------------------------------------------------
-- Operations for constructing universes

-- | The zero universe
zeroUniv :: Univ
zeroUniv = tryGetLeanValue $ lean_univ_mk_zero

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

{-# LINE 58 "src/Language/Lean/Univ.chs" #-}


-- | Successor of the universe
succUniv :: Univ -> Univ
succUniv x = tryGetLeanValue $ lean_univ_mk_succ x

lean_univ_mk_succ :: (Univ) -> (OutUnivPtr) -> (OutExceptionPtr) -> IO ((Bool))
lean_univ_mk_succ a1 a2 a3 =
  (withUniv) a1 $ \a1' -> 
  let {a2' = id a2} in 
  let {a3' = id a3} in 
  lean_univ_mk_succ'_ a1' a2' a3' >>= \res ->
  let {res' = toBool res} in
  return (res')

{-# LINE 65 "src/Language/Lean/Univ.chs" #-}


-- | The max of two universes.
maxUniv :: Univ -> Univ -> Univ
maxUniv x y = tryGetLeanValue $ lean_univ_mk_max x y

lean_univ_mk_max :: (Univ) -> (Univ) -> (OutUnivPtr) -> (OutExceptionPtr) -> IO ((Bool))
lean_univ_mk_max a1 a2 a3 a4 =
  (withUniv) a1 $ \a1' -> 
  (withUniv) a2 $ \a2' -> 
  let {a3' = id a3} in 
  let {a4' = id a4} in 
  lean_univ_mk_max'_ a1' a2' a3' a4' >>= \res ->
  let {res' = toBool res} in
  return (res')

{-# LINE 72 "src/Language/Lean/Univ.chs" #-}


-- | The imax of two universes.
imaxUniv :: Univ -> Univ -> Univ
imaxUniv x y = tryGetLeanValue $ lean_univ_mk_imax x y

lean_univ_mk_imax :: (Univ) -> (Univ) -> (OutUnivPtr) -> (OutExceptionPtr) -> IO ((Bool))
lean_univ_mk_imax a1 a2 a3 a4 =
  (withUniv) a1 $ \a1' -> 
  (withUniv) a2 $ \a2' -> 
  let {a3' = id a3} in 
  let {a4' = id a4} in 
  lean_univ_mk_imax'_ a1' a2' a3' a4' >>= \res ->
  let {res' = toBool res} in
  return (res')

{-# LINE 79 "src/Language/Lean/Univ.chs" #-}


-- | A universe parameter of the given name.
paramUniv :: Name -> Univ
paramUniv x = tryGetLeanValue $ lean_univ_mk_param x

lean_univ_mk_param :: (Name) -> (OutUnivPtr) -> (OutExceptionPtr) -> IO ((Bool))
lean_univ_mk_param a1 a2 a3 =
  (withName) a1 $ \a1' -> 
  let {a2' = id a2} in 
  let {a3' = id a3} in 
  lean_univ_mk_param'_ a1' a2' a3' >>= \res ->
  let {res' = toBool res} in
  return (res')

{-# LINE 86 "src/Language/Lean/Univ.chs" #-}


-- | A global universe with the given name.
globalUniv :: Name -> Univ
globalUniv x = tryGetLeanValue $ lean_univ_mk_global x

lean_univ_mk_global :: (Name) -> (OutUnivPtr) -> (OutExceptionPtr) -> IO ((Bool))
lean_univ_mk_global a1 a2 a3 =
  (withName) a1 $ \a1' -> 
  let {a2' = id a2} in 
  let {a3' = id a3} in 
  lean_univ_mk_global'_ a1' a2' a3' >>= \res ->
  let {res' = toBool res} in
  return (res')

{-# LINE 93 "src/Language/Lean/Univ.chs" #-}


-- | A universe meta-variable with the given name.
metaUniv :: Name -> Univ
metaUniv x = tryGetLeanValue $ lean_univ_mk_meta x

lean_univ_mk_meta :: (Name) -> (OutUnivPtr) -> (OutExceptionPtr) -> IO ((Bool))
lean_univ_mk_meta a1 a2 a3 =
  (withName) a1 $ \a1' -> 
  let {a2' = id a2} in 
  let {a3' = id a3} in 
  lean_univ_mk_meta'_ a1' a2' a3' >>= \res ->
  let {res' = toBool res} in
  return (res')

{-# LINE 100 "src/Language/Lean/Univ.chs" #-}


-- | Create an explicit universe level
explicitUniv :: Integer -> Univ
explicitUniv i0 | i0 < 0 = error "Universes cannot be negative."
                | otherwise = go zeroUniv i0
  where -- Make sure first argument is evaluated
        go r _ | seq r False = error "unexpected"
        go r 0 = r
        go r i = go (succUniv r) (i-1)

------------------------------------------------------------------------
-- View

-- | A view of a universe.
data UnivView
   = UnivZero
     -- ^ The zero universe.
   | UnivSucc !Univ
     -- ^ Successor of the previous universe.
   | UnivMax !Univ !Univ
     -- ^ Maximum of two universes.
   | UnivIMax !Univ !Univ
     -- ^ @UnivIMax x y@ denotes @y@ if @y@ is universe zero, otherwise @UnivMax x y@
   | UnivParam !Name
     -- ^ Universe parameter with the given name.
   | UnivGlobal !Name
     -- ^ Reference to a global universe.
   | UnivMeta !Name
     -- ^ Meta variable with the given name.
  deriving (Eq, Ord, Show)

-- | Create a view of the universe.
univView :: Univ -> UnivView
univView x =
  case lean_univ_get_kind x of
   LEAN_UNIV_ZERO -> UnivZero
   LEAN_UNIV_SUCC -> UnivSucc (tryGetLeanValue $ lean_univ_get_pred x)
   LEAN_UNIV_MAX ->
     UnivMax (tryGetLeanValue $ lean_univ_get_max_lhs x)
             (tryGetLeanValue $ lean_univ_get_max_rhs x)
   LEAN_UNIV_IMAX ->
     UnivIMax (tryGetLeanValue $ lean_univ_get_max_lhs x)
              (tryGetLeanValue $ lean_univ_get_max_rhs x)
   LEAN_UNIV_PARAM  -> UnivParam  (tryGetLeanValue $ lean_univ_get_name x)
   LEAN_UNIV_GLOBAL -> UnivGlobal (tryGetLeanValue $ lean_univ_get_name x)
   LEAN_UNIV_META   -> UnivMeta   (tryGetLeanValue $ lean_univ_get_name x)

data UnivKind = LEAN_UNIV_ZERO
              | LEAN_UNIV_SUCC
              | LEAN_UNIV_MAX
              | LEAN_UNIV_IMAX
              | LEAN_UNIV_PARAM
              | LEAN_UNIV_GLOBAL
              | LEAN_UNIV_META
  deriving (Enum,Eq)

{-# LINE 149 "src/Language/Lean/Univ.chs" #-}


lean_univ_get_kind :: (Univ) -> (UnivKind)
lean_univ_get_kind a1 =
  unsafePerformIO $
  (withUniv) a1 $ \a1' -> 
  let {res = lean_univ_get_kind'_ a1'} in
  let {res' = (toEnum . fromIntegral) res} in
  return (res')

{-# LINE 152 "src/Language/Lean/Univ.chs" #-}


lean_univ_get_pred :: (Univ) -> (OutUnivPtr) -> (OutExceptionPtr) -> IO ((Bool))
lean_univ_get_pred a1 a2 a3 =
  (withUniv) a1 $ \a1' -> 
  let {a2' = id a2} in 
  let {a3' = id a3} in 
  lean_univ_get_pred'_ a1' a2' a3' >>= \res ->
  let {res' = toBool res} in
  return (res')

{-# LINE 155 "src/Language/Lean/Univ.chs" #-}


lean_univ_get_max_lhs :: (Univ) -> (OutUnivPtr) -> (OutExceptionPtr) -> IO ((Bool))
lean_univ_get_max_lhs a1 a2 a3 =
  (withUniv) a1 $ \a1' -> 
  let {a2' = id a2} in 
  let {a3' = id a3} in 
  lean_univ_get_max_lhs'_ a1' a2' a3' >>= \res ->
  let {res' = toBool res} in
  return (res')

{-# LINE 158 "src/Language/Lean/Univ.chs" #-}


lean_univ_get_max_rhs :: (Univ) -> (OutUnivPtr) -> (OutExceptionPtr) -> IO ((Bool))
lean_univ_get_max_rhs a1 a2 a3 =
  (withUniv) a1 $ \a1' -> 
  let {a2' = id a2} in 
  let {a3' = id a3} in 
  lean_univ_get_max_rhs'_ a1' a2' a3' >>= \res ->
  let {res' = toBool res} in
  return (res')

{-# LINE 161 "src/Language/Lean/Univ.chs" #-}


lean_univ_get_name :: (Univ) -> (OutNamePtr) -> (OutExceptionPtr) -> IO ((Bool))
lean_univ_get_name a1 a2 a3 =
  (withUniv) a1 $ \a1' -> 
  let {a2' = id a2} in 
  let {a3' = id a3} in 
  lean_univ_get_name'_ a1' a2' a3' >>= \res ->
  let {res' = toBool res} in
  return (res')

{-# LINE 164 "src/Language/Lean/Univ.chs" #-}


-- | @geqUniv x y@ returns @true@ if @y@ is a larger universe level
-- than @x@ for all possible assignments to the variables in the
-- @x@ and @y@.
univGeq :: Univ -> Univ -> Bool
univGeq x y = tryGetLeanValue $ lean_univ_geq x y

lean_univ_geq :: (Univ) -> (Univ) -> (Ptr CInt) -> (OutExceptionPtr) -> IO ((Bool))
lean_univ_geq a1 a2 a3 a4 =
  (withUniv) a1 $ \a1' -> 
  (withUniv) a2 $ \a2' -> 
  let {a3' = id a3} in 
  let {a4' = id a4} in 
  lean_univ_geq'_ a1' a2' a3' a4' >>= \res ->
  let {res' = toBool res} in
  return (res')

{-# LINE 177 "src/Language/Lean/Univ.chs" #-}



------------------------------------------------------------------------
-- Normalize

lean_univ_normalize :: (Univ) -> (OutUnivPtr) -> (OutExceptionPtr) -> IO ((Bool))
lean_univ_normalize a1 a2 a3 =
  (withUniv) a1 $ \a1' -> 
  let {a2' = id a2} in 
  let {a3' = id a3} in 
  lean_univ_normalize'_ a1' a2' a3' >>= \res ->
  let {res' = toBool res} in
  return (res')

{-# LINE 187 "src/Language/Lean/Univ.chs" #-}


-- | Return the normal form for a universe.
normalizeUniv :: Univ -> Univ
normalizeUniv x = tryGetLeanValue $ lean_univ_normalize x

------------------------------------------------------------------------
-- Instantiate

-- | Instantiate the parameters with universes
instantiateUniv :: Univ -> [(Name,Univ)] -> Univ
instantiateUniv u bindings =
  instantiateUniv2 u (fromList (fst <$> bindings)) (fromList (snd <$> bindings))

-- | Instantiate the parameters with universes using separate lists for names and levels.
instantiateUniv2 :: Univ
                 -> List Name
                 -> List Univ
                 -> Univ
instantiateUniv2 u nms args = tryGetLeanValue $ lean_univ_instantiate u nms args

lean_univ_instantiate :: (Univ) -> (ListName) -> (ListUniv) -> (OutUnivPtr) -> (OutExceptionPtr) -> IO ((Bool))
lean_univ_instantiate a1 a2 a3 a4 a5 =
  (withUniv) a1 $ \a1' -> 
  (withListName) a2 $ \a2' -> 
  (withListUniv) a3 $ \a3' -> 
  let {a4' = id a4} in 
  let {a5' = id a5} in 
  lean_univ_instantiate'_ a1' a2' a3' a4' a5' >>= \res ->
  let {res' = toBool res} in
  return (res')

{-# LINE 214 "src/Language/Lean/Univ.chs" #-}


foreign import ccall unsafe "Language/Lean/Univ.chs.h lean_univ_mk_zero"
  lean_univ_mk_zero'_ :: ((OutUnivPtr) -> ((OutExceptionPtr) -> (IO CInt)))

foreign import ccall unsafe "Language/Lean/Univ.chs.h lean_univ_mk_succ"
  lean_univ_mk_succ'_ :: ((UnivPtr) -> ((OutUnivPtr) -> ((OutExceptionPtr) -> (IO CInt))))

foreign import ccall unsafe "Language/Lean/Univ.chs.h lean_univ_mk_max"
  lean_univ_mk_max'_ :: ((UnivPtr) -> ((UnivPtr) -> ((OutUnivPtr) -> ((OutExceptionPtr) -> (IO CInt)))))

foreign import ccall unsafe "Language/Lean/Univ.chs.h lean_univ_mk_imax"
  lean_univ_mk_imax'_ :: ((UnivPtr) -> ((UnivPtr) -> ((OutUnivPtr) -> ((OutExceptionPtr) -> (IO CInt)))))

foreign import ccall unsafe "Language/Lean/Univ.chs.h lean_univ_mk_param"
  lean_univ_mk_param'_ :: ((NamePtr) -> ((OutUnivPtr) -> ((OutExceptionPtr) -> (IO CInt))))

foreign import ccall unsafe "Language/Lean/Univ.chs.h lean_univ_mk_global"
  lean_univ_mk_global'_ :: ((NamePtr) -> ((OutUnivPtr) -> ((OutExceptionPtr) -> (IO CInt))))

foreign import ccall unsafe "Language/Lean/Univ.chs.h lean_univ_mk_meta"
  lean_univ_mk_meta'_ :: ((NamePtr) -> ((OutUnivPtr) -> ((OutExceptionPtr) -> (IO CInt))))

foreign import ccall unsafe "Language/Lean/Univ.chs.h lean_univ_get_kind"
  lean_univ_get_kind'_ :: ((UnivPtr) -> CInt)

foreign import ccall unsafe "Language/Lean/Univ.chs.h lean_univ_get_pred"
  lean_univ_get_pred'_ :: ((UnivPtr) -> ((OutUnivPtr) -> ((OutExceptionPtr) -> (IO CInt))))

foreign import ccall unsafe "Language/Lean/Univ.chs.h lean_univ_get_max_lhs"
  lean_univ_get_max_lhs'_ :: ((UnivPtr) -> ((OutUnivPtr) -> ((OutExceptionPtr) -> (IO CInt))))

foreign import ccall unsafe "Language/Lean/Univ.chs.h lean_univ_get_max_rhs"
  lean_univ_get_max_rhs'_ :: ((UnivPtr) -> ((OutUnivPtr) -> ((OutExceptionPtr) -> (IO CInt))))

foreign import ccall unsafe "Language/Lean/Univ.chs.h lean_univ_get_name"
  lean_univ_get_name'_ :: ((UnivPtr) -> ((OutNamePtr) -> ((OutExceptionPtr) -> (IO CInt))))

foreign import ccall unsafe "Language/Lean/Univ.chs.h lean_univ_geq"
  lean_univ_geq'_ :: ((UnivPtr) -> ((UnivPtr) -> ((Ptr CInt) -> ((OutExceptionPtr) -> (IO CInt)))))

foreign import ccall unsafe "Language/Lean/Univ.chs.h lean_univ_normalize"
  lean_univ_normalize'_ :: ((UnivPtr) -> ((OutUnivPtr) -> ((OutExceptionPtr) -> (IO CInt))))

foreign import ccall unsafe "Language/Lean/Univ.chs.h lean_univ_instantiate"
  lean_univ_instantiate'_ :: ((UnivPtr) -> ((ListNamePtr) -> ((ListUnivPtr) -> ((OutUnivPtr) -> ((OutExceptionPtr) -> (IO CInt))))))