{-# LANGUAGE DataKinds #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE TypeApplications #-}
{-# LANGUAGE TypeOperators #-}
{-# LANGUAGE UndecidableInstances #-}
{-# OPTIONS_GHC -Wno-unrecognised-pragmas #-}

{-# HLINT ignore "Eta reduce" #-}

-- |
-- Module      :   Grisette.Internal.SymPrim.Prim.Internal.Instances.PEvalOrdTerm
-- 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.Prim.Internal.Instances.PEvalOrdTerm
  ( pevalGeneralLtOrdTerm,
    pevalGeneralLeOrdTerm,
  )
where

import Control.Monad (msum)
import GHC.TypeNats (KnownNat, type (<=))
import Grisette.Internal.SymPrim.BV (IntN, WordN)
import Grisette.Internal.SymPrim.Prim.Internal.Instances.PEvalNumTerm ()
import Grisette.Internal.SymPrim.Prim.Internal.IsZero (IsZeroCases (IsZeroEvidence, NonZeroEvidence), KnownIsZero (isZero))
import Grisette.Internal.SymPrim.Prim.Internal.Term
  ( PEvalNumTerm (pevalNegNumTerm),
    PEvalOrdTerm (pevalLeOrdTerm, pevalLtOrdTerm, withSbvOrdTermConstraint),
    SupportedPrim (withPrim),
    Term (AddNumTerm, ConTerm),
    conTerm,
    leOrdTerm,
    ltOrdTerm,
    pevalSubNumTerm,
  )
import Grisette.Internal.SymPrim.Prim.Internal.Unfold (binaryUnfoldOnce)

-- Lt
pevalGeneralLtOrdTerm :: (PEvalOrdTerm a) => Term a -> Term a -> Term Bool
pevalGeneralLtOrdTerm :: forall a. PEvalOrdTerm a => Term a -> Term a -> Term Bool
pevalGeneralLtOrdTerm = PartialRuleBinary a a Bool
-> TotalRuleBinary a a Bool -> TotalRuleBinary a a Bool
forall a b c.
(Typeable a, Typeable b, SupportedPrim c) =>
PartialRuleBinary a b c
-> TotalRuleBinary a b c -> TotalRuleBinary a b c
binaryUnfoldOnce PartialRuleBinary a a Bool
forall a. PEvalOrdTerm a => Term a -> Term a -> Maybe (Term Bool)
doPevalGeneralLtOrdTerm TotalRuleBinary a a Bool
forall a. PEvalOrdTerm a => Term a -> Term a -> Term Bool
ltOrdTerm

doPevalGeneralLtOrdTerm ::
  (PEvalOrdTerm a) => Term a -> Term a -> Maybe (Term Bool)
doPevalGeneralLtOrdTerm :: forall a. PEvalOrdTerm a => Term a -> Term a -> Maybe (Term Bool)
doPevalGeneralLtOrdTerm (ConTerm Id
_ a
a) (ConTerm Id
_ a
b) = Term Bool -> Maybe (Term Bool)
forall a. a -> Maybe a
Just (Term Bool -> Maybe (Term Bool)) -> Term Bool -> Maybe (Term Bool)
forall a b. (a -> b) -> a -> b
$ Bool -> Term Bool
forall t.
(SupportedPrim t, Typeable t, Hashable t, Eq t, Show t) =>
t -> Term t
conTerm (Bool -> Term Bool) -> Bool -> Term Bool
forall a b. (a -> b) -> a -> b
$ a
a a -> a -> Bool
forall a. Ord a => a -> a -> Bool
< a
b
doPevalGeneralLtOrdTerm Term a
_ Term a
_ = Maybe (Term Bool)
forall a. Maybe a
Nothing

-- Le
pevalGeneralLeOrdTerm :: (PEvalOrdTerm a) => Term a -> Term a -> Term Bool
pevalGeneralLeOrdTerm :: forall a. PEvalOrdTerm a => Term a -> Term a -> Term Bool
pevalGeneralLeOrdTerm = PartialRuleBinary a a Bool
-> TotalRuleBinary a a Bool -> TotalRuleBinary a a Bool
forall a b c.
(Typeable a, Typeable b, SupportedPrim c) =>
PartialRuleBinary a b c
-> TotalRuleBinary a b c -> TotalRuleBinary a b c
binaryUnfoldOnce PartialRuleBinary a a Bool
forall a. PEvalOrdTerm a => Term a -> Term a -> Maybe (Term Bool)
doPevalGeneralLeOrdTerm TotalRuleBinary a a Bool
forall a. PEvalOrdTerm a => Term a -> Term a -> Term Bool
leOrdTerm

doPevalGeneralLeOrdTerm ::
  (PEvalOrdTerm a) => Term a -> Term a -> Maybe (Term Bool)
doPevalGeneralLeOrdTerm :: forall a. PEvalOrdTerm a => Term a -> Term a -> Maybe (Term Bool)
doPevalGeneralLeOrdTerm (ConTerm Id
_ a
a) (ConTerm Id
_ a
b) = Term Bool -> Maybe (Term Bool)
forall a. a -> Maybe a
Just (Term Bool -> Maybe (Term Bool)) -> Term Bool -> Maybe (Term Bool)
forall a b. (a -> b) -> a -> b
$ Bool -> Term Bool
forall t.
(SupportedPrim t, Typeable t, Hashable t, Eq t, Show t) =>
t -> Term t
conTerm (Bool -> Term Bool) -> Bool -> Term Bool
forall a b. (a -> b) -> a -> b
$ a
a a -> a -> Bool
forall a. Ord a => a -> a -> Bool
<= a
b
doPevalGeneralLeOrdTerm Term a
_ Term a
_ = Maybe (Term Bool)
forall a. Maybe a
Nothing

instance PEvalOrdTerm Integer where
  pevalLtOrdTerm :: Term Integer -> Term Integer -> Term Bool
pevalLtOrdTerm = PartialRuleBinary Integer Integer Bool
-> (Term Integer -> Term Integer -> Term Bool)
-> Term Integer
-> Term Integer
-> Term Bool
forall a b c.
(Typeable a, Typeable b, SupportedPrim c) =>
PartialRuleBinary a b c
-> TotalRuleBinary a b c -> TotalRuleBinary a b c
binaryUnfoldOnce PartialRuleBinary Integer Integer Bool
forall {a}.
(PEvalOrdTerm a, PEvalNumTerm a) =>
Term a -> Term a -> Maybe (Term Bool)
doPevalLtOrdTerm Term Integer -> Term Integer -> Term Bool
forall a. PEvalOrdTerm a => Term a -> Term a -> Term Bool
ltOrdTerm
    where
      doPevalLtOrdTerm :: Term a -> Term a -> Maybe (Term Bool)
doPevalLtOrdTerm Term a
l Term a
r =
        [Maybe (Term Bool)] -> Maybe (Term Bool)
forall (t :: * -> *) (m :: * -> *) a.
(Foldable t, MonadPlus m) =>
t (m a) -> m a
msum
          [ Term a -> Term a -> Maybe (Term Bool)
forall a. PEvalOrdTerm a => Term a -> Term a -> Maybe (Term Bool)
doPevalGeneralLtOrdTerm Term a
l Term a
r,
            case (Term a
l, Term a
r) of
              (ConTerm Id
_ a
l, AddNumTerm Id
_ (ConTerm Id
_ a
j) Term a
k) ->
                Term Bool -> Maybe (Term Bool)
forall a. a -> Maybe a
Just (Term Bool -> Maybe (Term Bool)) -> Term Bool -> Maybe (Term Bool)
forall a b. (a -> b) -> a -> b
$ Term a -> Term a -> Term Bool
forall a. PEvalOrdTerm a => Term a -> Term a -> Term Bool
pevalLtOrdTerm (a -> Term a
forall t.
(SupportedPrim t, Typeable t, Hashable t, Eq t, Show t) =>
t -> Term t
conTerm (a -> Term a) -> a -> Term a
forall a b. (a -> b) -> a -> b
$ a
l a -> a -> a
forall a. Num a => a -> a -> a
- a
j) Term a
k
              (AddNumTerm Id
_ (ConTerm Id
_ a
i) Term a
j, ConTerm Id
_ a
k) ->
                Term Bool -> Maybe (Term Bool)
forall a. a -> Maybe a
Just (Term Bool -> Maybe (Term Bool)) -> Term Bool -> Maybe (Term Bool)
forall a b. (a -> b) -> a -> b
$ Term a -> Term a -> Term Bool
forall a. PEvalOrdTerm a => Term a -> Term a -> Term Bool
pevalLtOrdTerm Term a
j (a -> Term a
forall t.
(SupportedPrim t, Typeable t, Hashable t, Eq t, Show t) =>
t -> Term t
conTerm (a -> Term a) -> a -> Term a
forall a b. (a -> b) -> a -> b
$ a
k a -> a -> a
forall a. Num a => a -> a -> a
- a
i)
              ((AddNumTerm Id
_ (ConTerm Id
_ a
j) Term a
k), Term a
l) ->
                Term Bool -> Maybe (Term Bool)
forall a. a -> Maybe a
Just (Term Bool -> Maybe (Term Bool)) -> Term Bool -> Maybe (Term Bool)
forall a b. (a -> b) -> a -> b
$
                  Term a -> Term a -> Term Bool
forall a. PEvalOrdTerm a => Term a -> Term a -> Term Bool
pevalLtOrdTerm
                    (a -> Term a
forall t.
(SupportedPrim t, Typeable t, Hashable t, Eq t, Show t) =>
t -> Term t
conTerm a
j)
                    (Term a -> Term a -> Term a
forall a. PEvalNumTerm a => Term a -> Term a -> Term a
pevalSubNumTerm Term a
l Term a
k)
              (Term a
j, (AddNumTerm Id
_ (ConTerm Id
_ a
k) Term a
l)) ->
                Term Bool -> Maybe (Term Bool)
forall a. a -> Maybe a
Just (Term Bool -> Maybe (Term Bool)) -> Term Bool -> Maybe (Term Bool)
forall a b. (a -> b) -> a -> b
$ Term a -> Term a -> Term Bool
forall a. PEvalOrdTerm a => Term a -> Term a -> Term Bool
pevalLtOrdTerm (a -> Term a
forall t.
(SupportedPrim t, Typeable t, Hashable t, Eq t, Show t) =>
t -> Term t
conTerm (a -> Term a) -> a -> Term a
forall a b. (a -> b) -> a -> b
$ -a
k) (Term a -> Term a -> Term a
forall a. PEvalNumTerm a => Term a -> Term a -> Term a
pevalSubNumTerm Term a
l Term a
j)
              (Term a
l, ConTerm Id
_ a
r) ->
                Term Bool -> Maybe (Term Bool)
forall a. a -> Maybe a
Just (Term Bool -> Maybe (Term Bool)) -> Term Bool -> Maybe (Term Bool)
forall a b. (a -> b) -> a -> b
$ Term a -> Term a -> Term Bool
forall a. PEvalOrdTerm a => Term a -> Term a -> Term Bool
pevalLtOrdTerm (a -> Term a
forall t.
(SupportedPrim t, Typeable t, Hashable t, Eq t, Show t) =>
t -> Term t
conTerm (a -> Term a) -> a -> Term a
forall a b. (a -> b) -> a -> b
$ -a
r) (Term a -> Term a
forall t. PEvalNumTerm t => Term t -> Term t
pevalNegNumTerm Term a
l)
              (Term a, Term a)
_ -> Maybe (Term Bool)
forall a. Maybe a
Nothing
          ]
  pevalLeOrdTerm :: Term Integer -> Term Integer -> Term Bool
pevalLeOrdTerm = PartialRuleBinary Integer Integer Bool
-> (Term Integer -> Term Integer -> Term Bool)
-> Term Integer
-> Term Integer
-> Term Bool
forall a b c.
(Typeable a, Typeable b, SupportedPrim c) =>
PartialRuleBinary a b c
-> TotalRuleBinary a b c -> TotalRuleBinary a b c
binaryUnfoldOnce PartialRuleBinary Integer Integer Bool
forall {a}.
(PEvalOrdTerm a, PEvalNumTerm a) =>
Term a -> Term a -> Maybe (Term Bool)
doPevalLeOrdTerm Term Integer -> Term Integer -> Term Bool
forall a. PEvalOrdTerm a => Term a -> Term a -> Term Bool
leOrdTerm
    where
      doPevalLeOrdTerm :: Term a -> Term a -> Maybe (Term Bool)
doPevalLeOrdTerm Term a
l Term a
r =
        [Maybe (Term Bool)] -> Maybe (Term Bool)
forall (t :: * -> *) (m :: * -> *) a.
(Foldable t, MonadPlus m) =>
t (m a) -> m a
msum
          [ Term a -> Term a -> Maybe (Term Bool)
forall a. PEvalOrdTerm a => Term a -> Term a -> Maybe (Term Bool)
doPevalGeneralLeOrdTerm Term a
l Term a
r,
            case (Term a
l, Term a
r) of
              (ConTerm Id
_ a
l, AddNumTerm Id
_ (ConTerm Id
_ a
j) Term a
k) ->
                Term Bool -> Maybe (Term Bool)
forall a. a -> Maybe a
Just (Term Bool -> Maybe (Term Bool)) -> Term Bool -> Maybe (Term Bool)
forall a b. (a -> b) -> a -> b
$ Term a -> Term a -> Term Bool
forall a. PEvalOrdTerm a => Term a -> Term a -> Term Bool
pevalLeOrdTerm (a -> Term a
forall t.
(SupportedPrim t, Typeable t, Hashable t, Eq t, Show t) =>
t -> Term t
conTerm (a -> Term a) -> a -> Term a
forall a b. (a -> b) -> a -> b
$ a
l a -> a -> a
forall a. Num a => a -> a -> a
- a
j) Term a
k
              (AddNumTerm Id
_ (ConTerm Id
_ a
i) Term a
j, ConTerm Id
_ a
k) ->
                Term Bool -> Maybe (Term Bool)
forall a. a -> Maybe a
Just (Term Bool -> Maybe (Term Bool)) -> Term Bool -> Maybe (Term Bool)
forall a b. (a -> b) -> a -> b
$ Term a -> Term a -> Term Bool
forall a. PEvalOrdTerm a => Term a -> Term a -> Term Bool
pevalLeOrdTerm Term a
j (a -> Term a
forall t.
(SupportedPrim t, Typeable t, Hashable t, Eq t, Show t) =>
t -> Term t
conTerm (a -> Term a) -> a -> Term a
forall a b. (a -> b) -> a -> b
$ a
k a -> a -> a
forall a. Num a => a -> a -> a
- a
i)
              (AddNumTerm Id
_ (ConTerm Id
_ a
j) Term a
k, Term a
l) ->
                Term Bool -> Maybe (Term Bool)
forall a. a -> Maybe a
Just (Term Bool -> Maybe (Term Bool)) -> Term Bool -> Maybe (Term Bool)
forall a b. (a -> b) -> a -> b
$ Term a -> Term a -> Term Bool
forall a. PEvalOrdTerm a => Term a -> Term a -> Term Bool
pevalLeOrdTerm (a -> Term a
forall t.
(SupportedPrim t, Typeable t, Hashable t, Eq t, Show t) =>
t -> Term t
conTerm a
j) (Term a -> Term a -> Term a
forall a. PEvalNumTerm a => Term a -> Term a -> Term a
pevalSubNumTerm Term a
l Term a
k)
              (Term a
j, AddNumTerm Id
_ (ConTerm Id
_ a
k) Term a
l) ->
                Term Bool -> Maybe (Term Bool)
forall a. a -> Maybe a
Just (Term Bool -> Maybe (Term Bool)) -> Term Bool -> Maybe (Term Bool)
forall a b. (a -> b) -> a -> b
$ Term a -> Term a -> Term Bool
forall a. PEvalOrdTerm a => Term a -> Term a -> Term Bool
pevalLeOrdTerm (a -> Term a
forall t.
(SupportedPrim t, Typeable t, Hashable t, Eq t, Show t) =>
t -> Term t
conTerm (a -> Term a) -> a -> Term a
forall a b. (a -> b) -> a -> b
$ -a
k) (Term a -> Term a -> Term a
forall a. PEvalNumTerm a => Term a -> Term a -> Term a
pevalSubNumTerm Term a
l Term a
j)
              (Term a
l, ConTerm Id
_ a
r) ->
                Term Bool -> Maybe (Term Bool)
forall a. a -> Maybe a
Just (Term Bool -> Maybe (Term Bool)) -> Term Bool -> Maybe (Term Bool)
forall a b. (a -> b) -> a -> b
$ Term a -> Term a -> Term Bool
forall a. PEvalOrdTerm a => Term a -> Term a -> Term Bool
pevalLeOrdTerm (a -> Term a
forall t.
(SupportedPrim t, Typeable t, Hashable t, Eq t, Show t) =>
t -> Term t
conTerm (a -> Term a) -> a -> Term a
forall a b. (a -> b) -> a -> b
$ -a
r) (Term a -> Term a
forall t. PEvalNumTerm t => Term t -> Term t
pevalNegNumTerm Term a
l)
              (Term a, Term a)
_ -> Maybe (Term Bool)
forall a. Maybe a
Nothing
          ]
  withSbvOrdTermConstraint :: forall (n :: Nat) (proxy :: Nat -> *) r.
KnownIsZero n =>
proxy n -> (OrdSymbolic (SBVType n Integer) => r) -> r
withSbvOrdTermConstraint proxy n
p OrdSymbolic (SBVType n Integer) => r
r = case proxy n -> IsZeroCases n
forall (a :: Nat) (proxy :: Nat -> *).
KnownIsZero a =>
proxy a -> IsZeroCases a
forall (proxy :: Nat -> *). proxy n -> IsZeroCases n
isZero proxy n
p of
    IsZeroCases n
IsZeroEvidence -> r
OrdSymbolic (SBVType n Integer) => r
r
    IsZeroCases n
NonZeroEvidence -> r
OrdSymbolic (SBVType n Integer) => r
r

instance (KnownNat n, 1 <= n) => PEvalOrdTerm (WordN n) where
  pevalLtOrdTerm :: Term (WordN n) -> Term (WordN n) -> Term Bool
pevalLtOrdTerm = Term (WordN n) -> Term (WordN n) -> Term Bool
forall a. PEvalOrdTerm a => Term a -> Term a -> Term Bool
pevalGeneralLtOrdTerm
  pevalLeOrdTerm :: Term (WordN n) -> Term (WordN n) -> Term Bool
pevalLeOrdTerm = Term (WordN n) -> Term (WordN n) -> Term Bool
forall a. PEvalOrdTerm a => Term a -> Term a -> Term Bool
pevalGeneralLeOrdTerm
  withSbvOrdTermConstraint :: forall (n :: Nat) (proxy :: Nat -> *) r.
KnownIsZero n =>
proxy n -> (OrdSymbolic (SBVType n (WordN n)) => r) -> r
withSbvOrdTermConstraint proxy n
p OrdSymbolic (SBVType n (WordN n)) => r
r = forall t (n :: Nat) (p :: Nat -> *) a.
(SupportedPrim t, KnownIsZero n) =>
p n
-> ((PrimConstraint n t, SMTDefinable (SBVType n t),
     Mergeable (SBVType n t), Typeable (SBVType n t)) =>
    a)
-> a
withPrim @(WordN n) proxy n
p r
OrdSymbolic (SBVType n (WordN n)) => r
(PrimConstraint n (WordN n), SMTDefinable (SBVType n (WordN n)),
 Mergeable (SBVType n (WordN n)), Typeable (SBVType n (WordN n))) =>
r
r

instance (KnownNat n, 1 <= n) => PEvalOrdTerm (IntN n) where
  pevalLtOrdTerm :: Term (IntN n) -> Term (IntN n) -> Term Bool
pevalLtOrdTerm = Term (IntN n) -> Term (IntN n) -> Term Bool
forall a. PEvalOrdTerm a => Term a -> Term a -> Term Bool
pevalGeneralLtOrdTerm
  pevalLeOrdTerm :: Term (IntN n) -> Term (IntN n) -> Term Bool
pevalLeOrdTerm = Term (IntN n) -> Term (IntN n) -> Term Bool
forall a. PEvalOrdTerm a => Term a -> Term a -> Term Bool
pevalGeneralLeOrdTerm
  withSbvOrdTermConstraint :: forall (n :: Nat) (proxy :: Nat -> *) r.
KnownIsZero n =>
proxy n -> (OrdSymbolic (SBVType n (IntN n)) => r) -> r
withSbvOrdTermConstraint proxy n
p OrdSymbolic (SBVType n (IntN n)) => r
r = forall t (n :: Nat) (p :: Nat -> *) a.
(SupportedPrim t, KnownIsZero n) =>
p n
-> ((PrimConstraint n t, SMTDefinable (SBVType n t),
     Mergeable (SBVType n t), Typeable (SBVType n t)) =>
    a)
-> a
withPrim @(IntN n) proxy n
p r
OrdSymbolic (SBVType n (IntN n)) => r
(PrimConstraint n (IntN n), SMTDefinable (SBVType n (IntN n)),
 Mergeable (SBVType n (IntN n)), Typeable (SBVType n (IntN n))) =>
r
r