{-# LINE 1 "src/runtime/haskell-bind/PGF2/Type.hsc" #-}

{-# LINE 2 "src/runtime/haskell-bind/PGF2/Type.hsc" #-}

module PGF2.Type where

import System.IO.Unsafe(unsafePerformIO)
import Foreign hiding (unsafePerformIO)
import Foreign.C
import qualified Text.PrettyPrint as PP
import Data.List(mapAccumL)
import PGF2.Expr
import PGF2.FFI

-- The C structure for the expression may point to other structures
-- which are allocated from other pools. In order to ensure that
-- they are not released prematurely we use the exprMaster to
-- store references to other Haskell objects
data Type = Type {typ :: PgfExpr, touchType :: Touch}

-- | 'Hypo' represents a hypothesis in a type i.e. in the type A -> B, A is the hypothesis
type Hypo = (BindType,CId,Type)

instance Show Type where
  show = showType []

-- | parses a 'String' as a type
readType :: String -> Maybe Type
readType str =
  unsafePerformIO $
    do typPl <- gu_new_pool
       withGuPool $ \tmpPl ->
         do c_str <- newUtf8CString str tmpPl
            guin <- gu_string_in c_str tmpPl
            exn <- gu_new_exn tmpPl
            c_type <- pgf_read_type guin typPl tmpPl exn
            status <- gu_exn_is_raised exn
            if (not status && c_type /= nullPtr)
              then do typFPl <- newForeignPtr gu_pool_finalizer typPl
                      return $ Just (Type c_type (touchForeignPtr typFPl))
              else do gu_pool_free typPl
                      return Nothing

-- | renders a type as a 'String'. The list
-- of identifiers is the list of all free variables
-- in the type in order reverse to the order
-- of binding.
showType :: [CId] -> Type -> String
showType scope (Type ty touch) = 
  unsafePerformIO $
    withGuPool $ \tmpPl ->
      do (sb,out) <- newOut tmpPl
         printCtxt <- newPrintCtxt scope tmpPl
         exn <- gu_new_exn tmpPl
         pgf_print_type ty printCtxt 0 out exn
         touch
         s <- gu_string_buf_freeze sb tmpPl
         peekUtf8CString s

-- | creates a type from a list of hypothesises, a category and 
-- a list of arguments for the category. The operation 
-- @mkType [h_1,...,h_n] C [e_1,...,e_m]@ will create 
-- @h_1 -> ... -> h_n -> C e_1 ... e_m@
mkType :: [Hypo] -> CId -> [Expr] -> Type
mkType hypos cat exprs = unsafePerformIO $ do
  typPl  <- gu_new_pool
  let n_exprs = fromIntegral (length exprs) :: CSizeT
  c_type <- gu_malloc typPl (((24)) + n_exprs * ((8)))
{-# LINE 67 "src/runtime/haskell-bind/PGF2/Type.hsc" #-}
  c_hypos <- newSequence ((24)) (pokeHypo typPl) hypos typPl
{-# LINE 68 "src/runtime/haskell-bind/PGF2/Type.hsc" #-}
  ((\hsc_ptr -> pokeByteOff hsc_ptr 0)) c_type c_hypos
{-# LINE 69 "src/runtime/haskell-bind/PGF2/Type.hsc" #-}
  ccat <- newUtf8CString cat typPl
  ((\hsc_ptr -> pokeByteOff hsc_ptr 8)) c_type ccat
{-# LINE 71 "src/runtime/haskell-bind/PGF2/Type.hsc" #-}
  ((\hsc_ptr -> pokeByteOff hsc_ptr 16)) c_type n_exprs
{-# LINE 72 "src/runtime/haskell-bind/PGF2/Type.hsc" #-}
  pokeExprs (c_type `plusPtr` ((24))) exprs
{-# LINE 73 "src/runtime/haskell-bind/PGF2/Type.hsc" #-}
  typFPl <- newForeignPtr gu_pool_finalizer typPl
  return (Type c_type (mapM_ touchHypo hypos >> mapM_ touchExpr exprs >> touchForeignPtr typFPl))

pokeHypo :: Ptr GuPool -> Ptr a -> Hypo -> IO ()
pokeHypo pool c_hypo (bind_type,cid,Type c_ty _) = do
  ((\hsc_ptr -> pokeByteOff hsc_ptr 0)) c_hypo cbind_type
{-# LINE 79 "src/runtime/haskell-bind/PGF2/Type.hsc" #-}
  newUtf8CString cid pool >>= ((\hsc_ptr -> pokeByteOff hsc_ptr 8)) c_hypo
{-# LINE 80 "src/runtime/haskell-bind/PGF2/Type.hsc" #-}
  ((\hsc_ptr -> pokeByteOff hsc_ptr 16)) c_hypo c_ty
{-# LINE 81 "src/runtime/haskell-bind/PGF2/Type.hsc" #-}
  where
    cbind_type :: CInt
    cbind_type =
      case bind_type of
        Explicit -> (0)
{-# LINE 86 "src/runtime/haskell-bind/PGF2/Type.hsc" #-}
        Implicit -> (1)
{-# LINE 87 "src/runtime/haskell-bind/PGF2/Type.hsc" #-}

pokeExprs ptr []              = return ()
pokeExprs ptr ((Expr e _):es) = do
  poke ptr e
  pokeExprs (plusPtr ptr ((8))) es
{-# LINE 92 "src/runtime/haskell-bind/PGF2/Type.hsc" #-}
    
touchHypo (_,_,ty) = touchType ty

-- | Decomposes a type into a list of hypothesises, a category and 
-- a list of arguments for the category.
unType :: Type -> ([Hypo],CId,[Expr])
unType (Type c_type touch) = unsafePerformIO $ do
  cid <- ((\hsc_ptr -> peekByteOff hsc_ptr 8)) c_type >>= peekUtf8CString
{-# LINE 100 "src/runtime/haskell-bind/PGF2/Type.hsc" #-}
  c_hypos <- ((\hsc_ptr -> peekByteOff hsc_ptr 0)) c_type
{-# LINE 101 "src/runtime/haskell-bind/PGF2/Type.hsc" #-}
  n_hypos <- ((\hsc_ptr -> peekByteOff hsc_ptr 0)) c_hypos
{-# LINE 102 "src/runtime/haskell-bind/PGF2/Type.hsc" #-}
  hs <- peekHypos (c_hypos `plusPtr` ((8))) 0 n_hypos
{-# LINE 103 "src/runtime/haskell-bind/PGF2/Type.hsc" #-}
  n_exprs <- ((\hsc_ptr -> peekByteOff hsc_ptr 16)) c_type
{-# LINE 104 "src/runtime/haskell-bind/PGF2/Type.hsc" #-}
  es <- peekExprs (c_type `plusPtr` ((24))) 0 n_exprs
{-# LINE 105 "src/runtime/haskell-bind/PGF2/Type.hsc" #-}
  return (hs,cid,es)
  where
    peekHypos :: Ptr a -> Int -> Int -> IO [Hypo]
    peekHypos c_hypo i n
      | i < n     = do cid <- ((\hsc_ptr -> peekByteOff hsc_ptr 8)) c_hypo >>= peekUtf8CString
{-# LINE 110 "src/runtime/haskell-bind/PGF2/Type.hsc" #-}
                       c_ty <- ((\hsc_ptr -> peekByteOff hsc_ptr 16)) c_hypo
{-# LINE 111 "src/runtime/haskell-bind/PGF2/Type.hsc" #-}
                       bt  <- fmap toBindType (((\hsc_ptr -> peekByteOff hsc_ptr 0)) c_hypo)
{-# LINE 112 "src/runtime/haskell-bind/PGF2/Type.hsc" #-}
                       hs <- peekHypos (plusPtr c_hypo ((24))) (i+1) n
{-# LINE 113 "src/runtime/haskell-bind/PGF2/Type.hsc" #-}
                       return ((bt,cid,Type c_ty touch) : hs)
      | otherwise = return []

    toBindType :: CInt -> BindType
    toBindType (0) = Explicit
{-# LINE 118 "src/runtime/haskell-bind/PGF2/Type.hsc" #-}
    toBindType (1) = Implicit
{-# LINE 119 "src/runtime/haskell-bind/PGF2/Type.hsc" #-}

    peekExprs ptr i n
      | i < n     = do e  <- peekElemOff ptr i
                       es <- peekExprs ptr (i+1) n
                       return (Expr e touch : es)
      | otherwise = return []

-- | renders a type as a 'String'. The list
-- of identifiers is the list of all free variables
-- in the type in order reverse to the order
-- of binding.
showContext :: [CId] -> [Hypo] -> String
showContext scope hypos =
  unsafePerformIO $
    withGuPool $ \tmpPl ->
      do (sb,out) <- newOut tmpPl
         c_hypos <- newSequence ((24)) (pokeHypo tmpPl) hypos tmpPl
{-# LINE 136 "src/runtime/haskell-bind/PGF2/Type.hsc" #-}
         printCtxt <- newPrintCtxt scope tmpPl
         exn <- gu_new_exn tmpPl
         pgf_print_context c_hypos printCtxt out exn
         mapM_ touchHypo hypos
         s <- gu_string_buf_freeze sb tmpPl
         peekUtf8CString s