{-# LANGUAGE PartialTypeSignatures #-}
{-# OPTIONS_GHC -Wno-partial-type-signatures #-}
{-# OPTIONS_GHC -Wno-unrecognised-pragmas #-}
{-# HLINT ignore "Use camelCase" #-}
{-|
    Module      :  PropaFP.DeriveBounds
    Description :  Deriving ranges for variables from hypotheses inside a formula
    Copyright   :  (c) Michal Konecny 2013, 2021
    License     :  BSD3

    Maintainer  :  mikkonecny@gmail.com
    Stability   :  experimental
    Portability :  portable

    Deriving ranges for variables from hypotheses inside a formula
-}
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 qualified Data.Bifunctor as Bifunctor

import AERN2.MP.Ball
import AERN2.MP.Dyadic

import PropaFP.Expression
import PropaFP.VarMap

import Debug.Trace (trace)
import Data.List

-- examples:


_f1 :: F -- eliminates "x"

_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 -- underivable "x"

_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 -- nested implication containing bound on "x" guarded by a condition on "n"

_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 -- two opposing implications which contain the same bound on "x"

_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
    -- undo implies false on 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 -- Make the given form imply false for derivation of bounds

    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)
              -- simplify where possible with the knowledge we are restricted to box b

              -- avoid simplifying form2 -> false, only simplify form2

        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 ())
              -- remove variables that do not appear in f2

        b2 :: VarBoundMap
b2 = F -> VarBoundMap -> VarBoundMap
scanHypotheses F
f2 VarBoundMap
b'
              -- attempt to improve the bounds on the variables


type VarBoundMap = Map.Map VarName (Maybe Rational, Maybe Rational)

-- TODO: Could refactor this to remove need of form -> false

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 f@(FConn And h1@(FConn Impl cond1 branch1) h2@(FConn Impl cond2 branch2)) False intervals 

--   =

--   trace (show f) $

--   trace (show intervals) $

--   trace (show (checkFWithEval cond1 intervals)) $

--   trace (show (checkFWithEval cond2 intervals)) $

--   -- doesn't work because cond1/2 is indeterminate most of the time

--   case checkFWithEval cond1 intervals of

--     Nothing -> (scanHypothesis h1 False . scanHypothesis h2 False) intervals

--     result1 -> 

--       case checkFWithEval cond2 intervals of

--         Nothing -> (scanHypothesis h1 False . scanHypothesis h2 False) intervals

--         result2 ->

--           if result1 P./= result2

--             then scanHypothesis (FConn Or branch1 branch2) False intervals

--             else (scanHypothesis h1 False . scanHypothesis h2 False) 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)

      -- mergeWorse (l1,r1) (l2,r2) = 

      --   case (l1, r1, l2, r2) of

      --     (Nothing, Nothing, Just _, Just _) -> (l2, r2) -- FIXME: hack, should only do this if variable of interest only exists in one branch

      --     (Just _, Just _, Nothing, Nothing) -> (l1, r1) -- FIXME: hack, should only do this if variable of interest only exists in one branch

      --     _ -> (min <$> l1 <*> l2, max <$> r1 <*> 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
      -- iterateUntilNoChange b1 f

      --   | b1 P.== b2 = b1

      --   | otherwise = scanHypothesis f isNegated 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
-- We need: data Comp = Gt | Ge | Lt | Le | Eq

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

-- Deal with negated inequalites

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
-- Bounds for absolute values of Vars

scanHypothesis (FComp Comp
Le (EUnOp UnOp
Abs (Var VarName
v)) E
e) Bool
False VarBoundMap
intervals =
  -- trace (show bounds)

    ((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)
-- reduce Le, Geq, Ge on equivalent Leq (note that we treat strict and non-strict the same way):

-- Fixme: Some way to treat strict/non-strict with integer variables differently

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

{-|
  Replace within a formula some comparisons with FTrue/FFalse, namely
  those comparisons that on the given box can be easily seen to be true/false.
  -}
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
-- x is inconsistent

-- since we have exists x in empty set

-- x > y is False 

-- we use exists instead of forall because we're looking for a model for x


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) --FIXME: deal with contradictions, inconsistent intervals, directly

  -- If we have an overlapping interval, turn conjunction into False

  -- l = 1, r = 0

  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 -- Needs to be at least 54 for turning double pi from Why3 into real pi FIXME: behaviour with very high prec (say prec 1000)?

  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)
--updateUpper _ _ = error "DeriveBounds: updateUpper failed"


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)
--updateLower _ _ = error "DeriveBounds: updateLower failed"


-- | compute the value of E with Vars at specified points

-- | (a generalised version of computeE)

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) -- FIXME: check isCertainNegative?

              (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) -- FIXME: check isCertainNegative?

                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 = --TODO: Use guards here

          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