{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE TemplateHaskell #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE TypeOperators #-}
{-# LANGUAGE UndecidableInstances #-}
{-# OPTIONS_GHC -Wno-unrecognised-pragmas #-}

{-# HLINT ignore "Unused LANGUAGE pragma" #-}

-- |
-- Module      :   Grisette.Internal.SymPrim.SymTabularFun
-- Copyright   :   (c) Sirui Lu 2024
-- License     :   BSD-3-Clause (see the LICENSE file)
--
-- Maintainer  :   siruilu@cs.washington.edu
-- Stability   :   Experimental
-- Portability :   GHC only
module Grisette.Internal.SymPrim.SymTabularFun (type (=~>) (..)) where

import Control.DeepSeq (NFData (rnf))
import Data.Hashable (Hashable (hashWithSalt))
import Data.String (IsString (fromString))
import Grisette.Internal.Core.Data.Class.Function
  ( Apply (FunType, apply),
    Function ((#)),
  )
import Grisette.Internal.Core.Data.Class.Solvable
  ( Solvable (con, conView, ssym, sym),
  )
import Grisette.Internal.SymPrim.AllSyms (AllSyms (allSymsS), SomeSym (SomeSym))
import Grisette.Internal.SymPrim.Prim.Term
  ( ConRep (ConType),
    LinkedRep (underlyingTerm, wrapTerm),
    PEvalApplyTerm (pevalApplyTerm),
    SupportedPrim,
    SymRep (SymType),
    Term (ConTerm),
    conTerm,
    pformat,
    symTerm,
  )
import Grisette.Internal.SymPrim.TabularFun (type (=->))
import Language.Haskell.TH.Syntax (Lift (liftTyped))

-- $setup
-- >>> import Grisette.Core
-- >>> import Grisette.SymPrim
-- >>> import Grisette.Backend
-- >>> import Data.Proxy

-- | Symbolic tabular function type.
--
-- >>> :set -XTypeOperators -XOverloadedStrings
-- >>> f' = "f" :: SymInteger =~> SymInteger
-- >>> f = (f' #)
-- >>> f 1
-- (apply f 1)
--
-- >>> f' = con (TabularFun [(1, 2), (2, 3)] 4) :: SymInteger =~> SymInteger
-- >>> f = (f' #)
-- >>> f 1
-- 2
-- >>> f 2
-- 3
-- >>> f 3
-- 4
-- >>> f "b"
-- (ite (= b 1) 2 (ite (= b 2) 3 4))
data sa =~> sb where
  SymTabularFun ::
    (LinkedRep ca sa, LinkedRep cb sb) =>
    Term (ca =-> cb) ->
    sa =~> sb

infixr 0 =~>

instance Lift (sa =~> sb) where
  liftTyped :: forall (m :: * -> *). Quote m => (sa =~> sb) -> Code m (sa =~> sb)
liftTyped (SymTabularFun Term (ca =-> cb)
t) = [||Term (ca =-> cb) -> sa =~> sb
forall ca sa cb sb.
(LinkedRep ca sa, LinkedRep cb sb) =>
Term (ca =-> cb) -> sa =~> sb
SymTabularFun Term (ca =-> cb)
t||]

instance NFData (sa =~> sb) where
  rnf :: (sa =~> sb) -> ()
rnf (SymTabularFun Term (ca =-> cb)
t) = Term (ca =-> cb) -> ()
forall a. NFData a => a -> ()
rnf Term (ca =-> cb)
t

instance (ConRep a, ConRep b) => ConRep (a =~> b) where
  type ConType (a =~> b) = ConType a =-> ConType b

instance (SymRep a, SymRep b, SupportedPrim (a =-> b)) => SymRep (a =-> b) where
  type SymType (a =-> b) = SymType a =~> SymType b

instance
  (LinkedRep ca sa, LinkedRep cb sb, SupportedPrim (ca =-> cb)) =>
  LinkedRep (ca =-> cb) (sa =~> sb)
  where
  underlyingTerm :: (sa =~> sb) -> Term (ca =-> cb)
underlyingTerm (SymTabularFun Term (ca =-> cb)
a) = Term (ca =-> cb)
Term (ca =-> cb)
a
  wrapTerm :: Term (ca =-> cb) -> sa =~> sb
wrapTerm = Term (ca =-> cb) -> sa =~> sb
forall ca sa cb sb.
(LinkedRep ca sa, LinkedRep cb sb) =>
Term (ca =-> cb) -> sa =~> sb
SymTabularFun

instance
  ( SupportedPrim ca,
    SupportedPrim cb,
    LinkedRep ca sa,
    LinkedRep cb sb,
    SupportedPrim (ca =-> cb)
  ) =>
  Function (sa =~> sb) sa sb
  where
  (SymTabularFun Term (ca =-> cb)
f) # :: (sa =~> sb) -> sa -> sb
# sa
t = Term cb -> sb
forall con sym. LinkedRep con sym => Term con -> sym
wrapTerm (Term cb -> sb) -> Term cb -> sb
forall a b. (a -> b) -> a -> b
$ Term (ca =-> cb) -> Term ca -> Term cb
forall f a b. PEvalApplyTerm f a b => Term f -> Term a -> Term b
pevalApplyTerm Term (ca =-> cb)
f (sa -> Term ca
forall con sym. LinkedRep con sym => sym -> Term con
underlyingTerm sa
t)

instance
  ( LinkedRep ca sa,
    LinkedRep ct st,
    Apply st,
    SupportedPrim ca,
    SupportedPrim ct,
    SupportedPrim (ca =-> ct)
  ) =>
  Apply (sa =~> st)
  where
  type FunType (sa =~> st) = sa -> FunType st
  apply :: (sa =~> st) -> FunType (sa =~> st)
apply sa =~> st
uf sa
a = st -> FunType st
forall uf. Apply uf => uf -> FunType uf
apply (sa =~> st
uf (sa =~> st) -> sa -> st
forall f arg ret. Function f arg ret => f -> arg -> ret
# sa
a)

instance
  ( SupportedPrim ca,
    SupportedPrim cb,
    LinkedRep ca sa,
    LinkedRep cb sb,
    SupportedPrim (ca =-> cb)
  ) =>
  Solvable (ca =-> cb) (sa =~> sb)
  where
  con :: (ca =-> cb) -> sa =~> sb
con = Term (ca =-> cb) -> sa =~> sb
forall ca sa cb sb.
(LinkedRep ca sa, LinkedRep cb sb) =>
Term (ca =-> cb) -> sa =~> sb
SymTabularFun (Term (ca =-> cb) -> sa =~> sb)
-> ((ca =-> cb) -> Term (ca =-> cb)) -> (ca =-> cb) -> sa =~> sb
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (ca =-> cb) -> Term (ca =-> cb)
forall t.
(SupportedPrim t, Typeable t, Hashable t, Eq t, Show t) =>
t -> Term t
conTerm
  sym :: Symbol -> sa =~> sb
sym = Term (ca =-> cb) -> sa =~> sb
forall ca sa cb sb.
(LinkedRep ca sa, LinkedRep cb sb) =>
Term (ca =-> cb) -> sa =~> sb
SymTabularFun (Term (ca =-> cb) -> sa =~> sb)
-> (Symbol -> Term (ca =-> cb)) -> Symbol -> sa =~> sb
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Symbol -> Term (ca =-> cb)
forall t. (SupportedPrim t, Typeable t) => Symbol -> Term t
symTerm
  conView :: (sa =~> sb) -> Maybe (ca =-> cb)
conView (SymTabularFun (ConTerm Int
_ ca =-> cb
t)) = (ca =-> cb) -> Maybe (ca =-> cb)
forall a. a -> Maybe a
Just ca =-> cb
ca =-> cb
t
  conView sa =~> sb
_ = Maybe (ca =-> cb)
forall a. Maybe a
Nothing

instance
  ( SupportedPrim (ca =-> cb),
    LinkedRep ca sa,
    LinkedRep cb sb
  ) =>
  IsString (sa =~> sb)
  where
  fromString :: String -> sa =~> sb
fromString = Identifier -> sa =~> sb
forall c t. Solvable c t => Identifier -> t
ssym (Identifier -> sa =~> sb)
-> (String -> Identifier) -> String -> sa =~> sb
forall b c a. (b -> c) -> (a -> b) -> a -> c
. String -> Identifier
forall a. IsString a => String -> a
fromString

instance
  (SupportedPrim (ca =-> cb), LinkedRep ca sa, LinkedRep cb sb) =>
  Show (sa =~> sb)
  where
  show :: (sa =~> sb) -> String
show (SymTabularFun Term (ca =-> cb)
t) = Term (ca =-> cb) -> String
forall t. SupportedPrim t => Term t -> String
pformat Term (ca =-> cb)
t

instance
  (SupportedPrim (ca =-> cb), LinkedRep ca sa, LinkedRep cb sb) =>
  Eq (sa =~> sb)
  where
  SymTabularFun Term (ca =-> cb)
l == :: (sa =~> sb) -> (sa =~> sb) -> Bool
== SymTabularFun Term (ca =-> cb)
r = Term (ca =-> cb)
l Term (ca =-> cb) -> Term (ca =-> cb) -> Bool
forall a. Eq a => a -> a -> Bool
== Term (ca =-> cb)
Term (ca =-> cb)
r

instance
  (SupportedPrim (ca =-> cb), LinkedRep ca sa, LinkedRep cb sb) =>
  Hashable (sa =~> sb)
  where
  hashWithSalt :: Int -> (sa =~> sb) -> Int
hashWithSalt Int
s (SymTabularFun Term (ca =-> cb)
v) = Int
s Int -> Term (ca =-> cb) -> Int
forall a. Hashable a => Int -> a -> Int
`hashWithSalt` Term (ca =-> cb)
v

instance
  (SupportedPrim (ca =-> cb), LinkedRep ca sa, LinkedRep cb sb) =>
  AllSyms (sa =~> sb)
  where
  allSymsS :: (sa =~> sb) -> [SomeSym] -> [SomeSym]
allSymsS sa =~> sb
v = ((sa =~> sb) -> SomeSym
forall con sym. LinkedRep con sym => sym -> SomeSym
SomeSym sa =~> sb
v SomeSym -> [SomeSym] -> [SomeSym]
forall a. a -> [a] -> [a]
:)