{-# LANGUAGE PartialTypeSignatures #-}
{-# OPTIONS_GHC -Wno-partial-type-signatures #-}
{-# OPTIONS_GHC -Wno-unrecognised-pragmas #-}
{-# HLINT ignore "Use camelCase" #-}
module PropaFP.DeriveBounds
where
import MixedTypesNumPrelude
import qualified Numeric.CollectErrors as CN
import qualified Prelude as P
import qualified Data.Map as Map
import qualified Data.List as List
import AERN2.MP.Ball
import AERN2.MP.Dyadic
import PropaFP.Expression
import PropaFP.VarMap
import Debug.Trace (trace)
import Data.List
_f1 :: F
_f1 :: F
_f1 = Conn -> F -> F -> F
FConn Conn
Impl (Conn -> F -> F -> F
FConn Conn
And (Comp -> E -> E -> F
FComp Comp
Le (VarName -> E
Var VarName
"x") (Rational -> E
Lit Rational
1.0)) (Comp -> E -> E -> F
FComp Comp
Le (Rational -> E
Lit Rational
0.0) (VarName -> E
Var VarName
"x"))) (Comp -> E -> E -> F
FComp Comp
Eq (Rational -> E
Lit Rational
0.0) (Rational -> E
Lit Rational
0.0))
_f2 :: F
_f2 :: F
_f2 = Conn -> F -> F -> F
FConn Conn
Impl (Conn -> F -> F -> F
FConn Conn
And (Comp -> E -> E -> F
FComp Comp
Le (VarName -> E
Var VarName
"x") (Rational -> E
Lit Rational
1.0)) (Comp -> E -> E -> F
FComp Comp
Le (Rational -> E
Lit Rational
0.0) (VarName -> E
Var VarName
"x"))) (Comp -> E -> E -> F
FComp Comp
Eq (VarName -> E
Var VarName
"x") (Rational -> E
Lit Rational
0.0))
_f3 :: F
_f3 :: F
_f3 = Conn -> F -> F -> F
FConn Conn
Impl (Conn -> F -> F -> F
FConn Conn
And (Comp -> E -> E -> F
FComp Comp
Le (VarName -> E
Var VarName
"x") (Rational -> E
Lit Rational
1.0)) (Comp -> E -> E -> F
FComp Comp
Le (VarName -> E
Var VarName
"x") (Rational -> E
Lit Rational
0.0))) (Comp -> E -> E -> F
FComp Comp
Eq (VarName -> E
Var VarName
"x") (Rational -> E
Lit Rational
0.0))
_f4 :: F
_f4 :: F
_f4 =
Conn -> F -> F -> F
FConn Conn
Impl
(Conn -> F -> F -> F
FConn Conn
And
(Conn -> F -> F -> F
FConn Conn
And
(Comp -> E -> E -> F
FComp Comp
Le (VarName -> E
Var VarName
"x") (Rational -> E
Lit Rational
1.0))
(Comp -> E -> E -> F
FComp Comp
Eq (VarName -> E
Var VarName
"n") (Rational -> E
Lit Rational
1.0)))
(Conn -> F -> F -> F
FConn Conn
Impl (Comp -> E -> E -> F
FComp Comp
Eq (VarName -> E
Var VarName
"n") (Rational -> E
Lit Rational
1.0)) (Comp -> E -> E -> F
FComp Comp
Le (Rational -> E
Lit Rational
0.0) (VarName -> E
Var VarName
"x"))))
(Comp -> E -> E -> F
FComp Comp
Eq (VarName -> E
Var VarName
"x") (Rational -> E
Lit Rational
0.0))
_f5 :: F
_f5 :: F
_f5 =
Conn -> F -> F -> F
FConn Conn
And
(
Conn -> F -> F -> F
FConn Conn
And
(Conn -> F -> F -> F
FConn Conn
And
(Comp -> E -> E -> F
FComp Comp
Ge (VarName -> E
Var VarName
"n") (Rational -> E
Lit Rational
0.0))
(Comp -> E -> E -> F
FComp Comp
Le (VarName -> E
Var VarName
"n") (Rational -> E
Lit Rational
2.0))
)
(Conn -> F -> F -> F
FConn Conn
And
(Conn -> F -> F -> F
FConn Conn
Impl
(Comp -> E -> E -> F
FComp Comp
Le (VarName -> E
Var VarName
"n") (Rational -> E
Lit Rational
1.0))
(Conn -> F -> F -> F
FConn Conn
And
(Comp -> E -> E -> F
FComp Comp
Ge (VarName -> E
Var VarName
"x") (Rational -> E
Lit (-Rational
1.0)))
(Comp -> E -> E -> F
FComp Comp
Le (VarName -> E
Var VarName
"x") (Rational -> E
Lit Rational
1.0))
)
)
(Conn -> F -> F -> F
FConn Conn
Impl
((Comp -> E -> E -> F
FComp Comp
Gt (VarName -> E
Var VarName
"n") (Rational -> E
Lit Rational
1.0)))
(Conn -> F -> F -> F
FConn Conn
And
(Comp -> E -> E -> F
FComp Comp
Ge (VarName -> E
Var VarName
"x") (Rational -> E
Lit (-Rational
1.0)))
(Comp -> E -> E -> F
FComp Comp
Le (VarName -> E
Var VarName
"x") (Rational -> E
Lit Rational
1.0))
)
)
)
)
(F -> F) -> F -> F
forall a b. (a -> b) -> a -> b
$
Comp -> E -> E -> F
FComp Comp
Ge (UnOp -> E -> E
EUnOp UnOp
Sin (VarName -> E
Var VarName
"x")) (Rational -> E
Lit Rational
0.0)
type VarName = String
deriveBoundsAndSimplify :: F -> (F, VarMap, [VarName])
deriveBoundsAndSimplify :: F -> (F, VarMap, [VarName])
deriveBoundsAndSimplify F
form' =
(F
finalSimplifiedF, VarMap
derivedRangesWithoutPoints, ((VarName, (Maybe Rational, Maybe Rational)) -> VarName)
-> [(VarName, (Maybe Rational, Maybe Rational))] -> [VarName]
forall a b. (a -> b) -> [a] -> [b]
map (VarName, (Maybe Rational, Maybe Rational)) -> VarName
forall a b. (a, b) -> a
fst [(VarName, (Maybe Rational, Maybe Rational))]
underivedRanges)
where
finalSimplifiedF :: F
finalSimplifiedF = F -> F
simplifyF F
simplifiedFWithSubstitutedPoints
simplifiedFWithSubstitutedPoints :: F
simplifiedFWithSubstitutedPoints = F -> [(VarName, Rational)] -> F
substitutePoints F
simplifiedF [(VarName, Rational)]
varsWithPoints
simplifiedF :: F
simplifiedF = (\(FConn Conn
Impl F
f F
FFalse) -> F
f) F
simplifiedFImpliesFalse
(VarMap
derivedRangesWithoutPoints, [(VarName, Rational)]
varsWithPoints) = VarMap -> (VarMap, [(VarName, Rational)])
seperatePoints VarMap
derivedRanges
derivedRanges :: VarMap
derivedRanges = ((VarName, (Maybe Rational, Maybe Rational))
-> (VarName, (Rational, Rational)))
-> [(VarName, (Maybe Rational, Maybe Rational))] -> VarMap
forall a b. (a -> b) -> [a] -> [b]
map (VarName, (Maybe Rational, Maybe Rational))
-> (VarName, (Rational, Rational))
forall {a} {a} {b}. (a, (Maybe a, Maybe b)) -> (a, (a, b))
removeJust [(VarName, (Maybe Rational, Maybe Rational))]
mDerivedRanges
([(VarName, (Maybe Rational, Maybe Rational))]
mDerivedRanges, [(VarName, (Maybe Rational, Maybe Rational))]
underivedRanges) = ((VarName, (Maybe Rational, Maybe Rational)) -> Bool)
-> [(VarName, (Maybe Rational, Maybe Rational))]
-> ([(VarName, (Maybe Rational, Maybe Rational))],
[(VarName, (Maybe Rational, Maybe Rational))])
forall a. (a -> Bool) -> [a] -> ([a], [a])
List.partition (VarName, (Maybe Rational, Maybe Rational)) -> Bool
forall {a} {a} {a}. (a, (Maybe a, Maybe a)) -> Bool
isGood [(VarName, (Maybe Rational, Maybe Rational))]
varRanges
isPoint :: (a, b) -> EqCompareType a b
isPoint (a
l, b
r) = a
l a -> b -> EqCompareType a b
forall a b. HasEqAsymmetric a b => a -> b -> EqCompareType a b
== b
r
substitutePoints :: F -> [(String, Rational)] -> F
substitutePoints :: F -> [(VarName, Rational)] -> F
substitutePoints F
f [] = F
f
substitutePoints F
f ((VarName
var, Rational
val) : [(VarName, Rational)]
varPoints) = F -> [(VarName, Rational)] -> F
substitutePoints (F -> VarName -> Rational -> F
substVarFWithLit F
f VarName
var Rational
val) [(VarName, Rational)]
varPoints
seperatePoints :: VarMap -> (VarMap, [(String, Rational)])
seperatePoints :: VarMap -> (VarMap, [(VarName, Rational)])
seperatePoints [] = ([], [])
seperatePoints ((VarName
var, (Rational, Rational)
bounds) : VarMap
varMap) =
if (Rational, Rational) -> EqCompareType Rational Rational
forall {a} {b}. HasEqAsymmetric a b => (a, b) -> EqCompareType a b
isPoint (Rational, Rational)
bounds
then (VarMap
resultingVarMap, (VarName
var, (Rational, Rational) -> Rational
forall a b. (a, b) -> a
fst (Rational, Rational)
bounds) (VarName, Rational)
-> [(VarName, Rational)] -> [(VarName, Rational)]
forall a. a -> [a] -> [a]
: [(VarName, Rational)]
resultingPoints)
else ((VarName
var, (Rational, Rational)
bounds) (VarName, (Rational, Rational)) -> VarMap -> VarMap
forall a. a -> [a] -> [a]
: VarMap
resultingVarMap, [(VarName, Rational)]
resultingPoints)
where
(VarMap
resultingVarMap, [(VarName, Rational)]
resultingPoints) = VarMap -> (VarMap, [(VarName, Rational)])
seperatePoints VarMap
varMap
form :: F
form = Conn -> F -> F -> F
FConn Conn
Impl F
form' F
FFalse
removeJust :: (a, (Maybe a, Maybe b)) -> (a, (a, b))
removeJust (a
v, (Just a
l, Just b
r)) = (a
v, (a
l, b
r))
removeJust (a, (Maybe a, Maybe b))
_ = VarName -> (a, (a, b))
forall a. HasCallStack => VarName -> a
error VarName
"deriveBounds: removeJust failed"
varRanges :: [(VarName, (Maybe Rational, Maybe Rational))]
varRanges = VarBoundMap -> [(VarName, (Maybe Rational, Maybe Rational))]
forall k a. Map k a -> [(k, a)]
Map.toList VarBoundMap
box
isGood :: (a, (Maybe a, Maybe a)) -> Bool
isGood (a
_v, (Just a
_,Just a
_)) = Bool
True
isGood (a, (Maybe a, Maybe a))
_ = Bool
False
initBox :: VarBoundMap
initBox = [(VarName, (Maybe Rational, Maybe Rational))] -> VarBoundMap
forall k a. Ord k => [(k, a)] -> Map k a
Map.fromList ([(VarName, (Maybe Rational, Maybe Rational))] -> VarBoundMap)
-> [(VarName, (Maybe Rational, Maybe Rational))] -> VarBoundMap
forall a b. (a -> b) -> a -> b
$ [VarName]
-> [(Maybe Rational, Maybe Rational)]
-> [(VarName, (Maybe Rational, Maybe Rational))]
forall a b. [a] -> [b] -> [(a, b)]
zip (F -> [VarName]
extractVariablesF F
form) ((Maybe Rational, Maybe Rational)
-> [(Maybe Rational, Maybe Rational)]
forall a. a -> [a]
repeat (Maybe Rational
forall a. Maybe a
Nothing, Maybe Rational
forall a. Maybe a
Nothing))
(VarBoundMap
box, F
simplifiedFImpliesFalse) = VarBoundMap -> F -> (VarBoundMap, F)
aux VarBoundMap
initBox (F -> (VarBoundMap, F)) -> F -> (VarBoundMap, F)
forall a b. (a -> b) -> a -> b
$ F
form
where
aux :: VarBoundMap -> F -> (VarBoundMap, F)
aux VarBoundMap
b F
f
| VarBoundMap
b VarBoundMap -> VarBoundMap -> Bool
forall a. Eq a => a -> a -> Bool
P.== VarBoundMap
b2 = (VarBoundMap
b, F
f2)
| Bool
otherwise = VarBoundMap -> F -> (VarBoundMap, F)
aux VarBoundMap
b2 F
f2
where
f2 :: F
f2 = (\(FConn Conn
Impl F
form2 F
_falseTerm) -> Conn -> F -> F -> F
FConn Conn
Impl (F -> F
simplifyF F
form2) F
_falseTerm) (VarBoundMap -> F -> F
evalF_comparisons VarBoundMap
b F
f)
b' :: VarBoundMap
b' = VarBoundMap -> Map VarName () -> VarBoundMap
forall k a b. Ord k => Map k a -> Map k b -> Map k a
Map.intersection VarBoundMap
b (Map VarName () -> VarBoundMap) -> Map VarName () -> VarBoundMap
forall a b. (a -> b) -> a -> b
$ [(VarName, ())] -> Map VarName ()
forall k a. Ord k => [(k, a)] -> Map k a
Map.fromList ([(VarName, ())] -> Map VarName ())
-> [(VarName, ())] -> Map VarName ()
forall a b. (a -> b) -> a -> b
$ [VarName] -> [()] -> [(VarName, ())]
forall a b. [a] -> [b] -> [(a, b)]
zip (F -> [VarName]
extractVariablesF F
f2) (() -> [()]
forall a. a -> [a]
repeat ())
b2 :: VarBoundMap
b2 = F -> VarBoundMap -> VarBoundMap
scanHypotheses F
f2 VarBoundMap
b'
type VarBoundMap = Map.Map VarName (Maybe Rational, Maybe Rational)
scanHypotheses :: F -> VarBoundMap -> VarBoundMap
scanHypotheses :: F -> VarBoundMap -> VarBoundMap
scanHypotheses (FConn Conn
Impl F
h F
c) =
F -> VarBoundMap -> VarBoundMap
scanHypotheses F
c (VarBoundMap -> VarBoundMap)
-> (VarBoundMap -> VarBoundMap) -> VarBoundMap -> VarBoundMap
forall b c a. (b -> c) -> (a -> b) -> a -> c
. F -> Bool -> VarBoundMap -> VarBoundMap
scanHypothesis F
h Bool
False
scanHypotheses F
_ = VarBoundMap -> VarBoundMap
forall a. a -> a
id
scanHypothesis :: F -> Bool -> VarBoundMap -> VarBoundMap
scanHypothesis :: F -> Bool -> VarBoundMap -> VarBoundMap
scanHypothesis (FNot F
h) Bool
isNegated VarBoundMap
intervals = F -> Bool -> VarBoundMap -> VarBoundMap
scanHypothesis F
h (Bool -> NegType Bool
forall t. CanNeg t => t -> NegType t
not Bool
isNegated) VarBoundMap
intervals
scanHypothesis (FConn Conn
And (FConn Conn
Impl F
cond1 F
branch1) (FConn Conn
Impl (FNot F
cond2) F
branch2)) Bool
False VarBoundMap
intervals
| F
cond1 F -> F -> Bool
forall a. Eq a => a -> a -> Bool
P.== F
cond2 = F -> Bool -> VarBoundMap -> VarBoundMap
scanHypothesis (Conn -> F -> F -> F
FConn Conn
Or F
branch1 F
branch2) Bool
False VarBoundMap
intervals
| F -> F
normalizeBoolean F
cond1 F -> F -> Bool
forall a. Eq a => a -> a -> Bool
P.== F -> F
normalizeBoolean F
cond2 = F -> Bool -> VarBoundMap -> VarBoundMap
scanHypothesis (Conn -> F -> F -> F
FConn Conn
Or F
branch1 F
branch2) Bool
False VarBoundMap
intervals
| [[ESafe]] -> [[ESafe]]
forall a. Ord a => [a] -> [a]
sort ([[ESafe]] -> [[ESafe]]
simplifyESafeDoubleList (F -> [[ESafe]]
fToEDNF (F -> F
simplifyF F
cond1))) [[ESafe]] -> [[ESafe]] -> Bool
forall a. Eq a => a -> a -> Bool
P.== [[ESafe]] -> [[ESafe]]
forall a. Ord a => [a] -> [a]
sort ([[ESafe]] -> [[ESafe]]
simplifyESafeDoubleList (F -> [[ESafe]]
fToEDNF (F -> F
simplifyF F
cond2))) = F -> Bool -> VarBoundMap -> VarBoundMap
scanHypothesis (Conn -> F -> F -> F
FConn Conn
Or F
branch1 F
branch2) Bool
False VarBoundMap
intervals
scanHypothesis (FConn Conn
And F
h1 F
h2) Bool
isNegated VarBoundMap
intervals =
if Bool
isNegated
then F -> Bool -> VarBoundMap -> VarBoundMap
scanHypothesis (Conn -> F -> F -> F
FConn Conn
Or (F -> F
FNot F
h1) (F -> F
FNot F
h2)) Bool
False VarBoundMap
intervals
else (F -> Bool -> VarBoundMap -> VarBoundMap
scanHypothesis F
h1 Bool
isNegated (VarBoundMap -> VarBoundMap)
-> (VarBoundMap -> VarBoundMap) -> VarBoundMap -> VarBoundMap
forall b c a. (b -> c) -> (a -> b) -> a -> c
. F -> Bool -> VarBoundMap -> VarBoundMap
scanHypothesis F
h2 Bool
isNegated) VarBoundMap
intervals
scanHypothesis (FConn Conn
Or F
h1 F
h2) Bool
isNegated VarBoundMap
intervals =
if Bool
isNegated
then F -> Bool -> VarBoundMap -> VarBoundMap
scanHypothesis (Conn -> F -> F -> F
FConn Conn
And (F -> F
FNot F
h1) (F -> F
FNot F
h2)) Bool
False VarBoundMap
intervals
else ((Maybe Rational, Maybe Rational)
-> (Maybe Rational, Maybe Rational)
-> (Maybe Rational, Maybe Rational))
-> VarBoundMap -> VarBoundMap -> VarBoundMap
forall k a. Ord k => (a -> a -> a) -> Map k a -> Map k a -> Map k a
Map.unionWith (Maybe Rational, Maybe Rational)
-> (Maybe Rational, Maybe Rational)
-> (Maybe Rational, Maybe Rational)
forall {f :: * -> *} {f :: * -> *} {a} {a} {a} {a}.
(Applicative f, Applicative f, CanMinMaxAsymmetric a a,
CanMinMaxAsymmetric a a) =>
(f a, f a)
-> (f a, f a) -> (f (MinMaxType a a), f (MinMaxType a a))
mergeWorse VarBoundMap
box1 VarBoundMap
box2
where
box1 :: VarBoundMap
box1 = (VarBoundMap -> VarBoundMap) -> VarBoundMap -> VarBoundMap
forall {t}. Eq t => (t -> t) -> t -> t
iterateUntilNoChange (F -> Bool -> VarBoundMap -> VarBoundMap
scanHypothesis F
h1 Bool
isNegated) VarBoundMap
intervals
box2 :: VarBoundMap
box2 = (VarBoundMap -> VarBoundMap) -> VarBoundMap -> VarBoundMap
forall {t}. Eq t => (t -> t) -> t -> t
iterateUntilNoChange (F -> Bool -> VarBoundMap -> VarBoundMap
scanHypothesis F
h2 Bool
isNegated) VarBoundMap
intervals
mergeWorse :: (f a, f a)
-> (f a, f a) -> (f (MinMaxType a a), f (MinMaxType a a))
mergeWorse (f a
l1,f a
r1) (f a
l2,f a
r2) = (a -> a -> MinMaxType a a
forall t1 t2.
CanMinMaxAsymmetric t1 t2 =>
t1 -> t2 -> MinMaxType t1 t2
min (a -> a -> MinMaxType a a) -> f a -> f (a -> MinMaxType a a)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> f a
l1 f (a -> MinMaxType a a) -> f a -> f (MinMaxType a a)
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> f a
l2, a -> a -> MinMaxType a a
forall t1 t2.
CanMinMaxAsymmetric t1 t2 =>
t1 -> t2 -> MinMaxType t1 t2
max (a -> a -> MinMaxType a a) -> f a -> f (a -> MinMaxType a a)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> f a
r1 f (a -> MinMaxType a a) -> f a -> f (MinMaxType a a)
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> f a
r2)
iterateUntilNoChange :: (t -> t) -> t -> t
iterateUntilNoChange t -> t
refineBox t
b1
| t
b1 t -> t -> Bool
forall a. Eq a => a -> a -> Bool
P.== t
b2 = t
b1
| Bool
otherwise = (t -> t) -> t -> t
iterateUntilNoChange t -> t
refineBox t
b2
where
b2 :: t
b2 = t -> t
refineBox t
b1
scanHypothesis (FConn Conn
Impl F
h1 F
h2) Bool
isNegated VarBoundMap
intervals = F -> Bool -> VarBoundMap -> VarBoundMap
scanHypothesis (Conn -> F -> F -> F
FConn Conn
Or (F -> F
FNot F
h1) F
h2) Bool
isNegated VarBoundMap
intervals
scanHypothesis (FComp Comp
Eq E
_ E
_) Bool
True VarBoundMap
intervals = VarBoundMap
intervals
scanHypothesis (FComp Comp
Eq _e1 :: E
_e1@(Var VarName
v1) _e2 :: E
_e2@(Var VarName
v2)) Bool
False VarBoundMap
intervals =
VarName
-> (Maybe Rational, Maybe Rational) -> VarBoundMap -> VarBoundMap
forall k a. Ord k => k -> a -> Map k a -> Map k a
Map.insert VarName
v1 (Maybe Rational, Maybe Rational)
val (VarBoundMap -> VarBoundMap) -> VarBoundMap -> VarBoundMap
forall a b. (a -> b) -> a -> b
$
VarName
-> (Maybe Rational, Maybe Rational) -> VarBoundMap -> VarBoundMap
forall k a. Ord k => k -> a -> Map k a -> Map k a
Map.insert VarName
v2 (Maybe Rational, Maybe Rational)
val (VarBoundMap -> VarBoundMap) -> VarBoundMap -> VarBoundMap
forall a b. (a -> b) -> a -> b
$
VarBoundMap
intervals
where
Just (Maybe Rational, Maybe Rational)
val1 = VarName -> VarBoundMap -> Maybe (Maybe Rational, Maybe Rational)
forall k a. Ord k => k -> Map k a -> Maybe a
Map.lookup VarName
v1 VarBoundMap
intervals
Just (Maybe Rational, Maybe Rational)
val2 = VarName -> VarBoundMap -> Maybe (Maybe Rational, Maybe Rational)
forall k a. Ord k => k -> Map k a -> Maybe a
Map.lookup VarName
v2 VarBoundMap
intervals
val :: (Maybe Rational, Maybe Rational)
val = (Maybe Rational, Maybe Rational)
-> (Maybe Rational, Maybe Rational)
-> (Maybe Rational, Maybe Rational)
forall a t t1.
CanMinMaxSameType a =>
(t, Maybe a) -> (t1, Maybe a) -> (t1, Maybe a)
updateUpper (Maybe Rational, Maybe Rational)
val1 ((Maybe Rational, Maybe Rational)
-> (Maybe Rational, Maybe Rational))
-> (Maybe Rational, Maybe Rational)
-> (Maybe Rational, Maybe Rational)
forall a b. (a -> b) -> a -> b
$ (Maybe Rational, Maybe Rational)
-> (Maybe Rational, Maybe Rational)
-> (Maybe Rational, Maybe Rational)
forall a t t1.
CanMinMaxSameType a =>
(Maybe a, t) -> (Maybe a, t1) -> (Maybe a, t1)
updateLower (Maybe Rational, Maybe Rational)
val1 ((Maybe Rational, Maybe Rational)
-> (Maybe Rational, Maybe Rational))
-> (Maybe Rational, Maybe Rational)
-> (Maybe Rational, Maybe Rational)
forall a b. (a -> b) -> a -> b
$ (Maybe Rational, Maybe Rational)
val2
scanHypothesis (FComp Comp
Eq (Var VarName
v) E
e) Bool
False VarBoundMap
intervals =
((Maybe Rational, Maybe Rational)
-> (Maybe Rational, Maybe Rational)
-> (Maybe Rational, Maybe Rational))
-> VarName
-> (Maybe Rational, Maybe Rational)
-> VarBoundMap
-> VarBoundMap
forall k a. Ord k => (a -> a -> a) -> k -> a -> Map k a -> Map k a
Map.insertWith (Maybe Rational, Maybe Rational)
-> (Maybe Rational, Maybe Rational)
-> (Maybe Rational, Maybe Rational)
forall a t t1.
CanMinMaxSameType a =>
(t, Maybe a) -> (t1, Maybe a) -> (t1, Maybe a)
updateUpper VarName
v (Maybe Rational, Maybe Rational)
val (VarBoundMap -> VarBoundMap) -> VarBoundMap -> VarBoundMap
forall a b. (a -> b) -> a -> b
$
((Maybe Rational, Maybe Rational)
-> (Maybe Rational, Maybe Rational)
-> (Maybe Rational, Maybe Rational))
-> VarName
-> (Maybe Rational, Maybe Rational)
-> VarBoundMap
-> VarBoundMap
forall k a. Ord k => (a -> a -> a) -> k -> a -> Map k a -> Map k a
Map.insertWith (Maybe Rational, Maybe Rational)
-> (Maybe Rational, Maybe Rational)
-> (Maybe Rational, Maybe Rational)
forall a t t1.
CanMinMaxSameType a =>
(Maybe a, t) -> (Maybe a, t1) -> (Maybe a, t1)
updateLower VarName
v (Maybe Rational, Maybe Rational)
val VarBoundMap
intervals
where
val :: (Maybe Rational, Maybe Rational)
val = VarBoundMap -> E -> (Maybe Rational, Maybe Rational)
evalE_Rational VarBoundMap
intervals E
e
scanHypothesis (FComp Comp
Eq E
e (Var VarName
v)) Bool
False VarBoundMap
intervals =
((Maybe Rational, Maybe Rational)
-> (Maybe Rational, Maybe Rational)
-> (Maybe Rational, Maybe Rational))
-> VarName
-> (Maybe Rational, Maybe Rational)
-> VarBoundMap
-> VarBoundMap
forall k a. Ord k => (a -> a -> a) -> k -> a -> Map k a -> Map k a
Map.insertWith (Maybe Rational, Maybe Rational)
-> (Maybe Rational, Maybe Rational)
-> (Maybe Rational, Maybe Rational)
forall a t t1.
CanMinMaxSameType a =>
(t, Maybe a) -> (t1, Maybe a) -> (t1, Maybe a)
updateUpper VarName
v (Maybe Rational, Maybe Rational)
val (VarBoundMap -> VarBoundMap) -> VarBoundMap -> VarBoundMap
forall a b. (a -> b) -> a -> b
$
((Maybe Rational, Maybe Rational)
-> (Maybe Rational, Maybe Rational)
-> (Maybe Rational, Maybe Rational))
-> VarName
-> (Maybe Rational, Maybe Rational)
-> VarBoundMap
-> VarBoundMap
forall k a. Ord k => (a -> a -> a) -> k -> a -> Map k a -> Map k a
Map.insertWith (Maybe Rational, Maybe Rational)
-> (Maybe Rational, Maybe Rational)
-> (Maybe Rational, Maybe Rational)
forall a t t1.
CanMinMaxSameType a =>
(Maybe a, t) -> (Maybe a, t1) -> (Maybe a, t1)
updateLower VarName
v (Maybe Rational, Maybe Rational)
val VarBoundMap
intervals
where
val :: (Maybe Rational, Maybe Rational)
val = VarBoundMap -> E -> (Maybe Rational, Maybe Rational)
evalE_Rational VarBoundMap
intervals E
e
scanHypothesis (FComp Comp
Le E
e1 E
e2) Bool
True VarBoundMap
intervals =
F -> Bool -> VarBoundMap -> VarBoundMap
scanHypothesis (Comp -> E -> E -> F
FComp Comp
Gt E
e1 E
e2) Bool
False VarBoundMap
intervals
scanHypothesis (FComp Comp
Lt E
e1 E
e2) Bool
True VarBoundMap
intervals =
F -> Bool -> VarBoundMap -> VarBoundMap
scanHypothesis (Comp -> E -> E -> F
FComp Comp
Ge E
e1 E
e2) Bool
False VarBoundMap
intervals
scanHypothesis (FComp Comp
Gt E
e1 E
e2) Bool
True VarBoundMap
intervals =
F -> Bool -> VarBoundMap -> VarBoundMap
scanHypothesis (Comp -> E -> E -> F
FComp Comp
Le E
e1 E
e2) Bool
False VarBoundMap
intervals
scanHypothesis (FComp Comp
Ge E
e1 E
e2) Bool
True VarBoundMap
intervals =
F -> Bool -> VarBoundMap -> VarBoundMap
scanHypothesis (Comp -> E -> E -> F
FComp Comp
Lt E
e1 E
e2) Bool
False VarBoundMap
intervals
scanHypothesis (FComp Comp
Le _e1 :: E
_e1@(Var VarName
v1) _e2 :: E
_e2@(Var VarName
v2)) Bool
False VarBoundMap
intervals =
VarName
-> (Maybe Rational, Maybe Rational) -> VarBoundMap -> VarBoundMap
forall k a. Ord k => k -> a -> Map k a -> Map k a
Map.insert VarName
v1 ((Maybe Rational, Maybe Rational)
-> (Maybe Rational, Maybe Rational)
-> (Maybe Rational, Maybe Rational)
forall a t t1.
CanMinMaxSameType a =>
(t, Maybe a) -> (t1, Maybe a) -> (t1, Maybe a)
updateUpper (Maybe Rational, Maybe Rational)
val2 (Maybe Rational, Maybe Rational)
val1) (VarBoundMap -> VarBoundMap) -> VarBoundMap -> VarBoundMap
forall a b. (a -> b) -> a -> b
$
VarName
-> (Maybe Rational, Maybe Rational) -> VarBoundMap -> VarBoundMap
forall k a. Ord k => k -> a -> Map k a -> Map k a
Map.insert VarName
v2 ((Maybe Rational, Maybe Rational)
-> (Maybe Rational, Maybe Rational)
-> (Maybe Rational, Maybe Rational)
forall a t t1.
CanMinMaxSameType a =>
(Maybe a, t) -> (Maybe a, t1) -> (Maybe a, t1)
updateLower (Maybe Rational, Maybe Rational)
val1 (Maybe Rational, Maybe Rational)
val2) (VarBoundMap -> VarBoundMap) -> VarBoundMap -> VarBoundMap
forall a b. (a -> b) -> a -> b
$
VarBoundMap
intervals
where
Just (Maybe Rational, Maybe Rational)
val1 = VarName -> VarBoundMap -> Maybe (Maybe Rational, Maybe Rational)
forall k a. Ord k => k -> Map k a -> Maybe a
Map.lookup VarName
v1 VarBoundMap
intervals
Just (Maybe Rational, Maybe Rational)
val2 = VarName -> VarBoundMap -> Maybe (Maybe Rational, Maybe Rational)
forall k a. Ord k => k -> Map k a -> Maybe a
Map.lookup VarName
v2 VarBoundMap
intervals
scanHypothesis (FComp Comp
Le (Var VarName
v) E
e) Bool
False VarBoundMap
intervals =
((Maybe Rational, Maybe Rational)
-> (Maybe Rational, Maybe Rational)
-> (Maybe Rational, Maybe Rational))
-> VarName
-> (Maybe Rational, Maybe Rational)
-> VarBoundMap
-> VarBoundMap
forall k a. Ord k => (a -> a -> a) -> k -> a -> Map k a -> Map k a
Map.insertWith (Maybe Rational, Maybe Rational)
-> (Maybe Rational, Maybe Rational)
-> (Maybe Rational, Maybe Rational)
forall a t t1.
CanMinMaxSameType a =>
(t, Maybe a) -> (t1, Maybe a) -> (t1, Maybe a)
updateUpper VarName
v (VarBoundMap -> E -> (Maybe Rational, Maybe Rational)
evalE_Rational VarBoundMap
intervals E
e) VarBoundMap
intervals
scanHypothesis (FComp Comp
Le E
e (Var VarName
v)) Bool
False VarBoundMap
intervals =
((Maybe Rational, Maybe Rational)
-> (Maybe Rational, Maybe Rational)
-> (Maybe Rational, Maybe Rational))
-> VarName
-> (Maybe Rational, Maybe Rational)
-> VarBoundMap
-> VarBoundMap
forall k a. Ord k => (a -> a -> a) -> k -> a -> Map k a -> Map k a
Map.insertWith (Maybe Rational, Maybe Rational)
-> (Maybe Rational, Maybe Rational)
-> (Maybe Rational, Maybe Rational)
forall a t t1.
CanMinMaxSameType a =>
(Maybe a, t) -> (Maybe a, t1) -> (Maybe a, t1)
updateLower VarName
v (VarBoundMap -> E -> (Maybe Rational, Maybe Rational)
evalE_Rational VarBoundMap
intervals E
e) VarBoundMap
intervals
scanHypothesis (FComp Comp
Le (EUnOp UnOp
Abs (Var VarName
v)) E
e) Bool
False VarBoundMap
intervals =
((Maybe Rational, Maybe Rational)
-> (Maybe Rational, Maybe Rational)
-> (Maybe Rational, Maybe Rational))
-> VarName
-> (Maybe Rational, Maybe Rational)
-> VarBoundMap
-> VarBoundMap
forall k a. Ord k => (a -> a -> a) -> k -> a -> Map k a -> Map k a
Map.insertWith (Maybe Rational, Maybe Rational)
-> (Maybe Rational, Maybe Rational)
-> (Maybe Rational, Maybe Rational)
forall a t t1.
CanMinMaxSameType a =>
(Maybe a, t) -> (Maybe a, t1) -> (Maybe a, t1)
updateLower VarName
v (Maybe Rational, Maybe Rational)
bounds (VarBoundMap -> VarBoundMap) -> VarBoundMap -> VarBoundMap
forall a b. (a -> b) -> a -> b
$ ((Maybe Rational, Maybe Rational)
-> (Maybe Rational, Maybe Rational)
-> (Maybe Rational, Maybe Rational))
-> VarName
-> (Maybe Rational, Maybe Rational)
-> VarBoundMap
-> VarBoundMap
forall k a. Ord k => (a -> a -> a) -> k -> a -> Map k a -> Map k a
Map.insertWith (Maybe Rational, Maybe Rational)
-> (Maybe Rational, Maybe Rational)
-> (Maybe Rational, Maybe Rational)
forall a t t1.
CanMinMaxSameType a =>
(t, Maybe a) -> (t1, Maybe a) -> (t1, Maybe a)
updateUpper VarName
v (Maybe Rational, Maybe Rational)
bounds VarBoundMap
intervals
where
(Maybe Rational
eValL, Maybe Rational
eValR) = VarBoundMap -> E -> (Maybe Rational, Maybe Rational)
evalE_Rational VarBoundMap
intervals E
e
bounds :: (Maybe Rational, Maybe Rational)
bounds = ((Rational -> Rational) -> Maybe Rational -> Maybe Rational
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap Rational -> Rational
forall t. CanNeg t => t -> NegType t
negate Maybe Rational
eValL, Maybe Rational
eValR)
scanHypothesis (FComp Comp
Lt E
e1 E
e2) Bool
False VarBoundMap
intervals = F -> Bool -> VarBoundMap -> VarBoundMap
scanHypothesis (Comp -> E -> E -> F
FComp Comp
Le E
e1 E
e2) Bool
False VarBoundMap
intervals
scanHypothesis (FComp Comp
Ge E
e1 E
e2) Bool
False VarBoundMap
intervals = F -> Bool -> VarBoundMap -> VarBoundMap
scanHypothesis (Comp -> E -> E -> F
FComp Comp
Le E
e2 E
e1) Bool
False VarBoundMap
intervals
scanHypothesis (FComp Comp
Gt E
e1 E
e2) Bool
False VarBoundMap
intervals = F -> Bool -> VarBoundMap -> VarBoundMap
scanHypothesis (Comp -> E -> E -> F
FComp Comp
Le E
e2 E
e1) Bool
False VarBoundMap
intervals
scanHypothesis F
_ Bool
_False VarBoundMap
intervals = VarBoundMap
intervals
evalF_comparisons :: VarBoundMap -> F -> F
evalF_comparisons :: VarBoundMap -> F -> F
evalF_comparisons VarBoundMap
intervals = F -> F
eC
where
eC :: F -> F
eC F
FTrue = F
FTrue
eC F
FFalse = F
FFalse
eC (FNot F
f) = F -> F
FNot (F -> F
eC F
f)
eC (FConn Conn
op F
f1 F
f2) = Conn -> F -> F -> F
FConn Conn
op (F -> F
eC F
f1) (F -> F
eC F
f2)
eC (FComp Comp
Gt E
e1 E
e2) = F -> F
eC (F -> F) -> F -> F
forall a b. (a -> b) -> a -> b
$ Comp -> E -> E -> F
FComp Comp
Lt E
e2 E
e1
eC (FComp Comp
Ge E
e1 E
e2) = F -> F
eC (F -> F) -> F -> F
forall a b. (a -> b) -> a -> b
$ Comp -> E -> E -> F
FComp Comp
Le E
e2 E
e1
eC (FComp Comp
Eq E
e1 E
e2) = F -> F
eC (F -> F) -> F -> F
forall a b. (a -> b) -> a -> b
$ Conn -> F -> F -> F
FConn Conn
And (Comp -> E -> E -> F
FComp Comp
Le E
e2 E
e1) (Comp -> E -> E -> F
FComp Comp
Le E
e1 E
e2)
eC f :: F
f@(FComp Comp
Le E
e1 E
e2) =
case (E -> (Maybe Rational, Maybe Rational)
eE E
e1, E -> (Maybe Rational, Maybe Rational)
eE E
e2) of
((Maybe Rational
_, Just Rational
e1R), (Just Rational
e2L, Maybe Rational
_)) | Rational
e1R Rational -> Rational -> OrderCompareType Rational Rational
forall a b.
HasOrderAsymmetric a b =>
a -> b -> OrderCompareType a b
<= Rational
e2L -> F
FTrue
((Just Rational
e1L, Maybe Rational
_), (Maybe Rational
_, Just Rational
e2R)) | Rational
e2R Rational -> Rational -> OrderCompareType Rational Rational
forall a b.
HasOrderAsymmetric a b =>
a -> b -> OrderCompareType a b
< Rational
e1L -> F
FFalse
((Maybe Rational, Maybe Rational),
(Maybe Rational, Maybe Rational))
_ -> F
f
eC f :: F
f@(FComp Comp
Lt E
e1 E
e2) =
case (E -> (Maybe Rational, Maybe Rational)
eE E
e1, E -> (Maybe Rational, Maybe Rational)
eE E
e2) of
((Maybe Rational
_, Just Rational
e1R), (Just Rational
e2L, Maybe Rational
_)) | Rational
e1R Rational -> Rational -> OrderCompareType Rational Rational
forall a b.
HasOrderAsymmetric a b =>
a -> b -> OrderCompareType a b
< Rational
e2L -> F
FTrue
((Just Rational
e1L, Maybe Rational
_), (Maybe Rational
_, Just Rational
e2R)) | Rational
e2R Rational -> Rational -> OrderCompareType Rational Rational
forall a b.
HasOrderAsymmetric a b =>
a -> b -> OrderCompareType a b
<= Rational
e1L -> F
FFalse
((Maybe Rational, Maybe Rational),
(Maybe Rational, Maybe Rational))
_ -> F
f
eE :: E -> (Maybe Rational, Maybe Rational)
eE = VarBoundMap -> E -> (Maybe Rational, Maybe Rational)
evalE_Rational VarBoundMap
intervals
evalE_Rational ::
VarBoundMap -> E -> (Maybe Rational, Maybe Rational)
evalE_Rational :: VarBoundMap -> E -> (Maybe Rational, Maybe Rational)
evalE_Rational VarBoundMap
intervals =
CN MPBall -> (Maybe Rational, Maybe Rational)
rationalBounds (CN MPBall -> (Maybe Rational, Maybe Rational))
-> (E -> CN MPBall) -> E -> (Maybe Rational, Maybe Rational)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Rational -> CN MPBall)
-> Map VarName (CN MPBall) -> Precision -> E -> CN MPBall
forall v.
(Ring v, CanDivSameType v, CanPowBy v Integer, CanMinMaxSameType v,
CanAbsSameType v, CanPowBy v v, CanSqrtSameType v,
CanSinCosSameType v, IsInterval v, HasDyadics v,
CanMinMaxSameType (IntervalEndpoint v),
CanDivIMod (NegType v) (NegType v),
ModType (NegType v) (NegType v) ~ NegType v,
NegType v ~ CN MPBall) =>
(Rational -> v) -> Map VarName v -> Precision -> E -> v
evalE (MPBall -> CN MPBall
forall v. v -> CN v
cn (MPBall -> CN MPBall)
-> (Rational -> MPBall) -> Rational -> CN MPBall
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Precision -> Rational -> MPBall
forall t. CanBeMPBallP t => Precision -> t -> MPBall
mpBallP Precision
p) Map VarName (CN MPBall)
intervalsMPBall Precision
p
where
intervalsMPBall :: Map VarName (CN MPBall)
intervalsMPBall = ((Maybe Rational, Maybe Rational) -> CN MPBall)
-> VarBoundMap -> Map VarName (CN MPBall)
forall a b k. (a -> b) -> Map k a -> Map k b
Map.map (Maybe Rational, Maybe Rational) -> CN MPBall
toMPBall VarBoundMap
intervals
toMPBall :: (Maybe Rational, Maybe Rational) -> CN MPBall
toMPBall :: (Maybe Rational, Maybe Rational) -> CN MPBall
toMPBall (Just Rational
l, Just Rational
r) = MPBall -> CN MPBall
forall v. v -> CN v
cn (MPBall -> CN MPBall) -> MPBall -> CN MPBall
forall a b. (a -> b) -> a -> b
$ (Precision -> Rational -> MPBall
forall t. CanBeMPBallP t => Precision -> t -> MPBall
mpBallP Precision
p Rational
l) MPBall -> MPBall -> MPBall
`hullMPBall` (Precision -> Rational -> MPBall
forall t. CanBeMPBallP t => Precision -> t -> MPBall
mpBallP Precision
p Rational
r)
toMPBall (Maybe Rational, Maybe Rational)
_ = NumError -> CN MPBall
forall v. NumError -> CN v
CN.noValueNumErrorCertain (NumError -> CN MPBall) -> NumError -> CN MPBall
forall a b. (a -> b) -> a -> b
$ VarName -> NumError
CN.NumError VarName
"no bounds"
p :: Precision
p = Integer -> Precision
prec Integer
60
rationalBounds :: CN MPBall -> (Maybe Rational, Maybe Rational)
rationalBounds :: CN MPBall -> (Maybe Rational, Maybe Rational)
rationalBounds CN MPBall
cnBall =
case CN MPBall -> Either NumErrors MPBall
forall es v. CanBeErrors es => CollectErrors es v -> Either es v
CN.toEither CN MPBall
cnBall of
Right MPBall
ball ->
let (MPFloat
l,MPFloat
r) = MPBall -> (IntervalEndpoint MPBall, IntervalEndpoint MPBall)
forall i.
IsInterval i =>
i -> (IntervalEndpoint i, IntervalEndpoint i)
endpoints MPBall
ball in
(Rational -> Maybe Rational
forall a. a -> Maybe a
Just (MPFloat -> Rational
forall t. CanBeRational t => t -> Rational
rational MPFloat
l), Rational -> Maybe Rational
forall a. a -> Maybe a
Just (MPFloat -> Rational
forall t. CanBeRational t => t -> Rational
rational MPFloat
r))
Either NumErrors MPBall
_ -> (Maybe Rational
forall a. Maybe a
Nothing, Maybe Rational
forall a. Maybe a
Nothing)
updateUpper ::
CanMinMaxSameType a =>
(t, Maybe a) -> (t1, Maybe a) -> (t1, Maybe a)
updateUpper :: forall a t t1.
CanMinMaxSameType a =>
(t, Maybe a) -> (t1, Maybe a) -> (t1, Maybe a)
updateUpper (t
_,Just a
u2) (t1
l, Just a
u1) = (t1
l, a -> Maybe a
forall a. a -> Maybe a
Just (a -> Maybe a) -> a -> Maybe a
forall a b. (a -> b) -> a -> b
$ a -> a -> MinMaxType a a
forall t1 t2.
CanMinMaxAsymmetric t1 t2 =>
t1 -> t2 -> MinMaxType t1 t2
min a
u1 a
u2)
updateUpper (t
_,Just a
u2) (t1
l, Maybe a
Nothing) = (t1
l, a -> Maybe a
forall a. a -> Maybe a
Just (a -> Maybe a) -> a -> Maybe a
forall a b. (a -> b) -> a -> b
$ a
u2)
updateUpper (t
_,Maybe a
Nothing) (t1
l, Just a
u1) = (t1
l, a -> Maybe a
forall a. a -> Maybe a
Just (a -> Maybe a) -> a -> Maybe a
forall a b. (a -> b) -> a -> b
$ a
u1)
updateUpper (t
_,Maybe a
Nothing) (t1
l, Maybe a
Nothing) = (t1
l, Maybe a
forall a. Maybe a
Nothing)
updateLower ::
CanMinMaxSameType a =>
(Maybe a, t) -> (Maybe a, t1) -> (Maybe a, t1)
updateLower :: forall a t t1.
CanMinMaxSameType a =>
(Maybe a, t) -> (Maybe a, t1) -> (Maybe a, t1)
updateLower (Just a
l2,t
_) (Just a
l1,t1
u) = (a -> Maybe a
forall a. a -> Maybe a
Just (a -> Maybe a) -> a -> Maybe a
forall a b. (a -> b) -> a -> b
$ a -> a -> MinMaxType a a
forall t1 t2.
CanMinMaxAsymmetric t1 t2 =>
t1 -> t2 -> MinMaxType t1 t2
max a
l1 a
l2, t1
u)
updateLower (Just a
l2,t
_) (Maybe a
Nothing,t1
u) = (a -> Maybe a
forall a. a -> Maybe a
Just (a -> Maybe a) -> a -> Maybe a
forall a b. (a -> b) -> a -> b
$ a
l2, t1
u)
updateLower (Maybe a
Nothing,t
_) (Just a
l1,t1
u) = (a -> Maybe a
forall a. a -> Maybe a
Just (a -> Maybe a) -> a -> Maybe a
forall a b. (a -> b) -> a -> b
$ a
l1, t1
u)
updateLower (Maybe a
Nothing,t
_) (Maybe a
Nothing,t1
u) = (Maybe a
forall a. Maybe a
Nothing, t1
u)
evalE ::
(Ring v, CanDivSameType v, CanPowBy v Integer,
CanMinMaxSameType v, CanAbsSameType v,
CanPowBy v v, CanSqrtSameType v, CanSinCosSameType v,
IsInterval v, CanAddThis v Integer, HasDyadics v, CanMinMaxSameType (IntervalEndpoint v), _
)
=>
(Rational -> v) ->
Map.Map VarName v -> Precision -> E -> v
evalE :: (Rational -> v) -> Map VarName v -> Precision -> E -> v
evalE Rational -> v
fromR (Map VarName v
varMap :: Map.Map VarName v) Precision
p = E -> v
evalVM
where
evalVM :: E -> v
evalVM :: E -> v
evalVM (EBinOp BinOp
op E
e1 E
e2) =
case BinOp
op of
BinOp
Min -> E -> v
evalVM E
e1 v -> v -> MinMaxType v v
forall t1 t2.
CanMinMaxAsymmetric t1 t2 =>
t1 -> t2 -> MinMaxType t1 t2
`min` E -> v
evalVM E
e2
BinOp
Max -> E -> v
evalVM E
e1 v -> v -> MinMaxType v v
forall t1 t2.
CanMinMaxAsymmetric t1 t2 =>
t1 -> t2 -> MinMaxType t1 t2
`max` E -> v
evalVM E
e2
BinOp
Add -> E -> v
evalVM E
e1 v -> v -> AddType v v
forall t1 t2. CanAddAsymmetric t1 t2 => t1 -> t2 -> AddType t1 t2
+ E -> v
evalVM E
e2
BinOp
Sub -> E -> v
evalVM E
e1 v -> v -> SubType v v
forall t1 t2. CanSub t1 t2 => t1 -> t2 -> SubType t1 t2
- E -> v
evalVM E
e2
BinOp
Mul -> E -> v
evalVM E
e1 v -> v -> MulType v v
forall t1 t2. CanMulAsymmetric t1 t2 => t1 -> t2 -> MulType t1 t2
* E -> v
evalVM E
e2
BinOp
Div -> E -> v
evalVM E
e1 v -> v -> DivType v v
forall t1 t2. CanDiv t1 t2 => t1 -> t2 -> DivType t1 t2
/ E -> v
evalVM E
e2
BinOp
Pow -> E -> v
evalVM E
e1 v -> v -> PowType v v
forall t1 t2. CanPow t1 t2 => t1 -> t2 -> PowType t1 t2
^ E -> v
evalVM E
e2
BinOp
Mod -> E -> v
evalVM E
e1 v -> v -> ModType v v
forall t1 t2. CanDivIMod t1 t2 => t1 -> t2 -> ModType t1 t2
`mod` E -> v
evalVM E
e2
evalVM (EUnOp UnOp
op E
e) =
case UnOp
op of
UnOp
Abs -> v -> AbsType v
forall t. CanAbs t => t -> AbsType t
abs (E -> v
evalVM E
e)
UnOp
Sqrt -> v -> SqrtType v
forall t. CanSqrt t => t -> SqrtType t
sqrt (E -> v
evalVM E
e)
UnOp
Negate -> v -> NegType v
forall t. CanNeg t => t -> NegType t
negate (E -> v
evalVM E
e)
UnOp
Sin -> v -> SinCosType v
forall t. CanSinCos t => t -> SinCosType t
sin (E -> v
evalVM E
e)
UnOp
Cos -> v -> SinCosType v
forall t. CanSinCos t => t -> SinCosType t
cos (E -> v
evalVM E
e)
evalVM (Var VarName
v) =
case VarName -> Map VarName v -> Maybe v
forall k a. Ord k => k -> Map k a -> Maybe a
Map.lookup VarName
v Map VarName v
varMap of
Maybe v
Nothing ->
VarName -> v
forall a. HasCallStack => VarName -> a
error (VarName
"evalE: varMap does not contain variable " VarName -> VarName -> VarName
forall a. [a] -> [a] -> [a]
++ VarName -> VarName
forall a. Show a => a -> VarName
show VarName
v)
Just v
r -> v
r
evalVM E
Pi = MPBall -> CN MPBall
forall v. v -> CN v
cn (Precision -> MPBall
piBallP Precision
p)
evalVM (Lit Rational
i) = (Rational -> v
fromR Rational
i)
evalVM (PowI E
e Integer
i) = E -> v
evalVM E
e v -> Integer -> PowType v Integer
forall t1 t2. CanPow t1 t2 => t1 -> t2 -> PowType t1 t2
^ Integer
i
evalVM (Float32 RoundingMode
_ E
e) = (v
onePlusMinusEpsilon v -> v -> MulType v v
forall t1 t2. CanMulAsymmetric t1 t2 => t1 -> t2 -> MulType t1 t2
* (E -> v
evalVM E
e)) NegType v -> v -> AddType (NegType v) v
forall t1 t2. CanAddAsymmetric t1 t2 => t1 -> t2 -> AddType t1 t2
+ v
zeroPlusMinusEpsilon
where
eps :: v
eps :: v
eps = Dyadic -> v
forall t1 t2. ConvertibleExactly t1 t2 => t1 -> t2
convertExactly (Dyadic -> v) -> Dyadic -> v
forall a b. (a -> b) -> a -> b
$ Rational -> Dyadic
forall t. CanBeDyadic t => t -> Dyadic
dyadic (Rational -> Dyadic) -> Rational -> Dyadic
forall a b. (a -> b) -> a -> b
$ Rational
0.5Rational -> Integer -> PowType Rational Integer
forall t1 t2. CanPow t1 t2 => t1 -> t2 -> PowType t1 t2
^Integer
23
onePlusMinusEpsilon :: v
onePlusMinusEpsilon :: v
onePlusMinusEpsilon = v -> v -> v
forall i.
(IsInterval i, CanMinMaxSameType (IntervalEndpoint i)) =>
i -> i -> i
fromEndpointsAsIntervals (Integer
1 Integer -> NegType v -> AddType Integer (NegType v)
forall t1 t2. CanAddAsymmetric t1 t2 => t1 -> t2 -> AddType t1 t2
+ (-v
eps)) (Integer
1 Integer -> v -> AddType Integer v
forall t1 t2. CanAddAsymmetric t1 t2 => t1 -> t2 -> AddType t1 t2
+ v
eps)
epsD :: v
epsD :: v
epsD = Dyadic -> v
forall t1 t2. ConvertibleExactly t1 t2 => t1 -> t2
convertExactly (Dyadic -> v) -> Dyadic -> v
forall a b. (a -> b) -> a -> b
$ Rational -> Dyadic
forall t. CanBeDyadic t => t -> Dyadic
dyadic (Rational -> Dyadic) -> Rational -> Dyadic
forall a b. (a -> b) -> a -> b
$ Rational
0.5Rational -> Integer -> PowType Rational Integer
forall t1 t2. CanPow t1 t2 => t1 -> t2 -> PowType t1 t2
^Integer
149
zeroPlusMinusEpsilon :: v
zeroPlusMinusEpsilon :: v
zeroPlusMinusEpsilon = v -> v -> v
forall i.
(IsInterval i, CanMinMaxSameType (IntervalEndpoint i)) =>
i -> i -> i
fromEndpointsAsIntervals (-v
epsD) v
epsD
evalVM (Float64 RoundingMode
_ E
e) = (v
onePlusMinusEpsilon v -> v -> MulType v v
forall t1 t2. CanMulAsymmetric t1 t2 => t1 -> t2 -> MulType t1 t2
* (E -> v
evalVM E
e)) NegType v -> v -> AddType (NegType v) v
forall t1 t2. CanAddAsymmetric t1 t2 => t1 -> t2 -> AddType t1 t2
+ v
zeroPlusMinusEpsilon
where
eps :: v
eps :: v
eps = Dyadic -> v
forall t1 t2. ConvertibleExactly t1 t2 => t1 -> t2
convertExactly (Dyadic -> v) -> Dyadic -> v
forall a b. (a -> b) -> a -> b
$ Rational -> Dyadic
forall t. CanBeDyadic t => t -> Dyadic
dyadic (Rational -> Dyadic) -> Rational -> Dyadic
forall a b. (a -> b) -> a -> b
$ Rational
0.5Rational -> Integer -> PowType Rational Integer
forall t1 t2. CanPow t1 t2 => t1 -> t2 -> PowType t1 t2
^Integer
52
onePlusMinusEpsilon :: v
onePlusMinusEpsilon :: v
onePlusMinusEpsilon = v -> v -> v
forall i.
(IsInterval i, CanMinMaxSameType (IntervalEndpoint i)) =>
i -> i -> i
fromEndpointsAsIntervals (Integer
1 Integer -> NegType v -> AddType Integer (NegType v)
forall t1 t2. CanAddAsymmetric t1 t2 => t1 -> t2 -> AddType t1 t2
+ (-v
eps)) (Integer
1 Integer -> v -> AddType Integer v
forall t1 t2. CanAddAsymmetric t1 t2 => t1 -> t2 -> AddType t1 t2
+ v
eps)
epsD :: v
epsD :: v
epsD = Dyadic -> v
forall t1 t2. ConvertibleExactly t1 t2 => t1 -> t2
convertExactly (Dyadic -> v) -> Dyadic -> v
forall a b. (a -> b) -> a -> b
$ Rational -> Dyadic
forall t. CanBeDyadic t => t -> Dyadic
dyadic (Rational -> Dyadic) -> Rational -> Dyadic
forall a b. (a -> b) -> a -> b
$ Rational
0.5Rational -> Integer -> PowType Rational Integer
forall t1 t2. CanPow t1 t2 => t1 -> t2 -> PowType t1 t2
^Integer
1074
zeroPlusMinusEpsilon :: v
zeroPlusMinusEpsilon :: v
zeroPlusMinusEpsilon = v -> v -> v
forall i.
(IsInterval i, CanMinMaxSameType (IntervalEndpoint i)) =>
i -> i -> i
fromEndpointsAsIntervals (-v
epsD) v
epsD
evalVM (RoundToInteger RoundingMode
mode E
e) = (MPBall -> MPBall) -> CN MPBall -> CN MPBall
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (RoundingMode -> MPBall -> MPBall
forall i p.
(Real (IntervalEndpoint i), IsInterval i, IsInterval p,
ConvertibleExactly Integer (IntervalEndpoint p)) =>
RoundingMode -> i -> p
roundMPBall RoundingMode
mode) (E -> v
evalVM E
e)
evalVM E
e = VarName -> v
forall a. HasCallStack => VarName -> a
error (VarName -> v) -> VarName -> v
forall a b. (a -> b) -> a -> b
$ VarName
"evalE: undefined for: " VarName -> VarName -> VarName
forall a. [a] -> [a] -> [a]
++ E -> VarName
forall a. Show a => a -> VarName
show E
e
roundMPBall :: (Real (IntervalEndpoint i), IsInterval i, IsInterval p,
ConvertibleExactly Integer (IntervalEndpoint p)) =>
RoundingMode -> i -> p
roundMPBall :: forall i p.
(Real (IntervalEndpoint i), IsInterval i, IsInterval p,
ConvertibleExactly Integer (IntervalEndpoint p)) =>
RoundingMode -> i -> p
roundMPBall RoundingMode
mode i
i =
let
(IntervalEndpoint i
l', IntervalEndpoint i
r') = i -> (IntervalEndpoint i, IntervalEndpoint i)
forall i.
IsInterval i =>
i -> (IntervalEndpoint i, IntervalEndpoint i)
endpoints i
i
l :: Rational
l = IntervalEndpoint i -> Rational
forall a. Real a => a -> Rational
toRational IntervalEndpoint i
l'
r :: Rational
r = IntervalEndpoint i -> Rational
forall a. Real a => a -> Rational
toRational IntervalEndpoint i
r'
lFloor :: RoundType Rational
lFloor = Rational -> RoundType Rational
forall t. CanRound t => t -> RoundType t
floor Rational
l
lCeil :: RoundType Rational
lCeil = Rational -> RoundType Rational
forall t. CanRound t => t -> RoundType t
ceiling Rational
l
rFloor :: RoundType Rational
rFloor = Rational -> RoundType Rational
forall t. CanRound t => t -> RoundType t
floor Rational
r
rCeil :: RoundType Rational
rCeil = Rational -> RoundType Rational
forall t. CanRound t => t -> RoundType t
ceiling Rational
r
in case RoundingMode
mode of
RoundingMode
RNE ->
IntervalEndpoint p -> IntervalEndpoint p -> p
forall i.
IsInterval i =>
IntervalEndpoint i -> IntervalEndpoint i -> i
fromEndpoints
(if Rational
l Rational -> Integer -> SubType Rational Integer
forall t1 t2. CanSub t1 t2 => t1 -> t2 -> SubType t1 t2
- Integer
RoundType Rational
lFloor Rational -> Rational -> EqCompareType Rational Rational
forall a b. HasEqAsymmetric a b => a -> b -> EqCompareType a b
== Rational
0.5
then (if Integer -> Bool
forall a. Integral a => a -> Bool
even Integer
RoundType Rational
lFloor then Integer -> IntervalEndpoint p
forall t1 t2. ConvertibleExactly t1 t2 => t1 -> t2
convertExactly Integer
RoundType Rational
lFloor else Integer -> IntervalEndpoint p
forall t1 t2. ConvertibleExactly t1 t2 => t1 -> t2
convertExactly Integer
RoundType Rational
lCeil)
else (if Rational
l Rational -> Integer -> SubType Rational Integer
forall t1 t2. CanSub t1 t2 => t1 -> t2 -> SubType t1 t2
- Integer
RoundType Rational
lFloor Rational -> Rational -> OrderCompareType Rational Rational
forall a b.
HasOrderAsymmetric a b =>
a -> b -> OrderCompareType a b
< Rational
0.5 then Integer -> IntervalEndpoint p
forall t1 t2. ConvertibleExactly t1 t2 => t1 -> t2
convertExactly Integer
RoundType Rational
lFloor else Integer -> IntervalEndpoint p
forall t1 t2. ConvertibleExactly t1 t2 => t1 -> t2
convertExactly Integer
RoundType Rational
lCeil))
(if Rational
r Rational -> Integer -> SubType Rational Integer
forall t1 t2. CanSub t1 t2 => t1 -> t2 -> SubType t1 t2
- Integer
RoundType Rational
rFloor Rational -> Rational -> EqCompareType Rational Rational
forall a b. HasEqAsymmetric a b => a -> b -> EqCompareType a b
== Rational
0.5
then (if Integer -> Bool
forall a. Integral a => a -> Bool
even Integer
RoundType Rational
rFloor then Integer -> IntervalEndpoint p
forall t1 t2. ConvertibleExactly t1 t2 => t1 -> t2
convertExactly Integer
RoundType Rational
rFloor else Integer -> IntervalEndpoint p
forall t1 t2. ConvertibleExactly t1 t2 => t1 -> t2
convertExactly Integer
RoundType Rational
rCeil)
else (if Rational
r Rational -> Integer -> SubType Rational Integer
forall t1 t2. CanSub t1 t2 => t1 -> t2 -> SubType t1 t2
- Integer
RoundType Rational
rFloor Rational -> Rational -> OrderCompareType Rational Rational
forall a b.
HasOrderAsymmetric a b =>
a -> b -> OrderCompareType a b
< Rational
0.5 then Integer -> IntervalEndpoint p
forall t1 t2. ConvertibleExactly t1 t2 => t1 -> t2
convertExactly Integer
RoundType Rational
rFloor else Integer -> IntervalEndpoint p
forall t1 t2. ConvertibleExactly t1 t2 => t1 -> t2
convertExactly Integer
RoundType Rational
rCeil))
RoundingMode
RTP -> IntervalEndpoint p -> IntervalEndpoint p -> p
forall i.
IsInterval i =>
IntervalEndpoint i -> IntervalEndpoint i -> i
fromEndpoints (Integer -> IntervalEndpoint p
forall t1 t2. ConvertibleExactly t1 t2 => t1 -> t2
convertExactly Integer
RoundType Rational
lCeil) (Integer -> IntervalEndpoint p
forall t1 t2. ConvertibleExactly t1 t2 => t1 -> t2
convertExactly Integer
RoundType Rational
rCeil)
RoundingMode
RTN -> IntervalEndpoint p -> IntervalEndpoint p -> p
forall i.
IsInterval i =>
IntervalEndpoint i -> IntervalEndpoint i -> i
fromEndpoints (Integer -> IntervalEndpoint p
forall t1 t2. ConvertibleExactly t1 t2 => t1 -> t2
convertExactly Integer
RoundType Rational
lFloor) (Integer -> IntervalEndpoint p
forall t1 t2. ConvertibleExactly t1 t2 => t1 -> t2
convertExactly Integer
RoundType Rational
rFloor)
RoundingMode
RTZ ->
IntervalEndpoint p -> IntervalEndpoint p -> p
forall i.
IsInterval i =>
IntervalEndpoint i -> IntervalEndpoint i -> i
fromEndpoints
(if Rational -> Bool
forall t. CanTestPosNeg t => t -> Bool
isCertainlyPositive Rational
l then Integer -> IntervalEndpoint p
forall t1 t2. ConvertibleExactly t1 t2 => t1 -> t2
convertExactly Integer
RoundType Rational
lFloor else Integer -> IntervalEndpoint p
forall t1 t2. ConvertibleExactly t1 t2 => t1 -> t2
convertExactly Integer
RoundType Rational
lCeil)
(if Rational -> Bool
forall t. CanTestPosNeg t => t -> Bool
isCertainlyPositive Rational
r then Integer -> IntervalEndpoint p
forall t1 t2. ConvertibleExactly t1 t2 => t1 -> t2
convertExactly Integer
RoundType Rational
rFloor else Integer -> IntervalEndpoint p
forall t1 t2. ConvertibleExactly t1 t2 => t1 -> t2
convertExactly Integer
RoundType Rational
rCeil)
RoundingMode
RNA ->
IntervalEndpoint p -> IntervalEndpoint p -> p
forall i.
IsInterval i =>
IntervalEndpoint i -> IntervalEndpoint i -> i
fromEndpoints
(if Rational
l Rational -> Integer -> SubType Rational Integer
forall t1 t2. CanSub t1 t2 => t1 -> t2 -> SubType t1 t2
- Integer
RoundType Rational
lFloor Rational -> Rational -> EqCompareType Rational Rational
forall a b. HasEqAsymmetric a b => a -> b -> EqCompareType a b
== Rational
0.5
then (if Rational -> Bool
forall t. CanTestPosNeg t => t -> Bool
isCertainlyPositive Rational
l then Integer -> IntervalEndpoint p
forall t1 t2. ConvertibleExactly t1 t2 => t1 -> t2
convertExactly Integer
RoundType Rational
lCeil else Integer -> IntervalEndpoint p
forall t1 t2. ConvertibleExactly t1 t2 => t1 -> t2
convertExactly Integer
RoundType Rational
lFloor)
else (if Rational
l Rational -> Integer -> SubType Rational Integer
forall t1 t2. CanSub t1 t2 => t1 -> t2 -> SubType t1 t2
- Integer
RoundType Rational
lFloor Rational -> Rational -> OrderCompareType Rational Rational
forall a b.
HasOrderAsymmetric a b =>
a -> b -> OrderCompareType a b
< Rational
0.5 then Integer -> IntervalEndpoint p
forall t1 t2. ConvertibleExactly t1 t2 => t1 -> t2
convertExactly Integer
RoundType Rational
lFloor else Integer -> IntervalEndpoint p
forall t1 t2. ConvertibleExactly t1 t2 => t1 -> t2
convertExactly Integer
RoundType Rational
lCeil))
(if Rational
r Rational -> Integer -> SubType Rational Integer
forall t1 t2. CanSub t1 t2 => t1 -> t2 -> SubType t1 t2
- Integer
RoundType Rational
rFloor Rational -> Rational -> EqCompareType Rational Rational
forall a b. HasEqAsymmetric a b => a -> b -> EqCompareType a b
== Rational
0.5
then (if Rational -> Bool
forall t. CanTestPosNeg t => t -> Bool
isCertainlyPositive Rational
r then Integer -> IntervalEndpoint p
forall t1 t2. ConvertibleExactly t1 t2 => t1 -> t2
convertExactly Integer
RoundType Rational
rCeil else Integer -> IntervalEndpoint p
forall t1 t2. ConvertibleExactly t1 t2 => t1 -> t2
convertExactly Integer
RoundType Rational
rFloor)
else (if Rational
r Rational -> Integer -> SubType Rational Integer
forall t1 t2. CanSub t1 t2 => t1 -> t2 -> SubType t1 t2
- Integer
RoundType Rational
rFloor Rational -> Rational -> OrderCompareType Rational Rational
forall a b.
HasOrderAsymmetric a b =>
a -> b -> OrderCompareType a b
< Rational
0.5 then Integer -> IntervalEndpoint p
forall t1 t2. ConvertibleExactly t1 t2 => t1 -> t2
convertExactly Integer
RoundType Rational
rFloor else Integer -> IntervalEndpoint p
forall t1 t2. ConvertibleExactly t1 t2 => t1 -> t2
convertExactly Integer
RoundType Rational
rCeil))
checkFWithEval :: F -> VarBoundMap -> Maybe Bool
checkFWithEval :: F -> VarBoundMap -> Maybe Bool
checkFWithEval F
f' VarBoundMap
varBoundMap = F -> Maybe Bool
aux F
f'
where
aux :: F -> Maybe Bool
aux (FComp Comp
op E
e1 E
e2) =
case (Maybe Rational
mE1L, Maybe Rational
mE1R, Maybe Rational
mE2L, Maybe Rational
mE2R) of
(Just Rational
e1L, Just Rational
e1R, Just Rational
e2L, Just Rational
e2R) -> Comp -> (Rational, Rational) -> (Rational, Rational) -> Maybe Bool
forall {a} {b}.
(HasOrderAsymmetric a b, OrderCompareType a b ~ Bool) =>
Comp -> (b, a) -> (b, a) -> Maybe Bool
decideKleenean Comp
op (Rational
e1L, Rational
e1R) (Rational
e2L, Rational
e2R)
(Maybe Rational
_, Maybe Rational
_, Maybe Rational
_, Maybe Rational
_) -> Maybe Bool
forall a. Maybe a
Nothing
where
(Maybe Rational
mE1L, Maybe Rational
mE1R) = VarBoundMap -> E -> (Maybe Rational, Maybe Rational)
evalE_Rational VarBoundMap
varBoundMap E
e1
(Maybe Rational
mE2L, Maybe Rational
mE2R) = VarBoundMap -> E -> (Maybe Rational, Maybe Rational)
evalE_Rational VarBoundMap
varBoundMap E
e2
decideKleenean :: Comp -> (b, a) -> (b, a) -> Maybe Bool
decideKleenean Comp
Lt (b
l1, a
r1) (b
l2, a
r2)
| a
r1 a -> b -> OrderCompareType a b
forall a b.
HasOrderAsymmetric a b =>
a -> b -> OrderCompareType a b
< b
l2 = Bool -> Maybe Bool
forall a. a -> Maybe a
Just Bool
True
| a
r2 a -> b -> OrderCompareType a b
forall a b.
HasOrderAsymmetric a b =>
a -> b -> OrderCompareType a b
<= b
l1 = Bool -> Maybe Bool
forall a. a -> Maybe a
Just Bool
False
| Bool
otherwise = Maybe Bool
forall a. Maybe a
Nothing
decideKleenean Comp
Le (b
l1, a
r1) (b
l2, a
r2)
| a
r1 a -> b -> OrderCompareType a b
forall a b.
HasOrderAsymmetric a b =>
a -> b -> OrderCompareType a b
<= b
l2 = Bool -> Maybe Bool
forall a. a -> Maybe a
Just Bool
True
| a
r2 a -> b -> OrderCompareType a b
forall a b.
HasOrderAsymmetric a b =>
a -> b -> OrderCompareType a b
< b
l1 = Bool -> Maybe Bool
forall a. a -> Maybe a
Just Bool
False
| Bool
otherwise = Maybe Bool
forall a. Maybe a
Nothing
decideKleenean Comp
Ge (b, a)
x (b, a)
y = Comp -> (b, a) -> (b, a) -> Maybe Bool
decideKleenean Comp
Le (b, a)
y (b, a)
x
decideKleenean Comp
Gt (b, a)
x (b, a)
y = Comp -> (b, a) -> (b, a) -> Maybe Bool
decideKleenean Comp
Lt (b, a)
y (b, a)
x
decideKleenean Comp
Eq (b, a)
x (b, a)
y =
case Comp -> (b, a) -> (b, a) -> Maybe Bool
decideKleenean Comp
Ge (b, a)
y (b, a)
x of
Just Bool
False -> Bool -> Maybe Bool
forall a. a -> Maybe a
Just Bool
False
Just Bool
True -> Comp -> (b, a) -> (b, a) -> Maybe Bool
decideKleenean Comp
Le (b, a)
y (b, a)
x
Maybe Bool
Nothing ->
case Comp -> (b, a) -> (b, a) -> Maybe Bool
decideKleenean Comp
Le (b, a)
y (b, a)
x of
Just Bool
False -> Bool -> Maybe Bool
forall a. a -> Maybe a
Just Bool
False
Maybe Bool
_ -> Maybe Bool
forall a. Maybe a
Nothing
aux (FConn Conn
op F
f1 F
f2) =
case Conn
op of
Conn
And ->
case (Maybe Bool
f1Val, Maybe Bool
f2Val) of
(Just Bool
r1, Just Bool
r2) -> Bool -> Maybe Bool
forall a. a -> Maybe a
Just (Bool -> Maybe Bool) -> Bool -> Maybe Bool
forall a b. (a -> b) -> a -> b
$ Bool
r1 Bool -> Bool -> AndOrType Bool Bool
forall a b. CanAndOrAsymmetric a b => a -> b -> AndOrType a b
&& Bool
r2
(Maybe Bool
_, Maybe Bool
_) -> Maybe Bool
forall a. Maybe a
Nothing
Conn
Or ->
case (Maybe Bool
f1Val, Maybe Bool
f2Val) of
(Just Bool
r1, Just Bool
r2) -> Bool -> Maybe Bool
forall a. a -> Maybe a
Just (Bool -> Maybe Bool) -> Bool -> Maybe Bool
forall a b. (a -> b) -> a -> b
$ Bool
r1 Bool -> Bool -> AndOrType Bool Bool
forall a b. CanAndOrAsymmetric a b => a -> b -> AndOrType a b
|| Bool
r2
(Maybe Bool
_, Maybe Bool
_) -> Maybe Bool
forall a. Maybe a
Nothing
Conn
Impl ->
case (Maybe Bool
f1Val, Maybe Bool
f2Val) of
(Just Bool
r1, Just Bool
r2) -> Bool -> Maybe Bool
forall a. a -> Maybe a
Just (Bool -> Maybe Bool) -> Bool -> Maybe Bool
forall a b. (a -> b) -> a -> b
$ Bool -> NegType Bool
forall t. CanNeg t => t -> NegType t
not Bool
r1 Bool -> Bool -> AndOrType Bool Bool
forall a b. CanAndOrAsymmetric a b => a -> b -> AndOrType a b
|| Bool
r2
(Maybe Bool
_, Maybe Bool
_) -> Maybe Bool
forall a. Maybe a
Nothing
where
f1Val :: Maybe Bool
f1Val = F -> Maybe Bool
aux F
f1
f2Val :: Maybe Bool
f2Val = F -> Maybe Bool
aux F
f2
aux (FNot F
f) = Bool -> Bool
forall t. CanNeg t => t -> NegType t
not (Bool -> Bool) -> Maybe Bool -> Maybe Bool
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> F -> Maybe Bool
aux F
f
aux F
FTrue = Bool -> Maybe Bool
forall a. a -> Maybe a
Just Bool
True
aux F
FFalse = Bool -> Maybe Bool
forall a. a -> Maybe a
Just Bool
False