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

Internal declarations for Lean universe values together with typeclass instances
for @Univ@.
-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE ForeignFunctionInterface #-}
{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE Trustworthy #-}
module Language.Lean.Internal.Univ
  ( Univ
  , showUniv
  , showUnivUsing
  , univLt
    -- * Internal Operations
  , UnivPtr
  , OutUnivPtr
  , withUniv
  , ListUniv
  , ListUnivPtr
  , OutListUnivPtr
  , withListUniv
  ) where

import Control.Lens (toListOf)
import Foreign
import Foreign.C
import System.IO.Unsafe

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

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










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


-- | A Lean universe level
newtype Univ = Univ (ForeignPtr Univ)

-- | Function @c2hs@ uses to pass @Univ@ values to Lean
withUniv :: Univ -> (Ptr Univ -> IO a) -> IO a
withUniv (Univ o) = withForeignPtr $! o

-- | Haskell type for @lean_univ@ FFI parameters.
type UnivPtr = Ptr (Univ)
{-# LINE 57 "src/Language/Lean/Internal/Univ.chs" #-}


-- | Haskell type for @lean_univ*@ FFI parameters.
type OutUnivPtr = Ptr (UnivPtr)
{-# LINE 60 "src/Language/Lean/Internal/Univ.chs" #-}


foreign import ccall unsafe "&lean_univ_del"
  lean_univ_del_ptr :: FunPtr (UnivPtr -> IO ())

instance IsLeanValue Univ (Ptr Univ) where
  mkLeanValue = fmap Univ . newForeignPtr lean_univ_del_ptr

------------------------------------------------------------------------
-- Equality and comparison of universes.

instance Eq Univ where
  x == y = tryGetLeanValue $ lean_univ_eq x y

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

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


instance Ord Univ where
  x <= y = not (tryGetLeanValue $ y `lean_univ_quick_lt` x)

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

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


-- | Total ordering over universes using structural equality.
univLt :: Univ -> Univ -> Bool
univLt x y = tryGetLeanValue $ x `lean_univ_lt` y

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

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


------------------------------------------------------------------------
-- Univ instance

instance Show Univ where
  show = showUniv

-- | Show a universe.
showUniv :: Univ -> String
showUniv u = tryGetLeanValue $ lean_univ_to_string u

-- | Show a universe with the given options.
showUnivUsing :: Univ -> Options -> String
showUnivUsing u options = tryGetLeanValue $ lean_univ_to_string_using u options

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

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


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

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


------------------------------------------------------------------------
-- Univ Lists

-- | A list of universes (constructor not actually exported)
newtype instance List Univ = ListUniv (ForeignPtr (List Univ))


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


-- | Haskell type for @lean_list_univ@ FFI parameters.
type ListUnivPtr = Ptr (ListUniv)
{-# LINE 138 "src/Language/Lean/Internal/Univ.chs" #-}

-- | Haskell type for @lean_list_univ*@ FFI parameters.
type OutListUnivPtr = Ptr (ListUnivPtr)
{-# LINE 140 "src/Language/Lean/Internal/Univ.chs" #-}


-- | Synonym for @List Expr@ that can be used in @c2hs@ bindings
type ListUniv = List Univ

-- | Function @c2hs@ uses to pass @ListUniv@ values to Lean
withListUniv :: ListUniv -> (Ptr ListUniv -> IO a) -> IO a
withListUniv (ListUniv p) = withForeignPtr $! p

instance IsLeanValue (List Univ) (Ptr (List Univ)) where
  mkLeanValue = fmap ListUniv . newForeignPtr lean_list_univ_del_ptr

foreign import ccall unsafe "&lean_list_univ_del"
  lean_list_univ_del_ptr :: FunPtr (ListUnivPtr -> IO ())

------------------------------------------------------------------------
-- ListUniv Eq instance

instance Eq (List Univ) where
  x == y = tryGetLeanValue $ lean_list_univ_eq x y

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

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


------------------------------------------------------------------------
-- ListUniv IsList instance

-- | Allow @(List Univ)@ to use @OverloadedLists@ extensions.
instance IsList (List Univ) where
  -- | List Univ type family instance needed by @IsList (List Univ)@
  type Item (List Univ) = Univ
  fromList = fromListDefault
  toList = toListOf traverseList

------------------------------------------------------------------------
-- ListUniv IsListIso instance

instance IsListIso (List Univ) where
  nil = tryGetLeanValue $ lean_list_univ_mk_nil
  h <| r = tryGetLeanValue $ lean_list_univ_mk_cons h r

  listView l =
    if lean_list_univ_is_cons l then
      tryGetLeanValue (lean_list_univ_head l)
        :< tryGetLeanValue (lean_list_univ_tail l)
    else
      Nil

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

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


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

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


lean_list_univ_is_cons :: (ListUniv) -> (Bool)
lean_list_univ_is_cons a1 =
  unsafePerformIO $
  (withListUniv) a1 $ \a1' -> 
  let {res = lean_list_univ_is_cons'_ a1'} in
  let {res' = toBool res} in
  return (res')

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


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

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


lean_list_univ_tail :: (ListUniv) -> (OutListUnivPtr) -> (OutExceptionPtr) -> IO ((Bool))
lean_list_univ_tail a1 a2 a3 =
  (withListUniv) a1 $ \a1' -> 
  let {a2' = id a2} in 
  let {a3' = id a3} in 
  lean_list_univ_tail'_ a1' a2' a3' >>= \res ->
  let {res' = toBool res} in
  return (res')

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


------------------------------------------------------------------------
-- ListUniv Show instance

instance Show (List Univ) where
  showsPrec _ l = showList (toList l)

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

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

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

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

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

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

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

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

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

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

foreign import ccall unsafe "Language/Lean/Internal/Univ.chs.h lean_list_univ_tail"
  lean_list_univ_tail'_ :: ((ListUnivPtr) -> ((OutListUnivPtr) -> ((OutExceptionPtr) -> (IO CInt))))