{-# 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)
-- | The E type represents the inequality: expression :: E >= 0
-- TODO: Add rounding operator with certain epsilon/floating-point type
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)

-- TODO: Could make prover work on 'Comp E E' (call it EComp)
-- Other method, add flag to E, whether or not it is strict

-- | The F type is used to specify comparisons between E types
-- and logical connectives between F types
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
          -- PowI    <$> subE <*> fmap getPositive (arbitrary :: Gen (Positive Integer)) -- We do not allow Floats here
        ]
        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]
          -- subE = eGenerator (pred n)

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]

-- data Comp = Gt | Ge | Lt | Le | Eq
--   deriving (Show, P.Eq)

-- data Conn = And | Or | Impl | Equiv
--   deriving (Show, P.Eq)

-- -- | The F type is used to specify comparisons between E types
-- -- and logical connectives between F types
-- data F = FComp Comp E E | FConn Conn F F | FNot F | FTrue | FFalse
--   deriving (Show, P.Eq)

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)))
-- Note, does not generate FTrue, FFalse

flipStrictness :: ESafe -> ESafe
flipStrictness :: ESafe -> ESafe
flipStrictness (EStrict E
e)    = E -> ESafe
ENonStrict E
e
flipStrictness (ENonStrict E
e) = E -> ESafe
EStrict E
e

-- | Equivalent to E * -1
-- Example: ENonStrict e == e >= 0. negateSafeE (ENonStrict e) == e < 0 == -e > 0 == (EStrict (EUnOp Negate 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
extractSafeE :: ESafe -> E
extractSafeE (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) -- !(f1 <= f2) -> (f1 > f2)
      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)) -- !(f1 = f2)
    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) -- f1 <  f2 == f1 - f2 <  0 == -f1 + f2 >= 0
      Comp
Lt -> Bool -> F -> [[ESafe]]
fToECNFB Bool
False (Comp -> E -> E -> F
FComp Comp
Gt E
e2 E
e1) -- f1 <= f2 == f1 - f2 <= 0 == -f1 + f2 >  0
      Comp
Ge -> [[E -> ESafe
ENonStrict (BinOp -> E -> E -> E
EBinOp BinOp
Sub E
e1 E
e2)]]                -- f1 >= f2 == f1 - f2 >= 0 
      Comp
Gt -> [[E -> ESafe
EStrict (BinOp -> E -> E -> E
EBinOp BinOp
Sub E
e1 E
e2)]]      -- f1 >  f2 == f1 - f2 >  0 
      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)) -- f1 = f2 == f1 >= f2 /\ f1 <= f2
    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 -- !(!p \/ q) == p /\ !q
    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 -- [e1 /\ e2 /\ (e3 \/ e4)] ++ [p1 /\ (p2 \/ p3) /\ p4] = [e1 /\ e2 /\ (e3 \/ e4) /\ p1 /\ (p2 \/ p3) /\ p4]
      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] -- [e1 /\ e2 /\ (e3 \/ e4)] \/ [p1 /\ (p2 \/ p3) /\ p4] 
      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 isNegated FTrue  _  = error "fToECNFB for FTrue undefined"  $ Lit 1.0
    -- fToECNFB isNegated FFalse _  = error "fToECNFB for FFalse undefined" $ Lit $ -1.0
    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)) -- !(f1 = f2)
      -- Eq -> [[EStrict (EBinOp Sub e1 e2)], [EStrict (EBinOp Sub e2 e1)]]
    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))
      -- Eq -> [[ENonStrict (EBinOp Sub e1 e2), ENonStrict (EBinOp Sub e2 e1)]]
    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))]]

-- Eq -> fToEDNFB True (FConn And (FComp Ge e1 e2) (FComp Le e1 e2)) -- !(f1 = f2)
-- Eq -> fToEDNFB False (FConn And (FComp Ge e1 e2) (FComp Le e1 e2))

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
        -- e1 < e2
        FComp Comp
Ge E
e1 E
e2 -> [[Comp -> E -> E -> F
FComp Comp
Gt E
e2 E
e1]]
        -- e1 <= e2
        FComp Comp
Gt E
e1 E
e2 -> [[Comp -> E -> E -> F
FComp Comp
Ge E
e2 E
e1]]
        -- e1 > e2
        FComp Comp
Le E
e1 E
e2 -> [[Comp -> E -> E -> F
FComp Comp
Gt E
e1 E
e2]]
        -- e1 >= 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 True  f@FComp {} = [[FNot f]]
    -- fToFDNFB False f@FComp {} = [[f]]
    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" -- Alternatively, this can be false?
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" -- Alternatively, this can be true?
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

-- eSafeCNFToESafeDNF :: [[ESafe]] -> [[ESafe]]
-- eSafeCNFToESafeDNF [] = []
-- eSafeCNFToESafeDNF [disjunction] = map (\term -> [term]) disjunction

-- | Add bounds for any Float expressions
-- addRoundingBounds :: E -> [[E]]
-- addRoundingBounds (Float e significand) = [[exactExpression - machineEpsilon], [exactExpression + machineEpsilon]]
--   where
--     exactExpression = addRoundingBounds e
--     machineEpsilon = 2^(-23)
-- addRoundingBounds e = e

-- | Various rules to simplify expressions
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
-- Simplify Or
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

    -- Collapse x < y OR x = y to x <= y (and similar)
    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)

    -- Eliminate implications with opposing conditions where the RHS is the same, replacing the two implications with the RHS
    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

    -- Collapse x /\ (!x \/ y) into x /\ y
    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)
    -- Collapse (!x \/ y) /\ x into y /\ x
    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)
    -- Collapse x /\ (y \/ !x) into x /\ y
    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)
    -- Collapse (y \/ !x) /\ x into y /\ x
    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))
      -- Collapse (x \/ y) /\ !x into y /\ !x
      | 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))
      -- Collapse (y \/ x) /\ !x into y /\ !x
      | 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))
      -- Turn x /\ !x into false
      | 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))
      -- Collapse !x /\ (x \/ y) into !x /\ y
      | 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)
      -- Collapse !x /\ (y \/ x) into !x /\ y
      | 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)
      -- Turn !x /\ x into false
      | 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)

    -- Collapse x /\ (x -> y) into x /\ y
    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)
    -- Collapse (x -> y) /\ x into y /\ x
    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)

    -- Boolean Rules
    -- And
    -- And contradictions and eliminations
    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)
    -- And collapse to Eq
    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 And f1@(FComp Ge e1 (Var v1)) f2@(FComp Ge (Var v2) e2)) = if e1 P.== e2 && v1 == v2 then simplify (FComp Eq (Var v1) e1) else FConn And (simplify f1) (simplify 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 And f1@(FComp Le e1 (Var v1)) f2@(FComp Le (Var v2) e2)) = if e1 P.== e2 && v1 == v2 then simplify (FComp Eq (Var v1) e1) else FConn And (simplify f1) (simplify 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 And f1@(FComp Ge e1 (Var v1)) f2@(FComp Le e2 (Var v2))) = if e1 P.== e2 && v1 == v2 then simplify (FComp Eq (Var v1) e1) else FConn And (simplify f1) (simplify 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 And f1@(FComp Le (v1) e1) f2@(FComp Ge (v2) e2)) = if e1 P.== e2 && v1 == v2 then simplify (FComp Eq (Var v1) e1) else FConn And (simplify f1) (simplify 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)
    -- Or
    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)
    -- Impl
    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
    -- Impl tautologies and eliminations
    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)

    -- Evaluate rational comparisons
    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


    -- Comp tautologies and eliminations
    -- Eliminate double not
    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)
    -- simplifyF FTrue = error "FTrue was not eliminated"
    -- simplifyF FFalse = error "FFalse was not eliminated"

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)

-- simplify all fs
-- look through, symbolic
-- f fnot, fnot f, etc.
-- nothing else, too complicated


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

    -- look for equalities like x == y and x == -y
    -- x == 0, y == 0
    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


    -- finds equalities in a conjunction (x >= y and y >= x)
    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
        -- say we have x >=y
        FComp Comp
Ge E
l1 E
r1 ->
          case F
f2 of
            -- y >= x is an equality
            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
        -- Returns Nothing if a conjunction contains a contradiction
        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 =
          -- Can be Ge or Gt
          case F
f1 of
            -- say this is x >= y
            FComp Comp
Ge E
l1 E
r1 ->
              case F
f2 of
                -- possible contradictions
                --  y > x
                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
                -- possible = 0
                -- y >= x (then x and y = 0)
                -- FComp Ge l2 r2 ->
                --   if l1 P.== r2 && r1 P.== l2 
                --     then ([FComp Ge l1 (Lit 0.0), FComp Ge (Lit 0.0) l1, FComp Ge l2 (Lit 0.0), FComp Ge (Lit 0.0) l2] ++) <$> aux f1 fs conj
                --     else aux f1 fs conj
                F
_ -> F -> [F] -> [F] -> Maybe [F]
removeContradictions F
f1 [F]
fs [F]
conj
            -- say this is x > y
            FComp Comp
Gt E
l1 E
r1 ->
              case F
f2 of
                -- possible contradictions
                -- y >  x
                -- y >= x
                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 -- Same length means no FNot (FComp Eq _ _)
    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
        -- cWithoutEqWithoutF = delete f cWithoutEq
        -- currentDNFWithoutC = cs ++ dnf
        -- newC1 = FNot (FComp Ge e1 e2) : cWithoutEqWithoutF
        -- newC2 = FNot (FComp Ge e2 e1) : cWithoutEqWithoutF
        -- newDNF = (newC1 : currentDNFWithoutC) ++ (newC2 : currentDNFWithoutC)
    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
-- fDNFToEDNF = map (fConjToE False)
  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

    -- fConjToE :: Bool -> [F] -> [ESafe]
    -- fConjToE _ [] = []
    -- fConjToE True  (FComp Eq e1 e2 : fs) = error "Negated FComp with Eq found in DNF" 
    -- fConjToE False (FComp Eq e1 e2 : fs) = fConjToE False $ [FComp Ge e1 e2, FComp Ge e2 e1] ++ fs
    -- fConjToE False (FComp Ge e1 e2 : fs) = ENonStrict (EBinOp Sub e1 e2)   : fConjToE False fs
    -- fConjToE False (FComp Gt e1 e2 : fs) = EStrict    (EBinOp Sub e1 e2)   : fConjToE False fs
    -- fConjToE False (FComp Le e1 e2 : fs) = fConjToE False $ FComp Ge e2 e1 : fs
    -- fConjToE False (FComp Lt e1 e2 : fs) = fConjToE False $ FComp Gt e2 e1 : fs
    -- fConjToE True  (FComp Ge e1 e2 : fs) = fConjToE False $ FComp Lt e1 e2 : fs
    -- fConjToE True  (FComp Gt e1 e2 : fs) = fConjToE False $ FComp Le e1 e2 : fs
    -- fConjToE True  (FComp Le e1 e2 : fs) = fConjToE False $ FComp Gt e1 e2 : fs
    -- fConjToE True  (FComp Lt e1 e2 : fs) = fConjToE False $ FComp Ge e1 e2 : fs
    -- fConjToE _ (FConn {} : _)           = error "non-atomic f found in DNF"
    -- fConjToE isNegated (FNot f : fs)     = fConjToE (not isNegated) (f : fs)
    -- fConjToE False (FTrue : fs)            = ENonStrict (Lit 1.0) : fConjToE False fs
    -- fConjToE False (FFalse : fs)           = ENonStrict (Lit (-1.0)) : fConjToE False fs
    -- fConjToE True (FTrue : fs)             = ENonStrict (Lit (-1.0)) : fConjToE False fs
    -- fConjToE True (FFalse : fs)            = ENonStrict (Lit 1.0) : fConjToE False 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))

-- | compute the value of E with Vars at specified points
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"

-- | Given a list of qualified Es and points for all Vars,
-- compute a list of valid values. 
-- 
-- A value is the computed result of the second element of 
-- the tuple and is valid if all the expressions in the list 
-- at the first element of the tuple compute to be above 0.
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
    -- |Show a disjunction of expressions > 0 in a human-readable format
    -- This is shown as an OR with each term tabbed in
    -- If there is only one term, the expression is shown without an OR 
    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
    -- |Show a disjunction of expressions > 0 in a human-readable format
    -- This is shown as an OR with each term tabbed in
    -- If there is only one term, the expression is shown without an OR 
    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
    -- |Show a disjunction of expressions > 0 in a human-readable format
    -- This is shown as an OR with each term tabbed in
    -- If there is only one term, the expression is shown without an OR 
    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

-- prettyShowF :: F -> Integer -> String
-- prettyShowF (FComp op e1 e2) numTabs = "\n" ++ concat (replicate numTabs "\t") ++ prettyShowE e1 ++ " " ++ prettyShowComp op ++ " " ++ prettyShowE e2
-- prettyShowF (FConn op f1 f2) numTabs = "\n" ++ concat (replicate numTabs "\t") ++ prettyShowConn op ++ prettyShowF f1 (numTabs + 1) ++ prettyShowF f2 (numTabs + 1)
-- prettyShowF (FNot f)         numTabs = "\n" ++ concat (replicate numTabs "\t") ++ "NOT" ++ prettyShowF f (numTabs + 1)
-- prettyShowF FTrue            numTabs = "\n" ++ concat (replicate numTabs "\t") ++ "True"
-- prettyShowF FFalse           numTabs = "\n" ++ concat (replicate numTabs "\t") ++ "False"

-- pretty show a Why3 VC which is typically a bunch of conjunctions
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"

-- latexShowESafeCNF :: [[ESafe]] -> String
-- latexShowESafeCNF cnf = "AND" ++ concatMap (\d -> "\n\t" ++ prettyShowDisjunction d) cnf
--   where
--     -- |Show a disjunction of expressions > 0 in a human-readable format
--     -- This is shown as an OR with each term tabbed in
--     -- If there is only one term, the expression is shown without an OR 
--     prettyShowDisjunction :: [ESafe] -> String
--     prettyShowDisjunction []  = []
--     prettyShowDisjunction [e'] = 
--       case e' of
--         EStrict e -> prettyShowE e ++ " > 0"
--         ENonStrict e -> prettyShowE e ++ " >= 0"
--     prettyShowDisjunction es  =
--       "OR" ++ 
--       concatMap 
--       (\case
--         EStrict e -> "\n\t\t" ++ prettyShowE e ++ " > 0" 
--         ENonStrict e -> "\n\t\t" ++ prettyShowE e ++ " >= 0")
--       es

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$"

-- |Show an expression in a human-readable format
-- Rationals are converted into doubles
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
")"

-- |Show a conjunction of expressions in a human-readable format
-- This is shown as an AND with each disjunction tabbed in with an OR
-- If there is only one term in a disjunction, the expression is shown without an OR 
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
    -- |Show a disjunction of expressions > 0 in a human-readable format
    -- This is shown as an OR with each term tabbed in
    -- If there is only one term, the expression is shown without an OR 
    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"

-- |Extract all variables in an expression
-- Will not return duplicationes
extractVariablesE :: E -> [String]
extractVariablesE :: E -> [String]
extractVariablesE = [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

-- |Extract all variables in an expression
-- Will not return duplicationes
extractVariablesF :: F -> [String]
extractVariablesF :: F -> [String]
extractVariablesF = [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]
extractVariablesECNF :: [[E]] -> [String]
extractVariablesECNF = [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

-- Replaces implications with ORs, i.e. p -> q becomes !p \/ q
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


    -- When we say False (unsat), the VC MUST be False
    -- When we say True (sat), the VC might not be True
    -- We safely remove variableFreeComparisons by adhering to the above statements
    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

-- |Normalize to and/or
-- aggressively apply elimination rules
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

    -- Turn and/or into or using demorgans laws
    normalizeToOr :: F -> F
normalizeToOr F
f =
      let
        -- convertAndToNegatedOr (FConn And (FNot x) y) = FNot $ FConn Or x $ convertAndToNegatedOr y
        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)
        -- convertAndToNegatedOr (FNot y) = y
        convertAndToOr F
y = F
y
      in
        F -> F
convertAndToOr F
f

    -- Aggressively simplify Ors
    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 (FConn Or x f@(FConn And (FNot x') y)) = if x P.== x' then aggressiveSimplify (FConn Or x y) else (FConn Or (aggressiveSimplify x) (aggressiveSimplify f))
    -- aggressiveSimplify (FConn Or x f@(FConn And y (FNot x'))) = if x P.== x' then aggressiveSimplify (FConn Or x y) else (FConn Or (aggressiveSimplify x) (aggressiveSimplify f))
    -- aggressiveSimplify (FConn Or f@(FConn And (FNot x') y) x) = if x P.== x' then aggressiveSimplify (FConn Or x y) else (FConn Or (aggressiveSimplify f) (aggressiveSimplify x))
    -- aggressiveSimplify (FConn Or f@(FConn And y (FNot x')) x) = if x P.== x' then aggressiveSimplify (FConn Or x y) else (FConn Or (aggressiveSimplify f) (aggressiveSimplify x))
    aggressiveSimplify F
f = F
f

    -- Eliminate implications and distribute FNots
    -- aux (FConn Or x f@(FConn And (FNot x') y)) = if x P.== x' then FConn And x y else FConn Or (aux x) (aux 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