module PropaFP.Translators.FPTaylor where

import MixedTypesNumPrelude

import PropaFP.Expression

import Data.List
import Data.Ratio
import System.IO.Unsafe (unsafePerformIO)
import PropaFP.VarMap

import System.IO
import Debug.Trace
import Data.Scientific
import AERN2.MP.Precision
import AERN2.MP.Ball (piBallP)
import Data.Bifunctor

-- | All variables must appear in the VarMap
expressionToFPTaylor :: E -> String
expressionToFPTaylor :: E -> String
expressionToFPTaylor (EBinOp BinOp
op E
e1 E
e2) =
  case BinOp
op of
    BinOp
Add -> String
"(" String -> String -> String
forall a. [a] -> [a] -> [a]
++ E -> String
expressionToFPTaylor E
e1 String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
" + " String -> String -> String
forall a. [a] -> [a] -> [a]
++ E -> String
expressionToFPTaylor E
e2 String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
")"
    BinOp
Sub -> String
"(" String -> String -> String
forall a. [a] -> [a] -> [a]
++ E -> String
expressionToFPTaylor E
e1 String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
" - " String -> String -> String
forall a. [a] -> [a] -> [a]
++ E -> String
expressionToFPTaylor E
e2 String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
")"
    BinOp
Mul -> String
"(" String -> String -> String
forall a. [a] -> [a] -> [a]
++ E -> String
expressionToFPTaylor E
e1 String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
" * " String -> String -> String
forall a. [a] -> [a] -> [a]
++ E -> String
expressionToFPTaylor E
e2 String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
")"
    BinOp
Div -> String
"(" String -> String -> String
forall a. [a] -> [a] -> [a]
++ E -> String
expressionToFPTaylor E
e1 String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
" / " String -> String -> String
forall a. [a] -> [a] -> [a]
++ E -> String
expressionToFPTaylor E
e2 String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
")"
    BinOp
Mod -> String
"(" String -> String -> String
forall a. [a] -> [a] -> [a]
++ E -> String
expressionToFPTaylor E
e1 String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
" / " String -> String -> String
forall a. [a] -> [a] -> [a]
++ E -> String
expressionToFPTaylor E
e2 String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
")" -- FIXME: not safe
    BinOp
Min ->
      let
        fpE1 :: String
fpE1 = E -> String
expressionToFPTaylor E
e1
        fpE2 :: String
fpE2 = E -> String
expressionToFPTaylor E
e2
      in
        String
"((" String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
fpE1 String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
" + " String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
fpE2 String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
" - " String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
"|" String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
fpE1 String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
" - " String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
fpE2 String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
"|) / 2)"
    BinOp
Max ->
      let
        fpE1 :: String
fpE1 = E -> String
expressionToFPTaylor E
e1
        fpE2 :: String
fpE2 = E -> String
expressionToFPTaylor E
e2
      in
        String
"((" String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
fpE1 String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
" + " String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
fpE2 String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
" + " String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
"|" String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
fpE1 String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
" - " String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
fpE2 String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
"|) / 2)"
    BinOp
Pow -> String -> String
forall a. HasCallStack => String -> a
error String
"FPTaylor does not support powers"
      -- case e2 of
      --   Lit rat -> 
      --     if denominator rat == 1
      --       then expressionToFPTaylor (PowI e1 (numerator rat)) 
      --       else error "FPTaylor does not support non-integer powers"
      --   _ ->     error "FPTaylor does not support non-integer powers"
expressionToFPTaylor (EUnOp UnOp
op E
e) =
    case UnOp
op of
    UnOp
Sqrt -> String
"sqrt(" String -> String -> String
forall a. [a] -> [a] -> [a]
++ E -> String
expressionToFPTaylor E
e String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
")"
    UnOp
Negate -> String
"(-1 * " String -> String -> String
forall a. [a] -> [a] -> [a]
++ E -> String
expressionToFPTaylor E
e String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
")"
    UnOp
Abs -> String
"|" String -> String -> String
forall a. [a] -> [a] -> [a]
++ E -> String
expressionToFPTaylor E
e String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
"|"
    UnOp
Sin -> String
"sin(" String -> String -> String
forall a. [a] -> [a] -> [a]
++ E -> String
expressionToFPTaylor E
e String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
")"
    UnOp
Cos -> String
"cos(" String -> String -> String
forall a. [a] -> [a] -> [a]
++ E -> String
expressionToFPTaylor E
e String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
")"
expressionToFPTaylor E
Pi         = String
"(4 * atan(1))"
expressionToFPTaylor (PowI E
e Integer
i) = String -> String
forall a. HasCallStack => String -> a
error String
"FPTaylor does not support powers" --TODO: Is it safe to change these to the equivalent with multiplications? A: Depends on SPARK power definition
expressionToFPTaylor (Lit Rational
r) = Rational -> String
showFrac Rational
r
expressionToFPTaylor (Var String
v) = String
v
expressionToFPTaylor (Float32 RoundingMode
mode E
e) = 
  case RoundingMode
mode of
    RoundingMode
RNE -> String
"rnd32(" String -> String -> String
forall a. [a] -> [a] -> [a]
++ E -> String
expressionToFPTaylor E
e String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
")"
    RoundingMode
RTP -> String
"rnd32_up(" String -> String -> String
forall a. [a] -> [a] -> [a]
++ E -> String
expressionToFPTaylor E
e String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
")"
    RoundingMode
RTN -> String
"rnd32_down(" String -> String -> String
forall a. [a] -> [a] -> [a]
++ E -> String
expressionToFPTaylor E
e String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
")"
    RoundingMode
RTZ -> String
"rnd32_0(" String -> String -> String
forall a. [a] -> [a] -> [a]
++ E -> String
expressionToFPTaylor E
e String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
")"
    RoundingMode
RNA -> String
"rnd32(" String -> String -> String
forall a. [a] -> [a] -> [a]
++ E -> String
expressionToFPTaylor E
e String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
")" -- We can treat RNA like RNE. See Rounding section here: https://github.com/soarlab/FPTaylor/blob/develop/REFERENCE.md
expressionToFPTaylor (Float64 RoundingMode
mode E
e) = 
  case RoundingMode
mode of
    RoundingMode
RNE -> String
"rnd64(" String -> String -> String
forall a. [a] -> [a] -> [a]
++ E -> String
expressionToFPTaylor E
e String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
")"
    RoundingMode
RTP -> String
"rnd64_up(" String -> String -> String
forall a. [a] -> [a] -> [a]
++ E -> String
expressionToFPTaylor E
e String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
")"
    RoundingMode
RTN -> String
"rnd64_down(" String -> String -> String
forall a. [a] -> [a] -> [a]
++ E -> String
expressionToFPTaylor E
e String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
")"
    RoundingMode
RTZ -> String
"rnd64_0(" String -> String -> String
forall a. [a] -> [a] -> [a]
++ E -> String
expressionToFPTaylor E
e String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
")"
    RoundingMode
RNA -> String
"rnd(" String -> String -> String
forall a. [a] -> [a] -> [a]
++ E -> String
expressionToFPTaylor E
e String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
")" -- We can treat RNA like RNE. See Rounding section here: https://github.com/soarlab/FPTaylor/blob/develop/REFERENCE.md
expressionToFPTaylor e :: E
e@(Float RoundingMode
_ E
_) = String -> String
forall a. HasCallStack => String -> a
error String
"Float type with no precision found when translating to FPTaylor: " String -> String -> String
forall a. [a] -> [a] -> [a]
++ E -> String
forall a. Show a => a -> String
show E
e
expressionToFPTaylor (RoundToInteger RoundingMode
mode E
e) = E -> String
expressionToFPTaylor E
e -- FIXME: is this ok because we are calculating abs error?
                                                                      -- alternative solution: manually add rounding logic for each case. possible without Ifs?
                                                                      -- This is ok for now
-- expressionToFPTaylor (Float e s) = "rnd32(" ++ expressionToFPTaylor e ++ ")" --TODO: FPTaylor only supports 16,32,64,128 floats. Use these numbers in PP2?

variableBoundsToFPTaylor :: VarMap -> String
variableBoundsToFPTaylor :: VarMap -> String
variableBoundsToFPTaylor [] = String
""
variableBoundsToFPTaylor ((String
v, (Rational
l, Rational
r)) : VarMap
vs) = String
"real " String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
v String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
" in [" String -> String -> String
forall a. [a] -> [a] -> [a]
++ Rational -> String
showFrac Rational
l String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
", " String -> String -> String
forall a. [a] -> [a] -> [a]
++ Rational -> String
showFrac Rational
r String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
"];\n" String -> String -> String
forall a. [a] -> [a] -> [a]
++ VarMap -> String
variableBoundsToFPTaylor VarMap
vs
  where

showFrac :: Rational -> [Char]
showFrac :: Rational -> String
showFrac Rational
rat = if Integer
den Integer -> Rational -> EqCompareType Integer Rational
forall a b. HasEqAsymmetric a b => a -> b -> EqCompareType a b
== Rational
1.0 then Integer -> String
forall a. Show a => a -> String
show Integer
num else Integer -> String
forall a. Show a => a -> String
show Integer
num String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
" / " String -> String -> String
forall a. [a] -> [a] -> [a]
++ Integer -> String
forall a. Show a => a -> String
show Integer
den
  where
    num :: Integer
num = Rational -> Integer
forall a. Ratio a -> a
numerator Rational
rat
    den :: Integer
den = Rational -> Integer
forall a. Ratio a -> a
denominator Rational
rat

expressionWithVarMapToFPTaylor :: E -> VarMap -> String
expressionWithVarMapToFPTaylor :: E -> VarMap -> String
expressionWithVarMapToFPTaylor E
e VarMap
vm =
  String
"Variables\n" String -> String -> String
forall a. [a] -> [a] -> [a]
++ VarMap -> String
variableBoundsToFPTaylor VarMap
vm String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
"\nExpressions\n" String -> String -> String
forall a. [a] -> [a] -> [a]
++ E -> String
expressionToFPTaylor E
e String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
";"

-- parseFPTaylorOutput :: String -> Rational
-- parseFPTaylorOutput output =
--   case elemIndex "(exact):" wordsOutput of
--     Just i -> wordsOutput !! (i + 1)
--   where
--     wordsOutput = words output  

-- "1.788139e-07"
-- "1788140 % 10^-13"

-- To parse the left side:
--  Store length of string
--  Find position of dot
--  remove dot
--  parse integer
--  Add one to compensate for missing digits
--  divide integer using position of dot and length of string to get the rational we want

parseFPTaylorRational :: String -> Maybe Rational
parseFPTaylorRational :: String -> Maybe Rational
parseFPTaylorRational String
output = Maybe Rational
mr
  where
    mr :: Maybe Rational
mr = Scientific -> Rational
forall a. Real a => a -> Rational
toRational (Scientific -> Rational)
-> (String -> Scientific) -> String -> Rational
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (String -> Scientific
forall a. Read a => String -> a
read :: String -> Scientific) (String -> Rational) -> Maybe String -> Maybe Rational
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [String] -> Maybe String
findErrorBound [String]
outputList

    outputList :: [String]
outputList = String -> [String]
words String
output

    findErrorBound :: [String] -> Maybe String
    findErrorBound :: [String] -> Maybe String
findErrorBound [] = Maybe String
forall a. Maybe a
Nothing
    findErrorBound (String
"Absolute" : String
"error" : String
"(exact):" : String
errorBound : [String]
_) = String -> Maybe String
forall a. a -> Maybe a
Just String
errorBound
    findErrorBound (String
_ : [String]
xs) = [String] -> Maybe String
findErrorBound [String]
xs
    -- ePos = Data.List.elemIndex 'e' output
    -- (decimal, exponentWithE) = Data.List.splitAt (ePos) output
    -- exponent = tail exponentWithE
    -- exponentInt = read exponent --Could throw exception

testOutput :: String 
testOutput :: String
testOutput = 
  String
"Loading configuration file: /home/junaid/Research/git/FPTaylor/default.cfg \
  \FPTaylor, version 0.9.2+dev \

  \Loading: heronInit1PlusXDiv1 copy.txt \
  \Processing: Expression 1 \

  \************************************* \
  \Taylor form for: rnd32((1 + rnd32((X / 1)))) \

  \Conservative bound: [1.500000, 3.000000] \

  \Simplified rounding: rnd[32,ne,1.00,-24,0]((1 + rnd32((X / 1)))) \
  \Building Taylor forms... \
  \Simplifying Taylor forms... \
  \success \
  \v0 = (1 + (X * (1 / 1))) \
  \-1 (9): exp = -24: (1/5070602400912917605986812821504) \
  \1 (3): exp = -24: floor_power2(((X * (1 / 1)) + 0)) \
  \2 (5): exp = -24: floor_power2(((1 + (X * (1 / 1))) + interval(-5.96046447753906382349e-08, 5.96046447753906382349e-08))) \

  \Corresponding original subexpressions: \
  \1: rnd32((X / 1)) \
  \2: rnd[32,ne,1.00,-24,0]((1 + rnd32((X / 1)))) \

  \bounds: [1.500000e+00, 3.000000e+00] \

  \Computing absolute errors \
  \-1: exp = -24: 1.972152e-31 (low = 1.972152e-31, subopt = 0.0%) \

  \Solving the exact optimization problem \
  \exact bound (exp = -24): 3.000000e+00 (low = 3.000000e+00, subopt = 0.0%) \
  \total2: 1.175494e-38 (low = 1.175494e-38, subopt = 0.0%) \
  \exact total: 1.788139e-07 (low = 1.788139e-07, subopt = 0.0%) \

  \Elapsed time: 0.36412 \
  \************************************* \

  \------------------------------------------------------------------------------- \
  \Problem: Expression 1 \

  \Optimization lower bounds for error models: \
  \The absolute error model (exact): 1.788139e-07 (suboptimality = 0.0%) \
 
  \Bounds (without rounding): [1.500000e+00, 3.000000e+00] \
  \Bounds (floating-point): [1.49999982118606545178e+00, 3.00000017881393477026e+00] \
 
  \Absolute error (exact): 1.788139e-07 \
 
  \Elapsed time: 0.36 \
 
 
 
  \"