{-# 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) = a -> Maybe b
forall a b. (Typeable a, Typeable b) => a -> Maybe b
cast a
b
numConTermView Term a
_ = Maybe b
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) -> (Void# -> 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) = a -> Maybe b
forall a b. (Typeable a, Typeable b) => a -> Maybe b
cast a
b
numOrdConTermView Term a
_ = Maybe b
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) -> (Void# -> 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 = PartialRuleBinary a a a
-> TotalRuleBinary a a a -> TotalRuleBinary a a a
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 a
forall a.
(Num a, SupportedPrim a) =>
Term a -> Term a -> Maybe (Term a)
doPevalAddNumTerm (\Term a
a Term a
b -> Term a -> Term a
forall a. (Num a, Typeable a) => Term a -> Term a
normalizeAddNum (Term a -> Term a) -> Term a -> Term a
forall a b. (a -> b) -> a -> b
$ TotalRuleBinary a a a
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) = Term a -> Maybe (Term a)
forall a. a -> Maybe a
Just (Term a -> Maybe (Term a)) -> Term a -> Maybe (Term a)
forall a b. (a -> b) -> a -> b
$ 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
a a -> 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) -> Term a -> Maybe (Term a)
forall a. a -> Maybe a
Just Term a
k
  (a
l1, AddNumTerm Id
_ (ConTerm Id
_ a
j) Term a
k) -> Term a -> Maybe (Term a)
forall a. a -> Maybe a
Just (Term a -> Maybe (Term a)) -> Term a -> Maybe (Term a)
forall a b. (a -> b) -> a -> b
$ Term a -> Term a -> Term a
forall a. (Num a, SupportedPrim a) => Term a -> Term a -> Term a
pevalAddNumTerm (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
l1 a -> a -> a
forall a. Num a => a -> a -> a
+ a
j) Term a
k
  (a, Term a)
_ -> Term a -> Term a -> Maybe (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
_) = Term a -> Term a -> Maybe (Term 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 = Term a -> Term a -> Maybe (Term a)
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 = Term a -> Maybe (Term a)
forall a. a -> Maybe a
Just (Term a -> Maybe (Term a)) -> Term a -> Maybe (Term a)
forall a b. (a -> b) -> a -> b
$ Term a -> Term a -> Term a
forall a. (Num a, SupportedPrim a) => Term a -> Term a -> Term a
pevalAddNumTerm Term a
i (Term a -> Term a) -> Term a -> Term a
forall a b. (a -> b) -> a -> b
$ Term a -> Term a -> Term a
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) = Term a -> Maybe (Term a)
forall a. a -> Maybe a
Just (Term a -> Maybe (Term a)) -> Term a -> Maybe (Term a)
forall a b. (a -> b) -> a -> b
$ Term a -> Term a -> Term a
forall a. (Num a, SupportedPrim a) => Term a -> Term a -> Term a
pevalAddNumTerm Term a
j (Term a -> Term a) -> Term a -> Term a
forall a b. (a -> b) -> a -> b
$ Term a -> Term a -> Term a
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) = Term a -> Maybe (Term a)
forall a. a -> Maybe a
Just (Term a -> Maybe (Term a)) -> Term a -> Maybe (Term a)
forall a b. (a -> b) -> a -> b
$ Term a -> Term a
forall a. (Num a, SupportedPrim a) => Term a -> Term a
pevalUMinusNumTerm (Term a -> Term a) -> Term a -> Term a
forall a b. (a -> b) -> a -> b
$ Term a -> Term a -> Term a
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 Term a -> Term a -> Bool
forall a. Eq a => a -> a -> Bool
== Term a
l = Term a -> Maybe (Term a)
forall a. a -> Maybe a
Just (Term a -> Maybe (Term a)) -> Term a -> Maybe (Term a)
forall a b. (a -> b) -> a -> b
$ Term a -> Term a -> Term a
forall a. (Num a, SupportedPrim a) => Term a -> Term a -> Term a
pevalTimesNumTerm (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
i a -> a -> a
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 Term a -> Term a -> Bool
forall a. Eq a => a -> a -> Bool
== Term a
k = Term a -> Maybe (Term a)
forall a. a -> Maybe a
Just (Term a -> Maybe (Term a)) -> Term a -> Maybe (Term a)
forall a b. (a -> b) -> a -> b
$ Term a -> Term a -> Term a
forall a. (Num a, SupportedPrim a) => Term a -> Term a -> Term a
pevalTimesNumTerm Term a
i (Term a -> Term a -> Term a
forall a. (Num a, SupportedPrim a) => Term a -> Term a -> Term a
pevalAddNumTerm Term a
j Term a
l)
doPevalAddNumTermNoConc Term a
_ Term a
_ = Maybe (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
_)) = Term a -> Term a -> Term 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 = Term a -> Term a -> Term a
forall a. (Num a, SupportedPrim a) => Term a -> Term a -> Term a
pevalAddNumTerm Term a
l (Term a -> Term a
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 = PartialRuleUnary a a -> TotalRuleUnary a a -> TotalRuleUnary a a
forall a b.
(Typeable a, SupportedPrim b) =>
PartialRuleUnary a b -> TotalRuleUnary a b -> TotalRuleUnary a b
unaryUnfoldOnce PartialRuleUnary a a
forall a. (Num a, SupportedPrim a) => Term a -> Maybe (Term a)
doPevalUMinusNumTerm TotalRuleUnary a a
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) = Term a -> Maybe (Term a)
forall a. a -> Maybe a
Just (Term a -> Maybe (Term a)) -> Term a -> Maybe (Term a)
forall a b. (a -> b) -> a -> b
$ 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
a
doPevalUMinusNumTerm (UMinusNumTerm Id
_ Term a
v) = Term a -> Maybe (Term a)
forall a. a -> Maybe a
Just Term a
v
doPevalUMinusNumTerm (AddNumTerm Id
_ (NumConTerm a
l) Term a
r) = Term a -> Maybe (Term a)
forall a. a -> Maybe a
Just (Term a -> Maybe (Term a)) -> Term a -> Maybe (Term a)
forall a b. (a -> b) -> a -> b
$ Term a -> Term a -> Term a
forall a. (Num a, SupportedPrim a) => Term a -> Term a -> Term a
pevalMinusNumTerm (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) Term a
r
doPevalUMinusNumTerm (AddNumTerm Id
_ (UMinusNumTerm Id
_ Term a
l) Term a
r) = Term a -> Maybe (Term a)
forall a. a -> Maybe a
Just (Term a -> Maybe (Term a)) -> Term a -> Maybe (Term a)
forall a b. (a -> b) -> a -> b
$ Term a -> Term a -> Term a
forall a. (Num a, SupportedPrim a) => Term a -> Term a -> Term a
pevalAddNumTerm Term a
l (Term a -> Term a
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)) = Term a -> Maybe (Term a)
forall a. a -> Maybe a
Just (Term a -> Maybe (Term a)) -> Term a -> Maybe (Term a)
forall a b. (a -> b) -> a -> b
$ Term a -> Term a -> Term a
forall a. (Num a, SupportedPrim a) => Term a -> Term a -> Term a
pevalAddNumTerm (Term a -> Term a
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) = Term a -> Maybe (Term a)
forall a. a -> Maybe a
Just (Term a -> Maybe (Term a)) -> Term a -> Maybe (Term a)
forall a b. (a -> b) -> a -> b
$ Term a -> Term a -> Term a
forall a. (Num a, SupportedPrim a) => Term a -> Term a -> Term a
pevalTimesNumTerm (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) Term a
r
doPevalUMinusNumTerm (TimesNumTerm Id
_ (UMinusNumTerm Id
_ Term a
_ :: Term a) (Term a
_ :: Term a)) = [Char] -> Maybe (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))) = [Char] -> Maybe (Term a)
forall a. HasCallStack => [Char] -> a
error [Char]
"Should not happen"
doPevalUMinusNumTerm (AddNumTerm Id
_ (Term a
_ :: Term a) ConTerm {}) = [Char] -> Maybe (Term a)
forall a. HasCallStack => [Char] -> a
error [Char]
"Should not happen"
doPevalUMinusNumTerm Term a
_ = Maybe (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 = PartialRuleBinary a a a
-> TotalRuleBinary a a a -> TotalRuleBinary a a a
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 a
forall a.
(Num a, SupportedPrim a) =>
Term a -> Term a -> Maybe (Term a)
doPevalTimesNumTerm (\Term a
a Term a
b -> Term a -> Term a
forall a. (Num a, Typeable a) => Term a -> Term a
normalizeTimesNum (Term a -> Term a) -> Term a -> Term a
forall a b. (a -> b) -> a -> b
$ TotalRuleBinary a a a
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
_)) = Term a -> Term a -> Term 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) = Term a -> Maybe (Term a)
forall a. a -> Maybe a
Just (Term a -> Maybe (Term a)) -> Term a -> Maybe (Term a)
forall a b. (a -> b) -> a -> b
$ 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
a a -> 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
_) -> Term a -> Maybe (Term a)
forall a. a -> Maybe a
Just (Term a -> Maybe (Term a)) -> Term a -> Maybe (Term a)
forall a b. (a -> b) -> a -> b
$ a -> Term a
forall t.
(SupportedPrim t, Typeable t, Hashable t, Eq t, Show t) =>
t -> Term t
conTerm a
0
  (a
1, Term a
k) -> Term a -> Maybe (Term a)
forall a. a -> Maybe a
Just Term a
k
  (-1, Term a
k) -> Term a -> Maybe (Term a)
forall a. a -> Maybe a
Just (Term a -> Maybe (Term a)) -> Term a -> Maybe (Term a)
forall a b. (a -> b) -> a -> b
$ Term a -> Term a
forall a. (Num a, SupportedPrim a) => Term a -> Term a
pevalUMinusNumTerm Term a
k
  (a
l1, TimesNumTerm Id
_ (NumConTerm a
j) Term a
k) -> Term a -> Maybe (Term a)
forall a. a -> Maybe a
Just (Term a -> Maybe (Term a)) -> Term a -> Maybe (Term a)
forall a b. (a -> b) -> a -> b
$ Term a -> Term a -> Term a
forall a. (Num a, SupportedPrim a) => Term a -> Term a -> Term a
pevalTimesNumTerm (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
l1 a -> a -> a
forall a. Num a => a -> a -> a
* a
j) Term a
k
  (a
l1, AddNumTerm Id
_ (NumConTerm a
j) Term a
k) -> Term a -> Maybe (Term a)
forall a. a -> Maybe a
Just (Term a -> Maybe (Term a)) -> Term a -> Maybe (Term a)
forall a b. (a -> b) -> a -> b
$ Term a -> Term a -> Term a
forall a. (Num a, SupportedPrim a) => Term a -> Term a -> Term a
pevalAddNumTerm (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
l1 a -> a -> a
forall a. Num a => a -> a -> a
* a
j) (Term a -> Term a -> Term a
forall a. (Num a, SupportedPrim a) => Term a -> Term a -> Term a
pevalTimesNumTerm (a -> Term a
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) -> Term a -> Maybe (Term a)
forall a. a -> Maybe a
Just (Term a -> Term a -> Term a
forall a. (Num a, SupportedPrim a) => Term a -> Term a -> Term a
pevalTimesNumTerm (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
l1) Term a
j)
  (a
_, TimesNumTerm Id
_ (Term a
_ :: Term a) ConTerm {}) -> [Char] -> Maybe (Term a)
forall a. HasCallStack => [Char] -> a
error [Char]
"Should not happen"
  (a
_, AddNumTerm Id
_ (Term a
_ :: Term a) ConTerm {}) -> [Char] -> Maybe (Term a)
forall a. HasCallStack => [Char] -> a
error [Char]
"Should not happen"
  (a, Term a)
_ -> Term a -> Term a -> Maybe (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
_) = Term a -> Term a -> Maybe (Term 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 = Term a -> Term a -> Maybe (Term a)
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 = Term a -> Maybe (Term a)
forall a. a -> Maybe a
Just (Term a -> Maybe (Term a)) -> Term a -> Maybe (Term a)
forall a b. (a -> b) -> a -> b
$ Term a -> Term a -> Term a
forall a. (Num a, SupportedPrim a) => Term a -> Term a -> Term a
pevalTimesNumTerm Term a
i (Term a -> Term a) -> Term a -> Term a
forall a b. (a -> b) -> a -> b
$ Term a -> Term a -> Term a
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) = Term a -> Maybe (Term a)
forall a. a -> Maybe a
Just (Term a -> Maybe (Term a)) -> Term a -> Maybe (Term a)
forall a b. (a -> b) -> a -> b
$ Term a -> Term a -> Term a
forall a. (Num a, SupportedPrim a) => Term a -> Term a -> Term a
pevalTimesNumTerm Term a
j (Term a -> Term a) -> Term a -> Term a
forall a b. (a -> b) -> a -> b
$ Term a -> Term a -> Term a
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 = Term a -> Maybe (Term a)
forall a. a -> Maybe a
Just (Term a -> Maybe (Term a)) -> Term a -> Maybe (Term a)
forall a b. (a -> b) -> a -> b
$ Term a -> Term a
forall a. (Num a, SupportedPrim a) => Term a -> Term a
pevalUMinusNumTerm (Term a -> Term a) -> Term a -> Term a
forall a b. (a -> b) -> a -> b
$ Term a -> Term a -> Term a
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) = Term a -> Maybe (Term a)
forall a. a -> Maybe a
Just (Term a -> Maybe (Term a)) -> Term a -> Maybe (Term a)
forall a b. (a -> b) -> a -> b
$ Term a -> Term a
forall a. (Num a, SupportedPrim a) => Term a -> Term a
pevalUMinusNumTerm (Term a -> Term a) -> Term a -> Term a
forall a b. (a -> b) -> a -> b
$ Term a -> Term a -> Term a
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 {} = Term a -> Maybe (Term a)
forall a. a -> Maybe a
Just (Term a -> Maybe (Term a)) -> Term a -> Maybe (Term a)
forall a b. (a -> b) -> a -> b
$ Term a -> Term a -> Term a
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
_ = [Char] -> Maybe (Term a)
forall a. HasCallStack => [Char] -> a
error [Char]
"Should not happen"
doPevalTimesNumTermNoConc Term a
_ (TimesNumTerm Id
_ (Term a
_ :: Term a) ConTerm {}) = [Char] -> Maybe (Term a)
forall a. HasCallStack => [Char] -> a
error [Char]
"Should not happen"
doPevalTimesNumTermNoConc Term a
_ Term a
_ = Maybe (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 = PartialRuleUnary a a -> TotalRuleUnary a a -> TotalRuleUnary a a
forall a b.
(Typeable a, SupportedPrim b) =>
PartialRuleUnary a b -> TotalRuleUnary a b -> TotalRuleUnary a b
unaryUnfoldOnce PartialRuleUnary a a
forall a. (Num a, SupportedPrim a) => Term a -> Maybe (Term a)
doPevalAbsNumTerm TotalRuleUnary a a
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) = Term a -> Maybe (Term a)
forall a. a -> Maybe a
Just (Term a -> Maybe (Term a)) -> Term a -> Maybe (Term a)
forall a b. (a -> b) -> a -> b
$ 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 -> a
forall a. Num a => a -> a
abs a
a
doPevalAbsNumTerm (UMinusNumTerm Id
_ Term a
v) = Term a -> Maybe (Term a)
forall a. a -> Maybe a
Just (Term a -> Maybe (Term a)) -> Term a -> Maybe (Term a)
forall a b. (a -> b) -> a -> b
$ Term a -> Term a
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)) = Term a -> Maybe (Term a)
forall a. a -> Maybe a
Just Term a
t
doPevalAbsNumTerm (TimesNumTerm Id
_ (Dyn (Term Integer
l :: Term Integer)) Term a
r) =
  Term a -> Maybe (Term a)
forall a. a -> Maybe a
Just (Term a -> Maybe (Term a)) -> Term a -> Maybe (Term a)
forall a b. (a -> b) -> a -> b
$ Term a -> Term a -> Term a
forall a. (Num a, SupportedPrim a) => Term a -> Term a -> Term a
pevalTimesNumTerm (Term a -> Term a
forall a. (SupportedPrim a, Num a) => Term a -> Term a
pevalAbsNumTerm (Term a -> Term a) -> Term a -> Term a
forall a b. (a -> b) -> a -> b
$ Term Integer -> Term a
forall a b. a -> b
unsafeCoerce Term Integer
l :: Term a) (Term a -> Term a) -> Term a -> Term a
forall a b. (a -> b) -> a -> b
$ Term a -> Term a
forall a. (SupportedPrim a, Num a) => Term a -> Term a
pevalAbsNumTerm (Term a -> Term a
forall a b. a -> b
unsafeCoerce Term a
r)
doPevalAbsNumTerm Term a
_ = Maybe (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 = PartialRuleUnary a a -> TotalRuleUnary a a -> TotalRuleUnary a a
forall a b.
(Typeable a, SupportedPrim b) =>
PartialRuleUnary a b -> TotalRuleUnary a b -> TotalRuleUnary a b
unaryUnfoldOnce PartialRuleUnary a a
forall a. (Num a, SupportedPrim a) => Term a -> Maybe (Term a)
doPevalSignumNumTerm TotalRuleUnary a a
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) = Term a -> Maybe (Term a)
forall a. a -> Maybe a
Just (Term a -> Maybe (Term a)) -> Term a -> Maybe (Term a)
forall a b. (a -> b) -> a -> b
$ 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 -> a
forall a. Num a => a -> a
signum a
a
doPevalSignumNumTerm (UMinusNumTerm Id
_ (Dyn (Term Integer
v :: Term Integer))) = Term a -> Maybe (Term a)
forall a. a -> Maybe a
Just (Term a -> Maybe (Term a)) -> Term a -> Maybe (Term a)
forall a b. (a -> b) -> a -> b
$ Term a -> Term a
forall a. (Num a, SupportedPrim a) => Term a -> Term a
pevalUMinusNumTerm (Term a -> Term a) -> Term a -> Term a
forall a b. (a -> b) -> a -> b
$ Term a -> Term a
forall a. (Num a, SupportedPrim a) => Term a -> Term a
pevalSignumNumTerm (Term a -> Term a) -> Term a -> Term a
forall a b. (a -> b) -> a -> b
$ Term Integer -> Term a
forall a b. a -> b
unsafeCoerce Term Integer
v
doPevalSignumNumTerm (TimesNumTerm Id
_ (Dyn (Term Integer
l :: Term Integer)) Term a
r) =
  Term a -> Maybe (Term a)
forall a. a -> Maybe a
Just (Term a -> Maybe (Term a)) -> Term a -> Maybe (Term a)
forall a b. (a -> b) -> a -> b
$ Term a -> Term a -> Term a
forall a. (Num a, SupportedPrim a) => Term a -> Term a -> Term a
pevalTimesNumTerm (Term a -> Term a
forall a. (Num a, SupportedPrim a) => Term a -> Term a
pevalSignumNumTerm (Term a -> Term a) -> Term a -> Term a
forall a b. (a -> b) -> a -> b
$ Term Integer -> Term a
forall a b. a -> b
unsafeCoerce Term Integer
l :: Term a) (Term a -> Term a) -> Term a -> Term a
forall a b. (a -> b) -> a -> b
$ Term a -> Term a
forall a. (Num a, SupportedPrim a) => Term a -> Term a
pevalSignumNumTerm (Term a -> Term a
forall a b. a -> b
unsafeCoerce Term a
r)
doPevalSignumNumTerm Term a
_ = Maybe (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 = 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.
(Num a, Ord a, SupportedPrim a) =>
Term a -> Term a -> Maybe (Term Bool)
doPevalLtNumTerm TotalRuleBinary a a Bool
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) = 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
doPevalLtNumTerm (ConTerm Id
_ a
l) (AddNumTerm Id
_ (ConTerm Id
_ (Dyn (Integer
j :: Integer))) 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 Integer -> Term Integer -> Term Bool
forall a.
(Num a, Ord a, SupportedPrim a) =>
Term a -> Term a -> Term Bool
pevalLtNumTerm (Integer -> Term Integer
forall t.
(SupportedPrim t, Typeable t, Hashable t, Eq t, Show t) =>
t -> Term t
conTerm (Integer -> Term Integer) -> Integer -> Term Integer
forall a b. (a -> b) -> a -> b
$ a -> Integer
forall a b. a -> b
unsafeCoerce a
l Integer -> Integer -> Integer
forall a. Num a => a -> a -> a
- Integer
j) (Term a -> Term Integer
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) =
  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 Integer -> Term Integer -> Term Bool
forall a.
(Num a, Ord a, SupportedPrim a) =>
Term a -> Term a -> Term Bool
pevalLtNumTerm (Term a -> Term Integer
forall a b. a -> b
unsafeCoerce Term a
j) (Integer -> Term Integer
forall t.
(SupportedPrim t, Typeable t, Hashable t, Eq t, Show t) =>
t -> Term t
conTerm (Integer -> Term Integer) -> Integer -> Term Integer
forall a b. (a -> b) -> a -> b
$ a -> Integer
forall a b. a -> b
unsafeCoerce a
k Integer -> Integer -> Integer
forall a. Num a => a -> a -> a
- Integer
i)
doPevalLtNumTerm (AddNumTerm Id
_ (ConTerm Id
_ (Dyn (Integer
j :: Integer))) 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 Integer -> Term Integer -> Term Bool
forall a.
(Num a, Ord a, SupportedPrim a) =>
Term a -> Term a -> Term Bool
pevalLtNumTerm (Integer -> Term Integer
forall t.
(SupportedPrim t, Typeable t, Hashable t, Eq t, Show t) =>
t -> Term t
conTerm Integer
j) (Term Integer -> Term Integer -> Term Integer
forall a. (Num a, SupportedPrim a) => Term a -> Term a -> Term a
pevalMinusNumTerm (Term a -> Term Integer
forall a b. a -> b
unsafeCoerce Term a
l) (Term a -> Term Integer
forall a b. a -> b
unsafeCoerce Term a
k))
doPevalLtNumTerm Term a
j (AddNumTerm Id
_ (ConTerm Id
_ (Dyn (Integer
k :: Integer))) 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 Integer -> Term Integer -> Term Bool
forall a.
(Num a, Ord a, SupportedPrim a) =>
Term a -> Term a -> Term Bool
pevalLtNumTerm (Integer -> Term Integer
forall t.
(SupportedPrim t, Typeable t, Hashable t, Eq t, Show t) =>
t -> Term t
conTerm (Integer -> Term Integer) -> Integer -> Term Integer
forall a b. (a -> b) -> a -> b
$ -Integer
k) (Term Integer -> Term Integer -> Term Integer
forall a. (Num a, SupportedPrim a) => Term a -> Term a -> Term a
pevalMinusNumTerm (Term a -> Term Integer
forall a b. a -> b
unsafeCoerce Term a
l) (Term a -> Term Integer
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)
forall a b. (Typeable a, Typeable b) => Maybe (a :~: b)
eqT @a @Integer of
    Just a :~: Integer
Refl ->
      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.
(Num a, Ord a, SupportedPrim a) =>
Term a -> Term a -> Term Bool
pevalLtNumTerm (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 a. (Num a, SupportedPrim a) => Term a -> Term a
pevalUMinusNumTerm Term a
l)
    Maybe (a :~: Integer)
_ -> Maybe (Term Bool)
forall a. Maybe a
Nothing
doPevalLtNumTerm Term a
_ Term a
_ = Maybe (Term Bool)
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 = 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.
(Num a, Ord a, SupportedPrim a) =>
Term a -> Term a -> Maybe (Term Bool)
doPevalLeNumTerm TotalRuleBinary a a Bool
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) = 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
doPevalLeNumTerm (ConTerm Id
_ a
l) (AddNumTerm Id
_ (ConTerm Id
_ (Dyn (Integer
j :: Integer))) 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 Integer -> Term Integer -> Term Bool
forall a.
(Num a, Ord a, SupportedPrim a) =>
Term a -> Term a -> Term Bool
pevalLeNumTerm (Integer -> Term Integer
forall t.
(SupportedPrim t, Typeable t, Hashable t, Eq t, Show t) =>
t -> Term t
conTerm (Integer -> Term Integer) -> Integer -> Term Integer
forall a b. (a -> b) -> a -> b
$ a -> Integer
forall a b. a -> b
unsafeCoerce a
l Integer -> Integer -> Integer
forall a. Num a => a -> a -> a
- Integer
j) (Term a -> Term Integer
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) =
  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 Integer -> Term Integer -> Term Bool
forall a.
(Num a, Ord a, SupportedPrim a) =>
Term a -> Term a -> Term Bool
pevalLeNumTerm (Term a -> Term Integer
forall a b. a -> b
unsafeCoerce Term a
j) (Integer -> Term Integer
forall t.
(SupportedPrim t, Typeable t, Hashable t, Eq t, Show t) =>
t -> Term t
conTerm (Integer -> Term Integer) -> Integer -> Term Integer
forall a b. (a -> b) -> a -> b
$ a -> Integer
forall a b. a -> b
unsafeCoerce a
k Integer -> Integer -> Integer
forall a. Num a => a -> a -> a
- Integer
i)
doPevalLeNumTerm (AddNumTerm Id
_ (ConTerm Id
_ (Dyn (Integer
j :: Integer))) 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 Integer -> Term Integer -> Term Bool
forall a.
(Num a, Ord a, SupportedPrim a) =>
Term a -> Term a -> Term Bool
pevalLeNumTerm (Integer -> Term Integer
forall t.
(SupportedPrim t, Typeable t, Hashable t, Eq t, Show t) =>
t -> Term t
conTerm Integer
j) (Term Integer -> Term Integer -> Term Integer
forall a. (Num a, SupportedPrim a) => Term a -> Term a -> Term a
pevalMinusNumTerm (Term a -> Term Integer
forall a b. a -> b
unsafeCoerce Term a
l) (Term a -> Term Integer
forall a b. a -> b
unsafeCoerce Term a
k))
doPevalLeNumTerm Term a
j (AddNumTerm Id
_ (ConTerm Id
_ (Dyn (Integer
k :: Integer))) 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 Integer -> Term Integer -> Term Bool
forall a.
(Num a, Ord a, SupportedPrim a) =>
Term a -> Term a -> Term Bool
pevalLeNumTerm (Integer -> Term Integer
forall t.
(SupportedPrim t, Typeable t, Hashable t, Eq t, Show t) =>
t -> Term t
conTerm (Integer -> Term Integer) -> Integer -> Term Integer
forall a b. (a -> b) -> a -> b
$ -Integer
k) (Term Integer -> Term Integer -> Term Integer
forall a. (Num a, SupportedPrim a) => Term a -> Term a -> Term a
pevalMinusNumTerm (Term a -> Term Integer
forall a b. a -> b
unsafeCoerce Term a
l) (Term a -> Term Integer
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)
forall a b. (Typeable a, Typeable b) => Maybe (a :~: b)
eqT @a @Integer of
    Just a :~: Integer
Refl ->
      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.
(Num a, Ord a, SupportedPrim a) =>
Term a -> Term a -> Term Bool
pevalLeNumTerm (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 a. (Num a, SupportedPrim a) => Term a -> Term a
pevalUMinusNumTerm Term a
l)
    Maybe (a :~: Integer)
_ -> Maybe (Term Bool)
forall a. Maybe a
Nothing
doPevalLeNumTerm Term a
_ Term a
_ = Maybe (Term Bool)
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 = (Term a -> Term a -> Term Bool) -> Term a -> Term a -> Term Bool
forall a b c. (a -> b -> c) -> b -> a -> c
flip Term a -> Term a -> Term Bool
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 = (Term a -> Term a -> Term Bool) -> Term a -> Term a -> Term Bool
forall a b c. (a -> b -> c) -> b -> a -> c
flip Term a -> Term a -> Term Bool
forall a.
(Num a, Ord a, SupportedPrim a) =>
Term a -> Term a -> Term Bool
pevalLeNumTerm