{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE TypeOperators #-}

-- |
-- Module      :   Grisette.IR.SymPrim.Data.Prim.PartialEval.GeneralFun
-- 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.IR.SymPrim.Data.Prim.PartialEval.GeneralFun
  ( pevalGeneralFunApplyTerm,
  )
where

import Grisette.IR.SymPrim.Data.Prim.InternedTerm.InternedCtors
  ( generalFunApplyTerm,
  )
import Grisette.IR.SymPrim.Data.Prim.InternedTerm.Term
  ( SupportedPrim,
    Term (ConTerm, ITETerm),
    type (-->) (GeneralFun),
  )
import {-# SOURCE #-} Grisette.IR.SymPrim.Data.Prim.InternedTerm.TermSubstitution
  ( substTerm,
  )
import Grisette.IR.SymPrim.Data.Prim.PartialEval.Bool (pevalITETerm)
import Grisette.IR.SymPrim.Data.Prim.PartialEval.PartialEval
  ( totalize2,
  )

pevalGeneralFunApplyTerm :: (SupportedPrim a, SupportedPrim b) => Term (a --> b) -> Term a -> Term b
pevalGeneralFunApplyTerm :: forall a b.
(SupportedPrim a, SupportedPrim b) =>
Term (a --> b) -> Term a -> Term b
pevalGeneralFunApplyTerm = (Term (a --> b) -> PartialFun (Term a) (Term b))
-> (Term (a --> b) -> Term a -> Term b)
-> Term (a --> b)
-> Term a
-> Term b
forall a b c. (a -> PartialFun b c) -> (a -> b -> c) -> a -> b -> c
totalize2 Term (a --> b) -> PartialFun (Term a) (Term b)
forall a b.
(SupportedPrim a, SupportedPrim b) =>
Term (a --> b) -> Term a -> Maybe (Term b)
doPevalGeneralFunApplyTerm Term (a --> b) -> Term a -> Term b
forall a b.
(SupportedPrim a, SupportedPrim b) =>
Term (a --> b) -> Term a -> Term b
generalFunApplyTerm

doPevalGeneralFunApplyTerm :: (SupportedPrim a, SupportedPrim b) => Term (a --> b) -> Term a -> Maybe (Term b)
doPevalGeneralFunApplyTerm :: forall a b.
(SupportedPrim a, SupportedPrim b) =>
Term (a --> b) -> Term a -> Maybe (Term b)
doPevalGeneralFunApplyTerm (ConTerm Id
_ (GeneralFun TypedSymbol a
arg Term b
tm)) Term a
v = Term b -> Maybe (Term b)
forall a. a -> Maybe a
Just (Term b -> Maybe (Term b)) -> Term b -> Maybe (Term b)
forall a b. (a -> b) -> a -> b
$ TypedSymbol a -> Term a -> Term b -> Term b
forall a b.
(SupportedPrim a, SupportedPrim b) =>
TypedSymbol a -> Term a -> Term b -> Term b
substTerm TypedSymbol a
arg Term a
v Term b
tm
doPevalGeneralFunApplyTerm (ITETerm Id
_ Term Bool
c Term (a --> b)
l Term (a --> b)
r) Term a
v =
  Term b -> Maybe (Term b)
forall a. a -> Maybe a
forall (m :: * -> *) a. Monad m => a -> m a
return (Term b -> Maybe (Term b)) -> Term b -> Maybe (Term b)
forall a b. (a -> b) -> a -> b
$ Term Bool -> Term b -> Term b -> Term b
forall a.
SupportedPrim a =>
Term Bool -> Term a -> Term a -> Term a
pevalITETerm Term Bool
c (Term (a --> b) -> Term a -> Term b
forall a b.
(SupportedPrim a, SupportedPrim b) =>
Term (a --> b) -> Term a -> Term b
pevalGeneralFunApplyTerm Term (a --> b)
l Term a
v) (Term (a --> b) -> Term a -> Term b
forall a b.
(SupportedPrim a, SupportedPrim b) =>
Term (a --> b) -> Term a -> Term b
pevalGeneralFunApplyTerm Term (a --> b)
r Term a
v)
doPevalGeneralFunApplyTerm Term (a --> b)
_ Term a
_ = Maybe (Term b)
forall a. Maybe a
Nothing