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)

-- Bool True means 'strengthen' the formula, i.e. rnd(x) >= rnd(y) becomes x - rndErrorX >= y + rndErrorY.
-- Bool False means 'weaken' the formula , i.e. rnd(x) >= rnd(y) becomes x + rndErrorX >= y - rndErrorY
-- Eqs are turned into <= and >=, and then floats are eliminated
-- TODO: Test Max,Min
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

-- |Made for Float32/64 expressions
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
    -- fptaylorFile = "fptaylor.txt"
    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 -- Ensure handler is finished writing before calling FPTaylor
        String -> [String] -> String -> IO (ExitCode, String, String)
readProcessWithExitCode String
fptaylorPath [String
filePath] []