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

Internal declarations for Lean expressions and typeclass instances for @Expr@.
-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE ForeignFunctionInterface #-}
{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE Trustworthy #-}
{-# OPTIONS_HADDOCK not-home #-}
module Language.Lean.Internal.Expr
  ( -- * Macro definitions
    MacroDef
  , MacroDefPtr
  , OutMacroDefPtr
  , withMacroDef
    -- * Expressions
  , Expr
  , ExprPtr
  , OutExprPtr
  , withExpr
  , exprLt
  , exprToString
  , BinderKind(..)
    -- * List of expressions
  , ListExpr
  , ListExprPtr
  , OutListExprPtr
  , withListExpr
  ) where

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

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

import Language.Lean.Internal.Exception.Unsafe









------------------------------------------------------------------------
-- MacroDef declaration


{-# LINE 56 "src/Language/Lean/Internal/Expr.chs" #-}


-- | A Lean macro definition
newtype MacroDef = MacroDef (ForeignPtr MacroDef)

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

-- | Haskell type for @lean_macro_def@ FFI parameters.
type MacroDefPtr = Ptr (MacroDef)
{-# LINE 66 "src/Language/Lean/Internal/Expr.chs" #-}

-- | Haskell type for @lean_macro_def*@ FFI parameters.
type OutMacroDefPtr = Ptr (MacroDefPtr)
{-# LINE 68 "src/Language/Lean/Internal/Expr.chs" #-}


instance IsLeanValue MacroDef (Ptr MacroDef) where
  mkLeanValue = fmap MacroDef . newForeignPtr lean_macro_def_del_ptr

foreign import ccall unsafe "&lean_macro_def_del"
  lean_macro_def_del_ptr :: FunPtr (MacroDefPtr -> IO ())

------------------------------------------------------------------------
-- MacroDef eq

instance Eq MacroDef where
  (==) = error "Equality comparison with macro definitions is not yet implemented."

instance Show MacroDef where
  show = error "MacroDef.show not yet implement"

------------------------------------------------------------------------
-- BinderKind declaration

-- | Kind of binding used for bound variables.
data BinderKind = BinderDefault
                | BinderImplicit
                | BinderStrictImplicit
                | BinderInstImplicit
                | BinderHidden
  deriving (Enum,Eq,Show)

{-# LINE 91 "src/Language/Lean/Internal/Expr.chs" #-}


------------------------------------------------------------------------
-- Expr declaration


{-# LINE 96 "src/Language/Lean/Internal/Expr.chs" #-}


-- | A Lean expression
newtype Expr = Expr (ForeignPtr Expr)

-- | Get access to @lean_expr@ within IO action.
withExpr :: Expr -> (Ptr Expr -> IO a) -> IO a
withExpr (Expr o) = withForeignPtr $! o

-- | Haskell type for @lean_expr@ FFI parameters.
type ExprPtr = Ptr (Expr)
{-# LINE 106 "src/Language/Lean/Internal/Expr.chs" #-}

-- | Haskell type for @lean_expr*@ FFI parameters.
type OutExprPtr = Ptr (ExprPtr)
{-# LINE 108 "src/Language/Lean/Internal/Expr.chs" #-}


instance IsLeanValue Expr (Ptr Expr) where
  mkLeanValue = fmap Expr . newForeignPtr lean_expr_del_ptr

foreign import ccall unsafe "&lean_expr_del"
  lean_expr_del_ptr :: FunPtr (ExprPtr -> IO ())

------------------------------------------------------------------------
-- ListExpr declaration

-- | A list of expressions (constructor not actually exported)
newtype instance List Expr = ListExpr (ForeignPtr (List Expr))

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

-- | Function @c2hs@ uses to pass @ListExpr@ values to Lean
withListExpr :: List Expr -> (Ptr (List Expr) -> IO a) -> IO a
withListExpr (ListExpr p) = withForeignPtr $! p


{-# LINE 129 "src/Language/Lean/Internal/Expr.chs" #-}


-- | Haskell type for @lean_list_expr@ FFI parameters.
type ListExprPtr = Ptr (ListExpr)
{-# LINE 132 "src/Language/Lean/Internal/Expr.chs" #-}

-- | Haskell type for @lean_list_expr*@ FFI parameters.
type OutListExprPtr = Ptr (ListExprPtr)
{-# LINE 134 "src/Language/Lean/Internal/Expr.chs" #-}


instance IsLeanValue (List Expr) (Ptr (List Expr)) where
  mkLeanValue = fmap ListExpr . newForeignPtr lean_list_expr_del_ptr

foreign import ccall unsafe "&lean_list_expr_del"
  lean_list_expr_del_ptr :: FunPtr (ListExprPtr -> IO ())

------------------------------------------------------------------------
-- Expression Show instance

-- | Return the string representation of an expression.
exprToString :: Expr -> String
exprToString x = tryGetLeanValue $ lean_expr_to_string x

instance Show Expr where
  show = show . exprToString

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

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


------------------------------------------------------------------------
-- Expression Comparison

instance Eq Expr where
  x == y = tryGetLeanValue $ lean_expr_eq x y

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

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


instance Ord Expr where
   x <= y = not $ tryGetLeanValue $ lean_expr_quick_lt y x

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

{-# LINE 168 "src/Language/Lean/Internal/Expr.chs" #-}


-- | Return true if first expression is structurally less than other.
exprLt :: Expr -> Expr -> Bool
exprLt x y = tryGetLeanValue $ lean_expr_lt x y

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

{-# LINE 175 "src/Language/Lean/Internal/Expr.chs" #-}


------------------------------------------------------------------------
-- ListExpr Eq instance

instance Eq (List Expr) where
  (==) = lean_list_expr_eq

lean_list_expr_eq :: (ListExpr) -> (ListExpr) -> (Bool)
lean_list_expr_eq a1 a2 =
  unsafePerformIO $
  (withListExpr) a1 $ \a1' -> 
  (withListExpr) a2 $ \a2' -> 
  let {res = lean_list_expr_eq'_ a1' a2'} in
  let {res' = toBool res} in
  return (res')

{-# LINE 184 "src/Language/Lean/Internal/Expr.chs" #-}


------------------------------------------------------------------------
-- ListExpr IsListIso instance

instance IsListIso (List Expr) where
  nil = tryGetLeanValue $ lean_list_expr_mk_nil
  h <| r = tryGetLeanValue $ lean_list_expr_mk_cons h r

  listView l =
    if lean_list_expr_is_cons l then
      tryGetLeanValue (lean_list_expr_head l)
        :< tryGetLeanValue (lean_list_expr_tail l)
    else
      Nil

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

{-# LINE 203 "src/Language/Lean/Internal/Expr.chs" #-}


lean_list_expr_mk_cons :: (Expr) -> (ListExpr) -> (OutListExprPtr) -> (OutExceptionPtr) -> IO ((Bool))
lean_list_expr_mk_cons a1 a2 a3 a4 =
  (withExpr) a1 $ \a1' -> 
  (withListExpr) a2 $ \a2' -> 
  let {a3' = id a3} in 
  let {a4' = id a4} in 
  lean_list_expr_mk_cons'_ a1' a2' a3' a4' >>= \res ->
  let {res' = toBool res} in
  return (res')

{-# LINE 210 "src/Language/Lean/Internal/Expr.chs" #-}


lean_list_expr_is_cons :: (ListExpr) -> (Bool)
lean_list_expr_is_cons a1 =
  unsafePerformIO $
  (withListExpr) a1 $ \a1' -> 
  let {res = lean_list_expr_is_cons'_ a1'} in
  let {res' = toBool res} in
  return (res')

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


lean_list_expr_head :: (ListExpr) -> (OutExprPtr) -> (OutExceptionPtr) -> IO ((Bool))
lean_list_expr_head a1 a2 a3 =
  (withListExpr) a1 $ \a1' -> 
  let {a2' = id a2} in 
  let {a3' = id a3} in 
  lean_list_expr_head'_ a1' a2' a3' >>= \res ->
  let {res' = toBool res} in
  return (res')

{-# LINE 220 "src/Language/Lean/Internal/Expr.chs" #-}


lean_list_expr_tail :: (ListExpr) -> (OutListExprPtr) -> (OutExceptionPtr) -> IO ((Bool))
lean_list_expr_tail a1 a2 a3 =
  (withListExpr) a1 $ \a1' -> 
  let {a2' = id a2} in 
  let {a3' = id a3} in 
  lean_list_expr_tail'_ a1' a2' a3' >>= \res ->
  let {res' = toBool res} in
  return (res')

{-# LINE 226 "src/Language/Lean/Internal/Expr.chs" #-}


------------------------------------------------------------------------
-- ListExpr IsList instance

instance IsList (List Expr) where
  type Item ListExpr = Expr
  fromList = fromListDefault
  toList = toListOf traverseList

------------------------------------------------------------------------
-- ListExpr Show instance

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

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

foreign import ccall unsafe "Language/Lean/Internal/Expr.chs.h lean_expr_eq"
  lean_expr_eq'_ :: ((ExprPtr) -> ((ExprPtr) -> ((Ptr CInt) -> ((OutExceptionPtr) -> (IO CInt)))))

foreign import ccall unsafe "Language/Lean/Internal/Expr.chs.h lean_expr_quick_lt"
  lean_expr_quick_lt'_ :: ((ExprPtr) -> ((ExprPtr) -> ((Ptr CInt) -> ((OutExceptionPtr) -> (IO CInt)))))

foreign import ccall unsafe "Language/Lean/Internal/Expr.chs.h lean_expr_lt"
  lean_expr_lt'_ :: ((ExprPtr) -> ((ExprPtr) -> ((Ptr CInt) -> ((OutExceptionPtr) -> (IO CInt)))))

foreign import ccall unsafe "Language/Lean/Internal/Expr.chs.h lean_list_expr_eq"
  lean_list_expr_eq'_ :: ((ListExprPtr) -> ((ListExprPtr) -> CInt))

foreign import ccall unsafe "Language/Lean/Internal/Expr.chs.h lean_list_expr_mk_nil"
  lean_list_expr_mk_nil'_ :: ((OutListExprPtr) -> ((OutExceptionPtr) -> (IO CInt)))

foreign import ccall unsafe "Language/Lean/Internal/Expr.chs.h lean_list_expr_mk_cons"
  lean_list_expr_mk_cons'_ :: ((ExprPtr) -> ((ListExprPtr) -> ((OutListExprPtr) -> ((OutExceptionPtr) -> (IO CInt)))))

foreign import ccall unsafe "Language/Lean/Internal/Expr.chs.h lean_list_expr_is_cons"
  lean_list_expr_is_cons'_ :: ((ListExprPtr) -> CInt)

foreign import ccall unsafe "Language/Lean/Internal/Expr.chs.h lean_list_expr_head"
  lean_list_expr_head'_ :: ((ListExprPtr) -> ((OutExprPtr) -> ((OutExceptionPtr) -> (IO CInt))))

foreign import ccall unsafe "Language/Lean/Internal/Expr.chs.h lean_list_expr_tail"
  lean_list_expr_tail'_ :: ((ListExprPtr) -> ((OutListExprPtr) -> ((OutExceptionPtr) -> (IO CInt))))