module PropaFP.EliminateFloats where
import MixedTypesNumPrelude
import PropaFP.Expression
import PropaFP.Translators.FPTaylor
import System.Process
import System.IO.Unsafe
import PropaFP.VarMap (VarMap, prettyShowVarMap)
import System.Exit
import System.IO.Temp
import GHC.IO.Handle
removeFloats :: E -> E
removeFloats :: E -> E
removeFloats (Float RoundingMode
_ E
e) = E -> E
removeFloats E
e
removeFloats (Float32 RoundingMode
_ E
e) = E -> E
removeFloats E
e
removeFloats (Float64 RoundingMode
_ E
e) = E -> E
removeFloats E
e
removeFloats (EBinOp BinOp
op E
e1 E
e2) = BinOp -> E -> E -> E
EBinOp BinOp
op (E -> E
removeFloats E
e1) (E -> E
removeFloats E
e2)
removeFloats (EUnOp UnOp
op E
e) = UnOp -> E -> E
EUnOp UnOp
op (E -> E
removeFloats E
e)
removeFloats (PowI E
e Integer
i) = E -> Integer -> E
PowI (E -> E
removeFloats E
e) Integer
i
removeFloats (Lit Rational
v) = Rational -> E
Lit Rational
v
removeFloats (Var String
v) = String -> E
Var String
v
removeFloats E
Pi = E
Pi
removeFloats (RoundToInteger RoundingMode
m E
e) = RoundingMode -> E -> E
RoundToInteger RoundingMode
m (E -> E
removeFloats E
e)
eliminateFloatsF :: F -> VarMap -> Bool -> FilePath -> IO F
eliminateFloatsF :: F -> VarMap -> Bool -> String -> IO F
eliminateFloatsF F
f VarMap
varMap Bool
strengthenFormula String
fptaylorPath =
F -> Bool -> IO F
aux F
f Bool
strengthenFormula
where
aux :: F -> Bool -> IO F
aux :: F -> Bool -> IO F
aux (FConn Conn
Impl F
context F
goal) Bool
strengthenFormula =
Conn -> F -> F -> F
FConn Conn
Impl
(F -> F -> F) -> IO F -> IO (F -> F)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> F -> Bool -> IO F
aux F
context (Bool -> NegType Bool
forall t. CanNeg t => t -> NegType t
not Bool
strengthenFormula)
IO (F -> F) -> IO F -> IO F
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> F -> Bool -> IO F
aux F
goal Bool
strengthenFormula
aux (FNot F
f) Bool
strengthenFormula = F -> F
FNot (F -> F) -> IO F -> IO F
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> F -> Bool -> IO F
aux F
f (Bool -> NegType Bool
forall t. CanNeg t => t -> NegType t
not Bool
strengthenFormula)
aux (FComp Comp
op E
e1 E
e2) Bool
strengthenFormula =
case Comp
op of
Comp
Gt -> Comp -> E -> E -> F
FComp Comp
op (E -> E -> F) -> IO E -> IO (E -> F)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> E -> Bool -> IfThenElseType Bool (IO E)
eliminateFloatsFromExpression E
e1 Bool
strengthenFormula IO (E -> F) -> IO E -> IO F
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> E -> Bool -> IfThenElseType Bool (IO E)
eliminateFloatsFromExpression E
e2 (Bool -> NegType Bool
forall t. CanNeg t => t -> NegType t
not Bool
strengthenFormula)
Comp
Ge -> Comp -> E -> E -> F
FComp Comp
op (E -> E -> F) -> IO E -> IO (E -> F)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> E -> Bool -> IfThenElseType Bool (IO E)
eliminateFloatsFromExpression E
e1 Bool
strengthenFormula IO (E -> F) -> IO E -> IO F
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> E -> Bool -> IfThenElseType Bool (IO E)
eliminateFloatsFromExpression E
e2 (Bool -> NegType Bool
forall t. CanNeg t => t -> NegType t
not Bool
strengthenFormula)
Comp
Lt -> Comp -> E -> E -> F
FComp Comp
op (E -> E -> F) -> IO E -> IO (E -> F)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> E -> Bool -> IfThenElseType Bool (IO E)
eliminateFloatsFromExpression E
e1 (Bool -> NegType Bool
forall t. CanNeg t => t -> NegType t
not Bool
strengthenFormula) IO (E -> F) -> IO E -> IO F
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> E -> Bool -> IfThenElseType Bool (IO E)
eliminateFloatsFromExpression E
e2 Bool
strengthenFormula
Comp
Le -> Comp -> E -> E -> F
FComp Comp
op (E -> E -> F) -> IO E -> IO (E -> F)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> E -> Bool -> IfThenElseType Bool (IO E)
eliminateFloatsFromExpression E
e1 (Bool -> NegType Bool
forall t. CanNeg t => t -> NegType t
not Bool
strengthenFormula) IO (E -> F) -> IO E -> IO F
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> E -> Bool -> IfThenElseType Bool (IO E)
eliminateFloatsFromExpression E
e2 Bool
strengthenFormula
Comp
Eq -> F -> Bool -> IO F
aux (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)) Bool
strengthenFormula
aux (FConn Conn
op F
e1 F
e2) Bool
strengthenFormula = Conn -> F -> F -> F
FConn Conn
op (F -> F -> F) -> IO F -> IO (F -> F)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> F -> Bool -> IO F
aux F
e1 Bool
strengthenFormula IO (F -> F) -> IO F -> IO F
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> F -> Bool -> IO F
aux F
e2 Bool
strengthenFormula
aux F
FTrue Bool
_ = F -> IO F
forall (m :: * -> *) a. Monad m => a -> m a
return F
FTrue
aux F
FFalse Bool
_ = F -> IO F
forall (m :: * -> *) a. Monad m => a -> m a
return F
FFalse
eliminateFloatsFromExpression :: E -> Bool -> IfThenElseType Bool (IO E)
eliminateFloatsFromExpression E
e Bool
subtractError =
if E -> Bool
hasFloatE E
e
then do
Rational
absError <- E -> VarMap -> String -> IO Rational
findAbsoluteErrorUsingFPTaylor E
e VarMap
varMap String
fptaylorPath
let eWithoutFloats :: E
eWithoutFloats = E -> E
removeFloats E
e
if Bool
subtractError
then E -> IO E
forall (m :: * -> *) a. Monad m => a -> m a
return (E -> IO E) -> E -> IO E
forall a b. (a -> b) -> a -> b
$ BinOp -> E -> E -> E
EBinOp BinOp
Sub E
eWithoutFloats (E -> E) -> E -> E
forall a b. (a -> b) -> a -> b
$ Rational -> E
Lit Rational
absError
else E -> IO E
forall (m :: * -> *) a. Monad m => a -> m a
return (E -> IO E) -> E -> IO E
forall a b. (a -> b) -> a -> b
$ BinOp -> E -> E -> E
EBinOp BinOp
Add E
eWithoutFloats (E -> E) -> E -> E
forall a b. (a -> b) -> a -> b
$ Rational -> E
Lit Rational
absError
else
E -> IO E
forall (m :: * -> *) a. Monad m => a -> m a
return E
e
findAbsoluteErrorUsingFPTaylor :: E -> VarMap -> FilePath -> IO Rational
findAbsoluteErrorUsingFPTaylor :: E -> VarMap -> String -> IO Rational
findAbsoluteErrorUsingFPTaylor E
e VarMap
varMap String
fptaylorPath =
do
(ExitCode
exitCode, String
output, String
errDetails) <- String
-> (String -> Handle -> IO (ExitCode, String, String))
-> IO (ExitCode, String, String)
forall (m :: * -> *) a.
(MonadIO m, MonadMask m) =>
String -> (String -> Handle -> m a) -> m a
withSystemTempFile String
"fptaylor" String -> Handle -> IO (ExitCode, String, String)
handleFPTaylorFile
case ExitCode
exitCode of
ExitCode
ExitSuccess ->
case String -> Maybe Rational
parseFPTaylorRational String
output of
Just Rational
result -> Rational -> IO Rational
forall (m :: * -> *) a. Monad m => a -> m a
return Rational
result
Maybe Rational
Nothing -> String -> IO Rational
forall a. HasCallStack => String -> a
error (String -> IO Rational) -> String -> IO Rational
forall a b. (a -> b) -> a -> b
$ String
"Could not parse FPTaylor output" String -> String -> String
forall a. [a] -> [a] -> [a]
++ String -> String
forall a. Show a => a -> String
show String
output
ExitFailure Int
_ -> String -> IO Rational
forall a. HasCallStack => String -> a
error (String -> IO Rational) -> String -> IO Rational
forall a b. (a -> b) -> a -> b
$ String
"Error when running FPTaylor on generated fptaylor.txt. Error message: " String -> String -> String
forall a. [a] -> [a] -> [a]
++ String -> String
forall a. Show a => a -> String
show String
errDetails
where
fptaylorInput :: String
fptaylorInput = E -> VarMap -> String
expressionWithVarMapToFPTaylor E
e VarMap
varMap
handleFPTaylorFile :: String -> Handle -> IO (ExitCode, String, String)
handleFPTaylorFile String
filePath Handle
fileHandle =
do
Handle -> String -> IO ()
hPutStr Handle
fileHandle String
fptaylorInput
String
_ <- Handle -> IO String
hGetContents Handle
fileHandle
String -> [String] -> String -> IO (ExitCode, String, String)
readProcessWithExitCode String
fptaylorPath [String
filePath] []