{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE PatternSynonyms #-}
{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE TypeApplications #-}
{-# LANGUAGE ViewPatterns #-}

-- |
-- Module      :   Grisette.IR.SymPrim.Data.Prim.PartialEval.Num
-- 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.Num
  ( pattern NumConTerm,
    pattern NumOrdConTerm,
    pevalAddNumTerm,
    pevalMinusNumTerm,
    pevalTimesNumTerm,
    pevalUMinusNumTerm,
    pevalAbsNumTerm,
    pevalSignumNumTerm,
    pevalLtNumTerm,
    pevalLeNumTerm,
    pevalGtNumTerm,
    pevalGeNumTerm,
  )
where

import Data.Typeable
import Grisette.IR.SymPrim.Data.Prim.InternedTerm.InternedCtors
import Grisette.IR.SymPrim.Data.Prim.InternedTerm.Term
import Grisette.IR.SymPrim.Data.Prim.PartialEval.Unfold
import Grisette.IR.SymPrim.Data.Prim.Utils
import Unsafe.Coerce

numConTermView :: (Num b, Typeable b) => Term a -> Maybe b
numConTermView :: forall b a. (Num b, Typeable b) => Term a -> Maybe b
numConTermView (ConTerm Id
_ a
b) = forall a b. (Typeable a, Typeable b) => a -> Maybe b
cast a
b
numConTermView Term a
_ = forall a. Maybe a
Nothing

pattern NumConTerm :: forall b a. (Num b, Typeable b) => b -> Term a
pattern $mNumConTerm :: forall {r} {b} {a}.
(Num b, Typeable b) =>
Term a -> (b -> r) -> ((# #) -> r) -> r
NumConTerm b <- (numConTermView -> Just b)

numOrdConTermView :: (Num b, Ord b, Typeable b) => Term a -> Maybe b
numOrdConTermView :: forall b a. (Num b, Ord b, Typeable b) => Term a -> Maybe b
numOrdConTermView (ConTerm Id
_ a
b) = forall a b. (Typeable a, Typeable b) => a -> Maybe b
cast a
b
numOrdConTermView Term a
_ = forall a. Maybe a
Nothing

pattern NumOrdConTerm :: forall b a. (Num b, Ord b, Typeable b) => b -> Term a
pattern $mNumOrdConTerm :: forall {r} {b} {a}.
(Num b, Ord b, Typeable b) =>
Term a -> (b -> r) -> ((# #) -> r) -> r
NumOrdConTerm b <- (numOrdConTermView -> Just b)

-- add
pevalAddNumTerm :: forall a. (Num a, SupportedPrim a) => Term a -> Term a -> Term a
pevalAddNumTerm :: forall a. (Num a, SupportedPrim a) => Term a -> Term a -> Term a
pevalAddNumTerm = forall a b c.
(Typeable a, Typeable b, SupportedPrim c) =>
PartialRuleBinary a b c
-> TotalRuleBinary a b c -> TotalRuleBinary a b c
binaryUnfoldOnce forall a.
(Num a, SupportedPrim a) =>
Term a -> Term a -> Maybe (Term a)
doPevalAddNumTerm (\Term a
a Term a
b -> forall a. (Num a, Typeable a) => Term a -> Term a
normalizeAddNum forall a b. (a -> b) -> a -> b
$ forall a. (SupportedPrim a, Num a) => Term a -> Term a -> Term a
addNumTerm Term a
a Term a
b)

doPevalAddNumTerm :: forall a. (Num a, SupportedPrim a) => Term a -> Term a -> Maybe (Term a)
doPevalAddNumTerm :: forall a.
(Num a, SupportedPrim a) =>
Term a -> Term a -> Maybe (Term a)
doPevalAddNumTerm (ConTerm Id
_ a
a) (ConTerm Id
_ a
b) = forall a. a -> Maybe a
Just forall a b. (a -> b) -> a -> b
$ forall t.
(SupportedPrim t, Typeable t, Hashable t, Eq t, Show t) =>
t -> Term t
conTerm forall a b. (a -> b) -> a -> b
$ a
a forall a. Num a => a -> a -> a
+ a
b
doPevalAddNumTerm l :: Term a
l@(ConTerm Id
_ a
a) Term a
b = case (a
a, Term a
b) of
  (a
0, Term a
k) -> forall a. a -> Maybe a
Just Term a
k
  (a
l1, AddNumTerm Id
_ (ConTerm Id
_ a
j) Term a
k) -> forall a. a -> Maybe a
Just forall a b. (a -> b) -> a -> b
$ forall a. (Num a, SupportedPrim a) => Term a -> Term a -> Term a
pevalAddNumTerm (forall t.
(SupportedPrim t, Typeable t, Hashable t, Eq t, Show t) =>
t -> Term t
conTerm forall a b. (a -> b) -> a -> b
$ a
l1 forall a. Num a => a -> a -> a
+ a
j) Term a
k
  (a, Term a)
_ -> forall a.
(Num a, SupportedPrim a) =>
Term a -> Term a -> Maybe (Term a)
doPevalAddNumTermNoConc Term a
l Term a
b
doPevalAddNumTerm Term a
a r :: Term a
r@(ConTerm Id
_ a
_) = forall a.
(Num a, SupportedPrim a) =>
Term a -> Term a -> Maybe (Term a)
doPevalAddNumTerm Term a
r Term a
a
doPevalAddNumTerm Term a
l Term a
r = forall a.
(Num a, SupportedPrim a) =>
Term a -> Term a -> Maybe (Term a)
doPevalAddNumTermNoConc Term a
l Term a
r

doPevalAddNumTermNoConc :: forall a. (Num a, SupportedPrim a) => Term a -> Term a -> Maybe (Term a)
doPevalAddNumTermNoConc :: forall a.
(Num a, SupportedPrim a) =>
Term a -> Term a -> Maybe (Term a)
doPevalAddNumTermNoConc (AddNumTerm Id
_ i :: Term a
i@ConTerm {} Term a
j) Term a
k = forall a. a -> Maybe a
Just forall a b. (a -> b) -> a -> b
$ forall a. (Num a, SupportedPrim a) => Term a -> Term a -> Term a
pevalAddNumTerm Term a
i forall a b. (a -> b) -> a -> b
$ forall a. (Num a, SupportedPrim a) => Term a -> Term a -> Term a
pevalAddNumTerm Term a
j Term a
k
doPevalAddNumTermNoConc Term a
i (AddNumTerm Id
_ j :: Term a
j@ConTerm {} Term a
k) = forall a. a -> Maybe a
Just forall a b. (a -> b) -> a -> b
$ forall a. (Num a, SupportedPrim a) => Term a -> Term a -> Term a
pevalAddNumTerm Term a
j forall a b. (a -> b) -> a -> b
$ forall a. (Num a, SupportedPrim a) => Term a -> Term a -> Term a
pevalAddNumTerm Term a
i Term a
k
doPevalAddNumTermNoConc (UMinusNumTerm Id
_ Term a
i) (UMinusNumTerm Id
_ Term a
j) = forall a. a -> Maybe a
Just forall a b. (a -> b) -> a -> b
$ forall a. (Num a, SupportedPrim a) => Term a -> Term a
pevalUMinusNumTerm forall a b. (a -> b) -> a -> b
$ forall a. (Num a, SupportedPrim a) => Term a -> Term a -> Term a
pevalAddNumTerm Term a
i Term a
j
doPevalAddNumTermNoConc (TimesNumTerm Id
_ (ConTerm Id
_ a
i) Term a
j) (TimesNumTerm Id
_ (ConTerm Id
_ a
k) Term a
l)
  | Term a
j forall a. Eq a => a -> a -> Bool
== Term a
l = forall a. a -> Maybe a
Just forall a b. (a -> b) -> a -> b
$ forall a. (Num a, SupportedPrim a) => Term a -> Term a -> Term a
pevalTimesNumTerm (forall t.
(SupportedPrim t, Typeable t, Hashable t, Eq t, Show t) =>
t -> Term t
conTerm forall a b. (a -> b) -> a -> b
$ a
i forall a. Num a => a -> a -> a
+ a
k) Term a
j
doPevalAddNumTermNoConc (TimesNumTerm Id
_ i :: Term a
i@ConTerm {} Term a
j) (TimesNumTerm Id
_ k :: Term a
k@(ConTerm Id
_ a
_) Term a
l)
  | Term a
i forall a. Eq a => a -> a -> Bool
== Term a
k = forall a. a -> Maybe a
Just forall a b. (a -> b) -> a -> b
$ forall a. (Num a, SupportedPrim a) => Term a -> Term a -> Term a
pevalTimesNumTerm Term a
i (forall a. (Num a, SupportedPrim a) => Term a -> Term a -> Term a
pevalAddNumTerm Term a
j Term a
l)
doPevalAddNumTermNoConc Term a
_ Term a
_ = forall a. Maybe a
Nothing

normalizeAddNum :: forall a. (Num a, Typeable a) => Term a -> Term a
normalizeAddNum :: forall a. (Num a, Typeable a) => Term a -> Term a
normalizeAddNum (AddNumTerm Id
_ Term a
l r :: Term a
r@(ConTerm Id
_ a
_)) = forall a. (SupportedPrim a, Num a) => Term a -> Term a -> Term a
addNumTerm Term a
r Term a
l
normalizeAddNum Term a
v = Term a
v

pevalMinusNumTerm :: (Num a, SupportedPrim a) => Term a -> Term a -> Term a
pevalMinusNumTerm :: forall a. (Num a, SupportedPrim a) => Term a -> Term a -> Term a
pevalMinusNumTerm Term a
l Term a
r = forall a. (Num a, SupportedPrim a) => Term a -> Term a -> Term a
pevalAddNumTerm Term a
l (forall a. (Num a, SupportedPrim a) => Term a -> Term a
pevalUMinusNumTerm Term a
r)

-- uminus
pevalUMinusNumTerm :: (Num a, SupportedPrim a) => Term a -> Term a
pevalUMinusNumTerm :: forall a. (Num a, SupportedPrim a) => Term a -> Term a
pevalUMinusNumTerm = forall a b.
(Typeable a, SupportedPrim b) =>
PartialRuleUnary a b -> TotalRuleUnary a b -> TotalRuleUnary a b
unaryUnfoldOnce forall a. (Num a, SupportedPrim a) => Term a -> Maybe (Term a)
doPevalUMinusNumTerm forall a. (SupportedPrim a, Num a) => Term a -> Term a
uminusNumTerm

doPevalUMinusNumTerm :: forall a. (Num a, SupportedPrim a) => Term a -> Maybe (Term a)
doPevalUMinusNumTerm :: forall a. (Num a, SupportedPrim a) => Term a -> Maybe (Term a)
doPevalUMinusNumTerm (ConTerm Id
_ a
a) = forall a. a -> Maybe a
Just forall a b. (a -> b) -> a -> b
$ forall t.
(SupportedPrim t, Typeable t, Hashable t, Eq t, Show t) =>
t -> Term t
conTerm forall a b. (a -> b) -> a -> b
$ -a
a
doPevalUMinusNumTerm (UMinusNumTerm Id
_ Term a
v) = forall a. a -> Maybe a
Just Term a
v
doPevalUMinusNumTerm (AddNumTerm Id
_ (NumConTerm a
l) Term a
r) = forall a. a -> Maybe a
Just forall a b. (a -> b) -> a -> b
$ forall a. (Num a, SupportedPrim a) => Term a -> Term a -> Term a
pevalMinusNumTerm (forall t.
(SupportedPrim t, Typeable t, Hashable t, Eq t, Show t) =>
t -> Term t
conTerm forall a b. (a -> b) -> a -> b
$ -a
l) Term a
r
doPevalUMinusNumTerm (AddNumTerm Id
_ (UMinusNumTerm Id
_ Term a
l) Term a
r) = forall a. a -> Maybe a
Just forall a b. (a -> b) -> a -> b
$ forall a. (Num a, SupportedPrim a) => Term a -> Term a -> Term a
pevalAddNumTerm Term a
l (forall a. (Num a, SupportedPrim a) => Term a -> Term a
pevalUMinusNumTerm Term a
r)
doPevalUMinusNumTerm (AddNumTerm Id
_ Term a
l (UMinusNumTerm Id
_ Term a
r)) = forall a. a -> Maybe a
Just forall a b. (a -> b) -> a -> b
$ forall a. (Num a, SupportedPrim a) => Term a -> Term a -> Term a
pevalAddNumTerm (forall a. (Num a, SupportedPrim a) => Term a -> Term a
pevalUMinusNumTerm Term a
l) Term a
r
doPevalUMinusNumTerm (TimesNumTerm Id
_ (NumConTerm a
l) Term a
r) = forall a. a -> Maybe a
Just forall a b. (a -> b) -> a -> b
$ forall a. (Num a, SupportedPrim a) => Term a -> Term a -> Term a
pevalTimesNumTerm (forall t.
(SupportedPrim t, Typeable t, Hashable t, Eq t, Show t) =>
t -> Term t
conTerm forall a b. (a -> b) -> a -> b
$ -a
l) Term a
r
doPevalUMinusNumTerm (TimesNumTerm Id
_ (UMinusNumTerm Id
_ Term a
_ :: Term a) (Term a
_ :: Term a)) = forall a. HasCallStack => [Char] -> a
error [Char]
"Should not happen"
doPevalUMinusNumTerm (TimesNumTerm Id
_ (Term a
_ :: Term a) (UMinusNumTerm Id
_ (Term a
_ :: Term a))) = forall a. HasCallStack => [Char] -> a
error [Char]
"Should not happen"
doPevalUMinusNumTerm (AddNumTerm Id
_ (Term a
_ :: Term a) ConTerm {}) = forall a. HasCallStack => [Char] -> a
error [Char]
"Should not happen"
doPevalUMinusNumTerm Term a
_ = forall a. Maybe a
Nothing

-- times
pevalTimesNumTerm :: forall a. (Num a, SupportedPrim a) => Term a -> Term a -> Term a
pevalTimesNumTerm :: forall a. (Num a, SupportedPrim a) => Term a -> Term a -> Term a
pevalTimesNumTerm = forall a b c.
(Typeable a, Typeable b, SupportedPrim c) =>
PartialRuleBinary a b c
-> TotalRuleBinary a b c -> TotalRuleBinary a b c
binaryUnfoldOnce forall a.
(Num a, SupportedPrim a) =>
Term a -> Term a -> Maybe (Term a)
doPevalTimesNumTerm (\Term a
a Term a
b -> forall a. (Num a, Typeable a) => Term a -> Term a
normalizeTimesNum forall a b. (a -> b) -> a -> b
$ forall a. (SupportedPrim a, Num a) => Term a -> Term a -> Term a
timesNumTerm Term a
a Term a
b)

normalizeTimesNum :: forall a. (Num a, Typeable a) => Term a -> Term a
normalizeTimesNum :: forall a. (Num a, Typeable a) => Term a -> Term a
normalizeTimesNum (TimesNumTerm Id
_ Term a
l r :: Term a
r@(ConTerm Id
_ a
_)) = forall a. (SupportedPrim a, Num a) => Term a -> Term a -> Term a
timesNumTerm Term a
r Term a
l
normalizeTimesNum Term a
v = Term a
v

doPevalTimesNumTerm :: forall a. (Num a, SupportedPrim a) => Term a -> Term a -> Maybe (Term a)
doPevalTimesNumTerm :: forall a.
(Num a, SupportedPrim a) =>
Term a -> Term a -> Maybe (Term a)
doPevalTimesNumTerm (ConTerm Id
_ a
a) (ConTerm Id
_ a
b) = forall a. a -> Maybe a
Just forall a b. (a -> b) -> a -> b
$ forall t.
(SupportedPrim t, Typeable t, Hashable t, Eq t, Show t) =>
t -> Term t
conTerm forall a b. (a -> b) -> a -> b
$ a
a forall a. Num a => a -> a -> a
* a
b
doPevalTimesNumTerm l :: Term a
l@(ConTerm Id
_ a
a) Term a
b = case (a
a, Term a
b) of
  (a
0, Term a
_) -> forall a. a -> Maybe a
Just forall a b. (a -> b) -> a -> b
$ forall t.
(SupportedPrim t, Typeable t, Hashable t, Eq t, Show t) =>
t -> Term t
conTerm a
0
  (a
1, Term a
k) -> forall a. a -> Maybe a
Just Term a
k
  (-1, Term a
k) -> forall a. a -> Maybe a
Just forall a b. (a -> b) -> a -> b
$ forall a. (Num a, SupportedPrim a) => Term a -> Term a
pevalUMinusNumTerm Term a
k
  (a
l1, TimesNumTerm Id
_ (NumConTerm a
j) Term a
k) -> forall a. a -> Maybe a
Just forall a b. (a -> b) -> a -> b
$ forall a. (Num a, SupportedPrim a) => Term a -> Term a -> Term a
pevalTimesNumTerm (forall t.
(SupportedPrim t, Typeable t, Hashable t, Eq t, Show t) =>
t -> Term t
conTerm forall a b. (a -> b) -> a -> b
$ a
l1 forall a. Num a => a -> a -> a
* a
j) Term a
k
  (a
l1, AddNumTerm Id
_ (NumConTerm a
j) Term a
k) -> forall a. a -> Maybe a
Just forall a b. (a -> b) -> a -> b
$ forall a. (Num a, SupportedPrim a) => Term a -> Term a -> Term a
pevalAddNumTerm (forall t.
(SupportedPrim t, Typeable t, Hashable t, Eq t, Show t) =>
t -> Term t
conTerm forall a b. (a -> b) -> a -> b
$ a
l1 forall a. Num a => a -> a -> a
* a
j) (forall a. (Num a, SupportedPrim a) => Term a -> Term a -> Term a
pevalTimesNumTerm (forall t.
(SupportedPrim t, Typeable t, Hashable t, Eq t, Show t) =>
t -> Term t
conTerm a
l1) Term a
k)
  (a
l1, UMinusNumTerm Id
_ Term a
j) -> forall a. a -> Maybe a
Just (forall a. (Num a, SupportedPrim a) => Term a -> Term a -> Term a
pevalTimesNumTerm (forall t.
(SupportedPrim t, Typeable t, Hashable t, Eq t, Show t) =>
t -> Term t
conTerm forall a b. (a -> b) -> a -> b
$ -a
l1) Term a
j)
  (a
_, TimesNumTerm Id
_ (Term a
_ :: Term a) ConTerm {}) -> forall a. HasCallStack => [Char] -> a
error [Char]
"Should not happen"
  (a
_, AddNumTerm Id
_ (Term a
_ :: Term a) ConTerm {}) -> forall a. HasCallStack => [Char] -> a
error [Char]
"Should not happen"
  (a, Term a)
_ -> forall a.
(Num a, SupportedPrim a) =>
Term a -> Term a -> Maybe (Term a)
doPevalTimesNumTermNoConc Term a
l Term a
b
doPevalTimesNumTerm Term a
a r :: Term a
r@(ConTerm Id
_ a
_) = forall a.
(Num a, SupportedPrim a) =>
Term a -> Term a -> Maybe (Term a)
doPevalTimesNumTerm Term a
r Term a
a
doPevalTimesNumTerm Term a
l Term a
r = forall a.
(Num a, SupportedPrim a) =>
Term a -> Term a -> Maybe (Term a)
doPevalTimesNumTermNoConc Term a
l Term a
r

doPevalTimesNumTermNoConc :: forall a. (Num a, SupportedPrim a) => Term a -> Term a -> Maybe (Term a)
doPevalTimesNumTermNoConc :: forall a.
(Num a, SupportedPrim a) =>
Term a -> Term a -> Maybe (Term a)
doPevalTimesNumTermNoConc (TimesNumTerm Id
_ i :: Term a
i@ConTerm {} Term a
j) Term a
k = forall a. a -> Maybe a
Just forall a b. (a -> b) -> a -> b
$ forall a. (Num a, SupportedPrim a) => Term a -> Term a -> Term a
pevalTimesNumTerm Term a
i forall a b. (a -> b) -> a -> b
$ forall a. (Num a, SupportedPrim a) => Term a -> Term a -> Term a
pevalTimesNumTerm Term a
j Term a
k
doPevalTimesNumTermNoConc Term a
i (TimesNumTerm Id
_ j :: Term a
j@ConTerm {} Term a
k) = forall a. a -> Maybe a
Just forall a b. (a -> b) -> a -> b
$ forall a. (Num a, SupportedPrim a) => Term a -> Term a -> Term a
pevalTimesNumTerm Term a
j forall a b. (a -> b) -> a -> b
$ forall a. (Num a, SupportedPrim a) => Term a -> Term a -> Term a
pevalTimesNumTerm Term a
i Term a
k
doPevalTimesNumTermNoConc (UMinusNumTerm Id
_ Term a
i) Term a
j = forall a. a -> Maybe a
Just forall a b. (a -> b) -> a -> b
$ forall a. (Num a, SupportedPrim a) => Term a -> Term a
pevalUMinusNumTerm forall a b. (a -> b) -> a -> b
$ forall a. (Num a, SupportedPrim a) => Term a -> Term a -> Term a
pevalTimesNumTerm Term a
i Term a
j
doPevalTimesNumTermNoConc Term a
i (UMinusNumTerm Id
_ Term a
j) = forall a. a -> Maybe a
Just forall a b. (a -> b) -> a -> b
$ forall a. (Num a, SupportedPrim a) => Term a -> Term a
pevalUMinusNumTerm forall a b. (a -> b) -> a -> b
$ forall a. (Num a, SupportedPrim a) => Term a -> Term a -> Term a
pevalTimesNumTerm Term a
i Term a
j
doPevalTimesNumTermNoConc Term a
i j :: Term a
j@ConTerm {} = forall a. a -> Maybe a
Just forall a b. (a -> b) -> a -> b
$ forall a. (Num a, SupportedPrim a) => Term a -> Term a -> Term a
pevalTimesNumTerm Term a
j Term a
i
doPevalTimesNumTermNoConc (TimesNumTerm Id
_ (Term a
_ :: Term a) ConTerm {}) Term a
_ = forall a. HasCallStack => [Char] -> a
error [Char]
"Should not happen"
doPevalTimesNumTermNoConc Term a
_ (TimesNumTerm Id
_ (Term a
_ :: Term a) ConTerm {}) = forall a. HasCallStack => [Char] -> a
error [Char]
"Should not happen"
doPevalTimesNumTermNoConc Term a
_ Term a
_ = forall a. Maybe a
Nothing

-- abs
pevalAbsNumTerm :: (SupportedPrim a, Num a) => Term a -> Term a
pevalAbsNumTerm :: forall a. (SupportedPrim a, Num a) => Term a -> Term a
pevalAbsNumTerm = forall a b.
(Typeable a, SupportedPrim b) =>
PartialRuleUnary a b -> TotalRuleUnary a b -> TotalRuleUnary a b
unaryUnfoldOnce forall a. (Num a, SupportedPrim a) => Term a -> Maybe (Term a)
doPevalAbsNumTerm forall a. (SupportedPrim a, Num a) => Term a -> Term a
absNumTerm

doPevalAbsNumTerm :: forall a. (Num a, SupportedPrim a) => Term a -> Maybe (Term a)
doPevalAbsNumTerm :: forall a. (Num a, SupportedPrim a) => Term a -> Maybe (Term a)
doPevalAbsNumTerm (ConTerm Id
_ a
a) = forall a. a -> Maybe a
Just forall a b. (a -> b) -> a -> b
$ forall t.
(SupportedPrim t, Typeable t, Hashable t, Eq t, Show t) =>
t -> Term t
conTerm forall a b. (a -> b) -> a -> b
$ forall a. Num a => a -> a
abs a
a
doPevalAbsNumTerm (UMinusNumTerm Id
_ Term a
v) = forall a. a -> Maybe a
Just forall a b. (a -> b) -> a -> b
$ forall a. (SupportedPrim a, Num a) => Term a -> Term a
pevalAbsNumTerm Term a
v
doPevalAbsNumTerm t :: Term a
t@(AbsNumTerm Id
_ (Term a
_ :: Term a)) = forall a. a -> Maybe a
Just Term a
t
doPevalAbsNumTerm (TimesNumTerm Id
_ (Dyn (Term Integer
l :: Term Integer)) Term a
r) =
  forall a. a -> Maybe a
Just forall a b. (a -> b) -> a -> b
$ forall a. (Num a, SupportedPrim a) => Term a -> Term a -> Term a
pevalTimesNumTerm (forall a. (SupportedPrim a, Num a) => Term a -> Term a
pevalAbsNumTerm forall a b. (a -> b) -> a -> b
$ forall a b. a -> b
unsafeCoerce Term Integer
l :: Term a) forall a b. (a -> b) -> a -> b
$ forall a. (SupportedPrim a, Num a) => Term a -> Term a
pevalAbsNumTerm (forall a b. a -> b
unsafeCoerce Term a
r)
doPevalAbsNumTerm Term a
_ = forall a. Maybe a
Nothing

-- signum
pevalSignumNumTerm :: (Num a, SupportedPrim a) => Term a -> Term a
pevalSignumNumTerm :: forall a. (Num a, SupportedPrim a) => Term a -> Term a
pevalSignumNumTerm = forall a b.
(Typeable a, SupportedPrim b) =>
PartialRuleUnary a b -> TotalRuleUnary a b -> TotalRuleUnary a b
unaryUnfoldOnce forall a. (Num a, SupportedPrim a) => Term a -> Maybe (Term a)
doPevalSignumNumTerm forall a. (SupportedPrim a, Num a) => Term a -> Term a
signumNumTerm

doPevalSignumNumTerm :: forall a. (Num a, SupportedPrim a) => Term a -> Maybe (Term a)
doPevalSignumNumTerm :: forall a. (Num a, SupportedPrim a) => Term a -> Maybe (Term a)
doPevalSignumNumTerm (ConTerm Id
_ a
a) = forall a. a -> Maybe a
Just forall a b. (a -> b) -> a -> b
$ forall t.
(SupportedPrim t, Typeable t, Hashable t, Eq t, Show t) =>
t -> Term t
conTerm forall a b. (a -> b) -> a -> b
$ forall a. Num a => a -> a
signum a
a
doPevalSignumNumTerm (UMinusNumTerm Id
_ (Dyn (Term Integer
v :: Term Integer))) = forall a. a -> Maybe a
Just forall a b. (a -> b) -> a -> b
$ forall a. (Num a, SupportedPrim a) => Term a -> Term a
pevalUMinusNumTerm forall a b. (a -> b) -> a -> b
$ forall a. (Num a, SupportedPrim a) => Term a -> Term a
pevalSignumNumTerm forall a b. (a -> b) -> a -> b
$ forall a b. a -> b
unsafeCoerce Term Integer
v
doPevalSignumNumTerm (TimesNumTerm Id
_ (Dyn (Term Integer
l :: Term Integer)) Term a
r) =
  forall a. a -> Maybe a
Just forall a b. (a -> b) -> a -> b
$ forall a. (Num a, SupportedPrim a) => Term a -> Term a -> Term a
pevalTimesNumTerm (forall a. (Num a, SupportedPrim a) => Term a -> Term a
pevalSignumNumTerm forall a b. (a -> b) -> a -> b
$ forall a b. a -> b
unsafeCoerce Term Integer
l :: Term a) forall a b. (a -> b) -> a -> b
$ forall a. (Num a, SupportedPrim a) => Term a -> Term a
pevalSignumNumTerm (forall a b. a -> b
unsafeCoerce Term a
r)
doPevalSignumNumTerm Term a
_ = forall a. Maybe a
Nothing

-- lt
pevalLtNumTerm :: (Num a, Ord a, SupportedPrim a) => Term a -> Term a -> Term Bool
pevalLtNumTerm :: forall a.
(Num a, Ord a, SupportedPrim a) =>
Term a -> Term a -> Term Bool
pevalLtNumTerm = forall a b c.
(Typeable a, Typeable b, SupportedPrim c) =>
PartialRuleBinary a b c
-> TotalRuleBinary a b c -> TotalRuleBinary a b c
binaryUnfoldOnce forall a.
(Num a, Ord a, SupportedPrim a) =>
Term a -> Term a -> Maybe (Term Bool)
doPevalLtNumTerm forall a.
(SupportedPrim a, Num a, Ord a) =>
Term a -> Term a -> Term Bool
ltNumTerm

doPevalLtNumTerm :: forall a. (Num a, Ord a, SupportedPrim a) => Term a -> Term a -> Maybe (Term Bool)
doPevalLtNumTerm :: forall a.
(Num a, Ord a, SupportedPrim a) =>
Term a -> Term a -> Maybe (Term Bool)
doPevalLtNumTerm (ConTerm Id
_ a
a) (ConTerm Id
_ a
b) = forall a. a -> Maybe a
Just forall a b. (a -> b) -> a -> b
$ forall t.
(SupportedPrim t, Typeable t, Hashable t, Eq t, Show t) =>
t -> Term t
conTerm forall a b. (a -> b) -> a -> b
$ a
a forall a. Ord a => a -> a -> Bool
< a
b
doPevalLtNumTerm (ConTerm Id
_ a
l) (AddNumTerm Id
_ (ConTerm Id
_ (Dyn (Integer
j :: Integer))) Term a
k) =
  forall a. a -> Maybe a
Just forall a b. (a -> b) -> a -> b
$ forall a.
(Num a, Ord a, SupportedPrim a) =>
Term a -> Term a -> Term Bool
pevalLtNumTerm (forall t.
(SupportedPrim t, Typeable t, Hashable t, Eq t, Show t) =>
t -> Term t
conTerm forall a b. (a -> b) -> a -> b
$ forall a b. a -> b
unsafeCoerce a
l forall a. Num a => a -> a -> a
- Integer
j) (forall a b. a -> b
unsafeCoerce Term a
k)
doPevalLtNumTerm (AddNumTerm Id
_ (ConTerm Id
_ (Dyn (Integer
i :: Integer))) Term a
j) (ConTerm Id
_ a
k) =
  forall a. a -> Maybe a
Just forall a b. (a -> b) -> a -> b
$ forall a.
(Num a, Ord a, SupportedPrim a) =>
Term a -> Term a -> Term Bool
pevalLtNumTerm (forall a b. a -> b
unsafeCoerce Term a
j) (forall t.
(SupportedPrim t, Typeable t, Hashable t, Eq t, Show t) =>
t -> Term t
conTerm forall a b. (a -> b) -> a -> b
$ forall a b. a -> b
unsafeCoerce a
k forall a. Num a => a -> a -> a
- Integer
i)
doPevalLtNumTerm (AddNumTerm Id
_ (ConTerm Id
_ (Dyn (Integer
j :: Integer))) Term a
k) Term a
l =
  forall a. a -> Maybe a
Just forall a b. (a -> b) -> a -> b
$ forall a.
(Num a, Ord a, SupportedPrim a) =>
Term a -> Term a -> Term Bool
pevalLtNumTerm (forall t.
(SupportedPrim t, Typeable t, Hashable t, Eq t, Show t) =>
t -> Term t
conTerm Integer
j) (forall a. (Num a, SupportedPrim a) => Term a -> Term a -> Term a
pevalMinusNumTerm (forall a b. a -> b
unsafeCoerce Term a
l) (forall a b. a -> b
unsafeCoerce Term a
k))
doPevalLtNumTerm Term a
j (AddNumTerm Id
_ (ConTerm Id
_ (Dyn (Integer
k :: Integer))) Term a
l) =
  forall a. a -> Maybe a
Just forall a b. (a -> b) -> a -> b
$ forall a.
(Num a, Ord a, SupportedPrim a) =>
Term a -> Term a -> Term Bool
pevalLtNumTerm (forall t.
(SupportedPrim t, Typeable t, Hashable t, Eq t, Show t) =>
t -> Term t
conTerm forall a b. (a -> b) -> a -> b
$ -Integer
k) (forall a. (Num a, SupportedPrim a) => Term a -> Term a -> Term a
pevalMinusNumTerm (forall a b. a -> b
unsafeCoerce Term a
l) (forall a b. a -> b
unsafeCoerce Term a
j))
doPevalLtNumTerm Term a
l (ConTerm Id
_ a
r) =
  case forall {k} (a :: k) (b :: k).
(Typeable a, Typeable b) =>
Maybe (a :~: b)
eqT @a @Integer of
    Just a :~: Integer
Refl ->
      forall a. a -> Maybe a
Just forall a b. (a -> b) -> a -> b
$ forall a.
(Num a, Ord a, SupportedPrim a) =>
Term a -> Term a -> Term Bool
pevalLtNumTerm (forall t.
(SupportedPrim t, Typeable t, Hashable t, Eq t, Show t) =>
t -> Term t
conTerm forall a b. (a -> b) -> a -> b
$ -a
r) (forall a. (Num a, SupportedPrim a) => Term a -> Term a
pevalUMinusNumTerm Term a
l)
    Maybe (a :~: Integer)
_ -> forall a. Maybe a
Nothing
doPevalLtNumTerm Term a
_ Term a
_ = forall a. Maybe a
Nothing

-- le
pevalLeNumTerm :: (Num a, Ord a, SupportedPrim a) => Term a -> Term a -> Term Bool
pevalLeNumTerm :: forall a.
(Num a, Ord a, SupportedPrim a) =>
Term a -> Term a -> Term Bool
pevalLeNumTerm = forall a b c.
(Typeable a, Typeable b, SupportedPrim c) =>
PartialRuleBinary a b c
-> TotalRuleBinary a b c -> TotalRuleBinary a b c
binaryUnfoldOnce forall a.
(Num a, Ord a, SupportedPrim a) =>
Term a -> Term a -> Maybe (Term Bool)
doPevalLeNumTerm forall a.
(SupportedPrim a, Num a, Ord a) =>
Term a -> Term a -> Term Bool
leNumTerm

doPevalLeNumTerm :: forall a. (Num a, Ord a, SupportedPrim a) => Term a -> Term a -> Maybe (Term Bool)
doPevalLeNumTerm :: forall a.
(Num a, Ord a, SupportedPrim a) =>
Term a -> Term a -> Maybe (Term Bool)
doPevalLeNumTerm (ConTerm Id
_ a
a) (ConTerm Id
_ a
b) = forall a. a -> Maybe a
Just forall a b. (a -> b) -> a -> b
$ forall t.
(SupportedPrim t, Typeable t, Hashable t, Eq t, Show t) =>
t -> Term t
conTerm forall a b. (a -> b) -> a -> b
$ a
a forall a. Ord a => a -> a -> Bool
<= a
b
doPevalLeNumTerm (ConTerm Id
_ a
l) (AddNumTerm Id
_ (ConTerm Id
_ (Dyn (Integer
j :: Integer))) Term a
k) =
  forall a. a -> Maybe a
Just forall a b. (a -> b) -> a -> b
$ forall a.
(Num a, Ord a, SupportedPrim a) =>
Term a -> Term a -> Term Bool
pevalLeNumTerm (forall t.
(SupportedPrim t, Typeable t, Hashable t, Eq t, Show t) =>
t -> Term t
conTerm forall a b. (a -> b) -> a -> b
$ forall a b. a -> b
unsafeCoerce a
l forall a. Num a => a -> a -> a
- Integer
j) (forall a b. a -> b
unsafeCoerce Term a
k)
doPevalLeNumTerm (AddNumTerm Id
_ (ConTerm Id
_ (Dyn (Integer
i :: Integer))) Term a
j) (ConTerm Id
_ a
k) =
  forall a. a -> Maybe a
Just forall a b. (a -> b) -> a -> b
$ forall a.
(Num a, Ord a, SupportedPrim a) =>
Term a -> Term a -> Term Bool
pevalLeNumTerm (forall a b. a -> b
unsafeCoerce Term a
j) (forall t.
(SupportedPrim t, Typeable t, Hashable t, Eq t, Show t) =>
t -> Term t
conTerm forall a b. (a -> b) -> a -> b
$ forall a b. a -> b
unsafeCoerce a
k forall a. Num a => a -> a -> a
- Integer
i)
doPevalLeNumTerm (AddNumTerm Id
_ (ConTerm Id
_ (Dyn (Integer
j :: Integer))) Term a
k) Term a
l =
  forall a. a -> Maybe a
Just forall a b. (a -> b) -> a -> b
$ forall a.
(Num a, Ord a, SupportedPrim a) =>
Term a -> Term a -> Term Bool
pevalLeNumTerm (forall t.
(SupportedPrim t, Typeable t, Hashable t, Eq t, Show t) =>
t -> Term t
conTerm Integer
j) (forall a. (Num a, SupportedPrim a) => Term a -> Term a -> Term a
pevalMinusNumTerm (forall a b. a -> b
unsafeCoerce Term a
l) (forall a b. a -> b
unsafeCoerce Term a
k))
doPevalLeNumTerm Term a
j (AddNumTerm Id
_ (ConTerm Id
_ (Dyn (Integer
k :: Integer))) Term a
l) =
  forall a. a -> Maybe a
Just forall a b. (a -> b) -> a -> b
$ forall a.
(Num a, Ord a, SupportedPrim a) =>
Term a -> Term a -> Term Bool
pevalLeNumTerm (forall t.
(SupportedPrim t, Typeable t, Hashable t, Eq t, Show t) =>
t -> Term t
conTerm forall a b. (a -> b) -> a -> b
$ -Integer
k) (forall a. (Num a, SupportedPrim a) => Term a -> Term a -> Term a
pevalMinusNumTerm (forall a b. a -> b
unsafeCoerce Term a
l) (forall a b. a -> b
unsafeCoerce Term a
j))
doPevalLeNumTerm Term a
l (ConTerm Id
_ a
r) =
  case forall {k} (a :: k) (b :: k).
(Typeable a, Typeable b) =>
Maybe (a :~: b)
eqT @a @Integer of
    Just a :~: Integer
Refl ->
      forall a. a -> Maybe a
Just forall a b. (a -> b) -> a -> b
$ forall a.
(Num a, Ord a, SupportedPrim a) =>
Term a -> Term a -> Term Bool
pevalLeNumTerm (forall t.
(SupportedPrim t, Typeable t, Hashable t, Eq t, Show t) =>
t -> Term t
conTerm forall a b. (a -> b) -> a -> b
$ -a
r) (forall a. (Num a, SupportedPrim a) => Term a -> Term a
pevalUMinusNumTerm Term a
l)
    Maybe (a :~: Integer)
_ -> forall a. Maybe a
Nothing
doPevalLeNumTerm Term a
_ Term a
_ = forall a. Maybe a
Nothing

pevalGtNumTerm :: (Num a, Ord a, SupportedPrim a) => Term a -> Term a -> Term Bool
pevalGtNumTerm :: forall a.
(Num a, Ord a, SupportedPrim a) =>
Term a -> Term a -> Term Bool
pevalGtNumTerm = forall a b c. (a -> b -> c) -> b -> a -> c
flip forall a.
(Num a, Ord a, SupportedPrim a) =>
Term a -> Term a -> Term Bool
pevalLtNumTerm

pevalGeNumTerm :: (Num a, Ord a, SupportedPrim a) => Term a -> Term a -> Term Bool
pevalGeNumTerm :: forall a.
(Num a, Ord a, SupportedPrim a) =>
Term a -> Term a -> Term Bool
pevalGeNumTerm = forall a b c. (a -> b -> c) -> b -> a -> c
flip forall a.
(Num a, Ord a, SupportedPrim a) =>
Term a -> Term a -> Term Bool
pevalLeNumTerm