{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE FunctionalDependencies #-}
{-# LANGUAGE Trustworthy #-}
{-# LANGUAGE TypeFamilies #-}

-- |
-- Module      :   Grisette.Internal.Core.Data.Class.Function
-- Copyright   :   (c) Sirui Lu 2021-2023
-- License     :   BSD-3-Clause (see the LICENSE file)
--
-- Maintainer  :   siruilu@cs.washington.edu
-- Stability   :   Experimental
-- Portability :   GHC only
module Grisette.Internal.Core.Data.Class.Function
  ( -- * Function operations
    Function (..),
    Apply (..),
  )
where

-- $setup
-- >>> import Grisette.Core
-- >>> import Grisette.SymPrim

-- | Abstraction for function-like types.
class Function f arg ret | f -> arg ret where
  -- | Function application operator.
  --
  -- The operator is not right associated (like `($)`). It is left associated,
  -- and you can provide many arguments with this operator once at a time.
  --
  -- >>> (+1) # 2
  -- 3
  --
  -- >>> (+) # 2 # 3
  -- 5
  (#) :: f -> arg -> ret

  infixl 9 #

instance Function (a -> b) a b where
  a -> b
f # :: (a -> b) -> a -> b
# a
a = a -> b
f a
a

-- | Applying an uninterpreted function.
--
-- >>> let f = "f" :: SymInteger =~> SymInteger =~> SymInteger
-- >>> apply f "a" "b"
-- (apply (apply f a) b)
--
-- Note that for implementation reasons, you can also use `apply` function on
-- a non-function symbolic value. In this case, the function is treated as an
-- `id` function.
class Apply uf where
  type FunType uf
  apply :: uf -> FunType uf

instance Apply Integer where
  type FunType Integer = Integer
  apply :: Integer -> FunType Integer
apply = Integer -> Integer
Integer -> FunType Integer
forall a. a -> a
id

instance Apply Bool where
  type FunType Bool = Bool
  apply :: Bool -> FunType Bool
apply = Bool -> Bool
Bool -> FunType Bool
forall a. a -> a
id

instance (Apply b) => Apply (a -> b) where
  type FunType (a -> b) = a -> FunType b
  apply :: (a -> b) -> FunType (a -> b)
apply a -> b
f a
a = b -> FunType b
forall uf. Apply uf => uf -> FunType uf
apply (a -> b
f a
a)