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

Interface to Lean typechecker
-}
{-# LANGUAGE ForeignFunctionInterface #-}
{-# LANGUAGE Trustworthy #-}
module Language.Lean.Typechecker
  ( Typechecker
  , ConstraintSeq
  , typechecker
  , inferType
  , checkType
  , whnf
  , isDefEq
  ) where

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

import Language.Lean.Internal.Decl
{-# LINE 25 "src/Language/Lean/Typechecker.chs" #-}

import Language.Lean.Internal.Exception
{-# LINE 26 "src/Language/Lean/Typechecker.chs" #-}

import Language.Lean.Internal.Exception.Unsafe
import Language.Lean.Internal.Expr
{-# LINE 28 "src/Language/Lean/Typechecker.chs" #-}

import Language.Lean.Internal.Typechecker
{-# LINE 29 "src/Language/Lean/Typechecker.chs" #-}













------------------------------------------------------------------------
-- Typechecker constructor

-- | Create a type checker object for the given environment.
typechecker :: Env -> Typechecker
typechecker e = tryGetLeanValue $ lean_type_checker_mk e

lean_type_checker_mk :: (Env) -> (OutTypecheckerPtr) -> (OutExceptionPtr) -> IO ((Bool))
lean_type_checker_mk a1 a2 a3 =
  (withEnv) a1 $ \a1' -> 
  let {a2' = id a2} in 
  let {a3' = id a3} in 
  lean_type_checker_mk'_ a1' a2' a3' >>= \res ->
  let {res' = toBool res} in
  return (res')

{-# LINE 50 "src/Language/Lean/Typechecker.chs" #-}


------------------------------------------------------------------------
-- Typechecker operations

-- | A lean partial function is a function that returns a value of type @a@, but
-- may fail.
type LeanPartialFn2 a b = (Ptr a -> Ptr b -> LeanPartialAction)

-- | @inferType t e@ infers the type of @e@ using @t@.
-- This returns the type and any constraints generated.
--
-- The expression @e@ must not contain any free variables (subexpressions with
-- type @ExprVar@.
tryGetLeanPair :: (IsLeanValue a p, IsLeanValue b q)
               => LeanPartialFn2 p q
               -> (a,b)
tryGetLeanPair alloc_fn = unsafePerformIO $ do
  alloca $ \p_ptr -> do
    alloca $ \q_ptr -> do
      runLeanPartialAction $ alloc_fn p_ptr q_ptr
      p <- mkLeanValue =<< peek p_ptr
      q <- mkLeanValue =<< peek q_ptr
      seq p $ seq q $ (return $! (p,q))

-- | @inferType t e@ infers the type of @e@ using @t@.
-- This returns the type and any constraints generated.
--
-- The expression @e@ must not contain any free variables (subexpressions with
-- type @ExprVar@).
inferType :: Typechecker -> Expr -> (Expr, ConstraintSeq)
inferType t e = tryGetLeanPair $ lean_type_checker_infer t e

lean_type_checker_infer :: (Typechecker) -> (Expr) -> (OutExprPtr) -> (OutConstraintSeqPtr) -> (OutExceptionPtr) -> IO ((Bool))
lean_type_checker_infer a1 a2 a3 a4 a5 =
  (withTypechecker) a1 $ \a1' -> 
  (withExpr) a2 $ \a2' -> 
  let {a3' = id a3} in 
  let {a4' = id a4} in 
  let {a5' = id a5} in 
  lean_type_checker_infer'_ a1' a2' a3' a4' a5' >>= \res ->
  let {res' = toBool res} in
  return (res')

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


-- | @inferType t e@ checks and infers the type of @e@ using @t@.
-- This returns the type and any constraints generated.
--
-- The expression @e@ must not contain any free variables (subexpressions with
-- type @ExprVar@).
checkType :: Typechecker -> Expr -> (Expr, ConstraintSeq)
checkType t e = tryGetLeanPair $ lean_type_checker_check t e

lean_type_checker_check :: (Typechecker) -> (Expr) -> (OutExprPtr) -> (OutConstraintSeqPtr) -> (OutExceptionPtr) -> IO ((Bool))
lean_type_checker_check a1 a2 a3 a4 a5 =
  (withTypechecker) a1 $ \a1' -> 
  (withExpr) a2 $ \a2' -> 
  let {a3' = id a3} in 
  let {a4' = id a4} in 
  let {a5' = id a5} in 
  lean_type_checker_check'_ a1' a2' a3' a4' a5' >>= \res ->
  let {res' = toBool res} in
  return (res')

{-# LINE 105 "src/Language/Lean/Typechecker.chs" #-}


-- | @whnf t e@ computes the weak-head-normal-form of @e@ using @t@, returning the
-- form and any generated constraints.
--
-- The expression @e@ must not contain any free variables (subexpressions with
-- type @ExprVar@).
whnf :: Typechecker -> Expr -> (Expr, ConstraintSeq)
whnf t e = tryGetLeanPair $ lean_type_checker_whnf t e

lean_type_checker_whnf :: (Typechecker) -> (Expr) -> (OutExprPtr) -> (OutConstraintSeqPtr) -> (OutExceptionPtr) -> IO ((Bool))
lean_type_checker_whnf a1 a2 a3 a4 a5 =
  (withTypechecker) a1 $ \a1' -> 
  (withExpr) a2 $ \a2' -> 
  let {a3' = id a3} in 
  let {a4' = id a4} in 
  let {a5' = id a5} in 
  lean_type_checker_whnf'_ a1' a2' a3' a4' a5' >>= \res ->
  let {res' = toBool res} in
  return (res')

{-# LINE 121 "src/Language/Lean/Typechecker.chs" #-}


-- | @is_def_eq t e1 e2@ returns @True@  iff @e1@ and @e2@ are definitionally equal along
-- with any generated constraints.
--
-- The expressions @e1@ and @e2@ must not contain any free variables
-- (subexpressions with type @ExprVar@).
isDefEq :: Typechecker -> Expr -> Expr -> (Bool, ConstraintSeq)
isDefEq t e1 e2 = tryGetLeanPair $ lean_type_checker_is_def_eq t e1 e2

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

{-# LINE 138 "src/Language/Lean/Typechecker.chs" #-}


foreign import ccall unsafe "Language/Lean/Typechecker.chs.h lean_type_checker_mk"
  lean_type_checker_mk'_ :: ((EnvPtr) -> ((OutTypecheckerPtr) -> ((OutExceptionPtr) -> (IO CInt))))

foreign import ccall unsafe "Language/Lean/Typechecker.chs.h lean_type_checker_infer"
  lean_type_checker_infer'_ :: ((TypecheckerPtr) -> ((ExprPtr) -> ((OutExprPtr) -> ((OutConstraintSeqPtr) -> ((OutExceptionPtr) -> (IO CInt))))))

foreign import ccall unsafe "Language/Lean/Typechecker.chs.h lean_type_checker_check"
  lean_type_checker_check'_ :: ((TypecheckerPtr) -> ((ExprPtr) -> ((OutExprPtr) -> ((OutConstraintSeqPtr) -> ((OutExceptionPtr) -> (IO CInt))))))

foreign import ccall unsafe "Language/Lean/Typechecker.chs.h lean_type_checker_whnf"
  lean_type_checker_whnf'_ :: ((TypecheckerPtr) -> ((ExprPtr) -> ((OutExprPtr) -> ((OutConstraintSeqPtr) -> ((OutExceptionPtr) -> (IO CInt))))))

foreign import ccall unsafe "Language/Lean/Typechecker.chs.h lean_type_checker_is_def_eq"
  lean_type_checker_is_def_eq'_ :: ((TypecheckerPtr) -> ((ExprPtr) -> ((ExprPtr) -> ((Ptr CInt) -> ((OutConstraintSeqPtr) -> ((OutExceptionPtr) -> (IO CInt)))))))