{-# LANGUAGE TupleSections #-}
{-# LANGUAGE LambdaCase #-}
{-# LANGUAGE LambdaCase #-}
module PropaFP.Parsers.Smt where

import MixedTypesNumPrelude hiding (unzip)
import qualified Prelude as P
import System.IO.Unsafe

import PropaFP.Expression

import qualified PropaFP.Parsers.Lisp.Parser as LP
import qualified PropaFP.Parsers.Lisp.DataTypes as LD

import Data.Char (digitToInt)

import Data.Word
import qualified Data.ByteString.Lazy as B
import Data.Binary.Get
import Data.Maybe (mapMaybe)

import PropaFP.VarMap
import PropaFP.DeriveBounds
import PropaFP.EliminateFloats
import PropaFP.Eliminator (minMaxAbsEliminatorECNF, minMaxAbsEliminator)
import Data.List (nub, sort, isPrefixOf, sortBy, partition, foldl')
import Data.List.NonEmpty (unzip)
import Control.Arrow ((&&&))
import Debug.Trace
import PropaFP.Translators.DReal (formulaAndVarMapToDReal)
import Text.Regex.TDFA ( (=~) )
import Data.Ratio
import PropaFP.DeriveBounds
import qualified Data.Map as M
import AERN2.MP (endpoints, mpBallP, prec)

data ParsingMode = Why3 | CNF
parser :: String -> [LD.Expression]
parser :: String -> [Expression]
parser = [Expression] -> [Expression]
LP.analyzeExpressionSequence ([Expression] -> [Expression])
-> (String -> [Expression]) -> String -> [Expression]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [String] -> [Expression]
LP.parseSequence ([String] -> [Expression])
-> (String -> [String]) -> String -> [Expression]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. String -> [String]
LP.tokenize

parseSMT2 :: FilePath -> IO [LD.Expression]
parseSMT2 :: String -> IO [Expression]
parseSMT2 String
filePath = (String -> [Expression]) -> IO String -> IO [Expression]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap String -> [Expression]
parser (IO String -> IO [Expression]) -> IO String -> IO [Expression]
forall a b. (a -> b) -> a -> b
$ String -> IO String
P.readFile String
filePath

-- |Find assertions in a parsed expression
-- Assertions are Application types with the operator being a Variable equal to "assert"
-- Assertions only have one 'operands'
findAssertions :: [LD.Expression] -> [LD.Expression]
findAssertions :: [Expression] -> [Expression]
findAssertions [] = []
-- findAssertions [LD.Application (LD.Variable "assert") [operands]] = [operands]
findAssertions ((LD.Application (LD.Variable String
"assert") [Expression
operands]) : [Expression]
expressions) = Expression
operands Expression -> [Expression] -> [Expression]
forall a. a -> [a] -> [a]
: [Expression] -> [Expression]
findAssertions [Expression]
expressions
-- findAssertions ((LD.Application (LD.Variable var) [operands]) : expressions) = operands : findAssertions expressions
findAssertions (Expression
e : [Expression]
expressions) = [Expression] -> [Expression]
findAssertions [Expression]
expressions

findFunctionInputsAndOutputs :: [LD.Expression] -> [(String, ([String], String))]
findFunctionInputsAndOutputs :: [Expression] -> [(String, ([String], String))]
findFunctionInputsAndOutputs [] = []
findFunctionInputsAndOutputs ((LD.Application (LD.Variable String
"declare-fun") [LD.Variable String
fName, Expression
fInputsAsExpressions, LD.Variable String
fOutputs]) : [Expression]
expressions) =
  (String
fName, (Expression -> [String]
expressionInputsAsString Expression
fInputsAsExpressions, String
fOutputs)) (String, ([String], String))
-> [(String, ([String], String))] -> [(String, ([String], String))]
forall a. a -> [a] -> [a]
: [Expression] -> [(String, ([String], String))]
findFunctionInputsAndOutputs [Expression]
expressions
  where
    expressionInputsAsString :: LD.Expression -> [String]
    expressionInputsAsString :: Expression -> [String]
expressionInputsAsString (LD.Application (LD.Variable String
inputTypeAsString) [Expression]
remainingInputsAsExpression) = String
inputTypeAsString String -> [String] -> [String]
forall a. a -> [a] -> [a]
: (Expression -> [String]) -> [Expression] -> [String]
forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap Expression -> [String]
expressionInputsAsString [Expression]
remainingInputsAsExpression
    expressionInputsAsString (LD.Variable String
inputTypeAsString) = [String
inputTypeAsString]
    expressionInputsAsString Expression
_ = []
findFunctionInputsAndOutputs (Expression
_ : [Expression]
expressions) = [Expression] -> [(String, ([String], String))]
findFunctionInputsAndOutputs [Expression]
expressions

-- |Find function declarations in a parsed expression
-- Function declarations are Application types with the operator being a Variable equal to "declare-fun"
-- Function declarations contain 3 operands
--   - Operand 1 is the name of the function
--   - Operand 2 is an Application type which can be thought of as the parameters of the functions
--     If the function has no paramters, this operand is LD.Null 
--   - Operand 3 is the type of the function
findDeclarations :: [LD.Expression] -> [LD.Expression]
findDeclarations :: [Expression] -> [Expression]
findDeclarations [] = []
findDeclarations (declaration :: Expression
declaration@(LD.Application (LD.Variable String
"declare-fun") [Expression]
_) : [Expression]
expressions) = Expression
declaration Expression -> [Expression] -> [Expression]
forall a. a -> [a] -> [a]
: [Expression] -> [Expression]
findDeclarations [Expression]
expressions
findDeclarations (Expression
_ : [Expression]
expressions) = [Expression] -> [Expression]
findDeclarations [Expression]
expressions

findVariables :: [LD.Expression] -> [(String, String)]
findVariables :: [Expression] -> [(String, String)]
findVariables [] = []
findVariables (LD.Application (LD.Variable String
"declare-const") [LD.Variable String
varName, LD.Variable String
varType] : [Expression]
expressions)
  = (String
varName, String
varType) (String, String) -> [(String, String)] -> [(String, String)]
forall a. a -> [a] -> [a]
: [Expression] -> [(String, String)]
findVariables [Expression]
expressions
findVariables (LD.Application (LD.Variable String
"declare-fun") [LD.Variable String
varName, Expression
LD.Null, LD.Variable String
varType] : [Expression]
expressions)
  = (String
varName, String
varType) (String, String) -> [(String, String)] -> [(String, String)]
forall a. a -> [a] -> [a]
: [Expression] -> [(String, String)]
findVariables [Expression]
expressions
findVariables (Expression
_ : [Expression]
expressions) = [Expression] -> [(String, String)]
findVariables [Expression]
expressions

findIntegerVariables :: [(String, String)] -> [(String, VarType)]
findIntegerVariables :: [(String, String)] -> [(String, VarType)]
findIntegerVariables []           = []
findIntegerVariables ((String
v,String
t) : [(String, String)]
vs) =
  if String
"Int" String -> String -> Bool
forall a. Eq a => [a] -> [a] -> Bool
`isPrefixOf` String
t Bool -> Bool -> AndOrType Bool Bool
forall a b. CanAndOrAsymmetric a b => a -> b -> AndOrType a b
|| String
"int" String -> String -> Bool
forall a. Eq a => [a] -> [a] -> Bool
`isPrefixOf` String
t
    then (String
v, VarType
Integer) (String, VarType) -> [(String, VarType)] -> [(String, VarType)]
forall a. a -> [a] -> [a]
: [(String, String)] -> [(String, VarType)]
findIntegerVariables [(String, String)]
vs
    else [(String, String)] -> [(String, VarType)]
findIntegerVariables [(String, String)]
vs

-- |Finds goals in assertion operands
-- Goals are S-Expressions with a top level 'not'
findGoalsInAssertions :: [LD.Expression] -> [LD.Expression]
findGoalsInAssertions :: [Expression] -> [Expression]
findGoalsInAssertions [] = []
findGoalsInAssertions ((LD.Application (LD.Variable String
operator) [Expression]
operands) : [Expression]
assertions) =
  if String
operator String -> String -> EqCompareType String String
forall a b. HasEqAsymmetric a b => a -> b -> EqCompareType a b
== String
"not"
    then [Expression] -> Expression
forall a. [a] -> a
head [Expression]
operands Expression -> [Expression] -> [Expression]
forall a. a -> [a] -> [a]
: [Expression] -> [Expression]
findGoalsInAssertions [Expression]
assertions -- Take head of operands since not has only one operand
    else [Expression] -> [Expression]
findGoalsInAssertions [Expression]
assertions
findGoalsInAssertions (Expression
_ : [Expression]
assertions) = [Expression] -> [Expression]
findGoalsInAssertions [Expression]
assertions

-- |Takes the last element from a list of assertions
-- We assume that the last element is the goal
takeGoalFromAssertions :: [LD.Expression] -> (LD.Expression, [LD.Expression])
takeGoalFromAssertions :: [Expression] -> (Expression, [Expression])
takeGoalFromAssertions [Expression]
asserts = (Expression
goal, [Expression]
assertsWithoutGoal)
  where
    numberOfAssertions :: Integer
numberOfAssertions = [Expression] -> Integer
forall (t :: * -> *) a. Foldable t => t a -> Integer
length [Expression]
asserts
    goal :: Expression
goal = [Expression] -> Expression
forall a. [a] -> a
last [Expression]
asserts -- FIXME: Unsafe. If asserts is empty, this will fail
    assertsWithoutGoal :: [Expression]
assertsWithoutGoal = Integer -> [Expression] -> [Expression]
forall n a. CanBeInteger n => n -> [a] -> [a]
take (Integer
numberOfAssertions Integer -> Integer -> SubType Integer Integer
forall t1 t2. CanSub t1 t2 => t1 -> t2 -> SubType t1 t2
- Integer
1) [Expression]
asserts

-- safelyTypeExpression :: String -> [(String, ([String], String))] -> E -> E
-- safelyTypeExpression smtFunction functionsWithInputsAndOutputs exactExpression =
--   case lookup smtFunction functionsWithInputsAndOutputs of
--     Just (inputs, output)

-- |Attempts to parse FComp Ops, i.e. parse bool_eq to Just (FComp Eq)
parseFCompOp :: String -> Maybe (E -> E -> F)
parseFCompOp :: String -> Maybe (E -> E -> F)
parseFCompOp String
operator =
  case String
operator of
    String
n
      | String
n String -> [String] -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` [String
">=", String
"fp.geq", String
"oge", String
"oge__logic"] Bool -> Bool -> AndOrType Bool Bool
forall a b. CanAndOrAsymmetric a b => a -> b -> AndOrType a b
|| (String
n String -> String -> Bool
forall source source1 target.
(RegexMaker Regex CompOption ExecOption source,
 RegexContext Regex source1 target) =>
source1 -> source -> target
=~ String
"^bool_ge$|^bool_ge[0-9]+$" :: Bool)     -> (E -> E -> F) -> Maybe (E -> E -> F)
forall a. a -> Maybe a
Just ((E -> E -> F) -> Maybe (E -> E -> F))
-> (E -> E -> F) -> Maybe (E -> E -> F)
forall a b. (a -> b) -> a -> b
$ Comp -> E -> E -> F
FComp Comp
Ge
      | String
n String -> [String] -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` [String
">",  String
"fp.gt", String
"ogt", String
"ogt__logic"] Bool -> Bool -> AndOrType Bool Bool
forall a b. CanAndOrAsymmetric a b => a -> b -> AndOrType a b
|| (String
n String -> String -> Bool
forall source source1 target.
(RegexMaker Regex CompOption ExecOption source,
 RegexContext Regex source1 target) =>
source1 -> source -> target
=~ String
"^bool_gt$|^bool_gt[0-9]+$" :: Bool)      -> (E -> E -> F) -> Maybe (E -> E -> F)
forall a. a -> Maybe a
Just ((E -> E -> F) -> Maybe (E -> E -> F))
-> (E -> E -> F) -> Maybe (E -> E -> F)
forall a b. (a -> b) -> a -> b
$ Comp -> E -> E -> F
FComp Comp
Gt
      | String
n String -> [String] -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` [String
"<=", String
"fp.leq", String
"ole", String
"ole__logic"] Bool -> Bool -> AndOrType Bool Bool
forall a b. CanAndOrAsymmetric a b => a -> b -> AndOrType a b
|| (String
n String -> String -> Bool
forall source source1 target.
(RegexMaker Regex CompOption ExecOption source,
 RegexContext Regex source1 target) =>
source1 -> source -> target
=~ String
"^bool_le$|^bool_le[0-9]+$" :: Bool)     -> (E -> E -> F) -> Maybe (E -> E -> F)
forall a. a -> Maybe a
Just ((E -> E -> F) -> Maybe (E -> E -> F))
-> (E -> E -> F) -> Maybe (E -> E -> F)
forall a b. (a -> b) -> a -> b
$ Comp -> E -> E -> F
FComp Comp
Le
      | String
n String -> [String] -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` [String
"<",  String
"fp.lt", String
"olt", String
"olt__logic"] Bool -> Bool -> AndOrType Bool Bool
forall a b. CanAndOrAsymmetric a b => a -> b -> AndOrType a b
|| (String
n String -> String -> Bool
forall source source1 target.
(RegexMaker Regex CompOption ExecOption source,
 RegexContext Regex source1 target) =>
source1 -> source -> target
=~ String
"^bool_lt$|^bool_lt[0-9]+$" :: Bool)      -> (E -> E -> F) -> Maybe (E -> E -> F)
forall a. a -> Maybe a
Just ((E -> E -> F) -> Maybe (E -> E -> F))
-> (E -> E -> F) -> Maybe (E -> E -> F)
forall a b. (a -> b) -> a -> b
$ Comp -> E -> E -> F
FComp Comp
Lt
      | String
n String -> [String] -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` [String
"=",  String
"fp.eq"] Bool -> Bool -> AndOrType Bool Bool
forall a b. CanAndOrAsymmetric a b => a -> b -> AndOrType a b
|| (String
n String -> String -> Bool
forall source source1 target.
(RegexMaker Regex CompOption ExecOption source,
 RegexContext Regex source1 target) =>
source1 -> source -> target
=~ String
"^bool_eq$|^bool_eq[0-9]+$|^user_eq$|^user_eq[0-9]+$" :: Bool) -> (E -> E -> F) -> Maybe (E -> E -> F)
forall a. a -> Maybe a
Just ((E -> E -> F) -> Maybe (E -> E -> F))
-> (E -> E -> F) -> Maybe (E -> E -> F)
forall a b. (a -> b) -> a -> b
$ Comp -> E -> E -> F
FComp Comp
Eq
      | String
"bool_neq" String -> String -> Bool
forall a. Eq a => [a] -> [a] -> Bool
`isPrefixOf` String
n                                                                        -> (E -> E -> F) -> Maybe (E -> E -> F)
forall a. a -> Maybe a
Just ((E -> E -> F) -> Maybe (E -> E -> F))
-> (E -> E -> F) -> Maybe (E -> E -> F)
forall a b. (a -> b) -> a -> b
$ \E
e1 E
e2 -> F -> F
FNot (Comp -> E -> E -> F
FComp Comp
Eq E
e1 E
e2)
    String
_ -> Maybe (E -> E -> F)
forall a. Maybe a
Nothing

-- parseIte :: LD.Expression -> LD.Expression -> LD.Expression -> Maybe F
parseIte :: Expression
-> Expression
-> Expression
-> [(String, ([String], String))]
-> Maybe (E -> F)
-> Maybe F
parseIte Expression
cond Expression
thenTerm Expression
elseTerm [(String, ([String], String))]
functionsWithInputsAndOutputs Maybe (E -> F)
Nothing =
  case Expression -> [(String, ([String], String))] -> Maybe F
termToF Expression
cond [(String, ([String], String))]
functionsWithInputsAndOutputs of
    Just F
condF -> 
      case (Expression -> [(String, ([String], String))] -> Maybe F
termToF Expression
thenTerm [(String, ([String], String))]
functionsWithInputsAndOutputs, Expression -> [(String, ([String], String))] -> Maybe F
termToF Expression
elseTerm [(String, ([String], String))]
functionsWithInputsAndOutputs) of
        (Just F
thenTermF, Just F
elseTermF) -> 
          F -> Maybe F
forall a. a -> Maybe a
Just (F -> Maybe F) -> F -> Maybe F
forall a b. (a -> b) -> a -> b
$ Conn -> F -> F -> F
FConn Conn
And
            (Conn -> F -> F -> F
FConn Conn
Impl F
condF        F
thenTermF)
            (Conn -> F -> F -> F
FConn Conn
Impl (F -> F
FNot F
condF) F
elseTermF)
        (Maybe F
_, Maybe F
_) -> Maybe F
forall a. Maybe a
Nothing
    Maybe F
Nothing -> Maybe F
forall a. Maybe a
Nothing
parseIte Expression
cond Expression
thenTerm Expression
elseTerm [(String, ([String], String))]
functionsWithInputsAndOutputs (Just E -> F
compTerm) =
  case Expression -> [(String, ([String], String))] -> Maybe F
termToF Expression
cond [(String, ([String], String))]
functionsWithInputsAndOutputs of
    (Just F
condF) ->
      case (Expression -> [(String, ([String], String))] -> Maybe E
termToE Expression
thenTerm [(String, ([String], String))]
functionsWithInputsAndOutputs, Expression -> [(String, ([String], String))] -> Maybe E
termToE Expression
elseTerm [(String, ([String], String))]
functionsWithInputsAndOutputs) of
        (Just E
thenTermE, Just E
elseTermE) ->
          F -> Maybe F
forall a. a -> Maybe a
Just (F -> Maybe F) -> F -> Maybe F
forall a b. (a -> b) -> a -> b
$ Conn -> F -> F -> F
FConn Conn
And
            (Conn -> F -> F -> F
FConn Conn
Impl F
condF            (E -> F
compTerm E
thenTermE))
            (Conn -> F -> F -> F
FConn Conn
Impl (F -> F
FNot F
condF)     (E -> F
compTerm E
elseTermE))
        (Just E
thenTermE, Maybe E
_) ->
          case Expression
elseTerm of
            LD.Application (LD.Variable String
"ite") [Expression
elseCond, Expression
elseThenTerm, Expression
elseElseTerm] ->
              case Expression
-> Expression
-> Expression
-> [(String, ([String], String))]
-> Maybe (E -> F)
-> Maybe F
parseIte Expression
elseCond Expression
elseThenTerm Expression
elseElseTerm [(String, ([String], String))]
functionsWithInputsAndOutputs ((E -> F) -> Maybe (E -> F)
forall a. a -> Maybe a
Just E -> F
compTerm) of
                Just F
elseTermF -> F -> Maybe F
forall a. a -> Maybe a
Just (F -> Maybe F) -> F -> Maybe F
forall a b. (a -> b) -> a -> b
$
                  Conn -> F -> F -> F
FConn Conn
And
                    (Conn -> F -> F -> F
FConn Conn
Impl F
condF        (E -> F
compTerm E
thenTermE))
                    (Conn -> F -> F -> F
FConn Conn
Impl (F -> F
FNot F
condF) F
elseTermF)
                Maybe F
_ -> Maybe F
forall a. Maybe a
Nothing
            Expression
_ -> Maybe F
forall a. Maybe a
Nothing
        (Maybe E
_, Just E
elseTermE) ->
          case Expression
thenTerm of
            LD.Application (LD.Variable String
"ite") [Expression
thenCond, Expression
thenThenTerm, Expression
thenElseTerm] ->
              case Expression
-> Expression
-> Expression
-> [(String, ([String], String))]
-> Maybe (E -> F)
-> Maybe F
parseIte Expression
thenCond Expression
thenThenTerm Expression
thenElseTerm [(String, ([String], String))]
functionsWithInputsAndOutputs ((E -> F) -> Maybe (E -> F)
forall a. a -> Maybe a
Just E -> F
compTerm) of
                Just F
thenTermF -> F -> Maybe F
forall a. a -> Maybe a
Just (F -> Maybe F) -> F -> Maybe F
forall a b. (a -> b) -> a -> b
$
                  Conn -> F -> F -> F
FConn Conn
And
                    (Conn -> F -> F -> F
FConn Conn
Impl F
condF        F
thenTermF)
                    (Conn -> F -> F -> F
FConn Conn
Impl (F -> F
FNot F
condF) (E -> F
compTerm E
elseTermE))
                Maybe F
_ -> Maybe F
forall a. Maybe a
Nothing
            Expression
_ -> Maybe F
forall a. Maybe a
Nothing
        (Maybe E
_, Maybe E
_) -> 
          case (Expression
thenTerm, Expression
elseTerm) of
            (LD.Application (LD.Variable String
"ite") [Expression
thenCond, Expression
thenThenTerm, Expression
thenElseTerm], LD.Application (LD.Variable String
"ite") [Expression
elseCond, Expression
elseThenTerm, Expression
elseElseTerm]) ->
              case (Expression
-> Expression
-> Expression
-> [(String, ([String], String))]
-> Maybe (E -> F)
-> Maybe F
parseIte Expression
thenCond Expression
thenThenTerm Expression
thenElseTerm [(String, ([String], String))]
functionsWithInputsAndOutputs ((E -> F) -> Maybe (E -> F)
forall a. a -> Maybe a
Just E -> F
compTerm), Expression
-> Expression
-> Expression
-> [(String, ([String], String))]
-> Maybe (E -> F)
-> Maybe F
parseIte Expression
elseCond Expression
elseThenTerm Expression
elseElseTerm [(String, ([String], String))]
functionsWithInputsAndOutputs ((E -> F) -> Maybe (E -> F)
forall a. a -> Maybe a
Just E -> F
compTerm)) of
                (Just F
thenTermF, Just F
elseTermF) -> F -> Maybe F
forall a. a -> Maybe a
Just (F -> Maybe F) -> F -> Maybe F
forall a b. (a -> b) -> a -> b
$
                  Conn -> F -> F -> F
FConn Conn
And
                    (Conn -> F -> F -> F
FConn Conn
Impl F
condF        F
thenTermF)
                    (Conn -> F -> F -> F
FConn Conn
Impl (F -> F
FNot F
condF) F
elseTermF)
                (Maybe F
_, Maybe F
_) -> Maybe F
forall a. Maybe a
Nothing
            (Expression
_, Expression
_) -> Maybe F
forall a. Maybe a
Nothing
    Maybe F
Nothing -> Maybe F
forall a. Maybe a
Nothing

termToF :: LD.Expression -> [(String, ([String], String))] -> Maybe F
termToF :: Expression -> [(String, ([String], String))] -> Maybe F
termToF (LD.Application (LD.Variable String
operator) [Expression
op]) [(String, ([String], String))]
functionsWithInputsAndOutputs = -- Single param operators
  case Expression -> [(String, ([String], String))] -> Maybe E
termToE Expression
op [(String, ([String], String))]
functionsWithInputsAndOutputs of -- Ops with E params
    Just E
e ->
      case String
operator of
        String
"fp.isFinite32" ->
          let maxFloat :: MulType Rational Integer
maxFloat = (Rational
2.0 Rational -> Rational -> SubType Rational Rational
forall t1 t2. CanSub t1 t2 => t1 -> t2 -> SubType t1 t2
- (Integer
1Integer -> Integer -> DivType Integer Integer
forall t1 t2. CanDiv t1 t2 => t1 -> t2 -> DivType t1 t2
/(Integer
2Integer -> Integer -> PowType Integer Integer
forall t1 t2. CanPow t1 t2 => t1 -> t2 -> PowType t1 t2
^Integer
23))) Rational -> Integer -> MulType Rational Integer
forall t1 t2. CanMulAsymmetric t1 t2 => t1 -> t2 -> MulType t1 t2
* (Integer
2Integer -> Integer -> PowType Integer Integer
forall t1 t2. CanPow t1 t2 => t1 -> t2 -> PowType t1 t2
^Integer
127)
              minFloat :: NegType Rational
minFloat = Rational -> NegType Rational
forall t. CanNeg t => t -> NegType t
negate Rational
maxFloat
          in
            F -> Maybe F
forall a. a -> Maybe a
Just (F -> Maybe F) -> F -> Maybe F
forall a b. (a -> b) -> a -> b
$ Conn -> F -> F -> F
FConn Conn
And (Comp -> E -> E -> F
FComp Comp
Le (Rational -> E
Lit Rational
minFloat) E
e)  (Comp -> E -> E -> F
FComp Comp
Le E
e (Rational -> E
Lit Rational
maxFloat))
        String
"fp.isFinite64" ->
          let maxFloat :: MulType Rational Integer
maxFloat = (Rational
2.0 Rational -> Rational -> SubType Rational Rational
forall t1 t2. CanSub t1 t2 => t1 -> t2 -> SubType t1 t2
- (Integer
1Integer -> Integer -> DivType Integer Integer
forall t1 t2. CanDiv t1 t2 => t1 -> t2 -> DivType t1 t2
/(Integer
2Integer -> Integer -> PowType Integer Integer
forall t1 t2. CanPow t1 t2 => t1 -> t2 -> PowType t1 t2
^Integer
52))) Rational -> Integer -> MulType Rational Integer
forall t1 t2. CanMulAsymmetric t1 t2 => t1 -> t2 -> MulType t1 t2
* (Integer
2Integer -> Integer -> PowType Integer Integer
forall t1 t2. CanPow t1 t2 => t1 -> t2 -> PowType t1 t2
^Integer
1023)
              minFloat :: NegType Rational
minFloat = Rational -> NegType Rational
forall t. CanNeg t => t -> NegType t
negate Rational
maxFloat
          in
            F -> Maybe F
forall a. a -> Maybe a
Just (F -> Maybe F) -> F -> Maybe F
forall a b. (a -> b) -> a -> b
$ Conn -> F -> F -> F
FConn Conn
And (Comp -> E -> E -> F
FComp Comp
Le (Rational -> E
Lit Rational
minFloat) E
e)  (Comp -> E -> E -> F
FComp Comp
Le E
e (Rational -> E
Lit Rational
maxFloat))
        String
_ -> Maybe F
forall a. Maybe a
Nothing
    Maybe E
Nothing ->
      case Expression -> [(String, ([String], String))] -> Maybe F
termToF Expression
op [(String, ([String], String))]
functionsWithInputsAndOutputs of
        Just F
f ->
          case String
operator of
            String
"not" -> F -> Maybe F
forall a. a -> Maybe a
Just (F -> Maybe F) -> F -> Maybe F
forall a b. (a -> b) -> a -> b
$ F -> F
FNot F
f
            String
_ -> Maybe F
forall a. Maybe a
Nothing
        Maybe F
_ -> Maybe F
forall a. Maybe a
Nothing
termToF (LD.Application (LD.Variable String
operator) [Expression
op1, Expression
op2]) [(String, ([String], String))]
functionsWithInputsAndOutputs = -- Two param operations
  case (Expression -> [(String, ([String], String))] -> Maybe E
termToE Expression
op1 [(String, ([String], String))]
functionsWithInputsAndOutputs, Expression -> [(String, ([String], String))] -> Maybe E
termToE Expression
op2 [(String, ([String], String))]
functionsWithInputsAndOutputs) of
    (Just E
e1, Just E
e2) ->
      case String -> Maybe (E -> E -> F)
parseFCompOp String
operator of
        Just E -> E -> F
fCompOp -> F -> Maybe F
forall a. a -> Maybe a
Just (F -> Maybe F) -> F -> Maybe F
forall a b. (a -> b) -> a -> b
$ E -> E -> F
fCompOp E
e1 E
e2 
        Maybe (E -> E -> F)
_ -> Maybe F
forall a. Maybe a
Nothing
    (Maybe E
_, Maybe E
_) ->
      case (Expression -> [(String, ([String], String))] -> Maybe F
termToF Expression
op1 [(String, ([String], String))]
functionsWithInputsAndOutputs, Expression -> [(String, ([String], String))] -> Maybe F
termToF Expression
op2 [(String, ([String], String))]
functionsWithInputsAndOutputs) of
        (Just F
f1, Just F
f2) ->
          case String
operator of
            String
"and" -> F -> Maybe F
forall a. a -> Maybe a
Just (F -> Maybe F) -> F -> Maybe F
forall a b. (a -> b) -> a -> b
$ Conn -> F -> F -> F
FConn Conn
And F
f1 F
f2
            String
"or"  -> F -> Maybe F
forall a. a -> Maybe a
Just (F -> Maybe F) -> F -> Maybe F
forall a b. (a -> b) -> a -> b
$ Conn -> F -> F -> F
FConn Conn
Or F
f1 F
f2
            String
"=>"  -> F -> Maybe F
forall a. a -> Maybe a
Just (F -> Maybe F) -> F -> Maybe F
forall a b. (a -> b) -> a -> b
$ Conn -> F -> F -> F
FConn Conn
Impl F
f1 F
f2
            String
"="   -> F -> Maybe F
forall a. a -> Maybe a
Just (F -> Maybe F) -> F -> Maybe F
forall a b. (a -> b) -> a -> b
$ Conn -> F -> F -> F
FConn Conn
And (Conn -> F -> F -> F
FConn Conn
Impl F
f1 F
f2) (Conn -> F -> F -> F
FConn Conn
Impl F
f2 F
f1)
            String
n
              | String
"bool_eq" String -> String -> Bool
forall a. Eq a => [a] -> [a] -> Bool
`isPrefixOf` String
n ->  F -> Maybe F
forall a. a -> Maybe a
Just (F -> Maybe F) -> F -> Maybe F
forall a b. (a -> b) -> a -> b
$ Conn -> F -> F -> F
FConn Conn
And (Conn -> F -> F -> F
FConn Conn
Impl F
f1 F
f2) (Conn -> F -> F -> F
FConn Conn
Impl F
f2 F
f1)
              | String
"bool_neq" String -> String -> Bool
forall a. Eq a => [a] -> [a] -> Bool
`isPrefixOf` String
n ->  F -> Maybe F
forall a. a -> Maybe a
Just (F -> Maybe F) -> F -> Maybe F
forall a b. (a -> b) -> a -> b
$ F -> F
FNot (F -> F) -> F -> F
forall a b. (a -> b) -> a -> b
$ Conn -> F -> F -> F
FConn Conn
And (Conn -> F -> F -> F
FConn Conn
Impl F
f1 F
f2) (Conn -> F -> F -> F
FConn Conn
Impl F
f2 F
f1)
              | String
"user_eq" String -> String -> Bool
forall a. Eq a => [a] -> [a] -> Bool
`isPrefixOf` String
n ->  F -> Maybe F
forall a. a -> Maybe a
Just (F -> Maybe F) -> F -> Maybe F
forall a b. (a -> b) -> a -> b
$ Conn -> F -> F -> F
FConn Conn
And (Conn -> F -> F -> F
FConn Conn
Impl F
f1 F
f2) (Conn -> F -> F -> F
FConn Conn
Impl F
f2 F
f1)
            String
_ -> Maybe F
forall a. Maybe a
Nothing
        -- Parse ite where it is used as an expression
        (Maybe F
_, Maybe F
_) ->
          case (Expression
op1, Expression -> [(String, ([String], String))] -> Maybe E
termToE Expression
op2 [(String, ([String], String))]
functionsWithInputsAndOutputs) of
            (LD.Application (LD.Variable String
"ite") [Expression
cond, Expression
thenTerm, Expression
elseTerm], Just E
e2) ->
              case String -> Maybe (E -> E -> F)
parseFCompOp String
operator of
                Just E -> E -> F
fCompOp -> Expression
-> Expression
-> Expression
-> [(String, ([String], String))]
-> Maybe (E -> F)
-> Maybe F
parseIte Expression
cond Expression
thenTerm Expression
elseTerm [(String, ([String], String))]
functionsWithInputsAndOutputs ((E -> F) -> Maybe (E -> F)
forall a. a -> Maybe a
Just (\E
e -> E -> E -> F
fCompOp E
e E
e2))
                Maybe (E -> E -> F)
Nothing -> Maybe F
forall a. Maybe a
Nothing
            (Expression
_, Maybe E
_) ->
              case (Expression -> [(String, ([String], String))] -> Maybe E
termToE Expression
op1 [(String, ([String], String))]
functionsWithInputsAndOutputs, Expression
op2) of
                (Just E
e1, LD.Application (LD.Variable String
"ite") [Expression
cond, Expression
thenTerm, Expression
elseTerm]) ->
                  case String -> Maybe (E -> E -> F)
parseFCompOp String
operator of
                    Just E -> E -> F
fCompOp -> Expression
-> Expression
-> Expression
-> [(String, ([String], String))]
-> Maybe (E -> F)
-> Maybe F
parseIte Expression
cond Expression
thenTerm Expression
elseTerm [(String, ([String], String))]
functionsWithInputsAndOutputs ((E -> F) -> Maybe (E -> F)
forall a. a -> Maybe a
Just (\E
e -> E -> E -> F
fCompOp E
e1 E
e))
                    Maybe (E -> E -> F)
Nothing -> Maybe F
forall a. Maybe a
Nothing
                (Maybe E
_, Expression
_) -> Maybe F
forall a. Maybe a
Nothing

termToF (LD.Application (LD.Variable String
"ite") [Expression
cond, Expression
thenTerm, Expression
elseTerm]) [(String, ([String], String))]
functionsWithInputsAndOutputs = -- if-then-else operator with F types
  Expression
-> Expression
-> Expression
-> [(String, ([String], String))]
-> Maybe (E -> F)
-> Maybe F
parseIte Expression
cond Expression
thenTerm Expression
elseTerm [(String, ([String], String))]
functionsWithInputsAndOutputs Maybe (E -> F)
forall a. Maybe a
Nothing
termToF (LD.Variable String
"true") [(String, ([String], String))]
functionsWithInputsAndOutputs  = F -> Maybe F
forall a. a -> Maybe a
Just F
FTrue
termToF (LD.Variable String
"false") [(String, ([String], String))]
functionsWithInputsAndOutputs = F -> Maybe F
forall a. a -> Maybe a
Just F
FFalse
termToF Expression
_ [(String, ([String], String))]
_ = Maybe F
forall a. Maybe a
Nothing

termToE :: LD.Expression -> [(String, ([String], String))] -> Maybe E
-- Parse 4 * atan(1) as Pi (used by our dReal SMT translator)
termToE :: Expression -> [(String, ([String], String))] -> Maybe E
termToE (LD.Application (LD.Variable String
"*") [LD.Number Rational
4, LD.Application (LD.Variable String
"atan") [LD.Number Rational
1]]) [(String, ([String], String))]
functionsWithInputsAndOutputs = E -> Maybe E
forall a. a -> Maybe a
Just (E -> Maybe E) -> E -> Maybe E
forall a b. (a -> b) -> a -> b
$ E
Pi
-- Symbols/Literals
termToE (LD.Variable String
"true")  [(String, ([String], String))]
functionsWithInputsAndOutputs = Maybe E
forall a. Maybe a
Nothing -- These should be parsed to F
termToE (LD.Variable String
"false") [(String, ([String], String))]
functionsWithInputsAndOutputs = Maybe E
forall a. Maybe a
Nothing -- These should be parsed to F
termToE (LD.Variable String
var) [(String, ([String], String))]
functionsWithInputsAndOutputs = E -> Maybe E
forall a. a -> Maybe a
Just (E -> Maybe E) -> E -> Maybe E
forall a b. (a -> b) -> a -> b
$ String -> E
Var String
var
termToE (LD.Number   Rational
num) [(String, ([String], String))]
functionsWithInputsAndOutputs    = E -> Maybe E
forall a. a -> Maybe a
Just (E -> Maybe E) -> E -> Maybe E
forall a b. (a -> b) -> a -> b
$ Rational -> E
Lit Rational
num
-- one param PropaFP translator functions
-- RoundToInt
termToE (LD.Application (LD.Variable String
"to_int_rne") [Expression
p]) [(String, ([String], String))]
functionsWithInputsAndOutputs = RoundingMode -> E -> E
RoundToInteger RoundingMode
RNE (E -> E) -> Maybe E -> Maybe E
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Expression -> [(String, ([String], String))] -> Maybe E
termToE Expression
p [(String, ([String], String))]
functionsWithInputsAndOutputs
termToE (LD.Application (LD.Variable String
"to_int_rtp") [Expression
p]) [(String, ([String], String))]
functionsWithInputsAndOutputs = RoundingMode -> E -> E
RoundToInteger RoundingMode
RTP (E -> E) -> Maybe E -> Maybe E
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Expression -> [(String, ([String], String))] -> Maybe E
termToE Expression
p [(String, ([String], String))]
functionsWithInputsAndOutputs
termToE (LD.Application (LD.Variable String
"to_int_rtn") [Expression
p]) [(String, ([String], String))]
functionsWithInputsAndOutputs = RoundingMode -> E -> E
RoundToInteger RoundingMode
RTN (E -> E) -> Maybe E -> Maybe E
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Expression -> [(String, ([String], String))] -> Maybe E
termToE Expression
p [(String, ([String], String))]
functionsWithInputsAndOutputs
termToE (LD.Application (LD.Variable String
"to_int_rtz") [Expression
p]) [(String, ([String], String))]
functionsWithInputsAndOutputs = RoundingMode -> E -> E
RoundToInteger RoundingMode
RTZ (E -> E) -> Maybe E -> Maybe E
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Expression -> [(String, ([String], String))] -> Maybe E
termToE Expression
p [(String, ([String], String))]
functionsWithInputsAndOutputs
termToE (LD.Application (LD.Variable String
"to_int_rna") [Expression
p]) [(String, ([String], String))]
functionsWithInputsAndOutputs = RoundingMode -> E -> E
RoundToInteger RoundingMode
RNA (E -> E) -> Maybe E -> Maybe E
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Expression -> [(String, ([String], String))] -> Maybe E
termToE Expression
p [(String, ([String], String))]
functionsWithInputsAndOutputs
-- Float32
termToE (LD.Application (LD.Variable String
"float32_rne") [Expression
p]) [(String, ([String], String))]
functionsWithInputsAndOutputs = RoundingMode -> E -> E
Float32 RoundingMode
RNE (E -> E) -> Maybe E -> Maybe E
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Expression -> [(String, ([String], String))] -> Maybe E
termToE Expression
p [(String, ([String], String))]
functionsWithInputsAndOutputs
termToE (LD.Application (LD.Variable String
"float32_rtp") [Expression
p]) [(String, ([String], String))]
functionsWithInputsAndOutputs = RoundingMode -> E -> E
Float32 RoundingMode
RTP (E -> E) -> Maybe E -> Maybe E
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Expression -> [(String, ([String], String))] -> Maybe E
termToE Expression
p [(String, ([String], String))]
functionsWithInputsAndOutputs
termToE (LD.Application (LD.Variable String
"float32_rtn") [Expression
p]) [(String, ([String], String))]
functionsWithInputsAndOutputs = RoundingMode -> E -> E
Float32 RoundingMode
RTN (E -> E) -> Maybe E -> Maybe E
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Expression -> [(String, ([String], String))] -> Maybe E
termToE Expression
p [(String, ([String], String))]
functionsWithInputsAndOutputs
termToE (LD.Application (LD.Variable String
"float32_rtz") [Expression
p]) [(String, ([String], String))]
functionsWithInputsAndOutputs = RoundingMode -> E -> E
Float32 RoundingMode
RTZ (E -> E) -> Maybe E -> Maybe E
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Expression -> [(String, ([String], String))] -> Maybe E
termToE Expression
p [(String, ([String], String))]
functionsWithInputsAndOutputs
termToE (LD.Application (LD.Variable String
"float32_rna") [Expression
p]) [(String, ([String], String))]
functionsWithInputsAndOutputs = RoundingMode -> E -> E
Float32 RoundingMode
RNA (E -> E) -> Maybe E -> Maybe E
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Expression -> [(String, ([String], String))] -> Maybe E
termToE Expression
p [(String, ([String], String))]
functionsWithInputsAndOutputs
-- Float64
termToE (LD.Application (LD.Variable String
"float64_rne") [Expression
p]) [(String, ([String], String))]
functionsWithInputsAndOutputs = RoundingMode -> E -> E
Float64 RoundingMode
RNE (E -> E) -> Maybe E -> Maybe E
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Expression -> [(String, ([String], String))] -> Maybe E
termToE Expression
p [(String, ([String], String))]
functionsWithInputsAndOutputs
termToE (LD.Application (LD.Variable String
"float64_rtp") [Expression
p]) [(String, ([String], String))]
functionsWithInputsAndOutputs = RoundingMode -> E -> E
Float64 RoundingMode
RTP (E -> E) -> Maybe E -> Maybe E
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Expression -> [(String, ([String], String))] -> Maybe E
termToE Expression
p [(String, ([String], String))]
functionsWithInputsAndOutputs
termToE (LD.Application (LD.Variable String
"float64_rtn") [Expression
p]) [(String, ([String], String))]
functionsWithInputsAndOutputs = RoundingMode -> E -> E
Float64 RoundingMode
RTN (E -> E) -> Maybe E -> Maybe E
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Expression -> [(String, ([String], String))] -> Maybe E
termToE Expression
p [(String, ([String], String))]
functionsWithInputsAndOutputs
termToE (LD.Application (LD.Variable String
"float64_rtz") [Expression
p]) [(String, ([String], String))]
functionsWithInputsAndOutputs = RoundingMode -> E -> E
Float64 RoundingMode
RTZ (E -> E) -> Maybe E -> Maybe E
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Expression -> [(String, ([String], String))] -> Maybe E
termToE Expression
p [(String, ([String], String))]
functionsWithInputsAndOutputs
termToE (LD.Application (LD.Variable String
"float64_rna") [Expression
p]) [(String, ([String], String))]
functionsWithInputsAndOutputs = RoundingMode -> E -> E
Float64 RoundingMode
RNA (E -> E) -> Maybe E -> Maybe E
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Expression -> [(String, ([String], String))] -> Maybe E
termToE Expression
p [(String, ([String], String))]
functionsWithInputsAndOutputs
-- one param functions
termToE (LD.Application (LD.Variable String
operator) [Expression
op]) [(String, ([String], String))]
functionsWithInputsAndOutputs =
  case Expression -> [(String, ([String], String))] -> Maybe E
termToE Expression
op [(String, ([String], String))]
functionsWithInputsAndOutputs of
    Maybe E
Nothing -> Maybe E
forall a. Maybe a
Nothing
    Just E
e -> case String
operator of
      String
n
        | (String
n String -> String -> Bool
forall source source1 target.
(RegexMaker Regex CompOption ExecOption source,
 RegexContext Regex source1 target) =>
source1 -> source -> target
=~ String
"^real_pi$|^real_pi[0-9]+$" :: Bool) -> E -> Maybe E
forall a. a -> Maybe a
Just E
Pi
        | (String
n String -> String -> Bool
forall source source1 target.
(RegexMaker Regex CompOption ExecOption source,
 RegexContext Regex source1 target) =>
source1 -> source -> target
=~ String
"^abs$|^abs[0-9]+$" :: Bool)   -> E -> Maybe E
forall a. a -> Maybe a
Just (E -> Maybe E) -> E -> Maybe E
forall a b. (a -> b) -> a -> b
$ UnOp -> E -> E
EUnOp UnOp
Abs E
e
        | (String
n String -> String -> Bool
forall source source1 target.
(RegexMaker Regex CompOption ExecOption source,
 RegexContext Regex source1 target) =>
source1 -> source -> target
=~ String
"^sin$|^sin[0-9]+$|^real_sin$|^real_sin[0-9]+$" :: Bool)   -> E -> Maybe E
forall a. a -> Maybe a
Just (E -> Maybe E) -> E -> Maybe E
forall a b. (a -> b) -> a -> b
$ UnOp -> E -> E
EUnOp UnOp
Sin E
e
        | (String
n String -> String -> Bool
forall source source1 target.
(RegexMaker Regex CompOption ExecOption source,
 RegexContext Regex source1 target) =>
source1 -> source -> target
=~ String
"^cos$|^cos[0-9]+$|^real_cos$|^real_cos[0-9]+$" :: Bool)   -> E -> Maybe E
forall a. a -> Maybe a
Just (E -> Maybe E) -> E -> Maybe E
forall a b. (a -> b) -> a -> b
$ UnOp -> E -> E
EUnOp UnOp
Cos E
e
        | (String
n String -> String -> Bool
forall source source1 target.
(RegexMaker Regex CompOption ExecOption source,
 RegexContext Regex source1 target) =>
source1 -> source -> target
=~ String
"^sqrt$|^sqrt[0-9]+$|^real_square_root$|^real_square_root[0-9]+$" :: Bool) -> E -> Maybe E
forall a. a -> Maybe a
Just (E -> Maybe E) -> E -> Maybe E
forall a b. (a -> b) -> a -> b
$ UnOp -> E -> E
EUnOp UnOp
Sqrt E
e
        | (String
n String -> String -> Bool
forall source source1 target.
(RegexMaker Regex CompOption ExecOption source,
 RegexContext Regex source1 target) =>
source1 -> source -> target
=~ String
"^fp.to_real$|^fp.to_real[0-9]+$|^to_real$|^to_real[0-9]+$" :: Bool) -> E -> Maybe E
forall a. a -> Maybe a
Just E
e
      String
"-"               -> E -> Maybe E
forall a. a -> Maybe a
Just (E -> Maybe E) -> E -> Maybe E
forall a b. (a -> b) -> a -> b
$ UnOp -> E -> E
EUnOp UnOp
Negate E
e
      -- SPARK Reals functions
      String
"from_int"        -> E -> Maybe E
forall a. a -> Maybe a
Just E
e
      -- Some to_int functions. different suffixes (1, 2, etc.)
      -- e.g. In one file, to_int1 :: Float -> Int
      --                   to_int2 :: Bool  -> Int
      -- Are these suffixes consistent?
      -- Float functions
      String
"fp.abs"          -> E -> Maybe E
forall a. a -> Maybe a
Just (E -> Maybe E) -> E -> Maybe E
forall a b. (a -> b) -> a -> b
$ UnOp -> E -> E
EUnOp UnOp
Abs E
e
      String
"fp.neg"          -> E -> Maybe E
forall a. a -> Maybe a
Just (E -> Maybe E) -> E -> Maybe E
forall a b. (a -> b) -> a -> b
$ UnOp -> E -> E
EUnOp UnOp
Negate E
e
      -- "fp.to_real"      -> Just e
      -- "to_real"         -> Just e
      -- "value"           -> Just e
      -- Undefined functions
      String
"fp.isNormal"     -> Maybe E
forall a. Maybe a
Nothing
      String
"fp.isSubnormal"  -> Maybe E
forall a. Maybe a
Nothing
      String
"fp.isZero"       -> Maybe E
forall a. Maybe a
Nothing
      String
"fp.isNaN"        -> Maybe E
forall a. Maybe a
Nothing
      String
"fp.isPositive"   -> Maybe E
forall a. Maybe a
Nothing
      String
"fp.isNegative"   -> Maybe E
forall a. Maybe a
Nothing
      String
"fp.isIntegral32" -> Maybe E
forall a. Maybe a
Nothing
      String
"fp.isIntegral64" -> Maybe E
forall a. Maybe a
Nothing
      String
_                 -> Maybe E
forall a. Maybe a
Nothing
  where
    deriveTypeForOneArgFunctions :: String -> (E -> E) -> E -> Maybe E
    deriveTypeForOneArgFunctions :: String -> (E -> E) -> E -> Maybe E
deriveTypeForOneArgFunctions String
functionName E -> E
functionAsExpression E
functionArg =
      -- case lookup functionName functionsWithInputsAndOutputs of
        -- Just ([inputType], outputType) ->
      let
        (Maybe [String]
mInputTypes, Maybe String
mOutputType) = Maybe ([String], String) -> (Maybe [String], Maybe String)
forall (f :: * -> *) a b. Functor f => f (a, b) -> (f a, f b)
unzip (Maybe ([String], String) -> (Maybe [String], Maybe String))
-> Maybe ([String], String) -> (Maybe [String], Maybe String)
forall a b. (a -> b) -> a -> b
$ String
-> [(String, ([String], String))] -> Maybe ([String], String)
forall a b. Eq a => a -> [(a, b)] -> Maybe b
lookup String
functionName [(String, ([String], String))]
functionsWithInputsAndOutputs
          -- case lookup functionName functionsWithInputsAndOutputs of
          --   Just (inputTypes, outputType) -> (Just inputTypes, Just outputType)
          --   Nothing -> (Nothing, Nothing)

        newFunctionArg :: E
newFunctionArg = E
functionArg
          -- case mInputTypes of
          --   Just [inputType] ->
          --     case inputType of
          --       -- "Float32" -> Float32 RNE functionArg
          --       -- "Float64" -> Float64 RNE functionArg
          --   _ -> functionArg -- Do not deal with multiple param args for one param functions. TODO: Check if these can occur, i.e. something like RoundingMode Float32

        mNewFunctionAsExpression :: Maybe (E -> E)
mNewFunctionAsExpression =
          case Maybe String
mOutputType of
            Just String
outputType ->
              case String
outputType of
                -- "Float32" -> Float32 RNE . functionAsExpression -- TODO: Make these Nothing if we can't deal with them
                -- "Float64" -> Float64 RNE . functionAsExpression -- TODO: Make these Nothing if we can't deal with them
                String
"Real" -> (E -> E) -> Maybe (E -> E)
forall a. a -> Maybe a
Just E -> E
functionAsExpression --FIXME: Should match on other possible names. Real/real Int/int/integer, etc. I've only seen these alt names in function definitions/axioms, not assertions, but would still be more safe.
                String
"Int" -> (E -> E) -> Maybe (E -> E)
forall a. a -> Maybe a
Just E -> E
functionAsExpression -- FIXME: Round here?
                String
_ -> Maybe (E -> E)
forall a. Maybe a
Nothing -- These should be floats, which we cannot deal with for now
            Maybe String
Nothing -> (E -> E) -> Maybe (E -> E)
forall a. a -> Maybe a
Just E -> E
functionAsExpression -- No type given, assume real
      in
        case Maybe (E -> E)
mNewFunctionAsExpression of
          Just E -> E
newFunctionAsExpression -> E -> Maybe E
forall a. a -> Maybe a
Just (E -> Maybe E) -> E -> Maybe E
forall a b. (a -> b) -> a -> b
$ E -> E
newFunctionAsExpression E
newFunctionArg
          Maybe (E -> E)
Nothing -> Maybe E
forall a. Maybe a
Nothing
        -- Nothing -> functionAsExpression functionArg
-- two param PropaFP translator functions
termToE (LD.Application (LD.Variable String
"min") [Expression
p1, Expression
p2]) [(String, ([String], String))]
functionsWithInputsAndOutputs = BinOp -> E -> E -> E
EBinOp BinOp
Min (E -> E -> E) -> Maybe E -> Maybe (E -> E)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Expression -> [(String, ([String], String))] -> Maybe E
termToE Expression
p1 [(String, ([String], String))]
functionsWithInputsAndOutputs Maybe (E -> E) -> Maybe E -> Maybe E
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> Expression -> [(String, ([String], String))] -> Maybe E
termToE Expression
p2 [(String, ([String], String))]
functionsWithInputsAndOutputs
termToE (LD.Application (LD.Variable String
"max") [Expression
p1, Expression
p2]) [(String, ([String], String))]
functionsWithInputsAndOutputs = BinOp -> E -> E -> E
EBinOp BinOp
Max (E -> E -> E) -> Maybe E -> Maybe (E -> E)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Expression -> [(String, ([String], String))] -> Maybe E
termToE Expression
p1 [(String, ([String], String))]
functionsWithInputsAndOutputs Maybe (E -> E) -> Maybe E -> Maybe E
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> Expression -> [(String, ([String], String))] -> Maybe E
termToE Expression
p2 [(String, ([String], String))]
functionsWithInputsAndOutputs
-- two param functions 
-- params are either two different E types, or one param is a rounding mode and another is the arg
termToE (LD.Application (LD.Variable String
operator) [Expression
op1, Expression
op2]) [(String, ([String], String))]
functionsWithInputsAndOutputs =
  case (Expression -> Maybe RoundingMode
parseRoundingMode Expression
op1, Expression -> [(String, ([String], String))] -> Maybe E
termToE Expression
op2 [(String, ([String], String))]
functionsWithInputsAndOutputs) of
    (Just RoundingMode
roundingMode, Just E
e) ->
      case String
operator of
        String
n
          | (String
n String -> String -> Bool
forall source source1 target.
(RegexMaker Regex CompOption ExecOption source,
 RegexContext Regex source1 target) =>
source1 -> source -> target
=~ String
"^round$|^round[0-9]+$" :: Bool)   -> E -> Maybe E
forall a. a -> Maybe a
Just (E -> Maybe E) -> E -> Maybe E
forall a b. (a -> b) -> a -> b
$ RoundingMode -> E -> E
Float RoundingMode
roundingMode E
e --FIXME: remove this? not used with cvc4 driver?
          | (String
n String -> String -> Bool
forall source source1 target.
(RegexMaker Regex CompOption ExecOption source,
 RegexContext Regex source1 target) =>
source1 -> source -> target
=~ String
"^to_int$|^to_int[0-9]+$" :: Bool) -> E -> Maybe E
forall a. a -> Maybe a
Just (E -> Maybe E) -> E -> Maybe E
forall a b. (a -> b) -> a -> b
$ RoundingMode -> E -> E
RoundToInteger RoundingMode
roundingMode E
e
          | (String
n String -> String -> Bool
forall source source1 target.
(RegexMaker Regex CompOption ExecOption source,
 RegexContext Regex source1 target) =>
source1 -> source -> target
=~ String
"^of_int$|^of_int[0-9]+$" :: Bool) ->
            case String
-> [(String, ([String], String))] -> Maybe ([String], String)
forall a b. Eq a => a -> [(a, b)] -> Maybe b
lookup String
n [(String, ([String], String))]
functionsWithInputsAndOutputs of
              Just ([String]
_, String
outputType) ->
                case String
outputType of
                  String
o -- Why3 will type check that the input is an integer, making these safe
                    | String
o String -> [String] -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` [String
"Float32", String
"single"] -> E -> Maybe E
forall a. a -> Maybe a
Just (E -> Maybe E) -> E -> Maybe E
forall a b. (a -> b) -> a -> b
$ RoundingMode -> E -> E
Float32 RoundingMode
roundingMode E
e
                    | String
o String -> [String] -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` [String
"Float64", String
"double"] -> E -> Maybe E
forall a. a -> Maybe a
Just (E -> Maybe E) -> E -> Maybe E
forall a b. (a -> b) -> a -> b
$ RoundingMode -> E -> E
Float64 RoundingMode
roundingMode E
e
                    | String
o String -> [String] -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` [String
"Real", String
"real"] -> E -> Maybe E
forall a. a -> Maybe a
Just E
e
                  String
_ -> Maybe E
forall a. Maybe a
Nothing
              Maybe ([String], String)
_ -> Maybe E
forall a. Maybe a
Nothing
        String
"fp.roundToIntegral" -> E -> Maybe E
forall a. a -> Maybe a
Just (E -> Maybe E) -> E -> Maybe E
forall a b. (a -> b) -> a -> b
$ RoundingMode -> E -> E
RoundToInteger RoundingMode
roundingMode E
e
        String
_ -> Maybe E
forall a. Maybe a
Nothing
    (Maybe RoundingMode, Maybe E)
_ ->
      case (Expression -> [(String, ([String], String))] -> Maybe E
termToE Expression
op1 [(String, ([String], String))]
functionsWithInputsAndOutputs, Expression -> [(String, ([String], String))] -> Maybe E
termToE Expression
op2 [(String, ([String], String))]
functionsWithInputsAndOutputs) of
        (Just E
e1, Just E
e2) ->
          case String
operator of
            String
n
              -- "o..." functions are from SPARK Reals
              | String
n String -> [String] -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` [String
"+", String
"oadd", String
"oadd__logic"]                    -> E -> Maybe E
forall a. a -> Maybe a
Just (E -> Maybe E) -> E -> Maybe E
forall a b. (a -> b) -> a -> b
$ BinOp -> E -> E -> E
EBinOp BinOp
Add E
e1 E
e2
              | String
n String -> [String] -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` [String
"-", String
"osubtract", String
"osubtract__logic"]          -> E -> Maybe E
forall a. a -> Maybe a
Just (E -> Maybe E) -> E -> Maybe E
forall a b. (a -> b) -> a -> b
$ BinOp -> E -> E -> E
EBinOp BinOp
Sub E
e1 E
e2
              | String
n String -> [String] -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` [String
"*", String
"omultiply", String
"omultiply__logic"]          -> E -> Maybe E
forall a. a -> Maybe a
Just (E -> Maybe E) -> E -> Maybe E
forall a b. (a -> b) -> a -> b
$ BinOp -> E -> E -> E
EBinOp BinOp
Mul E
e1 E
e2
              | String
n String -> [String] -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` [String
"/", String
"odivide", String
"odivide__logic"]              -> E -> Maybe E
forall a. a -> Maybe a
Just (E -> Maybe E) -> E -> Maybe E
forall a b. (a -> b) -> a -> b
$ BinOp -> E -> E -> E
EBinOp BinOp
Div E
e1 E
e2
              | (String
n String -> String -> Bool
forall source source1 target.
(RegexMaker Regex CompOption ExecOption source,
 RegexContext Regex source1 target) =>
source1 -> source -> target
=~ String
"^pow$|^pow[0-9]+$|^power$|^power[0-9]+$" :: Bool) -> E -> Maybe E
forall a. a -> Maybe a
Just (E -> Maybe E) -> E -> Maybe E
forall a b. (a -> b) -> a -> b
$ BinOp -> E -> E -> E
EBinOp BinOp
Pow E
e1 E
e2 --FIXME: remove int pow? only use int pow if actually specified?
              | String
n String -> String -> EqCompareType String String
forall a b. HasEqAsymmetric a b => a -> b -> EqCompareType a b
== String
"^" -> E -> Maybe E
forall a. a -> Maybe a
Just (E -> Maybe E) -> E -> Maybe E
forall a b. (a -> b) -> a -> b
$ BinOp -> E -> E -> E
EBinOp BinOp
Pow E
e1 E
e2
                -- case lookup n functionsWithInputsAndOutputs of
                --   Just (["Real", "Real"], "Real") -> Just $ EBinOp Pow e1 e2
                --   Just ([input1, "Int"], output) ->
                --     let
                --       mExactPowExpression =
                --         if input1 == "Int" || input1 == "Real"
                --           then case e2 of
                --             Lit l2 -> if denominator l2 == 1.0 then Just $ PowI e1 (numerator l2) else Just $ EBinOp Pow e1 e2
                --             _      -> Just $ EBinOp Pow e1 e2
                --           else Nothing
                --     in case mExactPowExpression of
                --       Just exactPowExpression -> case output of
                --         "Real" -> Just exactPowExpression
                --         "Int"  -> Just $ RoundToInteger RNE exactPowExpression

                --         _      -> Nothing
                --       Nothing -> Nothing
                --   Nothing -> -- No input/output, treat as real pow
                --     case e2 of
                --       Lit l2 -> if denominator l2 == 1.0 then Just $ PowI e1 (numerator l2) else Just $ EBinOp Pow e1 e2
                --       _      -> Just $ EBinOp Pow e1 e2
                --   _ -> Nothing
              | (String
n String -> String -> Bool
forall source source1 target.
(RegexMaker Regex CompOption ExecOption source,
 RegexContext Regex source1 target) =>
source1 -> source -> target
=~ String
"^mod$|^mod[0-9]+$" :: Bool)                       -> E -> Maybe E
forall a. a -> Maybe a
Just (E -> Maybe E) -> E -> Maybe E
forall a b. (a -> b) -> a -> b
$ BinOp -> E -> E -> E
EBinOp BinOp
Mod E
e1 E
e2
                -- case lookup n functionsWithInputsAndOutputs of
                --   Just (["Real", "Real"], "Real") -> Just $ EBinOp Mod e1 e2
                --   Just (["Int", "Int"], "Int") -> Just $ RoundToInteger RNE $ EBinOp Mod e1 e2 --TODO: might be worth implementing Int Mod
                --   -- No input/output, treat as real mod
                --   Nothing -> Just $ EBinOp Mod e1 e2
                --   _ -> Nothing
            String
_                                                            -> Maybe E
forall a. Maybe a
Nothing
        (Maybe E
_, Maybe E
_) -> Maybe E
forall a. Maybe a
Nothing

-- Float bits to Rational
termToE (LD.Application (LD.Variable String
"fp") [LD.Variable String
sSign, LD.Variable String
sExponent, LD.Variable String
sMantissa]) [(String, ([String], String))]
functionsWithInputsAndOutputs =
  let
    bSign :: String
bSign     = Integer -> String -> String
forall n a. CanBeInteger n => n -> [a] -> [a]
drop Integer
2 String
sSign
    bExponent :: String
bExponent = Integer -> String -> String
forall n a. CanBeInteger n => n -> [a] -> [a]
drop Integer
2 String
sExponent
    bMantissa :: String
bMantissa = Integer -> String -> String
forall n a. CanBeInteger n => n -> [a] -> [a]
drop Integer
2 String
sMantissa

    bFull :: String
bFull = String
bSign String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
bExponent String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
bMantissa

    -- Read a string of Bits ('1' or '0') where the first digit is the most significant
    -- The digit parameter denotes the current digit, should be equal to length of the first param at all times
    readBits :: String -> Integer -> Integer
    readBits :: String -> Integer -> Integer
readBits [] Integer
_ = Integer
0
    readBits (Char
bit : String
bits) Integer
digit = Char -> Int
digitToInt Char
bit Int -> Integer -> MulType Int Integer
forall t1 t2. CanMulAsymmetric t1 t2 => t1 -> t2 -> MulType t1 t2
* (Integer
2 Integer -> Integer -> PowType Integer Integer
forall t1 t2. CanPow t1 t2 => t1 -> t2 -> PowType t1 t2
^ (Integer
digit Integer -> Integer -> SubType Integer Integer
forall t1 t2. CanSub t1 t2 => t1 -> t2 -> SubType t1 t2
- Integer
1)) Integer -> Integer -> AddType Integer Integer
forall t1 t2. CanAddAsymmetric t1 t2 => t1 -> t2 -> AddType t1 t2
+ String -> Integer -> Integer
readBits String
bits (Integer
digit Integer -> Integer -> SubType Integer Integer
forall t1 t2. CanSub t1 t2 => t1 -> t2 -> SubType t1 t2
- Integer
1)

    bitsToWord8 :: String -> [Word8]
    bitsToWord8 :: String -> [Word8]
bitsToWord8 String
bits =
      let wordS :: String
wordS = Integer -> String -> String
forall n a. CanBeInteger n => n -> [a] -> [a]
take Integer
8 String
bits
          rem :: String
rem   = Integer -> String -> String
forall n a. CanBeInteger n => n -> [a] -> [a]
drop Integer
8 String
bits
          wordV :: Integer
wordV = String -> Integer -> Integer
readBits String
wordS Integer
8
      in
        Integer -> Word8
forall a. Num a => Integer -> a
P.fromInteger Integer
wordV Word8 -> [Word8] -> [Word8]
forall a. a -> [a] -> [a]
: String -> [Word8]
bitsToWord8 String
rem

    bsFloat :: ByteString
bsFloat    = [Word8] -> ByteString
B.pack ([Word8] -> ByteString) -> [Word8] -> ByteString
forall a b. (a -> b) -> a -> b
$ String -> [Word8]
bitsToWord8 String
bFull
  in
    if (Char -> Bool) -> String -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
all (Char -> String -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` String
"01") String
bFull
      then
        case String -> Integer
forall (t :: * -> *) a. Foldable t => t a -> Integer
length String
bFull of
          Integer
32 -> E -> Maybe E
forall a. a -> Maybe a
Just (E -> Maybe E) -> E -> Maybe E
forall a b. (a -> b) -> a -> b
$ Rational -> E
Lit (Rational -> E) -> Rational -> E
forall a b. (a -> b) -> a -> b
$ Float -> Rational
forall a. Real a => a -> Rational
toRational (Float -> Rational) -> Float -> Rational
forall a b. (a -> b) -> a -> b
$ Get Float -> ByteString -> Float
forall a. Get a -> ByteString -> a
runGet Get Float
getFloatbe ByteString
bsFloat
          Integer
64 -> E -> Maybe E
forall a. a -> Maybe a
Just (E -> Maybe E) -> E -> Maybe E
forall a b. (a -> b) -> a -> b
$ Rational -> E
Lit (Rational -> E) -> Rational -> E
forall a b. (a -> b) -> a -> b
$ Double -> Rational
forall a. Real a => a -> Rational
toRational (Double -> Rational) -> Double -> Rational
forall a b. (a -> b) -> a -> b
$ Get Double -> ByteString -> Double
forall a. Get a -> ByteString -> a
runGet Get Double
getDoublebe ByteString
bsFloat
          -- 32 -> Just $ Float32 RNE $ Lit $ toRational $ runGet getFloatbe bsFloat 
          -- 64 -> Just $ Float64 RNE $ Lit $ toRational $ runGet getDoublebe bsFloat
          Integer
_  -> Maybe E
forall a. Maybe a
Nothing
      else Maybe E
forall a. Maybe a
Nothing

-- Float functions, three params. Other three param functions should be placed before here
termToE (LD.Application (LD.Variable String
operator) [Expression
roundingMode, Expression
op1, Expression
op2]) [(String, ([String], String))]
functionsWithInputsAndOutputs =
  -- case operator of
  --   -- SPARK Reals
  --   "fp.to_real" -> Nothing 
  --   _ -> -- Known ops
  case (Expression -> [(String, ([String], String))] -> Maybe E
termToE Expression
op1 [(String, ([String], String))]
functionsWithInputsAndOutputs, Expression -> [(String, ([String], String))] -> Maybe E
termToE Expression
op2 [(String, ([String], String))]
functionsWithInputsAndOutputs) of
    (Just E
e1, Just E
e2) ->
      case Expression -> Maybe RoundingMode
parseRoundingMode Expression
roundingMode of -- Floating-point ops
        Just RoundingMode
mode ->
          case String
operator of
            String
"fp.add" -> E -> Maybe E
forall a. a -> Maybe a
Just (E -> Maybe E) -> E -> Maybe E
forall a b. (a -> b) -> a -> b
$ RoundingMode -> E -> E
Float RoundingMode
mode (E -> E) -> E -> E
forall a b. (a -> b) -> a -> b
$ BinOp -> E -> E -> E
EBinOp BinOp
Add E
e1 E
e2
            String
"fp.sub" -> E -> Maybe E
forall a. a -> Maybe a
Just (E -> Maybe E) -> E -> Maybe E
forall a b. (a -> b) -> a -> b
$ RoundingMode -> E -> E
Float RoundingMode
mode (E -> E) -> E -> E
forall a b. (a -> b) -> a -> b
$ BinOp -> E -> E -> E
EBinOp BinOp
Sub E
e1 E
e2
            String
"fp.mul" -> E -> Maybe E
forall a. a -> Maybe a
Just (E -> Maybe E) -> E -> Maybe E
forall a b. (a -> b) -> a -> b
$ RoundingMode -> E -> E
Float RoundingMode
mode (E -> E) -> E -> E
forall a b. (a -> b) -> a -> b
$ BinOp -> E -> E -> E
EBinOp BinOp
Mul E
e1 E
e2
            String
"fp.div" -> E -> Maybe E
forall a. a -> Maybe a
Just (E -> Maybe E) -> E -> Maybe E
forall a b. (a -> b) -> a -> b
$ RoundingMode -> E -> E
Float RoundingMode
mode (E -> E) -> E -> E
forall a b. (a -> b) -> a -> b
$ BinOp -> E -> E -> E
EBinOp BinOp
Div E
e1 E
e2
            String
_        -> Maybe E
forall a. Maybe a
Nothing
        Maybe RoundingMode
Nothing -> Maybe E
forall a. Maybe a
Nothing
    (Maybe E
_, Maybe E
_) -> Maybe E
forall a. Maybe a
Nothing
termToE Expression
_ [(String, ([String], String))]
_ = Maybe E
forall a. Maybe a
Nothing

collapseOrs :: [LD.Expression] -> [LD.Expression]
collapseOrs :: [Expression] -> [Expression]
collapseOrs = (Expression -> Expression) -> [Expression] -> [Expression]
forall a b. (a -> b) -> [a] -> [b]
map Expression -> Expression
collapseOr

collapseOr :: LD.Expression -> LD.Expression
collapseOr :: Expression -> Expression
collapseOr orig :: Expression
orig@(LD.Application (LD.Variable String
"or") [LD.Application (LD.Variable String
"<") [Expression]
args1, LD.Application (LD.Variable String
"=") [Expression]
args2]) =
  if [Expression]
args1 [Expression] -> [Expression] -> Bool
forall a. Eq a => a -> a -> Bool
P.== [Expression]
args2
    then Expression -> [Expression] -> Expression
LD.Application (String -> Expression
LD.Variable String
"<=") [Expression]
args1
    else Expression
orig
collapseOr orig :: Expression
orig@(LD.Application (LD.Variable String
"or") [LD.Application (LD.Variable String
"=") [Expression]
args1, LD.Application (LD.Variable String
"<") [Expression]
args2]) =
  if [Expression]
args1 [Expression] -> [Expression] -> Bool
forall a. Eq a => a -> a -> Bool
P.== [Expression]
args2
    then Expression -> [Expression] -> Expression
LD.Application (String -> Expression
LD.Variable String
"<=") [Expression]
args1
    else Expression
orig
collapseOr orig :: Expression
orig@(LD.Application (LD.Variable String
"or") [LD.Application (LD.Variable String
">") [Expression]
args1, LD.Application (LD.Variable String
"=") [Expression]
args2]) =
  if [Expression]
args1 [Expression] -> [Expression] -> Bool
forall a. Eq a => a -> a -> Bool
P.== [Expression]
args2
    then Expression -> [Expression] -> Expression
LD.Application (String -> Expression
LD.Variable String
">=") [Expression]
args1
    else Expression
orig
collapseOr orig :: Expression
orig@(LD.Application (LD.Variable String
"or") [LD.Application (LD.Variable String
"=") [Expression]
args1, LD.Application (LD.Variable String
">") [Expression]
args2]) =
  if [Expression]
args1 [Expression] -> [Expression] -> Bool
forall a. Eq a => a -> a -> Bool
P.== [Expression]
args2
    then Expression -> [Expression] -> Expression
LD.Application (String -> Expression
LD.Variable String
">=") [Expression]
args1
    else Expression
orig
collapseOr (LD.Application Expression
operator [Expression]
args) = Expression -> [Expression] -> Expression
LD.Application Expression
operator ([Expression] -> [Expression]
collapseOrs [Expression]
args)
collapseOr Expression
e = Expression
e

-- |Replace function guards which are known to be always true with true.
eliminateKnownFunctionGuards :: [LD.Expression] -> [LD.Expression]
eliminateKnownFunctionGuards :: [Expression] -> [Expression]
eliminateKnownFunctionGuards = (Expression -> Expression) -> [Expression] -> [Expression]
forall a b. (a -> b) -> [a] -> [b]
map Expression -> Expression
eliminateKnownFunctionGuard

-- |Replace function guard which is known to be always true with true.
eliminateKnownFunctionGuard :: LD.Expression -> LD.Expression
eliminateKnownFunctionGuard :: Expression -> Expression
eliminateKnownFunctionGuard orig :: Expression
orig@(LD.Application operator :: Expression
operator@(LD.Variable String
var) args :: [Expression]
args@(Expression
guardedFunction : [Expression]
_)) =
  let
    knownGuardsRegex :: String
knownGuardsRegex = 
      String
"^real_sin__function_guard$|^real_sin__function_guard[0-9]+$|" String -> String -> String
forall a. [a] -> [a] -> [a]
++
      String
"^real_cos__function_guard$|^real_cos__function_guard[0-9]+$|" String -> String -> String
forall a. [a] -> [a] -> [a]
++
      String
"^real_square_root__function_guard$|^real_square_root__function_guard[0-9]+$|" String -> String -> String
forall a. [a] -> [a] -> [a]
++
      String
"^real_pi__function_guard$|^real_pi__function_guard[0-9]+$"
  in
    if (String
var String -> String -> Bool
forall source source1 target.
(RegexMaker Regex CompOption ExecOption source,
 RegexContext Regex source1 target) =>
source1 -> source -> target
=~ String
knownGuardsRegex :: Bool)
      then String -> Expression
LD.Variable String
"true"
      else Expression -> [Expression] -> Expression
LD.Application Expression
operator ([Expression] -> [Expression]
eliminateKnownFunctionGuards [Expression]
args)
eliminateKnownFunctionGuard (LD.Application Expression
operator [Expression]
args) = Expression -> [Expression] -> Expression
LD.Application Expression
operator ([Expression] -> [Expression]
eliminateKnownFunctionGuards [Expression]
args)
eliminateKnownFunctionGuard Expression
e = Expression
e

termsToF :: [LD.Expression] -> [(String, ([String], String))] -> [F]
termsToF :: [Expression] -> [(String, ([String], String))] -> [F]
termsToF [Expression]
es [(String, ([String], String))]
fs = (Expression -> Maybe F) -> [Expression] -> [F]
forall a b. (a -> Maybe b) -> [a] -> [b]
mapMaybe (Expression -> [(String, ([String], String))] -> Maybe F
`termToF` [(String, ([String], String))]
fs) [Expression]
es

determineFloatTypeE :: E -> [(String, String)] -> Maybe E
determineFloatTypeE :: E -> [(String, String)] -> Maybe E
determineFloatTypeE (EBinOp BinOp
op E
e1 E
e2) [(String, String)]
varTypeMap  = case E -> [(String, String)] -> Maybe E
determineFloatTypeE E
e1 [(String, String)]
varTypeMap of
                                                      Just E
p1 ->
                                                        case E -> [(String, String)] -> Maybe E
determineFloatTypeE E
e2 [(String, String)]
varTypeMap of
                                                          Just E
p2 -> E -> Maybe E
forall a. a -> Maybe a
Just (E -> Maybe E) -> E -> Maybe E
forall a b. (a -> b) -> a -> b
$ BinOp -> E -> E -> E
EBinOp BinOp
op E
p1 E
p2
                                                          Maybe E
Nothing -> Maybe E
forall a. Maybe a
Nothing
                                                      Maybe E
Nothing -> Maybe E
forall a. Maybe a
Nothing
determineFloatTypeE (EUnOp UnOp
op E
e)      [(String, String)]
varTypeMap  = case E -> [(String, String)] -> Maybe E
determineFloatTypeE E
e [(String, String)]
varTypeMap of
                                                      Just E
p -> E -> Maybe E
forall a. a -> Maybe a
Just (E -> Maybe E) -> E -> Maybe E
forall a b. (a -> b) -> a -> b
$ UnOp -> E -> E
EUnOp UnOp
op E
p
                                                      Maybe E
Nothing -> Maybe E
forall a. Maybe a
Nothing
determineFloatTypeE (PowI E
e Integer
i)        [(String, String)]
varTypeMap  = case E -> [(String, String)] -> Maybe E
determineFloatTypeE E
e [(String, String)]
varTypeMap of
                                                      Just E
p -> E -> Maybe E
forall a. a -> Maybe a
Just (E -> Maybe E) -> E -> Maybe E
forall a b. (a -> b) -> a -> b
$ E -> Integer -> E
PowI E
p Integer
i
                                                      Maybe E
Nothing -> Maybe E
forall a. Maybe a
Nothing
determineFloatTypeE (Float RoundingMode
r E
e)       [(String, String)]
varTypeMap  = case Maybe String
mVariableType of
                                                      Just String
variableType ->
                                                        case String
variableType of
                                                          String
t
                                                            | String
t String -> [String] -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` [String
"Float32", String
"single"] ->
                                                                case E -> [(String, String)] -> Maybe E
determineFloatTypeE E
e [(String, String)]
varTypeMap of
                                                                  Just E
p -> E -> Maybe E
forall a. a -> Maybe a
Just (E -> Maybe E) -> E -> Maybe E
forall a b. (a -> b) -> a -> b
$ RoundingMode -> E -> E
Float32 RoundingMode
r E
p
                                                                  Maybe E
Nothing -> Maybe E
forall a. Maybe a
Nothing
                                                            | String
t String -> [String] -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` [String
"Float64", String
"double"] ->
                                                                case E -> [(String, String)] -> Maybe E
determineFloatTypeE E
e [(String, String)]
varTypeMap of
                                                                  Just E
p -> E -> Maybe E
forall a. a -> Maybe a
Just (E -> Maybe E) -> E -> Maybe E
forall a b. (a -> b) -> a -> b
$ RoundingMode -> E -> E
Float64 RoundingMode
r E
p
                                                                  Maybe E
Nothing -> Maybe E
forall a. Maybe a
Nothing
                                                          String
_ -> Maybe E
forall a. Maybe a
Nothing
                                                      Maybe String
Nothing -> Maybe E
forall a. Maybe a
Nothing
                                                    where
                                                      allVars :: [String]
allVars = E -> [String]
findVariablesInExpressions E
e
                                                      knownVarsWithPrecision :: [(String, Integer)]
knownVarsWithPrecision = E -> [(String, Integer)]
knownFloatVars E
e
                                                      knownVars :: [String]
knownVars = ((String, Integer) -> String) -> [(String, Integer)] -> [String]
forall a b. (a -> b) -> [a] -> [b]
map (String, Integer) -> String
forall a b. (a, b) -> a
fst [(String, Integer)]
knownVarsWithPrecision
                                                      unknownVars :: [String]
unknownVars = (String -> Bool) -> [String] -> [String]
forall a. (a -> Bool) -> [a] -> [a]
filter (String -> [String] -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`notElem` [String]
knownVars) [String]
allVars
                                                      mVariableType :: Maybe String
mVariableType = [String]
-> [(String, String)]
-> [(String, Integer)]
-> Maybe String
-> Maybe String
findVariableType [String]
unknownVars [(String, String)]
varTypeMap [(String, Integer)]
knownVarsWithPrecision Maybe String
forall a. Maybe a
Nothing
determineFloatTypeE (Float32 RoundingMode
r E
e)     [(String, String)]
varTypeMap  = case E -> [(String, String)] -> Maybe E
determineFloatTypeE E
e [(String, String)]
varTypeMap of
                                                      Just E
p -> E -> Maybe E
forall a. a -> Maybe a
Just (E -> Maybe E) -> E -> Maybe E
forall a b. (a -> b) -> a -> b
$ RoundingMode -> E -> E
Float32 RoundingMode
r E
p
                                                      Maybe E
Nothing -> Maybe E
forall a. Maybe a
Nothing
determineFloatTypeE (Float64 RoundingMode
r E
e)     [(String, String)]
varTypeMap  = case E -> [(String, String)] -> Maybe E
determineFloatTypeE E
e [(String, String)]
varTypeMap of
                                                      Just E
p -> E -> Maybe E
forall a. a -> Maybe a
Just (E -> Maybe E) -> E -> Maybe E
forall a b. (a -> b) -> a -> b
$ RoundingMode -> E -> E
Float64 RoundingMode
r E
p
                                                      Maybe E
Nothing -> Maybe E
forall a. Maybe a
Nothing
determineFloatTypeE (RoundToInteger RoundingMode
r E
e) [(String, String)]
varTypeMap = case E -> [(String, String)] -> Maybe E
determineFloatTypeE E
e [(String, String)]
varTypeMap of
                                                        Just E
p -> E -> Maybe E
forall a. a -> Maybe a
Just (E -> Maybe E) -> E -> Maybe E
forall a b. (a -> b) -> a -> b
$ RoundingMode -> E -> E
RoundToInteger RoundingMode
r E
p
                                                        Maybe E
Nothing -> Maybe E
forall a. Maybe a
Nothing
determineFloatTypeE E
Pi                [(String, String)]
_           = E -> Maybe E
forall a. a -> Maybe a
Just E
Pi
determineFloatTypeE (Var String
v)           [(String, String)]
varTypeMap  = case String -> [(String, String)] -> Maybe String
forall a b. Eq a => a -> [(a, b)] -> Maybe b
lookup String
v [(String, String)]
varTypeMap of
                                                      Just String
variableType ->
                                                        case String
variableType of
                                                          -- t
                                                          --   | t `elem` ["Float32", "single"] -> Just $ Float32 RNE $ Var v
                                                          --   | t `elem` ["Float64", "double"] -> Just $ Float64 RNE $ Var v
                                                          String
_ -> E -> Maybe E
forall a. a -> Maybe a
Just (E -> Maybe E) -> E -> Maybe E
forall a b. (a -> b) -> a -> b
$ String -> E
Var String
v -- It is safe to treat integers and rationals as reals
                                                      Maybe String
_ -> E -> Maybe E
forall a. a -> Maybe a
Just (E -> Maybe E) -> E -> Maybe E
forall a b. (a -> b) -> a -> b
$ String -> E
Var String
v
determineFloatTypeE (Lit Rational
n)           [(String, String)]
_           = E -> Maybe E
forall a. a -> Maybe a
Just (E -> Maybe E) -> E -> Maybe E
forall a b. (a -> b) -> a -> b
$ Rational -> E
Lit Rational
n

-- |Tries to determine whether a Float operation is single or double precision
-- by searching for the type of all variables appearing in the function. If the
-- types match and are all either Float32/Float64, we can determine the type.
determineFloatTypeF :: F -> [(String, String)] -> Maybe F
determineFloatTypeF :: F -> [(String, String)] -> Maybe F
determineFloatTypeF (FComp Comp
op E
e1 E
e2) [(String, String)]
varTypeMap = case (E -> [(String, String)] -> Maybe E
determineFloatTypeE E
e1 [(String, String)]
varTypeMap, E -> [(String, String)] -> Maybe E
determineFloatTypeE E
e2 [(String, String)]
varTypeMap) of
                                                    (Just E
p1, Just E
p2)  -> F -> Maybe F
forall a. a -> Maybe a
Just (F -> Maybe F) -> F -> Maybe F
forall a b. (a -> b) -> a -> b
$ Comp -> E -> E -> F
FComp Comp
op E
p1 E
p2
                                                    (Maybe E
_, Maybe E
_)              -> Maybe F
forall a. Maybe a
Nothing
determineFloatTypeF (FConn Conn
op F
f1 F
f2) [(String, String)]
varTypeMap = case (F -> [(String, String)] -> Maybe F
determineFloatTypeF F
f1 [(String, String)]
varTypeMap, F -> [(String, String)] -> Maybe F
determineFloatTypeF F
f2 [(String, String)]
varTypeMap) of
                                                    (Just F
p1, Just F
p2)  -> F -> Maybe F
forall a. a -> Maybe a
Just (F -> Maybe F) -> F -> Maybe F
forall a b. (a -> b) -> a -> b
$ Conn -> F -> F -> F
FConn Conn
op F
p1 F
p2
                                                    (Maybe F
_, Maybe F
_)              -> Maybe F
forall a. Maybe a
Nothing
determineFloatTypeF (FNot F
f)         [(String, String)]
varTypeMap = case F -> [(String, String)] -> Maybe F
determineFloatTypeF F
f [(String, String)]
varTypeMap of
                                                    Just F
p  -> F -> Maybe F
forall a. a -> Maybe a
Just (F -> Maybe F) -> F -> Maybe F
forall a b. (a -> b) -> a -> b
$ F -> F
FNot F
p
                                                    Maybe F
Nothing -> Maybe F
forall a. Maybe a
Nothing
determineFloatTypeF F
FTrue  [(String, String)]
_ = F -> Maybe F
forall a. a -> Maybe a
Just F
FTrue
determineFloatTypeF F
FFalse [(String, String)]
_ = F -> Maybe F
forall a. a -> Maybe a
Just F
FFalse

-- |Find the type for the given variables
-- Type is looked for in the supplied map
-- If all found types match, return this type
findVariableType :: [String] -> [(String, String)] -> [(String, Integer)] -> Maybe String -> Maybe String
findVariableType :: [String]
-> [(String, String)]
-> [(String, Integer)]
-> Maybe String
-> Maybe String
findVariableType [] [(String, String)]
_ [] Maybe String
mFoundType  = Maybe String
mFoundType
findVariableType [] [(String, String)]
_ ((String
_, Integer
precision) : [(String, Integer)]
vars) Maybe String
mFoundType =
  case Maybe String
mFoundType of
    Just String
t ->
      if (String
t String -> [String] -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` [String
"Float32", String
"single"] Bool -> Bool -> AndOrType Bool Bool
forall a b. CanAndOrAsymmetric a b => a -> b -> AndOrType a b
&& Integer
precision Integer -> Integer -> EqCompareType Integer Integer
forall a b. HasEqAsymmetric a b => a -> b -> EqCompareType a b
== Integer
32) Bool -> Bool -> AndOrType Bool Bool
forall a b. CanAndOrAsymmetric a b => a -> b -> AndOrType a b
|| ((String
t String -> [String] -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` [String
"Float64", String
"double"]) Bool -> Bool -> AndOrType Bool Bool
forall a b. CanAndOrAsymmetric a b => a -> b -> AndOrType a b
&& (Integer
precision Integer -> Integer -> EqCompareType Integer Integer
forall a b. HasEqAsymmetric a b => a -> b -> EqCompareType a b
== Integer
64))
        then [String]
-> [(String, String)]
-> [(String, Integer)]
-> Maybe String
-> Maybe String
findVariableType [] [] [(String, Integer)]
vars Maybe String
mFoundType
        else Maybe String
forall a. Maybe a
Nothing
    Maybe String
Nothing ->
      case Integer
precision of
        Integer
32 -> [String]
-> [(String, String)]
-> [(String, Integer)]
-> Maybe String
-> Maybe String
findVariableType [] [] [(String, Integer)]
vars (String -> Maybe String
forall a. a -> Maybe a
Just String
"Float32")
        Integer
64 -> [String]
-> [(String, String)]
-> [(String, Integer)]
-> Maybe String
-> Maybe String
findVariableType [] [] [(String, Integer)]
vars (String -> Maybe String
forall a. a -> Maybe a
Just String
"Float64")
        Integer
_ -> Maybe String
forall a. Maybe a
Nothing

findVariableType (String
v: [String]
vs) [(String, String)]
varTypeMap [(String, Integer)]
knownVarsWithPrecision Maybe String
mFoundType =
  case String -> [(String, String)] -> Maybe String
forall a b. Eq a => a -> [(a, b)] -> Maybe b
lookup String
v [(String, String)]
varTypeMap of
    Just String
t  ->
      if String
"Int" String -> String -> Bool
forall a. Eq a => [a] -> [a] -> Bool
`isPrefixOf` String
t then
        [String]
-> [(String, String)]
-> [(String, Integer)]
-> Maybe String
-> Maybe String
findVariableType [String]
vs [(String, String)]
varTypeMap [(String, Integer)]
knownVarsWithPrecision Maybe String
mFoundType
        else
          case Maybe String
mFoundType of
            Just String
f -> if String
f String -> String -> EqCompareType String String
forall a b. HasEqAsymmetric a b => a -> b -> EqCompareType a b
== String
t then [String]
-> [(String, String)]
-> [(String, Integer)]
-> Maybe String
-> Maybe String
findVariableType [String]
vs [(String, String)]
varTypeMap [(String, Integer)]
knownVarsWithPrecision (String -> Maybe String
forall a. a -> Maybe a
Just String
t) else Maybe String
forall a. Maybe a
Nothing
            Maybe String
Nothing -> [String]
-> [(String, String)]
-> [(String, Integer)]
-> Maybe String
-> Maybe String
findVariableType [String]
vs [(String, String)]
varTypeMap [(String, Integer)]
knownVarsWithPrecision (String -> Maybe String
forall a. a -> Maybe a
Just String
t)
    Maybe String
Nothing -> Maybe String
forall a. Maybe a
Nothing

knownFloatVars :: E -> [(String, Integer)]
knownFloatVars :: E -> [(String, Integer)]
knownFloatVars E
e = [(String, Integer)] -> [(String, Integer)]
removeConflictingVars ([(String, Integer)] -> [(String, Integer)])
-> ([(String, Integer)] -> [(String, Integer)])
-> [(String, Integer)]
-> [(String, Integer)]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [(String, Integer)] -> [(String, Integer)]
forall a. Eq a => [a] -> [a]
nub ([(String, Integer)] -> [(String, Integer)])
-> [(String, Integer)] -> [(String, Integer)]
forall a b. (a -> b) -> a -> b
$ E -> [(String, Integer)]
findAllFloatVars E
e
  where
    removeConflictingVars :: [(String, Integer)] -> [(String, Integer)]
    removeConflictingVars :: [(String, Integer)] -> [(String, Integer)]
removeConflictingVars [] = []
    removeConflictingVars ((String
v, Integer
t) : [(String, Integer)]
vs) =
      if String
v String -> [String] -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` ((String, Integer) -> String) -> [(String, Integer)] -> [String]
forall a b. (a -> b) -> [a] -> [b]
map (String, Integer) -> String
forall a b. (a, b) -> a
fst [(String, Integer)]
vs
        then [(String, Integer)] -> [(String, Integer)]
removeConflictingVars ([(String, Integer)] -> [(String, Integer)])
-> [(String, Integer)] -> [(String, Integer)]
forall a b. (a -> b) -> a -> b
$ ((String, Integer) -> Bool)
-> [(String, Integer)] -> [(String, Integer)]
forall a. (a -> Bool) -> [a] -> [a]
filter (\(String
v', Integer
_) -> String
v String -> String -> EqCompareType String String
forall a b. HasEqAsymmetric a b => a -> b -> EqCompareType a b
/= String
v') [(String, Integer)]
vs
        else (String
v, Integer
t) (String, Integer) -> [(String, Integer)] -> [(String, Integer)]
forall a. a -> [a] -> [a]
: [(String, Integer)] -> [(String, Integer)]
removeConflictingVars [(String, Integer)]
vs

    findAllFloatVars :: E -> [(String, Integer)]
findAllFloatVars (EBinOp BinOp
_ E
e1 E
e2) = E -> [(String, Integer)]
knownFloatVars E
e1 [(String, Integer)] -> [(String, Integer)] -> [(String, Integer)]
forall a. [a] -> [a] -> [a]
++ E -> [(String, Integer)]
knownFloatVars E
e2
    findAllFloatVars (EUnOp UnOp
_ E
e) = E -> [(String, Integer)]
knownFloatVars E
e
    findAllFloatVars (PowI E
e Integer
_) = E -> [(String, Integer)]
knownFloatVars E
e
    findAllFloatVars (Float RoundingMode
_ E
e) = E -> [(String, Integer)]
knownFloatVars E
e
    findAllFloatVars (Float32 RoundingMode
_ (Var String
v)) = [(String
v, Integer
32)]
    findAllFloatVars (Float64 RoundingMode
_ (Var String
v)) = [(String
v, Integer
64)]
    findAllFloatVars (Float32 RoundingMode
_ E
e) = E -> [(String, Integer)]
knownFloatVars E
e
    findAllFloatVars (Float64 RoundingMode
_ E
e) = E -> [(String, Integer)]
knownFloatVars E
e
    findAllFloatVars (RoundToInteger RoundingMode
_ E
e) = E -> [(String, Integer)]
knownFloatVars E
e
    findAllFloatVars (Var String
_) = []
    findAllFloatVars (Lit Rational
_) = []
    findAllFloatVars E
Pi = []

findVariablesInFormula :: F -> [String]
findVariablesInFormula :: F -> [String]
findVariablesInFormula F
f = [String] -> [String]
forall a. Eq a => [a] -> [a]
nub ([String] -> [String]) -> [String] -> [String]
forall a b. (a -> b) -> a -> b
$ F -> [String]
findVars F
f
  where
    findVars :: F -> [String]
findVars (FConn Conn
_ F
f1 F
f2) = F -> [String]
findVars F
f1 [String] -> [String] -> [String]
forall a. [a] -> [a] -> [a]
++ F -> [String]
findVars F
f2
    findVars (FComp Comp
_ E
e1 E
e2) = E -> [String]
findVariablesInExpressions E
e1 [String] -> [String] -> [String]
forall a. [a] -> [a] -> [a]
++ E -> [String]
findVariablesInExpressions E
e2
    findVars (FNot F
f1)       = F -> [String]
findVars F
f1
    findVars F
FTrue           = []
    findVars F
FFalse          = []

findVariablesInExpressions :: E -> [String]
findVariablesInExpressions :: E -> [String]
findVariablesInExpressions (EBinOp BinOp
_ E
e1 E
e2) = E -> [String]
findVariablesInExpressions E
e1 [String] -> [String] -> [String]
forall a. [a] -> [a] -> [a]
++ E -> [String]
findVariablesInExpressions E
e2
findVariablesInExpressions (EUnOp UnOp
_ E
e) = E -> [String]
findVariablesInExpressions E
e
findVariablesInExpressions (PowI E
e Integer
_) = E -> [String]
findVariablesInExpressions E
e
findVariablesInExpressions (Float RoundingMode
_ E
e) = E -> [String]
findVariablesInExpressions E
e
findVariablesInExpressions (Float32 RoundingMode
_ E
e) = E -> [String]
findVariablesInExpressions E
e
findVariablesInExpressions (Float64 RoundingMode
_ E
e) = E -> [String]
findVariablesInExpressions E
e
findVariablesInExpressions (RoundToInteger RoundingMode
_ E
e) = E -> [String]
findVariablesInExpressions E
e
findVariablesInExpressions (Var String
v) = [String
v]
findVariablesInExpressions (Lit Rational
_) = []
findVariablesInExpressions E
Pi      = []

parseRoundingMode :: LD.Expression -> Maybe RoundingMode
parseRoundingMode :: Expression -> Maybe RoundingMode
parseRoundingMode (LD.Variable String
mode) =
  case String
mode of
    String
m
      | String
m String -> [String] -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` [String
"RNE", String
"NearestTiesToEven"] -> RoundingMode -> Maybe RoundingMode
forall a. a -> Maybe a
Just RoundingMode
RNE
      | String
m String -> [String] -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` [String
"RTP", String
"Up"]                -> RoundingMode -> Maybe RoundingMode
forall a. a -> Maybe a
Just RoundingMode
RTP
      | String
m String -> [String] -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` [String
"RTN", String
"Down"]              -> RoundingMode -> Maybe RoundingMode
forall a. a -> Maybe a
Just RoundingMode
RTN
      | String
m String -> [String] -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` [String
"RTZ", String
"ToZero"]            -> RoundingMode -> Maybe RoundingMode
forall a. a -> Maybe a
Just RoundingMode
RTZ
      | String
m String -> [String] -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` [String
"RNA"]                      -> RoundingMode -> Maybe RoundingMode
forall a. a -> Maybe a
Just RoundingMode
RNA
    String
_                                         -> Maybe RoundingMode
forall a. Maybe a
Nothing
parseRoundingMode Expression
_ = Maybe RoundingMode
forall a. Maybe a
Nothing

-- |Process a parsed list of expressions to a VC. 
-- 
-- If the parsing mode is Why3, everything in the context implies the goal (empty context means we only have a goal). 
-- If the goal cannot be parsed, we return Nothing.
-- 
-- If the parsing mode is CNF, parse all assertions into a CNF. If any assertion cannot be parsed, return Nothing.
-- If any assertion contains Floats, return Nothing.
processVC :: [LD.Expression] -> Maybe (F, [(String, String)])
processVC :: [Expression] -> Maybe (F, [(String, String)])
processVC [Expression]
parsedExpressions =
  (F, [(String, String)]) -> Maybe (F, [(String, String)])
forall a. a -> Maybe a
Just ([F] -> F
foldAssertionsF [F]
assertionsF, [(String, String)]
variablesWithTypes)
  where
    assertions :: [Expression]
assertions  = [Expression] -> [Expression]
findAssertions [Expression]
parsedExpressions
    assertionsF :: [F]
assertionsF = (F -> Maybe F) -> [F] -> [F]
forall a b. (a -> Maybe b) -> [a] -> [b]
mapMaybe (F -> [(String, String)] -> Maybe F
`determineFloatTypeF` [(String, String)]
variablesWithTypes) ([F] -> [F]) -> [F] -> [F]
forall a b. (a -> b) -> a -> b
$ ([Expression] -> [(String, ([String], String))] -> [F]
termsToF ([Expression] -> [(String, ([String], String))] -> [F])
-> ([Expression] -> [Expression])
-> [Expression]
-> [(String, ([String], String))]
-> [F]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [Expression] -> [Expression]
eliminateKnownFunctionGuards ([Expression] -> [Expression])
-> ([Expression] -> [Expression]) -> [Expression] -> [Expression]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [Expression] -> [Expression]
collapseOrs)  [Expression]
assertions [(String, ([String], String))]
functionsWithInputsAndOutputs

    variablesWithTypes :: [(String, String)]
variablesWithTypes  = [Expression] -> [(String, String)]
findVariables [Expression]
parsedExpressions
    functionsWithInputsAndOutputs :: [(String, ([String], String))]
functionsWithInputsAndOutputs = [Expression] -> [(String, ([String], String))]
findFunctionInputsAndOutputs [Expression]
parsedExpressions

    foldAssertionsF :: [F] -> F
    foldAssertionsF :: [F] -> F
foldAssertionsF []       = String -> F
forall a. HasCallStack => String -> a
error String
"processVC - foldAssertionsF: Empty list given"
    foldAssertionsF [F
f]      = F
f
    foldAssertionsF (F
f : [F]
fs) = Conn -> F -> F -> F
FConn Conn
And F
f ([F] -> F
foldAssertionsF [F]
fs)

-- |Looks for pi vars (vars named pi/pi{i} where {i} is some integer) and symbolic bounds.
-- If the bounds are better than those given to the real pi in Why3, replace the variable with exact pi.
symbolicallySubstitutePiVars :: F -> F
symbolicallySubstitutePiVars :: F -> F
symbolicallySubstitutePiVars F
f = [String] -> F -> F
substVarsWithPi [String]
piVars F
f
  where
    piVars :: [String]
piVars = [String] -> [String]
forall a. Eq a => [a] -> [a]
nub (F -> [String]
aux F
f)

    substVarsWithPi :: [String] -> F -> F
    substVarsWithPi :: [String] -> F -> F
substVarsWithPi [] F
f' = F
f'
    substVarsWithPi (String
v : [String]
_) F
f' = String -> F -> E -> F
substVarFWithE String
v F
f' E
Pi

    aux :: F -> [String]
    aux :: F -> [String]
aux (FConn Conn
And F
f1 F
f2) = F -> [String]
aux F
f1 [String] -> [String] -> [String]
forall a. [a] -> [a] -> [a]
++ F -> [String]
aux F
f2
    aux (FComp Comp
Lt (EBinOp BinOp
Div (Lit Rational
numer) (Lit Rational
denom)) (Var String
var)) =
      [String
var | 
        -- If variable is pi or pi# where # is a number
        (String
var String -> String -> Bool
forall source source1 target.
(RegexMaker Regex CompOption ExecOption source,
 RegexContext Regex source1 target) =>
source1 -> source -> target
=~ String
"^pi$|^pi[0-9]+$" :: Bool) Bool -> Bool -> AndOrType Bool Bool
forall a b. CanAndOrAsymmetric a b => a -> b -> AndOrType a b
&&
        -- And bounds are equal or better than the bounds given by Why3 for Pi
        Rational
DivType Rational Rational
lb Rational -> Rational -> OrderCompareType Rational Rational
forall a b.
HasOrderAsymmetric a b =>
a -> b -> OrderCompareType a b
>= (Rational
7074237752028440.0 Rational -> Rational -> DivType Rational Rational
forall t1 t2. CanDiv t1 t2 => t1 -> t2 -> DivType t1 t2
/ Rational
2251799813685248.0) Bool -> Bool -> AndOrType Bool Bool
forall a b. CanAndOrAsymmetric a b => a -> b -> AndOrType a b
&&
        String -> F -> Bool
hasUB String
var F
f]
      where
        lb :: DivType Rational Rational
lb = Rational
numer Rational -> Rational -> DivType Rational Rational
forall t1 t2. CanDiv t1 t2 => t1 -> t2 -> DivType t1 t2
/ Rational
denom
    aux (FComp {}) = []
    aux (FConn {}) = []
    aux (FNot F
_) = []
    aux F
FTrue = []
    aux F
FFalse = []

    hasUB :: String -> F -> Bool
    hasUB :: String -> F -> Bool
hasUB String
piVar (FComp Comp
Lt (Var String
otherVar) (EBinOp BinOp
Div (Lit Rational
numer) (Lit Rational
denom))) = 
      String
piVar String -> String -> EqCompareType String String
forall a b. HasEqAsymmetric a b => a -> b -> EqCompareType a b
== String
otherVar Bool -> Bool -> AndOrType Bool Bool
forall a b. CanAndOrAsymmetric a b => a -> b -> AndOrType a b
&& Rational
DivType Rational Rational
ub Rational -> Rational -> OrderCompareType Rational Rational
forall a b.
HasOrderAsymmetric a b =>
a -> b -> OrderCompareType a b
<= (Rational
7074237752028441.0 Rational -> Rational -> DivType Rational Rational
forall t1 t2. CanDiv t1 t2 => t1 -> t2 -> DivType t1 t2
/ Rational
2251799813685248.0)
      where
        ub :: DivType Rational Rational
ub = Rational
numer Rational -> Rational -> DivType Rational Rational
forall t1 t2. CanDiv t1 t2 => t1 -> t2 -> DivType t1 t2
/ Rational
denom
    hasUB String
piVar (FConn Conn
And F
f1 F
f2) = String -> F -> Bool
hasUB String
piVar F
f1 Bool -> Bool -> AndOrType Bool Bool
forall a b. CanAndOrAsymmetric a b => a -> b -> AndOrType a b
|| String -> F -> Bool
hasUB String
piVar F
f2
    hasUB String
_ (FComp {}) = Bool
False
    hasUB String
_ (FConn {}) = Bool
False
    hasUB String
_ (FNot F
_) = Bool
False
    hasUB String
_ F
FTrue = Bool
False
    hasUB String
_ F
FFalse = Bool
False


-- |Derive ranges for a VC (Implication where a CNF implies a goal)
-- Remove anything which refers to a variable for which we cannot derive ranges
-- If the goal contains underivable variables, return Nothing
deriveVCRanges :: F -> [(String, String)] -> Maybe (F, TypedVarMap)
deriveVCRanges :: F -> [(String, String)] -> Maybe (F, TypedVarMap)
deriveVCRanges F
vc [(String, String)]
varsWithTypes =
  case F -> [String] -> Bool -> Maybe F
filterOutVars F
simplifiedF [String]
underivableVariables Bool
False of
    Just F
filteredF -> (F, TypedVarMap) -> Maybe (F, TypedVarMap)
forall a. a -> Maybe a
Just (F
filteredF, TypedVarMap -> TypedVarMap
safelyRoundTypedVarMap TypedVarMap
typedDerivedVarMap)
    Maybe F
Nothing -> Maybe (F, TypedVarMap)
forall a. Maybe a
Nothing
  where
    integerVariables :: [(String, VarType)]
integerVariables = [(String, String)] -> [(String, VarType)]
findIntegerVariables [(String, String)]
varsWithTypes

    (F
simplifiedFUnchecked, VarMap
derivedVarMapUnchecked, [String]
underivableVariables) = F -> (F, VarMap, [String])
deriveBoundsAndSimplify F
vc

    -- (piVars, derivedVarMap) = findRealPiVars derivedVarMapUnchecked
    ([Any]
piVars, VarMap
derivedVarMap) = ([], VarMap
derivedVarMapUnchecked)

    typedDerivedVarMap :: TypedVarMap
typedDerivedVarMap = VarMap -> [(String, VarType)] -> TypedVarMap
unsafeVarMapToTypedVarMap VarMap
derivedVarMap [(String, VarType)]
integerVariables

    -- safelyRoundTypedVarMap = id
    safelyRoundTypedVarMap :: TypedVarMap -> TypedVarMap
safelyRoundTypedVarMap [] = []
    safelyRoundTypedVarMap ((TypedVar (String
varName, (Rational
leftBound, Rational
rightBound)) VarType
Real) : TypedVarMap
vars)    =
      let
        leftBoundRoundedDown :: Rational
leftBoundRoundedDown = MPFloat -> Rational
forall t. CanBeRational t => t -> Rational
rational (MPFloat -> Rational) -> (MPBall -> MPFloat) -> MPBall -> Rational
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (MPFloat, MPFloat) -> MPFloat
forall a b. (a, b) -> a
fst ((MPFloat, MPFloat) -> MPFloat)
-> (MPBall -> (MPFloat, MPFloat)) -> MPBall -> MPFloat
forall b c a. (b -> c) -> (a -> b) -> a -> c
. MPBall -> (MPFloat, MPFloat)
forall i.
IsInterval i =>
i -> (IntervalEndpoint i, IntervalEndpoint i)
endpoints (MPBall -> Rational) -> MPBall -> Rational
forall a b. (a -> b) -> a -> b
$ Precision -> Rational -> MPBall
forall t. CanBeMPBallP t => Precision -> t -> MPBall
mpBallP (Integer -> Precision
prec Integer
23) Rational
leftBound
        rightBoundRoundedUp :: Rational
rightBoundRoundedUp = MPFloat -> Rational
forall t. CanBeRational t => t -> Rational
rational (MPFloat -> Rational) -> (MPBall -> MPFloat) -> MPBall -> Rational
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (MPFloat, MPFloat) -> MPFloat
forall a b. (a, b) -> b
snd ((MPFloat, MPFloat) -> MPFloat)
-> (MPBall -> (MPFloat, MPFloat)) -> MPBall -> MPFloat
forall b c a. (b -> c) -> (a -> b) -> a -> c
. MPBall -> (MPFloat, MPFloat)
forall i.
IsInterval i =>
i -> (IntervalEndpoint i, IntervalEndpoint i)
endpoints (MPBall -> Rational) -> MPBall -> Rational
forall a b. (a -> b) -> a -> b
$ Precision -> Rational -> MPBall
forall t. CanBeMPBallP t => Precision -> t -> MPBall
mpBallP (Integer -> Precision
prec Integer
23) Rational
rightBound
        newBound :: TypedVarInterval
newBound = (String, (Rational, Rational)) -> VarType -> TypedVarInterval
TypedVar (String
varName, (Rational
leftBoundRoundedDown, Rational
rightBoundRoundedUp)) VarType
Real
      in
        TypedVarInterval
newBound TypedVarInterval -> TypedVarMap -> TypedVarMap
forall a. a -> [a] -> [a]
: TypedVarMap -> TypedVarMap
safelyRoundTypedVarMap TypedVarMap
vars
    safelyRoundTypedVarMap (vi :: TypedVarInterval
vi@(TypedVar (String, (Rational, Rational))
_                               VarType
Integer) : TypedVarMap
vars) = TypedVarInterval
vi TypedVarInterval -> TypedVarMap -> TypedVarMap
forall a. a -> [a] -> [a]
: TypedVarMap -> TypedVarMap
safelyRoundTypedVarMap TypedVarMap
vars

    -- simplifiedF = substVarsWithPi piVars simplifiedFUnchecked
    simplifiedF :: F
simplifiedF = F
simplifiedFUnchecked

    -- TODO: Would be good to include a warning when this happens
    -- Could also make this an option
    -- First elem are the variables which can be assumed to be real pi
    -- Second elem is the varMap without the real pi vars
    findRealPiVars :: VarMap -> ([String], VarMap)
    findRealPiVars :: VarMap -> ([String], VarMap)
findRealPiVars [] = ([], [])
    findRealPiVars (varWithBounds :: (String, (Rational, Rational))
varWithBounds@(String
var, (Rational
l, Rational
r)) : VarMap
vars) =
      if
        -- If variable is pi or pi# where # is a number
        (String
var String -> String -> Bool
forall source source1 target.
(RegexMaker Regex CompOption ExecOption source,
 RegexContext Regex source1 target) =>
source1 -> source -> target
=~ String
"^pi$|^pi[0-9]+$" :: Bool) Bool -> Bool -> AndOrType Bool Bool
forall a b. CanAndOrAsymmetric a b => a -> b -> AndOrType a b
&&
        -- And bounds are equal or better than the bounds given by Why3 for Pi
        Rational
l Rational -> Rational -> OrderCompareType Rational Rational
forall a b.
HasOrderAsymmetric a b =>
a -> b -> OrderCompareType a b
>= (Rational
7074237752028440.0 Rational -> Rational -> DivType Rational Rational
forall t1 t2. CanDiv t1 t2 => t1 -> t2 -> DivType t1 t2
/ Rational
2251799813685248.0) Bool -> Bool -> AndOrType Bool Bool
forall a b. CanAndOrAsymmetric a b => a -> b -> AndOrType a b
&& Rational
r Rational -> Rational -> OrderCompareType Rational Rational
forall a b.
HasOrderAsymmetric a b =>
a -> b -> OrderCompareType a b
<= (Rational
7074237752028441.0 Rational -> Rational -> DivType Rational Rational
forall t1 t2. CanDiv t1 t2 => t1 -> t2 -> DivType t1 t2
/ Rational
2251799813685248.0) Bool -> Bool -> AndOrType Bool Bool
forall a b. CanAndOrAsymmetric a b => a -> b -> AndOrType a b
&&
        -- And the type of the variable is Real
        (String -> [(String, String)] -> Maybe String
forall a b. Eq a => a -> [(a, b)] -> Maybe b
lookup String
var [(String, String)]
varsWithTypes Maybe String
-> Maybe String -> EqCompareType (Maybe String) (Maybe String)
forall a b. HasEqAsymmetric a b => a -> b -> EqCompareType a b
== String -> Maybe String
forall a. a -> Maybe a
Just String
"Real")
          then (\([String]
foundPiVars, VarMap
varMapWithoutPi) -> ((String
var String -> [String] -> [String]
forall a. a -> [a] -> [a]
: [String]
foundPiVars), VarMap
varMapWithoutPi))           (([String], VarMap) -> ([String], VarMap))
-> ([String], VarMap) -> ([String], VarMap)
forall a b. (a -> b) -> a -> b
$ VarMap -> ([String], VarMap)
findRealPiVars VarMap
vars
          else (\([String]
foundPiVars, VarMap
varMapWithoutPi) -> ([String]
foundPiVars, ((String, (Rational, Rational))
varWithBounds (String, (Rational, Rational)) -> VarMap -> VarMap
forall a. a -> [a] -> [a]
: VarMap
varMapWithoutPi))) (([String], VarMap) -> ([String], VarMap))
-> ([String], VarMap) -> ([String], VarMap)
forall a b. (a -> b) -> a -> b
$ VarMap -> ([String], VarMap)
findRealPiVars VarMap
vars

    substVarsWithPi :: [String] -> F -> F
    substVarsWithPi :: [String] -> F -> F
substVarsWithPi [] F
f = F
f
    substVarsWithPi (String
v : [String]
_) F
f = String -> F -> E -> F
substVarFWithE String
v F
f E
Pi


    -- |Safely filter our terms that contain underivable variables.
    -- Need to preserve unsat terms, so we can safely remove x in FConn And x y if x contains underivable variables.
    -- We cannot safely remove x from FConn Or x y if x contains underivable variables
    -- (since x may be sat and y may be unsat, filtering out x would give an incorrect unsat result), so we remove the whole term
    -- Reverse logic as appropriate when a term is negated
    filterOutVars :: F -> [String] -> Bool -> Maybe F
    filterOutVars :: F -> [String] -> Bool -> Maybe F
filterOutVars (FConn Conn
And F
f1 F
f2) [String]
vars Bool
False =
      case (F -> [String] -> Bool -> Maybe F
filterOutVars F
f1 [String]
vars Bool
False, F -> [String] -> Bool -> Maybe F
filterOutVars F
f2 [String]
vars Bool
False) of
        (Just F
ff1, Just F
ff2) -> F -> Maybe F
forall a. a -> Maybe a
Just (F -> Maybe F) -> F -> Maybe F
forall a b. (a -> b) -> a -> b
$ Conn -> F -> F -> F
FConn Conn
And F
ff1 F
ff2
        (Just F
ff1, Maybe F
_)        -> F -> Maybe F
forall a. a -> Maybe a
Just F
ff1
        (Maybe F
_, Just F
ff2)        -> F -> Maybe F
forall a. a -> Maybe a
Just F
ff2
        (Maybe F
_, Maybe F
_)               -> Maybe F
forall a. Maybe a
Nothing
    filterOutVars (FConn Conn
Or F
f1 F
f2) [String]
vars Bool
False =
      case (F -> [String] -> Bool -> Maybe F
filterOutVars F
f1 [String]
vars Bool
False, F -> [String] -> Bool -> Maybe F
filterOutVars F
f2 [String]
vars Bool
False) of
        (Just F
ff1, Just F
ff2) -> F -> Maybe F
forall a. a -> Maybe a
Just (F -> Maybe F) -> F -> Maybe F
forall a b. (a -> b) -> a -> b
$ Conn -> F -> F -> F
FConn Conn
Or F
ff1 F
ff2
        (Maybe F
_, Maybe F
_)               -> Maybe F
forall a. Maybe a
Nothing
    filterOutVars (FConn Conn
Impl F
f1 F
f2) [String]
vars Bool
False =
      case (F -> [String] -> Bool -> Maybe F
filterOutVars F
f1 [String]
vars Bool
False, F -> [String] -> Bool -> Maybe F
filterOutVars F
f2 [String]
vars Bool
False) of
        (Just F
ff1, Just F
ff2) -> F -> Maybe F
forall a. a -> Maybe a
Just (F -> Maybe F) -> F -> Maybe F
forall a b. (a -> b) -> a -> b
$ Conn -> F -> F -> F
FConn Conn
Impl F
ff1 F
ff2
        (Maybe F
_, Maybe F
_)               -> Maybe F
forall a. Maybe a
Nothing
    filterOutVars (FConn Conn
And F
f1 F
f2) [String]
vars Bool
True =
      case (F -> [String] -> Bool -> Maybe F
filterOutVars F
f1 [String]
vars Bool
True, F -> [String] -> Bool -> Maybe F
filterOutVars F
f2 [String]
vars Bool
True) of
        (Just F
ff1, Just F
ff2) -> F -> Maybe F
forall a. a -> Maybe a
Just (F -> Maybe F) -> F -> Maybe F
forall a b. (a -> b) -> a -> b
$ Conn -> F -> F -> F
FConn Conn
And F
ff1 F
ff2
        (Maybe F
_, Maybe F
_)               -> Maybe F
forall a. Maybe a
Nothing
    filterOutVars (FConn Conn
Or F
f1 F
f2) [String]
vars Bool
True =
      case (F -> [String] -> Bool -> Maybe F
filterOutVars F
f1 [String]
vars Bool
True, F -> [String] -> Bool -> Maybe F
filterOutVars F
f2 [String]
vars Bool
True) of
        (Just F
ff1, Just F
ff2) -> F -> Maybe F
forall a. a -> Maybe a
Just (F -> Maybe F) -> F -> Maybe F
forall a b. (a -> b) -> a -> b
$ Conn -> F -> F -> F
FConn Conn
Or F
ff1 F
ff2
        (Just F
ff1, Maybe F
_)        -> F -> Maybe F
forall a. a -> Maybe a
Just F
ff1
        (Maybe F
_, Just F
ff2)        -> F -> Maybe F
forall a. a -> Maybe a
Just F
ff2
        (Maybe F
_, Maybe F
_)               -> Maybe F
forall a. Maybe a
Nothing
    filterOutVars (FConn Conn
Impl F
f1 F
f2) [String]
vars Bool
True =
      case (F -> [String] -> Bool -> Maybe F
filterOutVars F
f1 [String]
vars Bool
True, F -> [String] -> Bool -> Maybe F
filterOutVars F
f2 [String]
vars Bool
True) of
        (Just F
ff1, Just F
ff2) -> F -> Maybe F
forall a. a -> Maybe a
Just (F -> Maybe F) -> F -> Maybe F
forall a b. (a -> b) -> a -> b
$ Conn -> F -> F -> F
FConn Conn
Impl F
ff1 F
ff2
        (Just F
ff1, Maybe F
_)        -> F -> Maybe F
forall a. a -> Maybe a
Just F
ff1
        (Maybe F
_, Just F
ff2)        -> F -> Maybe F
forall a. a -> Maybe a
Just F
ff2
        (Maybe F
_, Maybe F
_)               -> Maybe F
forall a. Maybe a
Nothing
    filterOutVars (FNot F
f) [String]
vars Bool
isNegated = F -> F
FNot (F -> F) -> Maybe F -> Maybe F
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> F -> [String] -> Bool -> Maybe F
filterOutVars F
f [String]
vars (Bool -> NegType Bool
forall t. CanNeg t => t -> NegType t
not Bool
isNegated)

    filterOutVars (FComp Comp
op E
e1 E
e2) [String]
vars Bool
_isNegated =
      if [String] -> E -> Bool
eContainsVars [String]
vars E
e1 Bool -> Bool -> AndOrType Bool Bool
forall a b. CanAndOrAsymmetric a b => a -> b -> AndOrType a b
|| [String] -> E -> Bool
eContainsVars [String]
vars E
e2
        then Maybe F
forall a. Maybe a
Nothing
        else F -> Maybe F
forall a. a -> Maybe a
Just (Comp -> E -> E -> F
FComp Comp
op E
e1 E
e2)

    filterOutVars F
FTrue  [String]
_ Bool
_ = F -> Maybe F
forall a. a -> Maybe a
Just F
FTrue
    filterOutVars F
FFalse [String]
_ Bool
_ = F -> Maybe F
forall a. a -> Maybe a
Just F
FFalse

eContainsVars :: [String] -> E -> Bool
eContainsVars :: [String] -> E -> Bool
eContainsVars [String]
vars (Var String
var)        = String
var String -> [String] -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` [String]
vars
eContainsVars [String]
_ (Lit Rational
_)             = Bool
False
eContainsVars [String]
_ E
Pi                  = Bool
False

eContainsVars [String]
vars (EBinOp BinOp
_ E
e1 E
e2) = [String] -> E -> Bool
eContainsVars [String]
vars E
e1 Bool -> Bool -> AndOrType Bool Bool
forall a b. CanAndOrAsymmetric a b => a -> b -> AndOrType a b
|| [String] -> E -> Bool
eContainsVars [String]
vars E
e2
eContainsVars [String]
vars (EUnOp UnOp
_ E
e)      = [String] -> E -> Bool
eContainsVars [String]
vars E
e
eContainsVars [String]
vars (PowI E
e Integer
_)       = [String] -> E -> Bool
eContainsVars [String]
vars E
e
eContainsVars [String]
vars (Float32 RoundingMode
_ E
e)    = [String] -> E -> Bool
eContainsVars [String]
vars E
e
eContainsVars [String]
vars (Float64 RoundingMode
_ E
e)    = [String] -> E -> Bool
eContainsVars [String]
vars E
e
eContainsVars [String]
vars (Float RoundingMode
_ E
e)      = [String] -> E -> Bool
eContainsVars [String]
vars E
e
eContainsVars [String]
vars (RoundToInteger RoundingMode
_ E
e) = [String] -> E -> Bool
eContainsVars [String]
vars E
e

fContainsVars :: [String] -> F -> Bool
fContainsVars :: [String] -> F -> Bool
fContainsVars [String]
vars (FConn Conn
_ F
f1 F
f2)  = [String] -> F -> Bool
fContainsVars [String]
vars F
f1 Bool -> Bool -> AndOrType Bool Bool
forall a b. CanAndOrAsymmetric a b => a -> b -> AndOrType a b
|| [String] -> F -> Bool
fContainsVars [String]
vars F
f2
fContainsVars [String]
vars (FComp Comp
_ E
e1 E
e2)  = [String] -> E -> Bool
eContainsVars [String]
vars E
e1 Bool -> Bool -> AndOrType Bool Bool
forall a b. CanAndOrAsymmetric a b => a -> b -> AndOrType a b
|| [String] -> E -> Bool
eContainsVars [String]
vars E
e2
fContainsVars [String]
vars (FNot F
f)         = [String] -> F -> Bool
fContainsVars [String]
vars F
f
fContainsVars [String]
_ F
FTrue               = Bool
False
fContainsVars [String]
_ F
FFalse              = Bool
False

inequalityEpsilon :: Rational
inequalityEpsilon :: Rational
inequalityEpsilon = Rational
0.000000001
-- inequalityEpsilon = 1/(2^23)

findVarEqualities :: F -> [(String, E)]
findVarEqualities :: F -> [(String, E)]
findVarEqualities (FConn Conn
And F
f1 F
f2)     = F -> [(String, E)]
findVarEqualities F
f1 [(String, E)] -> [(String, E)] -> [(String, E)]
forall a. [a] -> [a] -> [a]
++ F -> [(String, E)]
findVarEqualities F
f2
findVarEqualities FConn {}              = []
findVarEqualities (FComp Comp
Eq (Var String
v) E
e2) = [(String
v, E
e2)]
findVarEqualities (FComp Comp
Eq E
e1 (Var String
v)) = [(String
v, E
e1)]
findVarEqualities FComp {}              = []
findVarEqualities (FNot F
_)              = [] -- Not EQ, means we can't do anything here?
findVarEqualities F
FTrue                 = []
findVarEqualities F
FFalse                = []

-- |Filter out var equalities which rely on themselves
filterOutCircularVarEqualities :: [(String, E)] -> [(String, E)]
filterOutCircularVarEqualities :: [(String, E)] -> [(String, E)]
filterOutCircularVarEqualities = ((String, E) -> Bool) -> [(String, E)] -> [(String, E)]
forall a. (a -> Bool) -> [a] -> [a]
filter (\(String
v, E
e) -> String
v String -> [String] -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`notElem` E -> [String]
findVariablesInExpressions E
e)

-- |Filter out var equalities which occur multiple times by choosing the var equality with the smallest length
filterOutDuplicateVarEqualities :: [(String, E)] -> [(String, E)]
filterOutDuplicateVarEqualities :: [(String, E)] -> [(String, E)]
filterOutDuplicateVarEqualities [] = []
filterOutDuplicateVarEqualities ((String
v, E
e) : [(String, E)]
vs) =
  case ((String, E) -> Bool)
-> [(String, E)] -> ([(String, E)], [(String, E)])
forall a. (a -> Bool) -> [a] -> ([a], [a])
partition (\(String
v',E
_) -> String
v String -> String -> EqCompareType String String
forall a b. HasEqAsymmetric a b => a -> b -> EqCompareType a b
== String
v')  [(String, E)]
vs of
    ([], [(String, E)]
_) -> (String
v, E
e) (String, E) -> [(String, E)] -> [(String, E)]
forall a. a -> [a] -> [a]
: [(String, E)] -> [(String, E)]
filterOutDuplicateVarEqualities [(String, E)]
vs
    ([(String, E)]
matchingEqualities, [(String, E)]
otherEqualities) ->
      let shortestVarEquality :: (String, E)
shortestVarEquality = [(String, E)] -> (String, E)
forall a. [a] -> a
head ([(String, E)] -> (String, E)) -> [(String, E)] -> (String, E)
forall a b. (a -> b) -> a -> b
$ ((String, E) -> (String, E) -> Ordering)
-> [(String, E)] -> [(String, E)]
forall a. (a -> a -> Ordering) -> [a] -> [a]
sortBy (\(String
_, E
e1) (String
_, E
e2) -> Integer -> Integer -> Ordering
forall a. Ord a => a -> a -> Ordering
P.compare (E -> Integer
lengthE E
e1) (E -> Integer
lengthE E
e2)) ([(String, E)] -> [(String, E)]) -> [(String, E)] -> [(String, E)]
forall a b. (a -> b) -> a -> b
$ (String
v, E
e) (String, E) -> [(String, E)] -> [(String, E)]
forall a. a -> [a] -> [a]
: [(String, E)]
matchingEqualities
      in (String, E)
shortestVarEquality (String, E) -> [(String, E)] -> [(String, E)]
forall a. a -> [a] -> [a]
: [(String, E)] -> [(String, E)]
filterOutDuplicateVarEqualities [(String, E)]
otherEqualities

-- FIXME: subst one at a time
substAllEqualities :: F -> F
substAllEqualities :: F -> F
substAllEqualities = F -> F
recursivelySubstVars
  where
    recursivelySubstVars :: F -> F
recursivelySubstVars f :: F
f@(FConn Conn
Impl F
context F
_) =
      case [(String, E)]
filteredVarEqualities of
        [] -> F
f
        [(String, E)]
_  -> if F
f F -> F -> Bool
forall a. Eq a => a -> a -> Bool
P.== F
substitutedF then F
f else F -> F
recursivelySubstVars (F -> F) -> (F -> F) -> F -> F
forall b c a. (b -> c) -> (a -> b) -> a -> c
. F -> F
simplifyF (F -> F) -> F -> F
forall a b. (a -> b) -> a -> b
$ F
substitutedF -- TODO: make this a var
      where
        substitutedF :: F
substitutedF = [(String, E)] -> F -> F
substVars [(String, E)]
filteredVarEqualities F
f
        filteredVarEqualities :: [(String, E)]
filteredVarEqualities = ([(String, E)] -> [(String, E)]
filterOutDuplicateVarEqualities ([(String, E)] -> [(String, E)])
-> ([(String, E)] -> [(String, E)])
-> [(String, E)]
-> [(String, E)]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [(String, E)] -> [(String, E)]
filterOutCircularVarEqualities) [(String, E)]
varEqualities
        varEqualities :: [(String, E)]
varEqualities = F -> [(String, E)]
findVarEqualities F
context

    recursivelySubstVars F
f =
      case [(String, E)]
filteredVarEqualities of
        [] -> F
f
        [(String, E)]
_  -> if F
f F -> F -> Bool
forall a. Eq a => a -> a -> Bool
P.== F
substitutedF then F
f else  F -> F
recursivelySubstVars (F -> F) -> (F -> F) -> F -> F
forall b c a. (b -> c) -> (a -> b) -> a -> c
. F -> F
simplifyF (F -> F) -> F -> F
forall a b. (a -> b) -> a -> b
$ F
substitutedF
      where
        substitutedF :: F
substitutedF = [(String, E)] -> F -> F
substVars [(String, E)]
filteredVarEqualities F
f
        filteredVarEqualities :: [(String, E)]
filteredVarEqualities = ([(String, E)] -> [(String, E)]
filterOutDuplicateVarEqualities ([(String, E)] -> [(String, E)])
-> ([(String, E)] -> [(String, E)])
-> [(String, E)]
-> [(String, E)]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [(String, E)] -> [(String, E)]
filterOutCircularVarEqualities) [(String, E)]
varEqualities
        varEqualities :: [(String, E)]
varEqualities = F -> [(String, E)]
findVarEqualities F
f

    substVars :: [(String, E)] -> F -> F
substVars [] F
f = F
f
    substVars ((String
v, E
e) : [(String, E)]
_) F
f = String -> F -> E -> F
substVarFWithE String
v F
f E
e

addVarMapBoundsToF :: F -> TypedVarMap -> F
addVarMapBoundsToF :: F -> TypedVarMap -> F
addVarMapBoundsToF F
f [] = F
f
addVarMapBoundsToF F
f (TypedVar (String
v, (Rational
l, Rational
r)) VarType
_ : TypedVarMap
vm) = Conn -> F -> F -> F
FConn Conn
And F
boundAsF (F -> F) -> F -> F
forall a b. (a -> b) -> a -> b
$ F -> TypedVarMap -> F
addVarMapBoundsToF F
f TypedVarMap
vm
  where
    boundAsF :: F
boundAsF = Conn -> F -> F -> F
FConn Conn
And (Comp -> E -> E -> F
FComp Comp
Ge (String -> E
Var String
v) (Rational -> E
Lit Rational
l)) (Comp -> E -> E -> F
FComp Comp
Le (String -> E
Var String
v) (Rational -> E
Lit Rational
r))

eliminateFloatsAndSimplifyVC :: F -> TypedVarMap -> Bool -> FilePath -> IO F
eliminateFloatsAndSimplifyVC :: F -> TypedVarMap -> Bool -> String -> IO F
eliminateFloatsAndSimplifyVC F
vc TypedVarMap
typedVarMap Bool
strengthenVC String
fptaylorPath =
  do
    F
vcWithoutFloats <- F -> VarMap -> Bool -> String -> IO F
eliminateFloatsF F
vc (TypedVarMap -> VarMap
typedVarMapToVarMap TypedVarMap
typedVarMap) Bool
strengthenVC String
fptaylorPath
    let typedVarMapAsMap :: Map String (Maybe Rational, Maybe Rational)
typedVarMapAsMap = [(String, (Maybe Rational, Maybe Rational))]
-> Map String (Maybe Rational, Maybe Rational)
forall k a. Ord k => [(k, a)] -> Map k a
M.fromList ([(String, (Maybe Rational, Maybe Rational))]
 -> Map String (Maybe Rational, Maybe Rational))
-> [(String, (Maybe Rational, Maybe Rational))]
-> Map String (Maybe Rational, Maybe Rational)
forall a b. (a -> b) -> a -> b
$ (TypedVarInterval -> (String, (Maybe Rational, Maybe Rational)))
-> TypedVarMap -> [(String, (Maybe Rational, Maybe Rational))]
forall a b. (a -> b) -> [a] -> [b]
map (\(TypedVar (String
varName, (Rational
leftBound, Rational
rightBound)) VarType
_) -> (String
varName, (Rational -> Maybe Rational
forall a. a -> Maybe a
Just Rational
leftBound, Rational -> Maybe Rational
forall a. a -> Maybe a
Just Rational
rightBound))) TypedVarMap
typedVarMap
    let simplifiedVCWithoutFloats :: F
simplifiedVCWithoutFloats = (F -> F
simplifyF (F -> F) -> (F -> F) -> F -> F
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Map String (Maybe Rational, Maybe Rational) -> F -> F
evalF_comparisons Map String (Maybe Rational, Maybe Rational)
typedVarMapAsMap) F
vcWithoutFloats
    F -> IO F
forall (m :: * -> *) a. Monad m => a -> m a
return F
simplifiedVCWithoutFloats

parseVCToF :: FilePath -> FilePath -> IO (Maybe (F, TypedVarMap))
parseVCToF :: String -> String -> IO (Maybe (F, TypedVarMap))
parseVCToF String
filePath String
fptaylorPath =
  do
    [Expression]
parsedFile  <- String -> IO [Expression]
parseSMT2 String
filePath

    case [Expression] -> Maybe (F, [(String, String)])
processVC [Expression]
parsedFile of
      Just (F
vc, [(String, String)]
varTypes) ->
        let
          simplifiedVC :: F
simplifiedVC = (F -> F
symbolicallySubstitutePiVars (F -> F) -> (F -> F) -> F -> F
forall b c a. (b -> c) -> (a -> b) -> a -> c
. F -> F
substAllEqualities (F -> F) -> (F -> F) -> F -> F
forall b c a. (b -> c) -> (a -> b) -> a -> c
. F -> F
simplifyF) F
vc
          mDerivedVCWithRanges :: Maybe (F, TypedVarMap)
mDerivedVCWithRanges = F -> [(String, String)] -> Maybe (F, TypedVarMap)
deriveVCRanges F
simplifiedVC [(String, String)]
varTypes
        in
        case Maybe (F, TypedVarMap)
mDerivedVCWithRanges of
          Just (F
derivedVC, TypedVarMap
derivedRanges) ->
            do
              -- The file we are given is assumed to be a contradiction, so weaken the VC
              let strengthenVC :: Bool
strengthenVC = Bool
False
              F
vcWithoutFloats <- F -> VarMap -> Bool -> String -> IO F
eliminateFloatsF F
derivedVC (TypedVarMap -> VarMap
typedVarMapToVarMap TypedVarMap
derivedRanges) Bool
strengthenVC String
fptaylorPath
              let vcWithoutFloatsWithBounds :: F
vcWithoutFloatsWithBounds = F -> TypedVarMap -> F
addVarMapBoundsToF F
vcWithoutFloats TypedVarMap
derivedRanges
              case F -> [(String, String)] -> Maybe (F, TypedVarMap)
deriveVCRanges F
vcWithoutFloatsWithBounds [(String, String)]
varTypes of
                Just (F
simplifiedVCWithoutFloats, TypedVarMap
finalDerivedRanges) -> Maybe (F, TypedVarMap) -> IO (Maybe (F, TypedVarMap))
forall (m :: * -> *) a. Monad m => a -> m a
return (Maybe (F, TypedVarMap) -> IO (Maybe (F, TypedVarMap)))
-> Maybe (F, TypedVarMap) -> IO (Maybe (F, TypedVarMap))
forall a b. (a -> b) -> a -> b
$ (F, TypedVarMap) -> Maybe (F, TypedVarMap)
forall a. a -> Maybe a
Just (F
simplifiedVCWithoutFloats, TypedVarMap
finalDerivedRanges)
                Maybe (F, TypedVarMap)
Nothing -> String -> IO (Maybe (F, TypedVarMap))
forall a. HasCallStack => String -> a
error String
"Error deriving bounds again after floating-point elimination"
          Maybe (F, TypedVarMap)
Nothing -> Maybe (F, TypedVarMap) -> IO (Maybe (F, TypedVarMap))
forall (m :: * -> *) a. Monad m => a -> m a
return Maybe (F, TypedVarMap)
forall a. Maybe a
Nothing
      Maybe (F, [(String, String)])
Nothing -> Maybe (F, TypedVarMap) -> IO (Maybe (F, TypedVarMap))
forall (m :: * -> *) a. Monad m => a -> m a
return Maybe (F, TypedVarMap)
forall a. Maybe a
Nothing

parseVCToSolver :: FilePath -> FilePath -> (F -> TypedVarMap -> String) -> Bool -> IO (Maybe String)
parseVCToSolver :: String
-> String
-> (F -> TypedVarMap -> String)
-> Bool
-> IO (Maybe String)
parseVCToSolver String
filePath String
fptaylorPath F -> TypedVarMap -> String
proverTranslator Bool
negateVC =
  do
    [Expression]
parsedFile <- String -> IO [Expression]
parseSMT2 String
filePath

    case [Expression] -> Maybe (F, [(String, String)])
processVC [Expression]
parsedFile of
      Just (F
vc, [(String, String)]
varTypes) ->
        let
          simplifiedVC :: F
simplifiedVC = (F -> F
substAllEqualities (F -> F) -> (F -> F) -> F -> F
forall b c a. (b -> c) -> (a -> b) -> a -> c
. F -> F
simplifyF) F
vc
          mDerivedVCWithRanges :: Maybe (F, TypedVarMap)
mDerivedVCWithRanges = F -> [(String, String)] -> Maybe (F, TypedVarMap)
deriveVCRanges F
simplifiedVC [(String, String)]
varTypes
        in
          case Maybe (F, TypedVarMap)
mDerivedVCWithRanges of
            Just (F
derivedVC, TypedVarMap
derivedRanges) ->
              do
                let strengthenVC :: Bool
strengthenVC = Bool
False
                F
vcWithoutFloats <- F -> VarMap -> Bool -> String -> IO F
eliminateFloatsF F
derivedVC (TypedVarMap -> VarMap
typedVarMapToVarMap TypedVarMap
derivedRanges) Bool
strengthenVC String
fptaylorPath
                let vcWithoutFloatsWithBounds :: F
vcWithoutFloatsWithBounds = F -> TypedVarMap -> F
addVarMapBoundsToF F
vcWithoutFloats TypedVarMap
derivedRanges
                case F -> [(String, String)] -> Maybe (F, TypedVarMap)
deriveVCRanges F
vcWithoutFloatsWithBounds [(String, String)]
varTypes of
                  Just (F
simplifiedVCWithoutFloats, TypedVarMap
finalDerivedRanges) ->
                    Maybe String -> IO (Maybe String)
forall (m :: * -> *) a. Monad m => a -> m a
return (Maybe String -> IO (Maybe String))
-> Maybe String -> IO (Maybe String)
forall a b. (a -> b) -> a -> b
$ String -> Maybe String
forall a. a -> Maybe a
Just (
                      F -> TypedVarMap -> String
proverTranslator
                      (
                        if Bool
negateVC
                          then
                            case F
simplifiedVCWithoutFloats of
                              FNot F
f -> F
f -- Eliminate double not
                              F
_      -> F -> F
FNot F
simplifiedVCWithoutFloats
                          else F
simplifiedVCWithoutFloats
                      )
                      TypedVarMap
finalDerivedRanges
                    )
                  Maybe (F, TypedVarMap)
Nothing -> String -> IO (Maybe String)
forall a. HasCallStack => String -> a
error String
"Error deriving bounds again after floating-point elimination"
                -- return $ Just (proverTranslator (if negateVC then simplifyF (FNot simplifiedVCWithoutFloats) else simplifiedVCWithoutFloats) derivedRanges)
            Maybe (F, TypedVarMap)
Nothing -> Maybe String -> IO (Maybe String)
forall (m :: * -> *) a. Monad m => a -> m a
return Maybe String
forall a. Maybe a
Nothing
      Maybe (F, [(String, String)])
Nothing -> Maybe String -> IO (Maybe String)
forall (m :: * -> *) a. Monad m => a -> m a
return Maybe String
forall a. Maybe a
Nothing