{-# LANGUAGE AllowAmbiguousTypes #-}
{-# 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
-- 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.Bool
  ( trueTerm,
    falseTerm,
    pattern BoolConTerm,
    pattern TrueTerm,
    pattern FalseTerm,
    pattern BoolTerm,
    pevalNotTerm,
    pevalEqvTerm,
    pevalNotEqvTerm,
    pevalOrTerm,
    pevalAndTerm,
    pevalITETerm,
    pevalImplyTerm,
    pevalXorTerm,
  )
where

import Control.Monad
import Data.Maybe
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.InternedTerm.TermUtils
import Grisette.IR.SymPrim.Data.Prim.Utils
import Unsafe.Coerce

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)

-- Not
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 #-}

-- Eqv
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
{-
pevalBinary _ (ConTerm l) (ConTerm r) =
  if l == r then trueTerm else 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 _ e1) (NotTerm _ e2) = andEqFalse e1 e2
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 x (NotTerm _ y) = andEqFalse x y
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 (NotTerm _ e1) (NotTerm _ e2) = orEqTrue e1 e2
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 #-}

-- Or
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 -- need test
  | 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 -- need test
  | Bool
otherwise = forall a. Maybe a
Nothing -- need work

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) -- later
  | 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 -- later
  | 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) -- later
  | 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))