{-# LANGUAGE AllowAmbiguousTypes #-}
{-# LANGUAGE ExplicitNamespaces #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE PatternSynonyms #-}
{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE TypeApplications #-}
{-# LANGUAGE UndecidableInstances #-}
{-# LANGUAGE ViewPatterns #-}
module Grisette.IR.SymPrim.Data.Prim.PartialEval.Bool
( trueTerm,
falseTerm,
pattern BoolConTerm,
pattern TrueTerm,
pattern FalseTerm,
pattern BoolTerm,
pevalNotTerm,
pevalEqvTerm,
pevalNotEqvTerm,
pevalOrTerm,
pevalAndTerm,
pevalITETerm,
pevalImplyTerm,
pevalXorTerm,
)
where
import Control.Monad (msum)
import Data.Maybe (fromMaybe)
import Data.Typeable (cast, eqT, type (:~:) (Refl))
import Grisette.IR.SymPrim.Data.Prim.InternedTerm.InternedCtors
( andTerm,
conTerm,
eqvTerm,
iteTerm,
notTerm,
orTerm,
)
import Grisette.IR.SymPrim.Data.Prim.InternedTerm.Term
( SupportedPrim,
Term
( AddNumTerm,
AndTerm,
ConTerm,
EqvTerm,
ITETerm,
NotTerm,
OrTerm
),
)
import Grisette.IR.SymPrim.Data.Prim.InternedTerm.TermUtils
( castTerm,
)
import Grisette.IR.SymPrim.Data.Prim.Utils (pattern Dyn)
import Unsafe.Coerce (unsafeCoerce)
trueTerm :: Term Bool
trueTerm :: Term Bool
trueTerm = forall t.
(SupportedPrim t, Typeable t, Hashable t, Eq t, Show t) =>
t -> Term t
conTerm Bool
True
{-# INLINE trueTerm #-}
falseTerm :: Term Bool
falseTerm :: Term Bool
falseTerm = forall t.
(SupportedPrim t, Typeable t, Hashable t, Eq t, Show t) =>
t -> Term t
conTerm Bool
False
{-# INLINE falseTerm #-}
boolConTermView :: forall a. Term a -> Maybe Bool
boolConTermView :: forall a. Term a -> Maybe Bool
boolConTermView (ConTerm Id
_ a
b) = forall a b. (Typeable a, Typeable b) => a -> Maybe b
cast a
b
boolConTermView Term a
_ = forall a. Maybe a
Nothing
{-# INLINE boolConTermView #-}
pattern BoolConTerm :: Bool -> Term a
pattern $mBoolConTerm :: forall {r} {a}. Term a -> (Bool -> r) -> ((# #) -> r) -> r
BoolConTerm b <- (boolConTermView -> Just b)
pattern TrueTerm :: Term a
pattern $mTrueTerm :: forall {r} {a}. Term a -> ((# #) -> r) -> ((# #) -> r) -> r
TrueTerm <- BoolConTerm True
pattern FalseTerm :: Term a
pattern $mFalseTerm :: forall {r} {a}. Term a -> ((# #) -> r) -> ((# #) -> r) -> r
FalseTerm <- BoolConTerm False
pattern BoolTerm :: Term Bool -> Term a
pattern $mBoolTerm :: forall {r} {a}. Term a -> (Term Bool -> r) -> ((# #) -> r) -> r
BoolTerm b <- (castTerm -> Just b)
pevalNotTerm :: Term Bool -> Term Bool
pevalNotTerm :: Term Bool -> Term Bool
pevalNotTerm (NotTerm Id
_ Term Bool
tm) = Term Bool
tm
pevalNotTerm (ConTerm Id
_ Bool
a) = if Bool
a then Term Bool
falseTerm else Term Bool
trueTerm
pevalNotTerm (OrTerm Id
_ (NotTerm Id
_ Term Bool
n1) Term Bool
n2) = Term Bool -> Term Bool -> Term Bool
pevalAndTerm Term Bool
n1 (Term Bool -> Term Bool
pevalNotTerm Term Bool
n2)
pevalNotTerm (OrTerm Id
_ Term Bool
n1 (NotTerm Id
_ Term Bool
n2)) = Term Bool -> Term Bool -> Term Bool
pevalAndTerm (Term Bool -> Term Bool
pevalNotTerm Term Bool
n1) Term Bool
n2
pevalNotTerm (AndTerm Id
_ (NotTerm Id
_ Term Bool
n1) Term Bool
n2) = Term Bool -> Term Bool -> Term Bool
pevalOrTerm Term Bool
n1 (Term Bool -> Term Bool
pevalNotTerm Term Bool
n2)
pevalNotTerm (AndTerm Id
_ Term Bool
n1 (NotTerm Id
_ Term Bool
n2)) = Term Bool -> Term Bool -> Term Bool
pevalOrTerm (Term Bool -> Term Bool
pevalNotTerm Term Bool
n1) Term Bool
n2
pevalNotTerm Term Bool
tm = Term Bool -> Term Bool
notTerm Term Bool
tm
{-# INLINEABLE pevalNotTerm #-}
pevalEqvTerm :: forall a. (SupportedPrim a) => Term a -> Term a -> Term Bool
pevalEqvTerm :: forall a. SupportedPrim a => Term a -> Term a -> Term Bool
pevalEqvTerm l :: Term a
l@ConTerm {} r :: Term a
r@ConTerm {} = forall t.
(SupportedPrim t, Typeable t, Hashable t, Eq t, Show t) =>
t -> Term t
conTerm forall a b. (a -> b) -> a -> b
$ Term a
l forall a. Eq a => a -> a -> Bool
== Term a
r
pevalEqvTerm l :: Term a
l@ConTerm {} Term a
r = forall a. SupportedPrim a => Term a -> Term a -> Term Bool
pevalEqvTerm Term a
r Term a
l
pevalEqvTerm Term a
l (BoolConTerm Bool
rv) = if Bool
rv then forall a b. a -> b
unsafeCoerce Term a
l else Term Bool -> Term Bool
pevalNotTerm forall a b. (a -> b) -> a -> b
$ forall a b. a -> b
unsafeCoerce Term a
l
pevalEqvTerm (NotTerm Id
_ Term Bool
lv) Term a
r
| Term Bool
lv forall a. Eq a => a -> a -> Bool
== forall a b. a -> b
unsafeCoerce Term a
r = Term Bool
falseTerm
pevalEqvTerm Term a
l (NotTerm Id
_ Term Bool
rv)
| forall a b. a -> b
unsafeCoerce Term a
l forall a. Eq a => a -> a -> Bool
== Term Bool
rv = Term Bool
falseTerm
pevalEqvTerm
( AddNumTerm
Id
_
(ConTerm Id
_ a
c :: Term a)
(Dyn (Term a
v :: Term a))
)
(Dyn (ConTerm Id
_ a
c2 :: Term a)) =
forall a. SupportedPrim a => Term a -> Term a -> Term Bool
pevalEqvTerm Term a
v (forall t.
(SupportedPrim t, Typeable t, Hashable t, Eq t, Show t) =>
t -> Term t
conTerm forall a b. (a -> b) -> a -> b
$ a
c2 forall a. Num a => a -> a -> a
- a
c)
pevalEqvTerm
(Dyn (ConTerm Id
_ a
c2 :: Term a))
( AddNumTerm
Id
_
(Dyn (ConTerm Id
_ a
c :: Term a))
(Dyn (Term a
v :: Term a))
) =
forall a. SupportedPrim a => Term a -> Term a -> Term Bool
pevalEqvTerm Term a
v (forall t.
(SupportedPrim t, Typeable t, Hashable t, Eq t, Show t) =>
t -> Term t
conTerm forall a b. (a -> b) -> a -> b
$ a
c2 forall a. Num a => a -> a -> a
- a
c)
pevalEqvTerm Term a
l (ITETerm Id
_ Term Bool
c Term a
t Term a
f)
| Term a
l forall a. Eq a => a -> a -> Bool
== Term a
t = Term Bool -> Term Bool -> Term Bool
pevalOrTerm Term Bool
c (forall a. SupportedPrim a => Term a -> Term a -> Term Bool
pevalEqvTerm Term a
l Term a
f)
| Term a
l forall a. Eq a => a -> a -> Bool
== Term a
f = Term Bool -> Term Bool -> Term Bool
pevalOrTerm (Term Bool -> Term Bool
pevalNotTerm Term Bool
c) (forall a. SupportedPrim a => Term a -> Term a -> Term Bool
pevalEqvTerm Term a
l Term a
t)
pevalEqvTerm (ITETerm Id
_ Term Bool
c Term a
t Term a
f) Term a
r
| Term a
t forall a. Eq a => a -> a -> Bool
== Term a
r = Term Bool -> Term Bool -> Term Bool
pevalOrTerm Term Bool
c (forall a. SupportedPrim a => Term a -> Term a -> Term Bool
pevalEqvTerm Term a
f Term a
r)
| Term a
f forall a. Eq a => a -> a -> Bool
== Term a
r = Term Bool -> Term Bool -> Term Bool
pevalOrTerm (Term Bool -> Term Bool
pevalNotTerm Term Bool
c) (forall a. SupportedPrim a => Term a -> Term a -> Term Bool
pevalEqvTerm Term a
t Term a
r)
pevalEqvTerm Term a
l Term a
r
| Term a
l forall a. Eq a => a -> a -> Bool
== Term a
r = Term Bool
trueTerm
| Bool
otherwise = forall a. SupportedPrim a => Term a -> Term a -> Term Bool
eqvTerm Term a
l Term a
r
{-# INLINEABLE pevalEqvTerm #-}
pevalNotEqvTerm :: (SupportedPrim a) => Term a -> Term a -> Term Bool
pevalNotEqvTerm :: forall a. SupportedPrim a => Term a -> Term a -> Term Bool
pevalNotEqvTerm Term a
l Term a
r = Term Bool -> Term Bool
pevalNotTerm forall a b. (a -> b) -> a -> b
$ forall a. SupportedPrim a => Term a -> Term a -> Term Bool
pevalEqvTerm Term a
l Term a
r
{-# INLINE pevalNotEqvTerm #-}
pevalImpliesTerm :: Term Bool -> Term Bool -> Bool
pevalImpliesTerm :: Term Bool -> Term Bool -> Bool
pevalImpliesTerm (ConTerm Id
_ Bool
False) Term Bool
_ = Bool
True
pevalImpliesTerm Term Bool
_ (ConTerm Id
_ Bool
True) = Bool
True
pevalImpliesTerm
(EqvTerm Id
_ (Term t1
e1 :: Term a) (ec1 :: Term t1
ec1@(ConTerm Id
_ t1
_) :: Term b))
(NotTerm Id
_ (EqvTerm Id
_ (Dyn (Term t1
e2 :: Term a)) (Dyn (ec2 :: Term t1
ec2@(ConTerm Id
_ t1
_) :: Term b))))
| Term t1
e1 forall a. Eq a => a -> a -> Bool
== Term t1
e2 Bool -> Bool -> Bool
&& Term t1
ec1 forall a. Eq a => a -> a -> Bool
/= Term t1
ec2 = Bool
True
pevalImpliesTerm Term Bool
a Term Bool
b
| Term Bool
a forall a. Eq a => a -> a -> Bool
== Term Bool
b = Bool
True
| Bool
otherwise = Bool
False
{-# INLINE pevalImpliesTerm #-}
orEqFirst :: Term Bool -> Term Bool -> Bool
orEqFirst :: Term Bool -> Term Bool -> Bool
orEqFirst Term Bool
_ (ConTerm Id
_ Bool
False) = Bool
True
orEqFirst
(NotTerm Id
_ (EqvTerm Id
_ (Term t1
e1 :: Term a) (ec1 :: Term t1
ec1@(ConTerm Id
_ t1
_) :: Term b)))
(EqvTerm Id
_ (Dyn (Term t1
e2 :: Term a)) (Dyn (ec2 :: Term t1
ec2@(ConTerm Id
_ t1
_) :: Term b)))
| Term t1
e1 forall a. Eq a => a -> a -> Bool
== Term t1
e2 Bool -> Bool -> Bool
&& Term t1
ec1 forall a. Eq a => a -> a -> Bool
/= Term t1
ec2 = Bool
True
orEqFirst Term Bool
x Term Bool
y
| Term Bool
x forall a. Eq a => a -> a -> Bool
== Term Bool
y = Bool
True
| Bool
otherwise = Bool
False
{-# INLINE orEqFirst #-}
orEqTrue :: Term Bool -> Term Bool -> Bool
orEqTrue :: Term Bool -> Term Bool -> Bool
orEqTrue (ConTerm Id
_ Bool
True) Term Bool
_ = Bool
True
orEqTrue Term Bool
_ (ConTerm Id
_ Bool
True) = Bool
True
orEqTrue
(NotTerm Id
_ (EqvTerm Id
_ (Term t1
e1 :: Term a) (ec1 :: Term t1
ec1@(ConTerm Id
_ t1
_) :: Term b)))
(NotTerm Id
_ (EqvTerm Id
_ (Dyn (Term t1
e2 :: Term a)) (Dyn (ec2 :: Term t1
ec2@(ConTerm Id
_ t1
_) :: Term b))))
| Term t1
e1 forall a. Eq a => a -> a -> Bool
== Term t1
e2 Bool -> Bool -> Bool
&& Term t1
ec1 forall a. Eq a => a -> a -> Bool
/= Term t1
ec2 = Bool
True
orEqTrue (NotTerm Id
_ Term Bool
l) Term Bool
r | Term Bool
l forall a. Eq a => a -> a -> Bool
== Term Bool
r = Bool
True
orEqTrue Term Bool
l (NotTerm Id
_ Term Bool
r) | Term Bool
l forall a. Eq a => a -> a -> Bool
== Term Bool
r = Bool
True
orEqTrue Term Bool
_ Term Bool
_ = Bool
False
{-# INLINE orEqTrue #-}
andEqFirst :: Term Bool -> Term Bool -> Bool
andEqFirst :: Term Bool -> Term Bool -> Bool
andEqFirst Term Bool
_ (ConTerm Id
_ Bool
True) = Bool
True
andEqFirst
(EqvTerm Id
_ (Term t1
e1 :: Term a) (ec1 :: Term t1
ec1@(ConTerm Id
_ t1
_) :: Term b))
(NotTerm Id
_ (EqvTerm Id
_ (Dyn (Term t1
e2 :: Term a)) (Dyn (ec2 :: Term t1
ec2@(ConTerm Id
_ t1
_) :: Term b))))
| Term t1
e1 forall a. Eq a => a -> a -> Bool
== Term t1
e2 Bool -> Bool -> Bool
&& Term t1
ec1 forall a. Eq a => a -> a -> Bool
/= Term t1
ec2 = Bool
True
andEqFirst Term Bool
x Term Bool
y
| Term Bool
x forall a. Eq a => a -> a -> Bool
== Term Bool
y = Bool
True
| Bool
otherwise = Bool
False
{-# INLINE andEqFirst #-}
andEqFalse :: Term Bool -> Term Bool -> Bool
andEqFalse :: Term Bool -> Term Bool -> Bool
andEqFalse (ConTerm Id
_ Bool
False) Term Bool
_ = Bool
True
andEqFalse Term Bool
_ (ConTerm Id
_ Bool
False) = Bool
True
andEqFalse
(EqvTerm Id
_ (Term t1
e1 :: Term a) (ec1 :: Term t1
ec1@(ConTerm Id
_ t1
_) :: Term b))
(EqvTerm Id
_ (Dyn (Term t1
e2 :: Term a)) (Dyn (ec2 :: Term t1
ec2@(ConTerm Id
_ t1
_) :: Term b)))
| Term t1
e1 forall a. Eq a => a -> a -> Bool
== Term t1
e2 Bool -> Bool -> Bool
&& Term t1
ec1 forall a. Eq a => a -> a -> Bool
/= Term t1
ec2 = Bool
True
andEqFalse (NotTerm Id
_ Term Bool
x) Term Bool
y | Term Bool
x forall a. Eq a => a -> a -> Bool
== Term Bool
y = Bool
True
andEqFalse Term Bool
x (NotTerm Id
_ Term Bool
y) | Term Bool
x forall a. Eq a => a -> a -> Bool
== Term Bool
y = Bool
True
andEqFalse Term Bool
_ Term Bool
_ = Bool
False
{-# INLINE andEqFalse #-}
pevalOrTerm :: Term Bool -> Term Bool -> Term Bool
pevalOrTerm :: Term Bool -> Term Bool -> Term Bool
pevalOrTerm Term Bool
l Term Bool
r
| Term Bool -> Term Bool -> Bool
orEqTrue Term Bool
l Term Bool
r = Term Bool
trueTerm
| Term Bool -> Term Bool -> Bool
orEqFirst Term Bool
l Term Bool
r = Term Bool
l
| Term Bool -> Term Bool -> Bool
orEqFirst Term Bool
r Term Bool
l = Term Bool
r
pevalOrTerm Term Bool
l r :: Term Bool
r@(OrTerm Id
_ Term Bool
r1 Term Bool
r2)
| Term Bool -> Term Bool -> Bool
orEqTrue Term Bool
l Term Bool
r1 = Term Bool
trueTerm
| Term Bool -> Term Bool -> Bool
orEqTrue Term Bool
l Term Bool
r2 = Term Bool
trueTerm
| Term Bool -> Term Bool -> Bool
orEqFirst Term Bool
r1 Term Bool
l = Term Bool
r
| Term Bool -> Term Bool -> Bool
orEqFirst Term Bool
r2 Term Bool
l = Term Bool
r
| Term Bool -> Term Bool -> Bool
orEqFirst Term Bool
l Term Bool
r1 = Term Bool -> Term Bool -> Term Bool
pevalOrTerm Term Bool
l Term Bool
r2
| Term Bool -> Term Bool -> Bool
orEqFirst Term Bool
l Term Bool
r2 = Term Bool -> Term Bool -> Term Bool
pevalOrTerm Term Bool
l Term Bool
r1
pevalOrTerm l :: Term Bool
l@(OrTerm Id
_ Term Bool
l1 Term Bool
l2) Term Bool
r
| Term Bool -> Term Bool -> Bool
orEqTrue Term Bool
l1 Term Bool
r = Term Bool
trueTerm
| Term Bool -> Term Bool -> Bool
orEqTrue Term Bool
l2 Term Bool
r = Term Bool
trueTerm
| Term Bool -> Term Bool -> Bool
orEqFirst Term Bool
l1 Term Bool
r = Term Bool
l
| Term Bool -> Term Bool -> Bool
orEqFirst Term Bool
l2 Term Bool
r = Term Bool
l
| Term Bool -> Term Bool -> Bool
orEqFirst Term Bool
r Term Bool
l1 = Term Bool -> Term Bool -> Term Bool
pevalOrTerm Term Bool
l2 Term Bool
r
| Term Bool -> Term Bool -> Bool
orEqFirst Term Bool
r Term Bool
l2 = Term Bool -> Term Bool -> Term Bool
pevalOrTerm Term Bool
l1 Term Bool
r
pevalOrTerm Term Bool
l (AndTerm Id
_ Term Bool
r1 Term Bool
r2)
| Term Bool -> Term Bool -> Bool
orEqFirst Term Bool
l Term Bool
r1 = Term Bool
l
| Term Bool -> Term Bool -> Bool
orEqFirst Term Bool
l Term Bool
r2 = Term Bool
l
| Term Bool -> Term Bool -> Bool
orEqTrue Term Bool
l Term Bool
r1 = Term Bool -> Term Bool -> Term Bool
pevalOrTerm Term Bool
l Term Bool
r2
| Term Bool -> Term Bool -> Bool
orEqTrue Term Bool
l Term Bool
r2 = Term Bool -> Term Bool -> Term Bool
pevalOrTerm Term Bool
l Term Bool
r1
pevalOrTerm (AndTerm Id
_ Term Bool
l1 Term Bool
l2) Term Bool
r
| Term Bool -> Term Bool -> Bool
orEqFirst Term Bool
r Term Bool
l1 = Term Bool
r
| Term Bool -> Term Bool -> Bool
orEqFirst Term Bool
r Term Bool
l2 = Term Bool
r
| Term Bool -> Term Bool -> Bool
orEqTrue Term Bool
l1 Term Bool
r = Term Bool -> Term Bool -> Term Bool
pevalOrTerm Term Bool
l2 Term Bool
r
| Term Bool -> Term Bool -> Bool
orEqTrue Term Bool
l2 Term Bool
r = Term Bool -> Term Bool -> Term Bool
pevalOrTerm Term Bool
l1 Term Bool
r
pevalOrTerm (NotTerm Id
_ Term Bool
nl) (NotTerm Id
_ Term Bool
nr) = Term Bool -> Term Bool
pevalNotTerm forall a b. (a -> b) -> a -> b
$ Term Bool -> Term Bool -> Term Bool
pevalAndTerm Term Bool
nl Term Bool
nr
pevalOrTerm Term Bool
l Term Bool
r = Term Bool -> Term Bool -> Term Bool
orTerm Term Bool
l Term Bool
r
{-# INLINEABLE pevalOrTerm #-}
pevalAndTerm :: Term Bool -> Term Bool -> Term Bool
pevalAndTerm :: Term Bool -> Term Bool -> Term Bool
pevalAndTerm Term Bool
l Term Bool
r
| Term Bool -> Term Bool -> Bool
andEqFalse Term Bool
l Term Bool
r = Term Bool
falseTerm
| Term Bool -> Term Bool -> Bool
andEqFirst Term Bool
l Term Bool
r = Term Bool
l
| Term Bool -> Term Bool -> Bool
andEqFirst Term Bool
r Term Bool
l = Term Bool
r
pevalAndTerm Term Bool
l r :: Term Bool
r@(AndTerm Id
_ Term Bool
r1 Term Bool
r2)
| Term Bool -> Term Bool -> Bool
andEqFalse Term Bool
l Term Bool
r1 = Term Bool
falseTerm
| Term Bool -> Term Bool -> Bool
andEqFalse Term Bool
l Term Bool
r2 = Term Bool
falseTerm
| Term Bool -> Term Bool -> Bool
andEqFirst Term Bool
r1 Term Bool
l = Term Bool
r
| Term Bool -> Term Bool -> Bool
andEqFirst Term Bool
r2 Term Bool
l = Term Bool
r
| Term Bool -> Term Bool -> Bool
andEqFirst Term Bool
l Term Bool
r1 = Term Bool -> Term Bool -> Term Bool
pevalAndTerm Term Bool
l Term Bool
r2
| Term Bool -> Term Bool -> Bool
andEqFirst Term Bool
l Term Bool
r2 = Term Bool -> Term Bool -> Term Bool
pevalAndTerm Term Bool
l Term Bool
r1
pevalAndTerm l :: Term Bool
l@(AndTerm Id
_ Term Bool
l1 Term Bool
l2) Term Bool
r
| Term Bool -> Term Bool -> Bool
andEqFalse Term Bool
l1 Term Bool
r = Term Bool
falseTerm
| Term Bool -> Term Bool -> Bool
andEqFalse Term Bool
l2 Term Bool
r = Term Bool
falseTerm
| Term Bool -> Term Bool -> Bool
andEqFirst Term Bool
l1 Term Bool
r = Term Bool
l
| Term Bool -> Term Bool -> Bool
andEqFirst Term Bool
l2 Term Bool
r = Term Bool
l
| Term Bool -> Term Bool -> Bool
andEqFirst Term Bool
r Term Bool
l1 = Term Bool -> Term Bool -> Term Bool
pevalAndTerm Term Bool
l2 Term Bool
r
| Term Bool -> Term Bool -> Bool
andEqFirst Term Bool
r Term Bool
l2 = Term Bool -> Term Bool -> Term Bool
pevalAndTerm Term Bool
l1 Term Bool
r
pevalAndTerm Term Bool
l (OrTerm Id
_ Term Bool
r1 Term Bool
r2)
| Term Bool -> Term Bool -> Bool
andEqFirst Term Bool
l Term Bool
r1 = Term Bool
l
| Term Bool -> Term Bool -> Bool
andEqFirst Term Bool
l Term Bool
r2 = Term Bool
l
| Term Bool -> Term Bool -> Bool
andEqFalse Term Bool
l Term Bool
r1 = Term Bool -> Term Bool -> Term Bool
pevalAndTerm Term Bool
l Term Bool
r2
| Term Bool -> Term Bool -> Bool
andEqFalse Term Bool
l Term Bool
r2 = Term Bool -> Term Bool -> Term Bool
pevalAndTerm Term Bool
l Term Bool
r1
pevalAndTerm (OrTerm Id
_ Term Bool
l1 Term Bool
l2) Term Bool
r
| Term Bool -> Term Bool -> Bool
andEqFirst Term Bool
r Term Bool
l1 = Term Bool
r
| Term Bool -> Term Bool -> Bool
andEqFirst Term Bool
r Term Bool
l2 = Term Bool
r
| Term Bool -> Term Bool -> Bool
andEqFalse Term Bool
l1 Term Bool
r = Term Bool -> Term Bool -> Term Bool
pevalAndTerm Term Bool
l2 Term Bool
r
| Term Bool -> Term Bool -> Bool
andEqFalse Term Bool
l2 Term Bool
r = Term Bool -> Term Bool -> Term Bool
pevalAndTerm Term Bool
l1 Term Bool
r
pevalAndTerm (NotTerm Id
_ Term Bool
nl) (NotTerm Id
_ Term Bool
nr) = Term Bool -> Term Bool
pevalNotTerm forall a b. (a -> b) -> a -> b
$ Term Bool -> Term Bool -> Term Bool
pevalOrTerm Term Bool
nl Term Bool
nr
pevalAndTerm Term Bool
l Term Bool
r = Term Bool -> Term Bool -> Term Bool
andTerm Term Bool
l Term Bool
r
{-# INLINEABLE pevalAndTerm #-}
pevalITEBoolLeftNot :: Term Bool -> Term Bool -> Term Bool -> Maybe (Term Bool)
pevalITEBoolLeftNot :: Term Bool -> Term Bool -> Term Bool -> Maybe (Term Bool)
pevalITEBoolLeftNot Term Bool
cond Term Bool
nIfTrue Term Bool
ifFalse
| Term Bool
cond forall a. Eq a => a -> a -> Bool
== Term Bool
nIfTrue = forall a. a -> Maybe a
Just forall a b. (a -> b) -> a -> b
$ Term Bool -> Term Bool -> Term Bool
pevalAndTerm (Term Bool -> Term Bool
pevalNotTerm Term Bool
cond) Term Bool
ifFalse
| Bool
otherwise = case Term Bool
nIfTrue of
AndTerm Id
_ Term Bool
nt1 Term Bool
nt2 -> Maybe (Term Bool)
ra
where
ra :: Maybe (Term Bool)
ra
| Term Bool -> Term Bool -> Bool
pevalImpliesTerm Term Bool
cond Term Bool
nt1 = forall a. a -> Maybe a
Just forall a b. (a -> b) -> a -> b
$ forall a.
SupportedPrim a =>
Term Bool -> Term a -> Term a -> Term a
pevalITETerm Term Bool
cond (Term Bool -> Term Bool
pevalNotTerm Term Bool
nt2) Term Bool
ifFalse
| Term Bool -> Term Bool -> Bool
pevalImpliesTerm Term Bool
cond Term Bool
nt2 = forall a. a -> Maybe a
Just forall a b. (a -> b) -> a -> b
$ forall a.
SupportedPrim a =>
Term Bool -> Term a -> Term a -> Term a
pevalITETerm Term Bool
cond (Term Bool -> Term Bool
pevalNotTerm Term Bool
nt1) Term Bool
ifFalse
| Term Bool -> Term Bool -> Bool
pevalImpliesTerm Term Bool
cond (Term Bool -> Term Bool
pevalNotTerm Term Bool
nt1) Bool -> Bool -> Bool
|| Term Bool -> Term Bool -> Bool
pevalImpliesTerm Term Bool
cond (Term Bool -> Term Bool
pevalNotTerm Term Bool
nt2) =
forall a. a -> Maybe a
Just forall a b. (a -> b) -> a -> b
$ Term Bool -> Term Bool -> Term Bool
pevalOrTerm Term Bool
cond Term Bool
ifFalse
| Bool
otherwise = forall a. Maybe a
Nothing
OrTerm Id
_ Term Bool
nt1 Term Bool
nt2 -> Maybe (Term Bool)
ra
where
ra :: Maybe (Term Bool)
ra
| Term Bool -> Term Bool -> Bool
pevalImpliesTerm Term Bool
cond Term Bool
nt1 Bool -> Bool -> Bool
|| Term Bool -> Term Bool -> Bool
pevalImpliesTerm Term Bool
cond Term Bool
nt2 = forall a. a -> Maybe a
Just forall a b. (a -> b) -> a -> b
$ Term Bool -> Term Bool -> Term Bool
pevalAndTerm (Term Bool -> Term Bool
pevalNotTerm Term Bool
cond) Term Bool
ifFalse
| Term Bool -> Term Bool -> Bool
pevalImpliesTerm Term Bool
cond (Term Bool -> Term Bool
pevalNotTerm Term Bool
nt1) = forall a. a -> Maybe a
Just forall a b. (a -> b) -> a -> b
$ forall a.
SupportedPrim a =>
Term Bool -> Term a -> Term a -> Term a
pevalITETerm Term Bool
cond (Term Bool -> Term Bool
pevalNotTerm Term Bool
nt2) Term Bool
ifFalse
| Term Bool -> Term Bool -> Bool
pevalImpliesTerm Term Bool
cond (Term Bool -> Term Bool
pevalNotTerm Term Bool
nt2) = forall a. a -> Maybe a
Just forall a b. (a -> b) -> a -> b
$ forall a.
SupportedPrim a =>
Term Bool -> Term a -> Term a -> Term a
pevalITETerm Term Bool
cond (Term Bool -> Term Bool
pevalNotTerm Term Bool
nt1) Term Bool
ifFalse
| Bool
otherwise = forall a. Maybe a
Nothing
Term Bool
_ -> forall a. Maybe a
Nothing
pevalITEBoolBothNot :: Term Bool -> Term Bool -> Term Bool -> Maybe (Term Bool)
pevalITEBoolBothNot :: Term Bool -> Term Bool -> Term Bool -> Maybe (Term Bool)
pevalITEBoolBothNot Term Bool
cond Term Bool
nIfTrue Term Bool
nIfFalse = forall a. a -> Maybe a
Just forall a b. (a -> b) -> a -> b
$ Term Bool -> Term Bool
pevalNotTerm forall a b. (a -> b) -> a -> b
$ forall a.
SupportedPrim a =>
Term Bool -> Term a -> Term a -> Term a
pevalITETerm Term Bool
cond Term Bool
nIfTrue Term Bool
nIfFalse
pevalITEBoolRightNot :: Term Bool -> Term Bool -> Term Bool -> Maybe (Term Bool)
pevalITEBoolRightNot :: Term Bool -> Term Bool -> Term Bool -> Maybe (Term Bool)
pevalITEBoolRightNot Term Bool
cond Term Bool
ifTrue Term Bool
nIfFalse
| Term Bool
cond forall a. Eq a => a -> a -> Bool
== Term Bool
nIfFalse = forall a. a -> Maybe a
Just forall a b. (a -> b) -> a -> b
$ Term Bool -> Term Bool -> Term Bool
pevalOrTerm (Term Bool -> Term Bool
pevalNotTerm Term Bool
cond) Term Bool
ifTrue
| Bool
otherwise = forall a. Maybe a
Nothing
pevalInferImplies :: Term Bool -> Term Bool -> Term Bool -> Term Bool -> Maybe (Term Bool)
pevalInferImplies :: Term Bool
-> Term Bool -> Term Bool -> Term Bool -> Maybe (Term Bool)
pevalInferImplies Term Bool
cond (NotTerm Id
_ Term Bool
nt1) Term Bool
trueRes Term Bool
falseRes
| Term Bool
cond forall a. Eq a => a -> a -> Bool
== Term Bool
nt1 = forall a. a -> Maybe a
Just Term Bool
falseRes
| Bool
otherwise = case (Term Bool
cond, Term Bool
nt1) of
( EqvTerm Id
_ (Term t1
e1 :: Term a) (ec1 :: Term t1
ec1@(ConTerm Id
_ t1
_) :: Term b),
EqvTerm Id
_ (Dyn (Term t1
e2 :: Term a)) (Dyn (ec2 :: Term t1
ec2@(ConTerm Id
_ t1
_) :: Term b))
)
| Term t1
e1 forall a. Eq a => a -> a -> Bool
== Term t1
e2 Bool -> Bool -> Bool
&& Term t1
ec1 forall a. Eq a => a -> a -> Bool
/= Term t1
ec2 -> forall a. a -> Maybe a
Just Term Bool
trueRes
(Term Bool, Term Bool)
_ -> forall a. Maybe a
Nothing
pevalInferImplies
(EqvTerm Id
_ (Term t1
e1 :: Term a) (ec1 :: Term t1
ec1@(ConTerm Id
_ t1
_) :: Term b))
(EqvTerm Id
_ (Dyn (Term t1
e2 :: Term a)) (Dyn (ec2 :: Term t1
ec2@(ConTerm Id
_ t1
_) :: Term b)))
Term Bool
_
Term Bool
falseRes
| Term t1
e1 forall a. Eq a => a -> a -> Bool
== Term t1
e2 Bool -> Bool -> Bool
&& Term t1
ec1 forall a. Eq a => a -> a -> Bool
/= Term t1
ec2 = forall a. a -> Maybe a
Just Term Bool
falseRes
pevalInferImplies Term Bool
_ Term Bool
_ Term Bool
_ Term Bool
_ = forall a. Maybe a
Nothing
pevalITEBoolLeftAnd :: Term Bool -> Term Bool -> Term Bool -> Term Bool -> Maybe (Term Bool)
pevalITEBoolLeftAnd :: Term Bool
-> Term Bool -> Term Bool -> Term Bool -> Maybe (Term Bool)
pevalITEBoolLeftAnd Term Bool
cond Term Bool
t1 Term Bool
t2 Term Bool
ifFalse
| Term Bool
t1 forall a. Eq a => a -> a -> Bool
== Term Bool
ifFalse = forall a. a -> Maybe a
Just forall a b. (a -> b) -> a -> b
$ Term Bool -> Term Bool -> Term Bool
pevalAndTerm Term Bool
t1 forall a b. (a -> b) -> a -> b
$ Term Bool -> Term Bool -> Term Bool
pevalImplyTerm Term Bool
cond Term Bool
t2
| Term Bool
t2 forall a. Eq a => a -> a -> Bool
== Term Bool
ifFalse = forall a. a -> Maybe a
Just forall a b. (a -> b) -> a -> b
$ Term Bool -> Term Bool -> Term Bool
pevalAndTerm Term Bool
t2 forall a b. (a -> b) -> a -> b
$ Term Bool -> Term Bool -> Term Bool
pevalImplyTerm Term Bool
cond Term Bool
t1
| Term Bool
cond forall a. Eq a => a -> a -> Bool
== Term Bool
t1 = forall a. a -> Maybe a
Just forall a b. (a -> b) -> a -> b
$ forall a.
SupportedPrim a =>
Term Bool -> Term a -> Term a -> Term a
pevalITETerm Term Bool
cond Term Bool
t2 Term Bool
ifFalse
| Term Bool
cond forall a. Eq a => a -> a -> Bool
== Term Bool
t2 = forall a. a -> Maybe a
Just forall a b. (a -> b) -> a -> b
$ forall a.
SupportedPrim a =>
Term Bool -> Term a -> Term a -> Term a
pevalITETerm Term Bool
cond Term Bool
t1 Term Bool
ifFalse
| Bool
otherwise =
forall (t :: * -> *) (m :: * -> *) a.
(Foldable t, MonadPlus m) =>
t (m a) -> m a
msum
[ Term Bool
-> Term Bool -> Term Bool -> Term Bool -> Maybe (Term Bool)
pevalInferImplies Term Bool
cond Term Bool
t1 (forall a.
SupportedPrim a =>
Term Bool -> Term a -> Term a -> Term a
pevalITETerm Term Bool
cond Term Bool
t2 Term Bool
ifFalse) (Term Bool -> Term Bool -> Term Bool
pevalAndTerm (Term Bool -> Term Bool
pevalNotTerm Term Bool
cond) Term Bool
ifFalse),
Term Bool
-> Term Bool -> Term Bool -> Term Bool -> Maybe (Term Bool)
pevalInferImplies Term Bool
cond Term Bool
t2 (forall a.
SupportedPrim a =>
Term Bool -> Term a -> Term a -> Term a
pevalITETerm Term Bool
cond Term Bool
t1 Term Bool
ifFalse) (Term Bool -> Term Bool -> Term Bool
pevalAndTerm (Term Bool -> Term Bool
pevalNotTerm Term Bool
cond) Term Bool
ifFalse)
]
pevalITEBoolBothAnd :: Term Bool -> Term Bool -> Term Bool -> Term Bool -> Term Bool -> Maybe (Term Bool)
pevalITEBoolBothAnd :: Term Bool
-> Term Bool
-> Term Bool
-> Term Bool
-> Term Bool
-> Maybe (Term Bool)
pevalITEBoolBothAnd Term Bool
cond Term Bool
t1 Term Bool
t2 Term Bool
f1 Term Bool
f2
| Term Bool
t1 forall a. Eq a => a -> a -> Bool
== Term Bool
f1 = forall a. a -> Maybe a
Just forall a b. (a -> b) -> a -> b
$ Term Bool -> Term Bool -> Term Bool
pevalAndTerm Term Bool
t1 forall a b. (a -> b) -> a -> b
$ forall a.
SupportedPrim a =>
Term Bool -> Term a -> Term a -> Term a
pevalITETerm Term Bool
cond Term Bool
t2 Term Bool
f2
| Term Bool
t1 forall a. Eq a => a -> a -> Bool
== Term Bool
f2 = forall a. a -> Maybe a
Just forall a b. (a -> b) -> a -> b
$ Term Bool -> Term Bool -> Term Bool
pevalAndTerm Term Bool
t1 forall a b. (a -> b) -> a -> b
$ forall a.
SupportedPrim a =>
Term Bool -> Term a -> Term a -> Term a
pevalITETerm Term Bool
cond Term Bool
t2 Term Bool
f1
| Term Bool
t2 forall a. Eq a => a -> a -> Bool
== Term Bool
f1 = forall a. a -> Maybe a
Just forall a b. (a -> b) -> a -> b
$ Term Bool -> Term Bool -> Term Bool
pevalAndTerm Term Bool
t2 forall a b. (a -> b) -> a -> b
$ forall a.
SupportedPrim a =>
Term Bool -> Term a -> Term a -> Term a
pevalITETerm Term Bool
cond Term Bool
t1 Term Bool
f2
| Term Bool
t2 forall a. Eq a => a -> a -> Bool
== Term Bool
f2 = forall a. a -> Maybe a
Just forall a b. (a -> b) -> a -> b
$ Term Bool -> Term Bool -> Term Bool
pevalAndTerm Term Bool
t2 forall a b. (a -> b) -> a -> b
$ forall a.
SupportedPrim a =>
Term Bool -> Term a -> Term a -> Term a
pevalITETerm Term Bool
cond Term Bool
t1 Term Bool
f1
| Bool
otherwise = forall a. Maybe a
Nothing
pevalITEBoolRightAnd :: Term Bool -> Term Bool -> Term Bool -> Term Bool -> Maybe (Term Bool)
pevalITEBoolRightAnd :: Term Bool
-> Term Bool -> Term Bool -> Term Bool -> Maybe (Term Bool)
pevalITEBoolRightAnd Term Bool
cond Term Bool
ifTrue Term Bool
f1 Term Bool
f2
| Term Bool
f1 forall a. Eq a => a -> a -> Bool
== Term Bool
ifTrue = forall a. a -> Maybe a
Just forall a b. (a -> b) -> a -> b
$ Term Bool -> Term Bool -> Term Bool
pevalAndTerm Term Bool
f1 forall a b. (a -> b) -> a -> b
$ Term Bool -> Term Bool -> Term Bool
pevalOrTerm Term Bool
cond Term Bool
f2
| Term Bool
f2 forall a. Eq a => a -> a -> Bool
== Term Bool
ifTrue = forall a. a -> Maybe a
Just forall a b. (a -> b) -> a -> b
$ Term Bool -> Term Bool -> Term Bool
pevalAndTerm Term Bool
f2 forall a b. (a -> b) -> a -> b
$ Term Bool -> Term Bool -> Term Bool
pevalOrTerm Term Bool
cond Term Bool
f1
| Bool
otherwise = forall a. Maybe a
Nothing
pevalITEBoolLeftOr :: Term Bool -> Term Bool -> Term Bool -> Term Bool -> Maybe (Term Bool)
pevalITEBoolLeftOr :: Term Bool
-> Term Bool -> Term Bool -> Term Bool -> Maybe (Term Bool)
pevalITEBoolLeftOr Term Bool
cond Term Bool
t1 Term Bool
t2 Term Bool
ifFalse
| Term Bool
t1 forall a. Eq a => a -> a -> Bool
== Term Bool
ifFalse = forall a. a -> Maybe a
Just forall a b. (a -> b) -> a -> b
$ Term Bool -> Term Bool -> Term Bool
pevalOrTerm Term Bool
t1 forall a b. (a -> b) -> a -> b
$ Term Bool -> Term Bool -> Term Bool
pevalAndTerm Term Bool
cond Term Bool
t2
| Term Bool
t2 forall a. Eq a => a -> a -> Bool
== Term Bool
ifFalse = forall a. a -> Maybe a
Just forall a b. (a -> b) -> a -> b
$ Term Bool -> Term Bool -> Term Bool
pevalOrTerm Term Bool
t2 forall a b. (a -> b) -> a -> b
$ Term Bool -> Term Bool -> Term Bool
pevalAndTerm Term Bool
cond Term Bool
t1
| Term Bool
cond forall a. Eq a => a -> a -> Bool
== Term Bool
t1 = forall a. a -> Maybe a
Just forall a b. (a -> b) -> a -> b
$ Term Bool -> Term Bool -> Term Bool
pevalOrTerm Term Bool
cond Term Bool
ifFalse
| Term Bool
cond forall a. Eq a => a -> a -> Bool
== Term Bool
t2 = forall a. a -> Maybe a
Just forall a b. (a -> b) -> a -> b
$ Term Bool -> Term Bool -> Term Bool
pevalOrTerm Term Bool
cond Term Bool
ifFalse
| Bool
otherwise =
forall (t :: * -> *) (m :: * -> *) a.
(Foldable t, MonadPlus m) =>
t (m a) -> m a
msum
[ Term Bool
-> Term Bool -> Term Bool -> Term Bool -> Maybe (Term Bool)
pevalInferImplies Term Bool
cond Term Bool
t1 (Term Bool -> Term Bool -> Term Bool
pevalOrTerm Term Bool
cond Term Bool
ifFalse) (forall a.
SupportedPrim a =>
Term Bool -> Term a -> Term a -> Term a
pevalITETerm Term Bool
cond Term Bool
t2 Term Bool
ifFalse),
Term Bool
-> Term Bool -> Term Bool -> Term Bool -> Maybe (Term Bool)
pevalInferImplies Term Bool
cond Term Bool
t2 (Term Bool -> Term Bool -> Term Bool
pevalOrTerm Term Bool
cond Term Bool
ifFalse) (forall a.
SupportedPrim a =>
Term Bool -> Term a -> Term a -> Term a
pevalITETerm Term Bool
cond Term Bool
t1 Term Bool
ifFalse)
]
pevalITEBoolBothOr :: Term Bool -> Term Bool -> Term Bool -> Term Bool -> Term Bool -> Maybe (Term Bool)
pevalITEBoolBothOr :: Term Bool
-> Term Bool
-> Term Bool
-> Term Bool
-> Term Bool
-> Maybe (Term Bool)
pevalITEBoolBothOr Term Bool
cond Term Bool
t1 Term Bool
t2 Term Bool
f1 Term Bool
f2
| Term Bool
t1 forall a. Eq a => a -> a -> Bool
== Term Bool
f1 = forall a. a -> Maybe a
Just forall a b. (a -> b) -> a -> b
$ Term Bool -> Term Bool -> Term Bool
pevalOrTerm Term Bool
t1 forall a b. (a -> b) -> a -> b
$ forall a.
SupportedPrim a =>
Term Bool -> Term a -> Term a -> Term a
pevalITETerm Term Bool
cond Term Bool
t2 Term Bool
f2
| Term Bool
t1 forall a. Eq a => a -> a -> Bool
== Term Bool
f2 = forall a. a -> Maybe a
Just forall a b. (a -> b) -> a -> b
$ Term Bool -> Term Bool -> Term Bool
pevalOrTerm Term Bool
t1 forall a b. (a -> b) -> a -> b
$ forall a.
SupportedPrim a =>
Term Bool -> Term a -> Term a -> Term a
pevalITETerm Term Bool
cond Term Bool
t2 Term Bool
f1
| Term Bool
t2 forall a. Eq a => a -> a -> Bool
== Term Bool
f1 = forall a. a -> Maybe a
Just forall a b. (a -> b) -> a -> b
$ Term Bool -> Term Bool -> Term Bool
pevalOrTerm Term Bool
t2 forall a b. (a -> b) -> a -> b
$ forall a.
SupportedPrim a =>
Term Bool -> Term a -> Term a -> Term a
pevalITETerm Term Bool
cond Term Bool
t1 Term Bool
f2
| Term Bool
t2 forall a. Eq a => a -> a -> Bool
== Term Bool
f2 = forall a. a -> Maybe a
Just forall a b. (a -> b) -> a -> b
$ Term Bool -> Term Bool -> Term Bool
pevalOrTerm Term Bool
t2 forall a b. (a -> b) -> a -> b
$ forall a.
SupportedPrim a =>
Term Bool -> Term a -> Term a -> Term a
pevalITETerm Term Bool
cond Term Bool
t1 Term Bool
f1
| Bool
otherwise = forall a. Maybe a
Nothing
pevalITEBoolRightOr :: Term Bool -> Term Bool -> Term Bool -> Term Bool -> Maybe (Term Bool)
pevalITEBoolRightOr :: Term Bool
-> Term Bool -> Term Bool -> Term Bool -> Maybe (Term Bool)
pevalITEBoolRightOr Term Bool
cond Term Bool
ifTrue Term Bool
f1 Term Bool
f2
| Term Bool
f1 forall a. Eq a => a -> a -> Bool
== Term Bool
ifTrue = forall a. a -> Maybe a
Just forall a b. (a -> b) -> a -> b
$ Term Bool -> Term Bool -> Term Bool
pevalOrTerm Term Bool
f1 forall a b. (a -> b) -> a -> b
$ Term Bool -> Term Bool -> Term Bool
pevalAndTerm (Term Bool -> Term Bool
pevalNotTerm Term Bool
cond) Term Bool
f2
| Term Bool
f2 forall a. Eq a => a -> a -> Bool
== Term Bool
ifTrue = forall a. a -> Maybe a
Just forall a b. (a -> b) -> a -> b
$ Term Bool -> Term Bool -> Term Bool
pevalOrTerm Term Bool
f2 forall a b. (a -> b) -> a -> b
$ Term Bool -> Term Bool -> Term Bool
pevalAndTerm (Term Bool -> Term Bool
pevalNotTerm Term Bool
cond) Term Bool
f1
| Bool
otherwise = forall a. Maybe a
Nothing
pevalITEBoolLeft :: Term Bool -> Term Bool -> Term Bool -> Maybe (Term Bool)
pevalITEBoolLeft :: Term Bool -> Term Bool -> Term Bool -> Maybe (Term Bool)
pevalITEBoolLeft Term Bool
cond (AndTerm Id
_ Term Bool
t1 Term Bool
t2) Term Bool
ifFalse =
forall (t :: * -> *) (m :: * -> *) a.
(Foldable t, MonadPlus m) =>
t (m a) -> m a
msum
[ Term Bool
-> Term Bool -> Term Bool -> Term Bool -> Maybe (Term Bool)
pevalITEBoolLeftAnd Term Bool
cond Term Bool
t1 Term Bool
t2 Term Bool
ifFalse,
case Term Bool
ifFalse of
AndTerm Id
_ Term Bool
f1 Term Bool
f2 -> Term Bool
-> Term Bool
-> Term Bool
-> Term Bool
-> Term Bool
-> Maybe (Term Bool)
pevalITEBoolBothAnd Term Bool
cond Term Bool
t1 Term Bool
t2 Term Bool
f1 Term Bool
f2
Term Bool
_ -> forall a. Maybe a
Nothing
]
pevalITEBoolLeft Term Bool
cond (OrTerm Id
_ Term Bool
t1 Term Bool
t2) Term Bool
ifFalse =
forall (t :: * -> *) (m :: * -> *) a.
(Foldable t, MonadPlus m) =>
t (m a) -> m a
msum
[ Term Bool
-> Term Bool -> Term Bool -> Term Bool -> Maybe (Term Bool)
pevalITEBoolLeftOr Term Bool
cond Term Bool
t1 Term Bool
t2 Term Bool
ifFalse,
case Term Bool
ifFalse of
OrTerm Id
_ Term Bool
f1 Term Bool
f2 -> Term Bool
-> Term Bool
-> Term Bool
-> Term Bool
-> Term Bool
-> Maybe (Term Bool)
pevalITEBoolBothOr Term Bool
cond Term Bool
t1 Term Bool
t2 Term Bool
f1 Term Bool
f2
Term Bool
_ -> forall a. Maybe a
Nothing
]
pevalITEBoolLeft Term Bool
cond (NotTerm Id
_ Term Bool
nIfTrue) Term Bool
ifFalse =
forall (t :: * -> *) (m :: * -> *) a.
(Foldable t, MonadPlus m) =>
t (m a) -> m a
msum
[ Term Bool -> Term Bool -> Term Bool -> Maybe (Term Bool)
pevalITEBoolLeftNot Term Bool
cond Term Bool
nIfTrue Term Bool
ifFalse,
case Term Bool
ifFalse of
NotTerm Id
_ Term Bool
nIfFalse ->
Term Bool -> Term Bool -> Term Bool -> Maybe (Term Bool)
pevalITEBoolBothNot Term Bool
cond Term Bool
nIfTrue Term Bool
nIfFalse
Term Bool
_ -> forall a. Maybe a
Nothing
]
pevalITEBoolLeft Term Bool
_ Term Bool
_ Term Bool
_ = forall a. Maybe a
Nothing
pevalITEBoolNoLeft :: Term Bool -> Term Bool -> Term Bool -> Maybe (Term Bool)
pevalITEBoolNoLeft :: Term Bool -> Term Bool -> Term Bool -> Maybe (Term Bool)
pevalITEBoolNoLeft Term Bool
cond Term Bool
ifTrue (AndTerm Id
_ Term Bool
f1 Term Bool
f2) = Term Bool
-> Term Bool -> Term Bool -> Term Bool -> Maybe (Term Bool)
pevalITEBoolRightAnd Term Bool
cond Term Bool
ifTrue Term Bool
f1 Term Bool
f2
pevalITEBoolNoLeft Term Bool
cond Term Bool
ifTrue (OrTerm Id
_ Term Bool
f1 Term Bool
f2) = Term Bool
-> Term Bool -> Term Bool -> Term Bool -> Maybe (Term Bool)
pevalITEBoolRightOr Term Bool
cond Term Bool
ifTrue Term Bool
f1 Term Bool
f2
pevalITEBoolNoLeft Term Bool
cond Term Bool
ifTrue (NotTerm Id
_ Term Bool
nIfFalse) = Term Bool -> Term Bool -> Term Bool -> Maybe (Term Bool)
pevalITEBoolRightNot Term Bool
cond Term Bool
ifTrue Term Bool
nIfFalse
pevalITEBoolNoLeft Term Bool
_ Term Bool
_ Term Bool
_ = forall a. Maybe a
Nothing
pevalITEBasic :: (SupportedPrim a) => Term Bool -> Term a -> Term a -> Maybe (Term a)
pevalITEBasic :: forall a.
SupportedPrim a =>
Term Bool -> Term a -> Term a -> Maybe (Term a)
pevalITEBasic (ConTerm Id
_ Bool
True) Term a
ifTrue Term a
_ = forall a. a -> Maybe a
Just Term a
ifTrue
pevalITEBasic (ConTerm Id
_ Bool
False) Term a
_ Term a
ifFalse = forall a. a -> Maybe a
Just Term a
ifFalse
pevalITEBasic (NotTerm Id
_ Term Bool
ncond) Term a
ifTrue Term a
ifFalse = forall a. a -> Maybe a
Just forall a b. (a -> b) -> a -> b
$ forall a.
SupportedPrim a =>
Term Bool -> Term a -> Term a -> Term a
pevalITETerm Term Bool
ncond Term a
ifFalse Term a
ifTrue
pevalITEBasic Term Bool
_ Term a
ifTrue Term a
ifFalse | Term a
ifTrue forall a. Eq a => a -> a -> Bool
== Term a
ifFalse = forall a. a -> Maybe a
Just Term a
ifTrue
pevalITEBasic (ITETerm Id
_ Term Bool
cc Term Bool
ct Term Bool
cf) (ITETerm Id
_ Term Bool
tc Term a
tt Term a
tf) (ITETerm Id
_ Term Bool
fc Term a
ft Term a
ff)
| Term Bool
cc forall a. Eq a => a -> a -> Bool
== Term Bool
tc Bool -> Bool -> Bool
&& Term Bool
cc forall a. Eq a => a -> a -> Bool
== Term Bool
fc = forall a. a -> Maybe a
Just forall a b. (a -> b) -> a -> b
$ forall a.
SupportedPrim a =>
Term Bool -> Term a -> Term a -> Term a
pevalITETerm Term Bool
cc (forall a.
SupportedPrim a =>
Term Bool -> Term a -> Term a -> Term a
pevalITETerm Term Bool
ct Term a
tt Term a
ft) (forall a.
SupportedPrim a =>
Term Bool -> Term a -> Term a -> Term a
pevalITETerm Term Bool
cf Term a
tf Term a
ff)
pevalITEBasic Term Bool
cond (ITETerm Id
_ Term Bool
tc Term a
tt Term a
tf) Term a
ifFalse
| Term Bool
cond forall a. Eq a => a -> a -> Bool
== Term Bool
tc = forall a. a -> Maybe a
Just forall a b. (a -> b) -> a -> b
$ forall a.
SupportedPrim a =>
Term Bool -> Term a -> Term a -> Term a
pevalITETerm Term Bool
cond Term a
tt Term a
ifFalse
| Term a
tt forall a. Eq a => a -> a -> Bool
== Term a
ifFalse = forall a. a -> Maybe a
Just forall a b. (a -> b) -> a -> b
$ forall a.
SupportedPrim a =>
Term Bool -> Term a -> Term a -> Term a
pevalITETerm (Term Bool -> Term Bool -> Term Bool
pevalOrTerm (Term Bool -> Term Bool
pevalNotTerm Term Bool
cond) Term Bool
tc) Term a
tt Term a
tf
| Term a
tf forall a. Eq a => a -> a -> Bool
== Term a
ifFalse = forall a. a -> Maybe a
Just forall a b. (a -> b) -> a -> b
$ forall a.
SupportedPrim a =>
Term Bool -> Term a -> Term a -> Term a
pevalITETerm (Term Bool -> Term Bool -> Term Bool
pevalAndTerm Term Bool
cond Term Bool
tc) Term a
tt Term a
tf
pevalITEBasic Term Bool
cond Term a
ifTrue (ITETerm Id
_ Term Bool
fc Term a
ft Term a
ff)
| Term a
ifTrue forall a. Eq a => a -> a -> Bool
== Term a
ft = forall a. a -> Maybe a
Just forall a b. (a -> b) -> a -> b
$ forall a.
SupportedPrim a =>
Term Bool -> Term a -> Term a -> Term a
pevalITETerm (Term Bool -> Term Bool -> Term Bool
pevalOrTerm Term Bool
cond Term Bool
fc) Term a
ifTrue Term a
ff
| Term a
ifTrue forall a. Eq a => a -> a -> Bool
== Term a
ff = forall a. a -> Maybe a
Just forall a b. (a -> b) -> a -> b
$ forall a.
SupportedPrim a =>
Term Bool -> Term a -> Term a -> Term a
pevalITETerm (Term Bool -> Term Bool -> Term Bool
pevalOrTerm Term Bool
cond (Term Bool -> Term Bool
pevalNotTerm Term Bool
fc)) Term a
ifTrue Term a
ft
| Term Bool -> Term Bool -> Bool
pevalImpliesTerm Term Bool
fc Term Bool
cond = forall a. a -> Maybe a
Just forall a b. (a -> b) -> a -> b
$ forall a.
SupportedPrim a =>
Term Bool -> Term a -> Term a -> Term a
pevalITETerm Term Bool
cond Term a
ifTrue Term a
ff
pevalITEBasic Term Bool
_ Term a
_ Term a
_ = forall a. Maybe a
Nothing
pevalITEBoolBasic :: Term Bool -> Term Bool -> Term Bool -> Maybe (Term Bool)
pevalITEBoolBasic :: Term Bool -> Term Bool -> Term Bool -> Maybe (Term Bool)
pevalITEBoolBasic Term Bool
cond Term Bool
ifTrue Term Bool
ifFalse
| Term Bool
cond forall a. Eq a => a -> a -> Bool
== Term Bool
ifTrue = forall a. a -> Maybe a
Just forall a b. (a -> b) -> a -> b
$ Term Bool -> Term Bool -> Term Bool
pevalOrTerm Term Bool
cond Term Bool
ifFalse
| Term Bool
cond forall a. Eq a => a -> a -> Bool
== Term Bool
ifFalse = forall a. a -> Maybe a
Just forall a b. (a -> b) -> a -> b
$ Term Bool -> Term Bool -> Term Bool
pevalAndTerm Term Bool
cond Term Bool
ifTrue
pevalITEBoolBasic Term Bool
cond (ConTerm Id
_ Bool
v) Term Bool
ifFalse
| Bool
v = forall a. a -> Maybe a
Just forall a b. (a -> b) -> a -> b
$ Term Bool -> Term Bool -> Term Bool
pevalOrTerm Term Bool
cond Term Bool
ifFalse
| Bool
otherwise = forall a. a -> Maybe a
Just forall a b. (a -> b) -> a -> b
$ Term Bool -> Term Bool -> Term Bool
pevalAndTerm (Term Bool -> Term Bool
pevalNotTerm Term Bool
cond) Term Bool
ifFalse
pevalITEBoolBasic Term Bool
cond Term Bool
ifTrue (ConTerm Id
_ Bool
v)
| Bool
v = forall a. a -> Maybe a
Just forall a b. (a -> b) -> a -> b
$ Term Bool -> Term Bool -> Term Bool
pevalOrTerm (Term Bool -> Term Bool
pevalNotTerm Term Bool
cond) Term Bool
ifTrue
| Bool
otherwise = forall a. a -> Maybe a
Just forall a b. (a -> b) -> a -> b
$ Term Bool -> Term Bool -> Term Bool
pevalAndTerm Term Bool
cond Term Bool
ifTrue
pevalITEBoolBasic Term Bool
_ Term Bool
_ Term Bool
_ = forall a. Maybe a
Nothing
pevalITEBool :: Term Bool -> Term Bool -> Term Bool -> Maybe (Term Bool)
pevalITEBool :: Term Bool -> Term Bool -> Term Bool -> Maybe (Term Bool)
pevalITEBool Term Bool
cond Term Bool
ifTrue Term Bool
ifFalse =
forall (t :: * -> *) (m :: * -> *) a.
(Foldable t, MonadPlus m) =>
t (m a) -> m a
msum
[ forall a.
SupportedPrim a =>
Term Bool -> Term a -> Term a -> Maybe (Term a)
pevalITEBasic Term Bool
cond Term Bool
ifTrue Term Bool
ifFalse,
Term Bool -> Term Bool -> Term Bool -> Maybe (Term Bool)
pevalITEBoolBasic Term Bool
cond Term Bool
ifTrue Term Bool
ifFalse,
Term Bool -> Term Bool -> Term Bool -> Maybe (Term Bool)
pevalITEBoolLeft Term Bool
cond Term Bool
ifTrue Term Bool
ifFalse,
Term Bool -> Term Bool -> Term Bool -> Maybe (Term Bool)
pevalITEBoolNoLeft Term Bool
cond Term Bool
ifTrue Term Bool
ifFalse
]
pevalITETerm :: forall a. (SupportedPrim a) => Term Bool -> Term a -> Term a -> Term a
pevalITETerm :: forall a.
SupportedPrim a =>
Term Bool -> Term a -> Term a -> Term a
pevalITETerm Term Bool
cond Term a
ifTrue Term a
ifFalse = forall a. a -> Maybe a -> a
fromMaybe (forall a.
SupportedPrim a =>
Term Bool -> Term a -> Term a -> Term a
iteTerm Term Bool
cond Term a
ifTrue Term a
ifFalse) forall a b. (a -> b) -> a -> b
$
case forall {k} (a :: k) (b :: k).
(Typeable a, Typeable b) =>
Maybe (a :~: b)
eqT @a @Bool of
Maybe (a :~: Bool)
Nothing -> forall a.
SupportedPrim a =>
Term Bool -> Term a -> Term a -> Maybe (Term a)
pevalITEBasic Term Bool
cond Term a
ifTrue Term a
ifFalse
Just a :~: Bool
Refl -> Term Bool -> Term Bool -> Term Bool -> Maybe (Term Bool)
pevalITEBool Term Bool
cond Term a
ifTrue Term a
ifFalse
pevalImplyTerm :: Term Bool -> Term Bool -> Term Bool
pevalImplyTerm :: Term Bool -> Term Bool -> Term Bool
pevalImplyTerm Term Bool
l = Term Bool -> Term Bool -> Term Bool
pevalOrTerm (Term Bool -> Term Bool
pevalNotTerm Term Bool
l)
pevalXorTerm :: Term Bool -> Term Bool -> Term Bool
pevalXorTerm :: Term Bool -> Term Bool -> Term Bool
pevalXorTerm Term Bool
l Term Bool
r = Term Bool -> Term Bool -> Term Bool
pevalOrTerm (Term Bool -> Term Bool -> Term Bool
pevalAndTerm (Term Bool -> Term Bool
pevalNotTerm Term Bool
l) Term Bool
r) (Term Bool -> Term Bool -> Term Bool
pevalAndTerm Term Bool
l (Term Bool -> Term Bool
pevalNotTerm Term Bool
r))