{-# LANGUAGE LambdaCase #-}
{-# LANGUAGE LambdaCase #-}
module PropaFP.Expression where
import MixedTypesNumPrelude
import qualified Prelude as P
import qualified Data.Map as Map
import Data.List (nub, delete)
import Test.QuickCheck
import Debug.Trace (trace)
import Test.QuickCheck.State (State(randomSeed))
import Data.Ratio
import PropaFP.VarMap
import AERN2.Normalize (CanNormalize(normalize))
data BinOp = Add | Sub | Mul | Div | Min | Max | Pow | Mod
deriving (Int -> BinOp -> ShowS
[BinOp] -> ShowS
BinOp -> String
(Int -> BinOp -> ShowS)
-> (BinOp -> String) -> ([BinOp] -> ShowS) -> Show BinOp
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [BinOp] -> ShowS
$cshowList :: [BinOp] -> ShowS
show :: BinOp -> String
$cshow :: BinOp -> String
showsPrec :: Int -> BinOp -> ShowS
$cshowsPrec :: Int -> BinOp -> ShowS
Show, BinOp -> BinOp -> Bool
(BinOp -> BinOp -> Bool) -> (BinOp -> BinOp -> Bool) -> Eq BinOp
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: BinOp -> BinOp -> Bool
$c/= :: BinOp -> BinOp -> Bool
== :: BinOp -> BinOp -> Bool
$c== :: BinOp -> BinOp -> Bool
P.Eq, Eq BinOp
Eq BinOp
-> (BinOp -> BinOp -> Ordering)
-> (BinOp -> BinOp -> Bool)
-> (BinOp -> BinOp -> Bool)
-> (BinOp -> BinOp -> Bool)
-> (BinOp -> BinOp -> Bool)
-> (BinOp -> BinOp -> BinOp)
-> (BinOp -> BinOp -> BinOp)
-> Ord BinOp
BinOp -> BinOp -> Bool
BinOp -> BinOp -> Ordering
BinOp -> BinOp -> BinOp
forall a.
Eq a
-> (a -> a -> Ordering)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> a)
-> (a -> a -> a)
-> Ord a
min :: BinOp -> BinOp -> BinOp
$cmin :: BinOp -> BinOp -> BinOp
max :: BinOp -> BinOp -> BinOp
$cmax :: BinOp -> BinOp -> BinOp
>= :: BinOp -> BinOp -> Bool
$c>= :: BinOp -> BinOp -> Bool
> :: BinOp -> BinOp -> Bool
$c> :: BinOp -> BinOp -> Bool
<= :: BinOp -> BinOp -> Bool
$c<= :: BinOp -> BinOp -> Bool
< :: BinOp -> BinOp -> Bool
$c< :: BinOp -> BinOp -> Bool
compare :: BinOp -> BinOp -> Ordering
$ccompare :: BinOp -> BinOp -> Ordering
P.Ord)
data UnOp = Sqrt | Negate | Abs | Sin | Cos
deriving (Int -> UnOp -> ShowS
[UnOp] -> ShowS
UnOp -> String
(Int -> UnOp -> ShowS)
-> (UnOp -> String) -> ([UnOp] -> ShowS) -> Show UnOp
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [UnOp] -> ShowS
$cshowList :: [UnOp] -> ShowS
show :: UnOp -> String
$cshow :: UnOp -> String
showsPrec :: Int -> UnOp -> ShowS
$cshowsPrec :: Int -> UnOp -> ShowS
Show, UnOp -> UnOp -> Bool
(UnOp -> UnOp -> Bool) -> (UnOp -> UnOp -> Bool) -> Eq UnOp
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: UnOp -> UnOp -> Bool
$c/= :: UnOp -> UnOp -> Bool
== :: UnOp -> UnOp -> Bool
$c== :: UnOp -> UnOp -> Bool
P.Eq, Eq UnOp
Eq UnOp
-> (UnOp -> UnOp -> Ordering)
-> (UnOp -> UnOp -> Bool)
-> (UnOp -> UnOp -> Bool)
-> (UnOp -> UnOp -> Bool)
-> (UnOp -> UnOp -> Bool)
-> (UnOp -> UnOp -> UnOp)
-> (UnOp -> UnOp -> UnOp)
-> Ord UnOp
UnOp -> UnOp -> Bool
UnOp -> UnOp -> Ordering
UnOp -> UnOp -> UnOp
forall a.
Eq a
-> (a -> a -> Ordering)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> a)
-> (a -> a -> a)
-> Ord a
min :: UnOp -> UnOp -> UnOp
$cmin :: UnOp -> UnOp -> UnOp
max :: UnOp -> UnOp -> UnOp
$cmax :: UnOp -> UnOp -> UnOp
>= :: UnOp -> UnOp -> Bool
$c>= :: UnOp -> UnOp -> Bool
> :: UnOp -> UnOp -> Bool
$c> :: UnOp -> UnOp -> Bool
<= :: UnOp -> UnOp -> Bool
$c<= :: UnOp -> UnOp -> Bool
< :: UnOp -> UnOp -> Bool
$c< :: UnOp -> UnOp -> Bool
compare :: UnOp -> UnOp -> Ordering
$ccompare :: UnOp -> UnOp -> Ordering
P.Ord)
data RoundingMode = RNE | RTP | RTN | RTZ | RNA deriving (Int -> RoundingMode -> ShowS
[RoundingMode] -> ShowS
RoundingMode -> String
(Int -> RoundingMode -> ShowS)
-> (RoundingMode -> String)
-> ([RoundingMode] -> ShowS)
-> Show RoundingMode
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [RoundingMode] -> ShowS
$cshowList :: [RoundingMode] -> ShowS
show :: RoundingMode -> String
$cshow :: RoundingMode -> String
showsPrec :: Int -> RoundingMode -> ShowS
$cshowsPrec :: Int -> RoundingMode -> ShowS
Show, RoundingMode -> RoundingMode -> Bool
(RoundingMode -> RoundingMode -> Bool)
-> (RoundingMode -> RoundingMode -> Bool) -> Eq RoundingMode
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: RoundingMode -> RoundingMode -> Bool
$c/= :: RoundingMode -> RoundingMode -> Bool
== :: RoundingMode -> RoundingMode -> Bool
$c== :: RoundingMode -> RoundingMode -> Bool
P.Eq, Eq RoundingMode
Eq RoundingMode
-> (RoundingMode -> RoundingMode -> Ordering)
-> (RoundingMode -> RoundingMode -> Bool)
-> (RoundingMode -> RoundingMode -> Bool)
-> (RoundingMode -> RoundingMode -> Bool)
-> (RoundingMode -> RoundingMode -> Bool)
-> (RoundingMode -> RoundingMode -> RoundingMode)
-> (RoundingMode -> RoundingMode -> RoundingMode)
-> Ord RoundingMode
RoundingMode -> RoundingMode -> Bool
RoundingMode -> RoundingMode -> Ordering
RoundingMode -> RoundingMode -> RoundingMode
forall a.
Eq a
-> (a -> a -> Ordering)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> a)
-> (a -> a -> a)
-> Ord a
min :: RoundingMode -> RoundingMode -> RoundingMode
$cmin :: RoundingMode -> RoundingMode -> RoundingMode
max :: RoundingMode -> RoundingMode -> RoundingMode
$cmax :: RoundingMode -> RoundingMode -> RoundingMode
>= :: RoundingMode -> RoundingMode -> Bool
$c>= :: RoundingMode -> RoundingMode -> Bool
> :: RoundingMode -> RoundingMode -> Bool
$c> :: RoundingMode -> RoundingMode -> Bool
<= :: RoundingMode -> RoundingMode -> Bool
$c<= :: RoundingMode -> RoundingMode -> Bool
< :: RoundingMode -> RoundingMode -> Bool
$c< :: RoundingMode -> RoundingMode -> Bool
compare :: RoundingMode -> RoundingMode -> Ordering
$ccompare :: RoundingMode -> RoundingMode -> Ordering
P.Ord)
data E = EBinOp BinOp E E | EUnOp UnOp E | Lit Rational | Var String | PowI E Integer | Float32 RoundingMode E | Float64 RoundingMode E | Float RoundingMode E | Pi | RoundToInteger RoundingMode E
deriving (Int -> E -> ShowS
[E] -> ShowS
E -> String
(Int -> E -> ShowS) -> (E -> String) -> ([E] -> ShowS) -> Show E
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [E] -> ShowS
$cshowList :: [E] -> ShowS
show :: E -> String
$cshow :: E -> String
showsPrec :: Int -> E -> ShowS
$cshowsPrec :: Int -> E -> ShowS
Show, E -> E -> Bool
(E -> E -> Bool) -> (E -> E -> Bool) -> Eq E
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: E -> E -> Bool
$c/= :: E -> E -> Bool
== :: E -> E -> Bool
$c== :: E -> E -> Bool
P.Eq, Eq E
Eq E
-> (E -> E -> Ordering)
-> (E -> E -> Bool)
-> (E -> E -> Bool)
-> (E -> E -> Bool)
-> (E -> E -> Bool)
-> (E -> E -> E)
-> (E -> E -> E)
-> Ord E
E -> E -> Bool
E -> E -> Ordering
E -> E -> E
forall a.
Eq a
-> (a -> a -> Ordering)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> a)
-> (a -> a -> a)
-> Ord a
min :: E -> E -> E
$cmin :: E -> E -> E
max :: E -> E -> E
$cmax :: E -> E -> E
>= :: E -> E -> Bool
$c>= :: E -> E -> Bool
> :: E -> E -> Bool
$c> :: E -> E -> Bool
<= :: E -> E -> Bool
$c<= :: E -> E -> Bool
< :: E -> E -> Bool
$c< :: E -> E -> Bool
compare :: E -> E -> Ordering
$ccompare :: E -> E -> Ordering
P.Ord)
data ESafe = EStrict E | ENonStrict E
deriving (Int -> ESafe -> ShowS
[ESafe] -> ShowS
ESafe -> String
(Int -> ESafe -> ShowS)
-> (ESafe -> String) -> ([ESafe] -> ShowS) -> Show ESafe
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [ESafe] -> ShowS
$cshowList :: [ESafe] -> ShowS
show :: ESafe -> String
$cshow :: ESafe -> String
showsPrec :: Int -> ESafe -> ShowS
$cshowsPrec :: Int -> ESafe -> ShowS
Show, ESafe -> ESafe -> Bool
(ESafe -> ESafe -> Bool) -> (ESafe -> ESafe -> Bool) -> Eq ESafe
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: ESafe -> ESafe -> Bool
$c/= :: ESafe -> ESafe -> Bool
== :: ESafe -> ESafe -> Bool
$c== :: ESafe -> ESafe -> Bool
P.Eq, Eq ESafe
Eq ESafe
-> (ESafe -> ESafe -> Ordering)
-> (ESafe -> ESafe -> Bool)
-> (ESafe -> ESafe -> Bool)
-> (ESafe -> ESafe -> Bool)
-> (ESafe -> ESafe -> Bool)
-> (ESafe -> ESafe -> ESafe)
-> (ESafe -> ESafe -> ESafe)
-> Ord ESafe
ESafe -> ESafe -> Bool
ESafe -> ESafe -> Ordering
ESafe -> ESafe -> ESafe
forall a.
Eq a
-> (a -> a -> Ordering)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> a)
-> (a -> a -> a)
-> Ord a
min :: ESafe -> ESafe -> ESafe
$cmin :: ESafe -> ESafe -> ESafe
max :: ESafe -> ESafe -> ESafe
$cmax :: ESafe -> ESafe -> ESafe
>= :: ESafe -> ESafe -> Bool
$c>= :: ESafe -> ESafe -> Bool
> :: ESafe -> ESafe -> Bool
$c> :: ESafe -> ESafe -> Bool
<= :: ESafe -> ESafe -> Bool
$c<= :: ESafe -> ESafe -> Bool
< :: ESafe -> ESafe -> Bool
$c< :: ESafe -> ESafe -> Bool
compare :: ESafe -> ESafe -> Ordering
$ccompare :: ESafe -> ESafe -> Ordering
P.Ord)
data Comp = Gt | Ge | Lt | Le | Eq
deriving (Int -> Comp -> ShowS
[Comp] -> ShowS
Comp -> String
(Int -> Comp -> ShowS)
-> (Comp -> String) -> ([Comp] -> ShowS) -> Show Comp
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [Comp] -> ShowS
$cshowList :: [Comp] -> ShowS
show :: Comp -> String
$cshow :: Comp -> String
showsPrec :: Int -> Comp -> ShowS
$cshowsPrec :: Int -> Comp -> ShowS
Show, Comp -> Comp -> Bool
(Comp -> Comp -> Bool) -> (Comp -> Comp -> Bool) -> Eq Comp
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: Comp -> Comp -> Bool
$c/= :: Comp -> Comp -> Bool
== :: Comp -> Comp -> Bool
$c== :: Comp -> Comp -> Bool
P.Eq, Eq Comp
Eq Comp
-> (Comp -> Comp -> Ordering)
-> (Comp -> Comp -> Bool)
-> (Comp -> Comp -> Bool)
-> (Comp -> Comp -> Bool)
-> (Comp -> Comp -> Bool)
-> (Comp -> Comp -> Comp)
-> (Comp -> Comp -> Comp)
-> Ord Comp
Comp -> Comp -> Bool
Comp -> Comp -> Ordering
Comp -> Comp -> Comp
forall a.
Eq a
-> (a -> a -> Ordering)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> a)
-> (a -> a -> a)
-> Ord a
min :: Comp -> Comp -> Comp
$cmin :: Comp -> Comp -> Comp
max :: Comp -> Comp -> Comp
$cmax :: Comp -> Comp -> Comp
>= :: Comp -> Comp -> Bool
$c>= :: Comp -> Comp -> Bool
> :: Comp -> Comp -> Bool
$c> :: Comp -> Comp -> Bool
<= :: Comp -> Comp -> Bool
$c<= :: Comp -> Comp -> Bool
< :: Comp -> Comp -> Bool
$c< :: Comp -> Comp -> Bool
compare :: Comp -> Comp -> Ordering
$ccompare :: Comp -> Comp -> Ordering
P.Ord)
data Conn = And | Or | Impl
deriving (Int -> Conn -> ShowS
[Conn] -> ShowS
Conn -> String
(Int -> Conn -> ShowS)
-> (Conn -> String) -> ([Conn] -> ShowS) -> Show Conn
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [Conn] -> ShowS
$cshowList :: [Conn] -> ShowS
show :: Conn -> String
$cshow :: Conn -> String
showsPrec :: Int -> Conn -> ShowS
$cshowsPrec :: Int -> Conn -> ShowS
Show, Conn -> Conn -> Bool
(Conn -> Conn -> Bool) -> (Conn -> Conn -> Bool) -> Eq Conn
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: Conn -> Conn -> Bool
$c/= :: Conn -> Conn -> Bool
== :: Conn -> Conn -> Bool
$c== :: Conn -> Conn -> Bool
P.Eq, Eq Conn
Eq Conn
-> (Conn -> Conn -> Ordering)
-> (Conn -> Conn -> Bool)
-> (Conn -> Conn -> Bool)
-> (Conn -> Conn -> Bool)
-> (Conn -> Conn -> Bool)
-> (Conn -> Conn -> Conn)
-> (Conn -> Conn -> Conn)
-> Ord Conn
Conn -> Conn -> Bool
Conn -> Conn -> Ordering
Conn -> Conn -> Conn
forall a.
Eq a
-> (a -> a -> Ordering)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> a)
-> (a -> a -> a)
-> Ord a
min :: Conn -> Conn -> Conn
$cmin :: Conn -> Conn -> Conn
max :: Conn -> Conn -> Conn
$cmax :: Conn -> Conn -> Conn
>= :: Conn -> Conn -> Bool
$c>= :: Conn -> Conn -> Bool
> :: Conn -> Conn -> Bool
$c> :: Conn -> Conn -> Bool
<= :: Conn -> Conn -> Bool
$c<= :: Conn -> Conn -> Bool
< :: Conn -> Conn -> Bool
$c< :: Conn -> Conn -> Bool
compare :: Conn -> Conn -> Ordering
$ccompare :: Conn -> Conn -> Ordering
P.Ord)
data F = FComp Comp E E | FConn Conn F F | FNot F | FTrue | FFalse
deriving (Int -> F -> ShowS
[F] -> ShowS
F -> String
(Int -> F -> ShowS) -> (F -> String) -> ([F] -> ShowS) -> Show F
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [F] -> ShowS
$cshowList :: [F] -> ShowS
show :: F -> String
$cshow :: F -> String
showsPrec :: Int -> F -> ShowS
$cshowsPrec :: Int -> F -> ShowS
Show, F -> F -> Bool
(F -> F -> Bool) -> (F -> F -> Bool) -> Eq F
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: F -> F -> Bool
$c/= :: F -> F -> Bool
== :: F -> F -> Bool
$c== :: F -> F -> Bool
P.Eq, Eq F
Eq F
-> (F -> F -> Ordering)
-> (F -> F -> Bool)
-> (F -> F -> Bool)
-> (F -> F -> Bool)
-> (F -> F -> Bool)
-> (F -> F -> F)
-> (F -> F -> F)
-> Ord F
F -> F -> Bool
F -> F -> Ordering
F -> F -> F
forall a.
Eq a
-> (a -> a -> Ordering)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> a)
-> (a -> a -> a)
-> Ord a
min :: F -> F -> F
$cmin :: F -> F -> F
max :: F -> F -> F
$cmax :: F -> F -> F
>= :: F -> F -> Bool
$c>= :: F -> F -> Bool
> :: F -> F -> Bool
$c> :: F -> F -> Bool
<= :: F -> F -> Bool
$c<= :: F -> F -> Bool
< :: F -> F -> Bool
$c< :: F -> F -> Bool
compare :: F -> F -> Ordering
$ccompare :: F -> F -> Ordering
P.Ord)
lengthF :: F -> Integer
lengthF :: F -> Integer
lengthF (FConn Conn
_ F
f1 F
f2) = F -> Integer
lengthF F
f1 Integer -> Integer -> AddType Integer Integer
forall t1 t2. CanAddAsymmetric t1 t2 => t1 -> t2 -> AddType t1 t2
+ F -> Integer
lengthF F
f2
lengthF (FComp Comp
_ E
e1 E
e2) = E -> Integer
lengthE E
e1 Integer -> Integer -> AddType Integer Integer
forall t1 t2. CanAddAsymmetric t1 t2 => t1 -> t2 -> AddType t1 t2
+ E -> Integer
lengthE E
e2
lengthF (FNot F
f) = F -> Integer
lengthF F
f
lengthF F
FTrue = Integer
1
lengthF F
FFalse = Integer
1
lengthE :: E -> Integer
lengthE :: E -> Integer
lengthE (EBinOp BinOp
_ E
e1 E
e2) = E -> Integer
lengthE E
e1 Integer -> Integer -> AddType Integer Integer
forall t1 t2. CanAddAsymmetric t1 t2 => t1 -> t2 -> AddType t1 t2
+ E -> Integer
lengthE E
e2
lengthE (EUnOp UnOp
_ E
e) = E -> Integer
lengthE E
e
lengthE (Var String
_) = Integer
1
lengthE (Lit Rational
_) = Integer
1
lengthE (PowI E
e Integer
_) = E -> Integer
lengthE E
e
lengthE (Float RoundingMode
_ E
e) = E -> Integer
lengthE E
e
lengthE (Float32 RoundingMode
_ E
e) = E -> Integer
lengthE E
e
lengthE (Float64 RoundingMode
_ E
e) = E -> Integer
lengthE E
e
lengthE E
Pi = Integer
1
lengthE (RoundToInteger RoundingMode
_ E
e) = E -> Integer
lengthE E
e
newtype Name = Name String deriving Int -> Name -> ShowS
[Name] -> ShowS
Name -> String
(Int -> Name -> ShowS)
-> (Name -> String) -> ([Name] -> ShowS) -> Show Name
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [Name] -> ShowS
$cshowList :: [Name] -> ShowS
show :: Name -> String
$cshow :: Name -> String
showsPrec :: Int -> Name -> ShowS
$cshowsPrec :: Int -> Name -> ShowS
Show
instance Arbitrary Name where
arbitrary :: Gen Name
arbitrary =
[Gen Name] -> Gen Name
forall a. [Gen a] -> Gen a
oneof
[
Name -> Gen Name
forall (m :: * -> *) a. Monad m => a -> m a
return (String -> Name
Name String
"a"),
Name -> Gen Name
forall (m :: * -> *) a. Monad m => a -> m a
return (String -> Name
Name String
"b"),
Name -> Gen Name
forall (m :: * -> *) a. Monad m => a -> m a
return (String -> Name
Name String
"c"),
Name -> Gen Name
forall (m :: * -> *) a. Monad m => a -> m a
return (String -> Name
Name String
"d"),
Name -> Gen Name
forall (m :: * -> *) a. Monad m => a -> m a
return (String -> Name
Name String
"e"),
Name -> Gen Name
forall (m :: * -> *) a. Monad m => a -> m a
return (String -> Name
Name String
"f"),
Name -> Gen Name
forall (m :: * -> *) a. Monad m => a -> m a
return (String -> Name
Name String
"g"),
Name -> Gen Name
forall (m :: * -> *) a. Monad m => a -> m a
return (String -> Name
Name String
"h"),
Name -> Gen Name
forall (m :: * -> *) a. Monad m => a -> m a
return (String -> Name
Name String
"i"),
Name -> Gen Name
forall (m :: * -> *) a. Monad m => a -> m a
return (String -> Name
Name String
"j"),
Name -> Gen Name
forall (m :: * -> *) a. Monad m => a -> m a
return (String -> Name
Name String
"k"),
Name -> Gen Name
forall (m :: * -> *) a. Monad m => a -> m a
return (String -> Name
Name String
"l")
]
instance Arbitrary UnOp where
arbitrary :: Gen UnOp
arbitrary =
[(Int, Gen UnOp)] -> Gen UnOp
forall a. [(Int, Gen a)] -> Gen a
frequency [(Integer -> Int
forall t. CanBeInt t => t -> Int
int Integer
11, UnOp -> Gen UnOp
forall (m :: * -> *) a. Monad m => a -> m a
return UnOp
Negate), (Integer -> Int
forall t. CanBeInt t => t -> Int
int Integer
1, UnOp -> Gen UnOp
forall (m :: * -> *) a. Monad m => a -> m a
return UnOp
Abs), (Integer -> Int
forall t. CanBeInt t => t -> Int
int Integer
4, UnOp -> Gen UnOp
forall (m :: * -> *) a. Monad m => a -> m a
return UnOp
Sin), (Integer -> Int
forall t. CanBeInt t => t -> Int
int Integer
4, UnOp -> Gen UnOp
forall (m :: * -> *) a. Monad m => a -> m a
return UnOp
Cos)]
instance Arbitrary BinOp where
arbitrary :: Gen BinOp
arbitrary =
[(Int, Gen BinOp)] -> Gen BinOp
forall a. [(Int, Gen a)] -> Gen a
frequency [(Integer -> Int
forall t. CanBeInt t => t -> Int
int Integer
10, BinOp -> Gen BinOp
forall (m :: * -> *) a. Monad m => a -> m a
return BinOp
Add), (Integer -> Int
forall t. CanBeInt t => t -> Int
int Integer
10, BinOp -> Gen BinOp
forall (m :: * -> *) a. Monad m => a -> m a
return BinOp
Sub), (Integer -> Int
forall t. CanBeInt t => t -> Int
int Integer
10, BinOp -> Gen BinOp
forall (m :: * -> *) a. Monad m => a -> m a
return BinOp
Mul), (Integer -> Int
forall t. CanBeInt t => t -> Int
int Integer
10, BinOp -> Gen BinOp
forall (m :: * -> *) a. Monad m => a -> m a
return BinOp
Div), (Integer -> Int
forall t. CanBeInt t => t -> Int
int Integer
1, BinOp -> Gen BinOp
forall (m :: * -> *) a. Monad m => a -> m a
return BinOp
Min), (Integer -> Int
forall t. CanBeInt t => t -> Int
int Integer
1, BinOp -> Gen BinOp
forall (m :: * -> *) a. Monad m => a -> m a
return BinOp
Max)]
instance Arbitrary RoundingMode where
arbitrary :: Gen RoundingMode
arbitrary =
[Gen RoundingMode] -> Gen RoundingMode
forall a. [Gen a] -> Gen a
oneof [RoundingMode -> Gen RoundingMode
forall (m :: * -> *) a. Monad m => a -> m a
return RoundingMode
RNE, RoundingMode -> Gen RoundingMode
forall (m :: * -> *) a. Monad m => a -> m a
return RoundingMode
RTP, RoundingMode -> Gen RoundingMode
forall (m :: * -> *) a. Monad m => a -> m a
return RoundingMode
RTN, RoundingMode -> Gen RoundingMode
forall (m :: * -> *) a. Monad m => a -> m a
return RoundingMode
RTN]
instance Arbitrary E where
arbitrary :: Gen E
arbitrary = (Int -> Gen E) -> Gen E
forall a. (Int -> Gen a) -> Gen a
sized Int -> Gen E
eGenerator
where
varName :: Gen Name
varName :: Gen Name
varName = Gen Name
forall a. Arbitrary a => Gen a
arbitrary
eGenerator :: Int -> Gen E
eGenerator :: Int -> Gen E
eGenerator Int
n | Int
nInt -> Integer -> OrderCompareType Int Integer
forall a b.
HasOrderAsymmetric a b =>
a -> b -> OrderCompareType a b
>Integer
0 =
[Gen E] -> Gen E
forall a. [Gen a] -> Gen a
oneof
[
Rational -> E
Lit (Rational -> E) -> Gen Rational -> Gen E
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (Integer -> Rational) -> Gen Integer -> Gen Rational
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap Integer -> Rational
forall a. Real a => a -> Rational
toRational (Gen Integer
forall a. Arbitrary a => Gen a
arbitrary :: Gen Integer),
String -> E
Var (String -> E) -> (Name -> String) -> Name -> E
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Name -> String
forall a. Show a => a -> String
show (Name -> E) -> Gen Name -> Gen E
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Gen Name
varName,
UnOp -> E -> E
EUnOp (UnOp -> E -> E) -> Gen UnOp -> Gen (E -> E)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Gen UnOp
forall a. Arbitrary a => Gen a
arbitrary Gen (E -> E) -> Gen E -> Gen E
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> Gen E
subE,
UnOp -> E -> E
EUnOp UnOp
Sqrt (E -> E) -> (Rational -> E) -> Rational -> E
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Rational -> E
Lit (Rational -> E) -> Gen Rational -> Gen E
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (Positive Rational -> Rational)
-> Gen (Positive Rational) -> Gen Rational
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap Positive Rational -> Rational
forall a. Positive a -> a
getPositive (Gen (Positive Rational)
forall a. Arbitrary a => Gen a
arbitrary :: Gen (Positive Rational)),
BinOp -> E -> E -> E
EBinOp (BinOp -> E -> E -> E) -> Gen BinOp -> Gen (E -> E -> E)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Gen BinOp
forall a. Arbitrary a => Gen a
arbitrary Gen (E -> E -> E) -> Gen E -> Gen (E -> E)
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> Gen E
subE Gen (E -> E) -> Gen E -> Gen E
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> Gen E
subE
]
where
subE :: Gen E
subE = Int -> Gen E
eGenerator (Integer -> Int
forall t. CanBeInt t => t -> Int
int (Rational -> RoundType Rational
forall t. CanRound t => t -> RoundType t
floor (Int
n Int -> Integer -> DivType Int Integer
forall t1 t2. CanDiv t1 t2 => t1 -> t2 -> DivType t1 t2
/ Integer
20)))
sqrtG :: Rational -> E
sqrtG Rational
x = UnOp -> E -> E
EUnOp UnOp
Sqrt (Rational -> E
Lit Rational
x)
eGenerator Int
_ = [Gen E] -> Gen E
forall a. [Gen a] -> Gen a
oneof [Rational -> E
Lit (Rational -> E) -> Gen Rational -> Gen E
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> ((Integer -> Rational) -> Gen Integer -> Gen Rational
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap Integer -> Rational
forall a. Real a => a -> Rational
toRational (Gen Integer
forall a. Arbitrary a => Gen a
arbitrary :: Gen Integer)), String -> E
Var (String -> E) -> (Name -> String) -> Name -> E
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Name -> String
forall a. Show a => a -> String
show (Name -> E) -> Gen Name -> Gen E
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Gen Name
varName]
instance Arbitrary ESafe where
arbitrary :: Gen ESafe
arbitrary = Gen (E -> ESafe)
randomStrictness Gen (E -> ESafe) -> Gen E -> Gen ESafe
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> Gen E
randomE
where
randomE :: Gen E
randomE :: Gen E
randomE = Gen E
forall a. Arbitrary a => Gen a
arbitrary
randomStrictness :: Gen (E -> ESafe)
randomStrictness = [Gen (E -> ESafe)] -> Gen (E -> ESafe)
forall a. [Gen a] -> Gen a
oneof [(E -> ESafe) -> Gen (E -> ESafe)
forall (m :: * -> *) a. Monad m => a -> m a
return E -> ESafe
EStrict, (E -> ESafe) -> Gen (E -> ESafe)
forall (m :: * -> *) a. Monad m => a -> m a
return E -> ESafe
ENonStrict]
instance Arbitrary Comp where
arbitrary :: Gen Comp
arbitrary = [Gen Comp] -> Gen Comp
forall a. [Gen a] -> Gen a
oneof [Comp -> Gen Comp
forall (m :: * -> *) a. Monad m => a -> m a
return Comp
Gt, Comp -> Gen Comp
forall (m :: * -> *) a. Monad m => a -> m a
return Comp
Ge, Comp -> Gen Comp
forall (m :: * -> *) a. Monad m => a -> m a
return Comp
Lt, Comp -> Gen Comp
forall (m :: * -> *) a. Monad m => a -> m a
return Comp
Le, Comp -> Gen Comp
forall (m :: * -> *) a. Monad m => a -> m a
return Comp
Eq]
instance Arbitrary Conn where
arbitrary :: Gen Conn
arbitrary = [Gen Conn] -> Gen Conn
forall a. [Gen a] -> Gen a
oneof [Conn -> Gen Conn
forall (m :: * -> *) a. Monad m => a -> m a
return Conn
And, Conn -> Gen Conn
forall (m :: * -> *) a. Monad m => a -> m a
return Conn
Or, Conn -> Gen Conn
forall (m :: * -> *) a. Monad m => a -> m a
return Conn
Impl]
instance Arbitrary F where
arbitrary :: Gen F
arbitrary = (Int -> Gen F) -> Gen F
forall a. (Int -> Gen a) -> Gen a
sized Int -> Gen F
fGenerator
where
varName :: Gen Name
varName :: Gen Name
varName = Gen Name
forall a. Arbitrary a => Gen a
arbitrary
fGenerator :: Int -> Gen F
fGenerator :: Int -> Gen F
fGenerator Int
0 = [Gen F] -> Gen F
forall a. [Gen a] -> Gen a
oneof [Comp -> E -> E -> F
FComp (Comp -> E -> E -> F) -> Gen Comp -> Gen (E -> E -> F)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Gen Comp
forall a. Arbitrary a => Gen a
arbitrary Gen (E -> E -> F) -> Gen E -> Gen (E -> F)
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> Gen E
forall a. Arbitrary a => Gen a
arbitrary Gen (E -> F) -> Gen E -> Gen F
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> Gen E
forall a. Arbitrary a => Gen a
arbitrary]
fGenerator Int
n =
[(Int, Gen F)] -> Gen F
forall a. [(Int, Gen a)] -> Gen a
frequency
[
(Integer -> Int
forall t. CanBeInt t => t -> Int
int Integer
10, Comp -> E -> E -> F
FComp Comp
Eq (E -> E -> F) -> (String -> E) -> String -> E -> F
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> String -> E
Var (String -> E -> F) -> (Name -> String) -> Name -> E -> F
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Name -> String
forall a. Show a => a -> String
show (Name -> E -> F) -> Gen Name -> Gen (E -> F)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Gen Name
varName Gen (E -> F) -> Gen E -> Gen F
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> Gen E
forall a. Arbitrary a => Gen a
arbitrary),
(Integer -> Int
forall t. CanBeInt t => t -> Int
int Integer
30, Comp -> E -> E -> F
FComp (Comp -> E -> E -> F) -> Gen Comp -> Gen (E -> E -> F)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Gen Comp
forall a. Arbitrary a => Gen a
arbitrary Gen (E -> E -> F) -> Gen E -> Gen (E -> F)
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> Gen E
forall a. Arbitrary a => Gen a
arbitrary Gen (E -> F) -> Gen E -> Gen F
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> Gen E
forall a. Arbitrary a => Gen a
arbitrary),
(Integer -> Int
forall t. CanBeInt t => t -> Int
int Integer
30, Conn -> F -> F -> F
FConn (Conn -> F -> F -> F) -> Gen Conn -> Gen (F -> F -> F)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Gen Conn
forall a. Arbitrary a => Gen a
arbitrary Gen (F -> F -> F) -> Gen F -> Gen (F -> F)
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> Gen F
subF Gen (F -> F) -> Gen F -> Gen F
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> Gen F
subF),
(Integer -> Int
forall t. CanBeInt t => t -> Int
int Integer
30, F -> F
FNot (F -> F) -> Gen F -> Gen F
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Gen F
subF)
]
where
subF :: Gen F
subF = Int -> Gen F
fGenerator (Integer -> Int
forall t. CanBeInt t => t -> Int
int (Rational -> RoundType Rational
forall t. CanRound t => t -> RoundType t
floor (Int
n Int -> Integer -> DivType Int Integer
forall t1 t2. CanDiv t1 t2 => t1 -> t2 -> DivType t1 t2
/ Integer
20)))
flipStrictness :: ESafe -> ESafe
flipStrictness :: ESafe -> ESafe
flipStrictness (EStrict E
e) = E -> ESafe
ENonStrict E
e
flipStrictness (ENonStrict E
e) = E -> ESafe
EStrict E
e
negateSafeE :: ESafe -> ESafe
negateSafeE :: ESafe -> ESafe
negateSafeE (EStrict E
e) = E -> ESafe
ENonStrict (UnOp -> E -> E
EUnOp UnOp
Negate E
e)
negateSafeE (ENonStrict E
e) = E -> ESafe
EStrict (UnOp -> E -> E
EUnOp UnOp
Negate E
e)
extractSafeE :: ESafe -> E
(EStrict E
e) = E
e
extractSafeE (ENonStrict E
e) = E
e
fmapESafe :: (E -> E) -> ESafe -> ESafe
fmapESafe :: (E -> E) -> ESafe -> ESafe
fmapESafe E -> E
f (EStrict E
e) = E -> ESafe
EStrict (E -> ESafe) -> E -> ESafe
forall a b. (a -> b) -> a -> b
$ E -> E
f E
e
fmapESafe E -> E
f (ENonStrict E
e) = E -> ESafe
ENonStrict (E -> ESafe) -> E -> ESafe
forall a b. (a -> b) -> a -> b
$ E -> E
f E
e
fToECNF :: F -> [[ESafe]]
fToECNF :: F -> [[ESafe]]
fToECNF = Bool -> F -> [[ESafe]]
fToECNFB Bool
False
where
fToECNFB :: Bool -> F -> [[ESafe]]
fToECNFB :: Bool -> F -> [[ESafe]]
fToECNFB Bool
isNegated (FNot F
f) = Bool -> F -> [[ESafe]]
fToECNFB (Bool -> NegType Bool
forall t. CanNeg t => t -> NegType t
not Bool
isNegated) F
f
fToECNFB Bool
True (FComp Comp
op E
e1 E
e2) = case Comp
op of
Comp
Le -> Bool -> F -> [[ESafe]]
fToECNFB Bool
False (Comp -> E -> E -> F
FComp Comp
Gt E
e1 E
e2)
Comp
Lt -> Bool -> F -> [[ESafe]]
fToECNFB Bool
False (Comp -> E -> E -> F
FComp Comp
Ge E
e1 E
e2)
Comp
Ge -> Bool -> F -> [[ESafe]]
fToECNFB Bool
False (Comp -> E -> E -> F
FComp Comp
Lt E
e1 E
e2)
Comp
Gt -> Bool -> F -> [[ESafe]]
fToECNFB Bool
False (Comp -> E -> E -> F
FComp Comp
Le E
e1 E
e2)
Comp
Eq -> Bool -> F -> [[ESafe]]
fToECNFB Bool
True (Conn -> F -> F -> F
FConn Conn
And (Comp -> E -> E -> F
FComp Comp
Ge E
e1 E
e2) (Comp -> E -> E -> F
FComp Comp
Le E
e1 E
e2))
fToECNFB Bool
False (FComp Comp
op E
e1 E
e2) = case Comp
op of
Comp
Le -> Bool -> F -> [[ESafe]]
fToECNFB Bool
False (Comp -> E -> E -> F
FComp Comp
Ge E
e2 E
e1)
Comp
Lt -> Bool -> F -> [[ESafe]]
fToECNFB Bool
False (Comp -> E -> E -> F
FComp Comp
Gt E
e2 E
e1)
Comp
Ge -> [[E -> ESafe
ENonStrict (BinOp -> E -> E -> E
EBinOp BinOp
Sub E
e1 E
e2)]]
Comp
Gt -> [[E -> ESafe
EStrict (BinOp -> E -> E -> E
EBinOp BinOp
Sub E
e1 E
e2)]]
Comp
Eq -> Bool -> F -> [[ESafe]]
fToECNFB Bool
False (Conn -> F -> F -> F
FConn Conn
And (Comp -> E -> E -> F
FComp Comp
Ge E
e1 E
e2) (Comp -> E -> E -> F
FComp Comp
Le E
e1 E
e2))
fToECNFB Bool
True (FConn Conn
op F
f1 F
f2) = case Conn
op of
Conn
And -> [[ESafe]
d1 [ESafe] -> [ESafe] -> [ESafe]
forall a. [a] -> [a] -> [a]
++ [ESafe]
d2 | [ESafe]
d1 <- Bool -> F -> [[ESafe]]
fToECNFB Bool
True F
f1, [ESafe]
d2 <- Bool -> F -> [[ESafe]]
fToECNFB Bool
True F
f2]
Conn
Or -> Bool -> F -> [[ESafe]]
fToECNFB Bool
True F
f1 [[ESafe]] -> [[ESafe]] -> [[ESafe]]
forall a. [a] -> [a] -> [a]
++ Bool -> F -> [[ESafe]]
fToECNFB Bool
True F
f2
Conn
Impl -> Bool -> F -> [[ESafe]]
fToECNFB Bool
False F
f1 [[ESafe]] -> [[ESafe]] -> [[ESafe]]
forall a. [a] -> [a] -> [a]
++ Bool -> F -> [[ESafe]]
fToECNFB Bool
True F
f2
fToECNFB Bool
False (FConn Conn
op F
f1 F
f2) = case Conn
op of
Conn
And -> Bool -> F -> [[ESafe]]
fToECNFB Bool
False F
f1 [[ESafe]] -> [[ESafe]] -> [[ESafe]]
forall a. [a] -> [a] -> [a]
++ Bool -> F -> [[ESafe]]
fToECNFB Bool
False F
f2
Conn
Or -> [[ESafe]
d1 [ESafe] -> [ESafe] -> [ESafe]
forall a. [a] -> [a] -> [a]
++ [ESafe]
d2 | [ESafe]
d1 <- Bool -> F -> [[ESafe]]
fToECNFB Bool
False F
f1, [ESafe]
d2 <- Bool -> F -> [[ESafe]]
fToECNFB Bool
False F
f2]
Conn
Impl -> [[ESafe]
d1 [ESafe] -> [ESafe] -> [ESafe]
forall a. [a] -> [a] -> [a]
++ [ESafe]
d2 | [ESafe]
d1 <- Bool -> F -> [[ESafe]]
fToECNFB Bool
True F
f1, [ESafe]
d2 <- Bool -> F -> [[ESafe]]
fToECNFB Bool
False F
f2]
fToECNFB Bool
True F
FTrue = Bool -> F -> [[ESafe]]
fToECNFB Bool
False F
FFalse
fToECNFB Bool
True F
FFalse = Bool -> F -> [[ESafe]]
fToECNFB Bool
False F
FTrue
fToECNFB Bool
False F
FTrue = [[E -> ESafe
ENonStrict (Rational -> E
Lit Rational
1.0)]]
fToECNFB Bool
False F
FFalse = [[E -> ESafe
ENonStrict (Rational -> E
Lit (-Rational
1.0))]]
fToEDNF :: F -> [[ESafe]]
fToEDNF :: F -> [[ESafe]]
fToEDNF = Bool -> F -> [[ESafe]]
fToEDNFB Bool
False
where
fToEDNFB :: Bool -> F -> [[ESafe]]
fToEDNFB :: Bool -> F -> [[ESafe]]
fToEDNFB Bool
isNegated (FNot F
f) = Bool -> F -> [[ESafe]]
fToEDNFB (Bool -> NegType Bool
forall t. CanNeg t => t -> NegType t
not Bool
isNegated) F
f
fToEDNFB Bool
True (FComp Comp
op E
e1 E
e2) = case Comp
op of
Comp
Le -> Bool -> F -> [[ESafe]]
fToEDNFB Bool
False (Comp -> E -> E -> F
FComp Comp
Gt E
e1 E
e2)
Comp
Lt -> Bool -> F -> [[ESafe]]
fToEDNFB Bool
False (Comp -> E -> E -> F
FComp Comp
Ge E
e1 E
e2)
Comp
Ge -> Bool -> F -> [[ESafe]]
fToEDNFB Bool
False (Comp -> E -> E -> F
FComp Comp
Lt E
e1 E
e2)
Comp
Gt -> Bool -> F -> [[ESafe]]
fToEDNFB Bool
False (Comp -> E -> E -> F
FComp Comp
Le E
e1 E
e2)
Comp
Eq -> Bool -> F -> [[ESafe]]
fToEDNFB Bool
True (Conn -> F -> F -> F
FConn Conn
And (Comp -> E -> E -> F
FComp Comp
Ge E
e1 E
e2) (Comp -> E -> E -> F
FComp Comp
Le E
e1 E
e2))
fToEDNFB Bool
False (FComp Comp
op E
e1 E
e2) = case Comp
op of
Comp
Le -> Bool -> F -> [[ESafe]]
fToEDNFB Bool
False (Comp -> E -> E -> F
FComp Comp
Ge E
e2 E
e1)
Comp
Lt -> Bool -> F -> [[ESafe]]
fToEDNFB Bool
False (Comp -> E -> E -> F
FComp Comp
Gt E
e2 E
e1)
Comp
Ge -> [[E -> ESafe
ENonStrict (BinOp -> E -> E -> E
EBinOp BinOp
Sub E
e1 E
e2)]]
Comp
Gt -> [[E -> ESafe
EStrict (BinOp -> E -> E -> E
EBinOp BinOp
Sub E
e1 E
e2)]]
Comp
Eq -> Bool -> F -> [[ESafe]]
fToEDNFB Bool
False (Conn -> F -> F -> F
FConn Conn
And (Comp -> E -> E -> F
FComp Comp
Ge E
e1 E
e2) (Comp -> E -> E -> F
FComp Comp
Le E
e1 E
e2))
fToEDNFB Bool
True (FConn Conn
op F
f1 F
f2) = case Conn
op of
Conn
And -> Bool -> F -> [[ESafe]]
fToEDNFB Bool
True F
f1 [[ESafe]] -> [[ESafe]] -> [[ESafe]]
forall a. [a] -> [a] -> [a]
++ Bool -> F -> [[ESafe]]
fToEDNFB Bool
True F
f2
Conn
Or -> [[ESafe]
d1 [ESafe] -> [ESafe] -> [ESafe]
forall a. [a] -> [a] -> [a]
++ [ESafe]
d2 | [ESafe]
d1 <- Bool -> F -> [[ESafe]]
fToEDNFB Bool
True F
f1, [ESafe]
d2 <- Bool -> F -> [[ESafe]]
fToEDNFB Bool
True F
f2]
Conn
Impl -> [[ESafe]
d1 [ESafe] -> [ESafe] -> [ESafe]
forall a. [a] -> [a] -> [a]
++ [ESafe]
d2 | [ESafe]
d1 <- Bool -> F -> [[ESafe]]
fToEDNFB Bool
False F
f1, [ESafe]
d2 <- Bool -> F -> [[ESafe]]
fToEDNFB Bool
True F
f2]
fToEDNFB Bool
False (FConn Conn
op F
f1 F
f2) = case Conn
op of
Conn
And -> [[ESafe]
d1 [ESafe] -> [ESafe] -> [ESafe]
forall a. [a] -> [a] -> [a]
++ [ESafe]
d2 | [ESafe]
d1 <- Bool -> F -> [[ESafe]]
fToEDNFB Bool
False F
f1, [ESafe]
d2 <- Bool -> F -> [[ESafe]]
fToEDNFB Bool
False F
f2]
Conn
Or -> Bool -> F -> [[ESafe]]
fToEDNFB Bool
False F
f1 [[ESafe]] -> [[ESafe]] -> [[ESafe]]
forall a. [a] -> [a] -> [a]
++ Bool -> F -> [[ESafe]]
fToEDNFB Bool
False F
f2
Conn
Impl -> Bool -> F -> [[ESafe]]
fToEDNFB Bool
True F
f1 [[ESafe]] -> [[ESafe]] -> [[ESafe]]
forall a. [a] -> [a] -> [a]
++ Bool -> F -> [[ESafe]]
fToEDNFB Bool
False F
f2
fToEDNFB Bool
True F
FTrue = Bool -> F -> [[ESafe]]
fToEDNFB Bool
False F
FFalse
fToEDNFB Bool
True F
FFalse = Bool -> F -> [[ESafe]]
fToEDNFB Bool
False F
FTrue
fToEDNFB Bool
False F
FTrue = [[E -> ESafe
ENonStrict (Rational -> E
Lit Rational
1.0)]]
fToEDNFB Bool
False F
FFalse = [[E -> ESafe
ENonStrict (Rational -> E
Lit (-Rational
1.0))]]
fToFDNF :: F -> [[F]]
fToFDNF :: F -> [[F]]
fToFDNF = Bool -> F -> [[F]]
fToFDNFB Bool
False
where
fToFDNFB :: Bool -> F -> [[F]]
fToFDNFB :: Bool -> F -> [[F]]
fToFDNFB Bool
isNegated (FNot F
f) = Bool -> F -> [[F]]
fToFDNFB (Bool -> NegType Bool
forall t. CanNeg t => t -> NegType t
not Bool
isNegated) F
f
fToFDNFB Bool
True f :: F
f@FComp {} =
case F
f of
FComp Comp
Ge E
e1 E
e2 -> [[Comp -> E -> E -> F
FComp Comp
Gt E
e2 E
e1]]
FComp Comp
Gt E
e1 E
e2 -> [[Comp -> E -> E -> F
FComp Comp
Ge E
e2 E
e1]]
FComp Comp
Le E
e1 E
e2 -> [[Comp -> E -> E -> F
FComp Comp
Gt E
e1 E
e2]]
FComp Comp
Lt E
e1 E
e2 -> [[Comp -> E -> E -> F
FComp Comp
Ge E
e1 E
e2]]
FComp Comp
Eq E
e1 E
e2 -> Bool -> F -> [[F]]
fToFDNFB Bool
False (F -> [[F]]) -> F -> [[F]]
forall a b. (a -> b) -> a -> b
$ Conn -> F -> F -> F
FConn Conn
Or (Comp -> E -> E -> F
FComp Comp
Gt E
e1 E
e2) (Comp -> E -> E -> F
FComp Comp
Gt E
e2 E
e1)
fToFDNFB Bool
False f :: F
f@FComp {} =
case F
f of
FComp Comp
Ge E
_ E
_ -> [[F
f]]
FComp Comp
Gt E
_ E
_ -> [[F
f]]
FComp Comp
Le E
e1 E
e2 -> [[Comp -> E -> E -> F
FComp Comp
Ge E
e2 E
e1]]
FComp Comp
Lt E
e1 E
e2 -> [[Comp -> E -> E -> F
FComp Comp
Gt E
e2 E
e1]]
FComp Comp
Eq E
e1 E
e2 -> [[Comp -> E -> E -> F
FComp Comp
Ge E
e1 E
e2, Comp -> E -> E -> F
FComp Comp
Ge E
e2 E
e1]]
fToFDNFB Bool
True (FConn Conn
op F
f1 F
f2) = case Conn
op of
Conn
And -> Bool -> F -> [[F]]
fToFDNFB Bool
True F
f1 [[F]] -> [[F]] -> [[F]]
forall a. [a] -> [a] -> [a]
++ Bool -> F -> [[F]]
fToFDNFB Bool
True F
f2
Conn
Or -> [[F]
d1 [F] -> [F] -> [F]
forall a. [a] -> [a] -> [a]
++ [F]
d2 | [F]
d1 <- Bool -> F -> [[F]]
fToFDNFB Bool
True F
f1, [F]
d2 <- Bool -> F -> [[F]]
fToFDNFB Bool
True F
f2]
Conn
Impl -> [[F]
d1 [F] -> [F] -> [F]
forall a. [a] -> [a] -> [a]
++ [F]
d2 | [F]
d1 <- Bool -> F -> [[F]]
fToFDNFB Bool
False F
f1, [F]
d2 <- Bool -> F -> [[F]]
fToFDNFB Bool
True F
f2]
fToFDNFB Bool
False (FConn Conn
op F
f1 F
f2) = case Conn
op of
Conn
And -> [[F]
d1 [F] -> [F] -> [F]
forall a. [a] -> [a] -> [a]
++ [F]
d2 | [F]
d1 <- Bool -> F -> [[F]]
fToFDNFB Bool
False F
f1, [F]
d2 <- Bool -> F -> [[F]]
fToFDNFB Bool
False F
f2]
Conn
Or -> Bool -> F -> [[F]]
fToFDNFB Bool
False F
f1 [[F]] -> [[F]] -> [[F]]
forall a. [a] -> [a] -> [a]
++ Bool -> F -> [[F]]
fToFDNFB Bool
False F
f2
Conn
Impl -> Bool -> F -> [[F]]
fToFDNFB Bool
True F
f1 [[F]] -> [[F]] -> [[F]]
forall a. [a] -> [a] -> [a]
++ Bool -> F -> [[F]]
fToFDNFB Bool
False F
f2
fToFDNFB Bool
True F
FTrue = Bool -> F -> [[F]]
fToFDNFB Bool
False F
FFalse
fToFDNFB Bool
True F
FFalse = Bool -> F -> [[F]]
fToFDNFB Bool
False F
FTrue
fToFDNFB Bool
False F
FTrue = [[F
FTrue]]
fToFDNFB Bool
False F
FFalse = [[F
FFalse]]
eSafeToF :: ESafe -> F
eSafeToF :: ESafe -> F
eSafeToF (EStrict E
e) = Comp -> E -> E -> F
FComp Comp
Gt E
e (Rational -> E
Lit Rational
0.0)
eSafeToF (ENonStrict E
e) = Comp -> E -> E -> F
FComp Comp
Ge E
e (Rational -> E
Lit Rational
0.0)
eSafeDisjToF :: [ESafe] -> F
eSafeDisjToF :: [ESafe] -> F
eSafeDisjToF [] = String -> F
forall a. HasCallStack => String -> a
error String
"empty disjunction given to eSafeDisjToF"
eSafeDisjToF [ESafe
e] = ESafe -> F
eSafeToF ESafe
e
eSafeDisjToF (ESafe
e : [ESafe]
es) = Conn -> F -> F -> F
FConn Conn
Or (ESafe -> F
eSafeToF ESafe
e) ([ESafe] -> F
eSafeDisjToF [ESafe]
es)
eSafeCNFToF :: [[ESafe]] -> F
eSafeCNFToF :: [[ESafe]] -> F
eSafeCNFToF [] = String -> F
forall a. HasCallStack => String -> a
error String
"empty disjunction given to eSafeCNFToF"
eSafeCNFToF [[ESafe]
disj] = [ESafe] -> F
eSafeDisjToF [ESafe]
disj
eSafeCNFToF ([ESafe]
disj : [[ESafe]]
disjs) = Conn -> F -> F -> F
FConn Conn
And ([ESafe] -> F
eSafeDisjToF [ESafe]
disj) ([[ESafe]] -> F
eSafeCNFToF [[ESafe]]
disjs)
eSafeCNFToDNF :: [[ESafe]] -> [[ESafe]]
eSafeCNFToDNF :: [[ESafe]] -> [[ESafe]]
eSafeCNFToDNF = F -> [[ESafe]]
fToEDNF (F -> [[ESafe]]) -> ([[ESafe]] -> F) -> [[ESafe]] -> [[ESafe]]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [[ESafe]] -> F
eSafeCNFToF
simplifyE :: E -> E
simplifyE :: E -> E
simplifyE E
unsimplifiedE = if E
unsimplifiedE E -> E -> Bool
forall a. Eq a => a -> a -> Bool
P.== E
simplifiedE then E
simplifiedE else E -> E
simplifyE E
simplifiedE
where
simplifiedE :: E
simplifiedE = E -> E
simplify E
unsimplifiedE
simplify :: E -> E
simplify (EBinOp BinOp
Div E
e (Lit Rational
1.0)) = E
e
simplify (EBinOp BinOp
Div (Lit Rational
0.0) E
_) = Rational -> E
Lit Rational
0.0
simplify (EBinOp BinOp
Mul (Lit (-1.0)) E
e) = E -> E
simplify (UnOp -> E -> E
EUnOp UnOp
Negate E
e)
simplify (EBinOp BinOp
Mul E
e (Lit (-1.0))) = E -> E
simplify (UnOp -> E -> E
EUnOp UnOp
Negate E
e)
simplify (EBinOp BinOp
Mul (Lit Rational
0.0) E
_) = Rational -> E
Lit Rational
0.0
simplify (EBinOp BinOp
Mul E
_ (Lit Rational
0.0)) = Rational -> E
Lit Rational
0.0
simplify (EBinOp BinOp
Mul (Lit Rational
1.0) E
e) = E
e
simplify (EBinOp BinOp
Mul E
e (Lit Rational
1.0)) = E
e
simplify (EBinOp BinOp
Add (Lit Rational
0.0) E
e) = E
e
simplify (EBinOp BinOp
Add E
e (Lit Rational
0.0)) = E
e
simplify (EBinOp BinOp
Sub E
e (Lit Rational
0.0)) = E
e
simplify (EBinOp BinOp
Sub E
e1 E
e2) = if E
e1 E -> E -> Bool
forall a. Eq a => a -> a -> Bool
P.== E
e2 then Rational -> E
Lit Rational
0.0 else BinOp -> E -> E -> E
EBinOp BinOp
Sub (E -> E
simplifyE E
e1) (E -> E
simplifyE E
e2)
simplify (EBinOp BinOp
Pow E
_ (Lit Rational
0.0)) = Rational -> E
Lit Rational
1.0
simplify (EBinOp BinOp
Pow E
e (Lit Rational
1.0)) = E
e
simplify (EBinOp BinOp
Pow E
e (Lit Rational
n)) = if Rational -> Integer
forall a. Ratio a -> a
denominator Rational
n Integer -> Integer -> EqCompareType Integer Integer
forall a b. HasEqAsymmetric a b => a -> b -> EqCompareType a b
== Integer
1 then E -> Integer -> E
PowI E
e (Rational -> Integer
forall a. Ratio a -> a
numerator Rational
n) else BinOp -> E -> E -> E
EBinOp BinOp
Pow E
e (Rational -> E
Lit Rational
n)
simplify (PowI E
_e Integer
0) = Rational -> E
Lit Rational
1.0
simplify (PowI E
e Integer
1) = E
e
simplify (EUnOp UnOp
Negate (Lit Rational
0.0)) = Rational -> E
Lit Rational
0.0
simplify (EUnOp UnOp
Negate (EUnOp UnOp
Negate E
e)) = E
e
simplify (EUnOp UnOp
Sqrt (Lit Rational
0.0)) = Rational -> E
Lit Rational
0.0
simplify (EUnOp UnOp
Sqrt (Lit Rational
1.0)) = Rational -> E
Lit Rational
1.0
simplify (EUnOp UnOp
Abs (Lit Rational
v)) = Rational -> E
Lit (Rational -> AbsType Rational
forall t. CanAbs t => t -> AbsType t
abs Rational
v)
simplify (EBinOp BinOp
Min E
e1 E
e2) = if E
e1 E -> E -> Bool
forall a. Eq a => a -> a -> Bool
P.== E
e2 then E
e1 else BinOp -> E -> E -> E
EBinOp BinOp
Min (E -> E
simplifyE E
e1) (E -> E
simplifyE E
e2)
simplify (EBinOp BinOp
Max E
e1 E
e2) = if E
e1 E -> E -> Bool
forall a. Eq a => a -> a -> Bool
P.== E
e2 then E
e1 else BinOp -> E -> E -> E
EBinOp BinOp
Max (E -> E
simplifyE E
e1) (E -> E
simplifyE E
e2)
simplify (EBinOp BinOp
op E
e1 E
e2) = BinOp -> E -> E -> E
EBinOp BinOp
op (E -> E
simplify E
e1) (E -> E
simplify E
e2)
simplify (EUnOp UnOp
op E
e) = UnOp -> E -> E
EUnOp UnOp
op (E -> E
simplify E
e)
simplify E
e = E
e
simplifyF :: F -> F
simplifyF :: F -> F
simplifyF F
unsimplifiedF = if F
unsimplifiedF F -> F -> Bool
forall a. Eq a => a -> a -> Bool
P.== F
simplifiedF then F
simplifiedF else F -> F
simplifyF F
simplifiedF
where
simplifiedF :: F
simplifiedF = F -> F
simplify F
unsimplifiedF
simplify :: F -> F
simplify (FConn Conn
Or f1 :: F
f1@(FComp Comp
Lt E
l1 E
r1) f2 :: F
f2@(FComp Comp
Eq E
l2 E
r2)) = if E
l1 E -> E -> Bool
forall a. Eq a => a -> a -> Bool
P.== E
l2 Bool -> Bool -> Bool
P.&& E
r1 E -> E -> Bool
forall a. Eq a => a -> a -> Bool
P.== E
r2 then Comp -> E -> E -> F
FComp Comp
Le E
l1 E
r1 else Conn -> F -> F -> F
FConn Conn
Or (F -> F
simplify F
f1) (F -> F
simplify F
f2)
simplify (FConn Conn
Or f1 :: F
f1@(FComp Comp
Eq E
l1 E
r1) f2 :: F
f2@(FComp Comp
Lt E
l2 E
r2)) = if E
l1 E -> E -> Bool
forall a. Eq a => a -> a -> Bool
P.== E
l2 Bool -> Bool -> Bool
P.&& E
r1 E -> E -> Bool
forall a. Eq a => a -> a -> Bool
P.== E
r2 then Comp -> E -> E -> F
FComp Comp
Le E
l1 E
r1 else Conn -> F -> F -> F
FConn Conn
Or (F -> F
simplify F
f1) (F -> F
simplify F
f2)
simplify (FConn Conn
Or f1 :: F
f1@(FComp Comp
Gt E
l1 E
r1) f2 :: F
f2@(FComp Comp
Eq E
l2 E
r2)) = if E
l1 E -> E -> Bool
forall a. Eq a => a -> a -> Bool
P.== E
l2 Bool -> Bool -> Bool
P.&& E
r1 E -> E -> Bool
forall a. Eq a => a -> a -> Bool
P.== E
r2 then Comp -> E -> E -> F
FComp Comp
Ge E
l1 E
r1 else Conn -> F -> F -> F
FConn Conn
Or (F -> F
simplify F
f1) (F -> F
simplify F
f2)
simplify (FConn Conn
Or f1 :: F
f1@(FComp Comp
Eq E
l1 E
r1) f2 :: F
f2@(FComp Comp
Gt E
l2 E
r2)) = if E
l1 E -> E -> Bool
forall a. Eq a => a -> a -> Bool
P.== E
l2 Bool -> Bool -> Bool
P.&& E
r1 E -> E -> Bool
forall a. Eq a => a -> a -> Bool
P.== E
r2 then Comp -> E -> E -> F
FComp Comp
Ge E
l1 E
r1 else Conn -> F -> F -> F
FConn Conn
Or (F -> F
simplify F
f1) (F -> F
simplify F
f2)
simplify (FConn Conn
And f1 :: F
f1@(FConn Conn
Impl F
cond1 F
branch1) f2 :: F
f2@(FConn Conn
Impl (FNot F
cond2) F
branch2)) =
if F
cond1 F -> F -> Bool
forall a. Eq a => a -> a -> Bool
P.== F
cond2 Bool -> Bool -> AndOrType Bool Bool
forall a b. CanAndOrAsymmetric a b => a -> b -> AndOrType a b
&& F
branch1 F -> F -> Bool
forall a. Eq a => a -> a -> Bool
P.== F
branch2
then F -> F
simplify F
branch1
else Conn -> F -> F -> F
FConn Conn
And (F -> F
simplify F
f1) (F -> F
simplify F
f2)
simplify (FConn Conn
And F
_ F
FFalse) = IfThenElseType Bool F
F
FFalse
simplify (FConn Conn
And F
FFalse F
_) = IfThenElseType Bool F
F
FFalse
simplify (FConn Conn
And F
f F
FTrue) = F -> F
simplify F
f
simplify (FConn Conn
And F
FTrue F
f) = F -> F
simplify F
f
simplify (FConn Conn
And F
x1 f2 :: F
f2@(FConn Conn
Or (FNot F
x2) F
y)) = if F
x1 F -> F -> Bool
forall a. Eq a => a -> a -> Bool
P.== F
x2 then F -> F
simplify (Conn -> F -> F -> F
FConn Conn
And F
x1 F
y) else Conn -> F -> F -> F
FConn Conn
And (F -> F
simplify F
x1) (F -> F
simplify F
f2)
simplify (FConn Conn
And f1 :: F
f1@(FConn Conn
Or (FNot F
x1) F
y) F
x2) = if F
x1 F -> F -> Bool
forall a. Eq a => a -> a -> Bool
P.== F
x2 then F -> F
simplify (Conn -> F -> F -> F
FConn Conn
And F
y F
x2) else Conn -> F -> F -> F
FConn Conn
And (F -> F
simplify F
f1) (F -> F
simplify F
x2)
simplify (FConn Conn
And F
x1 f2 :: F
f2@(FConn Conn
Or F
y (FNot F
x2))) = if F
x1 F -> F -> Bool
forall a. Eq a => a -> a -> Bool
P.== F
x2 then F -> F
simplify (Conn -> F -> F -> F
FConn Conn
And F
x1 F
y) else Conn -> F -> F -> F
FConn Conn
And (F -> F
simplify F
x1) (F -> F
simplify F
f2)
simplify (FConn Conn
And f1 :: F
f1@(FConn Conn
Or F
y (FNot F
x1)) F
x2) = if F
x1 F -> F -> Bool
forall a. Eq a => a -> a -> Bool
P.== F
x2 then F -> F
simplify (Conn -> F -> F -> F
FConn Conn
And F
y F
x2) else Conn -> F -> F -> F
FConn Conn
And (F -> F
simplify F
f1) (F -> F
simplify F
x2)
simplify (FConn Conn
And f1 :: F
f1@(FConn Conn
Or F
v1 F
v2) f2 :: F
f2@(FNot F
v3))
| F
v3 F -> F -> Bool
forall a. Eq a => a -> a -> Bool
P.== F
v1 = F -> F
simplify (Conn -> F -> F -> F
FConn Conn
And F
v2 (F -> F
FNot F
v3))
| F
v3 F -> F -> Bool
forall a. Eq a => a -> a -> Bool
P.== F
v2 = F -> F
simplify (Conn -> F -> F -> F
FConn Conn
And F
v1 (F -> F
FNot F
v3))
| F
f1 F -> F -> Bool
forall a. Eq a => a -> a -> Bool
P.== F
v3 = IfThenElseType Bool F
F
FFalse
| Bool
otherwise = Conn -> F -> F -> F
FConn Conn
And (F -> F
simplify F
f1) (F -> F
simplify F
f2)
simplify (FConn Conn
And f1 :: F
f1@(FNot F
v1) f2 :: F
f2@(FConn Conn
Or F
v2 F
v3))
| F
v1 F -> F -> Bool
forall a. Eq a => a -> a -> Bool
P.== F
v2 = F -> F
simplify (Conn -> F -> F -> F
FConn Conn
And (F -> F
FNot F
v1) F
v3)
| F
v1 F -> F -> Bool
forall a. Eq a => a -> a -> Bool
P.== F
v3 = F -> F
simplify (Conn -> F -> F -> F
FConn Conn
And (F -> F
FNot F
v1) F
v2)
| F
v1 F -> F -> Bool
forall a. Eq a => a -> a -> Bool
P.== F
f2 = IfThenElseType Bool F
F
FFalse
| Bool
otherwise = Conn -> F -> F -> F
FConn Conn
And (F -> F
simplify F
f1) (F -> F
simplify F
f2)
simplify (FConn Conn
And F
x1 f2 :: F
f2@(FConn Conn
Impl F
x2 F
y)) = if F
x1 F -> F -> Bool
forall a. Eq a => a -> a -> Bool
P.== F
x2 then F -> F
simplify (Conn -> F -> F -> F
FConn Conn
And F
x1 F
y) else Conn -> F -> F -> F
FConn Conn
And (F -> F
simplify F
x1) (F -> F
simplify F
f2)
simplify (FConn Conn
And f1 :: F
f1@(FConn Conn
Impl F
x1 F
y) F
x2) = if F
x1 F -> F -> Bool
forall a. Eq a => a -> a -> Bool
P.== F
x2 then F -> F
simplify (Conn -> F -> F -> F
FConn Conn
And F
y F
x2) else Conn -> F -> F -> F
FConn Conn
And (F -> F
simplify F
f1) (F -> F
simplify F
x2)
simplify (FConn Conn
And F
f1 fn2 :: F
fn2@(FNot F
f2)) = if F
f1 F -> F -> Bool
forall a. Eq a => a -> a -> Bool
P.== F
f2 then F
FFalse else Conn -> F -> F -> F
FConn Conn
And (F -> F
simplify F
f1) (F -> F
simplify F
fn2)
simplify (FConn Conn
And fn1 :: F
fn1@(FNot F
f1) F
f2) = if F
f1 F -> F -> Bool
forall a. Eq a => a -> a -> Bool
P.== F
f2 then F
FFalse else Conn -> F -> F -> F
FConn Conn
And (F -> F
simplify F
fn1) (F -> F
simplify F
f2)
simplify (FConn Conn
And f1 :: F
f1@(FComp Comp
Ge E
l1 E
r1) f2 :: F
f2@(FComp Comp
Ge E
l2 E
r2)) = if E
l1 E -> E -> Bool
forall a. Eq a => a -> a -> Bool
P.== E
r2 Bool -> Bool -> AndOrType Bool Bool
forall a b. CanAndOrAsymmetric a b => a -> b -> AndOrType a b
&& E
l2 E -> E -> Bool
forall a. Eq a => a -> a -> Bool
P.== E
r1 then F -> F
simplify (Comp -> E -> E -> F
FComp Comp
Eq E
l1 E
r1) else Conn -> F -> F -> F
FConn Conn
And (F -> F
simplify F
f1) (F -> F
simplify F
f2)
simplify (FConn Conn
And f1 :: F
f1@(FComp Comp
Le E
l1 E
r1) f2 :: F
f2@(FComp Comp
Le E
l2 E
r2)) = if E
l1 E -> E -> Bool
forall a. Eq a => a -> a -> Bool
P.== E
r2 Bool -> Bool -> AndOrType Bool Bool
forall a b. CanAndOrAsymmetric a b => a -> b -> AndOrType a b
&& E
l2 E -> E -> Bool
forall a. Eq a => a -> a -> Bool
P.== E
r1 then F -> F
simplify (Comp -> E -> E -> F
FComp Comp
Eq E
l1 E
r1) else Conn -> F -> F -> F
FConn Conn
And (F -> F
simplify F
f1) (F -> F
simplify F
f2)
simplify (FConn Conn
And f1 :: F
f1@(FComp Comp
Ge E
l1 E
r1) f2 :: F
f2@(FComp Comp
Le E
l2 E
r2)) = if E
l1 E -> E -> Bool
forall a. Eq a => a -> a -> Bool
P.== E
l2 Bool -> Bool -> AndOrType Bool Bool
forall a b. CanAndOrAsymmetric a b => a -> b -> AndOrType a b
&& E
r1 E -> E -> Bool
forall a. Eq a => a -> a -> Bool
P.== E
r2 then F -> F
simplify (Comp -> E -> E -> F
FComp Comp
Eq E
l1 E
r1) else Conn -> F -> F -> F
FConn Conn
And (F -> F
simplify F
f1) (F -> F
simplify F
f2)
simplify (FConn Conn
And f1 :: F
f1@(FComp Comp
Le E
l1 E
r1) f2 :: F
f2@(FComp Comp
Ge E
l2 E
r2)) = if E
l1 E -> E -> Bool
forall a. Eq a => a -> a -> Bool
P.== E
l2 Bool -> Bool -> AndOrType Bool Bool
forall a b. CanAndOrAsymmetric a b => a -> b -> AndOrType a b
&& E
r1 E -> E -> Bool
forall a. Eq a => a -> a -> Bool
P.== E
r2 then F -> F
simplify (Comp -> E -> E -> F
FComp Comp
Eq E
l1 E
r1) else Conn -> F -> F -> F
FConn Conn
And (F -> F
simplify F
f1) (F -> F
simplify F
f2)
simplify (FConn Conn
And F
f1 F
f2) = if F
f1 F -> F -> Bool
forall a. Eq a => a -> a -> Bool
P.== F
f2 then F -> F
simplify F
f1 else Conn -> F -> F -> F
FConn Conn
And (F -> F
simplify F
f1) (F -> F
simplify F
f2)
simplify (FConn Conn
Or F
_ F
FTrue) = IfThenElseType Bool F
F
FTrue
simplify (FConn Conn
Or F
FTrue F
_) = IfThenElseType Bool F
F
FTrue
simplify (FConn Conn
Or F
f F
FFalse) = F -> F
simplify F
f
simplify (FConn Conn
Or F
FFalse F
f) = F -> F
simplify F
f
simplify (FConn Conn
Or F
f1 fn2 :: F
fn2@(FNot F
f2)) = if F
f1 F -> F -> Bool
forall a. Eq a => a -> a -> Bool
P.== F
f2 then F
FTrue else Conn -> F -> F -> F
FConn Conn
Or (F -> F
simplify F
f1) (F -> F
simplify F
fn2)
simplify (FConn Conn
Or fn1 :: F
fn1@(FNot F
f1) F
f2) = if F
f1 F -> F -> Bool
forall a. Eq a => a -> a -> Bool
P.== F
f2 then F
FTrue else Conn -> F -> F -> F
FConn Conn
Or (F -> F
simplify F
fn1) (F -> F
simplify F
f2)
simplify (FConn Conn
Or F
f1 F
f2) = if F
f1 F -> F -> Bool
forall a. Eq a => a -> a -> Bool
P.== F
f2 then F -> F
simplify F
f1 else Conn -> F -> F -> F
FConn Conn
Or (F -> F
simplify F
f1) (F -> F
simplify F
f2)
simplify (FConn Conn
Impl F
FFalse F
_) = IfThenElseType Bool F
F
FTrue
simplify (FConn Conn
Impl F
_ F
FTrue) = IfThenElseType Bool F
F
FTrue
simplify (FConn Conn
Impl F
f F
FFalse) = F -> F
simplify (F -> F
FNot F
f)
simplify (FConn Conn
Impl F
FTrue F
f) = F -> F
simplify F
f
simplify (FConn Conn
Impl F
f1 fn2 :: F
fn2@(FNot F
f2)) = if F
f1 F -> F -> Bool
forall a. Eq a => a -> a -> Bool
P.== F
f2 then F -> F
simplify (F -> F
FNot F
f1) else Conn -> F -> F -> F
FConn Conn
Impl (F -> F
simplify F
f1) (F -> F
simplify F
fn2)
simplify (FConn Conn
Impl fn1 :: F
fn1@(FNot F
f1) F
f2) = if F
f1 F -> F -> Bool
forall a. Eq a => a -> a -> Bool
P.== F
f2 then F -> F
simplify F
f1 else Conn -> F -> F -> F
FConn Conn
Impl (F -> F
simplify F
fn1) (F -> F
simplify F
f2)
simplify (FConn Conn
Impl F
f1 F
f2) = if F
f1 F -> F -> Bool
forall a. Eq a => a -> a -> Bool
P.== F
f2 then F
FTrue else Conn -> F -> F -> F
FConn Conn
Impl (F -> F
simplify F
f1) (F -> F
simplify F
f2)
simplify (FComp Comp
op (Lit Rational
l1) (Lit Rational
l2)) =
case Comp
op of
Comp
Gt -> Bool -> F
boolToF (Bool -> F) -> Bool -> F
forall a b. (a -> b) -> a -> b
$ Rational
l1 Rational -> Rational -> OrderCompareType Rational Rational
forall a b.
HasOrderAsymmetric a b =>
a -> b -> OrderCompareType a b
> Rational
l2
Comp
Ge -> Bool -> F
boolToF (Bool -> F) -> Bool -> F
forall a b. (a -> b) -> a -> b
$ Rational
l1 Rational -> Rational -> OrderCompareType Rational Rational
forall a b.
HasOrderAsymmetric a b =>
a -> b -> OrderCompareType a b
>= Rational
l2
Comp
Lt -> Bool -> F
boolToF (Bool -> F) -> Bool -> F
forall a b. (a -> b) -> a -> b
$ Rational
l1 Rational -> Rational -> OrderCompareType Rational Rational
forall a b.
HasOrderAsymmetric a b =>
a -> b -> OrderCompareType a b
< Rational
l2
Comp
Le -> Bool -> F
boolToF (Bool -> F) -> Bool -> F
forall a b. (a -> b) -> a -> b
$ Rational
l1 Rational -> Rational -> OrderCompareType Rational Rational
forall a b.
HasOrderAsymmetric a b =>
a -> b -> OrderCompareType a b
<= Rational
l2
Comp
Eq -> Bool -> F
boolToF (Bool -> F) -> Bool -> F
forall a b. (a -> b) -> a -> b
$ Rational
l1 Rational -> Rational -> EqCompareType Rational Rational
forall a b. HasEqAsymmetric a b => a -> b -> EqCompareType a b
== Rational
l2
where
boolToF :: Bool -> F
boolToF Bool
True = F
FTrue
boolToF Bool
False = F
FFalse
simplify (FNot (FNot F
f)) = F -> F
simplify F
f
simplify (FComp Comp
Eq E
e1 E
e2) = if E
e1 E -> E -> Bool
forall a. Eq a => a -> a -> Bool
P.== E
e2 Bool -> Bool -> AndOrType Bool Bool
forall a b. CanAndOrAsymmetric a b => a -> b -> AndOrType a b
|| E -> E
simplifyE E
e1 E -> E -> Bool
forall a. Eq a => a -> a -> Bool
P.== E -> E
simplifyE E
e2 then F
FTrue else Comp -> E -> E -> F
FComp Comp
Eq (E -> E
simplifyE E
e1) (E -> E
simplifyE E
e2)
simplify (FComp Comp
op E
e1 E
e2) = Comp -> E -> E -> F
FComp Comp
op (E -> E
simplifyE E
e1) (E -> E
simplifyE E
e2)
simplify F
FTrue = IfThenElseType Bool F
F
FTrue
simplify F
FFalse = IfThenElseType Bool F
F
FFalse
simplify (FNot F
FTrue) = IfThenElseType Bool F
F
FFalse
simplify (FNot F
FFalse) = IfThenElseType Bool F
F
FTrue
simplify (FNot F
f) = F -> F
FNot (F -> F
simplify F
f)
simplifyEDoubleList :: [[E]] -> [[E]]
simplifyEDoubleList :: [[E]] -> [[E]]
simplifyEDoubleList = [[E]] -> [[E]]
forall a. Eq a => [a] -> [a]
nub ([[E]] -> [[E]]) -> ([[E]] -> [[E]]) -> [[E]] -> [[E]]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ([E] -> [E]) -> [[E]] -> [[E]]
forall a b. (a -> b) -> [a] -> [b]
map ([E] -> [E]
forall a. Eq a => [a] -> [a]
nub ([E] -> [E]) -> ([E] -> [E]) -> [E] -> [E]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (E -> E) -> [E] -> [E]
forall a b. (a -> b) -> [a] -> [b]
map E -> E
simplifyE)
simplifyFDNF :: [[F]] -> [[F]]
simplifyFDNF :: [[F]] -> [[F]]
simplifyFDNF [] = []
simplifyFDNF ([F]
c : [[F]]
cs) =
case [F] -> Maybe [F]
simplifyFConjunction [F]
c of
Maybe [F]
Nothing -> [[F]] -> [[F]]
simplifyFDNF [[F]]
cs
Just [] -> [[F]] -> [[F]]
simplifyFDNF [[F]]
cs
Just [F
checkedConjunctionHead] -> [F
checkedConjunctionHead] [F] -> [[F]] -> [[F]]
forall a. a -> [a] -> [a]
: [[F]] -> [[F]]
simplifyFDNF [[F]]
cs
Just checkedConjunction :: [F]
checkedConjunction@(F
checkedConjunctionHead : [F]
checkedConjunctionTail) ->
let
currentEqualities :: [(E, E)]
currentEqualities = F -> [F] -> [F] -> [(E, E)]
findEqualities F
checkedConjunctionHead [F]
checkedConjunctionTail [F]
checkedConjunctionTail
in
case [(E, E)]
currentEqualities of
[] -> [F]
checkedConjunction [F] -> [[F]] -> [[F]]
forall a. a -> [a] -> [a]
: [[F]] -> [[F]]
simplifyFDNF [[F]]
cs
[(E, E)
_eq1] -> [F]
checkedConjunction [F] -> [[F]] -> [[F]]
forall a. a -> [a] -> [a]
: [[F]] -> [[F]]
simplifyFDNF [[F]]
cs
((E, E)
currentEqualitiesHead : [(E, E)]
currentEqualitiesTail) ->
let
newEqualities :: [F]
newEqualities = (E, E) -> [(E, E)] -> [(E, E)] -> [F]
findEqZero (E, E)
currentEqualitiesHead [(E, E)]
currentEqualitiesTail [(E, E)]
currentEqualitiesTail
in
[F] -> [F]
forall a. Eq a => [a] -> [a]
nub ([F]
checkedConjunction [F] -> [F] -> [F]
forall a. [a] -> [a] -> [a]
++ [F]
newEqualities) [F] -> [[F]] -> [[F]]
forall a. a -> [a] -> [a]
: [[F]] -> [[F]]
simplifyFDNF [[F]]
cs
where
findEqZero :: (E,E) -> [(E,E)] -> [(E,E)] -> [F]
findEqZero :: (E, E) -> [(E, E)] -> [(E, E)] -> [F]
findEqZero (E, E)
_ [] [] = []
findEqZero (E, E)
_ [] ((E, E)
eq : [(E, E)]
conj) = (E, E) -> [(E, E)] -> [(E, E)] -> [F]
findEqZero (E, E)
eq [(E, E)]
conj [(E, E)]
conj
findEqZero (E, E)
eq1 ((E, E)
eq2 : [(E, E)]
eqs) [(E, E)]
conj =
case (E, E)
eq1 of
(EUnOp UnOp
Negate E
l1, EUnOp UnOp
Negate E
r1) ->
case (E, E)
eq2 of
(EUnOp UnOp
Negate E
l2, E
r2)
| E
l1 E -> E -> Bool
forall a. Eq a => a -> a -> Bool
P.== E
l2 Bool -> Bool -> AndOrType Bool Bool
forall a b. CanAndOrAsymmetric a b => a -> b -> AndOrType a b
&& E
r1 E -> E -> Bool
forall a. Eq a => a -> a -> Bool
P.== E
r2 -> [Comp -> E -> E -> F
FComp Comp
Ge E
l1 (Rational -> E
Lit Rational
0.0), Comp -> E -> E -> F
FComp Comp
Ge (Rational -> E
Lit Rational
0.0) E
l1, Comp -> E -> E -> F
FComp Comp
Ge E
r1 (Rational -> E
Lit Rational
0.0), Comp -> E -> E -> F
FComp Comp
Ge (Rational -> E
Lit Rational
0.0) E
r1] [F] -> [F] -> [F]
forall a. [a] -> [a] -> [a]
++ (E, E) -> [(E, E)] -> [(E, E)] -> [F]
findEqZero (E, E)
eq1 [(E, E)]
eqs [(E, E)]
conj
| E
l1 E -> E -> Bool
forall a. Eq a => a -> a -> Bool
P.== E
r2 Bool -> Bool -> AndOrType Bool Bool
forall a b. CanAndOrAsymmetric a b => a -> b -> AndOrType a b
&& E
r1 E -> E -> Bool
forall a. Eq a => a -> a -> Bool
P.== E
l2 -> [Comp -> E -> E -> F
FComp Comp
Ge E
l1 (Rational -> E
Lit Rational
0.0), Comp -> E -> E -> F
FComp Comp
Ge (Rational -> E
Lit Rational
0.0) E
l1, Comp -> E -> E -> F
FComp Comp
Ge E
r1 (Rational -> E
Lit Rational
0.0), Comp -> E -> E -> F
FComp Comp
Ge (Rational -> E
Lit Rational
0.0) E
r1] [F] -> [F] -> [F]
forall a. [a] -> [a] -> [a]
++ (E, E) -> [(E, E)] -> [(E, E)] -> [F]
findEqZero (E, E)
eq1 [(E, E)]
eqs [(E, E)]
conj
| Bool
otherwise -> (E, E) -> [(E, E)] -> [(E, E)] -> [F]
findEqZero (E, E)
eq1 [(E, E)]
eqs [(E, E)]
conj
(E
l2, EUnOp UnOp
Negate E
r2)
| E
l1 E -> E -> Bool
forall a. Eq a => a -> a -> Bool
P.== E
l2 Bool -> Bool -> AndOrType Bool Bool
forall a b. CanAndOrAsymmetric a b => a -> b -> AndOrType a b
&& E
r1 E -> E -> Bool
forall a. Eq a => a -> a -> Bool
P.== E
r2 -> [Comp -> E -> E -> F
FComp Comp
Ge E
l1 (Rational -> E
Lit Rational
0.0), Comp -> E -> E -> F
FComp Comp
Ge (Rational -> E
Lit Rational
0.0) E
l1, Comp -> E -> E -> F
FComp Comp
Ge E
r1 (Rational -> E
Lit Rational
0.0), Comp -> E -> E -> F
FComp Comp
Ge (Rational -> E
Lit Rational
0.0) E
r1] [F] -> [F] -> [F]
forall a. [a] -> [a] -> [a]
++ (E, E) -> [(E, E)] -> [(E, E)] -> [F]
findEqZero (E, E)
eq1 [(E, E)]
eqs [(E, E)]
conj
| E
l1 E -> E -> Bool
forall a. Eq a => a -> a -> Bool
P.== E
r2 Bool -> Bool -> AndOrType Bool Bool
forall a b. CanAndOrAsymmetric a b => a -> b -> AndOrType a b
&& E
r1 E -> E -> Bool
forall a. Eq a => a -> a -> Bool
P.== E
l2 -> [Comp -> E -> E -> F
FComp Comp
Ge E
l1 (Rational -> E
Lit Rational
0.0), Comp -> E -> E -> F
FComp Comp
Ge (Rational -> E
Lit Rational
0.0) E
l1, Comp -> E -> E -> F
FComp Comp
Ge E
r1 (Rational -> E
Lit Rational
0.0), Comp -> E -> E -> F
FComp Comp
Ge (Rational -> E
Lit Rational
0.0) E
r1] [F] -> [F] -> [F]
forall a. [a] -> [a] -> [a]
++ (E, E) -> [(E, E)] -> [(E, E)] -> [F]
findEqZero (E, E)
eq1 [(E, E)]
eqs [(E, E)]
conj
| Bool
otherwise -> (E, E) -> [(E, E)] -> [(E, E)] -> [F]
findEqZero (E, E)
eq1 [(E, E)]
eqs [(E, E)]
conj
(E, E)
_ -> (E, E) -> [(E, E)] -> [(E, E)] -> [F]
findEqZero (E, E)
eq1 [(E, E)]
eqs [(E, E)]
conj
(EUnOp UnOp
Negate E
l1, E
r1) ->
case (E, E)
eq2 of
(EUnOp UnOp
Negate E
l2, EUnOp UnOp
Negate E
r2)
| E
l1 E -> E -> Bool
forall a. Eq a => a -> a -> Bool
P.== E
l2 Bool -> Bool -> AndOrType Bool Bool
forall a b. CanAndOrAsymmetric a b => a -> b -> AndOrType a b
&& E
r1 E -> E -> Bool
forall a. Eq a => a -> a -> Bool
P.== E
r2 -> [Comp -> E -> E -> F
FComp Comp
Ge E
l1 (Rational -> E
Lit Rational
0.0), Comp -> E -> E -> F
FComp Comp
Ge (Rational -> E
Lit Rational
0.0) E
l1, Comp -> E -> E -> F
FComp Comp
Ge E
r1 (Rational -> E
Lit Rational
0.0), Comp -> E -> E -> F
FComp Comp
Ge (Rational -> E
Lit Rational
0.0) E
r1] [F] -> [F] -> [F]
forall a. [a] -> [a] -> [a]
++ (E, E) -> [(E, E)] -> [(E, E)] -> [F]
findEqZero (E, E)
eq1 [(E, E)]
eqs [(E, E)]
conj
| E
l1 E -> E -> Bool
forall a. Eq a => a -> a -> Bool
P.== E
r2 Bool -> Bool -> AndOrType Bool Bool
forall a b. CanAndOrAsymmetric a b => a -> b -> AndOrType a b
&& E
r1 E -> E -> Bool
forall a. Eq a => a -> a -> Bool
P.== E
l2 -> [Comp -> E -> E -> F
FComp Comp
Ge E
l1 (Rational -> E
Lit Rational
0.0), Comp -> E -> E -> F
FComp Comp
Ge (Rational -> E
Lit Rational
0.0) E
l1, Comp -> E -> E -> F
FComp Comp
Ge E
r1 (Rational -> E
Lit Rational
0.0), Comp -> E -> E -> F
FComp Comp
Ge (Rational -> E
Lit Rational
0.0) E
r1] [F] -> [F] -> [F]
forall a. [a] -> [a] -> [a]
++ (E, E) -> [(E, E)] -> [(E, E)] -> [F]
findEqZero (E, E)
eq1 [(E, E)]
eqs [(E, E)]
conj
| Bool
otherwise -> (E, E) -> [(E, E)] -> [(E, E)] -> [F]
findEqZero (E, E)
eq1 [(E, E)]
eqs [(E, E)]
conj
(E
l2, E
r2)
| E
l1 E -> E -> Bool
forall a. Eq a => a -> a -> Bool
P.== E
l2 Bool -> Bool -> AndOrType Bool Bool
forall a b. CanAndOrAsymmetric a b => a -> b -> AndOrType a b
&& E
r1 E -> E -> Bool
forall a. Eq a => a -> a -> Bool
P.== E
r2 -> [Comp -> E -> E -> F
FComp Comp
Ge E
l1 (Rational -> E
Lit Rational
0.0), Comp -> E -> E -> F
FComp Comp
Ge (Rational -> E
Lit Rational
0.0) E
l1, Comp -> E -> E -> F
FComp Comp
Ge E
r1 (Rational -> E
Lit Rational
0.0), Comp -> E -> E -> F
FComp Comp
Ge (Rational -> E
Lit Rational
0.0) E
r1] [F] -> [F] -> [F]
forall a. [a] -> [a] -> [a]
++ (E, E) -> [(E, E)] -> [(E, E)] -> [F]
findEqZero (E, E)
eq1 [(E, E)]
eqs [(E, E)]
conj
| E
l1 E -> E -> Bool
forall a. Eq a => a -> a -> Bool
P.== E
r2 Bool -> Bool -> AndOrType Bool Bool
forall a b. CanAndOrAsymmetric a b => a -> b -> AndOrType a b
&& E
r1 E -> E -> Bool
forall a. Eq a => a -> a -> Bool
P.== E
l2 -> [Comp -> E -> E -> F
FComp Comp
Ge E
l1 (Rational -> E
Lit Rational
0.0), Comp -> E -> E -> F
FComp Comp
Ge (Rational -> E
Lit Rational
0.0) E
l1, Comp -> E -> E -> F
FComp Comp
Ge E
r1 (Rational -> E
Lit Rational
0.0), Comp -> E -> E -> F
FComp Comp
Ge (Rational -> E
Lit Rational
0.0) E
r1] [F] -> [F] -> [F]
forall a. [a] -> [a] -> [a]
++ (E, E) -> [(E, E)] -> [(E, E)] -> [F]
findEqZero (E, E)
eq1 [(E, E)]
eqs [(E, E)]
conj
| Bool
otherwise -> (E, E) -> [(E, E)] -> [(E, E)] -> [F]
findEqZero (E, E)
eq1 [(E, E)]
eqs [(E, E)]
conj
(E
l1, EUnOp UnOp
Negate E
r1) ->
case (E, E)
eq2 of
(EUnOp UnOp
Negate E
l2, EUnOp UnOp
Negate E
r2)
| E
l1 E -> E -> Bool
forall a. Eq a => a -> a -> Bool
P.== E
l2 Bool -> Bool -> AndOrType Bool Bool
forall a b. CanAndOrAsymmetric a b => a -> b -> AndOrType a b
&& E
r1 E -> E -> Bool
forall a. Eq a => a -> a -> Bool
P.== E
r2 -> [Comp -> E -> E -> F
FComp Comp
Ge E
l1 (Rational -> E
Lit Rational
0.0), Comp -> E -> E -> F
FComp Comp
Ge (Rational -> E
Lit Rational
0.0) E
l1, Comp -> E -> E -> F
FComp Comp
Ge E
r1 (Rational -> E
Lit Rational
0.0), Comp -> E -> E -> F
FComp Comp
Ge (Rational -> E
Lit Rational
0.0) E
r1] [F] -> [F] -> [F]
forall a. [a] -> [a] -> [a]
++ (E, E) -> [(E, E)] -> [(E, E)] -> [F]
findEqZero (E, E)
eq1 [(E, E)]
eqs [(E, E)]
conj
| E
l1 E -> E -> Bool
forall a. Eq a => a -> a -> Bool
P.== E
r2 Bool -> Bool -> AndOrType Bool Bool
forall a b. CanAndOrAsymmetric a b => a -> b -> AndOrType a b
&& E
r1 E -> E -> Bool
forall a. Eq a => a -> a -> Bool
P.== E
l2 -> [Comp -> E -> E -> F
FComp Comp
Ge E
l1 (Rational -> E
Lit Rational
0.0), Comp -> E -> E -> F
FComp Comp
Ge (Rational -> E
Lit Rational
0.0) E
l1, Comp -> E -> E -> F
FComp Comp
Ge E
r1 (Rational -> E
Lit Rational
0.0), Comp -> E -> E -> F
FComp Comp
Ge (Rational -> E
Lit Rational
0.0) E
r1] [F] -> [F] -> [F]
forall a. [a] -> [a] -> [a]
++ (E, E) -> [(E, E)] -> [(E, E)] -> [F]
findEqZero (E, E)
eq1 [(E, E)]
eqs [(E, E)]
conj
| Bool
otherwise -> (E, E) -> [(E, E)] -> [(E, E)] -> [F]
findEqZero (E, E)
eq1 [(E, E)]
eqs [(E, E)]
conj
(E
l2, E
r2)
| E
l1 E -> E -> Bool
forall a. Eq a => a -> a -> Bool
P.== E
l2 Bool -> Bool -> AndOrType Bool Bool
forall a b. CanAndOrAsymmetric a b => a -> b -> AndOrType a b
&& E
r1 E -> E -> Bool
forall a. Eq a => a -> a -> Bool
P.== E
r2 -> [Comp -> E -> E -> F
FComp Comp
Ge E
l1 (Rational -> E
Lit Rational
0.0), Comp -> E -> E -> F
FComp Comp
Ge (Rational -> E
Lit Rational
0.0) E
l1, Comp -> E -> E -> F
FComp Comp
Ge E
r1 (Rational -> E
Lit Rational
0.0), Comp -> E -> E -> F
FComp Comp
Ge (Rational -> E
Lit Rational
0.0) E
r1] [F] -> [F] -> [F]
forall a. [a] -> [a] -> [a]
++ (E, E) -> [(E, E)] -> [(E, E)] -> [F]
findEqZero (E, E)
eq1 [(E, E)]
eqs [(E, E)]
conj
| E
l1 E -> E -> Bool
forall a. Eq a => a -> a -> Bool
P.== E
r2 Bool -> Bool -> AndOrType Bool Bool
forall a b. CanAndOrAsymmetric a b => a -> b -> AndOrType a b
&& E
r1 E -> E -> Bool
forall a. Eq a => a -> a -> Bool
P.== E
l2 -> [Comp -> E -> E -> F
FComp Comp
Ge E
l1 (Rational -> E
Lit Rational
0.0), Comp -> E -> E -> F
FComp Comp
Ge (Rational -> E
Lit Rational
0.0) E
l1, Comp -> E -> E -> F
FComp Comp
Ge E
r1 (Rational -> E
Lit Rational
0.0), Comp -> E -> E -> F
FComp Comp
Ge (Rational -> E
Lit Rational
0.0) E
r1] [F] -> [F] -> [F]
forall a. [a] -> [a] -> [a]
++ (E, E) -> [(E, E)] -> [(E, E)] -> [F]
findEqZero (E, E)
eq1 [(E, E)]
eqs [(E, E)]
conj
| Bool
otherwise -> (E, E) -> [(E, E)] -> [(E, E)] -> [F]
findEqZero (E, E)
eq1 [(E, E)]
eqs [(E, E)]
conj
(E
l1, E
r1) ->
case (E, E)
eq2 of
(E
l2, EUnOp UnOp
Negate E
r2)
| E
l1 E -> E -> Bool
forall a. Eq a => a -> a -> Bool
P.== E
l2 Bool -> Bool -> AndOrType Bool Bool
forall a b. CanAndOrAsymmetric a b => a -> b -> AndOrType a b
&& E
r1 E -> E -> Bool
forall a. Eq a => a -> a -> Bool
P.== E
r2 -> [Comp -> E -> E -> F
FComp Comp
Ge E
l1 (Rational -> E
Lit Rational
0.0), Comp -> E -> E -> F
FComp Comp
Ge (Rational -> E
Lit Rational
0.0) E
l1, Comp -> E -> E -> F
FComp Comp
Ge E
r1 (Rational -> E
Lit Rational
0.0), Comp -> E -> E -> F
FComp Comp
Ge (Rational -> E
Lit Rational
0.0) E
r1] [F] -> [F] -> [F]
forall a. [a] -> [a] -> [a]
++ (E, E) -> [(E, E)] -> [(E, E)] -> [F]
findEqZero (E, E)
eq1 [(E, E)]
eqs [(E, E)]
conj
| E
l1 E -> E -> Bool
forall a. Eq a => a -> a -> Bool
P.== E
r2 Bool -> Bool -> AndOrType Bool Bool
forall a b. CanAndOrAsymmetric a b => a -> b -> AndOrType a b
&& E
r1 E -> E -> Bool
forall a. Eq a => a -> a -> Bool
P.== E
l2 -> [Comp -> E -> E -> F
FComp Comp
Ge E
l1 (Rational -> E
Lit Rational
0.0), Comp -> E -> E -> F
FComp Comp
Ge (Rational -> E
Lit Rational
0.0) E
l1, Comp -> E -> E -> F
FComp Comp
Ge E
r1 (Rational -> E
Lit Rational
0.0), Comp -> E -> E -> F
FComp Comp
Ge (Rational -> E
Lit Rational
0.0) E
r1] [F] -> [F] -> [F]
forall a. [a] -> [a] -> [a]
++ (E, E) -> [(E, E)] -> [(E, E)] -> [F]
findEqZero (E, E)
eq1 [(E, E)]
eqs [(E, E)]
conj
| Bool
otherwise -> (E, E) -> [(E, E)] -> [(E, E)] -> [F]
findEqZero (E, E)
eq1 [(E, E)]
eqs [(E, E)]
conj
(EUnOp UnOp
Negate E
l2, E
r2)
| E
l1 E -> E -> Bool
forall a. Eq a => a -> a -> Bool
P.== E
l2 Bool -> Bool -> AndOrType Bool Bool
forall a b. CanAndOrAsymmetric a b => a -> b -> AndOrType a b
&& E
r1 E -> E -> Bool
forall a. Eq a => a -> a -> Bool
P.== E
r2 -> [Comp -> E -> E -> F
FComp Comp
Ge E
l1 (Rational -> E
Lit Rational
0.0), Comp -> E -> E -> F
FComp Comp
Ge (Rational -> E
Lit Rational
0.0) E
l1, Comp -> E -> E -> F
FComp Comp
Ge E
r1 (Rational -> E
Lit Rational
0.0), Comp -> E -> E -> F
FComp Comp
Ge (Rational -> E
Lit Rational
0.0) E
r1] [F] -> [F] -> [F]
forall a. [a] -> [a] -> [a]
++ (E, E) -> [(E, E)] -> [(E, E)] -> [F]
findEqZero (E, E)
eq1 [(E, E)]
eqs [(E, E)]
conj
| E
l1 E -> E -> Bool
forall a. Eq a => a -> a -> Bool
P.== E
r2 Bool -> Bool -> AndOrType Bool Bool
forall a b. CanAndOrAsymmetric a b => a -> b -> AndOrType a b
&& E
r1 E -> E -> Bool
forall a. Eq a => a -> a -> Bool
P.== E
l2 -> [Comp -> E -> E -> F
FComp Comp
Ge E
l1 (Rational -> E
Lit Rational
0.0), Comp -> E -> E -> F
FComp Comp
Ge (Rational -> E
Lit Rational
0.0) E
l1, Comp -> E -> E -> F
FComp Comp
Ge E
r1 (Rational -> E
Lit Rational
0.0), Comp -> E -> E -> F
FComp Comp
Ge (Rational -> E
Lit Rational
0.0) E
r1] [F] -> [F] -> [F]
forall a. [a] -> [a] -> [a]
++ (E, E) -> [(E, E)] -> [(E, E)] -> [F]
findEqZero (E, E)
eq1 [(E, E)]
eqs [(E, E)]
conj
| Bool
otherwise -> (E, E) -> [(E, E)] -> [(E, E)] -> [F]
findEqZero (E, E)
eq1 [(E, E)]
eqs [(E, E)]
conj
(E, E)
_ -> (E, E) -> [(E, E)] -> [(E, E)] -> [F]
findEqZero (E, E)
eq1 [(E, E)]
eqs [(E, E)]
conj
findEqualities :: F -> [F] -> [F] -> [(E, E)]
findEqualities :: F -> [F] -> [F] -> [(E, E)]
findEqualities F
_ [] [] = []
findEqualities F
_ [] (F
f : [F]
conj) = F -> [F] -> [F] -> [(E, E)]
findEqualities F
f [F]
conj [F]
conj
findEqualities F
f1 (F
f2 : [F]
fs) [F]
conj =
case F
f1 of
FComp Comp
Ge E
l1 E
r1 ->
case F
f2 of
FComp Comp
Ge E
l2 E
r2 ->
if E
l1 E -> E -> Bool
forall a. Eq a => a -> a -> Bool
P.== E
r2 Bool -> Bool -> AndOrType Bool Bool
forall a b. CanAndOrAsymmetric a b => a -> b -> AndOrType a b
&& E
r1 E -> E -> Bool
forall a. Eq a => a -> a -> Bool
P.== E
l2
then (E
l1, E
r1) (E, E) -> [(E, E)] -> [(E, E)]
forall a. a -> [a] -> [a]
: F -> [F] -> [F] -> [(E, E)]
findEqualities F
f1 [F]
fs [F]
conj
else F -> [F] -> [F] -> [(E, E)]
findEqualities F
f1 [F]
fs [F]
conj
F
_ -> F -> [F] -> [F] -> [(E, E)]
findEqualities F
f1 [F]
fs [F]
conj
F
_ -> F -> [F] -> [F] -> [(E, E)]
findEqualities F
f1 [F]
fs [F]
conj
simplifyFConjunction :: [F] -> Maybe [F]
simplifyFConjunction :: [F] -> Maybe [F]
simplifyFConjunction [] = [F] -> Maybe [F]
forall a. a -> Maybe a
Just []
simplifyFConjunction (F
simplifiedConjunctionHead : [F]
simplifiedConjunctionTail) =
let
removeContradictions :: F -> [F] -> [F] -> Maybe [F]
removeContradictions :: F -> [F] -> [F] -> Maybe [F]
removeContradictions F
f1 [] [] = [F] -> Maybe [F]
forall a. a -> Maybe a
Just [F
f1]
removeContradictions F
f1 [] (F
f : [F]
conj) = (F
f1 F -> [F] -> [F]
forall a. a -> [a] -> [a]
:) ([F] -> [F]) -> Maybe [F] -> Maybe [F]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> F -> [F] -> [F] -> Maybe [F]
removeContradictions F
f [F]
conj [F]
conj
removeContradictions F
f1 (F
f2 : [F]
fs) [F]
conj =
case F
f1 of
FComp Comp
Ge E
l1 E
r1 ->
case F
f2 of
FComp Comp
Gt E
l2 E
r2 ->
if E
l1 E -> E -> Bool
forall a. Eq a => a -> a -> Bool
P.== E
r2 Bool -> Bool -> AndOrType Bool Bool
forall a b. CanAndOrAsymmetric a b => a -> b -> AndOrType a b
&& E
r1 E -> E -> Bool
forall a. Eq a => a -> a -> Bool
P.== E
l2 then Maybe [F]
forall a. Maybe a
Nothing else F -> [F] -> [F] -> Maybe [F]
removeContradictions F
f1 [F]
fs [F]
conj
F
_ -> F -> [F] -> [F] -> Maybe [F]
removeContradictions F
f1 [F]
fs [F]
conj
FComp Comp
Gt E
l1 E
r1 ->
case F
f2 of
FComp Comp
Ge E
l2 E
r2 ->
if E
l1 E -> E -> Bool
forall a. Eq a => a -> a -> Bool
P.== E
r2 Bool -> Bool -> AndOrType Bool Bool
forall a b. CanAndOrAsymmetric a b => a -> b -> AndOrType a b
&& E
r1 E -> E -> Bool
forall a. Eq a => a -> a -> Bool
P.== E
l2 then Maybe [F]
forall a. Maybe a
Nothing else F -> [F] -> [F] -> Maybe [F]
removeContradictions F
f1 [F]
fs [F]
conj
FComp Comp
Gt E
l2 E
r2 ->
if E
l1 E -> E -> Bool
forall a. Eq a => a -> a -> Bool
P.== E
r2 Bool -> Bool -> AndOrType Bool Bool
forall a b. CanAndOrAsymmetric a b => a -> b -> AndOrType a b
&& E
r1 E -> E -> Bool
forall a. Eq a => a -> a -> Bool
P.== E
l2 then Maybe [F]
forall a. Maybe a
Nothing else F -> [F] -> [F] -> Maybe [F]
removeContradictions F
f1 [F]
fs [F]
conj
F
_ -> F -> [F] -> [F] -> Maybe [F]
removeContradictions F
f1 [F]
fs [F]
conj
F
_ -> F -> [F] -> [F] -> Maybe [F]
removeContradictions F
f1 [F]
fs [F]
conj
in
[F] -> [F]
forall a. Eq a => [a] -> [a]
nub ([F] -> [F]) -> Maybe [F] -> Maybe [F]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> F -> [F] -> [F] -> Maybe [F]
removeContradictions F
simplifiedConjunctionHead [F]
simplifiedConjunctionTail [F]
simplifiedConjunctionTail
fDNFToFDNFWithoutEq :: [[F]] -> [[F]] -> [[F]]
fDNFToFDNFWithoutEq :: [[F]] -> [[F]] -> [[F]]
fDNFToFDNFWithoutEq [] [[F]]
dnf = [[F]]
dnf
fDNFToFDNFWithoutEq ([F]
c : [[F]]
cs) [[F]]
dnf =
case Maybe [[F]]
mNewDNF of
Just [[F]]
newDNF -> [[F]] -> [[F]] -> [[F]]
fDNFToFDNFWithoutEq [[F]]
newDNF []
Maybe [[F]]
Nothing -> [[F]] -> [[F]] -> [[F]]
fDNFToFDNFWithoutEq [[F]]
cs ([F]
cWithoutEq [F] -> [[F]] -> [[F]]
forall a. a -> [a] -> [a]
: [[F]]
dnf)
where
cWithoutEq :: [F]
cWithoutEq = Bool -> [F] -> [F]
elimEq Bool
False [F]
c
mNewDNF :: Maybe [[F]]
mNewDNF = [F] -> Maybe [[F]]
elimNotEq [F]
cWithoutEq
elimNotEq :: [F] -> Maybe [[F]]
elimNotEq [] = Maybe [[F]]
forall a. Maybe a
Nothing
elimNotEq (f :: F
f@(FNot (FComp Comp
Eq E
e1 E
e2)) : [F]
_) = [[F]] -> Maybe [[F]]
forall a. a -> Maybe a
Just [[F]]
newDNF
where
currentDNF :: [[F]]
currentDNF = [F]
c [F] -> [[F]] -> [[F]]
forall a. a -> [a] -> [a]
: [[F]]
cs [[F]] -> [[F]] -> [[F]]
forall a. [a] -> [a] -> [a]
++ [[F]]
dnf
currentDNFWithoutF :: [[F]]
currentDNFWithoutF = ([F] -> [F]) -> [[F]] -> [[F]]
forall a b. (a -> b) -> [a] -> [b]
map (F -> [F] -> [F]
forall a. Eq a => a -> [a] -> [a]
delete F
f) [[F]]
currentDNF
newF1 :: F
newF1 = F -> F
FNot (Comp -> E -> E -> F
FComp Comp
Ge E
e1 E
e2)
newF2 :: F
newF2 = F -> F
FNot (Comp -> E -> E -> F
FComp Comp
Ge E
e2 E
e1)
newDNF :: [[F]]
newDNF = ([F] -> [F]) -> [[F]] -> [[F]]
forall a b. (a -> b) -> [a] -> [b]
map (F
newF1 F -> [F] -> [F]
forall a. a -> [a] -> [a]
:) [[F]]
currentDNFWithoutF [[F]] -> [[F]] -> [[F]]
forall a. [a] -> [a] -> [a]
++ ([F] -> [F]) -> [[F]] -> [[F]]
forall a b. (a -> b) -> [a] -> [b]
map (F
newF2 F -> [F] -> [F]
forall a. a -> [a] -> [a]
:) [[F]]
currentDNFWithoutF
elimNotEq (F
_ : [F]
fs) = [F] -> Maybe [[F]]
elimNotEq [F]
fs
elimEq :: Bool -> [F] -> [F]
elimEq Bool
_ [] = []
elimEq Bool
isNegated (FNot F
f : [F]
fs) = Bool -> [F] -> [F]
elimEq (Bool -> NegType Bool
forall t. CanNeg t => t -> NegType t
not Bool
isNegated) (F
f F -> [F] -> [F]
forall a. a -> [a] -> [a]
: [F]
fs)
elimEq Bool
False (FComp Comp
Eq E
e1 E
e2 : [F]
fs) = Comp -> E -> E -> F
FComp Comp
Ge E
e1 E
e2 F -> [F] -> [F]
forall a. a -> [a] -> [a]
: Comp -> E -> E -> F
FComp Comp
Ge E
e2 E
e1 F -> [F] -> [F]
forall a. a -> [a] -> [a]
: Bool -> [F] -> [F]
elimEq Bool
False [F]
fs
elimEq Bool
True (F
f : [F]
fs) = F -> F
FNot F
f F -> [F] -> [F]
forall a. a -> [a] -> [a]
: Bool -> [F] -> [F]
elimEq Bool
False [F]
fs
elimEq Bool
False (F
f : [F]
fs) = F
f F -> [F] -> [F]
forall a. a -> [a] -> [a]
: Bool -> [F] -> [F]
elimEq Bool
False [F]
fs
fDNFToEDNF :: [[F]] -> [[ESafe]]
fDNFToEDNF :: [[F]] -> [[ESafe]]
fDNFToEDNF = ([F] -> [ESafe]) -> [[F]] -> [[ESafe]]
forall a b. (a -> b) -> [a] -> [b]
map [F] -> [ESafe]
fConjToE
where
fConjToE :: [F] -> [ESafe]
fConjToE :: [F] -> [ESafe]
fConjToE [] = []
fConjToE (FComp Comp
Ge E
e1 E
e2 : [F]
fs) = E -> ESafe
ENonStrict (BinOp -> E -> E -> E
EBinOp BinOp
Sub E
e1 E
e2) ESafe -> [ESafe] -> [ESafe]
forall a. a -> [a] -> [a]
: [F] -> [ESafe]
fConjToE [F]
fs
fConjToE (FComp Comp
Gt E
e1 E
e2 : [F]
fs) = E -> ESafe
EStrict (BinOp -> E -> E -> E
EBinOp BinOp
Sub E
e1 E
e2) ESafe -> [ESafe] -> [ESafe]
forall a. a -> [a] -> [a]
: [F] -> [ESafe]
fConjToE [F]
fs
fConjToE (FComp {} : [F]
_) = String -> [ESafe]
forall a. HasCallStack => String -> a
error String
"Non-normalized FComp found in DNF"
fConjToE (FConn {} : [F]
_) = String -> [ESafe]
forall a. HasCallStack => String -> a
error String
"Non-atomic F found in DNF"
fConjToE (FNot F
f : [F]
fs) = String -> [ESafe]
forall a. HasCallStack => String -> a
error String
"Negated f found in DNF"
fConjToE (F
FTrue : [F]
fs) = E -> ESafe
ENonStrict (Rational -> E
Lit Rational
1.0) ESafe -> [ESafe] -> [ESafe]
forall a. a -> [a] -> [a]
: [F] -> [ESafe]
fConjToE [F]
fs
fConjToE (F
FFalse : [F]
fs) = E -> ESafe
ENonStrict (Rational -> E
Lit (-Rational
1.0)) ESafe -> [ESafe] -> [ESafe]
forall a. a -> [a] -> [a]
: [F] -> [ESafe]
fConjToE [F]
fs
compFToE :: Bool -> F -> ESafe
compFToE :: Bool -> F -> ESafe
compFToE Bool
_ (FComp Comp
Eq E
_ E
_) = String -> ESafe
forall a. HasCallStack => String -> a
error String
"FComp with Eq found in DNF"
compFToE Bool
False (FComp Comp
Ge E
e1 E
e2) = E -> ESafe
ENonStrict (E -> ESafe) -> E -> ESafe
forall a b. (a -> b) -> a -> b
$ BinOp -> E -> E -> E
EBinOp BinOp
Sub E
e1 E
e2
compFToE Bool
False (FComp Comp
Gt E
e1 E
e2) = E -> ESafe
EStrict (E -> ESafe) -> E -> ESafe
forall a b. (a -> b) -> a -> b
$ BinOp -> E -> E -> E
EBinOp BinOp
Sub E
e1 E
e2
compFToE Bool
False (FComp Comp
Le E
e1 E
e2) = Bool -> F -> ESafe
compFToE Bool
False (Comp -> E -> E -> F
FComp Comp
Ge E
e2 E
e1)
compFToE Bool
False (FComp Comp
Lt E
e1 E
e2) = Bool -> F -> ESafe
compFToE Bool
False (Comp -> E -> E -> F
FComp Comp
Gt E
e2 E
e1)
compFToE Bool
True (FComp Comp
Ge E
e1 E
e2) = Bool -> F -> ESafe
compFToE Bool
False (Comp -> E -> E -> F
FComp Comp
Lt E
e2 E
e1)
compFToE Bool
True (FComp Comp
Gt E
e1 E
e2) = Bool -> F -> ESafe
compFToE Bool
False (Comp -> E -> E -> F
FComp Comp
Le E
e2 E
e1)
compFToE Bool
True (FComp Comp
Le E
e1 E
e2) = Bool -> F -> ESafe
compFToE Bool
False (Comp -> E -> E -> F
FComp Comp
Gt E
e2 E
e1)
compFToE Bool
True (FComp Comp
Lt E
e1 E
e2) = Bool -> F -> ESafe
compFToE Bool
False (Comp -> E -> E -> F
FComp Comp
Ge E
e2 E
e1)
compFToE Bool
_ FConn {} = String -> ESafe
forall a. HasCallStack => String -> a
error String
"non-atomic f found in DNF"
compFToE Bool
isNegated (FNot F
f) = Bool -> F -> ESafe
compFToE (Bool -> NegType Bool
forall t. CanNeg t => t -> NegType t
not Bool
isNegated) F
f
compFToE Bool
False F
FTrue = E -> ESafe
ENonStrict (E -> ESafe) -> E -> ESafe
forall a b. (a -> b) -> a -> b
$ Rational -> E
Lit Rational
1.0
compFToE Bool
False F
FFalse = E -> ESafe
ENonStrict (E -> ESafe) -> E -> ESafe
forall a b. (a -> b) -> a -> b
$ Rational -> E
Lit (Rational -> E) -> Rational -> E
forall a b. (a -> b) -> a -> b
$ -Rational
1.0
compFToE Bool
True F
FTrue = E -> ESafe
ENonStrict (E -> ESafe) -> E -> ESafe
forall a b. (a -> b) -> a -> b
$ Rational -> E
Lit (Rational -> E) -> Rational -> E
forall a b. (a -> b) -> a -> b
$ -Rational
1.0
compFToE Bool
True F
FFalse = E -> ESafe
ENonStrict (E -> ESafe) -> E -> ESafe
forall a b. (a -> b) -> a -> b
$ Rational -> E
Lit Rational
1.0
simplifyFDoubleList :: [[F]] -> [[F]]
simplifyFDoubleList :: [[F]] -> [[F]]
simplifyFDoubleList = [[F]] -> [[F]]
forall a. Eq a => [a] -> [a]
nub ([[F]] -> [[F]]) -> ([[F]] -> [[F]]) -> [[F]] -> [[F]]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ([F] -> [F]) -> [[F]] -> [[F]]
forall a b. (a -> b) -> [a] -> [b]
map ([F] -> [F]
forall a. Eq a => [a] -> [a]
nub ([F] -> [F]) -> ([F] -> [F]) -> [F] -> [F]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (F -> F) -> [F] -> [F]
forall a b. (a -> b) -> [a] -> [b]
map F -> F
simplifyF)
simplifyESafeDoubleList :: [[ESafe]] -> [[ESafe]]
simplifyESafeDoubleList :: [[ESafe]] -> [[ESafe]]
simplifyESafeDoubleList = [[ESafe]] -> [[ESafe]]
forall a. Eq a => [a] -> [a]
nub ([[ESafe]] -> [[ESafe]])
-> ([[ESafe]] -> [[ESafe]]) -> [[ESafe]] -> [[ESafe]]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ([ESafe] -> [ESafe]) -> [[ESafe]] -> [[ESafe]]
forall a b. (a -> b) -> [a] -> [b]
map ([ESafe] -> [ESafe]
forall a. Eq a => [a] -> [a]
nub ([ESafe] -> [ESafe]) -> ([ESafe] -> [ESafe]) -> [ESafe] -> [ESafe]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (ESafe -> ESafe) -> [ESafe] -> [ESafe]
forall a b. (a -> b) -> [a] -> [b]
map ((E -> E) -> ESafe -> ESafe
fmapESafe E -> E
simplifyE))
computeE :: E -> [(String, Rational)] -> CN Double
computeE :: E -> [(String, Rational)] -> CN Double
computeE (EBinOp BinOp
op E
e1 E
e2) [(String, Rational)]
varMap =
case BinOp
op of
BinOp
Min -> E -> [(String, Rational)] -> CN Double
computeE E
e1 [(String, Rational)]
varMap CN Double -> CN Double -> MinMaxType (CN Double) (CN Double)
forall t1 t2.
CanMinMaxAsymmetric t1 t2 =>
t1 -> t2 -> MinMaxType t1 t2
`min` E -> [(String, Rational)] -> CN Double
computeE E
e2 [(String, Rational)]
varMap
BinOp
Max -> E -> [(String, Rational)] -> CN Double
computeE E
e1 [(String, Rational)]
varMap CN Double -> CN Double -> MinMaxType (CN Double) (CN Double)
forall t1 t2.
CanMinMaxAsymmetric t1 t2 =>
t1 -> t2 -> MinMaxType t1 t2
`max` E -> [(String, Rational)] -> CN Double
computeE E
e2 [(String, Rational)]
varMap
BinOp
Add -> E -> [(String, Rational)] -> CN Double
computeE E
e1 [(String, Rational)]
varMap CN Double -> CN Double -> AddType (CN Double) (CN Double)
forall t1 t2. CanAddAsymmetric t1 t2 => t1 -> t2 -> AddType t1 t2
+ E -> [(String, Rational)] -> CN Double
computeE E
e2 [(String, Rational)]
varMap
BinOp
Sub -> E -> [(String, Rational)] -> CN Double
computeE E
e1 [(String, Rational)]
varMap CN Double -> CN Double -> SubType (CN Double) (CN Double)
forall t1 t2. CanSub t1 t2 => t1 -> t2 -> SubType t1 t2
- E -> [(String, Rational)] -> CN Double
computeE E
e2 [(String, Rational)]
varMap
BinOp
Mul -> E -> [(String, Rational)] -> CN Double
computeE E
e1 [(String, Rational)]
varMap CN Double -> CN Double -> MulType (CN Double) (CN Double)
forall t1 t2. CanMulAsymmetric t1 t2 => t1 -> t2 -> MulType t1 t2
* E -> [(String, Rational)] -> CN Double
computeE E
e2 [(String, Rational)]
varMap
BinOp
Div -> E -> [(String, Rational)] -> CN Double
computeE E
e1 [(String, Rational)]
varMap CN Double -> CN Double -> DivType (CN Double) (CN Double)
forall t1 t2. CanDiv t1 t2 => t1 -> t2 -> DivType t1 t2
/ E -> [(String, Rational)] -> CN Double
computeE E
e2 [(String, Rational)]
varMap
BinOp
Pow -> E -> [(String, Rational)] -> CN Double
computeE E
e1 [(String, Rational)]
varMap CN Double -> CN Double -> PowType (CN Double) (CN Double)
forall t1 t2. CanPow t1 t2 => t1 -> t2 -> PowType t1 t2
^ E -> [(String, Rational)] -> CN Double
computeE E
e2 [(String, Rational)]
varMap
computeE (EUnOp UnOp
op E
e) [(String, Rational)]
varMap =
case UnOp
op of
UnOp
Abs -> CN Double -> AbsType (CN Double)
forall t. CanAbs t => t -> AbsType t
abs (E -> [(String, Rational)] -> CN Double
computeE E
e [(String, Rational)]
varMap)
UnOp
Sqrt -> CN Double -> SqrtType (CN Double)
forall t. CanSqrt t => t -> SqrtType t
sqrt (E -> [(String, Rational)] -> CN Double
computeE E
e [(String, Rational)]
varMap)
UnOp
Negate -> CN Double -> NegType (CN Double)
forall t. CanNeg t => t -> NegType t
negate (E -> [(String, Rational)] -> CN Double
computeE E
e [(String, Rational)]
varMap)
UnOp
Sin -> CN Double -> SinCosType (CN Double)
forall t. CanSinCos t => t -> SinCosType t
sin (E -> [(String, Rational)] -> CN Double
computeE E
e [(String, Rational)]
varMap)
UnOp
Cos -> CN Double -> SinCosType (CN Double)
forall t. CanSinCos t => t -> SinCosType t
cos (E -> [(String, Rational)] -> CN Double
computeE E
e [(String, Rational)]
varMap)
computeE (Var String
v) [(String, Rational)]
varMap =
case String -> Map String Rational -> Maybe Rational
forall k a. Ord k => k -> Map k a -> Maybe a
Map.lookup String
v ([(String, Rational)] -> Map String Rational
forall k a. Ord k => [(k, a)] -> Map k a
Map.fromList [(String, Rational)]
varMap) of
Maybe Rational
Nothing -> String -> CN Double
forall a. HasCallStack => String -> a
error (String
"map does not contain variable " String -> ShowS
forall a. [a] -> [a] -> [a]
++ ShowS
forall a. Show a => a -> String
show String
v)
Just Rational
r -> Double -> CN Double
forall v. v -> CN v
cn (Rational -> Double
forall t. CanBeDouble t => t -> Double
double Rational
r)
computeE (Lit Rational
i) [(String, Rational)]
_ = Double -> CN Double
forall v. v -> CN v
cn (Rational -> Double
forall t. CanBeDouble t => t -> Double
double Rational
i)
computeE (PowI E
e Integer
i) [(String, Rational)]
varMap = E -> [(String, Rational)] -> CN Double
computeE E
e [(String, Rational)]
varMap CN Double -> Integer -> PowType (CN Double) Integer
forall t1 t2. CanPow t1 t2 => t1 -> t2 -> PowType t1 t2
^ Integer
i
computeE (Float RoundingMode
_ E
_) [(String, Rational)]
_ = String -> CN Double
forall a. HasCallStack => String -> a
error String
"computeE for Floats not supported"
computeE (Float32 RoundingMode
_ E
_) [(String, Rational)]
_ = String -> CN Double
forall a. HasCallStack => String -> a
error String
"computeE for Floats not supported"
computeE (Float64 RoundingMode
_ E
_) [(String, Rational)]
_ = String -> CN Double
forall a. HasCallStack => String -> a
error String
"computeE for Floats not supported"
computeQualifiedEs :: [([E], E)] -> [(String, Rational)] -> [CN Double]
computeQualifiedEs :: [([E], E)] -> [(String, Rational)] -> [CN Double]
computeQualifiedEs [] [(String, Rational)]
_ = []
computeQualifiedEs (([E]
ps, E
q) : [([E], E)]
es) [(String, Rational)]
varMap =
if (E -> Bool) -> [E] -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
all (\E
p -> E -> [(String, Rational)] -> CN Double
computeE E
p [(String, Rational)]
varMap CN Double -> Integer -> Bool
forall a b. HasOrderCertainlyAsymmetric a b => a -> b -> Bool
!>=! Integer
0) [E]
ps
then E -> [(String, Rational)] -> CN Double
computeE E
q [(String, Rational)]
varMap CN Double -> [CN Double] -> [CN Double]
forall a. a -> [a] -> [a]
: [([E], E)] -> [(String, Rational)] -> [CN Double]
computeQualifiedEs [([E], E)]
es [(String, Rational)]
varMap
else [([E], E)] -> [(String, Rational)] -> [CN Double]
computeQualifiedEs [([E], E)]
es [(String, Rational)]
varMap
computeEDisjunction :: [E] -> [(String, Rational)] -> [CN Double]
computeEDisjunction :: [E] -> [(String, Rational)] -> [CN Double]
computeEDisjunction [E]
es [(String, Rational)]
varMap = (E -> CN Double) -> [E] -> [CN Double]
forall a b. (a -> b) -> [a] -> [b]
map (E -> [(String, Rational)] -> CN Double
`computeE` [(String, Rational)]
varMap) [E]
es
computeECNF :: [[E]] -> [(String, Rational)] -> [[CN Double]]
computeECNF :: [[E]] -> [(String, Rational)] -> [[CN Double]]
computeECNF [[E]]
cnf [(String, Rational)]
varMap = ([E] -> [CN Double]) -> [[E]] -> [[CN Double]]
forall a b. (a -> b) -> [a] -> [b]
map ([E] -> [(String, Rational)] -> [CN Double]
`computeEDisjunction` [(String, Rational)]
varMap) [[E]]
cnf
prettyShowESafeCNF :: [[ESafe]] -> String
prettyShowESafeCNF :: [[ESafe]] -> String
prettyShowESafeCNF [[ESafe]]
cnf = String
"AND" String -> ShowS
forall a. [a] -> [a] -> [a]
++ ([ESafe] -> String) -> [[ESafe]] -> String
forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap (\[ESafe]
d -> String
"\n\t" String -> ShowS
forall a. [a] -> [a] -> [a]
++ [ESafe] -> String
prettyShowDisjunction [ESafe]
d) [[ESafe]]
cnf
where
prettyShowDisjunction :: [ESafe] -> String
prettyShowDisjunction :: [ESafe] -> String
prettyShowDisjunction [] = []
prettyShowDisjunction [ESafe
e'] =
case ESafe
e' of
EStrict E
e -> E -> String
prettyShowE E
e String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
" > 0"
ENonStrict E
e -> E -> String
prettyShowE E
e String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
" >= 0"
prettyShowDisjunction [ESafe]
es =
String
"OR" String -> ShowS
forall a. [a] -> [a] -> [a]
++
(ESafe -> String) -> [ESafe] -> String
forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap
(\case
EStrict E
e -> String
"\n\t\t" String -> ShowS
forall a. [a] -> [a] -> [a]
++ E -> String
prettyShowE E
e String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
" > 0"
ENonStrict E
e -> String
"\n\t\t" String -> ShowS
forall a. [a] -> [a] -> [a]
++ E -> String
prettyShowE E
e String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
" >= 0")
[ESafe]
es
prettyShowESafeDNF :: [[ESafe]] -> String
prettyShowESafeDNF :: [[ESafe]] -> String
prettyShowESafeDNF [[ESafe]]
cnf = String
"OR" String -> ShowS
forall a. [a] -> [a] -> [a]
++ ([ESafe] -> String) -> [[ESafe]] -> String
forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap (\[ESafe]
d -> String
"\n\t" String -> ShowS
forall a. [a] -> [a] -> [a]
++ [ESafe] -> String
prettyShowDisjunction [ESafe]
d) [[ESafe]]
cnf
where
prettyShowDisjunction :: [ESafe] -> String
prettyShowDisjunction :: [ESafe] -> String
prettyShowDisjunction [] = []
prettyShowDisjunction [ESafe
e'] =
case ESafe
e' of
EStrict E
e -> E -> String
prettyShowE E
e String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
" > 0"
ENonStrict E
e -> E -> String
prettyShowE E
e String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
" >= 0"
prettyShowDisjunction [ESafe]
es =
String
"AND" String -> ShowS
forall a. [a] -> [a] -> [a]
++
(ESafe -> String) -> [ESafe] -> String
forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap
(\case
EStrict E
e -> String
"\n\t\t" String -> ShowS
forall a. [a] -> [a] -> [a]
++ E -> String
prettyShowE E
e String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
" > 0"
ENonStrict E
e -> String
"\n\t\t" String -> ShowS
forall a. [a] -> [a] -> [a]
++ E -> String
prettyShowE E
e String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
" >= 0")
[ESafe]
es
prettyShowFSafeDNF :: [[F]] -> String
prettyShowFSafeDNF :: [[F]] -> String
prettyShowFSafeDNF [[F]]
dnf = String
"OR" String -> ShowS
forall a. [a] -> [a] -> [a]
++ ([F] -> String) -> [[F]] -> String
forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap (\[F]
c -> String
"\n\t" String -> ShowS
forall a. [a] -> [a] -> [a]
++ [F] -> String
prettyShowConjunction [F]
c) [[F]]
dnf
where
prettyShowConjunction :: [F] -> String
prettyShowConjunction :: [F] -> String
prettyShowConjunction [] = []
prettyShowConjunction [F
f] = F -> Integer -> String
prettyShowF F
f Integer
2
prettyShowConjunction [F]
fs =
String
"AND" String -> ShowS
forall a. [a] -> [a] -> [a]
++
(F -> String) -> [F] -> String
forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap
(\F
f -> String
"\n\t\t" String -> ShowS
forall a. [a] -> [a] -> [a]
++ F -> Integer -> String
prettyShowF F
f Integer
3)
[F]
fs
prettyShowVC :: F -> TypedVarMap -> String
prettyShowVC :: F -> TypedVarMap -> String
prettyShowVC F
vc TypedVarMap
vm =
String
"Bounds on variables: \n" String -> ShowS
forall a. [a] -> [a] -> [a]
++
TypedVarMap -> String
prettyShowRanges TypedVarMap
vm String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
"\n" String -> ShowS
forall a. [a] -> [a] -> [a]
++
String
"exact NVC: \n" String -> ShowS
forall a. [a] -> [a] -> [a]
++
[F] -> String
prettyShowConjunction (F -> [F]
conjunctionToList F
vc)
where
prettyShowRanges :: TypedVarMap -> String
prettyShowRanges :: TypedVarMap -> String
prettyShowRanges [] = String
""
prettyShowRanges ((TypedVar (String
vName, (Rational
vLower, Rational
vUpper)) VarType
vType) : TypedVarMap
vm) =
String
vName String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
" (" String -> ShowS
forall a. [a] -> [a] -> [a]
++ VarType -> String
forall a. Show a => a -> String
show VarType
vType String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
")" String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
" in [" String -> ShowS
forall a. [a] -> [a] -> [a]
++ Rational -> IfThenElseType (EqCompareType Integer Integer) String
forall {a}.
(HasIfThenElse (EqCompareType a Integer) String,
HasEqAsymmetric a Integer, Show a) =>
Ratio a -> IfThenElseType (EqCompareType a Integer) String
showRational Rational
vLower String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
", " String -> ShowS
forall a. [a] -> [a] -> [a]
++ Rational -> IfThenElseType (EqCompareType Integer Integer) String
forall {a}.
(HasIfThenElse (EqCompareType a Integer) String,
HasEqAsymmetric a Integer, Show a) =>
Ratio a -> IfThenElseType (EqCompareType a Integer) String
showRational Rational
vUpper String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
"]" String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
"\n" String -> ShowS
forall a. [a] -> [a] -> [a]
++ TypedVarMap -> String
prettyShowRanges TypedVarMap
vm
showRational :: Ratio a -> IfThenElseType (EqCompareType a Integer) String
showRational Ratio a
r =
let
numer :: a
numer = Ratio a -> a
forall a. Ratio a -> a
numerator Ratio a
r
denom :: a
denom = Ratio a -> a
forall a. Ratio a -> a
denominator Ratio a
r
in
if a
denom a -> Integer -> EqCompareType a Integer
forall a b. HasEqAsymmetric a b => a -> b -> EqCompareType a b
== Integer
1
then a -> String
forall a. Show a => a -> String
show a
numer
else a -> String
forall a. Show a => a -> String
show a
numer String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
" / " String -> ShowS
forall a. [a] -> [a] -> [a]
++ a -> String
forall a. Show a => a -> String
show a
denom
conjunctionToList :: F -> [F]
conjunctionToList :: F -> [F]
conjunctionToList (FConn Conn
And F
f1 F
f2) = F -> [F]
conjunctionToList F
f1 [F] -> [F] -> [F]
forall a. [a] -> [a] -> [a]
++ F -> [F]
conjunctionToList F
f2
conjunctionToList F
f = [F
f]
prettyShowConjunction :: [F] -> String
prettyShowConjunction :: [F] -> String
prettyShowConjunction [] = []
prettyShowConjunction [F
f] = F -> Integer -> String
prettyShowF F
f Integer
2
prettyShowConjunction [F]
fs =
(F -> String) -> [F] -> String
forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap
(\F
f -> F -> Integer -> String
prettyShowAssert F
f Integer
0 String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
"\n\n")
[F]
fs
prettyShowAssert :: F -> Integer -> String
prettyShowAssert :: F -> Integer -> String
prettyShowAssert (FComp Comp
op E
e1 E
e2) Integer
indentTracker = [String] -> String
forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat (Integer -> String -> [String]
forall n a. CanBeInteger n => n -> a -> [a]
replicate Integer
indentTracker String
" ") String -> ShowS
forall a. [a] -> [a] -> [a]
++ E -> String
prettyShowE E
e1 String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
" " String -> ShowS
forall a. [a] -> [a] -> [a]
++ Comp -> String
prettyShowComp Comp
op String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
" " String -> ShowS
forall a. [a] -> [a] -> [a]
++ E -> String
prettyShowE E
e2
prettyShowAssert (FConn Conn
Impl F
f1 F
f2) Integer
indentTracker = [String] -> String
forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat (Integer -> String -> [String]
forall n a. CanBeInteger n => n -> a -> [a]
replicate Integer
indentTracker String
" ") String -> ShowS
forall a. [a] -> [a] -> [a]
++ Conn -> String
prettyShowConn Conn
Impl String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
"\n" String -> ShowS
forall a. [a] -> [a] -> [a]
++ F -> Integer -> String
prettyShowAssert F
f1 (Integer
indentTracker Integer -> Integer -> AddType Integer Integer
forall t1 t2. CanAddAsymmetric t1 t2 => t1 -> t2 -> AddType t1 t2
+ Integer
1) String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
"\n" String -> ShowS
forall a. [a] -> [a] -> [a]
++ [String] -> String
forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat (Integer -> String -> [String]
forall n a. CanBeInteger n => n -> a -> [a]
replicate (Integer
indentTracker Integer -> Integer -> AddType Integer Integer
forall t1 t2. CanAddAsymmetric t1 t2 => t1 -> t2 -> AddType t1 t2
+ Integer
1) String
" ") String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
"===========>\n" String -> ShowS
forall a. [a] -> [a] -> [a]
++ F -> Integer -> String
prettyShowAssert F
f2 (Integer
indentTracker Integer -> Integer -> AddType Integer Integer
forall t1 t2. CanAddAsymmetric t1 t2 => t1 -> t2 -> AddType t1 t2
+ Integer
1)
prettyShowAssert (FConn Conn
op F
f1 F
f2) Integer
indentTracker = [String] -> String
forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat (Integer -> String -> [String]
forall n a. CanBeInteger n => n -> a -> [a]
replicate Integer
indentTracker String
" ") String -> ShowS
forall a. [a] -> [a] -> [a]
++ Conn -> String
prettyShowConn Conn
op String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
"\n" String -> ShowS
forall a. [a] -> [a] -> [a]
++ F -> Integer -> String
prettyShowAssert F
f1 (Integer
indentTracker Integer -> Integer -> AddType Integer Integer
forall t1 t2. CanAddAsymmetric t1 t2 => t1 -> t2 -> AddType t1 t2
+ Integer
1) String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
"\n" String -> ShowS
forall a. [a] -> [a] -> [a]
++ F -> Integer -> String
prettyShowAssert F
f2 (Integer
indentTracker Integer -> Integer -> AddType Integer Integer
forall t1 t2. CanAddAsymmetric t1 t2 => t1 -> t2 -> AddType t1 t2
+ Integer
1)
prettyShowAssert (FNot F
f) Integer
indentTracker = [String] -> String
forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat (Integer -> String -> [String]
forall n a. CanBeInteger n => n -> a -> [a]
replicate Integer
indentTracker String
" ") String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
"NOT" String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
"\n" String -> ShowS
forall a. [a] -> [a] -> [a]
++ F -> Integer -> String
prettyShowAssert F
f (Integer
indentTracker Integer -> Integer -> AddType Integer Integer
forall t1 t2. CanAddAsymmetric t1 t2 => t1 -> t2 -> AddType t1 t2
+ Integer
1)
prettyShowAssert F
FTrue Integer
indentTracker = [String] -> String
forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat (Integer -> String -> [String]
forall n a. CanBeInteger n => n -> a -> [a]
replicate Integer
indentTracker String
" ") String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
"True"
prettyShowAssert F
FFalse Integer
indentTracker = [String] -> String
forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat (Integer -> String -> [String]
forall n a. CanBeInteger n => n -> a -> [a]
replicate Integer
indentTracker String
" ") String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
"False"
latexShowE :: E -> String
latexShowE :: E -> String
latexShowE (EBinOp BinOp
op E
e1 E
e2) =
case BinOp
op of
BinOp
Add -> String
"$(" String -> ShowS
forall a. [a] -> [a] -> [a]
++ E -> String
latexShowE E
e1 String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
" + " String -> ShowS
forall a. [a] -> [a] -> [a]
++ E -> String
latexShowE E
e2 String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
")$"
BinOp
Sub -> String
"$(" String -> ShowS
forall a. [a] -> [a] -> [a]
++ E -> String
latexShowE E
e1 String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
" - " String -> ShowS
forall a. [a] -> [a] -> [a]
++ E -> String
latexShowE E
e2 String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
")$"
BinOp
Div -> String
"$(" String -> ShowS
forall a. [a] -> [a] -> [a]
++ E -> String
latexShowE E
e1 String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
" \\div " String -> ShowS
forall a. [a] -> [a] -> [a]
++ E -> String
latexShowE E
e2 String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
")$"
BinOp
Mul -> String
"$(" String -> ShowS
forall a. [a] -> [a] -> [a]
++ E -> String
latexShowE E
e1 String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
" \\times " String -> ShowS
forall a. [a] -> [a] -> [a]
++ E -> String
latexShowE E
e2 String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
")$"
BinOp
Pow -> String
"$(" String -> ShowS
forall a. [a] -> [a] -> [a]
++ E -> String
latexShowE E
e1 String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
"_{" String -> ShowS
forall a. [a] -> [a] -> [a]
++ E -> String
latexShowE E
e2 String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
")}$"
BinOp
Min -> String
"$(min " String -> ShowS
forall a. [a] -> [a] -> [a]
++ E -> String
latexShowE E
e1 String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
" " String -> ShowS
forall a. [a] -> [a] -> [a]
++ E -> String
latexShowE E
e2 String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
")$"
BinOp
Max -> String
"$(max " String -> ShowS
forall a. [a] -> [a] -> [a]
++ E -> String
latexShowE E
e1 String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
" " String -> ShowS
forall a. [a] -> [a] -> [a]
++ E -> String
latexShowE E
e2 String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
")$"
BinOp
Mod -> String
"$(mod " String -> ShowS
forall a. [a] -> [a] -> [a]
++ E -> String
latexShowE E
e1 String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
" " String -> ShowS
forall a. [a] -> [a] -> [a]
++ E -> String
latexShowE E
e2 String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
")$"
latexShowE (EUnOp UnOp
op E
e) =
case UnOp
op of
UnOp
Abs -> String
"$|" String -> ShowS
forall a. [a] -> [a] -> [a]
++ E -> String
latexShowE E
e String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
"|$"
UnOp
Sqrt -> String
"$\\sqrt{" String -> ShowS
forall a. [a] -> [a] -> [a]
++ E -> String
latexShowE E
e String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
")}"
UnOp
Negate -> String
"$(-1 \\times " String -> ShowS
forall a. [a] -> [a] -> [a]
++ E -> String
latexShowE E
e String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
")$"
UnOp
Sin -> String
"$(sin " String -> ShowS
forall a. [a] -> [a] -> [a]
++ E -> String
latexShowE E
e String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
")$"
UnOp
Cos -> String
"$(cos " String -> ShowS
forall a. [a] -> [a] -> [a]
++ E -> String
latexShowE E
e String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
")$"
latexShowE (PowI E
e Integer
i) = String
"(" String -> ShowS
forall a. [a] -> [a] -> [a]
++ E -> String
latexShowE E
e String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
" ^ " String -> ShowS
forall a. [a] -> [a] -> [a]
++ Integer -> String
forall a. Show a => a -> String
show Integer
i String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
")"
latexShowE (Var String
v) = String
v
latexShowE (Lit Rational
v) = Double -> String
forall a. Show a => a -> String
show (Rational -> Double
forall t. CanBeDouble t => t -> Double
double Rational
v)
latexShowE (Float32 RoundingMode
m E
e) =
case RoundingMode
m of
RoundingMode
RNE -> String
"(rnd32_ne " String -> ShowS
forall a. [a] -> [a] -> [a]
++ E -> String
latexShowE E
e String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
")"
RoundingMode
RTP -> String
"(rnd32_tp " String -> ShowS
forall a. [a] -> [a] -> [a]
++ E -> String
latexShowE E
e String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
")"
RoundingMode
RTN -> String
"(rnd32_tn " String -> ShowS
forall a. [a] -> [a] -> [a]
++ E -> String
latexShowE E
e String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
")"
RoundingMode
RTZ -> String
"(rnd32_tz " String -> ShowS
forall a. [a] -> [a] -> [a]
++ E -> String
latexShowE E
e String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
")"
RoundingMode
RNA -> String
"(rnd32_na " String -> ShowS
forall a. [a] -> [a] -> [a]
++ E -> String
latexShowE E
e String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
")"
latexShowE (Float64 RoundingMode
m E
e) =
case RoundingMode
m of
RoundingMode
RNE -> String
"(rnd64_ne " String -> ShowS
forall a. [a] -> [a] -> [a]
++ E -> String
latexShowE E
e String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
")"
RoundingMode
RTP -> String
"(rnd64_tp " String -> ShowS
forall a. [a] -> [a] -> [a]
++ E -> String
latexShowE E
e String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
")"
RoundingMode
RTN -> String
"(rnd64_tn " String -> ShowS
forall a. [a] -> [a] -> [a]
++ E -> String
latexShowE E
e String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
")"
RoundingMode
RTZ -> String
"(rnd64_tz " String -> ShowS
forall a. [a] -> [a] -> [a]
++ E -> String
latexShowE E
e String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
")"
RoundingMode
RNA -> String
"(rnd64_na " String -> ShowS
forall a. [a] -> [a] -> [a]
++ E -> String
latexShowE E
e String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
")"
latexShowE (Float RoundingMode
m E
e) =
case RoundingMode
m of
RoundingMode
RNE -> String
"(rnd_ne " String -> ShowS
forall a. [a] -> [a] -> [a]
++ E -> String
latexShowE E
e String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
")"
RoundingMode
RTP -> String
"(rnd_tp " String -> ShowS
forall a. [a] -> [a] -> [a]
++ E -> String
latexShowE E
e String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
")"
RoundingMode
RTN -> String
"(rnd_tn " String -> ShowS
forall a. [a] -> [a] -> [a]
++ E -> String
latexShowE E
e String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
")"
RoundingMode
RTZ -> String
"(rnd_tz " String -> ShowS
forall a. [a] -> [a] -> [a]
++ E -> String
latexShowE E
e String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
")"
RoundingMode
RNA -> String
"(rnd_na " String -> ShowS
forall a. [a] -> [a] -> [a]
++ E -> String
latexShowE E
e String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
")"
latexShowE E
Pi = String
"$\\pi$"
latexShowE (RoundToInteger RoundingMode
m E
e) =
case RoundingMode
m of
RoundingMode
RNE -> String
"(rndToInt_ne " String -> ShowS
forall a. [a] -> [a] -> [a]
++ E -> String
latexShowE E
e String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
")"
RoundingMode
RTP -> String
"(rndToInt_tp " String -> ShowS
forall a. [a] -> [a] -> [a]
++ E -> String
latexShowE E
e String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
")"
RoundingMode
RTN -> String
"(rndToInt_tn " String -> ShowS
forall a. [a] -> [a] -> [a]
++ E -> String
latexShowE E
e String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
")"
RoundingMode
RTZ -> String
"(rndToInt_tz " String -> ShowS
forall a. [a] -> [a] -> [a]
++ E -> String
latexShowE E
e String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
")"
RoundingMode
RNA -> String
"(rndToInt_ta " String -> ShowS
forall a. [a] -> [a] -> [a]
++ E -> String
latexShowE E
e String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
")"
latexShowF :: F -> Integer -> String
latexShowF :: F -> Integer -> String
latexShowF (FComp Comp
op E
e1 E
e2) Integer
numTabs = String
"\n" String -> ShowS
forall a. [a] -> [a] -> [a]
++ [String] -> String
forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat (Integer -> String -> [String]
forall n a. CanBeInteger n => n -> a -> [a]
replicate Integer
numTabs String
"\t") String -> ShowS
forall a. [a] -> [a] -> [a]
++ E -> String
latexShowE E
e1 String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
" " String -> ShowS
forall a. [a] -> [a] -> [a]
++ Comp -> String
latexShowComp Comp
op String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
" " String -> ShowS
forall a. [a] -> [a] -> [a]
++ E -> String
latexShowE E
e2
latexShowF (FConn Conn
op F
f1 F
f2) Integer
numTabs = String
"\n" String -> ShowS
forall a. [a] -> [a] -> [a]
++ [String] -> String
forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat (Integer -> String -> [String]
forall n a. CanBeInteger n => n -> a -> [a]
replicate Integer
numTabs String
"\t") String -> ShowS
forall a. [a] -> [a] -> [a]
++ F -> Integer -> String
latexShowF F
f1 Integer
numTabs String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
" " String -> ShowS
forall a. [a] -> [a] -> [a]
++ Conn -> String
latexShowConn Conn
op String -> ShowS
forall a. [a] -> [a] -> [a]
++ F -> Integer -> String
latexShowF F
f2 (Integer
numTabs Integer -> Integer -> AddType Integer Integer
forall t1 t2. CanAddAsymmetric t1 t2 => t1 -> t2 -> AddType t1 t2
+ Integer
1)
latexShowF (FNot F
f) Integer
numTabs = String
"\n" String -> ShowS
forall a. [a] -> [a] -> [a]
++ [String] -> String
forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat (Integer -> String -> [String]
forall n a. CanBeInteger n => n -> a -> [a]
replicate Integer
numTabs String
"\t") String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
"$\\lnot$" String -> ShowS
forall a. [a] -> [a] -> [a]
++ F -> Integer -> String
latexShowF F
f (Integer
numTabs Integer -> Integer -> AddType Integer Integer
forall t1 t2. CanAddAsymmetric t1 t2 => t1 -> t2 -> AddType t1 t2
+ Integer
1)
latexShowF F
FTrue Integer
numTabs = String
"\n" String -> ShowS
forall a. [a] -> [a] -> [a]
++ [String] -> String
forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat (Integer -> String -> [String]
forall n a. CanBeInteger n => n -> a -> [a]
replicate Integer
numTabs String
"\t") String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
"$\\top$"
latexShowF F
FFalse Integer
numTabs = String
"\n" String -> ShowS
forall a. [a] -> [a] -> [a]
++ [String] -> String
forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat (Integer -> String -> [String]
forall n a. CanBeInteger n => n -> a -> [a]
replicate Integer
numTabs String
"\t") String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
"$\\bot$"
latexShowComp :: Comp -> String
latexShowComp :: Comp -> String
latexShowComp Comp
Gt = String
"$>$"
latexShowComp Comp
Ge = String
"$\\ge$"
latexShowComp Comp
Lt = String
"$<$"
latexShowComp Comp
Le = String
"$\\le$"
latexShowComp Comp
Eq = String
"$=$"
latexShowConn :: Conn -> String
latexShowConn :: Conn -> String
latexShowConn Conn
And = String
"$\\wedge$"
latexShowConn Conn
Or = String
"$\\vee$"
latexShowConn Conn
Impl = String
"$\\implies$"
prettyShowE :: E -> String
prettyShowE :: E -> String
prettyShowE (EBinOp BinOp
op E
e1 E
e2) =
case BinOp
op of
BinOp
Add -> String
"(" String -> ShowS
forall a. [a] -> [a] -> [a]
++ E -> String
prettyShowE E
e1 String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
" + " String -> ShowS
forall a. [a] -> [a] -> [a]
++ E -> String
prettyShowE E
e2 String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
")"
BinOp
Sub -> String
"(" String -> ShowS
forall a. [a] -> [a] -> [a]
++ E -> String
prettyShowE E
e1 String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
" - " String -> ShowS
forall a. [a] -> [a] -> [a]
++ E -> String
prettyShowE E
e2 String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
")"
BinOp
Div -> String
"(" String -> ShowS
forall a. [a] -> [a] -> [a]
++ E -> String
prettyShowE E
e1 String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
" / " String -> ShowS
forall a. [a] -> [a] -> [a]
++ E -> String
prettyShowE E
e2 String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
")"
BinOp
Mul -> String
"(" String -> ShowS
forall a. [a] -> [a] -> [a]
++ E -> String
prettyShowE E
e1 String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
" * " String -> ShowS
forall a. [a] -> [a] -> [a]
++ E -> String
prettyShowE E
e2 String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
")"
BinOp
Pow -> String
"(" String -> ShowS
forall a. [a] -> [a] -> [a]
++ E -> String
prettyShowE E
e1 String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
" ^ " String -> ShowS
forall a. [a] -> [a] -> [a]
++ E -> String
prettyShowE E
e2 String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
")"
BinOp
Min -> String
"(min " String -> ShowS
forall a. [a] -> [a] -> [a]
++ E -> String
prettyShowE E
e1 String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
" " String -> ShowS
forall a. [a] -> [a] -> [a]
++ E -> String
prettyShowE E
e2 String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
")"
BinOp
Max -> String
"(max " String -> ShowS
forall a. [a] -> [a] -> [a]
++ E -> String
prettyShowE E
e1 String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
" " String -> ShowS
forall a. [a] -> [a] -> [a]
++ E -> String
prettyShowE E
e2 String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
")"
BinOp
Mod -> String
"(mod " String -> ShowS
forall a. [a] -> [a] -> [a]
++ E -> String
prettyShowE E
e1 String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
" " String -> ShowS
forall a. [a] -> [a] -> [a]
++ E -> String
prettyShowE E
e2 String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
")"
prettyShowE (EUnOp UnOp
op E
e) =
case UnOp
op of
UnOp
Abs -> String
"|" String -> ShowS
forall a. [a] -> [a] -> [a]
++ E -> String
prettyShowE E
e String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
"|"
UnOp
Sqrt -> String
"(sqrt " String -> ShowS
forall a. [a] -> [a] -> [a]
++ E -> String
prettyShowE E
e String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
")"
UnOp
Negate -> String
"(-1 * " String -> ShowS
forall a. [a] -> [a] -> [a]
++ E -> String
prettyShowE E
e String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
")"
UnOp
Sin -> String
"(sin " String -> ShowS
forall a. [a] -> [a] -> [a]
++ E -> String
prettyShowE E
e String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
")"
UnOp
Cos -> String
"(cos " String -> ShowS
forall a. [a] -> [a] -> [a]
++ E -> String
prettyShowE E
e String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
")"
prettyShowE (PowI E
e Integer
i) = String
"(" String -> ShowS
forall a. [a] -> [a] -> [a]
++ E -> String
prettyShowE E
e String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
" ^ " String -> ShowS
forall a. [a] -> [a] -> [a]
++ Integer -> String
forall a. Show a => a -> String
show Integer
i String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
")"
prettyShowE (Var String
v) = String
v
prettyShowE (Lit Rational
v) =
if Integer
denom Integer -> Integer -> EqCompareType Integer Integer
forall a b. HasEqAsymmetric a b => a -> b -> EqCompareType a b
== Integer
1
then Integer -> String
forall a. Show a => a -> String
show Integer
numer
else Integer -> String
forall a. Show a => a -> String
show Integer
numer String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
" / " String -> ShowS
forall a. [a] -> [a] -> [a]
++ Integer -> String
forall a. Show a => a -> String
show Integer
denom
where
numer :: Integer
numer = Rational -> Integer
forall a. Ratio a -> a
numerator Rational
v
denom :: Integer
denom = Rational -> Integer
forall a. Ratio a -> a
denominator Rational
v
prettyShowE (Float32 RoundingMode
m E
e) =
case RoundingMode
m of
RoundingMode
RNE -> String
"(rnd32_ne " String -> ShowS
forall a. [a] -> [a] -> [a]
++ E -> String
prettyShowE E
e String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
")"
RoundingMode
RTP -> String
"(rnd32_tp " String -> ShowS
forall a. [a] -> [a] -> [a]
++ E -> String
prettyShowE E
e String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
")"
RoundingMode
RTN -> String
"(rnd32_tn " String -> ShowS
forall a. [a] -> [a] -> [a]
++ E -> String
prettyShowE E
e String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
")"
RoundingMode
RTZ -> String
"(rnd32_tz " String -> ShowS
forall a. [a] -> [a] -> [a]
++ E -> String
prettyShowE E
e String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
")"
RoundingMode
RNA -> String
"(rnd32_na " String -> ShowS
forall a. [a] -> [a] -> [a]
++ E -> String
prettyShowE E
e String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
")"
prettyShowE (Float64 RoundingMode
m E
e) =
case RoundingMode
m of
RoundingMode
RNE -> String
"(rnd64_ne " String -> ShowS
forall a. [a] -> [a] -> [a]
++ E -> String
prettyShowE E
e String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
")"
RoundingMode
RTP -> String
"(rnd64_tp " String -> ShowS
forall a. [a] -> [a] -> [a]
++ E -> String
prettyShowE E
e String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
")"
RoundingMode
RTN -> String
"(rnd64_tn " String -> ShowS
forall a. [a] -> [a] -> [a]
++ E -> String
prettyShowE E
e String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
")"
RoundingMode
RTZ -> String
"(rnd64_tz " String -> ShowS
forall a. [a] -> [a] -> [a]
++ E -> String
prettyShowE E
e String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
")"
RoundingMode
RNA -> String
"(rnd64_na " String -> ShowS
forall a. [a] -> [a] -> [a]
++ E -> String
prettyShowE E
e String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
")"
prettyShowE (Float RoundingMode
m E
e) =
case RoundingMode
m of
RoundingMode
RNE -> String
"(rnd_ne " String -> ShowS
forall a. [a] -> [a] -> [a]
++ E -> String
prettyShowE E
e String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
")"
RoundingMode
RTP -> String
"(rnd_tp " String -> ShowS
forall a. [a] -> [a] -> [a]
++ E -> String
prettyShowE E
e String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
")"
RoundingMode
RTN -> String
"(rnd_tn " String -> ShowS
forall a. [a] -> [a] -> [a]
++ E -> String
prettyShowE E
e String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
")"
RoundingMode
RTZ -> String
"(rnd_tz " String -> ShowS
forall a. [a] -> [a] -> [a]
++ E -> String
prettyShowE E
e String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
")"
RoundingMode
RNA -> String
"(rnd_na " String -> ShowS
forall a. [a] -> [a] -> [a]
++ E -> String
prettyShowE E
e String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
")"
prettyShowE E
Pi = String
"Pi"
prettyShowE (RoundToInteger RoundingMode
m E
e) =
case RoundingMode
m of
RoundingMode
RNE -> String
"(rndToInt_ne " String -> ShowS
forall a. [a] -> [a] -> [a]
++ E -> String
prettyShowE E
e String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
")"
RoundingMode
RTP -> String
"(rndToInt_tp " String -> ShowS
forall a. [a] -> [a] -> [a]
++ E -> String
prettyShowE E
e String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
")"
RoundingMode
RTN -> String
"(rndToInt_tn " String -> ShowS
forall a. [a] -> [a] -> [a]
++ E -> String
prettyShowE E
e String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
")"
RoundingMode
RTZ -> String
"(rndToInt_tz " String -> ShowS
forall a. [a] -> [a] -> [a]
++ E -> String
prettyShowE E
e String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
")"
RoundingMode
RNA -> String
"(rndToInt_ta " String -> ShowS
forall a. [a] -> [a] -> [a]
++ E -> String
prettyShowE E
e String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
")"
prettyShowECNF :: [[E]] -> String
prettyShowECNF :: [[E]] -> String
prettyShowECNF [[E]]
cnf =
String
"AND" String -> ShowS
forall a. [a] -> [a] -> [a]
++ ([E] -> String) -> [[E]] -> String
forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap (\[E]
d -> String
"\n\t" String -> ShowS
forall a. [a] -> [a] -> [a]
++ [E] -> String
prettyShowDisjunction [E]
d) [[E]]
cnf
where
prettyShowDisjunction :: [E] -> String
prettyShowDisjunction :: [E] -> String
prettyShowDisjunction [] = []
prettyShowDisjunction [E
e] = E -> String
prettyShowE E
e
prettyShowDisjunction [E]
es =
String
"OR" String -> ShowS
forall a. [a] -> [a] -> [a]
++ (E -> String) -> [E] -> String
forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap (\E
e -> String
"\n\t\t" String -> ShowS
forall a. [a] -> [a] -> [a]
++ E -> String
prettyShowE E
e String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
" > 0") [E]
es
prettyShowF :: F -> Integer -> String
prettyShowF :: F -> Integer -> String
prettyShowF (FComp Comp
op E
e1 E
e2) Integer
numTabs = String
"\n" String -> ShowS
forall a. [a] -> [a] -> [a]
++ [String] -> String
forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat (Integer -> String -> [String]
forall n a. CanBeInteger n => n -> a -> [a]
replicate Integer
numTabs String
"\t") String -> ShowS
forall a. [a] -> [a] -> [a]
++ E -> String
prettyShowE E
e1 String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
" " String -> ShowS
forall a. [a] -> [a] -> [a]
++ Comp -> String
prettyShowComp Comp
op String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
" " String -> ShowS
forall a. [a] -> [a] -> [a]
++ E -> String
prettyShowE E
e2
prettyShowF (FConn Conn
op F
f1 F
f2) Integer
numTabs = String
"\n" String -> ShowS
forall a. [a] -> [a] -> [a]
++ [String] -> String
forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat (Integer -> String -> [String]
forall n a. CanBeInteger n => n -> a -> [a]
replicate Integer
numTabs String
"\t") String -> ShowS
forall a. [a] -> [a] -> [a]
++ Conn -> String
prettyShowConn Conn
op String -> ShowS
forall a. [a] -> [a] -> [a]
++ F -> Integer -> String
prettyShowF F
f1 (Integer
numTabs Integer -> Integer -> AddType Integer Integer
forall t1 t2. CanAddAsymmetric t1 t2 => t1 -> t2 -> AddType t1 t2
+ Integer
1) String -> ShowS
forall a. [a] -> [a] -> [a]
++ F -> Integer -> String
prettyShowF F
f2 (Integer
numTabs Integer -> Integer -> AddType Integer Integer
forall t1 t2. CanAddAsymmetric t1 t2 => t1 -> t2 -> AddType t1 t2
+ Integer
1)
prettyShowF (FNot F
f) Integer
numTabs = String
"\n" String -> ShowS
forall a. [a] -> [a] -> [a]
++ [String] -> String
forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat (Integer -> String -> [String]
forall n a. CanBeInteger n => n -> a -> [a]
replicate Integer
numTabs String
"\t") String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
"NOT" String -> ShowS
forall a. [a] -> [a] -> [a]
++ F -> Integer -> String
prettyShowF F
f (Integer
numTabs Integer -> Integer -> AddType Integer Integer
forall t1 t2. CanAddAsymmetric t1 t2 => t1 -> t2 -> AddType t1 t2
+ Integer
1)
prettyShowF F
FTrue Integer
numTabs = String
"\n" String -> ShowS
forall a. [a] -> [a] -> [a]
++ [String] -> String
forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat (Integer -> String -> [String]
forall n a. CanBeInteger n => n -> a -> [a]
replicate Integer
numTabs String
"\t") String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
"True"
prettyShowF F
FFalse Integer
numTabs = String
"\n" String -> ShowS
forall a. [a] -> [a] -> [a]
++ [String] -> String
forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat (Integer -> String -> [String]
forall n a. CanBeInteger n => n -> a -> [a]
replicate Integer
numTabs String
"\t") String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
"False"
prettyShowComp :: Comp -> String
prettyShowComp :: Comp -> String
prettyShowComp Comp
Gt = String
">"
prettyShowComp Comp
Ge = String
">="
prettyShowComp Comp
Lt = String
"<"
prettyShowComp Comp
Le = String
"<="
prettyShowComp Comp
Eq = String
"=="
prettyShowConn :: Conn -> String
prettyShowConn :: Conn -> String
prettyShowConn Conn
And = String
"AND"
prettyShowConn Conn
Or = String
"OR"
prettyShowConn Conn
Impl = String
"IMPL"
extractVariablesE :: E -> [String]
= [String] -> [String]
forall a. Eq a => [a] -> [a]
nub ([String] -> [String]) -> (E -> [String]) -> E -> [String]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. E -> [String]
findAllVars
where
findAllVars :: E -> [String]
findAllVars (Lit Rational
_) = []
findAllVars E
Pi = []
findAllVars (Var String
v) = [String
v]
findAllVars (EUnOp UnOp
_ E
e) = E -> [String]
findAllVars E
e
findAllVars (EBinOp BinOp
_ E
e1 E
e2) = E -> [String]
findAllVars E
e1 [String] -> [String] -> [String]
forall a. [a] -> [a] -> [a]
++ E -> [String]
findAllVars E
e2
findAllVars (PowI E
e Integer
_) = E -> [String]
findAllVars E
e
findAllVars (Float32 RoundingMode
_ E
e) = E -> [String]
findAllVars E
e
findAllVars (Float64 RoundingMode
_ E
e) = E -> [String]
findAllVars E
e
findAllVars (Float RoundingMode
_ E
e) = E -> [String]
findAllVars E
e
findAllVars (RoundToInteger RoundingMode
_ E
e) = E -> [String]
findAllVars E
e
extractVariablesF :: F -> [String]
= [String] -> [String]
forall a. Eq a => [a] -> [a]
nub ([String] -> [String]) -> (F -> [String]) -> F -> [String]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. F -> [String]
findAllVars
where
findAllVars :: F -> [String]
findAllVars (FComp Comp
_ E
e1 E
e2) = E -> [String]
extractVariablesE E
e1 [String] -> [String] -> [String]
forall a. [a] -> [a] -> [a]
++ E -> [String]
extractVariablesE E
e2
findAllVars (FConn Conn
_ F
f1 F
f2) = F -> [String]
findAllVars F
f1 [String] -> [String] -> [String]
forall a. [a] -> [a] -> [a]
++ F -> [String]
findAllVars F
f2
findAllVars (FNot F
f) = F -> [String]
findAllVars F
f
findAllVars F
FTrue = []
findAllVars F
FFalse = []
extractVariablesECNF :: [[E]] -> [String]
= [String] -> [String]
forall a. Eq a => [a] -> [a]
nub ([String] -> [String]) -> ([[E]] -> [String]) -> [[E]] -> [String]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ([E] -> [String]) -> [[E]] -> [String]
forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap ((E -> [String]) -> [E] -> [String]
forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap E -> [String]
extractVariablesE)
hasVarsE :: E -> Bool
hasVarsE :: E -> Bool
hasVarsE (Float RoundingMode
_ E
_) = Bool
False
hasVarsE (Float32 RoundingMode
_ E
_) = Bool
False
hasVarsE (Float64 RoundingMode
_ E
_) = Bool
False
hasVarsE (EBinOp BinOp
_ E
e1 E
e2) = E -> Bool
hasFloatE E
e1 Bool -> Bool -> AndOrType Bool Bool
forall a b. CanAndOrAsymmetric a b => a -> b -> AndOrType a b
|| E -> Bool
hasFloatE E
e2
hasVarsE (EUnOp UnOp
_ E
e) = E -> Bool
hasFloatE E
e
hasVarsE (PowI E
e Integer
_) = E -> Bool
hasFloatE E
e
hasVarsE (Lit Rational
_) = Bool
False
hasVarsE (Var String
_) = Bool
True
hasVarsE E
Pi = Bool
False
hasVarsE (RoundToInteger RoundingMode
_ E
e) = E -> Bool
hasFloatE E
e
hasVarsF :: F -> Bool
hasVarsF :: F -> Bool
hasVarsF (FConn Conn
_ F
f1 F
f2) = F -> Bool
hasVarsF F
f1 Bool -> Bool -> AndOrType Bool Bool
forall a b. CanAndOrAsymmetric a b => a -> b -> AndOrType a b
|| F -> Bool
hasVarsF F
f2
hasVarsF (FComp Comp
_ E
e1 E
e2) = E -> Bool
hasVarsE E
e1 Bool -> Bool -> AndOrType Bool Bool
forall a b. CanAndOrAsymmetric a b => a -> b -> AndOrType a b
|| E -> Bool
hasVarsE E
e2
hasVarsF (FNot F
f) = F -> Bool
hasVarsF F
f
hasVarsF F
FTrue = Bool
False
hasVarsF F
FFalse = Bool
False
hasFloatE :: E -> Bool
hasFloatE :: E -> Bool
hasFloatE (Float RoundingMode
_ E
_) = Bool
True
hasFloatE (Float32 RoundingMode
_ E
_) = Bool
True
hasFloatE (Float64 RoundingMode
_ E
_) = Bool
True
hasFloatE (EBinOp BinOp
_ E
e1 E
e2) = E -> Bool
hasFloatE E
e1 Bool -> Bool -> AndOrType Bool Bool
forall a b. CanAndOrAsymmetric a b => a -> b -> AndOrType a b
|| E -> Bool
hasFloatE E
e2
hasFloatE (EUnOp UnOp
_ E
e) = E -> Bool
hasFloatE E
e
hasFloatE (PowI E
e Integer
_) = E -> Bool
hasFloatE E
e
hasFloatE (Lit Rational
_) = Bool
False
hasFloatE (Var String
_) = Bool
False
hasFloatE E
Pi = Bool
False
hasFloatE (RoundToInteger RoundingMode
_ E
e) = E -> Bool
hasFloatE E
e
hasFloatF :: F -> Bool
hasFloatF :: F -> Bool
hasFloatF (FConn Conn
_ F
f1 F
f2) = F -> Bool
hasFloatF F
f1 Bool -> Bool -> AndOrType Bool Bool
forall a b. CanAndOrAsymmetric a b => a -> b -> AndOrType a b
|| F -> Bool
hasFloatF F
f2
hasFloatF (FComp Comp
_ E
e1 E
e2) = E -> Bool
hasFloatE E
e1 Bool -> Bool -> AndOrType Bool Bool
forall a b. CanAndOrAsymmetric a b => a -> b -> AndOrType a b
|| E -> Bool
hasFloatE E
e2
hasFloatF (FNot F
f) = F -> Bool
hasFloatF F
f
hasFloatF F
FTrue = Bool
False
hasFloatF F
FFalse = Bool
False
substVarEWithLit :: E -> String -> Rational -> E
substVarEWithLit :: E -> String -> Rational -> E
substVarEWithLit (Var String
x) String
varToSubst Rational
valToSubst = if String
x String -> String -> EqCompareType String String
forall a b. HasEqAsymmetric a b => a -> b -> EqCompareType a b
== String
varToSubst then Rational -> E
Lit Rational
valToSubst else String -> E
Var String
x
substVarEWithLit (RoundToInteger RoundingMode
m E
e) String
var Rational
val = RoundingMode -> E -> E
RoundToInteger RoundingMode
m (E -> String -> Rational -> E
substVarEWithLit E
e String
var Rational
val)
substVarEWithLit E
Pi String
_ Rational
_ = E
Pi
substVarEWithLit l :: E
l@(Lit Rational
_) String
_ Rational
_ = E
l
substVarEWithLit (EBinOp BinOp
op E
e1 E
e2) String
var Rational
val = BinOp -> E -> E -> E
EBinOp BinOp
op (E -> String -> Rational -> E
substVarEWithLit E
e1 String
var Rational
val) (E -> String -> Rational -> E
substVarEWithLit E
e2 String
var Rational
val)
substVarEWithLit (EUnOp UnOp
op E
e) String
var Rational
val = UnOp -> E -> E
EUnOp UnOp
op (E -> String -> Rational -> E
substVarEWithLit E
e String
var Rational
val)
substVarEWithLit (PowI E
e Integer
i) String
var Rational
val = E -> Integer -> E
PowI (E -> String -> Rational -> E
substVarEWithLit E
e String
var Rational
val) Integer
i
substVarEWithLit (Float RoundingMode
m E
e) String
var Rational
val = RoundingMode -> E -> E
Float RoundingMode
m (E -> String -> Rational -> E
substVarEWithLit E
e String
var Rational
val)
substVarEWithLit (Float32 RoundingMode
m E
e) String
var Rational
val = RoundingMode -> E -> E
Float32 RoundingMode
m (E -> String -> Rational -> E
substVarEWithLit E
e String
var Rational
val)
substVarEWithLit (Float64 RoundingMode
m E
e) String
var Rational
val = RoundingMode -> E -> E
Float64 RoundingMode
m (E -> String -> Rational -> E
substVarEWithLit E
e String
var Rational
val)
substVarFWithLit :: F -> String -> Rational -> F
substVarFWithLit :: F -> String -> Rational -> F
substVarFWithLit (FConn Conn
op F
f1 F
f2) String
var Rational
val = Conn -> F -> F -> F
FConn Conn
op (F -> String -> Rational -> F
substVarFWithLit F
f1 String
var Rational
val) (F -> String -> Rational -> F
substVarFWithLit F
f2 String
var Rational
val)
substVarFWithLit (FComp Comp
op E
e1 E
e2) String
var Rational
val = Comp -> E -> E -> F
FComp Comp
op (E -> String -> Rational -> E
substVarEWithLit E
e1 String
var Rational
val) (E -> String -> Rational -> E
substVarEWithLit E
e2 String
var Rational
val)
substVarFWithLit (FNot F
f) String
var Rational
val = F -> F
FNot (F -> String -> Rational -> F
substVarFWithLit F
f String
var Rational
val)
substVarFWithLit F
FTrue String
_ Rational
_ = F
FTrue
substVarFWithLit F
FFalse String
_ Rational
_ = F
FFalse
substVarEWithE :: String -> E -> E -> E
substVarEWithE :: String -> E -> E -> E
substVarEWithE String
varToSubst (EBinOp BinOp
op E
e1 E
e2) E
eToSubst = BinOp -> E -> E -> E
EBinOp BinOp
op (String -> E -> E -> E
substVarEWithE String
varToSubst E
e1 E
eToSubst) (String -> E -> E -> E
substVarEWithE String
varToSubst E
e2 E
eToSubst)
substVarEWithE String
varToSubst (EUnOp UnOp
op E
e) E
eToSubst = UnOp -> E -> E
EUnOp UnOp
op (String -> E -> E -> E
substVarEWithE String
varToSubst E
e E
eToSubst)
substVarEWithE String
varToSubst (Float RoundingMode
mode E
e) E
eToSubst = RoundingMode -> E -> E
Float RoundingMode
mode (E -> E) -> E -> E
forall a b. (a -> b) -> a -> b
$ String -> E -> E -> E
substVarEWithE String
varToSubst E
e E
eToSubst
substVarEWithE String
varToSubst (Float32 RoundingMode
mode E
e) E
eToSubst = RoundingMode -> E -> E
Float32 RoundingMode
mode (E -> E) -> E -> E
forall a b. (a -> b) -> a -> b
$ String -> E -> E -> E
substVarEWithE String
varToSubst E
e E
eToSubst
substVarEWithE String
varToSubst (Float64 RoundingMode
mode E
e) E
eToSubst = RoundingMode -> E -> E
Float64 RoundingMode
mode (E -> E) -> E -> E
forall a b. (a -> b) -> a -> b
$ String -> E -> E -> E
substVarEWithE String
varToSubst E
e E
eToSubst
substVarEWithE String
varToSubst (RoundToInteger RoundingMode
mode E
e) E
eToSubst = RoundingMode -> E -> E
RoundToInteger RoundingMode
mode (E -> E) -> E -> E
forall a b. (a -> b) -> a -> b
$ String -> E -> E -> E
substVarEWithE String
varToSubst E
e E
eToSubst
substVarEWithE String
varToSubst (PowI E
e Integer
i) E
eToSubst = E -> Integer -> E
PowI (String -> E -> E -> E
substVarEWithE String
varToSubst E
e E
eToSubst) Integer
i
substVarEWithE String
_ E
Pi E
eToSubst = E
Pi
substVarEWithE String
_ e :: E
e@(Lit Rational
_) E
eToSubst = E
e
substVarEWithE String
varToSubst (Var String
y) E
eToSubst = if String
varToSubst String -> String -> EqCompareType String String
forall a b. HasEqAsymmetric a b => a -> b -> EqCompareType a b
== String
y then E
eToSubst else String -> E
Var String
y
substVarFWithE :: String -> F -> E -> F
substVarFWithE :: String -> F -> E -> F
substVarFWithE String
varToSubst (FConn Conn
op F
f1 F
f2) E
eToSubst = Conn -> F -> F -> F
FConn Conn
op (String -> F -> E -> F
substVarFWithE String
varToSubst F
f1 E
eToSubst) (String -> F -> E -> F
substVarFWithE String
varToSubst F
f2 E
eToSubst)
substVarFWithE String
varToSubst (FComp Comp
op E
e1 E
e2) E
eToSubst = Comp -> E -> E -> F
FComp Comp
op (String -> E -> E -> E
substVarEWithE String
varToSubst E
e1 E
eToSubst) (String -> E -> E -> E
substVarEWithE String
varToSubst E
e2 E
eToSubst)
substVarFWithE String
varToSubst (FNot F
f) E
eToSubst = F -> F
FNot (F -> F) -> F -> F
forall a b. (a -> b) -> a -> b
$ String -> F -> E -> F
substVarFWithE String
varToSubst F
f E
eToSubst
substVarFWithE String
_ F
FTrue E
_ = F
FTrue
substVarFWithE String
_ F
FFalse E
_ = F
FFalse
transformImplications :: F -> F
transformImplications :: F -> F
transformImplications (FConn Conn
Impl F
f1 F
f2) = Conn -> F -> F -> F
FConn Conn
Or (F -> F
transformImplications (F -> F
FNot F
f1)) (F -> F
transformImplications F
f2)
transformImplications (FConn Conn
op F
f1 F
f2) = Conn -> F -> F -> F
FConn Conn
op (F -> F
transformImplications F
f1) (F -> F
transformImplications F
f2)
transformImplications f :: F
f@(FComp Comp
op E
e1 E
e2) = F
f
transformImplications (FNot F
f) = F -> F
FNot (F -> F) -> F -> F
forall a b. (a -> b) -> a -> b
$ F -> F
transformImplications F
f
transformImplications F
FTrue = F
FTrue
transformImplications F
FFalse = F
FFalse
removeVariableFreeComparisons :: F -> F
removeVariableFreeComparisons :: F -> F
removeVariableFreeComparisons F
f =
F -> Bool -> F
forall {t}.
(CanNeg t, HasIfThenElse t F, NegType t ~ t,
IfThenElseType t F ~ F) =>
F -> t -> F
aux F
f Bool
False
where
expressionContainsVars :: E -> Bool
expressionContainsVars :: E -> Bool
expressionContainsVars (EBinOp BinOp
_ E
e1 E
e2) = E -> Bool
expressionContainsVars E
e1 Bool -> Bool -> AndOrType Bool Bool
forall a b. CanAndOrAsymmetric a b => a -> b -> AndOrType a b
|| E -> Bool
expressionContainsVars E
e2
expressionContainsVars (EUnOp UnOp
_ E
e) = E -> Bool
expressionContainsVars E
e
expressionContainsVars (PowI E
e Integer
_) = E -> Bool
expressionContainsVars E
e
expressionContainsVars (Float RoundingMode
_ E
e) = E -> Bool
expressionContainsVars E
e
expressionContainsVars (Float32 RoundingMode
_ E
e) = E -> Bool
expressionContainsVars E
e
expressionContainsVars (Float64 RoundingMode
_ E
e) = E -> Bool
expressionContainsVars E
e
expressionContainsVars (RoundToInteger RoundingMode
_ E
e) = E -> Bool
expressionContainsVars E
e
expressionContainsVars (Lit Rational
_) = Bool
False
expressionContainsVars E
Pi = Bool
False
expressionContainsVars (Var String
_) = Bool
True
aux :: F -> t -> F
aux f' :: F
f'@(FConn Conn
And F
f1 F
f2) t
isNegated = Conn -> F -> F -> F
FConn Conn
And (F -> t -> F
aux F
f1 t
isNegated) (F -> t -> F
aux F
f2 t
isNegated)
aux f' :: F
f'@(FConn Conn
Or F
f1 F
f2) t
isNegated = Conn -> F -> F -> F
FConn Conn
Or (F -> t -> F
aux F
f1 t
isNegated) (F -> t -> F
aux F
f2 t
isNegated)
aux f' :: F
f'@(FConn Conn
Impl F
f1 F
f2) t
isNegated = Conn -> F -> F -> F
FConn Conn
Impl (F -> t -> F
aux F
f1 (t -> NegType t
forall t. CanNeg t => t -> NegType t
not t
isNegated)) (F -> t -> F
aux F
f2 t
isNegated)
aux f' :: F
f'@(FComp Comp
_ E
e1 E
e2) t
isNegated =
case (E -> Bool
expressionContainsVars E
e1, E -> Bool
expressionContainsVars E
e2) of
(Bool
True, Bool
_) -> F
f'
(Bool
_, Bool
True) -> F
f'
(Bool, Bool)
_ -> if t
isNegated then F
FFalse else F
FTrue
aux (FNot F
f') t
isNegated = F -> F
FNot (F -> t -> F
aux F
f' (t -> NegType t
forall t. CanNeg t => t -> NegType t
not t
isNegated))
aux F
FTrue t
_ = F
FTrue
aux F
FFalse t
_ = F
FFalse
hasMinMaxAbsE :: E -> Bool
hasMinMaxAbsE :: E -> Bool
hasMinMaxAbsE (EBinOp BinOp
Max E
_ E
_) = Bool
True
hasMinMaxAbsE (EBinOp BinOp
Min E
_ E
_) = Bool
True
hasMinMaxAbsE (EBinOp BinOp
_ E
e1 E
e2) = E -> Bool
hasMinMaxAbsE E
e1 Bool -> Bool -> AndOrType Bool Bool
forall a b. CanAndOrAsymmetric a b => a -> b -> AndOrType a b
|| E -> Bool
hasMinMaxAbsE E
e2
hasMinMaxAbsE (EUnOp UnOp
Abs E
e) = Bool
True
hasMinMaxAbsE (EUnOp UnOp
_ E
e) = E -> Bool
hasMinMaxAbsE E
e
hasMinMaxAbsE (PowI E
e Integer
_) = E -> Bool
hasMinMaxAbsE E
e
hasMinMaxAbsE (Float32 RoundingMode
_ E
e) = E -> Bool
hasMinMaxAbsE E
e
hasMinMaxAbsE (Float64 RoundingMode
_ E
e) = E -> Bool
hasMinMaxAbsE E
e
hasMinMaxAbsE (Float RoundingMode
_ E
e) = E -> Bool
hasMinMaxAbsE E
e
hasMinMaxAbsE (RoundToInteger RoundingMode
_ E
e) = E -> Bool
hasMinMaxAbsE E
e
hasMinMaxAbsE (Lit Rational
_) = Bool
False
hasMinMaxAbsE (Var String
_) = Bool
False
hasMinMaxAbsE (E
Pi) = Bool
False
hasMinMaxAbsF :: F -> Bool
hasMinMaxAbsF :: F -> Bool
hasMinMaxAbsF (FComp Comp
_ E
e1 E
e2) = E -> Bool
hasMinMaxAbsE E
e1 Bool -> Bool -> AndOrType Bool Bool
forall a b. CanAndOrAsymmetric a b => a -> b -> AndOrType a b
|| E -> Bool
hasMinMaxAbsE E
e2
hasMinMaxAbsF (FConn Conn
_ F
f1 F
f2) = F -> Bool
hasMinMaxAbsF F
f1 Bool -> Bool -> AndOrType Bool Bool
forall a b. CanAndOrAsymmetric a b => a -> b -> AndOrType a b
|| F -> Bool
hasMinMaxAbsF F
f2
hasMinMaxAbsF (FNot F
f) = F -> Bool
hasMinMaxAbsF F
f
hasMinMaxAbsF F
FTrue = Bool
False
hasMinMaxAbsF F
FFalse = Bool
False
replaceEInE :: E -> E -> E -> E
replaceEInE :: E -> E -> E -> E
replaceEInE E
eContainingE E
eToFind E
eToReplace =
if E
eContainingE E -> E -> Bool
forall a. Eq a => a -> a -> Bool
P.== E
eToFind
then E
eToReplace
else
case E
eContainingE of
EBinOp BinOp
op E
e1 E
e2 -> BinOp -> E -> E -> E
EBinOp BinOp
op (E -> E -> E -> E
replaceEInE E
e1 E
eToFind E
eToReplace) (E -> E -> E -> E
replaceEInE E
e2 E
eToFind E
eToReplace)
EUnOp UnOp
op E
e -> UnOp -> E -> E
EUnOp UnOp
op (E -> E -> E -> E
replaceEInE E
e E
eToFind E
eToReplace)
Float32 RoundingMode
rnd E
e -> RoundingMode -> E -> E
Float32 RoundingMode
rnd (E -> E -> E -> E
replaceEInE E
e E
eToFind E
eToReplace)
Float64 RoundingMode
rnd E
e -> RoundingMode -> E -> E
Float64 RoundingMode
rnd (E -> E -> E -> E
replaceEInE E
e E
eToFind E
eToReplace)
Float RoundingMode
rnd E
e -> RoundingMode -> E -> E
Float64 RoundingMode
rnd (E -> E -> E -> E
replaceEInE E
e E
eToFind E
eToReplace)
RoundToInteger RoundingMode
rnd E
e -> RoundingMode -> E -> E
RoundToInteger RoundingMode
rnd (E -> E -> E -> E
replaceEInE E
e E
eToFind E
eToReplace)
PowI E
e Integer
i -> E -> Integer -> E
PowI (E -> E -> E -> E
replaceEInE E
e E
eToFind E
eToReplace) Integer
i
Lit Rational
_ -> E
eContainingE
Var String
_ -> E
eContainingE
E
Pi -> E
eContainingE
replaceEInF :: F -> E -> E -> F
replaceEInF :: F -> E -> E -> F
replaceEInF F
fContainingE E
eToFind E
eToReplace =
case F
fContainingE of
FConn Conn
op F
f1 F
f2 -> Conn -> F -> F -> F
FConn Conn
op (F -> E -> E -> F
replaceEInF F
f1 E
eToFind E
eToReplace) (F -> E -> E -> F
replaceEInF F
f2 E
eToFind E
eToReplace)
FComp Comp
op E
e1 E
e2 -> Comp -> E -> E -> F
FComp Comp
op (E -> E -> E -> E
replaceEInE E
e1 E
eToFind E
eToReplace) (E -> E -> E -> E
replaceEInE E
e2 E
eToFind E
eToReplace)
FNot F
f -> F -> F
FNot (F -> F) -> F -> F
forall a b. (a -> b) -> a -> b
$ F -> E -> E -> F
replaceEInF F
f E
eToFind E
eToReplace
F
FTrue -> F
FTrue
F
FFalse -> F
FFalse
normalizeBoolean :: F -> F
normalizeBoolean :: F -> F
normalizeBoolean F
form =
if F
form F -> F -> Bool
forall a. Eq a => a -> a -> Bool
P.== F
simplifiedForm
then F
simplifiedForm
else F -> F
normalizeBoolean F
simplifiedForm
where
simplifiedForm :: F
simplifiedForm = F -> F
aggressiveSimplify (F -> F) -> F -> F
forall a b. (a -> b) -> a -> b
$ F -> F
simplifyF (F -> F) -> F -> F
forall a b. (a -> b) -> a -> b
$ F -> F
normalizeToOr (F -> F) -> F -> F
forall a b. (a -> b) -> a -> b
$ F -> F
aux (F -> F) -> F -> F
forall a b. (a -> b) -> a -> b
$ F -> F
simplifyF F
form
normalizeToOr :: F -> F
normalizeToOr F
f =
let
convertAndToOr :: F -> F
convertAndToOr (FConn Conn
And F
x F
y) = F -> F
FNot (F -> F) -> F -> F
forall a b. (a -> b) -> a -> b
$ Conn -> F -> F -> F
FConn Conn
Or (F -> F
FNot F
x) (F -> F) -> F -> F
forall a b. (a -> b) -> a -> b
$ F -> F
convertAndToOr (F -> F
FNot F
y)
convertAndToOr (FConn Conn
Or F
x F
y) = Conn -> F -> F -> F
FConn Conn
Or (F -> F
convertAndToOr F
x) (F -> F
convertAndToOr F
y)
convertAndToOr F
y = F
y
in
F -> F
convertAndToOr F
f
aggressiveSimplify :: F -> F
aggressiveSimplify (FConn Conn
Or F
x f :: F
f@(FNot (FConn Conn
Or F
y F
z)))
| F
x F -> F -> Bool
forall a. Eq a => a -> a -> Bool
P.== F
y = F -> F
aggressiveSimplify (Conn -> F -> F -> F
FConn Conn
Or F
x (F -> F
FNot F
z))
| F
x F -> F -> Bool
forall a. Eq a => a -> a -> Bool
P.== F
z = F -> F
aggressiveSimplify (Conn -> F -> F -> F
FConn Conn
Or F
x (F -> F
FNot F
y))
| Bool
otherwise = Conn -> F -> F -> F
FConn Conn
Or (F -> F
aggressiveSimplify F
x) (F -> F
aggressiveSimplify F
f)
aggressiveSimplify (FConn Conn
Or f :: F
f@(FNot (FConn Conn
Or F
y F
z)) F
x)
| F
x F -> F -> Bool
forall a. Eq a => a -> a -> Bool
P.== F
y = F -> F
aggressiveSimplify (Conn -> F -> F -> F
FConn Conn
Or (F -> F
FNot F
z) F
x)
| F
x F -> F -> Bool
forall a. Eq a => a -> a -> Bool
P.== F
z = F -> F
aggressiveSimplify (Conn -> F -> F -> F
FConn Conn
Or (F -> F
FNot F
y) F
x)
| Bool
otherwise = Conn -> F -> F -> F
FConn Conn
Or (F -> F
aggressiveSimplify F
f) (F -> F
aggressiveSimplify F
x)
aggressiveSimplify (FNot (FNot F
f)) = F -> F
aggressiveSimplify F
f
aggressiveSimplify F
f = F
f
aux :: F -> F
aux (FConn Conn
Impl F
x F
y) = F -> F
aux (F -> F) -> F -> F
forall a b. (a -> b) -> a -> b
$ Conn -> F -> F -> F
FConn Conn
Or (F -> F
FNot F
x) F
y
aux (FNot f :: F
f@(FConn Conn
Impl F
x F
y)) = F -> F
aux (F -> F
FNot (F -> F
aux F
f))
aux (FNot (FConn Conn
Or F
x F
y)) = F -> F
aux (Conn -> F -> F -> F
FConn Conn
And (F -> F
FNot F
x) (F -> F
FNot F
y))
aux (FNot (FConn Conn
And F
x F
y)) = F -> F
aux (Conn -> F -> F -> F
FConn Conn
Or (F -> F
FNot F
x) (F -> F
FNot F
y))
aux (FConn Conn
Or F
x F
y) = Conn -> F -> F -> F
FConn Conn
Or (F -> F
aux F
x) (F -> F
aux F
y)
aux (FConn Conn
And F
x F
y) = Conn -> F -> F -> F
FConn Conn
And (F -> F
aux F
x) (F -> F
aux F
y)
aux (FNot (FNot F
f)) = F -> F
aux F
f
aux F
f = F
f