-- 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/Name.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 names
together with typeclass instances for @Name@.
-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE ForeignFunctionInterface #-}
{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE Trustworthy #-}
{-# OPTIONS_HADDOCK not-home #-}
module Language.Lean.Internal.Name
  ( Name
  , anonymousName
  , nameAppend
  , nameAppendIndex
  , NameView(..)
  , nameView
  , nameToString
    -- * Internal declarations
  , NamePtr
  , OutNamePtr
  , withName
  , ListName
  , ListNamePtr
  , OutListNamePtr
  , withListName
  ) where

import Control.Exception (assert, throw)
import Control.Lens (toListOf)
import Data.Char (isDigit)
import Data.String
import Foreign
import Foreign.C
import System.IO.Unsafe

import Language.Lean.List

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

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








{-# LINE 53 "src/Language/Lean/Internal/Name.chs" #-}


-- | A Lean name
newtype Name = Name (ForeignPtr Name)

-- | Function @c2hs@ uses to pass @Name@ values to Lean
withName :: Name -> (Ptr Name -> IO a) -> IO a
withName (Name fo) = withForeignPtr $! fo
{-# INLINE withName #-}

-- | Haskell type for @lean_name@ FFI parameters.
type NamePtr = Ptr (Name)
{-# LINE 64 "src/Language/Lean/Internal/Name.chs" #-}

-- | Haskell type for @lean_name*@ FFI parameters.
type OutNamePtr = Ptr (NamePtr)
{-# LINE 66 "src/Language/Lean/Internal/Name.chs" #-}


foreign import ccall unsafe "&lean_name_del"
  lean_name_del_ptr :: FunPtr (NamePtr -> IO ())

instance IsLeanValue Name (Ptr Name) where
  mkLeanValue v = Name <$> newForeignPtr lean_name_del_ptr v

instance Eq Name where
  (==) = lean_name_eq

lean_name_eq :: (Name) -> (Name) -> (Bool)
lean_name_eq a1 a2 =
  unsafePerformIO $
  (withName) a1 $ \a1' -> 
  (withName) a2 $ \a2' -> 
  let {res = lean_name_eq'_ a1' a2'} in
  let {res' = toBool res} in
  return (res')

{-# LINE 77 "src/Language/Lean/Internal/Name.chs" #-}


instance Ord Name where
   x <= y = not (lean_name_quick_lt y x)

lean_name_quick_lt :: (Name) -> (Name) -> (Bool)
lean_name_quick_lt a1 a2 =
  unsafePerformIO $
  (withName) a1 $ \a1' -> 
  (withName) a2 $ \a2' -> 
  let {res = lean_name_quick_lt'_ a1' a2'} in
  let {res' = toBool res} in
  return (res')

{-# LINE 82 "src/Language/Lean/Internal/Name.chs" #-}


-- | Return a name as a string with subnames separated by periods.
nameToString :: Name -> String
nameToString nm = tryGetLeanValue $ lean_name_to_string nm

instance Show Name where
  show = show . nameToString

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

{-# LINE 92 "src/Language/Lean/Internal/Name.chs" #-}


------------------------------------------------------------------------
-- Constructing Names

-- | The root "anonymous" name
anonymousName :: Name
anonymousName = tryGetLeanValue lean_name_mk_anonymous

-- | Append a string to a name.
nameAppend :: Name -> String -> Name
nameAppend pre r = tryGetLeanValue (lean_name_mk_str pre r)

-- | Append a numeric index to a name.
nameAppendIndex :: Name -> Word32 -> Name
nameAppendIndex pre i = tryGetLeanValue (lean_name_mk_idx pre i)

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

{-# LINE 112 "src/Language/Lean/Internal/Name.chs" #-}


lean_name_mk_str :: (Name) -> (String) -> (OutNamePtr) -> (OutExceptionPtr) -> IO ((Bool))
lean_name_mk_str a1 a2 a3 a4 =
  (withName) a1 $ \a1' -> 
  withLeanStringPtr a2 $ \a2' -> 
  let {a3' = id a3} in 
  let {a4' = id a4} in 
  lean_name_mk_str'_ a1' a2' a3' a4' >>= \res ->
  let {res' = toBool res} in
  return (res')

{-# LINE 119 "src/Language/Lean/Internal/Name.chs" #-}


lean_name_mk_idx :: (Name) -> (Word32) -> (OutNamePtr) -> (OutExceptionPtr) -> IO ((Bool))
lean_name_mk_idx a1 a2 a3 a4 =
  (withName) a1 $ \a1' -> 
  let {a2' = fromIntegral a2} in 
  let {a3' = id a3} in 
  let {a4' = id a4} in 
  lean_name_mk_idx'_ a1' a2' a3' a4' >>= \res ->
  let {res' = toBool res} in
  return (res')

{-# LINE 126 "src/Language/Lean/Internal/Name.chs" #-}


------------------------------------------------------------------------
-- Viewing Names

-- | A view of head of a lean name.
data NameView
   = AnonymousName
     -- ^ The anonymous name.
   | StringName Name String
     -- ^ A name with a string appended.
   | IndexName Name Word32
     -- ^ A name with a numeric value appended.
  deriving (Show)

-- | View the head of a Lean name.
nameView :: Name -> NameView
nameView nm =
  if lean_name_is_anonymous nm then
    AnonymousName
  else if lean_name_is_str nm then do
    StringName (tryGetLeanValue $ lean_name_get_prefix nm)
               (tryGetLeanValue $ lean_name_get_str nm)
  else assert (lean_name_is_idx nm) $ do
    IndexName (tryGetLeanValue $ lean_name_get_prefix nm)
              (tryGetLeanValue $ lean_name_get_idx nm)

lean_name_is_anonymous :: (Name) -> (Bool)
lean_name_is_anonymous a1 =
  unsafePerformIO $
  (withName) a1 $ \a1' -> 
  let {res = lean_name_is_anonymous'_ a1'} in
  let {res' = toBool res} in
  return (res')

{-# LINE 153 "src/Language/Lean/Internal/Name.chs" #-}

lean_name_is_str :: (Name) -> (Bool)
lean_name_is_str a1 =
  unsafePerformIO $
  (withName) a1 $ \a1' -> 
  let {res = lean_name_is_str'_ a1'} in
  let {res' = toBool res} in
  return (res')

{-# LINE 154 "src/Language/Lean/Internal/Name.chs" #-}

lean_name_is_idx :: (Name) -> (Bool)
lean_name_is_idx a1 =
  unsafePerformIO $
  (withName) a1 $ \a1' -> 
  let {res = lean_name_is_idx'_ a1'} in
  let {res' = toBool res} in
  return (res')

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


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

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


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

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


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

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


------------------------------------------------------------------------
-- Name IsString instance

instance IsString Name where
  fromString = go anonymousName
    where
      go nm "" = nm
      go nm s  =
        case break (== '.') s of
          (h,'.':r) -> go (go' nm h) r
          (h,r)     -> assert (null r) (go' nm h)
      go' nm s@(c:_) | isDigit c =
        case reads s of
          [(i,"")] -> nameAppendIndex nm i
          _        -> throw $ leanKernelException msg
            where
              msg = "Identifiers cannot begin with a digit."
      go' _ "" = throw $ leanKernelException "Identifiers cannot be empty"
      go' nm s = nameAppend nm s

------------------------------------------------------------------------
-- Name Monoid instance

-- Monoid instance allows one to write code like @nm <> "foo.bar"@ to append
-- "foo.bar" to a name.
instance Monoid Name where
  mempty  = anonymousName
  mappend x y =
    case nameView y of
      AnonymousName   -> x
      StringName yn s -> mappend x yn `nameAppend` s
      IndexName  yn i -> mappend x yn `nameAppendIndex` i

------------------------------------------------------------------------
-- Name Lists

-- | A list of names (constructor not actually exported)
newtype instance List Name = ListName (ForeignPtr (List Name))

-- | A list of Lean universe levels.

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

-- | Haskell type for @lean_list_name@ FFI parameters.
type ListNamePtr = Ptr (ListName)
{-# LINE 208 "src/Language/Lean/Internal/Name.chs" #-}

-- | Haskell type for @lean_list_name*@ FFI parameters.
type OutListNamePtr = Ptr (ListNamePtr)
{-# LINE 210 "src/Language/Lean/Internal/Name.chs" #-}


-- | Synonym for @List Expr@ that can be used in @c2hs@ bindings.
type ListName = List Name

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

instance IsLeanValue (List Name) (Ptr (List Name)) where
  mkLeanValue = fmap ListName . newForeignPtr lean_list_name_del_ptr

foreign import ccall unsafe "&lean_list_name_del"
  lean_list_name_del_ptr :: FunPtr (ListNamePtr -> IO ())

------------------------------------------------------------------------
-- ListName Eq instance

instance Eq (List Name) where
  (==) = lean_list_name_eq

lean_list_name_eq :: (ListName) -> (ListName) -> (Bool)
lean_list_name_eq a1 a2 =
  unsafePerformIO $
  (withListName) a1 $ \a1' -> 
  (withListName) a2 $ \a2' -> 
  let {res = lean_list_name_eq'_ a1' a2'} in
  let {res' = toBool res} in
  return (res')

{-# LINE 234 "src/Language/Lean/Internal/Name.chs" #-}


------------------------------------------------------------------------
-- ListName IsListIso instance

instance IsListIso (List Name) where
  nil = tryGetLeanValue $ lean_list_name_mk_nil
  h <| r = tryGetLeanValue $ lean_list_name_mk_cons h r

  listView l =
    if lean_list_name_is_cons l then
      tryGetLeanValue (lean_list_name_head l)
        :< tryGetLeanValue (lean_list_name_tail l)
    else
      Nil

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

{-# LINE 253 "src/Language/Lean/Internal/Name.chs" #-}


lean_list_name_mk_cons :: (Name) -> (ListName) -> (OutListNamePtr) -> (OutExceptionPtr) -> IO ((Bool))
lean_list_name_mk_cons a1 a2 a3 a4 =
  (withName) a1 $ \a1' -> 
  (withListName) a2 $ \a2' -> 
  let {a3' = id a3} in 
  let {a4' = id a4} in 
  lean_list_name_mk_cons'_ a1' a2' a3' a4' >>= \res ->
  let {res' = toBool res} in
  return (res')

{-# LINE 260 "src/Language/Lean/Internal/Name.chs" #-}


lean_list_name_is_cons :: (ListName) -> (Bool)
lean_list_name_is_cons a1 =
  unsafePerformIO $
  (withListName) a1 $ \a1' -> 
  let {res = lean_list_name_is_cons'_ a1'} in
  let {res' = toBool res} in
  return (res')

{-# LINE 264 "src/Language/Lean/Internal/Name.chs" #-}


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

{-# LINE 270 "src/Language/Lean/Internal/Name.chs" #-}


lean_list_name_tail :: (ListName) -> (OutListNamePtr) -> (OutExceptionPtr) -> IO ((Bool))
lean_list_name_tail a1 a2 a3 =
  (withListName) a1 $ \a1' -> 
  let {a2' = id a2} in 
  let {a3' = id a3} in 
  lean_list_name_tail'_ a1' a2' a3' >>= \res ->
  let {res' = toBool res} in
  return (res')

{-# LINE 276 "src/Language/Lean/Internal/Name.chs" #-}


------------------------------------------------------------------------
-- ListName IsList instance

instance IsList (List Name) where
  type Item ListName = Name
  fromList = fromListDefault
  toList = toListOf traverseList

------------------------------------------------------------------------
-- ListName Show instance

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

foreign import ccall unsafe "Language/Lean/Internal/Name.chs.h lean_name_eq"
  lean_name_eq'_ :: ((NamePtr) -> ((NamePtr) -> CInt))

foreign import ccall unsafe "Language/Lean/Internal/Name.chs.h lean_name_quick_lt"
  lean_name_quick_lt'_ :: ((NamePtr) -> ((NamePtr) -> CInt))

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

foreign import ccall unsafe "Language/Lean/Internal/Name.chs.h lean_name_mk_anonymous"
  lean_name_mk_anonymous'_ :: ((OutNamePtr) -> ((OutExceptionPtr) -> (IO CInt)))

foreign import ccall unsafe "Language/Lean/Internal/Name.chs.h lean_name_mk_str"
  lean_name_mk_str'_ :: ((NamePtr) -> ((Ptr CChar) -> ((OutNamePtr) -> ((OutExceptionPtr) -> (IO CInt)))))

foreign import ccall unsafe "Language/Lean/Internal/Name.chs.h lean_name_mk_idx"
  lean_name_mk_idx'_ :: ((NamePtr) -> (CUInt -> ((OutNamePtr) -> ((OutExceptionPtr) -> (IO CInt)))))

foreign import ccall unsafe "Language/Lean/Internal/Name.chs.h lean_name_is_anonymous"
  lean_name_is_anonymous'_ :: ((NamePtr) -> CInt)

foreign import ccall unsafe "Language/Lean/Internal/Name.chs.h lean_name_is_str"
  lean_name_is_str'_ :: ((NamePtr) -> CInt)

foreign import ccall unsafe "Language/Lean/Internal/Name.chs.h lean_name_is_idx"
  lean_name_is_idx'_ :: ((NamePtr) -> CInt)

foreign import ccall unsafe "Language/Lean/Internal/Name.chs.h lean_name_get_prefix"
  lean_name_get_prefix'_ :: ((NamePtr) -> ((OutNamePtr) -> ((OutExceptionPtr) -> (IO CInt))))

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

foreign import ccall unsafe "Language/Lean/Internal/Name.chs.h lean_name_get_idx"
  lean_name_get_idx'_ :: ((NamePtr) -> ((Ptr CUInt) -> ((OutExceptionPtr) -> (IO CInt))))

foreign import ccall unsafe "Language/Lean/Internal/Name.chs.h lean_list_name_eq"
  lean_list_name_eq'_ :: ((ListNamePtr) -> ((ListNamePtr) -> CInt))

foreign import ccall unsafe "Language/Lean/Internal/Name.chs.h lean_list_name_mk_nil"
  lean_list_name_mk_nil'_ :: ((OutListNamePtr) -> ((OutExceptionPtr) -> (IO CInt)))

foreign import ccall unsafe "Language/Lean/Internal/Name.chs.h lean_list_name_mk_cons"
  lean_list_name_mk_cons'_ :: ((NamePtr) -> ((ListNamePtr) -> ((OutListNamePtr) -> ((OutExceptionPtr) -> (IO CInt)))))

foreign import ccall unsafe "Language/Lean/Internal/Name.chs.h lean_list_name_is_cons"
  lean_list_name_is_cons'_ :: ((ListNamePtr) -> CInt)

foreign import ccall unsafe "Language/Lean/Internal/Name.chs.h lean_list_name_head"
  lean_list_name_head'_ :: ((ListNamePtr) -> ((OutNamePtr) -> ((OutExceptionPtr) -> (IO CInt))))

foreign import ccall unsafe "Language/Lean/Internal/Name.chs.h lean_list_name_tail"
  lean_list_name_tail'_ :: ((ListNamePtr) -> ((OutListNamePtr) -> ((OutExceptionPtr) -> (IO CInt))))